diff --git a/app/App.hs b/app/App.hs
index 3d537c685..aa7c62d7d 100644
--- a/app/App.hs
+++ b/app/App.hs
@@ -4,6 +4,7 @@ import CommonOptions
 import Data.ByteString qualified as ByteString
 import GlobalOptions
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Pipeline
 import Juvix.Data.Error qualified as Error
 import Juvix.Extra.Paths.Base
@@ -146,6 +147,13 @@ getEntryPoint inputFile = do
   _runAppIOArgsRoots <- askRoots
   embed (getEntryPoint' (RunAppIOArgs {..}) inputFile)
 
+runPipelineTermination :: (Member App r) => AppPath File -> Sem (Termination ': PipelineEff) a -> Sem r a
+runPipelineTermination input p = do
+  r <- runPipelineEither input (evalTermination iniTerminationState p)
+  case r of
+    Left err -> exitJuvixError err
+    Right res -> return (snd res)
+
 runPipeline :: (Member App r) => AppPath File -> Sem PipelineEff a -> Sem r a
 runPipeline input p = do
   r <- runPipelineEither input p
diff --git a/app/Commands/Dev/Internal/Arity.hs b/app/Commands/Dev/Internal/Arity.hs
index 85386cde5..02568930d 100644
--- a/app/Commands/Dev/Internal/Arity.hs
+++ b/app/Commands/Dev/Internal/Arity.hs
@@ -8,5 +8,5 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.D
 runCommand :: (Members '[Embed IO, App] r) => InternalArityOptions -> Sem r ()
 runCommand opts = do
   globalOpts <- askGlobalOptions
-  micro <- head . (^. InternalArity.resultModules) <$> runPipeline (opts ^. internalArityInputFile) upToInternalArity
+  micro <- head . (^. InternalArity.resultModules) <$> runPipelineTermination (opts ^. internalArityInputFile) upToInternalArity
   renderStdOut (Internal.ppOut globalOpts micro)
diff --git a/app/Commands/Dev/Internal/Pretty.hs b/app/Commands/Dev/Internal/Pretty.hs
index 8e4b6568a..71999cc8c 100644
--- a/app/Commands/Dev/Internal/Pretty.hs
+++ b/app/Commands/Dev/Internal/Pretty.hs
@@ -8,5 +8,5 @@ import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
 runCommand :: (Members '[Embed IO, App] r) => InternalPrettyOptions -> Sem r ()
 runCommand opts = do
   globalOpts <- askGlobalOptions
-  intern <- head . (^. Internal.resultModules) <$> runPipeline (opts ^. internalPrettyInputFile) upToInternal
+  intern <- head . (^. Internal.resultModules) <$> runPipelineTermination (opts ^. internalPrettyInputFile) upToInternal
   renderStdOut (Internal.ppOut globalOpts intern)
diff --git a/app/Commands/Dev/Internal/Reachability.hs b/app/Commands/Dev/Internal/Reachability.hs
index 3d8a4e0c3..b4dca8036 100644
--- a/app/Commands/Dev/Internal/Reachability.hs
+++ b/app/Commands/Dev/Internal/Reachability.hs
@@ -8,5 +8,5 @@ import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
 runCommand :: (Members '[Embed IO, App] r) => InternalReachabilityOptions -> Sem r ()
 runCommand opts = do
   globalOpts <- askGlobalOptions
-  depInfo <- (^. Internal.resultDepInfo) <$> runPipeline (opts ^. internalReachabilityInputFile) upToInternal
+  depInfo <- (^. Internal.resultDepInfo) <$> runPipelineTermination (opts ^. internalReachabilityInputFile) upToInternal
   renderStdOut (Internal.ppOut globalOpts depInfo)
diff --git a/app/Commands/Dev/Termination/CallGraph.hs b/app/Commands/Dev/Termination/CallGraph.hs
index 435387f90..5a05cb0ae 100644
--- a/app/Commands/Dev/Termination/CallGraph.hs
+++ b/app/Commands/Dev/Termination/CallGraph.hs
@@ -12,13 +12,13 @@ import Juvix.Prelude.Pretty
 runCommand :: (Members '[Embed IO, App] r) => CallGraphOptions -> Sem r ()
 runCommand CallGraphOptions {..} = do
   globalOpts <- askGlobalOptions
-  results <- runPipeline _graphInputFile upToInternal
+  results <- runPipelineTermination _graphInputFile upToInternal
   let topModules = results ^. Internal.resultModules
       mainModule = head topModules
       toAnsiText' :: forall a. (HasAnsiBackend a, HasTextBackend a) => a -> Text
       toAnsiText' = toAnsiText (not (globalOpts ^. globalNoColors))
       infotable = Internal.buildTable topModules
-      callMap = Termination.buildCallMap infotable mainModule
+      callMap = Termination.buildCallMap mainModule
       completeGraph = Termination.completeCallGraph callMap
       filteredGraph =
         maybe
diff --git a/app/Commands/Dev/Termination/Calls.hs b/app/Commands/Dev/Termination/Calls.hs
index cbb34b322..e2d4205ef 100644
--- a/app/Commands/Dev/Termination/Calls.hs
+++ b/app/Commands/Dev/Termination/Calls.hs
@@ -2,7 +2,6 @@ module Commands.Dev.Termination.Calls where
 
 import Commands.Base
 import Commands.Dev.Termination.Calls.Options
-import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal
 import Juvix.Compiler.Internal.Pretty qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qualified as Termination
@@ -10,10 +9,9 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qua
 runCommand :: (Members '[Embed IO, App] r) => CallsOptions -> Sem r ()
 runCommand localOpts@CallsOptions {..} = do
   globalOpts <- askGlobalOptions
-  results <- runPipeline _callsInputFile upToInternal
+  results <- runPipelineTermination _callsInputFile upToInternal
   let topModules = results ^. Internal.resultModules
-      infotable = Internal.buildTable topModules
-      callMap0 = Termination.buildCallMap infotable (head topModules)
+      callMap0 = Termination.buildCallMap (head topModules)
       callMap = case _callsFunctionNameFilter of
         Nothing -> callMap0
         Just f -> Termination.filterCallMap f callMap0
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 48dd3e844..b0e753445 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -1,6 +1,12 @@
 module Juvix.Compiler.Internal.Translation.FromConcrete
-  ( module Juvix.Compiler.Internal.Translation.FromConcrete,
-    module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context,
+  ( module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context,
+    fromConcrete,
+    MCache,
+    ConstructorInfos,
+    goModuleNoCache,
+    fromConcreteExpression,
+    fromConcreteImport,
+    fromConcreteOpenImport,
   )
 where
 
@@ -35,7 +41,7 @@ unsupported :: Text -> a
 unsupported msg = error $ msg <> "Scoped to Internal: not yet supported"
 
 fromConcrete ::
-  (Members '[Reader EntryPoint, Error JuvixError, Builtins, NameIdGen] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, Builtins, NameIdGen, Termination] r) =>
   Scoper.ScoperResult ->
   Sem r InternalResult
 fromConcrete _resultScoper =
@@ -127,23 +133,41 @@ buildLetMutualBlocks ss = nonEmpty' . mapMaybe nameToPreStatement $ scomponents
           AcyclicSCC a -> AcyclicSCC <$> a
           CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p)
 
-fromConcreteExpression :: (Members '[Builtins, Error JuvixError, NameIdGen] r) => Scoper.Expression -> Sem r Internal.Expression
-fromConcreteExpression = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goExpression
+fromConcreteExpression :: (Members '[Builtins, Error JuvixError, NameIdGen, Termination] r) => Scoper.Expression -> Sem r Internal.Expression
+fromConcreteExpression e = do
+  e' <-
+    mapError (JuvixError @ScoperError)
+      . runReader @Pragmas mempty
+      . goExpression
+      $ e
+  checkTerminationShallow e'
+  return e'
 
 fromConcreteImport ::
-  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache] r) =>
+  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache, Termination] r) =>
   Scoper.Import 'Scoped ->
   Sem r Internal.Import
-fromConcreteImport =
-  mapError (JuvixError @ScoperError)
-    . runReader @Pragmas mempty
-    . goImport
+fromConcreteImport i = do
+  i' <-
+    mapError (JuvixError @ScoperError)
+      . runReader @Pragmas mempty
+      . goImport
+      $ i
+  checkTerminationShallow i'
+  return i'
 
 fromConcreteOpenImport ::
-  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache] r) =>
+  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache, Termination] r) =>
   Scoper.OpenModule 'Scoped ->
   Sem r (Maybe Internal.Import)
-fromConcreteOpenImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goOpenModule'
+fromConcreteOpenImport i = do
+  i' <-
+    mapError (JuvixError @ScoperError)
+      . runReader @Pragmas mempty
+      . goOpenModule
+      $ i
+  whenJust i' checkTerminationShallow
+  return i'
 
 goLocalModule ::
   (Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos] r) =>
@@ -158,7 +182,7 @@ goTopModule ::
 goTopModule = cacheGet . ModuleIndex
 
 goModuleNoCache ::
-  (Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos] r) =>
+  (Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos, Termination] r) =>
   ModuleIndex ->
   Sem r Internal.Module
 goModuleNoCache (ModuleIndex m) = do
