diff options
Diffstat (limited to 'testsuite/tests/dependent')
33 files changed, 480 insertions, 0 deletions
diff --git a/testsuite/tests/dependent/Makefile b/testsuite/tests/dependent/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/dependent/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/dependent/should_compile/Dep1.hs b/testsuite/tests/dependent/should_compile/Dep1.hs new file mode 100644 index 0000000000..6f8fe0720d --- /dev/null +++ b/testsuite/tests/dependent/should_compile/Dep1.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE TypeInType #-} + +module Dep1 where + +import Data.Kind + +data Proxy k (a :: k) = P + +x :: Proxy * Int +x = P + +y :: Proxy Bool True +y = P diff --git a/testsuite/tests/dependent/should_compile/Dep2.hs b/testsuite/tests/dependent/should_compile/Dep2.hs new file mode 100644 index 0000000000..34be3cffc6 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/Dep2.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE PolyKinds, GADTs #-} + +module Dep2 where + +data G (a :: k) where + G1 :: G Int + G2 :: G Maybe diff --git a/testsuite/tests/dependent/should_compile/Dep3.hs b/testsuite/tests/dependent/should_compile/Dep3.hs new file mode 100644 index 0000000000..cba5043a08 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/Dep3.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE TypeFamilies, TypeInType, GADTs #-} + +module Dep3 where + +import Data.Kind +import GHC.Exts ( Constraint ) + +type Star1 = * + +data Id1 (a :: Star1) where + Id1 :: a -> Id1 a + +data Id1' :: Star1 -> * where + Id1' :: a -> Id1' a + +type family Star2 x where + Star2 x = * + +data Id2a (a :: Star2 Constraint) = Id2a a + + +data Id2 (a :: Star2 Constraint) where + Id2 :: a -> Id2 a + +data Id2' :: Star2 Constraint -> * where + Id2' :: a -> Id2' a diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.hs b/testsuite/tests/dependent/should_compile/KindEqualities.hs new file mode 100644 index 0000000000..1f2e82c302 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/KindEqualities.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE PolyKinds, GADTs, ExplicitForAll #-} +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +module KindEqualities where + +data TyRep1 :: * -> * where + TyInt1 :: TyRep1 Int + TyBool1 :: TyRep1 Bool + +zero1 :: forall a. TyRep1 a -> a +zero1 TyInt1 = 0 +zero1 TyBool1 = False + +data Proxy (a :: k) = P + +data TyRep :: k -> * where + TyInt :: TyRep Int + TyBool :: TyRep Bool + TyMaybe :: TyRep Maybe + TyApp :: TyRep a -> TyRep b -> TyRep (a b) + +zero :: forall (a :: *). TyRep a -> a +zero TyInt = 0 +zero TyBool = False +zero (TyApp TyMaybe _) = Nothing diff --git a/testsuite/tests/dependent/should_compile/KindEqualities2.hs b/testsuite/tests/dependent/should_compile/KindEqualities2.hs new file mode 100644 index 0000000000..5a6f60d40b --- /dev/null +++ b/testsuite/tests/dependent/should_compile/KindEqualities2.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll, + TemplateHaskell, UndecidableInstances, ScopedTypeVariables, + TypeInType #-} + +module KindEqualities2 where + +import Data.Kind +import GHC.Exts ( Any ) + +data Kind = Star | Arr Kind Kind + +data Ty :: Kind -> * where + TInt :: Ty Star + TBool :: Ty Star + TMaybe :: Ty (Arr Star Star) + TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2 + + +data TyRep (k :: Kind) (t :: Ty k) where + TyInt :: TyRep Star TInt + TyBool :: TyRep Star TBool + TyMaybe :: TyRep (Arr Star Star) TMaybe + TyApp :: TyRep (Arr k1 k2) a -> TyRep k1 b -> TyRep k2 (TApp a b) + +type family IK (k :: Kind) +type instance IK Star = * +type instance IK (Arr k1 k2) = IK k1 -> IK k2 + +$(return []) -- necessary because the following instances depend on the + -- previous ones. + +type family I (t :: Ty k) :: IK k +type instance I TInt = Int +type instance I TBool = Bool +type instance I TMaybe = Maybe +type instance I (TApp a b) = (I a) (I b) + +zero :: forall (a :: Ty 'Star). TyRep Star a -> I a +zero TyInt = 0 +zero TyBool = False +zero (TyApp TyMaybe TyInt) = Nothing + +main = print $ zero (TyApp TyMaybe TyInt) diff --git a/testsuite/tests/dependent/should_compile/KindLevels.hs b/testsuite/tests/dependent/should_compile/KindLevels.hs new file mode 100644 index 0000000000..80762978b2 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/KindLevels.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE DataKinds, PolyKinds #-} + +module KindLevels where + +data A +data B :: A -> * +data C :: B a -> * +data D :: C b -> * +data E :: D c -> * diff --git a/testsuite/tests/dependent/should_compile/Makefile b/testsuite/tests/dependent/should_compile/Makefile new file mode 100644 index 0000000000..9101fbd40a --- /dev/null +++ b/testsuite/tests/dependent/should_compile/Makefile @@ -0,0 +1,3 @@ +TOP=../../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/dependent/should_compile/RAE_T32b.hs b/testsuite/tests/dependent/should_compile/RAE_T32b.hs new file mode 100644 index 0000000000..7e067099c9 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/RAE_T32b.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, DataKinds, PolyKinds, + RankNTypes, TypeOperators, TypeInType #-} + +module RAE_T32b where + +import Data.Kind + +data family Sing (k :: *) :: k -> * + +data TyArr (a :: *) (b :: *) :: * +type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2 +$(return []) + +data Sigma (p :: *) (r :: TyArr p * -> *) :: * where + Sigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a). + Sing * p -> Sing (TyArr p * -> *) r -> Sing p a -> Sing (r @@ a) b -> Sigma p r +$(return []) + +data instance Sing (Sigma p r) (x :: Sigma p r) :: * where + SSigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a) + (sp :: Sing * p) (sr :: Sing (TyArr 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) diff --git a/testsuite/tests/dependent/should_compile/Rae31.hs b/testsuite/tests/dependent/should_compile/Rae31.hs new file mode 100644 index 0000000000..cedc019cf3 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/Rae31.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE TemplateHaskell, TypeOperators, PolyKinds, DataKinds, + TypeFamilies, TypeInType #-} + +module A where + +import Data.Kind + +data family Sing (k :: *) :: k -> * +type Sing' (x :: k) = Sing k x +data TyFun' (a :: *) (b :: *) :: * +type TyFun (a :: *) (b :: *) = TyFun' a b -> * +type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2 +data TyPi' (a :: *) (b :: TyFun a *) :: * +type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> * +type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b +$(return []) + +data A (a :: *) (b :: a) (c :: TyFun' a *) -- A :: forall a -> a -> a ~> * +type instance (@@) (A a b) c = * +$(return []) +data B (a :: *) (b :: TyFun' a *) -- B :: forall a -> a ~> * +type instance (@@) (B a) b = TyPi a (A a b) +$(return []) +data C (a :: *) (b :: TyPi a (B a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ c @@@ d) *) diff --git a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs new file mode 100644 index 0000000000..e99c7b5dd5 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies, + TypeInType #-} +{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-} + +module RaeBlogPost where + +import Data.Kind + +-- a Proxy type with an explicit kind +data Proxy k (a :: k) = P +prox :: Proxy * Bool +prox = P + +prox2 :: Proxy Bool 'True +prox2 = P + +-- implicit kinds still work +data A +data B :: A -> * +data C :: B a -> * +data D :: C b -> * +data E :: D c -> * +-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> * + +-- a kind-indexed GADT +data TypeRep (a :: k) where + TInt :: TypeRep Int + TMaybe :: TypeRep Maybe + TApp :: TypeRep a -> TypeRep b -> TypeRep (a b) + +zero :: TypeRep a -> a +zero TInt = 0 +zero (TApp TMaybe _) = Nothing + +data Nat = Zero | Succ Nat +type family a + b where + 'Zero + b = b + ('Succ a) + b = 'Succ (a + b) + +data Vec :: * -> Nat -> * where + Nil :: Vec a 'Zero + (:>) :: a -> Vec a n -> Vec a ('Succ n) +infixr 5 :> + +-- promoted GADT, and using + as a "kind family": +type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where + 'Nil ++ y = y + (h ':> t) ++ y = h ':> (t ++ y) + +-- datatype that mentions * +data U = Star (*) + | Bool Bool + +-- kind synonym +type Monadish = * -> * +class MonadTrans (t :: Monadish -> Monadish) where + lift :: Monad m => m a -> t m a +data Free :: Monadish where + Return :: a -> Free a + Bind :: Free a -> (a -> Free b) -> Free b + +-- yes, * really does have type *. +type Star = (* :: (* :: (* :: *))) diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T new file mode 100644 index 0000000000..0f231db699 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/all.T @@ -0,0 +1,10 @@ +test('Dep1', only_ways('normal'), compile, ['']) +test('Dep2', only_ways('normal'), compile, ['']) +test('Dep3', only_ways('normal'), compile, ['']) +test('KindEqualities', only_ways('normal'), compile, ['']) +test('KindEqualities2', only_ways('normal'), compile, ['']) +test('Rae31', only_ways('normal'), compile, ['']) +test('RAE_T32b', only_ways('normal'), compile, ['']) +test('KindLevels', normal, compile, ['']) +test('RaeBlogPost', normal, compile, ['']) +test('mkGADTVars', normal, compile, ['']) diff --git a/testsuite/tests/dependent/should_compile/mkGADTVars.hs b/testsuite/tests/dependent/should_compile/mkGADTVars.hs new file mode 100644 index 0000000000..1e74c6980a --- /dev/null +++ b/testsuite/tests/dependent/should_compile/mkGADTVars.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE GADTs, TypeInType #-} + +module GADTVars where + +import Data.Kind +import Data.Proxy + +data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where + MkT :: T x1 * (Proxy (y :: x1), z) z 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, ['']) |