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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
{-# LANGUAGE PolyKinds, GADTs, TypeApplications, TypeInType, DataKinds,
RankNTypes, ConstraintKinds, TypeFamilies #-}
module T12045a where
import Data.Kind
import Data.Typeable
data T (f :: k -> Type) a = MkT (f a)
newtype TType f a= MkTType (T @Type f a)
t1 :: TType Maybe Bool
t1 = MkTType (MkT (Just True))
t2 :: TType Maybe a
t2 = MkTType (MkT Nothing)
data Nat = O | S Nat
data T1 :: forall k1 k2. k1 -> k2 -> Type where
MkT1 :: T1 a b
x :: T1 @_ @Nat False n
x = MkT1
-- test from trac 12045
type Cat k = k -> k -> Type
data FreeCat :: Cat k -> Cat k where
Nil :: FreeCat f a a
Cons :: f a b -> FreeCat f b c -> FreeCat f a c
liftCat :: f a b -> FreeCat f a b
liftCat x = Cons x Nil
data Node = Unit | N
data NatGraph :: Cat Node where
One :: NatGraph Unit N
Succ :: NatGraph N N
one :: (FreeCat @Node NatGraph) Unit N
one = liftCat One
type Typeable1 = Typeable @(Type -> Type)
type Typeable2 = Typeable @(Type -> Type -> Type)
type Typeable3 = Typeable @(Cat Bool)
type family F a where
F Type = Type -> Type
F (Type -> Type) = Type
F other = other
data T2 :: F k -> Type
foo :: T2 @Type Maybe -> T2 @(Type -> Type) Int -> Type
foo a b = undefined
data family D (a :: k)
data instance D @Type a = DBool
data instance D @(Type -> Type) b = DChar
class C a where
tc :: (D a) -> Int
instance C Int where
tc DBool = 5
instance C Bool where
tc DBool = 6
instance C Maybe where
tc DChar = 7
-- Tests from D5229
data P a = MkP
type MkPTrue = MkP @Bool
type BoolEmpty = '[] @Bool
type family F1 (a :: k) :: Type
type G2 (a :: Bool) = F1 @Bool a
|
