[Agda] tuple pattern sugar

[Serge D. Mechveliani]

(a beginner question about `sugar')

Please, how to simplify the following code?

 Solve : {c c' l' : Level} -> {A : Set c} -> {sB : Setoid c' l'} -> Set _      
 Solve {_} {_} {_} {A} {sB} =                                                  
           let B    = Setoid.Carrier sB                                
               _~~_ = Setoid._~~_    sB                    
           in  (f : A -> B) -> (b : B) -> Dec (\exist (\a -> f a ~~ b))

(for this letter I change respectively the two math symbols).

This is for  Agda-2.3.2 MAlonzo.

Generally, it often occurs that 
a) there are many hidden arguments, and
b) one is forced to write a call like this:  f {_} {_} {_} {_} a b
   -- too many place holdes.

So I try

  Level3 : Set _                        
  Level3 = Level x Level x Level 

  Solve : {(c , c' , l') : Level3} -> {A : Set c} -> {sB : Setoid c' l'} -> 
                                                                      Set _
  Solve {_} {A} {sB} =  ...

But it is not parsed.
I have an impression that  case ... of \lambda { (x, y, z) -> ... }
does work.
And it is desirable to have working the patterns like
a)  let  (x , y , z) = f u  in ...,
b)  (c , c' , l') : Level3
(and records).
Could the future Agda language make such patterns valid?

Thanks,

------
Sergei