Skip to content

Commit

Permalink
Delayed errors: keep on non-delayed error
Browse files Browse the repository at this point in the history
When a non-delayed error happens after delayed errors, these should take
precedence and be raised rather than ignored. Indeed, it's often a consequence
of delayed errors.

This happened in the disambiguation phase where a type inconsistency would be
skipped, leading to a failure to disambiguate, and only the latter was printed
resulting in a puzzling error.
  • Loading branch information
AltGr committed Jan 8, 2025
1 parent d9a6958 commit 68d3a81
Show file tree
Hide file tree
Showing 5 changed files with 145 additions and 47 deletions.
33 changes: 18 additions & 15 deletions compiler/catala_utils/message.ml
Original file line number Diff line number Diff line change
Expand Up @@ -531,19 +531,22 @@ let with_delayed_errors
"delayed error called outside scope: encapsulate using \
'with_delayed_errors' first");
global_errors.stop_on_error <- stop_on_error;
try
let r = f () in
match global_errors.errors with
| None -> error ~internal:true "intertwined delayed error scope"
| Some [] ->
global_errors.errors <- None;
r
| Some [err] ->
global_errors.errors <- None;
raise (CompilerError err)
| Some errs ->
global_errors.errors <- None;
raise (CompilerErrors (List.rev errs))
with e ->
let result =
match f () with
| r -> fun () -> r
| exception (CompilerError _ as e) ->
let bt = Printexc.get_raw_backtrace () in
fun () -> Printexc.raise_with_backtrace e bt
| exception e -> raise e
in
match global_errors.errors with
| None -> error ~internal:true "intertwined delayed error scope"
| Some [] ->
global_errors.errors <- None;
result ()
| Some [err] ->
global_errors.errors <- None;
raise (CompilerError err)
| Some errs ->
global_errors.errors <- None;
raise e
raise (CompilerErrors (List.rev errs))
32 changes: 16 additions & 16 deletions compiler/shared_ast/typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -876,22 +876,21 @@ and typecheck_expr_top_down :
Message.error ~pos:(Expr.pos e)
"function has %d variables but was supplied %d types\n%a"
(Bindlib.mbinder_arity binder)
(List.length t_args) Expr.format e
else
let tau_args = List.map ast_to_typ t_args in
let t_ret = unionfind (TAny (Any.fresh ())) in
let t_func = unionfind (TArrow (tau_args, t_ret)) in
let mark = mark_with_tau_and_unify t_func in
let xs, body = Bindlib.unmbind binder in
let xs' = Array.map Var.translate xs in
let env =
List.fold_left2
(fun env x tau_arg -> Env.add x tau_arg env)
env (Array.to_list xs) tau_args
in
let body' = typecheck_expr_top_down ctx env t_ret body in
let binder' = Bindlib.bind_mvar xs' (Expr.Box.lift body') in
Expr.eabs binder' pos (List.map (typ_to_ast ~flags) tau_args) mark
(List.length t_args) Expr.format e;
let tau_args = List.map ast_to_typ t_args in
let t_ret = unionfind (TAny (Any.fresh ())) in
let t_func = unionfind (TArrow (tau_args, t_ret)) in
let mark = mark_with_tau_and_unify t_func in
let xs, body = Bindlib.unmbind binder in
let xs' = Array.map Var.translate xs in
let env =
List.fold_left2
(fun env x tau_arg -> Env.add x tau_arg env)
env (Array.to_list xs) tau_args
in
let body' = typecheck_expr_top_down ctx env t_ret body in
let binder' = Bindlib.bind_mvar xs' (Expr.Box.lift body') in
Expr.eabs binder' pos (List.map (typ_to_ast ~flags) tau_args) mark
| A.EApp { f = e1; args; tys } ->
(* Here we type the arguments first (in order), to ensure we know the types
of the arguments if [f] is [EAbs] before disambiguation. This is also the
Expand Down Expand Up @@ -939,6 +938,7 @@ and typecheck_expr_top_down :
operators are required to allow the resolution of all type
variables this way *)
unify ctx e (polymorphic_op_type op) t_func;
(* List.rev_map(2) applies the side effects in order *)
List.rev_map2
(typecheck_expr_top_down ctx env)
(List.rev t_args) (List.rev args)))
Expand Down
90 changes: 90 additions & 0 deletions tests/array/bad/type_error_in_filter.catala_en
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@

