Typeclass instance with parametrized types

Stream: lean4

[Andrés Goens]

I can't get typeclasses to work with types that depend on parametrized types (e.g. with variable). Here's an MWE:

variable {ParametrizedType : Type 0} [BEq ParametrizedType]

inductive Foo
  | constr₁ : ParametrizedType → Foo
  | constr₂ : ParametrizedType → Foo
  deriving BEq

instance : (BEq (@Foo ParametrizedType)) where beq := λ f₁ f₂ => match f₁, f₂ with
  | .constr₁ t₁, .constr₁ t₂ => t₁ == t₂
  | .constr₂ t₁, .constr₂ t₂ => t₁ == t₂
  | _, _ => false

def foosEqual (foo₁ foo₂ : @Foo ParamtrizedType) : String :=
  if foo₁ == foo₂ then "yes" else "no"
  -- if BEq.beq foo₁ foo₂ then "yes" else "no" -- also doesn't work

Am I missing something here?

[Andrés Goens]

I've tried both deriving and manually specifying the instance and both don't seem to work

[Sebastian Ullrich]

You misspelled your last ParametrizedType as ParamtrizedType