79bcce66ff1011c2e312723941d11ef531aaa018
[ghc.git] / testsuite / tests / dependent / should_compile / T14749.hs
1 {-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
2
3 module T14749 where
4
5 import Data.Kind
6
7 data KIND = STAR | KIND :> KIND
8
9 data Ty :: KIND -> Type where
10 TMaybe :: Ty (STAR :> STAR)
11 TApp :: Ty (a :> b) -> (Ty a -> Ty b)
12
13 type family IK (k :: KIND) = (res :: Type) where
14 IK STAR = Type
15 IK (a:>b) = IK a -> IK b
16
17 type family I (t :: Ty k) = (res :: IK k) where
18 I TMaybe = Maybe
19 I (TApp f a) = (I f) (I a)
20
21 data TyRep (k :: KIND) (t :: Ty k) where
22 TyMaybe :: TyRep (STAR:>STAR) TMaybe
23 TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
24
25 zero :: TyRep STAR a -> I a
26 zero x = case x of
27 TyApp TyMaybe _ -> Nothing