How can I use contradictory evidence?

While writing about how to do subtyping in Haskell, it occurred to me that it would be very convenient to be able to "use" contradictory evidence such as True ~ False to inform the compiler about dead branches. With another standard empty type, Void, the EmptyCase extension allows you to mark a dead branch (i.e. one that contains a value of type Void) this way:

use :: Void -> a
use x = case x of

I'd like to do something similar for unsatisfiable Constraints.

Is there a term which can be given the type True ~ False => a but cannot be given the type a?

Solution

You can often do this by separating the exact nature of the evidence from the way you plan to use it. If the type checker sees that you've introduced an absurd constraint, it will bark at you. So the trick is to delay that equality behind :~:, and then to manipulate the equality evidence using generally reasonable functions.

{-# LANGUAGE GADTs, TypeOperators, ScopedTypeVariables, DataKinds,
      PolyKinds, RankNTypes #-}
{-# OPTIONS_GHC -Wall #-}

module TrueFalse where
import Data.Type.Equality

data Foo (a :: Bool) where
  Can :: Foo 'False
  Can't :: (forall x . x) -> Foo 'True

extr :: Foo 'True -> a
extr (Can't x) = x

subst :: a :~: b -> f a -> f b
subst Refl x = x

whoop :: 'False :~: 'True -> a
whoop pf = extr $ subst pf Can

The whoop function seems to be approximately what you're looking for.

As András Kovács commented, you could even just use EmptyCase on the 'False :~: 'True value, e.g. by writing whoop = \case (yes, that's the whole equation!). At present (7.10.3), unfortunately, EmptyCase doesn't warn about non-exhaustive matches. This will hopefully be fixed soon.

Update 2019: that bug has been fixed.