summaryrefslogtreecommitdiff
path: root/tests/examples/ghc86/RAE_T32b.hs
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examples/ghc86/RAE_T32b.hs')
-rw-r--r--tests/examples/ghc86/RAE_T32b.hs23
1 files changed, 23 insertions, 0 deletions
diff --git a/tests/examples/ghc86/RAE_T32b.hs b/tests/examples/ghc86/RAE_T32b.hs
new file mode 100644
index 0000000..bcb7b64
--- /dev/null
+++ b/tests/examples/ghc86/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 :: Type) :: k -> Type
+
+data TyArr (a :: Type) (b :: Type) :: Type
+type family (a :: TyArr k1 k2 -> Type) @@ (b :: k1) :: k2
+$(return [])
+
+data Sigma (p :: Type) (r :: TyArr p Type -> Type) :: Type where
+ Sigma :: forall (p :: Type) (r :: TyArr p Type -> Type) (a :: p) (b :: r @@ a).
+ Sing Type p -> Sing (TyArr p Type -> Type) r -> Sing p a -> Sing (r @@ a) b -> Sigma p r
+$(return [])
+
+data instance Sing (Sigma p r) (x :: Sigma p r) :: Type where
+ SSigma :: forall (p :: Type) (r :: TyArr p Type -> Type) (a :: p) (b :: r @@ a)
+ (sp :: Sing Type p) (sr :: Sing (TyArr p Type -> Type) 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)