[Agda] _$_

[Serge D. Mechveliani]

For  Agda-2.3.0.1 + lib-0.6,  
     _$_  imported from  Function,  
     record IntIdeal (n : Nat) ...    my user type,

each of the following 4 declarations causes "unsolved metas":

  n : Nat
  n = suc $ suc 0

  foo : (g : Nat) -> IntIdeal $ suc $ suc g -> CommutativeRing _ _
  foo : (g : Nat) -> IntIdeal $ suc (suc g) -> CommutativeRing _ _
  foo : (g : Nat) -> IntIdeal (suc $ suc g) -> CommutativeRing _ _
  
But  
             foo : (g : Nat) -> IntIdeal $ suc g -> CommutativeRing _ _
is compiled.
What might this mean?

By using _$_, I tried to reduce the number of parentheses ...

Regards,

------
Sergei