Switch to an explicitly typed core language

[brendanzab]

This switches the core language to be explicitly typed, which might make compilation easier down the line, for example when figuring out if we need to compile to a term or a type. I remember this was tricky on my last time trying to implementing compilation/extraction, but I’d like to do some more experiments to see if this is actually the case, however, but this at least demonstrates the idea.

The resulting terms are a bit larger than I’d like, because we need to quote type annotations back to terms during elaboration. Glued evaluation potentially help here.

Closes #270

[Kmeakin]

Looks like a scoping error has been introduced somewhere?
Should be fun (A : Type) (a : A) => a : fun (A : Type) -> A -> A

[brendanzab]

ooooh yes you are right. wouldn't it be great if there was a way to ensure these were well scoped… 😅

[brendanzab]

I think it might be to do with when the function parameter types are quoted but I'll have a look

[brendanzab]

Was actually an issue in the distiller, which would have been a bit trickier to catch, alas. Perhaps with some sort of roundtrip test maybe.

[Kmeakin]

The resulting terms are a bit larger than I’d like, because we need to quote type annotations back to terms during elaboration. Glued evaluation potentially help here.

Should be fixed by #462? I'd like to see this merged

[brendanzab]

Hmm, not sure. I think most of the bloat added here is from terms that do not come from user code originally. Because they have been quoted from values, they would need something like glued evaluation to keep them small. Does having explicit type annotations help you in something you are looking at? Should we try to get this merged?

[Kmeakin]

Does having explicit type annotations help you in something you are looking at? Should we try to get this merged?

No, I just wanted symmetry with the type annotations in FunType. But if you want to let it cook longer, no pressure