Allowing (Char ~ Bool => Void)?

[Richard Eisenberg]

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
>