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