content: {-# LANGUAGE Haskell2010 #-}
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE StandaloneKindSignatures #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  module T11503 where
  
  import GHC.TypeLits
    ( TypeError, ErrorMessage(..) )
  import GHC.TypeNats
    ( Nat, type (+), type (<=?) )
  import Data.Kind
    ( Constraint, Type )
  
  -- Example 1: from #11503
  
  type NotInt :: Type -> Constraint
  type family NotInt a where
    NotInt Int = TypeError (Text "That's Int, silly.")
    NotInt _   = (() :: Constraint)
  
  data T a where
    MkT1 :: a -> T a
    MkT2 :: NotInt a => T a
  
  foo :: T Int -> Int
  foo (MkT1 x) = x
  -- Should not have any pattern match warnings for MkT2.
  
  -- Example 2: from #20180
  
  type Assert :: Bool -> Constraint -> Constraint
  type family Assert check errMsg where
    Assert 'True  _errMsg = ()
    Assert _check errMsg  = errMsg
  
  type List :: Nat -> Type -> Type
  data List n t where
    Nil  :: List 0 t
    (:-) :: t -> List n t -> List (n+1) t
  
  type (<=) :: Nat -> Nat -> Constraint
  type family x <= y where
    x <= y = Assert (x <=? y) (TypeError (Text "Impossible!"))
  
  head' :: 1 <= n => List n t -> t
  head' (x :- _) = x
  -- Should not have any pattern match warnings for Nil.
  