Skip to content

typing: precise diagnostics for failed operator applications #1050

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
strub merged 1 commit into from
Jun 17, 2026
Merged

typing: precise diagnostics for failed operator applications #1050

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions src/ec.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -826,6 +826,17 @@ let main () =
end;
raise (EcScope.toperror_of_exn ~gloc:loc e)
end;
p.EP.gl_expect |> oiter (fun expected ->
let actual =
Format.asprintf "%a" EcPException.exn_printer e in
if String.trim actual <> String.trim (EcLocation.unloc expected) then
EcScope.hierror ~loc:(EcLocation.loc expected)
"expect fail: error message mismatch@\n\
--- expected ---@\n\
%s@\n\
--- actual ---@\n\
%s"
(EcLocation.unloc expected) actual);
if T.interactive terminal then begin
let error =
Format.asprintf
Expand Down
10 changes: 8 additions & 2 deletions src/ecParser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3999,12 +3999,18 @@ stop:
| DROP DOT { }

global:
| db=debug_global? fail=boption(FAIL) g=global_action ep=FINAL
| db=debug_global? f=failmode g=global_action ep=FINAL
{ let lc = EcLocation.make $startpos ep in
{ gl_action = EcLocation.mk_loc lc g;
gl_fail = fail;
gl_fail = fst f;
gl_expect = snd f;
gl_debug = db; } }

%inline failmode:
| (* empty *) { (false, None ) }
| FAIL { (true , None ) }
| EXPECT FAIL s=loc(STRING) { (true , Some s) }

debug_global:
| TIME { `Timed }
| DEBUG { `Break }
Expand Down
1 change: 1 addition & 0 deletions src/ecParsetree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1388,6 +1388,7 @@ type global_action =
type global = {
gl_action : global_action located;
gl_fail : bool;
gl_expect : string located option; (* [expect fail "…"]: expected error *)
gl_debug : [`Timed | `Break] option;
}

Expand Down
124 changes: 89 additions & 35 deletions src/ecTyping.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,9 +122,16 @@ type filter_error =
| FE_InvalidIndex of int
| FE_NoMatch

type goal_shape_error =
type goal_shape_error =
| GSE_ExpectedTwoSided

(* A failed application candidate, tagged by the kind of entity. *)
type appcand = [
| `Op of EcPath.path * EcUnify.op_instance * ty
| `Pv of EcTypes.prog_var * ty
| `Lc of EcIdent.t * ty
]

type tyerror =
| UniVarNotAllowed
| FreeTypeVariables
Expand Down Expand Up @@ -159,6 +166,8 @@ type tyerror =
| NotAnInductive
| AbbrevLowArgs
| UnknownVarOrOp of qsymbol * ty list
| UnappliedOp of qsymbol * ty list * ty option
* (appcand * EcUnify.op_failure) list
| MultipleOpMatch of qsymbol * ty list * (opmatch * EcUnify.unienv) list
| UnknownModName of qsymbol
| UnknownTyModName of qsymbol
Expand Down Expand Up @@ -315,22 +324,22 @@ let select_local env (qs,s) =
else None

(* -------------------------------------------------------------------- *)
let select_pv env side name ue tvi (psig, retty) =
(* The program variable [name] if it applies to [psig]/[retty], else the
reason it does not. *)
let select_pv env side name ue tvi (psig, retty)
: (_ * ty * EcUnify.unienv) list * (appcand * EcUnify.op_failure) list =
if tvi <> None
then []
then ([], [])
else
try
let pvs = EcEnv.Var.lookup_progvar ?side name env in
let select (pv,ty) =
let subue = UE.copy ue in
let texpected = EcUnify.tfun_expected subue ?retty psig in
try
EcUnify.unify env subue ty texpected;
[(pv, ty, subue)]
with EcUnify.UnificationFailure _ -> []
in
select pvs
with EcEnv.LookupFailure _ -> []
let (pv, ty) = EcEnv.Var.lookup_progvar ?side name env in
let subue = UE.copy ue in
match EcUnify.classify_application env subue ty psig retty with
| None -> ([(pv, ty, subue)], [])
| Some f ->
let pv0 = match pv with `Var p -> p | `Proj (p, _) -> p in
([], [(`Pv (pv0, ty), f)])
with EcEnv.LookupFailure _ -> ([], [])

