[Agda] How to typecheck "How to keep your Neighbours in Order" in the latest version of Agda

[effectfully]

You can explicitly write

record One : Set where
  constructor it

instance
  One-Instance : One
  One-Instance = it