diff --git a/rzk/src/Language/Rzk/Free/Syntax.hs b/rzk/src/Language/Rzk/Free/Syntax.hs
index ad716ed38..391adf671 100644
--- a/rzk/src/Language/Rzk/Free/Syntax.hs
+++ b/rzk/src/Language/Rzk/Free/Syntax.hs
@@ -125,8 +125,19 @@ termIsNF (Free (AnnF info f)) = t'
     t' = Free (AnnF info { infoWHNF = Just t', infoNF = Just t' } f)
 
 invalidateWHNF :: TermT var -> TermT var
-invalidateWHNF = transFS $ \(AnnF info f) ->
-  AnnF info { infoWHNF = Nothing, infoNF = Nothing } f
+invalidateWHNF tt = case tt of
+  -- type layer terms that should not be evaluated further
+  LambdaT{} -> tt
+  ReflT{} -> tt
+  TypeFunT{} -> tt
+  TypeSigmaT{} -> tt
+  TypeIdT{} -> tt
+  RecBottomT{} -> tt
+  TypeUnitT{} -> tt
+  UnitT{} -> tt
+
+  _ -> (`transFS` tt) $ \(AnnF info f) ->
+          AnnF info { infoWHNF = Nothing, infoNF = Nothing } f
 
 substituteT :: TermT var -> Scope TermT var -> TermT var
 substituteT x = substitute x . invalidateWHNF
@@ -288,7 +299,7 @@ toTerm bvars = go
       Rzk.TypeSigma _loc pat tA tB ->
         TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB)
 
-      Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) ((Rzk.SigmaParam _ patB tB) : ps) tN -> 
+      Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) ((Rzk.SigmaParam _ patB tB) : ps) tN ->
         go (Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _loc patX tX) ps tN)
         where
           patX = Rzk.PatternPair _loc patA patB
@@ -299,7 +310,7 @@ toTerm bvars = go
       Rzk.Lambda _loc (Rzk.ParamPattern _ pat : params) body ->
         Lambda (patternVar pat) Nothing (toScopePattern pat bvars (Rzk.Lambda _loc params body))
       Rzk.Lambda _loc (Rzk.ParamPatternType _ [] _ty : params) body ->
-        go (Rzk.Lambda _loc params body)                        
+        go (Rzk.Lambda _loc params body)
       Rzk.Lambda _loc (Rzk.ParamPatternType _ (pat:pats) ty : params) body ->
         Lambda (patternVar pat) (Just (go ty, Nothing))
           (toScopePattern pat bvars (Rzk.Lambda _loc (Rzk.ParamPatternType _loc pats ty : params) body))
diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs
index 14d00c5e1..da596d382 100644
--- a/rzk/src/Rzk/TypeCheck.hs
+++ b/rzk/src/Rzk/TypeCheck.hs
@@ -24,6 +24,7 @@ import           Language.Rzk.Free.Syntax
 import qualified Language.Rzk.Syntax      as Rzk
 
 import           Debug.Trace
+import           Text.Read                (readMaybe)
 import           Unsafe.Coerce
 
 -- $setup
@@ -241,6 +242,10 @@ setOption "render" = \case
   "none"  -> localRenderBackend Nothing
   _ -> const $
     issueTypeError $ TypeErrorOther "unknown render backend (use \"svg\", \"latex\", or \"none\")"
+setOption "max-whnf-depth" = \case
+  str | Just n <- readMaybe str, n > 0 -> localMaxWhnfDepth n
+  _ -> const $
+    issueTypeError $ TypeErrorOther "invalid number (use any positive integer)"
 setOption optionName = const $ const $
   issueTypeError $ TypeErrorOther ("unknown option " <> show optionName)
 
@@ -645,6 +650,8 @@ data Context var = Context
   , verbosity              :: Verbosity
   , covariance             :: Covariance
   , renderBackend          :: Maybe RenderBackend
+  , maxWhnfDepth           :: !Int
+  , whnfDepth              :: !Int
   } deriving (Functor, Foldable)
 
 addVarInCurrentScope :: var -> VarInfo var -> Context var -> Context var
@@ -668,6 +675,8 @@ emptyContext = Context
   , verbosity = Normal
   , covariance = Covariant
   , renderBackend = Nothing
+  , maxWhnfDepth = 50
+  , whnfDepth = 0
   }
 
 askCurrentScope :: TypeCheck var (ScopeInfo var)
@@ -1458,12 +1467,22 @@ tryRestriction = \case
     go rs
   _ -> pure Nothing
 
+localMaxWhnfDepth :: Int -> TypeCheck var a -> TypeCheck var a
+localMaxWhnfDepth n = local $ \ctx -> ctx { maxWhnfDepth = n }
+
+incWhnfDepth :: a -> TypeCheck var a -> TypeCheck var a
+incWhnfDepth def tc = do
+  Context{..} <- ask
+  if whnfDepth > maxWhnfDepth
+    then return def
+    else local (\ctx -> ctx { whnfDepth = whnfDepth + 1}) tc
+
 -- | Compute a typed term to its WHNF.
 --
 -- >>> unsafeTypeCheck' $ whnfT "(\\ (x : Unit) -> x) unit"
 -- unit : Unit
 whnfT :: Eq var => TermT var -> TypeCheck var (TermT var)
-whnfT tt = performing (ActionWHNF tt) $ case tt of
+whnfT tt = incWhnfDepth tt $ case tt of
   -- use cached result if it exists
   Free (AnnF info _)
     | Just tt' <- infoWHNF info -> pure tt'