put trace info in .out files

25 files changed, 696 insertions, 4 deletions

diff --git a/testdata/language-features/basic-list/list01.out b/testdata/language-features/basic-list/list01.out
index 6ca83aa0..965841b3 100644
--- a/testdata/language-features/basic-list/list01.out
+++ b/testdata/language-features/basic-list/list01.out
@@ -1,4 +1,8 @@
 main is not found
+------------ trace
+value1 :: {a} -> 'List a
+value2 :: {a} -> {b : 'Num a} -> 'List a
+value3 :: 'List 'Char
 ------------ tooltips
 testdata/language-features/basic-list/list01.lc 1:1-1:7  {a} -> List a
 testdata/language-features/basic-list/list01.lc 1:10-1:12  {a} -> List a
diff --git a/testdata/language-features/basic-list/list02.out b/testdata/language-features/basic-list/list02.out
index 078475d7..5ebde853 100644
--- a/testdata/language-features/basic-list/list02.out
+++ b/testdata/language-features/basic-list/list02.out
@@ -1,4 +1,8 @@
 main is not found
+------------ trace
+value1 :: {a} -> 'List a
+value2 :: {a} -> {b : 'Num a} -> 'List a
+value3 :: 'List 'Char
 ------------ tooltips
 testdata/language-features/basic-list/list02.lc 1:1-1:7  {a} -> List a
 testdata/language-features/basic-list/list02.lc 1:10-2:4  {a} -> List a
diff --git a/testdata/language-features/basic-list/list03.reject.out b/testdata/language-features/basic-list/list03.reject.out
index d5a33d36..f5ad67d8 100644
--- a/testdata/language-features/basic-list/list03.reject.out
+++ b/testdata/language-features/basic-list/list03.reject.out
@@ -1,3 +1,7 @@
 testdata/language-features/basic-list/list03.reject.lc:2:1:
 expecting expression
-wrong indentation
\ No newline at end of file
+wrong indentation
+------------ trace
+!testdata/language-features/basic-list/list03.reject.lc:2:1:
+expecting expression
+wrong indentation
diff --git a/testdata/language-features/basic-list/list04.reject.out b/testdata/language-features/basic-list/list04.reject.out
index 6f169a95..02ee2348 100644
--- a/testdata/language-features/basic-list/list04.reject.out
+++ b/testdata/language-features/basic-list/list04.reject.out
@@ -1,3 +1,7 @@
 testdata/language-features/basic-list/list04.reject.lc:2:1:
 expecting expression
-wrong indentation
\ No newline at end of file
+wrong indentation
+------------ trace
+!testdata/language-features/basic-list/list04.reject.lc:2:1:
+expecting expression
+wrong indentation
diff --git a/testdata/language-features/basic-list/list05.reject.out b/testdata/language-features/basic-list/list05.reject.out
index 821b377d..4a4087cc 100644
--- a/testdata/language-features/basic-list/list05.reject.out
+++ b/testdata/language-features/basic-list/list05.reject.out
@@ -1,4 +1,9 @@
 testdata/language-features/basic-list/list05.reject.lc:2:1:
 unexpected end of input
 expecting expression
-wrong indentation
\ No newline at end of file
+wrong indentation
+------------ trace
+!testdata/language-features/basic-list/list05.reject.lc:2:1:
+unexpected end of input
+expecting expression
+wrong indentation
diff --git a/testdata/language-features/basic-list/list06.reject.out b/testdata/language-features/basic-list/list06.reject.out
index 7bcc0c09..47f8f104 100644
--- a/testdata/language-features/basic-list/list06.reject.out
+++ b/testdata/language-features/basic-list/list06.reject.out
@@ -1,3 +1,7 @@
 testdata/language-features/basic-list/list06.reject.lc:1:10:
 unexpected ','
-expecting expression
\ No newline at end of file
+expecting expression
+------------ trace
+!testdata/language-features/basic-list/list06.reject.lc:1:10:
+unexpected ','
+expecting expression
diff --git a/testdata/language-features/basic-list/list07.reject.out b/testdata/language-features/basic-list/list07.reject.out
index 330be399..7a29dae2 100644
--- a/testdata/language-features/basic-list/list07.reject.out
+++ b/testdata/language-features/basic-list/list07.reject.out
@@ -4,3 +4,162 @@ with
 'Char
 
 in builtin Nil
+
+------------ trace
+infer:  labelend (Cons (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {_ : _:'Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+check:  labEnd (Cons {(_ : _:'Type) :: Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons {(_ : _:'Type) : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons {\(a : _:'Type)->a : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons {\(b : (\a:'Type -> a))->b : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {\(b : (\a:Type -> a))->b : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons {\(b : \a->a)->b : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {\(b : \a->a)->b : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {\a b:a -> b:Type} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {\a b:a -> \(c : Type~a)->b} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {\a b:a a:=Type -> b} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {\a a:=Type -> \b->b} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (Cons {\a->a} (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons {a}) (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (\a->Cons (fromInt 1) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt 1)) (Cons 1.2 (Cons 'a' Nil)))
+check:  labEnd ((\a -> Cons (fromInt 1 :: a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {_ : _:'Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+check:  labEnd ((\a -> Cons (fromInt {(_ : _:'Type) :: Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons (fromInt {(_ : _:'Type) : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons (fromInt {\(b : _:'Type)->b : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons (fromInt {\(c : (\b:'Type -> b))->c : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {\(c : (\b:Type -> b))->c : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons (fromInt {\(c : \b->b)->c : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {\(c : \b->b)->c : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {\b c:b -> c:Type} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {\b c:b -> \(d : Type~b)->c} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {\b c:b b:=Type -> c} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {\b b:=Type -> \c->c} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (fromInt {\b->b} 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt {b}) 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b) 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {_ : _:'Type} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+check:  labEnd ((\a -> Cons ((\b -> fromInt b {(_ : _:'Type) :: 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {(_ : _:'Type) : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {\(c : _:'Type)->c : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : (\c:'Type -> c))->d : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : (\c:Type -> c))->d : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : \c->c)->d : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : \c->c)->d : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> d : 'Num b} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> \(e : 'Num b ~ c)->d} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> \(c := 'Num b)->d} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c (c := 'Num b) -> \(d : 'Num b)->d} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\(c : 'Num b)->c} 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> (\(c : 'Num b) -> fromInt b {c}) 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b -> (\(c : 'Num b) -> fromInt b c) 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+check:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1::'Int) : a)) (Cons 1.2 (Cons 'a' Nil)))
+infer:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1:'Int) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1:'Int) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c (\d:'Unit -> 1)) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (\b (c : 'Num b) -> fromInt b c 1 : a)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (\b (c : 'Num b) (d : a~b) -> fromInt b c 1)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (\b (c : 'Num b) b:=a -> fromInt a c 1)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (\b b:=a (c : 'Num a) -> fromInt a c 1)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a -> Cons (\(b : 'Num a) -> fromInt a b 1)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a (b : 'Num a) -> Cons (fromInt a b 1)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd ((\a (b : 'Num a) -> Cons (fromInt a b 1)) (Cons 1.2 (Cons 'a' Nil)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 (Cons 'a' Nil)))
+check:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 (Cons 'a' Nil) :: 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 (Cons 'a' Nil) : 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {_ : _:'Type} 1.2 (Cons 'a' Nil) : 'List a))
+check:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {(_ : _:'Type) :: Type} 1.2 (Cons 'a' Nil) : 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {(_ : _:'Type) : Type} 1.2 (Cons 'a' Nil) : 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\(c : _:'Type)->c : Type} 1.2 (Cons 'a' Nil) : 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\(d : (\c:'Type -> c))->d : Type} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\(d : (\c:Type -> c))->d : Type} 1.2 (Cons 'a' Nil) : 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\(d : \c->c)->d : Type} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\(d : \c->c)->d : Type} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {(\c d:c -> d) : Type} 1.2 (Cons 'a' Nil) : 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {(\c d:c -> d) : Type} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {(\c d:c -> d) : Type} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\c d:c -> d:Type} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\c d:c -> \(e : Type~c)->d} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\c d:c c:=Type -> d} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\c c:=Type -> \d->d} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons {\c->c} 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c -> Cons {c}) 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\c->Cons 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c -> Cons 1.2) (Cons 'a' Nil) : 'List a))
+check:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c -> Cons 1.2::c) (Cons 'a' Nil) : 'List a))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c -> Cons 1.2:c) (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c -> Cons 1.2:c) (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c -> Cons \(d : c~'Float)->1.2) (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c -> Cons (\c:='Float -> 1.2)) (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c c:='Float -> Cons 1.2) (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\c c:='Float -> Cons 1.2) (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 (Cons 'a' Nil) : 'List a))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\(c : a~'Float) -> Cons 1.2) (Cons 'a' Nil)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) ((\a:='Float -> Cons 1.2) (Cons 'a' Nil)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons 'a' Nil)))
+check:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons 'a' Nil :: 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons 'a' Nil : 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {_ : _:'Type} 'a' Nil : 'List 'Float)))
+check:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {(_ : _:'Type) :: Type} 'a' Nil : 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {(_ : _:'Type) : Type} 'a' Nil : 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\(c : _:'Type)->c : Type} 'a' Nil : 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\(d : (\c:'Type -> c))->d : Type} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\(d : (\c:Type -> c))->d : Type} 'a' Nil : 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\(d : \c->c)->d : Type} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\(d : \c->c)->d : Type} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {(\c d:c -> d) : Type} 'a' Nil : 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {(\c d:c -> d) : Type} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {(\c d:c -> d) : Type} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\c d:c -> d:Type} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\c d:c -> \(e : Type~c)->d} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\c d:c c:=Type -> d} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\c c:=Type -> \d->d} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons {\c->c} 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c -> Cons {c}) 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (\c->Cons 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c -> Cons 'a') Nil : 'List 'Float)))
+check:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c -> Cons 'a'::c) Nil : 'List 'Float)))
+infer:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c -> Cons 'a':c) Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c -> Cons 'a':c) Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c -> Cons \(d : c~'Char)->'a') Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c -> Cons (\c:='Char -> 'a')) Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c c:='Char -> Cons 'a') Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\c c:='Char -> Cons 'a') Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 (Cons 'a' Nil : 'List 'Float)))
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (\a:='Float -> Cons 1.2 ((\(c : 'Empty "can not unify\n\ESC[32m'Float\ESC[m\nwith\n\ESC[32m'Char\ESC[m\n") -> Cons 'a') Nil)))
+!type error: can not unify
+'Float
+with
+'Char
+
+in builtin Nil
+
+------------ tooltips
+testdata/language-features/basic-list/list07.reject.lc 1:10-1:11  V1
+testdata/language-features/basic-list/list07.reject.lc 1:12-1:15  Float
+testdata/language-features/basic-list/list07.reject.lc 1:16-1:19  Char
diff --git a/testdata/language-features/basic-list/list08.out b/testdata/language-features/basic-list/list08.out
index 36f905d9..fb69fb70 100644
--- a/testdata/language-features/basic-list/list08.out
+++ b/testdata/language-features/basic-list/list08.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: 'List 'Float
 ------------ tooltips
 testdata/language-features/basic-list/list08.lc 1:1-1:6  List Float
 testdata/language-features/basic-list/list08.lc 1:9-1:16  List Float
