diff --git a/src/boot/lib/mexpr.ml b/src/boot/lib/mexpr.ml
index e8dbd08f9..1838fbede 100644
--- a/src/boot/lib/mexpr.ml
+++ b/src/boot/lib/mexpr.ml
@@ -467,12 +467,38 @@ let getData = function
       (idDeclRecLets, fis, [len], tys, tms, strs, [], [], [], [], [], [])
   | PTreeTop (TopCon (Con (fi, str, ty))) ->
       (idDeclConDef, [fi], [], [ty], [], [str], [], [], [], [], [], [])
-  | PTreeTop (TopUtest (Utest (fi, tm1, tm2, tmUsing, _))) -> (
-    match tmUsing with
-    | Some tm ->
-        (idDeclUtest, [fi], [1], [], [tm1; tm2; tm], [], [], [], [], [], [], [])
-    | _ ->
-        (idDeclUtest, [fi], [0], [], [tm1; tm2], [], [], [], [], [], [], []) )
+  | PTreeTop (TopUtest (Utest (fi, tm1, tm2, tmUsing, tmOnFail))) -> (
+    match (tmUsing, tmOnFail) with
+    | None, None ->
+        (idDeclUtest, [fi], [2], [], [tm1; tm2], [], [], [], [], [], [], [])
+    | Some tmUsing, None ->
+        ( idDeclUtest
+        , [fi]
+        , [3]
+        , []
+        , [tm1; tm2; tmUsing]
+        , []
+        , []
+        , []
+        , []
+        , []
+        , []
+        , [] )
+    | Some tmUsing, Some tmOnFail ->
+        ( idDeclUtest
+        , [fi]
+        , [4]
+        , []
+        , [tm1; tm2; tmUsing; tmOnFail]
+        , []
+        , []
+        , []
+        , []
+        , []
+        , []
+        , [] )
+    | _, _ ->
+        failwith "bootparser getData undefined" )
   | PTreeTop (TopExt (Ext (fi, str, effect, ty))) ->
       ( idDeclExt
       , [fi]
diff --git a/stdlib/json.mc b/stdlib/json.mc
index f759b3a0a..458f8f30b 100644
--- a/stdlib/json.mc
+++ b/stdlib/json.mc
@@ -296,7 +296,7 @@ recursive let json2string: JsonValue -> String = lam value.
         concat acc "\\b"
       else if eqi cval 12 then
         concat acc "\\f"
-      else if or (lti cval 20) (eqi cval 127) then
+      else if or (lti cval 32) (eqi cval 127) then
         let tohex: Int -> Char = lam x.
           if lti x 10 then
             int2char (addi x (char2int '0'))
diff --git a/stdlib/mexpr/ast.mc b/stdlib/mexpr/ast.mc
index a0495b899..3f5b9e9f0 100644
--- a/stdlib/mexpr/ast.mc
+++ b/stdlib/mexpr/ast.mc
@@ -999,7 +999,7 @@ type PatName
 con PName : Name -> PatName
 con PWildcard : () -> PatName
 
-lang NamedPat = MatchAst
+lang NamedPat = Ast
   syn Pat =
   | PatNamed {ident : PatName,
               info : Info,
@@ -1018,7 +1018,7 @@ lang NamedPat = MatchAst
   | PatNamed r -> PatNamed {r with ty = ty}
 end
 
-lang SeqTotPat = MatchAst
+lang SeqTotPat = Ast
   syn Pat =
   | PatSeqTot {pats : [Pat],
                info : Info,
@@ -1043,7 +1043,7 @@ lang SeqTotPat = MatchAst
     else never
 end
 
-lang SeqEdgePat = MatchAst
+lang SeqEdgePat = Ast
   syn Pat =
   | PatSeqEdge {prefix : [Pat],
                 middle: PatName,
@@ -1072,7 +1072,7 @@ lang SeqEdgePat = MatchAst
     else never
 end
 
-lang RecordPat = MatchAst
+lang RecordPat = Ast
   syn Pat =
   | PatRecord {bindings : Map SID Pat,
                info: Info,
@@ -1097,7 +1097,7 @@ lang RecordPat = MatchAst
     else never
 end
 
-lang DataPat = MatchAst + DataAst
+lang DataPat = Ast + DataAst
   syn Pat =
   | PatCon {ident : Name,
             subpat : Pat,
@@ -1123,7 +1123,7 @@ lang DataPat = MatchAst + DataAst
     else never
 end
 
-lang IntPat = MatchAst + IntAst
+lang IntPat = Ast + IntAst
   syn Pat =
   | PatInt {val : Int,
             info : Info,
@@ -1142,7 +1142,7 @@ lang IntPat = MatchAst + IntAst
   | PatInt r -> PatInt {r with ty = ty}
 end
 
-lang CharPat = MatchAst
+lang CharPat = Ast
   syn Pat =
   | PatChar {val : Char,
              info : Info,
@@ -1161,7 +1161,7 @@ lang CharPat = MatchAst
   | PatChar r -> PatChar {r with ty = ty}
 end
 
-lang BoolPat = MatchAst + BoolAst
+lang BoolPat = Ast + BoolAst
   syn Pat =
   | PatBool {val : Bool,
              info : Info,
@@ -1180,7 +1180,7 @@ lang BoolPat = MatchAst + BoolAst
   | PatBool r -> PatBool {r with ty = ty}
 end
 
-lang AndPat = MatchAst
+lang AndPat = Ast
   syn Pat =
   | PatAnd {lpat : Pat,
             rpat : Pat,
@@ -1208,7 +1208,7 @@ lang AndPat = MatchAst
     else never
 end
 
-lang OrPat = MatchAst
+lang OrPat = Ast
   syn Pat =
   | PatOr {lpat : Pat,
            rpat : Pat,
@@ -1236,7 +1236,7 @@ lang OrPat = MatchAst
     else never
 end
 
-lang NotPat = MatchAst
+lang NotPat = Ast
   syn Pat =
   | PatNot {subpat : Pat,
             info : Info,
diff --git a/stdlib/mexpr/json-debug.mc b/stdlib/mexpr/json-debug.mc
new file mode 100644
index 000000000..52f1c5a55
--- /dev/null
+++ b/stdlib/mexpr/json-debug.mc
@@ -0,0 +1,670 @@
+-- This file supplies a set of functions for dumping MExpr ASTs to
+-- json, which can then be printed and examined in various other tools
+-- for exploring json values.
+
+include "json.mc"
+include "mexpr/pprint.mc"
+include "mexpr/ast.mc"
+include "mexpr/type.mc"
+include "mlang/ast.mc"
+
+lang AstToJson = Ast + DeclAst
+  sem exprToJson : Expr -> JsonValue
+  sem typeToJson : Type -> JsonValue
+  sem kindToJson : Kind -> JsonValue
+  sem patToJson : Pat -> JsonValue
+  sem declToJson : Decl -> JsonValue
+
+  sem optToNull : Option JsonValue -> JsonValue
+  sem optToNull =
+  | Some x -> x
+  | None _ -> JsonNull ()
+
+  sem nameToJson : Name -> JsonValue
+  sem nameToJson = | name ->
+    JsonArray [JsonString (nameGetStr name), optToNull (optionMap (lam x. JsonInt (sym2hash x)) (nameGetSym name))]
+
+  sem patNameToJson : PatName -> JsonValue
+  sem patNameToJson =
+  | PName n -> nameToJson n
+  | PWildcard _ -> JsonString "_"
+
+  sem infoToJson : Info -> JsonValue
+  sem infoToJson = | info -> JsonString (info2str info)
+
+  -- TODO(vipa, 2024-05-16): This is a temporary helper until
+  -- https://github.com/miking-lang/miking/issues/826 is implemented
+  sem exprAsDecl : Expr -> Option (Decl, Expr)
+  sem exprAsDecl =
+  | _ -> None ()
+end
+
+lang VarToJson = AstToJson + VarAst
+  sem exprToJson =
+  | TmVar x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmVar")
+    , ("ident", nameToJson x.ident)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    , ("frozen", JsonBool x.frozen)
+    ] )
+end
+
+lang AppToJson = AstToJson + AppAst
+  sem exprToJson =
+  | TmApp x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmApp")
+    , ("lhs", exprToJson x.lhs)
+    , ("rhs", exprToJson x.rhs)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang LamToJson = AstToJson + LamAst
+  sem exprToJson =
+  | TmLam x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmLam")
+    , ("ident", nameToJson x.ident)
+    , ("tyAnnot", typeToJson x.tyAnnot)
+    , ("tyParam", typeToJson x.tyParam)
+    , ("body", exprToJson x.body)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang DeclsToJson = AstToJson + LetAst + LetDeclAst + RecLetsAst + RecLetsDeclAst + TypeAst + TypeDeclAst + DataAst + DataDeclAst + UtestAst + UtestDeclAst + ExtAst + ExtDeclAst
+  sem exprAsDecl =
+  | TmLet x -> Some
+    ( DeclLet {ident = x.ident, tyAnnot = x.tyAnnot, tyBody = x.tyBody, body = x.body, info = x.info}
+    , x.inexpr
+    )
+  | TmRecLets x -> Some
+    ( DeclRecLets {info = x.info, bindings = x.bindings}
+    , x.inexpr
+    )
+  | TmType x -> Some
+    ( DeclType {ident = x.ident, params = x.params, tyIdent = x.tyIdent, info = x.info}
+    , x.inexpr
+    )
+  | TmConDef x -> Some
+    ( DeclConDef {ident = x.ident, tyIdent = x.tyIdent, info = x.info}
+    , x.inexpr
+    )
+  | TmUtest x -> Some
+    ( DeclUtest {test = x.test, expected = x.expected, tusing = x.tusing, tonfail = x.tonfail, info = x.info}
+    , x.next
+    )
+  | TmExt x -> Some
+    ( DeclExt {ident = x.ident, tyIdent = x.tyIdent, effect = x.effect, info = x.info}
+    , x.inexpr
+    )
+
+  sem exprToJson =
+  | tm & (TmLet _ | TmRecLets _ | TmType _ | TmConDef _ | TmUtest _ | TmExt _) ->
+    recursive let work = lam acc. lam expr.
+      match exprAsDecl expr with Some (decl, inexpr) then
+        work (snoc acc decl) inexpr
+      else (acc, expr) in
+    match work [] tm with (decls, inexpr) in
+    JsonObject (mapFromSeq cmpString
+      [ ("con", JsonString "TmDecl (merged)")
+      , ("decls", JsonArray (map declToJson decls))
+      , ("inexpr", exprToJson inexpr)
+      , ("ty", typeToJson (tyTm tm))
+      , ("info", infoToJson (infoTm tm))
+      ] )
+end
+
+lang ConstToJson = AstToJson + ConstAst + ConstPrettyPrint
+  sem exprToJson =
+  | TmConst x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmConst")
+    , ("const", JsonString (getConstStringCode 0 x.val))
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang SeqToJson = AstToJson + SeqAst
+  sem exprToJson =
+  | TmSeq x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmSeq")
+    , ("tms", JsonArray (map exprToJson x.tms))
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang RecordToJson = AstToJson + RecordAst
+  sem exprToJson =
+  | TmRecord x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmRecord")
+    , ("bindings", JsonObject
+      (mapFromSeq cmpString
+        (map (lam x. (sidToString x.0, exprToJson x.1))
+          (mapBindings x.bindings))))
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+  | TmRecordUpdate x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmRecordUpdate")
+    , ("rec", exprToJson x.rec)
+    , ("key", JsonString (sidToString x.key))
+    , ("value", exprToJson x.value)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang ConAppToJson = AstToJson + DataAst
+  sem exprToJson =
+  | TmConApp x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmConApp")
+    , ("ident", nameToJson x.ident)
+    , ("body", exprToJson x.body)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang MatchToJson = AstToJson + MatchAst
+  sem exprToJson =
+  | TmMatch x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmMatch")
+    , ("target", exprToJson x.target)
+    , ("pat", patToJson x.pat)
+    , ("thn", exprToJson x.thn)
+    , ("els", exprToJson x.els)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang NeverToJson = AstToJson + NeverAst
+  sem exprToJson =
+  | TmNever x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmNever")
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang NamedPatToJson = AstToJson + NamedPat
+  sem patToJson =
+  | PatNamed x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatNamed")
+    , ("ident", patNameToJson x.ident)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang SeqTotPatToJson = AstToJson + SeqTotPat
+  sem patToJson =
+  | PatSeqTot x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatSeqTot")
+    , ("pats", JsonArray (map patToJson x.pats))
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang SeqEdgePatToJson = AstToJson + SeqEdgePat
+  sem patToJson =
+  | PatSeqEdge x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatSeqEdge")
+    , ("prefix", JsonArray (map patToJson x.prefix))
+    , ("middle", patNameToJson x.middle)
+    , ("postfix", JsonArray (map patToJson x.postfix))
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang RecordPatToJson = AstToJson + RecordPat
+  sem patToJson =
+  | PatRecord x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatRecord")
+    , ("bindings", JsonObject
+      (mapFromSeq cmpString
+        (map (lam x. (sidToString x.0, patToJson x.1))
+          (mapBindings x.bindings))))
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang DataPatToJson = AstToJson + DataPat
+  sem patToJson =
+  | PatCon x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatCon")
+    , ("ident", nameToJson x.ident)
+    , ("subpat", patToJson x.subpat)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang IntPatToJson = AstToJson + IntPat
+  sem patToJson =
+  | PatInt x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatInt")
+    , ("val", JsonInt x.val)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang CharPatToJson = AstToJson + CharPat
+  sem patToJson =
+  | PatChar x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatChar")
+    , ("val", JsonString [x.val])
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang BoolPatToJson = AstToJson + BoolPat
+  sem patToJson =
+  | PatBool x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatBool")
+    , ("val", JsonBool x.val)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang AndPatToJson = AstToJson + AndPat
+  sem patToJson =
+  | PatAnd x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatAnd")
+    , ("lpat", patToJson x.lpat)
+    , ("rpat", patToJson x.rpat)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang OrPatToJson = AstToJson + OrPat
+  sem patToJson =
+  | PatOr x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatOr")
+    , ("lpat", patToJson x.lpat)
+    , ("rpat", patToJson x.rpat)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang NotPatToJson = AstToJson + NotPat
+  sem patToJson =
+  | PatNot x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "PatNot")
+    , ("subpat", patToJson x.subpat)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang UnknownTypeToJson = AstToJson + UnknownTypeAst
+  sem typeToJson =
+  | TyUnknown x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyUnknown")
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang BoolTypeToJson = AstToJson + BoolTypeAst
+  sem typeToJson =
+  | TyBool x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyBool")
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang IntTypeToJson = AstToJson + IntTypeAst
+  sem typeToJson =
+  | TyInt x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyInt")
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang FloatTypeToJson = AstToJson + FloatTypeAst
+  sem typeToJson =
+  | TyFloat x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyFloat")
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang CharTypeToJson = AstToJson + CharTypeAst
+  sem typeToJson =
+  | TyChar x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyChar")
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang FunTypeToJson = AstToJson + FunTypeAst
+  sem typeToJson =
+  | TyArrow x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyArrow")
+    , ("from", typeToJson x.from)
+    , ("to", typeToJson x.to)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang SeqTypeToJson = AstToJson + SeqTypeAst
+  sem typeToJson =
+  | TySeq x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TySeq")
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang TensorTypeToJson = AstToJson + TensorTypeAst
+  sem typeToJson =
+  | TyTensor x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyTensor")
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang RecordTypeToJson = AstToJson + RecordTypeAst
+  sem typeToJson =
+  | TyRecord x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyRecord")
+    , ("fields", JsonObject
+      (mapFromSeq cmpString
+        (map (lam x. (sidToString x.0, typeToJson x.1))
+          (mapBindings x.fields))))
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang VariantTypeToJson = AstToJson + VariantTypeAst
+  sem typeToJson =
+  | TyVariant x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyVariant")
+    , ("constrs", JsonArray
+      (map (lam x. JsonArray [nameToJson x.0, typeToJson x.1])
+        (mapBindings x.constrs)))
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang ConTypeToJson = AstToJson + ConTypeAst
+  sem typeToJson =
+  | TyCon x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyCon")
+    , ("ident", nameToJson x.ident)
+    , ("data", typeToJson x.data)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang DataTypeToJson = AstToJson + DataTypeAst
+  sem typeToJson =
+  | TyData x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyData")
+    , ("universe", JsonArray
+      (map (lam x. JsonArray [nameToJson x.0, JsonArray (map nameToJson (setToSeq x.1))])
+        (mapBindings x.universe)))
+    , ("positive", JsonBool x.positive)
+    , ("cons", JsonArray (map nameToJson (setToSeq x.cons)))
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang VarTypeToJson = AstToJson + VarTypeAst
+  sem typeToJson =
+  | TyVar x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyVar")
+    , ("ident", nameToJson x.ident)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang AllTypeToJson = AstToJson + AllTypeAst
+  sem typeToJson =
+  | TyAll x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyAll")
+    , ("ident", nameToJson x.ident)
+    , ("kind", kindToJson x.kind)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang AppTypeToJson = AstToJson + AppTypeAst
+  sem typeToJson =
+  | TyApp x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyApp")
+    , ("lhs", typeToJson x.lhs)
+    , ("rhs", typeToJson x.rhs)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang AliasTypeToJson = AstToJson + AliasTypeAst
+  sem typeToJson =
+  | TyAlias x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyAlias")
+    , ("display", typeToJson x.display)
+    , ("content", typeToJson x.content)
+    ] )
+end
+
+lang PolyKindToJson = AstToJson + PolyKindAst
+  sem kindToJson =
+  | Poly _ -> JsonString "Poly"
+end
+
+lang MonoKindToJson = AstToJson + MonoKindAst
+  sem kindToJson =
+  | Mono _ -> JsonString "Mono"
+end
+
+lang RecordKindToJson = AstToJson + RecordKindAst
+  sem kindToJson =
+  | Record x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "Record")
+    , ("bindings", JsonObject
+      (mapFromSeq cmpString
+        (map (lam x. (sidToString x.0, typeToJson x.1))
+          (mapBindings x.fields))))
+    ] )
+end
+
+lang DataKindToJson = AstToJson + DataKindAst
+  sem kindToJson =
+  | Data x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "Data")
+    , ("types",
+      let inner = lam r. JsonObject (mapFromSeq cmpString
+        [ ("lower", JsonArray (map nameToJson (setToSeq r.lower)))
+        , ("upper", optToNull
+          (optionMap (lam upper. JsonArray (map nameToJson (setToSeq upper)))
+            r.upper))
+        ] ) in
+      JsonArray (map (lam x. JsonArray [nameToJson x.0, inner x.1])
+        (mapBindings x.types)))
+    ] )
+end
+
+lang UseToJson = AstToJson + UseAst
+  -- TODO(vipa, 2024-05-17): This should probably actually be a Decl,
+  -- it's just not a good idea to do a `use` on the top-level right
+  -- now because of how includes work.
+  sem exprToJson =
+  | TmUse x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TmUse")
+    , ("ident", nameToJson x.ident)
+    , ("ty", typeToJson x.ty)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang LetToJson = LetDeclAst + AstToJson
+  sem declToJson =
+  | DeclLet x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "DeclLet")
+    , ("ident", nameToJson x.ident)
+    , ("tyAnnot", typeToJson x.tyAnnot)
+    , ("tyBody", typeToJson x.tyBody)
+    , ("body", exprToJson x.body)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+-- DeclType --
+lang TypeToJson = TypeDeclAst + AstToJson
+  sem declToJson =
+  | DeclType x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "DeclType")
+    , ("ident", nameToJson x.ident)
+    , ("params", JsonArray (map nameToJson x.params))
+    , ("tyIdent", typeToJson x.tyIdent)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+-- DeclRecLets --
+lang RecLetsToJson = RecLetsDeclAst + RecLetsAst + AstToJson
+  sem declToJson =
+  | DeclRecLets x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "DeclRecLets")
+    , ( "bindings"
+      , let bindingToJson = lam b. JsonObject (mapFromSeq cmpString
+          [ ("ident", nameToJson b.ident)
+          , ("tyAnnot", typeToJson b.tyAnnot)
+          , ("tyBody", typeToJson b.tyBody)
+          , ("body", exprToJson b.body)
+          , ("info", infoToJson b.info)
+          ] ) in
+        JsonArray (map bindingToJson x.bindings)
+      )
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+-- DeclConDef --
+lang DataToJson = DataDeclAst + AstToJson
+  sem declToJson =
+  | DeclConDef x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "DeclConDef")
+    , ("ident", nameToJson x.ident)
+    , ("tyIdent", typeToJson x.tyIdent)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+-- DeclUtest --
+lang UtestToJson = UtestDeclAst + AstToJson
+  sem declToJson =
+  | DeclUtest x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "DeclUtest")
+    , ("test", exprToJson x.test)
+    , ("expected", exprToJson x.expected)
+    , ("tusing", optToNull (optionMap exprToJson x.tusing))
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+-- DeclExt --
+lang ExtToJson = ExtDeclAst + AstToJson
+  sem declToJson =
+  | DeclExt x -> JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "DeclExt")
+    , ("ident", nameToJson x.ident)
+    , ("tyIdent", typeToJson x.tyIdent)
+    , ("effect", JsonBool x.effect)
+    , ("info", infoToJson x.info)
+    ] )
+end
+
+lang MetaVarToJson = AstToJson + MetaVarTypeAst
+  sem typeToJson =
+  | TyMetaVar x ->
+    let contents = switch deref x.contents
+      case Unbound u then
+        JsonObject (mapFromSeq cmpString
+          [ ("ident", nameToJson u.ident)
+          , ("level", JsonInt u.level)
+          , ("kind", kindToJson u.kind)
+          ])
+      case Link ty then
+        typeToJson ty
+      end in
+    JsonObject (mapFromSeq cmpString
+    [ ("con", JsonString "TyMetaVar")
+    , ("contents", contents)
+    ] )
+end
+
+lang MExprToJson
+  = VarToJson
+  + AppToJson
+  + LamToJson
+  + DeclsToJson
+  + ConstToJson
+  + SeqToJson
+  + RecordToJson
+  + ConAppToJson
+  + MatchToJson
+  + NeverToJson
+  + NamedPatToJson
+  + SeqTotPatToJson
+  + SeqEdgePatToJson
+  + RecordPatToJson
+  + DataPatToJson
+  + IntPatToJson
+  + CharPatToJson
+  + BoolPatToJson
+  + AndPatToJson
+  + OrPatToJson
+  + NotPatToJson
+  + UnknownTypeToJson
+  + BoolTypeToJson
+  + IntTypeToJson
+  + FloatTypeToJson
+  + CharTypeToJson
+  + FunTypeToJson
+  + SeqTypeToJson
+  + TensorTypeToJson
+  + RecordTypeToJson
+  + VariantTypeToJson
+  + ConTypeToJson
+  + DataTypeToJson
+  + VarTypeToJson
+  + AllTypeToJson
+  + AppTypeToJson
+  + AliasTypeToJson
+  + PolyKindToJson
+  + MonoKindToJson
+  + RecordKindToJson
+  + DataKindToJson
+  + UseToJson
+  + LetToJson
+  + TypeToJson
+  + RecLetsToJson
+  + DataToJson
+  + UtestToJson
+  + ExtToJson
+  + MetaVarToJson
+end
+
+mexpr
+
+use MExprToJson in
+
+utest json2string (exprToJson unit_) with "{\"ty\":{\"con\":\"TyRecord\",\"info\":\"<No file info>\",\"fields\":{}},\"con\":\"TmRecord\",\"info\":\"<No file info>\",\"bindings\":{}}" in
+
+()
diff --git a/stdlib/mexpr/type-check.mc b/stdlib/mexpr/type-check.mc
index 967c66fcc..9001eef59 100644
--- a/stdlib/mexpr/type-check.mc
+++ b/stdlib/mexpr/type-check.mc
@@ -973,7 +973,7 @@ lang VarTypeCheck = TypeCheck + VarAst
       errorSingle [t.info] msg
 end
 
