git.iko.soy/Idris-dev
on master help sign in
Update for new unification error messages
commit45a0addf691b2352294c41972b4e233e573c9928 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Mar 2014, 19:58 (13 years ago) parent465d169
2 files changed+28−25
compare with master
unifiedsplit
test/proof002/expected+10−9 test/reg034/expected+18−16
test/proof002/expected+10−9
@@ -1,11 +1,12 @@
1−test030a.idr:12:14:When elaborating right hand side of testReflect1:
2−Can't unify
3− IsJust (Just x)
4−with
5− IsJust (prove (getProof x))
6−
7−Specifically:
1+Reflect.idr:207:38:When elaborating right hand side of testReflect1:
2+When elaborating an application of function Reflect.getJust:
83 Can't unify
9− Just x
4+ IsJust (Just x)
105 with
11− Nothing
6+ IsJust (prove (getProof x))
7+
8+ Specifically:
9+ Can't unify
10+ Just x
11+ with
12+ Nothing
test/reg034/expected+18−16
@@ -1,22 +1,24 @@
11reg034.idr:6:5:When elaborating left hand side of bar:
2−Can't unify
3− length ys = length ys
4−with
5− length xs = length ys
6−
7−Specifically:
2+When elaborating an application of function main.bar:
83 Can't unify
9− length ys
4+ x = x
105 with
11− length xs
6+ length xs = length ys
7+
8+ Specifically:
9+ Can't unify
10+ length ys
11+ with
12+ length xs
1213reg034.idr:9:5:When elaborating left hand side of foo:
13−Can't unify
14− f y = f y
15−with
16− f x = f y
17−
18−Specifically:
14+When elaborating an application of function main.foo:
1915 Can't unify
20− f y
16+ x = x
2117 with
22− f x
18+ f x = f y
19+
20+ Specifically:
21+ Can't unify
22+ f y
23+ with
24+ f x