diff --git a/bench/Bench.hs b/bench/Bench.hs
--- a/bench/Bench.hs
+++ b/bench/Bench.hs
@@ -7,14 +7,14 @@
 main =
     defaultMain [ env envFiles $ \ ~(l, m) ->
                   bgroup "format"
-                      [ bench "lexATS (large)" $ nf lex l
+                      [ bench "lexATS (large)" $ nf lexATS l
                       , bench "parseATS . lexATS (large)" $ nf parse l
                       , bench "printATS . parseATS . lexATS (large)" $ nf (fmap printATS . parse) l
-                      , bench "lexATS (medium)" $ nf lex m
+                      , bench "lexATS (medium)" $ nf lexATS m
                       , bench "parseATS . lexATS (medium)" $ nf parse m
                       , bench "printATS . parseATS . lexATS (medium)" $ nf (fmap printATS . parse) m
                       ]
                 ]
     where large = readFile "test/data/polyglot.dats"
-          medium = readFile "test/data/stdlib/checkast.sats"
+          medium = readFile "test/data/concurrency.dats"
           envFiles = (,) <$> large <*> medium
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.3.0.1
+version:             0.3.0.2
 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.hs b/src/Language/ATS.hs
--- a/src/Language/ATS.hs
+++ b/src/Language/ATS.hs
@@ -1,10 +1,11 @@
 -- | Main module for the library
 module Language.ATS ( -- * Functions for working with syntax
-                      lex
+                      lexATS
                     , parse
                     , printATS
                     , printATSCustom
                     , printATSFast
+                    , printErr
                     -- * Library functions
                     , getDependencies
                     -- * Syntax Tree
@@ -46,20 +47,28 @@
                     , typeCallArgs
                     ) where
 
-import           Data.Maybe               (catMaybes)
+import           Control.Lens
+import           Control.Monad
+import           Control.Monad.IO.Class
+import           Data.Maybe                   (catMaybes)
+import           GHC.IO.Handle.FD             (stderr)
 import           Language.ATS.Lexer
 import           Language.ATS.Parser
 import           Language.ATS.PrettyPrint
 import           Language.ATS.Types
+import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 rewriteATS' :: ATS -> ATS
 rewriteATS' (ATS ds) = ATS (rewriteDecl <$> ds)
 
+printErr :: MonadIO m => ATSError String -> m ()
+printErr = liftIO . hPutDoc stderr . pretty
+
 -- | Parse a string containing ATS source.
 parse :: String -> Either (ATSError String) ATS
-parse = fmap rewriteATS' . parseATS . lexATS
+parse = fmap rewriteATS' . (parseATS <=< (over _Left LexError . lexATS))
 
--- TODO use Language.C.Parser here?
+-- TODO use prepocessing?? here?
 getDependencies :: ATS -> [FilePath]
 getDependencies (ATS ds) = catMaybes (g <$> ds)
     where g (Staload _ _ s) = Just s
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
--- a/src/Language/ATS/Lexer.x
+++ b/src/Language/ATS/Lexer.x
@@ -100,25 +100,25 @@
 
 @builtin = \$ (("effmask_" (wrt | all | ref)) | "extfcall" | "ldelay" | "delay" | "list_vt" | "tempenver" | "extype" | "mylocation" | "showtype")
 
-@block_comment_start = \(\* | \*\/
+@block_comment_start = \(\* | \/\*
 @block_comment_end = \*\) | \*\/
 
-@comment_in = [\*\)\(\/$white]
+@comment_in = [\*$white]
+@comment_general = @comment_in | [\)\(\/]
 
 tokens :-
 
     <0> $white+                  ;
-    -- <0> @block_comment_start     { begin one }
-    -- <one> @block_comment_end     { begin 0 }
-    -- <one> @block_comment_start   { begin two }
-    -- <one> [^\*\)\/]+             ;
-    -- <one> @comment_in+ / [^\)]   ;
-    -- <one> @comment_in            ;
-    -- <two> @block_comment_end     { begin one }
-    -- <two> [^\*\)\/]+             ;
-    -- <two> @comment_in+ / [^\)]   ;
-    -- <two> @comment_in            ;
-    @block_comment               { tok (\p s -> alex $ CommentLex p s) }
+    <0> @block_comment_start     { tok (\p s -> alex $ CommentBegin p) `andBegin` one }
+    <one> @block_comment_end     { tok (\p s -> alex $ CommentEnd p) `andBegin` 0 }
+    <one> @block_comment_start   { tok (\p s -> alex $ CommentContents p s) `andBegin` two }
+    <one> [^\*\(\)\/]+           { tok (\p s -> alex $ CommentContents p s) }
+    <one> @comment_in+ / [^\)]   { tok (\p s -> alex $ CommentContents p s) }
+    <one> @comment_general       { tok (\p s -> alex $ CommentContents p s) }
+    <two> @block_comment_end     { tok (\p s -> alex $ CommentContents p s) `andBegin` one }
+    <two> [^\*\(\)\/]+           { tok (\p s -> alex $ CommentContents p s) }
+    <two> @comment_in+ / [^\)]   { tok (\p s -> alex $ CommentContents p s) }
+    <two> @comment_general       { tok (\p s -> alex $ CommentContents p s) }
     <0> "//".*                   { tok (\p s -> alex $ CommentLex p s) }
     <0> "#define".*              { tok (\p s -> alex $ MacroBlock p s) }      
     <0> @if_block                { tok (\p s -> alex $ MacroBlock p s) }      
