diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # language-ats
 
+## 1.7.5.0
+
+  * Fix `StaticExpression` to allow calls with dynamic components
+
 ## 1.7.4.1
 
   * Improve pretty-printer
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.4.1
+version:         1.7.5.0
 license:         BSD3
 license-file:    LICENSE
 copyright:       Copyright: (c) 2018-2019 Vanessa McHale
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
@@ -465,8 +465,9 @@
      | Name openParen ExpressionPrf end {% left $ Expected $4 ")" "end"}
      | Name openParen ExpressionPrf else {% left $ Expected $4 ")" "else"}
 
-StaticArgs :: { [StaticExpression AlexPosn] }
-           : comma_sep(StaticExpression) { reverse (toList $1) }
+StaticArgs :: { ([StaticExpression AlexPosn], Maybe [Expression AlexPosn]) }
+           : comma_sep(StaticExpression) { (reverse (toList $1), Nothing) }
+           | comma_sep(StaticExpression) vbar comma_sep(Expression) { (reverse (toList $1), Just $ reverse (toList $3)) }
 
 StaticDecls :: { [Declaration AlexPosn] }
             : StaticDeclaration { [$1] }
@@ -483,15 +484,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 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!
+                 | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [] [$2] Nothing }
+                 | Name parens(StaticArgs) { SCall $1 [] [] (fst $2) (snd $2) }
+                 | Name Implicits parens(StaticArgs) { SCall $1 $2 [] (fst $3) (snd $3) }
+                 | Name TypeArgs parens(StaticArgs) { SCall $1 [] $2 (fst $3) (snd $3) }
+                 | Name TypeArgs doubleParens { SCall $1 [] $2 [] Nothing }
+                 | Name doubleParens { SCall $1 [] [] [] Nothing }
+                 | identifierSpace TypeArgs parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 (fst $3) (snd $3) }
+                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] [] (fst $2) (snd $2) }
+                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] [] Nothing } -- 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
@@ -278,14 +278,18 @@
         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 (SCallF n [] [] ["()"] Nothing)      = pretty n <> "()"
+        a (SCallF n [] us ["()"] Nothing)      = pretty n <> prettyTypes us <> "()"
+        a (SCallF n [] [] cs Nothing)          = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))
+        a (SCallF n [] us cs Nothing)          = pretty n <> prettyTypes us <> parens (commaTight cs)
+        a (SCallF n is [] ["()"] Nothing)      = pretty n <> prettyImplicits is <> "()"
+        a (SCallF n is us ["()"] Nothing)      = pretty n <> prettyImplicits is <> prettyTypes us <> "()"
+        a (SCallF n is [] cs Nothing)          = pretty n <> prettyImplicits is <> parens (commaTight cs)
+        a (SCallF n is us cs Nothing)          = pretty n <> prettyImplicits is <> prettyTypes us <> parens (commaTight cs)
+        a (SCallF n [] [] cs (Just ds))        = pretty n <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)
+        a (SCallF n [] us cs (Just ds))        = pretty n <> prettyTypes us <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)
+        a (SCallF n is [] cs (Just ds))        = pretty n <> prettyImplicits is <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)
+        a (SCallF n is us cs (Just ds))        = pretty n <> prettyImplicits is <> prettyTypes us <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)
         a (SPrecedeF e e')             = e <> ";" <+> e'
         a (SPrecedeListF es)           = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")
         a (SParensF e)                 = parens e
@@ -300,6 +304,12 @@
         a (ProofLinearLambdaF _ lt p e) = prettyLam "llam" p lt e
         a (WhereStaExpF e ds) = prettyWhere e ds
 
+        commaTight :: [Doc] -> Doc
+        commaTight = mconcat . punctuate ","
+
+        commaTightDyn :: Pretty b => [b] -> Doc
+        commaTightDyn = commaTight . fmap pretty
+
 instance Eq a => Pretty (Sort a) where
     pretty = cata a where
         a (T0pF ad)           = "t@ype" <> pretty ad
@@ -396,9 +406,9 @@
 isVal _         = False
 
 isOverload :: Declaration a -> Bool
-isOverload OverloadOp{} = True
+isOverload OverloadOp{}    = True
 isOverload OverloadIdent{} = True
-isOverload _ = False
+isOverload _               = False
 
 -- isTypeDef :: Declaration a -> Bool
 -- isTypeDef ViewTypeDef{} = True
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
@@ -86,7 +86,7 @@
 
 rewriteStaATS :: Eq a => FixityState a -> StaticExpression a -> StaticExpression a
 rewriteStaATS st = cata a where
-    a (SCallF n is ts [StaticVoid{}]) = SCall n is ts []
+    a (SCallF n is ts [StaticVoid{}] dyn) = SCall n is ts [] dyn
     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))
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
@@ -314,7 +314,7 @@
                         | 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]] [[Type a]] [StaticExpression a]
