From aed1974e92366ab8e117734f308505684f70cddf Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@richarde.dev>
Date: Mon, 22 Nov 2021 17:34:32 -0500
Subject: [PATCH] Refactor the treatment of loopy superclass dicts
This patch completely re-engineers how we deal with loopy superclass
dictionaries in instance declarations. It fixes #20666 and #19690
The highlights are
* Recognise that the loopy-superclass business should use precisely
the Paterson conditions. This is much much nicer. See
Note [Recursive superclasses] in GHC.Tc.TyCl.Instance
* With that in mind, define "Paterson-smaller" in
Note [Paterson conditions] in GHC.Tc.Validity, and the new
data type `PatersonSize` in GHC.Tc.Utils.TcType, along with
functions to compute and compare PatsonSizes
* Use the new PatersonSize stuff when solving superclass constraints
See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
* In GHC.Tc.Solver.Monad.lookupInInerts, add a missing call to
prohibitedSuperClassSolve. This was the original cause of #20666.
* Treat (TypeError "stuff") as having PatersonSize zero. See
Note [Paterson size for type family applications] in GHC.Tc.Utils.TcType.
* Treat the head of a Wanted quantified constraint in the same way
as the superclass of an instance decl; this is what fixes #19690.
See GHC.Tc.Solver.Canonical Note [Solving a Wanted forall-constraint]
(Thanks to Matthew Craven for this insight.)
This entailed refactoring the GivenSc constructor of CtOrigin a bit,
to say whether it comes from an instance decl or quantified constraint.
* Some refactoring way in which redundant constraints are reported; we
don't want to complain about the extra, apparently-redundant
constraints that we must add to an instance decl because of the
loopy-superclass thing. I moved some work from GHC.Tc.Errors to
GHC.Tc.Solver.
* Add a new section to the user manual to describe the loopy
superclass issue and what rules it follows.
---
compiler/GHC/Core/InstEnv.hs | 4 +-
compiler/GHC/Core/TyCo/FVs.hs | 7 +-
compiler/GHC/Tc/Deriv.hs | 2 +-
compiler/GHC/Tc/Deriv/Infer.hs | 57 +-
compiler/GHC/Tc/Errors.hs | 31 +-
compiler/GHC/Tc/Errors/Ppr.hs | 25 +-
compiler/GHC/Tc/Gen/HsType.hs | 4 +-
compiler/GHC/Tc/Solver.hs | 80 ++-
compiler/GHC/Tc/Solver/Canonical.hs | 114 ++--
compiler/GHC/Tc/Solver/InertSet.hs | 17 +-
compiler/GHC/Tc/Solver/Interact.hs | 71 ++-
compiler/GHC/Tc/Solver/Monad.hs | 18 +-
compiler/GHC/Tc/TyCl/Instance.hs | 204 +++++---
compiler/GHC/Tc/Types/Constraint.hs | 5 +-
compiler/GHC/Tc/Types/Origin.hs | 127 +++--
compiler/GHC/Tc/Utils/Backpack.hs | 31 +-
compiler/GHC/Tc/Utils/Instantiate.hs | 26 +-
compiler/GHC/Tc/Utils/TcMType.hs | 4 +-
compiler/GHC/Tc/Utils/TcType.hs | 359 ++++++++++---
compiler/GHC/Tc/Utils/Unify.hs | 8 +-
compiler/GHC/Tc/Validity.hs | 485 ++++++++----------
docs/users_guide/exts/instances.rst | 104 +++-
.../tests/deriving/should_compile/T14339.hs | 14 +-
.../tests/deriving/should_fail/T21302.hs | 6 +
.../deriving/should_fail/T8165_fail2.stderr | 4 +-
testsuite/tests/impredicative/T17332.stderr | 4 +-
.../should_fail/NotRelaxedExamples.stderr | 11 +-
.../indexed-types/should_fail/T10817.stderr | 4 +-
.../indexed-types/should_fail/T13271.stderr | 7 -
.../indexed-types/should_fail/T15172.stderr | 2 +-
.../should_fail/TyFamUndec.stderr | 11 +-
.../tests/quantified-constraints/T19690.hs | 15 +
.../quantified-constraints/T19690.stderr | 16 +
.../quantified-constraints/T19921.stderr | 5 +-
.../quantified-constraints/T21006.stderr | 1 +
testsuite/tests/quantified-constraints/all.T | 1 +
.../typecheck/should_compile/T15473.stderr | 5 +-
.../abstract_refinement_hole_fits.stderr | 56 +-
.../constraint_hole_fits.stderr | 4 +-
.../refinement_hole_fits.stderr | 20 +-
.../tests/typecheck/should_fail/T14884.stderr | 10 +-
.../typecheck/should_fail/T15552a.stderr | 15 +-
.../tests/typecheck/should_fail/T15801.stderr | 1 +
.../tests/typecheck/should_fail/T20666.hs | 19 +
.../tests/typecheck/should_fail/T20666.stderr | 20 +
.../tests/typecheck/should_fail/T20666a.hs | 12 +
.../typecheck/should_fail/T20666a.stderr | 10 +
testsuite/tests/typecheck/should_fail/all.T | 2 +
.../typecheck/should_fail/fd-loop.stderr | 4 +-
.../typecheck/should_fail/tcfail108.stderr | 5 +-
.../tests/typecheck/should_fail/tcfail133.hs | 8 +-
.../typecheck/should_fail/tcfail133.stderr | 6 +-
.../typecheck/should_fail/tcfail154.stderr | 4 +-
.../typecheck/should_fail/tcfail214.stderr | 2 +-
54 files changed, 1293 insertions(+), 794 deletions(-)
create mode 100644 testsuite/tests/quantified-constraints/T19690.hs
create mode 100644 testsuite/tests/quantified-constraints/T19690.stderr
create mode 100644 testsuite/tests/typecheck/should_fail/T20666.hs
create mode 100644 testsuite/tests/typecheck/should_fail/T20666.stderr
create mode 100644 testsuite/tests/typecheck/should_fail/T20666a.hs
create mode 100644 testsuite/tests/typecheck/should_fail/T20666a.stderr
diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs
index bb7315074f72..f06f12e89a64 100644
--- a/compiler/GHC/Core/InstEnv.hs
+++ b/compiler/GHC/Core/InstEnv.hs
@@ -232,10 +232,8 @@ pprInstances ispecs = vcat (map pprInstance ispecs)
instanceHead :: ClsInst -> ([TyVar], Class, [Type])
-- Returns the head, using the fresh tyvars from the ClsInst
-instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun })
+instanceHead (ClsInst { is_tvs = tvs, is_cls = cls, is_tys = tys })
= (tvs, cls, tys)
- where
- (_, _, cls, _) = tcSplitDFunTy (idType dfun)
-- | Collects the names of concrete types and type constructors that make
-- up the head of a class instance. For instance, given `class Foo a b`:
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 3685876fa4c8..689503ef899d 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -31,7 +31,7 @@ module GHC.Core.TyCo.FVs
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
-- * Free type constructors
- tyConsOfType,
+ tyConsOfType, tyConsOfTypes,
-- * Free vars with visible/invisible separate
visVarsOfTypes, visVarsOfType,
@@ -1069,7 +1069,7 @@ tyConsOfType ty
go ty | Just ty' <- coreView ty = go ty'
go (TyVarTy {}) = emptyUniqSet
go (LitTy {}) = emptyUniqSet
- go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys
+ go (TyConApp tc tys) = go_tc tc `unionUniqSets` tyConsOfTypes tys
go (AppTy a b) = go a `unionUniqSets` go b
go (FunTy af w a b) = go w `unionUniqSets`
go a `unionUniqSets` go b
@@ -1108,12 +1108,13 @@ tyConsOfType ty
-- this last case can happen from the tyConsOfType used from
-- checkTauTvUpdate
- go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys
go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
go_tc tc = unitUniqSet tc
go_ax ax = go_tc $ coAxiomTyCon ax
+tyConsOfTypes :: [Type] -> UniqSet TyCon
+tyConsOfTypes tys = foldr (unionUniqSets . tyConsOfType) emptyUniqSet tys
{- **********************************************************************
* *
diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index 4917b21a7774..4d7bf81f6c99 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -28,7 +28,7 @@ import GHC.Tc.Deriv.Utils
import GHC.Tc.TyCl.Class( instDeclCtxt3, tcATDefault )
import GHC.Tc.Utils.Env
import GHC.Tc.Deriv.Generate
-import GHC.Tc.Validity( allDistinctTyVars, checkValidInstHead )
+import GHC.Tc.Validity( checkValidInstHead )
import GHC.Core.InstEnv
import GHC.Tc.Utils.Instantiate
import GHC.Core.FamInstEnv
diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs
index feba275d7524..e90811979fb8 100644
--- a/compiler/GHC/Tc/Deriv/Infer.hs
+++ b/compiler/GHC/Tc/Deriv/Infer.hs
@@ -51,7 +51,6 @@ import GHC.Utils.Misc
import GHC.Types.Basic
import GHC.Types.Var
-import GHC.Types.Var.Set
import GHC.Data.Bag
@@ -701,7 +700,7 @@ simplifyInstanceContexts infer_specs
current_solns infer_specs
; new_solns <- checkNoErrs $
extendLocalInstEnv inst_specs $
- mapM gen_soln infer_specs
+ mapM simplifyDeriv infer_specs
; if (current_solns `eqSolution` new_solns) then
return [ setDerivSpecTheta soln spec
@@ -713,24 +712,6 @@ simplifyInstanceContexts infer_specs
-- Canonicalise for comparison
-- See Note [Deterministic simplifyInstanceContexts]
canSolution = map (sortBy nonDetCmpType)
- ------------------------------------------------------------------
- gen_soln :: DerivSpec ThetaSpec -> TcM ThetaType
- gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
- , 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 the_pred) $
- do { theta <- simplifyDeriv skol_info user_ctxt tyvars deriv_rhs
- -- checkValidInstance tyvars theta clas inst_tys
- -- Not necessary; see Note [Exotic derived instance contexts]
-
- ; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr theta)
- -- Claim: the result instance declaration is guaranteed valid
- -- Hence no need to call:
- -- checkValidInstance tyvars theta clas inst_tys
- ; return theta }
- where
- the_pred = mkClassPred clas inst_tys
derivInstCtxt :: PredType -> SDoc
derivInstCtxt pred
@@ -744,29 +725,27 @@ derivInstCtxt pred
***********************************************************************************
-}
+
-- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much
-- as possible. Fail if not possible.
-simplifyDeriv :: SkolemInfo -- ^ The 'SkolemInfo' used to skolemise the
- -- 'TcTyVar' arguments
- -> UserTypeCtxt -- ^ Used to inform error messages as to whether
- -- we are in a @deriving@ clause or a standalone
- -- @deriving@ declaration
- -> [TcTyVar] -- ^ The tyvars bound by @inst_ty@.
- -> ThetaSpec -- ^ The constraints to solve and simplify
+simplifyDeriv :: DerivSpec ThetaSpec
-> TcM ThetaType -- ^ Needed constraints (after simplification),
-- i.e. @['PredType']@.
-simplifyDeriv skol_info user_ctxt tvs theta
- = do { let skol_set = mkVarSet tvs
-
+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)) $
+ do {
-- See [STEP DAC BUILD]
-- Generate the implication constraints, one for each method, to solve
-- with the skolemized variables. Start "one level down" because
-- we are going to wrap the result in an implication with tvs,
-- in step [DAC RESIDUAL]
- ; (tc_lvl, wanteds) <- captureThetaSpecConstraints user_ctxt theta
+ ; (tc_lvl, wanteds) <- captureThetaSpecConstraints user_ctxt deriv_rhs
; traceTc "simplifyDeriv inputs" $
- vcat [ pprTyVars tvs $$ ppr theta $$ ppr wanteds, ppr skol_info ]
+ vcat [ pprTyVars tvs $$ ppr deriv_rhs $$ ppr wanteds, ppr skol_info ]
-- See [STEP DAC SOLVE]
-- Simplify the constraints, starting at the same level at which
@@ -783,6 +762,7 @@ simplifyDeriv skol_info user_ctxt tvs theta
-- From the simplified constraints extract a subset 'good' that will
-- become the context 'min_theta' for the derived instance.
; let residual_simple = approximateWC True solved_wanteds
+ head_size = pSizeClassPred clas inst_tys
good = mapMaybeBag get_good residual_simple
-- Returns @Just p@ (where @p@ is the type of the Ct) if a Ct is
@@ -791,10 +771,8 @@ simplifyDeriv skol_info user_ctxt tvs theta
-- See Note [Exotic derived instance contexts] for what
-- constitutes an exotic constraint.
get_good :: Ct -> Maybe PredType
- get_good ct | validDerivPred skol_set p
- = Just p
- | otherwise
- = Nothing
+ get_good ct | validDerivPred head_size p = Just p
+ | otherwise = Nothing
where p = ctPred ct
; traceTc "simplifyDeriv outputs" $
@@ -824,6 +802,13 @@ simplifyDeriv skol_info user_ctxt tvs theta
-- in this line of code.
; simplifyTopImplic leftover_implic
+ ; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr min_theta)
+
+ -- Claim: the result instance declaration is guaranteed valid
+ -- Hence no need to call:
+ -- checkValidInstance tyvars theta clas inst_tys
+ -- See Note [Exotic derived instance contexts]
+
; return min_theta }
{-
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 61caa2e45633..c22ab6a2e59c 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -391,7 +391,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
warnRedundantConstraints :: SolverReportErrCtxt -> TcLclEnv -> SkolemInfoAnon -> [EvVar] -> TcM ()
-- See Note [Tracking redundant constraints] in GHC.Tc.Solver
-warnRedundantConstraints ctxt env info ev_vars
+warnRedundantConstraints ctxt env info redundant_evs
| null redundant_evs
= return ()
@@ -423,18 +423,6 @@ warnRedundantConstraints ctxt env info ev_vars
[]
; reportDiagnostic msg }
- redundant_evs =
- filterOut is_type_error $
- case info of -- See Note [Redundant constraints in instance decls]
- InstSkol -> filterOut (improving . idType) ev_vars
- _ -> ev_vars
-
- -- See #15232
- is_type_error = isJust . userTypeError_maybe . idType
-
- improving pred -- (transSuperClasses p) does not include p
- = any isImprovementPred (pred : transSuperClasses pred)
-
reportBadTelescope :: SolverReportErrCtxt -> TcLclEnv -> SkolemInfoAnon -> [TcTyVar] -> TcM ()
reportBadTelescope ctxt env (ForAllSkol telescope) skols
= do { msg <- mkErrorReport
@@ -449,23 +437,6 @@ reportBadTelescope ctxt env (ForAllSkol telescope) skols
reportBadTelescope _ _ skol_info skols
= pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols)
-{- Note [Redundant constraints in instance decls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For instance declarations, we don't report unused givens if
-they can give rise to improvement. Example (#10100):
- class Add a b ab | a b -> ab, a ab -> b
- instance Add Zero b b
- instance Add a b ab => Add (Succ a) b (Succ ab)
-The context (Add a b ab) for the instance is clearly unused in terms
-of evidence, since the dictionary has no fields. But it is still
-needed! With the context, a wanted constraint
- Add (Succ Zero) beta (Succ Zero)
-we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
-But without the context we won't find beta := Zero.
-
-This only matters in instance declarations..
--}
-
-- | Should we completely ignore this constraint in error reporting?
-- It *must* be the case that any constraint for which this returns True
-- somehow causes an error to be reported elsewhere.
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 8d18cad2a2fe..2e17295073d4 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -2618,7 +2618,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
-- Don't suggest fixes for the provided context of a pattern
-- synonym; the right fix is to bind more in the pattern
show_fixes (ctxtFixes has_ambigs pred implics
- ++ drv_fixes)
+ ++ drv_fixes ++ naked_sc_fixes)
, ppWhen (not (null candidates))
(hang (text "There are instances for similar types:")
2 (vcat (map ppr candidates)))
@@ -2689,7 +2689,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
StandAloneDerivOrigin -> [drv_fix True]
DerivOriginDC _ _ standalone -> [drv_fix standalone]
DerivOriginCoerce _ _ _ standalone -> [drv_fix standalone]
- _ -> []
+ _ -> []
drv_fix standalone_wildcard
| standalone_wildcard
@@ -2698,6 +2698,25 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
= hang (text "use a standalone 'deriving instance' declaration,")
2 (text "so you can specify the instance context yourself")
+ -- naked_sc_fix: try to produce a helpful error message for
+ -- superclass constraints caught by the subtleties described by
+ -- Note [Recursive superclasses] in GHC.TyCl.Instance
+ naked_sc_fixes
+ | ScOrigin _ NakedSc <- orig -- A superclass wanted with no instance decls used yet
+ , any non_tyvar_preds useful_givens -- Some non-tyvar givens
+ = [vcat [ text "If the constraint looks soluble from a superclass of the instance context,"
+ , text "read 'Undecidable instances and loopy superclasses' in the user manual" ]]
+ | otherwise = []
+
+ non_tyvar_preds :: UserGiven -> Bool
+ non_tyvar_preds = any non_tyvar_pred . ic_given
+
+ non_tyvar_pred :: EvVar -> Bool
+ -- Tells if the Given is of form (C ty1 .. tyn), where the tys are not all tyvars
+ non_tyvar_pred given = case getClassPredTys_maybe (idType given) of
+ Just (_, tys) -> not (all isTyVarTy tys)
+ Nothing -> False
+
pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item matches unifiers) =
vcat
[ addArising ct_loc $
@@ -3529,7 +3548,7 @@ show_fixes (f:fs) = sep [ text "Possible fix:"
ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
ctxtFixes has_ambig_tvs pred implics
| not has_ambig_tvs
- , isTyVarClassPred pred
+ , isTyVarClassPred pred -- Don't suggest adding (Eq T) to the context, say
, (skol:skols) <- usefulContext implics pred
, let what | null skols
, SigSkol (PatSynCtxt {}) _ _ <- skol
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 0ea041233986..bf15393048ab 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -664,7 +664,9 @@ tcDerivStrategy mb_lds
tc_deriv_strategy (NewtypeStrategy _) = boring_case (NewtypeStrategy noExtField)
tc_deriv_strategy (ViaStrategy hs_sig)
= do { ty <- tcTopLHsType DerivClauseCtxt hs_sig
- ; rec { (via_tvs, via_pred) <- tcSkolemiseInvisibleBndrs (DerivSkol via_pred) ty}
+ -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ ; rec { (via_tvs, via_pred) <- tcSkolemiseInvisibleBndrs (DerivSkol via_pred) ty }
; pure (ViaStrategy via_pred, via_tvs) }
boring_case :: ds -> TcM (ds, [a])
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index cdc15959f8b8..6fc5b28ab0df 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -73,7 +73,7 @@ import Control.Monad
import Data.Foldable ( toList )
import Data.List ( partition )
import Data.List.NonEmpty ( NonEmpty(..) )
-import GHC.Data.Maybe ( mapMaybe )
+import GHC.Data.Maybe ( mapMaybe, isJust )
{-
*********************************************************************************
@@ -1199,10 +1199,12 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
-- NB: bound_theta are constraints we want to quantify over,
-- including the psig_theta, which we always quantify over
-- NB: bound_theta are fully zonked
+ -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
; rec { (qtvs, bound_theta, co_vars) <- decideQuantification skol_info infer_mode rhs_tclvl
name_taus partial_sigs
quant_pred_candidates
- ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
+ ; 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)
@@ -2490,18 +2492,7 @@ setImplicationStatus implic@(Implic { ic_status = status
; bad_telescope <- checkBadTelescope implic
- ; let (used_givens, unused_givens)
- | warnRedundantGivens info
- = partition (`elemVarSet` need_inner) givens
- | otherwise = (givens, []) -- None to report
-
- minimal_used_givens = mkMinimalBySCs evVarPred used_givens
- is_minimal = (`elemVarSet` mkVarSet minimal_used_givens)
-
- warn_givens
- | not (null unused_givens) = unused_givens
- | warnRedundantGivens info = filterOut is_minimal used_givens
- | otherwise = []
+ ; let warn_givens = findUnnecessaryGivens info need_inner givens
discard_entire_implication -- Can we discard the entire implication?
= null warn_givens -- No warning from this implication
@@ -2541,6 +2532,67 @@ setImplicationStatus implic@(Implic { ic_status = status
| otherwise
= True -- Otherwise, keep it
+findUnnecessaryGivens :: SkolemInfoAnon -> VarSet -> [EvVar] -> [EvVar]
+findUnnecessaryGivens info need_inner givens
+ | not (warnRedundantGivens info) -- Don't report redundant constraints at all
+ = []
+
+ | not (null unused_givens) -- Some givens are literally unused
+ = unused_givens
+
+ | otherwise -- All givens are used, but some might
+ = redundant_givens -- still be redundant e.g. (Eq a, Ord a)
+
+ where
+ in_instance_decl = case info of { InstSkol {} -> True; _ -> False }
+ -- See Note [Redundant constraints in instance decls]
+
+ unused_givens = filterOut is_used givens
+
+ is_used given = is_type_error given
+ || (given `elemVarSet` need_inner)
+ || (in_instance_decl && is_improving (idType given))
+
+ minimal_givens = mkMinimalBySCs evVarPred givens
+ is_minimal = (`elemVarSet` mkVarSet minimal_givens)
+ redundant_givens
+ | in_instance_decl = []
+ | otherwise = filterOut is_minimal givens
+
+ -- See #15232
+ is_type_error = isJust . userTypeError_maybe . idType
+
+ is_improving pred -- (transSuperClasses p) does not include p
+ = any isImprovementPred (pred : transSuperClasses pred)
+
+{- Note [Redundant constraints in instance decls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Instance declarations are special in two ways:
+
+* We don't report unused givens if they can give rise to improvement.
+ Example (#10100):
+ class Add a b ab | a b -> ab, a ab -> b
+ instance Add Zero b b
+ instance Add a b ab => Add (Succ a) b (Succ ab)
+ The context (Add a b ab) for the instance is clearly unused in terms
+ of evidence, since the dictionary has no fields. But it is still
+ needed! With the context, a wanted constraint
+ Add (Succ Zero) beta (Succ Zero)
+ we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
+ But without the context we won't find beta := Zero.
+
+ This only matters in instance declarations.
+
+* We don't report givens that are a superclass of another given. E.g.
+ class Ord r => UserOfRegs r a where ...
+ instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
+ The (Ord r) is not redundant, even though it is a superclass of
+ (UserOfRegs r CmmReg). See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.
+
+ Again this is specific to instance declarations.
+-}
+
+
checkBadTelescope :: Implication -> TcS Bool
-- True <=> the skolems form a bad telescope
-- See Note [Checking telescopes] in GHC.Tc.Types.Constraint
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 33ee8e854c8c..02ce8115ad71 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -1,6 +1,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE RecursiveDo #-}
module GHC.Tc.Solver.Canonical(
canonicalize,
@@ -530,7 +531,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
classSCSelIds cls
where
dict_ids = mkTemplateLocals theta
- size = sizeTypes tys
+ this_size = pSizeClassPred cls tys
do_one_given sel_id
| isUnliftedType sc_pred
@@ -570,37 +571,38 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
`App` (evId evar `mkVarApps` (tvs ++ dict_ids))
`mkVarApps` sc_tvs
- sc_loc
- | isCTupleClass cls
- = loc -- For tuple predicates, just take them apart, without
- -- adding their (large) size into the chain. When we
- -- get down to a base predicate, we'll include its size.
- -- #10335
-
- | isEqPredClass cls
- || cls `hasKey` coercibleTyConKey
- = loc -- The only superclasses of ~, ~~, and Coercible are primitive
- -- equalities, and they don't use the InstSCOrigin mechanism
- -- detailed in Note [Solving superclass constraints] in
- -- GHC.Tc.TyCl.Instance. Skip for a tiny performance win.
-
- -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
- -- for explanation of InstSCOrigin and Note [Replacement vs keeping] in
- -- GHC.Tc.Solver.Interact for why we need OtherSCOrigin and depths
- | otherwise
- = loc { ctl_origin = new_orig }
- where
- new_orig = case ctLocOrigin loc of
- -- these cases are when we have something that's already a superclass constraint
- InstSCOrigin sc_depth n -> InstSCOrigin (sc_depth + 1) (n `max` size)
- OtherSCOrigin sc_depth si -> OtherSCOrigin (sc_depth + 1) si
-
- -- these cases do not already have a superclass constraint: depth starts at 1
- GivenOrigin InstSkol -> InstSCOrigin 1 size
- GivenOrigin other_skol -> OtherSCOrigin 1 other_skol
-
- other_orig -> pprPanic "Given constraint without given origin" $
- ppr evar $$ ppr other_orig
+ sc_loc | isCTupleClass cls
+ = loc -- For tuple predicates, just take them apart, without
+ -- adding their (large) size into the chain. When we
+ -- get down to a base predicate, we'll include its size.
+ -- #10335
+
+ | isEqPredClass cls || cls `hasKey` coercibleTyConKey
+ = loc -- The only superclasses of ~, ~~, and Coercible are primitive
+ -- equalities, and they don't use the GivenSCOrigin mechanism
+ -- detailed in Note [Solving superclass constraints] in
+ -- GHC.Tc.TyCl.Instance. Skip for a tiny performance win.
+
+ | otherwise
+ = loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }
+
+ -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+ -- for explanation of GivenSCOrigin and Note [Replacement vs keeping] in
+ -- GHC.Tc.Solver.Interact for why we need depths
+ mk_sc_origin :: CtOrigin -> CtOrigin
+ mk_sc_origin (GivenSCOrigin skol_info sc_depth already_blocked)
+ = GivenSCOrigin skol_info (sc_depth + 1)
+ (already_blocked || newly_blocked skol_info)
+
+ mk_sc_origin (GivenOrigin skol_info)
+ = -- These cases do not already have a superclass constraint: depth starts at 1
+ GivenSCOrigin skol_info 1 (newly_blocked skol_info)
+
+ mk_sc_origin other_orig = pprPanic "Given constraint without given origin" $
+ ppr evar $$ ppr other_orig
+
+ newly_blocked (InstSkol _ head_size) = isJust (this_size `ltPatersonSize` head_size)
+ newly_blocked _ = False
mk_strict_superclasses rec_clss ev tvs theta cls tys
| all noFreeVarsOfType tys
@@ -861,16 +863,27 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
-- This setLclEnv is important: the emitImplicationTcS uses that
-- TcLclEnv for the implication, and that in turn sets the location
-- for the Givens when solving the constraint (#21006)
- do { skol_info <- mkSkolemInfo QuantCtxtSkol
- ; let empty_subst = mkEmptySubst $ mkInScopeSet $
+ do { let empty_subst = mkEmptySubst $ mkInScopeSet $
tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
- ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
- ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
-
+ is_qc = IsQC (ctLocOrigin loc)
+
+ -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ -- Very like the code in tcSkolDFunType
+ ; rec { skol_info <- mkSkolemInfo skol_info_anon
+ ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
+ ; let inst_pred = substTy subst pred
+ inst_theta = substTheta subst theta
+ skol_info_anon = InstSkol is_qc (get_size inst_pred) }
+
+ ; given_ev_vars <- mapM newEvVar inst_theta
; (lvl, (w_id, wanteds))
<- pushLevelNoWorkList (ppr skol_info) $
- do { wanted_ev <- newWantedEvVarNC loc rewriters $
- substTy subst pred
+ do { let loc' = setCtLocOrigin loc (ScOrigin is_qc NakedSc)
+ -- Set the thing to prove to have a ScOrigin, so we are
+ -- careful about its termination checks.
+ -- See (QC-INV) in Note [Solving a Wanted forall-constraint]
+ ; wanted_ev <- newWantedEvVarNC loc' rewriters inst_pred
; return ( ctEvEvId wanted_ev
, unitBag (mkNonCanonical wanted_ev)) }
@@ -882,6 +895,12 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
, et_binds = ev_binds, et_body = w_id }
; stopWith ev "Wanted forall-constraint" }
+ where
+ -- Getting the size of the head is a bit horrible
+ -- because of the special treament for class predicates
+ get_size pred = case classifyPredType pred of
+ ClassPred cls tys -> pSizeClassPred cls tys
+ _ -> pSizeType pred
-- See Note [Solving a Given forall-constraint]
solveForAll ev@(CtGiven {}) tvs _theta pred pend_sc
@@ -902,6 +921,23 @@ and discharge df thus:
where <binds> is filled in by solving the implication constraint.
All the machinery is to hand; there is little to do.
+The tricky point is about termination: see #19690. We want to maintain
+the invariant (QC-INV):
+
+ (QC-INV) Every quantified constraint returns a non-bottom dictionary
+
+just as every top-level instance declaration guarantees to return a non-bottom
+dictionary. But as #19690 shows, it is possible to get a bottom dicionary
+by superclass selection if we aren't careful. The situation is very similar
+to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance;
+and we use the same solution:
+
+* Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size))
+* Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc)
+
+Both of these things are done in solveForAll. Now the mechanism described
+in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over.
+
Note [Solving a Given forall-constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For a Given constraint
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index b3dcb3f5b176..5dc3431b9a7b 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -1633,12 +1633,17 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
= False
can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv
-prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
--- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-prohibitedSuperClassSolve from_loc solve_loc
- | InstSCOrigin _ given_size <- ctLocOrigin from_loc
- , ScOrigin wanted_size <- ctLocOrigin solve_loc
- = given_size >= wanted_size
+prohibitedSuperClassSolve :: CtLoc -- ^ is it loopy to use this one ...
+ -> CtLoc -- ^ ... to solve this one?
+ -> Bool -- ^ True ==> don't solve it
+-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2)
+prohibitedSuperClassSolve given_loc wanted_loc
+ | GivenSCOrigin _ _ blocked <- ctLocOrigin given_loc
+ , blocked
+ , ScOrigin _ NakedSc <- ctLocOrigin wanted_loc
+ = True -- Prohibited if the Wanted is a superclass
+ -- and the Given has come via a superclass selection from
+ -- a predicate bigger than the head
| otherwise
= False
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index c3aa2d2695cd..e69e7ae0feb9 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -6,8 +6,7 @@ module GHC.Tc.Solver.Interact (
) where
import GHC.Prelude
-import GHC.Types.Basic ( SwapFlag(..),
- infinity, IntWithInf, intGtLimit )
+import GHC.Types.Basic ( SwapFlag(..), IntWithInf, intGtLimit )
import GHC.Tc.Solver.Canonical
import GHC.Types.Var.Set
@@ -520,17 +519,18 @@ solveOneFromTheOther ct_i ct_w
pred = ctEvPred ev_i
- loc_i = ctEvLoc ev_i
- loc_w = ctEvLoc ev_w
- lvl_i = ctLocLevel loc_i
- lvl_w = ctLocLevel loc_w
+ loc_i = ctEvLoc ev_i
+ loc_w = ctEvLoc ev_w
+ orig_i = ctLocOrigin loc_i
+ orig_w = ctLocOrigin loc_w
+ lvl_i = ctLocLevel loc_i
+ lvl_w = ctLocLevel loc_w
is_psc_w = isPendingScDict ct_w
is_psc_i = isPendingScDict ct_i
- is_wsc_orig_i = is_wanted_superclass_loc loc_i
- is_wsc_orig_w = is_wanted_superclass_loc loc_w
- is_wanted_superclass_loc = isWantedSuperclassOrigin . ctLocOrigin
+ is_wsc_orig_i = isWantedSuperclassOrigin orig_i
+ is_wsc_orig_w = isWantedSuperclassOrigin orig_w
different_level_strategy -- Both Given
| isIPLikePred pred = if lvl_w > lvl_i then KeepWork else KeepInert
@@ -539,27 +539,20 @@ solveOneFromTheOther ct_i ct_w
-- For the isIPLikePred case see Note [Shadowing of Implicit Parameters]
same_level_strategy -- Both Given
- = case (ctLocOrigin loc_i, ctLocOrigin loc_w) of
- -- case 2(a) from Note [Replacement vs keeping]
- (InstSCOrigin _depth_i size_i, InstSCOrigin _depth_w size_w)
- | size_w < size_i -> KeepWork
- | otherwise -> KeepInert
+ = case (orig_i, orig_w) of
- -- case 2(c) from Note [Replacement vs keeping]
- (InstSCOrigin depth_i _, OtherSCOrigin depth_w _) -> choose_shallower depth_i depth_w
- (OtherSCOrigin depth_i _, InstSCOrigin depth_w _) -> choose_shallower depth_i depth_w
- (OtherSCOrigin depth_i _, OtherSCOrigin depth_w _) -> choose_shallower depth_i depth_w
+ (GivenSCOrigin _ depth_i blocked_i, GivenSCOrigin _ depth_w blocked_w)
+ | blocked_i, not blocked_w -> KeepWork -- Case 2(a) from
+ | not blocked_i, blocked_w -> KeepInert -- Note [Replacement vs keeping]
- -- case 2(b) from Note [Replacement vs keeping]
- (InstSCOrigin {}, _) -> KeepWork
- (OtherSCOrigin {}, _) -> KeepWork
+ -- Both blocked or both not blocked
- -- case 2(d) from Note [Replacement vs keeping]
- _ -> KeepInert
+ | depth_w < depth_i -> KeepWork -- Case 2(c) from
+ | otherwise -> KeepInert -- Note [Replacement vs keeping]
- choose_shallower depth_i depth_w | depth_w < depth_i = KeepWork
- | otherwise = KeepInert
- -- favor KeepInert in the equals case, according to 2(d) from the Note
+ (GivenSCOrigin {}, _) -> KeepWork -- Case 2(b) from Note [Replacement vs keeping]
+
+ _ -> KeepInert -- Case 2(d) from Note [Replacement vs keeping]
{-
Note [Replacement vs keeping]
@@ -585,7 +578,7 @@ solveOneFromTheOther.
2) Constraints coming from the same level (i.e. same implication)
- (a) If both are InstSCOrigin, choose the one with the smallest TypeSize,
+ (a) If both are GivenSCOrigin, choose the one that is unblocked if possible
according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
(b) Prefer constraints that are not superclass selections. Example:
@@ -601,11 +594,12 @@ solveOneFromTheOther.
Getting this wrong was #20602. See also
Note [Tracking redundant constraints] in GHC.Tc.Solver.
- (c) If both are superclass selections (but not both InstSCOrigin), choose the one
- with the shallower superclass-selection depth, in the hope of identifying
- more correct redundant constraints. This is really a generalization of
- point (b), because the superclass depth of a non-superclass
- constraint is 0.
+ (c) If both are GivenSCOrigin, chooose the one with the shallower
+ superclass-selection depth, in the hope of identifying more correct
+ redundant constraints. This is really a generalization of point (b),
+ because the superclass depth of a non-superclass constraint is 0.
+
+ (If the levels differ, we definitely won't have both with GivenSCOrigin.)
(d) Finally, when there is still a choice, use KeepInert rather than
KeepWork, for two reasons:
@@ -669,7 +663,10 @@ interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
-- See Note [Multiple matching irreds]
, let ev_i = ctEvidence ct_i
= do { what_next <- solveOneFromTheOther ct_i ct_w
- ; traceTcS "iteractIrred" (ppr ct_w $$ ppr what_next $$ ppr ct_i)
+ ; traceTcS "iteractIrred" $
+ vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
+ , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i))
+ , ppr what_next ]
; case what_next of
KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
@@ -2326,9 +2323,11 @@ checkInstanceOK loc what pred
origin = ctLocOrigin loc
zap_origin loc -- After applying an instance we can set ScOrigin to
- -- infinity, so that prohibitedSuperClassSolve never fires
- | ScOrigin {} <- origin
- = setCtLocOrigin loc (ScOrigin infinity)
+ -- NotNakedSc, so that prohibitedSuperClassSolve never fires
+ -- See Note [Solving superclass constraints] in
+ -- GHC.Tc.TyCl.Instance, (sc1).
+ | ScOrigin what _ <- origin
+ = setCtLocOrigin loc (ScOrigin what NotNakedSc)
| otherwise
= loc
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 67c90dcd8069..b5cf81ad9d5b 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -672,8 +672,16 @@ lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts loc pty
| ClassPred cls tys <- classifyPredType pty
= do { inerts <- getTcSInerts
- ; return (lookupSolvedDict inerts loc cls tys `mplus`
- fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)) }
+ ; return $ -- Maybe monad
+ do { found_ev <-
+ lookupSolvedDict inerts loc cls tys `mplus`
+ fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)
+ ; guard (not (prohibitedSuperClassSolve (ctEvLoc found_ev) loc))
+ -- We're about to "solve" the wanted we're looking up, so we
+ -- must make sure doing so wouldn't run afoul of
+ -- Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
+ -- Forgetting this led to #20666.
+ ; return found_ev }}
| otherwise -- NB: No caching for equalities, IPs, holes, or errors
= return Nothing
@@ -783,7 +791,11 @@ data TcSEnv
}
---------------
-newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } deriving (Functor)
+newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
+ deriving (Functor)
+
+instance MonadFix TcS where
+ mfix k = TcS $ \env -> mfix (\x -> unTcS (k x) env)
-- | Smart constructor for 'TcS', as describe in Note [The one-shot state
-- monad trick] in "GHC.Utils.Monad".
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 6fda868642c9..3d9b5dd550d7 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -490,7 +490,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
do { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty
; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty
-- NB: tcHsClsInstType does checkValidInstance
- ; skol_info <- mkSkolemInfo InstSkol
+ ; skol_info <- mkSkolemInfo (mkClsInstSkol clas inst_tys)
; (subst, skol_tvs) <- tcInstSkolTyVars skol_info tyvars
; let tv_skol_prs = [ (tyVarName tv, skol_tv)
| (tv, skol_tv) <- tyvars `zip` skol_tvs ]
@@ -1228,19 +1228,14 @@ the default method Ids replete with their INLINE pragmas. Urk.
tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc)
-- Returns a binding for the dfun
tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
- = recoverM (return emptyLHsBinds) $
- setSrcSpan loc $
- addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
+ = recoverM (return emptyLHsBinds) $
+ setSrcSpan loc $
+ addErrCtxt (instDeclCtxt2 dfun_ty) $
do { -- Instantiate the instance decl with skolem constants
- ; skol_info <- mkSkolemInfo InstSkol
- ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType skol_info dfun_id
+ (skol_info, inst_tyvars, dfun_theta, clas, inst_tys) <- tcSkolDFunType dfun_ty
; dfun_ev_vars <- newEvVars dfun_theta
- -- We instantiate the dfun_id with superSkolems.
- -- See Note [Subtle interaction of recursion and overlap]
- -- and Note [Binding when looking up instances]
- ; let (clas, inst_tys) = tcSplitDFunHead inst_head
- (class_tyvars, sc_theta, _, op_items) = classBigSig clas
+ ; let (class_tyvars, sc_theta, _, op_items) = classBigSig clas
sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
; traceTc "tcInstDecl2" (vcat [ppr inst_tyvars, ppr inst_tys, ppr dfun_theta, ppr sc_theta'])
@@ -1256,13 +1251,12 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics))
<- pushTcLevelM $
do { (sc_ids, sc_binds, sc_implics)
- <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
- inst_tys dfun_ev_binds
- sc_theta'
+ <- tcSuperClasses skol_info dfun_id clas inst_tyvars
+ dfun_ev_vars dfun_ev_binds sc_theta'
-- Typecheck the methods
; (meth_ids, meth_binds, meth_implics)
- <- tcMethods dfun_id clas inst_tyvars dfun_ev_vars
+ <- tcMethods skol_info dfun_id clas inst_tyvars dfun_ev_vars
inst_tys dfun_ev_binds spec_inst_info
op_items ibinds
@@ -1277,7 +1271,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
, ic_given = dfun_ev_vars
, ic_wanted = mkImplicWC sc_meth_implics
, ic_binds = dfun_ev_binds_var
- , ic_info = InstSkol }
+ , ic_info = skol_info }
-- Create the result bindings
; self_dict <- newDict clas inst_tys
@@ -1335,6 +1329,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
}
where
dfun_id = instanceDFunId ispec
+ dfun_ty = idType dfun_id
loc = getSrcSpan dfun_id
addDFunPrags :: DFunId -> [Id] -> DFunId
@@ -1442,7 +1437,8 @@ Notice that
************************************************************************
-}
-tcSuperClasses :: DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
+tcSuperClasses :: SkolemInfoAnon -> DFunId -> Class -> [TcTyVar]
+ -> [EvVar]
-> TcEvBinds
-> TcThetaType
-> TcM ([EvVar], LHsBinds GhcTc, Bag Implication)
@@ -1454,15 +1450,16 @@ tcSuperClasses :: DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
-- See Note [Recursive superclasses] for why this is so hard!
-- In effect, we build a special-purpose solver for the first step
-- of solving each superclass constraint
-tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
+tcSuperClasses skol_info dfun_id cls tyvars dfun_evs dfun_ev_binds sc_theta
= do { (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
; return (ids, listToBag binds, listToBag implics) }
where
loc = getSrcSpan dfun_id
- size = sizeTypes inst_tys
tc_super (sc_pred, n)
= do { (sc_implic, ev_binds_var, sc_ev_tm)
- <- checkInstConstraints $ emitWanted (ScOrigin size) sc_pred
+ <- checkInstConstraints skol_info $
+ emitWanted (ScOrigin IsClsInst NakedSc) sc_pred
+ -- ScOrigin IsClsInst True: see Note [Solving superclass constraints]
; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
; sc_ev_id <- newEvVar sc_pred
@@ -1484,10 +1481,10 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
; return (sc_top_id, L (noAnnSrcSpan loc) bind, sc_implic) }
-------------------
-checkInstConstraints :: TcM result
+checkInstConstraints :: SkolemInfoAnon -> TcM result
-> TcM (Implication, EvBindsVar, result)
-- See Note [Typechecking plan for instance declarations]
-checkInstConstraints thing_inside
+checkInstConstraints skol_info thing_inside
= do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints $
thing_inside
@@ -1496,7 +1493,7 @@ checkInstConstraints thing_inside
; let implic' = implic { ic_tclvl = tclvl
, ic_wanted = wanted
, ic_binds = ev_binds_var
- , ic_info = InstSkol }
+ , ic_info = skol_info }
; return (implic', ev_binds_var, result) }
@@ -1549,82 +1546,120 @@ definition. More precisely:
To achieve the Superclass Invariant, in a dfun definition we can
generate a guaranteed-non-bottom superclass witness from:
(sc1) one of the dictionary arguments itself (all non-bottom)
- (sc2) an immediate superclass of a smaller dictionary
+ (sc2) an immediate superclass of a non-bottom dictionary that is
+ /Paterson-smaller/ than the instance head
+ See Note [The PatersonSize of a type] in GHC.Tc.Utils.TcType
(sc3) a call of a dfun (always returns a dictionary constructor)
-The tricky case is (sc2). We proceed by induction on the size of
-the (type of) the dictionary, defined by GHC.Tc.Validity.sizeTypes.
-Let's suppose we are building a dictionary of size 3, and
-suppose the Superclass Invariant holds of smaller dictionaries.
-Then if we have a smaller dictionary, its immediate superclasses
-will be non-bottom by induction.
+The tricky case is (sc2). We proceed by induction on the size of the
+(type of) the dictionary, defined by GHC.Tc.Utils.TcType.pSizeType. Let's
+suppose we are building a dictionary of size 3 (the "head"), and suppose
+the Superclass Invariant holds of smaller dictionaries. Then if we have a
+smaller dictionary, its immediate superclasses will be non-bottom by
+induction.
+
+Why "Paterson-smaller"? See Note [Paterson conditions] in GHC.Tc.Validity.
+We want to be sure that the superclass dictionary is smaller /for any
+ground instatiation/ of the instance, so we need to account for type
+variables that occur more than once, and for type families (#20666). And
+that's exactly what the Paterson conditions check!
-What does "we have a smaller dictionary" mean? It might be
-one of the arguments of the instance, or one of its superclasses.
Here is an example, taken from CmmExpr:
class Ord r => UserOfRegs r a where ...
(i1) instance UserOfRegs r a => UserOfRegs r (Maybe a) where
(i2) instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
-For (i1) we can get the (Ord r) superclass by selection from (UserOfRegs r a),
-since it is smaller than the thing we are building (UserOfRegs r (Maybe a).
+For (i1) we can get the (Ord r) superclass by selection from
+(UserOfRegs r a), since it (i.e. UserOfRegs r a) is smaller than the
+thing we are building, namely (UserOfRegs r (Maybe a)).
-But for (i2) that isn't the case, so we must add an explicit, and
-perhaps surprising, (Ord r) argument to the instance declaration.
+But for (i2) that isn't the case: (UserOfRegs r CmmReg) is not smaller
+than the thing we are building (UserOfRegs r CmmExpr), so we can't use
+the superclasses of the former. Hence we must instead add an explicit,
+and perhaps surprising, (Ord r) argument to the instance declaration.
Here's another example from #6161:
- class Super a => Duper a where ...
- class Duper (Fam a) => Foo a where ...
-(i3) instance Foo a => Duper (Fam a) where ...
-(i4) instance Foo Float where ...
+ class Super a => Duper a where ...
+ class Duper (Maybe a) => Foo a where ...
+(i3) instance Foo a => Duper (Maybe a) where ...
+(i4) instance Foo Float where ...
It would be horribly wrong to define
- dfDuperFam :: Foo a -> Duper (Fam a) -- from (i3)
- dfDuperFam d = MkDuper (sc_sel1 (sc_sel2 d)) ...
+ dfDuperMaybe :: Foo a -> Duper (Maybe a) -- from (i3)
+ dfDuperMaybe d = MkDuper (sc_sel1 (sc_sel2 d)) ...
dfFooFloat :: Foo Float -- from (i4)
- dfFooFloat = MkFoo (dfDuperFam dfFooFloat) ...
-
-Now the Super superclass of Duper is definitely bottom!
-
-This won't happen because when processing (i3) we can use the
-superclasses of (Foo a), which is smaller, namely Duper (Fam a). But
-that is *not* smaller than the target so we can't take *its*
-superclasses. As a result the program is rightly rejected, unless you
-add (Super (Fam a)) to the context of (i3).
+ dfFooFloat = MkFoo (dfDuperMaybe dfFooFloat) ...
+
+Let's expand the RHS of dfFooFloat:
+ dfFooFloat = MkFoo (MkDuper (sc_sel1 (sc_sel2 dfFooFloat)) ...) ...
+That superclass argument to MkDuper is bottom!
+
+This program gets rejected because:
+* When processing (i3) we need to construct a dictionary for Super
+ (Maybe a), to put in the superclass field of (Duper (Maybe a)).
+* We /can/ use the superclasses of (Foo a), because the latter is
+ smaller than the head of the instance, namely Duper (Maybe a).
+* So we know (by (sc2)) that this Duper (Maybe a) dictionary is
+ non-bottom. But because (Duper (Maybe a)) is not smaller than the
+ instance head (Duper (Maybe a)), we can't take *its* superclasses.
+As a result the program is rightly rejected, unless you add
+(Super (Maybe a)) to the context of (i3).
+
+Wrinkle (W1):
+ (sc2) says we only get a non-bottom dict if the dict we are
+ selecting from is itself non-bottom. So in a superclass chain,
+ all the dictionaries in the chain must be non-bottom.
+ class C a => D3 a
+ class D2 a [[Maybe b]] => D1 a b
+ class D3 a => D2 a b
+ class C a => E a b
+ instance D1 a b => E a [b]
+ The instance needs the wanted superclass (C a). We can get it
+ by superclass selection from
+ D1 a b --> D2 a [[Maybe b]] --> D3 a --> C a
+ But on the way we go through the too-big (D2 a [[Maybe b]]), and
+ we don't know that is non-bottom.
Note [Solving superclass constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-How do we ensure that every superclass witness is generated by
-one of (sc1) (sc2) or (sc3) in Note [Recursive superclasses].
+How do we ensure that every superclass witness in an instance declaration
+is generated by one of (sc1) (sc2) or (sc3) in Note [Recursive superclasses]?
Answer:
- * Superclass "wanted" constraints have CtOrigin of (ScOrigin size)
- where 'size' is the size of the instance declaration. e.g.
- class C a => D a where...
- instance blah => D [a] where ...
- The wanted superclass constraint for C [a] has origin
- ScOrigin size, where size = size( D [a] ).
+ * The "given" constraints of an instance decl have CtOrigin of
+ (GivenOrigin (InstSkol head_size)), where head_size is the
+ PatersonSize of the head of the instance declaration. E.g. in
+ instance D a => C [a]
+ the `[G] D a` constraint has a CtOrigin whose head_size is the
+ PatersonSize of (C [a]).
+
+ * When we make a superclass selection from a Given (transitively)
+ we give it a CtOrigin of (GivenSCOrigin skol_info sc_depth blocked).
+
+ The 'blocked :: Bool' flag says if the superclass can be used to
+ solve a superclass Wanted. The new superclass is blocked unless:
+
+ it is the superclass of an unblocked dictionary (wrinkle (W1)),
+ that is Paterson-smaller than the instance head.
+
+ This is implemented in GHC.Tc.Solver.Canonical.mk_strict_superclasses
+ (in the mk_given_loc helper function).
+
+ * Superclass "Wanted" constraints have CtOrigin of (ScOrigin NakedSc)
+ The 'NakedSc' says that this is a naked superclass Wanted; we must
+ be careful when solving it.
* (sc1) When we rewrite such a wanted constraint, it retains its
origin. But if we apply an instance declaration, we can set the
- origin to (ScOrigin infinity), thus lifting any restrictions by
- making prohibitedSuperClassSolve return False.
+ origin to (ScOrigin NotNakedSc), thus lifting any restrictions by
+ making prohibitedSuperClassSolve return False. This happens
+ in GHC.Tc.Solver.Interact.checkInstanceOK.
* (sc2) ScOrigin wanted constraints can't be solved from a
superclass selection, except at a smaller type. This test is
- implemented by GHC.Tc.Solver.Interact.prohibitedSuperClassSolve
-
- * The "given" constraints of an instance decl have CtOrigin
- GivenOrigin InstSkol.
-
- * When we make a superclass selection from InstSkol we use
- a CtOrigin of (InstSCOrigin size), where 'size' is the size of
- the constraint whose superclass we are taking. And similarly
- when taking the superclass of an InstSCOrigin. This is implemented
- in GHC.Tc.Solver.Canonical.mk_strict_superclasses (in the
- mk_given_loc helper function).
+ implemented by GHC.Tc.Solver.InertSet.prohibitedSuperClassSolve
Note [Silent superclass arguments] (historical interest only)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1697,7 +1732,7 @@ tcMethod
- Use tcValBinds to do the checking
-}
-tcMethods :: DFunId -> Class
+tcMethods :: SkolemInfoAnon -> DFunId -> Class
-> [TcTyVar] -> [EvVar]
-> [TcType]
-> TcEvBinds
@@ -1707,7 +1742,7 @@ tcMethods :: DFunId -> Class
-> TcM ([Id], LHsBinds GhcTc, Bag Implication)
-- The returned inst_meth_ids all have types starting
-- forall tvs. theta => ...
-tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
+tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds (spec_inst_prags, prag_fn) op_items
(InstBindings { ib_binds = binds
, ib_tyvars = lexical_tvs
@@ -1740,10 +1775,10 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication)
tc_item (sel_id, dm_info)
| Just (user_bind, bndr_loc, prags) <- findMethodBind (idName sel_id) binds prag_fn
- = tcMethodBody clas tyvars dfun_ev_vars inst_tys
- dfun_ev_binds is_derived hs_sig_fn
- spec_inst_prags prags
- sel_id user_bind bndr_loc
+ = tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys
+ dfun_ev_binds is_derived hs_sig_fn
+ spec_inst_prags prags
+ sel_id user_bind bndr_loc
| otherwise
= do { traceTc "tc_def" (ppr sel_id)
; tc_default sel_id dm_info }
@@ -1754,7 +1789,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
tc_default sel_id (Just (dm_name, _))
= do { (meth_bind, inline_prags) <- mkDefMethBind inst_loc dfun_id clas sel_id dm_name
- ; tcMethodBody clas tyvars dfun_ev_vars inst_tys
+ ; tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived hs_sig_fn
spec_inst_prags inline_prags
sel_id meth_bind inst_loc }
@@ -1872,13 +1907,14 @@ Instead, we take the much simpler approach of always disabling
-}
------------------------
-tcMethodBody :: Class -> [TcTyVar] -> [EvVar] -> [TcType]
+tcMethodBody :: SkolemInfoAnon
+ -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
-> TcEvBinds -> Bool
-> HsSigFun
-> [LTcSpecPrag] -> [LSig GhcRn]
-> Id -> LHsBind GhcRn -> SrcSpan
-> TcM (TcId, LHsBind GhcTc, Maybe Implication)
-tcMethodBody clas tyvars dfun_ev_vars inst_tys
+tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys
dfun_ev_binds is_derived
sig_fn spec_inst_prags prags
sel_id (L bind_loc meth_bind) bndr_loc
@@ -1896,7 +1932,7 @@ tcMethodBody clas tyvars dfun_ev_vars inst_tys
-- taking instance signature into account might change the type of
-- the local_meth_id
; (meth_implic, ev_binds_var, tc_bind)
- <- checkInstConstraints $
+ <- checkInstConstraints skol_info $
tcMethodBodyHelp sig_fn sel_id local_meth_id (L bind_loc lm_bind)
; global_meth_id <- addInlinePrags global_meth_id prags
@@ -2353,9 +2389,9 @@ instDeclCtxt1 hs_inst_ty
instDeclCtxt2 :: Type -> SDoc
instDeclCtxt2 dfun_ty
- = inst_decl_ctxt (ppr (mkClassPred cls tys))
+ = inst_decl_ctxt (ppr head_ty)
where
- (_,_,cls,tys) = tcSplitDFunTy dfun_ty
+ (_,_,head_ty) = tcSplitQuantPredTy dfun_ty
inst_decl_ctxt :: SDoc -> SDoc
inst_decl_ctxt doc = hang (text "In the instance declaration for")
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 2fea177885ba..0623acd3d54d 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -1690,7 +1690,7 @@ checkSkolInfoAnon sk1 sk2 = go sk1 sk2
go (DerivSkol pred1) (DerivSkol pred2) = pred1 `tcEqType` pred2
go (TyConSkol f1 n1) (TyConSkol f2 n2) = f1==f2 && n1==n2
go (DataConSkol n1) (DataConSkol n2) = n1==n2
- go InstSkol InstSkol = True
+ go (InstSkol {}) (InstSkol {}) = True
go FamInstSkol FamInstSkol = True
go BracketSkol BracketSkol = True
go (RuleSkol n1) (RuleSkol n2) = n1==n2
@@ -1700,7 +1700,6 @@ checkSkolInfoAnon sk1 sk2 = go sk1 sk2
and (zipWith eq_pr ids1 ids2)
go (UnifyForAllSkol t1) (UnifyForAllSkol t2) = t1 `tcEqType` t2
go ReifySkol ReifySkol = True
- go QuantCtxtSkol QuantCtxtSkol = True
go RuntimeUnkSkol RuntimeUnkSkol = True
go ArrowReboundIfSkol ArrowReboundIfSkol = True
go (UnkSkol _) (UnkSkol _) = True
@@ -1716,7 +1715,7 @@ checkSkolInfoAnon sk1 sk2 = go sk1 sk2
-- in tcConDecl for MkT we'll have a SkolemInfo in the implication of
-- DataConSkol, but 'a' will have SkolemInfo of FamInstSkol
- go FamInstSkol InstSkol = True
+ go FamInstSkol (InstSkol {}) = True
-- In instance C (T a) where { type F (T a) b = ... }
-- we have 'a' with SkolemInfo InstSkol, but we make an implication wi
-- SkolemInfo of FamInstSkol. Very like the ConDecl/TyConSkol case
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 72ed58b04119..4a40528f1ff4 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -13,7 +13,7 @@ module GHC.Tc.Types.Origin (
-- * SkolemInfo
SkolemInfo(..), SkolemInfoAnon(..), mkSkolemInfo, getSkolemInfo, pprSigSkolInfo, pprSkolInfo,
- unkSkol, unkSkolAnon,
+ unkSkol, unkSkolAnon, mkClsInstSkol,
-- * CtOrigin
CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin,
@@ -29,6 +29,7 @@ module GHC.Tc.Types.Origin (
FixedRuntimeRepOrigin(..), FixedRuntimeRepContext(..),
pprFixedRuntimeRepContext,
StmtOrigin(..), RepPolyFun(..), ArgPos(..),
+ ClsInstOrQC(..), NakedScFlag(..),
-- * Arrow command origin
FRRArrowContext(..), pprFRRArrowContext,
@@ -45,6 +46,7 @@ import GHC.Hs
import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Core.TyCon
+import GHC.Core.Class
import GHC.Core.InstEnv
import GHC.Core.PatSyn
import GHC.Core.Multiplicity ( scaledThing )
@@ -210,8 +212,9 @@ isSigMaybe _ = Nothing
-- same place in a single report.
data SkolemInfo
= SkolemInfo
- Unique -- ^ used to common up skolem variables bound at the same location (only used in pprSkols)
- SkolemInfoAnon -- ^ the information about the origin of the skolem type variable
+ Unique -- ^ The Unique is used to common up skolem variables bound
+ -- at the same location (only used in pprSkols)
+ SkolemInfoAnon -- ^ The information about the origin of the skolem type variable
instance Uniquable SkolemInfo where
getUnique (SkolemInfo u _) = u
@@ -248,7 +251,9 @@ data SkolemInfoAnon
| DerivSkol Type -- Bound by a 'deriving' clause;
-- the type is the instance we are trying to derive
- | InstSkol -- Bound at an instance decl
+ | InstSkol -- Bound at an instance decl, or quantified constraint
+ ClsInstOrQC -- Whether class instance or quantified constraint
+ PatersonSize -- Head has the given PatersonSize
| FamInstSkol -- Bound at a family instance decl
| PatSkol -- An existential type variable bound by a pattern for
@@ -280,9 +285,6 @@ data SkolemInfoAnon
| ReifySkol -- Bound during Template Haskell reification
- | QuantCtxtSkol -- Quantified context, e.g.
- -- f :: forall c. (forall a. c a => c [a]) => blah
-
| RuntimeUnkSkol -- Runtime skolem from the GHCi debugger #14628
| ArrowReboundIfSkol -- Bound by the expected type of the rebound arrow ifThenElse command.
@@ -312,6 +314,8 @@ mkSkolemInfo sk_anon = do
getSkolemInfo :: SkolemInfo -> SkolemInfoAnon
getSkolemInfo (SkolemInfo _ skol_anon) = skol_anon
+mkClsInstSkol :: Class -> [Type] -> SkolemInfoAnon
+mkClsInstSkol cls tys = InstSkol IsClsInst (pSizeClassPred cls tys)
instance Outputable SkolemInfo where
ppr (SkolemInfo _ sk_info ) = ppr sk_info
@@ -327,7 +331,10 @@ pprSkolInfo (ForAllSkol tvs) = text "an explicit forall" <+> ppr tvs
pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for"
<+> pprWithCommas ppr ips
pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred)
-pprSkolInfo InstSkol = text "the instance declaration"
+pprSkolInfo (InstSkol IsClsInst sz) = vcat [ text "the instance declaration"
+ , whenPprDebug (braces (ppr sz)) ]
+pprSkolInfo (InstSkol (IsQC {}) sz) = vcat [ text "a quantified context"
+ , whenPprDebug (braces (ppr sz)) ]
pprSkolInfo FamInstSkol = text "a family instance declaration"
pprSkolInfo BracketSkol = text "a Template Haskell bracket"
pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name
@@ -341,7 +348,6 @@ pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaratio
pprSkolInfo (DataConSkol name) = text "the type signature for" <+> quotes (ppr name)
pprSkolInfo ReifySkol = text "the type being reified"
-pprSkolInfo (QuantCtxtSkol {}) = text "a quantified context"
pprSkolInfo RuntimeUnkSkol = text "Unknown type from GHCi runtime"
pprSkolInfo ArrowReboundIfSkol = text "the expected type of a rebound if-then-else command"
@@ -450,39 +456,25 @@ data CtOrigin
-- 'SkolemInfo' inside gives more information.
GivenOrigin SkolemInfoAnon
- -- The following are other origins for given constraints that cannot produce
- -- new skolems -- hence no SkolemInfo.
-
- -- | 'InstSCOrigin' is used for a Given constraint obtained by superclass selection
+ -- | 'GivenSCOrigin' is used for a Given constraint obtained by superclass selection
-- from the context of an instance declaration. E.g.
-- instance @(Foo a, Bar a) => C [a]@ where ...
-- When typechecking the instance decl itself, including producing evidence
-- for the superclasses of @C@, the superclasses of @(Foo a)@ and @(Bar a)@ will
- -- have 'InstSCOrigin' origin.
- | InstSCOrigin ScDepth -- ^ The number of superclass selections necessary to
- -- get this constraint; see Note [Replacement vs keeping]
- -- in GHC.Tc.Solver.Interact
- TypeSize -- ^ If @(C ty1 .. tyn)@ is the largest class from
- -- which we made a superclass selection in the chain,
- -- then @TypeSize = sizeTypes [ty1, .., tyn]@
- -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-
- -- | 'OtherSCOrigin' is used for a Given constraint obtained by superclass
- -- selection from a constraint /other than/ the context of an instance
- -- declaration. (For the latter we use 'InstSCOrigin'.) E.g.
- -- f :: Foo a => blah
- -- f = e
- -- When typechecking body of 'f', the superclasses of the Given (Foo a)
- -- will have 'OtherSCOrigin'.
- --
- -- Needed for Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
- | OtherSCOrigin ScDepth -- ^ The number of superclass selections necessary to
- -- get this constraint
- SkolemInfoAnon
- -- ^ Where the sub-class constraint arose from
- -- (used only for printing)
+ -- have 'GivenSCOrigin' origin.
+ | GivenSCOrigin
+ SkolemInfoAnon -- ^ Just like GivenOrigin
+
+ ScDepth -- ^ The number of superclass selections necessary to
+ -- get this constraint; see Note [Replacement vs keeping]
+ -- in GHC.Tc.Solver.Interact
- -- All the others are for *wanted* constraints
+ Bool -- ^ True => "blocked": cannot use this to solve naked superclass Wanteds
+ -- i.e. ones with (ScOrigin _ NakedSc)
+ -- False => can use this to solve all Wanted constraints
+ -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+
+ ----------- Below here, all are Origins for Wanted constraints ------------
| OccurrenceOf Name -- Occurrence of an overloaded identifier
| OccurrenceOfRecSel RdrName -- Occurrence of a record selector
@@ -531,11 +523,10 @@ data CtOrigin
| ViewPatOrigin
-- | 'ScOrigin' is used only for the Wanted constraints for the
- -- superclasses of an instance declaration.
- -- If the instance head is @C ty1 .. tyn@
- -- then @TypeSize = sizeTypes [ty1, .., tyn]@
- -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
- | ScOrigin TypeSize
+ -- superclasses of an instance declaration.
+ | ScOrigin
+ ClsInstOrQC -- Whether class instance or quantified constraint
+ NakedScFlag
| DerivClauseOrigin -- Typechecking a deriving clause (as opposed to
-- standalone deriving).
@@ -604,6 +595,7 @@ data CtOrigin
| CycleBreakerOrigin
CtOrigin -- origin of the original constraint
+
-- See Detail (7) of Note [Type equality cycles] in GHC.Tc.Solver.Canonical
| FRROrigin
FixedRuntimeRepOrigin
@@ -619,11 +611,25 @@ data CtOrigin
Type -- the instantiated type of the method
| AmbiguityCheckOrigin UserTypeCtxt
+
-- | The number of superclass selections needed to get this Given.
-- If @d :: C ty@ has @ScDepth=2@, then the evidence @d@ will look
-- like @sc_sel (sc_sel dg)@, where @dg@ is a Given.
type ScDepth = Int
+data ClsInstOrQC = IsClsInst
+ | IsQC CtOrigin
+
+data NakedScFlag = NakedSc | NotNakedSc
+ -- The NakedScFlag affects only GHC.Tc.Solver.InertSet.prohibitedSuperClassSolve
+ -- * For the original superclass constraints we use (ScOrigin _ NakedSc)
+ -- * But after using an instance declaration we use (ScOrigin _ NotNakedSc)
+ -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+
+instance Outputable NakedScFlag where
+ ppr NakedSc = text "NakedSc"
+ ppr NotNakedSc = text "NotNakedSc"
+
-- An origin is visible if the place where the constraint arises is manifest
-- in user code. Currently, all origins are visible except for invisible
-- TypeEqOrigins. This is used when choosing which error of
@@ -640,11 +646,10 @@ toInvisibleOrigin orig@(TypeEqOrigin {}) = orig { uo_visible = False }
toInvisibleOrigin orig = orig
isGivenOrigin :: CtOrigin -> Bool
-isGivenOrigin (GivenOrigin {}) = True
-isGivenOrigin (InstSCOrigin {}) = True
-isGivenOrigin (OtherSCOrigin {}) = True
-isGivenOrigin (CycleBreakerOrigin o) = isGivenOrigin o
-isGivenOrigin _ = False
+isGivenOrigin (GivenOrigin {}) = True
+isGivenOrigin (GivenSCOrigin {}) = True
+isGivenOrigin (CycleBreakerOrigin o) = isGivenOrigin o
+isGivenOrigin _ = False
-- See Note [Suppressing confusing errors] in GHC.Tc.Errors
isWantedWantedFunDepOrigin :: CtOrigin -> Bool
@@ -731,9 +736,12 @@ lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS"
pprCtOrigin :: CtOrigin -> SDoc
-- "arising from ..."
-pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
-pprCtOrigin (InstSCOrigin {}) = ctoHerald <+> pprSkolInfo InstSkol -- keep output in sync
-pprCtOrigin (OtherSCOrigin _ si) = ctoHerald <+> pprSkolInfo si
+pprCtOrigin (GivenOrigin sk)
+ = ctoHerald <+> ppr sk
+
+pprCtOrigin (GivenSCOrigin sk d blk)
+ = vcat [ ctoHerald <+> pprSkolInfo sk
+ , whenPprDebug (braces (text "given-sc:" <+> ppr d <> comma <> ppr blk)) ]
pprCtOrigin (SpecPragOrigin ctxt)
= case ctxt of
@@ -817,9 +825,6 @@ pprCtOrigin (InstProvidedOrigin mod cls_inst)
pprCtOrigin (CycleBreakerOrigin orig)
= pprCtOrigin orig
-pprCtOrigin (FRROrigin {})
- = ctoHerald <+> text "a representation-polymorphism check"
-
pprCtOrigin (WantedSuperclassOrigin subclass_pred subclass_orig)
= sep [ ctoHerald <+> text "a superclass required to satisfy" <+> quotes (ppr subclass_pred) <> comma
, pprCtOrigin subclass_orig ]
@@ -836,6 +841,15 @@ pprCtOrigin (AmbiguityCheckOrigin ctxt)
= ctoHerald <+> text "a type ambiguity check for" $$
pprUserTypeCtxt ctxt
+pprCtOrigin (ScOrigin IsClsInst nkd)
+ = vcat [ ctoHerald <+> text "the superclasses of an instance declaration"
+ , whenPprDebug (braces (text "sc-origin:" <> ppr nkd)) ]
+
+pprCtOrigin (ScOrigin (IsQC orig) nkd)
+ = vcat [ ctoHerald <+> text "the head of a quantified constraint"
+ , whenPprDebug (braces (text "sc-origin:" <> ppr nkd))
+ , pprCtOrigin orig ]
+
pprCtOrigin simple_origin
= ctoHerald <+> pprCtO simple_origin
@@ -859,8 +873,8 @@ pprCtO (HasFieldOrigin f) = hsep [text "selecting the field", quotes (ppr f)]
pprCtO AssocFamPatOrigin = text "the LHS of a family instance"
pprCtO TupleOrigin = text "a tuple"
pprCtO NegateOrigin = text "a use of syntactic negation"
-pprCtO (ScOrigin n) = text "the superclasses of an instance declaration"
- <> whenPprDebug (parens (ppr n))
+pprCtO (ScOrigin IsClsInst _) = text "the superclasses of an instance declaration"
+pprCtO (ScOrigin (IsQC {}) _) = text "the head of a quantified constraint"
pprCtO DerivClauseOrigin = text "the 'deriving' clause of a data type declaration"
pprCtO StandAloneDerivOrigin = text "a 'deriving' declaration"
pprCtO DefaultOrigin = text "a 'default' declaration"
@@ -884,8 +898,7 @@ pprCtO BracketOrigin = text "a quotation bracket"
-- get here via callStackOriginFS, when doing ambiguity checks
-- A bit silly, but no great harm
pprCtO (GivenOrigin {}) = text "a given constraint"
-pprCtO (InstSCOrigin {}) = text "the superclass of an instance constraint"
-pprCtO (OtherSCOrigin {}) = text "the superclass of a given constraint"
+pprCtO (GivenSCOrigin {}) = text "the superclass of a given constraint"
pprCtO (SpecPragOrigin {}) = text "a SPECIALISE pragma"
pprCtO (FunDepOrigin1 {}) = text "a functional dependency"
pprCtO (FunDepOrigin2 {}) = text "a functional dependency"
diff --git a/compiler/GHC/Tc/Utils/Backpack.hs b/compiler/GHC/Tc/Utils/Backpack.hs
index a73c01c90fd1..f11b900d6e4c 100644
--- a/compiler/GHC/Tc/Utils/Backpack.hs
+++ b/compiler/GHC/Tc/Utils/Backpack.hs
@@ -27,7 +27,6 @@ import GHC.Types.Fixity (defaultFixity)
import GHC.Types.Fixity.Env
import GHC.Types.TypeEnv
import GHC.Types.Name.Reader
-import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Types.Name.Set
@@ -35,6 +34,7 @@ import GHC.Types.Avail
import GHC.Types.SrcLoc
import GHC.Types.SourceFile
import GHC.Types.Var
+import GHC.Types.Id( idType )
import GHC.Types.Unique.DSet
import GHC.Types.Name.Shape
import GHC.Types.PkgQual
@@ -62,8 +62,6 @@ import GHC.Hs
import GHC.Core.InstEnv
import GHC.Core.FamInstEnv
-import GHC.Core.Type
-import GHC.Core.Multiplicity
import GHC.IfaceToCore
import GHC.Iface.Load
@@ -221,32 +219,23 @@ checkHsigIface tcg_env gr sig_iface
-- (we might conclude the module exports an instance when it doesn't, see
-- #9422), but we will never refuse to compile something.
check_inst :: ClsInst -> TcM ()
-check_inst sig_inst = do
+check_inst sig_inst@(ClsInst { is_dfun = dfun_id }) = do
-- TODO: This could be very well generalized to support instance
-- declarations in boot files.
tcg_env <- getGblEnv
-- NB: Have to tug on the interface, not necessarily
-- tugged... but it didn't work?
mapM_ tcLookupImported_maybe (nameSetElemsStable (orphNamesOfClsInst sig_inst))
+
-- Based off of 'simplifyDeriv'
- let ty = idType (instanceDFunId sig_inst)
- -- Based off of tcSplitDFunTy
- (tvs, theta, pred) =
- case tcSplitForAllInvisTyVars ty of { (tvs, rho) ->
- case splitFunTys rho of { (theta, pred) ->
- (tvs, theta, pred) }}
- origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
- skol_info <- mkSkolemInfo InstSkol
- (skol_subst, tvs_skols) <- tcInstSkolTyVars skol_info tvs -- Skolemize
+ let origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
+ (skol_info, tvs_skols, inst_theta, cls, inst_tys) <- tcSkolDFunType (idType dfun_id)
(tclvl,cts) <- pushTcLevelM $ do
- wanted <- newWanted origin
- (Just TypeLevel)
- (substTy skol_subst pred)
- givens <- forM theta $ \given -> do
+ wanted <- newWanted origin (Just TypeLevel) (mkClassPred cls inst_tys)
+ givens <- forM inst_theta $ \given -> do
loc <- getCtLocM origin (Just TypeLevel)
- let given_pred = substTy skol_subst (scaledThing given)
- new_ev <- newEvVar given_pred
- return CtGiven { ctev_pred = given_pred
+ new_ev <- newEvVar given
+ return CtGiven { ctev_pred = given
-- Doesn't matter, make something up
, ctev_evar = new_ev
, ctev_loc = loc
@@ -254,7 +243,7 @@ check_inst sig_inst = do
return $ wanted : givens
unsolved <- simplifyWantedsTcM cts
- (implic, _) <- buildImplicationFor tclvl (getSkolemInfo skol_info) tvs_skols [] unsolved
+ (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
reportAllUnsolved (mkImplicWC implic)
-- | For a module @modname@ of type 'HscSource', determine the list
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 0b6b519028c8..b8249bc3634f 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleContexts, RecursiveDo #-}
{-# LANGUAGE DisambiguateRecordFields #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
@@ -446,12 +446,24 @@ tcInstTypeBndrs poly_ty
; return (subst', Bndr tv' spec) }
--------------------------
-tcSkolDFunType :: SkolemInfo -> DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
+tcSkolDFunType :: Type -> TcM (SkolemInfoAnon, [TcTyVar], TcThetaType, Class, [TcType])
-- Instantiate a type signature with skolem constants.
-- This freshens the names, but no need to do so
-tcSkolDFunType skol_info dfun
- = do { (tv_prs, theta, tau) <- tcInstType (tcInstSuperSkolTyVars skol_info) dfun
- ; return (map snd tv_prs, theta, tau) }
+tcSkolDFunType dfun_ty
+ = do { let (tvs, theta, cls, tys) = tcSplitDFunTy dfun_ty
+
+ -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ ; rec { skol_info <- mkSkolemInfo skol_info_anon
+ ; (subst, inst_tvs) <- tcInstSuperSkolTyVars skol_info tvs
+ -- We instantiate the dfun_tyd with superSkolems.
+ -- See Note [Subtle interaction of recursion and overlap]
+ -- and Note [Binding when looking up instances]
+ ; let inst_tys = substTys subst tys
+ skol_info_anon = mkClsInstSkol cls inst_tys }
+
+ ; let inst_theta = substTheta subst theta
+ ; return (skol_info_anon, inst_tvs, inst_theta, cls, inst_tys) }
tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (Subst, [TcTyVar])
-- Make skolem constants, but do *not* give them new names, as above
@@ -483,7 +495,9 @@ tcInstSkolTyVarsX skol_info = tcInstSkolTyVarsPushLevel skol_info False
tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
-- This version freshens the names and creates "super skolems";
--- see comments around superSkolemTv.
+-- see comments around superSkolemTv.
+-- Must be lazy in skol_info:
+-- see Note [Keeping SkolemInfo inside a SkolemTv] in GHC.Tc.Utils.TcType
tcInstSuperSkolTyVars skol_info = tcInstSuperSkolTyVarsX skol_info emptySubst
tcInstSuperSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 5824c3e7f640..89614378cd5e 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -2579,10 +2579,10 @@ zonkTidyOrigin env (GivenOrigin skol_info)
= do { skol_info1 <- zonkSkolemInfoAnon skol_info
; let skol_info2 = tidySkolemInfoAnon env skol_info1
; return (env, GivenOrigin skol_info2) }
-zonkTidyOrigin env (OtherSCOrigin sc_depth skol_info)
+zonkTidyOrigin env (GivenSCOrigin skol_info sc_depth blocked)
= do { skol_info1 <- zonkSkolemInfoAnon skol_info
; let skol_info2 = tidySkolemInfoAnon env skol_info1
- ; return (env, OtherSCOrigin sc_depth skol_info2) }
+ ; return (env, GivenSCOrigin skol_info2 sc_depth blocked) }
zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
, uo_expected = exp })
= do { (env1, act') <- zonkTidyTcType env act
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 28894d68edbc..dc6bbe746bed 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -86,6 +86,7 @@ module GHC.Tc.Utils.TcType (
checkValidClsArgs, hasTyVarHead,
isRigidTy,
+
-- Re-exported from GHC.Core.TyCo.Compare
-- mainly just for back-compat reasons
eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX,
@@ -130,6 +131,18 @@ module GHC.Tc.Utils.TcType (
isFunPtrTy, -- :: Type -> Bool
tcSplitIOType_maybe, -- :: Type -> Maybe Type
+ ---------------------------------
+ -- Patersons sizes
+ PatersonSize(..), PatersonSizeFailure(..),
+ ltPatersonSize,
+ pSizeZero, pSizeOne,
+ pSizeType, pSizeTypeX, pSizeTypes,
+ pSizeClassPred, pSizeClassPredX,
+ pSizeTyConApp,
+ noMoreTyVars, allDistinctTyVars,
+ TypeSize, sizeType, sizeTypes, scopedSort,
+ isTerminatingClass, isStuckTypeFamily,
+
--------------------------------
-- Reexported from Kind
Kind, liftedTypeKind, constraintKind,
@@ -152,7 +165,7 @@ module GHC.Tc.Utils.TcType (
isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass,
mkClassPred,
- tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
+ tcSplitQuantPredTy, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
isRuntimeRepVar, isFixedRuntimeRepKind,
isVisiblePiTyBinder, isInvisiblePiTyBinder,
@@ -192,8 +205,6 @@ module GHC.Tc.Utils.TcType (
pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred,
pprTCvBndr, pprTCvBndrs,
- TypeSize, sizeType, sizeTypes, scopedSort,
-
---------------------------------
-- argument visibility
tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible
@@ -244,7 +255,7 @@ import qualified GHC.LanguageExtensions as LangExt
import Data.IORef
import Data.List.NonEmpty( NonEmpty(..) )
-import Data.List ( partition )
+import Data.List ( partition, nub, (\\) )
import GHC.Generics ( Generic )
@@ -585,13 +596,32 @@ vanillaSkolemTv for a TyVar.
But ultimately I want to separate Type from TcType, and in that case
we would need to enforce the separation.
+
+Note [Keeping SkolemInfo inside a SkolemTv]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A SkolemTv contains a SkolemInfo, which describes the binding side of that
+TcTyVar. This is very convenient to a consumer of a SkolemTv, but it is
+a bit awkward for the /producer/. Why? Because sometimes we can't produce
+the SkolemInfo until we have the TcTyVars!
+
+Example: in `GHC.Tc.Utils.Unify.tcTopSkolemise` we create SkolemTvs whose
+`SkolemInfo` is `SigSkol`, whose arguments in turn mention the newly-created
+SkolemTvs. So we a RecrusiveDo idiom, like this:
+
+ rec { (wrap, tv_prs, given, rho_ty) <- skolemise skol_info expected_ty
+ ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
+
+Note that the `skol_info` can't be created until we have the `tv_prs` returned
+by `skolemise`. Note also that `skolemise` had better be lazy in `skol_info`.
+
+All uses of this idiom should be flagged with a reference to this Note.
-}
-- A TyVarDetails is inside a TyVar
-- See Note [TyVars and TcTyVars during type checking]
data TcTyVarDetails
= SkolemTv -- A skolem
- SkolemInfo
+ SkolemInfo -- See Note [Keeping SkolemInfo inside a SkolemTv]
TcLevel -- Level of the implication that binds it
-- See GHC.Tc.Utils.Unify Note [Deeper level on the left] for
-- how this level number is used
@@ -1581,20 +1611,23 @@ tcIsTyVarTy (TyVarTy _) = True
tcIsTyVarTy _ = False
-----------------------
-tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
--- Split the type of a dictionary function
--- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
--- have non-Pred arguments, such as
--- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
---
--- Also NB splitFunTys, not tcSplitFunTys;
+tcSplitQuantPredTy :: Type -> ([TyVar], [Type], PredType)
+-- Split up the type of a quantified predicate
+-- forall tys, theta => head
+-- NB splitFunTys, not tcSplitFunTys;
-- the latter specifically stops at PredTy arguments,
-- and we don't want to do that here
-tcSplitDFunTy ty
+tcSplitQuantPredTy ty
= case tcSplitForAllInvisTyVars ty of { (tvs, rho) ->
- case splitFunTys rho of { (theta, tau) ->
- case tcSplitDFunHead tau of { (clas, tys) ->
- (tvs, map scaledThing theta, clas, tys) }}}
+ case splitFunTys rho of { (theta, head) ->
+ (tvs, map scaledThing theta, head) }}
+
+tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
+-- Split the type of a dictionary function
+tcSplitDFunTy ty
+ = case tcSplitQuantPredTy ty of { (tvs, theta, head) ->
+ case tcSplitDFunHead head of { (clas, tys) ->
+ (tvs, theta, clas, tys) }}
tcSplitDFunHead :: Type -> (Class, [Type])
tcSplitDFunHead = getClassPredTys
@@ -1645,8 +1678,8 @@ checkValidClsArgs :: Bool -> Class -> [KindOrType] -> Bool
-- If the Bool is True (flexible contexts), return True (i.e. ok)
-- Otherwise, check that the type (not kind) args are all headed by a tyvar
-- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
--- This function is here rather than in GHC.Tc.Validity because it is
--- called from GHC.Tc.Solver, which itself is imported by GHC.Tc.Validity
+-- This function is here in GHC.Tc.Utils.TcType, rather than in GHC.Tc.Validity,
+-- because it is called from GHC.Tc.Solver, which itself is imported by GHC.Tc.Validity
checkValidClsArgs flexible_contexts cls kts
| flexible_contexts = True
| otherwise = all hasTyVarHead tys
@@ -2261,71 +2294,11 @@ Reason: the back end falls over with panic "primRepHint:VoidRep";
{-
************************************************************************
* *
- The "Paterson size" of a type
+ Visiblities
* *
************************************************************************
-}
-{-
-Note [Paterson conditions on PredTypes]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We are considering whether *class* constraints terminate
-(see Note [Paterson conditions]). Precisely, the Paterson conditions
-would have us check that "the constraint has fewer constructors and variables
-(taken together and counting repetitions) than the head.".
-
-However, we can be a bit more refined by looking at which kind of constraint
-this actually is. There are two main tricks:
-
- 1. It seems like it should be OK not to count the tuple type constructor
- for a PredType like (Show a, Eq a) :: Constraint, since we don't
- count the "implicit" tuple in the ThetaType itself.
-
- In fact, the Paterson test just checks *each component* of the top level
- ThetaType against the size bound, one at a time. By analogy, it should be
- OK to return the size of the *largest* tuple component as the size of the
- whole tuple.
-
- 2. Once we get into an implicit parameter or equality we
- can't get back to a class constraint, so it's safe
- to say "size 0". See #4200.
-
-NB: we don't want to detect PredTypes in sizeType (and then call
-sizePred on them), or we might get an infinite loop if that PredType
-is irreducible. See #5581.
--}
-
-type TypeSize = IntWithInf
-
-sizeType :: Type -> TypeSize
--- Size of a type: the number of variables and constructors
--- Ignore kinds altogether
-sizeType = go
- where
- go ty | Just exp_ty <- coreView ty = go exp_ty
- go (TyVarTy {}) = 1
- go (TyConApp tc tys)
- | isTypeFamilyTyCon tc = infinity -- Type-family applications can
- -- expand to any arbitrary size
- | otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1
- -- Why filter out invisible args? I suppose any
- -- size ordering is sound, but why is this better?
- -- I came across this when investigating #14010.
- go (LitTy {}) = 1
- go (FunTy _ w arg res) = go w + go arg + go res + 1
- go (AppTy fun arg) = go fun + go arg
- go (ForAllTy (Bndr tv vis) ty)
- | isVisibleForAllTyFlag vis = go (tyVarKind tv) + go ty + 1
- | otherwise = go ty + 1
- go (CastTy ty _) = go ty
- go (CoercionTy {}) = 0
-
-sizeTypes :: [Type] -> TypeSize
-sizeTypes tys = sum (map sizeType tys)
-
------------------------------------------------------------------------------------
------------------------------------------------------------------------------------
------------------------
-- | For every arg a tycon can take, the returned list says True if the argument
-- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to
-- allow for oversaturation.
@@ -2347,3 +2320,231 @@ isNextArgVisible ty
| otherwise = True
-- this second case might happen if, say, we have an unzonked TauTv.
-- But TauTvs can't range over types that take invisible arguments
+
+{-
+************************************************************************
+* *
+ Paterson sizes
+* *
+************************************************************************
+-}
+
+{- Note [The PatersonSize of a type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The PatersonSize of type is something we can compare, with `ltPatersonSize`,
+to determine if the Paterson conditions are satisfied for an instance
+declaration. See Note [Paterson conditions] in GHC.Tc.Validity.
+
+There are some wrinkles
+
+(PS1) Once we get into an implicit parameter or equality we
+ can't get back to a class constraint, so it's safe
+ to say "size 0". See #4200.
+
+ We do this with isTerminatingClass
+
+Note [Invisible arguments and termination]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When checking the ​Paterson conditions for termination an instance
+declaration, we check for the number of "constructors and variables"
+in the instance head and constraints. Question: Do we look at
+
+ * All the arguments, visible or invisible?
+ * Just the visible arguments?
+
+I think both will ensure termination, provided we are consistent.
+Currently we are /not/ consistent, which is really a bug. It's
+described in #15177, which contains a number of examples.
+The suspicious bits are the calls to filterOutInvisibleTypes.
+See also #11833.
+
+Note [Stuck type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+A type-family application generally has infinite size (PS_TyFam);
+see (PC3) in Note [Paterson conditions] in GHC.Tc.Validity.
+
+But a couple of built-in type families have no axioms, and can never
+expand into anything else. They are:
+
+* (TypeError "stuff"). E.g. consider
+
+ type family F a where
+ F Int = Bool
+ F Bool = Char
+ F _ = TypeError "Bad"
+
+ We don't want to complain about possible non-termination of F, in
+ GHC.Tc.Validity.checkFamInstRhs. cf indexed-types/should_fail/T13271
+
+* (Any @k).
+
+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.
+
+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.
+-}
+
+
+data PatersonSizeFailure
+ = PSF_TyFam TyCon -- Type family
+ | PSF_Size -- Too many type constructors/variables
+ | PSF_TyVar [TyVar] -- These type variables appear more often than in instance head;
+ -- no duplicates in this list
+
+--------------------------------------
+
+data PatersonSize -- See Note [Paterson conditions] in GHC.Tc.Validity
+ = PS_TyFam TyCon -- Mentions a type family; infinite size
+
+ | PS_Vanilla { ps_tvs :: [TyVar] -- Free tyvars, including repetitions;
+ , ps_size :: Int -- Number of type constructors and variables
+ }
+ -- Always after expanding synonyms
+ -- Always ignore coercions (not user written)
+ -- ToDo: ignore invisible arguments? See Note [Invisible arguments and termination]
+
+instance Outputable PatersonSize where
+ ppr (PS_TyFam tc) = text "PS_TyFam" <+> ppr tc
+ ppr (PS_Vanilla { ps_tvs = tvs, ps_size = size })
+ = text "PS_Vanilla" <> braces (sep [ text "ps_tvs =" <+> ppr tvs <> comma
+ , text "ps_size =" <+> int size ])
+
+pSizeZero, pSizeOne :: PatersonSize
+pSizeZero = PS_Vanilla { ps_tvs = [], ps_size = 0 }
+pSizeOne = PS_Vanilla { ps_tvs = [], ps_size = 1 }
+
+ltPatersonSize :: PatersonSize -- Size of constraint
+ -> PatersonSize -- Size of instance head; never PS_TyFam
+ -> Maybe PatersonSizeFailure
+-- (ps1 `ltPatersonSize` ps2) returns
+-- Nothing iff ps1 is strictly smaller than p2
+-- Just ps_fail says what went wrong
+ltPatersonSize (PS_TyFam tc) _ = Just (PSF_TyFam tc)
+ltPatersonSize (PS_Vanilla { ps_tvs = tvs1, ps_size = s1 })
+ (PS_Vanilla { ps_tvs = tvs2, ps_size = s2 })
+ | s1 >= s2 = Just PSF_Size
+ | bad_tvs@(_:_) <- noMoreTyVars tvs1 tvs2 = Just (PSF_TyVar bad_tvs)
+ | otherwise = Nothing -- OK!
+ltPatersonSize (PS_Vanilla {}) (PS_TyFam tc)
+ = pprPanic "ltPSize" (ppr tc)
+ -- Impossible because we never have a type family in an instance head
+
+noMoreTyVars :: [TyVar] -- Free vars (with repetitions) of the constraint C
+ -> [TyVar] -- Free vars (with repetitions) of the head H
+ -> [TyVar] -- TyVars that appear more often in C than H;
+ -- no repetitions in this list
+noMoreTyVars tvs head_tvs
+ = nub (tvs \\ head_tvs) -- The (\\) is list difference; e.g.
+ -- [a,b,a,a] \\ [a,a] = [b,a]
+ -- So we are counting repetitions
+
+addPSize :: PatersonSize -> PatersonSize -> PatersonSize
+addPSize ps1@(PS_TyFam {}) _ = ps1
+addPSize _ ps2@(PS_TyFam {}) = ps2
+addPSize (PS_Vanilla { ps_tvs = tvs1, ps_size = s1 })
+ (PS_Vanilla { ps_tvs = tvs2, ps_size = s2 })
+ = PS_Vanilla { ps_tvs = tvs1 ++ tvs2, ps_size = s1 + s2 }
+ -- (++) is not very performant, but the types
+ -- are user-written and never large
+
+pSizeType :: Type -> PatersonSize
+pSizeType = pSizeTypeX emptyVarSet
+
+pSizeTypes :: [Type] -> PatersonSize
+pSizeTypes = pSizeTypesX emptyVarSet pSizeZero
+
+-- Paterson size of a type, retaining repetitions, and expanding synonyms
+-- This ignores coercions, as coercions aren't user-written
+pSizeTypeX :: VarSet -> Type -> PatersonSize
+pSizeTypeX bvs ty | Just exp_ty <- coreView ty = pSizeTypeX bvs exp_ty
+pSizeTypeX bvs (TyVarTy tv)
+ | tv `elemVarSet` bvs = pSizeOne
+ | otherwise = PS_Vanilla { ps_tvs = [tv], ps_size = 1 }
+pSizeTypeX _ (LitTy {}) = pSizeOne
+pSizeTypeX bvs (TyConApp tc tys) = pSizeTyConAppX bvs tc tys
+pSizeTypeX bvs (AppTy fun arg) = pSizeTypeX bvs fun `addPSize` pSizeTypeX bvs arg
+pSizeTypeX bvs (FunTy _ w arg res) = pSizeTypeX bvs w `addPSize` pSizeTypeX bvs arg `addPSize`
+ pSizeTypeX bvs res
+pSizeTypeX bvs (ForAllTy (Bndr tv _) ty) = pSizeTypeX bvs (tyVarKind tv) `addPSize`
+ pSizeTypeX (bvs `extendVarSet` tv) ty
+pSizeTypeX bvs (CastTy ty _) = pSizeTypeX bvs ty
+pSizeTypeX _ (CoercionTy {}) = pSizeOne
+
+pSizeTypesX :: VarSet -> PatersonSize -> [Type] -> PatersonSize
+pSizeTypesX bvs sz tys = foldr (addPSize . pSizeTypeX bvs) sz tys
+
+pSizeTyConApp :: TyCon -> [Type] -> PatersonSize
+pSizeTyConApp = pSizeTyConAppX emptyVarSet
+
+pSizeTyConAppX :: VarSet -> TyCon -> [Type] -> PatersonSize
+-- Open question: do we count all args, or just the visible ones?
+-- See Note [Invisible arguments and termination]
+pSizeTyConAppX bvs tc tys
+ | isTypeFamilyTyCon tc = pSizeTyFamApp tc
+ | otherwise = pSizeTypesX bvs pSizeOne tys
+
+pSizeTyFamApp :: TyCon -> PatersonSize
+-- See Note [Stuck type families]
+pSizeTyFamApp tc
+ | isStuckTypeFamily tc = pSizeZero
+ | otherwise = PS_TyFam tc
+
+pSizeClassPred :: Class -> [Type] -> PatersonSize
+pSizeClassPred = pSizeClassPredX emptyVarSet
+
+pSizeClassPredX :: VarSet -> Class -> [Type] -> PatersonSize
+pSizeClassPredX bvs cls tys
+ | isTerminatingClass cls -- See (PS1) in Note [The PatersonSize of a type]
+ = pSizeZero
+ | otherwise
+ = pSizeTypesX bvs pSizeOne $
+ filterOutInvisibleTypes (classTyCon cls) tys
+ -- filterOutInvisibleTypes Yuk! See Note [Invisible arguments and termination]
+
+isStuckTypeFamily :: TyCon -> Bool
+-- See Note [Stuck type families]
+isStuckTypeFamily tc
+ = tc `hasKey` errorMessageTypeErrorFamKey
+ || tc `hasKey` anyTyConKey
+
+-- | When this says "True", ignore this class constraint during
+-- a termination check
+-- See (PS1) in Note [The PatersonSize of a type]
+isTerminatingClass :: Class -> Bool
+isTerminatingClass cls
+ = isIPClass cls -- Implicit parameter constraints always terminate because
+ -- there are no instances for them --- they are only solved
+ -- by "local instances" in expressions
+ || isEqPredClass cls
+ || cls `hasKey` typeableClassKey
+ -- Typeable constraints are bigger than they appear due
+ -- to kind polymorphism, but we can never get instance divergence this way
+ || cls `hasKey` coercibleTyConKey
+
+allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
+-- (allDistinctTyVars tvs tys) returns True if tys are
+-- a) all tyvars
+-- b) all distinct
+-- c) disjoint from tvs
+allDistinctTyVars _ [] = True
+allDistinctTyVars tkvs (ty : tys)
+ = case getTyVar_maybe ty of
+ Nothing -> False
+ Just tv | tv `elemVarSet` tkvs -> False
+ | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys
+
+-----------------------
+type TypeSize = IntWithInf
+
+sizeType :: Type -> TypeSize
+-- Size of a type: the number of variables and constructors
+sizeType ty = toTypeSize (pSizeType ty)
+
+sizeTypes :: [Type] -> TypeSize
+sizeTypes tys = toTypeSize (foldr (addPSize . pSizeType) pSizeZero tys)
+
+toTypeSize :: PatersonSize -> TypeSize
+toTypeSize (PS_TyFam {}) = infinity
+toTypeSize (PS_Vanilla { ps_size = size }) = mkIntWithInf size
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 41faa2fece0f..eea0ed95efaf 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1477,8 +1477,8 @@ tcSkolemiseScoped ctxt expected_ty thing_inside
= do { deep_subsumption <- xoptM LangExt.DeepSubsumption
; let skolemise | deep_subsumption = deeplySkolemise
| otherwise = topSkolemise
- ; -- This (unpleasant) rec block allows us to pass skol_info to deeplySkolemise;
- -- but skol_info can't be built until we have tv_prs
+ ; -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
rec { (wrap, tv_prs, given, rho_ty) <- skolemise skol_info expected_ty
; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
@@ -1495,7 +1495,9 @@ tcTopSkolemise ctxt expected_ty thing_inside
= do { res <- thing_inside expected_ty
; return (idHsWrapper, res) }
| otherwise
- = do { rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
+ = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
; let skol_tvs = map snd tv_prs
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index ff1c6169747e..6bd86a81f0f4 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -17,7 +17,6 @@ module GHC.Tc.Validity (
checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
arityErr,
checkTyConTelescope,
- allDistinctTyVars
) where
import GHC.Prelude
@@ -29,12 +28,19 @@ import GHC.Data.Maybe
import GHC.Tc.Utils.Unify ( tcSubTypeAmbiguity )
import GHC.Tc.Solver ( simplifyAmbiguityCheck )
import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) )
-import GHC.Core.TyCo.FVs
-import GHC.Core.TyCo.Rep
-import GHC.Core.TyCo.Ppr
-import GHC.Tc.Utils.TcType hiding ( sizeType, sizeTypes )
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Types.Origin
+import GHC.Tc.Types.Rank
+import GHC.Tc.Errors.Types
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Env ( tcInitTidyEnv, tcInitOpenTidyEnv )
+import GHC.Tc.Instance.FunDeps
+import GHC.Tc.Instance.Family
+
import GHC.Builtin.Types
import GHC.Builtin.Names
+import GHC.Builtin.Uniques ( mkAlphaTyVarUnique )
+
import GHC.Core.Type
import GHC.Core.Unify ( tcMatchTyX_BM, BindFlag(..) )
import GHC.Core.Coercion
@@ -42,43 +48,41 @@ import GHC.Core.Coercion.Axiom
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.Predicate
-import GHC.Tc.Types.Origin
-import GHC.Tc.Types.Rank
-import GHC.Tc.Errors.Types
-import GHC.Types.Error
+import GHC.Core.TyCo.FVs
+import GHC.Core.TyCo.Rep
+import GHC.Core.TyCo.Ppr
+import GHC.Core.FamInstEnv ( isDominatedBy, injectiveBranches
+ , InjectivityCheckResult(..) )
--- others:
import GHC.Iface.Type ( pprIfaceType, pprIfaceTypeApp )
import GHC.CoreToIface ( toIfaceTyCon, toIfaceTcArgs, toIfaceType )
import GHC.Hs
-import GHC.Tc.Utils.Monad
-import GHC.Tc.Utils.Env ( tcInitTidyEnv, tcInitOpenTidyEnv )
-import GHC.Tc.Instance.FunDeps
-import GHC.Core.FamInstEnv
- ( isDominatedBy, injectiveBranches, InjectivityCheckResult(..) )
-import GHC.Tc.Instance.Family
+import GHC.Driver.Session
+import qualified GHC.LanguageExtensions as LangExt
+
+import GHC.Types.Error
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(..), isInvisibleFunArg, mkTyVar )
+import GHC.Types.SrcLoc
+import GHC.Types.Unique.Set( isEmptyUniqSet )
+
import GHC.Utils.FV
import GHC.Utils.Error
-import GHC.Driver.Session
import GHC.Utils.Misc
-import GHC.Data.List.SetOps
-import GHC.Types.SrcLoc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
-import GHC.Builtin.Uniques ( mkAlphaTyVarUnique )
-import qualified GHC.LanguageExtensions as LangExt
+
+import GHC.Data.List.SetOps
import Language.Haskell.Syntax.Basic (FieldLabelString(..))
import Control.Monad
import Data.Foldable
import Data.Function
-import Data.List ( (\\), nub )
+import Data.List ( (\\) )
import qualified Data.List.NonEmpty as NE
{-
@@ -1659,68 +1663,67 @@ The usual functional dependency checks also apply.
Note [Valid 'deriving' predicate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-validDerivPred checks for OK 'deriving' context. See Note [Exotic
-derived instance contexts] in GHC.Tc.Deriv. However the predicate is
-here because it uses sizeTypes, fvTypes.
+validDerivPred checks for OK 'deriving' context.
+See Note [Exotic derived instance contexts] in GHC.Tc.Deriv.Infer. However the predicate is
+here because it is quite similar to checkInstTermination.
-It checks for three things
+It checks for two things:
-(VD1) No repeated variables (hasNoDups fvs)
+(VD1) The Paterson conditions; see Note [Paterson conditions]
+ Not on do we want to check for termination (of course), but it also
+ deals with a nasty corner case:
+ instance C a b => D (T a) where ...
+ Note that 'b' isn't a parameter of T. This gives rise to all sorts of
+ problems; in particular, it's hard to compare solutions for equality
+ when finding the fixpoint, and that means the inferContext loop does
+ not converge. See #5287, #21302
-(VD2) No type constructors. This is done by comparing
- sizeTypes tys == length (fvTypes tys)
- sizeTypes counts variables and constructors; fvTypes returns variables.
- So if they are the same, there must be no constructors. But there
- might be applications thus (f (g x)).
+(VD2) No type constructors; no foralls, no equalities:
+ see Note [Exotic derived instance contexts] in GHC.Tc.Deriv.Infer
- Note that tys only includes the visible arguments of the class type
+ We check the no-type-constructor bit using tyConsOfType.
+ Wrinkle: we look only at the /visible/ arguments of the class type
constructor. Including the non-visible arguments can cause the following,
perfectly valid instance to be rejected:
class Category (cat :: k -> k -> *) where ...
newtype T (c :: * -> * -> *) a b = MkT (c a b)
instance Category c => Category (T c) where ...
- since the first argument to Category is a non-visible *, which sizeTypes
- would count as a constructor! See #11833.
+ since the first argument to Category is a non-visible *, which has a
+ type constructor! See #11833.
-(VD3) Also check for a bizarre corner case, when the derived instance decl
- would look like
- instance C a b => D (T a) where ...
- Note that 'b' isn't a parameter of T. This gives rise to all sorts of
- problems; in particular, it's hard to compare solutions for equality
- when finding the fixpoint, and that means the inferContext loop does
- not converge. See #5287, #21302
Note [Equality class instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We can't have users writing instances for the equality classes. But we
still need to be able to write instances for them ourselves. So we allow
instances only in the defining module.
-
-}
-validDerivPred :: TyVarSet -> PredType -> Bool
+validDerivPred :: PatersonSize -> PredType -> Bool
-- See Note [Valid 'deriving' predicate]
-validDerivPred tv_set pred
- | not (tyCoVarsOfType pred `subVarSet` tv_set)
- = False -- Check (VD3)
-
- | otherwise
+validDerivPred head_size pred
= case classifyPredType pred of
+ EqPred {} -> False -- Reject equality constraints
+ ForAllPred {} -> False -- Rejects quantified predicates
+
+ ClassPred cls tys -> check_size (pSizeClassPred cls tys)
+ && isEmptyUniqSet (tyConsOfTypes visible_tys)
+ where
+ visible_tys = filterOutInvisibleTypes (classTyCon cls) tys -- (VD2)
+
+ IrredPred {} -> check_size (pSizeType pred)
+ -- Very important that we do the "too many variable occurrences"
+ -- check here, via check_size. Example (test T21302):
+ -- instance c Eq a => Eq (BoxAssoc a)
+ -- data BAD = BAD (BoxAssoc Int) deriving( Eq )
+ -- We don't want to accept an inferred predicate (c0 Eq Int)
+ -- from that `deriving(Eq)` clause, because the c0 is fresh,
+ -- so we'll think it's a "new" one, and loop in
+ -- GHC.Tc.Deriv.Infer.simplifyInstanceContexts
- ClassPred cls tys
- | isTerminatingClass cls -> True
- -- Typeable constraints are bigger than they appear due
- -- to kind polymorphism, but that's OK
-
- | otherwise -> hasNoDups visible_fvs -- Check (VD1)
- && lengthIs visible_fvs (sizeTypes visible_tys) -- Check (VD2)
- where
- visible_tys = filterOutInvisibleTypes (classTyCon cls) tys
- visible_fvs = fvTypes visible_tys
-
- IrredPred {} -> True -- Accept (f a)
- EqPred {} -> False -- Reject equality constraints
- ForAllPred {} -> False -- Rejects quantified predicates
+ where
+ check_size pred_size = isNothing (pred_size `ltPatersonSize` head_size)
+ -- Check (VD1)
{-
************************************************************************
@@ -1730,35 +1733,73 @@ validDerivPred tv_set pred
************************************************************************
-}
-{- Note [Instances and constraint synonyms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Currently, we don't allow instances for constraint synonyms at all.
-Consider these (#13267):
- type C1 a = Show (a -> Bool)
- instance C1 Int where -- I1
- show _ = "ur"
+{- Note [Paterson conditions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The Paterson Conditions ensure termination of instance resolution.
+Given an instance declaration
+ instance (..., C t1.. tn, ...) => D s1 .. sm
-This elicits "show is not a (visible) method of class C1", which isn't
-a great message. But it comes from the renamer, so it's hard to improve.
+we check that each constraint in the context of the instance is
+"Paterson-smaller" than the instance head. The underlying idea of
+Paterson-smaller is that
-This needs a bit more care:
- type C2 a = (Show a, Show Int)
- instance C2 Int -- I2
+ For any ground substitution S, for each constraint P in the
+ context, S(P) has fewer type constructors, counting repetitions,
+ than the head S(H)
-If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
-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.
+We implement this check by checking the following syntactic conditions:
-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.
+(PC1) No type variable has more (shallow) occurrences in P than in H.
+
+ (If not, a substitution that replaces that variable with a big type
+ would make P have many more type constructors than H. Side note: we
+ could in principle skip this test for a variable of kind Bool,
+ since there are no big ground types we can substitute for it.)
+
+(PC2) The constraint P has fewer constructors and variables (taken
+ together and counting repetitions) than the head H. This size
+ metric is computed by sizeType.
+
+ (A substitution that replaces each variable with Int demonstrates
+ the need.)
+
+(PC3) The constraint P mentions no type functions.
+
+ (A type function application can in principle expand to a type of
+ arbitrary size, and so are rejected out of hand. See #15172.)
+
+(See Section 5 of "Understanding functional dependencies via Constraint
+Handling Rules", JFP Jan 2007; and the user manual section "Instance
+termination rules".)
+
+We measure "size" with the data type PatersonSize, in GHC.Tc.Utils.TcType.
+ data PatersonSize
+ = PS_TyFam TyCon
+ | PS_Vanilla { ps_tvs :: [TyVar] -- Free tyvars, including repetitions;
+ , ps_size :: Int} -- Number of type constructors and variables
+
+* ps_tvs deals with (PC1)
+* ps_size deals with (PC2)
+* PS_TyFam deals with (PC3)
+
+Note [Tuples in checkInstTermination]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider these two ways of giving the same instance decl (#8359):
+
+ instance (Eq a, Num a) => C (T a)
+
+ type X a = (Eq a, Num a)
+ instance X a => C (T a)
+
+In the former, `checkInstTermination` will check the size of two predicates:
+(Eq a) and (Num a). In the latter, it will see only one: (X a). But we want
+to treat the latter like the former.
+
+So the `check` function in `checkInstTermination`, we simply recurse
+if we find a constraint tuple.
-}
+
checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
checkValidInstance ctxt hs_type ty = case tau of
-- See Note [Instances and constraint synonyms]
@@ -1825,33 +1866,18 @@ splitInstTyForValidity = split_context [] . drop_foralls
| isInvisibleFunArg af = split_context (pred:preds) tau
split_context preds ty = (reverse preds, ty)
-{-
-Note [Paterson conditions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Termination test: the so-called "Paterson conditions" (see Section 5 of
-"Understanding functional dependencies via Constraint Handling Rules,
-JFP Jan 2007).
-
-We check that each assertion in the context satisfies:
- (1) no variable has more occurrences in the assertion than in the head, and
- (2) the assertion has fewer constructors and variables (taken together
- and counting repetitions) than the head.
-This is only needed with -fglasgow-exts, as Haskell 98 restrictions
-(which have already been checked) guarantee termination.
-
-The underlying idea is that
-
- for any ground substitution, each assertion in the
- context has fewer type constructors than the head.
--}
-
checkInstTermination :: ThetaType -> TcPredType -> TcM ()
-- See Note [Paterson conditions]
checkInstTermination theta head_pred
= check_preds emptyVarSet theta
where
- head_fvs = fvType head_pred
- head_size = sizeType head_pred
+ head_size = pSizeType head_pred
+ -- This is inconsistent and probably wrong. pSizeType does not filter out
+ -- invisible type args (making the instance head look big), whereas the use of
+ -- pSizeClassPredX below /does/ filter them out (making the tested constraints
+ -- look smaller). I'm sure there is non termination lurking here, but see #15177
+ -- 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
@@ -1860,86 +1886,84 @@ checkInstTermination theta head_pred
check foralld_tvs pred
= case classifyPredType pred of
EqPred {} -> return () -- See #4200.
- IrredPred {} -> check2 foralld_tvs pred (sizeType pred)
- ClassPred cls tys
- | isTerminatingClass cls
- -> return ()
+ IrredPred {} -> check2 (pSizeTypeX foralld_tvs pred)
- | isCTupleClass cls -- Look inside tuple predicates; #8359
+ ClassPred cls tys
+ | isCTupleClass cls -- See Note [Tuples in checkInstTermination]
-> check_preds foralld_tvs tys
| otherwise -- Other ClassPreds
- -> check2 foralld_tvs pred bogus_size
- where
- bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
- -- See Note [Invisible arguments and termination]
+ -> check2 (pSizeClassPredX foralld_tvs cls tys)
ForAllPred tvs _ head_pred'
-> check (foralld_tvs `extendVarSetList` tvs) head_pred'
-- Termination of the quantified predicate itself is checked
-- when the predicates are individually checked for validity
- check2 foralld_tvs pred pred_size
- | not (null bad_tvs) = failWithTc $ mkTcRnUnknownMessage $ mkPlainError noHints $
- (noMoreMsg bad_tvs what (ppr head_pred))
- | not (isTyFamFree pred) = failWithTc $ mkTcRnUnknownMessage $ mkPlainError noHints $
- (nestedMsg what)
- | pred_size >= head_size = failWithTc $ mkTcRnUnknownMessage $ mkPlainError noHints $
- (smallerMsg what (ppr head_pred))
- | otherwise = return ()
- -- isTyFamFree: see Note [Type families in instance contexts]
- where
- what = text "constraint" <+> quotes (ppr pred)
- bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
- \\ head_fvs
-
-smallerMsg :: SDoc -> SDoc -> SDoc
-smallerMsg what inst_head
- = vcat [ hang (text "The" <+> what)
- 2 (sep [ text "is no smaller than"
- , text "the instance head" <+> quotes inst_head ])
- , parens undecidableMsg ]
+ where
+ check2 pred_size
+ = case pred_size `ltPatersonSize` head_size of
+ Just ps_failure -> failWithTc $ mkInstSizeError ps_failure head_pred pred
+ Nothing -> return ()
-noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc
-noMoreMsg tvs what inst_head
- = vcat [ hang (text "Variable" <> plural tvs1 <+> quotes (pprWithCommas ppr tvs1)
- <+> occurs <+> text "more often")
- 2 (sep [ text "in the" <+> what
- , text "than in the instance head" <+> quotes inst_head ])
+
+mkInstSizeError :: PatersonSizeFailure -> TcPredType -> TcPredType -> TcRnMessage
+mkInstSizeError ps_failure head_pred pred
+ = mkTcRnUnknownMessage $ mkPlainError noHints $
+ vcat [ main_msg
, parens undecidableMsg ]
where
- tvs1 = nub tvs
- occurs = if isSingleton tvs1 then text "occurs"
- else text "occur"
+ pp_head = text "instance head" <+> quotes (ppr head_pred)
+ pp_pred = text "constraint" <+> quotes (ppr pred)
+
+ main_msg = case ps_failure of
+ PSF_TyFam tc -> -- See (PC3) of Note [Paterson conditions]
+ hang (text "Illegal use of type family" <+> quotes (ppr tc))
+ 2 (text "in the" <+> pp_pred)
+ PSF_TyVar tvs -> hang (occMsg tvs)
+ 2 (sep [ text "in the" <+> pp_pred
+ , text "than in the" <+> pp_head ])
+ PSF_Size -> hang (text "The" <+> pp_pred)
+ 2 (sep [ text "is no smaller than", text "the" <+> pp_head ])
+
+occMsg :: [TyVar] -> SDoc
+occMsg tvs = text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
+ <+> pp_occurs <+> text "more often"
+ where
+ pp_occurs | isSingleton tvs = text "occurs"
+ | otherwise = text "occur"
undecidableMsg :: SDoc
undecidableMsg = text "Use UndecidableInstances to permit this"
-{- Note [Type families in instance contexts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Are these OK?
- type family F a
- instance F a => C (Maybe [a]) where ...
- instance C (F a) => C [[[a]]] where ...
-No: the type family in the instance head might blow up to an
-arbitrarily large type, depending on how 'a' is instantiated.
-So we require UndecidableInstances if we have a type family
-in the instance head. #15172.
+{- Note [Instances and constraint synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Currently, we don't allow instances for constraint synonyms at all.
+Consider these (#13267):
+ type C1 a = Show (a -> Bool)
+ instance C1 Int where -- I1
+ show _ = "ur"
-Note [Invisible arguments and termination]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When checking the ​Paterson conditions for termination an instance
-declaration, we check for the number of "constructors and variables"
-in the instance head and constraints. Question: Do we look at
+This elicits "show is not a (visible) method of class C1", which isn't
+a great message. But it comes from the renamer, so it's hard to improve.
+
+This needs a bit more care:
+ type C2 a = (Show a, Show Int)
+ instance C2 Int -- I2
- * All the arguments, visible or invisible?
- * Just the visible arguments?
+If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
+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.
-I think both will ensure termination, provided we are consistent.
-Currently we are /not/ consistent, which is really a bug. It's
-described in #15177, which contains a number of examples.
-The suspicious bits are the calls to filterOutInvisibleTypes.
+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.
-}
@@ -2118,33 +2142,46 @@ checkValidAssocTyFamDeflt fam_tc pats =
suggestion = text "The arguments to" <+> quotes (ppr fam_tc)
<+> text "must all be distinct type variables"
--- Make sure that each type family application is
--- (1) strictly smaller than the lhs,
--- (2) mentions no type variable more often than the lhs, and
--- (3) does not contain any further type family instances.
---
checkFamInstRhs :: TyCon -> [Type] -- LHS
-> [(TyCon, [Type])] -- type family calls in RHS
-> [TcRnMessage]
+-- Ensure that the type family instance terminates. Specifically:
+-- ensure that each type family application in the RHS is
+-- (TF1) a call to a stuck family like (TypeError ...) or Any
+-- See Note [Stuck type families] in GHC.Tc.Utils.TcType
+-- or (TF2) obeys the Paterson conditions, namely:
+-- - strictly smaller than the lhs,
+-- - mentions no type variable more often than the lhs, and
+-- - does not contain any further type family applications
checkFamInstRhs lhs_tc lhs_tys famInsts
- = map (mkTcRnUnknownMessage . mkPlainError noHints) $ mapMaybe check famInsts
+ = mapMaybe check famInsts
where
- lhs_size = sizeTyConAppArgs lhs_tc lhs_tys
- inst_head = pprType (TyConApp lhs_tc lhs_tys)
- lhs_fvs = fvTypes lhs_tys
+ lhs_size = pSizeTypes lhs_tys
check (tc, tys)
- | not (all isTyFamFree tys) = Just (nestedMsg what)
- | not (null bad_tvs) = Just (noMoreMsg bad_tvs what inst_head)
- | lhs_size <= fam_app_size = Just (smallerMsg what inst_head)
- | otherwise = Nothing
- where
- what = text "type family application"
- <+> quotes (pprType (TyConApp tc tys))
- fam_app_size = sizeTyConAppArgs tc tys
- bad_tvs = fvTypes tys \\ lhs_fvs
- -- The (\\) is list difference; e.g.
- -- [a,b,a,a] \\ [a,a] = [b,a]
- -- So we are counting repetitions
+ | not (isStuckTypeFamily tc) -- (TF1)
+ , Just ps_failure <- pSizeTypes tys `ltPatersonSize` lhs_size -- (TF2)
+ = Just $ mkFamSizeError ps_failure (TyConApp lhs_tc lhs_tys) (TyConApp tc tys)
+ | otherwise
+ = Nothing
+
+mkFamSizeError :: PatersonSizeFailure -> Type -> Type -> TcRnMessage
+mkFamSizeError ps_failure lhs fam_call
+ = mkTcRnUnknownMessage $ mkPlainError noHints $
+ vcat [ main_msg
+ , parens undecidableMsg ]
+ where
+ pp_lhs = text "LHS of the family instance" <+> quotes (ppr lhs)
+ pp_call = text "type-family application" <+> quotes (ppr fam_call)
+
+ main_msg = case ps_failure of
+ PSF_TyFam tc -> -- See (PC3) of Note [Paterson conditions]
+ hang (text "Illegal nested use of type family" <+> quotes (ppr tc))
+ 2 (text "in the arguments of the" <+> pp_call)
+ PSF_TyVar tvs -> hang (occMsg tvs)
+ 2 (sep [ text "in the" <+> pp_call
+ , text "than in the" <+> pp_lhs ])
+ PSF_Size -> hang (text "The" <+> pp_call)
+ 2 (sep [ text "is no smaller than", text "the" <+> pp_lhs ])
-----------------
checkFamPatBinders :: TyCon
@@ -2249,11 +2286,6 @@ inaccessibleCoAxBranch fam_tc cur_branch
= text "Type family instance equation is overlapped:" $$
nest 2 (pprCoAxBranchUser fam_tc cur_branch)
-nestedMsg :: SDoc -> SDoc
-nestedMsg what
- = sep [ text "Illegal nested" <+> what
- , parens undecidableMsg ]
-
-------------------------
checkConsistentFamInst :: AssocInstInfo
-> TyCon -- ^ Family tycon
@@ -2812,70 +2844,3 @@ checkTyConTelescope tc
2 (vcat [ sep [ pp_inf, text "always come first"]
, sep [text "then Specified variables", pp_spec]])
-{-
-************************************************************************
-* *
-\subsection{Auxiliary functions}
-* *
-************************************************************************
--}
-
--- Free variables of a type, retaining repetitions, and expanding synonyms
--- This ignores coercions, as coercions aren't user-written
-fvType :: Type -> [TyCoVar]
-fvType ty | Just exp_ty <- coreView ty = fvType exp_ty
-fvType (TyVarTy tv) = [tv]
-fvType (TyConApp _ tys) = fvTypes tys
-fvType (LitTy {}) = []
-fvType (AppTy fun arg) = fvType fun ++ fvType arg
-fvType (FunTy _ w arg res) = fvType w ++ fvType arg ++ fvType res
-fvType (ForAllTy (Bndr tv _) ty)
- = fvType (tyVarKind tv) ++
- filter (/= tv) (fvType ty)
-fvType (CastTy ty _) = fvType ty
-fvType (CoercionTy {}) = []
-
-fvTypes :: [Type] -> [TyVar]
-fvTypes tys = concatMap fvType tys
-
-sizeType :: Type -> Int
--- Size of a type: the number of variables and constructors
-sizeType ty | Just exp_ty <- coreView ty = sizeType exp_ty
-sizeType (TyVarTy {}) = 1
-sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
-sizeType (LitTy {}) = 1
-sizeType (AppTy fun arg) = sizeType fun + sizeType arg
-sizeType (FunTy _ w arg res) = sizeType w + sizeType arg + sizeType res + 1
-sizeType (ForAllTy _ ty) = sizeType ty
-sizeType (CastTy ty _) = sizeType ty
-sizeType (CoercionTy _) = 0
-
-sizeTypes :: [Type] -> Int
-sizeTypes = foldr ((+) . sizeType) 0
-
-sizeTyConAppArgs :: TyCon -> [Type] -> Int
-sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
- -- See Note [Invisible arguments and termination]
-
--- | When this says "True", ignore this class constraint during
--- a termination check
-isTerminatingClass :: Class -> Bool
-isTerminatingClass cls
- = isIPClass cls -- Implicit parameter constraints always terminate because
- -- there are no instances for them --- they are only solved
- -- by "local instances" in expressions
- || isEqPredClass cls
- || cls `hasKey` typeableClassKey
- || cls `hasKey` coercibleTyConKey
-
-allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
--- (allDistinctTyVars tvs tys) returns True if tys are
--- a) all tyvars
--- b) all distinct
--- c) disjoint from tvs
-allDistinctTyVars _ [] = True
-allDistinctTyVars tkvs (ty : tys)
- = case getTyVar_maybe ty of
- Nothing -> False
- Just tv | tv `elemVarSet` tkvs -> False
- | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys
diff --git a/docs/users_guide/exts/instances.rst b/docs/users_guide/exts/instances.rst
index 7776a7f8332b..84276527a36a 100644
--- a/docs/users_guide/exts/instances.rst
+++ b/docs/users_guide/exts/instances.rst
@@ -180,18 +180,10 @@ syntactically allowed. Some further various observations about this grammar:
.. _instance-rules:
.. _instance-termination:
-.. _undecidable-instances:
Instance termination rules
~~~~~~~~~~~~~~~~~~~~~~~~~~
-.. extension:: UndecidableInstances
- :shortdesc: Enable undecidable instances.
-
- :since: 6.8.1
-
- Permit definition of instances which may lead to type-checker non-termination.
-
Regardless of :extension:`FlexibleInstances` and :extension:`FlexibleContexts`,
instance declarations must conform to some rules that ensure that
instance resolution will terminate. The restrictions can be lifted with
@@ -212,6 +204,9 @@ The rules are these:
application can in principle expand to a type of arbitrary size,
and so are rejected out of hand
+ If these three conditions hold we say that the constraint ``(C t1 ... tn)`` is
+ **Paterson-smaller** than the instance head.
+
2. The Coverage Condition. For each functional dependency,
⟨tvs⟩\ :sub:`left` ``->`` ⟨tvs⟩\ :sub:`right`, of the class, every
type variable in S(⟨tvs⟩\ :sub:`right`) must appear in
@@ -318,10 +313,99 @@ indeed the (somewhat strange) definition:
makes instance inference go into a loop, because it requires the
constraint ``(Mul a [b] b)``.
-The :extension:`UndecidableInstances` extension is also used to lift some of the
-restrictions imposed on type family instances. See
+.. _undecidable-instances:
+
+Undecidable instances and loopy superclasses
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. extension:: UndecidableInstances
+ :shortdesc: Enable undecidable instances.
+
+ :since: 6.8.1
+
+ Permit definition of instances which may lead to type-checker non-termination.
+
+The :extension:`UndecidableInstances` extension lifts the restrictions on
+on instance declarations described in :ref:`instance-termination`.
+The :extension:`UndecidableInstances` extension also lifts some of the
+restrictions imposed on type family instances; see
:ref:`type-family-decidability`.
+
+With :extension:`UndecidableInstances` it is possible to create a superclass cycle,
+which leads to the program failing to terminate. To avoid this, GHC imposes
+rules on the way in which superclass constraints are satisfied in an instance
+declaration. These rules apply even when :extension:`UndecidableInstances` is enabled.
+Consider::
+
+ class C a => D a where ...
+
+ instance Wombat [b] => D [b] where ...
+
+When typechecking this ``instance`` declaration, GHC must ensure that ``D``'s superclass,
+``(C [b])`` is satisfied. We say that ``(C [b])`` is a **Wanted superclass constraint** of the
+instance declaration.
+
+If there is an ``instance blah => C [b]``, which is often the
+case, GHC can use the instance declaration and all is well. But suppose there is no
+such instance, so GHC can only satisfy the Wanted ``(C [b])`` from the context of the instance,
+namely the Given constraint ``(Wombat [b])``. Perhaps the declaration of ``Wombat`` looks like this::
+
+ class C a => Wombat a
+
+So the Given ``(Wombat [b])`` has a superclass ``(C [b])``, and it looks as if we can satisfy the
+Wanted ``(C [b])`` constraint from this superclass of ``Wombat``. But it turns out that
+allowing this can lead to subtle looping dictionaries, and GHC prevents it.
+
+The rule is this: **a Wanted superclass constraint can only be satisfied in one of these three ways:**
+
+.. rst-class:: open
+
+1. *Directly from the context of the instance declaration*. For example, if the declaration looked like this::
+
+ instance (Wombat [b], C [b]) => D [b] where ...
+
+ we could satisfy the Wanted ``(C [b])`` from the Given ``(C [b])``.
+
+2. *Using another instance declaration*. For example, if we had::
+
+ instance C b => C [b] where ...
+
+ we can satisfy the Wanted superclass constraint ``(C [b])`` using this instance,
+ reducing it to the Wanted constraint ``(C b)`` (which still has to be solved).
+
+3. *Using the immediate superclass of a Given constraint X that is Paterson-smaller than the head of the instance declaration.*
+ The rules for Paterson-smaller are precisely those described in :ref:`instance-rules`:
+
+ - No type variable can occur more often in X than in the instance head.
+
+ - X must have fewer type constructors and variables (taken together and counting repetitions) than the instance head.
+
+ - X must mention no type functions.
+
+Rule (3) is the tricky one. Here is an example, taken from GHC's own source code::
+
+ class Ord r => UserOfRegs r a where ...
+ (i1) instance UserOfRegs r a => UserOfRegs r (Maybe a) where
+ (i2) instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
+
+For ``(i1)`` we can get the ``(Ord r)`` superclass by selection from
+``(UserOfRegs r a)``, since it (i.e. ``UserOfRegs r a``) is Paterson-smaller than the
+head of the instance declaration, namely ``(UserOfRegs r (Maybe a))``.
+
+But for ``(i2)`` that isn't the case: ``(UserOfRegs r CmmReg)`` is not Paterson-smaller
+than the head of the instance ``(UserOfRegs r CmmExpr)``, so we can't use
+the superclasses of the former. Hence we must instead add an explicit,
+and perhaps surprising, ``(Ord r)`` argument to the instance declaration.
+
+This fix, of simply adding an apparently-redundant constraint to the context
+of an instance declaration, is robust: it always fixes the problem.
+(We considered adding it automatically, but decided that it was better be explicit.)
+
+Fixing this subtle superclass cycle has a long history; if you are interested, read
+``Note [Recursive superclasses]`` and ``Note [Solving superclass constraints]``
+in ``GHC.Tc.TyCl.Instance``.
+
.. _instance-overlap:
Overlapping instances
diff --git a/testsuite/tests/deriving/should_compile/T14339.hs b/testsuite/tests/deriving/should_compile/T14339.hs
index e2521f2de0c7..098b6e829a01 100644
--- a/testsuite/tests/deriving/should_compile/T14339.hs
+++ b/testsuite/tests/deriving/should_compile/T14339.hs
@@ -5,9 +5,6 @@ module Bug where
import GHC.TypeLits
-newtype Baz = Baz Foo
- deriving Bar
-
newtype Foo = Foo Int
class Bar a where
@@ -15,3 +12,14 @@ class Bar a where
instance (TypeError (Text "Boo")) => Bar Foo where
bar = undefined
+
+newtype Baz = Baz Foo
+ deriving Bar
+
+-- Apparently we derive
+-- instance TypeError (Text "Boo") => Bar Baz
+--
+-- Is that really what we want? It defers the type
+-- error... surely we should use standalone deriving
+-- if that is what we want?
+-- See GHC.Tc.Validity.validDerivPred and #22696.
\ No newline at end of file
diff --git a/testsuite/tests/deriving/should_fail/T21302.hs b/testsuite/tests/deriving/should_fail/T21302.hs
index 16e7cf320d27..2e073e6f3c12 100644
--- a/testsuite/tests/deriving/should_fail/T21302.hs
+++ b/testsuite/tests/deriving/should_fail/T21302.hs
@@ -10,3 +10,9 @@ type family Assoc a
data BoxAssoc a = BoxAssoc (Assoc a)
deriving instance c Eq a => Eq (BoxAssoc a)
+
+{-
+[W] Eq (BoxAssoc Int)
+==>
+[W] c0 Eq Int
+-}
diff --git a/testsuite/tests/deriving/should_fail/T8165_fail2.stderr b/testsuite/tests/deriving/should_fail/T8165_fail2.stderr
index c0ceabf9206e..99e2c5fdbb11 100644
--- a/testsuite/tests/deriving/should_fail/T8165_fail2.stderr
+++ b/testsuite/tests/deriving/should_fail/T8165_fail2.stderr
@@ -1,6 +1,6 @@
T8165_fail2.hs:9:12: error:
- • The type family application ‘T Loop’
- is no smaller than the instance head ‘T Loop’
+ • The type-family application ‘T Loop’
+ is no smaller than the LHS of the family instance ‘T Loop’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘C Loop’
diff --git a/testsuite/tests/impredicative/T17332.stderr b/testsuite/tests/impredicative/T17332.stderr
index 5fb876b8c536..97c35bf70a20 100644
--- a/testsuite/tests/impredicative/T17332.stderr
+++ b/testsuite/tests/impredicative/T17332.stderr
@@ -1,5 +1,7 @@
T17332.hs:13:7: error: [GHC-05617]
- • Could not solve: ‘a’ arising from a use of ‘MkDict’
+ • Could not solve: ‘a’
+ arising from the head of a quantified constraint
+ arising from a use of ‘MkDict’
• In the expression: MkDict
In an equation for ‘aux’: aux = MkDict
diff --git a/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
index 500be78a5f66..733d90eafc31 100644
--- a/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
+++ b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
@@ -1,17 +1,18 @@
NotRelaxedExamples.hs:9:15: error:
- • Illegal nested type family application ‘F1 (F1 Char)’
+ • Illegal nested use of type family ‘F1’
+ in the arguments of the type-family application ‘F1 (F1 Char)’
(Use UndecidableInstances to permit this)
• In the type instance declaration for ‘F1’
NotRelaxedExamples.hs:10:15: error:
- • The type family application ‘F2 [x]’
- is no smaller than the instance head ‘F2 [x]’
+ • The type-family application ‘F2 [x]’
+ is no smaller than the LHS of the family instance ‘F2 [x]’
(Use UndecidableInstances to permit this)
• In the type instance declaration for ‘F2’
NotRelaxedExamples.hs:11:15: error:
- • The type family application ‘F3 [Char]’
- is no smaller than the instance head ‘F3 Bool’
+ • The type-family application ‘F3 [Char]’
+ is no smaller than the LHS of the family instance ‘F3 Bool’
(Use UndecidableInstances to permit this)
• In the type instance declaration for ‘F3’
diff --git a/testsuite/tests/indexed-types/should_fail/T10817.stderr b/testsuite/tests/indexed-types/should_fail/T10817.stderr
index af8acae33a83..b6851fe0f605 100644
--- a/testsuite/tests/indexed-types/should_fail/T10817.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T10817.stderr
@@ -1,7 +1,7 @@
T10817.hs:9:3: error:
- • The type family application ‘F a’
- is no smaller than the instance head ‘F a’
+ • The type-family application ‘F a’
+ is no smaller than the LHS of the family instance ‘F a’
(Use UndecidableInstances to permit this)
• In the default type instance declaration for ‘F’
In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T13271.stderr b/testsuite/tests/indexed-types/should_fail/T13271.stderr
index 4a8e7ebd2031..81af4cbbab84 100644
--- a/testsuite/tests/indexed-types/should_fail/T13271.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13271.stderr
@@ -13,10 +13,3 @@ T13271.hs:13:3: error: [GHC-05175]
X 2 = T2 -- Defined at T13271.hs:13:3
• In the equations for closed type family ‘X’
In the type family declaration for ‘X’
-
-T13271.hs:13:3: error:
- • The type family application ‘(TypeError ...)’
- is no smaller than the instance head ‘X 2’
- (Use UndecidableInstances to permit this)
- • In the equations for closed type family ‘X’
- In the type family declaration for ‘X’
diff --git a/testsuite/tests/indexed-types/should_fail/T15172.stderr b/testsuite/tests/indexed-types/should_fail/T15172.stderr
index 8c28c5148c7c..b96110905515 100644
--- a/testsuite/tests/indexed-types/should_fail/T15172.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15172.stderr
@@ -1,5 +1,5 @@
T15172.hs:11:10: error:
- • Illegal nested constraint ‘F a’
+ • Illegal use of type family ‘F’ in the constraint ‘F a’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘C [[a]]’
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr b/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
index 4ac7e2537c9e..2e111b9effa1 100644
--- a/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
+++ b/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
@@ -1,18 +1,19 @@
TyFamUndec.hs:6:15: error:
• Variable ‘b’ occurs more often
- in the type family application ‘T (b, b)’
- than in the instance head ‘T (a, [b])’
+ in the type-family application ‘T (b, b)’
+ than in the LHS of the family instance ‘T (a, [b])’
(Use UndecidableInstances to permit this)
• In the type instance declaration for ‘T’
TyFamUndec.hs:7:15: error:
- • The type family application ‘T (a, Maybe b)’
- is no smaller than the instance head ‘T (a, Maybe b)’
+ • The type-family application ‘T (a, Maybe b)’
+ is no smaller than the LHS of the family instance ‘T (a, Maybe b)’
(Use UndecidableInstances to permit this)
• In the type instance declaration for ‘T’
TyFamUndec.hs:8:15: error:
- • Illegal nested type family application ‘T (a, T b)’
+ • Illegal nested use of type family ‘T’
+ in the arguments of the type-family application ‘T (a, T b)’
(Use UndecidableInstances to permit this)
• In the type instance declaration for ‘T’
diff --git a/testsuite/tests/quantified-constraints/T19690.hs b/testsuite/tests/quantified-constraints/T19690.hs
new file mode 100644
index 000000000000..924ad359519c
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T19690.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses, ConstraintKinds, FlexibleInstances,
+ GADTs, QuantifiedConstraints, TypeApplications, ScopedTypeVariables #-}
+
+module T19690 where
+
+class c => Hold c
+instance c => Hold c
+
+data Dict c = c => Dict
+
+anythingDict :: Dict c
+anythingDict = go
+ where
+ go :: (Hold c => c) => Dict c
+ go = Dict
diff --git a/testsuite/tests/quantified-constraints/T19690.stderr b/testsuite/tests/quantified-constraints/T19690.stderr
new file mode 100644
index 000000000000..38c4dcda6435
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T19690.stderr
@@ -0,0 +1,16 @@
+
+T19690.hs:12:16: error: [GHC-05617]
+ • Could not deduce ‘c’
+ arising from the head of a quantified constraint
+ arising from a use of ‘go’
+ from the context: Hold c
+ bound by a quantified context at T19690.hs:12:16-17
+ • In the expression: go
+ In an equation for ‘anythingDict’:
+ anythingDict
+ = go
+ where
+ go :: (Hold c => c) => Dict c
+ go = Dict
+ • Relevant bindings include
+ anythingDict :: Dict c (bound at T19690.hs:12:1)
diff --git a/testsuite/tests/quantified-constraints/T19921.stderr b/testsuite/tests/quantified-constraints/T19921.stderr
index 4ebc2d227f5b..7284fbdbf7f2 100644
--- a/testsuite/tests/quantified-constraints/T19921.stderr
+++ b/testsuite/tests/quantified-constraints/T19921.stderr
@@ -1,6 +1,9 @@
T19921.hs:29:8: error: [GHC-05617]
- • Could not deduce ‘r’ arising from a use of ‘Dict’
+ • Could not deduce ‘r’
+ arising from the head of a quantified constraint
+ arising from the head of a quantified constraint
+ arising from a use of ‘Dict’
from the context: (x \/ y) \/ z
bound by a quantified context at T19921.hs:29:8-11
or from: (x ⇒ r, (y \/ z) ⇒ r)
diff --git a/testsuite/tests/quantified-constraints/T21006.stderr b/testsuite/tests/quantified-constraints/T21006.stderr
index 1abacf8eb5a3..7eb7c88a0736 100644
--- a/testsuite/tests/quantified-constraints/T21006.stderr
+++ b/testsuite/tests/quantified-constraints/T21006.stderr
@@ -1,6 +1,7 @@
T21006.hs:14:10: error: [GHC-05617]
• Could not deduce ‘c’
+ arising from the head of a quantified constraint
arising from the superclasses of an instance declaration
from the context: (Determines b, Determines c)
bound by a quantified context at T21006.hs:14:10-15
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index fba21ff79dd8..b3d0eb920f96 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -40,3 +40,4 @@ test('T22216c', normal, compile, [''])
test('T22216d', normal, compile, [''])
test('T22216e', normal, compile, [''])
test('T22223', normal, compile, [''])
+test('T19690', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T15473.stderr b/testsuite/tests/typecheck/should_compile/T15473.stderr
index 6fdeaa115cc4..42aeee63c2ee 100644
--- a/testsuite/tests/typecheck/should_compile/T15473.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15473.stderr
@@ -1,8 +1,9 @@
T15473.hs:11:3: error:
• Variable ‘a’ occurs more often
- in the type family application ‘Undefined’
- than in the instance head ‘LetInterleave xs t ts is y z’
+ in the type-family application ‘Undefined’
+ than in the LHS of the family instance ‘LetInterleave
+ xs t ts is y z’
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘LetInterleave’
In the type family declaration for ‘LetInterleave’
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
index d34792964a59..628a78aea6d0 100644
--- a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
@@ -41,12 +41,22 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
($) (_ :: [Integer] -> Integer)
where ($) :: forall a b. (a -> b) -> a -> b
+ ($!) (_ :: [Integer] -> Integer)
+ where ($!) :: forall a b. (a -> b) -> a -> b
+ id (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
+ where id :: forall a. a -> a
+ head (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
+ where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+ last (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
+ where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+ fst (_ :: (t0 -> [Integer] -> Integer, b1)) (_ :: t0)
+ where fst :: forall a b. (a, b) -> a
+ snd (_ :: (a2, t0 -> [Integer] -> Integer)) (_ :: t0)
+ where snd :: forall a b. (a, b) -> b
return (_ :: Integer)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
pure (_ :: Integer)
where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
- ($!) (_ :: [Integer] -> Integer)
- where ($!) :: forall a b. (a -> b) -> a -> b
(>>=) (_ :: [Integer] -> a8) (_ :: a8 -> [Integer] -> Integer)
where (>>=) :: forall (m :: * -> *) a b.
Monad m =>
@@ -83,16 +93,6 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
where (<$) :: forall (f :: * -> *) a b.
Functor f =>
a -> f b -> f a
- id (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
- where id :: forall a. a -> a
- head (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
- where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
- last (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
- where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
- fst (_ :: (t0 -> [Integer] -> Integer, b1)) (_ :: t0)
- where fst :: forall a b. (a, b) -> a
- snd (_ :: (a2, t0 -> [Integer] -> Integer)) (_ :: t0)
- where snd :: forall a b. (a, b) -> b
id (_ :: [Integer] -> Integer)
where id :: forall a. a -> a
head (_ :: [[Integer] -> Integer])
@@ -117,12 +117,12 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
where seq :: forall a b. a -> b -> b
($) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
where ($) :: forall a b. (a -> b) -> a -> b
+ ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
+ where ($!) :: forall a b. (a -> b) -> a -> b
return (_ :: [Integer] -> Integer) (_ :: t0)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
pure (_ :: [Integer] -> Integer) (_ :: t0)
where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
- ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
- where ($!) :: forall a b. (a -> b) -> a -> b
abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: Integer -> [Integer] -> Integer
@@ -158,12 +158,22 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
($) (_ :: Integer -> [Integer] -> Integer)
where ($) :: forall a b. (a -> b) -> a -> b
+ ($!) (_ :: Integer -> [Integer] -> Integer)
+ where ($!) :: forall a b. (a -> b) -> a -> b
+ id (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
+ where id :: forall a. a -> a
+ head (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
+ where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+ last (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
+ where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+ fst (_ :: (t0 -> Integer -> [Integer] -> Integer, b1)) (_ :: t0)
+ where fst :: forall a b. (a, b) -> a
+ snd (_ :: (a2, t0 -> Integer -> [Integer] -> Integer)) (_ :: t0)
+ where snd :: forall a b. (a, b) -> b
return (_ :: [Integer] -> Integer)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
pure (_ :: [Integer] -> Integer)
where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
- ($!) (_ :: Integer -> [Integer] -> Integer)
- where ($!) :: forall a b. (a -> b) -> a -> b
(>>=) (_ :: Integer -> a8)
(_ :: a8 -> Integer -> [Integer] -> Integer)
where (>>=) :: forall (m :: * -> *) a b.
@@ -203,16 +213,6 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
where (<$) :: forall (f :: * -> *) a b.
Functor f =>
a -> f b -> f a
- id (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
- where id :: forall a. a -> a
- head (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
- where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
- last (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
- where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
- fst (_ :: (t0 -> Integer -> [Integer] -> Integer, b1)) (_ :: t0)
- where fst :: forall a b. (a, b) -> a
- snd (_ :: (a2, t0 -> Integer -> [Integer] -> Integer)) (_ :: t0)
- where snd :: forall a b. (a, b) -> b
id (_ :: Integer -> [Integer] -> Integer)
where id :: forall a. a -> a
head (_ :: [Integer -> [Integer] -> Integer])
@@ -239,9 +239,9 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
where seq :: forall a b. a -> b -> b
($) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
where ($) :: forall a b. (a -> b) -> a -> b
+ ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
+ where ($!) :: forall a b. (a -> b) -> a -> b
return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
- ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
- where ($!) :: forall a b. (a -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
index 65e213a21b0c..44fa618172d0 100644
--- a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
@@ -36,12 +36,12 @@ constraint_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
where const :: forall a b. a -> b -> a
($) (_ :: [a] -> a)
where ($) :: forall a b. (a -> b) -> a -> b
+ ($!) (_ :: [a] -> a)
+ where ($!) :: forall a b. (a -> b) -> a -> b
return (_ :: a)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
pure (_ :: a)
where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
- ($!) (_ :: [a] -> a)
- where ($!) :: forall a b. (a -> b) -> a -> b
id (_ :: [a] -> a)
where id :: forall a. a -> a
head (_ :: [[a] -> a])
diff --git a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
index adb5ed75f27e..6dc4f2ba0a26 100644
--- a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
@@ -70,6 +70,11 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
with ($) @GHC.Types.LiftedRep @[Integer] @Integer
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
(and originally defined in ‘GHC.Base’))
+ ($!) (_ :: [Integer] -> Integer)
+ where ($!) :: forall a b. (a -> b) -> a -> b
+ with ($!) @GHC.Types.LiftedRep @[Integer] @Integer
+ (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+ (and originally defined in ‘GHC.Base’))
return (_ :: Integer)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
with return @((->) [Integer]) @Integer
@@ -80,11 +85,6 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
with pure @((->) [Integer]) @Integer
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
(and originally defined in ‘GHC.Base’))
- ($!) (_ :: [Integer] -> Integer)
- where ($!) :: forall a b. (a -> b) -> a -> b
- with ($!) @GHC.Types.LiftedRep @[Integer] @Integer
- (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
- (and originally defined in ‘GHC.Base’))
j (_ :: [Integer] -> Integer)
where j :: forall a. a -> a
with j @([Integer] -> Integer)
@@ -171,6 +171,11 @@ refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
with ($) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
(and originally defined in ‘GHC.Base’))
+ ($!) (_ :: Integer -> [Integer] -> Integer)
+ where ($!) :: forall a b. (a -> b) -> a -> b
+ with ($!) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
+ (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+ (and originally defined in ‘GHC.Base’))
return (_ :: [Integer] -> Integer)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
with return @((->) Integer) @([Integer] -> Integer)
@@ -181,11 +186,6 @@ refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
with pure @((->) Integer) @([Integer] -> Integer)
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
(and originally defined in ‘GHC.Base’))
- ($!) (_ :: Integer -> [Integer] -> Integer)
- where ($!) :: forall a b. (a -> b) -> a -> b
- with ($!) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
- (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
- (and originally defined in ‘GHC.Base’))
j (_ :: Integer -> [Integer] -> Integer)
where j :: forall a. a -> a
with j @(Integer -> [Integer] -> Integer)
diff --git a/testsuite/tests/typecheck/should_fail/T14884.stderr b/testsuite/tests/typecheck/should_fail/T14884.stderr
index 30e1ffbbfcad..5ce38cdecbe1 100644
--- a/testsuite/tests/typecheck/should_fail/T14884.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14884.stderr
@@ -18,6 +18,10 @@ T14884.hs:4:5: error: [GHC-88464]
with foldMap @[] @(IO ()) @Char
(imported from ‘Prelude’ at T14884.hs:1:8-13
(and originally defined in ‘Data.Foldable’))
+ id :: forall a. a -> a
+ with id @(String -> IO ())
+ (imported from ‘Prelude’ at T14884.hs:1:8-13
+ (and originally defined in ‘GHC.Base’))
($) :: forall a b. (a -> b) -> a -> b
with ($) @GHC.Types.LiftedRep @String @(IO ())
(imported from ‘Prelude’ at T14884.hs:1:8-13
@@ -26,10 +30,6 @@ T14884.hs:4:5: error: [GHC-88464]
with ($!) @GHC.Types.LiftedRep @String @(IO ())
(imported from ‘Prelude’ at T14884.hs:1:8-13
(and originally defined in ‘GHC.Base’))
- id :: forall a. a -> a
- with id @(String -> IO ())
- (imported from ‘Prelude’ at T14884.hs:1:8-13
- (and originally defined in ‘GHC.Base’))
T14884.hs:4:7: error: [GHC-39999]
• Ambiguous type variable ‘a0’ arising from a use of ‘print’
@@ -40,7 +40,7 @@ T14884.hs:4:7: error: [GHC-39999]
-- Defined in ‘Data.Either’
instance Show Ordering -- Defined in ‘GHC.Show’
...plus 26 others
- ...plus 28 instances involving out-of-scope types
+ ...plus 29 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘_’, namely ‘print’
In the expression: _ print "abc"
diff --git a/testsuite/tests/typecheck/should_fail/T15552a.stderr b/testsuite/tests/typecheck/should_fail/T15552a.stderr
index f7a6094d9ec4..af168c8d082a 100644
--- a/testsuite/tests/typecheck/should_fail/T15552a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15552a.stderr
@@ -1,21 +1,24 @@
T15552a.hs:26:9: error:
- • Illegal nested type family application ‘GetEntryOfVal
- (FirstEntryOfVal v kvs)’
+ • Illegal nested use of type family ‘FirstEntryOfVal’
+ in the arguments of the type-family application ‘GetEntryOfVal
+ (FirstEntryOfVal v kvs)’
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘FirstEntryOfVal’
In the type family declaration for ‘FirstEntryOfVal’
T15552a.hs:26:9: error:
- • Illegal nested type family application ‘EntryOfValKey
- (FirstEntryOfVal v kvs)’
+ • Illegal nested use of type family ‘FirstEntryOfVal’
+ in the arguments of the type-family application ‘EntryOfValKey
+ (FirstEntryOfVal v kvs)’
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘FirstEntryOfVal’
In the type family declaration for ‘FirstEntryOfVal’
T15552a.hs:26:9: error:
- • Illegal nested type family application ‘EntryOfValKey
- (FirstEntryOfVal v kvs)’
+ • Illegal nested use of type family ‘FirstEntryOfVal’
+ in the arguments of the type-family application ‘EntryOfValKey
+ (FirstEntryOfVal v kvs)’
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘FirstEntryOfVal’
In the type family declaration for ‘FirstEntryOfVal’
diff --git a/testsuite/tests/typecheck/should_fail/T15801.stderr b/testsuite/tests/typecheck/should_fail/T15801.stderr
index 9c7cdabeefea..922fae41a735 100644
--- a/testsuite/tests/typecheck/should_fail/T15801.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15801.stderr
@@ -2,5 +2,6 @@
T15801.hs:52:10: error: [GHC-18872]
• Couldn't match representation of type: UnOp op_a -> UnOp b
with that of: op_a --> b
+ arising from the head of a quantified constraint
arising from the superclasses of an instance declaration
• In the instance declaration for ‘OpRÃki (Op (*))’
diff --git a/testsuite/tests/typecheck/should_fail/T20666.hs b/testsuite/tests/typecheck/should_fail/T20666.hs
new file mode 100644
index 000000000000..279c8f4b7d18
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+type family T t
+type family S s
+
+class Show (T c) => C1 c
+class Show (T (S d)) => D d
+instance (D d, c ~ S d) => C1 c
+ -- this one fails in GHC 9.2
+
+class Show (T c) => C2 c
+instance (D d, c ~ S d, c' ~ c) => C2 c'
+ -- This one succeeded because it went via lookupInInerts.
+ -- It should fail, just like the one above.
diff --git a/testsuite/tests/typecheck/should_fail/T20666.stderr b/testsuite/tests/typecheck/should_fail/T20666.stderr
new file mode 100644
index 000000000000..bc2aad54971a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666.stderr
@@ -0,0 +1,20 @@
+
+T20666.hs:13:10: error: [GHC-39999]
+ • Could not deduce ‘Show (T c)’
+ arising from the superclasses of an instance declaration
+ from the context: (D d, c ~ S d)
+ bound by the instance declaration at T20666.hs:13:10-31
+ Possible fix:
+ If the constraint looks soluble from a superclass of the instance context,
+ read 'Undecidable instances and loopy superclasses' in the user manual
+ • In the instance declaration for ‘C1 c’
+
+T20666.hs:17:10: error: [GHC-39999]
+ • Could not deduce ‘Show (T c)’
+ arising from the superclasses of an instance declaration
+ from the context: (D d, c ~ S d, c' ~ c)
+ bound by the instance declaration at T20666.hs:17:10-40
+ Possible fix:
+ If the constraint looks soluble from a superclass of the instance context,
+ read 'Undecidable instances and loopy superclasses' in the user manual
+ • In the instance declaration for ‘C2 c'’
diff --git a/testsuite/tests/typecheck/should_fail/T20666a.hs b/testsuite/tests/typecheck/should_fail/T20666a.hs
new file mode 100644
index 000000000000..b1e4d2c174e2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T20666a where
+
+type family F a
+
+class Eq (F a) => D a
+class Eq (F a) => C a
+
+instance D [a] => C [a]
+
diff --git a/testsuite/tests/typecheck/should_fail/T20666a.stderr b/testsuite/tests/typecheck/should_fail/T20666a.stderr
new file mode 100644
index 000000000000..4192b88807c7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666a.stderr
@@ -0,0 +1,10 @@
+
+T20666a.hs:11:10: error: [GHC-39999]
+ • Could not deduce ‘Eq (F [a])’
+ arising from the superclasses of an instance declaration
+ from the context: D [a]
+ bound by the instance declaration at T20666a.hs:11:10-23
+ Possible fix:
+ If the constraint looks soluble from a superclass of the instance context,
+ read 'Undecidable instances and loopy superclasses' in the user manual
+ • In the instance declaration for ‘C [a]’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index b15a50b2282e..61514e725b7f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -667,3 +667,5 @@ test('T21530a', normal, compile_fail, [''])
test('T21530b', normal, compile_fail, [''])
test('T22570', normal, compile_fail, [''])
test('T22645', normal, compile_fail, [''])
+test('T20666', normal, compile_fail, [''])
+test('T20666a', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/fd-loop.stderr b/testsuite/tests/typecheck/should_fail/fd-loop.stderr
index 86a70f5b7600..a9320c009a50 100644
--- a/testsuite/tests/typecheck/should_fail/fd-loop.stderr
+++ b/testsuite/tests/typecheck/should_fail/fd-loop.stderr
@@ -1,6 +1,6 @@
fd-loop.hs:12:10: error:
- • Variable ‘b’ occurs more often
- in the constraint ‘C a b’ than in the instance head ‘Eq (T a)’
+ • The constraint ‘C a b’
+ is no smaller than the instance head ‘Eq (T a)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Eq (T a)’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail108.stderr b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
index 4096ad36c652..2c7db0dd7182 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail108.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
@@ -1,7 +1,6 @@
tcfail108.hs:7:10: error:
- • Variable ‘f’ occurs more often
- in the constraint ‘Eq (f (Rec f))’
- than in the instance head ‘Eq (Rec f)’
+ • The constraint ‘Eq (f (Rec f))’
+ is no smaller than the instance head ‘Eq (Rec f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Eq (Rec f)’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.hs b/testsuite/tests/typecheck/should_fail/tcfail133.hs
index 4aded61a2752..a892fbca7d4d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.hs
@@ -60,11 +60,13 @@ instance Number n
=> Add (n:@Zero) One (n:@One)
instance AddDigit n One r'
=> Add (n:@One) One (r':@Zero)
-instance (Number n1, Digit d1, Number n2, Digit n2
- ,Add n1 n2 nr', AddDigit (d1:@nr') d2 r)
+instance ( Number n1, Digit d1, Number n2, Digit n2
+ , Add n1 n2 nr', AddDigit (d1:@nr') d2 r
+ , Number r) -- Added when fixing #20666
+ -- Because (AddDigit (d1:@nr') d2 r) is not
+ -- Paterson-smaller than the instance head
=> Add (n1:@d1) (n2:@d2) r
-
foo = show $ add (One:@Zero) (One:@One)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.stderr b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
index 5b2a8944e580..ff2a76fec7d7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
@@ -2,7 +2,7 @@
tcfail133.hs:2:61: warning: [-Wdeprecated-flags (in -Wdefault)]
-XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
-tcfail133.hs:68:7: error: [GHC-39999]
+tcfail133.hs:70:7: error: [GHC-39999]
• Ambiguous type variable ‘a0’ arising from a use of ‘show’
prevents the constraint ‘(Show a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
@@ -11,14 +11,14 @@ tcfail133.hs:68:7: error: [GHC-39999]
instance (Number a, Digit b, Show a, Show b) => Show (a :@ b)
-- Defined at tcfail133.hs:11:54
...plus 28 others
- ...plus 12 instances involving out-of-scope types
+ ...plus 13 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘($)’, namely ‘show’
In the expression: show $ add (One :@ Zero) (One :@ One)
In an equation for ‘foo’:
foo = show $ add (One :@ Zero) (One :@ One)
-tcfail133.hs:68:14: error: [GHC-39999]
+tcfail133.hs:70:14: error: [GHC-39999]
• No instance for ‘AddDigit (Zero :@ (One :@ One)) One a0’
arising from a use of ‘add’
• In the second argument of ‘($)’, namely
diff --git a/testsuite/tests/typecheck/should_fail/tcfail154.stderr b/testsuite/tests/typecheck/should_fail/tcfail154.stderr
index a4bda5998e64..0fdf2e135b5a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail154.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail154.stderr
@@ -1,6 +1,6 @@
tcfail154.hs:13:10: error:
- • Variable ‘a’ occurs more often
- in the constraint ‘C a a’ than in the instance head ‘Eq (T a)’
+ • The constraint ‘C a a’
+ is no smaller than the instance head ‘Eq (T a)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Eq (T a)’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail214.stderr b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
index 83fa344834e3..d0b153725e4a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail214.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
@@ -1,5 +1,5 @@
tcfail214.hs:9:10: error:
- • Illegal nested constraint ‘F a’
+ • Illegal use of type family ‘F’ in the constraint ‘F a’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘C [a]’
--
GitLab