Produce type errors after looking at whole applications

Currently, the type error messages we produce in case of function applications are rather dumb, in particular if arguments were ommited, added, swapped or not parenthized correctly. (Examples in the first comment below.)

In many cases a procedure like the following would be better: For a given application f a1 a2 a3, present the user with the (inferred) type of f, as well as the (expected) type f needs to have to be used with arguments a1 a2 a3. This way, only one type error will be reported per function application, instead of many, and comparing these two reported types will allow the user to spot the problem more easily.

(With „one application“ I mean e1 e2 e3 … en where e1 is not of that form.)

Furthermore, once we have these two types in our hands, we can look for common patterns, and give even more helpful error messages, such as suggesting to swap two arguments.

Clearly, there are many tricky corner cases (e.g. polymorphic functions, types with constraints or type classes, type applications etc.). But that should not stop us from trying better in obvious, monomorphic cases.

changed weight to 5

added Tfeature request Trac import typechecker labels

Here are a few examples with proposed alternative error messages:

module ErrorMessages where

i1, i2, i3 :: Int
i1 = 0
i2 = 0
i3 = 0

d1 :: Double
d1 = 1


fid :: Int -> Double -> Int
fid = undefined

fii :: Int -> Int -> Int
fii = undefined

fidi :: Int -> Double -> Int -> Int
fidi = undefined


ex1 :: Int
ex1 = fid i1 i2

{-
ErrorMessages.hs:17:14: error:
    • Couldn't match expected type ‘Double’ with actual type ‘Int’
    • In the second argument of ‘fid’, namely ‘i2’
      In the expression: fid i1 i2
      In an equation for ‘ex1’: ex1 = fid i1 i2

So far ok
-}

ex2 :: Int
ex2 = fid d1 i1

{-
ErrorMessages.hs:36:11: error:
    • Couldn't match expected type ‘Int’ with actual type ‘Double’
    • In the first argument of ‘fid’, namely ‘d1’
      In the expression: fid d1 i1
      In an equation for ‘ex2’: ex2 = fid d1 i1

ErrorMessages.hs:36:14: error:
    • Couldn't match expected type ‘Double’ with actual type ‘Int’
    • In the second argument of ‘fid’, namely ‘i1’
      In the expression: fid d1 i1
      In an equation for ‘ex2’: ex2 = fid d1 i1

Two error messages for one simple error! Why not

ErrorMessages.hs:36:7: error:
    • Cannot use expression ‘fid’ of type ‘Double -> Int -> Int’
      as a function of type ‘Int -> Double -> Int’
    • Probable cause: The first and second argument are swapped
      In the expression: fid d1 i1
      In an equation for ‘ex2’: ex2 = fid d1 i1
-}

ex3 :: Int
ex3 = fidi i1 i2

{-
ErrorMessages.hs:20:7: error:
    • Couldn't match expected type ‘Int’ with actual type ‘Int -> Int’
    • Probable cause: ‘fidi’ is applied to too few arguments
      In the expression: fidi i1 i2
      In an equation for ‘ex3’: ex3 = fidi i1 i2

ErrorMessages.hs:20:15: error:
    • Couldn't match expected type ‘Double’ with actual type ‘Int’
    • In the second argument of ‘fidi’, namely ‘i2’
      In the expression: fidi i1 i2
      In an equation for ‘ex3’: ex3 = fidi i1 i2

Bad; two errors for one. Why not:

ErrorMessages.hs:20:15: error:
    • Missing second argument to ‘fidi’ of type ‘Double’
    • In the function application: fidi i1 i2
      In an equation for ‘ex3’: ex3 = fidi i1 i2
-}

ex4 :: Int
ex4 = fii i1 succ i2

{-
ErrorMessages.hs:57:7: error:
    • Couldn't match expected type ‘Int -> Int’ with actual type ‘Int’
    • The function ‘fii’ is applied to three arguments,
      but its type ‘Int -> Int -> Int’ has only two
      In the expression: fii i1 succ i2
      In an equation for ‘ex4’: ex4 = fii i1 succ i2

ErrorMessages.hs:57:14: error:
    • Couldn't match expected type ‘Int’ with actual type ‘a0 -> a0’
    • Probable cause: ‘succ’ is applied to too few arguments
      In the second argument of ‘fii’, namely ‘succ’
      In the expression: fii i1 succ i2
      In an equation for ‘ex4’: ex4 = fii i1 succ i2

Bad; again two errors for one. Why not:

ErrorMessages.hs:20:15: error:
    • Cannot use expression ‘fii’ of type ‘Int -> Int -> Int’
      as a function of type ‘Int -> (Int -> Int) -> Int -> Int’
    • Probable cause: Missing parenthesis around ‘succ i2’
    • In the function application: fii i1 succ i2
      In an equation for ‘ex4’: ex4 = fii i1 succ i2
-}

changed the description

I'm all for it, if you can see how to achieve it!

The second paragraph of the Description is extremely hard to parse.

changed the description

Reformulated it a bit. I stared a bit at the code, but it is not obvious how to do it: Type information moves from the function towards the arguments and then down, and eventually hits something that does not match. I don’t know enough about the type checker to see if this can sensibly be refactored, and what would be the cost (e.g. performance?) Maybe I’ll try to corner Richard someday and talk this over with him.

We briefly talked about this, and it is not obviously easily possible. Currently, the type checker will, for example with ex2 = fid d1 i1, create two insoluble wanted constraints, one at d1 and one at i1, which are then reported separately.

So here is a wild and not-thought through idea: We already have the machinery to turn (some) type errors into coercions. So how about this scheme:

• The type checker runs. Type errors that can be “fixed” by coercions are fixed this way, and not reported right now. The others are reported as ususal.
• (New step) We try to detect common, interesting patterns of code and error coercions, and possibly move them around. For example:

(i ▷ (DelayedError Int Double), d ▷ (DelayedError Double Int)) :: (Double, Int)

would be re-written to

(i, d) ▷ (DelayedError (Int, Double) (Double, Int)) :: (Double, Int) This pass would only move these coercion wrappers around, otherwise, we preserve the AST as entered by the user.

• Finally, the syntax tree is traversed as well, and all DelayedError axioms are reported.

One side-effect of this would be that we could report error messages citing the actual source of the context where they appear, in the actual syntax of the user (using annotations), which might work better than our current context-explanation-generating machinery.

added error messages label

added Pnormal label