src/Tools/subtyping.ML
changeset 49142 0f81eca1e473
parent 47060 e2741ec9ae36
child 49560 11430dd89e35
equal deleted inserted replaced
49141:aca966dc18f6 49142:0f81eca1e473
   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