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/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 e20cb53c5..135f2547c 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
@@ -428,6 +429,144 @@ 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 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,
+the following datatypes are uninhabited:
+```
+type Bad1 := B1(x: Bad2)
+type Bad2 := B2(x: Bad1)
+```
+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.
+-/
+
+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.
+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
+  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
+      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 m ← get
+  match m.find? ts 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.foldlM (fun accC c => do
+          -- A constructor is inhabited if all of its arguments are inhabited
+          let constrInhab ← (c.args.foldlM
+            (fun accA ty1 =>
+                do
+                  have hn: List.Nodup (l.name :: seen) := by
+                    rw[List.nodup_cons]; constructor
+                    . 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 := 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 (accC || constrInhab)
+          ) false)
+        knowType res
+  termination_by (adts.size - seen.length, 0)
+  decreasing_by
+    apply Prod.Lex.left; simp only[List.length]
+    apply Nat.sub_succ_lt_self
+    have hlen := List.subset_nodup_length hn hsub'; simp_all; omega
+
+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
+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.
+-/
+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. Returns `none` if
+all datatypes are inhabited, `some a` for some uninhabited type `a`
+-/
+def TypeFactory.all_inhab (adts: @TypeFactory IDMeta) : Option String :=
+  let x := (Array.foldlM (fun (x: Option String) (l: LDatatype IDMeta) =>
+    do
+      match x with
+      | some a => pure (some a)
+      | 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 ()
+  | some a => .error f!"Error: datatype {a} not inhabited"
 
 ---------------------------------------------------------------------
 
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..028b0ee49 100644
--- a/StrataTest/DL/Lambda/TypeFactoryTests.lean
+++ b/StrataTest/DL/Lambda/TypeFactoryTests.lean
@@ -481,11 +481,12 @@ end Tree
 
 /-
 1. Non-positive type
-type Bad := | C (Bad -> Bad)
+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,12 +494,13 @@ 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
+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
@@ -506,11 +508,12 @@ def badTy2 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [ba
 
 /-
 3. Non-strictly positive type 2
-type Bad a := | C (int -> (Bad a -> int))
+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
@@ -518,11 +521,12 @@ def badTy3 : LDatatype Unit := {name := "Bad", typeArgs := ["a"], constrs := [ba
 
 /-
 4. Strictly positive type
-type Good := | C (int -> (int -> Good))
+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,161 @@ 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: Standard 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]
+
+/-- 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 (note Odd does not have an explicit base case)
+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
+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 NeedsEmpty not inhabited -/
+#guard_msgs in
+#eval format $ typeCheckAndPartialEval #[needsEmptyTy, emptyTy] (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