You either need to unfold all solved metas in core syntax ("zonking"), or remember types of metas. Neither are too complicated but I prefer the latter, because zonked syntax is cluttered, and typed metas are needed anyway for more sophisticated unification.
Conversation
But in the absence of glued evaluation, meta solutions and their types are always greatly bloated.
3
1
My plan is to eventually head towards gluing, so yeah, maybe I’ll go with the latter option. Thanks again for all your help!
1
Would doing the latter option mean that I wouldn’t be able to easily synthesise the type of a hole (a metavariable)? Because then I’d need to know what level of type metavariable is at?
1
I'm not sure about your question, but you always need to return a type when synthesizing a hole, and saving metas doesn't affect this. Hole synthesizing creates at least two metas, one for the hole and one for its type.
1
It’s the second one I’m interested in: what type do I give it in the metavariable environment? I have universe levels, so I can’t just use it `Type`
1
1
Oh right. Unfortunately, you need one more meta for the level (yeah levels are painful). In Agda, levels are handled like any other term and have type Set-omega. I *think* in Idris there's a separate metacontext just for levels.
1
1
Hehe, oh dear... yeah I was hoping to avoid fancy level unification :3. Hum. Interesting! Will have a think about this!
1
If you don't have cumulativity, level polymorphism and level bounds, then level unification can stay dumb and simple (contrast Agda/Coq level solving), but then it's annoying to use. Why not go with type-in-type?
1
3
Idris maintains a graph of level constraints then solves later, which is a bit of a pain. For a programming language (rather than theorem prover) I don't think type-in-type loses enough to worry about. Though others may argue with this...
2
6
I hoped to use a McBride-style shifting operator - it seems like it could be nice without being too tricky impl wise (NbE not withstanding). The annoying thing is that it seems I'd probably only need this universe level unification for validating my elaborated syntax… 🤔