(* -------------------------------------------------------------------- *)
module OpSelect = struct
Expand All @@ -350,6 +359,8 @@ module OpSelect = struct

type gopsel =
opsel * EcTypes.ty * EcUnify.unienv * opmatch

type opfailure = appcand * EcUnify.op_failure
end

let gen_select_op
Expand All @@ -363,9 +374,11 @@ let gen_select_op
(ue : EcUnify.unienv)
(psig : EcTypes.dom * EcTypes.ty option)

: OpSelect.gopsel list
: OpSelect.gopsel list * OpSelect.opfailure list
=

let opfailures = ref [] in

let fpv me (pv, ty, ue) : OpSelect.gopsel =
(`Pv (me, pv), ty, ue, (pv :> opmatch))

Expand Down Expand Up @@ -405,18 +418,30 @@ let gen_select_op
else [] in

let ops () : OpSelect.gopsel list =
let ops = EcUnify.select_op ~filter:ue_filter tvi env name ue psig in
let outcomes =
EcUnify.select_op_outcomes ~filter:ue_filter tvi env name ue psig in
let ops =
List.filter_map
(function EcUnify.OK r -> Some r | EcUnify.KO _ -> None) outcomes in
opfailures := !opfailures @
List.filter_map
(function
| EcUnify.KO (p, inst, ty, f) -> Some (`Op (p, inst, ty), f)
| EcUnify.OK _ -> None)
outcomes;
let ops = opsc |> ofold (fun opsc -> List.mbfilter (by_scope opsc)) ops in
let ops = match List.mbfilter by_current ops with [] -> ops | ops -> ops in
let ops = match List.mbfilter by_tc ops with [] -> ops | ops -> ops in
(List.map fop ops)

and pvs () : OpSelect.gopsel list =
let me, pvs =
let me, (pvs, pvfailures) =
match EcEnv.Memory.get_active_ss env, actonly with
| None, true -> (None, [])
| None, true -> (None, ([], []))
| me , _ -> ( me, select_pv env me name ue tvi psig)
in List.map (fpv me) pvs
in
opfailures := !opfailures @ pvfailures;
List.map (fpv me) pvs
in

let select (filters : (unit -> OpSelect.gopsel list) list) : OpSelect.gopsel list =
Expand All @@ -425,14 +450,17 @@ let gen_select_op
filters
|> odfl [] in

match mode with
| `Expr `InOp -> select [locals; ops]
| `Form
| `Expr `InProc ->
if forcepv then
select [pvs; locals; ops]
else
select [locals; pvs; ops]
let selected =
match mode with
| `Expr `InOp -> select [locals; ops]
| `Form
| `Expr `InProc ->
if forcepv then
select [pvs; locals; ops]
else
select [locals; pvs; ops]
in
(selected, !opfailures)

(* -------------------------------------------------------------------- *)
let select_exp_op env mode opsc name ue tvi psig =
Expand All @@ -444,6 +472,14 @@ let select_form_op env mode ~forcepv opsc name ue tvi psig =
gen_select_op ~actonly:true ~mode ~forcepv
opsc tvi env name ue psig

(* -------------------------------------------------------------------- *)
(* [UnappliedOp] when candidates of that name exist but fail, else
[UnknownVarOrOp]. *)
let tyerror_noop env loc name esig retty (opfailures : OpSelect.opfailure list) =
match opfailures with
| [] -> tyerror loc env (UnknownVarOrOp (name, esig))
| _ -> tyerror loc env (UnappliedOp (name, esig, retty, opfailures))

(* -------------------------------------------------------------------- *)
let select_proj env opsc name ue tvi recty =
let filter = (fun _ op -> EcDecl.is_proj op) in
Expand Down Expand Up @@ -1668,6 +1704,24 @@ let form_of_opselect
EcUnify.UniEnv.restore ~src:subue ~dst:ue;

let esig = List.map (lmap f_ty) args in

(* Locals are selected without an applicability check (they shadow
operators unconditionally), so diagnose a failing application here. *)
begin match sel with
| `Lc id ->
let resolve t = ty_subst (Tuni.subst (EcUnify.UniEnv.assubst ue)) t in
let psig = List.map (fun t -> resolve (unloc t)) esig in
let ue' = EcUnify.UniEnv.copy ue in
begin match EcUnify.classify_application env ue' ty psig None with
| None -> ()
| Some f ->
tyerror loc env
(UnappliedOp (([], EcIdent.name id), psig, None,
[(`Lc (id, resolve ty), f)]))
end
| _ -> ()
end;

