[Agda] delaying computation to run time

[mechvel at scico.botik.ru]

People,

I am testing a certain method by arranging

---------------------------------------------Test2.agda ----------
foo : List Pol   -- a data for computation
foo =
   case varPols
   of \
   { (z ∷ y ∷ x ∷ []) →
                  (2 * z * y ^ 2 + 4 * x + 1) ∷
   ...
   }

main = (readFiniteFile "data.txt") >>= putStrLn ∘ toCostring ∘
                                        test foo 100 ∘ stringToNat

-- In another file  ---------------------------
test : List Pol → ℕ → ℕ → String
test fs n e =
   let
     fs'                  = map (_^ e) fs        -- fs
     (rs , ps , gs , bsE) = gBasis-ext n fs'
   in
   concatStr ...
------------------------------------------------------------------

e : Nat  is a dummy value being read from file, and to be put as 1.
So that it will hold  fs' == fs.

e is introduced because without inputting it, the example would be 
computed at the type
check time, which will be very expensive (gBasis-ext is expensive to 
compute).
Will it?

Now, after
   > agda -c $agdaLibOpt --ghc-flag -rtsopts Test2.agda

it is checked, compiled and linked. Then

   > time ./Test2 +RTS -M14G -RTS

computes and prints the result in  50 seconds.

And in the next program version I have forgotten to apply  "map (_^ e) 
fs",
so that  e  is being read, but is not used in the body of `test'.

And still the type checking, compilation, computation, printing and 
timing  are the same.
I think that  gBasis-ext  still evaluates only at the run time.

So that it occurs sufficient to read something from file and to set the 
type of this value
in the signature, without using this value in the function body.

Is this so? Is this a reliable approach?
(this is on Agda-2.6.0.1).

Thanks,

------
Sergei