equal
deleted
inserted
replaced
356 | INVARIANT => (cs, strong_unify ctxt constraint tye_idx |
356 | INVARIANT => (cs, strong_unify ctxt constraint tye_idx |
357 handle NO_UNIFIER (msg, _) => |
357 handle NO_UNIFIER (msg, _) => |
358 error (gen_msg err ("failed to unify invariant arguments" ^ msg)))); |
358 error (gen_msg err ("failed to unify invariant arguments" ^ msg)))); |
359 val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack)) |
359 val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack)) |
360 (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx))); |
360 (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx))); |
361 val test_update = is_compT orf is_freeT orf is_fixedvarT; |
361 val test_update = is_typeT orf is_freeT orf is_fixedvarT; |
362 val (ch, done') = |
362 val (ch, done') = |
363 if not (null new) then ([], done) |
363 if not (null new) then ([], done) |
364 else split_cs (test_update o Type_Infer.deref tye') done; |
364 else split_cs (test_update o Type_Infer.deref tye') done; |
365 val todo' = ch @ todo; |
365 val todo' = ch @ todo; |
366 in |
366 in |