[Agda] effect of skipping `module'

[Andreas Abel]

I fixed the bug on github.  With the latest development version of Agda, 
you should now get a parse error.

On 01.02.2016 11:31, Andreas Abel wrote:
> 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/