🧦 Splice Linter

[TOTBWF]

trafficstars

When constructing things inside of the splicer, it's easy to make mistakes and accidentally produce ill-typed terms, which can be really hard to debug. This is especially true when dealing with universes, as it's quite easy to forget an el_in/el_out somewhere and then spend a while reading bad do_el traces to figure out your mistake.

It would be nice to add some sort of optional "splice linter" that could typecheck any terms that it produces against a provided type. This could be used during development, hopefully making life a little less painful!

[favonia]

Is the following more radical approach possible? Give different OCaml types to genuine types and codes in universes.

[favonia]

Are you looking for a runtime checker or some magical OCaml GADT tricks?

[favonia]

Maybe we should just worship #189 and delete all the el_in and el_out...?