Debugging Trait Errors as Logic Programs D hatra ’23

Gavin Gray (@gavinleroy)	ETH Zürich
Will Crichton	Brown University

Traits are widely (ab)used

forth!(
  : factorial (n -- n) 1 swap fact0 ;
  : fact0 (n n -- n) dup 1 = if drop else dup rot * swap pred fact0 then ;
  5 factorial .
);

github.com/Ashymad/fortraith

diesel documentation

bevy discussions

Traits 101

trait IntoString {
  fn to_string(&self) -> String;
}

impl IntoString for (i32, i32) {
  fn to_string(&self) -> String {
    format!(
      "({}, {})",
      self.0, self.1
    )
  }
}

impl<T: IntoString>
  IntoString for Vec<T> {
  fn to_string(&self) -> String
  { /* ... */ }
}

fn main() {
  let v: Vec<(i32, i32)> = vec![
    (0, 1), (2, 3)
  ];
  println!("{}", v.to_string());
}

A trait definition, establishing the unit of shared behavior.

Traits 101

trait IntoString {
  fn to_string(&self) -> String;
}

impl IntoString for (i32, i32) {
  fn to_string(&self) -> String {
    format!(
      "({}, {})",
      self.0, self.1
    )
  }
}

impl<T: IntoString>
  IntoString for Vec<T> {
  fn to_string(&self) -> String
  { /* ... */ }
}

fn main() {
  let v: Vec<(i32, i32)> = vec![
    (0, 1), (2, 3)
  ];
  println!("{}", v.to_string());
}

(i32, i32): IntoString.

A trait implementation associates a type with a trait.

Traits 101

trait IntoString {
  fn to_string(&self) -> String;
}

impl IntoString for (i32, i32) {
  fn to_string(&self) -> String {
    format!(
      "({}, {})",
      self.0, self.1
    )
  }
}

impl<T: IntoString>
  IntoString for Vec<T> {
  fn to_string(&self) -> String
  { /* ... */ }
}

fn main() {
  let v: Vec<(i32, i32)> = vec![
    (0, 1), (2, 3)
  ];
  println!("{}", v.to_string());
}

(i32, i32): IntoString.

Vec<T>: IntoString :-
  T: IntoString.

Implementations can be parametric.

Traits 101

trait IntoString {
  fn to_string(&self) -> String;
}

impl IntoString for (i32, i32) {
  fn to_string(&self) -> String {
    format!(
      "({}, {})",
      self.0, self.1
    )
  }
}

impl<T: IntoString>
  IntoString for Vec<T> {
  fn to_string(&self) -> String
  { /* ... */ }
}

fn main() {
  let v: Vec<(i32, i32)> = vec![
    (0, 1), (2, 3)
  ];
  println!("{}", v.to_string());
}

(i32, i32): IntoString.

Vec<T>: IntoString :-
  T: IntoString.

?- Vec<(i32, i32)>: IntoString.

Type-checking queries the current facts.

Type-checking is tracing Prolog

(i32, i32): IntoString.

Vec<T>: IntoString :-
  T: IntoString.

?- Vec<(i32, i32)>: IntoString.

flowchart TD
A["?- Vec<(i32, i32)>: IntoString"]

Type-checking is tracing Prolog

(i32, i32): IntoString.

Vec<T>: IntoString :-
  T: IntoString.

?- Vec<(i32, i32)>: IntoString.

flowchart TD
A["?- Vec<(i32, i32)>: IntoString"]
B["(i32, i32): IntoString"];
A --> B

Type-checking is tracing Prolog

(i32, i32): IntoString.

Vec<T>: IntoString :-
  T: IntoString.

?- Vec<(i32, i32)>: IntoString.

flowchart TD
A["?- Vec<(i32, i32)>: IntoString"]
B["(i32, i32): IntoString"];
A --> B
C["Yes"]
B --> C

Tracing a failed query

