bizarre universe error

Stream: mathlib4

[Antoine Chambert-Loir]

In order to generalize docs#Module.forall_dual_apply_eq_zero_iff to the noncommutative setting (don't ask why, except that linear algebra works over division rings), I tried the following, and I get an error
declaration _example contains universe level metavariables at the expression
which I don't understand.

import Mathlib.RingTheory.Finiteness.Projective
import Mathlib.LinearAlgebra.Dual.Basis

open Module

universe uK uV
variable {K : Type uK} {V : Type uV}

variable [Semiring K] [AddCommMonoid V] [Module K V] [Module.Projective K V]

example (v : V) :  (∀ f : Dual K V, f v = 0) ↔ v = 0 := by
  let ⟨s, hs⟩ := Module.projective_def'.mp ‹Projective K V›
  refine ⟨fun hv ↦ ?_, fun hv ↦ by simp [hv]⟩
  rw [← LinearMap.id_apply (R := K) v, ← hs, LinearMap.coe_comp, Function.comp_apply]
  apply Finset.sum_eq_zero
  intro x _
  convert zero_smul
  suffices s v x = 0 by simp [this]
  simpa using hv (Finsupp.lapply x ∘ₗ s)

[Antoine Chambert-Loir]

(I hadn't noticed docs#Projective.exists_dual_ne_zero , but that doesn't explain the error neither.)

[Joël Riou]

The issue is with convert zero_smul: Lean may be unable to find the implicit parameters (let alone the universe they belong).
The code seems to work without the convert zero_smul line.

[Antoine Chambert-Loir]

Thanks!