**Update 2026-06-16:** You can find a reproducer / regression test on my [`wip/sjakobi/T27374` branch](https://gitlab.haskell.org/ghc/ghc/-/tree/wip/sjakobi/T27374) (d4939d2d5ff63433578fbdf2ac6bdd59cea4e41f). ---- I had Claude (Fable 5) look into #27016. During this work, it claims to have found a bug in `optCoercion`: ## Summary `optCoercion` is not kind-preserving on a certain shape of (well-formed, lint-valid) input coercion: a `TyConAppCo` transitively composed with `Sym (SelCo:Fun(arg) (InstCo ... (Refl (forall ...)) ...))`, where the `InstCo` chain instantiates a `Refl` of a forall-type and the instantiating argument coercions are `Sym` of type-family axioms. The output coercion has a *different right-hand type* than the input, and even contains an internally ill-formed transitivity composition (`Sym ax ; Sym ax` where the kinds don't line up), which Core Lint then rejects. As far as I know, GHC HEAD does not currently *build* coercions of this shape, so the bug is latent on master. I hit it while developing a fix for #27016 (making SPECIALISE rules fire when a call's type argument is an un-reduced type-family application): the natural way to build the compensating cast there is an `InstCo` chain over `Refl_R (idType f)`, and with that construction `T21689` fails `-dcore-lint`. Switching the construction to `liftCoSubstWith` avoids the optimiser bug, but `optCoercion` should be kind-preserving on any valid input. ## Concrete failing input/output Captured with a kind-preservation check added to `optCoercion'` (see below) while compiling `testsuite/tests/simplCore/should_compile/T21689.hs` with `-O -dcore-lint`. Here `D:R:DimVec <n>_N :: Dim (Vec n) ~N n` is the axiom for the type family instance `Dim (Vec n) = n` from T21689a.hs. Input (role R; both sides of its kind are the *same* type, i.e. the coercion is reflexive-but-not-Refl): ``` in_co: ((,,) (ArityPeano (Peano (Sym (D:R:DimVec <n_a1RN>_N)))_N)_N (KnownNat (Sym (D:R:DimVec <n_a1RN>_N)))_N ((~) <PeanoNum>_N (Peano (Sym (D:R:DimVec <n_a1RN>_N) + <1>_N)_N)_N ('S (Peano (Sym (D:R:DimVec <n_a1RN>_N)))_N)_N)_N)_R ; Sym (SelCo:Fun(arg) (Inst (Inst (Inst <forall (a :: Constraint) (b :: Constraint) (c :: Constraint). (a, b, c) => a>_R (Sym (ArityPeano (Peano (D:R:DimVec <n_a1RN>_N))_N)_N)) (Sym (KnownNat (D:R:DimVec <n_a1RN>_N))_N)) (Sym ((~) <PeanoNum>_N (Peano (D:R:DimVec <n_a1RN>_N + <1>_N)_N)_N ('S (Peano (D:R:DimVec <n_a1RN>_N))_N)_N)_N))) in_ty1: (ArityPeano (Peano n_a1RN), KnownNat n_a1RN, (Peano (n_a1RN + 1) :: PeanoNum) ~ ('S (Peano n_a1RN) :: PeanoNum)) in_ty2: (ArityPeano (Peano n_a1RN), KnownNat n_a1RN, (Peano (n_a1RN + 1) :: PeanoNum) ~ ('S (Peano n_a1RN) :: PeanoNum)) ``` Output of `optCoercion` on that input: ``` out_co: ((,,) <ArityPeano (Peano n_a1RN)>_N (KnownNat (Sym (D:R:DimVec <n_a1RN>_N) ; Sym (D:R:DimVec <n_a1RN>_N)))_N <(Peano (n_a1RN + 1) :: PeanoNum) ~ ('S (Peano n_a1RN) :: PeanoNum)>_N)_R out_ty1: (ArityPeano (Peano n_a1RN), KnownNat n_a1RN, (Peano (n_a1RN + 1) :: PeanoNum) ~ ('S (Peano n_a1RN) :: PeanoNum)) out_ty2: (ArityPeano (Peano n_a1RN), KnownNat (Dim (Vec n_a1RN)), (Peano (n_a1RN + 1) :: PeanoNum) ~ ('S (Peano n_a1RN) :: PeanoNum)) ``` Two things are wrong: 1. The right-hand type changed: the second tuple component became `KnownNat (Dim (Vec n))` instead of `KnownNat n`. 2. The output is internally ill-formed: `Sym (D:R:DimVec <n>) ; Sym (D:R:DimVec <n>)` composes `n ~ Dim (Vec n)` with `n ~ Dim (Vec n)`, whose kinds don't line up. Core Lint reports exactly this: ``` *** Core Lint errors : in result of Simplifier *** T21689.hs:27:3: warning: Trans coercion mis-match: Sym (D:R:DimVec <n_a3qz>_N) ; Sym (D:R:DimVec <n_a3qz>_N) n_a3qz ~ Dim (Vec n_a3qz) n_a3qz ~ Dim (Vec n_a3qz) ``` It looks as though a `Sym` is lost on the coercions substituted in via the lifting context: the second operand of the trans should contribute `KnownNat (D:R:DimVec <n>)` (i.e. with the ambient `Sym` of the `Sym (SelCo ...)` applied to the instantiating `Sym (KnownNat ...)` argument), but instead contributes `KnownNat (Sym (D:R:DimVec <n>))` un-sym'd. The suspect area is the `InstCo` case of `opt_co4'` in `GHC.Core.Coercion.Opt` together with the `(LC2)` convention ("lifting-context entries have *not* had the ambient sym applied") from `Note [The LiftingContext in optCoercion]` — the instantiating argument is deliberately optimised with `NotSwapped`, and somewhere downstream the ambient sym fails to be re-applied to it. The same compile produced six kind-preservation violations, all of this shape. ## Evidence that the coercion optimiser is at fault * With the triggering construction in place, `T21689` fails `-dcore-lint` as above; adding `-fno-opt-coercion` makes the same compile lint-clean. * The input coercion above is produced by lint-valid Core (everything lints before the offending `optCoercion` call); only the output is ill-formed. ## How to reproduce / trigger There is no known trigger from vanilla HEAD. The shape arises from a work-in-progress fix for #27016, which rewrites a call `f @t1 .. @tn --> (f @t1' .. @tn') |> co` (normalising type-family redexes in the `ti` so that SPECIALISE rules match), with `co` built as an `InstCo` chain. A reproducer branch is pushed to this repo: * branch `wip/sjakobi/optCoercion-repro`, tip af610a1e2d (one commit on top of master 7ab9028865) * at that commit, compiling `testsuite/tests/simplCore/should_compile/T21689.hs` (with its companion `T21689a.hs`) using `-O -dcore-lint` fails with the lint error above; adding `-fno-opt-coercion` makes it pass The relevant part of the patch builds the cast like this: ```haskell -- fun :: forall as. blah; for each type argument: -- unchanged ti: fun_co := mkInstCo fun_co (mkNomReflCo ti) -- reduced ti~ti' by arg_co (:: ti ~N ti'): -- fun_co := mkInstCo fun_co (mkSymCo arg_co) -- starting from fun_co := mkReflCo Representational (idType fun) ``` (Building the same cast with `liftCoSubstWith Representational tvs cos body_ty` instead — i.e. peeling the foralls and lifting once — produces equivalent input to the simplifier but does not tickle the optimiser, and everything lints.) A self-contained way to observe the bug without any patch would be to feed the `in_co` above to `optCoercion` directly (e.g. via the GHC API), since the input is a perfectly valid coercion; I can help construct that if useful. ## Suggested hardening `optCoercion'` already has a `debugIsOn` branch that computes the input and output `coercionKindRole` but only warns about "reflexive but not refl". It seems worth also asserting kind preservation there, e.g. ```haskell warnPprTrace (not (substTy env in_ty1 `eqType` out_ty1) || not (substTy env in_ty2 `eqType` out_ty2)) "optCoercion changed kind" details $ ... ``` That check is what caught the six violations above. ## Environment GHC HEAD, master at 7ab9028865 ("fix: make T27131 less flaky"), plus the trigger commit af610a1e2d on branch `wip/sjakobi/optCoercion-repro`. Linux x86_64, quick flavour.