experiment: use ctx dot instantiation

src/mo_frontend/bi_match.ml

@@ -72,13 +72,13 @@ let string_of_bounds (l, u) =
 
 (** Functions used only for debugging *)
 module Debug = struct
-  let print_solve ctx (ts1, ts2) must_solve =
+  let print_solve ctx (ts1, ts2) (must_solve : ConSet.t) =
     print_endline "solve ctx";
     print_endline (Printf.sprintf "var_list: %s" (String.concat ", " (List.map Cons.name ctx.var_list)));
     print_endline (Printf.sprintf "bounds: %s" (string_of_bounds ctx.bounds));
     print_endline (Printf.sprintf "variances: %s" (String.concat ", " (List.map (fun (c, t) -> Printf.sprintf "%s: %s" (Cons.name c) (Variance.string_of t)) (ConEnv.bindings ctx.variances))));
     print_endline (Printf.sprintf "subs: %s" (String.concat ", " (List.map (fun (t1, t2) -> Printf.sprintf "%s <: %s" (string_of_typ t1) (string_of_typ t2)) (List.combine ts1 ts2))));
-    print_endline (Printf.sprintf "must_solve : %s" (String.concat ", " (List.map string_of_typ must_solve)));
+    print_endline (Printf.sprintf "must_solve : %s" (String.concat ", " (List.map Cons.name (ConSet.elements must_solve))));
     verify_ctx ctx
 
   let print_variables_to_defer used to_defer to_solve =
@@ -362,19 +362,19 @@ let bi_match_typs ctx =
     Unused type variables can be deferred to the next round.
     [deferred_typs] are types to appear in the constraints of the next round. Used to determine which type variables to defer.
  *)
-let solve ctx (ts1, ts2) must_solve =
+let solve ctx (ts1, ts2) (must_solve : ConSet.t) =
   if debug then Debug.print_solve ctx (ts1, ts2) must_solve;
 
   (* Defer solving type variables that can be solved later. More constraints appear in the next round, let them influence as many variables as possible *)
-  let to_defer, defer_verify = if must_solve = [] then (ConSet.empty, false) else
+  let to_defer, defer_verify = if ConSet.is_empty must_solve then (ConSet.empty, false) else
     (* Type variables mentioned/used in subtyping constraints *)
     let cons1 = cons_typs ts1 in
     let cons2 = cons_typs ts2 in
     let used = ConSet.inter ctx.var_set (ConSet.union cons1 cons2) in
     let unused = ConSet.diff ctx.var_set used in
 
     (* Solve only variables that need to be solved now *)
-    let to_solve = cons_typs must_solve in
+    let to_solve = must_solve in
     (* Exclude variables that are not used in the constraints, it is better to raise an error than infer a default bound that could lead to confusing errors *)
     let to_solve = ConSet.diff to_solve unused in
     let to_defer = ConSet.diff ctx.var_set to_solve in
@@ -441,7 +441,7 @@ let solve ctx (ts1, ts2) must_solve =
           Format.asprintf "%a" display_rel (t1, "<:", t2))
           tts))))
 
-let bi_match_subs scope_opt tbs typ_opt =
+let bi_match_init scope_opt tbs typ_opt =
   (* Create a fresh constructor for each type parameter.
    * These constructors are used as type variables.
    *)
@@ -485,21 +485,31 @@ let bi_match_subs scope_opt tbs typ_opt =
     (Option.fold ~none:Any ~some:(open_ ts) typ_opt)
   in
   let ctx = { var_set; var_env; var_list = cs; bounds = (l, u); variances; to_verify = ([], [])} in
