[Agda] effect of skipping `module'

[Andreas Abel]

You discovered an instance of bug #1388:

   https://github.com/agda/agda/issues/1388

On 30.01.2016 19:33, Sergei Meshveliani wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/