Repeated variables in type family instances

[Richard Eisenberg]

On Jun 20, 2013, at 11:47 AM, AntC wrote:
> 
> Hmm. Several things seem 'fishy' in your examples. I'll take the second 
> one first:
> 
>>> type family G
>>> type family G = [G]
> 

Your criticisms of this example (that it is nullary and unusable) are valid. But, it would be easy to change the example to eliminate these problems and not change the fundamental character of what is going on. The changed version would just be a little more verbose.

> 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
> 

This is a subtle example, indeed.

There are two arguments why I believe that the two instances for F are problematic:

1) The type safety of Haskell (in GHC) is predicated on the type safety of System FC / Core, the typed language that Haskell is compiled to. Type family instances are compiled into axioms -- essentially, assertions of the equality of two types. So, the instances of F and G give us the following axioms (assuming no kind polymorphism):

axF1 :: forall (x :: *). F x x ~ Int
axF2 :: forall (x :: *). F [x] x ~ Bool
axG :: G ~ [G]

We can now fairly easily build a coercion from Int to Bool, with the following pieces:

axF1 G :: F G G ~ Int
sym (axF1 G) :: Int ~ F G G

<G> :: G ~ G
F axG <G> :: F G G ~ F [G] G   -- this is a congruence form of coercion, which lifts coercions through type constructors like F

sym (axF1 G) ; F axG <G> ; axF2 G :: Int ~ Bool

Yikes! That's bad if we can equate Int with Bool, and note that no infinite types are needed. In FC, type families don't compute, so the specter of infinite types doesn't even arise. 

But, would such a coercion ever come up in practice? It's hard to say. Although the bare coercions that GHC produces during type checking is unlikely to produce that, there are *lots* of transformations that happen to coercions after they are first produced. The type safety of FC (and, therefore, of Haskell) requires that a coercion between Int and Bool is impossible to form, not just that it doesn't come up in practice. Thus, we have a problem here.

2) I can get dangerously close to producing an inconsistency in Haskell by pushing on this. See attached. The payoff is in F3.hs, which contains a (ordinary) list that manifestly contains an Int and a Bool. Unfortunately for my example (but fortunately for Haskell), any access of this list produces a type error before treating an Int as a Bool or vice versa. The error is that we can't have infinite types. But, it is easy to imagine a slightly different evaluation strategy for type families that would avoid the need for infinite types that would allow these files to compile and the dangerous list to exist. It seems like a bad plan to have Haskell's type safety rest on these fragile grounds.


Happily, the fix proposed in http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/Nonlinearity is fairly non-invasive. It prohibits the instances for F, but it still allows nonlinear axioms. It also cleans up the syntax for closed type families (previously called branched instances) in a way that tells a nicer story, so to speak. I've implemented the proposal, and expect to merge in the next 24 hours -- just going through the last motions now (validating, updating the manual, etc.).

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!

Richard

-------------- next part --------------
A non-text attachment was scrubbed...
Name: F.tgz
Type: application/octet-stream
Size: 562 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130620/88235bf7/attachment.obj>
-------------- next part --------------