413 lines
21 KiB
HTML
413 lines
21 KiB
HTML
<!DOCTYPE HTML>
|
||
<html lang="en" class="light sidebar-visible" dir="ltr">
|
||
<head>
|
||
<!-- Book generated using mdBook -->
|
||
<meta charset="UTF-8">
|
||
<title>Canonical queries - Rust Compiler Development Guide</title>
|
||
|
||
|
||
<!-- Custom HTML head -->
|
||
|
||
<meta name="description" content="A guide to developing the Rust compiler (rustc)">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||
<meta name="theme-color" content="#ffffff">
|
||
|
||
<link rel="icon" href="../favicon.svg">
|
||
<link rel="shortcut icon" href="../favicon.png">
|
||
<link rel="stylesheet" href="../css/variables.css">
|
||
<link rel="stylesheet" href="../css/general.css">
|
||
<link rel="stylesheet" href="../css/chrome.css">
|
||
<link rel="stylesheet" href="../css/print.css" media="print">
|
||
|
||
<!-- Fonts -->
|
||
<link rel="stylesheet" href="../FontAwesome/css/font-awesome.css">
|
||
<link rel="stylesheet" href="../fonts/fonts.css">
|
||
|
||
<!-- Highlight.js Stylesheets -->
|
||
<link rel="stylesheet" id="highlight-css" href="../highlight.css">
|
||
<link rel="stylesheet" id="tomorrow-night-css" href="../tomorrow-night.css">
|
||
<link rel="stylesheet" id="ayu-highlight-css" href="../ayu-highlight.css">
|
||
|
||
<!-- Custom theme stylesheets -->
|
||
|
||
|
||
<!-- Provide site root and default themes to javascript -->
|
||
<script>
|
||
const path_to_root = "../";
|
||
const default_light_theme = "light";
|
||
const default_dark_theme = "navy";
|
||
</script>
|
||
<!-- Start loading toc.js asap -->
|
||
<script src="../toc.js"></script>
|
||
</head>
|
||
<body>
|
||
<div id="body-container">
|
||
<!-- Work around some values being stored in localStorage wrapped in quotes -->
|
||
<script>
|
||
try {
|
||
let theme = localStorage.getItem('mdbook-theme');
|
||
let sidebar = localStorage.getItem('mdbook-sidebar');
|
||
|
||
if (theme.startsWith('"') && theme.endsWith('"')) {
|
||
localStorage.setItem('mdbook-theme', theme.slice(1, theme.length - 1));
|
||
}
|
||
|
||
if (sidebar.startsWith('"') && sidebar.endsWith('"')) {
|
||
localStorage.setItem('mdbook-sidebar', sidebar.slice(1, sidebar.length - 1));
|
||
}
|
||
} catch (e) { }
|
||
</script>
|
||
|
||
<!-- Set the theme before any content is loaded, prevents flash -->
|
||
<script>
|
||
const default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? default_dark_theme : default_light_theme;
|
||
let theme;
|
||
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
|
||
if (theme === null || theme === undefined) { theme = default_theme; }
|
||
const html = document.documentElement;
|
||
html.classList.remove('light')
|
||
html.classList.add(theme);
|
||
html.classList.add("js");
|
||
</script>
|
||
|
||
<input type="checkbox" id="sidebar-toggle-anchor" class="hidden">
|
||
|
||
<!-- Hide / unhide sidebar before it is displayed -->
|
||
<script>
|
||
let sidebar = null;
|
||
const sidebar_toggle = document.getElementById("sidebar-toggle-anchor");
|
||
if (document.body.clientWidth >= 1080) {
|
||
try { sidebar = localStorage.getItem('mdbook-sidebar'); } catch(e) { }
|
||
sidebar = sidebar || 'visible';
|
||
} else {
|
||
sidebar = 'hidden';
|
||
}
|
||
sidebar_toggle.checked = sidebar === 'visible';
|
||
html.classList.remove('sidebar-visible');
|
||
html.classList.add("sidebar-" + sidebar);
|
||
</script>
|
||
|
||
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
|
||
<!-- populated by js -->
|
||
<mdbook-sidebar-scrollbox class="sidebar-scrollbox"></mdbook-sidebar-scrollbox>
|
||
<noscript>
|
||
<iframe class="sidebar-iframe-outer" src="../toc.html"></iframe>
|
||
</noscript>
|
||
<div id="sidebar-resize-handle" class="sidebar-resize-handle">
|
||
<div class="sidebar-resize-indicator"></div>
|
||
</div>
|
||
</nav>
|
||
|
||
<div id="page-wrapper" class="page-wrapper">
|
||
|
||
<div class="page">
|
||
<div id="menu-bar-hover-placeholder"></div>
|
||
<div id="menu-bar" class="menu-bar sticky">
|
||
<div class="left-buttons">
|
||
<label id="sidebar-toggle" class="icon-button" for="sidebar-toggle-anchor" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
|
||
<i class="fa fa-bars"></i>
|
||
</label>
|
||
<button id="theme-toggle" class="icon-button" type="button" title="Change theme" aria-label="Change theme" aria-haspopup="true" aria-expanded="false" aria-controls="theme-list">
|
||
<i class="fa fa-paint-brush"></i>
|
||
</button>
|
||
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
|
||
<li role="none"><button role="menuitem" class="theme" id="default_theme">Auto</button></li>
|
||
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
|
||
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
|
||
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
|
||
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
|
||
<li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
|
||
</ul>
|
||
<button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
|
||
<i class="fa fa-search"></i>
|
||
</button>
|
||
</div>
|
||
|
||
<h1 class="menu-title">Rust Compiler Development Guide</h1>
|
||
|
||
<div class="right-buttons">
|
||
<a href="../print.html" title="Print this book" aria-label="Print this book">
|
||
<i id="print-button" class="fa fa-print"></i>
|
||
</a>
|
||
<a href="https://github.com/rust-lang/rustc-dev-guide" title="Git repository" aria-label="Git repository">
|
||
<i id="git-repository-button" class="fa fa-github"></i>
|
||
</a>
|
||
<a href="https://github.com/rust-lang/rustc-dev-guide/edit/master/src/traits/canonical-queries.md" title="Suggest an edit" aria-label="Suggest an edit">
|
||
<i id="git-edit-button" class="fa fa-edit"></i>
|
||
</a>
|
||
|
||
</div>
|
||
</div>
|
||
|
||
<div id="search-wrapper" class="hidden">
|
||
<form id="searchbar-outer" class="searchbar-outer">
|
||
<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
|
||
</form>
|
||
<div id="searchresults-outer" class="searchresults-outer hidden">
|
||
<div id="searchresults-header" class="searchresults-header"></div>
|
||
<ul id="searchresults">
|
||
</ul>
|
||
</div>
|
||
</div>
|
||
|
||
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
|
||
<script>
|
||
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
|
||
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
|
||
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
|
||
link.setAttribute('tabIndex', sidebar === 'visible' ? 0 : -1);
|
||
});
|
||
</script>
|
||
|
||
<div id="content" class="content">
|
||
<main>
|
||
<h1 id="canonical-queries"><a class="header" href="#canonical-queries">Canonical queries</a></h1>
|
||
<p>The "start" of the trait system is the <strong>canonical query</strong> (these are
|
||
both queries in the more general sense of the word – something you
|
||
would like to know the answer to – and in the
|
||
<a href="../query.html">rustc-specific sense</a>). The idea is that the type
|
||
checker or other parts of the system, may in the course of doing their
|
||
thing want to know whether some trait is implemented for some type
|
||
(e.g., is <code>u32: Debug</code> true?). Or they may want to
|
||
normalize some associated type.</p>
|
||
<p>This section covers queries at a fairly high level of abstraction. The
|
||
subsections look a bit more closely at how these ideas are implemented
|
||
in rustc.</p>
|
||
<h2 id="the-traditional-interactive-prolog-query"><a class="header" href="#the-traditional-interactive-prolog-query">The traditional, interactive Prolog query</a></h2>
|
||
<p>In a traditional Prolog system, when you start a query, the solver
|
||
will run off and start supplying you with every possible answer it can
|
||
find. So given something like this:</p>
|
||
<pre><code class="language-text">?- Vec<i32>: AsRef<?U>
|
||
</code></pre>
|
||
<p>The solver might answer:</p>
|
||
<pre><code class="language-text">Vec<i32>: AsRef<[i32]>
|
||
continue? (y/n)
|
||
</code></pre>
|
||
<p>This <code>continue</code> bit is interesting. The idea in Prolog is that the
|
||
solver is finding <strong>all possible</strong> instantiations of your query that
|
||
are true. In this case, if we instantiate <code>?U = [i32]</code>, then the query
|
||
is true (note that a traditional Prolog interface does not, directly,
|
||
tell us a value for <code>?U</code>, but we can infer one by unifying the
|
||
response with our original query – Rust's solver gives back a
|
||
substitution instead). If we were to hit <code>y</code>, the solver might then
|
||
give us another possible answer:</p>
|
||
<pre><code class="language-text">Vec<i32>: AsRef<Vec<i32>>
|
||
continue? (y/n)
|
||
</code></pre>
|
||
<p>This answer derives from the fact that there is a reflexive impl
|
||
(<code>impl<T> AsRef<T> for T</code>) for <code>AsRef</code>. If were to hit <code>y</code> again,
|
||
then we might get back a negative response:</p>
|
||
<pre><code class="language-text">no
|
||
</code></pre>
|
||
<p>Naturally, in some cases, there may be no possible answers, and hence
|
||
the solver will just give me back <code>no</code> right away:</p>
|
||
<pre><code class="language-text">?- Box<i32>: Copy
|
||
no
|
||
</code></pre>
|
||
<p>In some cases, there might be an infinite number of responses. So for
|
||
example if I gave this query, and I kept hitting <code>y</code>, then the solver
|
||
would never stop giving me back answers:</p>
|
||
<pre><code class="language-text">?- Vec<?U>: Clone
|
||
Vec<i32>: Clone
|
||
continue? (y/n)
|
||
Vec<Box<i32>>: Clone
|
||
continue? (y/n)
|
||
Vec<Box<Box<i32>>>: Clone
|
||
continue? (y/n)
|
||
Vec<Box<Box<Box<i32>>>>: Clone
|
||
continue? (y/n)
|
||
</code></pre>
|
||
<p>As you can imagine, the solver will gleefully keep adding another
|
||
layer of <code>Box</code> until we ask it to stop, or it runs out of memory.</p>
|
||
<p>Another interesting thing is that queries might still have variables
|
||
in them. For example:</p>
|
||
<pre><code class="language-text">?- Rc<?T>: Clone
|
||
</code></pre>
|
||
<p>might produce the answer:</p>
|
||
<pre><code class="language-text">Rc<?T>: Clone
|
||
continue? (y/n)
|
||
</code></pre>
|
||
<p>After all, <code>Rc<?T></code> is true <strong>no matter what type <code>?T</code> is</strong>.</p>
|
||
<p><a id="query-response"></a></p>
|
||
<h2 id="a-trait-query-in-rustc"><a class="header" href="#a-trait-query-in-rustc">A trait query in rustc</a></h2>
|
||
<p>The trait queries in rustc work somewhat differently. Instead of
|
||
trying to enumerate <strong>all possible</strong> answers for you, they are looking
|
||
for an <strong>unambiguous</strong> answer. In particular, when they tell you the
|
||
value for a type variable, that means that this is the <strong>only possible
|
||
instantiation</strong> that you could use, given the current set of impls and
|
||
where-clauses, that would be provable.</p>
|
||
<p>The response to a trait query in rustc is typically a
|
||
<code>Result<QueryResult<T>, NoSolution></code> (where the <code>T</code> will vary a bit
|
||
depending on the query itself). The <code>Err(NoSolution)</code> case indicates
|
||
that the query was false and had no answers (e.g., <code>Box<i32>: Copy</code>).
|
||
Otherwise, the <code>QueryResult</code> gives back information about the possible answer(s)
|
||
we did find. It consists of four parts:</p>
|
||
<ul>
|
||
<li><strong>Certainty:</strong> tells you how sure we are of this answer. It can have two
|
||
values:
|
||
<ul>
|
||
<li><code>Proven</code> means that the result is known to be true.
|
||
<ul>
|
||
<li>This might be the result for trying to prove <code>Vec<i32>: Clone</code>,
|
||
say, or <code>Rc<?T>: Clone</code>.</li>
|
||
</ul>
|
||
</li>
|
||
<li><code>Ambiguous</code> means that there were things we could not yet prove to
|
||
be either true <em>or</em> false, typically because more type information
|
||
was needed. (We'll see an example shortly.)
|
||
<ul>
|
||
<li>This might be the result for trying to prove <code>Vec<?T>: Clone</code>.</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
<li><strong>Var values:</strong> Values for each of the unbound inference variables
|
||
(like <code>?T</code>) that appeared in your original query. (Remember that in Prolog,
|
||
we had to infer these.)
|
||
<ul>
|
||
<li>As we'll see in the example below, we can get back var values even
|
||
for <code>Ambiguous</code> cases.</li>
|
||
</ul>
|
||
</li>
|
||
<li><strong>Region constraints:</strong> these are relations that must hold between
|
||
the lifetimes that you supplied as inputs. We'll ignore these here.</li>
|
||
<li><strong>Value:</strong> The query result also comes with a value of type <code>T</code>. For
|
||
some specialized queries – like normalizing associated types –
|
||
this is used to carry back an extra result, but it's often just
|
||
<code>()</code>.</li>
|
||
</ul>
|
||
<h3 id="examples"><a class="header" href="#examples">Examples</a></h3>
|
||
<p>Let's work through an example query to see what all the parts mean.
|
||
Consider <a href="https://doc.rust-lang.org/std/borrow/trait.Borrow.html">the <code>Borrow</code> trait</a>. This trait has a number of
|
||
impls; among them, there are these two (for clarity, I've written the
|
||
<code>Sized</code> bounds explicitly):</p>
|
||
<pre><code class="language-rust ignore">impl<T> Borrow<T> for T where T: ?Sized
|
||
impl<T> Borrow<[T]> for Vec<T> where T: Sized</code></pre>
|
||
<p><strong>Example 1.</strong> Imagine we are type-checking this (rather artificial)
|
||
bit of code:</p>
|
||
<pre><code class="language-rust ignore">fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }
|
||
|
||
fn main() {
|
||
let mut t: Vec<_> = vec![]; // Type: Vec<?T>
|
||
let mut u: Option<_> = None; // Type: Option<?U>
|
||
foo(t, u); // Example 1: requires `Vec<?T>: Borrow<?U>`
|
||
...
|
||
}</code></pre>
|
||
<p>As the comments indicate, we first create two variables <code>t</code> and <code>u</code>;
|
||
<code>t</code> is an empty vector and <code>u</code> is a <code>None</code> option. Both of these
|
||
variables have unbound inference variables in their type: <code>?T</code>
|
||
represents the elements in the vector <code>t</code> and <code>?U</code> represents the
|
||
value stored in the option <code>u</code>. Next, we invoke <code>foo</code>; comparing the
|
||
signature of <code>foo</code> to its arguments, we wind up with <code>A = Vec<?T></code> and
|
||
<code>B = ?U</code>. Therefore, the where clause on <code>foo</code> requires that <code>Vec<?T>: Borrow<?U></code>. This is thus our first example trait query.</p>
|
||
<p>There are many possible solutions to the query <code>Vec<?T>: Borrow<?U></code>;
|
||
for example:</p>
|
||
<ul>
|
||
<li><code>?U = Vec<?T></code>,</li>
|
||
<li><code>?U = [?T]</code>,</li>
|
||
<li><code>?T = u32, ?U = [u32]</code></li>
|
||
<li>and so forth.</li>
|
||
</ul>
|
||
<p>Therefore, the result we get back would be as follows (I'm going to
|
||
ignore region constraints and the "value"):</p>
|
||
<ul>
|
||
<li>Certainty: <code>Ambiguous</code> – we're not sure yet if this holds</li>
|
||
<li>Var values: <code>[?T = ?T, ?U = ?U]</code> – we learned nothing about the values of
|
||
the variables</li>
|
||
</ul>
|
||
<p>In short, the query result says that it is too soon to say much about
|
||
whether this trait is proven. During type-checking, this is not an
|
||
immediate error: instead, the type checker would hold on to this
|
||
requirement (<code>Vec<?T>: Borrow<?U></code>) and wait. As we'll see in the next
|
||
example, it may happen that <code>?T</code> and <code>?U</code> wind up constrained from
|
||
other sources, in which case we can try the trait query again.</p>
|
||
<p><strong>Example 2.</strong> We can now extend our previous example a bit,
|
||
and assign a value to <code>u</code>:</p>
|
||
<pre><code class="language-rust ignore">fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }
|
||
|
||
fn main() {
|
||
// What we saw before:
|
||
let mut t: Vec<_> = vec![]; // Type: Vec<?T>
|
||
let mut u: Option<_> = None; // Type: Option<?U>
|
||
foo(t, u); // `Vec<?T>: Borrow<?U>` => ambiguous
|
||
|
||
// New stuff:
|
||
u = Some(vec![]); // ?U = Vec<?V>
|
||
}</code></pre>
|
||
<p>As a result of this assignment, the type of <code>u</code> is forced to be
|
||
<code>Option<Vec<?V>></code>, where <code>?V</code> represents the element type of the
|
||
vector. This in turn implies that <code>?U</code> is <a href="../type-checking.html">unified</a> to <code>Vec<?V></code>.</p>
|
||
<p>Let's suppose that the type checker decides to revisit the
|
||
"as-yet-unproven" trait obligation we saw before, <code>Vec<?T>: Borrow<?U></code>. <code>?U</code> is no longer an unbound inference variable; it now
|
||
has a value, <code>Vec<?V></code>. So, if we "refresh" the query with that value, we get:</p>
|
||
<pre><code class="language-text">Vec<?T>: Borrow<Vec<?V>>
|
||
</code></pre>
|
||
<p>This time, there is only one impl that applies, the reflexive impl:</p>
|
||
<pre><code class="language-text">impl<T> Borrow<T> for T where T: ?Sized
|
||
</code></pre>
|
||
<p>Therefore, the trait checker will answer:</p>
|
||
<ul>
|
||
<li>Certainty: <code>Proven</code></li>
|
||
<li>Var values: <code>[?T = ?T, ?V = ?T]</code></li>
|
||
</ul>
|
||
<p>Here, it is saying that we have indeed proven that the obligation
|
||
holds, and we also know that <code>?T</code> and <code>?V</code> are the same type (but we
|
||
don't know what that type is yet!).</p>
|
||
<p>(In fact, as the function ends here, the type checker would give an
|
||
error at this point, since the element types of <code>t</code> and <code>u</code> are still
|
||
not yet known, even though they are known to be the same.)</p>
|
||
|
||
</main>
|
||
|
||
<nav class="nav-wrapper" aria-label="Page navigation">
|
||
<!-- Mobile navigation buttons -->
|
||
<a rel="prev" href="../traits/goals-and-clauses.html" class="mobile-nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
|
||
<i class="fa fa-angle-left"></i>
|
||
</a>
|
||
|
||
<a rel="next prefetch" href="../traits/canonicalization.html" class="mobile-nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
|
||
<i class="fa fa-angle-right"></i>
|
||
</a>
|
||
|
||
<div style="clear: both"></div>
|
||
</nav>
|
||
</div>
|
||
</div>
|
||
|
||
<nav class="nav-wide-wrapper" aria-label="Page navigation">
|
||
<a rel="prev" href="../traits/goals-and-clauses.html" class="nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
|
||
<i class="fa fa-angle-left"></i>
|
||
</a>
|
||
|
||
<a rel="next prefetch" href="../traits/canonicalization.html" class="nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
|
||
<i class="fa fa-angle-right"></i>
|
||
</a>
|
||
</nav>
|
||
|
||
</div>
|
||
|
||
|
||
|
||
|
||
<script>
|
||
window.playground_copyable = true;
|
||
</script>
|
||
|
||
|
||
<script src="../elasticlunr.min.js"></script>
|
||
<script src="../mark.min.js"></script>
|
||
<script src="../searcher.js"></script>
|
||
|
||
<script src="../clipboard.min.js"></script>
|
||
<script src="../highlight.js"></script>
|
||
<script src="../book.js"></script>
|
||
|
||
<!-- Custom JS scripts -->
|
||
<script src="../mermaid.min.js"></script>
|
||
<script src="../mermaid-init.js"></script>
|
||
|
||
|
||
</div>
|
||
</body>
|
||
</html>
|