universe polymorphic Mutex

Stream: lean4

[Yuri]

Note: I am aware of recent discussions about universe polymorphic IO and the fact that this is not simple and on the radar.

Considering that IO.Mutex is not universe polymorphic, how to mutually exclude a universe polymorphic structure? Are there work arounds to make something like this to work?

The specific example is this:

structure AsyncTask (α : Type) where
  future : Future α

abbrev AnyTask := List <| Σ (α : Type), AsyncTask α

structure TaskManager where
  tasks : IO.Mutex AnyTask

Error:

application type mismatch
  IO.Mutex AnyTask
argument
  AnyTask
has type
  Type 1 : Type 2
but is expected to have type
  Type : Type 1

At the end of the day, I would like to create data structures similar to Vec<Box<dyn ATrait + 'a>> in Rust.