-lang OpVarTypeCheck = TypeCheck + OpVarAst + RepTypesHelpers + SubstituteNewReprs + NeverAst + NamedPat + RecordPat + VarAst
+lang OpVarTypeCheck = TypeCheck + OpVarAst + RepTypesHelpers + SubstituteNewReprs + NeverAst + NamedPat + RecordPat + VarAst + MatchAst
   sem typeCheckExpr env =
   | TmOpVar x ->
     match mapLookup x.ident env.varEnv with Some ty then
diff --git a/stdlib/mlang/ast-builder.mc b/stdlib/mlang/ast-builder.mc
index 323f82f10..c78bc618f 100644
--- a/stdlib/mlang/ast-builder.mc
+++ b/stdlib/mlang/ast-builder.mc
@@ -234,13 +234,21 @@ let decl_ucondef_ = use MLangAst in
   decl_condef_ s tyunknown_
 
 
+let decl_utestuf_ = use MLangAst in
+  lam t. lam e. lam u. lam f.
+  DeclUtest {test = t, expected = e, tusing = Some u, tonfail = Some f, info = NoInfo ()}
+
 let decl_utestu_ = use MLangAst in
   lam t. lam e. lam u.
-  DeclUtest {test = t, expected = e, tusing = Some u, info = NoInfo ()}
+  DeclUtest {test = t, expected = e, tusing = Some u, tonfail = None (), info = NoInfo ()}
+
+let decl_utestf_ = use MLangAst in
+  lam t. lam e. lam f.
+  DeclUtest {test = t, expected = e, tusing = None (), tonfail = Some f, info = NoInfo ()}
 
 let decl_utest_ = use MLangAst in
   lam t. lam e.
