[Agda] type check cost

[Sergei Meshveliani]

On Sun, 2015-10-11 at 21:13 -0400, Wolfram Kahl wrote:
> On Sun, Oct 11, 2015 at 11:09:29PM +0400, Sergei Meshveliani wrote:
> > But I recall now of  --sharing.
> > 
> > Probably, it is appeared in  Development Agda of October 8,  
> > is it?
> > I try 
> > 
> >   agda $agdaLibOpt +RTS -M..G -RTS --sharing  Goal.agda    
> > 
> > , and it reports
> > 
> > --------------------
> >  /home/mechvel/doconA/0.04/reports/costRep-oct8-2015/Nat0.agda:143,1-20
> > I'm not sure if there should be a case for the constructor s≤s,
> > because I get stuck when trying to solve the following unification
> > problems (inferred index ≟ expected index):
> >   suc m ≟ n
> >   suc n₁ ≟ 0
> > when checking the definition of ≤0→≡
> > --------------------
> > 
> > Nat0.agda  is in the very beginning of the code, that is referred below.
> > 
> > The function is 
> > 
> >   ≤0→≡ : ∀ {n} → n ≤ 0 → n ≡ 0
> >   ≤0→≡ z≤n =  PE.refl
> > 
> > Without --sharing, it is type-checked.
> > 
> > Is this a bug?
> 
> Yes --- I reported this as Issue 1574.
> Just open the offending module in emacs,
> restart Agda, and the load the module individually.
> (I have about four modules four which I need this.)


Thank you.
Currently I fail to run Agda from under  emacs.
On the other hand, I do not find Issue 1574.
Probably, it is fixed.

So, I am going to try the to-day Development version. in a hope that
`--sharing'  will work when Agda is run from the command line.

Regards,

------
Sergei