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

Reply via email to