always show parens

20 files changed, 313 insertions, 313 deletions

diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index 07783eca..aefc3cae 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -5,9 +5,9 @@ id :: {a} -> a->a
 V2 :: {a} -> a -> a -> 'VecS a 2
 V3 :: {a} -> a -> a -> a -> 'VecS a 3
 V4 :: {a} -> a -> a -> a -> a -> 'VecS a 4
-'VecSCase :: {a} -> (b : c:'Nat -> 'VecS a c -> Type) -> (d:a -> e:a -> b 2 (V2 d e)) -> (f:a -> g:a -> h:a -> b 3 (V3 f g h)) -> (i:a -> j:a -> k:a -> l:a -> b 4 (V4 i j k l)) -> {m:'Nat} -> (n : 'VecS a m) -> b m n
-match'VecS :: (a : Type->Type) -> (b:Type -> c:'Nat -> a ('VecS b c)) -> d:Type -> a d -> a d
-mapVec :: {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c
+'VecSCase :: {a} -> (b : (c:'Nat) -> 'VecS a c -> Type) -> ((d:a) -> (e:a) -> b 2 (V2 d e)) -> ((f:a) -> (g:a) -> (h:a) -> b 3 (V3 f g h)) -> ((i:a) -> (j:a) -> (k:a) -> (l:a) -> b 4 (V4 i j k l)) -> {m:'Nat} -> (n : 'VecS a m) -> b m n
+match'VecS :: (a : Type->Type) -> ((b:Type) -> (c:'Nat) -> a ('VecS b c)) -> (d:Type) -> a d -> a d
+mapVec :: {a} -> {b} -> {c:'Nat} -> (a->b) -> 'VecS a c -> 'VecS b c
 'Vec :: 'Nat -> Type->Type
 'VecScalar :: 'Nat -> Type->Type
 'Mat :: 'Nat -> 'Nat -> Type->Type
@@ -20,8 +20,8 @@ M43F :: 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 4 'Float -> 'Mat 4 3 'Float
 M24F :: 'Vec 2 'Float -> 'Vec 2 'Float -> 'Vec 2 'Float -> 'Vec 2 'Float -> 'Mat 2 4 'Float
 M34F :: 'Vec 3 'Float -> 'Vec 3 'Float -> 'Vec 3 'Float -> 'Vec 3 'Float -> 'Mat 3 4 'Float
 M44F :: 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 4 'Float -> 'Mat 4 4 'Float
-'MatCase :: (a : b:'Nat -> c:'Nat -> d:Type -> 'Mat b c d -> Type) -> ((e : 'Vec 2 'Float) -> (f : 'Vec 2 'Float) -> a 2 2 'Float (M22F e f)) -> ((g : 'Vec 3 'Float) -> (h : 'Vec 3 'Float) -> a 3 2 'Float (M32F g h)) -> ((i : 'Vec 4 'Float) -> (j : 'Vec 4 'Float) -> a 4 2 'Float (M42F i j)) -> ((k : 'Vec 2 'Float) -> (l : 'Vec 2 'Float) -> (m : 'Vec 2 'Float) -> a 2 3 'Float (M23F k l m)) -> ((n : 'Vec 3 'Float) -> (o : 'Vec 3 'Float) -> (p : 'Vec 3 'Float) -> a 3 3 'Float (M33F n o p)) -> ((q : 'Vec 4 'Float) -> (r : 'Vec 4 'Float) -> (s : 'Vec 4 'Float) -> a 4 3 'Float (M43F q r s)) -> ((t : 'Vec 2 'Float) -> (u : 'Vec 2 'Float) -> (v : 'Vec 2 'Float) -> (w : 'Vec 2 'Float) -> a 2 4 'Float (M24F t u v w)) -> ((x : 'Vec 3 'Float) -> (y : 'Vec 3 'Float) -> (z : 'Vec 3 'Float) -> (a' : 'Vec 3 'Float) -> a 3 4 'Float (M34F x y z a')) -> ((b' : 'Vec 4 'Float) -> (c' : 'Vec 4 'Float) -> (d' : 'Vec 4 'Float) -> (e' : 'Vec 4 'Float) -> a 4 4 'Float (M44F b' c' d' e')) -> {f':'Nat} -> {g':'Nat} -> {h'} -> (i' : 'Mat f' g' h') -> a f' g' h' i'
-match'Mat :: (a : Type->Type) -> (b:'Nat -> c:'Nat -> d:Type -> a ('Mat b c d)) -> e:Type -> a e -> a e
+'MatCase :: (a : (b:'Nat) -> (c:'Nat) -> (d:Type) -> 'Mat b c d -> Type) -> ((e : 'Vec 2 'Float) -> (f : 'Vec 2 'Float) -> a 2 2 'Float (M22F e f)) -> ((g : 'Vec 3 'Float) -> (h : 'Vec 3 'Float) -> a 3 2 'Float (M32F g h)) -> ((i : 'Vec 4 'Float) -> (j : 'Vec 4 'Float) -> a 4 2 'Float (M42F i j)) -> ((k : 'Vec 2 'Float) -> (l : 'Vec 2 'Float) -> (m : 'Vec 2 'Float) -> a 2 3 'Float (M23F k l m)) -> ((n : 'Vec 3 'Float) -> (o : 'Vec 3 'Float) -> (p : 'Vec 3 'Float) -> a 3 3 'Float (M33F n o p)) -> ((q : 'Vec 4 'Float) -> (r : 'Vec 4 'Float) -> (s : 'Vec 4 'Float) -> a 4 3 'Float (M43F q r s)) -> ((t : 'Vec 2 'Float) -> (u : 'Vec 2 'Float) -> (v : 'Vec 2 'Float) -> (w : 'Vec 2 'Float) -> a 2 4 'Float (M24F t u v w)) -> ((x : 'Vec 3 'Float) -> (y : 'Vec 3 'Float) -> (z : 'Vec 3 'Float) -> (a' : 'Vec 3 'Float) -> a 3 4 'Float (M34F x y z a')) -> ((b' : 'Vec 4 'Float) -> (c' : 'Vec 4 'Float) -> (d' : 'Vec 4 'Float) -> (e' : 'Vec 4 'Float) -> a 4 4 'Float (M44F b' c' d' e')) -> {f':'Nat} -> {g':'Nat} -> {h'} -> (i' : 'Mat f' g' h') -> a f' g' h' i'
+match'Mat :: (a : Type->Type) -> ((b:'Nat) -> (c:'Nat) -> (d:Type) -> a ('Mat b c d)) -> (e:Type) -> a e -> a e
 'MatVecScalarElem :: Type->Type
 'Signed :: Type->Type
 'Component :: Type->Type
@@ -141,34 +141,34 @@ head :: {a} -> 'List a -> a
 ++ :: {a} -> 'List a -> 'List a -> 'List a
 foldr :: {a} -> {b} -> (b -> a->a) -> a -> 'List b -> a
 concat :: {a} -> 'List ('List a) -> 'List a
-map :: {a} -> {b} -> a->b -> 'List a -> 'List b
+map :: {a} -> {b} -> (a->b) -> 'List a -> 'List b
 concatMap :: {a} -> {b} -> (a -> 'List b) -> 'List a -> 'List b
 len :: {a} -> 'List a -> 'Int
 'Maybe :: Type->Type
 Nothing :: {a} -> 'Maybe a
 Just :: {a} -> a -> 'Maybe a
-'MaybeCase :: {a} -> (b : 'Maybe a -> Type) -> b Nothing -> (c:a -> b (Just c)) -> (d : 'Maybe a) -> b d
-match'Maybe :: (a : Type->Type) -> (b:Type -> a ('Maybe b)) -> c:Type -> a c -> a c
+'MaybeCase :: {a} -> (b : 'Maybe a -> Type) -> b Nothing -> ((c:a) -> b (Just c)) -> (d : 'Maybe a) -> b d
+match'Maybe :: (a : Type->Type) -> ((b:Type) -> a ('Maybe b)) -> (c:Type) -> a c -> a c
 'Vector :: 'Nat -> Type->Type
 'VectorCase :: {a:'Nat} -> {b} -> (c : 'Vector a b -> Type) -> (d : 'Vector a b) -> c d
-match'Vector :: (a : Type->Type) -> (b:'Nat -> c:Type -> a ('Vector b c)) -> d:Type -> a d -> a d
+match'Vector :: (a : Type->Type) -> ((b:'Nat) -> (c:Type) -> a ('Vector b c)) -> (d:Type) -> a d -> a d
 'PrimitiveType :: Type
 Triangle :: 'PrimitiveType
 Line :: 'PrimitiveType
 Point :: 'PrimitiveType
 TriangleAdjacency :: 'PrimitiveType
 LineAdjacency :: 'PrimitiveType
-'PrimitiveTypeCase :: (a : 'PrimitiveType->Type) -> a Triangle -> a Line -> a Point -> a TriangleAdjacency -> a LineAdjacency -> b:'PrimitiveType -> a b
-match'PrimitiveType :: (a : Type->Type) -> a 'PrimitiveType -> b:Type -> a b -> a b
+'PrimitiveTypeCase :: (a : 'PrimitiveType->Type) -> a Triangle -> a Line -> a Point -> a TriangleAdjacency -> a LineAdjacency -> (b:'PrimitiveType) -> a b
+match'PrimitiveType :: (a : Type->Type) -> a 'PrimitiveType -> (b:Type) -> a b -> a b
 'Primitive :: Type -> 'PrimitiveType->Type
 PrimPoint :: {a} -> a -> 'Primitive a Point
 PrimLine :: {a} -> a -> a -> 'Primitive a Line
 PrimTriangle :: {a} -> a -> a -> a -> 'Primitive a Triangle
-'PrimitiveCase :: {a} -> (b : c:'PrimitiveType -> 'Primitive a c -> Type) -> (d:a -> b Point (PrimPoint d)) -> (e:a -> f:a -> b Line (PrimLine e f)) -> (g:a -> h:a -> i:a -> b Triangle (PrimTriangle g h i)) -> {j:'PrimitiveType} -> (k : 'Primitive a j) -> b j k
-match'Primitive :: (a : Type->Type) -> (b:Type -> c:'PrimitiveType -> a ('Primitive b c)) -> d:Type -> a d -> a d
-mapPrimitive :: {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive a c -> 'Primitive b c
+'PrimitiveCase :: {a} -> (b : (c:'PrimitiveType) -> 'Primitive a c -> Type) -> ((d:a) -> b Point (PrimPoint d)) -> ((e:a) -> (f:a) -> b Line (PrimLine e f)) -> ((g:a) -> (h:a) -> (i:a) -> b Triangle (PrimTriangle g h i)) -> {j:'PrimitiveType} -> (k : 'Primitive a j) -> b j k
+match'Primitive :: (a : Type->Type) -> ((b:Type) -> (c:'PrimitiveType) -> a ('Primitive b c)) -> (d:Type) -> a d -> a d
+mapPrimitive :: {a} -> {b} -> {c:'PrimitiveType} -> (a->b) -> 'Primitive a c -> 'Primitive b c
 'PrimitiveStream :: 'PrimitiveType -> Type->Type
-mapPrimitives :: {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'List ('Primitive a c) -> 'List ('Primitive b c)
+mapPrimitives :: {a} -> {b} -> {c:'PrimitiveType} -> (a->b) -> 'List ('Primitive a c) -> 'List ('Primitive b c)
 'ListElem :: Type->Type
 fetchArrays :: {a:'PrimitiveType} -> {b : 'List Type} -> {c : 'List Type} -> {_ : b ~ map Type Type 'ListElem c} -> 'HList c -> 'PrimitiveStream a ('HList b)
 fetch :: {a:'PrimitiveType} -> {b : 'List Type} -> 'String -> 'HList b -> 'PrimitiveStream a ('HList b)
@@ -176,28 +176,28 @@ Attribute :: {a} -> 'String->a
 fetchStream :: {a:'PrimitiveType} -> {b : 'List Type} -> 'String -> (c : 'List 'String) -> {_ : len 'String c ~ len Type b} -> 'PrimitiveStream a ('HList b)
 'SimpleFragment :: Type->Type
 SimpleFragment :: {a} -> 'Vec 3 'Float -> a -> 'SimpleFragment a
-'SimpleFragmentCase :: {a} -> (b : 'SimpleFragment a -> Type) -> ((c : 'Vec 3 'Float) -> d:a -> b (SimpleFragment c d)) -> (e : 'SimpleFragment a) -> b e
-match'SimpleFragment :: (a : Type->Type) -> (b:Type -> a ('SimpleFragment b)) -> c:Type -> a c -> a c
+'SimpleFragmentCase :: {a} -> (b : 'SimpleFragment a -> Type) -> ((c : 'Vec 3 'Float) -> (d:a) -> b (SimpleFragment c d)) -> (e : 'SimpleFragment a) -> b e
+match'SimpleFragment :: (a : Type->Type) -> ((b:Type) -> a ('SimpleFragment b)) -> (c:Type) -> a c -> a c
 'Fragment :: 'Nat -> Type->Type
 sFragmentCoords :: {a} -> 'SimpleFragment a -> 'VecS 'Float 3
 sFragmentValue :: {a} -> 'SimpleFragment a -> a
 'FragmentStream :: 'Nat -> Type->Type
