We could use https://github.com/astrieanna/TypeCheck.jl to get static guarantees that instances of theories were at least sort-correct. Could be pretty useful.