30 files changed, 372 insertions, 370 deletions

diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 2fb116f9..455a6e7b 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -115,13 +115,18 @@ simple x = case strip x of
     _ -> False
 
 renderDoc :: Doc -> P.Doc
-renderDoc = render . addPar (-10) . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']) . showVars
+renderDoc
+    = render
+    . addPar (-10)
+    . flip runReader ((\s n -> n: '_': s) <$> iterate ('\'':) "" <*> ['a'..'z'])
+    . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z'])
+    . showVars
   where
     showVars x = case x of
         DAtom s -> DAtom <$> showVarA s
         DDoc d -> DDoc <$> traverse showVars d
         DOp s pr x y -> DOp s pr <$> showVars x <*> showVars y
-        DVar i -> asks $ text . lookupVarName i
+        DVar i -> asks $ text . (!! i)
         DFreshName True x -> gets head >>= \n -> modify tail >> local (n:) (showVars x)
         DFreshName False x -> local ("_":) $ showVars x
         DUp i x -> local (dropNth i) $ showVars x
@@ -129,9 +134,6 @@ renderDoc = render . addPar (-10) . flip runReader [] . flip evalStateT (flip (:
         showVarA (SimpleAtom s) = pure $ SimpleAtom s
         showVarA (ComplexAtom s i d a) = ComplexAtom s i <$> showVars d <*> showVarA a
 
-        lookupVarName i xs | i < length xs = xs !! i
-        lookupVarName i _ = ((\s n -> n: '_': s) <$> iterate ('\'':) "" <*> ['a'..'z']) !! i
-
     addPar :: Int -> Doc -> Doc
     addPar pr x = case x of
         DAtom x -> DAtom $ addParA x
diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index 55a1ceed..1c0d0cc2 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -454,44 +454,44 @@ testdata/Builtins.lc 19:40-19:41  Type
 testdata/Builtins.lc 19:42-19:43  Nat
 testdata/Builtins.lc 20:1-20:7  {a} -> {b} -> {c:Nat} -> (a->b) -> VecS a c -> VecS b c
 testdata/Builtins.lc 20:21-20:23  {a} -> a -> a -> VecS a 2
-testdata/Builtins.lc 20:21-20:29  f_ -> VecS g_ 2
-testdata/Builtins.lc 20:21-20:35  VecS f_ 2 | a_ -> b_ -> VecS g_ 2 | b_ -> VecS g_ 2
-testdata/Builtins.lc 20:21-21:43  (e_ -> f_ -> g_ -> h_ -> VecS h_ 4) -> {a:Nat} -> VecS g_ a -> VecS g_ a
-testdata/Builtins.lc 20:21-22:51  (c_->c_) -> VecS d_ b_ -> VecS d_ c_ | VecS d_ b_ -> VecS d_ c_ | {a:Nat} -> VecS f_ a -> VecS f_ a
-testdata/Builtins.lc 20:25-20:26  i_->i_
+testdata/Builtins.lc 20:21-20:29  f_ -> VecS f_ 2
+testdata/Builtins.lc 20:21-20:35  VecS f_ 2 | a_ -> a_ -> VecS e_ 2 | b_ -> VecS f_ 2
+testdata/Builtins.lc 20:21-21:43  (e_ -> e_ -> e_ -> e_ -> VecS d_ 4) -> {a:Nat} -> VecS e_ a -> VecS d_ a
+testdata/Builtins.lc 20:21-22:51  (c_->b_) -> VecS c_ a_ -> VecS b_ a_ | VecS d_ b_ -> VecS c_ b_ | {a:Nat} -> VecS e_ a -> VecS d_ a
+testdata/Builtins.lc 20:25-20:26  i_->h_
 testdata/Builtins.lc 20:25-20:28  f_
 testdata/Builtins.lc 20:27-20:28  c_
-testdata/Builtins.lc 20:31-20:32  g_->g_
+testdata/Builtins.lc 20:31-20:32  g_->f_
 testdata/Builtins.lc 20:31-20:34  f_
 testdata/Builtins.lc 20:33-20:34  g_
 testdata/Builtins.lc 21:23-21:25  {a} -> a -> a -> a -> VecS a 3
-testdata/Builtins.lc 21:23-21:31  g_ -> h_ -> VecS i_ 3
-testdata/Builtins.lc 21:23-21:37  g_ -> VecS h_ 3
-testdata/Builtins.lc 21:23-21:43  VecS g_ 3 | e_ -> f_ -> g_ -> VecS g_ 3 | f_ -> g_ -> VecS g_ 3 | g_ -> VecS g_ 3
-testdata/Builtins.lc 21:27-21:28  i_->i_
+testdata/Builtins.lc 21:23-21:31  g_ -> g_ -> VecS g_ 3
+testdata/Builtins.lc 21:23-21:37  g_ -> VecS g_ 3
+testdata/Builtins.lc 21:23-21:43  VecS g_ 3 | e_ -> e_ -> e_ -> VecS d_ 3 | f_ -> f_ -> VecS e_ 3 | g_ -> VecS f_ 3
+testdata/Builtins.lc 21:27-21:28  i_->h_
 testdata/Builtins.lc 21:27-21:30  g_
 testdata/Builtins.lc 21:29-21:30  h_
-testdata/Builtins.lc 21:33-21:34  h_->h_
+testdata/Builtins.lc 21:33-21:34  h_->g_
 testdata/Builtins.lc 21:33-21:36  g_
 testdata/Builtins.lc 21:35-21:36  h_
-testdata/Builtins.lc 21:39-21:40  h_->h_
+testdata/Builtins.lc 21:39-21:40  h_->g_
 testdata/Builtins.lc 21:39-21:42  g_
 testdata/Builtins.lc 21:41-21:42  h_
 testdata/Builtins.lc 22:25-22:27  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Builtins.lc 22:25-22:33  h_ -> i_ -> j_ -> VecS k_ 4
-testdata/Builtins.lc 22:25-22:39  h_ -> i_ -> VecS j_ 4
-testdata/Builtins.lc 22:25-22:45  h_ -> VecS i_ 4
-testdata/Builtins.lc 22:25-22:51  VecS h_ 4 | e_ -> f_ -> g_ -> h_ -> VecS h_ 4 | f_ -> g_ -> h_ -> VecS h_ 4 | g_ -> h_ -> VecS h_ 4 | h_ -> VecS h_ 4
-testdata/Builtins.lc 22:29-22:30  j_->j_
+testdata/Builtins.lc 22:25-22:33  h_ -> h_ -> h_ -> VecS h_ 4
+testdata/Builtins.lc 22:25-22:39  h_ -> h_ -> VecS h_ 4
+testdata/Builtins.lc 22:25-22:45  h_ -> VecS h_ 4
+testdata/Builtins.lc 22:25-22:51  VecS h_ 4 | e_ -> e_ -> e_ -> e_ -> VecS d_ 4 | f_ -> f_ -> f_ -> VecS e_ 4 | g_ -> g_ -> VecS f_ 4 | h_ -> VecS g_ 4
+testdata/Builtins.lc 22:29-22:30  j_->i_
 testdata/Builtins.lc 22:29-22:32  h_
 testdata/Builtins.lc 22:31-22:32  i_
-testdata/Builtins.lc 22:35-22:36  i_->i_
+testdata/Builtins.lc 22:35-22:36  i_->h_
 testdata/Builtins.lc 22:35-22:38  h_
 testdata/Builtins.lc 22:37-22:38  i_
-testdata/Builtins.lc 22:41-22:42  i_->i_
+testdata/Builtins.lc 22:41-22:42  i_->h_
 testdata/Builtins.lc 22:41-22:44  h_
 testdata/Builtins.lc 22:43-22:44  i_
-testdata/Builtins.lc 22:47-22:48  i_->i_
+testdata/Builtins.lc 22:47-22:48  i_->h_
 testdata/Builtins.lc 22:47-22:50  h_
 testdata/Builtins.lc 22:49-22:50  i_
 testdata/Builtins.lc 24:23-24:26  Type
@@ -793,10 +793,10 @@ testdata/Builtins.lc 58:11-58:12  Type
 testdata/Builtins.lc 59:3-59:6  {a} -> {_ : Component a}->a
 testdata/Builtins.lc 59:10-59:11  Type
 testdata/Builtins.lc 62:10-62:11  b_
-testdata/Builtins.lc 62:10-89:36  b_ | {_ : Component a_}->b_ | {a} -> {_ : Component a}->a
+testdata/Builtins.lc 62:10-89:36  b_ | {_ : Component a_}->a_ | {a} -> {_ : Component a}->a
 testdata/Builtins.lc 62:15-62:18  Type
 testdata/Builtins.lc 63:9-63:10  b_
-testdata/Builtins.lc 63:9-90:31  b_ | {_ : Component a_}->b_ | {a} -> {_ : Component a}->a
+testdata/Builtins.lc 63:9-90:31  b_ | {_ : Component a_}->a_ | {a} -> {_ : Component a}->a
 testdata/Builtins.lc 63:14-63:17  Type
 testdata/Builtins.lc 65:10-65:11  b_
 testdata/Builtins.lc 65:10-89:36  b_
@@ -812,14 +812,14 @@ testdata/Builtins.lc 71:10-71:12  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 71:10-71:16  Float -> VecS Float 2
 testdata/Builtins.lc 71:10-71:20  VecS Float 2
 testdata/Builtins.lc 71:10-77:28  (a:Nat) -> VecS Float ('Succ ('Succ a)) | (a:Nat) -> VecS Float ('Succ a)
-testdata/Builtins.lc 71:10-89:36  (a:Nat) -> VecS b_ a | (a:Type) -> (b:Nat) -> VecS a b | VecS b_ a_
+testdata/Builtins.lc 71:10-89:36  (a:Nat) -> VecS a_ a | (a:Type) -> (b:Nat) -> VecS a b | VecS b_ a_
 testdata/Builtins.lc 71:13-71:16  Float
 testdata/Builtins.lc 71:17-71:20  Float
 testdata/Builtins.lc 72:9-72:11  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 72:9-72:15  Float -> VecS Float 2
 testdata/Builtins.lc 72:9-72:19  VecS Float 2
 testdata/Builtins.lc 72:9-78:27  (a:Nat) -> VecS Float ('Succ ('Succ a)) | (a:Nat) -> VecS Float ('Succ a)
-testdata/Builtins.lc 72:9-90:31  (a:Nat) -> VecS b_ a | (a:Type) -> (b:Nat) -> VecS a b | VecS b_ a_
+testdata/Builtins.lc 72:9-90:31  (a:Nat) -> VecS a_ a | (a:Type) -> (b:Nat) -> VecS a b | VecS b_ a_
 testdata/Builtins.lc 72:12-72:15  Float
 testdata/Builtins.lc 72:16-72:19  Float
 testdata/Builtins.lc 74:10-74:12  {a} -> a -> a -> a -> VecS a 3
@@ -1865,43 +1865,43 @@ testdata/Builtins.lc 187:55-187:66  Type
 testdata/Builtins.lc 187:59-187:60  b_
 testdata/Builtins.lc 187:61-187:66  Type
 testdata/Builtins.lc 201:1-201:5  {a} -> List a -> a
-testdata/Builtins.lc 201:15-201:16  List c_ -> c_ | b_ -> List c_ -> c_ | d_
+testdata/Builtins.lc 201:15-201:16  List c_ -> b_ | b_ -> List b_ -> a_ | d_
 testdata/Builtins.lc 203:6-203:8  {a} -> List a -> List a -> List a
 testdata/Builtins.lc 203:14-203:16  d_
-testdata/Builtins.lc 203:14-204:26  List a_ -> List b_ | a_->b_
+testdata/Builtins.lc 203:14-204:26  List a_ -> List a_ | a_->a_
 testdata/Builtins.lc 204:14-204:15  d_
-testdata/Builtins.lc 204:14-204:17  List c_ -> List d_
-testdata/Builtins.lc 204:14-204:26  List b_ -> e_ | List c_ | a_ -> List b_ -> e_
+testdata/Builtins.lc 204:14-204:17  List c_ -> List c_
+testdata/Builtins.lc 204:14-204:26  List b_ -> d_ | List c_ | a_ -> List a_ -> c_
 testdata/Builtins.lc 204:16-204:17  {a} -> a -> List a -> List a
 testdata/Builtins.lc 204:18-204:20  List f_
 testdata/Builtins.lc 204:21-204:23  h_
 testdata/Builtins.lc 204:24-204:26  List g_
 testdata/Builtins.lc 206:1-206:6  {a} -> {b} -> (b -> a->a) -> a -> List b -> a
 testdata/Builtins.lc 206:16-206:17  f_
-testdata/Builtins.lc 206:16-207:39  List b_ -> g_ | a_->b_
+testdata/Builtins.lc 206:16-207:39  List b_ -> f_ | a_->a_
 testdata/Builtins.lc 207:21-207:22  i_
-testdata/Builtins.lc 207:21-207:39  List b_ -> g_ | a_ -> List b_ -> g_
+testdata/Builtins.lc 207:21-207:39  List b_ -> f_ | a_ -> List a_ -> e_
 testdata/Builtins.lc 207:23-207:24  f_
 testdata/Builtins.lc 207:26-207:31  n_
-testdata/Builtins.lc 207:32-207:33  j_->h_
+testdata/Builtins.lc 207:32-207:33  j_->g_
 testdata/Builtins.lc 207:34-207:35  o_
 testdata/Builtins.lc 207:36-207:38  List k_
 testdata/Builtins.lc 209:1-209:7  {a} -> List (List a) -> List a
 testdata/Builtins.lc 209:10-209:15  {a} -> {b} -> (b -> a->a) -> a -> List b -> a
-testdata/Builtins.lc 209:10-209:20  List a_ -> List (List b_) -> List c_
-testdata/Builtins.lc 209:10-209:23  List (List a_) -> List b_
+testdata/Builtins.lc 209:10-209:20  List a_ -> List (List a_) -> List a_
+testdata/Builtins.lc 209:10-209:23  List (List a_) -> List a_
 testdata/Builtins.lc 209:16-209:20  {a} -> List a -> List a -> List a
 testdata/Builtins.lc 209:21-209:23  {a} -> List a
 testdata/Builtins.lc 211:1-211:4  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 211:16-211:18  {a} -> List a
-testdata/Builtins.lc 211:16-212:30  List b_ -> List b_ | a_->b_
+testdata/Builtins.lc 211:16-212:30  List b_ -> List a_ | a_->a_
 testdata/Builtins.lc 212:16-212:17  i_
-testdata/Builtins.lc 212:16-212:21  List a_ -> List b_
-testdata/Builtins.lc 212:16-212:30  List c_ | List c_ -> List c_ | b_ -> List c_ -> List c_
+testdata/Builtins.lc 212:16-212:21  List a_ -> List a_
+testdata/Builtins.lc 212:16-212:30  List c_ | List c_ -> List b_ | b_ -> List b_ -> List a_
 testdata/Builtins.lc 212:18-212:19  h_
 testdata/Builtins.lc 212:20-212:21  {a} -> a -> List a -> List a
 testdata/Builtins.lc 212:22-212:25  i_
-testdata/Builtins.lc 212:26-212:27  g_->g_
+testdata/Builtins.lc 212:26-212:27  g_->f_
 testdata/Builtins.lc 212:28-212:30  List h_
 testdata/Builtins.lc 214:14-214:38  Type
 testdata/Builtins.lc 214:15-214:16  d_
@@ -1914,18 +1914,18 @@ testdata/Builtins.lc 214:35-214:38  Type
 testdata/Builtins.lc 214:36-214:37  Type
 testdata/Builtins.lc 215:1-215:10  {a} -> {b} -> (a -> List b) -> List a -> List b
 testdata/Builtins.lc 215:17-215:23  {a} -> List (List a) -> List a
-testdata/Builtins.lc 215:17-215:33  (b_ -> List b_) -> List c_ -> List c_ | List c_ | List c_ -> List c_
+testdata/Builtins.lc 215:17-215:33  (b_ -> List a_) -> List b_ -> List a_ | List c_ | List c_ -> List b_
 testdata/Builtins.lc 215:25-215:28  {a} -> {b} -> (a->b) -> List a -> List b
-testdata/Builtins.lc 215:25-215:30  List e_ -> List (List e_)
+testdata/Builtins.lc 215:25-215:30  List e_ -> List (List d_)
 testdata/Builtins.lc 215:25-215:32  List (List c_)
-testdata/Builtins.lc 215:29-215:30  g_ -> List g_
+testdata/Builtins.lc 215:29-215:30  g_ -> List f_
 testdata/Builtins.lc 215:31-215:32  List d_
 testdata/Builtins.lc 217:1-217:4  {a} -> List a -> Int
 testdata/Builtins.lc 217:10-217:11  b_
-testdata/Builtins.lc 217:10-218:35  List b_ -> Int | a_->b_
+testdata/Builtins.lc 217:10-218:35  List b_ -> Int | a_->a_
 testdata/Builtins.lc 218:14-218:15  b_
 testdata/Builtins.lc 218:14-218:28  Int->Int
-testdata/Builtins.lc 218:14-218:35  Int | List d_ -> d_ | c_ -> List d_ -> d_
+testdata/Builtins.lc 218:14-218:35  Int | List d_ -> c_ | c_ -> List c_ -> b_
 testdata/Builtins.lc 218:16-218:28  Int -> Int->Int
 testdata/Builtins.lc 218:29-218:32  h_
 testdata/Builtins.lc 218:33-218:35  List g_
@@ -2022,10 +2022,10 @@ testdata/Builtins.lc 252:69-252:70  PrimitiveType
 testdata/Builtins.lc 252:71-252:72  Type
 testdata/Builtins.lc 253:1-253:14  {a} -> {b} -> {c:PrimitiveType} -> (a->b) -> List (Primitive a c) -> List (Primitive b c)
 testdata/Builtins.lc 253:19-253:22  {a} -> {b} -> (a->b) -> List a -> List b
-testdata/Builtins.lc 253:19-253:39  (c_->c_) -> PrimitiveStream b_ d_ -> PrimitiveStream c_ d_ | List (Primitive e_ a_) -> List (Primitive e_ b_)
+testdata/Builtins.lc 253:19-253:39  (c_->b_) -> PrimitiveStream a_ c_ -> PrimitiveStream a_ b_ | List (Primitive e_ a_) -> List (Primitive d_ a_)
 testdata/Builtins.lc 253:24-253:36  {a} -> {b} -> {c:PrimitiveType} -> (a->b) -> Primitive a c -> Primitive b c
-testdata/Builtins.lc 253:24-253:38  Primitive g_ a_ -> Primitive g_ b_
-testdata/Builtins.lc 253:37-253:38  i_->i_
+testdata/Builtins.lc 253:24-253:38  Primitive g_ a_ -> Primitive f_ a_
+testdata/Builtins.lc 253:37-253:38  i_->h_
 testdata/Builtins.lc 255:30-255:38  Type->Type
 testdata/Builtins.lc 255:45-255:46  Type | Type->Type
 testdata/Builtins.lc 260:1-260:12  {a:PrimitiveType} -> {b : List Type} -> {c : List Type} -> {_ : b ~ 'map Type Type ListElem c} -> HList c -> PrimitiveStream a (HList b)
@@ -2156,9 +2156,9 @@ testdata/Builtins.lc 281:73-281:74  Nat
 testdata/Builtins.lc 281:75-281:76  Type
 testdata/Builtins.lc 282:1-282:16  {a} -> {b:Nat} -> (a->Float) -> List (Vector b (Maybe (SimpleFragment a))) -> List (Vector b (Maybe (SimpleFragment a)))
 testdata/Builtins.lc 282:21-282:24  {a} -> {b} -> (a->b) -> List a -> List b
-testdata/Builtins.lc 282:21-282:43  (b_->Float) -> FragmentStream b_ c_ -> FragmentStream c_ d_ | List (Vector a_ (Maybe (SimpleFragment d_))) -> List (Vector b_ (Maybe (SimpleFragment e_)))
+testdata/Builtins.lc 282:21-282:43  (b_->Float) -> FragmentStream a_ b_ -> FragmentStream a_ b_ | List (Vector a_ (Maybe (SimpleFragment d_))) -> List (Vector a_ (Maybe (SimpleFragment d_)))
 testdata/Builtins.lc 282:26-282:40  {a} -> {b:Nat} -> (a->Float) -> Fragment b a -> Fragment b a
-testdata/Builtins.lc 282:26-282:42  Fragment a_ f_ -> Fragment b_ g_
+testdata/Builtins.lc 282:26-282:42  Fragment a_ f_ -> Fragment a_ f_
 testdata/Builtins.lc 282:41-282:42  g_->Float
 testdata/Builtins.lc 284:1-284:15  {a} -> {b:Nat} -> (a->Bool) -> Fragment b a -> Fragment b a
 testdata/Builtins.lc 284:19-284:62  Type
@@ -2191,9 +2191,9 @@ testdata/Builtins.lc 286:72-286:73  Nat
 testdata/Builtins.lc 286:74-286:75  Type
 testdata/Builtins.lc 287:1-287:16  {a} -> {b:Nat} -> (a->Bool) -> List (Vector b (Maybe (SimpleFragment a))) -> List (Vector b (Maybe (SimpleFragment a)))
 testdata/Builtins.lc 287:21-287:24  {a} -> {b} -> (a->b) -> List a -> List b
-testdata/Builtins.lc 287:21-287:43  (b_->Bool) -> FragmentStream b_ c_ -> FragmentStream c_ d_ | List (Vector a_ (Maybe (SimpleFragment d_))) -> List (Vector b_ (Maybe (SimpleFragment e_)))
+testdata/Builtins.lc 287:21-287:43  (b_->Bool) -> FragmentStream a_ b_ -> FragmentStream a_ b_ | List (Vector a_ (Maybe (SimpleFragment d_))) -> List (Vector a_ (Maybe (SimpleFragment d_)))
 testdata/Builtins.lc 287:26-287:40  {a} -> {b:Nat} -> (a->Bool) -> Fragment b a -> Fragment b a
-testdata/Builtins.lc 287:26-287:42  Fragment a_ f_ -> Fragment b_ g_
+testdata/Builtins.lc 287:26-287:42  Fragment a_ f_ -> Fragment a_ f_
 testdata/Builtins.lc 287:41-287:42  g_->Bool
 testdata/Builtins.lc 289:1-289:12  {a} -> {b} -> {c:Nat} -> (a->b) -> Fragment c a -> Fragment c b
 testdata/Builtins.lc 289:16-289:56  Type
@@ -2226,10 +2226,10 @@ testdata/Builtins.lc 291:66-291:67  Nat
 testdata/Builtins.lc 291:68-291:69  Type
 testdata/Builtins.lc 292:1-292:13  {a} -> {b} -> {c:Nat} -> (a->b) -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b)))
 testdata/Builtins.lc 292:18-292:21  {a} -> {b} -> (a->b) -> List a -> List b
-testdata/Builtins.lc 292:18-292:37  (c_->c_) -> FragmentStream b_ d_ -> FragmentStream c_ d_ | List (Vector a_ (Maybe (SimpleFragment e_))) -> List (Vector b_ (Maybe (SimpleFragment e_)))
+testdata/Builtins.lc 292:18-292:37  (c_->b_) -> FragmentStream a_ c_ -> FragmentStream a_ b_ | List (Vector a_ (Maybe (SimpleFragment e_))) -> List (Vector a_ (Maybe (SimpleFragment d_)))
 testdata/Builtins.lc 292:23-292:34  {a} -> {b} -> {c:Nat} -> (a->b) -> Fragment c a -> Fragment c b
-testdata/Builtins.lc 292:23-292:36  Fragment a_ g_ -> Fragment b_ g_
-testdata/Builtins.lc 292:35-292:36  i_->i_
+testdata/Builtins.lc 292:23-292:36  Fragment a_ g_ -> Fragment a_ f_
+testdata/Builtins.lc 292:35-292:36  i_->h_
 testdata/Builtins.lc 296:6-296:15  Type
 testdata/Builtins.lc 296:6-299:14  Type
 testdata/Builtins.lc 297:7-297:12  ImageKind | Type | Type->ImageKind
