Fix JIT of matchy calls #582
ice1000Annotations
4 errors
|
LibraryTest.testInMemoryAndPrim():
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L88
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]
|
|
LibraryTest.[1] success:
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L53
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]
|
|
LibraryTest.testLiterate():
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L74
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]
|
|
TestRunner.negative():
cli-impl/src/test/java/org/aya/test/TestRunner.java#L48
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 /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/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:10:7 ->
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
│ ╰──╯
Error: The solution
Vec (+-assoc {zero} {m} {o} i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:10:7 ->
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
│ ╰──╯
Error: Cannot check the expression
refl
of type
(=) {?A A m o ys zs} (?a A m o ys zs) (?a A m o ys zs)
(Normalized: ?a A m o ys zs = ?a A m o ys zs)
against the type
(++) {zero} {A} {m + o} [] ((++) {m} {A} {o} ys zs) = (++) {zero + m} {A}
{o} ((++) {zero} {A} {m} [] ys) zs
In particular, we failed to unify
?A A m o ys zs
with
Vec (+-assoc {zero} {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 (+-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 (+-assoc {suc 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
In particular, we failed to unify
?B A x n m o _ ys zs
with
Vec (+-assoc {suc 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!
9 error(s), 0 warning(s).
Let's learn from that.
>
|