diff --git a/Examples/Lean/BoogieLite.lean b/Examples/Lean/BoogieLite.lean
index 6251a297..82369181 100644
--- a/Examples/Lean/BoogieLite.lean
+++ b/Examples/Lean/BoogieLite.lean
@@ -60,6 +60,7 @@ def mkElabContext (ctx : DialectElabContext) (gctx : GlobalContext) (ictx : Pars
   globalContext := gctx
   inputContext := ictx
   syntaxElabs := ctx.syntaxElabMap
+  missingImport := false
 }
 
 end DialectElabContext
@@ -83,7 +84,7 @@ def ofExprImpl (elabGen : DialectElabContext) (ofExpr : Expr → OfAstM α) (ict
       | .error e => throw #[Lean.mkStringMessage ictx (stx.getPos?.getD 0) e]
       | .ok v => pure v
     else
-      throw <| s.errors.map (·.snd)
+      throw <| s.errors
 
 def ofTypeImpl (elabGen : DialectElabContext) (ofType : TypeExpr → OfAstM α) (ictx : InputContext) (tctx : Elab.TypingContext ) (stx : Lean.Syntax) : Except (Array Lean.Message) α := do
   let elabCtx : Elab.ElabContext := elabGen.mkElabContext tctx.globalContext ictx
@@ -94,7 +95,7 @@ def ofTypeImpl (elabGen : DialectElabContext) (ofType : TypeExpr → OfAstM α)
     | .error e => throw #[Lean.mkStringMessage ictx (stx.getPos?.getD 0) e]
     | .ok v => pure v
   else
-    throw <| s.errors.map (·.snd)
+    throw <| s.errors
 
 def format {α} [h : GenType α] (a : α) (ctx : GlobalContext := {}) (opts : FormatOptions := {}) (bindings : Array String := #[]) : String :=
   let fctx : FormatContext := .ofDialects h.dialectInfo.dialectMap ctx opts
@@ -126,7 +127,7 @@ def parse (α : Type) [h : GenType α] (leanEnv : Lean.Environment) (tctx : Elab
     GenType.ofArg inputCtx tctx stx
 
 def parseString (α : Type) [h : GenType α] (leanEnv : Lean.Environment) (contents : String) (tctx : Elab.TypingContext := default) : Except (Array Lean.Message) α := do
-  let ictx := Parser.stringInputContext contents
+  let ictx := Parser.stringInputContext "dummy" contents
   parse α leanEnv tctx ictx 0 contents.endPos
 
 end GenType
@@ -156,9 +157,27 @@ fn gt (x : Int, y : Int) : Bool => @[prec(20)] x " > " y;
 namespace Arith
 
 --set_option trace.Strata.generator true
--- set_option trace.Strata.DDM.syntax true
 #strata_gen Arith
---set_option trace.Strata.generator false
+
+/--
+info: inductive Strata.Arith.Expr : Type
+number of parameters: 0
+constructors:
+Strata.Arith.Expr.fvar : Nat → Expr
+Strata.Arith.Expr.btrue : Expr
+Strata.Arith.Expr.bfalse : Expr
+Strata.Arith.Expr.imp : Expr → Expr → Expr
+Strata.Arith.Expr.intLit : Nat → Expr
+Strata.Arith.Expr.add : Expr → Expr → Expr
+Strata.Arith.Expr.mul : Expr → Expr → Expr
+Strata.Arith.Expr.eq : ArithType → Expr → Expr → Expr
+Strata.Arith.Expr.le : Expr → Expr → Expr
+Strata.Arith.Expr.lt : Expr → Expr → Expr
+Strata.Arith.Expr.ge : Expr → Expr → Expr
+Strata.Arith.Expr.gt : Expr → Expr → Expr
+-/
+#guard_msgs in
+#print Expr
 
 
 def arithDialects : DialectMap := DialectMap.ofList! [initDialect, Arith]
diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean
index da73f17a..97dbe94f 100644
--- a/Strata/DDM/AST.lean
+++ b/Strata/DDM/AST.lean
@@ -34,7 +34,7 @@ instance : Quote QualifiedIdent where
   quote i := Syntax.mkCApp ``QualifiedIdent.mk #[quote i.dialect, quote i.name]
 
 @[macro quoteIdent] def quoteIdentImpl : Macro
-  | `(q`$l:ident ) =>
+  | `(q`$l:ident) =>
     if let .str (.str .anonymous d) suf := l.getId then
       pure (quote (QualifiedIdent.mk d suf) : Term)
     else
@@ -47,28 +47,28 @@ end QualifiedIdent
 
 #guard q`A.C = { dialect := "A", name := "C" }
 
-inductive SyntaxCat where
-| atom (ident : QualifiedIdent)
-| app (h : SyntaxCat) (a : SyntaxCat)
-deriving Inhabited, Repr, DecidableEq
+/--
+Denotes a fully specified syntax category in the Strata dialect.
+-/
+structure SyntaxCat where
+  name : QualifiedIdent
+  args : Array SyntaxCat
+deriving BEq, Inhabited, Repr
 
 namespace SyntaxCat
 
-protected def head : SyntaxCat → QualifiedIdent
-| .atom i => i
-| .app h _ => h.head
-
-protected def args : SyntaxCat → Array SyntaxCat
-| .atom _ => #[]
-| .app h a => h.args |>.push a
+def atom (ident : QualifiedIdent) : SyntaxCat where
+  name := ident
+  args := #[]
 
 /--
 Return true if this corresponds to builtin category `Init.Type`
 -/
-def isType (c : SyntaxCat) :=
-  match c with
-  | .atom q`Init.Type => true
-  | _ => false
+def isType (c : SyntaxCat) : Bool := c.name == q`Init.Type
+
+def sizeOf_spec (op : SyntaxCat) : sizeOf op = 1 + sizeOf op.name + sizeOf op.args :=
+  match op with
+  | { name, args } => by simp
 
 end SyntaxCat
 
@@ -109,28 +109,12 @@ termination_by e => e
 /-- Return true if type expression has no free variables. -/
 protected def isGround (tp : TypeExpr) := !tp.hasUnboundVar
 
-/-
-This applies global context to instantiate types and variables.
-
-Free type alias variables bound to alias
--/
-protected def instType (d : TypeExpr) (bindings : Array TypeExpr) : TypeExpr :=
-  match d with
-  | .ident i a =>
-    .ident i (a.attach.map (fun ⟨e, _⟩ => e.instType bindings))
-  | .bvar idx =>
-    assert! idx < bindings.size
-    bindings[bindings.size - (idx+1)]!
-  | .fvar idx a => .fvar idx (a.attach.map (fun ⟨e, _⟩ => e.instType bindings))
-  | .arrow a b => .arrow (a.instType bindings) (b.instType bindings)
-termination_by d
-
-/-
-This applies global context to instantiate types and variables.
+/--
+Applies a transformation to each bound variable in a type expression.
 
 Free type alias variables bound to alias
 -/
-protected def instTypeM [Monad m] (d : TypeExpr) (bindings : Nat → m TypeExpr) : m TypeExpr :=
+protected def instTypeM {m} [Monad m] (d : TypeExpr) (bindings : Nat → m TypeExpr) : m TypeExpr :=
   match d with
   | .ident i a =>
     .ident i <$> a.attach.mapM (fun ⟨e, _⟩ => e.instTypeM bindings)
@@ -364,7 +348,12 @@ deriving Repr, BEq
 
 namespace Metadata
 
-protected def empty : Metadata := { toArray := #[] }
+protected def emptyWithCapacity (c : Nat) : Metadata := { toArray := .emptyWithCapacity c }
+
+protected def empty : Metadata := .emptyWithCapacity 0
+
+protected def push (md : Metadata) (attr : MetadataAttr) : Metadata :=
+  .ofArray <| md.toArray.push attr
 
 instance : Inhabited Metadata where
   default := .empty
@@ -531,11 +520,6 @@ def toLevel : DebruijnIndex n → Fin n
 
 end DebruijnIndex
 
-private def varNameByIndex {n} (args : Vector Arg n) (idx : DebruijnIndex n) : String :=
-  match args[idx.toLevel] with
-  | .ident e => e
-  | a => panic! s!"Expected ident at {idx.val} {repr a}"
-
 /--
 This is the type information for an operator or function declaration.
 -/
@@ -569,22 +553,36 @@ structure ArgDecl where
   ident : Var
   kind : ArgDeclKind
   metadata : Metadata := .empty
-deriving Inhabited, Repr, BEq
+deriving BEq, Inhabited, Repr
 
-abbrev ArgDecls := Array ArgDecl
+structure ArgDecls where
+  ofArray ::
+  toArray : Array ArgDecl
+deriving BEq, Inhabited, Repr
 
 namespace ArgDecls
 
+protected def empty : ArgDecls := { toArray := #[] }
+
+protected def size (a : ArgDecls) : Nat := a.toArray.size
+
+protected def isEmpty (a : ArgDecls) : Bool := a.toArray.isEmpty
+
+instance : GetElem ArgDecls Nat ArgDecl fun a i => i < a.size where
+  getElem a i p := a.toArray[i]
+
+protected def foldl {α} (a : ArgDecls) (f : α → ArgDecl → α) (init : α): α  := a.toArray.foldl f init
+
 /-- Returns the index of the value in the binding for the given variable of the scope to use. -/
-def argScopeLevel (bindings : ArgDecls) (level : Fin bindings.size) : Option (Fin level.val) :=
-  match bindings[level].metadata.scopeIndex with
+def argScopeLevel (argDecls : ArgDecls) (level : Fin argDecls.size) : Option (Fin level.val) :=
+  match argDecls[level].metadata.scopeIndex with
   | none => none
   | some idx =>
     if h : idx < level.val then
       some ⟨level.val - (idx + 1), by omega⟩
     else
       -- TODO: Validate this is checked when attribute parsing occurs.
-      let varCount := bindings.size
+      let varCount := argDecls.size
       panic! s!"Scope index {idx} out of bounds ({level.val}, varCount = {varCount})"
 
 end ArgDecls
@@ -592,13 +590,13 @@ end ArgDecls
 /--
 Indices for introducing a new expression or operation.
 -/
-structure ValueBindingSpec (bindings : ArgDecls) where
+structure ValueBindingSpec (argDecls : ArgDecls) where
   -- deBrujin level of variable name.
-  nameIndex : DebruijnIndex bindings.size
+  nameIndex : DebruijnIndex argDecls.size
   -- deBrujin index of arguments if this is declaring a function (or none) if this declares a constant.
-  argsIndex : Option (DebruijnIndex bindings.size)
+  argsIndex : Option (DebruijnIndex argDecls.size)
   -- deBrujin index of type or a type/cat literal.
-  typeIndex : DebruijnIndex bindings.size
+  typeIndex : DebruijnIndex argDecls.size
   -- Whether categories are allowed
   allowCat : Bool
 deriving Repr
@@ -606,29 +604,26 @@ deriving Repr
 /--
 Indices for introducing a new type binding.
 -/
-structure TypeBindingSpec (bindings : ArgDecls) where
-  nameIndex : DebruijnIndex bindings.size
-  argsIndex : Option (DebruijnIndex bindings.size)
-  defIndex : Option (DebruijnIndex bindings.size)
+structure TypeBindingSpec (argDecls : ArgDecls) where
+  nameIndex : DebruijnIndex argDecls.size
+  argsIndex : Option (DebruijnIndex argDecls.size)
+  defIndex : Option (DebruijnIndex argDecls.size)
 deriving Repr
 
 /-
 A spec for introducing a new binding into a type context.
 -/
-inductive BindingSpec (bindings : ArgDecls) where
-| value (_ : ValueBindingSpec bindings)
-| type (_ : TypeBindingSpec bindings)
+inductive BindingSpec (argDecls : ArgDecls) where
+| value (_ : ValueBindingSpec argDecls)
+| type (_ : TypeBindingSpec argDecls)
 deriving Repr
 
 namespace BindingSpec
 
-def nameIndex : BindingSpec bindings → DebruijnIndex bindings.size
+def nameIndex {argDecls} : BindingSpec argDecls → DebruijnIndex argDecls.size
 | .value v => v.nameIndex
 | .type v => v.nameIndex
 
-def varName (b : BindingSpec bindings) (args : Vector Arg bindings.size) : String :=
-  varNameByIndex args b.nameIndex
-
 end BindingSpec
 
 abbrev NewBindingM := StateM (Array String)
@@ -665,39 +660,39 @@ private def mkValueBindingSpec
     newBindingErr "Arguments only allowed when result is a type."
   return { nameIndex, argsIndex, typeIndex, allowCat }
 
-def parseNewBindings (md : Metadata) (args : ArgDecls) : Array (BindingSpec args) × Array String :=
-  let ins (attr : MetadataAttr) : NewBindingM (Option (BindingSpec args)) := do
+def parseNewBindings (md : Metadata) (argDecls : ArgDecls) : Array (BindingSpec argDecls) × Array String :=
+  let ins (attr : MetadataAttr) : NewBindingM (Option (BindingSpec argDecls)) := do
         match attr.ident with
         | q`StrataDDL.declare => do
           let #[.catbvar nameIndex, .catbvar typeIndex] := attr.args
             | newBindingErr "declare does not have expected 2 arguments."; return none
-          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < args.size))
+          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < argDecls.size))
             | return panic! "Invalid name index"
-          let .isTrue typeP := inferInstanceAs (Decidable (typeIndex < args.size))
+          let .isTrue typeP := inferInstanceAs (Decidable (typeIndex < argDecls.size))
             | return panic! "Invalid name index"
-          some <$> .value <$> mkValueBindingSpec args ⟨nameIndex, nameP⟩ ⟨typeIndex, typeP⟩
+          some <$> .value <$> mkValueBindingSpec argDecls ⟨nameIndex, nameP⟩ ⟨typeIndex, typeP⟩
         | q`StrataDDL.declareFn => do
           let #[.catbvar nameIndex, .catbvar argsIndex, .catbvar typeIndex] := attr.args
             | newBindingErr "declareFn missing required arguments."; return none
-          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < args.size))
+          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < argDecls.size))
             | return panic! "Invalid name index"
-          let .isTrue argsP := inferInstanceAs (Decidable (argsIndex < args.size))
+          let .isTrue argsP := inferInstanceAs (Decidable (argsIndex < argDecls.size))
             | return panic! "Invalid arg index"
-          let .isTrue typeP := inferInstanceAs (Decidable (typeIndex < args.size))
+          let .isTrue typeP := inferInstanceAs (Decidable (typeIndex < argDecls.size))
             | return panic! "Invalid name index"
-          some <$> .value <$> mkValueBindingSpec args ⟨nameIndex, nameP⟩ ⟨typeIndex, typeP⟩ (argsIndex := some ⟨argsIndex, argsP⟩)
+          some <$> .value <$> mkValueBindingSpec argDecls ⟨nameIndex, nameP⟩ ⟨typeIndex, typeP⟩ (argsIndex := some ⟨argsIndex, argsP⟩)
         | q`StrataDDL.declareType => do
           let #[.catbvar nameIndex, .option mArgsArg ] := attr.args
             | newBindingErr s!"declareType has bad arguments {repr attr.args}."; return none
-          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < args.size))
+          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < argDecls.size))
             | return panic! "Invalid name index"
           let nameIndex := ⟨nameIndex, nameP⟩
-          checkNameIndexIsIdent args nameIndex
+          checkNameIndexIsIdent argDecls nameIndex
           let argsIndex ←
                 match mArgsArg with
                 | none => pure none
                 | some (.catbvar idx) =>
-                  let .isTrue argsP := inferInstanceAs (Decidable (idx < args.size))
+                  let .isTrue argsP := inferInstanceAs (Decidable (idx < argDecls.size))
                     | return panic! "Invalid arg index"
                   pure <| some ⟨idx, argsP⟩
                 | _ => newBindingErr "declareType args invalid."; return none
@@ -705,21 +700,21 @@ def parseNewBindings (md : Metadata) (args : ArgDecls) : Array (BindingSpec args
         | q`StrataDDL.aliasType => do
           let #[.catbvar nameIndex, .option mArgsArg, .catbvar defIndex] := attr.args
             | newBindingErr "aliasType missing arguments."; return none
-          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < args.size))
+          let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < argDecls.size))
             | return panic! "Invalid name index"
           let nameIndex := ⟨nameIndex, nameP⟩
-          checkNameIndexIsIdent args nameIndex
-          let argsIndex ←
+          checkNameIndexIsIdent argDecls nameIndex
+          let argsIndex : DebruijnIndex argDecls.size ←
                 match mArgsArg with
                 | none => pure none
                 | some (.catbvar idx) =>
-                  let .isTrue argsP := inferInstanceAs (Decidable (idx < args.size))
+                  let .isTrue argsP := inferInstanceAs (Decidable (idx < argDecls.size))
                     | return panic! "Invalid arg index"
                   pure <| some ⟨idx, argsP⟩
                 | _ => newBindingErr "aliasType args invalid."; return none
-          let .isTrue defP := inferInstanceAs (Decidable (defIndex < args.size))
+          let .isTrue defP := inferInstanceAs (Decidable (defIndex < argDecls.size))
             | return panic! "Invalid def index"
