Improving record type errors

language
#1

It came out from Slack that record type errors still need some love. I think it would be useful to discuss here what’s the best direction to take.

There’s also this issue which should be addressed but which I wasn’t able to replicate.

I’m pasting some error expamples below to help the discussion.

A

a = [{ a: 1, b: 2 }, { a: 1 }]

Could not match type

           ( b :: Int
           ...
           )

         with type

           ( ... )


       while trying to match type
                                    ( b :: Int
                                    ...
                                    )

         with type
                     ( ... )

       while inferring the type of [ { a: 1
                                     , b: 2
                                     }
                                   , { a: 1
                                     }
                                   ]
       in value declaration a

B

b = [{ a: { b: 1 } }, { a: { c: 1 } }]

 Could not match type

    ( b :: Int
    ...
    )

  with type

    ( c :: Int
    ...
    )


while trying to match type
                             ( b :: Int
                             ...
                             )

  with type
              ( c :: Int
              ...
              )

while inferring the type of [ { a: { b: ...
                                   }
                              }
                            , { a: { c: ...
                                   }
                              }
                            ]
in value declaration b

C

c = [{ a: 1, b: 2 }, {a : true, b: 2 }]

Could not match type

        Int

      with type

        Boolean


    while trying to match type
                                 ( a :: Int
                                 ...
                                 )

      with type
                  ( a :: Boolean
                  ...
                  )

    while inferring the type of [ { a: 1
                                  , b: 2
                                  }
                                , { a: true
                                  , b: 2
                                  }
                                ]
    in value declaration c

Case A and B are basically the same, just with a different nesting level of the error. In both, the while trying to match type ... with type ... is completely usess as it’s just a repetition of the Could not match type ... with type ... part.

Case C shows different informations in the two sections, but it could be made similar to the first two cases by still showing the rows diff instead of just the labels’ types.

A possible solution would be to eliminate the second section of the error section, making for example the new error for A as:

Could not match type

           ( b :: Int
           ...
           )

         with type

           ( ... )

       while inferring the type of [ { a: 1
                                     , b: 2
                                     }
                                   , { a: 1
                                     }
                                   ]
       in value declaration a


I think the error is a bit cryptic for new users maybe. Would a partial rewording help? Maybe it could be good to make the error message more specific to records instead of using the same structure of the other type errors.

#2

The unification trace is because of the ErrorUnifyingTypes hint. I’m not convinced of the utility of this hint since more often than not it’s redundant like in this type error. The reason why it might be helpful is if you unify Foo -> Bar with String -> Bar you’ll see Foo and `Bar, and then both of those larger types in the trace. But I’m pretty sure it will always have the one redundant unification trace. We could maybe do a check to remove the top-most unification hint if the types in the hint match the types in the actual error.

#3

@natefaubion

I’ve pushed some code that removes the ErrorUnifyingTypes hint when it’s a duplicate of the TypesDontUnify hint. It improves cases A and B, but not C right now. Not sure if I should do anything about it, though.

I also have found something that is probably a bug, let’s call it D:

a = [ { a: 1
      , b: 2 -- test
      }
    , { a: 1 }
    ]

In this case the first row is just shown as a generic t0. I think the comment messes up something somwhere.

I also have two partially related (and very noobish) questions:

  • What are the debug tools I should use? I’m going with Debug.Trace, but it’s kinda painful. If nothing is used right now, would it be possible to add a library to print data types in a more readable way?
  • How am I supposed to test something like this? Do I have a way to match the error message with the expected one?

Thanks!

#4

I’ve been thinking for a while that golden tests for error output might be nice to have. At the moment we only verify the set of error codes we expect a module to produce, but having golden tests for the full error output would allow us to catch bugs if we had accidentally removed or changed a source span, or something like that. That’s something which would ideally be its own PR though; if you wanted to work on that too I’d be happy to offer guidance.

#5

I don’t think there are any good debug tools right except that. I added a bunch in my polykinds branch so I could debug the typechecker environment. https://github.com/natefaubion/purescript/blob/4c0c1bfcc7091dcf02f63cb91fe0b5271970d9e5/src/Language/PureScript/TypeChecker/Monad.hs#L342-L431

#6

I also think golden tests for errors would be really nice.

#7

Yeah I’d like to work on golden tests :slight_smile: I’ll probablu need a bit of pointing in the right direction though.

1 Like
#8

There are golden tests for the CST lexer.

#9

I’m putting this on hold since stripping the redundant hints causes the issue with the TUnknown hint in some cases. I’m not entirely sure why it’s there, but anyways it would help to have golden tests for errors first.

#10

@natefaubion @hdgarrood
Would you rather have:

  1. An additional directive in the failing tests files to perform a golden test on the error output
  2. A sub folder in failing
  3. Something completely separated
#11

I think it would be best to have golden tests unconditionally - for every test case which should emit a warning or an error. I think that would mean that the existing directives would become obsolete, too, so we could remove those.

#12

I think preferably there would also be a flag you could optionally supply to the test runner to tell it that you do actually intend for there to be changes, so you would be giving it permission to overwrite the existing golden tests. (Or is this already the case for the CST lexer golden tests?)

#13

Tasty.Golden mentions an --accept flag that should do that.

1 Like
#14

Ok cool, there are two options to regenerate the output:

  1. pass --accept in the --test-arguments
  2. delete the .out file

It’s more or less complete, I just need a few more steps but I’m stopping for the day:

  1. How to avoid having the test output print the error message every time (The CST tests are not doing it, so there has to be a way :smiley: )
  2. Check that it works with warnings
  3. Replace the old directives code.
1 Like
#15

@natefaubion @hdgarrood

I have pushed a working commit on my repo, but there are a couple of issues remaining:

  • getTestFiles from TestUtils.hs uses absolute paths. This means that the absolute path appears in the error ouput, and this is obviously a problem.
    Can we change it to relative paths?
    Should I write a new function with relative paths just for the golden tests?

  • Are we gonna assume that all the newly generated .out files will have the correct output? How are we gonna check them otherwise? An option could be checking that the directive error appears in the out file as a one time check.

  • Once this is done can I remove all the shouldFail/Warn directives?

Thanks!

#16

This means that the absolute path appears in the error ouput, and this is obviously a problem.

I would like to change to relative paths everywhere then, if possible. Uniformity tends to make things simpler and more reliable in my experience.

Are we gonna assume that all the newly generated .out files will have the correct output?

When we (you) initially generate them, I think so, yes.

Once this is done can I remove all the shouldFail/Warn directives?

Yes please!

#17

I think that using relative paths (from the repo root) should be fine. Does stack expose that in some way, like through an environment variable?

Yes, with golden tests, you assume that what is committed has been verified by a human to be correct. When committing changes to an out file, the diff should be manually verified by a human as well. The point of golden tests is to prevent unintended changes. I’m actually fine though with keeping the directives, since it seems like a good sanity check.