-customizeDepth :: {a} -> {b:'Nat} -> a->'Float -> 'Fragment b a -> 'Fragment b a
-customizeDepths :: {a} -> {b:'Nat} -> a->'Float -> 'List ('Vector b ('Maybe ('SimpleFragment a))) -> 'List ('Vector b ('Maybe ('SimpleFragment a)))
-filterFragment :: {a} -> {b:'Nat} -> a->'Bool -> 'Fragment b a -> 'Fragment b a
-filterFragments :: {a} -> {b:'Nat} -> a->'Bool -> 'List ('Vector b ('Maybe ('SimpleFragment a))) -> 'List ('Vector b ('Maybe ('SimpleFragment a)))
-mapFragment :: {a} -> {b} -> {c:'Nat} -> a->b -> 'Fragment c a -> 'Fragment c b
-mapFragments :: {a} -> {b} -> {c:'Nat} -> a->b -> 'List ('Vector c ('Maybe ('SimpleFragment a))) -> 'List ('Vector c ('Maybe ('SimpleFragment b)))
+customizeDepth :: {a} -> {b:'Nat} -> (a->'Float) -> 'Fragment b a -> 'Fragment b a
+customizeDepths :: {a} -> {b:'Nat} -> (a->'Float) -> 'List ('Vector b ('Maybe ('SimpleFragment a))) -> 'List ('Vector b ('Maybe ('SimpleFragment a)))
+filterFragment :: {a} -> {b:'Nat} -> (a->'Bool) -> 'Fragment b a -> 'Fragment b a
+filterFragments :: {a} -> {b:'Nat} -> (a->'Bool) -> 'List ('Vector b ('Maybe ('SimpleFragment a))) -> 'List ('Vector b ('Maybe ('SimpleFragment a)))
+mapFragment :: {a} -> {b} -> {c:'Nat} -> (a->b) -> 'Fragment c a -> 'Fragment c b
+mapFragments :: {a} -> {b} -> {c:'Nat} -> (a->b) -> 'List ('Vector c ('Maybe ('SimpleFragment a))) -> 'List ('Vector c ('Maybe ('SimpleFragment b)))
 'ImageKind :: Type
 Color :: Type->'ImageKind
 Depth :: 'ImageKind
 Stencil :: 'ImageKind
-'ImageKindCase :: (a : 'ImageKind->Type) -> (b:Type -> a (Color b)) -> a Depth -> a Stencil -> c:'ImageKind -> a c
-match'ImageKind :: (a : Type->Type) -> a 'ImageKind -> b:Type -> a b -> a b
+'ImageKindCase :: (a : 'ImageKind->Type) -> ((b:Type) -> a (Color b)) -> a Depth -> a Stencil -> (c:'ImageKind) -> a c
+match'ImageKind :: (a : Type->Type) -> a 'ImageKind -> (b:Type) -> a b -> a b
 imageType :: 'ImageKind->Type
 'Image :: 'Nat -> 'ImageKind->Type
 'ImageCase :: {a:'Nat} -> {b:'ImageKind} -> (c : 'Image a b -> Type) -> (d : 'Image a b) -> c d
-match'Image :: (a : Type->Type) -> (b:'Nat -> c:'ImageKind -> a ('Image b c)) -> d:Type -> a d -> a d
+match'Image :: (a : Type->Type) -> ((b:'Nat) -> (c:'ImageKind) -> a ('Image b c)) -> (d:Type) -> a d -> a d
 ColorImage :: {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {_ : 'Num c} -> {_ : d ~ 'VecScalar b c} -> d -> 'Image a (Color d)
 DepthImage :: {a:'Nat} -> 'Float -> 'Image a Depth
 StencilImage :: {a:'Nat} -> 'Int -> 'Image a Stencil
@@ -208,8 +208,8 @@ Sx :: 'Swizz
 Sy :: 'Swizz
 Sz :: 'Swizz
 Sw :: 'Swizz
-'SwizzCase :: (a : 'Swizz->Type) -> a Sx -> a Sy -> a Sz -> a Sw -> b:'Swizz -> a b
-match'Swizz :: (a : Type->Type) -> a 'Swizz -> b:Type -> a b -> a b
+'SwizzCase :: (a : 'Swizz->Type) -> a Sx -> a Sy -> a Sz -> a Sw -> (b:'Swizz) -> a b
+match'Swizz :: (a : Type->Type) -> a 'Swizz -> (b:Type) -> a b -> a b
 swizzscalar :: {a} -> {b:'Nat} -> 'Vec b a -> 'Swizz->a
 definedVec :: {a} -> {b:'Nat} -> 'Vec b a -> 'Bool
 swizzvector :: {a} -> {b:'Nat} -> {c:'Nat} -> 'Vec b a -> 'Vec c 'Swizz -> 'VecS a c
@@ -229,16 +229,16 @@ OneMinusConstantColor :: 'BlendingFactor
 ConstantAlpha :: 'BlendingFactor
 OneMinusConstantAlpha :: 'BlendingFactor
 SrcAlphaSaturate :: 'BlendingFactor
-'BlendingFactorCase :: (a : 'BlendingFactor->Type) -> a ZeroBF -> a OneBF -> a SrcColor -> a OneMinusSrcColor -> a DstColor -> a OneMinusDstColor -> a SrcAlpha -> a OneMinusSrcAlpha -> a DstAlpha -> a OneMinusDstAlpha -> a ConstantColor -> a OneMinusConstantColor -> a ConstantAlpha -> a OneMinusConstantAlpha -> a SrcAlphaSaturate -> b:'BlendingFactor -> a b
-match'BlendingFactor :: (a : Type->Type) -> a 'BlendingFactor -> b:Type -> a b -> a b
+'BlendingFactorCase :: (a : 'BlendingFactor->Type) -> a ZeroBF -> a OneBF -> a SrcColor -> a OneMinusSrcColor -> a DstColor -> a OneMinusDstColor -> a SrcAlpha -> a OneMinusSrcAlpha -> a DstAlpha -> a OneMinusDstAlpha -> a ConstantColor -> a OneMinusConstantColor -> a ConstantAlpha -> a OneMinusConstantAlpha -> a SrcAlphaSaturate -> (b:'BlendingFactor) -> a b
+match'BlendingFactor :: (a : Type->Type) -> a 'BlendingFactor -> (b:Type) -> a b -> a b
 'BlendEquation :: Type
 FuncAdd :: 'BlendEquation
 FuncSubtract :: 'BlendEquation
 FuncReverseSubtract :: 'BlendEquation
 Min :: 'BlendEquation
 Max :: 'BlendEquation
-'BlendEquationCase :: (a : 'BlendEquation->Type) -> a FuncAdd -> a FuncSubtract -> a FuncReverseSubtract -> a Min -> a Max -> b:'BlendEquation -> a b
-match'BlendEquation :: (a : Type->Type) -> a 'BlendEquation -> b:Type -> a b -> a b
+'BlendEquationCase :: (a : 'BlendEquation->Type) -> a FuncAdd -> a FuncSubtract -> a FuncReverseSubtract -> a Min -> a Max -> (b:'BlendEquation) -> a b
+match'BlendEquation :: (a : Type->Type) -> a 'BlendEquation -> (b:Type) -> a b -> a b
 'LogicOperation :: Type
 Clear :: 'LogicOperation
 And :: 'LogicOperation
@@ -256,8 +256,8 @@ CopyInverted :: 'LogicOperation
 OrInverted :: 'LogicOperation
 Nand :: 'LogicOperation
 Set :: 'LogicOperation
-'LogicOperationCase :: (a : 'LogicOperation->Type) -> a Clear -> a And -> a AndReverse -> a Copy -> a AndInverted -> a Noop -> a Xor -> a Or -> a Nor -> a Equiv -> a Invert -> a OrReverse -> a CopyInverted -> a OrInverted -> a Nand -> a Set -> b:'LogicOperation -> a b
-match'LogicOperation :: (a : Type->Type) -> a 'LogicOperation -> b:Type -> a b -> a b
+'LogicOperationCase :: (a : 'LogicOperation->Type) -> a Clear -> a And -> a AndReverse -> a Copy -> a AndInverted -> a Noop -> a Xor -> a Or -> a Nor -> a Equiv -> a Invert -> a OrReverse -> a CopyInverted -> a OrInverted -> a Nand -> a Set -> (b:'LogicOperation) -> a b
+match'LogicOperation :: (a : Type->Type) -> a 'LogicOperation -> (b:Type) -> a b -> a b
 'StencilOperation :: Type
 OpZero :: 'StencilOperation
 OpKeep :: 'StencilOperation
@@ -267,8 +267,8 @@ OpIncrWrap :: 'StencilOperation
 OpDecr :: 'StencilOperation
 OpDecrWrap :: 'StencilOperation
 OpInvert :: 'StencilOperation
-'StencilOperationCase :: (a : 'StencilOperation->Type) -> a OpZero -> a OpKeep -> a OpReplace -> a OpIncr -> a OpIncrWrap -> a OpDecr -> a OpDecrWrap -> a OpInvert -> b:'StencilOperation -> a b
-match'StencilOperation :: (a : Type->Type) -> a 'StencilOperation -> b:Type -> a b -> a b
+'StencilOperationCase :: (a : 'StencilOperation->Type) -> a OpZero -> a OpKeep -> a OpReplace -> a OpIncr -> a OpIncrWrap -> a OpDecr -> a OpDecrWrap -> a OpInvert -> (b:'StencilOperation) -> a b
+match'StencilOperation :: (a : Type->Type) -> a 'StencilOperation -> (b:Type) -> a b -> a b
 'ComparisonFunction :: Type
 Never :: 'ComparisonFunction
 Less :: 'ComparisonFunction
@@ -278,72 +278,72 @@ Greater :: 'ComparisonFunction
 Notequal :: 'ComparisonFunction
 Gequal :: 'ComparisonFunction
 Always :: 'ComparisonFunction
-'ComparisonFunctionCase :: (a : 'ComparisonFunction->Type) -> a Never -> a Less -> a Equal -> a Lequal -> a Greater -> a Notequal -> a Gequal -> a Always -> b:'ComparisonFunction -> a b
-match'ComparisonFunction :: (a : Type->Type) -> a 'ComparisonFunction -> b:Type -> a b -> a b
+'ComparisonFunctionCase :: (a : 'ComparisonFunction->Type) -> a Never -> a Less -> a Equal -> a Lequal -> a Greater -> a Notequal -> a Gequal -> a Always -> (b:'ComparisonFunction) -> a b
+match'ComparisonFunction :: (a : Type->Type) -> a 'ComparisonFunction -> (b:Type) -> a b -> a b
 'ProvokingVertex :: Type
 LastVertex :: 'ProvokingVertex
 FirstVertex :: 'ProvokingVertex
-'ProvokingVertexCase :: (a : 'ProvokingVertex->Type) -> a LastVertex -> a FirstVertex -> b:'ProvokingVertex -> a b
-match'ProvokingVertex :: (a : Type->Type) -> a 'ProvokingVertex -> b:Type -> a b -> a b
+'ProvokingVertexCase :: (a : 'ProvokingVertex->Type) -> a LastVertex -> a FirstVertex -> (b:'ProvokingVertex) -> a b
+match'ProvokingVertex :: (a : Type->Type) -> a 'ProvokingVertex -> (b:Type) -> a b -> a b
 'CullMode :: Type
 CullFront :: 'CullMode
 CullBack :: 'CullMode
 CullNone :: 'CullMode
-'CullModeCase :: (a : 'CullMode->Type) -> a CullFront -> a CullBack -> a CullNone -> b:'CullMode -> a b
-match'CullMode :: (a : Type->Type) -> a 'CullMode -> b:Type -> a b -> a b
+'CullModeCase :: (a : 'CullMode->Type) -> a CullFront -> a CullBack -> a CullNone -> (b:'CullMode) -> a b
+match'CullMode :: (a : Type->Type) -> a 'CullMode -> (b:Type) -> a b -> a b
 'PointSize :: Type->Type
 PointSize :: {a} -> 'Float -> 'PointSize a
-ProgramPointSize :: {a} -> a->'Float -> 'PointSize a
-'PointSizeCase :: {a} -> (b : 'PointSize a -> Type) -> (c:'Float -> b (PointSize c)) -> ((d : a->'Float) -> b (ProgramPointSize d)) -> (e : 'PointSize a) -> b e
-match'PointSize :: (a : Type->Type) -> (b:Type -> a ('PointSize b)) -> c:Type -> a c -> a c
+ProgramPointSize :: {a} -> (a->'Float) -> 'PointSize a
+'PointSizeCase :: {a} -> (b : 'PointSize a -> Type) -> ((c:'Float) -> b (PointSize c)) -> ((d : a->'Float) -> b (ProgramPointSize d)) -> (e : 'PointSize a) -> b e
+match'PointSize :: (a : Type->Type) -> ((b:Type) -> a ('PointSize b)) -> (c:Type) -> a c -> a c
 'PolygonMode :: Type->Type
 PolygonFill :: {a} -> 'PolygonMode a
 PolygonPoint :: {a} -> 'PointSize a -> 'PolygonMode a
 PolygonLine :: {a} -> 'Float -> 'PolygonMode a
-'PolygonModeCase :: {a} -> (b : 'PolygonMode a -> Type) -> b PolygonFill -> ((c : 'PointSize a) -> b (PolygonPoint c)) -> (d:'Float -> b (PolygonLine d)) -> (e : 'PolygonMode a) -> b e
-match'PolygonMode :: (a : Type->Type) -> (b:Type -> a ('PolygonMode b)) -> c:Type -> a c -> a c
+'PolygonModeCase :: {a} -> (b : 'PolygonMode a -> Type) -> b PolygonFill -> ((c : 'PointSize a) -> b (PolygonPoint c)) -> ((d:'Float) -> b (PolygonLine d)) -> (e : 'PolygonMode a) -> b e
+match'PolygonMode :: (a : Type->Type) -> ((b:Type) -> a ('PolygonMode b)) -> (c:Type) -> a c -> a c
 'PolygonOffset :: Type
 NoOffset :: 'PolygonOffset
 Offset :: 'Float -> 'Float->'PolygonOffset
-'PolygonOffsetCase :: (a : 'PolygonOffset->Type) -> a NoOffset -> (b:'Float -> c:'Float -> a (Offset b c)) -> d:'PolygonOffset -> a d
-match'PolygonOffset :: (a : Type->Type) -> a 'PolygonOffset -> b:Type -> a b -> a b
+'PolygonOffsetCase :: (a : 'PolygonOffset->Type) -> a NoOffset -> ((b:'Float) -> (c:'Float) -> a (Offset b c)) -> (d:'PolygonOffset) -> a d
+match'PolygonOffset :: (a : Type->Type) -> a 'PolygonOffset -> (b:Type) -> a b -> a b
 'PointSpriteCoordOrigin :: Type
 LowerLeft :: 'PointSpriteCoordOrigin
 UpperLeft :: 'PointSpriteCoordOrigin
-'PointSpriteCoordOriginCase :: (a : 'PointSpriteCoordOrigin->Type) -> a LowerLeft -> a UpperLeft -> b:'PointSpriteCoordOrigin -> a b
-match'PointSpriteCoordOrigin :: (a : Type->Type) -> a 'PointSpriteCoordOrigin -> b:Type -> a b -> a b
+'PointSpriteCoordOriginCase :: (a : 'PointSpriteCoordOrigin->Type) -> a LowerLeft -> a UpperLeft -> (b:'PointSpriteCoordOrigin) -> a b
+match'PointSpriteCoordOrigin :: (a : Type->Type) -> a 'PointSpriteCoordOrigin -> (b:Type) -> a b -> a b
 primTexture :: () -> 'Vec 2 'Float -> 'Vec 4 'Float
 Uniform :: {a} -> 'String->a
 'RasterContext :: Type -> 'PrimitiveType->Type
 TriangleCtx :: {a} -> 'CullMode -> 'PolygonMode a -> 'PolygonOffset -> 'ProvokingVertex -> 'RasterContext a Triangle
 PointCtx :: {a} -> 'PointSize a -> 'Float -> 'PointSpriteCoordOrigin -> 'RasterContext a Point
 LineCtx :: {a} -> 'Float -> 'ProvokingVertex -> 'RasterContext a Line
-'RasterContextCase :: {a} -> (b : c:'PrimitiveType -> 'RasterContext a c -> Type) -> (d:'CullMode -> (e : 'PolygonMode a) -> f:'PolygonOffset -> g:'ProvokingVertex -> b Triangle (TriangleCtx d e f g)) -> ((h : 'PointSize a) -> i:'Float -> j:'PointSpriteCoordOrigin -> b Point (PointCtx h i j)) -> (k:'Float -> l:'ProvokingVertex -> b Line (LineCtx k l)) -> {m:'PrimitiveType} -> (n : 'RasterContext a m) -> b m n
-match'RasterContext :: (a : Type->Type) -> (b:Type -> c:'PrimitiveType -> a ('RasterContext b c)) -> d:Type -> a d -> a d
+'RasterContextCase :: {a} -> (b : (c:'PrimitiveType) -> 'RasterContext a c -> Type) -> ((d:'CullMode) -> (e : 'PolygonMode a) -> (f:'PolygonOffset) -> (g:'ProvokingVertex) -> b Triangle (TriangleCtx d e f g)) -> ((h : 'PointSize a) -> (i:'Float) -> (j:'PointSpriteCoordOrigin) -> b Point (PointCtx h i j)) -> ((k:'Float) -> (l:'ProvokingVertex) -> b Line (LineCtx k l)) -> {m:'PrimitiveType} -> (n : 'RasterContext a m) -> b m n
+match'RasterContext :: (a : Type->Type) -> ((b:Type) -> (c:'PrimitiveType) -> a ('RasterContext b c)) -> (d:Type) -> a d -> a d
 'Blending :: Type->Type
 NoBlending :: {a} -> 'Blending a
 BlendLogicOp :: {a} -> {_ : 'Integral a} -> 'LogicOperation -> 'Blending a
 Blend :: ('BlendEquation, 'BlendEquation) -> (('BlendingFactor, 'BlendingFactor), ('BlendingFactor, 'BlendingFactor)) -> 'Vec 4 'Float -> 'Blending 'Float
-'BlendingCase :: (a : b:Type -> 'Blending b -> Type) -> ({c} -> a c (NoBlending c)) -> ({d} -> {e : 'Integral d} -> f:'LogicOperation -> a d (BlendLogicOp d e f)) -> (g:('BlendEquation, 'BlendEquation) -> h:(('BlendingFactor, 'BlendingFactor), ('BlendingFactor, 'BlendingFactor)) -> (i : 'Vec 4 'Float) -> a 'Float (Blend g h i)) -> {j} -> (k : 'Blending j) -> a j k
-match'Blending :: (a : Type->Type) -> (b:Type -> a ('Blending b)) -> c:Type -> a c -> a c
+'BlendingCase :: (a : (b:Type) -> 'Blending b -> Type) -> ({c} -> a c (NoBlending c)) -> ({d} -> {e : 'Integral d} -> (f:'LogicOperation) -> a d (BlendLogicOp d e f)) -> ((g:('BlendEquation, 'BlendEquation)) -> (h:(('BlendingFactor, 'BlendingFactor), ('BlendingFactor, 'BlendingFactor))) -> (i : 'Vec 4 'Float) -> a 'Float (Blend g h i)) -> {j} -> (k : 'Blending j) -> a j k
+match'Blending :: (a : Type->Type) -> ((b:Type) -> a ('Blending b)) -> (c:Type) -> a c -> a c
 'StencilTests :: Type
-'StencilTestsCase :: (a : 'StencilTests->Type) -> b:'StencilTests -> a b
-match'StencilTests :: (a : Type->Type) -> a 'StencilTests -> b:Type -> a b -> a b
+'StencilTestsCase :: (a : 'StencilTests->Type) -> (b:'StencilTests) -> a b
+match'StencilTests :: (a : Type->Type) -> a 'StencilTests -> (b:Type) -> a b -> a b
 'StencilOps :: Type
-'StencilOpsCase :: (a : 'StencilOps->Type) -> b:'StencilOps -> a b
-match'StencilOps :: (a : Type->Type) -> a 'StencilOps -> b:Type -> a b -> a b
+'StencilOpsCase :: (a : 'StencilOps->Type) -> (b:'StencilOps) -> a b
+match'StencilOps :: (a : Type->Type) -> a 'StencilOps -> (b:Type) -> a b -> a b
 'FragmentOperation :: 'ImageKind->Type
 ColorOp :: {a} -> {b:'Nat} -> {_ : 'Num a} -> 'Blending a -> 'VecScalar b 'Bool -> 'FragmentOperation (Color ('VecScalar b a))
 DepthOp :: 'ComparisonFunction -> 'Bool -> 'FragmentOperation Depth
 StencilOp :: 'StencilTests -> 'StencilOps -> 'StencilOps -> 'FragmentOperation Stencil
-'FragmentOperationCase :: (a : b:'ImageKind -> 'FragmentOperation b -> Type) -> ({c} -> {d:'Nat} -> {e : 'Num c} -> (f : 'Blending c) -> (g : 'VecScalar d 'Bool) -> a (Color ('VecScalar d c)) (ColorOp c d e f g)) -> (h:'ComparisonFunction -> i:'Bool -> a Depth (DepthOp h i)) -> (j:'StencilTests -> k:'StencilOps -> l:'StencilOps -> a Stencil (StencilOp j k l)) -> {m:'ImageKind} -> (n : 'FragmentOperation m) -> a m n
-match'FragmentOperation :: (a : Type->Type) -> (b:'ImageKind -> a ('FragmentOperation b)) -> c:Type -> a c -> a c
+'FragmentOperationCase :: (a : (b:'ImageKind) -> 'FragmentOperation b -> Type) -> ({c} -> {d:'Nat} -> {e : 'Num c} -> (f : 'Blending c) -> (g : 'VecScalar d 'Bool) -> a (Color ('VecScalar d c)) (ColorOp c d e f g)) -> ((h:'ComparisonFunction) -> (i:'Bool) -> a Depth (DepthOp h i)) -> ((j:'StencilTests) -> (k:'StencilOps) -> (l:'StencilOps) -> a Stencil (StencilOp j k l)) -> {m:'ImageKind} -> (n : 'FragmentOperation m) -> a m n
+match'FragmentOperation :: (a : Type->Type) -> ((b:'ImageKind) -> a ('FragmentOperation b)) -> (c:Type) -> a c -> a c
 'Interpolated :: Type->Type
 Smooth :: {a} -> {_ : 'Floating a} -> 'Interpolated a
 NoPerspective :: {a} -> {_ : 'Floating a} -> 'Interpolated a
 Flat :: {a} -> 'Interpolated a
 'InterpolatedCase :: {a} -> (b : 'Interpolated a -> Type) -> ({c : 'Floating a} -> b (Smooth c)) -> ({d : 'Floating a} -> b (NoPerspective d)) -> b Flat -> (e : 'Interpolated a) -> b e
-match'Interpolated :: (a : Type->Type) -> (b:Type -> a ('Interpolated b)) -> c:Type -> a c -> a c
+match'Interpolated :: (a : Type->Type) -> ((b:Type) -> a ('Interpolated b)) -> (c:Type) -> a c -> a c
 rasterizePrimitive :: {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)
 rasterizePrimitives :: {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))))
 'ImageLC :: Type->'Nat
@@ -351,7 +351,7 @@ allSame :: {a} -> 'List a -> Type
 sameLayerCounts :: 'List Type -> Type
 'FrameBuffer :: 'Nat -> 'List 'ImageKind -> Type
 'FrameBufferCase :: {a:'Nat} -> {b : 'List 'ImageKind} -> (c : 'FrameBuffer a b -> Type) -> (d : 'FrameBuffer a b) -> c d
