title: Can GADTs be used to prove type inequalities in GHC?
body: <p>So, in my ongoing attempts to half-understand Curry-Howard through small Haskell exercises, I've gotten stuck at this point:</p>
  
  <pre><code>{-# LANGUAGE GADTs #-}
  
  import Data.Void
  
  type Not a = a -&gt; 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 = ???
  </code></pre>
  
  <p>Clearly the type <code>Equal Int Char</code> has no (non-bottom) inhabitants, and thus semantically there ought to be an <code>absurdEquality :: Equal Int Char -&gt; a</code> function... but for the life of me I can't figure out any way to write one other than using <code>undefined</code>.</p>
  
  <p>So either:</p>
  
  <ol>
  <li>I'm missing something, or</li>
  <li>There is some limitation of the language that makes this an impossible task, and I haven't managed to understand what it is.</li>
  </ol>
  
  <p>I suspect the answer is something like this: the compiler is unable to exploit the fact that there are no <code>Equal</code> constructors that don't have a = b.  But if that is so, what makes it true?</p>