Type variables: fix monomorphisation, update tests

This doesn't of course implement generic monomorphisation over quantified types,
only fixes on par with what it could handle previously.

compiler/lcalc/monomorphize.ml

@@ -55,7 +55,7 @@ let collect_monomorphized_instances (prg : typed program) :
   let tuple_instances_counter = ref 0 in
   let array_instances_counter = ref 0 in
   let rec collect_typ acc typ =
-    match Mark.remove typ with
+    match Mark.remove (Type.unquantify typ) with
     | TTuple args
       when List.for_all
              (function (TAny _ | TVar _), _ -> false | _ -> true)
@@ -148,7 +148,8 @@ let collect_monomorphized_instances (prg : typed program) :
       in
       collect_typ new_acc t
     | TStruct _ | TEnum _ | TClosureEnv | TLit _ -> acc
-    | TAny _ | TVar _ -> assert false (* TODO *)
+    | TAny _ -> assert false
+    | TVar _ -> (* TODO ? *) acc
     | TOption _ | TTuple _ ->
       Message.error ~internal:true ~pos:(Mark.get typ)
         "Some types in tuples or option have not been resolved by the \

compiler/shared_ast/operator.ml

@@ -556,7 +556,7 @@ let resolve_overload_aux (op : overloaded t) (operands : typ_lit list) :
     raise Not_found
 
 let resolve_overload
-    ctx
+    _ctx
     ((op, pos) : overloaded t Mark.pos)
     (operands : typ list) :
     < resolved : yes ; .. > t Mark.pos * [ `Straight | `Reversed ] =

tests/array/bad/type_error_in_filter.catala_en

@@ -36,7 +36,7 @@ $ catala dcalc
 │
 │  Error during typechecking, incompatible types:
 │  ─➤ St
-│  ─➤ list of any
+│  ─➤ list of <ty1>
 │
 │ While typechecking the following expression:
 ├─➤ tests/array/bad/type_error_in_filter.catala_en:13.34-13.38:
@@ -50,7 +50,7 @@ $ catala dcalc
 │ 7 │   input ll content list of St
 │   │                            ‾‾
 │
-│ Type list of any is coming from:
+│ Type list of <ty1> 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)
@@ -66,7 +66,7 @@ $ catala test-scope Test
 │
 │  Error during typechecking, incompatible types:
 │  ─➤ St
-│  ─➤ list of any
+│  ─➤ list of <ty1>
 │
 │ While typechecking the following expression:
 ├─➤ tests/array/bad/type_error_in_filter.catala_en:13.34-13.38:
@@ -80,7 +80,7 @@ $ catala test-scope Test
 │ 7 │   input ll content list of St
 │   │                            ‾‾
 │
-│ Type list of any is coming from:
+│ Type list of <ty1> 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)

tests/array/good/aggregation_4.catala_en

