Ah -- I think the waters have been muddied somewhat as our thoughts have evolved. The plan of action (of history, at this point -- I merged into HEAD yesterday) is to use the check labeled (B) on the wiki page. This check does *not* ban all nonlinear type families. It just makes certain combinations of standalone instances conflict. Equations in closed type families (the new name for "branched instances", which I'm trying to avoid saying) do not have any of these restrictions. And, many thanks for pointing out your contribution to that discussion page. I met with Simon PJ and Dimitrios V last summer to discuss this feature, and we went through the possibilities and settled on "type instance where". We're all now busy writing up a paper on the design and type safety ramifications, and we switched gears to "type family … where" because it made for a more consistent feature, in our eyes. I'm really happy with where this ended up, so thanks for making the suggestion originally! Richard On Jun 22, 2013, at 10:28 AM, AntC wrote:
Richard Eisenberg
writes: And, in response to your closing paragraph, having type-level equality is the prime motivator for a lot of this work, so we will indeed have it!
Thank you Richard, I'll take comfort in that.
I'd beware this though: the Nonlinearity wikipage says "a medium-intensity search did not find any uses of nonlinear ... family instances in existing code, ..."
That doesn't surprise me, but I wouldn't put much weight on it. The main purpose of repeated tyvars in a (class) instance is so that you can have a 'wider' overlapping instance with distinct tyvars (and a non-congruent result). Since family instances don't currently support non-congruent overlap, I guess there would be a pent-up demand to translate class instances to (branched?) family instances with repeated tyvars.
Here's two example instance from HList that mirror your two instances for family F:
-- pattern of instance F x x class TypeEq a b c | a b -> c instance TypeEq x x HTrue instance (c ~ HFalse) => TypeEq x y c
-- pattern of instance F [x] x -- actually F x (HCons x ...) class Has e l -- constraint instance Has e (HCons e l') instance (Has e l') => Has e (HCons e' l')
I haven't, though, seen those two patterns appearing as instances of the same class.
And given that those patterns are to be allowed only within branched instances, the 'cleaned up syntax' makes sense -- I'm glad I suggested it! (see http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage#Suggestio ns, under 'Idiom of a total function' ;-)
It still seems mildly 'unfair' to ban repeated tyvars when really the cause of the problem is infinite types. I take you to be saying that as soon as we allow UndecidableInstances, it's just too hard to guard against infinite types appearing from chains of instances, possibly in 'distant' imports or recursive module references.
So I understand it's not worth sacrificing type safety.
AntC
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users