From d2c3a59da7327ef75fc56e3851396ab0daa59ff0 Mon Sep 17 00:00:00 2001
From: Josh Cohen <cohenjo@amazon.com>
Date: Mon, 12 Jan 2026 11:44:53 -0500
Subject: [PATCH 1/5] Add inhabited types check and termination proof

Uses memoziation but only for provably inhabited
No tests yet
---
 Strata/DL/Lambda/LTy.lean         |   4 +
 Strata/DL/Lambda/TypeFactory.lean | 179 ++++++++++++++++++++++++++++++
 2 files changed, 183 insertions(+)

diff --git a/Strata/DL/Lambda/LTy.lean b/Strata/DL/Lambda/LTy.lean
index 296644d1a..793e18da0 100644
--- a/Strata/DL/Lambda/LTy.lean
+++ b/Strata/DL/Lambda/LTy.lean
@@ -173,6 +173,10 @@ theorem LMonoTy.size_gt_zero :
   unfold LMonoTys.size; split
   simp_all; omega
 
+theorem LMonoTy.size_lt_of_mem {ty: LMonoTy} {tys: LMonoTys} (h: ty ∈ tys):
+  ty.size <= tys.size := by
+  induction tys <;> simp only[LMonoTys.size]<;> grind
+
 /--
 Boolean equality for `LMonoTy`.
 -/
