Core Lint error in HEAD and others: The type or coercion variable @(n_sPG :: Nat) is out of scope

Summary

Core lint for the small reproducer by @tomsmeding at https://play.haskell.org/saved/MGwoMDRK produces the following error

*** Core Lint errors : in result of Float out(FOS {Lam = Just 0,
                                                   Consts = True,
                                                   JoinsToTop = True,
                                                   OverSatApps = True}) ***
refl.hs:44:1: warning:
    The type variable ‘n_sQ3’ is out of scope
    In the RHS of listsUncons :: forall {k} (sh1 :: [Nat]) (f :: k).
                                 ListX (MapJust sh1) JustN -> UnconsListSRes f sh1
    In the body of lambda with binder k_aMe :: *
    In the body of lambda with binder sh1_aMf :: [Nat]
    In the body of lambda with binder f_aMg :: k_aMe
    In the body of lambda with binder ds_DNZ :: ListX
                                                  (MapJust sh1_aMf) JustN
    Substitution: <InScope = {k_aMe sh1_aMf f_aMg}
                   IdSubst   = []
                   TvSubst   = []
                   CvSubst   = []>
*** Offending Program ***
unsafeCoerceRefl [InlPrag=NOINLINE]
  :: forall {k} (a :: k) (b :: k). a :~: b
[...]

and also I have a commit in ox-arrays that fails for similar reasons and a commit in horde-ad that fails similarly to #23329 probably for the same reason. I will confirm both are fixed after the problem with the small reproducer is fixed.

Steps to reproduce

Save https://play.haskell.org/saved/MGwoMDRK to file refl.hs and run ghc -O1 --make refl.hs. You can also read the complete lint complaint for different GHC versions (not HEAD unfortunately) by pushing the Run button at the given address.

Expected behavior

Lint and compile fine.

Environment

• GHC version used: 9.15.20251212 and others

Optional:

• Operating System: Ubuntu
• System Architecture: amd64