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