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.15
+version:             0.1.1.17
 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
@@ -114,9 +114,9 @@
     effmaskWrt { Identifier $$ "effmask_wrt" }
     effmaskAll { Identifier $$ "effmask_all" }
     effmaskRef { Identifier $$ "effmask_ref" }
+    extfcall { Identifier $$ "extfcall" }
     tempenver { Identifier $$ "tempenver" }
     extype { Identifier $$ "extype" }
-    extfcall { Identifier $$ "extfcall" }
     ldelay { Identifier $$ "ldelay" }
     listVT { Identifier $$ "list_vt" }
     foldAt { Identifier $$ "fold@" }
@@ -247,7 +247,7 @@
      | Type at Type { At $2 (Just $1) $3 }
      | at Type { At $1 Nothing $2 }
      | atbrace Records rbrace { AnonymousRecord $1 $2 }
-     | openParen Type vbar Type closeParen { ProofType $1 $2 $4 }
+     | 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)] }
      | openParen TypeIn closeParen { Tuple $1 $2 }
      | openParen Type closeParen { ParenType $1 $2 }
@@ -316,7 +316,7 @@
        | IfCase vbar Expression CaseArrow Expression { ($3, $4, $5) : $1 }
 
 ExpressionPrf : ExpressionIn { (Nothing, $1) }
-              | Expression vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?
+              | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?
 
 -- | A list of comma-separated expressions
 ExpressionIn : Expression { [$1] }
@@ -507,6 +507,7 @@
      | dollar effmaskWrt { SpecialName $1 "effmask_wrt" }
      | dollar effmaskAll { SpecialName $1 "effmask_all" }
      | dollar effmaskRef { SpecialName $1 "effmask_ref" }
+     | dollar extfcall { SpecialName $1 "extfcall" }
      | dollar tempenver { SpecialName $1 "tempenver" }
      | dollar extype { SpecialName $1 "effmask_all" }
      | dollar listVT { SpecialName $1 "list_vt" }
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
@@ -123,8 +123,8 @@
     | length (showFast d2) >= 30 = d1 <$> indent 4 d2
     | otherwise = d1 <+> d2
 
-prettyArgsProof :: (Pretty a) => Maybe a -> [Doc] -> Doc
-prettyArgsProof (Just e) = prettyArgsG ("(" <> pretty e <+> "| ") ")"
+prettyArgsProof :: (Pretty a) => Maybe [a] -> [Doc] -> Doc
+prettyArgsProof (Just e) = prettyArgsG ("(" <> prettyArgsG mempty mempty (fmap pretty e) <+> "| ") ")"
 prettyArgsProof Nothing  = prettyArgs
 
 instance Pretty Expression where
