Opened 3 years ago
Closed 3 years ago
#10845 closed bug (fixed)
Incorrect behavior when let binding implicit CallStack object
Reported by: | nitromaster101 | Owned by: | gridaphobe |
---|---|---|---|
Priority: | highest | Milestone: | 8.0.1 |
Component: | Compiler | Version: | 7.11 |
Keywords: | Cc: | gridaphobe | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #10846 | Differential Rev(s): | Phab:D1422 |
Wiki Page: |
Description
I'm trying out ghc HEAD at 062feee4e7408ad5b9d882e5fed2c700e337db72.
{-# LANGUAGE ImplicitParams #-} import GHC.Types f :: (?loc :: CallStack) => Int f = let y = length $ getCallStack ?loc in if y < 2 then 3 else 4 f2 :: (?loc :: CallStack) => Int f2 = if (length $ getCallStack ?loc) < 2 then 3 else 4 f3 :: (?loc :: [Int]) => Int f3 = let y = length ?loc in if y < 2 then 3 else 4
produces:
[1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:5:6: warning: Redundant constraint: ?loc::CallStack In the type signature for: f :: (?loc::CallStack) => Int
f3 doesn't produce an error which makes me think it's related to CallStack handling. The warning seems accurate: the returned callstack only contains the entry at f.
Change History (19)
comment:1 Changed 3 years ago by
Cc: | gridaphobe added |
---|
comment:2 Changed 3 years ago by
There are two issues: since f3 doesn't produce any warnings, neither should f since the only difference is the type of ?loc.
If I add some callers to f and f2:
{-# LANGUAGE ImplicitParams #-} import GHC.Types f :: (?loc :: CallStack) => String f = let y = show $ map (srcLocStartLine . snd) $ getCallStack ?loc in y f2 :: (?loc :: CallStack) => String f2 = show $ map (srcLocStartLine . snd) $ getCallStack ?loc f_caller = f f2_caller = f2
We get the warning:
[1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:5:6: warning: Redundant constraint: ?loc::CallStack In the type signature for: f :: (?loc::CallStack) => String
And when we run them the call stack returned by f is wrong, it should have two entries (the line number for f_caller and f):
*> f_caller "[6]" *> f2_caller "[10,13]"
comment:3 Changed 3 years ago by
Hmm, it looks like the ?loc
constraint in f
is being solved in an environment that doesn't include the given ?loc
from the function's context. Very strange, and certainly incorrect.
Thanks for the report!
comment:4 Changed 3 years ago by
Owner: | set to gridaphobe |
---|
comment:5 Changed 3 years ago by
Eric, I see you've taken these implicit-call-stack tickets. Excellent, thank you. Please yell when you understand what is going on, and want to propose a solution.
Simon
comment:6 Changed 3 years ago by
Related Tickets: | → #10846 |
---|
Ok, the problem is that when we infer the type of a let-bound variable, we attempt to solve any constraints generated from the RHS without consulting the given constraints from the surrounding context. Specifically, TcSimplify.simplifyInfer
tries to solve the wanteds with no givens.
This is problematic for CallStacks because of the special rule that allows us to discharge a CallStack IP constraint without a given CallStack, by creating one out of thin air.
So in
f :: (?loc :: CallStack) => [(String, SrcLoc)] f = let y = getCallStack ?loc in y
the use of getCallStack
tells GHC that ?loc :: CallStack
, and GHC immediately discharges the IP constraint without seeing the CallStack given by f
's context, while in
f :: (?loc :: CallStack) => [(String, SrcLoc)] f = let y = ?loc in getCallStack y
we end up with a generic ?loc::t
constraint that GHC can't solve, until it emits an implication with f
's given constraints.
I can work around this by splitting off any IP wanteds at the beginning of simplifyInfer
and stitching them back onto the final implication constraint that simplifyInfer
emits, but I'm not sure if this is the right solution. I don't think it should affect regular IPs since we always infer an IP constraint in local binders, but I still need to validate my patch.
Also, I believe #10846 is closely related to this issue because PartialTypeSignatures
triggers a similar code path through TcBinds.tcPolyInfer
and TcSimplify.simplifyInfer
, causing us to lose sight of the given IP constraint.
comment:7 Changed 3 years ago by
Hrm, unfortunately splitting off the wanted IP constraints in simplifyInfer
doesn't work because we need them to infer a corresponding given. For example, in
f :: (?x :: Int) => Int f = let y = ?x in y
we want to infer y :: (?x :: Int) => Int
(according to the Note "Inheriting Implicit Parameters"). But with CallStack IPs,
f :: (?x :: CallStack) => [(String, SrcLoc)] f = let y = getCallStack ?x in y
we want to infer y :: [(String, SrcLoc)]
. We really don't want to infer a CallStack IP here because that would add an extra location to the stack.
comment:8 Changed 3 years ago by
There are several things going on here.
First, let's just note that none of this arises if we have MonoLocalBinds
, which is what happens if you have GADTs etc.
Second, we have this magic rule that CallStack
constraints can be spontaneously solved by the solver. This is an ad-hoc rule that means we don't gratuitously infer top-level types like f :: (?x :: CallStack) => blah
. But it should really only apply at top level. For nested let-bindings I think it'd be fine to abstract.
So in the "spontaneous solve" code in TcInteract.interactDict
we can make it conditional on the tc_lvl
being 3. (Sorry about the 3; I'm committing a new Note [TcLevel assignment]
in TcType
to explain. There should be a definition topImplicationTcLevel = 3
alongside topTcLevel = 1
.)
Third, I think that if MonoLocalBinds
is off, then we do want to generalise over CallStack
constraints, just like any other implicit parameter. Consider
f :: (?loc :: CallStack) => blah f x = let g y = ...error "foo".... in ...(g x) ... (g v) ...
Now, if g
fails, calling error
, surely you'd like to see which of g
's call sites was implicated? So we'd expect g
to get an inferred type
g :: (?loc :: CallStack) => something
Does it make a difference if g
has no arguments? Well, the monomorphism restriction says we won't quantify over any constraints, so yes, it makes a difference.
Fourth you seems to want to treat getCallStack
specially, which I am doubtful about. In the above example g
's RHS has a call to error
, but it should not behave any differently if it had a call to getCallStack
instead. The latter is just another ordinary function with a (?x :: CallStack)
constraint.
Bottom line: I think that all we need do is suppress the spontaneous-solve code for CallStack
if we are not at top level.
comment:9 Changed 3 years ago by
Ah, I wasn't suggesting to treat getCallStack
specially, it was just the simplest way to get GHC to instantiate the ?x's type with CallStack
in the RHS of the local let-binder, which is a key ingredient in this bug.
Suppressing the special case for CallStack
seems to get us part of the way, we defer solving the CallStack until we get a toplevel implication
Implic { TcLevel = 3 Skolems = No-eqs = False Status = Unsolved Given = $dIP_anO :: ?loc::CallStack Wanted = WC {wc_impl = Implic { TcLevel = 5 Skolems = No-eqs = False Status = Unsolved Given = Wanted = WC {wc_simple = [W] $dIP_anT :: ?loc::CallStack (CNonCanonical)} Binds = EvBindsVar<anU> the inferred type of y_anr :: t_anQ[tau:5] }} Binds = EvBindsVar<anY> the type signature for: f :: (?loc::CallStack) => [(String, SrcLoc)] }
Unfortunately the wanted in this implication is itself an implication, so GHC raises the TcLevel again when it enters the nested implication and our special case remains suppressed.
I find it a bit strange though that the nested implication has no givens. Why emit an implication with no givens when we could just emit a simple wanted?
comment:10 Changed 3 years ago by
Ah, yes, you are correct. (You can have a nested implication with skolems but no givens; that's important. Here there are no skolems either, and it'd take a little longer to explain why.)
Rather than conditionally suppressing the no-given solver for CallStack
, a better way is probably this.
- Remove the auto-solve for
CallStack
(with no givens) altogether.
- Instead, look at
TcSimplify.simplifyInfer
. It figures out what to quantify over. At top level (look atrhs_tclvl
) we don't want to quantify overCallStack
constraints; instead we want to discharge (solve) them. After getting the constraints back fromapproximateWC
, we can simply solve any un-solvedCallStack
constraints.
Does that help? I should have though of this first.
comment:11 Changed 3 years ago by
Alas, we can't simply remove the no-given solver for CallStacks, what about
f :: CallStack f = ?callStack
Here we're given a type signature, so we won't pass through simplifyInfer
. In general, I'm pretty sure we need the no-given solver for CallStacks at levels 1 and 3.
Unfortunately that doesn't cut it either, consider our friend fail
class Monad m where fail :: String -> m a fail s = error s
fail
gives rise to an implication
Implic { TcLevel = 3 Skolems = (m_anr[ssk] :: * -> *) No-eqs = False Status = Unsolved Given = $dMonad_aon :: T10845.Monad m_anr[ssk] Wanted = WC {wc_impl = Implic { TcLevel = 5 Skolems = a_aop[sk] No-eqs = False Status = Unsolved Given = Wanted = WC {wc_simple = [W] $dIP_aot :: ?callStack::CallStack (CNonCanonical)} Binds = EvBindsVar<aov> the type signature for: T10845.fail :: String -> m_anr[ssk] a_aop[sk] }} Binds = EvBindsVar<aow> the class declaration for ‘T10845.Monad’ }
which has the CallStack wanted stuck back at level 5! Ugh..
Perhaps what we really want is to move the no-given solver to simplifyTop
, not simplifyInfer
. I see that simplifyTop
handles type-class defaulting, which feels similar in spirit to the no-given solver (ie we're defaulting the insoluble CallStacks to contain just the current source location).
comment:12 Changed 3 years ago by
Yes, making it part of defaulting sounds just right! Can you try that?
Simion
comment:13 Changed 3 years ago by
Differential Rev(s): | → Phab:D1422 |
---|
On D1422 you say: Sadly, it turns out we can't remove the no-given solver entirely. Consider
main = do putStrLn $ showCallStack ?loc putStrLn $ showCallStack ?loc
GHC treats the constraints arising from the two occurrences of ?loc as interchangeable (after all, they have the same type), and solves one from the other, giving us the incorrect output
% ./T10845 CallStack: ?loc, called at T10845.hs:33:36 in main:Main CallStack: ?loc, called at T10845.hs:33:36 in main:Main
(note that both CallStacks refer to the same location).
Good point! But there is a better way to solve this particular issue:
- In
Inst.instCallConstraints
, add a special case forCallStack
constraints, where you push on the call site (i.e. do what the solver currently does, inisCallStackIP
- Now any Wanted call-stack constraints encountered by the solver can be solved by equality from each other, or directly from a given. In fact this makes call-stack constraints behave even more like implicit-parameter constraints.
- Defaulting solves a
CallStack
constraint withEmptyStack
This is much simpler and more direct.
There is a wrinkle: what if the function being called had a type
like f :: c => T c -> Int
, and c
was subsequently inferred to
be IP "foo" CallStack
? So the fact that it's a call-stack constraint
isn't immediately obvious.
It's a pretty obscure problem but could be solved by NOT solving in
instCallConstraints
, but intead
- Have two kind of call-stack constraints, with origin
OccurrenceOf
, andIPOccOrigin
(this is actually true already; seeIPCallStackIP
.
- The only way to solve an
OccurrenceOf
call-stack constraint is by pushing on the call item, and producing a new wantedIPOccOrigin
call-stack constraint
- Solve wanted
IPOccOrigin
call-stack constraints as above, from each other, from givens, or by defaulting.
comment:14 Changed 3 years ago by
If I understand your suggestion correctly, this won't fix my example. Why? Because ?loc
creates an IPOccOrigin
constraint, which you suggest we should freely solve from other call-stack constraints (I take this to mean the usual form of solving an IP, ie we don't push on the stack). So the two ?loc
constraints would be consolidated to one, which we would default to the empty stack.
But perhaps this isn't so bad after all. My example was a bit of a red herring, what we really care about is that in
f :: (?stk :: CallStack) => .. main = print (f 0) >> print (f 1)
the two calls to f
are not consolidated to a single constraint. f x
gives rise to an OccurrenceOf
constraint, which you suggest we would solve by pushing on the stack and emitting an IPOccOrigin
constraint, so we would get the correct behavior here.
So, I think under your suggestion, we'll never see a ?loc
in the call-stack, but I think that's fine. (It always stuck me as a bit odd to have the root of the call-stack be an occurrence of an IP, rather than a function call)
comment:15 Changed 3 years ago by
(I think you are referring to my second version, post-wrinkle.) You are right. I was hi-jacking IPOccOrigin
to do "combine and default to empty stack". But yes, I think we can allow it not to add a location on its own behalf. If you wanted the current effect of ?loc
, you can always get the same effect by using
currentLoc :: ?loc :: Location => Location currentLoc = ?loc
We'd better document this carefully though.
Simon
comment:16 Changed 3 years ago by
Status: | new → patch |
---|
comment:17 Changed 3 years ago by
Milestone: | → 8.0.1 |
---|---|
Priority: | normal → highest |
comment:19 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
What is related to CallStack handling? What is the incorrect behavior? I'm sure it's obvious to you, but please mention it explicitly in the description. Thanks.