Opened 2 years ago

Closed 22 months 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 2 years ago by thomie

Cc: gridaphobe added

f3 doesn't produce an error which makes me think it's related to CallStack handling.

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.

comment:2 Changed 2 years ago by nitromaster101

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 2 years ago by gridaphobe

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 2 years ago by gridaphobe

Owner: set to gridaphobe

comment:5 Changed 2 years ago by simonpj

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 2 years ago by gridaphobe

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 2 years ago by gridaphobe

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 2 years ago by simonpj

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 2 years ago by gridaphobe

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 2 years ago by simonpj

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 at rhs_tclvl) we don't want to quantify over CallStack constraints; instead we want to discharge (solve) them. After getting the constraints back from approximateWC, we can simply solve any un-solved CallStack constraints.

Does that help? I should have though of this first.

comment:11 Changed 2 years ago by gridaphobe

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 2 years ago by simonpj

Yes, making it part of defaulting sounds just right! Can you try that?

Simion

comment:13 Changed 2 years ago by simonpj

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 for CallStack constraints, where you push on the call site (i.e. do what the solver currently does, in isCallStackIP
  • 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 with EmptyStack

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, and IPOccOrigin (this is actually true already; see IPCallStackIP.
  • The only way to solve an OccurrenceOf call-stack constraint is by pushing on the call item, and producing a new wanted IPOccOrigin call-stack constraint
  • Solve wanted IPOccOrigin call-stack constraints as above, from each other, from givens, or by defaulting.

comment:14 Changed 2 years ago by gridaphobe

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 2 years ago by simonpj

(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 23 months ago by gridaphobe

Status: newpatch

comment:17 Changed 23 months ago by bgamari

Milestone: 8.0.1
Priority: normalhighest

comment:18 Changed 22 months ago by Ben Gamari <ben@…>

In 3ec8288/ghc:

Rework the Implicit CallStack solver to handle local lets.

We can't just solve CallStack constraints indiscriminately when they
occur in the RHS of a let-binder. The top-level given CallStack (if
any) will not be in scope, so I've re-worked the CallStack solver as
follows:

1. CallStacks are treated like regular IPs unless one of the following
   two rules apply.

2. In a function call, we push the call-site onto a NEW wanted
   CallStack, which GHC will solve as a regular IP (either directly from a
   given, or by quantifying over it in a local let).

3. If, after the constraint solver is done, any wanted CallStacks
   remain, we default them to the empty CallStack. This rule exists mainly
   to clean up after rule 2 in a top-level binder with no given CallStack.

In rule (2) we have to be careful to emit the new wanted with an
IPOccOrigin instead of an OccurrenceOf origin, so rule (2) doesn't fire
again. This is a bit shady but I've updated the Note to explain the
trick.

Test Plan: validate

Reviewers: simonpj, austin, bgamari, hvr

Reviewed By: simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1422

GHC Trac Issues: #10845

comment:19 Changed 22 months ago by bgamari

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.