Allowing (Char ~ Bool => Void)?

Fri Apr 5 16:19:26 CEST 2013

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