org.opentest4j.AssertionFailedError: GoalAndMeta.txt ==> expected: <Unsolved:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 ->

  1 │   open import arith::nat::base
  2 │   def test : Nat => _
    │                     ╰╯

Error: Unsolved meta _

1 error(s), 0 warning(s).
Let's learn from that.

Goal:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 ->

  1 │   open import arith::nat::base
  2 │   def test (a : Nat) : Nat => {? a ?}
    │                               ╰─────╯

Goal: Goal of type
        Nat
        (Normalized: Nat)
      Context:
        a : Nat
      You are trying:
        a
      It has type:
        Nat

0 error(s), 0 warning(s).
Let's learn from that.

UnsolvedMetaLit:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->

  3 │   open inductive Option (A : Type)
  4 │     | some A
  5 │   def test => some 114514
    │                    ╰────╯

Error: Unsolved meta A
       in `some 114514`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->

  3 │   open inductive Option (A : Type)
  4 │     | some A
  5 │   def test => some 114514
    │                    ╰────╯

Error: Unable to solve the type of this literal:
         114514
       I'm confused about the following candidates:
         `Nat`, `Nat2`

2 error(s), 0 warning(s).
Let's learn from that.

Daylily:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 ->

  3 │       def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true
  4 │       example def test1 (A B : Type) (x : A) (y : B) =>
  5 │         wow A B x y
    │                 ╰╯  ╰╯ ?B A B x y A >= A
    │                   ╰╯ ?B A B x y B >= B

Info: Solving equation(s) with not very general solution(s)

That looks right!

Norell:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                               ╰╯

Error: Cannot check the expression
         X
       of type
         F (?_ F)
       against the type
         Type 0

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                                              ╰╯

Error: Cannot check the expression
         0
       of type
         Nat
       against the type
         F (?_ F)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                                            ╰─╯

Error: Cannot check the expression
         g 0
       of type
         F (Neg <X>)
         (Normalized: F (<X> → Empty))
       against the type
         Nat

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                  ╰╯

Error: Unsolved meta _
       in `^0 (?_ ^0)`
       in `^0 (?_ ^0) → ^1 (Neg <X>)`

4 error(s), 0 warning(s).
Let's learn from that.

ScopeCheck:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->

  3 │   
  4 │   // https://cstheory.stackexchange.com/a/49160/50892
  5 │   def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
    │                 ╰╯

Error: The solution
         B
       is not well-scoped
       Only the variables below are allowed: 

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 ->

  3 │     
  4 │     // https://cstheory.stackexchange.com/a/49160/50892
  5 │     def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
    │                                              ╰╯
    │                                              ╰╯ ?_ <= ?A a B b

Error: Equations do not have solutions!

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->

  3 │   
  4 │   // https://cstheory.stackexchange.com/a/49160/50892
  5 │   def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
    │                 ╰╯

Error: Unsolved meta _

3 error(s), 0 warning(s).
Let's learn from that.

LiteralAmbiguous3:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 ->

  4 │   
  5 │   def good : List Unit => [ ]
  6 │   def bad => [ unit ]
    │       ╰─╯

Error: Unsolved meta _
       in `?_`
       in `[unit]`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 ->

  4 │   
  5 │   def good : List Unit => [ ]
  6 │   def bad => [ unit ]
    │              ╰──────╯

Error: Unable to solve the type of this literal:
         [unit]
       I'm confused about the following candidates:
         `List`, `List2`

2 error(s), 0 warning(s).
Let's learn from that.

NonPattern:
In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 ->

  3 │   open inductive Vec (n : Nat) (A : Type) elim n
  4 │   | 0 => []
  5 │   | suc n => infixr :> A (Vec n A)
    │         ╰╯

Warning: The name `n` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 ->

  6 │       def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
  7 │         => Path (fn i => Vec (+-assoc i) A)
  8 │         (xs ++ (ys ++ zs))
    │          ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o,
                                ?a n A m o xs ys zs 0 >= n
  9 │         ((xs ++ ys) ++ zs)
    │          ╰──────────────╯
    │          ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m,
                                ?c n A m o xs ys zs 1 >= o

Info: Solving equation(s) with not very general solution(s)

That looks right!

UtensilFullFile:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 ->

  7 │       def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
  8 │       : Path (fn i ⇒ Vec (+-assoc i) A)
  9 │         (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
    │          ╰──────────────╯    ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c
                                                    n A m o xs ys zs 0 >= o, ?a n A
                                                    m o xs ys zs 0 >= n
    │                             ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n
                                                   A m o xs ys zs 1 >= m, ?c n A
                                                   m o xs ys zs 1 >= o

Info: Solving equation(s) with not very general solution(s)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
        ys zs} i) (?A A x n m o _ ys zs)
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                            ╰─────────────╯