(i32, i32): IntoString.

Vec<T>: IntoString :-
  T: IntoString.

?- Vec<String>: IntoString.

fn main() {
  let v: Vec<String> = vec![
    String::from("We're"),
    String::from("Strings!")
  ];
  println!("{}", v.to_string());
}

flowchart TD
  A["?- Vec&ltString>: IntoString"]
  B["String: IntoString"];
  A --> B
  C["No"]
  B --> C

A good Rust diagnostic

error[E0599]: the method `to_string` exists for struct `Vec<String>`,
  but its trait bounds were not satisfied
  --> src/main.rs:24:20
   |
24 |   println!("{}", v.to_string());
   |                    ^^^^^^^^^
   |   method cannot be called on `Vec<String>` due to unsatisfied trait bounds
   |
   = note: doesn't satisfy `String: IntoString`
   = note: doesn't satisfy `Vec<String>: IntoString`
   |
note: trait bound `String: IntoString` was not satisfied
  --> src/main.rs:14:9
   |
14 | impl<T: IntoString>
   |         ^^^^^^^^^^ unsatisfied trait bound introduced here
15 |   IntoString for Vec<T> {
   |   ----------     ------

flowchart TD
  A["?- Vec&ltString>: IntoString"]
  B["String: IntoString"];
  A --> B
  C["No"]
  B --> C

Trait-heavy crates across domains

bevy: game development.
axum: web applications.
nalgebra: linear algebra.
diesel: extensible ORM and query builder.
︙

bevyengine.org

How simple is it really?

Hello World! from Bevy

use bevy::prelude::*;

#[derive(Resource)]
struct Timer(usize);

fn run_timer(timer: Res<Timer>) {
  /* ... */
}

fn main() {
  App::new()
    .insert_resource(Timer(0))
    .add_system(run_timer)
    .run();
}

Hello World! from Bevy

use bevy::prelude::*;

#[derive(Resource)]
struct Timer(usize);

fn run_timer(timer: Timer) {
  /* ... */
}

fn main() {
  App::new()
    .insert_resource(Timer(0))
    .add_system(run_timer)
    .run();
}

A poor Rust diagnostic

We’re looking for the information about Timer: SystemParam.

Timer nor SystemParam is mentioned in the ~30 line diagnostic.

The trait bound `fn(Timer) {run_timer}: IntoSystem<(), (), _>` is not satisfied
  --> src/main.rs:6:24
   |
6  | fn main() { use_system(run_timer) }
   |             ---------- ^^^^^^^^^ the trait `IntoSystem<(), (), _>`
   |             | is not implemented for fn item `fn(Timer) {run_timer}`
   |             |
   |             required by a bound introduced by this call
   |
note: required for `fn(Timer) {run_timer}` to implement `bevy::prelude::IntoSystemConfig<_>`
  --> src/main.rs:41:9
   |
41 |         IntoSystemConfig<Marker> for F
   |         ^^^^^^^^^^^^^^^^^^^^^^^^     ^
42 |         where F: IntoSystem<(), (), Marker> {}
   |                  ------------------ unsatisfied trait bound introduced here
note: required by a bound in `use_system`
  --> src/main.rs:4:26
   |
4  | fn use_system<M>(_: impl IntoSystemConfig<M>) {}
   |                          ^^^^^^^^^^^^^^^^^^^ required by this bound in `use_system`

Why?

But…documentation!

Shouldn’t documentation aid developers in understanding diagnostics?

Information spans across:

3 pages
92 trait implementations!

Tracing the type-checker for our Bevy example

Why does Bevy produce a worse diagnostic?

Timer: Resource.
Res<T>: SystemParam :-
    T: Resource.

fn(P0): SystemParamFunc :-
  P0: SystemParam.

fn(TheWorld): ExclSystemParamFunc.

F: IntoSystem :-
  F: SystemParamFunc.

F: IntoSystem :-
  F: ExclSystemParamFunc.

F: IntoSystemConfigs :-
  F: IntoSystem.

?- fn(Timer): IntoSystem.

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A,B,C,D,E,F,H invisible

  A ~~~ B

  B ~~~ C

  C ~~~ D

  D ~~~ E

  B ~~~ F

  F ~~~ H

Why does Bevy produce a worse diagnostic?

Timer: Resource.
Res<T>: SystemParam :-
    T: Resource.

fn(P0): SystemParamFunc :-
  P0: SystemParam.

fn(TheWorld): ExclSystemParamFunc.

F: IntoSystem :-
  F: SystemParamFunc.

F: IntoSystem :-
  F: ExclSystemParamFunc.

F: IntoSystemConfigs :-
  F: IntoSystem.

?- fn(Timer): IntoSystem.

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A,C,D,E,F,H invisible

  B ~~~ C

  C ~~~ D

  D ~~~ E

  B ~~~ F

  F ~~~ H

Why does Bevy produce a worse diagnostic?

Timer: Resource.
Res<T>: SystemParam :-
    T: Resource.

fn(P0): SystemParamFunc :-
  P0: SystemParam.

fn(TheWorld): ExclSystemParamFunc.

F: IntoSystem :-
  F: SystemParamFunc.

F: IntoSystem :-
  F: ExclSystemParamFunc.

F: IntoSystemConfigs :-
  F: IntoSystem.

?- fn(Timer): IntoSystem.

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A,D,E,H invisible

  B -.-> C

  C ~~~ D

  D ~~~ E

  B -.-> F

  F ~~~ H

Why does Bevy produce a worse diagnostic?

Timer: Resource.
Res<T>: SystemParam :-
    T: Resource.

fn(P0): SystemParamFunc :-
  P0: SystemParam.

fn(TheWorld): ExclSystemParamFunc.

F: IntoSystem :-
  F: SystemParamFunc.

F: IntoSystem :-
  F: ExclSystemParamFunc.

F: IntoSystemConfigs :-
  F: IntoSystem.

?- fn(Timer): IntoSystem.

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A,D,E invisible

  B -.-> C

  C ~~~ D

  D ~~~ E

  B -.-> F

  F --> H

Why does Bevy produce a worse diagnostic?

Timer: Resource.
Res<T>: SystemParam :-
    T: Resource.

fn(P0): SystemParamFunc :-
  P0: SystemParam.

fn(TheWorld): ExclSystemParamFunc.

F: IntoSystem :-
  F: SystemParamFunc.

F: IntoSystem :-
  F: ExclSystemParamFunc.

F: IntoSystemConfigs :-
  F: IntoSystem.

?- fn(Timer): IntoSystem.

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A,E invisible

  B -.-> C

  C --> D

  D ~~~ E

  B -.-> F

  F --> H

Why does Bevy produce a worse diagnostic?

Timer: Resource.
Res<T>: SystemParam :-
    T: Resource.

fn(P0): SystemParamFunc :-
  P0: SystemParam.

fn(TheWorld): ExclSystemParamFunc.

F: IntoSystem :-
  F: SystemParamFunc.

F: IntoSystem :-
  F: ExclSystemParamFunc.

F: IntoSystemConfigs :-
  F: IntoSystem.

?- fn(Timer): IntoSystem.

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A invisible

  B -.-> C

  C --> D

  D --> E

  B -.-> F

  F --> H

error[E0599]: the method `to_string` exists for struct `Vec<String>`,
  but its trait bounds were not satisfied
  --> src/main.rs:24:20
   |
24 |   println!("{}", v.to_string());
   |                    ^^^^^^^^^
   |   method cannot be called on `Vec<String>` due to unsatisfied trait bounds
   |
   = note: doesn't satisfy `String: IntoString`
   = note: doesn't satisfy `Vec<String>: IntoString`
   |
note: trait bound `String: IntoString` was not satisfied
  --> src/main.rs:14:9
   |
14 | impl<T: IntoString>
   |         ^^^^^^^^^^ unsatisfied trait bound introduced here
15 |   IntoString for Vec<T> {
   |   ----------     ------

flowchart TD
  A["?- Vec&ltString>: IntoString"]
  B["String: IntoString"];
  A --> B
  C["No"]
  B --> C

The trait bound `fn(Timer) {run_timer}: IntoSystem<(), (), _>` is not satisfied
  --> src/main.rs:6:24
   |
6  | fn main() { use_system(run_timer) }
   |             ---------- ^^^^^^^^^ the trait `IntoSystem<(), (), _>`
   |             | is not implemented for fn item `fn(Timer) {run_timer}`
   |             |
   |             required by a bound introduced by this call
   |
note: required for `fn(Timer) {run_timer}` to implement `bevy::prelude::IntoSystemConfig<_>`
  --> src/main.rs:41:9
   |
41 |         IntoSystemConfig<Marker> for F
   |         ^^^^^^^^^^^^^^^^^^^^^^^^     ^
42 |         where F: IntoSystem<(), (), Marker> {}
   |                  ------------------ unsatisfied trait bound introduced here
note: required by a bound in `use_system`
  --> src/main.rs:4:26
   |
4  | fn use_system<M>(_: impl IntoSystemConfig<M>) {}
   |                          ^^^^^^^^^^^^^^^^^^^ required by this bound in `use_system`

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A invisible

  B -.-> C

  C --> D

  D --> E

  B -.-> F

  F --> H

We see this as an interface problem.

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A invisible

  B -.-> C

  C --> D

  D --> E

  B -.-> F

  F --> H

Debugging traits is debugging an arbitrary program!

overflow evaluating the requirement `_: diesel::Expression`
  --> src/main.rs:15:10
   |
15 |         .group_by(users::id)
   |          ^^^^^^^^

Demo

Dealing with large data

requirements on the impl of
  `LoadQuery<'_, _, (i32, std::string::String)>`
for
  `SelectStatement<FromClause<users::table>, diesel::query_builder::select_clause::DefaultSelectClause<FromClause<users::table>>, diesel::query_builder::distinct_clause::NoDistinctClause, diesel::query_builder::where_clause::WhereClause<diesel::expression::grouped::Grouped<diesel::expression::operators::Eq<users::columns::id, posts::columns::id>>>>`

Incremental information

requirements on the impl of
  LoadQuery●
'_, _, (●
i32, String
)
for
  SelectStatement●
FromClause●
users::table
, DefaultSelectClause●
FromClause●
users::table
, NoDistinctClause, WhereClause●
Grouped●
Eq●
users::columns::id, posts::columns::id

Summary

App::new()
  .insert_resource(Timer(0))
  .add_system(run_timer)
  .run();

flowchart TD
  A["?- Vec&ltString>: IntoString"]
  B["String: IntoString"];
  A --> B
  C["No"]
  B --> C

flowchart TD
  classDef invisible display:none
  A["?- fn(Timer): IntoSystemConfigs"]
  B{{"fn(Timer): IntoSystem"}}

  C["fn(Timer): SystemParamFunc"]
  D["Timer: SystemParam"]
  E["No"]

  F["fn(Timer): ExclSystemParamFunc"]
  H["No"]


  class A invisible

  B -.-> C

  C --> D

  D --> E

  B -.-> F

  F --> H

LoadQuery●
'_, _, (●
i32, String
)
: SelectStatement●
FromClause●
users::table
, DefaultSelectClause●
FromClause●
users::table
, NoDistinctClause, WhereClause●
Grouped●
Eq●
users::columns::id, posts::columns::id

What approach would you take if you were to build a trait debugger?
Are there related problems where this approach could be useful? (E.g., I think debugging Coq tactics is closely relatead.)
What features would you want in such an interface?