Allowing (Char ~ Bool => Void)?

[Richard Eisenberg]

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 <simonpj at microsoft.com> 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 at haskell.org [mailto:glasgow-haskell-
> | users-bounces at 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 <shachaf at gmail.com> 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 at haskell.org
> | > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> | >
> | 
> | 
> | _______________________________________________
> | Glasgow-haskell-users mailing list
> | Glasgow-haskell-users at haskell.org
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>