Recover arbitrary type from attribute data

Stream: lean4

[Thomas Murrills]

I'm in a situation where I need to somehow bundle a type into the data recorded by an attribute, and then recover this type in CommandElabM. For example, I was trying to do something schematically like

structure MyData where
  carrier : Type
  -- other meaningful fields which depend on `carrier`

@[my_attr specific_instance]
def specificData where carrier := sorry

-- e.g., ``specificName := `specific_instance`` returns `specificData`
def getMyDataFromMyAttr : Name → CommandElabM MyData := sorry

def useMyAttr (specificName : Name) : CommandElabM Unit := do
  let myData : MyData ← getMyDataFromMyAttr specificName
  ...

The issue is that MyData lives in too big a universe for CommandElabM, which can only use a Type, so (the type of) getMyDataFromMyAttr can't even be written down. I don't think I can give MyData a parameter, either, because uses of getMyDataFromMyAttr have no way of inferring this type from the Name argument, which is all that's accessible at the point of use.

I think I can find a workaround for my particular use case, but it's a little inelegant (involving aux decls), and I was wondering what the recommended way of dealing with this kind of situation was.

Is this a case of "you probably don't really want to do that"? Is the restriction of Lean monads like CommandElabM to Type real or artificial? And is there a standard way around this?

[Eric Wieser]

I have an RFC and example patch open against Lean for making IO universe-parametrized (lean4#3011), from which presumably all the other Monads could follow