[Agda] type check cost

[Sergei Meshveliani]

On Wed, 2015-10-07 at 15:03 +0200, Nils Anders Danielsson wrote:
> On 2015-10-04 15:57, mechvel at scico.botik.ru wrote:
> > Currently I use  Agda 2.4.2.4  to develop my algebraic library called DoCon-A.
> > And it cannot type-check on a machine of  16 Gb RAM.
> 
> During the last Agda meeting we implemented some optimisations that
> might be useful for you. However, AFAIR they have not been released yet.
> I suggest that you try the development version of Agda.
> 

It reports

------------------------------
...
/home/mechvel/doconA/0.04/source/DPrelude.agda:275,46-63
Don't know how to parse _~_ Respects2 _≈_. Could mean any one of:
  _Respects2_ _~_ _≈_
  _Respects2_ _~_ _≈_
...

Operators used in the grammar:
  Respects2 (infix operator, level 20) [_Respects2_
(/home/mechvel/doconA/0.04/source/DPrelude.agda:245,1-12)]
(the treatment of operators has changed,
...
-----------------------------

As I recall, there was a certain recent development version which
required fixity decl for each operator.
But  agda-2.4.2.4  has rejected this fixity requirement. 
Right?

Now, what have I to do, to set fixities everywhere in my (large) code?

How stable is this decision about the language?

Thanks,

------
Sergei