EmptyError is no longer a literal

it's much simpler to handle it as an AST node, as that makes the literal
identical across all AST passes.

compiler/dcalc/ast.ml

@@ -17,8 +17,6 @@
 
 open Shared_ast
 
-type lit = dcalc glit
-
 type 'm naked_expr = (dcalc, 'm mark) naked_gexpr
 and 'm expr = (dcalc, 'm mark) gexpr
 

compiler/dcalc/ast.mli

@@ -19,8 +19,6 @@
 
 open Shared_ast
 
-type lit = dcalc glit
-
 type 'm naked_expr = (dcalc, 'm mark) naked_gexpr
 and 'm expr = (dcalc, 'm mark) gexpr
 

compiler/dcalc/from_scopelang.ml

@@ -201,8 +201,8 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
   match Marked.unmark e with
   | EVar v -> Expr.evar (Var.Map.find v ctx.local_vars) m
   | ELit
-      (( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
-       | LDuration _ ) as l) ->
+      ((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
+      l) ->
     Expr.elit l m
   | EStruct { name; fields } ->
     let fields = StructField.Map.map (translate_expr ctx) fields in
@@ -254,7 +254,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
           let expr =
             match str_field, expr with
             | Some { scope_input_io = Desugared.Ast.Reentrant, _; _ }, None ->
-              Some (Expr.unbox (Expr.elit LEmptyError (mark_tany m pos)))
+              Some (Expr.unbox (Expr.eemptyerror (mark_tany m pos)))
             | _ -> expr
           in
           match str_field, expr with
@@ -410,7 +410,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
            (Marked.mark
               (Expr.with_ty m
                  (TStruct sc_sig.scope_sig_output_struct, Expr.pos e))
-              (ELit LEmptyError)))
+              EEmptyError))
         (Expr.with_ty m (TStruct sc_sig.scope_sig_output_struct, Expr.pos e))
     in
     (* let result_var = calling_expr in let result_eta_expanded_var =
@@ -561,6 +561,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
   | EOp { op = Add_dat_dur _; tys } ->
     Expr.eop (Add_dat_dur ctx.date_rounding) tys m
   | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
+  | EEmptyError -> Expr.eemptyerror m
   | EErrorOnEmpty e' -> Expr.eerroronempty (translate_expr ctx e') m
   | EArray es -> Expr.earray (List.map (translate_expr ctx) es) m
 

compiler/dcalc/interpreter.ml

@@ -23,7 +23,7 @@ module Runtime = Runtime_ocaml.Runtime
 (** {1 Helpers} *)
 
 let is_empty_error (e : 'm Ast.expr) : bool =
-  match Marked.unmark e with ELit LEmptyError -> true | _ -> false
+  match Marked.unmark e with EEmptyError -> true | _ -> false
 
 let log_indent = ref 0
 
@@ -150,8 +150,8 @@ and evaluate_operator :
        (should not happen if the term was well-typed)"
   in
   let open Runtime.Oper in
-  if List.exists (function ELit LEmptyError, _ -> true | _ -> false) args then
-    ELit LEmptyError
+  if List.exists (function EEmptyError, _ -> true | _ -> false) args then
+    EEmptyError
   else
     match op, args with
     | Length, [(EArray es, _)] ->
@@ -350,7 +350,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
           (List.length args)
     | EOp { op; _ } ->
       Marked.same_mark_as (evaluate_operator ctx op (Expr.pos e) args) e
-    | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
+    | EEmptyError -> Marked.same_mark_as EEmptyError e
     | _ ->
       Errors.raise_spanned_error (Expr.pos e)
         "function has not been reduced to a lambda at evaluation (should not \
@@ -359,7 +359,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
   | EStruct { fields = es; name } ->
     let new_es = StructField.Map.map (evaluate_expr ctx) es in
     if StructField.Map.exists (fun _ e -> is_empty_error e) new_es then
-      Marked.same_mark_as (ELit LEmptyError) e
+      Marked.same_mark_as EEmptyError e
     else Marked.same_mark_as (EStruct { fields = new_es; name }) e
   | EStructAccess { e = e1; name = s; field } -> (
     let e1 = evaluate_expr ctx e1 in
@@ -377,7 +377,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
           "Invalid field access %a in struct %a (should not happen if the term \
            was well-typed)"
           StructField.format_t field StructName.format_t s)
-    | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
+    | EEmptyError -> Marked.same_mark_as EEmptyError e
     | _ ->
       Errors.raise_spanned_error (Expr.pos e1)
         "The expression %a should be a struct %a but is not (should not happen \
@@ -397,7 +397,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
         e size)
   | EInj { e = e1; name; cons } ->
     let e1' = evaluate_expr ctx e1 in
