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