diff --git a/Cargo.lock b/Cargo.lock
index 1b9aeab97b7..f87cfd29157 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4,9 +4,9 @@ version = 3
 
 [[package]]
 name = "aho-corasick"
-version = "0.7.13"
+version = "0.7.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "043164d8ba5c4c3035fec9bbee8647c0261d788f3474306f93bb65901cae0e86"
+checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f"
 dependencies = [
  "memchr",
 ]
@@ -29,23 +29,11 @@ dependencies = [
  "winapi",
 ]
 
-[[package]]
-name = "arrayref"
-version = "0.3.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a4c527152e37cf757a3f78aae5a06fbeefdb07ccc535c980a3208ee3060dd544"
-
-[[package]]
-name = "arrayvec"
-version = "0.5.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cff77d8686867eceff3105329d4698d96c2391c176d5d03adc90c7389162b5b8"
-
 [[package]]
 name = "ascii-canvas"
-version = "2.0.0"
+version = "3.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ff8eb72df928aafb99fe5d37b383f2fe25bd2a765e3e5f7c365916b6f2463a29"
+checksum = "8824ecca2e851cec16968d54a01dd372ef8f95b244fb84b84e70128be347c3c6"
 dependencies = [
  "term",
 ]
@@ -63,15 +51,9 @@ dependencies = [
 
 [[package]]
 name = "autocfg"
-version = "1.0.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f8aac770f1885fd7e387acedd76065302551364496e46b3dd00860b2f8359b9d"
-
-[[package]]
-name = "base64"
-version = "0.11.0"
+version = "1.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b41b7ea54a0c9d92199de89e20e58d49f02f8e699814ef3fdf266f6f748d15c7"
+checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a"
 
 [[package]]
 name = "bit-set"
@@ -84,71 +66,21 @@ dependencies = [
 
 [[package]]
 name = "bit-vec"
-version = "0.6.2"
+version = "0.6.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5f0dc55f2d8a1a85650ac47858bb001b4c0dd73d79e3c455a842925e68d29cd3"
+checksum = "349f9b6a179ed607305526ca489b34ad0a41aed5f7980fa90eb03160b69598fb"
 
 [[package]]
 name = "bitflags"
-version = "1.2.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693"
-
-[[package]]
-name = "blake2b_simd"
-version = "0.5.10"
+version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d8fb2d74254a3a0b5cac33ac9f8ed0e44aa50378d9dbb2e5d83bd21ed1dc2c8a"
-dependencies = [
- "arrayref",
- "arrayvec",
- "constant_time_eq",
-]
-
-[[package]]
-name = "block-buffer"
-version = "0.7.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c0940dc441f31689269e10ac70eb1002a3a1d3ad1390e030043662eb7fe4688b"
-dependencies = [
- "block-padding",
- "byte-tools",
- "byteorder",
- "generic-array",
-]
-
-[[package]]
-name = "block-padding"
-version = "0.1.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fa79dedbb091f449f1f39e53edf88d5dbe95f895dae6135a8d7b881fb5af73f5"
-dependencies = [
- "byte-tools",
-]
-
-[[package]]
-name = "byte-tools"
-version = "0.3.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e3b5ca7a04898ad4bcd41c90c5285445ff5b791899bb1b0abdd2a2aa791211d7"
-
-[[package]]
-name = "byteorder"
-version = "1.3.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "08c48aae112d48ed9f069b33538ea9e3e90aa263cfa3d1c24309612b1f7472de"
+checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
 [[package]]
 name = "cc"
-version = "1.0.58"
+version = "1.0.70"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f9a06fb2e53271d7c279ec1efea6ab691c35a2ae67ec0d91d7acec0caf13b518"
-
-[[package]]
-name = "cfg-if"
-version = "0.1.10"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822"
+checksum = "d26a6ce4b6a484fa3edb70f7efa6fc430fd2b87285fe8b84304fd0936faa0dc0"
 
 [[package]]
 name = "cfg-if"
@@ -169,7 +101,7 @@ dependencies = [
  "chalk-solve",
  "diff",
  "docopt",
- "itertools 0.10.0",
+ "itertools",
  "pretty_assertions",
  "regex",
  "rustyline",
@@ -254,7 +186,7 @@ dependencies = [
  "chalk-integration",
  "chalk-ir",
  "ena",
- "itertools 0.10.0",
+ "itertools",
  "petgraph",
  "rustc-hash",
  "tracing",
@@ -264,56 +196,36 @@ dependencies = [
 
 [[package]]
 name = "chrono"
-version = "0.4.13"
+version = "0.4.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c74d84029116787153e02106bf53e66828452a4b325cc8652b788b5967c0a0b6"
+checksum = "670ad68c9088c2a963aaa298cb369688cf3f9465ce5e2d4ca10e6e0098a1ce73"
 dependencies = [
+ "libc",
  "num-integer",
  "num-traits",
- "time",
-]
-
-[[package]]
-name = "cloudabi"
-version = "0.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4344512281c643ae7638bbabc3af17a11307803ec8f0fcad9fae512a8bf36467"
-dependencies = [
- "bitflags",
+ "winapi",
 ]
 
-[[package]]
-name = "constant_time_eq"
-version = "0.1.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "245097e9a4535ee1e3e3931fcfcd55a796a44c643e8596ff6566d68f09b87bbc"
-
 [[package]]
 name = "crossbeam-utils"
-version = "0.7.2"
+version = "0.8.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c3c7c73a2d1e9fc0886a08b93e98eb643461230d5f1925e4036204d5f2e261a8"
+checksum = "d82cfc11ce7f2c3faef78d8a684447b40d503d9681acebed6cb728d45940c4db"
 dependencies = [
- "autocfg",
- "cfg-if 0.1.10",
- "lazy_static",
+ "cfg-if",
 ]
 
 [[package]]
-name = "crossbeam-utils"
-version = "0.8.3"
+name = "crunchy"
+version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e7e9d99fa91428effe99c5c6d4634cdeba32b8cf784fc428a2a687f61a952c49"
-dependencies = [
- "autocfg",
- "cfg-if 1.0.0",
-]
+checksum = "7a81dae078cea95a014a339291cec439d2f232ebe854a9d672b796c6afafa9b7"
 
 [[package]]
 name = "ctor"
-version = "0.1.15"
+version = "0.1.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "39858aa5bac06462d4dd4b9164848eb81ffc4aa5c479746393598fd193afa227"
+checksum = "ccc0a48a9b826acdf4028595adc9db92caea352f7af011a3034acd172a52a0aa"
 dependencies = [
  "quote",
  "syn",
@@ -332,19 +244,20 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "524cbf6897b527295dff137cec09ecf3a05f4fddffd7dfcd1585403449e74198"
 
 [[package]]
-name = "digest"
-version = "0.8.1"
+name = "dirs-next"
+version = "2.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f3d0c8c8752312f9713efd397ff63acb9f85585afbf179282e720e7704954dd5"
+checksum = "b98cf8ebf19c3d1b223e151f99a4f9f0690dca41414773390fc824184ac833e1"
 dependencies = [
- "generic-array",
+ "cfg-if",
+ "dirs-sys-next",
 ]
 
 [[package]]
-name = "dirs"
-version = "1.0.5"
+name = "dirs-sys-next"
+version = "0.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3fd78930633bd1c6e35c4b42b1df7b0cbc6bc191146e512bb3bedf243fcc3901"
+checksum = "4ebda144c4fe02d1f7ea1a7d9641b6fc6b580adcfa024ae48797ecdeb6825b4d"
 dependencies = [
  "libc",
  "redox_users",
@@ -353,9 +266,9 @@ dependencies = [
 
 [[package]]
 name = "docopt"
-version = "1.1.0"
+version = "1.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7f525a586d310c87df72ebcd98009e57f1cc030c8c268305287a476beb653969"
+checksum = "7f3f119846c823f9eafcf953a8f6ffb6ed69bf6240883261a7f13b634579a51f"
 dependencies = [
  "lazy_static",
  "regex",
@@ -365,9 +278,9 @@ dependencies = [
 
 [[package]]
 name = "either"
-version = "1.6.0"
+version = "1.6.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cd56b59865bce947ac5958779cfa508f6c3b9497cc762b7e24a12d11ccde2c4f"
+checksum = "e78d4f1cc4ae33bbfc157ed5d5a5ef3bc29227303d595861deb238fcec4e9457"
 
 [[package]]
 name = "ena"
@@ -378,12 +291,6 @@ dependencies = [
  "log",
 ]
 
-[[package]]
-name = "fake-simd"
-version = "0.1.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e88a8acf291dafb59c2d96e8f59828f3838bb1a70398823ade51a84de6a6deed"
-
 [[package]]
 name = "fixedbitset"
 version = "0.2.0"
@@ -400,58 +307,46 @@ dependencies = [
  "winapi",
 ]
 
-[[package]]
-name = "generic-array"
-version = "0.12.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
-dependencies = [
- "typenum",
-]
-
 [[package]]
 name = "getrandom"
-version = "0.1.14"
+version = "0.2.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7abc8dd8451921606d809ba32e95b6111925cd2906060d2dcc29c070220503eb"
+checksum = "7fcd999463524c52659517fe2cea98493cfe485d10565e7b0fb07dbba7ad2753"
 dependencies = [
- "cfg-if 0.1.10",
+ "cfg-if",
  "libc",
  "wasi",
 ]
 
 [[package]]
 name = "hashbrown"
-version = "0.8.2"
+version = "0.11.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e91b62f79061a0bc2e046024cb7ba44b08419ed238ecbd9adbd787434b9e8c25"
-dependencies = [
- "autocfg",
-]
+checksum = "ab5ef0d4909ef3724cc8cce6ccc8572c5c817592e9285f5464f8e86f8bd3726e"
 
 [[package]]
 name = "heck"
-version = "0.3.1"
+version = "0.3.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "20564e78d53d2bb135c343b3f47714a56af2061f1c928fdb541dc7b9fdd94205"
+checksum = "6d621efb26863f0e9924c6ac577e8275e5e6b77455db64ffa6c65c904e9e132c"
 dependencies = [
  "unicode-segmentation",
 ]
 
 [[package]]
 name = "hermit-abi"
-version = "0.1.15"
+version = "0.1.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3deed196b6e7f9e44a2ae8d94225d80302d81208b1bb673fd21fe634645c85a9"
+checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
 dependencies = [
  "libc",
 ]
 
 [[package]]
 name = "indexmap"
-version = "1.5.1"
+version = "1.7.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "86b45e59b16c76b11bf9738fd5d38879d3bd28ad292d7b313608becb17ae2df9"
+checksum = "bc633605454125dec4b66843673f01c7df2b89479b32e0ed634e43a91cff62a5"
 dependencies = [
  "autocfg",
  "hashbrown",
@@ -459,64 +354,56 @@ dependencies = [
 
 [[package]]
 name = "instant"
-version = "0.1.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5b141fdc7836c525d4d594027d318c84161ca17aaf8113ab1f81ab93ae897485"
-
-[[package]]
-name = "itertools"
-version = "0.9.0"
+version = "0.1.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "284f18f85651fe11e8a991b2adb42cb078325c996ed026d994719efcfca1d54b"
+checksum = "bee0328b1209d157ef001c94dd85b4f8f64139adb0eac2659f4b08382b2f474d"
 dependencies = [
- "either",
+ "cfg-if",
 ]
 
 [[package]]
 name = "itertools"
-version = "0.10.0"
+version = "0.10.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "37d572918e350e82412fe766d24b15e6682fb2ed2bbe018280caa810397cb319"
+checksum = "69ddb889f9d0d08a67338271fa9b62996bc788c7796a5c18cf057420aaed5eaf"
 dependencies = [
  "either",
 ]
 
 [[package]]
 name = "itoa"
-version = "0.4.6"
+version = "0.4.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dc6f3ad7b9d11a0c00842ff8de1b60ee58661048eb8049ed33c73594f359d7e6"
+checksum = "b71991ff56294aa922b450139ee08b3bfc70982c6b2c7562771375cf73542dd4"
 
 [[package]]
 name = "lalrpop"
-version = "0.19.0"
+version = "0.19.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d6f55673d283313791404be21209bb433f128f7e5c451986df107eb5fdbd68d2"
+checksum = "b15174f1c529af5bf1283c3bc0058266b483a67156f79589fab2a25e23cf8988"
 dependencies = [
  "ascii-canvas",
  "atty",
  "bit-set",
  "diff",
- "docopt",
  "ena",
- "itertools 0.9.0",
+ "itertools",
  "lalrpop-util",
  "petgraph",
+ "pico-args",
  "regex",
  "regex-syntax",
- "serde",
- "serde_derive",
- "sha2",
  "string_cache",
  "term",
+ "tiny-keccak",
  "unicode-xid",
 ]
 
 [[package]]
 name = "lalrpop-util"
-version = "0.19.0"
+version = "0.19.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f7e88f15a7d31dfa8fb607986819039127f0161058a3b248a146142d276cbd28"
+checksum = "d3e58cce361efcc90ba8a0a5f982c741ff86b603495bb15a998412e957dcd278"
 dependencies = [
  "regex",
 ]
@@ -529,26 +416,26 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
 
 [[package]]
 name = "libc"
-version = "0.2.86"
+version = "0.2.101"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7282d924be3275cec7f6756ff4121987bc6481325397dde6ba3e7802b1a8b1c"
+checksum = "3cb00336871be5ed2c8ed44b60ae9959dc5b9f08539422ed43f09e34ecaeba21"
 
 [[package]]
 name = "lock_api"
-version = "0.4.1"
+version = "0.4.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "28247cc5a5be2f05fbcd76dd0cf2c7d3b5400cb978a28042abcd4fa0b3f8261c"
+checksum = "712a4d093c9976e24e7dbca41db895dabcbac38eb5f4045393d17a95bdfb1109"
 dependencies = [
  "scopeguard",
 ]
 
 [[package]]
 name = "log"
-version = "0.4.11"
+version = "0.4.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4fabed175da42fed1fa0746b0ea71f412aa9d35e76e95e59b192c64b9dc2bf8b"
+checksum = "51b9bbe6c47d51fc3e1a9b945965946b4c44142ab8792c50835a980d362c2710"
 dependencies = [
- "cfg-if 0.1.10",
+ "cfg-if",
 ]
 
 [[package]]
@@ -562,9 +449,9 @@ dependencies = [
 
 [[package]]
 name = "memchr"
-version = "2.3.3"
+version = "2.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3728d817d99e5ac407411fa471ff9800a778d88a24685968b36824eaf4bee400"
+checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a"
 
 [[package]]
 name = "new_debug_unreachable"
@@ -580,15 +467,15 @@ checksum = "b2ccba0cfe4fdf15982d1674c69b1fd80bad427d293849982668dfe454bd61f2"
 dependencies = [
  "bitflags",
  "cc",
- "cfg-if 1.0.0",
+ "cfg-if",
  "libc",
 ]
 
 [[package]]
 name = "num-integer"
-version = "0.1.43"
+version = "0.1.44"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8d59457e662d541ba17869cf51cf177c0b5f0cbf476c66bdc90bf1edac4f875b"
+checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
 dependencies = [
  "autocfg",
  "num-traits",
@@ -596,24 +483,24 @@ dependencies = [
 
 [[package]]
 name = "num-traits"
-version = "0.2.12"
+version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ac267bcc07f48ee5f8935ab0d24f316fb722d7a1292e2913f0cc196b29ffd611"
+checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290"
 dependencies = [
  "autocfg",
 ]
 
 [[package]]
-name = "oorandom"
-version = "11.1.2"
+name = "once_cell"
+version = "1.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a170cebd8021a008ea92e4db85a72f80b35df514ec664b296fdcbb654eac0b2c"
+checksum = "692fcb63b64b1758029e0a96ee63e049ce8c5948587f2f7208df04625e5f6b56"
 
 [[package]]
-name = "opaque-debug"
-version = "0.2.3"
+name = "oorandom"
+version = "11.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2839e79665f131bdb5782e51f2c6c9599c133c6098982a54c794358bf432529c"
+checksum = "0ab1bc2a289d34bd04a330323ac98a1b4bc82c9d9fcb1e66b63caa84da26b575"
 
 [[package]]
 name = "output_vt100"
@@ -626,9 +513,9 @@ dependencies = [
 
 [[package]]
 name = "parking_lot"
-version = "0.11.0"
+version = "0.11.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a4893845fa2ca272e647da5d0e46660a314ead9c2fdd9a883aabc32e481a8733"
+checksum = "7d17b78036a60663b797adeaee46f5c9dfebb86948d1255007a1d6be0271ff99"
 dependencies = [
  "instant",
  "lock_api",
@@ -637,12 +524,11 @@ dependencies = [
 
 [[package]]
 name = "parking_lot_core"
-version = "0.8.0"
+version = "0.8.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c361aa727dd08437f2f1447be8b59a33b0edd15e0fcee698f935613d9efbca9b"
+checksum = "d76e8e1493bcac0d2766c42737f34458f1c8c50c0d23bcb24ea953affb273216"
 dependencies = [
- "cfg-if 0.1.10",
- "cloudabi",
+ "cfg-if",
  "instant",
  "libc",
  "redox_syscall",
@@ -669,6 +555,18 @@ dependencies = [
  "siphasher",
 ]
 
+[[package]]
+name = "pico-args"
+version = "0.4.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "db8bcd96cb740d03149cbad5518db9fd87126a10ab519c011893b1754134c468"
+
+[[package]]
+name = "pin-project-lite"
+version = "0.2.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8d31d11c69a6b52a174b42bdc0c30e5e11670f90788b2c471c31c1d17d449443"
+
 [[package]]
 name = "precomputed-hash"
 version = "0.1.1"
@@ -689,78 +587,66 @@ dependencies = [
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.19"
+version = "1.0.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "04f5f085b5d71e2188cb8271e5da0161ad52c3f227a661a3c135fdf28e258b12"
+checksum = "b9f5105d4fdaab20335ca9565e106a5d9b82b6219b5ba735731124ac6711d23d"
 dependencies = [
  "unicode-xid",
 ]
 
 [[package]]
 name = "quote"
-version = "1.0.7"
+version = "1.0.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aa563d17ecb180e500da1cfd2b028310ac758de548efdd203e18f283af693f37"
+checksum = "c3d0b9745dc2debf507c8422de05d7226cc1f0644216dfdfead988f9b1ab32a7"
 dependencies = [
  "proc-macro2",
 ]
 
 [[package]]
 name = "redox_syscall"
-version = "0.1.57"
+version = "0.2.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41cc0f7e4d5d4544e8861606a285bb08d3e70712ccc7d2b84d7c0ccfaf4b05ce"
+checksum = "8383f39639269cde97d255a32bdb68c047337295414940c68bdd30c2e13203ff"
+dependencies = [
+ "bitflags",
+]
 
 [[package]]
 name = "redox_users"
-version = "0.3.4"
+version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09b23093265f8d200fa7b4c2c76297f47e681c655f6f1285a8780d6a022f7431"
+checksum = "528532f3d801c87aec9def2add9ca802fe569e44a544afe633765267840abe64"
 dependencies = [
  "getrandom",
  "redox_syscall",
- "rust-argon2",
 ]
 
 [[package]]
 name = "regex"
-version = "1.3.9"
+version = "1.5.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9c3780fcf44b193bc4d09f36d2a3c87b251da4a046c87795a0d35f4f927ad8e6"
+checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461"
 dependencies = [
  "aho-corasick",
  "memchr",
  "regex-syntax",
- "thread_local",
 ]
 
 [[package]]
 name = "regex-automata"
-version = "0.1.9"
+version = "0.1.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ae1ded71d66a4a97f5e961fd0cb25a5f366a42a41570d16a763a69c092c26ae4"
+checksum = "6c230d73fb8d8c1b9c0b3135c5142a8acee3a0558fb8db5cf1cb65f8d7862132"
 dependencies = [
- "byteorder",
  "regex-syntax",
 ]
 
 [[package]]
 name = "regex-syntax"
-version = "0.6.18"
+version = "0.6.25"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "26412eb97c6b088a6997e05f69403a802a92d520de2f8e63c2b65f9e0f47c4e8"
-
-[[package]]
-name = "rust-argon2"
-version = "0.7.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2bc8af4bda8e1ff4932523b94d3dd20ee30a87232323eda55903ffd71d2fb017"
-dependencies = [
- "base64",
- "blake2b_simd",
- "constant_time_eq",
- "crossbeam-utils 0.7.2",
-]
+checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b"
 
 [[package]]
 name = "rustc-hash"
@@ -768,6 +654,12 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
 
+[[package]]
+name = "rustversion"
+version = "1.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "61b3909d758bb75c79f23d4736fac9433868679d3ad2ea7a61e3c25cfda9a088"
+
 [[package]]
 name = "rustyline"
 version = "7.1.0"
@@ -775,7 +667,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8227301bfc717136f0ecbd3d064ba8199e44497a0bdd46bb01ede4387cfd2cec"
 dependencies = [
  "bitflags",
- "cfg-if 1.0.0",
+ "cfg-if",
  "fs2",
  "libc",
  "log",
@@ -796,11 +688,11 @@ checksum = "71d301d4193d031abdd79ff7e3dd721168a9572ef3fe51a1517aba235bd8f86e"
 
 [[package]]
 name = "salsa"
-version = "0.16.0"
+version = "0.16.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d8fadca2ab5de17acf66d744f4888049ca8f1bb9b8a1ab8afd9d032cc959c5dc"
+checksum = "4b84d9f96071f3f3be0dc818eae3327625d8ebc95b58da37d6850724f31d3403"
 dependencies = [
- "crossbeam-utils 0.8.3",
+ "crossbeam-utils",
  "indexmap",
  "lock_api",
  "log",
@@ -831,18 +723,18 @@ checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd"
 
 [[package]]
 name = "serde"
-version = "1.0.115"
+version = "1.0.130"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e54c9a88f2da7238af84b5101443f0c0d0a3bbdc455e34a5c9497b1903ed55d5"
+checksum = "f12d06de37cf59146fbdecab66aa99f9fe4f78722e3607577a5375d66bd0c913"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.115"
+version = "1.0.130"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "609feed1d0a73cc36a0182a840a9b37b4a82f0b1150369f0536a9e3f2a31dc48"
+checksum = "d7bc1a1ab1961464eae040d96713baa5a724a8152c1222492465b54322ec508b"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -851,53 +743,41 @@ dependencies = [
 
 [[package]]
 name = "serde_json"
-version = "1.0.57"
+version = "1.0.67"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "164eacbdb13512ec2745fb09d51fd5b22b0d65ed294a1dcf7285a360c80a675c"
+checksum = "a7f9e390c27c3c0ce8bc5d725f6e4d30a29d26659494aa4b17535f7522c5c950"
 dependencies = [
  "itoa",
  "ryu",
  "serde",
 ]
 
-[[package]]
-name = "sha2"
-version = "0.8.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a256f46ea78a0c0d9ff00077504903ac881a1dafdc20da66545699e7776b3e69"
-dependencies = [
- "block-buffer",
- "digest",
- "fake-simd",
- "opaque-debug",
-]
-
 [[package]]
 name = "sharded-slab"
-version = "0.0.9"
+version = "0.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "06d5a3f5166fb5b42a5439f2eee8b9de149e235961e3eb21c5808fc3ea17ff3e"
+checksum = "740223c51853f3145fe7c90360d2d4232f2b62e3449489c207eccde818979982"
 dependencies = [
  "lazy_static",
 ]
 
 [[package]]
 name = "siphasher"
-version = "0.3.3"
+version = "0.3.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fa8f3741c7372e75519bd9346068370c9cdaabcc1f9599cbcf2a2719352286b7"
+checksum = "533494a8f9b724d33625ab53c6c4800f7cc445895924a8ef649222dcb76e938b"
 
 [[package]]
 name = "smallvec"
-version = "1.4.2"
+version = "1.6.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fbee7696b84bbf3d89a1c2eccff0850e3047ed46bfcd2e92c29a2d074d57e252"
+checksum = "fe0f37c9e8f3c5a4a66ad655a93c74daac4ad00c441533bf5c6e7990bb42604e"
 
 [[package]]
 name = "string_cache"
-version = "0.8.0"
+version = "0.8.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2940c75beb4e3bf3a494cef919a747a2cb81e52571e212bfbd185074add7208a"
+checksum = "8ddb1139b5353f96e429e1a5e19fbaf663bddedaa06d1dbd49f82e352601209a"
 dependencies = [
  "lazy_static",
  "new_debug_unreachable",
@@ -908,15 +788,15 @@ dependencies = [
 
 [[package]]
 name = "strsim"
-version = "0.9.3"
+version = "0.10.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6446ced80d6c486436db5c078dde11a9f73d42b57fb273121e160b84f63d894c"
+checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
 
 [[package]]
 name = "syn"
-version = "1.0.38"
+version = "1.0.76"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e69abc24912995b3038597a7a593be5053eb0fb44f3cc5beec0deb421790c1f4"
+checksum = "c6f107db402c2c2055242dbf4d2af0e69197202e9faacbef9571bbe47f5a1b84"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -937,59 +817,59 @@ dependencies = [
 
 [[package]]
 name = "term"
-version = "0.5.2"
+version = "0.7.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "edd106a334b7657c10b7c540a0106114feadeb4dc314513e97df481d5d966f42"
+checksum = "c59df8ac95d96ff9bede18eb7300b0fda5e5d8d90960e76f8e14ae765eedbf1f"
 dependencies = [
- "byteorder",
- "dirs",
+ "dirs-next",
+ "rustversion",
  "winapi",
 ]
 
 [[package]]
 name = "termcolor"
-version = "1.1.0"
+version = "1.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bb6bfa289a4d7c5766392812c0a1f4c1ba45afa1ad47803c11e1f407d846d75f"
+checksum = "2dfed899f0eb03f32ee8c6a0aabdb8a7949659e3466561fc0adf54e26d88c5f4"
 dependencies = [
  "winapi-util",
 ]
 
 [[package]]
 name = "thread_local"
-version = "1.0.1"
+version = "1.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d40c6d1b69745a6ec6fb1ca717914848da4b44ae29d9b3080cbee91d72a69b14"
+checksum = "8018d24e04c95ac8790716a5987d0fec4f8b27249ffa0f7d33f1369bdfb88cbd"
 dependencies = [
- "lazy_static",
+ "once_cell",
 ]
 
 [[package]]
-name = "time"
-version = "0.1.43"
+name = "tiny-keccak"
+version = "2.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ca8a50ef2360fbd1eeb0ecd46795a87a19024eb4b53c5dc916ca1fd95fe62438"
+checksum = "2c9d3793400a45f954c52e73d068316d76b6f4e36977e3fcebb13a2721e80237"
 dependencies = [
- "libc",
- "winapi",
+ "crunchy",
 ]
 
 [[package]]
 name = "tracing"
-version = "0.1.19"
+version = "0.1.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6d79ca061b032d6ce30c660fded31189ca0b9922bf483cd70759f13a2d86786c"
+checksum = "09adeb8c97449311ccd28a427f96fb563e7fd31aabf994189879d9da2394b89d"
 dependencies = [
- "cfg-if 0.1.10",
+ "cfg-if",
+ "pin-project-lite",
  "tracing-attributes",
  "tracing-core",
 ]
 
 [[package]]
 name = "tracing-attributes"
-version = "0.1.10"
+version = "0.1.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1fe233f4227389ab7df5b32649239da7ebe0b281824b4e84b342d04d3fd8c25e"
+checksum = "c42e6fa53307c8a17e4ccd4dc81cf5ec38db9209f59b222210375b54ee40d1e2"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -998,18 +878,18 @@ dependencies = [
 
 [[package]]
 name = "tracing-core"
-version = "0.1.14"
+version = "0.1.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "db63662723c316b43ca36d833707cc93dff82a02ba3d7e354f342682cc8b3545"
+checksum = "2ca517f43f0fb96e0c3072ed5c275fe5eece87e8cb52f4a77b69226d3b1c9df8"
 dependencies = [
  "lazy_static",
 ]
 
 [[package]]
 name = "tracing-log"
-version = "0.1.1"
+version = "0.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5e0f8c7178e13481ff6765bd169b33e8d554c5d2bbede5e32c356194be02b9b9"
+checksum = "a6923477a48e41c1951f1999ef8bb5a3023eb723ceadafe78ffb65dc366761e3"
 dependencies = [
  "lazy_static",
  "log",
@@ -1018,9 +898,9 @@ dependencies = [
 
 [[package]]
 name = "tracing-serde"
-version = "0.1.1"
+version = "0.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b6ccba2f8f16e0ed268fc765d9b7ff22e965e7185d32f8f1ec8294fe17d86e79"
+checksum = "fb65ea441fbb84f9f6748fd496cf7f63ec9af5bca94dd86456978d055e8eb28b"
 dependencies = [
  "serde",
  "tracing-core",
@@ -1028,9 +908,9 @@ dependencies = [
 
 [[package]]
 name = "tracing-subscriber"
-version = "0.2.11"
+version = "0.2.20"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "abd165311cc4d7a555ad11cc77a37756df836182db0d81aac908c8184c584f40"
+checksum = "b9cbe87a2fa7e35900ce5de20220a582a9483a7063811defce79d7cbd59d4cfe"
 dependencies = [
  "ansi_term 0.12.1",
  "chrono",
@@ -1042,6 +922,7 @@ dependencies = [
  "sharded-slab",
  "smallvec",
  "thread_local",
+ "tracing",
  "tracing-core",
  "tracing-log",
  "tracing-serde",
@@ -1049,29 +930,23 @@ dependencies = [
 
 [[package]]
 name = "tracing-tree"
-version = "0.1.5"
+version = "0.1.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e1a3dc4774db3a6b2d66a4f8d8de670e874ec3ed55615860c994927419b32c5f"
+checksum = "1712b40907f8d9bc2bc66763ab61dec914b7123d7149e59feb0d4e2a95fc4967"
 dependencies = [
  "ansi_term 0.12.1",
  "atty",
- "chrono",
  "termcolor",
  "tracing",
+ "tracing-log",
  "tracing-subscriber",
 ]
 
-[[package]]
-name = "typenum"
-version = "1.12.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "373c8a200f9e67a0c95e62a4f52fbf80c23b4381c05a17845531982fa99e6b33"
-
 [[package]]
 name = "unicode-segmentation"
-version = "1.6.0"
+version = "1.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e83e153d1053cbb5a118eeff7fd5be06ed99153f00dbcd8ae310c5fb2b22edc0"
+checksum = "8895849a949e7845e06bd6dc1aa51731a103c42707010a5b591c0038fb73385b"
 
 [[package]]
 name = "unicode-width"
@@ -1081,9 +956,9 @@ checksum = "9337591893a19b88d8d87f2cec1e73fad5cdfd10e5a6f349f498ad6ea2ffb1e3"
 
 [[package]]
 name = "unicode-xid"
-version = "0.2.1"
+version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f7fe0bb3479651439c9112f72b6c505038574c9fbb575ed1bf3b797fa39dd564"
+checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3"
 
 [[package]]
 name = "utf8parse"
@@ -1093,9 +968,9 @@ checksum = "936e4b492acfd135421d8dca4b1aa80a7bfc26e702ef3af710e0752684df5372"
 
 [[package]]
 name = "wasi"
-version = "0.9.0+wasi-snapshot-preview1"
+version = "0.10.2+wasi-snapshot-preview1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cccddf32554fecc6acb585f82a32a72e28b48f8c4c1883ddfeeeaa96f7d8e519"
+checksum = "fd6fbd9a79829dd1ad0cc20627bf1ed606756a7f77edff7b66b7064f9cb327c6"
 
 [[package]]
 name = "winapi"
diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index 4964400807c..da0fca3f5ee 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -1,10 +1,3 @@
-//! Defines traits used to embed the chalk-engine in another crate.
-//!
-//! chalk and rustc both define types which implement the traits in this
-//! module. This allows each user of chalk-engine to define their own
-//! `DomainGoal` type, add arena lifetime parameters, and more. See
-//! [`Context`] trait for a list of types.
-
 use crate::CompleteAnswer;
 use chalk_ir::interner::Interner;
 use chalk_ir::Substitution;
diff --git a/chalk-engine/src/slg.rs b/chalk-engine/src/slg.rs
index 028ef8492ea..c91a1abb018 100644
--- a/chalk-engine/src/slg.rs
+++ b/chalk-engine/src/slg.rs
@@ -212,9 +212,16 @@ impl<I: Interner> MayInvalidate<'_, I> {
                 TyKind::OpaqueType(id_b, substitution_b),
             ) => self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b),
             (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => self.aggregate_tys(ty_a, ty_b),
-            (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => {
-                self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
-            }
+            (
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_a,
+                    substitution: substitution_a,
+                }),
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_b,
+                    substitution: substitution_b,
+                }),
+            ) => self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b),
             (TyKind::Ref(id_a, lifetime_a, ty_a), TyKind::Ref(id_b, lifetime_b, ty_b)) => {
                 id_a != id_b
                     || self.aggregate_lifetimes(lifetime_a, lifetime_b)
diff --git a/chalk-engine/src/slg/aggregate.rs b/chalk-engine/src/slg/aggregate.rs
index ffb79ec0477..3d4d54183b9 100644
--- a/chalk-engine/src/slg/aggregate.rs
+++ b/chalk-engine/src/slg/aggregate.rs
@@ -305,9 +305,24 @@ impl<I: Interner> AntiUnifier<'_, '_, I> {
             (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => {
                 TyKind::Slice(self.aggregate_tys(ty_a, ty_b)).intern(interner)
             }
-            (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => self
+            (
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_a,
+                    substitution: substitution_a,
+                }),
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_b,
+                    substitution: substitution_b,
+                }),
+            ) => self
                 .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
-                .map(|(&name, substitution)| TyKind::FnDef(name, substitution).intern(interner))
+                .map(|(&name, substitution)| {
+                    TyKind::FnDef(FnDefTy {
+                        fn_def_id: name,
+                        substitution,
+                    })
+                    .intern(interner)
+                })
                 .unwrap_or_else(|| self.new_ty_variable()),
             (TyKind::Ref(id_a, lifetime_a, ty_a), TyKind::Ref(id_b, lifetime_b, ty_b)) => {
                 if id_a == id_b {
diff --git a/chalk-engine/src/slg/resolvent.rs b/chalk-engine/src/slg/resolvent.rs
index 906f8879a95..dd6c535f871 100644
--- a/chalk-engine/src/slg/resolvent.rs
+++ b/chalk-engine/src/slg/resolvent.rs
@@ -489,7 +489,16 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
                 )
             }
             (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => Zip::zip_with(self, variance, ty_a, ty_b),
-            (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => {
+            (
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_a,
+                    substitution: substitution_a,
+                }),
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_b,
+                    substitution: substitution_b,
+                }),
+            ) => {
                 if id_a != id_b {
                     return Err(NoSolution);
                 }
diff --git a/chalk-integration/src/db.rs b/chalk-integration/src/db.rs
index 262975b5654..58b26765257 100644
--- a/chalk-integration/src/db.rs
+++ b/chalk-integration/src/db.rs
@@ -13,9 +13,9 @@ use chalk_ir::{
     UnificationDatabase, Variances,
 };
 use chalk_solve::rust_ir::{
-    AdtDatum, AdtRepr, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind,
-    FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum,
-    OpaqueTyDatum, TraitDatum, WellKnownTrait,
+    AdtDatum, AdtRepr, AssociatedFnValue, AssociatedFnValueId, AssociatedTyDatum,
+    AssociatedTyValue, AssociatedTyValueId, ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum,
+    GeneratorDatum, GeneratorWitnessDatum, ImplDatum, OpaqueTyDatum, TraitDatum, WellKnownTrait,
 };
 use chalk_solve::{RustIrDatabase, Solution, SubstitutionResult};
 use salsa::Database;
@@ -91,6 +91,13 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
         self.program_ir().unwrap().associated_ty_data(ty)
     }
 
+    fn associated_fn_data(
+        &self,
+        f: chalk_ir::AssocFnDefId<ChalkIr>,
+    ) -> Arc<chalk_solve::rust_ir::AssociatedFnDatum<ChalkIr>> {
+        self.program_ir().unwrap().associated_fn_data(f)
+    }
+
     fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
         self.program_ir().unwrap().trait_datum(id)
     }
@@ -106,6 +113,13 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
         self.program_ir().unwrap().associated_ty_values[&id].clone()
     }
 
+    fn associated_fn_value(
+        &self,
+        id: AssociatedFnValueId<ChalkIr>,
+    ) -> Arc<AssociatedFnValue<ChalkIr>> {
+        self.program_ir().unwrap().associated_fn_values[&id].clone()
+    }
+
     fn opaque_ty_data(&self, id: OpaqueTyId<ChalkIr>) -> Arc<OpaqueTyDatum<ChalkIr>> {
         self.program_ir().unwrap().opaque_ty_data(id)
     }
diff --git a/chalk-integration/src/error.rs b/chalk-integration/src/error.rs
index ba223d2d249..a443d31bd1b 100644
--- a/chalk-integration/src/error.rs
+++ b/chalk-integration/src/error.rs
@@ -57,8 +57,13 @@ impl std::error::Error for ChalkError {}
 pub enum RustIrError {
     InvalidParameterName(Identifier),
     InvalidTraitName(Identifier),
+    InvalidImplName(Identifier),
+    InvalidImplMemberName(Identifier, Identifier),
     NotTrait(Identifier),
     NotStruct(Identifier),
+    NotAssociatedType(Identifier),
+    NotAssociatedFn(Identifier),
+    AmbiguousProjection(Identifier),
     DuplicateOrShadowedParameters,
     AutoTraitAssociatedTypes(Identifier),
     AutoTraitParameters(Identifier),
@@ -66,6 +71,7 @@ pub enum RustIrError {
     InvalidFundamentalTypesParameters(Identifier),
     NegativeImplAssociatedValues(Identifier),
     MissingAssociatedType(Identifier),
+    MissingAssociatedFn(Identifier),
     IncorrectNumberOfVarianceParameters {
         identifier: Identifier,
         expected: usize,
@@ -81,6 +87,11 @@ pub enum RustIrError {
         expected: usize,
         actual: usize,
     },
+    IncorrectNumberOfAssociatedFnParameters {
+        identifier: Identifier,
+        expected: usize,
+        actual: usize,
+    },
     IncorrectParameterKind {
         identifier: Identifier,
         expected: Kind,
@@ -96,6 +107,11 @@ pub enum RustIrError {
         expected: Kind,
         actual: Kind,
     },
+    IncorrectAssociatedFnParameterKind {
+        identifier: Identifier,
+        expected: Kind,
+        actual: Kind,
+    },
     CannotApplyTypeParameter(Identifier),
     InvalidExternAbi(Atom),
 }
@@ -107,6 +123,12 @@ impl std::fmt::Display for RustIrError {
                 write!(f, "invalid parameter name `{}`", name)
             }
             RustIrError::InvalidTraitName(name) => write!(f, "invalid trait name `{}`", name),
+            RustIrError::InvalidImplName(name) => write!(f, "invalid impl name `{}`", name),
+            RustIrError::InvalidImplMemberName(impl_name, member_name) => write!(
+                f,
+                "invalid impl member name `{}::{}`",
+                impl_name, member_name
+            ),
             RustIrError::NotTrait(name) => write!(
                 f,
                 "expected a trait, found `{}`, which is not a trait",
@@ -117,6 +139,22 @@ impl std::fmt::Display for RustIrError {
                 "expected a struct, found `{}`, which is not a struct",
                 name
             ),
+            RustIrError::NotAssociatedType(name) => write!(
+                f,
+                "expected an associated type, found `{}`, which is not",
+                name
+            ),
+            RustIrError::NotAssociatedFn(name) => write!(
+                f,
+                "expected an associated fn, found `{}`, which is not",
+                name
+            ),
+            RustIrError::AmbiguousProjection(name) => write!(
+                f,
+                "projection refers to `{}` which is both a fn and a type",
+                name
+            ),
+
             RustIrError::DuplicateOrShadowedParameters => {
                 write!(f, "duplicate or shadowed parameters")
             }
@@ -142,6 +180,9 @@ impl std::fmt::Display for RustIrError {
             RustIrError::MissingAssociatedType(name) => {
                 write!(f, "no associated type `{}` defined in trait", name)
             }
+            RustIrError::MissingAssociatedFn(name) => {
+                write!(f, "no associated fn `{}` defined in trait", name)
+            }
             RustIrError::IncorrectNumberOfVarianceParameters {
                 identifier,
                 expected,
@@ -169,6 +210,15 @@ impl std::fmt::Display for RustIrError {
                 "wrong number of parameters for associated type `{}` (expected {}, got {})",
                 identifier, expected, actual
             ),
+            RustIrError::IncorrectNumberOfAssociatedFnParameters {
+                identifier,
+                expected,
+                actual,
+            } => write!(
+                f,
+                "wrong number of parameters for associated fn `{}` (expected {}, got {})",
+                identifier, expected, actual
+            ),
             RustIrError::IncorrectParameterKind {
                 identifier,
                 expected,
@@ -196,6 +246,15 @@ impl std::fmt::Display for RustIrError {
                 "incorrect associated type parameter kind for `{}`: expected {}, found {}",
                 identifier, expected, actual
             ),
+            RustIrError::IncorrectAssociatedFnParameterKind {
+                identifier,
+                expected,
+                actual,
+            } => write!(
+                f,
+                "incorrect associated fn parameter kind for `{}`: expected {}, found {}",
+                identifier, expected, actual
+            ),
             RustIrError::CannotApplyTypeParameter(name) => {
                 write!(f, "cannot apply type parameter `{}`", name)
             }
diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
index ff37443b38c..723301c6bd5 100644
--- a/chalk-integration/src/lowering.rs
+++ b/chalk-integration/src/lowering.rs
@@ -22,6 +22,29 @@ use env::*;
 const SELF: &str = "Self";
 const FIXME_SELF: &str = "__FIXME_SELF__";
 
+/// The chalk-integration language can have projections either refer to types
+/// or functions
+pub enum ProjectionTarget {
+    ProjectionTy(chalk_ir::ProjectionTy<ChalkIr>),
+    ProjectionFn(chalk_ir::FnDefTy<ChalkIr>),
+}
+
+impl ProjectionTarget {
+    pub fn expect_ty(self, name: &Identifier) -> LowerResult<chalk_ir::ProjectionTy<ChalkIr>> {
+        match self {
+            ProjectionTarget::ProjectionTy(t) => Ok(t),
+            ProjectionTarget::ProjectionFn(_) => Err(RustIrError::NotAssociatedType(name.clone())),
+        }
+    }
+
+    pub fn expect_fn(self, name: &Identifier) -> LowerResult<chalk_ir::FnDefTy<ChalkIr>> {
+        match self {
+            ProjectionTarget::ProjectionFn(f) => Ok(f),
+            ProjectionTarget::ProjectionTy(_) => Err(RustIrError::NotAssociatedFn(name.clone())),
+        }
+    }
+}
+
 trait LowerWithEnv {
     type Lowered;
 
@@ -44,7 +67,7 @@ impl Lower for Program {
         // based just on its position:
         let raw_ids = self.items.iter().map(|_| lowerer.next_item_id()).collect();
 
-        lowerer.extract_associated_types(self, &raw_ids)?;
+        lowerer.extract_trait_decls(self, &raw_ids)?;
         lowerer.extract_ids(self, &raw_ids)?;
         lowerer.lower(self, &raw_ids)
     }
@@ -162,7 +185,9 @@ impl LowerWithEnv for WhereClause {
             }
             WhereClause::ProjectionEq { projection, ty } => vec![
                 chalk_ir::WhereClause::AliasEq(chalk_ir::AliasEq {
-                    alias: chalk_ir::AliasTy::Projection(projection.lower(env)?),
+                    alias: chalk_ir::AliasTy::Projection(
+                        projection.lower(env)?.expect_ty(&projection.name)?,
+                    ),
                     ty: ty.lower(env)?,
                 }),
                 chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?),
@@ -214,10 +239,18 @@ impl LowerWithEnv for DomainGoal {
                 .collect(),
             DomainGoal::Normalize { projection, ty } => {
                 vec![chalk_ir::DomainGoal::Normalize(chalk_ir::Normalize {
-                    alias: chalk_ir::AliasTy::Projection(projection.lower(env)?),
+                    alias: chalk_ir::AliasTy::Projection(
+                        projection.lower(env)?.expect_ty(&projection.name)?,
+                    ),
                     ty: ty.lower(env)?,
                 })]
             }
+            DomainGoal::NormalizeFn { projection, ty } => {
+                vec![chalk_ir::DomainGoal::NormalizeFn(
+                    projection.lower(env)?.expect_fn(&projection.name)?,
+                    ty.lower(env)?,
+                )]
+            }
             DomainGoal::TyWellFormed { ty } => vec![chalk_ir::DomainGoal::WellFormed(
                 chalk_ir::WellFormed::Ty(ty.lower(env)?),
             )],
@@ -333,13 +366,16 @@ impl LowerWithEnv for AdtRepr {
     }
 }
 
-impl LowerWithEnv for (&FnDefn, chalk_ir::FnDefId<ChalkIr>) {
+pub struct LowerFnDefn<'a>(&'a FnDefn, chalk_ir::FnDefId<ChalkIr>);
+
+impl<'a> LowerWithEnv for LowerFnDefn<'a> {
     type Lowered = rust_ir::FnDefDatum<ChalkIr>;
 
     fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
-        let (fn_defn, fn_def_id) = self;
-
-        let binders = env.in_binders(fn_defn.all_parameters(), |env| {
+        let LowerFnDefn(fn_defn, fn_def_id) = self;
+        let params = fn_defn.all_parameters();
+        debug!(params = ?params);
+        let binders = env.in_binders(params, |env| {
             let where_clauses = fn_defn.where_clauses.lower(env)?;
 
             let inputs_and_output = env.in_binders(vec![], |env| {
@@ -360,6 +396,8 @@ impl LowerWithEnv for (&FnDefn, chalk_ir::FnDefId<ChalkIr>) {
             })
         })?;
 
+        debug!("LowerFnDefn id={:?} binders={:?}", &fn_def_id, &binders);
+
         Ok(rust_ir::FnDefDatum {
             id: *fn_def_id,
             sig: fn_defn.sig.lower()?,
@@ -610,11 +648,11 @@ impl Lower for TraitFlags {
     }
 }
 
-impl LowerWithEnv for ProjectionTy {
-    type Lowered = chalk_ir::ProjectionTy<ChalkIr>;
+impl LowerWithEnv for Projection {
+    type Lowered = ProjectionTarget;
 
     fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
-        let ProjectionTy {
+        let Projection {
             ref trait_ref,
             ref name,
             ref args,
@@ -624,36 +662,87 @@ impl LowerWithEnv for ProjectionTy {
             trait_id,
             substitution: trait_substitution,
         } = trait_ref.lower(env)?;
-        let lookup = env.lookup_associated_ty(trait_id, name)?;
-        let mut args: Vec<_> = args
-            .iter()
-            .map(|a| a.lower(env))
-            .collect::<LowerResult<_>>()?;
+        match (
+            env.lookup_associated_ty(trait_id, name),
+            env.lookup_associated_fn(trait_id, name),
+        ) {
+            // both present; ambiguous in the chalk-integration language
+            (Ok(_), Ok(_)) => return Err(RustIrError::AmbiguousProjection(name.clone())),
+
+            // neither present
+            (
+                Err(e @ RustIrError::MissingAssociatedType(_)),
+                Err(RustIrError::MissingAssociatedFn(_)),
+            ) => return Err(e),
+
+            // type
+            (Ok(lookup), _) => {
+                let mut args: Vec<_> = args
+                    .iter()
+                    .map(|a| a.lower(env))
+                    .collect::<LowerResult<_>>()?;
+
+                if args.len() != lookup.addl_variable_kinds.len() {
+                    Err(RustIrError::IncorrectNumberOfAssociatedTypeParameters {
+                        identifier: self.name.clone(),
+                        expected: lookup.addl_variable_kinds.len(),
+                        actual: args.len(),
+                    })?;
+                }
 
-        if args.len() != lookup.addl_variable_kinds.len() {
-            Err(RustIrError::IncorrectNumberOfAssociatedTypeParameters {
-                identifier: self.name.clone(),
-                expected: lookup.addl_variable_kinds.len(),
-                actual: args.len(),
-            })?;
-        }
+                for (param, arg) in lookup.addl_variable_kinds.iter().zip(args.iter()) {
+                    if param.kind() != arg.kind() {
+                        Err(RustIrError::IncorrectAssociatedTypeParameterKind {
+                            identifier: self.name.clone(),
+                            expected: param.kind(),
+                            actual: arg.kind(),
+                        })?;
+                    }
+                }
 
-        for (param, arg) in lookup.addl_variable_kinds.iter().zip(args.iter()) {
-            if param.kind() != arg.kind() {
-                Err(RustIrError::IncorrectAssociatedTypeParameterKind {
-                    identifier: self.name.clone(),
-                    expected: param.kind(),
-                    actual: arg.kind(),
-                })?;
+                args.extend(trait_substitution.iter(interner).cloned());
+
+                Ok(ProjectionTarget::ProjectionTy(chalk_ir::ProjectionTy {
+                    associated_ty_id: lookup.id,
+                    substitution: chalk_ir::Substitution::from_iter(interner, args),
+                }))
             }
-        }
 
-        args.extend(trait_substitution.iter(interner).cloned());
+            // function
+            (_, Ok(lookup)) => {
+                let mut args: Vec<_> = args
+                    .iter()
+                    .map(|a| a.lower(env))
+                    .collect::<LowerResult<_>>()?;
+
+                if args.len() != lookup.addl_variable_kinds.len() {
+                    Err(RustIrError::IncorrectNumberOfAssociatedFnParameters {
+                        identifier: self.name.clone(),
+                        expected: lookup.addl_variable_kinds.len(),
+                        actual: args.len(),
+                    })?;
+                }
 
-        Ok(chalk_ir::ProjectionTy {
-            associated_ty_id: lookup.id,
-            substitution: chalk_ir::Substitution::from_iter(interner, args),
-        })
+                for (param, arg) in lookup.addl_variable_kinds.iter().zip(args.iter()) {
+                    if param.kind() != arg.kind() {
+                        Err(RustIrError::IncorrectAssociatedFnParameterKind {
+                            identifier: self.name.clone(),
+                            expected: param.kind(),
+                            actual: arg.kind(),
+                        })?;
+                    }
+                }
+
+                args.extend(trait_substitution.iter(interner).cloned());
+
+                Ok(ProjectionTarget::ProjectionFn(chalk_ir::FnDefTy {
+                    fn_def_id: lookup.id.as_fn(),
+                    substitution: chalk_ir::Substitution::from_iter(interner, args),
+                }))
+            }
+
+            (Err(e), _) => return Err(e),
+        }
     }
 }
 
@@ -705,7 +794,7 @@ impl LowerWithEnv for Ty {
 
             Ty::Apply { name, ref args } => {
                 macro_rules! tykind {
-                    ($k:expr, $tykind:ident, $id:expr) => {{
+                    ($k:expr, $id:expr => $f:expr) => {{
                         if $k.binders.len(interner) != args.len() {
                             Err(RustIrError::IncorrectNumberOfTypeParameters {
                                 identifier: name.clone(),
@@ -733,15 +822,25 @@ impl LowerWithEnv for Ty {
                                 })?;
                             }
                         }
-                        chalk_ir::TyKind::$tykind($id, substitution).intern(interner)
+                        ($f)($id, substitution).intern(interner)
                     }};
+                    ($k:expr, $tykind:ident, $id:expr) => {
+                        tykind!($k, $id => chalk_ir::TyKind::$tykind)
+                    };
                 }
                 match env.lookup_type(&name)? {
                     TypeLookup::Parameter(_) => {
                         return Err(RustIrError::CannotApplyTypeParameter(name.clone()))
                     }
                     TypeLookup::Adt(id) => tykind!(env.adt_kind(id), Adt, id),
-                    TypeLookup::FnDef(id) => tykind!(env.fn_def_kind(id), FnDef, id),
+                    TypeLookup::FnDef(id) => {
+                        tykind!(env.fn_def_kind(id), id => |x, y| chalk_ir::TyKind::FnDef(
+                            chalk_ir::FnDefTy {
+                                fn_def_id: x,
+                                substitution: y
+                            }
+                        ))
+                    }
                     TypeLookup::Closure(id) => tykind!(env.closure_kind(id), Closure, id),
                     TypeLookup::Opaque(id) => tykind!(env.opaque_kind(id), OpaqueType, id),
                     TypeLookup::Generator(id) => tykind!(env.generator_kind(id), Generator, id),
@@ -751,10 +850,10 @@ impl LowerWithEnv for Ty {
                 }
             }
 
-            Ty::Projection { ref proj } => {
-                chalk_ir::TyKind::Alias(chalk_ir::AliasTy::Projection(proj.lower(env)?))
-                    .intern(interner)
-            }
+            Ty::Projection { ref proj } => chalk_ir::TyKind::Alias(chalk_ir::AliasTy::Projection(
+                proj.lower(env)?.expect_ty(&proj.name)?,
+            ))
+            .intern(interner),
 
             Ty::ForAll {
                 lifetime_names,
@@ -808,6 +907,21 @@ impl LowerWithEnv for Ty {
             Ty::Str => chalk_ir::TyKind::Str.intern(interner),
 
             Ty::Never => chalk_ir::TyKind::Never.intern(interner),
+            Ty::ImplFn { func } => {
+                // resolve the function reference
+                let impl_fn = env.lookup_impl_fn(&func.impl_name, &func.fn_name)?;
+
+                let substitution = Substitution::from_fallible(
+                    interner,
+                    func.args.iter().map(|arg| arg.lower(env)),
+                )?;
+
+                chalk_ir::TyKind::FnDef(chalk_ir::FnDefTy {
+                    fn_def_id: impl_fn.as_fn(),
+                    substitution,
+                })
+                .intern(interner)
+            }
         })
     }
 }
@@ -884,11 +998,18 @@ impl LowerWithEnv for Lifetime {
     }
 }
 
-impl LowerWithEnv for (&Impl, ImplId<ChalkIr>, &AssociatedTyValueIds) {
+struct LowerImpl<'a>(
+    &'a Impl,
+    ImplId<ChalkIr>,
+    &'a AssociatedTyValueIds,
+    &'a AssociatedFnValueIds,
+);
+
+impl<'a> LowerWithEnv for LowerImpl<'a> {
     type Lowered = rust_ir::ImplDatum<ChalkIr>;
 
     fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
-        let (impl_, impl_id, associated_ty_value_ids) = self;
+        let LowerImpl(impl_, impl_id, associated_ty_value_ids, associated_fn_value_ids) = self;
 
         let polarity = impl_.polarity.lower();
         let binders = env.in_binders(impl_.all_parameters(), |env| {
@@ -920,11 +1041,18 @@ impl LowerWithEnv for (&Impl, ImplId<ChalkIr>, &AssociatedTyValueIds) {
 
         debug!(?associated_ty_value_ids);
 
+        let fn_defs = impl_
+            .fn_defs
+            .iter()
+            .map(|fd| associated_fn_value_ids[&(*impl_id, fd.name.str.clone())])
+            .collect();
+
         Ok(rust_ir::ImplDatum {
             polarity,
             binders,
             impl_type: impl_.impl_type.lower(),
             associated_ty_value_ids,
+            associated_fn_value_ids: fn_defs,
         })
     }
 }
@@ -969,11 +1097,13 @@ impl LowerWithEnv for Clause {
     }
 }
 
-impl LowerWithEnv for (&TraitDefn, chalk_ir::TraitId<ChalkIr>) {
+struct LowerTrait<'a>(&'a TraitDefn, chalk_ir::TraitId<ChalkIr>);
+
+impl LowerWithEnv for LowerTrait<'_> {
     type Lowered = rust_ir::TraitDatum<ChalkIr>;
 
     fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
-        let (trait_defn, trait_id) = self;
+        let LowerTrait(trait_defn, trait_id) = self;
 
         let all_parameters = trait_defn.all_parameters();
         let all_parameters_len = all_parameters.len();
@@ -998,12 +1128,19 @@ impl LowerWithEnv for (&TraitDefn, chalk_ir::TraitId<ChalkIr>) {
             .map(|defn| env.lookup_associated_ty(*trait_id, &defn.name).unwrap().id)
             .collect();
 
+        let associated_fn_def_ids = trait_defn
+            .fn_defs
+            .iter()
+            .map(|fd| env.lookup_associated_fn(*trait_id, &fd.name).unwrap().id)
+            .collect();
+
         let trait_datum = rust_ir::TraitDatum {
             id: *trait_id,
             binders,
             flags: trait_defn.flags.lower(),
             associated_ty_ids,
             well_known: trait_defn.well_known.map(|def| def.lower()),
+            fn_defs: associated_fn_def_ids,
         };
 
         debug!(?trait_datum);
@@ -1031,6 +1168,38 @@ pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir
         })
         .collect();
 
+    let associated_fn_lookups = program
+        .associated_fn_data
+        .iter()
+        .map(|(&fn_id, fn_datum)| {
+            let trait_datum = &program.trait_data[&fn_datum.trait_id];
+            let num_trait_params = trait_datum.binders.len(interner);
+            let num_addl_params = fn_datum.binders.len(interner) - num_trait_params;
+            let addl_variable_kinds =
+                fn_datum.binders.binders.as_slice(interner)[..num_addl_params].to_owned();
+            let lookup = AssociatedFnLookup {
+                id: fn_id,
+                addl_variable_kinds,
+            };
+            ((fn_datum.trait_id, fn_datum.name.clone()), lookup)
+        })
+        .collect();
+
+    let associated_fn_value_lookups = program
+        .impl_data
+        .iter()
+        .flat_map(|(&impl_id, impl_datum)| {
+            impl_datum
+                .associated_fn_value_ids
+                .iter()
+                .map(move |&value_id| {
+                    let def_id = program.associated_fn_values[&value_id].fn_id;
+                    let name = program.associated_fn_data[&def_id].name.clone();
+                    ((impl_id, name), value_id)
+                })
+        })
+        .collect();
+
     let auto_traits = program
         .trait_data
         .iter()
@@ -1042,6 +1211,7 @@ pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir
         fn_def_ids: &program.fn_def_ids,
         closure_ids: &program.closure_ids,
         trait_ids: &program.trait_ids,
+        impl_ids: &program.impl_ids,
         opaque_ty_ids: &program.opaque_ty_ids,
         generator_ids: &program.generator_ids,
         generator_kinds: &program.generator_kinds,
@@ -1051,6 +1221,8 @@ pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir
         trait_kinds: &program.trait_kinds,
         opaque_ty_kinds: &program.opaque_ty_kinds,
         associated_ty_lookups: &associated_ty_lookups,
+        associated_fn_lookups: &associated_fn_lookups,
+        associated_fn_value_lookups: &associated_fn_value_lookups,
         foreign_ty_ids: &program.foreign_ty_ids,
         parameter_map: BTreeMap::new(),
         auto_traits: &auto_traits,
diff --git a/chalk-integration/src/lowering/env.rs b/chalk-integration/src/lowering/env.rs
index 3a4e9b016bd..5b8881f8977 100644
--- a/chalk-integration/src/lowering/env.rs
+++ b/chalk-integration/src/lowering/env.rs
@@ -5,8 +5,9 @@ use chalk_ir::{
 };
 use chalk_ir::{cast::Cast, ForeignDefId, WithKind};
 use chalk_parse::ast::*;
-use chalk_solve::rust_ir::AssociatedTyValueId;
+use chalk_solve::rust_ir::{AssociatedFnValueId, AssociatedTyValueId};
 use std::collections::BTreeMap;
+use tracing::{debug, span, Level};
 
 use crate::error::RustIrError;
 use crate::interner::ChalkIr;
@@ -16,6 +17,7 @@ pub type AdtIds = BTreeMap<Ident, chalk_ir::AdtId<ChalkIr>>;
 pub type FnDefIds = BTreeMap<Ident, chalk_ir::FnDefId<ChalkIr>>;
 pub type ClosureIds = BTreeMap<Ident, chalk_ir::ClosureId<ChalkIr>>;
 pub type TraitIds = BTreeMap<Ident, chalk_ir::TraitId<ChalkIr>>;
+pub type ImplIds = BTreeMap<Ident, chalk_ir::ImplId<ChalkIr>>;
 pub type GeneratorIds = BTreeMap<Ident, chalk_ir::GeneratorId<ChalkIr>>;
 pub type OpaqueTyIds = BTreeMap<Ident, chalk_ir::OpaqueTyId<ChalkIr>>;
 pub type AdtKinds = BTreeMap<chalk_ir::AdtId<ChalkIr>, TypeKind>;
@@ -28,6 +30,9 @@ pub type GeneratorKinds = BTreeMap<chalk_ir::GeneratorId<ChalkIr>, TypeKind>;
 pub type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedTyLookup>;
 pub type AssociatedTyValueIds =
     BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedTyValueId<ChalkIr>>;
+pub type AssociatedFnLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedFnLookup>;
+pub type AssociatedFnValueIds =
+    BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedFnValueId<ChalkIr>>;
 pub type ForeignIds = BTreeMap<Ident, chalk_ir::ForeignDefId<ChalkIr>>;
 
 pub type ParameterMap = BTreeMap<Ident, chalk_ir::WithKind<ChalkIr, BoundVar>>;
@@ -43,10 +48,13 @@ pub struct Env<'k> {
     pub closure_ids: &'k ClosureIds,
     pub closure_kinds: &'k ClosureKinds,
     pub trait_ids: &'k TraitIds,
+    pub impl_ids: &'k ImplIds,
     pub trait_kinds: &'k TraitKinds,
     pub opaque_ty_ids: &'k OpaqueTyIds,
     pub opaque_ty_kinds: &'k OpaqueTyVariableKinds,
     pub associated_ty_lookups: &'k AssociatedTyLookups,
+    pub associated_fn_lookups: &'k AssociatedFnLookups,
+    pub associated_fn_value_lookups: &'k AssociatedFnValueIds,
     pub auto_traits: &'k AutoTraits,
     pub foreign_ty_ids: &'k ForeignIds,
     pub generator_ids: &'k GeneratorIds,
@@ -57,7 +65,8 @@ pub struct Env<'k> {
 }
 
 /// Information about an associated type **declaration** (i.e., an
-/// `AssociatedTyDatum`). This information is gathered in the first
+/// [`rust_ir::AssociatedTyDatum`](chalk_solve::rust_ir::AssociatedTyDatum)).
+/// This information is gathered in the first
 /// phase of creating the Rust IR and is then later used to lookup the
 /// "id" of an associated type.
 ///
@@ -75,6 +84,25 @@ pub struct AssociatedTyLookup {
     pub addl_variable_kinds: Vec<chalk_ir::VariableKind<ChalkIr>>,
 }
 
+/// Information about an associated function **declaration** (i.e., an
+/// [`AssociatedFnDatum`](chalk_solve::rust_ir::AssociatedFnDatum)). This
+/// information is gathered in the first phase of creating the Rust IR and is
+/// then later used to lookup the "id" of an associated function.
+///
+/// ```ignore
+/// trait Foo {
+///     fn foo<'a, T>(); // <-- associated fn declaration
+///         // -----
+///         // |
+///         // addl_variable_kinds
+/// }
+/// ```
+#[derive(Debug, PartialEq, Eq, Clone)]
+pub struct AssociatedFnLookup {
+    pub id: chalk_ir::AssocFnDefId<ChalkIr>,
+    pub addl_variable_kinds: Vec<chalk_ir::VariableKind<ChalkIr>>,
+}
+
 pub enum TypeLookup<'k> {
     Parameter(&'k WithKind<ChalkIr, BoundVar>),
     Adt(AdtId<ChalkIr>),
@@ -98,7 +126,7 @@ impl Env<'_> {
         let interner = self.interner();
 
         macro_rules! tykind {
-            ($k:expr, $tykind:ident, $id:expr) => {
+            ($k:expr, $id:expr => $f:expr) => {
                 if $k.binders.len(interner) > 0 {
                     Err(RustIrError::IncorrectNumberOfTypeParameters {
                         identifier: name.clone(),
@@ -107,12 +135,15 @@ impl Env<'_> {
                     })
                 } else {
                     Ok(
-                        chalk_ir::TyKind::$tykind($id, chalk_ir::Substitution::empty(interner))
+                        ($f)($id, chalk_ir::Substitution::empty(interner))
                             .intern(interner),
                     )
                     .cast(interner)
                 }
             };
+            ($k:expr, $tykind:ident, $id:expr) => {
+                tykind!($k, $id => chalk_ir::TyKind::$tykind)
+            };
         }
 
         match self.lookup_type(name) {
@@ -131,7 +162,9 @@ impl Env<'_> {
                 })
             }
             Ok(TypeLookup::Adt(id)) => tykind!(self.adt_kind(id), Adt, id),
-            Ok(TypeLookup::FnDef(id)) => tykind!(self.fn_def_kind(id), FnDef, id),
+            Ok(TypeLookup::FnDef(id)) => {
+                tykind!(self.fn_def_kind(id), id => |x, y| chalk_ir::TyKind::FnDef(chalk_ir::FnDefTy {fn_def_id: x, substitution: y}))
+            }
             Ok(TypeLookup::Closure(id)) => tykind!(self.closure_kind(id), Closure, id),
             Ok(TypeLookup::Generator(id)) => tykind!(self.generator_kind(id), Generator, id),
             Ok(TypeLookup::Opaque(id)) => Ok(chalk_ir::TyKind::Alias(chalk_ir::AliasTy::Opaque(
@@ -188,6 +221,23 @@ impl Env<'_> {
         }
     }
 
+    pub fn lookup_impl_fn(
+        &self,
+        impl_name: &Identifier,
+        fn_name: &Identifier,
+    ) -> LowerResult<AssociatedFnValueId<ChalkIr>> {
+        let impl_id = self
+            .impl_ids
+            .get(&impl_name.str)
+            .copied()
+            .ok_or_else(|| RustIrError::InvalidImplName(impl_name.clone()))?;
+
+        self.associated_fn_value_lookups
+            .get(&(impl_id, fn_name.str.clone()))
+            .copied()
+            .ok_or_else(|| RustIrError::InvalidImplMemberName(impl_name.clone(), fn_name.clone()))
+    }
+
     pub fn trait_kind(&self, id: chalk_ir::TraitId<ChalkIr>) -> &TypeKind {
         &self.trait_kinds[&id]
     }
@@ -222,6 +272,17 @@ impl Env<'_> {
             .ok_or(RustIrError::MissingAssociatedType(ident.clone()))
     }
 
+    pub fn lookup_associated_fn(
+        &self,
+        trait_id: TraitId<ChalkIr>,
+        ident: &Identifier,
+    ) -> LowerResult<AssociatedFnLookup> {
+        self.associated_fn_lookups
+            .get(&(trait_id, ident.str.clone()))
+            .cloned()
+            .ok_or(RustIrError::MissingAssociatedFn(ident.clone()))
+    }
+
     /// Introduces new parameters, shifting the indices of existing
     /// parameters to accommodate them. The indices of the new binders
     /// will be assigned in order as they are iterated.
@@ -235,13 +296,17 @@ impl Env<'_> {
         // because that is the key-value pair for ParameterMap.
         // `swap_inner` lets us do precisely that, replacing `Ident` inside
         // `ParameterKind<Ident>` with a `BoundVar` and returning both.
-        let binders = binders.into_iter().enumerate().map(|(i, k)| {
-            let (kind, name) = k.into();
-            (
-                name,
-                chalk_ir::WithKind::new(kind, BoundVar::new(DebruijnIndex::INNERMOST, i)),
-            )
-        });
+        let binders = binders
+            .into_iter()
+            .enumerate()
+            .map(|(i, k)| {
+                let (kind, name) = k.into();
+                (
+                    name,
+                    chalk_ir::WithKind::new(kind, BoundVar::new(DebruijnIndex::INNERMOST, i)),
+                )
+            })
+            .inspect(|(a, b)| debug!(binder_name = ?a, kind = ?b));
         let len = binders.len();
 
         // For things already in the parameter map, we take each existing key-value pair
@@ -252,6 +317,7 @@ impl Env<'_> {
             .map(|(k, v)| (k.clone(), v.map_ref(|b| b.shifted_in())))
             .chain(binders)
             .collect();
+        debug!(parameter_map = ?parameter_map, outer_parameter_map = ?self.parameter_map, extra_len = ?len);
         if parameter_map.len() != self.parameter_map.len() + len {
             Err(RustIrError::DuplicateOrShadowedParameters)?;
         }
@@ -261,6 +327,7 @@ impl Env<'_> {
         })
     }
 
+    #[track_caller]
     pub fn in_binders<I, T, OP>(&self, binders: I, op: OP) -> LowerResult<chalk_ir::Binders<T>>
     where
         I: IntoIterator<Item = chalk_ir::WithKind<ChalkIr, Ident>>,
@@ -268,6 +335,8 @@ impl Env<'_> {
         T: HasInterner<Interner = ChalkIr>,
         OP: FnOnce(&Self) -> LowerResult<T>,
     {
+        let _span =
+            span!(Level::DEBUG, "in_binders", loc = %std::panic::Location::caller()).entered();
         let binders: Vec<_> = binders.into_iter().collect();
         let env = self.introduce(binders.iter().cloned())?;
         Ok(chalk_ir::Binders::new(
diff --git a/chalk-integration/src/lowering/program_lowerer.rs b/chalk-integration/src/lowering/program_lowerer.rs
index 1f39cd9bf27..f8a7711bb66 100644
--- a/chalk-integration/src/lowering/program_lowerer.rs
+++ b/chalk-integration/src/lowering/program_lowerer.rs
@@ -1,19 +1,22 @@
 use chalk_ir::cast::Cast;
 use chalk_ir::{
-    self, AdtId, AssocTypeId, BoundVar, ClosureId, DebruijnIndex, FnDefId, ForeignDefId,
-    GeneratorId, ImplId, OpaqueTyId, TraitId, TyVariableKind, VariableKinds,
+    self, AdtId, AssocFnDefId, AssocTypeId, BoundVar, ClosureId, DebruijnIndex, FnDefId,
+    ForeignDefId, GeneratorId, ImplId, OpaqueTyId, TraitId, TyVariableKind, VariableKinds,
 };
 use chalk_parse::ast::*;
 use chalk_solve::rust_ir::{
-    self, Anonymize, AssociatedTyValueId, GeneratorDatum, GeneratorInputOutputDatum,
-    GeneratorWitnessDatum, GeneratorWitnessExistential, OpaqueTyDatum, OpaqueTyDatumBound,
+    self, Anonymize, AssociatedFnValueId, AssociatedTyValueId, GeneratorDatum,
+    GeneratorInputOutputDatum, GeneratorWitnessDatum, GeneratorWitnessExistential, OpaqueTyDatum,
+    OpaqueTyDatumBound,
 };
 use rust_ir::IntoWhereClauses;
 use std::collections::{BTreeMap, HashSet};
 use std::sync::Arc;
 use string_cache::DefaultAtom as Atom;
 
-use super::{env::*, Lower, LowerParameterMap, LowerWithEnv, FIXME_SELF};
+use super::{
+    env::*, Lower, LowerFnDefn, LowerImpl, LowerParameterMap, LowerTrait, LowerWithEnv, FIXME_SELF,
+};
 use crate::error::RustIrError;
 use crate::program::Program as LoweredProgram;
 use crate::RawId;
@@ -25,10 +28,13 @@ pub(super) struct ProgramLowerer {
 
     associated_ty_lookups: AssociatedTyLookups,
     associated_ty_value_ids: AssociatedTyValueIds,
+    associated_fn_lookups: AssociatedFnLookups,
+    associated_fn_value_ids: AssociatedFnValueIds,
     adt_ids: AdtIds,
     fn_def_ids: FnDefIds,
     closure_ids: ClosureIds,
     trait_ids: TraitIds,
+    impl_ids: ImplIds,
     auto_traits: AutoTraits,
     opaque_ty_ids: OpaqueTyIds,
     adt_kinds: AdtKinds,
@@ -49,8 +55,8 @@ impl ProgramLowerer {
         RawId { index }
     }
 
-    /// Create ids for associated type declarations and values
-    pub fn extract_associated_types(
+    /// Create ids for associated type/function declarations and values
+    pub fn extract_trait_decls(
         &mut self,
         program: &Program,
         raw_ids: &Vec<RawId>,
@@ -70,13 +76,30 @@ impl ProgramLowerer {
                         self.associated_ty_lookups
                             .insert((TraitId(raw_id), defn.name.str.clone()), lookup);
                     }
+
+                    for defn in &d.fn_defs {
+                        let addl_variable_kinds = defn.all_parameters();
+                        let lookup = AssociatedFnLookup {
+                            id: AssocFnDefId(FnDefId(self.next_item_id())),
+                            addl_variable_kinds: addl_variable_kinds.anonymize(),
+                        };
+                        self.associated_fn_lookups
+                            .insert((TraitId(raw_id), defn.name.str.clone()), lookup);
+                    }
                 }
 
                 Item::Impl(d) => {
+                    let impl_id = ImplId(raw_id);
                     for atv in &d.assoc_ty_values {
                         let atv_id = AssociatedTyValueId(self.next_item_id());
                         self.associated_ty_value_ids
-                            .insert((ImplId(raw_id), atv.name.str.clone()), atv_id);
+                            .insert((impl_id, atv.name.str.clone()), atv_id);
+                    }
+
+                    for f in &d.fn_defs {
+                        let id = AssociatedFnValueId(FnDefId(self.next_item_id()));
+                        self.associated_fn_value_ids
+                            .insert((impl_id, f.name.str.clone()), id);
                     }
                 }
 
@@ -117,6 +140,13 @@ impl ProgramLowerer {
                     if defn.flags.object_safe {
                         self.object_safe_traits.insert(id);
                     }
+
+                    for func in &defn.fn_defs {
+                        let fn_lookup =
+                            &self.associated_fn_lookups[&(TraitId(raw_id), func.name.str.clone())];
+                        self.fn_def_kinds
+                            .insert(fn_lookup.id.as_fn(), func.lower_type_kind()?);
+                    }
                 }
                 Item::OpaqueTyDefn(defn) => {
                     let type_kind = defn.lower_type_kind()?;
@@ -133,7 +163,18 @@ impl ProgramLowerer {
                     self.generator_ids.insert(defn.name.str.clone(), id);
                     self.generator_kinds.insert(id, defn.lower_type_kind()?);
                 }
-                Item::Impl(_) => continue,
+                Item::Impl(imp) => {
+                    if let Some(ref name) = imp.id {
+                        self.impl_ids.insert(name.str.clone(), ImplId(raw_id));
+                    }
+
+                    for func in &imp.fn_defs {
+                        let fn_id =
+                            self.associated_fn_value_ids[&(ImplId(raw_id), func.name.str.clone())];
+                        self.fn_def_kinds
+                            .insert(fn_id.as_fn(), func.lower_type_kind()?);
+                    }
+                }
                 Item::Clause(_) => continue,
             };
         }
@@ -154,12 +195,40 @@ impl ProgramLowerer {
         let mut impl_data = BTreeMap::new();
         let mut associated_ty_data = BTreeMap::new();
         let mut associated_ty_values = BTreeMap::new();
+        let mut associated_fn_data = BTreeMap::new();
+        let mut associated_fn_values = BTreeMap::new();
         let mut opaque_ty_data = BTreeMap::new();
         let mut generator_data = BTreeMap::new();
         let mut generator_witness_data = BTreeMap::new();
         let mut hidden_opaque_types = BTreeMap::new();
         let mut custom_clauses = Vec::new();
 
+        let mut process_fn_def = |defn: &FnDefn, fn_def_id, identifier: &Identifier, n_params| {
+            let variances = match defn.variances.clone() {
+                Some(v) => {
+                    if v.len() != n_params {
+                        return Err(RustIrError::IncorrectNumberOfVarianceParameters {
+                            identifier: identifier.clone(),
+                            expected: n_params,
+                            actual: v.len(),
+                        });
+                    }
+                    v.into_iter()
+                        .map(|v| match v {
+                            Variance::Invariant => chalk_ir::Variance::Invariant,
+                            Variance::Covariant => chalk_ir::Variance::Covariant,
+                            Variance::Contravariant => chalk_ir::Variance::Contravariant,
+                        })
+                        .collect()
+                }
+                None => (0..n_params)
+                    .map(|_| chalk_ir::Variance::Invariant)
+                    .collect(),
+            };
+            fn_def_variances.insert(fn_def_id, variances);
+            Ok(fn_def_id)
+        };
+
         for (item, &raw_id) in program.items.iter().zip(raw_ids) {
             let empty_env = Env {
                 adt_ids: &self.adt_ids,
@@ -169,6 +238,7 @@ impl ProgramLowerer {
                 closure_ids: &self.closure_ids,
                 closure_kinds: &self.closure_kinds,
                 trait_ids: &self.trait_ids,
+                impl_ids: &self.impl_ids,
                 trait_kinds: &self.trait_kinds,
                 opaque_ty_ids: &self.opaque_ty_ids,
                 opaque_ty_kinds: &self.opaque_ty_kinds,
@@ -178,6 +248,8 @@ impl ProgramLowerer {
                 parameter_map: BTreeMap::new(),
                 auto_traits: &self.auto_traits,
                 foreign_ty_ids: &self.foreign_ty_ids,
+                associated_fn_lookups: &self.associated_fn_lookups,
+                associated_fn_value_lookups: &self.associated_fn_value_ids,
             };
 
             match *item {
@@ -213,30 +285,11 @@ impl ProgramLowerer {
                 Item::FnDefn(ref defn) => {
                     let identifier = defn.name.clone();
                     let fn_def_id = FnDefId(raw_id);
-                    fn_def_data.insert(fn_def_id, Arc::new((defn, fn_def_id).lower(&empty_env)?));
-                    let n_params = defn.all_parameters().len();
-                    let variances = match defn.variances.clone() {
-                        Some(v) => {
-                            if v.len() != n_params {
-                                return Err(RustIrError::IncorrectNumberOfVarianceParameters {
-                                    identifier,
-                                    expected: n_params,
-                                    actual: v.len(),
-                                });
-                            }
-                            v.into_iter()
-                                .map(|v| match v {
-                                    Variance::Invariant => chalk_ir::Variance::Invariant,
-                                    Variance::Covariant => chalk_ir::Variance::Covariant,
-                                    Variance::Contravariant => chalk_ir::Variance::Contravariant,
-                                })
-                                .collect()
-                        }
-                        None => (0..n_params)
-                            .map(|_| chalk_ir::Variance::Invariant)
-                            .collect(),
-                    };
-                    fn_def_variances.insert(fn_def_id, variances);
+                    fn_def_data.insert(
+                        fn_def_id,
+                        Arc::new(LowerFnDefn(defn, fn_def_id).lower(&empty_env)?),
+                    );
+                    process_fn_def(defn, fn_def_id, &identifier, defn.all_parameters().len())?;
                 }
                 Item::ClosureDefn(ref defn) => {
                     let closure_def_id = ClosureId(raw_id);
@@ -257,7 +310,7 @@ impl ProgramLowerer {
                 }
                 Item::TraitDefn(ref trait_defn) => {
                     let trait_id = TraitId(raw_id);
-                    let trait_datum = (trait_defn, trait_id).lower(&empty_env)?;
+                    let trait_datum = LowerTrait(trait_defn, trait_id).lower(&empty_env)?;
 
                     if let Some(well_known) = trait_datum.well_known {
                         well_known_traits.insert(well_known, trait_id);
@@ -293,7 +346,7 @@ impl ProgramLowerer {
                         variable_kinds.extend(trait_defn.all_parameters());
 
                         let binders = empty_env.in_binders(variable_kinds, |env| {
-                            Ok(rust_ir::AssociatedTyDatumBound {
+                            Ok(rust_ir::AssociatedItemDatumBound {
                                 bounds: assoc_ty_defn.bounds.lower(&env)?,
                                 where_clauses: assoc_ty_defn.where_clauses.lower(&env)?,
                             })
@@ -309,11 +362,51 @@ impl ProgramLowerer {
                             }),
                         );
                     }
+
+                    for assoc_fn_defn in &trait_defn.fn_defs {
+                        let fn_id = self.associated_fn_lookups
+                            [&(trait_id, assoc_fn_defn.name.str.clone())]
+                            .id;
+                        let identifier = assoc_fn_defn.name.clone();
+
+                        let mut variable_kinds = assoc_fn_defn.all_parameters();
+                        variable_kinds.extend(trait_defn.all_parameters());
+                        let n_params = variable_kinds.len();
+
+                        let binders = empty_env.in_binders(variable_kinds, |env| {
+                            let fn_datum = LowerFnDefn(assoc_fn_defn, fn_id.as_fn()).lower(&env)?;
+                            process_fn_def(assoc_fn_defn, fn_id.as_fn(), &identifier, n_params)?;
+                            fn_def_data.insert(fn_id.as_fn(), Arc::new(fn_datum));
+
+                            Ok(rust_ir::AssociatedItemDatumBound {
+                                // in the chalk language, functions can't have inline bounds
+                                bounds: Vec::new(),
+                                where_clauses: assoc_fn_defn.where_clauses.lower(&env)?,
+                            })
+                        })?;
+
+                        associated_fn_data.insert(
+                            fn_id,
+                            Arc::new(rust_ir::AssociatedFnDatum {
+                                name: assoc_fn_defn.name.str.clone(),
+                                trait_id,
+                                binders,
+                                // this wrapping is ok because it's known to be attached to a trait
+                                fn_id,
+                            }),
+                        );
+                    }
                 }
                 Item::Impl(ref impl_defn) => {
                     let impl_id = ImplId(raw_id);
                     let impl_datum = Arc::new(
-                        (impl_defn, impl_id, &self.associated_ty_value_ids).lower(&empty_env)?,
+                        LowerImpl(
+                            impl_defn,
+                            impl_id,
+                            &self.associated_ty_value_ids,
+                            &self.associated_fn_value_ids,
+                        )
+                        .lower(&empty_env)?,
                     );
                     impl_data.insert(impl_id, impl_datum.clone());
                     let trait_id = impl_datum.trait_id();
@@ -345,6 +438,36 @@ impl ProgramLowerer {
                             }),
                         );
                     }
+
+                    for fn_def in &impl_defn.fn_defs {
+                        let fn_name = &fn_def.name.str;
+                        let id = self.associated_fn_value_ids[&(impl_id, fn_name.clone())];
+                        let lookup_on_trait =
+                            &self.associated_fn_lookups[&(trait_id, fn_name.clone())];
+
+                        let mut variable_kinds = fn_def.all_parameters();
+                        variable_kinds.extend(impl_defn.all_parameters());
+                        let n_params = variable_kinds.len();
+
+                        tracing::debug!(?variable_kinds);
+
+                        let value = empty_env.in_binders(variable_kinds, |env| {
+                            let datum = LowerFnDefn(fn_def, id.as_fn()).lower(env)?;
+                            let fn_def_id =
+                                process_fn_def(fn_def, datum.id, &fn_def.name, n_params)?;
+
+                            Ok(fn_def_id)
+                        })?;
+
+                        associated_fn_values.insert(
+                            id,
+                            Arc::new(rust_ir::AssociatedFnValue {
+                                impl_id,
+                                fn_id: lookup_on_trait.id,
+                                value,
+                            }),
+                        );
+                    }
                 }
                 Item::Clause(ref clause) => {
                     custom_clauses.extend(clause.lower(&empty_env)?);
@@ -474,6 +597,7 @@ impl ProgramLowerer {
             closure_upvars,
             closure_kinds: self.closure_kinds,
             trait_ids: self.trait_ids,
+            impl_ids: self.impl_ids,
             adt_kinds: self.adt_kinds,
             fn_def_kinds: self.fn_def_kinds,
             trait_kinds: self.trait_kinds,
@@ -493,6 +617,8 @@ impl ProgramLowerer {
             impl_data,
             associated_ty_values,
             associated_ty_data,
+            associated_fn_values,
+            associated_fn_data,
             opaque_ty_ids: self.opaque_ty_ids,
             opaque_ty_kinds: self.opaque_ty_kinds,
             opaque_ty_data,
diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs
index a77d5d1915e..4c8dba78406 100644
--- a/chalk-integration/src/program.rs
+++ b/chalk-integration/src/program.rs
@@ -8,10 +8,12 @@ use chalk_ir::{
     OpaqueTyId, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, Scalar,
     Substitution, TraitId, Ty, TyKind, UintTy, Variances,
 };
+use chalk_ir::{AssocFnDefId, FnDefTy};
 use chalk_solve::rust_ir::{
-    AdtDatum, AdtRepr, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind,
-    FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum,
-    ImplType, OpaqueTyDatum, TraitDatum, WellKnownTrait,
+    AdtDatum, AdtRepr, AssociatedFnDatum, AssociatedFnValue, AssociatedFnValueId,
+    AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind, FnDefDatum,
+    FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum, ImplType,
+    OpaqueTyDatum, TraitDatum, WellKnownTrait,
 };
 use chalk_solve::split::Split;
 use chalk_solve::RustIrDatabase;
@@ -53,6 +55,9 @@ pub struct Program {
     /// From trait name to item-id. Used during lowering only.
     pub trait_ids: BTreeMap<Identifier, TraitId<ChalkIr>>,
 
+    /// From impl name to item-id. Used during lowering only.
+    pub impl_ids: BTreeMap<Identifier, ImplId<ChalkIr>>,
+
     /// For each trait:
     pub trait_kinds: BTreeMap<TraitId<ChalkIr>, TypeKind>,
 
@@ -76,6 +81,10 @@ pub struct Program {
     pub associated_ty_values:
         BTreeMap<AssociatedTyValueId<ChalkIr>, Arc<AssociatedTyValue<ChalkIr>>>,
 
+    /// For each associated fn value `fn foo() { ... }` found in an impl:
+    pub associated_fn_values:
+        BTreeMap<AssociatedFnValueId<ChalkIr>, Arc<AssociatedFnValue<ChalkIr>>>,
+
     // From opaque type name to item-id. Used during lowering only.
     pub opaque_ty_ids: BTreeMap<Identifier, OpaqueTyId<ChalkIr>>,
 
@@ -97,6 +106,9 @@ pub struct Program {
     /// For each associated ty declaration `type Foo` found in a trait:
     pub associated_ty_data: BTreeMap<AssocTypeId<ChalkIr>, Arc<AssociatedTyDatum<ChalkIr>>>,
 
+    /// For each associated fn declaration `fn foo()` found in a trait
+    pub associated_fn_data: BTreeMap<AssocFnDefId<ChalkIr>, Arc<AssociatedFnDatum<ChalkIr>>>,
+
     /// For each user-specified clause
     pub custom_clauses: Vec<ProgramClause<ChalkIr>>,
 
@@ -147,6 +159,26 @@ impl tls::DebugContext for Program {
         }
     }
 
+    fn debug_impl_id(
+        &self,
+        impl_id: ImplId<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        if let Some(name) = self
+            .impl_ids
+            .iter()
+            .find_map(|(iname, &iid)| (iid == impl_id).then(|| iname))
+        {
+            write!(fmt, "{{impl @{}}}", name)
+        } else if self.impl_data.contains_key(&impl_id) {
+            write!(fmt, "{{impl id {:?}}}", impl_id.0)
+        } else {
+            fmt.debug_struct("InvalidImplId")
+                .field("index", &impl_id.0)
+                .finish()
+        }
+    }
+
     fn debug_assoc_type_id(
         &self,
         assoc_type_id: AssocTypeId<ChalkIr>,
@@ -180,6 +212,17 @@ impl tls::DebugContext for Program {
         fn_def_id: FnDefId<ChalkIr>,
         fmt: &mut fmt::Formatter<'_>,
     ) -> Result<(), fmt::Error> {
+        if let Some(impl_item) = self
+            .associated_fn_values
+            .get(&AssociatedFnValueId(fn_def_id))
+        {
+            self.debug_impl_id(impl_item.impl_id, fmt)?;
+            write!(fmt, "::")?;
+        } else if let Some(trait_item) = self.associated_fn_data.get(&AssocFnDefId(fn_def_id)) {
+            self.debug_trait_id(trait_item.trait_id, fmt)?;
+            write!(fmt, "::")?;
+        }
+
         if let Some(k) = self.fn_def_kinds.get(&fn_def_id) {
             write!(fmt, "{}", k.name)
         } else {
@@ -388,6 +431,10 @@ impl RustIrDatabase<ChalkIr> for Program {
         self.associated_ty_data[&ty].clone()
     }
 
+    fn associated_fn_data(&self, f: AssocFnDefId<ChalkIr>) -> Arc<AssociatedFnDatum<ChalkIr>> {
+        self.associated_fn_data[&f].clone()
+    }
+
     fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
         self.trait_data[&id].clone()
     }
@@ -403,6 +450,13 @@ impl RustIrDatabase<ChalkIr> for Program {
         self.associated_ty_values[&id].clone()
     }
 
+    fn associated_fn_value(
+        &self,
+        id: AssociatedFnValueId<ChalkIr>,
+    ) -> Arc<AssociatedFnValue<ChalkIr>> {
+        self.associated_fn_values[&id].clone()
+    }
+
     fn opaque_ty_data(&self, id: OpaqueTyId<ChalkIr>) -> Arc<OpaqueTyDatum<ChalkIr>> {
         self.opaque_ty_data[&id].clone()
     }
@@ -499,7 +553,14 @@ impl RustIrDatabase<ChalkIr> for Program {
                 (TyKind::Tuple(arity_a, _), TyKind::Tuple(arity_b, _)) => arity_a == arity_b,
                 (TyKind::OpaqueType(id_a, _), TyKind::OpaqueType(id_b, _)) => id_a == id_b,
                 (TyKind::Slice(_), TyKind::Slice(_)) => true,
-                (TyKind::FnDef(id_a, _), TyKind::FnDef(id_b, _)) => id_a == id_b,
+                (
+                    TyKind::FnDef(FnDefTy {
+                        fn_def_id: id_a, ..
+                    }),
+                    TyKind::FnDef(FnDefTy {
+                        fn_def_id: id_b, ..
+                    }),
+                ) => id_a == id_b,
                 (TyKind::Ref(id_a, _, _), TyKind::Ref(id_b, _, _)) => id_a == id_b,
                 (TyKind::Raw(id_a, _), TyKind::Raw(id_b, _)) => id_a == id_b,
                 (TyKind::Never, TyKind::Never) => true,
diff --git a/chalk-integration/src/tls.rs b/chalk-integration/src/tls.rs
index 58b1da3dfa8..e44505636e2 100644
--- a/chalk-integration/src/tls.rs
+++ b/chalk-integration/src/tls.rs
@@ -1,4 +1,5 @@
 use crate::interner::ChalkIr;
+use chalk_ir::ImplId;
 use chalk_ir::{
     debug::SeparatorTraitRef, AdtId, AliasTy, AssocTypeId, CanonicalVarKinds, Constraints, FnDefId,
     GenericArg, Goal, Goals, Lifetime, OpaqueTy, OpaqueTyId, ProgramClause,
@@ -26,6 +27,12 @@ pub trait DebugContext {
         fmt: &mut fmt::Formatter<'_>,
     ) -> Result<(), fmt::Error>;
 
+    fn debug_impl_id(
+        &self,
+        id: ImplId<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
     fn debug_assoc_type_id(
         &self,
         id: AssocTypeId<ChalkIr>,
diff --git a/chalk-ir/src/could_match.rs b/chalk-ir/src/could_match.rs
index e0da91e34e2..36d232d3257 100644
--- a/chalk-ir/src/could_match.rs
+++ b/chalk-ir/src/could_match.rs
@@ -73,8 +73,14 @@ where
                         ty_a.could_match(interner, self.db, ty_b)
                     }
                     (
-                        TyKind::FnDef(fn_def_a, substitution_a),
-                        TyKind::FnDef(fn_def_b, substitution_b),
+                        TyKind::FnDef(FnDefTy {
+                            fn_def_id: fn_def_a,
+                            substitution: substitution_a,
+                        }),
+                        TyKind::FnDef(FnDefTy {
+                            fn_def_id: fn_def_b,
+                            substitution: substitution_b,
+                        }),
                     ) => {
                         fn_def_a == fn_def_b
                             && self
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 4a13346d203..a8bf4679373 100644
--- a/chalk-ir/src/debug.rs
+++ b/chalk-ir/src/debug.rs
@@ -10,6 +10,12 @@ impl<I: Interner> Debug for TraitId<I> {
     }
 }
 
+impl<I: Interner> Debug for ImplId<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> std::fmt::Result {
+        I::debug_impl_id(*self, fmt).unwrap_or_else(|| write!(fmt, "ImplId({:?})", self.0))
+    }
+}
+
 impl<I: Interner> Debug for AdtId<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         I::debug_adt_id(*self, fmt).unwrap_or_else(|| write!(fmt, "AdtId({:?})", self.0))
@@ -23,6 +29,13 @@ impl<I: Interner> Debug for AssocTypeId<I> {
     }
 }
 
+impl<I: Interner> Debug for AssocFnDefId<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> std::fmt::Result {
+        I::debug_assoc_fn_def_id(*self, fmt)
+            .unwrap_or_else(|| write!(fmt, "AssocFnDefId({:?})", self.0))
+    }
+}
+
 impl<I: Interner> Debug for FnDefId<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> std::fmt::Result {
         I::debug_fn_def_id(*self, fmt).unwrap_or_else(|| write!(fmt, "FnDefId({:?})", self.0))
@@ -144,6 +157,13 @@ impl<I: Interner> Debug for ProjectionTy<I> {
     }
 }
 
+impl<I: Interner> Debug for FnDefTy<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_fn_def_ty(self, fmt)
+            .unwrap_or_else(|| write!(fmt, "{:?} {:?}", self.fn_def_id, self.substitution))
+    }
+}
+
 impl<I: Interner> Debug for OpaqueTy<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         I::debug_opaque_ty(self, fmt).unwrap_or_else(|| {
@@ -204,7 +224,10 @@ impl<I: Interner> Debug for TyKind<I> {
                 write!(fmt, "!{:?}<{:?}>", opaque_ty, substitution)
             }
             TyKind::Slice(substitution) => write!(fmt, "{{slice}}<{:?}>", substitution),
-            TyKind::FnDef(fn_def, substitution) => write!(fmt, "{:?}<{:?}>", fn_def, substitution),
+            TyKind::FnDef(FnDefTy {
+                fn_def_id,
+                substitution,
+            }) => write!(fmt, "{:?}<{:?}>", fn_def_id, substitution),
             TyKind::Ref(mutability, lifetime, ty) => match mutability {
                 Mutability::Mut => write!(fmt, "(&{:?} mut {:?})", lifetime, ty),
                 Mutability::Not => write!(fmt, "(&{:?} {:?})", lifetime, ty),
@@ -506,8 +529,16 @@ impl<'a, I: Interner> Debug for TyKindDebug<'a, I> {
                 substitution.with_angle(interner)
             ),
             TyKind::Slice(ty) => write!(fmt, "[{:?}]", ty),
-            TyKind::FnDef(fn_def, substitution) => {
-                write!(fmt, "{:?}{:?}", fn_def, substitution.with_angle(interner))
+            TyKind::FnDef(FnDefTy {
+                fn_def_id,
+                substitution,
+            }) => {
+                write!(
+                    fmt,
+                    "{:?}{:?}",
+                    fn_def_id,
+                    substitution.with_angle(interner)
+                )
             }
             TyKind::Ref(mutability, lifetime, ty) => match mutability {
                 Mutability::Mut => write!(fmt, "(&{:?} mut {:?})", lifetime, ty),
@@ -808,6 +839,7 @@ impl<I: Interner> Debug for DomainGoal<I> {
             DomainGoal::WellFormed(n) => write!(fmt, "{:?}", n),
             DomainGoal::FromEnv(n) => write!(fmt, "{:?}", n),
             DomainGoal::Normalize(n) => write!(fmt, "{:?}", n),
+            DomainGoal::NormalizeFn(a, b) => write!(fmt, "NormalizeFn({:?}, {:?})", a, b),
             DomainGoal::IsLocal(n) => write!(fmt, "IsLocal({:?})", n),
             DomainGoal::IsUpstream(n) => write!(fmt, "IsUpstream({:?})", n),
             DomainGoal::IsFullyVisible(n) => write!(fmt, "IsFullyVisible({:?})", n),
diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs
index 426164539d9..7794ba4b873 100644
--- a/chalk-ir/src/fold.rs
+++ b/chalk-ir/src/fold.rs
@@ -426,10 +426,13 @@ where
                 TyKind::Slice(substitution.clone().fold_with(folder, outer_binder)?)
                     .intern(folder.interner())
             }
-            TyKind::FnDef(fn_def, substitution) => TyKind::FnDef(
-                fn_def.fold_with(folder, outer_binder)?,
-                substitution.clone().fold_with(folder, outer_binder)?,
-            )
+            TyKind::FnDef(FnDefTy {
+                fn_def_id,
+                substitution,
+            }) => TyKind::FnDef(FnDefTy {
+                fn_def_id: fn_def_id.fold_with(folder, outer_binder)?,
+                substitution: substitution.clone().fold_with(folder, outer_binder)?,
+            })
             .intern(folder.interner()),
             TyKind::Ref(mutability, lifetime, ty) => TyKind::Ref(
                 mutability.fold_with(folder, outer_binder)?,
diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs
index 7c019216958..cce7dd65d04 100644
--- a/chalk-ir/src/fold/boring_impls.rs
+++ b/chalk-ir/src/fold/boring_impls.rs
@@ -251,6 +251,7 @@ id_fold!(TraitId);
 id_fold!(AssocTypeId);
 id_fold!(OpaqueTyId);
 id_fold!(FnDefId);
+id_fold!(AssocFnDefId);
 id_fold!(ClosureId);
 id_fold!(GeneratorId);
 id_fold!(ForeignDefId);
diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs
index 90bd98f95ae..410a5003898 100644
--- a/chalk-ir/src/interner.rs
+++ b/chalk-ir/src/interner.rs
@@ -1,5 +1,6 @@
 //! Encapsulates the concrete representation of core types such as types and goals.
 use crate::AliasTy;
+use crate::AssocFnDefId;
 use crate::AssocTypeId;
 use crate::CanonicalVarKind;
 use crate::CanonicalVarKinds;
@@ -7,6 +8,7 @@ use crate::ClosureId;
 use crate::Constraint;
 use crate::Constraints;
 use crate::FnDefId;
+use crate::FnDefTy;
 use crate::ForeignDefId;
 use crate::GeneratorId;
 use crate::GenericArg;
@@ -14,6 +16,7 @@ use crate::GenericArgData;
 use crate::Goal;
 use crate::GoalData;
 use crate::Goals;
+use crate::ImplId;
 use crate::InEnvironment;
 use crate::Lifetime;
 use crate::LifetimeData;
@@ -60,36 +63,40 @@ use std::sync::Arc;
 pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     /// "Interned" representation of types.  In normal user code,
     /// `Self::InternedType` is not referenced. Instead, we refer to
-    /// `Ty<Self>`, which wraps this type.
+    /// [`Ty<Self>`], which wraps this type.
     ///
     /// An `InternedType` must be something that can be created from a
-    /// `TyKind` (by the [`intern_ty`] method) and then later
-    /// converted back (by the [`ty_data`] method). The interned form
-    /// must also introduce indirection, either via a `Box`, `&`, or
-    /// other pointer type.
+    /// [`TyKind`] (by the [`intern_ty`](Interner::intern_ty) method) and
+    /// then later converted back (by the [`ty_data`](Interner::ty_data)
+    /// method). The interned form must also introduce indirection,
+    /// either via a `Box`, `&`, or other pointer type.
     type InternedType: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of lifetimes.  In normal user code,
     /// `Self::InternedLifetime` is not referenced. Instead, we refer to
-    /// `Lifetime<Self>`, which wraps this type.
+    /// [`Lifetime<Self>`], which wraps this type.
     ///
-    /// An `InternedLifetime` must be something that can be created
-    /// from a `LifetimeData` (by the [`intern_lifetime`] method) and
-    /// then later converted back (by the [`lifetime_data`] method).
+    /// An `InternedLifetime` must be something that can be created from
+    /// a [`LifetimeData`] (by the
+    /// [`intern_lifetime`](Interner::intern_lifetime) method) and then
+    /// later converted back (by the
+    /// [`lifetime_data`](Interner::lifetime_data) method).
     type InternedLifetime: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of const expressions. In normal user code,
     /// `Self::InternedConst` is not referenced. Instead, we refer to
-    /// `Const<Self>`, which wraps this type.
+    /// [`Const<Self>`], which wraps this type.
     ///
-    /// An `InternedConst` must be something that can be created
-    /// from a `ConstData` (by the [`intern_const`] method) and
-    /// then later converted back (by the [`const_data`] method).
+    /// An `InternedConst` must be something that can be created from a
+    /// [`ConstData`] (by the [`intern_const`](Interner::intern_const)
+    /// method) and then later converted back (by the
+    /// [`const_data`](Interner::const_data) method).
     type InternedConst: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of an evaluated const value.
     /// `Self::InternedConcreteConst` is not referenced. Instead,
-    /// we refer to `ConcreteConst<Self>`, which wraps this type.
+    /// we refer to [`ConcreteConst<Self>`](chalk_ir::ConcreteConst),
+    /// which wraps this type.
     ///
     /// `InternedConcreteConst` instances are not created by chalk,
     /// it can only make a query asking about equality of two
@@ -99,92 +106,111 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     /// "Interned" representation of a "generic parameter", which can
     /// be either a type or a lifetime.  In normal user code,
     /// `Self::InternedGenericArg` is not referenced. Instead, we refer to
-    /// `GenericArg<Self>`, which wraps this type.
+    /// [`GenericArg<Self>`], which wraps this type.
     ///
-    /// An `InternedType` is created by `intern_generic_arg` and can be
-    /// converted back to its underlying data via `generic_arg_data`.
+    /// An `InternedType` is created by
+    /// [`intern_generic_arg`](Self::intern_generic_arg) and can be
+    /// converted back to its underlying data via
+    /// [`generic_arg_data`](Self::generic_arg_data).
     type InternedGenericArg: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a "goal".  In normal user code,
     /// `Self::InternedGoal` is not referenced. Instead, we refer to
-    /// `Goal<Self>`, which wraps this type.
+    /// [`Goal<Self>`], which wraps this type.
     ///
-    /// An `InternedGoal` is created by `intern_goal` and can be
-    /// converted back to its underlying data via `goal_data`.
+    /// An `InternedGoal` is created by
+    /// [`intern_goal`](Self::intern_goal) and can be
+    /// converted back to its underlying [`GoalData`] via
+    /// [`goal_data`](Self::goal_data).
     type InternedGoal: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a list of goals.  In normal user code,
     /// `Self::InternedGoals` is not referenced. Instead, we refer to
-    /// `Goals<Self>`, which wraps this type.
+    /// [`Goals<Self>`], which wraps this type.
     ///
-    /// An `InternedGoals` is created by `intern_goals` and can be
-    /// converted back to its underlying data via `goals_data`.
+    /// An `InternedGoals` is created by
+    /// [`intern_goals`](Self::intern_goals) and can be converted back
+    /// to its underlying data via [`goals_data`](Self::goals_data).
     type InternedGoals: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a "substitution".  In normal user code,
     /// `Self::InternedSubstitution` is not referenced. Instead, we refer to
-    /// `Substitution<Self>`, which wraps this type.
+    /// [`Substitution<Self>`], which wraps this type.
     ///
-    /// An `InternedSubstitution` is created by `intern_substitution` and can be
-    /// converted back to its underlying data via `substitution_data`.
+    /// An `InternedSubstitution` is created by
+    /// [`intern_substitution`](Self::intern_substitution) and can be
+    /// converted back to its underlying data via
+    /// [`substitution_data`](Self::substitution_data).
     type InternedSubstitution: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a list of program clauses.  In normal user code,
     /// `Self::InternedProgramClauses` is not referenced. Instead, we refer to
-    /// `ProgramClauses<Self>`, which wraps this type.
+    /// [`ProgramClauses<Self>`], which wraps this type.
     ///
-    /// An `InternedProgramClauses` is created by `intern_program_clauses` and can be
-    /// converted back to its underlying data via `program_clauses_data`.
+    /// An `InternedProgramClauses` is created by
+    /// [`intern_program_clauses`](Self::intern_program_clauses) and can
+    /// be converted back to its underlying data via
+    /// [`program_clauses_data`](Self::program_clauses_data).
     type InternedProgramClauses: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a "program clause".  In normal user code,
     /// `Self::InternedProgramClause` is not referenced. Instead, we refer to
-    /// `ProgramClause<Self>`, which wraps this type.
+    /// [`ProgramClause<Self>`], which wraps this type.
     ///
-    /// An `InternedProgramClause` is created by `intern_program_clause` and can be
-    /// converted back to its underlying data via `program_clause_data`.
+    /// An `InternedProgramClause` is created by
+    /// [`intern_program_clause`](Self::intern_program_clause) and can
+    /// be converted back to its underlying data via
+    /// [`program_clause_data`](Self::program_clause_data).
     type InternedProgramClause: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a list of quantified where clauses.
     /// In normal user code, `Self::InternedQuantifiedWhereClauses` is not referenced.
-    /// Instead, we refer to `QuantifiedWhereClauses<Self>`, which wraps this type.
+    /// Instead, we refer to [`QuantifiedWhereClauses<Self>`], which wraps this type.
     ///
-    /// An `InternedQuantifiedWhereClauses` is created by `intern_quantified_where_clauses`
-    /// and can be converted back to its underlying data via `quantified_where_clauses_data`.
+    /// An `InternedQuantifiedWhereClauses` is created by
+    /// [`intern_quantified_where_clauses`](Self::intern_quantified_where_clauses)
+    /// and can be converted back to its underlying data via
+    /// [`quantified_where_clauses_data`](Self::quantified_where_clauses_data).
     type InternedQuantifiedWhereClauses: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a list of variable kinds.
     /// In normal user code, `Self::InternedVariableKinds` is not referenced.
-    /// Instead, we refer to `VariableKinds<Self>`, which wraps this type.
+    /// Instead, we refer to [`VariableKinds<Self>`], which wraps this type.
     ///
-    /// An `InternedVariableKinds` is created by `intern_generic_arg_kinds`
-    /// and can be converted back to its underlying data via `variable_kinds_data`.
+    /// An `InternedVariableKinds` is created by
+    /// [`intern_generic_arg_kinds`](Self::intern_generic_arg_kinds) and
+    /// can be converted back to its underlying data via
+    /// [`variable_kinds_data`](Self::variable_kinds_data).
     type InternedVariableKinds: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a list of variable kinds with universe index.
     /// In normal user code, `Self::InternedCanonicalVarKinds` is not referenced.
-    /// Instead, we refer to `CanonicalVarKinds<Self>`, which wraps this type.
+    /// Instead, we refer to [`CanonicalVarKinds<Self>`], which wraps this type.
     ///
     /// An `InternedCanonicalVarKinds` is created by
-    /// `intern_canonical_var_kinds` and can be converted back
-    /// to its underlying data via `canonical_var_kinds_data`.
+    /// [`intern_canonical_var_kinds`](Self::intern_canonical_var_kinds)
+    /// and can be converted back to its underlying data via
+    /// [`canonical_var_kinds_data`](Self::canonical_var_kinds_data).
     type InternedCanonicalVarKinds: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a list of region constraints.
     /// In normal user code, `Self::InternedConstraints` is not referenced.
-    /// Instead, we refer to `Constraints<Self>`, which wraps this type.
+    /// Instead, we refer to [`Constraints<Self>`], which wraps this type.
     ///
-    /// An `InternedConstraints` is created by `intern_constraints`
-    /// and can be converted back to its underlying data via `constraints_data`.
+    /// An `InternedConstraints` is created by
+    /// [`intern_constraints`](Self::intern_constraints) and can be
+    /// converted back to its underlying data via
+    /// [`constraints_data`](Self::constraints_data).
     type InternedConstraints: Debug + Clone + Eq + Hash;
 
     /// "Interned" representation of a list of `chalk_ir::Variance`.
     /// In normal user code, `Self::InternedVariances` is not referenced.
-    /// Instead, we refer to `Variances<Self>`, which wraps this type.
+    /// Instead, we refer to [`Variances<Self>`], which wraps this type.
     ///
     /// An `InternedVariances` is created by
-    /// `intern_variances` and can be converted back
-    /// to its underlying data via `variances_data`.
+    /// [`intern_variances`](Self::intern_variances) and can be
+    /// converted back to its underlying data via
+    /// [`variances_data`](Self::variances_data).
     type InternedVariances: Debug + Clone + Eq + Hash;
 
     /// The core "id" type used for trait-ids and the like.
@@ -206,7 +232,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a type-kind-id.
+    /// Prints the debug representation of a trait id.
     /// Returns `None` to fallback to the default debug output (e.g.,
     /// if no info about current program is available from TLS).
     #[allow(unused_variables)]
@@ -217,7 +243,15 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a type-kind-id.
+    /// Prints the debug representation of an impl id.
+    /// Returns `None` to fallback to the default debug output (e.g.,
+    /// if no info about current program is available from TLS).
+    #[allow(unused_variables)]
+    fn debug_impl_id(impl_id: ImplId<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
+        None
+    }
+
+    /// Prints the debug representation of a associated type id.
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_assoc_type_id(
@@ -227,6 +261,16 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
+    /// Prints the debug representation of an associated-function-def-id.
+    /// Returns `None` to fallback to the default debug output.
+    #[allow(unused_variables)]
+    fn debug_assoc_fn_def_id(
+        fn_def_id: AssocFnDefId<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
     /// Prints the debug representation of an opaque type.
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
@@ -267,7 +311,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of an alias.
+    /// Prints the debug representation of a generator.
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_generator_id(
@@ -289,7 +333,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a ProjectionTy.
+    /// Prints the debug representation of a [`ProjectionTy`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_projection_ty(
@@ -299,7 +343,17 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of an OpaqueTy.
+    /// Prints the debug representation of a [`FnDefTy`]
+    /// Returns `None` to fallback to the default debug output.
+    #[allow(unused_variables)]
+    fn debug_fn_def_ty(
+        fn_def_ty: &FnDefTy<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
+    /// Prints the debug representation of an [`OpaqueTy`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_opaque_ty(
@@ -309,14 +363,14 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a type.
+    /// Prints the debug representation of a [`Ty`]pe.
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_ty(ty: &Ty<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
         None
     }
 
-    /// Prints the debug representation of a lifetime.
+    /// Prints the debug representation of a [`Lifetime`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_lifetime(
@@ -326,7 +380,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a const.
+    /// Prints the debug representation of a [`Const`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_const(constant: &Const<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
@@ -373,22 +427,23 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of an goal.
+    /// Prints the debug representation of a [`Goal`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_goal(goal: &Goal<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
         None
     }
 
-    /// Prints the debug representation of a list of goals.
+    /// Prints the debug representation of a list of [`Goals`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_goals(goals: &Goals<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
         None
     }
 
-    /// Prints the debug representation of a ProgramClauseImplication.
-    /// Returns `None` to fallback to the default debug output.
+    /// Prints the debug representation of a
+    /// [`ProgramClauseImplication`]. Returns `None` to fallback to the
+    /// default debug output.
     #[allow(unused_variables)]
     fn debug_program_clause_implication(
         pci: &ProgramClauseImplication<Self>,
@@ -397,7 +452,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a ProgramClause.
+    /// Prints the debug representation of a [`ProgramClause`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_program_clause(
@@ -407,7 +462,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a ProgramClauses.
+    /// Prints the debug representation of a [`ProgramClauses`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_program_clauses(
@@ -417,7 +472,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a Substitution.
+    /// Prints the debug representation of a [`Substitution`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_substitution(
@@ -427,7 +482,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a SeparatorTraitRef.
+    /// Prints the debug representation of a [`SeparatorTraitRef`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_separator_trait_ref(
@@ -437,7 +492,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Prints the debug representation of a QuantifiedWhereClauses.
+    /// Prints the debug representation of a [`QuantifiedWhereClauses`].
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]
     fn debug_quantified_where_clauses(
@@ -467,30 +522,31 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
-    /// Create an "interned" type from `ty`. This is not normally
-    /// invoked directly; instead, you invoke `TyKind::intern` (which
+    /// Create an "interned" type from `kind`. This is not normally
+    /// invoked directly; instead, you invoke [`TyKind::intern`] (which
     /// will ultimately call this method).
     fn intern_ty(&self, kind: TyKind<Self>) -> Self::InternedType;
 
-    /// Lookup the `TyKind` from an interned type.
+    /// Lookup the [`TyKind`] from an interned type.
     fn ty_data<'a>(&self, ty: &'a Self::InternedType) -> &'a TyData<Self>;
 
     /// Create an "interned" lifetime from `lifetime`. This is not
     /// normally invoked directly; instead, you invoke
-    /// `LifetimeData::intern` (which will ultimately call this
+    /// [`LifetimeData::intern`] (which will ultimately call this
     /// method).
     fn intern_lifetime(&self, lifetime: LifetimeData<Self>) -> Self::InternedLifetime;
 
-    /// Lookup the `LifetimeData` that was interned to create a `InternedLifetime`.
+    /// Lookup the [`LifetimeData`] that was interned to create a
+    /// [`InternedLifetime`](Self::InternedLifetime).
     fn lifetime_data<'a>(&self, lifetime: &'a Self::InternedLifetime) -> &'a LifetimeData<Self>;
 
-    /// Create an "interned" const from `const`. This is not
-    /// normally invoked directly; instead, you invoke
-    /// `ConstData::intern` (which will ultimately call this
-    /// method).
+    /// Create an "interned" const from `constant`. This is not normally
+    /// invoked directly; instead, you invoke [`ConstData::intern`]
+    /// (which will ultimately call this method).
     fn intern_const(&self, constant: ConstData<Self>) -> Self::InternedConst;
 
-    /// Lookup the `ConstData` that was interned to create a `InternedConst`.
+    /// Lookup the [`ConstData`] that was interned to create a
+    /// [`InternedConst`](Self::InternedConst).
     fn const_data<'a>(&self, constant: &'a Self::InternedConst) -> &'a ConstData<Self>;
 
     /// Determine whether two concrete const values are equal.
@@ -503,11 +559,12 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
 
     /// Create an "interned" parameter from `data`. This is not
     /// normally invoked directly; instead, you invoke
-    /// `GenericArgData::intern` (which will ultimately call this
+    /// [`GenericArgData::intern`] (which will ultimately call this
     /// method).
     fn intern_generic_arg(&self, data: GenericArgData<Self>) -> Self::InternedGenericArg;
 
-    /// Lookup the `LifetimeData` that was interned to create a `InternedLifetime`.
+    /// Lookup the [`GenericArgData`] that was interned to create a
+    /// [`InternedGenericArg`](Self::InternedGenericArg).
     fn generic_arg_data<'a>(
         &self,
         lifetime: &'a Self::InternedGenericArg,
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
index 70a29fee9fa..90c81de72b4 100644
--- a/chalk-ir/src/lib.rs
+++ b/chalk-ir/src/lib.rs
@@ -301,7 +301,7 @@ pub enum Mutability {
 /// `forall<T> { Goal(T) }` (syntactical representation)
 /// `forall { Goal(?0) }` (used a DeBruijn index)
 /// `Goal(!U1)` (the quantifier was moved to the environment and replaced with a universe index)
-/// See https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference.html#placeholders-and-universes for more.
+/// See <https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference.html#placeholders-and-universes> for more.
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct UniverseIndex {
     /// The counter for the universe index, starts with 0.
@@ -376,19 +376,31 @@ pub struct ImplId<I: Interner>(pub I::DefId);
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct ClauseId<I: Interner>(pub I::DefId);
 
-/// The id for the associated type member of a trait. The details of the type
-/// can be found by invoking the [`associated_ty_data`] method.
+/// The id for the associated type member of a trait. The details of the
+/// type can be found by invoking the [`associated_ty_data`] method.
 ///
 /// [`associated_ty_data`]: ../chalk_solve/trait.RustIrDatabase.html#tymethod.associated_ty_data
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct AssocTypeId<I: Interner>(pub I::DefId);
 
+/// The ID of an associated function on a trait. This is a special case
+/// of a [`FnDefId`].
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct AssocFnDefId<I: Interner>(pub FnDefId<I>);
+
+impl<I: Interner> AssocFnDefId<I> {
+    /// Gets the function definition ID for this associated function
+    pub fn as_fn(self) -> FnDefId<I> {
+        self.0
+    }
+}
+
 /// Id for an opaque type.
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct OpaqueTyId<I: Interner>(pub I::DefId);
 
 /// Function definition id.
-#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, HasInterner)]
 pub struct FnDefId<I: Interner>(pub I::DefId);
 
 /// Id for Rust closures.
@@ -403,16 +415,16 @@ pub struct GeneratorId<I: Interner>(pub I::DefId);
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct ForeignDefId<I: Interner>(pub I::DefId);
 
-impl_debugs!(ImplId, ClauseId);
+impl_debugs!(ClauseId);
 
-/// A Rust type. The actual type data is stored in `TyKind`.
+/// A Rust type. The actual type data is stored in [`TyKind`].
 #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
 pub struct Ty<I: Interner> {
     interned: I::InternedType,
 }
 
 impl<I: Interner> Ty<I> {
-    /// Creates a type from `TyKind`.
+    /// Creates a type from [`TyKind`].
     pub fn new(interner: &I, data: impl CastTo<TyKind<I>>) -> Self {
         let ty_kind = data.cast(&interner);
         Ty {
@@ -611,7 +623,7 @@ pub enum TyKind<I: Interner> {
     OpaqueType(OpaqueTyId<I>, Substitution<I>),
 
     /// a function definition
-    FnDef(FnDefId<I>, Substitution<I>),
+    FnDef(FnDefTy<I>),
 
     /// the string primitive type
     Str,
@@ -686,7 +698,7 @@ impl<I: Interner> TyKind<I> {
         Ty::new(interner, self)
     }
 
-    /// Compute type flags for a TyKind
+    /// Compute type flags for a [`TyKind`]
     pub fn compute_flags(&self, interner: &I) -> TypeFlags {
         match self {
             TyKind::Adt(_, substitution)
@@ -695,7 +707,7 @@ impl<I: Interner> TyKind<I> {
             | TyKind::Closure(_, substitution)
             | TyKind::Generator(_, substitution)
             | TyKind::GeneratorWitness(_, substitution)
-            | TyKind::FnDef(_, substitution)
+            | TyKind::FnDef(FnDefTy { substitution, .. })
             | TyKind::OpaqueType(_, substitution) => substitution.compute_flags(interner),
             TyKind::Scalar(_) | TyKind::Str | TyKind::Never | TyKind::Foreign(_) => {
                 TypeFlags::empty()
@@ -1287,7 +1299,7 @@ impl<I: Interner> Lifetime<I> {
         }
     }
 
-    ///compute type flags for Lifetime
+    ///compute type flags for [`Lifetime`]
     fn compute_flags(&self, interner: &I) -> TypeFlags {
         match self.data(&interner) {
             LifetimeData::InferenceVar(_) => {
@@ -1424,14 +1436,14 @@ impl<I: Interner> VariableKind<I> {
     }
 }
 
-/// A generic argument, see `GenericArgData` for more information.
+/// A generic argument, see [`GenericArgData`] for more information.
 #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
 pub struct GenericArg<I: Interner> {
     interned: I::InternedGenericArg,
 }
 
 impl<I: Interner> GenericArg<I> {
-    /// Constructs a generic argument using `GenericArgData`.
+    /// Constructs a generic argument using [`GenericArgData`].
     pub fn new(interner: &I, data: GenericArgData<I>) -> Self {
         let interned = I::intern_generic_arg(interner, data);
         GenericArg { interned }
@@ -1495,7 +1507,7 @@ impl<I: Interner> GenericArg<I> {
         }
     }
 
-    /// Compute type flags for GenericArg<I>
+    /// Compute type flags for [`GenericArg<I>`]
     fn compute_flags(&self, interner: &I) -> TypeFlags {
         match self.data(&interner) {
             GenericArgData::Ty(ty) => ty.data(interner).flags,
@@ -1657,6 +1669,28 @@ impl<I: Interner> ProjectionTy<I> {
     }
 }
 
+/// A function definition item
+/// ```
+/// struct S;
+/// trait T {
+///     fn fun<X>() -> u32;
+/// }
+/// impl T for S {
+///     fn fun<X>() -> u32 {1}
+///     // ^^^ ^
+/// }
+/// ```
+#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)]
+pub struct FnDefTy<I: Interner> {
+    /// The id for the function definition
+    pub fn_def_id: FnDefId<I>,
+
+    /// Generic parameters for the function
+    pub substitution: Substitution<I>,
+}
+
+impl<I: Interner> Copy for FnDefTy<I> where I::InternedSubstitution: Copy {}
+
 /// An opaque type `opaque type T<..>: Trait = HiddenTy`.
 #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]
 pub struct OpaqueTy<I: Interner> {
@@ -1850,6 +1884,12 @@ pub enum DomainGoal<I: Interner> {
     /// True if the alias type can be normalized to some other type
     Normalize(Normalize<I>),
 
+    /// True if the [`FnDefTy`] can be normalized to the given function type.
+    ///
+    /// `.1` can in practice only be [`TyKind::BoundVar`],
+    /// [`TyKind::InferenceVar`] or [`TyKind::FnDef`].
+    NormalizeFn(FnDefTy<I>, Ty<I>),
+
     /// True if a type is considered to have been "defined" by the current crate. This is true for
     /// a `struct Foo { }` but false for a `#[upstream] struct Foo { }`. However, for fundamental types
     /// like `Box<T>`, it is true if `T` is local.
@@ -2104,7 +2144,7 @@ impl<T: HasInterner> Binders<T> {
     /// do with bound vars, or you are being very careful about
     /// your depth accounting.
     ///
-    /// Some examples where `skip_binder` is reasonable:
+    /// Some examples where `skip_binders` is reasonable:
     ///
     /// - extracting the `TraitId` from a TraitRef;
     /// - checking if there are any fields in a StructDatum
@@ -2113,7 +2153,7 @@ impl<T: HasInterner> Binders<T> {
     }
 
     /// Skips the binder and returns the "bound" value as well as the skipped free variables. This
-    /// is just as risky as [`skip_binders`].
+    /// is just as risky as [`skip_binders`](Self::skip_binders).
     pub fn into_value_and_skipped_binders(self) -> (T, VariableKinds<T::Interner>) {
         (self.value, self.binders)
     }
@@ -2366,6 +2406,8 @@ impl<I: Interner> ProgramClauseData<I> {
 }
 
 /// A program clause is a logic expression used to describe a part of the program.
+///
+/// See [`ProgramClauseData`] for the interned data.
 #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
 pub struct ProgramClause<I: Interner> {
     interned: I::InternedProgramClause,
@@ -2730,7 +2772,7 @@ impl<I: Interner> Substitution<I> {
             .cloned()
     }
 
-    /// Compute type flags for Substitution<I>
+    /// Compute type flags for [`Substitution<I>`]
     fn compute_flags(&self, interner: &I) -> TypeFlags {
         let mut flags = TypeFlags::empty();
         for generic_arg in self.iter(&interner) {
diff --git a/chalk-ir/src/visit.rs b/chalk-ir/src/visit.rs
index c7180d76966..efddb0d2c35 100644
--- a/chalk-ir/src/visit.rs
+++ b/chalk-ir/src/visit.rs
@@ -2,8 +2,8 @@
 use std::fmt::Debug;
 
 use crate::{
-    BoundVar, Const, ConstValue, DebruijnIndex, DomainGoal, Goal, InferenceVar, Interner, Lifetime,
-    LifetimeData, PlaceholderIndex, ProgramClause, Ty, TyKind, WhereClause,
+    BoundVar, Const, ConstValue, DebruijnIndex, DomainGoal, FnDefTy, Goal, InferenceVar, Interner,
+    Lifetime, LifetimeData, PlaceholderIndex, ProgramClause, Ty, TyKind, WhereClause,
 };
 
 mod binder_impls;
@@ -321,8 +321,11 @@ where
                 substitution.visit_with(visitor, outer_binder)
             }
             TyKind::Slice(substitution) => substitution.visit_with(visitor, outer_binder),
-            TyKind::FnDef(fn_def, substitution) => {
-                try_break!(fn_def.visit_with(visitor, outer_binder));
+            TyKind::FnDef(FnDefTy {
+                fn_def_id,
+                substitution,
+            }) => {
+                try_break!(fn_def_id.visit_with(visitor, outer_binder));
                 substitution.visit_with(visitor, outer_binder)
             }
             TyKind::Ref(mutability, lifetime, ty) => {
diff --git a/chalk-ir/src/visit/boring_impls.rs b/chalk-ir/src/visit/boring_impls.rs
index eef58ddb3ca..c25a248a349 100644
--- a/chalk-ir/src/visit/boring_impls.rs
+++ b/chalk-ir/src/visit/boring_impls.rs
@@ -5,11 +5,11 @@
 //! The more interesting impls of `Visit` remain in the `visit` module.
 
 use crate::{
-    try_break, AdtId, AssocTypeId, ClausePriority, ClosureId, Constraints, ControlFlow,
-    DebruijnIndex, FloatTy, FnDefId, ForeignDefId, GeneratorId, GenericArg, Goals, ImplId, IntTy,
-    Interner, Mutability, OpaqueTyId, PlaceholderIndex, ProgramClause, ProgramClauses,
-    QuantifiedWhereClauses, QuantifierKind, Safety, Scalar, Substitution, SuperVisit, TraitId,
-    UintTy, UniverseIndex, Visit, Visitor,
+    try_break, AdtId, AssocFnDefId, AssocTypeId, ClausePriority, ClosureId, Constraints,
+    ControlFlow, DebruijnIndex, FloatTy, FnDefId, ForeignDefId, GeneratorId, GenericArg, Goals,
+    ImplId, IntTy, Interner, Mutability, OpaqueTyId, PlaceholderIndex, ProgramClause,
+    ProgramClauses, QuantifiedWhereClauses, QuantifierKind, Safety, Scalar, Substitution,
+    SuperVisit, TraitId, UintTy, UniverseIndex, Visit, Visitor,
 };
 use std::{marker::PhantomData, sync::Arc};
 
@@ -232,6 +232,7 @@ id_visit!(TraitId);
 id_visit!(OpaqueTyId);
 id_visit!(AssocTypeId);
 id_visit!(FnDefId);
+id_visit!(AssocFnDefId);
 id_visit!(ClosureId);
 id_visit!(GeneratorId);
 id_visit!(ForeignDefId);
diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs
index d7a70d36615..3166195ca39 100644
--- a/chalk-ir/src/zip.rs
+++ b/chalk-ir/src/zip.rs
@@ -333,6 +333,32 @@ eq_zip!(I => ClausePriority);
 eq_zip!(I => Mutability);
 eq_zip!(I => Scalar);
 
+macro_rules! slice_zip {
+    ($I:ident => $t:ty) => {
+        impl<$I: Interner> Zip<$I> for $t {
+            fn zip_with<'i, Z: Zipper<'i, $I>>(
+                zipper: &mut Z,
+                variance: Variance,
+                a: &Self,
+                b: &Self,
+            ) -> Fallible<()>
+            where
+                $I: 'i,
+            {
+                let interner = zipper.interner();
+                Zip::zip_with(zipper, variance, a.as_slice(interner), b.as_slice(interner))?;
+                Ok(())
+            }
+        }
+    };
+}
+
+slice_zip!(I => Goals<I>);
+slice_zip!(I => ProgramClauses<I>);
+slice_zip!(I => Constraints<I>);
+slice_zip!(I => QuantifiedWhereClauses<I>);
+slice_zip!(I => Substitution<I>);
+
 impl<T: HasInterner<Interner = I> + Zip<I>, I: Interner> Zip<I> for InEnvironment<T> {
     fn zip_with<'i, Z: Zipper<'i, I>>(
         zipper: &mut Z,
@@ -371,70 +397,6 @@ impl<I: Interner> Zip<I> for Environment<I> {
     }
 }
 
-impl<I: Interner> Zip<I> for Goals<I> {
-    fn zip_with<'i, Z: Zipper<'i, I>>(
-        zipper: &mut Z,
-        variance: Variance,
-        a: &Self,
-        b: &Self,
-    ) -> Fallible<()>
-    where
-        I: 'i,
-    {
-        let interner = zipper.interner();
-        Zip::zip_with(zipper, variance, a.as_slice(interner), b.as_slice(interner))?;
-        Ok(())
-    }
-}
-
-impl<I: Interner> Zip<I> for ProgramClauses<I> {
-    fn zip_with<'i, Z: Zipper<'i, I>>(
-        zipper: &mut Z,
-        variance: Variance,
-        a: &Self,
-        b: &Self,
-    ) -> Fallible<()>
-    where
-        I: 'i,
-    {
-        let interner = zipper.interner();
-        Zip::zip_with(zipper, variance, a.as_slice(interner), b.as_slice(interner))?;
-        Ok(())
-    }
-}
-
-impl<I: Interner> Zip<I> for Constraints<I> {
-    fn zip_with<'i, Z: Zipper<'i, I>>(
-        zipper: &mut Z,
-        variance: Variance,
-        a: &Self,
-        b: &Self,
-    ) -> Fallible<()>
-    where
-        I: 'i,
-    {
-        let interner = zipper.interner();
-        Zip::zip_with(zipper, variance, a.as_slice(interner), b.as_slice(interner))?;
-        Ok(())
-    }
-}
-
-impl<I: Interner> Zip<I> for QuantifiedWhereClauses<I> {
-    fn zip_with<'i, Z: Zipper<'i, I>>(
-        zipper: &mut Z,
-        variance: Variance,
-        a: &Self,
-        b: &Self,
-    ) -> Fallible<()>
-    where
-        I: 'i,
-    {
-        let interner = zipper.interner();
-        Zip::zip_with(zipper, variance, a.as_slice(interner), b.as_slice(interner))?;
-        Ok(())
-    }
-}
-
 // Annoyingly, Goal cannot use `enum_zip` because some variants have
 // two parameters, and I'm too lazy to make the macro account for the
 // relevant name mangling.
diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs
index 0f0e9c54663..50dfc1d6521 100644
--- a/chalk-parse/src/ast.rs
+++ b/chalk-parse/src/ast.rs
@@ -143,6 +143,7 @@ pub struct TraitDefn {
     pub assoc_ty_defns: Vec<AssocTyDefn>,
     pub flags: TraitFlags,
     pub well_known: Option<WellKnownTrait>,
+    pub fn_defs: Vec<FnDefn>,
 }
 
 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
@@ -260,12 +261,26 @@ impl fmt::Display for Kind {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub enum ImplItem {
+    Assoc(AssocTyValue),
+    FnDefn(FnDefn),
+}
+
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub enum TraitItem {
+    Assoc(AssocTyDefn),
+    FnDefn(FnDefn),
+}
+
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub struct Impl {
+    pub id: Option<Identifier>,
     pub variable_kinds: Vec<VariableKind>,
     pub trait_ref: TraitRef,
     pub polarity: Polarity,
     pub where_clauses: Vec<QuantifiedWhereClause>,
+    pub fn_defs: Vec<FnDefn>,
     pub assoc_ty_values: Vec<AssocTyValue>,
     pub impl_type: ImplType,
 }
@@ -297,8 +312,11 @@ pub enum Ty {
         name: Identifier,
         args: Vec<GenericArg>,
     },
+    ImplFn {
+        func: ImplFnRef,
+    },
     Projection {
-        proj: ProjectionTy,
+        proj: Projection,
     },
     ForAll {
         lifetime_names: Vec<Identifier>,
@@ -393,12 +411,19 @@ pub enum Lifetime {
 }
 
 #[derive(Clone, PartialEq, Eq, Debug)]
-pub struct ProjectionTy {
+pub struct Projection {
     pub trait_ref: TraitRef,
     pub name: Identifier,
     pub args: Vec<GenericArg>,
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct ImplFnRef {
+    pub impl_name: Identifier,
+    pub fn_name: Identifier,
+    pub args: Vec<GenericArg>,
+}
+
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub struct TraitRef {
     pub trait_name: Identifier,
@@ -439,7 +464,7 @@ impl fmt::Display for Identifier {
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub enum WhereClause {
     Implemented { trait_ref: TraitRef },
-    ProjectionEq { projection: ProjectionTy, ty: Ty },
+    ProjectionEq { projection: Projection, ty: Ty },
     LifetimeOutlives { a: Lifetime, b: Lifetime },
     TypeOutlives { ty: Ty, lifetime: Lifetime },
 }
@@ -447,7 +472,8 @@ pub enum WhereClause {
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub enum DomainGoal {
     Holds { where_clause: WhereClause },
-    Normalize { projection: ProjectionTy, ty: Ty },
+    Normalize { projection: Projection, ty: Ty },
+    NormalizeFn { projection: Projection, ty: Ty },
     TraitRefWellFormed { trait_ref: TraitRef },
     TyWellFormed { ty: Ty },
     TyFromEnv { ty: Ty },
diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop
index 8f20258560e..5f180e55ec2 100644
--- a/chalk-parse/src/parser.lalrpop
+++ b/chalk-parse/src/parser.lalrpop
@@ -251,24 +251,40 @@ ClosureArgs: Vec<Ty> = {
     "," <args:FnArgs> => args.to_tys(),
 }
 
+TraitItem: TraitItem = {
+    <assoc:AssocTyDefn> => TraitItem::Assoc(assoc),
+    <fndef:FnDefn> => TraitItem::FnDefn(fndef),
+};
+
 TraitDefn: TraitDefn = {
     <auto:AutoKeyword?> <marker:MarkerKeyword?> <upstream:UpstreamKeyword?> <fundamental:FundamentalKeyword?> <non_enumerable:NonEnumerableKeyword?> <coinductive:CoinductiveKeyword?> <object_safe:ObjectSafeKeyword?> <well_known:WellKnownTrait?> "trait" <n:Id><p:Angle<VariableKind>>
-        <w:QuantifiedWhereClauses> "{" <a:AssocTyDefn*> "}" => TraitDefn
-    {
-        name: n,
-        variable_kinds: p,
-        where_clauses: w,
-        assoc_ty_defns: a,
-        well_known,
-        flags: TraitFlags {
-            auto: auto.is_some(),
-            marker: marker.is_some(),
-            upstream: upstream.is_some(),
-            fundamental: fundamental.is_some(),
-            non_enumerable: non_enumerable.is_some(),
-            coinductive: coinductive.is_some(),
-            object_safe: object_safe.is_some(),
-        },
+        <w:QuantifiedWhereClauses> "{" <t:TraitItem*> "}" => {
+        let mut assoc = vec![];
+        let mut fn_defs = vec![];
+        for item in t {
+            match item {
+                TraitItem::Assoc(v) => assoc.push(v),
+                TraitItem::FnDefn(v) => fn_defs.push(v),
+            }
+        }
+
+        TraitDefn {
+            name: n,
+            variable_kinds: p,
+            where_clauses: w,
+            assoc_ty_defns: assoc,
+            fn_defs,
+            well_known,
+            flags: TraitFlags {
+                auto: auto.is_some(),
+                marker: marker.is_some(),
+                upstream: upstream.is_some(),
+                fundamental: fundamental.is_some(),
+                non_enumerable: non_enumerable.is_some(),
+                coinductive: coinductive.is_some(),
+                object_safe: object_safe.is_some(),
+            },
+        }
     }
 };
 
@@ -338,13 +354,30 @@ QuantifiedInlineBound: QuantifiedInlineBound = {
     },
 };
 
+ImplItem: ImplItem = {
+    <assoc:AssocTyValue> => ImplItem::Assoc(assoc),
+    <fndef:FnDefn> => ImplItem::FnDefn(fndef),
+};
+
+
 Impl: Impl = {
-    <external:UpstreamKeyword?> "impl" <p:Angle<VariableKind>> <mark:"!"?> <t:Id> <a:Angle<GenericArg>> "for" <s:Ty>
-        <w:QuantifiedWhereClauses> "{" <assoc:AssocTyValue*> "}" =>
+    <external:UpstreamKeyword?> "impl" <id:ImplId?> <p:Angle<VariableKind>>
+        <mark:"!"?> <t:Id> <a:Angle<GenericArg>> "for" <s:Ty>
+        <w:QuantifiedWhereClauses> "{" <items:ImplItem*> "}" =>
     {
         let mut args = vec![GenericArg::Ty(s)];
         args.extend(a);
+        let mut assoc = vec![];
+        let mut fn_defs = vec![];
+        for item in items {
+            match item {
+                ImplItem::Assoc(v) => assoc.push(v),
+                ImplItem::FnDefn(v) => fn_defs.push(v),
+            }
+        }
+
         Impl {
+            id,
             variable_kinds: p,
             polarity: Polarity::from_bool(mark.is_none()),
             trait_ref: TraitRef {
@@ -353,6 +386,7 @@ Impl: Impl = {
             },
             where_clauses: w,
             assoc_ty_values: assoc,
+            fn_defs,
             impl_type: external.map(|_| ImplType::External).unwrap_or(ImplType::Local),
         }
     },
@@ -425,7 +459,8 @@ TyWithoutId: Ty = {
         lifetime: l,
     },
     <n:Id> "<" <a:Comma<GenericArg>> ">" => Ty::Apply { name: n, args: a },
-    <p:ProjectionTy> => Ty::Projection { proj: p },
+    <p:Projection> => Ty::Projection { proj: p },
+    <f:ImplFnRef> => Ty::ImplFn { func: f },
     "(" <t:TupleOrParensInner> ")" => t,
     "*" <m: RawMutability> <t:Ty> => Ty::Raw{ mutability: m, ty: Box::new(t) },
     "&" <l: Lifetime> "mut" <t:Ty> => Ty::Ref{ mutability: Mutability::Mut, lifetime: l, ty: Box::new(t) },
@@ -463,7 +498,7 @@ FloatTy: FloatTy = {
 ScalarType: ScalarType = {
     <i:IntTy> => ScalarType::Int(i),
     <u:UintTy> => ScalarType::Uint(u),
-    <f:FloatTy> => ScalarType::Float(f), 
+    <f:FloatTy> => ScalarType::Float(f),
     "bool" => ScalarType::Bool,
     "char" => ScalarType::Char,
 };
@@ -507,8 +542,8 @@ GenericArg: GenericArg = {
     ConstWithoutId => GenericArg::Const(<>),
 };
 
-ProjectionTy: ProjectionTy = {
-    "<" <t:TraitRef<"as">> ">" "::" <n:Id> <a:Angle<GenericArg>> => ProjectionTy {
+Projection: Projection = {
+    "<" <t:TraitRef<"as">> ">" "::" <n:Id> <a:Angle<GenericArg>> => Projection {
         trait_ref: t, name: n, args: a
     },
 };
@@ -572,7 +607,7 @@ WhereClause: WhereClause = {
         let mut args = vec![GenericArg::Ty(s)];
         if let Some(a) = a { args.extend(a); }
         let trait_ref = TraitRef { trait_name: t, args: args };
-        let projection = ProjectionTy { trait_ref, name, args: a2 };
+        let projection = Projection { trait_ref, name, args: a2 };
         WhereClause::ProjectionEq { projection, ty }
     },
 
@@ -616,7 +651,10 @@ DomainGoal: DomainGoal = {
     "FromEnv" "(" <t:TraitRef<":">> ")" => DomainGoal::TraitRefFromEnv { trait_ref: t },
 
     // `<T as Foo>::U -> Bar` -- a normalization
-    "Normalize" "(" <s:ProjectionTy> "->" <t:Ty> ")" => DomainGoal::Normalize { projection: s, ty: t },
+    "Normalize" "(" <s:Projection> "->" <t:Ty> ")" => DomainGoal::Normalize { projection: s, ty: t },
+
+    // `<T as Foo>::some_func -> @SomeImpl::some_func` -- a normalization
+    "NormalizeFn" "(" <s:Projection> "->" <t:Ty> ")" => DomainGoal::NormalizeFn { projection: s, ty: t },
 
     "IsLocal" "(" <ty:Ty> ")" => DomainGoal::IsLocal { ty },
     "IsUpstream" "(" <ty:Ty> ")" => DomainGoal::IsUpstream { ty },
@@ -640,6 +678,15 @@ LeafGoal: LeafGoal = {
     "Subtype" "(" <a:Ty> "," <b:Ty> ")" => LeafGoal::SubtypeGenericArgs { a, b },
 };
 
+// @ImplName::f<A, B>
+ImplFnRef: ImplFnRef = {
+    <imp:ImplId> "::" <f:Id> <a:Angle<GenericArg>> => ImplFnRef {
+        impl_name: imp,
+        fn_name: f,
+        args: a,
+    },
+}
+
 TraitRef<S>: TraitRef = {
     <s:Ty> S <t:Id> <a:Angle<GenericArg>> => {
         let mut args = vec![GenericArg::Ty(s)];
@@ -699,4 +746,11 @@ LifetimeId: Identifier = {
     }
 };
 
+ImplId: Identifier = {
+    <l:@L> "@" <s:r"([A-Za-z]|_)([A-Za-z0-9]|_)*"> <r:@R> => Identifier {
+        str: Atom::from(s),
+        span: Span::new(l, r),
+    }
+};
+
 ConstValue: u32 = <s:r"[0-9]+"> => u32::from_str_radix(s, 10).unwrap();
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
index e347a801737..93404647642 100644
--- a/chalk-solve/src/clauses.rs
+++ b/chalk-solve/src/clauses.rs
@@ -39,7 +39,7 @@ fn constituent_types<I: Interner>(db: &dyn RustIrDatabase<I>, ty: &TyKind<I>) ->
         // And for `PhantomData<T>`, we pass `T`.
         TyKind::Adt(_, substitution)
         | TyKind::Tuple(_, substitution)
-        | TyKind::FnDef(_, substitution) => substitution
+        | TyKind::FnDef(FnDefTy { substitution, .. }) => substitution
             .iter(interner)
             .filter_map(|x| x.ty(interner))
             .cloned()
@@ -457,7 +457,7 @@ pub fn program_clauses_that_could_match<I: Interner>(
                     let _ = db.adt_datum(*adt_id);
                 }
 
-                TyKind::FnDef(fn_def_id, _) => {
+                TyKind::FnDef(FnDefTy { fn_def_id, .. }) => {
                     let _ = db.fn_def_datum(*fn_def_id);
                 }
 
@@ -644,6 +644,26 @@ pub fn program_clauses_that_could_match<I: Interner>(
             }
             AliasTy::Opaque(_) => (),
         },
+        DomainGoal::NormalizeFn(a, _) => {
+            // XXX: mildly alarming cast between ID types from user provided
+            // data. It might panic or do something silly if they give us a
+            // function ID for a non associated function...
+            let associated_fn_datum = db.associated_fn_data(AssocFnDefId(a.fn_def_id));
+            let trait_id = associated_fn_datum.trait_id;
+
+            let (trait_params, _other_params) = db.split_associated_fn_parameters(
+                a.substitution.as_slice(db.interner()),
+                &associated_fn_datum,
+            );
+
+            push_program_clauses_for_associated_fn_values_in_impls_of(
+                builder,
+                environment,
+                trait_id,
+                trait_params,
+                binders,
+            );
+        }
         DomainGoal::Compatible | DomainGoal::Reveal => (),
     };
 
@@ -748,6 +768,37 @@ fn push_program_clauses_for_associated_type_values_in_impls_of<I: Interner>(
     }
 }
 
+/// Generate program clauses from the associated-fn values
+/// found in impls of the given trait. i.e., if `trait_id` = SomeTrait,
+/// then we would generate program clauses from each `fn do_thing()`
+/// found in any impls of `SomeTrait`.
+#[instrument(level = "debug", skip(builder))]
+fn push_program_clauses_for_associated_fn_values_in_impls_of<I: Interner>(
+    builder: &mut ClauseBuilder<'_, I>,
+    environment: &Environment<I>,
+    trait_id: TraitId<I>,
+    trait_parameters: &[GenericArg<I>],
+    binders: &CanonicalVarKinds<I>,
+) {
+    for impl_id in builder
+        .db
+        .impls_for_trait(trait_id, trait_parameters, binders)
+    {
+        let impl_datum = builder.db.impl_datum(impl_id);
+        if !impl_datum.is_positive() {
+            continue;
+        }
+
+        debug!(?impl_id);
+
+        for &afn_id in &impl_datum.associated_fn_value_ids {
+            let afv = builder.db.associated_fn_value(afn_id);
+            debug!(?afn_id, ?afv);
+            afv.to_program_clauses(builder, environment);
+        }
+    }
+}
+
 fn push_alias_implemented_clause<I: Interner>(
     builder: &mut ClauseBuilder<'_, I>,
     trait_ref: TraitRef<I>,
@@ -881,7 +932,7 @@ fn match_ty<I: Interner>(
             .db
             .associated_ty_data(*type_id)
             .to_program_clauses(builder, environment),
-        TyKind::FnDef(fn_def_id, _) => builder
+        TyKind::FnDef(FnDefTy { fn_def_id, .. }) => builder
             .db
             .fn_def_datum(*fn_def_id)
             .to_program_clauses(builder, environment),
diff --git a/chalk-solve/src/clauses/builtin_traits/copy.rs b/chalk-solve/src/clauses/builtin_traits/copy.rs
index 0b8f801430a..6929839de0c 100644
--- a/chalk-solve/src/clauses/builtin_traits/copy.rs
+++ b/chalk-solve/src/clauses/builtin_traits/copy.rs
@@ -45,7 +45,7 @@ pub fn add_copy_program_clauses<I: Interner>(
         TyKind::Array(ty, _) => {
             needs_impl_for_tys(db, builder, trait_ref, iter::once(ty.clone()));
         }
-        TyKind::FnDef(_, _) => {
+        TyKind::FnDef(_) => {
             builder.push_fact(trait_ref);
         }
         TyKind::Closure(closure_id, ref substitution) => {
diff --git a/chalk-solve/src/clauses/builtin_traits/fn_family.rs b/chalk-solve/src/clauses/builtin_traits/fn_family.rs
index 4645b139125..02346da5486 100644
--- a/chalk-solve/src/clauses/builtin_traits/fn_family.rs
+++ b/chalk-solve/src/clauses/builtin_traits/fn_family.rs
@@ -3,8 +3,8 @@ use crate::rust_ir::{ClosureKind, FnDefInputsAndOutputDatum, WellKnownTrait};
 use crate::{Interner, RustIrDatabase, TraitRef};
 use chalk_ir::cast::Cast;
 use chalk_ir::{
-    AliasTy, Binders, Floundered, Normalize, ProjectionTy, Safety, Substitution, TraitId, Ty,
-    TyKind,
+    AliasTy, Binders, Floundered, FnDefTy, Normalize, ProjectionTy, Safety, Substitution, TraitId,
+    Ty, TyKind,
 };
 
 fn push_clauses<I: Interner>(
@@ -91,7 +91,10 @@ pub fn add_fn_trait_program_clauses<I: Interner>(
     let trait_id = db.well_known_trait_id(well_known).unwrap();
 
     match self_ty.kind(interner) {
-        TyKind::FnDef(fn_def_id, substitution) => {
+        TyKind::FnDef(FnDefTy {
+            fn_def_id,
+            substitution,
+        }) => {
             let fn_def_datum = builder.db.fn_def_datum(*fn_def_id);
             if fn_def_datum.sig.safety == Safety::Safe && !fn_def_datum.sig.variadic {
                 let bound = fn_def_datum
diff --git a/chalk-solve/src/clauses/builtin_traits/sized.rs b/chalk-solve/src/clauses/builtin_traits/sized.rs
index 3ed46d42521..2122e180e2c 100644
--- a/chalk-solve/src/clauses/builtin_traits/sized.rs
+++ b/chalk-solve/src/clauses/builtin_traits/sized.rs
@@ -83,7 +83,7 @@ pub fn add_sized_program_clauses<I: Interner>(
         TyKind::Array(_, _)
         | TyKind::Never
         | TyKind::Closure(_, _)
-        | TyKind::FnDef(_, _)
+        | TyKind::FnDef(_)
         | TyKind::Scalar(_)
         | TyKind::Raw(_, _)
         | TyKind::Generator(_, _)
diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs
index 19811ff8b30..fa01fff86e7 100644
--- a/chalk-solve/src/clauses/program_clauses.rs
+++ b/chalk-solve/src/clauses/program_clauses.rs
@@ -134,6 +134,98 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyValue<I> {
     }
 }
 
+impl<I: Interner> ToProgramClauses<I> for AssociatedFnValue<I> {
+    /// Generate program clauses for an associated function implementation on an impl.
+    ///
+    /// For:
+    /// ```notrust
+    /// trait Trait {
+    ///     fn fun(self: &Self);
+    /// }
+    /// ```
+    ///
+    /// With the impl:
+    /// ```notrust
+    /// impl<T> @Impl Trait for Vec<T> where T: Clone {
+    ///     fn fun(self: &Self);
+    /// }
+    /// ```
+    ///
+    /// Generates:
+    /// ```notrust
+    /// forall<T> {
+    ///     NormalizeFn(<Vec<T> as Trait>::fun -> @Impl::fun) :-
+    ///         Implemented(T: Clone).
+    /// }
+    /// ```
+    fn to_program_clauses(
+        &self,
+        builder: &mut ClauseBuilder<'_, I>,
+        _environment: &Environment<I>,
+    ) {
+        let impl_datum = builder.db.impl_datum(self.impl_id);
+        let associated_fn = builder.db.associated_fn_data(self.fn_id);
+
+        builder.push_binders(self.value.clone(), |builder, assoc_fn_id| {
+            let all_parameters = builder.placeholders_in_scope().to_vec();
+            // FIXME: the example for this needs to be changed to show rule (2)
+
+            // Get the projection for this associated function:
+            //
+            // * `impl_params`: `[!T]`
+            // * `projection`: `@Impl::fun`
+            let (impl_params, projection) = builder
+                .db
+                .impl_parameters_and_projection_from_associated_fn_value(&all_parameters, self);
+
+            // Assemble the full list of conditions for projection to be valid.
+            // This comes in two parts, marked as (1) and (2) in doc above:
+            //
+            // 1. require that the where clauses from the impl apply
+            let interner = builder.db.interner();
+            let impl_where_clauses = impl_datum
+                .binders
+                .map_ref(|b| &b.where_clauses)
+                .into_iter()
+                .map(|wc| wc.cloned().substitute(interner, impl_params));
+
+            let impl_where_clauses = impl_where_clauses.collect::<Vec<_>>();
+            tracing::debug!(impl_where_clauses = ?impl_where_clauses);
+
+            // 2. any where-clauses from the `fn` declaration in the trait: the
+            //    parameters must be substituted with those of the impl
+            let assoc_fn_where_clauses = associated_fn
+                .binders
+                .map_ref(|b| &b.where_clauses)
+                .into_iter()
+                .map(|wc| wc.cloned().substitute(interner, &projection.substitution));
+
+            let substitution = builder.substitution_in_scope();
+
+            // Create the final program clause:
+            //
+            // ```notrust
+            // -- Rule NormalizeFn-From-Impl
+            // forall<T> {
+            //     NormalizeFn(<Vec<T> as Trait>::fun -> @Impl::fun<T>) :-
+            //         Implemented(T: Clone),  // (1)
+            // }
+            // ```
+            builder.push_clause(
+                DomainGoal::NormalizeFn(
+                    projection.clone(),
+                    TyKind::FnDef(FnDefTy {
+                        fn_def_id: assoc_fn_id,
+                        substitution,
+                    })
+                    .intern(interner),
+                ),
+                impl_where_clauses.into_iter().chain(assoc_fn_where_clauses),
+            );
+        });
+    }
+}
+
 impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
     /// Given `opaque type T<U>: A + B = HiddenTy where U: C;`, we generate:
     ///
@@ -470,7 +562,11 @@ impl<I: Interner> ToProgramClauses<I> for FnDefDatum<I> {
         let binders = self.binders.map_ref(|b| &b.where_clauses).cloned();
 
         builder.push_binders(binders, |builder, where_clauses| {
-            let ty = TyKind::FnDef(self.id, builder.substitution_in_scope()).intern(interner);
+            let ty = TyKind::FnDef(FnDefTy {
+                fn_def_id: self.id,
+                substitution: builder.substitution_in_scope(),
+            })
+            .intern(interner);
 
             well_formed_program_clauses(builder, ty.clone(), where_clauses.iter());
 
@@ -801,7 +897,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
         builder.push_binders(
             binders,
             |builder,
-             AssociatedTyDatumBound {
+             AssociatedItemDatumBound {
                  where_clauses,
                  bounds,
              }| {
diff --git a/chalk-solve/src/display/stub.rs b/chalk-solve/src/display/stub.rs
index 504b9c9e44e..193ebd42eb4 100644
--- a/chalk-solve/src/display/stub.rs
+++ b/chalk-solve/src/display/stub.rs
@@ -5,7 +5,7 @@ use std::sync::Arc;
 use crate::rust_ir::{GeneratorDatum, GeneratorWitnessDatum};
 use crate::{
     rust_ir::{
-        AdtDatumBound, AdtKind, AdtVariantDatum, AssociatedTyDatumBound, FnDefDatumBound,
+        AdtDatumBound, AdtKind, AdtVariantDatum, AssociatedItemDatumBound, FnDefDatumBound,
         OpaqueTyDatumBound, TraitDatumBound,
     },
     RustIrDatabase,
@@ -48,7 +48,7 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
         let mut v = (*self.db.associated_ty_data(ty)).clone();
         v.binders = Binders::new(
             v.binders.binders.clone(),
-            AssociatedTyDatumBound {
+            AssociatedItemDatumBound {
                 where_clauses: Vec::new(),
                 bounds: Vec::new(),
             },
@@ -56,6 +56,14 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
         Arc::new(v)
     }
 
+    fn associated_fn_data(
+        &self,
+        f: chalk_ir::AssocFnDefId<I>,
+    ) -> std::sync::Arc<crate::rust_ir::AssociatedFnDatum<I>> {
+        // there are no binders in here to stub out, those would be dealt with with FnDef
+        self.db.associated_fn_data(f)
+    }
+
     fn trait_datum(
         &self,
         trait_id: chalk_ir::TraitId<I>,
@@ -119,6 +127,13 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
         unreachable!("associated type values should never be stubbed")
     }
 
+    fn associated_fn_value(
+        &self,
+        _id: crate::rust_ir::AssociatedFnValueId<I>,
+    ) -> std::sync::Arc<crate::rust_ir::AssociatedFnValue<I>> {
+        unreachable!("associated function values should never be stubbed")
+    }
+
     fn opaque_ty_data(
         &self,
         id: chalk_ir::OpaqueTyId<I>,
diff --git a/chalk-solve/src/display/utils.rs b/chalk-solve/src/display/utils.rs
index 31a8a9357de..30660561679 100644
--- a/chalk-solve/src/display/utils.rs
+++ b/chalk-solve/src/display/utils.rs
@@ -24,7 +24,7 @@ macro_rules! write_joined_non_empty_list {
     }};
 }
 
-/// Processes a name given by an [`Interner`][chalk_ir::Interner] debug
+/// Processes a name given by an [`Interner`][chalk_ir::interner::Interner] debug
 /// method into something usable by the `display` module.
 ///
 /// This is specifically useful when implementing
diff --git a/chalk-solve/src/infer/invert.rs b/chalk-solve/src/infer/invert.rs
index 053cc18c1ce..d487bc2580c 100644
--- a/chalk-solve/src/infer/invert.rs
+++ b/chalk-solve/src/infer/invert.rs
@@ -21,7 +21,7 @@ impl<I: Interner> InferenceTable<I> {
     /// negation-as-failure paper [1], where negative goals are only
     /// permitted if they contain no free (existential) variables.
     ///
-    /// [1] https://www.doc.ic.ac.uk/~klc/NegAsFailure.pdf
+    /// [1]: https://www.doc.ic.ac.uk/~klc/NegAsFailure.pdf
     ///
     /// Restricting free existential variables is done because the
     /// semantics of such queries is not what you expect: it basically
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
index 2fd745d1798..a462cf51327 100644
--- a/chalk-solve/src/infer/unify.rs
+++ b/chalk-solve/src/infer/unify.rs
@@ -263,7 +263,16 @@ impl<'t, I: Interner> Unifier<'t, I> {
                 )
             }
             (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => Zip::zip_with(self, variance, ty_a, ty_b),
-            (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => {
+            (
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_a,
+                    substitution: substitution_a,
+                }),
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: id_b,
+                    substitution: substitution_b,
+                }),
+            ) => {
                 if id_a != id_b {
                     return Err(NoSolution);
                 }
@@ -536,7 +545,10 @@ impl<'t, I: Interner> Unifier<'t, I> {
             TyKind::Slice(ty) => {
                 TyKind::Slice(self.generalize_ty(ty, universe_index, variance)).intern(interner)
             }
-            TyKind::FnDef(id, substitution) => {
+            TyKind::FnDef(FnDefTy {
+                fn_def_id: id,
+                substitution,
+            }) => {
                 let variances = if matches!(variance, Variance::Invariant) {
                     None
                 } else {
@@ -548,10 +560,14 @@ impl<'t, I: Interner> Unifier<'t, I> {
                         .map(|v| v.as_slice(interner)[i])
                         .unwrap_or(Variance::Invariant)
                 };
-                TyKind::FnDef(
-                    *id,
-                    self.generalize_substitution(substitution, universe_index, get_variance),
-                )
+                TyKind::FnDef(FnDefTy {
+                    fn_def_id: *id,
+                    substitution: self.generalize_substitution(
+                        substitution,
+                        universe_index,
+                        get_variance,
+                    ),
+                })
                 .intern(interner)
             }
             TyKind::Ref(mutability, lifetime, ty) => {
diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs
index 6805dd9f6dd..29153adb9b8 100644
--- a/chalk-solve/src/lib.rs
+++ b/chalk-solve/src/lib.rs
@@ -49,6 +49,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {
     /// Returns the datum for the associated type with the given id.
     fn associated_ty_data(&self, ty: AssocTypeId<I>) -> Arc<AssociatedTyDatum<I>>;
 
+    /// Returns the datum for the associated fn with the given id.
+    fn associated_fn_data(&self, f: AssocFnDefId<I>) -> Arc<AssociatedFnDatum<I>>;
+
     /// Returns the datum for the definition with the given id.
     fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>>;
 
@@ -73,10 +76,13 @@ pub trait RustIrDatabase<I: Interner>: Debug {
     /// Returns the datum for the impl with the given id.
     fn impl_datum(&self, impl_id: ImplId<I>) -> Arc<ImplDatum<I>>;
 
-    /// Returns the `AssociatedTyValue` with the given id.
+    /// Returns the [`AssociatedTyValue`] with the given id.
     fn associated_ty_value(&self, id: AssociatedTyValueId<I>) -> Arc<AssociatedTyValue<I>>;
 
-    /// Returns the `OpaqueTyDatum` with the given id.
+    /// Returns the [`AssociatedFnValue`] with the given id.
+    fn associated_fn_value(&self, id: AssociatedFnValueId<I>) -> Arc<AssociatedFnValue<I>>;
+
+    /// Returns the [`OpaqueTyDatum`] with the given id.
     fn opaque_ty_data(&self, id: OpaqueTyId<I>) -> Arc<OpaqueTyDatum<I>>;
 
     /// Returns the "hidden type" corresponding with the opaque type.
diff --git a/chalk-solve/src/logging_db.rs b/chalk-solve/src/logging_db.rs
index 4e7fa0c4959..d03e4acc461 100644
--- a/chalk-solve/src/logging_db.rs
+++ b/chalk-solve/src/logging_db.rs
@@ -128,6 +128,15 @@ where
         ty_datum
     }
 
+    fn associated_fn_data(
+        &self,
+        f: chalk_ir::AssocFnDefId<I>,
+    ) -> Arc<crate::rust_ir::AssociatedFnDatum<I>> {
+        let datum = self.ws.db().associated_fn_data(f);
+        self.record(datum.trait_id);
+        datum
+    }
+
     fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>> {
         self.record(trait_id);
         self.ws.db().trait_datum(trait_id)
@@ -175,6 +184,15 @@ where
         value
     }
 
+    fn associated_fn_value(
+        &self,
+        id: crate::rust_ir::AssociatedFnValueId<I>,
+    ) -> Arc<crate::rust_ir::AssociatedFnValue<I>> {
+        let value = self.ws.db().associated_fn_value(id);
+        self.record(value.impl_id);
+        value
+    }
+
     fn opaque_ty_data(&self, id: OpaqueTyId<I>) -> Arc<OpaqueTyDatum<I>> {
         self.record(id);
         self.ws.db().opaque_ty_data(id)
@@ -395,6 +413,13 @@ where
         self.db.associated_ty_data(ty)
     }
 
+    fn associated_fn_data(
+        &self,
+        f: chalk_ir::AssocFnDefId<I>,
+    ) -> Arc<crate::rust_ir::AssociatedFnDatum<I>> {
+        self.db.associated_fn_data(f)
+    }
+
     fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>> {
         self.db.trait_datum(trait_id)
     }
@@ -430,6 +455,13 @@ where
         self.db.associated_ty_value(id)
     }
 
+    fn associated_fn_value(
+        &self,
+        id: crate::rust_ir::AssociatedFnValueId<I>,
+    ) -> Arc<crate::rust_ir::AssociatedFnValue<I>> {
+        self.db.associated_fn_value(id)
+    }
+
     fn opaque_ty_data(&self, id: OpaqueTyId<I>) -> Arc<OpaqueTyDatum<I>> {
         self.db.opaque_ty_data(id)
     }
diff --git a/chalk-solve/src/logging_db/id_collector.rs b/chalk-solve/src/logging_db/id_collector.rs
index 2a627494ad8..af7e12886fa 100644
--- a/chalk-solve/src/logging_db/id_collector.rs
+++ b/chalk-solve/src/logging_db/id_collector.rs
@@ -4,7 +4,7 @@ use chalk_ir::{
     interner::Interner,
     visit::{ControlFlow, Visitor},
     visit::{SuperVisit, Visit},
-    AliasTy, DebruijnIndex, TyKind, WhereClause,
+    AliasTy, DebruijnIndex, FnDefTy, TyKind, WhereClause,
 };
 use std::collections::BTreeSet;
 
@@ -134,7 +134,7 @@ where
     ) -> ControlFlow<()> {
         match ty.kind(self.db.interner()) {
             TyKind::Adt(adt, _) => self.record(*adt),
-            TyKind::FnDef(fn_def, _) => self.record(*fn_def),
+            TyKind::FnDef(FnDefTy { fn_def_id, .. }) => self.record(*fn_def_id),
             TyKind::OpaqueType(opaque, _) => self.record(*opaque),
             TyKind::Alias(alias) => self.visit_alias(&alias),
             TyKind::BoundVar(..) => (),
diff --git a/chalk-solve/src/rust_ir.rs b/chalk-solve/src/rust_ir.rs
index cc609f5b521..ce4dac76a4b 100644
--- a/chalk-solve/src/rust_ir.rs
+++ b/chalk-solve/src/rust_ir.rs
@@ -6,12 +6,13 @@ use chalk_derive::{Fold, HasInterner, Visit};
 use chalk_ir::cast::Cast;
 use chalk_ir::fold::shift::Shift;
 use chalk_ir::interner::Interner;
+
 use chalk_ir::{
     try_break,
     visit::{ControlFlow, Visit},
-    AdtId, AliasEq, AliasTy, AssocTypeId, Binders, DebruijnIndex, FnDefId, GenericArg, ImplId,
-    OpaqueTyId, ProjectionTy, QuantifiedWhereClause, Substitution, ToGenericArg, TraitId, TraitRef,
-    Ty, TyKind, VariableKind, WhereClause, WithKind,
+    AdtId, AliasEq, AliasTy, AssocFnDefId, AssocTypeId, Binders, DebruijnIndex, FnDefId,
+    GenericArg, ImplId, OpaqueTyId, ProjectionTy, QuantifiedWhereClause, Substitution,
+    ToGenericArg, TraitId, TraitRef, Ty, TyKind, VariableKind, WhereClause, WithKind,
 };
 use std::iter;
 
@@ -22,15 +23,38 @@ pub struct AssociatedTyValueId<I: Interner>(pub I::DefId);
 chalk_ir::id_visit!(AssociatedTyValueId);
 chalk_ir::id_fold!(AssociatedTyValueId);
 
+/// Identifier for an implementation of a function
+#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct AssociatedFnValueId<I: Interner>(pub FnDefId<I>);
+
+chalk_ir::id_visit!(AssociatedFnValueId);
+chalk_ir::id_fold!(AssociatedFnValueId);
+
+impl<I: Interner> AssociatedFnValueId<I> {
+    /// Gets the function definition ID corresponding to this associated
+    /// function value.
+    pub fn as_fn(&self) -> FnDefId<I> {
+        self.0
+    }
+}
+
+/// Data about a trait implementation.
 #[derive(Clone, Debug, PartialEq, Eq, Hash, Visit)]
 pub struct ImplDatum<I: Interner> {
+    /// Whether this is an `impl Trait` or `impl !Trait`
     pub polarity: Polarity,
+    /// Bindings of variables from the where clauses in the trait.
     pub binders: Binders<ImplDatumBound<I>>,
+    /// Whether this impl is local to this crate or from an external crate
     pub impl_type: ImplType,
+    /// IDs for associated types `type T = SomeTy`
     pub associated_ty_value_ids: Vec<AssociatedTyValueId<I>>,
+    /// IDs of the implemented functions
+    pub associated_fn_value_ids: Vec<AssociatedFnValueId<I>>,
 }
 
 impl<I: Interner> ImplDatum<I> {
+    /// True if this is an `impl Trait`, false if `impl !Trait`
     pub fn is_positive(&self) -> bool {
         self.polarity.is_positive()
     }
@@ -39,6 +63,7 @@ impl<I: Interner> ImplDatum<I> {
         self.binders.skip_binders().trait_ref.trait_id
     }
 
+    /// Gets the [`AdtId`] for the `Self` type of this impl.
     pub fn self_type_adt_id(&self, interner: &I) -> Option<AdtId<I>> {
         match self
             .binders
@@ -59,6 +84,7 @@ pub struct ImplDatumBound<I: Interner> {
     pub where_clauses: Vec<QuantifiedWhereClause<I>>,
 }
 
+/// Whether this impl is local to this crate or from an external crate
 #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
 pub enum ImplType {
     Local,
@@ -242,6 +268,9 @@ pub struct TraitDatum<I: Interner> {
     /// If this is a well-known trait, which one? If `None`, this is a regular,
     /// user-defined trait.
     pub well_known: Option<WellKnownTrait>,
+
+    /// Types of the functions defined in this trait
+    pub fn_defs: Vec<AssocFnDefId<I>>,
 }
 
 /// A list of the traits that are "well known" to chalk, which means that
@@ -487,7 +516,7 @@ pub struct AssociatedTyDatum<I: Interner> {
     /// from `Bar` come first (corresponding to the de bruijn concept
     /// that "inner" binders are lower indices, although within a
     /// given binder we do not have an ordering).
-    pub binders: Binders<AssociatedTyDatumBound<I>>,
+    pub binders: Binders<AssociatedItemDatumBound<I>>,
 }
 
 // Manual implementation to avoid I::Identifier type.
@@ -506,11 +535,12 @@ impl<I: Interner> Visit<I> for AssociatedTyDatum<I> {
     }
 }
 
-/// Encodes the parts of `AssociatedTyDatum` where the parameters
-/// `P0..Pm` are in scope (`bounds` and `where_clauses`).
+/// Encodes the parts of [`AssociatedTyDatum`] and [`AssociatedFnDatum`]
+/// where the parameters `P0..Pm` are in scope (`bounds` and
+/// `where_clauses`).
 #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]
-pub struct AssociatedTyDatumBound<I: Interner> {
-    /// Bounds on the associated type itself.
+pub struct AssociatedItemDatumBound<I: Interner> {
+    /// Bounds on the associated item itself.
     ///
     /// These must be proven by the implementer, for all possible parameters that
     /// would result in a well-formed projection.
@@ -596,14 +626,13 @@ pub struct AssociatedTyValue<I: Interner> {
     /// ```
     pub associated_ty_id: AssocTypeId<I>,
 
-    /// Additional binders declared on the associated type itself,
-    /// beyond those from the impl. This would be empty for normal
-    /// associated types, but non-empty for generic associated types.
+    /// All the binders declared on the impl and the associated type.
     ///
     /// ```ignore
     /// impl<T> Iterable for Vec<T> {
+    ///   // ^ refers to these generics here
     ///     type Iter<'a> = vec::Iter<'a, T>;
-    ///           // ^^^^ refers to these generics here
+    ///           // ^^^^ and here
     /// }
     /// ```
     pub value: Binders<AssociatedTyValueBound<I>>,
@@ -615,6 +644,45 @@ pub struct AssociatedTyValueBound<I: Interner> {
     pub ty: Ty<I>,
 }
 
+/// Data for an associated function on a trait
+#[derive(Clone, Debug, PartialEq, Eq, Hash, HasInterner)]
+pub struct AssociatedFnDatum<I: Interner> {
+    /// Trait the associated function is implemented on
+    pub trait_id: TraitId<I>,
+
+    /// Name of the associated function
+    pub name: I::Identifier,
+
+    /// ID of the function. You can use the [`FnDefId`] from [`AssocFnDefId::as_fn`] to look up
+    /// signature, binders, etc.
+    pub fn_id: AssocFnDefId<I>,
+
+    /// Binders introduced on the trait.
+    pub binders: Binders<AssociatedItemDatumBound<I>>,
+}
+
+/// An implementation of an associated fn.
+#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit)]
+pub struct AssociatedFnValue<I: Interner> {
+    /// Impl where this implementation is defined
+    pub impl_id: ImplId<I>,
+
+    /// ID of the function being defined (on the trait)
+    pub fn_id: AssocFnDefId<I>,
+    // FIXME: store if it's a default fn
+    //
+    /// All the binders from both the impl and the function.
+    ///
+    /// ```ignore
+    /// impl<T> TraitWithGenericFn for Vec<T> {
+    ///   // ^ this generic
+    ///     fn a<Y, 'a>(self: &Self, s: &'a [Y]);
+    ///       // ^^^^^  ^^^^^^^^^^^ these generics
+    /// }
+    /// ```
+    pub value: Binders<FnDefId<I>>,
+}
+
 /// Represents the bounds for an `impl Trait` type.
 ///
 /// ```ignore
@@ -714,7 +782,9 @@ pub struct GeneratorWitnessExistential<I: Interner> {
 
 #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
 pub enum Polarity {
+    /// `impl Trait for ..`
     Positive,
+    /// `impl !Trait for ..`
     Negative,
 }
 
diff --git a/chalk-solve/src/split.rs b/chalk-solve/src/split.rs
index 2aa6413838b..6d139e76a28 100644
--- a/chalk-solve/src/split.rs
+++ b/chalk-solve/src/split.rs
@@ -5,8 +5,8 @@ use chalk_ir::*;
 use std::sync::Arc;
 use tracing::{debug, instrument};
 
-/// Methods for splitting up the projections for associated types from
-/// the surrounding context.
+/// Methods for splitting up the projections for associated types and
+/// functions from the surrounding context.
 pub trait Split<I: Interner>: RustIrDatabase<I> {
     /// Given a projection of an associated type, split the type
     /// parameters into those that come from the *trait* and those
@@ -182,7 +182,7 @@ pub trait Split<I: Interner>: RustIrDatabase<I> {
     /// Returns the tuple of:
     ///
     /// * the parameters for the impl (`[Y]`, in our example)
-    /// * the parameters for the associated type value (`['a]`, in our example)
+    /// * the parameters for the associated type value (`['x]`, in our example)
     fn split_associated_ty_parameters<'p, P>(
         &self,
         parameters: &'p [P],
@@ -194,6 +194,146 @@ pub trait Split<I: Interner>: RustIrDatabase<I> {
         let (other_params, trait_params) = parameters.split_at(split_point);
         (trait_params, other_params)
     }
+
+    /// Given the full set of parameters (or binders) for an
+    /// associated function *value* (which appears in an impl), splits
+    /// them into the substitutions for the *impl* and those for the
+    /// *associated function*.
+    ///
+    /// # Example
+    ///
+    /// ```ignore (example)
+    /// impl<T> Iterable for Vec<T> {
+    ///     fn f<'a, U>(&self, r: &'a [U]);
+    /// }
+    /// ```
+    ///
+    /// in this example, the full set of parameters would be `['x, S,
+    /// Y]`, where `'x` is the value for `'a`, `S` is the value for
+    /// `self`, and `Y` is the value for `T`.
+    ///
+    /// # Returns
+    ///
+    /// Returns the pair of:
+    ///
+    /// * the parameters for the impl (`[Y]`, in our example)
+    /// * the parameters for the associated type value (`['a, S]`, in our example)
+    fn split_associated_fn_value_parameters<'p, P>(
+        &self,
+        parameters: &'p [P],
+        associated_fn_value: &AssociatedFnValue<I>,
+    ) -> (&'p [P], &'p [P]) {
+        let interner = self.interner();
+        let impl_datum = self.impl_datum(associated_fn_value.impl_id);
+        let impl_params_len = impl_datum.binders.len(interner);
+        assert!(parameters.len() >= impl_params_len);
+
+        // the impl parameters are a suffix
+        //
+        // [ P0..Pn, Pn...Pm ]
+        //           ^^^^^^^ impl parameters
+        let split_point = parameters.len() - impl_params_len;
+        let (other_params, impl_params) = parameters.split_at(split_point);
+        (impl_params, other_params)
+    }
+
+    /// Given the full set of parameters (or binders) for an associated
+    /// function datum (the one appearing in a trait), splits them into
+    /// the parameters for the *trait* and those for the *associated
+    /// function*.
+    ///
+    /// # Example
+    ///
+    /// ```ignore (example)
+    /// trait Foo<T> {
+    ///     fn f<'a>(&self, b: &'a ()) -> &'a ();
+    /// }
+    /// ```
+    ///
+    /// in this example, the full set of parameters would be `['x,
+    /// S, Y]`, where `'x` is the value for `'a`, `S` is the value for
+    /// `self` and `Y` is the value for `T`.
+    ///
+    /// # Returns
+    ///
+    /// Returns the tuple of:
+    ///
+    /// * the parameters for the impl (`[Y]`, in our example)
+    /// * the parameters for the associated fn value (`['x, S]`, in our
+    ///   example)
+    fn split_associated_fn_parameters<'p, P>(
+        &self,
+        parameters: &'p [P],
+        associated_ty_datum: &AssociatedFnDatum<I>,
+    ) -> (&'p [P], &'p [P]) {
+        let trait_datum = &self.trait_datum(associated_ty_datum.trait_id);
+        let trait_num_params = trait_datum.binders.len(self.interner());
+        let split_point = parameters.len() - trait_num_params;
+        let (other_params, trait_params) = parameters.split_at(split_point);
+        (trait_params, other_params)
+    }
+
+    /// Given the full set of parameters for an associated function
+    /// *value* (which appears in an impl), returns the trait reference
+    /// and projection that are being satisfied by that value.
+    ///
+    /// # Example
+    ///
+    /// ```ignore (example)
+    /// impl<T> Trait for Vec<T> {
+    ///     fn f<'a, U>(&self, r: &'a [U]);
+    /// }
+    /// ```
+    ///
+    /// Here we expect the full set of parameters for `f`, which would
+    /// be `['x, Y, Vec<T>, Z]`, where `'x` is the value for `'a`, `Y`
+    /// is the value for `U`, `Vec<T>` is the value for `&self`, and `Z`
+    /// is the value for `T`.
+    ///
+    /// Returns the pair of:
+    ///
+    /// * the parameters that apply to the impl (`Z`, in our example)
+    /// * the projection `<Vec<Z> as Trait>::f<'x, Y>`
+    #[instrument(level = "debug", skip(self, associated_fn_value))]
+    fn impl_parameters_and_projection_from_associated_fn_value<'p>(
+        &self,
+        parameters: &'p [GenericArg<I>],
+        associated_fn_value: &AssociatedFnValue<I>,
+    ) -> (&'p [GenericArg<I>], FnDefTy<I>) {
+        let interner = self.interner();
+
+        let impl_datum = self.impl_datum(associated_fn_value.impl_id);
+
+        // Get the trait ref from the impl -- so in our example above
+        // this would be `Box<!T>: Foo`.
+        let (impl_parameters, atv_parameters) =
+            self.split_associated_fn_value_parameters(&parameters, associated_fn_value);
+        let trait_ref = {
+            let opaque_ty_ref = impl_datum.binders.map_ref(|b| &b.trait_ref).cloned();
+            debug!(?opaque_ty_ref);
+            opaque_ty_ref.substitute(interner, impl_parameters)
+        };
+
+        // Create the parameters for the projection -- in our example
+        // above, this would be `['!a, Box<!T>]`, corresponding to
+        // `<Box<!T> as Foo>::Item<'!a>`
+        let projection_substitution = Substitution::from_iter(
+            interner,
+            atv_parameters
+                .iter()
+                .chain(trait_ref.substitution.iter(interner))
+                .cloned(),
+        );
+
+        let fn_def_ty = FnDefTy {
+            fn_def_id: associated_fn_value.fn_id.as_fn(),
+            substitution: projection_substitution,
+        };
+
+        debug!(?impl_parameters, ?trait_ref, ?fn_def_ty);
+
+        (impl_parameters, fn_def_ty)
+    }
 }
 
 impl<DB: RustIrDatabase<I> + ?Sized, I: Interner> Split<I> for DB {}
diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs
index ffe6c679b50..c41c9184926 100644
--- a/chalk-solve/src/wf.rs
+++ b/chalk-solve/src/wf.rs
@@ -135,9 +135,12 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> {
                 push_ty();
                 substitution.visit_with(self, outer_binder)
             }
-            TyKind::FnDef(fn_def, substitution) => {
+            TyKind::FnDef(FnDefTy {
+                fn_def_id,
+                substitution,
+            }) => {
                 push_ty();
-                fn_def.visit_with(self, outer_binder);
+                fn_def_id.visit_with(self, outer_binder);
                 substitution.visit_with(self, outer_binder)
             }
             TyKind::Ref(mutability, lifetime, ty) => {
@@ -604,7 +607,7 @@ fn compute_assoc_ty_goal<I: Interner>(
                 //     * original in trait, `Self: 'a`
                 //     * after substituting impl parameters, `Box<!T>: '!a`
                 let assoc_ty_datum = db.associated_ty_data(projection.associated_ty_id);
-                let AssociatedTyDatumBound {
+                let AssociatedItemDatumBound {
                     bounds: defn_bounds,
                     where_clauses: defn_where_clauses,
                 } = assoc_ty_datum
@@ -892,8 +895,8 @@ impl WfWellKnownConstraints {
 
     /// Verify constraints a CoerceUnsized impl.
     /// Rules for CoerceUnsized impl to be considered well-formed:
-    /// a) pointer conversions: &[mut] T -> &[mut] U, &[mut] T -> *[mut] U,
-    ///    *[mut] T -> *[mut] U are considered valid if
+    /// a) pointer conversions: `&[mut] T` -> `&[mut] U`, `&[mut] T` -> `*[mut] U`,
+    ///    `*[mut] T` -> `*[mut] U` are considered valid if
     ///    1) T: Unsize<U>
     ///    2) mutability is respected, i.e. immutable -> immutable, mutable -> immutable,
     ///       mutable -> mutable conversions are allowed, immutable -> mutable is not.
diff --git a/tests/display/unique_names.rs b/tests/display/unique_names.rs
index a566660a46a..494b2b0bc5d 100644
--- a/tests/display/unique_names.rs
+++ b/tests/display/unique_names.rs
@@ -64,6 +64,12 @@ where
     ) -> std::sync::Arc<chalk_solve::rust_ir::AssociatedTyDatum<I>> {
         self.db.associated_ty_data(ty)
     }
+    fn associated_fn_data(
+        &self,
+        f: chalk_ir::AssocFnDefId<I>,
+    ) -> Arc<chalk_solve::rust_ir::AssociatedFnDatum<I>> {
+        self.db.associated_fn_data(f)
+    }
     fn trait_datum(
         &self,
         trait_id: chalk_ir::TraitId<I>,
@@ -97,6 +103,12 @@ where
     ) -> std::sync::Arc<chalk_solve::rust_ir::AssociatedTyValue<I>> {
         self.db.associated_ty_value(id)
     }
+    fn associated_fn_value(
+        &self,
+        id: chalk_solve::rust_ir::AssociatedFnValueId<I>,
+    ) -> std::sync::Arc<chalk_solve::rust_ir::AssociatedFnValue<I>> {
+        self.db.associated_fn_value(id)
+    }
     fn generator_datum(
         &self,
         generator_id: chalk_ir::GeneratorId<I>,
diff --git a/tests/integration/panic.rs b/tests/integration/panic.rs
index 3c282aac0a2..af736595016 100644
--- a/tests/integration/panic.rs
+++ b/tests/integration/panic.rs
@@ -58,6 +58,10 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
         unimplemented!()
     }
 
+    fn associated_fn_data(&self, f: AssocFnDefId<ChalkIr>) -> Arc<AssociatedFnDatum<ChalkIr>> {
+        unimplemented!()
+    }
+
     // `trait Bar`, id `0`
     fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
         if let PanickingMethod::TraitDatum = self.panicking_method {
@@ -82,6 +86,7 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
                 coinductive: false,
             },
             associated_ty_ids: vec![],
+            fn_defs: vec![],
             well_known: None,
         })
     }
@@ -115,6 +120,7 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
             binders,
             impl_type: ImplType::Local,
             associated_ty_value_ids: vec![],
+            associated_fn_value_ids: vec![],
         })
     }
 
@@ -125,6 +131,13 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
         unimplemented!()
     }
 
+    fn associated_fn_value(
+        &self,
+        id: AssociatedFnValueId<ChalkIr>,
+    ) -> Arc<AssociatedFnValue<ChalkIr>> {
+        unimplemented!()
+    }
+
     fn opaque_ty_data(&self, id: OpaqueTyId<ChalkIr>) -> Arc<OpaqueTyDatum<ChalkIr>> {
         unimplemented!()
     }
diff --git a/tests/test/impls.rs b/tests/test/impls.rs
index 29bd458a98c..d325a1d599b 100644
--- a/tests/test/impls.rs
+++ b/tests/test/impls.rs
@@ -677,3 +677,238 @@ fn unify_types_in_impl() {
         }
     }
 }
+
+#[test]
+fn impl_function_basic() {
+    test! {
+        program {
+            trait Trait {
+                fn a();
+            }
+
+            struct A {}
+            struct B {}
+
+            impl@Impl Trait for A {
+                fn a();
+            }
+
+            impl@NotImpl Trait for B {
+                fn a();
+            }
+        }
+
+        goal {
+            exists <F> {
+                NormalizeFn(<A as Trait>::a -> F)
+            }
+        } yields {
+            "Unique; substitution [?0 := {impl @Impl}::a], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn impl_function_basic_generics() {
+    test! {
+        program {
+            trait Trait<T> {
+                fn a();
+            }
+
+            struct A<T> {}
+            struct B<T> {}
+            struct C {}
+
+            impl@Impl<T> Trait<T> for A<T> {
+                fn a();
+            }
+            impl@NotImpl<T> Trait<T> for B<T> {
+                fn a();
+            }
+        }
+
+        goal {
+            exists <F> {
+                NormalizeFn(<A<C> as Trait<C>>::a -> F)
+            }
+        } yields {
+            "Unique; substitution [?0 := {impl @Impl}::a<C>], lifetime constraints []"
+        }
+    }
+}
+
+#[ignore = "broken; TODO bug in chalk-integration"]
+#[test]
+fn impl_function_basic_fn_generics() {
+    test! {
+        program {
+            trait Trait<T> {
+                fn a<V>(v: V);
+            }
+
+            struct A<T> {}
+            struct B<T> {}
+            struct C {}
+
+            impl@Impl<T> Trait<T> for A<T> {
+                fn a<Vii>(v: Vii);
+            }
+            impl@NotImpl<T> Trait<T> for B<T> {
+                fn a<Vee>(v: Vee);
+            }
+        }
+
+        goal {
+            exists <F> {
+                NormalizeFn(<A<C> as Trait<C>>::a<C> -> F)
+            }
+        } yields {
+            "Unique; substitution [?0 := {impl @Impl}::a<C>], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn impl_function_tautology() {
+    test! {
+        program {
+            trait Trait<T> {
+                fn a();
+            }
+
+            struct A<T> {}
+            struct B<T> {}
+            struct C {}
+
+            impl@Impl<T> Trait<T> for A<T> {
+                fn a();
+            }
+            impl@NotImpl<T> Trait<T> for B<T> {
+                fn a();
+            }
+        }
+
+        goal {
+            NormalizeFn(<A<C> as Trait<C>>::a -> @Impl::a<C>)
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn impl_function_generic_arg() {
+    test! {
+        program {
+            trait Trait<T> {
+                fn a(v: T);
+            }
+
+            struct A<T> {}
+            struct B<T> {}
+            struct C {}
+
+            impl@Impl<T> Trait<T> for A<T> {
+                fn a(v: T);
+            }
+            impl@NotImpl<T> Trait<T> for B<T> {
+                fn a(v: T);
+            }
+        }
+
+        goal {
+            exists <F> {
+                NormalizeFn(<A<C> as Trait<C>>::a -> F)
+            }
+        } yields {
+            "Unique; substitution [?0 := {impl @Impl}::a<C>], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn impl_function_misses() {
+    test! {
+        program {
+            trait Trait {
+                fn a(v: u32);
+            }
+
+            struct A {}
+            struct C {}
+
+            impl@Impl Trait for A {
+                fn a(v: u32);
+            }
+        }
+
+        goal {
+            exists <F> {
+                NormalizeFn(<C as Trait>::a -> F)
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
+#[test]
+fn impl_function_where_unsat() {
+    test! {
+        program {
+            trait Trait {
+                fn a(v: u32);
+            }
+
+            trait WhereC {
+            }
+
+            struct A<T> {}
+            struct C {}
+
+
+            impl@Impl<T> Trait for A<T> where T: WhereC {
+                fn a(v: u32);
+            }
+        }
+
+        goal {
+            exists <F> {
+                NormalizeFn(<A<C> as Trait>::a -> F)
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
+#[test]
+fn impl_function_fn_where_unsat() {
+    test! {
+        program {
+            trait Trait<T> {
+                fn a(v: T) where T: WhereC;
+            }
+
+            trait WhereC {
+            }
+
+            struct A<T> {}
+            struct C {}
+
+
+            impl@Impl<T> Trait<T> for A<T> {
+                fn a(v: T) where T: WhereC;
+            }
+        }
+
+        goal {
+            exists <F> {
+                NormalizeFn(<A<C> as Trait<C>>::a -> F)
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
diff --git a/tests/test/mod.rs b/tests/test/mod.rs
index d6e20364aa7..c3b57ca94c6 100644
--- a/tests/test/mod.rs
+++ b/tests/test/mod.rs
@@ -231,9 +231,9 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>, co
         );
 
         let program = if coherence {
-            db.checked_program().unwrap()
+            db.checked_program().expect("checked_program failed")
         } else {
-            db.program_ir().unwrap()
+            db.program_ir().expect("program_ir failed")
         };
 
         for (goal_text, solver_choice, expected) in goals {
@@ -254,11 +254,14 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>, co
                 println!("goal {}", goal_text);
                 assert!(goal_text.starts_with("{"));
                 assert!(goal_text.ends_with("}"));
-                let goal = lower_goal(
-                    &*chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1]).unwrap(),
-                    &*program,
-                )
-                .unwrap();
+                let parsed = chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1]);
+
+                if let Err(e) = parsed {
+                    println!("Parse error:\n{}", e);
+                    panic!("parse error above");
+                }
+                let parsed = parsed.unwrap();
+                let goal = lower_goal(&*parsed, &*program).expect("lower_goal failed");
 
                 println!("using solver: {:?}", solver_choice);
                 let peeled_goal = goal.into_peeled_goal(db.interner());