[Agda] about serialization

[Sergei Meshveliani]

Dear Agda developers,

consider the modules  M1.agda and M2.agda  of

---------------------------------------
module M1 where
open import Data.Nat using (ℕ; _+_)

module M11 (p : ℕ)
  where
  f : ℕ → ℕ
  f x =  p + x 

----------------------------------------
module M2 where
open import Data.Nat using (ℕ; suc)
open import M1       using (module M11)

open M11 2 using (f)

g : ℕ → ℕ
g x =  f (suc x)
-----------------------------------------

And suppose that  M1  is type-checked earlier.  

1) Then, how eager is the type checker in processing the definition 
   for  g ?

Probably, it substitutes 2 into the body of  M11, and into  f,
and it becomes
       f x = 2 + x.

Then it normalizes everything, and f  becomes  f x = suc (suc x).

Then it substitutes the obtained definition for f into the definition
for  g,  and normalizes this to
g x = suc (suc (suc x)).

Right? 

Or may be, it delays the above operations for where  g  is used?

2) If we comment out the last two lines for  g,
   then will the type checker do the above substitution into M11 and
normalization for the definition of  f ?

Thanks,

------
Sergei