Allowing (Char ~ Bool => Void)?

[Simon Peyton-Jones]

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