Coercion Quantification
[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 {-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
8
9 module OptCoercion ( optCoercion, checkAxInstCo ) where
10
11 #include "HsVersions.h"
12
13 import GhcPrelude
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 (1) tv is a type variable
59 When we have (InstCo (ForAllCo tv h g) g2), we want to optimise.
60
61 Let's look at the typing rules.
62
63 h : k1 ~ k2
64 tv:k1 |- g : t1 ~ t2
65 -----------------------------
66 ForAllCo tv h g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym h])
67
68 g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
69 g2 : s1 ~ s2
70 --------------------
71 InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]
72
73 We thus want some coercion proving this:
74
75 (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])
76
77 If we substitute the *type* tv for the *coercion*
78 (g2 ; t2 ~ t2 |> sym h) in g, we'll get this result exactly.
79 This is bizarre,
80 though, because we're substituting a type variable with a coercion. However,
81 this operation already exists: it's called *lifting*, and defined in Coercion.
82 We just need to enhance the lifting operation to be able to deal with
83 an ambient substitution, which is why a LiftingContext stores a TCvSubst.
84
85 (2) cv is a coercion variable
86 Now consider we have (InstCo (ForAllCo cv h g) g2), we want to optimise.
87
88 h : (t1 ~r t2) ~N (t3 ~r t4)
89 cv : t1 ~r t2 |- g : t1' ~r2 t2'
90 n1 = nth r 2 (downgradeRole r N h) :: t1 ~r t3
91 n2 = nth r 3 (downgradeRole r N h) :: t2 ~r t4
92 ------------------------------------------------
93 ForAllCo cv h g : (all cv:t1 ~r t2. t1') ~r2
94 (all cv:t3 ~r t4. t2'[cv |-> n1 ; cv ; sym n2])
95
96 g1 : (all cv:t1 ~r t2. t1') ~ (all cv: t3 ~r t4. t2')
97 g2 : h1 ~N h2
98 h1 : t1 ~r t2
99 h2 : t3 ~r t4
100 ------------------------------------------------
101 InstCo g1 g2 : t1'[cv |-> h1] ~ t2'[cv |-> h2]
102
103 We thus want some coercion proving this:
104
105 t1'[cv |-> h1] ~ t2'[cv |-> n1 ; h2; sym n2]
106
107 So we substitute the coercion variable c for the coercion
108 (h1 ~N (n1; h2; sym n2)) in g.
109 -}
110
111 optCoercion :: DynFlags -> TCvSubst -> Coercion -> NormalCo
112 -- ^ optCoercion applies a substitution to a coercion,
113 -- *and* optimises it to reduce its size
114 optCoercion dflags env co
115 | hasNoOptCoercion dflags = substCo env co
116 | otherwise = optCoercion' env co
117
118 optCoercion' :: TCvSubst -> Coercion -> NormalCo
119 optCoercion' env co
120 | debugIsOn
121 = let out_co = opt_co1 lc False co
122 (Pair in_ty1 in_ty2, in_role) = coercionKindRole co
123 (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
124 in
125 ASSERT2( substTy env in_ty1 `eqType` out_ty1 &&
126 substTy env in_ty2 `eqType` out_ty2 &&
127 in_role == out_role
128 , text "optCoercion changed types!"
129 $$ hang (text "in_co:") 2 (ppr co)
130 $$ hang (text "in_ty1:") 2 (ppr in_ty1)
131 $$ hang (text "in_ty2:") 2 (ppr in_ty2)
132 $$ hang (text "out_co:") 2 (ppr out_co)
133 $$ hang (text "out_ty1:") 2 (ppr out_ty1)
134 $$ hang (text "out_ty2:") 2 (ppr out_ty2)
135 $$ hang (text "subst:") 2 (ppr env) )
136 out_co
137
138 | otherwise = opt_co1 lc False co
139 where
140 lc = mkSubstLiftingContext env
141
142 type NormalCo = Coercion
143 -- Invariants:
144 -- * The substitution has been fully applied
145 -- * For trans coercions (co1 `trans` co2)
146 -- co1 is not a trans, and neither co1 nor co2 is identity
147
148 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
149
150 -- | Do we apply a @sym@ to the result?
151 type SymFlag = Bool
152
153 -- | Do we force the result to be representational?
154 type ReprFlag = Bool
155
156 -- | Optimize a coercion, making no assumptions. All coercions in
157 -- the lifting context are already optimized (and sym'd if nec'y)
158 opt_co1 :: LiftingContext
159 -> SymFlag
160 -> Coercion -> NormalCo
161 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
162
163 -- See Note [Optimising coercion optimisation]
164 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
165 opt_co2 :: LiftingContext
166 -> SymFlag
167 -> Role -- ^ The role of the input coercion
168 -> Coercion -> NormalCo
169 opt_co2 env sym Phantom co = opt_phantom env sym co
170 opt_co2 env sym r co = opt_co3 env sym Nothing r co
171
172 -- See Note [Optimising coercion optimisation]
173 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
174 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
175 opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
176 opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True r co
177 -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
178 opt_co3 env sym _ r co = opt_co4_wrap env sym False r co
179
180 -- See Note [Optimising coercion optimisation]
181 -- | Optimize a non-phantom coercion.
182 opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
183
184 opt_co4_wrap = opt_co4
185 {-
186 opt_co4_wrap env sym rep r co
187 = pprTrace "opt_co4_wrap {"
188 ( vcat [ text "Sym:" <+> ppr sym
189 , text "Rep:" <+> ppr rep
190 , text "Role:" <+> ppr r
191 , text "Co:" <+> ppr co ]) $
192 ASSERT( r == coercionRole co )
193 let result = opt_co4 env sym rep r co in
194 pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
195 result
196 -}
197
198 opt_co4 env _ rep r (Refl ty)
199 = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r $$
200 text "Found role:" <+> ppr Nominal $$
201 text "Type:" <+> ppr ty )
202 liftCoSubst (chooseRole rep r) env ty
203
204 opt_co4 env _ rep r (GRefl _r ty MRefl)
205 = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
206 text "Found role:" <+> ppr _r $$
207 text "Type:" <+> ppr ty )
208 liftCoSubst (chooseRole rep r) env ty
209
210 opt_co4 env sym rep r (GRefl _r ty (MCo co))
211 = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
212 text "Found role:" <+> ppr _r $$
213 text "Type:" <+> ppr ty )
214 if isGReflCo co || isGReflCo co'
215 then liftCoSubst r' env ty
216 else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty)
217 where
218 r' = chooseRole rep r
219 ty' = substTy (lcSubstLeft env) ty
220 co' = opt_co4 env False False Nominal co
221
222 opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co
223 -- surprisingly, we don't have to do anything to the env here. This is
224 -- because any "lifting" substitutions in the env are tied to ForAllCos,
225 -- which treat their left and right sides differently. We don't want to
226 -- exchange them.
227
228 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
229 = ASSERT( r == _r )
230 case (rep, r) of
231 (True, Nominal) ->
232 mkTyConAppCo Representational tc
233 (zipWith3 (opt_co3 env sym)
234 (map Just (tyConRolesRepresentational tc))
235 (repeat Nominal)
236 cos)
237 (False, Nominal) ->
238 mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
239 (_, Representational) ->
240 -- must use opt_co2 here, because some roles may be P
241 -- See Note [Optimising coercion optimisation]
242 mkTyConAppCo r tc (zipWith (opt_co2 env sym)
243 (tyConRolesRepresentational tc) -- the current roles
244 cos)
245 (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
246
247 opt_co4 env sym rep r (AppCo co1 co2)
248 = mkAppCo (opt_co4_wrap env sym rep r co1)
249 (opt_co4_wrap env sym False Nominal co2)
250
251 opt_co4 env sym rep r (ForAllCo tv k_co co)
252 = case optForAllCoBndr env sym tv k_co of
253 (env', tv', k_co') -> mkForAllCo tv' k_co' $
254 opt_co4_wrap env' sym rep r co
255 -- Use the "mk" functions to check for nested Refls
256
257 opt_co4 env sym rep r (FunCo _r co1 co2)
258 = ASSERT( r == _r )
259 if rep
260 then mkFunCo Representational co1' co2'
261 else mkFunCo r co1' co2'
262 where
263 co1' = opt_co4_wrap env sym rep r co1
264 co2' = opt_co4_wrap env sym rep r co2
265
266 opt_co4 env sym rep r (CoVarCo cv)
267 | Just co <- lookupCoVar (lcTCvSubst env) cv
268 = opt_co4_wrap (zapLiftingContext env) sym rep r co
269
270 | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl]
271 = mkReflCo (chooseRole rep r) ty1
272
273 | otherwise
274 = ASSERT( isCoVar cv1 )
275 wrapRole rep r $ wrapSym sym $
276 CoVarCo cv1
277
278 where
279 Pair ty1 ty2 = coVarTypes cv1
280
281 cv1 = case lookupInScope (lcInScopeSet env) cv of
282 Just cv1 -> cv1
283 Nothing -> WARN( True, text "opt_co: not in scope:"
284 <+> ppr cv $$ ppr env)
285 cv
286 -- cv1 might have a substituted kind!
287
288 opt_co4 _ _ _ _ (HoleCo h)
289 = pprPanic "opt_univ fell into a hole" (ppr h)
290
291 opt_co4 env sym rep r (AxiomInstCo con ind cos)
292 -- Do *not* push sym inside top-level axioms
293 -- e.g. if g is a top-level axiom
294 -- g a : f a ~ a
295 -- then (sym (g ty)) /= g (sym ty) !!
296 = ASSERT( r == coAxiomRole con )
297 wrapRole rep (coAxiomRole con) $
298 wrapSym sym $
299 -- some sub-cos might be P: use opt_co2
300 -- See Note [Optimising coercion optimisation]
301 AxiomInstCo con ind (zipWith (opt_co2 env False)
302 (coAxBranchRoles (coAxiomNthBranch con ind))
303 cos)
304 -- Note that the_co does *not* have sym pushed into it
305
306 opt_co4 env sym rep r (UnivCo prov _r t1 t2)
307 = ASSERT( r == _r )
308 opt_univ env sym prov (chooseRole rep r) t1 t2
309
310 opt_co4 env sym rep r (TransCo co1 co2)
311 -- sym (g `o` h) = sym h `o` sym g
312 | sym = opt_trans in_scope co2' co1'
313 | otherwise = opt_trans in_scope co1' co2'
314 where
315 co1' = opt_co4_wrap env sym rep r co1
316 co2' = opt_co4_wrap env sym rep r co2
317 in_scope = lcInScopeSet env
318
319 opt_co4 env _sym rep r (NthCo _r n co)
320 | Just (ty, _) <- isReflCo_maybe co
321 , Just (_tc, args) <- ASSERT( r == _r )
322 splitTyConApp_maybe ty
323 = liftCoSubst (chooseRole rep r) env (args `getNth` n)
324 | Just (ty, _) <- isReflCo_maybe co
325 , n == 0
326 , Just (tv, _) <- splitForAllTy_maybe ty
327 -- works for both tyvar and covar
328 = liftCoSubst (chooseRole rep r) env (varType tv)
329
330 opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
331 = ASSERT( r == r1 )
332 opt_co4_wrap env sym rep r (cos `getNth` n)
333
334 opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
335 -- works for both tyvar and covar
336 = ASSERT( r == _r )
337 ASSERT( n == 0 )
338 opt_co4_wrap env sym rep Nominal eta
339
340 opt_co4 env sym rep r (NthCo _r n co)
341 | TyConAppCo _ _ cos <- co'
342 , let nth_co = cos `getNth` n
343 = if rep && (r == Nominal)
344 -- keep propagating the SubCo
345 then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co
346 else nth_co
347
348 | ForAllCo _ eta _ <- co'
349 = if rep
350 then opt_co4_wrap (zapLiftingContext env) False True Nominal eta
351 else eta
352
353 | otherwise
354 = wrapRole rep r $ NthCo r n co'
355 where
356 co' = opt_co1 env sym co
357
358 opt_co4 env sym rep r (LRCo lr co)
359 | Just pr_co <- splitAppCo_maybe co
360 = ASSERT( r == Nominal )
361 opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
362 | Just pr_co <- splitAppCo_maybe co'
363 = ASSERT( r == Nominal )
364 if rep
365 then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
366 else pick_lr lr pr_co
367 | otherwise
368 = wrapRole rep Nominal $ LRCo lr co'
369 where
370 co' = opt_co4_wrap env sym False Nominal co
371
372 pick_lr CLeft (l, _) = l
373 pick_lr CRight (_, r) = r
374
375 -- See Note [Optimising InstCo]
376 opt_co4 env sym rep r (InstCo co1 arg)
377 -- forall over type...
378 | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
379 = opt_co4_wrap (extendLiftingContext env tv
380 (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg'))
381 -- kind_co :: k1 ~ k2
382 -- arg' :: (t1 :: k1) ~ (t2 :: k2)
383 -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
384 sym rep r co_body
385
386 -- forall over coercion...
387 | Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1
388 , CoercionTy h1 <- t1
389 , CoercionTy h2 <- t2
390 = let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
391 in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body
392
393 -- See if it is a forall after optimization
394 -- If so, do an inefficient one-variable substitution, then re-optimize
395
396 -- forall over type...
397 | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
398 = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
399 (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg'))
400 False False r' co_body'
401
402 -- forall over coercion...
403 | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
404 , CoercionTy h1 <- t1
405 , CoercionTy h2 <- t2
406 = let new_co = mk_new_co cv' kind_co' h1 h2
407 in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
408 False False r' co_body'
409
410 | otherwise = InstCo co1' arg'
411 where
412 co1' = opt_co4_wrap env sym rep r co1
413 r' = chooseRole rep r
414 arg' = opt_co4_wrap env sym False Nominal arg
415 Pair t1 t2 = coercionKind arg'
416
417 mk_new_co cv kind_co h1 h2
418 = let -- h1 :: (t1 ~ t2)
419 -- h2 :: (t3 ~ t4)
420 -- kind_co :: (t1 ~ t2) ~ (t3 ~ t4)
421 -- n1 :: t1 ~ t3
422 -- n2 :: t2 ~ t4
423 -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
424 r2 = coVarRole cv
425 kind_co' = downgradeRole r2 Nominal kind_co
426 n1 = mkNthCo r2 2 kind_co'
427 n2 = mkNthCo r2 3 kind_co'
428 in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
429 (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
430
431 opt_co4 env sym _rep r (KindCo co)
432 = ASSERT( r == Nominal )
433 let kco' = promoteCoercion co in
434 case kco' of
435 KindCo co' -> promoteCoercion (opt_co1 env sym co')
436 _ -> opt_co4_wrap env sym False Nominal kco'
437 -- This might be able to be optimized more to do the promotion
438 -- and substitution/optimization at the same time
439
440 opt_co4 env sym _ r (SubCo co)
441 = ASSERT( r == Representational )
442 opt_co4_wrap env sym True Nominal co
443
444 -- This could perhaps be optimized more.
445 opt_co4 env sym rep r (AxiomRuleCo co cs)
446 = ASSERT( r == coaxrRole co )
447 wrapRole rep r $
448 wrapSym sym $
449 AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
450
451 {- Note [Optimise CoVarCo to Refl]
452 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
453 If we have (c :: t~t) we can optimise it to Refl. That increases the
454 chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
455
456 We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
457 in Coercion.
458 -}
459
460 -------------
461 -- | Optimize a phantom coercion. The input coercion may not necessarily
462 -- be a phantom, but the output sure will be.
463 opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
464 opt_phantom env sym co
465 = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
466 where
467 Pair ty1 ty2 = coercionKind co
468
469 {- Note [Differing kinds]
470 ~~~~~~~~~~~~~~~~~~~~~~
471 The two types may not have the same kind (although that would be very unusual).
472 But even if they have the same kind, and the same type constructor, the number
473 of arguments in a `CoTyConApp` can differ. Consider
474
475 Any :: forall k. k
476
477 Any * Int :: *
478 Any (*->*) Maybe Int :: *
479
480 Hence the need to compare argument lengths; see Trac #13658
481 -}
482
483 opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
484 -> Type -> Type -> Coercion
485 opt_univ env sym (PhantomProv h) _r ty1 ty2
486 | sym = mkPhantomCo h' ty2' ty1'
487 | otherwise = mkPhantomCo h' ty1' ty2'
488 where
489 h' = opt_co4 env sym False Nominal h
490 ty1' = substTy (lcSubstLeft env) ty1
491 ty2' = substTy (lcSubstRight env) ty2
492
493 opt_univ env sym prov role oty1 oty2
494 | Just (tc1, tys1) <- splitTyConApp_maybe oty1
495 , Just (tc2, tys2) <- splitTyConApp_maybe oty2
496 , tc1 == tc2
497 , equalLength tys1 tys2 -- see Note [Differing kinds]
498 -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
499 -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
500 = let roles = tyConRolesX role tc1
501 arg_cos = zipWith3 (mkUnivCo prov') roles tys1 tys2
502 arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
503 in
504 mkTyConAppCo role tc1 arg_cos'
505
506 -- can't optimize the AppTy case because we can't build the kind coercions.
507
508 | Just (tv1, ty1) <- splitForAllTy_ty_maybe oty1
509 , Just (tv2, ty2) <- splitForAllTy_ty_maybe oty2
510 -- NB: prov isn't interesting here either
511 = let k1 = tyVarKind tv1
512 k2 = tyVarKind tv2
513 eta = mkUnivCo prov' Nominal k1 k2
514 -- eta gets opt'ed soon, but not yet.
515 ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
516
517 (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
518 in
519 mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
520
521 | Just (cv1, ty1) <- splitForAllTy_co_maybe oty1
522 , Just (cv2, ty2) <- splitForAllTy_co_maybe oty2
523 -- NB: prov isn't interesting here either
524 = let k1 = varType cv1
525 k2 = varType cv2
526 r' = coVarRole cv1
527 eta = mkUnivCo prov' Nominal k1 k2
528 eta_d = downgradeRole r' Nominal eta
529 -- eta gets opt'ed soon, but not yet.
530 n_co = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo`
531 (mkCoVarCo cv1) `mkTransCo`
532 (mkNthCo r' 3 eta_d)
533 ty2' = substTyWithCoVars [cv2] [n_co] ty2
534
535 (env', cv1', eta') = optForAllCoBndr env sym cv1 eta
536 in
537 mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2')
538
539 | otherwise
540 = let ty1 = substTyUnchecked (lcSubstLeft env) oty1
541 ty2 = substTyUnchecked (lcSubstRight env) oty2
542 (a, b) | sym = (ty2, ty1)
543 | otherwise = (ty1, ty2)
544 in
545 mkUnivCo prov' role a b
546
547 where
548 prov' = case prov of
549 UnsafeCoerceProv -> prov
550 PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
551 ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
552 PluginProv _ -> prov
553
554 -------------
555 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
556 opt_transList is = zipWith (opt_trans is)
557
558 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
559 opt_trans is co1 co2
560 | isReflCo co1 = co2
561 -- optimize when co1 is a Refl Co
562 | otherwise = opt_trans1 is co1 co2
563
564 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
565 -- First arg is not the identity
566 opt_trans1 is co1 co2
567 | isReflCo co2 = co1
568 -- optimize when co2 is a Refl Co
569 | otherwise = opt_trans2 is co1 co2
570
571 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
572 -- Neither arg is the identity
573 opt_trans2 is (TransCo co1a co1b) co2
574 -- Don't know whether the sub-coercions are the identity
575 = opt_trans is co1a (opt_trans is co1b co2)
576
577 opt_trans2 is co1 co2
578 | Just co <- opt_trans_rule is co1 co2
579 = co
580
581 opt_trans2 is co1 (TransCo co2a co2b)
582 | Just co1_2a <- opt_trans_rule is co1 co2a
583 = if isReflCo co1_2a
584 then co2b
585 else opt_trans1 is co1_2a co2b
586
587 opt_trans2 _ co1 co2
588 = mkTransCo co1 co2
589
590 ------
591 -- Optimize coercions with a top-level use of transitivity.
592 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
593
594 opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
595 = ASSERT( r1 == r2 )
596 fireTransRule "GRefl" in_co1 in_co2 $
597 mkGReflRightCo r1 t1 (opt_trans is co1 co2)
598
599 -- Push transitivity through matching destructors
600 opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
601 | d1 == d2
602 , coercionRole co1 == coercionRole co2
603 , co1 `compatible_co` co2
604 = ASSERT( r1 == r2 )
605 fireTransRule "PushNth" in_co1 in_co2 $
606 mkNthCo r1 d1 (opt_trans is co1 co2)
607
608 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
609 | d1 == d2
610 , co1 `compatible_co` co2
611 = fireTransRule "PushLR" in_co1 in_co2 $
612 mkLRCo d1 (opt_trans is co1 co2)
613
614 -- Push transitivity inside instantiation
615 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
616 | ty1 `eqCoercion` ty2
617 , co1 `compatible_co` co2
618 = fireTransRule "TrPushInst" in_co1 in_co2 $
619 mkInstCo (opt_trans is co1 co2) ty1
620
621 opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
622 in_co2@(UnivCo p2 r2 _tyl2 tyr2)
623 | Just prov' <- opt_trans_prov p1 p2
624 = ASSERT( r1 == r2 )
625 fireTransRule "UnivCo" in_co1 in_co2 $
626 mkUnivCo prov' r1 tyl1 tyr2
627 where
628 -- if the provenances are different, opt'ing will be very confusing
629 opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv = Just UnsafeCoerceProv
630 opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
631 = Just $ PhantomProv $ opt_trans is kco1 kco2
632 opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
633 = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
634 opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
635 opt_trans_prov _ _ = Nothing
636
637 -- Push transitivity down through matching top-level constructors.
638 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
639 | tc1 == tc2
640 = ASSERT( r1 == r2 )
641 fireTransRule "PushTyConApp" in_co1 in_co2 $
642 mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
643
644 opt_trans_rule is in_co1@(FunCo r1 co1a co1b) in_co2@(FunCo r2 co2a co2b)
645 = ASSERT( r1 == r2 ) -- Just like the TyConAppCo/TyConAppCo case
646 fireTransRule "PushFun" in_co1 in_co2 $
647 mkFunCo r1 (opt_trans is co1a co2a) (opt_trans is co1b co2b)
648
649 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
650 -- Must call opt_trans_rule_app; see Note [EtaAppCo]
651 = opt_trans_rule_app is in_co1 in_co2 co1a [co1b] co2a [co2b]
652
653 -- Eta rules
654 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
655 | Just cos2 <- etaTyConAppCo_maybe tc co2
656 = ASSERT( cos1 `equalLength` cos2 )
657 fireTransRule "EtaCompL" co1 co2 $
658 mkTyConAppCo r tc (opt_transList is cos1 cos2)
659
660 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
661 | Just cos1 <- etaTyConAppCo_maybe tc co1
662 = ASSERT( cos1 `equalLength` cos2 )
663 fireTransRule "EtaCompR" co1 co2 $
664 mkTyConAppCo r tc (opt_transList is cos1 cos2)
665
666 opt_trans_rule is co1@(AppCo co1a co1b) co2
667 | Just (co2a,co2b) <- etaAppCo_maybe co2
668 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
669
670 opt_trans_rule is co1 co2@(AppCo co2a co2b)
671 | Just (co1a,co1b) <- etaAppCo_maybe co1
672 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
673
674 -- Push transitivity inside forall
675 -- forall over types.
676 opt_trans_rule is co1 co2
677 | Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1
678 , Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2
679 = push_trans tv1 eta1 r1 tv2 eta2 r2
680
681 | Just (tv2, eta2, r2) <- splitForAllCo_ty_maybe co2
682 , Just (tv1, eta1, r1) <- etaForAllCo_ty_maybe co1
683 = push_trans tv1 eta1 r1 tv2 eta2 r2
684
685 where
686 push_trans tv1 eta1 r1 tv2 eta2 r2
687 -- Given:
688 -- co1 = /\ tv1 : eta1. r1
689 -- co2 = /\ tv2 : eta2. r2
690 -- Wanted:
691 -- /\tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1])
692 = fireTransRule "EtaAllTy_ty" co1 co2 $
693 mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
694 where
695 is' = is `extendInScopeSet` tv1
696 r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
697
698 -- Push transitivity inside forall
699 -- forall over coercions.
700 opt_trans_rule is co1 co2
701 | Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1
702 , Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2
703 = push_trans cv1 eta1 r1 cv2 eta2 r2
704
705 | Just (cv2, eta2, r2) <- splitForAllCo_co_maybe co2
706 , Just (cv1, eta1, r1) <- etaForAllCo_co_maybe co1
707 = push_trans cv1 eta1 r1 cv2 eta2 r2
708
709 where
710 push_trans cv1 eta1 r1 cv2 eta2 r2
711 -- Given:
712 -- co1 = /\ cv1 : eta1. r1
713 -- co2 = /\ cv2 : eta2. r2
714 -- Wanted:
715 -- n1 = nth 2 eta1
716 -- n2 = nth 3 eta1
717 -- nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
718 = fireTransRule "EtaAllTy_co" co1 co2 $
719 mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
720 where
721 is' = is `extendInScopeSet` cv1
722 role = coVarRole cv1
723 eta1' = downgradeRole role Nominal eta1
724 n1 = mkNthCo role 2 eta1'
725 n2 = mkNthCo role 3 eta1'
726 r2' = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo`
727 (mkCoVarCo cv1) `mkTransCo` n2])
728 r2
729
730 -- Push transitivity inside axioms
731 opt_trans_rule is co1 co2
732
733 -- See Note [Why call checkAxInstCo during optimisation]
734 -- TrPushSymAxR
735 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
736 , True <- sym
737 , Just cos2 <- matchAxiom sym con ind co2
738 , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
739 , Nothing <- checkAxInstCo newAxInst
740 = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
741
742 -- TrPushAxR
743 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
744 , False <- sym
745 , Just cos2 <- matchAxiom sym con ind co2
746 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
747 , Nothing <- checkAxInstCo newAxInst
748 = fireTransRule "TrPushAxR" co1 co2 newAxInst
749
750 -- TrPushSymAxL
751 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
752 , True <- sym
753 , Just cos1 <- matchAxiom (not sym) con ind co1
754 , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
755 , Nothing <- checkAxInstCo newAxInst
756 = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
757
758 -- TrPushAxL
759 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
760 , False <- sym
761 , Just cos1 <- matchAxiom (not sym) con ind co1
762 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
763 , Nothing <- checkAxInstCo newAxInst
764 = fireTransRule "TrPushAxL" co1 co2 newAxInst
765
766 -- TrPushAxSym/TrPushSymAx
767 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
768 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
769 , con1 == con2
770 , ind1 == ind2
771 , sym1 == not sym2
772 , let branch = coAxiomNthBranch con1 ind1
773 qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
774 lhs = coAxNthLHS con1 ind1
775 rhs = coAxBranchRHS branch
776 pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
777 , all (`elemVarSet` pivot_tvs) qtvs
778 = fireTransRule "TrPushAxSym" co1 co2 $
779 if sym2
780 -- TrPushAxSym
781 then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
782 -- TrPushSymAx
783 else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
784 where
785 co1_is_axiom_maybe = isAxiom_maybe co1
786 co2_is_axiom_maybe = isAxiom_maybe co2
787 role = coercionRole co1 -- should be the same as coercionRole co2!
788
789 opt_trans_rule _ co1 co2 -- Identity rule
790 | (Pair ty1 _, r) <- coercionKindRole co1
791 , Pair _ ty2 <- coercionKind co2
792 , ty1 `eqType` ty2
793 = fireTransRule "RedTypeDirRefl" co1 co2 $
794 mkReflCo r ty2
795
796 opt_trans_rule _ _ _ = Nothing
797
798 -- See Note [EtaAppCo]
799 opt_trans_rule_app :: InScopeSet
800 -> Coercion -- original left-hand coercion (printing only)
801 -> Coercion -- original right-hand coercion (printing only)
802 -> Coercion -- left-hand coercion "function"
803 -> [Coercion] -- left-hand coercion "args"
804 -> Coercion -- right-hand coercion "function"
805 -> [Coercion] -- right-hand coercion "args"
806 -> Maybe Coercion
807 opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
808 | AppCo co1aa co1ab <- co1a
809 , Just (co2aa, co2ab) <- etaAppCo_maybe co2a
810 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
811
812 | AppCo co2aa co2ab <- co2a
813 , Just (co1aa, co1ab) <- etaAppCo_maybe co1a
814 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
815
816 | otherwise
817 = ASSERT( co1bs `equalLength` co2bs )
818 fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
819 let Pair _ rt1a = coercionKind co1a
820 (Pair lt2a _, rt2a) = coercionKindRole co2a
821
822 Pair _ rt1bs = traverse coercionKind co1bs
823 Pair lt2bs _ = traverse coercionKind co2bs
824 rt2bs = map coercionRole co2bs
825
826 kcoa = mkKindCo $ buildCoercion lt2a rt1a
827 kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
828
829 co2a' = mkCoherenceLeftCo rt2a lt2a kcoa co2a
830 co2bs' = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs
831 co2bs'' = zipWith mkTransCo co2bs' co2bs
832 in
833 mkAppCos (opt_trans is co1a co2a')
834 (zipWith (opt_trans is) co1bs co2bs'')
835
836 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
837 fireTransRule _rule _co1 _co2 res
838 = Just res
839
840 {-
841 Note [Conflict checking with AxiomInstCo]
842 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
843 Consider the following type family and axiom:
844
845 type family Equal (a :: k) (b :: k) :: Bool
846 type instance where
847 Equal a a = True
848 Equal a b = False
849 --
850 Equal :: forall k::*. k -> k -> Bool
851 axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
852 ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
853
854 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
855 0-based, so this is the second branch of the axiom.) The problem is that, on
856 the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
857 False) and that all is OK. But, all is not OK: we want to use the first branch
858 of the axiom in this case, not the second. The problem is that the parameters
859 of the first branch can unify with the supplied coercions, thus meaning that
860 the first branch should be taken. See also Note [Apartness] in
861 types/FamInstEnv.hs.
862
863 Note [Why call checkAxInstCo during optimisation]
864 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
865 It is possible that otherwise-good-looking optimisations meet with disaster
866 in the presence of axioms with multiple equations. Consider
867
868 type family Equal (a :: *) (b :: *) :: Bool where
869 Equal a a = True
870 Equal a b = False
871 type family Id (a :: *) :: * where
872 Id a = a
873
874 axEq :: { [a::*]. Equal a a ~ True
875 ; [a::*, b::*]. Equal a b ~ False }
876 axId :: [a::*]. Id a ~ a
877
878 co1 = Equal (axId[0] Int) (axId[0] Bool)
879 :: Equal (Id Int) (Id Bool) ~ Equal Int Bool
880 co2 = axEq[1] <Int> <Bool>
881 :: Equal Int Bool ~ False
882
883 We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
884 co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
885 happens when we push the coercions inside? We get
886
887 co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
888 :: Equal (Id Int) (Id Bool) ~ False
889
890 which is bogus! This is because the type system isn't smart enough to know
891 that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
892 families. At the time of writing, I (Richard Eisenberg) couldn't think of
893 a way of detecting this any more efficient than just building the optimised
894 coercion and checking.
895
896 Note [EtaAppCo]
897 ~~~~~~~~~~~~~~~
898 Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
899 like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
900 the resultant coercions might not be well kinded. Here is an example (things
901 labeled with x don't matter in this example):
902
903 k1 :: Type
904 k2 :: Type
905
906 a :: k1 -> Type
907 b :: k1
908
909 h :: k1 ~ k2
910
911 co1a :: x1 ~ (a |> (h -> <Type>)
912 co1b :: x2 ~ (b |> h)
913
914 co2a :: a ~ x3
915 co2b :: b ~ x4
916
917 First, convince yourself of the following:
918
919 co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
920 co2a co2b :: a b ~ x3 x4
921
922 (a |> (h -> <Type>)) (b |> h) `eqType` a b
923
924 That last fact is due to Note [Non-trivial definitional equality] in TyCoRep,
925 where we ignore coercions in types as long as two types' kinds are the same.
926 In our case, we meet this last condition, because
927
928 (a |> (h -> <Type>)) (b |> h) :: Type
929 and
930 a b :: Type
931
932 So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
933 suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
934 kinds don't match up.
935
936 The solution here is to twiddle the kinds in the output coercions. First, we
937 need to find coercions
938
939 ak :: kind(a |> (h -> <Type>)) ~ kind(a)
940 bk :: kind(b |> h) ~ kind(b)
941
942 This can be done with mkKindCo and buildCoercion. The latter assumes two
943 types are identical modulo casts and builds a coercion between them.
944
945 Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
946 output coercions. These are well-kinded.
947
948 Also, note that all of this is done after accumulated any nested AppCo
949 parameters. This step is to avoid quadratic behavior in calling coercionKind.
950
951 The problem described here was first found in dependent/should_compile/dynamic-paper.
952
953 -}
954
955 -- | Check to make sure that an AxInstCo is internally consistent.
956 -- Returns the conflicting branch, if it exists
957 -- See Note [Conflict checking with AxiomInstCo]
958 checkAxInstCo :: Coercion -> Maybe CoAxBranch
959 -- defined here to avoid dependencies in Coercion
960 -- If you edit this function, you may need to update the GHC formalism
961 -- See Note [GHC Formalism] in CoreLint
962 checkAxInstCo (AxiomInstCo ax ind cos)
963 = let branch = coAxiomNthBranch ax ind
964 tvs = coAxBranchTyVars branch
965 cvs = coAxBranchCoVars branch
966 incomps = coAxBranchIncomps branch
967 (tys, cotys) = splitAtList tvs (map (pFst . coercionKind) cos)
968 co_args = map stripCoercionTy cotys
969 subst = zipTvSubst tvs tys `composeTCvSubst`
970 zipCvSubst cvs co_args
971 target = Type.substTys subst (coAxBranchLHS branch)
972 in_scope = mkInScopeSet $
973 unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
974 flattened_target = flattenTys in_scope target in
975 check_no_conflict flattened_target incomps
976 where
977 check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
978 check_no_conflict _ [] = Nothing
979 check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
980 -- See Note [Apartness] in FamInstEnv
981 | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
982 = check_no_conflict flat rest
983 | otherwise
984 = Just b
985 checkAxInstCo _ = Nothing
986
987
988 -----------
989 wrapSym :: SymFlag -> Coercion -> Coercion
990 wrapSym sym co | sym = mkSymCo co
991 | otherwise = co
992
993 -- | Conditionally set a role to be representational
994 wrapRole :: ReprFlag
995 -> Role -- ^ current role
996 -> Coercion -> Coercion
997 wrapRole False _ = id
998 wrapRole True current = downgradeRole Representational current
999
1000 -- | If we require a representational role, return that. Otherwise,
1001 -- return the "default" role provided.
1002 chooseRole :: ReprFlag
1003 -> Role -- ^ "default" role
1004 -> Role
1005 chooseRole True _ = Representational
1006 chooseRole _ r = r
1007
1008 -----------
1009 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
1010 isAxiom_maybe (SymCo co)
1011 | Just (sym, con, ind, cos) <- isAxiom_maybe co
1012 = Just (not sym, con, ind, cos)
1013 isAxiom_maybe (AxiomInstCo con ind cos)
1014 = Just (False, con, ind, cos)
1015 isAxiom_maybe _ = Nothing
1016
1017 matchAxiom :: Bool -- True = match LHS, False = match RHS
1018 -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
1019 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
1020 | CoAxBranch { cab_tvs = qtvs
1021 , cab_cvs = [] -- can't infer these, so fail if there are any
1022 , cab_roles = roles
1023 , cab_lhs = lhs
1024 , cab_rhs = rhs } <- coAxiomNthBranch ax ind
1025 , Just subst <- liftCoMatch (mkVarSet qtvs)
1026 (if sym then (mkTyConApp tc lhs) else rhs)
1027 co
1028 , all (`isMappedByLC` subst) qtvs
1029 = zipWithM (liftCoSubstTyVar subst) roles qtvs
1030
1031 | otherwise
1032 = Nothing
1033
1034 -------------
1035 compatible_co :: Coercion -> Coercion -> Bool
1036 -- Check whether (co1 . co2) will be well-kinded
1037 compatible_co co1 co2
1038 = x1 `eqType` x2
1039 where
1040 Pair _ x1 = coercionKind co1
1041 Pair x2 _ = coercionKind co2
1042
1043 -------------
1044 {-
1045 etaForAllCo
1046 ~~~~~~~~~~~~~~~~~
1047 (1) etaForAllCo_ty_maybe
1048 Suppose we have
1049
1050 g : all a1:k1.t1 ~ all a2:k2.t2
1051
1052 but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
1053
1054 g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))
1055
1056 Call the kind coercion h1 and the body coercion h2. We can see that
1057
1058 h2 : t1 ~ t2[a2 |-> (a1 |> h1)]
1059
1060 According to the typing rule for ForAllCo, we get that
1061
1062 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])
1063
1064 or
1065
1066 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> a1])
1067
1068 as desired.
1069
1070 (2) etaForAllCo_co_maybe
1071 Suppose we have
1072
1073 g : all c1:(s1~s2). t1 ~ all c2:(s3~s4). t2
1074
1075 Similarly, we do this
1076
1077 g' = all c1:h1. h2
1078 : all c1:(s1~s2). t1 ~ all c1:(s3~s4). t2[c2 |-> (sym eta1;c1;eta2)]
1079 [c1 |-> eta1;c1;sym eta2]
1080
1081 Here,
1082
1083 h1 = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4)
1084 eta1 = mkNthCo r 2 h1 :: (s1 ~ s3)
1085 eta2 = mkNthCo r 3 h1 :: (s2 ~ s4)
1086 h2 = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
1087 -}
1088 etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
1089 -- Try to make the coercion be of form (forall tv:kind_co. co)
1090 etaForAllCo_ty_maybe co
1091 | Just (tv, kind_co, r) <- splitForAllCo_ty_maybe co
1092 = Just (tv, kind_co, r)
1093
1094 | Pair ty1 ty2 <- coercionKind co
1095 , Just (tv1, _) <- splitForAllTy_ty_maybe ty1
1096 , isForAllTy_ty ty2
1097 , let kind_co = mkNthCo Nominal 0 co
1098 = Just ( tv1, kind_co
1099 , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
1100
1101 | otherwise
1102 = Nothing
1103
1104 etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
1105 -- Try to make the coercion be of form (forall cv:kind_co. co)
1106 etaForAllCo_co_maybe co
1107 | Just (cv, kind_co, r) <- splitForAllCo_co_maybe co
1108 = Just (cv, kind_co, r)
1109
1110 | Pair ty1 ty2 <- coercionKind co
1111 , Just (cv1, _) <- splitForAllTy_co_maybe ty1
1112 , isForAllTy_co ty2
1113 = let kind_co = mkNthCo Nominal 0 co
1114 r = coVarRole cv1
1115 l_co = mkCoVarCo cv1
1116 kind_co' = downgradeRole r Nominal kind_co
1117 r_co = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo`
1118 l_co `mkTransCo`
1119 (mkNthCo r 3 kind_co')
1120 in Just ( cv1, kind_co
1121 , mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
1122
1123 | otherwise
1124 = Nothing
1125
1126 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
1127 -- If possible, split a coercion
1128 -- g :: t1a t1b ~ t2a t2b
1129 -- into a pair of coercions (left g, right g)
1130 etaAppCo_maybe co
1131 | Just (co1,co2) <- splitAppCo_maybe co
1132 = Just (co1,co2)
1133 | (Pair ty1 ty2, Nominal) <- coercionKindRole co
1134 , Just (_,t1) <- splitAppTy_maybe ty1
1135 , Just (_,t2) <- splitAppTy_maybe ty2
1136 , let isco1 = isCoercionTy t1
1137 , let isco2 = isCoercionTy t2
1138 , isco1 == isco2
1139 = Just (LRCo CLeft co, LRCo CRight co)
1140 | otherwise
1141 = Nothing
1142
1143 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
1144 -- If possible, split a coercion
1145 -- g :: T s1 .. sn ~ T t1 .. tn
1146 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
1147 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
1148 = ASSERT( tc == tc2 ) Just cos2
1149
1150 etaTyConAppCo_maybe tc co
1151 | mightBeUnsaturatedTyCon tc
1152 , (Pair ty1 ty2, r) <- coercionKindRole co
1153 , Just (tc1, tys1) <- splitTyConApp_maybe ty1
1154 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
1155 , tc1 == tc2
1156 , isInjectiveTyCon tc r -- See Note [NthCo and newtypes] in TyCoRep
1157 , let n = length tys1
1158 , tys2 `lengthIs` n -- This can fail in an erroneous progam
1159 -- E.g. T a ~# T a b
1160 -- Trac #14607
1161 = ASSERT( tc == tc1 )
1162 Just (decomposeCo n co (tyConRolesX r tc1))
1163 -- NB: n might be <> tyConArity tc
1164 -- e.g. data family T a :: * -> *
1165 -- g :: T a b ~ T c d
1166
1167 | otherwise
1168 = Nothing
1169
1170 {-
1171 Note [Eta for AppCo]
1172 ~~~~~~~~~~~~~~~~~~~~
1173 Suppose we have
1174 g :: s1 t1 ~ s2 t2
1175
1176 Then we can't necessarily make
1177 left g :: s1 ~ s2
1178 right g :: t1 ~ t2
1179 because it's possible that
1180 s1 :: * -> * t1 :: *
1181 s2 :: (*->*) -> * t2 :: * -> *
1182 and in that case (left g) does not have the same
1183 kind on either side.
1184
1185 It's enough to check that
1186 kind t1 = kind t2
1187 because if g is well-kinded then
1188 kind (s1 t2) = kind (s2 t2)
1189 and these two imply
1190 kind s1 = kind s2
1191
1192 -}
1193
1194 optForAllCoBndr :: LiftingContext -> Bool
1195 -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
1196 optForAllCoBndr env sym
1197 = substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env