[Agda] unstable composition checking

[Sergei Meshveliani]

On Wed, 2017-06-21 at 15:12 +0200, Nils Anders Danielsson wrote:
> On 2017-06-16 20:58, Sergei Meshveliani wrote:
> > What might it mean this cost hole for  (just ∘ oppose) ?
> 
> I'm guessing that "just" is overloaded, and that Agda has trouble
> inferring the implicit arguments of _∘_. What happens if you write
> "Maybe.just" instead?


Sorry, I have lost the precise example.
I find now this one:

  foo = record{ ... 
              ; invMb =  just ∘ decInv-fr              -- (I)
                         -- Maybe.just ∘ decInv-fr     -- (II)
                         -- \f → just (decInv-fr f)    -- (III)
              ...
              }

(there is a huge environment import).

Type checking (II) and (III) succeeds in 40 sec.
(I) leads to "unsolved metas", but this report appears within 40 sec. 
In the lost example it was taking more than 10 minutes (interrupted).


> I'm guessing that "just" is overloaded, and that Agda has trouble
> inferring the implicit arguments of _∘_.

But `yes' is also overloaded -- ?
And replacing Maybe with Decidable, (just ∘) with (yes ∘),  
I had a similar successful example with (yes ∘).

Thanks,

------
Sergei