-          let defBinding := args[args.size - (defIndex+1)]
+          let defBinding := argDecls[argDecls.size - (defIndex+1)]
           match defBinding.kind with
           | .cat (.atom q`Init.Type) =>
             pure ()
@@ -737,8 +732,8 @@ def parseNewBindings (md : Metadata) (args : ArgDecls) : Array (BindingSpec args
           pure none
   (md.toArray.filterMapM ins) #[]
 
-def parseNewBindings! (md : Metadata) (args : ArgDecls) : Array (BindingSpec args) :=
-  let (r, errs) := parseNewBindings md args
+def parseNewBindings! (md : Metadata) (argDecls : ArgDecls) : Array (BindingSpec argDecls) :=
+  let (r, errs) := parseNewBindings md argDecls
   if let some msg := errs[0]? then
     panic! msg
   else
@@ -801,14 +796,14 @@ structure FunctionDecl where
   result : PreType
   syntaxDef : SyntaxDef
   metadata : Metadata := .empty
-deriving Inhabited, Repr, BEq
+deriving BEq, Inhabited, Repr
 
 inductive MetadataArgType
 | num
 | ident
 | bool
 | opt (tp : MetadataArgType)
-deriving Repr, DecidableEq, Inhabited
+deriving DecidableEq, Inhabited, Repr
 
 structure MetadataArgDecl where
   ident : String
@@ -946,7 +941,9 @@ deriving Inhabited
 namespace Dialect
 
 instance : BEq Dialect where
-  beq x y := x.name = y.name && x.imports = y.imports && x.declarations == y.declarations
+  beq x y := x.name = y.name
+    && x.imports = y.imports
+    && x.declarations == y.declarations
 
 def syncats (d : Dialect) : Collection SynCatDecl where
   declarations := d.declarations
@@ -1025,7 +1022,6 @@ instance (nm : String) (d : Dialect) : Decidable (nm ∈ d) :=
 
 end Dialect
 
-
 /-- BEq between two Std HashMap; checked by doing inclusion test twice -/
 instance [BEq α] [Hashable α] [BEq β]: BEq (Std.HashMap α β) where
   beq x y := Id.run do
@@ -1036,7 +1032,6 @@ instance [BEq α] [Hashable α] [BEq β]: BEq (Std.HashMap α β) where
         return false
     return true
 
-
 structure DialectMap where
   map : Std.HashMap DialectName Dialect
 deriving Inhabited, BEq
@@ -1119,33 +1114,31 @@ end DialectMap
 mutual
 
 /--
-Invoke a function `f` over each of the binding specifications for an arg
-so that a result type context can be constructed.
+Invoke a function `f` over each of the declaration specifications for an arg.
 -/
-partial def foldArgBindingSpecs
+partial def foldOverArgBindingSpecs
     (m : DialectMap)
-    (f : α → ∀(argDecls : ArgDecls), BindingSpec argDecls → Vector Arg argDecls.size → α)
-    (init : α)
+    (f : β → ∀(argDecls : ArgDecls), BindingSpec argDecls → Vector Arg argDecls.size → β)
+    (init : β)
     (a : Arg)
-    : α :=
+    : β :=
   match a with
-  | .op op => foldOverOpBindings m f init op
-  | .expr _ | .type _ | .cat _ | .ident _ | .num _ | .decimal _ | .strlit _ => init
+  | .op op => op.foldBindingSpecs m f init
+  | .expr _ | .type _ | .cat _ | .ident .. | .num .. | .decimal .. | .strlit .. => init
   | .option none => init
-  | .option (some a) => foldArgBindingSpecs m f init a
-  | .seq a => a.attach.foldl (init := init) (fun init ⟨a, _⟩ => foldArgBindingSpecs m f init a)
-  | .commaSepList a => a.attach.foldl (init := init) (fun init ⟨a, _⟩ => foldArgBindingSpecs m f init a)
+  | .option (some a) => foldOverArgBindingSpecs m f init a
+  | .seq a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
+  | .commaSepList a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
 
 /--
-Invoke a function `f` over each of the binding specifications for an operator
-so that a result type context can be constructed.
+Invoke a function `f` over each of the declaration specifications for an operator.
 -/
-partial def foldOverOpBindings
+partial def Operation.foldBindingSpecs {β}
     (m : DialectMap)
-    (f : α → ∀{argDecls : ArgDecls}, BindingSpec argDecls → Vector Arg argDecls.size → α)
-    (init : α)
+    (f : β → ∀{argDecls : ArgDecls}, BindingSpec argDecls → Vector Arg argDecls.size → β)
+    (init : β)
     (op : Operation)
-    : α :=
+    : β :=
   let decl := m.opDecl! op.name
   let argDecls := decl.argDecls
   let args := op.args
@@ -1155,7 +1148,7 @@ partial def foldOverOpBindings
       match decl.metadata.resultLevel argDecls.size with
       | none => init
       | some lvl => foldOverArgAtLevel m f init argDecls argsV lvl
-    decl.newBindings.foldl (init := init) (fun a b => f a b ⟨args, by omega⟩)
+    decl.newBindings.foldl (init := init) fun a b => f a b argsV
   else
     @panic _ ⟨init⟩ "Expected arguments to match bindings"
 
@@ -1163,19 +1156,19 @@ partial def foldOverOpBindings
 Invoke a function `f` over a given argument for a function or operation so that
 the result context for that argument can be constructed.
 -/
-partial def foldOverArgAtLevel
+partial def foldOverArgAtLevel {β}
     (m : DialectMap)
-    (f : α → ∀{argDecls : ArgDecls}, BindingSpec argDecls → Vector Arg argDecls.size → α)
-    (init : α)
+    (f : β → ∀{argDecls : ArgDecls}, BindingSpec argDecls → Vector Arg argDecls.size → β)
+    (init : β)
     (bindings : ArgDecls)
     (args : Vector Arg bindings.size)
     (level : Fin bindings.size)
-    : α :=
+    : β :=
   let init :=
         match bindings.argScopeLevel level with
         | none => init
         | some lvl => foldOverArgAtLevel m f init bindings args ⟨lvl, by omega⟩
-  foldArgBindingSpecs m f init args[level]
+  foldOverArgBindingSpecs m f init args[level]
 
 end
 
@@ -1184,52 +1177,52 @@ inductive GlobalKind where
 | type (params : List String) (definition : Option TypeExpr)
 deriving Inhabited, Repr, BEq
 
-mutual
-
-/-- Resolves binding spec for a new value to its type. -/
-partial def resolveBindingType (m : DialectMap) (b : BindingSpec bindings) (argsV : Vector Arg bindings.size) : TypeExpr :=
-  match resolveBindingIndices m b argsV with
-  | .expr tp => tp
-  | .type _ _ => panic! s!"Expecbted binding to be expression."
-
 /-- Resolves a binding spec into a global kind. -/
-partial def resolveBindingIndices { args } (m : DialectMap) (b : BindingSpec args) (argsV : Vector Arg args.size) : GlobalKind :=
+partial def resolveBindingIndices { argDecls : ArgDecls } (m : DialectMap) (b : BindingSpec argDecls) (args : Vector Arg argDecls.size) : GlobalKind :=
   match b with
   | .value b =>
-    let fnBindings : Array (String × TypeExpr) :=
+    match args[b.typeIndex.toLevel] with
+    | .type tp =>
       match b.argsIndex with
       | none =>
-        #[]
+        .expr tp
       | some idx =>
-        let f (a : Array _) {args : ArgDecls} (b : BindingSpec args) argsV :=
-              let name := varNameByIndex argsV b.nameIndex
-              let type := resolveBindingType m b argsV
-              a.push (name, type)
-        foldOverArgAtLevel m f #[] args argsV idx.toLevel
-    match argsV[b.typeIndex.toLevel] with
-      | .type tp => .expr (.mkFunType fnBindings tp)
-      | .cat (.atom q`Init.Type) => .type [] none
-      | a => panic! s!"Expected new binding to be bound to type instead of {repr a}."
+        let f (a : Array _) {argDecls : ArgDecls} (b : BindingSpec argDecls) args :=
+                let type :=
+                      match resolveBindingIndices m b args with
+                      | .expr tp => tp
+                      | .type _ _ => panic! s!"Expected binding to be expression."
+                a.push type
+        let fnBindings : Array TypeExpr :=
+          foldOverArgAtLevel m f #[] argDecls args idx.toLevel
+        .expr <| fnBindings.foldr (init := tp) fun argType tp => .arrow argType tp
+    | .cat c =>
+      if c.name = q`Init.Type then
+        .type [] none
+      else
+        panic! s!"Expected new binding to be Type instead of {repr c}."
+    | a =>
+      panic! s!"Expected new binding to be bound to type instead of {repr a}."
   | .type b =>
     let params : Array String :=
         match b.argsIndex with
         | none => #[]
         | some idx =>
-          let addBinding (a : Array String) {args : _} (b : BindingSpec args) (argsV : Vector Arg args.size) :=
-              a.push (varNameByIndex argsV b.nameIndex)
-          foldOverArgAtLevel m addBinding #[] args argsV idx.toLevel
+          let addBinding (a : Array String) {argDecls : _} (b : BindingSpec argDecls) (args : Vector Arg argDecls.size) :=
+              match args[b.nameIndex.toLevel] with
+              | .ident name => a.push name
+              | a => panic! s!"Expected ident at {idx.val} {repr a}"
+          foldOverArgAtLevel m addBinding #[] argDecls args idx.toLevel
     let value :=
             match b.defIndex with
             | none => none
             | some idx =>
-              match argsV[idx.toLevel] with
+              match args[idx.toLevel] with
               | .type tp =>
                 some tp
               | _ => panic! "Bad arg"
     .type params.toList value
 
-end
-
 /--
 Typing environment created from declarations in an environment.
 -/
@@ -1268,9 +1261,12 @@ def kindOf! (ctx : GlobalContext) (idx : FreeVarIndex) : GlobalKind :=
   ctx.vars[idx]!.snd
 
 def addCommand (dialects : DialectMap) (init : GlobalContext) (op : Operation) : GlobalContext :=
-    foldOverOpBindings dialects addBinding init op
-  where addBinding gctx _ b args :=
-          let name := varNameByIndex args b.nameIndex
+    op.foldBindingSpecs dialects addBinding init
+  where addBinding (gctx : GlobalContext) _ b args :=
+          let name :=
+                match args[b.nameIndex.toLevel] with
+                | .ident e => e
+                | a => panic! s!"Expected ident at {b.nameIndex.toLevel} {repr a}"
           let kind := resolveBindingIndices dialects b args
           gctx.push name kind
 
@@ -1309,12 +1305,6 @@ def create (dialects : DialectMap) (dialect : DialectName) (commands : Array Ope
 
 end Program
 
-theorem sizeOf_lt_of_op_arg {e : Arg} {op : Operation} (p : e ∈ op.args) : sizeOf e < sizeOf op := by
-  cases op with
-  | mk name args =>
-  have q : sizeOf e < sizeOf args := by decreasing_tactic
-  decreasing_tactic
-
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf a < sizeOf as` when `a ∈ as`, which is useful for well founded recursions
 over a nested inductive like `inductive T | mk : List T → T`. -/
diff --git a/Strata/DDM/BuiltinDialects/Init.lean b/Strata/DDM/BuiltinDialects/Init.lean
index 67e741a8..552c2c91 100644
--- a/Strata/DDM/BuiltinDialects/Init.lean
+++ b/Strata/DDM/BuiltinDialects/Init.lean
@@ -11,9 +11,9 @@ namespace Strata
 open Elab
 open Parser (minPrec)
 