+                        | SCall (Name a) [[Type a]] [[Type a]] [StaticExpression a] (Maybe [Expression a])
                         | SUnary (UnOp a) (StaticExpression a)
                         | SLet a [Declaration a] (Maybe (StaticExpression a))
                         | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)]
@@ -334,7 +334,7 @@
                            | SPrecedeListF [x]
                            | StaticVoidF a
                            | SifF x x x
-                           | SCallF (Name a) [[Type a]] [[Type a]] [x]
+                           | SCallF (Name a) [[Type a]] [[Type a]] [x] (Maybe [Expression a])
                            | SUnaryF (UnOp a) x
                            | SLetF a [Declaration a] (Maybe x)
                            | SCaseF Addendum x [(Pattern a, LambdaType a, x)]
diff --git a/test/data/wc.dats b/test/data/wc.dats
new file mode 100644
--- /dev/null
+++ b/test/data/wc.dats
@@ -0,0 +1,132 @@
+staload "SATS/wc.sats"
+staload UN = "prelude/SATS/unsafe.sats"
+
+%{
+size_t sub_ptr1_ptr1_size(atstype_ptr p1, atstype_ptr p2) {
+  return ((char *)p1 - (char *)p2);
+}
+%}
+
+extern
+fn sub_ptr1_ptr1_size { l0, l1 : addr | l0 >= l1 }(p1 : ptr(l0), p2 : ptr(l1)) :<> size_t(l0-l1) =
+  "ext#"
+
+// bad (?) idea: use rawmemchr + append lol
+extern
+fn memchr { l : addr | l != null }{m:nat}{ n : nat | n <= m }(bytes_v(l,m) | ptr(l), int, size_t(n)) :
+  [ l0 : addr | l0 == null || l0 >= l && l0-l <= m ] (bytes_v(l, l0-l), bytes_v(l0, l+m-l0)| ptr(l0)) =
+  "mac#"
+
+extern
+fn memchr2 { l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m) | ptr(l), char, char, size_t(n)) :
+  Option_vt([ k : nat | k <= n ] size_t(k)) =
+  "ext#"
+
+extern
+fn memchr3 { l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m) | ptr(l), char, char, char, size_t(n)) :
+  Option_vt([ k : nat | k <= n ] size_t(k)) =
+  "ext#"
+
+fn freadc_ {l:addr}{ sz : nat | sz > 0 }{ n : nat | n <= sz }(pf : !bytes_v(l, sz)
+                                                             | inp : !FILEptr1, bufsize : size_t(sz), p : ptr(l)) :
+  size_t(n) =
+  let
+    extern
+    castfn as_fileref(x : !FILEptr1) :<> FILEref
+    
+    var n = $extfcall(size_t(n), "fread", p, sizeof<byte>, bufsize - 1, as_fileref(inp))
+  in
+    n
+  end
+
+extern
+fn count_char { l : addr | l != null }{m:nat}(!bytes_v(l, m) | ptr(l), c : char, bufsz : size_t(m)) :
+  [ n : nat | n <= m ] int(n) =
+  "ext#"
+
+fn count_lines { l : addr | l != null }{m:nat}(pf : !bytes_v(l, m) | p : ptr(l), bufsz : size_t(m)) :
+  [ n : nat | n <= m ] int(n) =
+  count_char(pf | p, '\n', bufsz)
+
+implement empty_file =
+  @{ lines = 0, blanks = 0, comments = 0, doc_comments = 0 } : file
+
+implement free_st (st) =
+  case+ st of
+    | ~in_string (_) => ()
+    | ~in_block_comment (_) => ()
+    | ~line_comment() => ()
+    | ~regular() => ()
+
+(* fun charptr1_add_guint{l:addr}{i:int}(p:ptr(l), offsz: size_t(i)) :<> ptr(l+i) = *)
+
+implement count_buf (pf | ptr, bufsz, st) =
+  case+ st of
+    | ~in_string (n) => let
+      // 34 -> "
+      val (pf0, pf1 | p2) = memchr(pf | ptr, 34, bufsz)
+    in
+      if ptr_is_null(p2) then
+        let
+          prval () = pf := bytes_v_unsplit(pf0,pf1)
+          var strlines = count_lines(pf | ptr, bufsz)
+          val () = st := in_string(n + strlines)
+        in
+          empty_file
+        end
+      else
+        let
+          //TODO: check that p2's predecessor is not a backslash
+          var pred_is_slash = if p2 > ptr then
+            let
+              val () = print(p2)
+            in
+              // 92 -> \
+              ptr1_pred<byte>(p2) = $UN.cast(92)
+            end
+          else
+            false
+          var bytes_taken = sub_ptr1_ptr1_size(p2, ptr)
+          var strlines = count_lines(pf0 | ptr, bytes_taken)
+          var in_str = strlines + n
+          var bytes_remaining = bufsz - bytes_taken
+          val () = st := regular()
+          var ret_file: file
+          val () = ret_file := count_buf(pf1 | p2, bytes_remaining, st)
+          val () = ret_file.lines := ret_file.lines + strlines
+          prval () = pf := bytes_v_unsplit(pf0,pf1)
+        in
+          ret_file
+        end
+    end
+    | in_block_comment (_) => empty_file
+    | line_comment () => empty_file
+    | regular() => let
+      val next_char_offset = memchr3(pf | ptr, '\n', '"', '/', bufsz)
+      val ret = case+ next_char_offset of
+        | ~Some_vt (char_ptr_off) => let
+          var char_ptr = add_ptr_bsz(ptr, char_ptr_off)
+          var char_val = $UN.ptr0_get<char>(char_ptr)
+          
+          extern
+          praxi ptr_eq { l0, l1 : addr }{m:nat} (pf : !bytes_v(l0, m) | ptr(l1)) : [l0 == l1 && l0 != null] void
+          
+          var ret_file = case- char_val of
+            | '\n' => let
+              prval (pf0, pf1) = bytes_v_split_at(pf | char_ptr_off)
+              prval () = ptr_eq(pf1 | char_ptr)
+              var bytes_remaining = bufsz - char_ptr_off
+              var ret_file: file
+              val () = ret_file := count_buf(pf1 | char_ptr, bytes_remaining, st)
+              prval () = pf := bytes_v_unsplit(pf0,pf1)
+            in
+              ret_file
+            end
+            | _ => empty_file
+        in
+          ret_file
+        end
+        | ~None_vt() => empty_file
+    in
+      ret
+    end
diff --git a/test/data/wc.out b/test/data/wc.out
new file mode 100644
--- /dev/null
+++ b/test/data/wc.out
@@ -0,0 +1,148 @@
+staload "SATS/wc.sats"
+staload UN = "prelude/SATS/unsafe.sats"
+
+%{
+size_t sub_ptr1_ptr1_size(atstype_ptr p1, atstype_ptr p2) {
+  return ((char *)p1 - (char *)p2);
+}
+%}
+
+extern
+fn sub_ptr1_ptr1_size { l0, l1 : addr | l0 >= l1 }( p1 : ptr(l0)
+                                                  , p2 : ptr(l1)
+                                                  ) :<> size_t(l0-l1) =
+  "ext#"
+
+// bad (?) idea: use rawmemchr + append lol
+extern
+fn memchr
+{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(bytes_v(l,m)
+                                                   | ptr(l), int, size_t(n)) :
+  [ l0 : addr | l0 == null || l0 >= l && l0-l <= m ] ( bytes_v(l, l0-l)
+                                                     , bytes_v(l0, l+m-l0)
+                                                     | ptr(l0)) =
+  "mac#"
+
+extern
+fn memchr2
+{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m)
+                                                   | ptr(l), char, char, size_t(n)) :
+  Option_vt([ k : nat | k <= n ] size_t(k)) =
+  "ext#"
+
+extern
+fn memchr3
+{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m)
+                                                   | ptr(l), char, char, char, size_t(n)) :
+  Option_vt([ k : nat | k <= n ] size_t(k)) =
+  "ext#"
+
+fn freadc_
+{l:addr}{ sz : nat | sz > 0 }{ n : nat | n <= sz }(pf : !bytes_v(l, sz)
+                                                  | inp : !FILEptr1, bufsize : size_t(sz), p : ptr(l)) : size_t(n) =
+  let
+    extern
+    castfn as_fileref(x : !FILEptr1) :<> FILEref
+    
+    var n = $extfcall( size_t(n)
+                     , "fread"
+                     , p
+                     , sizeof<byte>
+                     , bufsize - 1
+                     , as_fileref(inp)
+                     )
+  in
+    n
+  end
+
+extern
+fn count_char { l : addr | l != null }{m:nat}(!bytes_v(l, m)
+                                             | ptr(l), c : char, bufsz : size_t(m)) : [ n : nat | n <= m ] int(n) =
+  "ext#"
+
+fn count_lines { l : addr | l != null }{m:nat}(pf : !bytes_v(l, m)
+                                              | p : ptr(l), bufsz : size_t(m)) : [ n : nat | n <= m ] int(n) =
+  count_char(pf | p, '\n', bufsz)
+
+implement empty_file =
+  @{ lines = 0, blanks = 0, comments = 0, doc_comments = 0 } : file
+
+implement free_st (st) =
+  case+ st of
+    | ~in_string (_) => ()
+    | ~in_block_comment (_) => ()
+    | ~line_comment() => ()
+    | ~regular() => ()
+
+(* fun charptr1_add_guint{l:addr}{i:int}(p:ptr(l), offsz: size_t(i)) :<> ptr(l+i) = *)
+implement count_buf (pf | ptr, bufsz, st) =
+  case+ st of
+    | ~in_string (n) => let
+      // 34 -> "
+      val (pf0, pf1 | p2) = memchr(pf | ptr, 34, bufsz)
+    in
+      if ptr_is_null(p2) then
+        let
+          prval () = pf := bytes_v_unsplit(pf0,pf1)
+          var strlines = count_lines(pf | ptr, bufsz)
+          val () = st := in_string(n + strlines)
+        in
+          empty_file
+        end
+      else
+        let
+          //TODO: check that p2's predecessor is not a backslash
+          var pred_is_slash = if p2 > ptr then
+            let
+              val () = print(p2)
+            in
+              // 92 -> \
+              ptr1_pred<byte>(p2) = $UN.cast(92)
+            end
+          else
+            false
+          var bytes_taken = sub_ptr1_ptr1_size(p2, ptr)
+          var strlines = count_lines(pf0 | ptr, bytes_taken)
+          var in_str = strlines + n
+          var bytes_remaining = bufsz - bytes_taken
+          val () = st := regular()
+          var ret_file: file
+          val () = ret_file := count_buf(pf1 | p2, bytes_remaining, st)
+          val () = ret_file.lines := ret_file.lines + strlines
+          prval () = pf := bytes_v_unsplit(pf0,pf1)
+        in
+          ret_file
+        end
+    end
+    | in_block_comment (_) => empty_file
+    | line_comment () => empty_file
+    | regular() => let
+      val next_char_offset = memchr3(pf | ptr, '\n', '"', '/', bufsz)
+      val ret = case+ next_char_offset of
+        | ~Some_vt (char_ptr_off) => let
+          var char_ptr = add_ptr_bsz(ptr, char_ptr_off)
+          var char_val = $UN.ptr0_get<char>(char_ptr)
+          
+          extern
+          praxi ptr_eq { l0, l1 : addr }{m:nat} (pf : !bytes_v(l0, m) | ptr(l1)) :
+            [l0 == l1 && l0 != null] void
+          
+          var ret_file = case- char_val of
+            | '\n' => let
+              prval (pf0, pf1) = bytes_v_split_at(pf | char_ptr_off)
+              prval () = ptr_eq(pf1 | char_ptr)
+              var bytes_remaining = bufsz - char_ptr_off
+              var ret_file: file
+              val () = ret_file := count_buf(pf1 | char_ptr, bytes_remaining, st)
+              prval () = pf := bytes_v_unsplit(pf0,pf1)
+            in
+              ret_file
+            end
+            | _ => empty_file
+        in
+          ret_file
+        end
+        | ~None_vt() => empty_file
+    in
+      ret
+    end