Fix some remaining invalid type annots

compiler/dcalc/interpreter.ml

@@ -479,7 +479,7 @@ let interpret_program :
  fun (ctx : decl_ctx) (e : 'm Ast.expr) :
      (Uid.MarkedString.info * 'm Ast.expr) list ->
   match evaluate_expr ctx e with
-  | EAbs (_, [((TStruct s_in, _) as targs)]), mark_e -> begin
+  | EAbs (_, [((TStruct s_in, _) as _targs)]), mark_e as e -> begin
     (* At this point, the interpreter seeks to execute the scope but does not
        have a way to retrieve input values from the command line. [taus] contain
        the types of the scope arguments. For [context] arguments, we can provide
@@ -502,31 +502,11 @@ let interpret_program :
         taus
     in
     let to_interpret =
-      ( EApp
-          ( e,
-            [
-              ( ETuple (application_term, Some s_in),
-                let pos =
-                  match application_term with
-                  | a :: _ -> Expr.pos a
-                  | [] -> Pos.no_pos
-                in
-                Expr.with_ty mark_e ~pos targs );
-            ] ),
-        Expr.map_mark
-          (fun pos -> pos)
-          (fun ty ->
-            match application_term, ty with
-            | [], t_out -> t_out
-            | _ :: _, (TArrow (_, t_out), _) -> t_out
-            | _ :: _, (_, bad_pos) ->
-              Errors.raise_spanned_error bad_pos
-                "@[<hv 2>(bug) Result of interpretation doesn't have the \
-                 expected type:@ @[%a@]@]"
-                (Print.typ ctx) ty)
-          mark_e )
+      Expr.make_app (Bindlib.box e)
+        [ Expr.make_tuple application_term (Some s_in) mark_e ]
+        (Expr.pos e)
     in
-    match Marked.unmark (evaluate_expr ctx to_interpret) with
+    match Marked.unmark (evaluate_expr ctx (Bindlib.unbox to_interpret)) with
     | ETuple (args, Some s_out) ->
       let s_out_fields =
         List.map

compiler/scopelang/scope_to_dcalc.ml

@@ -526,7 +526,7 @@ let translate_rule
                should have been defined (even an empty definition, if they're
                not defined by any rule in the source code) by the translation
                from desugared to the scope language. *)
-            Bindlib.box (Expr.empty_thunked_term m)
+            Expr.empty_thunked_term m
           else
             let a_var, _, _ =
               ScopeVarMap.find subvar.scope_var_name subscope_vars_defined
@@ -635,20 +635,23 @@ let translate_rule
       } )
   | Assertion e ->
     let new_e = translate_expr ctx e in
+    let scope_let_pos = Expr.pos e in
+    let scope_let_typ = TLit TUnit, scope_let_pos in
     ( (fun next ->
         Bindlib.box_apply2
           (fun next new_e ->
             ScopeLet
               {
                 scope_let_next = next;
-                scope_let_pos = Expr.pos e;
-                scope_let_typ = TLit TUnit, Expr.pos e;
+                scope_let_pos;
+                scope_let_typ;
                 scope_let_expr =
                   (* To ensure that we throw an error if the value is not
                      defined, we add an check "ErrorOnEmpty" here. *)
-                  Marked.same_mark_as
+                  Marked.mark
+                    (Expr.map_ty (fun _ -> scope_let_typ) (Marked.get_mark e))
                     (EAssert (Marked.same_mark_as (ErrorOnEmpty new_e) e))
-                    new_e;
+                    ;
                 scope_let_kind = Assertion;
               })
           (Bindlib.bind_var (Var.make "_") next)

compiler/shared_ast/expr.ml

@@ -753,11 +753,10 @@ let make_app e u pos =
 let empty_thunked_term mark =
   let silent = Var.make "_" in
   let pos = mark_pos mark in
-  Bindlib.unbox
-    (make_abs [| silent |]
-       (Bindlib.box (ELit LEmptyError, mark))
-       [TLit TUnit, pos]
-       pos)
+  make_abs [| silent |]
+    (Bindlib.box (ELit LEmptyError, mark))
+    [TLit TUnit, pos]
+    pos
 
 let make_let_in x tau e1 e2 mpos =
   make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos (Bindlib.unbox e2))
@@ -781,3 +780,19 @@ let make_default exceptions just cons mark =
     EDefault (exceptions, just, cons), mark
   | [except], Some false, _ -> except
   | exceptions, _, cons -> EDefault (exceptions, just, cons), mark
+
+let make_tuple el structname m0 =
+  match el with
+  | [] ->
+    etuple [] structname
+      (with_ty m0 (match structname with
+           | Some n -> TStruct n, mark_pos m0
+           | None -> TTuple [], mark_pos m0))
+  | el ->
+    let m =
+      fold_marks
+        (fun posl -> List.hd posl)
+        (fun ml -> TTuple (List.map (fun t -> t.ty) ml), (List.hd ml).pos)
+        (List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) el)
+    in
+    etuple el structname m

compiler/shared_ast/expr.mli

@@ -188,7 +188,7 @@ val make_app :
   ('a, 'm mark) gexpr box
 
 val empty_thunked_term :
-  'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) gexpr
+  'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) gexpr box
 
 val make_let_in :
   ('a, 'm mark) gexpr Var.t ->
@@ -225,6 +225,13 @@ val make_default :
       exceptions, is collapsed into [<ex | def>]
     - [<ex | false :- _>], when [ex] is a single exception, is rewritten as [ex] *)
 
+(** Builds a tuple; the mark argument is only used as witness and for position when building 0-uples *)
+val make_tuple:
+  ([< dcalc | lcalc] as 'a, 'm mark) gexpr box list ->
+  StructName.t option ->
+  'm mark ->
+  ('a, 'm mark) gexpr box
+
 (** {2 Transformations} *)
 
 val remove_logging_calls : ('a any, 't) gexpr -> ('a, 't) gexpr box