The call argument names the parameter, and the condition states the rule

Two of the audit's top five, and both are the same complaint: the message
states a type fact and stops where the reader needed the other half.

A call argument's refusal now says which argument of which function it is and
notes the parameter's own declaration, which is [declared_note]'s shape moved
to the place the audit calls the most-hit message in the compiler. [fns]
threw the parameter names and locations away when it resolved the types, so
[fparams] keeps the vector as written; a foreign declare and a generic copy
have no entry and degrade to the message alone rather than a wrong pointer.
The enrichment is conditional on the refusal being raised against the
argument's own span, so a mismatch deeper inside it is not misattributed, and
the rekind stops a nested call being named twice.

A condition that is neither bool nor dyn now states the rule instead of the
fact, with the comparison spelled out using the condition's own name where it
has one. Two things it does not do: it does not offer a comparison for a type
that has no zero, and it does not say anything about the dyn side, where
Clojure's truthiness means 0 is true. The re-check at bool still runs first
and its answer is kept wherever it knows more — a literal names itself, and
[None] names itself, and both beat a type name.

lib/check.ml

@@ -79,6 +79,15 @@ type env = {
      the symbol and nothing else. *)
   extern_locs : (string, Loc.t) Hashtbl.t;
   fns     : (string, Types.t list * Types.t) Hashtbl.t;
