Record tails in error messages are printed wrong

[vkleen]

Record tails in error messages are printed without a preceding ;. E.g.

nickel> let fail : forall a. {; a} -> Bool = fun r => r
error: incompatible types
  ┌─ repl-input-0:1:47
  │
1 │ let fail : forall a. {; a} -> Bool = fun r => r
  │                                               ^ this expression
  │
  = The type of the expression was expected to be `Bool`
  = The type of the expression was inferred to be `{a}`
  = These types are not compatible

The {a} should really be {; a} in keeping with the surface syntax.

[yannham]

I guess the pretty printer is at fault, here

[vkleen]

It seems the pretty printer does the right thing:

❯ cargo run -- pprint-ast <<<'let f: forall a. {; a} = {} in f'
    Finished dev [unoptimized + debuginfo] target(s) in 0.10s
     Running `target/debug/nickel pprint-ast`
let f : forall a. { ; a}  = {  } in f%

It's probably the more ancient printer for error reporting?

[vkleen]

The problem seems to be that the Display implementation for Types doesn't use the pretty printer. Instead it's an ad-hoc implementation that's probably missing an edge case somewhere. I think we should replace that Display implementation with a call to the pretty printer similar to the one for RichTerm.

[yannham]

Ah, indeed, it should use the pretty printer. Note that we have to make sure the output is strictly the same, because the error reporting code for contracts relies on knowing the exact number of characters (at least, for basic type constructors) and spacing to underline the right thing. Or maybe we can do things differently, to ensure that we underline the right thing in a more resilient way.

[yannham]

This is fixed on master, probably because of #1262.