diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2015-12-15 14:26:13 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2015-12-15 14:33:32 +0000 |
| commit | 6eabb6ddb7c53784792ee26b1e0657bde7eee7fb (patch) | |
| tree | af17a00ab5a30d1ab9a9a11a4786f0f239fe82b4 | |
| parent | b8ca64592e331005def4f734e026d5418950e6e1 (diff) | |
| download | haskell-6eabb6ddb7c53784792ee26b1e0657bde7eee7fb.tar.gz | |
Allow recursive (undecidable) superclasses
This patch fulfils the request in Trac #11067, #10318, and #10592,
by lifting the conservative restrictions on superclass constraints.
These restrictions are there (and have been since Haskell was born) to
ensure that the transitive superclasses of a class constraint is a finite
set. However (a) this restriction is conservative, and can be annoying
when there really is no recursion, and (b) sometimes genuinely recursive
superclasses are useful (see the tickets).
Dimitrios and I worked out that there is actually a relatively simple way
to do the job. It’s described in some detail in
Note [The superclass story] in TcCanonical
Note [Expanding superclasses] in TcType
In brief, the idea is to expand superclasses only finitely, but to
iterate (using a loop that already existed) if there are more
superclasses to explore.
Other small things
- I improved grouping of error messages a bit in TcErrors
- I re-centred the haddock.compiler test, which was at 9.8%
above the norm, and which this patch pushed slightly over
57 files changed, 899 insertions, 686 deletions
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 98a363122c..63729182dc 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -565,6 +565,7 @@ data ExtensionFlag | Opt_OverlappingInstances | Opt_UndecidableInstances | Opt_IncoherentInstances + | Opt_UndecidableSuperClasses | Opt_MonomorphismRestriction | Opt_MonoPatBinds | Opt_MonoLocalBinds @@ -3261,6 +3262,7 @@ xFlags = [ flagSpec "TypeSynonymInstances" Opt_TypeSynonymInstances, flagSpec "UnboxedTuples" Opt_UnboxedTuples, flagSpec "UndecidableInstances" Opt_UndecidableInstances, + flagSpec "UndecidableSuperClasses" Opt_UndecidableSuperClasses, flagSpec "UnicodeSyntax" Opt_UnicodeSyntax, flagSpec "UnliftedFFITypes" Opt_UnliftedFFITypes, flagSpec "ViewPatterns" Opt_ViewPatterns diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 7ac2a9a3ab..4edc31207d 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -3,7 +3,7 @@ module TcCanonical( canonicalize, unifyDerived, - + makeSuperClasses, mkGivensWithSuperClasses, StopOrContinue(..), stopWith, continueWith ) where @@ -27,6 +27,7 @@ import OccName( OccName ) import Outputable import DynFlags( DynFlags ) import VarSet +import NameSet import RdrName import Pair @@ -147,11 +148,11 @@ canonicalize ct@(CNonCanonical { cc_ev = ev }) ; {-# SCC "canEvVar" #-} canEvNC ev } -canonicalize (CDictCan { cc_ev = ev - , cc_class = cls - , cc_tyargs = xis }) +canonicalize (CDictCan { cc_ev = ev, cc_class = cls + , cc_tyargs = xis, cc_pend_sc = pend_sc }) = {-# SCC "canClass" #-} - canClass ev cls xis -- Do not add any superclasses + canClass ev cls xis pend_sc + canonicalize (CTyEqCan { cc_ev = ev , cc_tyvar = tv , cc_rhs = xi @@ -191,59 +192,118 @@ canEvNC ev ************************************************************************ -} -canClass, canClassNC - :: CtEvidence - -> Class -> [Type] -> TcS (StopOrContinue Ct) +canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct) -- Precondition: EvVar is class evidence +canClassNC ev cls tys = canClass ev cls tys (has_scs cls) + where + has_scs cls = not (null (classSCTheta cls)) --- The canClassNC version is used on non-canonical constraints --- and adds superclasses. The plain canClass version is used --- for already-canonical class constraints (but which might have --- been subsituted or somthing), and hence do not need superclasses - -canClassNC ev cls tys - = canClass ev cls tys - `andWhenContinue` emitSuperclasses +canClass :: CtEvidence -> Class -> [Type] -> Bool -> TcS (StopOrContinue Ct) +-- Precondition: EvVar is class evidence -canClass ev cls tys +canClass ev cls tys pend_sc = -- all classes do *nominal* matching ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys ) do { (xis, cos) <- flattenManyNom ev tys ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos xi = mkClassPred cls xis mk_ct new_ev = CDictCan { cc_ev = new_ev - , cc_tyargs = xis, cc_class = cls } + , cc_tyargs = xis + , cc_class = cls + , cc_pend_sc = pend_sc } ; mb <- rewriteEvidence ev xi co ; traceTcS "canClass" (vcat [ ppr ev , ppr xi, ppr mb ]) ; return (fmap mk_ct mb) } -emitSuperclasses :: Ct -> TcS (StopOrContinue Ct) -emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls }) - -- Add superclasses of this one here, See Note [Adding superclasses]. - -- But only if we are not simplifying the LHS of a rule. - = do { newSCWorkFromFlavored ev cls xis_new - -- Arguably we should "seq" the coercions if they are derived, - -- as we do below for emit_kind_constraint, to allow errors in - -- superclasses to be executed if deferred to runtime! - ; continueWith ct } -emitSuperclasses _ = panic "emit_superclasses of non-class!" - -{- Note [Adding superclasses] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Since dictionaries are canonicalized only once in their lifetime, the -place to add their superclasses is canonicalisation. See Note [Add -superclasses only during canonicalisation]. Here is what we do: - - Givens: Add all their superclasses as Givens. - They may be needed to prove Wanteds. - - Wanteds/Derived: - Add all their superclasses as Derived. - The sole reason is to expose functional dependencies - in superclasses or equality superclasses. - -Examples of how adding superclasses as Derived is useful +{- Note [The superclass story] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We need to add superclass constraints for two reasons: + +* For givens, they give us a route to to proof. E.g. + f :: Ord a => a -> Bool + f x = x == x + We get a Wanted (Eq a), which can only be solved from the superclass + of the Given (Ord a). + +* For wanteds, they may give useful functional dependencies. E.g. + class C a b | a -> b where ... + class C a b => D a b where ... + Now a Wanted constraint (D Int beta) has (C Int beta) as a superclass + and that might tell us about beta, via C's fundeps. We can get this + by generateing a Derived (C Int beta) constraint. It's derived because + we don't actually have to cough up any evidence for it; it's only there + to generate fundep equalities. + +See Note [Why adding superclasses can help]. + +For these reasons we want to generate superclass constraints for both +Givens and Wanteds. But: + +* (Minor) they are often not needed, so generating them aggressively + is a waste of time. + +* (Major) if we want recursive superclasses, there would be an infinite + number of them. Here is a real-life example (Trac #10318); + + class (Frac (Frac a) ~ Frac a, + Fractional (Frac a), + IntegralDomain (Frac a)) + => IntegralDomain a where + type Frac a :: * + + Notice that IntegralDomain has an associated type Frac, and one + of IntegralDomain's superclasses is another IntegralDomain constraint. + +So here's the plan: + +1. Generate superclasses for given (but not wanted) constraints; + see Note [Aggressively expand given superclasses]. However + stop if you encounter the same class twice. That is, expand + eagerly, but have a conservative termination condition: see + Note [Expanding superclasses] in TcType. + +2. Solve the wanteds as usual, but do /no/ expansion of superclasses + in solveSimpleGivens or solveSimpleWanteds. + See Note [Danger of adding superclasses during solving] + +3. If we have any remaining unsolved wanteds, try harder: + take both the Givens and Wanteds, and expand superclasses again. + This may succeed in generating (a finite number of) extra Givens, + and extra Deriveds. Both may help the proof. + This is done in TcSimplify.expandSuperClasses. + +4. Go round to (2) again. This loop (2,3,4) is implemented + in TcSimplify.simpl_loop. + +We try to terminate the loop by flagging which class constraints +(given or wanted) are potentially un-expanded. This is what the +cc_pend_sc flag is for in CDictCan. So in Step 3 we only expand +superclasses for constraints with cc_pend_sc set to true (i.e. +isPendingScDict holds). + +When we take a CNonCanonical or CIrredCan, but end up classifying it +as a CDictCan, we set the cc_pend_sc flag to False. + +Note [Aggressively expand given superclasses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In step (1) of Note [The superclass story], why do we aggressively +expand Given superclasses by one layer? Mainly because of some very +obscure cases like this: + + instance Bad a => Eq (T a) + + f :: (Ord (T a)) => blah + f x = ....needs Eq (T a), Ord (T a).... + +Here if we can't satisfy (Eq (T a)) from the givens we'll use the +instance declaration; but then we are stuck with (Bad a). Sigh. +This is really a case of non-confluent proofs, but to stop our users +complaining we expand one layer in advance. + +Note [Why adding superclasses can help] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Examples of how adding superclasses can help: --- Example 1 class C a b | a -> b @@ -280,34 +340,8 @@ Examples of how adding superclasses as Derived is useful [D] beta ~ b which is what we want. ----------- Historical note ----------- -Example of why adding superclass of a Wanted as a Given would -be terrible, see Note [Do not add superclasses of solved dictionaries] -in TcSMonad, which has this example: - class Ord a => C a where - instance Ord [a] => C [a] where ... -Suppose we are trying to solve - [G] d1 : Ord a - [W] d2 : C [a] -If we (bogusly) added the superclass of d2 as Given we'd have - [G] d1 : Ord a - [W] d2 : C [a] - [G] d3 : Ord [a] -- Superclass of d2, bogus - -Then we'll use the instance decl to give - [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d4 - [G] d3 : Ord [a] -- Superclass of d2, bogus - [W] d4: Ord [a] - -And now we could bogusly solve d4 from d3. ----------- End of historical note ----------- - -Note [Add superclasses only during canonicalisation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We add superclasses only during canonicalisation, on the passage -from CNonCanonical to CDictCan. A class constraint can be repeatedly -rewritten, and there's no point in repeatedly adding its superclasses. - +Note [Danger of adding superclasses during solving] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Here's a serious, but now out-dated example, from Trac #4497: class Num (RealOf t) => Normed t @@ -334,27 +368,70 @@ Mind you, now that Wanteds cannot rewrite Derived, I think this particular situation can't happen. -} -newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS () --- Returns superclasses, see Note [Adding superclasses] -newSCWorkFromFlavored flavor cls xis - | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor - = do { given_evs <- newGivenEvVars (mk_given_loc loc) - (mkEvScSelectors (EvId evar) cls xis) - ; emitWorkNC given_evs } +mkGivensWithSuperClasses :: CtLoc -> [EvId] -> TcS [Ct] +-- From a given EvId, make its Ct, plus the Ct's of its superclasses +-- See Note [The superclass story] +-- The loop-breaking here follows Note [Expanding superclasses] in TcType +mkGivensWithSuperClasses loc ev_ids = concatMapM go ev_ids + where + go ev_id = mk_superclasses emptyNameSet $ + CtGiven { ctev_evar = ev_id + , ctev_pred = evVarPred ev_id + , ctev_loc = loc } + +makeSuperClasses :: [Ct] -> TcS [Ct] +-- Returns strict superclasses, transitively, see Note [The superclasses story] +-- See Note [The superclass story] +-- The loop-breaking here follows Note [Expanding superclasses] in TcType +makeSuperClasses cts = concatMapM go cts + where + go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) + = mk_strict_superclasses emptyNameSet ev cls tys + go ct = pprPanic "makeSuperClasses" (ppr ct) + +mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct] +-- Return this constraint, plus its superclasses, if any +mk_superclasses rec_clss ev + | ClassPred cls tys <- classifyPredType (ctEvPred ev) + = mk_superclasses_of rec_clss ev cls tys + + | otherwise -- Superclass is not a class predicate + = return [mkNonCanonical ev] + +mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct] +-- Return this class constraint, plus its superclasses +mk_superclasses_of rec_clss ev cls tys + | loop_found + = return [this_ct] + | otherwise + = do { sc_cts <- mk_strict_superclasses rec_clss' ev cls tys + ; return (this_ct : sc_cts) } + where + cls_nm = className cls + loop_found = cls_nm `elemNameSet` rec_clss + rec_clss' | isCTupleClass cls = rec_clss -- Never contribute to recursion + | otherwise = rec_clss `extendNameSet` cls_nm + this_ct = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys + , cc_pend_sc = loop_found } + +mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct] +mk_strict_superclasses rec_clss ev cls tys + | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev + = do { sc_evs <- newGivenEvVars (mk_given_loc loc) + (mkEvScSelectors (EvId evar) cls tys) + ; concatMapM (mk_superclasses rec_clss) sc_evs } - | isEmptyVarSet (tyCoVarsOfTypes xis) - = return () -- Wanteds with no variables yield no deriveds. + + | isEmptyVarSet (tyCoVarsOfTypes tys) + = return [] -- Wanteds with no variables yield no deriveds. -- See Note [Improvement from Ground Wanteds] | otherwise -- Wanted/Derived case, just add those SC that can lead to improvement. - = do { let sc_rec_theta = transSuperClasses cls xis - impr_theta = filter isImprovementPred sc_rec_theta - loc = ctEvLoc flavor - ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta - ; emitNewDeriveds loc impr_theta } - + = do { let loc = ctEvLoc ev + ; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys) + ; concatMapM (mk_superclasses rec_clss) sc_evs } where - size = sizeTypes xis + size = sizeTypes tys mk_given_loc loc | isCTupleClass cls = loc -- For tuple predicates, just take them apart, without @@ -373,6 +450,8 @@ newSCWorkFromFlavored flavor cls xis | otherwise -- Probably doesn't happen, since this function = loc -- is only used for Givens, but does no harm + + {- ************************************************************************ * * @@ -1876,3 +1955,4 @@ unify_derived loc role orig_ty1 orig_ty2 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion maybeSym IsSwapped co = mkTcSymCo co maybeSym NotSwapped co = co + diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 94cd9ad433..e23c750434 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -345,7 +345,7 @@ warnRedundantConstraints ctxt env info ev_vars _ -> ev_vars improving ev_var = any isImprovementPred $ - transSuperClassesPred (idType ev_var) + transSuperClasses (idType ev_var) {- Note [Redundant constraints in instance decls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -406,8 +406,9 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl True, mkUserTypeErrorReporter) , ("insoluble1", is_given_eq, True, mkGroupReporter mkEqErr) , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr) - , ("insoluble3", rigid_nom_tv_eq, True, mkSkolReporter) - , ("insoluble4", rigid_nom_eq, True, mkGroupReporter mkEqErr) + , ("skolem eq1", very_wrong, True, mkSkolReporter) + , ("skolem eq2", skolem_eq, True, mkSkolReporter) + , ("non-tv eq", non_tv_eq, True, mkSkolReporter) , ("Out of scope", is_out_of_scope, True, mkHoleReporter) , ("Holes", is_hole, False, mkHoleReporter) @@ -420,28 +421,41 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] - rigid_nom_eq, rigid_nom_tv_eq, is_hole, is_dict, + -- rigid_nom_eq, rigid_nom_tv_eq, + is_hole, is_dict, is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool - utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2 - utterly_wrong _ _ = False - - is_out_of_scope ct _ = isOutOfScopeCt ct - is_hole ct _ = isHoleCt ct - is_given_eq ct pred | EqPred {} <- pred = arisesFromGivens ct | otherwise = False -- I think all given residuals are equalities - is_user_type_error ct _ = isUserTypeErrorCt ct + -- Things like (Int ~N Bool) + utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2 + utterly_wrong _ _ = False + + -- Things like (a ~N Int) + very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2 + very_wrong _ _ = False + + -- Things like (a ~N b) or (a ~N F Bool) + skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1 + skolem_eq _ _ = False - -- Skolem (i.e. non-meta) type variable on the left - rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred + -- Things like (F a ~N Int) + non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1) + non_tv_eq _ _ = False - rigid_nom_tv_eq _ pred - | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1 - | otherwise = False +-- rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred +-- +-- rigid_nom_tv_eq _ pred +-- | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1 +-- | otherwise = False + + is_out_of_scope ct _ = isOutOfScopeCt ct + is_hole ct _ = isHoleCt ct + + is_user_type_error ct _ = isUserTypeErrorCt ct is_equality _ (EqPred {}) = True is_equality _ _ = False @@ -457,6 +471,15 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl --------------- +isSkolemTy :: TcLevel -> Type -> Bool +isSkolemTy tc_lvl ty + = case getTyVar_maybe ty of + Nothing -> False + Just tv -> isSkolemTyVar tv + || (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv) + -- The latter case is for touchable SigTvs + -- we postpone untouchables to a latter test (too obscure) + isTyFun_maybe :: Type -> Maybe TyCon isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of Just (tc,_) | isTypeFamilyTyCon tc -> Just tc @@ -476,15 +499,19 @@ type ReporterSpec , Reporter) -- The reporter itself mkSkolReporter :: Reporter --- Suppress duplicates with the same LHS +-- Suppress duplicates with either the same LHS, or same location mkSkolReporter ctxt cts - = mapM_ (reportGroup mkEqErr ctxt) (equivClasses cmp_lhs_type cts) + = mapM_ (reportGroup mkEqErr ctxt) (group cts) where - cmp_lhs_type ct1 ct2 - = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of - (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) -> - (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2) - _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2) + group [] = [] + group (ct:cts) = (ct : yeses) : group noes + where + (yeses, noes) = partition (group_with ct) cts + + group_with ct1 ct2 + | EQ <- cmp_loc ct1 ct2 = True + | EQ <- cmp_lhs_type ct1 ct2 = True + | otherwise = False mkHoleReporter :: Reporter -- Reports errors one at a time @@ -515,7 +542,16 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) mkGroupReporter mk_err ctxt cts = mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts) where - cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2) + +cmp_lhs_type :: Ct -> Ct -> Ordering +cmp_lhs_type ct1 ct2 + = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of + (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) -> + (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2) + _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2) + +cmp_loc :: Ct -> Ct -> Ordering +cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2) reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt -> [Ct] -> TcM () diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index c78d6bbaf2..c044d20b0d 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -1,7 +1,7 @@ {-# LANGUAGE CPP #-} module TcInteract ( - solveSimpleGivens, -- Solves [EvVar],GivenLoc + solveSimpleGivens, -- Solves [Ct] solveSimpleWanteds, -- Solves Cts solveCallStack, -- for use in TcSimplify @@ -132,24 +132,18 @@ that prepareInertsForImplications will discard the insolubles, so we must keep track of them separately. -} -solveSimpleGivens :: CtLoc -> [EvVar] -> TcS Cts --- Solves the givens, adding them to the inert set --- Returns any insoluble givens, which represent inaccessible code, --- taking those ones out of the inert set -solveSimpleGivens loc givens +solveSimpleGivens :: [Ct] -> TcS Cts +solveSimpleGivens givens | null givens -- Shortcut for common case = return emptyCts | otherwise - = do { go (map mk_given_ct givens) + = do { go givens ; takeGivenInsolubles } where - mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id - , ctev_pred = evVarPred ev_id - , ctev_loc = loc }) go givens = do { solveSimples (listToBag givens) ; new_givens <- runTcPluginsGiven - ; when (notNull new_givens) (go new_givens) - } + ; when (notNull new_givens) $ + go new_givens } solveSimpleWanteds :: Cts -> TcS WantedConstraints -- NB: 'simples' may contain /derived/ equalities, floated diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 94b74784ba..a6a6fa1a1a 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -81,7 +81,7 @@ module TcRnTypes( toDerivedWC, andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols, - isDroppableDerivedLoc, insolubleImplic, trulyInsoluble, + isDroppableDerivedLoc, insolubleImplic, arisesFromGivens, Implication(..), ImplicStatus(..), isInsolubleStatus, @@ -1339,7 +1339,13 @@ data Ct = CDictCan { -- e.g. Num xi cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] cc_class :: Class, - cc_tyargs :: [Xi] -- cc_tyargs are function-free, hence Xi + cc_tyargs :: [Xi], -- cc_tyargs are function-free, hence Xi + cc_pend_sc :: Bool -- True <=> (a) cc_class has superclasses + -- (b) we have not yet added those + -- superclasses as Givens + -- NB: cc_pend_sc is used for G/W/D. For W/D the reason + -- we need superclasses is to expose possible improvement + -- via fundeps } | CIrredEvCan { -- These stand for yet-unusable predicates @@ -1872,11 +1878,11 @@ trulyInsoluble :: TcLevel -> Ct -> Bool -- The constraint is in the wc_insol set, -- but we do not treat as truly isoluble -- a) type-holes, arising from PartialTypeSignatures, --- b) an out-of-scope variable +-- (except out-of-scope variables masquerading as type-holes) -- Yuk! -trulyInsoluble tc_lvl insol - = isOutOfScopeCt insol - || isRigidEqPred tc_lvl (classifyPredType (ctPred insol)) +trulyInsoluble _tc_lvl insol + | CHoleCan {} <- insol = isOutOfScopeCt insol + | otherwise = True instance Outputable WantedConstraints where ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n}) diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 1cc7533d5a..ac38e171b8 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -51,7 +51,7 @@ module TcSMonad ( emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles, matchableGivens, prohibitedSuperClassSolve, getUnsolvedInerts, - removeInertCts, + removeInertCts, getPendingScDicts, isPendingScDict, addInertCan, addInertEq, insertFunEq, emitInsoluble, emitWorkNC, emitWorkCt, @@ -558,9 +558,7 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- (b) emitDerivedShadows , inert_dicts :: DictMap Ct - -- Dictionaries only, index is the class - -- NB: index is /not/ the whole type because FD reactions - -- need to match the class but not necessarily the whole type. + -- Dictionaries only , inert_safehask :: DictMap Ct -- Failed dictionary resolution due to Safe Haskell overlapping @@ -1568,7 +1566,7 @@ After solving the Givens we take two things out of the inert set a) The insolubles; we return these to report inaccessible code We return these separately. We don't want to leave them in - the inert set, lest we onfuse them with insolubles arising from + the inert set, lest we confuse them with insolubles arising from solving wanteds b) Any Derived CFunEqCans. Derived CTyEqCans are in the @@ -1633,6 +1631,35 @@ getInertGivens $ concat (varEnvElts (inert_eqs inerts)) ; return (filter isGivenCt all_cts) } +getPendingScDicts :: TcS [Ct] +-- Find all inert Given dictionaries whose cc_pend_sc flag is True +-- Set the flag to False in the inert set, and return that Ct +getPendingScDicts = updRetInertCans get_sc_dicts + where + get_sc_dicts ic@(IC { inert_dicts = dicts }) + = (sc_pend_dicts, ic') + where + ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts } + + sc_pend_dicts :: [Ct] + sc_pend_dicts = foldDicts get_pending dicts [] + + get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True + -- but flipping the flag + get_pending dict dicts + | Just dict' <- isPendingScDict dict = dict' : dicts + | otherwise = dicts + + add :: Ct -> DictMap Ct -> DictMap Ct + add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts + = addDict dicts cls tys ct + add ct _ = pprPanic "getPendingScDicts" (ppr ct) + +isPendingScDict :: Ct -> Maybe Ct +isPendingScDict ct@(CDictCan { cc_pend_sc = True }) + = Just (ct { cc_pend_sc = False }) +isPendingScDict _ = Nothing + getUnsolvedInerts :: TcS ( Bag Implication , Cts -- Tyvar eqs: a ~ ty , Cts -- Fun eqs: F a ~ ty diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 261abd0991..c6aae95baa 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -31,6 +31,7 @@ import PrelNames import TcErrors import TcEvidence import TcInteract +import TcCanonical ( makeSuperClasses, mkGivensWithSuperClasses ) import TcMType as TcM import TcRnMonad as TcM import TcSMonad as TcS @@ -422,18 +423,36 @@ simplifyDefault theta ------------------ tcCheckSatisfiability :: Bag EvVar -> TcM Bool -- Return True if satisfiable, False if definitely contradictory -tcCheckSatisfiability givens +tcCheckSatisfiability given_ids = do { lcl_env <- TcM.getLclEnv ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env - ; traceTc "checkSatisfiability {" (ppr givens) ; (res, _ev_binds) <- runTcS $ - do { cts <- solveSimpleGivens given_loc (bagToList givens) - ; return (not (isEmptyBag cts)) } - ; traceTc "checkSatisfiability }" (ppr res) - ; return (not res) } - -{- -********************************************************************************* + do { traceTcS "checkSatisfiability {" (ppr given_ids) + ; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids) + -- Need their superclasses, because (Int ~ Bool) has (Int ~~ Bool) + -- as a superclass, and it's the latter that is insoluble + ; insols <- solveSimpleGivens given_cts + ; insols <- try_harder insols + ; traceTcS "checkSatisfiability }" (ppr insols) + ; return (isEmptyBag insols) } + ; return res } + where + try_harder :: Cts -> TcS Cts + -- Maybe we have to search up the superclass chain to find + -- an unsatisfiable constraint. Example: pmcheck/T3927b. + try_harder insols + | not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable + = return insols -- Hurrah -- stop now. + | otherwise + = do { pending_given <- getPendingScDicts + ; new_given <- makeSuperClasses pending_given + ; if null new_given -- No new superclasses to try, so no point + then return emptyBag -- in continuing + else -- Some new superclasses; have a go + do { insols <- solveSimpleGivens new_given + ; try_harder insols } } + +{- ******************************************************************************** * * * Inference * * @@ -971,12 +990,13 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics -- of adding Derived insolubles twice; see -- TcSMonad Note [Do not add duplicate derived insolubles] ; wc1 <- solveSimpleWanteds simples + ; (no_new_scs, wc1) <- expandSuperClasses wc1 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1) ; dflags <- getDynFlags - ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs + ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs (WC { wc_simple = simples1, wc_impl = implics2 , wc_insol = insols `unionBags` insols1 }) @@ -987,10 +1007,10 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics ; return final_wc } -simpl_loop :: Int -> IntWithInf -> Cts +simpl_loop :: Int -> IntWithInf -> Cts -> Bool -> WantedConstraints -> TcS WantedConstraints -simpl_loop n limit floated_eqs +simpl_loop n limit floated_eqs no_new_given_scs wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) | n `intGtLimit` limit = failTcS (hang (ptext (sLit "solveWanteds: too many iterations") @@ -998,7 +1018,7 @@ simpl_loop n limit floated_eqs 2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit") , ppr wc ] )) - | no_floated_eqs + | isEmptyBag floated_eqs && no_new_given_scs = return wc -- Done! | otherwise @@ -1011,19 +1031,42 @@ simpl_loop n limit floated_eqs -- NB: the floated_eqs may include /derived/ equalities -- arising from fundeps inside an implication + ; (no_new_scs, wc1) <- expandSuperClasses wc1 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1 - -- solveImplications may make progress only if unifs2 holds + -- We have already tried to solve the nested implications once + -- Try again only if we have unified some meta-variables + -- (which is a bit like adding more givens + -- See Note [Cutting off simpl_loop] ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1 then return (emptyBag, implics) else solveNestedImplications (implics `unionBags` implics1) - ; simpl_loop (n+1) limit floated_eqs2 + ; simpl_loop (n+1) limit floated_eqs2 no_new_scs (WC { wc_simple = simples1, wc_impl = implics2 , wc_insol = insols `unionBags` insols1 }) } - where - no_floated_eqs = isEmptyBag floated_eqs +expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints) +-- If there are any unsolved wanteds, expand one step of superclasses for +-- unsolved wanteds or givens +-- See Note [The superclass story] in TcCanonical +expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols }) + | isEmptyBag unsolved -- No unsolved simple wanteds, so do not add suerpclasses + = return (True, wc) + | otherwise + = do { let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved + get acc ct = case isPendingScDict ct of + Just ct' -> (ct':acc, ct') + Nothing -> (acc, ct) + ; pending_given <- getPendingScDicts + ; if null pending_given && null pending_wanted + then return (True, wc) + else + do { new_given <- makeSuperClasses pending_given + ; new_insols <- solveSimpleGivens new_given + ; new_wanted <- makeSuperClasses pending_wanted + ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted + , wc_insol = insols `unionBags` new_insols }) } } solveNestedImplications :: Bag Implication -> TcS (Cts, Bag Implication) @@ -1054,7 +1097,7 @@ solveImplication :: Implication -- Wanted solveImplication imp@(Implic { ic_tclvl = tclvl , ic_binds = m_ev_binds , ic_skols = skols - , ic_given = givens + , ic_given = given_ids , ic_wanted = wanteds , ic_info = info , ic_status = status @@ -1071,15 +1114,21 @@ solveImplication imp@(Implic { ic_tclvl = tclvl -- Solve the nested constraints ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs) - <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ givens)) tclvl $ - do { given_insols <- solveSimpleGivens (mkGivenLoc tclvl info env) givens - ; no_eqs <- getNoGivenEqs tclvl skols + <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $ + do { let loc = mkGivenLoc tclvl info env + ; givens_w_scs <- mkGivensWithSuperClasses loc given_ids + ; given_insols <- solveSimpleGivens givens_w_scs ; residual_wanted <- solveWanteds wanteds -- solveWanteds, *not* solveWantedsAndDrop, because -- we want to retain derived equalities so we can float -- them out in floatEqualities + ; no_eqs <- getNoGivenEqs tclvl skols + -- Call getNoGivenEqs /after/ solveWanteds, because + -- solveWanteds can augment the givens, via expandSuperClasses, + -- to reveal given superclass equalities + ; return (no_eqs, given_insols, residual_wanted) } ; (floated_eqs, residual_wanted) @@ -1355,27 +1404,17 @@ of progress. Trac #8474 is a classic example: * So there is no point in attempting to re-solve ?yn:betan => [W] ?x:Int - because we'll just get the same [D] again + via solveNestedImplications, because we'll just get the + same [D] again * If we *do* re-solve, we'll get an ininite loop. It is cut off by the fixed bound of 10, but solving the next takes 10*10*...*10 (ie exponentially many) iterations! -Conclusion: we should iterate simpl_loop iff we will get more 'givens' -in the inert set when solving the nested implications. That is the -result of prepareInertsForImplications is larger. How can we tell -this? - -Consider floated_eqs (all wanted or derived): - -(a) [W/D] CTyEqCan (a ~ ty). This can give rise to a new given only by causing - a unification. So we count those unifications. - -(b) [W] CFunEqCan (F tys ~ xi). Even though these are wanted, they - are pushed in as givens by prepareInertsForImplications. See Note - [Preparing inert set for implications] in TcSMonad. But because - of that very fact, we won't generate another copy if we iterate - simpl_loop. So we iterate if there any of these +Conclusion: we should call solveNestedImplications only if we did +some unifiction in solveSimpleWanteds; because that's the only way +we'll get more Givens (a unificaiton is like adding a Given) to +allow the implication to make progress. -} promoteTyVar :: TcLevel -> TcTyVar -> TcM () diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 915686b576..7523c6a263 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -1927,9 +1927,6 @@ Validity checking is done once the mutually-recursive knot has been tied, so we can look at things freely. -} -checkClassCycleErrs :: Class -> TcM () -checkClassCycleErrs cls = mapM_ recClsErr (calcClassCycles cls) - checkValidTyCl :: TyCon -> TcM TyCon checkValidTyCl tc = setSrcSpan (getSrcSpan tc) $ @@ -2208,9 +2205,10 @@ checkNewDataCon con checkValidClass :: Class -> TcM () checkValidClass cls = do { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods - ; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses - ; nullary_type_classes <- xoptM Opt_NullaryTypeClasses - ; fundep_classes <- xoptM Opt_FunctionalDependencies + ; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses + ; nullary_type_classes <- xoptM Opt_NullaryTypeClasses + ; fundep_classes <- xoptM Opt_FunctionalDependencies + ; undecidable_super_classes <- xoptM Opt_UndecidableSuperClasses -- Check that the class is unary, unless multiparameter type classes -- are enabled; also recognize deprecated nullary type classes @@ -2225,7 +2223,11 @@ checkValidClass cls -- Now check for cyclic superclasses -- If there are superclass cycles, checkClassCycleErrs bails. - ; checkClassCycleErrs cls + ; unless undecidable_super_classes $ + case checkClassCycles cls of + Just err -> setSrcSpan (getSrcSpan cls) $ + addErrTc err + Nothing -> return () -- Check the class operations. -- But only if there have been no earlier errors @@ -2541,11 +2543,6 @@ recSynErr syn_decls sorted_decls = sortLocated syn_decls ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl -recClsErr :: [TyCon] -> TcRn () -recClsErr cycles - = addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"), - nest 2 (hsep (intersperse (text "->") (map ppr cycles)))]) - badDataConTyCon :: DataCon -> Type -> Type -> SDoc badDataConTyCon data_con res_ty_tmpl actual_res_ty = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+> diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs index 4798463298..01ccae59ba 100644 --- a/compiler/typecheck/TcTyDecls.hs +++ b/compiler/typecheck/TcTyDecls.hs @@ -13,7 +13,8 @@ files for imported data types. module TcTyDecls( calcRecFlags, RecTyInfo(..), - calcSynCycles, calcClassCycles, + calcSynCycles, + checkClassCycles, -- * Roles RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots, @@ -56,19 +57,18 @@ import BasicTypes import SrcLoc import Unique ( mkBuiltinUnique ) import Outputable -import UniqSet import Util import Maybes import Data.List import Bag -import FastString ( fastStringToByteString ) +import FastString import Control.Monad {- ************************************************************************ * * - Cycles in class and type synonym declarations + Cycles in type synonym declarations * * ************************************************************************ @@ -139,123 +139,100 @@ mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs) calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)] calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges -{- -Note [Superclass cycle check] +{- Note [Superclass cycle check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We can't allow cycles via superclasses because it would result in the -type checker looping when it canonicalises a class constraint (superclasses -are added during canonicalisation). More precisely, given a constraint - C ty1 .. tyn -we want to instantiate all of C's superclasses, transitively, and -that set must be finite. So if - class (D b, E b a) => C a b -then when we encounter the constraint - C ty1 ty2 -we'll instantiate the superclasses - (D ty2, E ty2 ty1) -and then *their* superclasses, and so on. This set must be finite! - -It is OK for superclasses to be type synonyms for other classes, so -must "look through" type synonyms. Eg - type X a = C [a] - class X a => C a -- No! Recursive superclass! - -We want definitions such as: - - class C cls a where cls a => a -> a - class C D a => D a where - -to be accepted, even though a naive acyclicity check would reject the -program as having a cycle between D and its superclass. Why? Because -when we instantiate - D ty1 -we get the superclas - C D ty1 -and C has no superclasses, so we have terminated with a finite set. - -More precisely, the rule is this: the superclasses sup_C of a class C -are rejected iff: +The superclass cycle check for C decides if we can statically +guarantee that expanding C's superclass cycles transitively is +guaranteed to terminate. This is a Haskell98 requirement, +but one that we lift with -XUndecidableSuperClasses. - C \elem expand(sup_C) - -Where expand is defined as follows: - -(1) expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN) - -(2) expand(D ty1 ... tyN) = {D} - \union sup_D[ty1/x1, ..., tyP/xP] - \union expand(ty(P+1)) ... \union expand(tyN) - where (D x1 ... xM) is a class, P = min(M,N) - -(3) expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN) - where T is not a class - -Eqn (1) is conservative; when there's a type variable at the head, -look in all the argument types. Eqn (2) expands superclasses; the -third component of the union is like Eqn (1). Eqn (3) happens mainly -when the context is a (constraint) tuple, such as (Eq a, Show a). - -Furthermore, expand always looks through type synonyms. +The worry is that a superclass cycle could make the type checker loop. +More precisely, with a constraint (Given or Wanted) + C ty1 .. tyn +one approach is to instantiate all of C's superclasses, transitively. +We can only do so if that set is finite. + +This potential loop occurs only through superclasses. This, for +exmaple, is fine + class C a where + op :: C b => a -> b -> b +even though C's full definition uses C. + +Making the check static also makes it conservative. Eg + type family F a + class F a => C a +Here an instance of (F a) might mention C: + type instance F [a] = C a +and now we'd have a loop. + +The static check works like this, starting with C + * Look at C's superclass predicates + * If any is a type-function application, + or is headed by a type variable, fail + * If any has C at the head, fail + * If any has a type class D at the head, + make the same test with D + +A tricky point is: what if there is a type variable at the head? +Consider this: + class f (C f) => C f + class c => Id c +and now expand superclasses for constraint (C Id): + C Id + --> Id (C Id) + --> C Id + --> .... +Each step expands superclasses one layer, and clearly does not terminate. -} -calcClassCycles :: Class -> [[TyCon]] -calcClassCycles cls - = nubBy eqAsCycle $ - expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) [] +checkClassCycles :: Class -> Maybe SDoc +-- Nothing <=> ok +-- Just err <=> possible cycle error +checkClassCycles cls + = do { (definite_cycle, err) <- go emptyNameSet cls + ; let herald | definite_cycle = ptext (sLit "Superclass cycle for") + | otherwise = ptext (sLit "Potential superclass cycle for") + ; return (vcat [ herald <+> quotes (ppr cls) + , nest 2 err, hint]) } where - -- The last TyCon in the cycle is always the same as the first - eqAsCycle xs ys = any (xs ==) (cycles (tail ys)) - cycles xs = take n . map (take n) . tails . cycle $ xs - where n = length xs - - -- No more superclasses to expand ==> no problems with cycles - -- See Note [Superclass cycle check] - expandTheta :: UniqSet Class -- Path of Classes to here in set form - -> [TyCon] -- Path to here - -> ThetaType -- Superclass work list - -> [[TyCon]] -- Input error paths - -> [[TyCon]] -- Final error paths - expandTheta _ _ [] = id - expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta - - expandType seen path (TyConApp tc tys) - -- Expand unsaturated classes to their superclass theta if they are yet unseen. - -- If they have already been seen then we have detected an error! + hint = ptext (sLit "Use UndecidableSuperClasses to accept this") + + go :: NameSet -> Class -> Maybe (Bool, SDoc) + go so_far cls = firstJusts $ + map (go_pred (so_far `extendNameSet` getName cls)) $ + classSCTheta cls + + go_pred :: NameSet -> PredType -> Maybe (Bool, SDoc) + -- Nothing <=> ok + -- Just (True, err) <=> definite cycle + -- Just (False, err) <=> possible cycle + go_pred so_far pred -- NB: tcSplitTyConApp looks through synonyms + | Just (tc, _) <- tcSplitTyConApp_maybe pred + = go_tc so_far pred tc + | hasTyVarHead pred + = Just (False, hang (ptext (sLit "one of whose superclass constraints is headed by a type variable:")) + 2 (quotes (ppr pred))) + | otherwise + = Nothing + + go_tc :: NameSet -> PredType -> TyCon -> Maybe (Bool, SDoc) + go_tc so_far pred tc + | isFamilyTyCon tc + = Just (False, hang (ptext (sLit "one of whose superclass constraints is headed by a type family:")) + 2 (quotes (ppr pred))) | Just cls <- tyConClass_maybe tc - , let (env, remainder) = papp (classTyVars cls) tys - rest_tys = either (const []) id remainder - = if cls `elementOfUniqSet` seen - then (reverse (classTyCon cls:path):) - . flip (foldr (expandType seen path)) tys - else expandTheta (addOneToUniqSet seen cls) (tc:path) - (substTys (mkTopTCvSubst env) (classSCTheta cls)) - . flip (foldr (expandType seen path)) rest_tys - - -- For synonyms, try to expand them: some arguments might be - -- phantoms, after all. We can expand with impunity because at - -- this point the type synonym cycle check has already happened. - | Just (tvs, rhs) <- synTyConDefn_maybe tc - , let (env, remainder) = papp tvs tys - rest_tys = either (const []) id remainder - = expandType seen (tc:path) (substTy (mkTopTCvSubst env) rhs) - . flip (foldr (expandType seen path)) rest_tys - - -- For non-class, non-synonyms, just check the arguments - | otherwise - = flip (foldr (expandType seen path)) tys - - expandType _ _ (TyVarTy {}) = id - expandType _ _ (LitTy {}) = id - expandType seen path (AppTy t1 t2) = expandType seen path t1 . expandType seen path t2 - expandType seen path (ForAllTy b t) = expandType seen path (binderType b) . expandType seen path t - expandType seen path (CastTy ty _co) = expandType seen path ty - expandType _ _ (CoercionTy {}) = id - - papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type]) - papp [] tys = ([], Right tys) - papp tvs [] = ([], Left tvs) - papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder) - where (env, remainder) = papp tvs tys + = go_cls so_far cls + | otherwise -- Equality predicate, for example + = Nothing + + go_cls :: NameSet -> Class -> Maybe (Bool, SDoc) + go_cls so_far cls + | getName cls `elemNameSet` so_far + = Just (True, ptext (sLit "one of whose superclasses is") <+> quotes (ppr cls)) + | otherwise + = do { (b,err) <- go so_far cls + ; return (b, ptext (sLit "one of whose superclasses is") <+> quotes (ppr cls) + $$ err) } {- ************************************************************************ diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 69ac6b79f4..6b148cf05f 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -88,7 +88,7 @@ module TcType ( --------------------------------- -- Predicate types - mkMinimalBySCs, transSuperClasses, transSuperClassesPred, + mkMinimalBySCs, transSuperClasses, pickQuantifiablePreds, immSuperClasses, isImprovementPred, @@ -1590,7 +1590,33 @@ canUnifyWithPolyType dflags details _other -> True -- We can have non-meta tyvars in given constraints -{- +{- Note [Expanding superclasses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we expand superclasses, we use the following algorithm: + +expand( so_far, pred ) returns the transitive superclasses of pred, + not including pred itself + 1. If pred is not a class constraint, return empty set + Otherwise pred = C ts + 2. If C is in so_far, return empty set (breaks loops) + 3. Find the immediate superclasses constraints of (C ts) + 4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss ) + +Notice that + + * With normal Haskell-98 classes, the loop-detector will never bite, + so we'll get all the superclasses. + + * Since there is only a finite number of distinct classes, expansion + must terminate. + + * The loop breaking is a bit conservative. Notably, a tuple class + could contain many times without threatening termination: + (Eq a, (Ord a, Ix a)) + And this is try of any class that we can statically guarantee + as non-recursive (in some sense). For now, we just make a special + case for tuples + ************************************************************************ * * \subsection{Predicate types} @@ -1693,30 +1719,48 @@ pickQuantifiablePreds qtvs theta -- Superclasses +type PredWithSCs = (PredType, [PredType]) + mkMinimalBySCs :: [PredType] -> [PredType] -- Remove predicates that can be deduced from others by superclasses -mkMinimalBySCs ptys = [ pty | pty <- ptys - , pty `not_in_preds` rec_scs ] +-- Result is a subset of the input +mkMinimalBySCs ptys = go preds_with_scs [] where - rec_scs = concatMap trans_super_classes ptys - not_in_preds p ps = not (any (eqType p) ps) - - trans_super_classes pred -- Superclasses of pred, excluding pred itself - = case classifyPredType pred of - ClassPred cls tys -> transSuperClasses cls tys - _ -> [] - -transSuperClasses :: Class -> [Type] -> [PredType] -transSuperClasses cls tys -- Superclasses of (cls tys), - -- excluding (cls tys) itself - = concatMap transSuperClassesPred (immSuperClasses cls tys) - -transSuperClassesPred :: PredType -> [PredType] --- (transSuperClassesPred p) returns (p : p's superclasses) -transSuperClassesPred p - = case classifyPredType p of - ClassPred cls tys -> p : transSuperClasses cls tys - _ -> [p] + preds_with_scs :: [PredWithSCs] + preds_with_scs = [ (pred, transSuperClasses pred) + | pred <- ptys ] + + go :: [PredWithSCs] -- Work list + -> [PredWithSCs] -- Accumulating result + -> [PredType] + go [] min_preds = map fst min_preds + go (work_item@(p,_) : work_list) min_preds + | p `in_cloud` work_list || p `in_cloud` min_preds + = go work_list min_preds + | otherwise + = go work_list (work_item : min_preds) + + in_cloud :: PredType -> [PredWithSCs] -> Bool + in_cloud p ps = or [ p `eqType` p' | (_, scs) <- ps, p' <- scs ] + +transSuperClasses :: PredType -> [PredType] +-- (transSuperClasses p) returns (p's superclasses) +-- not including p +-- See Note [Expanding superclasses] +transSuperClasses p + = go emptyNameSet p + where + go :: NameSet -> PredType -> [PredType] + go rec_clss p + | ClassPred cls tys <- classifyPredType p + , let cls_nm = className cls + , not (cls_nm `elemNameSet` rec_clss) + , let rec_clss' | isCTupleClass cls = rec_clss + | otherwise = rec_clss `extendNameSet` cls_nm + = [ p' | sc <- immSuperClasses cls tys + , p' <- sc : go rec_clss' sc ] + | otherwise + = [] immSuperClasses :: Class -> [Type] -> [PredType] immSuperClasses cls tys diff --git a/compiler/utils/Bag.hs b/compiler/utils/Bag.hs index d85465081b..09fddccde1 100644 --- a/compiler/utils/Bag.hs +++ b/compiler/utils/Bag.hs @@ -17,7 +17,7 @@ module Bag ( filterBag, partitionBag, partitionBagWith, concatBag, catBagMaybes, foldBag, foldrBag, foldlBag, isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, - listToBag, bagToList, + listToBag, bagToList, mapAccumBagL, foldrBagM, foldlBagM, mapBagM, mapBagM_, flatMapBagM, flatMapBagPairM, mapAndUnzipBagM, mapAccumBagLM, @@ -30,7 +30,7 @@ import Util import MonadUtils import Control.Monad import Data.Data -import Data.List ( partition ) +import Data.List ( partition, mapAccumL ) import qualified Data.Foldable as Foldable infixr 3 `consBag` @@ -265,6 +265,18 @@ mapAndUnzipBagM f (ListBag xs) = do ts <- mapM f xs let (rs,ss) = unzip ts return (ListBag rs, ListBag ss) +mapAccumBagL ::(acc -> x -> (acc, y)) -- ^ combining funcction + -> acc -- ^ initial state + -> Bag x -- ^ inputs + -> (acc, Bag y) -- ^ final state, outputs +mapAccumBagL _ s EmptyBag = (s, EmptyBag) +mapAccumBagL f s (UnitBag x) = let (s1, x1) = f s x in (s1, UnitBag x1) +mapAccumBagL f s (TwoBags b1 b2) = let (s1, b1') = mapAccumBagL f s b1 + (s2, b2') = mapAccumBagL f s1 b2 + in (s2, TwoBags b1' b2') +mapAccumBagL f s (ListBag xs) = let (s', xs') = mapAccumL f s xs + in (s', ListBag xs') + mapAccumBagLM :: Monad m => (acc -> x -> m (acc, y)) -- ^ combining funcction -> acc -- ^ initial state diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 566ecdaf79..f9bd20d2f8 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -5996,6 +5996,55 @@ to subsume the ``OverloadedStrings`` extension (currently, as a special case, string literals benefit from statically allocated compact representation). +Undecidable (or recursive) superclasses +--------------------------------------- + +The language extension ``-XUndecidableSuperClasses`` allows much more flexible +constraints in superclasses. + +A class cannot generally have itself as a superclass. So this is illegal :: + + class C a => D a where ... + class D a => C a where ... + +GHC implements this test conservatively when type functions, or type variables, +are involved. For example :: + + type family F a :: Constraint + class F a => C a where ... + +GHC will complain about this, because you might later add :: + + type instance F Int = C Int + +and now we'd be in a superclass loop. Here's an example involving a type variable :: + + class f (C f) => C f + class c => Id c + +If we expanded the superclasses of ``C Id`` we'd get first ``Id (C Id)`` and +thence ``C Id`` again. + +But superclass constraints like these are sometimes useful, and the conservative +check is annoying where no actual recursion is involved. + +Moreover genuninely-recursive superclasses are sometimes useful. Here's a real-life +example (Trac #10318) :: + + class (Frac (Frac a) ~ Frac a, + Fractional (Frac a), + IntegralDomain (Frac a)) + => IntegralDomain a where + type Frac a :: * + +Here the superclass cycle does terminate but it's not entirely straightforward +to see that it does. + +With the language extension ``-XUndecidableSuperClasses`` GHC lifts all restrictions +on superclass constraints. If there really *is* a loop, GHC will only +expand it to finite depth. + + .. _type-families: Type families diff --git a/libraries/ghc-prim/GHC/Classes.hs b/libraries/ghc-prim/GHC/Classes.hs index d4c6697652..0e74bef07c 100644 --- a/libraries/ghc-prim/GHC/Classes.hs +++ b/libraries/ghc-prim/GHC/Classes.hs @@ -4,6 +4,8 @@ MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE AllowAmbiguousTypes #-} -- ip :: IP x a => a is strictly speaking ambiguous, but IP is magic +{-# LANGUAGE UndecidableSuperClasses #-} + -- Because of the type-variable superclasses for tuples {-# OPTIONS_GHC -fno-warn-unused-imports #-} -- -fno-warn-unused-imports needed for the GHC.Tuple import below. Sigh. diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr index a5fe638fea..6472310ece 100644 --- a/testsuite/tests/ado/ado004.stderr +++ b/testsuite/tests/ado/ado004.stderr @@ -3,23 +3,23 @@ TYPE SIGNATURES forall (f :: * -> *). Applicative f => (Int -> f Int) -> f Int test2 :: forall (f :: * -> *) b a. - (Num b, Num a, Applicative f) => + (Applicative f, Num a, Num b) => (a -> f b) -> f b test3 :: forall (m :: * -> *) a a1 a2. - (Monad m, Num a2) => + (Num a2, Monad m) => (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a test4 :: forall (m :: * -> *) a a1 a2. - (Monad m, Num a2) => + (Num a2, Monad m) => (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a test5 :: forall (m :: * -> *) a a1 a2. - (Monad m, Num a2) => + (Num a2, Monad m) => (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a test6 :: forall r (m :: * -> *) a. - (Monad m, Num (m a)) => + (Num (m a), Monad m) => (m a -> m (m a)) -> r -> m a TYPE CONSTRUCTORS COERCION AXIOMS diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs index 1b4f8e65ae..b6d04ef6c1 100644 --- a/testsuite/tests/driver/T4437.hs +++ b/testsuite/tests/driver/T4437.hs @@ -34,6 +34,7 @@ expectedGhcOnlyExtensions = ["RelaxedLayout", "AlternativeLayoutRule", "AlternativeLayoutRuleTransitional", "OverloadedLabels", + "UndecidableSuperClasses", "TemplateHaskellQuotes", "MonadFailDesugaring", "TypeInType"] diff --git a/testsuite/tests/ghci/scripts/ghci013.stdout b/testsuite/tests/ghci/scripts/ghci013.stdout index 245881f02b..d5afe0a691 100644 --- a/testsuite/tests/ghci/scripts/ghci013.stdout +++ b/testsuite/tests/ghci/scripts/ghci013.stdout @@ -1 +1 @@ -f :: (Monad m, ?callStack::CallStack) => (m a, r) -> m b +f :: (?callStack::CallStack, Monad m) => (m a, r) -> m b diff --git a/testsuite/tests/indexed-types/should_compile/T10318.hs b/testsuite/tests/indexed-types/should_compile/T10318.hs new file mode 100644 index 0000000000..04a2ca105c --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T10318.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE FlexibleContexts, TypeSynonymInstances, + FlexibleInstances, TypeFamilies, + UndecidableSuperClasses #-} + +module T10318 where + +-- | Product of non-zero elements always non-zero. +-- Every integral domain has a field of fractions. +-- The field of fractions of any field is itself. +class (Frac (Frac a) ~ Frac a, Fractional (Frac a), IntegralDomain (Frac a)) + => IntegralDomain a where + type Frac a :: * + embed :: a -> Frac a + +instance IntegralDomain Integer where + type Frac Integer = Rational + embed = fromInteger + +instance IntegralDomain Rational where + type Frac Rational = Rational + embed = id + +g :: IntegralDomain a => a -> a +g x = g x + +h :: a -> Frac a +h x = h x + +-- This is the test function + +f :: IntegralDomain a => a -> Frac a +f x = g (h (h x)) + -- Given: IntegralDomain (Frac a) + -- Wanted: IntegralDomain (Frac (Frac a)) + diff --git a/testsuite/tests/indexed-types/should_compile/T11067.hs b/testsuite/tests/indexed-types/should_compile/T11067.hs new file mode 100644 index 0000000000..0074fae685 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T11067.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleContexts #-} + +module T11067 where + +import Data.Monoid +import GHC.Exts (Constraint) + +type family Skolem (p :: k -> Constraint) :: k +type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1 + +-- | A quantified constraint +type Forall (p :: k -> Constraint) = p (Skolem p) +type ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) = p (f (SkolemF p f)) + +-- These work +class ForallF Monoid t => Monoid1 t +instance ForallF Monoid t => Monoid1 t + +class ForallF Monoid1 t => Monoid2 t +instance ForallF Monoid1 t => Monoid2 t + +-- Changing f a ~ g a to, (Ord (f a), Ord (g a)), say, removes the error +class (f a ~ g a) => H f g a +instance (f a ~ g a) => H f g a + +-- This one gives a superclass cycle error. +class Forall (H f g) => H1 f g +instance Forall (H f g) => H1 f g diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr index 53d7942958..1300626e17 100644 --- a/testsuite/tests/indexed-types/should_compile/T3017.stderr +++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr @@ -1,7 +1,7 @@ TYPE SIGNATURES emptyL :: forall a. ListColl a test2 :: - forall c t t1. (Num t, Num t1, Coll c, Elem c ~ (t, t1)) => c -> c + forall c t t1. (Elem c ~ (t, t1), Coll c, Num t1, Num t) => c -> c TYPE CONSTRUCTORS class Coll c where type family Elem c open diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.stderr b/testsuite/tests/indexed-types/should_compile/T3208b.stderr index 0a0a491f17..c017701a27 100644 --- a/testsuite/tests/indexed-types/should_compile/T3208b.stderr +++ b/testsuite/tests/indexed-types/should_compile/T3208b.stderr @@ -1,14 +1,4 @@ -T3208b.hs:15:10: error: - • Could not deduce: OTerm o0 ~ STerm o0 arising from a use of ‘fce’ - from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a) - bound by the type signature for: - fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c - at T3208b.hs:14:1-56 - The type variable ‘o0’ is ambiguous - • In the expression: fce (apply f) - In an equation for ‘fce'’: fce' f = fce (apply f) - T3208b.hs:15:15: error: • Could not deduce: OTerm o0 ~ STerm a arising from a use of ‘apply’ diff --git a/testsuite/tests/indexed-types/should_compile/T8889.stderr b/testsuite/tests/indexed-types/should_compile/T8889.stderr index 77e05d764b..44cb453421 100644 --- a/testsuite/tests/indexed-types/should_compile/T8889.stderr +++ b/testsuite/tests/indexed-types/should_compile/T8889.stderr @@ -1,6 +1,6 @@ -T8889.hs:12:1: Warning: +T8889.hs:12:1: warning: Top-level binding with no type signature: f :: forall (f :: * -> *) a b. - (C_fmap f a, C f) => + (C f, C_fmap f a) => (a -> b) -> f a -> f b diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 5de25bfe6b..d4ff607b56 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -266,3 +266,5 @@ test('T10806', normal, compile_fail, ['']) test('T10815', normal, compile, ['']) test('T10931', normal, compile, ['']) test('T11187', normal, compile, ['']) +test('T11067', normal, compile, ['']) +test('T10318', normal, compile, ['']) diff --git a/testsuite/tests/indexed-types/should_fail/T1897b.stderr b/testsuite/tests/indexed-types/should_fail/T1897b.stderr index 459f6c8a17..e70a256f98 100644 --- a/testsuite/tests/indexed-types/should_fail/T1897b.stderr +++ b/testsuite/tests/indexed-types/should_fail/T1897b.stderr @@ -1,13 +1,13 @@ T1897b.hs:16:1: error: - Couldn't match type ‘Depend a’ with ‘Depend a0’ - NB: ‘Depend’ is a type function, and may not be injective - The type variable ‘a0’ is ambiguous - Expected type: t (Depend a) -> Bool - Actual type: t (Depend a0) -> Bool - In the ambiguity check for the inferred type for ‘isValid’ - To defer the ambiguity check to use sites, enable AllowAmbiguousTypes - When checking the inferred type - isValid :: forall a (t :: * -> *). - (Foldable t, Bug a) => - t (Depend a) -> Bool + • Couldn't match type ‘Depend a’ with ‘Depend a0’ + NB: ‘Depend’ is a type function, and may not be injective + The type variable ‘a0’ is ambiguous + Expected type: t (Depend a) -> Bool + Actual type: t (Depend a0) -> Bool + • In the ambiguity check for the inferred type for ‘isValid’ + To defer the ambiguity check to use sites, enable AllowAmbiguousTypes + When checking the inferred type + isValid :: forall a (t :: * -> *). + (Bug a, Foldable t) => + t (Depend a) -> Bool diff --git a/testsuite/tests/indexed-types/should_fail/T3330a.stderr b/testsuite/tests/indexed-types/should_fail/T3330a.stderr index ea3b1d4001..f6a5deeeb7 100644 --- a/testsuite/tests/indexed-types/should_fail/T3330a.stderr +++ b/testsuite/tests/indexed-types/should_fail/T3330a.stderr @@ -1,23 +1,5 @@ T3330a.hs:19:34: error: - • Couldn't match type ‘ix’ - with ‘r ix1 -> Writer [AnyF s] (r'0 ix1)’ - ‘ix’ is a rigid type variable bound by - the type signature for: - children :: forall (s :: * -> *) ix (r :: * -> *). - s ix -> PF s r ix -> [AnyF s] - at T3330a.hs:18:13 - Expected type: (s0 ix0 -> ix1) - -> r ix1 -> Writer [AnyF s] (r'0 ix1) - Actual type: s ix - • In the first argument of ‘hmapM’, namely ‘p’ - In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’ - • Relevant bindings include - x :: PF s r ix (bound at T3330a.hs:19:12) - p :: s ix (bound at T3330a.hs:19:10) - children :: s ix -> PF s r ix -> [AnyF s] (bound at T3330a.hs:19:1) - -T3330a.hs:19:34: error: • Couldn't match type ‘s’ with ‘(->) (s0 ix0 -> ix1)’ ‘s’ is a rigid type variable bound by the type signature for: @@ -26,7 +8,7 @@ T3330a.hs:19:34: error: at T3330a.hs:18:13 Expected type: (s0 ix0 -> ix1) -> r ix1 -> Writer [AnyF s] (r'0 ix1) - Actual type: s ix + Actual type: s ix • In the first argument of ‘hmapM’, namely ‘p’ In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’ • Relevant bindings include @@ -43,7 +25,7 @@ T3330a.hs:19:44: error: s ix -> PF s r ix -> [AnyF s] at T3330a.hs:18:13 Expected type: PF s r (r0 ix0 -> Writer [AnyF s0] (r0 ix0)) - Actual type: PF s r ix + Actual type: PF s r ix • In the third argument of ‘hmapM’, namely ‘x’ In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’ • Relevant bindings include diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr b/testsuite/tests/indexed-types/should_fail/T4174.stderr index 60ae24ccfa..2b0524fa2f 100644 --- a/testsuite/tests/indexed-types/should_fail/T4174.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr @@ -14,19 +14,3 @@ T4174.hs:42:12: error: • Relevant bindings include testcase :: m (Field (Way (GHC6'8 minor) n t p) a b) (bound at T4174.hs:42:1) - -T4174.hs:42:12: error: - • Couldn't match type ‘b’ with ‘RtsSpinLock’ - ‘b’ is a rigid type variable bound by - the type signature for: - testcase :: forall (m :: * -> *) minor n t p a b. - Monad m => - m (Field (Way (GHC6'8 minor) n t p) a b) - at T4174.hs:41:13 - Expected type: m (Field (Way (GHC6'8 minor) n t p) a b) - Actual type: m (Field (WayOf m) SmStep RtsSpinLock) - • In the expression: sync_large_objects - In an equation for ‘testcase’: testcase = sync_large_objects - • Relevant bindings include - testcase :: m (Field (Way (GHC6'8 minor) n t p) a b) - (bound at T4174.hs:42:1) diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr index d52f4b447d..8ac3d94a55 100644 --- a/testsuite/tests/indexed-types/should_fail/T8227.stderr +++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr @@ -1,25 +1,12 @@ -T8227.hs:16:27: - Couldn't match expected type ‘Scalar (V a)’ - with actual type ‘Scalar (V (Scalar (V a))) - -> Scalar (V (Scalar (V a)))’ - In the expression: arcLengthToParam eps eps - In an equation for ‘absoluteToParam’: - absoluteToParam eps seg = arcLengthToParam eps eps - Relevant bindings include - seg :: a (bound at T8227.hs:16:21) - eps :: Scalar (V a) (bound at T8227.hs:16:17) - absoluteToParam :: Scalar (V a) -> a -> Scalar (V a) - (bound at T8227.hs:16:1) - -T8227.hs:16:44: - Couldn't match expected type ‘Scalar (V (Scalar (V a)))’ - with actual type ‘Scalar (V a)’ - NB: ‘Scalar’ is a type function, and may not be injective - In the first argument of ‘arcLengthToParam’, namely ‘eps’ - In the expression: arcLengthToParam eps eps - Relevant bindings include - seg :: a (bound at T8227.hs:16:21) - eps :: Scalar (V a) (bound at T8227.hs:16:17) - absoluteToParam :: Scalar (V a) -> a -> Scalar (V a) - (bound at T8227.hs:16:1) +T8227.hs:16:44: error: + • Couldn't match expected type ‘Scalar (V (Scalar (V a)))’ + with actual type ‘Scalar (V a)’ + NB: ‘Scalar’ is a type function, and may not be injective + • In the first argument of ‘arcLengthToParam’, namely ‘eps’ + In the expression: arcLengthToParam eps eps + • Relevant bindings include + seg :: a (bound at T8227.hs:16:21) + eps :: Scalar (V a) (bound at T8227.hs:16:17) + absoluteToParam :: Scalar (V a) -> a -> Scalar (V a) + (bound at T8227.hs:16:1) diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr index 2d55f9dcea..36b0716a9a 100644 --- a/testsuite/tests/indexed-types/should_fail/T9662.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr @@ -1,77 +1,21 @@ -T9662.hs:49:7: error: - • Couldn't match type ‘k’ with ‘n’ +T9662.hs:47:8: error: + • Couldn't match type ‘k’ with ‘Int’ ‘k’ is a rigid type variable bound by the type signature for: test :: forall sh k m n. Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) at T9662.hs:44:9 - ‘n’ is a rigid type variable bound by - the type signature for: - test :: forall sh k m n. - Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - Expected type: Exp (((sh :. m) :. n) :. k) - -> Exp (((sh :. k) :. m) :. n) - Actual type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. k) :. m) :. n) - • In the second argument of ‘backpermute’, namely ‘id’ - In the expression: - backpermute - (modify - (atom :. atom :. atom :. atom) - (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k))) - id - • Relevant bindings include - test :: Shape (((sh :. k) :. m) :. n) - -> Shape (((sh :. m) :. n) :. k) - (bound at T9662.hs:45:1) - -T9662.hs:49:7: error: - • Couldn't match type ‘m’ with ‘k’ - ‘m’ is a rigid type variable bound by - the type signature for: - test :: forall sh k m n. - Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - ‘k’ is a rigid type variable bound by - the type signature for: - test :: forall sh k m n. - Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - Expected type: Exp (((sh :. m) :. n) :. k) - -> Exp (((sh :. k) :. m) :. n) - Actual type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. k) :. m) :. n) - • In the second argument of ‘backpermute’, namely ‘id’ - In the expression: - backpermute - (modify - (atom :. atom :. atom :. atom) - (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k))) - id - • Relevant bindings include - test :: Shape (((sh :. k) :. m) :. n) - -> Shape (((sh :. m) :. n) :. k) - (bound at T9662.hs:45:1) - -T9662.hs:49:7: error: - • Couldn't match type ‘n’ with ‘m’ - ‘n’ is a rigid type variable bound by - the type signature for: - test :: forall sh k m n. - Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - ‘m’ is a rigid type variable bound by - the type signature for: - test :: forall sh k m n. - Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - Expected type: Exp (((sh :. m) :. n) :. k) - -> Exp (((sh :. k) :. m) :. n) - Actual type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. k) :. m) :. n) - • In the second argument of ‘backpermute’, namely ‘id’ + Expected type: Exp (((sh :. k) :. m) :. n) + -> Exp (((sh :. m) :. n) :. k) + Actual type: Exp + (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) + -> Exp + (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) + • In the first argument of ‘backpermute’, namely + ‘(modify + (atom :. atom :. atom :. atom) + (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’ In the expression: backpermute (modify diff --git a/testsuite/tests/module/mod40.stderr b/testsuite/tests/module/mod40.stderr index cd977d1e77..bd4fcf4bd9 100644 --- a/testsuite/tests/module/mod40.stderr +++ b/testsuite/tests/module/mod40.stderr @@ -1,8 +1,14 @@ -mod40.hs:3:1: - Cycle in class declaration (via superclasses): C1 -> C2 -> C1 - In the class declaration for ‘C1’ +mod40.hs:3:1: error: + • Superclass cycle for ‘C1’ + one of whose superclasses is ‘C2’ + one of whose superclasses is ‘C1’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘C1’ -mod40.hs:4:1: - Cycle in class declaration (via superclasses): C2 -> C1 -> C2 - In the class declaration for ‘C2’ +mod40.hs:4:1: error: + • Superclass cycle for ‘C2’ + one of whose superclasses is ‘C1’ + one of whose superclasses is ‘C2’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘C2’ diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr index 7554ce953d..0f0d6f91b2 100644 --- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr +++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr @@ -1,8 +1,8 @@ TYPE SIGNATURES - arbitCs1 :: forall a. (Enum a, Eq a, Show a) => a -> String - arbitCs2 :: forall a. (Show a, Enum a, Eq a) => a -> String + arbitCs1 :: forall a. (Show a, Eq a, Enum a) => a -> String + arbitCs2 :: forall a. (Show a, Eq a, Enum a) => a -> String arbitCs3 :: forall a. (Show a, Enum a, Eq a) => a -> String - arbitCs4 :: forall a. (Eq a, Enum a, Show a) => a -> String + arbitCs4 :: forall a. (Eq a, Show a, Enum a) => a -> String arbitCs5 :: forall a. (Eq a, Enum a, Show a) => a -> String TYPE CONSTRUCTORS COERCION AXIOMS diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr index 0c0410d0f2..e7fc912a12 100644 --- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr +++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr @@ -21,8 +21,8 @@ TYPE SIGNATURES >> :: forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >>= :: forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b - ^ :: forall a b. (Integral b, Num a) => a -> b -> a - ^^ :: forall a b. (Fractional a, Integral b) => a -> b -> a + ^ :: forall a b. (Num a, Integral b) => a -> b -> a + ^^ :: forall a b. (Integral b, Fractional a) => a -> b -> a abs :: forall a. Num a => a -> a acos :: forall a. Floating a => a -> a acosh :: forall a. Floating a => a -> a @@ -39,7 +39,7 @@ TYPE SIGNATURES atan2 :: forall a. RealFloat a => a -> a -> a atanh :: forall a. Floating a => a -> a break :: forall a. (a -> Bool) -> [a] -> ([a], [a]) - ceiling :: forall a b. (Integral b, RealFrac a) => a -> b + ceiling :: forall a b. (RealFrac a, Integral b) => a -> b compare :: forall a. Ord a => a -> a -> Ordering concat :: forall (t :: * -> *) a. Foldable t => t [a] -> [a] concatMap :: @@ -56,7 +56,7 @@ TYPE SIGNATURES dropWhile :: forall a. (a -> Bool) -> [a] -> [a] either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c elem :: - forall (t :: * -> *) a. (Eq a, Foldable t) => a -> t a -> Bool + forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool encodeFloat :: forall a. RealFloat a => Integer -> Int -> a enumFrom :: forall a. Enum a => a -> [a] enumFromThen :: forall a. Enum a => a -> a -> [a] @@ -72,7 +72,7 @@ TYPE SIGNATURES floatDigits :: forall a. RealFloat a => a -> Int floatRadix :: forall a. RealFloat a => a -> Integer floatRange :: forall a. RealFloat a => a -> (Int, Int) - floor :: forall a b. (Integral b, RealFrac a) => a -> b + floor :: forall a b. (RealFrac a, Integral b) => a -> b fmap :: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b foldl :: @@ -89,7 +89,7 @@ TYPE SIGNATURES forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a fromEnum :: forall a. Enum a => a -> Int fromInteger :: forall a. Num a => Integer -> a - fromIntegral :: forall a b. (Integral a, Num b) => a -> b + fromIntegral :: forall a b. (Num b, Integral a) => a -> b fromRational :: forall a. Fractional a => Rational -> a fst :: forall a b. (a, b) -> a gcd :: forall a. Integral a => a -> a -> a @@ -118,24 +118,24 @@ TYPE SIGNATURES map :: forall a b. (a -> b) -> [a] -> [b] mapM :: forall (t :: * -> *) (m :: * -> *) a b. - (Monad m, Traversable t) => + (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM_ :: forall (t :: * -> *) (m :: * -> *) a b. - (Monad m, Foldable t) => + (Foldable t, Monad m) => (a -> m b) -> t a -> m () max :: forall a. Ord a => a -> a -> a maxBound :: forall t. Bounded t => t - maximum :: forall (t :: * -> *) a. (Ord a, Foldable t) => t a -> a + maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a maybe :: forall b a. b -> (a -> b) -> Maybe a -> b min :: forall a. Ord a => a -> a -> a minBound :: forall t. Bounded t => t - minimum :: forall (t :: * -> *) a. (Ord a, Foldable t) => t a -> a + minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a mod :: forall a. Integral a => a -> a -> a negate :: forall a. Num a => a -> a not :: Bool -> Bool notElem :: - forall (t :: * -> *) a. (Eq a, Foldable t) => a -> t a -> Bool + forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool null :: forall (t :: * -> *) a. Foldable t => t a -> Bool odd :: forall a. Integral a => a -> Bool or :: forall (t :: * -> *). Foldable t => t Bool -> Bool @@ -143,9 +143,9 @@ TYPE SIGNATURES pi :: forall t. Floating t => t pred :: forall a. Enum a => a -> a print :: forall a. Show a => a -> IO () - product :: forall (t :: * -> *) a. (Num a, Foldable t) => t a -> a + product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a properFraction :: - forall a b. (Integral b, RealFrac a) => a -> (b, a) + forall a b. (RealFrac a, Integral b) => a -> (b, a) putChar :: Char -> IO () putStr :: String -> IO () putStrLn :: String -> IO () @@ -159,14 +159,14 @@ TYPE SIGNATURES readParen :: forall a. Bool -> ReadS a -> ReadS a reads :: forall a. Read a => ReadS a readsPrec :: forall a. Read a => Int -> ReadS a - realToFrac :: forall a b. (Fractional b, Real a) => a -> b + realToFrac :: forall a b. (Real a, Fractional b) => a -> b recip :: forall a. Fractional a => a -> a rem :: forall a. Integral a => a -> a -> a repeat :: forall a. a -> [a] replicate :: forall a. Int -> a -> [a] return :: forall (m :: * -> *) a. Monad m => a -> m a reverse :: forall a. [a] -> [a] - round :: forall a b. (Integral b, RealFrac a) => a -> b + round :: forall a b. (RealFrac a, Integral b) => a -> b scaleFloat :: forall a. RealFloat a => Int -> a -> a scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b] scanl1 :: forall a. (a -> a -> a) -> [a] -> [a] @@ -175,11 +175,11 @@ TYPE SIGNATURES seq :: forall a b. a -> b -> b sequence :: forall (t :: * -> *) (m :: * -> *) a. - (Monad m, Traversable t) => + (Traversable t, Monad m) => t (m a) -> m (t a) sequence_ :: forall (t :: * -> *) (m :: * -> *) a. - (Monad m, Foldable t) => + (Foldable t, Monad m) => t (m a) -> m () show :: forall a. Show a => a -> String showChar :: Char -> ShowS @@ -198,7 +198,7 @@ TYPE SIGNATURES sqrt :: forall a. Floating a => a -> a subtract :: forall a. Num a => a -> a -> a succ :: forall a. Enum a => a -> a - sum :: forall (t :: * -> *) a. (Num a, Foldable t) => t a -> a + sum :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a tail :: forall a. [a] -> [a] take :: forall a. Int -> [a] -> [a] takeWhile :: forall a. (a -> Bool) -> [a] -> [a] @@ -207,7 +207,7 @@ TYPE SIGNATURES toEnum :: forall a. Enum a => Int -> a toInteger :: forall a. Integral a => a -> Integer toRational :: forall a. Real a => a -> Rational - truncate :: forall a b. (Integral b, RealFrac a) => a -> b + truncate :: forall a b. (RealFrac a, Integral b) => a -> b uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c undefined :: forall t. (?callStack::CallStack) => t unlines :: [String] -> String diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr index 8b9eb466ad..3fd0860bb8 100644 --- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr +++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr @@ -10,7 +10,7 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0, WarningWildcardInstantiations.hs:5:14: warning: • Found type wildcard ‘_a’ standing for ‘a’ Where: ‘a’ is a rigid type variable bound by - the inferred type of foo :: (Enum a, Show a) => a -> String + the inferred type of foo :: (Show a, Enum a) => a -> String at WarningWildcardInstantiations.hs:6:1 • In the type signature: foo :: (Show _a, _) => _a -> _ diff --git a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr index 2df15443c9..30efb8fc14 100644 --- a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr +++ b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr @@ -2,7 +2,7 @@ InstantiatedNamedWildcardsInConstraints.hs:4:14: error: • Found type wildcard ‘_a’ standing for ‘b’ Where: ‘b’ is a rigid type variable bound by - the inferred type of foo :: (Enum b, Show b) => b -> (String, b) + the inferred type of foo :: (Show b, Enum b) => b -> (String, b) at InstantiatedNamedWildcardsInConstraints.hs:4:8 To use the inferred type, enable PartialTypeSignatures • In the type signature: diff --git a/testsuite/tests/partial-sigs/should_fail/T10999.stderr b/testsuite/tests/partial-sigs/should_fail/T10999.stderr index 408529185f..3244db60ca 100644 --- a/testsuite/tests/partial-sigs/should_fail/T10999.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T10999.stderr @@ -1,7 +1,7 @@ T10999.hs:5:6: error: - Found constraint wildcard ‘_’ standing for ‘(Ord a, - ?callStack::CallStack)’ + Found constraint wildcard ‘_’ standing for ‘(?callStack::CallStack, + Ord a)’ To use the inferred type, enable PartialTypeSignatures In the type signature: f :: _ => () -> _ @@ -10,7 +10,7 @@ T10999.hs:5:17: error: • Found type wildcard ‘_’ standing for ‘Set.Set a’ Where: ‘a’ is a rigid type variable bound by the inferred type of - f :: (Ord a, ?callStack::CallStack) => () -> Set.Set a + f :: (?callStack::CallStack, Ord a) => () -> Set.Set a at T10999.hs:6:1 To use the inferred type, enable PartialTypeSignatures • In the type signature: diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr index ddbb9e2b6c..ff18935c8d 100644 --- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr +++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr @@ -2,7 +2,7 @@ WildcardInstantiations.hs:5:14: error: • Found type wildcard ‘_a’ standing for ‘a’ Where: ‘a’ is a rigid type variable bound by - the inferred type of foo :: (Enum a, Show a) => a -> String + the inferred type of foo :: (Show a, Enum a) => a -> String at WildcardInstantiations.hs:6:1 To use the inferred type, enable PartialTypeSignatures • In the type signature: diff --git a/testsuite/tests/perf/haddock/all.T b/testsuite/tests/perf/haddock/all.T index 9b8785f9c8..49a126bad9 100644 --- a/testsuite/tests/perf/haddock/all.T +++ b/testsuite/tests/perf/haddock/all.T @@ -91,7 +91,7 @@ test('haddock.Cabal', test('haddock.compiler', [unless(in_tree_compiler(), skip), req_haddock ,stats_num_field('bytes allocated', - [(wordsize(64), 44721228752, 10) + [(wordsize(64), 49395782136, 10) # 2012P-08-14: 26070600504 (amd64/Linux) # 2012-08-29: 26353100288 (amd64/Linux, new CG) # 2012-09-18: 26882813032 (amd64/Linux) @@ -103,6 +103,7 @@ test('haddock.compiler', # 2015-06-02: 36740649320 (amd64/Linux) unknown cause # 2015-06-29: 40624322224 (amd64/Linux) due to #10482, not yet investigated # 2015-12-03: 44721228752 (amd64/Linux) slow creep upwards + # 2015-12-15: 49395782136 (amd64/Linux) more creep, following kind-equalities ,(platform('i386-unknown-mingw32'), 902576468, 10) # 2012-10-30: 13773051312 (x86/Windows) diff --git a/testsuite/tests/pmcheck/should_compile/T3927b.hs b/testsuite/tests/pmcheck/should_compile/T3927b.hs index d2eb8cd6cb..98e4cb9a33 100644 --- a/testsuite/tests/pmcheck/should_compile/T3927b.hs +++ b/testsuite/tests/pmcheck/should_compile/T3927b.hs @@ -6,6 +6,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-} module T3927b where diff --git a/testsuite/tests/polykinds/T7332.hs b/testsuite/tests/polykinds/T7332.hs index 79623e9803..a18b32b838 100644 --- a/testsuite/tests/polykinds/T7332.hs +++ b/testsuite/tests/polykinds/T7332.hs @@ -35,18 +35,36 @@ instance (Build dc r, a ~ dc) => Build dc (a->r) where tspan :: (Build (DC d) r, BuildR r ~ DC d) => r tspan = build (id :: DC d -> DC d) mempty -{- Wanted: +{- Solving 'tspan' + +Given: Build (DC d) r, BuildR r ~ DC d + (by sc) Monoid (DC d) + + Wanted: Build acc0 r0 Monid acc0 acc0 ~ DC d0 DC d0 ~ BuildR r0 + r ~ r0 ==> - Build (DC d0) r0 + Build (DC d0) r Monoid (DC d0) --> Monoid d0 - DC d- ~ BuildR r0 - -In fact Monoid (DC d0) is a superclass of (Build (DC do) r0) -But during inference we do not take upserclasses of wanteds + DC d0 ~ BuildR r + +From Given: BuildR r = DC d, hence + DC d0 ~ DC d +hence + d0 ~ d + +===> + Build (DC d) r + Monoid (DC d) + +Now things are delicate. Either the instance Monoid (DC d) will fire or, +if we are lucky, we might spot that (Monoid (DC d)) is a superclass of +a given. But now (Decl 15) we add superclasses lazily, so that is less +likely to happen, and was always fragile. So include (MOnoid d) in the +signature, as was the case in the orignal ticket. -} diff --git a/testsuite/tests/polykinds/T7594.hs b/testsuite/tests/polykinds/T7594.hs index 18da70342c..ae21956d45 100644 --- a/testsuite/tests/polykinds/T7594.hs +++ b/testsuite/tests/polykinds/T7594.hs @@ -1,11 +1,13 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE Rank2Types #-} + module T7594 where import GHC.Exts (Constraint) diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr index 3ee902ad78..2f1844ecdb 100644 --- a/testsuite/tests/polykinds/T7594.stderr +++ b/testsuite/tests/polykinds/T7594.stderr @@ -1,15 +1,16 @@ -T7594.hs:33:12: - Couldn't match type ‘b’ with ‘IO ()’ - ‘b’ is untouchable - inside the constraints: (:&:) c0 Real a - bound by a type expected by the context: (:&:) c0 Real a => a -> b - at T7594.hs:33:8-19 +T7594.hs:35:12: error: + • Couldn't match type ‘b’ with ‘IO ()’ + ‘b’ is untouchable + inside the constraints: (:&:) c0 Real a + bound by a type expected by the context: + (:&:) c0 Real a => a -> b + at T7594.hs:35:8-19 ‘b’ is a rigid type variable bound by - the inferred type of bar2 :: b at T7594.hs:33:1 - Possible fix: add a type signature for ‘bar2’ - Expected type: a -> b - Actual type: a -> IO () - In the first argument of ‘app’, namely ‘print’ - In the expression: app print q2 - Relevant bindings include bar2 :: b (bound at T7594.hs:33:1) + the inferred type of bar2 :: b at T7594.hs:35:1 + Possible fix: add a type signature for ‘bar2’ + Expected type: a -> b + Actual type: a -> IO () + • In the first argument of ‘app’, namely ‘print’ + In the expression: app print q2 + • Relevant bindings include bar2 :: b (bound at T7594.hs:35:1) diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr index 857d11aa96..4a2473ab51 100644 --- a/testsuite/tests/polykinds/T9017.stderr +++ b/testsuite/tests/polykinds/T9017.stderr @@ -11,16 +11,3 @@ T9017.hs:8:7: error: In an equation for ‘foo’: foo = arr return • Relevant bindings include foo :: a b (m b) (bound at T9017.hs:8:1) - -T9017.hs:8:7: error: - • Couldn't match kind ‘k1’ with ‘*’ - ‘k1’ is a rigid type variable bound by - the type signature for: - foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k). - a b (m b) - at T9017.hs:7:8 - When matching the kind of ‘a’ - • In the expression: arr return - In an equation for ‘foo’: foo = arr return - • Relevant bindings include - foo :: a b (m b) (bound at T9017.hs:8:1) diff --git a/testsuite/tests/simplCore/should_compile/T4398.stderr b/testsuite/tests/simplCore/should_compile/T4398.stderr index e2411e13c7..296e691e80 100644 --- a/testsuite/tests/simplCore/should_compile/T4398.stderr +++ b/testsuite/tests/simplCore/should_compile/T4398.stderr @@ -1,5 +1,5 @@ -T4398.hs:6:11: Warning: +T4398.hs:6:11: warning: Forall'd constraint ‘Ord a’ is not bound in RULE lhs Orig bndrs: [a, $dOrd, x, y] Orig lhs: let { diff --git a/testsuite/tests/typecheck/should_compile/T10100.hs b/testsuite/tests/typecheck/should_compile/T10100.hs index b88803c633..031be76ce2 100644 --- a/testsuite/tests/typecheck/should_compile/T10100.hs +++ b/testsuite/tests/typecheck/should_compile/T10100.hs @@ -2,6 +2,7 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module T10100 where diff --git a/testsuite/tests/typecheck/should_compile/T10109.hs b/testsuite/tests/typecheck/should_compile/T10109.hs index a61b2bc294..a517eea7f9 100644 --- a/testsuite/tests/typecheck/should_compile/T10109.hs +++ b/testsuite/tests/typecheck/should_compile/T10109.hs @@ -1,5 +1,6 @@ {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances #-} +{-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module T10109 where diff --git a/testsuite/tests/typecheck/should_compile/T10564.hs b/testsuite/tests/typecheck/should_compile/T10564.hs index 7b19f0092d..4579dbec77 100644 --- a/testsuite/tests/typecheck/should_compile/T10564.hs +++ b/testsuite/tests/typecheck/should_compile/T10564.hs @@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances, DataKinds, TypeFamilies, KindSignatures, PolyKinds, FunctionalDependencies #-} +{-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module T10564 where diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr index b3a6240a6b..6232a4b78c 100644 --- a/testsuite/tests/typecheck/should_compile/T9834.stderr +++ b/testsuite/tests/typecheck/should_compile/T9834.stderr @@ -1,41 +1,16 @@ T9834.hs:23:10: warning: - • Couldn't match type ‘a’ with ‘p a0’ - ‘a’ is a rigid type variable bound by - the type signature for: - afix :: forall a. - (forall (q :: * -> *). Applicative q => Comp p q a -> Comp p q a) - -> p a - at T9834.hs:22:11 - Expected type: (forall (q :: * -> *). - Applicative q => - Comp p q a -> Comp p q a) - -> p a - Actual type: (forall (q :: * -> *). - Applicative q => - Nat (Comp p q) (Comp p q)) - -> p a0 -> p a0 - • In the expression: wrapIdComp - In an equation for ‘afix’: afix = wrapIdComp - • Relevant bindings include - afix :: (forall (q :: * -> *). - Applicative q => - Comp p q a -> Comp p q a) - -> p a - (bound at T9834.hs:23:3) - -T9834.hs:23:10: warning: • Couldn't match type ‘p’ with ‘(->) (p a0)’ ‘p’ is a rigid type variable bound by the class declaration for ‘ApplicativeFix’ at T9834.hs:21:39 - Expected type: (forall (q :: * -> *). - Applicative q => - Comp p q a -> Comp p q a) - -> p a - Actual type: (forall (q :: * -> *). - Applicative q => - Nat (Comp p q) (Comp p q)) - -> p a0 -> p a0 + Expected type: (forall (q :: * -> *). + Applicative q => + Comp p q a -> Comp p q a) + -> p a + Actual type: (forall (q :: * -> *). + Applicative q => + Nat (Comp p q) (Comp p q)) + -> p a0 -> p a0 • In the expression: wrapIdComp In an equation for ‘afix’: afix = wrapIdComp • Relevant bindings include @@ -59,8 +34,8 @@ T9834.hs:23:10: warning: Applicative q => Comp p q a1 -> Comp p q a1 at T9834.hs:23:10 - Expected type: Comp p q a1 -> Comp p q a1 - Actual type: Comp p q a -> Comp p q a + Expected type: Comp p q a1 -> Comp p q a1 + Actual type: Comp p q a -> Comp p q a • In the expression: wrapIdComp In an equation for ‘afix’: afix = wrapIdComp • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_compile/tc256.hs b/testsuite/tests/typecheck/should_compile/tc256.hs index d33f7a6401..15c096e81c 100644 --- a/testsuite/tests/typecheck/should_compile/tc256.hs +++ b/testsuite/tests/typecheck/should_compile/tc256.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances #-} +{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances, UndecidableSuperClasses #-} module Ctx where import Data.Kind ( Constraint ) diff --git a/testsuite/tests/typecheck/should_fail/T2714.stderr b/testsuite/tests/typecheck/should_fail/T2714.stderr index 0991ddeec0..bba821bcac 100644 --- a/testsuite/tests/typecheck/should_fail/T2714.stderr +++ b/testsuite/tests/typecheck/should_fail/T2714.stderr @@ -1,26 +1,13 @@ -
-T2714.hs:8:5: error:
- Couldn't match type ‘a’ with ‘f0 b’
- ‘a’ is a rigid type variable bound by
- the type signature for:
- f :: forall a b. ((a -> b) -> b) -> forall c. c -> a
- at T2714.hs:7:6
- Expected type: ((a -> b) -> b) -> c -> a
- Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b
- In the expression: ffmap
- In an equation for ‘f’: f = ffmap
- Relevant bindings include
- f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)
-
-T2714.hs:8:5: error:
- Couldn't match type ‘c’ with ‘f0 (a -> b)’
- ‘c’ is a rigid type variable bound by
- the type signature for:
- f :: forall c. ((a -> b) -> b) -> c -> a
- at T2714.hs:8:1
- Expected type: ((a -> b) -> b) -> c -> a
- Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b
- In the expression: ffmap
- In an equation for ‘f’: f = ffmap
- Relevant bindings include
- f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)
+ +T2714.hs:8:5: error: + • Couldn't match type ‘a’ with ‘f0 b’ + ‘a’ is a rigid type variable bound by + the type signature for: + f :: forall a b. ((a -> b) -> b) -> forall c. c -> a + at T2714.hs:7:6 + Expected type: ((a -> b) -> b) -> c -> a + Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b + • In the expression: ffmap + In an equation for ‘f’: f = ffmap + • Relevant bindings include + f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1) diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr index dc23d4a064..33ae4e16ce 100644 --- a/testsuite/tests/typecheck/should_fail/T5853.stderr +++ b/testsuite/tests/typecheck/should_fail/T5853.stderr @@ -1,23 +1,23 @@ T5853.hs:15:52: error: - • Could not deduce: Subst t1 (Elem t2) ~ t2 + • Could not deduce: Subst t2 (Elem t1) ~ t1 arising from a use of ‘<$>’ from the context: (F t, Elem t ~ Elem t, - Elem t2 ~ Elem t2, - Subst t (Elem t2) ~ t2, - Subst t2 (Elem t) ~ t, - F t1, Elem t1 ~ Elem t1, - Elem t ~ Elem t, + Subst t (Elem t1) ~ t1, Subst t1 (Elem t) ~ t, - Subst t (Elem t1) ~ t1) + F t2, + Elem t2 ~ Elem t2, + Elem t ~ Elem t, + Subst t2 (Elem t) ~ t, + Subst t (Elem t2) ~ t2) bound by the RULE "map/map" at T5853.hs:15:2-57 - ‘t2’ is a rigid type variable bound by + ‘t1’ is a rigid type variable bound by the RULE "map/map" at T5853.hs:15:2 • In the expression: (f . g) <$> xs When checking the transformation rule "map/map" • Relevant bindings include - f :: Elem t -> Elem t2 (bound at T5853.hs:15:19) - g :: Elem t1 -> Elem t (bound at T5853.hs:15:21) - xs :: t1 (bound at T5853.hs:15:23) + f :: Elem t -> Elem t1 (bound at T5853.hs:15:19) + g :: Elem t2 -> Elem t (bound at T5853.hs:15:21) + xs :: t2 (bound at T5853.hs:15:23) diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr index 6431c274e5..f906a95e3e 100644 --- a/testsuite/tests/typecheck/should_fail/T7869.stderr +++ b/testsuite/tests/typecheck/should_fail/T7869.stderr @@ -1,29 +1,16 @@ -T7869.hs:3:12: - Couldn't match type ‘a’ with ‘a1’ - because type variable ‘a1’ would escape its scope - This (rigid, skolem) type variable is bound by - an expression type signature: [a1] -> b1 - at T7869.hs:3:5-27 - Expected type: [a1] -> b1 - Actual type: [a] -> b - In the expression: f x - In the expression: (\ x -> f x) :: [a] -> b - In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b - Relevant bindings include - x :: [a1] (bound at T7869.hs:3:7) - f :: [a] -> b (bound at T7869.hs:3:1) - -T7869.hs:3:12: - Couldn't match type ‘b’ with ‘b1’ - because type variable ‘b1’ would escape its scope - This (rigid, skolem) type variable is bound by - an expression type signature: [a1] -> b1 - at T7869.hs:3:5-27 - Expected type: [a1] -> b1 - Actual type: [a] -> b - In the expression: f x - In the expression: (\ x -> f x) :: [a] -> b - In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b - Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1) - +T7869.hs:3:12: error: + • Couldn't match type ‘a’ with ‘a1’ + because type variable ‘a1’ would escape its scope + This (rigid, skolem) type variable is bound by + an expression type signature: + [a1] -> b1 + at T7869.hs:3:5-27 + Expected type: [a1] -> b1 + Actual type: [a] -> b + • In the expression: f x + In the expression: (\ x -> f x) :: [a] -> b + In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b + • Relevant bindings include + x :: [a1] (bound at T7869.hs:3:7) + f :: [a] -> b (bound at T7869.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/T8883.stderr b/testsuite/tests/typecheck/should_fail/T8883.stderr index b18a97acb1..25fd7c06a0 100644 --- a/testsuite/tests/typecheck/should_fail/T8883.stderr +++ b/testsuite/tests/typecheck/should_fail/T8883.stderr @@ -1,8 +1,8 @@ -
-T8883.hs:20:1: error:
- Non type-variable argument in the constraint: Functor (PF a)
- (Use FlexibleContexts to permit this)
- When checking the inferred type
- fold :: forall b a.
- (Functor (PF a), Regular a) =>
- (PF a b -> b) -> a -> b
+ +T8883.hs:20:1: error: + • Non type-variable argument in the constraint: Functor (PF a) + (Use FlexibleContexts to permit this) + • When checking the inferred type + fold :: forall b a. + (Regular a, Functor (PF a)) => + (PF a b -> b) -> a -> b diff --git a/testsuite/tests/typecheck/should_fail/T9415.stderr b/testsuite/tests/typecheck/should_fail/T9415.stderr index 516759ee30..3250b67cd3 100644 --- a/testsuite/tests/typecheck/should_fail/T9415.stderr +++ b/testsuite/tests/typecheck/should_fail/T9415.stderr @@ -1,8 +1,14 @@ -T9415.hs:3:1: - Cycle in class declaration (via superclasses): C -> D -> C - In the class declaration for ‘C’ +T9415.hs:3:1: error: + • Superclass cycle for ‘C’ + one of whose superclasses is ‘D’ + one of whose superclasses is ‘C’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘C’ -T9415.hs:5:1: - Cycle in class declaration (via superclasses): D -> C -> D - In the class declaration for ‘D’ +T9415.hs:5:1: error: + • Superclass cycle for ‘D’ + one of whose superclasses is ‘C’ + one of whose superclasses is ‘D’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘D’ diff --git a/testsuite/tests/typecheck/should_fail/T9739.stderr b/testsuite/tests/typecheck/should_fail/T9739.stderr index 34e2f114f8..c35440a234 100644 --- a/testsuite/tests/typecheck/should_fail/T9739.stderr +++ b/testsuite/tests/typecheck/should_fail/T9739.stderr @@ -1,10 +1,14 @@ -T9739.hs:4:1: - Cycle in class declaration (via superclasses): - Class1 -> Class3 -> Class1 - In the class declaration for ‘Class1’ +T9739.hs:4:1: error: + • Superclass cycle for ‘Class1’ + one of whose superclasses is ‘Class3’ + one of whose superclasses is ‘Class1’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘Class1’ -T9739.hs:9:1: - Cycle in class declaration (via superclasses): - Class3 -> Class1 -> Class3 - In the class declaration for ‘Class3’ +T9739.hs:9:1: error: + • Superclass cycle for ‘Class3’ + one of whose superclasses is ‘Class1’ + one of whose superclasses is ‘Class3’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘Class3’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail027.stderr b/testsuite/tests/typecheck/should_fail/tcfail027.stderr index 9cfdcf4a9a..e8b2770e2b 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail027.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail027.stderr @@ -1,8 +1,14 @@ -tcfail027.hs:4:1: - Cycle in class declaration (via superclasses): A -> B -> A - In the class declaration for ‘A’ +tcfail027.hs:4:1: error: + • Superclass cycle for ‘A’ + one of whose superclasses is ‘B’ + one of whose superclasses is ‘A’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘A’ -tcfail027.hs:7:1: - Cycle in class declaration (via superclasses): B -> A -> B - In the class declaration for ‘B’ +tcfail027.hs:7:1: error: + • Superclass cycle for ‘B’ + one of whose superclasses is ‘A’ + one of whose superclasses is ‘B’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘B’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail216.hs b/testsuite/tests/typecheck/should_fail/tcfail216.hs index 34d4882e02..16a56e082e 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail216.hs +++ b/testsuite/tests/typecheck/should_fail/tcfail216.hs @@ -1,4 +1,3 @@ --- Test we do get a cycle for superclasses escaping via a free tyvar {-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, UndecidableInstances #-} module TcFail where diff --git a/testsuite/tests/typecheck/should_fail/tcfail216.stderr b/testsuite/tests/typecheck/should_fail/tcfail216.stderr index d354867480..520f5590dd 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail216.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail216.stderr @@ -1,4 +1,7 @@ -tcfail216.hs:5:1: - Cycle in class declaration (via superclasses): A -> A - In the class declaration for ‘A’ +tcfail216.hs:4:1: error: + • Potential superclass cycle for ‘A’ + one of whose superclass constraints is headed by a type variable: + ‘cls (A cls)’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘A’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail217.hs b/testsuite/tests/typecheck/should_fail/tcfail217.hs index 47c5078f02..62a6e5bae8 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail217.hs +++ b/testsuite/tests/typecheck/should_fail/tcfail217.hs @@ -4,4 +4,4 @@ module TcFail where type Aish = A -class cls (Aish cls) => A cls c where +class Aish a => A a where diff --git a/testsuite/tests/typecheck/should_fail/tcfail217.stderr b/testsuite/tests/typecheck/should_fail/tcfail217.stderr index 0dc1a593b1..729080373c 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail217.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail217.stderr @@ -1,4 +1,6 @@ tcfail217.hs:7:1: error: - Cycle in class declaration (via superclasses): A -> Aish -> A - In the class declaration for ‘A’ + • Superclass cycle for ‘A’ + one of whose superclasses is ‘A’ + Use UndecidableSuperClasses to accept this + • In the class declaration for ‘A’ |