Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / indexed-types / should_compile / T14162.hs
1 {-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds,
2 TypeFamilies, GADTs #-}
3
4 module T14162 where
5
6 import Data.Kind
7
8 data SubList (a :: Maybe w) :: Type where
9 SubNil :: SubList 'Nothing
10
11 data family Sing (a :: k)
12
13 data instance Sing (x :: SubList ys) where
14 SSubNil :: Sing SubNil
15
16 {-
17 SubList :: forall (w::*). Maybe w -> *
18 SubNil :: forall (w::*). SubList w (Nothing w)
19
20 wrkSubNil :: forall (w::*) (a :: Maybe w).
21 (a ~ Nothing w) =>
22 SubList w a
23
24 Sing :: forall k. k -> *
25
26 RepTc :: forall (w_aSy : *)
27 (ys_aRW :: Maybe w_aSy)
28 (x_aRX :: SubList w_aSy ys_aRW).
29 *
30
31 axiom forall (w : *) (ys : Maybe w) (x : SubList ys).
32 Sing (SubList ys) (x : SubList ys) ~ RepTc w ys x
33
34 data RepTc w ys x where
35 SSubNil :: RepTc w (Nothing w) (SubNil w)
36
37 SSubNil :: forall (w :: *). Sing (SubList w (Nothing w)) (SubNil w)
38
39 wrkSSubMil :: forall (w : *) (ys : Maybe w) (x : Sublist w ys).
40 () =>
41 RepTc w ys x
42 -}