Commit 2023-06-21 19:20 a7a9993c

feat: variable? command for automatically adding typeclass dependencies (#3162) The variable? command is like variable, but whenever there is an unsatisfied typeclass problem, it inserts this problem as a new instance argument and continues. For example, if you write

variable? [Module R M]

then, assuming there are no other instances in scope, it's as if you wrote

variable [Semiring R] [AddCommMonoid M] [Module R M]

It will not include instances that can be deduced from others in scope. It can handle parameterized instances:

variable? (f : α → Type) [(i : α) → Module R (f i)]

There are some inherent limitations with this system. The main one is that internally variables are stored as Syntax objects, so whenever variables? discovers a missing instance argument, it has to pretty print it. If pretty printing does not round trip (for instance due to implicit arguments) then the command might fail. As a safeguard against changes in the typeclass hierarchy, the command suggests replacing itself with a version that includes the expanded binders list, for example

variable? [Module R M] =>
  [Semiring R] [AddCommMonoid M] [Module R M]

This expanded list is elaborated separately for a defeq check on the resulting contexts. If the short version is not wanted, one can always replace everything up to and including the => with variable.