@@ -40,17 +40,17 @@ scope Section121SinglePerson:
 
 ```catala-test-inline
 $ catala lcalc --closure-conversion
-type Eoption = | ENone of unit | ESome of any
+type Eoption = | ENone of unit | ESome of <ty1>
 
 type Period = { begin: date; end: date; }
 type Section121SinglePerson_in = {
   date_of_sale_or_exchange_in: date;
-  property_ownage_in: list of Period {begin: date; end: date};
+  property_ownage_in: list of Period;
 }
 type Section121SinglePerson = { requirements_ownership_met: bool; }
 
 let topval closure_aggregate_periods_from_last_five_years :
-  (closure_env, Period {begin: date; end: date}) → duration =
+  (closure_env, Period) → duration =
   λ (env: closure_env) (period: Period) →
   let env__1 : (date) = from_closure_env env in
   let date_of_sale_or_exchange : date = env__1.0 in
@@ -72,7 +72,7 @@ let topval closure_aggregate_periods_from_last_five_years__1 :
   ((sum1 + sum2))
 
 let topval closure_aggregate_periods_from_last_five_years__2 :
-  (closure_env, (list of Period {begin: date; end: date})) → duration =
+  (closure_env, (list of Period)) → duration =
   λ (env: closure_env) (periods: list of Period) →
   let env__1 : (date) = from_closure_env env in
   let date_of_sale_or_exchange : date = env__1.0 in
@@ -97,22 +97,17 @@ let topval closure_aggregate_periods_from_last_five_years__2 :
   | ESome arg → arg
 
 let scope section121_single_person
-  (section121_single_person_in:
-     Section121SinglePerson_in {
-       date_of_sale_or_exchange_in: date;
-       property_ownage_in: list of Period {begin: date; end: date}
-     })
-  : Section121SinglePerson {requirements_ownership_met: bool}
+  (section121_single_person_in: Section121SinglePerson_in)
+  : Section121SinglePerson
   =
   let get date_of_sale_or_exchange : date =
     section121_single_person_in.date_of_sale_or_exchange_in
   in
-  let get property_ownage : list of Period {begin: date; end: date} =
+  let get property_ownage : list of Period =
     section121_single_person_in.property_ownage_in
   in
   let set aggregate_periods_from_last_five_years :
-      ((closure_env, (list of Period {begin: date; end: date})) → duration,
-        closure_env) =
+      ((closure_env, (list of Period)) → duration, closure_env) =
     let aggregate_periods_from_last_five_years__1 :
         (closure_env, (list of Period)) → duration =
       closure_aggregate_periods_from_last_five_years__2

tests/exception/good/double_definition.catala_en

@@ -84,7 +84,7 @@ $ catala Dcalc -s Foo
 │ 8 │   definition x equals 1
 │   │   ‾‾‾‾‾‾‾‾‾‾‾‾
 └─ Foo
-let scope Foo (Foo_in: Foo_in): Foo {x: integer} =
+let scope Foo (Foo_in: Foo_in): Foo =
   let set x : integer =
     error_empty ⟨ ⟨ ⟨true ⊢ ⟨1⟩⟩ | true ⊢ ⟨1⟩ ⟩ | false ⊢ ∅ ⟩
   in

tests/exception/good/groups_of_exceptions.catala_en

@@ -77,9 +77,8 @@ let scope Foo (y: integer|input) (x: integer|internal|output) =
         | true ⊢ ⟨ ⟨y = 2 ⊢ ⟨2⟩⟩, ⟨y = 3 ⊢ ⟨3⟩⟩ | false ⊢ ∅ ⟩ ⟩
       | true ⊢ ⟨ ⟨y = 0 ⊢ ⟨0⟩⟩, ⟨y = 1 ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩ ⟩
 
-let scope Test (x: integer|internal|output) (f: Foo {x: integer}|internal) =
-  let f : Foo {x: integer} =
-    Foo of {"y"= error_empty ⟨ ⟨true ⊢ ⟨2⟩⟩ | false ⊢ ∅ ⟩};
+let scope Test (x: integer|internal|output) (f: Foo|internal) =
+  let f : Foo = Foo of {"y"= error_empty ⟨ ⟨true ⊢ ⟨2⟩⟩ | false ⊢ ∅ ⟩};
   let x : integer = error_empty ⟨ ⟨true ⊢ ⟨f.x⟩⟩ | false ⊢ ∅ ⟩
 ```
 

tests/func/good/closure_conversion.catala_en

@@ -25,7 +25,7 @@ $ catala Typecheck --check-invariants
 
 ```catala-test-inline
 $ catala Lcalc -O --closure-conversion
-type Eoption = | ENone of unit | ESome of any
+type Eoption = | ENone of unit | ESome of <ty1>
 
 type S_in = { x_in: bool; }
 type S = { z: integer; }
@@ -34,7 +34,7 @@ let topval closure_f : (closure_env, integer) → integer =
   λ (env: closure_env) (y: integer) →
   if (from_closure_env env).0 then y else - y
 
-let scope s (s_in: S_in {x_in: bool}): S {z: integer} =
+let scope s (s_in: S_in): S =
   let get x : bool = s_in.x_in in
   let set f : ((closure_env, integer) → integer, closure_env) =
     (closure_f, to_closure_env (x))
@@ -68,32 +68,11 @@ scope S2Use:
 
 ```catala-test-inline
 $ catala Lcalc -O --closure-conversion -s S2Use
-let scope S2Use
-  (s2_use_in: S2Use_in)
-  : S2Use {
-      o:
-        (S2 {
-           dummy: bool;
-           cfun2: ((closure_env, integer) → decimal, closure_env)
-         },
-          S2 {
-            dummy: bool;
-            cfun2: ((closure_env, integer) → decimal, closure_env)
-          })
-    }
-  =
+let scope S2Use (s2_use_in: S2Use_in): S2Use =
   let set fun : ((closure_env, integer) → decimal, closure_env) =
     (closure_fun, to_closure_env ())
   in
