Non-dependent, irrelevant, nameless arguments aren't accepted in arrows

[andy-morris]

(Agda 2.6.1)

These are all accepted:

_ : A → B → A
_ : A → {B} → A
_ : A → .B → A
_ : A → .{_ : B} → A

But this is rejected with {B} cannot appear by itself:

_ : A → .{B} → A

[gallais]

Self-contained file:

module untypedbinding (A B : Set) where

_ : A → B → A
_ = {!!}

_ : A → {B} → A
_ = {!!}

_ : A → .B → A
_ = {!!}

_ : A → .{_ : B} → A
_ = {!!}

_ : A → .{B} → A
_ = {!!}

[andreasabel]

The fix 3a7316e also includes the case {.B} -> A.