[Agda] effect of skipping `module'

[Sergei Meshveliani]

People,
I discover that the following is not type-checked by

  > agda $agdaLibOpt TT.agda
:

------------------------------------------------------------- TT.agda
open import Data.Nat  using (ℕ; suc)
open import Data.List using (List; []; _∷_)

module _ {α} {A : Set α}
    where
    data Null : List A → Set α  where  isNull : Null []

f : (xs : List ℕ) → Null xs → ℕ
f _ _ = 0
------------------------------------------------------------------

It reports 

"Set != (Set α)
 when checking that the expression xs has type List A
"
for the signature of  f.

And after adding the header
                            module TT where
it is type-checked.

This is Development Agda of January 19, 2016,  ghc-7.10.2.
Is this a bug?

Thanks,

------
Sergei