-  let set o :
-      (S2 {
-         dummy: bool;
-         cfun2: ((closure_env, integer) → decimal, closure_env)
-       },
-        S2 {
-          dummy: bool;
-          cfun2: ((closure_env, integer) → decimal, closure_env)
-        }) =
+  let set o : (S2, S2) =
     (let result : S2 = s2 { S2_in cfun2_in = fun; } in
      { S2
        dummy = result.dummy;

tests/func/good/closure_conversion_reduce.catala_en

@@ -32,7 +32,7 @@ back on and translate to loops at some point.
 
 ```catala-test-inline
 $ catala Lcalc -s S -O --closure-conversion
-let scope S (s_in: S_in {x_in: list of integer}): S {y: integer} =
+let scope S (s_in: S_in): S =
   let get x : list of integer = s_in.x_in in
   let set y : integer =
     (reduce
@@ -55,7 +55,7 @@ with optimizations on passes.
 
 ```catala-test-inline
 $ catala Lcalc -s S --closure-conversion
-let scope S (s_in: S_in {x_in: list of integer}): S {y: integer} =
+let scope S (s_in: S_in): S =
   let get x : list of integer = s_in.x_in in
   let set y : integer =
     match

tests/func/good/closure_return.catala_en

@@ -23,7 +23,7 @@ $ catala Typecheck --check-invariants
 
 ```catala-test-inline
 $ catala Lcalc -O --closure-conversion
-type Eoption = | ENone of unit | ESome of any
+type Eoption = | ENone of unit | ESome of <ty1>
 
 type S_in = { x_in: bool; }
 type S = { f: ((closure_env, integer) → integer, closure_env); }
@@ -32,10 +32,7 @@ let topval closure_f : (closure_env, integer) → integer =
   λ (env: closure_env) (y: integer) →
   if (from_closure_env env).0 then y else - y
 
-let scope s
-  (s_in: S_in {x_in: bool})
-  : S {f: ((closure_env, integer) → integer, closure_env)}
-  =
+let scope s (s_in: S_in): S =
   let get x : bool = s_in.x_in in
   let set f : ((closure_env, integer) → integer, closure_env) =
     (closure_f, to_closure_env (x))

tests/func/good/closure_through_scope.catala_en

@@ -31,10 +31,8 @@ $ catala Typecheck --check-invariants
 
 ```catala-test-inline
 $ catala Lcalc -s T -O --closure-conversion
-let scope T (t_in: T_in): T {y: integer} =
-  let set s__1 : S {f: ((closure_env, integer) → integer, closure_env)} =
-    { S f = (closure_s, to_closure_env ()); }
-  in
+let scope T (t_in: T_in): T =
+  let set s__1 : S = { S f = (closure_s, to_closure_env ()); } in
   let set y : integer =
     let code_and_env : ((closure_env, integer) → integer, closure_env) =
       s__1.f

tests/func/good/context_func.catala_en

@@ -49,8 +49,8 @@ $ catala Scopelang -s B
 │ 9 │   a scope A
 │   │   ‾
 └─ Test
-let scope B (b: bool|input) (a: A {f: integer → integer}|internal) =
-  let a : A {f: integer → integer} =
+let scope B (b: bool|input) (a: A|internal) =
+  let a : A =
     A of {"f"= (λ (x: integer) → ⟨ ⟨b && x > 0 ⊢ ⟨x - 1⟩⟩ | false ⊢ ∅ ⟩)}
 ```
 
@@ -66,10 +66,7 @@ $ catala Dcalc -s A
 │ 9 │   a scope A
 │   │   ‾
 └─ Test
-let scope A
-  (A_in: A_in {f_in: integer → ⟨integer⟩})
-  : A {f: integer → integer}
-  =
+let scope A (A_in: A_in): A =
   let get f : integer → ⟨integer⟩ = A_in.f_in in
   let set f : integer → integer =
     λ (x: integer) →
@@ -91,9 +88,9 @@ $ catala Dcalc -s B
 │ 9 │   a scope A
 │   │   ‾
 └─ Test
-let scope B (B_in: B_in {b_in: bool}): B =
+let scope B (B_in: B_in): B =
   let get b : bool = B_in.b_in in
-  let set a : A {f: integer → integer} =
+  let set a : A =
     let result : A =
       A
         { A_in

tests/func/good/scope_call_func_struct_closure.catala_en

@@ -54,7 +54,7 @@ $ catala Typecheck --check-invariants
 
 ```catala-test-inline
 $ catala Lcalc -O --closure-conversion 
-type Eoption = | ENone of unit | ESome of any
+type Eoption = | ENone of unit | ESome of <ty1>
 
 type Result = {
   r: ((closure_env, integer) → integer, closure_env);
@@ -77,13 +77,7 @@ let topval closure_y : (closure_env, integer) → integer =
   λ (env: closure_env) (z: integer) →
   (from_closure_env env).0 + z
 
-let scope sub_foo1
-  (sub_foo1_in: SubFoo1_in {x_in: integer})
-  : SubFoo1 {
-      x: integer;
-      y: ((closure_env, integer) → integer, closure_env)
-    }
-  =
+let scope sub_foo1 (sub_foo1_in: SubFoo1_in): SubFoo1 =
   let get x : integer = sub_foo1_in.x_in in
   let set y : ((closure_env, integer) → integer, closure_env) =
     (closure_y, to_closure_env (x))
@@ -95,13 +89,7 @@ let topval closure_y__1 : (closure_env, integer) → integer =
   let env__1 : (integer, integer) = from_closure_env env in
   ((env__1.1 + env__1.0 + z))
 
-let scope sub_foo2
-  (sub_foo2_in: SubFoo2_in {x1_in: integer; x2_in: integer})
-  : SubFoo2 {
-      x1: integer;
-      y: ((closure_env, integer) → integer, closure_env)
-    }
-  =
+let scope sub_foo2 (sub_foo2_in: SubFoo2_in): SubFoo2 =
   let get x1 : integer = sub_foo2_in.x1_in in
   let get x2 : integer = sub_foo2_in.x2_in in
   let set y : ((closure_env, integer) → integer, closure_env) =
@@ -123,16 +111,12 @@ let topval closure_r__1 : (closure_env, integer) → integer =
   in
   code_and_env.0 code_and_env.1 param0
 
-let scope foo (foo_in: Foo_in {b_in: option bool}): Foo {z: integer} =
+let scope foo (foo_in: Foo_in): Foo =
   let get b : option bool = foo_in.b_in in
   let set b__1 : bool = match b with
                         | ENone → true
                         | ESome x → x in
-  let set r :
-      Result {
-        r: ((closure_env, integer) → integer, closure_env);
-        q: integer
-      } =
+  let set r : Result =
     if b__1 then
       let f : SubFoo1 =
         let result : SubFoo1 = sub_foo1 { SubFoo1_in x_in = 10; } in

tests/io/good/all_io.catala_en

@@ -31,11 +31,7 @@ $ catala Typecheck --check-invariants
 
 ```catala-test-inline
 $ catala Dcalc -s A
-let scope A
-  (A_in:
-     A_in {c_in: integer; d_in: integer; e_in: ⟨integer⟩; f_in: ⟨integer⟩})
-  : A {b: integer; d: integer; f: integer}
-  =
+let scope A (A_in: A_in): A =
   let get c : integer = A_in.c_in in
   let get d : integer = A_in.d_in in
   let get e : ⟨integer⟩ = A_in.e_in in

tests/io/good/condition_only_input.catala_en

@@ -29,7 +29,7 @@ $ catala Typecheck --check-invariants
 ```catala-test-inline
 $ catala Dcalc -s B
 let scope B (B_in: B_in): B =
-  let set a : A {y: integer} =
+  let set a : A =
     let result : A =
       A { A_in x_in = error_empty ⟨ ⟨true ⊢ ⟨false⟩⟩ | false ⊢ ∅ ⟩; }
     in

tests/io/good/subscope.catala_en

@@ -35,7 +35,7 @@ $ catala Typecheck --check-invariants
 ```catala-test-inline
 $ catala Dcalc -s B
 let scope B (B_in: B_in): B =
-  let set a : A {c: integer} =
+  let set a : A =
     let result : A =
       A
         { A_in

tests/monomorphisation/context_var.catala_en

@@ -12,14 +12,11 @@ scope TestXor:
 $ catala lcalc --monomorphize-types
 type option_1 = | None_1 of unit | Some_1 of bool
 
-type TestXor_in = { t_in: option_1[None_1: unit | Some_1: bool]; }
+type TestXor_in = { t_in: option_1; }
 type TestXor = { t: bool; }
 
-let scope test_xor
-  (test_xor_in: TestXor_in {t_in: option_1[None_1: unit | Some_1: bool]})
-  : TestXor {t: bool}
-  =
-  let get t : option_1[None_1: unit | Some_1: bool] = test_xor_in.t_in in
+let scope test_xor (test_xor_in: TestXor_in): TestXor =
+  let get t : option_1 = test_xor_in.t_in in
   let set t__1 : bool =
     match
       (match t with
@@ -48,8 +45,8 @@ scope TestXor2:
 
 ```catala-test-inline
 $ catala lcalc --monomorphize-types -s TestXor2
-let scope TestXor2 (test_xor2_in: TestXor2_in): TestXor2 {o: bool} =
-  let set t : TestXor {t: bool} =
+let scope TestXor2 (test_xor2_in: TestXor2_in): TestXor2 =
+  let set t : TestXor =
     let result : TestXor = test_xor { TestXor_in t_in = None_1 (); } in
     let result__1 : TestXor = { TestXor t = result.t; } in
     if true then result__1 else result__1