Poor error message in polymorphic tail type error

[matthew-healy]

Describe the bug

The following program:

let f : forall r. (forall p. [| 'blo, 'ble ; r |] -> [| 'bla, 'bli; p |]) =
  match { 'blo => 'bla, 'ble => 'bli, _ => 'blo } 
in f 'bli

raises a type error:

error: incompatible types
  ┌─ repl-input-0:2:44
  │
2 │   match { 'blo => 'bla, 'ble => 'bli, _ => 'blo } 
  │                                            ^^^^ this expression
  │
  = Expected an expression of type `a`
  = Found an expression of type `[| 'blo ; _erows_a |]`
  = These types are not compatible

The type a here is pulled out of thin air. What the error is really trying to say is that this function body should be valid for any tail p, including those that don't include the variant 'blo. We should improve the error message in this specific case to make that clearer.

Additional context

Note that record tails exhibit similar behaviour. E.g. in the program:

let f : forall r p { blo: String, ble: Number ; r } -> { bla: String, bli: Number ; p } =
  fun { blo, ble, .. } =>
    { bla = blo, bli = ble }
in f { blo = "", ble = 0 }

where the error message is:

error: incompatible types
  ┌─ repl-input-3:3:5
  │
3 │     { bla = blo, bli = ble }
  │     ^^^^^^^^^^^^^^^^^^^^^^^^ this expression
  │
  = Expected an expression of type `a`
  = Found an expression of type `{  }`
  = These types are not compatible