diff --git a/Makefile b/Makefile
index 5941ed2cdf..1cf43d4de6 100644
--- a/Makefile
+++ b/Makefile
@@ -264,7 +264,7 @@ SMOKE := $(shell command -v smoke 2> /dev/null)
 
 .PHONY : smoke-only
 smoke-only:
-	@$(if $(SMOKE),, $(error "Smoke not found, please install it from https://github.com/SamirTalwar/smoke"))
+	@$(if $(SMOKE),, $(error "Smoke not found, please install it from https://github.com/jonaprieto/smoke"))
 	@smoke $(shell find tests -name '*.smoke.yaml')
 
 .PHONY : smoke
diff --git a/app/Commands/Compile.hs b/app/Commands/Compile.hs
index a2c6a4e131..08b5618d9d 100644
--- a/app/Commands/Compile.hs
+++ b/app/Commands/Compile.hs
@@ -2,191 +2,30 @@ module Commands.Compile where
 
 import Commands.Base
 import Commands.Compile.Options
-import Data.ByteString qualified as BS
-import Data.FileEmbed qualified as FE
+import Commands.Dev.Core.Compile.Base qualified as Compile
+import Commands.Extra.Compile qualified as Compile
 import Data.Text.IO qualified as TIO
-import Juvix.Compiler.Backend.C.Translation.FromInternal qualified as MiniC
-import System.Environment
-import System.Process qualified as P
+import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Core.Pretty qualified as Core
 
 runCommand :: (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
 runCommand opts@CompileOptions {..} = do
-  miniC <- (^. MiniC.resultCCode) <$> runPipeline _compileInputFile upToMiniC
   inputFile <- someBaseToAbs' (_compileInputFile ^. pathPath)
-  result <- runCompile inputFile opts miniC
-  case result of
-    Left err -> printFailureExit err
-    _ -> return ()
-
-inputCFile :: (Members '[App] r) => Path Abs File -> Sem r (Path Abs File)
-inputCFile inputFileCompile = do
-  buildDir <- askBuildDir
-  return (buildDir <//> outputMiniCFile)
-  where
-    outputMiniCFile :: Path Rel File
-    outputMiniCFile = replaceExtension' ".c" (filename inputFileCompile)
-
-runCompile :: (Members '[Embed IO, App] r) => Path Abs File -> CompileOptions -> Text -> Sem r (Either Text ())
-runCompile inputFileCompile o minic = do
-  buildDir <- askBuildDir
-  ensureDir buildDir
-  f <- inputCFile inputFileCompile
-  embed (TIO.writeFile (toFilePath f) minic)
-  prepareRuntime o
-  case o ^. compileTarget of
-    TargetWasm -> runError (clangCompile inputFileCompile o)
-    TargetC -> return (Right ())
-    TargetNative -> runError (clangNativeCompile inputFileCompile o)
-
-prepareRuntime :: forall r. (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
-prepareRuntime o = mapM_ writeRuntime runtimeProjectDir
-  where
-    runtimeProjectDir :: [(Path Rel File, BS.ByteString)]
-    runtimeProjectDir = case o ^. compileTarget of
-      TargetNative -> libcRuntime
-      _ -> case o ^. compileRuntime of
-        RuntimeWasiStandalone -> wasiStandaloneRuntimeDir <> builtinCRuntimeDir <> wallocDir
-        RuntimeWasiLibC -> libcRuntime
-        RuntimeStandalone -> standaloneRuntimeDir <> builtinCRuntimeDir <> wallocDir
-
-    writeRuntime :: (Path Rel File, BS.ByteString) -> Sem r ()
-    writeRuntime (filePath, contents) = do
-      buildDir <- askBuildDir
-      embed (BS.writeFile (toFilePath (buildDir <//> filePath)) contents)
-
-wasiStandaloneRuntimeDir :: [(Path Rel File, BS.ByteString)]
-wasiStandaloneRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/wasi-standalone" >>= FE.embedDir)
-
-standaloneRuntimeDir :: [(Path Rel File, BS.ByteString)]
-standaloneRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/standalone" >>= FE.embedDir)
-
-wasiLibCRuntimeDir :: [(Path Rel File, BS.ByteString)]
-wasiLibCRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/wasi-libc" >>= FE.embedDir)
-
-builtinCRuntimeDir :: [(Path Rel File, BS.ByteString)]
-builtinCRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/builtins" >>= FE.embedDir)
-
-wallocDir :: [(Path Rel File, BS.ByteString)]
-wallocDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/walloc" >>= FE.embedDir)
-
-libcRuntime :: [(Path Rel File, BS.ByteString)]
-libcRuntime = wasiLibCRuntimeDir <> builtinCRuntimeDir
-
-clangNativeCompile ::
-  forall r.
-  (Members '[Embed IO, App, Error Text] r) =>
-  Path Abs File ->
-  CompileOptions ->
-  Sem r ()
-clangNativeCompile inputFileCompile o = do
-  inputFile <- getInputFile
-  outputFile <- getOutputFile
-  buildDir <- askBuildDir
-  runClang (nativeArgs buildDir outputFile inputFile)
-  where
-    getOutputFile :: Sem r (Path Abs File)
-    getOutputFile = case o ^. compileOutputFile of
-      Nothing -> return (removeExtension' inputFileCompile)
-      Just f -> someBaseToAbs' (f ^. pathPath)
-
-    getInputFile :: Sem r (Path Abs File)
-    getInputFile = inputCFile inputFileCompile
-
-clangCompile ::
-  forall r.
-  (Members '[Embed IO, App, Error Text] r) =>
-  Path Abs File ->
-  CompileOptions ->
-  Sem r ()
-clangCompile inputFileCompile o = do
-  outputFile <- getOutputFile
-  inputFile <- getInputFile
-  let clangArgs :: Sem r [String]
-      clangArgs = case o ^. compileRuntime of
-        RuntimeStandalone -> do
-          standaloneLibArgs outputFile inputFile
-        RuntimeWasiStandalone -> wasiStandaloneArgs outputFile inputFile
-        RuntimeWasiLibC -> wasiLibcArgs outputFile inputFile
-
-  clangArgs >>= runClang
-  where
-    getOutputFile :: Sem r (Path Abs File)
-    getOutputFile = maybe (return defaultOutputFile) someBaseToAbs' (o ^? compileOutputFile . _Just . pathPath)
-
-    defaultOutputFile :: Path Abs File
-    defaultOutputFile = replaceExtension' ".wasm" inputFileCompile
-
-    getInputFile :: Sem r (Path Abs File)
-    getInputFile = inputCFile inputFileCompile
-
-sysrootEnvVar :: (Members '[Error Text, Embed IO] r) => Sem r (Path Abs Dir)
-sysrootEnvVar =
-  absDir
-    <$> fromMaybeM (throw msg) (embed (lookupEnv "WASI_SYSROOT_PATH"))
-  where
-    msg :: Text
-    msg = "Missing environment variable WASI_SYSROOT_PATH"
-
-commonArgs :: Path Abs Dir -> Path Abs File -> [String]
-commonArgs buildDir wasmOutputFile =
-  [ "-std=c99",
-    "-Oz",
-    "-I",
-    toFilePath buildDir,
-    "-o",
-    toFilePath wasmOutputFile
-  ]
-
-standaloneLibArgs :: (Members '[App, Embed IO] r) => Path Abs File -> Path Abs File -> Sem r [String]
-standaloneLibArgs wasmOutputFile inputFile = do
-  buildDir <- askBuildDir
-  return $
-    commonArgs buildDir wasmOutputFile
-      <> [ "--target=wasm32",
-           "-nodefaultlibs",
-           "-nostartfiles",
-           "-Wl,--no-entry",
-           toFilePath (buildDir <//> $(mkRelFile "walloc.c")),
-           toFilePath inputFile
-         ]
-
-wasiStandaloneArgs :: (Members '[App, Error Text, Embed IO] r) => Path Abs File -> Path Abs File -> Sem r [String]
-wasiStandaloneArgs wasmOutputFile inputFile = do
-  buildDir <- askBuildDir
-  com <- wasiCommonArgs wasmOutputFile
-  return $
-    com
-      <> [ toFilePath (buildDir <//> $(mkRelFile "walloc.c")),
-           toFilePath inputFile
-         ]
-
-wasiLibcArgs :: (Members '[App, Error Text, Embed IO] r) => Path Abs File -> Path Abs File -> Sem r [String]
-wasiLibcArgs wasmOutputFile inputFile = do
-  com <- wasiCommonArgs wasmOutputFile
-  return $ com <> ["-lc", toFilePath inputFile]
-
-nativeArgs :: Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
-nativeArgs buildDir outputFile inputFile =
-  commonArgs buildDir outputFile <> [toFilePath inputFile]
-
-wasiCommonArgs :: (Members '[App, Error Text, Embed IO] r) => Path Abs File -> Sem r [String]
-wasiCommonArgs wasmOutputFile = do
-  sysrootPath <- sysrootEnvVar
-  buildDir <- askBuildDir
-  return $
-    commonArgs buildDir wasmOutputFile
-      <> [ "-nodefaultlibs",
-           "--target=wasm32-wasi",
-           "--sysroot",
-           toFilePath sysrootPath
-         ]
-
-runClang ::
-  (Members '[Embed IO, Error Text] r) =>
-  [String] ->
-  Sem r ()
-runClang args = do
-  (exitCode, _, err) <- embed (P.readProcessWithExitCode "clang" args "")
-  case exitCode of
-    ExitSuccess -> return ()
-    _ -> throw (pack err)
+  Core.CoreResult {..} <- runPipeline _compileInputFile upToCore
+  let arg =
+        Compile.PipelineArg
+          { _pipelineArgFile = inputFile,
+            _pipelineArgOptions = opts,
+            _pipelineArgInfoTable = _coreResultTable
+          }
+  case _compileTarget of
+    TargetNative64 -> Compile.runCPipeline arg
+    TargetWasm32Wasi -> Compile.runCPipeline arg
+    TargetGeb -> Compile.runGebPipeline arg
+    TargetCore -> writeCoreFile arg
+    TargetAsm -> Compile.runAsmPipeline arg
+
+writeCoreFile :: (Members '[Embed IO, App] r) => Compile.PipelineArg -> Sem r ()
+writeCoreFile Compile.PipelineArg {..} = do
+  coreFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  embed $ TIO.writeFile (toFilePath coreFile) (show $ Core.ppOut Core.defaultOptions {Core._optShowDeBruijnIndices = True} _pipelineArgInfoTable)
diff --git a/app/Commands/Compile/Options.hs b/app/Commands/Compile/Options.hs
index 9ad9605297..61c7b698a6 100644
--- a/app/Commands/Compile/Options.hs
+++ b/app/Commands/Compile/Options.hs
@@ -1,77 +1,6 @@
-module Commands.Compile.Options where
+module Commands.Compile.Options
+  ( module Commands.Extra.Compile.Options,
+  )
+where
 
-import CommonOptions
-
-data CompileTarget
-  = TargetC
-  | TargetWasm
-  | TargetNative
-  deriving stock (Show, Data)
-
-data CompileRuntime
-  = RuntimeWasiStandalone
-  | RuntimeWasiLibC
-  | RuntimeStandalone
-  deriving stock (Show, Data)
-
-data CompileOptions = CompileOptions
-  { _compileTarget :: CompileTarget,
-    _compileRuntime :: CompileRuntime,
-    _compileOutputFile :: Maybe (AppPath File),
-    _compileInputFile :: AppPath File
-  }
-  deriving stock (Data)
-
-makeLenses ''CompileOptions
-
-parseCompile :: Parser CompileOptions
-parseCompile = do
-  _compileTarget <-
-    option
-      (eitherReader parseTarget)
-      ( long "target"
-          <> short 't'
-          <> metavar "TARGET"
-          <> value TargetNative
-          <> showDefaultWith targetShow
-          <> help "select a target: wasm, c, native"
-      )
-  _compileRuntime <-
-    option
-      (eitherReader parseRuntime)
-      ( long "runtime"
-          <> short 'r'
-          <> metavar "RUNTIME"
-          <> value RuntimeWasiStandalone
-          <> showDefaultWith runtimeShow
-          <> help "select a runtime: wasi-standalone, wasi-libc, standalone"
-      )
-  _compileOutputFile <- optional parseGenericOutputFile
-  _compileInputFile <- parseInputJuvixFile
-  pure CompileOptions {..}
-  where
-    parseTarget :: String -> Either String CompileTarget
-    parseTarget = \case
-      "wasm" -> Right TargetWasm
-      "c" -> Right TargetC
-      "native" -> Right TargetNative
-      s -> Left $ "unrecognised target: " <> s
-
-    targetShow :: CompileTarget -> String
-    targetShow = \case
-      TargetC -> "c"
-      TargetWasm -> "wasm"
-      TargetNative -> "native"
-
-    parseRuntime :: String -> Either String CompileRuntime
-    parseRuntime = \case
-      "wasi-standalone" -> Right RuntimeWasiStandalone
-      "wasi-libc" -> Right RuntimeWasiLibC
-      "standalone" -> Right RuntimeStandalone
-      s -> Left $ "unrecognised runtime: " <> s
-
-    runtimeShow :: CompileRuntime -> String
-    runtimeShow = \case
-      RuntimeWasiStandalone -> "wasi-standalone"
-      RuntimeWasiLibC -> "wasi-libc"
-      RuntimeStandalone -> "standalone"
+import Commands.Extra.Compile.Options
diff --git a/app/Commands/Dev.hs b/app/Commands/Dev.hs
index 7d9e1128f1..a5d4431c76 100644
--- a/app/Commands/Dev.hs
+++ b/app/Commands/Dev.hs
@@ -11,7 +11,6 @@ import Commands.Dev.DisplayRoot qualified as DisplayRoot
 import Commands.Dev.Geb qualified as Geb
 import Commands.Dev.Highlight qualified as Highlight
 import Commands.Dev.Internal qualified as Internal
-import Commands.Dev.MiniC qualified as MiniC
 import Commands.Dev.Options
 import Commands.Dev.Parse qualified as Parse
 import Commands.Dev.Runtime qualified as Runtime
@@ -24,7 +23,6 @@ runCommand = \case
   Parse opts -> Parse.runCommand opts
   Scope opts -> Scope.runCommand opts
   Internal opts -> Internal.runCommand opts
-  MiniC opts -> MiniC.runCommand opts
   Termination opts -> Termination.runCommand opts
   Core opts -> Core.runCommand opts
   Geb opts -> Geb.runCommand opts
diff --git a/app/Commands/Dev/Asm/Compile.hs b/app/Commands/Dev/Asm/Compile.hs
index d3d2226994..359a142456 100644
--- a/app/Commands/Dev/Asm/Compile.hs
+++ b/app/Commands/Dev/Asm/Compile.hs
@@ -15,26 +15,30 @@ runCommand opts = do
   s <- embed (readFile (toFilePath file))
   case Asm.runParser (toFilePath file) s of
     Left err -> exitJuvixError (JuvixError err)
-    Right tab -> case run $ runError $ asmToMiniC asmOpts tab of
-      Left err -> exitJuvixError err
-      Right C.MiniCResult {..} -> do
-        buildDir <- askBuildDir
-        ensureDir buildDir
-        cFile <- inputCFile file
-        embed $ TIO.writeFile (toFilePath cFile) _resultCCode
-        Compile.runCommand opts {_compileInputFile = AppPath (Abs cFile) False}
+    Right tab -> do
+      tgt <- asmTarget (opts ^. compileTarget)
+      case run $ runError $ asmToMiniC (asmOpts tgt) tab of
+        Left err -> exitJuvixError err
+        Right C.MiniCResult {..} -> do
+          buildDir <- askBuildDir
+          ensureDir buildDir
+          cFile <- inputCFile file
+          embed $ TIO.writeFile (toFilePath cFile) _resultCCode
+          Compile.runCommand opts {_compileInputFile = AppPath (Abs cFile) False}
   where
     getFile :: Sem r (Path Abs File)
     getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath)
 
-    asmOpts :: Asm.Options
-    asmOpts = Asm.makeOptions (asmTarget (opts ^. compileTarget)) (opts ^. compileDebug)
+    asmOpts :: Backend.Target -> Asm.Options
+    asmOpts tgt = Asm.makeOptions tgt (opts ^. compileDebug)
 
-    asmTarget :: CompileTarget -> Backend.Target
+    asmTarget :: CompileTarget -> Sem r Backend.Target
     asmTarget = \case
-      TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
-      TargetNative64 -> Backend.TargetCNative64
-      TargetGeb -> error "GEB target not supported for JuvixAsm"
+      TargetWasm32Wasi -> return Backend.TargetCWasm32Wasi
+      TargetNative64 -> return Backend.TargetCNative64
+      TargetGeb -> exitMsg (ExitFailure 1) "error: GEB target not supported for JuvixAsm"
+      TargetCore -> exitMsg (ExitFailure 1) "error: JuvixCore target not supported for JuvixAsm"
+      TargetAsm -> exitMsg (ExitFailure 1) "error: JuvixAsm target not supported for JuvixAsm"
 
 inputCFile :: (Members '[App] r) => Path Abs File -> Sem r (Path Abs File)
 inputCFile inputFileCompile = do
diff --git a/app/Commands/Dev/Asm/Compile/Options.hs b/app/Commands/Dev/Asm/Compile/Options.hs
index ddd255eaaf..aa6c0e89df 100644
--- a/app/Commands/Dev/Asm/Compile/Options.hs
+++ b/app/Commands/Dev/Asm/Compile/Options.hs
@@ -10,4 +10,4 @@ import CommonOptions
 type AsmCompileOptions = CompileOptions
 
 parseAsmCompileOptions :: Parser AsmCompileOptions
-parseAsmCompileOptions = parseCompileOptions
+parseAsmCompileOptions = parseCompileOptions parseInputJuvixAsmFile
diff --git a/app/Commands/Dev/Core/Compile.hs b/app/Commands/Dev/Core/Compile.hs
index f4cfb42587..306baad447 100644
--- a/app/Commands/Dev/Core/Compile.hs
+++ b/app/Commands/Dev/Core/Compile.hs
@@ -1,77 +1,23 @@
-module Commands.Dev.Core.Compile (runCommand) where
+module Commands.Dev.Core.Compile where
 
 import Commands.Base
+import Commands.Dev.Core.Compile.Base
 import Commands.Dev.Core.Compile.Options
-import Commands.Extra.Compile qualified as Compile
-import Data.Text.IO qualified as TIO
-import Juvix.Compiler.Asm.Options qualified as Asm
-import Juvix.Compiler.Backend qualified as Backend
-import Juvix.Compiler.Backend.C qualified as C
-import Juvix.Compiler.Backend.Geb qualified as Geb
 import Juvix.Compiler.Core.Data.InfoTable qualified as Core
 import Juvix.Compiler.Core.Translation.FromSource qualified as Core
-import System.FilePath (takeBaseName)
 
-runCommand :: forall r. (Members '[Embed IO, App] r) => CoreCompileOptions -> Sem r ()
+runCommand :: forall r. (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
 runCommand opts = do
   file <- getFile
   s <- embed (readFile (toFilePath file))
   tab <- getRight (mapLeft JuvixError (Core.runParserMain file Core.emptyInfoTable s))
+  let arg = PipelineArg opts file tab
   case opts ^. compileTarget of
-    TargetGeb -> runGebPipeline (PipelineArg opts file tab)
-    TargetWasm32Wasi -> runCPipeline (PipelineArg opts file tab)
-    TargetNative64 -> runCPipeline (PipelineArg opts file tab)
+    TargetWasm32Wasi -> runCPipeline arg
+    TargetNative64 -> runCPipeline arg
+    TargetGeb -> runGebPipeline arg
+    TargetCore -> return ()
+    TargetAsm -> runAsmPipeline arg
   where
     getFile :: Sem r (Path Abs File)
     getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath)
-
-data PipelineArg = PipelineArg
-  { _pipelineArgOptions :: CoreCompileOptions,
-    _pipelineArgFile :: Path Abs File,
-    _pipelineArgInfoTable :: Core.InfoTable
-  }
-
-runCPipeline ::
-  forall r.
-  (Members '[Embed IO, App] r) =>
-  PipelineArg ->
-  Sem r ()
-runCPipeline PipelineArg {..} = do
-  C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts _pipelineArgInfoTable :: Sem '[Error JuvixError] C.MiniCResult)))
-  cFile <- inputCFile _pipelineArgFile
-  embed $ TIO.writeFile (toFilePath cFile) _resultCCode
-  Compile.runCommand _pipelineArgOptions {_compileInputFile = AppPath (Abs cFile) False}
-  where
-    asmOpts :: Asm.Options
-    asmOpts = Asm.makeOptions (asmTarget (_pipelineArgOptions ^. compileTarget)) (_pipelineArgOptions ^. compileDebug)
-
-    asmTarget :: CompileTarget -> Backend.Target
-    asmTarget = \case
-      TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
-      TargetNative64 -> Backend.TargetCNative64
-      TargetGeb -> impossible
-
-    inputCFile :: Path Abs File -> Sem r (Path Abs File)
-    inputCFile inputFileCompile = do
-      buildDir <- askBuildDir
-      ensureDir buildDir
-      return (buildDir <//> replaceExtension' ".c" (filename inputFileCompile))
-
-runGebPipeline ::
-  forall r.
-  (Members '[Embed IO, App] r) =>
-  PipelineArg ->
-  Sem r ()
-runGebPipeline PipelineArg {..} = do
-  gebFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  let spec =
-        if
-            | _pipelineArgOptions ^. compileTerm -> Geb.OnlyTerm
-            | otherwise ->
-                Geb.LispPackage
-                  Geb.LispPackageSpec
-                    { _lispPackageName = fromString $ takeBaseName $ toFilePath gebFile,
-                      _lispPackageEntry = "*entry*"
-                    }
-  Geb.Result {..} <- getRight (run (runError (coreToGeb spec _pipelineArgInfoTable :: Sem '[Error JuvixError] Geb.Result)))
-  embed $ TIO.writeFile (toFilePath gebFile) _resultCode
diff --git a/app/Commands/Dev/Core/Compile/Base.hs b/app/Commands/Dev/Core/Compile/Base.hs
new file mode 100644
index 0000000000..17522679a1
--- /dev/null
+++ b/app/Commands/Dev/Core/Compile/Base.hs
@@ -0,0 +1,78 @@
+module Commands.Dev.Core.Compile.Base where
+
+import Commands.Base
+import Commands.Dev.Core.Compile.Options
+import Commands.Extra.Compile qualified as Compile
+import Data.Text.IO qualified as TIO
+import Juvix.Compiler.Asm.Options qualified as Asm
+import Juvix.Compiler.Asm.Pretty qualified as Pretty
+import Juvix.Compiler.Backend qualified as Backend
+import Juvix.Compiler.Backend.C qualified as C
+import Juvix.Compiler.Backend.Geb qualified as Geb
+import Juvix.Compiler.Core.Data.InfoTable qualified as Core
+import System.FilePath (takeBaseName)
+
+data PipelineArg = PipelineArg
+  { _pipelineArgOptions :: CompileOptions,
+    _pipelineArgFile :: Path Abs File,
+    _pipelineArgInfoTable :: Core.InfoTable
+  }
+
+runCPipeline ::
+  forall r.
+  (Members '[Embed IO, App] r) =>
+  PipelineArg ->
+  Sem r ()
+runCPipeline PipelineArg {..} = do
+  C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts _pipelineArgInfoTable :: Sem '[Error JuvixError] C.MiniCResult)))
+  cFile <- inputCFile _pipelineArgFile
+  embed $ TIO.writeFile (toFilePath cFile) _resultCCode
+  outfile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  Compile.runCommand
+    _pipelineArgOptions
+      { _compileInputFile = AppPath (Abs cFile) False,
+        _compileOutputFile = Just (AppPath (Abs outfile) False)
+      }
+  where
+    asmOpts :: Asm.Options
+    asmOpts = Asm.makeOptions (asmTarget (_pipelineArgOptions ^. compileTarget)) (_pipelineArgOptions ^. compileDebug)
+
+    asmTarget :: CompileTarget -> Backend.Target
+    asmTarget = \case
+      TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
+      TargetNative64 -> Backend.TargetCNative64
+      TargetGeb -> impossible
+      TargetCore -> impossible
+      TargetAsm -> impossible
+
+    inputCFile :: Path Abs File -> Sem r (Path Abs File)
+    inputCFile inputFileCompile = do
+      buildDir <- askBuildDir
+      ensureDir buildDir
+      return (buildDir <//> replaceExtension' ".c" (filename inputFileCompile))
+
+runGebPipeline ::
+  forall r.
+  (Members '[Embed IO, App] r) =>
+  PipelineArg ->
+  Sem r ()
+runGebPipeline PipelineArg {..} = do
+  gebFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  let spec =
+        if
+            | _pipelineArgOptions ^. compileTerm -> Geb.OnlyTerm
+            | otherwise ->
+                Geb.LispPackage
+                  Geb.LispPackageSpec
+                    { _lispPackageName = fromString $ takeBaseName $ toFilePath gebFile,
+                      _lispPackageEntry = "*entry*"
+                    }
+  Geb.Result {..} <- getRight (run (runError (coreToGeb spec _pipelineArgInfoTable :: Sem '[Error JuvixError] Geb.Result)))
+  embed $ TIO.writeFile (toFilePath gebFile) _resultCode
+
+runAsmPipeline :: (Members '[Embed IO, App] r) => PipelineArg -> Sem r ()
+runAsmPipeline PipelineArg {..} = do
+  asmFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  let tab' = coreToAsm _pipelineArgInfoTable
+      code = Pretty.ppPrint tab' tab'
+  embed $ TIO.writeFile (toFilePath asmFile) code
diff --git a/app/Commands/Dev/Core/Compile/Options.hs b/app/Commands/Dev/Core/Compile/Options.hs
index 1f40e5a83f..201040596b 100644
--- a/app/Commands/Dev/Core/Compile/Options.hs
+++ b/app/Commands/Dev/Core/Compile/Options.hs
@@ -1,13 +1,6 @@
 module Commands.Dev.Core.Compile.Options
-  ( module Commands.Dev.Core.Compile.Options,
-    module Commands.Extra.Compile.Options,
+  ( module Commands.Extra.Compile.Options,
   )
 where
 
 import Commands.Extra.Compile.Options
-import CommonOptions
-
-type CoreCompileOptions = CompileOptions
-
-parseCoreCompileOptions :: Parser CoreCompileOptions
-parseCoreCompileOptions = parseCompileOptions
diff --git a/app/Commands/Dev/Core/FromConcrete.hs b/app/Commands/Dev/Core/FromConcrete.hs
index 776b71cf71..18cb68f692 100644
--- a/app/Commands/Dev/Core/FromConcrete.hs
+++ b/app/Commands/Dev/Core/FromConcrete.hs
@@ -15,7 +15,8 @@ runCommand localOpts = do
   let tab' :: InfoTable = Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
 
       inInputModule :: IdentifierInfo -> Bool
-      inInputModule = (== Just path) . (^? identifierLocation . _Just . intervalFile)
+      inInputModule _ | not (localOpts ^. coreFromConcreteFilter) = True
+      inInputModule x = (== Just path) . (^? identifierLocation . _Just . intervalFile) $ x
 
       mainIdens :: [IdentifierInfo] =
         sortOn
diff --git a/app/Commands/Dev/Core/FromConcrete/Options.hs b/app/Commands/Dev/Core/FromConcrete/Options.hs
index e47bff1218..0d43b67d47 100644
--- a/app/Commands/Dev/Core/FromConcrete/Options.hs
+++ b/app/Commands/Dev/Core/FromConcrete/Options.hs
@@ -8,6 +8,7 @@ import Juvix.Compiler.Core.Pretty.Options qualified as Core
 data CoreFromConcreteOptions = CoreFromConcreteOptions
   { _coreFromConcreteTransformations :: [TransformationId],
     _coreFromConcreteShowDeBruijn :: Bool,
+    _coreFromConcreteFilter :: Bool,
     _coreFromConcreteNoIO :: Bool,
     _coreFromConcreteEval :: Bool,
     _coreFromConcreteInputFile :: AppPath File,
@@ -38,6 +39,11 @@ parseCoreFromConcreteOptions = do
       ( long "show-de-bruijn"
           <> help "Show variable de Bruijn indices"
       )
+  _coreFromConcreteFilter <-
+    switch
+      ( long "filter"
+          <> help "Filter out the functions not from the input module"
+      )
   _coreFromConcreteEval <-
     switch
       ( long "eval"
diff --git a/app/Commands/Dev/Core/Options.hs b/app/Commands/Dev/Core/Options.hs
index ed3d74244d..7692197aab 100644
--- a/app/Commands/Dev/Core/Options.hs
+++ b/app/Commands/Dev/Core/Options.hs
@@ -16,7 +16,7 @@ data CoreCommand
   | FromConcrete CoreFromConcreteOptions
   | Strip CoreStripOptions
   | CoreAsm CoreAsmOptions
-  | CoreCompile CoreCompileOptions
+  | CoreCompile CompileOptions
   deriving stock (Data)
 
 parseCoreCommand :: Parser CoreCommand
@@ -92,5 +92,5 @@ parseCoreCommand =
     compileInfo :: ParserInfo CoreCommand
     compileInfo =
       info
-        (CoreCompile <$> parseCoreCompileOptions)
-        (progDesc "Compile a JuvixCore file to native code or WebAssembly")
+        (CoreCompile <$> parseCompileOptions parseInputJuvixCoreFile)
+        (progDesc "Compile a JuvixCore file to native code, WebAssembly or GEB")
diff --git a/app/Commands/Dev/Core/Strip.hs b/app/Commands/Dev/Core/Strip.hs
index e6ed234120..af82182d85 100644
--- a/app/Commands/Dev/Core/Strip.hs
+++ b/app/Commands/Dev/Core/Strip.hs
@@ -11,7 +11,7 @@ runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a Cor
 runCommand opts = do
   inputFile :: Path Abs File <- someBaseToAbs' sinputFile
   s' <- embed (readFile $ toFilePath inputFile)
-  (tab, _) <- getRight (mapLeft JuvixError (Core.runParser inputFile Core.emptyInfoTable s'))
+  tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
   let tab' = Stripped.fromCore (Core.toStripped tab)
   unless (project opts ^. coreStripNoPrint) $ do
     renderStdOut (Core.ppOut opts tab')
diff --git a/app/Commands/Dev/MiniC.hs b/app/Commands/Dev/MiniC.hs
deleted file mode 100644
index e00ddd096e..0000000000
--- a/app/Commands/Dev/MiniC.hs
+++ /dev/null
@@ -1,10 +0,0 @@
-module Commands.Dev.MiniC where
-
-import Commands.Base
-import Commands.Dev.MiniC.Options
-import Juvix.Compiler.Backend.C.Translation.FromInternal qualified as MiniC
-
-runCommand :: (Members '[Embed IO, App] r) => MiniCOptions -> Sem r ()
-runCommand opts = do
-  miniC <- (^. MiniC.resultCCode) <$> runPipeline (opts ^. miniCInputFile) upToMiniC
-  say miniC
diff --git a/app/Commands/Dev/Options.hs b/app/Commands/Dev/Options.hs
index 4aca25ff90..0bee6bd012 100644
--- a/app/Commands/Dev/Options.hs
+++ b/app/Commands/Dev/Options.hs
@@ -18,7 +18,6 @@ import Commands.Dev.DisplayRoot.Options
 import Commands.Dev.Geb.Options
 import Commands.Dev.Highlight.Options
 import Commands.Dev.Internal.Options
-import Commands.Dev.MiniC.Options
 import Commands.Dev.Parse.Options
 import Commands.Dev.Runtime.Options
 import Commands.Dev.Scope.Options
@@ -33,7 +32,6 @@ data DevCommand
   | Geb GebCommand
   | Asm AsmCommand
   | Runtime RuntimeCommand
-  | MiniC MiniCOptions
   | Parse ParseOptions
   | Scope ScopeOptions
   | Termination TerminationCommand
@@ -49,7 +47,6 @@ parseDevCommand =
           commandGeb,
           commandAsm,
           commandRuntime,
-          commandMiniC,
           commandParse,
           commandScope,
           commandShowRoot,
@@ -64,13 +61,6 @@ commandHighlight =
       (Highlight <$> parseHighlight)
       (progDesc "Highlight a Juvix file")
 
-commandMiniC :: Mod CommandFields DevCommand
-commandMiniC =
-  command "minic" $
-    info
-      (MiniC <$> parseMiniC)
-      (progDesc "Translate a Juvix file to MiniC")
-
 commandInternal :: Mod CommandFields DevCommand
 commandInternal =
   command "internal" $
diff --git a/app/Commands/Dev/Runtime/Options.hs b/app/Commands/Dev/Runtime/Options.hs
index a5cc83c8f7..cd7746877b 100644
--- a/app/Commands/Dev/Runtime/Options.hs
+++ b/app/Commands/Dev/Runtime/Options.hs
@@ -20,5 +20,5 @@ parseRuntimeCommand =
     compileInfo :: ParserInfo RuntimeCommand
     compileInfo =
       info
-        (Compile <$> parseCompileOptions)
+        (Compile <$> parseCompileOptions parseInputCFile)
         (progDesc "Compile a C file with Juvix runtime included")
diff --git a/app/Commands/Eval.hs b/app/Commands/Eval.hs
new file mode 100644
index 0000000000..717b490462
--- /dev/null
+++ b/app/Commands/Eval.hs
@@ -0,0 +1,38 @@
+module Commands.Eval where
+
+import Commands.Base
+import Commands.Eval.Options
+import Evaluator qualified as Eval
+import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Core.Data.InfoTable qualified as Core
+import Juvix.Compiler.Core.Language qualified as Core
+import Juvix.Compiler.Core.Pipeline qualified as Core
+
+runCommand :: (Members '[Embed IO, App] r) => EvalOptions -> Sem r ()
+runCommand opts@EvalOptions {..} = do
+  Core.CoreResult {..} <- runPipeline _evalInputFile upToCore
+  let tab = Core.toEval _coreResultTable
+      evalNode =
+        if
+            | isJust (_evalSymbolName) -> getNode' tab (selInfo tab)
+            | otherwise -> getNode' tab (mainInfo tab)
+  Eval.evalAndPrint opts tab evalNode
+  where
+    mainInfo :: Core.InfoTable -> Maybe Core.IdentifierInfo
+    mainInfo tab = do
+      s <- tab ^. Core.infoMain
+      tab ^. Core.infoIdentifiers . at s
+
+    selInfo :: Core.InfoTable -> Maybe Core.IdentifierInfo
+    selInfo tab = do
+      s <- _evalSymbolName
+      find (^. Core.identifierName . to (== s)) (tab ^. Core.infoIdentifiers)
+
+    getNode' :: Core.InfoTable -> Maybe Core.IdentifierInfo -> Core.Node
+    getNode' tab m = fromMaybe err (getNode tab m)
+
+    getNode :: Core.InfoTable -> Maybe Core.IdentifierInfo -> Maybe Core.Node
+    getNode tab m = m >>= \i -> tab ^. Core.identContext . at (i ^. Core.identifierSymbol)
+
+    err :: a
+    err = error "function not found"
diff --git a/app/Commands/Eval/Options.hs b/app/Commands/Eval/Options.hs
new file mode 100644
index 0000000000..958a6104db
--- /dev/null
+++ b/app/Commands/Eval/Options.hs
@@ -0,0 +1,51 @@
+module Commands.Eval.Options where
+
+import CommonOptions
+import Evaluator qualified as Eval
+import Juvix.Compiler.Core.Pretty.Options qualified as Core
+
+data EvalOptions = EvalOptions
+  { _evalShowDeBruijn :: Bool,
+    _evalNoIO :: Bool,
+    _evalInputFile :: AppPath File,
+    _evalSymbolName :: Maybe Text
+  }
+  deriving stock (Data)
+
+makeLenses ''EvalOptions
+
+instance CanonicalProjection EvalOptions Core.Options where
+  project c =
+    Core.defaultOptions
+      { Core._optShowDeBruijnIndices = c ^. evalShowDeBruijn
+      }
+
+instance CanonicalProjection EvalOptions Eval.EvalOptions where
+  project c =
+    Eval.EvalOptions
+      { _evalInputFile = c ^. evalInputFile,
+        _evalNoIO = c ^. evalNoIO
+      }
+
+parseEvalOptions :: Parser EvalOptions
+parseEvalOptions = do
+  _evalShowDeBruijn <-
+    switch
+      ( long "show-de-bruijn"
+          <> help "Show variable de Bruijn indices"
+      )
+  _evalNoIO <-
+    switch
+      ( long "no-io"
+          <> help "Don't interpret the IO effects"
+      )
+  _evalInputFile <- parseInputJuvixFile
+  _evalSymbolName <-
+    optional $
+      strOption
+        ( long "symbol-name"
+            <> short 's'
+            <> help "Evaluate a specific function identifier (default: main)"
+            <> metavar "NAME"
+        )
+  pure EvalOptions {..}
diff --git a/app/Commands/Extra/Compile.hs b/app/Commands/Extra/Compile.hs
index 3bee96c422..c34a02d385 100644
--- a/app/Commands/Extra/Compile.hs
+++ b/app/Commands/Extra/Compile.hs
@@ -30,6 +30,8 @@ runCompile inputFile o = do
     TargetWasm32Wasi -> runError (clangWasmWasiCompile inputFile o)
     TargetNative64 -> runError (clangNativeCompile inputFile o)
     TargetGeb -> return $ Right ()
+    TargetCore -> return $ Right ()
+    TargetAsm -> return $ Right ()
 
 prepareRuntime :: forall r. (Members '[App, Embed IO] r) => Path Abs Dir -> CompileOptions -> Sem r ()
 prepareRuntime buildDir o = do
@@ -40,6 +42,8 @@ prepareRuntime buildDir o = do
     TargetNative64 | o ^. compileDebug -> writeRuntime nativeDebugRuntime
     TargetNative64 -> writeRuntime nativeReleaseRuntime
     TargetGeb -> return ()
+    TargetCore -> return ()
+    TargetAsm -> return ()
   where
     wasiReleaseRuntime :: BS.ByteString
     wasiReleaseRuntime = $(FE.makeRelativeToProject "runtime/_build.wasm32-wasi/libjuvix.a" >>= FE.embedFile)
@@ -75,10 +79,6 @@ outputFile opts inputFile =
   where
     defaultOutputFile :: Path Abs File
     defaultOutputFile = case opts ^. compileTarget of
-      TargetGeb ->
-        if
-            | opts ^. compileTerm -> replaceExtension' ".geb" inputFile
-            | otherwise -> replaceExtension' ".lisp" inputFile
       TargetNative64 ->
         if
             | opts ^. compileCOutput -> replaceExtension' ".c" inputFile
@@ -91,6 +91,14 @@ outputFile opts inputFile =
             | opts ^. compilePreprocess -> addExtension' ".c" (addExtension' ".out" (removeExtension' inputFile))
             | opts ^. compileAssembly -> replaceExtension' ".wat" inputFile
             | otherwise -> replaceExtension' ".wasm" inputFile
+      TargetGeb ->
+        if
+            | opts ^. compileTerm -> replaceExtension' ".geb" inputFile
+            | otherwise -> replaceExtension' ".lisp" inputFile
+      TargetCore ->
+        replaceExtension' ".jvc" inputFile
+      TargetAsm ->
+        replaceExtension' ".jva" inputFile
 
 clangNativeCompile ::
   forall r.
diff --git a/app/Commands/Extra/Compile/Options.hs b/app/Commands/Extra/Compile/Options.hs
index f8e580bda4..4d968862d8 100644
--- a/app/Commands/Extra/Compile/Options.hs
+++ b/app/Commands/Extra/Compile/Options.hs
@@ -7,6 +7,8 @@ data CompileTarget
   = TargetWasm32Wasi
   | TargetNative64
   | TargetGeb
+  | TargetCore
+  | TargetAsm
   deriving stock (Data, Bounded, Enum)
 
 instance Show CompileTarget where
@@ -14,6 +16,8 @@ instance Show CompileTarget where
     TargetWasm32Wasi -> "wasm32-wasi"
     TargetNative64 -> "native"
     TargetGeb -> "geb"
+    TargetCore -> "core"
+    TargetAsm -> "asm"
 
 data CompileOptions = CompileOptions
   { _compileDebug :: Bool,
@@ -29,8 +33,8 @@ data CompileOptions = CompileOptions
 
 makeLenses ''CompileOptions
 
-parseCompileOptions :: Parser CompileOptions
-parseCompileOptions = do
+parseCompileOptions :: Parser (AppPath File) -> Parser CompileOptions
+parseCompileOptions parseInputFile = do
   _compileDebug <-
     switch
       ( short 'g'
@@ -63,7 +67,7 @@ parseCompileOptions = do
       )
   _compileTarget <- optCompileTarget
   _compileOutputFile <- optional parseGenericOutputFile
-  _compileInputFile <- parseGenericInputFile
+  _compileInputFile <- parseInputFile
   pure CompileOptions {..}
 
 optCompileTarget :: Parser CompileTarget
diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs
index beb69b3bbd..d90632e9ba 100644
--- a/app/Commands/Repl.hs
+++ b/app/Commands/Repl.hs
@@ -171,21 +171,19 @@ runCommand opts = do
           defaultLoc = singletonInterval (mkInitialLoc replPath)
 
           compileThenEval :: ReplContext -> String -> Repl (Either JuvixError Core.Node)
-          compileThenEval ctx s = bindEither (fmap transformNode' <$> compileString) eval
+          compileThenEval ctx s = bindEither compileString eval
             where
               eval :: Core.Node -> Repl (Either JuvixError Core.Node)
               eval n =
-                liftIO $
-                  mapLeft
-                    (JuvixError @Core.CoreError)
-                    <$> doEvalIO False defaultLoc infoTable n
+                let (tab', n') = runTransformations (Core.toEvalTransformations ++ opts ^. replTransformations) infoTable n
+                 in liftIO $
+                      mapLeft
+                        (JuvixError @Core.CoreError)
+                        <$> doEvalIO False defaultLoc tab' n'
 
               infoTable :: Core.InfoTable
               infoTable = ctx ^. replContextExpContext . contextCoreResult . Core.coreResultTable
 
-              transformNode' :: Core.Node -> Core.Node
-              transformNode' = transformNode infoTable (opts ^. replTransformations)
-
               compileString :: Repl (Either JuvixError Core.Node)
               compileString = liftIO $ compileExpressionIO' ctx (strip (pack s))
 
diff --git a/app/CommonOptions.hs b/app/CommonOptions.hs
index dafa6cee33..fd68ac5b57 100644
--- a/app/CommonOptions.hs
+++ b/app/CommonOptions.hs
@@ -240,7 +240,7 @@ optTransformationIds =
     (eitherReader parseTransf)
     ( long "transforms"
         <> short 't'
-        <> value mempty
+        <> value []
         <> metavar "[Transform]"
         <> completer (mkCompleter (return . completionsString))
         <> help "hint: use autocomplete"
diff --git a/app/TopCommand.hs b/app/TopCommand.hs
index 941cfddcb0..9c39111bb0 100644
--- a/app/TopCommand.hs
+++ b/app/TopCommand.hs
@@ -4,6 +4,7 @@ import Commands.Base
 import Commands.Compile qualified as Compile
 import Commands.Dev qualified as Dev
 import Commands.Doctor qualified as Doctor
+import Commands.Eval qualified as Eval
 import Commands.Html qualified as Html
 import Commands.Init qualified as Init
 import Commands.Repl qualified as Repl
@@ -29,5 +30,6 @@ runTopCommand = \case
   Dev opts -> Dev.runCommand opts
   Typecheck opts -> Typecheck.runCommand opts
   Compile opts -> Compile.runCommand opts
+  Eval opts -> Eval.runCommand opts
   Html opts -> Html.runCommand opts
   JuvixRepl opts -> Repl.runCommand opts
diff --git a/app/TopCommand/Options.hs b/app/TopCommand/Options.hs
index 1b9355a06b..40713fa5ff 100644
--- a/app/TopCommand/Options.hs
+++ b/app/TopCommand/Options.hs
@@ -1,8 +1,9 @@
 module TopCommand.Options where
 
 import Commands.Compile.Options
-import Commands.Dev.Options
+import Commands.Dev.Options qualified as Dev
 import Commands.Doctor.Options
+import Commands.Eval.Options
 import Commands.Html.Options
 import Commands.Repl.Options
 import Commands.Typecheck.Options
@@ -16,8 +17,9 @@ data TopCommand
   | DisplayHelp
   | Typecheck TypecheckOptions
   | Compile CompileOptions
+  | Eval EvalOptions
   | Html HtmlOptions
-  | Dev DevCommand
+  | Dev Dev.DevCommand
   | Doctor DoctorOptions
   | Init
   | JuvixRepl ReplOptions
@@ -98,9 +100,16 @@ commandCompile :: Mod CommandFields TopCommand
 commandCompile =
   command "compile" $
     info
-      (Compile <$> parseCompile)
+      (Compile <$> parseCompileOptions parseInputJuvixFile)
       (progDesc "Compile a Juvix file")
 
+commandEval :: Mod CommandFields TopCommand
+commandEval =
+  command "eval" $
+    info
+      (Eval <$> parseEvalOptions)
+      (progDesc "Evaluate a Juvix file")
+
 commandHtml :: Mod CommandFields TopCommand
 commandHtml =
   command "html" $
@@ -112,7 +121,7 @@ commandDev :: Mod CommandFields TopCommand
 commandDev =
   command "dev" $
     info
-      (Dev <$> parseDevCommand)
+      (Dev <$> Dev.parseDevCommand)
       (progDesc "Commands for the developers")
 
 parseCompilerCommand :: Parser TopCommand
@@ -123,6 +132,7 @@ parseCompilerCommand =
           metavar "COMPILER_CMD",
           commandCheck,
           commandCompile,
+          commandEval,
           commandHtml
         ]
     )
diff --git a/juvix-stdlib b/juvix-stdlib
index 3a7d37febd..402ffe1f23 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 3a7d37febd078380032d409531123c9436256b86
+Subproject commit 402ffe1f232c77ee8fe49ad645dfbfc8451f046a
diff --git a/package.yaml b/package.yaml
index d2297b8ca4..248a30cf7a 100644
--- a/package.yaml
+++ b/package.yaml
@@ -66,6 +66,7 @@ dependencies:
 - uniplate == 1.6.*
 - unix-compat == 0.5.*
 - unordered-containers == 0.2.*
+- utf8-string == 1.0.*
 - versions == 5.0.*
 - yaml == 0.11.*
 
diff --git a/src/Juvix/Compiler/Asm/Extra/Base.hs b/src/Juvix/Compiler/Asm/Extra/Base.hs
index 400155c392..f13c178620 100644
--- a/src/Juvix/Compiler/Asm/Extra/Base.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Base.hs
@@ -30,7 +30,7 @@ isFinalInstr = \case
   Return -> True
   TailCall {} -> True
   TailCallClosures {} -> True
-  Failure -> True
+  Failure {} -> False
   _ -> False
 
 getConstrSize :: MemRep -> Int -> Int
diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs
index 8c97dad9ba..8563d88fb1 100644
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs
@@ -146,7 +146,7 @@ checkValueStack' loc tab tys mem = do
   mapM_
     ( \(ty, idx) -> do
         let ty' = fromJust $ topValueStack idx mem
-        unless (isSubtype ty' ty) $
+        unless (isSubtype' ty' ty) $
           throw $
             AsmError loc $
               "type mismatch on value stack cell "
diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
index 76e81d38b0..e17bfa1ce5 100644
--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
@@ -187,7 +187,8 @@ recurse' sig = go True
           let argsNum = case _callType of
                 CallClosure -> length (typeArgs ty)
                 CallFun sym -> getFunInfo (sig ^. recursorInfoTable) sym ^. functionArgsNum
-          checkFunType ty
+          when (argsNum /= 0) $
+            checkFunType ty
           when (ty /= TyDynamic && argsNum /= _callArgsNum) $
             throw $
               AsmError loc "invalid call: the number of supplied arguments doesn't match the number of expected arguments"
diff --git a/src/Juvix/Compiler/Asm/Extra/Type.hs b/src/Juvix/Compiler/Asm/Extra/Type.hs
index 06d274e2b7..951cbc19bf 100644
--- a/src/Juvix/Compiler/Asm/Extra/Type.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Type.hs
@@ -112,12 +112,8 @@ unifyTypes' loc tab ty1 ty2 =
       -- The `if` is to ensure correct behaviour with dynamic type targets. E.g.
       -- `(A, B) -> *` should unify with `A -> B -> C -> D`.
       if
-          | tgt1 == TyDynamic && tgt2 == TyDynamic ->
+          | tgt1 == TyDynamic || tgt2 == TyDynamic ->
               unifyTypes (curryType ty1) (curryType ty2)
-          | tgt1 == TyDynamic ->
-              unifyTypes (uncurryType ty1) ty2
-          | tgt2 == TyDynamic ->
-              unifyTypes ty1 (uncurryType ty2)
           | otherwise ->
               unifyTypes ty1 ty2
   where
@@ -166,3 +162,17 @@ isSubtype ty1 ty2 = case (ty1, ty2) of
   (TyFun {}, _) -> False
   (_, TyFun {}) -> False
   (_, TyConstr {}) -> False
+
+isSubtype' :: Type -> Type -> Bool
+isSubtype' ty1 ty2
+  -- The guard is to ensure correct behaviour with dynamic type targets. E.g.
+  -- `A -> B -> C -> D` should be a subtype of `(A, B) -> *`.
+  | tgt1 == TyDynamic || tgt2 == TyDynamic =
+      isSubtype
+        (curryType ty1)
+        (curryType ty2)
+  where
+    tgt1 = typeTarget (uncurryType ty1)
+    tgt2 = typeTarget (uncurryType ty2)
+isSubtype' ty1 ty2 =
+  isSubtype ty1 ty2
diff --git a/src/Juvix/Compiler/Asm/Pretty/Base.hs b/src/Juvix/Compiler/Asm/Pretty/Base.hs
index 4deb9d2a9e..4c852105eb 100644
--- a/src/Juvix/Compiler/Asm/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Asm/Pretty/Base.hs
@@ -7,6 +7,7 @@ where
 import Data.Foldable
 import Data.HashMap.Strict qualified as HashMap
 import Data.List.NonEmpty qualified as NonEmpty
+import Data.Text qualified as Text
 import Juvix.Compiler.Abstract.Data.Name
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Extra.Base
@@ -36,20 +37,29 @@ wrapCore f c = do
   opts <- ask
   return $ run $ runReader (toCoreOptions opts) $ f c
 
+quoteAsmName :: Text -> Text
+quoteAsmName txt =
+  foldr
+    (uncurry Text.replace)
+    txt
+    [ ("$", "__dollar__"),
+      (":", "__colon__")
+    ]
+
 ppConstrName :: (Member (Reader Options) r) => Tag -> Sem r (Doc Ann)
 ppConstrName tag = do
   opts <- ask
   let tab = opts ^. optInfoTable
   maybe
     (wrapCore Core.ppCode tag)
-    (\ci -> return $ annotate (AnnKind KNameConstructor) (pretty (ci ^. constructorName)))
+    (\ci -> return $ annotate (AnnKind KNameConstructor) (pretty (quoteAsmName (ci ^. constructorName))))
     (HashMap.lookup tag (tab ^. infoConstrs))
 
 ppIndName :: (Member (Reader Options) r) => Symbol -> Sem r (Doc Ann)
 ppIndName sym = do
   opts <- ask
   let ci = fromMaybe impossible $ HashMap.lookup sym (opts ^. optInfoTable . infoInductives)
-  return $ annotate (AnnKind KNameInductive) (pretty (ci ^. inductiveName))
+  return $ annotate (AnnKind KNameInductive) (pretty (quoteAsmName (ci ^. inductiveName)))
 
 ppFunName :: (Member (Reader Options) r) => Symbol -> Sem r (Doc Ann)
 ppFunName sym = do
@@ -60,7 +70,7 @@ ppFunName sym = do
         annotate (AnnKind KNameFunction) $
           pretty ("unnamed_function_" ++ show sym :: String)
     )
-    (\fi -> return $ annotate (AnnKind KNameFunction) (pretty (fi ^. functionName)))
+    (\fi -> return $ annotate (AnnKind KNameFunction) (pretty (quoteAsmName (fi ^. functionName))))
     (HashMap.lookup sym (tab ^. infoFunctions))
 
 instance PrettyCode BuiltinDataTag where
@@ -344,7 +354,7 @@ ppFunSig FunctionInfo {..} = do
   targetty <- ppCode (typeTarget _functionType)
   return $
     keyword Str.function
-      <+> annotate (AnnKind KNameFunction) (pretty _functionName)
+      <+> annotate (AnnKind KNameFunction) (pretty (quoteAsmName _functionName))
         <> encloseSep lparen rparen ", " argtys
       <+> colon
       <+> targetty
@@ -353,19 +363,29 @@ ppFunSig FunctionInfo {..} = do
 instance PrettyCode ConstructorInfo where
   ppCode ConstructorInfo {..} = do
     ty <- ppCode _constructorType
-    return $ annotate (AnnKind KNameConstructor) (pretty _constructorName) <+> colon <+> ty
+    return $ annotate (AnnKind KNameConstructor) (pretty (quoteAsmName _constructorName)) <+> colon <+> ty
 
 instance PrettyCode InductiveInfo where
   ppCode InductiveInfo {..} = do
     ctrs <- mapM ppCode _inductiveConstructors
-    return $ kwInductive <+> annotate (AnnKind KNameInductive) (pretty _inductiveName) <+> braces' (vcat (map (<> semi) ctrs))
+    return $ kwInductive <+> annotate (AnnKind KNameInductive) (pretty (quoteAsmName _inductiveName)) <+> braces' (vcat (map (<> semi) ctrs))
 
 instance PrettyCode InfoTable where
   ppCode InfoTable {..} = do
-    inds <- mapM ppCode (HashMap.elems _infoInductives)
+    inds <- mapM ppCode (HashMap.elems (filterOutBuiltins _infoInductives))
     funsigs <- mapM ppFunSig (HashMap.elems _infoFunctions)
     funs <- mapM ppCode (HashMap.elems _infoFunctions)
     return $ vcat (map (<> line) inds) <> line <> vcat funsigs <> line <> line <> vcat (map (<> line) funs)
+    where
+      filterOutBuiltins :: HashMap Symbol InductiveInfo -> HashMap Symbol InductiveInfo
+      filterOutBuiltins =
+        HashMap.filter
+          ( \ii -> case ii ^. inductiveConstructors of
+              ci : _ -> case ci ^. constructorTag of
+                BuiltinTag _ -> False
+                UserTag _ -> True
+              [] -> True
+          )
 
 {--------------------------------------------------------------------------------}
 {- helper functions -}
diff --git a/src/Juvix/Compiler/Asm/Translation/FromCore.hs b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
index 205521cebc..b177157e1b 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
@@ -8,7 +8,6 @@ import Juvix.Compiler.Asm.Extra.Type
 import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Core
-import Juvix.Compiler.Core.Extra.Stripped.Base qualified as Core
 import Juvix.Compiler.Core.Language.Stripped qualified as Core
 
 type BinderList = BL.BinderList
@@ -60,6 +59,7 @@ genCode infoTable fi =
       Core.NCtr ctr -> goConstr isTail tempSize refs ctr
       Core.NLet lt -> goLet isTail tempSize refs lt
       Core.NCase c -> goCase isTail tempSize refs c
+      Core.NIf x -> goIf isTail tempSize refs x
 
     goVar :: Bool -> BinderList Value -> Core.Var -> Code'
     goVar isTail refs Core.Var {..} =
@@ -132,6 +132,7 @@ genCode infoTable fi =
                     (mkInstr $ Push (BL.lookup _varIndex refs))
                 )
                 (mkInstr $ (if isTail then TailCallClosures else CallClosures) (InstrCallClosures suppliedArgsNum))
+
     goBuiltinApp :: Bool -> Int -> BinderList Value -> Core.BuiltinApp -> Code'
     goBuiltinApp isTail tempSize refs (Core.BuiltinApp {..}) =
       snocReturn isTail $
@@ -165,50 +166,17 @@ genCode infoTable fi =
 
     goCase :: Bool -> Int -> BinderList Value -> Core.Case -> Code'
     goCase isTail tempSize refs (Core.Case {..}) =
-      case _caseBranches of
-        [br@Core.CaseBranch {..}]
-          | _caseBranchTag == Core.BuiltinTag Core.TagTrue ->
-              compileIf _caseValue (br ^. Core.caseBranchBody) (fromMaybe branchFailure _caseDefault)
-        [br@Core.CaseBranch {..}]
-          | _caseBranchTag == Core.BuiltinTag Core.TagFalse ->
-              compileIf _caseValue (fromMaybe branchFailure _caseDefault) (br ^. Core.caseBranchBody)
-        [br1, br2]
-          | br1 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagTrue
-              && br2 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagFalse ->
-              compileIf _caseValue (br1 ^. Core.caseBranchBody) (br2 ^. Core.caseBranchBody)
-          | br1 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagFalse
-              && br2 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagTrue ->
-              compileIf _caseValue (br2 ^. Core.caseBranchBody) (br1 ^. Core.caseBranchBody)
-        _ ->
-          DL.snoc
-            (go False tempSize refs _caseValue)
-            ( Case $
-                CmdCase
-                  { _cmdCaseInfo = emptyInfo,
-                    _cmdCaseInductive = _caseInductive,
-                    _cmdCaseBranches = compileCaseBranches _caseBranches,
-                    _cmdCaseDefault = fmap compileCaseDefault _caseDefault
-                  }
-            )
+      DL.snoc
+        (go False tempSize refs _caseValue)
+        ( Case $
+            CmdCase
+              { _cmdCaseInfo = emptyInfo,
+                _cmdCaseInductive = _caseInductive,
+                _cmdCaseBranches = compileCaseBranches _caseBranches,
+                _cmdCaseDefault = fmap compileCaseDefault _caseDefault
+              }
+        )
       where
-        compileIf :: Core.Node -> Core.Node -> Core.Node -> Code'
-        compileIf value br1 br2 =
-          DL.snoc
-            (go False tempSize refs value)
-            ( Branch $
-                CmdBranch
-                  { _cmdBranchInfo = emptyInfo,
-                    _cmdBranchTrue = DL.toList $ go isTail tempSize refs br1,
-                    _cmdBranchFalse = DL.toList $ go isTail tempSize refs br2
-                  }
-            )
-
-        branchFailure :: Core.Node
-        branchFailure =
-          Core.mkBuiltinApp
-            Core.OpFail
-            [Core.mkConstant (Core.ConstString "illegal `if` branch")]
-
         compileCaseBranches :: [Core.CaseBranch] -> [CaseBranch]
         compileCaseBranches branches =
           map
@@ -256,6 +224,18 @@ genCode infoTable fi =
             . DL.cons (mkInstr Pop)
             . go isTail tempSize refs
 
+    goIf :: Bool -> Int -> BinderList Value -> Core.If -> Code'
+    goIf isTail tempSize refs (Core.If {..}) =
+      DL.snoc
+        (go False tempSize refs _ifValue)
+        ( Branch $
+            CmdBranch
+              { _cmdBranchInfo = emptyInfo,
+                _cmdBranchTrue = DL.toList $ go isTail tempSize refs _ifTrue,
+                _cmdBranchFalse = DL.toList $ go isTail tempSize refs _ifFalse
+              }
+        )
+
     genOp :: Core.BuiltinOp -> Command
     genOp = \case
       Core.OpIntAdd -> mkBinop IntAdd
diff --git a/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs b/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs
index 4986fc0adf..0bd6d68334 100644
--- a/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs
+++ b/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs
@@ -1,5 +1,6 @@
 module Juvix.Compiler.Backend.C.Extra.Serialization where
 
+import Codec.Binary.UTF8.String qualified as UTF8
 import Juvix.Compiler.Backend.C.Language
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude hiding (Binary, Unary)
@@ -157,7 +158,7 @@ mkCExpr = \case
   ExpressionLiteral l -> case l of
     LiteralInt i -> CConst (CIntConst (cInteger i) C.undefNode)
     LiteralChar c -> CConst (CCharConst (cChar c) C.undefNode)
-    LiteralString s -> CConst (CStrConst (cString (unpack s)) C.undefNode)
+    LiteralString s -> CConst (CStrConst (cString (UTF8.encodeString (unpack s))) C.undefNode)
   ExpressionVar n -> CVar (mkIdent n) C.undefNode
   ExpressionBinary Binary {..} ->
     CBinary (mkBinaryOp _binaryOp) (mkCExpr _binaryLeft) (mkCExpr _binaryRight) C.undefNode
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index b3c10075eb..42d2199eb6 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -126,3 +126,20 @@ instance Pretty BuiltinAxiom where
     BuiltinIOReadline -> Str.ioReadline
     BuiltinTrace -> Str.trace_
     BuiltinFail -> Str.fail_
+
+data BuiltinType
+  = BuiltinTypeInductive BuiltinInductive
+  | BuiltinTypeAxiom BuiltinAxiom
+  deriving stock (Show, Eq, Ord, Generic, Data)
+
+instance Hashable BuiltinType
+
+instance Pretty BuiltinType where
+  pretty = \case
+    BuiltinTypeInductive ty -> pretty ty
+    BuiltinTypeAxiom ax -> pretty ax
+
+builtinTypeToPrim :: BuiltinType -> BuiltinPrim
+builtinTypeToPrim = \case
+  BuiltinTypeInductive b -> BuiltinsInductive b
+  BuiltinTypeAxiom b -> BuiltinsAxiom b
diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs
index 81cc71f4e9..26c5e90ed7 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@@ -72,7 +72,7 @@ data InductiveInfo = InductiveInfo
     _inductiveConstructors :: [ConstructorInfo],
     _inductiveParams :: [ParameterInfo],
     _inductivePositive :: Bool,
-    _inductiveBuiltin :: Maybe BuiltinInductive
+    _inductiveBuiltin :: Maybe BuiltinType
   }
 
 data ConstructorInfo = ConstructorInfo
diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
index daaf2d0f7b..40a751dc84 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@@ -39,6 +39,16 @@ getBoolSymbol = do
   ci <- getConstructorInfo (BuiltinTag TagTrue)
   return $ ci ^. constructorInductive
 
+getIOSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getIOSymbol = do
+  ci <- getConstructorInfo (BuiltinTag TagWrite)
+  return $ ci ^. constructorInductive
+
+getNatSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getNatSymbol = do
+  tab <- getInfoTable
+  return $ fromJust (lookupBuiltinInductive tab BuiltinNat) ^. inductiveSymbol
+
 checkSymbolDefined :: (Member InfoTableBuilder r) => Symbol -> Sem r Bool
 checkSymbolDefined sym = do
   tab <- getInfoTable
@@ -83,7 +93,7 @@ runInfoTableBuilder tab =
         let identKind = IdentInd sym
         whenJust
           (ii ^. inductiveBuiltin)
-          (\b -> modify' (over infoBuiltins (HashMap.insert (BuiltinsInductive b) identKind)))
+          (\b -> modify' (over infoBuiltins (HashMap.insert (builtinTypeToPrim b) identKind)))
         modify' (over infoInductives (HashMap.insert sym ii))
         modify' (over identMap (HashMap.insert idt identKind))
       RegisterIdentNode sym node ->
@@ -111,29 +121,36 @@ createBuiltinConstr ::
   Text ->
   Type ->
   Maybe BuiltinConstructor ->
-  Sem r ConstructorInfo
-createBuiltinConstr sym tag nameTxt ty cblt = do
-  return $
-    ConstructorInfo
-      { _constructorName = nameTxt,
-        _constructorLocation = Nothing,
-        _constructorTag = tag,
-        _constructorType = ty,
-        _constructorArgsNum = length (typeArgs ty),
-        _constructorInductive = sym,
-        _constructorBuiltin = cblt
-      }
+  ConstructorInfo
+createBuiltinConstr sym tag nameTxt ty cblt =
+  ConstructorInfo
+    { _constructorName = nameTxt,
+      _constructorLocation = Nothing,
+      _constructorTag = tag,
+      _constructorType = ty,
+      _constructorArgsNum = length (typeArgs ty),
+      _constructorInductive = sym,
+      _constructorBuiltin = cblt
+    }
+
+builtinConstrs ::
+  Symbol ->
+  Type ->
+  [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
+  [ConstructorInfo]
+builtinConstrs sym ty ctrs =
+  map (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) cblt) ctrs
 
 declareInductiveBuiltins ::
   (Member InfoTableBuilder r) =>
   Text ->
-  Maybe BuiltinInductive ->
+  Maybe BuiltinType ->
   [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
   Sem r ()
 declareInductiveBuiltins indName blt ctrs = do
   sym <- freshSymbol
   let ty = mkTypeConstr' sym []
-  constrs <- mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) cblt) ctrs
+      constrs = builtinConstrs sym ty ctrs
   registerInductive
     indName
     ( InductiveInfo
@@ -149,22 +166,26 @@ declareInductiveBuiltins indName blt ctrs = do
     )
   mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs
 
+builtinIOConstrs :: [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)]
+builtinIOConstrs =
+  [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
+    (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
+    (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
+    (BuiltinTag TagReadLn, "readLn", id, Nothing)
+  ]
+
 declareIOBuiltins :: (Member InfoTableBuilder r) => Sem r ()
 declareIOBuiltins =
   declareInductiveBuiltins
     "IO"
-    Nothing
-    [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
-      (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
-      (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
-      (BuiltinTag TagReadLn, "readLn", id, Nothing)
-    ]
+    (Just (BuiltinTypeAxiom BuiltinIO))
+    builtinIOConstrs
 
 declareBoolBuiltins :: (Member InfoTableBuilder r) => Sem r ()
 declareBoolBuiltins =
   declareInductiveBuiltins
     "bool"
-    (Just BuiltinBool)
+    (Just (BuiltinTypeInductive BuiltinBool))
     [ (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue),
       (BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse)
     ]
@@ -175,7 +196,7 @@ declareNatBuiltins = do
   tagSuc <- freshTag
   declareInductiveBuiltins
     "nat"
-    (Just BuiltinNat)
+    (Just (BuiltinTypeInductive BuiltinNat))
     [ (tagZero, "zero", id, Just BuiltinNatZero),
       (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
     ]
diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index 218b40e73e..724f805e1e 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -14,4 +14,45 @@ data TransformationId
   | UnrollRecursion
   | ComputeTypeInfo
   | MatchToCase
+  | EtaExpandApps
+  deriving stock (Data, Bounded, Enum)
+
+data PipelineId
+  = PipelineEval
+  | PipelineGeb
+  | PipelineStripped
+  deriving stock (Data, Bounded, Enum)
+
+data TransformationLikeId
+  = TransformationId TransformationId
+  | PipelineId PipelineId
   deriving stock (Data)
+
+allTransformationLikeIds :: [TransformationLikeId]
+allTransformationLikeIds =
+  map TransformationId allElements
+    ++ map PipelineId allElements
+
+fromTransformationLike :: TransformationLikeId -> [TransformationId]
+fromTransformationLike = \case
+  TransformationId i -> [i]
+  PipelineId p -> pipeline p
+
+fromTransformationLikes :: [TransformationLikeId] -> [TransformationId]
+fromTransformationLikes = concatMap fromTransformationLike
+
+toStrippedTransformations :: [TransformationId]
+toStrippedTransformations =
+  toEvalTransformations ++ [LambdaLetRecLifting, TopEtaExpand, MoveApps, RemoveTypeArgs]
+
+toGebTransformations :: [TransformationId]
+toGebTransformations = toEvalTransformations ++ [UnrollRecursion, ComputeTypeInfo]
+
+toEvalTransformations :: [TransformationId]
+toEvalTransformations = [EtaExpandApps, MatchToCase, NatToInt, ConvertBuiltinTypes]
+
+pipeline :: PipelineId -> [TransformationId]
+pipeline = \case
+  PipelineEval -> toEvalTransformations
+  PipelineGeb -> toGebTransformations
+  PipelineStripped -> toStrippedTransformations
diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
index eff505185a..02c8d3b760 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -14,7 +14,7 @@ parseHelper p t = case runParser p "<input>" t of
   Right r -> return r
 
 parseTransformations :: Text -> Either Text [TransformationId]
-parseTransformations = parseHelper transformations
+parseTransformations = fmap fromTransformationLikes . parseHelper transformations
 
 completionsString :: String -> [String]
 completionsString = map unpack . completions . pack
@@ -22,36 +22,23 @@ completionsString = map unpack . completions . pack
 completions :: Text -> [Text]
 completions = fromRight [] . parseHelper pcompletions
 
-transformations :: (MonadParsec e Text m) => m [TransformationId]
+transformations :: (MonadParsec e Text m) => m [TransformationLikeId]
 transformations = do
   L.hspace
-  sepEndBy transformation comma <* eof
+  sepEndBy transformationLike comma <* eof
 
 -- | returns a possible list of completions
 pcompletions :: (MonadParsec e Text m) => m [Text]
 pcompletions = do
   L.hspace
-  l <- sepEndBy transformation comma
+  l <- sepEndBy transformationLike comma
   rest <- Text.strip <$> takeRest
   return [ppTransL (notNull l) l <> str | str <- allStrings, Text.isPrefixOf rest str]
   where
-    ppTransL :: Bool -> [TransformationId] -> Text
+    ppTransL :: Bool -> [TransformationLikeId] -> Text
     ppTransL c =
       let f :: Text -> Text = if c then (<> ",") else id
-       in f . Text.intercalate "," . map ppTrans
-    ppTrans :: TransformationId -> Text
-    ppTrans = \case
-      LambdaLetRecLifting -> strLifting
-      LetRecLifting -> strLetRecLifting
-      TopEtaExpand -> strTopEtaExpand
-      MatchToCase -> strMatchToCase
-      Identity -> strIdentity
-      RemoveTypeArgs -> strRemoveTypeArgs
-      MoveApps -> strMoveApps
-      NatToInt -> strNatToInt
-      ConvertBuiltinTypes -> strConvertBuiltinTypes
-      ComputeTypeInfo -> strComputeTypeInfo
-      UnrollRecursion -> strUnrollRecursion
+       in f . Text.intercalate "," . map transformationLikeText
 
 lexeme :: (MonadParsec e Text m) => m a -> m a
 lexeme = L.lexeme L.hspace
@@ -62,33 +49,54 @@ comma = symbol ","
 symbol :: (MonadParsec e Text m) => Text -> m ()
 symbol = void . lexeme . chunk
 
-transformation :: (MonadParsec e Text m) => m TransformationId
-transformation =
-  symbol strLifting $> LambdaLetRecLifting
-    <|> symbol strLetRecLifting $> LetRecLifting
-    <|> symbol strIdentity $> Identity
-    <|> symbol strTopEtaExpand $> TopEtaExpand
-    <|> symbol strRemoveTypeArgs $> RemoveTypeArgs
-    <|> symbol strMoveApps $> MoveApps
-    <|> symbol strNatToInt $> NatToInt
-    <|> symbol strConvertBuiltinTypes $> ConvertBuiltinTypes
-    <|> symbol strUnrollRecursion $> UnrollRecursion
-    <|> symbol strComputeTypeInfo $> ComputeTypeInfo
-    <|> symbol strMatchToCase $> MatchToCase
+transformationLike :: MonadParsec e Text m => m TransformationLikeId
+transformationLike =
+  TransformationId <$> transformation
+    <|> PipelineId <$> parsePipeline
+
+pipelineText :: PipelineId -> Text
+pipelineText = \case
+  PipelineEval -> strEvalPipeline
+  PipelineGeb -> strGebPipeline
+  PipelineStripped -> strStrippedPipeline
+
+transformationLikeText :: TransformationLikeId -> Text
+transformationLikeText = \case
+  TransformationId t -> transformationText t
+  PipelineId p -> pipelineText p
+
+transformationText :: TransformationId -> Text
+transformationText = \case
+  LambdaLetRecLifting -> strLifting
+  LetRecLifting -> strLetRecLifting
+  TopEtaExpand -> strTopEtaExpand
+  MatchToCase -> strMatchToCase
+  EtaExpandApps -> strEtaExpandApps
+  Identity -> strIdentity
+  RemoveTypeArgs -> strRemoveTypeArgs
+  MoveApps -> strMoveApps
+  NatToInt -> strNatToInt
+  ConvertBuiltinTypes -> strConvertBuiltinTypes
+  ComputeTypeInfo -> strComputeTypeInfo
+  UnrollRecursion -> strUnrollRecursion
+
+parsePipeline :: MonadParsec e Text m => m PipelineId
+parsePipeline = choice [symbol (pipelineText t) $> t | t <- allElements]
+
+transformation :: MonadParsec e Text m => m TransformationId
+transformation = choice [symbol (transformationText t) $> t | t <- allElements]
 
 allStrings :: [Text]
-allStrings =
-  [ strLifting,
-    strTopEtaExpand,
-    strIdentity,
-    strRemoveTypeArgs,
-    strMoveApps,
-    strNatToInt,
-    strConvertBuiltinTypes,
-    strUnrollRecursion,
-    strComputeTypeInfo,
-    strMatchToCase
-  ]
+allStrings = map transformationLikeText allTransformationLikeIds
+
+strEvalPipeline :: Text
+strEvalPipeline = "pipeline-eval"
+
+strGebPipeline :: Text
+strGebPipeline = "pipeline-geb"
+
+strStrippedPipeline :: Text
+strStrippedPipeline = "pipeline-stripped"
 
 strLifting :: Text
 strLifting = "lifting"
@@ -102,6 +110,9 @@ strTopEtaExpand = "top-eta-expand"
 strMatchToCase :: Text
 strMatchToCase = "match-to-case"
 
+strEtaExpandApps :: Text
+strEtaExpandApps = "eta-expand-apps"
+
 strIdentity :: Text
 strIdentity = "identity"
 
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 3c54744536..427af7fe3d 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -75,7 +75,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
         case eval' env v of
           NCtr (Constr _ tag args) -> branch n env args tag def bs
           v' -> evalError "matching on non-data" (substEnv env (mkCase i sym v' bs def))
-      NMatch (Match _ vs bs) ->
+      NMatch (Match _ _ _ vs bs) ->
         let !vs' = map' (eval' env) (toList vs)
          in match n env vs' bs
       NPi {} -> substEnv env n
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 112d600fcb..2c69c49e86 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -5,6 +5,7 @@ module Juvix.Compiler.Core.Extra.Base
 where
 
 import Data.Functor.Identity
+import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Core.Data.BinderList (BinderList)
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Language
@@ -52,32 +53,26 @@ mkConstr' = mkConstr Info.empty
 mkLambda :: Info -> Binder -> Node -> Node
 mkLambda i bi b = NLam (Lambda i bi b)
 
-mkLambda' :: Node -> Node
-mkLambda' = mkLambda Info.empty emptyBinder
+mkLambda' :: Type -> Node -> Node
+mkLambda' ty = mkLambda Info.empty (mkBinder' ty)
 
-mkLambdaTy :: Node -> Node -> Node
-mkLambdaTy ty = mkLambda Info.empty (Binder "?" Nothing ty)
+mkLambdas' :: [Type] -> Node -> Node
+mkLambdas' tys n = foldl' (flip mkLambda') n (reverse tys)
 
-mkLambdasTy :: [Type] -> Node -> Node
-mkLambdasTy tys n = foldl' (flip mkLambdaTy) n (reverse tys)
-
-mkLetItem' :: Node -> LetItem
-mkLetItem' = LetItem emptyBinder
+mkLetItem' :: Type -> Node -> LetItem
+mkLetItem' ty = LetItem (mkBinder' ty)
 
 mkLet :: Info -> Binder -> Node -> Node -> Node
 mkLet i bi v b = NLet (Let i (LetItem bi v) b)
 
-mkLetTy :: Info -> Type -> Node -> Node -> Node
-mkLetTy i ty = mkLet i (Binder "?" Nothing ty)
-
-mkLet' :: Node -> Node -> Node
-mkLet' = mkLet Info.empty emptyBinder
+mkLet' :: Type -> Node -> Node -> Node
+mkLet' ty = mkLet Info.empty (mkBinder' ty)
 
 mkLetRec :: Info -> NonEmpty LetItem -> Node -> Node
 mkLetRec i vs b = NRec (LetRec i vs b)
 
-mkLetRec' :: NonEmpty Node -> Node -> Node
-mkLetRec' = mkLetRec Info.empty . fmap mkLetItem'
+mkLetRec' :: NonEmpty (Type, Node) -> Node -> Node
+mkLetRec' = mkLetRec Info.empty . fmap (uncurry mkLetItem')
 
 mkCase :: Info -> Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
 mkCase i sym v bs def = NCase (Case i sym v bs def)
@@ -85,10 +80,10 @@ mkCase i sym v bs def = NCase (Case i sym v bs def)
 mkCase' :: Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
 mkCase' = mkCase Info.empty
 
-mkMatch :: Info -> NonEmpty Node -> [MatchBranch] -> Node
-mkMatch i vs bs = NMatch (Match i vs bs)
+mkMatch :: Info -> NonEmpty Type -> Type -> NonEmpty Node -> [MatchBranch] -> Node
+mkMatch i vtys rty vs bs = NMatch (Match i vtys rty vs bs)
 
-mkMatch' :: NonEmpty Node -> [MatchBranch] -> Node
+mkMatch' :: NonEmpty Type -> Type -> NonEmpty Node -> [MatchBranch] -> Node
 mkMatch' = mkMatch Info.empty
 
 mkMatchBranch :: Info -> NonEmpty Pattern -> Node -> MatchBranch
@@ -112,6 +107,12 @@ mkIf i sym v b1 b2 = mkCase i sym v [br] (Just b2)
 mkIf' :: Symbol -> Node -> Node -> Node -> Node
 mkIf' = mkIf Info.empty
 
+mkBinder :: Text -> Type -> Binder
+mkBinder name ty = Binder name Nothing ty
+
+mkBinder' :: Type -> Binder
+mkBinder' ty = Binder "?" Nothing ty
+
 {------------------------------------------------------------------------}
 {- Type constructors -}
 
@@ -139,6 +140,9 @@ mkUniv i l = NUniv (Univ i l)
 mkUniv' :: Int -> Type
 mkUniv' = mkUniv Info.empty
 
+mkSmallUniv :: Type
+mkSmallUniv = mkUniv' (fromIntegral smallLevel)
+
 mkTypeConstr :: Info -> Symbol -> [Type] -> Type
 mkTypeConstr i sym args = NTyp (TypeConstr i sym args)
 
@@ -197,10 +201,9 @@ isDynamic = \case
   NDyn {} -> True
   _ -> False
 
-isTypeConstr :: Type -> Bool
-isTypeConstr ty = case typeTarget ty of
-  NUniv {} -> True
-  _ -> False
+isInductive :: Type -> Bool
+isInductive NTyp {} = True
+isInductive _ = False
 
 -- | `expandType argtys ty` expands the dynamic target of `ty` to match the
 -- number of arguments with types specified by `argstys`. For example,
@@ -252,11 +255,6 @@ mkLambdaB = mkLambda mempty
 mkLambdasB :: [Binder] -> Node -> Node
 mkLambdasB is n = foldl' (flip mkLambdaB) n (reverse is)
 
-mkLambdas' :: Int -> Node -> Node
-mkLambdas' k
-  | k < 0 = impossible
-  | otherwise = mkLambdasB (replicate k emptyBinder)
-
 -- | \x\y b gives ([y, x], b)
 unfoldLambdasRev :: Node -> ([LambdaLhs], Node)
 unfoldLambdasRev = go []
@@ -272,6 +270,9 @@ unfoldLambdas = first reverse . unfoldLambdasRev
 unfoldLambdas' :: Node -> (Int, Node)
 unfoldLambdas' = first length . unfoldLambdas
 
+lambdaTypes :: Node -> [Type]
+lambdaTypes = map (\LambdaLhs {..} -> _lambdaLhsBinder ^. binderType) . fst . unfoldLambdas
+
 isType :: Node -> Bool
 isType = \case
   NPi {} -> True
@@ -295,15 +296,18 @@ isType = \case
 {------------------------------------------------------------------------}
 {- functions on Pattern -}
 
-getPatternBinders :: Pattern -> [Binder]
-getPatternBinders = reverse . go []
+getPatternParts :: Pattern -> [Either Binder Node]
+getPatternParts = reverse . go []
   where
-    go :: [Binder] -> Pattern -> [Binder]
+    go :: [Either Binder Node] -> Pattern -> [Either Binder Node]
     go acc = \case
-      PatConstr PatternConstr {..} -> foldl' go acc _patternConstrArgs
-      PatBinder p -> go (p ^. patternBinder : acc) (p ^. patternBinderPattern)
+      PatConstr PatternConstr {..} -> Right _patternConstrType : foldl' go acc _patternConstrArgs
+      PatBinder p -> go (Left (p ^. patternBinder) : acc) (p ^. patternBinderPattern)
       PatWildcard {} -> acc
 
+getPatternBinders :: Pattern -> [Binder]
+getPatternBinders = lefts . getPatternParts
+
 getPatternInfos :: Pattern -> [Info]
 getPatternInfos = reverse . go []
   where
@@ -313,6 +317,32 @@ getPatternInfos = reverse . go []
       PatBinder PatternBinder {..} -> go acc _patternBinderPattern
       PatWildcard PatternWildcard {..} -> _patternWildcardInfo : acc
 
+mapPatternBinders :: (Int -> Binder -> Binder) -> Pattern -> Pattern
+mapPatternBinders f = snd . go 0
+  where
+    go :: Int -> Pattern -> (Int, Pattern)
+    go k = \case
+      PatConstr p ->
+        let (k', rargs') =
+              foldl'
+                ( \(m, acc) pat ->
+                    let (m', pat') = go m pat
+                     in (m', pat' : acc)
+                )
+                (k, [])
+                (p ^. patternConstrArgs)
+         in (k', PatConstr p {_patternConstrArgs = reverse rargs'})
+      PatBinder p ->
+        let (k', pat') = go (k + 1) (p ^. patternBinderPattern)
+         in ( k',
+              PatBinder
+                p
+                  { _patternBinder = f k (p ^. patternBinder),
+                    _patternBinderPattern = pat'
+                  }
+            )
+      PatWildcard p -> (k, PatWildcard p)
+
 {------------------------------------------------------------------------}
 {- generic Node destruction -}
 
@@ -342,7 +372,7 @@ data NodeDetails = NodeDetails
     -- | 'nodeReassemble' reassembles the node from the info, the subinfos and
     -- the children (which should be in the same fixed order as in the
     -- 'nodeSubinfos' and 'nodeChildren' components).
-    _nodeReassemble :: Info -> [Info] -> [NodeChild] -> Node
+    _nodeReassemble :: Info -> [Info] -> [Node] -> Node
   }
 
 makeLenses ''NodeDetails
@@ -374,44 +404,44 @@ manyBinders bis n =
       _childBindersNum = length bis
     }
 
-type Reassemble = Info -> [Info] -> [NodeChild] -> Node
+type Reassemble = Info -> [Info] -> [Node] -> Node
 
 {-# INLINE noChildren #-}
 noChildren :: (Info -> Node) -> Reassemble
 noChildren f i _ _ = f i
 
 {-# INLINE oneChild #-}
-oneChild :: (Info -> NodeChild -> Node) -> Reassemble
+oneChild :: (Info -> Node -> Node) -> Reassemble
 oneChild f i _ ch = case ch of
   [c] -> f i c
   _ -> impossible
 
 {-# INLINE twoChildren #-}
-twoChildren :: (Info -> NodeChild -> NodeChild -> Node) -> Reassemble
+twoChildren :: (Info -> Node -> Node -> Node) -> Reassemble
 twoChildren f i _ ch = case ch of
   [l, r] -> f i l r
   _ -> impossible
 
 {-# INLINE threeChildren #-}
-threeChildren :: (Info -> NodeChild -> NodeChild -> NodeChild -> Node) -> Reassemble
+threeChildren :: (Info -> Node -> Node -> Node -> Node) -> Reassemble
 threeChildren f i _ ch = case ch of
   [a, b, c] -> f i a b c
   _ -> impossible
 
 {-# INLINE manyChildren #-}
-manyChildren :: (Info -> [NodeChild] -> Node) -> Reassemble
+manyChildren :: (Info -> [Node] -> Node) -> Reassemble
 manyChildren f i _ = f i
 
 {-# INLINE someChildren #-}
-someChildren :: (Info -> NonEmpty NodeChild -> Node) -> Reassemble
+someChildren :: (Info -> NonEmpty Node -> Node) -> Reassemble
 someChildren f i _ = f i . nonEmpty'
 
 {-# INLINE someChildrenI #-}
-someChildrenI :: (Info -> [Info] -> NonEmpty NodeChild -> Node) -> Reassemble
+someChildrenI :: (Info -> [Info] -> NonEmpty Node -> Node) -> Reassemble
 someChildrenI f i is = f i is . nonEmpty'
 
 {-# INLINE twoManyChildrenI #-}
-twoManyChildrenI :: (Info -> [Info] -> NodeChild -> NodeChild -> [NodeChild] -> Node) -> Reassemble
+twoManyChildrenI :: (Info -> [Info] -> Node -> Node -> [Node] -> Node) -> Reassemble
 twoManyChildrenI f i is = \case
   (x : y : xs) -> f i is x y xs
   _ -> impossible
@@ -450,21 +480,21 @@ destruct = \case
       { _nodeInfo = i,
         _nodeSubinfos = [],
         _nodeChildren = map noBinders [l, r],
-        _nodeReassemble = twoChildren $ \i' l' r' -> mkApp i' (l' ^. childNode) (r' ^. childNode)
+        _nodeReassemble = twoChildren $ \i' l' r' -> mkApp i' l' r'
       }
   NBlt (BuiltinApp i op args) ->
     NodeDetails
       { _nodeInfo = i,
         _nodeSubinfos = [],
         _nodeChildren = map noBinders args,
-        _nodeReassemble = manyChildren $ \i' args' -> mkBuiltinApp i' op (map (^. childNode) args')
+        _nodeReassemble = manyChildren $ \i' args' -> mkBuiltinApp i' op args'
       }
   NCtr (Constr i tag args) ->
     NodeDetails
       { _nodeInfo = i,
         _nodeSubinfos = [],
         _nodeChildren = map noBinders args,
-        _nodeReassemble = manyChildren $ \i' -> mkConstr i' tag . map (^. childNode)
+        _nodeReassemble = manyChildren $ \i' -> mkConstr i' tag
       }
   NLam (Lambda i bi b) ->
     NodeDetails
@@ -473,8 +503,8 @@ destruct = \case
         _nodeChildren = [noBinders (bi ^. binderType), oneBinder bi b],
         _nodeReassemble = twoChildren $ \i' ty' b' ->
           let binder' :: Binder
-              binder' = set binderType (ty' ^. childNode) bi
-           in mkLambda i' binder' (b' ^. childNode)
+              binder' = set binderType ty' bi
+           in mkLambda i' binder' b'
       }
   NLet (Let i (LetItem bi v) b) ->
     NodeDetails
@@ -483,8 +513,8 @@ destruct = \case
         _nodeChildren = [noBinders (bi ^. binderType), noBinders v, oneBinder bi b],
         _nodeReassemble = threeChildren $ \i' ty' v' b' ->
           let binder' :: Binder
-              binder' = set binderType (ty' ^. childNode) bi
-           in mkLet i' binder' (v' ^. childNode) (b' ^. childNode)
+              binder' = set binderType ty' bi
+           in mkLet i' binder' v' b'
       }
   NRec (LetRec i vs b) ->
     NodeDetails
@@ -501,11 +531,11 @@ destruct = \case
           let numItems :: Int
               numItems = length vs
               tys' :: [Type]
-              values' :: [NodeChild]
-              (values', tys') = second (map (^. childNode)) (splitAtExact numItems valuesTys')
+              values' :: [Node]
+              (values', tys') = splitAtExact numItems valuesTys'
               items' =
                 nonEmpty'
-                  [ LetItem (Binder name loc ty') (v' ^. childNode)
+                  [ LetItem (Binder name loc ty') v'
                     | (v', ty', name, loc) <-
                         zip4Exact
                           values'
@@ -513,7 +543,7 @@ destruct = \case
                           (map (^. letItemBinder . binderName) (toList vs))
                           (map (^. letItemBinder . binderLocation) (toList vs))
                   ]
-           in mkLetRec i' items' (b' ^. childNode)
+           in mkLetRec i' items' b'
       }
   NCase (Case i sym v brs mdef) ->
     let branchChildren :: [([Binder], NodeChild)]
@@ -526,21 +556,21 @@ destruct = \case
         allNodes :: [NodeChild]
         allNodes =
           concat
-            [ b : map (noBinders . (^. binderType)) bi
-              | (bi, b) <- branchChildren
+            [ br : reverse (foldl' (\r b -> manyBinders (take (length r) bi) (b ^. binderType) : r) [] bi)
+              | (bi, br) <- branchChildren
             ]
-        mkBranch :: Info -> CaseBranch -> Sem '[Input (Maybe NodeChild)] CaseBranch
+        mkBranch :: Info -> CaseBranch -> Sem '[Input (Maybe Node)] CaseBranch
         mkBranch nfo' br = do
           b' <- input'
           let nBinders = br ^. caseBranchBindersNum
-          tys' <- map (^. childNode) <$> replicateM nBinders input'
+          tys' <- replicateM nBinders input'
           return
             br
               { _caseBranchInfo = nfo',
-                _caseBranchBinders = zipWithExact (set binderType) tys' (b' ^. childBinders),
-                _caseBranchBody = b' ^. childNode
+                _caseBranchBinders = zipWithExact (set binderType) tys' (br ^. caseBranchBinders),
+                _caseBranchBody = b'
               }
-        mkBranches :: [Info] -> [NodeChild] -> [CaseBranch]
+        mkBranches :: [Info] -> [Node] -> [CaseBranch]
         mkBranches is' allNodes' =
           run $
             runInputList allNodes' $
@@ -555,7 +585,7 @@ destruct = \case
                 _nodeSubinfos = map (^. caseBranchInfo) brs,
                 _nodeChildren = noBinders v : allNodes,
                 _nodeReassemble = someChildrenI $ \i' is' (v' :| allNodes') ->
-                  mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') Nothing
+                  mkCase i' sym v' (mkBranches is' allNodes') Nothing
               }
           Just def ->
             NodeDetails
@@ -563,23 +593,32 @@ destruct = \case
                 _nodeSubinfos = map (^. caseBranchInfo) brs,
                 _nodeChildren = noBinders v : noBinders def : allNodes,
                 _nodeReassemble = twoManyChildrenI $ \i' is' v' def' allNodes' ->
-                  mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') (Just (def' ^. childNode))
+                  mkCase i' sym v' (mkBranches is' allNodes') (Just def')
               }
-  NMatch (Match i vs branches) ->
+  NMatch (Match i vtys rty vs branches) ->
     let allNodes :: [NodeChild]
         allNodes =
-          concat
-            [ b
-                : map (noBinders . (^. binderType)) bis
-              | (bis, b) <- branchChildren
-            ]
+          noBinders rty
+            : map noBinders (toList vtys)
+            ++ map noBinders (toList vs)
+            ++ concat
+              [ br
+                  : reverse (foldl' (\acc b -> manyBinders (take (length acc) (lefts bis)) (getNode b) : acc) [] bis)
+                | (bis, br) <- branchChildren
+              ]
           where
-            branchChildren :: [([Binder], NodeChild)]
+            branchChildren :: [([Either Binder Node], NodeChild)]
             branchChildren =
-              [ (binders, manyBinders binders (br ^. matchBranchBody))
+              [ (parts, manyBinders (lefts parts) (br ^. matchBranchBody))
                 | br <- branches,
-                  let binders = concatMap getPatternBinders (toList (br ^. matchBranchPatterns))
+                  let parts = concatMap getPatternParts (toList (br ^. matchBranchPatterns))
               ]
+
+            getNode :: Either Binder Node -> Node
+            getNode = \case
+              Left b -> b ^. binderType
+              Right n -> n
+
         branchInfos :: [Info]
         branchInfos =
           concat
@@ -588,7 +627,8 @@ destruct = \case
                 : concatMap getPatternInfos (br ^. matchBranchPatterns)
               | br <- branches
             ]
-        setPatternsInfos :: forall r. (Members '[Input (Maybe Info), Input (Maybe NodeChild)] r) => NonEmpty Pattern -> Sem r (NonEmpty Pattern)
+        -- sets the infos and the binder types in the patterns
+        setPatternsInfos :: forall r. (Members '[Input (Maybe Info), Input (Maybe Node)] r) => NonEmpty Pattern -> Sem r (NonEmpty Pattern)
         setPatternsInfos = mapM goPattern
           where
             goPattern :: Pattern -> Sem r Pattern
@@ -597,20 +637,21 @@ destruct = \case
                 i' <- input'
                 return (PatWildcard (set patternWildcardInfo i' x))
               PatBinder x -> do
-                ty <- (^. childNode) <$> input'
+                ty <- input'
                 let _patternBinder = set binderType ty (x ^. patternBinder)
                 _patternBinderPattern <- goPattern (x ^. patternBinderPattern)
                 return (PatBinder PatternBinder {..})
               PatConstr x -> do
                 i' <- input'
                 args' <- mapM goPattern (x ^. patternConstrArgs)
-                return (PatConstr (set patternConstrInfo i' (set patternConstrArgs args' x)))
+                ty <- input'
+                return (PatConstr (set patternConstrType ty (set patternConstrInfo i' (set patternConstrArgs args' x))))
      in NodeDetails
           { _nodeInfo = i,
             _nodeSubinfos = branchInfos,
-            _nodeChildren = map noBinders (toList vs) ++ allNodes,
+            _nodeChildren = allNodes,
             _nodeReassemble = someChildrenI $ \i' is' chs' ->
-              let mkBranch :: MatchBranch -> Sem '[Input (Maybe NodeChild), Input (Maybe Info)] MatchBranch
+              let mkBranch :: MatchBranch -> Sem '[Input (Maybe Node), Input (Maybe Info)] MatchBranch
                   mkBranch br = do
                     bi' <- input'
                     b' <- input'
@@ -619,19 +660,28 @@ destruct = \case
                       br
                         { _matchBranchInfo = bi',
                           _matchBranchPatterns = pats',
-                          _matchBranchBody = b' ^. childNode
+                          _matchBranchBody = b'
                         }
                   numVals = length vs
-                  values' :: NonEmpty NodeChild
-                  branchesChilds' :: [NodeChild]
-                  (values', branchesChilds') = first nonEmpty' (splitAtExact numVals (toList chs'))
+                  values' :: NonEmpty Node
+                  valueTypes' :: NonEmpty Node
+                  returnType' :: Node
+                  branchesChildren' :: [Node]
+                  returnType' = head chs'
+                  (valueTypes', chs'') = first nonEmpty' (splitAtExact numVals (NonEmpty.tail chs'))
+                  (values', branchesChildren') = first nonEmpty' (splitAtExact numVals chs'')
                   branches' :: [MatchBranch]
                   branches' =
                     run $
                       runInputList is' $
-                        runInputList branchesChilds' $
+                        runInputList branchesChildren' $
                           mapM mkBranch branches
-               in mkMatch i' (fmap (^. childNode) values') branches'
+               in mkMatch
+                    i'
+                    valueTypes'
+                    returnType'
+                    values'
+                    branches'
           }
   NPi (Pi i bi b) ->
     NodeDetails
@@ -640,8 +690,8 @@ destruct = \case
         _nodeChildren = [noBinders (bi ^. binderType), oneBinder bi b],
         _nodeReassemble = twoChildren $ \i' bi' b' ->
           let binder' :: Binder
-              binder' = set binderType (bi' ^. childNode) bi
-           in mkPi i' binder' (b' ^. childNode)
+              binder' = set binderType bi' bi
+           in mkPi i' binder' b'
       }
   NUniv (Univ i l) ->
     NodeDetails
@@ -655,7 +705,7 @@ destruct = \case
       { _nodeInfo = i,
         _nodeSubinfos = [],
         _nodeChildren = map noBinders args,
-        _nodeReassemble = manyChildren $ \i' -> mkTypeConstr i' sym . map (^. childNode)
+        _nodeReassemble = manyChildren $ \i' -> mkTypeConstr i' sym
       }
   NPrim (TypePrim i prim) ->
     NodeDetails
@@ -677,14 +727,11 @@ destruct = \case
         _nodeSubinfos = [],
         _nodeChildren = oneBinder bi b : map noBinders env,
         _nodeReassemble = someChildren $ \i' (b' :| env') ->
-          Closure (map (^. childNode) env') (Lambda i' bi (b' ^. childNode))
+          Closure env' (Lambda i' bi b')
       }
 
 reassembleDetails :: NodeDetails -> [Node] -> Node
-reassembleDetails d ns = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos) children'
-  where
-    children' :: [NodeChild]
-    children' = zipWithExact (set childNode) ns (d ^. nodeChildren)
+reassembleDetails d ns = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos) ns
 
 reassemble :: Node -> [Node] -> Node
 reassemble = reassembleDetails . destruct
@@ -708,7 +755,7 @@ modifyInfoM f n =
    in do
         i' <- f (ni ^. nodeInfo)
         is' <- mapM f (ni ^. nodeSubinfos)
-        return ((ni ^. nodeReassemble) i' is' (ni ^. nodeChildren))
+        return ((ni ^. nodeReassemble) i' is' (map (^. childNode) (ni ^. nodeChildren)))
 
 modifyInfo :: (Info -> Info) -> Node -> Node
 modifyInfo f n = runIdentity $ modifyInfoM (pure . f) n
diff --git a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
index 26405c230b..34b30a48d6 100644
--- a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
@@ -41,3 +41,6 @@ mkLet binder value body = NLet (Let () item body)
 
 mkCase :: Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
 mkCase sym v bs def = NCase (Case () sym v bs def)
+
+mkIf :: Node -> Node -> Node -> Node
+mkIf v br1 br2 = NIf (If () v br1 br2)
diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
index be1f44b62f..a7e76f25bb 100644
--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/src/Juvix/Compiler/Core/Extra/Utils.hs
@@ -22,7 +22,6 @@ import Juvix.Compiler.Core.Extra.Recursors
 import Juvix.Compiler.Core.Extra.Recursors.Fold.Named
 import Juvix.Compiler.Core.Extra.Recursors.Map.Named
 import Juvix.Compiler.Core.Extra.SubstEnv
-import Juvix.Compiler.Core.Info.TypeInfo
 import Juvix.Compiler.Core.Language
 
 isClosed :: Node -> Bool
@@ -92,24 +91,39 @@ cosmos f = ufoldA reassemble f
 -- if fv = x1, x2, .., xn
 -- the result is of the form λx1 λx2 .. λ xn b
 captureFreeVars :: [(Index, Binder)] -> Node -> Node
-captureFreeVars fv
-  | n == 0 = id
-  | otherwise = mkLambdasB infos . mapFreeVars
+captureFreeVars freevars = goBinders freevars . mapFreeVars
   where
-    (indices, infos) = unzip fv
-    n = length fv
-    s :: HashMap Index Index
-    s = HashMap.fromList (zip (reverse indices) [0 ..])
     mapFreeVars :: Node -> Node
     mapFreeVars = dmapN go
       where
+        s :: HashMap Index Index
+        s = HashMap.fromList (zip (reverse (map fst freevars)) [0 ..])
         go :: Index -> Node -> Node
         go k = \case
           NVar (Var i u)
             | Just v <- s ^. at (u - k) -> NVar (Var i (v + k))
           m -> m
 
--- captures all free variables of a node. It also returns the list of captured
+    goBinders :: [(Index, Binder)] -> Node -> Node
+    goBinders fv = case unsnoc fv of
+      Nothing -> id
+      Just (fvs, (idx, bin)) -> goBinders fvs . mkLambdaB (mapBinder idx bin)
+      where
+        indices = map fst fv
+        mapBinder :: Index -> Binder -> Binder
+        mapBinder binderIndex = over binderType (dmapN go)
+          where
+            go :: Index -> Node -> Node
+            go k = \case
+              NVar u
+                | u ^. varIndex >= k ->
+                    let uCtx = u ^. varIndex - k + binderIndex + 1
+                        err = error ("impossible: could not find " <> show uCtx <> " in " <> show indices)
+                        u' = length indices - 2 - fromMaybe err (elemIndex uCtx indices) + k
+                     in NVar (set varIndex u' u)
+              m -> m
+
+-- | Captures all free variables of a node. It also returns the list of captured
 -- variables in left-to-right order: if snd is of the form λxλy... then fst is
 -- [x, y]
 captureFreeVarsCtx :: BinderList Binder -> Node -> ([(Var, Binder)], Node)
@@ -120,11 +134,11 @@ captureFreeVarsCtx bl n =
 freeVarsCtx' :: BinderList Binder -> Node -> [Var]
 freeVarsCtx' bl = map fst . freeVarsCtx bl
 
--- | the output list does not contain repeated elements and is sorted by *decreasing* variable index.
+-- | The output list does not contain repeated elements and is sorted by *decreasing* variable index.
 -- The indices are relative to the given binder list
 freeVarsCtx :: BinderList Binder -> Node -> [(Var, Binder)]
-freeVarsCtx ctx n =
-  BL.lookupsSortedRev ctx . run . fmap fst . runOutputList $ go (freeVarsSorted n)
+freeVarsCtx ctx =
+  BL.lookupsSortedRev ctx . run . fmap fst . runOutputList . go . freeVarsSorted
   where
     go ::
       -- set of free variables relative to the original ctx
@@ -135,9 +149,10 @@ freeVarsCtx ctx n =
       Just (v, vs) -> do
         output v
         let idx = v ^. varIndex
-            bi = BL.lookup idx ctx
+            bi :: Binder = BL.lookup idx ctx
+            fbi = freeVarsSorted (bi ^. binderType)
             freevarsbi' :: Set Var
-            freevarsbi' = Set.mapMonotonic (over varIndex (+ (idx + 1))) (freeVarsSorted (bi ^. binderType))
+            freevarsbi' = Set.mapMonotonic (over varIndex (+ (idx + 1))) fbi
         go (freevarsbi' <> vs)
 
 -- | subst for multiple bindings
@@ -157,6 +172,18 @@ substs t = umapN go
 subst :: Node -> Node -> Node
 subst t = substs [t]
 
+-- | `substDrop args argtys` drops `length args` from `argtys` and substitutes
+-- the corresponding variables with `args`. For example:
+-- ```
+-- substDrop [Nat, Var 3] [Type, Type, Var 1, Var 1] =
+--   [Nat, Var 4]
+-- ``
+substDrop :: [Node] -> [Node] -> [Node]
+substDrop args argtys =
+  reverse $ snd $ foldl' (\(args', acc) ty -> (mkVar' 0 : map (shift 1) args', substs args' ty : acc)) (reverse args, []) (drop k argtys)
+  where
+    k = length args
+
 -- | reduce all beta redexes present in a term and the ones created immediately
 -- downwards (i.e., a "beta-development")
 developBeta :: Node -> Node
@@ -167,9 +194,12 @@ developBeta = umap go
       NApp (App _ (NLam (Lambda {..})) arg) -> subst arg _lambdaBody
       _ -> n
 
-etaExpand :: Int -> Node -> Node
-etaExpand 0 n = n
-etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' (reverse [0 .. k - 1])))
+etaExpand :: [Type] -> Node -> Node
+etaExpand [] n = n
+etaExpand argtys n =
+  mkLambdas' argtys (mkApps' (shift k n) (map mkVar' (reverse [0 .. k - 1])))
+  where
+    k = length argtys
 
 convertClosures :: Node -> Node
 convertClosures = umap go
@@ -182,6 +212,26 @@ convertClosures = umap go
 convertRuntimeNodes :: Node -> Node
 convertRuntimeNodes = convertClosures
 
+squashApps :: Node -> Node
+squashApps = dmap go
+  where
+    go :: Node -> Node
+    go n =
+      let (l, args) = unfoldApps' n
+       in case l of
+            NCtr (Constr i tag args') -> mkConstr i tag (args' ++ args)
+            NBlt (BuiltinApp i op args') -> mkBuiltinApp i op (args' ++ args)
+            NTyp (TypeConstr i sym args') -> mkTypeConstr i sym (args' ++ args)
+            _ -> n
+
+binderFromArgumentInfo :: ArgumentInfo -> Binder
+binderFromArgumentInfo a =
+  Binder
+    { _binderName = a ^. argumentName,
+      _binderLocation = a ^. argumentLocation,
+      _binderType = a ^. argumentType
+    }
+
 argumentInfoFromBinder :: Binder -> ArgumentInfo
 argumentInfoFromBinder i =
   ArgumentInfo
@@ -202,6 +252,22 @@ patternBindersNum = length . (^.. patternBinders)
 
 patternType :: Pattern -> Node
 patternType = \case
-  PatWildcard w -> getInfoType (w ^. patternWildcardInfo)
+  PatWildcard w -> w ^. patternWildcardType
   PatBinder b -> b ^. patternBinder . binderType
-  PatConstr c -> getInfoType (c ^. patternConstrInfo)
+  PatConstr c -> c ^. patternConstrType
+
+builtinOpArgTypes :: BuiltinOp -> [Type]
+builtinOpArgTypes = \case
+  OpIntAdd -> [mkTypeInteger', mkTypeInteger']
+  OpIntSub -> [mkTypeInteger', mkTypeInteger']
+  OpIntMul -> [mkTypeInteger', mkTypeInteger']
+  OpIntDiv -> [mkTypeInteger', mkTypeInteger']
+  OpIntMod -> [mkTypeInteger', mkTypeInteger']
+  OpIntLt -> [mkTypeInteger', mkTypeInteger']
+  OpIntLe -> [mkTypeInteger', mkTypeInteger']
+  OpEq -> [mkDynamic', mkDynamic']
+  OpShow -> [mkDynamic']
+  OpStrConcat -> [mkTypeString', mkTypeString']
+  OpStrToInt -> [mkTypeString']
+  OpTrace -> [mkDynamic', mkDynamic']
+  OpFail -> [mkTypeString']
diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs
index 7410800f0a..338ebcc095 100644
--- a/src/Juvix/Compiler/Core/Language.hs
+++ b/src/Juvix/Compiler/Core/Language.hs
@@ -43,7 +43,7 @@ type Match = Match' Info Node
 
 type MatchBranch = MatchBranch' Info Node
 
-type PatternWildcard = PatternWildcard' Info
+type PatternWildcard = PatternWildcard' Info Node
 
 type PatternBinder = PatternBinder' Info Node
 
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 4f6e07ffd2..f679564bd0 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -104,6 +104,8 @@ data LetItem' a ty = LetItem
 -- body and in the values `length _letRecValues` implicit binders are introduced
 -- which hold the functions/values being defined.
 -- the last item in _letRecValues will have have index $0 in the body.
+-- The values are *not* in scope of the binders. I.e.
+-- the binders of the values cannot refer to the values
 data LetRec' i a ty = LetRec
   { _letRecInfo :: i,
     _letRecValues :: !(NonEmpty (LetItem' a ty)),
@@ -131,9 +133,19 @@ data CaseBranch' i a ty = CaseBranch
     _caseBranchBody :: !a
   }
 
+-- | A special form of `Case` for the booleans. Used only in Core.Stripped.
+data If' i a = If
+  { _ifInfo :: i,
+    _ifValue :: !a,
+    _ifTrue :: !a,
+    _ifFalse :: !a
+  }
+
 -- | Complex pattern match. `Match` is lazy: only the selected branch is evaluated.
 data Match' i a = Match
   { _matchInfo :: i,
+    _matchValueTypes :: !(NonEmpty a),
+    _matchReturnType :: !a,
     _matchValues :: !(NonEmpty a),
     _matchBranches :: ![MatchBranch' i a]
   }
@@ -151,12 +163,13 @@ data MatchBranch' i a = MatchBranch
   }
 
 data Pattern' i a
-  = PatWildcard (PatternWildcard' i)
+  = PatWildcard (PatternWildcard' i a)
   | PatBinder (PatternBinder' i a)
   | PatConstr (PatternConstr' i a)
 
-newtype PatternWildcard' i = PatternWildcard
-  { _patternWildcardInfo :: i
+data PatternWildcard' i a = PatternWildcard
+  { _patternWildcardInfo :: i,
+    _patternWildcardType :: a
   }
 
 data PatternBinder' i a = PatternBinder
@@ -167,7 +180,8 @@ data PatternBinder' i a = PatternBinder
 data PatternConstr' i a = PatternConstr
   { _patternConstrInfo :: i,
     _patternConstrTag :: !Tag,
-    _patternConstrArgs :: ![Pattern' i a]
+    _patternConstrArgs :: ![Pattern' i a],
+    _patternConstrType :: a
   }
 
 -- | Useful for unfolding Pi
@@ -251,10 +265,13 @@ instance HasAtomicity (LetRec' i a ty) where
 instance HasAtomicity (Case' i bi a ty) where
   atomicity _ = Aggregate lambdaFixity
 
+instance HasAtomicity (If' i a) where
+  atomicity _ = Aggregate lambdaFixity
+
 instance HasAtomicity (Match' i a) where
   atomicity _ = Aggregate lambdaFixity
 
-instance HasAtomicity (PatternWildcard' i) where
+instance HasAtomicity (PatternWildcard' i a) where
   atomicity _ = Atom
 
 instance HasAtomicity (PatternBinder' i a) where
@@ -341,15 +358,18 @@ instance (Eq a) => Eq (Constr' i a) where
 instance (Eq a) => Eq (Case' i bi a ty) where
   (Case _ sym1 v1 bs1 def1) == (Case _ sym2 v2 bs2 def2) = sym1 == sym2 && v1 == v2 && bs1 == bs2 && def1 == def2
 
+instance (Eq a) => Eq (If' i a) where
+  (If _ v1 b1 c1) == (If _ v2 b2 c2) = v1 == v2 && b1 == b2 && c1 == c2
+
 instance (Eq a) => Eq (CaseBranch' i a ty) where
   (==) =
     eqOn (^. caseBranchTag)
       ..&&.. eqOn (^. caseBranchBody)
 
 instance (Eq a) => Eq (Match' i a) where
-  (Match _ vs1 bs1) == (Match _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
+  (Match _ _ _ vs1 bs1) == (Match _ _ _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
 
-instance Eq (PatternWildcard' i) where
+instance Eq (PatternWildcard' i a) where
   _ == _ = True
 
 instance Eq (Univ' i) where
@@ -397,7 +417,7 @@ instance (Eq a) => Eq (MatchBranch' i a) where
   (MatchBranch _ pats1 b1) == (MatchBranch _ pats2 b2) = pats1 == pats2 && b1 == b2
 
 instance (Eq a) => Eq (PatternConstr' i a) where
-  (PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
+  (PatternConstr _ tag1 ps1 _) == (PatternConstr _ tag2 ps2 _) = tag1 == tag2 && ps1 == ps2
 
 instance Hashable (Ident' i) where
   hashWithSalt s = hashWithSalt s . (^. identSymbol)
diff --git a/src/Juvix/Compiler/Core/Language/Stripped.hs b/src/Juvix/Compiler/Core/Language/Stripped.hs
index 9510b50d3c..c2214718a7 100644
--- a/src/Juvix/Compiler/Core/Language/Stripped.hs
+++ b/src/Juvix/Compiler/Core/Language/Stripped.hs
@@ -64,6 +64,8 @@ type Let = Let' () Node Type
 
 type Case = Case' () CaseBranchInfo Node Type
 
+type If = If' () Node
+
 type CaseBranch = CaseBranch' CaseBranchInfo Node Type
 
 {---------------------------------------------------------------------------------}
@@ -77,6 +79,7 @@ data Node
   | NCtr Constr
   | NLet Let
   | NCase Case
+  | NIf If
   deriving stock (Eq)
 
 instance HasAtomicity Node where
@@ -89,6 +92,7 @@ instance HasAtomicity Node where
     NCtr x -> atomicity x
     NLet x -> atomicity x
     NCase x -> atomicity x
+    NIf x -> atomicity x
 
 makeLenses ''VarInfo
 makeLenses ''IdentInfo
diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs
index 9b35342e36..907a448199 100644
--- a/src/Juvix/Compiler/Core/Pipeline.hs
+++ b/src/Juvix/Compiler/Core/Pipeline.hs
@@ -7,24 +7,15 @@ where
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Transformation
 
-toEvalTransformations :: [TransformationId]
-toEvalTransformations = [MatchToCase, NatToInt, ConvertBuiltinTypes]
-
 -- | Perform transformations on Core necessary for efficient evaluation
 toEval :: InfoTable -> InfoTable
 toEval = applyTransformations toEvalTransformations
 
-toStrippedTransformations :: [TransformationId]
-toStrippedTransformations = toEvalTransformations ++ [LambdaLetRecLifting, MoveApps, TopEtaExpand, RemoveTypeArgs]
-
 -- | Perform transformations on Core necessary before the translation to
 -- Core.Stripped
 toStripped :: InfoTable -> InfoTable
 toStripped = applyTransformations toStrippedTransformations
 
-toGebTransformations :: [TransformationId]
-toGebTransformations = toEvalTransformations ++ [UnrollRecursion, ComputeTypeInfo]
-
 -- | Perform transformations on Core necessary before the translation to GEB
 toGeb :: InfoTable -> InfoTable
 toGeb = applyTransformations toGebTransformations
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 52f70173d6..9e7c0d2afd 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -146,6 +146,22 @@ instance (PrettyCode a) => PrettyCode (Binder' a) where
     ty' <- ppCode ty
     return (parens (pretty name' <+> kwColon <+> ty'))
 
+ppWithType :: Member (Reader Options) r => Doc Ann -> Type -> Sem r (Doc Ann)
+ppWithType d = \case
+  NDyn {} ->
+    return d
+  ty -> do
+    ty' <- ppCode ty
+    return $ parens (d <+> kwColon <+> ty')
+
+ppTypeAnnot :: Member (Reader Options) r => Type -> Sem r (Doc Ann)
+ppTypeAnnot = \case
+  NDyn {} ->
+    return mempty
+  ty -> do
+    ty' <- ppCode ty
+    return $ mempty <+> kwColon <+> parens ty'
+
 ppCodeLet' :: (PrettyCode a, Member (Reader Options) r) => Text -> Maybe (Doc Ann) -> Let' i a ty -> Sem r (Doc Ann)
 ppCodeLet' name mty lt = do
   n' <- ppName KNameConstructor name
@@ -186,6 +202,13 @@ ppCodeCase' branchBinderNames branchTagNames Case {..} =
       let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs''
       return $ kwCase <+> v <+> kwOf <+> bss
 
+instance PrettyCode a => PrettyCode (If' i a) where
+  ppCode If {..} = do
+    v <- ppCode _ifValue
+    l <- ppCode _ifTrue
+    r <- ppCode _ifFalse
+    return $ kwIf <+> v <+> kwThen <+> l <+> kwElse <+> r
+
 instance PrettyCode PatternWildcard where
   ppCode _ = return kwWildcard
 
@@ -193,10 +216,11 @@ instance PrettyCode PatternBinder where
   ppCode PatternBinder {..} = do
     n <- ppName KNameLocal (_patternBinder ^. binderName)
     case _patternBinderPattern of
-      PatWildcard {} -> return n
+      PatWildcard {} -> do
+        ppWithType n (_patternBinder ^. binderType)
       _ -> do
         pat <- ppRightExpression appFixity _patternBinderPattern
-        return $ n <> kwAt <> pat
+        ppWithType (n <> kwAt <> pat) (_patternBinder ^. binderType)
 
 instance PrettyCode PatternConstr where
   ppCode PatternConstr {..} = do
@@ -230,17 +254,25 @@ instance PrettyCode Let where
 instance PrettyCode LetRec where
   ppCode :: forall r. (Member (Reader Options) r) => LetRec -> Sem r (Doc Ann)
   ppCode LetRec {..} = do
+    let tys = fmap (^. letItemBinder . binderType) _letRecValues
     names <- mapM (getName . (^. letItemBinder)) _letRecValues
+    types <- mapM ppCode tys
     vs <- mapM (ppCode . (^. letItemValue)) _letRecValues
     b' <- ppCode _letRecBody
-    return $ case names of
-      hns :| [] -> kwLetRec <+> hns <+> kwAssign <+> head vs <+> kwIn <+> b'
+    let bs =
+          zipWith3Exact
+            (\n ty ty' -> if isDynamic ty' then n else n <+> colon <+> ty)
+            (toList names)
+            (toList types)
+            (toList tys)
+    return $ case bs of
+      [hbs] -> kwLetRec <+> hbs <+> kwAssign <+> head vs <+> kwIn <+> b'
       _ ->
         let bss =
               indent' $
                 align $
                   concatWith (\a b -> a <> kwSemicolon <> line <> b) $
-                    zipWithExact (\name val -> name <+> kwAssign <+> val) (toList names) (toList vs)
+                    zipWithExact (\b val -> b <+> kwAssign <+> val) (toList bs) (toList vs)
             nss = enclose kwSquareL kwSquareR (concatWith (<+>) names)
          in kwLetRec <> nss <> line <> bss <> line <> kwIn <> line <> b'
     where
@@ -283,23 +315,13 @@ instance PrettyCode Node where
           branchBodies = map (^. matchBranchBody) _matchBranches
       pats <- mapM ppPatterns branchPatterns
       vs <- mapM ppCode _matchValues
+      vs' <- zipWithM ppWithType (toList vs) (toList _matchValueTypes)
       bs <- sequence $ zipWithExact (\ps br -> ppCode br >>= \br' -> return $ ps <+> kwMapsto <+> br') pats branchBodies
       let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs
-      return $ kwMatch <+> hsep (punctuate comma (toList vs)) <+> kwWith <+> bss
-    NPi Pi {..} ->
-      let piType = _piBinder ^. binderType
-       in case _piBinder ^. binderName of
-            "?" -> do
-              ty <- ppLeftExpression funFixity piType
-              b <- ppRightExpression funFixity _piBody
-              return $ ty <+> kwArrow <+> b
-            name -> do
-              n <- ppName KNameLocal name
-              ty <- ppCode piType
-              b <- ppCode _piBody
-              return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
-    NUniv Univ {..} ->
-      return $ kwType <+> pretty _univLevel
+      rty <- ppTypeAnnot _matchReturnType
+      return $ kwMatch <+> hsep (punctuate comma vs') <+> kwWith <> rty <+> bss
+    NPi p -> ppCode p
+    NUniv u -> ppCode u
     NPrim TypePrim {..} -> ppCode _typePrimPrimitive
     NTyp TypeConstr {..} -> do
       args' <- mapM (ppRightExpression appFixity) _typeConstrArgs
@@ -309,6 +331,27 @@ instance PrettyCode Node where
     Closure env l@Lambda {} ->
       ppCode (substEnv env (NLam l))
 
+instance PrettyCode Pi where
+  ppCode Pi {..} =
+    let piType = _piBinder ^. binderType
+     in case _piBinder ^. binderName of
+          "?" -> do
+            ty <- ppLeftExpression funFixity piType
+            b <- ppRightExpression funFixity _piBody
+            return $ ty <+> kwArrow <+> b
+          name -> do
+            n <- ppName KNameLocal name
+            ty <- ppCode piType
+            b <- ppCode _piBody
+            return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
+
+instance PrettyCode (Univ' i) where
+  ppCode Univ {..} =
+    return $
+      if
+          | _univLevel == 0 -> kwType
+          | otherwise -> kwType <+> pretty _univLevel
+
 instance PrettyCode Stripped.TypeApp where
   ppCode Stripped.TypeApp {..} = do
     args' <- mapM (ppRightExpression appFixity) _typeAppArgs
@@ -350,6 +393,7 @@ instance PrettyCode Stripped.Node where
       let branchBinderNames = map (map (^. binderName) . (^. caseBranchBinders)) _caseBranches
           branchTagNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoConstrName)) _caseBranches
        in ppCodeCase' branchBinderNames branchTagNames x
+    Stripped.NIf x -> ppCode x
 
 instance PrettyCode ConstructorInfo where
   ppCode :: (Member (Reader Options) r) => ConstructorInfo -> Sem r (Doc Ann)
@@ -400,11 +444,19 @@ instance PrettyCode Stripped.ArgumentInfo where
     ty <- ppCode _argumentType
     return $ name <+> colon <+> ty
 
+instance PrettyCode Stripped.ConstructorInfo where
+  ppCode :: (Member (Reader Options) r) => Stripped.ConstructorInfo -> Sem r (Doc Ann)
+  ppCode ci = do
+    name <- ppName KNameConstructor (ci ^. Stripped.constructorName)
+    ty <- ppCode (ci ^. Stripped.constructorType)
+    return $ name <+> colon <+> ty
+
 instance PrettyCode Stripped.InfoTable where
   ppCode :: forall r. (Member (Reader Options) r) => Stripped.InfoTable -> Sem r (Doc Ann)
   ppCode tbl = do
+    inds' <- ppInductives (HashMap.elems (tbl ^. Stripped.infoInductives))
     ctx' <- ppFunctions (tbl ^. Stripped.infoFunctions)
-    return ("-- Functions" <> line <> ctx' <> line)
+    return ("-- Types" <> line <> inds' <> line <> "-- Functions" <> line <> ctx' <> line)
     where
       ppFunctions :: HashMap Symbol Stripped.FunctionInfo -> Sem r (Doc Ann)
       ppFunctions ctx = do
@@ -418,6 +470,17 @@ instance PrettyCode Stripped.InfoTable where
             body' <- ppCode (fi ^. Stripped.functionBody)
             return (kwDef <+> sym' <> encloseSep lparen rparen ", " args <+> kwAssign <+> body')
 
+      ppInductives :: [Stripped.InductiveInfo] -> Sem r (Doc Ann)
+      ppInductives inds = do
+        inds' <- mapM ppInductive inds
+        return (vsep inds')
+        where
+          ppInductive :: Stripped.InductiveInfo -> Sem r (Doc Ann)
+          ppInductive ii = do
+            name <- ppName KNameInductive (ii ^. Stripped.inductiveName)
+            ctrs <- mapM (fmap (<> semi) . ppCode) (ii ^. Stripped.inductiveConstructors)
+            return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line))
+
 instance (PrettyCode a) => PrettyCode (NonEmpty a) where
   ppCode x = ppCode (toList x)
 
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index 2bd9f0e064..9f46b20896 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -38,3 +38,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
       ComputeTypeInfo -> computeTypeInfo
       UnrollRecursion -> unrollRecursion
       MatchToCase -> matchToCase
+      EtaExpandApps -> etaExpansionApps
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 3e7d52226d..2b2229dd39 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -35,3 +35,32 @@ mapT' f tab =
 
 walkT :: (Applicative f) => (Symbol -> Node -> f ()) -> InfoTable -> f ()
 walkT f tab = for_ (HashMap.toList (tab ^. identContext)) (uncurry f)
+
+mapAllNodes :: (Node -> Node) -> InfoTable -> InfoTable
+mapAllNodes f tab =
+  mapAxioms convertAxiom $
+    mapInductives convertInductive $
+      mapConstructors convertConstructor $
+        mapIdents convertIdent $
+          mapT (const f) tab
+  where
+    convertIdent :: IdentifierInfo -> IdentifierInfo
+    convertIdent ii =
+      ii
+        { _identifierType = f (ii ^. identifierType),
+          _identifierArgsInfo = map (over argumentType f) (ii ^. identifierArgsInfo)
+        }
+
+    convertConstructor :: ConstructorInfo -> ConstructorInfo
+    convertConstructor = over constructorType f
+
+    convertInductive :: InductiveInfo -> InductiveInfo
+    convertInductive ii =
+      ii
+        { _inductiveKind = f (ii ^. inductiveKind),
+          _inductiveParams = map (over paramKind f) (ii ^. inductiveParams),
+          _inductiveConstructors = map convertConstructor (ii ^. inductiveConstructors)
+        }
+
+    convertAxiom :: AxiomInfo -> AxiomInfo
+    convertAxiom = over axiomType f
diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
index d4661dd00a..7d5983f0de 100644
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
@@ -61,7 +61,7 @@ computeNodeTypeInfo tab = umapL go
         let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
             ii = fromJust $ HashMap.lookup (ci ^. constructorInductive) (tab ^. infoInductives)
          in case ii ^. inductiveBuiltin of
-              Just BuiltinBool ->
+              Just (BuiltinTypeInductive BuiltinBool) ->
                 mkTypeBool'
               _ ->
                 mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs)
diff --git a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
index a731ce8b3e..f3c554ec61 100644
--- a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
@@ -14,37 +14,14 @@ convertNode tab = umap go
     go node = case node of
       NTyp TypeConstr {..} ->
         case ii ^. inductiveBuiltin of
-          Just BuiltinBool -> mkTypeBool'
+          Just (BuiltinTypeInductive BuiltinBool) -> mkTypeBool'
+          Just (BuiltinTypeInductive BuiltinNat) -> mkTypeInteger'
+          Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString'
           _ -> node
         where
           ii = fromJust $ tab ^. infoInductives . at _typeConstrSymbol
       _ -> node
 
-convertIdent :: InfoTable -> IdentifierInfo -> IdentifierInfo
-convertIdent tab ii =
-  ii
-    { _identifierType = convertNode tab (ii ^. identifierType),
-      _identifierArgsInfo = map (over argumentType (convertNode tab)) (ii ^. identifierArgsInfo)
-    }
-
-convertConstructor :: InfoTable -> ConstructorInfo -> ConstructorInfo
-convertConstructor tab = over constructorType (convertNode tab)
-
-convertInductive :: InfoTable -> InductiveInfo -> InductiveInfo
-convertInductive tab ii =
-  ii
-    { _inductiveKind = convertNode tab (ii ^. inductiveKind),
-      _inductiveParams = map (over paramKind (convertNode tab)) (ii ^. inductiveParams),
-      _inductiveConstructors = map (convertConstructor tab) (ii ^. inductiveConstructors)
-    }
-
-convertAxiom :: InfoTable -> AxiomInfo -> AxiomInfo
-convertAxiom tab = over axiomType (convertNode tab)
-
 convertBuiltinTypes :: InfoTable -> InfoTable
 convertBuiltinTypes tab =
-  mapAxioms (convertAxiom tab) $
-    mapInductives (convertInductive tab) $
-      mapConstructors (convertConstructor tab) $
-        mapIdents (convertIdent tab) $
-          mapT (const (convertNode tab)) tab
+  mapAllNodes (convertNode tab) tab
diff --git a/src/Juvix/Compiler/Core/Transformation/Eta.hs b/src/Juvix/Compiler/Core/Transformation/Eta.hs
index daf96e1e4c..be2e87a1cd 100644
--- a/src/Juvix/Compiler/Core/Transformation/Eta.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Eta.hs
@@ -15,64 +15,52 @@ etaExpandBuiltins = umap go
     go n = case n of
       NBlt BuiltinApp {..}
         | builtinOpArgsNum _builtinAppOp > length _builtinAppArgs ->
-            etaExpand (builtinOpArgsNum _builtinAppOp - length _builtinAppArgs) n
+            etaExpand (substDrop _builtinAppArgs (builtinOpArgTypes _builtinAppOp)) n
       _ -> n
 
-etaExpandConstrs :: (Tag -> Int) -> Node -> Node
-etaExpandConstrs argsNum = umap go
+etaExpandConstrs :: (Tag -> [Type]) -> Node -> Node
+etaExpandConstrs getArgtys = umap go
   where
     go :: Node -> Node
     go n = case n of
       NCtr Constr {..}
-        | k > length _constrArgs ->
-            etaExpand (k - length _constrArgs) n
+        | length argtys > length _constrArgs ->
+            etaExpand (substDrop _constrArgs argtys) n
         where
-          k = argsNum _constrTag
+          argtys = getArgtys _constrTag
       _ -> n
 
-etaExpandTypeConstrs :: (Symbol -> Int) -> Node -> Node
-etaExpandTypeConstrs argsNum = umap go
+etaExpandTypeConstrs :: (Symbol -> [Type]) -> Node -> Node
+etaExpandTypeConstrs getArgtys = umap go
   where
     go :: Node -> Node
     go n = case n of
       NTyp TypeConstr {..}
-        | k > length _typeConstrArgs ->
-            etaExpand (k - length _typeConstrArgs) n
+        | length argtys > length _typeConstrArgs ->
+            etaExpand (substDrop _typeConstrArgs argtys) n
         where
-          k = argsNum _typeConstrSymbol
+          argtys = getArgtys _typeConstrSymbol
       _ -> n
 
-squashApps :: Node -> Node
-squashApps = dmap go
-  where
-    go :: Node -> Node
-    go n =
-      let (l, args) = unfoldApps' n
-       in case l of
-            NCtr (Constr i tag args') -> mkConstr i tag (args' ++ args)
-            NBlt (BuiltinApp i op args') -> mkBuiltinApp i op (args' ++ args)
-            NTyp (TypeConstr i sym args') -> mkTypeConstr i sym (args' ++ args)
-            _ -> n
-
 etaExpandApps :: InfoTable -> Node -> Node
 etaExpandApps tab =
   squashApps
-    . etaExpandTypeConstrs typeConstrArgsNum
-    . etaExpandConstrs constrArgsNum
+    . etaExpandTypeConstrs typeConstrArgtys
+    . etaExpandConstrs constrArgtys
     . etaExpandBuiltins
     . squashApps
   where
-    constrArgsNum :: Tag -> Int
-    constrArgsNum tag =
+    constrArgtys :: Tag -> [Type]
+    constrArgtys tag =
       case HashMap.lookup tag (tab ^. infoConstructors) of
-        Just ci -> ci ^. constructorArgsNum
-        Nothing -> 0
+        Just ci -> typeArgs (ci ^. constructorType)
+        Nothing -> []
 
-    typeConstrArgsNum :: Symbol -> Int
-    typeConstrArgsNum sym =
+    typeConstrArgtys :: Symbol -> [Type]
+    typeConstrArgtys sym =
       case HashMap.lookup sym (tab ^. infoInductives) of
-        Just ci -> length (ci ^. inductiveParams)
-        Nothing -> 0
+        Just ci -> map (^. paramKind) (ci ^. inductiveParams)
+        Nothing -> []
 
 etaExpansionApps :: InfoTable -> InfoTable
-etaExpansionApps tab = mapT (const (etaExpandApps tab)) tab
+etaExpansionApps tab = mapAllNodes (etaExpandApps tab) tab
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs
index 7a6fc7d1be..8213dfe4f3 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs
@@ -25,7 +25,7 @@ lambdaLiftNode aboveBl top =
     typeFromArgs :: [ArgumentInfo] -> Type
     typeFromArgs = \case
       [] -> mkDynamic' -- change this when we have type info about the body
-      (a : as) -> mkPi' (a ^. argumentType) (typeFromArgs as)
+      (a : as) -> mkPi mempty (binderFromArgumentInfo a) (typeFromArgs as)
 
     goTop :: BinderList Binder -> Node -> [LambdaLhs] -> Sem r Node
     goTop bl body = \case
@@ -77,20 +77,21 @@ lambdaLiftNode aboveBl top =
         goLetRec :: LetRec -> Sem r Recur
         goLetRec letr = do
           let defs :: [Node]
-              defs = toList (letr ^.. letRecValues . each . letItemValue)
+              defs = letr ^.. letRecValues . each . letItemValue
               ndefs :: Int
               ndefs = length defs
-          letRecBinders' :: [Binder] <- mapM (lambdaLiftBinder bl) (letr ^.. letRecValues . each . letItemBinder)
+              binders :: [Binder]
+              binders = letr ^.. letRecValues . each . letItemBinder
+          letRecBinders' :: [Binder] <- mapM (lambdaLiftBinder bl) binders
+          topSyms :: [Symbol] <- forM defs (const freshSymbol)
           let bl' :: BinderList Binder
-              -- the reverse is necessary because the last item in letRecBinders has index 0
               bl' = BL.prependRev letRecBinders' bl
-          topSyms :: [Symbol] <- forM defs (const freshSymbol)
 
-          let topNames :: [Text]
+              topNames :: [Text]
               topNames = zipWithExact uniqueName (map (^. binderName) letRecBinders') topSyms
               topSymsWithName = zipExact topSyms topNames
 
-          let recItemsFreeVars :: [(Var, Binder)]
+              recItemsFreeVars :: [(Var, Binder)]
               recItemsFreeVars = mapMaybe helper (concatMap (freeVarsCtx' bl') defs)
                 where
                   helper :: Var -> Maybe (Var, Binder)
@@ -151,8 +152,7 @@ lambdaLiftNode aboveBl top =
                         | otherwise -> impossible
                       (y : ys) -> mkLet mempty bnd' (shift k x) (goShift (k + 1) (y :| ys))
                       where
-                        bnd' = over binderType (shift k . subsCalls . shift (-ndefs)) bnd
-          -- TODO: the types should also be lambda-lifted
+                        bnd' = over binderType (shift k . subsCalls) bnd
           let res :: Node
               res = shiftHelper body' (nonEmpty' (zipExact letItems letRecBinders'))
           return (Recur res)
diff --git a/src/Juvix/Compiler/Core/Transformation/MatchToCase.hs b/src/Juvix/Compiler/Core/Transformation/MatchToCase.hs
index e6c34c7c78..c688245516 100644
--- a/src/Juvix/Compiler/Core/Transformation/MatchToCase.hs
+++ b/src/Juvix/Compiler/Core/Transformation/MatchToCase.hs
@@ -4,7 +4,6 @@ import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info.LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo (setInfoName)
-import Juvix.Compiler.Core.Info.TypeInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation.MatchToCase.Data
@@ -12,14 +11,20 @@ import Juvix.Compiler.Core.Transformation.MatchToCase.Data
 matchToCase :: InfoTable -> InfoTable
 matchToCase = run . mapT' (const (umapM matchToCaseNode))
 
+mkShiftedPis' :: [Type] -> Type -> Type
+mkShiftedPis' lhs rhs = foldl' go (shift (length lhs) rhs) (reverse (indexFrom 0 lhs))
+  where
+    go :: Type -> Indexed Type -> Type
+    go t (Indexed i a) = mkPi' (shift i a) t
+
 matchToCaseNode :: forall r. Member InfoTableBuilder r => Node -> Sem r Node
 matchToCaseNode n = case n of
   NMatch m -> do
     let branches = m ^. matchBranches
         values = toList (m ^. matchValues)
-        matchType = getInfoType (m ^. matchInfo)
-        valueTypes = (getInfoType . getInfo <$> values)
-        branchType = mkPis' valueTypes matchType
+        matchType = m ^. matchReturnType
+        valueTypes = toList (m ^. matchValueTypes)
+        branchType = mkShiftedPis' valueTypes matchType
 
     -- Index from 1 because we prepend the fail branch.
     branchNodes <-
@@ -28,10 +33,12 @@ matchToCaseNode n = case n of
 
     -- The appNode calls the first branch with the values of the match
     let appNode = mkApps' (mkVar' 0) (shift (length branchNodes) <$> values)
-    return (foldr (mkLetTy mempty branchType) appNode branchNodes)
+    let branchBinder = typeToBinder branchType
+    let branchBinders = map (branchBinder,) branchNodes
+    return (mkShiftedBinderLets 0 branchBinders appNode)
   _ -> return n
 
--- | increase all free variable indices by a given value.
+-- | Increase all free variable indices by a given value.
 -- In this function we consider indices to be embedded at a specified level
 shiftEmbedded :: Level -> Index -> Node -> Node
 shiftEmbedded _ 0 = id
@@ -110,35 +117,71 @@ shiftEmbedded wrappingLevel m = umapN go
 -- branch.
 compileMatchBranch :: forall r. Members '[InfoTableBuilder] r => Indexed MatchBranch -> Sem r Node
 compileMatchBranch (Indexed branchNum br) = do
-  compiledBranch <- runReader initState' (combineCompiledPatterns (map (compilePattern patternsNum) patterns))
-  return (mkLambdasTy (patternType <$> patterns) ((compiledBranch ^. compiledPatMkNode) (wrapBody (compiledBranch ^. compiledPatBinders))))
+  compiledBranch <- runReader initState (combineCompiledPatterns (map (compilePattern 0 branchNum patternsNum) patterns))
+  return (mkShiftedLambdas branchNum shiftedPatternTypes ((compiledBranch ^. compiledPatMkNode) (wrapBody (compiledBranch ^. compiledPatBinders))))
   where
     patterns :: [Pattern]
     patterns = toList (br ^. matchBranchPatterns)
 
+    patternsNum :: Int
     patternsNum = length patterns
 
+    patternBindersNumList :: [Int]
+    patternBindersNumList = map (length . getPatternBinders) patterns
+
+    accumPatternBindersNum :: [Int]
+    accumPatternBindersNum = init (scanl (+) 0 patternBindersNumList)
+
+    shiftedPatternTypes :: [Type]
+    shiftedPatternTypes = [shift (-n) b | (n, b) <- zipExact accumPatternBindersNum (map patternType patterns)]
+
     wrapBody :: [CompiledBinder] -> Node
     wrapBody binders = foldr (uncurry (mkLet mempty)) shiftedBody vars
       where
         vars :: [(Binder, Node)]
-        vars = second mkVar' . swap . toTuple <$> extractOriginalBinders binders
+        vars = (bimap (shiftBinder patternBindersNum') mkVar' . swap . toTuple) <$> extractOriginalBinders binders
+
+        auxiliaryBindersNum :: Int
+        auxiliaryBindersNum = length (filter isAuxiliaryBinder binders)
+
+        patternBindersNum' :: Int
+        patternBindersNum' = sum patternBindersNumList
 
         shiftedBody :: Node
         shiftedBody =
-          let patternBindersNum' = length (concatMap getPatternBinders patterns)
-              auxiliaryBindersNum = length (filter isAuxiliaryBinder binders)
-           in shiftEmbedded
-                patternBindersNum'
-                (auxiliaryBindersNum + patternBindersNum' + patternsNum + branchNum)
-                (br ^. matchBranchBody)
-
-    initState' :: CompileState
-    initState' =
-      CompileState
-        { _compileStateBindersAbove = 0,
-          _compileStateCompiledPattern = mempty
-        }
+          shiftEmbedded
+            patternBindersNum'
+            (auxiliaryBindersNum + patternBindersNum' + patternsNum + branchNum)
+            (br ^. matchBranchBody)
+
+-- | Increase the indices of free variables in the binderTyped by a given value
+shiftBinder :: Index -> Binder -> Binder
+shiftBinder idx = over binderType (shift idx)
+
+-- | Make a sequence of nested lets from a list of binders / value pairs. The
+-- indices of free variables in binder types are shifted by the sum of
+-- `baseShift` and the number of lets that have already been added in the
+-- sequence.
+mkShiftedBinderLets :: Index -> [(Binder, Node)] -> Node -> Node
+mkShiftedBinderLets baseShift vars body = foldr f body (indexFrom 0 vars)
+  where
+    f :: Indexed (Binder, Node) -> Node -> Node
+    f (Indexed idx (b, v)) = mkLet mempty (shiftBinder (baseShift + idx) b) v
+
+mkShiftedLambdas :: Index -> [Type] -> Node -> Node
+mkShiftedLambdas baseShift tys body = foldr f body (indexFrom 0 tys)
+  where
+    f :: Indexed Type -> Node -> Node
+    f (Indexed idx ty) = mkLambda' (shift (baseShift + idx) ty)
+
+-- | Wrap a type node in an unnamed binder.
+typeToBinder :: Type -> Binder
+typeToBinder ty =
+  Binder
+    { _binderName = "?",
+      _binderLocation = Nothing,
+      _binderType = ty
+    }
 
 -- | Extract original binders (i.e binders which are referenced in the match
 -- branch body) from a list of `CompiledBinder`s indexed by the total number
@@ -187,13 +230,14 @@ combineCompiledPatterns ps = go indexedPatterns
 -- (wildcard, binder or constructor) introduces an auxiliary binder.
 -- The arguments are then compiled recursively using a new CompileState context.
 -- The default case points to the next branch pattern.
-compilePattern :: forall r. Members [Reader CompileState, Reader CompileStateNode, InfoTableBuilder] r => Int -> Pattern -> Sem r CompiledPattern
-compilePattern numPatterns = \case
+compilePattern :: forall r. Members [Reader CompileState, Reader CompileStateNode, InfoTableBuilder] r => Int -> Int -> Int -> Pattern -> Sem r CompiledPattern
+compilePattern baseShift branchNum numPatterns = \case
   PatWildcard {} -> return (CompiledPattern [] id)
   PatBinder b -> do
-    subPats <- resetCurrentNode (incBindersAbove (compilePattern numPatterns (b ^. patternBinderPattern)))
+    subPats <- resetCurrentNode (incBindersAbove (compilePattern baseShift branchNum numPatterns (b ^. patternBinderPattern)))
+    auxPatternsNum <- length . filter isAuxiliaryBinder <$> asks (^. compileStateCompiledPattern . compiledPatBinders)
     currentNode <- asks (^. compileStateNodeCurrent)
-    let newBinder = b ^. patternBinder
+    let newBinder = shiftBinder (baseShift + branchNum + numPatterns + auxPatternsNum) (b ^. patternBinder)
     let compiledBinder =
           CompiledPattern
             { _compiledPatBinders = [OriginalBinder newBinder],
@@ -208,41 +252,31 @@ compilePattern numPatterns = \case
     where
       compileCase :: [Pattern] -> Sem r CompiledPattern
       compileCase args = do
-        binders <- mapM mkBinder args
+        binders <- mapM mkBinder'' args
         CompiledPattern <$> mapM mkCompiledBinder args <*> mkCaseFromBinders binders
 
       compileArgs :: [Pattern] -> Sem r CompiledPattern
       compileArgs args = do
-        bindersAbove <- asks (^. compileStateBindersAbove)
-        let ctorArgsPatterns = compilePattern numPatterns <$> args
-            state = mkState bindersAbove
-        runReader state (combineCompiledPatterns ctorArgsPatterns)
-        where
-          mkState :: Int -> CompileState
-          mkState bindersAbove =
-            ( CompileState
-                { _compileStateBindersAbove = bindersAbove + length args,
-                  _compileStateCompiledPattern = mempty
-                }
-            )
+        let ctorArgsPatterns = compilePattern (length args) branchNum numPatterns <$> args
+        addBindersAbove (length args) (resetCompiledPattern (combineCompiledPatterns ctorArgsPatterns))
 
       mkCompiledBinder :: Pattern -> Sem r CompiledBinder
-      mkCompiledBinder p = AuxiliaryBinder <$> mkBinder p
+      mkCompiledBinder p = AuxiliaryBinder <$> mkBinder'' p
 
-      mkBinder :: Pattern -> Sem r Binder
-      mkBinder = \case
+      mkBinder'' :: Pattern -> Sem r Binder
+      mkBinder'' = \case
         PatBinder b -> return (b ^. patternBinder)
         PatWildcard w -> do
           let info = w ^. patternWildcardInfo
           return
             Binder
-              { _binderName = "_",
+              { _binderName = "?",
                 _binderLocation = getInfoLocation info,
-                _binderType = getInfoType info
+                _binderType = mkDynamic'
               }
         PatConstr c' -> do
           let info = c' ^. patternConstrInfo
-          mkUniqueBinder "arg" (getInfoLocation info) (getInfoType info)
+          mkUniqueBinder "arg" (getInfoLocation info) mkDynamic'
 
       mkCaseFromBinders :: [Binder] -> Sem r (Node -> Node)
       mkCaseFromBinders binders = do
@@ -277,7 +311,7 @@ compilePattern numPatterns = \case
               )
 
 failNode :: [Type] -> Node
-failNode tys = mkLambdasTy tys (mkBuiltinApp' OpFail [mkConstant' (ConstString "Non-exhaustive patterns")])
+failNode tys = mkShiftedLambdas 0 tys (mkBuiltinApp' OpFail [mkConstant' (ConstString "Non-exhaustive patterns")])
 
 mkUniqueBinder' :: Member InfoTableBuilder r => Text -> Node -> Sem r Binder
 mkUniqueBinder' name ty = mkUniqueBinder name Nothing ty
diff --git a/src/Juvix/Compiler/Core/Transformation/MatchToCase/Data.hs b/src/Juvix/Compiler/Core/Transformation/MatchToCase/Data.hs
index b01b576d79..221c6832bc 100644
--- a/src/Juvix/Compiler/Core/Transformation/MatchToCase/Data.hs
+++ b/src/Juvix/Compiler/Core/Transformation/MatchToCase/Data.hs
@@ -46,26 +46,18 @@ data CompileState = CompileState
 newtype CompileStateNode = CompileStateNode
   {_compileStateNodeCurrent :: Node}
 
-initState :: CompileState
-initState =
-  CompileState
-    { _compileStateBindersAbove = 0,
-      _compileStateCompiledPattern =
-        CompiledPattern
-          { _compiledPatBinders = [],
-            _compiledPatMkNode = id
-          }
-    }
-
-stateWithBindersAbove :: Int -> CompileState
-stateWithBindersAbove n = initState {_compileStateBindersAbove = n}
-
 makeLenses ''CompiledPattern
 makeLenses ''CompileState
 makeLenses ''CompileStateNode
 
+addBindersAbove :: Member (Reader CompileState) r => Int -> Sem r CompiledPattern -> Sem r CompiledPattern
+addBindersAbove bindersNum = local (over compileStateBindersAbove (+ bindersNum))
+
 incBindersAbove :: Member (Reader CompileState) r => Sem r CompiledPattern -> Sem r CompiledPattern
-incBindersAbove = local (over compileStateBindersAbove (+ 1))
+incBindersAbove = addBindersAbove 1
+
+resetCompiledPattern :: Member (Reader CompileState) r => Sem r CompiledPattern -> Sem r CompiledPattern
+resetCompiledPattern = local (set compileStateCompiledPattern mempty)
 
 resetCurrentNode :: Member (Reader CompileStateNode) r => Sem r CompiledPattern -> Sem r CompiledPattern
 resetCurrentNode = local (set compileStateNodeCurrent (mkVar' 0))
@@ -83,3 +75,13 @@ instance Monoid CompiledPattern where
       { _compiledPatBinders = [],
         _compiledPatMkNode = id
       }
+
+initState :: CompileState
+initState =
+  CompileState
+    { _compileStateBindersAbove = 0,
+      _compileStateCompiledPattern = mempty
+    }
+
+stateWithBindersAbove :: Int -> CompileState
+stateWithBindersAbove n = initState {_compileStateBindersAbove = n}
diff --git a/src/Juvix/Compiler/Core/Transformation/NatToInt.hs b/src/Juvix/Compiler/Core/Transformation/NatToInt.hs
index 41946575bc..07bc7d254c 100644
--- a/src/Juvix/Compiler/Core/Transformation/NatToInt.hs
+++ b/src/Juvix/Compiler/Core/Transformation/NatToInt.hs
@@ -24,15 +24,28 @@ convertNode tab = convert [] 0
       NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) ->
         Recur' (levels, convertIdentApp node (\g -> g _identInfo l r) _identSymbol)
       NApp (App _ (NIdt (Ident {..})) l) ->
-        Recur' (levels, convertIdentApp node (\g -> mkLet' l $ mkLambdaTy mkTypeInteger' $ g _identInfo (mkVar' 1) (mkVar' 0)) _identSymbol)
+        Recur'
+          ( levels,
+            convertIdentApp
+              node
+              ( \g ->
+                  mkLet' mkTypeInteger' l $
+                    mkLambda' mkTypeInteger' $
+                      g _identInfo (mkVar' 1) (mkVar' 0)
+              )
+              _identSymbol
+          )
+      NIdt (Ident {..})
+        | Just _identSymbol == tab ^. infoIntToNat ->
+            End' (mkLambda' mkTypeInteger' (mkVar' 0))
       NIdt (Ident {..}) ->
         Recur'
           ( levels,
             convertIdentApp
               node
               ( \g ->
-                  mkLambdaTy mkTypeInteger' $
-                    mkLambdaTy mkTypeInteger' $
+                  mkLambda' mkTypeInteger' $
+                    mkLambda' mkTypeInteger' $
                       g _identInfo (mkVar' 1) (mkVar' 0)
               )
               _identSymbol
@@ -48,7 +61,7 @@ convertNode tab = convert [] 0
       NCase (Case {..}) ->
         let ii = fromJust $ HashMap.lookup _caseInductive (tab ^. infoInductives)
          in case ii ^. inductiveBuiltin of
-              Just BuiltinNat ->
+              Just (BuiltinTypeInductive BuiltinNat) ->
                 case _caseBranches of
                   [br] -> makeIf br (maybeBranch _caseDefault)
                   [br1, br2] ->
@@ -94,7 +107,7 @@ convertNode tab = convert [] 0
             Just BuiltinNatSub ->
               f
                 ( \info x y ->
-                    mkLet' (mkBuiltinApp info OpIntSub [x, y]) $
+                    mkLet' mkTypeInteger' (mkBuiltinApp info OpIntSub [x, y]) $
                       mkIf'
                         boolSymbol
                         (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar' 0])
@@ -123,6 +136,6 @@ natToInt tab = mapT (const (convertNode tab')) tab'
     tab' =
       case tab ^. infoIntToNat of
         Just sym ->
-          tab {_identContext = HashMap.insert sym (mkLambda' (mkVar' 0)) (tab ^. identContext)}
+          tab {_identContext = HashMap.insert sym (mkLambda' mkTypeInteger' (mkVar' 0)) (tab ^. identContext)}
         Nothing ->
           tab
diff --git a/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs b/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
index d933626dcb..f3f0e74c82 100644
--- a/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
+++ b/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
@@ -7,13 +7,22 @@ where
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.Base
 
+isTypeConstr :: InfoTable -> Type -> Bool
+isTypeConstr tab ty = case typeTarget ty of
+  NUniv {} ->
+    True
+  NIdt Ident {..} ->
+    isTypeConstr tab (fromJust $ HashMap.lookup _identSymbol (tab ^. identContext))
+  _ -> False
+
 convertNode :: InfoTable -> Node -> Node
 convertNode tab = convert mempty
   where
-    unsupported :: forall a. a
-    unsupported = error "remove type arguments: unsupported node"
+    unsupported :: forall a. Node -> a
+    unsupported node = error ("remove type arguments: unsupported node\n\t" <> ppTrace node)
 
     convert :: BinderList Binder -> Node -> Node
     convert vars = dmapLR' (vars, go)
@@ -23,11 +32,18 @@ convertNode tab = convert mempty
       NVar v@(Var {..}) ->
         let ty = BL.lookup _varIndex vars ^. binderType
          in if
-                | isTypeConstr ty -> End (mkDynamic _varInfo)
+                | isTypeConstr tab ty -> End (mkDynamic _varInfo)
                 | otherwise -> End (NVar (shiftVar (-k) v))
         where
-          k = length (filter (isTypeConstr . (^. binderType)) (take _varIndex (toList vars)))
-      NApp (App {}) ->
+          k = length (filter (isTypeConstr tab . (^. binderType)) (take _varIndex (toList vars)))
+      NIdt Ident {..} ->
+        let fi = fromJust $ HashMap.lookup _identSymbol (tab ^. infoIdentifiers)
+         in if
+                | isTypeConstr tab (fi ^. identifierType) ->
+                    Recur (fromJust $ HashMap.lookup _identSymbol (tab ^. identContext))
+                | otherwise ->
+                    Recur node
+      NApp App {..} ->
         let (h, args) = unfoldApps node
             ty =
               case h of
@@ -36,9 +52,11 @@ convertNode tab = convert mempty
                 NIdt (Ident {..}) ->
                   let fi = fromJust $ HashMap.lookup _identSymbol (tab ^. infoIdentifiers)
                    in fi ^. identifierType
-                _ -> unsupported
+                _ -> unsupported node
             args' = filterArgs ty args
          in if
+                | isTypeConstr tab ty ->
+                    End (mkDynamic _appInfo)
                 | null args' ->
                     End (convert vars h)
                 | otherwise ->
@@ -51,12 +69,21 @@ convertNode tab = convert mempty
       NCase (Case {..}) ->
         End (mkCase _caseInfo _caseInductive (convert vars _caseValue) (map convertBranch _caseBranches) (fmap (convert vars) _caseDefault))
         where
+          nParams :: Int
+          nParams = maybe 0 (length . (^. inductiveParams)) (tab ^. infoInductives . at _caseInductive)
           convertBranch :: CaseBranch -> CaseBranch
           convertBranch br@CaseBranch {..} =
-            let binders' = filterBinders vars _caseBranchBinders
+            let paramBinders = map (set binderType mkSmallUniv) (take nParams _caseBranchBinders)
+                argBinders = drop nParams _caseBranchBinders
+                tyargs = drop nParams (typeArgs (fromJust (tab ^. infoConstructors . at _caseBranchTag) ^. constructorType))
+                argBinders' = zipWith (\b ty -> if isDynamic (b ^. binderType) && isTypeConstr tab ty then set binderType ty b else b) argBinders (tyargs ++ repeat mkDynamic')
+                binders' =
+                  filterBinders
+                    (BL.prependRev paramBinders vars)
+                    argBinders'
                 body' =
                   convert
-                    (BL.prependRev _caseBranchBinders vars)
+                    (BL.prependRev argBinders' (BL.prependRev paramBinders vars))
                     _caseBranchBody
              in br
                   { _caseBranchBinders = binders',
@@ -66,22 +93,25 @@ convertNode tab = convert mempty
           filterBinders :: BinderList Binder -> [Binder] -> [Binder]
           filterBinders _ [] = []
           filterBinders vars' (b : bs)
-            | isTypeConstr (b ^. binderType) =
+            | isTypeConstr tab (b ^. binderType) =
                 filterBinders (BL.cons b vars') bs
           filterBinders vars' (b : bs) =
             over binderType (convert vars') b : filterBinders (BL.cons b vars') bs
       NLam (Lambda {..})
-        | isTypeConstr (_lambdaBinder ^. binderType) ->
+        | isTypeConstr tab (_lambdaBinder ^. binderType) ->
             End (convert (BL.cons _lambdaBinder vars) _lambdaBody)
+      NLet (Let {..})
+        | isTypeConstr tab (_letItem ^. letItemBinder . binderType) ->
+            End (convert (BL.cons (_letItem ^. letItemBinder) vars) _letBody)
       NPi (Pi {..})
-        | isTypeConstr (_piBinder ^. binderType) && not (isTypeConstr _piBody) ->
+        | isTypeConstr tab (_piBinder ^. binderType) && not (isTypeConstr tab _piBody) ->
             End (convert (BL.cons _piBinder vars) _piBody)
       _ -> Recur node
       where
         filterArgs :: Type -> [a] -> [a]
         filterArgs ty args =
           map fst $
-            filter (not . isTypeConstr . snd) (zip args (typeArgs ty ++ repeat mkDynamic'))
+            filter (not . isTypeConstr tab . snd) (zip args (typeArgs ty ++ repeat mkDynamic'))
 
 convertIdent :: InfoTable -> IdentifierInfo -> IdentifierInfo
 convertIdent tab ii =
@@ -91,7 +121,7 @@ convertIdent tab ii =
         map (uncurry (set argumentType)) $
           zipExact tyargs' $
             map fst $
-              filter (not . isTypeConstr . snd) (zipExact (ii ^. identifierArgsInfo) tyargs),
+              filter (not . isTypeConstr tab . snd) (zipExact (ii ^. identifierArgsInfo) tyargs),
       _identifierArgsNum = length (typeArgs ty')
     }
   where
@@ -112,7 +142,7 @@ convertInductive :: InfoTable -> InductiveInfo -> InductiveInfo
 convertInductive tab ii =
   ii
     { _inductiveKind = ty',
-      _inductiveParams = map (over paramKind (convertNode tab) . fst) $ filter (not . isTypeConstr . snd) (zipExact (ii ^. inductiveParams) tyargs),
+      _inductiveParams = map (over paramKind (convertNode tab) . fst) $ filter (not . isTypeConstr tab . snd) (zipExact (ii ^. inductiveParams) tyargs),
       _inductiveConstructors = map (convertConstructor tab) (ii ^. inductiveConstructors)
     }
   where
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index 353ecc0593..4f8bcfcbfc 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Translation.FromInternal where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.List.NonEmpty (fromList)
+import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Abstract.Data.Name
 import Juvix.Compiler.Concrete.Data.Literal (LiteralLoc)
 import Juvix.Compiler.Core.Data
@@ -10,7 +11,6 @@ import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo
 import Juvix.Compiler.Core.Language
-import Juvix.Compiler.Core.Transformation.Eta (etaExpandApps)
 import Juvix.Compiler.Core.Translation.FromInternal.Data
 import Juvix.Compiler.Internal.Extra qualified as Internal
 import Juvix.Compiler.Internal.Translation.Extra qualified as Internal
@@ -18,9 +18,6 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qu
 import Juvix.Data.Loc qualified as Loc
 import Juvix.Extra.Strings qualified as Str
 
-unsupported :: Text -> a
-unsupported thing = error ("Internal to Core: Not yet supported: " <> thing)
-
 -- Translation of a Name into the identifier index used in the Core InfoTable
 mkIdentIndex :: Name -> Text
 mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
@@ -47,28 +44,28 @@ setupIntToNat sym tab =
                   _argumentIsImplicit = Explicit
                 }
             ],
-          _identifierType = mkDynamic',
+          _identifierType = mkPi' mkTypeInteger' mkTypeInteger',
           _identifierIsExported = False,
           _identifierBuiltin = Nothing
         }
     node =
       case (tagZeroM, tagSucM, boolSymM) of
         (Just tagZero, Just tagSuc, Just boolSym) ->
-          mkLambda' $
+          mkLambda' mkTypeInteger' $
             mkIf'
               boolSym
               (mkBuiltinApp' OpEq [mkVar' 0, mkConstant' (ConstInteger 0)])
               (mkConstr (setInfoName "zero" mempty) tagZero [])
               (mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
         _ ->
-          mkLambda' $ mkVar' 0
+          mkLambda' mkTypeInteger' $ mkVar' 0
     tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
     tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
     boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
 
 fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
 fromInternal i = do
-  (res, _) <- runInfoTableBuilder tab0 (runReader (i ^. InternalTyped.resultIdenTypes) f)
+  (res, _) <- runInfoTableBuilder tab0 (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
   return $
     CoreResult
       { _coreResultTable = setupIntToNat intToNatSym res,
@@ -81,13 +78,12 @@ fromInternal i = do
     intToNatSym :: Symbol
     intToNatSym = 0
 
-    f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable] r) => Sem r ()
+    f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) => Sem r ()
     f = do
-      declareIOBuiltins
       let resultModules = toList (i ^. InternalTyped.resultModules)
       runReader (Internal.buildTable resultModules) (mapM_ coreModule resultModules)
       where
-        coreModule :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) => Internal.Module -> Sem r ()
+        coreModule :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) => Internal.Module -> Sem r ()
         coreModule m = do
           registerInductiveDefs m
           registerFunctionDefs m
@@ -100,22 +96,25 @@ fromInternalExpression res exp = do
       (Internal.buildTable modules)
       ( runInfoTableBuilder
           (res ^. coreResultTable)
-          ( runReader
-              (res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
-              (runReader initIndexTable (goExpression exp))
+          ( evalState
+              (res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions)
+              ( runReader
+                  (res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
+                  (runReader initIndexTable (goExpression exp))
+              )
           )
       )
 
 registerInductiveDefs ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.Module ->
   Sem r ()
 registerInductiveDefs m = registerInductiveDefsBody (m ^. Internal.moduleBody)
 
 registerInductiveDefsBody ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.ModuleBody ->
   Sem r ()
 registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
@@ -131,14 +130,14 @@ registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
 
 registerFunctionDefs ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.Module ->
   Sem r ()
 registerFunctionDefs m = registerFunctionDefsBody (m ^. Internal.moduleBody)
 
 registerFunctionDefsBody ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.ModuleBody ->
   Sem r ()
 registerFunctionDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
@@ -152,28 +151,43 @@ registerFunctionDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
 
 goInductiveDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.InductiveDef ->
   Sem r ()
 goInductiveDef i = do
   sym <- freshSymbol
-  ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
-  let info =
+  let params =
+        map
+          ( \p ->
+              ParameterInfo
+                { _paramName = p ^. Internal.inductiveParamName . nameText,
+                  _paramLocation = Just $ p ^. Internal.inductiveParamName . nameLoc,
+                  _paramIsImplicit = False, -- TODO: not currently easily available in Internal
+                  _paramKind = mkSmallUniv
+                }
+          )
+          (i ^. Internal.inductiveParameters)
+      info =
         InductiveInfo
           { _inductiveName = i ^. Internal.inductiveName . nameText,
             _inductiveLocation = Just $ i ^. Internal.inductiveName . nameLoc,
             _inductiveSymbol = sym,
-            _inductiveKind = mkDynamic',
-            _inductiveConstructors = ctorInfos,
-            _inductiveParams = [],
+            _inductiveKind = mkSmallUniv,
+            _inductiveConstructors = [],
+            _inductiveParams = params,
             _inductivePositive = i ^. Internal.inductivePositive,
-            _inductiveBuiltin = i ^. Internal.inductiveBuiltin
+            _inductiveBuiltin = fmap BuiltinTypeInductive (i ^. Internal.inductiveBuiltin)
           }
-  registerInductive (mkIdentIndex (i ^. Internal.inductiveName)) info
+      idx = mkIdentIndex (i ^. Internal.inductiveName)
+  -- The inductive needs to be registered before translating the constructors,
+  -- because their types refer to the inductive
+  registerInductive idx info
+  ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
+  registerInductive idx info {_inductiveConstructors = ctorInfos}
 
 goConstructor ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
   Symbol ->
   Internal.InductiveConstructorDef ->
   Sem r ConstructorInfo
@@ -219,7 +233,7 @@ goConstructor sym ctor = do
       runReader
         initIndexTable
         ( Internal.constructorType ctorName
-            >>= goExpression
+            >>= goType
         )
 
     argsNum :: Sem r Int
@@ -229,32 +243,43 @@ goConstructor sym ctor = do
 
 goMutualBlock ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.MutualBlock ->
   Sem r ()
 goMutualBlock m = do
   funcsWithSym <- mapM withSym (m ^. Internal.mutualFunctions)
-  mapM_ goFunctionDefIden funcsWithSym
-  mapM_ goFunctionDef funcsWithSym
+  tys <- mapM goFunctionDefIden funcsWithSym
+  mapM_ goFunctionDef (zipExact (toList funcsWithSym) (toList tys))
   where
     withSym :: a -> Sem r (a, Symbol)
     withSym x = do
       sym <- freshSymbol
       return (x, sym)
 
+goType ::
+  forall r.
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader IndexTable] r) =>
+  Internal.Expression ->
+  Sem r Type
+goType ty = do
+  normTy <- evalState InternalTyped.iniState (InternalTyped.strongNormalize' ty)
+  squashApps <$> goExpression normTy
+
 goFunctionDefIden ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
   (Internal.FunctionDef, Symbol) ->
-  Sem r ()
+  Sem r Type
 goFunctionDefIden (f, sym) = do
-  funTy <- runReader initIndexTable (goExpression (f ^. Internal.funDefType))
+  funTy <- runReader initIndexTable (goType (f ^. Internal.funDefType))
   let info =
         IdentifierInfo
           { _identifierName = f ^. Internal.funDefName . nameText,
             _identifierLocation = Just $ f ^. Internal.funDefName . nameLoc,
             _identifierSymbol = sym,
             _identifierType = funTy,
+            -- _identiferArgsNum needs to match the number of lambdas in the
+            -- body. This needs to be filled in later (in goFunctionDef).
             _identifierArgsNum = 0,
             _identifierArgsInfo = [],
             _identifierIsExported = False,
@@ -262,97 +287,170 @@ goFunctionDefIden (f, sym) = do
           }
   registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info
   when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym)
+  return funTy
 
 goFunctionDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
-  (Internal.FunctionDef, Symbol) ->
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
+  ((Internal.FunctionDef, Symbol), Type) ->
   Sem r ()
-goFunctionDef (f, sym) = do
+goFunctionDef ((f, sym), ty) = do
   mbody <- case f ^. Internal.funDefBuiltin of
     Just Internal.BuiltinBoolIf -> return Nothing
-    Just _ -> Just <$> runReader initIndexTable (mkFunBody f)
-    Nothing -> Just <$> runReader initIndexTable (mkFunBody f)
+    Just _ -> Just <$> runReader initIndexTable (mkFunBody ty f)
+    Nothing -> Just <$> runReader initIndexTable (mkFunBody ty f)
   forM_ mbody (registerIdentNode sym)
+  forM_ mbody setIdentArgsInfo'
+  where
+    setIdentArgsInfo' :: Node -> Sem r ()
+    setIdentArgsInfo' node = do
+      let (is, _) = unfoldLambdas node
+      setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
 
 mkFunBody ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  Type -> -- converted type of the function
   Internal.FunctionDef ->
   Sem r Node
-mkFunBody f
-  | nPatterns == 0 = goExpression (f ^. Internal.funDefClauses . _head1 . Internal.clauseBody)
+mkFunBody ty f =
+  mkBody ty (fmap (\c -> (c ^. Internal.clausePatterns, c ^. Internal.clauseBody)) (f ^. Internal.funDefClauses))
+
+mkBody ::
+  forall r.
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  Type -> -- type of the function
+  NonEmpty ([Internal.PatternArg], Internal.Expression) ->
+  Sem r Node
+mkBody ty clauses
+  | nPatterns == 0 = goExpression (snd (head clauses))
   | otherwise = do
-      let values :: [Node]
-          values = mkVar Info.empty <$> vs
-      ms <-
-        local
-          (over indexTableVarsNum (+ nPatterns))
-          (mapM goFunctionClause (f ^. Internal.funDefClauses))
-      let match = mkMatch' (fromList values) (toList ms)
-      return $ foldr (\_ n -> mkLambda' n) match vs
+      let values = mkVar Info.empty <$> vs
+          argtys = take nPatterns (typeArgs ty)
+          values' = map fst $ filter (isInductive . snd) (zipExact values argtys)
+          matchArgtys = shiftMatchTypeArg <$> indexFrom 0 argtys
+          matchTypeTarget = typeTarget ty
+          matchIndArgTys = filter isInductive matchArgtys
+          matchReturnType' = mkPis' (drop nPatterns (typeArgs ty)) matchTypeTarget
+      case values' of
+        [] -> do
+          vars <- asks (^. indexTableVars)
+          varsNum <- asks (^. indexTableVarsNum)
+          let (pats, body) = head clauses
+              (vars', varsNum') =
+                foldl'
+                  (\(vrs, k) pat -> (addPatternVariableNames pat k vrs, k + 1))
+                  (vars, varsNum)
+                  pats
+          body' <-
+            local
+              (set indexTableVars vars' . set indexTableVarsNum varsNum')
+              (goExpression body)
+          return $ foldr mkLambda' body' argtys
+        _ : _ -> do
+          varsNum <- asks (^. indexTableVarsNum)
+          ms <- underBinders nPatterns (mapM (uncurry (goClause varsNum)) clauses)
+          let match = mkMatch' (fromList matchIndArgTys) matchReturnType' (fromList values') (toList ms)
+          return $ foldr mkLambda' match argtys
   where
     -- Assumption: All clauses have the same number of patterns
     nPatterns :: Int
-    nPatterns = length (f ^. Internal.funDefClauses . _head1 . Internal.clausePatterns)
+    nPatterns = checkPatternsNum (length (fst (head clauses))) (NonEmpty.tail $ fmap fst clauses)
 
     vs :: [Index]
     vs = reverse (take nPatterns [0 ..])
 
+    -- The types of arguments in the match must be shifted due to the
+    -- difference in level between when the type argument in bound (in a
+    -- surrounding lambda) and when it is used in the match constructor.
+    --
+    -- For example:
+    --
+    --    f : {A : Type} -> A -> List A -> A -> A -> List A;
+    --    f _ _ _ := \ { _ := nil };
+    --
+    -- f has the following type, with indices:
+    --
+    --    A -> A$0 -> List A$1 -> A$2 -> A$3 -> A$4 -> List A$5
+    --
+    -- Is translated to the following match (omiting the translation of the body):
+    --
+    --    λ(? : Type)
+    --      λ(? : A$0)
+    --        λ(? : List A$1)
+    --          λ(? : A$2)
+    --            λ(? : A$3)
+    --              match (?$2 : List A$4) with : (A$4 → List A$5)
+    --
+    -- The return type (A$4 -> List A$5) already has the correct indices
+    -- relative to the match node. However the type of the match argument has
+    -- been shifted by the number of pattern binders below it.
+    shiftMatchTypeArg :: Indexed Type -> Type
+    shiftMatchTypeArg (Indexed idx ty') = shift (nPatterns - idx) ty'
+
+    checkPatternsNum :: Int -> [[a]] -> Int
+    checkPatternsNum len = \case
+      [] -> len
+      ps : pats | length ps == len -> checkPatternsNum len pats
+      _ -> error "internal-to-core: all clauses must have the same number of patterns"
+
+    goClause :: Level -> [Internal.PatternArg] -> Internal.Expression -> Sem r MatchBranch
+    goClause lvl pats body = goPatternArgs lvl body pats ptys
+      where
+        ptys :: [Type]
+        ptys = take (length pats) (typeArgs ty)
+
 goCase ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   Internal.Case ->
   Sem r Node
 goCase c = do
   expr <- goExpression (c ^. Internal.caseExpression)
-  branches <- toList <$> mapM goCaseBranch (c ^. Internal.caseBranches)
-  return (mkMatch' (pure expr) branches)
-
-goCaseBranch ::
-  forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
-  Internal.CaseBranch ->
-  Sem r MatchBranch
-goCaseBranch b = goPatternArgs (b ^. Internal.caseBranchExpression) [b ^. Internal.caseBranchPattern]
-
-underBinders :: Members '[Reader IndexTable] r => Int -> Sem r a -> Sem r a
-underBinders nBinders = local (over indexTableVarsNum (+ nBinders))
+  ty <- goType (fromJust $ c ^. Internal.caseExpressionType)
+  case ty of
+    NTyp {} -> do
+      branches <- toList <$> mapM (goCaseBranch ty) (c ^. Internal.caseBranches)
+      rty <- goType (fromJust $ c ^. Internal.caseExpressionWholeType)
+      return (mkMatch' (NonEmpty.singleton ty) rty (pure expr) branches)
+    _ ->
+      case c ^. Internal.caseBranches of
+        Internal.CaseBranch {..} :| _ ->
+          case _caseBranchPattern ^. Internal.patternArgPattern of
+            Internal.PatternVariable {} -> do
+              vars <- asks (^. indexTableVars)
+              varsNum <- asks (^. indexTableVarsNum)
+              let vars' = addPatternVariableNames _caseBranchPattern varsNum vars
+              body <-
+                local
+                  (set indexTableVars vars')
+                  (underBinders 1 (goExpression _caseBranchExpression))
+              return $ mkLet' ty expr body
+            _ ->
+              impossible
+  where
+    goCaseBranch :: Type -> Internal.CaseBranch -> Sem r MatchBranch
+    goCaseBranch ty b = goPatternArgs 0 (b ^. Internal.caseBranchExpression) [b ^. Internal.caseBranchPattern] [ty]
 
 goLambda ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   Internal.Lambda ->
   Sem r Node
 goLambda l = do
-  ms <- underBinders nPatterns (mapM goLambdaClause (l ^. Internal.lambdaClauses))
-  let values = reverse (take nPatterns (mkVar' <$> [0 ..]))
-      match = mkMatch' (fromList values) (toList ms)
-  return $ foldr (\_ n -> mkLambda' n) match values
-  where
-    nPatterns :: Int
-    nPatterns = length (l ^. Internal.lambdaClauses . _head1 . Internal.lambdaPatterns)
-
-goLambdaClause ::
-  forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
-  Internal.LambdaClause ->
-  Sem r MatchBranch
-goLambdaClause clause = goPatternArgs (clause ^. Internal.lambdaBody) ps
-  where
-    ps :: [Internal.PatternArg]
-    ps = toList (clause ^. Internal.lambdaPatterns)
+  ty <- goType (fromJust (l ^. Internal.lambdaType))
+  mkBody ty (fmap (\c -> (toList (c ^. Internal.lambdaPatterns), c ^. Internal.lambdaBody)) (l ^. Internal.lambdaClauses))
 
 goLet ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   Internal.Let ->
   Sem r Node
 goLet l = do
   vars <- asks (^. indexTableVars)
   varsNum <- asks (^. indexTableVarsNum)
   let bs :: [Name]
-      bs = map (\(Internal.LetFunDef (Internal.FunctionDef {..})) -> _funDefName) (toList $ l ^. Internal.letClauses)
+      bs = map (\(Internal.LetFunDef Internal.FunctionDef {..}) -> _funDefName) (toList $ l ^. Internal.letClauses)
       (vars', varsNum') =
         foldl'
           ( \(vs, k) name ->
@@ -360,26 +458,27 @@ goLet l = do
           )
           (vars, varsNum)
           bs
-  (defs, value) <-
-    local
-      (set indexTableVars vars' . set indexTableVarsNum varsNum')
-      ( do
-          a <- mapM goLetClause (l ^. Internal.letClauses)
-          b <- goExpression (l ^. Internal.letExpression)
-          return (a, b)
-      )
-  return $ mkLetRec' defs value
+  (defs, value) <- do
+    values <-
+      mapM
+        ( \(Internal.LetFunDef f) -> do
+            funTy <- goType (f ^. Internal.funDefType)
+
+            funBody <- local (set indexTableVars vars' . set indexTableVarsNum varsNum') (mkFunBody funTy f)
+            return (funTy, funBody)
+        )
+        (l ^. Internal.letClauses)
 
-goLetClause ::
-  forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
-  Internal.LetClause ->
-  Sem r Node
-goLetClause (Internal.LetFunDef f) = mkFunBody f
+    lbody <-
+      local
+        (set indexTableVars vars' . set indexTableVarsNum varsNum')
+        (goExpression (l ^. Internal.letExpression))
+    return (values, lbody)
+  return $ mkLetRec' defs value
 
 goAxiomInductive ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.AxiomDef ->
   Sem r ()
 goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
@@ -391,8 +490,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinBoolPrint -> return ()
       Internal.BuiltinIOSequence -> return ()
       Internal.BuiltinIOReadline -> return ()
-      Internal.BuiltinString -> registerInductiveAxiom
-      Internal.BuiltinIO -> registerInductiveAxiom
+      Internal.BuiltinString -> registerInductiveAxiom (Just BuiltinString) []
+      Internal.BuiltinIO -> registerInductiveAxiom Nothing builtinIOConstrs
       Internal.BuiltinTrace -> return ()
       Internal.BuiltinFail -> return ()
       Internal.BuiltinStringConcat -> return ()
@@ -400,30 +499,34 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinStringToNat -> return ()
       Internal.BuiltinNatToString -> return ()
 
-    registerInductiveAxiom :: Sem r ()
-    registerInductiveAxiom = do
+    registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
+    registerInductiveAxiom ax ctrs = do
       sym <- freshSymbol
-      let info =
+      let ty = mkTypeConstr' sym []
+          ctrs' = builtinConstrs sym ty ctrs
+          info =
             InductiveInfo
               { _inductiveName = a ^. Internal.axiomName . nameText,
                 _inductiveLocation = Just $ a ^. Internal.axiomName . nameLoc,
                 _inductiveSymbol = sym,
-                _inductiveKind = mkDynamic',
-                _inductiveConstructors = [],
+                _inductiveKind = mkSmallUniv,
+                _inductiveConstructors = ctrs',
                 _inductiveParams = [],
                 _inductivePositive = False,
-                _inductiveBuiltin = Nothing
+                _inductiveBuiltin = fmap BuiltinTypeAxiom ax
               }
       registerInductive (mkIdentIndex (a ^. Internal.axiomName)) info
+      mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) ctrs'
 
 goAxiomDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.AxiomDef ->
   Sem r ()
 goAxiomDef a = do
   boolSym <- getBoolSymbol
-  case a ^. Internal.axiomBuiltin >>= builtinBody boolSym of
+  natSym <- getNatSymbol
+  case a ^. Internal.axiomBuiltin >>= builtinBody boolSym natSym of
     Just body -> do
       sym <- freshSymbol
       ty <- axiomType'
@@ -440,17 +543,20 @@ goAxiomDef a = do
               }
       registerIdent (mkIdentIndex (a ^. Internal.axiomName)) info
       registerIdentNode sym body
+      let (is, _) = unfoldLambdas body
+      setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
     Nothing -> return ()
   where
-    builtinBody :: Symbol -> Internal.BuiltinAxiom -> Maybe Node
-    builtinBody boolSym = \case
-      Internal.BuiltinNatPrint -> Just writeLambda
-      Internal.BuiltinStringPrint -> Just writeLambda
-      Internal.BuiltinBoolPrint -> Just writeLambda
+    builtinBody :: Symbol -> Symbol -> Internal.BuiltinAxiom -> Maybe Node
+    builtinBody boolSym natSym = \case
+      Internal.BuiltinNatPrint -> Just $ writeLambda (mkTypeConstr' natSym [])
+      Internal.BuiltinStringPrint -> Just $ writeLambda mkTypeString'
+      Internal.BuiltinBoolPrint -> Just $ writeLambda mkTypeBool'
       Internal.BuiltinIOSequence -> Nothing
       Internal.BuiltinIOReadline ->
         Just
           ( mkLambda'
+              mkTypeString'
               ( mkConstr'
                   (BuiltinTag TagBind)
                   [ mkConstr' (BuiltinTag TagReadLn) [],
@@ -459,13 +565,15 @@ goAxiomDef a = do
               )
           )
       Internal.BuiltinStringConcat ->
-        Just (mkLambda' (mkLambda' (mkBuiltinApp' OpStrConcat [mkVar' 1, mkVar' 0])))
+        Just (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpStrConcat [mkVar' 1, mkVar' 0])))
       Internal.BuiltinStringEq ->
-        Just (mkLambda' (mkLambda' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
+        Just (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
       Internal.BuiltinStringToNat -> do
         Just
           ( mkLambda'
+              mkTypeString'
               ( mkLet'
+                  mkTypeInteger'
                   (mkBuiltinApp' OpStrToInt [mkVar' 0])
                   ( mkIf'
                       boolSym
@@ -476,57 +584,82 @@ goAxiomDef a = do
               )
           )
       Internal.BuiltinNatToString ->
-        Just (mkLambda' (mkBuiltinApp' OpShow [mkVar' 0]))
+        Just (mkLambda' (mkTypeConstr' natSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
       Internal.BuiltinString -> Nothing
       Internal.BuiltinIO -> Nothing
       Internal.BuiltinTrace -> Nothing
       Internal.BuiltinFail ->
-        Just (mkLambda' (mkLambda' (mkBuiltinApp' OpFail [mkVar' 0])))
+        Just (mkLambda' mkSmallUniv (mkLambda' (mkVar' 0) (mkBuiltinApp' OpFail [mkVar' 0])))
 
     axiomType' :: Sem r Type
-    axiomType' = runReader initIndexTable (goExpression (a ^. Internal.axiomType))
+    axiomType' = runReader initIndexTable (goType (a ^. Internal.axiomType))
 
-    writeLambda :: Node
-    writeLambda = mkLambda' (mkConstr' (BuiltinTag TagWrite) [mkVar' 0])
+    writeLambda :: Type -> Node
+    writeLambda ty = mkLambda' ty (mkConstr' (BuiltinTag TagWrite) [mkVar' 0])
 
 fromPatternArg ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   Internal.PatternArg ->
   Sem r Pattern
 fromPatternArg pa = case pa ^. Internal.patternArgName of
-  Just pan -> wrapAsPattern pan <$> subPat
+  Just pan -> do
+    ty <- getPatternType pan
+    wrapAsPattern pan ty <$> subPat
   Nothing -> subPat
   where
     subPat :: Sem r Pattern
     subPat = fromPattern (pa ^. Internal.patternArgPattern)
 
-    wrapAsPattern :: Name -> Pattern -> Pattern
-    wrapAsPattern pan pat =
+    wrapAsPattern :: Name -> Type -> Pattern -> Pattern
+    wrapAsPattern pan ty pat =
       ( PatBinder
           ( PatternBinder
               { _patternBinder =
                   Binder
                     { _binderName = pan ^. nameText,
                       _binderLocation = Just (pan ^. nameLoc),
-                      _binderType = mkDynamic'
+                      _binderType = ty
                     },
                 _patternBinderPattern = pat
               }
           )
       )
 
+    getPatternType :: Name -> Sem r Type
+    getPatternType n = asks (fromJust . HashMap.lookup n) >>= goType
+
+    -- The types of the pattern must be shifted by the index of the argument
+    -- within the params
+    indexedPatternArgs :: [Internal.PatternArg] -> Sem r [Pattern]
+    indexedPatternArgs ps = mapM go (indexFrom 0 ps)
+      where
+        go :: Indexed (Internal.PatternArg) -> Sem r Pattern
+        go (Indexed i p) = local (over indexTableVarsNum (+ i)) (fromPatternArg p)
+
     fromPattern :: Internal.Pattern -> Sem r Pattern
     fromPattern = \case
-      Internal.PatternVariable n -> return $ PatBinder (PatternBinder (Binder (n ^. nameText) (Just (n ^. nameLoc)) mkDynamic') wildcard)
+      Internal.PatternVariable n -> do
+        ty <- getPatternType n
+        return $ PatBinder (PatternBinder (Binder (n ^. nameText) (Just (n ^. nameLoc)) ty) (wildcard ty))
       Internal.PatternConstructorApp c -> do
         (indParams, _) <- InternalTyped.lookupConstructorArgTypes n
-        patternArgs <- mapM fromPatternArg params
-        let indArgs = replicate (length indParams) wildcard
+        patternArgs <- indexedPatternArgs params
+        let indArgs = replicate (length indParams) (wildcard mkSmallUniv)
             args = indArgs ++ patternArgs
         m <- getIdent identIndex
+        ctorTy <- goType (fromJust (c ^. Internal.constrAppType))
         case m of
-          Just (IdentConstr tag) -> return $ PatConstr (PatternConstr (setInfoLocation (n ^. nameLoc) (setInfoName (n ^. nameText) Info.empty)) tag args)
+          Just (IdentConstr tag) ->
+            return $
+              PatConstr
+                ( PatternConstr
+                    { _patternConstrInfo = setInfoLocation (n ^. nameLoc) (setInfoName (n ^. nameText) Info.empty),
+                      _patternConstrTag = tag,
+                      _patternConstrArgs = args,
+                      _patternConstrType = ctorTy
+                    }
+                )
           Just _ -> error ("internal to core: not a constructor " <> txt)
           Nothing -> error ("internal to core: undeclared identifier: " <> txt)
         where
@@ -542,8 +675,8 @@ fromPatternArg pa = case pa ^. Internal.patternArgName of
           txt :: Text
           txt = c ^. Internal.constrAppConstructor . Internal.nameText
       where
-        wildcard :: Pattern
-        wildcard = PatWildcard (PatternWildcard Info.empty)
+        wildcard :: Type -> Pattern
+        wildcard ty = PatWildcard (PatternWildcard Info.empty ty)
 
 getPatternArgVars :: Internal.PatternArg -> [Name]
 getPatternArgVars pa = case pa ^. Internal.patternArgName of
@@ -561,59 +694,65 @@ getPatternArgVars pa = case pa ^. Internal.patternArgName of
 
 goPatternArgs ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  Level -> -- the level of the first binder for the matched value
   Internal.Expression ->
   [Internal.PatternArg] ->
+  [Type] -> -- types of the patterns
   Sem r MatchBranch
-goPatternArgs body ps = do
-  vars <- asks (^. indexTableVars)
-  varsNum <- asks (^. indexTableVarsNum)
-  pats <- patterns
-  let bs :: [Name]
-      bs = concatMap getPatternArgVars ps
-      (vars', varsNum') =
-        foldl'
-          ( \(vs, k) name ->
-              (HashMap.insert (name ^. nameId) k vs, k + 1)
-          )
-          (vars, varsNum)
-          bs
-      body' :: Sem r Node
-      body' =
+goPatternArgs lvl0 body ps0 ptys0 = go lvl0 [] ps0 ptys0
+  where
+    -- `lvl` is the level of the lambda-bound variable corresponding to the current pattern
+    go :: Level -> [Pattern] -> [Internal.PatternArg] -> [Type] -> Sem r MatchBranch
+    go lvl pats ps ptys = case (ps, ptys) of
+      -- The pattern has an inductive type, so can be matched on
+      (p : ps', NTyp {} : ptys') -> do
+        pat <- fromPatternArg p
+        vars <- asks (^. indexTableVars)
+        varsNum <- asks (^. indexTableVarsNum)
+        let bs :: [Name]
+            bs = getPatternArgVars p
+            (vars', varsNum') =
+              foldl'
+                ( \(vs, k) name ->
+                    (HashMap.insert (name ^. nameId) k vs, k + 1)
+                )
+                (vars, varsNum)
+                bs
         local
           (set indexTableVars vars' . set indexTableVarsNum varsNum')
-          (goExpression body)
-  MatchBranch Info.empty (fromList pats) <$> body'
-  where
-    patterns :: Sem r [Pattern]
-    patterns = mapM fromPatternArg ps
-
-goFunctionClause ::
-  forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
-  Internal.FunctionClause ->
-  Sem r MatchBranch
-goFunctionClause clause = goPatternArgs (clause ^. Internal.clauseBody) internalPatternArgs
-  where
-    internalPatternArgs :: [Internal.PatternArg]
-    internalPatternArgs = clause ^. Internal.clausePatterns
+          (go (lvl + 1) (pat : pats) ps' ptys')
+      (p : ps', _ : ptys') ->
+        -- The pattern does not have an inductive type, so is excluded from the match
+        case p ^. Internal.patternArgPattern of
+          Internal.PatternVariable {} -> do
+            vars <- asks (^. indexTableVars)
+            let vars' = addPatternVariableNames p lvl vars
+            local
+              (set indexTableVars vars')
+              (go (lvl + 1) pats ps' ptys')
+          _ ->
+            impossible
+      ([], []) -> do
+        body' <- goExpression body
+        return $ MatchBranch Info.empty (fromList (reverse pats)) body'
+      _ ->
+        impossible
+
+addPatternVariableNames ::
+  Internal.PatternArg ->
+  Level ->
+  HashMap NameId Level ->
+  HashMap NameId Level
+addPatternVariableNames p lvl vars =
+  foldl' (\vs name -> HashMap.insert (name ^. nameId) lvl vs) vars (getPatternArgVars p)
 
 goExpression ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
-  Internal.Expression ->
-  Sem r Node
-goExpression e = do
-  node <- goExpression' e
-  tab <- getInfoTable
-  return $ etaExpandApps tab node
-
-goExpression' ::
-  forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   Internal.Expression ->
   Sem r Node
-goExpression' = \case
+goExpression = \case
   Internal.ExpressionLet l -> goLet l
   Internal.ExpressionLiteral l -> do
     tab <- getInfoTable
@@ -626,9 +765,9 @@ goExpression' = \case
     Internal.IdenFunction n -> do
       funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
       case funInfoBuiltin of
-        Just Internal.BuiltinBoolIf -> error "if must be called with 3 arguments"
-        Just Internal.BuiltinBoolOr -> error "|| must be called with 2 arguments"
-        Just Internal.BuiltinBoolAnd -> error "&& must be called with 2 arguments"
+        Just Internal.BuiltinBoolIf -> error "internal to core: if must be called with 3 arguments"
+        Just Internal.BuiltinBoolOr -> error "internal to core: || must be called with 2 arguments"
+        Just Internal.BuiltinBoolAnd -> error "internal to core: && must be called with 2 arguments"
         _ -> return ()
       -- if the function was defined by a let, then in Core it is stored in a variable
       vars <- asks (^. indexTableVars)
@@ -657,8 +796,8 @@ goExpression' = \case
     Internal.IdenAxiom n -> do
       axiomInfoBuiltin <- Internal.getAxiomBuiltinInfo n
       case axiomInfoBuiltin of
-        Just Internal.BuiltinIOSequence -> error ">> must be called with 2 arguments"
-        Just Internal.BuiltinTrace -> error "trace must be called with 2 arguments"
+        Just Internal.BuiltinIOSequence -> error "internal to core: >> must be called with 2 arguments"
+        Just Internal.BuiltinTrace -> error "internal to core: trace must be called with 2 arguments"
         _ -> return ()
       m <- getIdent identIndex
       return $ case m of
@@ -679,34 +818,45 @@ goExpression' = \case
   Internal.ExpressionSimpleLambda l -> goSimpleLambda l
   Internal.ExpressionLambda l -> goLambda l
   Internal.ExpressionCase l -> goCase l
-  e@(Internal.ExpressionFunction {}) -> goFunction (Internal.unfoldFunType e)
-  Internal.ExpressionHole h -> error ("goExpression hole: " <> show (Loc.getLoc h))
-  Internal.ExpressionUniverse {} -> return (mkUniv' (fromIntegral smallLevel))
+  e@Internal.ExpressionFunction {} -> goFunction (Internal.unfoldFunType e)
+  Internal.ExpressionHole h -> error ("internal to core: goExpression hole: " <> show (Loc.getLoc h))
+  Internal.ExpressionUniverse {} -> return mkSmallUniv
 
 goFunction ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   ([Internal.FunctionParameter], Internal.Expression) ->
   Sem r Node
-goFunction (params, returnTypeExpr) = foldr f (goExpression returnTypeExpr) params
+goFunction (params, returnTypeExpr) = go params
   where
-    f :: Internal.FunctionParameter -> Sem r Node -> Sem r Node
-    f param acc = do
-      paramBinder <- Binder (maybe "?" (^. nameText) $ param ^. Internal.paramName) (fmap (^. nameLoc) $ param ^. Internal.paramName) <$> goExpression (param ^. Internal.paramType)
-      case param ^. Internal.paramName of
-        Nothing -> mkPi mempty paramBinder <$> acc
-        Just vn -> mkPi mempty paramBinder <$> localAddName vn acc
+    go :: [Internal.FunctionParameter] -> Sem r Node
+    go = \case
+      param : params' -> do
+        paramTy <- goType (param ^. Internal.paramType)
+        let paramBinder =
+              Binder
+                { _binderName = maybe "?" (^. nameText) $ param ^. Internal.paramName,
+                  _binderLocation = fmap (^. nameLoc) $ param ^. Internal.paramName,
+                  _binderType = paramTy
+                }
+        case param ^. Internal.paramName of
+          Nothing -> mkPi mempty paramBinder <$> local (over indexTableVarsNum (+ 1)) (go params')
+          Just vn -> mkPi mempty paramBinder <$> localAddName vn (go params')
+      [] ->
+        goType returnTypeExpr
 
 goSimpleLambda ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   Internal.SimpleLambda ->
   Sem r Node
-goSimpleLambda l = localAddName (l ^. Internal.slambdaVar) (mkLambda' <$> goExpression (l ^. Internal.slambdaBody))
+goSimpleLambda l = do
+  ty <- goType (l ^. Internal.slambdaVarType)
+  localAddName (l ^. Internal.slambdaVar) (mkLambda' ty <$> goExpression (l ^. Internal.slambdaBody))
 
 goApplication ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
   Internal.Application ->
   Sem r Node
 goApplication a = do
@@ -729,11 +879,18 @@ goApplication a = do
         Just Internal.BuiltinString -> app
         Just Internal.BuiltinIO -> app
         Just Internal.BuiltinIOSequence -> do
+          ioSym <- getIOSymbol
           as <- exprArgs
           case as of
             (arg1 : arg2 : xs) ->
-              return (mkApps' (mkConstr' (BuiltinTag TagBind) [arg1, mkLambda' (shift 1 arg2)]) xs)
-            _ -> error ">> must be called with 2 arguments"
+              return $
+                mkApps'
+                  ( mkConstr'
+                      (BuiltinTag TagBind)
+                      [arg1, mkLambda' (mkTypeConstr' ioSym []) (shift 1 arg2)]
+                  )
+                  xs
+            _ -> error "internal to core: >> must be called with 2 arguments"
         Just Internal.BuiltinIOReadline -> app
         Just Internal.BuiltinStringConcat -> app
         Just Internal.BuiltinStringEq -> app
@@ -744,7 +901,7 @@ goApplication a = do
           case as of
             (_ : _ : arg1 : arg2 : xs) ->
               return (mkApps' (mkBuiltinApp' OpTrace [arg1, arg2]) xs)
-            _ -> error "trace must be called with 2 arguments"
+            _ -> error "internal to core: trace must be called with 2 arguments"
         Just Internal.BuiltinFail -> app
         Nothing -> app
     Internal.ExpressionIden (Internal.IdenFunction n) -> do
@@ -755,19 +912,19 @@ goApplication a = do
           as <- exprArgs
           case as of
             (_ : v : b1 : b2 : xs) -> return (mkApps' (mkIf' sym v b1 b2) xs)
-            _ -> error "if must be called with 3 arguments"
+            _ -> error "internal to core: if must be called with 3 arguments"
         Just Internal.BuiltinBoolOr -> do
           sym <- getBoolSymbol
           as <- exprArgs
           case as of
             (x : y : xs) -> return (mkApps' (mkIf' sym x (mkConstr' (BuiltinTag TagTrue) []) y) xs)
-            _ -> error "|| must be called with 2 arguments"
+            _ -> error "internal to core: || must be called with 2 arguments"
         Just Internal.BuiltinBoolAnd -> do
           sym <- getBoolSymbol
           as <- exprArgs
           case as of
             (x : y : xs) -> return (mkApps' (mkIf' sym x y (mkConstr' (BuiltinTag TagFalse) [])) xs)
-            _ -> error "&& must be called with 2 arguments"
+            _ -> error "internal to core: && must be called with 2 arguments"
         _ -> app
     _ -> app
 
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs b/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs
index 715010d766..f4c960eabc 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs
@@ -26,3 +26,6 @@ localAddName n s = do
         ( over indexTableVars (HashMap.insert (n ^. nameId) idx)
             . over indexTableVarsNum (+ 1)
         )
+
+underBinders :: Members '[Reader IndexTable] r => Int -> Sem r a -> Sem r a
+underBinders nBinders = local (over indexTableVarsNum (+ nBinders))
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 9a1ac9e9ad..8166708560 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -156,16 +156,7 @@ parseDefinition sym ty = do
         && not (isDynamic (typeTarget ty))
     )
     $ parseFailure off "type mismatch: too many lambdas"
-  lift $ setIdentArgsInfo sym (map (toArgumentInfo . (^. lambdaLhsBinder)) is)
-  where
-    toArgumentInfo :: Binder -> ArgumentInfo
-    toArgumentInfo bi =
-      ArgumentInfo
-        { _argumentName = bi ^. binderName,
-          _argumentLocation = bi ^. binderLocation,
-          _argumentType = bi ^. binderType,
-          _argumentIsImplicit = Explicit
-        }
+  lift $ setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
 
 statementInductive ::
   (Member InfoTableBuilder r) =>
@@ -250,6 +241,15 @@ bracedExpr ::
   ParsecS r Node
 bracedExpr varsNum vars = braces (expr varsNum vars) <|> expr varsNum vars
 
+typeAnnot ::
+  (Member InfoTableBuilder r) =>
+  Index ->
+  HashMap Text Level ->
+  ParsecS r Node
+typeAnnot varsNum vars = do
+  kw kwColon
+  expr varsNum vars
+
 typeExpr ::
   (Member InfoTableBuilder r) =>
   Index ->
@@ -587,8 +587,7 @@ exprPi ::
 exprPi varsNum vars = do
   kw kwPi
   (name, loc) <- parseLocalName
-  kw kwColon
-  ty <- expr varsNum vars
+  ty <- typeAnnot varsNum vars
   kw kwComma
   let vars' = HashMap.insert name varsNum vars
       bi = Binder name (Just loc) ty
@@ -612,8 +611,7 @@ exprLambda varsNum vars = do
       parens
         ( do
             n <- parseLocalName
-            kw kwColon
-            ty <- expr varsNum vars
+            ty <- typeAnnot varsNum vars
             return (n, Just ty)
         )
         <|> (\n -> (n, Nothing)) <$> parseLocalName
@@ -667,12 +665,14 @@ letrecDefs names varsNum vars = forM names letrecItem
     letrecItem n = do
       off <- P.getOffset
       (txt, i) <- identifierL
+      mty <- optional (typeAnnot varsNum vars)
       when (n /= txt) $
         parseFailure off "identifier name doesn't match letrec signature"
       kw kwAssign
       v <- bracedExpr varsNum vars
       kw kwSemicolon
-      return $ LetItem (Binder txt (Just i) mkDynamic') v
+      let ty = fromMaybe mkDynamic' mty
+      return $ LetItem (Binder txt (Just i) ty) v
 
 letrecDef ::
   (Member InfoTableBuilder r) =>
@@ -693,7 +693,7 @@ exprLet ::
 exprLet varsNum vars = do
   kw kwLet
   (name, loc) <- parseLocalName
-  mty <- optional (kw kwColon >> expr varsNum vars)
+  mty <- optional (typeAnnot varsNum vars)
   kw kwAssign
   value <- bracedExpr varsNum vars
   kw kwIn
@@ -824,20 +824,42 @@ exprMatch ::
   ParsecS r Node
 exprMatch varsNum vars = do
   kw kwMatch
-  values <- P.sepBy (bracedExpr varsNum vars) (kw kwComma)
+  vals <- P.sepBy (exprMatchValue varsNum vars) (kw kwComma)
   kw kwWith
-  braces (exprMatch' values varsNum vars)
-    <|> exprMatch' values varsNum vars
+  mty <- optional (typeAnnot varsNum vars)
+  let rty = fromMaybe mkDynamic' mty
+  braces (exprMatch' vals rty varsNum vars)
+    <|> exprMatch' vals rty varsNum vars
+
+exprMatchValue ::
+  (Member InfoTableBuilder r) =>
+  Index ->
+  HashMap Text Level ->
+  ParsecS r (Node, Type)
+exprMatchValue varsNum vars = parens (exprMatchValue' varsNum vars) <|> exprMatchValue' varsNum vars
+
+exprMatchValue' ::
+  (Member InfoTableBuilder r) =>
+  Index ->
+  HashMap Text Level ->
+  ParsecS r (Node, Type)
+exprMatchValue' varsNum vars = do
+  val <- expr varsNum vars
+  mty <- optional (typeAnnot varsNum vars)
+  return (val, fromMaybe mkDynamic' mty)
 
 exprMatch' ::
   (Member InfoTableBuilder r) =>
-  [Node] ->
+  [(Node, Type)] ->
+  Type ->
   Index ->
   HashMap Text Level ->
   ParsecS r Node
-exprMatch' values varsNum vars = do
+exprMatch' vals rty varsNum vars = do
+  let values = map fst vals
+      types = map snd vals
   bs <- P.sepEndBy (matchBranch (length values) varsNum vars) (kw kwSemicolon)
-  return $ mkMatch' (fromList values) bs
+  return $ mkMatch' (fromList types) rty (fromList values) bs
 
 matchBranch ::
   (Member InfoTableBuilder r) =>
@@ -847,7 +869,7 @@ matchBranch ::
   ParsecS r MatchBranch
 matchBranch patsNum varsNum vars = do
   off <- P.getOffset
-  pats <- P.sepBy branchPattern (kw kwComma)
+  pats <- branchPatterns varsNum vars
   kw kwAssign
   unless (length pats == patsNum) $
     parseFailure off "wrong number of patterns"
@@ -863,50 +885,87 @@ matchBranch patsNum varsNum vars = do
   br <- bracedExpr varsNum' vars'
   return $ MatchBranch Info.empty (fromList pats) br
 
+branchPatterns ::
+  (Member InfoTableBuilder r) =>
+  Index ->
+  HashMap Text Level ->
+  ParsecS r [Pattern]
+branchPatterns varsNum vars = do
+  (pat, (varsNum', vars')) <- branchPattern varsNum vars
+  pats <- (kw kwComma >> branchPatterns varsNum' vars') <|> return []
+  return (pat : pats)
+
 branchPattern ::
   (Member InfoTableBuilder r) =>
-  ParsecS r Pattern
-branchPattern =
-  wildcardPattern
-    <|> binderOrConstrPattern True
-    <|> parens branchPattern
+  Index ->
+  HashMap Text Level ->
+  ParsecS r (Pattern, (Index, HashMap Text Level))
+branchPattern varsNum vars =
+  parens (branchPattern varsNum vars)
+    <|> wildcardPattern varsNum vars
+    <|> binderOrConstrPattern True varsNum vars
 
-wildcardPattern :: ParsecS r Pattern
-wildcardPattern = do
+wildcardPattern ::
+  Index ->
+  HashMap Text Level ->
+  ParsecS r (Pattern, (Index, HashMap Text Level))
+wildcardPattern varsNum vars = do
   kw kwWildcard
-  return $ PatWildcard (PatternWildcard Info.empty)
+  return (PatWildcard (PatternWildcard Info.empty mkDynamic'), (varsNum, vars))
 
 binderOrConstrPattern ::
   (Member InfoTableBuilder r) =>
   Bool ->
-  ParsecS r Pattern
-binderOrConstrPattern parseArgs = do
+  Index ->
+  HashMap Text Level ->
+  ParsecS r (Pattern, (Index, HashMap Text Level))
+binderOrConstrPattern parseArgs varsNum vars = do
   off <- P.getOffset
   (txt, i) <- identifierL
   r <- lift (getIdent txt)
   case r of
     Just (IdentConstr tag) -> do
-      ps <- if parseArgs then P.many branchPattern else return []
+      (ps, (varsNum', vars')) <- if parseArgs then constrArgPatterns varsNum vars else return ([], (varsNum, vars))
       ci <- lift $ getConstructorInfo tag
       when
         (ci ^. constructorArgsNum /= length ps)
         (parseFailure off "wrong number of constructor arguments")
       let info = setInfoName (ci ^. constructorName) Info.empty
-      return $ PatConstr (PatternConstr info tag ps)
+      mty <- optional (typeAnnot varsNum vars)
+      return (PatConstr (PatternConstr info tag ps (fromMaybe mkDynamic' mty)), (varsNum', vars'))
     _ -> do
-      mp <- optional binderPattern
-      let pat = fromMaybe (PatWildcard (PatternWildcard Info.empty)) mp
-          binder = Binder txt (Just i) mkDynamic'
-      return $ PatBinder (PatternBinder binder pat)
+      let vars1 = HashMap.insert txt varsNum vars
+      mp <- optional (binderPattern (varsNum + 1) vars1)
+      mty <- optional (typeAnnot varsNum vars)
+      let ty = fromMaybe mkDynamic' mty
+          (pat, (varsNum', vars')) = fromMaybe (PatWildcard (PatternWildcard Info.empty ty), (varsNum + 1, vars1)) mp
+          binder = Binder txt (Just i) ty
+      return (PatBinder (PatternBinder binder pat), (varsNum', vars'))
+
+constrArgPatterns ::
+  (Member InfoTableBuilder r) =>
+  Index ->
+  HashMap Text Level ->
+  ParsecS r ([Pattern], (Index, HashMap Text Level))
+constrArgPatterns varsNum vars = do
+  mr <- optional (branchPattern varsNum vars)
+  case mr of
+    Just (pat, (varsNum', vars')) -> do
+      (pats, (varsNum'', vars'')) <- constrArgPatterns varsNum' vars'
+      return (pat : pats, (varsNum'', vars''))
+    Nothing ->
+      return ([], (varsNum, vars))
 
 binderPattern ::
   (Member InfoTableBuilder r) =>
-  ParsecS r Pattern
-binderPattern = do
+  Index ->
+  HashMap Text Level ->
+  ParsecS r (Pattern, (Index, HashMap Text Level))
+binderPattern varsNum vars = do
   symbolAt
-  wildcardPattern
-    <|> binderOrConstrPattern False
-    <|> parens branchPattern
+  parens (branchPattern varsNum vars)
+    <|> wildcardPattern varsNum vars
+    <|> binderOrConstrPattern False varsNum vars
 
 exprNamed ::
   (Member InfoTableBuilder r) =>
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 71e0922fbb..e93542c9ab 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -14,10 +14,20 @@ fromCore :: InfoTable -> Stripped.InfoTable
 fromCore tab =
   Stripped.InfoTable
     { _infoMain = tab ^. infoMain,
-      _infoFunctions = fmap (translateFunctionInfo tab) (tab ^. infoIdentifiers),
-      _infoInductives = fmap translateInductiveInfo (tab ^. infoInductives),
-      _infoConstructors = fmap translateConstructorInfo (tab ^. infoConstructors)
+      _infoFunctions = fmap (translateFunctionInfo tab) (tab' ^. infoIdentifiers),
+      _infoInductives = fmap translateInductiveInfo (tab' ^. infoInductives),
+      _infoConstructors = fmap translateConstructorInfo (tab' ^. infoConstructors)
     }
+  where
+    tab' =
+      tab
+        { _infoIdentifiers = HashMap.filter (\ii -> isNothing (ii ^. identifierBuiltin)) (tab ^. infoIdentifiers),
+          _infoInductives = HashMap.filter (\ii -> isNothing (ii ^. inductiveBuiltin) || isIO (ii ^. inductiveBuiltin)) (tab ^. infoInductives),
+          _infoConstructors = HashMap.filter (\ci -> isNothing (ci ^. constructorBuiltin)) (tab ^. infoConstructors)
+        }
+    isIO :: Maybe BuiltinType -> Bool
+    isIO (Just (BuiltinTypeAxiom BuiltinIO)) = True
+    isIO _ = False
 
 translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo
 translateFunctionInfo tab IdentifierInfo {..} =
@@ -117,12 +127,26 @@ translateNode node = case node of
       )
       (translateNode (_letItem ^. letItemValue))
       (translateNode _letBody)
-  NCase Case {..} ->
-    Stripped.mkCase
-      _caseInductive
-      (translateNode _caseValue)
-      (map translateCaseBranch _caseBranches)
-      (fmap translateNode _caseDefault)
+  NCase Case {..} -> case _caseBranches of
+    [br@CaseBranch {..}]
+      | _caseBranchTag == BuiltinTag TagTrue ->
+          translateIf _caseValue (br ^. caseBranchBody) (fromMaybe branchFailure _caseDefault)
+    [br@CaseBranch {..}]
+      | _caseBranchTag == BuiltinTag TagFalse ->
+          translateIf _caseValue (fromMaybe branchFailure _caseDefault) (br ^. caseBranchBody)
+    [br1, br2]
+      | br1 ^. caseBranchTag == BuiltinTag TagTrue
+          && br2 ^. caseBranchTag == BuiltinTag TagFalse ->
+          translateIf _caseValue (br1 ^. caseBranchBody) (br2 ^. caseBranchBody)
+      | br1 ^. caseBranchTag == BuiltinTag TagFalse
+          && br2 ^. caseBranchTag == BuiltinTag TagTrue ->
+          translateIf _caseValue (br2 ^. caseBranchBody) (br1 ^. caseBranchBody)
+    _ ->
+      Stripped.mkCase
+        _caseInductive
+        (translateNode _caseValue)
+        (map translateCaseBranch _caseBranches)
+        (fmap translateNode _caseDefault)
   _
     | isType node ->
         Stripped.mkConstr (Stripped.ConstrInfo "()" Nothing Stripped.TyDynamic) (BuiltinTag TagTrue) []
@@ -132,7 +156,16 @@ translateNode node = case node of
     unsupported :: a
     unsupported = error "Core to Core.Stripped: unsupported node"
 
+    translateIf :: Node -> Node -> Node -> Stripped.Node
+    translateIf val br1 br2 = Stripped.mkIf (translateNode val) (translateNode br1) (translateNode br2)
+
+    branchFailure :: Node
+    branchFailure = mkBuiltinApp' OpFail [mkConstant' (ConstString "illegal `if` branch")]
+
     translateCaseBranch :: CaseBranch -> Stripped.CaseBranch
+    translateCaseBranch CaseBranch {..}
+      | _caseBranchTag == BuiltinTag TagTrue || _caseBranchTag == BuiltinTag TagFalse =
+          error "Core to Core.Stripped: invalid case on booleans"
     translateCaseBranch CaseBranch {..} =
       Stripped.CaseBranch
         { _caseBranchInfo =
@@ -190,4 +223,11 @@ translateType node = case node of
     Stripped.TyPrim _typePrimPrimitive
   NDyn Dynamic {} ->
     Stripped.TyDynamic
-  _ -> error "Core to Core.Stripped: unsupported type"
+  _ ->
+    Stripped.TyDynamic
+
+-- TODO: We need to return TyDynamic here to handle type synonyms. This should
+-- be handled by RemoveTypeArgs, but currently it cannot be because
+-- lambda-letrec-lifting doesn't preserve the type information about the body.
+
+-- _ -> error $ "Core to Core.Stripped: unsupported type: " <> ppTrace node
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index df5615d5ce..a813cc8511 100644
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@@ -222,7 +222,10 @@ class HasExpressions a where
   leafExpressions :: Traversal' a Expression
 
 instance HasExpressions LambdaClause where
-  leafExpressions f (LambdaClause ps b) = LambdaClause ps <$> leafExpressions f b
+  leafExpressions f l = do
+    _lambdaPatterns <- traverse (leafExpressions f) (l ^. lambdaPatterns)
+    _lambdaBody <- leafExpressions f (l ^. lambdaBody)
+    pure LambdaClause {..}
 
 instance HasExpressions Lambda where
   leafExpressions f l = do
@@ -243,8 +246,22 @@ instance HasExpressions Expression where
     ExpressionUniverse {} -> f e
     ExpressionHole {} -> f e
 
+instance HasExpressions ConstructorApp where
+  leafExpressions f = traverseOf (constrAppType . _Just) (leafExpressions f)
+
+instance HasExpressions PatternArg where
+  leafExpressions f = traverseOf patternArgPattern (leafExpressions f)
+
+instance HasExpressions Pattern where
+  leafExpressions f p = case p of
+    PatternVariable {} -> pure p
+    PatternConstructorApp a -> PatternConstructorApp <$> leafExpressions f a
+
 instance HasExpressions CaseBranch where
-  leafExpressions f = traverseOf caseBranchExpression (leafExpressions f)
+  leafExpressions f b = do
+    _caseBranchPattern <- leafExpressions f (b ^. caseBranchPattern)
+    _caseBranchExpression <- leafExpressions f (b ^. caseBranchExpression)
+    pure CaseBranch {..}
 
 instance HasExpressions Case where
   leafExpressions f l = do
@@ -315,9 +332,10 @@ subsHoles s = over leafExpressions helper
       _ -> e
 
 instance HasExpressions FunctionClause where
-  leafExpressions f (FunctionClause n ps b) = do
-    b' <- leafExpressions f b
-    pure (FunctionClause n ps b')
+  leafExpressions f c = do
+    _clauseBody <- leafExpressions f (c ^. clauseBody)
+    _clausePatterns <- traverse (leafExpressions f) (c ^. clausePatterns)
+    pure FunctionClause {_clauseName = c ^. clauseName, ..}
 
 instance HasExpressions Example where
   leafExpressions f = traverseOf exampleExpression (leafExpressions f)
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index b38baf9310..01b80a8008 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@@ -6,7 +6,6 @@ module Juvix.Compiler.Internal.Language
     module Juvix.Compiler.Concrete.Data.Literal,
     module Juvix.Data.Universe,
     module Juvix.Data.Hole,
-    module Juvix.Data.Wildcard,
     module Juvix.Compiler.Concrete.Data.Builtins,
   )
 where
@@ -17,7 +16,6 @@ import Juvix.Compiler.Concrete.Data.Literal
 import Juvix.Data.Hole
 import Juvix.Data.IsImplicit
 import Juvix.Data.Universe hiding (smallUniverse)
-import Juvix.Data.Wildcard
 import Juvix.Data.WithLoc
 import Juvix.Prelude
 
@@ -204,7 +202,9 @@ instance Hashable Application where
 -- | Fully applied constructor in a pattern.
 data ConstructorApp = ConstructorApp
   { _constrAppConstructor :: Name,
-    _constrAppParameters :: [PatternArg]
+    _constrAppParameters :: [PatternArg],
+    -- | The type checker fills this field
+    _constrAppType :: Maybe Expression
   }
   deriving stock (Eq, Generic, Data)
 
@@ -322,8 +322,8 @@ instance HasAtomicity Function where
   atomicity = const (Aggregate funFixity)
 
 instance HasAtomicity ConstructorApp where
-  atomicity (ConstructorApp _ args)
-    | null args = Atom
+  atomicity ConstructorApp {..}
+    | null _constrAppParameters = Atom
     | otherwise = Aggregate appFixity
 
 instance HasAtomicity PatternArg where
@@ -411,7 +411,7 @@ instance HasLoc PatternArg where
   getLoc a = fmap getLoc (a ^. patternArgName) ?<> getLoc (a ^. patternArgPattern)
 
 instance HasLoc ConstructorApp where
-  getLoc (ConstructorApp c ps) =
-    case last <$> nonEmpty ps of
-      Just p -> getLoc c <> getLoc p
-      Nothing -> getLoc c
+  getLoc ConstructorApp {..} =
+    case last <$> nonEmpty _constrAppParameters of
+      Just p -> getLoc _constrAppConstructor <> getLoc p
+      Nothing -> getLoc _constrAppConstructor
diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
index ac084d7606..97c5d1dcd8 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
@@ -259,7 +259,8 @@ goConstructorApp c = do
   return
     ConstructorApp
       { _constrAppConstructor = c ^. Abstract.constrAppConstructor . Abstract.constructorRefName,
-        _constrAppParameters = _constrAppParameters'
+        _constrAppParameters = _constrAppParameters',
+        _constrAppType = Nothing
       }
 
 isSmallType :: Abstract.Expression -> Bool
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
index 859251ef27..3985414f2b 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
@@ -322,16 +322,17 @@ checkPattern ari = traverseOf (patternArgName . each) nameAri >=> traverseOf pat
                   }
             )
 
--- | TODO: insert holes for constructor implicit arguments
 checkConstructorApp ::
   forall r.
   (Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r) =>
   ConstructorApp ->
   Sem r ConstructorApp
-checkConstructorApp ca@(ConstructorApp c ps) = do
+checkConstructorApp ca = do
+  let c = ca ^. constrAppConstructor
   args <- (^. constructorInfoArgs) <$> lookupConstructor c
   let arities = map typeArity args
       n = length arities
+      ps = ca ^. constrAppParameters
       lps = length ps
   when
     (n /= lps)
@@ -344,7 +345,7 @@ checkConstructorApp ca@(ConstructorApp c ps) = do
         )
     )
   ps' <- zipWithM checkPattern arities ps
-  return (ConstructorApp c ps')
+  return (ConstructorApp c ps' Nothing)
 
 checkCase ::
   forall r.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
index ec57c6913a..3d3a15be98 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -269,10 +269,11 @@ checkFunctionClause ::
   FunctionClause ->
   Sem r FunctionClause
 checkFunctionClause clauseType FunctionClause {..} = do
-  body' <- checkClause clauseType _clausePatterns _clauseBody
+  (patterns', body') <- checkClause clauseType _clausePatterns _clauseBody
   return
     FunctionClause
       { _clauseBody = body',
+        _clausePatterns = patterns',
         ..
       }
 
@@ -286,19 +287,21 @@ checkClause ::
   [PatternArg] ->
   -- | Body
   Expression ->
-  Sem r Expression -- Checked body
+  Sem r ([PatternArg], Expression) -- (Checked patterns, Checked body)
 checkClause clauseType clausePats body = do
   locals0 <- ask
-  (localsPats, bodyTy) <- helper clausePats clauseType
+  (localsPats, (checkedPatterns, bodyType)) <- helper clausePats clauseType
   let locals' = locals0 <> localsPats
-      bodyTy' = substitutionE (localsToSubsE locals') bodyTy
-  local (const locals') (checkExpression bodyTy' body)
+      bodyTy' = substitutionE (localsToSubsE locals') bodyType
+  checkedBody <- local (const locals') (checkExpression bodyTy' body)
+  return (checkedPatterns, checkedBody)
   where
-    helper :: [PatternArg] -> Expression -> Sem r (LocalVars, Expression)
+    helper :: [PatternArg] -> Expression -> Sem r (LocalVars, ([PatternArg], Expression))
     helper pats ty = runState emptyLocalVars (go pats ty)
-    go :: [PatternArg] -> Expression -> Sem (State LocalVars ': r) Expression
+
+    go :: [PatternArg] -> Expression -> Sem (State LocalVars ': r) ([PatternArg], Expression)
     go pats bodyTy = case pats of
-      [] -> return bodyTy
+      [] -> return ([], bodyTy)
       (p : ps) -> do
         bodyTy' <- weakNormalize bodyTy
         case bodyTy' of
@@ -308,8 +311,8 @@ checkClause clauseType clausePats body = do
           _ -> case unfoldFunType bodyTy' of
             ([], _) -> error "too many patterns"
             (par : pars, ret) -> do
-              checkPattern par p
-              go ps (foldFunType pars ret)
+              par' <- checkPattern par p
+              first (par' :) <$> go ps (foldFunType pars ret)
 
 -- | Refines a hole into a function type. I.e. '_@1' is matched with '_@fresh → _@fresh'
 holeRefineToFunction :: (Members '[Inference, NameIdGen] r) => Hole -> Sem r Function
@@ -347,10 +350,10 @@ checkPattern ::
   (Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen, State FunctionsTable] r) =>
   FunctionParameter ->
   PatternArg ->
-  Sem r ()
+  Sem r PatternArg
 checkPattern = go
   where
-    go :: FunctionParameter -> PatternArg -> Sem r ()
+    go :: FunctionParameter -> PatternArg -> Sem r PatternArg
     go argTy patArg = do
       matchIsImplicit (argTy ^. paramImplicit) patArg
       tyVarMap <- fmap (ExpressionIden . IdenVar) . (^. localTyMap) <$> get
@@ -358,8 +361,8 @@ checkPattern = go
           pat = patArg ^. patternArgPattern
           name = patArg ^. patternArgName
       whenJust name (\n -> addVar n ty argTy)
-      case pat of
-        PatternVariable v -> addVar v ty argTy
+      pat' <- case pat of
+        PatternVariable v -> addVar v ty argTy $> pat
         PatternConstructorApp a -> do
           s <- checkSaturatedInductive ty
           info <- lookupConstructor (a ^. constrAppConstructor)
@@ -388,7 +391,7 @@ checkPattern = go
                 (matchTypes patternTy (ExpressionHole hole))
                 err
               let tyArgs = zipExact indParams paramHoles
-              goConstr a tyArgs
+              PatternConstructorApp <$> goConstr indName a tyArgs
             Right (ind, tyArgs) -> do
               when
                 (ind /= constrIndName)
@@ -401,21 +404,24 @@ checkPattern = go
                           }
                     )
                 )
-              goConstr a tyArgs
+              PatternConstructorApp <$> goConstr (IdenInductive ind) a tyArgs
+      return (set patternArgPattern pat' patArg)
       where
         addVar :: VarName -> Expression -> FunctionParameter -> Sem r ()
         addVar v ty argType = do
           modify (addType v ty)
           registerIden v ty
           whenJust (argType ^. paramName) (\v' -> modify (addTypeMapping v' v))
-        goConstr :: ConstructorApp -> [(InductiveParameter, Expression)] -> Sem r ()
-        goConstr app@(ConstructorApp c ps) ctx = do
+        goConstr :: Iden -> ConstructorApp -> [(InductiveParameter, Expression)] -> Sem r ConstructorApp
+        goConstr inductivename app@(ConstructorApp c ps _) ctx = do
           (_, psTys) <- constructorArgTypes <$> lookupConstructor c
           let psTys' = map (substituteIndParams ctx) psTys
               expectedNum = length psTys
-          let w = map unnamedParameter psTys'
+              w = map unnamedParameter psTys'
           when (expectedNum /= length ps) (throw (appErr app expectedNum))
-          zipWithM_ go w ps
+          pis <- zipWithM go w ps
+          let appTy = foldExplicitApplication (ExpressionIden inductivename) (map snd ctx)
+          return app {_constrAppType = Just appTy, _constrAppParameters = pis}
         appErr :: ConstructorApp -> Int -> TypeCheckerError
         appErr app expected =
           ErrArity
@@ -555,11 +561,12 @@ inferExpression' hint e = case e of
           _caseExpressionType = Just (typedCaseExpression ^. typedType)
           _caseExpressionWholeType = Just ty
           goBranch :: CaseBranch -> Sem r CaseBranch
-          goBranch b =
-            traverseOf
-              caseBranchExpression
-              (checkClause funty (pure (b ^. caseBranchPattern)))
-              b
+          goBranch b = do
+            (onePat, _caseBranchExpression) <- checkClause funty [b ^. caseBranchPattern] (b ^. caseBranchExpression)
+            let _caseBranchPattern = case onePat of
+                  [x] -> x
+                  _ -> impossible
+            return CaseBranch {..}
             where
               funty :: Expression
               funty = ExpressionFunction (mkFunction (typedCaseExpression ^. typedType) ty)
@@ -587,8 +594,8 @@ inferExpression' hint e = case e of
       where
         goClause :: Expression -> LambdaClause -> Sem r LambdaClause
         goClause ty (LambdaClause pats body) = do
-          body' <- checkClause ty (toList pats) body
-          return (LambdaClause pats body')
+          (pats', body') <- checkClause ty (toList pats) body
+          return (LambdaClause (nonEmpty' pats') body')
 
     goUniverse :: SmallUniverse -> Sem r TypedExpression
     goUniverse u =
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
index 9f2e1bf99b..684d5f6c22 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@@ -384,7 +384,7 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) =
       (PatternVariable {}, _) -> err
       (_, PatternVariable {}) -> err
     goConstructor :: ConstructorApp -> ConstructorApp -> Sem r Bool
-    goConstructor (ConstructorApp c1 args1) (ConstructorApp c2 args2)
+    goConstructor (ConstructorApp c1 args1 _) (ConstructorApp c2 args2 _)
       | c1 /= c2 = err
       | otherwise = case zipExactMay args1 args2 of
           Nothing -> err
diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs
index 7777f16da5..5224a22e3d 100644
--- a/src/Juvix/Compiler/Pipeline.hs
+++ b/src/Juvix/Compiler/Pipeline.hs
@@ -156,17 +156,41 @@ upToCore ::
 upToCore =
   upToInternalReachability >>= Core.fromInternal
 
+upToAsm ::
+  (Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
+  Sem r Asm.InfoTable
+upToAsm =
+  upToCore >>= \Core.CoreResult {..} -> return (coreToAsm _coreResultTable)
+
 upToMiniC ::
   (Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
+  Asm.Options ->
   Sem r C.MiniCResult
-upToMiniC = upToInternalReachability >>= C.fromInternal
+upToMiniC opts =
+  upToAsm >>= asmToMiniC opts
+
+upToGeb ::
+  (Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
+  Geb.ResultSpec ->
+  Sem r Geb.Result
+upToGeb spec =
+  upToCore >>= \Core.CoreResult {..} -> coreToGeb spec _coreResultTable
+
+upToEval ::
+  (Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
+  Sem r Core.CoreResult
+upToEval =
+  upToCore >>= \r -> return r {Core._coreResultTable = Core.toEval (r ^. Core.coreResultTable)}
 
 --------------------------------------------------------------------------------
 -- Internal workflows
 --------------------------------------------------------------------------------
 
+coreToAsm :: Core.InfoTable -> Asm.InfoTable
+coreToAsm = Asm.fromCore . Stripped.fromCore . Core.toStripped
+
 coreToMiniC :: (Member (Error JuvixError) r) => Asm.Options -> Core.InfoTable -> Sem r C.MiniCResult
-coreToMiniC opts = asmToMiniC opts . Asm.fromCore . Stripped.fromCore . Core.toStripped
+coreToMiniC opts = asmToMiniC opts . coreToAsm
 
 asmToMiniC :: (Member (Error JuvixError) r) => Asm.Options -> Asm.InfoTable -> Sem r C.MiniCResult
 asmToMiniC opts = Asm.toReg opts >=> regToMiniC (opts ^. Asm.optLimits) . Reg.fromAsm
diff --git a/src/Juvix/Compiler/Pipeline/ExpressionContext.hs b/src/Juvix/Compiler/Pipeline/ExpressionContext.hs
index 9a92cc9755..cf5436218d 100644
--- a/src/Juvix/Compiler/Pipeline/ExpressionContext.hs
+++ b/src/Juvix/Compiler/Pipeline/ExpressionContext.hs
@@ -57,11 +57,10 @@ mainModuleScope e = fromJust (moduleScope e (mainModuleTopPath e))
 mainModuleTopPath :: ExpressionContext -> C.TopModulePath
 mainModuleTopPath = (^. contextScoperResult . Scoper.mainModule . C.modulePath . S.nameConcrete)
 
-transformNode :: InfoTable -> [TransformationId] -> Node -> Node
-transformNode tab ts n = snd (run (runInfoTableBuilder tab transformNode'))
-  where
-    transformNode' :: Member InfoTableBuilder r => Sem r Node
-    transformNode' = do
-      sym <- freshSymbol
-      registerIdentNode sym n
-      lookupDefault impossible sym . (^. identContext) . applyTransformations ts <$> getInfoTable
+runTransformations :: [TransformationId] -> InfoTable -> Node -> (InfoTable, Node)
+runTransformations ts tab n = snd $ run $ runInfoTableBuilder tab $ do
+  sym <- freshSymbol
+  registerIdentNode sym n
+  tab' <- applyTransformations ts <$> getInfoTable
+  let node' = lookupDefault impossible sym (tab' ^. identContext)
+  return (tab', node')
diff --git a/test/Asm/Compile/Base.hs b/test/Asm/Compile/Base.hs
index e63fcb575b..eec59dedf6 100644
--- a/test/Asm/Compile/Base.hs
+++ b/test/Asm/Compile/Base.hs
@@ -3,6 +3,7 @@ module Asm.Compile.Base where
 import Base
 import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Asm.Data.InfoTable
+import Juvix.Compiler.Asm.Error
 import Juvix.Compiler.Asm.Options
 import Juvix.Compiler.Asm.Translation.FromSource
 import Juvix.Compiler.Backend qualified as Backend
@@ -14,7 +15,9 @@ asmCompileAssertion' :: InfoTable -> Path Abs File -> Path Abs File -> (String -
 asmCompileAssertion' tab mainFile expectedFile step = do
   step "Generate C code"
   case run $ runError @JuvixError $ Pipeline.asmToMiniC asmOpts tab of
-    Left {} -> assertFailure "code generation failed"
+    Left e -> do
+      let err :: AsmError = fromJust (fromJuvixError e)
+      assertFailure ("code generation failed:" <> "\n" <> unpack (err ^. asmErrorMsg))
     Right C.MiniCResult {..} ->
       withTempDir'
         ( \dirPath -> do
diff --git a/test/BackendC.hs b/test/BackendC.hs
deleted file mode 100644
index e9f4aff0eb..0000000000
--- a/test/BackendC.hs
+++ /dev/null
@@ -1,8 +0,0 @@
-module BackendC where
-
-import BackendC.Examples qualified as E
-import BackendC.Positive qualified as P
-import Base
-
-allTests :: TestTree
-allTests = testGroup "Backend C tests" [P.allTests, E.allTests]
diff --git a/test/BackendC/Base.hs b/test/BackendC/Base.hs
deleted file mode 100644
index b36a4e68b6..0000000000
--- a/test/BackendC/Base.hs
+++ /dev/null
@@ -1,155 +0,0 @@
-module BackendC.Base where
-
-import Base
-import Data.FileEmbed
-import Data.Text.IO qualified as TIO
-import Juvix.Compiler.Backend.C.Translation.FromInternal as MiniC
-import Juvix.Compiler.Builtins (iniState)
-import Juvix.Compiler.Pipeline
-import System.Process qualified as P
-
-clangCompile ::
-  (Path Abs File -> Path Abs File -> [String]) ->
-  MiniC.MiniCResult ->
-  (Path Abs File -> IO Text) ->
-  (String -> IO ()) ->
-  IO Text
-clangCompile mkClangArgs cResult execute step =
-  withTempDir'
-    ( \dirPath -> do
-        let cOutputFile = dirPath <//> $(mkRelFile "out.c")
-            wasmOutputFile = dirPath <//> $(mkRelFile "Input.wasm")
-        TIO.writeFile (toFilePath cOutputFile) (cResult ^. MiniC.resultCCode)
-        step "WASM generation"
-        P.callProcess
-          "clang"
-          (mkClangArgs wasmOutputFile cOutputFile)
-        step "WASM execution"
-        execute wasmOutputFile
-    )
-
-wasmClangAssertionCGenOnly :: Path Abs File -> ((String -> IO ()) -> Assertion)
-wasmClangAssertionCGenOnly mainFile step = do
-  step "C Generation"
-  root <- getCurrentDir
-  let entryPoint = defaultEntryPoint root mainFile
-  (void . runIO' iniState entryPoint) upToMiniC
-
-wasmClangAssertion :: WASMInfo -> Path Abs File -> Path Abs File -> ((String -> IO ()) -> Assertion)
-wasmClangAssertion WASMInfo {..} mainFile expectedFile step = do
-  step "Check clang and wasmer are on path"
-  assertCmdExists $(mkRelFile "clang")
-  assertCmdExists $(mkRelFile "wasmer")
-  root <- getCurrentDir
-  step "C Generation"
-  let entryPoint = defaultEntryPoint root mainFile
-  p :: MiniC.MiniCResult <- snd <$> runIO' iniState entryPoint upToMiniC
-
-  expected <- TIO.readFile (toFilePath expectedFile)
-
-  step "Compile C with wasm standalone runtime"
-  actualStandalone <- clangCompile standaloneArgs p _wasmInfoActual step
-  step "Compare expected and actual program output"
-  assertEqDiffText ("Check: WASM output = " <> toFilePath expectedFile) actualStandalone expected
-
-wasiClangAssertion :: StdlibMode -> Path Abs File -> Path Abs File -> Text -> ((String -> IO ()) -> Assertion)
-wasiClangAssertion stdlibMode mainFile expectedFile stdinText step = do
-  step "Check clang and wasmer are on path"
-  assertCmdExists $(mkRelFile "clang")
-  assertCmdExists $(mkRelFile "wasmer")
-
-  step "Lookup WASI_SYSROOT_PATH"
-  sysrootPath <- getWasiSysrootPath
-
-  root <- getCurrentDir
-  step "C Generation"
-  let entryPoint = (defaultEntryPoint root mainFile) {_entryPointNoStdlib = stdlibMode == StdlibExclude}
-  p :: MiniC.MiniCResult <- snd <$> runIO' iniState entryPoint upToMiniC
-
-  expected <- TIO.readFile (toFilePath expectedFile)
-
-  let execute :: Path Abs File -> IO Text
-      execute outputFile = pack <$> P.readProcess "wasmer" [toFilePath outputFile] (unpack stdinText)
-
-  step "Compile C with standalone runtime"
-  actualStandalone <- clangCompile (wasiStandaloneArgs sysrootPath) p execute step
-  step "Compare expected and actual program output"
-  assertEqDiffText ("check: WASM output = " <> toFilePath expectedFile) actualStandalone expected
-
-  step "Compile C with libc runtime"
-  actualLibc <- clangCompile (libcArgs sysrootPath) p execute step
-  step "Compare expected and actual program output"
-  assertEqDiffText ("check: WASM output = " <> toFilePath expectedFile) actualLibc expected
-
-builtinRuntime :: Path Abs Dir
-builtinRuntime = absDir $(makeRelativeToProject "c-runtime/builtins" >>= strToExp)
-
-standaloneArgs :: Path Abs File -> Path Abs File -> [String]
-standaloneArgs wasmOutputFile cOutputFile =
-  [ "-nodefaultlibs",
-    "-std=c99",
-    "-Oz",
-    "-I",
-    toFilePath (parent minicRuntime),
-    "-I",
-    toFilePath builtinRuntime,
-    "-Werror",
-    "--target=wasm32",
-    "-nostartfiles",
-    "-Wl,--no-entry",
-    "-o",
-    toFilePath wasmOutputFile,
-    toFilePath wallocPath,
-    toFilePath cOutputFile
-  ]
-  where
-    minicRuntime :: Path Abs File
-    minicRuntime = absFile $(makeRelativeToProject "c-runtime/standalone/c-runtime.h" >>= strToExp)
-    wallocPath :: Path Abs File
-    wallocPath = absFile $(makeRelativeToProject "c-runtime/walloc/walloc.c" >>= strToExp)
-
-wasiStandaloneArgs :: Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
-wasiStandaloneArgs sysrootPath wasmOutputFile cOutputFile =
-  [ "-nodefaultlibs",
-    "-std=c99",
-    "-Oz",
-    "-I",
-    toFilePath (parent minicRuntime),
-    "-I",
-    toFilePath builtinRuntime,
-    "-Werror",
-    "--target=wasm32-wasi",
-    "--sysroot",
-    toFilePath sysrootPath,
-    "-o",
-    toFilePath wasmOutputFile,
-    toFilePath wallocPath,
-    toFilePath cOutputFile
-  ]
-  where
-    minicRuntime :: Path Abs File
-    minicRuntime = absFile $(makeRelativeToProject "c-runtime/wasi-standalone/c-runtime.h" >>= strToExp)
-    wallocPath :: Path Abs File
-    wallocPath = absFile $(makeRelativeToProject "c-runtime/walloc/walloc.c" >>= strToExp)
-
-libcArgs :: Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
-libcArgs sysrootPath wasmOutputFile cOutputFile =
-  [ "-nodefaultlibs",
-    "-std=c99",
-    "-Oz",
-    "-I",
-    toFilePath (parent minicRuntime),
-    "-I",
-    toFilePath builtinRuntime,
-    "-Werror",
-    "-lc",
-    "--target=wasm32-wasi",
-    "--sysroot",
-    toFilePath sysrootPath,
-    "-o",
-    toFilePath wasmOutputFile,
-    toFilePath cOutputFile
-  ]
-  where
-    minicRuntime :: Path Abs File
-    minicRuntime = absFile $(makeRelativeToProject "c-runtime/wasi-libc/c-runtime.h" >>= strToExp)
diff --git a/test/BackendC/Examples.hs b/test/BackendC/Examples.hs
deleted file mode 100644
index 4ead341f34..0000000000
--- a/test/BackendC/Examples.hs
+++ /dev/null
@@ -1,75 +0,0 @@
-module BackendC.Examples where
-
-import BackendC.Base
-import Base
-import Data.FileEmbed
-
-data ExampleTest
-  = ExampleExecTest ExecTest
-  | ExampleCGenOnlyTest TestSpec
-
-data TestSpec = TestSpec
-  { _name :: String,
-    _testDir :: Path Rel Dir,
-    _mainFile :: Path Rel File
-  }
-
-data ExecTest = ExecTest
-  { _spec :: TestSpec,
-    _expectedDir :: Path Rel Dir,
-    _stdinText :: Text,
-    _compileMode :: CompileMode
-  }
-
-makeLenses ''ExecTest
-makeLenses ''TestSpec
-
-execTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel Dir -> Text -> CompileMode -> ExecTest
-execTest _name _testDir _mainFile _expectedDir _stdinText _compileMode = ExecTest {_spec = TestSpec {..}, ..}
-
-exampleRoot :: Path Abs Dir
-exampleRoot = absDir $(makeRelativeToProject (toFilePath $(mkRelDir "examples/milestone")) >>= strToExp)
-
-testDescr :: ExampleTest -> TestDescr
-testDescr = \case
-  ExampleExecTest ExecTest {..} ->
-    let mainRoot = exampleRoot <//> _spec ^. testDir
-        mainFile' = mainRoot <//> (_spec ^. mainFile)
-        expectedFile = absDir $(makeRelativeToProject "tests/examplesExpected" >>= strToExp) <//> _expectedDir <//> $(mkRelFile "expected.golden")
-     in TestDescr
-          { _testName = _spec ^. name,
-            _testRoot = mainRoot,
-            _testAssertion = case _compileMode of
-              WASI stdlibMode -> Steps $ wasiClangAssertion stdlibMode mainFile' expectedFile _stdinText
-              WASM i -> Steps $ wasmClangAssertion i mainFile' expectedFile
-          }
-  ExampleCGenOnlyTest TestSpec {..} ->
-    let mainRoot = exampleRoot <//> _testDir
-        mainFile' = mainRoot <//> _mainFile
-     in TestDescr
-          { _testName = _name,
-            _testRoot = mainRoot,
-            _testAssertion = Steps $ wasmClangAssertionCGenOnly mainFile'
-          }
-
-allTests :: TestTree
-allTests =
-  testGroup
-    "Backend C milestone example tests"
-    (map (mkTest . testDescr) tests)
-
-tests :: [ExampleTest]
-tests =
-  map ExampleExecTest execTests <> map ExampleCGenOnlyTest testSpecs
-  where
-    execTests :: [ExecTest]
-    execTests =
-      [ execTest "Validity Predicate example" $(mkRelDir "ValidityPredicates") $(mkRelFile "Tests.juvix") $(mkRelDir "ValidityPredicates") "" (WASI StdlibInclude),
-        execTest "TicTacToe CLI example" $(mkRelDir "TicTacToe") $(mkRelFile "CLI/TicTacToe.juvix") $(mkRelDir "TicTacToe") "aaa\n0\n10\n1\n2\n3\n3\n4\n5\n6\n7\n8\n9\n" (WASI StdlibInclude),
-        execTest "Fibonacci example" $(mkRelDir "Fibonacci") $(mkRelFile "Fibonacci.juvix") $(mkRelDir "Fibonacci") "" (WASI StdlibInclude),
-        execTest "Collatz sequence generator" $(mkRelDir "Collatz") $(mkRelFile "Collatz.juvix") $(mkRelDir "Collatz") "123\n" (WASI StdlibInclude),
-        execTest "Towers of Hanoi" $(mkRelDir "Hanoi") $(mkRelFile "Hanoi.juvix") $(mkRelDir "Hanoi") "" (WASI StdlibInclude),
-        execTest "Pascal's triangle" $(mkRelDir "PascalsTriangle") $(mkRelFile "PascalsTriangle.juvix") $(mkRelDir "PascalsTriangle") "" (WASI StdlibInclude)
-      ]
-    testSpecs :: [TestSpec]
-    testSpecs = [TestSpec "TicTacToe Web example (C gen only)" $(mkRelDir "TicTacToe") $(mkRelFile "Web/TicTacToe.juvix")]
diff --git a/test/BackendC/Positive.hs b/test/BackendC/Positive.hs
deleted file mode 100644
index 2777ab6107..0000000000
--- a/test/BackendC/Positive.hs
+++ /dev/null
@@ -1,89 +0,0 @@
-module BackendC.Positive where
-
-import BackendC.Base
-import Base
-import System.Process qualified as P
-
-data PosTest = PosTest
-  { _name :: String,
-    _relDir :: Path Rel Dir,
-    _compileMode :: CompileMode
-  }
-
-makeLenses ''PosTest
-
-root :: Path Abs Dir
-root = relToProject $(mkRelDir "tests/positive/MiniC")
-
-mainFile :: Path Rel File
-mainFile = $(mkRelFile "Input.juvix")
-
-expectedFile :: Path Rel File
-expectedFile = $(mkRelFile "expected.golden")
-
-actualCallExport :: Text -> [Text] -> Path Abs File -> IO Text
-actualCallExport funName funArgs outputFile =
-  pack
-    <$> P.readProcess
-      "wasmer"
-      (["run", toFilePath outputFile, "--invoke", unpack funName] <> (unpack <$> funArgs))
-      ""
-
-actualCallNode :: Path Rel File -> Path Abs File -> IO Text
-actualCallNode jsFile outputFile = do
-  assertCmdExists $(mkRelFile "node")
-  let outputDir = parent outputFile
-      outputJsFile = outputDir <//> jsFile
-  copyFile jsFile outputJsFile
-  withCurrentDir
-    outputDir
-    ( pack
-        <$> P.readProcess
-          "node"
-          [toFilePath outputJsFile]
-          ""
-    )
-
-testDescr :: PosTest -> TestDescr
-testDescr PosTest {..} =
-  let tRoot = root <//> _relDir
-      mainFile' = tRoot <//> mainFile
-      expectedFile' = tRoot <//> expectedFile
-   in TestDescr
-        { _testName = _name,
-          _testRoot = tRoot,
-          _testAssertion = Steps $ case _compileMode of
-            WASI stdlibMode -> wasiClangAssertion stdlibMode mainFile' expectedFile' ""
-            WASM i -> wasmClangAssertion i mainFile' expectedFile'
-        }
-
-allTests :: TestTree
-allTests =
-  testGroup
-    "Backend C positive tests"
-    (map (mkTest . testDescr) tests)
-
-tests :: [PosTest]
-tests =
-  [ PosTest "HelloWorld" $(mkRelDir "HelloWorld") (WASI StdlibExclude),
-    PosTest "Inductive types and pattern matching" $(mkRelDir "Nat") (WASI StdlibExclude),
-    PosTest "Polymorphic types" $(mkRelDir "Polymorphism") (WASI StdlibExclude),
-    PosTest "Polymorphic axioms" $(mkRelDir "PolymorphicAxioms") (WASI StdlibExclude),
-    PosTest "Polymorphic target" $(mkRelDir "PolymorphicTarget") (WASI StdlibExclude),
-    PosTest "Multiple modules" $(mkRelDir "MultiModules") (WASI StdlibExclude),
-    PosTest "Higher Order Functions" $(mkRelDir "HigherOrder") (WASI StdlibExclude),
-    PosTest "Higher Order Functions and explicit holes" $(mkRelDir "PolymorphismHoles") (WASI StdlibExclude),
-    PosTest "Closures with no environment" $(mkRelDir "ClosureNoEnv") (WASI StdlibExclude),
-    PosTest "Closures with environment" $(mkRelDir "ClosureEnv") (WASI StdlibExclude),
-    PosTest "SimpleFungibleTokenImplicit" $(mkRelDir "SimpleFungibleTokenImplicit") (WASI StdlibExclude),
-    PosTest "Mutually recursive function" $(mkRelDir "MutuallyRecursive") (WASI StdlibExclude),
-    PosTest "Nested List type" $(mkRelDir "NestedList") (WASI StdlibExclude),
-    PosTest "Builtin types and functions" $(mkRelDir "Builtins") (WASI StdlibExclude),
-    PosTest "Builtin types and functions from stdlib" $(mkRelDir "BuiltinsStdlib") (WASI StdlibInclude),
-    PosTest "Import from embedded standard library" $(mkRelDir "StdlibImport") (WASI StdlibInclude),
-    PosTest "Axiom without a compile block" $(mkRelDir "AxiomNoCompile") (WASI StdlibInclude),
-    PosTest "Invoke a function using exported name" $(mkRelDir "ExportName") (WASM (WASMInfo (actualCallExport "fun" []))),
-    PosTest "Invoke a function using exported name with args" $(mkRelDir "ExportNameArgs") (WASM (WASMInfo (actualCallExport "fun" ["0"]))),
-    PosTest "Invoke an imported function in Juvix and exported function in JS" $(mkRelDir "ImportExportName") (WASM (WASMInfo (actualCallNode $(mkRelFile "input.js")))),
-    PosTest "Invoke an exported function using Anoma _validate_tx signature" $(mkRelDir "AlwaysValidVP") (WASM (WASMInfo (actualCallNode $(mkRelFile "input.js"))))
-  ]
diff --git a/test/BackendGeb/Eval/Base.hs b/test/BackendGeb/Eval/Base.hs
index 821f24fa97..a5e3aec710 100644
--- a/test/BackendGeb/Eval/Base.hs
+++ b/test/BackendGeb/Eval/Base.hs
@@ -16,7 +16,7 @@ gebEvalAssertion mainFile expectedFile step = do
   case Geb.runParser mainFile input of
     Left err -> assertFailure (show (pretty err))
     Right (Geb.ExpressionObject _) -> do
-      step "No evalution for objects"
+      step "No evaluation for objects"
       assertFailure (unpack Geb.objNoEvalMsg)
     Right (Geb.ExpressionMorphism gebMorphism) ->
       gebEvalAssertion' mainFile expectedFile step gebMorphism
diff --git a/test/Compilation/Base.hs b/test/Compilation/Base.hs
index cf072826da..34bbca9b7d 100644
--- a/test/Compilation/Base.hs
+++ b/test/Compilation/Base.hs
@@ -1,50 +1,24 @@
 module Compilation.Base where
 
 import Base
+import Core.Compile.Base
 import Core.Eval.Base
-import Data.HashMap.Strict qualified as HashMap
-import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Builtins (iniState)
-import Juvix.Compiler.Core.Data.InfoTable qualified as Core
-import Juvix.Compiler.Core.Extra
-import Juvix.Compiler.Core.Info qualified as Info
-import Juvix.Compiler.Core.Info.NoDisplayInfo
 import Juvix.Compiler.Core.Pipeline qualified as Core
-import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Translation.FromInternal.Data qualified as Core
 import Juvix.Compiler.Pipeline
 
 compileAssertion ::
+  Bool ->
   Path Abs File ->
   Path Abs File ->
   (String -> IO ()) ->
   Assertion
-compileAssertion mainFile expectedFile step = do
+compileAssertion onlyEval mainFile expectedFile step = do
   step "Translate to JuvixCore"
   cwd <- getCurrentDir
   let entryPoint = defaultEntryPoint cwd mainFile
-  tab' <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
-  let tab = Core.toEval tab'
-  case (tab ^. Core.infoMain) >>= ((tab ^. Core.identContext) HashMap.!?) of
-    Just node -> do
-      withTempDir'
-        ( \dirPath -> do
-            let outputFile = dirPath <//> $(mkRelFile "out.out")
-            hout <- openFile (toFilePath outputFile) WriteMode
-            step "Evaluate"
-            r' <- doEval mainFile hout tab node
-            case r' of
-              Left err -> do
-                hClose hout
-                assertFailure (show (pretty err))
-              Right value -> do
-                unless
-                  (Info.member kNoDisplayInfo (getInfo value))
-                  (hPutStrLn hout (ppPrint value))
-                hClose hout
-                actualOutput <- TIO.readFile (toFilePath outputFile)
-                step "Compare expected and actual program output"
-                expected <- TIO.readFile (toFilePath expectedFile)
-                assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) actualOutput expected
-        )
-    Nothing -> assertFailure ("No main function registered in: " <> toFilePath mainFile)
+  tab <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
+  coreEvalAssertion' (Core.toEval tab) mainFile expectedFile step
+  unless onlyEval $
+    coreCompileAssertion' tab mainFile expectedFile step
diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs
index 32c255ed01..a116aa3bd1 100644
--- a/test/Compilation/Positive.hs
+++ b/test/Compilation/Positive.hs
@@ -7,6 +7,7 @@ data PosTest = PosTest
   { _name :: String,
     _dir :: Path Abs Dir,
     _file :: Path Abs File,
+    _onlyEval :: Bool,
     _expectedFile :: Path Abs File
   }
 
@@ -26,32 +27,29 @@ toTestDescr PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ compileAssertion file' expected'
+          _testAssertion = Steps $ compileAssertion _onlyEval file' expected'
         }
 
-filterOutTests :: [String] -> [PosTest] -> [PosTest]
-filterOutTests out = filter (\PosTest {..} -> _name `notElem` out)
-
 allTests :: TestTree
 allTests =
   testGroup
     "Juvix compilation pipeline positive tests"
-    ( map
-        (mkTest . toTestDescr)
-        ( filterOutTests
-            [ "Nested binders with variable capture"
-            ]
-            tests
-        )
-    )
+    (map (mkTest . toTestDescr) tests)
 
-posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
-posTest _name rdir rfile routfile =
+posTest' :: Bool -> String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
+posTest' _onlyEval _name rdir rfile routfile =
   let _dir = root <//> rdir
       _file = _dir <//> rfile
       _expectedFile = root <//> routfile
    in PosTest {..}
 
+posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
+posTest = posTest' False
+
+-- tests which use large integers are only evaluated but not compiled
+posTestEval :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
+posTestEval = posTest' True
+
 tests :: [PosTest]
 tests =
   [ posTest
@@ -104,7 +102,7 @@ tests =
       $(mkRelDir ".")
       $(mkRelFile "test010.juvix")
       $(mkRelFile "out/test010.out"),
-    posTest
+    posTestEval
       "Tail recursion: Fibonacci numbers in linear time"
       $(mkRelDir ".")
       $(mkRelFile "test011.juvix")
diff --git a/test/Core/Asm/Positive.hs b/test/Core/Asm/Positive.hs
index d05ce688e4..cd4eeaab74 100644
--- a/test/Core/Asm/Positive.hs
+++ b/test/Core/Asm/Positive.hs
@@ -8,9 +8,7 @@ allTests :: TestTree
 allTests = testGroup "JuvixCore to JuvixAsm positive tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.tests))
 
 ignoredTests :: [String]
-ignoredTests =
-  [ "Match with complex patterns"
-  ]
+ignoredTests = []
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =
diff --git a/test/Core/Compile/Base.hs b/test/Core/Compile/Base.hs
index 998f083e55..4ee139eef7 100644
--- a/test/Core/Compile/Base.hs
+++ b/test/Core/Compile/Base.hs
@@ -5,6 +5,8 @@ import Base
 import Core.Eval.Base
 import Core.Eval.Positive qualified as Eval
 import Data.Text.IO qualified as TIO
+import GHC.Base (seq)
+import Juvix.Compiler.Asm.Pretty qualified as Asm
 import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm
 import Juvix.Compiler.Core.Pipeline
 import Juvix.Compiler.Core.Translation.FromSource
@@ -42,7 +44,8 @@ coreCompileAssertion' ::
 coreCompileAssertion' tab mainFile expectedFile step = do
   step "Translate to JuvixAsm"
   let tab' = Asm.fromCore $ Stripped.fromCore $ toStripped tab
-  Asm.asmCompileAssertion' tab' mainFile expectedFile step
+  length (fromText (Asm.ppPrint tab' tab') :: String) `seq`
+    Asm.asmCompileAssertion' tab' mainFile expectedFile step
 
 coreCompileAssertion ::
   Path Abs File ->
diff --git a/test/Core/Compile/Positive.hs b/test/Core/Compile/Positive.hs
index 4b1804f936..67a44442ea 100644
--- a/test/Core/Compile/Positive.hs
+++ b/test/Core/Compile/Positive.hs
@@ -7,7 +7,7 @@ import Core.Eval.Positive qualified as Eval
 allTests :: TestTree
 allTests = testGroup "JuvixCore compilation tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.tests))
 
--- Arbitrary precision integers and general pattern matching not yet supported
+-- Arbitrary precision integers not yet supported
 ignoredTests :: [String]
 ignoredTests =
   [ "Tail recursion: Fibonacci numbers in linear time",
@@ -15,8 +15,7 @@ ignoredTests =
     "Nested 'case', 'let' and 'if' with variable capture",
     "Mutual recursion",
     "LetRec",
-    "Big numbers",
-    "Match with complex patterns"
+    "Big numbers"
   ]
 
 liftTest :: Eval.PosTest -> TestTree
diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs
index 1c2a4f8fcd..7178ad1419 100644
--- a/test/Core/Eval/Base.hs
+++ b/test/Core/Eval/Base.hs
@@ -1,7 +1,9 @@
 module Core.Eval.Base where
 
 import Base
+import Data.HashMap.Strict qualified as HashMap
 import Data.Text.IO qualified as TIO
+import GHC.Base (seq)
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Evaluator
@@ -13,6 +15,38 @@ import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation
 import Juvix.Compiler.Core.Translation.FromSource
 
+coreEvalAssertion' ::
+  InfoTable ->
+  Path Abs File ->
+  Path Abs File ->
+  (String -> IO ()) ->
+  Assertion
+coreEvalAssertion' tab mainFile expectedFile step =
+  length (fromText (ppPrint tab) :: String) `seq`
+    case (tab ^. infoMain) >>= ((tab ^. identContext) HashMap.!?) of
+      Just node -> do
+        withTempDir'
+          ( \dirPath -> do
+              let outputFile = dirPath <//> $(mkRelFile "out.out")
+              hout <- openFile (toFilePath outputFile) WriteMode
+              step "Evaluate"
+              r' <- doEval mainFile hout tab node
+              case r' of
+                Left err -> do
+                  hClose hout
+                  assertFailure (show (pretty err))
+                Right value -> do
+                  unless
+                    (Info.member kNoDisplayInfo (getInfo value))
+                    (hPutStrLn hout (ppPrint value))
+                  hClose hout
+                  actualOutput <- TIO.readFile (toFilePath outputFile)
+                  step "Compare expected and actual program output"
+                  expected <- TIO.readFile (toFilePath expectedFile)
+                  assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) actualOutput expected
+          )
+      Nothing -> assertFailure ("No main function registered in: " <> toFilePath mainFile)
+
 coreEvalAssertion ::
   Path Abs File ->
   Path Abs File ->
@@ -32,27 +66,7 @@ coreEvalAssertion mainFile expectedFile trans testTrans step = do
     Right (tabIni, Just node) -> do
       let tab = applyTransformations trans (setupMainFunction tabIni node)
       testTrans tab
-      let node' = fromJust $ tab ^. identContext . at (fromJust $ tab ^. infoMain)
-      withTempDir'
-        ( \dirPath -> do
-            let outputFile = dirPath <//> $(mkRelFile "out.out")
-            hout <- openFile (toFilePath outputFile) WriteMode
-            step "Evaluate"
-            r' <- doEval mainFile hout tab node'
-            case r' of
-              Left err -> do
-                hClose hout
-                assertFailure (show (pretty err))
-              Right value -> do
-                unless
-                  (Info.member kNoDisplayInfo (getInfo value))
-                  (hPutStrLn hout (ppPrint value))
-                hClose hout
-                actualOutput <- TIO.readFile (toFilePath outputFile)
-                step "Compare expected and actual program output"
-                expected <- TIO.readFile (toFilePath expectedFile)
-                assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) actualOutput expected
-        )
+      coreEvalAssertion' tab mainFile expectedFile step
 
 coreEvalErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
 coreEvalErrorAssertion mainFile step = do
diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs
index 681edd20b4..9fe44dc075 100644
--- a/test/Core/Eval/Positive.hs
+++ b/test/Core/Eval/Positive.hs
@@ -10,6 +10,8 @@ data PosTest = PosTest
     _expectedFile :: Path Rel File
   }
 
+makeLenses ''PosTest
+
 root :: Path Abs Dir
 root = relToProject $(mkRelDir "tests/Core/positive")
 
@@ -274,5 +276,55 @@ tests =
       "String builtins"
       $(mkRelDir ".")
       $(mkRelFile "test048.jvc")
-      $(mkRelFile "out/test048.out")
+      $(mkRelFile "out/test048.out"),
+    PosTest
+      "Lifting and polymorphism"
+      $(mkRelDir ".")
+      $(mkRelFile "test049.jvc")
+      $(mkRelFile "out/test049.out"),
+    PosTest
+      "Church numerals with pattern matching"
+      $(mkRelDir ".")
+      $(mkRelFile "test050.jvc")
+      $(mkRelFile "out/test050.out"),
+    PosTest
+      "Type annotations for patterns"
+      $(mkRelDir ".")
+      $(mkRelFile "test051.jvc")
+      $(mkRelFile "out/test051.out"),
+    PosTest
+      "foldl with match"
+      $(mkRelDir ".")
+      $(mkRelFile "test052.jvc")
+      $(mkRelFile "out/test052.out"),
+    PosTest
+      "Match with higher-order polymorphic functions"
+      $(mkRelDir ".")
+      $(mkRelFile "test053.jvc")
+      $(mkRelFile "out/test053.out"),
+    PosTest
+      "Typed match"
+      $(mkRelDir ".")
+      $(mkRelFile "test054.jvc")
+      $(mkRelFile "out/test054.out"),
+    PosTest
+      "Eta-expansion of polymorphic constructors"
+      $(mkRelDir ".")
+      $(mkRelFile "test055.jvc")
+      $(mkRelFile "out/test055.out"),
+    PosTest
+      "LetRec with type annotations"
+      $(mkRelDir ".")
+      $(mkRelFile "test056.jvc")
+      $(mkRelFile "out/test056.out"),
+    PosTest
+      "Type synonyms"
+      $(mkRelDir ".")
+      $(mkRelFile "test057.jvc")
+      $(mkRelFile "out/test057.out"),
+    PosTest
+      "Lifting and partial application"
+      $(mkRelDir ".")
+      $(mkRelFile "test058.jvc")
+      $(mkRelFile "out/test058.out")
   ]
diff --git a/test/Core/Transformation/Pipeline.hs b/test/Core/Transformation/Pipeline.hs
index 04069acfb5..ba668de14f 100644
--- a/test/Core/Transformation/Pipeline.hs
+++ b/test/Core/Transformation/Pipeline.hs
@@ -3,7 +3,6 @@ module Core.Transformation.Pipeline (allTests) where
 import Base
 import Core.Eval.Positive qualified as Eval
 import Core.Transformation.Base
-import Juvix.Compiler.Core.Pipeline
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
diff --git a/test/Internal/Eval/Base.hs b/test/Internal/Eval/Base.hs
index ccf0eddc0e..62a1ee4e70 100644
--- a/test/Internal/Eval/Base.hs
+++ b/test/Internal/Eval/Base.hs
@@ -10,6 +10,7 @@ import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo
 import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Transformation (etaExpansionApps)
 import Juvix.Compiler.Core.Translation.FromInternal.Data as Core
 import Juvix.Compiler.Pipeline
 
@@ -18,7 +19,8 @@ internalCoreAssertion mainFile expectedFile step = do
   step "Translate to Core"
   cwd <- getCurrentDir
   let entryPoint = defaultEntryPoint cwd mainFile
-  tab <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
+  tab0 <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
+  let tab = etaExpansionApps tab0
   case (tab ^. infoMain) >>= ((tab ^. identContext) HashMap.!?) of
     Just node -> do
       withTempDir'
diff --git a/test/Main.hs b/test/Main.hs
index 0c5fdb379d..efd80ab6b9 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,7 +2,6 @@ module Main (main) where
 
 import Arity qualified
 import Asm qualified
-import BackendC qualified
 import BackendGeb qualified
 import Base
 import Compilation qualified
@@ -20,8 +19,7 @@ slowTests :: TestTree
 slowTests =
   testGroup
     "Juvix slow tests"
-    [ BackendC.allTests,
-      BackendGeb.allTests,
+    [ BackendGeb.allTests,
       Runtime.allTests,
       Asm.allTests,
       Core.allTests,
diff --git a/tests/Asm/negative/vtest010.jva b/tests/Asm/negative/vtest010.jva
index 7d8dd70818..298414adc2 100644
--- a/tests/Asm/negative/vtest010.jva
+++ b/tests/Asm/negative/vtest010.jva
@@ -1,6 +1,6 @@
 -- Value stack type mismatch
 
-function id(*) {
+function id(integer) : integer {
   push arg[0];
   ret;
 }
diff --git a/tests/Compilation/positive/out/test035.out b/tests/Compilation/positive/out/test035.out
index c5b601879d..80257c93d2 100644
--- a/tests/Compilation/positive/out/test035.out
+++ b/tests/Compilation/positive/out/test035.out
@@ -1,9 +1,9 @@
 9 :: 7 :: 5 :: 3 :: 1 :: nil
-20300
-1380938444160
-328376729742336
-635244975397025280
-10896523177832686508800
-209585186558797617308313141313536
+300
+4160
+2336
+5280
+8800
+13536
 1
 0
diff --git a/tests/Compilation/positive/test005.juvix b/tests/Compilation/positive/test005.juvix
index d2e898b3b4..02556ff5fa 100644
--- a/tests/Compilation/positive/test005.juvix
+++ b/tests/Compilation/positive/test005.juvix
@@ -13,6 +13,6 @@ I : {A : Type} → A → A;
 I := S K (K {_} {Bool});
 
 main : IO;
-main := printNatLn $ I 1 + I I 1 + I (I 1) + I I I 1 + I (I I) I (I I I) 1 + I I I (I I I (I I)) I (I I) I I I 1;
+main := printNatLn (I 1 + I I 1 + I (I 1) + I I I 1 + I (I I) I (I I I) 1 + I I I (I I I (I I)) I (I I) I I I 1);
 
 end;
diff --git a/tests/Compilation/positive/test030.juvix b/tests/Compilation/positive/test030.juvix
index 32a3ed0bcb..8d53e58156 100644
--- a/tests/Compilation/positive/test030.juvix
+++ b/tests/Compilation/positive/test030.juvix
@@ -4,7 +4,9 @@ module test030;
 open import Stdlib.Prelude;
 
 iterate : {A : Type} → (A → A) → Nat → A → A;
-iterate f zero x := x;
+-- clauses with differing number of patterns not yet supported
+-- iterate f zero x := x;
+iterate f zero := id;
 iterate f (suc n) := f ∘ (iterate f n);
 
 plus : Nat → Nat → Nat;
diff --git a/tests/Compilation/positive/test035.juvix b/tests/Compilation/positive/test035.juvix
index 9f7752392d..b106023408 100644
--- a/tests/Compilation/positive/test035.juvix
+++ b/tests/Compilation/positive/test035.juvix
@@ -28,9 +28,9 @@ f leaf := 1;
 f (node l r) :=
   case g l, g r
     | (leaf, leaf) := 3
-    | (node l r, leaf) := (f l + f r) * 2
-    | (node l1 r1, node l2 r2) := (f l1 + f r1) * (f l2 + f r2)
-    | (_, node l r) := f l + f r;
+    | (node l r, leaf) := mod ((f l + f r) * 2) 20000
+    | (node l1 r1, node l2 r2) := mod ((f l1 + f r1) * (f l2 + f r2)) 20000
+    | (_, node l r) := mod (f l + f r) 20000;
 
 g leaf := leaf;
 g (node (node _ _) r) := r;
diff --git a/tests/Compilation/positive/test036.juvix b/tests/Compilation/positive/test036.juvix
index 0ae0ad9918..e9f988e8d8 100644
--- a/tests/Compilation/positive/test036.juvix
+++ b/tests/Compilation/positive/test036.juvix
@@ -1,7 +1,7 @@
 -- eta-expansion
 module test036;
 
-open import Stdlib.Prelude public;
+open import Stdlib.Prelude;
 
 expand : {A : Type} → A → Nat → A;
 expand f x := f;
diff --git a/tests/Core/positive/out/test041.out b/tests/Core/positive/out/test041.out
index 2f5bb2d1ca..f24de3c69b 100644
--- a/tests/Core/positive/out/test041.out
+++ b/tests/Core/positive/out/test041.out
@@ -1,7 +1,7 @@
 cons 9 (cons 7 (cons 5 (cons 3 (cons 1 nil))))
 -12096
--1448007509520
-5510602057585725
--85667472308246220
-527851146861989286336
--441596546382859135501706333021475
+10480
+5725
+13780
+-13664
+18525
diff --git a/tests/Core/positive/out/test049.out b/tests/Core/positive/out/test049.out
new file mode 100644
index 0000000000..d00491fd7e
--- /dev/null
+++ b/tests/Core/positive/out/test049.out
@@ -0,0 +1 @@
+1
diff --git a/tests/Core/positive/out/test050.out b/tests/Core/positive/out/test050.out
new file mode 100644
index 0000000000..00750edc07
--- /dev/null
+++ b/tests/Core/positive/out/test050.out
@@ -0,0 +1 @@
+3
diff --git a/tests/Core/positive/out/test051.out b/tests/Core/positive/out/test051.out
new file mode 100644
index 0000000000..d00491fd7e
--- /dev/null
+++ b/tests/Core/positive/out/test051.out
@@ -0,0 +1 @@
+1
diff --git a/tests/Core/positive/out/test052.out b/tests/Core/positive/out/test052.out
new file mode 100644
index 0000000000..1e8b314962
--- /dev/null
+++ b/tests/Core/positive/out/test052.out
@@ -0,0 +1 @@
+6
diff --git a/tests/Core/positive/out/test053.out b/tests/Core/positive/out/test053.out
new file mode 100644
index 0000000000..8f92bfdd49
--- /dev/null
+++ b/tests/Core/positive/out/test053.out
@@ -0,0 +1 @@
+35
diff --git a/tests/Core/positive/out/test054.out b/tests/Core/positive/out/test054.out
new file mode 100644
index 0000000000..bbad99e187
--- /dev/null
+++ b/tests/Core/positive/out/test054.out
@@ -0,0 +1,7 @@
+25
+-12096
+10480
+5725
+13780
+-13664
+18525
diff --git a/tests/Core/positive/out/test055.out b/tests/Core/positive/out/test055.out
new file mode 100644
index 0000000000..d00491fd7e
--- /dev/null
+++ b/tests/Core/positive/out/test055.out
@@ -0,0 +1 @@
+1
diff --git a/tests/Core/positive/out/test056.out b/tests/Core/positive/out/test056.out
new file mode 100644
index 0000000000..b8626c4cff
--- /dev/null
+++ b/tests/Core/positive/out/test056.out
@@ -0,0 +1 @@
+4
diff --git a/tests/Core/positive/out/test057.out b/tests/Core/positive/out/test057.out
new file mode 100644
index 0000000000..7ed6ff82de
--- /dev/null
+++ b/tests/Core/positive/out/test057.out
@@ -0,0 +1 @@
+5
diff --git a/tests/Core/positive/out/test058.out b/tests/Core/positive/out/test058.out
new file mode 100644
index 0000000000..7ed6ff82de
--- /dev/null
+++ b/tests/Core/positive/out/test058.out
@@ -0,0 +1 @@
+5
diff --git a/tests/Core/positive/test022.jvc b/tests/Core/positive/test022.jvc
index ee1f74ddd3..87ed2a3d51 100644
--- a/tests/Core/positive/test022.jvc
+++ b/tests/Core/positive/test022.jvc
@@ -1,4 +1,4 @@
--- power
+-- fast exponentiation
 
 def power' := \a \b \acc
   if b = 0 then
diff --git a/tests/Core/positive/test041.jvc b/tests/Core/positive/test041.jvc
index 133f30283c..ea824f287f 100644
--- a/tests/Core/positive/test041.jvc
+++ b/tests/Core/positive/test041.jvc
@@ -28,9 +28,9 @@ def f := \t match t with {
   node l r :=
     match g l, g r with {
       leaf, leaf := 0 - 6;
-      node l r, leaf := (f l + f r) * 2;
-      node l1 r1, node l2 r2 := (f l1 + f r1) * (f l2 + f r2);
-      _, node l r := (f l + f r) * (0 - 3)
+      node l r, leaf := ((f l + f r) * 2) % 20000;
+      node l1 r1, node l2 r2 := ((f l1 + f r1) * (f l2 + f r2)) % 20000;
+      _, node l r := ((f l + f r) * (0 - 3)) % 20000;
     }
 };
 
diff --git a/tests/Core/positive/test043.jvc b/tests/Core/positive/test043.jvc
index b46150e86a..df4f88dc96 100644
--- a/tests/Core/positive/test043.jvc
+++ b/tests/Core/positive/test043.jvc
@@ -2,9 +2,10 @@
 
 def fun := λ(A : Type) λ(x : A) let f := λ(h : A → A) h (h x) in f (λ(y : A) x);
 
-def fun' := λ(T : Type → Type) λ(A : Type) λ(B : T A) λ(x : B)
+def fun' : Π T : Type → Type, Π X : Type, Π A : Type, any :=
+  λ(T : Type → Type) λ(_ : Type) λ(A : Type) λ(B : T A) λ(x : B)
   let f := λ(g : B → B) g (g x) in
   let h := λ(b : B) λ(a : A) a * b - b in
   f (λ(y : B) h y x);
 
-fun int 2 + fun' (λ(A : Type) A) int int 3
+fun int 2 + fun' (λ(A : Type) A) bool int int 3
diff --git a/tests/Core/positive/test049.jvc b/tests/Core/positive/test049.jvc
new file mode 100644
index 0000000000..93639e0c34
--- /dev/null
+++ b/tests/Core/positive/test049.jvc
@@ -0,0 +1,15 @@
+-- lifting and polymorphism
+
+type Boxed {
+    Box : Π A : Type, A → Boxed A
+};
+
+def g : Π A : Type, A → Boxed A → A → A := λ(A : Type) λ(a : A) λ(_ : Boxed A) λ(a' : A) a;
+
+def f : Π A : Type, int → int → Boxed A → int → A → A :=
+    λ(A : Type) λ(n : int) λ(m : int) λ(b : Boxed A) λ(k : int) λ(a' : A)
+        case b of {
+            Box _ a := (λ(_ : int) g A a b a') (n + m + k);
+        };
+
+f int 0 1 (Box int 1) 2 3
diff --git a/tests/Core/positive/test050.jvc b/tests/Core/positive/test050.jvc
new file mode 100644
index 0000000000..3ed80ae12c
--- /dev/null
+++ b/tests/Core/positive/test050.jvc
@@ -0,0 +1,24 @@
+-- Church numerals with pattern matching
+
+def czero : Π A : Type, (A → A) → A → A :=
+  λ(A : Type) λ(f : A → A) λ(x : A) x;
+
+def csuc : (Π A : Type, (A → A) → A → A) → Π A : Type, (A → A) → A → A :=
+  λ(n : Π A : Type, (A → A) → A → A) λ(A : Type) λ(f : A → A) λ(x : A) f (n A f x);
+
+def num : nat → Π A : Type, (A → A) → A → A :=
+  λ(n : nat) match n : nat with : Π A : Type, (A → A) → A → A {
+    zero := czero;
+    suc (n : nat) := csuc (num n);
+  };
+
+def toNat : (Π A : Type, (A → A) → A → A) → nat :=
+  λ(n : Π A : Type, (A → A) → A → A) n nat suc zero;
+
+def toInt : nat → int :=
+  λ(n : nat) case n of {
+    zero := 0;
+    suc n := toInt n + 1;
+  };
+
+toInt (toNat (num (suc (suc (suc zero)))))
diff --git a/tests/Core/positive/test051.jvc b/tests/Core/positive/test051.jvc
new file mode 100644
index 0000000000..b206d0a299
--- /dev/null
+++ b/tests/Core/positive/test051.jvc
@@ -0,0 +1,13 @@
+-- Type annotations for patterns
+
+type Box {
+    box : Π A : Type, A → Box A;
+};
+
+def f : Box (Π A : Type, A → A) → int := \(x : Box (Π A : Type, A → A))
+    match x : Box (Π A : Type, A → A) with : int {
+        box _ (g : Π A : Type, A → A) : Box (Π A : Type, A → A)  := g int 1;
+    };
+
+f (box (Π A : Type, A → A) \(A : Type) \(x : A) x)
+-- result: 1
diff --git a/tests/Core/positive/test052.jvc b/tests/Core/positive/test052.jvc
new file mode 100644
index 0000000000..c77e539efd
--- /dev/null
+++ b/tests/Core/positive/test052.jvc
@@ -0,0 +1,15 @@
+-- foldl with match
+
+type List {
+    nil : Π A : Type, List A;
+    cons : Π A : Type, A → List A → List A;
+};
+
+def foldl : Π A : Type, Π B : Type, (B → A → B) → B → List A → B :=
+    λ(A : Type) λ(B : Type) λ(f : B → A → B) λ(b : B) λ(l : List A)
+    match (l : List A) with : B {
+        nil _ := b;
+        cons _ (h : A) (hs : List A) := foldl A B f (f b h) hs
+    };
+
+foldl int int (+) 0 (cons int 1 (cons int 2 (cons int 3 (nil int))))
diff --git a/tests/Core/positive/test053.jvc b/tests/Core/positive/test053.jvc
new file mode 100644
index 0000000000..435a5c7ae4
--- /dev/null
+++ b/tests/Core/positive/test053.jvc
@@ -0,0 +1,12 @@
+-- Match with higher-order polymorphic functions
+type Box {
+    mkBox : Π A : Type, A → Box A;
+};
+
+def tt : Π A : Type, (int → A) → Box A → int :=
+    λ(A : Type) λ(f : int → A) λ(l : Box A)
+    match (l : Box A) with : int {
+        mkBox _ _ := f 33
+    };
+
+tt int ((+) 2) (mkBox int 1)
diff --git a/tests/Core/positive/test054.jvc b/tests/Core/positive/test054.jvc
new file mode 100644
index 0000000000..a93cfd856b
--- /dev/null
+++ b/tests/Core/positive/test054.jvc
@@ -0,0 +1,60 @@
+-- typed match
+
+type List {
+  cons : Π A : Type, A -> List A -> List A;
+  nil : Π A : Type, List A;
+};
+
+def lgen : int → List int := \(n : int)
+    if n = 0 then nil int else cons int n (lgen (n - 1));
+
+def sum2 : List int → List int := \(x : List int) {
+  match x : List int with : List int {
+    cons _ x y@(cons _ z _) := cons int (x + z) (sum2 y);
+    _ := x
+  }
+};
+
+def sum : List int → int := \(x : List int) {
+  match x : List int with : int {
+    cons _ x y := x + sum y;
+    _ := 0
+  }
+};
+
+type Tree {
+  leaf : Π A : Type, A -> Tree A;
+  node : Π A : Type, Tree A -> Tree A -> Tree A;
+};
+
+def gen : int → Tree int := \(n : int)
+    if n <= 0 then leaf int 1 else node int (gen (n - 2)) (gen (n - 1));
+
+def g : Π A : Type, Tree A → Tree A := \(A : Type) \(t : Tree A) {
+  match t : Tree A with : Tree A {
+    leaf (A : Type) (x : A) := t;
+    node _ (node _ _ _) r := r;
+    node (A' : Type) (l : Tree A) (r : Tree A') := node A' r l;
+  }
+};
+
+def f : Tree int → int := \(t : Tree int) match t : Tree int with : int {
+  leaf _ (x : int) := x;
+  node _ (l : Tree int) r :=
+    match (g int l : Tree int), (g int r : Tree int) with : int {
+      leaf _ _, leaf _ _ := 0 - 6;
+      node (A : Type) (l : Tree A) (r : Tree int), leaf _ _ := ((f l + f r) * 2) % 20000;
+      node (A : Type) (l1 : Tree A) (r1 : Tree A), node (B : Type) (l2 : Tree A) (r2 : Tree B) := ((f l1 + f r1) * (f l2 + f r2)) % 20000;
+      _, node _ l r := ((f l + f r) * (0 - 3)) % 20000;
+    }
+};
+
+def writeLn := \x write x >> write "\n";
+
+writeLn (sum (sum2 (lgen 5))) >>
+writeLn (f (gen 10)) >>
+writeLn (f (gen 15)) >>
+writeLn (f (gen 16)) >>
+writeLn (f (gen 17)) >>
+writeLn (f (gen 18)) >>
+writeLn (f (gen 20))
diff --git a/tests/Core/positive/test055.jvc b/tests/Core/positive/test055.jvc
new file mode 100644
index 0000000000..d56a38336c
--- /dev/null
+++ b/tests/Core/positive/test055.jvc
@@ -0,0 +1,10 @@
+-- eta-expansion of polymorphic constructors
+
+type Box {
+    box : Π T : Type, Π A : T, A → A → Box A;
+};
+
+def f : Box int → int := \(x : Box int) case x of { box _ _ a b := b - a };
+def g : (int → int → Box int) → Box int := \(f : int → int → Box int) f 2 3;
+
+f (g (box Type int))
diff --git a/tests/Core/positive/test056.jvc b/tests/Core/positive/test056.jvc
new file mode 100644
index 0000000000..1b4e4fa89e
--- /dev/null
+++ b/tests/Core/positive/test056.jvc
@@ -0,0 +1,25 @@
+-- letrec with type annotations
+
+type Box {
+    box : Π A : Type, A → Box A;
+};
+
+def unbox : Π A : Type, Box A → A := \(A : Type) \(b : Box A)
+    case b of {
+        box _ x := x
+    };
+
+def id : Π A : Type, A → A := \(A : Type) \(x : A) x;
+
+def g : Π A : Type, A → A := \(A : Type) \(x : A)
+    letrec[b h]
+        b : Box A := box A x;
+        h : Π A : Type, A → A := id;
+    in
+    h A (unbox A b);
+
+letrec[A f]
+    A : Type := int;
+    f : A → int := \(x : A) x;
+in
+g int (f 4)
diff --git a/tests/Core/positive/test057.jvc b/tests/Core/positive/test057.jvc
new file mode 100644
index 0000000000..9cb66b11a9
--- /dev/null
+++ b/tests/Core/positive/test057.jvc
@@ -0,0 +1,10 @@
+-- type synonyms
+
+def T : Type := Type;
+def I : Type := int;
+
+def id : Π A : T, A → A := \(A : T) \(x : A) x;
+
+def id' : I → I := \(x : I) id I x;
+
+id int 4 + id' 1
diff --git a/tests/Core/positive/test058.jvc b/tests/Core/positive/test058.jvc
new file mode 100644
index 0000000000..436afb04c6
--- /dev/null
+++ b/tests/Core/positive/test058.jvc
@@ -0,0 +1,8 @@
+-- lifting and partial application
+
+def f : (int -> int -> int) -> int := \(h : int -> int -> int) h 1 2;
+def g : int -> int := \(x : int) x;
+
+let h : int -> int -> int := \(x : int) g
+in
+f h + h 2 3
diff --git a/tests/Internal/positive/Inductive.juvix b/tests/Internal/positive/Inductive.juvix
index 401c147ac7..32f57207cd 100644
--- a/tests/Internal/positive/Inductive.juvix
+++ b/tests/Internal/positive/Inductive.juvix
@@ -1,9 +1,11 @@
 module Inductive;
 
+type Unit := unit : Unit;
+
 type A (B : Type) :=
   a : A B;
 
-main : Type -> Type;
-main := A;
+main : Type;
+main := A Unit;
 
 end;
diff --git a/tests/Internal/positive/out/FunctionType.out b/tests/Internal/positive/out/FunctionType.out
index 8fc423b6de..1e3bf3207c 100644
--- a/tests/Internal/positive/out/FunctionType.out
+++ b/tests/Internal/positive/out/FunctionType.out
@@ -1 +1 @@
-Π A : Type 0, Π B : Type 0, A → B
+Π A : Type, Π B : Type, A → B
diff --git a/tests/Internal/positive/out/Inductive.out b/tests/Internal/positive/out/Inductive.out
index f70f10e4db..3439b2d2c0 100644
--- a/tests/Internal/positive/out/Inductive.out
+++ b/tests/Internal/positive/out/Inductive.out
@@ -1 +1 @@
-A
+A (Unit)
diff --git a/tests/Internal/positive/out/Universe.out b/tests/Internal/positive/out/Universe.out
index 3cb0236998..245bc9dcd0 100644
--- a/tests/Internal/positive/out/Universe.out
+++ b/tests/Internal/positive/out/Universe.out
@@ -1 +1 @@
-Type 0
+Type
diff --git a/tests/smoke/Commands/compile.smoke.yaml b/tests/smoke/Commands/compile.smoke.yaml
index bbd577a451..008c42b312 100644
--- a/tests/smoke/Commands/compile.smoke.yaml
+++ b/tests/smoke/Commands/compile.smoke.yaml
@@ -11,17 +11,6 @@ tests:
         JUVIX_FILE
     exit-status: 0
 
-  - name: minic-compilation
-    command:
-      shell:
-        - bash
-      script: |
-        juvix compile positive/MiniC/HelloWorld/Input.juvix -o hello.wasm
-        [ -f hello.wasm ]
-        
-    stdout: ""
-    exit-status: 0
-  
   - name: hello-world
     command:
       shell:
@@ -29,7 +18,7 @@ tests:
       script: |
         cd ./../examples/milestone/HelloWorld
         juvix compile HelloWorld.juvix
-        [ -f HelloWorld ] 
+        [ -f HelloWorld ]
         ./HelloWorld
     exit-status: 0
     stdout: |
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
index f33f811638..a6e0814be8 100644
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@@ -125,7 +125,7 @@ tests:
     stdin: "let x : Nat; x := 2 + 1 in x"
     stdout:
       contains:
-        "suc (suc (suc zero))"
+        "3"
     exit-status: 0
 
   - name: load-builtin-bool
@@ -137,7 +137,7 @@ tests:
     stdin: ":load BuiltinBool.juvix"
     stdout:
       contains:
-        BuiltinBool>
+        "BuiltinBool>"
     exit-status: 0
 
   - name: load-builtin-bool-with-spaces
@@ -197,7 +197,7 @@ tests:
     stdin: "1 + 2"
     stdout:
       contains: |
-        suc (suc (suc zero))
+        3
     exit-status: 0
 
   - name: repl-trace
@@ -209,9 +209,9 @@ tests:
     stdin: trace 2 (printNatLn 3)
     stdout:
       contains: |
-        suc (suc (suc zero))
+        3
     stderr: |
-        suc (suc zero)
+        2
     exit-status: 0
 
   - name: repl-trace-file
@@ -223,12 +223,12 @@ tests:
     stdin: f 4 0
     stdout:
       contains: |
-       zero
+       0
     stderr: |
-       suc (suc (suc (suc zero)))
-       suc (suc (suc zero))
-       suc (suc zero)
-       suc zero
+       4
+       3
+       2
+       1
     exit-status: 0
 
   - name: repl-fail
@@ -245,14 +245,3 @@ tests:
       contains: |
         evaluation error: failure: Enough
     exit-status: 0
-
-  - name: repl-nat-to-int-transform
-    command:
-      - juvix
-      - repl
-      - -t nat-to-int
-    stdin: "1 + 2"
-    stdout:
-      contains: |
-        3
-    exit-status: 0