Hi all some more, Continuing the idea of a restrained form of instance overlap for type functions ... Type inference I don't expect to be totally decidable, so that may torpedo the idea altogether. I do expect it to be more coherent than GHC's current handling of overlap with fundeps. What's impressive is how much of a 'cottage industry' has grown up using overlaps. Do we really want to throw all that away? SPJ summarises that the idea is that:
... type inference only picks an equation when all the earlier equations are guaranteed not to match. So there is no danger of making different choices in different parts of the program (which is what gives rise to unsoundness).
In my earlier post I proposed how to validate instances so that they don't overlap (although the instance heads might do), by using type inequality restraints. In an ancient mail list discussion of similar ideas [haskell-prime February 2006 'overlapping instances and constraints'] when type families were first mooted, SPJ commented: "Concerning [a suggested approach] it involves *search* which the current mechanism does not. Presumably you have in mind that the type system should "commit" only when there is only one remaining instance declaration that can fit. You need to be very careful not to prune off search branches prematurely, because in a traditional HM type checker you don't know what all the type are completely. And you need to take functional dependencies into account during the search (but not irrevocably). I have not implemented this in GHC. I don't know anyone who has. I don't even know anyone who has specified it. All good stuff to debate. [...] In general, I think that type-system proposals are much easier to evaluate when accompanied with formal type rules. It's not just a macho thing -- it really helps in debugging the dark corners. " Inference for instances without restraints proceeds as usual. Instances with type inequality restraints are validated not to overlap those without, so if there's an instance that fits, we can apply it confidently. What we do need is rules for how type inference gathers evidence of a type inequality from the type environment. Once we've inferred that evidence, we can 'fit' to the instance head and apply the RHS of the type function (or apply the type Class). Evidence of type inequality: Base case: T t1 t2 ... tn /~ U u1 u2 ... um, where T, U type constructors and T /= U n, m >= 0 Derived case: T t1 t2 ... tn /~ T u1 u2 ... un, where T type constructor And ti /~ ui for some i (I suspect this is far as GHC tries currently to discriminate overlaps, based on the groundedness experiments discussed in the HList paper section 9. I think it's possible to get a bit further ...) also derived: t t1 t2 ... tn /~ t u1 u2 ... un, where t is a type term AND ti /~ ui (t can be type term except a type function) and: T t1 t2 ... tn /~ t u1 u2 ... un, if ti /~ ui, where T type constructor (again t can be any type term except a type function note that matching type args is from the right-hand end, because t might turn out to be of the form (tt uu1 uu2 ...) essentially: whatever t resolves to, the overall types must be unequal) as well: T t1 t2 ... tn /~ t u1 u2 ... um, where T type constructor And m > n (t any type term except a type function, if m > n then t's arity is more than T's, so they can't be the same.) Algebra: Type inequality is symmetric: t /~ u ==> u /~ t transitive across equality: t /~ u, u ~ v ==> t /~ v My (highly hand-wavy) understanding from the 'outside-in' papers of how type inference proceeds is that the possible instances 'compete' to apply until one fits. (If there would be several that might fit, it's 'first come first served'. So it's essential under GHC's current forms of type families that overlapping instances are confluent.) With type inequality restraints we keep to that rule: inference must not apply an instance until the type environment provides evidence of the inequality. AntC