Update Trac ticket URLs to point to GitLab
[ghc.git] / testsuite / tests / indexed-types / should_compile / IndTypesPerfMerge.hs
1 {-# LANGUAGE EmptyDataDecls, TypeFamilies, UndecidableInstances,
2 ScopedTypeVariables, TypeOperators,
3 FlexibleInstances, NoMonomorphismRestriction,
4 MultiParamTypeClasses, FlexibleContexts #-}
5 module IndTypesPerfMerge where
6
7 data a :* b = a :* b
8 infixr 6 :*
9
10 data TRUE
11 data FALSE
12 data Zero
13 data Succ a
14
15 type family Equals m n
16 type instance Equals Zero Zero = TRUE
17 type instance Equals (Succ a) Zero = FALSE
18 type instance Equals Zero (Succ a) = FALSE
19 type instance Equals (Succ a) (Succ b) = Equals a b
20
21 type family LessThan m n
22 type instance LessThan Zero Zero = FALSE
23 type instance LessThan (Succ n) Zero = FALSE
24 type instance LessThan Zero (Succ n) = TRUE
25 type instance LessThan (Succ m) (Succ n) = LessThan m n
26
27 newtype Tagged n a = Tagged a deriving (Show,Eq)
28
29 type family Cond p a b
30
31 type instance Cond TRUE a b = a
32 type instance Cond FALSE a b = b
33
34 class Merger a where
35 type Merged a
36 type UnmergedLeft a
37 type UnmergedRight a
38 mkMerge :: a -> UnmergedLeft a -> UnmergedRight a -> Merged a
39
40 class Mergeable a b where
41 type MergerType a b
42 merger :: a -> b -> MergerType a b
43
44 {-
45 merge ::
46 forall a b.
47 (Merger (MergerType a b), Mergeable a b,
48 UnmergedLeft (MergerType a b) ~ a,
49 UnmergedRight (MergerType a b) ~ b) =>
50 a -> b -> Merged (MergerType a b)
51 -}
52 merge x y = mkMerge (merger x y) x y
53
54
55 {- ------------- NASTY TYPE FOR merge -----------------
56 -- See #11408
57
58 x:tx, y:ty
59 mkMerge @ gamma
60 merger @ alpha beta
61 merge :: tx -> ty -> tr
62
63 Constraints generated:
64 gamma ~ MergerType alpha beta
65 UnmergedLeft gamma ~ tx
66 UnmergedRight gamma ~ ty
67 alpha ~ tx
68 beta ~ ty
69 tr ~ Merged gamma
70 Mergeable tx ty
71 Merger gamma
72
73 One solve path:
74 gamma := t
75 tx := alpha := UnmergedLeft t
76 ty := beta := UnmergedRight t
77
78 Mergeable (UnmergedLeft t) (UnmergedRight t)
79 Merger t
80 t ~ MergerType (UnmergedLeft t) (UnmergedRight t)
81
82 LEADS TO AMBIGUOUS TYPE
83
84 Another solve path:
85 tx := alpha
86 ty := beta
87 gamma := MergerType alpha beta
88
89 UnmergedLeft (MergerType alpha beta) ~ alpha
90 UnmergedRight (MergerType alpha beta) ~ beta
91 Merger (MergerType alpha beta)
92 Mergeable alpha beta
93
94 LEADS TO NON-AMBIGUOUS TYPE
95 --------------- -}
96
97
98 data TakeRight a
99 data TakeLeft a
100 data DiscardRightHead a b c d
101 data LeftHeadFirst a b c d
102 data RightHeadFirst a b c d
103 data EndMerge
104
105 instance Mergeable () () where
106 type MergerType () () = EndMerge
107 merger = undefined
108
109 instance Mergeable () (a :* b) where
110 type MergerType () (a :* b) = TakeRight (a :* b)
111 merger = undefined
112 instance Mergeable (a :* b) () where
113 type MergerType (a :* b) () = TakeLeft (a :* b)
114 merger = undefined
115
116 instance Mergeable (Tagged m a :* t1) (Tagged n b :* t2) where
117 type MergerType (Tagged m a :* t1) (Tagged n b :* t2) =
118 Cond (Equals m n) (DiscardRightHead (Tagged m a) t1 (Tagged n b) t2)
119 (Cond (LessThan m n) (LeftHeadFirst (Tagged m a) t1 (Tagged n b) t2)
120 (RightHeadFirst (Tagged m a ) t1 (Tagged n b) t2))
121 merger = undefined
122
123 instance Merger EndMerge where
124 type Merged EndMerge = ()
125 type UnmergedLeft EndMerge = ()
126 type UnmergedRight EndMerge = ()
127 mkMerge _ () () = ()
128
129 instance Merger (TakeRight a) where
130 type Merged (TakeRight a) = a
131 type UnmergedLeft (TakeRight a) = ()
132 type UnmergedRight (TakeRight a) = a
133 mkMerge _ () a = a
134
135 instance Merger (TakeLeft a) where
136 type Merged (TakeLeft a) = a
137 type UnmergedLeft (TakeLeft a) = a
138 type UnmergedRight (TakeLeft a) = ()
139 mkMerge _ a () = a
140
141 instance
142 (Mergeable t1 t2,
143 Merger (MergerType t1 t2),
144 t1 ~ UnmergedLeft (MergerType t1 t2),
145 t2 ~ UnmergedRight (MergerType t1 t2)) =>
146 Merger (DiscardRightHead h1 t1 h2 t2) where
147 type Merged (DiscardRightHead h1 t1 h2 t2) = h1 :* Merged (MergerType t1 t2)
148 type UnmergedLeft (DiscardRightHead h1 t1 h2 t2) = h1 :* t1
149 type UnmergedRight (DiscardRightHead h1 t1 h2 t2) = h2 :* t2
150 mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 t2) t1 t2
151
152 instance
153 (Mergeable t1 (h2 :* t2),
154 Merger (MergerType t1 (h2 :* t2)),
155 t1 ~ UnmergedLeft (MergerType t1 (h2 :* t2)),
156 (h2 :* t2) ~ UnmergedRight (MergerType t1 (h2 :* t2))) =>
157 Merger (LeftHeadFirst h1 t1 h2 t2) where
158 type Merged (LeftHeadFirst h1 t1 h2 t2) = h1 :* Merged (MergerType t1 (h2 :* t2))
159 type UnmergedLeft (LeftHeadFirst h1 t1 h2 t2) = h1 :* t1
160 type UnmergedRight (LeftHeadFirst h1 t1 h2 t2) = h2 :* t2
161 mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 (h2 :* t2)) t1 (h2 :* t2)
162
163 instance
164 (Mergeable (h1 :* t1) t2,
165 Merger (MergerType (h1 :* t1) t2),
166 (h1 :* t1) ~ UnmergedLeft (MergerType (h1 :* t1) t2),
167 t2 ~ UnmergedRight (MergerType (h1 :* t1) t2)) =>
168 Merger (RightHeadFirst h1 t1 h2 t2) where
169 type Merged (RightHeadFirst h1 t1 h2 t2) = h2 :* Merged (MergerType (h1 :* t1) t2)
170 type UnmergedLeft (RightHeadFirst h1 t1 h2 t2) = h1 :* t1
171 type UnmergedRight (RightHeadFirst h1 t1 h2 t2) = h2 :* t2
172 mkMerge _ (h1 :* t1) (h2 :* t2) = h2 :* mkMerge (merger (h1 :* t1) t2) (h1 :* t1) t2