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