New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improved Type Error Messages #156

Open
wants to merge 72 commits into
base: master
from

Conversation

Projects
None yet
@NadineTheBean

NadineTheBean commented Jul 20, 2018

Rendered

NadineTheBean added some commits Jul 6, 2018

@AntC2

This comment has been minimized.

AntC2 commented Jul 20, 2018

this can go the path of a regular GHC code improvement.

Thanks @nomeata, where in that path would we get feedback from people who read the messages (and are confused by them) as opposed to those who write the messages (who are presumably less confused)?

I agree (some) messages need overhaul -- although in general GHC's messages these days do a pretty good job. I strongly dislike several of the proposals here:

  • Putting the tags in [ ] is terrible: they look like list constructors.
  • in the underlined code below doesn't seem less wordy than In the ... phrases.
  • I'm not particularly in love with those In the ... phrases, but it is essential for GHC to narrowly point out which sub-term it's having trouble with. The proposal includes only toy examples, where the location of the problem is obvious. It needs some examples where the equation or declaration is spread over (say) a dozen lines.

Remember that any compiler messages are really a 'best guess'. All the compiler can see is an inconsistency, it doesn't know whether some earlier declaration is right, so this code is wrong vs. this code is right, the declaration was wrong.

This proposal doesn't address what is for me (as a casual Haskeller) the most exasperating about GHC's messages: I made a simple typo; GHC thinks I was trying to write some pointy-headed type-in-type higher-kinded doo-hickey. Try:

x = length (3, 2, 1)

I get three messages of which the first complains about something called Foldable. The other two messages are much longer, something about Ambiguous type variable. The only variable I can see in the code is x.

If you want examples of clear error messages, try that in Hugs.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Jul 20, 2018

Thanks @nomeata, where in that path would we get feedback from people who read the messages (and are confused by them) as opposed to those who write the messages (who are presumably less confused)?

Beat the drum on the various mailing lists, twitter, reddit, and ask people to weigh into the discussion, I guess.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jul 21, 2018

I encouraged my student to post here because I've found the quality of feedback and engagement to be very high. In the past, when I've sought feedback from mailing lists, I've either gotten nothing/very little or started threads that quickly went off subject.

You're right, @nomeata, that this is out of scope -- the proposal even says so. Nevertheless, I'm hoping that we can get active feedback here before this is fully implemented and merged and everyone complains.

@AntC2 is also right, in my opinion, that it would be more beneficial to fix the more complex error messages. But we have to start somewhere.

This proposal asks, essentially, for feedback about 4 design choices:

  1. Should we drop the "In the ..." lines? To me, these are subsumed by the caret diagnostics at the bottom of the messages these days.

  2. Should we start using tags (like [E] and [A]) in messages? I like these because they nicely separate the boring boilerplate from the part that varies in each error. They also will work well with tool integration. (Of course, there are even better ways to do tool integration, but we're not there yet.)

  3. Should we aim to remove technical terms from errors? I'm thinking of "occurs check", "untouchable variable", and "skolem" here, perhaps among others. This one is a harder call (technical terms have precise meanings and may be easier to search for), but I'm generally in favor of this change.

  4. Should GHC ever refer to itself as "I"? Now that GHC's brain explode any more, this would be new territory. I think it makes Haskell seem friendlier. You might find it creepy.

So, what do we think?

@gbaz

This comment has been minimized.

gbaz commented Jul 21, 2018

  1. I agree with dropping "In the ..." lines.

  2. the tags are fine, but I would like to change "Expected type [E] but the underlined code below has type [A]" to "Expected type [E] but the underlined code below has actual type [A]" to make clear why "A" is used.

  3. I thought we'd already eliminated all uses of "skolem" (which is also nonstandard technically, but common jargon among anyone who's tried to write nontrivial type inference). I would consider any remaining uses of "skolem" to certainly be bugs. I don't know how to rewrite away from "untouchable" and "rigid" as well without making things too vague. However, I think any technical terms used should be described and defined explicitly in the ghc manual, ideally with a (sub)entry in the ToC. That way at least users can find them!