-
-  fun subs must_solve ->
-    let must_solve = List.map (open_ ts) must_solve in
-    let ts1 = List.map (fun (t1, _) -> open_ ts t1) subs in
-    let ts2 = List.map (fun (_, t2) -> open_ ts t2) subs in
-    let env, remaining = solve ctx (ts1, ts2) must_solve in
-    List.map (subst env) ts, remaining
+  ctx, ts
+
+let bi_match_subs scope_opt tbs typ_opt subs must_solve =
+  let ctx, ts = bi_match_init scope_opt tbs typ_opt in
+  let must_solve = List.map (open_ ts) must_solve in
+  let ts1 = List.map (fun (t1, _) -> open_ ts t1) subs in
+  let ts2 = List.map (fun (_, t2) -> open_ ts t2) subs in
+  let env, remaining = solve ctx (ts1, ts2) (cons_typs must_solve) in
+  List.map (subst env) ts, remaining
+
+let bi_match_receiver tbs (t1, t2) =
+  let ctx, ts = bi_match_init None tbs None in
+  let t1 = open_ ts t1 in
+  let t2 = open_ ts t2 in
+  let must_solve = ConSet.diff ctx.var_set (cons_typs [t1; t2]) in
+  let env, remaining = solve ctx ([t1], [t2]) must_solve in
+  List.map (fun t -> ConEnv.find_opt (as_con_var t) env) ts
 
 let finalize ts1 ctx subs =
   if is_ctx_empty ctx then begin
     assert (subs = []);
     ts1, ConEnv.empty
   end else begin
     (* Solve the 2nd round of sub-type problems *)
-    let env, remaining = solve ctx (List.split subs) [] in
+    let env, remaining = solve ctx (List.split subs) ConSet.empty in
 
     (* The 2nd round should not leave any remaining type variables *)
     assert (is_ctx_empty remaining);

src/mo_frontend/bi_match.mli

@@ -76,6 +76,11 @@ val bi_match_subs :
   typ list ->
   typ list * ctx
 
+val bi_match_receiver :
+  bind list ->
+  typ * typ ->
+  typ option list
+
 (** [finalize ts ctx subs] returns the final solution and the substitution of the remaining type variables from the 1st round.
   - [ts] is the solution from the 1st round
   - [ctx] is the remaining context for variables to be solved in this 2nd round

src/mo_frontend/typing.ml

@@ -1501,7 +1501,7 @@ let resolve_hole env at hole_sort typ =
 type ctx_dot_candidate =
   { module_name : T.lab;
     func_ty : T.typ;
-    inst : T.typ list;
+    inst : T.typ option list;
     module_ty : T.typ;
   }
 
@@ -1515,8 +1515,7 @@ let contextual_dot env name receiver_ty =
   (* Does an instantiation for [tbs] exist that makes [t1] <: [t2]? *)
   let permissive_sub t1 (tbs, t2) =
     try
-      let (inst, c) = Bi_match.bi_match_subs None tbs None [t1, t2] [] in
-      ignore (Bi_match.finalize inst c []);
+      let inst = Bi_match.bi_match_receiver tbs (t1, t2) in
       Some inst
     with _ ->
       None in
@@ -2623,14 +2622,24 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt =
     | TupE es when not parenthesized -> es
     | _ -> [exp2]
   in
-  let t_args, extra_subtype_problems = match ctx_dot with
-    | None -> t_args, []
-    | Some(e, t, _id, _inst) -> begin
+  let t_args, extra_subtype_problems, inst_ctx_dot = match ctx_dot with
+    | None -> t_args, [], None
+    | Some(e, t, _id, inst) -> begin
       match t_args with
-      | t'::ts -> ts, [(t, t')]
+      | t'::ts -> ts, [(t, t')], Some inst
       | [] -> assert false
     end
   in
+  let ctx_dot = Option.bind ctx_dot (fun (e, t, id, inst) -> 
+    if List.for_all Option.is_some inst then
+      Some (e, t, id, List.map Option.get inst)
+    else
+      None)
+  in
+  let dot_full_inst = match inst_ctx_dot with
+    | Some ts when List.for_all Option.is_some ts -> Some (List.map Option.get ts)
+    | _ -> None
+  in
   let saturated_arity, implicits_arity = arity_with_implicits t_args in
   let is_correct_arity =
     let n = List.length syntax_args in
