Ulf Norell, would it make sense to give a special treatment for level metas wrt instance search? Records are very often parameterized by levels and it doesn't feel good to choose between universe polymorphism and instance search.