Re: Allowing (Char ~ Bool => Void)?

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