-match'FrameBuffer :: (a : Type->Type) -> (b:'Nat -> (c : 'List 'ImageKind) -> a ('FrameBuffer b c)) -> d:Type -> a d -> a d
+match'FrameBuffer :: (a : Type->Type) -> ((b:'Nat) -> (c : 'List 'ImageKind) -> a ('FrameBuffer b c)) -> (d:Type) -> a d -> a d
 imageType' :: 'List 'ImageKind -> 'List Type
 'FragmentOperationKind :: Type->'ImageKind
 Accumulate :: {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
@@ -365,29 +365,29 @@ PrjImage :: {a:'ImageKind} -> 'FrameBuffer 1 (Cons a Nil) -> 'Image 1 a[39
 PrjImageColor :: 'FrameBuffer 1 (Cons Depth (Cons (Color ('Vec 4 'Float)) Nil)) -> 'Image 1 (Color ('Vec 4 'Float))
 'Output :: Type
 ScreenOut :: {a:'Nat} -> {b : 'List 'ImageKind} -> 'FrameBuffer a b -> 'Output
-'OutputCase :: (a : 'Output->Type) -> ({b:'Nat} -> {c : 'List 'ImageKind} -> (d : 'FrameBuffer b c) -> a (ScreenOut b c d)) -> e:'Output -> a e
-match'Output :: (a : Type->Type) -> a 'Output -> b:Type -> a b -> a b
+'OutputCase :: (a : 'Output->Type) -> ({b:'Nat} -> {c : 'List 'ImageKind} -> (d : 'FrameBuffer b c) -> a (ScreenOut b c d)) -> (e:'Output) -> a e
+match'Output :: (a : Type->Type) -> a 'Output -> (b:Type) -> a b -> a b
 renderFrame :: {a:'Nat} -> {b : 'List 'ImageKind} -> 'FrameBuffer a b -> 'Output
 'Texture :: Type
 Texture2DSlot :: 'String->'Texture
 Texture2D :: 'Vec 2 'Int -> 'Image 1 (Color ('Vec 4 'Float)) -> 'Texture
-'TextureCase :: (a : 'Texture->Type) -> (b:'String -> a (Texture2DSlot b)) -> ((c : 'Vec 2 'Int) -> (d : 'Image 1 (Color ('Vec 4 'Float))) -> a (Texture2D c d)) -> e:'Texture -> a e
-match'Texture :: (a : Type->Type) -> a 'Texture -> b:Type -> a b -> a b
+'TextureCase :: (a : 'Texture->Type) -> ((b:'String) -> a (Texture2DSlot b)) -> ((c : 'Vec 2 'Int) -> (d : 'Image 1 (Color ('Vec 4 'Float))) -> a (Texture2D c d)) -> (e:'Texture) -> a e
+match'Texture :: (a : Type->Type) -> a 'Texture -> (b:Type) -> a b -> a b
 'Filter :: Type
 PointFilter :: 'Filter
 LinearFilter :: 'Filter
-'FilterCase :: (a : 'Filter->Type) -> a PointFilter -> a LinearFilter -> b:'Filter -> a b
-match'Filter :: (a : Type->Type) -> a 'Filter -> b:Type -> a b -> a b
+'FilterCase :: (a : 'Filter->Type) -> a PointFilter -> a LinearFilter -> (b:'Filter) -> a b
+match'Filter :: (a : Type->Type) -> a 'Filter -> (b:Type) -> a b -> a b
 'EdgeMode :: Type
 Repeat :: 'EdgeMode
 MirroredRepeat :: 'EdgeMode
 ClampToEdge :: 'EdgeMode
-'EdgeModeCase :: (a : 'EdgeMode->Type) -> a Repeat -> a MirroredRepeat -> a ClampToEdge -> b:'EdgeMode -> a b
-match'EdgeMode :: (a : Type->Type) -> a 'EdgeMode -> b:Type -> a b -> a b
+'EdgeModeCase :: (a : 'EdgeMode->Type) -> a Repeat -> a MirroredRepeat -> a ClampToEdge -> (b:'EdgeMode) -> a b
+match'EdgeMode :: (a : Type->Type) -> a 'EdgeMode -> (b:Type) -> a b -> a b
 'Sampler :: Type
 Sampler :: 'Filter -> 'EdgeMode -> 'Texture->'Sampler
-'SamplerCase :: (a : 'Sampler->Type) -> (b:'Filter -> c:'EdgeMode -> d:'Texture -> a (Sampler b c d)) -> e:'Sampler -> a e
-match'Sampler :: (a : Type->Type) -> a 'Sampler -> b:Type -> a b -> a b
+'SamplerCase :: (a : 'Sampler->Type) -> ((b:'Filter) -> (c:'EdgeMode) -> (d:'Texture) -> a (Sampler b c d)) -> (e:'Sampler) -> a e
+match'Sampler :: (a : Type->Type) -> a 'Sampler -> (b:Type) -> a b -> a b
 texture2D :: 'Sampler -> 'Vec 2 'Float -> 'Vec 4 'Float
 accumulationContext :: {a} -> a->a
 ------------ tooltips
@@ -452,12 +452,12 @@ testdata/Builtins.lc 19:35-19:41  Nat->Type
 testdata/Builtins.lc 19:35-19:43  Type
 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: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  VecS d_ b_ -> VecS d_ c_ | c_->c_ -> VecS d_ b_ -> VecS d_ c_ | {a:Nat} -> VecS f_ a -> VecS f_ 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:25-20:28  f_
 testdata/Builtins.lc 20:27-20:28  c_
@@ -540,7 +540,7 @@ testdata/Builtins.lc 33:41-33:46  Nat -> Type->Type
 testdata/Builtins.lc 33:41-33:48  Type->Type
 testdata/Builtins.lc 33:41-33:54  Type
 testdata/Builtins.lc 33:45-33:46  b_
-testdata/Builtins.lc 33:45-33:48  a:Type -> Mat 2 2 a -> Type
+testdata/Builtins.lc 33:45-33:48  (a:Type) -> Mat 2 2 a -> Type
 testdata/Builtins.lc 33:45-33:54  Mat 2 2 Float -> Type
 testdata/Builtins.lc 33:47-33:48  b_
 testdata/Builtins.lc 33:49-33:54  Type
@@ -562,7 +562,7 @@ testdata/Builtins.lc 34:41-34:46  Nat -> Type->Type
 testdata/Builtins.lc 34:41-34:48  Type->Type
 testdata/Builtins.lc 34:41-34:54  Type
 testdata/Builtins.lc 34:45-34:46  b_
-testdata/Builtins.lc 34:45-34:48  a:Type -> Mat 3 2 a -> Type
+testdata/Builtins.lc 34:45-34:48  (a:Type) -> Mat 3 2 a -> Type
 testdata/Builtins.lc 34:45-34:54  Mat 3 2 Float -> Type
 testdata/Builtins.lc 34:47-34:48  b_
 testdata/Builtins.lc 34:49-34:54  Type
@@ -584,7 +584,7 @@ testdata/Builtins.lc 35:41-35:46  Nat -> Type->Type
 testdata/Builtins.lc 35:41-35:48  Type->Type
 testdata/Builtins.lc 35:41-35:54  Type
 testdata/Builtins.lc 35:45-35:46  b_
-testdata/Builtins.lc 35:45-35:48  a:Type -> Mat 4 2 a -> Type
+testdata/Builtins.lc 35:45-35:48  (a:Type) -> Mat 4 2 a -> Type
 testdata/Builtins.lc 35:45-35:54  Mat 4 2 Float -> Type
 testdata/Builtins.lc 35:47-35:48  b_
 testdata/Builtins.lc 35:49-35:54  Type
@@ -612,7 +612,7 @@ testdata/Builtins.lc 36:56-36:61  Nat -> Type->Type
 testdata/Builtins.lc 36:56-36:63  Type->Type
 testdata/Builtins.lc 36:56-36:69  Type
 testdata/Builtins.lc 36:60-36:61  b_
-testdata/Builtins.lc 36:60-36:63  a:Type -> Mat 2 3 a -> Type
+testdata/Builtins.lc 36:60-36:63  (a:Type) -> Mat 2 3 a -> Type
 testdata/Builtins.lc 36:60-36:69  Mat 2 3 Float -> Type
 testdata/Builtins.lc 36:62-36:63  b_
 testdata/Builtins.lc 36:64-36:69  Type
@@ -640,7 +640,7 @@ testdata/Builtins.lc 37:56-37:61  Nat -> Type->Type
 testdata/Builtins.lc 37:56-37:63  Type->Type
 testdata/Builtins.lc 37:56-37:69  Type
 testdata/Builtins.lc 37:60-37:61  b_
-testdata/Builtins.lc 37:60-37:63  a:Type -> Mat 3 3 a -> Type
+testdata/Builtins.lc 37:60-37:63  (a:Type) -> Mat 3 3 a -> Type
 testdata/Builtins.lc 37:60-37:69  Mat 3 3 Float -> Type
 testdata/Builtins.lc 37:62-37:63  b_
 testdata/Builtins.lc 37:64-37:69  Type
@@ -668,7 +668,7 @@ testdata/Builtins.lc 38:56-38:61  Nat -> Type->Type
 testdata/Builtins.lc 38:56-38:63  Type->Type
 testdata/Builtins.lc 38:56-38:69  Type
 testdata/Builtins.lc 38:60-38:61  b_
-testdata/Builtins.lc 38:60-38:63  a:Type -> Mat 4 3 a -> Type
+testdata/Builtins.lc 38:60-38:63  (a:Type) -> Mat 4 3 a -> Type
 testdata/Builtins.lc 38:60-38:69  Mat 4 3 Float -> Type
 testdata/Builtins.lc 38:62-38:63  b_
 testdata/Builtins.lc 38:64-38:69  Type
@@ -702,7 +702,7 @@ testdata/Builtins.lc 39:71-39:76  Nat -> Type->Type
 testdata/Builtins.lc 39:71-39:78  Type->Type
 testdata/Builtins.lc 39:71-39:84  Type
 testdata/Builtins.lc 39:75-39:76  b_
-testdata/Builtins.lc 39:75-39:78  a:Type -> Mat 2 4 a -> Type
+testdata/Builtins.lc 39:75-39:78  (a:Type) -> Mat 2 4 a -> Type
 testdata/Builtins.lc 39:75-39:84  Mat 2 4 Float -> Type
 testdata/Builtins.lc 39:77-39:78  b_
 testdata/Builtins.lc 39:79-39:84  Type
@@ -736,7 +736,7 @@ testdata/Builtins.lc 40:71-40:76  Nat -> Type->Type
 testdata/Builtins.lc 40:71-40:78  Type->Type
 testdata/Builtins.lc 40:71-40:84  Type
 testdata/Builtins.lc 40:75-40:76  b_
-testdata/Builtins.lc 40:75-40:78  a:Type -> Mat 3 4 a -> Type
+testdata/Builtins.lc 40:75-40:78  (a:Type) -> Mat 3 4 a -> Type
 testdata/Builtins.lc 40:75-40:84  Mat 3 4 Float -> Type
 testdata/Builtins.lc 40:77-40:78  b_
 testdata/Builtins.lc 40:79-40:84  Type
@@ -770,7 +770,7 @@ testdata/Builtins.lc 41:71-41:76  Nat -> Type->Type
 testdata/Builtins.lc 41:71-41:78  Type->Type
 testdata/Builtins.lc 41:71-41:84  Type
 testdata/Builtins.lc 41:75-41:76  b_
-testdata/Builtins.lc 41:75-41:78  a:Type -> Mat 4 4 a -> Type
+testdata/Builtins.lc 41:75-41:78  (a:Type) -> Mat 4 4 a -> Type
 testdata/Builtins.lc 41:75-41:84  Mat 4 4 Float -> Type
 testdata/Builtins.lc 41:77-41:78  b_
 testdata/Builtins.lc 41:79-41:84  Type
@@ -811,22 +811,22 @@ testdata/Builtins.lc 69:9-90:31  b_
 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  VecS b_ a_ | a:Nat -> VecS b_ a | a:Type -> b:Nat -> VecS a b
+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: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  VecS b_ a_ | a:Nat -> VecS b_ a | a:Type -> b:Nat -> VecS a b
+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: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
 testdata/Builtins.lc 74:10-74:16  Float -> Float -> VecS Float 3
 testdata/Builtins.lc 74:10-74:20  Float -> VecS Float 3
 testdata/Builtins.lc 74:10-74:24  VecS Float 3
-testdata/Builtins.lc 74:10-77:28  a:Nat -> VecS Float ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 74:10-77:28  (a:Nat) -> VecS Float ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 74:13-74:16  Float
 testdata/Builtins.lc 74:17-74:20  Float
 testdata/Builtins.lc 74:21-74:24  Float
@@ -834,7 +834,7 @@ testdata/Builtins.lc 75:9-75:11  {a} -> a -> a -> a -> VecS a 3
 testdata/Builtins.lc 75:9-75:15  Float -> Float -> VecS Float 3
 testdata/Builtins.lc 75:9-75:19  Float -> VecS Float 3
 testdata/Builtins.lc 75:9-75:23  VecS Float 3
-testdata/Builtins.lc 75:9-78:27  a:Nat -> VecS Float ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 75:9-78:27  (a:Nat) -> VecS Float ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 75:12-75:15  Float
 testdata/Builtins.lc 75:16-75:19  Float
 testdata/Builtins.lc 75:20-75:23  Float
@@ -842,7 +842,7 @@ testdata/Builtins.lc 77:10-77:12  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 77:10-77:16  Float -> Float -> Float -> VecS Float 4
 testdata/Builtins.lc 77:10-77:20  Float -> Float -> VecS Float 4
 testdata/Builtins.lc 77:10-77:24  Float -> VecS Float 4
-testdata/Builtins.lc 77:10-77:28  VecS Float 4 | a:Nat -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 77:10-77:28  (a:Nat) -> VecS Float ('Succ ('Succ ('Succ ('Succ a)))) | VecS Float 4
 testdata/Builtins.lc 77:13-77:16  Float
 testdata/Builtins.lc 77:17-77:20  Float
 testdata/Builtins.lc 77:21-77:24  Float
@@ -851,7 +851,7 @@ testdata/Builtins.lc 78:9-78:11  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 78:9-78:15  Float -> Float -> Float -> VecS Float 4
 testdata/Builtins.lc 78:9-78:19  Float -> Float -> VecS Float 4
 testdata/Builtins.lc 78:9-78:23  Float -> VecS Float 4
-testdata/Builtins.lc 78:9-78:27  VecS Float 4 | a:Nat -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 78:9-78:27  (a:Nat) -> VecS Float ('Succ ('Succ ('Succ ('Succ a)))) | VecS Float 4
 testdata/Builtins.lc 78:12-78:15  Float
 testdata/Builtins.lc 78:16-78:19  Float
 testdata/Builtins.lc 78:20-78:23  Float
@@ -861,20 +861,20 @@ testdata/Builtins.lc 81:9-81:13  Bool
 testdata/Builtins.lc 83:10-83:12  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 83:10-83:18  Bool -> VecS Bool 2
 testdata/Builtins.lc 83:10-83:24  VecS Bool 2