+  (* The parameter vector as it was *written*, by function name: the names and
+     the locations [fns] threw away when it resolved the types. Nothing needs
+     it to compile; it exists so that a refusal at a call argument can point
+     at the parameter that wanted the other type, which is the second half of
+     every message in Elm and was the one thing the reader could not see from
+     the caret. Missing for a foreign [declare] and for a generic copy, and a
+     missing entry degrades to the message alone rather than to a wrong
+     pointer — [declared_note]'s rule. *)
+  fparams : (string, Ast.field list) Hashtbl.t;
   globals : (string, Types.t * bool) Hashtbl.t;   (* type, is a constant *)
   (* Functions the checker made up: a handler-bind clause is lifted into one,
      because a handler is called from wherever the signal was and cannot be a
@@ -145,6 +154,7 @@ let new_env () = {
   externs = Hashtbl.create 32;
   extern_locs = Hashtbl.create 32;
   fns     = Hashtbl.create 32;
+  fparams = Hashtbl.create 32;
   globals = Hashtbl.create 16;
   lifted = [];
   generics = Hashtbl.create 8;
@@ -1986,8 +1996,12 @@ let expect ctx loc ~want (got : Tast.expr) =
     in
     if Types.fits ~expected:w ~actual:got.Tast.ty then got
     else
-      fail loc "expected %s, found %s" (Types.to_string w)
+      (* Kinded so that the one caller who knows more — a call argument, which
-        (Types.to_string got.Tast.ty)
+         can name the function and the parameter — can recognise this exact
+         refusal at this exact span and say the rest. Every other reader of a
+         diagnostic ignores [kind]. *)
+      Loc.failk "check/type-mismatch" loc "expected %s, found %s"
+        (Types.to_string w) (Types.to_string got.Tast.ty)
 
 (* Something a [break] may not jump out of, named so the refusal can say which.
    See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@@ -3730,7 +3744,46 @@ and check_truthy ctx c =
   | c0 when c0.Tast.ty = Types.Dyn ->
     widen loc Types.Bool (rt loc (Types.Int Types.I32) "flan_dyn_truthy" [ c0 ])
   | c0 when Types.fits ~expected:Types.Bool ~actual:c0.Tast.ty -> c0
-  | _ -> check ctx ~want:Types.Bool c
+  | c0 ->
+    (* Re-checked at [bool] first, and the answer is kept only when it is a
+       message that knows something this one does not: a literal names itself
+       ("found the integer literal 1"), and [None] names itself, and both of
+       those point at the mistake better than a type name would. What comes
+       back as the *generic* mismatch — "expected bool, found i32", which is
+       true and tells a reader nothing they did not have — is the one replaced
+       below.
+
+       The rule, rather than the fact. [expected bool, found i32] is true and
+       says nothing a reader did not already know; what they do not know is
+       that this language has exactly two things a condition may be, and that
+       the dyn one is not the typed one. A dyn condition is Clojure's — nil
+       and false are false and 0 is true — so a message that told somebody to
+       compare against zero *in general* would be wrong about half the
+       language. It is said only of the typed side, which is where they are.
+
+       The comparison is spelled with the condition's own name where there is
+       one, because [(not= x 0)] is a thing to type and [(not= … 0)] is not.
+       Anything more complicated than a name gets the operator and no
+       template: a reconstructed expression would be a guess at code the
+       reader can see for themselves. *)
+    (match check ctx ~want:Types.Bool c with
+     | c1 -> c1
+     | exception Loc.Error d when not (String.equal d.Loc.kind "check/type-mismatch") ->
+       raise (Loc.Error d)
+     | exception Loc.Error _ ->
+    let how =
+      let zero = match c0.Tast.ty with Types.Float _ -> "0.0" | _ -> "0" in
+      let comparable =
+        match c0.Tast.ty with Types.Int _ | Types.Float _ -> true | _ -> false
+      in
+      match c.Ast.e, comparable with
+      | Ast.Var n, true -> Printf.sprintf " — test it, as (not= %s %s)" n zero
+      | _, true -> Printf.sprintf " — test it against %s with not=" zero
+      | _ -> ""
+    in
+    Loc.failk "check/condition-not-bool" loc
+      "a condition is a bool or a dyn, and this is %s%s"
+      (Types.to_string c0.Tast.ty) how)
   | exception Loc.Error _ -> check ctx ~want:Types.Bool c
 
 and check_if ctx ?(tail = false) ?want loc c t e =
@@ -4208,6 +4261,45 @@ and unknown_name : 'a. ctx -> Loc.t -> string -> 'a =
       Loc.failk "check/unknown-name" loc "unknown name %s — did you mean %s?" name m
     | None -> Loc.failk "check/unknown-name" loc "unknown name %s" name
 
+(* 1st, 2nd, 3rd, and every other one. *)
+and ordinal n =
+  let suffix =
+    if n mod 100 >= 11 && n mod 100 <= 13 then "th"
+    else match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th"
+  in
+  string_of_int n ^ suffix
+
+(* Check one argument of a call to [name], and if the refusal is the plain
+   type mismatch raised against *this* argument's own span, say the two things
+   the caret cannot: which argument of which function this is, and where the
+   parameter that wanted the other type is declared.
+
+   The span test is what keeps the claim true. A mismatch deeper inside the
+   argument — an element of a vec literal, an argument of a nested call — is
+   raised against its own location and is re-raised untouched, because calling
+   that "the 2nd argument of add" would be a sentence that reads well and
+   points at the wrong form. The rekind is what stops a nested call from being
+   named twice: once enriched, it is no longer the kind this looks for. *)
+and check_arg ctx name i (want : Types.t) (a : Ast.expr) =
+  match check ctx ~want a with
+  | e -> e
+  | exception Loc.Error d
+    when String.equal d.Loc.kind "check/type-mismatch"
+         && d.Loc.dloc == a.Ast.loc ->
+    let which = ordinal (i + 1) in
+    let notes =
+      match Hashtbl.find_opt ctx.env.fparams name with
+      | Some ps when List.length ps > i ->
+        let p = List.nth ps i in
+        [ Loc.note p.Ast.floc
+            (Printf.sprintf "%s's %s parameter %s is declared %s"
+               name which p.Ast.fname (Types.to_string want)) ]
+      | _ -> []
+    in
+    Loc.raise_diag
+      (Loc.diag ~kind:"check/argument-type" ~notes a.Ast.loc
+         (Printf.sprintf "%s — this is the %s argument of %s" d.Loc.dmsg which name))
+
 and fields_named env n : Tast.structure option =
   match Hashtbl.find_opt env.structs n with
   | Some s -> Some s
@@ -6472,7 +6564,10 @@ and named_call ctx ~want loc name args =
           (List.length params)
           (if List.length params = 1 then "" else "s")
           (List.length args);
-      let args = map2_lr (fun p a -> check ctx ~want:p a) params args in
+      let i = ref (-1) in
+      let args =
+        map2_lr (fun p a -> incr i; check_arg ctx name !i p a) params args
+      in
       expect ctx loc ~want (mk loc ret (Tast.Call (name, args)))
     | None ->
       if Hashtbl.mem ctx.env.datas name then
@@ -7382,7 +7477,10 @@ let collect env (decls : Ast.decl list) =
          in
          env.tyvars <- [];
          env.tvpreds <- [];
-         if vars = [] then Hashtbl.replace env.fns fn.Ast.name (params, ret)
+         if vars = [] then begin
+           Hashtbl.replace env.fns fn.Ast.name (params, ret);
+           Hashtbl.replace env.fparams fn.Ast.name fn.Ast.params
+         end
          else begin
            Hashtbl.replace env.generics fn.Ast.name fn;
            Hashtbl.replace env.gsigs fn.Ast.name (vars, params, ret)

test/test_flan.ml

@@ -3690,6 +3690,60 @@ let () =
       | _ -> check "an unknown field has one note" false)
    | None -> check "an unknown field is refused" false);
 
+  (* The call argument, which is the most-hit refusal in the compiler and was
+     the one that said least: the caret was right and the sentence never named
+     which argument of which function, nor pointed at the parameter that
+     wanted the other type. Both halves are asserted here, plus the rule that
+     keeps the claim honest — a mismatch *inside* an argument is not this
+     argument's, and is left as it was. *)
+  (match diag_of "(defn add [a i32 b i32] i32 (+ a b))\n                  (defn f [] i32 (add 1 \"two\"))" with
+   | Some d ->
+     check "a bad call argument has a kind" (d.Loc.kind = "check/argument-type");
+     check "and says which argument of which function"
+       (contains d.Loc.dmsg "this is the 2nd argument of add");
+     (match d.Loc.notes with
+      | [ n ] ->
+        check "and notes the parameter's declaration" (n.Loc.nloc.Loc.line = 1);
+        check "and names the parameter"
+          (contains n.Loc.nmsg "add's 2nd parameter b is declared i32")
+      | _ -> check "a bad call argument has one note" false)
+   | None -> check "a bad call argument is refused" false);
+  (match diag_of "(defn add [a i32 b i32] i32 (+ a b))\n                  (defn f [] i32 (add 1 (add 2 \"x\")))" with
+   | Some d ->
+     let times needle hay =
+       let n = String.length needle in
+       List.length
+         (List.filter
+            (fun i -> String.length hay - i >= n && String.sub hay i n = needle)
+            (List.init (max 1 (String.length hay)) Fun.id))
+     in
+     (* Named once, by the call that owns it. The outer call sees a refusal
+        raised against a span that is not its argument's and passes it on
+        untouched, which is what stops "the 2nd argument of add" being said
+        twice about two different forms. *)
+     check "the inner call owns its own argument, and says so once"
+       (times "argument of add" d.Loc.dmsg = 1)
+   | None -> check "a nested bad argument is refused" false);
+
+  (* The condition, which used to state a type fact and stop. The rule has two
+     halves and the dyn half is not the typed half — a dyn condition is
+     Clojure's, where 0 is true — so the comparison is offered only where it
+     is right, and with the condition's own name where it has one. *)
+  rejects_check "a non-bool condition states the rule"
+    "(defn f [] i32 (let [x 1] (if x 1 0)))"
+    ~needle:"a condition is a bool or a dyn, and this is i32 — test it, as (not= x 0)";
+  rejects_check "and offers no template for a form it cannot name"
+    "(defn f [] i32 (if (+ 1 2) 1 0))"
+    ~needle:"this is i32 — test it against 0 with not=";
+  rejects_check "and offers no comparison at all for a type that has none"
+    "(defstruct P [x i32]) (defn f [] i32 (let [p (P {.x 1})] (if p 1 0)))"
+    ~needle:"a condition is a bool or a dyn, and this is P";
+  (* A literal still names itself: that message knows something the rule does
+     not, so the re-check's answer is kept wherever it is more specific. *)
+  rejects_check "a literal condition keeps its own message"
+    "(defn f [] i32 (if 1 1 2))"
+    ~needle:"expected bool, found the integer literal 1";
+
   (* The reader's own two-place error. The bracket that is open is the error
      and the end of input is the note, because the fix goes at the first and
      the surprise is at the second. *)