20070530-1

Dummy.agda:

module Dummy where

M.agda

import Dummy as D
module M (A : Set) where

Top.agda

module Top where
  import M
  postulate A : Set
  open module MA = M A

In this example the typechecker doesn't think that M takes any arguments. If Dummy is imported without as D then everything work fine.

Notes

• The problem is an implicit assumption that the name of the top-level module is the first name to be generated in a file.