diff options
Diffstat (limited to 'compiler/GHC/Tc')
| -rw-r--r-- | compiler/GHC/Tc/Errors.hs | 10 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 24 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/InertSet.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 138 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Instance.hs | 6 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Origin.hs | 77 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 5 |
7 files changed, 180 insertions, 82 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index 7177f7347f..6a6ccecf20 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -1028,11 +1028,11 @@ tryReporter ctxt (str, keep_me, suppress_after, reporter) cts pprArising :: CtOrigin -> SDoc -- Used for the main, top-level error message --- We've done special processing for TypeEq, KindEq, Given -pprArising (TypeEqOrigin {}) = empty -pprArising (KindEqOrigin {}) = empty -pprArising (GivenOrigin {}) = empty -pprArising orig = pprCtOrigin orig +-- We've done special processing for TypeEq, KindEq, givens +pprArising (TypeEqOrigin {}) = empty +pprArising (KindEqOrigin {}) = empty +pprArising orig | isGivenOrigin orig = empty + | otherwise = pprCtOrigin orig -- Add the "arising from..." part to a message about bunch of dicts addArising :: CtOrigin -> SDoc -> SDoc diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 5a504211f0..0ec6532105 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -586,23 +586,23 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) -- get down to a base predicate, we'll include its size. -- #10335 - | GivenOrigin skol_info <- ctLocOrigin loc -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance - -- for explantation of InstSC and Note [Replacement vs keeping] in - -- GHC.Tc.Solver.Interact for why we need OtherSC and depths - = let new_skol_info = case skol_info of + -- for explantation of InstSCOrigin and Note [Replacement vs keeping] in + -- GHC.Tc.Solver.Interact for why we need OtherSCOrigin and depths + | otherwise + = loc { ctl_origin = new_orig } + where + new_orig = case ctLocOrigin loc of -- these cases are when we have something that's already a superclass constraint - InstSC sc_depth n -> InstSC (sc_depth + 1) (n `max` size) - OtherSC sc_depth si -> OtherSC (sc_depth + 1) si + InstSCOrigin sc_depth n -> InstSCOrigin (sc_depth + 1) (n `max` size) + OtherSCOrigin sc_depth si -> OtherSCOrigin (sc_depth + 1) si -- these cases do not already have a superclass constraint: depth starts at 1 - InstSkol -> InstSC 1 size - _ -> OtherSC 1 skol_info - in - loc { ctl_origin = GivenOrigin new_skol_info } + GivenOrigin InstSkol -> InstSCOrigin 1 size + GivenOrigin other_skol -> OtherSCOrigin 1 other_skol - | otherwise -- Probably doesn't happen, since this function - = loc -- is only used for Givens, but does no harm + other_orig -> pprPanic "Given constraint without given origin" $ + ppr evar $$ ppr other_orig mk_strict_superclasses rec_clss ev tvs theta cls tys | all noFreeVarsOfType tys diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index 0ab5f5facb..53b6097ec7 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -1649,7 +1649,7 @@ mightEqualLater (IS { inert_cycle_breakers = cbvs }) prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance prohibitedSuperClassSolve from_loc solve_loc - | GivenOrigin (InstSC _ given_size) <- ctLocOrigin from_loc + | InstSCOrigin _ given_size <- ctLocOrigin from_loc , ScOrigin wanted_size <- ctLocOrigin solve_loc = given_size >= wanted_size | otherwise diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index a1bd9f7d0b..a088637e46 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -491,7 +491,7 @@ solveOneFromTheOther ev_i ev_w -- After this, neither ev_i or ev_w are Derived | CtWanted { ctev_loc = loc_w } <- ev_w - , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w + , prohibitedSuperClassSolve loc_i loc_w = -- inert must be Given do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w) ; return KeepWork } @@ -539,31 +539,28 @@ solveOneFromTheOther ev_i ev_w different_level_strategy -- Both Given | isIPLikePred pred = if lvl_w > lvl_i then KeepWork else KeepInert | otherwise = if lvl_w > lvl_i then KeepInert else KeepWork - -- See Note [Replacement vs keeping] (the different-level bullet) + -- See Note [Replacement vs keeping] part (1) -- For the isIPLikePred case see Note [Shadowing of Implicit Parameters] same_level_strategy -- Both Given - = case (un_given (ctLocOrigin loc_i), un_given (ctLocOrigin loc_w)) of - -- case 2(b) from Note [Replacement vs keeping] - (InstSC _depth_i size_i, InstSC _depth_w size_w) | size_w < size_i -> KeepWork - | otherwise -> KeepInert + = case (ctLocOrigin loc_i, ctLocOrigin loc_w) of + -- case 2(a) from Note [Replacement vs keeping] + (InstSCOrigin _depth_i size_i, InstSCOrigin _depth_w size_w) + | size_w < size_i -> KeepWork + | otherwise -> KeepInert -- case 2(c) from Note [Replacement vs keeping] - (InstSC depth_i _, OtherSC depth_w _) -> choose_shallower depth_i depth_w - (OtherSC depth_i _, InstSC depth_w _) -> choose_shallower depth_i depth_w - (OtherSC depth_i _, OtherSC depth_w _) -> choose_shallower depth_i depth_w + (InstSCOrigin depth_i _, OtherSCOrigin depth_w _) -> choose_shallower depth_i depth_w + (OtherSCOrigin depth_i _, InstSCOrigin depth_w _) -> choose_shallower depth_i depth_w + (OtherSCOrigin depth_i _, OtherSCOrigin depth_w _) -> choose_shallower depth_i depth_w - -- case 2(a) from Note [Replacement vs keeping] - (InstSC {}, _) -> KeepWork - (OtherSC {}, _) -> KeepWork + -- case 2(b) from Note [Replacement vs keeping] + (InstSCOrigin {}, _) -> KeepWork + (OtherSCOrigin {}, _) -> KeepWork -- case 2(d) from Note [Replacement vs keeping] _ -> KeepInert - un_given (GivenOrigin skol_info) = skol_info - un_given orig = pprPanic "Given without GivenOrigin in solveOneFromTheOther" $ - vcat [ppr ev_i, ppr ev_w, ppr orig] - choose_shallower depth_i depth_w | depth_w < depth_i = KeepWork | otherwise = KeepInert -- favor KeepInert in the equals case, according to 2(d) from the Note @@ -592,7 +589,10 @@ solveOneFromTheOther. 2) Constraints coming from the same level (i.e. same implication) - (a) Prefer constraints that are not superclass selections. Example: + (a) If both are InstSCOrigin, choose the one with the smallest TypeSize, + according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance. + + (b) Prefer constraints that are not superclass selections. Example: f :: (Eq a, Ord a) => a -> Bool f x = x == x @@ -605,20 +605,18 @@ solveOneFromTheOther. Getting this wrong was #20602. See also Note [Tracking redundant constraints] in GHC.Tc.Solver. - (b) If both are InstSC, choose the one with the smallest TypeSize, - according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance. - - (c) If both are superclass selections (but not both InstSC), choose the one + (c) If both are superclass selections (but not both InstSCOrigin), choose the one with the shallower superclass-selection depth, in the hope of identifying more correct redundant constraints. This is really a generalization of - point (a). + point (b), because the superclass depth of a non-superclass + constraint is 0. (d) Finally, when there is still a choice, use KeepInert rather than KeepWork, for two reasons: - to avoid unnecessary munging of the inert set. - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Canonical -Doing the depth-check for implicit parameters, rather than making the work item +Doing the level-check for implicit parameters, rather than making the work item always override, is important. Consider data T a where { T1 :: (?x::Int) => T Int; T2 :: T a } @@ -634,7 +632,7 @@ Now consider these steps - process a~Int, kicking out (?x::a) - process (?x::Int), the inner given, adding to inert set - process (?x::a), the outer given, overriding the inner given -Wrong! The depth-check ensures that the inner implicit parameter wins. +Wrong! The level-check ensures that the inner implicit parameter wins. (Actually I think that the order in which the work-list is processed means that this chain of events won't happen, but that's very fragile.) @@ -2455,35 +2453,57 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult matchLocalInst pred loc = do { inerts@(IS { inert_cans = ics }) <- getTcSInerts ; case match_local_inst inerts (inert_insts ics) of - ([], False) -> do { traceTcS "No local instance for" (ppr pred) - ; return NoInstance } - ([(dfun_ev, inst_tys)], unifs) - | not unifs + ([], Nothing) -> do { traceTcS "No local instance for" (ppr pred) + ; return NoInstance } + + -- See Note [Use only the best local instance] about + -- superclass depths + (matches, unifs) + | [(dfun_ev, inst_tys)] <- best_matches + , maybe True (> min_sc_depth) unifs -> do { let dfun_id = ctEvEvId dfun_ev ; (tys, theta) <- instDFunType dfun_id inst_tys ; let result = OneInst { cir_new_theta = theta , cir_mk_ev = evDFunApp dfun_id tys , cir_what = LocalInstance } - ; traceTcS "Local inst found:" (ppr result) + ; traceTcS "Best local inst found:" (ppr result) + ; traceTcS "All local insts:" (ppr matches) ; return result } - _ -> do { traceTcS "Multiple local instances for" (ppr pred) - ; return NotSure }} + + | otherwise + -> do { traceTcS "Multiple local instances for" (ppr pred) + ; return NotSure } + + where + extract_depth = sc_depth . ctEvLoc . fst + min_sc_depth = minimum (map extract_depth matches) + best_matches = filter ((== min_sc_depth) . extract_depth) matches } where pred_tv_set = tyCoVarsOfType pred + sc_depth :: CtLoc -> Int + sc_depth ctloc = case ctLocOrigin ctloc of + InstSCOrigin depth _ -> depth + OtherSCOrigin depth _ -> depth + _ -> 0 + + -- See Note [Use only the best local instance] about superclass depths match_local_inst :: InertSet -> [QCInst] -> ( [(CtEvidence, [DFunInstType])] - , Bool ) -- True <=> Some unify but do not match + , Maybe Int ) -- Nothing ==> no unifying local insts + -- Just n ==> unifying local insts, with + -- minimum superclass depth + -- of n match_local_inst _inerts [] - = ([], False) + = ([], Nothing) match_local_inst inerts (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred - , qci_ev = ev }) + , qci_ev = qev }) : qcis) | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set) , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope) emptyTvSubstEnv qpred pred - , let match = (ev, map (lookupVarEnv tv_subst) qtvs) + , let match = (qev, map (lookupVarEnv tv_subst) qtvs) = (match:matches, unif) | otherwise @@ -2491,8 +2511,52 @@ matchLocalInst pred loc (ppr qci $$ ppr pred) -- ASSERT: unification relies on the -- quantified variables being fresh - (matches, unif || this_unif) + (matches, unif `combine` this_unif) where + qloc = ctEvLoc qev qtv_set = mkVarSet qtvs - this_unif = mightEqualLater inerts qpred (ctEvLoc ev) pred loc + this_unif + | mightEqualLater inerts qpred qloc pred loc = Just (sc_depth qloc) + | otherwise = Nothing (matches, unif) = match_local_inst inerts qcis + + combine Nothing Nothing = Nothing + combine (Just n) Nothing = Just n + combine Nothing (Just n) = Just n + combine (Just n1) (Just n2) = Just (n1 `min` n2) + +{- Note [Use only the best local instance] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (#20582) the ambiguity check for + (forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int + +Because of eager expansion of given superclasses, we get + [G] forall a. Ord (m a) + [G] forall a. Eq (m a) + [G] forall a. Semigroup a => Eq (m a) + + [W] forall a. Ord (m a) + [W] forall a. Semigroup a => Eq (m a) + +The first wanted is solved straightforwardly. But the second wanted +matches *two* local instances. Our general rule around multiple local +instances is that we refuse to commit to any of them. However, that +means that our type fails the ambiguity check. That's bad: the type +is perfectly fine. (This actually came up in the wild, in the streamly +library.) + +The solution is to prefer local instances with fewer superclass selections. +So, matchLocalInst is careful to whittle down the matches only to the +ones with the shallowest superclass depth, and also to worry about unifying +local instances that are at that depth (or less). + +By preferring these shallower local instances, we can use the last given +listed above and pass the ambiguity check. + +The instance-depth mechanism uses the same superclass depth +information as described in Note [Replacement vs keeping], 2a. + +Test case: typecheck/should_compile/T20582. + +-} + diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 26e1689e59..98fb149c27 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -1601,9 +1601,9 @@ Answer: GivenOrigin InstSkol. * When we make a superclass selection from InstSkol we use - a SkolemInfo of (InstSC size), where 'size' is the size of - the constraint whose superclass we are taking. A similarly - when taking the superclass of an InstSC. This is implemented + a CtOrigin of (InstSCOrigin size), where 'size' is the size of + the constraint whose superclass we are taking. And similarly + when taking the superclass of an InstSCOrigin. This is implemented in GHC.Tc.Solver.Canonical.mk_strict_superclasses (in the mk_given_loc helper function). diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 7953336a6b..a2229342d8 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -220,21 +220,6 @@ data SkolemInfo | InstSkol -- Bound at an instance decl - -- | A "given" constraint obtained by superclass selection. - | InstSC Int -- ^ The number of superclass selections necessary to - -- get this constraint; see Note [Replacement vs keeping] in - -- GHC.Tc.Solver.Interact - TypeSize -- ^ If @(C ty1 .. tyn)@ is the largest class from - -- which we made a superclass selection in the chain, - -- then @TypeSize = sizeTypes [ty1, .., tyn]@ - -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance - - -- | A "given" constraint obtained by superclass selection, but not from an instance context. - -- Needed for Note [Replacement vs keeping] in GHC.Tc.Solver.Interact. - | OtherSC Int -- ^ The number of superclass selections necessary to - -- get this constraint - SkolemInfo -- ^ Where the sub-class constraint arose from - | FamInstSkol -- Bound at a family instance decl | PatSkol -- An existential type variable bound by a pattern for ConLike -- a data constructor with an existential type. @@ -284,8 +269,6 @@ pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural <+> pprWithCommas ppr ips pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred) pprSkolInfo InstSkol = text "the instance declaration" -pprSkolInfo (InstSC _ n) = text "the instance declaration" <> whenPprDebug (parens (ppr n)) -pprSkolInfo (OtherSC _ si) = pprSkolInfo si -- superclass constraints don't bind skolems pprSkolInfo FamInstSkol = text "a family instance declaration" pprSkolInfo BracketSkol = text "a Template Haskell bracket" pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name @@ -376,9 +359,44 @@ in the right place. So we proceed as follows: -} data CtOrigin - = GivenOrigin SkolemInfo + = -- | A given constraint from a user-written type signature. The + -- 'SkolemInfo' inside gives more information. + GivenOrigin SkolemInfo + + -- The following are other origins for given constraints that cannot produce + -- new skolems -- hence no SkolemInfo. + + -- | 'InstSCOrigin' is used for a Given constraint obtained by superclass selection + -- from the context of an instance declaration. E.g. + -- instance @(Foo a, Bar a) => C [a]@ where ... + -- When typechecking the instance decl itself, including producing evidence + -- for the superclasses of @C@, the superclasses of @(Foo a)@ and @(Bar a)@ will + -- have 'InstSCOrigin' origin. + | InstSCOrigin ScDepth -- ^ The number of superclass selections necessary to + -- get this constraint; see Note [Replacement vs keeping] + -- and Note [Use only the best local instance], both in + -- GHC.Tc.Solver.Interact + TypeSize -- ^ If @(C ty1 .. tyn)@ is the largest class from + -- which we made a superclass selection in the chain, + -- then @TypeSize = sizeTypes [ty1, .., tyn]@ + -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance + + -- | 'OtherSCOrigin' is used for a Given constraint obtained by superclass + -- selection from a constraint /other than/ the context of an instance + -- declaration. (For the latter we use 'InstSCOrigin'.) E.g. + -- f :: Foo a => blah + -- f = e + -- When typechecking body of 'f', the superclasses of the Given (Foo a) + -- will have 'OtherSCOrigin'. + -- Needed for Note [Replacement vs keeping] and + -- Note [Use only the best local instance], both in GHC.Tc.Solver.Interact. + | OtherSCOrigin ScDepth -- ^ The number of superclass selections necessary to + -- get this constraint + SkolemInfo -- ^ Where the sub-class constraint arose from + -- (used only for printing) -- All the others are for *wanted* constraints + | OccurrenceOf Name -- Occurrence of an overloaded identifier | OccurrenceOfRecSel RdrName -- Occurrence of a record selector | AppOrigin -- An application of some kind @@ -422,10 +440,12 @@ data CtOrigin | RecordUpdOrigin | ViewPatOrigin - | ScOrigin TypeSize -- Typechecking superclasses of an instance declaration - -- If the instance head is C ty1 .. tyn - -- then TypeSize = sizeTypes [ty1, .., tyn] - -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance + -- | 'ScOrigin' is used only for the Wanted constraints for the + -- superclasses of an instance declaration. + -- If the instance head is @C ty1 .. tyn@ + -- then @TypeSize = sizeTypes [ty1, .., tyn]@ + -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance + | ScOrigin TypeSize | DerivClauseOrigin -- Typechecking a deriving clause (as opposed to -- standalone deriving). @@ -497,6 +517,11 @@ data CtOrigin -- We record it here for access in 'GHC.Tc.Errors.mkFRRErr'. !FRROrigin +-- | The number of superclass selections needed to get this Given. +-- If @d :: C ty@ has @ScDepth=2@, then the evidence @d@ will look +-- like @sc_sel (sc_sel dg)@, where @dg@ is a Given. +type ScDepth = Int + -- An origin is visible if the place where the constraint arises is manifest -- in user code. Currently, all origins are visible except for invisible -- TypeEqOrigins. This is used when choosing which error of @@ -514,6 +539,8 @@ toInvisibleOrigin orig = orig isGivenOrigin :: CtOrigin -> Bool isGivenOrigin (GivenOrigin {}) = True +isGivenOrigin (InstSCOrigin {}) = True +isGivenOrigin (OtherSCOrigin {}) = True isGivenOrigin (FunDepOrigin1 _ o1 _ _ o2 _) = isGivenOrigin o1 && isGivenOrigin o2 isGivenOrigin (FunDepOrigin2 _ o1 _ _) = isGivenOrigin o1 isGivenOrigin (CycleBreakerOrigin o) = isGivenOrigin o @@ -591,7 +618,9 @@ lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS" pprCtOrigin :: CtOrigin -> SDoc -- "arising from ..." -- Not an instance of Outputable because of the "arising from" prefix -pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk +pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk +pprCtOrigin (InstSCOrigin {}) = ctoHerald <+> pprSkolInfo InstSkol -- keep output in sync +pprCtOrigin (OtherSCOrigin _ si) = ctoHerald <+> pprSkolInfo si pprCtOrigin (SpecPragOrigin ctxt) = case ctxt of @@ -717,6 +746,8 @@ pprCtO BracketOrigin = text "a quotation bracket" -- get here via callStackOriginFS, when doing ambiguity checks -- A bit silly, but no great harm pprCtO (GivenOrigin {}) = text "a given constraint" +pprCtO (InstSCOrigin {}) = text "the superclass of an instance constraint" +pprCtO (OtherSCOrigin {}) = text "the superclass of a given constraint" pprCtO (SpecPragOrigin {}) = text "a SPECIALISE pragma" pprCtO (FunDepOrigin1 {}) = text "a functional dependency" pprCtO (FunDepOrigin2 {}) = text "a functional dependency" diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 65c5d3a50e..56facd6970 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -2428,7 +2428,6 @@ zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys ; return (InferSkol ntys') } where do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') } -zonkSkolemInfo (OtherSC depth si) = OtherSC depth <$> zonkSkolemInfo si zonkSkolemInfo skol_info = return skol_info {- @@ -2567,6 +2566,10 @@ zonkTidyOrigin env (GivenOrigin skol_info) = do { skol_info1 <- zonkSkolemInfo skol_info ; let skol_info2 = tidySkolemInfo env skol_info1 ; return (env, GivenOrigin skol_info2) } +zonkTidyOrigin env (OtherSCOrigin sc_depth skol_info) + = do { skol_info1 <- zonkSkolemInfo skol_info + ; let skol_info2 = tidySkolemInfo env skol_info1 + ; return (env, OtherSCOrigin sc_depth skol_info2) } zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act , uo_expected = exp }) = do { (env1, act') <- zonkTidyTcType env act |