[Agda] dangerous _$_

[Serge D. Mechveliani]

Who can tell, please, what is the matter with using _$_ in the 
following fragment?

  ...
  sMbFinEnum : Maybe $ DecFiniteEnumeration sSetoid
  sMbFinEnum =
        case  DSet.mbFiniteEnum dSet  of \
        { nothing                 -> nothing
        ; (just (no _))           -> nothing
        ; (just (yes hasFinEnum)) ->
                     just $ yes (finEnumForSubsetoid bSetoid member?
                                                             hasFinEnum)
 
The checker of  Agda-2.3.2 MAlonzo  (lib-0.7)  reports  "unsolved metas"
for the line of          "just $ yes ...".
And if I replace it with 
                         just (yes (finEnumForSubsetoid ...))
,
then the code is type-checked and compiled.
I have spent 6 hours to find who makes this "unsolved metas".
Now, I see, who it is. But do not understand -- why;
and also start to fear of _$_ !

Thank you in advance for explanation,

------
Sergei