equal
deleted
inserted
replaced
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_typeT 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 done |
364 else split_cs (test_update o Type_Infer.deref tye') done; |
364 |> map (apfst (pairself (Type_Infer.deref tye'))) |
|
365 |> (if not (null new) then rpair [] else split_cs test_update); |
365 val todo' = ch @ todo; |
366 val todo' = ch @ todo; |
366 in |
367 in |
367 simplify done' (new @ todo') (tye', idx') |
368 simplify done' (new @ todo') (tye', idx') |
368 end |
369 end |
369 (*xi is definitely a parameter*) |
370 (*xi is definitely a parameter*) |