1-- (c) The University of Glasgow 2006 2 3{-# LANGUAGE CPP #-} 4 5module GHC.Core.Coercion.Opt ( optCoercion, checkAxInstCo ) where 6 7#include "GhclibHsVersions.h" 8 9import GHC.Prelude 10 11import GHC.Driver.Session 12import GHC.Core.TyCo.Rep 13import GHC.Core.TyCo.Subst 14import GHC.Core.Coercion 15import GHC.Core.Type as Type hiding( substTyVarBndr, substTy ) 16import GHC.Tc.Utils.TcType ( exactTyCoVarsOfType ) 17import GHC.Core.TyCon 18import GHC.Core.Coercion.Axiom 19import GHC.Types.Var.Set 20import GHC.Types.Var.Env 21import GHC.Utils.Outputable 22import GHC.Core.FamInstEnv ( flattenTys ) 23import GHC.Data.Pair 24import GHC.Data.List.SetOps ( getNth ) 25import GHC.Utils.Misc 26import GHC.Core.Unify 27import GHC.Core.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 GHC.Core.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 cow co1 co2) 255 = ASSERT( r == _r ) 256 if rep 257 then mkFunCo Representational cow' co1' co2' 258 else mkFunCo r cow' 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 cow' = opt_co1 env sym cow 263 264opt_co4 env sym rep r (CoVarCo cv) 265 | Just co <- lookupCoVar (lcTCvSubst env) cv 266 = opt_co4_wrap (zapLiftingContext env) sym rep r co 267 268 | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl] 269 = mkReflCo (chooseRole rep r) ty1 270 271 | otherwise 272 = ASSERT( isCoVar cv1 ) 273 wrapRole rep r $ wrapSym sym $ 274 CoVarCo cv1 275 276 where 277 Pair ty1 ty2 = coVarTypes cv1 278 279 cv1 = case lookupInScope (lcInScopeSet env) cv of 280 Just cv1 -> cv1 281 Nothing -> WARN( True, text "opt_co: not in scope:" 282 <+> ppr cv $$ ppr env) 283 cv 284 -- cv1 might have a substituted kind! 285 286opt_co4 _ _ _ _ (HoleCo h) 287 = pprPanic "opt_univ fell into a hole" (ppr h) 288 289opt_co4 env sym rep r (AxiomInstCo con ind cos) 290 -- Do *not* push sym inside top-level axioms 291 -- e.g. if g is a top-level axiom 292 -- g a : f a ~ a 293 -- then (sym (g ty)) /= g (sym ty) !! 294 = ASSERT( r == coAxiomRole con ) 295 wrapRole rep (coAxiomRole con) $ 296 wrapSym sym $ 297 -- some sub-cos might be P: use opt_co2 298 -- See Note [Optimising coercion optimisation] 299 AxiomInstCo con ind (zipWith (opt_co2 env False) 300 (coAxBranchRoles (coAxiomNthBranch con ind)) 301 cos) 302 -- Note that the_co does *not* have sym pushed into it 303 304opt_co4 env sym rep r (UnivCo prov _r t1 t2) 305 = ASSERT( r == _r ) 306 opt_univ env sym prov (chooseRole rep r) t1 t2 307 308opt_co4 env sym rep r (TransCo co1 co2) 309 -- sym (g `o` h) = sym h `o` sym g 310 | sym = opt_trans in_scope co2' co1' 311 | otherwise = opt_trans in_scope co1' co2' 312 where 313 co1' = opt_co4_wrap env sym rep r co1 314 co2' = opt_co4_wrap env sym rep r co2 315 in_scope = lcInScopeSet env 316 317opt_co4 env _sym rep r (NthCo _r n co) 318 | Just (ty, _) <- isReflCo_maybe co 319 , Just (_tc, args) <- ASSERT( r == _r ) 320 splitTyConApp_maybe ty 321 = liftCoSubst (chooseRole rep r) env (args `getNth` n) 322 | Just (ty, _) <- isReflCo_maybe co 323 , n == 0 324 , Just (tv, _) <- splitForAllTy_maybe ty 325 -- works for both tyvar and covar 326 = liftCoSubst (chooseRole rep r) env (varType tv) 327 328opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos)) 329 = ASSERT( r == r1 ) 330 opt_co4_wrap env sym rep r (cos `getNth` n) 331 332opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _)) 333 -- works for both tyvar and covar 334 = ASSERT( r == _r ) 335 ASSERT( n == 0 ) 336 opt_co4_wrap env sym rep Nominal eta 337 338opt_co4 env sym rep r (NthCo _r n co) 339 | TyConAppCo _ _ cos <- co' 340 , let nth_co = cos `getNth` n 341 = if rep && (r == Nominal) 342 -- keep propagating the SubCo 343 then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co 344 else nth_co 345 346 | ForAllCo _ eta _ <- co' 347 = if rep 348 then opt_co4_wrap (zapLiftingContext env) False True Nominal eta 349 else eta 350 351 | otherwise 352 = wrapRole rep r $ NthCo r n co' 353 where 354 co' = opt_co1 env sym co 355 356opt_co4 env sym rep r (LRCo lr co) 357 | Just pr_co <- splitAppCo_maybe co 358 = ASSERT( r == Nominal ) 359 opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co) 360 | Just pr_co <- splitAppCo_maybe co' 361 = ASSERT( r == Nominal ) 362 if rep 363 then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co) 364 else pick_lr lr pr_co 365 | otherwise 366 = wrapRole rep Nominal $ LRCo lr co' 367 where 368 co' = opt_co4_wrap env sym False Nominal co 369 370 pick_lr CLeft (l, _) = l 371 pick_lr CRight (_, r) = r 372 373-- See Note [Optimising InstCo] 374opt_co4 env sym rep r (InstCo co1 arg) 375 -- forall over type... 376 | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1 377 = opt_co4_wrap (extendLiftingContext env tv 378 (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg)) 379 -- mkSymCo kind_co :: k1 ~ k2 380 -- sym_arg :: (t1 :: k1) ~ (t2 :: k2) 381 -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1) 382 sym rep r co_body 383 384 -- forall over coercion... 385 | Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1 386 , CoercionTy h1 <- t1 387 , CoercionTy h2 <- t2 388 = let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2 389 in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body 390 391 -- See if it is a forall after optimization 392 -- If so, do an inefficient one-variable substitution, then re-optimize 393 394 -- forall over type... 395 | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1' 396 = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv' 397 (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg')) 398 False False r' co_body' 399 400 -- forall over coercion... 401 | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1' 402 , CoercionTy h1' <- t1' 403 , CoercionTy h2' <- t2' 404 = let new_co = mk_new_co cv' kind_co' h1' h2' 405 in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co) 406 False False r' co_body' 407 408 | otherwise = InstCo co1' arg' 409 where 410 co1' = opt_co4_wrap env sym rep r co1 411 r' = chooseRole rep r 412 arg' = opt_co4_wrap env sym False Nominal arg 413 sym_arg = wrapSym sym arg' 414 415 -- Performance note: don't be alarmed by the two calls to coercionKind 416 -- here, as only one call to coercionKind is actually demanded per guard. 417 -- t1/t2 are used when checking if co1 is a forall, and t1'/t2' are used 418 -- when checking if co1' (i.e., co1 post-optimization) is a forall. 419 -- 420 -- t1/t2 must come from sym_arg, not arg', since it's possible that arg' 421 -- might have an extra Sym at the front (after being optimized) that co1 422 -- lacks, so we need to use sym_arg to balance the number of Syms. (#15725) 423 Pair t1 t2 = coercionKind sym_arg 424 Pair t1' t2' = coercionKind arg' 425 426 mk_new_co cv kind_co h1 h2 427 = let -- h1 :: (t1 ~ t2) 428 -- h2 :: (t3 ~ t4) 429 -- kind_co :: (t1 ~ t2) ~ (t3 ~ t4) 430 -- n1 :: t1 ~ t3 431 -- n2 :: t2 ~ t4 432 -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2) 433 r2 = coVarRole cv 434 kind_co' = downgradeRole r2 Nominal kind_co 435 n1 = mkNthCo r2 2 kind_co' 436 n2 = mkNthCo r2 3 kind_co' 437 in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1 438 (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2)) 439 440opt_co4 env sym _rep r (KindCo co) 441 = ASSERT( r == Nominal ) 442 let kco' = promoteCoercion co in 443 case kco' of 444 KindCo co' -> promoteCoercion (opt_co1 env sym co') 445 _ -> opt_co4_wrap env sym False Nominal kco' 446 -- This might be able to be optimized more to do the promotion 447 -- and substitution/optimization at the same time 448 449opt_co4 env sym _ r (SubCo co) 450 = ASSERT( r == Representational ) 451 opt_co4_wrap env sym True Nominal co 452 453-- This could perhaps be optimized more. 454opt_co4 env sym rep r (AxiomRuleCo co cs) 455 = ASSERT( r == coaxrRole co ) 456 wrapRole rep r $ 457 wrapSym sym $ 458 AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs) 459 460{- Note [Optimise CoVarCo to Refl] 461~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 462If we have (c :: t~t) we can optimise it to Refl. That increases the 463chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t) 464 465We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo] 466in GHC.Core.Coercion. 467-} 468 469------------- 470-- | Optimize a phantom coercion. The input coercion may not necessarily 471-- be a phantom, but the output sure will be. 472opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo 473opt_phantom env sym co 474 = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2 475 where 476 Pair ty1 ty2 = coercionKind co 477 478{- Note [Differing kinds] 479 ~~~~~~~~~~~~~~~~~~~~~~ 480The two types may not have the same kind (although that would be very unusual). 481But even if they have the same kind, and the same type constructor, the number 482of arguments in a `CoTyConApp` can differ. Consider 483 484 Any :: forall k. k 485 486 Any * Int :: * 487 Any (*->*) Maybe Int :: * 488 489Hence the need to compare argument lengths; see #13658 490 -} 491 492opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role 493 -> Type -> Type -> Coercion 494opt_univ env sym (PhantomProv h) _r ty1 ty2 495 | sym = mkPhantomCo h' ty2' ty1' 496 | otherwise = mkPhantomCo h' ty1' ty2' 497 where 498 h' = opt_co4 env sym False Nominal h 499 ty1' = substTy (lcSubstLeft env) ty1 500 ty2' = substTy (lcSubstRight env) ty2 501 502opt_univ env sym prov role oty1 oty2 503 | Just (tc1, tys1) <- splitTyConApp_maybe oty1 504 , Just (tc2, tys2) <- splitTyConApp_maybe oty2 505 , tc1 == tc2 506 , equalLength tys1 tys2 -- see Note [Differing kinds] 507 -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom); 508 -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps 509 = let roles = tyConRolesX role tc1 510 arg_cos = zipWith3 (mkUnivCo prov') roles tys1 tys2 511 arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos 512 in 513 mkTyConAppCo role tc1 arg_cos' 514 515 -- can't optimize the AppTy case because we can't build the kind coercions. 516 517 | Just (tv1, ty1) <- splitForAllTy_ty_maybe oty1 518 , Just (tv2, ty2) <- splitForAllTy_ty_maybe oty2 519 -- NB: prov isn't interesting here either 520 = let k1 = tyVarKind tv1 521 k2 = tyVarKind tv2 522 eta = mkUnivCo prov' Nominal k1 k2 523 -- eta gets opt'ed soon, but not yet. 524 ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2 525 526 (env', tv1', eta') = optForAllCoBndr env sym tv1 eta 527 in 528 mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2') 529 530 | Just (cv1, ty1) <- splitForAllTy_co_maybe oty1 531 , Just (cv2, ty2) <- splitForAllTy_co_maybe oty2 532 -- NB: prov isn't interesting here either 533 = let k1 = varType cv1 534 k2 = varType cv2 535 r' = coVarRole cv1 536 eta = mkUnivCo prov' Nominal k1 k2 537 eta_d = downgradeRole r' Nominal eta 538 -- eta gets opt'ed soon, but not yet. 539 n_co = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo` 540 (mkCoVarCo cv1) `mkTransCo` 541 (mkNthCo r' 3 eta_d) 542 ty2' = substTyWithCoVars [cv2] [n_co] ty2 543 544 (env', cv1', eta') = optForAllCoBndr env sym cv1 eta 545 in 546 mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2') 547 548 | otherwise 549 = let ty1 = substTyUnchecked (lcSubstLeft env) oty1 550 ty2 = substTyUnchecked (lcSubstRight env) oty2 551 (a, b) | sym = (ty2, ty1) 552 | otherwise = (ty1, ty2) 553 in 554 mkUnivCo prov' role a b 555 556 where 557 prov' = case prov of 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 :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo] 564opt_transList is = zipWithEqual "opt_transList" (opt_trans is) 565 -- The input lists must have identical length. 566 567opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo 568opt_trans is co1 co2 569 | isReflCo co1 = co2 570 -- optimize when co1 is a Refl Co 571 | otherwise = opt_trans1 is co1 co2 572 573opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo 574-- First arg is not the identity 575opt_trans1 is co1 co2 576 | isReflCo co2 = co1 577 -- optimize when co2 is a Refl Co 578 | otherwise = opt_trans2 is co1 co2 579 580opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo 581-- Neither arg is the identity 582opt_trans2 is (TransCo co1a co1b) co2 583 -- Don't know whether the sub-coercions are the identity 584 = opt_trans is co1a (opt_trans is co1b co2) 585 586opt_trans2 is co1 co2 587 | Just co <- opt_trans_rule is co1 co2 588 = co 589 590opt_trans2 is co1 (TransCo co2a co2b) 591 | Just co1_2a <- opt_trans_rule is co1 co2a 592 = if isReflCo co1_2a 593 then co2b 594 else opt_trans1 is co1_2a co2b 595 596opt_trans2 _ co1 co2 597 = mkTransCo co1 co2 598 599------ 600-- Optimize coercions with a top-level use of transitivity. 601opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo 602 603opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2)) 604 = ASSERT( r1 == r2 ) 605 fireTransRule "GRefl" in_co1 in_co2 $ 606 mkGReflRightCo r1 t1 (opt_trans is co1 co2) 607 608-- Push transitivity through matching destructors 609opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2) 610 | d1 == d2 611 , coercionRole co1 == coercionRole co2 612 , co1 `compatible_co` co2 613 = ASSERT( r1 == r2 ) 614 fireTransRule "PushNth" in_co1 in_co2 $ 615 mkNthCo r1 d1 (opt_trans is co1 co2) 616 617opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2) 618 | d1 == d2 619 , co1 `compatible_co` co2 620 = fireTransRule "PushLR" in_co1 in_co2 $ 621 mkLRCo d1 (opt_trans is co1 co2) 622 623-- Push transitivity inside instantiation 624opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2) 625 | ty1 `eqCoercion` ty2 626 , co1 `compatible_co` co2 627 = fireTransRule "TrPushInst" in_co1 in_co2 $ 628 mkInstCo (opt_trans is co1 co2) ty1 629 630opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1) 631 in_co2@(UnivCo p2 r2 _tyl2 tyr2) 632 | Just prov' <- opt_trans_prov p1 p2 633 = ASSERT( r1 == r2 ) 634 fireTransRule "UnivCo" in_co1 in_co2 $ 635 mkUnivCo prov' r1 tyl1 tyr2 636 where 637 -- if the provenances are different, opt'ing will be very confusing 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 w1 co1a co1b) in_co2@(FunCo r2 w2 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 w1 w2) (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 = fireTransRule "EtaCompL" co1 co2 $ 665 mkTyConAppCo r tc (opt_transList is cos1 cos2) 666 667opt_trans_rule is co1 co2@(TyConAppCo r tc cos2) 668 | Just cos1 <- etaTyConAppCo_maybe tc co1 669 = fireTransRule "EtaCompR" co1 co2 $ 670 mkTyConAppCo r tc (opt_transList is cos1 cos2) 671 672opt_trans_rule is co1@(AppCo co1a co1b) co2 673 | Just (co2a,co2b) <- etaAppCo_maybe co2 674 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b] 675 676opt_trans_rule is co1 co2@(AppCo co2a co2b) 677 | Just (co1a,co1b) <- etaAppCo_maybe co1 678 = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b] 679 680-- Push transitivity inside forall 681-- forall over types. 682opt_trans_rule is co1 co2 683 | Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1 684 , Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2 685 = push_trans tv1 eta1 r1 tv2 eta2 r2 686 687 | Just (tv2, eta2, r2) <- splitForAllCo_ty_maybe co2 688 , Just (tv1, eta1, r1) <- etaForAllCo_ty_maybe co1 689 = push_trans tv1 eta1 r1 tv2 eta2 r2 690 691 where 692 push_trans tv1 eta1 r1 tv2 eta2 r2 693 -- Given: 694 -- co1 = /\ tv1 : eta1. r1 695 -- co2 = /\ tv2 : eta2. r2 696 -- Wanted: 697 -- /\tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1]) 698 = fireTransRule "EtaAllTy_ty" co1 co2 $ 699 mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2') 700 where 701 is' = is `extendInScopeSet` tv1 702 r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2 703 704-- Push transitivity inside forall 705-- forall over coercions. 706opt_trans_rule is co1 co2 707 | Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1 708 , Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2 709 = push_trans cv1 eta1 r1 cv2 eta2 r2 710 711 | Just (cv2, eta2, r2) <- splitForAllCo_co_maybe co2 712 , Just (cv1, eta1, r1) <- etaForAllCo_co_maybe co1 713 = push_trans cv1 eta1 r1 cv2 eta2 r2 714 715 where 716 push_trans cv1 eta1 r1 cv2 eta2 r2 717 -- Given: 718 -- co1 = /\ cv1 : eta1. r1 719 -- co2 = /\ cv2 : eta2. r2 720 -- Wanted: 721 -- n1 = nth 2 eta1 722 -- n2 = nth 3 eta1 723 -- nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2]) 724 = fireTransRule "EtaAllTy_co" co1 co2 $ 725 mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2') 726 where 727 is' = is `extendInScopeSet` cv1 728 role = coVarRole cv1 729 eta1' = downgradeRole role Nominal eta1 730 n1 = mkNthCo role 2 eta1' 731 n2 = mkNthCo role 3 eta1' 732 r2' = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo` 733 (mkCoVarCo cv1) `mkTransCo` n2]) 734 r2 735 736-- Push transitivity inside axioms 737opt_trans_rule is co1 co2 738 739 -- See Note [Why call checkAxInstCo during optimisation] 740 -- TrPushSymAxR 741 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe 742 , True <- sym 743 , Just cos2 <- matchAxiom sym con ind co2 744 , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1) 745 , Nothing <- checkAxInstCo newAxInst 746 = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst 747 748 -- TrPushAxR 749 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe 750 , False <- sym 751 , Just cos2 <- matchAxiom sym con ind co2 752 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2) 753 , Nothing <- checkAxInstCo newAxInst 754 = fireTransRule "TrPushAxR" co1 co2 newAxInst 755 756 -- TrPushSymAxL 757 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe 758 , True <- sym 759 , Just cos1 <- matchAxiom (not sym) con ind co1 760 , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1)) 761 , Nothing <- checkAxInstCo newAxInst 762 = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst 763 764 -- TrPushAxL 765 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe 766 , False <- sym 767 , Just cos1 <- matchAxiom (not sym) con ind co1 768 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2) 769 , Nothing <- checkAxInstCo newAxInst 770 = fireTransRule "TrPushAxL" co1 co2 newAxInst 771 772 -- TrPushAxSym/TrPushSymAx 773 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe 774 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe 775 , con1 == con2 776 , ind1 == ind2 777 , sym1 == not sym2 778 , let branch = coAxiomNthBranch con1 ind1 779 qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch 780 lhs = coAxNthLHS con1 ind1 781 rhs = coAxBranchRHS branch 782 pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs) 783 , all (`elemVarSet` pivot_tvs) qtvs 784 = fireTransRule "TrPushAxSym" co1 co2 $ 785 if sym2 786 -- TrPushAxSym 787 then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs 788 -- TrPushSymAx 789 else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs 790 where 791 co1_is_axiom_maybe = isAxiom_maybe co1 792 co2_is_axiom_maybe = isAxiom_maybe co2 793 role = coercionRole co1 -- should be the same as coercionRole co2! 794 795opt_trans_rule _ co1 co2 -- Identity rule 796 | let ty1 = coercionLKind co1 797 r = coercionRole co1 798 ty2 = coercionRKind co2 799 , ty1 `eqType` ty2 800 = fireTransRule "RedTypeDirRefl" co1 co2 $ 801 mkReflCo r ty2 802 803opt_trans_rule _ _ _ = Nothing 804 805-- See Note [EtaAppCo] 806opt_trans_rule_app :: InScopeSet 807 -> Coercion -- original left-hand coercion (printing only) 808 -> Coercion -- original right-hand coercion (printing only) 809 -> Coercion -- left-hand coercion "function" 810 -> [Coercion] -- left-hand coercion "args" 811 -> Coercion -- right-hand coercion "function" 812 -> [Coercion] -- right-hand coercion "args" 813 -> Maybe Coercion 814opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs 815 | AppCo co1aa co1ab <- co1a 816 , Just (co2aa, co2ab) <- etaAppCo_maybe co2a 817 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs) 818 819 | AppCo co2aa co2ab <- co2a 820 , Just (co1aa, co1ab) <- etaAppCo_maybe co1a 821 = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs) 822 823 | otherwise 824 = ASSERT( co1bs `equalLength` co2bs ) 825 fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $ 826 let rt1a = coercionRKind co1a 827 828 lt2a = coercionLKind co2a 829 rt2a = coercionRole co2a 830 831 rt1bs = map coercionRKind co1bs 832 lt2bs = map coercionLKind co2bs 833 rt2bs = map coercionRole co2bs 834 835 kcoa = mkKindCo $ buildCoercion lt2a rt1a 836 kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs 837 838 co2a' = mkCoherenceLeftCo rt2a lt2a kcoa co2a 839 co2bs' = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs 840 co2bs'' = zipWith mkTransCo co2bs' co2bs 841 in 842 mkAppCos (opt_trans is co1a co2a') 843 (zipWith (opt_trans is) co1bs co2bs'') 844 845fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion 846fireTransRule _rule _co1 _co2 res 847 = Just res 848 849{- 850Note [Conflict checking with AxiomInstCo] 851~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 852Consider the following type family and axiom: 853 854type family Equal (a :: k) (b :: k) :: Bool 855type instance where 856 Equal a a = True 857 Equal a b = False 858-- 859Equal :: forall k::*. k -> k -> Bool 860axEqual :: { forall k::*. forall a::k. Equal k a a ~ True 861 ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False } 862 863We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is 8640-based, so this is the second branch of the axiom.) The problem is that, on 865the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ 866False) and that all is OK. But, all is not OK: we want to use the first branch 867of the axiom in this case, not the second. The problem is that the parameters 868of the first branch can unify with the supplied coercions, thus meaning that 869the first branch should be taken. See also Note [Apartness] in 870"GHC.Core.FamInstEnv". 871 872Note [Why call checkAxInstCo during optimisation] 873~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 874It is possible that otherwise-good-looking optimisations meet with disaster 875in the presence of axioms with multiple equations. Consider 876 877type family Equal (a :: *) (b :: *) :: Bool where 878 Equal a a = True 879 Equal a b = False 880type family Id (a :: *) :: * where 881 Id a = a 882 883axEq :: { [a::*]. Equal a a ~ True 884 ; [a::*, b::*]. Equal a b ~ False } 885axId :: [a::*]. Id a ~ a 886 887co1 = Equal (axId[0] Int) (axId[0] Bool) 888 :: Equal (Id Int) (Id Bool) ~ Equal Int Bool 889co2 = axEq[1] <Int> <Bool> 890 :: Equal Int Bool ~ False 891 892We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that 893co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what 894happens when we push the coercions inside? We get 895 896co3 = axEq[1] (axId[0] Int) (axId[0] Bool) 897 :: Equal (Id Int) (Id Bool) ~ False 898 899which is bogus! This is because the type system isn't smart enough to know 900that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type 901families. At the time of writing, I (Richard Eisenberg) couldn't think of 902a way of detecting this any more efficient than just building the optimised 903coercion and checking. 904 905Note [EtaAppCo] 906~~~~~~~~~~~~~~~ 907Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd 908like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that 909the resultant coercions might not be well kinded. Here is an example (things 910labeled with x don't matter in this example): 911 912 k1 :: Type 913 k2 :: Type 914 915 a :: k1 -> Type 916 b :: k1 917 918 h :: k1 ~ k2 919 920 co1a :: x1 ~ (a |> (h -> <Type>) 921 co1b :: x2 ~ (b |> h) 922 923 co2a :: a ~ x3 924 co2b :: b ~ x4 925 926First, convince yourself of the following: 927 928 co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h) 929 co2a co2b :: a b ~ x3 x4 930 931 (a |> (h -> <Type>)) (b |> h) `eqType` a b 932 933That last fact is due to Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep, 934where we ignore coercions in types as long as two types' kinds are the same. 935In our case, we meet this last condition, because 936 937 (a |> (h -> <Type>)) (b |> h) :: Type 938 and 939 a b :: Type 940 941So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the 942suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the 943kinds don't match up. 944 945The solution here is to twiddle the kinds in the output coercions. First, we 946need to find coercions 947 948 ak :: kind(a |> (h -> <Type>)) ~ kind(a) 949 bk :: kind(b |> h) ~ kind(b) 950 951This can be done with mkKindCo and buildCoercion. The latter assumes two 952types are identical modulo casts and builds a coercion between them. 953 954Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the 955output coercions. These are well-kinded. 956 957Also, note that all of this is done after accumulated any nested AppCo 958parameters. This step is to avoid quadratic behavior in calling coercionKind. 959 960The problem described here was first found in dependent/should_compile/dynamic-paper. 961 962-} 963 964-- | Check to make sure that an AxInstCo is internally consistent. 965-- Returns the conflicting branch, if it exists 966-- See Note [Conflict checking with AxiomInstCo] 967checkAxInstCo :: Coercion -> Maybe CoAxBranch 968-- defined here to avoid dependencies in GHC.Core.Coercion 969-- If you edit this function, you may need to update the GHC formalism 970-- See Note [GHC Formalism] in GHC.Core.Lint 971checkAxInstCo (AxiomInstCo ax ind cos) 972 = let branch = coAxiomNthBranch ax ind 973 tvs = coAxBranchTyVars branch 974 cvs = coAxBranchCoVars branch 975 incomps = coAxBranchIncomps branch 976 (tys, cotys) = splitAtList tvs (map coercionLKind cos) 977 co_args = map stripCoercionTy cotys 978 subst = zipTvSubst tvs tys `composeTCvSubst` 979 zipCvSubst cvs co_args 980 target = Type.substTys subst (coAxBranchLHS branch) 981 in_scope = mkInScopeSet $ 982 unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps) 983 flattened_target = flattenTys in_scope target in 984 check_no_conflict flattened_target incomps 985 where 986 check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch 987 check_no_conflict _ [] = Nothing 988 check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest) 989 -- See Note [Apartness] in GHC.Core.FamInstEnv 990 | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp 991 = check_no_conflict flat rest 992 | otherwise 993 = Just b 994checkAxInstCo _ = Nothing 995 996 997----------- 998wrapSym :: SymFlag -> Coercion -> Coercion 999wrapSym sym co | sym = mkSymCo co 1000 | otherwise = co 1001 1002-- | Conditionally set a role to be representational 1003wrapRole :: ReprFlag 1004 -> Role -- ^ current role 1005 -> Coercion -> Coercion 1006wrapRole False _ = id 1007wrapRole True current = downgradeRole Representational current 1008 1009-- | If we require a representational role, return that. Otherwise, 1010-- return the "default" role provided. 1011chooseRole :: ReprFlag 1012 -> Role -- ^ "default" role 1013 -> Role 1014chooseRole True _ = Representational 1015chooseRole _ r = r 1016 1017----------- 1018isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion]) 1019isAxiom_maybe (SymCo co) 1020 | Just (sym, con, ind, cos) <- isAxiom_maybe co 1021 = Just (not sym, con, ind, cos) 1022isAxiom_maybe (AxiomInstCo con ind cos) 1023 = Just (False, con, ind, cos) 1024isAxiom_maybe _ = Nothing 1025 1026matchAxiom :: Bool -- True = match LHS, False = match RHS 1027 -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion] 1028matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co 1029 | CoAxBranch { cab_tvs = qtvs 1030 , cab_cvs = [] -- can't infer these, so fail if there are any 1031 , cab_roles = roles 1032 , cab_lhs = lhs 1033 , cab_rhs = rhs } <- coAxiomNthBranch ax ind 1034 , Just subst <- liftCoMatch (mkVarSet qtvs) 1035 (if sym then (mkTyConApp tc lhs) else rhs) 1036 co 1037 , all (`isMappedByLC` subst) qtvs 1038 = zipWithM (liftCoSubstTyVar subst) roles qtvs 1039 1040 | otherwise 1041 = Nothing 1042 1043------------- 1044compatible_co :: Coercion -> Coercion -> Bool 1045-- Check whether (co1 . co2) will be well-kinded 1046compatible_co co1 co2 1047 = x1 `eqType` x2 1048 where 1049 x1 = coercionRKind co1 1050 x2 = coercionLKind co2 1051 1052------------- 1053{- 1054etaForAllCo 1055~~~~~~~~~~~~~~~~~ 1056(1) etaForAllCo_ty_maybe 1057Suppose we have 1058 1059 g : all a1:k1.t1 ~ all a2:k2.t2 1060 1061but g is *not* a ForAllCo. We want to eta-expand it. So, we do this: 1062 1063 g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g)) 1064 1065Call the kind coercion h1 and the body coercion h2. We can see that 1066 1067 h2 : t1 ~ t2[a2 |-> (a1 |> h1)] 1068 1069According to the typing rule for ForAllCo, we get that 1070 1071 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1]) 1072 1073or 1074 1075 g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> a1]) 1076 1077as desired. 1078 1079(2) etaForAllCo_co_maybe 1080Suppose we have 1081 1082 g : all c1:(s1~s2). t1 ~ all c2:(s3~s4). t2 1083 1084Similarly, we do this 1085 1086 g' = all c1:h1. h2 1087 : all c1:(s1~s2). t1 ~ all c1:(s3~s4). t2[c2 |-> (sym eta1;c1;eta2)] 1088 [c1 |-> eta1;c1;sym eta2] 1089 1090Here, 1091 1092 h1 = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4) 1093 eta1 = mkNthCo r 2 h1 :: (s1 ~ s3) 1094 eta2 = mkNthCo r 3 h1 :: (s2 ~ s4) 1095 h2 = mkInstCo g (cv1 ~ (sym eta1;c1;eta2)) 1096-} 1097etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion) 1098-- Try to make the coercion be of form (forall tv:kind_co. co) 1099etaForAllCo_ty_maybe co 1100 | Just (tv, kind_co, r) <- splitForAllCo_ty_maybe co 1101 = Just (tv, kind_co, r) 1102 1103 | Pair ty1 ty2 <- coercionKind co 1104 , Just (tv1, _) <- splitForAllTy_ty_maybe ty1 1105 , isForAllTy_ty ty2 1106 , let kind_co = mkNthCo Nominal 0 co 1107 = Just ( tv1, kind_co 1108 , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co)) 1109 1110 | otherwise 1111 = Nothing 1112 1113etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion) 1114-- Try to make the coercion be of form (forall cv:kind_co. co) 1115etaForAllCo_co_maybe co 1116 | Just (cv, kind_co, r) <- splitForAllCo_co_maybe co 1117 = Just (cv, kind_co, r) 1118 1119 | Pair ty1 ty2 <- coercionKind co 1120 , Just (cv1, _) <- splitForAllTy_co_maybe ty1 1121 , isForAllTy_co ty2 1122 = let kind_co = mkNthCo Nominal 0 co 1123 r = coVarRole cv1 1124 l_co = mkCoVarCo cv1 1125 kind_co' = downgradeRole r Nominal kind_co 1126 r_co = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo` 1127 l_co `mkTransCo` 1128 (mkNthCo r 3 kind_co') 1129 in Just ( cv1, kind_co 1130 , mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co)) 1131 1132 | otherwise 1133 = Nothing 1134 1135etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion) 1136-- If possible, split a coercion 1137-- g :: t1a t1b ~ t2a t2b 1138-- into a pair of coercions (left g, right g) 1139etaAppCo_maybe co 1140 | Just (co1,co2) <- splitAppCo_maybe co 1141 = Just (co1,co2) 1142 | (Pair ty1 ty2, Nominal) <- coercionKindRole co 1143 , Just (_,t1) <- splitAppTy_maybe ty1 1144 , Just (_,t2) <- splitAppTy_maybe ty2 1145 , let isco1 = isCoercionTy t1 1146 , let isco2 = isCoercionTy t2 1147 , isco1 == isco2 1148 = Just (LRCo CLeft co, LRCo CRight co) 1149 | otherwise 1150 = Nothing 1151 1152etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion] 1153-- If possible, split a coercion 1154-- g :: T s1 .. sn ~ T t1 .. tn 1155-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] 1156etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2) 1157 = ASSERT( tc == tc2 ) Just cos2 1158 1159etaTyConAppCo_maybe tc co 1160 | not (mustBeSaturated tc) 1161 , (Pair ty1 ty2, r) <- coercionKindRole co 1162 , Just (tc1, tys1) <- splitTyConApp_maybe ty1 1163 , Just (tc2, tys2) <- splitTyConApp_maybe ty2 1164 , tc1 == tc2 1165 , isInjectiveTyCon tc r -- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep 1166 , let n = length tys1 1167 , tys2 `lengthIs` n -- This can fail in an erroneous program 1168 -- E.g. T a ~# T a b 1169 -- #14607 1170 = ASSERT( tc == tc1 ) 1171 Just (decomposeCo n co (tyConRolesX r tc1)) 1172 -- NB: n might be <> tyConArity tc 1173 -- e.g. data family T a :: * -> * 1174 -- g :: T a b ~ T c d 1175 1176 | otherwise 1177 = Nothing 1178 1179{- 1180Note [Eta for AppCo] 1181~~~~~~~~~~~~~~~~~~~~ 1182Suppose we have 1183 g :: s1 t1 ~ s2 t2 1184 1185Then we can't necessarily make 1186 left g :: s1 ~ s2 1187 right g :: t1 ~ t2 1188because it's possible that 1189 s1 :: * -> * t1 :: * 1190 s2 :: (*->*) -> * t2 :: * -> * 1191and in that case (left g) does not have the same 1192kind on either side. 1193 1194It's enough to check that 1195 kind t1 = kind t2 1196because if g is well-kinded then 1197 kind (s1 t2) = kind (s2 t2) 1198and these two imply 1199 kind s1 = kind s2 1200 1201-} 1202 1203optForAllCoBndr :: LiftingContext -> Bool 1204 -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion) 1205optForAllCoBndr env sym 1206 = substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env 1207