diff --git a/bench/Bench.hs b/bench/Bench.hs
--- a/bench/Bench.hs
+++ b/bench/Bench.hs
@@ -16,5 +16,5 @@
                       ]
                 ]
     where large = readFile "test/data/polyglot.dats"
-          medium = readFile "test/data/toml-parse.dats"
+          medium = readFile "test/data/stdlib/checkast.sats"
           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.2.0.3
+version:             0.2.0.5
 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
@@ -33,6 +33,7 @@
                     , Fixity (..)
                     , SortArg (..)
                     , Sort (..)
+                    , SortArgs
                     -- * Lexical types
                     , Token (..)
                     , AlexPosn (..)
@@ -56,6 +57,7 @@
 parseATS' :: String -> Either (ATSError String) ATS
 parseATS' = parseATS . lexATS
 
+-- TODO use Language.C.Parser 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
@@ -52,7 +52,7 @@
 
 -- Floats
 @decimals = $digit+
-@float = @decimals \. @decimals
+@float = @decimals \. @decimals ("f" | "")
 
 -- Strings
 @string = \" ($printable # [\"\\] | @escape_str | $esc_char | \\ \n | \n)* \"
@@ -76,7 +76,7 @@
 @not_close_c = \% [^\}]
 @c_block = \%\{ ("#" | "$" | "^" | "") ([^\%] | @not_close_c | \n)* \%\}
 
-@inner_signature = ("!wrt" | "!exn" | "!exnwrt" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | "fe" | @block_comment)
+@inner_signature = ("!wrt" | "!exn" | "!refwrt" | "!exnwrt" | "!exnrefwrt" | "!exnref" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | "fe" | @block_comment)
 @inner_signature_mult = (@inner_signature (("," | "") @inner_signature)*) | ""
 
 @lambda = "=>" | "=>>" | "=<" @inner_signature_mult ">"
@@ -97,7 +97,7 @@
 
 @fixity_decl = "infixr" | "infixl" | "prefix" | "postfix"
 
-@builtin = \$ (("effmask_" (wrt | all | ref)) | "extfcall" | "ldelay" | "delay" | "list_vt" | "tempenver" | "extype")
+@builtin = \$ (("effmask_" (wrt | all | ref)) | "extfcall" | "ldelay" | "delay" | "list_vt" | "tempenver" | "extype" | "mylocation" | "showtype")
 
 tokens :-
 
@@ -214,7 +214,7 @@
     $br / @ref_call          { tok (\p s -> alex $ SpecialBracket p) }
     @operator                { tok (\p s -> alex $ Operator p s) }
     @signature               { tok (\p s -> alex $ SignatureTok p (tail s)) }
-    @builtin                 { tok (\p s -> alex $ Identifier p s) }
+    @builtin                 { tok (\p s -> alex $ SpecialIdentifier p (tail s)) }
     $special                 { tok (\p s -> alex $ Special p s) }
     @identifier / " "        { tok (\p s -> alex $ IdentifierSpace p s) }
     @identifier              { tok (\p s -> alex $ Identifier p s) }
@@ -322,6 +322,7 @@
              deriving (Eq, Show, Generic, NFData)
 
 data Token = Identifier AlexPosn String
+           | SpecialIdentifier AlexPosn String
            | Keyword AlexPosn Keyword
            | IntTok AlexPosn Int
            | FloatTok AlexPosn Float
@@ -426,6 +427,7 @@
     pretty KwMacdef = "macdef"
 
 instance Pretty Token where
+    pretty (SpecialIdentifier _ s) = text ('$' : s)
     pretty (Identifier _ s) = text s
     pretty (IdentifierSpace _ s) = text s
     pretty (Keyword _ kw) = pretty kw
@@ -452,8 +454,10 @@
 to_string (CommentLex _ s) = s
 to_string (Identifier _ s) = s
 to_string (IdentifierSpace _ s) = s
+to_string (SpecialIdentifier _ s) = s
 to_string _ = undefined
 
