Richard, I'm interested by your argument at the bottom of the wiki page about the alternative (non-)solution of disallowing non-linear patterns altogether. I'll quote it for reference: One way we (Simon, Dimitrios, and Richard) considered proceeding was to prohibit nonlinear unbranched instances entirely. Unfortunately, that doesn't work. Consider this: type family H (x :: [k]) :: * type instance H '[] = Bool Innocent enough, it seems. However, that instance expands to type instance H k ('[] k) = Bool internally. And that expansion contains a repeated variable! Yuck. We Thought Hard about this and came up with various proposals to fix it, but we weren't convinced that any of them were any good. So, we concluded to allow nonlinear unbranched instances, but we linearize them when checking overlap. This may surprise some users, but we will put in a helpful error message in this case. So in summary, if you extend the pattern with explicit kind info, you get linearity for patterns that are actually fine. It's not clear to me why you would in fact use the expanded form when checking linearity. Wouldn't you get the same problem if you try to check a value-level pattern's linearity after including explicit type info. If so, why is that a problem for type instance patterns if it isn't a problem for value-level patterns? For example, take the following value-level function null :: [a] -> Bool null [] = True null (_:_) = False After including explicit System F-like type arguments, that would become null @a ([] @a) = True null @a ((:) @a _ _) = False So we get the same problem of non-linearity of the expansion even though the original is fine, right? Perhaps we could consider adding an internal annotation like the "@" above on the arguments inserted by the expansion of a type instance pattern with kinding info (or sort info if that's more correct?). Then one could ignore those arguments altogether during the linearity check. Note: I'm in favor of avoiding non-linear patterns for type families if at all possible, in order to keep the type-level computational model functional and close to the value-leve one. I would hope we could forbid linear patterns for type classes as well at some point in the future, although that could perhaps be more controversial still... Thanks! Dominique P.S.: I hope you'll be writing a more detailed account of this work (a research paper?) at some point and I look forward to reading it... P.S.2: On an unrelated note: will you also do a completeness check on closed type family definitions? 2013/5/29 Richard Eisenberg <eir@cis.upenn.edu>:
(Sorry for the re-send – got the wrong subject line last time.)
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
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users