simplify label handling (some test may be slower because of a TODO)

4 files changed, 66 insertions, 66 deletions

diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index f43295c7..564b4060 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -528,11 +528,11 @@ testdata/Builtins.lc 95:15-95:16  Type
 testdata/Builtins.lc 96:3-96:10  {a} -> {b : Component a}->a
 testdata/Builtins.lc 96:14-96:15  Type
 testdata/Builtins.lc 98:20-98:23  Type
-testdata/Builtins.lc 98:20-99:22  {a : Component V0}->V1 -> {c : Component V1}->V2
-testdata/Builtins.lc 98:20-100:21  {a : Component V0}->V1 -> {c : Component V1}->V2
+testdata/Builtins.lc 98:20-99:22  V1->V2
+testdata/Builtins.lc 98:20-100:21  V1->V2
 testdata/Builtins.lc 98:20-116:24  Type | Type->Type
-testdata/Builtins.lc 98:20-126:40  {a : Component V0}->V1 | {a} -> {b : Component a}->a
-testdata/Builtins.lc 98:20-127:35  {a : Component V0}->V1 | {a} -> {b : Component a}->a
+testdata/Builtins.lc 98:20-126:40  V1 | {a : Component V0}->V1 | {a} -> {b : Component a}->a
+testdata/Builtins.lc 98:20-127:35  V1 | {a : Component V0}->V1 | {a} -> {b : Component a}->a
 testdata/Builtins.lc 99:14-99:15  V1
 testdata/Builtins.lc 99:14-99:22  Int
 testdata/Builtins.lc 99:19-99:22  Type
@@ -540,11 +540,11 @@ testdata/Builtins.lc 100:13-100:14  V1
 testdata/Builtins.lc 100:13-100:21  Int
 testdata/Builtins.lc 100:18-100:21  Type
 testdata/Builtins.lc 101:20-101:24  Type
-testdata/Builtins.lc 101:20-102:23  {a : Component V0}->V1 -> {c : Component V1}->V2
-testdata/Builtins.lc 101:20-103:22  {a : Component V0}->V1 -> {c : Component V1}->V2
+testdata/Builtins.lc 101:20-102:23  V1->V2
+testdata/Builtins.lc 101:20-103:22  V1->V2
 testdata/Builtins.lc 101:20-116:24  Type
-testdata/Builtins.lc 101:20-126:40  {a : Component V0}->V1
-testdata/Builtins.lc 101:20-127:35  {a : Component V0}->V1
+testdata/Builtins.lc 101:20-126:40  V1
+testdata/Builtins.lc 101:20-127:35  V1
 testdata/Builtins.lc 102:14-102:15  V1
 testdata/Builtins.lc 102:14-102:23  Word
 testdata/Builtins.lc 102:19-102:23  Type
@@ -552,36 +552,36 @@ testdata/Builtins.lc 103:13-103:14  V1
 testdata/Builtins.lc 103:13-103:22  Word
 testdata/Builtins.lc 103:18-103:22  Type
 testdata/Builtins.lc 104:20-104:25  Type
-testdata/Builtins.lc 104:20-105:17  {a : Component V0}->V1 -> {c : Component V1}->V2
-testdata/Builtins.lc 104:20-106:16  {a : Component V0}->V1 -> {c : Component V1}->V2
+testdata/Builtins.lc 104:20-105:17  V1->V2
+testdata/Builtins.lc 104:20-106:16  V1->V2
 testdata/Builtins.lc 104:20-116:24  Type
-testdata/Builtins.lc 104:20-126:40  {a : Component V0}->V1
-testdata/Builtins.lc 104:20-127:35  {a : Component V0}->V1
+testdata/Builtins.lc 104:20-126:40  V1
+testdata/Builtins.lc 104:20-127:35  V1
 testdata/Builtins.lc 105:14-105:17  Float
 testdata/Builtins.lc 106:13-106:16  Float
 testdata/Builtins.lc 107:26-107:31  Type
 testdata/Builtins.lc 107:26-116:24  Type
