2 % (c) The University of Glasgow 2006
\r
6 {-# OPTIONS_GHC -w #-}
\r
11 #include "HsVersions.h"
\r
13 import Unify ( tcMatchTy )
\r
25 %************************************************************************
\r
27 Optimising coercions
\r
29 %************************************************************************
\r
32 optCoercion :: TvSubst -> Coercion -> NormalCo
\r
33 -- ^ optCoercion applies a substitution to a coercion,
\r
34 -- *and* optimises it to reduce its size
\r
35 optCoercion env co = opt_co env False co
\r
37 type NormalCo = Coercion
\r
39 -- * The substitution has been fully applied
\r
40 -- * For trans coercions (co1 `trans` co2)
\r
41 -- co1 is not a trans, and neither co1 nor co2 is identity
\r
42 -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
\r
44 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
\r
46 opt_co, opt_co' :: TvSubst
\r
47 -> Bool -- True <=> return (sym co)
\r
51 -- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
\r
53 -- pprTrace "opt_co done }" (ppr co1)
\r
54 -- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1)
\r
55 -- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
\r
58 -- co1 = opt_co' sym co
\r
59 -- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
\r
60 -- (s,t) = coercionKind co
\r
61 -- (s1,t1) | sym = (t,s)
\r
62 -- | otherwise = (s,t)
\r
63 -- (s2,t2) = coercionKind co1
\r
65 opt_co' env sym (AppTy ty1 ty2) = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)
\r
66 opt_co' env sym (FunTy ty1 ty2) = FunTy (opt_co env sym ty1) (opt_co env sym ty2)
\r
67 opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))
\r
68 opt_co' env sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co env sym ty))
\r
69 opt_co' _ _ co@(PredTy (EqPred {})) = pprPanic "optCoercion" (ppr co)
\r
71 opt_co' env sym co@(TyVarTy tv)
\r
72 | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty
\r
73 | not (isCoVar tv) = co -- Identity; does not mention a CoVar
\r
74 | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..
\r
76 | otherwise = mkSymCoercion co
\r
78 (ty1,ty2) = coVarKind tv
\r
80 opt_co' env sym (ForAllTy tv cor)
\r
81 | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)
\r
82 | otherwise = case substTyVarBndr env tv of
\r
83 (env', tv') -> ForAllTy tv' (opt_co env' sym cor)
\r
85 (co1,co2) = coVarKind tv
\r
87 opt_co' env sym (TyConApp tc cos)
\r
88 | Just (arity, desc) <- isCoercionTyCon_maybe tc
\r
89 = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))
\r
90 (map (opt_co env sym) (drop arity cos))
\r
92 = TyConApp tc (map (opt_co env sym) cos)
\r
95 opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo
\r
96 -- Used for CoercionTyCons only
\r
97 -- Arguments are *not* already simplified/substituted
\r
98 opt_co_tc_app env sym tc desc cos
\r
100 CoAxiom {} -- Do *not* push sym inside top-level axioms
\r
101 -- e.g. if g is a top-level axiom
\r
103 -- Then (sym (g ty)) /= g (sym ty) !!
\r
104 | sym -> mkSymCoercion the_co
\r
105 | otherwise -> the_co
\r
107 the_co = TyConApp tc (map (opt_co env False) cos)
\r
108 -- Note that the_co does *not* have sym pushed into it
\r
111 | sym -> opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g
\r
112 | otherwise -> opt_trans opt_co1 opt_co2
\r
115 | sym -> mkUnsafeCoercion ty2' ty1'
\r
116 | otherwise -> mkUnsafeCoercion ty1' ty2'
\r
118 CoSym -> opt_co env (not sym) co1
\r
119 CoLeft -> opt_lr fst
\r
120 CoRight -> opt_lr snd
\r
121 CoCsel1 -> opt_csel fstOf3
\r
122 CoCsel2 -> opt_csel sndOf3
\r
123 CoCselR -> opt_csel thirdOf3
\r
125 CoInst -- See if the first arg is already a forall
\r
126 -- ...then we can just extend the current substitution
\r
127 | Just (tv, co1_body) <- splitForAllTy_maybe co1
\r
128 -> opt_co (extendTvSubst env tv ty2') sym co1_body
\r
130 -- See if is *now* a forall
\r
131 | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1
\r
132 -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution
\r
135 -> TyConApp tc [opt_co1, ty2']
\r
141 ty1' = substTy env co1
\r
142 ty2' = substTy env co2
\r
144 -- These opt_cos have the sym pushed into them
\r
145 opt_co1 = opt_co env sym co1
\r
146 opt_co2 = opt_co env sym co2
\r
148 the_unary_opt_co = TyConApp tc [opt_co1]
\r
150 opt_lr sel = case splitAppTy_maybe opt_co1 of
\r
151 Nothing -> the_unary_opt_co
\r
153 opt_csel sel = case splitCoPredTy_maybe opt_co1 of
\r
154 Nothing -> the_unary_opt_co
\r
158 opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]
\r
159 opt_transL = zipWith opt_trans
\r
161 opt_trans :: NormalCo -> NormalCo -> NormalCo
\r
163 | isIdNormCo co1 = co2
\r
164 | otherwise = opt_trans1 co1 co2
\r
166 opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
\r
167 -- First arg is not the identity
\r
169 | isIdNormCo co2 = co1
\r
170 | otherwise = opt_trans2 co1 co2
\r
172 opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
\r
173 -- Neither arg is the identity
\r
174 opt_trans2 (TyConApp tc [co1a,co1b]) co2
\r
175 | tc `hasKey` transCoercionTyConKey
\r
176 = opt_trans1 co1a (opt_trans2 co1b co2)
\r
178 opt_trans2 co1 co2
\r
179 | Just co <- opt_trans_rule co1 co2
\r
182 opt_trans2 co1 (TyConApp tc [co2a,co2b])
\r
183 | tc `hasKey` transCoercionTyConKey
\r
184 , Just co1_2a <- opt_trans_rule co1 co2a
\r
185 = if isIdNormCo co1_2a
\r
187 else opt_trans2 co1_2a co2b
\r
190 = mkTransCoercion co1 co2
\r
193 opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
\r
194 opt_trans_rule (TyConApp tc1 args1) (TyConApp tc2 args2)
\r
196 = case isCoercionTyCon_maybe tc1 of
\r
198 -> Just (TyConApp tc1 (opt_transL args1 args2))
\r
199 Just (arity, desc)
\r
200 | arity == length args1
\r
201 -> opt_trans_rule_equal_tc desc args1 args2
\r
203 -> case opt_trans_rule_equal_tc desc
\r
204 (take arity args1)
\r
205 (take arity args2) of
\r
206 Just co -> Just $ mkAppTys co $
\r
207 opt_transL (drop arity args1) (drop arity args2)
\r
208 Nothing -> Nothing
\r
210 -- Push transitivity inside apply
\r
211 opt_trans_rule co1 co2
\r
212 | Just (co1a, co1b) <- splitAppTy_maybe co1
\r
213 , Just (co2a, co2b) <- etaApp_maybe co2
\r
214 = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
\r
216 | Just (co2a, co2b) <- splitAppTy_maybe co2
\r
217 , Just (co1a, co1b) <- etaApp_maybe co1
\r
218 = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
\r
220 -- Push transitivity inside (s~t)=>r
\r
221 opt_trans_rule co1 co2
\r
222 | Just (s1,t1,r1) <- splitCoPredTy_maybe co1
\r
223 , Just (s2,t2,r2) <- etaCoPred_maybe co2
\r
224 = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))
\r
226 | Just (s2,t2,r2) <- splitCoPredTy_maybe co2
\r
227 , Just (s1,t1,r1) <- etaCoPred_maybe co1
\r
228 = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))
\r
230 -- Push transitivity inside forall
\r
231 opt_trans_rule co1 co2
\r
232 | Just (tv1,r1) <- splitTypeForAll_maybe co1
\r
233 , Just (tv2,r2) <- etaForAll_maybe co2
\r
234 , let r2' = substTyWith [tv2] [TyVarTy tv1] r2
\r
235 = Just (ForAllTy tv1 (opt_trans2 r1 r2'))
\r
237 | Just (tv2,r2) <- splitTypeForAll_maybe co2
\r
238 , Just (tv1,r1) <- etaForAll_maybe co1
\r
239 , let r1' = substTyWith [tv1] [TyVarTy tv2] r1
\r
240 = Just (ForAllTy tv1 (opt_trans2 r1' r2))
\r
242 opt_trans_rule co1 co2
\r
243 {- Omitting for now, because unsound
\r
244 | Just (sym1, (ax_tc1, ax1_args, ax_tvs, ax_lhs, ax_rhs)) <- co1_is_axiom_maybe
\r
245 , Just (sym2, (ax_tc2, ax2_args, _, _, _)) <- co2_is_axiom_maybe
\r
250 then substTyWith ax_tvs (opt_transL (map mkSymCoercion ax1_args) ax2_args) ax_rhs
\r
251 else substTyWith ax_tvs (opt_transL ax1_args (map mkSymCoercion ax2_args)) ax_lhs
\r
254 | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- co1_is_axiom_maybe
\r
255 , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co2
\r
258 then mkSymCoercion $ TyConApp ax_tc (opt_transL (map mkSymCoercion cos) ax_args)
\r
259 else TyConApp ax_tc (opt_transL ax_args cos)
\r
261 | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- isAxiom_maybe co2
\r
262 , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co1
\r
265 then mkSymCoercion $ TyConApp ax_tc (opt_transL ax_args (map mkSymCoercion cos))
\r
266 else TyConApp ax_tc (opt_transL cos ax_args)
\r
268 co1_is_axiom_maybe = isAxiom_maybe co1
\r
269 co2_is_axiom_maybe = isAxiom_maybe co2
\r
271 opt_trans_rule co1 co2 -- Identity rule
\r
272 | (ty1,_) <- coercionKind co1
\r
273 , (_,ty2) <- coercionKind co2
\r
274 , ty1 `coreEqType` ty2
\r
277 opt_trans_rule _ _ = Nothing
\r
280 isAxiom_maybe :: Coercion -> Maybe (Bool, (TyCon, [Coercion], [TyVar], Type, Type))
\r
282 | Just (tc, args) <- splitTyConApp_maybe co
\r
283 , Just (_, desc) <- isCoercionTyCon_maybe tc
\r
285 CoAxiom { co_ax_tvs = tvs, co_ax_lhs = lhs, co_ax_rhs = rhs }
\r
286 -> Just (False, (tc, args, tvs, lhs, rhs))
\r
287 CoSym | (arg1:_) <- args
\r
288 -> case isAxiom_maybe arg1 of
\r
290 Just (sym, stuff) -> Just (not sym, stuff)
\r
295 matchesAxiomLhs :: [TyVar] -> Type -> Type -> Maybe [Type]
\r
296 matchesAxiomLhs tvs ty_tmpl ty
\r
297 = case tcMatchTy (mkVarSet tvs) ty_tmpl ty of
\r
299 Just subst -> Just (map (substTyVar subst) tvs)
\r
302 opt_trans_rule_equal_tc :: CoTyConDesc -> [Coercion] -> [Coercion] -> Maybe Coercion
\r
303 -- Rules for Coercion TyCons only
\r
305 -- Push transitivity inside instantiation
\r
306 opt_trans_rule_equal_tc desc [co1,ty1] [co2,ty2]
\r
308 , ty1 `coreEqType` ty2
\r
309 , co1 `compatible_co` co2
\r
310 = Just (mkInstCoercion (opt_trans2 co1 co2) ty1)
\r
312 opt_trans_rule_equal_tc desc [co1] [co2]
\r
313 | CoLeft <- desc, is_compat = Just (mkLeftCoercion res_co)
\r
314 | CoRight <- desc, is_compat = Just (mkRightCoercion res_co)
\r
315 | CoCsel1 <- desc, is_compat = Just (mkCsel1Coercion res_co)
\r
316 | CoCsel2 <- desc, is_compat = Just (mkCsel2Coercion res_co)
\r
317 | CoCselR <- desc, is_compat = Just (mkCselRCoercion res_co)
\r
319 is_compat = co1 `compatible_co` co2
\r
320 res_co = opt_trans2 co1 co2
\r
322 opt_trans_rule_equal_tc _ _ _ = Nothing
\r
325 compatible_co :: Coercion -> Coercion -> Bool
\r
326 -- Check whether (co1 . co2) will be well-kinded
\r
327 compatible_co co1 co2
\r
328 = x1 `coreEqType` x2
\r
330 (_,x1) = coercionKind co1
\r
331 (x2,_) = coercionKind co2
\r
334 etaForAll_maybe :: Coercion -> Maybe (TyVar, Coercion)
\r
335 -- Try to make the coercion be of form (forall tv. co)
\r
337 | Just (tv, r) <- splitForAllTy_maybe co
\r
338 , not (isCoVar tv) -- Check it is a *type* forall, not a (t1~t2)=>co
\r
341 | (ty1,ty2) <- coercionKind co
\r
342 , Just (tv1, _) <- splitTypeForAll_maybe ty1
\r
343 , Just (tv2, _) <- splitTypeForAll_maybe ty2
\r
344 , tyVarKind tv1 `eqKind` tyVarKind tv2
\r
345 = Just (tv1, mkInstCoercion co (mkTyVarTy tv1))
\r
350 etaCoPred_maybe :: Coercion -> Maybe (Coercion, Coercion, Coercion)
\r
351 etaCoPred_maybe co
\r
352 | Just (s,t,r) <- splitCoPredTy_maybe co
\r
355 -- co :: (s1~t1)=>r1 ~ (s2~t2)=>r2
\r
356 | (ty1,ty2) <- coercionKind co -- We know ty1,ty2 have same kind
\r
357 , Just (s1,_,_) <- splitCoPredTy_maybe ty1
\r
358 , Just (s2,_,_) <- splitCoPredTy_maybe ty2
\r
359 , typeKind s1 `eqKind` typeKind s2 -- t1,t2 have same kinds
\r
360 = Just (mkCsel1Coercion co, mkCsel2Coercion co, mkCselRCoercion co)
\r
365 etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)
\r
366 -- Split a coercion g :: t1a t1b ~ t2a t2b
\r
367 -- into (left g, right g) if possible
\r
369 | Just (co1, co2) <- splitAppTy_maybe co
\r
372 | (ty1,ty2) <- coercionKind co
\r
373 , Just (ty1a, _) <- splitAppTy_maybe ty1
\r
374 , Just (ty2a, _) <- splitAppTy_maybe ty2
\r
375 , typeKind ty1a `eqKind` typeKind ty2a
\r
376 = Just (mkLeftCoercion co, mkRightCoercion co)
\r
382 splitTypeForAll_maybe :: Type -> Maybe (TyVar, Type)
\r
383 -- Returns Just only for a *type* forall, not a (t1~t2)=>co
\r
384 splitTypeForAll_maybe ty
\r
385 | Just (tv, rty) <- splitForAllTy_maybe ty
\r
393 isIdNormCo :: NormalCo -> Bool
\r
394 -- Cheap identity test: look for coercions with no coercion variables at all
\r
395 -- So it'll return False for (sym g `trans` g)
\r
396 isIdNormCo ty = go ty
\r
398 go (TyVarTy tv) = not (isCoVar tv)
\r
399 go (AppTy t1 t2) = go t1 && go t2
\r
400 go (FunTy t1 t2) = go t1 && go t2
\r
401 go (ForAllTy tv ty) = go (tyVarKind tv) && go ty
\r
402 go (TyConApp tc tys) = not (isCoercionTyCon tc) && all go tys
\r
403 go (PredTy (IParam _ ty)) = go ty
\r
404 go (PredTy (ClassP _ tys)) = all go tys
\r
405 go (PredTy (EqPred t1 t2)) = go t1 && go t2
\r