<div dir="ltr">Why don't you try to nail down the culprit further by replacing terms by<div>'any', defined as</div><div><br></div><div>postulate any : ∀ {a} {A : Set a} <span style="font-size:12.8px">→</span> Set</div><div><br></div><div>?</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 17, 2017 at 11:14 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Mon, 2017-04-17 at 23:07 +0300, Sergei Meshveliani wrote:<br>
> Dear Agda developers,<br>
><br>
> I continue investigating the type check cost of various parts in my<br>
> project.<br>
> And for certain module  Integer2.agda,  the option  -v profile:7<br>
> shows something new:<br>
><br>
>     Typing.CheckRHS    267,464ms<br>
><br>
> This occurs the greatest part in Total for this module<br>
> (while in other considered modules the main part was Serialization and<br>
> Serialization).<br>
> Can you, please comment this?<br>
<br>
<br>
</span>First I comment out a large last part in  Integer2.agda.<br>
Then I move the "{-" mark down, to add a small current piece of code,<br>
and see how the checker profile report changes.<br>
And I find the point at which the cost jumps up.<br>
The Total increases 2.5 times, and instead of  Serialization and<br>
Deserialization, the main cost part becomes<br>
<br>
  Typing.CheckRHS   266,620ms<br>
<br>
What does this Typing.CheckRHS mean, what is its difference to<br>
Serialization ?<br>
The responsible fragment is small:<br>
<br>
hasSquare?-asd :  Decidable HasSquare-asd<br>
hasSquare?-asd (asd' (x , x≢0)) =<br>
  case<br>
      Nat2.hasSquare? ∣ x ∣<br>
  of \<br>
  { (yes hasSq-∣x∣) →<br>
               let hasSq-x : HasSquare x<br>
                   hasSq-x = proj₂ HasSquare-x←→HasSquare-∣x∣ hasSq-∣x∣<br>
               in  yes $ HasSquare→HasSquare-asd hasSq-x<br>
<br>
  ; (no ¬hasSq-∣x∣) →<br>
       let<br>
         ¬hasSq[X] : ¬ HasSquare-asd (asd' (x , x≢0))<br>
         ¬hasSq[X] =<br>
            \hasSq[X] →<br>
            let hasSq-x   = HasSquare-asd→HasSquare x≢0 hasSq[X]<br>
                hasSq-∣x∣ = proj₁ HasSquare-x←→HasSquare-∣x∣ hasSq-x<br>
            in  ¬hasSq-∣x∣ hasSq-∣x∣<br>
       in<br>
       no ¬hasSq[X]<br>
  }<br>
<br>
Can you please, give a hint about what can be happening there in the<br>
checker?<br>
<br>
(The code is about an integer  x  having a square factor,  (abs x) : Nat<br>
having a square factor,  and  (asd x)   having a square factor<br>
-- about the relation between these three assertions. And  asd x  means<br>
here  x  or  (- x).<br>
<br>
The module  Integer2.hs  uses many instances for ℤ of rather complex<br>
deneric structures.<br>
).<br>
<div class="HOEnZb"><div class="h5"><br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>