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 Constraint
s.
Is there a term which can be given the type True ~ False => a
but cannot be given the type a
?
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.