Curry-Howard, void, and type checking in Haskell
I would find a different tutorial because the author of that one is fundamentally confused. They wrongly claim that $\neg a$ and $\bot\to a$ are equivalent ($a\to\bot$ would be correct), and also wrongly claim that you can't write a function of type $\texttt{Void}\to a$.
$\texttt{Void}\to a$ is vacuously true. In principle a function of that type should require no definition at all because the number of cases for which you need to define it is zero. GHC doesn't accept that, but (with -XEmptyCase) it does accept
f :: Void -&gt; a
f x = case x of {}

which is a perfectly valid, logically sound definition.

Why does the Haskell compiler approve the type of proposition?

The proposition as written in the Haskell code is actually true. The proof is invalid though since it uses $\texttt{undefined}$.
If you replaced the right hand side with $(b\to\texttt{Void},a)$ then it would be false, but you could still &quot;prove&quot; it using $\texttt{undefined}$; in fact you could just write $\texttt{proposition} = \texttt{undefined}$ and the type checker would accept that. It would also accept $\texttt{proposition} = \texttt{proposition}$. If you want to use Haskell as a Curry-Howard sandbox you have to take care that your code doesn't throw an exception or fail to terminate, because the compiler won't catch those errors.

Response to edit: your proof is correct but it can be simplified. In the first case, there's no need to create a function and immediately apply it to one of its arguments. Instead of (\z1 z2 -&gt; z1) x you can write \z2 -&gt; x, or \_ -&gt; x since the argument/premise isn't used. In the second case, you don't need to prove b -&gt; a since you already have g :: b -&gt; a. The simplified proof is
proposition (Left x, _) = Right (\_ -&gt; x)
proposition (Right g, _) = Right g

In addition to the pitfalls that Dan Doel mentioned in a comment, missing cases are another thing to watch out for. GHC by default doesn't even warn about them. With -Werror=incomplete-patterns it will refuse to accept programs with missing cases.
You can prove negations. You need to return a value of type $\texttt{Void}$, which you can't create yourself but you can get from elsewhere. For example here's a proof of $((P\Rightarrow Q) \mathbin{\&amp;} \neg Q)\Rightarrow \neg P$:
f :: (a -&gt; b, b -&gt; Void) -&gt; (a -&gt; Void)
f (x, y) = \z -&gt; y (x z)

You may reasonably wonder where your caller got the value of type $\texttt{Void}$, but that's the caller's problem, not yours. Deriving a contradiction in a subproof doesn't mean the logic is inconsistent, it just means you've shown that you'll never actually reach this point in the real world.