-  DeclUtest {test = t, expected = e, tusing = None (), info = NoInfo ()}
+  DeclUtest {test = t, expected = e, tusing = None (), tonfail = None (), info = NoInfo ()}
 
 
 let decl_next_ = use MLangAst in
diff --git a/stdlib/mlang/ast.mc b/stdlib/mlang/ast.mc
index 3b861afcf..b6efda12e 100644
--- a/stdlib/mlang/ast.mc
+++ b/stdlib/mlang/ast.mc
@@ -167,6 +167,7 @@ lang UtestDeclAst = DeclAst
   | DeclUtest {test : Expr,
                expected : Expr,
                tusing : Option Expr,
+               tonfail : Option Expr,
                info : Info}
 
   sem infoDecl =
diff --git a/stdlib/mlang/boot-parser.mc b/stdlib/mlang/boot-parser.mc
index c1d5d893c..ea9d69a73 100644
--- a/stdlib/mlang/boot-parser.mc
+++ b/stdlib/mlang/boot-parser.mc
@@ -1,13 +1,13 @@
 -- This language fragment BootParserMLang allows you to parse
 -- files or strings into MLang programs.
 --
--- The parsing is done by calling the instrinsic functions 
+-- The parsing is done by calling the instrinsic functions
 -- `bootParserParseMLangFile` and `bootParserMlangString` whose functionality
