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