--- a/src/HOL/Library/adhoc_overloading.ML Tue Apr 16 17:28:58 2024 +0200
+++ b/src/HOL/Library/adhoc_overloading.ML Wed Apr 17 15:04:27 2024 +0200
@@ -154,7 +154,9 @@
fun get_candidates ctxt (c, T) =
get_variants ctxt c
|> Option.map (map_filter (fn (t, T') =>
- if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
+ if unifiable_with (Proof_Context.theory_of ctxt) T T'
+ (*keep the type constraint for the type-inference check phase*)
+ then SOME (Type.constraint T t)
else NONE));
fun insert_variants ctxt t (oconst as Const (c, T)) =