Branched type family instances

[Richard Eisenberg]

Hello all,

 

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. Consider the following:

 

> type family F a b

> type instance F x x = Int

> type instance F [x] x = Bool

> 

> type family G

> type family G = [G]

 

This declarations are all valid in GHC 7.6.3. However, depending on the
reduction strategy used, it is possible to reduce `F G G` to either Int or
Bool. I haven't been able to get this problem to cause a seg-fault in
practice, but I think that's more due to type families' strictness than
anything more fundamental. Thus, we need to do something about it.

 

I have written a proposal on the GHC wiki at
http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/Nonlinearity

 

It proposes a change to the syntax for branched instances (a new form of
type family instance that allows for ordered matching), but as those haven't
yet been officially released (only available in HEAD), I'm not too worried
about it.

 

There are two changes, though, that break code that compiles in released
versions of GHC:

---

1) Type family instances like the two for F, above, would no longer be
accepted. In particular, the overlap check for unbranched (regular
standalone instances like we've had for years) would now check for overlap
if all variables were distinct. (This freshening of variables is called
'linearization'.) Thus, the check for F would look at `F x y` and `F [x] y`,
which clearly overlap and would be conflicting.

 

2) Coincident overlap between unbranched instances would now be prohibited.
In the new version of GHC, these uses of coincident overlap would have to be
grouped in a branched instance. This would mean that all equations that
participate in coincident overlap would have be defined in the same module.
Cross-module uses of coincident overlap may be hard to refactor.

---

 

Breaking change #1 is quite necessary, as that's the part that closes the
hole in the type system.

Breaking change #2 is strongly encouraged by the fix to #1, as the
right-hand side of an instance is ill-defined after the left-hand side is
linearized. It is conceivable that there is some way to recover coincident
overlap on unbranched instances, but it's not obvious at the moment. Note
that this proposal does not contain a migration path surrounding coincident
overlap. In GHC <= 7.6.x, branched instances don't exist and we have
coincident overlap among unbranched instances; and in GHC >= 7.8.x, we will
prohibit coincident overlap except within branched instances. We (Simon PJ
and I) think that this shouldn't be too big of a problem, but please do
shout if it would affect you.

 

Please let me know what you think about this proposal!

 

Thanks,

Richard

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130529/4b3192bc/attachment.htm>