let args = List.map unloc args in
let codom = ty_fun_app loc env ue ty esig in

Expand Down Expand Up @@ -2884,13 +2938,13 @@ and translvalue ue (env : EcEnv.env) lvalue =

let name = ([], EcCoreLib.s_set) in
let esig = [xty; ety; codom] in
let ops = select_exp_op env `InProc None name ue tvi (esig, None) in
let ops, opfailures = select_exp_op env `InProc None name ue tvi (esig, None) in

match ops with
| [] ->
let uidmap = UE.assubst ue in
let esig = Tuni.subst_dom uidmap esig in
tyerror x.pl_loc env (UnknownVarOrOp (name, esig))
tyerror_noop env x.pl_loc name esig None opfailures

| [`Op (p, tys), opty, subue, _] ->
EcUnify.UniEnv.restore ~src:subue ~dst:ue;
Expand All @@ -2903,7 +2957,7 @@ and translvalue ue (env : EcEnv.env) lvalue =
| [_] ->
let uidmap = UE.assubst ue in
let esig = Tuni.subst_dom uidmap esig in
tyerror x.pl_loc env (UnknownVarOrOp (name, esig))
tyerror_noop env x.pl_loc name esig None opfailures

| _ ->
let uidmap = UE.assubst ue in
Expand Down Expand Up @@ -3195,13 +3249,13 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =

| PFident ({ pl_desc = name; pl_loc = loc }, tvi) ->
let tvi = tvi |> omap (transtvi env ue) in
let ops =
let ops, opfailures =
select_form_op
~forcepv:(PFS.isforced state)
env mode opsc name ue tvi ([], tt) in
begin match ops with
| [] ->
tyerror loc env (UnknownVarOrOp (name, []))
tyerror_noop env loc name [] tt opfailures

| [sel] -> begin
let op = form_of_opselect (env, ue) loc sel [] in
Expand Down Expand Up @@ -3357,7 +3411,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
select_form_op ~forcepv:(PFS.isforced state)
env mode opsc name ue tvi (esig, tt)
with
| [sel] -> Some (sel, (es, esig, tvi))
| [sel], _ -> Some (sel, (es, esig, tvi))
| _ ->
Option.iter (fun ps -> ps := !(Option.get ps')) ps;
EcUnify.UniEnv.restore ~dst:ue ~src:ue';
Expand All @@ -3367,15 +3421,15 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
let tvi = tvi |> omap (transtvi env ue) in
let es = List.map (transf env) pes in
let esig = List.map EcFol.f_ty es in
let ops =
let ops, opfailures =
select_form_op ~forcepv:(PFS.isforced state)
env mode opsc name ue tvi (esig, tt) in

begin match ops with
| [] ->
let uidmap = UE.assubst ue in
let esig = Tuni.subst_dom uidmap esig in
tyerror loc env (UnknownVarOrOp (name, esig))
tyerror_noop env loc name esig tt opfailures

| [sel] ->
let es = List.map2 (fun e l -> mk_loc l.pl_loc e) es pes in
Expand Down
9 changes: 9 additions & 0 deletions src/ecTyping.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,13 @@ type opmatch = [
| `Proj of EcTypes.prog_var * EcMemory.proj_arg
]

(* A failed application candidate, tagged by the kind of entity. *)
type appcand = [
| `Op of EcPath.path * EcUnify.op_instance * EcTypes.ty
| `Pv of EcTypes.prog_var * EcTypes.ty
| `Lc of EcIdent.t * EcTypes.ty
]

type 'a mismatch_sets = [`Eq of 'a * 'a | `Sub of 'a ]


Expand Down Expand Up @@ -152,6 +159,8 @@ type tyerror =
| NotAnInductive
| AbbrevLowArgs
| UnknownVarOrOp of qsymbol * ty list
| UnappliedOp of qsymbol * ty list * ty option
* (appcand * EcUnify.op_failure) list
| MultipleOpMatch of qsymbol * ty list * (opmatch * EcUnify.unienv) list
| UnknownModName of qsymbol
| UnknownTyModName of qsymbol
Expand Down
Loading
Loading