git.iko.soy/Idris-dev
on master help sign in
Update for new unification error messages
45a0addDavid Raymond Christiansen
test/proof002/expected+10−9
compare with master
unifiedsplit
@@ -1,11 +1,12 @@
1−test030a.idr:12:14:When elaborating right hand side of testReflect1:
1+Reflect.idr:207:38:When elaborating right hand side of testReflect1:
2−Can't unify
2+When elaborating an application of function Reflect.getJust:
3− IsJust (Just x)
4−with
5− IsJust (prove (getProof x))
6−
7−Specifically:
8 Can't unify
3 Can't unify
9− Just x
4+ IsJust (Just x)
10 with
5 with
6+ IsJust (prove (getProof x))
7+
8+ Specifically:
9+ Can't unify
10+ Just x
11+ with
11− Nothing
12+ Nothing
test/reg034/expected+18−16
@@ -1,22 +1,24 @@
1reg034.idr:6:5:When elaborating left hand side of bar:
1reg034.idr:6:5:When elaborating left hand side of bar:
2−Can't unify
2+When elaborating an application of function main.bar:
3− length ys = length ys
4−with
5− length xs = length ys
6−
7−Specifically:
8 Can't unify
3 Can't unify
9− length ys
4+ x = x
10 with
5 with
11− length xs
6+ length xs = length ys
7+
8+ Specifically:
9+ Can't unify
10+ length ys
11+ with
12+ length xs
12reg034.idr:9:5:When elaborating left hand side of foo:
13reg034.idr:9:5:When elaborating left hand side of foo:
13−Can't unify
14+When elaborating an application of function main.foo:
14− f y = f y
15−with
16− f x = f y
17−
18−Specifically:
19 Can't unify
15 Can't unify
20− f y
16+ x = x
21 with
17 with
22− f x
18+ f x = f y
19+
20+ Specifically:
21+ Can't unify
22+ f y
23+ with
24+ f x