@@ -213,6 +213,7 @@
     <0> sta                      { tok (\p s -> alex $ Keyword p KwSta) }
     <0> symintr                  { tok (\p s -> alex $ Keyword p KwSymintr) }
     <0> absview                  { tok (\p s -> alex $ Keyword p KwAbsview) }
+    <0> exception                { tok (\p s -> alex $ Keyword p KwException) }
     <0> "$list"                  { tok (\p s -> alex $ Keyword p (KwListLit "")) }
     <0> "$list_vt"               { tok (\p s -> alex $ Keyword p (KwListLit "_vt")) }
     <0> "fold@"                  { tok (\p s -> alex $ IdentifierSpace p s) }
@@ -337,6 +338,7 @@
              | KwListLit String
              | KwMacdef
              | KwDatasort
+             | KwException
              deriving (Eq, Show, Generic, NFData)
 
 data Token = Identifier AlexPosn String
@@ -353,6 +355,9 @@
            | Arrow AlexPosn String
            | FuncType AlexPosn String
            | CommentLex AlexPosn String
+           | CommentBegin AlexPosn
+           | CommentEnd AlexPosn
+           | CommentContents AlexPosn String
            | MacroBlock AlexPosn String
            | TimeTok AlexPosn String
            | SignatureTok AlexPosn String
@@ -391,6 +396,7 @@
     pretty (KwCase c) = "case" <> pretty c
     pretty KwIfCase = "ifcase"
     pretty KwIf = "if"
+    pretty KwException = "exception"
     pretty KwSif = "sif"
     pretty KwThen = "then"
     pretty KwElse = "else"
@@ -458,6 +464,9 @@
     pretty CBlockLex{} = "%{"
     pretty (Arrow _ s) = text s
     pretty (CommentLex _ s) = text $ take 2 s
+    pretty CommentBegin{} = "(*"
+    pretty CommentEnd{} = "*)"
+    pretty (CommentContents _ s) = text s
     pretty (FuncType _ s) = text s
     pretty (TimeTok _ s) = text s
     pretty (SignatureTok _ s) = ":" <> text s
@@ -475,6 +484,7 @@
 to_string (IdentifierSpace _ s) = s
 to_string (SpecialIdentifier _ s) = s
 to_string (Operator _ s) = s
+to_string (CommentContents _ s) = s
 to_string _ = undefined
 
 token_posn (SpecialIdentifier p _) = p
@@ -499,6 +509,9 @@
 token_posn (DoubleBracketTok p) = p
 token_posn (SpecialBracket p) = p
 token_posn (FixityTok p _) = p
+token_posn (CommentContents p _) = p
+token_posn (CommentBegin p) = p
+token_posn (CommentEnd p) = p
 token_posn End = undefined
 
 toChar :: String -> Char
@@ -511,8 +524,8 @@
 alexEOF = pure End
 
 -- | This function turns a string into a stream of tokens for the parser.
-lexATS :: String -> [Token]
-lexATS str = either error id . runAlex str $ loop
+lexATS :: String -> Either String [Token]
+lexATS str = runAlex str $ loop
 
 loop :: Alex [Token]
 loop = do
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
@@ -6,7 +6,7 @@
 
     -- | This module contains the parser.
     module Language.ATS.Parser ( parseATS
-                               , ATSError
+                               , ATSError (..)
                                ) where
 
 import Language.ATS.Types