--- is provided in boot. The result of a call to these intrinsics is the 
--- opaque type CBootParserTree. We use various intrinsics, such as 
+-- is provided in boot. The result of a call to these intrinsics is the
+-- opaque type CBootParserTree. We use various intrinsics, such as
 -- `bootParserGetDecl` or `bootParserGetInt`, to inspect terms of this type.
 --
--- BootParserMLang is built on top of the boot parser defined in 
+-- BootParserMLang is built on top of the boot parser defined in
 -- `stdlib/mexpr/boot-parser.mc`.
 
 include "ast.mc"
@@ -25,7 +25,7 @@ include "result.mc"
 
 lang BootParserMLang = BootParser + MLangAst
   sem parseMLangFile : all a. String -> Result a (Info, String) MLangProgram
-  sem parseMLangFile =| filepath -> 
+  sem parseMLangFile =| filepath ->
     let p = bootParserParseMLangFile filepath in
     if eqi (bootParserGetId p) 600 /- Error -/ then
       let n = glistlen p 0 in
@@ -47,25 +47,25 @@ lang BootParserMLang = BootParser + MLangAst
       result.ok (matchProgram p (bootParserGetId p))
 
   sem matchProgram : Unknown -> Int -> MLangProgram
-  sem matchProgram p = 
-  | 700 -> 
-    let nIncludes = bootParserGetListLength p 0 in 
-    let nTops = bootParserGetListLength p 1 in 
+  sem matchProgram p =
+  | 700 ->
+    let nIncludes = bootParserGetListLength p 0 in
+    let nTops = bootParserGetListLength p 1 in
 
