On Fri, 2017-03-31 at 07:24 +0200, Ulf Norell wrote:
> Your code turns into (roughly)
> module M1 where
> M11.f : (p : ℕ) → ℕ → ℕ
> M11.f p x = p + x
>
>
> module M2 where
> f = M1.M11.f 2
> g : ℕ → ℕ
> g x = f (suc x)
>
>
> No normalisation takes place.
My real example is of the scheme
----------------- M1.agda -----------
module M1 where
open import Data.Nat using (ℕ; _+_)
module M11 (p : ℕ)
where
f : ℕ → ℕ
f x = p + x
----------------- M2.agda -----------
module M2 where
open import Data.Nat using (ℕ; suc)
open import M1 using (module M11)
module M11-2 = M11 2
-------------------------------------
So that M2 does almost nothing.
Only in the real example M11 has certain complex definitions inside
it, with p : CommutativeMonoid (represented by a dependent record).
But real M2 has nothing besides importing p from a certain
parametric module and declaring
module M11-p = M11 p.
In the above example I replace this with the line
module M11-2 = M11 2.
And type-checking of the real M2.agda takes 75 sec on a 3 GHz machine,
and needs more than 3 Gb heap.
The question is: what does it with M2.agda ?
What is substituted where and what is being normalized?
Thanks,
------
Sergei