@@ -71,9 +71,11 @@
     case { Keyword _ (KwCase $$) }
     ifcase { Keyword $$ KwIfCase }
     datatype { Keyword $$ KwDatatype }
+    dataview { Keyword $$ KwDataview }
     datavtype { Keyword $$ KwDatavtype }
     while { Keyword $$ KwWhile }
     of { Keyword $$ KwOf }
+    exception { Keyword $$ KwException }
     include { Keyword $$ KwInclude }
     staload { $$@(Keyword _ (KwStaload _)) }
     overload { Keyword $$ KwOverload }
@@ -177,6 +179,9 @@
     prefix { FixityTok $$ "prefix" }
     postfix { FixityTok $$ "postfix" }
     customOperator { $$@Operator{} }
+    beginComment { CommentBegin $$ }
+    endComment { CommentEnd $$ }
+    commentContents { CommentContents _ $$ }
 
 %%
 
@@ -215,7 +220,8 @@
      | Type prfTransform underscore { AsProof $1 Nothing }
      | view at Type { ViewType $1 $3 }
      | viewPlusMinus { ViewLiteral $1 }
-     | Existential Type { Ex $1 $2 }
+     | Existential Type { Ex $1 (Just $2) }
+     | Existential { Ex $1 Nothing }
      | Universal Type { ForA $1 $2 }
      | Type at StaticExpression { AtExpr $2 $1 $3 }
      | at Type { AtType $1 $2 }
@@ -239,6 +245,7 @@
      | Arg vbar Arg { [ PrfArg $1 $3 ] }
      | lineComment { [] }
      | Args lineComment { $1 }
+     | Args Comment { $1 }
      | { [] }
 
 TypeArg : identifier { Arg (First $ to_string $1) }
@@ -394,7 +401,6 @@
               | viewAt PreExpression { ViewAt $1 $2 }
               | atbrace RecordVal rbrace { RecordValue $1 $2 Nothing }
               | atbrace RecordVal rbrace colon Type { RecordValue $1 $2 (Just $5) }
-              | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }
               | begin Expression end { Begin $1 $2 }
               | identifierSpace { NamedVal (Unqualified $ to_string $1) }
               | Name { NamedVal $1 }
@@ -402,6 +408,7 @@
               | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }
               | lineComment PreExpression { CommentExpr (to_string $1) $2 }
               | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }
+              | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }
               | include {% Left $ Expected $1 "Expression" "include" }
               | staload {% Left $ Expected (token_posn $1) "Expression" "staload" }
               | overload {% Left $ Expected $1 "Expression" "overload" }
@@ -417,6 +424,7 @@
               | 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" ";" }
+              | let ATS if {% Left $ Expected $3 "in" "if" }
               | if Expression then Expression else else {% Left $ Expected $6 "Expression" "else" }
 
 -- | Parse a termetric
@@ -434,10 +442,11 @@
      | viewContra { View $1 Minus }
      | vtype { VType (token_posn $1) (get_addendum $1) }
      | IdentifierOr { NamedSort $1 }
+     | IdentifierOr plus { NamedSort ($1 <> "+") }
 
 QuantifierArgs : IdentifierOr { [$1] }
-               | { [] }
                | QuantifierArgs comma IdentifierOr { $3 : $1 }
+               | { [] }
 
 Existential : lsqbracket QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 False (Just $4) (Just $6) }
             | lsqbracket QuantifierArgs colon Sort rsqbracket { Existential $2 False (Just $4) Nothing }
@@ -507,17 +516,20 @@
 OfType : { Nothing }
        | of Type { Just $2 }
 
+StaticExpressionsIn : StaticExpression { [$1] }
+                    | StaticExpressionsIn comma StaticExpression { $3 : $1 }
+
 -- | Parse a constructor for a sum type
 SumLeaf : vbar Universals identifier { Leaf $2 (to_string $3) [] Nothing }
         | vbar Universals identifierSpace of Type { Leaf $2 (to_string $3) [] (Just $5) }
