diff --git a/Cargo.lock b/Cargo.lock
index 18b95d64e..ca53ffb76 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -88,9 +88,9 @@ dependencies = [
 
 [[package]]
 name = "anyhow"
-version = "1.0.94"
+version = "1.0.95"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c1fd03a028ef38ba2276dce7e33fcd6369c158a1bca17946c4b1b701891c1ff7"
+checksum = "34ac096ce696dc2fcabef30516bb13c0a68a11d30131d3df6f04711467681b04"
 
 [[package]]
 name = "arrayvec"
@@ -133,7 +133,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "serde",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -323,13 +323,13 @@ checksum = "8b75356056920673b02621b35afd0f7dda9306d03c79a30f5c56c44cf256e3de"
 
 [[package]]
 name = "async-trait"
-version = "0.1.83"
+version = "0.1.84"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "721cae7de5c34fbb2acd27e21e6d2cf7b886dce0c27388d46c4e6c47ea4318dd"
+checksum = "1b1244b10dcd56c92219da4e14caa97e312079e185f04ba3eea25061561dc0a0"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -346,7 +346,7 @@ checksum = "3c87f3f15e7794432337fc718554eaa4dc8f04c9677a950ffe366f20a162ae42"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -360,7 +360,9 @@ name = "backend"
 version = "0.1.0"
 dependencies = [
  "ast",
+ "miette",
  "printer",
+ "thiserror",
  "url",
 ]
 
@@ -466,9 +468,9 @@ dependencies = [
 
 [[package]]
 name = "bstr"
-version = "1.11.0"
+version = "1.11.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1a68f1f47cdf0ec8ee4b941b2eee2a80cb796db73118c0dd09ac63fbe405be22"
+checksum = "531a9155a481e2ee699d4f98f43c0ca4ff8ee1bfd55c31e9e98fb29d2b176fe0"
 dependencies = [
  "memchr",
  "regex-automata",
@@ -495,9 +497,9 @@ checksum = "325918d6fe32f23b19878fe4b34794ae41fc19ddbe53b10571a4874d44ffd39b"
 
 [[package]]
 name = "cc"
-version = "1.2.3"
+version = "1.2.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "27f657647bcff5394bf56c7317665bbf790a137a50eaaa5c6bfbb9e27a518f2d"
+checksum = "a012a0df96dd6d06ba9a1b29d6402d1a5d77c6befd2566afdc26e10603dc93d7"
 dependencies = [
  "shlex",
 ]
@@ -538,9 +540,9 @@ dependencies = [
 
 [[package]]
 name = "clap_complete"
-version = "4.5.38"
+version = "4.5.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d9647a559c112175f17cf724dc72d3645680a883c58481332779192b0d8e7a01"
+checksum = "ac2e663e3e3bed2d32d065a8404024dad306e699a04263ec59919529f803aee9"
 dependencies = [
  "clap",
 ]
@@ -554,7 +556,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -632,18 +634,18 @@ dependencies = [
 
 [[package]]
 name = "crossbeam-channel"
-version = "0.5.13"
+version = "0.5.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "33480d6946193aa8033910124896ca395333cae7e2d1113d1fef6c3272217df2"
+checksum = "06ba6d68e24814cb8de6bb986db8222d3a027d15872cabc0d18817bc3c0e4471"
 dependencies = [
  "crossbeam-utils",
 ]
 
 [[package]]
 name = "crossbeam-deque"
-version = "0.8.5"
+version = "0.8.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d"
+checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51"
 dependencies = [
  "crossbeam-epoch",
  "crossbeam-utils",
@@ -660,9 +662,9 @@ dependencies = [
 
 [[package]]
 name = "crossbeam-utils"
-version = "0.8.20"
+version = "0.8.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80"
+checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28"
 
 [[package]]
 name = "crunchy"
@@ -746,7 +748,7 @@ checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -835,9 +837,9 @@ dependencies = [
 
 [[package]]
 name = "env_filter"
-version = "0.1.2"
+version = "0.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4f2c92ceda6ceec50f43169f9ee8424fe2db276791afde7b2cd8bc084cb376ab"
+checksum = "186e05a59d4c50738528153b83b0b0194d3a29507dfec16eccd4b342903397d0"
 dependencies = [
  "log",
  "regex",
@@ -845,9 +847,9 @@ dependencies = [
 
 [[package]]
 name = "env_logger"
-version = "0.11.5"
+version = "0.11.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e13fa619b91fb2381732789fc5de83b45675e882f66623b7d8cb4f643017018d"
+checksum = "dcaee3d8e3cfc3fd92428d477bc97fc29ec8716d180c0d74c643bb26166660e0"
 dependencies = [
  "anstream",
  "anstyle",
@@ -928,9 +930,9 @@ dependencies = [
 
 [[package]]
 name = "fastrand"
-version = "2.2.0"
+version = "2.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "486f806e73c5707928240ddc295403b1b93c96a02038563881c4a2fd84b81ac4"
+checksum = "37909eebbb50d72f9059c3b6d82c0463f2ff062c9e95845c43a6c9c0355411be"
 
 [[package]]
 name = "fixedbitset"
@@ -1056,7 +1058,7 @@ checksum = "162ee34ebcb7c64a8abebc059ce0fee27c2262618d7b60ed8faf72fef13c3650"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -1248,9 +1250,9 @@ checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
 
 [[package]]
 name = "hyper"
-version = "1.5.1"
+version = "1.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "97818827ef4f364230e16705d4706e2897df2bb60617d6ca15d598025a3c481f"
+checksum = "256fb8d4bd6413123cc9d91832d78325c48ff41677595be797d90f42969beae0"
 dependencies = [
  "bytes",
  "futures-channel",
@@ -1268,9 +1270,9 @@ dependencies = [
 
 [[package]]
 name = "hyper-rustls"
-version = "0.27.3"
+version = "0.27.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "08afdbb5c31130e3034af566421053ab03787c640246a446327f550d11bcb333"
+checksum = "2d191583f3da1305256f22463b9bb0471acad48a4e534a5218b9963e9c1f59b2"
 dependencies = [
  "futures-util",
  "http",
@@ -1433,7 +1435,7 @@ checksum = "1ec89e9337638ecdc08744df490b221a7399bf8d164eb52a665454e60e075ad6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -1627,9 +1629,9 @@ checksum = "0c2cdeb66e45e9f36bfad5bbdb4d2384e70936afbee843c6f6543f0c551ebb25"
 
 [[package]]
 name = "libc"
-version = "0.2.167"
+version = "0.2.169"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09d6582e104315a817dff97f75133544b2e094ee22447d2acf4a74e189ba06fc"
+checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a"
 
 [[package]]
 name = "libm"
@@ -1680,18 +1682,18 @@ dependencies = [
 
 [[package]]
 name = "logos"
-version = "0.14.2"
+version = "0.14.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1c6b6e02facda28ca5fb8dbe4b152496ba3b1bd5a4b40bb2b1b2d8ad74e0f39b"
+checksum = "7251356ef8cb7aec833ddf598c6cb24d17b689d20b993f9d11a3d764e34e6458"
 dependencies = [
  "logos-derive",
 ]
 
 [[package]]
 name = "logos-codegen"
-version = "0.14.3"
+version = "0.14.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5f3303189202bb8a052bcd93d66b6c03e6fe70d9c7c47c0ea5e974955e54c876"
+checksum = "59f80069600c0d66734f5ff52cc42f2dabd6b29d205f333d61fd7832e9e9963f"
 dependencies = [
  "beef",
  "fnv",
@@ -1699,15 +1701,14 @@ dependencies = [
  "proc-macro2",
  "quote",
  "regex-syntax 0.8.5",
- "rustc_version",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
 name = "logos-derive"
-version = "0.14.3"
+version = "0.14.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "774a1c225576486e4fdf40b74646f672c542ca3608160d348749693ae9d456e6"
+checksum = "24fb722b06a9dc12adb0963ed585f19fc61dc5413e6a9be9422ef92c091e731d"
 dependencies = [
  "logos-codegen",
 ]
@@ -1841,7 +1842,7 @@ checksum = "23c9b935fbe1d6cbd1dac857b54a688145e2d93f48db36010514d0f612d0ad67"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -1876,9 +1877,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
 
 [[package]]
 name = "miniz_oxide"
-version = "0.8.0"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1"
+checksum = "4ffbe83022cedc1d264172192511ae958937694cd57ce297164951b8b3568394"
 dependencies = [
  "adler2",
 ]
@@ -1982,9 +1983,9 @@ dependencies = [
 
 [[package]]
 name = "object"
-version = "0.36.5"
+version = "0.36.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e"
+checksum = "62948e14d923ea95ea2c7c86c71013138b66525b86bdc08d2dcc262bdb497b87"
 dependencies = [
  "memchr",
 ]
@@ -2034,7 +2035,7 @@ checksum = "a948666b637a0f465e8564c73e89d4dde00d72d4d473cc972f390fc3dcee7d9c"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -2237,9 +2238,9 @@ checksum = "925383efa346730478fb4838dbe9137d2a47675ad789c546d150a6e1dd4ab31c"
 
 [[package]]
 name = "predicates"
-version = "3.1.2"
+version = "3.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e9086cc7640c29a356d1a29fd134380bee9d8f79a17410aa76e7ad295f42c97"
+checksum = "a5d19ee57562043d37e82899fade9a22ebab7be9cef5026b07fda9cdd4293573"
 dependencies = [
  "anstyle",
  "difflib",
@@ -2248,15 +2249,15 @@ dependencies = [
 
 [[package]]
 name = "predicates-core"
-version = "1.0.8"
+version = "1.0.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ae8177bee8e75d6846599c6b9ff679ed51e882816914eec639944d7c9aa11931"
+checksum = "727e462b119fe9c93fd0eb1429a5f7647394014cf3c04ab2c0350eeb09095ffa"
 
 [[package]]
 name = "predicates-tree"
-version = "1.0.11"
+version = "1.0.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41b740d195ed3166cd147c8047ec98db0e22ec019eb8eeb76d343b795304fb13"
+checksum = "72dd2d6d381dfb73a193c7fca536518d7caee39fc8503f74e7dc0be0531b425c"
 dependencies = [
  "predicates-core",
  "termtree",
@@ -2304,9 +2305,9 @@ dependencies = [
 
 [[package]]
 name = "quote"
-version = "1.0.37"
+version = "1.0.38"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
+checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc"
 dependencies = [
  "proc-macro2",
 ]
@@ -2363,9 +2364,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.7"
+version = "0.5.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f"
+checksum = "03a862b389f93e68874fbf580b9de08dd02facb9a788ebadaf4a3fd33cf58834"
 dependencies = [
  "bitflags 2.6.0",
 ]
@@ -2424,9 +2425,9 @@ checksum = "2b15c43186be67a4fd63bee50d0303afffcef381492ebe2c5d87f324e1b8815c"
 
 [[package]]
 name = "reqwest"
-version = "0.12.9"
+version = "0.12.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a77c62af46e79de0a562e1a9849205ffcb7fc1238876e9bd743357570e04046f"
+checksum = "43e734407157c3c2034e0258f5e4473ddb361b1e85f95a66690d67264d7cd1da"
 dependencies = [
  "base64 0.22.1",
  "bytes",
@@ -2453,10 +2454,11 @@ dependencies = [
  "serde",
  "serde_json",
  "serde_urlencoded",
- "sync_wrapper 1.0.2",
+ "sync_wrapper",
  "system-configuration",
  "tokio",
  "tokio-native-tls",
+ "tower",
  "tower-service",
  "url",
  "wasm-bindgen",
@@ -2515,33 +2517,24 @@ version = "0.1.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
 
-[[package]]
-name = "rustc_version"
-version = "0.4.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
-dependencies = [
- "semver",
-]
-
 [[package]]
 name = "rustix"
-version = "0.38.41"
+version = "0.38.42"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d7f649912bc1495e167a6edee79151c84b1bad49748cb4f1f1167f459f6224f6"
+checksum = "f93dc38ecbab2eb790ff964bb77fa94faf256fd3e73285fd7ba0903b76bedb85"
 dependencies = [
  "bitflags 2.6.0",
  "errno",
  "libc",
  "linux-raw-sys",
- "windows-sys 0.52.0",
+ "windows-sys 0.59.0",
 ]
 
 [[package]]
 name = "rustls"
-version = "0.23.19"
+version = "0.23.20"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "934b404430bb06b3fae2cba809eb45a1ab1aecd64491213d7c3301b88393f8d1"
+checksum = "5065c3f250cbd332cd894be57c40fa52387247659b14a2d6041d121547903b1b"
 dependencies = [
  "once_cell",
  "rustls-pki-types",
@@ -2561,9 +2554,9 @@ dependencies = [
 
 [[package]]
 name = "rustls-pki-types"
-version = "1.10.0"
+version = "1.10.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "16f1201b3c9a7ee8039bcadc17b7e605e2945b27eee7631788c1bd2b0643674b"
+checksum = "d2bf47e6ff922db3825eb750c4e2ff784c6ff8fb9e13046ef6a1d1c5401b0b37"
 
 [[package]]
 name = "rustls-webpki"
@@ -2578,9 +2571,9 @@ dependencies = [
 
 [[package]]
 name = "rustversion"
-version = "1.0.18"
+version = "1.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248"
+checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4"
 
 [[package]]
 name = "ryu"
@@ -2627,45 +2620,39 @@ dependencies = [
 
 [[package]]
 name = "security-framework-sys"
-version = "2.12.1"
+version = "2.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fa39c7303dc58b5543c94d22c1766b0d31f2ee58306363ea622b10bbc075eaa2"
+checksum = "1863fd3768cd83c56a7f60faa4dc0d403f1b6df0a38c3c25f44b7894e45370d5"
 dependencies = [
  "core-foundation-sys",
  "libc",
 ]
 
-[[package]]
-name = "semver"
-version = "1.0.23"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b"
-
 [[package]]
 name = "serde"
-version = "1.0.215"
+version = "1.0.217"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f"
+checksum = "02fc4265df13d6fa1d00ecff087228cc0a2b5f3c0e87e258d8b94a156e984c70"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.215"
+version = "1.0.217"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0"
+checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.133"
+version = "1.0.134"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c7fceb2473b9166b2294ef05efcb65a3db80803f0b03ef86a5fc88a2b85ee377"
+checksum = "d00f4175c42ee48b15416f6193a959ba3a0d67fc699a0db9ad12df9f83991c7d"
 dependencies = [
  "itoa",
  "memchr",
@@ -2681,7 +2668,7 @@ checksum = "6c64451ba24fc7a6a2d60fc75dd9c83c90903b19028d4eff35e88fc1e86564e9"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -2810,21 +2797,15 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.90"
+version = "2.0.94"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31"
+checksum = "987bc0be1cdea8b10216bd06e2ca407d40b9543468fafd3ddfb02f36e77f71f3"
 dependencies = [
  "proc-macro2",
  "quote",
  "unicode-ident",
 ]
 
-[[package]]
-name = "sync_wrapper"
-version = "0.1.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2047c6ded9c721764247e62cd3b03c09ffc529b2ba5b10ec482ae507a4a70160"
-
 [[package]]
 name = "sync_wrapper"
 version = "1.0.2"
@@ -2842,7 +2823,7 @@ checksum = "c8af7666ab7b6390ab78131fb5b0fce11d6b7a6951602017c35fa82800708971"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -2957,12 +2938,13 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.14.0"
+version = "3.15.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "28cce251fcbc87fac86a866eeb0d6c2d536fc16d06f184bb61aeae11aa4cee0c"
+checksum = "9a8a559c81686f576e8cd0290cd2a24a2a9ad80c98b3478856500fcbd7acd704"
 dependencies = [
  "cfg-if",
  "fastrand",
+ "getrandom",
  "once_cell",
  "rustix",
  "windows-sys 0.59.0",
@@ -3010,9 +2992,9 @@ dependencies = [
 
 [[package]]
 name = "termtree"
-version = "0.4.1"
+version = "0.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3369f5ac52d5eb6ab48c6b4ffdc8efbcad6b89c765749064ba298f2c68a16a76"
+checksum = "8f50febec83f5ee1df3015341d8bd429f2d1cc62bcba7ea2076759d315084683"
 
 [[package]]
 name = "test-runner"
@@ -3064,7 +3046,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -3176,14 +3158,15 @@ dependencies = [
 
 [[package]]
 name = "tower"
-version = "0.5.1"
+version = "0.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2873938d487c3cfb9aed7546dc9f2711d867c9f90c46b889989a2cb84eba6b4f"
+checksum = "d039ad9159c98b70ecfd540b2573b97f7f52c3e8d9f8ad57a24b916a536975f9"
 dependencies = [
  "futures-core",
  "futures-util",
  "pin-project-lite",
- "sync_wrapper 0.1.2",
+ "sync_wrapper",
+ "tokio",
  "tower-layer",
  "tower-service",
 ]
@@ -3222,7 +3205,7 @@ source = "git+https://github.com/tower-lsp/tower-lsp?rev=19f5a87810ff4b643d2bc39
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -3250,7 +3233,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -3288,9 +3271,9 @@ checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a"
 
 [[package]]
 name = "unicase"
-version = "2.8.0"
+version = "2.8.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e51b68083f157f853b6379db119d1c1be0e6e4dec98101079dec41f6f5cf6df"
+checksum = "75b844d17643ee918803943289730bec8aac480150456169e647ed0b576ba539"
 
 [[package]]
 name = "unicode-ident"
@@ -3446,7 +3429,7 @@ dependencies = [
  "log",
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
  "wasm-bindgen-shared",
 ]
 
@@ -3482,7 +3465,7 @@ checksum = "30d7a95b763d3c45903ed6c81f156801839e5ee968bb07e534c44df0fcd330c2"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
  "wasm-bindgen-backend",
  "wasm-bindgen-shared",
 ]
@@ -3697,7 +3680,7 @@ checksum = "2380878cad4ac9aac1e2435f3eb4020e8374b5f13c296cb75b4620ff8e229154"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
  "synstructure",
 ]
 
@@ -3719,7 +3702,7 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
 
 [[package]]
@@ -3739,7 +3722,7 @@ checksum = "595eed982f7d355beb85837f651fa22e90b3c044842dc7f2c2842c086f295808"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
  "synstructure",
 ]
 
@@ -3768,5 +3751,5 @@ checksum = "6eafa6dfb17584ea3e2bd6e76e0cc15ad7af12b09abdd1ca55961bed9b1063c6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.90",
+ "syn 2.0.94",
 ]
diff --git a/lang/ast/src/decls.rs b/lang/ast/src/decls.rs
index ae4dbbb52..0fce2ac37 100644
--- a/lang/ast/src/decls.rs
+++ b/lang/ast/src/decls.rs
@@ -601,11 +601,13 @@ pub struct Dtor {
     pub params: Telescope,
     pub self_param: SelfParam,
     pub ret_typ: Box<Exp>,
+    /// Whether the destructor is erased during compilation.
+    pub erased: bool,
 }
 
 impl Print for Dtor {
     fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
-        let Dtor { span: _, doc, name, params, self_param, ret_typ } = self;
+        let Dtor { span: _, doc, name, params, self_param, ret_typ, erased: _ } = self;
 
         let doc = doc.print(cfg, alloc);
         let head = if self_param.is_simple() {
@@ -624,7 +626,7 @@ impl Print for Dtor {
 
 impl Zonk for Dtor {
     fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
-        let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ } = self;
+        let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ, erased: _ } = self;
         params.zonk(meta_vars)?;
         self_param.zonk(meta_vars)?;
         ret_typ.zonk(meta_vars)?;
@@ -634,7 +636,7 @@ impl Zonk for Dtor {
 
 impl ContainsMetaVars for Dtor {
     fn contains_metavars(&self) -> bool {
-        let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ } = self;
+        let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ, erased: _ } = self;
 
         params.contains_metavars() || self_param.contains_metavars() || ret_typ.contains_metavars()
     }
@@ -654,6 +656,8 @@ pub struct Def {
     pub self_param: SelfParam,
     pub ret_typ: Box<Exp>,
     pub cases: Vec<Case>,
+    /// Whether the definition is erased during compilation.
+    pub erased: bool,
 }
 
 impl Def {
@@ -665,13 +669,14 @@ impl Def {
             params: self.params.clone(),
             self_param: self.self_param.clone(),
             ret_typ: self.ret_typ.clone(),
+            erased: self.erased,
         }
     }
 }
 
 impl Print for Def {
     fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
-        let Def { span: _, doc, name, attr, params, self_param, ret_typ, cases } = self;
+        let Def { span: _, doc, name, attr, params, self_param, ret_typ, cases, erased: _ } = self;
         if !attr.is_visible() {
             return alloc.nil();
         }
@@ -696,7 +701,17 @@ impl Print for Def {
 
 impl Zonk for Def {
     fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
-        let Def { span: _, doc: _, name: _, attr: _, params, self_param, ret_typ, cases } = self;
+        let Def {
+            span: _,
+            doc: _,
+            name: _,
+            attr: _,
+            params,
+            self_param,
+            ret_typ,
+            cases,
+            erased: _,
+        } = self;
         params.zonk(meta_vars)?;
         self_param.zonk(meta_vars)?;
         ret_typ.zonk(meta_vars)?;
@@ -709,7 +724,17 @@ impl Zonk for Def {
 
 impl ContainsMetaVars for Def {
     fn contains_metavars(&self) -> bool {
-        let Def { span: _, doc: _, name: _, attr: _, params, self_param, ret_typ, cases } = self;
+        let Def {
+            span: _,
+            doc: _,
+            name: _,
+            attr: _,
+            params,
+            self_param,
+            ret_typ,
+            cases,
+            erased: _,
+        } = self;
 
         params.contains_metavars()
             || self_param.contains_metavars()
@@ -805,6 +830,8 @@ pub struct Let {
     pub params: Telescope,
     pub typ: Box<Exp>,
     pub body: Box<Exp>,
+    /// Whether the let binding is erased during compilation.
+    pub erased: bool,
 }
 
 impl Let {
@@ -816,7 +843,7 @@ impl Let {
 
 impl Print for Let {
     fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
-        let Let { span: _, doc, name, attr, params, typ, body } = self;
+        let Let { span: _, doc, name, attr, params, typ, body, erased: _ } = self;
         if !attr.is_visible() {
             return alloc.nil();
         }
@@ -839,7 +866,7 @@ impl Print for Let {
 
 impl Zonk for Let {
     fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
-        let Let { span: _, doc: _, name: _, attr: _, params, typ, body } = self;
+        let Let { span: _, doc: _, name: _, attr: _, params, typ, body, erased: _ } = self;
         params.zonk(meta_vars)?;
         typ.zonk(meta_vars)?;
         body.zonk(meta_vars)?;
@@ -849,7 +876,7 @@ impl Zonk for Let {
 
 impl ContainsMetaVars for Let {
     fn contains_metavars(&self) -> bool {
-        let Let { span: _, doc: _, name: _, attr: _, params, typ, body } = self;
+        let Let { span: _, doc: _, name: _, attr: _, params, typ, body, erased: _ } = self;
 
         params.contains_metavars() || typ.contains_metavars() || body.contains_metavars()
     }
@@ -873,6 +900,7 @@ impl SelfParam {
                 implicit: false,
                 name: self.name.clone().unwrap_or_else(|| VarBind::from_string("")),
                 typ: Box::new(self.typ.to_exp()),
+                erased: false,
             }],
         }
     }
@@ -946,11 +974,12 @@ impl Telescope {
         let params = self
             .params
             .iter()
-            .map(|Param { name, .. }| ParamInst {
+            .map(|Param { name, erased, .. }| ParamInst {
                 span: None,
                 name: name.clone(),
                 info: None,
                 typ: None,
+                erased: *erased,
             })
             .collect();
         TelescopeInst { params }
@@ -978,7 +1007,7 @@ impl Print for Telescope {
         };
         // Running stands for the type and implicitness of the current "chunk" we are building.
         let mut running: Option<(&Exp, bool)> = None;
-        for Param { implicit, name, typ } in params {
+        for Param { implicit, name, typ, erased: _ } in params {
             match running {
                 // We need to shift before comparing to ensure we compare the correct De-Bruijn indices
                 Some((rtype, rimplicit))
@@ -1063,11 +1092,13 @@ mod print_telescope_tests {
             implicit: false,
             name: VarBind::from_string("x"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let param2 = Param {
             implicit: false,
             name: VarBind::from_string("y"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let tele = Telescope { params: vec![param1, param2] };
         assert_eq!(tele.print_to_string(Default::default()), "(x y: Type)")
@@ -1079,11 +1110,13 @@ mod print_telescope_tests {
             implicit: true,
             name: VarBind::from_string("x"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let param2 = Param {
             implicit: true,
             name: VarBind::from_string("y"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let tele = Telescope { params: vec![param1, param2] };
         assert_eq!(tele.print_to_string(Default::default()), "(implicit x y: Type)")
@@ -1095,11 +1128,13 @@ mod print_telescope_tests {
             implicit: true,
             name: VarBind::from_string("x"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let param2 = Param {
             implicit: false,
             name: VarBind::from_string("y"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let tele = Telescope { params: vec![param1, param2] };
         assert_eq!(tele.print_to_string(Default::default()), "(implicit x: Type, y: Type)")
@@ -1111,11 +1146,13 @@ mod print_telescope_tests {
             implicit: false,
             name: VarBind::from_string("x"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let param2 = Param {
             implicit: true,
             name: VarBind::from_string("y"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let tele = Telescope { params: vec![param1, param2] };
         assert_eq!(tele.print_to_string(Default::default()), "(x: Type, implicit y: Type)")
@@ -1127,6 +1164,7 @@ mod print_telescope_tests {
             implicit: false,
             name: VarBind::from_string("a"),
             typ: Box::new(TypeUniv::new().into()),
+            erased: false,
         };
         let param2 = Param {
             implicit: false,
@@ -1137,6 +1175,7 @@ mod print_telescope_tests {
                 name: VarBound::from_string("a"),
                 inferred_type: None,
             })),
+            erased: false,
         };
         let param3 = Param {
             implicit: false,
@@ -1147,6 +1186,7 @@ mod print_telescope_tests {
                 name: VarBound::from_string("a"),
                 inferred_type: None,
             })),
+            erased: false,
         };
         let tele = Telescope { params: vec![param1, param2, param3] };
         assert_eq!(tele.print_to_string(Default::default()), "(a: Type, x y: a)")
@@ -1164,19 +1204,21 @@ pub struct Param {
     #[derivative(PartialEq = "ignore", Hash = "ignore")]
     pub name: VarBind,
     pub typ: Box<Exp>,
+    /// Whether the parameter is erased during compilation.
+    pub erased: bool,
 }
 
 impl Substitutable for Param {
     type Result = Param;
     fn subst<S: Substitution>(&self, ctx: &mut LevelCtx, by: &S) -> Self {
-        let Param { implicit, name, typ } = self;
-        Param { implicit: *implicit, name: name.clone(), typ: typ.subst(ctx, by) }
+        let Param { implicit, name, typ, erased } = self;
+        Param { implicit: *implicit, name: name.clone(), typ: typ.subst(ctx, by), erased: *erased }
     }
 }
 
 impl Print for Param {
     fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
-        let Param { implicit, name, typ } = self;
+        let Param { implicit, name, typ, erased: _ } = self;
         if *implicit {
             alloc
                 .text(IMPLICIT)
@@ -1193,14 +1235,14 @@ impl Print for Param {
 
 impl Zonk for Param {
     fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
-        let Param { implicit: _, name: _, typ } = self;
+        let Param { implicit: _, name: _, typ, erased: _ } = self;
         typ.zonk(meta_vars)
     }
 }
 
 impl ContainsMetaVars for Param {
     fn contains_metavars(&self) -> bool {
-        let Param { implicit: _, name: _, typ } = self;
+        let Param { implicit: _, name: _, typ, erased: _ } = self;
 
         typ.contains_metavars()
     }
diff --git a/lang/ast/src/exp/args.rs b/lang/ast/src/exp/args.rs
index df07f194a..6ba6303ec 100644
--- a/lang/ast/src/exp/args.rs
+++ b/lang/ast/src/exp/args.rs
@@ -23,21 +23,29 @@ use super::{Exp, Hole, Lvl, MetaVar, VarBound};
 #[derive(Debug, Clone, Derivative)]
 #[derivative(Eq, PartialEq, Hash)]
 pub enum Arg {
-    UnnamedArg(Box<Exp>),
-    NamedArg(VarBound, Box<Exp>),
-    InsertedImplicitArg(Hole),
+    UnnamedArg { arg: Box<Exp>, erased: bool },
+    NamedArg { name: VarBound, arg: Box<Exp>, erased: bool },
+    InsertedImplicitArg { hole: Hole, erased: bool },
 }
 
 impl Arg {
     pub fn is_inserted_implicit(&self) -> bool {
-        matches!(self, Arg::InsertedImplicitArg(_))
+        matches!(self, Arg::InsertedImplicitArg { .. })
     }
 
     pub fn exp(&self) -> Box<Exp> {
         match self {
-            Arg::UnnamedArg(e) => e.clone(),
-            Arg::NamedArg(_, e) => e.clone(),
-            Arg::InsertedImplicitArg(hole) => Box::new(hole.clone().into()),
+            Arg::UnnamedArg { arg, .. } => arg.clone(),
+            Arg::NamedArg { arg, .. } => arg.clone(),
+            Arg::InsertedImplicitArg { hole, .. } => Box::new(hole.clone().into()),
+        }
+    }
+
+    pub fn erased(&self) -> bool {
+        match self {
+            Arg::UnnamedArg { erased, .. } => *erased,
+            Arg::NamedArg { erased, .. } => *erased,
+            Arg::InsertedImplicitArg { erased, .. } => *erased,
         }
     }
 }
@@ -45,9 +53,9 @@ impl Arg {
 impl HasSpan for Arg {
     fn span(&self) -> Option<Span> {
         match self {
-            Arg::UnnamedArg(e) => e.span(),
-            Arg::NamedArg(_, e) => e.span(),
-            Arg::InsertedImplicitArg(hole) => hole.span(),
+            Arg::UnnamedArg { arg, .. } => arg.span(),
+            Arg::NamedArg { arg, .. } => arg.span(),
+            Arg::InsertedImplicitArg { hole, .. } => hole.span(),
         }
     }
 }
@@ -55,9 +63,9 @@ impl HasSpan for Arg {
 impl Shift for Arg {
     fn shift_in_range<R: ShiftRange>(&mut self, range: &R, by: (isize, isize)) {
         match self {
-            Arg::UnnamedArg(e) => e.shift_in_range(range, by),
-            Arg::NamedArg(_, e) => e.shift_in_range(range, by),
-            Arg::InsertedImplicitArg(hole) => hole.shift_in_range(range, by),
+            Arg::UnnamedArg { arg, .. } => arg.shift_in_range(range, by),
+            Arg::NamedArg { arg, .. } => arg.shift_in_range(range, by),
+            Arg::InsertedImplicitArg { hole, .. } => hole.shift_in_range(range, by),
         }
     }
 }
@@ -65,9 +73,9 @@ impl Shift for Arg {
 impl Occurs for Arg {
     fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool {
         match self {
-            Arg::UnnamedArg(e) => e.occurs(ctx, lvl),
-            Arg::NamedArg(_, e) => e.occurs(ctx, lvl),
-            Arg::InsertedImplicitArg(hole) => hole.occurs(ctx, lvl),
+            Arg::UnnamedArg { arg, .. } => arg.occurs(ctx, lvl),
+            Arg::NamedArg { arg, .. } => arg.occurs(ctx, lvl),
+            Arg::InsertedImplicitArg { hole, .. } => hole.occurs(ctx, lvl),
         }
     }
 }
@@ -75,9 +83,9 @@ impl Occurs for Arg {
 impl HasType for Arg {
     fn typ(&self) -> Option<Box<Exp>> {
         match self {
-            Arg::UnnamedArg(e) => e.typ(),
-            Arg::NamedArg(_, e) => e.typ(),
-            Arg::InsertedImplicitArg(hole) => hole.typ(),
+            Arg::UnnamedArg { arg, .. } => arg.typ(),
+            Arg::NamedArg { arg, .. } => arg.typ(),
+            Arg::InsertedImplicitArg { hole, .. } => hole.typ(),
         }
     }
 }
@@ -86,9 +94,15 @@ impl Substitutable for Arg {
     type Result = Arg;
     fn subst<S: Substitution>(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result {
         match self {
-            Arg::UnnamedArg(e) => Arg::UnnamedArg(e.subst(ctx, by)),
-            Arg::NamedArg(i, e) => Arg::NamedArg(i.clone(), e.subst(ctx, by)),
-            Arg::InsertedImplicitArg(hole) => Arg::InsertedImplicitArg(hole.subst(ctx, by)),
+            Arg::UnnamedArg { arg, erased } => {
+                Arg::UnnamedArg { arg: arg.subst(ctx, by), erased: *erased }
+            }
+            Arg::NamedArg { name: var, arg, erased } => {
+                Arg::NamedArg { name: var.clone(), arg: arg.subst(ctx, by), erased: *erased }
+            }
+            Arg::InsertedImplicitArg { hole, erased } => {
+                Arg::InsertedImplicitArg { hole: hole.subst(ctx, by), erased: *erased }
+            }
         }
     }
 }
@@ -96,9 +110,11 @@ impl Substitutable for Arg {
 impl Print for Arg {
     fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
         match self {
-            Arg::UnnamedArg(e) => e.print(cfg, alloc),
-            Arg::NamedArg(i, e) => alloc.text(&i.id).append(COLONEQ).append(e.print(cfg, alloc)),
-            Arg::InsertedImplicitArg(_) => {
+            Arg::UnnamedArg { arg, .. } => arg.print(cfg, alloc),
+            Arg::NamedArg { name: var, arg, .. } => {
+                alloc.text(&var.id).append(COLONEQ).append(arg.print(cfg, alloc))
+            }
+            Arg::InsertedImplicitArg { .. } => {
                 panic!("Inserted implicit arguments should not be printed")
             }
         }
@@ -111,9 +127,9 @@ impl Zonk for Arg {
         meta_vars: &crate::HashMap<MetaVar, crate::MetaVarState>,
     ) -> Result<(), ZonkError> {
         match self {
-            Arg::UnnamedArg(e) => e.zonk(meta_vars),
-            Arg::NamedArg(_, e) => e.zonk(meta_vars),
-            Arg::InsertedImplicitArg(hole) => hole.zonk(meta_vars),
+            Arg::UnnamedArg { arg, .. } => arg.zonk(meta_vars),
+            Arg::NamedArg { arg, .. } => arg.zonk(meta_vars),
+            Arg::InsertedImplicitArg { hole, .. } => hole.zonk(meta_vars),
         }
     }
 }
@@ -121,9 +137,9 @@ impl Zonk for Arg {
 impl ContainsMetaVars for Arg {
     fn contains_metavars(&self) -> bool {
         match self {
-            Arg::UnnamedArg(e) => e.contains_metavars(),
-            Arg::NamedArg(_, e) => e.contains_metavars(),
-            Arg::InsertedImplicitArg(hole) => hole.contains_metavars(),
+            Arg::UnnamedArg { arg, .. } => arg.contains_metavars(),
+            Arg::NamedArg { arg, .. } => arg.contains_metavars(),
+            Arg::InsertedImplicitArg { hole, .. } => hole.contains_metavars(),
         }
     }
 }
@@ -249,13 +265,19 @@ mod args_tests {
         );
 
         assert_eq!(
-            Args { args: vec![Arg::UnnamedArg(ctor.clone())] }.print_to_string(Default::default()),
+            Args { args: vec![Arg::UnnamedArg { arg: ctor.clone(), erased: false }] }
+                .print_to_string(Default::default()),
             "(T)".to_string()
         );
 
         assert_eq!(
-            Args { args: vec![Arg::UnnamedArg(ctor.clone()), Arg::UnnamedArg(ctor)] }
-                .print_to_string(Default::default()),
+            Args {
+                args: vec![
+                    Arg::UnnamedArg { arg: ctor.clone(), erased: false },
+                    Arg::UnnamedArg { arg: ctor, erased: false }
+                ]
+            }
+            .print_to_string(Default::default()),
             "(T, T)".to_string()
         )
     }
@@ -273,7 +295,8 @@ mod args_tests {
         };
 
         assert_eq!(
-            Args { args: vec![Arg::InsertedImplicitArg(hole)] }.print_to_string(Default::default()),
+            Args { args: vec![Arg::InsertedImplicitArg { hole, erased: false }] }
+                .print_to_string(Default::default()),
             "".to_string()
         )
     }
diff --git a/lang/ast/src/exp/telescope_inst.rs b/lang/ast/src/exp/telescope_inst.rs
index 832c9d063..9da74b0f5 100644
--- a/lang/ast/src/exp/telescope_inst.rs
+++ b/lang/ast/src/exp/telescope_inst.rs
@@ -75,11 +75,13 @@ pub struct ParamInst {
     pub name: VarBind,
     #[derivative(PartialEq = "ignore", Hash = "ignore")]
     pub typ: Option<Box<Exp>>,
+    /// Whether the parameter is erased during compilation.
+    pub erased: bool,
 }
 
 impl Print for ParamInst {
     fn print<'a>(&'a self, _cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
-        let ParamInst { span: _, info: _, name, typ: _ } = self;
+        let ParamInst { span: _, info: _, name, typ: _, erased: _ } = self;
         alloc.text(&name.id)
     }
 }
@@ -89,7 +91,7 @@ impl Zonk for ParamInst {
         &mut self,
         meta_vars: &crate::HashMap<MetaVar, crate::MetaVarState>,
     ) -> Result<(), ZonkError> {
-        let ParamInst { span: _, info, name: _, typ } = self;
+        let ParamInst { span: _, info, name: _, typ, erased: _ } = self;
 
         info.zonk(meta_vars)?;
         typ.zonk(meta_vars)?;
@@ -99,7 +101,7 @@ impl Zonk for ParamInst {
 
 impl ContainsMetaVars for ParamInst {
     fn contains_metavars(&self) -> bool {
-        let ParamInst { span: _, info, name: _, typ } = self;
+        let ParamInst { span: _, info, name: _, typ, erased: _ } = self;
 
         info.contains_metavars() || typ.contains_metavars()
     }
diff --git a/lang/backend/Cargo.toml b/lang/backend/Cargo.toml
index c629e787a..5b2b34a90 100644
--- a/lang/backend/Cargo.toml
+++ b/lang/backend/Cargo.toml
@@ -12,6 +12,9 @@ categories.workspace = true
 [dependencies]
 # ir structures
 url = { workspace = true }
+# error handling
+miette = { workspace = true }
+thiserror = { workspace = true }
 # workspace dependencies
 ast = { path = "../ast" }
 printer = { path = "../printer" }
diff --git a/lang/backend/src/ir/decls.rs b/lang/backend/src/ir/decls.rs
index 5d9e29486..c6c67f7cd 100644
--- a/lang/backend/src/ir/decls.rs
+++ b/lang/backend/src/ir/decls.rs
@@ -1,6 +1,3 @@
-//! High-level intermediate respresentation of the AST after erasure.
-//! This representation is shared between any compiler backends and hence can only make few assumptions about the compilation target.
-
 use url::Url;
 
 use ast::UseDecl;
diff --git a/lang/backend/src/ir/exprs.rs b/lang/backend/src/ir/exprs.rs
index 6a216eada..70b77eaff 100644
--- a/lang/backend/src/ir/exprs.rs
+++ b/lang/backend/src/ir/exprs.rs
@@ -205,6 +205,8 @@ impl Print for Case {
 pub struct Pattern {
     pub is_copattern: bool,
     pub name: String,
+    /// The URI of the module where `name` is defined.
+    pub module_uri: Url,
     pub params: Vec<String>,
 }
 
diff --git a/lang/backend/src/ir/mod.rs b/lang/backend/src/ir/mod.rs
index fe4b9e011..3a414a0a5 100644
--- a/lang/backend/src/ir/mod.rs
+++ b/lang/backend/src/ir/mod.rs
@@ -1,3 +1,10 @@
+//! High-level intermediate respresentation of the AST after erasure.
+//! This representation is shared between any compiler backends and hence can only make few assumptions about the compilation target.
+
 pub mod decls;
 pub mod exprs;
-pub mod lookup_table;
+pub mod symbol_table;
+
+pub use decls::*;
+pub use exprs::*;
+pub use symbol_table::*;
diff --git a/lang/backend/src/ir/lookup_table.rs b/lang/backend/src/ir/symbol_table.rs
similarity index 79%
rename from lang/backend/src/ir/lookup_table.rs
rename to lang/backend/src/ir/symbol_table.rs
index 8910cdcbd..a4d043bb6 100644
--- a/lang/backend/src/ir/lookup_table.rs
+++ b/lang/backend/src/ir/symbol_table.rs
@@ -1,10 +1,11 @@
 use ast::HashMap;
 
-pub struct GlobalLookupTable {
-    pub modules: HashMap<String, ModuleLookupTable>,
+pub struct GlobalSymbolTable {
+    pub modules: HashMap<String, ModuleSymbolTable>,
 }
 
-pub struct ModuleLookupTable {
+#[derive(Default)]
+pub struct ModuleSymbolTable {
     pub data_decls: HashMap<String, Data>,
     pub codata_decls: HashMap<String, Codata>,
 }
diff --git a/lang/backend/src/lib.rs b/lang/backend/src/lib.rs
index 19d2d13f0..a22196e51 100644
--- a/lang/backend/src/lib.rs
+++ b/lang/backend/src/lib.rs
@@ -1 +1,2 @@
 pub mod ir;
+pub mod result;
diff --git a/lang/backend/src/result.rs b/lang/backend/src/result.rs
new file mode 100644
index 000000000..c63a3d6da
--- /dev/null
+++ b/lang/backend/src/result.rs
@@ -0,0 +1,8 @@
+use miette::Diagnostic;
+use thiserror::Error;
+
+#[derive(Error, Debug, Diagnostic, Clone)]
+pub enum BackendError {
+    #[error("Impossible: {0}")]
+    Impossible(String),
+}
diff --git a/lang/docs/src/generate.rs b/lang/docs/src/generate.rs
index 77b1cc3b2..928038314 100644
--- a/lang/docs/src/generate.rs
+++ b/lang/docs/src/generate.rs
@@ -21,7 +21,7 @@ impl Generate for Ctor {
 
 impl Generate for Dtor {
     fn generate(&self) -> String {
-        let Dtor { span: _, doc, name, params, self_param, ret_typ } = self;
+        let Dtor { span: _, doc, name, params, self_param, ret_typ, erased: _ } = self;
         let self_parameter = self_param.print_html_to_string(Some(&PrintCfg::default()));
         let parmeter = params.print_html_to_string(Some(&PrintCfg::default()));
         let ret_typ = ret_typ.print_html_to_string(Some(&PrintCfg::default()));
diff --git a/lang/docs/src/generate_docs.rs b/lang/docs/src/generate_docs.rs
index c6b67712b..fa9d673e3 100644
--- a/lang/docs/src/generate_docs.rs
+++ b/lang/docs/src/generate_docs.rs
@@ -66,7 +66,8 @@ impl GenerateDocs for Codata {
 
 impl GenerateDocs for Def {
     fn generate_docs(&self) -> String {
-        let Def { span: _, doc, name, attr: _, params, self_param, ret_typ, cases } = self;
+        let Def { span: _, doc, name, attr: _, params, self_param, ret_typ, cases, erased: _ } =
+            self;
 
         let doc = if doc.is_none() { "".to_string() } else { format!("{}<br>", doc.generate()) };
         let name = &name.id;
@@ -114,7 +115,7 @@ impl GenerateDocs for Codef {
 
 impl GenerateDocs for Let {
     fn generate_docs(&self) -> String {
-        let Let { span: _, doc, name, attr: _, params, typ, body } = self;
+        let Let { span: _, doc, name, attr: _, params, typ, body, erased: _ } = self;
 
         let doc = if doc.is_none() { "".to_string() } else { format!("{}<br>", doc.generate()) };
         let name = &name.id;
diff --git a/lang/driver/src/info/collect.rs b/lang/driver/src/info/collect.rs
index 382f09a53..1aaebfbdc 100644
--- a/lang/driver/src/info/collect.rs
+++ b/lang/driver/src/info/collect.rs
@@ -220,7 +220,7 @@ impl CollectInfo for Ctor {
 
 impl CollectInfo for Dtor {
     fn collect_info(&self, db: &Database, collector: &mut InfoCollector) {
-        let Dtor { span, name, doc, self_param, params, ret_typ } = self;
+        let Dtor { span, name, doc, self_param, params, ret_typ, erased: _ } = self;
         if let Some(span) = span {
             // Add info
             let doc = doc.clone().map(|doc| doc.docs);
@@ -477,9 +477,9 @@ impl CollectInfo for Args {
 impl CollectInfo for Arg {
     fn collect_info(&self, db: &Database, collector: &mut InfoCollector) {
         match self {
-            Arg::UnnamedArg(exp) => exp.collect_info(db, collector),
-            Arg::NamedArg(_, exp) => exp.collect_info(db, collector),
-            Arg::InsertedImplicitArg(hole) => hole.collect_info(db, collector),
+            Arg::UnnamedArg { arg, .. } => arg.collect_info(db, collector),
+            Arg::NamedArg { arg, .. } => arg.collect_info(db, collector),
+            Arg::InsertedImplicitArg { hole, .. } => hole.collect_info(db, collector),
         }
     }
 }
diff --git a/lang/elaborator/src/normalizer/eval.rs b/lang/elaborator/src/normalizer/eval.rs
index dbdb5636f..ad41f42ad 100644
--- a/lang/elaborator/src/normalizer/eval.rs
+++ b/lang/elaborator/src/normalizer/eval.rs
@@ -457,11 +457,11 @@ impl Eval for Arg {
 
     fn eval(&self, info_table: &Rc<TypeInfoTable>, env: &mut Env) -> Result<Self::Val, TypeError> {
         match self {
-            Arg::UnnamedArg(exp) => Ok(val::Arg::UnnamedArg(exp.eval(info_table, env)?)),
-            Arg::NamedArg(name, exp) => {
-                Ok(val::Arg::NamedArg(name.clone(), exp.eval(info_table, env)?))
+            Arg::UnnamedArg { arg, .. } => Ok(val::Arg::UnnamedArg(arg.eval(info_table, env)?)),
+            Arg::NamedArg { name, arg, .. } => {
+                Ok(val::Arg::NamedArg(name.clone(), arg.eval(info_table, env)?))
             }
-            Arg::InsertedImplicitArg(hole) => {
+            Arg::InsertedImplicitArg { hole, .. } => {
                 Ok(val::Arg::InsertedImplicitArg(hole.eval(info_table, env)?))
             }
         }
diff --git a/lang/elaborator/src/normalizer/val.rs b/lang/elaborator/src/normalizer/val.rs
index 3bbdae24f..3e8316d4f 100644
--- a/lang/elaborator/src/normalizer/val.rs
+++ b/lang/elaborator/src/normalizer/val.rs
@@ -849,11 +849,17 @@ impl ReadBack for Arg {
 
     fn read_back(&self, info_table: &Rc<TypeInfoTable>) -> Result<Self::Nf, TypeError> {
         match self {
-            Arg::UnnamedArg(val) => Ok(ast::Arg::UnnamedArg(val.read_back(info_table)?)),
-            Arg::NamedArg(name, val) => {
-                Ok(ast::Arg::NamedArg(name.clone(), val.read_back(info_table)?))
+            Arg::UnnamedArg(val) => {
+                Ok(ast::Arg::UnnamedArg { arg: val.read_back(info_table)?, erased: false })
+            }
+            Arg::NamedArg(name, val) => Ok(ast::Arg::NamedArg {
+                name: name.clone(),
+                arg: val.read_back(info_table)?,
+                erased: false,
+            }),
+            Arg::InsertedImplicitArg(val) => {
+                Ok(ast::Arg::UnnamedArg { arg: val.read_back(info_table)?, erased: false })
             }
-            Arg::InsertedImplicitArg(val) => Ok(ast::Arg::UnnamedArg(val.read_back(info_table)?)),
         }
     }
 }
diff --git a/lang/elaborator/src/typechecker/decls/codatatype.rs b/lang/elaborator/src/typechecker/decls/codatatype.rs
index 65bc0d9d6..32e2aa67c 100644
--- a/lang/elaborator/src/typechecker/decls/codatatype.rs
+++ b/lang/elaborator/src/typechecker/decls/codatatype.rs
@@ -39,7 +39,7 @@ impl CheckToplevel for Codata {
 fn check_dtor_wf(codata_name: &IdBind, dtor: &Dtor, ctx: &mut Ctx) -> Result<Dtor, TypeError> {
     trace!("Checking well-formedness of destructor: {}", dtor.name);
 
-    let Dtor { span, doc, name, params, self_param, ret_typ } = dtor;
+    let Dtor { span, doc, name, params, self_param, ret_typ, erased } = dtor;
 
     // Check that the destructor lies in the codata type it is defined in
     if &self_param.typ.name != codata_name {
@@ -61,6 +61,7 @@ fn check_dtor_wf(codata_name: &IdBind, dtor: &Dtor, ctx: &mut Ctx) -> Result<Dto
                 params: params_out,
                 self_param: self_param_out,
                 ret_typ: ret_typ_out,
+                erased: *erased,
             })
         })
     })
diff --git a/lang/elaborator/src/typechecker/decls/definition.rs b/lang/elaborator/src/typechecker/decls/definition.rs
index 01a8773a7..269539017 100644
--- a/lang/elaborator/src/typechecker/decls/definition.rs
+++ b/lang/elaborator/src/typechecker/decls/definition.rs
@@ -19,7 +19,7 @@ impl CheckToplevel for Def {
     fn check_wf(&self, ctx: &mut Ctx) -> Result<Self, TypeError> {
         trace!("Checking well-formedness of definition: {}", self.name);
 
-        let Def { span, doc, name, attr, params, self_param, ret_typ, cases } = self;
+        let Def { span, doc, name, attr, params, self_param, ret_typ, cases, erased } = self;
 
         params.infer_telescope(ctx, |ctx, params_out| {
             let self_param_nf = self_param.typ.normalize(&ctx.type_info_table, &mut ctx.env())?;
@@ -45,6 +45,7 @@ impl CheckToplevel for Def {
                 self_param: self_param_out,
                 ret_typ: ret_typ_out,
                 cases,
+                erased: *erased,
             })
         })
     }
diff --git a/lang/elaborator/src/typechecker/decls/global_let.rs b/lang/elaborator/src/typechecker/decls/global_let.rs
index ae1df3512..845d550d0 100644
--- a/lang/elaborator/src/typechecker/decls/global_let.rs
+++ b/lang/elaborator/src/typechecker/decls/global_let.rs
@@ -17,7 +17,7 @@ impl CheckToplevel for Let {
     fn check_wf(&self, ctx: &mut Ctx) -> Result<Self, TypeError> {
         trace!("Checking well-formedness of global let: {}", self.name);
 
-        let Let { span, doc, name, attr, params, typ, body } = self;
+        let Let { span, doc, name, attr, params, typ, body, erased } = self;
 
         params.infer_telescope(ctx, |ctx, params_out| {
             let typ_out = typ.infer(ctx)?;
@@ -32,6 +32,7 @@ impl CheckToplevel for Let {
                 params: params_out,
                 typ: typ_out,
                 body: body_out,
+                erased: *erased,
             })
         })
     }
diff --git a/lang/elaborator/src/typechecker/exprs/local_comatch.rs b/lang/elaborator/src/typechecker/exprs/local_comatch.rs
index 801d3dc58..e34a446c6 100644
--- a/lang/elaborator/src/typechecker/exprs/local_comatch.rs
+++ b/lang/elaborator/src/typechecker/exprs/local_comatch.rs
@@ -224,15 +224,18 @@ impl WithExpectedType<'_> {
                                     let args = (0..*n_label_args)
                                         .rev()
                                         .map(|snd| {
-                                            Arg::UnnamedArg(Box::new(Exp::Variable(Variable {
-                                                span: None,
-                                                // The field `fst` has to be `2` because we have two surrounding telescopes:
-                                                // - The arguments to the toplevel codefinition
-                                                // - The arguments bound by the destructor copattern.
-                                                idx: Idx { fst: 2, snd },
-                                                name: VarBound::from_string(""),
-                                                inferred_type: None,
-                                            })))
+                                            Arg::UnnamedArg {
+                                                arg: Box::new(Exp::Variable(Variable {
+                                                    span: None,
+                                                    // The field `fst` has to be `2` because we have two surrounding telescopes:
+                                                    // - The arguments to the toplevel codefinition
+                                                    // - The arguments bound by the destructor copattern.
+                                                    idx: Idx { fst: 2, snd },
+                                                    name: VarBound::from_string(""),
+                                                    inferred_type: None,
+                                                })),
+                                                erased: false,
+                                            }
                                         })
                                         .collect();
                                     let ctor = Box::new(Exp::Call(Call {
diff --git a/lang/elaborator/src/typechecker/exprs/local_match.rs b/lang/elaborator/src/typechecker/exprs/local_match.rs
index 0fd957bd2..20a147fe6 100644
--- a/lang/elaborator/src/typechecker/exprs/local_match.rs
+++ b/lang/elaborator/src/typechecker/exprs/local_match.rs
@@ -73,6 +73,7 @@ impl CheckInfer for LocalMatch {
                         info: Some(self_t_nf),
                         name: param.name.clone(),
                         typ: Box::new(typ_app.to_exp()).into(),
+                        erased: param.erased,
                     },
                     ret_typ: ret_typ_out,
                 });
@@ -212,13 +213,14 @@ impl WithScrutineeType<'_> {
                     //
                     let args = (0..params.len())
                         .rev()
-                        .map(|snd| {
-                            Arg::UnnamedArg(Box::new(Exp::Variable(Variable {
+                        .map(|snd| Arg::UnnamedArg {
+                            arg: Box::new(Exp::Variable(Variable {
                                 span: None,
                                 idx: Idx { fst: 1, snd },
                                 name: VarBound::from_string(""),
                                 inferred_type: None,
-                            })))
+                            })),
+                            erased: false,
                         })
                         .collect();
                     let ctor = Box::new(Exp::Call(Call {
diff --git a/lang/elaborator/src/typechecker/exprs/mod.rs b/lang/elaborator/src/typechecker/exprs/mod.rs
index 46472ad64..57fcee948 100644
--- a/lang/elaborator/src/typechecker/exprs/mod.rs
+++ b/lang/elaborator/src/typechecker/exprs/mod.rs
@@ -103,17 +103,29 @@ impl CheckInfer for Exp {
 impl CheckInfer for Arg {
     fn check(&self, ctx: &mut Ctx, t: &Exp) -> Result<Self, TypeError> {
         match self {
-            Arg::UnnamedArg(exp) => Ok(Arg::UnnamedArg(exp.check(ctx, t)?)),
-            Arg::NamedArg(name, exp) => Ok(Arg::NamedArg(name.clone(), exp.check(ctx, t)?)),
-            Arg::InsertedImplicitArg(hole) => Ok(Arg::InsertedImplicitArg(hole.check(ctx, t)?)),
+            Arg::UnnamedArg { arg, erased } => {
+                Ok(Arg::UnnamedArg { arg: arg.check(ctx, t)?, erased: *erased })
+            }
+            Arg::NamedArg { name, arg, erased } => {
+                Ok(Arg::NamedArg { name: name.clone(), arg: arg.check(ctx, t)?, erased: *erased })
+            }
+            Arg::InsertedImplicitArg { hole, erased } => {
+                Ok(Arg::InsertedImplicitArg { hole: hole.check(ctx, t)?, erased: *erased })
+            }
         }
     }
 
     fn infer(&self, ctx: &mut Ctx) -> Result<Self, TypeError> {
         match self {
-            Arg::UnnamedArg(exp) => Ok(Arg::UnnamedArg(exp.infer(ctx)?)),
-            Arg::NamedArg(name, exp) => Ok(Arg::NamedArg(name.clone(), exp.infer(ctx)?)),
-            Arg::InsertedImplicitArg(hole) => Ok(Arg::InsertedImplicitArg(hole.infer(ctx)?)),
+            Arg::UnnamedArg { arg, erased } => {
+                Ok(Arg::UnnamedArg { arg: arg.infer(ctx)?, erased: *erased })
+            }
+            Arg::NamedArg { name, arg, erased } => {
+                Ok(Arg::NamedArg { name: name.clone(), arg: arg.infer(ctx)?, erased: *erased })
+            }
+            Arg::InsertedImplicitArg { hole, erased } => {
+                Ok(Arg::InsertedImplicitArg { hole: hole.infer(ctx)?, erased: *erased })
+            }
         }
     }
 }
@@ -203,7 +215,7 @@ impl CheckTelescope for TelescopeInst {
             vec![],
             |ctx, params_out, (param_actual, param_expected)| {
                 let ParamInst { span, name, .. } = param_actual;
-                let Param { typ, .. } = param_expected;
+                let Param { typ, erased, .. } = param_expected;
                 let typ_out = typ.check(ctx, &Box::new(TypeUniv::new().into()))?;
                 let typ_nf = typ.normalize(&ctx.type_info_table, &mut ctx.env())?;
                 let mut params_out = params_out;
@@ -212,6 +224,7 @@ impl CheckTelescope for TelescopeInst {
                     info: Some(typ_nf.clone()),
                     name: name.clone(),
                     typ: typ_out.into(),
+                    erased: *erased,
                 };
                 params_out.push(param_out);
                 let elem = Binder { name: param_actual.name.clone(), typ: typ_nf };
@@ -236,10 +249,15 @@ impl InferTelescope for Telescope {
             params.iter(),
             vec![],
             |ctx, mut params_out, param| {
-                let Param { implicit, typ, name } = param;
+                let Param { implicit, typ, name, erased } = param;
                 let typ_out = typ.check(ctx, &Box::new(TypeUniv::new().into()))?;
                 let typ_nf = typ.normalize(&ctx.type_info_table, &mut ctx.env())?;
-                let param_out = Param { implicit: *implicit, name: name.clone(), typ: typ_out };
+                let param_out = Param {
+                    implicit: *implicit,
+                    name: name.clone(),
+                    typ: typ_out,
+                    erased: *erased,
+                };
                 params_out.push(param_out);
                 let elem = Binder { name: param.name.clone(), typ: typ_nf };
                 Result::<_, TypeError>::Ok(BindElem { elem, ret: params_out })
diff --git a/lang/lowering/src/lower/decls/codata_declaration.rs b/lang/lowering/src/lower/decls/codata_declaration.rs
index 8e526b48b..edd7e888e 100644
--- a/lang/lowering/src/lower/decls/codata_declaration.rs
+++ b/lang/lowering/src/lower/decls/codata_declaration.rs
@@ -74,6 +74,7 @@ fn lower_destructor(
                 params,
                 self_param,
                 ret_typ: ret_typ.lower(ctx)?,
+                erased: false,
             })
         })
     })
diff --git a/lang/lowering/src/lower/decls/definition.rs b/lang/lowering/src/lower/decls/definition.rs
index 792318171..42b7f97ae 100644
--- a/lang/lowering/src/lower/decls/definition.rs
+++ b/lang/lowering/src/lower/decls/definition.rs
@@ -27,6 +27,7 @@ impl Lower for cst::decls::Def {
                     self_param,
                     ret_typ: ret_typ.lower(ctx)?,
                     cases,
+                    erased: false,
                 })
             })
         })
diff --git a/lang/lowering/src/lower/decls/mod.rs b/lang/lowering/src/lower/decls/mod.rs
index 2a94f947a..0da744e88 100644
--- a/lang/lowering/src/lower/decls/mod.rs
+++ b/lang/lowering/src/lower/decls/mod.rs
@@ -161,7 +161,7 @@ where
                 }
             };
             let name = VarBind { span: Some(name.span), id: name.id.clone() };
-            let param_out = ast::Param { implicit: *implicit, name, typ: typ_out };
+            let param_out = ast::Param { implicit: *implicit, name, typ: typ_out, erased: false };
             params_out.push(param_out);
             Ok(params_out)
         },
diff --git a/lang/lowering/src/lower/decls/toplevel_let.rs b/lang/lowering/src/lower/decls/toplevel_let.rs
index ccd3b44ee..623f1629f 100644
--- a/lang/lowering/src/lower/decls/toplevel_let.rs
+++ b/lang/lowering/src/lower/decls/toplevel_let.rs
@@ -21,6 +21,7 @@ impl Lower for cst::decls::Let {
                 params,
                 typ: typ.lower(ctx)?,
                 body: body.lower(ctx)?,
+                erased: false,
             })
         })
     }
diff --git a/lang/lowering/src/lower/exp/mod.rs b/lang/lowering/src/lower/exp/mod.rs
index 3811374ef..7b33607e6 100644
--- a/lang/lowering/src/lower/exp/mod.rs
+++ b/lang/lowering/src/lower/exp/mod.rs
@@ -56,6 +56,7 @@ fn lower_telescope_inst<T, F: FnOnce(&mut Ctx, ast::TelescopeInst) -> Result<T,
                 info: None,
                 name: VarBind { span: Some(span), id: name.id.clone() },
                 typ: None,
+                erased: false,
             };
             params_out.push(param_out);
             Ok(params_out)
@@ -160,7 +161,7 @@ fn lower_args(
         };
         match arg {
             cst::exp::Arg::UnnamedArg(exp) => {
-                args_out.push(ast::Arg::UnnamedArg(exp.lower(ctx)?));
+                args_out.push(ast::Arg::UnnamedArg { arg: exp.lower(ctx)?, erased: false });
             }
             cst::exp::Arg::NamedArg(name, exp) => {
                 let expected_name = match &expected_bs {
@@ -180,7 +181,7 @@ fn lower_args(
                     });
                 }
                 let name = VarBound { span: Some(name.span), id: name.id.clone() };
-                args_out.push(ast::Arg::NamedArg(name, exp.lower(ctx)?));
+                args_out.push(ast::Arg::NamedArg { name, arg: exp.lower(ctx)?, erased: false });
             }
         }
         Ok(())
@@ -216,7 +217,7 @@ fn lower_args(
                     solution: None,
                 };
 
-                args_out.push(ast::Arg::InsertedImplicitArg(hole));
+                args_out.push(ast::Arg::InsertedImplicitArg { hole, erased: false });
             } else {
                 pop_arg(span, &mut given_iter, expected_bs, &mut args_out, ctx)?;
             }
@@ -503,7 +504,9 @@ impl Lower for cst::exp::NatLit {
                 span: Some(*span),
                 kind: call_kind,
                 name: ast::IdBound { span: Some(*span), id: "S".to_owned(), uri: uri.clone() },
-                args: ast::Args { args: vec![ast::Arg::UnnamedArg(Box::new(out))] },
+                args: ast::Args {
+                    args: vec![ast::Arg::UnnamedArg { arg: Box::new(out), erased: false }],
+                },
                 inferred_type: None,
             });
         }
@@ -522,8 +525,8 @@ impl Lower for cst::exp::Fun {
             name: ast::IdBound { span: Some(*span), id: "Fun".to_owned(), uri: uri.clone() },
             args: ast::Args {
                 args: vec![
-                    ast::Arg::UnnamedArg(from.lower(ctx)?),
-                    ast::Arg::UnnamedArg(to.lower(ctx)?),
+                    ast::Arg::UnnamedArg { arg: from.lower(ctx)?, erased: false },
+                    ast::Arg::UnnamedArg { arg: to.lower(ctx)?, erased: false },
                 ],
             },
         }
@@ -586,6 +589,7 @@ impl Lower for cst::exp::Motive {
                 info: None,
                 name: ast::VarBind { span: Some(bs_to_span(param)), id: bs_to_name(param).id },
                 typ: None,
+                erased: false,
             },
             ret_typ: ctx.bind_single(param, |ctx| ret_typ.lower(ctx))?,
         })
diff --git a/lang/transformations/src/lifting/fv.rs b/lang/transformations/src/lifting/fv.rs
index 62c2dbeb8..c8a79fc15 100644
--- a/lang/transformations/src/lifting/fv.rs
+++ b/lang/transformations/src/lifting/fv.rs
@@ -101,9 +101,9 @@ impl FV for Args {
 impl FV for Arg {
     fn visit_fv(&self, v: &mut USTVisitor) {
         match self {
-            Arg::UnnamedArg(exp) => exp.visit_fv(v),
-            Arg::NamedArg(_, exp) => exp.visit_fv(v),
-            Arg::InsertedImplicitArg(hole) => hole.visit_fv(v),
+            Arg::UnnamedArg { arg, .. } => arg.visit_fv(v),
+            Arg::NamedArg { arg, .. } => arg.visit_fv(v),
+            Arg::InsertedImplicitArg { hole, .. } => hole.visit_fv(v),
         }
     }
 }
@@ -194,14 +194,21 @@ impl FreeVars {
 
             let typ = typ.subst(&mut ctx, &subst.in_param());
 
-            let param =
-                Param { implicit: false, name: VarBind::from_string(&name), typ: typ.clone() };
-            let arg = Arg::UnnamedArg(Box::new(Exp::Variable(Variable {
-                span: None,
-                idx: base_ctx.lvl_to_idx(fv.lvl),
-                name: VarBound::from_string(&name),
-                inferred_type: None,
-            })));
+            let param = Param {
+                implicit: false,
+                name: VarBind::from_string(&name),
+                typ: typ.clone(),
+                erased: false,
+            };
+            let arg = Arg::UnnamedArg {
+                arg: Box::new(Exp::Variable(Variable {
+                    span: None,
+                    idx: base_ctx.lvl_to_idx(fv.lvl),
+                    name: VarBound::from_string(&name),
+                    inferred_type: None,
+                })),
+                erased: false,
+            };
             args.push(arg);
             params.push(param);
             subst.add(name, lvl);
diff --git a/lang/transformations/src/lifting/mod.rs b/lang/transformations/src/lifting/mod.rs
index 8c4f5c8dd..82c6a4adf 100644
--- a/lang/transformations/src/lifting/mod.rs
+++ b/lang/transformations/src/lifting/mod.rs
@@ -169,14 +169,22 @@ impl Lift for Dtor {
     type Target = Dtor;
 
     fn lift(&self, ctx: &mut Ctx) -> Self::Target {
-        let Dtor { span, doc, name, params, self_param, ret_typ } = self;
+        let Dtor { span, doc, name, params, self_param, ret_typ, erased } = self;
 
         params.lift_telescope(ctx, |ctx, params| {
             let (self_param, ret_typ) = self_param.lift_telescope(ctx, |ctx, self_param| {
                 let ret_typ = ret_typ.lift(ctx);
                 (self_param, ret_typ)
             });
-            Dtor { span: *span, doc: doc.clone(), name: name.clone(), params, self_param, ret_typ }
+            Dtor {
+                span: *span,
+                doc: doc.clone(),
+                name: name.clone(),
+                params,
+                self_param,
+                ret_typ,
+                erased: *erased,
+            }
         })
     }
 }
@@ -185,7 +193,7 @@ impl Lift for Def {
     type Target = Def;
 
     fn lift(&self, ctx: &mut Ctx) -> Self::Target {
-        let Def { span, doc, name, attr, params, self_param, ret_typ, cases } = self;
+        let Def { span, doc, name, attr, params, self_param, ret_typ, cases, erased } = self;
 
         params.lift_telescope(ctx, |ctx, params| {
             let (self_param, ret_typ) = self_param.lift_telescope(ctx, |ctx, self_param| {
@@ -202,6 +210,7 @@ impl Lift for Def {
                 self_param,
                 ret_typ,
                 cases: cases.lift(ctx),
+                erased: *erased,
             }
         })
     }
@@ -229,7 +238,7 @@ impl Lift for Let {
     type Target = Let;
 
     fn lift(&self, ctx: &mut Ctx) -> Self::Target {
-        let Let { span, doc, name, attr, params, typ, body } = self;
+        let Let { span, doc, name, attr, params, typ, body, erased } = self;
 
         params.lift_telescope(ctx, |ctx, params| Let {
             span: *span,
@@ -239,6 +248,7 @@ impl Lift for Let {
             params,
             typ: typ.lift(ctx),
             body: body.lift(ctx),
+            erased: *erased,
         })
     }
 }
@@ -479,9 +489,15 @@ impl Lift for Arg {
 
     fn lift(&self, ctx: &mut Ctx) -> Self::Target {
         match self {
-            Arg::UnnamedArg(exp) => Arg::UnnamedArg(exp.lift(ctx)),
-            Arg::NamedArg(name, exp) => Arg::NamedArg(name.clone(), exp.lift(ctx)),
-            Arg::InsertedImplicitArg(hole) => Arg::InsertedImplicitArg(hole.lift(ctx)),
+            Arg::UnnamedArg { arg, erased } => {
+                Arg::UnnamedArg { arg: arg.lift(ctx), erased: *erased }
+            }
+            Arg::NamedArg { name, arg, erased } => {
+                Arg::NamedArg { name: name.clone(), arg: arg.lift(ctx), erased: *erased }
+            }
+            Arg::InsertedImplicitArg { hole, erased } => {
+                Arg::InsertedImplicitArg { hole: hole.lift(ctx), erased: *erased }
+            }
         }
     }
 }
@@ -490,9 +506,9 @@ impl Lift for Param {
     type Target = Param;
 
     fn lift(&self, ctx: &mut Ctx) -> Self::Target {
-        let Param { implicit, name, typ } = self;
+        let Param { implicit, name, typ, erased } = self;
 
-        Param { implicit: *implicit, name: name.clone(), typ: typ.lift(ctx) }
+        Param { implicit: *implicit, name: name.clone(), typ: typ.lift(ctx), erased: *erased }
     }
 }
 
@@ -500,9 +516,9 @@ impl Lift for ParamInst {
     type Target = ParamInst;
 
     fn lift(&self, _ctx: &mut Ctx) -> Self::Target {
-        let ParamInst { span, name, typ: _, .. } = self;
+        let ParamInst { span, name, typ: _, erased, .. } = self;
 
-        ParamInst { span: *span, info: None, name: name.clone(), typ: None }
+        ParamInst { span: *span, info: None, name: name.clone(), typ: None, erased: *erased }
     }
 }
 
@@ -602,6 +618,7 @@ impl Ctx {
             },
             ret_typ: def_ret_typ,
             cases,
+            erased: false,
         };
 
         self.new_decls.push(Decl::Def(def));
diff --git a/lang/transformations/src/renaming/ast.rs b/lang/transformations/src/renaming/ast.rs
index b3a50d513..df9d6c9a3 100644
--- a/lang/transformations/src/renaming/ast.rs
+++ b/lang/transformations/src/renaming/ast.rs
@@ -279,9 +279,9 @@ impl Rename for Args {
 impl Rename for Arg {
     fn rename_in_ctx(&mut self, ctx: &mut Ctx) {
         match self {
-            Arg::UnnamedArg(exp) => exp.rename_in_ctx(ctx),
-            Arg::NamedArg(_name, exp) => exp.rename_in_ctx(ctx),
-            Arg::InsertedImplicitArg(hole) => hole.rename_in_ctx(ctx),
+            Arg::UnnamedArg { arg, .. } => arg.rename_in_ctx(ctx),
+            Arg::NamedArg { arg, .. } => arg.rename_in_ctx(ctx),
+            Arg::InsertedImplicitArg { hole, .. } => hole.rename_in_ctx(ctx),
         }
     }
 }
diff --git a/lang/transformations/src/xfunc/matrix.rs b/lang/transformations/src/xfunc/matrix.rs
index 9676bc8e2..71bf1838c 100644
--- a/lang/transformations/src/xfunc/matrix.rs
+++ b/lang/transformations/src/xfunc/matrix.rs
@@ -220,6 +220,7 @@ impl XData {
                     self_param: dtor.self_param.clone(),
                     ret_typ: dtor.ret_typ.clone(),
                     cases,
+                    erased: false,
                 }
             })
             .collect();