@@ -293,7 +293,7 @@
         a (Vt0pF ad)              = "vt@ype" <> pretty ad
         a (AtF _ (Just t) t')     = t <+> "@" <+> t'
         a (AtF _ Nothing t)       = "@" <> t
-        a (ProofTypeF _ t t')     = parens (t <+> "|" <+> t')
+        a (ProofTypeF _ t t')     = parens (prettyArgsU "" "" t <+> "|" <+> t')
         a (ConcreteTypeF e)       = pretty e
         a (TupleF _ ts)           = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
         a (RefTypeF t)            = "&" <> 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
@@ -144,7 +144,7 @@
           | T0p Addendum -- t@ype
           | Vt0p Addendum -- vt@ype
           | At AlexPosn (Maybe Type) Type
-          | ProofType AlexPosn Type Type -- Aka (prf | val)
+          | ProofType AlexPosn [Type] Type -- Aka (prf | val)
           | ConcreteType StaticExpression
           | RefType Type
           | ViewType AlexPosn Type
@@ -244,7 +244,7 @@
                 | VoidLiteral -- The '()' literal representing inaction.
                     AlexPosn
                 -- function call: <a>, then {n}
-                | Call Name [[Type]] [Type] (Maybe Expression) [Expression]
+                | Call Name [[Type]] [Type] (Maybe [Expression]) [Expression]
                 | NamedVal Name
                 | ListLiteral AlexPosn String Type [Expression]
                 | If { cond     :: Expression -- ^ Expression evaluating to a boolean value
diff --git a/test/data/fastcount.dats b/test/data/fastcount.dats
new file mode 100644
--- /dev/null
+++ b/test/data/fastcount.dats
@@ -0,0 +1,99 @@
+(*
+**
+** A fast approach to counting newlines
+**
+** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
+** Time: April 17, 2013
+**
+*)
+#include "share/atspre_staload.hats"
+
+staload UN = "prelude/SATS/unsafe.sats"
+staload "libats/libc/SATS/stdio.sats"
+
+%{^
+extern void *rawmemchr(const void *s, int c);
+#define atslib_rawmemchr rawmemchr
+%}
+
+extern
+fun rawmemchr {l:addr}{m:int}(pf : bytes_v(l, m) | p : ptr(l), c : int) :
+  [ l2 : addr | l+m > l2 ] (bytes_v(l, l2-l),bytes_v(l2, l+m-l2) | ptr(l2)) =
+  "mac#atslib_rawmemchr"
+
+(* ****** ****** *)
+#define BUFSZ (16*1024)
+
+(* ****** ****** *)
+extern
+fun freadc {l:addr} (pf : !bytes_v(l, BUFSZ) | inp : FILEref, p : ptr(l), c : char) : size_t
+
+implement freadc (pf | inp, p, c) =
+  let
+    var n = $extfcall(size_t, "fread", p, sizeof<char>, BUFSZ - 1, inp)
+    val () = $UN.ptr0_set<char>(ptr_add<char>(p, n), c)
+  in
+    n
+  end
+
+(* ****** ****** *)
+extern
+fun wclbuf {l:addr}{n:int} (pf : !bytes_v(l, n) | p : ptr(l), pz : ptr, c : int, res : int) :
+  int
+
+implement wclbuf (pf | p, pz, c, res) =
+  let
+    val (pf1, pf2 | p2) = rawmemchr(pf | p, c)
+  in
+    if p2 < pz then
+      let
+        prval (pf21, pf22) = array_v_uncons(pf2)
+        var res = wclbuf(pf22 | ptr_succ<byte>(p2), pz, c, res + 1)
+        prval () = pf2 := array_v_cons(pf21, pf22)
+        prval () = pf := bytes_v_unsplit(pf1, pf2)
+      in
+        res
+      end
+    else
+      let
+        prval () = pf := bytes_v_unsplit(pf1, pf2)
+      in
+        res
+      end
+  end
+
+(* ****** ****** *)
+extern
+fun wclfil {l:addr} (pf : !bytes_v(l, BUFSZ) | inp : FILEref, p : ptr(l), c : int) : int
+
+implement wclfil {l} (pf | inp, p, c) =
+  let
+    fun loop(pf : !bytes_v(l, BUFSZ) | inp : FILEref, p : ptr(l), c : int, res : int) : int =
+      let
+        val n = freadc(pf | inp, p, $UN.cast{char}(c))
+      in
+        if n > 0 then
+          let
+            var pz = ptr_add<char>(p, n)
+            var res = wclbuf(pf | p, pz, c, res)
+          in
+            loop(pf | inp, p, c, res)
+          end
+        else
+          res
+      end
+  in
+    loop(pf | inp, p, c, 0)
+  end
+
+(* ****** ****** *)
+fun line_count(s : string) : int =
+  let
+    var inp: FILEref = fopen_ref_exn(s, file_mode_r)
+    val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))
+    prval () = pfat := b0ytes2bytes_v(pfat)
+    var res = wclfil(pfat | inp, p, $UN.cast2int('\n'))
+    val () = mfree_gc(pfat, pfgc | p)
+  in
+    res
+  end
diff --git a/test/data/fastcount.out b/test/data/fastcount.out
new file mode 100644
--- /dev/null
+++ b/test/data/fastcount.out
@@ -0,0 +1,115 @@
+(*
+**
+** A fast approach to counting newlines
+**
+** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
+** Time: April 17, 2013
+**
+*)
+#include "share/atspre_staload.hats"
+
+staload UN = "prelude/SATS/unsafe.sats"
+staload "libats/libc/SATS/stdio.sats"
+
+%{^
+extern void *rawmemchr(const void *s, int c);
+#define atslib_rawmemchr rawmemchr
+%}
+
+extern
+fun rawmemchr {l:addr}{m:int}( pf : bytes_v(l, m) | p : ptr(l)
+                             , c : int
+                             ) : [ l2 : addr | l+m > l2 ] ( bytes_v(l, l2-l)
+                                                          ,bytes_v(l2, l+m-l2)
+                                                           | ptr(l2)) =
+  "mac#atslib_rawmemchr"
+
+(* ****** ****** *)
+#define BUFSZ (16*1024)
+
+(* ****** ****** *)
+extern
+fun freadc {l:addr} ( pf : !bytes_v(l, BUFSZ) | inp : FILEref
+                    , p : ptr(l)
+                    , c : char
+                    ) : size_t
+
+implement freadc (pf | inp, p, c) =
+  let
+    var n = $extfcall(size_t, "fread", p, sizeof<char>, BUFSZ - 1, inp)
+    val () = $UN.ptr0_set<char>(ptr_add<char>(p, n), c)
+  in
+    n
+  end
+
+(* ****** ****** *)
+extern
+fun wclbuf {l:addr}{n:int} ( pf : !bytes_v(l, n) | p : ptr(l)
+                           , pz : ptr
+                           , c : int
+                           , res : int
+                           ) : int
+
+implement wclbuf (pf | p, pz, c, res) =
+  let
+    val (pf1, pf2 | p2) = rawmemchr(pf | p, c)
+  in
+    if p2 < pz then
+      let
+        prval (pf21, pf22) = array_v_uncons(pf2)
+        var res = wclbuf(pf22 | ptr_succ<byte>(p2), pz, c, res + 1)
+        prval () = pf2 := array_v_cons(pf21, pf22)
+        prval () = pf := bytes_v_unsplit(pf1, pf2)
+      in
+        res
+      end
+    else
+      let
+        prval () = pf := bytes_v_unsplit(pf1, pf2)
+      in
+        res
+      end
+  end
+
+(* ****** ****** *)
+extern
+fun wclfil {l:addr} ( pf : !bytes_v(l, BUFSZ) | inp : FILEref
+                    , p : ptr(l)
+                    , c : int
+                    ) : int
+
+implement wclfil {l} (pf | inp, p, c) =
+  let
+    fun loop( pf : !bytes_v(l, BUFSZ) | inp : FILEref
+            , p : ptr(l)
+            , c : int
+            , res : int
+            ) : int =
+      let
+        val n = freadc(pf | inp, p, $UN.cast{char}(c))
+      in
+        if n > 0 then
+          let
+            var pz = ptr_add<char>(p, n)
+            var res = wclbuf(pf | p, pz, c, res)
+          in
+            loop(pf | inp, p, c, res)
+          end
+        else
+          res
+      end
+  in
+    loop(pf | inp, p, c, 0)
+  end
+
+(* ****** ****** *)
+fun line_count(s : string) : int =
+  let
+    var inp: FILEref = fopen_ref_exn(s, file_mode_r)
+    val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))
+    prval () = pfat := b0ytes2bytes_v(pfat)
+    var res = wclfil(pfat | inp, p, $UN.cast2int('\n'))
+    val () = mfree_gc(pfat, pfgc | p)
+  in
+    res
+  end