-        | vbar Universals IdentifierOr openParen IdentifiersIn closeParen OfType { Leaf $2 $3 $5 $7 }
+        | vbar Universals IdentifierOr openParen StaticExpressionsIn closeParen OfType { Leaf $2 $3 $5 $7 } -- FIXME could also be e.g. '0' (static expression)
 
 -- | Parse all constructors of a sum type
 Leaves : SumLeaf { [$1] }
        | Leaves SumLeaf { $2 : $1 }
        | Universals identifierSpace of Type { [Leaf $1 (to_string $2) [] (Just $4)] }
        | Universals identifier { [Leaf $1 (to_string $2) [] Nothing] }
-       | Universals identifier openParen IdentifiersIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.
+       | Universals identifier openParen StaticExpressionsIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.
        | dollar {% Left $ Expected $1 "|" "$" }
 
 Universals : { [] }
@@ -611,10 +623,9 @@
         | sortdef IdentifierOr eq Sort { SortDef $1 $2 (Left $4) }
         | sortdef IdentifierOr eq Universal { SortDef $1 $2 (Right $4) }
 
-AndStadef : stadef IdentifierOr eq Name { Stadef $2 $4 [] }
-          | stadef IdentifierOr eq identifierSpace { Stadef $2 (Unqualified $ to_string $4) [] }
-          | AndStadef and IdentifierOr eq identifierSpace { AndD $1 (Stadef $3 (Unqualified $ to_string $5) []) }
-          | AndStadef and IdentifierOr eq identifier { AndD $1 (Stadef $3 (Unqualified $ to_string $5) []) }
+-- Feb. 15th 2pm
+AndStadef : stadef IdentifierOr SortArgs eq Type { Stadef $2 $3 $5 }
+          | AndStadef and IdentifierOr SortArgs eq Type { AndD $1 (Stadef $3 $4 $6) }
 
 StafunDecl : prfun PreFunction { Func $1 (PrFun $2) }
            | prfn PreFunction { Func $1 (PrFn $2) }
@@ -657,6 +668,7 @@
         | SortArg comma Sort { Anonymous $3 : $1 }
         | IdentifierOr { [ Anonymous (NamedSort $1) ] }
         | Sort { [Anonymous $1] }
+        | SortArg Comment { $1 }
 
 SortArgs : openParen SortArg closeParen { Just $2 }
          | doubleParens { Just [] }
@@ -667,7 +679,10 @@
          | vtypedef IdentifierOr SortArgs eq Type { ViewTypeDef $1 $2 $3 $5 }
          | extern vtypedef string SortArgs eq Type { Extern $1 $ ViewTypeDef $2 $3 $4 $6 }
          | datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 }
+         | datatype lineComment IdentifierOr SortArgs eq Leaves { SumType $3 $4 $6 }
          | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 }
+         | datavtype lineComment IdentifierOr SortArgs eq Leaves { SumViewType $3 $4 $6 }
+         | dataview IdentifierOr SortArgs eq Leaves { DataView $1 $2 $3 $5 }
          | abst0p IdentifierOr SortArgs MaybeType { AbsT0p $1 $2 $3 $4 }
          | viewdef IdentifierOr SortArgs eq Type { ViewDef $1 $2 $3 $5 }
          | absvt0p IdentifierOr SortArgs eq Type { AbsVT0p $1 $2 $3 (Just $5) }
@@ -683,6 +698,8 @@
          | typedef IdentifierOr SortArgs eq vbar {% Left $ Expected $5 "Type" "|" }
          | datavtype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
          | datatype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
+         | dataview IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
+         | dataprop IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
 
 Fixity : infixr intLit { RightFix $1 $2 }
        | infixl intLit { LeftFix $1 $2 }
@@ -719,6 +736,11 @@
 DataSortLeaves : DataSortLeaf { [$1] }
                | DataSortLeaves DataSortLeaf { $2 : $1 }
 
+CommentContents : commentContents { Comment $1 }
+                | CommentContents commentContents { over comment (<> $2) $1 }
+
+Comment : beginComment CommentContents endComment { over comment ((<> "*)") . ("(*" <>)) $2 }
+
 -- | Parse a declaration
 Declaration : include string { Include $2 }
             | define { Define $1 }
@@ -730,6 +752,7 @@
             | macdef IdentifierOr doubleParens eq Expression { MacDecl $1 $2 [] $5 }
             | macdef IdentifierOr openParen IdentifiersIn closeParen eq Expression { MacDecl $1 $2 $4 $7 }
             | lineComment { Comment (to_string $1) }
