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.2.0.15
+version: 1.2.0.16
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale
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
@@ -155,6 +155,7 @@
     <0> fnx                      { tok (\p _ -> alex $ Keyword p KwFnx) }
     <0> and                      { tok (\p _ -> alex $ Keyword p KwAnd) }
     <0> prval                    { tok (\p _ -> alex $ Keyword p KwPrval) }
+    <0> prvar                    { tok (\p _ -> alex $ Keyword p KwPrvar) }
     <0> prfn                     { tok (\p _ -> alex $ Keyword p KwPrfn) }
     <0> prfun                    { tok (\p _ -> alex $ Keyword p KwPrfun) }
     <0> datatype                 { tok (\p _ -> alex $ Keyword p KwDatatype) }
@@ -365,6 +366,7 @@
              | KwOf
              | KwAbsprop
              | KwPrval
+             | KwPrvar
              | KwStadef
              | KwPraxi
              | KwWhile
@@ -491,6 +493,7 @@
     pretty KwOf = "of"
     pretty KwAbsprop = "absprop"
     pretty KwPrval = "prval"
+    pretty KwPrvar = "prvar"
     pretty KwStadef = "stadef"
     pretty KwPraxi = "praxi"
     pretty KwWhile = "while"
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
@@ -77,6 +77,7 @@
     stadef { Keyword $$ KwStadef }
     val { $$@(Keyword _ (KwVal _)) }
     prval { Keyword $$ KwPrval }
+    prvar { Keyword $$ KwPrvar }
     var { Keyword $$ KwVar }
     then { Keyword $$ KwThen }
     let { Keyword $$ KwLet }
@@ -481,7 +482,8 @@
               | lbrace ATS rbrace { Actions $2 }
               | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }
               | for openParen PreExpression closeParen PreExpression { For $1 $3 $5 }
-              | whileStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $8 $9 }
+              | whileStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $8 $9 Nothing }
+              | whileStar Universals Termetric openParen Args closeParen colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $12 $13 (Just $9) }
               | forStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { ForStar $1 $2 (snd $3) $5 $8 $9 }
               | lineComment PreExpression { CommentExpr (to_string $1) $2 }
               | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }
@@ -850,6 +852,9 @@
 StaticDeclaration : prval Pattern eq Expression { PrVal $2 (Just $4) Nothing }
                   | prval Pattern colon Type { PrVal $2 Nothing (Just $4) }
                   | prval Pattern colon Type eq Expression { PrVal $2 (Just $6) (Just $4) }
+                  | prvar Pattern eq Expression { PrVar $2 (Just $4) Nothing }
+                  | prvar Pattern colon Type { PrVar $2 Nothing (Just $4) }
+                  | prvar Pattern colon Type eq Expression { PrVar $2 (Just $6) (Just $4) }
                   | praxi PreFunction { Func $1 (Praxi $2) }
                   | primplmnt FunArgs StaticImplementation { ProofImpl $2 $3 }
                   | StafunDecl { $1 }
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
@@ -141,11 +141,15 @@
         a (CallF nam [] [] Nothing []) = pretty nam <> "()"
         a (CallF nam [] [] e xs) = pretty nam <> prettyArgsProof e xs
         a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us