diff --git a/testdata/language-features/basic-list/list09.out b/testdata/language-features/basic-list/list09.out
index a64ddd90..4ac018ac 100644
--- a/testdata/language-features/basic-list/list09.out
+++ b/testdata/language-features/basic-list/list09.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: 'List 'Float
 ------------ tooltips
 testdata/language-features/basic-list/list09.lc 1:1-1:6  List Float
 testdata/language-features/basic-list/list09.lc 1:9-1:16  List Float
diff --git a/testdata/language-features/basic-list/list10.reject.out b/testdata/language-features/basic-list/list10.reject.out
index 8f1376a7..6c108119 100644
--- a/testdata/language-features/basic-list/list10.reject.out
+++ b/testdata/language-features/basic-list/list10.reject.out
@@ -4,3 +4,144 @@ with
 'Float
 
 in builtin Nil
+
+------------ trace
+infer:  labelend (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+check:  labEnd (('List 'Int :: Type) : ??)
+infer:  labEnd (('List 'Int : Type) : ??)
+focus:  labEnd (('List 'Int : Type) : ??)
+focus:  labEnd ((\a:'Unit -> 'List) 'Int : ??)
+focus:  labEnd ('List 'Int : ??)
+check:  labEnd ('List 'Int::Type : ??)
+infer:  labEnd ('List 'Int:Type : ??)
+focus:  labEnd ('List 'Int:Type : ??)
+focus:  labEnd ('List (\a:'Unit -> 'Int) : ??)
+focus:  labEnd ('List 'Int : ??)
+focus:  labEnd ('List 'Int : ??)
+check:  labEnd (Cons (fromInt 1) (Cons 1.2 Nil) :: 'List 'Int)
+infer:  labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {_ : _:'Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+check:  labEnd (Cons {(_ : _:'Type) :: Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd (Cons {(_ : _:'Type) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd (Cons {\(a : _:'Type)->a : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd (Cons {\(b : (\a:'Type -> a))->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {\(b : (\a:Type -> a))->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd (Cons {\(b : \a->a)->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {\(b : \a->a)->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {\a b:a -> b:Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {\a b:a -> \(c : Type~a)->b} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {\a b:a a:=Type -> b} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {\a a:=Type -> \b->b} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (Cons {\a->a} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons {a}) (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (\a->Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt 1)) (Cons 1.2 Nil) : 'List 'Int)
+check:  labEnd ((\a -> Cons (fromInt 1 :: a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {_ : _:'Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+check:  labEnd ((\a -> Cons (fromInt {(_ : _:'Type) :: Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons (fromInt {(_ : _:'Type) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons (fromInt {\(b : _:'Type)->b : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons (fromInt {\(c : (\b:'Type -> b))->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {\(c : (\b:Type -> b))->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons (fromInt {\(c : \b->b)->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {\(c : \b->b)->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {\b c:b -> c:Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {\b c:b -> \(d : Type~b)->c} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {\b c:b b:=Type -> c} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {\b b:=Type -> \c->c} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (fromInt {\b->b} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt {b}) 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b) 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {_ : _:'Type} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+check:  labEnd ((\a -> Cons ((\b -> fromInt b {(_ : _:'Type) :: 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {(_ : _:'Type) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {\(c : _:'Type)->c : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : (\c:'Type -> c))->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : (\c:Type -> c))->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : \c->c)->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\(d : \c->c)->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> \(e : 'Num b ~ c)->d} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> \(c := 'Num b)->d} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\c (c := 'Num b) -> \(d : 'Num b)->d} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> fromInt b {\(c : 'Num b)->c} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> (\(c : 'Num b) -> fromInt b {c}) 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b -> (\(c : 'Num b) -> fromInt b c) 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+check:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1::'Int) : a)) (Cons 1.2 Nil) : 'List 'Int)
+infer:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1:'Int) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1:'Int) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c (\d:'Unit -> 1)) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (\b (c : 'Num b) -> fromInt b c 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (\b (c : 'Num b) (d : a~b) -> fromInt b c 1)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (\b (c : 'Num b) b:=a -> fromInt a c 1)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (\b b:=a (c : 'Num a) -> fromInt a c 1)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a -> Cons (\(b : 'Num a) -> fromInt a b 1)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a (b : 'Num a) -> Cons (fromInt a b 1)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd ((\a (b : 'Num a) -> Cons (fromInt a b 1)) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 Nil) : 'List 'Int)
+focus:  labEnd (\a (b : 'Num a) -> (\(c : 'Int~a) -> Cons (fromInt a b 1)) (Cons 1.2 Nil))
+focus:  labEnd (\a (b : 'Num a) -> (\a:='Int -> Cons 1) (Cons 1.2 Nil))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil))
+check:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil :: 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {_ : _:'Type} 1.2 Nil : 'List 'Int))
+check:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(_ : _:'Type) :: Type} 1.2 Nil : 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(_ : _:'Type) : Type} 1.2 Nil : 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(c : _:'Type)->c : Type} 1.2 Nil : 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : (\c:'Type -> c))->d : Type} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : (\c:Type -> c))->d : Type} 1.2 Nil : 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : \c->c)->d : Type} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : \c->c)->d : Type} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(\c d:c -> d) : Type} 1.2 Nil : 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(\c d:c -> d) : Type} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(\c d:c -> d) : Type} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c d:c -> d:Type} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c d:c -> \(e : Type~c)->d} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c d:c c:=Type -> d} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c c:=Type -> \d->d} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c->c} 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons {c}) 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (\c->Cons 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2) Nil : 'List 'Int))
+check:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2::c) Nil : 'List 'Int))
+infer:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2:c) Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2:c) Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons \(d : c~'Float)->1.2) Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons (\c:='Float -> 1.2)) Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c c:='Float -> Cons 1.2) Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c c:='Float -> Cons 1.2) Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
+focus:  labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\(c : 'Empty "can not unify\n\ESC[32m'Int\ESC[m\nwith\n\ESC[32m'Float\ESC[m\n") -> Cons 1.2) Nil))
+!type error: can not unify
+'Int
+with
+'Float
+
+in builtin Nil
+
+------------ tooltips
+testdata/language-features/basic-list/list10.reject.lc 1:10-1:11  V1
+testdata/language-features/basic-list/list10.reject.lc 1:12-1:15  Float
+testdata/language-features/basic-list/list10.reject.lc 1:20-1:25  Type
+testdata/language-features/basic-list/list10.reject.lc 1:21-1:24  Type
diff --git a/testdata/language-features/basic-list/list11.out b/testdata/language-features/basic-list/list11.out
index a9ddb798..f447dd7c 100644
--- a/testdata/language-features/basic-list/list11.out
+++ b/testdata/language-features/basic-list/list11.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: {a} -> {b : 'Num a} -> 'List a
 ------------ tooltips
 testdata/language-features/basic-list/list11.lc 1:1-1:6  {a} -> {b : Num a} -> List a
 testdata/language-features/basic-list/list11.lc 1:9-1:10  V1
diff --git a/testdata/language-features/basic-list/list12.out b/testdata/language-features/basic-list/list12.out
index 840ebd6a..fb253041 100644
--- a/testdata/language-features/basic-list/list12.out
+++ b/testdata/language-features/basic-list/list12.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: {a} -> {b : 'Num a} -> 'List a
 ------------ tooltips
 testdata/language-features/basic-list/list12.lc 1:1-1:6  {a} -> {b : Num a} -> List a
 testdata/language-features/basic-list/list12.lc 1:9-1:10  V1
diff --git a/testdata/language-features/basic-list/list13.out b/testdata/language-features/basic-list/list13.out
index cc92303b..b3a4a01b 100644
--- a/testdata/language-features/basic-list/list13.out
+++ b/testdata/language-features/basic-list/list13.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: 'List 'Char
 ------------ tooltips
 testdata/language-features/basic-list/list13.lc 1:1-1:6  List Char
 testdata/language-features/basic-list/list13.lc 1:9-1:12  Char
diff --git a/testdata/language-features/basic-list/list14.reject.out b/testdata/language-features/basic-list/list14.reject.out
index befa6180..85d77268 100644
--- a/testdata/language-features/basic-list/list14.reject.out
+++ b/testdata/language-features/basic-list/list14.reject.out
@@ -6,3 +6,89 @@ with
 in testdata/language-features/basic-list/list14.reject.lc:1:17:
 value = 'h':'i':()
                 ^^
+
+------------ trace
+infer:  labelend (Cons 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {_ : _:'Type} 'h' (Cons 'i' Tuple0))
+check:  labEnd (Cons {(_ : _:'Type) :: Type} 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons {(_ : _:'Type) : Type} 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons {\(a : _:'Type)->a : Type} 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons {\(b : (\a:'Type -> a))->b : Type} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {\(b : (\a:Type -> a))->b : Type} 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons {\(b : \a->a)->b : Type} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {\(b : \a->a)->b : Type} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {(\a b:a -> b) : Type} 'h' (Cons 'i' Tuple0))
+infer:  labEnd (Cons {(\a b:a -> b) : Type} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {(\a b:a -> b) : Type} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {\a b:a -> b:Type} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {\a b:a -> \(c : Type~a)->b} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {\a b:a a:=Type -> b} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {\a a:=Type -> \b->b} 'h' (Cons 'i' Tuple0))
+focus:  labEnd (Cons {\a->a} 'h' (Cons 'i' Tuple0))
+focus:  labEnd ((\a -> Cons {a}) 'h' (Cons 'i' Tuple0))
+focus:  labEnd (\a->Cons 'h' (Cons 'i' Tuple0))
+focus:  labEnd ((\a -> Cons 'h') (Cons 'i' Tuple0))
+check:  labEnd ((\a -> Cons 'h'::a) (Cons 'i' Tuple0))
+infer:  labEnd ((\a -> Cons 'h':a) (Cons 'i' Tuple0))
+focus:  labEnd ((\a -> Cons 'h':a) (Cons 'i' Tuple0))
+focus:  labEnd ((\a -> Cons \(b : a~'Char)->'h') (Cons 'i' Tuple0))
+focus:  labEnd ((\a -> Cons (\a:='Char -> 'h')) (Cons 'i' Tuple0))
+focus:  labEnd ((\a a:='Char -> Cons 'h') (Cons 'i' Tuple0))
+focus:  labEnd ((\a a:='Char -> Cons 'h') (Cons 'i' Tuple0))
+focus:  labEnd (Cons 'h' (Cons 'i' Tuple0))
+check:  labEnd (Cons 'h' (Cons 'i' Tuple0 :: 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons 'i' Tuple0 : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {_ : _:'Type} 'i' Tuple0 : 'List 'Char))
+check:  labEnd (Cons 'h' (Cons {(_ : _:'Type) :: Type} 'i' Tuple0 : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {(_ : _:'Type) : Type} 'i' Tuple0 : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {\(a : _:'Type)->a : Type} 'i' Tuple0 : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {\(b : (\a:'Type -> a))->b : Type} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\(b : (\a:Type -> a))->b : Type} 'i' Tuple0 : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {\(b : \a->a)->b : Type} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\(b : \a->a)->b : Type} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {(\a b:a -> b) : Type} 'i' Tuple0 : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {(\a b:a -> b) : Type} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {(\a b:a -> b) : Type} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a b:a -> b:Type} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a b:a -> \(c : Type~a)->b} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a b:a a:=Type -> b} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a a:=Type -> \b->b} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a->a} 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons {a}) 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (\a->Cons 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons 'i') Tuple0 : 'List 'Char))
+check:  labEnd (Cons 'h' ((\a -> Cons 'i'::a) Tuple0 : 'List 'Char))
+infer:  labEnd (Cons 'h' ((\a -> Cons 'i':a) Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons 'i':a) Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons \(b : a~'Char)->'i') Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons (\a:='Char -> 'i')) Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a a:='Char -> Cons 'i') Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a a:='Char -> Cons 'i') Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons 'i' Tuple0 : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a:'Unit -> Cons 'i') Tuple0))
+focus:  labEnd (Cons 'h' (Cons 'i' Tuple0))
+check:  labEnd (Cons 'h' (Cons 'i' (Tuple0 :: 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Tuple0 : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Tuple0 : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' \(a : 'Empty "can not unify\n\ESC[32m'List 'Char\ESC[m\nwith\n\ESC[32m'Tuple0\ESC[m\n")->Tuple0))
+!type error: can not unify
+'List 'Char
+with
+'Tuple0
+
+in testdata/language-features/basic-list/list14.reject.lc:1:17
+
+------------ tooltips
+testdata/language-features/basic-list/list14.reject.lc 1:9-1:12  Char
+testdata/language-features/basic-list/list14.reject.lc 1:9-1:13  List Char -> List Char
+testdata/language-features/basic-list/list14.reject.lc 1:12-1:13  {a} -> a -> List a -> List a
+testdata/language-features/basic-list/list14.reject.lc 1:13-1:16  Char
+testdata/language-features/basic-list/list14.reject.lc 1:13-1:17  List Char -> List Char
+testdata/language-features/basic-list/list14.reject.lc 1:16-1:17  {a} -> a -> List a -> List a
+testdata/language-features/basic-list/list14.reject.lc 1:17-1:19  Tuple0
diff --git a/testdata/language-features/basic-list/list15.reject.out b/testdata/language-features/basic-list/list15.reject.out
index 7491f8e8..518ab256 100644
--- a/testdata/language-features/basic-list/list15.reject.out
+++ b/testdata/language-features/basic-list/list15.reject.out
@@ -6,3 +6,119 @@ with
 in testdata/language-features/basic-list/list15.reject.lc:1:20:
 value = 'h':'i':():[]
                    ^^
+
+------------ trace
+infer:  labelend (Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {_ : _:'Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+check:  labEnd (Cons {(_ : _:'Type) :: Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons {(_ : _:'Type) : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons {\(a : _:'Type)->a : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons {\(b : (\a:'Type -> a))->b : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {\(b : (\a:Type -> a))->b : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons {\(b : \a->a)->b : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {\(b : \a->a)->b : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {(\a b:a -> b) : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd (Cons {(\a b:a -> b) : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {(\a b:a -> b) : Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {\a b:a -> b:Type} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {\a b:a -> \(c : Type~a)->b} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {\a b:a a:=Type -> b} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {\a a:=Type -> \b->b} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons {\a->a} 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd ((\a -> Cons {a}) 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (\a->Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd ((\a -> Cons 'h') (Cons 'i' (Cons Tuple0 Nil)))
+check:  labEnd ((\a -> Cons 'h'::a) (Cons 'i' (Cons Tuple0 Nil)))
+infer:  labEnd ((\a -> Cons 'h':a) (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd ((\a -> Cons 'h':a) (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd ((\a -> Cons \(b : a~'Char)->'h') (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd ((\a -> Cons (\a:='Char -> 'h')) (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd ((\a a:='Char -> Cons 'h') (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd ((\a a:='Char -> Cons 'h') (Cons 'i' (Cons Tuple0 Nil)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+check:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil) :: 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil) : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {_ : _:'Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+check:  labEnd (Cons 'h' (Cons {(_ : _:'Type) :: Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {(_ : _:'Type) : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {\(a : _:'Type)->a : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {\(b : (\a:'Type -> a))->b : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\(b : (\a:Type -> a))->b : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {\(b : \a->a)->b : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\(b : \a->a)->b : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {(\a b:a -> b) : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+infer:  labEnd (Cons 'h' (Cons {(\a b:a -> b) : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {(\a b:a -> b) : Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a b:a -> b:Type} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a b:a -> \(c : Type~a)->b} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a b:a a:=Type -> b} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a a:=Type -> \b->b} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons {\a->a} 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons {a}) 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (\a->Cons 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons 'i') (Cons Tuple0 Nil) : 'List 'Char))
+check:  labEnd (Cons 'h' ((\a -> Cons 'i'::a) (Cons Tuple0 Nil) : 'List 'Char))
+infer:  labEnd (Cons 'h' ((\a -> Cons 'i':a) (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons 'i':a) (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons \(b : a~'Char)->'i') (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a -> Cons (\a:='Char -> 'i')) (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a a:='Char -> Cons 'i') (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a a:='Char -> Cons 'i') (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil) : 'List 'Char))
+focus:  labEnd (Cons 'h' ((\a:'Unit -> Cons 'i') (Cons Tuple0 Nil)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil)))
+check:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil :: 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil : 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {_ : _:'Type} Tuple0 Nil : 'List 'Char)))
+check:  labEnd (Cons 'h' (Cons 'i' (Cons {(_ : _:'Type) :: Type} Tuple0 Nil : 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons {(_ : _:'Type) : Type} Tuple0 Nil : 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons {\(a : _:'Type)->a : Type} Tuple0 Nil : 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons {\(b : (\a:'Type -> a))->b : Type} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {\(b : (\a:Type -> a))->b : Type} Tuple0 Nil : 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons {\(b : \a->a)->b : Type} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {\(b : \a->a)->b : Type} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {(\a b:a -> b) : Type} Tuple0 Nil : 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' (Cons {(\a b:a -> b) : Type} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {(\a b:a -> b) : Type} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {\a b:a -> b:Type} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {\a b:a -> \(c : Type~a)->b} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {\a b:a a:=Type -> b} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {\a a:=Type -> \b->b} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons {\a->a} Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\a -> Cons {a}) Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (\a->Cons Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\a -> Cons Tuple0) Nil : 'List 'Char)))
+check:  labEnd (Cons 'h' (Cons 'i' ((\a -> Cons Tuple0::a) Nil : 'List 'Char)))
+infer:  labEnd (Cons 'h' (Cons 'i' ((\a -> Cons Tuple0:a) Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\a -> Cons Tuple0:a) Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\a -> Cons \(b : a~'Tuple0)->Tuple0) Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\a -> Cons (\a:='Tuple0 -> Tuple0)) Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\a a:='Tuple0 -> Cons Tuple0) Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\a a:='Tuple0 -> Cons Tuple0) Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' (Cons Tuple0 Nil : 'List 'Char)))
+focus:  labEnd (Cons 'h' (Cons 'i' ((\(a : 'Empty "can not unify\n\ESC[32m'Char\ESC[m\nwith\n\ESC[32m'Tuple0\ESC[m\n") -> Cons Tuple0) Nil)))
+!type error: can not unify
+'Char
+with
+'Tuple0
+
+in testdata/language-features/basic-list/list15.reject.lc:1:20
+
+------------ tooltips
+testdata/language-features/basic-list/list15.reject.lc 1:9-1:12  Char
+testdata/language-features/basic-list/list15.reject.lc 1:9-1:13  List Char -> List Char
+testdata/language-features/basic-list/list15.reject.lc 1:12-1:13  {a} -> a -> List a -> List a
+testdata/language-features/basic-list/list15.reject.lc 1:13-1:16  Char
+testdata/language-features/basic-list/list15.reject.lc 1:13-1:17  List Char -> List Char
+testdata/language-features/basic-list/list15.reject.lc 1:16-1:17  {a} -> a -> List a -> List a
+testdata/language-features/basic-list/list15.reject.lc 1:17-1:19  Tuple0
+testdata/language-features/basic-list/list15.reject.lc 1:17-1:20  List Tuple0 -> List Tuple0
+testdata/language-features/basic-list/list15.reject.lc 1:19-1:20  {a} -> a -> List a -> List a
diff --git a/testdata/language-features/basic-list/list16.reject.out b/testdata/language-features/basic-list/list16.reject.out
index 5f26cbf1..6c99607b 100644
--- a/testdata/language-features/basic-list/list16.reject.out
+++ b/testdata/language-features/basic-list/list16.reject.out
@@ -6,3 +6,53 @@ with
 in testdata/language-features/basic-list/list16.reject.lc:1:13:
 value = 'h':'i'
             ^^^
+
+------------ trace
+infer:  labelend (Cons 'h' 'i')
+infer:  labEnd (Cons 'h' 'i')
+infer:  labEnd (Cons 'h' 'i')
+infer:  labEnd (Cons 'h' 'i')
+focus:  labEnd (Cons 'h' 'i')
+focus:  labEnd (Cons {_ : _:'Type} 'h' 'i')
+check:  labEnd (Cons {(_ : _:'Type) :: Type} 'h' 'i')
+infer:  labEnd (Cons {(_ : _:'Type) : Type} 'h' 'i')
+infer:  labEnd (Cons {\(a : _:'Type)->a : Type} 'h' 'i')
+infer:  labEnd (Cons {\(b : (\a:'Type -> a))->b : Type} 'h' 'i')
+focus:  labEnd (Cons {\(b : (\a:Type -> a))->b : Type} 'h' 'i')
+infer:  labEnd (Cons {\(b : \a->a)->b : Type} 'h' 'i')
+focus:  labEnd (Cons {\(b : \a->a)->b : Type} 'h' 'i')
+focus:  labEnd (Cons {(\a b:a -> b) : Type} 'h' 'i')
+infer:  labEnd (Cons {(\a b:a -> b) : Type} 'h' 'i')
+focus:  labEnd (Cons {(\a b:a -> b) : Type} 'h' 'i')
+focus:  labEnd (Cons {\a b:a -> b:Type} 'h' 'i')
+focus:  labEnd (Cons {\a b:a -> \(c : Type~a)->b} 'h' 'i')
+focus:  labEnd (Cons {\a b:a a:=Type -> b} 'h' 'i')
+focus:  labEnd (Cons {\a a:=Type -> \b->b} 'h' 'i')
+focus:  labEnd (Cons {\a->a} 'h' 'i')
+focus:  labEnd ((\a -> Cons {a}) 'h' 'i')
+focus:  labEnd (\a->Cons 'h' 'i')
+focus:  labEnd ((\a -> Cons 'h') 'i')
+check:  labEnd ((\a -> Cons 'h'::a) 'i')
+infer:  labEnd ((\a -> Cons 'h':a) 'i')
+focus:  labEnd ((\a -> Cons 'h':a) 'i')
+focus:  labEnd ((\a -> Cons \(b : a~'Char)->'h') 'i')
+focus:  labEnd ((\a -> Cons (\a:='Char -> 'h')) 'i')
+focus:  labEnd ((\a a:='Char -> Cons 'h') 'i')
+focus:  labEnd ((\a a:='Char -> Cons 'h') 'i')
+focus:  labEnd (Cons 'h' 'i')
+check:  labEnd (Cons 'h' ('i' :: 'List 'Char))
+infer:  labEnd (Cons 'h' ('i' : 'List 'Char))
+focus:  labEnd (Cons 'h' ('i' : 'List 'Char))
+focus:  labEnd (Cons 'h' \(a : 'Empty "can not unify\n\ESC[32m'List 'Char\ESC[m\nwith\n\ESC[32m'Char\ESC[m\n")->'i')
+!type error: can not unify
+'List 'Char
+with
+'Char
+
+in testdata/language-features/basic-list/list16.reject.lc:1:13
+
+------------ tooltips
+testdata/language-features/basic-list/list16.reject.lc 1:9-1:12  Char
+testdata/language-features/basic-list/list16.reject.lc 1:9-1:13  List Char -> List Char
+testdata/language-features/basic-list/list16.reject.lc 1:12-1:13  {a} -> a -> List a -> List a
+testdata/language-features/basic-list/list16.reject.lc 1:13-1:16  Char
diff --git a/testdata/language-features/basic-list/listcomp01.out b/testdata/language-features/basic-list/listcomp01.out
index f9053dd2..e5d0ba2d 100644
--- a/testdata/language-features/basic-list/listcomp01.out
+++ b/testdata/language-features/basic-list/listcomp01.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: 'List 'Tuple0
 ------------ tooltips
 testdata/language-features/basic-list/listcomp01.lc 1:1-1:6  List Tuple0
 testdata/language-features/basic-list/listcomp01.lc 1:9-1:34  List Tuple0
diff --git a/testdata/language-features/basic-list/listcomp02.out b/testdata/language-features/basic-list/listcomp02.out
index 4ade3a2f..a2835375 100644
--- a/testdata/language-features/basic-list/listcomp02.out
+++ b/testdata/language-features/basic-list/listcomp02.out
@@ -1,4 +1,7 @@
 main is not found
+------------ trace
+l :: 'List 'Tuple0
+value :: 'List 'Tuple0
 ------------ tooltips
 testdata/language-features/basic-list/listcomp02.lc 1:1-1:2  List Tuple0
 testdata/language-features/basic-list/listcomp02.lc 1:5-1:18  List Tuple0
diff --git a/testdata/language-features/basic-list/listcomp03.out b/testdata/language-features/basic-list/listcomp03.out
index 001484be..9d31c0b3 100644
--- a/testdata/language-features/basic-list/listcomp03.out
+++ b/testdata/language-features/basic-list/listcomp03.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: 'List 'Tuple0
 ------------ tooltips
 testdata/language-features/basic-list/listcomp03.lc 1:1-1:6  List Tuple0
 testdata/language-features/basic-list/listcomp03.lc 1:9-1:41  List Tuple0
diff --git a/testdata/language-features/basic-list/listcomp04.out b/testdata/language-features/basic-list/listcomp04.out
index ebf9b00a..87bebdaf 100644
--- a/testdata/language-features/basic-list/listcomp04.out
+++ b/testdata/language-features/basic-list/listcomp04.out
@@ -1,4 +1,7 @@
 main is not found
+------------ trace
+l :: 'List 'Tuple0
+value :: 'List 'Tuple0
 ------------ tooltips
 testdata/language-features/basic-list/listcomp04.lc 1:1-1:2  List Tuple0
 testdata/language-features/basic-list/listcomp04.lc 1:5-1:18  List Tuple0
diff --git a/testdata/language-features/basic-list/listcomp05.out b/testdata/language-features/basic-list/listcomp05.out
index c4c03e58..8163ffcc 100644
--- a/testdata/language-features/basic-list/listcomp05.out
+++ b/testdata/language-features/basic-list/listcomp05.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value :: 'List 'Tuple0
 ------------ tooltips
 testdata/language-features/basic-list/listcomp05.lc 1:1-1:6  List Tuple0
 testdata/language-features/basic-list/listcomp05.lc 1:9-1:39  List Tuple0
diff --git a/testdata/language-features/basic-list/listcomp06.out b/testdata/language-features/basic-list/listcomp06.out
index 02b0300a..1231475f 100644
--- a/testdata/language-features/basic-list/listcomp06.out
+++ b/testdata/language-features/basic-list/listcomp06.out
@@ -1,4 +1,7 @@
 main is not found
+------------ trace
+value1 :: 'List 'Tuple0
+value2 :: 'List 'Tuple0
 ------------ tooltips
 testdata/language-features/basic-list/listcomp06.lc 1:1-1:7  List Tuple0
 testdata/language-features/basic-list/listcomp06.lc 1:10-1:46  List Tuple0
diff --git a/testdata/language-features/basic-list/listcomp07.out b/testdata/language-features/basic-list/listcomp07.out
index 9721ad28..f753d50a 100644
--- a/testdata/language-features/basic-list/listcomp07.out
+++ b/testdata/language-features/basic-list/listcomp07.out
@@ -1,4 +1,8 @@
 main is not found
+------------ trace
+value1 :: 'List 'Tuple0
+value2 :: 'List 'Tuple0
+value3 :: 'List 'Tuple0
 ------------ tooltips
 testdata/language-features/basic-list/listcomp07.lc 1:1-1:7  List Tuple0
 testdata/language-features/basic-list/listcomp07.lc 1:10-6:11  List Tuple0
diff --git a/testdata/language-features/basic-list/listcomp08.reject.out b/testdata/language-features/basic-list/listcomp08.reject.out
index 3c21bdc9..8cde0e3b 100644
--- a/testdata/language-features/basic-list/listcomp08.reject.out
+++ b/testdata/language-features/basic-list/listcomp08.reject.out
@@ -6,3 +6,87 @@ with
 in testdata/language-features/basic-list/listcomp08.reject.lc:1:23:
 value = [x | x <- [], "not Bool"]
                       ^^^^^^^^^^
+
+------------ trace
+infer:  labelend (concatMap (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+infer:  labEnd (concatMap (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+infer:  labEnd (concatMap (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+infer:  labEnd (concatMap (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+focus:  labEnd (concatMap (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+focus:  labEnd (concatMap {_ : _:'Type} (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+check:  labEnd (concatMap {(_ : _:'Type) :: Type} (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+infer:  labEnd (concatMap {(_ : _:'Type) : Type} (\(a : _:'Type) -> primIfThenElse "not Bool" (Cons a Nil) Nil) Nil)
+infer:  labEnd (concatMap {\(a : _:'Type)->a : Type} (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil) Nil)
+infer:  labEnd (concatMap {\(b : (\a:'Type -> a))->b : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {\(b : (\a:Type -> a))->b : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+infer:  labEnd (concatMap {\(b : \a->a)->b : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {\(b : \a->a)->b : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {(\a b:a -> b) : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+infer:  labEnd (concatMap {(\a b:a -> b) : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {(\a b:a -> b) : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {\a b:a -> b:Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {\a b:a -> \(c : Type~a)->b} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil) Nil)
+focus:  labEnd (concatMap {\a b:a a:=Type -> b} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {\a a:=Type -> \b->b} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) Nil)
+focus:  labEnd (concatMap {\a->a} (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil) Nil)
+focus:  labEnd ((\a -> concatMap {a}) (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil) Nil)
+focus:  labEnd ((\a -> concatMap a) (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil) Nil)
+focus:  labEnd ((\a -> concatMap a (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {_ : _:'Type} (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil)) Nil)
+check:  labEnd ((\a -> concatMap a {(_ : _:'Type) :: Type} (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil)) Nil)
+infer:  labEnd ((\a -> concatMap a {(_ : _:'Type) : Type} (\(b : _:'Type) -> primIfThenElse "not Bool" (Cons b Nil) Nil)) Nil)
+infer:  labEnd ((\a -> concatMap a {\(b : _:'Type)->b : Type} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil)) Nil)
+infer:  labEnd ((\a -> concatMap a {\(c : (\b:'Type -> b))->c : Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {\(c : (\b:Type -> b))->c : Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+infer:  labEnd ((\a -> concatMap a {\(c : \b->b)->c : Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {\(c : \b->b)->c : Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {(\b c:b -> c) : Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+infer:  labEnd ((\a -> concatMap a {(\b c:b -> c) : Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {(\b c:b -> c) : Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {\b c:b -> c:Type} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {\b c:b -> \(d : Type~b)->c} (\(e : _:'Type) -> primIfThenElse "not Bool" (Cons e Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {\b c:b b:=Type -> c} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {\b b:=Type -> \c->c} (\(d : _:'Type) -> primIfThenElse "not Bool" (Cons d Nil) Nil)) Nil)
+focus:  labEnd ((\a -> concatMap a {\b->b} (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil)) Nil)
+focus:  labEnd ((\a -> (\b -> concatMap a {b}) (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil)) Nil)
+focus:  labEnd ((\a -> (\b -> concatMap a b) (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil)) Nil)
+check:  labEnd ((\a b -> concatMap a b ((\(c : _:'Type) -> primIfThenElse "not Bool" (Cons c Nil) Nil) :: a -> 'List b)) Nil)
+check:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse "not Bool" (Cons c Nil) Nil :: 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {_ : _:'Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+check:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {(_ : _:'Type) :: Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {(_ : _:'Type) : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\(d : _:'Type)->d : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\(e : (\d:'Type -> d))->e : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\(e : (\d:Type -> d))->e : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\(e : \d->d)->e : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\(e : \d->d)->e : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {(\d e:d -> e) : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {(\d e:d -> e) : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {(\d e:d -> e) : Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\d e:d -> e:Type} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\d e:d -> \(f : Type~d)->e} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\d e:d d:=Type -> e} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\d d:=Type -> \e->e} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> primIfThenElse {\d->d} "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> (\d -> primIfThenElse {d}) "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> (\d -> primIfThenElse d) "not Bool" (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> (\d -> primIfThenElse d "not Bool") (Cons c Nil) Nil : 'List b)) Nil)
+check:  labEnd ((\a b -> concatMap a b (\c:a -> (\d -> primIfThenElse d "not Bool"::'Bool) (Cons c Nil) Nil : 'List b)) Nil)
+infer:  labEnd ((\a b -> concatMap a b (\c:a -> (\d -> primIfThenElse d "not Bool":'Bool) (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> (\d -> primIfThenElse d "not Bool":'Bool) (Cons c Nil) Nil : 'List b)) Nil)
+focus:  labEnd ((\a b -> concatMap a b (\c:a -> (\d -> primIfThenElse d \(e : 'Empty "can not unify\n\ESC[32m'Bool\ESC[m\nwith\n\ESC[32m'String\ESC[m\n")->"not Bool") (Cons c Nil) Nil : 'List b)) Nil)
+!type error: can not unify
+'Bool
+with
+'String
+
+in testdata/language-features/basic-list/listcomp08.reject.lc:1:23
+
+------------ tooltips
+testdata/language-features/basic-list/listcomp08.reject.lc 1:10-1:33  V1 -> List V1
+testdata/language-features/basic-list/listcomp08.reject.lc 1:23-1:33  String
diff --git a/testdata/language-features/basic-list/listcomp09.out b/testdata/language-features/basic-list/listcomp09.out
index dfb10524..91ad2305 100644
--- a/testdata/language-features/basic-list/listcomp09.out
+++ b/testdata/language-features/basic-list/listcomp09.out
@@ -1,4 +1,6 @@
 main is not found
+------------ trace
+value1 :: {a} -> 'List 'Tuple0->'String
 ------------ tooltips
 testdata/language-features/basic-list/listcomp09.lc 1:1-1:7  {a} -> List Tuple0->String
 testdata/language-features/basic-list/listcomp09.lc 1:10-1:36  List Tuple0->String