+token_posn (SpecialIdentifier p _) = p
 token_posn (Identifier p _) = p
 token_posn (IdentifierSpace p _) = p
 token_posn (Keyword p _) = p
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
@@ -90,6 +90,7 @@
     sortdef { Keyword $$ KwSortdef }
     local { Keyword $$ KwLocal }
     view { Keyword $$ (KwView None) }
+    viewContra { Keyword $$ (KwView Minus) }
     vtype { $$@(Keyword _ KwVtype{}) }
     viewPlusMinus { Keyword _ (KwView $$) }
     raise { Keyword $$ KwRaise }
@@ -105,15 +106,7 @@
     timeLit { TimeTok _ $$ }
     intLit { IntTok _ $$ }
     floatLit { FloatTok _ $$ }
-    effmaskWrt { Identifier $$ "$effmask_wrt" }
-    effmaskAll { Identifier $$ "$effmask_all" }
-    effmaskRef { Identifier $$ "$effmask_ref" }
-    extfcall { Identifier $$ "$extfcall" }
-    tempenver { Identifier $$ "$tempenver" }
-    extype { Identifier $$ "$extype" }
-    ldelay { Identifier $$ "$ldelay" }
-    delay { Identifier $$ "$delay" }
-    listVT { Identifier $$ "$list_vt" }
+    specialIdentifier { $$@SpecialIdentifier{} }
     foldAt { Identifier $$ "fold@" }
     identifier { $$@Identifier{} }
     identifierSpace { $$@IdentifierSpace{} }
@@ -223,8 +216,8 @@
      | viewPlusMinus { ViewLiteral $1 }
      | Existential Type { Ex $1 $2 }
      | Universal Type { ForA $1 $2 }
-     | Type at Type { At $2 (Just $1) $3 }
-     | at Type { At $1 Nothing $2 }
+     | Type at StaticExpression { At $2 $1 $3 }
+     | at Type { AtType $1 $2 }
      | atbrace Records rbrace { AnonymousRecord $1 $2 }
      | openParen TypeIn vbar Type closeParen { ProofType $1 $2 $4 } -- FIXME can have multiple first parts
      | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }
@@ -323,7 +316,6 @@
 -- | Expression or named call to an expression
 Expression : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [] [] Nothing [$2] }
            | PreExpression { $1 }
-           | openParen Tuple closeParen { TupleEx $1 $2 }
            | openParen PreExpression comma PreExpression vbar PreExpression closeParen { TupleEx $1 [$2, $4, $6] } -- FIXME this is wrong
            | Expression semicolon Expression { Precede $1 $3 }
            | Expression semicolon { $1 }
@@ -332,7 +324,6 @@
            | openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 }
            | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }
            | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 } -- TODO is this legal??
-           | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }
            | begin Expression extern {% Left $ Expected $3 "end" "extern" }
            | Expression prfTransform underscore {% Left $ Expected $2 "Rest of expression or declaration" ">>" }
 
@@ -377,11 +368,12 @@
                  | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] }
                  | let StaticDecls in end { SLet $1 $2 Nothing }
                  | let StaticDecls in StaticExpression end { SLet $1 $2 (Just $4) }
-    
+
 -- | Parse an expression that can be called without parentheses
 PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }
               | Literal { $1 }
               | Call { $1 }
+              | openParen Tuple closeParen { TupleEx $1 $2 }
               | case Expression of Case { Case $3 $1 $2 $4 }
               | ifcase IfCase { IfCase $1 $2 }
               | openParen Expression closeParen { ParenExpr $1 $2 }
@@ -414,6 +406,7 @@
               | lbrace ATS rbrace { Actions $2 }
               | 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) }
               | include {% Left $ Expected $1 "Expression" "include" }
               | staload {% Left $ Expected (token_posn $1) "Expression" "staload" }
               | overload {% Left $ Expected $1 "Expression" "overload" }
