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. Jean-Alexandre ________________________________ From: Typer <typer-bounces@IRO.UMontreal.CA> on behalf of Stefan Monnier <monnier@IRO.UMontreal.CA> Sent: Tuesday, June 9, 2020 2:02 PM To: Jean-Alexandre Barszcz via Typer <typer@IRO.UMontreal.CA> Subject: Re: [Typer] [Git][monnier/typer][ja-barszcz] WIP WIP WIP
+ if not (is_typeclass t' ctx) then None else + match check_typeclass_match t t' lctx sl with + | Impossible -> None + (* | Possible -> None *) + | (Possible | Match) -> Some (i, elem, e, t') in
IIRC currently unification can have side-effects (instantiation of metavars) even if it fails, so we may need to be careful to undo them if we end up not using that unification's result. Stefan _______________________________________________ Typer mailing list Typer@iro.umontreal.ca https://mailman.iro.umontreal.ca/cgi-bin/mailman/listinfo/typer