diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected
index 42d196d35..e7738537b 100644
--- a/tests/ideMode/ideMode001/expected
+++ b/tests/ideMode/ideMode001/expected
@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:277} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:278}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:277}_[] ?{_:278}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:279}_[] ?{_:278}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
-0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:268}_[] ?{_:267}_[])")))))) 1)
+0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:258} : (Main.Vect n[0] a[1])) -> (({arg:259} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
diff --git a/tests/ideMode/ideMode003/expected b/tests/ideMode/ideMode003/expected
index 0623bafe6..bc31b0566 100644
--- a/tests/ideMode/ideMode003/expected
+++ b/tests/ideMode/ideMode003/expected
@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:277} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:278}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:277}_[] ?{_:278}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:279}_[] ?{_:278}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
-0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:268}_[] ?{_:267}_[])")))))) 1)
+0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:258} : (Main.Vect n[0] a[1])) -> (({arg:259} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected
index 56407ab79..0ac963019 100644
--- a/tests/idris2/coverage008/expected
+++ b/tests/idris2/coverage008/expected
@@ -1,6 +1,6 @@
 1/1: Building wcov (wcov.idr)
 Main> Main.tfoo is total
 Main> Main.wfoo is total
-Main> Main.wbar is not covering due to call to function Main.with block in 1393
+Main> Main.wbar is not covering due to call to function Main.with block in 1395
 Main> Main.wbar1 is total
 Main> Bye for now!
diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected
index 7d829778c..3162567ff 100644
--- a/tests/idris2/coverage010/expected
+++ b/tests/idris2/coverage010/expected
@@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
 12	main : IO ()
 13	main = do
 
-	Calls non covering function Main.case block in 2145(622)
+	Calls non covering function Main.case block in 2147(630)
diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected
index 9054bd47f..92f0c1a78 100644
--- a/tests/idris2/reflection003/expected
+++ b/tests/idris2/reflection003/expected
@@ -1,6 +1,6 @@
 1/1: Building refprims (refprims.idr)
 LOG 0: Name: Prelude.List.++
-LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6310}) (Prelude.List a) (Prelude.List a))))
+LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6318}) (Prelude.List a) (Prelude.List a))))
 LOG 0: Name: Prelude.Strings.++
 LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String))
 LOG 0: Resolved name: Prelude.Nat