Richard Eisenberg
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 one first:
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(?) Anthony