Agda: How usual/curly braces are used relative to each other and to ':' sign

while

data _≡_ :  ∀{a}{P : Set a} (x : P) →  P → Set a where
  refl :  x ≡ x

is not.

This example parses fine; the error is from scope checking:

Not in scope:
  x at ...
when scope checking x

This error is beyond the scope of this question. As you seem to be noticing, though, there is a lot of similarity between your two putative definitions of _≡_: the ∀ symbol tells the parser that what follows should parse as a parameter list (like before the colon pertaining to the _≡_), but be understood as a list of Curried arguments. The main practical use of ∀ is to distinguish between x → P x and ∀ x → P x. The former desugars to (_ : x) → P x (i.e, x is a type), while the latter desugars to (x : _) → P x (i.e, x stands for some individual, and its type is deduced from the type of P).

I think your other test cases can now mostly be worked out. The following doesn't have a sugared form because the A → B argument isn't given a name.

What troubles me is that type declaration:

map : {A B : Set} -> (A -> B) -> List A -> List B

is fine, while

map : {A B : Set} (A -> B) -> List A -> List B

is not.

You could instead write:

 map : {A B : Set} (f : A -> B) -> List A -> List B

or

 map : {A B : Set} (_ : A -> B) -> List A -> List B

if you really wanted.