Error: Cannot check the expression
         ++-assoc' _ _ _
       of type
         (++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs +
        ?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A
        A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
        n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A
        A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A
        A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
        n m o _ ys zs)) (?_ A x n m o _ ys zs)
       against the type
         ?a A x n m o _ ys zs = ?b A x n m o _ ys zs
       In particular, we failed to unify
         ?A A x n m o _ ys zs
       with
         Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
        ys zs} i) (?A A x n m o _ ys zs)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (suc (+-assoc {n} {m} {o} i)) A
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │               ╰───────────────────────────╯

Error: Cannot check the expression
         pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
       of type
         (=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
        o _ ys zs)
         (Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs))
       against the type
         (++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n +
        m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs
         (Normalized: (x :> (++) {n} {A} {m + o} _ ((++) {m} {A} {o} ys zs)) = (x :>
        (++) {n + m} {A} {o} ((++) {n} {A} {m} _ ys) zs))
       In particular, we failed to unify
         ?B A x n m o _ ys zs
       with
         Vec (+-assoc {suc n} {m} {o} i) A
         (Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _)
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _)
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │         (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │       | [] ⇒ refl
  11 │       | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                         ╰──╯
     │                         ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m
                                    o _ ys zs _)) (?A A x n m o _ ys zs _)
     │                           ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys
                                    zs _) (?A A x n m o _ ys zs _)

Error: Equations do not have solutions!

7 error(s), 0 warning(s).
Let's learn from that.

> but was: <Unsolved:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 ->

  1 │   open import arith::nat::base
  2 │   def test : Nat => _
    │                     ╰╯

Error: Unsolved meta _

1 error(s), 0 warning(s).
Let's learn from that.

Goal:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 ->

  1 │   open import arith::nat::base
  2 │   def test (a : Nat) : Nat => {? a ?}
    │                               ╰─────╯

Goal: Goal of type
        Nat
        (Normalized: Nat)
      Context:
        a : Nat
      You are trying:
        a
      It has type:
        Nat

0 error(s), 0 warning(s).
Let's learn from that.

UnsolvedMetaLit:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->

  3 │   open inductive Option (A : Type)
  4 │     | some A
  5 │   def test => some 114514
    │                    ╰────╯

Error: Unsolved meta A
       in `some 114514`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->

  3 │   open inductive Option (A : Type)
  4 │     | some A
  5 │   def test => some 114514
    │                    ╰────╯

Error: Unable to solve the type of this literal:
         114514
       I'm confused about the following candidates:
         `Nat`, `Nat2`

2 error(s), 0 warning(s).
Let's learn from that.

Daylily:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 ->

  3 │       def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true
  4 │       example def test1 (A B : Type) (x : A) (y : B) =>
  5 │         wow A B x y
    │                 ╰╯  ╰╯ ?B A B x y A >= A
    │                   ╰╯ ?B A B x y B >= B

Info: Solving equation(s) with not very general solution(s)

That looks right!

Norell:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                               ╰╯

Error: Cannot check the expression
         X
       of type
         F (?_ F)
       against the type
         Type 0

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                                              ╰╯

Error: Cannot check the expression
         0
       of type
         Nat
       against the type
         F (?_ F)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                                            ╰─╯

Error: Cannot check the expression
         g 0
       of type
         F (Neg <X>)
         (Normalized: F (<X> → Empty))
       against the type
         Nat

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 ->

  5 │   def test
  6 │    (F : Type -> Type)
  7 │    (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
    │                  ╰╯

Error: Unsolved meta _
       in `^0 (?_ ^0)`
       in `^0 (?_ ^0) → ^1 (Neg <X>)`

4 error(s), 0 warning(s).
Let's learn from that.

ScopeCheck:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->

  3 │   
  4 │   // https://cstheory.stackexchange.com/a/49160/50892
  5 │   def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
    │                 ╰╯

Error: The solution
         B
       is not well-scoped
       Only the variables below are allowed: 

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 ->

  3 │     
  4 │     // https://cstheory.stackexchange.com/a/49160/50892
  5 │     def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
    │                                              ╰╯
    │                                              ╰╯ ?_ <= ?A a B b

Error: Equations do not have solutions!

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->

  3 │   
  4 │   // https://cstheory.stackexchange.com/a/49160/50892
  5 │   def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
    │                 ╰╯

Error: Unsolved meta _

3 error(s), 0 warning(s).
Let's learn from that.

LiteralAmbiguous3:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 ->

  4 │   
  5 │   def good : List Unit => [ ]
  6 │   def bad => [ unit ]
    │       ╰─╯

Error: Unsolved meta _
       in `?_`
       in `[unit]`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 ->

  4 │   
  5 │   def good : List Unit => [ ]
  6 │   def bad => [ unit ]
    │              ╰──────╯

Error: Unable to solve the type of this literal:
         [unit]
       I'm confused about the following candidates:
         `List`, `List2`

2 error(s), 0 warning(s).
Let's learn from that.

NonPattern:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/data/vec/base.aya:5:6 ->

  3 │   open inductive Vec (n : Nat) (A : Type) elim n
  4 │   | 0 => []
  5 │   | suc n => infixr :> A (Vec n A)
    │         ╰╯

Warning: The name `n` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 ->

  6 │       def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
  7 │         => Path (fn i => Vec (+-assoc i) A)
  8 │         (xs ++ (ys ++ zs))
    │          ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o,
                                ?a n A m o xs ys zs 0 >= n
  9 │         ((xs ++ ys) ++ zs)
    │          ╰──────────────╯
    │          ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m,
                                ?c n A m o xs ys zs 1 >= o

Info: Solving equation(s) with not very general solution(s)

That looks right!

UtensilFullFile:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 ->

  7 │       def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
  8 │       : Path (fn i ⇒ Vec (+-assoc i) A)
  9 │         (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
    │          ╰──────────────╯    ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c
                                                    n A m o xs ys zs 0 >= o, ?a n A
                                                    m o xs ys zs 0 >= n
    │                             ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n
                                                   A m o xs ys zs 1 >= m, ?c n A
                                                   m o xs ys zs 1 >= o

Info: Solving equation(s) with not very general solution(s)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
        ys zs} i) (?A A x n m o _ ys zs)
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                            ╰─────────────╯