+            | Comment { $1 }
             | staload underscore eq string { Staload (get_staload $1) (Just "_") $4 }
             | staload string { Staload (get_staload $1) Nothing $2 }
             | staload IdentifierOr eq string { Staload (get_staload $1) (Just $2) $4 }
@@ -760,6 +783,8 @@
             | symintr Name { SymIntr $1 $2 }
             | stacst IdentifierOr colon Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 }
             | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 }
+            | exception identifierSpace of doubleParens { Exception (to_string $2) (Tuple $4 mempty) }
+            | exception identifierSpace of openParen Type closeParen { Exception (to_string $2) (Tuple $4 [$5]) }
             | Fixity Operators { FixityDecl $1 $2 }
             | val Universals IdentifierOr colon Type { StaVal $2 $3 $5 }
             | lambda {% Left $ Expected $1 "Declaration" "lam" }
@@ -770,11 +795,13 @@
             | prfTransform {% Left $ Expected $1 "Declaration" ">>" }
             | maybeProof {% Left $ Expected $1 "Declaration" "?" }
             | identifier {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) }
+            | identifierSpace {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) }
 
 {
 
 data ATSError a = Expected AlexPosn a a
-                | Unknown Token -- FIXME error type for expression when a static expression was expected (?)
+                | Unknown Token
+                | LexError String
                 deriving (Eq, Show, Generic, NFData)
 
 instance Pretty AlexPosn where
@@ -784,6 +811,7 @@
     pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s2) <> ", expected:" <+> squotes (text 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
+    pretty (LexError s) = red "Lexical error:" <+> text s
 
 parseError :: [Token] -> Either (ATSError String) a
 parseError = Left . Unknown . head 
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
@@ -284,7 +284,8 @@
     pretty = cata a where
         a (NamedF n)              = pretty n
         a (ViewTypeF _ t)         = "view@" <> parens t
-        a (ExF e t)               = pretty e <+> t
+        a (ExF e (Just t))        = pretty e <+> t
+        a (ExF e Nothing)         = pretty e
         a (DependentF n ts)       = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
         a (ForAF u t)             = pretty u <+> t
         a (UnconsumedF t)         = "!" <> t
@@ -356,6 +357,7 @@
 glue x y
     | isVal x && isVal y = True
 glue Staload{} Staload{}           = True
+glue Define{} Define{} = True
 glue Include{} Include{}           = True
 glue ViewTypeDef{} ViewTypeDef{}   = True
 glue TypeDef{} TypeDef{}           = True
@@ -502,6 +504,7 @@
     pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgsNil as <+> ":" <> text si <#> pretty rt
     pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt
     pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si pus [] as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> prettyArgsNil as <+> ":" <> text si <#> pretty rt
     pretty (PreF i si pus us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt
 
 instance Pretty DataPropLeaf where
@@ -527,10 +530,12 @@
 prettySortArgs (Just as) = prettyArgs' ", " "(" ")" as
 
 instance Pretty Declaration where
+    pretty (Exception s t)                 = "exception" <+> text s <+> "of" <+> pretty t
     pretty (AbsType _ s as t)              = "abstype" <+> text s <> prettySortArgs as <> prettyMaybeType t
     pretty (AbsViewType _ s as Nothing)    = "absvtype" <+> text s <> prettySortArgs as
     pretty (AbsViewType _ s as (Just t))   = "absvtype" <+> text s <> prettySortArgs as <+> "=" <+> pretty t
     pretty (SumViewType s as ls)           = "datavtype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls
+    pretty (DataView _ s as ls)            = "dataview" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls
     pretty (SumType s as ls)               = "datatype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls
     pretty (DataSort _ s ls)               = "datasort" <+> text s <+> "=" <$> prettyDSL ls
     pretty (Impl as i)                     = "implement" <+> prettyArgsNil as <> pretty i -- mconcat (fmap pretty us) <+> pretty i
@@ -576,10 +581,8 @@
     pretty (Local _ d d')                  = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"
     pretty (FixityDecl f ss)               = pretty f <+> hsep (fmap text ss)
     pretty (StaVal us i t)                 = "val" </> mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t
-    pretty (Stadef i n [])                 = "stadef" <+> text i <+> pretty n
-    pretty (Stadef i n as)                 = "stadef" <+> text i <+> pretty n <> prettyArgs as
-    pretty (AndD d (Stadef i n []))        = pretty d <+> "and" <+> text i <+> pretty n
-    pretty (AndD d (Stadef i n as))        = pretty d <+> "and" <+> text i <+> pretty n <> prettyArgs as
+    pretty (Stadef i as t)                 = "stadef" <+> text i <+> prettySortArgs as <> pretty t
+    pretty (AndD d (Stadef i as t))        = pretty d <+> "and" <+> text i <+> prettySortArgs as <> pretty t
     pretty (AbsView _ i as t)              = "absview" <+> text i <> prettySortArgs as <> prettyMaybeType t
     pretty (AbsVT0p _ i as t)              = "absvt@ype" <+> text i <> prettySortArgs as <> prettyMaybeType t
     pretty (AbsT0p _ i as t)               = "abst@ype" <+> text i <> prettySortArgs as <> "=" <+> 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
@@ -53,6 +53,7 @@
     , constructorUniversals
     , typeCall
     , typeCallArgs
+    , comment
     ) where
 
 import           Control.Composition
@@ -79,7 +80,7 @@
     deriving (Show, Eq, Generic)
     deriving newtype (NFData, Semigroup, Monoid)
 
-data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [String], maybeType :: Maybe Type }
+data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [StaticExpression], maybeType :: Maybe Type }
     deriving (Show, Eq, Generic, NFData)
 
 type SortArgs = Maybe [SortArg]