@@ -167,14 +191,7 @@ goModuleNoCache (ModuleIndex m) = do
   let depInfo = buildDependencyInfoPreModule p tbl
   r <- runReader depInfo (fromPreModule p)
   noTerminationOption <- asks (^. entryPointNoTermination)
-  -- TODO we should reuse this table
-  let itbl = buildTableShallow r
-  unless
-    noTerminationOption
-    ( mapError
-        (JuvixError @TerminationError)
-        (checkTermination itbl r)
-    )
+  unless noTerminationOption (checkTerminationShallow r)
   return r
 
 goPragmas :: (Member (Reader Pragmas) r) => Maybe ParsedPragmas -> Sem r Pragmas
@@ -356,11 +373,6 @@ goImport Import {..} = do
         }
     )
 
-guardNotCached :: (Bool, Internal.Module) -> Maybe Internal.Module
-guardNotCached (hit, m) = do
-  guard (not hit)
-  return m
-
 -- | Ignores functions
 goAxiomInductive ::
   forall r.
@@ -377,32 +389,24 @@ goAxiomInductive = \case
   StatementOpenModule {} -> return []
   StatementProjectionDef {} -> return []
 
-goOpenModule' ::
-  forall r.
-  (Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) =>
-  OpenModule 'Scoped ->
-  Sem r (Maybe Internal.Import)
-goOpenModule' o =
-  case o ^. openModuleImportKw of
-    Just kw ->
-      case o ^. openModuleName of
-        ModuleRef' (SModuleTop :&: m) ->
-          Just
-            <$> goImport
-              Import
-                { _importKw = kw,
-                  _importModule = m,
-                  _importAsName = o ^. openImportAsName
-                }
-        _ -> impossible
-    Nothing -> return Nothing
-
 goOpenModule ::
   forall r.
   (Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) =>
   OpenModule 'Scoped ->
   Sem r (Maybe Internal.Import)
-goOpenModule o = goOpenModule' o
+goOpenModule o = runFail $ do
+  case o ^. openModuleImportKw of
+    Nothing -> fail
+    Just kw ->
+      case o ^. openModuleName of
+        ModuleRef' (SModuleTop :&: m) ->
+          goImport
+            Import
+              { _importKw = kw,
+                _importModule = m,
+                _importAsName = o ^. openImportAsName
+              }
+        _ -> impossible
 
 goProjectionDef ::
   forall r.
@@ -977,8 +981,12 @@ goFunctionParameters FunctionParameters {..} = do
             Internal._paramImplicit = _paramImplicit,
             Internal._paramName = goSymbol <$> param
           }
-  return . fromMaybe (pure (mkParam Nothing)) . nonEmpty $
-    mkParam . goFunctionParameter <$> _paramNames
+  return
+    . fromMaybe (pure (mkParam Nothing))
+    . nonEmpty
+    $ mkParam
+      . goFunctionParameter
+      <$> _paramNames
   where
     goFunctionParameter :: FunctionParameter 'Scoped -> Maybe (SymbolType 'Scoped)
     goFunctionParameter = \case
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
index 6cea89455..c7304863c 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
@@ -17,6 +17,7 @@ import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -68,13 +69,12 @@ arityCheckImport i = do
 
 typeCheckExpressionType ::
   forall r.