-testdata/Builtins.lc 83:10-89:36  a:Nat -> VecS Bool ('Succ ('Succ a)) | a:Nat -> VecS Bool ('Succ a)
+testdata/Builtins.lc 83:10-89:36  (a:Nat) -> VecS Bool ('Succ ('Succ a)) | (a:Nat) -> VecS Bool ('Succ a)
 testdata/Builtins.lc 83:13-83:18  Bool
 testdata/Builtins.lc 83:19-83:24  Bool
 testdata/Builtins.lc 84:9-84:11  {a} -> a -> a -> VecS a 2
 testdata/Builtins.lc 84:9-84:16  Bool -> VecS Bool 2
 testdata/Builtins.lc 84:9-84:21  VecS Bool 2
-testdata/Builtins.lc 84:9-90:31  a:Nat -> VecS Bool ('Succ ('Succ a)) | a:Nat -> VecS Bool ('Succ a)
+testdata/Builtins.lc 84:9-90:31  (a:Nat) -> VecS Bool ('Succ ('Succ a)) | (a:Nat) -> VecS Bool ('Succ a)
 testdata/Builtins.lc 84:12-84:16  Bool
 testdata/Builtins.lc 84:17-84:21  Bool
 testdata/Builtins.lc 86:10-86:12  {a} -> a -> a -> a -> VecS a 3
 testdata/Builtins.lc 86:10-86:18  Bool -> Bool -> VecS Bool 3
 testdata/Builtins.lc 86:10-86:24  Bool -> VecS Bool 3
 testdata/Builtins.lc 86:10-86:30  VecS Bool 3
-testdata/Builtins.lc 86:10-89:36  a:Nat -> VecS Bool ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 86:10-89:36  (a:Nat) -> VecS Bool ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 86:13-86:18  Bool
 testdata/Builtins.lc 86:19-86:24  Bool
 testdata/Builtins.lc 86:25-86:30  Bool
@@ -882,7 +882,7 @@ testdata/Builtins.lc 87:9-87:11  {a} -> a -> a -> a -> VecS a 3
 testdata/Builtins.lc 87:9-87:16  Bool -> Bool -> VecS Bool 3
 testdata/Builtins.lc 87:9-87:21  Bool -> VecS Bool 3
 testdata/Builtins.lc 87:9-87:26  VecS Bool 3
-testdata/Builtins.lc 87:9-90:31  a:Nat -> VecS Bool ('Succ ('Succ ('Succ a)))
+testdata/Builtins.lc 87:9-90:31  (a:Nat) -> VecS Bool ('Succ ('Succ ('Succ a)))
 testdata/Builtins.lc 87:12-87:16  Bool
 testdata/Builtins.lc 87:17-87:21  Bool
 testdata/Builtins.lc 87:22-87:26  Bool
@@ -890,7 +890,7 @@ testdata/Builtins.lc 89:10-89:12  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 89:10-89:18  Bool -> Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 89:10-89:24  Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 89:10-89:30  Bool -> VecS Bool 4
-testdata/Builtins.lc 89:10-89:36  VecS Bool 4 | a:Nat -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 89:10-89:36  (a:Nat) -> VecS Bool ('Succ ('Succ ('Succ ('Succ a)))) | VecS Bool 4
 testdata/Builtins.lc 89:13-89:18  Bool
 testdata/Builtins.lc 89:19-89:24  Bool
 testdata/Builtins.lc 89:25-89:30  Bool
@@ -899,7 +899,7 @@ testdata/Builtins.lc 90:9-90:11  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Builtins.lc 90:9-90:16  Bool -> Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 90:9-90:21  Bool -> Bool -> VecS Bool 4
 testdata/Builtins.lc 90:9-90:26  Bool -> VecS Bool 4
-testdata/Builtins.lc 90:9-90:31  VecS Bool 4 | a:Nat -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
+testdata/Builtins.lc 90:9-90:31  (a:Nat) -> VecS Bool ('Succ ('Succ ('Succ ('Succ a)))) | VecS Bool 4
 testdata/Builtins.lc 90:12-90:16  Bool
 testdata/Builtins.lc 90:17-90:21  Bool
 testdata/Builtins.lc 90:22-90:26  Bool
@@ -1892,7 +1892,7 @@ 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: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: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 212:16-212:17  i_
@@ -1915,7 +1915,7 @@ 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:25-215:28  {a} -> {b} -> a->b -> List a -> 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:32  List (List c_)
 testdata/Builtins.lc 215:29-215:30  g_ -> List g_
@@ -1984,7 +1984,7 @@ testdata/Builtins.lc 241:36-241:47  PrimitiveType->Type
 testdata/Builtins.lc 241:36-241:56  Type
 testdata/Builtins.lc 241:46-241:47  Type
 testdata/Builtins.lc 241:48-241:56  PrimitiveType
-testdata/Builtins.lc 243:1-243:13  {a} -> {b} -> {c:PrimitiveType} -> a->b -> Primitive a c -> Primitive b c
+testdata/Builtins.lc 243:1-243:13  {a} -> {b} -> {c:PrimitiveType} -> (a->b) -> Primitive a c -> Primitive b c
 testdata/Builtins.lc 243:17-243:59  Type
 testdata/Builtins.lc 243:18-243:19  f_
 testdata/Builtins.lc 243:23-243:24  Type | e_
@@ -2020,10 +2020,10 @@ testdata/Builtins.lc 252:53-252:70  Type->Type
 testdata/Builtins.lc 252:53-252:72  Type
 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  List (Primitive e_ a_) -> List (Primitive e_ b_) | c_->c_ -> PrimitiveStream b_ d_ -> PrimitiveStream c_ d_
-testdata/Builtins.lc 253:24-253:36  {a} -> {b} -> {c:PrimitiveType} -> a->b -> Primitive a c -> Primitive b c
+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: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 255:30-255:38  Type->Type
@@ -2034,7 +2034,7 @@ testdata/Builtins.lc 260:56-260:57  e_
 testdata/Builtins.lc 260:56-260:59  d_->Type
 testdata/Builtins.lc 260:56-260:75  Type
 testdata/Builtins.lc 260:58-260:59  {a} -> a -> a->Type
-testdata/Builtins.lc 260:60-260:63  {a} -> {b} -> a->b -> List a -> List b
+testdata/Builtins.lc 260:60-260:63  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 260:60-260:72  List Type -> List Type
 testdata/Builtins.lc 260:60-260:75  List Type
 testdata/Builtins.lc 260:64-260:72  Type->Type
@@ -2125,7 +2125,7 @@ testdata/Builtins.lc 277:28-277:38  Type->Type
 testdata/Builtins.lc 277:28-277:40  Type
 testdata/Builtins.lc 277:37-277:38  d_
 testdata/Builtins.lc 277:39-277:40  b_
-testdata/Builtins.lc 279:1-279:15  {a} -> {b:Nat} -> a->Float -> Fragment b a -> Fragment b a
+testdata/Builtins.lc 279:1-279:15  {a} -> {b:Nat} -> (a->Float) -> Fragment b a -> Fragment b a
 testdata/Builtins.lc 279:19-279:63  Type
 testdata/Builtins.lc 279:20-279:21  d_
 testdata/Builtins.lc 279:25-279:30  Type
@@ -2154,13 +2154,13 @@ testdata/Builtins.lc 281:58-281:74  Type->Type
 testdata/Builtins.lc 281:58-281:76  Type
 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  List (Vector a_ (Maybe (SimpleFragment d_))) -> List (Vector b_ (Maybe (SimpleFragment e_))) | b_->Float -> FragmentStream b_ c_ -> FragmentStream c_ d_
-testdata/Builtins.lc 282:26-282:40  {a} -> {b:Nat} -> a->Float -> Fragment b a -> Fragment b a
+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: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: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:1-284:15  {a} -> {b:Nat} -> (a->Bool) -> Fragment b a -> Fragment b a
 testdata/Builtins.lc 284:19-284:62  Type
 testdata/Builtins.lc 284:20-284:21  d_
 testdata/Builtins.lc 284:25-284:29  Type
@@ -2189,13 +2189,13 @@ testdata/Builtins.lc 286:57-286:73  Type->Type
 testdata/Builtins.lc 286:57-286:75  Type
 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  List (Vector a_ (Maybe (SimpleFragment d_))) -> List (Vector b_ (Maybe (SimpleFragment e_))) | b_->Bool -> FragmentStream b_ c_ -> FragmentStream c_ d_
-testdata/Builtins.lc 287:26-287:40  {a} -> {b:Nat} -> a->Bool -> Fragment b a -> Fragment b a
+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: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: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:1-289:12  {a} -> {b} -> {c:Nat} -> (a->b) -> Fragment c a -> Fragment c b
 testdata/Builtins.lc 289:16-289:56  Type
 testdata/Builtins.lc 289:17-289:18  f_
 testdata/Builtins.lc 289:22-289:23  Type | e_
@@ -2224,10 +2224,10 @@ testdata/Builtins.lc 291:51-291:67  Type->Type
 testdata/Builtins.lc 291:51-291:69  Type
 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  List (Vector a_ (Maybe (SimpleFragment e_))) -> List (Vector b_ (Maybe (SimpleFragment e_))) | c_->c_ -> FragmentStream b_ d_ -> FragmentStream c_ d_
-testdata/Builtins.lc 292:23-292:34  {a} -> {b} -> {c:Nat} -> a->b -> Fragment c a -> Fragment c b
+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: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 296:6-296:15  Type
@@ -2367,7 +2367,7 @@ 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: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: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:58  VecS e_ c_
 testdata/Builtins.lc 357:42-357:53  {a} -> {b:Nat} -> Vec b a -> Swizz->a
@@ -2453,7 +2453,7 @@ testdata/Builtins.lc 432:6-434:36  Type
 testdata/Builtins.lc 432:16-432:17  Type
 testdata/Builtins.lc 433:7-433:16  PointSize c_ | Type | {a} -> Float -> PointSize a
 testdata/Builtins.lc 433:17-433:22  Type
-testdata/Builtins.lc 434:7-434:23  PointSize d_ | Type | {a} -> a->Float -> PointSize a
+testdata/Builtins.lc 434:7-434:23  PointSize d_ | Type | {a} -> (a->Float) -> PointSize a
 testdata/Builtins.lc 434:25-434:26  Type
 testdata/Builtins.lc 434:30-434:35  Type
 testdata/Builtins.lc 436:6-436:17  Type | Type->Type
@@ -2657,7 +2657,7 @@ testdata/Builtins.lc 478:42-478:56  Type
 testdata/Builtins.lc 478:55-478:56  Type
 testdata/Builtins.lc 480:1-480:19  {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 481:8-486:34  Type
-testdata/Builtins.lc 481:10-481:13  {a} -> {b} -> a->b -> List a -> List b
+testdata/Builtins.lc 481:10-481:13  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 481:10-481:26  List Type -> List Type
 testdata/Builtins.lc 481:10-481:28  List Type
 testdata/Builtins.lc 481:10-481:30  List Type -> Type
@@ -2710,7 +2710,7 @@ testdata/Builtins.lc 486:32-486:33  List Type
 testdata/Builtins.lc 488:1-488:20  {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/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: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: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)
@@ -2750,7 +2750,7 @@ testdata/Builtins.lc 495:46-495:48  List e_
 testdata/Builtins.lc 497:1-497:16  List Type -> Type
 testdata/Builtins.lc 497:21-497:28  {a} -> List a -> Type
 testdata/Builtins.lc 497:21-497:45  Type
-testdata/Builtins.lc 497:30-497:33  {a} -> {b} -> a->b -> List a -> List b
+testdata/Builtins.lc 497:30-497:33  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 497:30-497:42  List Type -> List Nat
 testdata/Builtins.lc 497:30-497:44  List Nat
 testdata/Builtins.lc 497:34-497:42  Type->Nat
@@ -2765,13 +2765,13 @@ testdata/Builtins.lc 511:16-511:25  Type
 testdata/Builtins.lc 511:30-511:36  Type
 testdata/Builtins.lc 511:31-511:35  Type
 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: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: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: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:20-513:29  ImageKind->Type
@@ -2790,7 +2790,7 @@ testdata/Builtins.lc 517:50-517:51  e_
 testdata/Builtins.lc 517:50-517:53  d_->Type
 testdata/Builtins.lc 517:50-517:81  Type
 testdata/Builtins.lc 517:52-517:53  {a} -> a -> a->Type
-testdata/Builtins.lc 517:54-517:57  {a} -> {b} -> a->b -> List a -> List b
+testdata/Builtins.lc 517:54-517:57  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 517:54-517:79  List Type -> List ImageKind
 testdata/Builtins.lc 517:54-517:81  List ImageKind
 testdata/Builtins.lc 517:58-517:79  Type->ImageKind
@@ -2854,7 +2854,7 @@ testdata/Builtins.lc 530:87-530:103  Nat
 testdata/Builtins.lc 530:96-530:100  {a} -> List a -> a
 testdata/Builtins.lc 530:96-530:102  Type
 testdata/Builtins.lc 530:101-530:102  List Type
-testdata/Builtins.lc 530:106-530:109  {a} -> {b} -> a->b -> List a -> List b
+testdata/Builtins.lc 530:106-530:109  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Builtins.lc 530:106-530:122  List Type -> List ImageKind
 testdata/Builtins.lc 530:106-530:124  List ImageKind
 testdata/Builtins.lc 530:110-530:122  Type->ImageKind
@@ -2867,7 +2867,7 @@ testdata/Builtins.lc 534:34-534:48  FragmentStream b_ (HList ('imageType' ('map
 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: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: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:75  List (Vector c_ (Maybe (SimpleFragment (HList ('imageType' ('map Type ImageKind FragmentOperationKind b_))))))
 testdata/Builtins.lc 534:63-534:70  k_
diff --git a/testdata/Internals.out b/testdata/Internals.out
index dca27f59..2fd24406 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -3,52 +3,52 @@ main is not found
 typeAnn :: {a} -> a->a
 parens :: {a} -> a->a
 undefined :: {a}->a
-primFix :: {a} -> a->a -> a
+primFix :: {a} -> (a->a)->a
 'Unit :: Type
 TT :: 'Unit
-'UnitCase :: (a : 'Unit->Type) -> a TT -> b:'Unit -> a b
-match'Unit :: (a : Type->Type) -> a 'Unit -> b:Type -> a b -> a b
+'UnitCase :: (a : 'Unit->Type) -> a TT -> (b:'Unit) -> a b
+match'Unit :: (a : Type->Type) -> a 'Unit -> (b:Type) -> a b -> a b
 'String :: Type
-'StringCase :: (a : 'String->Type) -> b:'String -> a b
-match'String :: (a : Type->Type) -> a 'String -> b:Type -> a b -> a b
+'StringCase :: (a : 'String->Type) -> (b:'String) -> a b
+match'String :: (a : Type->Type) -> a 'String -> (b:Type) -> a b -> a b
 'Empty :: 'String->Type
 'EmptyCase :: {a:'String} -> (b : 'Empty a -> Type) -> (c : 'Empty a) -> b c
-match'Empty :: (a : Type->Type) -> (b:'String -> a ('Empty b)) -> c:Type -> a c -> a c
+match'Empty :: (a : Type->Type) -> ((b:'String) -> a ('Empty b)) -> (c:Type) -> a c -> a c
 unsafeCoerce :: {a} -> {b} -> a->b
-'EqCT :: a:Type -> a -> a->Type
-parEval :: a:Type -> a -> a->a
+'EqCT :: (a:Type) -> a -> a->Type
+parEval :: (a:Type) -> a -> a->a
 'T2 :: Type -> Type->Type
-match'Type :: (a : Type->Type) -> a Type -> b:Type -> a b -> a b
+match'Type :: (a : Type->Type) -> a Type -> (b:Type) -> a b -> a b
 'EqCTt :: {a} -> a -> a->Type
 t2C :: 'Unit -> 'Unit->'Unit
 'Int :: Type
-'IntCase :: (a : 'Int->Type) -> b:'Int -> a b
-match'Int :: (a : Type->Type) -> a 'Int -> b:Type -> a b -> a b
+'IntCase :: (a : 'Int->Type) -> (b:'Int) -> a b
+match'Int :: (a : Type->Type) -> a 'Int -> (b:Type) -> a b -> a b
 'Word :: Type
-'WordCase :: (a : 'Word->Type) -> b:'Word -> a b
-match'Word :: (a : Type->Type) -> a 'Word -> b:Type -> a b -> a b
+'WordCase :: (a : 'Word->Type) -> (b:'Word) -> a b
+match'Word :: (a : Type->Type) -> a 'Word -> (b:Type) -> a b -> a b
 'Float :: Type
-'FloatCase :: (a : 'Float->Type) -> b:'Float -> a b
-match'Float :: (a : Type->Type) -> a 'Float -> b:Type -> a b -> a b
+'FloatCase :: (a : 'Float->Type) -> (b:'Float) -> a b
+match'Float :: (a : Type->Type) -> a 'Float -> (b:Type) -> a b -> a b
 'Char :: Type
-'CharCase :: (a : 'Char->Type) -> b:'Char -> a b
-match'Char :: (a : Type->Type) -> a 'Char -> b:Type -> a b -> a b
+'CharCase :: (a : 'Char->Type) -> (b:'Char) -> a b
+match'Char :: (a : Type->Type) -> a 'Char -> (b:Type) -> a b -> a b
 'Bool :: Type
 False :: 'Bool
 True :: 'Bool
-'BoolCase :: (a : 'Bool->Type) -> a False -> a True -> b:'Bool -> a b
-match'Bool :: (a : Type->Type) -> a 'Bool -> b:Type -> a b -> a b
+'BoolCase :: (a : 'Bool->Type) -> a False -> a True -> (b:'Bool) -> a b
+match'Bool :: (a : Type->Type) -> a 'Bool -> (b:Type) -> a b -> a b
 'Ordering :: Type
 LT :: 'Ordering
 EQ :: 'Ordering
 GT :: 'Ordering
-'OrderingCase :: (a : 'Ordering->Type) -> a LT -> a EQ -> a GT -> b:'Ordering -> a b
-match'Ordering :: (a : Type->Type) -> a 'Ordering -> b:Type -> a b -> a b
+'OrderingCase :: (a : 'Ordering->Type) -> a LT -> a EQ -> a GT -> (b:'Ordering) -> a b
+match'Ordering :: (a : Type->Type) -> a 'Ordering -> (b:Type) -> a b -> a b
 'Nat :: Type
 Zero :: 'Nat
 Succ :: 'Nat->'Nat
-'NatCase :: (a : 'Nat->Type) -> a 0 -> (b:'Nat -> a (Succ b)) -> c:'Nat -> a c
-match'Nat :: (a : Type->Type) -> a 'Nat -> b:Type -> a b -> a b
+'NatCase :: (a : 'Nat->Type) -> a 0 -> ((b:'Nat) -> a (Succ b)) -> (c:'Nat) -> a c
+match'Nat :: (a : Type->Type) -> a 'Nat -> (b:Type) -> a b -> a b
 primIntToWord :: 'Int->'Word
 primIntToFloat :: 'Int->'Float
 primIntToNat :: 'Int->'Nat
@@ -76,15 +76,15 @@ negate :: {a} -> {_ : 'Num a} -> a->a
 'List :: Type->Type
 Nil :: {a} -> 'List a
 Cons :: {a} -> a -> 'List a -> 'List a
-'ListCase :: {a} -> (b : 'List a -> Type) -> b Nil -> (c:a -> (d : 'List a) -> b (Cons c d)) -> (e : 'List a) -> b e
-match'List :: (a : Type->Type) -> (b:Type -> a ('List b)) -> c:Type -> a c -> a c
+'ListCase :: {a} -> (b : 'List a -> Type) -> b Nil -> ((c:a) -> (d : 'List a) -> b (Cons c d)) -> (e : 'List a) -> b e
+match'List :: (a : Type->Type) -> ((b:Type) -> a ('List b)) -> (c:Type) -> a c -> a c
 'HList :: 'List Type -> Type
 HNil :: ()
 HCons :: {a} -> {b : 'List Type} -> a -> 'HList b -> 'HList (Cons a b)
-'HListCase :: (a : (b : 'List Type) -> 'HList b -> Type) -> a Nil () -> ({c} -> {d : 'List Type} -> e:c -> (f : 'HList d) -> a (Cons c d) (HCons c d e f)) -> {g : 'List Type} -> (h : 'HList g) -> a g h
-match'HList :: (a : Type->Type) -> ((b : 'List Type) -> a ('HList b)) -> c:Type -> a c -> a c
-hlistNilCase :: a:Type -> a -> ()->a
-hlistConsCase :: {a} -> {b : 'List Type} -> c:Type -> (a -> 'HList b -> c) -> 'HList (Cons a b) -> c
+'HListCase :: (a : (b : 'List Type) -> 'HList b -> Type) -> a Nil () -> ({c} -> {d : 'List Type} -> (e:c) -> (f : 'HList d) -> a (Cons c d) (HCons c d e f)) -> {g : 'List Type} -> (h : 'HList g) -> a g h
+match'HList :: (a : Type->Type) -> ((b : 'List Type) -> a ('HList b)) -> (c:Type) -> a c -> a c
+hlistNilCase :: (a:Type) -> a -> ()->a
+hlistConsCase :: {a} -> {b : 'List Type} -> (c:Type) -> (a -> 'HList b -> c) -> 'HList (Cons a b) -> c
 ------------ tooltips
 testdata/Internals.lc 6:1-6:8  {a} -> a->a
 testdata/Internals.lc 6:13-6:14  b_
@@ -93,7 +93,7 @@ testdata/Internals.lc 9:12-9:13  b_
 testdata/Internals.lc 11:1-11:10  {a}->a
 testdata/Internals.lc 11:27-11:31  Type
 testdata/Internals.lc 11:35-11:36  Type
-testdata/Internals.lc 13:1-13:8  {a} -> a->a -> a
+testdata/Internals.lc 13:1-13:8  {a} -> (a->a)->a
 testdata/Internals.lc 13:25-13:29  Type
 testdata/Internals.lc 13:33-13:46  Type
 testdata/Internals.lc 13:34-13:35  Type
@@ -109,19 +109,19 @@ testdata/Internals.lc 19:1-19:13  {a} -> {b} -> a->b
 testdata/Internals.lc 19:30-19:31  d_
 testdata/Internals.lc 19:30-19:36  Type
 testdata/Internals.lc 19:35-19:36  Type | c_
-testdata/Internals.lc 22:13-22:17  a:Type -> a -> a->Type
+testdata/Internals.lc 22:13-22:17  (a:Type) -> a -> a->Type
 testdata/Internals.lc 22:24-22:28  Type
 testdata/Internals.lc 22:36-22:37  Type
 testdata/Internals.lc 22:36-22:46  Type
 testdata/Internals.lc 22:45-22:46  Type
-testdata/Internals.lc 31:1-31:8  a:Type -> a -> a->a
+testdata/Internals.lc 31:1-31:8  (a:Type) -> a -> a->a
 testdata/Internals.lc 31:24-31:25  b_
 testdata/Internals.lc 31:24-31:35  Type
 testdata/Internals.lc 31:29-31:30  Type
 testdata/Internals.lc 31:29-31:35  Type
 testdata/Internals.lc 31:34-31:35  Type
 testdata/Internals.lc 34:13-34:15  Type -> Type->Type
-testdata/Internals.lc 36:1-36:11  (a : Type->Type) -> a Type -> b:Type -> a b -> a b
+testdata/Internals.lc 36:1-36:11  (a : Type->Type) -> a Type -> (b:Type) -> a b -> a b
 testdata/Internals.lc 36:28-36:32  Type
 testdata/Internals.lc 36:36-36:40  Type
 testdata/Internals.lc 36:45-36:46  Type->Type
@@ -138,7 +138,7 @@ testdata/Internals.lc 36:84-36:85  Type->Type
 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:18  (a:Type) -> a -> a->Type
 testdata/Internals.lc 38:14-38:20  a_ -> b_->Type
 testdata/Internals.lc 41:1-41:4  Unit -> Unit->Unit
 testdata/Internals.lc 41:8-41:12  Type
@@ -373,7 +373,7 @@ testdata/Internals.lc 128:39-128:41  List Type -> List Type
 testdata/Internals.lc 128:39-128:44  List Type
 testdata/Internals.lc 128:40-128:41  {a} -> a -> List a -> List a
 testdata/Internals.lc 128:42-128:44  List Type
-testdata/Internals.lc 130:1-130:13  a:Type -> a -> ()->a
+testdata/Internals.lc 130:1-130:13  (a:Type) -> a -> ()->a
 testdata/Internals.lc 130:29-130:30  b_
 testdata/Internals.lc 130:29-130:48  Type
 testdata/Internals.lc 130:34-130:39  List Type -> Type
@@ -381,7 +381,7 @@ testdata/Internals.lc 130:34-130:43  Type
 testdata/Internals.lc 130:34-130:48  Type
 testdata/Internals.lc 130:40-130:43  {a} -> List a
 testdata/Internals.lc 130:47-130:48  Type
-testdata/Internals.lc 131:1-131:14  {a} -> {b : List Type} -> c:Type -> (a -> HList b -> c) -> HList ('Cons a b) -> c
+testdata/Internals.lc 131:1-131:14  {a} -> {b : List Type} -> (c:Type) -> (a -> HList b -> c) -> HList ('Cons a b) -> c
 testdata/Internals.lc 132:21-132:25  Type
 testdata/Internals.lc 132:33-132:37  Type->Type
 testdata/Internals.lc 132:33-132:42  Type
diff --git a/testdata/Material.out b/testdata/Material.out
index 487f201b..874319e4 100644
--- a/testdata/Material.out
+++ b/testdata/Material.out
@@ -3,8 +3,8 @@ main is not found
 identityLight :: 'Float
 'Entity :: Type
 Entity :: 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 3 'Float -> 'Vec 4 'Float -> 'Entity
-'EntityCase :: (a : 'Entity->Type) -> ((b : 'Vec 4 'Float) -> (c : 'Vec 4 'Float) -> (d : 'Vec 3 'Float) -> (e : 'Vec 4 'Float) -> a (Entity b c d e)) -> f:'Entity -> a f
-match'Entity :: (a : Type->Type) -> a 'Entity -> b:Type -> a b -> a b
+'EntityCase :: (a : 'Entity->Type) -> ((b : 'Vec 4 'Float) -> (c : 'Vec 4 'Float) -> (d : 'Vec 3 'Float) -> (e : 'Vec 4 'Float) -> a (Entity b c d e)) -> (f:'Entity) -> a f
+match'Entity :: (a : Type->Type) -> a 'Entity -> (b:Type) -> a b -> a b
 eAmbientLight :: 'Entity -> 'VecS 'Float 4
 eDirectedLight :: 'Entity -> 'VecS 'Float 4
 eLightDir :: 'Entity -> 'VecS 'Float 3
@@ -16,12 +16,12 @@ WT_Square :: 'WaveType
 WT_Sawtooth :: 'WaveType
 WT_InverseSawtooth :: 'WaveType
 WT_Noise :: 'WaveType
-'WaveTypeCase :: (a : 'WaveType->Type) -> a WT_Sin -> a WT_Triangle -> a WT_Square -> a WT_Sawtooth -> a WT_InverseSawtooth -> a WT_Noise -> b:'WaveType -> a b
-match'WaveType :: (a : Type->Type) -> a 'WaveType -> b:Type -> a b -> a b
+'WaveTypeCase :: (a : 'WaveType->Type) -> a WT_Sin -> a WT_Triangle -> a WT_Square -> a WT_Sawtooth -> a WT_InverseSawtooth -> a WT_Noise -> (b:'WaveType) -> a b
+match'WaveType :: (a : Type->Type) -> a 'WaveType -> (b:Type) -> a b -> a b
 'Wave :: Type
 Wave :: 'WaveType -> 'Float -> 'Float -> 'Float -> 'Float->'Wave
-'WaveCase :: (a : 'Wave->Type) -> (b:'WaveType -> c:'Float -> d:'Float -> e:'Float -> f:'Float -> a (Wave b c d e f)) -> g:'Wave -> a g
-match'Wave :: (a : Type->Type) -> a 'Wave -> b:Type -> a b -> a b
+'WaveCase :: (a : 'Wave->Type) -> ((b:'WaveType) -> (c:'Float) -> (d:'Float) -> (e:'Float) -> (f:'Float) -> a (Wave b c d e f)) -> (g:'Wave) -> a g
+match'Wave :: (a : Type->Type) -> a 'Wave -> (b:Type) -> a b -> a b
 'Deform :: Type
 D_AutoSprite :: 'Deform
 D_AutoSprite2 :: 'Deform
@@ -38,14 +38,14 @@ D_Text5 :: 'Deform
 D_Text6 :: 'Deform
 D_Text7 :: 'Deform
 D_Wave :: 'Float -> 'Wave->'Deform
-'DeformCase :: (a : 'Deform->Type) -> a D_AutoSprite -> a D_AutoSprite2 -> (b:'Float -> c:'Float -> d:'Float -> a (D_Bulge b c d)) -> ((e : 'Vec 3 'Float) -> f:'Wave -> a (D_Move e f)) -> (g:'Float -> h:'Float -> a (D_Normal g h)) -> a D_ProjectionShadow -> a D_Text0 -> a D_Text1 -> a D_Text2 -> a D_Text3 -> a D_Text4 -> a D_Text5 -> a D_Text6 -> a D_Text7 -> (i:'Float -> j:'Wave -> a (D_Wave i j)) -> k:'Deform -> a k
-match'Deform :: (a : Type->Type) -> a 'Deform -> b:Type -> a b -> a b
+'DeformCase :: (a : 'Deform->Type) -> a D_AutoSprite -> a D_AutoSprite2 -> ((b:'Float) -> (c:'Float) -> (d:'Float) -> a (D_Bulge b c d)) -> ((e : 'Vec 3 'Float) -> (f:'Wave) -> a (D_Move e f)) -> ((g:'Float) -> (h:'Float) -> a (D_Normal g h)) -> a D_ProjectionShadow -> a D_Text0 -> a D_Text1 -> a D_Text2 -> a D_Text3 -> a D_Text4 -> a D_Text5 -> a D_Text6 -> a D_Text7 -> ((i:'Float) -> (j:'Wave) -> a (D_Wave i j)) -> (k:'Deform) -> a k
+match'Deform :: (a : Type->Type) -> a 'Deform -> (b:Type) -> a b -> a b
 'CullType :: Type
 CT_FrontSided :: 'CullType
 CT_BackSided :: 'CullType
 CT_TwoSided :: 'CullType
-'CullTypeCase :: (a : 'CullType->Type) -> a CT_FrontSided -> a CT_BackSided -> a CT_TwoSided -> b:'CullType -> a b
-match'CullType :: (a : Type->Type) -> a 'CullType -> b:Type -> a b -> a b
+'CullTypeCase :: (a : 'CullType->Type) -> a CT_FrontSided -> a CT_BackSided -> a CT_TwoSided -> (b:'CullType) -> a b
+match'CullType :: (a : Type->Type) -> a 'CullType -> (b:Type) -> a b -> a b
 'Blending' :: Type
 B_DstAlpha :: 'Blending'
 B_DstColor :: 'Blending'
@@ -58,8 +58,8 @@ B_SrcAlpha :: 'Blending'
 B_SrcAlphaSaturate :: 'Blending'
 B_SrcColor :: 'Blending'
 B_Zero :: 'Blending'
-'Blending'Case :: (a : 'Blending'->Type) -> a B_DstAlpha -> a B_DstColor -> a B_One -> a B_OneMinusDstAlpha -> a B_OneMinusDstColor -> a B_OneMinusSrcAlpha -> a B_OneMinusSrcColor -> a B_SrcAlpha -> a B_SrcAlphaSaturate -> a B_SrcColor -> a B_Zero -> b:'Blending' -> a b
-match'Blending' :: (a : Type->Type) -> a 'Blending' -> b:Type -> a b -> a b
+'Blending'Case :: (a : 'Blending'->Type) -> a B_DstAlpha -> a B_DstColor -> a B_One -> a B_OneMinusDstAlpha -> a B_OneMinusDstColor -> a B_OneMinusSrcAlpha -> a B_OneMinusSrcColor -> a B_SrcAlpha -> a B_SrcAlphaSaturate -> a B_SrcColor -> a B_Zero -> (b:'Blending') -> a b
+match'Blending' :: (a : Type->Type) -> a 'Blending' -> (b:Type) -> a b -> a b
 'RGBGen :: Type
 RGB_Wave :: 'Wave->'RGBGen
 RGB_Const :: 'Float -> 'Float -> 'Float->'RGBGen
@@ -72,8 +72,8 @@ RGB_Vertex :: 'RGBGen
 RGB_LightingDiffuse :: 'RGBGen
 RGB_OneMinusVertex :: 'RGBGen
 RGB_Undefined :: 'RGBGen
-'RGBGenCase :: (a : 'RGBGen->Type) -> (b:'Wave -> a (RGB_Wave b)) -> (c:'Float -> d:'Float -> e:'Float -> a (RGB_Const c d e)) -> a RGB_Identity -> a RGB_IdentityLighting -> a RGB_Entity -> a RGB_OneMinusEntity -> a RGB_ExactVertex -> a RGB_Vertex -> a RGB_LightingDiffuse -> a RGB_OneMinusVertex -> a RGB_Undefined -> f:'RGBGen -> a f
-match'RGBGen :: (a : Type->Type) -> a 'RGBGen -> b:Type -> a b -> a b
+'RGBGenCase :: (a : 'RGBGen->Type) -> ((b:'Wave) -> a (RGB_Wave b)) -> ((c:'Float) -> (d:'Float) -> (e:'Float) -> a (RGB_Const c d e)) -> a RGB_Identity -> a RGB_IdentityLighting -> a RGB_Entity -> a RGB_OneMinusEntity -> a RGB_ExactVertex -> a RGB_Vertex -> a RGB_LightingDiffuse -> a RGB_OneMinusVertex -> a RGB_Undefined -> (f:'RGBGen) -> a f
+match'RGBGen :: (a : Type->Type) -> a 'RGBGen -> (b:Type) -> a b -> a b
 'AlphaGen :: Type
 A_Wave :: 'Wave->'AlphaGen
 A_Const :: 'Float->'AlphaGen
@@ -84,16 +84,16 @@ A_OneMinusEntity :: 'AlphaGen
 A_Vertex :: 'AlphaGen
 A_LightingSpecular :: 'AlphaGen
 A_OneMinusVertex :: 'AlphaGen
-'AlphaGenCase :: (a : 'AlphaGen->Type) -> (b:'Wave -> a (A_Wave b)) -> (c:'Float -> a (A_Const c)) -> a A_Portal -> a A_Identity -> a A_Entity -> a A_OneMinusEntity -> a A_Vertex -> a A_LightingSpecular -> a A_OneMinusVertex -> d:'AlphaGen -> a d
-match'AlphaGen :: (a : Type->Type) -> a 'AlphaGen -> b:Type -> a b -> a b
+'AlphaGenCase :: (a : 'AlphaGen->Type) -> ((b:'Wave) -> a (A_Wave b)) -> ((c:'Float) -> a (A_Const c)) -> a A_Portal -> a A_Identity -> a A_Entity -> a A_OneMinusEntity -> a A_Vertex -> a A_LightingSpecular -> a A_OneMinusVertex -> (d:'AlphaGen) -> a d
+match'AlphaGen :: (a : Type->Type) -> a 'AlphaGen -> (b:Type) -> a b -> a b
 'TCGen :: Type
 TG_Base :: 'TCGen
 TG_Lightmap :: 'TCGen
 TG_Environment :: 'TCGen
 TG_Vector :: 'Vec 3 'Float -> 'Vec 3 'Float -> 'TCGen
 TG_Undefined :: 'TCGen
-'TCGenCase :: (a : 'TCGen->Type) -> a TG_Base -> a TG_Lightmap -> a TG_Environment -> ((b : 'Vec 3 'Float) -> (c : 'Vec 3 'Float) -> a (TG_Vector b c)) -> a TG_Undefined -> d:'TCGen -> a d
-match'TCGen :: (a : Type->Type) -> a 'TCGen -> b:Type -> a b -> a b
+'TCGenCase :: (a : 'TCGen->Type) -> a TG_Base -> a TG_Lightmap -> a TG_Environment -> ((b : 'Vec 3 'Float) -> (c : 'Vec 3 'Float) -> a (TG_Vector b c)) -> a TG_Undefined -> (d:'TCGen) -> a d
+match'TCGen :: (a : Type->Type) -> a 'TCGen -> (b:Type) -> a b -> a b
 'TCMod :: Type
 TM_EntityTranslate :: 'TCMod
 TM_Rotate :: 'Float->'TCMod
@@ -102,31 +102,31 @@ TM_Scale :: 'Float -> 'Float->'TCMod
 TM_Stretch :: 'Wave->'TCMod
 TM_Transform :: 'Float -> 'Float -> 'Float -> 'Float -> 'Float -> 'Float->'TCMod
 TM_Turb :: 'Float -> 'Float -> 'Float -> 'Float->'TCMod
-'TCModCase :: (a : 'TCMod->Type) -> a TM_EntityTranslate -> (b:'Float -> a (TM_Rotate b)) -> (c:'Float -> d:'Float -> a (TM_Scroll c d)) -> (e:'Float -> f:'Float -> a (TM_Scale e f)) -> (g:'Wave -> a (TM_Stretch g)) -> (h:'Float -> i:'Float -> j:'Float -> k:'Float -> l:'Float -> m:'Float -> a (TM_Transform h i j k l m)) -> (n:'Float -> o:'Float -> p:'Float -> q:'Float -> a (TM_Turb n o p q)) -> r:'TCMod -> a r
-match'TCMod :: (a : Type->Type) -> a 'TCMod -> b:Type -> a b -> a b
+'TCModCase :: (a : 'TCMod->Type) -> a TM_EntityTranslate -> ((b:'Float) -> a (TM_Rotate b)) -> ((c:'Float) -> (d:'Float) -> a (TM_Scroll c d)) -> ((e:'Float) -> (f:'Float) -> a (TM_Scale e f)) -> ((g:'Wave) -> a (TM_Stretch g)) -> ((h:'Float) -> (i:'Float) -> (j:'Float) -> (k:'Float) -> (l:'Float) -> (m:'Float) -> a (TM_Transform h i j k l m)) -> ((n:'Float) -> (o:'Float) -> (p:'Float) -> (q:'Float) -> a (TM_Turb n o p q)) -> (r:'TCMod) -> a r
+match'TCMod :: (a : Type->Type) -> a 'TCMod -> (b:Type) -> a b -> a b
 'StageTexture :: Type
 ST_Map :: 'String->'StageTexture
 ST_ClampMap :: 'String->'StageTexture
 ST_AnimMap :: 'Float -> 'List 'String -> 'StageTexture
 ST_Lightmap :: 'StageTexture
 ST_WhiteImage :: 'StageTexture
-'StageTextureCase :: (a : 'StageTexture->Type) -> (b:'String -> a (ST_Map b)) -> (c:'String -> a (ST_ClampMap c)) -> (d:'Float -> (e : 'List 'String) -> a (ST_AnimMap d e)) -> a ST_Lightmap -> a ST_WhiteImage -> f:'StageTexture -> a f
-match'StageTexture :: (a : Type->Type) -> a 'StageTexture -> b:Type -> a b -> a b
+'StageTextureCase :: (a : 'StageTexture->Type) -> ((b:'String) -> a (ST_Map b)) -> ((c:'String) -> a (ST_ClampMap c)) -> ((d:'Float) -> (e : 'List 'String) -> a (ST_AnimMap d e)) -> a ST_Lightmap -> a ST_WhiteImage -> (f:'StageTexture) -> a f
+match'StageTexture :: (a : Type->Type) -> a 'StageTexture -> (b:Type) -> a b -> a b
 'AlphaFunction :: Type
 A_Gt0 :: 'AlphaFunction
 A_Lt128 :: 'AlphaFunction
 A_Ge128 :: 'AlphaFunction
-'AlphaFunctionCase :: (a : 'AlphaFunction->Type) -> a A_Gt0 -> a A_Lt128 -> a A_Ge128 -> b:'AlphaFunction -> a b
-match'AlphaFunction :: (a : Type->Type) -> a 'AlphaFunction -> b:Type -> a b -> a b
+'AlphaFunctionCase :: (a : 'AlphaFunction->Type) -> a A_Gt0 -> a A_Lt128 -> a A_Ge128 -> (b:'AlphaFunction) -> a b
+match'AlphaFunction :: (a : Type->Type) -> a 'AlphaFunction -> (b:Type) -> a b -> a b
 'DepthFunction :: Type
 D_Equal :: 'DepthFunction
 D_Lequal :: 'DepthFunction
-'DepthFunctionCase :: (a : 'DepthFunction->Type) -> a D_Equal -> a D_Lequal -> b:'DepthFunction -> a b
-match'DepthFunction :: (a : Type->Type) -> a 'DepthFunction -> b:Type -> a b -> a b
+'DepthFunctionCase :: (a : 'DepthFunction->Type) -> a D_Equal -> a D_Lequal -> (b:'DepthFunction) -> a b
+match'DepthFunction :: (a : Type->Type) -> a 'DepthFunction -> (b:Type) -> a b -> a b
 'StageAttrs :: Type
 StageAttrs :: 'Maybe ('Blending', 'Blending') -> 'RGBGen -> 'AlphaGen -> 'TCGen -> 'List 'TCMod -> 'StageTexture -> 'Bool -> 'DepthFunction -> 'Maybe 'AlphaFunction -> 'Bool -> 'String->'StageAttrs
-'StageAttrsCase :: (a : 'StageAttrs->Type) -> ((b : 'Maybe ('Blending', 'Blending')) -> c:'RGBGen -> d:'AlphaGen -> e:'TCGen -> (f : 'List 'TCMod) -> g:'StageTexture -> h:'Bool -> i:'DepthFunction -> (j : 'Maybe 'AlphaFunction) -> k:'Bool -> l:'String -> a (StageAttrs b c d e f g h i j k l)) -> m:'StageAttrs -> a m
-match'StageAttrs :: (a : Type->Type) -> a 'StageAttrs -> b:Type -> a b -> a b
+'StageAttrsCase :: (a : 'StageAttrs->Type) -> ((b : 'Maybe ('Blending', 'Blending')) -> (c:'RGBGen) -> (d:'AlphaGen) -> (e:'TCGen) -> (f : 'List 'TCMod) -> (g:'StageTexture) -> (h:'Bool) -> (i:'DepthFunction) -> (j : 'Maybe 'AlphaFunction) -> (k:'Bool) -> (l:'String) -> a (StageAttrs b c d e f g h i j k l)) -> (m:'StageAttrs) -> a m
+match'StageAttrs :: (a : Type->Type) -> a 'StageAttrs -> (b:Type) -> a b -> a b
 saBlend :: 'StageAttrs -> 'Maybe ('Blending', 'Blending')
 saRGBGen :: 'StageAttrs->'RGBGen
 saAlphaGen :: 'StageAttrs->'AlphaGen
@@ -141,8 +141,8 @@ saTextureUniform :: 'StageAttrs->'String
 defaultStageAttrs :: 'StageAttrs
 'CommonAttrs :: Type
 CommonAttrs :: () -> () -> 'Bool -> 'Float -> 'Bool -> 'Bool -> 'CullType -> 'List 'Deform -> 'Bool -> 'Bool -> 'List 'StageAttrs -> 'Bool->'CommonAttrs
-'CommonAttrsCase :: (a : 'CommonAttrs->Type) -> (b:() -> c:() -> d:'Bool -> e:'Float -> f:'Bool -> g:'Bool -> h:'CullType -> (i : 'List 'Deform) -> j:'Bool -> k:'Bool -> (l : 'List 'StageAttrs) -> m:'Bool -> a (CommonAttrs b c d e f g h i j k l m)) -> n:'CommonAttrs -> a n
-match'CommonAttrs :: (a : Type->Type) -> a 'CommonAttrs -> b:Type -> a b -> a b
+'CommonAttrsCase :: (a : 'CommonAttrs->Type) -> ((b:()) -> (c:()) -> (d:'Bool) -> (e:'Float) -> (f:'Bool) -> (g:'Bool) -> (h:'CullType) -> (i : 'List 'Deform) -> (j:'Bool) -> (k:'Bool) -> (l : 'List 'StageAttrs) -> (m:'Bool) -> a (CommonAttrs b c d e f g h i j k l m)) -> (n:'CommonAttrs) -> a n
+match'CommonAttrs :: (a : Type->Type) -> a 'CommonAttrs -> (b:Type) -> a b -> a b
 caSkyParms :: 'CommonAttrs->()
 caFogParms :: 'CommonAttrs->()
 caPortal :: 'CommonAttrs->'Bool
diff --git a/testdata/Prelude.out b/testdata/Prelude.out
index ee451b4f..631f7aea 100644
--- a/testdata/Prelude.out
+++ b/testdata/Prelude.out
@@ -2,15 +2,15 @@ main is not found
 ------------ trace
 const :: {a} -> {b} -> a -> b->a
 otherwise :: 'Bool
-& :: {a} -> {b} -> a -> a->b -> b
-$ :: {a} -> {b} -> a->b -> a->b
-. :: {a} -> {b} -> {c} -> b->c -> a->b -> a->c
+& :: {a} -> {b} -> a -> (a->b)->b
+$ :: {a} -> {b} -> (a->b) -> a->b
+. :: {a} -> {b} -> {c} -> (b->c) -> (a->b) -> a->c
 uncurry :: {a} -> {b} -> {c} -> (a -> c->b) -> (a, c)->b
-*** :: {a} -> {b} -> {c} -> {d} -> a->c -> b->d -> (a, b)->(c, d)
+*** :: {a} -> {b} -> {c} -> {d} -> (a->c) -> (b->d) -> (a, b)->(c, d)
 pi :: 'Float
 zip :: {a} -> {b} -> 'List a -> 'List b -> 'List (a, b)
 unzip :: {a} -> {b} -> 'List (a, b) -> ('List a, 'List b)
-filter :: {a} -> a->'Bool -> 'List a -> 'List a
+filter :: {a} -> (a->'Bool) -> 'List a -> 'List a
 tail :: {a} -> 'List a -> 'List a
 pairs :: {a} -> 'List a -> 'List (a, a)
 foldl' :: {a} -> {b} -> (a -> b->a) -> a -> 'List b -> a
@@ -18,24 +18,24 @@ foldr1 :: {a} -> (a -> a->a) -> 'List a -> a
 split :: {a} -> 'List a -> ('List a, 'List a)
 mergeBy :: {a} -> (a -> a->'Ordering) -> 'List a -> 'List a -> 'List a
 sortBy :: {a} -> (a -> a->'Ordering) -> 'List a -> 'List a
-iterate :: {a} -> a->a -> a -> 'List a
+iterate :: {a} -> (a->a) -> a -> 'List a
 fst :: {a} -> {b} -> (a, b)->a
 snd :: {a} -> {b} -> (a, b)->b
 ||| :: 'Bool -> 'Bool->'Bool
 &&& :: 'Bool -> 'Bool->'Bool
 'RecItem :: Type
 RecItem :: 'String -> Type->'RecItem
-'RecItemCase :: (a : 'RecItem->Type) -> (b:'String -> c:Type -> a (RecItem b c)) -> d:'RecItem -> a d
-match'RecItem :: (a : Type->Type) -> a 'RecItem -> b:Type -> a b -> a b
+'RecItemCase :: (a : 'RecItem->Type) -> ((b:'String) -> (c:Type) -> a (RecItem b c)) -> (d:'RecItem) -> a d
+match'RecItem :: (a : Type->Type) -> a 'RecItem -> (b:Type) -> a b -> a b
 recItemType :: 'RecItem->Type
 'RecordC :: 'List 'RecItem -> Type
 RecordCons :: {a : 'List 'RecItem} -> 'HList (map 'RecItem Type recItemType a) -> 'RecordC a
 'RecordCCase :: {a : 'List 'RecItem} -> (b : 'RecordC a -> Type) -> ((c : 'HList (map 'RecItem Type recItemType a)) -> b (RecordCons c)) -> (d : 'RecordC a) -> b d
-match'RecordC :: (a : Type->Type) -> ((b : 'List 'RecItem) -> a ('RecordC b)) -> c:Type -> a c -> a c
+match'RecordC :: (a : Type->Type) -> ((b : 'List 'RecItem) -> a ('RecordC b)) -> (c:Type) -> a c -> a c
 isKeyC :: 'String -> Type -> 'List 'RecItem -> Type
 fstTup :: {a} -> {b : 'List Type} -> 'HList (Cons a b) -> a
 sndTup :: {a} -> {b : 'List Type} -> 'HList (Cons a b) -> 'HList b
-project :: {a} -> {b : 'List 'RecItem} -> c:'String -> {_ : isKeyC c a b} -> 'RecordC b -> a
+project :: {a} -> {b : 'List 'RecItem} -> (c:'String) -> {_ : isKeyC c a b} -> 'RecordC b -> a
 rgb :: 'Float -> 'Float -> 'Float -> 'VecS 'Float 4
 black :: 'VecS 'Float 4
 gray :: 'VecS 'Float 4
@@ -176,13 +176,13 @@ testdata/Prelude.lc 16:1-16:6  {a} -> {b} -> a -> b->a
 testdata/Prelude.lc 16:13-16:14  d_
 testdata/Prelude.lc 18:1-18:10  Bool
 testdata/Prelude.lc 18:13-18:17  Bool
-testdata/Prelude.lc 20:3-20:4  {a} -> {b} -> a -> a->b -> b
+testdata/Prelude.lc 20:3-20:4  {a} -> {b} -> a -> (a->b)->b
 testdata/Prelude.lc 20:9-20:10  b_
 testdata/Prelude.lc 20:11-20:12  g_
-testdata/Prelude.lc 22:2-22:3  {a} -> {b} -> a->b -> a->b
+testdata/Prelude.lc 22:2-22:3  {a} -> {b} -> (a->b) -> a->b
 testdata/Prelude.lc 22:15-22:16  d_
 testdata/Prelude.lc 22:17-22:18  e_
-testdata/Prelude.lc 23:2-23:3  {a} -> {b} -> {c} -> b->c -> a->b -> a->c
+testdata/Prelude.lc 23:2-23:3  {a} -> {b} -> {c} -> (b->c) -> (a->b) -> a->c
 testdata/Prelude.lc 23:17-23:18  f_
 testdata/Prelude.lc 23:20-23:21  g_
 testdata/Prelude.lc 23:22-23:23  h_
@@ -191,7 +191,7 @@ 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: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: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:21-27:22  s_
 testdata/Prelude.lc 27:23-27:24  p_
@@ -264,7 +264,7 @@ testdata/Prelude.lc 39:13-39:15  HList c_ -> c_ | c_ | c_ -> HList c_ -> c_ | 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: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_
@@ -392,10 +392,10 @@ testdata/Prelude.lc 71:24-71:33  List a_ -> List b_ -> List c_
 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: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:46-71:49  {a} -> {b} -> {c} -> {d} -> a->c -> b->d -> (a, b)->(c, d)
+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
@@ -403,19 +403,19 @@ 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_->b_ | {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
 testdata/Prelude.lc 73:24-73:32  Type
 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: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  List c_ | a_->b_ -> b_ -> List c_ | b_ -> List c_
+testdata/Prelude.lc 74:16-74:35  (a_->b_) -> b_ -> List c_ | List c_ | b_ -> List c_
 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:27  {a} -> (a->a) -> a -> List a
 testdata/Prelude.lc 74:20-74:29  c_ -> List d_
 testdata/Prelude.lc 74:20-74:35  List c_
 testdata/Prelude.lc 74:28-74:29  d_->e_
@@ -452,7 +452,7 @@ testdata/Prelude.lc 126:22-126:29  Type
 testdata/Prelude.lc 127:7-127:17  RecordC c_ | Type | {a : List RecItem} -> HList ('map RecItem Type 'recItemType a) -> RecordC a
 testdata/Prelude.lc 127:19-127:24  List Type -> Type
 testdata/Prelude.lc 127:19-127:45  Type
-testdata/Prelude.lc 127:26-127:29  {a} -> {b} -> a->b -> List a -> List b
+testdata/Prelude.lc 127:26-127:29  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Prelude.lc 127:26-127:41  List RecItem -> List Type
 testdata/Prelude.lc 127:26-127:44  List Type
 testdata/Prelude.lc 127:30-127:41  RecItem->Type
@@ -479,18 +479,18 @@ testdata/Prelude.lc 130:69-130:70  String
 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: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 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: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 136:12-138:181  a_->b_ | {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
@@ -509,11 +509,11 @@ testdata/Prelude.lc 136:82-136:92  Type
 testdata/Prelude.lc 136:82-136:97  Type
 testdata/Prelude.lc 136:90-136:92  List RecItem
 testdata/Prelude.lc 136:96-136:97  Type
-testdata/Prelude.lc 137:1-137:8  {a} -> {b : List RecItem} -> c:String -> {_ : 'isKeyC c a b} -> RecordC b -> a
+testdata/Prelude.lc 137:1-137:8  {a} -> {b : List RecItem} -> (c:String) -> {_ : 'isKeyC c a b} -> RecordC b -> a
 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  HList ('map RecItem Type 'recItemType b_) -> b_ | List c_ -> c_ | RecordC c_ -> e_ | String -> Type->c_ | Type->c_ | a:String -> {_ : 'isKeyC a c_ b_} -> RecordC c_ -> e_ | 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 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: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
@@ -529,15 +529,15 @@ testdata/Prelude.lc 137:101-137:102  Type
 testdata/Prelude.lc 137:101-137:104  List Type -> List Type
 testdata/Prelude.lc 137:101-137:123  List Type
 testdata/Prelude.lc 137:103-137:104  {a} -> a -> List a -> List a
-testdata/Prelude.lc 137:105-137:108  {a} -> {b} -> a->b -> List a -> List b
+testdata/Prelude.lc 137:105-137:108  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Prelude.lc 137:105-137:120  List RecItem -> List Type
 testdata/Prelude.lc 137:105-137:123  List Type
 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: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:181  n_
@@ -567,7 +567,7 @@ testdata/Prelude.lc 138:151-138:152  Type
 testdata/Prelude.lc 138:151-138:154  List Type -> List Type
 testdata/Prelude.lc 138:151-138:173  List Type
 testdata/Prelude.lc 138:153-138:154  {a} -> a -> List a -> List a
-testdata/Prelude.lc 138:155-138:158  {a} -> {b} -> a->b -> List a -> List b
+testdata/Prelude.lc 138:155-138:158  {a} -> {b} -> (a->b) -> List a -> List b
 testdata/Prelude.lc 138:155-138:170  List RecItem -> List Type
 testdata/Prelude.lc 138:155-138:173  List Type
 testdata/Prelude.lc 138:159-138:170  RecItem->Type
@@ -1481,7 +1481,7 @@ 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:33  VecScalar 3 Float
-testdata/Prelude.lc 375:19-375:20  {a} -> {b} -> a->b -> a->b
+testdata/Prelude.lc 375:19-375:20  {a} -> {b} -> (a->b) -> a->b
 testdata/Prelude.lc 375:21-375:24  Vec 3 Float
 testdata/Prelude.lc 375:21-375:26  VecS Float 3 -> VecS Float 3
 testdata/Prelude.lc 375:21-375:33  VecS Float 3
@@ -1490,7 +1490,7 @@ 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:33  VecScalar 3 Float
-testdata/Prelude.lc 376:19-376:20  {a} -> {b} -> a->b -> a->b
+testdata/Prelude.lc 376:19-376:20  {a} -> {b} -> (a->b) -> a->b
 testdata/Prelude.lc 376:21-376:23  Vec 3 Float
 testdata/Prelude.lc 376:21-376:31  VecS Float 3 -> VecS Float 3
 testdata/Prelude.lc 376:21-376:33  VecS Float 3
@@ -1504,7 +1504,7 @@ 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:65  Mat 4 4 Float
-testdata/Prelude.lc 378:19-378:20  {a} -> {b} -> a->b -> a->b
+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
 testdata/Prelude.lc 378:21-378:34  Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
 testdata/Prelude.lc 378:21-378:43  Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
diff --git a/testdata/adhoc.reject.out b/testdata/adhoc.reject.out
index 640292db..730a6f84 100644
--- a/testdata/adhoc.reject.out
+++ b/testdata/adhoc.reject.out
@@ -6,8 +6,8 @@ x = one :: Vec 4 A
 ------------ trace
 'A :: Type
 A :: 'A
-'ACase :: (a : 'A->Type) -> a A -> b:'A -> a b
-match'A :: (a : Type->Type) -> a 'A -> b:Type -> a b -> a b
+'ACase :: (a : 'A->Type) -> a A -> (b:'A) -> a b
+match'A :: (a : Type->Type) -> a 'A -> (b:Type) -> a b -> a b
 !type error: no instance of 'Component on ???
 in testdata/adhoc.reject.lc:4:5:
 x = one :: Vec 4 A
diff --git a/testdata/complex.out b/testdata/complex.out
index f751c2bb..7c33a18a 100644
--- a/testdata/complex.out
+++ b/testdata/complex.out
@@ -3,12 +3,12 @@ main is not found
 'Repr :: Type
 Normal :: 'Repr
 Polar :: 'Repr
-'ReprCase :: (a : 'Repr->Type) -> a Normal -> a Polar -> b:'Repr -> a b
-match'Repr :: (a : Type->Type) -> a 'Repr -> b:Type -> a b -> a b
+'ReprCase :: (a : 'Repr->Type) -> a Normal -> a Polar -> (b:'Repr) -> a b
+match'Repr :: (a : Type->Type) -> a 'Repr -> (b:Type) -> a b -> a b
 'Complex :: 'Repr->Type
 Complex :: {a:'Repr} -> 'Float -> 'Float -> 'Complex a
-'ComplexCase :: (a : b:'Repr -> 'Complex b -> Type) -> ({c:'Repr} -> d:'Float -> e:'Float -> a c (Complex c d e)) -> {f:'Repr} -> (g : 'Complex f) -> a f g
-match'Complex :: (a : Type->Type) -> (b:'Repr -> a ('Complex b)) -> c:Type -> a c -> a c
+'ComplexCase :: (a : (b:'Repr) -> 'Complex b -> Type) -> ({c:'Repr} -> (d:'Float) -> (e:'Float) -> a c (Complex c d e)) -> {f:'Repr} -> (g : 'Complex f) -> a f g
+match'Complex :: (a : Type->Type) -> ((b:'Repr) -> a ('Complex b)) -> (c:Type) -> a c -> a c
 repr :: {a:'Repr} -> 'Complex a -> 'Repr
 normal :: 'Float -> 'Float -> 'Complex Normal
 polar :: 'Float -> 'Float -> 'Complex Polar
diff --git a/testdata/data.out b/testdata/data.out
index 4613e04f..1dddf3f4 100644
--- a/testdata/data.out
+++ b/testdata/data.out
@@ -2,27 +2,27 @@ main is not found
 ------------ trace
 'Data0 :: Type
 Data0 :: 'Data0
-'Data0Case :: (a : 'Data0->Type) -> a Data0 -> b:'Data0 -> a b
-match'Data0 :: (a : Type->Type) -> a 'Data0 -> b:Type -> a b -> a b
+'Data0Case :: (a : 'Data0->Type) -> a Data0 -> (b:'Data0) -> a b
+match'Data0 :: (a : Type->Type) -> a 'Data0 -> (b:Type) -> a b -> a b
 'Data1 :: Type -> Type -> Type->Type
 Data1 :: {a} -> {b} -> {c} -> a -> b -> c -> 'Data1 a b c
-'Data1Case :: {a} -> {b} -> {c} -> (d : 'Data1 a b c -> Type) -> (e:a -> f:b -> g:c -> d (Data1 e f g)) -> (h : 'Data1 a b c) -> d h
-match'Data1 :: (a : Type->Type) -> (b:Type -> c:Type -> d:Type -> a ('Data1 b c d)) -> e:Type -> a e -> a e
+'Data1Case :: {a} -> {b} -> {c} -> (d : 'Data1 a b c -> Type) -> ((e:a) -> (f:b) -> (g:c) -> d (Data1 e f g)) -> (h : 'Data1 a b c) -> d h
+match'Data1 :: (a : Type->Type) -> ((b:Type) -> (c:Type) -> (d:Type) -> a ('Data1 b c d)) -> (e:Type) -> a e -> a e
 'Data2 :: Type
 Data21 :: 'Int->'Data2
 Data22 :: 'Int -> 'Int->'Data2
 Data23 :: 'Int->'Data2
 Data24 :: 'Data2
