!4#4629 Cannot find synthesization order

Stream: mathlib4

[Pim Otte]

This instance in https://github.com/leanprover-community/mathlib4/pull/4629 is causing the following errors:

 Error: ./././Mathlib/RingTheory/Perfection.lean:387:0: error: cannot find synthesization order for instance charPmodP with type
  ∀ (K : Type u₁) [inst : Field K] (v : Valuation K ℝ≥0) (O : Type u₂) [inst_1 : CommRing O] [inst_2 : Algebra O K],
    Valuation.Integers v O → ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] [hvp : Fact (↑v ↑p ≠ 1)], CharP (ModP O p) p
all remaining arguments have metavariables:
  Field ?K
  @Algebra O ?K CommRing.toCommSemiring DivisionSemiring.toSemiring
  Fact (↑?v ↑p ≠ 1)

 Error: ./././Mathlib/RingTheory/Perfection.lean:387:0: error: cannot find synthesization order for instance charPmodP with type
  ∀ (K : Type u₁) [inst : Field K] (v : Valuation K ℝ≥0) (O : Type u₂) [inst_1 : CommRing O] [inst_2 : Algebra O K],
    Valuation.Integers v O → ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] [hvp : Fact (↑v ↑p ≠ 1)], CharP (ModP O p) p
all remaining arguments have metavariables:
  Fact (↑?v ↑p ≠ 1)

The following is the instance with variables written out:

instance charPmodP (K : Type u₁) [inst : Field K] (v : Valuation K ℝ≥0) (O : Type u₂) [inst_1 : CommRing O] [inst_2 : Algebra O K]
    [hp : Fact (Nat.Prime p)] [hvp : Fact (v p ≠ 1)] : CharP (ModP O p) p:=
  CharP.quotient O p <| mt hv.one_of_isUnit <| (map_natCast (algebraMap O K) p).symm ▸ hvp.1

I've tried playing with outparams and couldn't get it to work, but the thing that really boggles my mind is that it doesn't seem to pick up K as a variable, since it's complaining about it being a meta-variabele. Any pointers?