AFAIK the Agda implementations use a closed universe of types and cannot be translated to an implementation of runST in Haskell which doesn't have that restriction. Please correct me if I'm wrong. From a quick reading I can't tell if the new paper makes progress on that front, what do you think?