diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # language-ats 
 
+## 1.7.0.3
+
+  * Bump `recursion` version bounds
+
 ## 1.7.0.2
 
 Bug fixes:
diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.18
 name: language-ats
-version: 1.7.0.2
+version: 1.7.0.3
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale
@@ -54,7 +54,7 @@
     build-depends:
         base >=4.9 && <5,
         array -any,
-        recursion -any,
+        recursion >=1.0.0.0,
         microlens -any,
         deepseq -any,
         ansi-wl-pprint >=0.6.8,
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -454,14 +454,15 @@
                  | doubleParens { StaticVoid $1 } -- TODO: static tuple?
                  | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 }
                  | identifierSpace { StaticVal (Unqualified $ to_string $1) }
-                 | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [$2] }
-                 | Name parens(StaticArgs) { SCall $1 [] $2 }
-                 | Name TypeArgs parens(StaticArgs) { SCall $1 $2 $3 }
-                 | Name TypeArgs doubleParens { SCall $1 $2 [] }
-                 | Name doubleParens { SCall $1 [] [] }
-                 | identifierSpace TypeArgs parens(StaticArgs) { SCall (Unqualified $ to_string $1) $2 $3 }
-                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 }
-                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] } -- TODO: this causes an ambiguity because we might have SCall void instead!
+                 | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [] [$2] }
+                 | Name parens(StaticArgs) { SCall $1 [] [] $2 }
+                 | Name Implicits parens(StaticArgs) { SCall $1 $2 [] $3 }
+                 | Name TypeArgs parens(StaticArgs) { SCall $1 [] $2 $3 }
+                 | Name TypeArgs doubleParens { SCall $1 [] $2 [] }
+                 | Name doubleParens { SCall $1 [] [] [] }
+                 | identifierSpace TypeArgs parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 $3 }
+                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] [] $2 }
+                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] [] } -- TODO: this causes an ambiguity because we might have SCall void instead!
                  | StaticExpression semicolon StaticExpression { SPrecede $1 $3 }
                  | UnOp StaticExpression { SUnary $1 $2 }
                  | let StaticDecls comment_after(in) end { SLet $1 (reverse $2) Nothing }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -127,7 +127,6 @@
 
 instance Eq a => Pretty (Expression a) where
     pretty = cata a where