```catala
declaration structure St:
data x content integer

declaration scope S:
input ll content list of St
output out content list of St

scope S:
definition out equals
combine acc initially []
with (acc ++ list of x among in_n such that x.x > 2)
# acc ++ filter (x -> x.x > 2) in_n
for in_n among ll

declaration scope Test:
output s scope S

declaration st content St
depends on x content integer
equals St { -- x: x }

scope Test:
definition s.ll equals [
[st of 1; st of 2; st of 3];
[st of 2; st of 3; st of 4];
[st of 3; st of 4; st of 5]
]
```


```catala-test-inline
$ catala dcalc
┌─[ERROR]─
│ Error during typechecking, incompatible types:
│ ─➤ St
│ ─➤ list of any
│ While typechecking the following expression:
├─➤ tests/array/bad/type_error_in_filter.catala_en:13.34-13.38:
│ │
│ 13 │ with (acc ++ list of x among in_n such that x.x > 2)
│ │ ‾‾‾‾
│ Type St is coming from:
├─➤ tests/array/bad/type_error_in_filter.catala_en:7.28-7.30:
│ │
│ 7 │ input ll content list of St
│ │ ‾‾
│ Type list of any is coming from:
├─➤ tests/array/bad/type_error_in_filter.catala_en:13.18-13.56:
│ │
│ 13 │ with (acc ++ list of x among in_n such that x.x > 2)
│ │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─
#return code 123#
```


```catala-test-inline
$ catala test-scope Test
┌─[ERROR]─
│ Error during typechecking, incompatible types:
│ ─➤ St
│ ─➤ list of any
│ While typechecking the following expression:
├─➤ tests/array/bad/type_error_in_filter.catala_en:13.34-13.38:
│ │
│ 13 │ with (acc ++ list of x among in_n such that x.x > 2)
│ │ ‾‾‾‾
│ Type St is coming from:
├─➤ tests/array/bad/type_error_in_filter.catala_en:7.28-7.30:
│ │
│ 7 │ input ll content list of St
│ │ ‾‾
│ Type list of any is coming from:
├─➤ tests/array/bad/type_error_in_filter.catala_en:13.18-13.56:
│ │
│ 13 │ with (acc ++ list of x among in_n such that x.x > 2)
│ │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─
#return code 123#
```
33 changes: 19 additions & 14 deletions tests/array/good/broken-message.catala_en
Original file line number Diff line number Diff line change
Expand Up @@ -26,33 +26,38 @@ scope B:
(acc1 ++ [x + acc2], acc2 + x) for x among a.x
```

The positions in this error message are completely wrong and misleading.
Investigation needed...
There was an error -- now fixed -- where the issue was pointed on `x+acc2` with
a confusing message.

This was diagnosed to be due to delayed error messages that got skipped.

```catala-test-inline
$ catala Typecheck --check-invariants
┌─[ERROR]─
│ I don't know how to apply operator + on types list of money and money
│ Error during typechecking, incompatible types:
│ ─➤ money
│ ─➤ list of money
├─➤ tests/array/good/broken-message.catala_en:26.17-26.25:
│ While typechecking the following expression:
├─➤ tests/array/good/broken-message.catala_en:21.8-21.9:
│ │
│ 26 │ (acc1 ++ [x + acc2], acc2 + x) for x among a.x
│ │ ‾‾‾‾‾‾‾‾
│ 21 │ (x ++ acc) for x among a.x
│ │ ‾
├─ Article
│ Type money is coming from:
├─➤ tests/array/good/broken-message.catala_en:5.28-5.33:
│ │
│ 5 │ output x content list of money
│ │ ‾‾‾‾‾
├─ Article
│ Type list of money coming from expression:
│ Type list of money is coming from:
├─➤ tests/array/good/broken-message.catala_en:21.10-21.12:
│ │
│ 21 │ (x ++ acc) for x among a.x
│ │ ‾‾
├─ Article
│ Type money coming from expression:
├─➤ tests/array/good/broken-message.catala_en:25.41-25.43:
│ │
│ 25 │ combine (acc1, acc2) initially ([], $1) with
│ │ ‾‾
└─ Article
#return code 123#
```
4 changes: 2 additions & 2 deletions tests/struct/bad/wrong_qualified_field.catala_en
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ scope A:
$ catala test-scope A
┌─[ERROR]─
│ Field "g" does not belong to structure "Foo" (however, structure "Bar"
defines it).
│ Field g does not belong to structure Foo (however, structure Bar defines
│ it).
├─➤ tests/struct/bad/wrong_qualified_field.catala_en:17.23-17.30:
│ │
│17 │ definition y equals x.Foo.g
Expand Down

0 comments on commit 68d3a81

Please sign in to comment.