issue !4#12094: Porting note: unimplemented `dangerous_in...

Stream: triage

[Random Issue Bot]

Today I chose issue 12094 for discussion!

Porting note: unimplemented dangerous_instance linter
Created by @None (@grunweg) on 2024-04-12
Labels: t-meta, porting-notes, tech debt

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 12094 for discussion!

Porting note: unimplemented dangerous_instance linter
Created by @None (@grunweg) on 2024-04-12
Labels: t-meta, porting-notes, tech debt

Is this issue still relevant? Any recent updates? Anyone making progress?

[Jireh Loreaux]

Isn't this just not relevant anymore? That is, isn't it now the case that Lean handles this when declaring the instace? If it is what used to be called a dangerous_instance, Lean will just complain "failed to determine synthesization order".

[Kyle Miller]

Yes, exactly @Jireh Loreaux. I just read the mathlib3 source code to be sure, and it's nowadays it's handled by the "cannot find synthesization order" error.

instance (p : Prop) [Decidable p] : Decidable True := sorry
/-
cannot find synthesization order for instance instDecidableTrue_lean with type
  (p : Prop) → [inst : Decidable p] → Decidable True
all remaining arguments have metavariables:
  Decidable ?p
-/

[Johan Commelin]

Thanks Kyle!
I went ahead and closed the issue.

[Jireh Loreaux]

@Johan Commelin we should first make sure there are no porting notes about this.

[Johan Commelin]

Good catch. :see_no_evil: :man_facepalming:

$ rg "dangerous_instance"
Mathlib/Algebra/Ring/CompTypeclasses.lean
160:-- Porting note(#12094): removed nolint; dangerous_instance linter not ported yet
161:-- @[nolint dangerous_instance]

Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
92:-- Porting note(#12094): removed nolint; dangerous_instance linter not ported yet
93:--attribute [nolint dangerous_instance] Valued.toUniformSpace

Mathlib/Topology/Algebra/Module/Basic.lean
250:-- Porting note(#12094): removed nolint; dangerous_instance linter not ported yet
251:-- attribute [nolint dangerous_instance] ContinuousSemilinearMapClass.toContinuousMapClass

Mathlib/Algebra/AddTorsor.lean
57:-- Porting note(#12094): removed nolint; dangerous_instance linter not ported yet
58:--attribute [nolint dangerous_instance] AddTorsor.toVSub

Mathlib/Analysis/RCLike/Lemmas.lean
34:-- Porting note(#12094): removed nolint; dangerous_instance linter not ported yet
35:-- @[nolint dangerous_instance]

[Johan Commelin]

I will remove those now

[Johan Commelin]

Done: #17798