Repeated variables in type family instances
anthony_clayden at clear.net.nz
Thu Jun 20 12:47:28 CEST 2013
> Richard Eisenberg <eir <at> cis.upenn.edu> writes:
Hi Richard, I was hoping one of the type/class/family luminaries would
pick this up, but I'll make a crack at moving it along.
> It’s come to my attention that there is a tiny lurking potential hole in
> GHC’s type safety around type families in the presence of
> UndecidableInstances. ...
Hmm. Several things seem 'fishy' in your examples. I'll take the second
> > type family G
> > type family G = [G]
> This declarations are all valid in GHC 7.6.3.
G is 0-adic, so only one instance is allowed, so it should be like a
simple type synonym. What about:
> type G2 = [G2]
ghc rejects "Cycle in type synonym declarations"
But I guess ghc doesn't want to make a special case of 0-adic type
functions. Really that G instance is no different to:
> type instance F Int Bool = [F Int Bool]
G's instance is degenerate because I can't declare a term of type G:
> g :: G
> g = undefined
ghc says "Occurs check: cannot construct the infinite type: uf0 = [uf0]"
This isn't unusual in the borderlands of UndecidableInstances: you can
declare an instance but never use it.
Now to your main example:
> > type family F a b
> > type instance F x x = Int
> > type instance F [x] x = Bool
I plain disagree that these are overlapping. That code compiles OK with
OverlappingInstances switched off (at ghc 7.6.1). What's more, I can
access both instances:
*Main> :t undefined :: F Int Int
undefined :: F Int Int :: Int
*Main> :t undefined :: F [Int] Int
undefined :: F [Int] Int :: Bool
For them to overlap would require the two arguments to be equal in the
second instance. In other words: [x] ~ x
Let's try to do that with a class instance:
> class F2 a b
> instance ([x] ~ x) => F2 [x] x
ghc rejects "Couldn't match type `x' with `[x]'"
So you haven't yet convinced me that there's anything that needs 'fixing'.
Especially if you're proposing a breaking change.
I make heavy use of repeated type vars in class instances (in combination
with an overlapped instance with distinct type vars). I have been waiting
patiently for overlapping instances to appear with type funs, so I can
make my code easier to read (more functional ;-).
I guess the key thing I'm looking for is a type-level test for type
equality -- which needs repeated type vars(?)
More information about the Glasgow-haskell-users