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