@@ -2668,7 +2677,14 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt =
             warn env inst.at "M0223" "redundant type instantiation";
       ts, t_arg', t_ret'
     | _::_, None -> (* implicit, infer *)
-      infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems
+      match dot_full_inst with
+      | Some ts ->
+        let t_arg' = T.open_ ts t_arg in
+        let t_ret' = T.open_ ts t_ret in
+        if not env.pre then check_exp_strong env t_arg' exp2;
+        ts, t_arg', t_ret'
+      | None ->
+        infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems
   in
   inst.note <- ts;
   if not env.pre then begin

test/fail/ok/inf-error-small.tc.ok

@@ -1,37 +1,35 @@
-inf-error-small.mo:44.13-44.34: type error [M0098], cannot apply function `.get` of type
-  (n : Nat) -> ?Text
-to argument of type
+inf-error-small.mo:44.27-44.33: type error [M0050], literal of type
   Text
-to produce result of expected type
-  Text
-inf-error-small.mo:45.13-45.47: type error [M0098], cannot apply function `.get` of type
-  (compare : (implicit : (Nat, Nat) -> Order), n : Nat) -> ?Text
-to argument of type
-  ((n : Nat, m : Nat) -> Order, Text)
-to produce result of expected type
+does not have expected type
+  Nat
+inf-error-small.mo:45.40-45.46: type error [M0050], literal of type
   Text
-inf-error-small.mo:47.13-47.45: type error [M0098], cannot apply function `.get` of type
-  (compare : (implicit : (Nat, Nat) -> Order), n : Nat) -> ?Text
-to argument of type
-  ({map : [(Nat, [var Text])]}, Text)
-to produce result of expected type
+does not have expected type
+  Nat
+inf-error-small.mo:47.27-47.36: type error [M0096], expression of type
+  {map : [(Nat, [var Text])]}
+cannot produce expected type
+  (Nat, Nat) -> Order
+inf-error-small.mo:47.38-47.44: type error [M0050], literal of type
   Text
+does not have expected type
+  Nat
 inf-error-small.mo:48.26-48.58: type error [M0233], wrong number of arguments: expected 1 but got 3
 Expected 1 argument of type:
   (n : K)
 But got 3 arguments of type:
   {map : [(Nat, [var Text])]}
   (n : Nat, m : Nat) -> Order
   Text
-inf-error-small.mo:49.13-49.45: type error [M0098], cannot apply function `.get` of type
-  (compare : (implicit : (Nat, Nat) -> Order), n : Nat) -> ?Text
-to argument of type
-  ({map : [(Nat, [var Text])]}, Text)
-to produce result of expected type
+inf-error-small.mo:49.27-49.36: type error [M0096], expression of type
+  {map : [(Nat, [var Text])]}
+cannot produce expected type
+  (Nat, Nat) -> Order
+inf-error-small.mo:49.38-49.44: type error [M0050], literal of type
   Text
-inf-error-small.mo:51.13-51.29: type error [M0098], cannot apply function `.get` of type
-  (n : Nat) -> ?Text
-to argument of type
+does not have expected type
   Nat
-to produce result of expected type
+inf-error-small.mo:51.13-51.29: type error [M0096], expression of type
+  ?Text
+cannot produce expected type
   Bool

test/fail/ok/inf-error.tc.ok

@@ -7,15 +7,14 @@ to produce result of expected type
 inf-error.mo:48.13-48.39: type error [M0230], Cannot determine implicit argument `compare` of type
   (Any, Any) -> Order
 Hint: If you're trying to omit an implicit argument named `compare` you need to have a matching declaration named `compare` in scope.