-'Data2Case :: (a : 'Data2->Type) -> (b:'Int -> a (Data21 b)) -> (c:'Int -> d:'Int -> a (Data22 c d)) -> (e:'Int -> a (Data23 e)) -> a Data24 -> f:'Data2 -> a f
-match'Data2 :: (a : Type->Type) -> a 'Data2 -> b:Type -> a b -> a b
+'Data2Case :: (a : 'Data2->Type) -> ((b:'Int) -> a (Data21 b)) -> ((c:'Int) -> (d:'Int) -> a (Data22 c d)) -> ((e:'Int) -> a (Data23 e)) -> a Data24 -> (f:'Data2) -> a f
+match'Data2 :: (a : Type->Type) -> a 'Data2 -> (b:Type) -> a b -> a b
 x :: 'Data2->'Int
 y :: 'Data2->'Int
 'Data5 :: Type -> Type -> Type->Type
 Data51 :: {a} -> {b} -> {c} -> a -> 'Data5 a b c
 Data52 :: {a} -> {b} -> {c} -> a -> b -> c -> 'Data5 a b c
 Data53 :: {a} -> {b} -> {c} -> 'Int -> a -> 'Float -> b -> c -> 'Data5 a b c
-'Data5Case :: {a} -> {b} -> {c} -> (d : 'Data5 a b c -> Type) -> (e:a -> d (Data51 e)) -> (f:a -> g:b -> h:c -> d (Data52 f g h)) -> (i:'Int -> j:a -> k:'Float -> l:b -> m:c -> d (Data53 i j k l m)) -> (n : 'Data5 a b c) -> d n
-match'Data5 :: (a : Type->Type) -> (b:Type -> c:Type -> d:Type -> a ('Data5 b c d)) -> e:Type -> a e -> a e
+'Data5Case :: {a} -> {b} -> {c} -> (d : 'Data5 a b c -> Type) -> ((e:a) -> d (Data51 e)) -> ((f:a) -> (g:b) -> (h:c) -> d (Data52 f g h)) -> ((i:'Int) -> (j:a) -> (k:'Float) -> (l:b) -> (m:c) -> d (Data53 i j k l m)) -> (n : 'Data5 a b c) -> d n
+match'Data5 :: (a : Type->Type) -> ((b:Type) -> (c:Type) -> (d:Type) -> a ('Data5 b c d)) -> (e:Type) -> a e -> a e
 a5 :: {a} -> {b} -> {c} -> 'Data5 a b c -> a
 b5 :: {a} -> {b} -> {c} -> 'Data5 a b c -> b
 c5 :: {a} -> {b} -> {c} -> 'Data5 a b c -> c
