2 % (c) The University of Glasgow 2006
\r
6 {-# OPTIONS_GHC -w #-}
\r
11 #include "HsVersions.h"
\r
13 import Unify ( tcMatchTy )
\r
22 import StaticFlags ( opt_NoOptCoercion )
\r
27 %************************************************************************
\r
29 Optimising coercions
\r
31 %************************************************************************
\r
33 Note [Subtle shadowing in coercions]
\r
34 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\r
35 Supose we optimising a coercion
\r
36 optCoercion (forall (co_X5:t1~t2). ...co_B1...)
\r
37 The co_X5 is a wild-card; the bound variable of a coercion for-all
\r
38 should never appear in the body of the forall. Indeed we often
\r
40 optCoercion ( (t1~t2) => ...co_B1... )
\r
42 Just because it's a wild-card doesn't mean we are free to choose
\r
43 whatever variable we like. For example it'd be wrong for optCoercion
\r
45 forall (co_B1:t1~t2). ...co_B1...
\r
46 because now the co_B1 (which is really free) has been captured, and
\r
47 subsequent substitutions will go wrong. That's why we can't use
\r
48 mkCoPredTy in the ForAll case, where this note appears.
\r
51 optCoercion :: TvSubst -> Coercion -> NormalCo
\r
52 -- ^ optCoercion applies a substitution to a coercion,
\r
53 -- *and* optimises it to reduce its size
\r
55 | opt_NoOptCoercion = substTy env co
\r
56 | otherwise = opt_co env False co
\r
58 type NormalCo = Coercion
\r
60 -- * The substitution has been fully applied
\r
61 -- * For trans coercions (co1 `trans` co2)
\r
62 -- co1 is not a trans, and neither co1 nor co2 is identity
\r
63 -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
\r
65 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
\r
67 opt_co, opt_co' :: TvSubst
\r
68 -> Bool -- True <=> return (sym co)
\r
75 -- = pprTrace "opt_co {" (ppr sym <+> ppr co) $
\r
77 -- pprTrace "opt_co done }" (ppr co1)
\r
78 -- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1)
\r
79 -- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
\r
80 = WARN( not (coreEqType co1 simple_result),
\r
81 (text "env=" <+> ppr env) $$
\r
82 (text "input=" <+> ppr co) $$
\r
83 (text "simple=" <+> ppr simple_result) $$
\r
84 (text "opt=" <+> ppr co1) )
\r
87 co1 = opt_co' env sym co
\r
88 same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
\r
89 (s,t) = coercionKind (substTy env co)
\r
90 (s1,t1) | sym = (t,s)
\r
92 (s2,t2) = coercionKind co1
\r
94 simple_result | sym = mkSymCoercion (substTy env co)
\r
95 | otherwise = substTy env co
\r
98 opt_co' env sym (AppTy ty1 ty2) = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)
\r
99 opt_co' env sym (FunTy ty1 ty2) = FunTy (opt_co env sym ty1) (opt_co env sym ty2)
\r
100 opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))
\r
101 opt_co' env sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co env sym ty))
\r
102 opt_co' _ _ co@(PredTy (EqPred {})) = pprPanic "optCoercion" (ppr co)
\r
104 opt_co' env sym co@(TyVarTy tv)
\r
105 | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty
\r
106 | not (isCoVar tv) = co -- Identity; does not mention a CoVar
\r
107 | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..
\r
109 | otherwise = mkSymCoercion co
\r
111 (ty1,ty2) = coVarKind tv
\r
113 opt_co' env sym (ForAllTy tv cor)
\r
114 | isTyVar tv = case substTyVarBndr env tv of
\r
115 (env', tv') -> ForAllTy tv' (opt_co' env' sym cor)
\r
117 opt_co' env sym co@(ForAllTy co_var cor)
\r
119 = WARN( co_var `elemVarSet` tyVarsOfType cor, ppr co )
\r
120 ForAllTy co_var' cor'
\r
122 (co1,co2) = coVarKind co_var
\r
123 co1' = opt_co' env sym co1
\r
124 co2' = opt_co' env sym co2
\r
125 cor' = opt_co' env sym cor
\r
126 co_var' = uniqAway (getTvInScope env) (mkWildCoVar (mkCoKind co1' co2'))
\r
127 -- See Note [Subtle shadowing in coercions]
\r
129 opt_co' env sym (TyConApp tc cos)
\r
130 | Just (arity, desc) <- isCoercionTyCon_maybe tc
\r
131 = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))
\r
132 (map (opt_co env sym) (drop arity cos))
\r
134 = TyConApp tc (map (opt_co env sym) cos)
\r
137 opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo
\r
138 -- Used for CoercionTyCons only
\r
139 -- Arguments are *not* already simplified/substituted
\r
140 opt_co_tc_app env sym tc desc cos
\r
142 CoAxiom {} -- Do *not* push sym inside top-level axioms
\r
143 -- e.g. if g is a top-level axiom
\r
145 -- Then (sym (g ty)) /= g (sym ty) !!
\r
146 | sym -> mkSymCoercion the_co
\r
147 | otherwise -> the_co
\r
149 the_co = TyConApp tc (map (opt_co env False) cos)
\r
150 -- Note that the_co does *not* have sym pushed into it
\r
153 | sym -> opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g
\r
154 | otherwise -> opt_trans opt_co1 opt_co2
\r
157 | sym -> mkUnsafeCoercion ty2' ty1'
\r
158 | otherwise -> mkUnsafeCoercion ty1' ty2'
\r
160 CoSym -> opt_co env (not sym) co1
\r
161 CoLeft -> opt_lr fst
\r
162 CoRight -> opt_lr snd
\r
163 CoCsel1 -> opt_csel fstOf3
\r
164 CoCsel2 -> opt_csel sndOf3
\r
165 CoCselR -> opt_csel thirdOf3
\r
167 CoInst -- See if the first arg is already a forall
\r
168 -- ...then we can just extend the current substitution
\r
169 | Just (tv, co1_body) <- splitForAllTy_maybe co1
\r
170 -> opt_co (extendTvSubst env tv ty2') sym co1_body
\r
172 -- See if is *now* a forall
\r
173 | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1
\r
174 -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution
\r
177 -> TyConApp tc [opt_co1, ty2']
\r
183 ty1' = substTy env co1
\r
184 ty2' = substTy env co2
\r
186 -- These opt_cos have the sym pushed into them
\r
187 opt_co1 = opt_co env sym co1
\r
188 opt_co2 = opt_co env sym co2
\r
190 the_unary_opt_co = TyConApp tc [opt_co1]
\r
192 opt_lr sel = case splitAppTy_maybe opt_co1 of
\r
193 Nothing -> the_unary_opt_co
\r
195 opt_csel sel = case splitCoPredTy_maybe opt_co1 of
\r
196 Nothing -> the_unary_opt_co
\r
200 opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]
\r
201 opt_transL = zipWith opt_trans
\r
203 opt_trans :: NormalCo -> NormalCo -> NormalCo
\r
205 | isIdNormCo co1 = co2
\r
206 | otherwise = opt_trans1 co1 co2
\r
208 opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
\r
209 -- First arg is not the identity
\r
211 | isIdNormCo co2 = co1
\r
212 | otherwise = opt_trans2 co1 co2
\r
214 opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
\r
215 -- Neither arg is the identity
\r
216 opt_trans2 (TyConApp tc [co1a,co1b]) co2
\r
217 | tc `hasKey` transCoercionTyConKey
\r
218 = opt_trans1 co1a (opt_trans2 co1b co2)
\r
220 opt_trans2 co1 co2
\r
221 | Just co <- opt_trans_rule co1 co2
\r
224 opt_trans2 co1 (TyConApp tc [co2a,co2b])
\r
225 | tc `hasKey` transCoercionTyConKey
\r
226 , Just co1_2a <- opt_trans_rule co1 co2a
\r
227 = if isIdNormCo co1_2a
\r
229 else opt_trans2 co1_2a co2b
\r
232 = mkTransCoercion co1 co2
\r
235 opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
\r
236 opt_trans_rule (TyConApp tc1 args1) (TyConApp tc2 args2)
\r
238 = case isCoercionTyCon_maybe tc1 of
\r
240 -> Just (TyConApp tc1 (opt_transL args1 args2))
\r
241 Just (arity, desc)
\r
242 | arity == length args1
\r
243 -> opt_trans_rule_equal_tc desc args1 args2
\r
245 -> case opt_trans_rule_equal_tc desc
\r
246 (take arity args1)
\r
247 (take arity args2) of
\r
248 Just co -> Just $ mkAppTys co $
\r
249 opt_transL (drop arity args1) (drop arity args2)
\r
250 Nothing -> Nothing
\r
252 -- Push transitivity inside apply
\r
253 opt_trans_rule co1 co2
\r
254 | Just (co1a, co1b) <- splitAppTy_maybe co1
\r
255 , Just (co2a, co2b) <- etaApp_maybe co2
\r
256 = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
\r
258 | Just (co2a, co2b) <- splitAppTy_maybe co2
\r
259 , Just (co1a, co1b) <- etaApp_maybe co1
\r
260 = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
\r
262 -- Push transitivity inside (s~t)=>r
\r
263 -- We re-use the CoVar rather than using mkCoPredTy
\r
264 -- See Note [Subtle shadowing in coercions]
\r
265 opt_trans_rule co1 co2
\r
266 | Just (cv1,r1) <- splitForAllTy_maybe co1
\r
268 , Just (s1,t1) <- coVarKind_maybe cv1
\r
269 , Just (s2,t2,r2) <- etaCoPred_maybe co2
\r
270 = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))
\r
273 | Just (cv2,r2) <- splitForAllTy_maybe co2
\r
275 , Just (s2,t2) <- coVarKind_maybe cv2
\r
276 , Just (s1,t1,r1) <- etaCoPred_maybe co1
\r
277 = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))
\r
280 -- Push transitivity inside forall
\r
281 opt_trans_rule co1 co2
\r
282 | Just (tv1,r1) <- splitTypeForAll_maybe co1
\r
283 , Just (tv2,r2) <- etaForAll_maybe co2
\r
284 , let r2' = substTyWith [tv2] [TyVarTy tv1] r2
\r
285 = Just (ForAllTy tv1 (opt_trans2 r1 r2'))
\r
287 | Just (tv2,r2) <- splitTypeForAll_maybe co2
\r
288 , Just (tv1,r1) <- etaForAll_maybe co1
\r
289 , let r1' = substTyWith [tv1] [TyVarTy tv2] r1
\r
290 = Just (ForAllTy tv1 (opt_trans2 r1' r2))
\r
292 opt_trans_rule co1 co2
\r
293 {- Omitting for now, because unsound
\r
294 | Just (sym1, (ax_tc1, ax1_args, ax_tvs, ax_lhs, ax_rhs)) <- co1_is_axiom_maybe
\r
295 , Just (sym2, (ax_tc2, ax2_args, _, _, _)) <- co2_is_axiom_maybe
\r
300 then substTyWith ax_tvs (opt_transL (map mkSymCoercion ax1_args) ax2_args) ax_rhs
\r
301 else substTyWith ax_tvs (opt_transL ax1_args (map mkSymCoercion ax2_args)) ax_lhs
\r
304 | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- co1_is_axiom_maybe
\r
305 , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co2
\r
308 then mkSymCoercion $ TyConApp ax_tc (opt_transL (map mkSymCoercion cos) ax_args)
\r
309 else TyConApp ax_tc (opt_transL ax_args cos)
\r
311 | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- isAxiom_maybe co2
\r
312 , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co1
\r
315 then mkSymCoercion $ TyConApp ax_tc (opt_transL ax_args (map mkSymCoercion cos))
\r
316 else TyConApp ax_tc (opt_transL cos ax_args)
\r
318 co1_is_axiom_maybe = isAxiom_maybe co1
\r
319 co2_is_axiom_maybe = isAxiom_maybe co2
\r
321 opt_trans_rule co1 co2 -- Identity rule
\r
322 | (ty1,_) <- coercionKind co1
\r
323 , (_,ty2) <- coercionKind co2
\r
324 , ty1 `coreEqType` ty2
\r
327 opt_trans_rule _ _ = Nothing
\r
330 isAxiom_maybe :: Coercion -> Maybe (Bool, (TyCon, [Coercion], [TyVar], Type, Type))
\r
332 | Just (tc, args) <- splitTyConApp_maybe co
\r
333 , Just (_, desc) <- isCoercionTyCon_maybe tc
\r
335 CoAxiom { co_ax_tvs = tvs, co_ax_lhs = lhs, co_ax_rhs = rhs }
\r
336 -> Just (False, (tc, args, tvs, lhs, rhs))
\r
337 CoSym | (arg1:_) <- args
\r
338 -> case isAxiom_maybe arg1 of
\r
340 Just (sym, stuff) -> Just (not sym, stuff)
\r
345 matchesAxiomLhs :: [TyVar] -> Type -> Type -> Maybe [Type]
\r
346 matchesAxiomLhs tvs ty_tmpl ty
\r
347 = case tcMatchTy (mkVarSet tvs) ty_tmpl ty of
\r
349 Just subst -> Just (map (substTyVar subst) tvs)
\r
352 opt_trans_rule_equal_tc :: CoTyConDesc -> [Coercion] -> [Coercion] -> Maybe Coercion
\r
353 -- Rules for Coercion TyCons only
\r
355 -- Push transitivity inside instantiation
\r
356 opt_trans_rule_equal_tc desc [co1,ty1] [co2,ty2]
\r
358 , ty1 `coreEqType` ty2
\r
359 , co1 `compatible_co` co2
\r
360 = Just (mkInstCoercion (opt_trans2 co1 co2) ty1)
\r
362 opt_trans_rule_equal_tc desc [co1] [co2]
\r
363 | CoLeft <- desc, is_compat = Just (mkLeftCoercion res_co)
\r
364 | CoRight <- desc, is_compat = Just (mkRightCoercion res_co)
\r
365 | CoCsel1 <- desc, is_compat = Just (mkCsel1Coercion res_co)
\r
366 | CoCsel2 <- desc, is_compat = Just (mkCsel2Coercion res_co)
\r
367 | CoCselR <- desc, is_compat = Just (mkCselRCoercion res_co)
\r
369 is_compat = co1 `compatible_co` co2
\r
370 res_co = opt_trans2 co1 co2
\r
372 opt_trans_rule_equal_tc _ _ _ = Nothing
\r
375 compatible_co :: Coercion -> Coercion -> Bool
\r
376 -- Check whether (co1 . co2) will be well-kinded
\r
377 compatible_co co1 co2
\r
378 = x1 `coreEqType` x2
\r
380 (_,x1) = coercionKind co1
\r
381 (x2,_) = coercionKind co2
\r
384 etaForAll_maybe :: Coercion -> Maybe (TyVar, Coercion)
\r
385 -- Try to make the coercion be of form (forall tv. co)
\r
387 | Just (tv, r) <- splitForAllTy_maybe co
\r
388 , not (isCoVar tv) -- Check it is a *type* forall, not a (t1~t2)=>co
\r
391 | (ty1,ty2) <- coercionKind co
\r
392 , Just (tv1, _) <- splitTypeForAll_maybe ty1
\r
393 , Just (tv2, _) <- splitTypeForAll_maybe ty2
\r
394 , tyVarKind tv1 `eqKind` tyVarKind tv2
\r
395 = Just (tv1, mkInstCoercion co (mkTyVarTy tv1))
\r
400 etaCoPred_maybe :: Coercion -> Maybe (Coercion, Coercion, Coercion)
\r
401 etaCoPred_maybe co
\r
402 | Just (s,t,r) <- splitCoPredTy_maybe co
\r
405 -- co :: (s1~t1)=>r1 ~ (s2~t2)=>r2
\r
406 | (ty1,ty2) <- coercionKind co -- We know ty1,ty2 have same kind
\r
407 , Just (s1,_,_) <- splitCoPredTy_maybe ty1
\r
408 , Just (s2,_,_) <- splitCoPredTy_maybe ty2
\r
409 , typeKind s1 `eqKind` typeKind s2 -- t1,t2 have same kinds
\r
410 = Just (mkCsel1Coercion co, mkCsel2Coercion co, mkCselRCoercion co)
\r
415 etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)
\r
416 -- Split a coercion g :: t1a t1b ~ t2a t2b
\r
417 -- into (left g, right g) if possible
\r
419 | Just (co1, co2) <- splitAppTy_maybe co
\r
422 | (ty1,ty2) <- coercionKind co
\r
423 , Just (ty1a, _) <- splitAppTy_maybe ty1
\r
424 , Just (ty2a, _) <- splitAppTy_maybe ty2
\r
425 , typeKind ty1a `eqKind` typeKind ty2a
\r
426 = Just (mkLeftCoercion co, mkRightCoercion co)
\r
432 splitTypeForAll_maybe :: Type -> Maybe (TyVar, Type)
\r
433 -- Returns Just only for a *type* forall, not a (t1~t2)=>co
\r
434 splitTypeForAll_maybe ty
\r
435 | Just (tv, rty) <- splitForAllTy_maybe ty
\r
443 isIdNormCo :: NormalCo -> Bool
\r
444 -- Cheap identity test: look for coercions with no coercion variables at all
\r
445 -- So it'll return False for (sym g `trans` g)
\r
446 isIdNormCo ty = go ty
\r
448 go (TyVarTy tv) = not (isCoVar tv)
\r
449 go (AppTy t1 t2) = go t1 && go t2
\r
450 go (FunTy t1 t2) = go t1 && go t2
\r
451 go (ForAllTy tv ty) = go (tyVarKind tv) && go ty
\r
452 go (TyConApp tc tys) = not (isCoercionTyCon tc) && all go tys
\r
453 go (PredTy (IParam _ ty)) = go ty
\r
454 go (PredTy (ClassP _ tys)) = all go tys
\r
455 go (PredTy (EqPred t1 t2)) = go t1 && go t2
\r