好吧，你可以使用一个可怕的CPP黑客：

{-# LANGUAGE CPP #-}
#define Absurd      = \case {}

f :: X1 :~: X2 -> Void
f Absurd   -- expands to "f = case {}"

但是，如果您正在寻找一个使用纯Haskell语法的解决方案，我敢肯定答案是否定的。与空case不同，您不能使用模式语法定义f，而至少没有一个模式。而且，没有GHC认为是无人居住类型术语的密码的模式。（即使有，也没有语法允许您定义没有右侧的f pat。）

这里是一个使用模式同义词的尝试。它并不完全令人满意，可能不是你真正想要的。它只在移动\case{}远离你的眼睛。我们仍然需要在某些点上使用absurd。

{-# LANGUAGE PatternSynonyms, ViewPatterns, GADTs #-}
{-# LANGUAGE DataKinds, EmptyCase, LambdaCase, TypeOperators #-}

import Data.Type.Equality
import Data.Void

data X = X1 | X2

pattern Abs :: Void -> a
pattern Abs x <- (\case{} -> x)

f :: 'X1 :~: 'X2 -> Void
f (Abs x) = x

g :: 'X1 :~: 'X2 -> a
g (Abs x) = absurd x

{-
    Pattern match(es) are non-exhaustive
    In an equation for `h':
        Patterns of type 'X1 :~: 'X1 not matched: Refl
-}
h :: 'X1 :~: 'X1 -> Void
h (Abs x) = x

另一种方法是利用Template Haskell。

我想如果你想模仿这一点，最简单的方法就是类似于在评论中贴出一个答案：

f _ = undefined

然而，这是懒惰：

f (error "aw beans")  -- undefined

而空格则是严格的：

(\ case {} :: X1 :~: X2 -> Void) (error "aw beans")  -- beans

因此，更好的替代方法是使用seq：

impossible :: a -> Void
impossible x = x `seq` impossible x

或者BangPatterns：

{-# Language BangPatterns #-}

impossible :: a -> Void
impossible !x = impossible x

因此，你可以直接写f = impossible，这对我来说似乎很好。（a上的量词在逻辑上更像是“for any”，而不是“for all”。）当然，你可以抛出一些更具描述性的东西，而不是进入一个无限循环，以防这种情况实际上不是不可能的-error "the impossible was possible after all"。
这也适用于void包中Void的老式定义data Void = Void !Void或newtype Void = Void Void。