-def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := .app (.atom q`Init.Option) c
-def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := .app (.atom q`Init.Seq) c
-def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := .app (.atom q`Init.CommaSepBy) c
+def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := { name := q`Init.Option, args := #[c] }
+def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { name := q`Init.Seq, args := #[c] }
+def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { name := q`Init.CommaSepBy, args := #[c] }
 
 def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   let Ident : ArgDeclKind := .cat <| .atom q`Init.Ident
@@ -35,13 +35,13 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat QualifiedIdent
   declareOp {
      name := "qualifiedIdentType",
-     argDecls := #[],
+     argDecls := .empty,
      category := QualifiedIdent,
      syntaxDef := .ofList [.str "Type"],
   }
   declareOp {
      name := "qualifiedIdentImplicit",
-     argDecls := #[
+     argDecls := .ofArray #[
         { ident := "name", kind := Ident }
      ],
      category := QualifiedIdent,
@@ -49,7 +49,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
      name := "qualifiedIdentExplicit",
-     argDecls := #[
+     argDecls := .ofArray #[
         { ident := "dialect", kind := Ident },
         { ident := "name", kind := Ident }
      ],
@@ -62,7 +62,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat TypeExprId
   declareOp {
     name := "TypeIdent",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := .cat <| .atom QualifiedIdent }
     ]
     category := TypeExprId,
@@ -70,7 +70,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "TypeParen",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := TypeExpr }
     ]
     category := TypeExprId,
@@ -78,7 +78,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "TypeArrow",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "lhs", kind := TypeExpr },
       { ident := "rhs", kind := TypeExpr }
     ]
@@ -87,7 +87,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "TypeApp",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "fn", kind := TypeExpr },
       { ident := "val", kind := TypeExpr }
     ]
@@ -99,7 +99,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat «Type»
   declareOp  {
     name := "mkType",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "type", kind := TypeExpr }
     ],
     category := «Type»,
@@ -110,7 +110,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat Expr
   declareOp {
     name := "exprIdent",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := Ident }
     ],
     category := Expr,
@@ -118,7 +118,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "exprParen",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := .cat (.atom Expr) }
     ],
     category := Expr,
@@ -126,7 +126,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "exprApp",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "function", kind := Ident },
       { ident := "args", kind := .cat <| .mkCommaSepBy (.atom Expr) }
     ],
@@ -138,7 +138,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat MetadataArg
   declareOp {
     name := "MetadataArgParen",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := .cat (.atom MetadataArg) }
     ],
     category := MetadataArg,
@@ -146,7 +146,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "MetadataArgNum",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := .cat Num }
     ],
     category := MetadataArg,
@@ -154,7 +154,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "MetadataArgIdent",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := Ident }
     ],
     category := MetadataArg,
@@ -162,28 +162,28 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "MetadataArgTrue",
-    argDecls := #[],
+    argDecls := .empty,
     category := MetadataArg,
     syntaxDef := .ofList [.str "true"]
   }
   declareOp {
     name := "MetadataArgFalse",
-    argDecls := #[],
+    argDecls := .empty,
     category := MetadataArg,
     syntaxDef := .ofList [.str "false"]
   }
   declareOp {
     name := "MetadataArgSome",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := .cat (.atom MetadataArg) }
     ],
     category := MetadataArg,
     syntaxDef := .ofList [.str "some", .ident 0 appPrec]
   }
   declareOp {
-    name := "MetadataArgNone",
-    argDecls := #[],
-    category := MetadataArg,
+    name := "MetadataArgNone"
+    argDecls := .empty
+    category := MetadataArg
     syntaxDef := .ofList [.str "none"]
   }
 
@@ -191,7 +191,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat MetadataArgs
   declareOp {
     name := "MetadataArgsMk",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "args", kind := .cat <| .mkCommaSepBy <| .atom MetadataArg }
     ],
     category := MetadataArgs,
@@ -202,7 +202,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat MetadataAttr
   declareOp {
     name := "MetadataAttrMk",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "name", kind := .cat <| .atom QualifiedIdent },
       { ident := "args", kind := .cat <| .mkOpt <| .atom MetadataArgs }
     ],
@@ -214,7 +214,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat Metadata
   declareOp {
     name := "MetadataMk",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "attrs", kind := .cat <| .mkCommaSepBy <| .atom MetadataAttr }
     ],
     category := Metadata,
@@ -228,7 +228,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat BindingType
   declareOp  {
     name := "mkBindingType",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "type", kind := TypeExpr }
     ],
     category := BindingType,
@@ -240,7 +240,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat TypeP
   declareOp  {
     name := "mkTypeP",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "type", kind := TypeExpr }
     ],
     category := TypeP,
@@ -251,7 +251,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat SyntaxAtomPrec
   declareOp {
     name := "syntaxAtomPrec",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := .cat Num }
     ],
     category := SyntaxAtomPrec,
@@ -262,7 +262,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat SyntaxAtom
   declareOp {
     name := "syntaxAtomIdent",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "ident", kind := Ident },
       { ident := "prec", kind := .cat <| .mkOpt <| .atom SyntaxAtomPrec }
     ],
@@ -272,7 +272,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "syntaxAtomString",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "value", kind := .cat Str }
     ],
     category := SyntaxAtom,
@@ -280,7 +280,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   }
   declareOp {
     name := "syntaxAtomIndent",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "indent", kind := .cat Num },
       { ident := "args", kind := .cat <| .mkSeq <| .atom SyntaxAtom }
     ],
@@ -292,7 +292,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareCat SyntaxDef
   declareOp {
     name := "mkSyntaxDef",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "args", kind := .cat <| .mkSeq (.atom SyntaxAtom) }
     ],
     category := SyntaxDef,
diff --git a/Strata/DDM/BuiltinDialects/StrataDDL.lean b/Strata/DDM/BuiltinDialects/StrataDDL.lean
index 4e0c2a3c..4d12b59c 100644
--- a/Strata/DDM/BuiltinDialects/StrataDDL.lean
+++ b/Strata/DDM/BuiltinDialects/StrataDDL.lean
@@ -22,7 +22,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   -- from bindings name and type.
   declareOp {
     name := "TypeFn",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "bindings", kind := Ident },
       { ident := "val", kind := .cat <| .atom TypeExpr }
     ]
@@ -34,7 +34,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   declareCat Binding
   declareOp {
       name := "mkBinding",
-      argDecls := #[
+      argDecls := .ofArray #[
         { ident := "name", kind := Ident, },
         { ident := "type", kind := .cat <| .atom BindingType, },
         { ident := "metadata", kind := .cat <| .mkOpt (.atom Metadata), }
@@ -47,7 +47,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   declareCat Bindings
   declareOp {
       name := "mkBindings",
-      argDecls := #[
+      argDecls := .ofArray #[
         { ident := "bs", kind := .cat <| .mkCommaSepBy <| .atom Binding }
       ],
       category := Bindings,
@@ -56,7 +56,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
 
   declareOp {
     name := "importCommand",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "name", kind := Ident }
     ],
     category := Command,
@@ -64,7 +64,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   }
   declareOp {
     name := "categoryCommand",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "name", kind := Ident }
     ],
     category := Command,
@@ -72,7 +72,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   }
   declareOp {
     name := "opCommand",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "name",
         kind := Ident
       },
@@ -101,7 +101,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   }
   declareOp {
     name := "typeCommand",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "name", kind := Ident },
       { ident := "args", kind := .cat (.mkOpt (.atom Bindings)) }
     ],
@@ -110,7 +110,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   }
   declareOp {
     name := "fnCommand",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "name",
         kind := Ident
       },
@@ -139,7 +139,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   }
   declareOp {
     name := "mdCommand",
-    argDecls := #[
+    argDecls := .ofArray #[
       { ident := "name", kind := Ident },
       { ident := "args", kind := .cat (.mkOpt (.atom Bindings)) }
     ],
diff --git a/Strata/DDM/BuiltinDialects/StrataHeader.lean b/Strata/DDM/BuiltinDialects/StrataHeader.lean
index 901bc2f2..00be9f01 100644
--- a/Strata/DDM/BuiltinDialects/StrataHeader.lean
+++ b/Strata/DDM/BuiltinDialects/StrataHeader.lean
@@ -16,7 +16,7 @@ def headerDialect : Dialect := BuiltinM.create! "StrataHeader" #[initDialect] do
 
   declareOp {
      name := "dialectCommand",
-     argDecls := #[
+     argDecls := .ofArray #[
         { ident := "name", kind := Ident }
      ],
      category := Command,
@@ -24,7 +24,7 @@ def headerDialect : Dialect := BuiltinM.create! "StrataHeader" #[initDialect] do
   }
   declareOp {
      name := "programCommand",
-     argDecls := #[
+     argDecls := .ofArray #[
         { ident := "name", kind := Ident }
      ],
      category := Command,
diff --git a/Strata/DDM/Elab.lean b/Strata/DDM/Elab.lean
index 3e4f5bd7..ac59590d 100644
--- a/Strata/DDM/Elab.lean
+++ b/Strata/DDM/Elab.lean
@@ -62,7 +62,7 @@ partial def elabHeader
   let s : DeclState := .initDeclState
   let s := s.openLoadedDialect! .builtin headerDialect
   let s := { s with pos := startPos }
-  let ctx := { inputContext := inputContext, stopPos := stopPos, loader := .builtin }
+  let ctx := { inputContext := inputContext, stopPos := stopPos, loader := .builtin, missingImport := false }
   let (mtree, s) := elabCommand leanEnv ctx s
   if s.errors.isEmpty then
     match mtree with
@@ -107,7 +107,7 @@ def elabProgramRest
   let s := DeclState.initDeclState
   let s := { s with pos := startPos }
   let s := s.openLoadedDialect! loader d
-  let ctx : DeclContext := { inputContext, stopPos, loader := loader }
+  let ctx : DeclContext := { inputContext, stopPos, loader := loader, missingImport := false }
   let (cmds, s) := runCommand leanEnv #[] stopPos ctx s
   if s.errors.isEmpty then
     let openDialects := loader.dialects.importedDialects! dialect
@@ -358,6 +358,7 @@ partial def elabDialectRest
         imports := #[initDialect.name]
     },
     loaded := dialects
+    missingImport := false
   }
   let ((), ds) ← act dctx |>.run ds
   pure (ds.loaded, ds.dialect, ds.declState)
diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean
index 44f2a244..9d8aac9b 100644
--- a/Strata/DDM/Elab/Core.lean
+++ b/Strata/DDM/Elab/Core.lean
@@ -16,6 +16,22 @@ open Strata.Parser (DeclParser InputContext ParserState)
 
 namespace Strata
 
+namespace TypeExpr
+
+/-
+This applies global context to instantiate types and variables.
+
+Free type alias variables bound to alias
+-/
+protected def instType (d : TypeExpr) (bindings : Array TypeExpr) : TypeExpr := Id.run <|
+  d.instTypeM fun idx =>
+    if p : idx < bindings.size then
+      pure <| bindings[bindings.size - (idx+1)]
+    else
+      .bvar (idx - bindings.size)
+
+end TypeExpr
+
 /--
 Get the kind as a qualified identifier.
 -/
@@ -37,13 +53,62 @@ partial def expandMacros (m : DialectMap) (f : PreType) (args : Nat → Option A
     | none =>
       .error ()
     | some a =>
-      let addType tps _ s args := tps.push (resolveBindingType m s args)
-      let argTypes := foldArgBindingSpecs m addType (init := #[]) a
-      --let argTypes := foldOverArgAtLevel m addType (init := #[]) bindings args level
+      let addType (tps : Array TypeExpr) _ s args : Array TypeExpr :=
+        match resolveBindingIndices m s args with
+        | .expr tp => tps.push tp
+        | .type _ _ => panic! s!"Expected binding to be expression."
+      let argTypes := foldOverArgBindingSpecs m addType (init := #[]) a
       pure <| argTypes.foldr (init := r) .arrow
 
 namespace Elab
 
+namespace TypingContext
+
+/--
+This expands type aliases appearing at the head of the term so
+the head is in a normal form.
+-/
+partial def hnf (tctx : TypingContext) (e : TypeExpr) : TypeExpr :=
+  match e with
+  | .arrow .. | .ident .. => e
+  | .fvar idx args =>
+    let gctx := tctx.globalContext
+    match gctx.kindOf! idx with
+    | .expr _ => panic! "Type free variable bound to expression."
+    | .type params (some d) =>
+      assert! params.length = args.size
+      assert! !d.hasUnboundVar (bindingCount := args.size)
+      hnf (.empty gctx) (d.instType args)
+    | .type _ none => e
+  | .bvar idx =>
+    match tctx.bindings[tctx.bindings.size - 1 - idx]!.kind with
+    | .type params (some d) =>
+      assert! params.isEmpty
+      assert! d.isGround
+      hnf (tctx.drop (idx + 1)) d
+    | .type _ none => e
+    | _ => panic! "Expected a type"
+
+/--
+Attempt to interpret `e` as a `n`-ary function, and
+return the type of the arguments along with the return type if possible,
+or `error (args, r)` where `args` is an array with size `args.size < n` and `r`
+is the resulting type.
+-/
+def applyNArgs (tctx : TypingContext) (e : TypeExpr) (n : Nat) := aux #[] e
+  where aux (args : Array TypeExpr) (e : TypeExpr) : Except (Array TypeExpr × TypeExpr) (Vector TypeExpr n × TypeExpr) :=
+    if argsLt : args.size < n then
+      match tctx.hnf e with
+      | .arrow a r => aux (args.push a) r
+      | e => .error (args, e)
+    else
+      if argsGt : args.size > n then
+        .ok (⟨args.take n, by simp; omega⟩, e)
+      else
+        .ok (⟨args, by omega⟩, e)
+
+end TypingContext
+
 def commaPrec := 30
 
 def elabIdent (stx : Syntax) : String :=
@@ -66,6 +131,8 @@ structure ElabContext where
   syntaxElabs : SyntaxElabMap
   inputContext : InputContext
   globalContext : GlobalContext
+  /-- Flag to indicate we are missing an import (silences some warnings)-/
+  missingImport : Bool
 
 structure ElabState where
   -- Errors found in elaboration.
@@ -136,24 +203,26 @@ def resolveTypeBinding (tctx : TypingContext) (loc : SourceRange) (name : String
 This translate a possibly qualified identifier into a declaration in an
 open dialect.
 -/
-def resolveTypeOrCat (loc : SourceRange) (tpId : MaybeQualifiedIdent) : ElabM (Option (QualifiedIdent × TypeOrCatDecl)) :=
+def resolveTypeOrCat (loc : SourceRange) (tpId : MaybeQualifiedIdent) : ElabM (Option (QualifiedIdent × TypeOrCatDecl)) := do
   match tpId with
-  | .qid qid => do
+  | .qid qid =>
     let decls := (← read).typeOrCatDeclMap.get qid.name
     let decls := decls.filter fun (dialect, _) => dialect = qid.dialect
     match decls[0]? with
-    | none => do
-      logErrorMF loc mf!"Undeclared type or category {qid}."
+    | none =>
+      let isSilent := (←read).missingImport
+      logErrorMF loc mf!"Undeclared type or category {qid}." (isSilent := isSilent)
       return none
     | some (_, decl) =>
       assert! decls.size = 1
       return some (qid, decl.val)
-  | .name name => do
+  | .name name =>
     let m := (← read).typeOrCatDeclMap
     let decls:= m.get name
     match decls[0]? with
     | none => do
-      logErrorMF loc mf!"Undeclared type or category {name}."
+      let isSilent := (←read).missingImport
+      logErrorMF loc mf!"Undeclared type or category {name}." (isSilent := isSilent)
       return none
     | some (d, decl) =>
       if let some (candD, _) := decls[1]? then
@@ -165,12 +234,19 @@ def resolveTypeOrCat (loc : SourceRange) (tpId : MaybeQualifiedIdent) : ElabM (O
 
 def translateQualifiedIdent (t : Tree) : MaybeQualifiedIdent :=
   let op := t.info.asOp!.op
-  match op.name, op.args with
-  | q`Init.qualifiedIdentImplicit, #[.ident name] =>
+  let args := op.args
+  match op.name, sz : args.size with
+  | q`Init.qualifiedIdentImplicit, 1 => Id.run do
+    let .ident name := args[0]
+      | return panic! "Expected ident"
     .name name
-  | q`Init.qualifiedIdentExplicit, #[.ident dialect, .ident name] =>
+  | q`Init.qualifiedIdentExplicit, 2 => Id.run do
+    let .ident dialect := args[0]
+      | return panic! "Expected ident"
+    let .ident name := args[1]
+      | return panic! "Expected ident"
     .qid { dialect, name }
-  | q`Init.qualifiedIdentType, #[] =>
+  | q`Init.qualifiedIdentType, 0 =>
     .qid { dialect := "Init", name := "Type" }
   | name, _ =>
     panic! s!"Unknown qualified ident {name.fullName}"
@@ -215,14 +291,15 @@ def translateTypeIdent (elabInfo : ElabInfo) (qualIdentInfo : Tree) (args : Arra
     let (_, success) ← runChecked <| checkArgSize loc ident decl.argNames.size args
     if !success then
       return default
-    let mut sc : SyntaxCat := .atom ident
+    let mut scArgs : Array SyntaxCat := .emptyWithCapacity args.size
     for a in args do
       match a.info with
       | .ofCatInfo info =>
-        sc := .app sc info.cat
+        scArgs := scArgs.push info.cat
       | _ =>
         logError a.info.loc "Expected category."
         return default
+    let sc : SyntaxCat := SyntaxCat.mk ident scArgs
     let info : CatInfo := { toElabInfo := elabInfo, cat := sc }
     return .node (.ofCatInfo info) args
 
@@ -249,31 +326,6 @@ partial def headExpandTypeAlias (gctx : GlobalContext) (e : TypeExpr) : TypeExpr
       headExpandTypeAlias gctx (d.instType args)
     | .type _ none => e
 
-/--
-This expands type aliases appearing at the head of the term so
-the root is in a normal form.
--/
-partial def rnf (tctx : TypingContext) (e : TypeExpr) : TypeExpr :=
-  match e with
-  | .arrow _ _ | .ident _ _ => e
-  | .fvar idx args =>
-    let gctx := tctx.globalContext
-    match gctx.kindOf! idx with
-    | .expr _ => panic! "Type free variable bound to expression."
-    | .type params (some d) =>
-      assert! params.length = args.size
-      assert! !d.hasUnboundVar (bindingCount := args.size)
-      rnf (.empty gctx) (d.instType args)
-    | .type _ none => e
-  | .bvar idx =>
-    match tctx.bindings[tctx.bindings.size - 1 - idx]!.kind with
-    | .type params (some d) =>
-      assert! params.isEmpty
-      assert! d.isGround
-      rnf (tctx.drop (idx + 1)) d
-    | .type _ none => e
-    | _ => panic! "Expected a type"
-
 /--
 This checks that two types `itype` and `rtype` are equivalent.
 
@@ -282,8 +334,8 @@ at position `stx` and `rtype` refers to a type inferred or specifed by a previou
 argument.
 -/
 partial def checkExpressionType (tctx : TypingContext) (itype rtype : TypeExpr) : ElabM Bool := do
-  let itype := rnf tctx itype
-  let rtype := rnf tctx rtype
+  let itype := tctx.hnf itype
+  let rtype := tctx.hnf rtype
   match itype, rtype with
   | .ident iq ia, .ident rq ra =>
     if p : iq = rq ∧ ia.size = ra.size then do
@@ -312,14 +364,15 @@ partial def checkExpressionType (tctx : TypingContext) (itype rtype : TypeExpr)
 mutual
 
 partial def unifyTypeVectors
-  (b : ArgDecls)
-  (argLevel0 : Fin b.size)
+  {argc : Nat}
+  (b : Vector ArgDecl argc)
+  (argLevel0 : Fin argc)
   (ea : Array TypeExpr)
   (tctx : TypingContext)
   (exprSyntax : Syntax)
   (ia : Array TypeExpr)
-  (args : Vector (Option Tree) b.size)
-  : ElabM (Vector (Option Tree) b.size) := do
+  (args : Vector (Option Tree) argc)
+  : ElabM (Vector (Option Tree) argc) := do
   assert! ea.size = ia.size
   let mut res := args
   for i in Fin.range ea.size do
@@ -344,14 +397,15 @@ inferred.
    new arguments are returned.
 -/
 partial def unifyTypes
-    (b : ArgDecls)
-    (argLevel0 : Fin b.size)
+    {argc : Nat}
+    (b : Vector ArgDecl argc)
+    (argLevel0 : Fin argc)
     (expectedType : TypeExpr)
     (tctx : TypingContext)
     (exprSyntax : Syntax)
     (inferredType : TypeExpr)
-    (args : Vector (Option Tree) b.size)
-    : ElabM (Vector (Option Tree) b.size) := do
+    (args : Vector (Option Tree) argc)
+    : ElabM (Vector (Option Tree) argc) := do
   let ⟨argLevel, argLevelP⟩ := argLevel0
   -- Expand defined free vars at root to get head norm form
   let expectedType := headExpandTypeAlias tctx.globalContext expectedType
@@ -360,7 +414,7 @@ partial def unifyTypes
     | panic! "unifyTypes missing source location"
   match expectedType with
   | .ident eid ea =>
-    let inferredHead := rnf tctx inferredType
+    let inferredHead := tctx.hnf inferredType
     match inferredHead with
     | .ident iid ia =>
       if eid != iid then
@@ -372,7 +426,7 @@ partial def unifyTypes
       logErrorMF exprLoc mf!"Encountered {inferredHead} expression when {expectedType} expected."
       return args
   | .fvar eid ea =>
-    match rnf tctx inferredType with
+    match tctx.hnf inferredType with
     | .fvar iid ia =>
       if eid != iid then
         logErrorMF exprLoc mf!"Encountered {inferredType} expression when {expectedType} expected."
@@ -386,7 +440,6 @@ partial def unifyTypes
     let .isTrue idxP := inferInstanceAs (Decidable (idx < argLevel))
       | return panic! "Invalid index"
     let typeLevel := argLevel - (idx + 1)
-    have typeLevelP : typeLevel < b.size := by omega
     -- Verify type level is a type parameter.
     assert! b[typeLevel].kind.isType
 
@@ -569,10 +622,8 @@ partial def translateSyntaxCat (tree : Tree) : ElabM SyntaxCat := do
     match decl with
     | .syncat decl =>
       checkArgSize argInfo.loc name decl.argNames.size args
-      let r : SyntaxCat := .atom name
-      args.attach.foldlM (init := r) fun r ⟨a, _⟩ => do
-        have p : sizeOf a < sizeOf args := by decreasing_tactic
-        return .app r (← translateSyntaxCat a)
+      let scArgs ← args.mapM translateSyntaxCat
+      pure { name := name, args := scArgs }
     | _ =>
       logError nameLoc s!"Expected category"; pure default
 
@@ -590,16 +641,6 @@ Evaluate the tree as a type expression.
 def translateTypeExpr (tree : Tree) : ElabM TypeExpr := do
   match feq : flattenTypeApp tree #[] with
   | (⟨argInfo, argChildren⟩, args) =>
-  have argcP : sizeOf argChildren < sizeOf tree := by
-    have p := flattenTypeApp_size tree #[]
-    have q := Array.sizeOf_min args
-    simp [feq] at p
-    omega
-  have argsP : sizeOf args ≤ sizeOf tree := by
-    have p := flattenTypeApp_size tree #[]
-    have q := Array.sizeOf_min argChildren
-    simp [feq] at p
-    omega
   let opInfo :=
         match argInfo with
         | .ofOperationInfo info => info
@@ -617,7 +658,6 @@ def translateTypeExpr (tree : Tree) : ElabM TypeExpr := do
     | .type decl =>
       checkArgSize opInfo.loc qname decl.argNames.size args
       let args ← args.attach.mapM fun ⟨a, _⟩ =>
-        have p : sizeOf a < sizeOf args := by decreasing_tactic
         translateTypeExpr a
       return .ident qname args
     | _ =>
@@ -638,10 +678,26 @@ def translateTypeExpr (tree : Tree) : ElabM TypeExpr := do
     return default
   termination_by tree
   decreasing_by
-    · decreasing_tactic
-    · have p : sizeOf argChildren[0] < sizeOf argChildren := by decreasing_tactic
+    · have argsP : sizeOf args ≤ sizeOf tree := by
+          have p := flattenTypeApp_size tree #[]
+          have q := Array.sizeOf_min argChildren
+          simp [feq] at p
+          omega
+      have p : sizeOf a < sizeOf args := by decreasing_tactic
+      decreasing_tactic
+    · have argcP : sizeOf argChildren < sizeOf tree := by
+        have p := flattenTypeApp_size tree #[]
+        have q := Array.sizeOf_min args
+        simp [feq] at p
+        omega
+      have p : sizeOf argChildren[0] < sizeOf argChildren := by decreasing_tactic
       decreasing_tactic
-    · have p : sizeOf argChildren[1] < sizeOf argChildren := by decreasing_tactic
+    · have argcP : sizeOf argChildren < sizeOf tree := by
+        have p := flattenTypeApp_size tree #[]
+        have q := Array.sizeOf_min args
+        simp [feq] at p
+        omega
+      have p : sizeOf argChildren[1] < sizeOf argChildren := by decreasing_tactic
       decreasing_tactic
 
 /--
@@ -653,7 +709,6 @@ partial def translateBindingKind (tree : Tree) : ElabM BindingKind := do
         match argInfo with
         | .ofOperationInfo info => info
         | _ => panic! s!"translateBindingTypeExpr expected operator, type or cat {repr argInfo}"
-  let op := opInfo.op.name
   match opInfo.op.name, szp : argChildren.size with
   | q`Init.TypeIdent, 1 => do
     let nameTree := argChildren[0]
@@ -669,9 +724,8 @@ partial def translateBindingKind (tree : Tree) : ElabM BindingKind := do
     | .syncat decl =>
       checkArgSize argInfo.loc name decl.argNames.size args
       let r : SyntaxCat := .atom name
-      let r ← args.foldlM (init := r) fun r a => do
-        return .app r (← translateSyntaxCat a)
-      return .cat r
+      let scArgs ← args.mapM translateSyntaxCat
+      return .cat { name := name, args := scArgs }
   | q`Init.TypeArrow, 2 => do
     let aType ← translateTypeExpr argChildren[0]
     let rType ← translateTypeExpr argChildren[1]
@@ -744,28 +798,6 @@ def evalBindingSpec
               panic! "Bad arg"
     pure { ident, kind := .type params.toList value }
 
-namespace TypingContext
-
-/--
-Attempt to interpret `e` as a `n`-ary function, and
-return the type of the arguments along with the return type if possible,
-or `error (args, r)` where `args` is an array with size `args.size < n` and `r`
-is the resulting type.
--/
-def applyNArgs (tctx : TypingContext) (e : TypeExpr) (n : Nat) := aux #[] e
-  where aux (args : Array TypeExpr) (e : TypeExpr) : Except (Array TypeExpr × TypeExpr) (Vector TypeExpr n × TypeExpr) :=
-    if argsLt : args.size < n then
-      match rnf tctx e with
-      | .arrow a r => aux (args.push a) r
-      | e => .error (args, e)
-    else
-      if argsGt : args.size > n then
-        .ok (⟨args.take n, by simp; omega⟩, e)
-      else
-        .ok (⟨args, by omega⟩, e)
-
-end TypingContext
-
 /--
 Given a type expression and a natural number, this returns a
 -/
@@ -774,7 +806,11 @@ def resultType! (tctx : TypingContext) (e : TypeExpr) (n : Nat) : TypeExpr :=
   | .ok (_, r) => r
   | .error (n, _) => panic! s!"{n.size} unexpected arguments to function."
 
+/--
+Returns the type of `e` in typing context `tctx`.
+-/
 partial def inferType (tctx : TypingContext) (e : Expr) : ElabM TypeExpr := do
+  -- Compute head normal form of e.
   let ⟨f, a⟩ := e.hnf
   match f with
   | .bvar idx => do
@@ -861,27 +897,28 @@ partial def elabOperation (tctx : TypingContext) (stx : Syntax) : ElabM Tree :=
   let some se := (←read).syntaxElabs[i]?
     | return panic! s!"Unknown elaborator {i.fullName}"
   let initSize := tctx.bindings.size
-  let ((args, newCtx), success) ← runChecked <| runSyntaxElaborator se decl.argDecls tctx stx.getArgs
+  let argDecls := decl.argDecls.toArray.toVector
+  let ((args, newCtx), success) ← runChecked <| runSyntaxElaborator se argDecls tctx stx.getArgs
   if !success then
     return default
-  let newBindings := decl.newBindings
-  let resultCtx ← newBindings.foldlM (init := newCtx) <| fun ctx spec => do
+  let resultCtx ← decl.newBindings.foldlM (init := newCtx) <| fun ctx spec => do
     ctx.push <$> evalBindingSpec initSize spec args
   let op : Operation := { name := i, args := args.toArray.map (·.arg) }
   let info : OperationInfo := { loc := loc, inputCtx := tctx, op, resultCtx }
   return .node (.ofOperationInfo info) args.toArray
 
 partial def runSyntaxElaborator
+  {argc : Nat}
   (se : SyntaxElaborator)
-  (b : ArgDecls)
+  (b : Vector ArgDecl argc)
   (tctx0 : TypingContext)
-  (args : Array Syntax) : ElabM (Vector Tree b.size × TypingContext) := do
-  let mut trees : Vector (Option Tree) b.size := .replicate b.size none
+  (args : Array Syntax) : ElabM (Vector Tree argc × TypingContext) := do
+  let mut trees : Vector (Option Tree) argc := .replicate argc none
   for ae in se.argElaborators do
     let .isTrue syntaxLevelP := inferInstanceAs (Decidable (ae.syntaxLevel < args.size))
         | return panic! "Invalid syntaxLevel"
     let argLevel := ae.argLevel
-    let .isTrue argLevelP := inferInstanceAs (Decidable (argLevel < b.size))
+    let .isTrue argLevelP := inferInstanceAs (Decidable (argLevel < argc))
         | return panic! "Invalid argLevel"
     let tctx ←
       match ae.contextLevel with
@@ -920,7 +957,7 @@ partial def runSyntaxElaborator
     match se.resultScope with
     | none => tctx0
     | some idx => Id.run do
-      let .isTrue p := inferInstanceAs (Decidable (idx < b.size))
+      let .isTrue p := inferInstanceAs (Decidable (idx < argc))
         | return panic! "Invalid index"
       treesr[idx].resultContext
   return (treesr, tctx)
@@ -943,16 +980,16 @@ partial def elabType (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
   pure tree
 
 partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM Tree :=
-  match c with
-  | .atom q`Init.Expr =>
+  match c.name with
+  | q`Init.Expr =>
     elabExpr
-  | .atom q`Init.Ident =>
+  | q`Init.Ident =>
     fun tctx stx => do
       let some loc := mkSourceRange? stx
         | panic! "ident missing source location"
       let info : IdentInfo := { inputCtx := tctx, loc := loc, val := stx.getId.toString }
       pure <| .node (.ofIdentInfo info) #[]
-  | .atom q`Init.Num =>
+  | q`Init.Num =>
     fun tctx stx => do
       let some loc := mkSourceRange? stx
         | panic! "num missing source location"
@@ -962,7 +999,7 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
         pure <| .node (.ofNumInfo info) #[]
       | none =>
         panic! s!"Invalid Init.Num {repr stx}"
-  | .atom q`Init.Decimal =>
+  | q`Init.Decimal =>
     fun tctx stx => do
       let some loc := mkSourceRange? stx
         | panic! "decimal missing source location"
@@ -973,7 +1010,7 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
         pure <| .node (.ofDecimalInfo info) #[]
       | none =>
         panic! s!"Invalid Init.Num {repr stx}"
-  | .atom q`Init.Str =>
+  | q`Init.Str =>
     fun tctx stx => do
       let some loc := mkSourceRange? stx
         | panic! "str missing source location"
@@ -983,8 +1020,8 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
         pure <| .node (.ofStrlitInfo info) #[]
       | none =>
         panic! s!"String not supported {stx} {stx.isStrLit?}"
-  | .atom q`Init.Type => elabType
-  | .atom q`Init.TypeP =>
+  | q`Init.Type => elabType
+  | q`Init.TypeP =>
       fun tctx stx => do
         let (tree, true) ← runChecked <| elabOperation tctx stx
           | return default
@@ -995,14 +1032,18 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
         let ok :=
               match tree.info with
               | .ofTypeInfo _ => true
-              | .ofCatInfo info => info.cat = .atom q`Init.Type
+              | .ofCatInfo info => info.cat.isType
               | _ => false
         if !ok then
           logErrorMF tree.info.loc mf!"Expected a type or Type instead of {c}"
         pure tree
-  | .app (.atom q`Init.Option) a =>
+  | q`Init.Option =>
+    assert! c.args.size = 1
+    let a := c.args[0]!
     elabOption (catElaborator a)
-  | .app (.atom q`Init.Seq) a =>
+  |  q`Init.Seq =>
+    assert! c.args.size = 1
+    let a := c.args[0]!
     let f := elabManyElement (catElaborator a)
     fun tctx stx => do
       let some loc := mkSourceRange? stx
@@ -1010,7 +1051,9 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
       let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx)
       let info : SeqInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx }
       pure <| .node (.ofSeqInfo info) args
-  | .app (.atom q`Init.CommaSepBy) a =>
+  | q`Init.CommaSepBy =>
+    assert! c.args.size = 1
+    let a := c.args[0]!
     let f := elabManyElement (catElaborator a)
     fun tctx stx => do
       let some loc := mkSourceRange? stx
@@ -1018,10 +1061,9 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
       let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx)
       let info : CommaSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx }
       pure <| .node (.ofCommaSepInfo info) args
-  | .atom _ =>
-    elabOperation
   | _ =>
-    panic! s!"Unsupport category {eformat c}"
+    assert! c.args.isEmpty
+    elabOperation
 
 partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
   match stx.getKind with
@@ -1093,7 +1135,7 @@ partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
                { syntaxLevel := lvl, argLevel := lvl }
             resultScope := none
           }
