[Agda] unstable composition checking

[Sergei Meshveliani]

Dear Agda developers,

I observe the following effect:

  oppose :  (f : T) → Foo f
  oppose = ...  	

  foo :  (f : T) → Maybe $ Foo f
  foo =  just ∘ oppose

         -- \f → just (oppose f)
   
Its type check takes much of time and more than 15 Gb heap.
I have interrupted it. 
And I suspect that it would end with "unsolved metas".
And
  foo =  \f → just (oppose f)

is type-checked fast, in a small heap.

Further, replacing in this example  Maybe with Dec  and  
just  with  yes  
leads to fast type checking for both variants.

What might it mean this cost hole for  (just ∘ oppose) ?

Regards,

------
Sergei