Misleading Type Error for Chain of Function Apps

[montymxb]

For the following program:

-- oops is undefined
f1 : Int -> Int
f1(x) = if x < 0 then x else oops(x+1)

f2 : Int -> Bool
f2(x) = if f1(x) == 0 then True else False

The error indicated is:

Type error in "Program" (line 33, column 15)
You did not define f1

However, if we remove f2, we get:

Type error in "Program" (line 30, column 42)
You did not define oops

Although the first error is correct, it's a bit misleading, as it suggests that f1 is not correct. It is syntactically correct, but it does not type check because oops is undefined, and in turn this results in f1 being undefined as well. The resulting error we then see is that f1 is the problem, which can be a bit misleading when the issue is related to a function called by f1. To see this further, if we have 4 or more functions, then the underlying source of the propagated type error is obscured.

-- f0 is undefined...
f1 : Int -> Int
f1(x) = f0(x)

f2 : Int -> Int
f2(x) = f1(x)

f3 : Int -> Int
f3(x) = f2(x)

f4 : Int -> Int
f4(x) = f3(x)

Type error in "Program" (line 40, column 12)
You did not define f3

[MartinErwig]

Alex and Ben,

We should discuss type error messages and their creation in a systematic way; maybe in a separate meeting at some point in time.

First, we need a type system. Only then we can extend the type system by (helpful) error messages.

-- Martin

On Oct 30, 2020, at 9:35 AM, Benjamin Wilson Friedman notifications@github.com wrote:

For the following program:

f1 : Int -> Int

f1(x) = if x < 0 then x else oops(x+1 )

f2 : Int -> Bool

f2(x) = if f1(x) == 0 then True else False The error indicated is:

Type error in "Program" (line 33, column 15) You did not define f1

However, if we remove f2, we get:

Type error in "Program" (line 30, column 42) You did not define oops

Although the first error is correct, it's a bit misleading, as it suggests that f1 is not correct. It is syntactically correct, but it does not type check because oops is undefined, and in turn this results in f1 being undefined as well. The resulting error we then see is that f1 is the problem, which can be a bit misleading when the issue is related to a function called by f1. To see this further, if we have 4 or more functions, then the underlying source of the propagated type error is obscured.

f1 : Int -> Int

f1(x)

f0(x)

f2 : Int -> Int

f2(x)

f1(x)

f3 : Int -> Int

f3(x)

f2(x)

f4 : Int -> Int

f4(x) = f3(x) Type error in "Program" (line 40, column 12) You did not define f3

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[alexgrejuc]

First, we need a type system

Yes, I would like to rewrite the bogl types and a lot of the type checker once we agree on this. I think this can be done quite soon.

As we have all noticed over the last few months, the type checker had plenty of issues. Ben and I have patched it up, but in an ad-hoc way. A more systematic rewrite will help us fix fledgling issues that we currently have and that we are currently just patching rather than truly resolving.

[alexgrejuc]

As for this specific issue, I believe that a list of type errors is produced. In the past, we used to display them all, but that was overwhelming. Now, the last element is shown.

A simple fix for this specific issue is to show the head instead since that is the direction that the causality propagates. In general though, causality and determining the best set of type errors to display is of course a more difficult problem and something we can think about quite a bit more.

[alexgrejuc]

Fixed by this commit.