-    let (args, _) ← runSyntaxElaborator se argDecls.toArray tctx args
+    let (args, _) ← runSyntaxElaborator se argDecls tctx args
     let e := args.toArray.foldl (init := fvar) fun e t =>
       .app e t.arg
     let info : ExprInfo := { toElabInfo := einfo, expr := e }
@@ -1110,7 +1152,8 @@ partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
       | return panic! (f!"unknown operation {eformat i}").pretty
     let some se := (←read).syntaxElabs[i]?
       | return panic! s!"Unknown expression elaborator {i.fullName}"
-    let ((args, _), success) ← runChecked <| runSyntaxElaborator se fn.argDecls tctx stx.getArgs
+    let argDecls := fn.argDecls.toArray.toVector
+    let ((args, _), success) ← runChecked <| runSyntaxElaborator se argDecls tctx stx.getArgs
     if !success then
       return default
     let e := args.toArray.foldl (init := Expr.fn i) fun e t => .app e t.arg
@@ -1119,7 +1162,7 @@ partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
 
 end
 
-def runElab (action : ElabM α) : DeclM α := do
+def runElab {α} (action : ElabM α) : DeclM α := do
   let loader := (← read).loader
   let s ← get
   let ctx : ElabContext := {
@@ -1130,6 +1173,7 @@ def runElab (action : ElabM α) : DeclM α := do
         metadataDeclMap := s.metadataDeclMap,
         globalContext := s.globalContext,
         inputContext := (←read).inputContext,
+        missingImport := (← read).missingImport
   }
   let errors := (←get).errors
   -- Clear errors from decl
diff --git a/Strata/DDM/Elab/DeclM.lean b/Strata/DDM/Elab/DeclM.lean
index 45bc52da..fbeddbab 100644
--- a/Strata/DDM/Elab/DeclM.lean
+++ b/Strata/DDM/Elab/DeclM.lean
@@ -125,16 +125,16 @@ def runChecked {m α} [ElabClass m] (action : m α) : m (α × Bool) := do
   let r ← action
   return (r, errorCount = (← ElabClass.getErrorCount))
 
-def logError {m} [ElabClass m] (loc : SourceRange) (msg : String) : m Unit := do
+def logError {m} [ElabClass m] (loc : SourceRange) (msg : String) (isSilent : Bool := false): m Unit := do
   let inputCtx ← ElabClass.getInputContext
-  let m := Lean.mkStringMessage inputCtx loc.start msg
+  let m := Lean.mkStringMessage inputCtx loc.start msg (isSilent := isSilent)
   let m := if loc.isNone then m else { m with endPos := inputCtx.fileMap.toPosition loc.stop }
   logErrorMessage m
 
-def logErrorMF {m} [ElabClass m] (loc : SourceRange) (msg : StrataFormat) : m Unit := do
+def logErrorMF {m} [ElabClass m] (loc : SourceRange) (msg : StrataFormat) (isSilent : Bool := false) : m Unit := do
   let c : FormatContext := .ofDialects (← ElabClass.getDialects) (← ElabClass.getGlobalContext) {}
   let s : FormatState := { openDialects := ← ElabClass.getOpenDialects }
-  logError loc (msg c s |>.format |>.pretty)
+  logError loc (msg c s |>.format |>.pretty) (isSilent := isSilent)
 
 -- DeclM
 
@@ -143,6 +143,8 @@ structure DeclContext where
   stopPos : String.Pos
   -- Map from dialect names to the dialect definition
   loader : LoadedDialects
+  /-- Flag indicating imports are missing (silences some errors). -/
+  missingImport : Bool
 
 namespace DeclContext
 
@@ -150,6 +152,7 @@ def empty : DeclContext where
   inputContext := default
   loader := .empty
   stopPos := 0
+  missingImport := false
 
 end DeclContext
 
diff --git a/Strata/DDM/Elab/DialectM.lean b/Strata/DDM/Elab/DialectM.lean
index 487339e6..a848ddcf 100644
--- a/Strata/DDM/Elab/DialectM.lean
+++ b/Strata/DDM/Elab/DialectM.lean
@@ -157,7 +157,6 @@ def translatePreType {argc : Nat} (argDecls : ArgDeclsMap argc) (tree : Tree) :
       | return panic! "Invalid arguments to Init.TypeArrow"
     let bindingsTree := argChildren[0]
     let valTree := argChildren[1]
-    have p : sizeOf valTree < sizeOf argChildren := by decreasing_tactic
     let rType ← translatePreType argDecls valTree
     translateFunMacro argDecls bindingsTree rType
   | _ =>
@@ -193,6 +192,7 @@ def translatePreType {argc : Nat} (argDecls : ArgDeclsMap argc) (tree : Tree) :
         simp [feq] at p
         omega
       decreasing_tactic
+
 /--
 Evaluate the tree as a type expression.
 -/
