parametrizing modules: variable vs constant (i.e. opaque)

Stream: lean4

[Andrés Goens]

I'm writing polymorphic code where I want to fix a value for a whole file, but keep it as a parameter that I can later instantiate. It seems that neither variable nor opaque are what I'm looking for, but somewhere in-between. This sounds like it could be a common use case, so maybe there's already a solution?

To be more concrete, say I was writing something like this

inductive SomeOption
  | variant₁ : SomeOption
  | variant₂ : SomeOption
  | variant₃ : SomeOption

structure SomeConfiguration where
  options : List SomeOption
  otherstuff : String

def someFunction : SomeOption → SomeConfiguration → SomeConfiguration
  | op, conf => { conf with options := op::conf.options }

If I want to be able to change the options/variants I have, I probably want to make the SomeOption type a parameter of everything else. But then I need to put it everywhere explicitly to make sure I'm using the same type, e.g.:

variable {SomeOption : Type 0} [BEq SomeOptions]

structure SomeConfiguration where
  options : List SomeOption
  otherstuff : String

def someFunction : SomeOption → @SomeConfiguration SomeOption → @SomeConfiguration SomeOption
  | op, conf => { conf with options := op::conf.options }

AFAIU the opaque keyword would allow me to fix this type here, but then I cannot later define my inductive SomeOption from above and recover the original version, while letting me use a different type somewhere else, right? Or would I be able to do this with@[implementedBy SomeOption] (and e.g. have multiple "implementations" at different parts)?

[Andrés Goens]

(I'm aware the solution of putting it explicitly everywhere works, it just makes the code much less readable in my opinion, I guess my question is premised on that opinion)