9 Jui
2020
9 Jui
'20
14:02
+ 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