Adding coercions mechanism

[gabrielhdt]

This pull request adds a coercion mechanism on top of the new typechecker. Adding such a mechanism involves:

• creating a new symbol in its own signature that stands for the coercion operator (it is noted #c).
• allowing the type checker to call unification while typechecking (a coercion t: a == b is triggered only if a cannot be unified with b). To avoid lifting the typechecker into a functor (parametrised by the unification algorithm), a reference is used Infer.solve.
• since unification isn't postponed, some equations may need other equations to be solved. A new function solve1 tries to solve the global problem including a new constraint which may be unsolvable. Such a mechanism requires the unification algorithm to not backtrack (which must be already the case).

Regarding the last topic, for the moment solve1 considers that if the unification fails, it must be because of the new equation. But it may not be the case. Perhaps the equation is solved, but others cannot be solved yet. It seems that to be able to make the distinction, we should be able to trace where new constraints are coming from.

It should also be noted that for the moment, no coercion can be done at the level of types. For this, we'd like to enter the coercion #c Set $a TYPE --> El $a but TYPE is not (yet) in the language of patterns accepted by the decision tree compiler.

Remaining:

• [x] The coercion operator should have the rule #c $a $t $a --> $t built in.
• [x] Collect metavariables that may be generated when coercions are reduced.
• [x] Protected symbols shouldn't appear in coerced terms.
• [ ] Update CHANGES.md, lambdapi.bnf and user manual.

[gabrielhdt]

It seems to me that as of https://github.com/Deducteam/lambdapi/pull/809/commits/d405f4d3aa8c11e604ce0df765390449bb2c6a17, the algorithm is ready. What lacks is to be able to parametrise reduction to not reduce protected symbols. But this can be done in a follow-up pull request. What are your thoughts @fblanqui?

[gabrielhdt]

There seem to be no impact performance-wise.

[fblanqui]

@gabrielhdt Let me know when this PR will be up to date and ready for review.

[fblanqui]

Is this PR still necessary?

[gabrielhdt]

No it isn't. It contains the redopaque mechanism, and I use it to type check PVS files, but it should not be merged anyway.