diff --git a/Strata/DL/Lambda/TypeFactory.lean b/Strata/DL/Lambda/TypeFactory.lean
index e20cb53c5..38a54735a 100644
--- a/Strata/DL/Lambda/TypeFactory.lean
+++ b/Strata/DL/Lambda/TypeFactory.lean
@@ -415,6 +415,17 @@ def TypeFactory.genFactory {T: LExprParams} [inst: Inhabited T.Metadata] [Inhabi
 def TypeFactory.getType (F : @TypeFactory IDMeta) (name : String) : Option (LDatatype IDMeta) :=
   F.find? (fun d => d.name == name)
 
+omit [DecidableEq IDMeta] [Inhabited IDMeta] in theorem TypeFactory.getType_name {F : @TypeFactory IDMeta} {name : String}
+  {l: LDatatype IDMeta}:
+  F.getType name = some l → l.name = name := by
+    unfold TypeFactory.getType; grind
+
+omit [DecidableEq IDMeta] [Inhabited IDMeta] in theorem TypeFactory.getType_mem {F : @TypeFactory IDMeta} {name : String}
+  {l: LDatatype IDMeta}:
+  F.getType name = some l → @Membership.mem (LDatatype IDMeta) (Array (LDatatype IDMeta)) _ F l := by apply Array.mem_of_find?_eq_some
+
+
+
 /--
 Add an `LDatatype` to an existing `TypeFactory`, checking that no
 types are duplicated.
@@ -428,6 +439,174 @@ def TypeFactory.addDatatype (t: @TypeFactory IDMeta) (d: LDatatype IDMeta) : Exc
               Existing Type: {d'}\n\
               New Type:{d}"
 
+---------------------------------------------------------------------
+
+-- Inhabited types
+
+/-
+Because we generate destructors, it is vital to ensure that every datatype
+is inhabited. Otherwise, we can have the following:
+```
+type Empty :=.
+type List := Nil | Cons (hd: Empty) (tl: List)
+```
+The only element of `List` is `Nil`, but we also create the destructor
+`hd : List → Empty`, which means `hd Nil` has type `Empty`, contradicting the
+fact that `Empty` is uninhabited.
+
+However, checking type inhabitation is hard for several reasons:
+1. Datatypes can refer to other datatypes. E.g. `type Bad = B(x: Empty)` is
+uninhabited
+2. These dependencies need not be linear. For example,
+the following datatypes are uninhabited:
+```
+type Bad1 := B1(x: Bad2)
+type Bad2 := B2(x: Bad1)
+```
+3. Instantiated type parameters affect things as well. `List Empty` is
+inhabited, but `Either Empty Empty` is not.
+
+We determine if all types in a TypeFactory are inhabited simulataneously,
+memoizing the results. Proving the termination of this function is very
+tricky (though possible), so we leave it `partial` for now.
+
+-/
+
+def typeSet : Type := List String --Temp
+
+def typeInSet (l: String) (s: typeSet) : Bool :=
+  s.elem l
+
+def addTypeToSet (l: String) (s: typeSet) : typeSet :=
+  l :: s
+
+-- TODO: is this anywhere?
+def List.subset {α} (s1 s2: List α) := ∀ x, x ∈ s1 → x ∈ s2
+
+theorem List.subset_nodup_length {α} {s1 s2: List α} (hn: s1.Nodup) (hsub: List.subset s1 s2) : s1.length ≤ s2.length := by
+  induction s1 generalizing s2 with
+  | nil => simp
+  | cons x t IH =>
+    simp only[List.length]
+    -- Idea: x is in s2, so we can remove it
+    have xin: x ∈ s2 := by apply hsub; grind
+    rw[List.mem_iff_append] at xin
+    rcases xin with ⟨l1, ⟨l2, hs2⟩⟩; subst_vars
+    have hsub1: subset t (l1 ++ l2) := by unfold subset at *; grind
+    grind
+
+def List.subset_cons_iff {α} {x: α} {s1 s2: List α}:
+  List.subset (x :: s1) s2 ↔ x ∈ s2 ∧ List.subset s1 s2 := by
+    unfold subset; grind
+
+mutual
+
+/--
+Prove that type symbol `ts` is inhabited, assuming
+that types `seen` are unknown. All other types are assumed inhabited.
+This check is currently conservative: it requires that all type arguments
+are inhabited which rules out the following (valid) type:
+```
+type A := A1(x: Option B)
+type B := B1(y: A)
+```
+-/
+def typesym_inhab (adts: @TypeFactory IDMeta) (seen: typeSet)
+  (hnodup: List.Nodup seen) (hsub: List.subset seen (List.map (fun x => x.name) adts.toList))
+  (ts: String)
+   : StateM typeSet Bool := do
+  let knowType : StateM typeSet Bool := do
+    let s ← get
+    set (addTypeToSet ts s)
+    pure true
+  -- Check if type is already known to be inhabited
+  let s ← get
+  if typeInSet ts s then pure true
+  -- If type in `seen`, it is unknown, so we return false
+  else if hin: typeInSet ts seen then pure false
+  else
+    match ha: adts.getType ts with
+    | none => pure true -- Assume all non-datatypes are inhabited, TODO should we add?
+    | some l =>
+      -- A datatype is inhabited if it has an inhabited constructor
+      let res ← (l.constrs.attach.foldrM (fun c (accC : Bool) => do
+        -- A constructor is inhabited if all of its arguments are inhabited
+        let constrInhab ← (c.1.args.attach.foldrM
+          (fun ty1 (accA: Bool) =>
+              do
+                have hn: List.Nodup (addTypeToSet l.name seen) := by
+                  unfold addTypeToSet; rw[List.nodup_cons]; constructor
+                  . have := TypeFactory.getType_name ha; subst_vars
+                    rw[←List.elem_iff]; apply hin
+                  . assumption
+                have hsub' : List.subset (addTypeToSet l.name seen) (List.map (fun x => x.name) adts.toList) := by
+                  unfold addTypeToSet; rw[List.subset_cons_iff]
+                  constructor <;> try assumption
+                  rw[List.mem_map]; exists l; constructor <;> try grind
+                  have := TypeFactory.getType_mem ha; grind
+                let b1 ← ty_inhab adts (addTypeToSet l.name seen) hn hsub' ty1.1.2
+                pure (b1 && accA)
+            ) true)
+        pure (constrInhab || accC)
+        ) false)
+      if res then knowType else pure false
+  termination_by (adts.size - seen.length, 0)
+  decreasing_by
+    apply Prod.Lex.left; simp only[addTypeToSet, List.length]
+    apply Nat.sub_succ_lt_self
+    have hlen := List.subset_nodup_length hn hsub'; simp_all[addTypeToSet]; omega
+
+def ty_inhab (adts: @TypeFactory IDMeta) (seen: typeSet)
+  (hnodup: List.Nodup seen) (hsub: List.subset seen (List.map (fun x => x.name) adts.toList))
+  (t: LMonoTy) : StateM typeSet Bool :=
+  match t with
+    | .tcons name args => do
+        -- name(args) is inhabited if name is inhabited as a typesym
+        -- and all args are inhabited as types (note this is conservative)
+        let checkTy ← typesym_inhab adts seen hnodup hsub name
+        if checkTy then
+          args.foldrM (fun ty acc => do
+            let x ← ty_inhab adts seen hnodup hsub ty
+            pure (x && acc)
+          ) true
+        else pure false
+    | _ => pure true -- Type variables and bitvectors are inhabited
+termination_by (adts.size - seen.length, t.size)
+decreasing_by
+  . apply Prod.Lex.right; simp only[LMonoTy.size]; omega
+  . rename_i h; have := LMonoTy.size_lt_of_mem h;
+    apply Prod.Lex.right; simp only[LMonoTy.size]; omega
+end
+
+/--
+Prove that ADT with name `a` is inhabited. All other types are assumed inhabited.
+This check is currently conservative: it requires that all type arguments
+are inhabited which rules out the following (valid) type:
+```
+type A := A1(x: Option B)
+type B := B1(y: A)
+```
+-/
+def adt_inhab  (adts: @TypeFactory IDMeta) (a: String) : StateM typeSet Bool :=
+  typesym_inhab adts [] (by grind) (by unfold List.subset; grind) a
+
+/--
+Check that all ADTs in TypeFactory `adts` are inhabited. This uses memoization
+to avoid computing the intermediate results more than once.
+-/
+def TypeFactory.all_inhab (adts: @TypeFactory IDMeta) : Bool :=
+  let x := (Array.foldlM (fun (b: Bool) (l: LDatatype IDMeta) =>
+    do
+      if not b then pure false
+      else
+      adt_inhab adts l.name) true adts)
+  (StateT.run x []).1
+
+
+
+
+-- TODO: change to map
+
 
 ---------------------------------------------------------------------
 

From 76640d3d1e4efefb416be585c4a5ebcecf98aae5 Mon Sep 17 00:00:00 2001
From: Josh Cohen <cohenjo@amazon.com>
Date: Mon, 12 Jan 2026 13:00:59 -0500
Subject: [PATCH 2/5] Change to map, add error messages, use built-in subset
 function

---
 Strata/DL/Lambda/Lambda.lean      |   1 +
 Strata/DL/Lambda/TypeFactory.lean | 133 ++++++++++++++----------------
 2 files changed, 65 insertions(+), 69 deletions(-)

diff --git a/Strata/DL/Lambda/Lambda.lean b/Strata/DL/Lambda/Lambda.lean
index 6485f39bd..abea509e0 100644
--- a/Strata/DL/Lambda/Lambda.lean
+++ b/Strata/DL/Lambda/Lambda.lean
@@ -44,6 +44,7 @@ def typeCheckAndPartialEval
   Except Std.Format (LExpr T.mono) := do
   let E := TEnv.default
   let C := LContext.default.addFactoryFunctions f
+  let _ ← TypeFactory.checkInhab t
   let C ← C.addTypeFactory t
   let (et, _T) ← LExpr.annotate C E e
   dbg_trace f!"Annotated expression:{Format.line}{et}{Format.line}"
diff --git a/Strata/DL/Lambda/TypeFactory.lean b/Strata/DL/Lambda/TypeFactory.lean
index 38a54735a..f9a331dd2 100644
--- a/Strata/DL/Lambda/TypeFactory.lean
+++ b/Strata/DL/Lambda/TypeFactory.lean
@@ -472,33 +472,25 @@ tricky (though possible), so we leave it `partial` for now.
 
 -/
 
-def typeSet : Type := List String --Temp
+def typeMap : Type := Map String Bool
 
-def typeInSet (l: String) (s: typeSet) : Bool :=
-  s.elem l
+def getTypeInMap (l: String) (m: typeMap) : Option Bool :=
+  Map.find? m l
 
-def addTypeToSet (l: String) (s: typeSet) : typeSet :=
-  l :: s
+def addTypeToMap (l: String) (b: Bool) (m: typeMap) : typeMap :=
+  Map.insert m l b
 
--- TODO: is this anywhere?
-def List.subset {α} (s1 s2: List α) := ∀ x, x ∈ s1 → x ∈ s2
-
-theorem List.subset_nodup_length {α} {s1 s2: List α} (hn: s1.Nodup) (hsub: List.subset s1 s2) : s1.length ≤ s2.length := by
+theorem List.subset_nodup_length {α} {s1 s2: List α} (hn: s1.Nodup) (hsub: s1 ⊆ s2) : s1.length ≤ s2.length := by
   induction s1 generalizing s2 with
   | nil => simp
   | cons x t IH =>
     simp only[List.length]
-    -- Idea: x is in s2, so we can remove it
     have xin: x ∈ s2 := by apply hsub; grind
     rw[List.mem_iff_append] at xin
     rcases xin with ⟨l1, ⟨l2, hs2⟩⟩; subst_vars
-    have hsub1: subset t (l1 ++ l2) := by unfold subset at *; grind
+    have hsub1: t ⊆ (l1 ++ l2) := by grind
     grind
 
-def List.subset_cons_iff {α} {x: α} {s1 s2: List α}:
-  List.subset (x :: s1) s2 ↔ x ∈ s2 ∧ List.subset s1 s2 := by
-    unfold subset; grind
-
 mutual
 
 /--
@@ -511,60 +503,63 @@ type A := A1(x: Option B)
 type B := B1(y: A)
 ```
 -/
-def typesym_inhab (adts: @TypeFactory IDMeta) (seen: typeSet)
-  (hnodup: List.Nodup seen) (hsub: List.subset seen (List.map (fun x => x.name) adts.toList))
+def typesym_inhab (adts: @TypeFactory IDMeta) (seen: List String)
+  (hnodup: List.Nodup seen) (hsub: seen ⊆ (List.map (fun x => x.name) adts.toList))
   (ts: String)
-   : StateM typeSet Bool := do
-  let knowType : StateM typeSet Bool := do
+   : StateM typeMap (Option String) := do
+  let knowType (b: Bool) : StateM typeMap (Option String) := do
     let s ← get
-    set (addTypeToSet ts s)
-    pure true
+    set (addTypeToMap ts b s)
+    if b then pure none else pure (some ts)
   -- Check if type is already known to be inhabited
   let s ← get
-  if typeInSet ts s then pure true
-  -- If type in `seen`, it is unknown, so we return false
-  else if hin: typeInSet ts seen then pure false
-  else
-    match ha: adts.getType ts with
-    | none => pure true -- Assume all non-datatypes are inhabited, TODO should we add?
-    | some l =>
-      -- A datatype is inhabited if it has an inhabited constructor
-      let res ← (l.constrs.attach.foldrM (fun c (accC : Bool) => do
-        -- A constructor is inhabited if all of its arguments are inhabited
-        let constrInhab ← (c.1.args.attach.foldrM
-          (fun ty1 (accA: Bool) =>
-              do
-                have hn: List.Nodup (addTypeToSet l.name seen) := by
-                  unfold addTypeToSet; rw[List.nodup_cons]; constructor
-                  . have := TypeFactory.getType_name ha; subst_vars
-                    rw[←List.elem_iff]; apply hin
-                  . assumption
-                have hsub' : List.subset (addTypeToSet l.name seen) (List.map (fun x => x.name) adts.toList) := by
-                  unfold addTypeToSet; rw[List.subset_cons_iff]
-                  constructor <;> try assumption
-                  rw[List.mem_map]; exists l; constructor <;> try grind
-                  have := TypeFactory.getType_mem ha; grind
-                let b1 ← ty_inhab adts (addTypeToSet l.name seen) hn hsub' ty1.1.2
-                pure (b1 && accA)
-            ) true)
-        pure (constrInhab || accC)
-        ) false)
-      if res then knowType else pure false
+  match getTypeInMap ts s with
+  | some true => pure none
+  | some false => pure (some ts)
+  | none =>
+    -- If type in `seen`, it is unknown, so we return false
+    if hin: List.elem ts seen then pure (some ts)
+    else
+      match ha: adts.getType ts with
+      | none => pure none -- Assume all non-datatypes are inhabited
+      | some l =>
+        -- A datatype is inhabited if it has an inhabited constructor
+        let res ← (l.constrs.attach.foldrM (fun c (accC : Bool) => do
+          -- A constructor is inhabited if all of its arguments are inhabited
+          let constrInhab ← (c.1.args.attach.foldrM
+            (fun ty1 (accA: Bool) =>
+                do
+                  have hn: List.Nodup (l.name :: seen) := by
+                    rw[List.nodup_cons]; constructor
+                    . have := TypeFactory.getType_name ha; subst_vars
+                      rw[←List.elem_iff]; apply hin
+                    . assumption
+                  have hsub' : (l.name :: seen) ⊆ (List.map (fun x => x.name) adts.toList) := by
+                    apply List.cons_subset.mpr
+                    constructor <;> try assumption
+                    rw[List.mem_map]; exists l; constructor <;> try grind
+                    have := TypeFactory.getType_mem ha; grind
+                  let b1 ← ty_inhab adts (l.name :: seen) hn hsub' ty1.1.2
+                  pure (b1 && accA)
+              ) true)
+          pure (constrInhab || accC)
+          ) false)
+        knowType res
   termination_by (adts.size - seen.length, 0)
   decreasing_by
-    apply Prod.Lex.left; simp only[addTypeToSet, List.length]
+    apply Prod.Lex.left; simp only[List.length]
     apply Nat.sub_succ_lt_self
-    have hlen := List.subset_nodup_length hn hsub'; simp_all[addTypeToSet]; omega
+    have hlen := List.subset_nodup_length hn hsub'; simp_all; omega
 
-def ty_inhab (adts: @TypeFactory IDMeta) (seen: typeSet)
-  (hnodup: List.Nodup seen) (hsub: List.subset seen (List.map (fun x => x.name) adts.toList))
-  (t: LMonoTy) : StateM typeSet Bool :=
+def ty_inhab (adts: @TypeFactory IDMeta) (seen: List String)
+  (hnodup: List.Nodup seen) (hsub: seen ⊆  (List.map (fun x => x.name) adts.toList))
+  (t: LMonoTy) : StateM typeMap Bool :=
   match t with
     | .tcons name args => do
         -- name(args) is inhabited if name is inhabited as a typesym
         -- and all args are inhabited as types (note this is conservative)
         let checkTy ← typesym_inhab adts seen hnodup hsub name
-        if checkTy then
+        if checkTy.isNone then
           args.foldrM (fun ty acc => do
             let x ← ty_inhab adts seen hnodup hsub ty
             pure (x && acc)
@@ -587,26 +582,26 @@ type A := A1(x: Option B)
 type B := B1(y: A)
 ```
 -/
-def adt_inhab  (adts: @TypeFactory IDMeta) (a: String) : StateM typeSet Bool :=
-  typesym_inhab adts [] (by grind) (by unfold List.subset; grind) a
+def adt_inhab  (adts: @TypeFactory IDMeta) (a: String) : StateM typeMap (Option String) :=
+  typesym_inhab adts [] (by grind) (by grind) a
 
 /--
 Check that all ADTs in TypeFactory `adts` are inhabited. This uses memoization
-to avoid computing the intermediate results more than once.
+to avoid computing the intermediate results more than once. Returns `none` if
+all datatypes are inhabited, `some a` for some uninhabited type `a`
 -/
-def TypeFactory.all_inhab (adts: @TypeFactory IDMeta) : Bool :=
-  let x := (Array.foldlM (fun (b: Bool) (l: LDatatype IDMeta) =>
+def TypeFactory.all_inhab (adts: @TypeFactory IDMeta) : Option String :=
+  let x := (Array.foldlM (fun (x: Option String) (l: LDatatype IDMeta) =>
     do
-      if not b then pure false
-      else
-      adt_inhab adts l.name) true adts)
+      match x with
+      | some a => pure (some a)
+      | none => adt_inhab adts l.name) none adts)
   (StateT.run x []).1
 
-
-
-
--- TODO: change to map
-
+def TypeFactory.checkInhab (adts: @TypeFactory IDMeta) : Except Format Unit :=
+  match adts.all_inhab with
+  | none => .ok ()
+  | some a => .error f!"Error: datatype {a} not inhabited"
 
 ---------------------------------------------------------------------
 

From 2e97aa83507b0669f7bdc3f50bc4a27042014307 Mon Sep 17 00:00:00 2001
From: Josh Cohen <cohenjo@amazon.com>
Date: Mon, 12 Jan 2026 13:42:23 -0500
Subject: [PATCH 3/5] Add tests, fix cyclic bug, clean up code and comments

---
 Strata/DL/Lambda/TypeFactory.lean          |  56 ++----
 Strata/DL/Util/List.lean                   |  11 ++
 StrataTest/DL/Lambda/TypeFactoryTests.lean | 200 +++++++++++++++++++--
 3 files changed, 209 insertions(+), 58 deletions(-)

diff --git a/Strata/DL/Lambda/TypeFactory.lean b/Strata/DL/Lambda/TypeFactory.lean
index f9a331dd2..31a149bd1 100644
--- a/Strata/DL/Lambda/TypeFactory.lean
+++ b/Strata/DL/Lambda/TypeFactory.lean
@@ -7,6 +7,7 @@
 import Strata.DL.Lambda.LExprWF
 import Strata.DL.Lambda.LTy
 import Strata.DL.Lambda.Factory
+import Strata.DL.Util.List
 
 /-!
 ## Lambda's Type Factory
@@ -454,7 +455,7 @@ The only element of `List` is `Nil`, but we also create the destructor
 `hd : List → Empty`, which means `hd Nil` has type `Empty`, contradicting the
 fact that `Empty` is uninhabited.
 
-However, checking type inhabitation is hard for several reasons:
+However, checking type inhabitation is complicated for several reasons:
 1. Datatypes can refer to other datatypes. E.g. `type Bad = B(x: Empty)` is
 uninhabited
 2. These dependencies need not be linear. For example,
@@ -463,57 +464,35 @@ the following datatypes are uninhabited:
 type Bad1 := B1(x: Bad2)
 type Bad2 := B2(x: Bad1)
 ```
-3. Instantiated type parameters affect things as well. `List Empty` is
-inhabited, but `Either Empty Empty` is not.
+3. Instantiated type parameters matter: `List Empty` is
+inhabited, but `Either Empty Empty` is not. Our check is conservative and will
+not allow either of these types.
 
 We determine if all types in a TypeFactory are inhabited simulataneously,
-memoizing the results. Proving the termination of this function is very
-tricky (though possible), so we leave it `partial` for now.
-
+memoizing the results.
 -/
 
-def typeMap : Type := Map String Bool
-
-def getTypeInMap (l: String) (m: typeMap) : Option Bool :=
-  Map.find? m l
-
-def addTypeToMap (l: String) (b: Bool) (m: typeMap) : typeMap :=
-  Map.insert m l b
-
-theorem List.subset_nodup_length {α} {s1 s2: List α} (hn: s1.Nodup) (hsub: s1 ⊆ s2) : s1.length ≤ s2.length := by
-  induction s1 generalizing s2 with
-  | nil => simp
-  | cons x t IH =>
-    simp only[List.length]
-    have xin: x ∈ s2 := by apply hsub; grind
-    rw[List.mem_iff_append] at xin
-    rcases xin with ⟨l1, ⟨l2, hs2⟩⟩; subst_vars
-    have hsub1: t ⊆ (l1 ++ l2) := by grind
-    grind
+abbrev typeMap : Type := Map String Bool
 
 mutual
 
 /--
 Prove that type symbol `ts` is inhabited, assuming
 that types `seen` are unknown. All other types are assumed inhabited.
-This check is currently conservative: it requires that all type arguments
-are inhabited which rules out the following (valid) type:
-```
-type A := A1(x: Option B)
-type B := B1(y: A)
-```
 -/
 def typesym_inhab (adts: @TypeFactory IDMeta) (seen: List String)
   (hnodup: List.Nodup seen) (hsub: seen ⊆ (List.map (fun x => x.name) adts.toList))
   (ts: String)
    : StateM typeMap (Option String) := do
   let knowType (b: Bool) : StateM typeMap (Option String) := do
-    let s ← get
-    set (addTypeToMap ts b s)
+    -- Only add false if not in a cycle, it may resolve later
+    if b || seen.isEmpty then
+      let m ← get
+      set (m.insert ts b)
     if b then pure none else pure (some ts)
   -- Check if type is already known to be inhabited
-  let s ← get
-  match getTypeInMap ts s with
+  let m ← get
+  match m.find? ts with
   | some true => pure none
   | some false => pure (some ts)
   | none =>
@@ -575,12 +554,6 @@ end
 
 /--
 Prove that ADT with name `a` is inhabited. All other types are assumed inhabited.
-This check is currently conservative: it requires that all type arguments
-are inhabited which rules out the following (valid) type:
-```
-type A := A1(x: Option B)
-type B := B1(y: A)
-```
 -/
 def adt_inhab  (adts: @TypeFactory IDMeta) (a: String) : StateM typeMap (Option String) :=
   typesym_inhab adts [] (by grind) (by grind) a
@@ -598,6 +571,9 @@ def TypeFactory.all_inhab (adts: @TypeFactory IDMeta) : Option String :=
       | none => adt_inhab adts l.name) none adts)
   (StateT.run x []).1
 
+/--
+Check that all ADTs in TypeFactory `adts` are inhabited.
+-/
 def TypeFactory.checkInhab (adts: @TypeFactory IDMeta) : Except Format Unit :=
   match adts.all_inhab with
   | none => .ok ()
diff --git a/Strata/DL/Util/List.lean b/Strata/DL/Util/List.lean
index c9fdffe45..38097bcd4 100644
--- a/Strata/DL/Util/List.lean
+++ b/Strata/DL/Util/List.lean
@@ -411,4 +411,15 @@ theorem length_dedup_of_subset_le {α : Type} [DecidableEq α] (l₁ l₂ : List
       simp_all [dedup]
       omega
 
+theorem subset_nodup_length {α} {s1 s2: List α} (hn: s1.Nodup) (hsub: s1 ⊆ s2) : s1.length ≤ s2.length := by
+  induction s1 generalizing s2 with
+  | nil => simp
+  | cons x t IH =>
+    simp only[List.length]
+    have xin: x ∈ s2 := by apply hsub; grind
+    rw[List.mem_iff_append] at xin
+    rcases xin with ⟨l1, ⟨l2, hs2⟩⟩; subst_vars
+    have hsub1: t ⊆ (l1 ++ l2) := by grind
+    grind
+
 end List
diff --git a/StrataTest/DL/Lambda/TypeFactoryTests.lean b/StrataTest/DL/Lambda/TypeFactoryTests.lean
index 0a4eba152..69a8e1ca0 100644
--- a/StrataTest/DL/Lambda/TypeFactoryTests.lean
+++ b/StrataTest/DL/Lambda/TypeFactoryTests.lean
@@ -480,12 +480,13 @@ end Tree
 -- Typechecking tests
 
 /-
-1. Non-positive type
-type Bad := | C (Bad -> Bad)
+1. Non-positive type (with trivial base case for inhabitation)
+type Bad := | Base | C (Bad -> Bad)
 -/
 
 def badConstr1: LConstr Unit := {name := "C", args := [⟨"x", .arrow (.tcons "Bad" []) (.tcons "Bad" [])⟩], testerName := "isC"}
-def badTy1 : LDatatype Unit := {name := "Bad", typeArgs := [], constrs := [badConstr1], constrs_ne := rfl}
+def badConstr1Base: LConstr Unit := {name := "Base", args := [], testerName := "isBase"}
+def badTy1 : LDatatype Unit := {name := "Bad", typeArgs := [], constrs := [badConstr1Base, badConstr1], constrs_ne := rfl}
 
 /-- info: Error in constructor C: Non-strictly positive occurrence of Bad in type (arrow Bad Bad)
 -/
@@ -493,36 +494,39 @@ def badTy1 : LDatatype Unit := {name := "Bad", typeArgs := [], constrs := [badCo
 #eval format $ typeCheckAndPartialEval #[badTy1] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-2.Non-strictly positive type
-type Bad a := | C ((Bad a -> int) -> int)
+2. Non-strictly positive type (with trivial base case for inhabitation)
+type Bad a := | Base | C ((Bad a -> int) -> int)
 -/
 
 def badConstr2: LConstr Unit := {name := "C", args := [⟨"x", .arrow (.arrow (.tcons "Bad" [.ftvar "a"]) .int) .int⟩], testerName := "isC"}
-def badTy2 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [badConstr2], constrs_ne := rfl}
+def badConstr2Base: LConstr Unit := {name := "Base", args := [], testerName := "isBase"}
+def badTy2 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [badConstr2Base, badConstr2], constrs_ne := rfl}
 
 /-- info: Error in constructor C: Non-strictly positive occurrence of Bad in type (arrow (arrow (Bad a) int) int)-/
 #guard_msgs in
 #eval format $ typeCheckAndPartialEval #[badTy2] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-3. Non-strictly positive type 2
-type Bad a := | C (int -> (Bad a -> int))
+3. Non-strictly positive type 2 (with trivial base case for inhabitation)
+type Bad a := | Base | C (int -> (Bad a -> int))
 -/
 
 def badConstr3: LConstr Unit := {name := "C", args := [⟨"x", .arrow .int (.arrow (.tcons "Bad" [.ftvar "a"]) .int)⟩], testerName := "isC"}
-def badTy3 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [badConstr3], constrs_ne := rfl}
+def badConstr3Base: LConstr Unit := {name := "Base", args := [], testerName := "isBase"}
+def badTy3 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [badConstr3Base, badConstr3], constrs_ne := rfl}
 
 /--info: Error in constructor C: Non-strictly positive occurrence of Bad in type (arrow (Bad a) int)-/
 #guard_msgs in
 #eval format $ typeCheckAndPartialEval #[badTy3] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-4. Strictly positive type
-type Good := | C (int -> (int -> Good))
+4. Strictly positive type (with trivial base case for inhabitation)
+type Good := | Base | C (int -> (int -> Good))
 -/
 
 def goodConstr1: LConstr Unit := {name := "C", args := [⟨"x", .arrow .int (.arrow .int (.tcons "Good" [.ftvar "a"]))⟩], testerName := "isC"}
-def goodTy1 : LDatatype Unit := {name := "Good", typeArgs := ["a"], constrs := [goodConstr1], constrs_ne := rfl}
+def goodConstr1Base: LConstr Unit := {name := "Base", args := [], testerName := "isBase"}
+def goodTy1 : LDatatype Unit := {name := "Good", typeArgs := ["a"], constrs := [goodConstr1Base, goodConstr1], constrs_ne := rfl}
 
 /-- info: Annotated expression:
 #0
@@ -534,22 +538,24 @@ info: #0
 #eval format $ typeCheckAndPartialEval #[goodTy1] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-5. Non-uniform type
-type Nonunif a := | C (int -> Nonunif (List a))
+5. Non-uniform type (with trivial base case for inhabitation)
+type Nonunif a := | Base | C (int -> Nonunif (List a))
 -/
 def nonUnifConstr1: LConstr Unit := {name := "C", args := [⟨"x", .arrow .int (.arrow .int (.tcons "Nonunif" [.tcons "List" [.ftvar "a"]]))⟩], testerName := "isC"}
-def nonUnifTy1 : LDatatype Unit := {name := "Nonunif", typeArgs := ["a"], constrs := [nonUnifConstr1], constrs_ne := rfl}
+def nonUnifConstr1Base: LConstr Unit := {name := "Base", args := [], testerName := "isBase"}
+def nonUnifTy1 : LDatatype Unit := {name := "Nonunif", typeArgs := ["a"], constrs := [nonUnifConstr1Base, nonUnifConstr1], constrs_ne := rfl}
 
 /-- info: Error in constructor C: Non-uniform occurrence of Nonunif, which is applied to [(List a)] when it should be applied to [a]-/
 #guard_msgs in
 #eval format $ typeCheckAndPartialEval #[listTy, nonUnifTy1] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-6. Nested types are allowed, though they won't produce a useful elimination principle
-type Nest a := | C (List (Nest a))
+6. Nested types are allowed, though they won't produce a useful elimination principle (with trivial base case for inhabitation)
+type Nest a := | Base | C (List (Nest a))
 -/
 def nestConstr1: LConstr Unit := {name := "C", args := [⟨"x", .tcons "List" [.tcons "Nest" [.ftvar "a"]]⟩], testerName := "isC"}
-def nestTy1 : LDatatype Unit := {name := "Nest", typeArgs := ["a"], constrs := [nestConstr1], constrs_ne := rfl}
+def nestConstr1Base: LConstr Unit := {name := "Base", args := [], testerName := "isBase"}
+def nestTy1 : LDatatype Unit := {name := "Nest", typeArgs := ["a"], constrs := [nestConstr1Base, nestConstr1], constrs_ne := rfl}
 
 /-- info: Annotated expression:
 #0
@@ -590,4 +596,162 @@ New Function:func Int.Add :  ((x : int)) → Bad;-/
 #guard_msgs in
 #eval format $ typeCheckAndPartialEval #[badTy5] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
+---------------------------------------------------------------------
+
+-- Inhabited type tests
+
+section InhabitedTests
+
+-- Test 1: Normal inhabited types
+
+-- Option type: Some | None
+def optionTy : LDatatype Unit := {
+  name := "Option", typeArgs := ["a"],
+  constrs := [
+    {name := "None", args := []},
+    {name := "Some", args := [("x", .ftvar "a")]}
+  ], constrs_ne := rfl
+}
+
+/-- info: none -/
+#guard_msgs in #eval TypeFactory.all_inhab #[optionTy]
+
+-- List is already defined above, test it
+/-- info: none -/
+#guard_msgs in #eval TypeFactory.all_inhab #[listTy]
+
+-- Either type: Left a | Right b
+def eitherTy : LDatatype Unit := {
+  name := "Either", typeArgs := ["a", "b"],
+  constrs := [
+    {name := "Left", args := [("l", .ftvar "a")]},
+    {name := "Right", args := [("r", .ftvar "b")]}
+  ], constrs_ne := rfl
+}
+
+/-- info: none -/
+#guard_msgs in #eval TypeFactory.all_inhab #[eitherTy]
+
+-- Nat type: Zero | Succ Nat
+def natTy : LDatatype Unit := {
+  name := "Nat", typeArgs := [],
+  constrs := [
+    {name := "Zero", args := []},
+    {name := "Succ", args := [("n", .tcons "Nat" [])]}
+  ], constrs_ne := rfl
+}
+
+/-- info: none -/
+#guard_msgs in #eval TypeFactory.all_inhab #[natTy]
+
+-- Test 2: Mutually recursive inhabited types
+
+-- Even/Odd mutual recursion (both inhabited via base cases)
+def evenTy : LDatatype Unit := {
+  name := "Even", typeArgs := [],
+  constrs := [
+    {name := "EvenZ", args := []},
+    {name := "EvenS", args := [("o", .tcons "Odd" [])]}
+  ], constrs_ne := rfl
+}
+
+def oddTy : LDatatype Unit := {
+  name := "Odd", typeArgs := [],
+  constrs := [
+    {name := "OddS", args := [("e", .tcons "Even" [])]}
+  ], constrs_ne := rfl
+}
+
+/-- info: none -/
+#guard_msgs in #eval TypeFactory.all_inhab #[evenTy, oddTy]
+
+-- Forest/Tree mutual recursion
+def forestTy : LDatatype Unit := {
+  name := "Forest", typeArgs := ["a"],
+  constrs := [
+    {name := "FNil", args := []},
+    {name := "FCons", args := [("t", .tcons "Tree" [.ftvar "a"]), ("f", .tcons "Forest" [.ftvar "a"])]}
+  ], constrs_ne := rfl
+}
+
+def treeTy2 : LDatatype Unit := {
+  name := "Tree", typeArgs := ["a"],
+  constrs := [
+    {name := "TNode", args := [("x", .ftvar "a"), ("children", .tcons "Forest" [.ftvar "a"])]}
+  ], constrs_ne := rfl
+}
+
+/-- info: none -/
+#guard_msgs in #eval TypeFactory.all_inhab #[forestTy, treeTy2]
+
+-- Test 3: Uninhabited types
+
+-- Empty type (no constructors would be invalid, so single constructor requiring itself)
+def emptyTy : LDatatype Unit := {
+  name := "Empty", typeArgs := [],
+  constrs := [
+    {name := "MkEmpty", args := [("x", .tcons "Empty" [])]}
+  ], constrs_ne := rfl
+}
+
+/-- info: Error: datatype Empty not inhabited -/
+#guard_msgs in
+#eval format $ typeCheckAndPartialEval #[emptyTy] (IntBoolFactory : @Factory TestParams) (intConst () 0)
+
+-- Type requiring uninhabited type
+def needsEmptyTy : LDatatype Unit := {
+  name := "NeedsEmpty", typeArgs := [],
+  constrs := [
+    {name := "MkNeedsEmpty", args := [("x", .tcons "Empty" [])]}
+  ], constrs_ne := rfl
+}
+
+/-- info: Error: datatype Empty not inhabited -/
+#guard_msgs in
+#eval format $ typeCheckAndPartialEval #[emptyTy, needsEmptyTy] (IntBoolFactory : @Factory TestParams) (intConst () 0)
+
+-- Mutually uninhabited types
+def bad1Ty : LDatatype Unit := {
+  name := "Bad1", typeArgs := [],
+  constrs := [
+    {name := "B1", args := [("x", .tcons "Bad2" [])]}
+  ], constrs_ne := rfl
+}
+
+def bad2Ty : LDatatype Unit := {
+  name := "Bad2", typeArgs := [],
+  constrs := [
+    {name := "B2", args := [("x", .tcons "Bad1" [])]}
+  ], constrs_ne := rfl
+}
+
+/-- info: Error: datatype Bad1 not inhabited -/
+#guard_msgs in
+#eval format $ typeCheckAndPartialEval #[bad1Ty, bad2Ty] (IntBoolFactory : @Factory TestParams) (intConst () 0)
+
+-- Three-way mutual uninhabited cycle
+def cycle1Ty : LDatatype Unit := {
+  name := "Cycle1", typeArgs := [],
+  constrs := [{name := "C1", args := [("x", .tcons "Cycle2" [])]}],
+  constrs_ne := rfl
+}
+
+def cycle2Ty : LDatatype Unit := {
+  name := "Cycle2", typeArgs := [],
+  constrs := [{name := "C2", args := [("x", .tcons "Cycle3" [])]}],
+  constrs_ne := rfl
+}
+
+def cycle3Ty : LDatatype Unit := {
+  name := "Cycle3", typeArgs := [],
+  constrs := [{name := "C3", args := [("x", .tcons "Cycle1" [])]}],
+  constrs_ne := rfl
+}
+
+/-- info: Error: datatype Cycle1 not inhabited -/
+#guard_msgs in
+#eval format $ typeCheckAndPartialEval #[cycle1Ty, cycle2Ty, cycle3Ty] (IntBoolFactory : @Factory TestParams) (intConst () 0)
+
+end InhabitedTests
+
 end Lambda

From d6b612620ebfaa5952790e029e92ae5c9389e651 Mon Sep 17 00:00:00 2001
From: Josh Cohen <cohenjo@amazon.com>
Date: Mon, 12 Jan 2026 13:58:41 -0500
Subject: [PATCH 4/5] Remove unneeded lemmas, change to foldl, improve comments

---
 Strata/DL/Lambda/TypeFactory.lean          | 29 +++++++---------------
 StrataTest/DL/Lambda/TypeFactoryTests.lean | 19 +++++++-------
 2 files changed, 18 insertions(+), 30 deletions(-)

diff --git a/Strata/DL/Lambda/TypeFactory.lean b/Strata/DL/Lambda/TypeFactory.lean
index 31a149bd1..a86f866ad 100644
--- a/Strata/DL/Lambda/TypeFactory.lean
+++ b/Strata/DL/Lambda/TypeFactory.lean
@@ -416,17 +416,6 @@ def TypeFactory.genFactory {T: LExprParams} [inst: Inhabited T.Metadata] [Inhabi
 def TypeFactory.getType (F : @TypeFactory IDMeta) (name : String) : Option (LDatatype IDMeta) :=
   F.find? (fun d => d.name == name)
 
-omit [DecidableEq IDMeta] [Inhabited IDMeta] in theorem TypeFactory.getType_name {F : @TypeFactory IDMeta} {name : String}
-  {l: LDatatype IDMeta}:
-  F.getType name = some l → l.name = name := by
-    unfold TypeFactory.getType; grind
-
-omit [DecidableEq IDMeta] [Inhabited IDMeta] in theorem TypeFactory.getType_mem {F : @TypeFactory IDMeta} {name : String}
-  {l: LDatatype IDMeta}:
-  F.getType name = some l → @Membership.mem (LDatatype IDMeta) (Array (LDatatype IDMeta)) _ F l := by apply Array.mem_of_find?_eq_some
-
-
-
 /--
 Add an `LDatatype` to an existing `TypeFactory`, checking that no
 types are duplicated.
@@ -479,6 +468,7 @@ mutual
 /--
 Prove that type symbol `ts` is inhabited, assuming
 that types `seen` are unknown. All other types are assumed inhabited.
+The `List.Nodup` and `⊆` hypotheses are only used to prove termination.
 -/
 def typesym_inhab (adts: @TypeFactory IDMeta) (seen: List String)
   (hnodup: List.Nodup seen) (hsub: seen ⊆ (List.map (fun x => x.name) adts.toList))
@@ -503,25 +493,24 @@ def typesym_inhab (adts: @TypeFactory IDMeta) (seen: List String)
       | none => pure none -- Assume all non-datatypes are inhabited
       | some l =>
         -- A datatype is inhabited if it has an inhabited constructor
-        let res ← (l.constrs.attach.foldrM (fun c (accC : Bool) => do
+        let res ← (l.constrs.foldlM (fun accC c => do
           -- A constructor is inhabited if all of its arguments are inhabited
-          let constrInhab ← (c.1.args.attach.foldrM
-            (fun ty1 (accA: Bool) =>
+          let constrInhab ← (c.args.foldlM
+            (fun accA ty1 =>
                 do
                   have hn: List.Nodup (l.name :: seen) := by
                     rw[List.nodup_cons]; constructor
-                    . have := TypeFactory.getType_name ha; subst_vars
-                      rw[←List.elem_iff]; apply hin
+                    . have := Array.find?_some ha; grind
                     . assumption
                   have hsub' : (l.name :: seen) ⊆ (List.map (fun x => x.name) adts.toList) := by
                     apply List.cons_subset.mpr
                     constructor <;> try assumption
                     rw[List.mem_map]; exists l; constructor <;> try grind
-                    have := TypeFactory.getType_mem ha; grind
-                  let b1 ← ty_inhab adts (l.name :: seen) hn hsub' ty1.1.2
-                  pure (b1 && accA)
+                    have := Array.mem_of_find?_eq_some ha; grind
+                  let b1 ← ty_inhab adts (l.name :: seen) hn hsub' ty1.2
+                  pure (accA && b1)
               ) true)
-          pure (constrInhab || accC)
+          pure (accC || constrInhab)
           ) false)
         knowType res
   termination_by (adts.size - seen.length, 0)
diff --git a/StrataTest/DL/Lambda/TypeFactoryTests.lean b/StrataTest/DL/Lambda/TypeFactoryTests.lean
index 69a8e1ca0..028b0ee49 100644
--- a/StrataTest/DL/Lambda/TypeFactoryTests.lean
+++ b/StrataTest/DL/Lambda/TypeFactoryTests.lean
@@ -480,7 +480,7 @@ end Tree
 -- Typechecking tests
 
 /-
-1. Non-positive type (with trivial base case for inhabitation)
+1. Non-positive type
 type Bad := | Base | C (Bad -> Bad)
 -/
 
@@ -494,7 +494,7 @@ def badTy1 : LDatatype Unit := {name := "Bad", typeArgs := [], constrs := [badCo
 #eval format $ typeCheckAndPartialEval #[badTy1] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-2. Non-strictly positive type (with trivial base case for inhabitation)
+2. Non-strictly positive type
 type Bad a := | Base | C ((Bad a -> int) -> int)
 -/
 
@@ -507,7 +507,7 @@ def badTy2 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [ba
 #eval format $ typeCheckAndPartialEval #[badTy2] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-3. Non-strictly positive type 2 (with trivial base case for inhabitation)
+3. Non-strictly positive type 2
 type Bad a := | Base | C (int -> (Bad a -> int))
 -/
 
@@ -520,7 +520,7 @@ def badTy3 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [ba
 #eval format $ typeCheckAndPartialEval #[badTy3] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 /-
-4. Strictly positive type (with trivial base case for inhabitation)
+4. Strictly positive type
 type Good := | Base | C (int -> (int -> Good))
 -/
 
@@ -602,7 +602,7 @@ New Function:func Int.Add :  ((x : int)) → Bad;-/
 
 section InhabitedTests
 
--- Test 1: Normal inhabited types
+-- Test 1: Standard inhabited types
 
 -- Option type: Some | None
 def optionTy : LDatatype Unit := {
@@ -616,7 +616,6 @@ def optionTy : LDatatype Unit := {
 /-- info: none -/
 #guard_msgs in #eval TypeFactory.all_inhab #[optionTy]
 
--- List is already defined above, test it
 /-- info: none -/
 #guard_msgs in #eval TypeFactory.all_inhab #[listTy]
 
@@ -646,7 +645,7 @@ def natTy : LDatatype Unit := {
 
 -- Test 2: Mutually recursive inhabited types
 
--- Even/Odd mutual recursion (both inhabited via base cases)
+-- Even/Odd mutual recursion (note Odd does not have an explicit base case)
 def evenTy : LDatatype Unit := {
   name := "Even", typeArgs := [],
   constrs := [
@@ -686,7 +685,7 @@ def treeTy2 : LDatatype Unit := {
 
 -- Test 3: Uninhabited types
 
--- Empty type (no constructors would be invalid, so single constructor requiring itself)
+-- Empty type
 def emptyTy : LDatatype Unit := {
   name := "Empty", typeArgs := [],
   constrs := [
@@ -706,9 +705,9 @@ def needsEmptyTy : LDatatype Unit := {
   ], constrs_ne := rfl
 }
 
-/-- info: Error: datatype Empty not inhabited -/
+/-- info: Error: datatype NeedsEmpty not inhabited -/
 #guard_msgs in
-#eval format $ typeCheckAndPartialEval #[emptyTy, needsEmptyTy] (IntBoolFactory : @Factory TestParams) (intConst () 0)
+#eval format $ typeCheckAndPartialEval #[needsEmptyTy, emptyTy] (IntBoolFactory : @Factory TestParams) (intConst () 0)
 
 -- Mutually uninhabited types
 def bad1Ty : LDatatype Unit := {

From 2430142295012de13249c9e2d9393e43455947aa Mon Sep 17 00:00:00 2001
From: Josh Cohen <cohenjo@amazon.com>
Date: Mon, 12 Jan 2026 14:00:04 -0500
Subject: [PATCH 5/5] Minor formatting fixes

---
 Strata/DL/Lambda/TypeFactory.lean | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/Strata/DL/Lambda/TypeFactory.lean b/Strata/DL/Lambda/TypeFactory.lean
index a86f866ad..135f2547c 100644
--- a/Strata/DL/Lambda/TypeFactory.lean
+++ b/Strata/DL/Lambda/TypeFactory.lean
@@ -471,9 +471,9 @@ that types `seen` are unknown. All other types are assumed inhabited.
 The `List.Nodup` and `⊆` hypotheses are only used to prove termination.
 -/
 def typesym_inhab (adts: @TypeFactory IDMeta) (seen: List String)
-  (hnodup: List.Nodup seen) (hsub: seen ⊆ (List.map (fun x => x.name) adts.toList))
-  (ts: String)
-   : StateM typeMap (Option String) := do
+  (hnodup: List.Nodup seen)
+  (hsub: seen ⊆ (List.map (fun x => x.name) adts.toList))
+  (ts: String) : StateM typeMap (Option String) := do
   let knowType (b: Bool) : StateM typeMap (Option String) := do
     -- Only add false if not in a cycle, it may resolve later
     if b || seen.isEmpty then
@@ -523,17 +523,17 @@ def ty_inhab (adts: @TypeFactory IDMeta) (seen: List String)
   (hnodup: List.Nodup seen) (hsub: seen ⊆  (List.map (fun x => x.name) adts.toList))
   (t: LMonoTy) : StateM typeMap Bool :=
   match t with
-    | .tcons name args => do
-        -- name(args) is inhabited if name is inhabited as a typesym
-        -- and all args are inhabited as types (note this is conservative)
-        let checkTy ← typesym_inhab adts seen hnodup hsub name
-        if checkTy.isNone then
-          args.foldrM (fun ty acc => do
-            let x ← ty_inhab adts seen hnodup hsub ty
-            pure (x && acc)
-          ) true
-        else pure false
-    | _ => pure true -- Type variables and bitvectors are inhabited
+  | .tcons name args => do
+      -- name(args) is inhabited if name is inhabited as a typesym
+      -- and all args are inhabited as types (note this is conservative)
+      let checkTy ← typesym_inhab adts seen hnodup hsub name
+      if checkTy.isNone then
+        args.foldrM (fun ty acc => do
+          let x ← ty_inhab adts seen hnodup hsub ty
+          pure (x && acc)
+        ) true
+      else pure false
+  | _ => pure true -- Type variables and bitvectors are inhabited
 termination_by (adts.size - seen.length, t.size)
 decreasing_by
   . apply Prod.Lex.right; simp only[LMonoTy.size]; omega