diff options
Diffstat (limited to 'testsuite/tests/unsatisfiable/T11503_Unsat.hs')
-rw-r--r-- | testsuite/tests/unsatisfiable/T11503_Unsat.hs | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/testsuite/tests/unsatisfiable/T11503_Unsat.hs b/testsuite/tests/unsatisfiable/T11503_Unsat.hs new file mode 100644 index 0000000000..a685daf066 --- /dev/null +++ b/testsuite/tests/unsatisfiable/T11503_Unsat.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE Haskell2010 #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module T11503_Unsat where + +import GHC.TypeError + ( Unsatisfiable, 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 = Unsatisfiable (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) (Unsatisfiable (Text "Impossible!")) + +head' :: 1 <= n => List n t -> t +head' (x :- _) = x +-- Should not have any pattern match warnings for Nil. |