universe 変数（宇宙多相性）が重要になる例

HasParser で Type もパースしたいことがある (lean-update から出てきた例)

module

/-- A type that can be parsed from a string. -/
public class HasParser (α : Type u) where
  parse : String → Except String α

/-- Parse a string as a value of the given type. -/
public def parseAs (α : Type u) [HasParser α] (s : String) : Except String α :=
  HasParser.parse s

/-- parse a string into a `Bool` -/
public def Bool.parse (s : String) : Except String Bool :=
  match s.toLower with
  | "true" => .ok true
  | "false" => .ok false
  | _ => throw s!"Invalid boolean value: '{s}'. Allowed values are 'true' and 'false'."

public instance : HasParser Bool where
  parse := Bool.parse

public instance : HasParser System.FilePath where
  parse s := .ok (System.FilePath.mk s)

/-- parse a string into a `Type` -/
public def Type.parse (s : String) : Except String Type :=
  match s with
  | "Bool" => .ok Bool
  | "FilePath" => .ok System.FilePath
  | "String" => .ok String
  | _ => throw s!"Invalid type: {s}. The parser of this type is not implemented."

public instance : HasParser Type where
  parse := Type.parse

Start with the HasParser and Type.parse example included in the issue, then inspect how examples are organized in lean-by-example. Add a clear example explaining when the universe variable matters and verify that the Lean code builds; the issue is done when the example demonstrates universe polymorphism without ambiguity.