You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
Environment
Steps to reproduce
Given:
Hover over the def and usage of x, y, and bar.
Expected behavior
?a
?b
?b -> ?a * ?b
Actual behavior
?a
?a -> ?a * ?a
at def and "most general" usage, but?b -> ?a * ?b
at "this usage" usageComments
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 (
val
s). 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.The text was updated successfully, but these errors were encountered: