How can I use contradictory evidence?

Question

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?

Answer 1

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

Answer 2

Such a constraint will cause a type error if it ever appears as a given constraint. In general, this applies to any constraint the typechecker deems impossible.

Even writing a function

f :: ('True ~ 'False) => x
f = undefined 

does not typecheck, because the context of a function is a given constraint in the body of the function - and 'True ~ 'False simply cannot appear as a given constraint.

At best you could have e.g.

import Data.Type.Equality ((:~:)(..))

type family (==) (a :: k) (b :: k) :: Bool where 
  a == a = 'True 
  a == b = 'False 

f :: ((x == y) ~ 'False) => x :~: y -> a
-- f Refl = undefined -- Inaccessible code 
f = \case{} 

which again comes back to an EmptyCase, this time on the :~:. Note that

f :: ((x == y) ~ 'False, x ~ y) => a 

also reduces to a trivially impossible constraint, because x == x reduces to True. You could write an equality predicate which doesn't reduce for trivially equal types (e.g. the one in Data.Type.Equality), which allows you to write:

import Data.Type.Equality 

f :: ((x == y) ~ 'False, x ~ y) => Proxy '(x,y) -> a 
f = undefined 

There may be a way to write this function without undefined but it is sort of moot anyways since this type is immediately reduced by GHC:

>:t f
f :: forall (k :: BOX) (y :: k) a. ((y == y) ~ 'False) => Proxy '(y, y) -> a

Even without the constraint there, it is definitionally impossible to call the function Proxy '(y,y) -> a with two different types. There is no way to hide an equality constraint ~ from the typechecker - you must use a different form of equality, one which does not reduce to ~.