-    if is_empty_error e then Marked.same_mark_as (ELit LEmptyError) e
+    if is_empty_error e then Marked.same_mark_as EEmptyError e
     else Marked.same_mark_as (EInj { e = e1'; name; cons }) e
   | EMatch { e = e1; cases = es; name } -> (
     let e1 = evaluate_expr ctx e1 in
@@ -418,7 +418,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
       in
       let new_e = Marked.same_mark_as (EApp { f = es_n; args = [e1] }) e in
       evaluate_expr ctx new_e
-    | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
+    | EEmptyError -> Marked.same_mark_as EEmptyError e
     | _ ->
       Errors.raise_spanned_error (Expr.pos e1)
         "Expected a term having a sum type as an argument to a match (should \
@@ -430,9 +430,9 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
     | 0 -> (
       let just = evaluate_expr ctx just in
       match Marked.unmark just with
-      | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
+      | EEmptyError -> Marked.same_mark_as EEmptyError e
       | ELit (LBool true) -> evaluate_expr ctx cons
-      | ELit (LBool false) -> Marked.same_mark_as (ELit LEmptyError) e
+      | ELit (LBool false) -> Marked.same_mark_as EEmptyError e
       | _ ->
         Errors.raise_spanned_error (Expr.pos e)
           "Default justification has not been reduced to a boolean at \
@@ -450,19 +450,19 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
     match Marked.unmark (evaluate_expr ctx cond) with
     | ELit (LBool true) -> evaluate_expr ctx etrue
     | ELit (LBool false) -> evaluate_expr ctx efalse
-    | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
+    | EEmptyError -> Marked.same_mark_as EEmptyError e
     | _ ->
       Errors.raise_spanned_error (Expr.pos cond)
         "Expected a boolean literal for the result of this condition (should \
          not happen if the term was well-typed)")
   | EArray es ->
     let new_es = List.map (evaluate_expr ctx) es in
-    if List.exists is_empty_error new_es then
-      Marked.same_mark_as (ELit LEmptyError) e
+    if List.exists is_empty_error new_es then Marked.same_mark_as EEmptyError e
     else Marked.same_mark_as (EArray new_es) e
+  | EEmptyError -> Marked.same_mark_as EEmptyError e
   | EErrorOnEmpty e' ->
     let e' = evaluate_expr ctx e' in
-    if Marked.unmark e' = ELit LEmptyError then
+    if Marked.unmark e' = EEmptyError then
       Errors.raise_spanned_error (Expr.pos e')
         "This variable evaluated to an empty term (no rule that defined it \
          applied in this situation)"
@@ -515,7 +515,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
       | _ ->
         Cli.debug_format "%a" (Expr.format ctx) e';
         Errors.raise_spanned_error (Expr.pos e') "Assertion failed")
-    | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
+    | EEmptyError -> Marked.same_mark_as EEmptyError e
     | _ ->
       Errors.raise_spanned_error (Expr.pos e')
         "Expected a boolean literal for the result of this assertion (should \
@@ -543,7 +543,7 @@ let interpret_program :
           | TArrow (ty_in, ty_out) ->
             Expr.make_abs
               (Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
-              (Bindlib.box (ELit LEmptyError), Expr.with_ty mark_e ty_out)
+              (Bindlib.box EEmptyError, Expr.with_ty mark_e ty_out)
               ty_in (Expr.mark_pos mark_e)
           | _ ->
             Errors.raise_spanned_error (Marked.get_mark ty)

compiler/dcalc/optimizations.ml

@@ -29,7 +29,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
   let e = Expr.map ~f:(partial_evaluation ctx) e in
   let mark = Marked.get_mark e in
   (* Then reduce the parent node *)
-  let reduce e =
+  let reduce (e : 'm expr) =
     (* Todo: improve the handling of eapp(log,elit) cases here, it obfuscates
        the matches and the log calls are not preserved, which would be a good
        property *)
@@ -99,9 +99,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
     | EDefault { excepts; just; cons } -> (
       (* TODO: mechanically prove each of these optimizations correct :) *)
       let excepts =
-        List.filter
-          (fun except -> Marked.unmark except <> ELit LEmptyError)
-          excepts
+        List.filter (fun except -> Marked.unmark except <> EEmptyError) excepts
         (* we can discard the exceptions that are always empty error *)
       in
       let value_except_count =
@@ -137,7 +135,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
                     args = [(ELit (LBool false), _)];
                   } ),
               _ ) ) ->
-          ELit LEmptyError
+          EEmptyError
         | [], just when not !Cli.avoid_exceptions_flag ->
           (* without exceptions, a default is just an [if then else] raising an
              error in the else case. This exception is only valid in the context
@@ -145,8 +143,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
              flag to know if we will be compiling using exceptions or the option
              monad. FIXME: move this optimisation somewhere else to avoid this
              check *)
-          EIfThenElse
-            { cond = just; etrue = cons; efalse = ELit LEmptyError, mark }
+          EIfThenElse { cond = just; etrue = cons; efalse = EEmptyError, mark }
         | excepts, just -> EDefault { excepts; just; cons })
     | EIfThenElse
         {

compiler/desugared/ast.ml

@@ -145,7 +145,7 @@ let empty_rule
     (parameters : (Uid.MarkedString.info * typ) list Marked.pos option) : rule =
   {
     rule_just = Expr.box (ELit (LBool false), Untyped { pos });
-    rule_cons = Expr.box (ELit LEmptyError, Untyped { pos });
+    rule_cons = Expr.box (EEmptyError, Untyped { pos });
     rule_parameter =
       Option.map
         (Marked.map_under_mark

compiler/lcalc/ast.ml

@@ -17,8 +17,6 @@
 open Catala_utils
 include Shared_ast
 
-type lit = lcalc glit
-
 type 'm naked_expr = (lcalc, 'm mark) naked_gexpr
 and 'm expr = (lcalc, 'm mark) gexpr
 

compiler/lcalc/ast.mli

@@ -21,8 +21,6 @@ open Shared_ast
 
 (** {1 Abstract syntax tree} *)
 
-type lit = lcalc glit
-
 type 'm naked_expr = (lcalc, 'm mark) naked_gexpr
 and 'm expr = (lcalc, 'm mark) gexpr
 

compiler/lcalc/compile_with_exceptions.ml

@@ -77,7 +77,7 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed =
       ((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
       l) ->
     Expr.elit l m
-  | ELit LEmptyError -> Expr.eraise EmptyError m
+  | EEmptyError -> Expr.eraise EmptyError m
   | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
   | EIfThenElse { cond; etrue; efalse } ->
     Expr.eifthenelse (translate_expr ctx cond) (translate_expr ctx etrue)

compiler/lcalc/compile_without_exceptions.ml

@@ -182,7 +182,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
   | EDefault _ ->
     let v' = Var.make "default_term" in
     Expr.make_var v' mark, Var.Map.singleton v' e
-  | ELit LEmptyError ->
+  | EEmptyError ->
     let v' = Var.make "empty_litteral" in
     Expr.make_var v' mark, Var.Map.singleton v' e
   (* This one is a very special case. It transform an unpure expression
@@ -333,7 +333,7 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
             (Expr.make_var (Var.translate A.handle_default_opt) mark_hoist)
             [Expr.earray excepts' mark_hoist; just'; cons']
             pos
-        | ELit LEmptyError -> A.make_none mark_hoist
+        | EEmptyError -> A.make_none mark_hoist
         | EAssert arg ->
           let arg' = translate_expr ctx arg in
 

compiler/scalc/ast.ml

@@ -36,7 +36,7 @@ and naked_expr =
   | EStructFieldAccess : expr * StructField.t * StructName.t -> naked_expr
   | EInj : expr * EnumConstructor.t * EnumName.t -> naked_expr
   | EArray : expr list -> naked_expr
-  | ELit : L.lit -> naked_expr
+  | ELit : lit -> naked_expr
   | EApp : expr * expr list -> naked_expr
   | EOp : operator -> naked_expr
 

compiler/scalc/to_python.ml

@@ -22,7 +22,7 @@ module Runtime = Runtime_ocaml.Runtime
 module D = Dcalc.Ast
 module L = Lcalc.Ast
 
-let format_lit (fmt : Format.formatter) (l : L.lit Marked.pos) : unit =
+let format_lit (fmt : Format.formatter) (l : lit Marked.pos) : unit =
   match Marked.unmark l with
   | LBool true -> Format.pp_print_string fmt "True"
   | LBool false -> Format.pp_print_string fmt "False"

compiler/scopelang/from_desugared.ml

@@ -120,8 +120,8 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
          args ScopeVar.Map.empty)
       m
   | ELit
-      (( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
-       | LDuration _ ) as l) ->
+      ((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
+      l) ->
     Expr.elit l m
   | EAbs { binder; tys } ->
     let vars, body = Bindlib.unmbind binder in
@@ -159,6 +159,7 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
       (translate_expr ctx efalse)
       m
   | EArray args -> Expr.earray (List.map (translate_expr ctx) args) m
+  | EEmptyError -> Expr.eemptyerror m
   | EErrorOnEmpty e1 -> Expr.eerroronempty (translate_expr ctx e1) m
 
 (** {1 Rule tree construction} *)
@@ -292,8 +293,7 @@ let rec rule_tree_to_expr
          (translate_and_unbox_list base_just_list)
          (translate_and_unbox_list base_cons_list))
       (Expr.elit (LBool false) emark)
-      (Expr.elit LEmptyError emark)
-      emark
+      (Expr.eemptyerror emark) emark
   in
   let exceptions =
     List.map
@@ -390,7 +390,7 @@ let translate_def
        caller. *)
   then
     let m = Untyped { pos = Desugared.Ast.ScopeDef.get_position def_info } in
-    let empty_error = Expr.elit LEmptyError m in
+    let empty_error = Expr.eemptyerror m in
     match params with
     | Some (ps, _) ->
       let labels, tys = List.split ps in

compiler/shared_ast/definitions.ml

@@ -267,15 +267,14 @@ type except = ConflictError | EmptyError | NoValueProvided | Crash
 
 (** Literals are the same throughout compilation except for the [LEmptyError]
     case which is eliminated midway through. *)
-type _ glit =
-  | LBool : bool -> 'a glit
-  | LInt : Runtime.integer -> 'a glit
-  | LRat : Runtime.decimal -> 'a glit
-  | LMoney : Runtime.money -> 'a glit
-  | LUnit : 'a glit
-  | LDate : date -> 'a glit
-  | LDuration : duration -> 'a glit
-  | LEmptyError : [> `DefaultTerms ] glit
+type lit =
+  | LBool of bool
+  | LInt of Runtime.integer
+  | LRat of Runtime.decimal
+  | LMoney of Runtime.money
+  | LUnit
+  | LDate of date
+  | LDuration of duration
 
 (** Locations are handled differently in [desugared] and [scopelang] *)
 type 'a glocation =
@@ -306,7 +305,7 @@ type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t
 
 and ('a, 't) naked_gexpr =
   (* Constructors common to all ASTs *)
-  | ELit : 'a glit -> (([< all ] as 'a), 't) naked_gexpr
+  | ELit : lit -> (([< all ] as 'a), 't) naked_gexpr
   | EApp : {
       f : ('a, 't) gexpr;
       args : ('a, 't) gexpr list;
@@ -388,6 +387,7 @@ and ('a, 't) naked_gexpr =
       cons : ('a, 't) gexpr;
     }
       -> (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr
+  | EEmptyError : (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr
   | EErrorOnEmpty :
       ('a, 't) gexpr
       -> (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr

compiler/shared_ast/expr.ml

@@ -101,6 +101,7 @@ let eifthenelse cond etrue efalse =
   @@ fun cond etrue efalse -> EIfThenElse { cond; etrue; efalse }
 
 let eerroronempty e1 = Box.app1 e1 @@ fun e1 -> EErrorOnEmpty e1
+let eemptyerror mark = Marked.mark mark (Bindlib.box EEmptyError)
 let eraise e1 = Box.app0 @@ ERaise e1
 
 let ecatch body exn handler =
@@ -228,6 +229,7 @@ let map
   | EAssert e1 -> eassert (f e1) m
   | EDefault { excepts; just; cons } ->
     edefault (List.map f excepts) (f just) (f cons) m
+  | EEmptyError -> eemptyerror m
   | EErrorOnEmpty e1 -> eerroronempty (f e1) m
   | ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m
   | ERaise exn -> eraise exn m
@@ -259,7 +261,7 @@ let shallow_fold
     (acc : 'acc) : 'acc =
   let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in
   match Marked.unmark e with
-  | ELit _ | EOp _ | EVar _ | ERaise _ | ELocation _ -> acc
+  | ELit _ | EOp _ | EVar _ | ERaise _ | ELocation _ | EEmptyError -> acc
   | EApp { f = e; args } -> acc |> f e |> lfold args
   | EArray args -> acc |> lfold args
   | EAbs _ -> acc
@@ -334,6 +336,7 @@ let map_gather
     let acc2, just = f just in
     let acc3, cons = f cons in
     join (join acc1 acc2) acc3, edefault excepts just cons m
+  | EEmptyError -> acc, eemptyerror m
   | EErrorOnEmpty e ->
     let acc, e = f e in
     acc, eerroronempty e m
@@ -396,27 +399,23 @@ let is_value (type a) (e : (a, _) gexpr) =
   | ELit _ | EAbs _ | EOp _ | ERaise _ -> true
   | _ -> false
 
-let equal_lit (type a) (l1 : a glit) (l2 : a glit) =
+let equal_lit (l1 : lit) (l2 : lit) =
   let open Runtime.Oper in
   match l1, l2 with
   | LBool b1, LBool b2 -> not (o_xor b1 b2)
-  | LEmptyError, LEmptyError -> true
   | LInt n1, LInt n2 -> o_eq_int_int n1 n2
   | LRat r1, LRat r2 -> o_eq_rat_rat r1 r2
   | LMoney m1, LMoney m2 -> o_eq_mon_mon m1 m2
   | LUnit, LUnit -> true
   | LDate d1, LDate d2 -> o_eq_dat_dat d1 d2
   | LDuration d1, LDuration d2 -> o_eq_dur_dur d1 d2
-  | ( ( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
-      | LDuration _ ),
-      _ ) ->
+  | (LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _), _ ->
     false
 
-let compare_lit (type a) (l1 : a glit) (l2 : a glit) =
+let compare_lit (l1 : lit) (l2 : lit) =
   let open Runtime.Oper in
   match l1, l2 with
   | LBool b1, LBool b2 -> Bool.compare b1 b2
-  | LEmptyError, LEmptyError -> 0
   | LInt n1, LInt n2 ->
     if o_lt_int_int n1 n2 then -1 else if o_eq_int_int n1 n2 then 0 else 1
   | LRat r1, LRat r2 ->
@@ -436,8 +435,6 @@ let compare_lit (type a) (l1 : a glit) (l2 : a glit) =
     | n -> n)
   | LBool _, _ -> -1
   | _, LBool _ -> 1
-  | LEmptyError, _ -> -1
-  | _, LEmptyError -> 1
   | LInt _, _ -> -1
   | _, LInt _ -> 1
   | LRat _, _ -> -1
@@ -516,6 +513,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
   | ( EIfThenElse { cond = if1; etrue = then1; efalse = else1 },
       EIfThenElse { cond = if2; etrue = then2; efalse = else2 } ) ->
     equal if1 if2 && equal then1 then2 && equal else1 else2
+  | EEmptyError, EEmptyError -> true
   | EErrorOnEmpty e1, EErrorOnEmpty e2 -> equal e1 e2
   | ERaise ex1, ERaise ex2 -> equal_except ex1 ex2
   | ( ECatch { body = etry1; exn = ex1; handler = ewith1 },
@@ -544,9 +542,9 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
       EScopeCall { scope = s2; args = fields2 } ) ->
     ScopeName.equal s1 s2 && ScopeVar.Map.equal equal fields1 fields2
   | ( ( EVar _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _ | EAbs _ | EApp _
-      | EAssert _ | EOp _ | EDefault _ | EIfThenElse _ | EErrorOnEmpty _
-      | ERaise _ | ECatch _ | ELocation _ | EStruct _ | EDStructAccess _
-      | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ ),
+      | EAssert _ | EOp _ | EDefault _ | EIfThenElse _ | EEmptyError
+      | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EStruct _
+      | EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ ),
       _ ) ->
     false
 
@@ -623,6 +621,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
     compare just1 just2 @@< fun () ->
     compare cons1 cons2 @@< fun () ->
     List.compare compare exs1 exs2
+  | EEmptyError, EEmptyError -> 0
   | EErrorOnEmpty e1, EErrorOnEmpty e2 ->
     compare e1 e2
   | ERaise ex1, ERaise ex2 ->
@@ -650,6 +649,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
   | EInj _, _ -> -1 | _, EInj _ -> 1
   | EAssert _, _ -> -1 | _, EAssert _ -> 1
   | EDefault _, _ -> -1 | _, EDefault _ -> 1
+  | EEmptyError , _ -> -1 | _, EEmptyError  -> 1
   | EErrorOnEmpty _, _ -> -1 | _, EErrorOnEmpty _ -> 1
   | ERaise _, _ -> -1 | _, ERaise _ -> 1
   | ECatch _, _ -> . | _, ECatch _ -> .
@@ -674,7 +674,7 @@ let format ?debug decl_ctx ppf e = Print.expr ?debug decl_ctx ppf e
 let rec size : type a. (a, 't) gexpr -> int =
  fun e ->
   match Marked.unmark e with
-  | EVar _ | ELit _ | EOp _ -> 1
+  | EVar _ | ELit _ | EOp _ | EEmptyError -> 1
   | ETuple args -> List.fold_left (fun acc arg -> acc + size arg) 1 args
   | EArray args -> List.fold_left (fun acc arg -> acc + size arg) 1 args
   | ETupleAccess { e; _ } -> size e + 1
@@ -738,10 +738,7 @@ let make_app e args pos =
 let empty_thunked_term mark =
   let silent = Var.make "_" in
   let pos = mark_pos mark in
-  make_abs [| silent |]
-    (Bindlib.box (ELit LEmptyError), mark)
-    [TLit TUnit, pos]
-    pos
+  make_abs [| silent |] (Bindlib.box EEmptyError, mark) [TLit TUnit, pos] pos
 
 let make_let_in x tau e1 e2 mpos =
   make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos e2)

compiler/shared_ast/expr.mli

@@ -49,7 +49,7 @@ val etupleaccess :
   ('a, 't) boxed_gexpr -> int -> int -> 't -> ('a any, 't) boxed_gexpr
 
 val earray : ('a, 't) boxed_gexpr list -> 't -> ('a any, 't) boxed_gexpr
-val elit : 'a glit -> 't -> ('a any, 't) boxed_gexpr
+val elit : lit -> 't -> ('a any, 't) boxed_gexpr
 
 val eabs :
   (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box ->
@@ -82,6 +82,8 @@ val eifthenelse :
   't ->
   ('a any, 't) boxed_gexpr
 
+val eemptyerror : 't -> (([< all > `DefaultTerms ] as 'a), 't) boxed_gexpr
+
 val eerroronempty :
   ('a, 't) boxed_gexpr ->
   't ->
@@ -324,8 +326,8 @@ val format :
 
 (** {2 Analysis and tests} *)
 
-val equal_lit : 'a glit -> 'a glit -> bool
-val compare_lit : 'a glit -> 'a glit -> int
+val equal_lit : lit -> lit -> bool
+val compare_lit : lit -> lit -> int
 val equal_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> bool
 val compare_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> int
 

compiler/shared_ast/print.ml

@@ -126,11 +126,10 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
     Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "collection" typ t1
   | TAny -> base_type fmt "any"
 
-let lit (type a) (fmt : Format.formatter) (l : a glit) : unit =
+let lit (fmt : Format.formatter) (l : lit) : unit =
   match l with
   | LBool b -> lit_style fmt (string_of_bool b)
   | LInt i -> lit_style fmt (Runtime.integer_to_string i)
-  | LEmptyError -> lit_style fmt "∅ "
   | LUnit -> lit_style fmt "()"
   | LRat i ->
     lit_style fmt
@@ -364,6 +363,7 @@ let rec expr_aux :
            expr)
         excepts punctuation "|" expr just punctuation "⊢" expr cons punctuation
         "⟩"
+  | EEmptyError -> lit_style fmt "∅ "
   | EErrorOnEmpty e' ->
     Format.fprintf fmt "%a@ %a" op_style "error_empty" with_parens e'
   | EAssert e' ->

compiler/shared_ast/print.mli

@@ -34,7 +34,7 @@ val enum_constructor : Format.formatter -> EnumConstructor.t -> unit
 val tlit : Format.formatter -> typ_lit -> unit
 val location : Format.formatter -> 'a glocation -> unit
 val typ : decl_ctx -> Format.formatter -> typ -> unit
-val lit : Format.formatter -> 'a glit -> unit
+val lit : Format.formatter -> lit -> unit
 val operator : Format.formatter -> 'a operator -> unit
 val log_entry : Format.formatter -> log_entry -> unit
 val except : Format.formatter -> except -> unit

compiler/shared_ast/typing.ml

@@ -221,7 +221,7 @@ let handle_type_error ctx e t1 t2 =
     (Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold])
     "-->" t2_s ()
 
