blob: 6049b1934ed847b7b0d75b95a934052af569e8f7 (
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
|
{-# Language UndecidableInstances, DataKinds, TypeOperators, TypeFamilies,
PolyKinds, GADTs, LambdaCase, ScopedTypeVariables #-}
module T14554 where
import Data.Kind
import Data.Proxy
type a ~> b = (a, b) -> Type
data IdSym0 :: (Type,Type) -> Type
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') = IK k ~> IK k'
type family IT (ty::TY kind) :: IK kind
zero :: TyRep X a -> IT a
zero x = case x of
TFnApp TID a -> undefined
|
