[Agda] type check performance

[Sergei Meshveliani]

On Wed, 2017-01-11 at 14:21 -0500, Wolfram Kahl wrote:
> 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.
> 

I have there

--------------------------------------------
open import Level using (_⊔_)
...
...
module OfEuclideanRing {α α=} (upIR∣? : UpIntegralRing-with∣? α α=)
                 (open OverIntegralRing-0 upIR∣? using (EuclideanRing))
                 E : EuclideanRing)  
  where
  upIR = proj₁ upIR∣?
  _∣?_ = proj₂ upIR∣?

  open UpIntegralRing upIR using 
                           (setoid; ... _≈_;  ... 0#; ... *upMonoid)
                           renaming (Carrier to C)

  open UpMonoid *upMonoid using (_∣_; _∤_; ∣cong; ... ∣trans)
                          renaming (∣∙ to ∣*; _~asd_ to _~_)
  ... 
  open EuclideanRing E using (eucRem; ...)
  ...

  remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#
  ...
--------------------------------------------               

I go to the beginning of this file and command

  C-c C-d  
  remByDivisor

And it prints its type.
Now, try with the _∣_.

This _∣_ instance is opened from   open UpMonoid *upMonoid,

and  *upMonoid  is opened from  open UpIntegralRing upIR.

What expression need I to put to the   C-c C-d   input window?
I try 
  let *UM = UpIntegralRing.*upMonoid upIR in UpMonoid._∣_ *UM

It reports

---------------
Structures0.DSet.Carrier
(.Structures0.Magma.dS (Structures0.UpMagma.magma
  (.Structures0a.UpSemigroup.upMagma
   (UpMonoid.upSemigroup (UpIntegralRing.*upMonoid upIR))))) →
Structures0.DSet.Carrier
(.Structures0.Magma.dS (Structures0.UpMagma.magma
  (.Structures0a.UpSemigroup.upMagma
   (UpMonoid.upSemigroup (UpIntegralRing.*upMonoid upIR))))) →
Set (α= ⊔ α)
------------------

It searches down:  
   UpIntegralRing --> UpMonoid --> UpSemigroup --> UpMagma --> DSet --> 
   Carrier

for each argument in the signature of  _∣_  -- as it was intended.

Further:
  C-c C-d
  EuclideanRing.eucRem E

leads to an error:
------------------
(OverIntegralRing-0.EuclideanRing upIR∣?) !=<
(Data.Product.Σ (UpIntegralRing (_α_0 upIR∣? E) (_α=_1 upIR∣? E))
 (λ upR → Decidable₂ (Magma._∣_ (UpIntegralRing.*magma upR))))
of type (Set (α= ⊔ α))
when checking that the expression E has type
UpIntegralRing-with∣? (_α_0 upIR∣? E) (_α=_1 upIR∣? E)
------------------

E  is a parameter in the head module, and  eucRem  is opened in
open EuclideanRing E ...
as shown above.
I wonder, why does this C-c C-d fail.

Thanks,

------
Sergei