@@ -2239,7 +2239,7 @@ testdata/Builtins.lc 299:7-299:14  ImageKind
 testdata/Builtins.lc 301:14-301:23  Type
 testdata/Builtins.lc 301:27-301:31  Type
 testdata/Builtins.lc 302:1-302:10  ImageKind->Type
-testdata/Builtins.lc 302:23-302:24  Type | Type->b_
+testdata/Builtins.lc 302:23-302:24  Type | Type->a_
 testdata/Builtins.lc 302:23-303:25  Type -> ImageKind->Type
 testdata/Builtins.lc 302:23-304:25  ImageKind->Type | Type
 testdata/Builtins.lc 303:19-303:25  Type
@@ -2314,19 +2314,19 @@ testdata/Builtins.lc 339:38-339:48  Type
 testdata/Builtins.lc 339:47-339:48  Type
 testdata/Builtins.lc 340:1-340:12  {a} -> {b:Nat} -> Vec b a -> Swizz->a
 testdata/Builtins.lc 340:27-340:28  e_
-testdata/Builtins.lc 340:27-341:28  b_ -> c_->c_ | c_ | c_->c_ | d_ -> e_ -> Swizz->g_
-testdata/Builtins.lc 340:27-344:30  (a_ -> b_ -> c_ -> d_->e_) -> {a:Nat} -> VecS c_ a -> d_
-testdata/Builtins.lc 340:27-348:32  Swizz->d_ | Vec a_ b_ -> Swizz->d_ | d_ | {a:Nat} -> VecS b_ a -> c_
+testdata/Builtins.lc 340:27-341:28  b_ -> b_->a_ | c_ | c_->b_ | d_ -> d_ -> Swizz->d_
+testdata/Builtins.lc 340:27-344:30  (a_ -> a_ -> a_ -> a_->a_) -> {a:Nat} -> VecS a_ a -> a_
+testdata/Builtins.lc 340:27-348:32  Swizz->c_ | Vec a_ b_ -> Swizz->b_ | d_ | {a:Nat} -> VecS a_ a -> a_
 testdata/Builtins.lc 341:27-341:28  d_
 testdata/Builtins.lc 342:29-342:30  e_
-testdata/Builtins.lc 342:29-343:30  d_ -> e_ -> Swizz->g_
-testdata/Builtins.lc 342:29-344:30  a_ -> b_ -> c_->d_ | b_ -> c_->d_ | c_->d_ | d_ | d_ -> Swizz->f_
+testdata/Builtins.lc 342:29-343:30  d_ -> d_ -> Swizz->d_
+testdata/Builtins.lc 342:29-344:30  a_ -> a_ -> a_->a_ | b_ -> b_->b_ | c_->c_ | d_ | d_ -> Swizz->d_
 testdata/Builtins.lc 343:29-343:30  d_
 testdata/Builtins.lc 344:29-344:30  d_
 testdata/Builtins.lc 345:31-345:32  f_
-testdata/Builtins.lc 345:31-346:32  e_ -> f_ -> Swizz->h_
-testdata/Builtins.lc 345:31-347:32  e_ -> Swizz->g_
-testdata/Builtins.lc 345:31-348:32  Swizz->f_ | a_ -> b_ -> c_ -> d_->e_ | b_ -> c_ -> d_->e_ | c_ -> d_->e_ | d_->e_ | e_
+testdata/Builtins.lc 345:31-346:32  e_ -> e_ -> Swizz->e_
+testdata/Builtins.lc 345:31-347:32  e_ -> Swizz->e_
+testdata/Builtins.lc 345:31-348:32  Swizz->e_ | a_ -> a_ -> a_ -> a_->a_ | b_ -> b_ -> b_->b_ | c_ -> c_->c_ | d_->d_ | e_
 testdata/Builtins.lc 346:31-346:32  e_
 testdata/Builtins.lc 347:31-347:32  e_
 testdata/Builtins.lc 348:31-348:32  e_
@@ -2338,11 +2338,11 @@ testdata/Builtins.lc 351:32-351:33  b_
 testdata/Builtins.lc 351:34-351:35  c_
 testdata/Builtins.lc 351:39-351:43  Type
 testdata/Builtins.lc 352:1-352:11  {a} -> {b:Nat} -> Vec b a -> Bool
-testdata/Builtins.lc 352:23-352:27  Bool | b_ -> c_->c_ | c_->c_
-testdata/Builtins.lc 352:23-353:29  (a_ -> b_ -> c_ -> d_->Bool) -> {a:Nat} -> VecS c_ a -> Bool
-testdata/Builtins.lc 352:23-354:31  Bool | Vec a_ b_ -> Bool | {a:Nat} -> VecS b_ a -> Bool
-testdata/Builtins.lc 353:25-353:29  Bool | a_ -> b_ -> c_->Bool | b_ -> c_->Bool | c_->Bool
-testdata/Builtins.lc 354:27-354:31  Bool | a_ -> b_ -> c_ -> d_->Bool | b_ -> c_ -> d_->Bool | c_ -> d_->Bool | d_->Bool
+testdata/Builtins.lc 352:23-352:27  Bool | b_ -> b_->a_ | c_->b_
+testdata/Builtins.lc 352:23-353:29  (a_ -> a_ -> a_ -> a_->Bool) -> {a:Nat} -> VecS a_ a -> Bool
+testdata/Builtins.lc 352:23-354:31  Bool | Vec a_ b_ -> Bool | {a:Nat} -> VecS a_ a -> Bool
+testdata/Builtins.lc 353:25-353:29  Bool | a_ -> a_ -> a_->Bool | b_ -> b_->Bool | c_->Bool
+testdata/Builtins.lc 354:27-354:31  Bool | a_ -> a_ -> a_ -> a_->Bool | b_ -> b_ -> b_->Bool | c_ -> c_->Bool | d_->Bool
 testdata/Builtins.lc 356:16-356:71  Type
 testdata/Builtins.lc 356:27-356:71  Type
 testdata/Builtins.lc 356:38-356:41  Nat -> Type->Type
@@ -2365,13 +2365,13 @@ testdata/Builtins.lc 356:70-356:71  Type
 testdata/Builtins.lc 357:1-357:12  {a} -> {b:Nat} -> {c:Nat} -> Vec b a -> Vec c Swizz -> VecS a c
 testdata/Builtins.lc 357:19-357:29  {a} -> {b:Nat} -> Vec b a -> Bool
 testdata/Builtins.lc 357:19-357:31  Bool
-testdata/Builtins.lc 357:19-357:58  Vec b_ Swizz -> Vec c_ e_ | Vec b_ c_ -> Vec b_ Swizz -> Vec c_ e_ | VecS e_ c_
+testdata/Builtins.lc 357:19-357:58  Vec b_ Swizz -> Vec b_ d_ | Vec b_ c_ -> Vec a_ Swizz -> Vec a_ c_ | VecS e_ c_
 testdata/Builtins.lc 357:30-357:31  Vec f_ g_
 testdata/Builtins.lc 357:34-357:40  {a} -> {b} -> {c:Nat} -> (a->b) -> VecS a c -> VecS b c
-testdata/Builtins.lc 357:34-357:56  VecS Swizz a_ -> VecS h_ b_
+testdata/Builtins.lc 357:34-357:56  VecS Swizz a_ -> VecS g_ a_
 testdata/Builtins.lc 357:34-357:58  VecS e_ c_
 testdata/Builtins.lc 357:42-357:53  {a} -> {b:Nat} -> Vec b a -> Swizz->a
-testdata/Builtins.lc 357:42-357:55  Swizz->j_
+testdata/Builtins.lc 357:42-357:55  Swizz->i_
 testdata/Builtins.lc 357:54-357:55  Vec j_ k_
 testdata/Builtins.lc 357:57-357:58  Vec d_ Swizz
 testdata/Builtins.lc 361:6-361:20  Type
@@ -2711,11 +2711,11 @@ testdata/Builtins.lc 488:1-488:20  {a : List Type} -> {b:PrimitiveType} -> Raste
 testdata/Builtins.lc 488:32-488:38  {a} -> List (List a) -> List a
 testdata/Builtins.lc 488:32-488:74  List (Vector 1 (Maybe (SimpleFragment (HList b_))))
 testdata/Builtins.lc 488:40-488:43  {a} -> {b} -> (a->b) -> List a -> List b
