Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: Unbundled subclasses of
outParam
classes should not repeat the…
… parents' `outParam` This PR fixes a large amount of issues encountered in the port of `GroupTheory.Subgroup.Basic`, #1797. Subobject classes such as `MulMemClass` and `SubmonoidClass` take a `SetLike` parameter, and we were used to just copy over the `M : outParam Type` declaration from `SetLike`. Since Lean 3 synthesized from left to right, we'd fill in the `outParam` from `SetLike`, then the `Mul M` instance would be available for synthesis and we'd be in business. In Lean 4 however, we often go from right to left, so that `MulMemClass ?M S [?inst : Mul ?M]` is handled first, which can't be solved before finding a `Mul ?M` instance on the metavariable `?M`, causing search through all `Mul` instances. The solution is: whenever a class is declared that takes another class as parameter (i.e. unbundled inheritance), the `outParam`s of the parent class should be unmarked and become in-params in the child class. Then Lean will try to find the parent class instance first, fill in the `outParam`s and we'll be able to synthesize the child class instance without problems.
- Loading branch information