packages feed

Agda-2.3.2.2: test/succeed/Issue34.agda

-- There was a bug with module applications in let.
module Issue34 where

module A (X : Set) where
  postulate A : Set

T : (X : Set) -> let open A X in A -> Set
T X _ = X

record B (X : Set) : Set where
  open A X
  field f : A

postulate
  foo : (X : Set)(b : B X) ->
        let open A X
            open B b in
        A -> Set