Can I use this library to implement type elaboration?

[bglgwyng]

More specifically, I'm trying to implement Higher-Order Pattern Unification using propagator.
At first, I thought it would be straightforward, however after I played with holmes for a while now I'm a bit uncertain about this approach

To implement HOPU, I need to be able to add meta-variables dynamically, but Holmes demands that I initialize at the beginning by configuring Config. The solutions I think of are

• use internal functions instead of satisfying and deal with MoriarT
• use .>>=? It may not be used to introduce new metavars.

Also, I considered defining new semi-lattice definition that supports a recursive structure that can write a constraint like

Exactly (Unkown, Exactly 2) .== Exactly (Exactly 1, Unkown) -- imagine unifying (?1, 2) = (1, ?2)

which doesn't make sense in the current Defined. However, I'm not sure such a definition works well with propagator. From my understanding, the meta-variables should be flattened and put into the initial configuration for now.

Does anyone have ideas? Or do we have some examples of type checker based on propagator?