On Sun, Mar 24, 2013 at 10:49:24AM -0400, Richard Eisenberg wrote:

Though I've never run into the problem Shachaf mentions, this certainly seems useful. However, when testing Shachaf's code, I get the same error that I get when writing an impossible branch of a case statement. I imagine that the same code in GHC powers both scenarios, so any change would have to be careful to preserve the case-branch behavior, which (I think) is useful.

Perhaps a general solution to this problem is to have some new term construct "contra" (supply a better name please!) that can be used only when there is an inconsistent equality in the context but can typecheck at any type. With "contra", we could allow impossible case branches, because now there would be something sensible to put there. This would be an alternate effective solution to long-standing bug #3927, which is about checking exhaustiveness of case matches.

+1 for contra. Alternative name suggestions: 'exfalso', 'shazam', 'pizza'. -Brent

On Mar 24, 2013, at 5:16 AM, Shachaf Ben-Kiki wrote:

...

Is there a good reason that GHC doesn't allow any value of type (Char ~ Bool => Void), even undefined?

There are various use cases for this. It's allowed indirectly, via GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x of {}" (with EmptyCase in HEAD) -- but not directly.

One thing this prevents, for instance, is CPSifying GADTs:

data Foo a = a ~ Char => A | a ~ Bool => B -- valid newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~ Bool => r) -> r } -- unusable

Trying to use a type like the latter in practice runs into problems quickly because one needs to provide an absurd value of type (Char ~ Bool => r), which is generally impossible (even if we're willing to cheat with ⊥!). It seems that this sort of thing should be doable.

Shachaf

_______________________________________________ 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

I would call this more of an idea than a proposal -- I'm not advocating that it's necessarily the right thing, but one possible solution both to Shachaf's original question and the problem of spurious warnings about bogus case branches. The idea is to introduce some new keyword, which I've called "contra", which has the type (a ~ b) => c, where a cannot unify with b (and c is totally unconstrained). Currently, whenever such an equality (a ~ b) is in the context, GHC issues an error and prevents any further code. This is often good behavior of a compiler, to prevent people from writing impossible code. However, Shachaf found a case where it would be nice to have code that executes in an inconsistent context. And, if we had contra, then we could just stick contra in any inconsistent pattern matches, and there would be no need to fix the warnings about incomplete pattern matches. For example:

data Nat = Zero | Succ Nat data SNat :: Nat -> * where SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n)

safePred :: SNat (Succ n) -> SNat n safePred (SSucc n) = n safePred SZero = contra

(Seeing the code here, perhaps "impossible" is a better name.) The last clause of safePred is indeed impossible. GHC issues an error on the code above. If we remove the last line, GHC (rightly) does not issue a warning about an incomplete pattern match. But, as documented on Trac #3927, there are other places where GHC does issue a warning about missing impossible branches. With contra, we could fill out such pattern matches and suppress the warning. When I initially wrote up my "contra" idea, I was remembering a case where GHC did not issue a warning on an inconsistent pattern match. In the process of writing this email, I found that old case, and I realized that it was my fault, not GHC's. I had originally thought that GHC's "impossible code" identification feature was incomplete, but now perhaps I was wrong. If GHC can always detect impossible code, the "contra" idea is less appealing than it once was to me, though it would still solve Shachaf's problem. Does this clarify the idea? Richard On Apr 3, 2013, at 1:49 PM, Simon Peyton-Jones wrote:

What precisely is the proposal here? That "unreachable code" be a warning rather than an error?

Would you care to make a ticket with a clear specification? Thanks!

Simon

| -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Richard Eisenberg | Sent: 24 March 2013 14:49 | To: Shachaf Ben-Kiki | Cc: glasgow-haskell-users | Subject: Re: Allowing (Char ~ Bool => Void)? | | Though I've never run into the problem Shachaf mentions, this certainly | seems useful. However, when testing Shachaf's code, I get the same error | that I get when writing an impossible branch of a case statement. I | imagine that the same code in GHC powers both scenarios, so any change | would have to be careful to preserve the case-branch behavior, which (I | think) is useful. | | Perhaps a general solution to this problem is to have some new term | construct "contra" (supply a better name please!) that can be used only | when there is an inconsistent equality in the context but can typecheck | at any type. With "contra", we could allow impossible case branches, | because now there would be something sensible to put there. This would | be an alternate effective solution to long-standing bug #3927, which is | about checking exhaustiveness of case matches. | | Richard | | On Mar 24, 2013, at 5:16 AM, Shachaf Ben-Kiki wrote: | | > Is there a good reason that GHC doesn't allow any value of type (Char | > ~ Bool => Void), even undefined? | > | > There are various use cases for this. It's allowed indirectly, via | > GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x | > of {}" (with EmptyCase in HEAD) -- but not directly. | > | > One thing this prevents, for instance, is CPSifying GADTs: | > | > data Foo a = a ~ Char => A | a ~ Bool => B -- valid | > newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~ | > Bool => r) -> r } -- unusable | > | > Trying to use a type like the latter in practice runs into problems | > quickly because one needs to provide an absurd value of type (Char ~ | > Bool => r), which is generally impossible (even if we're willing to | > cheat with ⊥!). It seems that this sort of thing should be doable. | > | > Shachaf | > | > _______________________________________________ | > 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

On Apr 5, 2013, at 3:10 AM, Simon Peyton-Jones wrote:

