[wip] improve Elpi elaborator

[gares]

Changes:

• CHR rule to propagate restrictions from a "refined evar" Y to the "raw one" X in evar X T Y. The point is that Y can occur elsewhere, and unif can restrict it. The CHR rule for UT uses Y's scope to operate, and if X is larger we don't know what to do. So we immediately restrict X whenever Y is.
  Todo:
• coercions (not very well tested)
• TC (only for non hint extern, should be reasonably easy)
• CS (should be easy)
• error messages. That is the pink elephant. I guess adding a type loc loc -> term -> term would be step 0, the one would need a more efficient implementation of safe or some auxiliary API to close wrt the context, since now it only supports ground terms, eg strings, but during elaboration one may want to just store the (non-ground) data needed in order to print an error (for efficiency). Syntactic Constraints kind of do that, but how to use them is not 100% clear yet (they key is simple, but not ground either, unless you don't key them...)