Repeated variables in type family instances
anthony_clayden at clear.net.nz
Sat Jun 22 11:28:53 CEST 2013
> Richard Eisenberg <eir <at> cis.upenn.edu> 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
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
> -- 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
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!
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.
More information about the Glasgow-haskell-users