-  (Members '[Error JuvixError, State Artifacts] r) =>
+  (Members '[Error JuvixError, State Artifacts, Termination] r) =>
   Expression ->
   Sem r TypedExpression
 typeCheckExpressionType exp = do
   table <- extendedTableReplArtifacts exp
-  mapError (JuvixError @TypeCheckerError)
-    . runTypesTableArtifacts
+  runTypesTableArtifacts
     . ignoreHighlightBuilder
     . runFunctionsTableArtifacts
     . runBuiltinsArtifacts
@@ -82,17 +82,19 @@ typeCheckExpressionType exp = do
     . runReader table
     . ignoreOutput @Example
     . withEmptyVars
+    . mapError (JuvixError @TypeCheckerError)
     . runInferenceDef
-    $ inferExpression' Nothing exp >>= traverseOf typedType strongNormalize
+    $ inferExpression' Nothing exp
+      >>= traverseOf typedType strongNormalize
 
 typeCheckExpression ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
+  (Members '[Error JuvixError, State Artifacts, Termination] r) =>
   Expression ->
   Sem r Expression
 typeCheckExpression exp = (^. typedExpression) <$> typeCheckExpressionType exp
 
 typeCheckImport ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   Import ->
   Sem r Import
 typeCheckImport i = do
@@ -113,31 +115,34 @@ typeCheckImport i = do
     $ checkImport i
 
 typeChecking ::
+  forall r.
   (Members '[HighlightBuilder, Error JuvixError, Builtins, NameIdGen] r) =>
-  ArityChecking.InternalArityResult ->
+  Sem (Termination ': r) ArityChecking.InternalArityResult ->
   Sem r InternalTypedResult
-typeChecking res@ArityChecking.InternalArityResult {..} =
-  mapError (JuvixError @TypeCheckerError) $ do
-    (normalized, (idens, (funs, r))) <-
-      runOutputList
-        . runReader entryPoint
-        . runState (mempty :: TypesTable)
-        . runState (mempty :: FunctionsTable)
-        . runReader table
-        . evalCacheEmpty checkModuleNoCache
-        $ mapM checkModule _resultModules
-    return
-      InternalTypedResult
-        { _resultInternalArityResult = res,
-          _resultModules = r,
-          _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],
-          _resultIdenTypes = idens,
-          _resultFunctions = funs,
-          _resultInfoTable = buildTable r
-        }
-  where
-    table :: InfoTable
-    table = buildTable _resultModules
+typeChecking a = do
+  (termin, (res, (normalized, (idens, (funs, r))))) <- runTermination iniTerminationState $ do
+    res <- a
+    let table :: InfoTable
+        table = buildTable (res ^. ArityChecking.resultModules)
 
-    entryPoint :: EntryPoint
-    entryPoint = res ^. ArityChecking.internalArityResultEntryPoint
+        entryPoint :: EntryPoint
+        entryPoint = res ^. ArityChecking.internalArityResultEntryPoint
+    fmap (res,)
+      . runOutputList
+      . runReader entryPoint
+      . runState (mempty :: TypesTable)
+      . runState (mempty :: FunctionsTable)
+      . runReader table
+      . mapError (JuvixError @TypeCheckerError)
+      . evalCacheEmpty checkModuleNoCache
+      $ mapM checkModule (res ^. ArityChecking.resultModules)
+  return
+    InternalTypedResult
+      { _resultInternalArityResult = res,
+        _resultModules = r,
+        _resultTermination = termin,
+        _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],
+        _resultIdenTypes = idens,
+        _resultFunctions = funs,
+        _resultInfoTable = buildTable r
+      }
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/FunctionCall.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/FunctionCall.hs
index 8c1bbb5d5..fa8854541 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/FunctionCall.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/FunctionCall.hs
@@ -70,6 +70,12 @@ addCall fun c = over callMap (HashMap.alter (Just . insertCall c) fun)
       HashMap FunctionRef [FunCall]
     addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callRef) [fc]
 
+registerFunctionDef ::
+  (Members '[State CallMap] r) =>
+  FunctionDef ->
+  Sem r ()
+registerFunctionDef f = modify' (set ((callMapScanned . at (f ^. funDefName))) (Just f))
+
 registerCall ::
   (Members '[State CallMap, Reader FunctionRef] r) =>
   FunCall ->
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
index 904eb3468..a0f7bb980 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
@@ -1,45 +1,110 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
-  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.FunctionCall,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Error,
+  ( Termination,
+    buildCallMap,
+    checkTerminationShallow,
+    runTermination,
+    evalTermination,
+    execTermination,
+    functionIsTerminating,
+    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.TerminationState,
   )
 where
 
 import Data.HashMap.Internal.Strict qualified as HashMap
-import Juvix.Compiler.Internal.Data.InfoTable as Internal
 import Juvix.Compiler.Internal.Language as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.FunctionCall
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.TerminationState
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Error
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.LexOrder
 import Juvix.Prelude
 
-checkTermination ::
-  (Members '[Error TerminationError] r) =>
-  InfoTable ->
-  Module ->
+class Scannable a where
+  buildCallMap :: a -> CallMap
+
+data Termination m a where
+  CheckTerminationShallow :: (Scannable a) => a -> Termination m ()
+  FunctionTermination :: FunctionRef -> Termination m IsTerminating
+
+makeSem ''Termination
+
+functionIsTerminating :: (Members '[Termination] r) => FunctionRef -> Sem r Bool
+functionIsTerminating = fmap terminates . functionTermination
+  where
+    terminates :: IsTerminating -> Bool
+    terminates = \case
+      TerminatingCheckedOrMarked -> True
+      TerminatingFailed -> False
+
+runTermination :: forall r a. (Members '[Error JuvixError] r) => TerminationState -> Sem (Termination ': r) a -> Sem r (TerminationState, a)
+runTermination ini m = do
+  res <- runState ini (re m)
+  checkNonTerminating (fst res)
+  return res
+  where
+    checkNonTerminating :: TerminationState -> Sem r ()
+    checkNonTerminating i =
+      whenJust (i ^. terminationFailedSet . to (nonEmpty . toList)) $
+        throw . JuvixError . ErrNoLexOrder . NoLexOrder
+
+evalTermination :: (Members '[Error JuvixError] r) => TerminationState -> Sem (Termination ': r) a -> Sem r a
+evalTermination s = fmap snd . runTermination s
+
+execTermination :: (Members '[Error JuvixError] r) => TerminationState -> Sem (Termination ': r) a -> Sem r TerminationState
+execTermination s = fmap fst . runTermination s
+
+instance Scannable Import where
+  buildCallMap = buildCallMap . (^. importModule . moduleIxModule)
+
+instance Scannable Module where
+  buildCallMap =
+    run
+      . execState emptyCallMap
+      . scanModule
+
+instance Scannable Expression where
+  buildCallMap =
+    run
+      . execState emptyCallMap
+      . scanTopExpression
+
+re :: Sem (Termination ': r) a -> Sem (State TerminationState ': r) a
+re = reinterpret $ \case
+  CheckTerminationShallow m -> checkTerminationShallow' m
+  FunctionTermination m -> functionTermination' m
+
+-- | If the function is missing, can we assume that it is not recursive
+functionTermination' ::
+  forall r.
+  (Members '[State TerminationState] r) =>
+  FunctionName ->
+  Sem r IsTerminating
+functionTermination' f = fromMaybe TerminatingCheckedOrMarked <$> gets (^. terminationTable . at f)
+
+-- | Returns the set of non-terminating functions. Does not go into imports.
+checkTerminationShallow' ::
+  forall r m.
+  (Members '[State TerminationState] r, Scannable m) =>
+  m ->
   Sem r ()
-checkTermination infotable topModule = do
-  let callmap = buildCallMap infotable topModule
+checkTerminationShallow' topModule = do
+  let callmap = buildCallMap topModule
       completeGraph = completeCallGraph callmap
       rEdges = reflexiveEdges completeGraph
       recBehav = map recursiveBehaviour rEdges
-  forM_ recBehav $ \r -> do
-    let funName = r ^. recursiveBehaviourFun
-        markedTerminating :: Bool = funInfo ^. (Internal.functionInfoDef . Internal.funDefTerminating)
-        funInfo :: FunctionInfo
-        funInfo = HashMap.lookupDefault err funName (infotable ^. Internal.infoFunctions)
+  forM_ recBehav $ \rb -> do
+    let funName = rb ^. recursiveBehaviourFun
+        markedTerminating :: Bool = funInfo ^. Internal.funDefTerminating
+        funInfo :: FunctionDef
+        funInfo = HashMap.lookupDefault err funName (callmap ^. callMapScanned)
           where
             err = error ("Impossible: function not found: " <> funName ^. nameText)
-    if
-        | markedTerminating -> return ()
-        | otherwise ->
-            case findOrder r of
-              Nothing -> throw (ErrNoLexOrder (NoLexOrder funName))
-              Just _ -> return ()
-
-buildCallMap :: InfoTable -> Module -> CallMap
-buildCallMap infotable = run . execState mempty . runReader infotable . scanModule
+        order = findOrder rb
+    addTerminating funName $
+      if
+          | markedTerminating -> TerminatingCheckedOrMarked
+          | Nothing <- order -> TerminatingFailed
+          | Just {} <- order -> TerminatingCheckedOrMarked
 
 scanModule ::
   (Members '[State CallMap] r) =>
@@ -48,31 +113,51 @@ scanModule ::
 scanModule m = scanModuleBody (m ^. moduleBody)
 
 scanModuleBody :: (Members '[State CallMap] r) => ModuleBody -> Sem r ()
-scanModuleBody body =
-  mapM_ scanFunctionDef moduleFunctions
+scanModuleBody body = mapM_ scanStatement (body ^. moduleStatements)
+
+scanStatement :: (Members '[State CallMap] r) => Statement -> Sem r ()
+scanStatement = \case
+  StatementAxiom a -> scanAxiom a
+  StatementMutual m -> scanMutual m
+
+scanMutual :: (Members '[State CallMap] r) => MutualBlock -> Sem r ()
+scanMutual (MutualBlock ss) = mapM_ scanMutualStatement ss
+
+scanInductive :: forall r. (Members '[State CallMap] r) => InductiveDef -> Sem r ()
+scanInductive i = do
+  scanTopExpression (i ^. inductiveType)
+  mapM_ scanConstructor (i ^. inductiveConstructors)
   where
-    moduleFunctions =
-      [ f | StatementMutual (MutualBlock m) <- body ^. moduleStatements, StatementFunction f <- toList m
-      ]
+    scanConstructor :: ConstructorDef -> Sem r ()
+    scanConstructor c = scanTopExpression (c ^. inductiveConstructorType)
+
+scanMutualStatement :: (Members '[State CallMap] r) => MutualStatement -> Sem r ()
+scanMutualStatement = \case
+  StatementInductive i -> scanInductive i
+  StatementFunction i -> scanFunctionDef i
+
+scanAxiom :: (Members '[State CallMap] r) => AxiomDef -> Sem r ()
+scanAxiom = scanTopExpression . (^. axiomType)
 
 scanFunctionDef ::
   (Members '[State CallMap] r) =>
   FunctionDef ->
   Sem r ()
-scanFunctionDef FunctionDef {..} =
-  runReader _funDefName $ do
+scanFunctionDef f@FunctionDef {..} = do
+  registerFunctionDef f
+  runReader (Just _funDefName) $ do
     scanTypeSignature _funDefType
     mapM_ scanFunctionClause _funDefClauses
 
 scanTypeSignature ::
-  (Members '[State CallMap, Reader FunctionRef] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef)] r) =>
   Expression ->
   Sem r ()
 scanTypeSignature = runReader emptySizeInfo . scanExpression
 
 scanFunctionClause ::
   forall r.
-  (Members '[State CallMap, Reader FunctionRef] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef)] r) =>
   FunctionClause ->
   Sem r ()
 scanFunctionClause FunctionClause {..} = go (reverse _clausePatterns) _clauseBody
@@ -86,7 +171,7 @@ scanFunctionClause FunctionClause {..} = go (reverse _clausePatterns) _clauseBod
         goClause (LambdaClause pats clBody) = go (reverse (toList pats) ++ revArgs) clBody
 
 scanCase ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Case ->
   Sem r ()
 scanCase c = do
@@ -94,13 +179,13 @@ scanCase c = do
   scanExpression (c ^. caseExpression)
 
 scanCaseBranch ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   CaseBranch ->
   Sem r ()
 scanCaseBranch = scanExpression . (^. caseBranchExpression)
 
 scanLet ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Let ->
   Sem r ()
 scanLet l = do
@@ -116,14 +201,20 @@ scanLetClause = \case
 scanMutualBlockLet :: (Members '[State CallMap] r) => MutualBlockLet -> Sem r ()
 scanMutualBlockLet MutualBlockLet {..} = mapM_ scanFunctionDef _mutualLet
 
+scanTopExpression ::
+  (Members '[State CallMap] r) =>
+  Expression ->
+  Sem r ()
+scanTopExpression = runReader (Nothing @FunctionRef) . runReader emptySizeInfo . scanExpression
+
 scanExpression ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Expression ->
   Sem r ()
 scanExpression e =
   viewCall e >>= \case
     Just c -> do
-      registerCall c
+      whenJustM (ask @(Maybe FunctionRef)) (\caller -> runReader caller (registerCall c))
       mapM_ (scanExpression . snd) (c ^. callArgs)
     Nothing -> case e of
       ExpressionApplication a -> scanApplication a
@@ -139,14 +230,14 @@ scanExpression e =
 
 scanSimpleLambda ::
   forall r.
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   SimpleLambda ->
   Sem r ()
 scanSimpleLambda SimpleLambda {..} = scanExpression _slambdaBody
 
 scanLambda ::
   forall r.
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Lambda ->
   Sem r ()
 scanLambda Lambda {..} = mapM_ scanClause _lambdaClauses
@@ -155,7 +246,7 @@ scanLambda Lambda {..} = mapM_ scanClause _lambdaClauses
     scanClause LambdaClause {..} = scanExpression _lambdaBody
 
 scanApplication ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Application ->
   Sem r ()
 scanApplication (Application l r _) = do
@@ -163,7 +254,7 @@ scanApplication (Application l r _) = do
   scanExpression r
 
 scanFunction ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Function ->
   Sem r ()
 scanFunction (Function l r) = do
@@ -171,7 +262,7 @@ scanFunction (Function l r) = do
   scanExpression r
 
 scanFunctionParameter ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   FunctionParameter ->
   Sem r ()
 scanFunctionParameter p = scanExpression (p ^. paramType)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/FunctionCall.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/FunctionCall.hs
index 278f22b37..a5843f145 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/FunctionCall.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/FunctionCall.hs
@@ -9,10 +9,10 @@ import Juvix.Prelude
 
 type FunctionRef = FunctionName
 
-newtype CallMap = CallMap
-  { _callMap :: HashMap FunctionRef (HashMap FunctionRef [FunCall])
+data CallMap = CallMap
+  { _callMap :: HashMap FunctionRef (HashMap FunctionRef [FunCall]),
+    _callMapScanned :: HashMap FunctionRef FunctionDef
   }
-  deriving newtype (Semigroup, Monoid)
 
 data FunCall = FunCall
   { _callRef :: FunctionRef,
@@ -91,7 +91,7 @@ instance PrettyCode CallMap where
     (Members '[Reader Options] r) =>
     CallMap ->
     Sem r (Doc Ann)
-  ppCode (CallMap m) = vsep <$> mapM ppEntry (HashMap.toList m)
+  ppCode (CallMap m _) = vsep <$> mapM ppEntry (HashMap.toList m)
     where
       ppEntry :: (FunctionRef, HashMap FunctionRef [FunCall]) -> Sem r (Doc Ann)
       ppEntry (fun, mcalls) = do
@@ -115,3 +115,10 @@ kwQuestion = keyword Str.questionMark
 
 kwWaveArrow :: Doc Ann
 kwWaveArrow = keyword Str.waveArrow
+
+emptyCallMap :: CallMap
+emptyCallMap =
+  CallMap
+    { _callMap = mempty,
+      _callMapScanned = mempty
+    }
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/TerminationState.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/TerminationState.hs
new file mode 100644
index 000000000..6b22ce881
--- /dev/null
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/TerminationState.hs
@@ -0,0 +1,49 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.TerminationState
+  ( IsTerminating (..),
+    TerminationState,
+    iniTerminationState,
+    addTerminating,
+    terminationTable,
+    terminationFailedSet,
+  )
+where
+
+import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Internal.Language
+import Juvix.Prelude
+
+data IsTerminating
+  = -- | Has been checked or marked for termination.
+    TerminatingCheckedOrMarked
+  | -- | Has been checked for termination but failed.
+    TerminatingFailed
+
+data TerminationState = TerminationState
+  { _iterminationTable :: HashMap FunctionName IsTerminating,
+    _iterminationFailed :: HashSet FunctionName
+  }
+
+makeLenses ''TerminationState
+
+iniTerminationState :: TerminationState
+iniTerminationState =
+  TerminationState
+    { _iterminationTable = mempty,
+      _iterminationFailed = mempty
+    }
+
+addTerminating :: (Members '[State TerminationState] r) => FunctionName -> IsTerminating -> Sem r ()
+addTerminating f i = do
+  modify' (set (iterminationTable . at f) (Just i))
+  when isFailed (modify' (over iterminationFailed (HashSet.insert f)))
+  where
+    isFailed :: Bool
+    isFailed = case i of
+      TerminatingFailed -> True
+      TerminatingCheckedOrMarked -> False
+
+terminationTable :: SimpleGetter TerminationState (HashMap FunctionName IsTerminating)
+terminationTable = iterminationTable
+
+terminationFailedSet :: SimpleGetter TerminationState (HashSet FunctionName)
+terminationFailedSet = iterminationFailed
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Error/Types.hs
index e0ec0204e..cadbe154b 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Error/Types.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Error/Types.hs
@@ -5,7 +5,7 @@ import Juvix.Data.PPOutput
 import Juvix.Prelude
 
 newtype NoLexOrder = NoLexOrder
-  { _noLexOrderFun :: Name
+  { _noLexOrderFun :: NonEmpty Name
   }
   deriving stock (Show)
 
@@ -20,11 +20,26 @@ instance ToGenericError NoLexOrder where
           _genericErrorIntervals = [i]
         }
     where
-      name = _noLexOrderFun
-      i = getLoc name
+      names = _noLexOrderFun
+      i = getLocSpan names
 
+      single = case names of
+        _ :| [] -> True
+        _ -> False
       msg :: Doc Ann
       msg = do
-        "The function"
-          <+> code (pretty name)
-          <+> "fails the termination checker."
+        "The following"
+          <+> function
+          <+> fails
+          <+> "the termination checker:"
+            <> line
+            <> itemize (fmap (code . pretty) names)
+        where
+          function :: Doc Ann
+          function
+            | single = "function"
+            | otherwise = "functions"
+          fails :: Doc Ann
+          fails
+            | single = "fails"
+            | otherwise = "fail"
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
index 248ac91b1..3f19ab5e1 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -11,6 +11,7 @@ import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (Termination)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
@@ -43,7 +44,7 @@ checkModuleIndex ::
 checkModuleIndex = fmap ModuleIndex . cacheGet
 
 checkModuleNoCache ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) =>
   ModuleIndex ->
   Sem r Module
 checkModuleNoCache (ModuleIndex Module {..}) = do
@@ -61,7 +62,7 @@ checkModuleNoCache (ModuleIndex Module {..}) = do
       }
 
 checkModuleBody ::
-  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -74,13 +75,13 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkImport ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) =>
   Import ->
   Sem r Import
 checkImport = traverseOf importModule checkModuleIndex
 
 checkStatement ::
-  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) =>
   Statement ->
   Sem r Statement
 checkStatement s = case s of
@@ -91,7 +92,7 @@ checkStatement s = case s of
 
 checkInductiveDef ::
   forall r.
-  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins, Termination] r) =>
   InductiveDef ->
   Sem r InductiveDef
 checkInductiveDef InductiveDef {..} = runInferenceDef $ do
@@ -155,14 +156,14 @@ withEmptyVars = runReader emptyLocalVars
 
 -- TODO should we register functions (type synonyms) first?
 checkTopMutualBlock ::
-  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) =>
   MutualBlock ->
   Sem r MutualBlock
 checkTopMutualBlock (MutualBlock ds) =
   MutualBlock <$> runInferenceDefs (mapM checkMutualStatement ds)
 
 checkMutualStatement ::
-  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) =>
   MutualStatement ->
   Sem r MutualStatement
 checkMutualStatement = \case
@@ -170,7 +171,7 @@ checkMutualStatement = \case
   StatementInductive f -> StatementInductive <$> checkInductiveDef f
 
 checkFunctionDef ::
-  (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference] r) =>
+  (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference, Termination] r) =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
@@ -188,7 +189,7 @@ checkFunctionDef FunctionDef {..} = do
   traverseOf funDefExamples (mapM checkExample) funDef
 
 checkIsType ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   Interval ->
   Expression ->
   Sem r Expression
@@ -196,7 +197,7 @@ checkIsType = checkExpression . smallUniverseE
 
 checkDefType ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   Expression ->
   Sem r Expression
 checkDefType ty = checkIsType loc ty
@@ -204,7 +205,7 @@ checkDefType ty = checkIsType loc ty
     loc = getLoc ty
 
 checkExample ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable, Termination] r) =>
   Example ->
   Sem r Example
 checkExample e = do
@@ -214,7 +215,7 @@ checkExample e = do
 
 checkExpression ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, State TypesTable, Termination] r) =>
   Expression ->
   Expression ->
   Sem r Expression
@@ -238,7 +239,7 @@ checkExpression expectedTy e = do
           )
 
 checkFunctionParameter ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   FunctionParameter ->
   Sem r FunctionParameter
 checkFunctionParameter (FunctionParameter mv i e) = do
@@ -287,7 +288,7 @@ checkConstructorReturnType indType ctor = do
     )
 
 inferExpression ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   Maybe Expression -> -- type hint
   Expression ->
   Sem r Expression
@@ -300,7 +301,7 @@ lookupVar v = HashMap.lookupDefault err v <$> asks (^. localTypes)
 
 checkFunctionClause ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins, State TypesTable, Output Example, Reader LocalVars] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins, State TypesTable, Output Example, Reader LocalVars, Termination] r) =>
   Expression ->
   FunctionClause ->
   Sem r FunctionClause
@@ -316,7 +317,7 @@ checkFunctionClause clauseType FunctionClause {..} = do
 -- | helper function for function clauses and lambda functions
 checkClause ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   -- | Type
   Expression ->
   -- | Arguments
@@ -508,7 +509,7 @@ checkPattern = go
 
 inferExpression' ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins, Termination] r) =>
   Maybe Expression ->
   Expression ->
   Sem r TypedExpression
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs
index 97abf4d48..3cd57a05b 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs
@@ -10,6 +10,7 @@ import Juvix.Compiler.Internal.Data.InfoTable
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context (InternalArityResult)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Arity
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (TerminationState)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable
 import Juvix.Compiler.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude
@@ -21,6 +22,7 @@ type NormalizedTable = HashMap NameId Expression
 data InternalTypedResult = InternalTypedResult
   { _resultInternalArityResult :: InternalArityResult,
     _resultModules :: NonEmpty Module,
+    _resultTermination :: TerminationState,
     _resultNormalized :: NormalizedTable,
     _resultIdenTypes :: TypesTable,
     _resultFunctions :: FunctionsTable,
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
index 66e35289b..af6ff7555 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@@ -8,6 +8,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Concrete.Data.Highlight.Input
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
@@ -417,10 +418,16 @@ addIdens idens = do
   modify (HashMap.union idens)
   modify (over highlightTypes (HashMap.union idens))
 
--- | Assumes the given function has been type checked.
--- Does *not* register the function.
--- Throws an error if the return type is Type and returns Nothing.
-functionDefEval :: forall r'. (Members '[State FunctionsTable, Error TypeCheckerError] r') => FunctionDef -> Sem r' (Maybe Expression)
+-- | Assumes the given function has been type checked. Does *not* register the
+-- function.
+-- Conditons:
+-- 1. Only one clause.
+-- 2. No pattern matching.
+-- 3. Terminates.
+--
+-- Throws an error if the return type is Type and it does not satisfy the
+-- some condition.
+functionDefEval :: forall r'. (Members '[State FunctionsTable, Termination, Error TypeCheckerError] r') => FunctionDef -> Sem r' (Maybe Expression)
 functionDefEval f = do
   r <- runFail goTop
   retTy <- returnsType
@@ -439,12 +446,16 @@ functionDefEval f = do
     returnsType :: (Members '[State FunctionsTable] r) => Sem r Bool
     returnsType = isUniverse ret
 
-    goTop :: forall r. (Members '[Fail, State FunctionsTable, Error TypeCheckerError] r) => Sem r Expression
-    goTop =
+    goTop :: forall r. (Members '[Fail, State FunctionsTable, Error TypeCheckerError, Termination] r) => Sem r Expression
+    goTop = do
+      checkTerminating
       case f ^. funDefClauses of
         c :| [] -> goClause c
         _ -> fail
       where
+        checkTerminating :: Sem r ()
+        checkTerminating = unlessM (functionIsTerminating (f ^. funDefName)) fail
+
         goClause :: FunctionClause -> Sem r Expression
         goClause c = do
           let pats = c ^. clausePatterns
@@ -472,6 +483,6 @@ functionDefEval f = do
                 | Implicit <- p ^. patternArgIsImplicit -> fail
                 | otherwise -> go ps >>= goPattern (p ^. patternArgPattern, ty)
 
-registerFunctionDef :: (Members '[State FunctionsTable, Error TypeCheckerError] r) => FunctionDef -> Sem r ()
+registerFunctionDef :: (Members '[State FunctionsTable, Error TypeCheckerError, Termination] r) => FunctionDef -> Sem r ()
 registerFunctionDef f = whenJustM (functionDefEval f) $ \e ->
   modify (over functionsTable (HashMap.insert (f ^. funDefName) e))
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
index 37031edd5..5324c87d4 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@@ -335,7 +335,7 @@ instance ToGenericError UnsupportedTypeFunction where
             <+> ppCode opts (_unsupportedTypeFunction ^. funDefName)
               <> "."
               <> line
-              <> "Only functions with a single clause and no pattern matching are supported."
+              <> "Only terminating functions with a single clause and no pattern matching are supported."
     return
       GenericError
         { _genericErrorLoc = i,
diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs
index 26e7e28cf..30a21b101 100644
--- a/src/Juvix/Compiler/Pipeline.hs
+++ b/src/Juvix/Compiler/Pipeline.hs
@@ -29,6 +29,7 @@ import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Arity
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -57,19 +58,19 @@ upToScoping ::
 upToScoping = upToParsing >>= Scoper.fromParsed
 
 upToInternal ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver, Termination] r) =>
   Sem r Internal.InternalResult
 upToInternal = upToScoping >>= Internal.fromConcrete
 
 upToInternalArity ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver, Termination] r) =>
   Sem r Internal.InternalArityResult
 upToInternalArity = upToInternal >>= Internal.arityChecking
 
 upToInternalTyped ::
   (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
   Sem r Internal.InternalTypedResult
-upToInternalTyped = upToInternalArity >>= Internal.typeChecking
+upToInternalTyped = Internal.typeChecking upToInternalArity
 
 upToInternalReachability ::
   (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
@@ -162,6 +163,9 @@ coreToVampIR' = Core.toVampIR' >=> return . VampIR.toResult . VampIR.fromCore
 runIOEither :: forall a. EntryPoint -> Sem PipelineEff a -> IO (Either JuvixError (ResolverState, a))
 runIOEither entry = fmap snd . runIOEitherHelper entry
 
+runIOEitherTermination :: forall a. EntryPoint -> Sem (Termination ': PipelineEff) a -> IO (Either JuvixError (ResolverState, a))
+runIOEitherTermination entry = fmap snd . runIOEitherHelper entry . evalTermination iniTerminationState
+
 runPipelineHighlight :: forall a. EntryPoint -> Sem PipelineEff a -> IO HighlightInput
 runPipelineHighlight entry = fmap fst . runIOEitherHelper entry
 
@@ -253,20 +257,22 @@ corePipelineIOEither entry = do
           mainModuleScope_ :: Scope
           mainModuleScope_ = Scoped.mainModuleSope scopedResult
        in Right $
-            foldl'
-              (flip ($))
-              art
-              [ set artifactMainModuleScope (Just mainModuleScope_),
-                set artifactParsing (parserResult ^. P.resultBuilderState),
-                set artifactInternalModuleCache (internalResult ^. Internal.resultModulesCache),
-                set artifactInternalTypedTable typedTable,
-                set artifactCoreTable coreTable,
-                set artifactScopeTable resultScoperTable,
-                set artifactScopeExports (scopedResult ^. Scoped.resultExports),
-                set artifactTypes typesTable,
-                set artifactFunctions functionsTable,
-                set artifactScoperState (scopedResult ^. Scoped.resultScoperState)
-              ]
+            Artifacts
+              { _artifactMainModuleScope = Just mainModuleScope_,
+                _artifactParsing = parserResult ^. P.resultBuilderState,
+                _artifactInternalModuleCache = internalResult ^. Internal.resultModulesCache,
+                _artifactInternalTypedTable = typedTable,
+                _artifactTerminationState = typedResult ^. Typed.resultTermination,
+                _artifactCoreTable = coreTable,
+                _artifactScopeTable = resultScoperTable,
+                _artifactScopeExports = scopedResult ^. Scoped.resultExports,
+                _artifactTypes = typesTable,
+                _artifactFunctions = functionsTable,
+                _artifactScoperState = scopedResult ^. Scoped.resultScoperState,
+                _artifactResolver = art ^. artifactResolver,
+                _artifactBuiltins = art ^. artifactBuiltins,
+                _artifactNameIdState = art ^. artifactNameIdState
+              }
   where
     initialArtifacts :: Artifacts
     initialArtifacts =
@@ -275,6 +281,7 @@ corePipelineIOEither entry = do
           _artifactMainModuleScope = Nothing,
           _artifactInternalTypedTable = mempty,
           _artifactTypes = mempty,
+          _artifactTerminationState = iniTerminationState,
           _artifactResolver = PathResolver.iniResolverState,
           _artifactNameIdState = allNameIds,
           _artifactFunctions = mempty,
diff --git a/src/Juvix/Compiler/Pipeline/Artifacts.hs b/src/Juvix/Compiler/Pipeline/Artifacts.hs
index ea4f3a1a2..8d47ff5bd 100644
--- a/src/Juvix/Compiler/Pipeline/Artifacts.hs
+++ b/src/Juvix/Compiler/Pipeline/Artifacts.hs
@@ -19,6 +19,7 @@ import Juvix.Compiler.Core.Data.InfoTableBuilder qualified as Core
 import Juvix.Compiler.Internal.Extra.DependencyBuilder (ExportsTable)
 import Juvix.Compiler.Internal.Language qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Prelude
@@ -37,6 +38,7 @@ data Artifacts = Artifacts
     _artifactScoperState :: Scoped.ScoperState,
     -- Concrete -> Internal
     _artifactInternalModuleCache :: Internal.ModulesCache,
+    _artifactTerminationState :: TerminationState,
     -- Typechecking
     _artifactTypes :: TypesTable,
     _artifactFunctions :: FunctionsTable,
@@ -93,6 +95,9 @@ runFunctionsTableArtifacts = runStateArtifacts artifactFunctions
 readerTypesTableArtifacts :: (Members '[State Artifacts] r) => Sem (Reader TypesTable ': r) a -> Sem r a
 readerTypesTableArtifacts = runReaderArtifacts artifactTypes
 
+runTerminationArtifacts :: (Members '[Error JuvixError, State Artifacts] r) => Sem (Termination ': r) a -> Sem r a
+runTerminationArtifacts = runStateLikeArtifacts runTermination artifactTerminationState
+
 runTypesTableArtifacts :: (Members '[State Artifacts] r) => Sem (State TypesTable ': r) a -> Sem r a
 runTypesTableArtifacts = runStateArtifacts artifactTypes
 
@@ -131,8 +136,8 @@ runFromConcreteCache ::
 runFromConcreteCache =
   runCacheArtifacts
     (artifactInternalModuleCache . Internal.cachedModules)
-    ( mapError (JuvixError @ScoperError)
-        . runReader (mempty :: Pragmas)
-        . evalState (mempty :: Internal.ConstructorInfos)
-        . Internal.goModuleNoCache
-    )
+    $ mapError (JuvixError @ScoperError)
+      . runReader (mempty :: Pragmas)
+      . evalState (mempty :: Internal.ConstructorInfos)
+      . runTerminationArtifacts
+      . Internal.goModuleNoCache
diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs
index 923271d21..5fddccc3c 100644
--- a/src/Juvix/Compiler/Pipeline/Repl.hs
+++ b/src/Juvix/Compiler/Pipeline/Repl.hs
@@ -11,12 +11,13 @@ import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
 import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as FromConcrete
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Prelude
 
 arityCheckExpression ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
+  (Members '[Error JuvixError, State Artifacts, Termination] r) =>
   ExpressionAtoms 'Parsed ->
   Sem r Internal.Expression
 arityCheckExpression p = do
@@ -93,7 +94,7 @@ runToInternal m = do
     $ m
 
 openImportToInternal ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   OpenModule 'Parsed ->
   Sem r (Maybe Internal.Import)
 openImportToInternal o = runToInternal $ do
@@ -101,18 +102,18 @@ openImportToInternal o = runToInternal $ do
     >>= Internal.fromConcreteOpenImport
 
 importToInternal ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   Import 'Parsed ->
   Sem r Internal.Import
 importToInternal i = runToInternal $ do
   Scoper.scopeCheckImport i
     >>= Internal.fromConcreteImport
 
-importToInternal' ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+importToInternalTyped ::
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   Internal.Import ->
   Sem r Internal.Import
-importToInternal' = Internal.arityCheckImport >=> Internal.typeCheckImport
+importToInternalTyped = Internal.arityCheckImport >=> Internal.typeCheckImport
 
 parseReplInput ::
   (Members '[PathResolver, Files, State Artifacts, Error JuvixError] r) =>
@@ -132,32 +133,40 @@ expressionUpToTyped ::
   Sem r Internal.TypedExpression
 expressionUpToTyped fp txt = do
   p <- expressionUpToAtomsParsed fp txt
-  arityCheckExpression p
-    >>= Internal.typeCheckExpressionType
+  runTerminationArtifacts
+    ( arityCheckExpression p
+        >>= Internal.typeCheckExpressionType
+    )
 
 compileExpression ::
   (Members '[Error JuvixError, State Artifacts] r) =>
   ExpressionAtoms 'Parsed ->
   Sem r Core.Node
 compileExpression p = do
-  arityCheckExpression p
-    >>= Internal.typeCheckExpression
+  runTerminationArtifacts
+    ( arityCheckExpression p
+        >>= Internal.typeCheckExpression
+    )
     >>= fromInternalExpression
 
 registerImport ::
   (Members '[Error JuvixError, State Artifacts, Reader EntryPoint] r) =>
   Import 'Parsed ->
   Sem r ()
-registerImport =
-  importToInternal >=> importToInternal' >=> fromInternalImport
+registerImport p =
+  runTerminationArtifacts
+    ( importToInternal p
+        >>= importToInternalTyped
+    )
+    >>= fromInternalImport
 
 registerOpenImport ::
   (Members '[Error JuvixError, State Artifacts, Reader EntryPoint] r) =>
   OpenModule 'Parsed ->
   Sem r ()
-registerOpenImport o = do
-  mImport <- openImportToInternal o
-  whenJust mImport (importToInternal' >=> fromInternalImport)
+registerOpenImport o = ignoreFail $ do
+  mImport <- runTerminationArtifacts (openImportToInternal o >>= failMaybe >>= importToInternalTyped)
+  fromInternalImport mImport
 
 fromInternalImport :: (Members '[State Artifacts] r) => Internal.Import -> Sem r ()
 fromInternalImport i = do
diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs
index 9fc79c8c2..0d8cb70fd 100644
--- a/test/Arity/Negative.hs
+++ b/test/Arity/Negative.hs
@@ -21,7 +21,7 @@ testDescr NegTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- defaultEntryPointCwdIO file'
-            result <- runIOEither entryPoint upToInternalArity
+            result <- runIOEitherTermination entryPoint upToInternalArity
             case mapLeft fromJuvixError result of
               Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
               Left Nothing -> assertFailure "The arity checker did not find an error."
@@ -97,5 +97,12 @@ tests =
       $(mkRelFile "LazyBuiltin.juvix")
       $ \case
         ErrBuiltinNotFullyApplied {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "issue 2293: Non-terminating function with arity error"
+      $(mkRelDir "Internal")
+      $(mkRelFile "issue2293.juvix")
+      $ \case
+        ErrWrongConstructorAppLength {} -> Nothing
         _ -> wrongError
   ]
diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs
index 57f6cae95..7bb4e8691 100644
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@@ -24,7 +24,7 @@ testDescr NegTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- defaultEntryPointCwdIO file'
-            res <- runIOEither entryPoint upToInternal
+            res <- runIOEitherTermination entryPoint upToInternal
             case mapLeft fromJuvixError res of
               Left (Just err) -> whenJust (_checkErr err) assertFailure
               Left Nothing -> assertFailure "An error ocurred but it was not in the scoper."
diff --git a/test/Termination/Negative.hs b/test/Termination/Negative.hs
index f42bc4603..139c262df 100644
--- a/test/Termination/Negative.hs
+++ b/test/Termination/Negative.hs
@@ -21,7 +21,7 @@ testDescr NegTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- set entryPointNoStdlib True <$> defaultEntryPointCwdIO file'
-            result <- runIOEither entryPoint upToInternal
+            result <- runIOEither entryPoint upToInternalTyped
             case mapLeft fromJuvixError result of
               Left (Just lexError) -> whenJust (_checkErr lexError) assertFailure
               Left Nothing -> assertFailure "The termination checker did not find an error."
@@ -73,6 +73,12 @@ tests =
       "Quicksort is not terminating"
       $(mkRelDir ".")
       $(mkRelFile "Data/QuickSort.juvix")
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Loop in axiom type"
+      $(mkRelDir ".")
+      $(mkRelFile "Axiom.juvix")
       $ \case
         ErrNoLexOrder {} -> Nothing
   ]
diff --git a/test/Termination/Positive.hs b/test/Termination/Positive.hs
index 44b9117bb..9b94fc0b5 100644
--- a/test/Termination/Positive.hs
+++ b/test/Termination/Positive.hs
@@ -21,7 +21,7 @@ testDescr PosTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- set entryPointNoStdlib True <$> defaultEntryPointCwdIO file'
-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' entryPoint) upToInternalTyped
         }
 
 --------------------------------------------------------------------------------
@@ -43,7 +43,7 @@ testDescrFlag N.NegTest {..} =
               set entryPointNoTermination True
                 . set entryPointNoStdlib True
                 <$> defaultEntryPointCwdIO file'
-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' entryPoint) upToInternalTyped
         }
 
 tests :: [PosTest]
diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
index 1a04dcd43..eccf640c6 100644
--- a/test/Typecheck/Positive.hs
+++ b/test/Typecheck/Positive.hs
@@ -47,7 +47,7 @@ testNoPositivityFlag N.NegTest {..} =
             entryPoint <-
               set entryPointNoPositivity True
                 <$> defaultEntryPointCwdIO file'
-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' entryPoint) upToInternalTyped
         }
 
 negPositivityTests :: [N.NegTest]
diff --git a/tests/negative/Internal/issue2293.juvix b/tests/negative/Internal/issue2293.juvix
new file mode 100644
index 000000000..65b0641b9
--- /dev/null
+++ b/tests/negative/Internal/issue2293.juvix
@@ -0,0 +1,7 @@
+module issue2293;
+
+type List A := nil | cons A (List A);
+
+map {A B} (f : A → B) : List A → List B
+  | nil := nil
+  | cons h t := cons (f h) (map f t);
diff --git a/tests/negative/Termination/Axiom.juvix b/tests/negative/Termination/Axiom.juvix
new file mode 100644
index 000000000..3c849a06c
--- /dev/null
+++ b/tests/negative/Termination/Axiom.juvix
@@ -0,0 +1,5 @@
+module Axiom;
+
+axiom A : let
+    x : Type := x;
+  in x;
diff --git a/tests/negative/Termination/Data/Bool.juvix b/tests/negative/Termination/Data/Bool.juvix
index a954caa42..88f75fa15 100644
--- a/tests/negative/Termination/Data/Bool.juvix
+++ b/tests/negative/Termination/Data/Bool.juvix
@@ -18,9 +18,9 @@ syntax operator && logical;
   | false _ := false
   | true a := a;
 
-ite : (a : Type) → Bool → a → a → a
-  | _ true a _ := a
-  | _ false _ b := b;
+ite : {a : Type} → Bool → a → a → a
+  | true a _ := a
+  | false _ b := b;
 
 not : Bool → Bool
   | true := false
diff --git a/tests/negative/Termination/Data/QuickSort.juvix b/tests/negative/Termination/Data/QuickSort.juvix
index 6c2879d59..b19984710 100644
--- a/tests/negative/Termination/Data/QuickSort.juvix
+++ b/tests/negative/Termination/Data/QuickSort.juvix
@@ -10,33 +10,30 @@ type List (A : Type) :=
   | nil : List A
   | cons : A → List A → List A;
 
-filter : (A : Type) → (A → Bool) → List A → List A
-  | A f nil := nil A
-  | A f (cons h hs) :=
+filter : {A : Type} → (A → Bool) → List A → List A
+  | f nil := nil
+  | f (cons h hs) :=
     ite
-      (List A)
       (f h)
-      (cons A h (filter A f hs))
-      (filter A f hs);
+      (cons h (filter f hs))
+      (filter f hs);
 
-concat : (A : Type) → List A → List A → List A
-  | A nil ys := ys
-  | A (cons x xs) ys := cons A x (concat A xs ys);
+concat : {A : Type} → List A → List A → List A
+  | nil ys := ys
+  | (cons x xs) ys := cons x (concat xs ys);
 
-ltx : (A : Type) → (A → A → Bool) → A → A → Bool
-  | A lessThan x y := lessThan y x;
+ltx : {A : Type} → (A → A → Bool) → A → A → Bool
+  | lessThan x y := lessThan y x;
 
-gex : (A : Type) → (A → A → Bool) → A → A → Bool
-  | A lessThan x y := not (ltx A lessThan x y);
+gex : {A : Type} → (A → A → Bool) → A → A → Bool
+  | lessThan x y := not (ltx lessThan x y);
 
-quicksort : (A : Type) → (A → A → Bool) → List A → List A
-  | A _ nil := nil A
-  | A _ (cons x nil) := cons A x (nil A)
-  | A lessThan (cons x ys) :=
+quicksort : {A : Type} → (A → A → Bool) → List A → List A
+  | _ nil := nil
+  | _ (cons x nil) := cons x nil
+  | lessThan (cons x ys) :=
     concat
-      A
-      (quicksort A lessThan (filter A (ltx A lessThan x) ys))
+      (quicksort lessThan (filter (ltx lessThan x) ys))
       (concat
-        A
-        (cons A x (nil A))
-        (quicksort A lessThan (filter A (gex A lessThan x)) ys));
+        (cons x nil)
+        (quicksort lessThan (filter (gex lessThan x) ys)));
diff --git a/tests/negative/Termination/Ord.juvix b/tests/negative/Termination/Ord.juvix
index 8bf362f7c..2c94f4c59 100644
--- a/tests/negative/Termination/Ord.juvix
+++ b/tests/negative/Termination/Ord.juvix
@@ -17,4 +17,3 @@ addord : Ord -> Ord -> Ord
 aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord
   
   | f y z := addord (f z) y;
-
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
index 36e97d2ab..9678ba15b 100644
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@@ -1,6 +1,20 @@
 working-directory: ./../../../tests/
 
 tests:
+  - name: repl-non-terminating
+    command:
+      - juvix
+      - repl
+    stdin: "let x : Bool := x in x"
+    stdout:
+      matches: |
+        .*
+    stderr:
+      contains: |
+        The following function fails the termination checker:
+        • x
+    exit-status: 0
+
   - name: repl-doc
     command:
       - juvix