diff options
| author | Richard Eisenberg <rae@richarde.dev> | 2021-11-22 17:34:32 -0500 |
|---|---|---|
| committer | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-01-11 08:30:42 +0000 |
| commit | aed1974e92366ab8e117734f308505684f70cddf (patch) | |
| tree | bbfe7fdd00f1e0ef8dacdcf8d070a07efa38561b | |
| parent | 083f701553852c4460159cd6deb2515d3373714d (diff) | |
| download | haskell-aed1974e92366ab8e117734f308505684f70cddf.tar.gz | |
Refactor the treatment of loopy superclass dictswip/T20666
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.
54 files changed, 1293 insertions, 794 deletions
diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs index bb7315074f..f06f12e89a 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 3685876fa4..689503ef89 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 4917b21a77..4d7bf81f6c 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 feba275d75..e90811979f 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 61caa2e456..c22ab6a2e5 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 8d18cad2a2..2e17295073 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 0ea0412339..bf15393048 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 cdc15959f8..6fc5b28ab0 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 33ee8e854c..02ce8115ad 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 b3dcb3f5b1..5dc3431b9a 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 c3aa2d2695..e69e7ae0fe 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 67c90dcd80..b5cf81ad9d 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 6fda868642..3d9b5dd550 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 2fea177885..0623acd3d5 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 72ed58b041..4a40528f1f 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 a73c01c90f..f11b900d6e 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 0b6b519028..b8249bc363 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 5824c3e7f6..89614378cd 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 28894d68ed..dc6bbe746b 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 41faa2fece..eea0ed95ef 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 ff1c616974..6bd86a81f0 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 7776a7f833..84276527a3 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 e2521f2de0..098b6e829a 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 16e7cf320d..2e073e6f3c 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 c0ceabf920..99e2c5fdbb 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 5fb876b8c5..97c35bf70a 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 500be78a5f..733d90eafc 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 af8acae33a..b6851fe0f6 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 4a8e7ebd20..81af4cbbab 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 8c28c5148c..b961109055 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 4ac7e2537c..2e111b9eff 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 0000000000..924ad35951 --- /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 0000000000..38c4dcda64 --- /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 4ebc2d227f..7284fbdbf7 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 1abacf8eb5..7eb7c88a07 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 fba21ff79d..b3d0eb920f 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 6fdeaa115c..42aeee63c2 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 d34792964a..628a78aea6 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 65e213a21b..44fa618172 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 adb5ed75f2..6dc4f2ba0a 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 30e1ffbbfc..5ce38cdecb 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 f7a6094d9e..af168c8d08 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 9c7cdabeef..922fae41a7 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 0000000000..279c8f4b7d --- /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 0000000000..bc2aad5497 --- /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 0000000000..b1e4d2c174 --- /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 0000000000..4192b88807 --- /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 b15a50b228..61514e725b 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 86a70f5b76..a9320c009a 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 4096ad36c6..2c7db0dd71 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 4aded61a27..a892fbca7d 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 5b2a8944e5..ff2a76fec7 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 a4bda5998e..0fdf2e135b 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 83fa344834..d0b153725e 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]’ |