On Sat, Jan 14, 2012 at 2:38 PM, Dominique Devriese
I may or may not have thought about it. Maybe you can give an example of parametric instances where there could be problems, so that I can figure out whether my system works on the example or not.
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: 1. If "g" has an implicit parameter "f", search for values which matches the name and instantiated type in the current scope. 2. If a value is found, use it as the argument. 3. Check if the value is a function with implicit parameters, if so, search for values that matches the name and type of the implicit parameters. 4. Do this recursively until no more arguments contain implicit parameters.
This coupling you talk about is not actually there for instance arguments. Instance arguments are perfectly usable without records. There is some special support for automatically constructing record projections with instance arguments though.
Cool. So it seems to be close to what I had in mind.
I am not sure about the exact workings of your system, but I want to point out that alternative choices can be made about the workings of inferencing and resolving type-class instances such that local instances can be allowed. For example, in Agda, we do not infer instance arguments and we give an error in case of ambiguity, but because of this, we can allow local instances...
Certainly it should report error when there are ambiguities, but sometimes it should report an error even there is only one value that matches the name and type. For example, 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.