checkValidInst: Don't expand synonyms when splitting sigma typeswip/T22570

Previously, the `checkValidInst` function (used when checking that an instance
declaration is headed by an actual type class, not a type synonym) was using
`tcSplitSigmaTy` to split apart the `forall`s and instance context. This is
incorrect, however, as `tcSplitSigmaTy` expands type synonyms, which can cause
instances headed by quantified constraint type synonyms to be accepted
erroneously.

This patch introduces `splitInstTyForValidity`, a variant of `tcSplitSigmaTy`
specialized for validity checking that does _not_ expand type synonyms, and
uses it in `checkValidInst`.

Fixes #22570.

4 files changed, 55 insertions, 2 deletions

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 15168ddd2f..5ac3377a33 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -61,7 +61,7 @@ import GHC.Types.Basic   ( UnboxedTupleOrSum(..), unboxedTupleOrSumExtension )
 import GHC.Types.Name
 import GHC.Types.Var.Env
 import GHC.Types.Var.Set
-import GHC.Types.Var     ( VarBndr(..), mkTyVar )
+import GHC.Types.Var     ( VarBndr(..), isInvisibleFunArg, mkTyVar )
 import GHC.Utils.FV
 import GHC.Utils.Error
 import GHC.Driver.Session
@@ -1731,6 +1731,13 @@ the instance head, we'll expand the synonym on fly, and it'll look like
   instance (%,%) (Show Int, Show Int)
 and we /really/ don't want that.  So we carefully do /not/ expand
 synonyms, by matching on TyConApp directly.
+
+For similar reasons, we do not use tcSplitSigmaTy when decomposing the instance
+context, as the looks through type synonyms. If we looked through type
+synonyms, then it could be possible to write an instance for a type synonym
+involving a quantified constraint (see #22570). Instead, we define
+splitInstTyForValidity, a specialized version of tcSplitSigmaTy (local to
+GHC.Tc.Validity) that does not expand type synonyms.
 -}
 
 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
@@ -1774,11 +1781,31 @@ checkValidInstance ctxt hs_type ty = case tau of
         ; return () }
   _ -> failWithTc (TcRnNoClassInstHead tau)
   where
-    (_tvs, theta, tau)   = tcSplitSigmaTy ty
+    (theta, tau) = splitInstTyForValidity ty
 
         -- The location of the "head" of the instance
     head_loc = getLoc (getLHsInstDeclHead hs_type)
 
+-- | Split an instance type of the form @forall tvbs. inst_ctxt => inst_head@
+-- and return @(inst_ctxt, inst_head)@. This function makes no attempt to look
+-- through type synonyms. See @Note [Instances and constraint synonyms]@.
+splitInstTyForValidity :: Type -> (ThetaType, Type)
+splitInstTyForValidity = split_context [] . drop_foralls
+  where
+    -- This is like 'dropForAlls', except that it does not look through type
+    -- synonyms.
+    drop_foralls :: Type -> Type
+    drop_foralls (ForAllTy (Bndr _tv argf) ty)
+      | isInvisibleForAllTyFlag argf = drop_foralls ty
+    drop_foralls ty = ty
+
+    -- This is like 'tcSplitPhiTy', except that it does not look through type
+    -- synonyms.
+    split_context :: ThetaType -> Type -> (ThetaType, Type)
+    split_context preds (FunTy { ft_af = af, ft_arg = pred, ft_res = tau })
+      | isInvisibleFunArg af = split_context (pred:preds) tau
+    split_context preds ty = (reverse preds, ty)
+
 {-
 Note [Paterson conditions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/typecheck/should_fail/T22570.hs b/testsuite/tests/typecheck/should_fail/T22570.hs
new file mode 100644
index 0000000000..25a54aa29b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22570.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+module T22570 where
+
+import Data.Kind
+
+class SomeClass a
+class OtherClass
+
+type SomeClassUnit = OtherClass => SomeClass () :: Constraint
+
+instance SomeClassUnit
+
+type SomeClassSyn a = OtherClass => SomeClass a :: Constraint
+
+instance SomeClassSyn ()
diff --git a/testsuite/tests/typecheck/should_fail/T22570.stderr b/testsuite/tests/typecheck/should_fail/T22570.stderr
new file mode 100644
index 0000000000..023d1508e4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22570.stderr
@@ -0,0 +1,10 @@
+
+T22570.hs:11:10: error: [GHC-53946]
+    • Illegal instance for a type synonym
+      A class instance must be for a class
+    • In the instance declaration for ‘SomeClassUnit’
+
+T22570.hs:15:10: error: [GHC-53946]
+    • Illegal instance for a type synonym
+      A class instance must be for a class
+    • In the instance declaration for ‘SomeClassSyn ()’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 8d3af674ab..a99792e5ab 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -665,3 +665,4 @@ test('MissingDefaultMethodBinding', normal, compile_fail, [''])
 test('T21447', normal, compile_fail, [''])
 test('T21530a', normal, compile_fail, [''])
 test('T21530b', normal, compile_fail, [''])
+test('T22570', normal, compile_fail, [''])