Re: Repeated variables in type family instances
Richard, Thanks for your answers. 2013/6/24 Richard Eisenberg e...@cis.upenn.edu: The nub of the difference is that type families can pattern-match on kinds, whereas term-level functions cannot pattern-match on types. So, while the @a is repeated in the pattern as written above, GHC does not, when matching a pattern, check that these are the same. In fact, they have to be the same if the function argument is well-typed. On the other hand, type family equations *can* branch based solely on kind information, making the repeated variable semantically important. Interesting, I wasn't aware this was possible. I agree that if it's possible to branch solely on kind info, then they should be taken into account for the linearity check. Do you perhaps have an example of how to do this sort of branching? Thanks, Dominique ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Repeated variables in type family instances
Sure. Say you want a default type at any given kind. You could write something like this: type family Default (a :: k) :: k type instance Default (a :: *) = () type instance Default (a :: * - *) = [] type instance Default (a :: * - * - *) = (,) type instance Default (a :: * - * - * - *) = (,,) This isn't perhaps the most useful example, but it works. Richard On Jun 26, 2013, at 8:33 AM, Dominique Devriese wrote: Richard, Thanks for your answers. 2013/6/24 Richard Eisenberg e...@cis.upenn.edu: The nub of the difference is that type families can pattern-match on kinds, whereas term-level functions cannot pattern-match on types. So, while the @a is repeated in the pattern as written above, GHC does not, when matching a pattern, check that these are the same. In fact, they have to be the same if the function argument is well-typed. On the other hand, type family equations *can* branch based solely on kind information, making the repeated variable semantically important. Interesting, I wasn't aware this was possible. I agree that if it's possible to branch solely on kind info, then they should be taken into account for the linearity check. Do you perhaps have an example of how to do this sort of branching? Thanks, Dominique ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Repeated variables in type family instances
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 e...@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,
RE: Repeated variables in type family instances - UndecidableInstances
In an attempt to dredge out the mud from these waters, I have updated the wiki page at http://hackage.haskell.org/trac/ghc/wiki/NewAxioms to have the correct details about the current implementation (which has been merged with HEAD). A few salient points: * Open (normal, old-fashioned) type families are essentially unchanged. In particular, coincident overlap and non-linear patterns *are* allowed. * The overlap check between open type family instances now does a unification without an occurs check to mark (x, x) and ([y], y) as overlapping, as necessary for type soundness. * Coincident overlap within closed families works just fine, the way you might expect. In particular, in both the theory and the implementation, any set of type instances you could write in an open family can be combined in a closed family, and they will behave in exactly the same way. This is a marked improvement over the last implementation. As for AntC's finer-grained UndecidableInstances: I think that would be great, too. In general, I'm of the opinion that the brutal termination checker could use some improvements. But, there's little incentive to do so, with the ease of just saying UndecidableInstances. Even then, though, some reasonable type-level computations really don't terminate in all cases (division) and these still have a role to play. Richard PS: Sorry to those of you who have used type instance where and now find that your code doesn't compile. We (Simon, Dimitrios, and I) put a good deal of thought into the original design. But, we really liked the new one more. Given that the feature never made it into a released GHC, we thought it was OK to make this breaking change before it became impossible. Note that you can simulate the openness of type instance where by using an open family with closed family helpers. -Original Message- From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell- users-boun...@haskell.org] On Behalf Of AntC Sent: 24 June 2013 03:59 To: glasgow-haskell-users@haskell.org Subject: Re: Repeated variables in type family instances - UndecidableInstances Richard Eisenberg eir at cis.upenn.edu writes: ... The plan of action is to use the check labeled (B) on the wiki page. This check does *not* ban all nonlinear type families. Thanks Richard, great! Then the focus of attention moves to infinite types. I don't think anybody intentionally wants infinite types, so UndecidableInstances ought to be switched off, to catch unintended instances. But often there's a need for one or two instances to break the coverage conditions. (For example one of Oleg's standard techniques is to introduce a 'helper class' that has the same parameters as the based-on class, plus some extra parameter that drives instance selection, and is computed from the types of the arguments. It's not easy to see at this stage how that technique will translate into 'closed type families'.) The trouble with the UndecidableInstances flag is that it's a very blunt instrument module-wide. A 'nice to have' would be to make it finer-grained: - set Undecidableness on a per-instance or per-family basis. - or even: validate that the RHS of this instance uses a decidable family but allow the RHS to break cover compared to LHS (OK, I know that for a 'decidable' family there could be instances declared in other modules that get compiled with a different flag setting. But with 'closed type families', that can't happen, right?) AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Repeated variables in type family instances
Interesting points you make here. See my comments below: -Original Message- From: dominique.devri...@gmail.com [mailto:dominique.devri...@gmail.com] On Behalf Of Dominique Devriese [snip] 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? The nub of the difference is that type families can pattern-match on kinds, whereas term-level functions cannot pattern-match on types. So, while the @a is repeated in the pattern as written above, GHC does not, when matching a pattern, check that these are the same. In fact, they have to be the same if the function argument is well-typed. On the other hand, type family equations *can* branch based solely on kind information, making the repeated variable semantically important. Another salient difference is that pattern-matching on the term level desugars to case statements internally, whereas pattern-matching at the type level does not. It is conceivable that a clever check could fix this problem and disallow dangerous non-linearity at the type level while still allowing benign non-linearity. But, we seem to have found a consistent approach that doesn't bother with linearity, anyway. 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... I think this would really lower the expressiveness of type-level computation, and I'm not sure what the gain would be. I, too, like type-level things to mimic term-level things, but in the end, the type world and the term world are very different places with different needs. (Specifically, type-level things need to be reasoned about at compile time to ensure type safety, and term level things need to be able to run in an executable.) I recognize that the difference cause problems with things that want to be share between the worlds (such as singletons), but in my opinion, that's not a good enough reason to disallow non-linearity altogether. 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... Yes, we're busy on it now. It turns out that the proof that all of this is type-safe is... well... interesting. A draft should be online in the next few weeks, and I'll add links from the wiki, etc. P.S.2: On an unrelated note: will you also do a completeness check on closed type family definitions? There is no plan for this, no. In the presence of non-linear equations, I'm not sure off the top of my head how I would do this. Richard 2013/5/29 Richard Eisenberg e...@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
Re: Repeated variables in type family instances - UndecidableInstances
Richard Eisenberg eir at cis.upenn.edu writes: ... The plan of action is to use the check labeled (B) on the wiki page. This check does *not* ban all nonlinear type families. Thanks Richard, great! Then the focus of attention moves to infinite types. I don't think anybody intentionally wants infinite types, so UndecidableInstances ought to be switched off, to catch unintended instances. But often there's a need for one or two instances to break the coverage conditions. (For example one of Oleg's standard techniques is to introduce a 'helper class' that has the same parameters as the based-on class, plus some extra parameter that drives instance selection, and is computed from the types of the arguments. It's not easy to see at this stage how that technique will translate into 'closed type families'.) The trouble with the UndecidableInstances flag is that it's a very blunt instrument module-wide. A 'nice to have' would be to make it finer-grained: - set Undecidableness on a per-instance or per-family basis. - or even: validate that the RHS of this instance uses a decidable family but allow the RHS to break cover compared to LHS (OK, I know that for a 'decidable' family there could be instances declared in other modules that get compiled with a different flag setting. But with 'closed type families', that can't happen, right?) AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Repeated variables in type family instances
Richard Eisenberg eir at cis.upenn.edu writes: 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! Thank you Richard, I'll take comfort in that. I'd beware this though: the Nonlinearity wikipage says a medium-intensity search did not find any uses of nonlinear ... family instances in existing code, ... That doesn't surprise me, but I wouldn't put much weight on it. The main purpose of repeated tyvars in a (class) instance is so that you can have a 'wider' overlapping instance with distinct tyvars (and a non-congruent result). Since family instances don't currently support non-congruent overlap, I guess there would be a pent-up demand to translate class instances to (branched?) family instances with repeated tyvars. Here's two example instance from HList that mirror your two instances for family F: -- pattern of instance F x x class TypeEq a b c| a b - c instance TypeEq x x HTrue instance (c ~ HFalse) = TypeEq x y c -- pattern of instance F [x] x -- actually F x (HCons x ...) class Has e l-- constraint instance Has e (HCons e l') instance (Has e l') = Has e (HCons e' l') I haven't, though, seen those two patterns appearing as instances of the same class. And given that those patterns are to be allowed only within branched instances, the 'cleaned up syntax' makes sense -- I'm glad I suggested it! (see http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage#Suggestio ns, under 'Idiom of a total function' ;-) It still seems mildly 'unfair' to ban repeated tyvars when really the cause of the problem is infinite types. I take you to be saying that as soon as we allow UndecidableInstances, it's just too hard to guard against infinite types appearing from chains of instances, possibly in 'distant' imports or recursive module references. So I understand it's not worth sacrificing type safety. AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Repeated variables in type family instances
Ah -- I think the waters have been muddied somewhat as our thoughts have evolved. The plan of action (of history, at this point -- I merged into HEAD yesterday) is to use the check labeled (B) on the wiki page. This check does *not* ban all nonlinear type families. It just makes certain combinations of standalone instances conflict. Equations in closed type families (the new name for branched instances, which I'm trying to avoid saying) do not have any of these restrictions. And, many thanks for pointing out your contribution to that discussion page. I met with Simon PJ and Dimitrios V last summer to discuss this feature, and we went through the possibilities and settled on type instance where. We're all now busy writing up a paper on the design and type safety ramifications, and we switched gears to type family … where because it made for a more consistent feature, in our eyes. I'm really happy with where this ended up, so thanks for making the suggestion originally! Richard On Jun 22, 2013, at 10:28 AM, AntC wrote: Richard Eisenberg eir at cis.upenn.edu writes: 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! Thank you Richard, I'll take comfort in that. I'd beware this though: the Nonlinearity wikipage says a medium-intensity search did not find any uses of nonlinear ... family instances in existing code, ... That doesn't surprise me, but I wouldn't put much weight on it. The main purpose of repeated tyvars in a (class) instance is so that you can have a 'wider' overlapping instance with distinct tyvars (and a non-congruent result). Since family instances don't currently support non-congruent overlap, I guess there would be a pent-up demand to translate class instances to (branched?) family instances with repeated tyvars. Here's two example instance from HList that mirror your two instances for family F: -- pattern of instance F x x class TypeEq a b c| a b - c instance TypeEq x x HTrue instance (c ~ HFalse) = TypeEq x y c -- pattern of instance F [x] x -- actually F x (HCons x ...) class Has e l-- constraint instance Has e (HCons e l') instance (Has e l') = Has e (HCons e' l') I haven't, though, seen those two patterns appearing as instances of the same class. And given that those patterns are to be allowed only within branched instances, the 'cleaned up syntax' makes sense -- I'm glad I suggested it! (see http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage#Suggestio ns, under 'Idiom of a total function' ;-) It still seems mildly 'unfair' to ban repeated tyvars when really the cause of the problem is infinite types. I take you to be saying that as soon as we allow UndecidableInstances, it's just too hard to guard against infinite types appearing from chains of instances, possibly in 'distant' imports or recursive module references. So I understand it's not worth sacrificing type safety. AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Repeated variables in type family instances
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 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Repeated variables in type family instances
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 F.tgz Description: Binary data ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Repeated variables in type family instances
(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
