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
Structural hashing and equality for dependent types.
Dependent types RecType and HKLambda were generative. Any two such
types were considered to be different, even if they had the same structure.
This causes problems for subtyping and constraint solving. For instance,
we cannot detect that a Hk-Lambda has already been added to a constraint,
which can cause a cycle. Also, monitoredIsSubtype would not work if
the compared types are dependent. Test cases are i3695.scala and i3965a.scala.
To fix this, we need to have a notion of hashing and equality which
identifies isomorphic HkLambdas and RecTypes. Since these are very
frequently called operations, a lot of attention to detail is needed
in order not to lose performance.
0 commit comments