[Git][ghc/ghc][wip/T23070-dicts] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon May 15 11:00:17 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
f72a67cc by Simon Peyton Jones at 2023-05-15T12:02:12+01:00
Wibbles
- - - - -
2 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Irred.hs
Changes:
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -69,14 +69,17 @@ solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage ()
-- NC: this comes from CNonCanonical or CIrredCan
-- Precondition: already rewritten by inert set
solveDictNC ev cls tys
- = do { dict_ct <- canDictCt ev cls tys
+ = do { simpleStage $ traceTcS "solveDictNC" (ppr (mkClassPred cls tys) $$ ppr ev)
+ ; dict_ct <- canDictCt ev cls tys
; solveDict dict_ct }
solveDict :: DictCt -> SolverStage ()
-- Preconditions: `tys` are already rewritten by the inert set
solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
= assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
- do { tryInertDicts dict_ct
+ do { simpleStage $ traceTcS "solveDict" (ppr dict_ct)
+
+ ; tryInertDicts dict_ct
; tryInstances dict_ct
-- Try fundeps /after/ tryInstances:
@@ -182,20 +185,84 @@ solveCallStack ev ev_cs
{- Note [Kick out existing binding for implicit parameter]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we add a new /given/ implicit parameter to the inert set, it /replaces/
+any existing givens for the same implicit parameter.
+
+Example 1:
+
Suppose we have (typecheck/should_compile/ImplicitParamFDs)
flub :: (?x :: Int) => (Int, Integer)
flub = (?x, let ?x = 5 in ?x)
-When we are checking the last ?x occurrence, we guess its type
-to be a fresh unification variable alpha and emit an (IP "x" alpha)
-constraint. But the given (?x :: Int) has been translated to an
-IP "x" Int constraint, which has a functional dependency from the
-name to the type. So fundep interaction tells us that alpha ~ Int,
-and we get a type error. This is bad.
-
-Instead, we wish to excise any old given for an IP when adding a
-new one.
+When we are checking the last ?x occurrence, we guess its type to be a fresh
+unification variable alpha and emit an (IP "x" alpha) constraint. But the given
+(?x :: Int) has been translated to an IP "x" Int constraint, which has a
+functional dependency from the name to the type. So if that (?x::Int) is still
+in the inert set, we'd get a fundep interaction that tells us that alpha ~ Int,
+and we get a type error. This is bad. The "replacement" semantics stops this
+happening.
+
+Example 2:
+
+f :: (?x :: Char) => Char
+f = let ?x = 'a' in ?x
+
+The "let ?x = ..." generates an implication constraint of the form:
+
+?x :: Char => ?x :: Char
+
+Furthermore, the signature for `f` also generates an implication
+constraint, so we end up with the following nested implication:
+
+?x :: Char => (?x :: Char => ?x :: Char)
+
+Note that the wanted (?x :: Char) constraint may be solved in two incompatible
+ways: either by using the parameter from the signature, or by using the local
+definition. Our intention is that the local definition should "shadow" the
+parameter of the signature. The "replacement" semantics for implicit parameters
+does this.
+
+Example 3:
+
+Similarly, consider
+ f :: (?x::a) => Bool -> a
+
+ g v = let ?x::Int = 3
+ in (f v, let ?x::Bool = True in f v)
+
+This should probably be well typed, with
+ g :: Bool -> (Int, Bool)
+
+So the inner binding for ?x::Bool *overrides* the outer one.
+
+See ticket #17104 for a rather tricky example of this overriding
+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
+
+Both of these are actually wrong: when we try to use either one,
+we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
+which would lead to an error.
+
+I can think of two ways to fix this:
+
+ 1. Simply disallow multiple constraints for the same implicit
+ parameter---this is never useful, and it can be detected completely
+ syntactically.
+
+ 2. Move the shadowing machinery to the location where we nest
+ implications, and add some code here that will produce an
+ error if we get multiple givens for the same implicit parameter.
-}
+
{- ******************************************************************************
* *
interactDict
@@ -510,12 +577,6 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys
; updInertCans (updDicts $ delDict dict_w)
; continueWith () } } }
-{-
- | cls `hasKey` ipClassKey
- , isGiven ev_w
- = interactGivenIP inerts dict_w
--}
-
| otherwise
= continueWith ()
@@ -620,100 +681,6 @@ shortCutSolver dflags ev_w ev_i
Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty
| otherwise = mzero
-{-
-**********************************************************************
-* *
- Implicit parameters
-* *
-**********************************************************************
--}
-
-{-
-interactGivenIP :: InertCans -> DictCt -> TcS (StopOrContinue ())
--- Work item is Given (?x:ty)
--- See Note [Shadowing of Implicit Parameters]
-interactGivenIP inerts workItem@(DictCt { di_ev = ev, di_cls = cls
- , di_tys = tys })
- = do { updInertCans $ \cans -> cans { inert_dicts = addDict workItem filtered_dicts }
- ; stopWith ev "Given IP" }
- where
- dicts = inert_dicts inerts
- ip_dicts = findDictsByClass dicts cls
- other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
- filtered_dicts = addDictsByClass dicts cls other_ip_dicts
-
- ip_str = case tys of
- ip_str:_ -> ip_str
- [] -> pprPanic "interactGivenIP" (ppr workItem)
-
- -- Pick out any Given constraints for the same implicit parameter
- is_this_ip (DictCt { di_ev = ev, di_tys = ip_str':_ })
- = isGiven ev && ip_str `tcEqType` ip_str'
- is_this_ip _ = False
--}
-{- Note [Shadowing of Implicit Parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following example:
-
-f :: (?x :: Char) => Char
-f = let ?x = 'a' in ?x
-
-The "let ?x = ..." generates an implication constraint of the form:
-
-?x :: Char => ?x :: Char
-
-Furthermore, the signature for `f` also generates an implication
-constraint, so we end up with the following nested implication:
-
-?x :: Char => (?x :: Char => ?x :: Char)
-
-Note that the wanted (?x :: Char) constraint may be solved in
-two incompatible ways: either by using the parameter from the
-signature, or by using the local definition. Our intention is
-that the local definition should "shadow" the parameter of the
-signature, and we implement this as follows: when we add a new
-*given* implicit parameter to the inert set, it replaces any existing
-givens for the same implicit parameter.
-
-Similarly, consider
- f :: (?x::a) => Bool -> a
-
- g v = let ?x::Int = 3
- in (f v, let ?x::Bool = True in f v)
-
-This should probably be well typed, with
- g :: Bool -> (Int, Bool)
-
-So the inner binding for ?x::Bool *overrides* the outer one.
-
-See ticket #17104 for a rather tricky example of this overriding
-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
-
-Both of these are actually wrong: when we try to use either one,
-we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
-which would lead to an error.
-
-I can think of two ways to fix this:
-
- 1. Simply disallow multiple constraints for the same implicit
- parameter---this is never useful, and it can be detected completely
- syntactically.
-
- 2. Move the shadowing machinery to the location where we nest
- implications, and add some code here that will produce an
- error if we get multiple givens for the same implicit parameter.
--}
-
{- *******************************************************************
* *
Top-level reaction for class constraints (CDictCan)
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -62,17 +62,13 @@ tryInertIrreds irred
try_inert_irreds :: InertCans -> IrredCt -> TcS (StopOrContinue ())
try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
- | isInsolubleReason reason
- -- For insolubles, don't allow the constraint to be dropped
- -- which can happen with solveOneFromTheOther, so that
- -- we get distinct error messages with -fdefer-type-errors
- = continueWith ()
-
| let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
, ((irred_i, swap) : _rest) <- bagToList matching_irreds
-- See Note [Multiple matching irreds]
, let ev_i = irredCtEvidence irred_i
ct_i = CIrredCan irred_i
+ , not (isInsolubleReason reason && isWanted ev_i && isWanted ev_w)
+ -- See Note [Insoluble irreds]
= do { traceTcS "iteractIrred" $
vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
, text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
@@ -106,6 +102,16 @@ matching irreds in the inert set. When another irred comes along that we have
not yet labeled insoluble, we can find multiple matches. These multiple matches
cause no harm, but it would be wrong to ASSERT that they aren't there (as we
once had done). This problem can be tickled by typecheck/should_compile/holes.
+
+Note [Insoluble irreds]
+~~~~~~~~~~~~~~~~~~~~~~~
+For insoluble Wanteds, don't allow a duplicate Wanted to be dropped which
+can happen with solveOneFromTheOther, so that we get distinct error messages
+with -fdefer-type-errors
+
+However we do allow an insoluble constraint to be solved from an insoluble
+Given. This might seem a little odd, but it's very much a corner case, and
+it helps in tests bkpfail24.run, T15450, GivenForallLoop, T20189, T8392a.
-}
{- *********************************************************************
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f72a67cc8d88293a2b6e11103a6f37dffd331974
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f72a67cc8d88293a2b6e11103a6f37dffd331974
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230515/1c3dd7a3/attachment-0001.html>
More information about the ghc-commits
mailing list