@@ -220,11 +220,10 @@ partial def translateArgDeclKind {argc} (argDecls : ArgDeclsMap argc) (tree : Tr
       return .type <| .ident name args
     | .syncat decl =>
       checkArgSize argInfo.loc name decl.argNames.size args
-      let r : SyntaxCat := .atom name
-      let r ← args.attach.foldlM (init := r) fun r ⟨a, _⟩ => do
-        have p : sizeOf a < sizeOf args := by decreasing_tactic
-        return .app r (← translateSyntaxCat a)
-      return .cat r
+      return .cat {
+        name := name
+        args := ← args.mapM translateSyntaxCat
+      }
   | q`Init.TypeArrow => do
     assert! argChildren.size = 2
     let aType ← translatePreType argDecls argChildren[0]!
@@ -393,12 +392,14 @@ def translateArgDecls (tree : Tree) : ElabM (Σ argc, ArgDeclsMap argc) := do
     else
       pure ⟨c+1, newArgs.push d p⟩
 
-partial def elabMetadataArgCatType (loc : SourceRange) (ci : SyntaxCat) : DeclM MetadataArgType := do
-  match ci with
-  | .atom q`Init.Bool => pure .bool
-  | .atom q`Init.Num => pure .num
-  | .atom q`Init.Ident => pure .ident
-  | .app (.atom q`Init.Option) e => .opt <$> elabMetadataArgCatType loc e
+partial def elabMetadataArgCatType (loc : SourceRange) (cat : SyntaxCat) : DeclM MetadataArgType := do
+  match cat.name with
+  | q`Init.Bool => pure .bool
+  | q`Init.Num => pure .num
+  | q`Init.Ident => pure .ident
+  | q`Init.Option =>
+    assert! cat.args.size = 1
+    .opt <$> elabMetadataArgCatType loc cat.args[0]!
   | c =>
     logErrorMF loc mf!"Unsupported metadata category {c}"
     pure default
@@ -519,6 +520,11 @@ structure DialectState where
   loaded : LoadedDialects
   declState : DeclState
   dialect : Dialect
+  /--
+  Flag to indicate dialect is missing an import.
+  Missing declarations will be silenced.
+  -/
+  missingImport : Bool
 
 abbrev DialectM := ReaderT DialectContext (StateRefT DialectState BaseIO)
 
@@ -528,14 +534,17 @@ instance :  MonadState DialectState DialectM := inferInstanceAs (MonadState Dial
 
 instance : MonadLift DeclM DialectM where
   monadLift act := fun c => do
-    let { loaded := loaded, declState := ds, dialect := dialect } ← get
+    let s ← get
+    let dialect := s.dialect
+    let missingImport := s.missingImport
     let ctx : DeclContext := {
         inputContext := c.inputContext,
         stopPos := c.stopPos,
-        loader := loaded
+        loader := s.loaded
+        missingImport := missingImport
     }
-    let (r, ds) := act ctx ds
-    set ({ loaded := loaded, declState := ds, dialect := dialect } : DialectState)
+    let (r, ds) := act ctx s.declState
+    set ({ loaded := ctx.loader, declState := ds, dialect := dialect, missingImport } : DialectState)
     pure  r
 
 def getDeclState : DialectM DeclState := fun _ => DialectState.declState <$> get
@@ -565,7 +574,7 @@ private def checkTypeDeclarationArgs (tree : Tree) : ElabM (Array String) := do
     if !arg.val.kind.isType then
       logErrorMF arg.typeLoc mf!"Parameters for a type declaration must have category {q`Init.Type}."
       return default
-  return argDecls.decls.toArray.map (·.val.ident)
+  return argDecls.decls.toArray.map fun a => a.val.ident
 
 def checkTreeSize (tree : Tree) (size : Nat) : Decidable (tree.children.size = size) := inferInstance
 
@@ -576,6 +585,10 @@ def elabDialectImportCommand : DialectElab := fun tree => do
     | panic! "Invalid tree size"
   let identTree := tree[0].info
   let name := identTree.asIdent!.val
+  if name ∈ (←getDeclState).openDialectSet then
+    logError identTree.loc <| s!"Dialect {name} already open."
+    return
+  modifyDialect fun d => { d with imports := d.imports.push name }
   let d ←
     match (← get).loaded.dialects[name]? with
     | some d =>
@@ -593,12 +606,9 @@ def elabDialectImportCommand : DialectElab := fun tree => do
         pure d
       | .error msg =>
         logError identTree.loc msg
+        modify fun s => { s with missingImport := true }
         return
-  if name ∈ (←getDeclState).openDialectSet then
-    logError identTree.loc <| s!"Dialect {name} already open."
-    return
   modify fun s => { s with declState := s.declState.openLoadedDialect! s.loaded d }
-  modifyDialect fun d => { d with imports := d.imports.push name }
 
 private def elabCategoryCommand : DialectElab := fun tree => do
   let .isTrue p := checkTreeSize tree 1
@@ -640,7 +650,7 @@ def elabOpCommand : DialectElab := fun tree => do
   let (syntaxDef, opStxSuccess) ← runElab <| runChecked <| translateSyntaxDef argDeclMap opMdTree opStxTree
 
   -- FIXME. Change this to use stxArgDecls so we get better error messages.
-  let argDecls : ArgDecls := argDeclMap.decls.toArray.map (·.val)
+  let argDecls := ArgDecls.ofArray <| argDeclMap.decls.toArray.map (·.val)
   let (newBindings, newBindingErrors) := parseNewBindings opMetadata argDecls
   for err in newBindingErrors do
     logError opMetadataTree.info.loc err
@@ -650,13 +660,10 @@ def elabOpCommand : DialectElab := fun tree => do
   if !opStxSuccess then
     return
 
-  let category ←
-      match category with
-      | .atom c =>
-        pure c
-      | .app _ _ =>
-        logError categoryTree.info.loc s!"Expected atomic category"
-        return
+  if category.args.size > 0 then
+      logError categoryTree.info.loc s!"Expected atomic category"
+      return
+  let category := category.name
 
   let ctx := (←getDeclState).fixedParsers
   let ident : QualifiedIdent := { dialect := d.name, name }
@@ -685,7 +692,7 @@ private def elabTypeCommand : DialectElab := fun tree => do
   let d ← getCurrentDialect
 
   -- Get arguments
-  let ((name, argNames), success) ← runElab <| runChecked <| do
+  let (decl, success) ← runElab <| runChecked <| do
     -- Get name
     let .node (.ofIdentInfo nameInfo) _ := tree[0]
       | panic! "Expected identifier"
@@ -693,9 +700,8 @@ private def elabTypeCommand : DialectElab := fun tree => do
     if name ∈ d.cache then
       logError nameInfo.loc  s!"{name} already declared."
     let args ← checkTypeDeclarationArgs tree[1]
-    pure (name, args)
+    pure ({ name, argNames := args } : TypeDecl)
   if success then
-    let decl := { name, argNames }
     addTypeOrCatDecl d.name (.type decl)
     addDeclToDialect (.type decl)
 
@@ -713,7 +719,7 @@ def elabFnCommand : DialectElab := fun tree => do
 
   let argsTree := tree[1]!
   let (⟨argc, argDeclsMap⟩, argDeclsSuccess) ← runElab <| runChecked <| translateArgDecls argsTree
-  let argDecls : ArgDecls := argDeclsMap.decls.toArray.map (·.val)
+  let argDecls := ArgDecls.ofArray <| argDeclsMap.decls.toArray.map (·.val)
 
   let returnTypeTree := tree[2].asBindingType!
   let (result, resultSuccess) ← runElab <| runChecked <| translatePreType argDeclsMap returnTypeTree
@@ -803,7 +809,7 @@ def dialectElabs : Std.HashMap QualifiedIdent DialectElab :=
 
 partial def runDialectCommand (leanEnv : Lean.Environment) : DialectM Bool := do
   assert! "StrataDDL" ∈ (← get).loaded.dialects.map.keys
-  let (mtree, success) ← runChecked <| elabCommand leanEnv
+  let (mtree, success) ← MonadLift.monadLift <| runChecked <| elabCommand leanEnv
   match mtree with
   | none =>
     pure false
diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean
index d58f9545..29c23220 100644
--- a/Strata/DDM/Format.lean
+++ b/Strata/DDM/Format.lean
@@ -245,9 +245,12 @@ end PreType
 
 namespace SyntaxCat
 
-protected def mformat : SyntaxCat → StrataFormat
-| .atom n => mf!"{n}"
-| .app h r => mf!"{h.mformat.ensurePrec appPrec} {r.mformat.ensurePrec (appPrec+1) }".ensurePrec appPrec
+protected def mformat (cat : SyntaxCat) : StrataFormat :=
+  let init := mformat cat.name
+  cat.args.foldl (init := init) (fun f a => mf!"{f} {a.mformat.ensurePrec (appPrec+1)}")
+  decreasing_by
+    rw [SyntaxCat.sizeOf_spec cat]
+    decreasing_tactic
 
 instance : ToStrataFormat SyntaxCat where
   mformat := SyntaxCat.mformat
@@ -361,17 +364,20 @@ private partial def Operation.mformatM (op : Operation) : FormatM PrecFormat :=
   match (← read).getOpDecl op.name with
   | some decl =>
     let bindings := decl.argDecls
-    let args := op.args
-    let .isTrue bsize := decEq args.size bindings.size
+    let .isTrue bsize := decEq op.args.size bindings.size
           | return panic! "Mismatch betweeen binding and arg size"
-    let argsV : Vector Arg bindings.size := ⟨args, bsize⟩
-    let argResults := formatArguments (← read) (← get) bindings argsV
+    let args : Vector _ bindings.size := ⟨op.args, bsize⟩
+    let argResults := formatArguments (← read) (← get) bindings args
     let fmt := ppOp (← read).opts decl.syntaxDef (Prod.fst <$> argResults)
     match decl.metadata.resultLevel bindings.size with
     | some idx => set argResults[idx]!.snd
     | none => pure ()
     for b in decl.newBindings do
-      modify (·.pushBinding <| b.varName argsV)
+      match args[b.nameIndex.toLevel] with
+      | .ident e =>
+        modify (·.pushBinding e)
+      | _ =>
+        return panic! s!"Expected ident at {b.nameIndex.toLevel}."
     return fmt
   | none =>
     -- FIXME: Consider reporting error here.
@@ -448,7 +454,7 @@ end ArgDecl
 
 namespace ArgDecls
 
-private def mformatAux (f : Format) (c : FormatContext) (s : FormatState) (a : Array ArgDecl) (idx : Nat) : Format × FormatState :=
+private def mformatAux (f : Format) (c : FormatContext) (s : FormatState) (a : ArgDecls) (idx : Nat) : Format × FormatState :=
   if h : idx < a.size then
     let b := a[idx]
     mformatAux (f ++ ", " ++ cformat b c s) c (s.pushBinding b.ident) a (idx + 1)
@@ -467,7 +473,7 @@ instance : ToStrataFormat ArgDecls where
 
 /- Format `fmt` in a context with additional bindings `b`. -/
 protected def formatIn [ToStrataFormat α] (b : ArgDecls) (fmt : α) : StrataFormat := fun c s =>
-  mformat fmt c (b.foldl (init := s) (·.pushBinding ·.ident))
+  mformat fmt c (b.toArray.foldl (init := s) (·.pushBinding ·.ident))
 
 end ArgDecls
 
diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean
index a93e4e7f..ab048382 100644
--- a/Strata/DDM/Integration/Lean/Gen.lean
+++ b/Strata/DDM/Integration/Lean/Gen.lean
@@ -12,16 +12,15 @@ import Strata.DDM.Integration.Lean.OfAstM
 import Strata.DDM.Integration.Lean.Quote
 import Strata.DDM.Util.Graph.Tarjan
 
-open Lean (Command Name Ident Term TSyntax getEnv logError profileitM quote withTraceNode)
+open Lean (Command Name Ident Term TSyntax getEnv logError profileitM quote withTraceNode mkIdentFrom)
 open Lean.Elab (throwUnsupportedSyntax)
 open Lean.Elab.Command (CommandElab CommandElabM elabCommand)
-open Lean.Elab.Term (mkFreshIdent)
 open Lean.MonadOptions (getOptions)
 open Lean.MonadResolveName (getCurrNamespace)
 open Lean.Parser.Command (ctor)
 open Lean.Parser.Term (bracketedBinderF doSeqItem matchAltExpr)
 open Lean.Parser.Termination (terminationBy suffix)
-open Lean.Syntax (mkStrLit)
+open Lean.Syntax (mkApp mkCApp mkStrLit)
 
 namespace Strata
 
@@ -54,6 +53,8 @@ private def vecLit [Monad m] [Lean.MonadQuotation m] (as : Array Term) : m Term
 abbrev LeanCategoryName := Lean.Name
 
 structure GenContext where
+  -- Syntax for #strata_gen for source location purposes.
+  src : Lean.Syntax
   categoryNameMap : Std.HashMap QualifiedIdent String
   exprHasEta : Bool
 
@@ -61,6 +62,26 @@ abbrev GenM := ReaderT GenContext CommandElabM
 
 def runCmd {α} (act : CommandElabM α) : GenM α := fun _ => act
 
+/-- Create a fresh name. -/
+private def genFreshLeanName (s : String) : GenM Name := do
+  let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
+  let n : Name := .anonymous |>.str s
+  return Lean.addMacroScope (← getEnv).mainModule n fresh
+
+/-- Create a fresh name. -/
+private def genFreshIdentPair (s : String) : GenM (Ident × Ident) := do
+  let name ← genFreshLeanName s
+  let src := (←read).src
+  return (mkIdentFrom src name true, mkIdentFrom src name)
+
+/-- Create a canonical identifier. -/
+def mkCanIdent (src : Lean.Syntax) (val : Name) : Ident :=
+  mkIdentFrom src val true
+
+/-- Create a identifier from a name. -/
+private def genIdentFrom (name : Name) (canonical : Bool := false) : GenM Ident := do
+  return mkIdentFrom (←read).src name canonical
+
 def reservedCats : Std.HashSet String := { "Type" }
 
 structure OrderedSet (α : Type _) [BEq α] [Hashable α] where
@@ -146,7 +167,7 @@ structure DefaultCtor where
 
   This is guaranteed to be unique for the category.
   -/
-  leanName : String
+  leanNameStr : String
   /--
   The name in the Strata dialect for this constructor.  If `none`, then
   this must be an auto generated constructor.
@@ -154,6 +175,8 @@ structure DefaultCtor where
   strataName : Option QualifiedIdent
   argDecls : Array (String × SyntaxCat)
 
+def DefaultCtor.leanName (c : DefaultCtor) : Name := .str .anonymous c.leanNameStr
+
 /--
 An operation at the category level.
 -/
@@ -165,7 +188,7 @@ namespace CatOp
 
 partial def checkCat (op : QualifiedIdent) (c : SyntaxCat) : Except String Unit := do
   c.args.forM (checkCat op)
-  let f := c.head
+  let f := c.name
   if f ∈ forbiddenCategories then
     throw s!"{op.fullName} refers to unsupported category {f.fullName}."
 
@@ -181,7 +204,7 @@ def ofArgDecl (op : QualifiedIdent) (d : ArgDecl) : Except String (String × Syn
 
 def ofOpDecl (d : DialectName) (o : OpDecl) : Except String CatOp := do
   let name := ⟨d, o.name⟩
-  let argDecls ← o.argDecls |>.mapM (ofArgDecl name)
+  let argDecls ← o.argDecls.toArray |>.mapM (ofArgDecl name)
   return { name, argDecls }
 
 def ofTypeDecl (d : DialectName) (o : TypeDecl) : CatOp := {
@@ -189,14 +212,13 @@ def ofTypeDecl (d : DialectName) (o : TypeDecl) : CatOp := {
   argDecls := o.argNames |>.map fun nm => ⟨nm, .atom q`Init.Type⟩
 }
 
-end CatOp
-
-
-def CatOp.ofFunctionDecl (d : DialectName) (o : FunctionDecl) : Except String CatOp := do
+def ofFunctionDecl (d : DialectName) (o : FunctionDecl) : Except String CatOp := do
   let name := ⟨d, o.name⟩
-  let argDecls ← o.argDecls |>.mapM (ofArgDecl name)
+  let argDecls ← o.argDecls.toArray |>.mapM (ofArgDecl name)
   return { name, argDecls }
 
+end CatOp
+
 /--
 This maps names of categories that we are going to declare to
 the list of operators in that category.
@@ -258,13 +280,7 @@ def addDecl (d : DialectName) (decl : Decl) : CatOpM Unit :=
       .addError msg
   match decl with
   | .syncat decl =>
-    if d = "Init" ∧ decl.name = "TypeP" then do
-      let cat := q`Init.TypeP
-      addCatM ⟨d, decl.name⟩
-      addOpM cat { name := q`Init.type, argDecls := #[] }
-      addOpM cat { name := q`Init.expr, argDecls := #[("type", .atom q`Init.Type)] }
-    else
-      addCatM ⟨d, decl.name⟩
+    addCatM ⟨d, decl.name⟩
   | .op decl => do
     if decl.category ∈ ignoredCategories ∨ decl.category ∈ specialCategories then
       if d ≠ "Init" then
@@ -310,11 +326,14 @@ namespace SyntaxCat
 Invoke `f` over all atomic (no argument) category names in `c`.
 -/
 private
-def foldOverAtomicCategories {α} (c : SyntaxCat) (init : α)  (f : α  → QualifiedIdent → α) : α := aux c init false
-  where aux (c : SyntaxCat) (init : α) (hasArg : Bool) :=
-          match c with
-          | .atom i => if hasArg then init else f init i
-          | .app d e => aux d (aux e init false) true
+def foldOverAtomicCategories {α} (cat : SyntaxCat) (init : α)  (f : α  → QualifiedIdent → α) : α :=
+  if cat.args.size = 0 then
+    f init cat.name
+  else
+    cat.args.foldl (init := init) fun v a => foldOverAtomicCategories a v f
+decreasing_by
+  rw [sizeOf_spec cat]
+  decreasing_tactic
 
 end SyntaxCat
 
@@ -350,12 +369,16 @@ partial def mkUsedCategories.aux (m : CatOpMap) (s : WorkSet CategoryName) : Cat
   match s.pop with
   | none => s.set
   | some (s, c) =>
-    let ops := m.getD c #[]
-    let addArgs {α:Type} (f : α → CategoryName → α) (a : α) (op : CatOp) :=
-      op.argDecls.foldl (init := a) fun r (_, c) => c.foldOverAtomicCategories (init := r) f
-    let addName (pa : WorkSet CategoryName) c := pa.add c
-    let s := ops.foldl (init := s) (addArgs addName)
-    mkUsedCategories.aux m s
+    match c with
+    | q`Init.TypeP =>
+      mkUsedCategories.aux m (s.add q`Init.Type)
+    | _ =>
+      let ops := m.getD c #[]
+      let addArgs {α:Type} (f : α → CategoryName → α) (a : α) (op : CatOp) :=
+        op.argDecls.foldl (init := a) fun r (_, c) => c.foldOverAtomicCategories (init := r) f
+      let addName (pa : WorkSet CategoryName) (c : CategoryName) := pa.add c
+      let s := ops.foldl (init := s) (addArgs addName)
+      mkUsedCategories.aux m s
 
 def mkUsedCategories (m : CatOpMap) (d : Dialect) : CategorySet :=
   let dname := d.name
@@ -378,10 +401,8 @@ def mkUsedCategories (m : CatOpMap) (d : Dialect) : CategorySet :=
 def mkStandardCtors (exprHasEta : Bool) (cat : QualifiedIdent) : Array DefaultCtor :=
   match cat with
   | q`Init.Expr =>
-    let fvarCtor : DefaultCtor := .mk "fvar" none #[("idx", .atom q`Init.Num)]
     if exprHasEta then
       #[
-        fvarCtor,
         .mk "bvar" none #[("idx", .atom q`Init.Num)],
         .mk "lambda" none #[
           ("var", .atom q`Init.Str),
@@ -390,68 +411,56 @@ def mkStandardCtors (exprHasEta : Bool) (cat : QualifiedIdent) : Array DefaultCt
         ]
       ]
     else
-      #[
-        fvarCtor
-      ]
-      /-
-  | q`Init.TypeP =>
-    #[ .mk "type" none #[],
-       .mk "expr" none #[("type", .atom q`Init.Type)]
-    ]-/
+      #[]
   | _ =>
     #[]
 
-def countSimilar {α} {β} [BEq β] [Hashable β] (as : Array α) (init : Std.HashMap β Nat := {}) (f : α → β) : Std.HashMap β Nat :=
-  as.foldl (init := init) fun m a =>
-    m.alter (f a) (fun old => some (old.getD 0 + 1))
-
-def mkOpGroups (standardCtors : Array DefaultCtor) (ops : Array CatOp) : Std.HashMap String Nat :=
-  let opGroups : Std.HashMap String Nat :=
-        standardCtors.foldl (init := {}) fun m c =>
-          assert! c.leanName ∉ m
-          m.insert c.leanName 1
-  countSimilar ops (init := opGroups) (·.name.name)
+partial def genFreshName (s : Std.HashSet String) (base : String) (i : Nat) :=
+  let name := s!"{base}_{i}"
+  if name ∈ s then
+    genFreshName s base (i+1)
+  else
+    name
 
-def toDefaultOp (disambiguateCtor : String → Bool) (op : CatOp) : DefaultCtor :=
+def toDefaultOp (s : Std.HashSet String) (op : CatOp) : DefaultCtor :=
   let name := op.name
   let leanName :=
-        if disambiguateCtor name.name then
-          -- FIXME: We should ensure this is actually unique.
-          s!"{name.dialect}_{name.name}"
-        else
-          name.name
+    if name.name ∈ s then
+      let leanName := s!"{name.dialect}_{name.name}"
+      if leanName ∈ s then
+        genFreshName s name.name 0
+      else
+        leanName
+    else
+      name.name
   {
-    leanName := leanName,
-    strataName := some name,
+    leanNameStr := leanName,
+    strataName := some op.name,
     argDecls := op.argDecls
   }
 
-
-def mkCategoryCtors (standardCtors : Array DefaultCtor) (ops : Array CatOp) : Array DefaultCtor :=
-  let opGroups := mkOpGroups standardCtors ops
-  standardCtors ++ ops.map (toDefaultOp (opGroups.getD · 0 > 1))
-
-def mkCategories (catMap : CatOpMap) (exprHasEta : Bool) : Array (QualifiedIdent × Array DefaultCtor) :=
-  catMap.fold (init := #[]) fun a cat ops =>
-    if cat ∈ declaredCategories then
-      a
-    else
-      let standardCtors := mkStandardCtors exprHasEta cat
-      let allCtors := mkCategoryCtors standardCtors ops
-      a.push (cat, allCtors)
-
 def CatOpMap.onlyUsedCategories (m : CatOpMap) (d : Dialect) (exprHasEta : Bool) : Array (QualifiedIdent × Array DefaultCtor) :=
   let usedSet := mkUsedCategories m d
   m.fold (init := #[]) fun a cat ops =>
     if cat ∉ declaredCategories ∧ cat ∈ usedSet then
+      let usedNames : Std.HashSet String :=
+            match cat with
+            | q`Init.Expr => { "fvar" }
+            | _ => {}
       let standardCtors := mkStandardCtors exprHasEta cat
-      let allCtors := mkCategoryCtors standardCtors ops
+      let usedNames : Std.HashSet String :=
+        standardCtors.foldl (init := usedNames) fun m c =>
+          assert! c.leanNameStr ∉ m
+          m.insert c.leanNameStr
+      let (allCtors, _) := ops.foldl (init := (standardCtors, usedNames)) fun (a, s) op =>
+            let dOp := toDefaultOp s op
+            (a.push dOp, s.insert dOp.leanNameStr)
       a.push (cat, allCtors)
     else
       a
 
-/- Creates a local variable name from a string -/
-def mkLocalIdent (name : String) : Ident :=
+/- Returns an identifier from a string. -/
+def localIdent (name : String) : Ident :=
   let dName := .anonymous |>.str name
   .mk (.ident .none name.toSubstring dName [])
 
@@ -474,10 +483,16 @@ def orderedSyncatGroups (categories : Array (QualifiedIdent × Array DefaultCtor
   let g : OutGraph n :=
         categories.foldl (init := g) fun g (cat, ops) => Id.run do
           let some resIdx := getIndex cat
-            | panic! s!"Unknown category {cat.fullName}"
-          ops.foldl (init := g) fun g op =>
-            op.argDecls.foldl (init := g) fun g (_, c) =>
-              addArgIndices cat op.leanName c g resIdx
+            | panic! s!"Unknown category {cat}"
+          match cat with
+          | q`Init.TypeP =>
+            let some typeIdx := getIndex q`Init.Type
+              | panic! s!"Unknown category Init.Type."
+            g.addEdge typeIdx resIdx
+          | _ =>
+            ops.foldl (init := g) fun g op =>
+              op.argDecls.foldl (init := g) fun g (_, c) =>
+                addArgIndices cat op.leanNameStr c g resIdx
   let indices := OutGraph.tarjan g
   indices.map (·.map (categories[·]))
 
@@ -501,6 +516,20 @@ def mkCategoryIdent (scope : Name) (name : Name) : Ident :=
         aux p' (.str .anonymous v :: r)
   aux name []
 
+/--
+Prepend the current namespace to the Lean name and convert to an identifier.
+-/
+def scopedIdent (scope subName : Lean.Name) : Ident :=
+  let name := scope ++ subName
+  let nameStr := toString subName
+  .mk (.ident .none nameStr.toSubstring subName [.decl name []])
+
+/--
+Prepend the current namespace to the Lean name and convert to an identifier.
+-/
+def mkScopedIdent {m} [Monad m] [Lean.MonadResolveName m] (subName : Lean.Name) : m Ident :=
+  (scopedIdent · subName) <$> getCurrNamespace
+
 /-- Return identifier for operator with given name to suport category. -/
 def getCategoryScopedName (cat : QualifiedIdent) : GenM Name := do
   match (←read).categoryNameMap[cat]? with
@@ -515,17 +544,28 @@ def getCategoryIdent (cat : QualifiedIdent) : GenM Ident := do
     return mkRootIdent nm
   currScopedIdent (← getCategoryScopedName cat)
 
+def getCategoryTerm (cat : QualifiedIdent) : GenM Term := do
+  mkScopedIdent (← getCategoryScopedName cat)
+
 /-- Return identifier for operator with given name to suport category. -/
-def getCategoryOpIdent (cat : QualifiedIdent) (name : String) : GenM Ident := do
-  currScopedIdent <| (← getCategoryScopedName cat) |>.str name
+def getCategoryOpIdent (cat : QualifiedIdent) (name : Name) : GenM Ident := do
+  currScopedIdent <| (← getCategoryScopedName cat) ++ name
 
 partial def ppCat (c : SyntaxCat) : GenM Term := do
   let args ← c.args.mapM ppCat
-  match c.head, args with
-  | q`Init.CommaSepBy, #[c] => ``(Array $c)
-  | q`Init.Option, #[c] => ``(Option $c)
-  | q`Init.Seq, #[c] => ``(Array $c)
-  | cat, #[] => getCategoryIdent cat
+  match c.name, eq : args.size with
+  | q`Init.CommaSepBy, 1 =>
+    return mkCApp ``Array #[args[0]]
+  | q`Init.Option, 1 =>
+    return mkCApp ``Option #[args[0]]
+  | q`Init.Seq, 1 =>
+    return mkCApp ``Array #[args[0]]
+  | cat, 0 =>
+    match declaredCategories[cat]? with
+    | some nm =>
+      pure <| mkRootIdent nm
+    | none => do
+      getCategoryTerm cat
   | f, _ => throwError "Unsupported {f.fullName}"
 
 def elabCommands (commands : Array Command) : CommandElabM Unit := do
@@ -557,20 +597,36 @@ def elabCommands (commands : Array Command) : CommandElabM Unit := do
 
 abbrev BracketedBinder := TSyntax ``Lean.Parser.Term.bracketedBinder
 
-def genBinder (name : String) (typeStx : Term) : CommandElabM BracketedBinder := do
-  let nameStx := mkLocalIdent name
+def explicitBinder (name : String) (typeStx : Term) : CommandElabM BracketedBinder := do
+  let nameStx := localIdent name
   `(bracketedBinderF| ($nameStx : $typeStx))
 
 def genCtor (op : DefaultCtor) : GenM (TSyntax ``ctor) := do
-  let ctorId : Ident := mkLocalIdent op.leanName
+  let ctorId : Ident := localIdent op.leanNameStr
   let binders ← op.argDecls.mapM fun (name, tp) => do
-        genBinder name (← ppCat tp)
+        explicitBinder name (← ppCat tp)
   `(ctor| | $ctorId:ident $binders:bracketedBinder* )
 
 def mkInductive (cat : QualifiedIdent) (ctors : Array DefaultCtor) : GenM Command := do
-  let ident ←  getCategoryIdent cat
+  assert! cat ∉ declaredCategories
+  let ident ← mkScopedIdent (← getCategoryScopedName cat)
   trace[Strata.generator] "Generating {ident}"
+  let builtinCtors : Array (TSyntax ``ctor) ←
+        match cat with
+        | q`Init.Expr => do
+            pure #[
+              ← `(ctor| | $(localIdent "fvar"):ident (idx : Nat))
+            ]
+        | q`Init.TypeP => do
+          let typeIdent ← getCategoryTerm q`Init.Type
+          pure #[
+              ← `(ctor| | $(localIdent "expr"):ident (tp : $typeIdent)),
+              ← `(ctor| | $(localIdent "type"):ident)
+          ]
+        | _ =>
+          pure #[]
   `(inductive $ident : Type where
+    $builtinCtors:ctor*
     $(← ctors.mapM genCtor):ctor*
     deriving Repr)
 
@@ -592,153 +648,191 @@ def toAstIdentM (cat : QualifiedIdent) : GenM Ident := do
 def ofAstIdentM (cat : QualifiedIdent) : GenM Ident := do
   currScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst
 
-def argCtor (v : Ident) (i : SyntaxCat) : GenM Term :=
-  match i with
-  | .atom qid@q`Init.Expr => do
-    let toAst ← toAstIdentM qid
-    ``(Arg.expr ($toAst $v))
-  | .atom q`Init.Ident => ``(Arg.ident $v)
-  | .atom q`Init.Num => ``(Arg.num $v)
-  | .atom q`Init.Decimal => ``(Arg.decimal $v)
-  | .atom q`Init.Str => ``(Arg.strlit $v)
-  | .atom qid@q`Init.Type => do
-    let toAst ← toAstIdentM qid
+partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) : GenM Term := do
+  let v := mkIdentFrom (←read).src vn
+  match cat.name with
+  | q`Init.Expr => do
+    let toAst ← toAstIdentM cat.name
+    return mkCApp ``Arg.expr #[mkApp toAst #[v]]
+  | q`Init.Ident =>
+    return mkCApp ``Arg.ident #[v]
+  | q`Init.Num =>
+    return mkCApp ``Arg.num #[v]
+  | q`Init.Decimal =>
+    return mkCApp ``Arg.decimal #[v]
+  | q`Init.Str =>
+    return mkCApp ``Arg.strlit #[v]
+  | q`Init.Type => do
+    let toAst ← toAstIdentM cat.name
     ``(Arg.type ($toAst $v))
-  | .atom qid@q`Init.TypeP => do
-    let toAst ← toAstIdentM qid
+  | q`Init.TypeP => do
+    let toAst ← toAstIdentM cat.name
     ``($toAst $v)
-  | .atom qid => do
+  | q`Init.CommaSepBy => do
+    assert! cat.args.size = 1
+    let c := cat.args[0]!
+    let e ← genFreshLeanName "e"
+    let canE ← genIdentFrom e (canonical := true)
+    let t ← toAstApplyArg e c
+    let args := mkCApp ``Array.map #[
+          ←`(fun ⟨$canE, _⟩ => $t),
+          mkCApp ``Array.attach #[v]
+    ]
+    return mkCApp ``Arg.commaSepList #[args]
+  | q`Init.Option => do
+    assert! cat.args.size = 1
+    let c := cat.args[0]!
+    let e ← genFreshLeanName "e"
+    let canE ← genIdentFrom e (canonical := true)
+    let t ← toAstApplyArg e c
+    let args := mkCApp ``Option.map #[
+          ←`(fun ⟨$canE, _⟩ => $t),
+          mkCApp ``Option.attach #[v]
+    ]
+    return mkCApp ``Arg.option #[args]
+  | q`Init.Seq => do
+    assert! cat.args.size = 1
+    let c := cat.args[0]!
+    let e ← genFreshLeanName "e"
+    let canE ← genIdentFrom e (canonical := true)
+    let t ← toAstApplyArg e c
+    let args := mkCApp ``Array.map #[
+          ←`(fun ⟨$canE, _⟩ => $t),
+          mkCApp ``Array.attach #[v]
+    ]
+    return mkCApp ``Arg.seq #[args]
+  | qid => do
+    assert! cat.args.size = 0
     let toAst ← toAstIdentM qid
     ``(Arg.op ($toAst $v))