Further on the specific suggestion in example 6, I think important information is thrown away. In particular, "cannot construct the infinite kind: k0 ~ k0 -> *" is pretty helpful in showing how the unification would create an infinite type, which is what induces the error. Additionally, and this touches on 4, we can write "Type checking cannot" instead of "I cannot" which I think is clearer and no less friendly. Further, I also think the pattern is to have fixed text for the first line of error message to help automated tooling, which the proposed message still doesn't satisfy.

I would suggest:

* Type checking got stuck because because a kind was inferred to be infinite.
* The underlined code has infinite kind [A]
  [A] k0 ~ k0 -> * 
@AntC2

This comment has been minimized.

AntC2 commented Jul 21, 2018

I agree with @goldfirere this is probably the best venue to get feedback from those who more read than write compiler messages. (I have similar experience from mailing lists, which is sad commentary, but for another venue ...)

  1. Should we start using tags like ([E] and [A]) in messages?

I'm neutral on the idea of using tags; strongly against putting them in square brackets, because they look like list types -- especially with the word type right beside them, and because currently you might well see a list type. Perhaps:

  • Angle brackets, as in BNF or in HTML tags <E>, <A>.

  • Words, then we can accomodate @gbaz's point re actual

      * Couldn't match expected type with actual type
        Expected type: String
          Actual type: Bool
    

Should GHC express a personality in its messages? The Couldn't match omits who/what it is doing the matching. GHC panic sounds acceptably animate. But yes I do find "I" over the limit: sounds like some marketing/promotion trying to make 'friends' with me.

