diff --git a/TODO.org b/TODO.org index 899c9b6e..0a5e280d 100644 --- a/TODO.org +++ b/TODO.org @@ -767,12 +767,6 @@ clause here admits nothing but type predicates. Whether it should take value predicates over a length parameter deserves answering deliberately rather than falling out of the implementation. -** TODO "In instantiation of" notes -A refusal inside a copy points at the generic's source with no note naming the -call site that asked for that type. The data is there — =instantiation_origin= -exists and the session already uses it — and wiring it into every failure under an -instantiation is a lane of its own. - ** DONE A program is one compilation, so a generic's body is always visible CLOSED: [2026-09-25] Odin's and Zig's model: packages are never compiled separately. The cost is build @@ -1030,15 +1024,6 @@ ignore order, writable access has to alias the real storage. Flexible field orde waits for classes deliberately, because a class owns its layout and a =Vector2= should not pay for identity and metadata. Not implemented. -** TODO An error in a called generic's body is reported twice -=(defn g [x $t] u64 (nosuch x))= called once from =main= prints "unknown -function nosuch" twice at the same place and counts 2 errors — once from the -abstract pass and once from the instantiation. - -** TODO A type variable is printed without its $ -=Types.to_string= prints =Var t= as =t=, so a refusal reads "selection-sort -expects [t] here, found [3 i32]" where the source wrote =[$t]=. - ** DONE Two refusals suggested something that does not compile CLOSED: [2026-09-25] =vec-new= and =map-new= with no type no longer say "or give the binding a type"; diff --git a/lib/check.ml b/lib/check.ml index ee0c4daf..0c03ca82 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -192,6 +192,12 @@ type env = { chain. Odin has no cap of its own to copy, so there was nothing to borrow. *) mutable chain : (string * Types.t list * Loc.t) list; + (* Generics whose abstract pass was refused and recorded, in a whole-file + check that goes on after a refusal. A call site still gets a copy's + signature, but its body is not checked again: every refusal the abstract + pass made would come back from the copy, at the same line, once per type + it was called at. *) + refused_generics : (string, unit) Hashtbl.t; (* Set while a struct, data-case or union field's type is being resolved, and only then. It exists for one message: an unknown lowercase name in a type slot is told to introduce a type variable with [$name] in the @@ -240,6 +246,7 @@ let new_env () = { subst = []; tvpreds = []; chain = []; + refused_generics = Hashtbl.create 4; in_field = false; classes = Hashtbl.create 8; tracks = Hashtbl.create 16; @@ -2157,7 +2164,7 @@ let unconstrained env loc op ~needs (t : Types.t) = | _ -> Loc.failk "check/unconstrained-type-variable" loc "%s over the type variable %s: nothing declares %s %s. Write \ - {:where (%s $%s)} at the head of the body, or take the operation as \ + {:where (%s %s)} at the head of the body, or take the operation as \ a parameter, a (Fn [%s %s] ...), and call it here" op (Types.to_string t) (Types.to_string t) needs needs (Types.to_string t) (Types.to_string t) (Types.to_string t) @@ -2185,6 +2192,9 @@ let rec mangle_ty (t : Types.t) = | Types.CFn (ps, r) -> Printf.sprintf "cfn-%s-to-%s" (String.concat "-" (List.map mangle_ty ps)) (mangle_ty r) + (* Bare, because [Types.to_string] spells a variable with its [$] for the + reader and a symbol has no room for one. *) + | Types.Var n -> n | t -> Types.to_string t (* ── The runaway instantiation, refused by name rather than by depth ──── @@ -4099,14 +4109,14 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = | Some (Types.Int k) -> not (Types.signed k) | _ -> false) -> let t = Option.get want in - let gname, _, at = List.nth ctx.env.chain (List.length ctx.env.chain - 1) in + (* [instantiate] adds the note naming the call that asked for this copy. *) + let gname, _, _ = List.nth ctx.env.chain (List.length ctx.env.chain - 1) in let var = match List.find_opt (fun (_, u) -> Types.equal u t) ctx.env.subst with | Some (v, _) -> Printf.sprintf "$%s = %s" v (Types.to_string t) | None -> Types.to_string t in Loc.failk literal_at_want loc - ~notes:[ Loc.note at (Printf.sprintf "%s is instantiated at %s here" gname var) ] "%Ld does not fit in %s, which holds no negative number, and %s is called \ at %s — the body has to work at every type it is called at, so write \ it with no negative literal, as in (- x %Ld) in place of (+ x %Ld)" @@ -6548,9 +6558,7 @@ and mixed_refusal : 'a. ctx -> Ast.expr list -> Loc.diag -> 'a = (Printf.sprintf "this array's first element is %s, so every \ element is" - (match first.Tast.ty with - | Types.Var v -> "$" ^ v - | t -> Types.to_string t)) ] })) + (Types.to_string first.Tast.ty)) ] })) rest; raise (Loc.Error d) @@ -11284,11 +11292,39 @@ and instantiate env loc gname vars subst cparams cret = env.subst <- saved_subst; env.tyvars <- saved_vars; env.tvpreds <- saved_preds; env.chain <- saved_chain in + if Hashtbl.mem env.refused_generics gname then begin + restore (); + sym + end else let tfn = match !check_fn_ref env { fn with Ast.name = sym } with | tfn -> restore (); tfn | exception e -> restore (); + (* The refusal is inside the generic's source, which says nothing about + which call asked for this copy; the note names it. Nested copies + each add their own, so the notes walk the chain back to the call + the programmer wrote. *) + let e = + match e with + | Loc.Error d when d.Loc.dloc <> loc -> + let at = + String.concat ", " + (List.map + (fun v -> Printf.sprintf "$%s = %s" v + (Types.to_string (List.assoc v subst))) + vars) + in + Loc.Error + (Loc.sort_notes + { d with + Loc.notes = + d.Loc.notes + @ [ Loc.note loc + (Printf.sprintf "%s is instantiated at %s here" + gname at) ] }) + | e -> e + in (* A copy whose body did not check is not a copy. Both entries go back out, so a second call at the same types is the same refusal again rather than a cache hit on a function that does not exist. *) @@ -13933,9 +13969,12 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) : (fun (d : Ast.decl) -> match d.Ast.d with | Ast.Defn fn when Hashtbl.mem env.gsigs fn.Ast.name -> - ignore - (Loc.caught s (fun () -> - tolerant fn.Ast.name (fun () -> Some (check_generic env fn)))) + (match + Loc.caught s (fun () -> + tolerant fn.Ast.name (fun () -> Some (check_generic env fn))) + with + | None -> Hashtbl.replace env.refused_generics fn.Ast.name () + | Some _ -> ()) | _ -> ()) decls; let globals = diff --git a/lib/dev.ml b/lib/dev.ml index 7f052f25..8c54e3e7 100644 --- a/lib/dev.ml +++ b/lib/dev.ml @@ -669,14 +669,12 @@ let host_loc t name = that was written finds nothing in the program, and these are how it gets from that name to what the program does hold. *) -(* Its signature as written, [$] and all — [Types.to_string] prints a variable - bare, and [[t]] is not how anyone wrote it. *) +(* Its signature as written, [$] and all. *) let generic_signature t name = match Hashtbl.find_opt t.session.Session.env.Check.gsigs name with | None -> None - | Some (vars, params, ret) -> - let dollar = List.map (fun v -> (v, Types.Var ("$" ^ v))) vars in - let show ty = Types.to_string (Check.subst_ty dollar ty) in + | Some (_, params, ret) -> + let show ty = Types.to_string ty in Some (Printf.sprintf "%s [%s] %s" name (String.concat " " (List.map show params)) (show ret)) diff --git a/lib/types.ml b/lib/types.ml index 3513621f..6e2bb57d 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -231,7 +231,7 @@ let rec to_string = function | CFn (ps, r) -> Printf.sprintf "(CFn [%s] %s)" (String.concat " " (List.map to_string ps)) (to_string r) - | Var n -> n + | Var n -> "$" ^ n | Dyn -> "dyn" let is_numeric = function Int _ | Float _ -> true | _ -> false diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index a0fe1a0f..4f08c8bf 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -3608,7 +3608,7 @@ let () = chain of instantiations and not a depth it gave up at. *) refuses "an unconstrained operator in a generic body" "programs/generic-reject.flan" - "nothing declares t numeric?"; + "nothing declares $t numeric?"; refuses "an unconstrained operator names the way out" "programs/generic-reject.flan" "{:where (numeric? $t)}"; refuses "a runaway instantiation" "programs/generic-runaway.flan" @@ -4680,10 +4680,10 @@ level "1" the easier of the two to leave open. *) refuses "a nested function type does not widen" "programs/fn-generic-nested.flan" - "hof expects (Fn [(Fn [t] t)] i32) here"; + "hof expects (Fn [(Fn [$t] $t)] i32) here"; refuses "and neither does one in return position" "programs/fn-generic-nested-return.flan" - "call-twice expects (Fn [] (Fn [] t)) here"; + "call-twice expects (Fn [] (Fn [] $t)) here"; outputs ~dev:true "an fn capturing by value, dev" "programs/fn-capture.flan" fn_capture_out; diff --git a/test/test_flan.ml b/test/test_flan.ml index 4d0f57f7..d306b1d1 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -1417,7 +1417,7 @@ let () = accepts "all-distinct over a type variable" "(defn three [a $t b $t c $t] bool {:where (equal? $t)} (!= a b c))"; rejects_check "a chain still wants the right predicate" - ~needle:"nothing declares t ordered?" + ~needle:"nothing declares $t ordered?" "(defn between [a $t b $t c $t] bool {:where (equal? $t)} (< a b c))"; (* One operand and none. Both would have to be [true] whatever they were handed, which is a typo carrying a value. *) @@ -5988,6 +5988,37 @@ let () = check "and they are in source order" (List.map (fun (d : Loc.diag) -> d.Loc.dloc.Loc.line) ds = [ 1; 2; 3 ])); + (* A generic whose abstract pass was refused is not checked again at each + copy: the refusal is one error, however many types call it, and the + caller's own later refusal is still found. *) + (match + Check.program_all + (Parse.program_all + (read "(defn g [x $t] u64 (nosuch x))\n\ + (defn main [] i32 (g 3) (g true) nope 0)\n")) + with + | _ -> check "a refused generic body is refused" false + | exception Loc.Errors ds -> + check "a refused generic body is one error, and its caller's is another" + (List.map (fun (d : Loc.diag) -> d.Loc.dloc.Loc.line) ds = [ 1; 2 ])); + + (* A refusal inside a copy names the call that asked for it, and each copy + between: the chain walks back to the line the programmer wrote. *) + (match + checked + "(defn show [v $t] () (println v)) \ + (defn outer [v $t] () (show v)) \ + (defn main [] i32 (outer main) 0)" + with + | _ -> check "a copy with no printer is refused" false + | exception Loc.Error d -> + let notes = List.map (fun (n : Loc.note) -> n.Loc.nmsg) d.Loc.notes in + check "a refusal in a copy names both instantiations" + (contains d.Loc.dmsg "no printer for" + && notes + = [ "show is instantiated at $t = (CFn [] i32) here"; + "outer is instantiated at $t = (CFn [] i32) here" ])); + (* The parser resynchronises on a top-level form, so two bad declarations are two errors rather than one. *) (match Parse.program_all (read "(defn a)\n(defn b)\n") with @@ -6046,7 +6077,7 @@ let () = accepts "numeric? admits +" "(defn add [a $t b $t] $t {:where (numeric? $t)} (+ a b))"; rejects_check "equal? does not admit <" - ~needle:"nothing declares t ordered?" + ~needle:"nothing declares $t ordered?" "(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))"; (* The entailments, which are the reason a signature is one predicate long rather than two. Every type the language orders is a number or an enum, @@ -6074,10 +6105,10 @@ let () = accepts "integer? admits the shifts" "(defn dbl [x $t] $t {:where (integer? $t)} (<< x 1))"; rejects_check "numeric? does not admit bit-and" - ~needle:"nothing declares t integer?" + ~needle:"nothing declares $t integer?" "(defn low? [x $t] bool {:where (numeric? $t)} (= (bit-and x 1) 1))"; rejects_check "nor the shifts" - ~needle:"nothing declares t integer?" + ~needle:"nothing declares $t integer?" "(defn dbl [x $t] $t {:where (numeric? $t)} (<< x 1))"; (* An integer?-bounded caller satisfies a numeric?-bounded callee: the entailment carries across generic calls exactly as ordered?-over-equal?