Write a function with an empty case without case-CodePudding

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 ???

CodePudding user response：

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.)

CodePudding user response：

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.