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