[Agda] type check performance

[Wolfram Kahl]

On Wed, Jan 11, 2017 at 09:46:00PM +0300, Sergei Meshveliani wrote:
> And my case is different. I define standard classical algebraic
> structures: Semigroup, Group, Ring, EuclideanRing, and such, and prove
> in Agda certain well-known properties of their operations. There cannot
> appear such type expressions like above for  id id ... id.
> 
> And still its type check needs 7Gb RAM and 60 minutes of time (on a 3
> GHz computer).  
> 
> [...]
>
> There is something strange in these 60 minutes and 7 Gb minimum.
> For example,  EuclideanRing  is far enough in the hierarchy. 
> And I ask to print the type (C-c C-d)  of the function (lemma)
> 
>   remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#                 
>  
> in the module parameterized by an instance of  EuclideanRing.
> It shows
> 
> (a b : UpIntegralRing.Carrier upIR) →
> (UpIntegralRing.*upMonoid upIR UpMonoid.∣ b) a →
> (upIR UpIntegralRing.≈ EuclideanRing.eucRem upIR∣? E a b)
> (UpIntegralRing.0# upIR)
> 
> This does not look like a large expression
> (though it contains several parts that may need to be replaced with
> their expanded definitions, depending on situation).

Can you go to the top-level of the file module in which this is defined,
and ask for the type  (C-c C-d) of the qualified name of remByDivisor,
qualified as necessary to be able to refer to it from the top-level
of the file module?

And also do that for each of  ∣  ,  eucRem ,  ≈ , and  0# ?

If my understanding is correct, then at least in some circumstances
and to a certain degree, these are the types that Agda is really dealing with.


Wolfram