How does one take the meet of two polymorphic function types? The issue I’m finding is that the two function types can have a different number of type variables. Or the same number of variables, but distinct names.
I’m following along with Local Type Inference (Pierce and Turner). On page 7, they give the rule for taking the meet of two polymorphic function types as:
$$ S wedge T = All(bar X ) bar J to M space textrm{if} \ S = All(bar X)(bar V) to P \ T = All(bar X)(bar W) to Q \ bar V vee bar W = bar J \ bar P wedge bar Q = bar J \ \ Bot space textrm{otherwise} $$
The overbars represent multiple parameters in a parameter list, so $bar X$ means something like $X_1, X_2, X_3$. $wedge$ is meet and $vee$ is join. $Bot$ is the bottom of the type latttice.
Is the rule saying that the meet of two polymorphic functions is $Bot$ unless the two functions have the same number of type variables and those type variables have the same names? That surprises me, because I’d expect $(All(X)X to X)space wedge space (All(Y) to Y) = All(X)X to X$ because I wouldn’t expect choice of type variable name to matter.
