[Git][ghc/ghc][wip/T22570] checkValidInst: Don't expand synonyms when splitting sigma types

[Ryan Scott (@RyanGlScott)]

Ryan Scott pushed to branch wip/T22570 at Glasgow Haskell Compiler / GHC


Commits:
21a7d83f by Ryan Scott at 2022-12-13T06:32:59-05:00
checkValidInst: Don't expand synonyms when splitting sigma types

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 changed files:

- compiler/GHC/Tc/Validity.hs
- + testsuite/tests/typecheck/should_fail/T22570.hs
- + testsuite/tests/typecheck/should_fail/T22570.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~


=====================================
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 ()


=====================================
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 ()’


=====================================
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, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/21a7d83f6d48d970cb823730bc89561494d3e5af

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/21a7d83f6d48d970cb823730bc89561494d3e5af
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221213/c67ee23f/attachment-0001.html>