Avoiding technical terms is certainly valuable. (But that's down to individual messages rather than a general overhaul?) As @gbaz points out, "untouchable" and "rigid" are particularly ornery. I just know them as that error I don't understand but do know how to fix. (There's heaps of questions on StackOverflow about "untouchable"/"rigid"; perhaps we can steal some words from answers there?)

@int-index

This comment has been minimized.

Contributor

int-index commented Jul 21, 2018

I dislike the [A] and [E] tags.

I like proper English words as @AntC2 suggests:

 * Couldn't match expected type with actual type
    Expected type: String
      Actual type: Bool

I even think the "Couldn't match expected type with actual type" part of the message is redundant. Words "expected" and "actual" are clear enough. So we can simply have

 * Expected type: String
     Actual type: Bool

I like shorter error messages: sometimes GHC reports too much and I have to scroll.

@int-index

This comment has been minimized.

Contributor

int-index commented Jul 21, 2018

As to the tooling motivation, I've had enough with tools trying to parse messages intended for humans.

Parsing is the worst, and error messages don't have a formal grammar (and shouldn't have!)

Whoever wants good tooling should stop messing around and start adding JSON error message output format.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Jul 21, 2018

I agree that caret positions subsume the In... stuff, and welcome shorter, more concise error messages when it does not lose important information

@mitchellwrosen

This comment has been minimized.

mitchellwrosen commented Jul 21, 2018

FYI, Elm has a similar syntax and has put a lot of time into making nice error messages. We could get inspiration from there. Here's what it outputs for example1:

-- TYPE MISMATCH ------------------------------------------------------ Main.elm

The definition of `example1` does not match its type annotation.

1| example1 : String -> String
2|>example1 xs = True

The type annotation for `example1` says it always returns:

    String

But the returned value (shown above) is a:

    Bool
@mitchellwrosen

This comment has been minimized.

mitchellwrosen commented Jul 21, 2018

What I like about this particular error message: It makes no mention of expected / actual, which requires me to think from the perspective of the compiler. I still have some trouble with this, and I much prefer the above, which just tells me what the type annotation is (expected) and what the value's type is (actual). It's wordy, but meaningful to my human brain

@mitchellwrosen

This comment has been minimized.

mitchellwrosen commented Jul 21, 2018

Here's an example of type inference kicking in, and again no mention of expected / actual:

The right side of (++) is causing a type mismatch.

1|            "Hello" ++ True
                         ^^^^
(++) is expecting the right side to be a:

    String

But the right side is:

    Bool

Hint: With operators like (++) I always check the left side first. If it seems
fine, I assume it is correct and check the right side. So the problem may be in
how the left and right arguments interact.
@mitchellwrosen

This comment has been minimized.

mitchellwrosen commented Jul 21, 2018

@NadineTheBean, does your work cover type holes as well? I'd love to see some improvements here :)

hylo.hs:93:22: error:
    • Found hole: _ :: r
      Where: ‘r’ is a rigid type variable bound by
               the inferred type of f :: [a1] -> ListF a1 r
               at hylo.hs:(92,3)-(93,22)
    • In the second argument of ‘ConsF’, namely ‘_’
      In the expression: ConsF x _
      In an equation for ‘f’: f (x : xs) = ConsF x _
    • Relevant bindings include
        xs :: [a1] (bound at hylo.hs:93:8)
        x :: a1 (bound at hylo.hs:93:6)
        f :: [a1] -> ListF a1 r (bound at hylo.hs:92:3)
        g :: forall t. t (bound at hylo.hs:95:3)
        rev' :: [a] -> b (bound at hylo.hs:90:1)
      Valid substitutions include
        undefined :: forall (a :: TYPE r).
                     GHC.Stack.Types.HasCallStack =>
                     a
          (imported from ‘Prelude’ at hylo.hs:1:1
           (and originally defined in ‘GHC.Err’))
   |
93 |   f (x:xs) = ConsF x _
   |                      ^

I feel this can be simplified to something like:

hylo.hs:93:22: error:
    • Found hole

        _ :: r

    • Relevant bindings include

        xs :: [a1]
        x :: a1
        f :: [a1] -> ListF a1 r
        g :: forall t. t
        rev' :: [a] -> b

    • Valid substitutions include
        
        undefined :: forall (a :: TYPE r).
                     GHC.Stack.Types.HasCallStack =>
                     a
   |
93 |   f (x:xs) = ConsF x _
   |                      ^
@tejon

This comment has been minimized.

tejon commented Jul 22, 2018

Count me among those who have been confused by "expected" and "actual." For example, when I'm stuck writing code that needs a type signature for disambiguation and I get that signature wrong, the fact that my wrong signature is the "expected" type throws me off every time.

Elm's errors are perhaps more verbose than I'd prefer, but they're very clear.

@int-index

This comment has been minimized.

Contributor

int-index commented Jul 22, 2018

and I get that signature wrong, the fact that my wrong signature is the "expected" type throws me off every time.

@tejon Interesting. Why? For me it's clear: when I write a type signarute, I tell the compiler to expect a term to have that type. Regardless of expectations, there's the actual type which it infers. Both of these types could be correct or incorrect. I find it all very intuitive and never had a problem even as a beginner.

Could you please share your thinking process? Why are these words confusing to you? Can you think of better ones?

Here's one idea: perhaps it would be more clear with words like "specified" and "inferred"? They sound a bit more technical, though.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Jul 22, 2018

I too ignore what GHC is labeling as expected and as actual, and try to make sense of it otherwise... so I would probably benefit from a different wording.

@LeanderK

This comment has been minimized.

LeanderK commented Jul 22, 2018

I recently wrote some code where it was easy to construct infinite types and I happened to me a few times. I remember that I was very frustrated with GHCs error because I couldn't figure out which part of the code was responsible for the infinite type from the error message. I can't give you example unfortunately.

@JoannaSharrad

This comment has been minimized.

JoannaSharrad commented Jul 22, 2018

I can't give you example unfortunately.

I believe that this is one of the issues with reviewing type errors. I am currently working on type errors for my PhD and trying to gather "real-life" examples is difficult as most do not keep to share or even push to github when a type error happens, when you do get examples you do not get the "feel" behind why it was difficult to solve, just that it was not understandable. I feel that having such a collection that contained these insights would be beneficial in seeing which errors are most problematic, however, understand that they would also be hard (near impossible) to collect!

@tejon

This comment has been minimized.

tejon commented Jul 22, 2018

For me it's clear: when I write a type signarute, I tell the compiler to expect a term to have that type. Regardless of expectations, there's the actual type which it infers.

That's exactly it: as @mitchellwrosen said, this error is from the compiler's perspective. To truly understand it, I have to shift to that perspective. The thing is, in the vast majority of cases, I don't really have to understand it. My brain can take a shortcut, applying these same terms at a code level: the "expected" type is one that a function expected, and the "actual" type is the one that I provided to a function, and this carries a whole set of implications about where to look for the root cause of error. And that heuristic does not include "bad type signature" because it's just too uncommon to make it into my first-pass debugging habits.

Yes, I can shift into "think like the compiler" mode and figure it out. But my understanding at that level is abstract. I've never written a compiler; I learned programming from the other end, starting as a hobbyist. The transition has non-trivial cost, I work slower at that level, and most of the time I don't need to do so to resolve this error. In fact, most of the time I can just parse it structurally and not really read the keywords at all, which is vastly more efficient. The confusion and frustration happens in the period between that heuristic failing, and me remembering that it's just a heuristic and shifting gears.

Changing terminology to something that doesn't make as much sense outside the compiler mindset probably would help (and this isn't the first time I've thought about it). The question is whether there's any terminology that is unambiguously compiler-centric and always correct. Replacing "actual" with "inferred" is the best thing that's come to mind so far, but I'm not sure it's the right term in every case? Consider:

foo :: Int
foo = 7
bar :: Bool -> Bool
bar x = foo && x

In bar, is it correct for the error to say foo's type is inferred as Int? It's very clearly specified in foo's definition. Genuine question, I just don't know -- which points to potential confusion for others, too, even if it is correct. On the other hand, this is soundly in the "learn it once" camp.

Other remappings I've thought of:

  • "expected" -> "required," "requested" or "specified"
  • "actual" -> "discovered"

I doubt "required/requested" or "discovered" would help, since they also map easily to function-level thought. "Specified" is on the line there, and I'm not sure its meaning is clear (or correct) enough in any case.

All told, if nobody with more expertise sees an issue with "inferred" instead of "actual," I think I'd recommend that change at minimum. But I should emphasize that this is not a replacement for thinking more about Elm's errors as a directional motivation.

Edit: @int-index In the course of typing this I completely forgot about your last paragraph, where you also came up with "specified" and "inferred." As I mentioned, this is not the first time I've thought about exactly this topic, and those terms were already in my head prior; point being, we landed on them independently. That does seem like a point in favor!

@simonmar

This comment has been minimized.

simonmar commented Jul 23, 2018

I agree with leaving out the redundant "In the .. " context messages. However, the proposal omits the useful Couldn't match type X with Y part of the message, which helps to narrow down exactly which part of the types didn't match. e.g.

<interactive>:7:111: error:
    • Couldn't match type ‘Char’ with ‘Bool’
      Expected type: (Bool, Char, Bool, Char, Bool, Char)
        Actual type: (Bool, Char, Bool, Char, Char, Bool)
    • In the first argument of ‘f’, namely ‘x’
      In the expression: f x
      In the expression:
        let
          f (a, b, c, d, e, f) = if e then ... else ...
          x = (True, 'a', False, 'b', 'c', True)
        in f x

In this case the compiler is telling us which part of the unification failed. If the expected and actual types are large and complex, then figuring out which part didn't match can sometimes be really hard.

Now, perhaps the current formulation also isn't ideal, it would be a lot easier if the compiler underlined the offending portions of the types, or rendered them in a different colour or something. But I don't think we should discard this information. e.g.

<interactive>:7:111: error:
    • Type mismatch
      Expected type: (Bool, Char, Bool, Char, Bool, Char)
                                              ^^^^  ^^^^
        Actual type: (Bool, Char, Bool, Char, Char, Bool)
                                              ^^^^  ^^^^

In fact there might be a complicated edit between the two types, so we might have multiple parts underlined. Colours would make this a lot easier to comprehend.

@NadineTheBean

This comment has been minimized.

NadineTheBean commented Jul 24, 2018

Thank you for the feedback so far everyone, I really appreciate it! :)

  • @mitchellwrosen Yes, this change would affect type holes, but it would only shorten the message by removing the "In the..." statements. I don't plan on touching the rigid type variable/relevant binding statements for now, although I believe that these could be improved in the future as well. As for the Elm syntax, I think that it's wonderfully clear, but I agree with @tejon that the messages are a bit too verbose.

  • @tejon @int-index Although they make sense to me, I did consider that the "expected" and "actual" terms cause additional confusion for many users, and have been studying messages from other languages in search of replacements. I think "specified" and "inferred" are too technical and would cause a lot more confusion than "expected" and "actual" (at least for beginners.) Another idea would be to borrow Java's terms, "required" and "found". I like this, but I think pairing "expected" with "found" could be even better because they sort of imply that you need to think about it from the compiler's perspective. Any thoughts on this?

