[Git][ghc/ghc][wip/T25621] Delete validDerivPred in favor of instPredTerminates/checkInstTermination
Ryan Scott (@RyanGlScott)
gitlab at gitlab.haskell.org
Fri Jan 10 20:17:37 UTC 2025
Ryan Scott pushed to branch wip/T25621 at Glasgow Haskell Compiler / GHC
Commits:
61ec9613 by Ryan Scott at 2025-01-10T08:21:43-05:00
Delete validDerivPred in favor of instPredTerminates/checkInstTermination
In a previous commit, the functionality of `validDerivPred` was reduced to only
check for the Paterson conditions (i.e., termination). This is something which
the `checkInstTermination` function already checks for, however. As such,
`validDerivPred` is redundant.
This commit removes `validDerivPred`, splits out `instPredTerminates` (a pure
subset of `checkInstTermination` that can more-or-less be used as a drop-in
replacement for `validDerivPred`), and uses `instPredTerminates` in the places
it can be used.
- - - - -
4 changed files:
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Tc/Deriv/Infer.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Validity.hs
Changes:
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -1103,8 +1103,7 @@ tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
It is slightly odd to find the TyCons of a type. Especially since, via a type
family reduction or axiom, a type that doesn't mention T might start to mention T.
-This function is used in only three places:
-* In GHC.Tc.Validity.validDerivPred, when identifying "exotic" predicates.
+This function is used in only two places:
* In GHC.Tc.Errors.Ppr.pprTcSolverReportMsg, when trying to print a helpful
error about overlapping instances
* In utils/dump-decls/Main.hs, an ill-documented module.
=====================================
compiler/GHC/Tc/Deriv/Infer.hs
=====================================
@@ -29,7 +29,7 @@ import GHC.Tc.Utils.TcType
import GHC.Tc.Solver( pickQuantifiablePreds, simplifyTopImplic )
import GHC.Tc.Solver.Solve( solveWanteds )
import GHC.Tc.Solver.Monad ( runTcS )
-import GHC.Tc.Validity (checkValidTheta, validDerivPred)
+import GHC.Tc.Validity (checkValidTheta, instPredTerminates)
import GHC.Tc.Utils.Unify (buildImplicationFor)
import GHC.Tc.Zonk.TcType ( zonkWC )
import GHC.Tc.Zonk.Env ( ZonkFlexi(..), initZonkEnv )
@@ -820,7 +820,7 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
, ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs
, ds_skol_info = skol_info, ds_user_ctxt = user_ctxt })
= setSrcSpan loc $
- addErrCtxt (derivInstCtxt (mkClassPred clas inst_tys)) $
+ addErrCtxt (derivInstCtxt inst_head) $
do {
-- See [STEP DAC BUILD]
-- Generate the implication constraints, one for each method, to solve
@@ -850,8 +850,7 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
; let residual_simple = approximateWC False solved_wanteds
-- False: ignore any non-quantifiable constraints,
-- including equalities hidden under Given equalities
- head_size = pSizeClassPred clas inst_tys
- good = mapMaybeBag get_good residual_simple
+ good = mapMaybeBag get_good residual_simple
-- Returns @Just p@ (where @p@ is the type of the Ct) if a Ct
-- satisfies the Paterson conditions (and is therefore suitable to
@@ -859,8 +858,9 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
-- @Nothing@ otherwise. See Note [Valid 'deriving' predicate]
-- (Wrinkle: The Paterson conditions) in GHC.Tc.Validity.
get_good :: Ct -> Maybe PredType
- get_good ct | validDerivPred head_size p = Just p
- | otherwise = Nothing
+ get_good ct
+ | isNothing (instPredTerminates p inst_head) = Just p
+ | otherwise = Nothing
where p = ctPred ct
; traceTc "simplifyDeriv outputs" $
@@ -902,6 +902,8 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
-- See (B3) in Note [Valid 'deriving' predicate] in GHC.Tc.Validity.
; return min_theta }
+ where
+ inst_head = mkClassPred clas inst_tys
{-
Note [Overlap and deriving]
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -2223,7 +2223,7 @@ expand into anything else. They are:
For now we treat them as being size zero, but (#22696) I think we should
actually treat them as big (like any other ype family) because we don't
-want to abstract over them in e.g. validDerivPred.
+want to abstract over them.
The type-family termination test, in GHC.Tc.Validity.checkFamInstRhs, already
has a separate call to isStuckTypeFamily, so the `F` above will still be accepted.
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -12,7 +12,7 @@
module GHC.Tc.Validity (
Rank(..), UserTypeCtxt(..), checkValidType, checkValidMonoType,
checkValidTheta,
- checkValidInstance, checkValidInstHead, validDerivPred,
+ checkValidInstance, checkValidInstHead, instPredTerminates,
checkTySynRhs, checkEscapingKind,
checkValidCoAxiom, checkValidCoAxBranch,
checkFamPatBinders, checkTyFamEqnValidityInfo,
@@ -1879,11 +1879,10 @@ B3. Finally, the constraints are checked by `checkValidTheta`. This step differs
Also, in order to be absolutely sure that the inferred context will
terminate, GHC explicitly checks that the inferred context satisfies the
- Paterson conditions. This check is implemented in the `validDerivPred`
+ Paterson conditions. This check is implemented in the `instPredTerminates`
function. (See "Wrinkle: The Paterson conditions" below for more on this.)
- While `validDerivPred` is similar to other things defined in
- GHC.Tc.Deriv.Infer, we define it here in GHC.Tc.Validity because it is quite
- similar to `checkInstTermination`.
+ Note that `instPredTerminates` is the same function that powers
+ `checkInstTermination`.
--------------------------------------
-- Wrinkle: The Paterson conditions --
@@ -1940,25 +1939,6 @@ still need to be able to write instances for them ourselves. So we allow
instances only in the defining module.
-}
-validDerivPred :: PatersonSize -> PredType -> Bool
--- See Note [Valid 'deriving' predicate] (Wrinkle: The Paterson conditions)
-validDerivPred head_size pred
- = case classifyPredType pred of
- -- Equality constraints don't need to be checked in order to satisfy
- -- the Paterson conditions, so we simply return True here. (They are
- -- validity checked elsewhere in `approximateWC`, however.
- -- See Note [ApproximateWC] in GHC.Tc.Types.Constraint.)
- EqPred {} -> True
- -- Similarly, we don't need to check quantified constraints for
- -- Paterson condition purposes, so simply return True here. (It
- -- doesn't really matter what we return here, since `approximateWC`
- -- won't quantify over a quantified constraint anywya.)
- ForAllPred {} -> True
- ClassPred cls tys -> check_size (pSizeClassPred cls tys)
- IrredPred {} -> check_size (pSizeType pred)
- where
- check_size pred_size = isNothing (pred_size `ltPatersonSize` head_size)
-
{-
************************************************************************
* *
@@ -2108,10 +2088,39 @@ splitInstTyForValidity = split_context [] . drop_foralls
| isInvisibleFunArg af = split_context (pred:preds) tau
split_context preds ty = (reverse preds, ty)
+-- | @'checkInstTermation' theta head_pred@ checks if the instance context
+-- @theta@ satisfies the Paterson conditions (i.e., checks if it would
+-- terminate) if put into an instance of the form @instance theta => head_pred at .
+-- See @Note [Paterson conditions]@. If it doesn't satisfy the Paterson
+-- conditions, throw an error.
+--
+-- This function is like 'instPredTerminates', except that this function is
+-- monadic and works over an entire instance context instead of just a single
+-- instance constraint.
checkInstTermination :: ThetaType -> TcPredType -> TcM ()
--- See Note [Paterson conditions]
-checkInstTermination theta head_pred
- = check_preds emptyVarSet theta
+checkInstTermination theta head_pred =
+ let terminates :: PredType -> Maybe TcRnMessage
+ terminates theta_pred = instPredTerminates theta_pred head_pred
+
+ terminationErrors :: [Maybe TcRnMessage]
+ terminationErrors = map terminates theta
+
+ firstTerminationError :: Maybe TcRnMessage
+ firstTerminationError = asum terminationErrors in
+
+ case firstTerminationError of
+ Just err -> failWithTc err
+ Nothing -> pure ()
+
+-- | @'instPredTerminates' theta_pred head_pred@ checks if the instance
+-- constraint @theta_pred@ satisfies the Paterson conditions (i.e., checks if it
+-- would terminate) if put into an instance of the form
+-- @instance theta_pred => head_pred at . See @Note [Paterson conditions]@.
+-- If it does satisfy the Paterson conditions, return 'Nothing'. Otherwise,
+-- return @'Just' err@, where @err@ is the reason why it does not terminate.
+instPredTerminates :: PredType -> TcPredType -> Maybe TcRnMessage
+instPredTerminates theta_pred head_pred
+ = check emptyVarSet theta_pred
where
head_size = pSizeType head_pred
-- This is inconsistent and probably wrong. pSizeType does not filter out
@@ -2121,13 +2130,13 @@ checkInstTermination theta head_pred
-- for why I didn't change it. See Note [Invisible arguments and termination]
-- in GHC.Tc.Utils.TcType
- check_preds :: VarSet -> [PredType] -> TcM ()
- check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds
+ check_preds :: VarSet -> [PredType] -> Maybe TcRnMessage
+ check_preds foralld_tvs preds = asum $ map (check foralld_tvs) preds
- check :: VarSet -> PredType -> TcM ()
+ check :: VarSet -> PredType -> Maybe TcRnMessage
check foralld_tvs pred
= case classifyPredType pred of
- EqPred {} -> return () -- See #4200.
+ EqPred {} -> Nothing -- See #4200.
IrredPred {} -> check2 (pSizeTypeX foralld_tvs pred)
ClassPred cls tys
@@ -2145,8 +2154,8 @@ checkInstTermination theta head_pred
where
check2 pred_size
= case pred_size `ltPatersonSize` head_size of
- Just pc_failure -> failWithTc $ TcRnPatersonCondFailure pc_failure InInstanceDecl pred head_pred
- Nothing -> return ()
+ Just pc_failure -> Just $ TcRnPatersonCondFailure pc_failure InInstanceDecl pred head_pred
+ Nothing -> Nothing
{- Note [Instances and constraint synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/61ec961314e0438aac8dbf2e6878bc8618288925
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/61ec961314e0438aac8dbf2e6878bc8618288925
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/20250110/f2fc86ca/attachment-0001.html>
More information about the ghc-commits
mailing list