Simon Peyton Jones pushed to branch wip/spj-try-opt-coercion at Glasgow Haskell Compiler / GHC Commits: ce739998 by Simon Peyton Jones at 2026-05-04T17:39:49+01:00 Improve the gobbler - - - - - 1 changed file: - compiler/GHC/Core/Coercion/Opt.hs Changes: ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -326,7 +326,7 @@ opt_co_refl subst co go_hole h@(CH { ch_co_var = cv }) = h { ch_co_var = updateVarType go_ty cv } - go (Refl ty) = Refl (substTy subst ty) + go (Refl ty) = Refl $!! substTy subst ty go (GRefl r ty mco) = GRefl r $!! go_ty ty $!! go_m mco go (CoVarCo cv) = substCoVar subst cv go (HoleCo h) = HoleCo $!! go_hole h @@ -351,40 +351,64 @@ opt_co_refl subst co -- The TransCo case fires up the main loop for -- eliminating reflexive chains of TransCo - go (TransCo co1 co2) - | lk' `eqTypeIgnoringMultiplicity` rk' = go co2 - | otherwise = gobble0 gs1 [co2] - where - co1' = go co1 - Pair lk' rk' = coercionKind co1' - role = coercionRole co1 - - gs0, gs1 :: GobbleState - gs0 = GS (mkReflCo role lk') tm0 - gs1 = GS co1' (insertTM rk' gs1 tm0) - - tm0 = insertTM lk' gs0 emptyTM - - gobble0 :: GobbleState -> [InCoercion] -> OutCoercion - gobble0 (GS co _) [] = co - gobble0 gs (co:cos) = gobble gs co cos - - gobble :: GobbleState -> InCoercion -> [InCoercion] -> OutCoercion - -- gobble (GS co1 tm) co2 cos returns a coercion equivalent to (co1;co2;cos) - gobble gs (TransCo co2 co3) cos - = gobble gs co2 (co3 : cos) - gobble (GS co1' tm) co2 cos - = case lookupTM rk' tm of - Just gs -> gobble0 gs cos - Nothing -> gobble0 gs' cos - where - co2' = go co2 - rk' = coercionRKind co2' - gs' = GS (co1' `mkTransCo` co2') (insertTM rk' gs' tm) - - -data GobbleState = GS OutCoercion (TypeMap GobbleState) - -- The map is keyed by OutType + -- See Note [Optimising TransCo sequences] + go co@(TransCo {}) = gobble gs0 out_cos + where + out_cos :: [OutCoercion] -- None of these are TransCos + out_cos@(out_co1:_) = get_in co [] + gs0 = GS (mkReflCo role lk) tm0 + tm0 = insertTM lk gs0 emptyTM + lk = coercionLKind out_co1 + role = coercionRole out_co1 + + get_in :: InCoercion -> [OutCoercion] -> [OutCoercion] + get_in (TransCo co1 co2) cos = get_in co1 (get_in co2 cos) + get_in (SymCo (TransCo co1 co2)) cos = get_in (mkSymCo co2) (get_in (mkSymCo co1) cos) + get_in co cos = get_out (go co) cos + + get_out :: OutCoercion -> [OutCoercion] -> [OutCoercion] + -- Maybe `go` returned an OutCoercion that is a `TransCo` + get_out (TransCo co1 co2) cos = get_out co1 (get_out co2 cos) + get_out (SymCo (TransCo co1 co2)) cos = get_out (mkSymCo co2) (get_out (mkSymCo co1) cos) + get_out co cos = co : cos + + gobble :: GobbleState -> [OutCoercion] -> OutCoercion + gobble (GS co0 tm) cos + = case cos of + [] -> co0 + (co1:cos) -> case lookupTM rk1 tm of + Just gs -> gobble gs cos -- A hit in the GobbleState map; + -- revert to the earlier state gs + Nothing -> gobble gs' cos -- Miss: make a new GobbleState gs' + where + rk1 = coercionRKind co1 + gs' = GS (co0 `mkTransCo` co1) (insertTM rk1 gs' tm) + +data GobbleState = GS OutCoercion !(TypeMap GobbleState) + +{- Note [Optimising TransCo sequences] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In a composition (co1; co2; co3; ... ; con) we work left-to-right, maintaining +a `GobbleState`. Imagine we start with gs0::GobbleState, we process `co1` to get +`gs1` and so on. + +When composing co_i, if coercionRKind( co_i ) is the same as any earlier type in +the chain, we want to discard it and simply revert to the GobbleState of that +earlier point. + +So a GobbleState has + +* The coercion so far: a coercion equivalent to (co1;co2;cok) +* A map from types to all earlier GobbleStates, thus + tyR_i :-> gs_i + where (INVARIANT) tyR_i is the coercionRKind of gs_i + +Wrinkles: + +* Wart: the TypeMap is (currently) multiplicity-sensitive so we might + miss a possible TransCo optimisation. + +-} optUnivCo :: UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce7399982c7a57a4d4b9eb41c32a5b96... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce7399982c7a57a4d4b9eb41c32a5b96... You're receiving this email because of your account on gitlab.haskell.org.