-- Sometimes we can't infer a record type module InferRecordTypes-4 where postulate A : Set record R : Set₁ where field x₁ : Set x₂ : Set record R′ : Set₁ where field x₁ : Set x₃ : Set bad = record { x₁ = A }