-        a :: Eq a => ExpressionF a Doc -> Doc
         a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
         a (IfF e e' Nothing)            = "if" <+> e <+> "then" <$> indent 2 e'
         a (LetF _ e e')          = flatAlt
@@ -217,7 +216,6 @@
 
 instance Eq a => Pretty (Pattern a) where
     pretty = cata a where
-        a :: Eq a => PatternF a Doc -> Doc
         a (PSumF s x)                  = string s <+> x
         a (PLiteralF e)                = pretty e
         a (PNameF s [])                = pretty s
@@ -271,21 +269,26 @@
 
 instance Eq a => Pretty (StaticExpression a) where
     pretty = cata a where
-        a :: Eq a => StaticExpressionF a Doc -> Doc
         a (StaticValF n)            = pretty n
         a (StaticBinaryF op se se')
             | squish op = se <> pretty op <> se'
             | otherwise = se <+> pretty op <+> se'
-        a (StaticIntF i)            = pretty i
-        a (StaticHexF h)            = text h
-        a StaticVoidF{}             = "()"
-        a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
-        a (SCallF n [] ["()"])      = pretty n <> "()"
-        a (SCallF n us ["()"])      = pretty n <> prettyTypes us <> "()"
-        a (SCallF n [] cs)          = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))
-        a (SCallF n us cs)          = pretty n <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs))
-        a (SPrecedeF e e')          = e <> ";" <+> e'
-        a (SUnaryF op e)            = pretty op <> e
+        a (StaticIntF i)               = pretty i
+        a (StaticHexF h)               = text h
+        a StaticVoidF{}                = "()"
+        a (SifF e e' e'')              = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
+        a (SCallF n [] [] ["()"])      = pretty n <> "()"
+        a (SCallF n [] us ["()"])      = pretty n <> prettyTypes us <> "()"
+        a (SCallF n [] [] cs)          = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))
+        a (SCallF n [] us cs)          = pretty n <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs))
+        a (SCallF n is [] ["()"])      = pretty n <> prettyImplicits is <> "()"
+        a (SCallF n is us ["()"])      = pretty n <> prettyImplicits is <> prettyTypes us <> "()"
+        a (SCallF n is [] cs)          = pretty n <> prettyImplicits is <> parens (mconcat (punctuate "," . fmap pretty $ cs))
+        a (SCallF n is us cs)          = pretty n <> prettyImplicits is <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs))
+        a (SPrecedeF e e')             = e <> ";" <+> e'
+        a (SPrecedeListF es)           = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")
+        a (SParensF e)                 = parens e
+        a (SUnaryF op e)               = pretty op <> e
         a (SLetF _ e e') = flatAlt
             ("let" <$> indent 2 (concatSame e) <$> endLet e')
             ("let" <+> concatSame e <$> endLet e')
@@ -298,7 +301,6 @@
 
 instance Eq a => Pretty (Sort a) where
     pretty = cata a where
-        a :: Eq a => SortF a Doc -> Doc
         a (T0pF ad)           = "t@ype" <> pretty ad
         a (Vt0pF ad)          = "vt@ype" <> pretty ad
         a (NamedSortF s)      = text s
@@ -310,7 +312,6 @@
 
 instance Eq a => Pretty (Type a) where
     pretty = cata a where
-        a :: Eq a => TypeF a Doc -> Doc
         a (NamedF n)                       = pretty n
         a (ViewTypeF _ t)                  = "view@" <> parens t
         a (ExF e (Just t))
diff --git a/src/Language/ATS/Rewrite.hs b/src/Language/ATS/Rewrite.hs
--- a/src/Language/ATS/Rewrite.hs
+++ b/src/Language/ATS/Rewrite.hs
@@ -87,11 +87,13 @@
 
 rewriteStaATS :: Eq a => FixityState a -> StaticExpression a -> StaticExpression a
 rewriteStaATS st = cata a where
-    a (SCallF n ts [StaticVoid{}]) = SCall n ts []
+    a (SCallF n is ts [StaticVoid{}]) = SCall n is ts []
     a (StaticBinaryF op (StaticBinary op' e e') e'')
         | compareFixity st op op'  = StaticBinary op e (StaticBinary op' e' e'')
     a (WhereStaExpF se (ATS ds))   = WhereStaExp se (ATS (rewriteDecl st <$> ds))
-    a x                            = embed x
+    a (SPrecedeF e e'@SPrecedeList{})                 = SPrecedeList (e : _sExprs e')
+    a (SPrecedeF e e')                                = SPrecedeList [e, e']
+    a x                                               = embed x
 
 -- | Among other things, this rewrites expressions so that operator precedence
 -- is respected; this ensures @1 + 2 * 3@ will be parsed as the correct
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -1,5 +1,4 @@
 {-# OPTIONS_GHC -fno-warn-duplicate-exports #-}
-
 {-# LANGUAGE DeriveAnyClass             #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveGeneric              #-}
@@ -8,6 +7,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE PatternSynonyms            #-}
+{-# LANGUAGE TypeFamilies               #-}
 
 -- | This is a module containing types to model the ATS syntax tree. As it is
 -- collapsed by the pretty printer, you may see that in some places it is
@@ -182,9 +182,9 @@
                | AddrTypeF a
                deriving (Functor)
 
-instance Base (Type a) (TypeF b)
+type instance Base (Type a) = TypeF a
 
-instance Recursive (TypeF a) (Type a) where
+instance Recursive (Type a) where
     project (Tuple x tys)              = TupleF x tys
     project (BoxTuple x tys)           = BoxTupleF x tys
     project (Named n)                  = NamedF n
@@ -254,9 +254,9 @@
                   | BinPatternF a (BinOp a) x x
                   deriving (Functor)
 
-instance Base (Pattern a) (PatternF b)
+type instance Base (Pattern a) = PatternF a
 
-instance Recursive (PatternF a) (Pattern a) where
+instance Recursive (Pattern a) where
     project (PName x ps)                = PNameF x ps
     project (PSum x p)                  = PSumF x p
     project (PLiteral e)                = PLiteralF e
@@ -306,9 +306,9 @@
                | ArrowSortF a x x
                deriving (Functor)
 
-instance Base (Sort a) (SortF b)
+type instance Base (Sort a) = SortF a
 
-instance Recursive (SortF a) (Sort a) where
+instance Recursive (Sort a) where
     project (NamedSort s)      = NamedSortF s
     project (T0p a)            = T0pF a
     project (Vt0p a)           = Vt0pF a
@@ -361,9 +361,10 @@
                         | StaticInt Int
                         | StaticHex String
                         | SPrecede (StaticExpression a) (StaticExpression a)
+                        | SPrecedeList { _sExprs :: [StaticExpression a] }
                         | StaticVoid a
                         | Sif { scond :: StaticExpression a, whenTrue :: StaticExpression a, selseExpr :: StaticExpression a } -- Static if (for proofs)
-                        | SCall (Name a) [[Type a]] [StaticExpression a]
+                        | SCall (Name a) [[Type a]] [[Type a]] [StaticExpression a]
                         | SUnary (UnOp a) (StaticExpression a)
                         | SLet a [Declaration a] (Maybe (StaticExpression a))
                         | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)]
@@ -372,6 +373,7 @@
                         | ProofLambda a (LambdaType a) (Pattern a) (StaticExpression a)
                         | ProofLinearLambda a (LambdaType a) (Pattern a) (StaticExpression a)
                         | WhereStaExp (StaticExpression a) (ATS a)
+                        | SParens (StaticExpression a)
                         deriving (Show, Eq, Generic, NFData)
 
 data StaticExpressionF a x = StaticValF (Name a)
@@ -379,9 +381,10 @@
                            | StaticIntF Int
                            | StaticHexF String
                            | SPrecedeF x x
+                           | SPrecedeListF [x]
                            | StaticVoidF a
                            | SifF x x x
-                           | SCallF (Name a) [[Type a]] [x]
+                           | SCallF (Name a) [[Type a]] [[Type a]] [x]
                            | SUnaryF (UnOp a) x
                            | SLetF a [Declaration a] (Maybe x)
                            | SCaseF Addendum x [(Pattern a, LambdaType a, x)]
@@ -390,19 +393,21 @@
                            | ProofLambdaF a (LambdaType a) (Pattern a) x
                            | ProofLinearLambdaF a (LambdaType a) (Pattern a) x
                            | WhereStaExpF x (ATS a)
+                           | SParensF x
                            deriving (Functor)
 
-instance Base (StaticExpression a) (StaticExpressionF b)
+type instance Base (StaticExpression a) = StaticExpressionF a
 
-instance Recursive (StaticExpressionF a) (StaticExpression a) where
+instance Recursive (StaticExpression a) where
     project (StaticVal n)               = StaticValF n
     project (StaticBinary b x x')       = StaticBinaryF b x x'
     project (StaticHex h)               = StaticHexF h
     project (StaticInt i)               = StaticIntF i
     project (SPrecede x x')             = SPrecedeF x x'
+    project (SPrecedeList xs)           = SPrecedeListF xs
     project (StaticVoid x)              = StaticVoidF x
     project (Sif e e' e'')              = SifF e e' e''
-    project (SCall n ts es)             = SCallF n ts es
+    project (SCall n is ts es)          = SCallF n is ts es
     project (SUnary u x)                = SUnaryF u x
     project (SLet x ds e)               = SLetF x ds e
     project (SCase a x ples)            = SCaseF a x ples
@@ -411,16 +416,18 @@
     project (ProofLambda a l p e)       = ProofLambdaF a l p e
     project (ProofLinearLambda a l p e) = ProofLinearLambdaF a l p e
     project (WhereStaExp e ds)          = WhereStaExpF e ds
+    project (SParens e)                 = SParensF e
 
-instance Corecursive (StaticExpressionF a) (StaticExpression a) where
+instance Corecursive (StaticExpression a) where
     embed (StaticValF n)               = StaticVal n
     embed (StaticBinaryF b e e')       = StaticBinary b e e'
     embed (StaticHexF h)               = StaticHex h
     embed (StaticIntF i)               = StaticInt i
     embed (SPrecedeF e e')             = SPrecede e e'
+    embed (SPrecedeListF es)           = SPrecedeList es
     embed (StaticVoidF l)              = StaticVoid l
     embed (SifF e e' e'')              = Sif e e' e''
-    embed (SCallF n ts es)             = SCall n ts es
+    embed (SCallF n is ts es)          = SCall n is ts es
     embed (SUnaryF u e)                = SUnary u e
     embed (SLetF l ds e)               = SLet l ds e
     embed (SCaseF a x ples)            = SCase a x ples
@@ -429,6 +436,7 @@
     embed (ProofLambdaF a l p e)       = ProofLambda a l p e
     embed (ProofLinearLambdaF a l p e) = ProofLinearLambda a l p e
     embed (WhereStaExpF e ds)          = WhereStaExp e ds
+    embed (SParensF e)                 = SParens e
 
 -- | A (possibly effectful) expression.
 data Expression a = Let a (ATS a) (Maybe (Expression a))
@@ -539,9 +547,9 @@
                      | MacroVarF a String
                      deriving (Functor)
 
-instance Base (Expression a) (ExpressionF b)
+type instance Base (Expression a) = (ExpressionF a)
 
-instance Recursive (ExpressionF a) (Expression a) where
+instance Recursive (Expression a) where
     project (Let l ds me)                 = LetF l ds me
     project (VoidLiteral l)               = VoidLiteralF l
     project (Call n is us mps as)         = CallF n is us mps as
@@ -588,7 +596,7 @@
     project (CommentExpr s e)             = CommentExprF s e
     project (MacroVar l s)                = MacroVarF l s
 
-instance Corecursive (ExpressionF a) (Expression a) where
+instance Corecursive (Expression a) where
     embed (LetF l ds me)                 = Let l ds me
     embed (VoidLiteralF l)               = VoidLiteral l
     embed (CallF n is us mps as)         = Call n is us mps as