more list syntax in pretty print

1 files changed, 281 insertions, 284 deletions

diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index 85fa9d7f..4010c01b 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -1,9 +1,9 @@
 ------------ desugared source code
 id = \(a :: _) -> _rhs a
 data VecS (_ :: Type) :: Nat -> Type where
-    V2 :: _a -> _a -> VecS _a (fromInt 2)
-    V3 :: _a -> _a -> _a -> VecS _a (fromInt 3)
-    V4 :: _a -> _a -> _a -> _a -> VecS _a (fromInt 4)
+    V2 :: forall a . a -> a -> VecS a (fromInt 2)
+    V3 :: forall b . b -> b -> b -> VecS b (fromInt 3)
+    V4 :: forall c . c -> c -> c -> c -> VecS c (fromInt 4)
 mapVec
   = (\(a :: _) (b :: _) -> 'VecSCase
       \_ -> \_ -> _ :: _
@@ -566,7 +566,7 @@ PrimSign
   :: forall (a :: _) (b :: _) (c :: _) . (Signed a, b ~ VecScalar c a) => b -> b
 PrimModF
   :: forall (a :: _) (b :: _)
-    . (a ~ VecScalar b Float) => a -> HList (a : a : 'Nil)
+    . (a ~ VecScalar b Float) => a -> HList (a : a : '[])
 PrimClamp
   :: forall (a :: _) (b :: _) (c :: _)
     . (Num a, b ~ VecScalar c a) => b -> b -> b -> b
@@ -671,7 +671,7 @@ map
     b
 concatMap
   = (\(a :: _) (b :: _) -> _rhs (concat (map a b)))
-    :: forall (c :: _) (d :: _) . (c -> List d) -> List c -> List d
+    :: forall (c :: _) (d :: _) . (c -> [d]) -> [c] -> [d]
 len
   = \(a :: _) -> 'ListCase
     \_ -> _ :: _
@@ -679,8 +679,8 @@ len
     \_ (b :: _) -> _rhs (fromInt 1 `primAddInt` len b)
     a
 data Maybe (_ :: Type) :: Type where
-    Nothing :: Maybe _a
-    Just :: _a -> Maybe _a
+    Nothing :: forall a . Maybe a
+    Just :: forall b . b -> Maybe b
 data Vector (_ :: Nat) (_ :: Type) :: Type where
     
 data PrimitiveType :: Type where
@@ -690,13 +690,13 @@ data PrimitiveType :: Type where
     TriangleAdjacency :: PrimitiveType
     LineAdjacency :: PrimitiveType
 data Primitive (_ :: Type) :: PrimitiveType -> Type where
-    PrimPoint :: _a -> Primitive _a Point
-    PrimLine :: _a -> _a -> Primitive _a Line
-    PrimTriangle :: _a -> _a -> _a -> Primitive _a Triangle
+    PrimPoint :: forall a . a -> Primitive a Point
+    PrimLine :: forall b . b -> b -> Primitive b Line
+    PrimTriangle :: forall c . c -> c -> c -> Primitive c Triangle
 mapPrimitive
   :: forall (a :: _) (b :: _) (c :: _)
     . (a -> b) -> Primitive a c -> Primitive b c
-'PrimitiveStream = \(a :: _) (b :: _) -> _rhs ('List ('Primitive b a))
+'PrimitiveStream = \(a :: _) (b :: _) -> _rhs ['Primitive b a]
 mapPrimitives
   = (\(a :: _) -> _rhs (map (mapPrimitive a)))
     :: forall (b :: _) (c :: _) (d :: _)
@@ -711,17 +711,17 @@ fetch
   :: forall (a :: _) (b :: _) . String -> HList b -> PrimitiveStream a (HList b)
 Attribute :: forall (a :: _) . String -> a
 fetchStream
-  :: forall (a :: _) (b :: List Type)
+  :: forall (a :: _) (b :: [Type])
     . String
-      -> forall (c :: List String) -> (len c ~ len b) => PrimitiveStream a (HList b)
+      -> forall (c :: [String]) -> (len c ~ len b) => PrimitiveStream a (HList b)
 data SimpleFragment (_ :: Type) :: Type where
-    SimpleFragment :: Vec (fromInt 3) Float -> _a -> SimpleFragment _a
+    SimpleFragment :: forall a . Vec (fromInt 3) Float -> a -> SimpleFragment a
 'Fragment = \(a :: _) (b :: _) -> _rhs ('Vector a ('Maybe ('SimpleFragment b)))
 sFragmentCoords
   = \(a :: _) -> 'SimpleFragmentCase \_ -> _ :: _ \(b :: _) -> \_ -> _rhs b a
 sFragmentValue
   = \(a :: _) -> 'SimpleFragmentCase \_ -> _ :: _ \_ (b :: _) -> _rhs b a
-'FragmentStream = \(a :: _) (b :: _) -> _rhs ('List ('Fragment a b))
+'FragmentStream = \(a :: _) (b :: _) -> _rhs ['Fragment a b]
 customizeDepth
   :: forall (a :: _) (b :: _) . (a -> Float) -> Fragment b a -> Fragment b a
 customizeDepths
@@ -872,36 +872,37 @@ data CullMode :: Type where
     CullBack :: CullMode
     CullNone :: CullMode
 data PointSize (_ :: Type) :: Type where
-    PointSize :: Float -> PointSize _a
-    ProgramPointSize :: (_a -> Float) -> PointSize _a
+    PointSize :: forall a . Float -> PointSize a
+    ProgramPointSize :: forall b . (b -> Float) -> PointSize b
 data PolygonMode (_ :: Type) :: Type where
-    PolygonFill :: PolygonMode _a
-    PolygonPoint :: PointSize _a -> PolygonMode _a
-    PolygonLine :: Float -> PolygonMode _a
+    PolygonFill :: forall a . PolygonMode a
+    PolygonPoint :: forall b . PointSize b -> PolygonMode b
+    PolygonLine :: forall c . Float -> PolygonMode c
 data PolygonOffset :: Type where
     NoOffset :: PolygonOffset
     Offset :: Float -> Float -> PolygonOffset
 data PointSpriteCoordOrigin :: Type where
     LowerLeft :: PointSpriteCoordOrigin
     UpperLeft :: PointSpriteCoordOrigin
-primTexture :: HList 'Nil -> Vec (fromInt 2) Float -> Vec (fromInt 4) Float
+primTexture :: HList '[] -> Vec (fromInt 2) Float -> Vec (fromInt 4) Float
 Uniform :: forall (a :: _) . String -> a
 data RasterContext (_ :: Type) :: PrimitiveType -> Type where
     TriangleCtx
-      :: CullMode
-        -> PolygonMode _a
-          -> PolygonOffset -> ProvokingVertex -> RasterContext _a Triangle
+      :: forall a
+        . CullMode
+          -> PolygonMode a -> PolygonOffset -> ProvokingVertex -> RasterContext a Triangle
     PointCtx
-      :: PointSize _a -> Float -> PointSpriteCoordOrigin -> RasterContext _a Point
-    LineCtx :: Float -> ProvokingVertex -> RasterContext _a Line
+      :: forall b
+        . PointSize b -> Float -> PointSpriteCoordOrigin -> RasterContext b Point
+    LineCtx :: forall c . Float -> ProvokingVertex -> RasterContext c Line
 data Blending :: Type -> Type where
     NoBlending :: forall (a :: _) . Blending a
     BlendLogicOp :: forall (b :: _) . Integral b => LogicOperation -> Blending b
     Blend
-      :: HList (BlendEquation : BlendEquation : 'Nil)
+      :: HList (BlendEquation : BlendEquation : '[])
         -> HList
-            (HList (BlendingFactor : BlendingFactor : 'Nil)
-              : HList (BlendingFactor : BlendingFactor : 'Nil) : 'Nil)
+            (HList (BlendingFactor : BlendingFactor : '[])
+              : HList (BlendingFactor : BlendingFactor : '[]) : '[])
           -> Vec (fromInt 4) Float -> Blending Float
 data StencilTests :: Type where
     
@@ -916,9 +917,9 @@ data FragmentOperation :: ImageKind -> Type where
     StencilOp
       :: StencilTests -> StencilOps -> StencilOps -> FragmentOperation Stencil
 data Interpolated (_ :: Type) :: Type where
-    Smooth :: Floating _a => Interpolated _a
-    NoPerspective :: Floating _a => Interpolated _a
-    Flat :: Interpolated _a
+    Smooth :: forall a . Floating a => Interpolated a
+    NoPerspective :: forall b . Floating b => Interpolated b
+    Flat :: forall c . Interpolated c
 rasterizePrimitive
   :: forall (a :: _) (b :: _) (c :: _) (d :: _)
     . (map Interpolated a ~ b, c ~ Vec (fromInt 4) Float : a)
@@ -940,9 +941,9 @@ allSame
         \(d :: _) (e :: _) -> _rhs ('T2 (b ~ d) (allSame (d : e)))
         c
       a)
-    :: forall (f :: _) . List f -> Type
+    :: forall (f :: _) . [f] -> Type
 sameLayerCounts = \(a :: _) -> _rhs (allSame (map 'ImageLC a))
-data FrameBuffer (_ :: Nat) (_ :: List ImageKind) :: Type where
+data FrameBuffer (_ :: Nat) (_ :: [ImageKind]) :: Type where
     
 imageType'
   = (\(a :: _) -> 'ListCase
@@ -955,12 +956,12 @@ imageType'
         (_rhs (map imageType a))
         b
       a)
-    :: List ImageKind -> List Type
+    :: [ImageKind] -> [Type]
 'FragmentOperationKind
   = (\(a :: _) -> match'FragmentOperation \_ -> _ \(b :: _) -> _rhs b a undefined)
     :: Type -> ImageKind
 Accumulate
-  :: forall (a :: _) (b :: Nat) (c :: List Type)
+  :: forall (a :: _) (b :: Nat) (c :: [Type])
     . (a ~ map FragmentOperationKind c)
       => HList c
         -> FragmentStream b (HList (imageType' a)) -> FrameBuffer b a -> FrameBuffer b a
@@ -978,7 +979,7 @@ infixl 0 overlay
   = (\(a :: _) -> match'Image \_ -> _ \_ (b :: _) -> _rhs b a undefined)
     :: Type -> ImageKind
 FrameBuffer
-  :: forall (a :: List Type)
+  :: forall (a :: [Type])
     . sameLayerCounts a
       => HList a -> FrameBuffer (ImageLC (head a)) (map GetImageKind a)
 imageFrame = _rhs FrameBuffer
@@ -986,9 +987,9 @@ accumulate
   = \(a :: _) (b :: _) (c :: _) (d :: _) -> _rhs
     (Accumulate a (mapFragments b c) d)
 PrjImage
-  :: forall (a :: _) . FrameBuffer (fromInt 1) (a : 'Nil) -> Image (fromInt 1) a
+  :: forall (a :: _) . FrameBuffer (fromInt 1) (a : '[]) -> Image (fromInt 1) a
 PrjImageColor
-  :: FrameBuffer (fromInt 1) ('Depth : 'Color (Vec (fromInt 4) Float) : 'Nil)
+  :: FrameBuffer (fromInt 1) ('Depth : 'Color (Vec (fromInt 4) Float) : '[])
     -> Image (fromInt 1) (Color (Vec (fromInt 4) Float))
 data Output :: Type where
     ScreenOut :: forall (a :: _) (b :: _) . FrameBuffer a b -> Output
@@ -1222,13 +1223,13 @@ PrimNoise1 :: forall (a :: Nat) . VecScalar a Float -> Float
 PrimNoise2 :: forall (a :: Nat) . VecScalar a Float -> Vec 2 Float
 PrimNoise3 :: forall (a :: Nat) . VecScalar a Float -> Vec 3 Float
 PrimNoise4 :: forall (a :: Nat) . VecScalar a Float -> Vec 4 Float
-head :: forall a . List a -> a
-++ :: forall a . List a -> List a -> List a
-foldr :: forall a b . (b -> a -> a) -> a -> List b -> a
-concat :: forall a . List (List a) -> List a
-map :: forall a b . (a -> b) -> List a -> List b
-concatMap :: forall a b . (a -> List b) -> List a -> List b
-len :: forall a . List a -> Int
+head :: forall a . [a] -> a
+++ :: forall a . [a] -> [a] -> [a]
+foldr :: forall a b . (b -> a -> a) -> a -> [b] -> a
+concat :: forall a . [[a]] -> [a]
+map :: forall a b . (a -> b) -> [a] -> [b]
+concatMap :: forall a b . (a -> [b]) -> [a] -> [b]
+len :: forall a . [a] -> Int
 'Maybe :: Type -> Type
 Nothing :: forall a . Maybe a
 Just :: forall a . a -> Maybe a
@@ -1282,19 +1283,19 @@ mapPrimitive
 'PrimitiveStream :: PrimitiveType -> Type -> Type
 mapPrimitives
   :: forall a b (c :: PrimitiveType)
-    . (a -> b) -> List (Primitive a c) -> List (Primitive b c)
+    . (a -> b) -> [Primitive a c] -> [Primitive b c]
 'ListElem :: Type -> Type
 fetchArrays
-  :: forall (a :: PrimitiveType) (b :: List Type) (c :: List Type)
+  :: forall (a :: PrimitiveType) (b :: [Type]) (c :: [Type])
     . (b ~ map Type Type ListElem c) => HList c -> PrimitiveStream a (HList b)
 fetch
-  :: forall (a :: PrimitiveType) (b :: List Type)
+  :: forall (a :: PrimitiveType) (b :: [Type])
     . String -> HList b -> PrimitiveStream a (HList b)
 Attribute :: forall a . String -> a
 fetchStream
-  :: forall (a :: PrimitiveType) (b :: List Type)
+  :: forall (a :: PrimitiveType) (b :: [Type])
     . String
-      -> forall (c :: List String)
+      -> forall (c :: [String])
         -> (len String c ~ len Type b) => PrimitiveStream a (HList b)
 'SimpleFragment :: Type -> Type
 SimpleFragment :: forall a . Vec 3 Float -> a -> SimpleFragment a
@@ -1315,21 +1316,21 @@ customizeDepth
 customizeDepths
   :: forall a (b :: Nat)
     . (a -> Float)
-      -> List (Vector b (Maybe (SimpleFragment a)))
-        -> List (Vector b (Maybe (SimpleFragment a)))
+      -> [Vector b (Maybe (SimpleFragment a))]
+        -> [Vector b (Maybe (SimpleFragment a))]
 filterFragment
   :: forall a (b :: Nat) . (a -> Bool) -> Fragment b a -> Fragment b a
 filterFragments
   :: forall a (b :: Nat)
     . (a -> Bool)
-      -> List (Vector b (Maybe (SimpleFragment a)))
-        -> List (Vector b (Maybe (SimpleFragment a)))
+      -> [Vector b (Maybe (SimpleFragment a))]
+        -> [Vector b (Maybe (SimpleFragment a))]
 mapFragment :: forall a b (c :: Nat) . (a -> b) -> Fragment c a -> Fragment c b
 mapFragments
   :: forall a b (c :: Nat)
     . (a -> b)
-      -> List (Vector c (Maybe (SimpleFragment a)))
-        -> List (Vector c (Maybe (SimpleFragment b)))
+      -> [Vector c (Maybe (SimpleFragment a))]
+        -> [Vector c (Maybe (SimpleFragment b))]
 'ImageKind :: Type
 Color :: Type -> ImageKind
 Depth :: ImageKind
@@ -1646,75 +1647,74 @@ match'Interpolated
   :: forall (a :: Type -> Type)
     -> (forall b -> a (Interpolated b)) -> forall c -> a c -> a c
 rasterizePrimitive
-  :: forall (a :: List Type)
-      (b :: List Type) (c :: List Type) (d :: PrimitiveType)
+  :: forall (a :: [Type]) (b :: [Type]) (c :: [Type]) (d :: PrimitiveType)
     . (map Type Type Interpolated a ~ b, c ~ : (Vec 4 Float) a)
       => HList b
         -> RasterContext (HList c) d
           -> Primitive (HList c) d -> FragmentStream 1 (HList a)
 rasterizePrimitives
-  :: forall (a :: List Type) (b :: PrimitiveType)
+  :: forall (a :: [Type]) (b :: PrimitiveType)
     . RasterContext (HList (: (Vec 4 Float) a)) b
       -> HList (map Type Type Interpolated a)
-        -> List (Primitive (HList (: (Vec 4 Float) a)) b)
-          -> List (Vector 1 (Maybe (SimpleFragment (HList a))))
+        -> [Primitive (HList (: (Vec 4 Float) a)) b]
+          -> [Vector 1 (Maybe (SimpleFragment (HList a)))]
 'ImageLC :: Type -> Nat
-allSame :: forall a . List a -> Type
-sameLayerCounts :: List Type -> Type
-'FrameBuffer :: Nat -> List ImageKind -> Type
+allSame :: forall a . [a] -> Type
+sameLayerCounts :: [Type] -> Type
+'FrameBuffer :: Nat -> [ImageKind] -> Type
 'FrameBufferCase
-  :: forall (a :: Nat) (b :: List ImageKind)
+  :: forall (a :: Nat) (b :: [ImageKind])
     . forall (c :: FrameBuffer a b -> Type) (d :: FrameBuffer a b) -> c d
 match'FrameBuffer
   :: forall (a :: Type -> Type)
-    -> (forall (b :: Nat) (c :: List ImageKind) -> a (FrameBuffer b c))
+    -> (forall (b :: Nat) (c :: [ImageKind]) -> a (FrameBuffer b c))
       -> forall d -> a d -> a d
-imageType' :: List ImageKind -> List Type
+imageType' :: [ImageKind] -> [Type]
 'FragmentOperationKind :: Type -> ImageKind
 Accumulate
-  :: forall (a :: List ImageKind) (b :: Nat) (c :: List Type)
+  :: forall (a :: [ImageKind]) (b :: Nat) (c :: [Type])
     . (a ~ map Type ImageKind FragmentOperationKind c)
       => HList c
         -> FragmentStream b (HList (imageType' a)) -> FrameBuffer b a -> FrameBuffer b a
 accumulateWith :: forall a b . a -> b -> (a, b)
 overlay
-  :: forall (a :: Nat) (b :: List Type)
+  :: forall (a :: Nat) (b :: [Type])
     . FrameBuffer a (map Type ImageKind FragmentOperationKind b)
-      -> (HList b, List
-            (Fragment a (HList (imageType' (map Type ImageKind FragmentOperationKind b)))))
+      -> (HList b, [Fragment
+            a
+            (HList (imageType' (map Type ImageKind FragmentOperationKind b)))])
         -> FrameBuffer a (map Type ImageKind FragmentOperationKind b)
 'GetImageKind :: Type -> ImageKind
 FrameBuffer
-  :: forall (a :: List Type)
+  :: forall (a :: [Type])
     . sameLayerCounts a
       => HList a
         -> FrameBuffer (ImageLC (head Type a)) (map Type ImageKind GetImageKind a)
 imageFrame
-  :: forall (a :: List Type)
+  :: forall (a :: [Type])
     . sameLayerCounts a
       => HList a
         -> FrameBuffer (ImageLC (head Type a)) (map Type ImageKind GetImageKind a)
 accumulate
-  :: forall (a :: Nat) (b :: List Type) c
+  :: forall (a :: Nat) (b :: [Type]) c
     . HList b
       -> (c -> HList (imageType' (map Type ImageKind FragmentOperationKind b)))
-        -> List (Vector a (Maybe (SimpleFragment c)))
+        -> [Vector a (Maybe (SimpleFragment c))]
           -> FrameBuffer a (map Type ImageKind FragmentOperationKind b)
             -> FrameBuffer a (map Type ImageKind FragmentOperationKind b)
-PrjImage :: forall (a :: ImageKind) . FrameBuffer 1 (: a 'Nil) -> Image 1 a
+PrjImage :: forall (a :: ImageKind) . FrameBuffer 1 (: a '[]) -> Image 1 a
 PrjImageColor
-  :: FrameBuffer 1 (: 'Depth (: ('Color (Vec 4 Float)) 'Nil))
+  :: FrameBuffer 1 (: 'Depth (: ('Color (Vec 4 Float)) '[]))
     -> Image 1 ('Color (Vec 4 Float))
 'Output :: Type
-ScreenOut :: forall (a :: Nat) (b :: List ImageKind) . FrameBuffer a b -> Output
+ScreenOut :: forall (a :: Nat) (b :: [ImageKind]) . FrameBuffer a b -> Output
 'OutputCase
   :: forall (a :: Output -> Type)
-    -> (forall (b :: Nat) (c :: List ImageKind)
+    -> (forall (b :: Nat) (c :: [ImageKind])
         . forall (d :: FrameBuffer b c) -> a ('ScreenOut b c d))
       -> forall (e :: Output) -> a e
 match'Output :: forall (a :: Type -> Type) -> a Output -> forall b -> a b -> a b
-renderFrame
-  :: forall (a :: Nat) (b :: List ImageKind) . FrameBuffer a b -> Output
+renderFrame :: forall (a :: Nat) (b :: [ImageKind]) . FrameBuffer a b -> Output
 'Texture :: Type
 Texture2DSlot :: String -> Texture
 Texture2D :: Vec 2 Int -> Image 1 ('Color (Vec 4 Float)) -> Texture
@@ -3628,9 +3628,9 @@ testdata/Builtins.lc 145:66-145:72
 testdata/Builtins.lc 145:67-145:68
     Type
 testdata/Builtins.lc 145:67-145:71
-    List Type
+    [Type]
 testdata/Builtins.lc 145:70-145:71
-    Type | List Type
+    Type | [Type]
 testdata/Builtins.lc 146:1-146:10
     forall a b (c :: Nat) . (Num a, b ~ VecScalar c a) => b -> b -> b -> b
 testdata/Builtins.lc 146:34-146:80
@@ -4761,35 +4761,35 @@ testdata/Builtins.lc 187:59-187:60
 testdata/Builtins.lc 187:61-187:66
     Type
 testdata/Builtins.lc 201:1-201:5
-    forall a . List a -> a
+    forall a . [a] -> a
 testdata/Builtins.lc 201:15-201:16
     _d
 testdata/Builtins.lc 203:6-203:8
-    forall a . List a -> List a -> List a
+    forall a . [a] -> [a] -> [a]
 testdata/Builtins.lc 203:14-203:16
     _d
 testdata/Builtins.lc 203:14-204:26
-    List _a -> List _a
+    [_a] -> [_a]
 testdata/Builtins.lc 204:14-204:15
     _d
 testdata/Builtins.lc 204:14-204:17
-    List _c -> List _c
+    [_c] -> [_c]
 testdata/Builtins.lc 204:14-204:26
-    List _c
+    [_c]
 testdata/Builtins.lc 204:16-204:17
-    forall a . a -> List a -> List a
+    forall a . a -> [a] -> [a]
 testdata/Builtins.lc 204:18-204:20
-    List _f
+    [_f]
 testdata/Builtins.lc 204:21-204:23
     _h
 testdata/Builtins.lc 204:24-204:26
-    List _g
+    [_g]
 testdata/Builtins.lc 206:1-206:6
-    forall a b . (b -> a -> a) -> a -> List b -> a
+    forall a b . (b -> a -> a) -> a -> [b] -> a
 testdata/Builtins.lc 206:16-206:17
     _f
 testdata/Builtins.lc 206:16-207:39
-    List _b -> _f
+    [_b] -> _f
 testdata/Builtins.lc 207:21-207:22
     _i
 testdata/Builtins.lc 207:23-207:24
@@ -4801,41 +4801,41 @@ testdata/Builtins.lc 207:32-207:33
 testdata/Builtins.lc 207:34-207:35
     _o
 testdata/Builtins.lc 207:36-207:38
-    List _k
+    [_k]
 testdata/Builtins.lc 209:1-209:7
-    forall a . List (List a) -> List a
+    forall a . [[a]] -> [a]
 testdata/Builtins.lc 209:10-209:15
-    forall a b . (b -> a -> a) -> a -> List b -> a
+    forall a b . (b -> a -> a) -> a -> [b] -> a
 testdata/Builtins.lc 209:10-209:20
-    List _a -> List (List _a) -> List _a
+    [_a] -> [[_a]] -> [_a]
 testdata/Builtins.lc 209:10-209:23
-    List (List _a) -> List _a
+    [[_a]] -> [_a]
 testdata/Builtins.lc 209:16-209:20
-    forall a . List a -> List a -> List a
+    forall a . [a] -> [a] -> [a]
 testdata/Builtins.lc 209:21-209:23
-    forall a . List a
+    forall a . [a]
 testdata/Builtins.lc 211:1-211:4
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 211:16-211:18
-    forall a . List a
+    forall a . [a]
 testdata/Builtins.lc 211:16-212:30
-    List _b -> List _a
+    [_b] -> [_a]
 testdata/Builtins.lc 212:16-212:17
     _i
 testdata/Builtins.lc 212:16-212:21
-    List _a -> List _a
+    [_a] -> [_a]
 testdata/Builtins.lc 212:16-212:30
-    List _c
+    [_c]
 testdata/Builtins.lc 212:18-212:19
     _h
 testdata/Builtins.lc 212:20-212:21
-    forall a . a -> List a -> List a
+    forall a . a -> [a] -> [a]
 testdata/Builtins.lc 212:22-212:25
     _i
 testdata/Builtins.lc 212:26-212:27
     _g -> _f
 testdata/Builtins.lc 212:28-212:30
-    List _h
+    [_h]
 testdata/Builtins.lc 214:14-214:38
     Type | Type
 testdata/Builtins.lc 214:15-214:16
@@ -4855,27 +4855,27 @@ testdata/Builtins.lc 214:35-214:38
 testdata/Builtins.lc 214:36-214:37
     Type
 testdata/Builtins.lc 215:1-215:10
-    forall a b . (a -> List b) -> List a -> List b
+    forall a b . (a -> [b]) -> [a] -> [b]
 testdata/Builtins.lc 215:17-215:23
-    forall a . List (List a) -> List a
+    forall a . [[a]] -> [a]
 testdata/Builtins.lc 215:17-215:33
-    List _c
+    [_c]
 testdata/Builtins.lc 215:25-215:28
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 215:25-215:30
-    List _e -> List (List _d)
+    [_e] -> [[_d]]
 testdata/Builtins.lc 215:25-215:32
-    List (List _c)
+    [[_c]]
 testdata/Builtins.lc 215:29-215:30
-    _g -> List _f
+    _g -> [_f]
 testdata/Builtins.lc 215:31-215:32
-    List _d
+    [_d]
 testdata/Builtins.lc 217:1-217:4
-    forall a . List a -> Int
+    forall a . [a] -> Int
 testdata/Builtins.lc 217:10-217:11
     _b
 testdata/Builtins.lc 217:10-218:35
-    List _b -> Int
+    [_b] -> Int
 testdata/Builtins.lc 218:14-218:15
     _b
 testdata/Builtins.lc 218:14-218:28
@@ -4887,7 +4887,7 @@ testdata/Builtins.lc 218:16-218:28
 testdata/Builtins.lc 218:29-218:32
     _h
 testdata/Builtins.lc 218:33-218:35
-    List _g
+    [_g]
 testdata/Builtins.lc 222:6-222:11
     Type -> Type | Type -> Type | Type -> Type | Type -> Type | Type -> Type | Type
 testdata/Builtins.lc 222:6-222:13
@@ -5073,12 +5073,11 @@ testdata/Builtins.lc 252:69-252:70
 testdata/Builtins.lc 252:71-252:72
     Type
 testdata/Builtins.lc 253:1-253:14
-    forall a b (c :: PrimitiveType)
-      . (a -> b) -> List (Primitive a c) -> List (Primitive b c)
+    forall a b (c :: PrimitiveType) . (a -> b) -> [Primitive a c] -> [Primitive b c]
 testdata/Builtins.lc 253:19-253:22
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 253:19-253:39
-    List (Primitive _e _a) -> List (Primitive _d _a)
+    [Primitive _e _a] -> [Primitive _d _a]
 testdata/Builtins.lc 253:24-253:36
     forall a b (c :: PrimitiveType) . (a -> b) -> Primitive a c -> Primitive b c
 testdata/Builtins.lc 253:24-253:38
@@ -5090,7 +5089,7 @@ testdata/Builtins.lc 255:30-255:38
 testdata/Builtins.lc 255:45-255:46
     Type
 testdata/Builtins.lc 260:1-260:12
-    forall (a :: PrimitiveType) (b :: List Type) (c :: List Type)
+    forall (a :: PrimitiveType) (b :: [Type]) (c :: [Type])
       . (b ~ map Type Type ListElem c) => HList c -> PrimitiveStream a (HList b)
 testdata/Builtins.lc 260:32-260:119
     Type | Type | Type
@@ -5103,23 +5102,23 @@ testdata/Builtins.lc 260:56-260:75
 testdata/Builtins.lc 260:58-260:59
     forall a . a -> a -> Type
 testdata/Builtins.lc 260:60-260:63
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 260:60-260:72
-    List Type -> List Type
+    [Type] -> [Type]
 testdata/Builtins.lc 260:60-260:75
-    List Type
+    [Type]
 testdata/Builtins.lc 260:64-260:72
     Type -> Type
 testdata/Builtins.lc 260:73-260:75
     _b
 testdata/Builtins.lc 260:80-260:85
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 260:80-260:88
     Type
 testdata/Builtins.lc 260:80-260:119
     Type
 testdata/Builtins.lc 260:86-260:88
-    List Type
+    [Type]
 testdata/Builtins.lc 260:92-260:107
     PrimitiveType -> Type -> Type
 testdata/Builtins.lc 260:92-260:109
@@ -5129,20 +5128,20 @@ testdata/Builtins.lc 260:92-260:119
 testdata/Builtins.lc 260:108-260:109
     _f
 testdata/Builtins.lc 260:111-260:116
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 260:111-260:118
     Type
 testdata/Builtins.lc 260:117-260:118
-    List Type
+    [Type]
 testdata/Builtins.lc 262:1-262:6
-    forall (a :: PrimitiveType) (b :: List Type)
+    forall (a :: PrimitiveType) (b :: [Type])
       . String -> HList b -> PrimitiveStream a (HList b)
 testdata/Builtins.lc 262:56-262:62
     Type
 testdata/Builtins.lc 262:56-262:104
     Type | Type
 testdata/Builtins.lc 262:66-262:71
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 262:66-262:73
     Type
 testdata/Builtins.lc 262:66-262:104
@@ -5158,11 +5157,11 @@ testdata/Builtins.lc 262:77-262:104
 testdata/Builtins.lc 262:93-262:94
     _e
 testdata/Builtins.lc 262:96-262:101
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 262:96-262:103
     Type
 testdata/Builtins.lc 262:102-262:103
-    List Type
+    [Type]
 testdata/Builtins.lc 264:1-264:10
     forall a . String -> a
 testdata/Builtins.lc 264:14-264:20
@@ -5172,9 +5171,9 @@ testdata/Builtins.lc 264:14-264:25
 testdata/Builtins.lc 264:24-264:25
     _c | Type
 testdata/Builtins.lc 266:1-266:12
-    forall (a :: PrimitiveType) (b :: List Type)
+    forall (a :: PrimitiveType) (b :: [Type])
       . String
-        -> forall (c :: List String)
+        -> forall (c :: [String])
           -> (len String c ~ len Type b) => PrimitiveStream a (HList b)
 testdata/Builtins.lc 266:31-266:37
     Type
@@ -5193,7 +5192,7 @@ testdata/Builtins.lc 266:65-266:73
 testdata/Builtins.lc 266:66-266:72
     Type
 testdata/Builtins.lc 266:78-266:81
-    forall a . List a -> Int
+    forall a . [a] -> Int
 testdata/Builtins.lc 266:78-266:84
     Int
 testdata/Builtins.lc 266:78-266:86
@@ -5203,15 +5202,15 @@ testdata/Builtins.lc 266:78-266:92
 testdata/Builtins.lc 266:78-266:123
     Type
 testdata/Builtins.lc 266:82-266:84
-    List String
+    [String]
 testdata/Builtins.lc 266:85-266:86
     forall a . a -> a -> Type
 testdata/Builtins.lc 266:87-266:90
-    forall a . List a -> Int
+    forall a . [a] -> Int
 testdata/Builtins.lc 266:87-266:92
     Int
 testdata/Builtins.lc 266:91-266:92
-    List Type
+    [Type]
 testdata/Builtins.lc 266:96-266:111
     PrimitiveType -> Type -> Type
 testdata/Builtins.lc 266:96-266:113
@@ -5221,11 +5220,11 @@ testdata/Builtins.lc 266:96-266:123
 testdata/Builtins.lc 266:112-266:113
     _f
 testdata/Builtins.lc 266:115-266:120
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 266:115-266:122
     Type
 testdata/Builtins.lc 266:121-266:122
-    List Type
+    [Type]
 testdata/Builtins.lc 270:6-270:14
     Nat -> Type -> Type
 testdata/Builtins.lc 270:21-270:27
@@ -5350,13 +5349,13 @@ testdata/Builtins.lc 281:75-281:76
 testdata/Builtins.lc 282:1-282:16
     forall a (b :: Nat)
       . (a -> Float)
-        -> List (Vector b (Maybe (SimpleFragment a)))
-          -> List (Vector b (Maybe (SimpleFragment a)))
+        -> [Vector b (Maybe (SimpleFragment a))]
+          -> [Vector b (Maybe (SimpleFragment a))]
 testdata/Builtins.lc 282:21-282:24
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 282:21-282:43
-    List (Vector _a (Maybe (SimpleFragment _d)))
-      -> List (Vector _a (Maybe (SimpleFragment _d)))
+    [Vector _a (Maybe (SimpleFragment _d))]
+      -> [Vector _a (Maybe (SimpleFragment _d))]
 testdata/Builtins.lc 282:26-282:40
     forall a (b :: Nat) . (a -> Float) -> Fragment b a -> Fragment b a
 testdata/Builtins.lc 282:26-282:42
@@ -5424,13 +5423,13 @@ testdata/Builtins.lc 286:74-286:75
 testdata/Builtins.lc 287:1-287:16
     forall a (b :: Nat)
       . (a -> Bool)
-        -> List (Vector b (Maybe (SimpleFragment a)))
-          -> List (Vector b (Maybe (SimpleFragment a)))
+        -> [Vector b (Maybe (SimpleFragment a))]
+          -> [Vector b (Maybe (SimpleFragment a))]
 testdata/Builtins.lc 287:21-287:24
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 287:21-287:43
-    List (Vector _a (Maybe (SimpleFragment _d)))
-      -> List (Vector _a (Maybe (SimpleFragment _d)))
+    [Vector _a (Maybe (SimpleFragment _d))]
+      -> [Vector _a (Maybe (SimpleFragment _d))]
 testdata/Builtins.lc 287:26-287:40
     forall a (b :: Nat) . (a -> Bool) -> Fragment b a -> Fragment b a
 testdata/Builtins.lc 287:26-287:42
@@ -5498,13 +5497,13 @@ testdata/Builtins.lc 291:68-291:69
 testdata/Builtins.lc 292:1-292:13
     forall a b (c :: Nat)
       . (a -> b)
-        -> List (Vector c (Maybe (SimpleFragment a)))
-          -> List (Vector c (Maybe (SimpleFragment b)))
+        -> [Vector c (Maybe (SimpleFragment a))]
+          -> [Vector c (Maybe (SimpleFragment b))]
 testdata/Builtins.lc 292:18-292:21
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 292:18-292:37
-    List (Vector _a (Maybe (SimpleFragment _e)))
-      -> List (Vector _a (Maybe (SimpleFragment _d)))
+    [Vector _a (Maybe (SimpleFragment _e))]
+      -> [Vector _a (Maybe (SimpleFragment _d))]
 testdata/Builtins.lc 292:23-292:34
     forall a b (c :: Nat) . (a -> b) -> Fragment c a -> Fragment c b
 testdata/Builtins.lc 292:23-292:36
@@ -6208,9 +6207,9 @@ testdata/Builtins.lc 463:26-463:56
 testdata/Builtins.lc 463:27-463:40
     Type
 testdata/Builtins.lc 463:27-463:55
-    List Type
+    [Type]
 testdata/Builtins.lc 463:42-463:55
-    Type | List Type
+    Type | [Type]
 testdata/Builtins.lc 464:29-464:97
     Type
 testdata/Builtins.lc 464:29-465:74
@@ -6218,21 +6217,21 @@ testdata/Builtins.lc 464:29-465:74
 testdata/Builtins.lc 464:30-464:62
     Type
 testdata/Builtins.lc 464:30-464:96
-    List Type
+    [Type]
 testdata/Builtins.lc 464:31-464:45
     Type
 testdata/Builtins.lc 464:31-464:61
-    List Type
+    [Type]
 testdata/Builtins.lc 464:47-464:61
-    Type | List Type
+    Type | [Type]
 testdata/Builtins.lc 464:64-464:96
-    Type | List Type
+    Type | [Type]
 testdata/Builtins.lc 464:65-464:79
     Type
 testdata/Builtins.lc 464:65-464:95
-    List Type
+    [Type]
 testdata/Builtins.lc 464:81-464:95
-    Type | List Type
+    Type | [Type]
 testdata/Builtins.lc 465:29-465:32
     Nat -> Type -> Type
 testdata/Builtins.lc 465:29-465:34
@@ -6388,7 +6387,7 @@ testdata/Builtins.lc 478:42-478:56
 testdata/Builtins.lc 478:55-478:56
     Type
 testdata/Builtins.lc 480:1-480:19
-    forall (a :: List Type) (b :: List Type) (c :: List Type) (d :: PrimitiveType)
+    forall (a :: [Type]) (b :: [Type]) (c :: [Type]) (d :: PrimitiveType)
       . (map Type Type Interpolated a ~ b, c ~ : (Vec 4 Float) a)
         => HList b
           -> RasterContext (HList c) d
@@ -6396,13 +6395,13 @@ testdata/Builtins.lc 480:1-480:19
 testdata/Builtins.lc 481:8-486:34
     Type | Type | Type | Type
 testdata/Builtins.lc 481:10-481:13
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 481:10-481:26
-    List Type -> List Type
+    [Type] -> [Type]
 testdata/Builtins.lc 481:10-481:28
-    List Type
+    [Type]
 testdata/Builtins.lc 481:10-481:30
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 481:10-481:44
     Type
 testdata/Builtins.lc 481:14-481:26
@@ -6430,25 +6429,25 @@ testdata/Builtins.lc 482:14-482:19
 testdata/Builtins.lc 482:14-482:25
     Type
 testdata/Builtins.lc 482:14-482:26
-    List Type -> List Type
+    [Type] -> [Type]
 testdata/Builtins.lc 482:14-482:28
-    List Type
+    [Type]
 testdata/Builtins.lc 482:18-482:19
     _b
 testdata/Builtins.lc 482:20-482:25
     Type
 testdata/Builtins.lc 482:25-482:26
-    forall a . a -> List a -> List a
+    forall a . a -> [a] -> [a]
 testdata/Builtins.lc 482:27-482:28
-    List Type
+    [Type]
 testdata/Builtins.lc 483:8-483:13
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 483:8-483:27
     Type
 testdata/Builtins.lc 483:8-486:34
     Type
 testdata/Builtins.lc 483:14-483:27
-    List Type
+    [Type]
 testdata/Builtins.lc 484:8-484:21
     Type -> PrimitiveType -> Type
 testdata/Builtins.lc 484:8-484:31
@@ -6458,11 +6457,11 @@ testdata/Builtins.lc 484:8-484:33
 testdata/Builtins.lc 484:8-486:34
     Type
 testdata/Builtins.lc 484:23-484:28
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 484:23-484:30
     Type
 testdata/Builtins.lc 484:29-484:30
-    List Type
+    [Type]
 testdata/Builtins.lc 484:32-484:33
     _e
 testdata/Builtins.lc 485:8-485:17
@@ -6474,11 +6473,11 @@ testdata/Builtins.lc 485:8-485:29
 testdata/Builtins.lc 485:8-486:34
     Type
 testdata/Builtins.lc 485:19-485:24
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 485:19-485:26
     Type
 testdata/Builtins.lc 485:25-485:26
-    List Type
+    [Type]
 testdata/Builtins.lc 485:28-485:29
     PrimitiveType
 testdata/Builtins.lc 486:8-486:22
@@ -6490,30 +6489,29 @@ testdata/Builtins.lc 486:8-486:34
 testdata/Builtins.lc 486:23-486:24
     _b
 testdata/Builtins.lc 486:26-486:31
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 486:26-486:33
     Type
 testdata/Builtins.lc 486:32-486:33
-    List Type
+    [Type]
 testdata/Builtins.lc 488:1-488:20
-    forall (a :: List Type) (b :: PrimitiveType)
+    forall (a :: [Type]) (b :: PrimitiveType)
       . RasterContext (HList (: (Vec 4 Float) a)) b
         -> HList (map Type Type Interpolated a)
-          -> List (Primitive (HList (: (Vec 4 Float) a)) b)
-            -> List (Vector 1 (Maybe (SimpleFragment (HList a))))
+          -> [Primitive (HList (: (Vec 4 Float) a)) b]
+            -> [Vector 1 (Maybe (SimpleFragment (HList a)))]
 testdata/Builtins.lc 488:32-488:38
-    forall a . List (List a) -> List a
+    forall a . [[a]] -> [a]
 testdata/Builtins.lc 488:32-488:74
-    List (Vector 1 (Maybe (SimpleFragment (HList _b))))
+    [Vector 1 (Maybe (SimpleFragment (HList _b)))]
 testdata/Builtins.lc 488:40-488:43
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 488:40-488:71
-    List (Primitive (HList (: (Vec 4 Float) _b)) _a)
-      -> List (List (Fragment 1 (HList _b)))
+    [Primitive (HList (: (Vec 4 Float) _b)) _a] -> [[Fragment 1 (HList _b)]]
 testdata/Builtins.lc 488:40-488:73
-    List (List (Fragment 1 (HList _b)))
+    [[Fragment 1 (HList _b)]]
 testdata/Builtins.lc 488:45-488:63
-    forall (a :: List Type) (b :: List Type) (c :: List Type) (d :: PrimitiveType)
+    forall (a :: [Type]) (b :: [Type]) (c :: [Type]) (d :: PrimitiveType)
       . (map Type Type Interpolated a ~ b, c ~ : (Vec 4 Float) a)
         => HList b
           -> RasterContext (HList c) d
@@ -6540,21 +6538,21 @@ testdata/Builtins.lc 492:12-492:15
 testdata/Builtins.lc 492:12-492:23
     Type
 testdata/Builtins.lc 492:12-495:50
-    forall a . List a -> Type
+    forall a . [a] -> Type
 testdata/Builtins.lc 492:13-492:14
     _b
 testdata/Builtins.lc 492:19-492:23
     Type | Type
 testdata/Builtins.lc 493:1-493:8
-    forall a . List a -> Type
+    forall a . [a] -> Type
 testdata/Builtins.lc 493:14-493:19
     Type
 testdata/Builtins.lc 493:14-495:50
-    List _a -> Type | Type
+    [_a] -> Type | Type
 testdata/Builtins.lc 494:15-494:20
     Type
 testdata/Builtins.lc 494:15-495:50
-    List _c -> Type | Type
+    [_c] -> Type | Type
 testdata/Builtins.lc 495:22-495:25
     Type -> Type -> Type
 testdata/Builtins.lc 495:22-495:33
@@ -6572,38 +6570,38 @@ testdata/Builtins.lc 495:29-495:30
 testdata/Builtins.lc 495:31-495:32
     _c
 testdata/Builtins.lc 495:35-495:42
-    forall a . List a -> Type
+    forall a . [a] -> Type
 testdata/Builtins.lc 495:35-495:49
     Type
 testdata/Builtins.lc 495:44-495:45
     _g
 testdata/Builtins.lc 495:44-495:46
-    List _f -> List _f
+    [_f] -> [_f]
 testdata/Builtins.lc 495:44-495:48
-    List _e
+    [_e]
 testdata/Builtins.lc 495:45-495:46
-    forall a . a -> List a -> List a
+    forall a . a -> [a] -> [a]
 testdata/Builtins.lc 495:46-495:48
-    List _e
+    [_e]
 testdata/Builtins.lc 497:1-497:16
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 497:21-497:28
-    forall a . List a -> Type
+    forall a . [a] -> Type
 testdata/Builtins.lc 497:21-497:45
     Type
 testdata/Builtins.lc 497:30-497:33
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 497:30-497:42
-    List Type -> List Nat
+    [Type] -> [Nat]
 testdata/Builtins.lc 497:30-497:44
-    List Nat
+    [Nat]
 testdata/Builtins.lc 497:34-497:42
     Type -> Nat
 testdata/Builtins.lc 497:43-497:44
     _b
 testdata/Builtins.lc 509:6-509:17
-    Nat -> List ImageKind -> Type | Nat -> List ImageKind -> Type | Nat
-      -> List ImageKind -> Type | Type | Type
+    Nat -> [ImageKind] -> Type | Nat -> [ImageKind] -> Type | Nat
+      -> [ImageKind] -> Type | Type | Type
 testdata/Builtins.lc 509:6-509:46
     Type
 testdata/Builtins.lc 509:24-509:27
@@ -6621,31 +6619,30 @@ testdata/Builtins.lc 511:30-511:36
 testdata/Builtins.lc 511:31-511:35
     Type
 testdata/Builtins.lc 512:1-512:11
-    List ImageKind -> List Type
+    [ImageKind] -> [Type]
 testdata/Builtins.lc 512:25-512:28
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 512:25-512:38
-    List ImageKind -> List Type
+    [ImageKind] -> [Type]
 testdata/Builtins.lc 512:25-512:40
-    List Type
+    [Type]
 testdata/Builtins.lc 512:25-513:31
-    List Type -> ImageKind -> List Type | List Type | List Type
+    [Type] -> ImageKind -> [Type] | [Type] | [Type]
 testdata/Builtins.lc 512:29-512:38
     ImageKind -> Type
 testdata/Builtins.lc 512:39-512:40
-    List _c
+    [_c]
 testdata/Builtins.lc 513:16-513:19
-    forall a b . (a -> b) -> List a -> List b | forall a b
-      . (a -> b) -> List a -> List b | forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b] | forall a b
+      . (a -> b) -> [a] -> [b] | forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 513:16-513:29
-    List ImageKind -> List Type | List ImageKind -> List Type | List ImageKind
-      -> List Type
+    [ImageKind] -> [Type] | [ImageKind] -> [Type] | [ImageKind] -> [Type]
 testdata/Builtins.lc 513:16-513:31
-    List Type | List Type | List Type
+    [Type] | [Type] | [Type]
 testdata/Builtins.lc 513:20-513:29
     ImageKind -> Type | ImageKind -> Type | ImageKind -> Type
 testdata/Builtins.lc 513:30-513:31
-    List ImageKind | List ImageKind | List ImageKind
+    [ImageKind] | [ImageKind] | [ImageKind]
 testdata/Builtins.lc 515:40-515:49
     Type | Type
 testdata/Builtins.lc 515:56-515:77
@@ -6653,7 +6650,7 @@ testdata/Builtins.lc 515:56-515:77
 testdata/Builtins.lc 515:102-515:103
     ImageKind
 testdata/Builtins.lc 517:1-517:11
-    forall (a :: List ImageKind) (b :: Nat) (c :: List Type)
+    forall (a :: [ImageKind]) (b :: Nat) (c :: [Type])
       . (a ~ map Type ImageKind FragmentOperationKind c)
         => HList c
           -> FragmentStream b (HList (imageType' a)) -> FrameBuffer b a -> FrameBuffer b a
@@ -6678,23 +6675,23 @@ testdata/Builtins.lc 517:50-517:81
 testdata/Builtins.lc 517:52-517:53
     forall a . a -> a -> Type
 testdata/Builtins.lc 517:54-517:57
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 517:54-517:79
-    List Type -> List ImageKind
+    [Type] -> [ImageKind]
 testdata/Builtins.lc 517:54-517:81
-    List ImageKind
+    [ImageKind]
 testdata/Builtins.lc 517:58-517:79
     Type -> ImageKind
 testdata/Builtins.lc 517:80-517:81
-    List Type
+    [Type]
 testdata/Builtins.lc 517:86-517:91
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 517:86-517:93
     Type
 testdata/Builtins.lc 517:86-517:174
     Type
 testdata/Builtins.lc 517:92-517:93
-    List Type
+    [Type]
 testdata/Builtins.lc 517:97-517:111
     Nat -> Type -> Type
 testdata/Builtins.lc 517:97-517:113
@@ -6706,19 +6703,19 @@ testdata/Builtins.lc 517:97-517:174
 testdata/Builtins.lc 517:112-517:113
     Nat
 testdata/Builtins.lc 517:115-517:120
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 517:115-517:135
     Type
 testdata/Builtins.lc 517:122-517:132
-    List ImageKind -> List Type
+    [ImageKind] -> [Type]
 testdata/Builtins.lc 517:122-517:134
-    List Type
+    [Type]
 testdata/Builtins.lc 517:133-517:134
-    List ImageKind
+    [ImageKind]
 testdata/Builtins.lc 517:140-517:151
-    Nat -> List ImageKind -> Type
+    Nat -> [ImageKind] -> Type
 testdata/Builtins.lc 517:140-517:153
-    List ImageKind -> Type
+    [ImageKind] -> Type
 testdata/Builtins.lc 517:140-517:155
     Type
 testdata/Builtins.lc 517:140-517:174
@@ -6726,17 +6723,17 @@ testdata/Builtins.lc 517:140-517:174
 testdata/Builtins.lc 517:152-517:153
     Nat
 testdata/Builtins.lc 517:154-517:155
-    List ImageKind
+    [ImageKind]
 testdata/Builtins.lc 517:159-517:170
-    Nat -> List ImageKind -> Type
+    Nat -> [ImageKind] -> Type
 testdata/Builtins.lc 517:159-517:172
-    List ImageKind -> Type
+    [ImageKind] -> Type
 testdata/Builtins.lc 517:159-517:174
     Type | Type
 testdata/Builtins.lc 517:171-517:172
     Nat
 testdata/Builtins.lc 517:173-517:174
-    List ImageKind
+    [ImageKind]
 testdata/Builtins.lc 519:1-519:15
     forall a b . a -> b -> (a, b)
 testdata/Builtins.lc 519:24-519:32
@@ -6746,13 +6743,14 @@ testdata/Builtins.lc 519:25-519:28
 testdata/Builtins.lc 519:30-519:31
     _e | ((_b))
 testdata/Builtins.lc 520:1-520:8
-    forall (a :: Nat) (b :: List Type)
+    forall (a :: Nat) (b :: [Type])
       . FrameBuffer a (map Type ImageKind FragmentOperationKind b)
-        -> (HList b, List
-              (Fragment a (HList (imageType' (map Type ImageKind FragmentOperationKind b)))))
+        -> (HList b, [Fragment
+              a
+              (HList (imageType' (map Type ImageKind FragmentOperationKind b)))])
           -> FrameBuffer a (map Type ImageKind FragmentOperationKind b)
 testdata/Builtins.lc 520:25-520:35
-    forall (a :: List ImageKind) (b :: Nat) (c :: List Type)
+    forall (a :: [ImageKind]) (b :: Nat) (c :: [Type])
       . (a ~ map Type ImageKind FragmentOperationKind c)
         => HList c
           -> FragmentStream b (HList (imageType' a)) -> FrameBuffer b a -> FrameBuffer b a
@@ -6784,7 +6782,7 @@ testdata/Builtins.lc 524:47-524:59
 testdata/Builtins.lc 524:74-524:75
     ImageKind
 testdata/Builtins.lc 530:1-530:12
-    forall (a :: List Type)
+    forall (a :: [Type])
       . sameLayerCounts a
         => HList a
           -> FrameBuffer (ImageLC (head Type a)) (map Type ImageKind GetImageKind a)
@@ -6795,23 +6793,23 @@ testdata/Builtins.lc 530:31-530:35
 testdata/Builtins.lc 530:40-530:125
     Type
 testdata/Builtins.lc 530:41-530:56
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 530:41-530:58
     Type
 testdata/Builtins.lc 530:57-530:58
-    List Type
+    [Type]
 testdata/Builtins.lc 530:63-530:68
-    List Type -> Type
+    [Type] -> Type
 testdata/Builtins.lc 530:63-530:70
     Type
 testdata/Builtins.lc 530:63-530:125
     Type
 testdata/Builtins.lc 530:69-530:70
-    List Type
+    [Type]
 testdata/Builtins.lc 530:74-530:85
-    Nat -> List ImageKind -> Type
+    Nat -> [ImageKind] -> Type
 testdata/Builtins.lc 530:74-530:104
-    List ImageKind -> Type
+    [ImageKind] -> Type
 testdata/Builtins.lc 530:74-530:125
     Type | Type
 testdata/Builtins.lc 530:87-530:94
@@ -6819,40 +6817,40 @@ testdata/Builtins.lc 530:87-530:94
 testdata/Builtins.lc 530:87-530:103
     Nat
 testdata/Builtins.lc 530:96-530:100
-    forall a . List a -> a
+    forall a . [a] -> a
 testdata/Builtins.lc 530:96-530:102
     Type
 testdata/Builtins.lc 530:101-530:102
-    List Type
+    [Type]
 testdata/Builtins.lc 530:106-530:109
-    forall a b . (a -> b) -> List a -> List b
+    forall a b . (a -> b) -> [a] -> [b]
 testdata/Builtins.lc 530:106-530:122
-    List Type -> List ImageKind
+    [Type] -> [ImageKind]
 testdata/Builtins.lc 530:106-530:124
-    List ImageKind
+    [ImageKind]
 testdata/Builtins.lc 530:110-530:122
     Type -> ImageKind
 testdata/Builtins.lc 530:123-530:124
-    List Type
+    [Type]
 testdata/Builtins.lc 532:1-532:11
-    forall (a :: List Type)
+    forall (a :: [Type])
       . sameLayerCounts a
         => HList a
           -> FrameBuffer (ImageLC (head Type a)) (map Type ImageKind GetImageKind a)
 testdata/Builtins.lc 532:14-532:25
-    forall (a :: List Type)
+    forall (a :: [Type])
       . sameLayerCounts a
         => HList a
           -> FrameBuffer (ImageLC (head Type a)) (map Type ImageKind GetImageKind a)
 testdata/Builtins.lc 534:1-534:11
-    forall (a :: Nat) (b :: List Type) c
+    forall (a :: Nat) (b :: [Type]) c
       . HList b
         -> (c -> HList (imageType' (map Type ImageKind FragmentOperationKind b)))
-          -> List (Vector a (Maybe (SimpleFragment c)))
+          -> [Vector a (Maybe (SimpleFragment c))]
             -> FrameBuffer a (map Type ImageKind FragmentOperationKind b)
               -> FrameBuffer a (map Type ImageKind FragmentOperationKind b)
 testdata/Builtins.lc 534:34-534:44
-    forall (a :: List ImageKind) (b :: Nat) (c :: List Type)
+    forall (a :: [ImageKind]) (b :: Nat) (c :: [Type])
       . (a ~ map Type ImageKind FragmentOperationKind c)
         => HList c
           -> FragmentStream b (HList (imageType' a)) -> FrameBuffer b a -> FrameBuffer b a
@@ -6872,18 +6870,17 @@ testdata/Builtins.lc 534:45-534:48
 testdata/Builtins.lc 534:50-534:62
     forall a b (c :: Nat)
       . (a -> b)
-        -> List (Vector c (Maybe (SimpleFragment a)))
-          -> List (Vector c (Maybe (SimpleFragment b)))
+        -> [Vector c (Maybe (SimpleFragment a))]
+          -> [Vector c (Maybe (SimpleFragment b))]
 testdata/Builtins.lc 534:50-534:70
-    List (Vector _a (Maybe (SimpleFragment _c)))
-      -> List (Vector _a (Maybe (SimpleFragment _b)))
+    [Vector _a (Maybe (SimpleFragment _c))]
+      -> [Vector _a (Maybe (SimpleFragment _b))]
 testdata/Builtins.lc 534:50-534:75
-    List
-      (Vector
-        _c
-        (Maybe
-          (SimpleFragment
-            (HList (imageType' (map Type ImageKind FragmentOperationKind _b))))))
+    [Vector
+      _c
+      (Maybe
+        (SimpleFragment
+          (HList (imageType' (map Type ImageKind FragmentOperationKind _b)))))]
 testdata/Builtins.lc 534:63-534:70
     _k
 testdata/Builtins.lc 534:71-534:75
@@ -6891,11 +6888,11 @@ testdata/Builtins.lc 534:71-534:75
 testdata/Builtins.lc 534:77-534:79
     _e
 testdata/Builtins.lc 537:1-537:9
-    forall (a :: ImageKind) . FrameBuffer 1 (: a 'Nil) -> Image 1 a
+    forall (a :: ImageKind) . FrameBuffer 1 (: a '[]) -> Image 1 a
 testdata/Builtins.lc 537:24-537:35
-    Nat -> List ImageKind -> Type
+    Nat -> [ImageKind] -> Type
 testdata/Builtins.lc 537:24-537:37
-    List ImageKind -> Type
+    [ImageKind] -> Type
 testdata/Builtins.lc 537:24-537:42
     Type
 testdata/Builtins.lc 537:24-537:55
@@ -6903,7 +6900,7 @@ testdata/Builtins.lc 537:24-537:55
 testdata/Builtins.lc 537:36-537:37
     _b
 testdata/Builtins.lc 537:38-537:42
-    List ImageKind
+    [ImageKind]
 testdata/Builtins.lc 537:40-537:41
     _c
 testdata/Builtins.lc 537:46-537:51
@@ -6917,24 +6914,24 @@ testdata/Builtins.lc 537:52-537:53
 testdata/Builtins.lc 537:54-537:55
     ImageKind
 testdata/Builtins.lc 538:1-538:14
-    FrameBuffer 1 (: 'Depth (: ('Color (Vec 4 Float)) 'Nil))
+    FrameBuffer 1 (: 'Depth (: ('Color (Vec 4 Float)) '[]))
       -> Image 1 ('Color (Vec 4 Float))
 testdata/Builtins.lc 538:24-538:35
-    Nat -> List ImageKind -> Type
+    Nat -> [ImageKind] -> Type
 testdata/Builtins.lc 538:24-538:37
-    List ImageKind -> Type
+    [ImageKind] -> Type
 testdata/Builtins.lc 538:24-538:70
     Type
 testdata/Builtins.lc 538:36-538:37
     _b
 testdata/Builtins.lc 538:38-538:70
-    List ImageKind
+    [ImageKind]
 testdata/Builtins.lc 538:41-538:47
     ImageKind
 testdata/Builtins.lc 538:49-538:55
     Type -> ImageKind
 testdata/Builtins.lc 538:49-538:69
-    ImageKind | List ImageKind
+    ImageKind | [ImageKind]
 testdata/Builtins.lc 538:57-538:60
     Nat -> Type -> Type
 testdata/Builtins.lc 538:57-538:62
@@ -6972,12 +6969,12 @@ testdata/Builtins.lc 540:6-540:12
 testdata/Builtins.lc 540:6-541:12
     Type
 testdata/Builtins.lc 541:3-541:12
-    forall (a :: Nat) (b :: List ImageKind)
+    forall (a :: Nat) (b :: [ImageKind])
       . FrameBuffer a b -> Output | Output | Type | Type | Type | Type
 testdata/Builtins.lc 541:26-541:37
-    Nat -> List ImageKind -> Type
+    Nat -> [ImageKind] -> Type
 testdata/Builtins.lc 541:26-541:39
-    List ImageKind -> Type
+    [ImageKind] -> Type
 testdata/Builtins.lc 541:26-541:41
     Type
 testdata/Builtins.lc 541:26-541:51
@@ -6989,9 +6986,9 @@ testdata/Builtins.lc 541:40-541:41
 testdata/Builtins.lc 541:45-541:51
     Type | Type
 testdata/Builtins.lc 543:1-543:12
-    forall (a :: Nat) (b :: List ImageKind) . FrameBuffer a b -> Output
+    forall (a :: Nat) (b :: [ImageKind]) . FrameBuffer a b -> Output
 testdata/Builtins.lc 543:15-543:24
-    forall (a :: Nat) (b :: List ImageKind) . FrameBuffer a b -> Output
+    forall (a :: Nat) (b :: [ImageKind]) . FrameBuffer a b -> Output
 testdata/Builtins.lc 549:6-549:13
     Type | Type | Type | Type
 testdata/Builtins.lc 549:6-553:12