[Merged by Bors] - chore: bump to std4 2022-12-05 #865
Conversation
| @@ -61,7 +61,7 @@ Mario made the following analysis of uses in mathlib3: | |||
|
|
|||
| universe u v | |||
|
|
|||
| class IsSymmOp (α : Type u) (β : outParam (Type v)) (op : outParam (α → α → β)) : Prop where | |||
| class IsSymmOp (α : Type u) (β : Type v) (op : α → α → β) : Prop where | |||
There was a problem hiding this comment.
This was obviously an error. The whole point of unbundled classes is that we can have more than one operation per type, and the out-param version only allowed a single commutative operation per type.
The error was indirectly flagged by the new dangerousInstances linter: it complained about the is_symm_op_of_is_commutative instance below, correctly pointing out that it used the non-out-param IsCommutative class (which may have more than one solution for the operation✝) to (nondeterministically) fill in the out-param of the IsSymmOp class.
✝ And even worse, instances for IsCommutative may rely on op not being a metavariable. This mismatch can result in nontermination of type class search.
| @@ -141,7 +141,7 @@ variable {F α β} [i : FunLike F α β] | |||
|
|
|||
| -- Give this a priority between `coe_fn_trans` and the default priority | |||
| -- `α` and `β` are out_params, so this instance should not be dangerous | |||
| -- Porting note: @[nolint dangerous_instance] | |||
| @[nolint dangerousInstance] | |||
There was a problem hiding this comment.
This nolint is actually unnecessary now. The new linter is much smarter than the old one (it understands out-params, and I've also taught it about the not-quite-out-params in CoeHead/CoeTail/Coe).
There was a problem hiding this comment.
Was the dangerous instance linter also responsible for the change to the RBMap.keys coe? What makes that one dangerous?
There was a problem hiding this comment.
Yes, the linter also flagged those. This particular case should be fine, since we don't have any other instances mentioning Keys. But if you added a hypothetical [Coe β β'] : Coe (Keys α β cmp) (Keys α β' cmp) instance, then you'd get nontermination.
The general rule for TC search is that we don't want to have any metavariables in non-out-params. Otherwise, you get goals like Group ?α and end up enumerating all groups.
There was a problem hiding this comment.
This rule might be a bit on the cautious side, as it also rules out Coe (Fin n) Nat ✝️, which is in core. I'm open for other clear rules that rein in the coercion instances as well. But coercion instances are an easy way to break everything (including notations and macros, since they rely on coercions!). So we definitely need some strict linters here.
✝️ (which notably conflicts with a hypothetical Coe (Fin n) (Fin (n+1)))
There was a problem hiding this comment.
I'm inclined to follow the cautious rule until we find a compelling counterexample to examine and derive some rules from. (The Fin n -> Nat coe can be made into a CoeHead as well, I think.)
There was a problem hiding this comment.
Yes, it can and probably should.
There was a problem hiding this comment.
Hmm, this breaks somewhat easily because we don't chain CoeHead.
|
bors merge |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
|
bors merge |
|
Already running a review |
No description provided.