Generating better type-error messages is a hoary chestnut, but Herbert brought my attention to this thread on reddit, which has the following idea.
At the moment, from
module Foo where addThree = \x -> x + 3 :: Int y = addThree $ Just 5
we get this error:
Foo.hs:2:20 Couldn't match expected type `Int' with actual type `Maybe a0' In the return type of a call of `Just' In the second argument of `($)', namely `Just 5' In the expression: addThree $ Just 5
Maybe we could generate this instead
Foo.hs:2:20 inferred: "Just 5" has type "Maybe a0" expected: second argument of "($)" must have type "Int" in the expression: addThree $ Just 5
Trac metadata
Trac field
Value
Version
7.8.2
Type
Bug
TypeOfFailure
OtherFailure
Priority
normal
Resolution
Unresolved
Component
Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Edited
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Child items
0
Show closed items
No child items are currently assigned. Use child items to break down this issue into smaller parts.
Linked items
0
Link issues together to show that they're related or that one is blocking others.
Learn more.
I like this, and think the second set of output reads much, much better. Bonus points: use ANSI terminal colors to highlight some key words in the output, such as "Warning" or "Error" should they exist.
Here's an error that a noob making a subtle typo might get from GHC:
Prelude> map 1 [1..5]<interactive>:2:1: Could not deduce (Num (a0 -> b)) arising from the ambiguity check for ‛it’ from the context (Num (a -> b), Num a, Enum a) bound by the inferred type for ‛it’: (Num (a -> b), Num a, Enum a) => [b] at <interactive>:2:1-12 The type variable ‛a0’ is ambiguous When checking that ‛it’ has the inferred type ‛forall a b. (Num (a -> b), Num a, Enum a) => [b]’ Probable cause: the inferred type is ambiguous
I wholeheartedly agree that the information needs to be presented in a way that's easier to digest.
For what should be a really simple error, I really have to stare that down to understand what it's actually trying to say ...
Despite the very general ticket title, let’s not confalte multiple errors. The original ticket was a about a type mismatch (inferred vs. expected). The example by schlyer is about an ambiguous type in the GHCi prompt. Note that with some more instances added, map 1 [1..5] would type check!
This seems like a nice and easy ticket to handle by a newcomer.
The function to change is misMatchMsg in compiler/typecheck/TcErrors.hs.
Don't forget to update the expected test output. Use 'make accept', see Building/RunningTests/Updating. Please make sure you get all of them (grep for the old error message).
While I love the the proposal in the ticket, I feel that a purely textual change to the error message could be a great boon without changing a single line of code.
"Expected" versus "actual" don't really the nature of the problem. For example, what is the type of foo in the following
foo :: Intfoo = "Howdy!"
Is foo actually an Int, since that was declared? Did the compiler expect foo to be a String, since that's what we passed it? Or is foo actually a "String", since that's what it contained, but the compiler expected a Int, since that's what we told it would be contained?
Perhaps just changing
Couldn't match expected type 'Foo' with actual type 'Bar'
to
Couldn't match declared type 'Foo' against a value of type `Bar'
The error there would not be about the type of foo, though. It would be about the type of "Howdy!".
Foo.hs:4:7: Couldn't match expected type ‘Int’ with actual type ‘[Char]’ In the expression: "Howdy!" In an equation for ‘foo’: foo = "Howdy!"
The "actual type" is ... the actual type of the expression "Howdy!" that the compiler points out. The "expected type" is the type expected from the context, that is, the type the expression would have to have for the whole thing to type check. I know lots of people find this confusing but I have never been able to understand why...
I wonder if it would help at all to just reverse the order of the two, that is,
Couldn't match actual type ‘[Char]’ with expected type ‘Int’ In the expression: "Howdy!"
Presumably the programmer has a strong association between the expression and its (actual) type, and then can work out what "expected type" refers to by elimination.
I'm also not that attached to the phrase "expected type". We could be more explicit and say something like "type ‘Int’ expected from context". I think the phrase "actual type" is quite good, though.
The trouble with "declared type" is that it often isn't declared. Consider
not 'c'
The actual type of 'c' is Char, but the type expected by the context (the call of not) is Bool. But it'd be confusing to say that Bool was the "declared" type!
Switching the order as Reid suggests in ticket:9173#comment:107699 would be easy, and I can see that it might help. Do others like that?
I'd also be ok with saying "type expected by the context" instead of just "expected". That longer phrase would also suggest putting it second.
Foo.hs:4:7: Couldn't match expected type ‘Int’ with actual type ‘[Char]’ In the expression: "Howdy!" In an equation for ‘foo’: foo = "Howdy!"
This example reminded me that sometimes the phrase "In the expression" is confusing to me. It seems that the phrase *should* be "Of the expression". Using 'in' makes me expect that the error message is referring to some particular component of the expression, rather than the whole thing.
It's a small incongruence, but it's big enough to force me to stop thinking about code and start thinking about the possible meanings of the error message.
Switching the order as Reid suggests in ticket:9173#comment:107699 would be easy, and I can see that it might help. Do others like that?
I'd also be ok with saying "type expected by the context" instead of just "expected". That longer phrase would also suggest putting it second.
+1. E.g.:
foo.hs:1:11: Couldn't match actual type ‘Char’ with type expected by context, ‘Bool’ In the first argument of ‘not’, namely ‘'c'’ In the expression: not 'c' In an equation for ‘foo’: foo = not 'c'
(I recall now that "In the expression" is used because the message often *does* refer to a component of the whole expression. Still, I think it would be nice if it switched to "In the expression" when referring to the whole thing.)
Once D808 gets merged (could be today! but more likely in 2-3), printing out the expression that has the bad type will be much easier, as I've restructured how that information sloshes around internally. So that will be a viable improvement very soon.
The information needed in !TcErrors to address this ticket is now very much to hand, in the uo_thing field of a TypeEqOrigin. There is some refactoring to do to improve the plumbing, but it would now be easy for someone to take an honest stab at this ticket.
I guess that the patch mentioned above makes those bigger changes possible, but still.
For the wording change, I think adding "...from context" is universally desired. See my ticket:9173#comment:107778, and the one following it, for suggested text.
Incidentally, I dislike the eldest proposal (quoted in this comment) because it splits the necessary information over a couple lines, which is not so nice for integrating with vim's :make command. ;)
Replying to [[span(style=color: #FF0000, simonpj )]]\\
Hello simonpj,\\
I agree with rwbarton.
But instead of using the word "context" I prefer the use of the word "signature".\\
A signature is a description of each component of a definition of a function,
or in a more general way by talking about an expression.\\
A Type signature defined by the programmer takes precedence over the Type of the result of the calculated function.\\
We could write :
Type Int expected by signature.\\
or this sentence that is simple and sounds well\\
The Type of the result is not in accordance with the Type of the signature
Or with the Type write inside\\
The Type `[Char]` of the result is not in accordance with the Type `Int` of the signature
The word "context" is quite different.\\
It implies a greater scope in the code.
It would be the equivalent of a set.\\
But one thing must be noted.\\
This thing is not to write the signature of the function.\\
If I write\\
module Foo where addThree = \x -> x + 3 y = addThree $ Just 5
GHCi sayd\\
Prelude> :l foo.hs[1 of 1] Compiling Foo ( foo.hs, interpreted )foo.hs:2:22: error: * No instance for (Num (Maybe a0)) arising from a use of `+' * In the expression: x + 3 In the expression: \ x -> x + 3 In an equation for `addThree': addThree = \ x -> x + 3foo.hs:3:25: error: * Ambiguous type variable `a0' arising from the literal `5' prevents the constraint `(Num a0)' from being solved. Relevant bindings include y :: Maybe a0 (bound at foo.hs:3:5) Probable fix: use a type annotation to specify what `a0' should be. These potential instances exist: instance Num Integer -- Defined in `GHC.Num' instance Num Double -- Defined in `GHC.Float' instance Num Float -- Defined in `GHC.Float' ...plus two others (use -fprint-potential-instances to see them all) * In the first argument of `Just', namely `5' In the second argument of `($)', namely `Just 5' In the expression: addThree $ Just 5Failed, modules loaded: none.Prelude>
Here there is no Type signature in the context.\\
The sentence * No instance for (Num (Maybe a0)) arising from a use of +'` is
more explicit.\\
I hope this will help.
I would love to look into this, but it is unclear what the new message is supposed to be. Should we go with the suggestion of the original post, or one of the other rewording suggestions?
I agree with bgamari too.\\
Well, I glanced at the Oxford Dictionary. I have compared the words "context" and "signature".\\
Here is the definition of the word "context":\\
The circumstances that form the setting for an event, statement, or idea, and in terms of which it can be fully understood.\\
Examples:\\
‘the proposals need to be considered in the context of new European directives’\\
‘We are going to be able, within a European context, to be in a more positive position.’\\
‘This is down to his determination to place current events in a historical context.’\\
‘For new readers this can be an advantage, but they become disadvantages in contexts of closer study.’\\\\
Synonyms of the word context: circumstances, conditions, surroundings, factors, state of affairs\\
frame of reference, contextual relationship.\\
\\
Here is the definition of the word "signature":\\
A distinctive pattern, product, or characteristic by which someone or something can be identified.\\
Examples:\\
‘the chef produced the pâté that was his signature’\\
‘Changes in population size tend to leave recognizable signatures in the patterns of nucleotide diversity.’\\
‘This process, called intrinsic catalysis, has a characteristic signature in the exchange time measurements versus pH.’\\
‘Cells tugged in one direction sent biochemical signals in the opposite direction in the form of a signature pattern of fluorescent light.’\\\\
Obviously, the word signature has a more precise meaning, characterizing a
thing and the word context has a broader meaning.
I'm coming back about the solution provided by rwbarton.
This solution is not appropriate in the case below.
let y = [True, 'a']
What is the actual type? What is the expected type?\\
If I change the order of the values in the list like this:
let y = ['a', True]
What is the actual type? What is the expected type?\\\\
An obvious answer is The types must be identical in a list or The types are not equal
Here we see that there is no signature. If the signature had been y :: [Char]
The obvious answer is the one I have given in comment 23, and which is
The Type of the result is not in accordance with the Type of the signature
Or so I thought, but in fact there is: after stating the translation, the standard states that in [e1, ..., ek], "the types of e1 ... ek must all be the same". Is this normative, or just a (redundant) explanation?
I do think that compiler (error) messages should use wording from the standard. (So, looking up words in OED does not really help. The committee that wrote the standard already did this.)
I think the time is ripe for this ticket, and it shouldn't be hard. Here are the pieces:
Update TcErrors.mkExpectedActualMsg to print out the uo_thing field of the TypeEqOrigin passed in. For example, if we're reporting an actual of Maybe Int and an expected of Bool, then uo_thing might hold Just 5. This step can likely be done by changing msg1 of mkExpectedActualMsg.
Rip out the special treatment of kinds in mkExpectedActualMsg. Other than swapping out the word "kind" for "type", kinds and types should be treated the same. This special treatment is currently there solely to match pre-8.0 behavior. Doing this step should improve the error messages worsened by #14066 (closed) and fix, e.g., #14887 (closed). Concretely, this step is essentially to remove msg5 from mkExpectedActualMsg.
Those two steps, by themselves, would nail this ticket. But Simon and I think we can do better. Currently, the uo_thing of a TypeEqOrigin tracks the term (or type, during kind-checking) that has the "actual" type. (It's the Just 5 mentioned in step 1.) However, we can also track the aspect of the context that leads us to expect the "expected" type. For example, this string could be something like "required as the condition of an if" or "of the second argument of ($)" or "of the type used in a type signature". Here are example error messages:
Code: if 'x' then foo else bar
Type mismatch: `Char' /= `Bool' Actual: `Char' is the type of `'x'' Expected: `Bool` is the type required as the condition of an `if'
Code: not $ 'x'
Type mismatch: `Char' /= `Bool' Actual: `Char` is the type of `'x'' Expected: `Bool` is the type of the second argument of ($)
Code: foo :: Maybe
Kind mismatch: `* -> *' /= `*' Actual: `* -> *' is the kind of `Maybe' Expected: `*` is the kind of the type used in a type signature
Aren't these just lovely?
To do this:
Add an SDoc field to the Check constructor of an ExpType (in TcType). Then, in every mkCheckExpType, supply an appropriate message. Ideally, this message will not mention any types, because there will be no chance to zonk them later.
Add a new field uo_context to TypeEqOrigin (of type Maybe SDoc) that will get the doc from the Check. This seems like it will happen in TcUnify.tcSubTypeDS_NC_O, but perhaps in other places, too. It's worth checking every place we make a TypeEqOrigin.
Teach TcErrors.mkExpectedActualMsg to use this new info.
We could do steps 1-2 separately from 3-5, but given the very large number of error messages one would have to sweep through to do so, it seems best to common these changes up.
I was able to make some progress on this ticket (screenshot with new error messages: https://prnt.sc/ktm8u2).
I will keep working on 3-5. Shouldn't take long to finish this part!
Great stuff! I think it would be Really Helpful to write down a Note explaining how all the moving parts work. Then we can review that against your code. It always does my head in!
I was able to locate all the places where we make TypeEqOrigin. We do this with a help of a smart constructor mkCheckExpType. There are around 80-90 places (across 12 modules) where we use it. There is another function synKnownType that uses mkCheckExpType which has another 25 occurrences.
For now I just used dummy text everywhere to be able to compile it.
Here you can see more detailed search results for these functions:
I have already changed some of the messages where I was able to infer the context and come up with meaningful explanations. Here is a screenshot of examples from the ticket with new messages - https://prnt.sc/kycm4c, however, some places are tricky so I will probably need more time to spend on them.
Right now my plan is the following - I want to come up with all the test cases(programs) that would call all the code parts where we use the above mentioned functions. By doing that, I will slowly weed out all the dummy messages and replace with meaningful ones.
As suggested, I am collecting all the notes of my changes.
Perhaps, it is a good time to submit a patch to Phabricator? We could proceed with a discussion there and it would be much easier to discuss all the new messages (with line comments). By the way, If someone could code review and help with new messages - that would be greatly appreciated! Thank you.
I think it would be very helpful if you wrote a wiki page (on the Trac wiki) explaining (a) the problem you are trying to solve (being more specific than "better error messages"), and (b) how you are solving it.
Concerning (b) there are quite a few moving parts, and it really helps to explain how they work together. It may well be that we iterate the design a bit, and it's best to do that before you have invested a great deal of effort in it.
Thanks!
Alex Dchanged title from Better type error messages to Improve type mismatch error messages
changed title from Better type error messages to Improve type mismatch error messages
Nowadays, we would just have to tweak the pretty-printing of GHC-83865 error, maybe adding some new fields to MismatchMsg constructors.
The following patch is enough to start implementing Richard's suggestions in #9173 (comment 152647):
--- compiler/GHC/Tc/Errors/Ppr.hs+++compiler/GHC/Tc/Errors/Ppr.hs@@-4102,7+4102,8@@pprMismatchMsgctxt|isAtomicTyty1||isAtomicTyty2=-- Print with quotes-sep[textherald1<+>quotes(pprty1)+sep[text"Type mismatch:"<+>quotes(pprty1)<+>text"/="<+>quotes(pprty2)+,textherald1<+>quotes(pprty1),nestpadding$textherald2<+>quotes(pprty2)]
❯ cat Foo.hsmodule Foo where addThree = \x -> x + 3 :: Int y = addThree $ Just 5❯ ~/projects/ghc/master/_build/stage1/bin/ghc Foo.hs[1 of 1] Compiling Foo ( Foo.hs, Foo.o )Foo.hs:3:18: error: [GHC-83865] • Type mismatch: ‘Int’ /= ‘Maybe a0’ Couldn't match expected type ‘Int’ with actual type ‘Maybe a0’ • In the second argument of ‘($)’, namely ‘Just 5’ In the expression: addThree $ Just 5 In an equation for ‘y’: y = addThree $ Just 5 |3 | y = addThree $ Just 5 |
It would be great if there was. Error message generation is well separated from the rest of GHC so, although it is never simple to generate insightful messages, it's a task that can be worked on at least somewhat independently from the complexities of the typechecker.