Entonces, en mis intentos continuos de entender a Curry-Howard a través de pequeños ejercicios de Haskell, me he quedado atascado en este punto:

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

Claramente el tipoEqual Int Char no tiene habitantes (no inferiores), y por lo tanto semánticamente debería haber unaabsurdEquality :: Equal Int Char -> a función ... pero por mi vida no puedo encontrar otra manera de escribir otra que no sea usarundefined.

Entonces, o bien:

Me falta algo, oExiste una limitación en el lenguaje que hace que esto sea una tarea imposible, y no he logrado entender de qué se trata.

Sospecho que la respuesta es algo así: el compilador no puede explotar el hecho de que no hayEqual Constructores que no tienen a = b. Pero si eso es así, ¿qué lo hace cierto?