b1aa646a9795fd06de3f0913327624cb800709aa
[ghc.git] / compiler / types / OptCoercion.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP #-}
4
5 -- The default iteration limit is a bit too low for the definitions
6 -- in this module.
7 #if __GLASGOW_HASKELL__ >= 800
8 {-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
9 #endif
10
11 module OptCoercion ( optCoercion, checkAxInstCo ) where
12
13 #include "HsVersions.h"
14
15 import DynFlags
16 import TyCoRep
17 import Coercion
18 import Type hiding( substTyVarBndr, substTy )
19 import TcType ( exactTyCoVarsOfType )
20 import TyCon
21 import CoAxiom
22 import VarSet
23 import VarEnv
24 import Outputable
25 import FamInstEnv ( flattenTys )
26 import Pair
27 import ListSetOps ( getNth )
28 import Util
29 import Unify
30 import InstEnv
31 import Control.Monad ( zipWithM )
32
33 {-
34 %************************************************************************
35 %* *
36 Optimising coercions
37 %* *
38 %************************************************************************
39
40 Note [Optimising coercion optimisation]
41 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
42 Looking up a coercion's role or kind is linear in the size of the
43 coercion. Thus, doing this repeatedly during the recursive descent
44 of coercion optimisation is disastrous. We must be careful to avoid
45 doing this if at all possible.
46
47 Because it is generally easy to know a coercion's components' roles
48 from the role of the outer coercion, we pass down the known role of
49 the input in the algorithm below. We also keep functions opt_co2
50 and opt_co3 separate from opt_co4, so that the former two do Phantom
51 checks that opt_co4 can avoid. This is a big win because Phantom coercions
52 rarely appear within non-phantom coercions -- only in some TyConAppCos
53 and some AxiomInstCos. We handle these cases specially by calling
54 opt_co2.
55
56 Note [Optimising InstCo]
57 ~~~~~~~~~~~~~~~~~~~~~~~~
58 When we have (InstCo (ForAllCo tv h g) g2), we want to optimise.
59
60 Let's look at the typing rules.
61
62 h : k1 ~ k2
63 tv:k1 |- g : t1 ~ t2
64 -----------------------------
65 ForAllCo tv h g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym h])
66
67 g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
68 g2 : s1 ~ s2
69 --------------------
70 InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]
71
72 We thus want some coercion proving this:
73
74 (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])
75
76 If we substitute the *type* tv for the *coercion*
77 (g2 `mkCoherenceRightCo` sym h) in g, we'll get this result exactly.
78 This is bizarre,
79 though, because we're substituting a type variable with a coercion. However,
80 this operation already exists: it's called *lifting*, and defined in Coercion.
81 We just need to enhance the lifting operation to be able to deal with
82 an ambient substitution, which is why a LiftingContext stores a TCvSubst.
83
84 -}
85
86 optCoercion :: TCvSubst -> Coercion -> NormalCo
87 -- ^ optCoercion applies a substitution to a coercion,
88 -- *and* optimises it to reduce its size
89 optCoercion env co
90 | hasNoOptCoercion unsafeGlobalDynFlags = substCo env co
91 | debugIsOn
92 = let out_co = opt_co1 lc False co
93 (Pair in_ty1 in_ty2, in_role) = coercionKindRole co
94 (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
95 in
96 ASSERT2( substTyUnchecked env in_ty1 `eqType` out_ty1 &&
97 substTyUnchecked env in_ty2 `eqType` out_ty2 &&
98 in_role == out_role
99 , text "optCoercion changed types!"
100 $$ hang (text "in_co:") 2 (ppr co)
101 $$ hang (text "in_ty1:") 2 (ppr in_ty1)
102 $$ hang (text "in_ty2:") 2 (ppr in_ty2)
103 $$ hang (text "out_co:") 2 (ppr out_co)
104 $$ hang (text "out_ty1:") 2 (ppr out_ty1)
105 $$ hang (text "out_ty2:") 2 (ppr out_ty2)
106 $$ hang (text "subst:") 2 (ppr env) )
107 out_co
108
109 | otherwise = opt_co1 lc False co
110 where
111 lc = mkSubstLiftingContext env
112
113 type NormalCo = Coercion
114 -- Invariants:
115 -- * The substitution has been fully applied
116 -- * For trans coercions (co1 `trans` co2)
117 -- co1 is not a trans, and neither co1 nor co2 is identity
118
119 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
120
121 -- | Do we apply a @sym@ to the result?
122 type SymFlag = Bool
123
124 -- | Do we force the result to be representational?
125 type ReprFlag = Bool
126
127 -- | Optimize a coercion, making no assumptions. All coercions in
128 -- the lifting context are already optimized (and sym'd if nec'y)
129 opt_co1 :: LiftingContext
130 -> SymFlag
131 -> Coercion -> NormalCo
132 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
133
134 -- See Note [Optimising coercion optimisation]
135 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
136 opt_co2 :: LiftingContext
137 -> SymFlag
138 -> Role -- ^ The role of the input coercion
139 -> Coercion -> NormalCo
140 opt_co2 env sym Phantom co = opt_phantom env sym co
141 opt_co2 env sym r co = opt_co3 env sym Nothing r co
142
143 -- See Note [Optimising coercion optimisation]
144 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
145 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
146 opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
147 opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True r co
148 -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
149 opt_co3 env sym _ r co = opt_co4_wrap env sym False r co
150
151 -- See Note [Optimising coercion optimisation]
152 -- | Optimize a non-phantom coercion.
153 opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
154
155 opt_co4_wrap = opt_co4
156 {-
157 opt_co4_wrap env sym rep r co
158 = pprTrace "opt_co4_wrap {"
159 ( vcat [ text "Sym:" <+> ppr sym
160 , text "Rep:" <+> ppr rep
161 , text "Role:" <+> ppr r
162 , text "Co:" <+> ppr co ]) $
163 ASSERT( r == coercionRole co )
164 let result = opt_co4 env sym rep r co in
165 pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
166 result
167 -}
168
169 opt_co4 env _ rep r (Refl _r ty)
170 = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
171 text "Found role:" <+> ppr _r $$
172 text "Type:" <+> ppr ty )
173 liftCoSubst (chooseRole rep r) env ty
174
175 opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co
176 -- surprisingly, we don't have to do anything to the env here. This is
177 -- because any "lifting" substitutions in the env are tied to ForAllCos,
178 -- which treat their left and right sides differently. We don't want to
179 -- exchange them.
180
181 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
182 = ASSERT( r == _r )
183 case (rep, r) of
184 (True, Nominal) ->
185 mkTyConAppCo Representational tc
186 (zipWith3 (opt_co3 env sym)
187 (map Just (tyConRolesRepresentational tc))
188 (repeat Nominal)
189 cos)
190 (False, Nominal) ->
191 mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
192 (_, Representational) ->
193 -- must use opt_co2 here, because some roles may be P
194 -- See Note [Optimising coercion optimisation]
195 mkTyConAppCo r tc (zipWith (opt_co2 env sym)
196 (tyConRolesRepresentational tc) -- the current roles
197 cos)
198 (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
199
200 opt_co4 env sym rep r (AppCo co1 co2)
201 = mkAppCo (opt_co4_wrap env sym rep r co1)
202 (opt_co4_wrap env sym False Nominal co2)
203
204 opt_co4 env sym rep r (ForAllCo tv k_co co)
205 = case optForAllCoBndr env sym tv k_co of
206 (env', tv', k_co') -> mkForAllCo tv' k_co' $
207 opt_co4_wrap env' sym rep r co
208 -- Use the "mk" functions to check for nested Refls
209
210 opt_co4 env sym rep r (FunCo _r co1 co2)
211 = ASSERT( r == _r )
212 if rep
213 then mkFunCo Representational co1' co2'
214 else mkFunCo r co1' co2'
215 where
216 co1' = opt_co4_wrap env sym rep r co1
217 co2' = opt_co4_wrap env sym rep r co2
218
219 opt_co4 env sym rep r (CoVarCo cv)
220 | Just co <- lookupCoVar (lcTCvSubst env) cv
221 = opt_co4_wrap (zapLiftingContext env) sym rep r co
222
223 | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl]
224 = Refl (chooseRole rep r) ty1
225
226 | otherwise
227 = ASSERT( isCoVar cv1 )
228 wrapRole rep r $ wrapSym sym $
229 CoVarCo cv1
230
231 where
232 Pair ty1 ty2 = coVarTypes cv1
233
234 cv1 = case lookupInScope (lcInScopeSet env) cv of
235 Just cv1 -> cv1
236 Nothing -> WARN( True, text "opt_co: not in scope:"
237 <+> ppr cv $$ ppr env)
238 cv
239 -- cv1 might have a substituted kind!
240
241
242 opt_co4 env sym rep r (AxiomInstCo con ind cos)
243 -- Do *not* push sym inside top-level axioms
244 -- e.g. if g is a top-level axiom
245 -- g a : f a ~ a
246 -- then (sym (g ty)) /= g (sym ty) !!
247 = ASSERT( r == coAxiomRole con )
248 wrapRole rep (coAxiomRole con) $
249 wrapSym sym $
250 -- some sub-cos might be P: use opt_co2
251 -- See Note [Optimising coercion optimisation]
252 AxiomInstCo con ind (zipWith (opt_co2 env False)
253 (coAxBranchRoles (coAxiomNthBranch con ind))
254 cos)
255 -- Note that the_co does *not* have sym pushed into it
256
257 opt_co4 env sym rep r (UnivCo prov _r t1 t2)
258 = ASSERT( r == _r )
259 opt_univ env sym prov (chooseRole rep r) t1 t2
260
261 opt_co4 env sym rep r (TransCo co1 co2)
262 -- sym (g `o` h) = sym h `o` sym g
263 | sym = opt_trans in_scope co2' co1'
264 | otherwise = opt_trans in_scope co1' co2'
265 where
266 co1' = opt_co4_wrap env sym rep r co1
267 co2' = opt_co4_wrap env sym rep r co2
268 in_scope = lcInScopeSet env
269
270
271 opt_co4 env sym rep r co@(NthCo {}) = opt_nth_co env sym rep r co
272
273 opt_co4 env sym rep r (LRCo lr co)
274 | Just pr_co <- splitAppCo_maybe co
275 = ASSERT( r == Nominal )
276 opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
277 | Just pr_co <- splitAppCo_maybe co'
278 = ASSERT( r == Nominal )
279 if rep
280 then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
281 else pick_lr lr pr_co
282 | otherwise
283 = wrapRole rep Nominal $ LRCo lr co'
284 where
285 co' = opt_co4_wrap env sym False Nominal co
286
287 pick_lr CLeft (l, _) = l
288 pick_lr CRight (_, r) = r
289
290 -- See Note [Optimising InstCo]
291 opt_co4 env sym rep r (InstCo co1 arg)
292 -- forall over type...
293 | Just (tv, kind_co, co_body) <- splitForAllCo_maybe co1
294 = opt_co4_wrap (extendLiftingContext env tv
295 (arg' `mkCoherenceRightCo` mkSymCo kind_co))
296 sym rep r co_body
297
298 -- See if it is a forall after optimization
299 -- If so, do an inefficient one-variable substitution, then re-optimize
300
301 -- forall over type...
302 | Just (tv', kind_co', co_body') <- splitForAllCo_maybe co1'
303 = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
304 (arg' `mkCoherenceRightCo` mkSymCo kind_co'))
305 False False r' co_body'
306
307 | otherwise = InstCo co1' arg'
308 where
309 co1' = opt_co4_wrap env sym rep r co1
310 r' = chooseRole rep r
311 arg' = opt_co4_wrap env sym False Nominal arg
312
313 opt_co4 env sym rep r (CoherenceCo co1 co2)
314 | TransCo col1 cor1 <- co1
315 = opt_co4_wrap env sym rep r (mkTransCo (mkCoherenceCo col1 co2) cor1)
316
317 | TransCo col1' cor1' <- co1'
318 = if sym then opt_trans in_scope col1'
319 (optCoercion (zapTCvSubst (lcTCvSubst env))
320 (mkCoherenceRightCo cor1' co2'))
321 else opt_trans in_scope (mkCoherenceCo col1' co2') cor1'
322
323 | otherwise
324 = wrapSym sym $ mkCoherenceCo (opt_co4_wrap env False rep r co1) co2'
325 where co1' = opt_co4_wrap env sym rep r co1
326 co2' = opt_co4_wrap env False False Nominal co2
327 in_scope = lcInScopeSet env
328
329 opt_co4 env sym _rep r (KindCo co)
330 = ASSERT( r == Nominal )
331 let kco' = promoteCoercion co in
332 case kco' of
333 KindCo co' -> promoteCoercion (opt_co1 env sym co')
334 _ -> opt_co4_wrap env sym False Nominal kco'
335 -- This might be able to be optimized more to do the promotion
336 -- and substitution/optimization at the same time
337
338 opt_co4 env sym _ r (SubCo co)
339 = ASSERT( r == Representational )
340 opt_co4_wrap env sym True Nominal co
341
342 -- This could perhaps be optimized more.
343 opt_co4 env sym rep r (AxiomRuleCo co cs)
344 = ASSERT( r == coaxrRole co )
345 wrapRole rep r $
346 wrapSym sym $
347 AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
348
349 {- Note [Optimise CoVarCo to Refl]
350 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
351 If we have (c :: t~t) we can optimise it to Refl. That increases the
352 chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
353
354 We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
355 in Coercion.
356 -}
357
358 -------------
359 -- | Optimize a phantom coercion. The input coercion may not necessarily
360 -- be a phantom, but the output sure will be.
361 opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
362 opt_phantom env sym co
363 = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
364 where
365 Pair ty1 ty2 = coercionKind co
366
367 opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
368 -> Type -> Type -> Coercion
369 opt_univ env sym (PhantomProv h) _r ty1 ty2
370 | sym = mkPhantomCo h' ty2' ty1'
371 | otherwise = mkPhantomCo h' ty1' ty2'
372 where
373 h' = opt_co4 env sym False Nominal h
374 ty1' = substTy (lcSubstLeft env) ty1
375 ty2' = substTy (lcSubstRight env) ty2
376
377 opt_univ env sym prov role oty1 oty2
378 | Just (tc1, tys1) <- splitTyConApp_maybe oty1
379 , Just (tc2, tys2) <- splitTyConApp_maybe oty2
380 , tc1 == tc2
381 -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
382 -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
383 = let roles = tyConRolesX role tc1
384 arg_cos = zipWith3 (mkUnivCo prov) roles tys1 tys2
385 arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
386 in
387 mkTyConAppCo role tc1 arg_cos'
388
389 -- can't optimize the AppTy case because we can't build the kind coercions.
390
391 | Just (tv1, ty1) <- splitForAllTy_maybe oty1
392 , Just (tv2, ty2) <- splitForAllTy_maybe oty2
393 -- NB: prov isn't interesting here either
394 = let k1 = tyVarKind tv1
395 k2 = tyVarKind tv2
396 eta = mkUnivCo prov Nominal k1 k2
397 -- eta gets opt'ed soon, but not yet.
398 ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
399
400 (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
401 in
402 mkForAllCo tv1' eta' (opt_univ env' sym prov role ty1 ty2')
403
404 | otherwise
405 = let ty1 = substTyUnchecked (lcSubstLeft env) oty1
406 ty2 = substTyUnchecked (lcSubstRight env) oty2
407 (a, b) | sym = (ty2, ty1)
408 | otherwise = (ty1, ty2)
409 in
410 mkUnivCo prov' role a b
411
412 where
413 prov' = case prov of
414 UnsafeCoerceProv -> prov
415 PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
416 ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
417 PluginProv _ -> prov
418 HoleProv h -> pprPanic "opt_univ fell into a hole" (ppr h)
419
420
421 -------------
422 -- NthCo must be handled separately, because it's the one case where we can't
423 -- tell quickly what the component coercion's role is from the containing
424 -- coercion. To avoid repeated coercionRole calls as opt_co1 calls opt_co2,
425 -- we just look for nested NthCo's, which can happen in practice.
426 opt_nth_co :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
427 opt_nth_co env sym rep r = go []
428 where
429 go ns (NthCo n co) = go (n:ns) co
430 -- previous versions checked if the tycon is decomposable. This
431 -- is redundant, because a non-decomposable tycon under an NthCo
432 -- is entirely bogus. See docs/core-spec/core-spec.pdf.
433 go ns co
434 = opt_nths ns co
435
436 -- try to resolve 1 Nth
437 push_nth n (Refl r1 ty)
438 | Just (tc, args) <- splitTyConApp_maybe ty
439 = Just (Refl (nthRole r1 tc n) (args `getNth` n))
440 | n == 0
441 , Just (tv, _) <- splitForAllTy_maybe ty
442 = Just (Refl Nominal (tyVarKind tv))
443 push_nth n (TyConAppCo _ _ cos)
444 = Just (cos `getNth` n)
445 push_nth 0 (ForAllCo _ eta _)
446 = Just eta
447 push_nth _ _ = Nothing
448
449 -- input coercion is *not* yet sym'd or opt'd
450 opt_nths [] co = opt_co4_wrap env sym rep r co
451 opt_nths (n:ns) co
452 | Just co' <- push_nth n co
453 = opt_nths ns co'
454
455 -- here, the co isn't a TyConAppCo, so we opt it, hoping to get
456 -- a TyConAppCo as output. We don't know the role, so we use
457 -- opt_co1. This is slightly annoying, because opt_co1 will call
458 -- coercionRole, but as long as we don't have a long chain of
459 -- NthCo's interspersed with some other coercion former, we should
460 -- be OK.
461 opt_nths ns co = opt_nths' ns (opt_co1 env sym co)
462
463 -- input coercion *is* sym'd and opt'd
464 opt_nths' [] co
465 = if rep && (r == Nominal)
466 -- propagate the SubCo:
467 then opt_co4_wrap (zapLiftingContext env) False True r co
468 else co
469 opt_nths' (n:ns) co
470 | Just co' <- push_nth n co
471 = opt_nths' ns co'
472 opt_nths' ns co = wrapRole rep r (mk_nths ns co)
473
474 mk_nths [] co = co
475 mk_nths (n:ns) co = mk_nths ns (mkNthCo n co)
476
477 -------------
478 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
479 opt_transList is = zipWith (opt_trans is)
480
481 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
482 opt_trans is co1 co2
483 | isReflCo co1 = co2
484 | otherwise = opt_trans1 is co1 co2
485
486 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
487 -- First arg is not the identity
488 opt_trans1 is co1 co2
489 | isReflCo co2 = co1
490 | otherwise = opt_trans2 is co1 co2
491
492 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
493 -- Neither arg is the identity
494 opt_trans2 is (TransCo co1a co1b) co2
495 -- Don't know whether the sub-coercions are the identity
496 = opt_trans is co1a (opt_trans is co1b co2)
497
498 opt_trans2 is co1 co2
499 | Just co <- opt_trans_rule is co1 co2
500 = co
501
502 opt_trans2 is co1 (TransCo co2a co2b)
503 | Just co1_2a <- opt_trans_rule is co1 co2a
504 = if isReflCo co1_2a
505 then co2b
506 else opt_trans1 is co1_2a co2b
507
508 opt_trans2 _ co1 co2
509 = mkTransCo co1 co2
510
511 ------
512 -- Optimize coercions with a top-level use of transitivity.
513 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
514
515 -- Push transitivity through matching destructors
516 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
517 | d1 == d2
518 , co1 `compatible_co` co2
519 = fireTransRule "PushNth" in_co1 in_co2 $
520 mkNthCo d1 (opt_trans is co1 co2)
521
522 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
523 | d1 == d2
524 , co1 `compatible_co` co2
525 = fireTransRule "PushLR" in_co1 in_co2 $
526 mkLRCo d1 (opt_trans is co1 co2)
527
528 -- Push transitivity inside instantiation
529 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
530 | ty1 `eqCoercion` ty2
531 , co1 `compatible_co` co2
532 = fireTransRule "TrPushInst" in_co1 in_co2 $
533 mkInstCo (opt_trans is co1 co2) ty1
534
535 opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
536 in_co2@(UnivCo p2 r2 _tyl2 tyr2)
537 | Just prov' <- opt_trans_prov p1 p2
538 = ASSERT( r1 == r2 )
539 fireTransRule "UnivCo" in_co1 in_co2 $
540 mkUnivCo prov' r1 tyl1 tyr2
541 where
542 -- if the provenances are different, opt'ing will be very confusing
543 opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv = Just UnsafeCoerceProv
544 opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
545 = Just $ PhantomProv $ opt_trans is kco1 kco2
546 opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
547 = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
548 opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
549 opt_trans_prov _ _ = Nothing
550
551 -- Push transitivity down through matching top-level constructors.
552 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
553 | tc1 == tc2
554 = ASSERT( r1 == r2 )
555 fireTransRule "PushTyConApp" in_co1 in_co2 $
556 mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
557
558 opt_trans_rule is in_co1@(FunCo r1 co1a co1b) in_co2@(FunCo r2 co2a co2b)
559 = ASSERT( r1 == r2 ) -- Just like the TyConAppCo/TyConAppCo case
560 fireTransRule "PushFun" in_co1 in_co2 $
561 mkFunCo r1 (opt_trans is co1a co2a) (opt_trans is co1b co2b)
562
563 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
564 = fireTransRule "TrPushApp" in_co1 in_co2 $
565 mkAppCo (opt_trans is co1a co2a)
566 (opt_trans is co1b co2b)
567
568 -- Eta rules
569 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
570 | Just cos2 <- etaTyConAppCo_maybe tc co2
571 = ASSERT( length cos1 == length cos2 )
572 fireTransRule "EtaCompL" co1 co2 $
573 mkTyConAppCo r tc (opt_transList is cos1 cos2)
574
575 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
576 | Just cos1 <- etaTyConAppCo_maybe tc co1
577 = ASSERT( length cos1 == length cos2 )
578 fireTransRule "EtaCompR" co1 co2 $
579 mkTyConAppCo r tc (opt_transList is cos1 cos2)
580
581 opt_trans_rule is co1@(AppCo co1a co1b) co2
582 | Just (co2a,co2b) <- etaAppCo_maybe co2
583 = fireTransRule "EtaAppL" co1 co2 $
584 mkAppCo (opt_trans is co1a co2a)
585 (opt_trans is co1b co2b)
586
587 opt_trans_rule is co1 co2@(AppCo co2a co2b)
588 | Just (co1a,co1b) <- etaAppCo_maybe co1
589 = fireTransRule "EtaAppR" co1 co2 $
590 mkAppCo (opt_trans is co1a co2a)
591 (opt_trans is co1b co2b)
592
593 -- Push transitivity inside forall
594 opt_trans_rule is co1 co2
595 | ForAllCo tv1 eta1 r1 <- co1
596 , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2
597 = push_trans tv1 eta1 r1 tv2 eta2 r2
598
599 | ForAllCo tv2 eta2 r2 <- co2
600 , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1
601 = push_trans tv1 eta1 r1 tv2 eta2 r2
602
603 where
604 push_trans tv1 eta1 r1 tv2 eta2 r2
605 = fireTransRule "EtaAllTy" co1 co2 $
606 mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
607 where
608 is' = is `extendInScopeSet` tv1
609 r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2
610
611 -- Push transitivity inside axioms
612 opt_trans_rule is co1 co2
613
614 -- See Note [Why call checkAxInstCo during optimisation]
615 -- TrPushSymAxR
616 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
617 , True <- sym
618 , Just cos2 <- matchAxiom sym con ind co2
619 , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
620 , Nothing <- checkAxInstCo newAxInst
621 = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
622
623 -- TrPushAxR
624 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
625 , False <- sym
626 , Just cos2 <- matchAxiom sym con ind co2
627 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
628 , Nothing <- checkAxInstCo newAxInst
629 = fireTransRule "TrPushAxR" co1 co2 newAxInst
630
631 -- TrPushSymAxL
632 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
633 , True <- sym
634 , Just cos1 <- matchAxiom (not sym) con ind co1
635 , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
636 , Nothing <- checkAxInstCo newAxInst
637 = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
638
639 -- TrPushAxL
640 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
641 , False <- sym
642 , Just cos1 <- matchAxiom (not sym) con ind co1
643 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
644 , Nothing <- checkAxInstCo newAxInst
645 = fireTransRule "TrPushAxL" co1 co2 newAxInst
646
647 -- TrPushAxSym/TrPushSymAx
648 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
649 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
650 , con1 == con2
651 , ind1 == ind2
652 , sym1 == not sym2
653 , let branch = coAxiomNthBranch con1 ind1
654 qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
655 lhs = coAxNthLHS con1 ind1
656 rhs = coAxBranchRHS branch
657 pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
658 , all (`elemVarSet` pivot_tvs) qtvs
659 = fireTransRule "TrPushAxSym" co1 co2 $
660 if sym2
661 -- TrPushAxSym
662 then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
663 -- TrPushSymAx
664 else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
665 where
666 co1_is_axiom_maybe = isAxiom_maybe co1
667 co2_is_axiom_maybe = isAxiom_maybe co2
668 role = coercionRole co1 -- should be the same as coercionRole co2!
669
670 opt_trans_rule is co1 co2
671 | Just (lco, lh) <- isCohRight_maybe co1
672 , Just (rco, rh) <- isCohLeft_maybe co2
673 , (coercionType lh) `eqType` (coercionType rh)
674 = opt_trans_rule is lco rco
675
676 opt_trans_rule _ co1 co2 -- Identity rule
677 | (Pair ty1 _, r) <- coercionKindRole co1
678 , Pair _ ty2 <- coercionKind co2
679 , ty1 `eqType` ty2
680 = fireTransRule "RedTypeDirRefl" co1 co2 $
681 Refl r ty2
682
683 opt_trans_rule _ _ _ = Nothing
684
685 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
686 fireTransRule _rule _co1 _co2 res
687 = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
688 Just res
689
690 {-
691 Note [Conflict checking with AxiomInstCo]
692 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
693 Consider the following type family and axiom:
694
695 type family Equal (a :: k) (b :: k) :: Bool
696 type instance where
697 Equal a a = True
698 Equal a b = False
699 --
700 Equal :: forall k::*. k -> k -> Bool
701 axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
702 ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
703
704 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
705 0-based, so this is the second branch of the axiom.) The problem is that, on
706 the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
707 False) and that all is OK. But, all is not OK: we want to use the first branch
708 of the axiom in this case, not the second. The problem is that the parameters
709 of the first branch can unify with the supplied coercions, thus meaning that
710 the first branch should be taken. See also Note [Apartness] in
711 types/FamInstEnv.hs.
712
713 Note [Why call checkAxInstCo during optimisation]
714 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
715 It is possible that otherwise-good-looking optimisations meet with disaster
716 in the presence of axioms with multiple equations. Consider
717
718 type family Equal (a :: *) (b :: *) :: Bool where
719 Equal a a = True
720 Equal a b = False
721 type family Id (a :: *) :: * where
722 Id a = a
723
724 axEq :: { [a::*]. Equal a a ~ True
725 ; [a::*, b::*]. Equal a b ~ False }
726 axId :: [a::*]. Id a ~ a
727
728 co1 = Equal (axId[0] Int) (axId[0] Bool)
729 :: Equal (Id Int) (Id Bool) ~ Equal Int Bool
730 co2 = axEq[1] <Int> <Bool>
731 :: Equal Int Bool ~ False
732
733 We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
734 co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
735 happens when we push the coercions inside? We get
736
737 co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
738 :: Equal (Id Int) (Id Bool) ~ False
739
740 which is bogus! This is because the type system isn't smart enough to know
741 that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
742 families. At the time of writing, I (Richard Eisenberg) couldn't think of
743 a way of detecting this any more efficient than just building the optimised
744 coercion and checking.
745 -}
746
747 -- | Check to make sure that an AxInstCo is internally consistent.
748 -- Returns the conflicting branch, if it exists
749 -- See Note [Conflict checking with AxiomInstCo]
750 checkAxInstCo :: Coercion -> Maybe CoAxBranch
751 -- defined here to avoid dependencies in Coercion
752 -- If you edit this function, you may need to update the GHC formalism
753 -- See Note [GHC Formalism] in CoreLint
754 checkAxInstCo (AxiomInstCo ax ind cos)
755 = let branch = coAxiomNthBranch ax ind
756 tvs = coAxBranchTyVars branch
757 cvs = coAxBranchCoVars branch
758 incomps = coAxBranchIncomps branch
759 (tys, cotys) = splitAtList tvs (map (pFst . coercionKind) cos)
760 co_args = map stripCoercionTy cotys
761 subst = zipTvSubst tvs tys `composeTCvSubst`
762 zipCvSubst cvs co_args
763 target = Type.substTys subst (coAxBranchLHS branch)
764 in_scope = mkInScopeSet $
765 unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
766 flattened_target = flattenTys in_scope target in
767 check_no_conflict flattened_target incomps
768 where
769 check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
770 check_no_conflict _ [] = Nothing
771 check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
772 -- See Note [Apartness] in FamInstEnv
773 | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
774 = check_no_conflict flat rest
775 | otherwise
776 = Just b
777 checkAxInstCo _ = Nothing
778
779
780 -----------
781 wrapSym :: SymFlag -> Coercion -> Coercion
782 wrapSym sym co | sym = SymCo co
783 | otherwise = co
784
785 -- | Conditionally set a role to be representational
786 wrapRole :: ReprFlag
787 -> Role -- ^ current role
788 -> Coercion -> Coercion
789 wrapRole False _ = id
790 wrapRole True current = downgradeRole Representational current
791
792 -- | If we require a representational role, return that. Otherwise,
793 -- return the "default" role provided.
794 chooseRole :: ReprFlag
795 -> Role -- ^ "default" role
796 -> Role
797 chooseRole True _ = Representational
798 chooseRole _ r = r
799
800 -----------
801 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
802 isAxiom_maybe (SymCo co)
803 | Just (sym, con, ind, cos) <- isAxiom_maybe co
804 = Just (not sym, con, ind, cos)
805 isAxiom_maybe (AxiomInstCo con ind cos)
806 = Just (False, con, ind, cos)
807 isAxiom_maybe _ = Nothing
808
809 matchAxiom :: Bool -- True = match LHS, False = match RHS
810 -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
811 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
812 | CoAxBranch { cab_tvs = qtvs
813 , cab_cvs = [] -- can't infer these, so fail if there are any
814 , cab_roles = roles
815 , cab_lhs = lhs
816 , cab_rhs = rhs } <- coAxiomNthBranch ax ind
817 , Just subst <- liftCoMatch (mkVarSet qtvs)
818 (if sym then (mkTyConApp tc lhs) else rhs)
819 co
820 , all (`isMappedByLC` subst) qtvs
821 = zipWithM (liftCoSubstTyVar subst) roles qtvs
822
823 | otherwise
824 = Nothing
825
826 -------------
827 -- destruct a CoherenceCo
828 isCohLeft_maybe :: Coercion -> Maybe (Coercion, Coercion)
829 isCohLeft_maybe (CoherenceCo co1 co2) = Just (co1, co2)
830 isCohLeft_maybe _ = Nothing
831
832 -- destruct a (sym (co1 |> co2)).
833 -- if isCohRight_maybe co = Just (co1, co2), then (sym co1) `mkCohRightCo` co2 = co
834 isCohRight_maybe :: Coercion -> Maybe (Coercion, Coercion)
835 isCohRight_maybe (SymCo (CoherenceCo co1 co2)) = Just (mkSymCo co1, co2)
836 isCohRight_maybe _ = Nothing
837
838 -------------
839 compatible_co :: Coercion -> Coercion -> Bool
840 -- Check whether (co1 . co2) will be well-kinded
841 compatible_co co1 co2
842 = x1 `eqType` x2
843 where
844 Pair _ x1 = coercionKind co1
845 Pair x2 _ = coercionKind co2
846
847 -------------
848 {-
849 etaForAllCo_maybe
850 ~~~~~~~~~~~~~~~~~
851 Suppose we have
852
853 g : all a1:k1.t1 ~ all a2:k2.t2
854
855 but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
856
857 g' = all a1:(ForAllKindCo g).(InstCo g (a1 `mkCoherenceRightCo` ForAllKindCo g))
858
859 Call the kind coercion h1 and the body coercion h2. We can see that
860
861 h2 : t1 ~ t2[a2 |-> (a1 |> h2)]
862
863 According to the typing rule for ForAllCo, we get that
864
865 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h2)][a1 |-> a1 |> sym h2])
866
867 or
868
869 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> a1])
870
871 as desired.
872 -}
873 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
874 -- Try to make the coercion be of form (forall tv:kind_co. co)
875 etaForAllCo_maybe co
876 | ForAllCo tv kind_co r <- co
877 = Just (tv, kind_co, r)
878
879 | Pair ty1 ty2 <- coercionKind co
880 , Just (tv1, _) <- splitForAllTy_maybe ty1
881 , isForAllTy ty2
882 , let kind_co = mkNthCo 0 co
883 = Just ( tv1, kind_co
884 , mkInstCo co (mkNomReflCo (TyVarTy tv1) `mkCoherenceRightCo` kind_co) )
885
886 | otherwise
887 = Nothing
888
889 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
890 -- If possible, split a coercion
891 -- g :: t1a t1b ~ t2a t2b
892 -- into a pair of coercions (left g, right g)
893 etaAppCo_maybe co
894 | Just (co1,co2) <- splitAppCo_maybe co
895 = Just (co1,co2)
896 | (Pair ty1 ty2, Nominal) <- coercionKindRole co
897 , Just (_,t1) <- splitAppTy_maybe ty1
898 , Just (_,t2) <- splitAppTy_maybe ty2
899 , let isco1 = isCoercionTy t1
900 , let isco2 = isCoercionTy t2
901 , isco1 == isco2
902 = Just (LRCo CLeft co, LRCo CRight co)
903 | otherwise
904 = Nothing
905
906 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
907 -- If possible, split a coercion
908 -- g :: T s1 .. sn ~ T t1 .. tn
909 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
910 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
911 = ASSERT( tc == tc2 ) Just cos2
912
913 etaTyConAppCo_maybe tc co
914 | mightBeUnsaturatedTyCon tc
915 , (Pair ty1 ty2, r) <- coercionKindRole co
916 , Just (tc1, tys1) <- splitTyConApp_maybe ty1
917 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
918 , tc1 == tc2
919 , isInjectiveTyCon tc r -- See Note [NthCo and newtypes] in TyCoRep
920 , let n = length tys1
921 = ASSERT( tc == tc1 )
922 ASSERT( n == length tys2 )
923 Just (decomposeCo n co)
924 -- NB: n might be <> tyConArity tc
925 -- e.g. data family T a :: * -> *
926 -- g :: T a b ~ T c d
927
928 | otherwise
929 = Nothing
930
931 {-
932 Note [Eta for AppCo]
933 ~~~~~~~~~~~~~~~~~~~~
934 Suppose we have
935 g :: s1 t1 ~ s2 t2
936
937 Then we can't necessarily make
938 left g :: s1 ~ s2
939 right g :: t1 ~ t2
940 because it's possible that
941 s1 :: * -> * t1 :: *
942 s2 :: (*->*) -> * t2 :: * -> *
943 and in that case (left g) does not have the same
944 kind on either side.
945
946 It's enough to check that
947 kind t1 = kind t2
948 because if g is well-kinded then
949 kind (s1 t2) = kind (s2 t2)
950 and these two imply
951 kind s1 = kind s2
952
953 -}
954
955 optForAllCoBndr :: LiftingContext -> Bool
956 -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
957 optForAllCoBndr env sym
958 = substForAllCoBndrCallbackLC sym (opt_co4_wrap env sym False Nominal) env