Hole in the middle of a record is malformed

[laMudri]

The following code gives the error below.

Code:

open import Agda.Primitive using (Level; lsuc)

record Foo (o : Level) : Set (lsuc o) where

  field
    Obj : Set o
    Hom : Set o

  Sub : Set ?
  Sub = Hom

  field
    id : Set o

Error:

Set o != Set (λ Hom₁ → o)
when checking that the expression Hom has type Set (λ Hom₁ → o)

[andreasabel]

Similar: #5478, #2257

[andreasabel]

After #5483 the error is now:

Set o != Set Hom

[andreasabel]

Seems like this was fixed by my work on #5478.