Bad type error reporting mixing type vars and type id with the same name

[francois-caddet]

Describe the bug

Sometimes the typechecker can throw something like:

  = The type of the expression was expected to be `a`
  = The type of the expression was inferred to be `a`
  = These types are not compatible

it can actualy append when one is a type variable and the other one is a type identifier.

To Reproduce

let f : forall a. {_: a} -> {_: a} -> {_: a}
  = fun fst snd => ((fst & s nd) | {_: a})

the function below isn't very usefull ;) for a more complet and real case example you can check my comment in #423

Expected behavior I'm not sure if this error can appen in others contexts than the one described by #423 But if it can or if fixing #423 is more dificult, we should probably find a way to distinguish types variables and identifiers in errors.

My first idea would be to force casing of type identifier to start with uper case letter and variables with lower case. But I realy do not think of what changes it imply in nickel.

Thank to share example if you have betters 👍

Environment

• OS name + version:
• Version of the code:

Additional context Add any other context about the problem here.

[yannham]

My first idea would be to force casing of type identifier to start with uper case letter and variables with lower case. But I realy do not think of what changes it imply in nickel.

That wouldn't work so well, because while types are usually capitalized, type variables are not. Also contracts are usually written with a capital letter, but contracts are not types, they are values. We could require terms used in types (i.e. contracts) to be capitalized. On the other hand, it would go a bit against the idea of merging type and terms syntax.

I think printing type variables in a specific way is also an acceptable solution.