[Agda] type check cost for `open'

[Sergei Meshveliani]

People,

I have a problem of the  type check cost for the `open' declaration.

The project consists of about 20 files:

  Foo1.agda ... Foo18, OverIntegralRing-0.agda, OverIntegralRing-1.agda.

It is for               Agda 2.4.2.3.
The machine is of       16 Gb RAM,  3 GHz.
Type checking is under  -M13G -H13G

(-A1G does not effect essentially).

The first 19 files are type-checked in 1-2 hours,
and I take this as "Anyway, it is done. let us type-check the next and
see".
 
OverIntegralRing-0.agdai  has  12 Mb size.
Other .agdai files have         4 Mb on average.

There arises a question of type-checking  OverIntegralRing-1.agda.
This file is as follows:


************************************** OverIntegralRing-1.agda **
open import Level using ...
...
open import Relation.Binary using ...
...
open import Data.Nat using (ℕ; suc)

-- of DoCon-A --
open import Structures0 using (module Magma; module UpMagma)
...
open import Structures3 using (module IntegralRing; UpIntegralRing; 
                                                module UpIntegralRing) 
open import Factorization.FtMonoid using 
                                   (module OfCancellativeCommMonoid)
import OverIntegralRing-0   --
 
-------------------------------------------------------------
module OverIntegralRing-1 {α α=} (upIR : UpIntegralRing α α=)
                   (_∣?_ : let Mg = UpIntegralRing.*magma upIR
                           in  Decidable₂ $ Magma._∣_ Mg 
                   )
  where
  open UpIntegralRing upIR using (...)
                renaming (Carrier to C; *upCommutativeMonoid to *upCMon)
  open IsEquivalence isEquivalence using () 
                  renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)
  open EqR setoid renaming (_≈⟨_⟩_ to _≈[_]_)
  open UpMagma *upMagma using (_∣_; _∤_; ∣cong₁; ∣cong₂; ∤cong₁)
                                                renaming (_~asd_ to _~_)
  open UpMonoid *upMonoid using (_^_; ^1=id; ∣trans)
  open CommutativeSemigroup *commutativeSemigroup using (bothFactors∣)
  open MonoidLemmata *upMonoid     using (^cong₁; x∣x; x^2≈xx)
  open RingLemmata   upRing        using (0*; ∣nonzero→≉0)
  open Ring1Lemmata  upRingWithOne using (∣1→≉0; 0^suc) 

{- -- expensive 
  open OverIntegralRing-0 upIR _∣?_ using                       
       (_∣'?_; *cancel-nz; *cMon-NZ; *upCMon-NZ; IsPrime; prime→≉0; 
        Factorization; IsPrime-nz→IsPrime; IsPrime→IsPrime-nz)
-}
*******************************************************************

And that is all:  
only open several modules imported from previous files.

1. It is type-checked in  41 sec,  with  .agdai  of ~ 900 Kb
   (the smallest .agdai).


2. Uncomment the last `open'.
Then  30 min  is not enough to type-check. Many Gb are allocated.

Giving  14 Gb  leads to swapping, this slows down the process greatly
(I expect that on a 32 Gb machine and under -M24G it will type-check in 
1 minute).

I need to program several functions in this environment.
But this very environment fails to type check on a 16 Gb machine.

The are two functions set under  NO_TERMINATION_CHECK
-- this pragma will be removed after certain `panic' is fixed in Agda.
Probably, this pragma does not increase the type check cost
(can it?).

Is something wrong in the Agda implementation approach?
(a real sharing, the normal form interpreter ... I do not know).

Regards,

------
Sergei