diff --git a/testdata/empty.out b/testdata/empty.out
index c1178ed4..bcb2f224 100644
--- a/testdata/empty.out
+++ b/testdata/empty.out
@@ -1,7 +1,7 @@
 main is not found
 ------------ trace
 'Empty :: Type
-'EmptyCase :: (a : 'Empty->Type) -> b:'Empty -> a b
-match'Empty :: (a : Type->Type) -> a 'Empty -> b:Type -> a b -> a b
+'EmptyCase :: (a : 'Empty->Type) -> (b:'Empty) -> a b
+match'Empty :: (a : Type->Type) -> a 'Empty -> (b:Type) -> a b -> a b
 ------------ tooltips
 testdata/empty.lc 3:6-3:11  Type
diff --git a/testdata/language-features/adt/adt02.reject.out b/testdata/language-features/adt/adt02.reject.out
index 59901cda..48ca3cb9 100644
--- a/testdata/language-features/adt/adt02.reject.out
+++ b/testdata/language-features/adt/adt02.reject.out
@@ -9,8 +9,8 @@ in proj
 'Data3 :: Type
 Data3 :: 'Bool -> 'Char -> 'Bool->'Data3
 Data31 :: 'Int -> 'String -> 'Int->'Data3
-'Data3Case :: (a : 'Data3->Type) -> (b:'Bool -> c:'Char -> d:'Bool -> a (Data3 b c d)) -> (e:'Int -> f:'String -> g:'Int -> a (Data31 e f g)) -> h:'Data3 -> a h
-match'Data3 :: (a : Type->Type) -> a 'Data3 -> b:Type -> a b -> a b
+'Data3Case :: (a : 'Data3->Type) -> ((b:'Bool) -> (c:'Char) -> (d:'Bool) -> a (Data3 b c d)) -> ((e:'Int) -> (f:'String) -> (g:'Int) -> a (Data31 e f g)) -> (h:'Data3) -> a h
+match'Data3 :: (a : Type->Type) -> a 'Data3 -> (b:Type) -> a b -> a b
 !type error: can not unify
 'Bool
 with
diff --git a/testdata/language-features/adt/gadt03.reject.out b/testdata/language-features/adt/gadt03.reject.out
index 86e6efc4..cb6cd714 100644
--- a/testdata/language-features/adt/gadt03.reject.out
+++ b/testdata/language-features/adt/gadt03.reject.out
@@ -2,8 +2,8 @@ illegal data definition (parameters are not uniform)
 ------------ trace
 'M2 :: Type -> 'String->Type
 Value2 :: {a} -> a -> {b:'String} -> 'M2 a b
-'M2Case :: {a} -> (b : c:'String -> 'M2 a c -> Type) -> (d:a -> {e:'String} -> b e (Value2 d e)) -> {f:'String} -> (g : 'M2 a f) -> b f g
-match'M2 :: (a : Type->Type) -> (b:Type -> c:'String -> a ('M2 b c)) -> d:Type -> a d -> a d
+'M2Case :: {a} -> (b : (c:'String) -> 'M2 a c -> Type) -> ((d:a) -> {e:'String} -> b e (Value2 d e)) -> {f:'String} -> (g : 'M2 a f) -> b f g
+match'M2 :: (a : Type->Type) -> ((b:Type) -> (c:'String) -> a ('M2 b c)) -> (d:Type) -> a d -> a d
 'M3 :: Type -> 'String->Type
 !illegal data definition (parameters are not uniform)
 ------------ tooltips
diff --git a/testdata/language-features/adt/gadt04.reject.out b/testdata/language-features/adt/gadt04.reject.out
index 02b21961..1871c4aa 100644
--- a/testdata/language-features/adt/gadt04.reject.out
+++ b/testdata/language-features/adt/gadt04.reject.out
@@ -7,8 +7,8 @@ already defined Value at testdata/language-features/adt/gadt04.reject.lc:6:3:
 ------------ trace
 'M :: Type -> 'String->Type
 Value :: {a} -> a -> {b:'String} -> 'M a b
-'MCase :: (a : b:Type -> c:'String -> 'M b c -> Type) -> ({d} -> e:d -> {f:'String} -> a d f (Value d e f)) -> {g} -> {h:'String} -> (i : 'M g h) -> a g h i
-match'M :: (a : Type->Type) -> (b:Type -> c:'String -> a ('M b c)) -> d:Type -> a d -> a d
+'MCase :: (a : (b:Type) -> (c:'String) -> 'M b c -> Type) -> ({d} -> (e:d) -> {f:'String} -> a d f (Value d e f)) -> {g} -> {h:'String} -> (i : 'M g h) -> a g h i
+match'M :: (a : Type->Type) -> ((b:Type) -> (c:'String) -> a ('M b c)) -> (d:Type) -> a d -> a d
 'M2 :: Type -> 'String->Type
 Value :: {a} -> a -> {b:'String} -> 'M2 a b
 !already defined Value at testdata/language-features/adt/gadt04.reject.lc:6:3:
diff --git a/testdata/language-features/basic-list/listcomp09.out b/testdata/language-features/basic-list/listcomp09.out
index fa57c421..694e13a4 100644
--- a/testdata/language-features/basic-list/listcomp09.out
+++ b/testdata/language-features/basic-list/listcomp09.out
@@ -1,9 +1,9 @@
 main is not found
 ------------ trace
-value1 :: {_} -> 'List ()->'String
+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: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: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/data01.out b/testdata/language-features/basic-values/data01.out
index 65afa571..55a3f99f 100644
--- a/testdata/language-features/basic-values/data01.out
+++ b/testdata/language-features/basic-values/data01.out
@@ -4,20 +4,20 @@ main is not found
 B :: 'A
 C :: 'A
 D :: 'A
-'ACase :: (a : 'A->Type) -> a B -> a C -> a D -> b:'A -> a b
-match'A :: (a : Type->Type) -> a 'A -> b:Type -> a b -> a b
+'ACase :: (a : 'A->Type) -> a B -> a C -> a D -> (b:'A) -> a b
+match'A :: (a : Type->Type) -> a 'A -> (b:Type) -> a b -> a b
 'E :: Type
 F :: 'E
 G :: ()->'E
 H :: 'E
-'ECase :: (a : 'E->Type) -> a F -> (b:() -> a (G b)) -> a H -> c:'E -> a c
-match'E :: (a : Type->Type) -> a 'E -> b:Type -> a b -> a b
+'ECase :: (a : 'E->Type) -> a F -> ((b:()) -> a (G b)) -> a H -> (c:'E) -> a c
+match'E :: (a : Type->Type) -> a 'E -> (b:Type) -> a b -> a b
 'D1 :: Type
 C1 :: 'D1
 C2 :: ()->'D1
 C3 :: 'D1
-'D1Case :: (a : 'D1->Type) -> a C1 -> (b:() -> a (C2 b)) -> a C3 -> c:'D1 -> a c
-match'D1 :: (a : Type->Type) -> a 'D1 -> b:Type -> a b -> a b
+'D1Case :: (a : 'D1->Type) -> a C1 -> ((b:()) -> a (C2 b)) -> a C3 -> (c:'D1) -> a c
+match'D1 :: (a : Type->Type) -> a 'D1 -> (b:Type) -> a b -> a b
 ------------ tooltips
 testdata/language-features/basic-values/data01.lc 1:6-1:7  Type
 testdata/language-features/basic-values/data01.lc 1:6-1:13  Type
diff --git a/testdata/language-features/basic-values/infix03.out b/testdata/language-features/basic-values/infix03.out
index da5c00d2..31c99f85 100644
--- a/testdata/language-features/basic-values/infix03.out
+++ b/testdata/language-features/basic-values/infix03.out
@@ -3,8 +3,8 @@ main is not found
 'D :: Type
 D2 :: () -> ()->'D
 D3 :: () -> () -> ()->'D
-'DCase :: (a : 'D->Type) -> (b:() -> c:() -> a (D2 b c)) -> (d:() -> e:() -> f:() -> a (D3 d e f)) -> g:'D -> a g
-match'D :: (a : Type->Type) -> a 'D -> b:Type -> a b -> a b
+'DCase :: (a : 'D->Type) -> ((b:()) -> (c:()) -> a (D2 b c)) -> ((d:()) -> (e:()) -> (f:()) -> a (D3 d e f)) -> (g:'D) -> a g
+match'D :: (a : Type->Type) -> a 'D -> (b:Type) -> a b -> a b
 d2 :: () -> ()->'D
 d3 :: () -> () -> ()->'D
 ------------ tooltips
diff --git a/testdata/language-features/basic-values/typesig04.out b/testdata/language-features/basic-values/typesig04.out
index 773e6f5a..fe8c7208 100644
--- a/testdata/language-features/basic-values/typesig04.out
+++ b/testdata/language-features/basic-values/typesig04.out
@@ -1,7 +1,7 @@
 main is not found
 ------------ trace
-fun1 :: {a} -> {b} -> {c} -> a -> b->c -> ()
-fun2 :: {a} -> {b} -> {c} -> a -> b->c -> ()
+fun1 :: {a} -> {b} -> {c} -> a -> (b->c)->()
+fun2 :: {a} -> {b} -> {c} -> a -> (b->c)->()
 ------------ tooltips
 testdata/language-features/basic-values/typesig04.lc 1:9-1:10  f_
 testdata/language-features/basic-values/typesig04.lc 1:9-1:28  Type
@@ -9,13 +9,13 @@ testdata/language-features/basic-values/typesig04.lc 1:14-1:28  Type
 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: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 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
 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: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_)->()
