5dd7c0c935975f1abfceaf4b7e38e0b774b24721
[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 {-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
8
9 module OptCoercion ( optCoercion, checkAxInstCo ) where
10
11 #include "HsVersions.h"
12
13 import GhcPrelude
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 ; t2 ~ t2 |> 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 :: DynFlags -> TCvSubst -> Coercion -> NormalCo
87 -- ^ optCoercion applies a substitution to a coercion,
88 -- *and* optimises it to reduce its size
89 optCoercion dflags env co
90 | hasNoOptCoercion dflags = substCo env co
91 | otherwise = optCoercion' env co
92
93 optCoercion' :: TCvSubst -> Coercion -> NormalCo
94 optCoercion' env co
95 | debugIsOn
96 = let out_co = opt_co1 lc False co
97 (Pair in_ty1 in_ty2, in_role) = coercionKindRole co
98 (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
99 in
100 ASSERT2( substTy env in_ty1 `eqType` out_ty1 &&
101 substTy env in_ty2 `eqType` out_ty2 &&
102 in_role == out_role
103 , text "optCoercion changed types!"
104 $$ hang (text "in_co:") 2 (ppr co)
105 $$ hang (text "in_ty1:") 2 (ppr in_ty1)
106 $$ hang (text "in_ty2:") 2 (ppr in_ty2)
107 $$ hang (text "out_co:") 2 (ppr out_co)
108 $$ hang (text "out_ty1:") 2 (ppr out_ty1)
109 $$ hang (text "out_ty2:") 2 (ppr out_ty2)
110 $$ hang (text "subst:") 2 (ppr env) )
111 out_co
112
113 | otherwise = opt_co1 lc False co
114 where
115 lc = mkSubstLiftingContext env
116
117 type NormalCo = Coercion
118 -- Invariants:
119 -- * The substitution has been fully applied
120 -- * For trans coercions (co1 `trans` co2)
121 -- co1 is not a trans, and neither co1 nor co2 is identity
122
123 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
124
125 -- | Do we apply a @sym@ to the result?
126 type SymFlag = Bool
127
128 -- | Do we force the result to be representational?
129 type ReprFlag = Bool
130
131 -- | Optimize a coercion, making no assumptions. All coercions in
132 -- the lifting context are already optimized (and sym'd if nec'y)
133 opt_co1 :: LiftingContext
134 -> SymFlag
135 -> Coercion -> NormalCo
136 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
137
138 -- See Note [Optimising coercion optimisation]
139 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
140 opt_co2 :: LiftingContext
141 -> SymFlag
142 -> Role -- ^ The role of the input coercion
143 -> Coercion -> NormalCo
144 opt_co2 env sym Phantom co = opt_phantom env sym co
145 opt_co2 env sym r co = opt_co3 env sym Nothing r co
146
147 -- See Note [Optimising coercion optimisation]
148 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
149 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
150 opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
151 opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True r co
152 -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
153 opt_co3 env sym _ r co = opt_co4_wrap env sym False r co
154
155 -- See Note [Optimising coercion optimisation]
156 -- | Optimize a non-phantom coercion.
157 opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
158
159 opt_co4_wrap = opt_co4
160 {-
161 opt_co4_wrap env sym rep r co
162 = pprTrace "opt_co4_wrap {"
163 ( vcat [ text "Sym:" <+> ppr sym
164 , text "Rep:" <+> ppr rep
165 , text "Role:" <+> ppr r
166 , text "Co:" <+> ppr co ]) $
167 ASSERT( r == coercionRole co )
168 let result = opt_co4 env sym rep r co in
169 pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
170 result
171 -}
172
173 opt_co4 env _ rep r (Refl ty)
174 = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r $$
175 text "Found role:" <+> ppr Nominal $$
176 text "Type:" <+> ppr ty )
177 liftCoSubst (chooseRole rep r) env ty
178
179 opt_co4 env _ rep r (GRefl _r ty MRefl)
180 = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
181 text "Found role:" <+> ppr _r $$
182 text "Type:" <+> ppr ty )
183 liftCoSubst (chooseRole rep r) env ty
184
185 opt_co4 env sym rep r (GRefl _r ty (MCo co))
186 = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
187 text "Found role:" <+> ppr _r $$
188 text "Type:" <+> ppr ty )
189 if isGReflCo co || isGReflCo co'
190 then liftCoSubst r' env ty
191 else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty)
192 where
193 r' = chooseRole rep r
194 ty' = substTy (lcSubstLeft env) ty
195 co' = opt_co4 env False False Nominal co
196
197 opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co
198 -- surprisingly, we don't have to do anything to the env here. This is
199 -- because any "lifting" substitutions in the env are tied to ForAllCos,
200 -- which treat their left and right sides differently. We don't want to
201 -- exchange them.
202
203 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
204 = ASSERT( r == _r )
205 case (rep, r) of
206 (True, Nominal) ->
207 mkTyConAppCo Representational tc
208 (zipWith3 (opt_co3 env sym)
209 (map Just (tyConRolesRepresentational tc))
210 (repeat Nominal)
211 cos)
212 (False, Nominal) ->
213 mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
214 (_, Representational) ->
215 -- must use opt_co2 here, because some roles may be P
216 -- See Note [Optimising coercion optimisation]
217 mkTyConAppCo r tc (zipWith (opt_co2 env sym)
218 (tyConRolesRepresentational tc) -- the current roles
219 cos)
220 (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
221
222 opt_co4 env sym rep r (AppCo co1 co2)
223 = mkAppCo (opt_co4_wrap env sym rep r co1)
224 (opt_co4_wrap env sym False Nominal co2)
225
226 opt_co4 env sym rep r (ForAllCo tv k_co co)
227 = case optForAllCoBndr env sym tv k_co of
228 (env', tv', k_co') -> mkForAllCo tv' k_co' $
229 opt_co4_wrap env' sym rep r co
230 -- Use the "mk" functions to check for nested Refls
231
232 opt_co4 env sym rep r (FunCo _r co1 co2)
233 = ASSERT( r == _r )
234 if rep
235 then mkFunCo Representational co1' co2'
236 else mkFunCo r co1' co2'
237 where
238 co1' = opt_co4_wrap env sym rep r co1
239 co2' = opt_co4_wrap env sym rep r co2
240
241 opt_co4 env sym rep r (CoVarCo cv)
242 | Just co <- lookupCoVar (lcTCvSubst env) cv
243 = opt_co4_wrap (zapLiftingContext env) sym rep r co
244
245 | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl]
246 = mkReflCo (chooseRole rep r) ty1
247
248 | otherwise
249 = ASSERT( isCoVar cv1 )
250 wrapRole rep r $ wrapSym sym $
251 CoVarCo cv1
252
253 where
254 Pair ty1 ty2 = coVarTypes cv1
255
256 cv1 = case lookupInScope (lcInScopeSet env) cv of
257 Just cv1 -> cv1
258 Nothing -> WARN( True, text "opt_co: not in scope:"
259 <+> ppr cv $$ ppr env)
260 cv
261 -- cv1 might have a substituted kind!
262
263 opt_co4 _ _ _ _ (HoleCo h)
264 = pprPanic "opt_univ fell into a hole" (ppr h)
265
266 opt_co4 env sym rep r (AxiomInstCo con ind cos)
267 -- Do *not* push sym inside top-level axioms
268 -- e.g. if g is a top-level axiom
269 -- g a : f a ~ a
270 -- then (sym (g ty)) /= g (sym ty) !!
271 = ASSERT( r == coAxiomRole con )
272 wrapRole rep (coAxiomRole con) $
273 wrapSym sym $
274 -- some sub-cos might be P: use opt_co2
275 -- See Note [Optimising coercion optimisation]
276 AxiomInstCo con ind (zipWith (opt_co2 env False)
277 (coAxBranchRoles (coAxiomNthBranch con ind))
278 cos)
279 -- Note that the_co does *not* have sym pushed into it
280
281 opt_co4 env sym rep r (UnivCo prov _r t1 t2)
282 = ASSERT( r == _r )
283 opt_univ env sym prov (chooseRole rep r) t1 t2
284
285 opt_co4 env sym rep r (TransCo co1 co2)
286 -- sym (g `o` h) = sym h `o` sym g
287 | sym = opt_trans in_scope co2' co1'
288 | otherwise = opt_trans in_scope co1' co2'
289 where
290 co1' = opt_co4_wrap env sym rep r co1
291 co2' = opt_co4_wrap env sym rep r co2
292 in_scope = lcInScopeSet env
293
294 opt_co4 env _sym rep r (NthCo _r n co)
295 | Just (ty, _) <- isReflCo_maybe co
296 , Just (_tc, args) <- ASSERT( r == _r )
297 splitTyConApp_maybe ty
298 = liftCoSubst (chooseRole rep r) env (args `getNth` n)
299 | Just (ty, _) <- isReflCo_maybe co
300 , n == 0
301 , Just (tv, _) <- splitForAllTy_maybe ty
302 = liftCoSubst (chooseRole rep r) env (tyVarKind tv)
303
304 opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
305 = ASSERT( r == r1 )
306 opt_co4_wrap env sym rep r (cos `getNth` n)
307
308 opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
309 = ASSERT( r == _r )
310 ASSERT( n == 0 )
311 opt_co4_wrap env sym rep Nominal eta
312
313 opt_co4 env sym rep r (NthCo _r n co)
314 | TyConAppCo _ _ cos <- co'
315 , let nth_co = cos `getNth` n
316 = if rep && (r == Nominal)
317 -- keep propagating the SubCo
318 then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co
319 else nth_co
320
321 | ForAllCo _ eta _ <- co'
322 = if rep
323 then opt_co4_wrap (zapLiftingContext env) False True Nominal eta
324 else eta
325
326 | otherwise
327 = wrapRole rep r $ NthCo r n co'
328 where
329 co' = opt_co1 env sym co
330
331 opt_co4 env sym rep r (LRCo lr co)
332 | Just pr_co <- splitAppCo_maybe co
333 = ASSERT( r == Nominal )
334 opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
335 | Just pr_co <- splitAppCo_maybe co'
336 = ASSERT( r == Nominal )
337 if rep
338 then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
339 else pick_lr lr pr_co
340 | otherwise
341 = wrapRole rep Nominal $ LRCo lr co'
342 where
343 co' = opt_co4_wrap env sym False Nominal co
344
345 pick_lr CLeft (l, _) = l
346 pick_lr CRight (_, r) = r
347
348 -- See Note [Optimising InstCo]
349 opt_co4 env sym rep r (InstCo co1 arg)
350 -- forall over type...
351 | Just (tv, kind_co, co_body) <- splitForAllCo_maybe co1
352 = opt_co4_wrap (extendLiftingContext env tv
353 (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg'))
354 sym rep r co_body
355
356 -- See if it is a forall after optimization
357 -- If so, do an inefficient one-variable substitution, then re-optimize
358
359 -- forall over type...
360 | Just (tv', kind_co', co_body') <- splitForAllCo_maybe co1'
361 = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
362 (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg'))
363 False False r' co_body'
364
365 | otherwise = InstCo co1' arg'
366 where
367 co1' = opt_co4_wrap env sym rep r co1
368 r' = chooseRole rep r
369 arg' = opt_co4_wrap env sym False Nominal arg
370 Pair _ t2 = coercionKind arg'
371
372 opt_co4 env sym _rep r (KindCo co)
373 = ASSERT( r == Nominal )
374 let kco' = promoteCoercion co in
375 case kco' of
376 KindCo co' -> promoteCoercion (opt_co1 env sym co')
377 _ -> opt_co4_wrap env sym False Nominal kco'
378 -- This might be able to be optimized more to do the promotion
379 -- and substitution/optimization at the same time
380
381 opt_co4 env sym _ r (SubCo co)
382 = ASSERT( r == Representational )
383 opt_co4_wrap env sym True Nominal co
384
385 -- This could perhaps be optimized more.
386 opt_co4 env sym rep r (AxiomRuleCo co cs)
387 = ASSERT( r == coaxrRole co )
388 wrapRole rep r $
389 wrapSym sym $
390 AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
391
392 {- Note [Optimise CoVarCo to Refl]
393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
394 If we have (c :: t~t) we can optimise it to Refl. That increases the
395 chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
396
397 We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
398 in Coercion.
399 -}
400
401 -------------
402 -- | Optimize a phantom coercion. The input coercion may not necessarily
403 -- be a phantom, but the output sure will be.
404 opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
405 opt_phantom env sym co
406 = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
407 where
408 Pair ty1 ty2 = coercionKind co
409
410 {- Note [Differing kinds]
411 ~~~~~~~~~~~~~~~~~~~~~~
412 The two types may not have the same kind (although that would be very unusual).
413 But even if they have the same kind, and the same type constructor, the number
414 of arguments in a `CoTyConApp` can differ. Consider
415
416 Any :: forall k. k
417
418 Any * Int :: *
419 Any (*->*) Maybe Int :: *
420
421 Hence the need to compare argument lengths; see Trac #13658
422 -}
423
424 opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
425 -> Type -> Type -> Coercion
426 opt_univ env sym (PhantomProv h) _r ty1 ty2
427 | sym = mkPhantomCo h' ty2' ty1'
428 | otherwise = mkPhantomCo h' ty1' ty2'
429 where
430 h' = opt_co4 env sym False Nominal h
431 ty1' = substTy (lcSubstLeft env) ty1
432 ty2' = substTy (lcSubstRight env) ty2
433
434 opt_univ env sym prov role oty1 oty2
435 | Just (tc1, tys1) <- splitTyConApp_maybe oty1
436 , Just (tc2, tys2) <- splitTyConApp_maybe oty2
437 , tc1 == tc2
438 , equalLength tys1 tys2 -- see Note [Differing kinds]
439 -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
440 -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
441 = let roles = tyConRolesX role tc1
442 arg_cos = zipWith3 (mkUnivCo prov') roles tys1 tys2
443 arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
444 in
445 mkTyConAppCo role tc1 arg_cos'
446
447 -- can't optimize the AppTy case because we can't build the kind coercions.
448
449 | Just (tv1, ty1) <- splitForAllTy_maybe oty1
450 , Just (tv2, ty2) <- splitForAllTy_maybe oty2
451 -- NB: prov isn't interesting here either
452 = let k1 = tyVarKind tv1
453 k2 = tyVarKind tv2
454 eta = mkUnivCo prov' Nominal k1 k2
455 -- eta gets opt'ed soon, but not yet.
456 ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
457
458 (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
459 in
460 mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
461
462 | otherwise
463 = let ty1 = substTyUnchecked (lcSubstLeft env) oty1
464 ty2 = substTyUnchecked (lcSubstRight env) oty2
465 (a, b) | sym = (ty2, ty1)
466 | otherwise = (ty1, ty2)
467 in
468 mkUnivCo prov' role a b
469
470 where
471 prov' = case prov of
472 UnsafeCoerceProv -> prov
473 PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
474 ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
475 PluginProv _ -> prov
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 -- optimize when co1 is a Refl Co
485 | otherwise = opt_trans1 is co1 co2
486
487 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
488 -- First arg is not the identity
489 opt_trans1 is co1 co2
490 | isReflCo co2 = co1
491 -- optimize when co2 is a Refl Co
492 | otherwise = opt_trans2 is co1 co2
493
494 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
495 -- Neither arg is the identity
496 opt_trans2 is (TransCo co1a co1b) co2
497 -- Don't know whether the sub-coercions are the identity
498 = opt_trans is co1a (opt_trans is co1b co2)
499
500 opt_trans2 is co1 co2
501 | Just co <- opt_trans_rule is co1 co2
502 = co
503
504 opt_trans2 is co1 (TransCo co2a co2b)
505 | Just co1_2a <- opt_trans_rule is co1 co2a
506 = if isReflCo co1_2a
507 then co2b
508 else opt_trans1 is co1_2a co2b
509
510 opt_trans2 _ co1 co2
511 = mkTransCo co1 co2
512
513 ------
514 -- Optimize coercions with a top-level use of transitivity.
515 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
516
517 opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
518 = ASSERT( r1 == r2 )
519 fireTransRule "GRefl" in_co1 in_co2 $
520 mkGReflRightCo r1 t1 (opt_trans is co1 co2)
521
522 -- Push transitivity through matching destructors
523 opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
524 | d1 == d2
525 , coercionRole co1 == coercionRole co2
526 , co1 `compatible_co` co2
527 = ASSERT( r1 == r2 )
528 fireTransRule "PushNth" in_co1 in_co2 $
529 mkNthCo r1 d1 (opt_trans is co1 co2)
530
531 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
532 | d1 == d2
533 , co1 `compatible_co` co2
534 = fireTransRule "PushLR" in_co1 in_co2 $
535 mkLRCo d1 (opt_trans is co1 co2)
536
537 -- Push transitivity inside instantiation
538 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
539 | ty1 `eqCoercion` ty2
540 , co1 `compatible_co` co2
541 = fireTransRule "TrPushInst" in_co1 in_co2 $
542 mkInstCo (opt_trans is co1 co2) ty1
543
544 opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
545 in_co2@(UnivCo p2 r2 _tyl2 tyr2)
546 | Just prov' <- opt_trans_prov p1 p2
547 = ASSERT( r1 == r2 )
548 fireTransRule "UnivCo" in_co1 in_co2 $
549 mkUnivCo prov' r1 tyl1 tyr2
550 where
551 -- if the provenances are different, opt'ing will be very confusing
552 opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv = Just UnsafeCoerceProv
553 opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
554 = Just $ PhantomProv $ opt_trans is kco1 kco2
555 opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
556 = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
557 opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
558 opt_trans_prov _ _ = Nothing
559
560 -- Push transitivity down through matching top-level constructors.
561 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
562 | tc1 == tc2
563 = ASSERT( r1 == r2 )
564 fireTransRule "PushTyConApp" in_co1 in_co2 $
565 mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
566
567 opt_trans_rule is in_co1@(FunCo r1 co1a co1b) in_co2@(FunCo r2 co2a co2b)
568 = ASSERT( r1 == r2 ) -- Just like the TyConAppCo/TyConAppCo case
569 fireTransRule "PushFun" in_co1 in_co2 $
570 mkFunCo r1 (opt_trans is co1a co2a) (opt_trans is co1b co2b)
571
572 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
573 -- Must call opt_trans_rule_app; see Note [EtaAppCo]
574 = opt_trans_rule_app is in_co1 in_co2 co1a [co1b] co2a [co2b]
575
576 -- Eta rules
577 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
578 | Just cos2 <- etaTyConAppCo_maybe tc co2
579 = ASSERT( cos1 `equalLength` cos2 )
580 fireTransRule "EtaCompL" co1 co2 $
581 mkTyConAppCo r tc (opt_transList is cos1 cos2)
582
583 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
584 | Just cos1 <- etaTyConAppCo_maybe tc co1
585 = ASSERT( cos1 `equalLength` cos2 )
586 fireTransRule "EtaCompR" co1 co2 $
587 mkTyConAppCo r tc (opt_transList is cos1 cos2)
588
589 opt_trans_rule is co1@(AppCo co1a co1b) co2
590 | Just (co2a,co2b) <- etaAppCo_maybe co2
591 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
592
593 opt_trans_rule is co1 co2@(AppCo co2a co2b)
594 | Just (co1a,co1b) <- etaAppCo_maybe co1
595 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
596
597 -- Push transitivity inside forall
598 opt_trans_rule is co1 co2
599 | ForAllCo tv1 eta1 r1 <- co1
600 , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2
601 = push_trans tv1 eta1 r1 tv2 eta2 r2
602
603 | ForAllCo tv2 eta2 r2 <- co2
604 , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1
605 = push_trans tv1 eta1 r1 tv2 eta2 r2
606
607 where
608 push_trans tv1 eta1 r1 tv2 eta2 r2
609 -- Given:
610 -- co1 = \/ tv1 : eta1. r1
611 -- co2 = \/ tv2 : eta2. r2
612 -- Wanted:
613 -- \/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1])
614 = fireTransRule "EtaAllTy" co1 co2 $
615 mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
616 where
617 is' = is `extendInScopeSet` tv1
618 r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
619
620 -- Push transitivity inside axioms
621 opt_trans_rule is co1 co2
622
623 -- See Note [Why call checkAxInstCo during optimisation]
624 -- TrPushSymAxR
625 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
626 , True <- sym
627 , Just cos2 <- matchAxiom sym con ind co2
628 , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
629 , Nothing <- checkAxInstCo newAxInst
630 = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
631
632 -- TrPushAxR
633 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
634 , False <- sym
635 , Just cos2 <- matchAxiom sym con ind co2
636 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
637 , Nothing <- checkAxInstCo newAxInst
638 = fireTransRule "TrPushAxR" co1 co2 newAxInst
639
640 -- TrPushSymAxL
641 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
642 , True <- sym
643 , Just cos1 <- matchAxiom (not sym) con ind co1
644 , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
645 , Nothing <- checkAxInstCo newAxInst
646 = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
647
648 -- TrPushAxL
649 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
650 , False <- sym
651 , Just cos1 <- matchAxiom (not sym) con ind co1
652 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
653 , Nothing <- checkAxInstCo newAxInst
654 = fireTransRule "TrPushAxL" co1 co2 newAxInst
655
656 -- TrPushAxSym/TrPushSymAx
657 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
658 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
659 , con1 == con2
660 , ind1 == ind2
661 , sym1 == not sym2
662 , let branch = coAxiomNthBranch con1 ind1
663 qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
664 lhs = coAxNthLHS con1 ind1
665 rhs = coAxBranchRHS branch
666 pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
667 , all (`elemVarSet` pivot_tvs) qtvs
668 = fireTransRule "TrPushAxSym" co1 co2 $
669 if sym2
670 -- TrPushAxSym
671 then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
672 -- TrPushSymAx
673 else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
674 where
675 co1_is_axiom_maybe = isAxiom_maybe co1
676 co2_is_axiom_maybe = isAxiom_maybe co2
677 role = coercionRole co1 -- should be the same as coercionRole co2!
678
679 opt_trans_rule _ co1 co2 -- Identity rule
680 | (Pair ty1 _, r) <- coercionKindRole co1
681 , Pair _ ty2 <- coercionKind co2
682 , ty1 `eqType` ty2
683 = fireTransRule "RedTypeDirRefl" co1 co2 $
684 mkReflCo r ty2
685
686 opt_trans_rule _ _ _ = Nothing
687
688 -- See Note [EtaAppCo]
689 opt_trans_rule_app :: InScopeSet
690 -> Coercion -- original left-hand coercion (printing only)
691 -> Coercion -- original right-hand coercion (printing only)
692 -> Coercion -- left-hand coercion "function"
693 -> [Coercion] -- left-hand coercion "args"
694 -> Coercion -- right-hand coercion "function"
695 -> [Coercion] -- right-hand coercion "args"
696 -> Maybe Coercion
697 opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
698 | AppCo co1aa co1ab <- co1a
699 , Just (co2aa, co2ab) <- etaAppCo_maybe co2a
700 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
701
702 | AppCo co2aa co2ab <- co2a
703 , Just (co1aa, co1ab) <- etaAppCo_maybe co1a
704 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
705
706 | otherwise
707 = ASSERT( co1bs `equalLength` co2bs )
708 fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
709 let Pair _ rt1a = coercionKind co1a
710 (Pair lt2a _, rt2a) = coercionKindRole co2a
711
712 Pair _ rt1bs = traverse coercionKind co1bs
713 Pair lt2bs _ = traverse coercionKind co2bs
714 rt2bs = map coercionRole co2bs
715
716 kcoa = mkKindCo $ buildCoercion lt2a rt1a
717 kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
718
719 co2a' = mkCoherenceLeftCo rt2a lt2a kcoa co2a
720 co2bs' = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs
721 co2bs'' = zipWith mkTransCo co2bs' co2bs
722 in
723 mkAppCos (opt_trans is co1a co2a')
724 (zipWith (opt_trans is) co1bs co2bs'')
725
726 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
727 fireTransRule _rule _co1 _co2 res
728 = Just res
729
730 {-
731 Note [Conflict checking with AxiomInstCo]
732 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
733 Consider the following type family and axiom:
734
735 type family Equal (a :: k) (b :: k) :: Bool
736 type instance where
737 Equal a a = True
738 Equal a b = False
739 --
740 Equal :: forall k::*. k -> k -> Bool
741 axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
742 ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
743
744 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
745 0-based, so this is the second branch of the axiom.) The problem is that, on
746 the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
747 False) and that all is OK. But, all is not OK: we want to use the first branch
748 of the axiom in this case, not the second. The problem is that the parameters
749 of the first branch can unify with the supplied coercions, thus meaning that
750 the first branch should be taken. See also Note [Apartness] in
751 types/FamInstEnv.hs.
752
753 Note [Why call checkAxInstCo during optimisation]
754 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
755 It is possible that otherwise-good-looking optimisations meet with disaster
756 in the presence of axioms with multiple equations. Consider
757
758 type family Equal (a :: *) (b :: *) :: Bool where
759 Equal a a = True
760 Equal a b = False
761 type family Id (a :: *) :: * where
762 Id a = a
763
764 axEq :: { [a::*]. Equal a a ~ True
765 ; [a::*, b::*]. Equal a b ~ False }
766 axId :: [a::*]. Id a ~ a
767
768 co1 = Equal (axId[0] Int) (axId[0] Bool)
769 :: Equal (Id Int) (Id Bool) ~ Equal Int Bool
770 co2 = axEq[1] <Int> <Bool>
771 :: Equal Int Bool ~ False
772
773 We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
774 co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
775 happens when we push the coercions inside? We get
776
777 co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
778 :: Equal (Id Int) (Id Bool) ~ False
779
780 which is bogus! This is because the type system isn't smart enough to know
781 that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
782 families. At the time of writing, I (Richard Eisenberg) couldn't think of
783 a way of detecting this any more efficient than just building the optimised
784 coercion and checking.
785
786 Note [EtaAppCo]
787 ~~~~~~~~~~~~~~~
788 Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
789 like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
790 the resultant coercions might not be well kinded. Here is an example (things
791 labeled with x don't matter in this example):
792
793 k1 :: Type
794 k2 :: Type
795
796 a :: k1 -> Type
797 b :: k1
798
799 h :: k1 ~ k2
800
801 co1a :: x1 ~ (a |> (h -> <Type>)
802 co1b :: x2 ~ (b |> h)
803
804 co2a :: a ~ x3
805 co2b :: b ~ x4
806
807 First, convince yourself of the following:
808
809 co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
810 co2a co2b :: a b ~ x3 x4
811
812 (a |> (h -> <Type>)) (b |> h) `eqType` a b
813
814 That last fact is due to Note [Non-trivial definitional equality] in TyCoRep,
815 where we ignore coercions in types as long as two types' kinds are the same.
816 In our case, we meet this last condition, because
817
818 (a |> (h -> <Type>)) (b |> h) :: Type
819 and
820 a b :: Type
821
822 So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
823 suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
824 kinds don't match up.
825
826 The solution here is to twiddle the kinds in the output coercions. First, we
827 need to find coercions
828
829 ak :: kind(a |> (h -> <Type>)) ~ kind(a)
830 bk :: kind(b |> h) ~ kind(b)
831
832 This can be done with mkKindCo and buildCoercion. The latter assumes two
833 types are identical modulo casts and builds a coercion between them.
834
835 Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
836 output coercions. These are well-kinded.
837
838 Also, note that all of this is done after accumulated any nested AppCo
839 parameters. This step is to avoid quadratic behavior in calling coercionKind.
840
841 The problem described here was first found in dependent/should_compile/dynamic-paper.
842
843 -}
844
845 -- | Check to make sure that an AxInstCo is internally consistent.
846 -- Returns the conflicting branch, if it exists
847 -- See Note [Conflict checking with AxiomInstCo]
848 checkAxInstCo :: Coercion -> Maybe CoAxBranch
849 -- defined here to avoid dependencies in Coercion
850 -- If you edit this function, you may need to update the GHC formalism
851 -- See Note [GHC Formalism] in CoreLint
852 checkAxInstCo (AxiomInstCo ax ind cos)
853 = let branch = coAxiomNthBranch ax ind
854 tvs = coAxBranchTyVars branch
855 cvs = coAxBranchCoVars branch
856 incomps = coAxBranchIncomps branch
857 (tys, cotys) = splitAtList tvs (map (pFst . coercionKind) cos)
858 co_args = map stripCoercionTy cotys
859 subst = zipTvSubst tvs tys `composeTCvSubst`
860 zipCvSubst cvs co_args
861 target = Type.substTys subst (coAxBranchLHS branch)
862 in_scope = mkInScopeSet $
863 unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
864 flattened_target = flattenTys in_scope target in
865 check_no_conflict flattened_target incomps
866 where
867 check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
868 check_no_conflict _ [] = Nothing
869 check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
870 -- See Note [Apartness] in FamInstEnv
871 | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
872 = check_no_conflict flat rest
873 | otherwise
874 = Just b
875 checkAxInstCo _ = Nothing
876
877
878 -----------
879 wrapSym :: SymFlag -> Coercion -> Coercion
880 wrapSym sym co | sym = mkSymCo co
881 | otherwise = co
882
883 -- | Conditionally set a role to be representational
884 wrapRole :: ReprFlag
885 -> Role -- ^ current role
886 -> Coercion -> Coercion
887 wrapRole False _ = id
888 wrapRole True current = downgradeRole Representational current
889
890 -- | If we require a representational role, return that. Otherwise,
891 -- return the "default" role provided.
892 chooseRole :: ReprFlag
893 -> Role -- ^ "default" role
894 -> Role
895 chooseRole True _ = Representational
896 chooseRole _ r = r
897
898 -----------
899 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
900 isAxiom_maybe (SymCo co)
901 | Just (sym, con, ind, cos) <- isAxiom_maybe co
902 = Just (not sym, con, ind, cos)
903 isAxiom_maybe (AxiomInstCo con ind cos)
904 = Just (False, con, ind, cos)
905 isAxiom_maybe _ = Nothing
906
907 matchAxiom :: Bool -- True = match LHS, False = match RHS
908 -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
909 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
910 | CoAxBranch { cab_tvs = qtvs
911 , cab_cvs = [] -- can't infer these, so fail if there are any
912 , cab_roles = roles
913 , cab_lhs = lhs
914 , cab_rhs = rhs } <- coAxiomNthBranch ax ind
915 , Just subst <- liftCoMatch (mkVarSet qtvs)
916 (if sym then (mkTyConApp tc lhs) else rhs)
917 co
918 , all (`isMappedByLC` subst) qtvs
919 = zipWithM (liftCoSubstTyVar subst) roles qtvs
920
921 | otherwise
922 = Nothing
923
924 -------------
925 compatible_co :: Coercion -> Coercion -> Bool
926 -- Check whether (co1 . co2) will be well-kinded
927 compatible_co co1 co2
928 = x1 `eqType` x2
929 where
930 Pair _ x1 = coercionKind co1
931 Pair x2 _ = coercionKind co2
932
933 -------------
934 {-
935 etaForAllCo_maybe
936 ~~~~~~~~~~~~~~~~~
937 Suppose we have
938
939 g : all a1:k1.t1 ~ all a2:k2.t2
940
941 but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
942
943 g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))
944
945 Call the kind coercion h1 and the body coercion h2. We can see that
946
947 h2 : t1 ~ t2[a2 |-> (a1 |> h1)]
948
949 According to the typing rule for ForAllCo, we get that
950
951 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])
952
953 or
954
955 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> a1])
956
957 as desired.
958 -}
959 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
960 -- Try to make the coercion be of form (forall tv:kind_co. co)
961 etaForAllCo_maybe co
962 | ForAllCo tv kind_co r <- co
963 = Just (tv, kind_co, r)
964
965 | Pair ty1 ty2 <- coercionKind co
966 , Just (tv1, _) <- splitForAllTy_maybe ty1
967 , isForAllTy ty2
968 , let kind_co = mkNthCo Nominal 0 co
969 = Just ( tv1, kind_co
970 , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
971
972 | otherwise
973 = Nothing
974
975 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
976 -- If possible, split a coercion
977 -- g :: t1a t1b ~ t2a t2b
978 -- into a pair of coercions (left g, right g)
979 etaAppCo_maybe co
980 | Just (co1,co2) <- splitAppCo_maybe co
981 = Just (co1,co2)
982 | (Pair ty1 ty2, Nominal) <- coercionKindRole co
983 , Just (_,t1) <- splitAppTy_maybe ty1
984 , Just (_,t2) <- splitAppTy_maybe ty2
985 , let isco1 = isCoercionTy t1
986 , let isco2 = isCoercionTy t2
987 , isco1 == isco2
988 = Just (LRCo CLeft co, LRCo CRight co)
989 | otherwise
990 = Nothing
991
992 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
993 -- If possible, split a coercion
994 -- g :: T s1 .. sn ~ T t1 .. tn
995 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
996 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
997 = ASSERT( tc == tc2 ) Just cos2
998
999 etaTyConAppCo_maybe tc co
1000 | mightBeUnsaturatedTyCon tc
1001 , (Pair ty1 ty2, r) <- coercionKindRole co
1002 , Just (tc1, tys1) <- splitTyConApp_maybe ty1
1003 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
1004 , tc1 == tc2
1005 , isInjectiveTyCon tc r -- See Note [NthCo and newtypes] in TyCoRep
1006 , let n = length tys1
1007 , tys2 `lengthIs` n -- This can fail in an erroneous progam
1008 -- E.g. T a ~# T a b
1009 -- Trac #14607
1010 = ASSERT( tc == tc1 )
1011 Just (decomposeCo n co (tyConRolesX r tc1))
1012 -- NB: n might be <> tyConArity tc
1013 -- e.g. data family T a :: * -> *
1014 -- g :: T a b ~ T c d
1015
1016 | otherwise
1017 = Nothing
1018
1019 {-
1020 Note [Eta for AppCo]
1021 ~~~~~~~~~~~~~~~~~~~~
1022 Suppose we have
1023 g :: s1 t1 ~ s2 t2
1024
1025 Then we can't necessarily make
1026 left g :: s1 ~ s2
1027 right g :: t1 ~ t2
1028 because it's possible that
1029 s1 :: * -> * t1 :: *
1030 s2 :: (*->*) -> * t2 :: * -> *
1031 and in that case (left g) does not have the same
1032 kind on either side.
1033
1034 It's enough to check that
1035 kind t1 = kind t2
1036 because if g is well-kinded then
1037 kind (s1 t2) = kind (s2 t2)
1038 and these two imply
1039 kind s1 = kind s2
1040
1041 -}
1042
1043 optForAllCoBndr :: LiftingContext -> Bool
1044 -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
1045 optForAllCoBndr env sym
1046 = substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env