Mis-oriented <.> in mkWpFun_FRR builds ill-kinded coercion (#27639) · Issues · Glasgow Haskell Compiler / GHC · GitLab

Mis-oriented <.> in mkWpFun_FRR builds ill-kinded coercion

## Summary Commit 8adfc22242b0 ("Fix orientation in HsWrapper composition (`<.>`)", fixing #26350) changed the cast-composition rule to match the function-composition semantics of `<.>`: ```haskell WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1) -- was: c1 ; c2 ``` It fixed the *outer* composition in `GHC.Tc.Utils.Unify.mkWpFun_FRR` (test T26350), but the *inner* composition in the same function is still written in the old, leftmost-applied-first orientation (`compiler/GHC/Tc/Utils/Unify.hs:2362` on master, `:2132` on ghc-9.14 with the backport b4f0eba7aba3): ```haskell arg_wrap_frr = mkWpCastN (mkSymCo exp_arg_co) <.> arg_wrap <.> mkWpCastN act_arg_co -- exp_arg_co :: exp_arg ~> exp_arg_frr -- act_arg_co :: act_arg ~> act_arg_frr -- arg_wrap :: exp_arg ~> act_arg -- arg_wrap_frr :: exp_arg_frr ~> act_arg_frr ``` Per the direction comments right next to it, the components are ``` mkWpCastN (mkSymCo exp_arg_co) :: exp_arg_frr ~> exp_arg arg_wrap :: exp_arg ~> act_arg mkWpCastN act_arg_co :: act_arg ~> act_arg_frr ``` and the required result is `arg_wrap_frr :: exp_arg_frr ~> act_arg_frr` (forced by its use in `mkWpFun arg_wrap_frr res_wrap ...`, whose `WpFun` desugaring applies `arg_wrap_frr` to the lambda binder of type `exp_arg_frr`). Since `<.>` composes like function composition — rightmost wrapper applied first, exactly what 8adfc222's new comment in `GHC.Tc.Types.Evidence` documents — the composition must be the mirror image: ```haskell arg_wrap_frr = mkWpCastN act_arg_co <.> arg_wrap <.> mkWpCastN (mkSymCo exp_arg_co) ``` As written, when `arg_wrap` is a `WpCast` and the `hasFixedRuntimeRep` coercions are non-reflexive, the old rule happened to produce the well-kinded `WpCast (sym exp_arg_co ; w ; act_arg_co)`; the fixed rule now produces `WpCast (act_arg_co ; w ; sym exp_arg_co)`, whose `TransCo` joins `w`'s RHS (`act_arg`) to `sym exp_arg_co`'s LHS (`exp_arg_frr`) — ill-kinded (`mkTransCo` does no kind checking), and rejected by Core Lint. So for this sub-case the fix trades one ill-kinded wrapper for another, regressing programs that GHC 9.14.1 compiles cleanly. The new T26350 test doesn't catch this because its types have syntactically fixed runtime representations: both FRR coercions are `Refl`, `mkWpCastN` collapses to `WpHole`, and the composition order is irrelevant. Triggering it needs DeepSubsumption where (a) eta-expansion is required (`needs_frr_checks`), and (b) the argument type's runtime rep is fixed only up to a non-trivial coercion, so `hasFixedRuntimeRep` returns non-`Refl` — which is precisely the situation this FRR code path exists to handle. ## Reproducer ```haskell {-# LANGUAGE DeepSubsumption, RankNTypes, PolyKinds, DataKinds, GADTs, TypeOperators, ScopedTypeVariables #-} module Repro where import GHC.Exts import Data.Type.Equality h :: forall r (a :: TYPE r) (b :: TYPE r). (r :~: LiftedRep) -> (a :~: b) -> () h Refl Refl = let v :: a -> (Int -> Int) -> Int v = undefined u :: b -> (forall c. c -> c) -> Int u = v in () ``` `u = v` needs deep subsumption. The result comparison `(Int -> Int) -> Int ≤ (forall c. c -> c) -> Int` requires a type application under a lambda, so `res_wrap` is not a cast and `mkWpFun_FRR` takes the `WpFun` path with FRR checks. The argument types `a`, `b :: TYPE r` have a fixed runtime rep only via the given `r ~ LiftedRep`, so both FRR coercions are non-`Refl` `GRefl` casts, and `arg_wrap` is the non-trivial cast `b ~ a` from the second given. With a master build containing 8adfc222 (10.1.20260710 = d415f38a75): ``` $ ghc -dcore-lint Repro.hs [1 of 1] Compiling Repro ( Repro.hs, Repro.o ) *** Core Lint errors : in result of Desugar (before optimization) *** Repro.hs:7:1: warning: Trans coercion mis-match: Sub co_atQ ; Sub (Sym (GRefl nominal b_atK (TYPE co_av3)_N)) b_atK ~ a_atJ (b_atK |> (TYPE co_av3)_N) ~ b_atK ... ``` The mismatched `TransCo` is exactly the mis-ordered composition: `co_atQ :: b ~# a` is `arg_wrap`'s coercion and is transitivity-composed with `sym exp_arg_co :: (b |> TYPE co) ~ b` — RHS `a` against LHS `b |> TYPE co`. GHC 9.14.1 (which has `mkWpFun_FRR` via d44e8dbe24 but the old `<.>` orientation) compiles the same file cleanly with `-dcore-lint`, so this is a regression introduced by 8adfc222 on master and by its backport b4f0eba7aba3 on ghc-9.14 (slated for 9.14.2). Without `-dcore-lint` compilation "succeeds" but produces the ill-kinded coercion in the desugared Core. <details><summary>Repro.hs</summary> ```haskell {-# LANGUAGE DeepSubsumption, RankNTypes, PolyKinds, DataKinds, GADTs, TypeOperators, ScopedTypeVariables #-} module Repro where import GHC.Exts import Data.Type.Equality h :: forall r (a :: TYPE r) (b :: TYPE r). (r :~: LiftedRep) -> (a :~: b) -> () h Refl Refl = let v :: a -> (Int -> Int) -> Int v = undefined u :: b -> (forall c. c -> c) -> Int u = v in () ``` </details> <details><summary>run.sh</summary> ```sh #!/bin/sh # Core Lint failure from mis-oriented arg_wrap_frr composition in mkWpFun_FRR. # Usage: GHC=/path/to/ghc sh run.sh # - GHC containing 8adfc22242b0 (master) / b4f0eba7aba3 (ghc-9.14): Lint error # - GHC 9.14.1 (pre-fix <.>): compiles cleanly : "${GHC:=ghc}" $GHC --version $GHC -dcore-lint -fforce-recomp Repro.hs ``` </details> ## Suggested fix Swap the composition (untested, but forced by the direction comments): ```haskell arg_wrap_frr = mkWpCastN act_arg_co <.> arg_wrap <.> mkWpCastN (mkSymCo exp_arg_co) ``` Side observation from the same analysis: when `arg_wrap` is *not* a hole/cast (e.g. contains a type application), the `WpCompose` desugaring applied the rightmost wrapper first even before 8adfc222, so that sub-case of the line appears to have been wrong already in 9.14.1; the swap above should fix both sub-cases. The reproducer above would make a reasonable regression test next to T26350. ## Provenance Found by [GlaHiCo](https://gitlab.haskell.org/sjakobi/GlaHiCo), an LLM-driven review pipeline, while reviewing the 9.14.2 backports; the published review of b4f0eba7aba3 (= master 8adfc22242b0) is at https://gitlab.haskell.org/sjakobi/GlaHiCo/-/snippets/6142 (finding f1). This draft was prepared by an LLM agent (which also built and ran the reproducer) and reviewed by a human before filing.

issue

Admin message