Pattern synonyms with named arguments can be defined but not used

[andreasabel]

Pattern synonyms with named arguments can be defined but not used

[andreasabel]

Apparently, named arguments in pattern lhss are already discarded (silently!) in the parser. The concrete syntax only has one name per lhs argument:

agda/src/full/Agda/Syntax/Concrete.hs

Line 481 in 3503636

| PatternSyn Range Name [Arg Name] Pattern

agda/src/full/Agda/Syntax/Parser/Parser.y

Lines 1369 to 1370 in 3503636

	PatternSynArgs :: { [Arg Name] }
	PatternSynArgs : DomainFreeBindings {% patternSynArgs $1 }

The culprit is then the patternSynArgs function in the parser:

agda/src/full/Agda/Syntax/Parser/Parser.y

Lines 2368 to 2378 in 3503636

	patternSynArgs :: [NamedArg Binder] -> Parser [Arg Name]
	patternSynArgs = mapM pSynArg
	where
	pSynArg x
	| let h = getHiding x, h `notElem` [Hidden, NotHidden] =
	abort $ prettyShow h ++ " arguments not allowed to pattern synonyms"
	| not (isRelevant x) =
	abort "Arguments to pattern synonyms must be relevant"
	| Just p <- binderPattern (namedArg x) =
	abort "Arguments to pattern synonyms cannot be patterns themselves"
	| otherwise = return $ fmap (boundName . binderName . namedThing) x

Named arguments were never supported in pattern synonym definitions; the initial implementation for hidden patsyn parameters only has an example for an unnamed hidden parameter: c935600

Agda < 2.6 rejects to parse them (correct behavior), Agda 2.6.0 and up parses them but can't use them (bad behavior). Thus, this is a regression in 2.6.0.

[andreasabel]

Agda also silently discards tactic attributes in pattern definitions:

open import Agda.Builtin.Nat
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

nothing : Term → TC ⊤
nothing hole = returnTC _

pattern p {@(tactic nothing) x} = suc x
-- Accepted, but should complain about tactics not being allowed in pattern synonyms

[andreasabel]

It should maybe also not allow erasure annotations in pattern synonyms...

{-# OPTIONS --erasure #-}

open import Agda.Builtin.Nat

pattern p (@0 x) = suc x
-- should be rejected!

pred : Nat → Nat
pred (p x) = x
pred zero  = zero