Allowing (Char ~ Bool => Void)?

[Brent Yorgey]

On Sun, Mar 24, 2013 at 10:49:24AM -0400, Richard Eisenberg wrote:
> 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.

+1 for contra.  Alternative name suggestions: 'exfalso', 'shazam',
'pizza'.

-Brent



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