@@ -443,10 +436,12 @@
      | vt0pCo { Vt0p Plus }
      | addr { Addr }
      | view { View $1 None }
+     | viewContra { View $1 Minus }
      | vtype { VType (token_posn $1) (get_addendum $1) }
      | IdentifierOr { 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) }
@@ -487,6 +482,7 @@
 FunName : IdentifierOr { Unqualified $1 }
         | identifier dollar identifier { Functorial (to_string $1) (to_string $3) }
         | dollar identifier dot IdentifierOr { Qualified $1 (to_string $2) $4 }
+        | FunName lineComment { $1 }
 
 -- | Parse a general name
 Name : identifier { Unqualified (to_string $1) }
@@ -499,15 +495,7 @@
      | dollar identifier dot identifier { Qualified $1 (to_string $4) (to_string $2) }
      | dollar identifier dot identifierSpace { Qualified $1 (to_string $4) (to_string $2) }
      | dollar identifier dot identifier dollar IdentifierOr { Qualified $1 (to_string $4 ++ ('$' : $6)) (to_string $2) }
-     | effmaskWrt { SpecialName $1 "effmask_wrt" }
-     | effmaskAll { SpecialName $1 "effmask_all" }
-     | effmaskRef { SpecialName $1 "effmask_ref" }
-     | extfcall { SpecialName $1 "extfcall" }
-     | tempenver { SpecialName $1 "tempenver" }
-     | extype { SpecialName $1 "effmask_all" }
-     | listVT { SpecialName $1 "list_vt" }
-     | ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better way of doing this
-     | delay { SpecialName $1 "delay" }
+     | specialIdentifier { SpecialName (token_posn $1) (to_string $1) }
      | dollar {% Left $ Expected $1 "Name" "$" }
 
 -- | Parse a list of values in a record
@@ -677,9 +665,9 @@
          | datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 }
          | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 }
          | abst0p IdentifierOr SortArgs MaybeType { AbsT0p $1 $2 $3 $4 }
-         | viewdef IdentifierOr openParen FullArgs closeParen eq Type { ViewDef $1 $2 $4 $7 }
+         | viewdef IdentifierOr SortArgs eq Type { ViewDef $1 $2 $3 $5 }
          | absvt0p IdentifierOr SortArgs eq Type { AbsVT0p $1 $2 $3 (Just $5) }
-         | absview IdentifierOr openParen FullArgs closeParen MaybeType { AbsView $1 $2 $4 $6 }
+         | absview IdentifierOr SortArgs MaybeType { AbsView $1 $2 $3 $4 }
          | abstype IdentifierOr SortArgs MaybeType { AbsType $1 $2 $3 $4 }
          | absvtype IdentifierOr SortArgs MaybeType { AbsViewType $1 $2 $3 $4 }
          | dataprop IdentifierOr SortArgs eq DataPropLeaves { DataProp $1 $2 $3 $5 }
@@ -726,6 +714,7 @@
             | define identifier string { Define ($1 ++ " " ++ to_string $2 ++ $3) } -- FIXME better approach?
             | define identifierSpace intLit { Define ($1 ++ " " ++ to_string $2 ++ " " ++ show $3) }
             | cblock { CBlock $1 }
+            | 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) }
             | staload underscore eq string { Staload (get_staload $1) (Just "_") $4 }
@@ -742,10 +731,13 @@
             | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $5) Nothing }
             | implement FunArgs Implementation { Impl $2 $3 }
             | StaticDeclaration { $1 }
-            | overload BinOp with Name { OverloadOp $1 $2 $4 }
+            | overload BinOp with Name { OverloadOp $1 $2 $4 Nothing }
+            | overload BinOp with identifierSpace of intLit { OverloadOp $1 $2 (Unqualified $ to_string $4) (Just $6) }
             | overload identifierSpace with Name { OverloadIdent $1 (to_string $2) $4 Nothing }
             | overload identifierSpace with identifierSpace of intLit { OverloadIdent $1 (to_string $2) (Unqualified $ to_string $4) (Just $6) }
             | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) } -- FIXME figure out a general solution.