I suppose you could have a magic constraint INSOLUBLE, say, with contra :: INSOLUBLE => c which had the effect of suppressing any enclosing "impossible branch" failure error reports.

That's *exactly* what I meant -- sorry if I was unclear.

It's not clear how far out it would go. What about safePred SZero = if ... then contra else True or safePred SZero = case .. of { ...some other GADT matching… }

I think to have a consistent system, we would have to allow these, too. That's silly perhaps, but it's not dangerous and it wouldn't break anything. We could even imagine a new language flag that suppresses the "impossible code" error, and then it's up to the programmer to figure out what code is impossible and what isn't.

I can't say I'm enthusiastic here.

To be fair, neither am I. This was just one idea of a way to proceed. I'm happy to consider this idea abandoned.

I WOULD like someone to help beef up the pattern-match overlap detector in the desugarer. That would be really useful.

Simon

| -----Original Message----- | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | Sent: 03 April 2013 19:59 | To: Simon Peyton-Jones | Cc: Shachaf Ben-Kiki; glasgow-haskell-users | Subject: Re: Allowing (Char ~ Bool => Void)? | | I would call this more of an idea than a proposal -- I'm not advocating | that it's necessarily the right thing, but one possible solution both to | Shachaf's original question and the problem of spurious warnings about | bogus case branches. | | The idea is to introduce some new keyword, which I've called "contra", | which has the type (a ~ b) => c, where a cannot unify with b (and c is | totally unconstrained). Currently, whenever such an equality (a ~ b) is | in the context, GHC issues an error and prevents any further code. This | is often good behavior of a compiler, to prevent people from writing | impossible code. However, Shachaf found a case where it would be nice to | have code that executes in an inconsistent context. And, if we had | contra, then we could just stick contra in any inconsistent pattern | matches, and there would be no need to fix the warnings about incomplete | pattern matches. | | For example: | | > data Nat = Zero | Succ Nat | > data SNat :: Nat -> * where | > SZero :: SNat Zero | > SSucc :: SNat n -> SNat (Succ n) | > | > safePred :: SNat (Succ n) -> SNat n | > safePred (SSucc n) = n | > safePred SZero = contra | | (Seeing the code here, perhaps "impossible" is a better name.) | | The last clause of safePred is indeed impossible. GHC issues an error on | the code above. If we remove the last line, GHC (rightly) does not issue | a warning about an incomplete pattern match. But, as documented on Trac | #3927, there are other places where GHC does issue a warning about | missing impossible branches. With contra, we could fill out such pattern | matches and suppress the warning. | | When I initially wrote up my "contra" idea, I was remembering a case | where GHC did not issue a warning on an inconsistent pattern match. In | the process of writing this email, I found that old case, and I realized | that it was my fault, not GHC's. I had originally thought that GHC's | "impossible code" identification feature was incomplete, but now perhaps | I was wrong. If GHC can always detect impossible code, the "contra" idea | is less appealing than it once was to me, though it would still solve | Shachaf's problem. | | Does this clarify the idea? | | Richard | | On Apr 3, 2013, at 1:49 PM, Simon Peyton-Jones | wrote: | | > What precisely is the proposal here? That "unreachable code" be a | warning rather than an error? | > | > Would you care to make a ticket with a clear specification? Thanks! | > | > Simon | > | > | -----Original Message----- | > | From: glasgow-haskell-users-bounces@haskell.org | > | [mailto:glasgow-haskell- users-bounces@haskell.org] On Behalf Of | > | Richard Eisenberg | > | Sent: 24 March 2013 14:49 | > | To: Shachaf Ben-Kiki | > | Cc: glasgow-haskell-users | > | Subject: Re: Allowing (Char ~ Bool => Void)? | > | | > | Though I've never run into the problem Shachaf mentions, this | > | certainly seems useful. However, when testing Shachaf's code, I get | > | the same error that I get when writing an impossible branch of a | > | case statement. I imagine that the same code in GHC powers both | > | scenarios, so any change would have to be careful to preserve the | > | case-branch behavior, which (I | > | think) is useful. | > | | > | Perhaps a general solution to this problem is to have some new term | > | construct "contra" (supply a better name please!) that can be used | > | only when there is an inconsistent equality in the context but can | > | typecheck at any type. With "contra", we could allow impossible case | > | branches, because now there would be something sensible to put | > | there. This would be an alternate effective solution to | > | long-standing bug #3927, which is about checking exhaustiveness of | case matches. | > | | > | Richard | > | | > | On Mar 24, 2013, at 5:16 AM, Shachaf Ben-Kiki | wrote: | > | | > | > Is there a good reason that GHC doesn't allow any value of type | > | > (Char ~ Bool => Void), even undefined? | > | > | > | > There are various use cases for this. It's allowed indirectly, via | > | > GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case | > | > x of {}" (with EmptyCase in HEAD) -- but not directly. | > | > | > | > One thing this prevents, for instance, is CPSifying GADTs: | > | > | > | > data Foo a = a ~ Char => A | a ~ Bool => B -- valid | > | > newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a | > | > ~ Bool => r) -> r } -- unusable | > | > | > | > Trying to use a type like the latter in practice runs into | > | > problems quickly because one needs to provide an absurd value of | > | > type (Char ~ Bool => r), which is generally impossible (even if | > | > we're willing to cheat with ⊥!). It seems that this sort of thing | should be doable. | > | > | > | > Shachaf | > | > | > | > _______________________________________________ | > | > 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 | >