A refusal in a prelude generic's body stands at the call that asked for the copy, with the prelude's line as a note
This commit is contained in:
parent
8eac6734f0
commit
b51b7d0a53
34
lib/check.ml
34
lib/check.ml
@ -12049,16 +12049,34 @@ and instantiate env loc gname vars subst cparams cret =
|
||||
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 at () =
|
||||
String.concat ", "
|
||||
(List.map
|
||||
(fun v -> Printf.sprintf "$%s = %s" v
|
||||
(Types.to_string (List.assoc v subst)))
|
||||
vars)
|
||||
in
|
||||
let in_prelude (l : Loc.t) = String.equal l.Loc.file Prelude.file in
|
||||
let e =
|
||||
match e with
|
||||
(* A prelude generic's body is source nobody at this call wrote, and
|
||||
an editor cannot jump to it. The refusal moves to the call that
|
||||
asked for the copy, and the prelude's line comes along as a
|
||||
note. *)
|
||||
| Loc.Error d when in_prelude d.Loc.dloc && not (in_prelude loc) ->
|
||||
Loc.Error
|
||||
(Loc.sort_notes
|
||||
{ d with
|
||||
Loc.dloc = loc;
|
||||
dmsg =
|
||||
Printf.sprintf "%s cannot be made at %s. In its body: %s"
|
||||
gname (at ()) d.Loc.dmsg;
|
||||
notes =
|
||||
d.Loc.notes
|
||||
@ [ Loc.note d.Loc.dloc
|
||||
(Printf.sprintf "in %s's body, in the prelude" gname) ];
|
||||
expansion = None })
|
||||
| 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
|
||||
@ -12066,7 +12084,7 @@ and instantiate env loc gname vars subst cparams cret =
|
||||
d.Loc.notes
|
||||
@ [ Loc.note loc
|
||||
(Printf.sprintf "%s is instantiated at %s here"
|
||||
gname at) ] })
|
||||
gname (at ())) ] })
|
||||
| e -> e
|
||||
in
|
||||
(* A copy whose body did not check is not a copy. Both entries go back
|
||||
|
||||
@ -6017,6 +6017,37 @@ let () =
|
||||
= [ "show is instantiated at $t = (CFn [] i32) here";
|
||||
"outer is instantiated at $t = (CFn [] i32) here" ]));
|
||||
|
||||
(* A copy that cannot be built at a closure's type: the zeroed value in the
|
||||
body is refused there, and the call that asked is named. *)
|
||||
(match
|
||||
checked
|
||||
"(defn blank [x $t] $t (let [z (the $t (zeroed))] z)) \
|
||||
(defn use-it [f (Fn [i32] i32)] i32 (blank f) 0)"
|
||||
with
|
||||
| _ -> check "a zeroed closure in a copy is refused" false
|
||||
| exception Loc.Error d ->
|
||||
check "a copy at a closure type names the call that asked"
|
||||
(List.exists
|
||||
(fun (n : Loc.note) ->
|
||||
contains n.Loc.nmsg "blank is instantiated at $t = (Fn [i32] i32) here")
|
||||
d.Loc.notes));
|
||||
|
||||
(* A prelude generic's body is nobody's source at the call: the refusal is
|
||||
at the call, and the prelude's line is a note. *)
|
||||
(match
|
||||
checked
|
||||
"(defn keep [g (Vec u8)] bool true) \
|
||||
(defn use-it [xs [(Vec u8)]] i32 (length (filter xs keep)))"
|
||||
with
|
||||
| _ -> check "a prelude copy that cannot be built is refused" false
|
||||
| exception Loc.Error d ->
|
||||
check "a prelude copy's refusal is at the user's call"
|
||||
(d.Loc.dloc.Loc.file <> Prelude.file
|
||||
&& contains d.Loc.dmsg "filter cannot be made at $t = (Vec u8)"
|
||||
&& List.exists
|
||||
(fun (n : Loc.note) -> n.Loc.nloc.Loc.file = Prelude.file)
|
||||
d.Loc.notes));
|
||||
|
||||
(* 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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user