[Merged by Bors] - feat: variable? command for automatically adding typeclass dependencies

[kmill]

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.

---

[semorrison]

We probably should have a discussion on zulip about whether it is acceptable to leave variable! in code. I hope/think the answer should be yes (it's easy to remove later if we change our mind, so we might as well try it out?), but if the answer is no we'd probably want to make ? the default mode.

[jcommelin]

Does it check whether [Semiring R] is already deducible in the current context?

Answer: yes

I figured out from the tests that this is happening. I think it would be good to add a sentence about this in the docstring.

[semorrison]

I finally asked on zulip for opinions on leaving variable! in committed code.

[eric-wieser]

This seems to trick it:

variable!? (A : ℕ → Type) [∀ i : ℕ, Module R (A i)] [∀ i : ℕ, Algebra S (A i)]

giving

variable (A : ℕ → Type) [Semiring R] [(i : ℕ) → AddCommMonoid (A i)] [∀ i : ℕ, Module R (A i)]
  [CommSemiring S] [(i : ℕ) → Semiring (A i)] [∀ i : ℕ, Algebra S (A i)]

which has two different add operations on A i

[kmill]

I've done some cleanup and switched it to be variable?, so it's situated more as an informational command.

@eric-wieser Your example also applies to

variable? [Module R A] [Algebra S A]

I'm not sure there's a good way to fix it since it processes variables left-to-right and it doesn't check that previous binders can be inferred from successive ones. I've at least left this in the test file.

[kmill]

Now the command suggests an expansion like variable? [Module R M] => [Semiring R] [AddCommMonoid M] [Module R M] to save the expanded form to help the reader and to improve maintainability.

[semorrison]

Two suggestions about the documentation, otherwise let's try it out!

bors d+

[bors]

✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kmill]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style