diff --git a/src/Agda2Lambox/Compile/Type.hs b/src/Agda2Lambox/Compile/Type.hs
index 42d6ff8..b045dfd 100644
--- a/src/Agda2Lambox/Compile/Type.hs
+++ b/src/Agda2Lambox/Compile/Type.hs
@@ -143,6 +143,7 @@ compileTypeTerm = \case
 
     -- if it's an inductive, we only apply the parameters
     else if isDataOrRecDef def then do
+      lift $ requireDef q
       ind <- liftTCM $ toInductive q
       ([],) . foldl' LBox.TApp (LBox.TInd ind)
         <$> compileElims (take (getInductiveParams def) es)