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