如何在类型级别清空大小写

使用EmptyCase，可以实现以下功能：

{-# LANGUAGE EmptyCase, EmptyDataDecls #-}

data Void

absurd :: Void -> a
absurd v = case v of

使用DataKinds，数据类型可以提升到种类级别（它们的构造函数被提升为类型构造函数）。这也适用于无人居住的数据类型Void。

这里的问题是是否有办法absurd为无人居住的种类写出等价物：

tabsurd :: Proxy (_ :: Void) -> a
tabsurd = _

这实际上是一种“EmptyCase在类型级别”的形式。在合理范围内，您可以随意替换Proxy为一些其他合适的类型（例如TypeRep）。

注：据我所知，我只能求助于error或类似不安全的技术在这里，但我想看看有没有办法做到这一点，就不会，如果类型不无人居住工作。所以对于我们提出的任何技术，都不应该使用相同的技术来实现以下功能：

data Unit = Unit

notsoabsurd :: Proxy (_ :: Unit) -> a
notsoabsurd = _