-    let parseInclude = lam i. 
-      let inf = bootParserGetInfo p i in 
+    let parseInclude = lam i.
+      let inf = bootParserGetInfo p i in
       DeclInclude {path = bootParserGetString p i,
                    info = matchInfo inf (bootParserGetId inf)}
     in
-    let includes = map parseInclude (range 0 nIncludes 1) in 
+    let includes = map parseInclude (range 0 nIncludes 1) in
 
-    let parseDecl = lam i. 
-      let d = bootParserGetTop p i in 
+    let parseDecl = lam i.
+      let d = bootParserGetTop p i in
       matchTop d (bootParserGetId d)
     in
-    let decls = map parseDecl (range 0 nTops 1) in 
+    let decls = map parseDecl (range 0 nTops 1) in
 
-    let unparsedExpr = bootParserGetTerm p 0 in 
+    let unparsedExpr = bootParserGetTerm p 0 in
 
     {decls = concat includes decls,
      expr = matchTerm unparsedExpr (bootParserGetId unparsedExpr)}
@@ -74,54 +74,54 @@ lang BootParserMLang = BootParser + MLangAst
   -- + cases. This function merges sems into a single declaration.
   sem mergeSems : [Decl] -> [Decl]
   sem mergeSems =| decls ->
-    let work = lam acc : ([Decl], Map String Decl). lam decl : Decl. 
-      match acc with (res, m) in 
-      match decl with DeclSem s1 then 
-        let str = nameGetStr s1.ident in 
+    let work = lam acc : ([Decl], Map String Decl). lam decl : Decl.
+      match acc with (res, m) in
+      match decl with DeclSem s1 then
+        let str = nameGetStr s1.ident in
         match mapLookup str m with Some (DeclSem s2) then
           match s1.tyAnnot with TyUnknown _ then
