Merge branch 'master' into c_backend

2024-09-19 00:15:39 +03:00 · 2024-01-26 17:43:07 +01:00 · 2024-01-26 17:43:07 +01:00 · a39b67bf12
commit a39b67bf12
parent 8a139f6a3c 2d8bdca624
149 changed files with 927 additions and 1009 deletions
--- a/.github/workflows/harness.yml
+++ b/.github/workflows/harness.yml
@ -0,0 +1,205 @@
+name: CI
+
+on:
+  push:
+    branches: [master]
+    tags: ['*.*.*']
+  workflow_dispatch:
+  pull_request_target:
+  # It is important to use `pull_request_target` and not `pull_request` here: it
+  # means the version of this file from master is used rather than the one from
+  # the PR. This allows writing to the docker caches, etc. from PRs ; but mind
+  # that if you attempt modification in a PR, of course.
+
+# A workflow run is made up of one or more jobs that can run sequentially or in parallel
+jobs:
+
+  build:
+    name: Build Catala and generate image
+    runs-on: self-hosted
+    permissions:
+      packages: write
+    outputs:
+      image: ghcr.io/catalalang/catala@${{ steps.image.outputs.digest }}
+      version: ${{ steps.describe.outputs.version }}
+    steps:
+      - name: Checkout
+        # This is *only* needed to extract the git version...
+        # Approaches like proudust/gh-describe@v1 don't work
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 0 # Need full commit history for 'git describe'
+      - name: Get git-describe version
+        id: describe
+        run: echo "version=$(git describe --tags)" >> "$GITHUB_OUTPUT"
+      - name: Get an image tag that Docker accepts
+        id: branch
+        run: sed 's/[^a-zA-Z0-9-]/-/g; s/^/tag=/' <<<"${{ github.head_ref || github.ref_name }}" >> "$GITHUB_OUTPUT"
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v3
+      - name: Login to GHCR
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+      - name: Make build context image
+        uses: docker/build-push-action@v5
+        with:
+          target: dev-build-context
+          # Caching using GH cache doesn't work, use registry caching directly
+          # instead
+          cache-from: |
+            type=registry,ref=ghcr.io/catalalang/catala:dev-cache-master
+            type=registry,ref=ghcr.io/catalalang/catala:dev-cache-${{ steps.branch.outputs.tag }}
+          cache-to: |
+            type=registry,ref=ghcr.io/catalalang/catala:dev-cache-${{ steps.branch.outputs.tag }},mode=max
+      - name: Build and push
+        id: image
+        uses: docker/build-push-action@v5
+        with:
+          push: true
+          tags: ghcr.io/catalalang/catala:${{ steps.describe.outputs.version }}
+          build-args: "CATALA_VERSION=${{ steps.describe.outputs.version }}"
+          labels: org.opencontainers.image.source=${{ github.server_url }}/${{ github.repository }}
+          cache-from: |
+            type=registry,ref=ghcr.io/catalalang/catala:build-cache-master
+            type=registry,ref=ghcr.io/catalalang/catala:build-cache-${{ steps.branch.outputs.tag }}
+          cache-to: |
+            type=registry,ref=ghcr.io/catalalang/catala:build-cache-${{ steps.branch.outputs.tag }},mode=max
+
+  tests:
+    name: Run integrated tests
+    needs: build
+    runs-on: self-hosted
+    container:
+      image: ${{ needs.build.outputs.image }}
+      options: --user ocaml
+    steps:
+      - name: Check promoted files
+        run: cd /home/ocaml/catala && opam exec -- make check-promoted
+      - name: Run tests
+        if: ${{ always() }}
+        run: cd /home/ocaml/catala && opam exec -- make tests
+
+  examples:
+    name: Build examples and generate artifacts
+    needs: build
+    runs-on: self-hosted
+    container:
+      image: ${{ needs.build.outputs.image }}
+      options: --user ocaml
+      env:
+        DUNE_PROFILE: release
+    steps:
+      - name: Fix home
+        # Workaround Github actions issue, see
+        # https://github.com/actions/runner/issues/863
+        run: sudo sh -c "echo HOME=/home/ocaml >> ${GITHUB_ENV}"
+      - name: Install LaTeX deps
+        # This is done late because caching would not benefit compared to
+        # installation through apk (1,5G upload is slow)
+        run: sudo apk add texlive-xetex texmf-dist-latexextra texmf-dist-pictures font-dejavu groff
+      - name: Build Catala extra docs
+        run: |
+          cd ~/catala
+          opam --cli=2.1 exec -- make syntax
+          opam --cli=2.1 exec -- make doc
+      - name: Checkout examples repo
+        # Github fetch action is expected to work for containers, but doesn't
+        # (permission issues)
+        run: git clone https://github.com/CatalaLang/catala-examples --depth 1 ~/catala-examples
+      - name: Build examples
+        run: cd ~/catala-examples && opam --cli=2.1 exec -- make build install
+      - name: Checkout french-law repo
+        run: git clone https://github.com/CatalaLang/french-law --depth 1 ~/french-law
+      - name: Build french-law
+        run: |
+          cd ~/french-law
+          opam --cli=2.1 exec -- make dependencies
+          opam --cli=2.1 exec -- make all
+      - name: Gather all artifacts
+        run: |
+          cd
+          mkdir -p artifacts
+          mv catala/_build/default/_doc/_html artifacts/api-doc
+          mv catala/doc/syntax/syntax.pdf artifacts/
+          mv catala/_build/default/*.html artifacts/
+          mv ~/.opam/catala/doc/catala-examples/tuto*/*.html artifacts/
+          tar czf "artifacts/french_law_ocaml.tar.gz" french-law/ocaml
+          tar czf "artifacts/french_law_js.tar.gz" french-law/js
+          tar czf "artifacts/french_law_python.tar.gz" french-law/python
+      - name: Upload artifacts
+        continue-on-error: true
+        # Uploading artifacts works but then return failure with:
+        # EACCES: permission denied, open '/__w/_temp/_runner_file_commands/set_output_xxx'
+        # a chmod doesn't work around it so we resort to just ignoring the error...
+        uses: actions/upload-artifact@v4
+        with:
+          name: Catala examples
+          path: /home/ocaml/artifacts/*
+
+  binaries:
+    name: Build static binaries
+    runs-on: self-hosted
+    if: ${{ github.event_name != 'pull_request_target' }}
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 0 # Need full commit history for 'git describe'
+      - name: Get git-describe version
+        id: describe
+        run: echo "version=$(git describe --tags)" >> "$GITHUB_OUTPUT"
+      - name: Build release binaries
+        run: |
+          mkdir -p artifacts
+          export CATALA_VERSION="${{ steps.describe.outputs.version }}"
+          ./build_release.sh -C artifacts
+      - name: Upload artifacts
+        uses: actions/upload-artifact@v4
+        with:
+          name: Catala binaries
+          path: artifacts/*
+
+  pages:
+    name: Publish static content to github-pages
+    needs: [ examples, binaries, tests ]
+    # Doesn't really depend on tests, but we don't want to publish if they fail
+    if: ${{ github.event_name != 'pull_request_target' && github.ref == 'refs/heads/master' }}
+    # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+    permissions:
+      contents: read
+      pages: write
+      id-token: write
+    # Allow one concurrent deployment
+    concurrency:
+      group: "pages"
+      cancel-in-progress: true
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    steps:
+      - name: Setup Pages
+        uses: actions/configure-pages@v3
+      - name: Download artifacts
+        uses: actions/download-artifact@v4
+        with:
+          merge-multiple: true
+          path: artifacts/
+      - uses: awalsh128/cache-apt-pkgs-action@latest
+        with:
+          packages: tree
+          version: 1.0
+      - name: Generate HTML index
+        run: |
+          cd artifacts
+          tree -H . -L 1 --noreport --dirsfirst -T 'Catala latest development artifacts' --charset utf-8 -o index.html
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: 'artifacts/'
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1
--- a/.github/workflows/publish-artifacts.yml
+++ b/.github/workflows/publish-artifacts.yml
@ -1,59 +0,0 @@
-# Simple workflow for deploying static content to GitHub Pages
-name: Deploy static content to Pages
-
-on:
-  workflow_run:
-    workflows: ["Harness"]
-    branches: [master]
-    types:
-      - completed
-
-  # Allows you to run this workflow manually from the Actions tab
-  workflow_dispatch:
-
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
-permissions:
-  contents: read
-  pages: write
-  id-token: write
-
-# Allow one concurrent deployment
-concurrency:
-  group: "pages"
-  cancel-in-progress: true
-
-jobs:
-  # Single deploy job since we're just deploying
-  deploy:
-    # Don't run if test harness failed
-    if: ${{ github.event.workflow_run.conclusion == 'success' }}
-    environment:
-      name: github-pages
-      url: ${{ steps.deployment.outputs.page_url }}
-    runs-on: ubuntu-latest
-    steps:
-      - name: Setup Pages
-        uses: actions/configure-pages@v3
-      - name: Download build artifacts
-        # Not the default gh download-artifact action, which doesn't work
-        # between workflows
-        uses: dawidd6/action-download-artifact@v2
-        with:
-          workflow: ${{ github.event.workflow_run.workflow_id }}
-          name: Catala artifacts
-          path: artifacts/
-      - uses: awalsh128/cache-apt-pkgs-action@latest
-        with:
-          packages: tree
-          version: 1.0
-      - name: Generate HTML index
-        run: |
-          cd artifacts
-          tree -H . -L 1 --noreport --dirsfirst -T 'Catala latest development artifacts' --charset utf-8 -o index.html
-      - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
-        with:
-          path: 'artifacts/'
-      - name: Deploy to GitHub Pages
-        id: deployment
-        uses: actions/deploy-pages@v1
--- a/.github/workflows/run-make-all.yml
+++ b/.github/workflows/run-make-all.yml
@ -1,65 +0,0 @@
-name: Harness
-
-on:
-  push:
-    branches: [master]
-  pull_request:
-
-# A workflow run is made up of one or more jobs that can run sequentially or in parallel
-jobs:
-  run-make-all:
-    # The type of runner that the job will run on
-    runs-on: self-hosted
-
-    env:
-      IMAGE_TAG: ${{ github.head_ref || github.ref_name }}
-
-    # Steps represent a sequence of tasks that will be executed as part of the job
-    steps:
-      - name: Checkout code
-        uses: actions/checkout@v3
-        with:
-          fetch-depth: 0
-      - name: Prepare container with all dependencies
-        run: git archive HEAD | docker build - --target dev-build-context
-      - name: Escape chars in IMAGE_TAG (to avoid Docker issues)
-        run: sed 's/[^a-zA-Z0-9-]/-/g; s/^/IMAGE_TAG=/' <<<"${IMAGE_TAG}" >> $GITHUB_ENV
-      - name: Run builds, checks and tests
-        run: git archive HEAD | docker build - --force-rm -t "catalalang/catala-build:${IMAGE_TAG}"
-      - name: Cleanup Docker image
-        if: ${{ github.ref != 'refs/heads/master' }}
-        run: docker image rm catalalang/catala-build:${IMAGE_TAG}
-      - name: Build architecture-independent artifacts
-        if: ${{ github.ref == 'refs/heads/master' }}
-        run: |
-          RELEASE_TAG=$(git describe --tags)
-          docker run --rm catalalang/catala-build:${IMAGE_TAG} sh -uexc '
-              opam --cli=2.1 remove z3 >&2
-              opam --cli=2.1 exec -- dune build --profile=release french_law compiler/catala.bc.js >&2
-              opam --cli=2.1 exec -- dune build --profile=release @doc >&2
-              sudo apk add font-dejavu >&2
-              opam --cli=2.1 exec -- make -C doc/syntax >&2
-              opam --cli=2.1 exec -- make literate_tutorial_en literate_tutoriel_fr >&2
-              opam --cli=2.1 exec -- dune build --profile=release grammar.html catala.html clerk.html >&2
-              mkdir -p artifacts >&2
-              mv _build/default/compiler/catala.bc.js artifacts/catala_'"${RELEASE_TAG}"'_node.js >&2
-              mv _build/default/_doc/_html artifacts/api-doc >&2
-              mv doc/syntax/syntax.pdf artifacts/ >&2
-              mv examples/tuto*/*.html _build/default/*.html artifacts/ >&2
-              tar czf artifacts/french_law_'"${RELEASE_TAG}"'_ocaml.tar.gz french_law/ocaml >&2
-              tar czf artifacts/french_law_'"${RELEASE_TAG}"'_js.tar.gz french_law/js --exclude french_law/js/node_modules >&2
-              tar czf artifacts/french_law_'"${RELEASE_TAG}"'_python.tar.gz french_law/python >&2
-              ln -s french_law_'"${RELEASE_TAG}"'_ocaml.tar.gz artifacts/french_law_ocaml.tar.gz >&2
-              ln -s french_law_'"${RELEASE_TAG}"'_js.tar.gz artifacts/french_law_js.tar.gz >&2
-              ln -s french_law_'"${RELEASE_TAG}"'_python.tar.gz artifacts/french_law_python.tar.gz >&2
-              tar c artifacts/*
-            ' | tar vx
-      - name: Build static binaries
-        if: ${{ github.ref == 'refs/heads/master' }}
-        run: ./build_release.sh -C artifacts
-      - name: Publish artifacts
-        if: ${{ github.ref == 'refs/heads/master' }}
-        uses: actions/upload-artifact@v3
-        with:
-          name: Catala artifacts
-          path: artifacts/*
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@ -21,10 +21,10 @@ distributed under the Apache2 license.

 Before writing Catala code, please read the
 [tutorial](https://catala-lang.org/en/examples/tutorial). You can run the
-programs of the tutorial yourself by following the instruction in the
-[README of the `examples` directory](examples/README.md). Then, it is suggested
-that you create a new example directory again according to the instructions of
-this README.
+programs of the tutorial yourself by following the instruction in the [README of
+the `examples` repository](https://github.com/CatalaLang/catala-examples/README.md).
+Then, it is suggested that you create a new example directory again according to
+the instructions of this README.

 Let us now present the typical Catala workflow. First, you need to locate
 the legislative text that you want to use as a reference. Then, simply
@ -77,9 +77,11 @@ declaration structure FooBar:
 ```
 ````

-Again, make sure to regularly check that your example is parsing correctly. The error message from the compiler should help you debug the syntax if need be. You can also
-live-test the programs you wrote by feeding them to the interpreter
-(see the [README of the `examples` directory](examples/README.md)); this will
+Again, make sure to regularly check that your example is parsing correctly. The
+error message from the compiler should help you debug the syntax if need be. You
+can also live-test the programs you wrote by feeding them to the interpreter
+(see the [README of the `examples`
+repository](https://github.com/CatalaLang/catala-examples/README.md)); this will
 also type-check the programs, which is useful for debugging them.

 ## Working on the compiler
--- a/27
+++ b/27
@ -26,34 +26,29 @@ RUN opam --cli=2.1 switch create catala ocaml-system && \
 # should be enough once opam 2.2 is released (see opam#5185)

 #
-# STAGE 2: get the whole repo, run checks and builds
+# STAGE 2: get the whole repo and build
 #
 FROM dev-build-context

+# Prepare extra local dependencies (doing this first allows caching)
+ADD --chown=ocaml:ocaml runtimes/python/pyproject.toml runtimes/python/pyproject.toml
+ADD --chown=ocaml:ocaml Makefile .
+ADD --chown=ocaml:ocaml syntax_highlighting syntax_highlighting
+RUN opam exec -- make dependencies-python pygments
+
 # Get the full repo
 ADD --chown=ocaml:ocaml . .

-# Prepare extra local dependencies
-RUN opam exec -- make dependencies-python pygments
-
 # OCaml backtraces may be useful on failure
 ENV OCAMLRUNPARAM=b
 # Make sure warnings are treated as errors (variable used in Makefile, profile
 # defined in ./dune)
 ENV DUNE_PROFILE=check

-# Check promoted files (but delay failure)
-RUN opam exec -- make check-promoted > promotion.out 2>&1 || touch bad-promote
+ARG CATALA_VERSION

 # Check the build
-RUN opam exec -- make build
+RUN opam exec -- make build js_build

-# Check tests & all alt targets
-RUN OCAMLRUNPARAM=b opam exec -- make all -B
-
-# Forward results of promotion check
-RUN if [ -e bad-promote ]; then \
-  echo "[ERROR] Some promoted files were not up-to-date"; \
-  cat promotion.out; \
-  exit 1; \
-fi
+# Install to prefix
+RUN opam exec -- make install && opam clean
--- a/21
+++ b/21
@ -88,8 +88,7 @@ build: parser-messages format build_dev

 #> js_build				: Builds the Web-compatible JS versions of the Catala compiler
 js_build:
-	dune build $(COMPILER_DIR)/catala.bc.js
-	dune build $(COMPILER_DIR)/catala_web_interpreter.bc.js
+	dune build $(COMPILER_DIR)/catala.bc.js $(COMPILER_DIR)/catala_web_interpreter.bc.js

 #> doc					: Generates the HTML OCaml documentation
 doc:
@ -180,6 +179,7 @@ vscode: vscode_fr vscode_en
 # Extra documentation
 ##########################################

+#> syntax					: Buils syntax sheet (requires latexmk and dejavu fonts)
 syntax:
 	$(MAKE) -C doc/syntax

@ -199,8 +199,11 @@ CLERK=$(CLERK_BIN) --exe $(CATALA_BIN) \

 .FORCE:

+unit-tests: .FORCE
+	dune runtest
+
 #> tests					: Run interpreter tests
-tests: .FORCE prepare-install
+tests: .FORCE prepare-install unit-tests
 	@$(MAKE) -C tests pass_all_tests

 tests/%: .FORCE
@ -210,6 +213,8 @@ tests/%: .FORCE
 # Website assets
 ##########################################

+# Note: these are already built by the @doc dune alias
+# (and therefore the doc target here)
 WEBSITE_ASSETS = grammar.html catala.html clerk.html

 $(addprefix _build/default/,$(WEBSITE_ASSETS)):
@ -231,21 +236,13 @@ all: \
 	build js_build doc \
 	tests \
 	runtimes \
-	plugins \
-	website-assets-base
+	plugins


 #> clean					: Clean build artifacts
 clean:
 	dune clean
 	rm -rf artifacts
-	$(MAKE) -C $(AIDES_LOGEMENT_DIR) clean
-	$(MAKE) -C $(ALLOCATIONS_FAMILIALES_DIR) clean
-	$(MAKE) -C $(US_TAX_CODE_DIR) clean
-	$(MAKE) -C $(TUTORIEL_FR_DIR) clean
-	$(MAKE) -C $(TUTORIAL_EN_DIR) clean
-	$(MAKE) -C $(POLISH_TAXES_DIR) clean
-	$(MAKE) -C $(CODE_GENERAL_IMPOTS_DIR) clean

 inspect:
 	gitinspector -f ml,mli,mly,iro,tex,catala,catala_en,catala_pl,catala_fr,md,fst,mld --grading
--- a/README.md
+++ b/README.md
@ -185,7 +185,7 @@ to generate the documentation, then open the `doc/odoc.html` file in any browser
 ## Examples

 To explore the different programs written in Catala, see
-[the dedicated readme](examples/README.md).
+[the dedicated readme](https://github.com/CatalaLang/catala-examples/README.md).

 ## API

--- a/build_release.sh
+++ b/build_release.sh
@ -2,9 +2,9 @@

 set -ue

-RELEASE_TAG=${RELEASE_TAG:-$(git describe --tags 2>/dev/null || echo dev)}
+CATALA_VERSION=${CATALA_VERSION:-$(git describe --tags 2>/dev/null || echo dev)}

-BIN_TAG=${BIN_TAG:-$(uname -s)_$(uname -m)}
+BIN_TAG=${BIN_TAG:-$(uname -s)-$(uname -m)}

 CUSTOM_LINKING_CATALA_Z3="\
 (-cclib -static
@ -26,21 +26,21 @@ CUSTOM_LINKING_CATALA_NOZ3="(-cclib -static -cclib -no-pie)"
 CUSTOM_LINKING_CLERK="(-cclib -static -cclib -no-pie)"

 git archive HEAD --prefix catala/ | \
-docker run --rm -i registry.gitlab.inria.fr/lgesbert/catala-ci-images:ocaml.4.14-z3static.4.11.2 \
+docker run --rm -i registry.gitlab.inria.fr/verifisc/docker-catala:ocaml.4.14-z3static.4.11.2 \
  sh -uexc \
    '{ tar x &&
       cd catala &&
+       export CATALA_VERSION='"${CATALA_VERSION}"' &&
       echo "'"${CUSTOM_LINKING_CATALA_Z3}"'" >compiler/custom_linking.sexp &&
       echo "'"${CUSTOM_LINKING_CLERK}"'" >build_system/custom_linking.sexp &&
-       opam --cli=2.1 install ./ninja_utils.opam ./clerk.opam ./catala.opam --destdir ../release.out/ &&
+       opam --cli=2.1 install ./catala.opam --destdir ../release.out/ &&
       mv ../release.out/bin/catala ../release.out/bin/catala-z3 &&
       opam --cli=2.1 remove z3 catala &&
       echo "'"${CUSTOM_LINKING_CATALA_NOZ3}"'" >compiler/custom_linking.sexp &&
       opam --cli=2.1 install ./catala.opam --destdir ../release.out/ &&
-       rm -f ../release.out/bin/catala_web_interpreter &&
-       for f in ../release.out/bin/*; do
-         strip ${f};
-         mv ${f} ${f}_'"${RELEASE_TAG}"'_'"${BIN_TAG}"';
-       done;
+       for f in ../release.out/bin/*; do case ${f} in
+         *.js) mv ${f} ${f%.js}-'"${CATALA_VERSION}"'.js;;
+         *) strip ${f}; mv ${f} ${f}-'"${CATALA_VERSION}"'-'"${BIN_TAG}"';;
+       esac; done;
     } >&2 && tar c -hC ../release.out/bin .' |
 tar vx "$@"
--- a/build_system/clerk_driver.ml
+++ b/build_system/clerk_driver.ml
@ -256,7 +256,10 @@ module Poll = struct
  let catala_project_root : File.t option Lazy.t =
    lazy
      (match Lazy.force project_root with
-      | Some root when Sys.file_exists File.(root / "catala.opam") -> Some root
+      | Some root
+        when Sys.file_exists File.(root / "catala.opam")
+             && Sys.file_exists File.(root / "dune-project") ->
+        Some root
      | _ -> None)

  let exec_dir : File.t =
@ -337,9 +340,10 @@ module Poll = struct
         dir
       | None ->
         Message.raise_error
-           "@[<hov>Could not locate the Catala runtime library.@ Make sure \
-            that either catala is correctly installed,@ or you are running \
-            from the root of a compiled source tree.@]")
+           "@[<hov>Could not locate the Catala runtime library at %s.@ Make \
+            sure that either catala is correctly installed,@ or you are \
+            running from the root of a compiled source tree.@]"
+           d)

  let ocaml_link_flags : string list Lazy.t =
    lazy
@ -712,7 +716,7 @@ let gen_build_statements
                reset but that shouldn't cause trouble. *)
             Nj.build "post-test" ~inputs:[reference; test_out]
               ~implicit_in:["always"]
-               ~outputs:[reference ^ "@post"]
+               ~outputs:[(!Var.builddir / reference) ^ "@post"]
          :: acc)
        [] item.legacy_tests
    in
@ -740,7 +744,8 @@ let gen_build_statements
            ~implicit_in:
              ("always"
              :: List.map
-                   (fun test -> legacy_test_reference test ^ "@post")
+                   (fun test ->
+                     (!Var.builddir / legacy_test_reference test) ^ "@post")
                   item.legacy_tests);
          results;
        ]
@ -751,7 +756,8 @@ let gen_build_statements
            ~implicit_out:[srcv ^ "@test"]
            ~inputs:
              (List.map
-                 (fun test -> legacy_test_reference test ^ "@post")
+                 (fun test ->
+                   (!Var.builddir / legacy_test_reference test) ^ "@post")
                 item.legacy_tests);
          results;
        ]
--- a/catala.opam
+++ b/catala.opam
@ -25,7 +25,6 @@ depends: [
  "cppo" {>= "1"}
  "dates_calc" {>= "0.0.4"}
  "dune" {>= "3.11"}
-  "dune-build-info" {>= "3.0"}
  "js_of_ocaml-ppx" {= "4.1.0"}
  "menhir" {>= "20200211"}
  "menhirLib" {>= "20200211"}
@ -75,10 +74,14 @@ build: [
 ]
 dev-repo: "git+https://github.com/CatalaLang/catala.git"
 depexts: [
-  ["groff" "latexmk" "python3-pip" "pandoc"]
+  ["groff"] { with-doc }
+  ["python3-pip" "pandoc"]
+    # "latexmk"
    {cataladevmode & os-family = "debian"}
-  ["groff" "texlive-xetex" "texmf-dist-latexextra" "texmf-dist-pictures" "py3-pip" "py3-pygments" "pandoc-cli"]
+  ["py3-pip" "py3-pygments" "pandoc-cli"]
+    # "texlive-xetex" "texmf-dist-latexextra" "texmf-dist-pictures"
    {cataladevmode & os-distribution = "alpine"}
-  ["groff" "latex-mk" "python-pygments" "pandoc"]
+  ["python-pygments" "pandoc"]
+    # "latex-mk"
    {cataladevmode & os-family = "arch"}
 ]
--- a/compiler/catala_utils/cli.ml
+++ b/compiler/catala_utils/cli.ml
@ -451,10 +451,7 @@ module Flags = struct
 end

 (* Retrieve current version from dune *)
-let version =
-  Option.value ~default:"dev"
-    Build_info.V1.(Option.map Version.to_string (version ()))
-
+let version = Version.v
 let s_plugins = "INSTALLED PLUGINS"

 let info =
--- a/compiler/catala_utils/dune
+++ b/compiler/catala_utils/dune
@ -1,16 +1,24 @@
 (library
 (name catala_utils)
 (public_name catala.catala_utils)
- (libraries
-  unix
-  cmdliner
-  ubase
-  ocolor
-  re
-  bindlib
-  catala.runtime_ocaml
-  dune-build-info))
+ (modules
+  (:standard \ get_version))
+ (libraries unix cmdliner ubase ocolor re bindlib catala.runtime_ocaml))
+
+(executable
+ (name get_version)
+ (modules get_version)
+ (libraries unix))

 (documentation
 (package catala)
 (mld_files catala_utils))
+
+(rule
+ (deps
+  (universe)
+  (env_var CATALA_VERSION))
+ (action
+  (with-stdout-to
+   version.ml
+   (run %{exe:get_version.exe}))))
--- a/compiler/catala_utils/get_version.ml
+++ b/compiler/catala_utils/get_version.ml
@ -0,0 +1,17 @@
+(** This trivial binary is run at build-time to get the correct version from the
+    build environment (either the CATALA_VERSION) environment variable if
+    defined, or `git describe`, or resorting to just "dev" if none of these can
+    be found *)
+
+let v =
+  match Sys.getenv_opt "CATALA_VERSION" with
+  | None | Some "" -> (
+    let ic = Unix.open_process_in "git describe --tags --dirty 2>/dev/null" in
+    let v = try input_line ic with _ -> "dev" in
+    match Unix.close_process_in ic with Unix.WEXITED 0 -> v | _ -> "dev")
+  | Some v -> v
+
+let () =
+  print_string "let v = \"";
+  print_string (String.escaped v);
+  print_endline "\""
--- a/compiler/catala_utils/version.mli
+++ b/compiler/catala_utils/version.mli
@ -0,0 +1,4 @@
+(** The implementation of this module is generated by the build system (through
+    [get_version.ml]), and should only contain a static string *)
+
+val v : string
--- a/compiler/dcalc/invariants.ml
+++ b/compiler/dcalc/invariants.ml
@ -52,7 +52,7 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
        e')
  in
  assert (Bindlib.free_vars p' = Bindlib.empty_ctxt);
-  Message.emit_result "Invariant %s checked.@ result: [%d/%d]" name !ok !total;
+  Message.emit_debug "Invariant %s checked.@ result: [%d/%d]" name !ok !total;
  !result

 (* Structural invariant: no default can have as type A -> B *)
--- a/compiler/desugared/from_surface.ml
+++ b/compiler/desugared/from_surface.ml
@ -226,6 +226,40 @@ let rec translate_expr
  let rec_helper ?(local_vars = local_vars) e =
    translate_expr scope inside_definition_of ctxt local_vars e
  in
+  let rec detuplify_list = function
+    (* Where a list is expected (e.g. after [among]), as syntactic sugar, if a
+       tuple is found instead we transpose it into a list of tuples *)
+    | S.Tuple ls, pos ->
+      let m = Untyped { pos } in
+      let ls = List.map detuplify_list ls in
+      let rec zip = function
+        | [] -> assert false
+        | [l] -> l
+        | l1 :: r ->
+          let rhs = zip r in
+          let rtys, explode =
+            match List.length r with
+            | 1 -> (TAny, pos), fun e -> [e]
+            | size ->
+              ( (TTuple (List.map (fun _ -> TAny, pos) r), pos),
+                fun e ->
+                  List.init size (fun index ->
+                      Expr.etupleaccess ~e ~size ~index m) )
+          in
+          let tys = [TAny, pos; rtys] in
+          let f_join =
+            let x1 = Var.make "x1" and x2 = Var.make "x2" in
+            Expr.make_abs [| x1; x2 |]
+              (Expr.make_tuple (Expr.evar x1 m :: explode (Expr.evar x2 m)) m)
+              tys pos
+          in
+          Expr.eappop ~op:Map2 ~args:[f_join; l1; rhs]
+            ~tys:((TAny, pos) :: List.map (fun ty -> TArray ty, pos) tys)
+            m
+      in
+      zip ls
+    | e -> rec_helper e
+  in
  let pos = Mark.get expr in
  let emark = Untyped { pos } in
  match Mark.remove expr with
@ -498,7 +532,9 @@ let rec translate_expr
    let ctxt = Name_resolution.module_ctx ctxt path in
    let s_uid =
      match Ident.Map.find_opt (Mark.remove s_name) ctxt.local.typedefs with
-      | Some (Name_resolution.TStruct s_uid) -> s_uid
+      | Some (Name_resolution.TStruct s_uid)
+      | Some (Name_resolution.TScope (_, { out_struct_name = s_uid; _ })) ->
+        s_uid
      | _ ->
        Message.raise_spanned_error (Mark.get s_name)
          "This identifier should refer to a struct name"
@ -526,13 +562,22 @@ let rec translate_expr
        StructField.Map.empty fields
    in
    let expected_s_fields = StructName.Map.find s_uid ctxt.structs in
-    StructField.Map.iter
-      (fun expected_f _ ->
-        if not (StructField.Map.mem expected_f s_fields) then
-          Message.raise_spanned_error pos
-            "Missing field for structure %a: \"%a\"" StructName.format s_uid
-            StructField.format expected_f)
-      expected_s_fields;
+    if
+      StructField.Map.exists
+        (fun expected_f _ -> not (StructField.Map.mem expected_f s_fields))
+        expected_s_fields
+    then
+      Message.raise_spanned_error pos "Missing field(s) for structure %a:@\n%a"
+        StructName.format s_uid
+        (Format.pp_print_list
+           ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
+           (fun fmt (expected_f, _) ->
+             Format.fprintf fmt "\"%a\"" StructField.format expected_f))
+        (StructField.Map.bindings
+           (StructField.Map.filter
+              (fun expected_f _ ->
+                not (StructField.Map.mem expected_f s_fields))
+              expected_s_fields));

    Expr.estruct ~name:s_uid ~fields:s_fields emark
  | EnumInject (((path, (constructor, pos_constructor)), _), payload) -> (
@ -618,16 +663,39 @@ let rec translate_expr
  | ArrayLit es -> Expr.earray (List.map rec_helper es) emark
  | Tuple es -> Expr.etuple (List.map rec_helper es) emark
  | CollectionOp (((S.Filter { f } | S.Map { f }) as op), collection) ->
-    let collection = rec_helper collection in
-    let param_name, predicate = f in
-    let param = Var.make (Mark.remove param_name) in
-    let local_vars = Ident.Map.add (Mark.remove param_name) param local_vars in
+    let collection = detuplify_list collection in
+    let param_names, predicate = f in
+    let params = List.map (fun n -> Var.make (Mark.remove n)) param_names in
+    let local_vars =
+      List.fold_left2
+        (fun vars n p -> Ident.Map.add (Mark.remove n) p vars)
+        local_vars param_names params
+    in
    let f_pred =
-      Expr.make_abs [| param |]
+      Expr.make_abs (Array.of_list params)
        (rec_helper ~local_vars predicate)
-        [TAny, pos]
+        (List.map (fun _ -> TAny, pos) params)
        pos
    in
+    let f_pred =
+      (* Detuplification (TODO: check if we couldn't fit this in the general
+         detuplification later) *)
+      match List.length param_names with
+      | 1 -> f_pred
+      | nb_args ->
+        let v =
+          Var.make (String.concat "_" (List.map Mark.remove param_names))
+        in
+        let x = Expr.evar v emark in
+        let tys = List.map (fun _ -> TAny, pos) param_names in
+        Expr.make_abs [| v |]
+          (Expr.make_app f_pred
+             (List.init nb_args (fun i ->
+                  Expr.etupleaccess ~e:x ~index:i ~size:nb_args emark))
+             tys pos)
+          [TAny, pos]
+          pos
+    in
    Expr.eappop
      ~op:
        (match op with
@ -637,49 +705,69 @@ let rec translate_expr
      ~tys:[TAny, pos; TAny, pos]
      ~args:[f_pred; collection] emark
  | CollectionOp
-      ( S.AggregateArgExtremum { max; default; f = param_name, predicate },
+      ( S.AggregateArgExtremum { max; default; f = param_names, predicate },
        collection ) ->
    let default = rec_helper default in
    let pos_dft = Expr.pos default in
-    let collection = rec_helper collection in
-    let param = Var.make (Mark.remove param_name) in
-    let local_vars = Ident.Map.add (Mark.remove param_name) param local_vars in
+    let collection = detuplify_list collection in
+    let params = List.map (fun n -> Var.make (Mark.remove n)) param_names in
+    let local_vars =
+      List.fold_left2
+        (fun vars n p -> Ident.Map.add (Mark.remove n) p vars)
+        local_vars param_names params
+    in
    let cmp_op = if max then Op.Gt else Op.Lt in
    let f_pred =
-      Expr.make_abs [| param |]
+      Expr.make_abs (Array.of_list params)
        (rec_helper ~local_vars predicate)
        [TAny, pos]
        pos
    in
-    let param_name = Bindlib.name_of param in
-    let v1, v2 = Var.make (param_name ^ "_1"), Var.make (param_name ^ "_2") in
-    let x1 = Expr.make_var v1 emark in
-    let x2 = Expr.make_var v2 emark in
+    let add_weight_f =
+      let vs = List.map (fun p -> Var.make (Bindlib.name_of p)) params in
+      let xs = List.map (fun v -> Expr.evar v emark) vs in
+      let x = match xs with [x] -> x | xs -> Expr.etuple xs emark in
+      Expr.make_abs (Array.of_list vs)
+        (Expr.make_tuple [x; Expr.eapp ~f:f_pred ~args:xs ~tys:[] emark] emark)
+        [TAny, pos]
+        pos
+    in
    let reduce_f =
-      (* fun x1 x2 -> cmp_op (pred x1) (pred x2) *)
-      (* Note: this computes f_pred twice on every element, but we'd rather not
-         rely on returning tuples here *)
+      (* fun x1 x2 -> if cmp_op (x1.2) (x2.2) cmp *)
+      let v1, v2 = Var.make "x1", Var.make "x2" in
+      let x1, x2 = Expr.make_var v1 emark, Expr.make_var v2 emark in
      Expr.make_abs [| v1; v2 |]
        (Expr.eifthenelse
           (Expr.eappop ~op:cmp_op
              ~tys:[TAny, pos_dft; TAny, pos_dft]
              ~args:
                [
-                  Expr.eapp ~f:f_pred ~args:[x1] ~tys:[] emark;
-                  Expr.eapp ~f:f_pred ~args:[x2] ~tys:[] emark;
+                  Expr.etupleaccess ~e:x1 ~index:1 ~size:2 emark;
+                  Expr.etupleaccess ~e:x2 ~index:1 ~size:2 emark;
                ]
              emark)
           x1 x2 emark)
        [TAny, pos; TAny, pos]
        pos
    in
-    Expr.eappop ~op:Reduce
-      ~tys:[TAny, pos; TAny, pos; TAny, pos]
-      ~args:[reduce_f; default; collection]
-      emark
+    let weights_var = Var.make "weights" in
+    let default = Expr.make_app add_weight_f [default] [TAny, pos] pos_dft in
+    let weighted_result =
+      Expr.make_let_in weights_var
+        (TArray (TTuple [TAny, pos; TAny, pos], pos), pos)
+        (Expr.eappop ~op:Map
+           ~tys:[TAny, pos; TArray (TAny, pos), pos]
+           ~args:[add_weight_f; collection] emark)
+        (Expr.eappop ~op:Reduce
+           ~tys:[TAny, pos; TAny, pos; TAny, pos]
+           ~args:[reduce_f; default; Expr.evar weights_var emark]
+           emark)
+        pos
+    in
+    Expr.etupleaccess ~e:weighted_result ~index:0 ~size:2 emark
  | CollectionOp
      (((Exists { predicate } | Forall { predicate }) as op), collection) ->
-    let collection = rec_helper collection in
+    let collection = detuplify_list collection in
    let init, op =
      match op with
      | Exists _ -> false, S.Or
@ -687,14 +775,21 @@ let rec translate_expr
      | _ -> assert false
    in
    let init = Expr.elit (LBool init) emark in
-    let param0, predicate = predicate in
-    let param = Var.make (Mark.remove param0) in
-    let local_vars = Ident.Map.add (Mark.remove param0) param local_vars in
+    let params0, predicate = predicate in
+    let params = List.map (fun n -> Var.make (Mark.remove n)) params0 in
+    let local_vars =
+      List.fold_left2
+        (fun vars n p -> Ident.Map.add (Mark.remove n) p vars)
+        local_vars params0 params
+    in
    let f =
      let acc_var = Var.make "acc" in
-      let acc = Expr.make_var acc_var (Untyped { pos = Mark.get param0 }) in
+      let acc =
+        Expr.make_var acc_var (Untyped { pos = Mark.get (List.hd params0) })
+      in
      Expr.eabs
-        (Expr.bind [| acc_var; param |]
+        (Expr.bind
+           (Array.of_list (acc_var :: params))
           (translate_binop (op, pos) pos acc
              (rec_helper ~local_vars predicate)))
        [TAny, pos; TAny, pos]
@ -755,7 +850,7 @@ let rec translate_expr
  | MemCollection (member, collection) ->
    let param_var = Var.make "collection_member" in
    let param = Expr.make_var param_var emark in
-    let collection = rec_helper collection in
+    let collection = detuplify_list collection in
    let init = Expr.elit (LBool false) emark in
    let acc_var = Var.make "acc" in
    let acc = Expr.make_var acc_var emark in
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@ -206,8 +206,9 @@ module Passes = struct
      Message.emit_debug "Checking invariants...";
      match typed with
      | Typed _ ->
-        let result = Dcalc.Invariants.check_all_invariants prg in
-        if not result then
+        if Dcalc.Invariants.check_all_invariants prg then
+          Message.emit_result "All invariant checks passed"
+        else
          raise
            (Message.raise_internal_error "Some Dcalc invariants are invalid")
      | _ ->
@ -562,9 +563,10 @@ module Commands = struct
          (Program.untype prg)
      in
      Message.emit_debug "Checking invariants...";
-      let result = Dcalc.Invariants.check_all_invariants prg in
-      if not result then
-        raise (Message.raise_internal_error "Some Dcalc invariants are invalid"));
+        if Dcalc.Invariants.check_all_invariants prg then
+          Message.emit_result "All invariant checks passed"
+        else
+          raise (Message.raise_internal_error "Some Dcalc invariants are invalid"));
    Message.emit_result "Typechecking successful!"

  let typecheck_cmd =
--- a/compiler/dune
+++ b/compiler/dune
@ -17,8 +17,6 @@
 (executable
 (name catala_web_interpreter)
 (modes byte js)
- (package catala)
- (public_name catala_web_interpreter)
 (modules catala_web_interpreter)
 (preprocess
  (pps js_of_ocaml-ppx))
@ -28,11 +26,23 @@
  catala.runtime_ocaml
  catala.runtime_jsoo))

+(install
+ (section bin)
+ (package catala)
+ (files
+  (catala_web_interpreter.bc.js as catala_web_interpreter.js)))
+
 (executable
 (name tests)
 (modules tests)
 (libraries catala.driver alcotest))

+(install
+ (section bin)
+ (package catala)
+ (files
+  (catala.bc.js as catala.js)))
+
 (rule
 (target custom_linking.sexp)
 (mode fallback)
--- a/compiler/scalc/to_python.ml
+++ b/compiler/scalc/to_python.ml
@ -84,6 +84,7 @@ let format_op (fmt : Format.formatter) (op : operator Mark.pos) : unit =
  | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ->
    Format.pp_print_string fmt "=="
  | Map -> Format.pp_print_string fmt "list_map"
+  | Map2 -> Format.pp_print_string fmt "list_map2"
  | Reduce -> Format.pp_print_string fmt "list_reduce"
  | Filter -> Format.pp_print_string fmt "list_filter"
  | Fold -> Format.pp_print_string fmt "list_fold_left"
--- a/compiler/scalc/to_r.ml
+++ b/compiler/scalc/to_r.ml
@ -99,6 +99,7 @@ let format_op (fmt : Format.formatter) (op : operator Mark.pos) : unit =
  | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ->
    Format.pp_print_string fmt "=="
  | Map -> Format.pp_print_string fmt "catala_list_map"
+  | Map2 -> Format.pp_print_string fmt "catala_list_map2"
  | Reduce -> Format.pp_print_string fmt "catala_list_reduce"
  | Filter -> Format.pp_print_string fmt "catala_list_filter"
  | Fold -> Format.pp_print_string fmt "catala_list_fold_left"
--- a/compiler/shared_ast/definitions.ml
+++ b/compiler/shared_ast/definitions.ml
@ -314,6 +314,7 @@ module Op = struct
    (* * polymorphic *)
    | Eq : < polymorphic ; .. > t
    | Map : < polymorphic ; .. > t
+    | Map2 : < polymorphic ; .. > t
    | Concat : < polymorphic ; .. > t
    | Filter : < polymorphic ; .. > t
    (* * overloaded *)
--- a/compiler/shared_ast/interpreter.ml
+++ b/compiler/shared_ast/interpreter.ml
@ -198,6 +198,22 @@ let rec evaluate_operator
             (Mark.copy e'
                (EApp { f; args = [e']; tys = [Expr.maybe_ty (Mark.get e')] })))
         es)
+  | Map2, [f; (EArray es1, _); (EArray es2, _)] ->
+    EArray
+      (List.map2
+         (fun e1 e2 ->
+           evaluate_expr
+             (Mark.add m
+                (EApp
+                   {
+                     f;
+                     args = [e1; e2];
+                     tys =
+                       [
+                         Expr.maybe_ty (Mark.get e1); Expr.maybe_ty (Mark.get e2);
+                       ];
+                   })))
+         es1 es2)
  | Reduce, [_; default; (EArray [], _)] -> Mark.remove default
  | Reduce, [f; _; (EArray (x0 :: xn), _)] ->
    Mark.remove
@ -249,7 +265,8 @@ let rec evaluate_operator
                       ];
                   })))
         init es)
-  | (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ -> err ()
+  | (Length | Log _ | Eq | Map | Map2 | Concat | Filter | Fold | Reduce), _ ->
+    err ()
  | Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b))
  | GetDay, [(ELit (LDate d), _)] -> ELit (LInt (o_getDay d))
  | GetMonth, [(ELit (LDate d), _)] -> ELit (LInt (o_getMonth d))
--- a/compiler/shared_ast/operator.ml
+++ b/compiler/shared_ast/operator.ml
@ -45,6 +45,7 @@ let name : type a. a t -> string = function
  | Xor -> "o_xor"
  | Eq -> "o_eq"
  | Map -> "o_map"
+  | Map2 -> "o_map2"
  | Concat -> "o_concat"
  | Filter -> "o_filter"
  | Reduce -> "o_reduce"
@ -174,6 +175,7 @@ let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
  | Xor, Xor
  | Eq, Eq
  | Map, Map
+  | Map2, Map2
  | Concat, Concat
  | Filter, Filter
  | Reduce, Reduce
@ -259,6 +261,7 @@ let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
  | Xor, _ -> -1 | _, Xor -> 1
  | Eq, _ -> -1 | _, Eq -> 1
  | Map, _ -> -1 | _, Map -> 1
+  | Map2, _ -> -1 | _, Map2 -> 1
  | Concat, _ -> -1 | _, Concat -> 1
  | Filter, _ -> -1 | _, Filter -> 1
  | Reduce, _ -> -1 | _, Reduce -> 1
@ -339,7 +342,7 @@ let kind_dispatch :
  | ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | And
    | Or | Xor ) as op ->
    monomorphic op
-  | ( Log _ | Length | Eq | Map | Concat | Filter | Reduce | Fold
+  | ( Log _ | Length | Eq | Map | Map2 | Concat | Filter | Reduce | Fold
    | HandleDefault | HandleDefaultOpt | FromClosureEnv | ToClosureEnv ) as op
    ->
    polymorphic op
@ -372,7 +375,7 @@ let translate (t : 'a no_overloads t) : 'b no_overloads t =
  match t with
  | ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | And
    | Or | Xor | HandleDefault | HandleDefaultOpt | Log _ | Length | Eq | Map
-    | Concat | Filter | Reduce | Fold | Minus_int | Minus_rat | Minus_mon
+    | Map2 | Concat | Filter | Reduce | Fold | Minus_int | Minus_rat | Minus_mon
    | Minus_dur | ToRat_int | ToRat_mon | ToMoney_rat | Round_rat | Round_mon
    | Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur
    | Sub_int_int | Sub_rat_rat | Sub_mon_mon | Sub_dat_dat | Sub_dat_dur
--- a/compiler/shared_ast/optimizations.ml
+++ b/compiler/shared_ast/optimizations.ml
@ -302,12 +302,12 @@ let test_iota_reduction_1 () =
  let matchA = Expr.ematch ~e:injA ~name:enumT ~cases nomark in
  Alcotest.(check string)
    "same string"
-    "before=match (A x)\n\
-    \       with\n\
-    \       | A → (λ (x: any) → C x)\n\
-    \       | B → (λ (x: any) → D x)\n\
-     after=C\n\
-     x"
+    begin[@ocamlformat "disable"]
+      "before=match (A x) with\n\
+      \       | A x → C x\n\
+      \       | B x → D x\n\
+       after=C x"
+    end
    (Format.asprintf "before=%a\nafter=%a" Expr.format (Expr.unbox matchA)
       Expr.format
       (Expr.unbox (optimize_expr Program.empty_ctx (Expr.unbox matchA))))
@ -360,18 +360,16 @@ let test_iota_reduction_2 () =
  in
  Alcotest.(check string)
    "same string "
-    "before=match\n\
-    \         (match 1\n\
-    \          with\n\
-    \          | A → (λ (x: any) → A 20)\n\
-    \          | B → (λ (x: any) → B B x))\n\
-    \       with\n\
-    \       | A → (λ (x: any) → C x)\n\
-    \       | B → (λ (x: any) → D x)\n\
-     after=match 1\n\
-    \      with\n\
-    \      | A → (λ (x: any) → C 20)\n\
-    \      | B → (λ (x: any) → D B x)\n"
+    begin[@ocamlformat "disable"]
+      "before=match (match 1 with\n\
+      \              | A x → A 20\n\
+      \              | B x → B (B x)) with\n\
+      \       | A x → C x\n\
+      \       | B x → D x\n\
+       after=match 1 with\n\
+      \      | A x → C 20\n\
+      \      | B x → D B x"
+    end
    (Format.asprintf "before=@[%a@]@.after=%a@." Expr.format (Expr.unbox matchA)
       Expr.format
       (Expr.unbox (optimize_expr Program.empty_ctx (Expr.unbox matchA))))
--- a/compiler/shared_ast/print.ml
+++ b/compiler/shared_ast/print.ml
@ -222,6 +222,7 @@ let operator_to_string : type a. a Op.t -> string =
  | Xor -> "xor"
  | Eq -> "="
  | Map -> "map"
+  | Map2 -> "map2"
  | Reduce -> "reduce"
  | Concat -> "++"
  | Filter -> "filter"
@ -306,6 +307,7 @@ let operator_to_shorter_string : type a. a Op.t -> string =
  | Xor -> "xor"
  | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dur_dur | Eq_dat_dat | Eq -> "="
  | Map -> "map"
+  | Map2 -> "map2"
  | Reduce -> "reduce"
  | Concat -> "++"
  | Filter -> "filter"
@ -407,8 +409,8 @@ module Precedence = struct
      | Div | Div_int_int | Div_rat_rat | Div_mon_rat | Div_mon_mon
      | Div_dur_dur ->
        Op Div
-      | HandleDefault | HandleDefaultOpt | Map | Concat | Filter | Reduce | Fold
-      | ToClosureEnv | FromClosureEnv ->
+      | HandleDefault | HandleDefaultOpt | Map | Map2 | Concat | Filter | Reduce
+      | Fold | ToClosureEnv | FromClosureEnv ->
        App)
    | EApp _ -> App
    | EArray _ -> Contained
@ -1092,12 +1094,18 @@ module UserFacing = struct
       ppf e ->
    match Mark.remove e with
    | ELit l -> lit lang ppf l
-    | EArray l | ETuple l ->
+    | EArray l ->
      Format.fprintf ppf "@[<hv 2>[@,@[<hov>%a@]@;<0 -2>]@]"
        (Format.pp_print_list
           ~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ")
           (value ~fallback lang))
        l
+    | ETuple l ->
+      Format.fprintf ppf "@[<hv 2>(@,@[<hov>%a@]@;<0 -2>)@]"
+        (Format.pp_print_list
+           ~pp_sep:(fun ppf () -> Format.fprintf ppf ",@ ")
+           (value ~fallback lang))
+        l
    | EStruct { name; fields } ->
      Format.fprintf ppf "@[<hv 2>%a {@ %a@;<1 -2>}@]" StructName.format name
        (StructField.Map.format_bindings ~pp_sep:Format.pp_print_space
--- a/compiler/shared_ast/typing.ml
+++ b/compiler/shared_ast/typing.ml
@ -291,6 +291,7 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
  let pos = Mark.get op in
  let any = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in
  let any2 = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in
+  let any3 = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in
  let bt = lazy (UnionFind.make (TLit TBool, pos)) in
  let ut = lazy (UnionFind.make (TLit TUnit, pos)) in
  let it = lazy (UnionFind.make (TLit TInt, pos)) in
@ -304,6 +305,7 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
    | Fold -> [[any2; any] @-> any2; any2; array any] @-> any2
    | Eq -> [any; any] @-> bt
    | Map -> [[any] @-> any2; array any] @-> array any2
+    | Map2 -> [[any; any2] @-> any3; array any; array any2] @-> array any3
    | Filter -> [[any] @-> bt; array any] @-> array any
    | Reduce -> [[any; any] @-> any; any; array any] @-> any
    | Concat -> [array any; array any] @-> array any
@ -755,9 +757,9 @@ and typecheck_expr_top_down :
  | A.EAbs { binder; tys = t_args } ->
    if Bindlib.mbinder_arity binder <> List.length t_args then
      Message.raise_spanned_error (Expr.pos e)
-        "function has %d variables but was supplied %d types"
+        "function has %d variables but was supplied %d types\n%a"
        (Bindlib.mbinder_arity binder)
-        (List.length t_args)
+        (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
--- a/compiler/surface/ast.ml
+++ b/compiler/surface/ast.ml
@ -145,10 +145,10 @@ and literal =
  | LDate of literal_date

 and collection_op =
-  | Exists of { predicate : lident Mark.pos * expression }
-  | Forall of { predicate : lident Mark.pos * expression }
-  | Map of { f : lident Mark.pos * expression }
-  | Filter of { f : lident Mark.pos * expression }
+  | Exists of { predicate : lident Mark.pos list * expression }
+  | Forall of { predicate : lident Mark.pos list * expression }
+  | Map of { f : lident Mark.pos list * expression }
+  | Filter of { f : lident Mark.pos list * expression }
  | AggregateSum of { typ : primitive_typ }
  (* it would be nice to remove the need for specifying the and here like for
     extremums, but we need an additionl overload for "neutral element for
@ -157,7 +157,7 @@ and collection_op =
  | AggregateArgExtremum of {
      max : bool;
      default : expression;
-      f : lident Mark.pos * expression;
+      f : lident Mark.pos list * expression;
    }

 and explicit_match_case = {
--- a/compiler/surface/parser.mly
+++ b/compiler/surface/parser.mly
@ -157,6 +157,10 @@ let qlident :=
 }
 | id = lident ; { [], id }

+let mbinder ==
+| id = lident ; { [id] }
+| LPAREN ; ids = separated_nonempty_list(COMMA,lident) ; RPAREN ; <>
+
 let expression :=
 | e = addpos(naked_expression) ; <>

@ -216,7 +220,7 @@ let naked_expression ==
  CollectionOp (AggregateSum { typ = Mark.remove typ }, coll)
 } %prec apply
 | f = expression ;
-  FOR ; i = lident ;
+  FOR ; i = mbinder ;
  AMONG ; coll = expression ; {
  CollectionOp (Map {f = i, f}, coll)
 } %prec apply
@ -234,12 +238,12 @@ let naked_expression ==
  e2 = expression ; {
  Binop (binop, e1, e2)
 }
-| EXISTS ; i = lident ;
+| EXISTS ; i = mbinder ;
  AMONG ; coll = expression ;
  SUCH ; THAT ; predicate = expression ; {
  CollectionOp (Exists {predicate = i, predicate}, coll)
 } %prec let_expr
-| FOR ; ALL ; i = lident ;
+| FOR ; ALL ; i = mbinder ;
  AMONG ; coll = expression ;
  WE_HAVE ; predicate = expression ; {
  CollectionOp (Forall {predicate = i, predicate}, coll)
@ -254,28 +258,28 @@ let naked_expression ==
  ELSE ; e3 = expression ; {
  IfThenElse (e1, e2, e3)
 } %prec let_expr
-| LET ; ids = separated_nonempty_list(COMMA,lident) ;
+| LET ; ids = mbinder ;
  DEFINED_AS ; e1 = expression ;
  IN ; e2 = expression ; {
  LetIn (ids, e1, e2)
 } %prec let_expr
-| i = lident ;
+| i = lident ; (* FIXME: should be mbinder *)
  AMONG ; coll = expression ;
  SUCH ; THAT ; f = expression ; {
-  CollectionOp (Filter {f = i, f}, coll)
+  CollectionOp (Filter {f = [i], f}, coll)
 } %prec top_expr
 | fmap = expression ;
-  FOR ; i = lident ;
+  FOR ; i = mbinder ;
  AMONG ; coll = expression ;
  SUCH ; THAT ; ffilt = expression ; {
  CollectionOp (Map {f = i, fmap}, (CollectionOp (Filter {f = i, ffilt}, coll), Pos.from_lpos $loc))
 } %prec top_expr
-| i = lident ;
+| i = lident ; (* FIXME: should be mbinder *)
  AMONG ; coll = expression ;
  SUCH ; THAT ; f = expression ;
  IS ; max = minmax ;
  OR ; IF ; LIST_EMPTY ; THEN ; default = expression ; {
-  CollectionOp (AggregateArgExtremum { max; default; f = i, f }, coll)
+  CollectionOp (AggregateArgExtremum { max; default; f = [i], f }, coll)
 } %prec top_expr


--- a/compiler/tests.ml
+++ b/compiler/tests.ml
@ -5,6 +5,7 @@ let () =
      ( "Iota-reduction",
        [
          test_case "#1" `Quick Shared_ast.Optimizations.test_iota_reduction_1;
-          test_case "#2" `Quick Shared_ast.Optimizations.test_iota_reduction_2;
+          (* test_case "#2" `Quick
+             Shared_ast.Optimizations.test_iota_reduction_2; FIXME *)
        ] );
    ]
--- a/24
+++ b/24
@ -2,7 +2,9 @@

 (data_only_dirs tests syntax_highlighting)

-(copy_files compiler/surface/grammar.html)
+(copy_files
+ (alias doc)
+ (files compiler/surface/grammar.html))

 ; Override dune default warnings with sane settings

@ -10,7 +12,7 @@
 ; don't stop building because of warnings
 (dev
  (flags
-   (:standard -warn-error -a -w -67)))
+   (:standard -warn-error -a+8 -w -67)))
 ; for CI runs: must fail on warnings
 (check
  (flags
@ -29,6 +31,7 @@
    -a))))

 (rule
+ (alias doc)
 (action
  (with-stdout-to
   catala.html
@ -37,6 +40,7 @@
    (run groff -P -l -P -r -mandoc -Thtml)))))

 (rule
+ (alias doc)
 (action
  (with-stdout-to
   clerk.html
@ -48,10 +52,12 @@
 (name exec)
 (deps compiler/catala.exe build_system/clerk.exe))

-(rule
- (alias runtest)
- (package catala)
- (deps
-  (source_tree tests))
- (action
-  (run clerk --exe %{bin:catala} test tests)))
+;; This garbles Clerk output, prefer to run from Makefile
+;; (rule
+;;  (alias runtest)
+;;  (package catala)
+;;  (deps
+;;   (source_tree tests)
+;;   (alias install))
+;;  (action
+;;   (run %{bin:clerk} test --exe %{bin:catala} tests)))
--- a/runtimes/ocaml/runtime.ml
+++ b/runtimes/ocaml/runtime.ml
@ -50,6 +50,7 @@ exception UncomparableDurations
 exception IndivisibleDurations
 exception ImpossibleDate
 exception NoValueProvided of source_position
+exception NotSameLength

 (* TODO: register exception printers for the above
   (Printexc.register_printer) *)
@ -661,6 +662,9 @@ module Oper = struct
  let o_eq = ( = )
  let o_map = Array.map

+  let o_map2 f a b =
+    try Array.map2 f a b with Invalid_argument _ -> raise NotSameLength
+
  let o_reduce f dft a =
    let len = Array.length a in
    if len = 0 then dft
--- a/runtimes/ocaml/runtime.mli
+++ b/runtimes/ocaml/runtime.mli
@ -353,6 +353,7 @@ module Oper : sig
  val o_xor : bool -> bool -> bool
  val o_eq : 'a -> 'a -> bool
  val o_map : ('a -> 'b) -> 'a array -> 'b array
+  val o_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
  val o_reduce : ('a -> 'a -> 'a) -> 'a -> 'a array -> 'a
  val o_concat : 'a array -> 'a array -> 'a array
  val o_filter : ('a -> bool) -> 'a array -> 'a array
--- a/runtimes/python/src/catala/py.typed
+++ b/runtimes/python/src/catala/py.typed
--- a/runtimes/python/src/catala/runtime.py
+++ b/runtimes/python/src/catala/runtime.py
@ -571,6 +571,8 @@ def list_filter(f: Callable[[Alpha], bool], l: List[Alpha]) -> List[Alpha]:
 def list_map(f: Callable[[Alpha], Beta], l: List[Alpha]) -> List[Beta]:
    return [f(i) for i in l]

+def list_map2(f: Callable[[Alpha, Beta], Gamma], l1: List[Alpha], l2: List[Beta]) -> List[Gamma]:
+    return [f(i, j) for i, j in zip(l1, l2, strict=True)]

 def list_reduce(f: Callable[[Alpha, Alpha], Alpha], dft: Alpha, l: List[Alpha]) -> Alpha:
    if l == []:
--- a/runtimes/r/R/runtime.R
+++ b/runtimes/r/R/runtime.R
@ -285,6 +285,10 @@ catala_list_map <- function(f, l) {
  Map(f, l)
 }
 #' @export
+catala_list_map2 <- function(f, l1, l2) {
+  Map(f, l1, l2)
+}
+#' @export
 catala_list_reduce <- function(f, default, l) {
  if (length(l) == 0) {
    default
--- a/tests/Makefile
+++ b/tests/Makefile
@ -5,20 +5,18 @@
 CATALA_OPTS?=
 CLERK_OPTS?=--makeflags="$(MAKEFLAGS)"

-CLERK=_build/default/build_system/clerk.exe test --exe "_build/default/compiler/catala.exe" \
+CLERK=dune exec -- ../build_system/clerk.exe test \
 	$(CLERK_OPTS) $(if $(CATALA_OPTS),--catala-opts=$(CATALA_OPTS),)

 # Forces all the tests to be redone
 .FORCE:

 %.catala_en %.catala_fr %.catala_pl: .FORCE
-    # Here we cd to the root of the Catala repository such that the paths \
-	# displayed in error messages start with `tests/` uniformly.
-	@cd ..; $(CLERK) tests/$@
+	$(CLERK) $@

 pass_all_tests:
-	@cd ..; $(CLERK) tests
+	$(CLERK) .

 reset_all_tests: CLERK_OPTS+=--reset
 reset_all_tests:
-	@cd ..; $(CLERK) tests
+	$(CLERK) .
--- a/tests/test_arithmetic/good/priorities.catala_en
+++ b/tests/test_arithmetic/good/priorities.catala_en
@ -16,12 +16,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [62/62]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [8/8]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_arithmetic/good/trivial.catala_en
+++ b/tests/test_arithmetic/good/trivial.catala_en
@ -10,12 +10,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [14/14]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [2/2]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/aggregation.catala_en
+++ b/tests/test_array/good/aggregation.catala_en
@ -27,12 +27,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [104/104]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [7/7]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [10/10]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/aggregation_2.catala_en
+++ b/tests/test_array/good/aggregation_2.catala_en
@ -33,12 +33,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [105/105]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [6/6]
-[RESULT] Invariant no_return_a_function checked. result: [7/7]
-[RESULT] Invariant no_partial_evaluation checked. result: [6/6]
-[RESULT] Invariant default_no_arrow checked. result: [7/7]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/aggregation_3.catala_en
+++ b/tests/test_array/good/aggregation_3.catala_en
@ -35,12 +35,7 @@ scope S:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [181/181]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [14/14]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [2/2]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

@ -77,18 +72,19 @@ let scope S (x: integer|internal|output) =
            10.
            map (λ (i: integer) → to_rat i) [1; 2; 3])
         = 3.;
-  assert (reduce
-            (λ (i_1: integer) (i_2: integer) →
-             if
-               (let i : integer = i_1 in
-                to_rat ((2 - i) * (2 - i)))
-               < let i : integer = i_2 in
-                 to_rat ((2 - i) * (2 - i))
-             then
-               i_1
-             else i_2)
-            42
-            [1; 2; 3])
+  assert (let weights : list of (integer * decimal) =
+            map (λ (i: integer) →
+                 (i, let i1 : integer = i in
+                     to_rat ((2 - i1) * (2 - i1))))
+              [1; 2; 3]
+          in
+          reduce
+            (λ (x1: (integer * decimal)) (x2: (integer * decimal)) →
+             if x1.1 < x2.1 then x1 else x2)
+            let i : integer = 42 in
+            (i, let i1 : integer = i in
+                to_rat ((2 - i1) * (2 - i1)))
+            weights).0
         = 2
 ```

--- a/tests/test_array/good/concatenation.catala_en
+++ b/tests/test_array/good/concatenation.catala_en
@ -14,12 +14,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [36/36]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/filter.catala_en
+++ b/tests/test_array/good/filter.catala_en
@ -20,12 +20,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [37/37]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/filter_map.catala_en
+++ b/tests/test_array/good/filter_map.catala_en
@ -21,12 +21,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [51/51]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [2/2]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/fold.catala_en
+++ b/tests/test_array/good/fold.catala_en
@ -33,12 +33,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [105/105]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [6/6]
-[RESULT] Invariant no_return_a_function checked. result: [7/7]
-[RESULT] Invariant no_partial_evaluation checked. result: [6/6]
-[RESULT] Invariant default_no_arrow checked. result: [7/7]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/map.catala_en
+++ b/tests/test_array/good/map.catala_en
@ -14,12 +14,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [26/26]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/simple.catala_en
+++ b/tests/test_array/good/simple.catala_en
@ -25,12 +25,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [84/84]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [3/3]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [10/10]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/simpler.catala_en
+++ b/tests/test_array/good/simpler.catala_en
@ -14,12 +14,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [34/34]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_array/good/simplest.catala_en
+++ b/tests/test_array/good/simplest.catala_en
@ -12,12 +12,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [13/13]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [2/2]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_bool/good/test_bool.catala_en
+++ b/tests/test_bool/good/test_bool.catala_en
@ -15,12 +15,7 @@ scope TestBool:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [45/45]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [7/7]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_bool/good/test_precedence.catala_en
+++ b/tests/test_bool/good/test_precedence.catala_en
@ -12,12 +12,7 @@ scope TestBool:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [26/26]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [3/3]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_bool/good/test_xor.catala_en
+++ b/tests/test_bool/good/test_xor.catala_en
@ -18,12 +18,7 @@ scope TestXor:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [81/81]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [4/4]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [4/4]
-[RESULT] Invariant default_no_arrow checked. result: [12/12]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_date/good/durations.catala_en
+++ b/tests/test_date/good/durations.catala_en
@ -27,12 +27,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [78/78]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [14/14]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_date/good/rounding_option_en.catala_en
+++ b/tests/test_date/good/rounding_option_en.catala_en
@ -26,12 +26,7 @@ scope Test:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [49/49]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [3/3]
-[RESULT] Invariant no_return_a_function checked. result: [2/2]
-[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_date/good/rounding_option_fr.catala_fr
+++ b/tests/test_date/good/rounding_option_fr.catala_fr
@ -26,12 +26,7 @@ champ d'application Test:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [49/49]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [3/3]
-[RESULT] Invariant no_return_a_function checked. result: [2/2]
-[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_date/good/simple.catala_en
+++ b/tests/test_date/good/simple.catala_en
@ -16,12 +16,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [57/57]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [3/3]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
-[RESULT] Invariant default_no_arrow checked. result: [9/9]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_dec/good/infinite_precision.catala_en
+++ b/tests/test_dec/good/infinite_precision.catala_en
@ -18,12 +18,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [88/88]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [4/4]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [4/4]
-[RESULT] Invariant default_no_arrow checked. result: [12/12]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_dec/good/rounding.catala_en
+++ b/tests/test_dec/good/rounding.catala_en
@ -18,12 +18,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [39/39]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [8/8]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_dec/good/simple.catala_en
+++ b/tests/test_dec/good/simple.catala_en
@ -18,12 +18,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [68/68]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [3/3]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
-[RESULT] Invariant default_no_arrow checked. result: [11/11]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_dec/good/zero_after_comma.catala_en
+++ b/tests/test_dec/good/zero_after_comma.catala_en
@ -15,12 +15,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [45/45]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_default/good/mutliple_definitions.catala_en
+++ b/tests/test_default/good/mutliple_definitions.catala_en
@ -24,12 +24,7 @@ $ catala Typecheck --check-invariants
 └─┐
 6 │   definition w equals 3
  │   ‾‾‾‾‾‾‾‾‾‾‾‾
-[RESULT] Invariant typing_defaults checked. result: [14/14]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [3/3]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_enum/good/disambiguated_cases.catala_en
+++ b/tests/test_enum/good/disambiguated_cases.catala_en
@ -25,12 +25,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [62/62]
-[RESULT] Invariant match_inversion checked. result: [1/1]
-[RESULT] Invariant app_inversion checked. result: [3/3]
-[RESULT] Invariant no_return_a_function checked. result: [2/2]
-[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
-[RESULT] Invariant default_no_arrow checked. result: [9/9]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_enum/good/quick_pattern_check.catala_en
+++ b/tests/test_enum/good/quick_pattern_check.catala_en
@ -20,12 +20,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [66/66]
-[RESULT] Invariant match_inversion checked. result: [2/2]
-[RESULT] Invariant app_inversion checked. result: [3/3]
-[RESULT] Invariant no_return_a_function checked. result: [4/4]
-[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
-[RESULT] Invariant default_no_arrow checked. result: [9/9]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_enum/good/simple.catala_en
+++ b/tests/test_enum/good/simple.catala_en
@ -20,12 +20,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [43/43]
-[RESULT] Invariant match_inversion checked. result: [1/1]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [2/2]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_enum/good/wildcard.catala_en
+++ b/tests/test_enum/good/wildcard.catala_en
@ -40,12 +40,7 @@ scope Simple_case_2:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [90/90]
-[RESULT] Invariant match_inversion checked. result: [2/2]
-[RESULT] Invariant app_inversion checked. result: [4/4]
-[RESULT] Invariant no_return_a_function checked. result: [6/6]
-[RESULT] Invariant no_partial_evaluation checked. result: [4/4]
-[RESULT] Invariant default_no_arrow checked. result: [12/12]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/context_with_default.catala_en
+++ b/tests/test_exception/good/context_with_default.catala_en
@ -19,12 +19,7 @@ scope Bar:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [47/47]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [8/8]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/double_definition.catala_en
+++ b/tests/test_exception/good/double_definition.catala_en
@ -27,12 +27,7 @@ $ catala Typecheck --check-invariants
 8 │   definition x equals 1
  │   ‾‾‾‾‾‾‾‾‾‾‾‾
  └─ Foo
-[RESULT] Invariant typing_defaults checked. result: [14/14]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [3/3]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/duplicate_labels.catala_en
+++ b/tests/test_exception/good/duplicate_labels.catala_en
@ -22,12 +22,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [56/56]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [10/10]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/exception.catala_en
+++ b/tests/test_exception/good/exception.catala_en
@ -16,12 +16,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [28/28]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/exceptions_squared.catala_en
+++ b/tests/test_exception/good/exceptions_squared.catala_en
@ -20,12 +20,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [37/37]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [9/9]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/grouped_exceptions.catala_en
+++ b/tests/test_exception/good/grouped_exceptions.catala_en
@ -50,12 +50,7 @@ scope Benefit:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [59/59]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [10/10]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/groups_of_exceptions.catala_en
+++ b/tests/test_exception/good/groups_of_exceptions.catala_en
@ -44,12 +44,7 @@ scope Test:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [78/78]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [15/15]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/same_label_two_variables.catala_en
+++ b/tests/test_exception/good/same_label_two_variables.catala_en
@ -23,12 +23,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [66/66]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [3/3]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
-[RESULT] Invariant default_no_arrow checked. result: [12/12]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/split_unlabeled_exception.catala_en
+++ b/tests/test_exception/good/split_unlabeled_exception.catala_en
@ -18,12 +18,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [28/28]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/two_exceptions_same_outcome.catala_en
+++ b/tests/test_exception/good/two_exceptions_same_outcome.catala_en
@ -24,12 +24,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [43/43]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [10/10]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/two_unlabeled_exceptions.catala_en
+++ b/tests/test_exception/good/two_unlabeled_exceptions.catala_en
@ -21,12 +21,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [55/55]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [12/12]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/unlabeled_exception.catala_en
+++ b/tests/test_exception/good/unlabeled_exception.catala_en
@ -15,12 +15,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [28/28]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en
+++ b/tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en
@ -21,12 +21,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [55/55]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [12/12]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_func/good/closure_conversion.catala_en
+++ b/tests/test_func/good/closure_conversion.catala_en
@ -15,12 +15,7 @@ scope S:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [27/27]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_func/good/closure_conversion_reduce.catala_en
+++ b/tests/test_func/good/closure_conversion_reduce.catala_en
@ -15,12 +15,7 @@ scope S:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [27/27]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [3/3]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [2/2]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

@ -29,12 +24,12 @@ $ catala Lcalc -s S --avoid-exceptions -O --closure-conversion
 let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
  let get x : list of integer = S_in.x_in in
  let set y : integer =
-    reduce
-      (λ (potential_max_1: integer) (potential_max_2: integer) →
-       if potential_max_1 < potential_max_2 then potential_max_1
-       else potential_max_2)
-      -1
-      x
+    (reduce
+       (λ (x1: (integer * integer)) (x2: (integer * integer)) →
+        if x1.1 < x2.1 then x1 else x2)
+       let potential_max : integer = -1 in
+       (potential_max, potential_max)
+       map (λ (potential_max: integer) → (potential_max, potential_max)) x).0
  in
  return { S y = y; }
 ```
@ -62,18 +57,21 @@ let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
             (λ (_: unit) → true)
             (λ (_: unit) →
              ESome
-                (reduce
-                   (λ (potential_max_1: integer) (potential_max_2: integer) →
-                    if
-                      (let potential_max : integer = potential_max_1 in
-                       potential_max)
-                      < let potential_max : integer = potential_max_2 in
-                        potential_max
-                    then
-                      potential_max_1
-                    else potential_max_2)
-                   -1
-                   x))
+                (let weights : list of (integer * integer) =
+                   map (λ (potential_max: integer) →
+                        (potential_max,
+                          let potential_max1 : integer = potential_max in
+                          potential_max1))
+                     x
+                 in
+                 reduce
+                   (λ (x1: (integer * integer)) (x2: (integer * integer)) →
+                    if x1.1 < x2.1 then x1 else x2)
+                   let potential_max : integer = -1 in
+                   (potential_max,
+                     let potential_max1 : integer = potential_max in
+                     potential_max1)
+                   weights).0)
         ]
         (λ (_: unit) → false)
         (λ (_: unit) → ENone ()))
--- a/tests/test_func/good/closure_return.catala_en
+++ b/tests/test_func/good/closure_return.catala_en
@ -13,12 +13,7 @@ scope S:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [17/17]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [2/2]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_func/good/closure_through_scope.catala_en
+++ b/tests/test_func/good/closure_through_scope.catala_en
@ -21,12 +21,7 @@ scope T:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [43/43]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_func/good/context_func.catala_en
+++ b/tests/test_func/good/context_func.catala_en
@ -19,12 +19,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [45/45]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [2/2]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [5/5]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_func/good/func.catala_en
+++ b/tests/test_func/good/func.catala_en
@ -25,12 +25,7 @@ scope R:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [110/110]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [6/6]
-[RESULT] Invariant no_return_a_function checked. result: [4/4]
-[RESULT] Invariant no_partial_evaluation checked. result: [6/6]
-[RESULT] Invariant default_no_arrow checked. result: [15/15]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_func/good/param_consistency.catala_en
+++ b/tests/test_func/good/param_consistency.catala_en
@ -16,12 +16,7 @@ scope S:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [33/33]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [5/5]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_func/good/scope_call_func_struct_closure.catala_en
+++ b/tests/test_func/good/scope_call_func_struct_closure.catala_en
@ -44,12 +44,7 @@ two closures in Foo.r are different even with optimizations enabled.

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [130/130]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [12/12]
-[RESULT] Invariant no_return_a_function checked. result: [10/10]
-[RESULT] Invariant no_partial_evaluation checked. result: [12/12]
-[RESULT] Invariant default_no_arrow checked. result: [11/11]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_io/good/all_io.catala_en
+++ b/tests/test_io/good/all_io.catala_en
@ -21,12 +21,7 @@ scope A:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [68/68]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [10/10]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_io/good/condition_only_input.catala_en
+++ b/tests/test_io/good/condition_only_input.catala_en
@ -18,12 +18,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [34/34]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_io/good/subscope.catala_en
+++ b/tests/test_io/good/subscope.catala_en
@ -24,12 +24,7 @@ scope B:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [63/63]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [9/9]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_literate/good/test_grave_char_en.catala_en
+++ b/tests/test_literate/good/test_grave_char_en.catala_en
@ -31,12 +31,7 @@ int main(void) { return 0; }

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [19/19]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [3/3]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_literate/good/test_grave_char_fr.catala_fr
+++ b/tests/test_literate/good/test_grave_char_fr.catala_fr
@ -31,12 +31,7 @@ int main(void) { return 0; }

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [19/19]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [3/3]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_metadata/good/test_markup_refactoring.catala_en
+++ b/tests/test_metadata/good/test_markup_refactoring.catala_en
@ -32,12 +32,7 @@ scope S2:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [40/40]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [6/6]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/mod_def.catala_en
+++ b/tests/test_modules/good/mod_def.catala_en
@ -31,12 +31,7 @@ scope S:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [24/24]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [0/0]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
-[RESULT] Invariant default_no_arrow checked. result: [4/4]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/mod_def_context.catala_en
+++ b/tests/test_modules/good/mod_def_context.catala_en
@ -60,12 +60,7 @@ scope Stest:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [207/207]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [18/18]
-[RESULT] Invariant no_return_a_function checked. result: [17/17]
-[RESULT] Invariant no_partial_evaluation checked. result: [18/18]
-[RESULT] Invariant default_no_arrow checked. result: [22/22]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/mod_middle.catala_en
+++ b/tests/test_modules/good/mod_middle.catala_en
@ -21,12 +21,7 @@ scope S:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [65/65]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [4/4]
-[RESULT] Invariant no_return_a_function checked. result: [2/2]
-[RESULT] Invariant no_partial_evaluation checked. result: [4/4]
-[RESULT] Invariant default_no_arrow checked. result: [7/7]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/mod_use.catala_en
+++ b/tests/test_modules/good/mod_use.catala_en
@ -27,12 +27,7 @@ scope T2:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [74/74]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [2/2]
-[RESULT] Invariant no_return_a_function checked. result: [0/0]
-[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
-[RESULT] Invariant default_no_arrow checked. result: [8/8]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/mod_use2.catala_en
+++ b/tests/test_modules/good/mod_use2.catala_en
@ -19,12 +19,7 @@ scope T:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [49/49]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [8/8]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/mod_use3.catala_en
+++ b/tests/test_modules/good/mod_use3.catala_en
@ -23,12 +23,7 @@ scope T:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [49/49]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [1/1]
-[RESULT] Invariant no_return_a_function checked. result: [1/1]
-[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
-[RESULT] Invariant default_no_arrow checked. result: [8/8]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/mod_use_context.catala_en
+++ b/tests/test_modules/good/mod_use_context.catala_en
@ -44,12 +44,7 @@ scope TestCall:

 ```catala-test-inline
 $ catala Typecheck --check-invariants
-[RESULT] Invariant typing_defaults checked. result: [146/146]
-[RESULT] Invariant match_inversion checked. result: [0/0]
-[RESULT] Invariant app_inversion checked. result: [15/15]
-[RESULT] Invariant no_return_a_function checked. result: [16/16]
-[RESULT] Invariant no_partial_evaluation checked. result: [15/15]
-[RESULT] Invariant default_no_arrow checked. result: [13/13]
+[RESULT] All invariant checks passed
 [RESULT] Typechecking successful!
 ```

--- a/tests/test_modules/good/prorata_syntax.catala_en
+++ b/tests/test_modules/good/prorata_syntax.catala_en
@ -0,0 +1,65 @@
+> Using Prorata_external as Ext
+
+
+```catala
+declaration structure HouseholdMember:
+  data birthdate content date
+  data revenue content money
+
+declaration structure HouseholdMemberTaxed:
+  data member content HouseholdMember
+  data tax content money
+
+declaration individual_tax_amount content list of HouseholdMemberTaxed
+  depends on members content list of HouseholdMember,
+             tax_to_distribute content money
+  equals
+  let revenues equals member.revenue for member among members in
+  let distributed_tax equals Ext.prorata of tax_to_distribute, revenues in
+  HouseholdMemberTaxed {
+    -- member: member
+    -- tax: tax_amount
+  }
+  for (member, tax_amount) among (members, distributed_tax)
+
+declaration scope S:
+  output result content list of HouseholdMemberTaxed
+
+scope S:
+  definition result equals
+  individual_tax_amount of
+    [ HouseholdMember { -- birthdate: |2000-01-01| -- revenue: $10000 };
+      HouseholdMember { -- birthdate: |2000-01-02| -- revenue: $1000 };
+      HouseholdMember { -- birthdate: |2000-01-02| -- revenue: $100 } ],
+    $300
+```
+
+```catala-test-inline
+$ catala typecheck --check-invariants
+[RESULT] All invariant checks passed
+[RESULT] Typechecking successful!
+```
+
+```catala-test-inline
+$ catala interpret -s S
+[RESULT] Computation successful! Results:
+[RESULT]
+result =
+  [
+    HouseholdMemberTaxed {
+      -- member:
+        HouseholdMember { -- birthdate: 2000-01-01 -- revenue: $10,000.00 }
+      -- tax: $270.27
+    };
+    HouseholdMemberTaxed {
+      -- member:
+        HouseholdMember { -- birthdate: 2000-01-02 -- revenue: $1,000.00 }
+      -- tax: $27.03
+    };
+    HouseholdMemberTaxed {
+      -- member:
+        HouseholdMember { -- birthdate: 2000-01-02 -- revenue: $100.00 }
+      -- tax: $2.70
+    }
+  ]
+```
--- a/Show More
+++ b/Show More