+        a (CallF nam [] us Nothing [x])
+            | startsParens x = pretty nam <> prettyArgsU "{" "}" us <> pretty x
         a (CallF nam [] us e xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
         a (CallF nam is [] Nothing []) = pretty nam <> prettyImplicits is
         a (CallF nam is [] Nothing [x])
             | startsParens x = pretty nam <> prettyImplicits is <> pretty x
         a (CallF nam is [] e xs) = pretty nam <> prettyImplicits is <> prettyArgsProof e xs
+        a (CallF nam is us Nothing [x])
+            | startsParens x = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> pretty x
         a (CallF nam is us e xs) = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
         a (CaseF _ add' e cs)           = "case" <> pretty add' <+> e <+> "of" <$> indent 2 (prettyCases cs)
         a (IfCaseF _ cs)                = "ifcase" <$> indent 2 (prettyIfCase cs)
@@ -169,7 +173,8 @@
         a (BoxTupleExF _ es)           = "'(" <> mconcat (punctuate ", " (reverse es)) <> ")"
         a (WhileF _ e e')              = "while" <> parens e <> e'
         a (ForF _ e e')                = "for" <> parens e <> e'
-        a (WhileStarF _ us t as e e')  = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'
+        a (WhileStarF _ us t as e e' Nothing)   = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'
+        a (WhileStarF _ us t as e e' (Just ty)) = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> ":" <+> prettyArgs ty <+> "=>" <$> indent 4 e <$> indent 4 e'
         a (ForStarF _ us t as e e')    = "for*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'
         a (ActionsF (ATS [d]))         = "{" <+> pretty d <+> "}"
         a (ActionsF as)                = "{" <$> indent 2 (pretty as) <$> "}"
@@ -349,6 +354,7 @@
 isVal Val{}   = True
 isVal Var{}   = True
 isVal PrVal{} = True
+isVal PrVar{} = True
 isVal _       = False
 
 glue :: Declaration a -> Declaration a -> Bool
@@ -559,6 +565,10 @@
     pretty (PrVal p Nothing (Just t))       = "prval" <+> pretty p <+> ":" <+> pretty t
     pretty (PrVal p (Just e) (Just t))      = "prval" <+> pretty p <+> ":" <+> pretty t <+> "=" <+> pretty e
     pretty PrVal{}                          = undefined
+    pretty (PrVar p (Just e) Nothing)       = "prvar" <+> pretty p <+> "=" <+> pretty e
+    pretty (PrVar p Nothing (Just t))       = "prvar" <+> pretty p <+> ":" <+> pretty t
+    pretty (PrVar p (Just e) (Just t))      = "prvar" <+> pretty p <+> ":" <+> pretty t <+> "=" <+> pretty e
+    pretty PrVar{}                          = undefined
     pretty (AndDecl t p e)                  = "and" <+> pretty p <> valSig t <+> "=" <+> pretty e
     pretty (Val a t p e)                    = "val" <> pretty a <+> pretty p <> valSig t <+> "=" <+> pretty e
     pretty (Var t p Nothing (Just e))       = "var" <+> pretty p <> valSig t <+> "with" <+> pretty e
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
@@ -143,6 +143,7 @@
                    | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Pattern a, _valExpression :: Expression a }
                    | StaVal [Universal a] String (Type a)
                    | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (Expression a), prValType :: Maybe (Type a) }
+                   | PrVar { prvarPat :: Pattern a, _prVarExpr :: Maybe (Expression a), prVarType :: Maybe (Type a) }
                    | Var { varT :: Maybe (Type a), varPat :: Pattern a, _varExpr1 :: Maybe (Expression a), _varExpr2 :: Maybe (Expression a) }
                    | AndDecl { andT :: Maybe (Type a), andPat :: Pattern a, _andExpr :: Expression a }
                    | Include String
@@ -515,7 +516,7 @@
                   | TupleEx a [Expression a]
                   | BoxTupleEx a [Expression a]
                   | While a (Expression a) (Expression a)
-                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) -- ^ A @while@ loop that is guaranteed to terminate.
+                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Maybe [Arg a]) -- ^ A @while@ loop that is guaranteed to terminate.
                   | For a (Expression a) (Expression a)
                   | ForStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) -- ^ A @for@ loop that is guaranteed to terminate.
                   | Actions (ATS a)
@@ -560,7 +561,7 @@
                      | TupleExF a [x]
                      | BoxTupleExF a [x]
                      | WhileF a x x
-                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x
+                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x (Maybe [Arg a])
                      | ForF a x x
                      | ForStarF a [Universal a] (StaticExpression a) [Arg a] x x
                      | ActionsF (ATS a)
@@ -577,94 +578,94 @@
 type instance Base (Expression a) = ExpressionF a
 
 instance Recursive (Expression a) where
-    project (Let l ds me)              = LetF l ds me
-    project (VoidLiteral l)            = VoidLiteralF l
-    project (Call n is us mps as)      = CallF n is us mps as
-    project (NamedVal n)               = NamedValF n
-    project (ListLiteral l s t es)     = ListLiteralF l s t es
-    project (If e e' me)               = IfF e e' me
-    project (UintLit u)                = UintLitF u
-    project (FloatLit f)               = FloatLitF f
-    project (IntLit i)                 = IntLitF i
-    project (HexLit s)                 = HexLitF s
-    project (UnderscoreLit l)          = UnderscoreLitF l
-    project (Lambda l lt p e)          = LambdaF l lt p e
-    project (LinearLambda l lt p e)    = LinearLambdaF l lt p e
-    project (Index l n e)              = IndexF l n e
-    project (Access l e n)             = AccessF l e n
-    project (StringLit s)              = StringLitF s
-    project (CharLit c)                = CharLitF c
-    project (AddrAt l e)               = AddrAtF l e
-    project (ViewAt l e)               = ViewAtF l e
-    project (Binary op e e')           = BinaryF op e e'
-    project (Unary op e)               = UnaryF op e
-    project (IfCase l arms)            = IfCaseF l arms
-    project (Case l k e arms)          = CaseF l k e arms
-    project (RecordValue l recs mty)   = RecordValueF l recs mty
-    project (Precede e e')             = PrecedeF e e'
-    project (ProofExpr a e e')         = ProofExprF a e e'
-    project (TypeSignature e ty)       = TypeSignatureF e ty
-    project (WhereExp e ds)            = WhereExpF e ds
-    project (TupleEx l es)             = TupleExF l es
-    project (BoxTupleEx l es)          = BoxTupleExF l es
-    project (While l e e')             = WhileF l e e'
-    project (WhileStar l us t as e e') = WhileStarF l us t as e e'
-    project (For l e e')               = ForF l e e'
-    project (ForStar l us t as e e')   = ForStarF l us t as e e'
-    project (Actions ds)               = ActionsF ds
-    project (Begin l e)                = BeginF l e
-    project (BinList op es)            = BinListF op es
-    project (PrecedeList es)           = PrecedeListF es
-    project (FixAt a s sfun)           = FixAtF a s sfun
-    project (LambdaAt a sfun)          = LambdaAtF a sfun
-    project (ParenExpr l e)            = ParenExprF l e
-    project (CommentExpr s e)          = CommentExprF s e
-    project (MacroVar l s)             = MacroVarF l s
+    project (Let l ds me)                 = LetF l ds me
+    project (VoidLiteral l)               = VoidLiteralF l
+    project (Call n is us mps as)         = CallF n is us mps as
+    project (NamedVal n)                  = NamedValF n
+    project (ListLiteral l s t es)        = ListLiteralF l s t es
+    project (If e e' me)                  = IfF e e' me
+    project (UintLit u)                   = UintLitF u
+    project (FloatLit f)                  = FloatLitF f
+    project (IntLit i)                    = IntLitF i
+    project (HexLit s)                    = HexLitF s
+    project (UnderscoreLit l)             = UnderscoreLitF l
+    project (Lambda l lt p e)             = LambdaF l lt p e
+    project (LinearLambda l lt p e)       = LinearLambdaF l lt p e
+    project (Index l n e)                 = IndexF l n e
+    project (Access l e n)                = AccessF l e n
+    project (StringLit s)                 = StringLitF s
+    project (CharLit c)                   = CharLitF c
+    project (AddrAt l e)                  = AddrAtF l e
+    project (ViewAt l e)                  = ViewAtF l e
+    project (Binary op e e')              = BinaryF op e e'
+    project (Unary op e)                  = UnaryF op e
+    project (IfCase l arms)               = IfCaseF l arms
+    project (Case l k e arms)             = CaseF l k e arms
+    project (RecordValue l recs mty)      = RecordValueF l recs mty
+    project (Precede e e')                = PrecedeF e e'
+    project (ProofExpr a e e')            = ProofExprF a e e'
+    project (TypeSignature e ty)          = TypeSignatureF e ty
+    project (WhereExp e ds)               = WhereExpF e ds
+    project (TupleEx l es)                = TupleExF l es
+    project (BoxTupleEx l es)             = BoxTupleExF l es
+    project (While l e e')                = WhileF l e e'
+    project (WhileStar l us t as e e' ty) = WhileStarF l us t as e e' ty
+    project (For l e e')                  = ForF l e e'
+    project (ForStar l us t as e e')      = ForStarF l us t as e e'
+    project (Actions ds)                  = ActionsF ds
+    project (Begin l e)                   = BeginF l e
+    project (BinList op es)               = BinListF op es
+    project (PrecedeList es)              = PrecedeListF es
+    project (FixAt a s sfun)              = FixAtF a s sfun
+    project (LambdaAt a sfun)             = LambdaAtF a sfun
+    project (ParenExpr l e)               = ParenExprF l e
+    project (CommentExpr s e)             = CommentExprF s e
+    project (MacroVar l s)                = MacroVarF l s
 
 instance Corecursive (Expression a) where
-    embed (LetF l ds me)              = Let l ds me
-    embed (VoidLiteralF l)            = VoidLiteral l
-    embed (CallF n is us mps as)      = Call n is us mps as
-    embed (NamedValF n)               = NamedVal n
-    embed (ListLiteralF l s t es)     = ListLiteral l s t es
-    embed (IfF e e' me)               = If e e' me
-    embed (UintLitF u)                = UintLit u
-    embed (IntLitF i)                 = IntLit i
-    embed (FloatLitF f)               = FloatLit f
-    embed (HexLitF s)                 = HexLit s
-    embed (UnderscoreLitF l)          = UnderscoreLit l
-    embed (LambdaF l lt p e)          = Lambda l lt p e
-    embed (LinearLambdaF l lt p e)    = LinearLambda l lt p e
-    embed (IndexF l n e)              = Index l n e
-    embed (AccessF l n e)             = Access l n e
-    embed (StringLitF s)              = StringLit s
-    embed (CharLitF c)                = CharLit c
-    embed (AddrAtF l e)               = AddrAt l e
-    embed (ViewAtF l e)               = ViewAt l e
-    embed (BinaryF op e e')           = Binary op e e'
-    embed (UnaryF op e)               = Unary op e
-    embed (IfCaseF l arms)            = IfCase l arms
-    embed (CaseF l k e arms)          = Case l k e arms
-    embed (RecordValueF l recs mty)   = RecordValue l recs mty
-    embed (PrecedeF e e')             = Precede e e'
-    embed (ProofExprF a e e')         = ProofExpr a e e'
-    embed (TypeSignatureF e ty)       = TypeSignature e ty
-    embed (WhereExpF e ds)            = WhereExp e ds
-    embed (TupleExF l es)             = TupleEx l es
-    embed (BoxTupleExF l es)          = BoxTupleEx l es
-    embed (WhileF l e e')             = While l e e'
-    embed (WhileStarF l us t as e e') = WhileStar l us t as e e'
-    embed (ForF l e e')               = For l e e'
-    embed (ForStarF l us t as e e')   = ForStar l us t as e e'
-    embed (ActionsF ds)               = Actions ds
-    embed (BeginF l e)                = Begin l e
-    embed (BinListF op es)            = BinList op es
-    embed (PrecedeListF es)           = PrecedeList es
-    embed (FixAtF a s sfun)           = FixAt a s sfun
-    embed (LambdaAtF a sfun)          = LambdaAt a sfun
-    embed (ParenExprF l e)            = ParenExpr l e
-    embed (CommentExprF s e)          = CommentExpr s e
-    embed (MacroVarF l s)             = MacroVar l s
+    embed (LetF l ds me)                 = Let l ds me
+    embed (VoidLiteralF l)               = VoidLiteral l
+    embed (CallF n is us mps as)         = Call n is us mps as
+    embed (NamedValF n)                  = NamedVal n
+    embed (ListLiteralF l s t es)        = ListLiteral l s t es
+    embed (IfF e e' me)                  = If e e' me
+    embed (UintLitF u)                   = UintLit u
+    embed (IntLitF i)                    = IntLit i
+    embed (FloatLitF f)                  = FloatLit f
+    embed (HexLitF s)                    = HexLit s
+    embed (UnderscoreLitF l)             = UnderscoreLit l
+    embed (LambdaF l lt p e)             = Lambda l lt p e
+    embed (LinearLambdaF l lt p e)       = LinearLambda l lt p e
+    embed (IndexF l n e)                 = Index l n e
+    embed (AccessF l n e)                = Access l n e
+    embed (StringLitF s)                 = StringLit s
+    embed (CharLitF c)                   = CharLit c
+    embed (AddrAtF l e)                  = AddrAt l e
+    embed (ViewAtF l e)                  = ViewAt l e
+    embed (BinaryF op e e')              = Binary op e e'
+    embed (UnaryF op e)                  = Unary op e
+    embed (IfCaseF l arms)               = IfCase l arms
+    embed (CaseF l k e arms)             = Case l k e arms
+    embed (RecordValueF l recs mty)      = RecordValue l recs mty
+    embed (PrecedeF e e')                = Precede e e'
+    embed (ProofExprF a e e')            = ProofExpr a e e'
+    embed (TypeSignatureF e ty)          = TypeSignature e ty
+    embed (WhereExpF e ds)               = WhereExp e ds
+    embed (TupleExF l es)                = TupleEx l es
+    embed (BoxTupleExF l es)             = BoxTupleEx l es
+    embed (WhileF l e e')                = While l e e'
+    embed (WhileStarF l us t as e e' ty) = WhileStar l us t as e e' ty
+    embed (ForF l e e')                  = For l e e'
+    embed (ForStarF l us t as e e')      = ForStar l us t as e e'
+    embed (ActionsF ds)                  = Actions ds
+    embed (BeginF l e)                   = Begin l e
+    embed (BinListF op es)               = BinList op es
+    embed (PrecedeListF es)              = PrecedeList es
+    embed (FixAtF a s sfun)              = FixAt a s sfun
+    embed (LambdaAtF a sfun)             = LambdaAt a sfun
+    embed (ParenExprF l e)               = ParenExpr l e
+    embed (CommentExprF s e)             = CommentExpr s e
+    embed (MacroVarF l s)                = MacroVar l s
 
 -- | An 'implement' or 'primplmnt' declaration
 data Implementation a = Implement { pos            :: a
diff --git a/test/data/concurrency.out b/test/data/concurrency.out
--- a/test/data/concurrency.out
+++ b/test/data/concurrency.out
@@ -212,7 +212,7 @@
     val+ CHANNEL{l0,l1,l2,l3}(ch) = chan
     val mutex = unsafe_mutex_vt2t(ch.mutex)
     val (prf | ()) = mutex_lock(mutex)
-    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))
+    val xs = $UN.castvwtp0{queue(a)}(prf | ch.queue)
     val () = channel_insert_helper<a>(chan, xs, x)
     prval prf = $UN.castview0{locked_v(l1)}(xs)
     val () = mutex_unlock(prf | mutex)
@@ -223,7 +223,7 @@
   { val+ CHANNEL{l0,l1,l2,l3}(ch) = chan
     val mutex = unsafe_mutex_vt2t(ch.mutex)
     val (prf | ()) = mutex_lock(mutex)
-    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))
+    val xs = $UN.castvwtp0{queue(a)}(prf | ch.queue)
     val x = channel_remove_helper<a>(chan, xs)
     prval prf = $UN.castview0{locked_v(l1)}(xs)
     val () = mutex_unlock(prf | mutex) }
diff --git a/test/data/levenshtein.out b/test/data/levenshtein.out
--- a/test/data/levenshtein.out
+++ b/test/data/levenshtein.out
@@ -18,7 +18,7 @@
     
     val () = loop1(sz2i(s1_l))
     val () = while* {i:nat}  .<i>. (i : int(i)) =>
-        ((i > 0))
+        (i > 0)
         (column[i] := i ; i := i - 1)
     val () = while(i > 0)(column[i] := i ; i := i - 1)
     val () = for* { i : nat | i <= m }  .<i>. (i : int(i)) =>
diff --git a/test/data/levenshtein2.dats b/test/data/levenshtein2.dats
new file mode 100644
--- /dev/null
+++ b/test/data/levenshtein2.dats
@@ -0,0 +1,124 @@
+staload UN = "prelude/SATS/unsafe.sats"
+
+// Ported over from https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C
+fn min_3(x : int, y : int, z : int) : int =
+  min(x, (min(y, z)))
+
+fn bool2int(c0 : char, c1 : char) : int =
+  if c0 = c1 then
+    0
+  else
+    1
+
+fn levenshtein {m:nat}{n:nat}(s1 : string(m), s2 : string(n)) : int =
+  let
+    val s1_l: size_t(m) = length(s1)
+    val s2_l: size_t(n) = length(s2)
+    
+    fun loop1() : arrayref(int, m+1) =
+      let
+        val (pf_arr, pf_gc | p_arr) = array_ptr_alloc<int>(succ(s1_l))
+        
+        //
+        val p1_arr = ptr1_succ<int>(p_arr)
+        prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr)
+        val () = ptr_set<int>(pf1_at | p_arr, 0)
+        
+        //
+        var i: int = 0
+        prval [larr:addr]EQADDR () = eqaddr_make_ptr(p1_arr)
+        var p = p1_arr
+        
+        prvar pf0 = array_v_nil{int}(())
+        
+        prvar pf1 = pf_arr
+        
+        //
+        val () = while* { i : nat | i <= m }  .<m-i>. ( i : int(i)
+                                                      , p : ptr(larr+i*sizeof(int))
+                                                      , pf0 : array_v(int, larr, i)
+                                                      , pf1 : array_v(int?, larr+i*sizeof(int), m-i)
+                                                      ) : ( pf0 : array_v(int, larr, m)
+                                                          , pf1 : array_v(int?, larr+i*sizeof(int), 0)
+                                                          ) =>
+            (i < sz2i(s1_l))
+            {
+              //
+              prval (pf_at, pf1_res) = array_v_uncons{int?}(pf1)
+              prval () = pf1 := pf1_res
+              
+              //
+              val c = g0ofg1(i)
+              val () = ptr_set<int>(pf_at | p, c)
+              val () = p := ptr1_succ<int>(p)
+              
+              //
+              prval () = pf0 := array_v_extend{int}(pf0, pf_at)
+              val () = i := i + 1
+              
+              //
+            }
+        
+        // end of [val]
+        //
+        prval () = pf_arr := pf0
+        prval () = array_v_unnil{int?}(pf1)
+        prval pf_arr = array_v_cons{int}(pf1_at, pf_arr)
+        
+        //
+        val res = arrayptr_encode(pf_arr, pf_gc | p_arr)
+      in
+        arrayptr_refize(res)
+      end
+    
+    val column = loop1(())
+    
+    fun loop2 { i : nat | i > 0 && i <= n+1 } .<n-i+1>. (x : int(i)) :
+      void =
+      if x <= sz2i(s2_l) then
+        {
+          val () = column[0] := x
+          val () = let
+            fun inner_loop { j : nat | j > 0 && j <= m+1 } .<m-j+1>. ( y : int(j)
+                                                                     , last_diag : int
+                                                                     ) : void =
+              if y <= sz2i(s1_l) then
+                let
+                  var old_diag = column[y]
+                  val () = column[y] := min_3( column[y] + 1
+                                             , column[y - 1] + 1
+                                             , last_diag + bool2int(s1[y - 1], s2[x - 1])
+                                             )
+                in
+                  inner_loop(y + 1, old_diag)
+                end
+          in
+            inner_loop(1, x - 1)
+          end
+          val () = loop2(x + 1)
+        }
+    
+    val () = loop2(1)
+  in
+    column[s1_l]
+  end
+
+fn levenshtein_(s1 : string, s2 : string) : int =
+  let
+    fn witness(s : string) : [m:nat] string(m) =
+      $UN.cast(s)
+  in
+    levenshtein(witness(s1), witness(s2))
+  end
+
+fn levenshtein_vt {m:nat}{n:nat}(s1 : !strnptr(m), s2 : !strnptr(n)) :
+  int =
+  let
+    var p1 = strnptr2ptr(s1)
+    var p2 = strnptr2ptr(s2)
+    var s1 = $UN.ptr0_get<string(m)>(p1)
+    var s2 = $UN.ptr0_get<string(n)>(p2)
+  in
+    levenshtein(s1, s2)
+  end
+
diff --git a/test/data/levenshtein2.out b/test/data/levenshtein2.out
new file mode 100644
--- /dev/null
+++ b/test/data/levenshtein2.out
@@ -0,0 +1,121 @@
+staload UN = "prelude/SATS/unsafe.sats"
+
+// Ported over from https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C
+fn min_3(x : int, y : int, z : int) : int =
+  min(x, (min(y, z)))
+
+fn bool2int(c0 : char, c1 : char) : int =
+  if c0 = c1 then
+    0
+  else
+    1
+
+fn levenshtein {m:nat}{n:nat}(s1 : string(m), s2 : string(n)) : int =
+  let
+    val s1_l: size_t(m) = length(s1)
+    val s2_l: size_t(n) = length(s2)
+    
+    fun loop1() : arrayref(int, m+1) =
+      let
+        val (pf_arr, pf_gc | p_arr) = array_ptr_alloc<int>(succ(s1_l))
+        
+        //
+        val p1_arr = ptr1_succ<int>(p_arr)
+        prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr)
+        val () = ptr_set<int>(pf1_at | p_arr, 0)
+        
+        //
+        var i: int = 0
+        prval [larr:addr]EQADDR () = eqaddr_make_ptr(p1_arr)
+        var p = p1_arr
+        prvar pf0 = array_v_nil{int}()
+        prvar pf1 = pf_arr
+        
+        //
+        val () = while* { i : nat | i <= m }  .<m-i>. ( i : int(i)
+                                                      , p : ptr(larr+i*sizeof(int))
+                                                      , pf0 : array_v(int, larr, i)
+                                                      , pf1 : array_v(int?, larr+i*sizeof(int), m-i)
+                                                      ) : ( pf0 : array_v(int, larr, m)
+                                                          , pf1 : array_v(int?, larr+i*sizeof(int), 0)
+                                                          ) =>
+            (i < sz2i(s1_l))
+            {
+              //
+              prval (pf_at, pf1_res) = array_v_uncons{int?}(pf1)
+              prval () = pf1 := pf1_res
+              
+              //
+              val c = g0ofg1(i)
+              val () = ptr_set<int>(pf_at | p, c)
+              val () = p := ptr1_succ<int>(p)
+              
+              //
+              prval () = pf0 := array_v_extend{int}(pf0, pf_at)
+              val () = i := i + 1
+              
+              //
+            }
+        
+        // end of [val]
+        //
+        prval () = pf_arr := pf0
+        prval () = array_v_unnil{int?}(pf1)
+        prval pf_arr = array_v_cons{int}(pf1_at, pf_arr)
+        
+        //
+        val res = arrayptr_encode(pf_arr, pf_gc | p_arr)
+      in
+        arrayptr_refize(res)
+      end
+    
+    val column = loop1(())
+    
+    fun loop2 { i : nat | i > 0 && i <= n+1 } .<n-i+1>. (x : int(i)) :
+      void =
+      if x <= sz2i(s2_l) then
+        {
+          val () = column[0] := x
+          val () = let
+            fun inner_loop { j : nat | j > 0 && j <= m+1 } .<m-j+1>. ( y : int(j)
+                                                                     , last_diag : int
+                                                                     ) : void =
+              if y <= sz2i(s1_l) then
+                let
+                  var old_diag = column[y]
+                  val () = column[y] := min_3( column[y] + 1
+                                             , column[y - 1] + 1
+                                             , last_diag + bool2int(s1[y - 1], s2[x - 1])
+                                             )
+                in
+                  inner_loop(y + 1, old_diag)
+                end
+          in
+            inner_loop(1, x - 1)
+          end
+          val () = loop2(x + 1)
+        }
+    
+    val () = loop2(1)
+  in
+    column[s1_l]
+  end
+
+fn levenshtein_(s1 : string, s2 : string) : int =
+  let
+    fn witness(s : string) : [m:nat] string(m) =
+      $UN.cast(s)
+  in
+    levenshtein(witness(s1), witness(s2))
+  end
+
+fn levenshtein_vt {m:nat}{n:nat}(s1 : !strnptr(m), s2 : !strnptr(n)) :
+  int =
+  let
+    var p1 = strnptr2ptr(s1)
+    var p2 = strnptr2ptr(s2)
+    var s1 = $UN.ptr0_get<string(m)>(p1)
+    var s2 = $UN.ptr0_get<string(n)>(p2)
+  in
+    levenshtein(s1, s2)
+  end