Typing regression on polymorphic fields

[stedolan]

The patch in #10959 fixed a serious soundness bug (#10907) in which the types of variables bound in patterns were being incorrectly generalised even when they refer to existentials.

However, the fix also breaks some uses of polymorphic record fields, where the generalisation is sound (and seemingly required, by the semantics of first-class polymorphism). The following program fails to typecheck since 4.14:

type ('a, 'b) t
type 'a ex = T : ('a, 'b) t -> 'a ex
type forall = { f : 'a. 'a ex }

let eta { f = T x } = { f = T x }

This is an eta-expansion of the type forall 'a . exists 'b . ('a, 'b) t, but since 4.14 it yields the error:

Error: This field value has type 'b ex which is less general than 'a. 'a ex

because the type of the field f is not generalised.

[gasche]

(In the discussion, @lpw25 proposed a refined criterion to lower the level not of all type variables occurring under a GADT constructor, as implemented, but all type variables that occurs in the type of a term variable that also captures an existential. This refined criterion would also reject the example, as x mentions both 'a and the existential 'b.)

I'm not sure about your claim that the generalization is sound (and I don't understand the semantics of first-class polymorphism well enough to tell that it is required). The following versions work:

let eta (p : forall) : forall =
  { f = match p with {f = T x} -> T x }

let eta (p : forall) : forall =
  let p = match p with {f = T x} -> T x in
  { f = p }

but these ones do not work

let eta { f = T x } = { f = T x }

let eta (p : forall) : forall =
  match p with {f = T x} -> { f = T x }

If I think about the logical statement you are encoding in your GADTs, I see one proof:

-------------------------------
a, b, x : (a, b) t |- (a, b) t 
------------------------------------
a, b, x : (a, b) t |- ∃b₁. (a, b₁) t 
---------------------------------------
a, v : ∃b₀. (a, b₀) t |- ∃b₁. (a, b₀) t
-----------------------------------------------
p : (∀a₀. ∃b₀. (a₀, b₀) t), a |- ∃b₁. (a, b₁) t
----------------------------------------------------
p : (∀a₀. ∃b₀. (a₀, b₀) t) |- (∀a₁. ∃b₁. (a₁, b₁) t)
 
proof term:
  Λa₁.
   let v = p a₁ in
   unpack (b, x) = v in
   pack (b, x)

In this proof, I need to apply the right rule on the forall in the goal before I can apply a left rule on the hypothesis in the context. This is consistent with rejecting programs that start by opening { f = T x} as a pattern and continue from there, and forcing you to introduce { f = ... } first (or another forall-right-rule through a generalized let).

[gasche]

On the other hand, the following program is accepted, while it would be rejected by my reasoning above:

type 'a w
type forall = { f : 'a . 'a w }
let eta { f = x } = { f = x }

[stedolan]

Thanks for the explanation. I was confused here and misunderstood the bug and its fix, your explanation looks correct to me.

On the other hand, the following program is accepted, while it would be rejected by my reasoning above:

type 'a w
type forall = { f : 'a . 'a w }
let eta { f = x } = { f = x }

I think that matching on a polymorphic record (the pattern { f = x }) is not generally a left rule for forall. The context can contain polymorphic values, so matching {f = x} simply moves x, with its foralls, into the context. The actual elimination of the forall takes place in the variable rule later, so your eta function does in fact introduce the forall on the right hand side of the = before eliminating the forall on the occurrence of x.

The same reasoning explains why this version of eta works as well:

let eta { f = x } = { f = match x with T y -> T y }

Again, the left rule for forall is applied after the right rule, in the scrutinee of match. The initial unpacking moves the value around, keeping its polymorphism.

However, my original example contains the pattern {f = T x}, where the polymorphic value T x is unpacked, eliminating the forall as well as the existential. So, here the left rule is being applied during matching, and it would be incorrect for it to remain polymorphic.

(So there's no bug here and 4.14 and onwards are doing the right thing. I'll fix the code that triggered this, thanks for the help)