diff options
author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-05-17 22:24:54 +0100 |
---|---|---|
committer | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-05-17 22:26:07 +0100 |
commit | fbf5bcef8d532a88b68c15744d4df3c08a1c736c (patch) | |
tree | 75cf184ffeabee65a34bfe657a34af2a3e56dbd2 | |
parent | 8a9164911df87cbf4ec6d86d0119b64b03d7aa7b (diff) | |
download | haskell-wip/T23070-dicts.tar.gz |
Wibbleswip/T23070-dicts
-rw-r--r-- | compiler/GHC/Core/Predicate.hs | 89 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Dict.hs | 46 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/InertSet.hs | 21 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 4 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Types.hs | 24 | ||||
-rw-r--r-- | testsuite/tests/gadt/T3651.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/should_compile/T15450.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr | 12 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T20189.stderr | 10 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T22924b.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_run/Defer01.hs | 2 |
12 files changed, 110 insertions, 108 deletions
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs index 86acfbee23..1946d4cee9 100644 --- a/compiler/GHC/Core/Predicate.hs +++ b/compiler/GHC/Core/Predicate.hs @@ -25,7 +25,7 @@ module GHC.Core.Predicate ( classMethodTy, classMethodInstTy, -- Implicit parameters - isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass, + isIPLikePred, mentionsIP, isIPTyCon, isIPClass, isCallStackTy, isCallStackPred, isCallStackPredTy, isIPPred_maybe, @@ -260,39 +260,16 @@ isIPTyCon tc = tc `hasKey` ipClassKey isIPClass :: Class -> Bool isIPClass cls = cls `hasKey` ipClassKey -isIPLikePred :: Type -> Bool --- See Note [Local implicit parameters] -isIPLikePred = is_ip_like_pred initIPRecTc - - -is_ip_like_pred :: RecTcChecker -> Type -> Bool -is_ip_like_pred rec_clss ty - | Just (tc, tys) <- splitTyConApp_maybe ty - , Just rec_clss' <- if isTupleTyCon tc -- Tuples never cause recursion - then Just rec_clss - else checkRecTc rec_clss tc - , Just cls <- tyConClass_maybe tc - = isIPClass cls || has_ip_super_classes rec_clss' cls tys - +-- | Decomposes a predicate if it is an implicit parameter. Does not look in +-- superclasses. See also [Local implicit parameters]. +isIPPred_maybe :: Class -> [Type] -> Maybe (FastString, Type) +isIPPred_maybe cls tys + | isIPClass cls + , [t1,t2] <- tys + , Just x <- isStrLitTy t1 + = Just (x,t2) | otherwise - = False -- Includes things like (D []) where D is - -- a Constraint-ranged family; #7785 - -hasIPSuperClasses :: Class -> [Type] -> Bool --- See Note [Local implicit parameters] -hasIPSuperClasses = has_ip_super_classes initIPRecTc - -has_ip_super_classes :: RecTcChecker -> Class -> [Type] -> Bool -has_ip_super_classes rec_clss cls tys - = any ip_ish (classSCSelIds cls) - where - -- Check that the type of a superclass determines its value - -- sc_sel_id :: forall a b. C a b -> <superclass type> - ip_ish sc_sel_id = is_ip_like_pred rec_clss $ - classMethodInstTy sc_sel_id tys - -initIPRecTc :: RecTcChecker -initIPRecTc = setRecTcMaxBound 1 initRecTc + = Nothing -- --------------------- CallStack predicates --------------------------------- @@ -326,20 +303,48 @@ isCallStackTy ty | otherwise = False +-- --------------------- isIPLike and mentionsIP -------------------------- +-- See Note [Local implicit parameters] --- | Decomposes a predicate if it is an implicit parameter. Does not look in --- superclasses. See also [Local implicit parameters]. -isIPPred_maybe :: Class -> [Type] -> Maybe (FastString, Type) -isIPPred_maybe cls tys - | cls `hasKey` ipClassKey - , [t1,t2] <- tys - , Just x <- isStrLitTy t1 - = Just (x,t2) +isIPLikePred :: Type -> Bool +-- Is `pred`, or any of its superclasses, an implicit parameter? +-- See Note [Local implicit parameters] +isIPLikePred pred = mentions_ip_pred initIPRecTc Nothing pred + +mentionsIP :: FastString -> Class -> [Type] -> Bool +-- Is (cls tys) an implicit parameter with string `fs`, or +-- is any of its superclasses such at thing. +-- See Note [Local implicit parameters] +mentionsIP fs cls tys = mentions_ip initIPRecTc (Just fs) cls tys + +mentions_ip :: RecTcChecker -> Maybe FastString -> Class -> [Type] -> Bool +mentions_ip rec_clss mb_fs cls tys + | Just (fs', _) <- isIPPred_maybe cls tys + = case mb_fs of + Nothing -> True + Just fs -> fs == fs' | otherwise - = Nothing + = or [ mentions_ip_pred rec_clss mb_fs (classMethodInstTy sc_sel_id tys) + | sc_sel_id <- classSCSelIds cls ] + +mentions_ip_pred :: RecTcChecker -> Maybe FastString -> Type -> Bool +mentions_ip_pred rec_clss mb_fs ty + | Just (cls, tys) <- getClassPredTys_maybe ty + , let tc = classTyCon cls + , Just rec_clss' <- if isTupleTyCon tc then Just rec_clss + else checkRecTc rec_clss tc + = mentions_ip rec_clss' mb_fs cls tys + | otherwise + = False -- Includes things like (D []) where D is + -- a Constraint-ranged family; #7785 + +initIPRecTc :: RecTcChecker +initIPRecTc = setRecTcMaxBound 1 initRecTc {- Note [Local implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Shadowing of Implicit Parameters] in GHC.Tc.Solver.Dict. + The function isIPLikePred tells if this predicate, or any of its superclasses, is an implicit parameter. diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs index f0303a9aa0..ac5f3aae25 100644 --- a/compiler/GHC/Tc/Solver/Dict.hs +++ b/compiler/GHC/Tc/Solver/Dict.hs @@ -106,8 +106,10 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys }) ; stopWithStage (dictCtEvidence dict_ct) "Kept inert DictCt" } updInertDicts :: DictCt -> TcS () -updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev }) - = do { -- See Note [Shadowing of Implicit Parameters] +updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev, di_tys = tys }) + = do { traceTcS "Adding inert dict" (ppr dict_ct $$ ppr cls <+> ppr tys) + + -- See Note [Shadowing of Implicit Parameters] ; when (isGiven ev && isIPClass cls) $ updInertCans (updDicts (delIPDict dict_ct)) @@ -195,7 +197,24 @@ in two places: (?x :: ty) in the inert set and an identical (?x :: ty) as the work item. * In `updInertDicts` in this module, when adding [G] (?x :: ty), remove any - existing [G] (?x :: ty'), regardless of ty' + existing [G] (?x :: ty'), regardless of ty'. + +* Wrinkle (SIP1): we must be careful of superclasses. Consider + f,g :: (?x::Int, C a) => a -> a + f v = let ?x = 4 in g v + + The call to 'g' gives rise to a Wanted constraint (?x::Int, C a). + We must /not/ solve this from the Given (?x::Int, C a), because of + the intervening binding for (?x::Int). #14218. + + We deal with this by arranging that when we add [G] (?x::ty) we delete any + existing [G] (?x::ty) /and/ any [G] C tys, where (C tys) has a superclass + with (?x::ty). See Note [Local implicit parameters] in GHC.Core.Predicate. + An important special case is constraint tuples like [G] (% ?x::ty, Eq a ) + +* Wrinkle (SIP2): we delete dictionaries in inert_dicts, but we don't need to + look in inert_solved_dicts. They are never implicit parameters. See + Note [Solved dictionaries] in GHC.Tc.Solver.InertSet Example 1: @@ -248,13 +267,14 @@ behaviour. All this works for the normal cases but it has an odd side effect in some pathological programs like this: --- This is accepted, the second parameter shadows -f1 :: (?x :: Int, ?x :: Char) => Char -f1 = ?x --- This is rejected, the second parameter shadows -f2 :: (?x :: Int, ?x :: Char) => Int -f2 = ?x + -- This is accepted, the second parameter shadows + f1 :: (?x :: Int, ?x :: Char) => Char + f1 = ?x + + -- This is rejected, the second parameter shadows + f2 :: (?x :: Int, ?x :: Char) => Int + f2 = ?x Both of these are actually wrong: when we try to use either one, we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char), @@ -618,7 +638,8 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys ; continueWith () } } } | otherwise - = continueWith () + = do { traceTcS "tryInertDicts:no" (ppr dict_w $$ ppr cls <+> ppr tys) + ; continueWith () } -- See Note [Shortcut solving] shortCutSolver :: DynFlags @@ -810,9 +831,10 @@ matchClassInst dflags inerts clas tys loc -- whether top level, or local quantified constraints. -- See Note [Instance and Given overlap] | not (xopt LangExt.IncoherentInstances dflags) + , not (isCTupleClass clas) -- It is always safe to unpack constraint tuples , not (noMatchableGivenDicts inerts loc clas tys) = do { traceTcS "Delaying instance application" $ - vcat [ text "Work item=" <+> pprClassPred clas tys ] + vcat [ text "Work item:" <+> pprClassPred clas tys ] ; return NotSure } | otherwise @@ -989,7 +1011,7 @@ The same reasoning applies to And less obviously to: * Tuple classes. For reasons described in GHC.Tc.Solver.Types - Note [Tuples hiding implicit parameters], we may have a constraint + Note [Shadowing of implicit parameters], we may have a constraint [W] (?x::Int, C a) with an exactly-matching Given constraint. We must decompose this tuple and solve the components separately, otherwise we won't solve diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index 1b85fdab0c..f621de211b 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -79,6 +79,7 @@ import GHC.Utils.Panic import GHC.Utils.Panic.Plain import GHC.Data.Maybe import GHC.Data.Bag +import GHC.Data.FastString import Data.List.NonEmpty ( NonEmpty(..), (<|) ) import qualified Data.List.NonEmpty as NE @@ -321,6 +322,7 @@ data InertSet , inert_solved_dicts :: DictMap CtEvidence -- All Wanteds, of form (C t1 .. tn) + -- Always a dictionary solved by an instance decl; never an implict parameter -- See Note [Solved dictionaries] -- and Note [Do not add superclasses of solved dictionaries] } @@ -1323,20 +1325,15 @@ delDict (DictCt { di_cls = cls, di_tys = tys }) m = delTcApp m (classTyCon cls) tys delIPDict :: DictCt -> DictMap DictCt -> DictMap DictCt -delIPDict (DictCt { di_cls = cls, di_tys = tys }) m - | [ip_str, _] <- tys - = assert (isIPClass cls) $ - filterDicts (doesn't_match ip_str) m +delIPDict dict@(DictCt { di_cls = cls, di_tys = tys }) dict_map + | Just (fs, _) <- isIPPred_maybe cls tys + = filterDicts (doesn't_match fs) dict_map | otherwise - = m + = pprPanic "delIPDict" (ppr dict) where - doesn't_match :: TcType -> DictCt -> Bool - doesn't_match ip_str (DictCt { di_cls = cls, di_tys = tys }) - | isIPClass cls - , [ip_str', _] <- tys - = not (ip_str `eqType` ip_str') - | otherwise - = True + doesn't_match :: FastString -> DictCt -> Bool + doesn't_match fs (DictCt { di_cls = cls, di_tys = tys }) + = not (mentionsIP fs cls tys) addDict :: DictCt -> DictMap DictCt -> DictMap DictCt addDict item@(DictCt { di_cls = cls, di_tys = tys }) dm diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index d385d27b29..c89a9f282b 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -707,9 +707,7 @@ lookupInInerts loc pty -- | Look up a dictionary inert. lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt lookupInertDict (IC { inert_dicts = dicts }) loc cls tys - = case findDict dicts loc cls tys of - Just ct -> Just ct - _ -> Nothing + = findDict dicts loc cls tys -- | Look up a solved inert. lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs index 0d34022df7..d47eef71b7 100644 --- a/compiler/GHC/Tc/Solver/Types.hs +++ b/compiler/GHC/Tc/Solver/Types.hs @@ -133,9 +133,6 @@ emptyDictMap = emptyTcAppMap findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a findDict m loc cls tys - | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters] - = Nothing - | Just {} <- isCallStackPred cls tys , isPushCallStackOrigin (ctLocOrigin loc) = Nothing -- See Note [Solving CallStack constraints] @@ -157,25 +154,8 @@ dictsToBag = tcAppMapToBag foldDicts :: (a -> b -> b) -> DictMap a -> b -> b foldDicts = foldTcAppMap -{- Note [Tuples hiding implicit parameters] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - f,g :: (?x::Int, C a) => a -> a - f v = let ?x = 4 in g v - -The call to 'g' gives rise to a Wanted constraint (?x::Int, C a). -We must /not/ solve this from the Given (?x::Int, C a), because of -the intervening binding for (?x::Int). #14218. - -We deal with this by arranging that we always fail when looking up a -tuple constraint that hides an implicit parameter. Note that this applies - * both to the inert_dicts (lookupInertDict) - * and to the solved_dicts (looukpSolvedDict) -An alternative would be not to extend these sets with such tuple -constraints, but it seemed more direct to deal with the lookup. - -Note [Solving CallStack constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Solving CallStack constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See also Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence. Suppose f :: HasCallStack => blah. Then diff --git a/testsuite/tests/gadt/T3651.stderr b/testsuite/tests/gadt/T3651.stderr index b4c7a2e65d..aaf69f6dec 100644 --- a/testsuite/tests/gadt/T3651.stderr +++ b/testsuite/tests/gadt/T3651.stderr @@ -6,7 +6,7 @@ T3651.hs:11:15: error: [GHC-83865] • In the expression: () In an equation for ‘unsafe1’: unsafe1 B U = () -T3651.hs:14:15: error: [GHC-83865] +T3651.hs:27:15: error: [GHC-83865] • Couldn't match type ‘()’ with ‘Bool’ Expected: a Actual: () diff --git a/testsuite/tests/pmcheck/should_compile/T15450.stderr b/testsuite/tests/pmcheck/should_compile/T15450.stderr index 18f4a931f8..ca5f6ae71c 100644 --- a/testsuite/tests/pmcheck/should_compile/T15450.stderr +++ b/testsuite/tests/pmcheck/should_compile/T15450.stderr @@ -1,11 +1,11 @@ -T15450.hs:6:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] +T15450.hs:8:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] Pattern match(es) are non-exhaustive In a case alternative: Patterns of type ‘Bool’ not matched: False True -T15450.hs:9:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] +T15450.hs:11:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] Pattern match(es) are non-exhaustive In a case alternative: Patterns of type ‘Bool’ not matched: False diff --git a/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr index ae71b40a91..b615c3b86f 100644 --- a/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr +++ b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr @@ -1,20 +1,20 @@ -GivenForallLoop.hs:8:11: error: [GHC-25897] +GivenForallLoop.hs:9:11: error: [GHC-25897] • Could not deduce ‘a ~ b’ from the context: a ~ (forall b1. F a b1) bound by the type signature for: loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b - at GivenForallLoop.hs:7:1-42 + at GivenForallLoop.hs:8:1-42 ‘a’ is a rigid type variable bound by the type signature for: loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b - at GivenForallLoop.hs:7:1-42 + at GivenForallLoop.hs:8:1-42 ‘b’ is a rigid type variable bound by the type signature for: loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b - at GivenForallLoop.hs:7:1-42 + at GivenForallLoop.hs:8:1-42 • In the expression: x In an equation for ‘loopy’: loopy x = x • Relevant bindings include - x :: a (bound at GivenForallLoop.hs:8:7) - loopy :: a -> b (bound at GivenForallLoop.hs:8:1) + x :: a (bound at GivenForallLoop.hs:9:7) + loopy :: a -> b (bound at GivenForallLoop.hs:9:1) diff --git a/testsuite/tests/typecheck/should_fail/T20189.stderr b/testsuite/tests/typecheck/should_fail/T20189.stderr index 077f57d6d5..e1dd352506 100644 --- a/testsuite/tests/typecheck/should_fail/T20189.stderr +++ b/testsuite/tests/typecheck/should_fail/T20189.stderr @@ -1,12 +1,12 @@ -T20189.hs:6:5: error: [GHC-88464] +T20189.hs:7:5: error: [GHC-88464] • Found hole: _ :: t Where: ‘t’ is a rigid type variable bound by the type signature for: y :: forall t. (t ~ (forall x. Show x => x -> IO ())) => t - at T20189.hs:5:1-49 + at T20189.hs:6:1-49 • In an equation for ‘y’: y = _ - • Relevant bindings include y :: t (bound at T20189.hs:6:1) + • Relevant bindings include y :: t (bound at T20189.hs:7:1) Constraints include - t ~ (forall x. Show x => x -> IO ()) (from T20189.hs:5:1-49) - Valid hole fits include y :: t (bound at T20189.hs:6:1) + t ~ (forall x. Show x => x -> IO ()) (from T20189.hs:6:1-49) + Valid hole fits include y :: t (bound at T20189.hs:7:1) diff --git a/testsuite/tests/typecheck/should_fail/T22924b.stderr b/testsuite/tests/typecheck/should_fail/T22924b.stderr index ba4bd79198..46f456fc1f 100644 --- a/testsuite/tests/typecheck/should_fail/T22924b.stderr +++ b/testsuite/tests/typecheck/should_fail/T22924b.stderr @@ -1,7 +1,7 @@ T22924b.hs:10:5: error: • Reduction stack overflow; size = 201 - When simplifying the following type: R + When simplifying the following type: S Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr index bbb18280c7..be1b5928b3 100644 --- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr +++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr @@ -50,7 +50,7 @@ TcCoercibleFail.hs:30:9: error: [GHC-18872] TcCoercibleFail.hs:35:8: error: • Reduction stack overflow; size = 201 - When simplifying the following type: Age + When simplifying the following type: Fix (Either Age) Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if diff --git a/testsuite/tests/typecheck/should_run/Defer01.hs b/testsuite/tests/typecheck/should_run/Defer01.hs index 551c626f7c..8fcf999b32 100644 --- a/testsuite/tests/typecheck/should_run/Defer01.hs +++ b/testsuite/tests/typecheck/should_run/Defer01.hs @@ -1,8 +1,8 @@ -- Test -fdefer-type-errors -- Should compile and run - {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE AllowAmbiguousTypes #-} -- Allows the strange type for `k` {-# OPTIONS_GHC -fdefer-type-errors #-} module Main where |