In practice yes, so when you try to execute the function that accepts `Void`, that will error out. But there is no reason to not compile it because it will never actually execute. This may sound unpractical but quite the contrary it's very useful. For instance, it's used to model functions that panics in Rust (https://doc.rust-lang.org/reference/types/never.html). That way you can have a function called `todo` which fails when executed, but keeps the type checker happy until you actually implement it.

Right, it's very useful for lots of reasons, one being that any construct that actually tries to use a Void return value or construct a parameter value will be rejected at compile time.

What I am really curious about is whether there's any uses of `absurd :: Void -> a` in the wild. I guess it's a top type for arbitrary functions, though I'm not sure how useful that is in itself...