@@ -95,7 +96,7 @@
                  | AndDecl (Maybe Type) Pattern Expression
                  | Include String
                  | Staload Bool (Maybe String) String
-                 | Stadef String Name [Type]
+                 | Stadef String SortArgs Type -- [Type] -- FIXME stadef array(a:vt@ype, n:int) = @[a][n]
                  | CBlock String
                  | TypeDef AlexPosn String SortArgs Type
                  | ViewTypeDef AlexPosn String SortArgs Type
@@ -109,8 +110,9 @@
                  | ViewDef AlexPosn String SortArgs Type
                  | OverloadOp AlexPosn BinOp Name (Maybe Int)
                  | OverloadIdent AlexPosn String Name (Maybe Int)
-                 | Comment String
+                 | Comment { _comment :: String }
                  | DataProp AlexPosn String SortArgs [DataPropLeaf]
+                 | DataView AlexPosn String SortArgs [Leaf]
                  | Extern AlexPosn Declaration
                  | Define String
                  | SortDef AlexPosn String (Either Sort Universal)
@@ -125,6 +127,7 @@
                  | FixityDecl Fixity [String]
                  | MacDecl AlexPosn String [String] Expression
                  | DataSort AlexPosn String [DataSortLeaf]
+                 | Exception String Type
                  deriving (Show, Eq, Generic, NFData)
 
 data DataSortLeaf = DataSortLeaf [Universal] Sort (Maybe Sort)
@@ -136,13 +139,13 @@
 -- | A type for parsed ATS types
 data Type = Tuple AlexPosn [Type]
           | Named Name
-          | Ex Existential Type
+          | Ex Existential (Maybe Type)
           | ForA Universal Type
           | Dependent { _typeCall :: Name, _typeCallArgs :: [Type] }
-          | Unconsumed Type -- !a
-          | AsProof Type (Maybe Type) -- a >> b
-          | FromVT Type -- For a viewtype VT, we can prove there exist a view V and type T such that `VT` is equivalent to `(V | T)` - that T is `VT?!`
-          | MaybeVal Type -- This is just `a?` or the like
+          | Unconsumed Type -- @!a@
+          | AsProof Type (Maybe Type) -- @a >> b@
+          | FromVT Type -- | @a?!@
+          | MaybeVal Type -- | @a?@
           | AtExpr AlexPosn Type StaticExpression
           | AtType AlexPosn Type
           | ProofType AlexPosn [Type] Type -- Aka (prf | val)
@@ -202,7 +205,7 @@
     deriving (Show, Eq, Generic, NFData)
 
 -- | A datatype for sorts.
-data Sort = NamedSort String
+data Sort = NamedSort { _sortName :: String }
           | T0p Addendum -- ^ t@ype
           | Vt0p Addendum -- ^ vt@ype
           | Addr