-let lit_type (type a) (lit : a A.glit) : naked_typ =
+let lit_type (lit : A.lit) : naked_typ =
   match lit with
   | LBool _ -> TLit TBool
   | LInt _ -> TLit TInt
@@ -230,7 +230,6 @@ let lit_type (type a) (lit : a A.glit) : naked_typ =
   | LDate _ -> TLit TDate
   | LDuration _ -> TLit TDuration
   | LUnit -> TLit TUnit
-  | LEmptyError -> TAny (Any.fresh ())
 
 (** [op_type] and [resolve_overload] are a bit similar, and work on disjoint
     sets of operators. However, their assumptions are different so we keep the
@@ -742,6 +741,7 @@ and typecheck_expr_top_down :
         e1
     in
     Expr.eassert e1' mark
+  | A.EEmptyError -> Expr.eemptyerror (ty_mark (TAny (Any.fresh ())))
   | A.EErrorOnEmpty e1 ->
     let e1' = typecheck_expr_top_down ~leave_unresolved ctx env tau e1 in
     Expr.eerroronempty e1' context_mark

compiler/verification/conditions.ml

@@ -198,7 +198,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
             (Marked.get_mark e);
         ])
       (Marked.get_mark e)
-  | ELit LEmptyError -> Marked.same_mark_as (ELit (LBool false)) e
+  | EEmptyError -> Marked.same_mark_as (ELit (LBool false)) e
   | EVar _
   (* Per default calculus semantics, you cannot call a function with an argument
      that evaluates to the empty error. Thus, all variable evaluate to

compiler/verification/z3backend.real.ml

@@ -374,7 +374,6 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr =
   match l with
   | LBool b ->
     if b then Boolean.mk_true ctx.ctx_z3 else Boolean.mk_false ctx.ctx_z3
-  | LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
   | LInt n ->
     Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.integer_to_int n)
   | LRat r ->
@@ -785,6 +784,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
             (Boolean.mk_not ctx.ctx_z3 z3_if)
             z3_else;
         ] )
+  | EEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
   | EErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
 
 (** [create_z3unit] creates a Z3 sort and expression corresponding to the unit