[Git][ghc/ghc][wip/T22570] checkValidInst: Don't expand synonyms when splitting sigma types
Ryan Scott (@RyanGlScott)
gitlab at gitlab.haskell.org
Sat Dec 10 02:21:15 UTC 2022
Ryan Scott pushed to branch wip/T22570 at Glasgow Haskell Compiler / GHC
Commits:
260b79d9 by Ryan Scott at 2022-12-09T21:04:06-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 `tcSplitSigmaTyNoView`, a version of `tcSplitSigmaTy`
that does _not_ expand type synonyms, and uses it in `checkValidInst`.
Fixes #22570.
- - - - -
5 changed files:
- compiler/GHC/Tc/Utils/TcType.hs
- 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/Utils/TcType.hs
=====================================
@@ -63,16 +63,19 @@ module GHC.Tc.Utils.TcType (
-- Splitters
getTyVar, getTyVar_maybe, getCastedTyVar_maybe,
tcSplitForAllTyVarBinder_maybe,
- tcSplitForAllTyVars, tcSplitForAllInvisTyVars, tcSplitSomeForAllTyVars,
+ tcSplitForAllTyVars,
+ tcSplitForAllInvisTyVars, tcSplitForAllInvisTyVarsNoView,
+ tcSplitSomeForAllTyVars, tcSplitSomeForAllTyVarsNoView,
tcSplitForAllReqTVBinders, tcSplitForAllInvisTVBinders,
tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBinders,
- tcSplitPhiTy, tcSplitPredFunTy_maybe,
+ tcSplitPhiTy, tcSplitPhiTyNoView,
+ tcSplitPredFunTy_maybe, tcSplitPredFunTyNoView_maybe,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
tcSplitFunTysN,
tcSplitTyConApp, tcSplitTyConApp_maybe,
tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitAppTyNoView_maybe,
- tcSplitSigmaTy, tcSplitNestedSigmaTys,
+ tcSplitSigmaTy, tcSplitSigmaTyNoView, tcSplitNestedSigmaTys,
---------------------------------
-- Predicates.
@@ -1373,6 +1376,10 @@ tcSplitForAllTyVars ty
tcSplitForAllInvisTyVars :: Type -> ([TyVar], Type)
tcSplitForAllInvisTyVars ty = tcSplitSomeForAllTyVars isInvisibleForAllTyFlag ty
+-- | Same as 'tcSplitForAllInvisTyVars' but without looking through synonyms.
+tcSplitForAllInvisTyVarsNoView :: Type -> ([TyVar], Type)
+tcSplitForAllInvisTyVarsNoView ty = tcSplitSomeForAllTyVarsNoView isInvisibleForAllTyFlag ty
+
-- | Like 'tcSplitForAllTyVars', but only splits a 'ForAllTy' if @argf_pred argf@
-- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
-- @argf_pred@ is a predicate over visibilities provided as an argument to this
@@ -1386,6 +1393,15 @@ tcSplitSomeForAllTyVars argf_pred ty
split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split orig_ty _ tvs = (reverse tvs, orig_ty)
+-- | Same as 'tcSplitSomeForAllTyVars' but without looking through synonyms.
+tcSplitSomeForAllTyVarsNoView :: (ForAllTyFlag -> Bool) -> Type -> ([TyVar], Type)
+tcSplitSomeForAllTyVarsNoView argf_pred ty
+ = split ty ty []
+ where
+ split _ (ForAllTy (Bndr tv argf) ty) tvs
+ | argf_pred argf = split ty ty (tv:tvs)
+ split orig_ty _ tvs = (reverse tvs, orig_ty)
+
-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Required' type
-- variable binders. All split tyvars are annotated with '()'.
tcSplitForAllReqTVBinders :: Type -> ([TcReqTVBinder], Type)
@@ -1413,6 +1429,14 @@ tcSplitPredFunTy_maybe (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
tcSplitPredFunTy_maybe _
= Nothing
+-- | Same as 'tcSplitPredFunTy_maybe' but without looking through synonyms.
+tcSplitPredFunTyNoView_maybe :: Type -> Maybe (PredType, Type)
+tcSplitPredFunTyNoView_maybe (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
+ | isInvisibleFunArg af
+ = Just (arg, res)
+tcSplitPredFunTyNoView_maybe _
+ = Nothing
+
tcSplitPhiTy :: Type -> (ThetaType, Type)
tcSplitPhiTy ty
= split ty []
@@ -1422,6 +1446,16 @@ tcSplitPhiTy ty
Just (pred, ty) -> split ty (pred:ts)
Nothing -> (reverse ts, ty)
+-- | Same as 'tcSplitPhiTy' but without looking through synonyms.
+tcSplitPhiTyNoView :: Type -> (ThetaType, Type)
+tcSplitPhiTyNoView ty
+ = split ty []
+ where
+ split ty ts
+ = case tcSplitPredFunTyNoView_maybe ty of
+ Just (pred, ty) -> split ty (pred:ts)
+ Nothing -> (reverse ts, ty)
+
-- | Split a sigma type into its parts. This only splits /invisible/ type
-- variable binders, as these are the only forms of binder that the typechecker
-- will implicitly instantiate.
@@ -1430,6 +1464,14 @@ tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
(tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
+-- | Same as 'tcSplitSigmaTy' but without looking through synonyms.
+tcSplitSigmaTyNoView :: Type -> ([TyVar], ThetaType, Type)
+tcSplitSigmaTyNoView ty =
+ case tcSplitForAllInvisTyVarsNoView ty of
+ (tvs, rho) ->
+ case tcSplitPhiTyNoView rho of
+ (theta, tau) -> (tvs, theta, tau)
+
-- | Split a sigma type into its parts, going underneath as many arrows
-- and foralls as possible. See Note [tcSplitNestedSigmaTys]
tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -1731,6 +1731,12 @@ 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 use tcSplitSigmaTyNoView rather than tcSplitSigmaTy
+when decomposing the type variable binders and instance context, as the latter
+looks through type synonyms. If we used the latter, then it could be possible
+to write an instance for a type synonym involving a quantified constraint
+(see #22570).
-}
checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
@@ -1774,7 +1780,7 @@ checkValidInstance ctxt hs_type ty = case tau of
; return () }
_ -> failWithTc (TcRnNoClassInstHead tau)
where
- (_tvs, theta, tau) = tcSplitSigmaTy ty
+ (_tvs, theta, tau) = tcSplitSigmaTyNoView ty
-- The location of the "head" of the instance
head_loc = getLoc (getLHsInstDeclHead hs_type)
=====================================
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/260b79d9768628ea14bc98caa5017fb49fca435a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/260b79d9768628ea14bc98caa5017fb49fca435a
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/20221209/a7967e80/attachment-0001.html>
More information about the ghc-commits
mailing list