Instance parameters should not be turned into hidden parameters in record modules

[UlfNorell]

record Additive {ℓ} (A : Set ℓ) : Set ℓ where
  field
    zero : A
    _+_ : A → A → A

open Additive {{...}} public

record Subtractive {ℓ} (A : Set ℓ) {{ADD : Additive A}} : Set ℓ where
  field
    _-_ : A → A → A

  neg : A → A
  neg x = zero - x  -- no instance Additive A found

open Subtractive {{...}} public