Unify Signature with AbstractTele.Locns #275
HoshinoTentedAnnotations
4 errors
|
PatternTyckTest.test1():
base/src/test/java/org/aya/tyck/PatternTyckTest.java#L26
java.lang.AssertionError: Failed with `class org.aya.normalize.error.UnsolvedMeta`: In file <baka>:11:2 ->
9 |
10 | def threeTimesAhThreeTimes (A : Type) (a : A) : Vec 3 A =>
11 | a vcons a vcons a vcons vnil
| ^^
Error: Unsolved meta n
in `(vcons) {S (S 0)} {^1} ^0 ((vcons) {S 0} {^1} ^0 ((vcons) {0} {^1} ^0
(vnil {^1})))`
at (279-279) [11,2-11,2]
|
|
TyckTest.classTyck():
base/src/test/java/org/aya/tyck/TyckTest.java#L151
java.lang.AssertionError: carrier
|
|
TyckTest.sort():
base/src/test/java/org/aya/tyck/TyckTest.java#L170
java.lang.AssertionError: Failed with `class org.aya.tyck.error.UnifyError$Type`: In file <baka>:22:60 ->
20 | def rbTreeToList (rb : RBTree A) (r : List A) : List A elim rb
21 | | rbLeaf => r
22 | | rbNode x t1 a t2 => rbTreeToList t1 (a :> rbTreeToList t2 r)
| ^^
Error: Cannot check the expression
r
of type
List A
against the type
List B
In particular, we failed to unify
A
with
B
at (507-507) [22,60-22,60]
|
|
TyckTest.elimResolve():
base/src/test/java/org/aya/tyck/TyckTest.java#L139
java.lang.AssertionError: Failed with `class org.aya.normalize.error.UnsolvedMeta`: In file <baka>:5:10 ->
3 | variable a b : Nat
4 | def plus : Phantom a b Nat elim a
5 | | O => mk b
| ^^
Error: Unsolved meta _3
in `mk {O} {^0} {Nat} ^0`
at (143-143) [5,10-5,10]
|