Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / dependent / should_compile / T14556.hs
1 {-# Language UndecidableInstances, DataKinds, TypeOperators, PolyKinds,
2 TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
3
4 module T14556 where
5
6 import Data.Kind
7 import Data.Proxy
8
9 data Fn a b where
10 IdSym :: Fn Type Type
11
12 type family
13 (@@) (f::Fn k k') (a::k)::k' where
14 IdSym @@ a = a
15
16 data KIND = X | FNARR KIND KIND
17
18 data TY :: KIND -> Type where
19 ID :: TY (FNARR X X)
20 FNAPP :: TY (FNARR k k') -> TY k -> TY k'
21
22 data TyRep (kind::KIND) :: TY kind -> Type where
23 TID :: TyRep (FNARR X X) ID
24 TFnApp :: TyRep (FNARR k k') f
25 -> TyRep k a
26 -> TyRep k' (FNAPP f a)
27
28 type family
29 IK (kind::KIND) :: Type where
30 IK X = Type
31 IK (FNARR k k') = Fn (IK k) (IK k')
32
33 type family
34 IT (ty::TY kind) :: IK kind where
35 IT ID = IdSym
36 IT (FNAPP f x) = IT f @@ IT x
37
38 zero :: TyRep X a -> IT a
39 zero = undefined