Get the right in-scope set in etaBodyForJoinPointwip/T23026

Fixes #23026

3 files changed, 40 insertions, 4 deletions

diff --git a/compiler/GHC/Core/Opt/Arity.hs b/compiler/GHC/Core/Opt/Arity.hs
index cd0463961e..dfcf1f1ab7 100644
--- a/compiler/GHC/Core/Opt/Arity.hs
+++ b/compiler/GHC/Core/Opt/Arity.hs
@@ -3105,7 +3105,7 @@ etaExpandToJoinPointRule join_arity rule@(Rule { ru_bndrs = bndrs, ru_rhs = rhs
 -- Adds as many binders as asked for; assumes expr is not a lambda
 etaBodyForJoinPoint :: Int -> CoreExpr -> ([CoreBndr], CoreExpr)
 etaBodyForJoinPoint need_args body
-  = go need_args (exprType body) (init_subst body) [] body
+  = go need_args body_ty (mkEmptySubst in_scope) [] body
   where
     go 0 _  _     rev_bs e
       = (reverse rev_bs, e)
@@ -3124,9 +3124,16 @@ etaBodyForJoinPoint need_args body
       = pprPanic "etaBodyForJoinPoint" $ int need_args $$
                                          ppr body $$ ppr (exprType body)
 
-    init_subst e = mkEmptySubst (mkInScopeSet (exprFreeVars e))
-
-
+    body_ty = exprType body
+    in_scope = mkInScopeSet (exprFreeVars body `unionVarSet` tyCoVarsOfType body_ty)
+    -- in_scope is a bit tricky.
+    -- - We are wrapping `body` in some value lambdas, so must not shadow
+    --   any free vars of `body`
+    -- - We are wrapping `body` in some type lambdas, so must not shadow any
+    --   tyvars in body_ty.  Example: body is just a variable
+    --            (g :: forall (a::k). T k a -> Int)
+    --   We must not shadown that `k` when adding the /\a. So treat the free vars
+    --   of body_ty as in-scope.  Showed up in #23026.
 
 --------------
 freshEtaId :: Int -> Subst -> Scaled Type -> (Subst, Id)
diff --git a/testsuite/tests/simplCore/should_compile/T23026.hs b/testsuite/tests/simplCore/should_compile/T23026.hs
new file mode 100644
index 0000000000..4ca2a82550
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T23026.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+
+module T23026 where
+
+import Data.Kind (Type)
+
+data Sing (a :: k)
+data SingInstance (a :: k) = SingInstance (Sing a)
+
+app :: (Sing a -> SingInstance a) -> Sing a -> SingInstance a
+app f x = f x
+{-# NOINLINE app #-}
+
+withSomeSing
+  :: forall k2 k1 (f :: k2 -> k1 -> Type) a2 a1.
+     (Sing a2, Sing a1)
+  -> f a2 a1
+  -> (forall b2 b1. f b2 b1 -> Int)
+  -> Int
+withSomeSing (sa2, sa1) x g =
+  case app SingInstance sa2 of
+    SingInstance _ ->
+      case app SingInstance sa1 of
+        SingInstance _ -> g x
+{-# INLINABLE withSomeSing #-}
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index c4e78e0f75..bf7f4e58dd 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -476,3 +476,4 @@ test('T23012', normal, compile, ['-O'])
 
 test('RewriteHigherOrderPatterns', normal, compile, ['-O -ddump-rule-rewrites -dsuppress-all -dsuppress-uniques'])
 test('T23024', normal, multimod_compile, ['T23024', '-O -v0'])
+test('T23026', normal, compile, ['-O'])