9 Jui
2020
9 Jui
'20
15:48
Yes, the unification done by `check_typeclass_match` might instantiate some metavariables, but I've changed it so that it only instantiates the metavariables that we create during the instance search (those in the current scope level). Since those new metavars can only appear in the candidate instance, and nowhere else, the side-effects are not "visible" outside of the instance search and we do not need to worry about undoing anything.
Great! Please mention this in a comment in the code.
Stefan