Allow "impredicative" universe polymorphism

* samples/hurkens.typer (𝓅): Make it universe-polymorphic.

* src/elab.ml (infer_level): New function.
(sform_type): Use it.

* src/log.ml (log_fatal): Set print_at_log before calling log_msg so
the message is printed before raising the exception, otherwise it's lost.

* src/opslexp.ml (deep_universe_poly): New const.
(sort_compose): Add one more context for k2.  Fix k2 scoping.
Obey deep_universe_poly.