+            | overload lsqbracket rsqbracket with identifierSpace of intLit { OverloadIdent $1 "[]" (Unqualified $ to_string $5) (Just $7) }
+            | overload dot identifierSpace with Name { OverloadIdent $1 ('.' : (to_string $3)) $5 Nothing }
             | assume identifierSpace eq Type { Assume (Unqualified (to_string $2)) [NoArgs] $4 }
             | assume Name eq Type { Assume $2 [NoArgs] $4 }
             | assume Name doubleParens eq Type { Assume $2 [] $5 }
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
@@ -293,8 +293,8 @@
         a (AsProofF t Nothing)    = t <+> ">> _"
         a (FromVTF t)             = t <> "?!"
         a (MaybeValF t)           = t <> "?"
-        a (AtF _ (Just t) t')     = t <+> "@" <+> t'
-        a (AtF _ Nothing t)       = "@" <> t
+        a (AtF _ t t')            = t <+> "@" <+> pretty t'
+        a (AtTypeF _ t)           = "@" <> t
         a (ProofTypeF _ t t')     = parens (prettyArgsG "" "" t <+> "|" <+> t')
         a (ConcreteTypeF e)       = pretty e
         a (TupleF _ ts)           = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
@@ -489,16 +489,14 @@
 
 -- FIXME figure out a nicer algorithm for when/how to split lines.
 instance Pretty PreFunction where
-    pretty (PreF i si [] [] NoA rt Nothing (Just e)) = pretty i <> prettySig si rt <> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack
-    pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] us NoA rt t (Just e)) = pretty i </> fancyU us <> prettyTermetric t <> prettySig si rt <> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] us as rt t (Just e)) = pretty i </> fancyU us <> prettyTermetric t <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si pus us as rt t (Just e)) = fancyU pus </> pretty i </> fancyU us <> prettyTermetric t <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us as rt t (Just e)) = pretty i </> fancyU us <> prettyTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus us as rt t (Just e)) = fancyU pus </> pretty i </> fancyU us <> prettyTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
+    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 </> prettyArgs as <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si pus us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgs as <+> ":" <> 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 us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt
 
 instance Pretty DataPropLeaf where
     pretty (DataPropLeaf us e Nothing)   = "|" <+> foldMap pretty (reverse us) <+> pretty e
@@ -540,7 +538,8 @@
     pretty (Staload b (Just q) s)          = bool "" "#" b <> "staload" <+> pretty q <+> "=" <+> pretty s
     pretty (CBlock s)                      = string s
     pretty (Comment s)                     = string s
