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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
{-# LANGUAGE EmptyDataDecls, TypeFamilies, UndecidableInstances,
ScopedTypeVariables, TypeOperators,
FlexibleInstances, NoMonomorphismRestriction,
MultiParamTypeClasses, FlexibleContexts #-}
module IndTypesPerfMerge where
data a :* b = a :* b
infixr 6 :*
data TRUE
data FALSE
data Zero
data Succ a
type family Equals m n
type instance Equals Zero Zero = TRUE
type instance Equals (Succ a) Zero = FALSE
type instance Equals Zero (Succ a) = FALSE
type instance Equals (Succ a) (Succ b) = Equals a b
type family LessThan m n
type instance LessThan Zero Zero = FALSE
type instance LessThan (Succ n) Zero = FALSE
type instance LessThan Zero (Succ n) = TRUE
type instance LessThan (Succ m) (Succ n) = LessThan m n
newtype Tagged n a = Tagged a deriving (Show,Eq)
type family Cond p a b
type instance Cond TRUE a b = a
type instance Cond FALSE a b = b
class Merger a where
type Merged a
type UnmergedLeft a
type UnmergedRight a
mkMerge :: a -> UnmergedLeft a -> UnmergedRight a -> Merged a
class Mergeable a b where
type MergerType a b
merger :: a -> b -> MergerType a b
{-
merge ::
forall a b.
(Merger (MergerType a b), Mergeable a b,
UnmergedLeft (MergerType a b) ~ a,
UnmergedRight (MergerType a b) ~ b) =>
a -> b -> Merged (MergerType a b)
-}
merge x y = mkMerge (merger x y) x y
{- ------------- NASTY TYPE FOR merge -----------------
-- See Trac #11408
x:tx, y:ty
mkMerge @ gamma
merger @ alpha beta
merge :: tx -> ty -> tr
Constraints generated:
gamma ~ MergerType alpha beta
UnmergedLeft gamma ~ tx
UnmergedRight gamma ~ ty
alpha ~ tx
beta ~ ty
tr ~ Merged gamma
Mergeable tx ty
Merger gamma
One solve path:
gamma := t
tx := alpha := UnmergedLeft t
ty := beta := UnmergedRight t
Mergeable (UnmergedLeft t) (UnmergedRight t)
Merger t
t ~ MergerType (UnmergedLeft t) (UnmergedRight t)
LEADS TO AMBIGUOUS TYPE
Another solve path:
tx := alpha
ty := beta
gamma := MergerType alpha beta
UnmergedLeft (MergerType alpha beta) ~ alpha
UnmergedRight (MergerType alpha beta) ~ beta
Merger (MergerType alpha beta)
Mergeable alpha beta
LEADS TO NON-AMBIGUOUS TYPE
--------------- -}
data TakeRight a
data TakeLeft a
data DiscardRightHead a b c d
data LeftHeadFirst a b c d
data RightHeadFirst a b c d
data EndMerge
instance Mergeable () () where
type MergerType () () = EndMerge
merger = undefined
instance Mergeable () (a :* b) where
type MergerType () (a :* b) = TakeRight (a :* b)
merger = undefined
instance Mergeable (a :* b) () where
type MergerType (a :* b) () = TakeLeft (a :* b)
merger = undefined
instance Mergeable (Tagged m a :* t1) (Tagged n b :* t2) where
type MergerType (Tagged m a :* t1) (Tagged n b :* t2) =
Cond (Equals m n) (DiscardRightHead (Tagged m a) t1 (Tagged n b) t2)
(Cond (LessThan m n) (LeftHeadFirst (Tagged m a) t1 (Tagged n b) t2)
(RightHeadFirst (Tagged m a ) t1 (Tagged n b) t2))
merger = undefined
instance Merger EndMerge where
type Merged EndMerge = ()
type UnmergedLeft EndMerge = ()
type UnmergedRight EndMerge = ()
mkMerge _ () () = ()
instance Merger (TakeRight a) where
type Merged (TakeRight a) = a
type UnmergedLeft (TakeRight a) = ()
type UnmergedRight (TakeRight a) = a
mkMerge _ () a = a
instance Merger (TakeLeft a) where
type Merged (TakeLeft a) = a
type UnmergedLeft (TakeLeft a) = a
type UnmergedRight (TakeLeft a) = ()
mkMerge _ a () = a
instance
(Mergeable t1 t2,
Merger (MergerType t1 t2),
t1 ~ UnmergedLeft (MergerType t1 t2),
t2 ~ UnmergedRight (MergerType t1 t2)) =>
Merger (DiscardRightHead h1 t1 h2 t2) where
type Merged (DiscardRightHead h1 t1 h2 t2) = h1 :* Merged (MergerType t1 t2)
type UnmergedLeft (DiscardRightHead h1 t1 h2 t2) = h1 :* t1
type UnmergedRight (DiscardRightHead h1 t1 h2 t2) = h2 :* t2
mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 t2) t1 t2
instance
(Mergeable t1 (h2 :* t2),
Merger (MergerType t1 (h2 :* t2)),
t1 ~ UnmergedLeft (MergerType t1 (h2 :* t2)),
(h2 :* t2) ~ UnmergedRight (MergerType t1 (h2 :* t2))) =>
Merger (LeftHeadFirst h1 t1 h2 t2) where
type Merged (LeftHeadFirst h1 t1 h2 t2) = h1 :* Merged (MergerType t1 (h2 :* t2))
type UnmergedLeft (LeftHeadFirst h1 t1 h2 t2) = h1 :* t1
type UnmergedRight (LeftHeadFirst h1 t1 h2 t2) = h2 :* t2
mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 (h2 :* t2)) t1 (h2 :* t2)
instance
(Mergeable (h1 :* t1) t2,
Merger (MergerType (h1 :* t1) t2),
(h1 :* t1) ~ UnmergedLeft (MergerType (h1 :* t1) t2),
t2 ~ UnmergedRight (MergerType (h1 :* t1) t2)) =>
Merger (RightHeadFirst h1 t1 h2 t2) where
type Merged (RightHeadFirst h1 t1 h2 t2) = h2 :* Merged (MergerType (h1 :* t1) t2)
type UnmergedLeft (RightHeadFirst h1 t1 h2 t2) = h1 :* t1
type UnmergedRight (RightHeadFirst h1 t1 h2 t2) = h2 :* t2
mkMerge _ (h1 :* t1) (h2 :* t2) = h2 :* mkMerge (merger (h1 :* t1) t2) (h1 :* t1) t2
|
