[Agda] Typing.CheckRHS

[Sergei Meshveliani]

On Mon, 2017-04-17 at 23:07 +0300, Sergei Meshveliani wrote:
> Dear Agda developers,
> 
> I continue investigating the type check cost of various parts in my
> project.
> And for certain module  Integer2.agda,  the option  -v profile:7 
> shows something new:
> 
>     Typing.CheckRHS    267,464ms
> 
> This occurs the greatest part in Total for this module
> (while in other considered modules the main part was Serialization and
> Serialization).    
> Can you, please comment this?


First I comment out a large last part in  Integer2.agda.
Then I move the "{-" mark down, to add a small current piece of code,
and see how the checker profile report changes.
And I find the point at which the cost jumps up.
The Total increases 2.5 times, and instead of  Serialization and
Deserialization, the main cost part becomes  
   
  Typing.CheckRHS   266,620ms            

What does this Typing.CheckRHS mean, what is its difference to
Serialization ?
The responsible fragment is small:

hasSquare?-asd :  Decidable HasSquare-asd
hasSquare?-asd (asd' (x , x≢0)) =
  case
      Nat2.hasSquare? ∣ x ∣
  of \
  { (yes hasSq-∣x∣) → 
               let hasSq-x : HasSquare x
                   hasSq-x = proj₂ HasSquare-x←→HasSquare-∣x∣ hasSq-∣x∣
               in  yes $ HasSquare→HasSquare-asd hasSq-x

  ; (no ¬hasSq-∣x∣) →
       let 
         ¬hasSq[X] : ¬ HasSquare-asd (asd' (x , x≢0))
         ¬hasSq[X] =
            \hasSq[X] →
            let hasSq-x   = HasSquare-asd→HasSquare x≢0 hasSq[X]
                hasSq-∣x∣ = proj₁ HasSquare-x←→HasSquare-∣x∣ hasSq-x
            in  ¬hasSq-∣x∣ hasSq-∣x∣
       in
       no ¬hasSq[X]
  }

Can you please, give a hint about what can be happening there in the
checker?

(The code is about an integer  x  having a square factor,  (abs x) : Nat
having a square factor,  and  (asd x)   having a square factor
-- about the relation between these three assertions. And  asd x  means
here  x  or  (- x).

The module  Integer2.hs  uses many instances for ℤ of rather complex
deneric structures.
).

Thanks,

------
Sergei