[INFO] cloning repository https://github.com/ivanmoreau/lambdatype
[INFO] running `Command { std: "git" "-c" "credential.helper=" "-c" "credential.helper=/workspace/cargo-home/bin/git-credential-null" "clone" "--bare" "https://github.com/ivanmoreau/lambdatype" "/workspace/cache/git-repos/https%3A%2F%2Fgithub.com%2Fivanmoreau%2Flambdatype", kill_on_drop: false }`
[INFO] [stderr] Cloning into bare repository '/workspace/cache/git-repos/https%3A%2F%2Fgithub.com%2Fivanmoreau%2Flambdatype'...
[INFO] running `Command { std: "git" "rev-parse" "HEAD", kill_on_drop: false }`
[INFO] [stdout] 6f77cc3afaf728abba2a97f4f27fa14cfc909ef3
[INFO] checking ivanmoreau/lambdatype against try#44e31dee3cf6f37b4f652572897bb0eb25c477ee for pr-139763
[INFO] running `Command { std: "git" "clone" "/workspace/cache/git-repos/https%3A%2F%2Fgithub.com%2Fivanmoreau%2Flambdatype" "/workspace/builds/worker-3-tc2/source", kill_on_drop: false }`
[INFO] [stderr] Cloning into '/workspace/builds/worker-3-tc2/source'...
[INFO] [stderr] done.
[INFO] validating manifest of git repo https://github.com/ivanmoreau/lambdatype on toolchain 44e31dee3cf6f37b4f652572897bb0eb25c477ee
[INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+44e31dee3cf6f37b4f652572897bb0eb25c477ee" "metadata" "--manifest-path" "Cargo.toml" "--no-deps", kill_on_drop: false }`
[INFO] started tweaking git repo https://github.com/ivanmoreau/lambdatype
[INFO] finished tweaking git repo https://github.com/ivanmoreau/lambdatype
[INFO] tweaked toml for git repo https://github.com/ivanmoreau/lambdatype written to /workspace/builds/worker-3-tc2/source/Cargo.toml
[INFO] crate git repo https://github.com/ivanmoreau/lambdatype already has a lockfile, it will not be regenerated
[INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+44e31dee3cf6f37b4f652572897bb0eb25c477ee" "fetch" "--manifest-path" "Cargo.toml", kill_on_drop: false }`
[INFO] [stderr]     Blocking waiting for file lock on package cache
[INFO] [stderr]     Blocking waiting for file lock on package cache
[INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-3-tc2/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-3-tc2/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:b0b074c097205a61b89e8ad263052f976b2b332c4dc5f02aef1fe52501660d6e" "/opt/rustwide/cargo-home/bin/cargo" "+44e31dee3cf6f37b4f652572897bb0eb25c477ee" "metadata" "--no-deps" "--format-version=1", kill_on_drop: false }`
[INFO] [stdout] 47446a2048bb53aebef860510d0a2a8ab369c27ef460353bf1fa86c1b6c7e56e
[INFO] running `Command { std: "docker" "start" "-a" "47446a2048bb53aebef860510d0a2a8ab369c27ef460353bf1fa86c1b6c7e56e", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "inspect" "47446a2048bb53aebef860510d0a2a8ab369c27ef460353bf1fa86c1b6c7e56e", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "rm" "-f" "47446a2048bb53aebef860510d0a2a8ab369c27ef460353bf1fa86c1b6c7e56e", kill_on_drop: false }`
[INFO] [stdout] 47446a2048bb53aebef860510d0a2a8ab369c27ef460353bf1fa86c1b6c7e56e
[INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-3-tc2/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-3-tc2/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=forbid" "-e" "RUSTDOCFLAGS=--cap-lints=forbid" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:b0b074c097205a61b89e8ad263052f976b2b332c4dc5f02aef1fe52501660d6e" "/opt/rustwide/cargo-home/bin/cargo" "+44e31dee3cf6f37b4f652572897bb0eb25c477ee" "check" "--frozen" "--all" "--all-targets" "--message-format=json", kill_on_drop: false }`
[INFO] [stdout] 7fe0d0e97b584afe64b83a66d29e57373bcf41ad49de6fc15f0f20b838c0c3bb
[INFO] running `Command { std: "docker" "start" "-a" "7fe0d0e97b584afe64b83a66d29e57373bcf41ad49de6fc15f0f20b838c0c3bb", kill_on_drop: false }`
[INFO] [stderr]     Checking lambdatype v0.1.0 (/opt/rustwide/workdir)
[INFO] [stdout] error[E0275]: overflow evaluating the requirement `(Z, S<_>): LessT`
[INFO] [stdout]    |
[INFO] [stdout]    = help: consider increasing the recursion limit by adding a `#![recursion_limit = "4000"]` attribute to your crate (`lambdatype`)
[INFO] [stdout] note: required for `(S<Z>, S<S<_>>)` to implement `LessT`
[INFO] [stdout]   --> src/main.rs:59:22
[INFO] [stdout]    |
[INFO] [stdout] 59 | impl<N: Nat, M: Nat> LessT for (S<N>, S<M>) 
[INFO] [stdout]    |                      ^^^^^     ^^^^^^^^^^^^
[INFO] [stdout] 60 | where (N, M) : LessT
[INFO] [stdout]    |                ----- unsatisfied trait bound introduced here
[INFO] [stdout]    = note: 1998 redundant requirements hidden
[INFO] [stdout]    = note: required for `(S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<...>>>>>>>>>>>>>>>>>>>>, ...)` to implement `LessT`
[INFO] [stdout]    = note: the full name for the type has been written to '/opt/rustwide/target/debug/deps/lambdatype-ee9a7e4430299b80.long-type-7012635971493708198.txt'
[INFO] [stdout]    = note: consider using `--verbose` to print the full type name to the console
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, T): Shift` is not satisfied
[INFO] [stdout]   --> src/main.rs:74:19
[INFO] [stdout]    |
[INFO] [stdout] 74 |     type Output = Abs< <(C, I, T) as Shift>::Output >;
[INFO] [stdout]    |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Shift` is not implemented for `(C, I, T)`
[INFO] [stdout]    |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]    |
[INFO] [stdout] 73 | impl<C: Nat, I: Nat, T: Term> Shift for (C, I, Abs<T>) where (C, I, T): Shift {
[INFO] [stdout]    |                                                        ++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, F): Shift` is not satisfied
[INFO] [stdout]   --> src/main.rs:78:19
[INFO] [stdout]    |
[INFO] [stdout] 78 |       type Output = App< 
[INFO] [stdout]    |  ___________________^
[INFO] [stdout] 79 | |         <(C, I, F) as Shift>::Output, 
[INFO] [stdout] 80 | |         <(C, I, L) as Shift>::Output 
[INFO] [stdout] 81 | |     >;
[INFO] [stdout]    | |_____^ the trait `Shift` is not implemented for `(C, I, F)`
[INFO] [stdout]    |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]    |
[INFO] [stdout] 77 | impl<C: Nat, I: Nat, F: Term, L: Term> Shift for (C, I, App<F, L>) where (C, I, F): Shift {
[INFO] [stdout]    |                                                                    ++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, L): Shift` is not satisfied
[INFO] [stdout]   --> src/main.rs:78:19
[INFO] [stdout]    |
[INFO] [stdout] 78 |       type Output = App< 
[INFO] [stdout]    |  ___________________^
[INFO] [stdout] 79 | |         <(C, I, F) as Shift>::Output, 
[INFO] [stdout] 80 | |         <(C, I, L) as Shift>::Output 
[INFO] [stdout] 81 | |     >;
[INFO] [stdout]    | |_____^ the trait `Shift` is not implemented for `(C, I, L)`
[INFO] [stdout]    |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]    |
[INFO] [stdout] 77 | impl<C: Nat, I: Nat, F: Term, L: Term> Shift for (C, I, App<F, L>) where (C, I, L): Shift {
[INFO] [stdout]    |                                                                    ++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(N, M): Sub` is not satisfied
[INFO] [stdout]    --> src/main.rs:118:19
[INFO] [stdout]     |
[INFO] [stdout] 118 |     type Output = <(N, M) as Sub>::Output;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^ the trait `Sub` is not implemented for `(N, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 117 | impl<N: Nat, M:Nat> Sub for (S<N>, S<M>) where (N, M): Sub {
[INFO] [stdout]     |                                          +++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0275]: overflow evaluating the requirement `(Z, S<_>): LessT`
[INFO] [stdout]    |
[INFO] [stdout]    = help: consider increasing the recursion limit by adding a `#![recursion_limit = "4000"]` attribute to your crate (`lambdatype`)
[INFO] [stdout] note: required for `(S<Z>, S<S<_>>)` to implement `LessT`
[INFO] [stdout]   --> src/main.rs:59:22
[INFO] [stdout]    |
[INFO] [stdout] 59 | impl<N: Nat, M: Nat> LessT for (S<N>, S<M>) 
[INFO] [stdout]    |                      ^^^^^     ^^^^^^^^^^^^
[INFO] [stdout] 60 | where (N, M) : LessT
[INFO] [stdout]    |                ----- unsatisfied trait bound introduced here
[INFO] [stdout]    = note: 1998 redundant requirements hidden
[INFO] [stdout]    = note: required for `(S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<...>>>>>>>>>>>>>>>>>>>>, ...)` to implement `LessT`
[INFO] [stdout]    = note: the full name for the type has been written to '/opt/rustwide/target/debug/deps/lambdatype-98a6b4ebee17d054.long-type-17865862436567113313.txt'
[INFO] [stdout]    = note: consider using `--verbose` to print the full type name to the console
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, T): Shift` is not satisfied
[INFO] [stdout]   --> src/main.rs:74:19
[INFO] [stdout]    |
[INFO] [stdout] 74 |     type Output = Abs< <(C, I, T) as Shift>::Output >;
[INFO] [stdout]    |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Shift` is not implemented for `(C, I, T)`
[INFO] [stdout]    |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]    |
[INFO] [stdout] 73 | impl<C: Nat, I: Nat, T: Term> Shift for (C, I, Abs<T>) where (C, I, T): Shift {
[INFO] [stdout]    |                                                        ++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, F): Shift` is not satisfied
[INFO] [stdout]   --> src/main.rs:78:19
[INFO] [stdout]    |
[INFO] [stdout] 78 |       type Output = App< 
[INFO] [stdout]    |  ___________________^
[INFO] [stdout] 79 | |         <(C, I, F) as Shift>::Output, 
[INFO] [stdout] 80 | |         <(C, I, L) as Shift>::Output 
[INFO] [stdout] 81 | |     >;
[INFO] [stdout]    | |_____^ the trait `Shift` is not implemented for `(C, I, F)`
[INFO] [stdout]    |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]    |
[INFO] [stdout] 77 | impl<C: Nat, I: Nat, F: Term, L: Term> Shift for (C, I, App<F, L>) where (C, I, F): Shift {
[INFO] [stdout]    |                                                                    ++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, L): Shift` is not satisfied
[INFO] [stdout]   --> src/main.rs:78:19
[INFO] [stdout]    |
[INFO] [stdout] 78 |       type Output = App< 
[INFO] [stdout]    |  ___________________^
[INFO] [stdout] 79 | |         <(C, I, F) as Shift>::Output, 
[INFO] [stdout] 80 | |         <(C, I, L) as Shift>::Output 
[INFO] [stdout] 81 | |     >;
[INFO] [stdout]    | |_____^ the trait `Shift` is not implemented for `(C, I, L)`
[INFO] [stdout]    |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]    |
[INFO] [stdout] 77 | impl<C: Nat, I: Nat, F: Term, L: Term> Shift for (C, I, App<F, L>) where (C, I, L): Shift {
[INFO] [stdout]    |                                                                    ++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(N, M): Sub` is not satisfied
[INFO] [stdout]    --> src/main.rs:118:19
[INFO] [stdout]     |
[INFO] [stdout] 118 |     type Output = <(N, M) as Sub>::Output;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^ the trait `Sub` is not implemented for `(N, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 117 | impl<N: Nat, M:Nat> Sub for (S<N>, S<M>) where (N, M): Sub {
[INFO] [stdout]     |                                          +++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0275]: overflow evaluating the requirement `(Z, S<_>): LessT`
[INFO] [stdout]    |
[INFO] [stdout]    = help: consider increasing the recursion limit by adding a `#![recursion_limit = "4000"]` attribute to your crate (`lambdatype`)
[INFO] [stdout] note: required for `(S<Z>, S<S<_>>)` to implement `LessT`
[INFO] [stdout]   --> src/main.rs:59:22
[INFO] [stdout]    |
[INFO] [stdout] 59 | impl<N: Nat, M: Nat> LessT for (S<N>, S<M>) 
[INFO] [stdout]    |                      ^^^^^     ^^^^^^^^^^^^
[INFO] [stdout] 60 | where (N, M) : LessT
[INFO] [stdout]    |                ----- unsatisfied trait bound introduced here
[INFO] [stdout]    = note: 1998 redundant requirements hidden
[INFO] [stdout]    = note: required for `(S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<...>>>>>>>>>>>>>>>>>>>>, ...)` to implement `LessT`
[INFO] [stdout]    = note: the full name for the type has been written to '/opt/rustwide/target/debug/deps/lambdatype-ee9a7e4430299b80.long-type-4822432949164846947.txt'
[INFO] [stdout]    = note: consider using `--verbose` to print the full type name to the console
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, T): Unshift` is not satisfied
[INFO] [stdout]    --> src/main.rs:131:19
[INFO] [stdout]     |
[INFO] [stdout] 131 |     type Output = Abs< <(C, I, T) as Unshift>::Output >;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Unshift` is not implemented for `(C, I, T)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 130 | impl<C: Nat, I: Nat, T: Term> Unshift for (C, I, Abs<T>) where (C, I, T): Unshift {
[INFO] [stdout]     |                                                          ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, F): Unshift` is not satisfied
[INFO] [stdout]    --> src/main.rs:135:19
[INFO] [stdout]     |
[INFO] [stdout] 135 |       type Output = App< 
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 136 | |         <(C, I, F) as Unshift>::Output, 
[INFO] [stdout] 137 | |         <(C, I, L) as Unshift>::Output 
[INFO] [stdout] 138 | |     >;
[INFO] [stdout]     | |_____^ the trait `Unshift` is not implemented for `(C, I, F)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 134 | impl<C: Nat, I: Nat, F: Term, L: Term> Unshift for (C, I, App<F, L>) where (C, I, F): Unshift {
[INFO] [stdout]     |                                                                      ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, L): Unshift` is not satisfied
[INFO] [stdout]    --> src/main.rs:135:19
[INFO] [stdout]     |
[INFO] [stdout] 135 |       type Output = App< 
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 136 | |         <(C, I, F) as Unshift>::Output, 
[INFO] [stdout] 137 | |         <(C, I, L) as Unshift>::Output 
[INFO] [stdout] 138 | |     >;
[INFO] [stdout]     | |_____^ the trait `Unshift` is not implemented for `(C, I, L)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 134 | impl<C: Nat, I: Nat, F: Term, L: Term> Unshift for (C, I, App<F, L>) where (C, I, L): Unshift {
[INFO] [stdout]     |                                                                      ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(N, M): Sub` is not satisfied
[INFO] [stdout]    --> src/main.rs:146:19
[INFO] [stdout]     |
[INFO] [stdout] 146 |       type Output = <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 147 | |          <(<(<(N, M) as Sub>::Output, S<Z>) as LessT>::Output,
[INFO] [stdout] 148 | |          <(<(M, N) as Sub>::Output, S<Z>) as LessT>::Output) as And>::Output,
[INFO] [stdout] 149 | |          T, Var<N>
[INFO] [stdout] 150 | |     ) as IfT>::Output;
[INFO] [stdout]     | |_____________________^ the trait `Sub` is not implemented for `(N, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 145 | impl<N: Nat, T: Term, M: Nat> Substitution for (Var<N>, T, M) where (N, M): Sub {
[INFO] [stdout]     |                                                               +++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(M, N): Sub` is not satisfied
[INFO] [stdout]    --> src/main.rs:146:19
[INFO] [stdout]     |
[INFO] [stdout] 146 |       type Output = <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 147 | |          <(<(<(N, M) as Sub>::Output, S<Z>) as LessT>::Output,
[INFO] [stdout] 148 | |          <(<(M, N) as Sub>::Output, S<Z>) as LessT>::Output) as And>::Output,
[INFO] [stdout] 149 | |          T, Var<N>
[INFO] [stdout] 150 | |     ) as IfT>::Output;
[INFO] [stdout]     | |_____________________^ the trait `Sub` is not implemented for `(M, N)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 145 | impl<N: Nat, T: Term, M: Nat> Substitution for (Var<N>, T, M) where (M, N): Sub {
[INFO] [stdout]     |                                                               +++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `F: Term` is not satisfied
[INFO] [stdout]    --> src/main.rs:153:56
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) {
[INFO] [stdout]     |                                                        ^^^^^^^^^^^^^^^^^ the trait `Term` is not implemented for `F`
[INFO] [stdout]     |
[INFO] [stdout] note: required by a bound in `App`
[INFO] [stdout]    --> src/main.rs:17:15
[INFO] [stdout]     |
[INFO] [stdout] 17  | struct App<F: Term, L: Term>(PhantomData<F>, PhantomData<L>);
[INFO] [stdout]     |               ^^^^ required by this bound in `App`
[INFO] [stdout] help: consider further restricting type parameter `F` with trait `Term`
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat + Term, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) {
[INFO] [stdout]     |             ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(F, T, M): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:154:19
[INFO] [stdout]     |
[INFO] [stdout] 154 |       type Output = App<
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 155 | |         <(F, T, M) as Substitution>::Output,
[INFO] [stdout] 156 | |         <(L, T, M) as Substitution>::Output
[INFO] [stdout] 157 | |     >;
[INFO] [stdout]     | |_____^ the trait `Substitution` is not implemented for `(F, T, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) where (F, T, M): Substitution {
[INFO] [stdout]     |                                                                          +++++++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(L, T, M): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:154:19
[INFO] [stdout]     |
[INFO] [stdout] 154 |       type Output = App<
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 155 | |         <(F, T, M) as Substitution>::Output,
[INFO] [stdout] 156 | |         <(L, T, M) as Substitution>::Output
[INFO] [stdout] 157 | |     >;
[INFO] [stdout]     | |_____^ the trait `Substitution` is not implemented for `(L, T, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) where (L, T, M): Substitution {
[INFO] [stdout]     |                                                                          +++++++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `E: Term` is not satisfied
[INFO] [stdout]    --> src/main.rs:160:48
[INFO] [stdout]     |
[INFO] [stdout] 160 | impl<E: Nat, T: Term, M: Nat> Substitution for (Abs<E>, T, M) {
[INFO] [stdout]     |                                                ^^^^^^^^^^^^^^ the trait `Term` is not implemented for `E`
[INFO] [stdout]     |
[INFO] [stdout] note: required by a bound in `Abs`
[INFO] [stdout]    --> src/main.rs:18:15
[INFO] [stdout]     |
[INFO] [stdout] 18  | struct Abs<E: Term>(PhantomData<E>);
[INFO] [stdout]     |               ^^^^ required by this bound in `Abs`
[INFO] [stdout] help: consider further restricting type parameter `E` with trait `Term`
[INFO] [stdout]     |
[INFO] [stdout] 160 | impl<E: Nat + Term, T: Term, M: Nat> Substitution for (Abs<E>, T, M) {
[INFO] [stdout]     |             ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(Z, S<Z>, T): Shift` is not satisfied
[INFO] [stdout]    --> src/main.rs:161:19
[INFO] [stdout]     |
[INFO] [stdout] 161 |       type Output = Abs<<(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 162 | |         E,
[INFO] [stdout] 163 | |         <(Z, S<Z>, T) as Shift>::Output,
[INFO] [stdout] 164 | |         S<M>
[INFO] [stdout] 165 | |     ) as Substitution>::Output>;
[INFO] [stdout]     | |_______________________________^ the trait `Shift` is not implemented for `(Z, S<Z>, T)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 160 | impl<E: Nat, T: Term, M: Nat> Substitution for (Abs<E>, T, M) where (Z, S<Z>, T): Shift {
[INFO] [stdout]     |                                                               +++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(E, _, S<M>): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:161:19
[INFO] [stdout]     |
[INFO] [stdout] 161 |       type Output = Abs<<(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 162 | |         E,
[INFO] [stdout] 163 | |         <(Z, S<Z>, T) as Shift>::Output,
[INFO] [stdout] 164 | |         S<M>
[INFO] [stdout] 165 | |     ) as Substitution>::Output>;
[INFO] [stdout]     | |_______________________________^ the trait `Substitution` is not implemented for `(E, _, S<M>)`
[INFO] [stdout]     |
[INFO] [stdout]     = help: the following other types implement trait `Substitution`:
[INFO] [stdout]               (Abs<E>, T, M)
[INFO] [stdout]               (App<F, L>, T, M)
[INFO] [stdout]               (Var<N>, T, M)
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(Z, S<Z>, T2): Shift` is not satisfied
[INFO] [stdout]    --> src/main.rs:173:19
[INFO] [stdout]     |
[INFO] [stdout] 173 |       type Output = <( Z, S<Z>, <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 174 | |         T1,
[INFO] [stdout] 175 | |         <(Z, S<Z>, T2) as Shift>::Output,
[INFO] [stdout] 176 | |         Z
[INFO] [stdout] 177 | |     )as Substitution>::Output)as Unshift>::Output;
[INFO] [stdout]     | |_________________________________________________^ the trait `Shift` is not implemented for `(Z, S<Z>, T2)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 172 | impl<T1: Term, T2: Term> Beta for App<Abs<T1>, T2> where (Z, S<Z>, T2): Shift {
[INFO] [stdout]     |                                                    ++++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(T1, _, Z): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:173:19
[INFO] [stdout]     |
[INFO] [stdout] 173 |       type Output = <( Z, S<Z>, <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 174 | |         T1,
[INFO] [stdout] 175 | |         <(Z, S<Z>, T2) as Shift>::Output,
[INFO] [stdout] 176 | |         Z
[INFO] [stdout] 177 | |     )as Substitution>::Output)as Unshift>::Output;
[INFO] [stdout]     | |_________________________________________________^ the trait `Substitution` is not implemented for `(T1, _, Z)`
[INFO] [stdout]     |
[INFO] [stdout]     = help: the following other types implement trait `Substitution`:
[INFO] [stdout]               (Abs<E>, T, M)
[INFO] [stdout]               (App<F, L>, T, M)
[INFO] [stdout]               (Var<N>, T, M)
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `App<T1, T11>: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:181:19
[INFO] [stdout]     |
[INFO] [stdout] 181 |     type Output = App<<App<T1, T11> as Beta>::Output, <T2 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `App<T1, T11>`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 180 | impl<T1: Term, T11: Term, T2: Term> Beta for App<App<T1,T11>, T2> where App<T1, T11>: Beta {
[INFO] [stdout]     |                                                                   ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `T2: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:181:19
[INFO] [stdout]     |
[INFO] [stdout] 181 |     type Output = App<<App<T1, T11> as Beta>::Output, <T2 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `T2`
[INFO] [stdout]     |
[INFO] [stdout] help: consider further restricting type parameter `T2` with trait `Beta`
[INFO] [stdout]     |
[INFO] [stdout] 180 | impl<T1: Term, T11: Term, T2: Term + Beta> Beta for App<App<T1,T11>, T2> {
[INFO] [stdout]     |                                    ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `T2: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:185:19
[INFO] [stdout]     |
[INFO] [stdout] 185 |     type Output = App<<Var<T1> as Beta>::Output, <T2 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `T2`
[INFO] [stdout]     |
[INFO] [stdout] help: consider further restricting type parameter `T2` with trait `Beta`
[INFO] [stdout]     |
[INFO] [stdout] 184 | impl<T1: Nat, T2: Term + Beta> Beta for App<Var<T1>, T2> {
[INFO] [stdout]     |                        ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `T1: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:189:19
[INFO] [stdout]     |
[INFO] [stdout] 189 |     type Output = Abs<<T1 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `T1`
[INFO] [stdout]     |
[INFO] [stdout] help: consider further restricting type parameter `T1` with trait `Beta`
[INFO] [stdout]     |
[INFO] [stdout] 188 | impl<T1: Term + Beta> Beta for Abs<T1> {
[INFO] [stdout]     |               ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0275, E0277.
[INFO] [stdout] 
[INFO] [stdout] For more information about an error, try `rustc --explain E0275`.
[INFO] [stdout] 
[INFO] [stderr] error: could not compile `lambdatype` (bin "lambdatype" test) due to 23 previous errors
[INFO] [stderr] warning: build failed, waiting for other jobs to finish...
[INFO] [stdout] error[E0275]: overflow evaluating the requirement `(Z, S<_>): LessT`
[INFO] [stdout]    |
[INFO] [stdout]    = help: consider increasing the recursion limit by adding a `#![recursion_limit = "4000"]` attribute to your crate (`lambdatype`)
[INFO] [stdout] note: required for `(S<Z>, S<S<_>>)` to implement `LessT`
[INFO] [stdout]   --> src/main.rs:59:22
[INFO] [stdout]    |
[INFO] [stdout] 59 | impl<N: Nat, M: Nat> LessT for (S<N>, S<M>) 
[INFO] [stdout]    |                      ^^^^^     ^^^^^^^^^^^^
[INFO] [stdout] 60 | where (N, M) : LessT
[INFO] [stdout]    |                ----- unsatisfied trait bound introduced here
[INFO] [stdout]    = note: 1998 redundant requirements hidden
[INFO] [stdout]    = note: required for `(S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<...>>>>>>>>>>>>>>>>>>>>, ...)` to implement `LessT`
[INFO] [stdout]    = note: the full name for the type has been written to '/opt/rustwide/target/debug/deps/lambdatype-98a6b4ebee17d054.long-type-10899325929211480072.txt'
[INFO] [stdout]    = note: consider using `--verbose` to print the full type name to the console
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, T): Unshift` is not satisfied
[INFO] [stdout]    --> src/main.rs:131:19
[INFO] [stdout]     |
[INFO] [stdout] 131 |     type Output = Abs< <(C, I, T) as Unshift>::Output >;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Unshift` is not implemented for `(C, I, T)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 130 | impl<C: Nat, I: Nat, T: Term> Unshift for (C, I, Abs<T>) where (C, I, T): Unshift {
[INFO] [stdout]     |                                                          ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, F): Unshift` is not satisfied
[INFO] [stdout]    --> src/main.rs:135:19
[INFO] [stdout]     |
[INFO] [stdout] 135 |       type Output = App< 
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 136 | |         <(C, I, F) as Unshift>::Output, 
[INFO] [stdout] 137 | |         <(C, I, L) as Unshift>::Output 
[INFO] [stdout] 138 | |     >;
[INFO] [stdout]     | |_____^ the trait `Unshift` is not implemented for `(C, I, F)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 134 | impl<C: Nat, I: Nat, F: Term, L: Term> Unshift for (C, I, App<F, L>) where (C, I, F): Unshift {
[INFO] [stdout]     |                                                                      ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(C, I, L): Unshift` is not satisfied
[INFO] [stdout]    --> src/main.rs:135:19
[INFO] [stdout]     |
[INFO] [stdout] 135 |       type Output = App< 
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 136 | |         <(C, I, F) as Unshift>::Output, 
[INFO] [stdout] 137 | |         <(C, I, L) as Unshift>::Output 
[INFO] [stdout] 138 | |     >;
[INFO] [stdout]     | |_____^ the trait `Unshift` is not implemented for `(C, I, L)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 134 | impl<C: Nat, I: Nat, F: Term, L: Term> Unshift for (C, I, App<F, L>) where (C, I, L): Unshift {
[INFO] [stdout]     |                                                                      ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(N, M): Sub` is not satisfied
[INFO] [stdout]    --> src/main.rs:146:19
[INFO] [stdout]     |
[INFO] [stdout] 146 |       type Output = <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 147 | |          <(<(<(N, M) as Sub>::Output, S<Z>) as LessT>::Output,
[INFO] [stdout] 148 | |          <(<(M, N) as Sub>::Output, S<Z>) as LessT>::Output) as And>::Output,
[INFO] [stdout] 149 | |          T, Var<N>
[INFO] [stdout] 150 | |     ) as IfT>::Output;
[INFO] [stdout]     | |_____________________^ the trait `Sub` is not implemented for `(N, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 145 | impl<N: Nat, T: Term, M: Nat> Substitution for (Var<N>, T, M) where (N, M): Sub {
[INFO] [stdout]     |                                                               +++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(M, N): Sub` is not satisfied
[INFO] [stdout]    --> src/main.rs:146:19
[INFO] [stdout]     |
[INFO] [stdout] 146 |       type Output = <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 147 | |          <(<(<(N, M) as Sub>::Output, S<Z>) as LessT>::Output,
[INFO] [stdout] 148 | |          <(<(M, N) as Sub>::Output, S<Z>) as LessT>::Output) as And>::Output,
[INFO] [stdout] 149 | |          T, Var<N>
[INFO] [stdout] 150 | |     ) as IfT>::Output;
[INFO] [stdout]     | |_____________________^ the trait `Sub` is not implemented for `(M, N)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 145 | impl<N: Nat, T: Term, M: Nat> Substitution for (Var<N>, T, M) where (M, N): Sub {
[INFO] [stdout]     |                                                               +++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `F: Term` is not satisfied
[INFO] [stdout]    --> src/main.rs:153:56
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) {
[INFO] [stdout]     |                                                        ^^^^^^^^^^^^^^^^^ the trait `Term` is not implemented for `F`
[INFO] [stdout]     |
[INFO] [stdout] note: required by a bound in `App`
[INFO] [stdout]    --> src/main.rs:17:15
[INFO] [stdout]     |
[INFO] [stdout] 17  | struct App<F: Term, L: Term>(PhantomData<F>, PhantomData<L>);
[INFO] [stdout]     |               ^^^^ required by this bound in `App`
[INFO] [stdout] help: consider further restricting type parameter `F` with trait `Term`
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat + Term, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) {
[INFO] [stdout]     |             ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(F, T, M): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:154:19
[INFO] [stdout]     |
[INFO] [stdout] 154 |       type Output = App<
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 155 | |         <(F, T, M) as Substitution>::Output,
[INFO] [stdout] 156 | |         <(L, T, M) as Substitution>::Output
[INFO] [stdout] 157 | |     >;
[INFO] [stdout]     | |_____^ the trait `Substitution` is not implemented for `(F, T, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) where (F, T, M): Substitution {
[INFO] [stdout]     |                                                                          +++++++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(L, T, M): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:154:19
[INFO] [stdout]     |
[INFO] [stdout] 154 |       type Output = App<
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 155 | |         <(F, T, M) as Substitution>::Output,
[INFO] [stdout] 156 | |         <(L, T, M) as Substitution>::Output
[INFO] [stdout] 157 | |     >;
[INFO] [stdout]     | |_____^ the trait `Substitution` is not implemented for `(L, T, M)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 153 | impl<F: Nat, L:Term, T: Term, M: Nat> Substitution for (App<F, L>, T, M) where (L, T, M): Substitution {
[INFO] [stdout]     |                                                                          +++++++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `E: Term` is not satisfied
[INFO] [stdout]    --> src/main.rs:160:48
[INFO] [stdout]     |
[INFO] [stdout] 160 | impl<E: Nat, T: Term, M: Nat> Substitution for (Abs<E>, T, M) {
[INFO] [stdout]     |                                                ^^^^^^^^^^^^^^ the trait `Term` is not implemented for `E`
[INFO] [stdout]     |
[INFO] [stdout] note: required by a bound in `Abs`
[INFO] [stdout]    --> src/main.rs:18:15
[INFO] [stdout]     |
[INFO] [stdout] 18  | struct Abs<E: Term>(PhantomData<E>);
[INFO] [stdout]     |               ^^^^ required by this bound in `Abs`
[INFO] [stdout] help: consider further restricting type parameter `E` with trait `Term`
[INFO] [stdout]     |
[INFO] [stdout] 160 | impl<E: Nat + Term, T: Term, M: Nat> Substitution for (Abs<E>, T, M) {
[INFO] [stdout]     |             ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(Z, S<Z>, T): Shift` is not satisfied
[INFO] [stdout]    --> src/main.rs:161:19
[INFO] [stdout]     |
[INFO] [stdout] 161 |       type Output = Abs<<(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 162 | |         E,
[INFO] [stdout] 163 | |         <(Z, S<Z>, T) as Shift>::Output,
[INFO] [stdout] 164 | |         S<M>
[INFO] [stdout] 165 | |     ) as Substitution>::Output>;
[INFO] [stdout]     | |_______________________________^ the trait `Shift` is not implemented for `(Z, S<Z>, T)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 160 | impl<E: Nat, T: Term, M: Nat> Substitution for (Abs<E>, T, M) where (Z, S<Z>, T): Shift {
[INFO] [stdout]     |                                                               +++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(E, _, S<M>): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:161:19
[INFO] [stdout]     |
[INFO] [stdout] 161 |       type Output = Abs<<(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 162 | |         E,
[INFO] [stdout] 163 | |         <(Z, S<Z>, T) as Shift>::Output,
[INFO] [stdout] 164 | |         S<M>
[INFO] [stdout] 165 | |     ) as Substitution>::Output>;
[INFO] [stdout]     | |_______________________________^ the trait `Substitution` is not implemented for `(E, _, S<M>)`
[INFO] [stdout]     |
[INFO] [stdout]     = help: the following other types implement trait `Substitution`:
[INFO] [stdout]               (Abs<E>, T, M)
[INFO] [stdout]               (App<F, L>, T, M)
[INFO] [stdout]               (Var<N>, T, M)
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(Z, S<Z>, T2): Shift` is not satisfied
[INFO] [stdout]    --> src/main.rs:173:19
[INFO] [stdout]     |
[INFO] [stdout] 173 |       type Output = <( Z, S<Z>, <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 174 | |         T1,
[INFO] [stdout] 175 | |         <(Z, S<Z>, T2) as Shift>::Output,
[INFO] [stdout] 176 | |         Z
[INFO] [stdout] 177 | |     )as Substitution>::Output)as Unshift>::Output;
[INFO] [stdout]     | |_________________________________________________^ the trait `Shift` is not implemented for `(Z, S<Z>, T2)`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 172 | impl<T1: Term, T2: Term> Beta for App<Abs<T1>, T2> where (Z, S<Z>, T2): Shift {
[INFO] [stdout]     |                                                    ++++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `(T1, _, Z): Substitution` is not satisfied
[INFO] [stdout]    --> src/main.rs:173:19
[INFO] [stdout]     |
[INFO] [stdout] 173 |       type Output = <( Z, S<Z>, <(
[INFO] [stdout]     |  ___________________^
[INFO] [stdout] 174 | |         T1,
[INFO] [stdout] 175 | |         <(Z, S<Z>, T2) as Shift>::Output,
[INFO] [stdout] 176 | |         Z
[INFO] [stdout] 177 | |     )as Substitution>::Output)as Unshift>::Output;
[INFO] [stdout]     | |_________________________________________________^ the trait `Substitution` is not implemented for `(T1, _, Z)`
[INFO] [stdout]     |
[INFO] [stdout]     = help: the following other types implement trait `Substitution`:
[INFO] [stdout]               (Abs<E>, T, M)
[INFO] [stdout]               (App<F, L>, T, M)
[INFO] [stdout]               (Var<N>, T, M)
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `App<T1, T11>: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:181:19
[INFO] [stdout]     |
[INFO] [stdout] 181 |     type Output = App<<App<T1, T11> as Beta>::Output, <T2 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `App<T1, T11>`
[INFO] [stdout]     |
[INFO] [stdout] help: consider introducing a `where` clause, but there might be an alternative better way to express this requirement
[INFO] [stdout]     |
[INFO] [stdout] 180 | impl<T1: Term, T11: Term, T2: Term> Beta for App<App<T1,T11>, T2> where App<T1, T11>: Beta {
[INFO] [stdout]     |                                                                   ++++++++++++++++++++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `T2: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:181:19
[INFO] [stdout]     |
[INFO] [stdout] 181 |     type Output = App<<App<T1, T11> as Beta>::Output, <T2 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `T2`
[INFO] [stdout]     |
[INFO] [stdout] help: consider further restricting type parameter `T2` with trait `Beta`
[INFO] [stdout]     |
[INFO] [stdout] 180 | impl<T1: Term, T11: Term, T2: Term + Beta> Beta for App<App<T1,T11>, T2> {
[INFO] [stdout]     |                                    ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `T2: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:185:19
[INFO] [stdout]     |
[INFO] [stdout] 185 |     type Output = App<<Var<T1> as Beta>::Output, <T2 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `T2`
[INFO] [stdout]     |
[INFO] [stdout] help: consider further restricting type parameter `T2` with trait `Beta`
[INFO] [stdout]     |
[INFO] [stdout] 184 | impl<T1: Nat, T2: Term + Beta> Beta for App<Var<T1>, T2> {
[INFO] [stdout]     |                        ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] error[E0277]: the trait bound `T1: Beta` is not satisfied
[INFO] [stdout]    --> src/main.rs:189:19
[INFO] [stdout]     |
[INFO] [stdout] 189 |     type Output = Abs<<T1 as Beta>::Output>;
[INFO] [stdout]     |                   ^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Beta` is not implemented for `T1`
[INFO] [stdout]     |
[INFO] [stdout] help: consider further restricting type parameter `T1` with trait `Beta`
[INFO] [stdout]     |
[INFO] [stdout] 188 | impl<T1: Term + Beta> Beta for Abs<T1> {
[INFO] [stdout]     |               ++++++
[INFO] [stdout] 
[INFO] [stdout] 
[INFO] [stdout] Some errors have detailed explanations: E0275, E0277.
[INFO] [stdout] 
[INFO] [stdout] For more information about an error, try `rustc --explain E0275`.
[INFO] [stdout] 
[INFO] [stderr] error: could not compile `lambdatype` (bin "lambdatype") due to 23 previous errors
[INFO] running `Command { std: "docker" "inspect" "7fe0d0e97b584afe64b83a66d29e57373bcf41ad49de6fc15f0f20b838c0c3bb", kill_on_drop: false }`
[INFO] running `Command { std: "docker" "rm" "-f" "7fe0d0e97b584afe64b83a66d29e57373bcf41ad49de6fc15f0f20b838c0c3bb", kill_on_drop: false }`
[INFO] [stdout] 7fe0d0e97b584afe64b83a66d29e57373bcf41ad49de6fc15f0f20b838c0c3bb