I can write something impossible with an empty case, and use it with Decision, for example.
{-# LANGUAGE DataKinds, EmptyCase, LambdaCase, TypeOperators #-}
import Data.Type.Equality
import Data.Void
data X = X1 | X2
f :: X1 :~: X2 -> Void
f = \case {}
-- or
-- f x = case x of {}
Is there a way to write the equivalent without using case by directly pattern-matching the parameter?
f :: X1 :~: X2 -> Void
f ???
Well, you can use a horrible CPP hack:
{-# LANGUAGE CPP #-}
#define Absurd = \case {}
f :: X1 :~: X2 -> Void
f Absurd -- expands to "f = case {}"
However, if you're looking for a solution using pure Haskell syntax, I'm pretty sure the answer is no. Unlike with an empty case, you can't define f using pattern syntax without at least one pattern. And, there's no pattern that GHC understands as secret code for a term of uninhabited type. (Even if there was, there's no syntax that allows you define an f pat without a right-hand side.)
Here's an attempt using pattern synonyms. It is not completely satisfactory and probably not what you really want. It only achieves in moving the \case{} away from your eye. We still need to use absurd in some points.
{-# 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
Another alternative could be exploiting Template Haskell.
I think if you want to imitate this, the simplest way is akin to an answer posted in the comments:
f _ = undefined
However, this is lazy:
f (error "aw beans") -- undefined
While the empty case is strict:
(\ case {} :: X1 :~: X2 -> Void) (error "aw beans") -- beans
So a better replacement would use seq:
impossible :: a -> Void
impossible x = x `seq` impossible x
Or BangPatterns:
{-# Language BangPatterns #-}
impossible :: a -> Void
impossible !x = impossible x
Whereupon you can just write f = impossible, which seems pretty good to me. (The quantifier on a is logically more like “for any” than “for all”, but oh well.) You could of course throw something slightly more descriptive instead of going into an infinite loop in case the situation isn’t actually impossible—error "the impossible was possible after all".
This should also work with the old-fashioned definition of Void as data Void = Void !Void or newtype Void = Void Void in the void package.
g :: X1 :~: X1 -> Void. I can no longer take advantage of it with this definition.
LambdaCase is about as short as it gets. At best you can make this more tolerant of code motion by repeating the intended type argument, impossible @(X1 :~: X2).
f _ = undefinedwork?undefinedto use an empty case. So I'd like to know how I can write it withoutundefined.Data.Void.absurdis also defined usingcase x of {}.)casenormally has one or more branches; generalizing to zero branches (because no pattern could match) still leaves thecase ... ofheader, so there's something to write to indicate that's what you want to do. But function definition syntax has you write an equation for each branch, so zero branches should mean zero equations, leaving nothing at all! But that can't be told apart from just not having implemented the function yet.