Data.Sym.Basic mathlib4#1672

Stream: mathlib4

[Johan Commelin]

The linter complains:

/- The `dangerousInstance` linter reports:
SOME INSTANCES ARE DANGEROUS
During type-class search, they produce subgoals like `Group ?M`.
Try marking the dangerous arguments as implicit instead. -/
#check Sym.hasCoe /- unassigned metavariable in out-param: Coe (Sym α ?n) (Multiset α) -/

but

instance Sym.hasCoe (α : Type _) (n : ℕ) : Coe (Sym α n) (Multiset α) :=
  ⟨toMultiset⟩

doesn't even take any instances as arguments.

[Johan Commelin]

It doesn't like that the n in Sym alpha n doesn't appear in Multiset alpha... but I don't see why that should be problematic here.

[Kevin Buzzard]

yeah that is pretty odd. Is it dangerous or is it a bug in the linter?

[Kyle Miller]

Does it stop being dangerous if it's instead a CoeTail instance? I think that should be fine as one.

[Chris Hughes]

I fixed this. I used CoeOut instead of Coe which is the same thing that is used for the coercion from subtypes.

[Chris Hughes]

Maybe CoeTail is better, I don't understand the difference between these things

[Kyle Miller]

I don't really either. Maybe a reason for CoeTail over CoeOut is that I'm not sure if Sym should be regarded as a subtype of Multiset exactly. :shrug:

[Kyle Miller]

Oh, CoeTail would be dangerous too. Never mind.

[Kyle Miller]

Johan Commelin said:

It doesn't like that the n in Sym alpha n doesn't appear in Multiset alpha... but I don't see why that should be problematic here.

Maybe it's that if transitive Coes are solved backwards, then this introduces a free n that can never be solved for.

[Johan Commelin]

Fair enough