Instantiating modules in a record declaration does not quite work

[agda]

Instantiating modules in a record declaration does not quite work

[GoogleCodeExporter]

The problem is with open in let. Same error is obtained for

  B : (x : Set) -> let open A x in A -> Set
  B x _ = x

Original comment by [email protected] on 7 Dec 2007 at 2:02

[GoogleCodeExporter]

Original comment by [email protected] on 7 Dec 2007 at 3:04

• Changed state: Fixed

[GoogleCodeExporter]

The fix was only partial. Here is another problematic case:

  module Bug where

  record A : Set1 where
    field
      carrier : Set
      X       : carrier -> Set

  module B (a : A) where

  record C (a : A) : Set where
    open A a
    open B a
    field
      foo : forall (x : carrier) -> X x

If "open B a" is commented out the code type checks, otherwise the
following error message is issued:

  Bug.agda:14,23-30
  A -> Set != _19 of type Set1
  when checking that the expression carrier has type _19

Original comment by nils.anders.danielsson on 7 Dec 2007 at 4:55

• Changed state: Accepted

[GoogleCodeExporter]

Original comment by [email protected] on 11 Dec 2007 at 11:52

• Changed state: Fixed