Fix in-scope set assertion failure (#23918)

Patch by Simon

compiler/GHC/Tc/Solver.hs

@@ -1360,7 +1360,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
              ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
 
              ; let full_theta = map idType bound_theta_vars
-             ; skol_info <- mkSkolemInfo (InferSkol [ (name, mkSigmaTy [] full_theta ty)
+             ; skol_info <- mkSkolemInfo (InferSkol [ (name, mkPhiTy full_theta ty)
                                                     | (name, ty) <- name_taus ])
        }
 
@@ -1425,7 +1425,7 @@ emitResidualConstraints rhs_tclvl ev_binds_var
                                    , wc_impl   = implics }) }
   where
     full_theta = map idType full_theta_vars
-    skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
+    skol_info = InferSkol [ (name, mkPhiTy full_theta ty)
                           | (name, ty) <- name_taus ]
     -- We don't add the quantified variables here, because they are
     -- also bound in ic_skols and we want them to be tidied

compiler/GHC/Tc/Utils/Instantiate.hs

@@ -80,7 +80,6 @@ import GHC.Types.Error
 import GHC.Types.SourceText
 import GHC.Types.SrcLoc as SrcLoc
 import GHC.Types.Var.Env
-import GHC.Types.Var.Set
 import GHC.Types.Id
 import GHC.Types.Name
 import GHC.Types.Name.Env
@@ -246,8 +245,9 @@ instantiateSigma orig concs tvs theta body_ty
 
       ; return (inst_tvs, wrap, inst_body) }
   where
-    free_tvs = tyCoVarsOfType body_ty `unionVarSet` tyCoVarsOfTypes theta
-    in_scope = mkInScopeSet (free_tvs `delVarSetList` tvs)
+    in_scope = mkInScopeSet (tyCoVarsOfType (mkSpecSigmaTy tvs theta body_ty))
+               -- mkSpecSigmaTy: Inferred vs Specified is not important here;
+               --                We just want an accurate free-var set
     empty_subst = mkEmptySubst in_scope
     new_meta :: Subst -> Subst -> TyVar -> TcM (Subst, TcTyVar)
     new_meta final_subst subst tv

testsuite/tests/typecheck/should_compile/T23918.hs

+module T23918 where
+
+import Data.Kind
+
+f :: forall (a :: Type). a -> a
+f = g @a
+
+g :: forall (k :: Type) (a :: Type) (r :: k). a -> a
+g = g

testsuite/tests/typecheck/should_compile/all.T

@@ -893,3 +893,4 @@ test('T23413', normal, compile, [''])
 test('TcIncompleteRecSel', normal, compile, ['-Wincomplete-record-selectors'])
 test('InstanceWarnings', normal, multimod_compile, ['InstanceWarnings', ''])
 test('T23861', normal, compile, [''])
+test('T23918', normal, compile, [''])