> It turns out that it is possible if you do it in a special way with locales

What was special about it? From memory, the formalisation [1] proceeded exactly how you would expect. Locales are simply an Isabelle mechanism (in addition to type classes) through which hierarchies of structures are built up.

[1]: https://www.isa-afp.org/entries/Grothendieck_Schemes.html