Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / dependent / should_compile / RAE_T32b.hs
1 {-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, DataKinds, PolyKinds,
2 RankNTypes, TypeOperators #-}
3
4 module RAE_T32b where
5
6 import Data.Kind
7
8 data family Sing (k :: Type) :: k -> Type
9
10 data TyArr (a :: Type) (b :: Type) :: Type
11 type family (a :: TyArr k1 k2 -> Type) @@ (b :: k1) :: k2
12 $(return [])
13
14 data Sigma (p :: Type) (r :: TyArr p Type -> Type) :: Type where
15 Sigma :: forall (p :: Type) (r :: TyArr p Type -> Type)
16 (a :: p) (b :: r @@ a).
17 Sing Type p -> Sing (TyArr p Type -> Type) r -> Sing p a ->
18 Sing (r @@ a) b -> Sigma p r
19 $(return [])
20
21 data instance Sing (Sigma p r) (x :: Sigma p r) :: Type where
22 SSigma :: forall (p :: Type) (r :: TyArr p Type -> Type)
23 (a :: p) (b :: r @@ a)
24 (sp :: Sing Type p) (sr :: Sing (TyArr p Type -> Type) r)
25 (sa :: Sing p a) (sb :: Sing (r @@ a) b).
26 Sing (Sing (r @@ a) b) sb ->
27 Sing (Sigma p r) ('Sigma sp sr sa sb)