summaryrefslogtreecommitdiff
path: root/testsuite/tests/dependent/should_fail/RAE_T32a.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/dependent/should_fail/RAE_T32a.hs')
-rw-r--r--testsuite/tests/dependent/should_fail/RAE_T32a.hs28
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)