[Agda] hiding implementation

[Sergei Meshveliani]

People,

there is the following effect in Agda (of July 2014).
There are some programs of kind 

  foo : <signature>
  foo x =  <implementation>

  -- in another module ----
  f : <signature2>
  f y =  ...
         foo y       -- using  foo
         ...


They are type-checked.
And if we                      postulate foo : <signature>
and remove its implementation,
then Agda reports an error for  f  for the place where  foo  is applied.

Such cases as with  foo and f  are rare, but they present in my
application.

Is this an error in Agda ?

Regards,

------
Sergei