@alanz

This comment has been minimized.

alanz commented Jul 24, 2018

I think the terms expected and actual are too loaded, many times the mismatch is caused by a bug in the thing that the compiler regards as setting the expected value.

So perhaps some sort of neutral terminology would be better, using A and B instead of E and A.

@int-index

This comment has been minimized.

Contributor

int-index commented Jul 24, 2018

What about

Could not unify types
    (Bool, Char, Bool, Char, Bool, Char)
                       ^^^^  ^^^^
and
    (Bool, Char, Bool, Bool, Char, Char)
                       ^^^^  ^^^^
@tejon

This comment has been minimized.

tejon commented Jul 24, 2018

I like found. It initially strikes me as a verb; actual is unambiguously an adjective, implying expected is also. Reading these labels as verbs shifts the tone from denotational to imperative, which feels like it could be enough to shake me out of pure-code reverie. :)

Bonus option: pair found with wanted?

@mgsloan

This comment has been minimized.

mgsloan commented Jul 29, 2018

I think I like expected better than wanted. But found seems much better than actual. How about:

    * Expected type ‘String’, but found type ‘Bool’
    |
 57 | example1 xs = True
    |               ^^^^

If the types are long, use [E] / [F], I like that:

    * Expected type [E], but found type [F]
      [E] Proxy "This is a rather large expected type, don't you think?"
      [F] Proxy "One can be small"  
    |
 57 | example1 xs = True
    |               ^^^^

