[Agda] expensive `with'

[mechvel at scico.botik.ru]

Dear Agda developers,

I have the code fragment

------------------------------------------------------------
       ... | yes hmS | yes hmF₂ =  inj₂ (hmS , degS≤k)
              where
              open ≤-Reasoning
              s       = f₁+f₂
              degF₂   = deg f₂ hmF₂

              degF₂≤k : degF₂ ≤ k
              degF₂≤k = <⇒≤ (degF₂<k hmF₂)

              degS≤k : deg s hmS ≤ k
              degS≤k = case deg[f+g]≤max f₁ f₂ hmF₁ hmF₂
                       of \
                       { (inj₁ nullS) → contradiction hmS
                                               (null⇒¬HasMon {s} nullS)
                       ; (inj₂ (hmS' , degS'≤degF₁⊔degF₂)) →
                           begin deg f₁+f₂ hmS   ≡⟨ refl ⟩
                                 deg f₁+f₂ hmS'  ≤⟨ degS'≤degF₁⊔degF₂ ⟩
                                 degF₁ ⊔ degF₂   ≤⟨ ⊔-least degF₁≤k 
degF₂≤k ⟩
                                 k
                           ∎
                       }
-----------------------------------------------------------

where the file is type-checked in 1 minute (on a 3 GHz machine).

Initially, there was `with' instead of the last `case'.
And 20 minutes was not enough.
Then I set types explicitly in most places and also change the last
`case` with
                     with deg[f+g]≤max f₁ f₂ hmF₁ hmF₂
                 ... | inj₁ _ = anything
                 ... | inj₂ _ = anything

After 25 minutes it reports
Checking ... .agda).
agda: Heap exhausted;
agda: Current maximum heap size is 3758096384 bytes (3584 MB).

The `top' command shows that after 5 minutes about 3 Gb is taken by 
Agda,
then it stops eating memory, and finally breaks by heap.

I tend to think that when the type checker becomes very slow, it is 
desirable
to use `case' rather than `with' in the responsible code.

Can people, please, comment?

------
Sergei