diff --git a/testdata/performance/Material.out b/testdata/performance/Material.out
index 5e629ad7..0e92cbe1 100644
--- a/testdata/performance/Material.out
+++ b/testdata/performance/Material.out
@@ -3,8 +3,8 @@ main is not found
 identityLight :: 'Float
 'Entity :: Type
 Entity :: 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 3 'Float -> 'Vec 4 'Float -> 'Entity
-'EntityCase :: (a : 'Entity->Type) -> ((b : 'Vec 4 'Float) -> (c : 'Vec 4 'Float) -> (d : 'Vec 3 'Float) -> (e : 'Vec 4 'Float) -> a (Entity b c d e)) -> f:'Entity -> a f
-match'Entity :: (a : Type->Type) -> a 'Entity -> b:Type -> a b -> a b
+'EntityCase :: (a : 'Entity->Type) -> ((b : 'Vec 4 'Float) -> (c : 'Vec 4 'Float) -> (d : 'Vec 3 'Float) -> (e : 'Vec 4 'Float) -> a (Entity b c d e)) -> (f:'Entity) -> a f
+match'Entity :: (a : Type->Type) -> a 'Entity -> (b:Type) -> a b -> a b
 eAmbientLight :: 'Entity -> 'VecS 'Float 4
 eDirectedLight :: 'Entity -> 'VecS 'Float 4
 eLightDir :: 'Entity -> 'VecS 'Float 3
@@ -16,12 +16,12 @@ WT_Square :: 'WaveType
 WT_Sawtooth :: 'WaveType
 WT_InverseSawtooth :: 'WaveType
 WT_Noise :: 'WaveType
-'WaveTypeCase :: (a : 'WaveType->Type) -> a WT_Sin -> a WT_Triangle -> a WT_Square -> a WT_Sawtooth -> a WT_InverseSawtooth -> a WT_Noise -> b:'WaveType -> a b
-match'WaveType :: (a : Type->Type) -> a 'WaveType -> b:Type -> a b -> a b
+'WaveTypeCase :: (a : 'WaveType->Type) -> a WT_Sin -> a WT_Triangle -> a WT_Square -> a WT_Sawtooth -> a WT_InverseSawtooth -> a WT_Noise -> (b:'WaveType) -> a b
+match'WaveType :: (a : Type->Type) -> a 'WaveType -> (b:Type) -> a b -> a b
 'Wave :: Type
 Wave :: 'WaveType -> 'Float -> 'Float -> 'Float -> 'Float->'Wave
-'WaveCase :: (a : 'Wave->Type) -> (b:'WaveType -> c:'Float -> d:'Float -> e:'Float -> f:'Float -> a (Wave b c d e f)) -> g:'Wave -> a g
-match'Wave :: (a : Type->Type) -> a 'Wave -> b:Type -> a b -> a b
+'WaveCase :: (a : 'Wave->Type) -> ((b:'WaveType) -> (c:'Float) -> (d:'Float) -> (e:'Float) -> (f:'Float) -> a (Wave b c d e f)) -> (g:'Wave) -> a g
+match'Wave :: (a : Type->Type) -> a 'Wave -> (b:Type) -> a b -> a b
 'Deform :: Type
 D_AutoSprite :: 'Deform
 D_AutoSprite2 :: 'Deform
@@ -38,14 +38,14 @@ D_Text5 :: 'Deform
 D_Text6 :: 'Deform
 D_Text7 :: 'Deform
 D_Wave :: 'Float -> 'Wave->'Deform
-'DeformCase :: (a : 'Deform->Type) -> a D_AutoSprite -> a D_AutoSprite2 -> (b:'Float -> c:'Float -> d:'Float -> a (D_Bulge b c d)) -> ((e : 'Vec 3 'Float) -> f:'Wave -> a (D_Move e f)) -> (g:'Float -> h:'Float -> a (D_Normal g h)) -> a D_ProjectionShadow -> a D_Text0 -> a D_Text1 -> a D_Text2 -> a D_Text3 -> a D_Text4 -> a D_Text5 -> a D_Text6 -> a D_Text7 -> (i:'Float -> j:'Wave -> a (D_Wave i j)) -> k:'Deform -> a k
-match'Deform :: (a : Type->Type) -> a 'Deform -> b:Type -> a b -> a b
+'DeformCase :: (a : 'Deform->Type) -> a D_AutoSprite -> a D_AutoSprite2 -> ((b:'Float) -> (c:'Float) -> (d:'Float) -> a (D_Bulge b c d)) -> ((e : 'Vec 3 'Float) -> (f:'Wave) -> a (D_Move e f)) -> ((g:'Float) -> (h:'Float) -> a (D_Normal g h)) -> a D_ProjectionShadow -> a D_Text0 -> a D_Text1 -> a D_Text2 -> a D_Text3 -> a D_Text4 -> a D_Text5 -> a D_Text6 -> a D_Text7 -> ((i:'Float) -> (j:'Wave) -> a (D_Wave i j)) -> (k:'Deform) -> a k
+match'Deform :: (a : Type->Type) -> a 'Deform -> (b:Type) -> a b -> a b
 'CullType :: Type
 CT_FrontSided :: 'CullType
 CT_BackSided :: 'CullType
 CT_TwoSided :: 'CullType
-'CullTypeCase :: (a : 'CullType->Type) -> a CT_FrontSided -> a CT_BackSided -> a CT_TwoSided -> b:'CullType -> a b
-match'CullType :: (a : Type->Type) -> a 'CullType -> b:Type -> a b -> a b
+'CullTypeCase :: (a : 'CullType->Type) -> a CT_FrontSided -> a CT_BackSided -> a CT_TwoSided -> (b:'CullType) -> a b
+match'CullType :: (a : Type->Type) -> a 'CullType -> (b:Type) -> a b -> a b
 'Blending' :: Type
 B_DstAlpha :: 'Blending'
 B_DstColor :: 'Blending'
@@ -58,8 +58,8 @@ B_SrcAlpha :: 'Blending'
 B_SrcAlphaSaturate :: 'Blending'
 B_SrcColor :: 'Blending'
 B_Zero :: 'Blending'
-'Blending'Case :: (a : 'Blending'->Type) -> a B_DstAlpha -> a B_DstColor -> a B_One -> a B_OneMinusDstAlpha -> a B_OneMinusDstColor -> a B_OneMinusSrcAlpha -> a B_OneMinusSrcColor -> a B_SrcAlpha -> a B_SrcAlphaSaturate -> a B_SrcColor -> a B_Zero -> b:'Blending' -> a b
-match'Blending' :: (a : Type->Type) -> a 'Blending' -> b:Type -> a b -> a b
+'Blending'Case :: (a : 'Blending'->Type) -> a B_DstAlpha -> a B_DstColor -> a B_One -> a B_OneMinusDstAlpha -> a B_OneMinusDstColor -> a B_OneMinusSrcAlpha -> a B_OneMinusSrcColor -> a B_SrcAlpha -> a B_SrcAlphaSaturate -> a B_SrcColor -> a B_Zero -> (b:'Blending') -> a b
+match'Blending' :: (a : Type->Type) -> a 'Blending' -> (b:Type) -> a b -> a b
 'RGBGen :: Type
 RGB_Wave :: 'Wave->'RGBGen
 RGB_Const :: 'Float -> 'Float -> 'Float->'RGBGen
@@ -72,8 +72,8 @@ RGB_Vertex :: 'RGBGen
 RGB_LightingDiffuse :: 'RGBGen
 RGB_OneMinusVertex :: 'RGBGen
 RGB_Undefined :: 'RGBGen
-'RGBGenCase :: (a : 'RGBGen->Type) -> (b:'Wave -> a (RGB_Wave b)) -> (c:'Float -> d:'Float -> e:'Float -> a (RGB_Const c d e)) -> a RGB_Identity -> a RGB_IdentityLighting -> a RGB_Entity -> a RGB_OneMinusEntity -> a RGB_ExactVertex -> a RGB_Vertex -> a RGB_LightingDiffuse -> a RGB_OneMinusVertex -> a RGB_Undefined -> f:'RGBGen -> a f
-match'RGBGen :: (a : Type->Type) -> a 'RGBGen -> b:Type -> a b -> a b
+'RGBGenCase :: (a : 'RGBGen->Type) -> ((b:'Wave) -> a (RGB_Wave b)) -> ((c:'Float) -> (d:'Float) -> (e:'Float) -> a (RGB_Const c d e)) -> a RGB_Identity -> a RGB_IdentityLighting -> a RGB_Entity -> a RGB_OneMinusEntity -> a RGB_ExactVertex -> a RGB_Vertex -> a RGB_LightingDiffuse -> a RGB_OneMinusVertex -> a RGB_Undefined -> (f:'RGBGen) -> a f
+match'RGBGen :: (a : Type->Type) -> a 'RGBGen -> (b:Type) -> a b -> a b
 'AlphaGen :: Type
 A_Wave :: 'Wave->'AlphaGen
 A_Const :: 'Float->'AlphaGen
@@ -84,16 +84,16 @@ A_OneMinusEntity :: 'AlphaGen
 A_Vertex :: 'AlphaGen
 A_LightingSpecular :: 'AlphaGen
 A_OneMinusVertex :: 'AlphaGen
-'AlphaGenCase :: (a : 'AlphaGen->Type) -> (b:'Wave -> a (A_Wave b)) -> (c:'Float -> a (A_Const c)) -> a A_Portal -> a A_Identity -> a A_Entity -> a A_OneMinusEntity -> a A_Vertex -> a A_LightingSpecular -> a A_OneMinusVertex -> d:'AlphaGen -> a d
-match'AlphaGen :: (a : Type->Type) -> a 'AlphaGen -> b:Type -> a b -> a b
+'AlphaGenCase :: (a : 'AlphaGen->Type) -> ((b:'Wave) -> a (A_Wave b)) -> ((c:'Float) -> a (A_Const c)) -> a A_Portal -> a A_Identity -> a A_Entity -> a A_OneMinusEntity -> a A_Vertex -> a A_LightingSpecular -> a A_OneMinusVertex -> (d:'AlphaGen) -> a d
+match'AlphaGen :: (a : Type->Type) -> a 'AlphaGen -> (b:Type) -> a b -> a b
 'TCGen :: Type
 TG_Base :: 'TCGen
 TG_Lightmap :: 'TCGen
 TG_Environment :: 'TCGen
 TG_Vector :: 'Vec 3 'Float -> 'Vec 3 'Float -> 'TCGen
 TG_Undefined :: 'TCGen
-'TCGenCase :: (a : 'TCGen->Type) -> a TG_Base -> a TG_Lightmap -> a TG_Environment -> ((b : 'Vec 3 'Float) -> (c : 'Vec 3 'Float) -> a (TG_Vector b c)) -> a TG_Undefined -> d:'TCGen -> a d
-match'TCGen :: (a : Type->Type) -> a 'TCGen -> b:Type -> a b -> a b
+'TCGenCase :: (a : 'TCGen->Type) -> a TG_Base -> a TG_Lightmap -> a TG_Environment -> ((b : 'Vec 3 'Float) -> (c : 'Vec 3 'Float) -> a (TG_Vector b c)) -> a TG_Undefined -> (d:'TCGen) -> a d
+match'TCGen :: (a : Type->Type) -> a 'TCGen -> (b:Type) -> a b -> a b
 'TCMod :: Type
 TM_EntityTranslate :: 'TCMod
 TM_Rotate :: 'Float->'TCMod
@@ -102,31 +102,31 @@ TM_Scale :: 'Float -> 'Float->'TCMod
 TM_Stretch :: 'Wave->'TCMod
 TM_Transform :: 'Float -> 'Float -> 'Float -> 'Float -> 'Float -> 'Float->'TCMod
 TM_Turb :: 'Float -> 'Float -> 'Float -> 'Float->'TCMod
-'TCModCase :: (a : 'TCMod->Type) -> a TM_EntityTranslate -> (b:'Float -> a (TM_Rotate b)) -> (c:'Float -> d:'Float -> a (TM_Scroll c d)) -> (e:'Float -> f:'Float -> a (TM_Scale e f)) -> (g:'Wave -> a (TM_Stretch g)) -> (h:'Float -> i:'Float -> j:'Float -> k:'Float -> l:'Float -> m:'Float -> a (TM_Transform h i j k l m)) -> (n:'Float -> o:'Float -> p:'Float -> q:'Float -> a (TM_Turb n o p q)) -> r:'TCMod -> a r
-match'TCMod :: (a : Type->Type) -> a 'TCMod -> b:Type -> a b -> a b
+'TCModCase :: (a : 'TCMod->Type) -> a TM_EntityTranslate -> ((b:'Float) -> a (TM_Rotate b)) -> ((c:'Float) -> (d:'Float) -> a (TM_Scroll c d)) -> ((e:'Float) -> (f:'Float) -> a (TM_Scale e f)) -> ((g:'Wave) -> a (TM_Stretch g)) -> ((h:'Float) -> (i:'Float) -> (j:'Float) -> (k:'Float) -> (l:'Float) -> (m:'Float) -> a (TM_Transform h i j k l m)) -> ((n:'Float) -> (o:'Float) -> (p:'Float) -> (q:'Float) -> a (TM_Turb n o p q)) -> (r:'TCMod) -> a r
+match'TCMod :: (a : Type->Type) -> a 'TCMod -> (b:Type) -> a b -> a b
 'StageTexture :: Type
 ST_Map :: 'String->'StageTexture
 ST_ClampMap :: 'String->'StageTexture
 ST_AnimMap :: 'Float -> 'List 'String -> 'StageTexture
 ST_Lightmap :: 'StageTexture
 ST_WhiteImage :: 'StageTexture
-'StageTextureCase :: (a : 'StageTexture->Type) -> (b:'String -> a (ST_Map b)) -> (c:'String -> a (ST_ClampMap c)) -> (d:'Float -> (e : 'List 'String) -> a (ST_AnimMap d e)) -> a ST_Lightmap -> a ST_WhiteImage -> f:'StageTexture -> a f
-match'StageTexture :: (a : Type->Type) -> a 'StageTexture -> b:Type -> a b -> a b
+'StageTextureCase :: (a : 'StageTexture->Type) -> ((b:'String) -> a (ST_Map b)) -> ((c:'String) -> a (ST_ClampMap c)) -> ((d:'Float) -> (e : 'List 'String) -> a (ST_AnimMap d e)) -> a ST_Lightmap -> a ST_WhiteImage -> (f:'StageTexture) -> a f
+match'StageTexture :: (a : Type->Type) -> a 'StageTexture -> (b:Type) -> a b -> a b
 'AlphaFunction :: Type
 A_Gt0 :: 'AlphaFunction
 A_Lt128 :: 'AlphaFunction
 A_Ge128 :: 'AlphaFunction
-'AlphaFunctionCase :: (a : 'AlphaFunction->Type) -> a A_Gt0 -> a A_Lt128 -> a A_Ge128 -> b:'AlphaFunction -> a b
-match'AlphaFunction :: (a : Type->Type) -> a 'AlphaFunction -> b:Type -> a b -> a b
+'AlphaFunctionCase :: (a : 'AlphaFunction->Type) -> a A_Gt0 -> a A_Lt128 -> a A_Ge128 -> (b:'AlphaFunction) -> a b
+match'AlphaFunction :: (a : Type->Type) -> a 'AlphaFunction -> (b:Type) -> a b -> a b
 'DepthFunction :: Type
 D_Equal :: 'DepthFunction
 D_Lequal :: 'DepthFunction
-'DepthFunctionCase :: (a : 'DepthFunction->Type) -> a D_Equal -> a D_Lequal -> b:'DepthFunction -> a b
-match'DepthFunction :: (a : Type->Type) -> a 'DepthFunction -> b:Type -> a b -> a b
+'DepthFunctionCase :: (a : 'DepthFunction->Type) -> a D_Equal -> a D_Lequal -> (b:'DepthFunction) -> a b
+match'DepthFunction :: (a : Type->Type) -> a 'DepthFunction -> (b:Type) -> a b -> a b
 'StageAttrs :: Type
 StageAttrs :: 'Maybe ('Blending', 'Blending') -> 'RGBGen -> 'AlphaGen -> 'TCGen -> 'List 'TCMod -> 'StageTexture -> 'Bool -> 'DepthFunction -> 'Maybe 'AlphaFunction -> 'Bool -> 'String->'StageAttrs
-'StageAttrsCase :: (a : 'StageAttrs->Type) -> ((b : 'Maybe ('Blending', 'Blending')) -> c:'RGBGen -> d:'AlphaGen -> e:'TCGen -> (f : 'List 'TCMod) -> g:'StageTexture -> h:'Bool -> i:'DepthFunction -> (j : 'Maybe 'AlphaFunction) -> k:'Bool -> l:'String -> a (StageAttrs b c d e f g h i j k l)) -> m:'StageAttrs -> a m
-match'StageAttrs :: (a : Type->Type) -> a 'StageAttrs -> b:Type -> a b -> a b
+'StageAttrsCase :: (a : 'StageAttrs->Type) -> ((b : 'Maybe ('Blending', 'Blending')) -> (c:'RGBGen) -> (d:'AlphaGen) -> (e:'TCGen) -> (f : 'List 'TCMod) -> (g:'StageTexture) -> (h:'Bool) -> (i:'DepthFunction) -> (j : 'Maybe 'AlphaFunction) -> (k:'Bool) -> (l:'String) -> a (StageAttrs b c d e f g h i j k l)) -> (m:'StageAttrs) -> a m
+match'StageAttrs :: (a : Type->Type) -> a 'StageAttrs -> (b:Type) -> a b -> a b
 saBlend :: 'StageAttrs -> 'Maybe ('Blending', 'Blending')
 saRGBGen :: 'StageAttrs->'RGBGen
 saAlphaGen :: 'StageAttrs->'AlphaGen
@@ -141,8 +141,8 @@ saTextureUniform :: 'StageAttrs->'String
 defaultStageAttrs :: 'StageAttrs
 'CommonAttrs :: Type
 CommonAttrs :: () -> () -> 'Bool -> 'Float -> 'Bool -> 'Bool -> 'CullType -> 'List 'Deform -> 'Bool -> 'Bool -> 'List 'StageAttrs -> 'Bool->'CommonAttrs
-'CommonAttrsCase :: (a : 'CommonAttrs->Type) -> (b:() -> c:() -> d:'Bool -> e:'Float -> f:'Bool -> g:'Bool -> h:'CullType -> (i : 'List 'Deform) -> j:'Bool -> k:'Bool -> (l : 'List 'StageAttrs) -> m:'Bool -> a (CommonAttrs b c d e f g h i j k l m)) -> n:'CommonAttrs -> a n
-match'CommonAttrs :: (a : Type->Type) -> a 'CommonAttrs -> b:Type -> a b -> a b
+'CommonAttrsCase :: (a : 'CommonAttrs->Type) -> ((b:()) -> (c:()) -> (d:'Bool) -> (e:'Float) -> (f:'Bool) -> (g:'Bool) -> (h:'CullType) -> (i : 'List 'Deform) -> (j:'Bool) -> (k:'Bool) -> (l : 'List 'StageAttrs) -> (m:'Bool) -> a (CommonAttrs b c d e f g h i j k l m)) -> (n:'CommonAttrs) -> a n
+match'CommonAttrs :: (a : Type->Type) -> a 'CommonAttrs -> (b:Type) -> a b -> a b
 caSkyParms :: 'CommonAttrs->()
 caFogParms :: 'CommonAttrs->()
 caPortal :: 'CommonAttrs->'Bool
diff --git a/testdata/record01.reject.out b/testdata/record01.reject.out
index 78ef20e3..32ed09fc 100644
--- a/testdata/record01.reject.out
+++ b/testdata/record01.reject.out
@@ -167,7 +167,7 @@ testdata/record01.reject.lc 18:65-18:70  Type->Type
 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: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: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)
