Refactor handling of decomposition.
[ghc.git] / compiler / types / OptCoercion.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP #-}
4
5 module OptCoercion ( optCoercion, checkAxInstCo ) where
6
7 #include "HsVersions.h"
8
9 import Coercion
10 import Type hiding( substTyVarBndr, substTy, extendTvSubst )
11 import TcType ( exactTyVarsOfType )
12 import TyCon
13 import CoAxiom
14 import Var
15 import VarSet
16 import FamInstEnv ( flattenTys )
17 import VarEnv
18 import StaticFlags ( opt_NoOptCoercion )
19 import Outputable
20 import Pair
21 import FastString
22 import Util
23 import Unify
24 import ListSetOps
25 import InstEnv
26 import Control.Monad ( zipWithM )
27
28 {-
29 ************************************************************************
30 * *
31 Optimising coercions
32 * *
33 ************************************************************************
34
35 Note [Subtle shadowing in coercions]
36 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
37 Supose we optimising a coercion
38 optCoercion (forall (co_X5:t1~t2). ...co_B1...)
39 The co_X5 is a wild-card; the bound variable of a coercion for-all
40 should never appear in the body of the forall. Indeed we often
41 write it like this
42 optCoercion ( (t1~t2) => ...co_B1... )
43
44 Just because it's a wild-card doesn't mean we are free to choose
45 whatever variable we like. For example it'd be wrong for optCoercion
46 to return
47 forall (co_B1:t1~t2). ...co_B1...
48 because now the co_B1 (which is really free) has been captured, and
49 subsequent substitutions will go wrong. That's why we can't use
50 mkCoPredTy in the ForAll case, where this note appears.
51
52 Note [Optimising coercion optimisation]
53 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
54 Looking up a coercion's role or kind is linear in the size of the
55 coercion. Thus, doing this repeatedly during the recursive descent
56 of coercion optimisation is disastrous. We must be careful to avoid
57 doing this if at all possible.
58
59 Because it is generally easy to know a coercion's components' roles
60 from the role of the outer coercion, we pass down the known role of
61 the input in the algorithm below. We also keep functions opt_co2
62 and opt_co3 separate from opt_co4, so that the former two do Phantom
63 checks that opt_co4 can avoid. This is a big win because Phantom coercions
64 rarely appear within non-phantom coercions -- only in some TyConAppCos
65 and some AxiomInstCos. We handle these cases specially by calling
66 opt_co2.
67 -}
68
69 optCoercion :: CvSubst -> Coercion -> NormalCo
70 -- ^ optCoercion applies a substitution to a coercion,
71 -- *and* optimises it to reduce its size
72 optCoercion env co
73 | opt_NoOptCoercion = substCo env co
74 | otherwise = opt_co1 env False co
75
76 type NormalCo = Coercion
77 -- Invariants:
78 -- * The substitution has been fully applied
79 -- * For trans coercions (co1 `trans` co2)
80 -- co1 is not a trans, and neither co1 nor co2 is identity
81 -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
82
83 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
84
85 -- | Do we apply a @sym@ to the result?
86 type SymFlag = Bool
87
88 -- | Do we force the result to be representational?
89 type ReprFlag = Bool
90
91 -- | Optimize a coercion, making no assumptions.
92 opt_co1 :: CvSubst
93 -> SymFlag
94 -> Coercion -> NormalCo
95 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
96 {-
97 opt_co env sym co
98 = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
99 co1 `seq`
100 pprTrace "opt_co done }" (ppr co1) $
101 (WARN( not same_co_kind, ppr co <+> dcolon <+> ppr (coercionType co)
102 $$ ppr co1 <+> dcolon <+> ppr (coercionType co1) )
103 WARN( not (coreEqCoercion co1 simple_result),
104 (text "env=" <+> ppr env) $$
105 (text "input=" <+> ppr co) $$
106 (text "simple=" <+> ppr simple_result) $$
107 (text "opt=" <+> ppr co1) )
108 co1)
109 where
110 co1 = opt_co' env sym co
111 same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
112 Pair s t = coercionKind (substCo env co)
113 (s1,t1) | sym = (t,s)
114 | otherwise = (s,t)
115 Pair s2 t2 = coercionKind co1
116
117 simple_result | sym = mkSymCo (substCo env co)
118 | otherwise = substCo env co
119 -}
120
121 -- See Note [Optimising coercion optimisation]
122 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
123 opt_co2 :: CvSubst
124 -> SymFlag
125 -> Role -- ^ The role of the input coercion
126 -> Coercion -> NormalCo
127 opt_co2 env sym Phantom co = opt_phantom env sym co
128 opt_co2 env sym r co = opt_co3 env sym Nothing r co
129
130 -- See Note [Optimising coercion optimisation]
131 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
132 opt_co3 :: CvSubst -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
133 opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
134 opt_co3 env sym (Just Representational) r co = opt_co4 env sym True r co
135 -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
136 opt_co3 env sym _ r co = opt_co4 env sym False r co
137
138
139 -- See Note [Optimising coercion optimisation]
140 -- | Optimize a non-phantom coercion.
141 opt_co4 :: CvSubst -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
142
143 opt_co4 env _ rep r (Refl _r ty)
144 = ASSERT( r == _r )
145 Refl (chooseRole rep r) (substTy env ty)
146
147 opt_co4 env sym rep r (SymCo co) = opt_co4 env (not sym) rep r co
148
149 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
150 = ASSERT( r == _r )
151 case (rep, r) of
152 (True, Nominal) ->
153 mkTyConAppCo Representational tc
154 (zipWith3 (opt_co3 env sym)
155 (map Just (tyConRolesX Representational tc))
156 (repeat Nominal)
157 cos)
158 (False, Nominal) ->
159 mkTyConAppCo Nominal tc (map (opt_co4 env sym False Nominal) cos)
160 (_, Representational) ->
161 -- must use opt_co2 here, because some roles may be P
162 -- See Note [Optimising coercion optimisation]
163 mkTyConAppCo r tc (zipWith (opt_co2 env sym)
164 (tyConRolesX r tc) -- the current roles
165 cos)
166 (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
167
168 opt_co4 env sym rep r (AppCo co1 co2) = mkAppCo (opt_co4 env sym rep r co1)
169 (opt_co4 env sym False Nominal co2)
170 opt_co4 env sym rep r (ForAllCo tv co)
171 = case substTyVarBndr env tv of
172 (env', tv') -> mkForAllCo tv' (opt_co4 env' sym rep r co)
173 -- Use the "mk" functions to check for nested Refls
174
175 opt_co4 env sym rep r (CoVarCo cv)
176 | Just co <- lookupCoVar env cv
177 = opt_co4 (zapCvSubstEnv env) sym rep r co
178
179 | Just cv1 <- lookupInScope (getCvInScope env) cv
180 = ASSERT( isCoVar cv1 ) wrapRole rep r $ wrapSym sym (CoVarCo cv1)
181 -- cv1 might have a substituted kind!
182
183 | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
184 ASSERT( isCoVar cv )
185 wrapRole rep r $ wrapSym sym (CoVarCo cv)
186
187 opt_co4 env sym rep r (AxiomInstCo con ind cos)
188 -- Do *not* push sym inside top-level axioms
189 -- e.g. if g is a top-level axiom
190 -- g a : f a ~ a
191 -- then (sym (g ty)) /= g (sym ty) !!
192 = ASSERT( r == coAxiomRole con )
193 wrapRole rep (coAxiomRole con) $
194 wrapSym sym $
195 -- some sub-cos might be P: use opt_co2
196 -- See Note [Optimising coercion optimisation]
197 AxiomInstCo con ind (zipWith (opt_co2 env False)
198 (coAxBranchRoles (coAxiomNthBranch con ind))
199 cos)
200 -- Note that the_co does *not* have sym pushed into it
201
202 opt_co4 env sym rep r (UnivCo s _r oty1 oty2)
203 = ASSERT( r == _r )
204 opt_univ env s (chooseRole rep r) a b
205 where
206 (a,b) = if sym then (oty2,oty1) else (oty1,oty2)
207
208 opt_co4 env sym rep r (TransCo co1 co2)
209 -- sym (g `o` h) = sym h `o` sym g
210 | sym = opt_trans in_scope co2' co1'
211 | otherwise = opt_trans in_scope co1' co2'
212 where
213 co1' = opt_co4 env sym rep r co1
214 co2' = opt_co4 env sym rep r co2
215 in_scope = getCvInScope env
216
217 opt_co4 env sym rep r co@(NthCo {}) = opt_nth_co env sym rep r co
218
219 opt_co4 env sym rep r (LRCo lr co)
220 | Just pr_co <- splitAppCo_maybe co
221 = ASSERT( r == Nominal )
222 opt_co4 env sym rep Nominal (pickLR lr pr_co)
223 | Just pr_co <- splitAppCo_maybe co'
224 = ASSERT( r == Nominal )
225 if rep
226 then opt_co4 (zapCvSubstEnv env) False True Nominal (pickLR lr pr_co)
227 else pickLR lr pr_co
228 | otherwise
229 = wrapRole rep Nominal $ LRCo lr co'
230 where
231 co' = opt_co4 env sym False Nominal co
232
233 opt_co4 env sym rep r (InstCo co ty)
234 -- See if the first arg is already a forall
235 -- ...then we can just extend the current substitution
236 | Just (tv, co_body) <- splitForAllCo_maybe co
237 = opt_co4 (extendTvSubst env tv ty') sym rep r co_body
238
239 -- See if it is a forall after optimization
240 -- If so, do an inefficient one-variable substitution
241 | Just (tv, co'_body) <- splitForAllCo_maybe co'
242 = substCoWithTy (getCvInScope env) tv ty' co'_body
243
244 | otherwise = InstCo co' ty'
245 where
246 co' = opt_co4 env sym rep r co
247 ty' = substTy env ty
248
249 opt_co4 env sym _ r (SubCo co)
250 = ASSERT( r == Representational )
251 opt_co4 env sym True Nominal co
252
253 -- XXX: We could add another field to CoAxiomRule that
254 -- would allow us to do custom simplifications.
255 opt_co4 env sym rep r (AxiomRuleCo co ts cs)
256 = ASSERT( r == coaxrRole co )
257 wrapRole rep r $
258 wrapSym sym $
259 AxiomRuleCo co (map (substTy env) ts)
260 (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
261
262
263 -------------
264 -- | Optimize a phantom coercion. The input coercion may not necessarily
265 -- be a phantom, but the output sure will be.
266 opt_phantom :: CvSubst -> SymFlag -> Coercion -> NormalCo
267 opt_phantom env sym co
268 = if sym
269 then opt_univ env (fsLit "opt_phantom") Phantom ty2 ty1
270 else opt_univ env (fsLit "opt_phantom") Phantom ty1 ty2
271 where
272 Pair ty1 ty2 = coercionKind co
273
274 opt_univ :: CvSubst -> FastString -> Role -> Type -> Type -> Coercion
275 opt_univ env prov role oty1 oty2
276 | Just (tc1, tys1) <- splitTyConApp_maybe oty1
277 , Just (tc2, tys2) <- splitTyConApp_maybe oty2
278 , tc1 == tc2
279 = mkTyConAppCo role tc1 (zipWith3 (opt_univ env prov) (tyConRolesX role tc1) tys1 tys2)
280
281 | Just (l1, r1) <- splitAppTy_maybe oty1
282 , Just (l2, r2) <- splitAppTy_maybe oty2
283 , typeKind l1 `eqType` typeKind l2 -- kind(r1) == kind(r2) by consequence
284 = let role' = if role == Phantom then Phantom else Nominal in
285 -- role' is to comform to mkAppCo's precondition
286 mkAppCo (opt_univ env prov role l1 l2) (opt_univ env prov role' r1 r2)
287
288 | Just (tv1, ty1) <- splitForAllTy_maybe oty1
289 , Just (tv2, ty2) <- splitForAllTy_maybe oty2
290 , tyVarKind tv1 `eqType` tyVarKind tv2 -- rule out a weird unsafeCo
291 = case substTyVarBndr2 env tv1 tv2 of { (env1, env2, tv') ->
292 let ty1' = substTy env1 ty1
293 ty2' = substTy env2 ty2 in
294 mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) prov role ty1' ty2') }
295
296 | otherwise
297 = mkUnivCo prov role (substTy env oty1) (substTy env oty2)
298
299 -------------
300 -- NthCo must be handled separately, because it's the one case where we can't
301 -- tell quickly what the component coercion's role is from the containing
302 -- coercion. To avoid repeated coercionRole calls as opt_co1 calls opt_co2,
303 -- we just look for nested NthCo's, which can happen in practice.
304 opt_nth_co :: CvSubst -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
305 opt_nth_co env sym rep r = go []
306 where
307 go ns (NthCo n co) = go (n:ns) co
308 -- previous versions checked if the tycon is decomposable. This
309 -- is redundant, because a non-decomposable tycon under an NthCo
310 -- is entirely bogus. See docs/core-spec/core-spec.pdf.
311 go ns co
312 = opt_nths ns co
313
314 -- input coercion is *not* yet sym'd or opt'd
315 opt_nths [] co = opt_co4 env sym rep r co
316 opt_nths (n:ns) (TyConAppCo _ _ cos) = opt_nths ns (cos `getNth` n)
317
318 -- here, the co isn't a TyConAppCo, so we opt it, hoping to get
319 -- a TyConAppCo as output. We don't know the role, so we use
320 -- opt_co1. This is slightly annoying, because opt_co1 will call
321 -- coercionRole, but as long as we don't have a long chain of
322 -- NthCo's interspersed with some other coercion former, we should
323 -- be OK.
324 opt_nths ns co = opt_nths' ns (opt_co1 env sym co)
325
326 -- input coercion *is* sym'd and opt'd
327 opt_nths' [] co
328 = if rep && (r == Nominal)
329 -- propagate the SubCo:
330 then opt_co4 (zapCvSubstEnv env) False True r co
331 else co
332 opt_nths' (n:ns) (TyConAppCo _ _ cos) = opt_nths' ns (cos `getNth` n)
333 opt_nths' ns co = wrapRole rep r (mk_nths ns co)
334
335 mk_nths [] co = co
336 mk_nths (n:ns) co = mk_nths ns (mkNthCo n co)
337
338 -------------
339 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
340 opt_transList is = zipWith (opt_trans is)
341
342 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
343 opt_trans is co1 co2
344 | isReflCo co1 = co2
345 | otherwise = opt_trans1 is co1 co2
346
347 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
348 -- First arg is not the identity
349 opt_trans1 is co1 co2
350 | isReflCo co2 = co1
351 | otherwise = opt_trans2 is co1 co2
352
353 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
354 -- Neither arg is the identity
355 opt_trans2 is (TransCo co1a co1b) co2
356 -- Don't know whether the sub-coercions are the identity
357 = opt_trans is co1a (opt_trans is co1b co2)
358
359 opt_trans2 is co1 co2
360 | Just co <- opt_trans_rule is co1 co2
361 = co
362
363 opt_trans2 is co1 (TransCo co2a co2b)
364 | Just co1_2a <- opt_trans_rule is co1 co2a
365 = if isReflCo co1_2a
366 then co2b
367 else opt_trans1 is co1_2a co2b
368
369 opt_trans2 _ co1 co2
370 = mkTransCo co1 co2
371
372 ------
373 -- Optimize coercions with a top-level use of transitivity.
374 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
375
376 -- Push transitivity through matching destructors
377 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
378 | d1 == d2
379 , co1 `compatible_co` co2
380 = fireTransRule "PushNth" in_co1 in_co2 $
381 mkNthCo d1 (opt_trans is co1 co2)
382
383 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
384 | d1 == d2
385 , co1 `compatible_co` co2
386 = fireTransRule "PushLR" in_co1 in_co2 $
387 mkLRCo d1 (opt_trans is co1 co2)
388
389 -- Push transitivity inside instantiation
390 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
391 | ty1 `eqType` ty2
392 , co1 `compatible_co` co2
393 = fireTransRule "TrPushInst" in_co1 in_co2 $
394 mkInstCo (opt_trans is co1 co2) ty1
395
396 -- Push transitivity down through matching top-level constructors.
397 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
398 | tc1 == tc2
399 = ASSERT( r1 == r2 )
400 fireTransRule "PushTyConApp" in_co1 in_co2 $
401 TyConAppCo r1 tc1 (opt_transList is cos1 cos2)
402
403 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
404 = fireTransRule "TrPushApp" in_co1 in_co2 $
405 mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
406
407 -- Eta rules
408 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
409 | Just cos2 <- etaTyConAppCo_maybe tc co2
410 = ASSERT( length cos1 == length cos2 )
411 fireTransRule "EtaCompL" co1 co2 $
412 TyConAppCo r tc (opt_transList is cos1 cos2)
413
414 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
415 | Just cos1 <- etaTyConAppCo_maybe tc co1
416 = ASSERT( length cos1 == length cos2 )
417 fireTransRule "EtaCompR" co1 co2 $
418 TyConAppCo r tc (opt_transList is cos1 cos2)
419
420 opt_trans_rule is co1@(AppCo co1a co1b) co2
421 | Just (co2a,co2b) <- etaAppCo_maybe co2
422 = fireTransRule "EtaAppL" co1 co2 $
423 mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
424
425 opt_trans_rule is co1 co2@(AppCo co2a co2b)
426 | Just (co1a,co1b) <- etaAppCo_maybe co1
427 = fireTransRule "EtaAppR" co1 co2 $
428 mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
429
430 -- Push transitivity inside forall
431 opt_trans_rule is co1 co2
432 | Just (tv1,r1) <- splitForAllCo_maybe co1
433 , Just (tv2,r2) <- etaForAllCo_maybe co2
434 , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
435 is' = is `extendInScopeSet` tv1
436 = fireTransRule "EtaAllL" co1 co2 $
437 mkForAllCo tv1 (opt_trans2 is' r1 r2')
438
439 | Just (tv2,r2) <- splitForAllCo_maybe co2
440 , Just (tv1,r1) <- etaForAllCo_maybe co1
441 , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
442 is' = is `extendInScopeSet` tv2
443 = fireTransRule "EtaAllR" co1 co2 $
444 mkForAllCo tv1 (opt_trans2 is' r1' r2)
445
446 -- Push transitivity inside axioms
447 opt_trans_rule is co1 co2
448
449 -- See Note [Why call checkAxInstCo during optimisation]
450 -- TrPushSymAxR
451 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
452 , Just cos2 <- matchAxiom sym con ind co2
453 , True <- sym
454 , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
455 , Nothing <- checkAxInstCo newAxInst
456 = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
457
458 -- TrPushAxR
459 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
460 , Just cos2 <- matchAxiom sym con ind co2
461 , False <- sym
462 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
463 , Nothing <- checkAxInstCo newAxInst
464 = fireTransRule "TrPushAxR" co1 co2 newAxInst
465
466 -- TrPushSymAxL
467 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
468 , Just cos1 <- matchAxiom (not sym) con ind co1
469 , True <- sym
470 , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
471 , Nothing <- checkAxInstCo newAxInst
472 = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
473
474 -- TrPushAxL
475 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
476 , Just cos1 <- matchAxiom (not sym) con ind co1
477 , False <- sym
478 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
479 , Nothing <- checkAxInstCo newAxInst
480 = fireTransRule "TrPushAxL" co1 co2 newAxInst
481
482 -- TrPushAxSym/TrPushSymAx
483 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
484 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
485 , con1 == con2
486 , ind1 == ind2
487 , sym1 == not sym2
488 , let branch = coAxiomNthBranch con1 ind1
489 qtvs = coAxBranchTyVars branch
490 lhs = coAxNthLHS con1 ind1
491 rhs = coAxBranchRHS branch
492 pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
493 , all (`elemVarSet` pivot_tvs) qtvs
494 = fireTransRule "TrPushAxSym" co1 co2 $
495 if sym2
496 then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs -- TrPushAxSym
497 else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs -- TrPushSymAx
498 where
499 co1_is_axiom_maybe = isAxiom_maybe co1
500 co2_is_axiom_maybe = isAxiom_maybe co2
501 role = coercionRole co1 -- should be the same as coercionRole co2!
502
503 opt_trans_rule _ co1 co2 -- Identity rule
504 | (Pair ty1 _, r) <- coercionKindRole co1
505 , Pair _ ty2 <- coercionKind co2
506 , ty1 `eqType` ty2
507 = fireTransRule "RedTypeDirRefl" co1 co2 $
508 Refl r ty2
509
510 opt_trans_rule _ _ _ = Nothing
511
512 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
513 fireTransRule _rule _co1 _co2 res
514 = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
515 Just res
516
517 {-
518 Note [Conflict checking with AxiomInstCo]
519 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
520 Consider the following type family and axiom:
521
522 type family Equal (a :: k) (b :: k) :: Bool
523 type instance where
524 Equal a a = True
525 Equal a b = False
526 --
527 Equal :: forall k::BOX. k -> k -> Bool
528 axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
529 ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }
530
531 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
532 0-based, so this is the second branch of the axiom.) The problem is that, on
533 the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
534 False) and that all is OK. But, all is not OK: we want to use the first branch
535 of the axiom in this case, not the second. The problem is that the parameters
536 of the first branch can unify with the supplied coercions, thus meaning that
537 the first branch should be taken. See also Note [Branched instance checking]
538 in types/FamInstEnv.hs.
539
540 Note [Why call checkAxInstCo during optimisation]
541 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
542 It is possible that otherwise-good-looking optimisations meet with disaster
543 in the presence of axioms with multiple equations. Consider
544
545 type family Equal (a :: *) (b :: *) :: Bool where
546 Equal a a = True
547 Equal a b = False
548 type family Id (a :: *) :: * where
549 Id a = a
550
551 axEq :: { [a::*]. Equal a a ~ True
552 ; [a::*, b::*]. Equal a b ~ False }
553 axId :: [a::*]. Id a ~ a
554
555 co1 = Equal (axId[0] Int) (axId[0] Bool)
556 :: Equal (Id Int) (Id Bool) ~ Equal Int Bool
557 co2 = axEq[1] <Int> <Bool>
558 :: Equal Int Bool ~ False
559
560 We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
561 co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
562 happens when we push the coercions inside? We get
563
564 co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
565 :: Equal (Id Int) (Id Bool) ~ False
566
567 which is bogus! This is because the type system isn't smart enough to know
568 that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
569 families. At the time of writing, I (Richard Eisenberg) couldn't think of
570 a way of detecting this any more efficient than just building the optimised
571 coercion and checking.
572 -}
573
574 -- | Check to make sure that an AxInstCo is internally consistent.
575 -- Returns the conflicting branch, if it exists
576 -- See Note [Conflict checking with AxiomInstCo]
577 checkAxInstCo :: Coercion -> Maybe CoAxBranch
578 -- defined here to avoid dependencies in Coercion
579 -- If you edit this function, you may need to update the GHC formalism
580 -- See Note [GHC Formalism] in CoreLint
581 checkAxInstCo (AxiomInstCo ax ind cos)
582 = let branch = coAxiomNthBranch ax ind
583 tvs = coAxBranchTyVars branch
584 incomps = coAxBranchIncomps branch
585 tys = map (pFst . coercionKind) cos
586 subst = zipOpenTvSubst tvs tys
587 target = Type.substTys subst (coAxBranchLHS branch)
588 in_scope = mkInScopeSet $
589 unionVarSets (map (tyVarsOfTypes . coAxBranchLHS) incomps)
590 flattened_target = flattenTys in_scope target in
591 check_no_conflict flattened_target incomps
592 where
593 check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
594 check_no_conflict _ [] = Nothing
595 check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
596 -- See Note [Apartness] in FamInstEnv
597 | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
598 = check_no_conflict flat rest
599 | otherwise
600 = Just b
601 checkAxInstCo _ = Nothing
602
603 -----------
604 wrapSym :: SymFlag -> Coercion -> Coercion
605 wrapSym sym co | sym = SymCo co
606 | otherwise = co
607
608 -- | Conditionally set a role to be representational
609 wrapRole :: ReprFlag
610 -> Role -- ^ current role
611 -> Coercion -> Coercion
612 wrapRole False _ = id
613 wrapRole True current = downgradeRole Representational current
614
615 -- | If we require a representational role, return that. Otherwise,
616 -- return the "default" role provided.
617 chooseRole :: ReprFlag
618 -> Role -- ^ "default" role
619 -> Role
620 chooseRole True _ = Representational
621 chooseRole _ r = r
622 -----------
623 -- takes two tyvars and builds env'ts to map them to the same tyvar
624 substTyVarBndr2 :: CvSubst -> TyVar -> TyVar
625 -> (CvSubst, CvSubst, TyVar)
626 substTyVarBndr2 env tv1 tv2
627 = case substTyVarBndr env tv1 of
628 (env1, tv1') -> (env1, extendTvSubstAndInScope env tv2 (mkTyVarTy tv1'), tv1')
629
630 zapCvSubstEnv2 :: CvSubst -> CvSubst -> CvSubst
631 zapCvSubstEnv2 env1 env2 = mkCvSubst (is1 `unionInScope` is2) []
632 where is1 = getCvInScope env1
633 is2 = getCvInScope env2
634 -----------
635 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
636 isAxiom_maybe (SymCo co)
637 | Just (sym, con, ind, cos) <- isAxiom_maybe co
638 = Just (not sym, con, ind, cos)
639 isAxiom_maybe (AxiomInstCo con ind cos)
640 = Just (False, con, ind, cos)
641 isAxiom_maybe _ = Nothing
642
643 matchAxiom :: Bool -- True = match LHS, False = match RHS
644 -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
645 -- If we succeed in matching, then *all the quantified type variables are bound*
646 -- E.g. if tvs = [a,b], lhs/rhs = [b], we'll fail
647 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
648 = let (CoAxBranch { cab_tvs = qtvs
649 , cab_roles = roles
650 , cab_lhs = lhs
651 , cab_rhs = rhs }) = coAxiomNthBranch ax ind in
652 case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
653 Nothing -> Nothing
654 Just subst -> zipWithM (liftCoSubstTyVar subst) roles qtvs
655
656 -------------
657 compatible_co :: Coercion -> Coercion -> Bool
658 -- Check whether (co1 . co2) will be well-kinded
659 compatible_co co1 co2
660 = x1 `eqType` x2
661 where
662 Pair _ x1 = coercionKind co1
663 Pair x2 _ = coercionKind co2
664
665 -------------
666 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
667 -- Try to make the coercion be of form (forall tv. co)
668 etaForAllCo_maybe co
669 | Just (tv, r) <- splitForAllCo_maybe co
670 = Just (tv, r)
671
672 | Pair ty1 ty2 <- coercionKind co
673 , Just (tv1, _) <- splitForAllTy_maybe ty1
674 , Just (tv2, _) <- splitForAllTy_maybe ty2
675 , tyVarKind tv1 `eqKind` tyVarKind tv2
676 = Just (tv1, mkInstCo co (mkTyVarTy tv1))
677
678 | otherwise
679 = Nothing
680
681 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
682 -- If possible, split a coercion
683 -- g :: t1a t1b ~ t2a t2b
684 -- into a pair of coercions (left g, right g)
685 etaAppCo_maybe co
686 | Just (co1,co2) <- splitAppCo_maybe co
687 = Just (co1,co2)
688 | (Pair ty1 ty2, Nominal) <- coercionKindRole co
689 , Just (_,t1) <- splitAppTy_maybe ty1
690 , Just (_,t2) <- splitAppTy_maybe ty2
691 , typeKind t1 `eqType` typeKind t2 -- Note [Eta for AppCo]
692 = Just (LRCo CLeft co, LRCo CRight co)
693 | otherwise
694 = Nothing
695
696 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
697 -- If possible, split a coercion
698 -- g :: T s1 .. sn ~ T t1 .. tn
699 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
700 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
701 = ASSERT( tc == tc2 ) Just cos2
702
703 etaTyConAppCo_maybe tc co
704 | mightBeUnsaturatedTyCon tc
705 , Pair ty1 ty2 <- coercionKind co
706 , Just (tc1, tys1) <- splitTyConApp_maybe ty1
707 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
708 , tc1 == tc2
709 , let n = length tys1
710 = ASSERT( tc == tc1 )
711 ASSERT( n == length tys2 )
712 Just (decomposeCo n co)
713 -- NB: n might be <> tyConArity tc
714 -- e.g. data family T a :: * -> *
715 -- g :: T a b ~ T c d
716
717 | otherwise
718 = Nothing
719
720 {-
721 Note [Eta for AppCo]
722 ~~~~~~~~~~~~~~~~~~~~
723 Suppose we have
724 g :: s1 t1 ~ s2 t2
725
726 Then we can't necessarily make
727 left g :: s1 ~ s2
728 right g :: t1 ~ t2
729 because it's possible that
730 s1 :: * -> * t1 :: *
731 s2 :: (*->*) -> * t2 :: * -> *
732 and in that case (left g) does not have the same
733 kind on either side.
734
735 It's enough to check that
736 kind t1 = kind t2
737 because if g is well-kinded then
738 kind (s1 t2) = kind (s2 t2)
739 and these two imply
740 kind s1 = kind s2
741 -}