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