[Agda] `with' vs `case'

[Sergei Meshveliani]

Dear Agda team,

Style guide  of standard library writes for the code committers that
it is better to use the `with' construct than  case_of_. 
But

(1) Earlier the team advised me to use case_of_ as possible.

(2) I have a small application that adds a few items to standard     
    library, and a certain function  f  in the end that type-checks in 
    5 seconds when f is written via case_of_ and its type check seems 
    to loop infinitely when f is written via `with'.

Currently the Style guide actually suggests to use `with' everywhere
where it type-checks reasonably fast, and to use case_of_ in other
cases.

Let a function  g  from standard be written via `with' and be
type-checked fast. May it occur that when it is used in application, it
explodes the type checking as in the example (2) ?

Is not it better to use case_of_ instead of `with' in standard library
everywhere where it is type-checked?

Thanks,

------
Sergei