@@ -205,7 +205,7 @@ 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: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: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)))
diff --git a/testdata/traceTest.out b/testdata/traceTest.out
index b2893066..06096c39 100644
--- a/testdata/traceTest.out
+++ b/testdata/traceTest.out
@@ -3,8 +3,8 @@ main is not found
 id :: {a} -> a->a
 'X :: {a} -> a->Type
 'XCase :: {a} -> {b:a} -> (c : 'X a b -> Type) -> (d : 'X a b) -> c d
-match'X :: (a : Type->Type) -> ({b} -> c:b -> a ('X b c)) -> d:Type -> a d -> a d
-x :: 'X (Type -> Type->Type) (\a:Type b:Type -> (a, b))
+match'X :: (a : Type->Type) -> ({b} -> (c:b) -> a ('X b c)) -> (d:Type) -> a d -> a d
+x :: 'X (Type -> Type->Type) (\(a:Type) (b:Type) -> (a, b))
 ------------ tooltips
 testdata/traceTest.lc 6:1-6:3  {a} -> a->a
 testdata/traceTest.lc 6:8-6:9  b_
@@ -17,5 +17,5 @@ testdata/traceTest.lc 10:17-10:24  Type
 testdata/traceTest.lc 10:19-10:20  e_
 testdata/traceTest.lc 10:19-10:23  List Type
 testdata/traceTest.lc 10:22-10:23  List Type | c_
-testdata/traceTest.lc 11:1-11:2  X (Type -> Type->Type) (\a:Type b:Type -> (a, b))
+testdata/traceTest.lc 11:1-11:2  X (Type -> Type->Type) (\(a:Type) (b:Type) -> (a, b))
 testdata/traceTest.lc 11:5-11:14  {a}->a
diff --git a/testdata/typesig.reject.out b/testdata/typesig.reject.out
index f6a0fd30..923cc1be 100644
--- a/testdata/typesig.reject.out
+++ b/testdata/typesig.reject.out
@@ -1,11 +1,11 @@
-focus checkMetas: \a -> (\b:Type -> primFix a b) (\(a:=Type) -> \c:Type -> <<HERE>>)
+focus checkMetas: \a -> (\(b:Type) -> primFix a b) (\(a:=Type) -> \(c:Type) -> <<HERE>>)
 \(a : Type~a_) (b : b_~'X) -> typeAnn c_ (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>>)
+'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)
 ------------ tooltips
 testdata/typesig.reject.lc 4:6-4:7  Type
diff --git a/testdata/typesigctx.reject.out b/testdata/typesigctx.reject.out
index b0c80fab..6696ad4a 100644
--- a/testdata/typesigctx.reject.out
+++ b/testdata/typesigctx.reject.out
@@ -4,8 +4,8 @@ in Wildcard2 builtin 'Type
 ------------ 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
+'XCase :: (a : 'X->Type) -> a X -> (b:'X) -> a b
+match'X :: (a : Type->Type) -> a 'X -> (b:Type) -> a b -> a b
 'Show' :: Type->Type
 show' :: {a} -> {_ : 'Show' a} -> a->'X
 !type error: no instance of 'Show' on ???