-inf-error.mo:52.13-52.47: type error [M0098], cannot apply function `.get` of type
-  (compare : (implicit : (Nat, Nat) -> Order), n : Nat) -> ?Text
-to argument of type
-  ((n : Nat, m : Nat) -> Order, Text)
-to produce result of expected type
-  Any
-inf-error.mo:53.13-53.34: type error [M0230], Cannot determine implicit argument `compare` of type
-  (Any, Any) -> Order
-Hint: If you're trying to omit an implicit argument named `compare` you need to have a matching declaration named `compare` in scope.
+inf-error.mo:52.40-52.46: type error [M0050], literal of type
+  Text
+does not have expected type
+  Nat
+inf-error.mo:53.27-53.33: type error [M0050], literal of type
+  Text
+does not have expected type
+  Nat
 inf-error.mo:60.13-60.56: type error [M0098], cannot apply function of type
   (map : Map<K, V>, compare : (implicit : (K, K) -> Order), n : K, v : V) ->
     Map<K, V>
@@ -26,20 +25,15 @@ to produce result of expected type
 inf-error.mo:61.13-61.43: type error [M0230], Cannot determine implicit argument `compare` of type
   (Any, Any) -> Order
 Hint: If you're trying to omit an implicit argument named `compare` you need to have a matching declaration named `compare` in scope.
-inf-error.mo:63.13-63.51: type error [M0098], cannot apply function `.set` of type
-  (compare : (implicit : (Nat, Nat) -> Order), n : Nat, v : Text) ->
-    Map<Nat, Text>
-to argument of type
-  ((n : Nat, m : Nat) -> Order, Text, Text)
-to produce result of expected type
-  Any
-inf-error.mo:65.13-65.51: type error [M0098], cannot apply function `.set` of type
-  (compare : (implicit : (Nat, Nat) -> Order), n : Nat, v : Text) ->
-    Map<Nat, Text>
-to argument of type
-  ((n : Nat, m : Nat) -> Order, Text, Text)
-to produce result of expected type
-  Any
-inf-error.mo:66.13-66.38: type error [M0230], Cannot determine implicit argument `compare` of type
-  (Any, Any) -> Order
-Hint: If you're trying to omit an implicit argument named `compare` you need to have a matching declaration named `compare` in scope.
+inf-error.mo:63.40-63.46: type error [M0050], literal of type
+  Text
+does not have expected type
+  Nat
+inf-error.mo:65.40-65.46: type error [M0050], literal of type
+  Text
+does not have expected type
+  Nat
+inf-error.mo:66.27-66.33: type error [M0050], literal of type
+  Text
+does not have expected type
+  Nat

test/fail/ok/wrong-call-args.tc.ok

@@ -14,12 +14,10 @@ wrong-call-args.mo:35.12-35.14: type error [M0233], wrong number of arguments: e
 Expected 1 argument of type:
   (key : K)
 But got no arguments
-wrong-call-args.mo:39.5-39.31: type error [M0098], cannot apply function `.add` of type
-  (key : Text, value : Text) -> ()
-to argument of type
-  ((t1 : Text, t2 : Text) -> Order, Text)
-to produce result of expected type
-  ()
+wrong-call-args.mo:39.13-39.25: type error [M0096], expression of type
+  (t1 : Text, t2 : Text) -> Order
+cannot produce expected type
+  Text
 wrong-call-args.mo:45.5-45.17: type error [M0098], cannot apply function of type
   (map : Map<K, V>, compare : (implicit : (K, K) -> Order), key : K) -> ?V
 to argument of type

test/run/ok/contextual-dot.tc.ok

@@ -0,0 +1,8 @@
+contextual-dot.mo:50.33-50.40: type error [M0050], literal of type
+  Text
+does not have expected type
+  B
+contextual-dot.mo:56.39-56.46: type error [M0050], literal of type
+  Text
+does not have expected type
+  B

test/run/ok/contextual-dot.tc.ret.ok

@@ -0,0 +1 @@
+Return code 1