[Agda] Typing.CheckRHS

[Sergei Meshveliani]

On Tue, 2017-04-18 at 06:58 +0200, Ulf Norell wrote:
> Why don't you try to nail down the culprit further by replacing terms
> by
> 'any', defined as
> 
> 
> postulate any : ∀ {a} {A : Set a} → Set
> 
> 
> ?


Indeed, I did this. But the thing is not clear.
By setting `anything' in various places, I find that in the below `case'
the main cost gives the `yes' branch:
 
  (yes hasSq-∣x∣) → 
       let hasSq-x : HasSquare x
           hasSq-x = proj₂ HasSquare-x←→HasSquare-∣x∣ hasSq-∣x∣   -- (1)
       in  
       yes $ HasSquare→HasSquare-asd hasSq-x                      -- (2)

This makes it
  Total            408             
  Typing.CheckRHS  150     
  Serialization    121 (156) 
  Deserialization   64    

There remain the two RHS to try to replace with `anything': (1) and (2).
If any one of them is replaced with `anything', then the profiling shows

  Total            155           
  Typing.CheckRHS    0    
  Serialization     72 (81) 
  Deserialization   65  

CheckRHS disappears, for some unknown reason.

I hoped to find a place for which inserting a signature reduces greatly
the type check cost, similarly as with the example (call it (I)) where
the cost is reduced more than 100 times.
But now I think that there is not such a place.
The effect of (I) is probably due to a bug in Agda: instead of reporting
of that something is not solved ("providing some signature may help") it
continues trying to solve something. And as the whole project is
type-checked under 12 Gb in 64 minutes, then there probably is not any
similar place. 
(?)

Thanks,

------
Sergei



> / Ulf
> 
> On Mon, Apr 17, 2017 at 11:14 PM, Sergei Meshveliani
> <mechvel at botik.ru> wrote:
>         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
>         
>         
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
>         
> 
>