How to EmptyCase at the type level

Question

Using EmptyCase, it is possible to implement the following function:

{-# LANGUAGE EmptyCase, EmptyDataDecls #-}

data Void

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

With DataKinds, data types can be promoted to the kind level (their constructors are promoted to type constructors). This works for uninhabited data types like Void as well.

The question here is whether there is a way to write the equivalent of absurd for an uninhabited kind:

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

This would effectively be a form of "EmptyCase at the type level". Within reason, feel free to substitute Proxy with some other suitable type (e.g. TypeRep).

NB: I understand that I can just resort to error or similar unsafe techniques here, but I want to see if there's a way to do this that would not work if the type wasn't uninhabited. So for whatever technique we come up with, it should not be possible to use the same technique to inhabit the following function:

data Unit = Unit

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

Answer 1

The type-level equivalent of pattern-matching is type classes (well, also type families, but they don't apply here, since you want a term-level result).

So you could conceivably make tabsurd a member of a class that has an associated type of kind Void:

class TAbsurd a where
  type TAbsurdVoid a :: Void
  tabsurd :: a

Here, tabsurd will have type signature tabsurd :: TAbsurd a => a, but if you insist on a Proxy, you can obviously easily convert one to the other:

pabsurd :: TAbsurd a => Proxy a -> a
pabsurd _ = tabsurd

So calling such function or using it in any other way would presumably be impossible, because you can't implement class TAbsurd a for any a, because you can't provide the type TAbsurdVoid a.

---

According to your requirement, the same approach does work fine for Unit:

data Unit = Unit

class V a where
  type VU a :: Unit
  uabsurd :: a

instance V Int where
  type VU Int = 'Unit
  uabsurd = 42

---

Keep in mind however that in Haskell, any kind (including Void) is potentially inhabited by a non-terminating type family. For example, this works:

type family F a :: x

instance TAbsurd Int where
  type TAbsurdVoid Int = F String
  tabsurd = 42

However, this limitation is akin to any type (including Void) being inhabited by the value undefined at term level, so that you can actually call absurd like this:

x = absurd undefined

The difference with type level is that you can actually call function tabsurd (given the instance above) and it will return 42:

print (tabsurd :: Int)

This can be fixed by having tabsurd return not a, but a Proxy (TAbsurdVoid a):

class TAbsurd a where
  type TAbsurdVoid a :: Void
  tabsurd :: Proxy (TAbsurdVoid a)