-    pretty (OverloadOp _ o n)              = "overload" <+> pretty o <+> "with" <+> pretty n
+    pretty (OverloadOp _ o n (Just n'))    = "overload" <+> pretty o <+> "with" <+> pretty n <+> "of" <+> pretty n'
+    pretty (OverloadOp _ o n Nothing)      = "overload" <+> pretty o <+> "with" <+> pretty n
     pretty (OverloadIdent _ i n Nothing)   = "overload" <+> text i <+> "with" <+> pretty n
     pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n'
     -- We use 'text' here, which means indentation might get fucked up for
@@ -565,7 +564,7 @@
     pretty (SymIntr _ n)                   = "symintr" <+> pretty n
     pretty (Stacst _ n t Nothing)          = "stacst" </> pretty n <+> ":" </> pretty t
     pretty (Stacst _ n t (Just e))         = "stacst" </> pretty n <+> ":" </> pretty t <+> "=" </> pretty e
-    pretty (PropDef _ s as t)              = "propdef" </> text s <+> prettyArgs as <+> "=" </> pretty t
+    pretty (PropDef _ s as t)              = "propdef" </> text s <+> prettyArgsNil as <+> "=" </> pretty t
     pretty (Local _ d d')                  = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"
     pretty (FixityDecl f (Left s) ss)      = pretty f <+> "(" <> text s <> ")" <+> hsep (fmap text ss)
     pretty (FixityDecl f (Right i) ss)     = pretty f <+> pretty i <+> hsep (fmap text ss)
@@ -574,11 +573,10 @@
     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 (AbsView _ i as t)              = "absview" <+> text i <> prettyArgs as <> prettyMaybeType 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
-    pretty (ViewDef _ s [] t)              = "viewdef" <+> text s <+> "=" <#> pretty t
-    pretty (ViewDef _ s as t)              = "viewdef" <+> text s <> prettyArgs as <+> "=" <#> pretty t
+    pretty (ViewDef _ s as t)              = "viewdef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t
     pretty (TKind _ n s)                   = pretty n <+> "=" <+> text s
     pretty (SortDef _ s t)                 = "sortdef" <+> text s <+> "=" <+> either pretty pretty t
     pretty (AndD d (SortDef _ i t))        = pretty d <+> "and" <+> text i <+> "=" <+> either pretty 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
@@ -97,11 +97,11 @@
                  | SumViewType { typeName :: String, typeArgs :: SortArgs, _leaves :: [Leaf] }
                  | AbsType AlexPosn String SortArgs (Maybe Type)
                  | AbsViewType AlexPosn String SortArgs (Maybe Type)
-                 | AbsView AlexPosn String [Arg] (Maybe Type)
+                 | AbsView AlexPosn String SortArgs (Maybe Type)
                  | AbsVT0p AlexPosn String SortArgs (Maybe Type)
                  | AbsT0p AlexPosn String SortArgs (Maybe Type)
-                 | ViewDef AlexPosn String [Arg] Type
-                 | OverloadOp AlexPosn BinOp Name
+                 | ViewDef AlexPosn String SortArgs Type
+                 | OverloadOp AlexPosn BinOp Name (Maybe Int)
                  | OverloadIdent AlexPosn String Name (Maybe Int)
                  | Comment String
                  | DataProp AlexPosn String SortArgs [DataPropLeaf]
@@ -135,7 +135,8 @@
           | 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
-          | At AlexPosn (Maybe Type) Type
+          | At AlexPosn Type StaticExpression
+          | AtType AlexPosn Type
           | ProofType AlexPosn [Type] Type -- Aka (prf | val)
           | ConcreteType StaticExpression
           | RefType Type
@@ -154,13 +155,13 @@
                 | Spear AlexPosn
                 deriving (Show, Eq, Generic, NFData)
 
--- | A name can be qualified (@$UN.unsafefn@) or not
+
 data Name = Unqualified String
-          | Qualified AlexPosn String String -- TODO String Name
-          | SpecialName AlexPosn String
+          | Qualified AlexPosn String String -- ^ A name can be qualified (@$UN.unsafefn@)
+          | SpecialName AlexPosn String -- ^ A name for builtin functions such as @$showtype@.
           | Functorial String String
-          | Unnamed AlexPosn
           | FieldName AlexPosn String String
+          | Unnamed AlexPosn
           deriving (Show, Eq, Generic, NFData)
 
 -- | A data type for patterns.
@@ -311,7 +312,7 @@
                 | MacroVar AlexPosn String
                 deriving (Show, Eq, Generic, NFData)
 
--- | An 'implement' declaration
+-- | An 'implement' or 'primplmnt' declaration
 data Implementation = Implement { pos            :: AlexPosn
                                 , preUniversalsI :: [Universal]
                                 , implicits      :: [[Type]] -- ^ Implicit arguments
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -11,4 +11,5 @@
 main :: IO ()
 main = hspec $
     describe "pretty-print" $ parallel $
-        testFiles "test/data" isATS (fmap printATS . parseATS . lexATS)
+        mapM_ (\x -> testFiles x isATS (fmap printATS . parseATS . lexATS))
+            ["test/data", "test/data/stdlib", "test/data/stdlib/DATS"]