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