-testdata/Builtins.lc 488:40-488:71  List (Primitive (HList ('Cons (Vec 4 Float) b_)) a_) -> List (List (Fragment 1 (HList c_)))
+testdata/Builtins.lc 488:40-488:71  List (Primitive (HList ('Cons (Vec 4 Float) b_)) a_) -> List (List (Fragment 1 (HList b_)))
 testdata/Builtins.lc 488:40-488:73  List (List (Fragment 1 (HList b_)))
 testdata/Builtins.lc 488:45-488:63  {a : List Type} -> {b : List Type} -> {c : List Type} -> {d:PrimitiveType} -> {_ : 'map Type Type Interpolated a ~ b} -> {_ : c ~ 'Cons (Vec 4 Float) a} -> HList b -> RasterContext (HList c) d -> Primitive (HList c) d -> FragmentStream 1 (HList a)
-testdata/Builtins.lc 488:45-488:66  RasterContext (HList ('Cons (Vec 4 Float) b_)) a_ -> Primitive (HList ('Cons (Vec 4 Float) c_)) b_ -> FragmentStream 1 (HList d_)
-testdata/Builtins.lc 488:45-488:70  Primitive (HList ('Cons (Vec 4 Float) b_)) a_ -> FragmentStream 1 (HList c_)
+testdata/Builtins.lc 488:45-488:66  RasterContext (HList ('Cons (Vec 4 Float) b_)) a_ -> Primitive (HList ('Cons (Vec 4 Float) b_)) a_ -> FragmentStream 1 (HList b_)
+testdata/Builtins.lc 488:45-488:70  Primitive (HList ('Cons (Vec 4 Float) b_)) a_ -> FragmentStream 1 (HList b_)
 testdata/Builtins.lc 488:64-488:66  i_
 testdata/Builtins.lc 488:67-488:70  h_
 testdata/Builtins.lc 488:72-488:73  d_
@@ -2724,17 +2724,17 @@ testdata/Builtins.lc 490:36-490:43  Type->Nat
 testdata/Builtins.lc 490:58-490:59  ImageKind->Nat | Nat | Nat -> ImageKind->Nat | Type->Nat
 testdata/Builtins.lc 492:12-492:15  Type
 testdata/Builtins.lc 492:12-492:23  Type
-testdata/Builtins.lc 492:12-495:50  a_->b_ | {a} -> List a -> Type
+testdata/Builtins.lc 492:12-495:50  a_->a_ | {a} -> List a -> Type
 testdata/Builtins.lc 492:13-492:14  b_
 testdata/Builtins.lc 492:19-492:23  Type
 testdata/Builtins.lc 493:1-493:8  {a} -> List a -> Type
 testdata/Builtins.lc 493:14-493:19  Type
 testdata/Builtins.lc 493:14-495:50  List a_ -> Type | Type
 testdata/Builtins.lc 494:15-494:20  Type
-testdata/Builtins.lc 494:15-495:50  List b_ -> Type | List c_ -> Type | Type | a_ -> List b_ -> Type
+testdata/Builtins.lc 494:15-495:50  List b_ -> Type | List c_ -> Type | Type | a_ -> List a_ -> Type
 testdata/Builtins.lc 495:22-495:25  Type -> Type->Type
 testdata/Builtins.lc 495:22-495:33  Type->Type
-testdata/Builtins.lc 495:22-495:50  List b_ -> Type | Type | a_ -> List b_ -> Type
+testdata/Builtins.lc 495:22-495:50  List b_ -> Type | Type | a_ -> List a_ -> Type
 testdata/Builtins.lc 495:27-495:28  g_
 testdata/Builtins.lc 495:27-495:30  f_->Type
 testdata/Builtins.lc 495:27-495:32  Type
@@ -2743,7 +2743,7 @@ testdata/Builtins.lc 495:31-495:32  c_
 testdata/Builtins.lc 495:35-495:42  {a} -> List a -> Type
 testdata/Builtins.lc 495:35-495:49  Type
 testdata/Builtins.lc 495:44-495:45  g_
-testdata/Builtins.lc 495:44-495:46  List f_ -> List g_
+testdata/Builtins.lc 495:44-495:46  List f_ -> List f_
 testdata/Builtins.lc 495:44-495:48  List e_
 testdata/Builtins.lc 495:45-495:46  {a} -> a -> List a -> List a
 testdata/Builtins.lc 495:46-495:48  List e_
@@ -2768,12 +2768,12 @@ testdata/Builtins.lc 512:1-512:11  List ImageKind -> List Type
 testdata/Builtins.lc 512:25-512:28  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 512:25-512:38  List ImageKind -> List Type
 testdata/Builtins.lc 512:25-512:40  List Type
-testdata/Builtins.lc 512:25-513:31  List ImageKind -> List Type | List Type | List Type -> ImageKind -> List Type | List b_ -> List Type | a_ -> List b_ -> List Type
+testdata/Builtins.lc 512:25-513:31  List ImageKind -> List Type | List Type | List Type -> ImageKind -> List Type | List b_ -> List Type | a_ -> List a_ -> List Type
 testdata/Builtins.lc 512:29-512:38  ImageKind->Type
 testdata/Builtins.lc 512:39-512:40  List c_
 testdata/Builtins.lc 513:16-513:19  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 513:16-513:29  List ImageKind -> List Type
-testdata/Builtins.lc 513:16-513:31  List Type | Type->b_
+testdata/Builtins.lc 513:16-513:31  List Type | Type->a_
 testdata/Builtins.lc 513:20-513:29  ImageKind->Type
 testdata/Builtins.lc 513:30-513:31  List ImageKind
 testdata/Builtins.lc 515:40-515:49  Type
@@ -2826,9 +2826,9 @@ testdata/Builtins.lc 519:25-519:28  f_
 testdata/Builtins.lc 519:30-519:31  ((b_)) | e_
 testdata/Builtins.lc 520:1-520:8  {a:Nat} -> {b : List Type} -> FrameBuffer a ('map Type ImageKind FragmentOperationKind b) -> (HList b, List (Fragment a (HList ('imageType' ('map Type ImageKind FragmentOperationKind b))))) -> FrameBuffer a ('map Type ImageKind FragmentOperationKind b)
 testdata/Builtins.lc 520:25-520:35  {a : List ImageKind} -> {b:Nat} -> {c : List Type} -> {_ : a ~ 'map Type ImageKind FragmentOperationKind c} -> HList c -> FragmentStream b (HList ('imageType' a)) -> FrameBuffer b a -> FrameBuffer b a
-testdata/Builtins.lc 520:25-520:39  FragmentStream b_ (HList ('imageType' ('map Type ImageKind FragmentOperationKind a_))) -> FrameBuffer c_ ('map Type ImageKind FragmentOperationKind b_) -> FrameBuffer d_ ('map Type ImageKind FragmentOperationKind c_)
-testdata/Builtins.lc 520:25-520:43  FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_) -> FrameBuffer c_ ('map Type ImageKind FragmentOperationKind b_)
-testdata/Builtins.lc 520:25-520:46  FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_) | HList c_ -> c_ | c_ -> HList c_ -> c_
+testdata/Builtins.lc 520:25-520:39  FragmentStream b_ (HList ('imageType' ('map Type ImageKind FragmentOperationKind a_))) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_)
+testdata/Builtins.lc 520:25-520:43  FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_)
+testdata/Builtins.lc 520:25-520:46  FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_) | HList c_ -> b_ | c_ -> HList b_ -> a_
 testdata/Builtins.lc 520:36-520:39  m_
 testdata/Builtins.lc 520:40-520:43  h_
 testdata/Builtins.lc 520:44-520:46  n_
@@ -2863,12 +2863,12 @@ testdata/Builtins.lc 532:1-532:11  {a : List Type} -> {_ : 'sameLayerCounts a} -
 testdata/Builtins.lc 532:14-532:25  {a : List Type} -> {_ : 'sameLayerCounts a} -> HList a -> FrameBuffer (ImageLC ('head Type a)) ('map Type ImageKind GetImageKind a)
 testdata/Builtins.lc 534:1-534:11  {a:Nat} -> {b : List Type} -> {c} -> HList b -> (c -> HList ('imageType' ('map Type ImageKind FragmentOperationKind b))) -> List (Vector a (Maybe (SimpleFragment c))) -> FrameBuffer a ('map Type ImageKind FragmentOperationKind b) -> FrameBuffer a ('map Type ImageKind FragmentOperationKind b)
 testdata/Builtins.lc 534:34-534:44  {a : List ImageKind} -> {b:Nat} -> {c : List Type} -> {_ : a ~ 'map Type ImageKind FragmentOperationKind c} -> HList c -> FragmentStream b (HList ('imageType' a)) -> FrameBuffer b a -> FrameBuffer b a
-testdata/Builtins.lc 534:34-534:48  FragmentStream b_ (HList ('imageType' ('map Type ImageKind FragmentOperationKind a_))) -> FrameBuffer c_ ('map Type ImageKind FragmentOperationKind b_) -> FrameBuffer d_ ('map Type ImageKind FragmentOperationKind c_)
-testdata/Builtins.lc 534:34-534:76  FrameBuffer c_ ('map Type ImageKind FragmentOperationKind b_) -> FrameBuffer d_ ('map Type ImageKind FragmentOperationKind c_)
+testdata/Builtins.lc 534:34-534:48  FragmentStream b_ (HList ('imageType' ('map Type ImageKind FragmentOperationKind a_))) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind a_)
+testdata/Builtins.lc 534:34-534:76  FrameBuffer c_ ('map Type ImageKind FragmentOperationKind b_) -> FrameBuffer c_ ('map Type ImageKind FragmentOperationKind b_)
 testdata/Builtins.lc 534:34-534:79  FrameBuffer c_ ('map Type ImageKind FragmentOperationKind b_)
 testdata/Builtins.lc 534:45-534:48  j_
 testdata/Builtins.lc 534:50-534:62  {a} -> {b} -> {c:Nat} -> (a->b) -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b)))
-testdata/Builtins.lc 534:50-534:70  List (Vector a_ (Maybe (SimpleFragment c_))) -> List (Vector b_ (Maybe (SimpleFragment c_)))
+testdata/Builtins.lc 534:50-534:70  List (Vector a_ (Maybe (SimpleFragment c_))) -> List (Vector a_ (Maybe (SimpleFragment b_)))
 testdata/Builtins.lc 534:50-534:75  List (Vector c_ (Maybe (SimpleFragment (HList ('imageType' ('map Type ImageKind FragmentOperationKind b_))))))
 testdata/Builtins.lc 534:63-534:70  k_
 testdata/Builtins.lc 534:71-534:75  g_
diff --git a/testdata/Internals.out b/testdata/Internals.out
index 8f9dc73c..7ca88d81 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -139,7 +139,7 @@ testdata/Internals.lc 36:84-36:87  Type
 testdata/Internals.lc 36:86-36:87  Type
 testdata/Internals.lc 38:6-38:11  {a} -> a -> a->Type
 testdata/Internals.lc 38:14-38:18  (a:Type) -> a -> a->Type
-testdata/Internals.lc 38:14-38:20  a_ -> b_->Type
+testdata/Internals.lc 38:14-38:20  a_ -> a_->Type
 testdata/Internals.lc 41:1-41:4  Unit -> Unit->Unit
 testdata/Internals.lc 41:8-41:12  Type
 testdata/Internals.lc 41:16-41:20  Type
@@ -236,7 +236,7 @@ testdata/Internals.lc 74:32-74:38  Type
 testdata/Internals.lc 74:37-74:38  Type
 testdata/Internals.lc 75:1-75:15  {a} -> Bool -> a -> a->a
 testdata/Internals.lc 75:28-75:29  d_
-testdata/Internals.lc 75:28-76:29  Bool -> b_ -> c_->d_ | Bool->e_ | b_ -> c_->d_ | c_->d_ | d_
+testdata/Internals.lc 75:28-76:29  Bool -> a_ -> a_->a_ | Bool->d_ | b_ -> b_->b_ | c_->c_ | d_
 testdata/Internals.lc 76:28-76:29  e_
 testdata/Internals.lc 78:1-78:5  Ordering->Bool
 testdata/Internals.lc 78:11-78:15  Bool
@@ -260,30 +260,30 @@ testdata/Internals.lc 85:3-85:9  {a} -> {_ : Num a} -> a->a
 testdata/Internals.lc 85:13-85:14  Type
 testdata/Internals.lc 85:13-85:19  Type
 testdata/Internals.lc 85:18-85:19  Type
-testdata/Internals.lc 88:13-100:25  Int->c_ | {_ : Num a_} -> Int->c_ | {a} -> {_ : Num a} -> Int->a
+testdata/Internals.lc 88:13-100:25  Int->b_ | {_ : Num a_} -> Int->a_ | {a} -> {_ : Num a} -> Int->a
 testdata/Internals.lc 88:19-88:20  b_
 testdata/Internals.lc 89:13-89:27  Int -> Int->Ordering
-testdata/Internals.lc 89:13-101:22  b_ -> c_->Ordering | {_ : Num a_} -> b_ -> c_->Ordering | {a} -> {_ : Num a} -> a -> a->Ordering
+testdata/Internals.lc 89:13-101:22  b_ -> b_->Ordering | {_ : Num a_} -> a_ -> a_->Ordering | {a} -> {_ : Num a} -> a -> a->Ordering
 testdata/Internals.lc 90:13-90:26  Int->Int
-testdata/Internals.lc 90:13-102:22  b_->c_ | {_ : Num a_} -> b_->c_ | {a} -> {_ : Num a} -> a->a
+testdata/Internals.lc 90:13-102:22  b_->b_ | {_ : Num a_} -> a_->a_ | {a} -> {_ : Num a} -> a->a
 testdata/Internals.lc 92:13-92:26  Int->Word
-testdata/Internals.lc 92:13-100:25  Int->c_
+testdata/Internals.lc 92:13-100:25  Int->b_
 testdata/Internals.lc 93:13-93:28  Word -> Word->Ordering
-testdata/Internals.lc 93:13-101:22  b_ -> c_->Ordering
+testdata/Internals.lc 93:13-101:22  b_ -> b_->Ordering
 testdata/Internals.lc 94:13-94:27  Word->Word
-testdata/Internals.lc 94:13-102:22  b_->c_
+testdata/Internals.lc 94:13-102:22  b_->b_
 testdata/Internals.lc 96:13-96:27  Int->Float
-testdata/Internals.lc 96:13-100:25  Int->c_
+testdata/Internals.lc 96:13-100:25  Int->b_
 testdata/Internals.lc 97:13-97:29  Float -> Float->Ordering
-testdata/Internals.lc 97:13-101:22  b_ -> c_->Ordering
+testdata/Internals.lc 97:13-101:22  b_ -> b_->Ordering
 testdata/Internals.lc 98:13-98:28  Float->Float
-testdata/Internals.lc 98:13-102:22  b_->c_
+testdata/Internals.lc 98:13-102:22  b_->b_
 testdata/Internals.lc 100:13-100:25  Int->Nat
 testdata/Internals.lc 101:13-101:22  {a}->a
 testdata/Internals.lc 102:13-102:22  {a}->a
 testdata/Internals.lc 104:7-104:9  Type->Type
 testdata/Internals.lc 104:7-105:27  Type
-testdata/Internals.lc 104:7-120:29  a_->b_ | {a} -> {_ : Eq a} -> a -> a->Bool
+testdata/Internals.lc 104:7-120:29  a_->a_ | {a} -> {_ : Eq a} -> a -> a->Bool
 testdata/Internals.lc 105:6-105:8  {a} -> {_ : Eq a} -> a -> a->Bool
 testdata/Internals.lc 105:13-105:14  Type
 testdata/Internals.lc 105:13-105:27  Type
@@ -292,7 +292,7 @@ testdata/Internals.lc 105:18-105:27  Type
 testdata/Internals.lc 105:23-105:27  Type
 testdata/Internals.lc 109:35-109:39  Ordering->Bool
 testdata/Internals.lc 109:35-109:63  Bool
-testdata/Internals.lc 109:35-120:29  b_ -> c_->Bool | {_ : Eq a_} -> b_ -> c_->Bool | {a} -> {_ : Eq a} -> a -> a->Bool
+testdata/Internals.lc 109:35-120:29  b_ -> b_->Bool | {_ : Eq a_} -> a_ -> a_->Bool | {a} -> {_ : Eq a} -> a -> a->Bool
 testdata/Internals.lc 109:41-109:58  String -> String->Ordering
 testdata/Internals.lc 109:41-109:60  String->Ordering
 testdata/Internals.lc 109:41-109:62  Ordering
@@ -300,7 +300,7 @@ testdata/Internals.lc 109:59-109:60  d_
 testdata/Internals.lc 109:61-109:62  b_
 testdata/Internals.lc 110:33-110:37  Ordering->Bool
 testdata/Internals.lc 110:33-110:59  Bool
-testdata/Internals.lc 110:33-120:29  b_ -> c_->Bool
+testdata/Internals.lc 110:33-120:29  b_ -> b_->Bool
 testdata/Internals.lc 110:39-110:54  Char -> Char->Ordering
 testdata/Internals.lc 110:39-110:56  Char->Ordering
 testdata/Internals.lc 110:39-110:58  Ordering
@@ -308,7 +308,7 @@ testdata/Internals.lc 110:55-110:56  d_
 testdata/Internals.lc 110:57-110:58  b_
 testdata/Internals.lc 111:32-111:36  Ordering->Bool
 testdata/Internals.lc 111:32-111:57  Bool
-testdata/Internals.lc 111:32-120:29  b_ -> c_->Bool
+testdata/Internals.lc 111:32-120:29  b_ -> b_->Bool
 testdata/Internals.lc 111:38-111:52  Int -> Int->Ordering
 testdata/Internals.lc 111:38-111:54  Int->Ordering
 testdata/Internals.lc 111:38-111:56  Ordering
@@ -316,7 +316,7 @@ testdata/Internals.lc 111:53-111:54  d_
 testdata/Internals.lc 111:55-111:56  b_
 testdata/Internals.lc 112:34-112:38  Ordering->Bool
 testdata/Internals.lc 112:34-112:61  Bool
-testdata/Internals.lc 112:34-120:29  b_ -> c_->Bool
+testdata/Internals.lc 112:34-120:29  b_ -> b_->Bool
 testdata/Internals.lc 112:40-112:56  Float -> Float->Ordering
 testdata/Internals.lc 112:40-112:58  Float->Ordering
 testdata/Internals.lc 112:40-112:60  Ordering
@@ -324,7 +324,7 @@ testdata/Internals.lc 112:57-112:58  d_
 testdata/Internals.lc 112:59-112:60  b_
 testdata/Internals.lc 114:20-114:24  Bool
 testdata/Internals.lc 114:20-116:19  Bool | Bool->Bool
-testdata/Internals.lc 114:20-120:29  b_ -> c_->Bool
+testdata/Internals.lc 114:20-120:29  b_ -> b_->Bool
 testdata/Internals.lc 115:22-115:26  Bool
 testdata/Internals.lc 115:22-116:19  Bool | Bool->Bool
 testdata/Internals.lc 116:14-116:19  Bool
diff --git a/testdata/Prelude.out b/testdata/Prelude.out
index 99401d65..d5d3852b 100644
--- a/testdata/Prelude.out
+++ b/testdata/Prelude.out
@@ -188,11 +188,11 @@ testdata/Prelude.lc 23:20-23:21  g_
 testdata/Prelude.lc 23:22-23:23  h_
 testdata/Prelude.lc 25:1-25:8  {a} -> {b} -> {c} -> (a -> c->b) -> (a, c)->b
 testdata/Prelude.lc 25:20-25:21  o_
-testdata/Prelude.lc 25:20-25:25  HList c_ -> c_ | c_ | c_ -> HList c_ -> c_ | d_
+testdata/Prelude.lc 25:20-25:25  HList c_ -> b_ | c_ | c_ -> HList b_ -> a_ | d_
 testdata/Prelude.lc 25:22-25:23  n_
 testdata/Prelude.lc 25:24-25:25  j_
 testdata/Prelude.lc 27:2-27:5  {a} -> {b} -> {c} -> {d} -> (a->c) -> (b->d) -> (a, b)->(c, d)
-testdata/Prelude.lc 27:20-27:30  (b_, a_) | HList c_ -> c_ | c_ -> HList c_ -> c_
+testdata/Prelude.lc 27:20-27:30  (b_, a_) | HList c_ -> b_ | c_ -> HList b_ -> a_
 testdata/Prelude.lc 27:21-27:22  s_
 testdata/Prelude.lc 27:23-27:24  p_
 testdata/Prelude.lc 27:26-27:27  r_
@@ -202,7 +202,7 @@ testdata/Prelude.lc 29:1-29:3  Float
 testdata/Prelude.lc 29:6-29:23  Float
 testdata/Prelude.lc 31:8-31:11  Type
 testdata/Prelude.lc 31:8-31:29  Type
-testdata/Prelude.lc 31:8-34:39  a_->b_ | {a} -> {b} -> List a -> List b -> List (a, b)
+testdata/Prelude.lc 31:8-34:39  a_->a_ | {a} -> {b} -> List a -> List b -> List (a, b)
 testdata/Prelude.lc 31:9-31:10  d_
 testdata/Prelude.lc 31:15-31:18  Type
 testdata/Prelude.lc 31:15-31:29  Type
@@ -214,23 +214,23 @@ testdata/Prelude.lc 31:24-31:27  List Type
 testdata/Prelude.lc 31:26-31:27  List Type | Type
 testdata/Prelude.lc 32:1-32:4  {a} -> {b} -> List a -> List b -> List (a, b)
 testdata/Prelude.lc 32:22-32:24  {a} -> List a
-testdata/Prelude.lc 32:22-34:39  List (d_, c_) | List a_ -> List (b_, e_) | List b_ -> List (d_, c_) | List b_ -> List b_ -> List (d_, c_)
+testdata/Prelude.lc 32:22-34:39  List (d_, c_) | List a_ -> List (a_, d_) | List b_ -> List (c_, b_) | List b_ -> List a_ -> List (b_, a_)
 testdata/Prelude.lc 33:22-33:24  {a} -> List a
-testdata/Prelude.lc 33:22-34:39  List (c_, f_) | List a_ -> List (f_, b_) | List c_ -> List c_ | b_ -> List c_ -> List c_
+testdata/Prelude.lc 33:22-34:39  List (c_, f_) | List a_ -> List (e_, a_) | List c_ -> List b_ | b_ -> List b_ -> List a_
 testdata/Prelude.lc 34:23-34:28  (h_, d_)
-testdata/Prelude.lc 34:23-34:29  List (h_, d_) -> List (i_, e_)
-testdata/Prelude.lc 34:23-34:39  List (g_, c_) | List c_ -> List c_ | b_ -> List c_ -> List c_
+testdata/Prelude.lc 34:23-34:29  List (h_, d_) -> List (h_, d_)
+testdata/Prelude.lc 34:23-34:39  List (g_, c_) | List c_ -> List b_ | b_ -> List b_ -> List a_
 testdata/Prelude.lc 34:24-34:25  k_
 testdata/Prelude.lc 34:26-34:27  ((d_)) | g_
 testdata/Prelude.lc 34:28-34:29  {a} -> a -> List a -> List a
 testdata/Prelude.lc 34:30-34:33  {a} -> {b} -> List a -> List b -> List (a, b)
-testdata/Prelude.lc 34:30-34:36  List a_ -> List (i_, b_)
+testdata/Prelude.lc 34:30-34:36  List a_ -> List (h_, a_)
 testdata/Prelude.lc 34:30-34:39  List (g_, c_)
 testdata/Prelude.lc 34:34-34:36  List i_
 testdata/Prelude.lc 34:37-34:39  List c_
 testdata/Prelude.lc 36:10-36:17  Type
 testdata/Prelude.lc 36:10-36:30  Type
-testdata/Prelude.lc 36:10-39:27  a_->b_ | {a} -> {b} -> List (a, b) -> (List a, List b)
+testdata/Prelude.lc 36:10-39:27  a_->a_ | {a} -> {b} -> List (a, b) -> (List a, List b)
 testdata/Prelude.lc 36:11-36:16  Type
 testdata/Prelude.lc 36:12-36:13  e_
 testdata/Prelude.lc 36:12-36:15  List Type
@@ -243,40 +243,40 @@ testdata/Prelude.lc 36:26-36:29  List Type | Type
 testdata/Prelude.lc 36:27-36:28  Type
 testdata/Prelude.lc 37:1-37:6  {a} -> {b} -> List (a, b) -> (List a, List b)
 testdata/Prelude.lc 37:12-37:19  (List b_, List a_)
-testdata/Prelude.lc 37:12-39:27  (List c_, List b_) | List (b_, a_) -> (List c_, List b_)
+testdata/Prelude.lc 37:12-39:27  (List c_, List b_) | List (b_, a_) -> (List b_, List a_)
 testdata/Prelude.lc 37:13-37:15  {a} -> List a
 testdata/Prelude.lc 37:16-37:18  ((List a_)) | {a} -> List a
 testdata/Prelude.lc 38:20-38:31  (List n_, List i_)
-testdata/Prelude.lc 38:20-39:27  (List d_, List a_) | (List d_, List c_) | (List h_, List c_) | HList c_ -> c_ | List d_ -> (List d_, List c_) | c_ -> HList c_ -> c_ | c_ -> List d_ -> (List d_, List c_)
+testdata/Prelude.lc 38:20-39:27  (List d_, List a_) | (List d_, List c_) | (List h_, List c_) | HList c_ -> b_ | List d_ -> (List c_, List b_) | c_ -> HList b_ -> a_ | c_ -> List c_ -> (List b_, List a_)
 testdata/Prelude.lc 38:21-38:22  s_
-testdata/Prelude.lc 38:21-38:23  List r_ -> List s_
+testdata/Prelude.lc 38:21-38:23  List r_ -> List r_
 testdata/Prelude.lc 38:21-38:25  List p_
 testdata/Prelude.lc 38:22-38:23  {a} -> a -> List a -> List a
 testdata/Prelude.lc 38:23-38:25  List f_
 testdata/Prelude.lc 38:26-38:27  n_
-testdata/Prelude.lc 38:26-38:28  List m_ -> List n_
+testdata/Prelude.lc 38:26-38:28  List m_ -> List m_
 testdata/Prelude.lc 38:26-38:30  ((List i_)) | List k_
 testdata/Prelude.lc 38:27-38:28  {a} -> a -> List a -> List a
 testdata/Prelude.lc 38:28-38:30  List f_
-testdata/Prelude.lc 39:10-39:12  HList c_ -> c_ | c_ -> HList c_ -> c_ | d_ | h_ | k_
+testdata/Prelude.lc 39:10-39:12  HList c_ -> b_ | c_ -> HList b_ -> a_ | d_ | h_ | k_
 testdata/Prelude.lc 39:10-39:15  (List e_, List d_) | (List f_, List e_)
-testdata/Prelude.lc 39:13-39:15  HList c_ -> c_ | c_ | c_ -> HList c_ -> c_ | f_
+testdata/Prelude.lc 39:13-39:15  HList c_ -> b_ | c_ | c_ -> HList b_ -> a_ | f_
 testdata/Prelude.lc 39:19-39:24  {a} -> {b} -> List (a, b) -> (List a, List b)
 testdata/Prelude.lc 39:19-39:27  (List b_, List a_)
 testdata/Prelude.lc 39:25-39:27  List r_
 testdata/Prelude.lc 41:1-41:7  {a} -> (a->Bool) -> List a -> List a
 testdata/Prelude.lc 41:21-41:23  {a} -> List a
-testdata/Prelude.lc 41:21-44:49  List a_ -> List b_ | a_->b_
-testdata/Prelude.lc 42:22-44:49  List c_ | List c_ -> List c_ | b_ -> List c_ -> List c_
+testdata/Prelude.lc 41:21-44:49  List a_ -> List a_ | a_->a_
+testdata/Prelude.lc 42:22-44:49  List c_ | List c_ -> List b_ | b_ -> List b_ -> List a_
 testdata/Prelude.lc 42:27-42:31  g_
 testdata/Prelude.lc 42:32-42:33  f_
-testdata/Prelude.lc 43:32-44:49  Bool -> List g_
+testdata/Prelude.lc 43:32-44:49  Bool -> List f_
 testdata/Prelude.lc 43:33-43:34  h_
-testdata/Prelude.lc 43:33-43:36  List g_ -> List h_
+testdata/Prelude.lc 43:33-43:36  List g_ -> List g_
 testdata/Prelude.lc 43:33-43:51  List f_
 testdata/Prelude.lc 43:35-43:36  {a} -> a -> List a -> List a
-testdata/Prelude.lc 43:37-43:43  j_ -> List g_ -> List h_
-testdata/Prelude.lc 43:37-43:48  List f_ -> List g_
+testdata/Prelude.lc 43:37-43:43  j_ -> List f_ -> List f_
+testdata/Prelude.lc 43:37-43:48  List f_ -> List f_
 testdata/Prelude.lc 43:37-43:51  List f_
 testdata/Prelude.lc 43:44-43:48  j_
 testdata/Prelude.lc 43:49-43:51  List f_
@@ -289,7 +289,7 @@ testdata/Prelude.lc 49:10-49:11  b_
 testdata/Prelude.lc 49:16-49:19  Type
 testdata/Prelude.lc 49:17-49:18  Type
 testdata/Prelude.lc 50:1-50:5  {a} -> List a -> List a
-testdata/Prelude.lc 50:16-50:18  List a_ -> List b_ | List b_ | List c_ -> c_ | List d_ | b_ -> List c_ -> c_
+testdata/Prelude.lc 50:16-50:18  List a_ -> List a_ | List b_ | List c_ -> b_ | List d_ | b_ -> List b_ -> a_
 testdata/Prelude.lc 52:10-52:13  Type
 testdata/Prelude.lc 52:10-52:25  Type
 testdata/Prelude.lc 52:11-52:12  b_
@@ -300,17 +300,17 @@ testdata/Prelude.lc 52:19-52:23  List Type
 testdata/Prelude.lc 52:22-52:23  List Type | Type
 testdata/Prelude.lc 53:1-53:6  {a} -> List a -> List (a, a)
 testdata/Prelude.lc 53:11-53:14  {a} -> {b} -> List a -> List b -> List (a, b)
-testdata/Prelude.lc 53:11-53:16  List a_ -> List (d_, b_)
-testdata/Prelude.lc 53:11-53:25  List (b_, b_) | List a_ -> List (b_, b_)
+testdata/Prelude.lc 53:11-53:16  List a_ -> List (c_, a_)
+testdata/Prelude.lc 53:11-53:25  List (b_, b_) | List a_ -> List (a_, a_)
 testdata/Prelude.lc 53:15-53:16  List d_
 testdata/Prelude.lc 53:18-53:22  {a} -> List a -> List a
 testdata/Prelude.lc 53:18-53:24  List b_
 testdata/Prelude.lc 53:23-53:24  List c_
 testdata/Prelude.lc 55:1-55:7  {a} -> {b} -> (a -> b->a) -> a -> List b -> a
 testdata/Prelude.lc 55:17-55:18  f_
-testdata/Prelude.lc 55:17-56:41  List b_ -> g_ | a_->b_
+testdata/Prelude.lc 55:17-56:41  List b_ -> f_ | a_->a_
 testdata/Prelude.lc 56:22-56:28  k_
-testdata/Prelude.lc 56:22-56:41  List b_ -> g_ | a_ -> List b_ -> g_
+testdata/Prelude.lc 56:22-56:41  List b_ -> f_ | a_ -> List a_ -> e_
 testdata/Prelude.lc 56:29-56:30  l_
 testdata/Prelude.lc 56:32-56:33  m_
 testdata/Prelude.lc 56:34-56:35  n_
@@ -318,60 +318,60 @@ testdata/Prelude.lc 56:36-56:37  k_
 testdata/Prelude.lc 56:39-56:41  List h_
 testdata/Prelude.lc 58:1-58:7  {a} -> (a -> a->a) -> List a -> a
 testdata/Prelude.lc 58:20-58:25  {a} -> {b} -> (b -> a->a) -> a -> List b -> a
-testdata/Prelude.lc 58:20-58:27  b_ -> List b_ -> d_
-testdata/Prelude.lc 58:20-58:29  List a_ -> f_
-testdata/Prelude.lc 58:20-58:32  List c_ -> c_ | b_ -> List c_ -> c_ | c_
+testdata/Prelude.lc 58:20-58:27  b_ -> List a_ -> b_
+testdata/Prelude.lc 58:20-58:29  List a_ -> e_
+testdata/Prelude.lc 58:20-58:32  List c_ -> b_ | b_ -> List b_ -> a_ | c_
 testdata/Prelude.lc 58:26-58:27  j_
 testdata/Prelude.lc 58:28-58:29  f_
 testdata/Prelude.lc 58:30-58:32  List d_
 testdata/Prelude.lc 60:1-60:6  {a} -> List a -> (List a, List a)
 testdata/Prelude.lc 60:12-60:20  (List b_, List a_)
-testdata/Prelude.lc 60:12-61:55  List b_ -> (List c_, List b_) | a_->b_
+testdata/Prelude.lc 60:12-61:55  List b_ -> (List b_, List a_) | a_->a_
 testdata/Prelude.lc 60:13-60:15  {a} -> List a
 testdata/Prelude.lc 60:17-60:19  ((List a_)) | {a} -> List a
 testdata/Prelude.lc 61:17-61:28  (List i_, c_)
-testdata/Prelude.lc 61:17-61:55  List d_ -> (List d_, List c_) | c_ -> List d_ -> (List d_, List c_)
+testdata/Prelude.lc 61:17-61:55  List d_ -> (List c_, List b_) | c_ -> List c_ -> (List b_, List a_)
 testdata/Prelude.lc 61:18-61:19  m_
-testdata/Prelude.lc 61:18-61:20  List l_ -> List m_
+testdata/Prelude.lc 61:18-61:20  List l_ -> List l_
 testdata/Prelude.lc 61:18-61:23  List j_
 testdata/Prelude.lc 61:19-61:20  {a} -> a -> List a -> List a
 testdata/Prelude.lc 61:21-61:23  d_
 testdata/Prelude.lc 61:25-61:27  ((c_)) | f_
-testdata/Prelude.lc 61:37-61:39  HList c_ -> c_ | c_ -> HList c_ -> c_ | d_ | h_ | k_
+testdata/Prelude.lc 61:37-61:39  HList c_ -> b_ | c_ -> HList b_ -> a_ | d_ | h_ | k_
 testdata/Prelude.lc 61:37-61:43  (e_, d_) | d_
-testdata/Prelude.lc 61:41-61:43  HList c_ -> c_ | c_ | c_ -> HList c_ -> c_ | f_
+testdata/Prelude.lc 61:41-61:43  HList c_ -> b_ | c_ | c_ -> HList b_ -> a_ | f_
 testdata/Prelude.lc 61:47-61:52  i_
 testdata/Prelude.lc 61:53-61:55  List h_
 testdata/Prelude.lc 63:1-63:8  {a} -> (a -> a->Ordering) -> List a -> List a -> List a
-testdata/Prelude.lc 63:27-65:32  List b_ -> j_ | List e_ | a_ -> List b_ -> j_
-testdata/Prelude.lc 63:27-67:21  List b_ -> e_ | List c_ | List c_ -> List d_ | a_ -> List b_ -> e_ | a_->b_
+testdata/Prelude.lc 63:27-65:32  List b_ -> i_ | List e_ | a_ -> List a_ -> h_
+testdata/Prelude.lc 63:27-67:21  List b_ -> d_ | List c_ | List c_ -> List c_ | a_ -> List a_ -> c_ | a_->a_
 testdata/Prelude.lc 63:32-63:33  j_
 testdata/Prelude.lc 63:34-63:35  h_
 testdata/Prelude.lc 63:36-63:37  i_
 testdata/Prelude.lc 64:11-64:12  j_
-testdata/Prelude.lc 64:11-64:13  List i_ -> List j_
+testdata/Prelude.lc 64:11-64:13  List i_ -> List i_
 testdata/Prelude.lc 64:11-64:33  List h_
-testdata/Prelude.lc 64:11-65:32  List g_ -> Ordering -> List i_
+testdata/Prelude.lc 64:11-65:32  List g_ -> Ordering -> List g_
 testdata/Prelude.lc 64:12-64:13  {a} -> a -> List a -> List a
 testdata/Prelude.lc 64:14-64:21  p_
 testdata/Prelude.lc 64:22-64:23  q_
 testdata/Prelude.lc 64:24-64:26  List l_
 testdata/Prelude.lc 64:28-64:29  j_
-testdata/Prelude.lc 64:28-64:30  List i_ -> List j_
+testdata/Prelude.lc 64:28-64:30  List i_ -> List i_
 testdata/Prelude.lc 64:28-64:32  List i_
 testdata/Prelude.lc 64:29-64:30  {a} -> a -> List a -> List a
 testdata/Prelude.lc 64:30-64:32  List i_
 testdata/Prelude.lc 65:10-65:11  f_ | h_
-testdata/Prelude.lc 65:10-65:12  List e_ -> List f_ | List g_ -> List h_
+testdata/Prelude.lc 65:10-65:12  List e_ -> List e_ | List g_ -> List g_
 testdata/Prelude.lc 65:10-65:32  List g_
 testdata/Prelude.lc 65:11-65:12  {a} -> a -> List a -> List a
-testdata/Prelude.lc 65:13-65:20  m_ -> List h_ -> List i_ -> List j_
-testdata/Prelude.lc 65:13-65:22  List g_ -> List h_ -> List i_
-testdata/Prelude.lc 65:13-65:29  List g_ -> List h_
+testdata/Prelude.lc 65:13-65:20  m_ -> List g_ -> List g_ -> List g_
+testdata/Prelude.lc 65:13-65:22  List g_ -> List g_ -> List g_
+testdata/Prelude.lc 65:13-65:29  List g_ -> List g_
 testdata/Prelude.lc 65:13-65:32  List g_
 testdata/Prelude.lc 65:21-65:22  m_
 testdata/Prelude.lc 65:24-65:25  h_
-testdata/Prelude.lc 65:24-65:26  List g_ -> List h_
+testdata/Prelude.lc 65:24-65:26  List g_ -> List g_
 testdata/Prelude.lc 65:24-65:28  List g_
 testdata/Prelude.lc 65:25-65:26  {a} -> a -> List a -> List a
 testdata/Prelude.lc 65:26-65:28  List g_
@@ -380,30 +380,30 @@ testdata/Prelude.lc 66:19-66:21  d_
 testdata/Prelude.lc 67:19-67:21  i_
 testdata/Prelude.lc 69:1-69:7  {a} -> (a -> a->Ordering) -> List a -> List a
 testdata/Prelude.lc 69:15-69:17  {a} -> List a
-testdata/Prelude.lc 69:15-71:71  List b_ -> List c_ | a_->b_
+testdata/Prelude.lc 69:15-71:71  List b_ -> List b_ | a_->a_
 testdata/Prelude.lc 70:16-70:19  List e_
-testdata/Prelude.lc 70:16-71:71  List b_ -> List g_ | List c_ -> List c_ | List d_ | b_ -> List c_ -> List c_
+testdata/Prelude.lc 70:16-71:71  List b_ -> List f_ | List c_ -> List b_ | List d_ | b_ -> List b_ -> List a_
 testdata/Prelude.lc 70:17-70:18  g_
 testdata/Prelude.lc 71:15-71:22  {a} -> {b} -> {c} -> (a -> c->b) -> (a, c)->b
-testdata/Prelude.lc 71:15-71:34  (List a_, List a_) -> List b_
-testdata/Prelude.lc 71:15-71:71  List b_ -> List g_ | List h_ | a_ -> List b_ -> List g_
+testdata/Prelude.lc 71:15-71:34  (List a_, List a_) -> List a_
+testdata/Prelude.lc 71:15-71:71  List b_ -> List f_ | List h_ | a_ -> List a_ -> List e_
 testdata/Prelude.lc 71:24-71:31  {a} -> (a -> a->Ordering) -> List a -> List a -> List a
-testdata/Prelude.lc 71:24-71:33  List a_ -> List b_ -> List c_
+testdata/Prelude.lc 71:24-71:33  List a_ -> List a_ -> List a_
 testdata/Prelude.lc 71:32-71:33  o_
 testdata/Prelude.lc 71:36-71:70  (List h_, List h_)
 testdata/Prelude.lc 71:37-71:43  p_
-testdata/Prelude.lc 71:37-71:49  (c_->b_) -> (e_, d_)->(d_, c_)
-testdata/Prelude.lc 71:37-71:58  (b_, b_)->(b_, b_)
-testdata/Prelude.lc 71:44-71:45  n_ -> o_->Ordering
+testdata/Prelude.lc 71:37-71:49  (c_->a_) -> (d_, c_)->(b_, a_)
+testdata/Prelude.lc 71:37-71:58  (b_, b_)->(a_, a_)
+testdata/Prelude.lc 71:44-71:45  n_ -> n_->Ordering
 testdata/Prelude.lc 71:46-71:49  {a} -> {b} -> {c} -> {d} -> (a->c) -> (b->d) -> (a, b)->(c, d)
-testdata/Prelude.lc 71:50-71:56  (k_ -> l_->Ordering) -> e_->d_
-testdata/Prelude.lc 71:50-71:58  b_->b_
-testdata/Prelude.lc 71:57-71:58  i_ -> j_->Ordering
+testdata/Prelude.lc 71:50-71:56  (k_ -> k_->Ordering) -> d_->b_
+testdata/Prelude.lc 71:50-71:58  b_->a_
+testdata/Prelude.lc 71:57-71:58  i_ -> i_->Ordering
 testdata/Prelude.lc 71:61-71:66  {a} -> List a -> (List a, List a)
 testdata/Prelude.lc 71:61-71:69  (List a_, List a_)
 testdata/Prelude.lc 71:67-71:69  k_
 testdata/Prelude.lc 73:12-73:32  Type
-testdata/Prelude.lc 73:12-74:35  a_->b_ | {a} -> (a->a) -> a -> List a
+testdata/Prelude.lc 73:12-74:35  a_->a_ | {a} -> (a->a) -> a -> List a
 testdata/Prelude.lc 73:13-73:14  b_
 testdata/Prelude.lc 73:18-73:19  Type
 testdata/Prelude.lc 73:24-73:25  Type
@@ -412,20 +412,20 @@ testdata/Prelude.lc 73:29-73:32  Type
 testdata/Prelude.lc 73:30-73:31  Type
 testdata/Prelude.lc 74:1-74:8  {a} -> (a->a) -> a -> List a
 testdata/Prelude.lc 74:16-74:17  d_
-testdata/Prelude.lc 74:16-74:19  List c_ -> List d_
-testdata/Prelude.lc 74:16-74:35  (a_->b_) -> b_ -> List c_ | List c_ | b_ -> List c_
+testdata/Prelude.lc 74:16-74:19  List c_ -> List c_
+testdata/Prelude.lc 74:16-74:35  (a_->a_) -> a_ -> List a_ | List c_ | b_ -> List b_
 testdata/Prelude.lc 74:18-74:19  {a} -> a -> List a -> List a
 testdata/Prelude.lc 74:20-74:27  {a} -> (a->a) -> a -> List a
-testdata/Prelude.lc 74:20-74:29  c_ -> List d_
+testdata/Prelude.lc 74:20-74:29  c_ -> List c_
 testdata/Prelude.lc 74:20-74:35  List c_
-testdata/Prelude.lc 74:28-74:29  d_->e_
-testdata/Prelude.lc 74:31-74:32  c_->d_
+testdata/Prelude.lc 74:28-74:29  d_->d_
+testdata/Prelude.lc 74:31-74:32  c_->c_
 testdata/Prelude.lc 74:31-74:34  c_
 testdata/Prelude.lc 74:33-74:34  c_
 testdata/Prelude.lc 76:1-76:4  {a} -> {b} -> (a, b)->a
-testdata/Prelude.lc 76:14-76:15  HList c_ -> c_ | c_ -> HList c_ -> c_ | d_ | h_ | k_
+testdata/Prelude.lc 76:14-76:15  HList c_ -> b_ | c_ -> HList b_ -> a_ | d_ | h_ | k_
 testdata/Prelude.lc 77:1-77:4  {a} -> {b} -> (a, b)->b
-testdata/Prelude.lc 77:14-77:15  HList c_ -> c_ | c_ | c_ -> HList c_ -> c_ | f_
+testdata/Prelude.lc 77:14-77:15  HList c_ -> b_ | c_ | c_ -> HList b_ -> a_ | f_
 testdata/Prelude.lc 79:7-79:10  Bool -> Bool->Bool
 testdata/Prelude.lc 79:15-79:16  c_
 testdata/Prelude.lc 79:15-80:18  Bool->Bool
@@ -441,7 +441,7 @@ testdata/Prelude.lc 122:16-122:23  RecItem | String -> Type->RecItem | Type
 testdata/Prelude.lc 122:24-122:30  Type
 testdata/Prelude.lc 122:31-122:35  Type
 testdata/Prelude.lc 124:1-124:12  RecItem->Type
-testdata/Prelude.lc 124:29-124:30  String -> Type->c_ | Type | Type->c_
+testdata/Prelude.lc 124:29-124:30  String -> Type->a_ | Type | Type->b_
 testdata/Prelude.lc 126:6-126:13  List RecItem -> Type | Type
 testdata/Prelude.lc 126:6-126:17  Type
 testdata/Prelude.lc 126:6-127:17  Type
@@ -460,9 +460,9 @@ testdata/Prelude.lc 127:42-127:44  List RecItem
 testdata/Prelude.lc 129:1-129:7  String -> Type -> List RecItem -> Type
 testdata/Prelude.lc 129:17-129:23  String->Type
 testdata/Prelude.lc 129:17-129:26  Type
-testdata/Prelude.lc 129:17-130:75  List RecItem -> Type | a_->b_
+testdata/Prelude.lc 129:17-130:75  List RecItem -> Type | a_->a_
 testdata/Prelude.lc 129:24-129:26  String
-testdata/Prelude.lc 130:34-130:75  List b_ -> Type | String -> Type->c_ | Type | Type->c_ | a_ -> List b_ -> Type
+testdata/Prelude.lc 130:34-130:75  List b_ -> Type | String -> Type->a_ | Type | Type->b_ | a_ -> List a_ -> Type
 testdata/Prelude.lc 130:37-130:38  o_
 testdata/Prelude.lc 130:37-130:41  n_->Bool
 testdata/Prelude.lc 130:37-130:44  Bool
@@ -480,17 +480,17 @@ testdata/Prelude.lc 130:71-130:72  Type
 testdata/Prelude.lc 130:73-130:75  List i_
 testdata/Prelude.lc 132:1-132:7  {a} -> {b : List Type} -> HList ('Cons a b) -> a
 testdata/Prelude.lc 132:10-132:23  {a} -> {b : List Type} -> (c:Type) -> (a -> HList b -> c) -> HList ('Cons a b) -> c
-testdata/Prelude.lc 132:10-132:25  (c_ -> HList c_ -> c_) -> HList ('Cons d_ c_) -> c_
-testdata/Prelude.lc 132:10-132:37  HList ('Cons b_ a_) -> c_
-testdata/Prelude.lc 132:27-132:36  c_ -> HList c_ -> c_
-testdata/Prelude.lc 132:35-132:36  HList c_ -> c_ | e_
+testdata/Prelude.lc 132:10-132:25  (c_ -> HList b_ -> a_) -> HList ('Cons c_ b_) -> a_
+testdata/Prelude.lc 132:10-132:37  HList ('Cons b_ a_) -> b_
+testdata/Prelude.lc 132:27-132:36  c_ -> HList b_ -> a_
+testdata/Prelude.lc 132:35-132:36  HList c_ -> b_ | e_
 testdata/Prelude.lc 133:1-133:7  {a} -> {b : List Type} -> HList ('Cons a b) -> HList b
 testdata/Prelude.lc 133:10-133:23  {a} -> {b : List Type} -> (c:Type) -> (a -> HList b -> c) -> HList ('Cons a b) -> c
-testdata/Prelude.lc 133:10-133:25  (c_ -> HList c_ -> c_) -> HList ('Cons d_ c_) -> c_
-testdata/Prelude.lc 133:10-133:37  HList ('Cons b_ a_) -> HList b_
-testdata/Prelude.lc 133:27-133:36  c_ -> HList c_ -> c_
-testdata/Prelude.lc 133:35-133:36  HList c_ -> c_ | HList d_
-testdata/Prelude.lc 136:12-138:181  a_->b_ | {a} -> {b : List RecItem} -> (c:String) -> {_ : 'isKeyC c a b} -> RecordC b -> a
+testdata/Prelude.lc 133:10-133:25  (c_ -> HList b_ -> a_) -> HList ('Cons c_ b_) -> a_
+testdata/Prelude.lc 133:10-133:37  HList ('Cons b_ a_) -> HList a_
+testdata/Prelude.lc 133:27-133:36  c_ -> HList b_ -> a_
+testdata/Prelude.lc 133:35-133:36  HList c_ -> b_ | HList d_
+testdata/Prelude.lc 136:12-138:181  a_->a_ | {a} -> {b : List RecItem} -> (c:String) -> {_ : 'isKeyC c a b} -> RecordC b -> a
 testdata/Prelude.lc 136:28-136:37  Type
 testdata/Prelude.lc 136:28-136:97  Type
 testdata/Prelude.lc 136:29-136:36  Type
@@ -513,15 +513,15 @@ testdata/Prelude.lc 137:1-137:8  {a} -> {b : List RecItem} -> (c:String) -> {_ :
 testdata/Prelude.lc 137:57-137:58  String
 testdata/Prelude.lc 137:57-137:61  String->Bool
 testdata/Prelude.lc 137:57-137:64  Bool
-testdata/Prelude.lc 137:57-138:181  (a:String) -> {_ : 'isKeyC a c_ b_} -> RecordC c_ -> e_ | HList ('map RecItem Type 'recItemType b_) -> b_ | List c_ -> c_ | RecordC c_ -> e_ | String -> Type->c_ | Type->c_ | b_ -> List c_ -> c_ | e_ | g_ | j_ | m_ | {_ : 'isKeyC a_ c_ b_} -> RecordC c_ -> e_ | {a : List RecItem} -> (b:String) -> {_ : 'isKeyC b c_ a} -> RecordC a -> e_ | {a} -> {b : List RecItem} -> (c:String) -> {_ : 'isKeyC c a b} -> RecordC b -> a
+testdata/Prelude.lc 137:57-138:181  (a:String) -> {_ : 'isKeyC a b_ a_} -> RecordC a_ -> b_ | HList ('map RecItem Type 'recItemType b_) -> a_ | List c_ -> b_ | RecordC c_ -> d_ | String -> Type->a_ | Type->b_ | b_ -> List b_ -> a_ | e_ | g_ | j_ | m_ | {_ : 'isKeyC a_ c_ b_} -> RecordC b_ -> c_ | {a : List RecItem} -> (b:String) -> {_ : 'isKeyC b a_ a} -> RecordC a -> a_ | {a} -> {b : List RecItem} -> (c:String) -> {_ : 'isKeyC c a b} -> RecordC b -> a
 testdata/Prelude.lc 137:59-137:61  {a} -> {_ : Eq a} -> a -> a->Bool
 testdata/Prelude.lc 137:62-137:64  String
 testdata/Prelude.lc 137:67-137:73  {a} -> {b : List Type} -> HList ('Cons a b) -> a
 testdata/Prelude.lc 137:67-137:129  n_
-testdata/Prelude.lc 137:67-138:181  Bool->o_
+testdata/Prelude.lc 137:67-138:181  Bool->n_
 testdata/Prelude.lc 137:75-137:87  {a} -> {b} -> a->b
-testdata/Prelude.lc 137:75-137:90  {a} -> b_->a
-testdata/Prelude.lc 137:75-137:125  a_ -> HList ('Cons r_ ('map RecItem Type 'recItemType k_))
+testdata/Prelude.lc 137:75-137:90  {a} -> a_->a
+testdata/Prelude.lc 137:75-137:125  a_ -> HList ('Cons q_ ('map RecItem Type 'recItemType j_))
 testdata/Prelude.lc 137:75-137:128  HList ('Cons n_ ('map RecItem Type 'recItemType g_))
 testdata/Prelude.lc 137:93-137:98  List Type -> Type
 testdata/Prelude.lc 137:93-137:124  Type
@@ -536,10 +536,10 @@ testdata/Prelude.lc 137:109-137:120  RecItem->Type
 testdata/Prelude.lc 137:121-137:123  List RecItem
 testdata/Prelude.lc 137:126-137:128  HList ('map RecItem Type 'recItemType d_)
 testdata/Prelude.lc 138:57-138:64  {a} -> {b : List RecItem} -> (c:String) -> {_ : 'isKeyC c a b} -> RecordC b -> a
-testdata/Prelude.lc 138:57-138:67  {a : List RecItem} -> (b:String) -> {_ : 'isKeyC b r_ a} -> RecordC a -> t_
-testdata/Prelude.lc 138:57-138:71  (a:String) -> {_ : 'isKeyC a p_ i_} -> RecordC j_ -> r_
-testdata/Prelude.lc 138:57-138:73  {_ : 'isKeyC m_ o_ h_} -> RecordC i_ -> q_
-testdata/Prelude.lc 138:57-138:103  RecordC h_ -> p_
+testdata/Prelude.lc 138:57-138:67  {a : List RecItem} -> (b:String) -> {_ : 'isKeyC b p_ a} -> RecordC a -> p_
+testdata/Prelude.lc 138:57-138:71  (a:String) -> {_ : 'isKeyC a o_ h_} -> RecordC h_ -> o_
+testdata/Prelude.lc 138:57-138:73  {_ : 'isKeyC m_ o_ h_} -> RecordC h_ -> o_
+testdata/Prelude.lc 138:57-138:103  RecordC h_ -> o_
 testdata/Prelude.lc 138:57-138:181  n_
 testdata/Prelude.lc 138:66-138:67  Type
 testdata/Prelude.lc 138:69-138:71  List k_
@@ -558,8 +558,8 @@ testdata/Prelude.lc 138:105-138:180  RecordC b_
 testdata/Prelude.lc 138:117-138:123  {a} -> {b : List Type} -> HList ('Cons a b) -> HList b
 testdata/Prelude.lc 138:117-138:179  HList ('map RecItem Type 'recItemType h_)
 testdata/Prelude.lc 138:125-138:137  {a} -> {b} -> a->b
-testdata/Prelude.lc 138:125-138:140  {a} -> b_->a
-testdata/Prelude.lc 138:125-138:175  a_ -> HList ('Cons s_ ('map RecItem Type 'recItemType l_))
+testdata/Prelude.lc 138:125-138:140  {a} -> a_->a
+testdata/Prelude.lc 138:125-138:175  a_ -> HList ('Cons r_ ('map RecItem Type 'recItemType k_))
 testdata/Prelude.lc 138:125-138:178  HList ('Cons o_ ('map RecItem Type 'recItemType h_))
 testdata/Prelude.lc 138:143-138:148  List Type -> Type
 testdata/Prelude.lc 138:143-138:174  Type
@@ -575,9 +575,9 @@ testdata/Prelude.lc 138:171-138:173  List RecItem
 testdata/Prelude.lc 138:176-138:178  HList ('map RecItem Type 'recItemType e_)
 testdata/Prelude.lc 142:1-142:4  Float -> Float -> Float -> VecS Float 4
 testdata/Prelude.lc 142:13-142:15  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 142:13-142:17  f_ -> g_ -> h_ -> VecS i_ 4
-testdata/Prelude.lc 142:13-142:19  e_ -> f_ -> VecS g_ 4
-testdata/Prelude.lc 142:13-142:21  d_ -> VecS e_ 4
+testdata/Prelude.lc 142:13-142:17  f_ -> f_ -> f_ -> VecS f_ 4
+testdata/Prelude.lc 142:13-142:19  e_ -> e_ -> VecS e_ 4
+testdata/Prelude.lc 142:13-142:21  d_ -> VecS d_ 4
 testdata/Prelude.lc 142:13-142:25  VecS Float 4
 testdata/Prelude.lc 142:16-142:17  g_
 testdata/Prelude.lc 142:18-142:19  d_
@@ -906,31 +906,31 @@ testdata/Prelude.lc 263:1-263:16  {a:Nat} -> VecScalar a Word -> VecScalar a Flo
 testdata/Prelude.lc 263:19-263:38  {a:Nat} -> VecScalar a Word -> VecScalar a Float
 testdata/Prelude.lc 281:3-281:4  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
 testdata/Prelude.lc 281:9-281:16  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
-testdata/Prelude.lc 281:9-281:18  e_->f_
+testdata/Prelude.lc 281:9-281:18  e_->e_
 testdata/Prelude.lc 281:9-281:20  d_
 testdata/Prelude.lc 281:17-281:18  f_
 testdata/Prelude.lc 281:19-281:20  c_
 testdata/Prelude.lc 282:3-282:4  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
 testdata/Prelude.lc 282:9-282:16  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
-testdata/Prelude.lc 282:9-282:18  e_->f_
+testdata/Prelude.lc 282:9-282:18  e_->e_
 testdata/Prelude.lc 282:9-282:20  d_
 testdata/Prelude.lc 282:17-282:18  f_
 testdata/Prelude.lc 282:19-282:20  c_
 testdata/Prelude.lc 283:3-283:4  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
 testdata/Prelude.lc 283:9-283:16  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
-testdata/Prelude.lc 283:9-283:18  e_->f_
+testdata/Prelude.lc 283:9-283:18  e_->e_
 testdata/Prelude.lc 283:9-283:20  d_
 testdata/Prelude.lc 283:17-283:18  f_
 testdata/Prelude.lc 283:19-283:20  c_
 testdata/Prelude.lc 284:3-284:4  {a} -> {b:Nat} -> {_ : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b a
 testdata/Prelude.lc 284:9-284:16  {a} -> {b} -> {c:Nat} -> {_ : Num a} -> {_ : b ~ VecScalar c a} -> b -> b->b
-testdata/Prelude.lc 284:9-284:18  VecScalar b_ c_ -> VecScalar c_ d_
+testdata/Prelude.lc 284:9-284:18  VecScalar b_ c_ -> VecScalar b_ c_
 testdata/Prelude.lc 284:9-284:20  VecScalar b_ c_
 testdata/Prelude.lc 284:17-284:18  g_
 testdata/Prelude.lc 284:19-284:20  e_
 testdata/Prelude.lc 285:3-285:4  {a} -> {b:Nat} -> {_ : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b a
 testdata/Prelude.lc 285:9-285:16  {a} -> {b} -> {c:Nat} -> {_ : Num a} -> {_ : b ~ VecScalar c a} -> b -> b->b
-testdata/Prelude.lc 285:9-285:18  VecScalar b_ c_ -> VecScalar c_ d_
+testdata/Prelude.lc 285:9-285:18  VecScalar b_ c_ -> VecScalar b_ c_
 testdata/Prelude.lc 285:9-285:20  VecScalar b_ c_
 testdata/Prelude.lc 285:17-285:18  g_
 testdata/Prelude.lc 285:19-285:20  e_
@@ -946,25 +946,25 @@ testdata/Prelude.lc 291:23-291:24  e_
 testdata/Prelude.lc 291:25-291:26  b_
 testdata/Prelude.lc 292:3-292:4  {a:Nat} -> {b} -> {_ : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/Prelude.lc 292:9-292:21  {a} -> {b:Nat} -> {c} -> {d} -> {_ : Num c} -> {_ : a ~ VecScalar b c} -> {_ : d ~ VecScalar b Bool} -> a -> a->d
-testdata/Prelude.lc 292:9-292:23  VecScalar c_ b_ -> VecScalar d_ Bool
+testdata/Prelude.lc 292:9-292:23  VecScalar c_ b_ -> VecScalar c_ Bool
 testdata/Prelude.lc 292:9-292:25  VecScalar c_ Bool
 testdata/Prelude.lc 292:22-292:23  g_
 testdata/Prelude.lc 292:24-292:25  e_
 testdata/Prelude.lc 293:3-293:5  {a:Nat} -> {b} -> {_ : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/Prelude.lc 293:10-293:27  {a} -> {b:Nat} -> {c} -> {d} -> {_ : Num c} -> {_ : a ~ VecScalar b c} -> {_ : d ~ VecScalar b Bool} -> a -> a->d
-testdata/Prelude.lc 293:10-293:29  VecScalar c_ b_ -> VecScalar d_ Bool
+testdata/Prelude.lc 293:10-293:29  VecScalar c_ b_ -> VecScalar c_ Bool
 testdata/Prelude.lc 293:10-293:31  VecScalar c_ Bool
 testdata/Prelude.lc 293:28-293:29  g_
 testdata/Prelude.lc 293:30-293:31  e_
 testdata/Prelude.lc 294:3-294:5  {a:Nat} -> {b} -> {_ : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/Prelude.lc 294:10-294:30  {a} -> {b:Nat} -> {c} -> {d} -> {_ : Num c} -> {_ : a ~ VecScalar b c} -> {_ : d ~ VecScalar b Bool} -> a -> a->d
-testdata/Prelude.lc 294:10-294:32  VecScalar c_ b_ -> VecScalar d_ Bool
+testdata/Prelude.lc 294:10-294:32  VecScalar c_ b_ -> VecScalar c_ Bool
 testdata/Prelude.lc 294:10-294:34  VecScalar c_ Bool
 testdata/Prelude.lc 294:31-294:32  g_
 testdata/Prelude.lc 294:33-294:34  e_
 testdata/Prelude.lc 295:3-295:4  {a:Nat} -> {b} -> {_ : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/Prelude.lc 295:9-295:24  {a} -> {b:Nat} -> {c} -> {d} -> {_ : Num c} -> {_ : a ~ VecScalar b c} -> {_ : d ~ VecScalar b Bool} -> a -> a->d
-testdata/Prelude.lc 295:9-295:26  VecScalar c_ b_ -> VecScalar d_ Bool
+testdata/Prelude.lc 295:9-295:26  VecScalar c_ b_ -> VecScalar c_ Bool
 testdata/Prelude.lc 295:9-295:28  VecScalar c_ Bool
 testdata/Prelude.lc 295:25-295:26  g_
 testdata/Prelude.lc 295:27-295:28  e_
@@ -996,49 +996,49 @@ testdata/Prelude.lc 303:9-303:18  Bool
 testdata/Prelude.lc 303:17-303:18  c_
 testdata/Prelude.lc 306:3-306:6  {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c
 testdata/Prelude.lc 306:11-306:24  {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c
-testdata/Prelude.lc 306:11-306:26  Mat c_ a_ b_ -> Mat e_ b_ c_
+testdata/Prelude.lc 306:11-306:26  Mat c_ a_ b_ -> Mat d_ a_ b_
 testdata/Prelude.lc 306:11-306:28  Mat d_ a_ b_
 testdata/Prelude.lc 306:25-306:26  h_
 testdata/Prelude.lc 306:27-306:28  f_
 testdata/Prelude.lc 307:3-307:5  {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> VecS c b -> Vec a c
 testdata/Prelude.lc 307:10-307:23  {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Vec b c -> Vec a c
-testdata/Prelude.lc 307:10-307:25  Vec b_ a_ -> Vec d_ b_
+testdata/Prelude.lc 307:10-307:25  Vec b_ a_ -> Vec c_ a_
 testdata/Prelude.lc 307:10-307:27  Vec c_ a_
 testdata/Prelude.lc 307:24-307:25  g_
 testdata/Prelude.lc 307:26-307:27  e_
 testdata/Prelude.lc 308:3-308:5  {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> Mat a c b -> Vec c b
 testdata/Prelude.lc 308:10-308:23  {a:Nat} -> {b} -> {c:Nat} -> Vec a b -> Mat a c b -> Vec c b
-testdata/Prelude.lc 308:10-308:25  Mat c_ a_ b_ -> Vec b_ c_
+testdata/Prelude.lc 308:10-308:25  Mat c_ a_ b_ -> Vec a_ b_
 testdata/Prelude.lc 308:10-308:27  Vec a_ b_
 testdata/Prelude.lc 308:24-308:25  g_
 testdata/Prelude.lc 308:26-308:27  e_
 testdata/Prelude.lc 315:3-315:5  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> MatVecScalarElem a -> a
 testdata/Prelude.lc 315:10-315:18  {a} -> {b} -> {_ : a ~ MatVecScalarElem b} -> {_ : Num a} -> b -> a->b
-testdata/Prelude.lc 315:10-315:20  MatVecScalarElem e_ -> f_
+testdata/Prelude.lc 315:10-315:20  MatVecScalarElem e_ -> e_
 testdata/Prelude.lc 315:10-315:22  d_
 testdata/Prelude.lc 315:19-315:20  f_
 testdata/Prelude.lc 315:21-315:22  c_
 testdata/Prelude.lc 316:3-316:5  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> MatVecScalarElem a -> a
 testdata/Prelude.lc 316:10-316:18  {a} -> {b} -> {_ : a ~ MatVecScalarElem b} -> {_ : Num a} -> b -> a->b
-testdata/Prelude.lc 316:10-316:20  MatVecScalarElem e_ -> f_
+testdata/Prelude.lc 316:10-316:20  MatVecScalarElem e_ -> e_
 testdata/Prelude.lc 316:10-316:22  d_
 testdata/Prelude.lc 316:19-316:20  f_
 testdata/Prelude.lc 316:21-316:22  c_
 testdata/Prelude.lc 317:3-317:5  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> MatVecScalarElem a -> a
 testdata/Prelude.lc 317:10-317:18  {a} -> {b} -> {_ : a ~ MatVecScalarElem b} -> {_ : Num a} -> b -> a->b
-testdata/Prelude.lc 317:10-317:20  MatVecScalarElem e_ -> f_
+testdata/Prelude.lc 317:10-317:20  MatVecScalarElem e_ -> e_
 testdata/Prelude.lc 317:10-317:22  d_
 testdata/Prelude.lc 317:19-317:20  f_
 testdata/Prelude.lc 317:21-317:22  c_
 testdata/Prelude.lc 318:3-318:5  {a} -> {b:Nat} -> {_ : Num a} -> VecScalar b a -> a -> VecScalar b a
 testdata/Prelude.lc 318:10-318:18  {a} -> {b} -> {c:Nat} -> {_ : Num a} -> {_ : b ~ VecScalar c a} -> b -> a->b
-testdata/Prelude.lc 318:10-318:20  c_ -> VecScalar c_ d_
+testdata/Prelude.lc 318:10-318:20  c_ -> VecScalar b_ c_
 testdata/Prelude.lc 318:10-318:22  VecScalar b_ d_
 testdata/Prelude.lc 318:19-318:20  g_
 testdata/Prelude.lc 318:21-318:22  e_
 testdata/Prelude.lc 319:3-319:5  {a} -> {b:Nat} -> {_ : Num a} -> VecScalar b a -> a -> VecScalar b a
 testdata/Prelude.lc 319:10-319:18  {a} -> {b} -> {c:Nat} -> {_ : Num a} -> {_ : b ~ VecScalar c a} -> b -> a->b
-testdata/Prelude.lc 319:10-319:20  c_ -> VecScalar c_ d_
+testdata/Prelude.lc 319:10-319:20  c_ -> VecScalar b_ c_
 testdata/Prelude.lc 319:10-319:22  VecScalar b_ d_
 testdata/Prelude.lc 319:19-319:20  g_
 testdata/Prelude.lc 319:21-319:22  e_
@@ -1069,7 +1069,7 @@ testdata/Prelude.lc 332:11-332:29  Float -> Float -> VecS Float 4
 testdata/Prelude.lc 332:11-332:43  Float -> VecS Float 4
 testdata/Prelude.lc 332:11-332:58  VecS Float 4
 testdata/Prelude.lc 332:15-332:16  b_
-testdata/Prelude.lc 332:15-332:17  c_->d_
+testdata/Prelude.lc 332:15-332:17  c_->c_
 testdata/Prelude.lc 332:15-332:18  VecScalar 1 Float
 testdata/Prelude.lc 332:15-332:19  VecScalar 1 Float -> VecScalar 1 Float
 testdata/Prelude.lc 332:15-332:24  VecScalar 1 Float
@@ -1085,13 +1085,13 @@ testdata/Prelude.lc 332:28-332:29  b_
 testdata/Prelude.lc 332:42-332:43  b_
 testdata/Prelude.lc 332:57-332:58  b_
 testdata/Prelude.lc 333:11-333:13  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 333:11-333:15  b_ -> c_ -> d_ -> VecS e_ 4
+testdata/Prelude.lc 333:11-333:15  b_ -> b_ -> b_ -> VecS b_ 4
 testdata/Prelude.lc 333:11-333:39  Float -> Float -> VecS Float 4
 testdata/Prelude.lc 333:11-333:43  Float -> VecS Float 4
 testdata/Prelude.lc 333:11-333:58  VecS Float 4
 testdata/Prelude.lc 333:14-333:15  b_
 testdata/Prelude.lc 333:29-333:30  b_
-testdata/Prelude.lc 333:29-333:31  c_->d_
+testdata/Prelude.lc 333:29-333:31  c_->c_
 testdata/Prelude.lc 333:29-333:32  VecScalar 1 Float
 testdata/Prelude.lc 333:29-333:33  VecScalar 1 Float -> VecScalar 1 Float
 testdata/Prelude.lc 333:29-333:38  VecScalar 1 Float
@@ -1155,8 +1155,8 @@ testdata/Prelude.lc 334:58-334:59  {a} -> {_ : Num (MatVecScalarElem a)} -> a ->
 testdata/Prelude.lc 334:58-334:60  Float
 testdata/Prelude.lc 334:59-334:60  b_
 testdata/Prelude.lc 335:11-335:13  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 335:11-335:15  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 335:11-335:29  c_ -> d_ -> VecS e_ 4
+testdata/Prelude.lc 335:11-335:15  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 335:11-335:29  c_ -> c_ -> VecS c_ 4
 testdata/Prelude.lc 335:11-335:56  Float -> VecS Float 4
 testdata/Prelude.lc 335:11-335:58  VecS Float 4
 testdata/Prelude.lc 335:14-335:15  b_
@@ -1164,7 +1164,7 @@ testdata/Prelude.lc 335:28-335:29  b_
 testdata/Prelude.lc 335:43-335:44  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
 testdata/Prelude.lc 335:43-335:55  Float
 testdata/Prelude.lc 335:44-335:45  b_
-testdata/Prelude.lc 335:44-335:46  c_->d_
+testdata/Prelude.lc 335:44-335:46  c_->c_
 testdata/Prelude.lc 335:44-335:47  Float
 testdata/Prelude.lc 335:44-335:48  Float->Float
 testdata/Prelude.lc 335:44-335:49  Float
@@ -1210,9 +1210,9 @@ testdata/Prelude.lc 342:16-342:49  Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
 testdata/Prelude.lc 342:16-342:62  Vec 4 Float -> Mat 4 4 Float
 testdata/Prelude.lc 342:16-342:75  Mat 4 4 Float
 testdata/Prelude.lc 342:22-342:24  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 342:22-342:26  VecScalar c_ Float -> VecScalar d_ Float -> VecScalar e_ Float -> VecS (VecScalar f_ Float) 4
-testdata/Prelude.lc 342:22-342:28  VecScalar c_ Float -> VecScalar d_ Float -> VecS (VecScalar e_ Float) 4
-testdata/Prelude.lc 342:22-342:30  VecScalar d_ Float -> VecS (VecScalar e_ Float) 4
+testdata/Prelude.lc 342:22-342:26  VecScalar c_ Float -> VecScalar c_ Float -> VecScalar c_ Float -> VecS (VecScalar c_ Float) 4
+testdata/Prelude.lc 342:22-342:28  VecScalar c_ Float -> VecScalar c_ Float -> VecS (VecScalar c_ Float) 4
+testdata/Prelude.lc 342:22-342:30  VecScalar d_ Float -> VecS (VecScalar d_ Float) 4
 testdata/Prelude.lc 342:22-342:32  VecS (VecScalar 1 Float) 4
 testdata/Prelude.lc 342:25-342:26  VecScalar d_ Float
 testdata/Prelude.lc 342:27-342:28  VecScalar c_ Float
@@ -1230,18 +1230,18 @@ testdata/Prelude.lc 342:43-342:44  VecScalar 1 Float
 testdata/Prelude.lc 342:45-342:46  b_
 testdata/Prelude.lc 342:47-342:48  b_
 testdata/Prelude.lc 342:51-342:53  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 342:51-342:55  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 342:51-342:57  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 342:51-342:59  c_ -> VecS d_ 4
+testdata/Prelude.lc 342:51-342:55  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 342:51-342:57  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 342:51-342:59  c_ -> VecS c_ 4
 testdata/Prelude.lc 342:51-342:61  VecS Float 4
 testdata/Prelude.lc 342:54-342:55  b_
 testdata/Prelude.lc 342:56-342:57  b_
 testdata/Prelude.lc 342:58-342:59  b_
 testdata/Prelude.lc 342:60-342:61  b_
 testdata/Prelude.lc 342:64-342:66  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 342:64-342:68  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 342:64-342:70  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 342:64-342:72  c_ -> VecS d_ 4
+testdata/Prelude.lc 342:64-342:68  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 342:64-342:70  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 342:64-342:72  c_ -> VecS c_ 4
 testdata/Prelude.lc 342:64-342:74  VecS Float 4
 testdata/Prelude.lc 342:67-342:68  b_
 testdata/Prelude.lc 342:69-342:70  b_
@@ -1260,9 +1260,9 @@ testdata/Prelude.lc 347:16-347:49  Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
 testdata/Prelude.lc 347:16-347:62  Vec 4 Float -> Mat 4 4 Float
 testdata/Prelude.lc 347:16-347:75  Mat 4 4 Float
 testdata/Prelude.lc 347:22-347:24  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 347:22-347:26  VecScalar c_ Float -> VecScalar d_ Float -> VecScalar e_ Float -> VecS (VecScalar f_ Float) 4
-testdata/Prelude.lc 347:22-347:28  VecScalar d_ Float -> VecScalar e_ Float -> VecS (VecScalar f_ Float) 4
-testdata/Prelude.lc 347:22-347:33  VecScalar f_ Float -> VecS (VecScalar g_ Float) 4
+testdata/Prelude.lc 347:22-347:26  VecScalar c_ Float -> VecScalar c_ Float -> VecScalar c_ Float -> VecS (VecScalar c_ Float) 4
+testdata/Prelude.lc 347:22-347:28  VecScalar d_ Float -> VecScalar d_ Float -> VecS (VecScalar d_ Float) 4
+testdata/Prelude.lc 347:22-347:33  VecScalar f_ Float -> VecS (VecScalar f_ Float) 4
 testdata/Prelude.lc 347:22-347:35  VecS (VecScalar 1 Float) 4
 testdata/Prelude.lc 347:25-347:26  VecScalar d_ Float
 testdata/Prelude.lc 347:27-347:28  b_
@@ -1271,9 +1271,9 @@ testdata/Prelude.lc 347:30-347:32  VecScalar f_ Float
 testdata/Prelude.lc 347:31-347:32  VecScalar f_ Float
 testdata/Prelude.lc 347:34-347:35  b_
 testdata/Prelude.lc 347:38-347:40  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 347:38-347:42  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 347:38-347:44  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 347:38-347:46  c_ -> VecS d_ 4
+testdata/Prelude.lc 347:38-347:42  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 347:38-347:44  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 347:38-347:46  c_ -> VecS c_ 4
 testdata/Prelude.lc 347:38-347:48  VecS Float 4
 testdata/Prelude.lc 347:41-347:42  b_
 testdata/Prelude.lc 347:43-347:44  b_
@@ -1289,9 +1289,9 @@ testdata/Prelude.lc 347:56-347:57  b_
 testdata/Prelude.lc 347:58-347:59  VecScalar 1 Float
 testdata/Prelude.lc 347:60-347:61  b_
 testdata/Prelude.lc 347:64-347:66  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 347:64-347:68  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 347:64-347:70  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 347:64-347:72  c_ -> VecS d_ 4
+testdata/Prelude.lc 347:64-347:68  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 347:64-347:70  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 347:64-347:72  c_ -> VecS c_ 4
 testdata/Prelude.lc 347:64-347:74  VecS Float 4
 testdata/Prelude.lc 347:67-347:68  b_
 testdata/Prelude.lc 347:69-347:70  b_
@@ -1310,25 +1310,25 @@ testdata/Prelude.lc 352:16-352:46  Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
 testdata/Prelude.lc 352:16-352:62  Vec 4 Float -> Mat 4 4 Float
 testdata/Prelude.lc 352:16-352:75  Mat 4 4 Float
 testdata/Prelude.lc 352:22-352:24  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 352:22-352:26  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 352:22-352:28  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 352:22-352:30  c_ -> VecS d_ 4
+testdata/Prelude.lc 352:22-352:26  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 352:22-352:28  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 352:22-352:30  c_ -> VecS c_ 4
 testdata/Prelude.lc 352:22-352:32  VecS Float 4
 testdata/Prelude.lc 352:25-352:26  b_
 testdata/Prelude.lc 352:27-352:28  b_
 testdata/Prelude.lc 352:29-352:30  b_
 testdata/Prelude.lc 352:31-352:32  b_
 testdata/Prelude.lc 352:35-352:37  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 352:35-352:39  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 352:35-352:41  VecScalar d_ Float -> VecScalar e_ Float -> VecS (VecScalar f_ Float) 4
-testdata/Prelude.lc 352:35-352:43  VecScalar d_ Float -> VecS (VecScalar e_ Float) 4
+testdata/Prelude.lc 352:35-352:39  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 352:35-352:41  VecScalar d_ Float -> VecScalar d_ Float -> VecS (VecScalar d_ Float) 4
+testdata/Prelude.lc 352:35-352:43  VecScalar d_ Float -> VecS (VecScalar d_ Float) 4
 testdata/Prelude.lc 352:35-352:45  VecS (VecScalar 1 Float) 4
 testdata/Prelude.lc 352:38-352:39  b_
 testdata/Prelude.lc 352:40-352:41  VecScalar e_ Float
 testdata/Prelude.lc 352:42-352:43  VecScalar d_ Float
 testdata/Prelude.lc 352:44-352:45  b_
 testdata/Prelude.lc 352:48-352:50  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 352:48-352:52  b_ -> c_ -> d_ -> VecS e_ 4
+testdata/Prelude.lc 352:48-352:52  b_ -> b_ -> b_ -> VecS b_ 4
 testdata/Prelude.lc 352:48-352:57  Float -> Float -> VecS Float 4
 testdata/Prelude.lc 352:48-352:59  Float -> VecS Float 4
 testdata/Prelude.lc 352:48-352:61  VecS Float 4
@@ -1339,9 +1339,9 @@ testdata/Prelude.lc 352:55-352:56  VecScalar 1 Float
 testdata/Prelude.lc 352:58-352:59  VecScalar 1 Float
 testdata/Prelude.lc 352:60-352:61  b_
 testdata/Prelude.lc 352:64-352:66  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 352:64-352:68  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 352:64-352:70  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 352:64-352:72  c_ -> VecS d_ 4
+testdata/Prelude.lc 352:64-352:68  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 352:64-352:70  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 352:64-352:72  c_ -> VecS c_ 4
 testdata/Prelude.lc 352:64-352:74  VecS Float 4
 testdata/Prelude.lc 352:67-352:68  b_
 testdata/Prelude.lc 352:69-352:70  b_
@@ -1356,9 +1356,9 @@ testdata/Prelude.lc 355:13-355:14  VecScalar c_ Float
 testdata/Prelude.lc 357:1-357:14  Float -> Float -> Float -> Mat 4 4 Float
 testdata/Prelude.lc 357:23-357:33  VecScalar 1 Float -> Mat 4 4 Float
 testdata/Prelude.lc 357:23-357:35  Mat 4 4 Float
-testdata/Prelude.lc 357:23-357:39  Mat 4 a_ Float -> Mat 4 b_ Float
+testdata/Prelude.lc 357:23-357:39  Mat 4 a_ Float -> Mat 4 a_ Float
 testdata/Prelude.lc 357:23-357:52  Mat 4 4 Float
-testdata/Prelude.lc 357:23-357:56  Mat 4 a_ Float -> Mat 4 b_ Float
+testdata/Prelude.lc 357:23-357:56  Mat 4 a_ Float -> Mat 4 a_ Float
 testdata/Prelude.lc 357:23-357:69  Mat 4 4 Float
 testdata/Prelude.lc 357:34-357:35  k_
 testdata/Prelude.lc 357:36-357:39  {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c
@@ -1393,27 +1393,27 @@ testdata/Prelude.lc 360:30-360:32  {a} -> {_ : Num a} -> VecS a 4
 testdata/Prelude.lc 360:33-360:35  {a} -> {_ : Num a} -> VecS a 4
 testdata/Prelude.lc 360:36-360:38  VecS Float 4
 testdata/Prelude.lc 362:9-362:11  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 362:9-362:13  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 362:9-362:15  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 362:9-362:17  c_ -> VecS d_ 4
+testdata/Prelude.lc 362:9-362:13  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 362:9-362:15  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 362:9-362:17  c_ -> VecS c_ 4
 testdata/Prelude.lc 362:9-362:19  VecS c_ 4
 testdata/Prelude.lc 362:12-362:13  b_
 testdata/Prelude.lc 362:14-362:15  b_
 testdata/Prelude.lc 362:16-362:17  b_
 testdata/Prelude.lc 362:18-362:19  b_
 testdata/Prelude.lc 363:9-363:11  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 363:9-363:13  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 363:9-363:15  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 363:9-363:17  c_ -> VecS d_ 4
+testdata/Prelude.lc 363:9-363:13  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 363:9-363:15  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 363:9-363:17  c_ -> VecS c_ 4
 testdata/Prelude.lc 363:9-363:19  VecS c_ 4
 testdata/Prelude.lc 363:12-363:13  b_
 testdata/Prelude.lc 363:14-363:15  b_
 testdata/Prelude.lc 363:16-363:17  b_
 testdata/Prelude.lc 363:18-363:19  b_
 testdata/Prelude.lc 364:9-364:11  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 364:9-364:13  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 364:9-364:15  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 364:9-364:17  c_ -> VecS d_ 4
+testdata/Prelude.lc 364:9-364:13  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 364:9-364:15  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 364:9-364:17  c_ -> VecS c_ 4
 testdata/Prelude.lc 364:9-364:19  VecS c_ 4
 testdata/Prelude.lc 364:12-364:13  b_
 testdata/Prelude.lc 364:14-364:15  b_
@@ -1457,7 +1457,7 @@ testdata/Prelude.lc 371:17-371:18  b_
 testdata/Prelude.lc 371:19-371:24  Type
 testdata/Prelude.lc 372:1-372:7  Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 4 4 Float
 testdata/Prelude.lc 372:24-372:25  Mat 4 4 Float
-testdata/Prelude.lc 372:24-372:29  Mat 4 a_ Float -> Mat 4 b_ Float
+testdata/Prelude.lc 372:24-372:29  Mat 4 a_ Float -> Mat 4 a_ Float
 testdata/Prelude.lc 372:24-372:56  Mat 4 4 Float
 testdata/Prelude.lc 372:24-378:65  Vec 3 Float -> Mat 4 4 Float | Vec 3 Float -> Vec 3 Float -> Mat 4 4 Float | Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 4 4 Float
 testdata/Prelude.lc 372:26-372:29  {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c
@@ -1467,9 +1467,9 @@ testdata/Prelude.lc 372:48-372:51  {a} -> {_ : Signed (MatVecScalarElem a)} -> a
 testdata/Prelude.lc 372:48-372:55  VecS Float 3
 testdata/Prelude.lc 372:52-372:55  Vec 3 Float
 testdata/Prelude.lc 374:14-374:16  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 374:14-374:20  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 374:14-374:24  b_ -> c_ -> VecS d_ 4
-testdata/Prelude.lc 374:14-374:28  b_ -> VecS c_ 4
+testdata/Prelude.lc 374:14-374:20  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 374:14-374:24  b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 374:14-374:28  b_ -> VecS b_ 4
 testdata/Prelude.lc 374:14-374:30  VecS c_ 4
 testdata/Prelude.lc 374:17-374:18  e_
 testdata/Prelude.lc 374:17-374:20  b_
@@ -1479,7 +1479,7 @@ testdata/Prelude.lc 374:25-374:26  VecS d_ c_
 testdata/Prelude.lc 374:25-374:28  b_
 testdata/Prelude.lc 374:29-374:30  b_
 testdata/Prelude.lc 375:9-375:18  {a} -> {b:Nat} -> {_ : a ~ VecScalar b Float} -> a->a
-testdata/Prelude.lc 375:9-375:20  VecScalar a_ Float -> VecScalar b_ Float
+testdata/Prelude.lc 375:9-375:20  VecScalar a_ Float -> VecScalar a_ Float
 testdata/Prelude.lc 375:9-375:33  VecScalar 3 Float
 testdata/Prelude.lc 375:19-375:20  {a} -> {b} -> (a->b) -> a->b
 testdata/Prelude.lc 375:21-375:24  Vec 3 Float
@@ -1488,7 +1488,7 @@ testdata/Prelude.lc 375:21-375:33  VecS Float 3
 testdata/Prelude.lc 375:25-375:26  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
 testdata/Prelude.lc 375:27-375:33  Vec 3 Float
 testdata/Prelude.lc 376:9-376:18  {a} -> {b:Nat} -> {_ : a ~ VecScalar b Float} -> a->a
-testdata/Prelude.lc 376:9-376:20  VecScalar a_ Float -> VecScalar b_ Float
+testdata/Prelude.lc 376:9-376:20  VecScalar a_ Float -> VecScalar a_ Float
 testdata/Prelude.lc 376:9-376:33  VecScalar 3 Float
 testdata/Prelude.lc 376:19-376:20  {a} -> {b} -> (a->b) -> a->b
 testdata/Prelude.lc 376:21-376:23  Vec 3 Float
@@ -1502,7 +1502,7 @@ testdata/Prelude.lc 377:9-377:20  VecS Float 3
 testdata/Prelude.lc 377:11-377:18  {a} -> {_ : a ~ VecS Float 3} -> a -> a->a
 testdata/Prelude.lc 377:19-377:20  VecScalar 3 Float
 testdata/Prelude.lc 378:9-378:18  {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Mat b a c
-testdata/Prelude.lc 378:9-378:20  Mat c_ b_ a_ -> Mat c_ d_ b_
+testdata/Prelude.lc 378:9-378:20  Mat c_ b_ a_ -> Mat b_ c_ a_
 testdata/Prelude.lc 378:9-378:65  Mat 4 4 Float
 testdata/Prelude.lc 378:19-378:20  {a} -> {b} -> (a->b) -> a->b
 testdata/Prelude.lc 378:21-378:25  Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
@@ -1520,9 +1520,9 @@ testdata/Prelude.lc 378:45-378:49  {a} -> {b:Nat} -> {_ : Num a} -> VecS a b ->
 testdata/Prelude.lc 378:45-378:51  VecS Float 4
 testdata/Prelude.lc 378:50-378:51  VecScalar 3 Float
 testdata/Prelude.lc 378:54-378:56  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 378:54-378:58  b_ -> c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 378:54-378:60  c_ -> d_ -> VecS e_ 4
-testdata/Prelude.lc 378:54-378:62  c_ -> VecS d_ 4
+testdata/Prelude.lc 378:54-378:58  b_ -> b_ -> b_ -> VecS b_ 4
+testdata/Prelude.lc 378:54-378:60  c_ -> c_ -> VecS c_ 4
+testdata/Prelude.lc 378:54-378:62  c_ -> VecS c_ 4
 testdata/Prelude.lc 378:54-378:64  VecS Float 4
 testdata/Prelude.lc 378:57-378:58  b_
 testdata/Prelude.lc 378:59-378:60  b_
@@ -1530,20 +1530,20 @@ testdata/Prelude.lc 378:61-378:62  b_
 testdata/Prelude.lc 378:63-378:64  b_
 testdata/Prelude.lc 380:1-380:6  Float -> VecS Float 4 -> VecS Float 4
 testdata/Prelude.lc 380:13-380:14  d_
-testdata/Prelude.lc 380:13-380:16  c_->d_
+testdata/Prelude.lc 380:13-380:16  c_->c_
 testdata/Prelude.lc 380:13-380:29  VecS Float 4
 testdata/Prelude.lc 380:15-380:16  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
 testdata/Prelude.lc 380:17-380:19  {a} -> a -> a -> a -> a -> VecS a 4
-testdata/Prelude.lc 380:17-380:21  e_ -> f_ -> g_ -> VecS h_ 4
-testdata/Prelude.lc 380:17-380:23  e_ -> f_ -> VecS g_ 4
-testdata/Prelude.lc 380:17-380:25  e_ -> VecS f_ 4
+testdata/Prelude.lc 380:17-380:21  e_ -> e_ -> e_ -> VecS e_ 4
+testdata/Prelude.lc 380:17-380:23  e_ -> e_ -> VecS e_ 4
+testdata/Prelude.lc 380:17-380:25  e_ -> VecS e_ 4
 testdata/Prelude.lc 380:17-380:29  VecS Float 4
 testdata/Prelude.lc 380:20-380:21  f_
 testdata/Prelude.lc 380:22-380:23  e_
 testdata/Prelude.lc 380:24-380:25  e_
 testdata/Prelude.lc 380:26-380:29  Float
 testdata/Prelude.lc 382:11-382:16  Type
-testdata/Prelude.lc 382:11-385:38  Float -> Float -> List Float | a_->b_
+testdata/Prelude.lc 382:11-385:38  Float -> Float -> List Float | a_->a_
 testdata/Prelude.lc 382:20-382:25  Type
 testdata/Prelude.lc 382:20-382:36  Type
 testdata/Prelude.lc 382:29-382:36  Type
@@ -1572,16 +1572,16 @@ testdata/Prelude.lc 385:34-385:35  b_
 testdata/Prelude.lc 385:37-385:38  Float
 testdata/Prelude.lc 387:9-387:12  Type
 testdata/Prelude.lc 387:9-387:24  Type
-testdata/Prelude.lc 387:9-389:30  a_->b_ | {a} -> List a -> Int->a
+testdata/Prelude.lc 387:9-389:30  a_->a_ | {a} -> List a -> Int->a
 testdata/Prelude.lc 387:10-387:11  b_
 testdata/Prelude.lc 387:16-387:19  Type
 testdata/Prelude.lc 387:16-387:24  Type
 testdata/Prelude.lc 387:23-387:24  Type
 testdata/Prelude.lc 388:10-388:12  {a} -> List a -> Int->a
 testdata/Prelude.lc 388:19-388:20  d_
-testdata/Prelude.lc 388:19-389:30  Bool->e_ | Int->c_ | List a_ -> Int->c_ | List c_ -> c_ | b_ -> List c_ -> c_ | c_
+testdata/Prelude.lc 388:19-389:30  Bool->d_ | Int->b_ | List a_ -> Int->a_ | List c_ -> b_ | b_ -> List b_ -> a_ | c_
 testdata/Prelude.lc 389:19-389:21  List f_
-testdata/Prelude.lc 389:19-389:24  Int->f_
+testdata/Prelude.lc 389:19-389:24  Int->e_
 testdata/Prelude.lc 389:19-389:30  d_
 testdata/Prelude.lc 389:22-389:24  {a} -> List a -> Int->a
 testdata/Prelude.lc 389:26-389:27  Int
diff --git a/testdata/ambig.out b/testdata/ambig.out
index 04e30108..04665182 100644
--- a/testdata/ambig.out
+++ b/testdata/ambig.out
@@ -6,7 +6,7 @@ testdata/ambig.lc 4:1-4:2  {a} -> {b} -> {c} -> {d} -> (b -> d->c) -> (b, d) ->
 testdata/ambig.lc 4:11-4:12  c_
 testdata/ambig.lc 7:9-7:29  b_
 testdata/ambig.lc 7:21-7:22  s_
-testdata/ambig.lc 7:21-7:26  HList c_ -> c_ | c_ | c_ -> HList c_ -> c_ | d_
+testdata/ambig.lc 7:21-7:26  HList c_ -> b_ | c_ | c_ -> HList b_ -> a_ | d_
 testdata/ambig.lc 7:23-7:24  n_
 testdata/ambig.lc 7:25-7:26  j_
 testdata/ambig.lc 7:28-7:29  g_
diff --git a/testdata/complex.out b/testdata/complex.out
index 59a9beaa..6152c39a 100644
--- a/testdata/complex.out
+++ b/testdata/complex.out
@@ -55,7 +55,7 @@ testdata/complex.lc 11:29-11:43  Type
 testdata/complex.lc 11:37-11:43  Repr
 testdata/complex.lc 12:1-12:7  Float -> Float -> Complex 'Normal
 testdata/complex.lc 12:14-12:21  {a:Repr} -> Float -> Float -> Complex a
-testdata/complex.lc 12:14-12:23  Float -> Complex b_
+testdata/complex.lc 12:14-12:23  Float -> Complex a_
 testdata/complex.lc 12:14-12:25  Complex 'Normal | Float -> Complex 'Normal | Float -> Float -> Complex 'Normal
 testdata/complex.lc 12:22-12:23  Float
 testdata/complex.lc 12:24-12:25  Float
@@ -67,7 +67,7 @@ testdata/complex.lc 14:28-14:41  Type
 testdata/complex.lc 14:36-14:41  Repr
 testdata/complex.lc 15:1-15:6  Float -> Float -> Complex 'Polar
 testdata/complex.lc 15:13-15:20  {a:Repr} -> Float -> Float -> Complex a
-testdata/complex.lc 15:13-15:22  Float -> Complex b_
+testdata/complex.lc 15:13-15:22  Float -> Complex a_
 testdata/complex.lc 15:13-15:24  Complex 'Polar | Float -> Complex 'Polar | Float -> Float -> Complex 'Polar
 testdata/complex.lc 15:21-15:22  Float
 testdata/complex.lc 15:23-15:24  Float
@@ -78,7 +78,7 @@ testdata/complex.lc 18:28-18:29  b_
 testdata/complex.lc 18:33-18:38  Type
 testdata/complex.lc 19:1-19:5  {a:Repr} -> Complex a -> Float
 testdata/complex.lc 19:34-19:38  {a} -> {b:Nat} -> {_ : a ~ VecScalar b Float} -> a->a
-testdata/complex.lc 19:34-19:50  Float | Float -> Float->d_ | Float->d_ | VecScalar 1 Float
+testdata/complex.lc 19:34-19:50  Float | Float -> Float->b_ | Float->c_ | VecScalar 1 Float
 testdata/complex.lc 19:34-20:35  Complex a_ -> Float | Float | Repr->Float | {a:Repr} -> Complex a -> Float
 testdata/complex.lc 19:40-19:41  Float
 testdata/complex.lc 19:40-19:42  Float->Float
@@ -93,7 +93,7 @@ testdata/complex.lc 19:46-19:48  Float->Float
 testdata/complex.lc 19:46-19:49  Float
 testdata/complex.lc 19:47-19:48  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
 testdata/complex.lc 19:48-19:49  Float
-testdata/complex.lc 20:34-20:35  Float | Float -> Float->d_ | Float->d_
+testdata/complex.lc 20:34-20:35  Float | Float -> Float->b_ | Float->c_
 testdata/complex.lc 22:12-22:19  Repr->Type
 testdata/complex.lc 22:12-22:26  Type
 testdata/complex.lc 22:20-22:26  Repr
@@ -102,7 +102,7 @@ testdata/complex.lc 22:30-22:43  Type
 testdata/complex.lc 22:38-22:43  Repr
 testdata/complex.lc 23:1-23:8  Complex 'Normal -> Complex 'Polar
 testdata/complex.lc 24:8-29:17  Complex 'Polar
-testdata/complex.lc 24:8-31:25  Complex 'Normal -> Complex 'Polar | Complex 'Polar | Float -> Float->d_ | Float->d_
+testdata/complex.lc 24:8-31:25  Complex 'Normal -> Complex 'Polar | Complex 'Polar | Float -> Float->b_ | Float->c_
 testdata/complex.lc 24:11-24:12  Float
 testdata/complex.lc 24:11-24:14  VecScalar 1 Float -> VecScalar 1 Bool
 testdata/complex.lc 24:11-24:19  VecScalar 1 Bool
@@ -254,8 +254,8 @@ testdata/complex.lc 64:30-64:44  Type
 testdata/complex.lc 64:38-64:44  Repr
 testdata/complex.lc 65:1-65:9  Complex 'Polar -> Complex 'Normal
 testdata/complex.lc 65:28-65:35  {a:Repr} -> Float -> Float -> Complex a
-testdata/complex.lc 65:28-65:49  Float -> Complex b_
-testdata/complex.lc 65:28-65:63  Complex 'Polar -> Complex 'Normal | Complex a_ | Float -> Float->d_ | Float->d_
+testdata/complex.lc 65:28-65:49  Float -> Complex a_
+testdata/complex.lc 65:28-65:63  Complex 'Polar -> Complex 'Normal | Complex a_ | Float -> Float->b_ | Float->c_
 testdata/complex.lc 65:37-65:38  Float
 testdata/complex.lc 65:37-65:40  Float->Float
 testdata/complex.lc 65:37-65:48  Float
@@ -271,7 +271,7 @@ testdata/complex.lc 65:55-65:58  {a} -> {b:Nat} -> {_ : a ~ VecScalar b Float} -
 testdata/complex.lc 65:55-65:62  VecScalar 1 Float
 testdata/complex.lc 65:59-65:62  Float
 testdata/complex.lc 111:1-111:15  {a:Repr} -> Complex a -> Float
-testdata/complex.lc 111:38-111:39  Float | Float -> Float->d_ | Float->d_
+testdata/complex.lc 111:38-111:39  Float | Float -> Float->b_ | Float->c_
 testdata/complex.lc 113:20-113:70  Type
 testdata/complex.lc 113:32-113:39  Repr->Type
 testdata/complex.lc 113:32-113:42  Type
@@ -286,8 +286,8 @@ testdata/complex.lc 113:60-113:70  Type
 testdata/complex.lc 113:68-113:70  Repr
 testdata/complex.lc 114:1-114:4  {a:Repr} -> {b:Repr} -> Complex a -> Complex b -> Complex a
 testdata/complex.lc 114:53-114:60  {a:Repr} -> Float -> Float -> Complex a
-testdata/complex.lc 114:53-114:68  Float -> Complex b_
-testdata/complex.lc 114:53-114:76  Complex a_ | Complex b_ -> Complex b_ -> Complex d_ | Complex b_ -> Complex d_ | Complex d_ | Float -> Float->d_ | Float->d_ | {a:Repr} -> Complex b_ -> Complex a -> Complex d_ | {a:Repr} -> {b:Repr} -> Complex a -> Complex b -> Complex a
+testdata/complex.lc 114:53-114:68  Float -> Complex a_
+testdata/complex.lc 114:53-114:76  Complex a_ | Complex b_ -> Complex a_ -> Complex b_ | Complex b_ -> Complex c_ | Complex d_ | Float -> Float->b_ | Float->c_ | {a:Repr} -> Complex a_ -> Complex a -> Complex a_ | {a:Repr} -> {b:Repr} -> Complex a -> Complex b -> Complex a
 testdata/complex.lc 114:62-114:63  Float
 testdata/complex.lc 114:62-114:65  Float->Float
 testdata/complex.lc 114:62-114:67  Float
@@ -311,8 +311,8 @@ testdata/complex.lc 128:51-128:61  Type
 testdata/complex.lc 128:59-128:61  Repr
 testdata/complex.lc 129:1-129:4  {a:Repr} -> {b:Repr} -> Complex a -> Complex b -> Complex a
 testdata/complex.lc 129:53-129:60  {a:Repr} -> Float -> Float -> Complex a
-testdata/complex.lc 129:53-129:72  Float -> Complex b_
-testdata/complex.lc 129:53-129:84  Complex a_ | Complex b_ -> Complex b_ -> Complex d_ | Complex b_ -> Complex d_ | Complex d_ | Float -> Float->d_ | Float->d_ | {a:Repr} -> Complex b_ -> Complex a -> Complex d_ | {a:Repr} -> {b:Repr} -> Complex a -> Complex b -> Complex a
+testdata/complex.lc 129:53-129:72  Float -> Complex a_
+testdata/complex.lc 129:53-129:84  Complex a_ | Complex b_ -> Complex a_ -> Complex b_ | Complex b_ -> Complex c_ | Complex d_ | Float -> Float->b_ | Float->c_ | {a:Repr} -> Complex a_ -> Complex a -> Complex a_ | {a:Repr} -> {b:Repr} -> Complex a -> Complex b -> Complex a
 testdata/complex.lc 129:62-129:63  Float
 testdata/complex.lc 129:62-129:64  Float->Float
 testdata/complex.lc 129:62-129:65  Float
@@ -347,10 +347,10 @@ testdata/complex.lc 137:19-137:26  Repr->Type
 testdata/complex.lc 137:19-137:28  Type
 testdata/complex.lc 137:27-137:28  Repr
 testdata/complex.lc 138:1-138:2  {a:Repr} -> Complex a -> Complex a
-testdata/complex.lc 138:7-138:22  Complex a_ -> Complex d_
-testdata/complex.lc 138:7-138:24  Complex a_ -> Complex b_ | Complex b_
+testdata/complex.lc 138:7-138:22  Complex a_ -> Complex c_
+testdata/complex.lc 138:7-138:24  Complex a_ -> Complex a_ | Complex b_
 testdata/complex.lc 138:8-138:11  {a:Repr} -> {b:Repr} -> Complex a -> Complex b -> Complex a
-testdata/complex.lc 138:8-138:13  Complex a_ -> Complex f_
+testdata/complex.lc 138:8-138:13  Complex a_ -> Complex e_
 testdata/complex.lc 138:8-138:15  Complex c_
 testdata/complex.lc 138:12-138:13  Complex f_
 testdata/complex.lc 138:14-138:15  Complex d_
diff --git a/testdata/language-features/basic-list/list11.out b/testdata/language-features/basic-list/list11.out
index db160d1b..53a243cf 100644
--- a/testdata/language-features/basic-list/list11.out
+++ b/testdata/language-features/basic-list/list11.out
@@ -4,7 +4,7 @@ value :: {a} -> {_ : 'Num a[
 ------------ tooltips
 testdata/language-features/basic-list/list11.lc 1:1-1:6  {a} -> {_ : Num a} -> List a
 testdata/language-features/basic-list/list11.lc 1:9-1:10  b_
-testdata/language-features/basic-list/list11.lc 1:9-1:11  List b_ -> List c_
+testdata/language-features/basic-list/list11.lc 1:9-1:11  List b_ -> List b_
 testdata/language-features/basic-list/list11.lc 1:9-1:13  List b_
 testdata/language-features/basic-list/list11.lc 1:10-1:11  {a} -> a -> List a -> List a
 testdata/language-features/basic-list/list11.lc 1:11-1:13  {a} -> List a
diff --git a/testdata/language-features/basic-list/list12.out b/testdata/language-features/basic-list/list12.out
index eebc55d2..78811ae1 100644
--- a/testdata/language-features/basic-list/list12.out
+++ b/testdata/language-features/basic-list/list12.out
@@ -4,23 +4,23 @@ value :: {a} -> {_ : 'Num a[
 ------------ tooltips
 testdata/language-features/basic-list/list12.lc 1:1-1:6  {a} -> {_ : Num a} -> List a
 testdata/language-features/basic-list/list12.lc 1:9-1:10  b_
-testdata/language-features/basic-list/list12.lc 1:9-1:11  List b_ -> List c_
+testdata/language-features/basic-list/list12.lc 1:9-1:11  List b_ -> List b_
 testdata/language-features/basic-list/list12.lc 1:9-1:21  List c_
 testdata/language-features/basic-list/list12.lc 1:10-1:11  {a} -> a -> List a -> List a
 testdata/language-features/basic-list/list12.lc 1:11-1:12  b_
-testdata/language-features/basic-list/list12.lc 1:11-1:13  List b_ -> List c_
+testdata/language-features/basic-list/list12.lc 1:11-1:13  List b_ -> List b_
 testdata/language-features/basic-list/list12.lc 1:11-1:21  List d_
 testdata/language-features/basic-list/list12.lc 1:12-1:13  {a} -> a -> List a -> List a
 testdata/language-features/basic-list/list12.lc 1:13-1:14  b_
-testdata/language-features/basic-list/list12.lc 1:13-1:15  List b_ -> List c_
+testdata/language-features/basic-list/list12.lc 1:13-1:15  List b_ -> List b_
 testdata/language-features/basic-list/list12.lc 1:13-1:21  List e_
 testdata/language-features/basic-list/list12.lc 1:14-1:15  {a} -> a -> List a -> List a
 testdata/language-features/basic-list/list12.lc 1:15-1:16  b_
-testdata/language-features/basic-list/list12.lc 1:15-1:17  List b_ -> List c_
+testdata/language-features/basic-list/list12.lc 1:15-1:17  List b_ -> List b_
 testdata/language-features/basic-list/list12.lc 1:15-1:21  List f_
 testdata/language-features/basic-list/list12.lc 1:16-1:17  {a} -> a -> List a -> List a
 testdata/language-features/basic-list/list12.lc 1:17-1:18  b_
-testdata/language-features/basic-list/list12.lc 1:17-1:19  List b_ -> List c_
+testdata/language-features/basic-list/list12.lc 1:17-1:19  List b_ -> List b_
 testdata/language-features/basic-list/list12.lc 1:17-1:21  List f_
 testdata/language-features/basic-list/list12.lc 1:18-1:19  {a} -> a -> List a -> List a
 testdata/language-features/basic-list/list12.lc 1:19-1:21  {a} -> List a
diff --git a/testdata/language-features/basic-list/listcomp01.out b/testdata/language-features/basic-list/listcomp01.out
index 8b857f79..649a2f20 100644
--- a/testdata/language-features/basic-list/listcomp01.out
+++ b/testdata/language-features/basic-list/listcomp01.out
@@ -4,7 +4,7 @@ value :: 'List ()
 ------------ tooltips
 testdata/language-features/basic-list/listcomp01.lc 1:1-1:6  List ()
 testdata/language-features/basic-list/listcomp01.lc 1:9-1:34  List ()
-testdata/language-features/basic-list/listcomp01.lc 1:10-1:12  () | List () | b_ -> List b_
+testdata/language-features/basic-list/listcomp01.lc 1:10-1:12  () | List () | b_ -> List a_
 testdata/language-features/basic-list/listcomp01.lc 1:20-1:33  List ()
 testdata/language-features/basic-list/listcomp01.lc 1:21-1:23  ()
 testdata/language-features/basic-list/listcomp01.lc 1:24-1:26  ()
diff --git a/testdata/language-features/basic-list/listcomp02.out b/testdata/language-features/basic-list/listcomp02.out
index 464eb751..691c04df 100644
--- a/testdata/language-features/basic-list/listcomp02.out
+++ b/testdata/language-features/basic-list/listcomp02.out
@@ -13,5 +13,5 @@ testdata/language-features/basic-list/listcomp02.lc 1:12-1:17  List ()
 testdata/language-features/basic-list/listcomp02.lc 1:15-1:17  () | List ()
 testdata/language-features/basic-list/listcomp02.lc 2:1-2:6  List ()
 testdata/language-features/basic-list/listcomp02.lc 2:9-2:21  List ()
-testdata/language-features/basic-list/listcomp02.lc 2:10-2:11  List b_ | b_ -> List b_ | d_
+testdata/language-features/basic-list/listcomp02.lc 2:10-2:11  List b_ | b_ -> List a_ | d_
 testdata/language-features/basic-list/listcomp02.lc 2:19-2:20  List ()
diff --git a/testdata/language-features/basic-list/listcomp03.out b/testdata/language-features/basic-list/listcomp03.out
index 1873533b..d9d98c75 100644
--- a/testdata/language-features/basic-list/listcomp03.out
+++ b/testdata/language-features/basic-list/listcomp03.out
@@ -5,7 +5,7 @@ value :: 'List ()
 testdata/language-features/basic-list/listcomp03.lc 1:1-1:6  List ()
 testdata/language-features/basic-list/listcomp03.lc 1:9-1:41  List ()
 testdata/language-features/basic-list/listcomp03.lc 1:10-1:12  () | List ()
-testdata/language-features/basic-list/listcomp03.lc 1:10-1:40  List () | List () -> List () | b_ -> List b_
+testdata/language-features/basic-list/listcomp03.lc 1:10-1:40  List () | List () -> List () | b_ -> List a_
 testdata/language-features/basic-list/listcomp03.lc 1:20-1:33  List ()
 testdata/language-features/basic-list/listcomp03.lc 1:21-1:23  ()
 testdata/language-features/basic-list/listcomp03.lc 1:24-1:26  ()
diff --git a/testdata/language-features/basic-list/listcomp04.out b/testdata/language-features/basic-list/listcomp04.out
index 7fe1306f..627ab11f 100644
--- a/testdata/language-features/basic-list/listcomp04.out
+++ b/testdata/language-features/basic-list/listcomp04.out
@@ -13,7 +13,7 @@ testdata/language-features/basic-list/listcomp04.lc 1:12-1:17  List ()
 testdata/language-features/basic-list/listcomp04.lc 1:15-1:17  () | List ()
 testdata/language-features/basic-list/listcomp04.lc 2:1-2:6  List ()
 testdata/language-features/basic-list/listcomp04.lc 2:9-2:30  List ()
-testdata/language-features/basic-list/listcomp04.lc 2:10-2:12  () | List () | b_ -> List b_
-testdata/language-features/basic-list/listcomp04.lc 2:10-2:29  List () | b_ -> List b_
+testdata/language-features/basic-list/listcomp04.lc 2:10-2:12  () | List () | b_ -> List a_
+testdata/language-features/basic-list/listcomp04.lc 2:10-2:29  List () | b_ -> List a_
 testdata/language-features/basic-list/listcomp04.lc 2:20-2:21  List ()
 testdata/language-features/basic-list/listcomp04.lc 2:28-2:29  List ()
diff --git a/testdata/language-features/basic-list/listcomp05.out b/testdata/language-features/basic-list/listcomp05.out
index ff871c08..7602c5ef 100644
--- a/testdata/language-features/basic-list/listcomp05.out
+++ b/testdata/language-features/basic-list/listcomp05.out
@@ -5,7 +5,7 @@ value :: 'List ()
 testdata/language-features/basic-list/listcomp05.lc 1:1-1:6  List ()
 testdata/language-features/basic-list/listcomp05.lc 1:9-1:39  List ()
 testdata/language-features/basic-list/listcomp05.lc 1:10-1:11  ()
-testdata/language-features/basic-list/listcomp05.lc 1:10-1:38  b_ -> List b_
+testdata/language-features/basic-list/listcomp05.lc 1:10-1:38  b_ -> List a_
 testdata/language-features/basic-list/listcomp05.lc 1:19-1:26  List ()
 testdata/language-features/basic-list/listcomp05.lc 1:20-1:22  ()
 testdata/language-features/basic-list/listcomp05.lc 1:23-1:25  () | List ()
diff --git a/testdata/language-features/basic-list/listcomp06.out b/testdata/language-features/basic-list/listcomp06.out
index 65679284..231185e2 100644
--- a/testdata/language-features/basic-list/listcomp06.out
+++ b/testdata/language-features/basic-list/listcomp06.out
@@ -6,7 +6,7 @@ value2 :: 'List ()
 testdata/language-features/basic-list/listcomp06.lc 1:1-1:7  List ()
 testdata/language-features/basic-list/listcomp06.lc 1:10-1:46  List ()
 testdata/language-features/basic-list/listcomp06.lc 1:11-1:12  () | List ()
-testdata/language-features/basic-list/listcomp06.lc 1:11-1:45  List () -> List () | b_ -> List b_
+testdata/language-features/basic-list/listcomp06.lc 1:11-1:45  List () -> List () | b_ -> List a_
 testdata/language-features/basic-list/listcomp06.lc 1:20-1:27  List ()
 testdata/language-features/basic-list/listcomp06.lc 1:21-1:23  ()
 testdata/language-features/basic-list/listcomp06.lc 1:24-1:26  () | List ()
@@ -16,7 +16,7 @@ testdata/language-features/basic-list/listcomp06.lc 1:41-1:45  Bool
 testdata/language-features/basic-list/listcomp06.lc 3:1-3:7  List ()
 testdata/language-features/basic-list/listcomp06.lc 3:10-3:46  List ()
 testdata/language-features/basic-list/listcomp06.lc 3:11-3:12  ()
-testdata/language-features/basic-list/listcomp06.lc 3:11-3:45  List () | b_ -> List b_
+testdata/language-features/basic-list/listcomp06.lc 3:11-3:45  List () | b_ -> List a_
 testdata/language-features/basic-list/listcomp06.lc 3:20-3:27  List ()
 testdata/language-features/basic-list/listcomp06.lc 3:21-3:23  ()
 testdata/language-features/basic-list/listcomp06.lc 3:24-3:26  () | List ()
diff --git a/testdata/language-features/basic-list/listcomp07.out b/testdata/language-features/basic-list/listcomp07.out
index 6238e239..a3f66edc 100644
--- a/testdata/language-features/basic-list/listcomp07.out
+++ b/testdata/language-features/basic-list/listcomp07.out
@@ -7,7 +7,7 @@ value3 :: 'List ()
 testdata/language-features/basic-list/listcomp07.lc 1:1-1:7  List ()
 testdata/language-features/basic-list/listcomp07.lc 1:10-6:11  List ()
 testdata/language-features/basic-list/listcomp07.lc 1:12-1:13  ()
-testdata/language-features/basic-list/listcomp07.lc 1:12-5:21  b_ -> List b_
+testdata/language-features/basic-list/listcomp07.lc 1:12-5:21  b_ -> List a_
 testdata/language-features/basic-list/listcomp07.lc 2:17-2:24  List ()
 testdata/language-features/basic-list/listcomp07.lc 2:18-2:20  ()
 testdata/language-features/basic-list/listcomp07.lc 2:21-2:23  () | List ()
@@ -19,7 +19,7 @@ testdata/language-features/basic-list/listcomp07.lc 5:20-5:21  ()
 testdata/language-features/basic-list/listcomp07.lc 8:1-8:7  List ()
 testdata/language-features/basic-list/listcomp07.lc 8:10-12:11  List ()
 testdata/language-features/basic-list/listcomp07.lc 8:12-8:13  ()
-testdata/language-features/basic-list/listcomp07.lc 8:12-11:21  b_ -> List b_
+testdata/language-features/basic-list/listcomp07.lc 8:12-11:21  b_ -> List a_
 testdata/language-features/basic-list/listcomp07.lc 8:21-8:28  List ()
 testdata/language-features/basic-list/listcomp07.lc 8:22-8:24  ()
 testdata/language-features/basic-list/listcomp07.lc 8:25-8:27  () | List ()
@@ -31,7 +31,7 @@ testdata/language-features/basic-list/listcomp07.lc 11:20-11:21  ()
 testdata/language-features/basic-list/listcomp07.lc 14:1-14:7  List ()
 testdata/language-features/basic-list/listcomp07.lc 14:10-20:3  List ()
 testdata/language-features/basic-list/listcomp07.lc 14:12-14:13  ()
-testdata/language-features/basic-list/listcomp07.lc 14:12-19:15  b_ -> List b_
+testdata/language-features/basic-list/listcomp07.lc 14:12-19:15  b_ -> List a_
 testdata/language-features/basic-list/listcomp07.lc 15:15-15:22  List ()
 testdata/language-features/basic-list/listcomp07.lc 15:16-15:18  ()
 testdata/language-features/basic-list/listcomp07.lc 15:19-15:21  () | List ()
diff --git a/testdata/language-features/basic-list/listcomp08.reject.out b/testdata/language-features/basic-list/listcomp08.reject.out
index 8bf99ab5..10384134 100644
--- a/testdata/language-features/basic-list/listcomp08.reject.out
+++ b/testdata/language-features/basic-list/listcomp08.reject.out
@@ -18,5 +18,5 @@ value = [x | x <- [], "not Bool"]
                       ^^^^^^^^^^
 
 ------------ tooltips
-testdata/language-features/basic-list/listcomp08.reject.lc 1:10-1:33  b_ -> List b_
+testdata/language-features/basic-list/listcomp08.reject.lc 1:10-1:33  b_ -> List a_
 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 55d987eb..d720baaf 100644
--- a/testdata/language-features/basic-list/listcomp09.out
+++ b/testdata/language-features/basic-list/listcomp09.out
@@ -4,6 +4,6 @@ value1 :: {_} -> 'List (()->'String)
 ------------ tooltips
 testdata/language-features/basic-list/listcomp09.lc 1:1-1:7  {_} -> List (()->String)
 testdata/language-features/basic-list/listcomp09.lc 1:10-1:36  List (()->String)
-testdata/language-features/basic-list/listcomp09.lc 1:11-1:25  List (()->String) | b_ -> List b_
+testdata/language-features/basic-list/listcomp09.lc 1:11-1:25  List (()->String) | b_ -> List a_
 testdata/language-features/basic-list/listcomp09.lc 1:18-1:25  String
 testdata/language-features/basic-list/listcomp09.lc 1:33-1:35  {a} -> List a
diff --git a/testdata/language-features/basic-values/fixity02.out b/testdata/language-features/basic-values/fixity02.out
index 6683f3d9..bed65026 100644
--- a/testdata/language-features/basic-values/fixity02.out
+++ b/testdata/language-features/basic-values/fixity02.out
@@ -31,28 +31,28 @@ testdata/language-features/basic-values/fixity02.lc 5:3-5:5  {a} -> {b} -> a ->
 testdata/language-features/basic-values/fixity02.lc 5:10-5:11  b_
 testdata/language-features/basic-values/fixity02.lc 11:1-11:7  Float
 testdata/language-features/basic-values/fixity02.lc 11:10-11:12  ()
-testdata/language-features/basic-values/fixity02.lc 11:10-11:15  a_->b_
+testdata/language-features/basic-values/fixity02.lc 11:10-11:15  a_->a_
 testdata/language-features/basic-values/fixity02.lc 11:10-11:34  Float
 testdata/language-features/basic-values/fixity02.lc 11:13-11:15  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 11:16-11:19  Char
-testdata/language-features/basic-values/fixity02.lc 11:16-11:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 11:16-11:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 11:16-11:34  Float
 testdata/language-features/basic-values/fixity02.lc 11:20-11:22  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 11:23-11:27  String
-testdata/language-features/basic-values/fixity02.lc 11:23-11:30  a_->b_
+testdata/language-features/basic-values/fixity02.lc 11:23-11:30  a_->a_
 testdata/language-features/basic-values/fixity02.lc 11:23-11:34  Float
 testdata/language-features/basic-values/fixity02.lc 11:28-11:30  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 11:31-11:34  Float
 testdata/language-features/basic-values/fixity02.lc 11:38-11:43  Type
 testdata/language-features/basic-values/fixity02.lc 12:1-12:7  Float
 testdata/language-features/basic-values/fixity02.lc 12:10-12:12  ()
-testdata/language-features/basic-values/fixity02.lc 12:10-12:15  a_->b_
+testdata/language-features/basic-values/fixity02.lc 12:10-12:15  a_->a_
 testdata/language-features/basic-values/fixity02.lc 12:10-12:34  Float
 testdata/language-features/basic-values/fixity02.lc 12:13-12:15  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 12:16-12:19  Char
 testdata/language-features/basic-values/fixity02.lc 12:16-12:22  a_->Char
 testdata/language-features/basic-values/fixity02.lc 12:16-12:27  Char
-testdata/language-features/basic-values/fixity02.lc 12:16-12:30  a_->b_
+testdata/language-features/basic-values/fixity02.lc 12:16-12:30  a_->a_
 testdata/language-features/basic-values/fixity02.lc 12:16-12:34  Float
 testdata/language-features/basic-values/fixity02.lc 12:20-12:22  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 12:23-12:27  String
@@ -63,13 +63,13 @@ testdata/language-features/basic-values/fixity02.lc 13:1-13:7  Float
 testdata/language-features/basic-values/fixity02.lc 13:10-13:12  ()
 testdata/language-features/basic-values/fixity02.lc 13:10-13:15  a_->()
 testdata/language-features/basic-values/fixity02.lc 13:10-13:19  ()
-testdata/language-features/basic-values/fixity02.lc 13:10-13:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 13:10-13:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 13:10-13:34  Float
 testdata/language-features/basic-values/fixity02.lc 13:13-13:15  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 13:16-13:19  Char
 testdata/language-features/basic-values/fixity02.lc 13:20-13:22  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 13:23-13:27  String
-testdata/language-features/basic-values/fixity02.lc 13:23-13:30  a_->b_
+testdata/language-features/basic-values/fixity02.lc 13:23-13:30  a_->a_
 testdata/language-features/basic-values/fixity02.lc 13:23-13:34  Float
 testdata/language-features/basic-values/fixity02.lc 13:28-13:30  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 13:31-13:34  Float
@@ -78,7 +78,7 @@ testdata/language-features/basic-values/fixity02.lc 14:1-14:7  Float
 testdata/language-features/basic-values/fixity02.lc 14:10-14:12  ()
 testdata/language-features/basic-values/fixity02.lc 14:10-14:15  a_->()
 testdata/language-features/basic-values/fixity02.lc 14:10-14:27  ()
-testdata/language-features/basic-values/fixity02.lc 14:10-14:30  a_->b_
+testdata/language-features/basic-values/fixity02.lc 14:10-14:30  a_->a_
 testdata/language-features/basic-values/fixity02.lc 14:10-14:34  Float
 testdata/language-features/basic-values/fixity02.lc 14:13-14:15  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 14:16-14:19  Char
@@ -91,11 +91,11 @@ testdata/language-features/basic-values/fixity02.lc 14:31-14:34  Float
 testdata/language-features/basic-values/fixity02.lc 14:38-14:43  Type
 testdata/language-features/basic-values/fixity02.lc 15:1-15:7  String
 testdata/language-features/basic-values/fixity02.lc 15:10-15:12  ()
-testdata/language-features/basic-values/fixity02.lc 15:10-15:15  a_->b_
+testdata/language-features/basic-values/fixity02.lc 15:10-15:15  a_->a_
 testdata/language-features/basic-values/fixity02.lc 15:10-15:34  String
 testdata/language-features/basic-values/fixity02.lc 15:13-15:15  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 15:16-15:19  Char
-testdata/language-features/basic-values/fixity02.lc 15:16-15:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 15:16-15:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 15:16-15:34  String
 testdata/language-features/basic-values/fixity02.lc 15:20-15:22  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 15:23-15:27  String
@@ -106,7 +106,7 @@ testdata/language-features/basic-values/fixity02.lc 15:31-15:34  Float
 testdata/language-features/basic-values/fixity02.lc 15:38-15:44  Type
 testdata/language-features/basic-values/fixity02.lc 16:1-16:7  Char
 testdata/language-features/basic-values/fixity02.lc 16:10-16:12  ()
-testdata/language-features/basic-values/fixity02.lc 16:10-16:15  a_->b_
+testdata/language-features/basic-values/fixity02.lc 16:10-16:15  a_->a_
 testdata/language-features/basic-values/fixity02.lc 16:10-16:34  Char
 testdata/language-features/basic-values/fixity02.lc 16:13-16:15  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 16:16-16:19  Char
@@ -123,7 +123,7 @@ testdata/language-features/basic-values/fixity02.lc 17:1-17:7  String
 testdata/language-features/basic-values/fixity02.lc 17:10-17:12  ()
 testdata/language-features/basic-values/fixity02.lc 17:10-17:15  a_->()
 testdata/language-features/basic-values/fixity02.lc 17:10-17:19  ()
-testdata/language-features/basic-values/fixity02.lc 17:10-17:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 17:10-17:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 17:10-17:34  String
 testdata/language-features/basic-values/fixity02.lc 17:13-17:15  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 17:16-17:19  Char
@@ -151,28 +151,28 @@ testdata/language-features/basic-values/fixity02.lc 18:31-18:34  Float
 testdata/language-features/basic-values/fixity02.lc 18:38-18:40  Type
 testdata/language-features/basic-values/fixity02.lc 20:1-20:10  Float
 testdata/language-features/basic-values/fixity02.lc 20:13-20:15  ()
-testdata/language-features/basic-values/fixity02.lc 20:13-20:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 20:13-20:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 20:13-20:49  Float
 testdata/language-features/basic-values/fixity02.lc 20:16-20:22  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 20:23-20:26  Char
-testdata/language-features/basic-values/fixity02.lc 20:23-20:33  a_->b_
+testdata/language-features/basic-values/fixity02.lc 20:23-20:33  a_->a_
 testdata/language-features/basic-values/fixity02.lc 20:23-20:49  Float
 testdata/language-features/basic-values/fixity02.lc 20:27-20:33  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 20:34-20:38  String
-testdata/language-features/basic-values/fixity02.lc 20:34-20:45  a_->b_
+testdata/language-features/basic-values/fixity02.lc 20:34-20:45  a_->a_
 testdata/language-features/basic-values/fixity02.lc 20:34-20:49  Float
 testdata/language-features/basic-values/fixity02.lc 20:39-20:45  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 20:46-20:49  Float
 testdata/language-features/basic-values/fixity02.lc 20:53-20:58  Type
 testdata/language-features/basic-values/fixity02.lc 21:1-21:10  Float
 testdata/language-features/basic-values/fixity02.lc 21:13-21:15  ()
-testdata/language-features/basic-values/fixity02.lc 21:13-21:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 21:13-21:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 21:13-21:49  Float
 testdata/language-features/basic-values/fixity02.lc 21:16-21:22  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 21:23-21:26  Char
 testdata/language-features/basic-values/fixity02.lc 21:23-21:33  a_->Char
 testdata/language-features/basic-values/fixity02.lc 21:23-21:38  Char
-testdata/language-features/basic-values/fixity02.lc 21:23-21:45  a_->b_
+testdata/language-features/basic-values/fixity02.lc 21:23-21:45  a_->a_
 testdata/language-features/basic-values/fixity02.lc 21:23-21:49  Float
 testdata/language-features/basic-values/fixity02.lc 21:27-21:33  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 21:34-21:38  String
@@ -183,13 +183,13 @@ testdata/language-features/basic-values/fixity02.lc 22:1-22:10  Float
 testdata/language-features/basic-values/fixity02.lc 22:13-22:15  ()
 testdata/language-features/basic-values/fixity02.lc 22:13-22:22  a_->()
 testdata/language-features/basic-values/fixity02.lc 22:13-22:26  ()
-testdata/language-features/basic-values/fixity02.lc 22:13-22:33  a_->b_
+testdata/language-features/basic-values/fixity02.lc 22:13-22:33  a_->a_
 testdata/language-features/basic-values/fixity02.lc 22:13-22:49  Float
 testdata/language-features/basic-values/fixity02.lc 22:16-22:22  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 22:23-22:26  Char
 testdata/language-features/basic-values/fixity02.lc 22:27-22:33  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 22:34-22:38  String
-testdata/language-features/basic-values/fixity02.lc 22:34-22:45  a_->b_
+testdata/language-features/basic-values/fixity02.lc 22:34-22:45  a_->a_
 testdata/language-features/basic-values/fixity02.lc 22:34-22:49  Float
 testdata/language-features/basic-values/fixity02.lc 22:39-22:45  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 22:46-22:49  Float
@@ -198,7 +198,7 @@ testdata/language-features/basic-values/fixity02.lc 23:1-23:10  Float
 testdata/language-features/basic-values/fixity02.lc 23:13-23:15  ()
 testdata/language-features/basic-values/fixity02.lc 23:13-23:22  a_->()
 testdata/language-features/basic-values/fixity02.lc 23:13-23:38  ()
-testdata/language-features/basic-values/fixity02.lc 23:13-23:45  a_->b_
+testdata/language-features/basic-values/fixity02.lc 23:13-23:45  a_->a_
 testdata/language-features/basic-values/fixity02.lc 23:13-23:49  Float
 testdata/language-features/basic-values/fixity02.lc 23:16-23:22  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 23:23-23:26  Char
@@ -211,11 +211,11 @@ testdata/language-features/basic-values/fixity02.lc 23:46-23:49  Float
 testdata/language-features/basic-values/fixity02.lc 23:53-23:58  Type
 testdata/language-features/basic-values/fixity02.lc 24:1-24:10  String
 testdata/language-features/basic-values/fixity02.lc 24:13-24:15  ()
-testdata/language-features/basic-values/fixity02.lc 24:13-24:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 24:13-24:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 24:13-24:49  String
 testdata/language-features/basic-values/fixity02.lc 24:16-24:22  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 24:23-24:26  Char
-testdata/language-features/basic-values/fixity02.lc 24:23-24:33  a_->b_
+testdata/language-features/basic-values/fixity02.lc 24:23-24:33  a_->a_
 testdata/language-features/basic-values/fixity02.lc 24:23-24:49  String
 testdata/language-features/basic-values/fixity02.lc 24:27-24:33  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 24:34-24:38  String
@@ -226,7 +226,7 @@ testdata/language-features/basic-values/fixity02.lc 24:46-24:49  Float
 testdata/language-features/basic-values/fixity02.lc 24:53-24:59  Type
 testdata/language-features/basic-values/fixity02.lc 25:1-25:10  Char
 testdata/language-features/basic-values/fixity02.lc 25:13-25:15  ()
-testdata/language-features/basic-values/fixity02.lc 25:13-25:22  a_->b_
+testdata/language-features/basic-values/fixity02.lc 25:13-25:22  a_->a_
 testdata/language-features/basic-values/fixity02.lc 25:13-25:49  Char
 testdata/language-features/basic-values/fixity02.lc 25:16-25:22  {a} -> {b} -> a -> b->b
 testdata/language-features/basic-values/fixity02.lc 25:23-25:26  Char
@@ -243,7 +243,7 @@ testdata/language-features/basic-values/fixity02.lc 26:1-26:10  String
 testdata/language-features/basic-values/fixity02.lc 26:13-26:15  ()
 testdata/language-features/basic-values/fixity02.lc 26:13-26:22  a_->()
 testdata/language-features/basic-values/fixity02.lc 26:13-26:26  ()
-testdata/language-features/basic-values/fixity02.lc 26:13-26:33  a_->b_
+testdata/language-features/basic-values/fixity02.lc 26:13-26:33  a_->a_
 testdata/language-features/basic-values/fixity02.lc 26:13-26:49  String
 testdata/language-features/basic-values/fixity02.lc 26:16-26:22  {a} -> {b} -> a -> b->a
 testdata/language-features/basic-values/fixity02.lc 26:23-26:26  Char
diff --git a/testdata/language-features/basic-values/infix02.out b/testdata/language-features/basic-values/infix02.out
index 16d50a6f..c5c2b99c 100644
--- a/testdata/language-features/basic-values/infix02.out
+++ b/testdata/language-features/basic-values/infix02.out
@@ -7,7 +7,7 @@ testdata/language-features/basic-values/infix02.lc 1:1-1:4  {a} -> {b} -> {c} ->
 testdata/language-features/basic-values/infix02.lc 1:13-1:15  ()
 testdata/language-features/basic-values/infix02.lc 3:1-3:6  {a} -> {b} -> {c} -> a -> b -> c->()
 testdata/language-features/basic-values/infix02.lc 3:13-3:14  g_
-testdata/language-features/basic-values/infix02.lc 3:13-3:20  b_ -> b_->()
+testdata/language-features/basic-values/infix02.lc 3:13-3:20  b_ -> a_->()
 testdata/language-features/basic-values/infix02.lc 3:13-3:22  a_->()
 testdata/language-features/basic-values/infix02.lc 3:15-3:20  {a} -> {b} -> {c} -> a -> b -> c->()
 testdata/language-features/basic-values/infix02.lc 3:21-3:22  d_
diff --git a/testdata/language-features/basic-values/typesig03.out b/testdata/language-features/basic-values/typesig03.out
index 49f21cd9..720df136 100644
--- a/testdata/language-features/basic-values/typesig03.out
+++ b/testdata/language-features/basic-values/typesig03.out
@@ -11,7 +11,7 @@ testdata/language-features/basic-values/typesig03.lc 1:19-1:20  d_
 testdata/language-features/basic-values/typesig03.lc 1:19-1:26  Type
 testdata/language-features/basic-values/typesig03.lc 1:24-1:26  Type
 testdata/language-features/basic-values/typesig03.lc 2:1-2:5  {a} -> {b} -> {c} -> a -> b -> c->()
-testdata/language-features/basic-values/typesig03.lc 2:14-2:16  () | c_ -> c_ -> c_->() | c_ -> c_->() | c_->()
+testdata/language-features/basic-values/typesig03.lc 2:14-2:16  () | c_ -> b_ -> a_->() | c_ -> b_->() | c_->()
 testdata/language-features/basic-values/typesig03.lc 4:7-4:8  f_
 testdata/language-features/basic-values/typesig03.lc 4:7-4:18  Type
 testdata/language-features/basic-values/typesig03.lc 4:10-4:11  e_
@@ -20,4 +20,4 @@ testdata/language-features/basic-values/typesig03.lc 4:13-4:14  d_
 testdata/language-features/basic-values/typesig03.lc 4:13-4:18  Type
 testdata/language-features/basic-values/typesig03.lc 4:16-4:18  Type
 testdata/language-features/basic-values/typesig03.lc 5:1-5:5  {a} -> {b} -> {c} -> a -> b -> c->()
-testdata/language-features/basic-values/typesig03.lc 5:14-5:16  () | c_ -> c_ -> c_->() | c_ -> c_->() | c_->()
+testdata/language-features/basic-values/typesig03.lc 5:14-5:16  () | c_ -> b_ -> a_->() | c_ -> b_->() | c_->()
diff --git a/testdata/language-features/basic-values/typesig04.out b/testdata/language-features/basic-values/typesig04.out
index 0661ca9c..9d7d2072 100644
--- a/testdata/language-features/basic-values/typesig04.out
+++ b/testdata/language-features/basic-values/typesig04.out
@@ -10,7 +10,7 @@ testdata/language-features/basic-values/typesig04.lc 1:15-1:16  e_
 testdata/language-features/basic-values/typesig04.lc 1:20-1:21  Type | d_
 testdata/language-features/basic-values/typesig04.lc 1:26-1:28  Type
 testdata/language-features/basic-values/typesig04.lc 2:1-2:5  {a} -> {b} -> {c} -> a -> (b->c)->()
-testdata/language-features/basic-values/typesig04.lc 2:12-2:14  () | (c_->c_)->() | c_ -> (c_->c_)->()
+testdata/language-features/basic-values/typesig04.lc 2:12-2:14  () | (c_->b_)->() | c_ -> (b_->a_)->()
 testdata/language-features/basic-values/typesig04.lc 4:7-4:8  f_
 testdata/language-features/basic-values/typesig04.lc 4:7-4:20  Type
 testdata/language-features/basic-values/typesig04.lc 4:10-4:20  Type
@@ -18,4 +18,4 @@ testdata/language-features/basic-values/typesig04.lc 4:11-4:12  e_
 testdata/language-features/basic-values/typesig04.lc 4:14-4:15  Type | d_
 testdata/language-features/basic-values/typesig04.lc 4:18-4:20  Type
 testdata/language-features/basic-values/typesig04.lc 5:1-5:5  {a} -> {b} -> {c} -> a -> (b->c)->()
-testdata/language-features/basic-values/typesig04.lc 5:12-5:14  () | (c_->c_)->() | c_ -> (c_->c_)->()
+testdata/language-features/basic-values/typesig04.lc 5:12-5:14  () | (c_->b_)->() | c_ -> (b_->a_)->()
diff --git a/testdata/language-features/basic-values/typesig05.out b/testdata/language-features/basic-values/typesig05.out
index 4c781fa8..a2d2e91d 100644
--- a/testdata/language-features/basic-values/typesig05.out
+++ b/testdata/language-features/basic-values/typesig05.out
@@ -20,7 +20,7 @@ testdata/language-features/basic-values/typesig05.lc 4:19-4:22  String
 testdata/language-features/basic-values/typesig05.lc 4:26-4:30  Type
 testdata/language-features/basic-values/typesig05.lc 5:1-5:7  String
 testdata/language-features/basic-values/typesig05.lc 5:10-5:14  {a} -> {b} -> a -> b->b
-testdata/language-features/basic-values/typesig05.lc 5:10-5:18  a_->b_
+testdata/language-features/basic-values/typesig05.lc 5:10-5:18  a_->a_
 testdata/language-features/basic-values/typesig05.lc 5:10-5:22  String
 testdata/language-features/basic-values/typesig05.lc 5:15-5:18  Char
 testdata/language-features/basic-values/typesig05.lc 5:19-5:22  String
@@ -35,7 +35,7 @@ testdata/language-features/basic-values/typesig05.lc 8:19-8:22  String
 testdata/language-features/basic-values/typesig05.lc 10:11-10:17  Type
 testdata/language-features/basic-values/typesig05.lc 11:1-11:7  String
 testdata/language-features/basic-values/typesig05.lc 11:10-11:14  {a} -> {b} -> a -> b->b
-testdata/language-features/basic-values/typesig05.lc 11:10-11:18  a_->b_
+testdata/language-features/basic-values/typesig05.lc 11:10-11:18  a_->a_
 testdata/language-features/basic-values/typesig05.lc 11:10-11:22  String
 testdata/language-features/basic-values/typesig05.lc 11:15-11:18  Char
 testdata/language-features/basic-values/typesig05.lc 11:19-11:22  String
diff --git a/testdata/language-features/pattern/uncovered.out b/testdata/language-features/pattern/uncovered.out
index 74f875cb..c96c691e 100644
--- a/testdata/language-features/pattern/uncovered.out
+++ b/testdata/language-features/pattern/uncovered.out
@@ -4,10 +4,10 @@ f :: {a} -> {_ : 'Num a[0;32
 ------------ tooltips
 testdata/language-features/pattern/uncovered.lc 4:1-4:2  {a} -> {_ : Num a} -> Bool -> Bool -> Bool->a
 testdata/language-features/pattern/uncovered.lc 4:18-4:19  b_
-testdata/language-features/pattern/uncovered.lc 4:18-5:19  Bool->d_ | c_
-testdata/language-features/pattern/uncovered.lc 4:18-6:19  Bool->d_
+testdata/language-features/pattern/uncovered.lc 4:18-5:19  Bool->c_ | c_
+testdata/language-features/pattern/uncovered.lc 4:18-6:19  Bool->c_
 testdata/language-features/pattern/uncovered.lc 5:18-5:19  b_ | c_
-testdata/language-features/pattern/uncovered.lc 5:18-6:19  Bool->d_ | b_
+testdata/language-features/pattern/uncovered.lc 5:18-6:19  Bool->c_ | b_
 testdata/language-features/pattern/uncovered.lc 6:18-6:19  b_
 ------------ warnings
 Uncovered pattern(s) at testdata/language-features/pattern/uncovered.lc:4:1:
diff --git a/testdata/language-features/recursion/simplerec01.out b/testdata/language-features/recursion/simplerec01.out
index e975d532..9be285c9 100644
--- a/testdata/language-features/recursion/simplerec01.out
+++ b/testdata/language-features/recursion/simplerec01.out
@@ -4,6 +4,6 @@ fun :: {a} -> {_ : 'Num a[0;
 ------------ tooltips
 testdata/language-features/recursion/simplerec01.lc 1:1-1:4  {a} -> {_ : Num a} -> {_ : Eq a} -> {_ : Num a} -> a->Char
 testdata/language-features/recursion/simplerec01.lc 1:9-1:12  Char
-testdata/language-features/recursion/simplerec01.lc 1:9-2:14  Bool->Char | a_->b_
+testdata/language-features/recursion/simplerec01.lc 1:9-2:14  Bool->Char | a_->a_
 testdata/language-features/recursion/simplerec01.lc 2:9-2:12  e_
 testdata/language-features/recursion/simplerec01.lc 2:13-2:14  b_
diff --git a/testdata/language-features/recursion/simplerec02.out b/testdata/language-features/recursion/simplerec02.out
index 96ad9d37..43dd847f 100644
--- a/testdata/language-features/recursion/simplerec02.out
+++ b/testdata/language-features/recursion/simplerec02.out
@@ -4,7 +4,7 @@ value :: ()
 ------------ tooltips
 testdata/language-features/recursion/simplerec02.lc 1:1-1:6  ()
 testdata/language-features/recursion/simplerec02.lc 1:21-1:24  Char
-testdata/language-features/recursion/simplerec02.lc 1:21-2:26  Bool->Char | a_->b_
+testdata/language-features/recursion/simplerec02.lc 1:21-2:26  Bool->Char | a_->a_
 testdata/language-features/recursion/simplerec02.lc 2:21-2:24  e_
 testdata/language-features/recursion/simplerec02.lc 2:25-2:26  b_
 testdata/language-features/recursion/simplerec02.lc 3:12-3:14  ()
diff --git a/testdata/language-features/recursion/simplerec03.out b/testdata/language-features/recursion/simplerec03.out
index 27c2981e..30b0755d 100644
--- a/testdata/language-features/recursion/simplerec03.out
+++ b/testdata/language-features/recursion/simplerec03.out
@@ -5,6 +5,6 @@ value :: ()
 testdata/language-features/recursion/simplerec03.lc 1:1-1:6  ()
 testdata/language-features/recursion/simplerec03.lc 1:9-1:11  ()
 testdata/language-features/recursion/simplerec03.lc 3:13-3:16  Char
-testdata/language-features/recursion/simplerec03.lc 3:13-4:18  Bool->Char | a_->b_
+testdata/language-features/recursion/simplerec03.lc 3:13-4:18  Bool->Char | a_->a_
 testdata/language-features/recursion/simplerec03.lc 4:13-4:16  e_
 testdata/language-features/recursion/simplerec03.lc 4:17-4:18  b_
diff --git a/testdata/record01.reject.out b/testdata/record01.reject.out
index b2d8d0e8..38d10686 100644
--- a/testdata/record01.reject.out
+++ b/testdata/record01.reject.out
@@ -107,9 +107,9 @@ testdata/record01.reject.lc 11:47-11:51  Float
 testdata/record01.reject.lc 12:10-12:18  CullMode
 testdata/record01.reject.lc 13:11-13:20  CullMode
 testdata/record01.reject.lc 14:23-14:34  {a} -> CullMode -> PolygonMode a -> PolygonOffset -> ProvokingVertex -> RasterContext a 'Triangle
-testdata/record01.reject.lc 14:23-14:39  PolygonMode a_ -> PolygonOffset -> ProvokingVertex -> RasterContext d_ 'Triangle
-testdata/record01.reject.lc 14:23-14:49  PolygonOffset -> ProvokingVertex -> RasterContext c_ 'Triangle
-testdata/record01.reject.lc 14:23-14:58  ProvokingVertex -> RasterContext b_ 'Triangle
+testdata/record01.reject.lc 14:23-14:39  PolygonMode a_ -> PolygonOffset -> ProvokingVertex -> RasterContext a_ 'Triangle
+testdata/record01.reject.lc 14:23-14:49  PolygonOffset -> ProvokingVertex -> RasterContext a_ 'Triangle
+testdata/record01.reject.lc 14:23-14:58  ProvokingVertex -> RasterContext a_ 'Triangle
 testdata/record01.reject.lc 14:23-14:70  RasterContext a_ 'Triangle
 testdata/record01.reject.lc 14:35-14:39  CullMode
 testdata/record01.reject.lc 14:40-14:49  {a} -> PolygonMode a
@@ -124,7 +124,7 @@ testdata/record01.reject.lc 15:44-15:61  FragmentOperation 'Depth
 testdata/record01.reject.lc 15:52-15:56  ComparisonFunction
 testdata/record01.reject.lc 15:57-15:61  Bool
 testdata/record01.reject.lc 15:63-15:70  {a} -> {b:Nat} -> {_ : Num a} -> Blending a -> VecScalar b Bool -> FragmentOperation ('Color (VecScalar b a))
-testdata/record01.reject.lc 15:63-15:76  VecScalar b_ Bool -> FragmentOperation ('Color (VecScalar c_ Float))
+testdata/record01.reject.lc 15:63-15:76  VecScalar b_ Bool -> FragmentOperation ('Color (VecScalar b_ Float))
 testdata/record01.reject.lc 15:63-15:101  ((FragmentOperation ('Color (VecScalar 4 Float)))) | FragmentOperation ('Color (VecScalar 4 Float))
 testdata/record01.reject.lc 15:71-15:76  Blending Float
 testdata/record01.reject.lc 15:78-15:80  {a} -> a -> a -> a -> a -> VecS a 4
@@ -146,7 +146,7 @@ testdata/record01.reject.lc 16:40-16:53  Type
 testdata/record01.reject.lc 16:44-16:45  b_
 testdata/record01.reject.lc 16:46-16:47  b_
 testdata/record01.reject.lc 16:48-16:53  Type
-testdata/record01.reject.lc 17:27-17:61  (VecS Float 4, VecS Float 4) | HList c_ -> c_ | c_ -> HList c_ -> c_
+testdata/record01.reject.lc 17:27-17:61  (VecS Float 4, VecS Float 4) | HList c_ -> b_ | c_ -> HList b_ -> a_
 testdata/record01.reject.lc 17:28-17:41  {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Vec b c -> Vec a c
 testdata/record01.reject.lc 17:28-17:55  Vec 4 Float -> Vec 4 Float
 testdata/record01.reject.lc 17:28-17:57  Vec 4 Float
@@ -154,7 +154,7 @@ testdata/record01.reject.lc 17:42-17:55  Mat 4 4 Float
 testdata/record01.reject.lc 17:56-17:57  g_
 testdata/record01.reject.lc 17:59-17:60  ((VecS Float 4)) | VecS Float 4
 testdata/record01.reject.lc 18:23-18:28  {a:PrimitiveType} -> {b : List Type} -> String -> HList b -> PrimitiveStream a (HList b)
-testdata/record01.reject.lc 18:23-18:37  HList a_ -> PrimitiveStream c_ (HList b_)
+testdata/record01.reject.lc 18:23-18:37  HList a_ -> PrimitiveStream b_ (HList a_)
 testdata/record01.reject.lc 18:23-18:79  PrimitiveStream a_ ((Vec 4 Float))
 testdata/record01.reject.lc 18:29-18:37  String
 testdata/record01.reject.lc 18:39-18:48  {a} -> String->a
@@ -168,19 +168,19 @@ testdata/record01.reject.lc 18:65-18:76  List Type | Type
 testdata/record01.reject.lc 18:69-18:70  b_
 testdata/record01.reject.lc 18:71-18:76  Type
 testdata/record01.reject.lc 19:23-19:36  {a} -> {b} -> {c:PrimitiveType} -> (a->b) -> List (Primitive a c) -> List (Primitive b c)
-testdata/record01.reject.lc 19:23-19:49  List (Primitive ((VecS Float 4)) a_) -> List (Primitive (VecS Float 4, VecS Float 4) b_)
+testdata/record01.reject.lc 19:23-19:49  List (Primitive ((VecS Float 4)) a_) -> List (Primitive (VecS Float 4, VecS Float 4) a_)
 testdata/record01.reject.lc 19:23-19:62  List (Primitive (VecS Float 4, VecS Float 4) a_)
 testdata/record01.reject.lc 19:37-19:49  ((VecS Float 4))->(VecS Float 4, VecS Float 4)
 testdata/record01.reject.lc 19:50-19:62  {a:PrimitiveType} -> PrimitiveStream a ((Vec 4 Float))
 testdata/record01.reject.lc 20:23-20:42  {a : List Type} -> {b:PrimitiveType} -> RasterContext (HList ('Cons (Vec 4 Float) a)) b -> HList ('map Type Type Interpolated a) -> List (Primitive (HList ('Cons (Vec 4 Float) a)) b) -> List (Vector 1 (Maybe (SimpleFragment (HList a))))
-testdata/record01.reject.lc 20:23-20:52  HList ('map Type Type Interpolated a_) -> List (Primitive (HList ('Cons (Vec 4 Float) b_)) 'Triangle) -> List (Vector 1 (Maybe (SimpleFragment (HList c_))))
-testdata/record01.reject.lc 20:23-20:63  List (Primitive (HList ('Cons (Vec 4 Float) d_)) 'Triangle) -> List (Vector 1 (Maybe (SimpleFragment (HList e_))))
+testdata/record01.reject.lc 20:23-20:52  HList ('map Type Type Interpolated a_) -> List (Primitive (HList ('Cons (Vec 4 Float) a_)) 'Triangle) -> List (Vector 1 (Maybe (SimpleFragment (HList a_))))
+testdata/record01.reject.lc 20:23-20:63  List (Primitive (HList ('Cons (Vec 4 Float) d_)) 'Triangle) -> List (Vector 1 (Maybe (SimpleFragment (HList d_))))
 testdata/record01.reject.lc 20:23-20:79  List (Vector 1 (Maybe (SimpleFragment ((VecS Float 4)))))
 testdata/record01.reject.lc 20:43-20:52  {a} -> RasterContext a 'Triangle
 testdata/record01.reject.lc 20:53-20:63  ((Interpolated c_))
 testdata/record01.reject.lc 20:55-20:61  {a} -> {_ : Floating a} -> Interpolated a
 testdata/record01.reject.lc 20:64-20:79  {a:PrimitiveType} -> List (Primitive (VecS Float 4, VecS Float 4) a)
-testdata/record01.reject.lc 21:33-21:55  ((VecS Float 4)) | HList c_ -> c_ | c_ -> HList c_ -> c_
+testdata/record01.reject.lc 21:33-21:55  ((VecS Float 4)) | HList c_ -> b_ | c_ -> HList b_ -> a_
 testdata/record01.reject.lc 21:35-21:37  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/record01.reject.lc 21:35-21:41  Float -> Float -> Float -> VecS Float 4
 testdata/record01.reject.lc 21:35-21:45  Float -> Float -> VecS Float 4
@@ -190,9 +190,9 @@ testdata/record01.reject.lc 21:38-21:41  Float
 testdata/record01.reject.lc 21:42-21:45  Float
 testdata/record01.reject.lc 21:46-21:49  Float
 testdata/record01.reject.lc 21:50-21:53  Float
-testdata/record01.reject.lc 22:33-22:67  ((VecS Float 4)) | HList c_ -> c_ | c_ -> HList c_ -> c_
+testdata/record01.reject.lc 22:33-22:67  ((VecS Float 4)) | HList c_ -> b_ | c_ -> HList b_ -> a_
 testdata/record01.reject.lc 22:35-22:42  {a} -> {_ : Num (MatVecScalarElem a)} -> a -> a->a
-testdata/record01.reject.lc 22:35-22:44  i_->j_
+testdata/record01.reject.lc 22:35-22:44  i_->i_
 testdata/record01.reject.lc 22:35-22:65  VecS Float 4
 testdata/record01.reject.lc 22:43-22:44  j_
 testdata/record01.reject.lc 22:46-22:48  {a} -> a -> a -> a -> a -> VecS a 4
@@ -205,8 +205,8 @@ testdata/record01.reject.lc 22:53-22:56  Float
 testdata/record01.reject.lc 22:57-22:60  Float
 testdata/record01.reject.lc 22:61-22:64  Float
 testdata/record01.reject.lc 23:23-23:33  {a:Nat} -> {b : List Type} -> {c} -> HList b -> (c -> HList ('imageType' ('map Type ImageKind FragmentOperationKind b))) -> List (Vector a (Maybe (SimpleFragment c))) -> FrameBuffer a ('map Type ImageKind FragmentOperationKind b) -> FrameBuffer a ('map Type ImageKind FragmentOperationKind b)
-testdata/record01.reject.lc 23:23-23:45  (a_->(('imageType (FragmentOperationKind (FragmentOperation ('Color (VecScalar 4 Float))))))) -> List (Vector c_ (Maybe (SimpleFragment b_))) -> FrameBuffer d_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil))) -> FrameBuffer e_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil)))
-testdata/record01.reject.lc 23:23-23:60  List (Vector a_ (Maybe (SimpleFragment ((VecS Float 4))))) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil))) -> FrameBuffer c_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil)))
+testdata/record01.reject.lc 23:23-23:45  (a_->(('imageType (FragmentOperationKind (FragmentOperation ('Color (VecScalar 4 Float))))))) -> List (Vector b_ (Maybe (SimpleFragment a_))) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil))) -> FrameBuffer b_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil)))
+testdata/record01.reject.lc 23:23-23:60  List (Vector a_ (Maybe (SimpleFragment ((VecS Float 4))))) -> FrameBuffer a_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil))) -> FrameBuffer a_ ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil)))
 testdata/record01.reject.lc 23:23-23:75  FrameBuffer 1 ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil))) -> FrameBuffer 1 ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil)))
 testdata/record01.reject.lc 23:23-23:83  FrameBuffer 1 ('map Type ImageKind FragmentOperationKind ('Cons (FragmentOperation 'Depth) ('Cons (FragmentOperation ('Color (VecScalar 4 Float))) 'Nil)))
 testdata/record01.reject.lc 23:34-23:45  (FragmentOperation 'Depth, FragmentOperation ('Color (VecScalar 4 Float)))
diff --git a/testdata/typeclass.out b/testdata/typeclass.out
index e0da48d1..c325cfed 100644
--- a/testdata/typeclass.out
+++ b/testdata/typeclass.out
@@ -36,7 +36,7 @@ testdata/typeclass.lc 20:15-20:21  Bool
 testdata/typeclass.lc 20:17-20:19  {a} -> {_ : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 20:20-20:21  c_
 testdata/typeclass.lc 23:17-23:18  Bool
-testdata/typeclass.lc 23:17-24:23  Bool->Bool | {_ : Eq a_} -> b_ -> c_->Bool | {a} -> {_ : Eq a} -> a -> a->Bool
+testdata/typeclass.lc 23:17-24:23  Bool->Bool | {_ : Eq a_} -> a_ -> a_->Bool | {a} -> {_ : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 24:18-24:21  Bool->Bool
 testdata/typeclass.lc 24:18-24:23  Bool
 testdata/typeclass.lc 24:22-24:23  b_
diff --git a/testdata/typesig.reject.out b/testdata/typesig.reject.out
index 05632bc8..50c13202 100644
--- a/testdata/typesig.reject.out
+++ b/testdata/typesig.reject.out
@@ -1,16 +1,16 @@
 focus checkMetas: \a -> (\(b:Type) -> primFix a b) (\(a:=Type) -> \(c:Type) -> <<HERE>>)
-\(a : Type~a_) (b : b_~'X) -> typeAnn c_ (labend X)
+\(a : Type~a_) (b : a_~'X) -> typeAnn a_ (labend X)
 ------------ trace
 'X :: Type
 X :: 'X
 'XCase :: (a : 'X->Type) -> a X -> (b:'X) -> a b
 match'X :: (a : Type->Type) -> a 'X -> (b:Type) -> a b -> a b
 !focus checkMetas: \a -> (\(b:Type) -> primFix a b) (\(a:=Type) -> \(c:Type) -> <<HERE>>)
-\(a : Type~a_) (b : b_~'X) -> typeAnn c_ (labend X)
+\(a : Type~a_) (b : a_~'X) -> typeAnn a_ (labend X)
 ------------ tooltips
 testdata/typesig.reject.lc 4:6-4:7  Type
 testdata/typesig.reject.lc 4:6-4:11  Type
 testdata/typesig.reject.lc 4:10-4:11  X
 testdata/typesig.reject.lc 6:6-6:7  b_
-testdata/typesig.reject.lc 6:6-7:6  a_->b_ | c_
+testdata/typesig.reject.lc 6:6-7:6  a_->a_ | c_
 testdata/typesig.reject.lc 7:5-7:6  X
diff --git a/testdata/zip01.out b/testdata/zip01.out
index 02f84ae5..10a48894 100644
--- a/testdata/zip01.out
+++ b/testdata/zip01.out
@@ -4,7 +4,7 @@ zip2 :: {a} -> {b} -> 'List a -> 'List
 ------------ tooltips
 testdata/zip01.lc 1:9-1:12  Type
 testdata/zip01.lc 1:9-1:30  Type
-testdata/zip01.lc 1:9-4:40  a_->b_ | {a} -> {b} -> List a -> List b -> List (a, b)
+testdata/zip01.lc 1:9-4:40  a_->a_ | {a} -> {b} -> List a -> List b -> List (a, b)
 testdata/zip01.lc 1:10-1:11  d_
 testdata/zip01.lc 1:16-1:19  Type
 testdata/zip01.lc 1:16-1:30  Type
@@ -16,17 +16,17 @@ testdata/zip01.lc 1:25-1:28  List Type
 testdata/zip01.lc 1:27-1:28  List Type | Type
 testdata/zip01.lc 2:1-2:5  {a} -> {b} -> List a -> List b -> List (a, b)
 testdata/zip01.lc 2:22-2:24  {a} -> List a
-testdata/zip01.lc 2:22-4:40  List (d_, c_) | List a_ -> List (b_, e_) | List b_ -> List (d_, c_) | List b_ -> List b_ -> List (d_, c_)
+testdata/zip01.lc 2:22-4:40  List (d_, c_) | List a_ -> List (a_, d_) | List b_ -> List (c_, b_) | List b_ -> List a_ -> List (b_, a_)
 testdata/zip01.lc 3:22-3:24  {a} -> List a
-testdata/zip01.lc 3:22-4:40  List (c_, f_) | List a_ -> List (f_, b_) | List c_ -> List c_ | b_ -> List c_ -> List c_
+testdata/zip01.lc 3:22-4:40  List (c_, f_) | List a_ -> List (e_, a_) | List c_ -> List b_ | b_ -> List b_ -> List a_
 testdata/zip01.lc 4:22-4:27  (h_, d_)
-testdata/zip01.lc 4:22-4:29  List (h_, d_) -> List (i_, e_)
-testdata/zip01.lc 4:22-4:40  List (g_, c_) | List c_ -> List c_ | b_ -> List c_ -> List c_
+testdata/zip01.lc 4:22-4:29  List (h_, d_) -> List (h_, d_)
+testdata/zip01.lc 4:22-4:40  List (g_, c_) | List c_ -> List b_ | b_ -> List b_ -> List a_
 testdata/zip01.lc 4:23-4:24  k_
 testdata/zip01.lc 4:25-4:26  ((d_)) | g_
 testdata/zip01.lc 4:28-4:29  {a} -> a -> List a -> List a
 testdata/zip01.lc 4:30-4:34  {a} -> {b} -> List a -> List b -> List (a, b)
-testdata/zip01.lc 4:30-4:37  List a_ -> List (i_, b_)
+testdata/zip01.lc 4:30-4:37  List a_ -> List (h_, a_)
 testdata/zip01.lc 4:30-4:40  List (g_, c_)
 testdata/zip01.lc 4:35-4:37  List i_
 testdata/zip01.lc 4:38-4:40  List c_