0a2d121e45
closes #5333 This PR tries to address issue #5333. My conjecture is that the binder annotations for `C.toB` and `Algebra.toSMul` are not ideal. `Algebra.toSMul` is one of declarations where the new command `set_synth_order` was used. Both classes, `C` and `Algebra`, are parametric over instances, and in both cases, the issue arises due to projection instances: `C.toB` and `Algebra.toSMul`. Let's focus on the binder annotations for `C.toB`. They are as follows: ``` C.toB [inst : A 20000] [self : @C inst] : @B ... ``` As a projection, it seems odd that `inst` is an instance-implicit argument instead of an implicit one, given that its value is fixed by `self`. We observe the same issue in `Algebra.toSMul`: ``` Algebra.toSMul {R : Type u} {A : Type v} [inst1 : CommSemiring R] [inst2 : Semiring A] [self : @Algebra R A inst1 inst2] : SMul R A ``` The PR changes the binder annotations as follows: ``` C.toB {inst : A 20000} [self : @C inst] : @B ... ``` and ``` Algebra.toSMul {R : Type u} {A : Type v} {inst1 : CommSemiring R} {inst2 : Semiring A} [self : @Algebra R A inst1 inst2] : SMul R A ``` In both cases, the `set_synth_order` is used to force `self` to be processed first. In the MWE, there is no instance for `C ...`, and `C.toB` is quickly discarded. I suspect a similar issue occurs when trying to use `Algebra.toSMul`, where there is no `@Algebra R A ... ...`, but Lean spends unnecessary time trying to synthesize `CommSemiring R` and `Semiring A` instances. I believe the new binder annotations make sense, as if there is a way to synthesize `Algebra R A ... ...`, it will tell us how to retrieve the instance-implicit arguments. TODO: - Impact on Mathlib. - Document changes. --------- Co-authored-by: Kim Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
21 lines
949 B
Text
21 lines
949 B
Text
synthorder.lean:4:0-4:40: error: instance does not provide concrete values for (semi-)out-params
|
||
Foo A (B × ?C)
|
||
synthorder.lean:7:0-7:38: error: cannot find synthesization order for instance @instFooNat with type
|
||
{A : Type} → [inst : Foo A Nat] → Foo Nat A
|
||
all remaining arguments have metavariables:
|
||
Foo ?A Nat
|
||
[Meta.synthOrder] synthesizing the arguments of @instFoo in the order [3, 4]:
|
||
Foo A B
|
||
Foo B C
|
||
[Meta.synthOrder] synthesizing the arguments of @instFoo_1 in the order [4, 3]:
|
||
Foo A B
|
||
Foo B C
|
||
[Meta.synthOrder] synthesizing the arguments of @instFooOption in the order []:
|
||
[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [2]:
|
||
TwoHalf α
|
||
[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4]:
|
||
Four α β
|
||
[Meta.synthOrder] synthesizing the arguments of @instFourOfThree in the order [4, 2, 3]:
|
||
Three α β
|
||
One β
|
||
TwoHalf β
|