Remove old typechecker (#2545)

app/Commands/Dev/Internal.hs

@@ -1,7 +1,6 @@
 module Commands.Dev.Internal where
 
 import Commands.Base
-import Commands.Dev.Internal.Arity qualified as Arity
 import Commands.Dev.Internal.Options
 import Commands.Dev.Internal.Pretty qualified as Pretty
 import Commands.Dev.Internal.Reachability qualified as Reachability
@@ -10,6 +9,5 @@ import Commands.Dev.Internal.Typecheck qualified as Typecheck
 runCommand :: (Members '[Embed IO, App] r) => InternalCommand -> Sem r ()
 runCommand = \case
   Pretty opts -> Pretty.runCommand opts
-  Arity opts -> Arity.runCommand opts
   TypeCheck opts -> Typecheck.runCommand opts
   Reachability opts -> Reachability.runCommand opts

app/Commands/Dev/Internal/Arity.hs

@@ -1,12 +0,0 @@
-module Commands.Dev.Internal.Arity where
-
-import Commands.Base
-import Commands.Dev.Internal.Arity.Options
-import Juvix.Compiler.Internal.Pretty qualified as Internal
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity
-
-runCommand :: (Members '[Embed IO, App] r) => InternalArityOptions -> Sem r ()
-runCommand opts = do
-  globalOpts <- askGlobalOptions
-  micro <- head . (^. InternalArity.resultModules) <$> runPipelineTermination (opts ^. internalArityInputFile) upToInternalArity
-  renderStdOut (Internal.ppOut globalOpts micro)

app/Commands/Dev/Internal/Arity/Options.hs

@@ -1,15 +0,0 @@
-module Commands.Dev.Internal.Arity.Options where
-
-import CommonOptions
-
-newtype InternalArityOptions = InternalArityOptions
-  { _internalArityInputFile :: AppPath File
-  }
-  deriving stock (Data)
-
-makeLenses ''InternalArityOptions
-
-parseInternalArity :: Parser InternalArityOptions
-parseInternalArity = do
-  _internalArityInputFile <- parseInputFile FileExtJuvix
-  pure InternalArityOptions {..}

app/Commands/Dev/Internal/Options.hs

@@ -1,6 +1,5 @@
 module Commands.Dev.Internal.Options where
 
-import Commands.Dev.Internal.Arity.Options
 import Commands.Dev.Internal.Pretty.Options
 import Commands.Dev.Internal.Reachability.Options
 import Commands.Dev.Internal.Typecheck.Options
@@ -9,7 +8,6 @@ import CommonOptions
 data InternalCommand
   = Pretty InternalPrettyOptions
   | TypeCheck InternalTypeOptions
-  | Arity InternalArityOptions
   | Reachability InternalReachabilityOptions
   deriving stock (Data)
 
@@ -18,14 +16,10 @@ parseInternalCommand =
   hsubparser $
     mconcat
       [ commandPretty,
-        commandArity,
         commandTypeCheck,
         commandReachability
       ]
   where
-    commandArity :: Mod CommandFields InternalCommand
-    commandArity = command "arity" arityInfo
-
     commandPretty :: Mod CommandFields InternalCommand
     commandPretty = command "pretty" prettyInfo
 
@@ -35,12 +29,6 @@ parseInternalCommand =
     commandReachability :: Mod CommandFields InternalCommand
     commandReachability = command "reachability" reachabilityInfo
 
-    arityInfo :: ParserInfo InternalCommand
-    arityInfo =
-      info
-        (Arity <$> parseInternalArity)
-        (progDesc "Translate a Juvix file to Internal and insert holes")
-
     prettyInfo :: ParserInfo InternalCommand
     prettyInfo =
       info

app/GlobalOptions.hs

@@ -20,8 +20,7 @@ data GlobalOptions = GlobalOptions
     _globalNoCoverage :: Bool,
     _globalNoStdlib :: Bool,
     _globalUnrollLimit :: Int,
-    _globalOffline :: Bool,
+    _globalOffline :: Bool
-    _globalNewTypecheckingAlgorithm :: Bool
   }
   deriving stock (Eq, Show)
 
@@ -61,8 +60,7 @@ defaultGlobalOptions =
       _globalNoCoverage = False,
       _globalNoStdlib = False,
       _globalUnrollLimit = defaultUnrollLimit,
-      _globalOffline = False,
+      _globalOffline = False
-      _globalNewTypecheckingAlgorithm = False
     }
 
 -- | Get a parser for global flags which can be hidden or not depending on
@@ -128,11 +126,6 @@ parseGlobalFlags = do
       ( long "show-name-ids"
           <> help "[DEV] Show the unique number of each identifier when pretty printing"
       )
-  _globalNewTypecheckingAlgorithm <-
-    switch
-      ( long "new-typechecker"
-          <> help "[DEV] Use the new experimental typechecker"
-      )
   return GlobalOptions {..}
 
 parseBuildDir :: Mod OptionFields (Prepath Dir) -> Parser (AppPath Dir)
@@ -165,8 +158,7 @@ entryPointFromGlobalOptions root mainFile opts = do
         _entryPointUnrollLimit = opts ^. globalUnrollLimit,
         _entryPointGenericOptions = project opts,
         _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
-        _entryPointOffline = opts ^. globalOffline,
+        _entryPointOffline = opts ^. globalOffline
-        _entryPointNewTypeCheckingAlgorithm = opts ^. globalNewTypecheckingAlgorithm
       }
   where
     optBuildDir :: Maybe (Prepath Dir)

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -18,7 +18,6 @@ import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Print
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoped
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -166,8 +165,7 @@ genJudocHtml JudocArgs {..} =
     cs :: Comments
     cs =
       _judocArgsCtx
-        ^. resultInternalArityResult
+        ^. resultInternalResult
-          . InternalArity.resultInternalResult
           . Internal.resultScoper
           . Scoped.comments
 
@@ -180,8 +178,7 @@ genJudocHtml JudocArgs {..} =
     mainMod :: Module 'Scoped 'ModuleTop
     mainMod =
       _judocArgsCtx
