# Pastebin pDzfFHrL
module Test where

open import Data.Unit

module Foo where
  record Foo : Set where
    field
      a : ⊤
      b : ⊤

  open Foo public
  bar : Foo → Foo
  bar p = record p { a = tt }