-  | .app (.atom q`Init.CommaSepBy) c => do
-    let e ← mkFreshIdent (mkLocalIdent "e")
-    let t ← argCtor e c
-    ``(Arg.commaSepList (Array.map (fun ⟨$e, _⟩ => $t) (Array.attach $v)))
-  | .app (.atom q`Init.Option) c => do
-    let e ← mkFreshIdent (mkLocalIdent "e")
-    let t ← argCtor e c
-    ``(Arg.option (Option.map (fun ⟨$e, _⟩ => $t) (Option.attach $v)))
-  | .app (.atom q`Init.Seq) c => do
-    let e ← mkFreshIdent (mkLocalIdent "e")
-    let t ← argCtor e c
-    ``(Arg.seq (Array.map (fun ⟨$e, _⟩ => $t) (Array.attach $v)))
-  | _ =>
-    throwError s!"Unexpected category {repr i}"
 
 abbrev MatchAlt := TSyntax ``Lean.Parser.Term.matchAlt
 
+def toAstBuiltinMatches (cat : QualifiedIdent) : GenM (Array MatchAlt) := do
+  let src := (←read).src
+  match cat with
+  | q`Init.Expr =>
+    let ctor ← getCategoryOpIdent cat `fvar
+    let pat : Term := mkApp ctor #[mkCanIdent src `idx]
+    let rhs := mkCApp ``Expr.fvar #[mkIdentFrom src `idx]
+    return #[← `(matchAltExpr| | $pat => $rhs)]
+  | q`Init.TypeP => do
+    let typeP ← getCategoryOpIdent cat `type
+    let typeCat := Lean.Syntax.mkCApp ``SyntaxCat.atom #[quote q`Init.Type]
+    let typeRhs := Lean.Syntax.mkCApp ``Arg.cat #[typeCat]
+    let typeN ← genFreshLeanName "type"
+    let exprP := mkApp (← getCategoryOpIdent cat `expr) #[mkCanIdent src typeN]
+    let exprRhs ← toAstApplyArg typeN (.atom q`Init.Type)
+    return #[
+      ← `(matchAltExpr| | $typeP => $typeRhs),
+      ← `(matchAltExpr| | $exprP => $exprRhs)
+    ]
+  | _ =>
+    return #[]
+
 def toAstMatch (cat : QualifiedIdent) (op : DefaultCtor) : GenM MatchAlt := do
+  let src := (←read).src
   let argDecls := op.argDecls
   let ctor : Ident ← getCategoryOpIdent cat op.leanName
-  let args : Array (Ident × SyntaxCat) ← argDecls.mapM fun (nm, c) =>
-    return (← mkFreshIdent (mkLocalIdent nm), c)
-  let pat : Term ← ``($ctor $(args.map (·.fst)):term*)
+  let args : Array (Name × SyntaxCat) ← argDecls.mapM fun (nm, c) =>
+    return (← genFreshLeanName nm, c)
+  let argTerms : Array Term := args.map fun p => mkCanIdent src p.fst
+  let pat : Term ← ``($ctor $argTerms:term*)
   let rhs : Term ←
         match cat with
         | q`Init.Expr =>
-          match op.leanName with
-          | "fvar" =>
-            assert! args.size = 1
-            ``(Expr.fvar $(args[0]!.fst))
-          | lname =>
-            let some nm := op.strataName
-              | return panic! s!"Unexpected builtin expression {lname}"
-            let init ← ``(Expr.fn $(quote nm))
-            args.foldlM (init := init) fun a (nm, tp) => do
-              let e ← argCtor nm tp
-              ``(Expr.app $a $e)
+          let lname := op.leanNameStr
+          let some nm := op.strataName
+            | return panic! s!"Unexpected builtin expression {lname}"
+          let init := mkCApp ``Expr.fn #[quote nm]
+          args.foldlM (init := init) fun a (nm, tp) => do
+            let e ← toAstApplyArg nm tp
+            return Lean.Syntax.mkCApp ``Expr.app #[a, e]
         | q`Init.Type => do
           let some nm := op.strataName
             | return panic! "Expected type name"
           let toAst ← toAstIdentM cat
-          let argTerms : Array Term ← args.mapM fun (v, _) => ``($toAst $v)
-          ``(TypeExpr.ident $(quote nm) $(← arrayLit argTerms))
-        | q`Init.TypeP => do
-          match op.leanName with
-          | "type" => ``(Arg.cat (SyntaxCat.atom $(quote q`Init.Type)))
-          | "expr" =>
-            assert! args.size = 1
-            let (nm, tp) := args[0]!
-            argCtor nm tp
-          | name =>
-            panic! s!"Unexpected operator {name}"
+          let argTerms ← arrayLit <| args.map fun (v, c) =>
+            assert! c.isType
+            Lean.Syntax.mkApp toAst #[mkIdentFrom src v]
+          pure <| Lean.Syntax.mkCApp ``TypeExpr.ident #[quote nm, argTerms]
         | _ =>
           let mName ←
             match op.strataName with
             | some n => pure n
             | none => throwError s!"Internal: Operation requires strata name"
-          let argTerms : Array Term ← args.mapM fun (nm, tp) => argCtor nm tp
-          ``(Operation.mk $(quote mName) $(← arrayLit argTerms))
+          let argTerms : Array Term ← args.mapM fun (nm, tp) => toAstApplyArg nm tp
+          pure <| mkCApp ``Operation.mk #[quote mName, ← arrayLit argTerms]
   `(matchAltExpr| | $pat => $rhs)
 
-def genToAst (cat : QualifiedIdent) (ops : Array DefaultCtor) (isRecursive : Bool) : GenM Command := do
-  let catIdent ← getCategoryIdent cat
-  let astType := categoryToAstTypeIdent cat
-  let cases : Array MatchAlt ← ops.mapM (toAstMatch cat)
+def genToAst (cat : QualifiedIdent) (ops : Array DefaultCtor) : GenM Command := do
+  let catTerm ← getCategoryTerm cat
+  let astType : Term := categoryToAstTypeIdent cat
+  let cases ← toAstBuiltinMatches cat
+  let cases : Array MatchAlt ← ops.mapM_off (init := cases) (toAstMatch cat)
   let toAst ← toAstIdentM cat
   trace[Strata.generator] "Generating {toAst}"
-  let v ← mkFreshIdent (mkLocalIdent "v")
-  let t ←
-    if isRecursive then
-      `(suffix|termination_by sizeOf $v)
-    else
-      `(suffix|)
-  `(def $toAst ($v : $catIdent) : $astType :=
-      match $v:ident with $cases:matchAlt*
-      $t:suffix)
-
-def getOfIdentArg (vnm : String) (c : SyntaxCat) : GenM Term :=
-  match c with
-  | .atom cid@q`Init.Expr => do
-    let vi ← mkFreshIdent <| mkLocalIdent <| vnm ++ "_inner"
+  let src := (←read).src
+  let v ← genFreshLeanName "v"
+  `(partial def $toAst ($(mkCanIdent src v) : $catTerm) : $astType :=
+      match $(mkIdentFrom src v):ident with $cases:matchAlt*)
+
+partial def getOfIdentArg (varName : String) (cat : SyntaxCat) (e : Term) : GenM Term := do
+  match cat.name with
+  | cid@q`Init.Expr => do
+    let (vc, vi) ← genFreshIdentPair <| varName ++ "_inner"
     let ofAst ← ofAstIdentM cid
-    ``(OfAstM.ofExpressionM fun ⟨$vi, _⟩ => $ofAst $vi)
-  | .atom q`Init.Ident => do
-    ``(OfAstM.ofIdentM)
-  | .atom q`Init.Num => do
-    ``(OfAstM.ofNumM)
-  | .atom q`Init.Decimal => do
-    ``(OfAstM.ofDecimalM)
-  | .atom q`Init.Str => do
-    ``(OfAstM.ofStrlitM)
-  | .atom cid@q`Init.Type => do
-    let vi ← mkFreshIdent <| mkLocalIdent <| vnm ++ "_inner"
+    ``(OfAstM.ofExpressionM $e fun $vc _ => $ofAst $vi)
+  | q`Init.Ident => do
+    ``(OfAstM.ofIdentM $e)
+  | q`Init.Num => do
+    ``(OfAstM.ofNumM $e)
+  | q`Init.Decimal => do
+    ``(OfAstM.ofDecimalM $e)
+  | q`Init.Str => do
+    ``(OfAstM.ofStrlitM $e)
+  | cid@q`Init.Type => do
+    let (vc, vi) ← genFreshIdentPair varName
     let ofAst ← ofAstIdentM cid
-    ``(OfAstM.ofTypeM fun ⟨$vi, _⟩ => $ofAst $vi)
-  | .atom cid@q`Init.TypeP => do
-    let vi ← mkFreshIdent <| mkLocalIdent <| vnm ++ "_inner"
+    ``(OfAstM.ofTypeM $e fun $vc _ => $ofAst $vi)
+  | cid@q`Init.TypeP => do
     let ofAst ← ofAstIdentM cid
-    ``(fun ⟨$vi, _⟩ => $ofAst $vi)
-  | .atom cid => do
-    let vi ← mkFreshIdent <| mkLocalIdent <| vnm ++ "_inner"
+    pure <| mkApp ofAst #[e]
+  | q`Init.CommaSepBy => do
+    let c := cat.args[0]!
+    let (vc, vi) ← genFreshIdentPair varName
+    let body ← getOfIdentArg varName c vi
+    ``(OfAstM.ofCommaSepByM $e fun $vc _ => $body)
+  | q`Init.Option => do
+    let c := cat.args[0]!
+    let (vc, vi) ← genFreshIdentPair varName
+    let body ← getOfIdentArg varName c vi
+    ``(OfAstM.ofOptionM $e fun $vc _ => $body)
+  | q`Init.Seq => do
+    let c := cat.args[0]!
+    let (vc, vi) ← genFreshIdentPair varName
+    let body ← getOfIdentArg "e" c vi
+    ``(OfAstM.ofSeqM $e fun $vc _ => $body)
+  | cid => do
+    assert! cat.args.isEmpty
+    let (vc, vi) ← genFreshIdentPair varName
     let ofAst ← ofAstIdentM cid