-            let m = mapRemove str m in 
+            let m = mapRemove str m in
             (res, mapInsert str (DeclSem {s1 with tyAnnot = s2.tyAnnot}) m)
-          else 
-            let m = mapRemove str m in 
+          else
+            let m = mapRemove str m in
             (res, mapInsert str (DeclSem {s1 with args = s2.args, cases = s2.cases}) m)
-        else 
+        else
           (res, mapInsert str decl m)
-      else 
+      else
         (cons decl res, m)
-    in 
-    match foldl work ([], mapEmpty cmpString) decls with (res, m) in 
+    in
+    match foldl work ([], mapEmpty cmpString) decls with (res, m) in
     concat res (mapValues m)
 
 
   sem matchDecl : Unknown -> Int -> Decl
   sem matchDecl d =
-  | 702 -> 
-    let nCons = glistlen d 0 in 
-    let nParams = if eqi nCons 0 then 0 else glistlen d 1 in 
+  | 702 ->
+    let nCons = glistlen d 0 in
+    let nParams = if eqi nCons 0 then 0 else glistlen d 1 in
 
-    let parseCon = lam i. 
-      let ident = gname d (addi i 1) in 
-      let ty = gtype d i in 
+    let parseCon = lam i.
+      let ident = gname d (addi i 1) in
+      let ty = gtype d i in
       {ident = ident, tyIdent = ty}
-    in 
+    in
 
     DeclSyn {ident = gname d 0,
              includes = [],
              defs = map parseCon (range 0 nCons 1),
              params = map (lam i. gname d (addi (addi 1 nCons) i)) (range 0 nParams 1),
              info = ginfo d 0}
-  | 703 -> 
-    let nCases = glistlen d 0 in 
-    let nArgs = glistlen d 1 in 
-    let parseCase = lam i. 
+  | 703 ->
+    let nCases = glistlen d 0 in
+    let nArgs = glistlen d 1 in
+    let parseCase = lam i.
       {pat = gpat d i, thn = gterm d i}
-    in 
-    let parseArg = (lam i. {ident = gname d i, tyAnnot = gtype d i}) in 
+    in
+    let parseArg = (lam i. {ident = gname d i, tyAnnot = gtype d i}) in
 
-    let args = if eqi nArgs -1 then 
+    let args = if eqi nArgs -1 then
       None ()
-    else 
+    else
       Some (map (lam i. {ident = gname d i, tyAnnot = gtype d i}) (range 1 (addi 1 nArgs) 1))
     in
 
@@ -139,27 +139,27 @@ lang BootParserMLang = BootParser + MLangAst
               info = ginfo d 0}
 
   sem matchTop : Unknown -> Int -> Decl
-  sem matchTop d = 
-  | 701 -> 
-    let nIncludes = glistlen d 0 in 
-    let nDecls = glistlen d 1 in 
+  sem matchTop d =
+  | 701 ->
+    let nIncludes = glistlen d 0 in
+    let nDecls = glistlen d 1 in
 
-    let includes = map (gname d) (range 1 (addi nIncludes 1) 1) in 
+    let includes = map (gname d) (range 1 (addi nIncludes 1) 1) in
 
-    let parseDecl = lam i. 
-      let a = bootParserGetDecl d i in 
+    let parseDecl = lam i.
+      let a = bootParserGetDecl d i in
       matchDecl a (bootParserGetId a)
     in
 
-    let decls = map parseDecl (range 0 nDecls 1) in 
-    let decls = reverse (mergeSems decls) in 
+    let decls = map parseDecl (range 0 nDecls 1) in
+    let decls = reverse (mergeSems decls) in
 
 
     DeclLang {ident = gname d 0,
               info = ginfo d 0,
               includes = includes,
               decls = decls}
-  | 704 -> 
+  | 704 ->
     DeclLet {ident = gname d 0,
              tyAnnot = gtype d 0,
              tyBody = tyunknown_,
@@ -170,7 +170,7 @@ lang BootParserMLang = BootParser + MLangAst
               params = map (gname d) (range 1 (addi 1 (glistlen d 0)) 1),
               tyIdent = gtype d 0,
               info = ginfo d 0}
-  | 706 -> 
+  | 706 ->
     DeclRecLets {bindings =
                  create (glistlen d 0)
                         (lam n. {ident = gname d n,
@@ -179,29 +179,30 @@ lang BootParserMLang = BootParser + MLangAst
                                  body = gterm d n,
                                  info = ginfo d (addi n 1)}),
                  info = ginfo d 0}
