lean4
lean4 copied to clipboard
leanprover
feat: weaken CoeFun -> CoeOut instance to -> CoeOTC
We change the instance that turns CoeFun into CoeOut into an instance that turns it into a CoeOTC instead. This reduces our ability to chain together CoeFuns.
I don't have a particularly good justification for this, but the benchmarking consequences at leanprover-community/mathlib4#8378 are dramatic:
- 4.5% reduction in instruction count
- 3.8% reduction in wall-clock
- 12% reduction in typeclass inference
Also:
import Mathlib
inductive P
inductive Q
#time example (p : P) : Q := p
drops from around 250ms(!) to around 20ms.
Now, an alternative interpretation of all of this is that Mathlib is doing something it shouldn't with its enormous hierarchy of FunLike instances...
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
- 🟡 Mathlib branch lean-pr-testing-2869 build against this PR was cancelled. (2023-11-13 08:02:33) View Log
- ✅ Mathlib branch lean-pr-testing-2869 has successfully built against this PR. (2023-11-13 09:15:03) View Log
- 🟡 Mathlib branch lean-pr-testing-2869 build against this PR was cancelled. (2024-06-26 02:02:55) View Log
- 🟡 Mathlib branch lean-pr-testing-2869 build this PR didn't complete normally. (2024-06-26 02:02:58) View Log
- 🟡 Mathlib branch lean-pr-testing-2869 build this PR didn't complete normally. (2024-06-26 02:24:24) View Log
- 🟡 Mathlib branch lean-pr-testing-2869 build against this PR was cancelled. (2024-06-26 02:59:29) View Log
- ✅ Mathlib branch lean-pr-testing-2869 has successfully built against this PR. (2024-06-26 03:46:06) View Log
I've posted a long message on zulip explaining the cause of the 250ms coercion failure, and explaining how it leads to this patch.
@semorrison I think a change like this makes a lot of sense! CoeFun as it is described in the docs is designed to covert a non-function type to a function type when the non-function type appears as the head of an application (e.g., as f in f x). That defines CoeFun a single-use coercion with an expected input type. The use case also implies that coercions should still be possible on its input and output. It so happens that the way to implement such a coercion is in fact to use CoeOTC (even though that is not immediately obvious from CoeOTC's doc). Conversely, The current CoeFun -> CoeOut coercion implies that CoeFun is chainable, which seems very confused. That is, it tells Lean that even during normal coercions (e.g., between a non-function types A to B) it should also try to apply CoeFun step in-between if it can. A similar argument applies to CoeSort as well.
Code-wise, this doc needs to change to CoeOTC also :
https://github.com/leanprover/lean4/blob/d420252dcf9f419cc33944b4a0caad730ab25a5c/src/Init/Coe.lean#L102
In the meantime the 250ms example
import Mathlib
inductive P
inductive Q
#time example (p : P) : Q := p
has been fixed independently in Mathlib.
Coming back to this, I noticed that this doc also needs to be changed to CoeOTC:
https://github.com/leanprover/lean4/blob/84431c2eeb3064f1220d7ede8b820055bf367072/src/Init/Coe.lean#L260
The mathlib speedup from this has vanished in the meantime, thanks to https://github.com/leanprover-community/mathlib4/pull/8386, so I'll close this.