blob: b6b1f48a853bf0f67c26e0aed12f4233e4e28007 (
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
40
41
|
{-# Language UndecidableInstances, DataKinds, TypeOperators, PolyKinds,
TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables,
StandaloneKindSignatures #-}
module T14556 where
import Data.Kind
import Data.Proxy
data Fn a b where
IdSym :: Fn Type Type
type (@@) :: Fn k k' -> k -> k'
type family f @@ a 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'
type TyRep :: forall (kind::KIND) -> TY kind -> Type
data TyRep k t where
TID :: TyRep (FNARR X X) ID
TFnApp :: TyRep (FNARR k k') f
-> TyRep k a
-> TyRep k' (FNAPP f a)
type IK :: KIND -> Type
type family IK kind where
IK X = Type
IK (FNARR k k') = Fn (IK k) (IK k')
type IT :: TY kind -> IK kind
type family IT ty where
IT ID = IdSym
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a -> IT a
zero = undefined
|