-    ``(OfAstM.ofOperationM fun ⟨$vi, _⟩ => $ofAst $vi)
-  | .app (.atom q`Init.CommaSepBy) c => do
-    let f ← getOfIdentArg (vnm ++ "_e") c
-    ``(OfAstM.ofCommaSepByM $f)
-  | .app (.atom q`Init.Option) c => do
-    let f ← getOfIdentArg (vnm ++ "_e") c
-    ``(OfAstM.ofOptionM $f)
-  | .app (.atom q`Init.Seq) c => do
-    let f ← getOfIdentArg (vnm ++ "_e") c
-    ``(OfAstM.ofSeqM $f)
-  | _ =>
-    return panic! s!"getOfIdentArg {repr c} not supported."
+    ``(OfAstM.ofOperationM $e fun $vc _ => $ofAst $vi)
 
 def ofAstArgs (argDecls : Array (String × SyntaxCat)) (argsVar : Ident) : GenM (Array Ident × Array (TSyntax ``doSeqItem)) := do
   let argCount := argDecls.size
   let args ← Array.ofFnM (n := argCount) fun ⟨i, _isLt⟩  => do
     let (vnm, c) := argDecls[i]
-    let v ← mkFreshIdent <| mkLocalIdent <| vnm ++ "_bind"
-    let rhs0 ← getOfIdentArg vnm c
-    let rhs ← ``(OfAstM.atArg $argsVar $(quote i) $rhs0)
-    let stmt ← `(doSeqItem| let $v ← $rhs:term)
-    return (v, stmt)
+    let (vc, vi) ← genFreshIdentPair <| vnm ++ "_bind"
+    let av ← ``($argsVar[$(quote i)])
+    let rhs ← getOfIdentArg vnm c av
+    let stmt ← `(doSeqItem| let $vc ← $rhs:term)
+    return (vi, stmt)
   return args.unzip
 
 def ofAstMatch (nameIndexMap : Std.HashMap QualifiedIdent Nat) (op : DefaultCtor) (rhs : Term) : GenM MatchAlt := do
   let some name := op.strataName
-    | return panic! s!"Unexpected operator {op.leanName}"
+    | return panic! s!"Unexpected operator {op.leanNameStr}"
   let some nameIndex := nameIndexMap[name]?
     | return panic! s!"Unbound operator name {name}"
   `(matchAltExpr| | Option.some $(quote nameIndex) => $rhs)
@@ -750,31 +844,27 @@ def ofAstExprMatchRhs (cat : QualifiedIdent) (argsVar : Ident) (op : DefaultCtor
   let argDecls := op.argDecls
   let argCount := argDecls.size
   let (parsedArgs, stmts) ← ofAstArgs argDecls argsVar
-  let checkExpr ← ``(OfAstM.checkArgCount $(quote nm) $(quote argCount) (Subtype.val $(argsVar)))
+  let checkExpr ← ``(OfAstM.checkArgCount $(quote nm) $(quote argCount) $argsVar)
   `(do
     let .up p ← $checkExpr:term
     $stmts:doSeqItem*
     return $ctorIdent $parsedArgs:term*)
 
-
 def ofAstExprMatch (nameIndexMap : Std.HashMap QualifiedIdent Nat)
-      (cat : QualifiedIdent) (argsVar : Ident) (op : DefaultCtor) : GenM (Option MatchAlt) := do
-  match op.leanName with
-  | "fvar" =>
-    pure none
-  | _ => do
-    let rhs ← ofAstExprMatchRhs cat argsVar op
-    some <$> ofAstMatch nameIndexMap op rhs
+      (cat : QualifiedIdent) (argsVar : Ident) (op : DefaultCtor) : GenM MatchAlt := do
+  let rhs ← ofAstExprMatchRhs cat argsVar op
+  ofAstMatch nameIndexMap op rhs
 
 def ofAstTypeArgs (argDecls : Array (String × SyntaxCat)) (argsVar : Ident) : GenM (Array Ident × Array (TSyntax ``doSeqItem)) := do
   let argCount := argDecls.size
   let ofAst ← ofAstIdentM q`Init.Type
   let args ← Array.ofFnM (n := argCount) fun ⟨i, _isLt⟩  => do
     let (vnm, _) := argDecls[i]
-    let v ← mkFreshIdent <| mkLocalIdent vnm
+    let v ← genFreshLeanName vnm
+    let src := (←read).src
     let rhs ← ``($ofAst $argsVar[$(quote i)])
-    let stmt ← `(doSeqItem| let $v ← $rhs:term)
-    return (v, stmt)
+    let stmt ← `(doSeqItem| let $(mkIdentFrom src v true) ← $rhs:term)
+    return (mkIdentFrom src v, stmt)
   return args.unzip
 
 def ofAstTypeMatchRhs (cat : QualifiedIdent) (argsVar : Ident) (op : DefaultCtor) : GenM Term := do
@@ -789,11 +879,11 @@ def ofAstTypeMatchRhs (cat : QualifiedIdent) (argsVar : Ident) (op : DefaultCtor
 
 def ofAstOpMatchRhs (cat : QualifiedIdent) (argsVar : Ident) (op : DefaultCtor) : GenM Term := do
   let some name := op.strataName
-    | return panic! s!"Unexpected operator {op.leanName}"
+    | return panic! s!"Unexpected operator {op.leanNameStr}"
   let ctorIdent ← getCategoryOpIdent cat op.leanName
   let argDecls := op.argDecls
   let argCount := argDecls.size
-  let checkExpr ← ``(OfAstM.checkArgCount $(quote name) $(quote argCount) (Subtype.val $(argsVar)))
+  let checkExpr ← ``(OfAstM.checkArgCount $(quote name) $(quote argCount) $argsVar)
   let (parsedArgs, stmts) ← ofAstArgs argDecls argsVar
   `(do
     let .up p ← $checkExpr:term
@@ -809,32 +899,35 @@ def createNameIndexMap (cat : QualifiedIdent) (ops : Array DefaultCtor) : GenM (
     match op.strataName with
     | none => map  -- Skip operators without a name
     | some name => map.insert name map.size  -- Assign the next available index
-  let ofAstNameMap ← currScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst.map
+  let ofAstNameMap ← currScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst.nameIndexMap
   let cmd ← `(def $ofAstNameMap : Std.HashMap Strata.QualifiedIdent Nat := Std.HashMap.ofList $(quote nameIndexMap.toList))
   pure (nameIndexMap, ofAstNameMap, cmd)
 
-def mkOfAstDef (cat : QualifiedIdent) (ofAst : Ident) (v : Ident) (rhs : Term) (isRecursive : Bool) : GenM Command := do
-  let catIdent ← getCategoryIdent cat
-  let t ←
-    if isRecursive ∧ false then
-      `(suffix|termination_by sizeOf $v)
-    else
-      `(suffix|)
-  `(partial def $ofAst ($v : $(categoryToAstTypeIdent cat)) : OfAstM $catIdent := $rhs $t:suffix)
+def mkOfAstDef (cat : QualifiedIdent) (ofAst : Ident) (v : Name) (rhs : Term) : GenM Command := do
+  let src := (←read).src
+  let catTerm ← getCategoryTerm cat
+  `(partial def $ofAst ($(mkCanIdent src v) : $(categoryToAstTypeIdent cat)) : OfAstM $catTerm := $rhs)
+
+def matchTypeParamOrType (a : Arg) (onTypeParam : α) (onType : TypeExpr → OfAstM α) : OfAstM α :=
+  match a with
+  | .cat (.atom q`Init.Type) => pure onTypeParam
+  | .type tp => onType tp
+  | _ => .throwExpected "Type parameter or type expression" a
 
-def genOfAst (cat : QualifiedIdent) (ops : Array DefaultCtor) (isRecursive : Bool) : GenM (Array Command × Command) := do
+def genOfAst (cat : QualifiedIdent) (ops : Array DefaultCtor) : GenM (Array Command × Command) := do
+  let src := (←read).src
   let ofAst ← ofAstIdentM cat
   trace[Strata.generator] "Generating {ofAst}"
-  let v ← mkFreshIdent (mkLocalIdent "v")
   match cat with
   | q`Init.Expr =>
-    let argsVar ← mkFreshIdent (mkLocalIdent "args")
+    let v ← genFreshLeanName "v"
+    let argsVar ← genFreshLeanName "args"
     let (nameIndexMap, ofAstNameMap, cmd) ← createNameIndexMap cat ops
-    let fvarCtorIdent ← getCategoryOpIdent cat "fvar"
-    let cases : Array MatchAlt ← ops.filterMapM (ofAstExprMatch nameIndexMap cat argsVar)
+    let fvarCtorIdent ← getCategoryOpIdent cat `fvar
+    let cases : Array MatchAlt ← ops.mapM (ofAstExprMatch nameIndexMap cat (mkIdentFrom src argsVar))
     let rhs ←
-      `(let vnf := ($v).hnf
-        let $argsVar := vnf.args
+      `(let vnf := ($(mkIdentFrom src v)).hnf
+        let $(mkCanIdent src argsVar) := vnf.args.val
         match (vnf.fn) with
         | Strata.Expr.fvar i => pure ($fvarCtorIdent i)
         | Strata.Expr.fn fnId =>
@@ -842,68 +935,65 @@ def genOfAst (cat : QualifiedIdent) (ops : Array DefaultCtor) (isRecursive : Boo
           $cases:matchAlt*
           | _ => OfAstM.throwUnknownIdentifier $(quote cat) fnId)
         | _ => pure (panic! "Unexpected argument"))
-    pure (#[cmd], ← mkOfAstDef cat ofAst v rhs isRecursive)
+    pure (#[cmd], ← mkOfAstDef cat ofAst v rhs)
   | q`Init.Type =>
-    let argsVar ← mkFreshIdent (mkLocalIdent "args")
+    let v ← genFreshLeanName "v"
+    let (argsC, argsI) ← genFreshIdentPair "args"
     let (nameIndexMap, ofAstNameMap, cmd) ← createNameIndexMap cat ops
     let cases : Array MatchAlt ← ops.mapM fun op =>
-      ofAstMatch nameIndexMap op =<< ofAstTypeMatchRhs cat argsVar op
-    let rhs ← `(match ($v) with
-      | Strata.TypeExpr.ident typeIdent $argsVar =>
-        (match ($ofAstNameMap[typeIdent]?) with
-        $cases:matchAlt*
-        | _ => OfAstM.throwUnknownIdentifier $(quote cat) typeIdent)
-      | _ => OfAstM.throwExpected "Expected type" (Arg.type $v))
-    pure (#[cmd], ← mkOfAstDef cat ofAst v rhs isRecursive)
+      ofAstMatch nameIndexMap op =<< ofAstTypeMatchRhs cat argsI op
+    let rhs ←
+      `(match ($(mkIdentFrom src v)) with
+        | Strata.TypeExpr.ident typeIdent $argsC =>
+          (match ($ofAstNameMap[typeIdent]?) with
+          $cases:matchAlt*
+          | _ => OfAstM.throwUnknownIdentifier $(quote cat) typeIdent)
+        | _ => OfAstM.throwExpected "Expected type" (Arg.type $(mkIdentFrom src v)))
+    pure (#[cmd], ← mkOfAstDef cat ofAst v rhs)
   | q`Init.TypeP =>
-    let catCtorIdent ← getCategoryOpIdent cat "type"
-    let exprCtorIdent ← getCategoryOpIdent cat "expr"
+    let v ← genFreshLeanName "v"
+    let catCtorIdent ← getCategoryOpIdent cat `type
+    let exprCtorIdent ← getCategoryOpIdent cat `expr
     let typeOfAst ← ofAstIdentM q`Init.Type
-    let rhs ← `(match $v:term with
-      | Arg.cat (SyntaxCat.atom $(quote q`Init.Type)) =>
-        return $catCtorIdent
-      | Arg.type strataType => do
-        let tp ← $typeOfAst:term strataType
-        return $exprCtorIdent tp
-      | a =>
-        OfAstM.throwExpected "Type parameter or type expression" a)
-    pure (#[], ← mkOfAstDef cat ofAst v rhs isRecursive)
+    let rhs ← ``(
+      matchTypeParamOrType $(mkIdentFrom src v) $catCtorIdent (fun tp => $exprCtorIdent <$> $typeOfAst tp)
+    )
+    pure (#[], ← mkOfAstDef cat ofAst v rhs)
   | _ =>
-    let argsVar ← mkFreshIdent (mkLocalIdent "args")
+    let v ← genFreshLeanName "v"
+    let vi := mkIdentFrom src v
+    let (argsC, argsI) ← genFreshIdentPair "args"
     let (nameIndexMap, ofAstNameMap, cmd) ← createNameIndexMap cat ops
     let cases : Array MatchAlt ← ops.mapM fun op =>
-      ofAstMatch nameIndexMap op =<< ofAstOpMatchRhs cat argsVar op
+      ofAstMatch nameIndexMap op =<< ofAstOpMatchRhs cat argsI op
     let rhs ← `(
-      let $argsVar : Strata.SizeBounded (Array Arg) $v 1 := Subtype.mk (Operation.args $v) (by
-            simp only [Strata.Operation.sizeOf_spec $v]
-            omega)
-      match ($ofAstNameMap[Operation.name $v]?) with
+      let $argsC := Operation.args $vi
+      match ($ofAstNameMap[Operation.name $vi]?) with
       $cases:matchAlt*
-      | _ => OfAstM.throwUnknownIdentifier $(quote cat) (Operation.name $v))
-    pure (#[cmd], ← mkOfAstDef cat ofAst v rhs isRecursive)
+      | _ => OfAstM.throwUnknownIdentifier $(quote cat) (Operation.name $vi))
+    pure (#[cmd], ← mkOfAstDef cat ofAst v rhs)
 
 abbrev InhabitedSet := Std.HashSet QualifiedIdent
 
 def checkInhabited (cat : QualifiedIdent) (ops : Array DefaultCtor) : StateT InhabitedSet GenM Unit := do
   if cat ∈ (←get) then
     return ()
-  let catIdent ← getCategoryIdent cat
+  let catTerm ← getCategoryTerm cat
   for op in ops do
     let inhabited ← get
     let isInhabited := op.argDecls.all fun (_, c) =>
-        match c with
-        | .atom c => c ∈ inhabited
-        | .app (.atom q`Init.Seq) _ => true
-        | .app (.atom q`Init.CommaSepBy) _ => true
-        | .app (.atom q`Init.Option) _ => true
-        | _ => panic! s!"Unknown category {repr c}"
+        match c.name with
+        | q`Init.Seq => true
+        | q`Init.CommaSepBy => true
+        | q`Init.Option => true
+        | c => c ∈ inhabited
     if !isInhabited then
       continue
-    let ctor ← getCategoryOpIdent cat op.leanName
-    let d ← `(default)
-    let e ← op.argDecls.size.foldM (init := ctor) fun _ _ e => `($e $d)
+    let ctor : Term ← getCategoryOpIdent cat op.leanName
+    let d := Lean.mkCIdent ``default
+    let e := Lean.Syntax.mkApp ctor (Array.replicate op.argDecls.size d)
     StateT.lift <| runCmd <|
-      elabCommand =<< `(instance : Inhabited $catIdent where default := $e)
+      elabCommand =<< `(instance : Inhabited $catTerm where default := $e)
     modify (·.insert cat)
     break
 
@@ -923,17 +1013,19 @@ def gen (categories : Array (QualifiedIdent × Array DefaultCtor)) : GenM Unit :
     Std.HashSet.ofArray
       declaredCategories.keysArray
   for allCtors in orderedSyncatGroups categories do
-    let newCats := Std.HashSet.ofArray <| allCtors.map (·.fst)
     let s ←
       withTraceNode `Strata.generator (fun _ =>
         return m!"Declarations group: {allCtors.map (·.fst)}") do
         -- Check if the toAst/ofAst definitions will be recursive by looking for
         -- categories that are not already in inhabited set.
-        let isRecursive := allCtors.any fun (_, ops) =>
-              ops.any fun op =>
-                op.argDecls.any fun (_, c) =>
-                  c.foldOverAtomicCategories (init := false)
-                    fun b qid => b || qid ∈ newCats
+        -- N.B. This is not used as we use partial functions, but
+        -- kept as we want to eventually switch back
+        -- let newCats := Std.HashSet.ofArray <| allCtors.map (·.fst)
+        --let _isRecursive := allCtors.any fun (_, ops) =>
+        --      ops.any fun op =>
+        --        op.argDecls.any fun (_, c) =>
+        --          c.foldOverAtomicCategories (init := false)
+        --            fun b qid => b || qid ∈ newCats
         let cats := allCtors.map (·.fst)
         profileitM Lean.Exception s!"Generating inductives {cats}" (← getOptions) do
           let inductives ← allCtors.mapM fun (cat, ctors) => do
@@ -947,18 +1039,18 @@ def gen (categories : Array (QualifiedIdent × Array DefaultCtor)) : GenM Unit :
         let inhabitedCats := inhabitedCats2
         profileitM Lean.Exception s!"Generating toAstDefs {cats}" (← getOptions) do
           let toAstDefs ← allCtors.mapM fun (cat, ctors) => do
-            genToAst cat ctors (isRecursive := isRecursive)
+            genToAst cat ctors
           runCmd <| elabCommands toAstDefs
         profileitM Lean.Exception s!"Generating ofAstDefs {cats}" (← getOptions) do
           let ofAstDefs ← allCtors.mapM fun (cat, ctors) => do
-            let (cmds, d) ← genOfAst cat ctors (isRecursive := isRecursive)
+            let (cmds, d) ← genOfAst cat ctors
             (cmds.forM elabCommand : CommandElabM Unit)
             pure d
           runCmd <| elabCommands ofAstDefs
         pure inhabitedCats
     inhabitedCats := s
 
-def runGenM (pref : String) (catNames : Array QualifiedIdent) (exprHasEta : Bool) (m : GenM α) : CommandElabM α := do
+def runGenM (src : Lean.Syntax) (pref : String) (catNames : Array QualifiedIdent) (exprHasEta : Bool) (m : GenM α) : CommandElabM α := do
   let catNameCounts : Std.HashMap String Nat :=
     catNames.foldl (init := {}) fun m k =>
       m.alter k.name (fun v => some (v.getD 0 + 1))
@@ -972,7 +1064,8 @@ def runGenM (pref : String) (catNames : Array QualifiedIdent) (exprHasEta : Bool
             i.name
     m.insert i name
   let ctx : GenContext := {
-    categoryNameMap := categoryNameMap,
+    src := src
+    categoryNameMap := categoryNameMap
     exprHasEta := exprHasEta
   }
   m ctx
@@ -980,7 +1073,8 @@ def runGenM (pref : String) (catNames : Array QualifiedIdent) (exprHasEta : Bool
 /--
 `#strata_gen ident` generates an AST for the dialect `ident`.
 
-This includes functions for
+This includes functions for converting from the standard AST to the generated AST
+and back.
 -/
 syntax (name := strataGenCmd) "#strata_gen" ident : command -- declare the syntax
 
@@ -1006,7 +1100,7 @@ def genAstImpl : CommandElab := fun stx =>
     let exprHasEta := false -- FIXME
     let cats := cm.onlyUsedCategories d exprHasEta
     let catNames := cats.map (·.fst)
-    runGenM dialectName catNames exprHasEta (gen cats)
+    runGenM stx dialectName catNames exprHasEta (gen cats)
   | _ =>
     throwUnsupportedSyntax
 
diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean
index cb581ad1..b2bd86ad 100644
--- a/Strata/DDM/Integration/Lean/OfAstM.lean
+++ b/Strata/DDM/Integration/Lean/OfAstM.lean
@@ -53,7 +53,7 @@ def throwUnknownType (e : TypeExpr) : OfAstM α :=
 /--
 Raise error when passed an argument that is not an expression when expression expected.
 -/
-def throwExpected (cat : String) (a : Arg) : OfAstM α :=
+def throwExpected {α} (cat : String) (a : Arg) : OfAstM α :=
   Except.error s!"Expected {cat} {repr a}."
 
 /--
@@ -80,7 +80,7 @@ def throwUnknownIdentifier (tp : QualifiedIdent) (f: QualifiedIdent) : OfAstM α
 
 protected def checkTypeArgCount
     (expected : Nat)
-    (args : Array TypeExpr)
+    (args : Array α)
     : OfAstM (PLift (args.size = expected)) :=
   if p : args.size = expected then
     return .up p
@@ -90,7 +90,7 @@ protected def checkTypeArgCount
 protected def checkArgCount
     (tp : QualifiedIdent)
     (expected : Nat)
-    (args : Array Arg)
+    (args : Array α)
     : OfAstM (PLift (args.size = expected)) :=
   if p : args.size = expected then
     return .up p
@@ -108,80 +108,77 @@ protected def checkEtaExprArgCount
   else
     .throwUnexpectedArgCount tp expected.size args.size
 
-def ofExpressionM {α β} [SizeOf α] {e : α} {c : Int}
-        (act : SizeBounded Expr e c → OfAstM β)
-      : SizeBounded Arg e c → OfAstM β
-| ⟨.expr a1, p⟩ => act ⟨a1, by simp at p; omega⟩
-| a => .throwExpected "expression" a.val
-
-def ofTypeM {α β} [SizeOf α] {e : α} {c : Int}
-        (act : SizeBounded TypeExpr e c → OfAstM β)
-      : SizeBounded Arg e c → OfAstM β
-| ⟨.type a1, p⟩ => act ⟨a1, by simp at p; omega⟩
-| a => .throwExpected "type" a.val
-
-def ofOperationM {α β} [SizeOf α] {e : α} {c : Int}
-        (act : SizeBounded Operation e c → OfAstM β)
-      : SizeBounded Arg e c → OfAstM β
-| ⟨.op a1, p⟩ => act ⟨a1, by simp only [Arg.op.sizeOf_spec] at p; omega⟩
-| a => .throwExpected "operation" a.val
-
-def ofIdentM {α} [SizeOf α] {e : α} {c : Int}
-      : SizeBounded Arg e c → OfAstM String
-| ⟨.ident a, _⟩ => pure a
-| a => .throwExpected "identifier" a.val
-
-def ofNumM {α} [SizeOf α] {e : α} {c : Int}
-      : SizeBounded Arg e c → OfAstM Nat
-| ⟨.num a, _⟩ => pure a
-| a => .throwExpected "numeric literal" a.val
-
-def ofDecimalM {α} [SizeOf α] {e : α} {c : Int}
-      : SizeBounded Arg e c → OfAstM Decimal
-| ⟨.decimal a, _⟩ => pure a
-| a => .throwExpected "scientific literal" a.val
-
-def ofStrlitM {α} [SizeOf α] {e : α} {c : Int}
-      : SizeBounded Arg e c → OfAstM String
-| ⟨.strlit a, _⟩ => pure a
-| a => .throwExpected "string literal" a.val
-
-def ofOptionM {α} [SizeOf α] {e : α} {c : Int}
-      (act : SizeBounded Arg e c → OfAstM β)
-      (a : SizeBounded Arg e c)
+def ofExpressionM {β} (val : Arg) (act : ∀(e : Expr), sizeOf e < sizeOf val → OfAstM β)
+  : OfAstM β :=
+  match val with
+  | .expr a1 => act a1 (by decreasing_tactic)
+  | a => .throwExpected "expression" a
+
+def ofTypeM {β}
+      (val : Arg)
+      (act : ∀(e : TypeExpr), sizeOf e < sizeOf val → OfAstM β)
+      : OfAstM β :=
+  match val with
+  | .type a1 => act a1 (by decreasing_tactic)
+  | a => .throwExpected "type" a
+
+def ofOperationM {β}
+        (val : Arg)
+        (act : ∀(o : Operation), sizeOf o < sizeOf val → OfAstM β)
+      : OfAstM β :=
+  match val with
+  | .op a1 => act a1 (by decreasing_tactic)
+  | a => .throwExpected "operation" a
+
+def ofIdentM : Arg → OfAstM String
+| .ident val => pure val
+| a => .throwExpected "identifier" a
+
+def ofNumM : Arg → OfAstM Nat
+| .num val => pure val
+| a => .throwExpected "numeric literal" a
+
+def ofDecimalM : Arg → OfAstM Decimal
+| .decimal val => pure val
+| a => .throwExpected "scientific literal" a
+
+def ofStrlitM : Arg → OfAstM String
+| .strlit val => pure val
+| a => .throwExpected "string literal" a
+
+def ofOptionM {β}
+      (arg : Arg)
+      (act : ∀(e : Arg), sizeOf e < sizeOf arg → OfAstM β)
       : OfAstM (Option β) :=
-  match a with
-  | ⟨.option none, _⟩ => pure none
-  | ⟨.option (some v), bndP⟩ => some <$> act ⟨v, by
-    simp at bndP
-    omega⟩
-  | _ => throwExpected "option" a.val
-
-def ofCommaSepByM {α} [SizeOf α] {e : α} {c : Int}
-      (act : SizeBounded Arg e c → OfAstM β)
-      (arg : SizeBounded Arg e c)
+  match arg with
+  | .option mv =>
+    match mv with
+    | none =>
+      pure none
+    | some v =>
+      some <$> act v (by decreasing_tactic)
+  | _ => throwExpected "option" arg
+
+def ofCommaSepByM {β}
+      (arg : Arg)
+      (act : ∀(e : Arg), sizeOf e < sizeOf arg → OfAstM β)
       : OfAstM (Array β) :=
   match arg with
-  | ⟨.commaSepList a, bndP⟩ =>
-    a.attach.mapM fun ⟨v, vp⟩  => do
-      act ⟨v, by
-        have p := Array.sizeOf_lt_of_mem_strict vp
-        simp at bndP
-        omega⟩
-  | _ => throwExpected "seq" arg.val
-
-def ofSeqM {α} [SizeOf α] {e : α} {c : Int}
-      (act : SizeBounded Arg e c → OfAstM β)
-      (arg : SizeBounded Arg e c)
+  | .commaSepList a => do
+    let val ← a.attach.mapM fun ⟨v, vIn⟩  => do
+      act v (by decreasing_tactic)
+    pure val
+  | _ => throwExpected "seq" arg
+
+def ofSeqM {β}
+      (arg : Arg)
+      (act : ∀(e : Arg), sizeOf e < sizeOf arg → OfAstM β)
       : OfAstM (Array β) :=
   match arg with
-  | ⟨.seq a, bndP⟩ =>
-    a.attach.mapM fun ⟨v, vp⟩  => do
-      act ⟨v, by
-        have p := Array.sizeOf_lt_of_mem_strict vp
-        simp at bndP
-        omega⟩
-  | _ => throwExpected "seq" arg.val
+  | .seq a => do
+    a.attach.mapM fun ⟨v, vIn⟩ =>
+      act v (by decreasing_tactic)
+  | _ => throwExpected "seq" arg
 
 /--
 Get the expression at index `lvl` in the arguments.
@@ -205,7 +202,7 @@ Get the expression at index `lvl` in the arguments.
 
 Note that in conversion, we will
 -/
-def exprEtaArg [HasEta α T] {e : Expr} {n : Nat} (as : SizeBounded (Array Arg) e 1) (_ : as.val.size ≤ n) (lvl : Nat)
+def exprEtaArg{α T} [HasEta α T] {e : Expr} {n : Nat} (as : SizeBounded (Array Arg) e 1) (_ : as.val.size ≤ n) (lvl : Nat)
         (act : (s : Expr) → sizeOf s < sizeOf e → OfAstM α) :
         OfAstM α :=
   if lvlP : lvl < as.val.size then
diff --git a/Strata/DDM/Integration/Lean/Quote.lean b/Strata/DDM/Integration/Lean/Quote.lean
index a2723282..acc02908 100644
--- a/Strata/DDM/Integration/Lean/Quote.lean
+++ b/Strata/DDM/Integration/Lean/Quote.lean
@@ -56,9 +56,13 @@ end
 
 namespace SyntaxCat
 
-protected def quote : SyntaxCat → Term
-| .atom a => Syntax.mkCApp ``SyntaxCat.atom #[quote a]
-| .app f a => Syntax.mkCApp ``SyntaxCat.app #[f.quote, a.quote]
+protected def quote (cat : SyntaxCat) : Term :=
+  let r := quoteArray <| cat.args.map fun x => x.quote
+  astQuote! SyntaxCat.mk (quote cat.name) r
+termination_by sizeOf cat
+decreasing_by
+  simp [sizeOf_spec cat]
+  decreasing_tactic
 
 instance : Quote SyntaxCat where
   quote := SyntaxCat.quote
@@ -192,6 +196,9 @@ instance : Quote SyntaxDef where
 
 end SyntaxDef
 
+instance : Quote ArgDecls where
+  quote a :=  Syntax.mkCApp ``ArgDecls.ofArray #[quote a.toArray]
+
 instance : Quote SynCatDecl where
   quote d :=  Syntax.mkCApp ``SynCatDecl.mk #[quote d.name, quote d.argNames]
 
diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean
index 0d6757ce..e900d8ec 100644
--- a/Strata/DDM/Integration/Lean/ToExpr.lean
+++ b/Strata/DDM/Integration/Lean/ToExpr.lean
@@ -62,12 +62,17 @@ end
 
 namespace SyntaxCat
 
-protected def toExpr : SyntaxCat → Lean.Expr
-| .atom a => mkApp (mkConst ``SyntaxCat.atom) (toExpr a)
-| .app f a => mkApp2 (mkConst ``SyntaxCat.app) (f.toExpr) (a.toExpr)
+protected def typeExpr : Lean.Expr := astExpr! SyntaxCat
+
+protected def toExpr (cat : SyntaxCat) : Lean.Expr :=
+  let args := arrayToExpr SyntaxCat.typeExpr (cat.args.map fun e => e.toExpr)
+  astExpr! mk (toExpr cat.name) args
+decreasing_by
+  simp [SyntaxCat.sizeOf_spec cat]
+  decreasing_tactic
 
 instance : ToExpr SyntaxCat where
-  toTypeExpr := mkConst ``SyntaxCat
+  toTypeExpr := SyntaxCat.typeExpr
   toExpr := SyntaxCat.toExpr
 
 end SyntaxCat
@@ -187,12 +192,15 @@ instance : ToExpr MetadataArg where
 end MetadataArg
 
 instance MetadataAttr.instToExpr : ToExpr MetadataAttr where
-  toTypeExpr := mkConst ``MetadataAttr
+  toTypeExpr := astExpr! MetadataAttr
   toExpr a := astExpr! MetadataAttr.mk (toExpr a.ident) (toExpr a.args)
 
 instance Metadata.instToExpr : ToExpr Metadata where
-  toTypeExpr := mkConst ``Metadata
-  toExpr m := astExpr! Metadata.ofArray (toExpr m.toArray)
+  toTypeExpr := astExpr! Metadata
+  toExpr m :=
+    let init := astExpr! Metadata.empty
+    let push := astExpr! Metadata.push
+    m.toArray.foldl (init := init) fun m a => push m (toExpr a)
 
 namespace ArgDeclKind
 
@@ -295,6 +303,10 @@ def toExpr {argDecls} (bi : BindingSpec argDecls) (argDeclsExpr : Lean.Expr) : L
 
 end BindingSpec
 
+instance ArgDecls.instToExpr : ToExpr ArgDecls where
+  toTypeExpr := astExpr! ArgDecls
+  toExpr a := astExpr! ArgDecls.ofArray (toExpr a.toArray)
+
 namespace OpDecl
 
 instance : ToExpr OpDecl where
diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean
index aab5a89f..0f7cd178 100644
--- a/Strata/DDM/Ion.lean
+++ b/Strata/DDM/Ion.lean
@@ -326,21 +326,25 @@ end QualifiedIdent
 
 namespace SyntaxCat
 
-def toIon : SyntaxCat → Array (Ion SymbolId) → Ion.InternM (Ion SymbolId)
-| .atom sym, a =>
-  return .sexp (#[(← sym.toIon)] ++ a)
-| .app f x, a => do
-  f.toIon <| a.push <| ←x.toIon #[]
+protected def toIon (cat : SyntaxCat) : Ion.InternM (Ion SymbolId) := do
+  let args := #[ ← cat.name.toIon ]
+  let args ← cat.args.attach.mapM_off (init := args) fun ⟨e, _⟩ => e.toIon
+  return .sexp args
+decreasing_by
+  rw [SyntaxCat.sizeOf_spec cat]
+  decreasing_tactic
 
 protected def fromIon (v : Ion SymbolId) : FromIonM SyntaxCat := do
-  let ⟨args, p⟩ ← .asSexp "Category" v
-  let init ← .atom <$> QualifiedIdent.fromIon "Category name" args[0]
-  args.attach.foldlM (start := 1) (init := init) fun a ⟨u, _⟩ => do
-    let c ← SyntaxCat.fromIon u
-    return .app a c
+  let ⟨args, p⟩ ← .asSexp "Category reference" v
+  let name ← QualifiedIdent.fromIon "Category name" args[0]
+  let args ← args.attach.mapM_off (start := 1) fun ⟨e, _⟩ => SyntaxCat.fromIon e
+  return {
+    name := name
+    args := args
+  }
 termination_by v
 decreasing_by
-  have _ : sizeOf u < sizeOf args := by decreasing_tactic
+  have p : sizeOf e < sizeOf args := by decreasing_tactic
   decreasing_tactic
 
 instance : FromIon SyntaxCat where
@@ -456,7 +460,7 @@ protected def Arg.toIon (refs : SymbolIdCache) (arg : Arg) : InternM (Ion Symbol
     | .expr e =>
       return .sexp #[ ionSymbol! "expr", ← e.toIon (ionRefEntry! ``Expr) ]
     | .cat c =>
-      return .sexp #[ ionSymbol! "cat", ← c.toIon #[] ]
+      return .sexp #[ ionSymbol! "cat", ← c.toIon ]
     | .type e =>
       return .sexp #[ ionSymbol! "type", ← e.toIon (ionRefEntry! ``TypeExpr) ]
     | .ident s  =>
@@ -812,7 +816,7 @@ instance : CachedToIon ArgDeclKind where
   cachedToIon refs tpc := ionScope! ArgDeclKind refs :
   match tpc with
   | .cat k =>
-    return .sexp #[ionSymbol! "category", ← k.toIon #[]]
+    return .sexp #[ionSymbol! "category", ← k.toIon]
   | .type tp =>
     return .sexp #[ionSymbol! "type", ← ionRef! tp]
 
@@ -943,7 +947,7 @@ instance : CachedToIon OpDecl where
       (ionSymbol! "name", .string d.name),
     ]
     if d.argDecls.size > 0 then
-      let v ← d.argDecls.mapM (fun (de : ArgDecl) => ionRef! de)
+      let v ← d.argDecls.toArray.mapM (fun (de : ArgDecl) => ionRef! de)
       flds := flds.push (ionSymbol! "args", .list v)
     flds := flds.push (ionSymbol! "result", ← d.category.toIon)
     flds := flds.push (ionSymbol! "syntax",   ← ionRef! d.syntaxDef)
@@ -965,7 +969,7 @@ protected def fromIon (fields : Array (SymbolId × Ion SymbolId)) : FromIonM OpD
   let argDecls ←
         match fldArgs[2] with
         | .null _ => pure .empty
-        | v => .asListOf "Op declaration arguments" v fromIon
+        | v => ArgDecls.ofArray <$> .asListOf "Op declaration arguments" v fromIon
   let category ← QualifiedIdent.fromIon "Op declaration result" fldArgs[3]
   let syntaxDef ←
         match fldArgs[4] with
@@ -1015,7 +1019,7 @@ instance : CachedToIon FunctionDecl where
       (ionSymbol! "name", .string d.name),
     ]
     if d.argDecls.size > 0 then
-      let v ← d.argDecls.mapM (fun (de : ArgDecl) => ionRef! de)
+      let v ← d.argDecls.toArray.mapM (fun (de : ArgDecl) => ionRef! de)
       flds := flds.push (ionSymbol! "args", .list v)
     flds := flds.push (ionSymbol! "returns", ← ionRef! d.result)
     flds := flds.push (ionSymbol! "syntax", ← ionRef! d.syntaxDef)
@@ -1036,7 +1040,7 @@ protected def fromIon (fields : Array (SymbolId × Ion SymbolId)) : FromIonM Fun
   let argDecls ←
         match fldArgs[2] with
         | .null _ => pure .empty
-        | .list a => Array.mapM fromIon a
+        | .list a => ArgDecls.ofArray <$> Array.mapM fromIon a
         | r => throw s!"OpDecl.args expected a list."
   let returns ← fromIon fldArgs[3]
   let syntaxDef ←
diff --git a/Strata/DDM/Parser.lean b/Strata/DDM/Parser.lean
index 5af6ef89..ce695c9f 100644
--- a/Strata/DDM/Parser.lean
+++ b/Strata/DDM/Parser.lean
@@ -684,30 +684,32 @@ def checkLeftRec (thisCatName : QualifiedIdent) (argDecls : ArgDecls) (as : List
   | .ident v argPrec :: rest => Id.run do
     let .isTrue lt := inferInstanceAs (Decidable (v < argDecls.size))
       | return panic! "Invalid index"
-    match argDecls[v].kind.categoryOf with
-    | .app (.atom (q`Init.CommaSepBy)) (.atom c) =>
-      if c == thisCatName then
+    let cat := argDecls[v].kind.categoryOf
+    match cat.name with
+    | q`Init.CommaSepBy =>
+      assert! cat.args.size = 1
+      let c := cat.args[0]!
+      if c.name == thisCatName then
         .invalid mf!"Leading symbol cannot be recursive call to {c}"
       else
         .isLeading as
-    | .app (.atom (q`Init.Many)) (.atom c) =>
-      if c == thisCatName then
+    | q`Init.Option =>
+      assert! cat.args.size = 1
+      let c := cat.args[0]!
+      if c.name == thisCatName then
         .invalid mf!"Leading symbol cannot be recursive call to {c}"
       else
         .isLeading as
-    | .app (.atom (q`Init.Option)) (.atom c) =>
-      if c == thisCatName then
+    | q`Init.Seq =>
+      assert! cat.args.size = 1
+      let c := cat.args[0]!
+      if c.name == thisCatName then
         .invalid mf!"Leading symbol cannot be recursive call to {c}"
       else
         .isLeading as
-    | .app (.atom (q`Init.Seq)) (.atom c) =>
-      if c == thisCatName then
-        .invalid mf!"Leading symbol cannot be recursive call to {c}"
-      else
-        .isLeading as
-    | .app c _ =>
-      panic! s!"Unknown parametric category '{eformat c}' is not supported."
-    | .atom qid =>
+    | qid =>
+      if cat.args.size > 0 then
+        panic! s!"Unknown parametric category '{eformat cat}' is not supported."
       if qid == thisCatName then
         .isTrailing (min (argPrec+1) maxPrec) rest
       else
@@ -774,19 +776,22 @@ def manyParser (p : Parser) : Parser := {
 }
 
 /-- Parser function for given syntax category -/
-def catParser (ctx : ParsingContext) (cat : SyntaxCat) : Except SyntaxCat Parser :=
-  match cat with
-  | .app (.atom (q`Init.CommaSepBy)) c =>
-    (sepByParser · (symbolNoAntiquot ",")) <$> catParser ctx c
-  | .app (.atom (q`Init.Option)) c =>
-    optionalNoAntiquot <$> catParser ctx c
-  | .app (.atom (q`Init.Seq)) c =>
-    manyParser <$> catParser ctx c
-  | .atom c =>
-    .ok (atomCatParser ctx c)
-  | c =>
-    .error c
-
+partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) : Except SyntaxCat Parser :=
+  match cat.name with
+  | q`Init.CommaSepBy =>
+    assert! cat.args.size = 1
+    (sepByParser · (symbolNoAntiquot ",")) <$> catParser ctx cat.args[0]!
+  | q`Init.Option =>
+    assert! cat.args.size = 1
+    optionalNoAntiquot <$> catParser ctx cat.args[0]!
+  | q`Init.Seq =>
+    assert! cat.args.size = 1
+    manyParser <$> catParser ctx cat.args[0]!
+  | qid =>
+    if cat.args.isEmpty then
+      .ok (atomCatParser ctx qid)
+    else
+      .error cat
 /-
 This walks the SyntaxDefAtomParser and prepends extracted parser to state.
 
diff --git a/Strata/DDM/Util/Lean.lean b/Strata/DDM/Util/Lean.lean
index 6ec58430..7a74c841 100644
--- a/Strata/DDM/Util/Lean.lean
+++ b/Strata/DDM/Util/Lean.lean
@@ -15,7 +15,7 @@ def mkLocalDeclId (name : String) : TSyntax `Lean.Parser.Command.declId :=
   let dName := .anonymous |>.str name
   .mk (.ident .none name.toSubstring dName [])
 
-partial def mkErrorMessage (c : InputContext) (pos : String.Pos) (stk : SyntaxStack) (e : Parser.Error) : Message := Id.run do
+partial def mkErrorMessage (c : InputContext) (pos : String.Pos) (stk : SyntaxStack) (e : Parser.Error) (isSilent : Bool := false) : Message := Id.run do
   let mut pos := pos
   let mut endPos? := none
   let mut e := e
@@ -38,6 +38,7 @@ partial def mkErrorMessage (c : InputContext) (pos : String.Pos) (stk : SyntaxSt
     pos := c.fileMap.toPosition pos
     endPos := c.fileMap.toPosition <$> endPos?
     keepFullRange := true
+    isSilent := isSilent
     data := toString e }
 where
   -- Error recovery might lead to there being some "junk" on the stack
@@ -46,8 +47,8 @@ where
       if let .original (trailing := trailing) .. := stx.getTailInfo then pure (some trailing)
         else none
 
-partial def mkStringMessage (c : InputContext) (pos : String.Pos) (msg : String) : Message :=
-  mkErrorMessage c pos SyntaxStack.empty { unexpected := msg }
+partial def mkStringMessage (c : InputContext) (pos : String.Pos) (msg : String) (isSilent : Bool := false) : Message :=
+  mkErrorMessage c pos SyntaxStack.empty { unexpected := msg } (isSilent := isSilent)
 
 instance : Quote Int where
   quote
diff --git a/StrataMain.lean b/StrataMain.lean
index 061743a6..1ce06ef7 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -60,7 +60,13 @@ def readStrataText (fm : Strata.DialectFileMap) (input : System.FilePath) (bytes
       exitFailure (← Strata.mkErrorReport input s.errors)
     pure (loaded.addDialect! d, .dialect d)
 
-def readStrataIon (fm : Strata.DialectFileMap) (bytes : ByteArray) : IO (Strata.Elab.LoadedDialects × Strata.DialectOrProgram) := do
+def fileReadError {α} (path : System.FilePath) (msg : String) : IO α := do
+  IO.eprintln s!"Error reading {path}:"
+  IO.eprintln s!"  {msg}\n"
+  IO.eprintln s!"Either the file is invalid or there is a bug in Strata."
+  IO.Process.exit 1
+
+def readStrataIon (fm : Strata.DialectFileMap) (path : System.FilePath) (bytes : ByteArray) : IO (Strata.Elab.LoadedDialects × Strata.DialectOrProgram) := do
   let (hdr, frag) ←
     match Strata.Ion.Header.parse bytes with
     | .error msg =>
@@ -71,7 +77,7 @@ def readStrataIon (fm : Strata.DialectFileMap) (bytes : ByteArray) : IO (Strata.
   | .dialect dialect =>
     match ← Strata.Elab.loadDialectFromIonFragment fm .builtin #[] dialect frag with
     | (_, .error msg) =>
-      exitFailure msg
+      fileReadError path msg
     | (dialects, .ok d) =>
       pure (dialects, .dialect d)
   | .program dialect => do
@@ -83,7 +89,7 @@ def readStrataIon (fm : Strata.DialectFileMap) (bytes : ByteArray) : IO (Strata.
     | .ok pgm =>
       pure (dialects, .program pgm)
     | .error msg =>
-      exitFailure msg
+      fileReadError path msg
 
 def readFile (fm : Strata.DialectFileMap) (path : System.FilePath) : IO (Strata.Elab.LoadedDialects × Strata.DialectOrProgram) := do
   let bytes ←
@@ -92,7 +98,7 @@ def readFile (fm : Strata.DialectFileMap) (path : System.FilePath) : IO (Strata.
       exitFailure s!"Error reading {path}."
     | .ok c => pure c
   if bytes.startsWith Ion.binaryVersionMarker then
-    readStrataIon fm bytes
+    readStrataIon fm path bytes
   else
     readStrataText fm path bytes
 
diff --git a/StrataTest/DDM/Gen.lean b/StrataTest/DDM/Gen.lean
index 0f76ba27..64cc762b 100644
--- a/StrataTest/DDM/Gen.lean
+++ b/StrataTest/DDM/Gen.lean
@@ -88,37 +88,26 @@ TestDialect.MutB.opB : MutA → MutB
 #print MutB
 
 /--
-info: Strata.Expr.fvar 1
+info: inductive TestDialect.TypeP : Type
+number of parameters: 0
+constructors:
+TestDialect.TypeP.expr : TestDialectType → TypeP
+TestDialect.TypeP.type : TypeP
 -/
 #guard_msgs in
-#eval Expr.fvar 1 |>.toAst
+#print TypeP
 
 /--
-info: @[irreducible] def TestDialect.Expr.toAst : Expr → Strata.Expr :=
-Expr.toAst._proof_1.fix fun x a =>
-  (match (motive :=
-      (x : Expr) → ((y : Expr) → (invImage (fun x => sizeOf x) sizeOfWFRel).1 y x → Strata.Expr) → Strata.Expr) x with
-    | Expr.fvar a => fun x => Strata.Expr.fvar a
-    | Expr.trueExpr => fun x => Strata.Expr.fn { dialect := "TestDialect", name := "trueExpr" }
-    | a.and a_1 => fun x =>
-      ((Strata.Expr.fn { dialect := "TestDialect", name := "and" }).app (Strata.Arg.expr (x a ⋯))).app
-        (Strata.Arg.expr (x a_1 ⋯))
-    | Expr.lambda a a_1 a_2 => fun x =>
-      (((Strata.Expr.fn { dialect := "TestDialect", name := "lambda" }).app (Strata.Arg.type a.toAst)).app
-            (Strata.Arg.op a_1.toAst)).app
-        (Strata.Arg.expr (x a_2 ⋯)))
-    a
+info: Strata.Expr.fvar 1
 -/
 #guard_msgs in
-#print Expr.toAst
+#eval Expr.fvar 1 |>.toAst
 
 /--
-info: theorem TestDialect.Expr.toAst._proof_1 : WellFounded (invImage (fun x => sizeOf x) sizeOfWFRel).1 := Lean.opaqueId (invImage (fun x => sizeOf x) sizeOfWFRel).2
+info: opaque TestDialect.Expr.toAst : Expr → Strata.Expr
 -/
 #guard_msgs in
-#print Expr.toAst._proof_1
-
---#print Expr.ofStrata
+#print Expr.toAst
 
 deriving instance DecidableEq for TestDialectType
 deriving instance DecidableEq for TypeP
diff --git a/StrataTest/DDM/LoadDialect.lean b/StrataTest/DDM/LoadDialect.lean
index 726fd916..ba430a7b 100644
--- a/StrataTest/DDM/LoadDialect.lean
+++ b/StrataTest/DDM/LoadDialect.lean
@@ -19,13 +19,10 @@ error: Could not find file INVALID!
 #load_dialect "INVALID!"
 
 -- This tests that dialects must be loaded in order.
+
 /--
-error: 5 error(s) in ../../Examples/dialects/Arith.dialect.st:
+error: 1 error(s) in ../../Examples/dialects/Arith.dialect.st:
   2:7: Unknown dialect Bool
-  11:27: Undeclared type or category Bool.
-  12:27: Undeclared type or category Bool.
-  13:27: Undeclared type or category Bool.
-  14:27: Undeclared type or category Bool.
 -/
 #guard_msgs in
 #load_dialect "../../Examples/dialects/Arith.dialect.st"
diff --git a/StrataTest/DDM/TypeP.lean b/StrataTest/DDM/TypeP.lean
index a5326423..a63cf9c7 100644
--- a/StrataTest/DDM/TypeP.lean
+++ b/StrataTest/DDM/TypeP.lean
@@ -26,7 +26,7 @@ op mkBinding (name : Ident, tp : TypeP) : Binding => @[prec(40)] name ":" tp;
 info: inductive TypeP : Type
 number of parameters: 0
 constructors:
-TypeP.type : TypeP
 TypeP.expr : TestTypePType → TypeP
+TypeP.type : TypeP
 -/
 #guard_msgs in #print TypeP