-  | 707 -> 
+  | 707 ->
     DeclConDef {ident = gname d 0,
                 tyIdent = gtype d 0,
                 info = ginfo d 0}
-  | 708 -> 
+  | 708 ->
     DeclUtest {test = gterm d 0,
                expected = gterm d 1,
-               tusing = match glistlen d 0 with 0 then None () else Some (gterm d 2),
+               tusing = if geqi (glistlen d 0) 3 then Some (gterm d 2) else None (),
+               tonfail = if geqi (glistlen d 0) 4 then Some (gterm d 3) else None (),
                info = ginfo d 0}
-  | 709 -> 
+  | 709 ->
     DeclExt {ident = gname d 0,
              tyIdent = gtype d 0,
              effect = neqi (gint d 0) 0,
              info = ginfo d 0}
 
   sem matchTerm t =
-  | 116 -> 
+  | 116 ->
     TmUse {info = ginfo t 0,
            inexpr = gterm t 0,
            ty = tyunknown_,
            ident = gname t 0}
 
-  sem matchType t = 
+  sem matchType t =
   | 214 ->
     TyUse {ident = gname t 0,
            info = ginfo t 0,
@@ -209,18 +210,18 @@ lang BootParserMLang = BootParser + MLangAst
 end
 
 mexpr
-use BootParserMLang in 
-use MLangPrettyPrint in 
-use MExprEq in 
+use BootParserMLang in
+use MLangPrettyPrint in
+use MExprEq in
 
 let parseProgram = lam str.
   match result.consume (parseMLangString str) with (_, Right p) in p
 in
 
 let getIncludeStrings : MLangProgram -> [String] = lam p.
-  let decls = p.decls in 
-  mapOption 
-    (lam d. match d with DeclInclude r then Some r.path else None ()) 
+  let decls = p.decls in
+  mapOption
+    (lam d. match d with DeclInclude r then Some r.path else None ())
     decls
 in
 
@@ -233,11 +234,11 @@ let p = parseProgram str in
 utest getIncludeStrings p with ["foo.mc", "bar.mc", "baz.mc", "bar.mc"] using eqSeq eqString in
 
 -- Test expression is parsed
-utest match p.expr with TmVar {ident = ident} in ident with nameNoSym "x" using nameEqStr in 
+utest match p.expr with TmVar {ident = ident} in ident with nameNoSym "x" using nameEqStr in
 
 -- Test TypeDecl
-let str = "type Pair = (Int, Char)\nmexpr\n1" in 
-let p = parseProgram str in 
+let str = "type Pair = (Int, Char)\nmexpr\n1" in
+let p = parseProgram str in
 utest match head p.decls with DeclType {ident = ident} in ident with nameNoSym "Pair" using nameEqStr in
 
 -- Test Reclets
@@ -249,12 +250,12 @@ let str = strJoin "\n" [
   "mexpr",
   "isOdd 43"
 ] in
-let p = parseProgram str in 
-match head p.decls with DeclRecLets d in 
-utest map (lam b. nameGetStr b.ident) d.bindings with ["isOdd", "isEven"] using eqSeq eqString in 
+let p = parseProgram str in
+match head p.decls with DeclRecLets d in
+utest map (lam b. nameGetStr b.ident) d.bindings with ["isOdd", "isEven"] using eqSeq eqString in
 -- printLn (mlang2str p) ;
 
--- Test ConDef 
+-- Test ConDef
 let str = strJoin "\n" [
   "type Tree",
   "con Leaf: Int -> Tree",
@@ -268,14 +269,14 @@ let str = strJoin "\n" [
   "mexpr",
   "sum (Node (Leaf 10) (Leaf 20))"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 -- printLn (mlang2str p);
-match head p.decls with DeclType d in 
-utest d.ident with nameNoSym "Tree" using nameEqStr in 
-match get p.decls 1 with DeclConDef d in 
-utest d.ident with nameNoSym "Leaf" using nameEqStr in 
-match get p.decls 2 with DeclConDef d in 
-utest d.ident with nameNoSym "Node" using nameEqStr in 
+match head p.decls with DeclType d in
+utest d.ident with nameNoSym "Tree" using nameEqStr in
+match get p.decls 1 with DeclConDef d in
+utest d.ident with nameNoSym "Leaf" using nameEqStr in
+match get p.decls 2 with DeclConDef d in
+utest d.ident with nameNoSym "Node" using nameEqStr in
 -- printLn (mlang2str p) ;
 
 -- Test Utest
@@ -285,12 +286,12 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
-match head p.decls with DeclUtest d in 
-utest d.test with int_ 10 using eqExpr in 
+let p = parseProgram str in
+match head p.decls with DeclUtest d in
+utest d.test with int_ 10 using eqExpr in
 utest optionIsNone d.tusing with true in
-match get p.decls 1 with DeclUtest d in 
-utest d.test with int_ 12 using eqExpr in 
+match get p.decls 1 with DeclUtest d in
+utest d.test with int_ 12 using eqExpr in
 utest optionIsSome d.tusing with true in
 -- printLn (mlang2str p) ;
 
@@ -301,10 +302,10 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "L1" in
-utest length d.decls with 0 in 
+utest length d.decls with 0 in
 -- printLn (mlang2str p) ;
 
 -- Test language with syn definition
@@ -317,12 +318,12 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "IntArith" in
-match head d.decls with DeclSyn s in 
-utest nameGetStr s.ident with "Expr" in 
-utest nameGetStr (head s.defs).ident with "IntExpr" in 
+match head d.decls with DeclSyn s in
+utest nameGetStr s.ident with "Expr" in
+utest nameGetStr (head s.defs).ident with "IntExpr" in
 utest nameGetStr (get s.defs 1).ident with "AddExpr" in
 -- printLn (mlang2str p) ;
 
@@ -336,12 +337,12 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "AVLTreeImpl" in
-match head d.decls with DeclSyn s in 
-utest nameGetStr s.ident with "AVL" in 
-utest map nameGetStr s.params with ["k", "v"] using eqSeq eqString in 
+match head d.decls with DeclSyn s in
+utest nameGetStr s.ident with "AVL" in
+utest map nameGetStr s.params with ["k", "v"] using eqSeq eqString in
 
 
 -- Test syn with type parameters without constructors
@@ -352,11 +353,11 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "AVLTreeImpl" in
-match head d.decls with DeclSyn s in 
-utest nameGetStr s.ident with "AVL" in 
+match head d.decls with DeclSyn s in
+utest nameGetStr s.ident with "AVL" in
 -- TODO(voorberg, 08/05/2024): Figure out what the params are supposed to be
 -- in this case
 
@@ -370,13 +371,13 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "IntArith" in
-match head d.decls with DeclSem s in 
-utest nameGetStr s.ident with "f" in 
-utest (head s.cases).thn with int_ 0 using eqExpr in 
-utest (get s.cases 1).thn with int_ 1 using eqExpr in 
+match head d.decls with DeclSem s in
+utest nameGetStr s.ident with "f" in
+utest (head s.cases).thn with int_ 0 using eqExpr in
+utest (get s.cases 1).thn with int_ 1 using eqExpr in
 -- printLn (mlang2str p) ;
 
 -- Test language with semantic function
@@ -397,7 +398,7 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match get p.decls 3 with DeclLang d in
 utest nameGetStr d.ident with "L12" in
 utest d.includes with [nameNoSym "L1", nameNoSym "L2"] using eqSeq nameEqStr in
@@ -412,13 +413,13 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
-let p = parseProgram str in 
+let p = parseProgram str in
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "IntArith" in
-match head d.decls with DeclSem s in 
-utest nameGetStr s.ident with "f" in 
-utest optionMap (map (lam a. nameGetStr a.ident)) s.args with Some (["x", "y"]) using optionEq (eqSeq eqString) in 
+match head d.decls with DeclSem s in
+utest nameGetStr s.ident with "f" in
+utest optionMap (map (lam a. nameGetStr a.ident)) s.args with Some (["x", "y"]) using optionEq (eqSeq eqString) in
 -- printLn (mlang2str p) ;
 
 -- Test semantic function with type params
@@ -432,18 +433,18 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "IdLang" in
-match head d.decls with DeclSem s in 
-utest nameGetStr s.ident with "id" in 
-match s.tyAnnot with TyAll tyall in 
+match head d.decls with DeclSem s in
+utest nameGetStr s.ident with "id" in
+match s.tyAnnot with TyAll tyall in
 utest nameGetStr tyall.ident with "a" in
-match tyall.ty with TyArrow tyarrow in 
-match tyarrow.from with TyVar tyvar in 
-utest nameGetStr tyvar.ident with "a" in 
-match tyarrow.to with TyVar tyvar in 
-utest nameGetStr tyvar.ident with "a" in 
+match tyall.ty with TyArrow tyarrow in
+match tyarrow.from with TyVar tyvar in
+utest nameGetStr tyvar.ident with "a" in
+match tyarrow.to with TyVar tyvar in
+utest nameGetStr tyvar.ident with "a" in
 -- Test type declaratin in langauge
 let str = strJoin "\n" [
   "lang MyLang",
@@ -452,11 +453,11 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "MyLang" in
-match head d.decls with DeclType s in 
-utest nameGetStr s.ident with "Point" in 
+match head d.decls with DeclType s in
+utest nameGetStr s.ident with "Point" in
 -- printLn (mlang2str p) ;
 
 -- Test type declaration with params
@@ -467,22 +468,22 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 match head p.decls with DeclLang d in
 utest nameGetStr d.ident with "MyLang" in
-match head d.decls with DeclType s in 
-utest nameGetStr s.ident with "Point" in 
-utest map nameGetStr s.params with ["a", "b"] using eqSeq eqString in 
+match head d.decls with DeclType s in
+utest nameGetStr s.ident with "Point" in
+utest map nameGetStr s.params with ["a", "b"] using eqSeq eqString in
 
 let str = strJoin "\n" [
   "type Point a b = {x : Int, y : Int}",
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
-match head p.decls with DeclType s in 
-utest nameGetStr s.ident with "Point" in 
-utest map nameGetStr s.params with ["a", "b"] using eqSeq eqString in 
+let p = parseProgram str in
+match head p.decls with DeclType s in
+utest nameGetStr s.ident with "Point" in
+utest map nameGetStr s.params with ["a", "b"] using eqSeq eqString in
 
 -- Test TmUse parsing
 let str = strJoin "\n" [
@@ -491,9 +492,9 @@ let str = strJoin "\n" [
   "use L in",
   "()"
 ] in
-let p = parseProgram str in 
-match p.expr with TmUse u in 
-utest nameGetStr u.ident with "L" in 
+let p = parseProgram str in
+match p.expr with TmUse u in
+utest nameGetStr u.ident with "L" in
 
 -- Test TyUse parsing
 let str = strJoin "\n" [
@@ -505,7 +506,7 @@ let str = strJoin "\n" [
   "use L in",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 
 let str = strJoin "\n" [
   "lang L",
@@ -515,7 +516,7 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
+let p = parseProgram str in
 
 let str = strJoin "\n" [
   "lang L",
@@ -524,9 +525,9 @@ let str = strJoin "\n" [
   "mexpr",
   "()"
 ] in
-let p = parseProgram str in 
-match head p.decls with DeclLang l in 
-match head l.decls with DeclSem f in 
-match optionIsNone f.args with true in 
+let p = parseProgram str in
+match head p.decls with DeclLang l in
+match head l.decls with DeclSem f in
+match optionIsNone f.args with true in
 
 ()