diff options
Diffstat (limited to 'testsuite/tests/dependent/should_fail/RAE_T32a.hs')
-rw-r--r-- | testsuite/tests/dependent/should_fail/RAE_T32a.hs | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.hs b/testsuite/tests/dependent/should_fail/RAE_T32a.hs index 08a4ad78a8..d71b863f02 100644 --- a/testsuite/tests/dependent/should_fail/RAE_T32a.hs +++ b/testsuite/tests/dependent/should_fail/RAE_T32a.hs @@ -1,34 +1,36 @@ {-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds, - PolyKinds, TypeFamilies, GADTs, TypeInType #-} + PolyKinds, TypeFamilies, GADTs #-} module RAE_T32a where import Data.Kind -data family Sing (k :: *) :: k -> * +data family Sing (k :: Type) :: k -> Type -data TyArr' (a :: *) (b :: *) :: * -type TyArr (a :: *) (b :: *) = TyArr' a b -> * +data TyArr' (a :: Type) (b :: Type) :: Type +type TyArr (a :: Type) (b :: Type) = TyArr' a b -> Type type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2 -data TyPi' (a :: *) (b :: TyArr a *) :: * -type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> * +data TyPi' (a :: Type) (b :: TyArr a Type) :: Type +type TyPi (a :: Type) (b :: TyArr a Type) = TyPi' a b -> Type type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b $(return []) -data MkStar (p :: *) (x :: TyArr' p *) -type instance MkStar p @@ x = * +data MkStar (p :: Type) (x :: TyArr' p Type) +type instance MkStar p @@ x = Type $(return []) -data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where +data Sigma (p :: Type) (r :: TyPi p (MkStar p)) :: Type 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 + forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a). + Sing Type 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). + forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a) + (sp :: Sing Type 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) |