diff options
Diffstat (limited to 'testsuite/tests/dependent/should_fail')
20 files changed, 222 insertions, 0 deletions
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.hs b/testsuite/tests/dependent/should_fail/BadTelescope.hs new file mode 100644 index 0000000000..acabffec54 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeInType #-} + +module BadTelescope where + +import Data.Kind + +data SameKind :: k -> k -> * + +data X a k (b :: k) (c :: SameKind a b) diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr new file mode 100644 index 0000000000..2fbc35a9ba --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr @@ -0,0 +1,9 @@ + +BadTelescope.hs:9:1: error: + • These kind and type variables: (a :: k) + k + (b :: k) + (c :: SameKind a b) + are out of dependency order. Perhaps try this ordering: + k (a :: k) (b :: k) (c :: SameKind a b) + • In the data type declaration for ‘X’ diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs new file mode 100644 index 0000000000..6237df4488 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE TypeInType, ExplicitForAll #-} + +module BadTelescope2 where + +import Data.Kind +import Data.Proxy + +data SameKind :: k -> k -> * + +foo :: forall a k (b :: k). SameKind a b +foo = undefined + +bar :: forall a (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d +bar = undefined diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr new file mode 100644 index 0000000000..2a9dc76310 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr @@ -0,0 +1,16 @@ + +BadTelescope2.hs:10:8: error: + • These kind and type variables: a k (b :: k) + are out of dependency order. Perhaps try this ordering: + k (a :: k) (b :: k) + • In the type signature: + foo :: forall a k (b :: k). SameKind a b + +BadTelescope2.hs:13:8: error: + • The kind of variable ‘b’, namely ‘Proxy a’, + depends on variable ‘a’ from an inner scope + Perhaps bind ‘b’ sometime after binding ‘a’ + NB: Implicitly-bound variables always come before other ones. + • In the type signature: + bar :: forall a (c :: Proxy b) (d :: Proxy a). + Proxy c -> SameKind b d diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.hs b/testsuite/tests/dependent/should_fail/BadTelescope3.hs new file mode 100644 index 0000000000..807479f634 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope3.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeInType, ExplicitForAll #-} + +module BadTelescope3 where + +import Data.Kind + +data SameKind :: k -> k -> * + +type S a k (b :: k) = SameKind a b diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr new file mode 100644 index 0000000000..4ea7458bb2 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr @@ -0,0 +1,6 @@ + +BadTelescope3.hs:9:1: error: + • These kind and type variables: (a :: k) k (b :: k) + are out of dependency order. Perhaps try this ordering: + k (a :: k) (b :: k) + • In the type synonym declaration for ‘S’ diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.hs b/testsuite/tests/dependent/should_fail/BadTelescope4.hs new file mode 100644 index 0000000000..566922a4a0 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope4.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE ExistentialQuantification, TypeInType #-} +module BadTelescope4 where + +import Data.Proxy +import Data.Kind + +data SameKind :: k -> k -> * + +data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d) + +data Borked a (b :: k) = forall (c :: k). B (Proxy c) + -- this last one is OK. But there was a bug involving renaming + -- that failed here, so the test case remains. diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr new file mode 100644 index 0000000000..158aec650d --- /dev/null +++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr @@ -0,0 +1,15 @@ + +BadTelescope4.hs:9:1: error: + • These kind and type variables: (a :: k1) + (c :: Proxy b) + (d :: Proxy a) + (x :: SameKind b d) + are out of dependency order. Perhaps try this ordering: + k1 + (a :: k1) + (b :: Proxy a) + (c :: Proxy b) + (d :: Proxy a) + (x :: SameKind b d) + NB: Implicitly declared kind variables are put first. + • In the data type declaration for ‘Bad’ diff --git a/testsuite/tests/dependent/should_fail/DepFail1.hs b/testsuite/tests/dependent/should_fail/DepFail1.hs new file mode 100644 index 0000000000..425a8159c4 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/DepFail1.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE TypeInType #-} + +module DepFail1 where + +data Proxy k (a :: k) = P + +z :: Proxy Bool +z = P + +a :: Proxy Int Bool +a = P diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr new file mode 100644 index 0000000000..630f010fa3 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr @@ -0,0 +1,12 @@ + +DepFail1.hs:7:6: error: + • Expecting one more argument to ‘Proxy Bool’ + Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’ + • In the type signature: + z :: Proxy Bool + +DepFail1.hs:10:16: error: + • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’ + • In the second argument of ‘Proxy’, namely ‘Bool’ + In the type signature: + a :: Proxy Int Bool diff --git a/testsuite/tests/dependent/should_fail/Makefile b/testsuite/tests/dependent/should_fail/Makefile new file mode 100644 index 0000000000..13938e423d --- /dev/null +++ b/testsuite/tests/dependent/should_fail/Makefile @@ -0,0 +1,5 @@ +TOP=../../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk + + diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.hs b/testsuite/tests/dependent/should_fail/PromotedClass.hs new file mode 100644 index 0000000000..6c3f415e5d --- /dev/null +++ b/testsuite/tests/dependent/should_fail/PromotedClass.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE TypeInType, GADTs #-} + +module PromotedClass where + +import Data.Proxy + +data X a where + MkX :: Show a => a -> X a + +foo :: Proxy ('MkX 'True) +foo = Proxy diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.stderr b/testsuite/tests/dependent/should_fail/PromotedClass.stderr new file mode 100644 index 0000000000..544124ed07 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/PromotedClass.stderr @@ -0,0 +1,6 @@ + +PromotedClass.hs:10:15: error: + • Illegal constraint in a type: Show a0 + • In the first argument of ‘Proxy’, namely ‘MkX True’ + In the type signature: + foo :: Proxy (MkX True) diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.hs b/testsuite/tests/dependent/should_fail/RAE_T32a.hs new file mode 100644 index 0000000000..08a4ad78a8 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/RAE_T32a.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds, + PolyKinds, TypeFamilies, GADTs, TypeInType #-} + +module RAE_T32a where + +import Data.Kind + +data family Sing (k :: *) :: k -> * + +data TyArr' (a :: *) (b :: *) :: * +type TyArr (a :: *) (b :: *) = TyArr' a b -> * +type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2 +data TyPi' (a :: *) (b :: TyArr a *) :: * +type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> * +type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b +$(return []) + +data MkStar (p :: *) (x :: TyArr' p *) +type instance MkStar p @@ x = * +$(return []) + +data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where + Sigma :: + forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a). + Sing * p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> Sing (r @@@ a) b -> Sigma p r +$(return []) + +data instance Sing Sigma (Sigma p r) x where + SSigma :: + forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a) + (sp :: Sing * p) (sr :: Sing (TyPi p (MkStar p)) r) (sa :: Sing p a) (sb :: Sing (r @@@ a) b). + Sing (Sing (r @@@ a) b) sb -> + Sing (Sigma p r) ('Sigma sp sr sa sb) + +-- I (RAE) believe this last definition is ill-typed. diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr new file mode 100644 index 0000000000..1a54c7d53b --- /dev/null +++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr @@ -0,0 +1,19 @@ + +RAE_T32a.hs:28:1: error: + Too many parameters to Sing: + x is unexpected; + expected only two parameters + In the data instance declaration for ‘Sing’ + +RAE_T32a.hs:28:20: error: + Expecting two more arguments to ‘Sigma’ + Expected a type, but + ‘Sigma’ has kind + ‘forall p -> TyPi p (MkStar p) -> *’ + In the first argument of ‘Sing’, namely ‘Sigma’ + In the data instance declaration for ‘Sing’ + +RAE_T32a.hs:28:27: error: + Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’ + In the second argument of ‘Sing’, namely ‘Sigma p r’ + In the data instance declaration for ‘Sing’ diff --git a/testsuite/tests/dependent/should_fail/SelfDep.hs b/testsuite/tests/dependent/should_fail/SelfDep.hs new file mode 100644 index 0000000000..f54b92752b --- /dev/null +++ b/testsuite/tests/dependent/should_fail/SelfDep.hs @@ -0,0 +1,3 @@ +module SelfDep where + +data T :: T -> * diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr new file mode 100644 index 0000000000..f4014f7277 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr @@ -0,0 +1,5 @@ + +SelfDep.hs:3:11: error: + Type constructor ‘T’ cannot be used here + (it is defined and used in the same recursive group) + In the kind ‘T -> *’ diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs new file mode 100644 index 0000000000..09845ed87e --- /dev/null +++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-} + +module TypeSkolEscape where + +import GHC.Types +import GHC.Exts + +type Bad = forall (v :: Levity) (a :: TYPE v). a diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr new file mode 100644 index 0000000000..1574c017ce --- /dev/null +++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr @@ -0,0 +1,7 @@ + +TypeSkolEscape.hs:8:1: error: + Quantified type's kind mentions quantified type variable + (skolem escape) + type: forall (v1 :: Levity) (a1 :: TYPE v1). a1 + of kind: TYPE v + In the type synonym declaration for ‘Bad’ diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T new file mode 100644 index 0000000000..8d4b288e96 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/all.T @@ -0,0 +1,9 @@ +test('DepFail1', normal, compile_fail, ['']) +test('RAE_T32a', normal, compile_fail, ['']) +test('TypeSkolEscape', normal, compile_fail, ['']) +test('BadTelescope', normal, compile_fail, ['']) +test('BadTelescope2', normal, compile_fail, ['']) +test('BadTelescope3', normal, compile_fail, ['']) +test('PromotedClass', normal, compile_fail, ['']) +test('SelfDep', normal, compile_fail, ['']) +test('BadTelescope4', normal, compile_fail, ['']) |