diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean
index fe00c4b..81a65a7 100644
--- a/Qpf/Macro/Data/View.lean
+++ b/Qpf/Macro/Data/View.lean
@@ -232,19 +232,14 @@ instance : ToString (DataView) := ⟨
   specifications
 -/
 def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do
-  if view.liveBinders.isEmpty then
-    if view.deadBinders.isEmpty then
-      if view.command == .Codata then
-        throwError "Due to a bug, codatatype without any parameters don't quite work yet. Please try adding parameters to your type"
-      else
-        throwError "Trying to define a datatype without variables, you probably want an `inductive` type instead"
-    else
-      throwErrorAt view.binders "You should mark some variables as live by removing the type ascription (they will be automatically inferred as `Type _`), or if you don't have variables of type `Type _`, you probably want an `inductive` type"
-
-  -- TODO: remove once dead variables are fully supported
-  if !view.deadBinders.isEmpty then
-    dbg_trace "Dead variables are not fully supported yet"
-
+  -- if view.liveBinders.isEmpty then
+  --   if view.deadBinders.isEmpty then
+  --     if view.command == .Codata then
+  --       throwError "Due to a bug, codatatype without any parameters don't quite work yet. Please try adding parameters to your type"
+  --     else
+  --       throwError "Trying to define a datatype without variables, you probably want an `inductive` type instead"
+  --   else
+  --     throwErrorAt view.binders "You should mark some variables as live by removing the type ascription (they will be automatically inferred as `Type _`), or if you don't have variables of type `Type _`, you probably want an `inductive` type"
 
   -- TODO: make this more intelligent. In particular, allow types like `Type`, `Type 3`, or `Type u`
   --       and only throw an error if the user tries to define a family of types
diff --git a/Test.lean b/Test.lean
index 6003607..b4edc82 100644
--- a/Test.lean
+++ b/Test.lean
@@ -9,3 +9,4 @@ import Test.Tree
 -- import Test.Variable
 import Test.WithBindersInCtor
 import Test.Wrap
+import Test.NoLiveVariables
diff --git a/Test/NoLiveVars.lean b/Test/NoLiveVars.lean
new file mode 100644
index 0000000..5aefc07
--- /dev/null
+++ b/Test/NoLiveVars.lean
@@ -0,0 +1,14 @@
+import Qpf
+
+/-!
+Tests to assert we can have (`co`)`data` types without
+any live variables
+-/
+
+namespace Qpf.Test.NoLiveVars
+
+data Data (α : Type) where
+  | dat : α → Data α
+
+codata Codata (α : Type) where
+  | dat : α → Codata α → Codata α