What goes wrong if you were to allow matching against value/neutral forms of functions? Are there any good references on this?

HypotheticalFunMatching.agda

open import Data.Bool
open import Data.Nat
module HypotheticalFunMatching where

{-
Imagine that the expressions in the pattern positions are first evaluated to values/neutrals.
So for example, "not" really becomes elimBool and "_+_" becomes two nested elimℕ's.

A wildcard match is always necessary because there are infinitely many intentionally different
functions.
However if 2 expressions reduce to the same value/neutral form, then you get an error
for overlapping.
-}

match1 : (Bool → Bool) → Bool
match1 (λ b → not (not b)) = true
match1 (λ b → b) = false
match1 _ = false

match2 : (ℕ → ℕ → ℕ) → Bool
match2 (λ m n → m + n) = true
match2 (λ m n → n + m) = false
match2 _ = false

match3 : (ℕ → ℕ) → Bool
match3 (λ n → n + 0) = true
match3 (λ n → n) = false
-- below not allowed because it reduces to an overlapping neutral form
-- match3 (λ n → 0 + n) = true
match3 _ = false

Contradiction example by elliott in #agda, thanks!

http://paste.tryhaskell.org/5096125747794280448