-testdata/Builtins.lc 107:26-126:40  {a : Component V0}->V1 -> {c : Component V1}->V2
-testdata/Builtins.lc 107:26-127:35  {a : Component V0}->V1 -> {c : Component V1}->V2
+testdata/Builtins.lc 107:26-126:40  V1->V2
+testdata/Builtins.lc 107:26-127:35  V1->V2
 testdata/Builtins.lc 108:14-108:16  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 108:14-108:20  Float -> VecS Float 2
 testdata/Builtins.lc 108:14-108:24  VecS Float 2
-testdata/Builtins.lc 108:14-114:32  a:Nat -> {b : Component (VecS Float ('Succ ('Succ a)))} -> VecS Float ('Succ ('Succ a)) | a:Nat -> {b : Component (VecS Float ('Succ a))} -> VecS Float ('Succ a)
-testdata/Builtins.lc 108:14-126:40  a:Nat -> {b : Component (VecS V1 a)} -> VecS V2 a | a:Type -> b:Nat -> {c : Component (VecS a b)} -> VecS a b | {a : Component (VecS V1 V0)} -> VecS V2 V1
+testdata/Builtins.lc 108:14-114:32  a:Nat -> VecS Float ('Succ ('Succ a)) | a:Nat -> VecS Float ('Succ a)
+testdata/Builtins.lc 108:14-126:40  VecS V1 V0 | a:Nat -> VecS V1 a | a:Type -> b:Nat -> VecS a b
 testdata/Builtins.lc 108:17-108:20  Float
 testdata/Builtins.lc 108:21-108:24  Float
 testdata/Builtins.lc 109:13-109:15  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 109:13-109:19  Float -> VecS Float 2
 testdata/Builtins.lc 109:13-109:23  VecS Float 2
-testdata/Builtins.lc 109:13-115:31  a:Nat -> {b : Component (VecS Float ('Succ ('Succ a)))} -> VecS Float ('Succ ('Succ a)) | a:Nat -> {b : Component (VecS Float ('Succ a))} -> VecS Float ('Succ a)
-testdata/Builtins.lc 109:13-127:35  a:Nat -> {b : Component (VecS V1 a)} -> VecS V2 a | a:Type -> b:Nat -> {c : Component (VecS a b)} -> VecS a b | {a : Component (VecS V1 V0)} -> VecS V2 V1
+testdata/Builtins.lc 109:13-115:31  a:Nat -> VecS Float ('Succ ('Succ a)) | a:Nat -> VecS Float ('Succ a)
+testdata/Builtins.lc 109:13-127:35  VecS V1 V0 | a:Nat -> VecS V1 a | a:Type -> b:Nat -> VecS a b
 testdata/Builtins.lc 109:16-109:19  Float
 testdata/Builtins.lc 109:20-109:23  Float
 testdata/Builtins.lc 111:14-111:16  {a} -> a -> a -> a -> VecS a 3
 testdata/Builtins.lc 111:14-111:20  Float -> Float -> VecS Float 3
 testdata/Builtins.lc 111:14-111:24  Float -> VecS Float 3
 testdata/Builtins.lc 111:14-111:28  VecS Float 3
-testdata/Builtins.lc 111:14-114:32  a:Nat -> {b : Component (VecS Float ('Succ ('Succ ('Succ a))))} -> VecS Float ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 111:14-114:32  a:Nat -> VecS Float ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 111:17-111:20  Float
 testdata/Builtins.lc 111:21-111:24  Float
 testdata/Builtins.lc 111:25-111:28  Float
@@ -589,7 +589,7 @@ testdata/Builtins.lc 112:13-112:15  {a} -> a -> a -> a -> VecS a 3
 testdata/Builtins.lc 112:13-112:19  Float -> Float -> VecS Float 3
 testdata/Builtins.lc 112:13-112:23  Float -> VecS Float 3
 testdata/Builtins.lc 112:13-112:27  VecS Float 3
-testdata/Builtins.lc 112:13-115:31  a:Nat -> {b : Component (VecS Float ('Succ ('Succ ('Succ a))))} -> VecS Float ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 112:13-115:31  a:Nat -> VecS Float ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 112:16-112:19  Float
 testdata/Builtins.lc 112:20-112:23  Float
 testdata/Builtins.lc 112:24-112:27  Float
@@ -597,7 +597,7 @@ testdata/Builtins.lc 114:14-114:16  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 114:14-114:20  Float -> Float -> Float -> VecS Float 4
 testdata/Builtins.lc 114:14-114:24  Float -> Float -> VecS Float 4
 testdata/Builtins.lc 114:14-114:28  Float -> VecS Float 4
-testdata/Builtins.lc 114:14-114:32  VecS Float 4 | a:Nat -> {b : Component (VecS Float ('Succ ('Succ ('Succ ('Succ a)))))} -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 114:14-114:32  VecS Float 4 | a:Nat -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
 testdata/Builtins.lc 114:17-114:20  Float
 testdata/Builtins.lc 114:21-114:24  Float
 testdata/Builtins.lc 114:25-114:28  Float
@@ -606,33 +606,33 @@ testdata/Builtins.lc 115:13-115:15  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 115:13-115:19  Float -> Float -> Float -> VecS Float 4
 testdata/Builtins.lc 115:13-115:23  Float -> Float -> VecS Float 4
 testdata/Builtins.lc 115:13-115:27  Float -> VecS Float 4
-testdata/Builtins.lc 115:13-115:31  VecS Float 4 | a:Nat -> {b : Component (VecS Float ('Succ ('Succ ('Succ ('Succ a)))))} -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 115:13-115:31  VecS Float 4 | a:Nat -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
 testdata/Builtins.lc 115:16-115:19  Float
 testdata/Builtins.lc 115:20-115:23  Float
 testdata/Builtins.lc 115:24-115:27  Float
 testdata/Builtins.lc 115:28-115:31  Float
 testdata/Builtins.lc 116:20-116:24  Type
-testdata/Builtins.lc 116:20-117:19  {a : Component V0}->V1 -> {c : Component V1}->V2
-testdata/Builtins.lc 116:20-118:17  {a : Component V0}->V1 -> {c : Component V1}->V2
+testdata/Builtins.lc 116:20-117:19  V1->V2
+testdata/Builtins.lc 116:20-118:17  V1->V2
 testdata/Builtins.lc 117:14-117:19  Bool
 testdata/Builtins.lc 118:13-118:17  Bool
 testdata/Builtins.lc 120:14-120:16  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 120:14-120:22  Bool -> VecS Bool 2
 testdata/Builtins.lc 120:14-120:28  VecS Bool 2
-testdata/Builtins.lc 120:14-126:40  a:Nat -> {b : Component (VecS Bool ('Succ ('Succ a)))} -> VecS Bool ('Succ ('Succ a)) | a:Nat -> {b : Component (VecS Bool ('Succ a))} -> VecS Bool ('Succ a)
+testdata/Builtins.lc 120:14-126:40  a:Nat -> VecS Bool ('Succ ('Succ a)) | a:Nat -> VecS Bool ('Succ a)
 testdata/Builtins.lc 120:17-120:22  Bool
 testdata/Builtins.lc 120:23-120:28  Bool
 testdata/Builtins.lc 121:13-121:15  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 121:13-121:20  Bool -> VecS Bool 2
 testdata/Builtins.lc 121:13-121:25  VecS Bool 2
-testdata/Builtins.lc 121:13-127:35  a:Nat -> {b : Component (VecS Bool ('Succ ('Succ a)))} -> VecS Bool ('Succ ('Succ a)) | a:Nat -> {b : Component (VecS Bool ('Succ a))} -> VecS Bool ('Succ a)
+testdata/Builtins.lc 121:13-127:35  a:Nat -> VecS Bool ('Succ ('Succ a)) | a:Nat -> VecS Bool ('Succ a)
 testdata/Builtins.lc 121:16-121:20  Bool
 testdata/Builtins.lc 121:21-121:25  Bool
 testdata/Builtins.lc 123:14-123:16  {a} -> a -> a -> a -> VecS a 3
 testdata/Builtins.lc 123:14-123:22  Bool -> Bool -> VecS Bool 3
 testdata/Builtins.lc 123:14-123:28  Bool -> VecS Bool 3
 testdata/Builtins.lc 123:14-123:34  VecS Bool 3
-testdata/Builtins.lc 123:14-126:40  a:Nat -> {b : Component (VecS Bool ('Succ ('Succ ('Succ a))))} -> VecS Bool ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 123:14-126:40  a:Nat -> VecS Bool ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 123:17-123:22  Bool
 testdata/Builtins.lc 123:23-123:28  Bool
 testdata/Builtins.lc 123:29-123:34  Bool
@@ -640,7 +640,7 @@ testdata/Builtins.lc 124:13-124:15  {a} -> a -> a -> a -> VecS a 3
 testdata/Builtins.lc 124:13-124:20  Bool -> Bool -> VecS Bool 3
 testdata/Builtins.lc 124:13-124:25  Bool -> VecS Bool 3
 testdata/Builtins.lc 124:13-124:30  VecS Bool 3
-testdata/Builtins.lc 124:13-127:35  a:Nat -> {b : Component (VecS Bool ('Succ ('Succ ('Succ a))))} -> VecS Bool ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 124:13-127:35  a:Nat -> VecS Bool ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 124:16-124:20  Bool
 testdata/Builtins.lc 124:21-124:25  Bool
 testdata/Builtins.lc 124:26-124:30  Bool
@@ -648,7 +648,7 @@ testdata/Builtins.lc 126:14-126:16  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 126:14-126:22  Bool -> Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 126:14-126:28  Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 126:14-126:34  Bool -> VecS Bool 4
-testdata/Builtins.lc 126:14-126:40  VecS Bool 4 | a:Nat -> {b : Component (VecS Bool ('Succ ('Succ ('Succ ('Succ a)))))} -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 126:14-126:40  VecS Bool 4 | a:Nat -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
 testdata/Builtins.lc 126:17-126:22  Bool
 testdata/Builtins.lc 126:23-126:28  Bool
 testdata/Builtins.lc 126:29-126:34  Bool
@@ -657,7 +657,7 @@ testdata/Builtins.lc 127:13-127:15  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 127:13-127:20  Bool -> Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 127:13-127:25  Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 127:13-127:30  Bool -> VecS Bool 4
-testdata/Builtins.lc 127:13-127:35  VecS Bool 4 | a:Nat -> {b : Component (VecS Bool ('Succ ('Succ ('Succ ('Succ a)))))} -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 127:13-127:35  VecS Bool 4 | a:Nat -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
 testdata/Builtins.lc 127:16-127:20  Bool
 testdata/Builtins.lc 127:21-127:25  Bool
 testdata/Builtins.lc 127:26-127:30  Bool
diff --git a/testdata/Internals.out b/testdata/Internals.out
index 23c7121b..aa562d54 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -262,46 +262,46 @@ testdata/Internals.lc 105:13-105:14  Type
 testdata/Internals.lc 105:13-105:19  Type
 testdata/Internals.lc 105:18-105:19  Type
 testdata/Internals.lc 107:14-107:17  Type
-testdata/Internals.lc 107:14-108:20  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
-testdata/Internals.lc 107:14-109:27  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
-testdata/Internals.lc 107:14-110:26  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
+testdata/Internals.lc 107:14-108:20  Int->V2 -> Int->V3
+testdata/Internals.lc 107:14-109:27  (V1 -> V2->Ordering) -> V2 -> V3->Ordering
+testdata/Internals.lc 107:14-110:26  V1->V2 -> V2->V3
 testdata/Internals.lc 107:14-119:17  Type | Type->Type
-testdata/Internals.lc 107:14-120:25  {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a
-testdata/Internals.lc 107:14-121:22  {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering
-testdata/Internals.lc 107:14-122:22  {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a
+testdata/Internals.lc 107:14-120:25  Int->V2 | {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a
+testdata/Internals.lc 107:14-121:22  V1 -> V2->Ordering | {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering
+testdata/Internals.lc 107:14-122:22  V1->V2 | {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a
 testdata/Internals.lc 108:13-108:20  Int->Int
 testdata/Internals.lc 108:19-108:20  Int
 testdata/Internals.lc 109:13-109:27  Int -> Int->Ordering
 testdata/Internals.lc 110:13-110:26  Int->Int
 testdata/Internals.lc 111:14-111:18  Type
-testdata/Internals.lc 111:14-112:26  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
-testdata/Internals.lc 111:14-113:28  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
-testdata/Internals.lc 111:14-114:27  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
+testdata/Internals.lc 111:14-112:26  Int->V2 -> Int->V3
+testdata/Internals.lc 111:14-113:28  (V1 -> V2->Ordering) -> V2 -> V3->Ordering
+testdata/Internals.lc 111:14-114:27  V1->V2 -> V2->V3
 testdata/Internals.lc 111:14-119:17  Type
-testdata/Internals.lc 111:14-120:25  {a : Num V0} -> Int->V2
-testdata/Internals.lc 111:14-121:22  {a : Num V0} -> V1 -> V2->Ordering
-testdata/Internals.lc 111:14-122:22  {a : Num V0} -> V1->V2
+testdata/Internals.lc 111:14-120:25  Int->V2
+testdata/Internals.lc 111:14-121:22  V1 -> V2->Ordering
+testdata/Internals.lc 111:14-122:22  V1->V2
 testdata/Internals.lc 112:13-112:26  Int->Word
 testdata/Internals.lc 113:13-113:28  Word -> Word->Ordering
 testdata/Internals.lc 114:13-114:27  Word->Word
 testdata/Internals.lc 115:14-115:19  Type
-testdata/Internals.lc 115:14-116:27  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
-testdata/Internals.lc 115:14-117:29  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
-testdata/Internals.lc 115:14-118:28  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
+testdata/Internals.lc 115:14-116:27  Int->V2 -> Int->V3
+testdata/Internals.lc 115:14-117:29  (V1 -> V2->Ordering) -> V2 -> V3->Ordering
+testdata/Internals.lc 115:14-118:28  V1->V2 -> V2->V3
 testdata/Internals.lc 115:14-119:17  Type
-testdata/Internals.lc 115:14-120:25  {a : Num V0} -> Int->V2
-testdata/Internals.lc 115:14-121:22  {a : Num V0} -> V1 -> V2->Ordering
-testdata/Internals.lc 115:14-122:22  {a : Num V0} -> V1->V2
+testdata/Internals.lc 115:14-120:25  Int->V2
+testdata/Internals.lc 115:14-121:22  V1 -> V2->Ordering
+testdata/Internals.lc 115:14-122:22  V1->V2
 testdata/Internals.lc 116:13-116:27  Int->Float
 testdata/Internals.lc 117:13-117:29  Float -> Float->Ordering
 testdata/Internals.lc 118:13-118:28  Float->Float
 testdata/Internals.lc 119:14-119:17  Type
-testdata/Internals.lc 119:14-120:25  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
-testdata/Internals.lc 119:14-121:22  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
-testdata/Internals.lc 119:14-122:22  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
+testdata/Internals.lc 119:14-120:25  Int->V2 -> Int->V3
+testdata/Internals.lc 119:14-121:22  (V1 -> V2->Ordering) -> V2 -> V3->Ordering
+testdata/Internals.lc 119:14-122:22  V1->V2 -> V2->V3
 testdata/Internals.lc 120:13-120:25  Int->Nat
-testdata/Internals.lc 121:13-121:22  {a:Unit} -> Nat -> Nat->Ordering
-testdata/Internals.lc 122:13-122:22  {a:Unit} -> Nat->Nat
+testdata/Internals.lc 121:13-121:22  Nat -> Nat->Ordering
+testdata/Internals.lc 122:13-122:22  Nat->Nat
 testdata/Internals.lc 124:7-124:9  Type->Type
 testdata/Internals.lc 124:7-125:27  Type
 testdata/Internals.lc 124:7-140:29  V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool
@@ -312,9 +312,9 @@ testdata/Internals.lc 125:18-125:19  Type
 testdata/Internals.lc 125:18-125:27  Type
 testdata/Internals.lc 125:23-125:27  Type
 testdata/Internals.lc 129:13-129:19  Type
-testdata/Internals.lc 129:13-129:63  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
+testdata/Internals.lc 129:13-129:63  (V1 -> V2->Bool) -> V2 -> V3->Bool
 testdata/Internals.lc 129:13-137:16  Type | Type->Type
-testdata/Internals.lc 129:13-140:29  {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool
+testdata/Internals.lc 129:13-140:29  V1 -> V2->Bool | {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool
 testdata/Internals.lc 129:35-129:39  Ordering->Bool
 testdata/Internals.lc 129:35-129:63  Bool | String -> String->Bool | String->Bool
 testdata/Internals.lc 129:40-129:63  Ordering
@@ -323,9 +323,9 @@ testdata/Internals.lc 129:41-129:60  String->Ordering
 testdata/Internals.lc 129:59-129:60  String
 testdata/Internals.lc 129:61-129:62  String
 testdata/Internals.lc 130:13-130:17  Type
-testdata/Internals.lc 130:13-130:59  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
+testdata/Internals.lc 130:13-130:59  (V1 -> V2->Bool) -> V2 -> V3->Bool
 testdata/Internals.lc 130:13-137:16  Type
-testdata/Internals.lc 130:13-140:29  {a : Eq V0} -> V1 -> V2->Bool
+testdata/Internals.lc 130:13-140:29  V1 -> V2->Bool
 testdata/Internals.lc 130:33-130:37  Ordering->Bool
 testdata/Internals.lc 130:33-130:59  Bool | Char -> Char->Bool | Char->Bool
 testdata/Internals.lc 130:38-130:59  Ordering
@@ -334,9 +334,9 @@ testdata/Internals.lc 130:39-130:56  Char->Ordering
 testdata/Internals.lc 130:55-130:56  Char
 testdata/Internals.lc 130:57-130:58  Char
 testdata/Internals.lc 131:13-131:16  Type
-testdata/Internals.lc 131:13-131:57  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
+testdata/Internals.lc 131:13-131:57  (V1 -> V2->Bool) -> V2 -> V3->Bool
 testdata/Internals.lc 131:13-137:16  Type
-testdata/Internals.lc 131:13-140:29  {a : Eq V0} -> V1 -> V2->Bool
+testdata/Internals.lc 131:13-140:29  V1 -> V2->Bool
 testdata/Internals.lc 131:32-131:36  Ordering->Bool
 testdata/Internals.lc 131:32-131:57  Bool | Int -> Int->Bool | Int->Bool
 testdata/Internals.lc 131:37-131:57  Ordering
@@ -345,9 +345,9 @@ testdata/Internals.lc 131:38-131:54  Int->Ordering
 testdata/Internals.lc 131:53-131:54  Int
 testdata/Internals.lc 131:55-131:56  Int
 testdata/Internals.lc 132:13-132:18  Type
-testdata/Internals.lc 132:13-132:61  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
+testdata/Internals.lc 132:13-132:61  (V1 -> V2->Bool) -> V2 -> V3->Bool
 testdata/Internals.lc 132:13-137:16  Type
-testdata/Internals.lc 132:13-140:29  {a : Eq V0} -> V1 -> V2->Bool
+testdata/Internals.lc 132:13-140:29  V1 -> V2->Bool
 testdata/Internals.lc 132:34-132:38  Ordering->Bool
 testdata/Internals.lc 132:34-132:61  Bool | Float -> Float->Bool | Float->Bool
 testdata/Internals.lc 132:39-132:61  Ordering
@@ -356,9 +356,9 @@ testdata/Internals.lc 132:40-132:58  Float->Ordering
 testdata/Internals.lc 132:57-132:58  Float
 testdata/Internals.lc 132:59-132:60  Float
 testdata/Internals.lc 133:13-133:17  Type
-testdata/Internals.lc 133:13-136:19  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
+testdata/Internals.lc 133:13-136:19  (V1 -> V2->Bool) -> V2 -> V3->Bool
 testdata/Internals.lc 133:13-137:16  Type
-testdata/Internals.lc 133:13-140:29  {a : Eq V0} -> V1 -> V2->Bool
+testdata/Internals.lc 133:13-140:29  V1 -> V2->Bool
 testdata/Internals.lc 134:5-134:9  Bool
 testdata/Internals.lc 134:5-136:19  Bool | Bool -> Bool->Bool | Bool->Bool
 testdata/Internals.lc 134:13-134:17  Bool
@@ -371,7 +371,7 @@ testdata/Internals.lc 135:22-135:26  Bool
 testdata/Internals.lc 135:22-136:19  Bool->Bool
 testdata/Internals.lc 136:14-136:19  Bool
 testdata/Internals.lc 137:13-137:16  Type
-testdata/Internals.lc 137:13-140:29  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
+testdata/Internals.lc 137:13-140:29  (V1 -> V2->Bool) -> V2 -> V3->Bool
 testdata/Internals.lc 138:5-138:9  Nat
 testdata/Internals.lc 138:5-140:29  Bool | Nat -> Nat->Bool | Nat->Bool
 testdata/Internals.lc 138:15-138:19  Nat
diff --git a/testdata/language-features/adt/gadt01.lc b/testdata/language-features/adt/gadt01.lc
index 6c2b0107..b68762ca 100644
--- a/testdata/language-features/adt/gadt01.lc
+++ b/testdata/language-features/adt/gadt01.lc
@@ -1,4 +1,4 @@
-
+{-# LANGUAGE TraceTypeCheck #-}
 data V :: Nat -> Type -> Type where
   V1_ :: a -> V 1 a
   V2_ :: a -> a -> V 2 a
diff --git a/testdata/typeclass.out b/testdata/typeclass.out
index b4ffbf39..3ad6a5bb 100644
--- a/testdata/typeclass.out
+++ b/testdata/typeclass.out
@@ -35,7 +35,7 @@ testdata/typeclass.lc 20:15-20:19  V4->Bool
 testdata/typeclass.lc 20:17-20:19  {a} -> {b : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 20:20-20:21  V2
 testdata/typeclass.lc 22:13-22:17  Type | Type->Type
-testdata/typeclass.lc 22:13-24:23  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool | {a} -> {b : Eq a} -> a -> a->Bool
+testdata/typeclass.lc 22:13-24:23  (V1 -> V2->Bool) -> V2 -> V3->Bool | {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 23:5-23:9  Bool
 testdata/typeclass.lc 23:5-24:23  Bool | Bool -> Bool->Bool | Bool->Bool
 testdata/typeclass.lc 23:17-23:18  Bool