testsuite: Assert that testsuite ways are known
[ghc.git] / testsuite / tests / typecheck / should_compile / T4524.hs
1 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
2 {-# LANGUAGE
3 GADTs,
4 TypeOperators,
5 ScopedTypeVariables,
6 RankNTypes,
7 NoMonoLocalBinds
8 #-}
9 {-# OPTIONS_GHC -O2 -w #-}
10 {-
11 Copyright (C) 2002-2003 David Roundy
12
13 This program is free software; you can redistribute it and/or modify
14 it under the terms of the GNU General Public License as published by
15 the Free Software Foundation; either version 2, or (at your option)
16 any later version.
17
18 This program is distributed in the hope that it will be useful,
19 but WITHOUT ANY WARRANTY; without even the implied warranty of
20 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
21 GNU General Public License for more details.
22
23 You should have received a copy of the GNU General Public License
24 along with this program; see the file COPYING. If not, write to
25 the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
26 Boston, MA 02110-1301, USA.
27 -}
28
29 module T4524 where
30
31 import Data.Maybe ( mapMaybe )
32 import Control.Applicative ( Alternative(..) )
33 import Control.Monad ( MonadPlus(..), msum, ap, liftM )
34 import Unsafe.Coerce (unsafeCoerce)
35
36 newtype FileName = FN FilePath deriving ( Eq, Ord )
37
38 data FL a x z where
39 (:>:) :: a x y -> FL a y z -> FL a x z
40 NilFL :: FL a x x
41 data RL a x z where
42 (:<:) :: a y z -> RL a x y -> RL a x z
43 NilRL :: RL a x x
44 data (a1 :> a2) x y = forall z. (a1 x z) :> (a2 z y)
45 infixr 1 :>
46 data (a1 :< a2) x y = forall z. (a1 z y) :< (a2 x z)
47 infix 1 :<
48 infixr 5 :>:, :<:
49
50 data EqCheck a b where
51 IsEq :: EqCheck a a
52 NotEq :: EqCheck a b
53
54 class MyEq p => Invert p where
55 invert :: p x y -> p y x
56 identity :: p x x
57
58 class MyEq p where
59 unsafeCompare :: p a b -> p c d -> Bool
60 unsafeCompare a b = IsEq == (a =/\= unsafeCoerceP b)
61
62 (=\/=) :: p a b -> p a c -> EqCheck b c
63 a =\/= b | unsafeCompare a b = unsafeCoerceP IsEq
64 | otherwise = NotEq
65
66 (=/\=) :: p a c -> p b c -> EqCheck a b
67 a =/\= b | IsEq == (a =\/= unsafeCoerceP b) = unsafeCoerceP IsEq
68 | otherwise = NotEq
69
70 infix 4 =\/=, =/\=
71
72 class Commute p where
73 commute :: (p :> p) x y -> Maybe ((p :> p) x y)
74
75 instance (MyEq p, Commute p) => MyEq (FL p) where
76 instance (MyEq p, Commute p) => MyEq (RL p) where
77 instance Commute p => Commute (RL p) where
78 instance (Commute p, Invert p) => Invert (RL p) where
79 instance (Invert p, Commute p) => Invert (FL p) where
80 instance Eq (EqCheck a b) where
81 instance MyEq FilePatchType where
82 instance Invert Patch where
83
84 instance MyEq Patch where
85 unsafeCompare = eqPatches
86
87 eqPatches :: Patch x y -> Patch w z -> Bool
88 eqPatches (PP p1) (PP p2) = undefined
89 eqPatches (Merger _ _ p1a p1b) (Merger _ _ p2a p2b)
90 = eqPatches p1a p2a &&
91 eqPatches p1b p2b
92 eqPatches (Regrem _ _ p1a p1b) (Regrem _ _ p2a p2b)
93 = eqPatches p1a p2a &&
94 eqPatches p1b p2b
95 eqPatches _ _ = False
96
97 data Prim x y where
98 FP :: !FileName -> !(FilePatchType x y) -> Prim x y
99
100 data FilePatchType x y = FilePatchType
101 deriving (Eq,Ord)
102
103 data Patch x y where
104 PP :: Prim x y -> Patch x y
105 Merger :: FL Patch x y
106 -> RL Patch x b
107 -> Patch c b
108 -> Patch c d
109 -> Patch x y
110 Regrem :: FL Patch x y
111 -> RL Patch x b
112 -> Patch c b
113 -> Patch c a
114 -> Patch y x
115
116 data Sealed a where
117 Sealed :: a x -> Sealed a
118 data FlippedSeal a y where
119 FlippedSeal :: !(a x y) -> FlippedSeal a y
120
121 mapFlipped :: (forall x. a x y -> b x z) -> FlippedSeal a y -> FlippedSeal b z
122 mapFlipped f (FlippedSeal x) = FlippedSeal (f x)
123
124 headPermutationsRL :: Commute p => RL p x y -> [RL p x y]
125 headPermutationsRL NilRL = []
126 headPermutationsRL (p:<:ps) =
127 (p:<:ps) : mapMaybe (swapfirstRL.(p:<:)) (headPermutationsRL ps)
128 where swapfirstRL (p1:<:p2:<:xs) = do p1':>p2' <- commute (p2:>p1)
129 Just $ p2':<:p1':<:xs
130 swapfirstRL _ = Nothing
131
132 is_filepatch :: Prim x y -> Maybe FileName
133 is_filepatch (FP f _) = Just f
134 is_filepatch _ = Nothing
135
136 toFwdCommute :: (Commute p, Commute q, Monad m)
137 => ((p :< q) x y -> m ((q :< p) x y))
138 -> (q :> p) x y -> m ((p :> q) x y)
139 toFwdCommute c (x :> y) = do x' :< y' <- c (y :< x)
140 return (y' :> x')
141
142 unsafeUnseal :: Sealed a -> a x
143 unsafeUnseal (Sealed a) = unsafeCoerceP1 a
144
145 unsafeUnsealFlipped :: FlippedSeal a y -> a x y
146 unsafeUnsealFlipped (FlippedSeal a) = unsafeCoerceP a
147
148 unsafeCoerceP :: a x y -> a b c
149 unsafeCoerceP = unsafeCoerce
150
151 unsafeCoercePStart :: a x1 y -> a x2 y
152 unsafeCoercePStart = unsafeCoerce
153
154 unsafeCoercePEnd :: a x y1 -> a x y2
155 unsafeCoercePEnd = unsafeCoerce
156
157 unsafeCoerceP1 :: a x -> a y
158 unsafeCoerceP1 = unsafeCoerce
159
160 data Perhaps a = Unknown | Failed | Succeeded a
161
162 instance Functor Perhaps where
163 fmap = liftM
164
165 instance Applicative Perhaps where
166 pure = return
167 (<*>) = ap
168
169 instance Monad Perhaps where
170 (Succeeded x) >>= k = k x
171 Failed >>= _ = Failed
172 Unknown >>= _ = Unknown
173 Failed >> _ = Failed
174 (Succeeded _) >> k = k
175 Unknown >> k = k
176 return = Succeeded
177
178 instance MonadFail Perhaps where
179 fail _ = Unknown
180
181 instance Alternative Perhaps where
182 (<|>) = mplus
183 empty = mzero
184
185 instance MonadPlus Perhaps where
186 mzero = Unknown
187 Unknown `mplus` ys = ys
188 Failed `mplus` _ = Failed
189 (Succeeded x) `mplus` _ = Succeeded x
190
191 toMaybe :: Perhaps a -> Maybe a
192 toMaybe (Succeeded x) = Just x
193 toMaybe _ = Nothing
194
195 cleverCommute :: CommuteFunction -> CommuteFunction
196 cleverCommute c (p1:<p2) =
197 case c (p1 :< p2) of
198 Succeeded x -> Succeeded x
199 Failed -> Failed
200
201 speedyCommute :: CommuteFunction
202 speedyCommute (p1 :< p2) -- Deal with common case quickly!
203 | p1_modifies /= Nothing && p2_modifies /= Nothing &&
204 p1_modifies /= p2_modifies = undefined
205 | otherwise = Unknown
206 where p1_modifies = isFilepatchMerger p1
207 p2_modifies = isFilepatchMerger p2
208
209 everythingElseCommute :: MaybeCommute -> CommuteFunction
210 everythingElseCommute _ x = undefined
211
212 unsafeMerger :: String -> Patch x y -> Patch x z -> Patch a b
213 unsafeMerger x p1 p2 = unsafeCoercePStart $ unsafeUnseal $ merger x p1 p2
214
215 mergerCommute :: (Patch :< Patch) x y -> Perhaps ((Patch :< Patch) x y)
216 mergerCommute (Merger _ _ p1 p2 :< pA)
217 | unsafeCompare pA p1 = Succeeded (unsafeMerger "0.0" p2 p1 :< unsafeCoercePStart p2)
218 | unsafeCompare pA (invert (unsafeMerger "0.0" p2 p1)) = Failed
219 mergerCommute (Merger _ _
220 (Merger _ _ c b)
221 (Merger _ _ c' a) :<
222 Merger _ _ b' c'')
223 | unsafeCompare b' b && unsafeCompare c c' && unsafeCompare c c'' = undefined
224 mergerCommute _ = Unknown
225
226 instance Commute Patch where
227 commute x = toMaybe $ msum
228 [toFwdCommute speedyCommute x,
229 toFwdCommute (cleverCommute mergerCommute) x,
230 toFwdCommute (everythingElseCommute undefined) x
231 ]
232
233 isFilepatchMerger :: Patch x y -> Maybe FileName
234 isFilepatchMerger (PP p) = is_filepatch p
235 isFilepatchMerger (Regrem und unw p1 p2)
236 = isFilepatchMerger (Merger und unw p1 p2)
237
238 type CommuteFunction = forall x y. (Patch :< Patch) x y -> Perhaps ((Patch :< Patch) x y)
239 type MaybeCommute = forall x y. (Patch :< Patch) x y -> Maybe ((Patch :< Patch) x y)
240
241 {- unwind, trueUnwind, reconcleUnwindings, and merger are most likely
242 where the problem lies. Everything above is just brought in to bring
243 in enough context so that those four will compile. -}
244 unwind :: Patch x y -> Sealed (RL Patch x) -- Recreates a patch history in reverse.
245 unwind (Merger _ unwindings _ _) = Sealed unwindings
246 unwind p = Sealed (p :<: NilRL)
247
248 trueUnwind :: Patch x y -> Sealed (RL Patch x) -- Recreates a patch history in reverse.
249 trueUnwind p@(Merger _ _ p1 p2) =
250 case (unwind p1, unwind p2) of
251 (Sealed (_:<:p1s),Sealed (_:<:p2s)) ->
252 Sealed (p :<: unsafeCoerceP p1 :<: unsafeUnsealFlipped (reconcileUnwindings p1s (unsafeCoercePEnd p2s)))
253
254 reconcileUnwindings :: RL Patch x z -> RL Patch y z -> FlippedSeal (RL Patch) z
255 reconcileUnwindings p1s NilRL = FlippedSeal p1s
256 reconcileUnwindings (p1:<:_) (p2:<:_) =
257 case [undefined | p1s'@(_:<:_) <- headPermutationsRL (p1:<:undefined)] of
258 ((_:<:p1s', _:<:p2s'):_) ->
259 mapFlipped (undefined :<:) $ reconcileUnwindings p1s' (unsafeCoercePEnd p2s')
260
261 merger :: String -> Patch x y -> Patch x z -> Sealed (Patch y)
262 merger "0.0" p1 p2 = Sealed $ Merger undoit unwindings p1 p2
263 where fake_p = Merger identity NilRL p1 p2
264 unwindings = unsafeUnseal (trueUnwind fake_p)
265 p = undefined
266 undoit = undefined