Specialiser drops quantification of type variables free only in a SpecDict argument, giving out-of-scope Core (#27629) · Issues · Glasgow Haskell Compiler / GHC · GitLab

Specialiser drops quantification of type variables free only in a SpecDict argument, giving out-of-scope Core

## Summary Commit 641ec3f01974dff9dfd756f3f0499796c8df1a8b ("Fix scoping errors in specialisation", fixing #26682; cherry-picked to `ghc-9.14` as 55f0de7cebf5da569f56e1a2d39fe3cc2c787cde for 9.14.2) refactored `specHeader`/`spec_call` in `GHC.Core.Opt.Specialise` so that the extra type variables to quantify in a specialisation are computed in `specHeader` alone. The new code collects them only in the `SpecType` case (`free_tvs`, from `tyCoVarsOfTypeList ty`). The old `spec_call` code computed `poly_qvars` from the free variables of *all* `SpecArg`s, including dictionary *expressions* (`specArgsFVs` has `get (SpecDict dx) = exprFVs dx`). So a type variable that is free in a `SpecDict` argument's *expression* but not in its *type* (and not in any `SpecType` argument) is no longer quantified anywhere: the specialised RHS (or a floated `dx_bind`) mentions it out of scope. This is exactly the shape documented in Note [Weird special case for SpecDict] (from #22459), and it violates (MP2) of Note [Specialising polymorphic dictionaries]. It needs `-fpolymorphic-specialisation`: with that flag `ci_fvs` deliberately omits type variables (see (MP1) and `singleCall`), so such calls float past their `/\a` binders by design. Note [Weird special case for SpecDict] claims the case is prevented by a guard in the `SpecDict` case of `specHeader`: ``` allVarSet (`elemInScopeSet` in_scope) (exprFreeVars d) ``` but that guard does not exist: it was deleted in 695fc5d2b2, precisely when `poly_qvars` was introduced to subsume it — and 641ec3f019 now deletes `poly_qvars` without restoring the guard. (Two stale references to `poly_qvars` also survive in comments in `spec_call`.) Both `master` and `ghc-9.14` are affected. ## Reproducer The triggering dictionary shape (`mkD @a :: C T` with `a` free only in the expression) cannot be written in source Haskell — the known producer (`abstractFloats` over-abstraction, #22459) was fixed — so the reproducer uses a small Core plugin to inject the Note's example before the Core pipeline runs. The injected Core is scope-correct, ordinary Core; the specialiser is expected to handle it. `Repro.hs` (compiled with `-O -fpolymorphic-specialisation -dcore-lint`) defines a recursive overloaded `split :: C b => [b] -> [b]` and `poly :: forall (x :: Type). T -> [T]`; the plugin adds `mkD :: forall a. T -> C T` (NOINLINE, `mkD = /\a. \_. $fCT`) and rewrites `poly` to ``` poly = /\x. \t. split @T (mkD @x MkT) [t] ``` With a compiler containing 641ec3f019 (tested: in-tree stage2 at d415f38a75, 10.1.20260710), specialising `split` produces: ``` *** Core Lint errors : in result of Specialise *** <no location info>: warning: The type variable ‘x_auL’ is out of scope In the RHS of $dC_swk :: C T ... $dC_swk :: C T $dC_swk = mkD_sw1 @x_auL MkT Rec { $ssplit_swj :: [T] -> [T] $ssplit_swj = \ (ds_DvU :: [T]) -> case ds_DvU of { [] -> [] @T; : x_aqt xs_aqu -> : @T (meth @T $dC_swk x_aqt) (split @T $dC_swk xs_aqu) } ``` The floated dictionary binding `$dC_swk = mkD @x MkT` has escaped its `/\x` binder. Without `-dcore-lint` this small example compiles silently, i.e. the scope-broken Core goes unnoticed. Control: GHC 9.14.1 (pre-patch) on the same input correctly builds `$ssplit = /\x. let $dC = mkD @x MkT in ...` via `poly_qvars` — but Lint instead reports `Rule "SPEC split @T": unbound [x_aG6]`, the rule template variable that is not bound on the rule LHS. That is the #26682 bug which 641ec3f019 fixed. So the old quantification was also not a complete answer for this call shape; the patch fixed the rule but made the specialised code itself scope-broken, which seems worse. Presumably the right treatment for a call whose dictionary argument has out-of-scope free variables is to decline to specialise it — i.e. restore the guard that Note [Weird special case for SpecDict] still describes (or quantify the dict expression's tyvars in `specHeader`'s `SpecDict` case and keep them off the RULE). If instead the case is deemed impossible nowadays, the Note should be updated to say why, and the stale `poly_qvars` comments removed. `run.sh` (set `GHC=` to a plugin-capable build containing 641ec3f019; defaults to an in-tree stage2): <details> <summary>run.sh</summary> ```sh #!/bin/sh # Reproduces the SpecDict quantification bug introduced by 641ec3f019 # ("Fix scoping errors in specialisation"). # # GHC must contain 641ec3f019 and be plugin-capable (a stage-2 in-tree # build works). Expected result: Core Lint "out of scope" errors after # the Specialiser pass. set -e GHC=${GHC:-$HOME/ghc/work/_build/stage1/bin/ghc} cd "$(dirname "$0")" rm -f ./*.hi ./*.o "$GHC" --make -package ghc -dynamic-too -c ReproPlugin.hs "$GHC" -c -O -fpolymorphic-specialisation -dcore-lint Repro.hs ``` </details> <details> <summary>Repro.hs</summary> ```haskell {-# LANGUAGE AllowAmbiguousTypes #-} {-# OPTIONS_GHC -fplugin=ReproPlugin #-} -- The plugin rewrites 'poly' to the example of -- Note [Weird special case for SpecDict]: -- -- poly = /\x. \t. split @T (mkD @x MkT) [t] -- -- where mkD :: forall a. T -> C T is a new top-level binding -- (mkD = /\a. \_. $fCT), so the tyvar x is free in the dictionary -- *expression* but not in its *type* (C T). module Repro (poly, split, T (..), C (..)) where import Data.Kind (Type) data T = MkT class C b where meth :: b -> b instance C T where meth x = x split :: C b => [b] -> [b] split [] = [] split (x : xs) = meth x : split xs poly :: forall (x :: Type). T -> [T] poly t = [t] ``` </details> <details> <summary>ReproPlugin.hs</summary> ```haskell -- Injects the example of Note [Weird special case for SpecDict] in -- GHC.Core.Opt.Specialise, which cannot be written in source Haskell: -- a call whose dictionary argument mentions a type variable that is -- free in the dictionary expression but not in its type. -- -- Runs before the main Core pipeline (in particular before the -- Specialiser). It adds -- -- mkD :: forall a. T -> C T {-# NOINLINE mkD #-} -- mkD = /\a. \_. $fCT -- -- and rewrites poly = /\x. \t. [t] -- to poly = /\x. \t. split @T (mkD @x MkT) [t] {-# LANGUAGE CPP #-} module ReproPlugin (plugin) where import GHC.Core.Make (mkCoreApps, mkListExpr) import GHC.Core.Predicate (getClassPredTys_maybe) import GHC.Plugins #if __GLASGOW_HASKELL__ >= 1000 import GHC.Types.InlinePragma (neverInlinePragma) #else import GHC.Types.Basic (neverInlinePragma) #endif plugin :: Plugin plugin = defaultPlugin { installCoreToDos = \_ todos -> return (CoreDoPluginPass "inject-weird-specdict" pass : todos) , pluginRecompile = purePlugin } pass :: ModGuts -> CoreM ModGuts pass guts = do let binds = mg_binds guts dfun = case [b | b <- bindersOfBinds binds, isDFunId b] of (b : _) -> b [] -> panic "ReproPlugin: no dfun binding in module" dictTy = idType dfun -- C T tyT = case getClassPredTys_maybe dictTy of Just (_cls, [t]) -> t _ -> panic "ReproPlugin: dfun type is not C T" mkTCon = case tyConDataCons (tyConAppTyCon tyT) of (dc : _) -> dataConWorkId dc [] -> panic "ReproPlugin: T has no data constructors" findTopId nm = case [b | b <- bindersOfBinds binds, occNameString (getOccName b) == nm] of (b : _) -> b [] -> panic ("ReproPlugin: no top-level binding " ++ nm) splitId = findTopId "split" polyId = findTopId "poly" uMkD <- getUniqueM uTv <- getUniqueM uWild <- getUniqueM let aTv = mkTyVar (mkSystemName uTv (mkTyVarOcc "a")) liftedTypeKind mkDTy = mkSpecForAllTys [aTv] (mkFunctionType ManyTy tyT dictTy) mkDId = setInlinePragma (mkExportedVanillaId (mkSystemName uMkD (mkVarOcc "mkD")) mkDTy) neverInlinePragma wild = mkSysLocal (fsLit "eta") uWild ManyTy tyT mkDBind = NonRec mkDId (mkLams [aTv, wild] (Var dfun)) rewritePoly rhs | (bndrs, _body) <- collectBinders rhs , (x : _) <- reverse (filter isTyVar bndrs) , (t : _) <- filter isId bndrs = mkLams bndrs $ mkCoreApps (Var splitId) [ Type tyT , mkCoreApps (Var mkDId) [Type (mkTyVarTy x), Var mkTCon] , mkListExpr tyT [Var t] ] | otherwise = pprPanic "ReproPlugin: unexpected shape of poly" (ppr rhs) go (b, rhs) | b == polyId = (b, rewritePoly rhs) | otherwise = (b, rhs) -- One top-level Rec, so bind order is irrelevant. binds' = [Rec (map go (flattenBinds binds) ++ flattenBinds [mkDBind])] putMsgS "ReproPlugin: injected weird SpecDict call into poly" return guts {mg_binds = binds'} ``` </details> ## Impact assessment Narrow in practice today: it needs `-fpolymorphic-specialisation` (off by default; #23559 tracks re-enabling it) *and* a dictionary expression whose type variables are hidden from its type, whose one known in-tree producer was fixed. But the triggering Core is valid input that any pass or plugin may produce, the specialiser is expected to be robust to it, and the compiled result is scope-broken Core that only `-dcore-lint` notices. At minimum the code and Note [Weird special case for SpecDict] now contradict each other and one of them should change. ## Provenance This issue was found by GlaHiCo, an LLM-generated review of 641ec3f019 / 55f0de7cebf5 (review published at https://gitlab.haskell.org/sjakobi/GlaHiCo/-/snippets/6128), and was verified and written up with LLM assistance. A human reviewed the finding before filing.

issue

Admin message