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