From ad2eb6f6a51792d0b0965b75c2099a15b0ed7d5b Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Thu, 10 May 2018 15:22:12 -0700 Subject: [PATCH 1/8] Added an overview of chalk --- src/doc/rustc-dev-guide/src/SUMMARY.md | 1 + src/doc/rustc-dev-guide/src/chalk-overview.md | 140 ++++++++++++++++++ src/doc/rustc-dev-guide/src/traits-slg.md | 2 + 3 files changed, 143 insertions(+) create mode 100644 src/doc/rustc-dev-guide/src/chalk-overview.md diff --git a/src/doc/rustc-dev-guide/src/SUMMARY.md b/src/doc/rustc-dev-guide/src/SUMMARY.md index 1839f59cb164..4923d4972494 100644 --- a/src/doc/rustc-dev-guide/src/SUMMARY.md +++ b/src/doc/rustc-dev-guide/src/SUMMARY.md @@ -38,6 +38,7 @@ - [The lowering module in rustc](./traits-lowering-module.md) - [Well-formedness checking](./traits-wf.md) - [The SLG solver](./traits-slg.md) + - [An Overview of Chalk](./chalk-overview.md) - [Bibliography](./traits-bibliography.md) - [Type checking](./type-checking.md) - [Method Lookup](./method-lookup.md) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md new file mode 100644 index 000000000000..63757f7baacf --- /dev/null +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -0,0 +1,140 @@ +# An Overview of Chalk + +> Chalk is under heavy development, so if any of these links are broken or if +> any of the information is inconsistent with the code or outdated, please open +> an issue so we can fix it. If you are able to fix the issue yourself, we would +> love your contribution! + +[Chalk][chalk] recasts Rust's trait system explicitly in terms of logic +programming by "lowering" Rust code into a kind of logic program we can then +execute queries against. Its goal is to be an executable, highly readable +specification of the Rust trait system.[^negativechalk] + +There are many expected benefits from this work. It will consolidate our +existing, somewhat ad-hoc implementation into something far more principled and +expressive, which should behave better in corner cases, and be much easier to +extend.[^negativechalk] + +## Resources + +* [Chalk Source Code](https://github.com/rust-lang-nursery/chalk) +* [Chalk Glossary](https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md) +* The traits section of the rustc guide (you are here) + +### Blog Posts + +* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/) +* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/) +* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/) +* [Negative reasoning in Chalk](http://aturon.github.io/blog/2017/04/24/negative-chalk/) +* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/) +* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/) +* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/) + +## Parsing + +Chalk is designed to be incorporated with the Rust compiler, so the syntax and +concepts it deals with heavily borrow from Rust. It is convenient for the sake +of testing to be able to run chalk on its own, so chalk includes a parser for a +Rust-like syntax. + +The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. +You can find the [complete definition of the AST][chalk-ast] in the source code. + +The syntax contains things from Rust that we know and love for example traits, +impls, and struct definitions. Parsing is often the first "phase" of +transformation that a program goes through in order to become a format that +chalk can understand. + +## Lowering + +After parsing, there is a "lowering" phase. This aims to convert traits/impls +into "program clauses". A [`ProgramClause` (source code)][programclause] is +essentially one of the following: + +* A [clause] of the form `consequence :- conditions` where `:-` is read as + "if" and `conditions = cond1 && cond2 && ...` +* A universally quantified clause of the form `forall { consequence :- conditions }` + * `forall { ... }` is used to represent [universal quantification]. See the + section on [Lowering to logic][lowering-forall] for more information. + * A key thing to note about `forall` is that we don't allow you to "quantify" + over traits, only types and regions (lifetimes). That is, you can't make a + rule like `forall { u32: Trait }` which would say "`u32` implements + all traits". You can however say `forall { T: Trait }` meaning "`Trait` + is implemented by all types". + * `forall { ... }` is represented in the code using the [`Binders` + struct][binders-struct]. + +This is the phase where we encode the rules of the trait system into logic. For +example, if we have: + +```rust +impl Clone for Vec {} +``` + +We generate: + +```rust +forall { (Vec: Clone) :- (T: Clone) } +``` + +This rule dictates that `Vec: Clone` is only satisfied if `T: Clone` is also +satisfied (i.e. "provable"). + +### Well-formedness checks + +As part of lowering from the AST to the internal IR, we also do some "well +formedness" checks. See the [source code][well-formedness-checks] for where +those are done. The call to `record_specialization_priorities` checks +"coherence" which means that it ensures that two impls of the same trait for the +same type cannot exist. + +## Intermediate Representation (IR) + +The second intermediate representation in chalk is called, well, the "ir". :) +The [IR source code][ir-code] contains the complete definition. The +`ir::Program` struct contains some "rust things" but indexed and accessible in +a different way. This is sort of analogous to the [HIR] in Rust. + +For example, if you have a type like `Foo`, we would represent `Foo` as a +string in the AST but in `ir::Program`, we use numeric indices (`ItemId`). + +In addition to `ir::Program` which has "rust-like things", there is also +`ir::ProgramEnvironment` which is "pure logic". The main field in that is +`program_clauses` which contains the `ProgramClause`s that we generated +previously. + +## Rules + +The `rules` module works by iterating over every trait, impl, etc. and emitting +the rules that come from each one. The traits section of the rustc-guide (that +you are currently reading) contains the most up-to-date reference on that. + +The `ir::ProgramEnvironment` is created [in this module][rules-environment]. + +## Testing + +TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L112-L148) +that will take syntax and run it through the full pipeline described above. +[This](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L83-L110) +is the function that is ultimately called. + +## Solver + +See [The SLG Solver][slg]. + +[^negativechalk]: [*Negative reasoning in Chalk* by Aaron Turon](http://aturon.github.io/blog/2017/04/24/negative-chalk/) + +[chalk]: https://github.com/rust-lang-nursery/chalk +[ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree +[chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs +[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification +[lowering-forall]: traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses +[programclause]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L721 +[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause +[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/lowering/mod.rs#L230-L232 +[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/ir/mod.rs +[HIR]: hir.html +[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L661 +[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/rules/mod.rs#L9 +[slg]: traits-slg.html diff --git a/src/doc/rustc-dev-guide/src/traits-slg.md b/src/doc/rustc-dev-guide/src/traits-slg.md index cdd52ece953f..1dc56e14c713 100644 --- a/src/doc/rustc-dev-guide/src/traits-slg.md +++ b/src/doc/rustc-dev-guide/src/traits-slg.md @@ -1 +1,3 @@ # The SLG solver + +TODO: From 78034750d366a7c1981510b793161602704d0028 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Thu, 10 May 2018 15:43:18 -0700 Subject: [PATCH 2/8] Lines must be <= 80 characters UNLESS there is a link --- src/doc/rustc-dev-guide/src/chalk-overview.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md index 63757f7baacf..8c5bc1594fce 100644 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -54,7 +54,8 @@ essentially one of the following: * A [clause] of the form `consequence :- conditions` where `:-` is read as "if" and `conditions = cond1 && cond2 && ...` -* A universally quantified clause of the form `forall { consequence :- conditions }` +* A universally quantified clause of the form + `forall { consequence :- conditions }` * `forall { ... }` is used to represent [universal quantification]. See the section on [Lowering to logic][lowering-forall] for more information. * A key thing to note about `forall` is that we don't allow you to "quantify" @@ -129,7 +130,7 @@ See [The SLG Solver][slg]. [ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree [chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification -[lowering-forall]: traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses +[lowering-forall]: https://rust-lang-nursery.github.io/rustc-guide/traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses [programclause]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L721 [clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause [well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/lowering/mod.rs#L230-L232 From cf689b2db429c6286b47b009cc9df26a9b56cba6 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Thu, 10 May 2018 15:48:24 -0700 Subject: [PATCH 3/8] Ignoring code examples that aren't actually compile-able --- src/doc/rustc-dev-guide/src/chalk-overview.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md index 8c5bc1594fce..49f685149175 100644 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -69,13 +69,13 @@ essentially one of the following: This is the phase where we encode the rules of the trait system into logic. For example, if we have: -```rust +```rust,ignore impl Clone for Vec {} ``` We generate: -```rust +```rust,ignore forall { (Vec: Clone) :- (T: Clone) } ``` From a5254db9b72940af4657bed2b68cf7ece9044225 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Fri, 11 May 2018 17:14:26 -0700 Subject: [PATCH 4/8] Updating links to match latest code --- src/doc/rustc-dev-guide/src/chalk-overview.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md index 49f685149175..7cea6acef7b3 100644 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -115,9 +115,9 @@ The `ir::ProgramEnvironment` is created [in this module][rules-environment]. ## Testing -TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L112-L148) +TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L112-L148) that will take syntax and run it through the full pipeline described above. -[This](https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/solve/test/mod.rs#L83-L110) +[This](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L83-L110) is the function that is ultimately called. ## Solver @@ -131,11 +131,11 @@ See [The SLG Solver][slg]. [chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification [lowering-forall]: https://rust-lang-nursery.github.io/rustc-guide/traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses -[programclause]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L721 +[programclause]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L721 [clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause -[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/lowering/mod.rs#L230-L232 -[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/ir/mod.rs +[well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir/lowering.rs#L230-L232 +[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/ir.rs [HIR]: hir.html -[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/ir/mod.rs#L661 -[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/17abbabe53c2f78b04af04a9bc9e8a0e3fc676e3/src/rules/mod.rs#L9 +[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661 +[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9 [slg]: traits-slg.html From 3788625a9769388298d865e7bf4f0a8bcc4b1ea6 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 10:52:21 -0700 Subject: [PATCH 5/8] Changes from review --- src/doc/rustc-dev-guide/src/chalk-overview.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md index 7cea6acef7b3..cd2c98b88ea6 100644 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -1,19 +1,20 @@ # An Overview of Chalk > Chalk is under heavy development, so if any of these links are broken or if -> any of the information is inconsistent with the code or outdated, please open -> an issue so we can fix it. If you are able to fix the issue yourself, we would +> any of the information is inconsistent with the code or outdated, please +> [open an issue][rustc-issues] so we can fix it. If you are able to fix the issue yourself, we would > love your contribution! [Chalk][chalk] recasts Rust's trait system explicitly in terms of logic programming by "lowering" Rust code into a kind of logic program we can then -execute queries against. Its goal is to be an executable, highly readable -specification of the Rust trait system.[^negativechalk] +execute queries against. (See [*Lowering to Logic*][lowering-to-logic] and +[*Lowering Rules*][lowering-rules]) Its goal is to be an executable, highly +readable specification of the Rust trait system. There are many expected benefits from this work. It will consolidate our existing, somewhat ad-hoc implementation into something far more principled and expressive, which should behave better in corner cases, and be much easier to -extend.[^negativechalk] +extend. ## Resources @@ -124,9 +125,10 @@ is the function that is ultimately called. See [The SLG Solver][slg]. -[^negativechalk]: [*Negative reasoning in Chalk* by Aaron Turon](http://aturon.github.io/blog/2017/04/24/negative-chalk/) - +[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues [chalk]: https://github.com/rust-lang-nursery/chalk +[lowering-to-logic]: traits-lowering-to-logic.html +[lowering-rules]: traits-lowering-rules.html [ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree [chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs [universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification From 97c8ed36232a3cc2ab696d86022143e0ef7f2d84 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 11:18:14 -0700 Subject: [PATCH 6/8] More review changes --- src/doc/rustc-dev-guide/src/chalk-overview.md | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md index cd2c98b88ea6..926c7f5ace5e 100644 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -2,8 +2,8 @@ > Chalk is under heavy development, so if any of these links are broken or if > any of the information is inconsistent with the code or outdated, please -> [open an issue][rustc-issues] so we can fix it. If you are able to fix the issue yourself, we would -> love your contribution! +> [open an issue][rustc-issues] so we can fix it. If you are able to fix the +> issue yourself, we would love your contribution! [Chalk][chalk] recasts Rust's trait system explicitly in terms of logic programming by "lowering" Rust code into a kind of logic program we can then @@ -42,7 +42,7 @@ Rust-like syntax. The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. You can find the [complete definition of the AST][chalk-ast] in the source code. -The syntax contains things from Rust that we know and love for example traits, +The syntax contains things from Rust that we know and love, for example: traits, impls, and struct definitions. Parsing is often the first "phase" of transformation that a program goes through in order to become a format that chalk can understand. @@ -67,14 +67,14 @@ essentially one of the following: * `forall { ... }` is represented in the code using the [`Binders` struct][binders-struct]. -This is the phase where we encode the rules of the trait system into logic. For -example, if we have: +Lowering is the phase where we encode the rules of the trait system into logic. +For example, if we have the following Rust: ```rust,ignore impl Clone for Vec {} ``` -We generate: +We generate the following program clause: ```rust,ignore forall { (Vec: Clone) :- (T: Clone) } @@ -102,22 +102,23 @@ For example, if you have a type like `Foo`, we would represent `Foo` as a string in the AST but in `ir::Program`, we use numeric indices (`ItemId`). In addition to `ir::Program` which has "rust-like things", there is also -`ir::ProgramEnvironment` which is "pure logic". The main field in that is +`ir::ProgramEnvironment` which is "pure logic". The main field in that struct is `program_clauses` which contains the `ProgramClause`s that we generated previously. ## Rules The `rules` module works by iterating over every trait, impl, etc. and emitting -the rules that come from each one. The traits section of the rustc-guide (that -you are currently reading) contains the most up-to-date reference on that. +the rules that come from each one. See [Lowering Rules][lowering-rules] for the +most up-to-date reference on that. The `ir::ProgramEnvironment` is created [in this module][rules-environment]. ## Testing TODO: Basically, [there is a macro](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L112-L148) -that will take syntax and run it through the full pipeline described above. +that will take chalk's Rust-like syntax and run it through the full pipeline +described above. [This](https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/solve/test.rs#L83-L110) is the function that is ultimately called. From 7741e2f4caab612a4cb8d49d3d20708719ca4b1d Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 11:21:20 -0700 Subject: [PATCH 7/8] Even more review changes --- src/doc/rustc-dev-guide/src/chalk-overview.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md index 926c7f5ace5e..02e094293015 100644 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -37,7 +37,8 @@ extend. Chalk is designed to be incorporated with the Rust compiler, so the syntax and concepts it deals with heavily borrow from Rust. It is convenient for the sake of testing to be able to run chalk on its own, so chalk includes a parser for a -Rust-like syntax. +Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is +not intended to look exactly like it or support the exact same syntax. The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. You can find the [complete definition of the AST][chalk-ast] in the source code. From 131ae09207f37a46d1bb3f1de6565bd773b40e36 Mon Sep 17 00:00:00 2001 From: Sunjay Varma Date: Mon, 14 May 2018 11:26:15 -0700 Subject: [PATCH 8/8] Missed a few things because of GitHub's UI --- src/doc/rustc-dev-guide/src/chalk-overview.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/doc/rustc-dev-guide/src/chalk-overview.md b/src/doc/rustc-dev-guide/src/chalk-overview.md index 02e094293015..76c119a5ed34 100644 --- a/src/doc/rustc-dev-guide/src/chalk-overview.md +++ b/src/doc/rustc-dev-guide/src/chalk-overview.md @@ -68,6 +68,8 @@ essentially one of the following: * `forall { ... }` is represented in the code using the [`Binders` struct][binders-struct]. +*See also: [Goals and Clauses][goals-and-clauses]* + Lowering is the phase where we encode the rules of the trait system into logic. For example, if we have the following Rust: @@ -137,6 +139,7 @@ See [The SLG Solver][slg]. [lowering-forall]: https://rust-lang-nursery.github.io/rustc-guide/traits-lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses [programclause]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L721 [clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause +[goals-and-clauses]: traits-goals-and-clauses.html [well-formedness-checks]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir/lowering.rs#L230-L232 [ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/ir.rs [HIR]: hir.html