No-fun/puzzlement with pattern synonyms as functions

Question

With PatternSynonyms (explicitly bidirectional form), the pattern-to-expr equations in effect form a function but spelled upper-case (providing you end up with an fully saturated data constr of the correct type). Then consider (at GHC 8.10.2)

{-# LANGUAGE  PatternSynonyms, ViewPatterns  #-}

data Nat = Zero | Succ Nat                deriving (Eq, Show, Read)

--  Pattern Synonyms as functions?

pattern Pred :: Nat -> Nat
pattern Pred n <- {- what goes here? -}           where
  Pred (Succ n) = n
pattern One           = Succ Zero

zero = Pred One                      -- shows as Zero OK

So what do I put for the pattern Pred n <- ??? value-to-pattern top line? Or can I just not use Pred n in a pattern match? What seems to work (but I don't understand why) is a view pattern

pattern Pred n <-  (Succ -> n)          where ...   -- seems to work, but why?

isZero (Pred One) = True
isZero _          = False

-- isZero (Pred One) ===> True ; isZero Zero ===> True
-- isZero (Succ One) ===> False; isZero One  ===> False

It looks sweet to use Pred as a pseudo-constructor/pattern here, because it's an injective function.

Answer 1

Consider this usage of your pattern synonym:

succ' :: Nat -> Nat
succ' (Pred n) = n

where the intent is, of course, to return the successor of the argument.

In this case it is clear that when the argument is, say, k, then variable n must be bound to Succ k. Given this intuition, we need to find a pattern that does exactly that, a pattern that could be used here instead of Pred n:

succ' :: Nat -> Nat
succ' ({- bind n to Succ k -}) = n

It turns out that your view pattern does exactly that. This would work just fine:

succ' :: Nat -> Nat
succ' (Succ -> n) = n

Consequently, we have to define

pattern Pred n <- (Succ -> n)

In my own (limited) experience, this is fairly idiomatic. When you have a bidirectional pattern synonym, you will often use a view pattern as done above.