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.
Conversation
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
What in particular were you interested in learning about?
1
Are you interested in these in relation to dependent type system implementation? You can get by without unification (see Dhall), but it means you have to be more explicit. Doing stuff like `id String "hello"` can get annoying after a while.
1
Hindley Milner type inference is one common example of a type checking algorithm that uses unification/constraint solving, but the design decisions it makes don't really scale to more interesting type systems, like those with dependent types.
So eventually you end up with a foundation built on bidirectional type checking (like in andres-loeh.de/LambdaPi/), and some higher-order unification (see example here github.com/AndrasKovacs/m).
1
I have some more examples in this issue too: github.com/pikelet-lang/p