I appreciate your response here, though I do question your dependent function isEven. How is a function type (IsEven n -> Void) a proof that "n is even" is absurd? The Void return type is uninhabited but that doesn't require that IsEven n be absurd, that could also be the result of an infinite loop or program abort. More generally in Rust the equivalent function here I'd interpret as "this function doesn't ever return". I'd feel slightly better about a function that was the equivalent of fn (IsEven) -> T because that one says "if you give me an IsEven n then I can give you anything" which is closer to the notion of absurdity than an uninhabited type, though I don't know how to write this in Haskell and of course you can't actually write that in Rust (you'd have to make isEven itself generic instead).