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