Overloading Doesn't Play Nice with Generics

[HalflingHelper]

Something Like This Breaks

function length(List<Nat>) -> Nat {
  length(empty) = 0
  length(node(n, next)) = 1 + length(next)
}

function length<E>(List<E>) -> Nat {
  length(empty) = 0
  length(node(n, next)) = 1 + length(next)
}

with the error

List.pf:37.31-37.43: could not find a match for call to function length
overloads:
        (<E> fn List<E> -> Nat)
        (fn List<Nat> -> Nat)

(Specifically the call to length in the generic method).

This is an issue for defining an overloaded list equality method with the equal for Nat. We can obviously work around this for the time being, but might be something we want to fix.

I stared at the logic stemming from type_check_call_funty for a while, and didn't see something that could immediately solve this.

[jsiek]

This is currently the intended behavior, except that the error message could be nicer or come earlier. For example, one could disallow the second definition of length because it is a generic.

On the other hand, we could add more smarts to the overload resolution algorithm to handle this situation. I know how to do that, its just a bit more complicated.