Error: Cannot check the expression
         ++-assoc' _ _ _
       of type
         (++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs +
        ?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A
        A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
        n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A
        A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A
        A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
        n m o _ ys zs)) (?_ A x n m o _ ys zs)
       against the type
         ?a A x n m o _ ys zs = ?b A x n m o _ ys zs
       In particular, we failed to unify
         ?A A x n m o _ ys zs
       with
         Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
        ys zs} i) (?A A x n m o _ ys zs)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (suc (+-assoc {n} {m} {o} i)) A
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │               ╰───────────────────────────╯

Error: Cannot check the expression
         pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
       of type
         (=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
        o _ ys zs)
         (Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs))
       against the type
         (++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n +
        m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs
         (Normalized: (x :> (++) {n} {A} {m + o} _ ((++) {m} {A} {o} ys zs)) = (x :>
        (++) {n + m} {A} {o} ((++) {n} {A} {m} _ ys) zs))
       In particular, we failed to unify
         ?B A x n m o _ ys zs
       with
         Vec (+-assoc {suc n} {m} {o} i) A
         (Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A)

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _)
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │     (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │   | [] ⇒ refl
  11 │   | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                     ╰──╯

Error: The solution
         Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _)
       is not well-scoped
       Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
       `zs`

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->

  9  │         (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
  10 │       | [] ⇒ refl
  11 │       | x :> _ => pmap (x :>) (++-assoc' _ _ _)
     │                         ╰──╯
     │                         ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m
                                    o _ ys zs _)) (?A A x n m o _ ys zs _)
     │                           ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys
                                    zs _) (?A A x n m o _ ys zs _)

Error: Equations do not have solutions!

7 error(s), 0 warning(s).
Let's learn from that.

>
	at app//org.junit.jupiter.api.AssertionFailureBuilder.build(AssertionFailureBuilder.java:151)
	at app//org.junit.jupiter.api.AssertionFailureBuilder.buildAndThrow(AssertionFailureBuilder.java:132)
	at app//org.junit.jupiter.api.AssertEquals.failNotEqual(AssertEquals.java:197)
	at app//org.junit.jupiter.api.AssertEquals.assertEquals(AssertEquals.java:182)
	at app//org.junit.jupiter.api.Assertions.assertEquals(Assertions.java:1156)
	at app//org.aya.test.TestRunner.checkOutput(TestRunner.java:76)
	at app//org.aya.test.TestRunner.expectFixture(TestRunner.java:88)
	at app//kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
	at app//kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:460)
	at app//kala.collection.base.Traversable.forEachChecked(Traversable.java:976)
	at app//org.aya.test.TestRunner.negative(TestRunner.java:48)
	at [email protected]/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at [email protected]/java.lang.reflect.Method.invoke(Method.java:580)
	at app//org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
	at app//org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
	at [email protected]/java.util.ArrayList.forEach(ArrayList.java:1597)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
	at [email protected]/java.util.ArrayList.forEach(ArrayList.java:1597)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
	at app//org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:124)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:99)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:94)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:63)
	at [email protected]/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at [email protected]/java.lang.reflect.Method.invoke(Method.java:580)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:92)
	at jdk.proxy2/jdk.proxy2.$Proxy6.stop(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:200)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:132)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:103)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:63)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:121)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)