diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,5 +1,5 @@
 name:                language-ats
-version:             0.1.1.10
+version:             0.1.1.11
 synopsis:            Parser and pretty-printer for ATS.
 description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex.
 license:             BSD3
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
@@ -250,7 +250,7 @@
      | openParen Type vbar Type closeParen { ProofType $1 $2 $4 }
      | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }
      | openParen TypeIn closeParen { Tuple $1 $2 }
-     | openParen Type closeParen { $2 }
+     | openParen Type closeParen { ParenType $1 $2 }
      | int StaticExpression { DependentInt $2 }
      | doubleParens { NoneType $1 }
      | minus {% Left $ Expected $1 "Type" "-" }
@@ -438,6 +438,7 @@
               | let ATS in Expression fun {% Left $ Expected $5 "end" "fun" }
               | let ATS in Expression vtypedef {% Left $ Expected $5 "end" "vtypedef" }
               | let ATS in Expression implement {% Left $ Expected $5 "end" "implement" }
+              | let ATS in Expression semicolon {% Left $ Expected $5 "end" ";" }
               | if Expression then Expression else else {% Left $ Expected $6 "Expression" "else" }
 
 -- | Parse a termetric
@@ -662,6 +663,7 @@
          | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 }
          | AndSort { $1 }
          | vtypedef IdentifierOr eq vbar {% Left $ Expected $3 "Type" "|" }
+         | datavtype IdentifierOr openParen Args closeParen vbar {% Left $ Expected $6 "=" "|" }
 
 Fixity : infixr { RightFix $1 }
        | infixl { LeftFix $1 }
@@ -745,6 +747,7 @@
 
 instance Pretty (ATSError String) where
     pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (string s2) <> ", expected:" <+> squotes (string s1)) <> linebreak
+    pretty (Unknown (Special l ")")) = red "Error:" <+> "unmatched ')' at" <+> pretty l <> linebreak 
     pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak
 
 parseError :: [Token] -> Either (ATSError String) a
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
@@ -195,7 +195,7 @@
         a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es
         a BinListF{} = undefined
         a CallF{} = undefined
-        prettyImplicits = mconcat . fmap (prettyArgsU "<" ">")
+        prettyImplicits = mconcat . fmap (prettyArgsU "<" ">") . reverse
         prettyIfCase []              = mempty
         prettyIfCase [(s, l, t)]     = "|" <+> s <+> pretty l <+> t
         prettyIfCase ((s, l, t): xs) = prettyIfCase xs $$ "|" <+> s <+> pretty l <+> t
@@ -277,9 +277,7 @@
         a DoubleF                 = "double"
         a FloatF                  = "float"
         a (ForAF u t)             = pretty u <+> t
-        a (UnconsumedF t)
-            | hasFunction "<> " t = "!" <> parens t
-            | otherwise = "!" <> t
+        a (UnconsumedF t)         = "!" <> t
         a (AsProofF t (Just t'))  = t <+> ">>" <+> t'
         a (AsProofF t Nothing)    = t <+> ">> _"
         a (FromVTF t)             = t <> "?!"
@@ -293,19 +291,12 @@
         a (TupleF _ ts)           = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
         a (RefTypeF t)            = "&" <> t
         a (ViewTypeF _ t)         = "view@" <> parens t
-        a (FunctionTypeF s t t')
-            | startsAnd t = parens t <+> string s <+> t'
-            | otherwise = t <+> string s <+> t'
+        a (FunctionTypeF s t t')  = t <+> string s <+> t'
         a (ViewLiteralF c)        = "view" <> pretty c
         a NoneTypeF{}             = "()"
         a ImplicitTypeF{}         = ".."
         a (AnonymousRecordF _ rs) = prettyRecord rs
-
-hasFunction :: String -> Doc -> Bool
-hasFunction is = (\x -> all (`elem` x) is) . showFast
-
-startsAnd :: Doc -> Bool
-startsAnd = (=='&') . head . showFast
+        a (ParenTypeF _ t)        = parens t
 
 gan :: Maybe Type -> Doc
 gan (Just t) = " : " <> pretty t <> " "
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
@@ -153,6 +153,7 @@
           | ImplicitType AlexPosn
           | ViewLiteral Addendum
           | AnonymousRecord AlexPosn [(String, Type)]
+          | ParenType AlexPosn Type
           deriving (Show, Eq, Generic, NFData)
 
 -- | A type for the various lambda arrows (@=>@, @=\<cloref1>@, etc.)
diff --git a/test/data/polyglot.out b/test/data/polyglot.out
--- a/test/data/polyglot.out
+++ b/test/data/polyglot.out
@@ -1451,7 +1451,7 @@
 
 fnx get_cli { n : int | n >= 1 }{ m : nat | m < n } .<n-m>.
 ( argc : int(n)
-, argv : !argv(n)
+, argv : !(argv(n))
 , current : int(m)
 , prev_is_exclude : bool
 , acc : command_line