2012/1/16 Yin Wang :

...

...

...

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.

You may want to look at scala's approach for their implicit arguments. They use a certain to conservatively detect infinite loops during the instance search, but I don't remember the details off hand. While talking about related work, you may also want to take a look at Scala's implicit arguments, GHC implicit arguments and C++ concepts...

...

...

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.

Yes, but different ones may be in scope at different places in the code, right?

But it may be useful to allow nested definitions (using let) to shadow the existing instances in the outer scope of the overloaded call.

I considered something like this for instance arguments in Agda, but it was hard to make the instance resolution deterministic when allowing such a form of prioritisation. The problem occurred if a shadower and shadowee instance had slightly different types, such that only the shadowee was actually type-valid for a certain instance argument. However, the type information which caused the shadower to become invalid only became available late in the type inference process. In such a case, it is necessary to somehow ascertain that the shadower instance is not chosen, but I did not manage to figure out how to get this right. Dominique