-        ^. InternalTyped.resultInternalArityResult
+        ^. InternalTyped.resultInternalResult
-          . InternalArity.resultInternalResult
           . Internal.resultScoper
           . Scoped.mainModule
 

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -11,10 +11,8 @@ import Juvix.Compiler.Internal.Data.InstanceInfo (instanceInfoResult, instanceTa
 import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Data.NameDependencyInfo
 import Juvix.Compiler.Internal.Data.TypedHole
-import Juvix.Compiler.Internal.Extra.Base
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty.Options
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types (Arity)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Data.CodeAnn
 import Juvix.Prelude
@@ -113,13 +111,6 @@ ppMutual l = do
       return (braces (line <> indent' b' <> line))
   return (kwMutual <+> defs')
 
-instance PrettyCode Arity where
-  ppCode = return . pretty
-
-instance PrettyCode ApplicationArg where
-  ppCode ApplicationArg {..} =
-    implicitDelim _appArgIsImplicit <$> ppCode _appArg
-
 instance PrettyCode LetClause where
   ppCode :: forall r. (Member (Reader Options) r) => LetClause -> Sem r (Doc Ann)
   ppCode = \case

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -503,19 +503,6 @@ goInductiveParameters ::
   Sem r [Internal.InductiveParameter]
 goInductiveParameters params@InductiveParameters {..} = do
   paramType' <- goRhs _inductiveParametersRhs
-  newAlgo <- asks (^. entryPointNewTypeCheckingAlgorithm)
-  case paramType' of
-    Internal.ExpressionUniverse {} -> return ()
-    Internal.ExpressionHole {} -> return ()
-    _ ->
-      unless newAlgo
-        . throw
-        $ ErrUnsupported
-          Unsupported
-            { _unsupportedMsg = "only type variables of small types are allowed",
-              _unsupportedLoc = getLoc params
-            }
-
   let goInductiveParameter :: S.Symbol -> Internal.InductiveParameter
       goInductiveParameter var =
         Internal.InductiveParameter

src/Juvix/Compiler/Internal/Translation/FromInternal.hs

@@ -1,12 +1,9 @@
 module Juvix.Compiler.Internal.Translation.FromInternal
   ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability,
-    arityChecking,
     typeChecking,
     typeCheckingNew,
     typeCheckExpression,
     typeCheckExpressionType,
-    arityCheckExpression,
-    arityCheckImport,
     typeCheckImport,
   )
 where
@@ -17,60 +14,14 @@ import Juvix.Compiler.Concrete.Data.Highlight.Input
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context as Internal
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context (InternalArityResult (InternalArityResult))
 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.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew qualified as New
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Data.Effect.NameIdGen
 import Juvix.Prelude hiding (fromEither)
 
-arityChecking ::
-  (Members '[Error JuvixError, NameIdGen] r) =>
-  InternalResult ->
-  Sem r ArityChecking.InternalArityResult
-arityChecking res@InternalResult {..} =
-  mapError (JuvixError @ArityChecking.ArityCheckerError) $ do
-    r <-
-      runReader table
-        . evalCacheEmpty ArityChecking.checkModuleIndexNoCache
-        $ mapM ArityChecking.checkModule _resultModules
-    return
-      ArityChecking.InternalArityResult
-        { _resultInternalResult = res,
-          _resultModules = r
-        }
-  where
-    table :: InfoTable
-    table = buildTable _resultModules
-
-arityCheckExpression ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
-  Expression ->
-  Sem r Expression
-arityCheckExpression exp = do
-  table <- extendedTableReplArtifacts exp
-  mapError (JuvixError @ArityChecking.ArityCheckerError)
-    . runReader table
-    . runNameIdGenArtifacts
-    $ ArityChecking.inferReplExpression exp
-
-arityCheckImport ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
-  Import ->
-  Sem r Import
-arityCheckImport i = do
-  artiTable <- gets (^. artifactInternalTypedTable)
-  let table = buildTable [i ^. importModule . moduleIxModule] <> artiTable
-  mapError (JuvixError @ArityChecking.ArityCheckerError)
-    . runReader table
-    . runNameIdGenArtifacts
-    . evalCacheEmpty ArityChecking.checkModuleIndexNoCache
-    $ ArityChecking.checkImport i
-
 typeCheckExpressionType ::
   forall r.
   (Members '[Error JuvixError, State Artifacts, Termination] r) =>
@@ -85,7 +36,8 @@ typeCheckExpressionType exp = do
     . runNameIdGenArtifacts
     . runReader table
     . ignoreOutput @Example
-    . withEmptyVars
+    . withEmptyLocalVars
+    . withEmptyInsertedArgsStack
     . mapError (JuvixError @TypeCheckerError)
     . runInferenceDef
     $ inferExpression Nothing exp
@@ -113,7 +65,7 @@ typeCheckImport i = do
     . runNameIdGenArtifacts
     . ignoreOutput @Example
     . runReader table
-    . withEmptyVars
+    . withEmptyLocalVars
     -- TODO Store cache in Artifacts and use it here
     . evalCacheEmpty checkModuleNoCache
     $ checkTable >> checkImport i
@@ -121,16 +73,16 @@ typeCheckImport i = do
 typeChecking ::
   forall r.
   (Members '[HighlightBuilder, Error JuvixError, Builtins, NameIdGen] r) =>
-  Sem (Termination ': r) ArityChecking.InternalArityResult ->
+  Sem (Termination ': r) Internal.InternalResult ->
   Sem r InternalTypedResult
 typeChecking a = do
   (termin, (res, table, (normalized, (idens, (funs, r))))) <- runTermination iniTerminationState $ do
     res <- a
     let table :: InfoTable
-        table = buildTable (res ^. ArityChecking.resultModules)
+        table = buildTable (res ^. Internal.resultModules)
 
         entryPoint :: EntryPoint
-        entryPoint = res ^. ArityChecking.internalArityResultEntryPoint
+        entryPoint = res ^. Internal.internalResultEntryPoint
     fmap (res,table,)
       . runOutputList
       . runReader entryPoint
@@ -139,10 +91,10 @@ typeChecking a = do
       . runReader table
       . mapError (JuvixError @TypeCheckerError)
       . evalCacheEmpty checkModuleNoCache
-      $ checkTable >> mapM checkModule (res ^. ArityChecking.resultModules)
+      $ checkTable >> mapM checkModule (res ^. Internal.resultModules)
   return
     InternalTypedResult
-      { _resultInternalArityResult = res,
+      { _resultInternalResult = res,
         _resultModules = r,
         _resultTermination = termin,
         _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],
@@ -171,17 +123,11 @@ typeCheckingNew a = do
       . runState (mempty :: FunctionsTable)
       . runReader table
       . mapError (JuvixError @TypeCheckerError)
-      . evalCacheEmpty New.checkModuleNoCache
+      . evalCacheEmpty checkModuleNoCache
-      $ checkTable >> mapM New.checkModule (res ^. Internal.resultModules)
+      $ checkTable >> mapM checkModule (res ^. Internal.resultModules)
-  let ariRes :: InternalArityResult
-      ariRes =
-        InternalArityResult
-          { _resultInternalResult = res,
-            _resultModules = res ^. Internal.resultModules
-          }
   return
     InternalTypedResult
-      { _resultInternalArityResult = ariRes,
+      { _resultInternalResult = res,
         _resultModules = r,
         _resultTermination = termin,
         _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking.hs

@@ -1,10 +0,0 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking
-  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error,
-  )
-where
-
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs

@@ -1,905 +0,0 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker
-  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error,
-  )
-where
-
-import Data.List.NonEmpty qualified as NonEmpty
-import Juvix.Compiler.Internal.Extra
-import Juvix.Compiler.Internal.Extra qualified as Internal
-import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error
-import Juvix.Data.Effect.NameIdGen
-import Juvix.Prelude hiding (fromEither)
-
-type MCache = Cache ModuleIndex Module
-
-checkModule ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) =>
-  Module ->
-  Sem r Module
-checkModule = cacheGet . ModuleIndex
-
-checkModuleIndexNoCache ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) =>
-  ModuleIndex ->
-  Sem r Module
-checkModuleIndexNoCache (ModuleIndex Module {..}) = do
-  _moduleBody' <- runReader @InsertedArgsStack mempty (checkModuleBody _moduleBody)
-  return
-    Module
-      { _moduleBody = _moduleBody',
-        ..
-      }
-
-checkModuleBody ::
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) =>
-  ModuleBody ->
-  Sem r ModuleBody
-checkModuleBody ModuleBody {..} = do
-  _moduleStatements' <- mapM checkMutualBlock _moduleStatements
-  _moduleImports' <- mapM checkImport _moduleImports
-  return
-    ModuleBody
-      { _moduleStatements = _moduleStatements',
-        _moduleImports = _moduleImports'
-      }
-
-checkModuleIndex ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) =>
-  ModuleIndex ->
-  Sem r ModuleIndex
-checkModuleIndex (ModuleIndex m) = ModuleIndex <$> checkModule m
-
-checkImport ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) =>
-  Import ->
-  Sem r Import
-checkImport = traverseOf importModule checkModuleIndex
-
-checkInductive :: forall r. (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveDef -> Sem r InductiveDef
-checkInductive d = do
-  let _inductiveName = d ^. inductiveName
-      _inductiveBuiltin = d ^. inductiveBuiltin
-      _inductivePositive = d ^. inductivePositive
-      _inductiveTrait = d ^. inductiveTrait
-      _inductivePragmas = d ^. inductivePragmas
-  (localVars, _inductiveParameters) <- checkParameters (d ^. inductiveParameters)
-  _inductiveExamples <- runReader localVars (mapM checkExample (d ^. inductiveExamples))
-  _inductiveConstructors <- runReader localVars (mapM checkConstructor (d ^. inductiveConstructors))
-  _inductiveType <- runReader localVars (checkType (d ^. inductiveType))
-  return InductiveDef {..}
-  where
-    checkParameters :: [InductiveParameter] -> Sem r (LocalVars, [InductiveParameter])
-    checkParameters = runState emptyLocalVars . mapM checkParam
-      where
-        checkParam :: InductiveParameter -> Sem (State LocalVars ': r) InductiveParameter
-        checkParam param = do
-          lv1 <- get @LocalVars
-          ty' <- runReader lv1 (checkType (param ^. inductiveParamType))
-          addArity (param ^. inductiveParamName) (typeArity ty')
-          return
-            InductiveParameter
-              { _inductiveParamName = param ^. inductiveParamName,
-                _inductiveParamType = ty'
-              }
-
-checkConstructor :: (Members '[Reader InsertedArgsStack, Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => ConstructorDef -> Sem r ConstructorDef
-checkConstructor c = do
-  let _inductiveConstructorName = c ^. inductiveConstructorName
-      _inductiveConstructorPragmas = c ^. inductiveConstructorPragmas
-  _inductiveConstructorType <- checkType (c ^. inductiveConstructorType)
-  _inductiveConstructorExamples <- mapM checkExample (c ^. inductiveConstructorExamples)
-  return ConstructorDef {..}
-
--- | check the arity of some ty : Type
-checkType :: (Members '[Reader InsertedArgsStack, Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression
-checkType = checkExpression ArityUnit
-
-checkAxiom :: (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => AxiomDef -> Sem r AxiomDef
-checkAxiom a = do
-  let _axiomName = a ^. axiomName
-      _axiomBuiltin = a ^. axiomBuiltin
-      _axiomPragmas = a ^. axiomPragmas
-  _axiomType <- withEmptyLocalVars (checkType (a ^. axiomType))
-  return AxiomDef {..}
-
-checkMutualStatement ::
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
-  MutualStatement ->
-  Sem r MutualStatement
-checkMutualStatement = \case
-  StatementFunction f -> StatementFunction <$> checkFunctionDef f
-  StatementInductive f -> StatementInductive <$> checkInductive f
-  StatementAxiom a -> StatementAxiom <$> checkAxiom a
-
-checkMutualBlockLet ::
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
-  MutualBlockLet ->
-  Sem r MutualBlockLet
-checkMutualBlockLet (MutualBlockLet funs) = MutualBlockLet <$> mapM checkFunctionDef funs
-
-checkMutualBlock ::
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
-  MutualBlock ->
-  Sem r MutualBlock
-checkMutualBlock (MutualBlock funs) = MutualBlock <$> mapM checkMutualStatement funs
-
-checkFunctionDef ::
-  forall r.
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
-  FunctionDef ->
-  Sem r FunctionDef
-checkFunctionDef FunctionDef {..} = do
-  let arity = typeArity _funDefType
-  _funDefType' <- withEmptyLocalVars (checkType _funDefType)
-  _funDefBody' <- checkFunctionBody arity _funDefBody
-  _funDefExamples' <- withEmptyLocalVars (mapM checkExample _funDefExamples)
-  let argTys = fst (unfoldFunType _funDefType')
-  _funDefArgsInfo' <- withEmptyLocalVars (checkArgsInfo _funDefArgsInfo argTys)
-  return
-    FunctionDef
-      { _funDefBody = _funDefBody',
-        _funDefExamples = _funDefExamples',
-        _funDefType = _funDefType',
-        _funDefArgsInfo = _funDefArgsInfo',
-        _funDefName,
-        _funDefTerminating,
-        _funDefInstance,
-        _funDefCoercion,
-        _funDefBuiltin,
-        _funDefPragmas
-      }
-
-checkArgsInfo ::
-  forall r.
-  (Members '[Reader InsertedArgsStack, NameIdGen, Reader LocalVars, Error ArityCheckerError, Reader InfoTable] r) =>
-  [ArgInfo] ->
-  [FunctionParameter] ->
-  Sem r [ArgInfo]
-checkArgsInfo defaults =
-  execOutputList
-    . go defaults
-  where
-    go :: [ArgInfo] -> [FunctionParameter] -> Sem (Output ArgInfo ': r) ()
-    go = \case
-      [] -> const (return ())
-      d : ds' -> \case
-        [] -> impossible
-        p : ps' -> do
-          let ari = typeArity (p ^. paramType)
-          dval <- case (d ^. argInfoDefault, p ^. paramImplicit) of
-            (Nothing, _) -> return Nothing
-            (Just val, Implicit) ->
-              Just <$> checkExpression ari val
-            (Just {}, _) -> impossible
-          output (set argInfoDefault dval d)
-          withLocalVarMaybe ari (p ^. paramName) (go ds' ps')
-
-checkFunctionBody ::
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
-  Arity ->
-  Expression ->
-  Sem r Expression
-checkFunctionBody ari body = do
-  case body of
-    ExpressionLambda {} ->
-      withEmptyLocalVars (checkExpression ari body)
-    _ -> do
-      hint <- guessArity body
-      (patterns', locals, bodyAri) <- checkLhs (getLoc body) hint ari []
-      body' <- runReader locals (checkExpression bodyAri body)
-      return $ case nonEmpty patterns' of
-        Nothing -> body'
-        Just lambdaPatterns' ->
-          ExpressionLambda
-            Lambda
-              { _lambdaType = Nothing,
-                _lambdaClauses =
-                  pure
-                    LambdaClause
-                      { _lambdaPatterns = lambdaPatterns',
-                        _lambdaBody = body'
-                      }
-              }
-
-simplelambda :: a
-simplelambda = error "simple lambda expressions are not supported by the arity checker"
-
-withLocalVarMaybe :: (Members '[Reader LocalVars] r) => Arity -> Maybe VarName -> Sem r a -> Sem r a
-withLocalVarMaybe ari mv = case mv of
-  Nothing -> id
-  Just v -> withLocalVar ari v
-
-withLocalVar :: (Members '[Reader LocalVars] r) => Arity -> VarName -> Sem r a -> Sem r a
-withLocalVar ari v = local (withArity v ari)
-
-withEmptyLocalVars :: Sem (Reader LocalVars ': r) a -> Sem r a
-withEmptyLocalVars = runReader emptyLocalVars
-
-arityLet :: (Members '[Reader InfoTable] r) => Let -> Sem r Arity
-arityLet l = guessArity (l ^. letExpression)
-
-inferReplExpression :: (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression
-inferReplExpression e = do
-  ari <- guessArity e
-  withEmptyLocalVars
-    . runReader @InsertedArgsStack mempty
-    $ checkExpression ari e
-
-guessArity ::
-  forall r.
-  (Members '[Reader InfoTable] r) =>
-  Expression ->
-  Sem r Arity
-guessArity = \case
-  ExpressionHole {} -> return ArityUnknown
-  ExpressionInstanceHole {} -> return ArityUnit
-  ExpressionFunction {} -> return ArityUnit
-  ExpressionLiteral {} -> return arityLiteral
-  ExpressionApplication a -> appHelper a
-  ExpressionIden i -> idenHelper i
-  ExpressionUniverse {} -> return arityUniverse
-  ExpressionSimpleLambda {} -> simplelambda
-  ExpressionLambda l -> return (arityLambda l)
-  ExpressionLet l -> arityLet l
-  ExpressionCase l -> arityCase l
-  where
-    idenHelper :: Iden -> Sem r Arity
-    idenHelper i = case i of
-      IdenVar {} -> return ArityUnknown
-      _ -> withEmptyLocalVars (idenArity i)
-
-    appHelper :: Application -> Sem r Arity
-    appHelper a = do
-      f' <- arif
-      let u = unfoldArity' f'
-      return $ case refine args (u ^. ufoldArityParams) of
-        Nothing -> ArityUnknown
-        Just a' -> foldArity (set ufoldArityParams a' u)
-      where
-        (f, args) = second (map (^. appArgIsImplicit) . toList) (unfoldApplication' a)
-
-        refine :: [IsImplicit] -> [ArityParameter] -> Maybe [ArityParameter]
-        refine as ps = case (as, ps) of
-          (Explicit : as', ArityParameter {_arityParameterImplicit = Explicit} : ps') -> refine as' ps'
-          (Implicit : as', ArityParameter {_arityParameterImplicit = Implicit} : ps') -> refine as' ps'
-          (ImplicitInstance : as', ArityParameter {_arityParameterImplicit = ImplicitInstance} : ps') -> refine as' ps'
-          (as'@(Explicit : _), ArityParameter {_arityParameterImplicit = Implicit} : ps') -> refine as' ps'
-          (as'@(Explicit : _), ArityParameter {_arityParameterImplicit = ImplicitInstance} : ps') -> refine as' ps'
-          (Implicit : _, ArityParameter {_arityParameterImplicit = Explicit} : _) -> Nothing
-          (ImplicitInstance : _, ArityParameter {_arityParameterImplicit = Explicit} : _) -> Nothing
-          (Implicit : _, ArityParameter {_arityParameterImplicit = ImplicitInstance} : _) -> Nothing
-          (ImplicitInstance : _, ArityParameter {_arityParameterImplicit = Implicit} : _) -> Nothing
-          ([], ps') -> Just ps'
-          (_ : _, []) -> Nothing
-
-        arif :: Sem r Arity
-        arif = guessArity f
-
-arityLiteral :: Arity
-arityLiteral = ArityUnit
-
-arityUniverse :: Arity
-arityUniverse = ArityUnit
-
--- | All branches should have the same arity. If they are all the same, we
--- return that, otherwise we return ArityUnknown. Probably something better can
--- be done.
-arityCase :: (Members '[Reader InfoTable] r) => Case -> Sem r Arity
-arityCase c = do
-  aris <- mapM (guessArity . (^. caseBranchExpression)) (c ^. caseBranches)
-  return
-    if
-        | allSame aris -> head aris
-        | otherwise -> ArityUnknown
-
--- | Lambdas can only have explicit arguments. Since we do not have dependent
--- types, it is ok to (partially) infer the arity of the lambda from the clause
--- with the most patterns.
-arityLambda :: Lambda -> Arity
-arityLambda l =
-  foldArity
-    UnfoldedArity
-      { _ufoldArityParams =
-          replicate
-            (maximum1 (fmap numPatterns (l ^. lambdaClauses)))
-            ( ArityParameter
-                { _arityParameterArity = ArityUnknown,
-                  _arityParameterImplicit = Explicit,
-                  _arityParameterInfo = emptyArgInfo
-                }
-            ),
-        _ufoldArityRest = ArityRestUnknown
-      }
-  where
-    numPatterns :: LambdaClause -> Int
-    numPatterns (LambdaClause ps _) = length ps
-
-checkLhs ::
-  forall r.
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
-  Interval ->
-  Arity ->
-  Arity ->
-  [PatternArg] ->
-  Sem r ([PatternArg], LocalVars, Arity)
-checkLhs loc guessedBody ariSignature pats = do
-  (locals, (pats', bodyAri)) <- runState emptyLocalVars (goLhs ariSignature pats)
-  return (pats', locals, bodyAri)
-  where
-    -- returns the expanded patterns and the rest of the Arity (the arity of the
-    -- body once all the patterns have been processed).
-    -- Does not insert holes greedily. I.e. implicit wildcards are only inserted
-    -- between explicit parameters already in the pattern.
-    goLhs :: Arity -> [PatternArg] -> Sem (State LocalVars ': r) ([PatternArg], Arity)
-    goLhs a = \case
-      [] -> case tailHelper a of
-        Nothing -> return ([], a)
-        Just tailUnderscores -> do
-          let n = length tailUnderscores
-              a' = foldArity (over ufoldArityParams (drop n) (unfoldArity' a))
-          wildcards <- mapM genWildcard' tailUnderscores
-          return (wildcards, a')
-      lhs@(p : ps) -> case a of
-        ArityUnit ->
-          throw
-            ( ErrLhsTooManyPatterns
-                LhsTooManyPatterns
-                  { _lhsTooManyPatternsRemaining = p :| ps
-                  }
-            )
-        ArityUnknown -> do
-          p' <- checkPattern ArityUnknown p
-          first (p' :) <$> goLhs ArityUnknown ps
-        ArityFunction (FunctionArity l r) ->
-          case (p ^. patternArgIsImplicit, l ^. arityParameterImplicit) of
-            (Implicit, Implicit {}) -> do
-              b' <- checkPattern (arityParameter l) p
-              first (b' :) <$> goLhs r ps
-            (Implicit, Explicit {}) ->
-              throw
-                ( ErrWrongPatternIsImplicit
-                    WrongPatternIsImplicit
-                      { _wrongPatternIsImplicitExpected = Explicit,
-                        _wrongPatternIsImplicitActual = p
-                      }
-                )
-            (Implicit, ImplicitInstance {}) ->
-              throw
-                ( ErrWrongPatternIsImplicit
-                    WrongPatternIsImplicit
-                      { _wrongPatternIsImplicitExpected = ImplicitInstance,
-                        _wrongPatternIsImplicitActual = p
-                      }
-                )
-            (ImplicitInstance, ImplicitInstance) -> do
-              b' <- checkPattern (arityParameter l) p
-              first (b' :) <$> goLhs r ps
-            (ImplicitInstance, Explicit {}) ->
-              throw
-                ( ErrWrongPatternIsImplicit
-                    WrongPatternIsImplicit
-                      { _wrongPatternIsImplicitExpected = Explicit,
-                        _wrongPatternIsImplicitActual = p
-                      }
-                )
-            (ImplicitInstance, Implicit {}) -> do
-              wildcard <- genWildcard' Implicit
-              first (wildcard :) <$> goLhs r lhs
-            (Explicit, Implicit {}) -> do
-              wildcard <- genWildcard' Implicit
-              first (wildcard :) <$> goLhs r lhs
-            (Explicit, ImplicitInstance) -> do
-              wildcard <- genWildcard' ImplicitInstance
-              first (wildcard :) <$> goLhs r lhs
-            (Explicit, Explicit) -> do
-              p' <- checkPattern (l ^. arityParameterArity) p
-              first (p' :) <$> goLhs r ps
-      where
-        genWildcard' :: forall r'. (Members '[NameIdGen] r') => IsImplicit -> Sem r' PatternArg
-        genWildcard' = genWildcard loc
-
-    -- This is an heuristic and it can have an undesired result.
-    -- Sometimes the outcome may even be confusing.
-    tailHelper :: Arity -> Maybe [IsImplicit]
-    tailHelper a
-      | 0 < pref = Just pref'
-      | otherwise = Nothing
-      where
-        pref' :: [IsImplicit]
-        pref' = map paramToImplicit (take pref (unfoldArity a))
-        pref :: Int
-        pref = aI - targetI
-        preceedingImplicits :: Arity -> Int
-        preceedingImplicits = length . takeWhile (isImplicitOrInstance . (^. arityParameterImplicit)) . unfoldArity
-        aI :: Int
-        aI = preceedingImplicits a
-        targetI :: Int
-        targetI = preceedingImplicits guessedBody
-        paramToImplicit :: ArityParameter -> IsImplicit
-        paramToImplicit = (^. arityParameterImplicit)
-
-checkPattern ::
-  forall r.
-  (Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars, NameIdGen] r) =>
-  Arity ->
-  PatternArg ->
-  Sem r PatternArg
-checkPattern ari = traverseOf (patternArgName . each) nameAri >=> traverseOf patternArgPattern patternAri
-  where
-    nameAri :: VarName -> Sem r VarName
-    nameAri n = addArity n ari $> n
-
-    patternAri :: Pattern -> Sem r Pattern
-    patternAri = \case
-      PatternVariable v -> addArity v ari $> PatternVariable v
-      PatternWildcardConstructor v -> PatternConstructorApp <$> checkWildcardConstructor v
-      PatternConstructorApp c -> case ari of
-        ArityUnit -> PatternConstructorApp <$> checkConstructorApp c
-        ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c
-        ArityFunction {} ->
-          throw
-            ( ErrPatternFunction
-                PatternFunction
-                  { _patternFunction = c
-                  }
-            )
-
-checkWildcardConstructor ::
-  forall r.
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, State LocalVars] r) =>
-  WildcardConstructor ->
-  Sem r ConstructorApp
-checkWildcardConstructor w = do
-  let c = w ^. wildcardConstructor
-  numArgs <- length . constructorArgs . (^. constructorInfoType) <$> lookupConstructor c
-  holeArgs <- replicateM numArgs (genWildcard (getLoc w) Explicit)
-  return
-    ConstructorApp
-      { _constrAppConstructor = c,
-        _constrAppParameters = holeArgs,
-        _constrAppType = Nothing
-      }
-
-checkConstructorApp ::
-  forall r.
-  (Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars, NameIdGen] r) =>
-  ConstructorApp ->
-  Sem r ConstructorApp
-checkConstructorApp ca = do
-  let c = ca ^. constrAppConstructor
-  args <- constructorArgs . (^. constructorInfoType) <$> lookupConstructor c
-  let arities = map typeArity args
-      n = length arities
-      ps = ca ^. constrAppParameters
-      lps = length ps
-  when
-    (n /= lps)
-    ( throw
-        ( ErrWrongConstructorAppLength
-            WrongConstructorAppLength
-              { _wrongConstructorAppLength = ca,
-                _wrongConstructorAppLengthExpected = n
-              }
-        )
-    )
-  ps' <- zipWithM checkPattern arities ps
-  return (ConstructorApp c ps' Nothing)
-
-checkCase ::
-  forall r.
-  (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
-  Arity ->
-  Case ->
-  Sem r Case
-checkCase ari l = do
-  _caseBranches <- mapM checkCaseBranch (l ^. caseBranches)
-  _caseExpression <- checkExpression ArityUnit (l ^. caseExpression)
-  let _caseParens = l ^. caseParens
-      _caseExpressionType :: Maybe Expression = Nothing
-      _caseExpressionWholeType :: Maybe Expression = Nothing
-  return Case {..}
-  where
-    checkCaseBranch :: CaseBranch -> Sem r CaseBranch
-    checkCaseBranch = traverseOf caseBranchExpression (checkExpression ari)
-
-checkLet ::
-  forall r.
-  (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
-  Arity ->
-  Let ->
-  Sem r Let
-checkLet ari l = do
-  _letClauses <- mapM checkLetClause (l ^. letClauses)
-  _letExpression <- checkExpression ari (l ^. letExpression)
-  return Let {..}
-  where
-    checkLetClause :: LetClause -> Sem r LetClause
-    checkLetClause = \case
-      LetFunDef f -> LetFunDef <$> checkFunctionDef f
-      LetMutualBlock f -> LetMutualBlock <$> checkMutualBlockLet f
-
-checkLambda ::
-  forall r.
-  (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
-  Arity ->
-  Lambda ->
-  Sem r Lambda
-checkLambda ari l = do
-  let _lambdaType = l ^. lambdaType
-  _lambdaClauses <- mapM checkLambdaClause (l ^. lambdaClauses)
-  return Lambda {..}
-  where
-    checkLambdaClause ::
-      LambdaClause ->
-      Sem r LambdaClause
-    checkLambdaClause cl = do
-      hint <- guessArity (cl ^. lambdaBody)
-      (patterns', locals, bodyAri) <- checkLhs loc hint ari (toList (cl ^. lambdaPatterns))
-      body' <- runReader locals (checkExpression bodyAri (cl ^. lambdaBody))
-      return
-        LambdaClause
-          { _lambdaPatterns = nonEmpty' patterns',
-            _lambdaBody = body'
-          }
-      where
-        loc = getLoc cl
-
-idenArity :: (Members '[Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r Arity
-idenArity = \case
-  IdenVar v -> getLocalArity v
-  IdenInductive i -> typeArity <$> lookupInductiveType i
-  IdenFunction f -> do
-    fun <- (^. functionInfoDef) <$> lookupFunction f
-    let ari = typeArity (fun ^. funDefType)
-        defaults = fun ^. funDefArgsInfo
-    return (addArgsInfo defaults ari)
-  IdenConstructor c -> typeArity <$> lookupConstructorType c
-  IdenAxiom a -> typeArity . (^. axiomInfoDef . axiomType) <$> lookupAxiom a
-
-addArgsInfo :: [ArgInfo] -> Arity -> Arity
-addArgsInfo = unfoldingArity . helper
-  where
-    helper :: [ArgInfo] -> UnfoldedArity -> UnfoldedArity
-    helper = over ufoldArityParams . go
-
-    go :: [ArgInfo] -> [ArityParameter] -> [ArityParameter]
-    go infos params = case infos of
-      [] -> params
-      info : infos' -> case params of
-        [] -> impossible
-        para : params' ->
-          set arityParameterInfo info para : go infos' params'
-
--- | let x be some expression of type T. The argument of this function is T and it returns
--- the arity of x. In other words, given (T : Type), it returns the arity of the elements of T.
-typeArity :: Expression -> Arity
-typeArity = go
-  where
-    go :: Expression -> Arity
-    go = \case
-      ExpressionIden i -> goIden i
-      ExpressionApplication a -> goApplication a
-      ExpressionLiteral {} -> ArityUnknown
-      ExpressionFunction f -> ArityFunction (goFun f)
-      ExpressionHole {} -> ArityUnknown
-      ExpressionInstanceHole {} -> ArityUnit
-      ExpressionLambda {} -> ArityUnknown
-      ExpressionCase {} -> ArityUnknown
-      ExpressionUniverse {} -> ArityUnit
-      ExpressionSimpleLambda {} -> simplelambda
-      ExpressionLet l -> goLet l
-
-    goApplication :: Application -> Arity
-    goApplication a = case lhs of
-      ExpressionIden IdenInductive {} -> ArityUnit
-      _ -> ArityUnknown
-      where
-        lhs :: Expression
-        lhs = fst (unfoldApplication a)
-
-    goLet :: Let -> Arity
-    goLet l = typeArity (l ^. letExpression)
-
-    goIden :: Iden -> Arity
-    goIden = \case
-      IdenVar {} -> ArityUnknown
-      IdenInductive {} -> ArityUnit
-      IdenFunction {} -> ArityUnknown -- we need normalization to determine the arity
-      IdenConstructor {} -> ArityUnknown -- will be a type error
-      IdenAxiom {} -> ArityUnknown
-
-    goParam :: FunctionParameter -> ArityParameter
-    goParam FunctionParameter {..} =
-      ArityParameter
-        { _arityParameterArity = case _paramImplicit of
-            Explicit -> go _paramType
-            Implicit -> go _paramType
-            ImplicitInstance -> ArityUnit,
-          _arityParameterImplicit = _paramImplicit,
-          _arityParameterInfo = emptyArgInfo
-        }
-
-    goFun :: Function -> FunctionArity
-    goFun (Function l r) =
-      let l' = goParam l
-          r' = go r
-       in FunctionArity
-            { _functionArityLeft = l',
-              _functionArityRight = r'
-            }
-
-checkExample ::
-  forall r.
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) =>
-  Example ->
-  Sem r Example
-checkExample = traverseOf exampleExpression (checkExpression ArityUnknown)
-
-checkExpression ::
-  forall r.
-  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) =>
-  Arity ->
-  Expression ->
-  Sem r Expression
-checkExpression hintArity expr = case expr of
-  ExpressionIden {} -> goApp expr []
-  ExpressionApplication a -> uncurry goApp $ second toList (unfoldApplication' a)
-  ExpressionLiteral {} -> appHelper expr []
-  ExpressionFunction f -> ExpressionFunction <$> goFunction f
-  ExpressionUniverse {} -> return expr
-  ExpressionHole {} -> return expr
-  ExpressionInstanceHole {} -> return expr
-  ExpressionSimpleLambda {} -> simplelambda
-  ExpressionLambda l -> ExpressionLambda <$> checkLambda hintArity l
-  ExpressionLet l -> ExpressionLet <$> checkLet hintArity l
-  ExpressionCase l -> ExpressionCase <$> checkCase hintArity l
-  where
-    goFunction :: Function -> Sem r Function
-    goFunction (Function l r) = do
-      l' <- goFunctionParameter l
-      let ari = typeArity (l' ^. paramType)
-      r' <- maybe id (withLocalVar ari) (l ^. paramName) (checkType r)
-      return (Function l' r')
-      where
-        goFunctionParameter :: FunctionParameter -> Sem r FunctionParameter
-        goFunctionParameter p = do
-          let _paramName = p ^. paramName
-              _paramImplicit = p ^. paramImplicit
-          _paramType <- checkType (p ^. paramType)
-          return FunctionParameter {..}
-
-    goApp :: Expression -> [ApplicationArg] -> Sem r Expression
-    goApp f args = do
-      case f of
-        ExpressionIden (IdenAxiom n) -> do
-          blt <- getAxiomBuiltinInfo n
-          case blt of
-            Just BuiltinIOSequence -> goBuiltinApp n 0 2 f args
-            Just BuiltinTrace -> goBuiltinApp n 1 1 f args
-            _ -> appHelper f args
-        ExpressionIden (IdenFunction n) -> do
-          blt <- getFunctionBuiltinInfo n
-          case blt of
-            Just BuiltinBoolIf -> goBuiltinApp n 1 3 f args
-            Just BuiltinBoolOr -> goBuiltinApp n 0 2 f args
-            Just BuiltinBoolAnd -> goBuiltinApp n 0 2 f args
-            Just BuiltinSeq -> goBuiltinApp n 2 2 f args
-            _ -> appHelper f args
-        _ -> appHelper f args
-
-    goBuiltinApp :: Name -> Int -> Int -> Expression -> [ApplicationArg] -> Sem r Expression
-    goBuiltinApp n implArgsNum argsNum f args = do
-      args' <- goImplArgs implArgsNum args
-      if
-          | length args' >= argsNum -> appHelper f args
-          | otherwise ->
-              throw $
-                ErrBuiltinNotFullyApplied
-                  BuiltinNotFullyApplied
-                    { _builtinNotFullyAppliedName = n,
-                      _builtinNotFullyAplliedExpectedArgsNum = argsNum
-                    }
-      where
-        goImplArgs :: Int -> [ApplicationArg] -> Sem r [ApplicationArg]
-        goImplArgs 0 as = return as
-        goImplArgs k ((ApplicationArg Implicit _) : as) = goImplArgs (k - 1) as
-        goImplArgs _ as = return as
-
-    appHelper :: Expression -> [ApplicationArg] -> Sem r Expression
-    appHelper fun0 args = do
-      (fun', args') :: (Expression, [ApplicationArg]) <- case fun0 of
-        ExpressionHole {} -> (fun0,) <$> mapM (traverseOf appArg (checkExpression ArityUnknown)) args
-        ExpressionInstanceHole {} -> (fun0,) <$> mapM (traverseOf appArg (checkExpression ArityUnknown)) args
-        ExpressionIden i -> (,[]) <$> goAppLeftIden i
-        ExpressionLiteral l -> (fun0,) <$> helper (getLoc l) arityLiteral
-        ExpressionUniverse l -> (fun0,) <$> helper (getLoc l) arityUniverse
-        ExpressionLambda l -> do
-          l' <- checkLambda ArityUnknown l
-          (ExpressionLambda l',) <$> helper (getLoc l') (arityLambda l')
-        ExpressionSimpleLambda {} -> simplelambda
-        ExpressionCase l -> do
-          l' <- checkCase ArityUnknown l
-          (ExpressionCase l',) <$> (arityCase l' >>= helper (getLoc l'))
-        ExpressionLet l -> do
-          l' <- checkLet ArityUnknown l
-          (ExpressionLet l',) <$> (arityLet l' >>= helper (getLoc l'))
-        ExpressionFunction f ->
-          throw
-            ( ErrFunctionApplied
-                FunctionApplied
-                  { _functionAppliedFunction = f,
-                    _functionAppliedArguments = args
-                  }
-            )
-        ExpressionApplication {} -> impossible
-      return (foldApplication fun' args')
-      where
-        goAppLeftIden :: Iden -> Sem r Expression
-        goAppLeftIden i = case i of
-          IdenFunction f -> do
-            infos <- (^. functionInfoDef . funDefArgsInfo) <$> lookupFunction f
-            let hasADefault = has (each . argInfoDefault . _Just) infos
-            if
-                | hasADefault -> goAppLeftIdenWithDefaults i
-                | otherwise -> noDefaults
-          _ -> noDefaults
-          where
-            noDefaults :: Sem r Expression
-            noDefaults = do
-              args' :: [ApplicationArg] <- map (^. insertedArg) <$> (idenArity i >>= helperDefaultArgs (getLoc i))
-              return (foldApplication fun0 args')
-
-        goAppLeftIdenWithDefaults :: Iden -> Sem r Expression
-        goAppLeftIdenWithDefaults i = do
-          namedArgs :: [InsertedArg] <- idenArity i >>= helperDefaultArgs (getLoc i)
-          case nonEmpty namedArgs of
-            Nothing -> return (toExpression i)
-            Just args' -> do
-              let mkClause :: InsertedArg -> Sem r Internal.PreLetStatement
-                  mkClause InsertedArg {..} = do
-                    -- TODO put actual type instead of hole?
-                    let arg = _insertedArg
-                        nm = _insertedArgName
-                    ty <- mkFreshHole (getLoc arg)
-                    return (Internal.PreLetFunctionDef (Internal.simpleFunDef nm ty (arg ^. appArg)))
-                  mkAppArg :: InsertedArg -> ApplicationArg
-                  mkAppArg InsertedArg {..} =
-                    ApplicationArg
-                      { _appArgIsImplicit = _insertedArg ^. appArgIsImplicit,
-                        _appArg = toExpression _insertedArgName
-                      }
-              clauses :: NonEmpty Internal.LetClause <- nonEmpty' . Internal.mkLetClauses <$> mapM mkClause args'
-              let app = foldApplication (toExpression fun0) (map mkAppArg namedArgs)
-              letexpr <-
-                Internal.substitutionE (renameKind KNameFunction (map (^. insertedArgName) namedArgs)) $
-                  ExpressionLet
-                    Let
-                      { _letClauses = clauses,
-                        _letExpression = app
-                      }
-              Internal.clone letexpr
-
-        helper :: Interval -> Arity -> Sem r [ApplicationArg]
-        helper i ari = map (^. insertedArg) <$> helperDefaultArgs i ari
-
-        helperDefaultArgs :: Interval -> Arity -> Sem r [InsertedArg]
-        helperDefaultArgs i ari = do
-          let argsAris :: [Arity]
-              argsAris = map arityParameter (unfoldArity ari)
-          argsWithHoles :: [InsertedArg] <- addHoles i hintArity ari args
-          let argsWithAris :: [(InsertedArg, Arity)]
-              argsWithAris = zip argsWithHoles (argsAris ++ repeat ArityUnknown)
-          forM argsWithAris $ \(ia, argAri) -> do
-            checkDefaultArgCycle ia
-            let adjustCtx
-                  | ia ^. insertedArgDefault = over insertedArgsStack ((ia ^. insertedArgName) :)
-                  | otherwise = id
-            local adjustCtx (traverseOf (insertedArg . appArg) (checkExpression argAri) ia)
-          where
-            checkDefaultArgCycle :: InsertedArg -> Sem r ()
-            checkDefaultArgCycle ia = do
-              st <- asks (^. insertedArgsStack)
-              case span (/= (ia ^. insertedArgName)) st of
-                (_, []) -> return ()
-                (c, _) ->
-                  let cyc = NonEmpty.reverse (ia ^. insertedArgName :| c)
-                   in throw (ErrDefaultArgCycle (DefaultArgCycle cyc))
-
-        addHoles ::
-          Interval ->
-          Arity ->
-          Arity ->
-          [ApplicationArg] ->
-          Sem r [InsertedArg]
-        addHoles loc hint ari0 = evalState 0 . execOutputList . go ari0
-          where
-            go ::
-              Arity ->
-              [ApplicationArg] ->
-              Sem (Output InsertedArg ': State Int ': r) ()
-            go ari goargs = do
-              let emitNoName :: Bool -> ApplicationArg -> Sem (Output InsertedArg ': State Int ': r) ()
-                  emitNoName isDef x = do
-                    let l = getLoc x
-                    v <- freshFunVar l "gen_helper"
-                    emit isDef v x
-                  emitWithParameter :: Bool -> ArityParameter -> ApplicationArg -> Sem (Output InsertedArg ': State Int ': r) ()
-                  emitWithParameter isDef p = maybe (emitNoName isDef) (emit isDef) (p ^. arityParameterName)
-                  emitInstanceHole :: Sem (Output InsertedArg ': State Int ': r) ()
-                  emitInstanceHole = do
-                    h <- newHoleInstance loc
-                    emitNoName False (ApplicationArg ImplicitInstance (ExpressionInstanceHole h))
-                  emitImplicitHole :: ArityParameter -> Sem (Output InsertedArg ': State Int ': r) ()
-                  emitImplicitHole p = do
-                    (isDef, h) <- newHoleImplicit p loc
-                    emitWithParameter isDef p (ApplicationArg Implicit h)
-                  emit :: Bool -> Name -> ApplicationArg -> Sem (Output InsertedArg ': State Int ': r) ()
-                  emit isDef n x = do
-                    output
-                      InsertedArg
-                        { _insertedArg = x,
-                          _insertedArgDefault = isDef,
-                          _insertedArgName = n
-                        }
-                    modify' @Int succ
-              case (ari, goargs) of
-                (ArityFunction (FunctionArity (p@ArityParameter {_arityParameterImplicit = Implicit}) r), (ApplicationArg Implicit e) : rest) -> do
-                  emitWithParameter False p (ApplicationArg Implicit e)
-                  go r rest
-                (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = ImplicitInstance}) r), (ApplicationArg ImplicitInstance e) : rest) -> do
-                  emitNoName False (ApplicationArg ImplicitInstance e)
-                  go r rest
-                (ArityFunction (FunctionArity (p@ArityParameter {_arityParameterImplicit = Explicit}) r), (ApplicationArg Explicit e) : rest) -> do
-                  emitWithParameter False p (ApplicationArg Explicit e)
-                  go r rest
-                (ArityFunction (FunctionArity impl _), [])
-                  -- When there are no remaining arguments and the expected arity of the
-                  -- expression matches the current arity we should *not* insert a hole.
-                  | arityParameterImplicitOrInstance impl
-                      && ari == hint ->
-                      return ()
-                (ArityFunction (FunctionArity (p@ArityParameter {_arityParameterImplicit = Implicit}) r), _) -> do
-                  -- h <- newHoleImplicit p loc
-                  -- emitWithParameter p (ApplicationArg Implicit h)
-                  emitImplicitHole p
-                  go r goargs
-                (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = ImplicitInstance}) r), _) -> do
-                  emitInstanceHole
-                  go r goargs
-                (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = Explicit}) _), (ApplicationArg _ _) : _) -> do
-                  idx <- get @Int
-                  throw
-                    ( ErrExpectedExplicitArgument
-                        ExpectedExplicitArgument
-                          { _expectedExplicitArgumentApp = (fun0, args),
-                            _expectedExplicitArgumentIx = idx
-                          }
-                    )
-                (ArityUnit, []) -> return ()
-                (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = Explicit}) _), []) -> return ()
-                (ArityUnit, _ : _) ->
-                  throw
-                    ( ErrTooManyArguments
-                        TooManyArguments
-                          { _tooManyArgumentsApp = (fun0, args),
-                            _tooManyArgumentsUnexpected = length goargs
-                          }
-                    )
-                (ArityUnknown, []) -> return ()
-                (ArityUnknown, p : ps) -> do
-                  emitNoName False p
-                  go ArityUnknown ps
-
-newHoleImplicit :: (Member NameIdGen r) => ArityParameter -> Interval -> Sem r (Bool, Expression)
-newHoleImplicit i loc = case i ^. arityParameterInfo . argInfoDefault of
-  Nothing -> (False,) . ExpressionHole . mkHole loc <$> freshNameId
-  Just e -> do
-    -- TODO update location
-    return (True, e)
-
-newHoleInstance :: (Member NameIdGen r) => Interval -> Sem r InstanceHole
-newHoleInstance loc = mkInstanceHole loc <$> freshNameId

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data.hs

@@ -1,10 +0,0 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data
-  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context,
-  )
-where
-
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs

@@ -1,23 +0,0 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context where
-
-import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Scoped
-import Juvix.Compiler.Internal.Language
-import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal
-import Juvix.Compiler.Pipeline.EntryPoint qualified as E
-import Juvix.Prelude
-
-data InternalArityResult = InternalArityResult
-  { _resultInternalResult :: Internal.InternalResult,
-    _resultModules :: NonEmpty Module
-  }
-
-makeLenses ''InternalArityResult
-
-mainModule :: Lens' InternalArityResult Module
-mainModule = resultModules . _head1
-
-internalArityResultEntryPoint :: Lens' InternalArityResult E.EntryPoint
-internalArityResultEntryPoint = resultInternalResult . Internal.internalResultEntryPoint
-
-internalArityResultScoped :: Lens' InternalArityResult Scoped.ScoperResult
-internalArityResultScoped = resultInternalResult . Internal.resultScoper

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/LocalVars.hs

@@ -1,25 +0,0 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars where
-
-import Data.HashMap.Strict qualified as HashMap
-import Juvix.Compiler.Internal.Language
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types
-import Juvix.Prelude
-
-newtype LocalVars = LocalVars
-  { _localArities :: HashMap VarName Arity
-  }
-  deriving newtype (Semigroup, Monoid)
-
-makeLenses ''LocalVars
-
-addArity :: (Member (State LocalVars) r) => VarName -> Arity -> Sem r ()
-addArity v t = modify (withArity v t)
-
-withArity :: VarName -> Arity -> LocalVars -> LocalVars
-withArity v t = over localArities (HashMap.insert v t)
-
-getLocalArity :: (Member (Reader LocalVars) r) => VarName -> Sem r Arity
-getLocalArity v = fromMaybe ArityUnknown <$> asks (^. localArities . at v)
-
-emptyLocalVars :: LocalVars
-emptyLocalVars = mempty

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs

@@ -1,149 +0,0 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types where
-
-import Juvix.Compiler.Internal.Extra.Base
-import Juvix.Compiler.Internal.Language
-import Juvix.Prelude
-import Juvix.Prelude.Pretty
-
--- | Used to detect of cycles of default arguments in the arity checker.
-newtype InsertedArgsStack = InsertedArgsStack
-  { _insertedArgsStack :: [Name]
-  }
-  deriving newtype (Monoid, Semigroup)
-
--- | Helper type used during insertion of default arguments in the arity
--- checker.
-data InsertedArg = InsertedArg
-  { _insertedArgName :: Name,
-    _insertedArg :: ApplicationArg,
-    -- | True if this corresponds to an automatically inserted default argument.
-    -- False if it is an inserted hole or an argument present in the source code.
-    _insertedArgDefault :: Bool
-  }
-
-data Arity
-  = ArityUnit
-  | ArityFunction FunctionArity
-  | ArityUnknown
-  deriving stock (Eq)
-
-data FunctionArity = FunctionArity
-  { _functionArityLeft :: ArityParameter,
-    _functionArityRight :: Arity
-  }
-  deriving stock (Eq)
-
-data ArityRest
-  = ArityRestUnit
-  | ArityRestUnknown
-  deriving stock (Eq)
-
-data UnfoldedArity = UnfoldedArity
-  { _ufoldArityParams :: [ArityParameter],
-    _ufoldArityRest :: ArityRest
-  }
-  deriving stock (Eq)
-
-data ArityParameter = ArityParameter
-  { _arityParameterArity :: Arity,
-    _arityParameterImplicit :: IsImplicit,
-    _arityParameterInfo :: ArgInfo
-  }
-
-instance Eq ArityParameter where
-  (ArityParameter ari impl _info) == (ArityParameter ari' impl' _info') =
-    (ari, impl) == (ari', impl')
-
-makeLenses ''UnfoldedArity
-makeLenses ''InsertedArg
-makeLenses ''ArityParameter
-makeLenses ''InsertedArgsStack
-
-arityParameterName :: Lens' ArityParameter (Maybe Name)
-arityParameterName = arityParameterInfo . argInfoName
-
-unfoldingArity :: (UnfoldedArity -> UnfoldedArity) -> Arity -> Arity
-unfoldingArity f = foldArity . f . unfoldArity'
-
-arityParameter :: ArityParameter -> Arity
-arityParameter = (^. arityParameterArity)
-
-arityParameterImplicitOrInstance :: ArityParameter -> Bool
-arityParameterImplicitOrInstance a = case a ^. arityParameterImplicit of
-  Explicit {} -> False
-  Implicit {} -> True
-  ImplicitInstance -> True
-
-arityCommonPrefix :: Arity -> Arity -> [ArityParameter]
-arityCommonPrefix p1 p2 = commonPrefix u1 u2
-  where
-    u1 = unfoldArity p1
-    u2 = unfoldArity p2
-
-unfoldArity' :: Arity -> UnfoldedArity
-unfoldArity' = \case
-  ArityUnit ->
-    UnfoldedArity
-      { _ufoldArityParams = [],
-        _ufoldArityRest = ArityRestUnit
-      }
-  ArityUnknown ->
-    UnfoldedArity
-      { _ufoldArityParams = [],
-        _ufoldArityRest = ArityRestUnknown
-      }
-  ArityFunction (FunctionArity l r) ->
-    over ufoldArityParams (l :) (unfoldArity' r)
-
-unfoldArity :: Arity -> [ArityParameter]
-unfoldArity = (^. ufoldArityParams) . unfoldArity'
-
-foldArity :: UnfoldedArity -> Arity
-foldArity UnfoldedArity {..} = go _ufoldArityParams
-  where
-    go :: [ArityParameter] -> Arity
-    go = \case
-      [] -> case _ufoldArityRest of
-        ArityRestUnit -> ArityUnit
-        ArityRestUnknown -> ArityUnknown
-      a : as -> ArityFunction (FunctionArity a (go as))
-
-instance HasAtomicity FunctionArity where
-  atomicity = const (Aggregate funFixity)
-
-instance HasAtomicity Arity where
-  atomicity = \case
-    ArityUnit -> Atom
-    ArityUnknown -> Atom
-    ArityFunction f -> atomicity f
-
-instance Pretty ArityParameter where
-  pretty a =
-    let ari = arityParameter a
-     in case a ^. arityParameterImplicit of
-          Implicit -> "{" <> pretty ari <> "}"
-          ImplicitInstance -> "{{𝟙}}"
-          Explicit -> pretty ari
-
-instance HasAtomicity ArityParameter where
-  atomicity a = case a ^. arityParameterImplicit of
-    Explicit -> atomicity (a ^. arityParameterArity)
-    Implicit {} -> Atom
-    ImplicitInstance -> Atom
-
-instance Pretty FunctionArity where
-  pretty (FunctionArity l r) =
-    ppSide False l
-      <> " → "
-      <> ppSide True r
-    where
-      ppSide :: (HasAtomicity a, Pretty a) => Bool -> a -> Doc ann
-      ppSide isright lr = parensCond (atomParens (const isright) (atomicity lr) funFixity) (pretty lr)
-      parensCond :: Bool -> Doc a -> Doc a
-      parensCond t d = if t then parens d else d
-
-instance Pretty Arity where
-  pretty = \case
-    ArityUnit -> "𝟙"
-    ArityUnknown -> "?"
-    ArityFunction f -> pretty f

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs

@@ -3,7 +3,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability (f
 import Juvix.Compiler.Internal.Data.NameDependencyInfo
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as Arity
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Prelude
@@ -16,7 +15,7 @@ filterUnreachable r = do
     KeepAll -> return r
     FilterUnreachable -> return (set Typed.resultModules modules' r)
   where
-    depInfo = r ^. Typed.resultInternalArityResult . Arity.resultInternalResult . resultDepInfo
+    depInfo = r ^. Typed.resultInternalResult . resultDepInfo
     modules = r ^. Typed.resultModules
     modules' =
       run

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs

@@ -1,12 +1,12 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking
-  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Checker,
+  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew,
     module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference,
     module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable,
     module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context,
   )
 where
 
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Checker
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew
 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.Data.Inference

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -166,9 +166,6 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
                   }
             )
 
-withEmptyVars :: Sem (Reader LocalVars ': r) a -> Sem r a
-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, Termination] r) =>
@@ -332,7 +329,7 @@ checkExample ::
   Example ->
   Sem r Example
 checkExample e = do
-  e' <- withEmptyVars (runInferenceDef (traverseOf exampleExpression (fmap (^. typedExpression) . inferExpression Nothing >=> strongNormalize) e))
+  e' <- withEmptyLocalVars (runInferenceDef (traverseOf exampleExpression (fmap (^. typedExpression) . inferExpression Nothing >=> strongNormalize) e))
   output e'
   return e'
 

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -4,6 +4,10 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Ch
     checkTable,
     checkModuleIndex,
     checkModuleNoCache,
+    checkImport,
+    withEmptyInsertedArgsStack,
+    withEmptyLocalVars,
+    inferExpression,
   )
 where
 
@@ -138,11 +142,14 @@ checkModuleIndex ::
   Sem r ModuleIndex
 checkModuleIndex = fmap ModuleIndex . cacheGet
 
+withEmptyInsertedArgsStack :: Sem (Reader InsertedArgsStack ': r) a -> Sem r a
+withEmptyInsertedArgsStack = runReader (mempty @InsertedArgsStack)
+
 checkModuleNoCache ::
   (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 {..}) = runReader (mempty @InsertedArgsStack) $ do
+checkModuleNoCache (ModuleIndex Module {..}) = withEmptyInsertedArgsStack $ do
   _moduleBody' <-
     evalState (mempty :: NegativeTypeParameters)
       . checkModuleBody

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs

@@ -8,8 +8,7 @@ where
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Scoped
 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.FromConcrete.Data.Context 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 (TerminationState)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable
 import Juvix.Compiler.Pipeline.EntryPoint qualified as E
@@ -20,7 +19,7 @@ type TypesTable = HashMap NameId Expression
 type NormalizedTable = HashMap NameId Expression
 
 data InternalTypedResult = InternalTypedResult
-  { _resultInternalArityResult :: InternalArityResult,
+  { _resultInternalResult :: Internal.InternalResult,
     _resultModules :: NonEmpty Module,
     _resultTermination :: TerminationState,
     _resultNormalized :: NormalizedTable,
@@ -35,7 +34,7 @@ mainModule :: Lens' InternalTypedResult Module
 mainModule = resultModules . _head1
 
 internalTypedResultEntryPoint :: Lens' InternalTypedResult E.EntryPoint
-internalTypedResultEntryPoint = resultInternalArityResult . Arity.internalArityResultEntryPoint
+internalTypedResultEntryPoint = resultInternalResult . Internal.internalResultEntryPoint
 
 internalTypedResultScoped :: Lens' InternalTypedResult Scoped.ScoperResult
-internalTypedResultScoped = resultInternalArityResult . Arity.internalArityResultScoped
+internalTypedResultScoped = resultInternalResult . Internal.resultScoper

src/Juvix/Compiler/Internal/Translation/FromInternal/Data.hs

@@ -1,8 +1,6 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Data
-  ( Arity.InternalArityResult,
+  ( Typechecking.InternalTypedResult,
-    Typechecking.InternalTypedResult,
   )
 where
 
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data qualified as Arity
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data qualified as Typechecking

src/Juvix/Compiler/Pipeline.hs

@@ -69,19 +69,10 @@ upToInternal ::
   Sem r Internal.InternalResult
 upToInternal = upToScoping >>= Internal.fromConcrete
 
-upToInternalArity ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, GitClone, PathResolver, Termination] r) =>
-  Sem r Internal.InternalArityResult
-upToInternalArity = upToInternal >>= Internal.arityChecking
-
 upToInternalTyped ::
   (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, GitClone, PathResolver] r) =>
   Sem r Internal.InternalTypedResult
-upToInternalTyped = do
+upToInternalTyped = Internal.typeCheckingNew upToInternal
-  newAlgorithm <- asks (^. entryPointNewTypeCheckingAlgorithm)
-  if
-      | newAlgorithm -> Internal.typeCheckingNew upToInternal
-      | otherwise -> Internal.typeChecking upToInternalArity
 
 upToInternalReachability ::
   (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, GitClone, PathResolver] r) =>

src/Juvix/Compiler/Pipeline/EntryPoint.hs

@@ -38,8 +38,7 @@ data EntryPoint = EntryPoint
     _entryPointGenericOptions :: GenericOptions,
     _entryPointModulePaths :: [Path Abs File],
     _entryPointSymbolPruningMode :: SymbolPruningMode,
-    _entryPointOffline :: Bool,
+    _entryPointOffline :: Bool
-    _entryPointNewTypeCheckingAlgorithm :: Bool
   }
   deriving stock (Eq, Show)
 
@@ -73,8 +72,7 @@ defaultEntryPointNoFile root =
       _entryPointInliningDepth = defaultInliningDepth,
       _entryPointModulePaths = [],
       _entryPointSymbolPruningMode = FilterUnreachable,
-      _entryPointOffline = False,
+      _entryPointOffline = False
-      _entryPointNewTypeCheckingAlgorithm = False
     }
 
 defaultUnrollLimit :: Int

src/Juvix/Compiler/Pipeline/Repl.hs

@@ -23,18 +23,17 @@ import Juvix.Data.Effect.Process (runProcessIO)
 import Juvix.Data.Effect.TaggedLock
 import Juvix.Prelude
 
-arityCheckExpression ::
+upToInternalExpression ::
   (Members '[Error JuvixError, State Artifacts, Termination] r) =>
   ExpressionAtoms 'Parsed ->
   Sem r Internal.Expression
-arityCheckExpression p = do
+upToInternalExpression p = do
   scopeTable <- gets (^. artifactScopeTable)
   runBuiltinsArtifacts
     . runScoperScopeArtifacts
     . runStateArtifacts artifactScoperState
     $ runNameIdGenArtifacts (Scoper.scopeCheckExpression scopeTable p)
       >>= runNameIdGenArtifacts . Internal.fromConcreteExpression
-      >>= Internal.arityCheckExpression
 
 expressionUpToAtomsParsed ::
   (Members '[State Artifacts, Error JuvixError] r) =>
@@ -111,7 +110,7 @@ importToInternalTyped ::
   (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   Internal.Import ->
   Sem r Internal.Import
-importToInternalTyped = Internal.arityCheckImport >=> Internal.typeCheckImport
+importToInternalTyped = Internal.typeCheckImport
 
 parseReplInput ::
   (Members '[PathResolver, Files, State Artifacts, Error JuvixError] r) =>
@@ -132,7 +131,7 @@ expressionUpToTyped ::
 expressionUpToTyped fp txt = do
   p <- expressionUpToAtomsParsed fp txt
   runTerminationArtifacts
-    ( arityCheckExpression p
+    ( upToInternalExpression p
         >>= Internal.typeCheckExpressionType
     )
 
@@ -142,7 +141,7 @@ compileExpression ::
   Sem r Core.Node
 compileExpression p =
   runTerminationArtifacts
-    ( arityCheckExpression p
+    ( upToInternalExpression p
         >>= Internal.typeCheckExpression
     )
     >>= fromInternalExpression

src/Juvix/Compiler/Pipeline/Run.hs

@@ -15,7 +15,6 @@ import Juvix.Compiler.Concrete.Translation.FromSource qualified as P
 import Juvix.Compiler.Core.Data.InfoTable qualified as Core
 import Juvix.Compiler.Core.Translation.FromInternal.Data qualified as Core
 import Juvix.Compiler.Internal.Translation qualified as Internal
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as Arity
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as Typed
 import Juvix.Compiler.Pipeline
@@ -165,8 +164,7 @@ corePipelineIOEither' lockMode entry = do
           internalResult :: Internal.InternalResult
           internalResult =
             typedResult
-              ^. Typed.resultInternalArityResult
+              ^. Typed.resultInternalResult
-                . Arity.resultInternalResult
 
           coreTable :: Core.InfoTable
           coreTable = coreRes ^. Core.coreResultTable

test/Arity.hs

@@ -1,10 +0,0 @@
-module Arity
-  ( allTests,
-  )
-where
-
-import Arity.Negative qualified as N
-import Base
-
-allTests :: TestTree
-allTests = testGroup "Arity tests" [N.allTests]

test/Arity/Negative.hs

@@ -1,116 +0,0 @@
-module Arity.Negative where
-
-import Base
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error
-import Juvix.Data.Effect.TaggedLock
-
-type FailMsg = String
-
-data NegTest = NegTest
-  { _name :: String,
-    _relDir :: Path Rel Dir,
-    _file :: Path Rel File,
-    _checkErr :: ArityCheckerError -> Maybe FailMsg
-  }
-
-testDescr :: NegTest -> TestDescr
-testDescr NegTest {..} =
-  let tRoot = root <//> _relDir
-      file' = tRoot <//> _file
-   in TestDescr
-        { _testName = _name,
-          _testRoot = tRoot,
-          _testAssertion = Single $ do
-            entryPoint <- defaultEntryPointIO' LockModeExclusive tRoot file'
-            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."
-              Right _ -> assertFailure "An error ocurred but it was not in the arity checker."
-        }
-
-allTests :: TestTree
-allTests =
-  testGroup
-    "Arity checker negative tests"
-    (map (mkTest . testDescr) tests)
-
-root :: Path Abs Dir
-root = relToProject $(mkRelDir "tests/negative")
-
-wrongError :: Maybe FailMsg
-wrongError = Just "Incorrect error"
-
-tests :: [NegTest]
-tests =
-  [ NegTest
-      "Too many arguments in expression"
-      $(mkRelDir "Internal")
-      $(mkRelFile "TooManyArguments.juvix")
-      $ \case
-        ErrTooManyArguments {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Pattern match a function type"
-      $(mkRelDir "Internal")
-      $(mkRelFile "FunctionPattern.juvix")
-      $ \case
-        ErrPatternFunction {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Function type (* → *) application"
-      $(mkRelDir "Internal")
-      $(mkRelFile "FunctionApplied.juvix")
-      $ \case
-        ErrFunctionApplied {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Expected explicit pattern"
-      $(mkRelDir "Internal")
-      $(mkRelFile "ExpectedExplicitPattern.juvix")
-      $ \case
-        ErrWrongPatternIsImplicit {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Expected explicit argument"
-      $(mkRelDir "Internal")
-      $(mkRelFile "ExpectedExplicitArgument.juvix")
-      $ \case
-        ErrExpectedExplicitArgument {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Function clause with two many patterns in the lhs"
-      $(mkRelDir "Internal")
-      $(mkRelFile "LhsTooManyPatterns.juvix")
-      $ \case
-        ErrLhsTooManyPatterns {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Too many arguments for the return type of a constructor"
-      $(mkRelDir "Internal")
-      $(mkRelFile "WrongReturnTypeTooManyArguments.juvix")
-      $ \case
-        ErrTooManyArguments {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Lazy builtin not fully applied"
-      $(mkRelDir "Internal")
-      $(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,
-    NegTest
-      "Detect default argument cycle in the arity checker"
-      $(mkRelDir "Internal")
-      $(mkRelFile "DefaultArgCycleArity.juvix")
-      $ \case
-        ErrDefaultArgCycle {} -> Nothing
-        _ -> wrongError
-  ]

test/Compilation.hs

@@ -3,7 +3,6 @@ module Compilation where
 import Base
 import Compilation.Negative qualified as N
 import Compilation.Positive qualified as P
-import Compilation.PositiveNew qualified as New
 
 allTests :: TestTree
-allTests = testGroup "Juvix compilation pipeline tests" [New.allTestsNoOptimize, P.allTestsNoOptimize, P.allTests, N.allTests]
+allTests = testGroup "Juvix compilation pipeline tests" [P.allTestsNoOptimize, P.allTests, N.allTests]

test/Compilation/Positive.hs

@@ -2,6 +2,7 @@ module Compilation.Positive where
 
 import Base
 import Compilation.Base
+import Data.HashSet qualified as HashSet
 
 data PosTest = PosTest
   { _name :: String,
@@ -60,362 +61,379 @@ posTest = posTest' EvalAndCompile
 posTestEval :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
 posTestEval = posTest' EvalOnly
 
+isIgnored :: PosTest -> Bool
+isIgnored t = HashSet.member (t ^. name) ignored
+
+ignored :: HashSet String
+ignored =
+  HashSet.fromList
+    [ -- TODO allow lambda branches of different number of patterns
+      "Test027: Church numerals"
+    ]
+
 tests :: [PosTest]
 tests =
-  [ posTest
+  filter
-      "Test001: Arithmetic operators"
+    (not . isIgnored)
-      $(mkRelDir ".")
+    [ posTest
-      $(mkRelFile "test001.juvix")
+        "Test001: Arithmetic operators"
-      $(mkRelFile "out/test001.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test001.juvix")
-      "Test002: Arithmetic operators inside lambdas"
+        $(mkRelFile "out/test001.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test002.juvix")
+        "Test002: Arithmetic operators inside lambdas"
-      $(mkRelFile "out/test002.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test002.juvix")
-      "Test003: Integer arithmetic"
+        $(mkRelFile "out/test002.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test003.juvix")
+        "Test003: Integer arithmetic"
-      $(mkRelFile "out/test003.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test003.juvix")
-      "Test004: IO builtins"
+        $(mkRelFile "out/test003.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test004.juvix")
+        "Test004: IO builtins"
-      $(mkRelFile "out/test004.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test004.juvix")
-      "Test005: Higher-order functions"
+        $(mkRelFile "out/test004.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test005.juvix")
+        "Test005: Higher-order functions"
-      $(mkRelFile "out/test005.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test005.juvix")
-      "Test006: If-then-else and lazy boolean operators"
+        $(mkRelFile "out/test005.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test006.juvix")
+        "Test006: If-then-else and lazy boolean operators"
-      $(mkRelFile "out/test006.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test006.juvix")
-      "Test007: Pattern matching and lambda-case"
+        $(mkRelFile "out/test006.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test007.juvix")
+        "Test007: Pattern matching and lambda-case"
-      $(mkRelFile "out/test007.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test007.juvix")
-      "Test008: Recursion"
+        $(mkRelFile "out/test007.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test008.juvix")
+        "Test008: Recursion"
-      $(mkRelFile "out/test008.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test008.juvix")
-      "Test009: Tail recursion"
+        $(mkRelFile "out/test008.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test009.juvix")
+        "Test009: Tail recursion"
-      $(mkRelFile "out/test009.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test009.juvix")
-      "Test010: Let"
+        $(mkRelFile "out/test009.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test010.juvix")
+        "Test010: Let"
-      $(mkRelFile "out/test010.out"),
+        $(mkRelDir ".")
-    posTestEval
+        $(mkRelFile "test010.juvix")
-      "Test011: Tail recursion: Fibonacci numbers in linear time"
+        $(mkRelFile "out/test010.out"),
-      $(mkRelDir ".")
+      posTestEval
-      $(mkRelFile "test011.juvix")
+        "Test011: Tail recursion: Fibonacci numbers in linear time"
-      $(mkRelFile "out/test011.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test011.juvix")
-      "Test012: Trees"
+        $(mkRelFile "out/test011.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test012.juvix")
+        "Test012: Trees"
-      $(mkRelFile "out/test012.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test012.juvix")
-      "Test013: Functions returning functions with variable capture"
+        $(mkRelFile "out/test012.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test013.juvix")
+        "Test013: Functions returning functions with variable capture"
-      $(mkRelFile "out/test013.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test013.juvix")
-      "Test014: Arithmetic"
+        $(mkRelFile "out/test013.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test014.juvix")
+        "Test014: Arithmetic"
-      $(mkRelFile "out/test014.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test014.juvix")
-      "Test015: Local functions with free variables"
+        $(mkRelFile "out/test014.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test015.juvix")
+        "Test015: Local functions with free variables"
-      $(mkRelFile "out/test015.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test015.juvix")
-      "Test016: Recursion through higher-order functions"
+        $(mkRelFile "out/test015.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test016.juvix")
+        "Test016: Recursion through higher-order functions"
-      $(mkRelFile "out/test016.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test016.juvix")
-      "Test017: Tail recursion through higher-order functions"
+        $(mkRelFile "out/test016.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test017.juvix")
+        "Test017: Tail recursion through higher-order functions"
-      $(mkRelFile "out/test017.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test017.juvix")
-      "Test018: Higher-order functions and recursion"
+        $(mkRelFile "out/test017.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test018.juvix")
+        "Test018: Higher-order functions and recursion"
-      $(mkRelFile "out/test018.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test018.juvix")
-      "Test019: Self-application"
+        $(mkRelFile "out/test018.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test019.juvix")
+        "Test019: Self-application"
-      $(mkRelFile "out/test019.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test019.juvix")
-      "Test020: Recursive functions: McCarthy's 91 function, subtraction by increments"
+        $(mkRelFile "out/test019.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test020.juvix")
+        "Test020: Recursive functions: McCarthy's 91 function, subtraction by increments"
-      $(mkRelFile "out/test020.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test020.juvix")
-      "Test021: Fast exponentiation"
+        $(mkRelFile "out/test020.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test021.juvix")
+        "Test021: Fast exponentiation"
-      $(mkRelFile "out/test021.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test021.juvix")
-      "Test022: Lists"
+        $(mkRelFile "out/test021.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test022.juvix")
+        "Test022: Lists"
-      $(mkRelFile "out/test022.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test022.juvix")
-      "Test023: Mutual recursion"
+        $(mkRelFile "out/test022.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test023.juvix")
+        "Test023: Mutual recursion"
-      $(mkRelFile "out/test023.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test023.juvix")
-      "Test024: Nested binders with variable capture"
+        $(mkRelFile "out/test023.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test024.juvix")
+        "Test024: Nested binders with variable capture"
-      $(mkRelFile "out/test024.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test024.juvix")
-      "Test025: Euclid's algorithm"
+        $(mkRelFile "out/test024.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test025.juvix")
+        "Test025: Euclid's algorithm"
-      $(mkRelFile "out/test025.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test025.juvix")
-      "Test026: Functional queues"
+        $(mkRelFile "out/test025.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test026.juvix")
+        "Test026: Functional queues"
-      $(mkRelFile "out/test026.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test026.juvix")
-      "Test027: Church numerals"
+        $(mkRelFile "out/test026.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test027.juvix")
+        "Test027: Church numerals"
-      $(mkRelFile "out/test027.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test027.juvix")
-      "Test028: Streams without memoization"
+        $(mkRelFile "out/test027.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test028.juvix")
+        "Test028: Streams without memoization"
-      $(mkRelFile "out/test028.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test028.juvix")
-      "Test029: Ackermann function"
+        $(mkRelFile "out/test028.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test029.juvix")
+        "Test029: Ackermann function"
-      $(mkRelFile "out/test029.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test029.juvix")
-      "Test030: Ackermann function (higher-order definition)"
+        $(mkRelFile "out/test029.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test030.juvix")
+        "Test030: Ackermann function (higher-order definition)"
-      $(mkRelFile "out/test030.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test030.juvix")
-      "Test031: Nested lists"
+        $(mkRelFile "out/test030.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test031.juvix")
+        "Test031: Nested lists"
-      $(mkRelFile "out/test031.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test031.juvix")
-      "Test032: Merge sort"
+        $(mkRelFile "out/test031.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test032.juvix")
+        "Test032: Merge sort"
-      $(mkRelFile "out/test032.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test032.juvix")
-      "Test033: Eta-expansion of builtins and constructors"
+        $(mkRelFile "out/test032.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test033.juvix")
+        "Test033: Eta-expansion of builtins and constructors"
-      $(mkRelFile "out/test033.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test033.juvix")
-      "Test034: Recursive let"
+        $(mkRelFile "out/test033.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test034.juvix")
+        "Test034: Recursive let"
-      $(mkRelFile "out/test034.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test034.juvix")
-      "Test035: Pattern matching"
+        $(mkRelFile "out/test034.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test035.juvix")
+        "Test035: Pattern matching"
-      $(mkRelFile "out/test035.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test035.juvix")
-      "Test036: Eta-expansion"
+        $(mkRelFile "out/test035.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test036.juvix")
+        "Test036: Eta-expansion"
-      $(mkRelFile "out/test036.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test036.juvix")
-      "Test037: Applications with lets and cases in function position"
+        $(mkRelFile "out/test036.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test037.juvix")
+        "Test037: Applications with lets and cases in function position"
-      $(mkRelFile "out/test037.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test037.juvix")
-      "Test038: Simple case expression"
+        $(mkRelFile "out/test037.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test038.juvix")
+        "Test038: Simple case expression"
-      $(mkRelFile "out/test038.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test038.juvix")
-      "Test039: Mutually recursive let expression"
+        $(mkRelFile "out/test038.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test039.juvix")
+        "Test039: Mutually recursive let expression"
-      $(mkRelFile "out/test039.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test039.juvix")
-      "Test040: Pattern matching nullary constructor"
+        $(mkRelFile "out/test039.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test040.juvix")
+        "Test040: Pattern matching nullary constructor"
-      $(mkRelFile "out/test040.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test040.juvix")
-      "Test041: Use a builtin inductive in an inductive constructor"
+        $(mkRelFile "out/test040.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test041.juvix")
+        "Test041: Use a builtin inductive in an inductive constructor"
-      $(mkRelFile "out/test041.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test041.juvix")
-      "Test042: Builtin string-to-nat"
+        $(mkRelFile "out/test041.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test042.juvix")
+        "Test042: Builtin string-to-nat"
-      $(mkRelFile "out/test042.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test042.juvix")
-      "Test043: Builtin trace"
+        $(mkRelFile "out/test042.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test043.juvix")
+        "Test043: Builtin trace"
-      $(mkRelFile "out/test043.out"),
+        $(mkRelDir ".")
-    posTestStdin
+        $(mkRelFile "test043.juvix")
-      "Test044: Builtin readline"
+        $(mkRelFile "out/test043.out"),
-      $(mkRelDir ".")
+      posTestStdin
-      $(mkRelFile "test044.juvix")
+        "Test044: Builtin readline"
-      $(mkRelFile "out/test044.out")
+        $(mkRelDir ".")
-      "a\n",
+        $(mkRelFile "test044.juvix")
-    posTest
+        $(mkRelFile "out/test044.out")
-      "Test045: Implicit builtin bool"
+        "a\n",
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test045.juvix")
+        "Test045: Implicit builtin bool"
-      $(mkRelFile "out/test045.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test045.juvix")
-      "Test046: Polymorphic type arguments"
+        $(mkRelFile "out/test045.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test046.juvix")
+        "Test046: Polymorphic type arguments"
-      $(mkRelFile "out/test046.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test046.juvix")
-      "Test047: Local Modules"
+        $(mkRelFile "out/test046.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test047.juvix")
+        "Test047: Local Modules"
-      $(mkRelFile "out/test047.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test047.juvix")
-      "Test048: String quoting"
+        $(mkRelFile "out/test047.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test048.juvix")
+        "Test048: String quoting"
-      $(mkRelFile "out/test048.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test048.juvix")
-      "Test049: Builtin Int"
+        $(mkRelFile "out/test048.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test049.juvix")
+        "Test049: Builtin Int"
-      $(mkRelFile "out/test049.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test049.juvix")
-      "Test050: Pattern matching with integers"
+        $(mkRelFile "out/test049.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test050.juvix")
+        "Test050: Pattern matching with integers"
-      $(mkRelFile "out/test050.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test050.juvix")
-      "Test051: Local recursive function using IO >>"
+        $(mkRelFile "out/test050.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test051.juvix")
+        "Test051: Local recursive function using IO >>"
-      $(mkRelFile "out/test051.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test051.juvix")
-      "Test052: Simple lambda calculus"
+        $(mkRelFile "out/test051.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test052.juvix")
+        "Test052: Simple lambda calculus"
-      $(mkRelFile "out/test052.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test052.juvix")
-      "Test053: Inlining"
+        $(mkRelFile "out/test052.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test053.juvix")
+        "Test053: Inlining"
-      $(mkRelFile "out/test053.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test053.juvix")
-      "Test054: Iterators"
+        $(mkRelFile "out/test053.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test054.juvix")
+        "Test054: Iterators"
-      $(mkRelFile "out/test054.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test054.juvix")
-      "Test055: Constructor printing"
+        $(mkRelFile "out/test054.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test055.juvix")
+        "Test055: Constructor printing"
-      $(mkRelFile "out/test055.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test055.juvix")
-      "Test056: Argument specialization"
+        $(mkRelFile "out/test055.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test056.juvix")
+        "Test056: Argument specialization"
-      $(mkRelFile "out/test056.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test056.juvix")
-      "Test057: Case folding"
+        $(mkRelFile "out/test056.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test057.juvix")
+        "Test057: Case folding"
-      $(mkRelFile "out/test057.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test057.juvix")
-      "Test058: Ranges"
+        $(mkRelFile "out/test057.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test058.juvix")
+        "Test058: Ranges"
-      $(mkRelFile "out/test058.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test058.juvix")
-      "Test059: Builtin list"
+        $(mkRelFile "out/test058.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test059.juvix")
+        "Test059: Builtin list"
-      $(mkRelFile "out/test059.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test059.juvix")
-      "Test060: Record update"
+        $(mkRelFile "out/test059.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test060.juvix")
+        "Test060: Record update"
-      $(mkRelFile "out/test060.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test060.juvix")
-      "Test061: Traits"
+        $(mkRelFile "out/test060.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test061.juvix")
+        "Test061: Traits"
-      $(mkRelFile "out/test061.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test061.juvix")
-      "Test062: Overapplication"
+        $(mkRelFile "out/test061.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test062.juvix")
+        "Test062: Overapplication"
-      $(mkRelFile "out/test062.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test062.juvix")
-      "Test063: Coercions"
+        $(mkRelFile "out/test062.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test063.juvix")
+        "Test063: Coercions"
-      $(mkRelFile "out/test063.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test063.juvix")
-      "Test064: Constant folding"
+        $(mkRelFile "out/test063.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test064.juvix")
+        "Test064: Constant folding"
-      $(mkRelFile "out/test064.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test064.juvix")
-      "Test065: Arithmetic simplification"
+        $(mkRelFile "out/test064.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test065.juvix")
+        "Test065: Arithmetic simplification"
-      $(mkRelFile "out/test065.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test065.juvix")
-      "Test066: Import function with a function call in default argument"
+        $(mkRelFile "out/test065.out"),
-      $(mkRelDir "test066")
+      posTest
-      $(mkRelFile "M.juvix")
+        "Test066: Import function with a function call in default argument"
-      $(mkRelFile "out/test066.out"),
+        $(mkRelDir "test066")
-    posTest
+        $(mkRelFile "M.juvix")
-      "Test067: Dependent default values inserted during translation FromConcrete"
+        $(mkRelFile "out/test066.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test067.juvix")
+        "Test067: Dependent default values inserted during translation FromConcrete"
-      $(mkRelFile "out/test067.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test067.juvix")
-      "Test068: Dependent default values inserted in the arity checker"
+        $(mkRelFile "out/test067.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test068.juvix")
+        "Test068: Dependent default values inserted in the arity checker"
-      $(mkRelFile "out/test068.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test068.juvix")
-      "Test069: Dependent default values for Ord trait"
+        $(mkRelFile "out/test068.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test069.juvix")
+        "Test069: Dependent default values for Ord trait"
-      $(mkRelFile "out/test069.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test069.juvix")
-      "Test070: Nested default values and named arguments"
+        $(mkRelFile "out/test069.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test070.juvix")
+        "Test070: Nested default values and named arguments"
-      $(mkRelFile "out/test070.out"),
+        $(mkRelDir ".")
-    posTest
+        $(mkRelFile "test070.juvix")
-      "Test071: Named application (Ord instance with default cmp)"
+        $(mkRelFile "out/test070.out"),
-      $(mkRelDir ".")
+      posTest
-      $(mkRelFile "test071.juvix")
+        "Test071: Named application (Ord instance with default cmp)"
-      $(mkRelFile "out/test071.out")
+        $(mkRelDir ".")
-  ]
+        $(mkRelFile "test071.juvix")
+        $(mkRelFile "out/test071.out"),
+      posTest
+        "Test072: Monad transformers (ReaderT + StateT + Identity)"
+        $(mkRelDir "test072")
+        $(mkRelFile "ReaderT.juvix")
+        $(mkRelFile "out/test072.out")
+    ]

test/Compilation/PositiveNew.hs

@@ -1,56 +0,0 @@
-module Compilation.PositiveNew where
-
-import Base
-import Compilation.Base
-import Compilation.Positive qualified as Old
-import Data.HashSet qualified as HashSet
-
-root :: Path Abs Dir
-root = relToProject $(mkRelDir "tests/positive")
-
-posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> Old.PosTest
-posTest = posTest' EvalAndCompile
-
-posTest' :: CompileAssertionMode -> String -> Path Rel Dir -> Path Rel File -> Path Rel File -> Old.PosTest
-posTest' _assertionMode _name rdir rfile routfile =
-  let _dir = root <//> rdir
-      _file = _dir <//> rfile
-      _expectedFile = root <//> routfile
-   in Old.PosTest {..}
-
-testDescr :: Int -> Old.PosTest -> TestDescr
-testDescr optLevel Old.PosTest {..} =
-  TestDescr
-    { _testName = _name,
-      _testRoot = _dir,
-      _testAssertion =
-        Steps $
-          let f = set entryPointNewTypeCheckingAlgorithm True
-           in compileAssertionEntry f _dir optLevel _assertionMode _file _expectedFile
-    }
-
-allTestsNoOptimize :: TestTree
-allTestsNoOptimize =
-  testGroup
-    "New typechecker compilation positive tests (no optimization)"
-    (map (mkTest . testDescr 0) (filter (not . isIgnored) (extraTests <> Old.tests)))
-
-isIgnored :: Old.PosTest -> Bool
-isIgnored t = HashSet.member (t ^. Old.name) ignored
-
-extraTests :: [Old.PosTest]
-extraTests =
-  [ Old.posTest
-      "Test073: Monad transformers (ReaderT + StateT + Identity)"
-      $(mkRelDir "test072")
-      $(mkRelFile "ReaderT.juvix")
-      $(mkRelFile "out/test072.out")
-  ]
-
-ignored :: HashSet String
-ignored =
-  HashSet.fromList
-    [ "Test046: Polymorphic type arguments",
-      -- TODO allow lambda branches of different number of patterns
-      "Test027: Church numerals"
-    ]

test/Main.hs

@@ -1,6 +1,5 @@
 module Main (main) where
 
-import Arity qualified
 import Asm qualified
 import BackendGeb qualified
 import BackendMarkdown qualified
@@ -41,7 +40,6 @@ fastTests =
     [ Parsing.allTests,
       Scope.allTests,
       Termination.allTests,
-      Arity.allTests,
       Typecheck.allTests,
       Reachability.allTests,
       Format.allTests,

test/Scope/Negative.hs

@@ -380,13 +380,6 @@ scoperErrorTests =
       $ \case
         ErrWrongDefaultValue {} -> Nothing
         _ -> wrongError,
-    NegTest
-      "Unsupported type"
-      $(mkRelDir ".")
-      $(mkRelFile "UnsupportedType.juvix")
-      $ \case
-        ErrUnsupported {} -> Nothing
-        _ -> wrongError,
     NegTest
       "Default argument cycle in FromConcrete"
       $(mkRelDir ".")

test/Typecheck.hs

@@ -2,9 +2,7 @@ module Typecheck (allTests) where
 
 import Base
 import Typecheck.Negative qualified as N
-import Typecheck.NegativeNew qualified as NewNeg
 import Typecheck.Positive qualified as P
-import Typecheck.PositiveNew qualified as New
 
 allTests :: TestTree
-allTests = testGroup "Type checker tests" [New.allTests, P.allTests, N.allTests, NewNeg.allTests]
+allTests = testGroup "Type checker tests" [P.allTests, N.allTests]

test/Typecheck/NegativeNew.hs

@@ -30,7 +30,7 @@ testDescr Old.NegTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive tRoot file'
+            entryPoint <- defaultEntryPointIO' LockModeExclusive tRoot file'
             result <- runIOEither' LockModeExclusive entryPoint upToCore
             case mapLeft fromJuvixError result of
               Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure

test/Typecheck/PositiveNew.hs

@@ -1,48 +0,0 @@
-module Typecheck.PositiveNew where
-
-import Base
-import Data.HashSet qualified as HashSet
-import Juvix.Data.Effect.TaggedLock
-import Typecheck.Positive qualified as Old
-
-root :: Path Abs Dir
-root = relToProject $(mkRelDir "tests/positive")
-
-posTest :: String -> Path Rel Dir -> Path Rel File -> Old.PosTest
-posTest _name rdir rfile =
-  let _dir = root <//> rdir
-      _file = _dir <//> rfile
-   in Old.PosTest {..}
-
-testDescr :: Old.PosTest -> TestDescr
-testDescr Old.PosTest {..} =
-  TestDescr
-    { _testName = _name,
-      _testRoot = _dir,
-      _testAssertion = Single $ do
-        entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive _dir _file
-        (void . runIOExclusive entryPoint) upToInternalTyped
-    }
-
-allTests :: TestTree
-allTests =
-  testGroup
-    "New typechecker positive tests"
-    [ testGroup
-        "New typechecker General typechecking tests"
-        (map (mkTest . testDescr) (filter (not . isIgnored) (extraTests <> Old.tests)))
-    ]
-
-isIgnored :: Old.PosTest -> Bool
-isIgnored t = HashSet.member (t ^. Old.name) ignored
-
-extraTests :: [Old.PosTest]
-extraTests = []
-
--- | Default values are not supported by the new type checker at the moment
-ignored :: HashSet String
-ignored =
-  HashSet.fromList
-    [ -- This test does not pass with the new hole insertion algorithm
-      "Test046: Polymorphic type arguments"
-    ]

tests/Compilation/positive/test046.juvix

@@ -1,13 +1,17 @@
 -- polymorphic type arguments
 module test046;
 
-import Stdlib.Prelude open;
+import Stdlib.Data.Nat open;
+import Stdlib.Function open;
 
 Ty : Type := {B : Type} -> B -> B;
 
 id' : Ty
   | {_} x := x;
 
-fun : {A : Type} → A → Ty := id λ {_ := id'};
+-- In PR https://github.com/anoma/juvix/pull/2545 we had to slightly modify
+-- the `fun` definition. The previous version is kept here as a comment.
+-- fun : {A : Type} → A → Ty := id λ {_ := id'};
+fun {A : Type} : A → Ty := id { _ -> {C : Type} → C → C } λ {_ := id'};
 
 main : Nat := fun 5 {Nat} 7;

tests/negative/UnsupportedType.juvix

@@ -1,5 +0,0 @@
-module UnsupportedType;
-
-type List' (A : Type -> Type) :=
-  | nil'
-  | cons' A (List' A);