[Agda] type check cost

[Wolfram Kahl]

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.)


Best regards,

Wolfram