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