Issue155.agda

-- There was a bug with module application in a let in a
-- parameterised module.
module Issue155 (A : Set) where

module M (Y : Set) where
  postulate F : Set → Set

Foo : Set₁
Foo = let module M′ = M A in (B : Set) → M′.F B

record R : Set₁ where
  open M A
  field
    B : Set
    C : F A