Reporting generated ty var names does not consider nesting

[azdavis]

Environment

• Millet version: v0.12.2

Steps to reproduce

Given:

fun foo x =
  let
    fun bar y = (x, y)
  in
    bar
  end

Hover over the def and usage of x, y, and bar.

Expected behavior

• x has type ?a
• y has type ?b
• bar has type ?b -> ?a * ?b

Actual behavior

• x and y both are shown as type ?a
• bar is shown as type ?a -> ?a * ?a at def and "most general" usage, but ?b -> ?a * ?b at "this usage" usage

Comments

This is because we associate the bound ty var from the ty scheme with the meta var when generalizing. But we do not then shift the bound var when crossing another binding site as we should (since bound vars are de brujin indices) and so e.g. the type of bar is shown incorrectly.

We might be able to hack a fix by pushing and popping the current level of generalizing sites (vals). Or maybe we already have this info with the meta var ranks.

Note that there is no actual type-checker unsoundness or incorrect inference, it just is displaying types incorrectly when hovering sometimes. For instance the type of foo is computed as ?a -> ?b -> ?a * ?b, and this is correctly reported.

[azdavis]

This is also already checked in as a failing test:

https://github.com/azdavis/millet/blob/bd97f38f0f333c803090bf6bbb4637e2f877ef46/crates/tests/src/hover/ty.rs/#L196

[azdavis]

Thinking about it more, I don’t think the meta var rank is enough information to offset the bound var index. We don’t know how many variables will be generalized and therefore bound at a given generalization site (val binding) until we do it.