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