Allowing (Char ~ Bool => Void)?

[Simon Peyton-Jones]

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

So you do not mean
	contra :: forall abc. (a~b) => c
(where obviously a and b will unify).  You mean rather
	contra :: forall c. (Int ~ Bool) => c
or something like that.

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

This part I don't understand *at all*!  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

From the last equation we get the constraint

	(Zero ~ Succ n) => (Int ~ Bool)

(assuming my type for contra). The presence of an insoluble contraint after the => does not make it the slightest bit easier to suppress the error that current arises from the insoluble given constraint before the =>.

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.  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 can't say I'm enthusiastic here.


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