summaryrefslogtreecommitdiff
path: root/testsuite/tests/printer/Ppr040.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/printer/Ppr040.hs')
-rw-r--r--testsuite/tests/printer/Ppr040.hs43
1 files changed, 43 insertions, 0 deletions
diff --git a/testsuite/tests/printer/Ppr040.hs b/testsuite/tests/printer/Ppr040.hs
new file mode 100644
index 0000000000..a9885a9d53
--- /dev/null
+++ b/testsuite/tests/printer/Ppr040.hs
@@ -0,0 +1,43 @@
+{-# 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 [])
+
+type instance (MkStar p) @@ x = *
+$(return [])
+
+foo :: forall p x . MkStar p @@ x
+foo = undefined
+
+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.