RE: Allowing (Char ~ Bool => Void)?

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@haskell.org [mailto:glasgow-haskell- | users-bounces@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 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@haskell.org | > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users | > | | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users