diff --git a/test/data/concurrency.out b/test/data/concurrency.out
--- a/test/data/concurrency.out
+++ b/test/data/concurrency.out
@@ -36,10 +36,10 @@
 (ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a
 
 extern
-fun {a:vt0p} queue_make  (cap : intGt(0)) : queue(a)
+fun {a:vt0p} queue_make (cap : intGt(0)) : queue(a)
 
 extern
-fun {a:t@ype} queue_free  (que : queue(a)) : void
+fun {a:t@ype} queue_free (que : queue(a)) : void
 
 assume queue_vtype(a : vt0p, id : int) = deqarray(a)
 assume ISNIL(id : int, b : bool) = unit_p
@@ -50,18 +50,18 @@
 vtypedef channel(a: vt0p) = channel_vtype(a)
 
 extern
-fun {a:vt0p} channel_insert  (!channel(a), a) : void
+fun {a:vt0p} channel_insert (!channel(a), a) : void
 
 extern
-fun {a:vt0p} channel_remove  (chan : !channel(a)) : a
+fun {a:vt0p} channel_remove (chan : !channel(a)) : a
 
 extern
-fun {a:vt0p} channel_remove_helper  ( chan : !channel(a)
-                                    , !queue(a) >> _
-                                    ) : a
+fun {a:vt0p} channel_remove_helper ( chan : !channel(a)
+                                   , !queue(a) >> _
+                                   ) : a
 
 extern
-fun {a:vt0p} channel_insert_helper  (!channel(a), !queue(a) >> _, a) :
+fun {a:vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) :
   void
 
 datavtype channel_ =
@@ -75,13 +75,13 @@
                                          }
 
 extern
-fun {a:vt0p} channel_make  (cap : intGt(0)) : channel(a)
+fun {a:vt0p} channel_make (cap : intGt(0)) : channel(a)
 
 extern
-fun {a:vt0p} channel_ref  (ch : !channel(a)) : channel(a)
+fun {a:vt0p} channel_ref (ch : !channel(a)) : channel(a)
 
 extern
-fun {a:vt0p} channel_unref  (ch : channel(a)) : Option_vt(queue(a))
+fun {a:vt0p} channel_unref (ch : channel(a)) : Option_vt(queue(a))
 
 extern
 fun channel_refcount {a:vt0p} (ch : !channel(a)) : intGt(0)
diff --git a/test/data/either.out b/test/data/either.out
new file mode 100644
--- /dev/null
+++ b/test/data/either.out
@@ -0,0 +1,37 @@
+#include "share/atspre_staload_libats_ML.hats"
+#include "libats/ML/SATS/SHARE/monad.hats"
+
+datatype either(a: t@ype, b: t@ype+) =
+  | left of a
+  | right of b
+
+fun {a:t@ype}{b:t@ype+} eq_either_either ( x : either(a, INV(b))
+                                         , y : either(a, b)
+                                         ) : bool
+
+fun {a:t@ype}{b:t@ype+} neq_either_either ( x : either(a, INV(b))
+                                          , y : either(a, b)
+                                          ) : bool
+
+overload = with eq_either_either
+
+overload != with neq_either_either
+
+fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
+  [ m : int | m <= n ] list(a, m)
+
+fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
+  [ m : int | m <= n ] list(b, m)
+
+fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} ( f : a -> c
+                                         , g : b -> c
+                                         , x : either(a, b)
+                                         ) : c
+
+fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
+
+fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
+
+fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b
+
+fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a
diff --git a/test/data/either.sats b/test/data/either.sats
new file mode 100644
--- /dev/null
+++ b/test/data/either.sats
@@ -0,0 +1,30 @@
+#include "share/atspre_staload_libats_ML.hats"
+#include "libats/ML/SATS/SHARE/monad.hats"
+
+datatype either(a: t@ype, b: t@ype+) =
+  | left of a
+  | right of b
+
+fun {a:t@ype}{b:t@ype+} eq_either_either  (x : either(a, INV(b)), y : either(a, b)) : bool
+
+fun {a:t@ype}{b:t@ype+} neq_either_either  (x : either(a, INV(b)), y : either(a, b)) : bool
+
+overload = with eq_either_either
+
+overload != with neq_either_either
+
+fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
+  [ m : int | m <= n ] list(a, m)
+
+fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
+  [ m : int | m <= n ] list(b, m)
+
+fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} (f : a -> c, g : b -> c, x : either(a, b)) : c
+
+fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
+
+fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool
+
+fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b
+
+fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a