Not sure if the prettyprinter supports alternate forms when there's a horizontal overflow, but this is what you'd get in that case.

@tejon

This comment has been minimized.

tejon commented Jul 29, 2018

I can definitely get on board with that.

@ChShersh

This comment has been minimized.

ChShersh commented Aug 7, 2018

@mgsloan Even if found might be a better word than actual I don't like having first letters F and E. These two letters look very similar. And you might have hard times in attempts to recognise where is F and where is A on different terminals (with different colors or you might be sleepy or tired). Eventually you will just remember that found is on second line. And in that case having [E] and [F] letters won't really help you, so they're useless. Maybe we can use another words? Like:

  • Expected/Actual (original)
  • Specified/Inferred (proposed by @int-index)
  • Wanted/Found (proposed by @tejon)
  • Goal/Found
  • Need/Have (bonus points for same number of letters)
  • Any combination of the above or something else.
@ChShersh

This comment has been minimized.

ChShersh commented Aug 7, 2018

My 2 cents into this proposal. If we have code like this:

example2 :: (Bool,Char,Bool,Char,Bool,Char) -> (Bool,Char,Bool,Bool,Char,Char)
example2 (a,b,c,d,e,f) = (a,b,c,d,e,f)

then it would be cool to have error message like this (inspired by multiple sources):

   Could not unify expected type [E]
      [E] (Bool, Char, Bool, Char, Bool, Char)
                             ^^^^  ^^^^
    and actual type [A]
      [A] (Bool, Char, Bool, Bool, Char, Char)
                             ^^^^  ^^^^
    in the code below:
      C:\Users\Example\Documents\Examples.hs:44:10-15
   ┏━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
43  example2 :: (Bool,Char,Bool,Char,Bool,Char) -> (Bool,Char,Bool,Bool,Char,Char)
                                                                   ^^^^ ^^^^
44  example2 (a,b,c,d,e,f) = (a,b,c,d,e,f)
                                     ┗━ e :: [E] Char
                                             [A] Bool
                                    
                                    ┗━ d :: [E] Bool
                                            [A] Char

@bravit bravit added the Proposal label Nov 11, 2018

@bravit bravit removed the Proposal label Dec 3, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment