unassigned metavariable in out-param

Stream: mathlib4

[Kevin Buzzard]

I've made huge progress today in understanding typeclass inference and the dangerous instance linter, but this one still eludes me. This comes up in mathlib4#1636, and I can't get rid of the lint error (I've tried various permutations).

import Mathlib.Order.Hom.Basic

class SupHomClass (F : Type _) (α β : outParam <| Type _) [HasSup α] [HasSup β] extends
  FunLike F α fun _ => β where
  map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b

class SupBotHomClass (F : Type _) (α β : outParam <| Type _) [HasSup α] [HasSup β] [Bot α]
  [Bot β] extends SupHomClass F α β where
  map_bot (f : F) : f ⊥ = ⊥

instance (priority := 100) OrderIsoClass.toSupBotHomClass {_ : SemilatticeSup α} {_ : OrderBot α}
    {_ : SemilatticeSup β} {_ : OrderBot β} [OrderIsoClass F α β] : SupBotHomClass F α β :=
sorry

#lint only dangerousInstance
/- 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 @OrderIsoClass.toSupBotHomClass /- unassigned metavariable in out-param: SupBotHomClass F α β -/

I searched the chat for unassigned metavariable in out-param and got two hits but they didn't help me :-/

[Kevin Buzzard]

Actually, it looks the same as this. @Anne Baanen do you know how to fix this issue?

[Kevin Buzzard]

Oh! My understanding is that the fix is @[nolint dangerousInstance] even though the instance is dangerous? @Gabriel Ebner would you agree with this? See here for possibly analogous shenannigans in mathlib4 master (the porting note at the end in particular).

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

Ah, the linter doesn't figure out that unification will assign the metavariable using nested TC synthesis.

[Kevin Buzzard]

So I can nolint safely?

[Gabriel Ebner]

I think so.