The typical example would be
instance Eq a => Eq [a] where [] == [] = True (a : as) == (b : bs) = a == b && as == bs _ == _ = False
It can handle this case, although it doesn't handle it as a parametric instance. I suspect that we don't need the concept of "parameter instances" at all. We just searches for instances recursively at the call site:
That seems like it could work, but typically, one would like termination guarantees for this search, to avoid the type-checker getting stuck...
Good point. Currently I'm guessing that we need to keep a stack of the traced calls. If a recursive call needs an implicit parameter X which is matched by one of the functions in the stack, we back up from the stack and resolve X to the function found on stack.
foo x = let overload bar (x:Int) = x + 1 in \() -> bar x
baz = in foo (1::Int)
Even if we have only one definition of "bar" in the program, we should not resolve it to the definition of "bar" inside foo. Because that "bar" is not visible at the call site "foo (1::int)". We should report an error in this case. Think of "bar" as a "typed dynamically scoped variable" helps to justify this decision.
So you're saying that any function that calls an overloaded function should always allow its own callers to provide this, even if a correct instance is in scope. Would that mean all instances have to be resolved from main? This also strikes me as strange, since I gather you would get something like "length :: Monoid Int => [a] -> Int", which would break if you happen to have a multiplicative monoid in scope at the call site?
If you already have a correct instance in scope, then you should have no way defining another instance with the same name and type in the scope as the existing one. This is the case for Haskell. But it may be useful to allow nested definitions (using let) to shadow the existing instances in the outer scope of the overloaded call.