diff --git a/app/Main.hs b/app/Main.hs
index 020cda3f63..1fe759a53d 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -25,8 +25,8 @@ import Juvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell
 import Juvix.Syntax.MonoJuvix.Pretty qualified as Mono
 import Juvix.Termination qualified as Termination
 import Juvix.Translation.AbstractToMicroJuvix qualified as Micro
+import Juvix.Translation.MicroJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
-import Juvix.Translation.MonoJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
 import Juvix.Translation.ScopedToAbstract qualified as Abstract
 import Juvix.Utils.Version (runDisplayVersion)
diff --git a/juvix-stdlib b/juvix-stdlib
index dd73f5d783..092d6e8465 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit dd73f5d7838041ef9b4c307a385bda415283b280
+Subproject commit 092d6e8465b22c1d35aabfe8c39a4163b04212e1
diff --git a/src/Juvix/Pipeline.hs b/src/Juvix/Pipeline.hs
index 2083e87721..1e1825a828 100644
--- a/src/Juvix/Pipeline.hs
+++ b/src/Juvix/Pipeline.hs
@@ -17,8 +17,8 @@ import Juvix.Syntax.MicroJuvix.MicroJuvixResult qualified as MicroJuvix
 import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroJuvix
 import Juvix.Syntax.MicroJuvix.TypeChecker qualified as MicroJuvix
 import Juvix.Translation.AbstractToMicroJuvix qualified as MicroJuvix
+import Juvix.Translation.MicroJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MicroJuvixToMonoJuvix qualified as MonoJuvix
-import Juvix.Translation.MonoJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
 import Juvix.Translation.ScopedToAbstract qualified as Abstract
 
@@ -95,7 +95,7 @@ upToMiniC ::
   Members '[Files, NameIdGen, Builtins, Error JuvixError] r =>
   EntryPoint ->
   Sem r MiniC.MiniCResult
-upToMiniC = upToMonoJuvix >=> pipelineMiniC
+upToMiniC = upToMicroJuvixTyped >=> pipelineMiniC
 
 --------------------------------------------------------------------------------
 
@@ -149,6 +149,6 @@ pipelineMiniHaskell = MiniHaskell.entryMiniHaskell
 
 pipelineMiniC ::
   Member Builtins r =>
-  MonoJuvix.MonoJuvixResult ->
+  MicroJuvix.MicroJuvixTypedResult ->
   Sem r MiniC.MiniCResult
 pipelineMiniC = MiniC.entryMiniC
diff --git a/src/Juvix/Syntax/MicroJuvix/InfoTable.hs b/src/Juvix/Syntax/MicroJuvix/InfoTable.hs
index 14897e6331..ecc329fbda 100644
--- a/src/Juvix/Syntax/MicroJuvix/InfoTable.hs
+++ b/src/Juvix/Syntax/MicroJuvix/InfoTable.hs
@@ -7,15 +7,17 @@ import Juvix.Syntax.MicroJuvix.Language.Extra
 data ConstructorInfo = ConstructorInfo
   { _constructorInfoInductiveParameters :: [InductiveParameter],
     _constructorInfoArgs :: [Expression],
-    _constructorInfoInductive :: InductiveName
+    _constructorInfoInductive :: InductiveName,
+    _constructorInfoBuiltin :: Maybe BuiltinConstructor
   }
 
 newtype FunctionInfo = FunctionInfo
   { _functionInfoDef :: FunctionDef
   }
 
-newtype AxiomInfo = AxiomInfo
-  { _axiomInfoType :: Expression
+data AxiomInfo = AxiomInfo
+  { _axiomInfoType :: Expression,
+    _axiomInfoBuiltin :: Maybe BuiltinAxiom
   }
 
 newtype InductiveInfo = InductiveInfo
@@ -71,11 +73,13 @@ buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes)
     _infoConstructors :: HashMap Name ConstructorInfo
     _infoConstructors =
       HashMap.fromList
-        [ (c ^. constructorName, ConstructorInfo params args ind)
+        [ (c ^. constructorName, ConstructorInfo params args ind builtin)
           | StatementInductive d <- ss,
             let ind = d ^. inductiveName,
+            let n = length (d ^. inductiveConstructors),
             let params = d ^. inductiveParameters,
-            c <- d ^. inductiveConstructors,
+            let builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin),
+            (builtin, c) <- zipExact builtins (d ^. inductiveConstructors),
             let args = c ^. constructorParameters
         ]
     _infoFunctions :: HashMap Name FunctionInfo
@@ -87,7 +91,7 @@ buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes)
     _infoAxioms :: HashMap Name AxiomInfo
     _infoAxioms =
       HashMap.fromList
-        [ (d ^. axiomName, AxiomInfo (d ^. axiomType))
+        [ (d ^. axiomName, AxiomInfo (d ^. axiomType) (d ^. axiomBuiltin))
           | StatementAxiom d <- ss
         ]
     ss = m ^. (moduleBody . moduleStatements)
diff --git a/src/Juvix/Syntax/MicroJuvix/Language.hs b/src/Juvix/Syntax/MicroJuvix/Language.hs
index f33749baec..2accb5e5e9 100644
--- a/src/Juvix/Syntax/MicroJuvix/Language.hs
+++ b/src/Juvix/Syntax/MicroJuvix/Language.hs
@@ -69,6 +69,14 @@ data Iden
   | IdenInductive Name
   deriving stock (Eq, Generic)
 
+getName :: Iden -> Name
+getName = \case
+  IdenFunction n -> n
+  IdenConstructor n -> n
+  IdenVar n -> n
+  IdenAxiom n -> n
+  IdenInductive n -> n
+
 instance Hashable Iden
 
 data TypedExpression = TypedExpression
diff --git a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs
index af0e2e0ffb..f1743d0ae2 100644
--- a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs
+++ b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs
@@ -112,6 +112,46 @@ mkConcreteType = fmap ConcreteType . go
       e' <- go e
       return (FunctionParameter m i e')
 
+newtype PolyType = PolyType {_unpolyType :: Expression}
+  deriving stock (Eq, Generic)
+
+instance Hashable PolyType
+
+makeLenses ''PolyType
+
+mkPolyType' :: Expression -> PolyType
+mkPolyType' =
+  fromMaybe (error "the given type is not concrete")
+    . mkPolyType
+
+-- mkPolyType removes all named function parameters; currently the assumption in
+-- MicroJuvixToMiniC.hs is that these coincide with type parameters
+mkPolyType :: Expression -> Maybe PolyType
+mkPolyType = fmap PolyType . go
+  where
+    go :: Expression -> Maybe Expression
+    go t = case t of
+      ExpressionApplication (Application l r i) -> do
+        l' <- go l
+        r' <- go r
+        return (ExpressionApplication (Application l' r' i))
+      ExpressionUniverse {} -> return t
+      ExpressionFunction (Function (FunctionParameter m i e) r) ->
+        if isNothing m
+          then do
+            e' <- go e
+            r' <- go r
+            return (ExpressionFunction (Function (FunctionParameter m i e') r'))
+          else go r
+      ExpressionHole {} -> Nothing
+      ExpressionLiteral {} -> return t
+      ExpressionIden i -> case i of
+        IdenFunction {} -> return t
+        IdenInductive {} -> return t
+        IdenConstructor {} -> return t
+        IdenAxiom {} -> return t
+        IdenVar {} -> return t
+
 class HasExpressions a where
   leafExpressions :: Traversal' a Expression
 
diff --git a/src/Juvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs b/src/Juvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs
index c6465ed6e4..799f3ce0db 100644
--- a/src/Juvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs
+++ b/src/Juvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs
@@ -9,10 +9,12 @@ import Juvix.Syntax.MicroJuvix.InfoTable
 import Juvix.Syntax.MicroJuvix.Language
 import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult (MicroJuvixArityResult)
 
+type TypesTable = HashMap Name Expression
+
 data MicroJuvixTypedResult = MicroJuvixTypedResult
   { _resultMicroJuvixArityResult :: MicroJuvixArityResult,
     _resultModules :: NonEmpty Module,
-    _resultIdenTypes :: HashMap Iden Expression
+    _resultIdenTypes :: TypesTable
   }
 
 makeLenses ''MicroJuvixTypedResult
diff --git a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs
index 384fc11e8e..a6440fe8d9 100644
--- a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs
+++ b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs
@@ -16,12 +16,20 @@ import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult
 import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult
 import Juvix.Syntax.MicroJuvix.TypeChecker.Inference
 
+addIdens :: Member (State TypesTable) r => TypesTable -> Sem r ()
+addIdens idens = modify (HashMap.union idens)
+
+registerConstructor :: Members '[State TypesTable, Reader InfoTable] r => InductiveConstructorDef -> Sem r ()
+registerConstructor ctr = do
+  ty <- constructorType (ctr ^. constructorName)
+  modify (HashMap.insert (ctr ^. constructorName) ty)
+
 entryMicroJuvixTyped ::
   Members '[Error TypeCheckerError, NameIdGen] r =>
   MicroJuvixArityResult ->
   Sem r MicroJuvixTypedResult
 entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do
-  (idens, r) <- runState (mempty :: HashMap Iden Expression) (runReader table (mapM checkModule _resultModules))
+  (idens, r) <- runState (mempty :: TypesTable) (runReader table (mapM checkModule _resultModules))
   return
     MicroJuvixTypedResult
       { _resultMicroJuvixArityResult = res,
@@ -33,7 +41,7 @@ entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do
     table = buildTable _resultModules
 
 checkModule ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Module ->
   Sem r Module
 checkModule Module {..} = do
@@ -45,7 +53,7 @@ checkModule Module {..} = do
       }
 
 checkModuleBody ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -56,30 +64,37 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkInclude ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Include ->
   Sem r Include
 checkInclude = traverseOf includeModule checkModule
 
 checkStatement ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Statement ->
   Sem r Statement
 checkStatement s = case s of
   StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
   StatementForeign {} -> return s
-  StatementInductive {} -> return s
+  StatementInductive ind -> do
+    mapM_ registerConstructor (ind ^. inductiveConstructors)
+    ty <- inductiveType (ind ^. inductiveName)
+    modify (HashMap.insert (ind ^. inductiveName) ty)
+    return s
   StatementInclude i -> StatementInclude <$> checkInclude i
-  StatementAxiom {} -> return s
+  StatementAxiom ax -> do
+    modify (HashMap.insert (ax ^. axiomName) (ax ^. axiomType))
+    return s
 
 checkFunctionDef ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
   (funDef, idens) <- runInferenceDef $ do
     info <- lookupFunction _funDefName
     checkFunctionDefType _funDefType
+    registerIden _funDefName _funDefType
     _funDefClauses' <- mapM (checkFunctionClause info) _funDefClauses
     return
       FunctionDef
@@ -89,9 +104,6 @@ checkFunctionDef FunctionDef {..} = do
   addIdens idens
   return funDef
 
-addIdens :: Member (State (HashMap Iden Expression)) r => HashMap Iden Expression -> Sem r ()
-addIdens idens = modify (HashMap.union idens)
-
 checkFunctionDefType :: forall r. Members '[Inference] r => Expression -> Sem r ()
 checkFunctionDefType = traverseOf_ (leafExpressions . _ExpressionHole) go
   where
@@ -172,7 +184,7 @@ checkFunctionClause info FunctionClause {..} = do
               }
 
 checkPatterns ::
-  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, Inference] r =>
   FunctionName ->
   [(FunctionParameter, Pattern)] ->
   Sem r LocalVars
@@ -183,7 +195,7 @@ typeOfArg = (^. paramType)
 
 checkPattern ::
   forall r.
-  Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference] r =>
   FunctionName ->
   FunctionParameter ->
   Pattern ->
@@ -202,6 +214,7 @@ checkPattern funName = go
         PatternBraces {} -> impossible
         PatternVariable v -> do
           modify (addType v ty)
+          registerIden v ty
           case argTy ^. paramName of
             Just v' -> do
               modify (over localTyMap (HashMap.insert v' v))
diff --git a/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs b/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs
index 88103e98a2..b4cbaeff77 100644
--- a/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs
+++ b/src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs
@@ -4,6 +4,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Prelude hiding (fromEither)
 import Juvix.Syntax.MicroJuvix.Error
 import Juvix.Syntax.MicroJuvix.Language.Extra
+import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult
 
 data MetavarState
   = Fresh
@@ -14,13 +15,13 @@ data Inference m a where
   FreshMetavar :: Hole -> Inference m TypedExpression
   MatchTypes :: Expression -> Expression -> Inference m Bool
   QueryMetavar :: Hole -> Inference m (Maybe Expression)
-  RegisterIden :: Iden -> Expression -> Inference m ()
+  RegisterIden :: Name -> Expression -> Inference m ()
 
 makeSem ''Inference
 
 data InferenceState = InferenceState
   { _inferenceMap :: HashMap Hole MetavarState,
-    _inferenceIdens :: HashMap Iden Expression
+    _inferenceIdens :: TypesTable
   }
 
 makeLenses ''InferenceState
@@ -28,8 +29,14 @@ makeLenses ''InferenceState
 iniState :: InferenceState
 iniState = InferenceState mempty mempty
 
-closeState :: Member (Error TypeCheckerError) r => InferenceState -> Sem r (HashMap Hole Expression,
-                                                                             HashMap Iden Expression)
+closeState ::
+  Member (Error TypeCheckerError) r =>
+  InferenceState ->
+  Sem
+    r
+    ( HashMap Hole Expression,
+      TypesTable
+    )
 closeState = \case
   InferenceState m idens -> do
     holeMap <- execState mempty (f m)
@@ -73,7 +80,7 @@ re = reinterpret $ \case
   QueryMetavar h -> queryMetavar' h
   RegisterIden i ty -> registerIden' i ty
   where
-    registerIden' :: Members '[State InferenceState] r => Iden -> Expression -> Sem r ()
+    registerIden' :: Members '[State InferenceState] r => Name -> Expression -> Sem r ()
     registerIden' i ty = modify (over inferenceIdens (HashMap.insert i ty))
 
     queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Expression)
@@ -163,8 +170,10 @@ re = reinterpret $ \case
                     andM [go l1 l2, local' (go r1 r2)]
                 | otherwise = return False
 
-runInferenceDef :: Member (Error TypeCheckerError) r => Sem (Inference ': r) FunctionDef
-   -> Sem r (FunctionDef, HashMap Iden Expression)
+runInferenceDef ::
+  Member (Error TypeCheckerError) r =>
+  Sem (Inference ': r) FunctionDef ->
+  Sem r (FunctionDef, TypesTable)
 runInferenceDef a = do
   ((subs, idens), expr) <- runState iniState (re a) >>= firstM closeState
   return (fillHolesFunctionDef subs expr, fillHoles subs <$> idens)
diff --git a/src/Juvix/Translation/MonoJuvixToMiniC.hs b/src/Juvix/Translation/MicroJuvixToMiniC.hs
similarity index 62%
rename from src/Juvix/Translation/MonoJuvixToMiniC.hs
rename to src/Juvix/Translation/MicroJuvixToMiniC.hs
index de9b9da222..59fb51388c 100644
--- a/src/Juvix/Translation/MonoJuvixToMiniC.hs
+++ b/src/Juvix/Translation/MicroJuvixToMiniC.hs
@@ -1,6 +1,6 @@
-module Juvix.Translation.MonoJuvixToMiniC
-  ( module Juvix.Translation.MonoJuvixToMiniC,
-    module Juvix.Translation.MonoJuvixToMiniC.Types,
+module Juvix.Translation.MicroJuvixToMiniC
+  ( module Juvix.Translation.MicroJuvixToMiniC,
+    module Juvix.Translation.MicroJuvixToMiniC.Types,
   )
 where
 
@@ -8,25 +8,49 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Builtins
 import Juvix.Internal.Strings qualified as Str
 import Juvix.Prelude
+import Juvix.Syntax.Abstract.AbstractResult qualified as Abstract
 import Juvix.Syntax.Backends
 import Juvix.Syntax.Concrete.Language qualified as C
-import Juvix.Syntax.Concrete.Scoped.InfoTable qualified as S
+import Juvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoper
+import Juvix.Syntax.Concrete.Scoped.Name qualified as Scoper
+import Juvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
 import Juvix.Syntax.ForeignBlock
+import Juvix.Syntax.MicroJuvix.Language.Extra (mkPolyType')
+import Juvix.Syntax.MicroJuvix.Language.Extra qualified as Micro
+import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as Micro1
+import Juvix.Syntax.MicroJuvix.MicroJuvixResult qualified as Micro2
+import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
 import Juvix.Syntax.MiniC.Language
 import Juvix.Syntax.MiniC.Serialization
-import Juvix.Syntax.MonoJuvix.Language qualified as Mono
 import Juvix.Syntax.NameId
-import Juvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
-import Juvix.Translation.MonoJuvixToMiniC.Base
-import Juvix.Translation.MonoJuvixToMiniC.BuiltinTable
-import Juvix.Translation.MonoJuvixToMiniC.Closure
-import Juvix.Translation.MonoJuvixToMiniC.Types
+import Juvix.Translation.MicroJuvixToMiniC.Base
+import Juvix.Translation.MicroJuvixToMiniC.BuiltinTable
+import Juvix.Translation.MicroJuvixToMiniC.Closure
+import Juvix.Translation.MicroJuvixToMiniC.Types
+
+type CompileInfoTable = HashMap Scoper.NameId Scoper.CompileInfo
+
+compileInfoTable :: Micro.MicroJuvixTypedResult -> CompileInfoTable
+compileInfoTable r =
+  HashMap.mapKeys
+    (^. Scoper.nameId)
+    ( r
+        ^. Micro.resultMicroJuvixArityResult
+        . Micro1.resultMicroJuvixResult
+        . Micro2.resultAbstract
+        . Abstract.resultScoper
+        . Scoper.resultScoperTable
+        . Scoper.infoCompilationRules
+    )
 
-entryMiniC :: forall r. Member Builtins r => Mono.MonoJuvixResult -> Sem r MiniCResult
+entryMiniC :: forall r. Member Builtins r => Micro.MicroJuvixTypedResult -> Sem r MiniCResult
 entryMiniC i = MiniCResult . serialize <$> cunitResult
   where
-    compileInfo :: Mono.CompileInfoTable
-    compileInfo = Mono.compileInfoTable i
+    compileInfo :: CompileInfoTable
+    compileInfo = compileInfoTable i
+
+    typesTable :: Micro.TypesTable
+    typesTable = i ^. Micro.resultIdenTypes
 
     cunitResult :: Sem r CCodeUnit
     cunitResult = do
@@ -44,85 +68,90 @@ entryMiniC i = MiniCResult . serialize <$> cunitResult
           CppIncludeFile Str.minicRuntime
         ]
 
-    cmodule :: Mono.Module -> Sem r [CCode]
+    cmodule :: Micro.Module -> Sem r [CCode]
     cmodule m = do
-      let buildTable = Mono.buildTable m
+      let buildTable = Micro.buildTable [m]
       let defs =
             genStructDefs m
               <> run (runReader compileInfo (genAxioms m))
               <> run (runReader buildTable (genCTypes m))
-              <> run (runReader buildTable (genFunctionSigs m))
-              <> run (runReader buildTable (genClosures m))
-      funDefs <- runReader buildTable (genFunctionDefs m)
+              <> run (runReader buildTable (runReader typesTable (genFunctionSigs m)))
+              <> run (runReader buildTable (runReader typesTable (genClosures m)))
+      funDefs <- runReader buildTable (runReader typesTable (genFunctionDefs m))
       return (defs <> funDefs)
 
     cmodules :: Sem r [CCode]
-    cmodules = concatMapM cmodule (toList (i ^. Mono.resultModules))
+    cmodules = concatMapM cmodule (toList (i ^. Micro.resultModules))
 
-genStructDefs :: Mono.Module -> [CCode]
-genStructDefs Mono.Module {..} =
-  concatMap go (_moduleBody ^. Mono.moduleStatements)
+genStructDefs :: Micro.Module -> [CCode]
+genStructDefs Micro.Module {..} =
+  concatMap go (_moduleBody ^. Micro.moduleStatements)
   where
-    go :: Mono.Statement -> [CCode]
+    go :: Micro.Statement -> [CCode]
     go = \case
-      Mono.StatementInductive d -> mkInductiveTypeDef d
+      Micro.StatementInductive d -> mkInductiveTypeDef d
+      Micro.StatementInclude i ->
+        concatMap go (i ^. Micro.includeModule . Micro.moduleBody . Micro.moduleStatements)
       _ -> []
 
-genAxioms :: forall r. Members '[Reader Mono.CompileInfoTable] r => Mono.Module -> Sem r [CCode]
-genAxioms Mono.Module {..} =
-  concatMapM go (_moduleBody ^. Mono.moduleStatements)
+genAxioms :: forall r. Members '[Reader CompileInfoTable] r => Micro.Module -> Sem r [CCode]
+genAxioms Micro.Module {..} =
+  concatMapM go (_moduleBody ^. Micro.moduleStatements)
   where
-    go :: Mono.Statement -> Sem r [CCode]
+    go :: Micro.Statement -> Sem r [CCode]
     go = \case
-      Mono.StatementInductive {} -> return []
-      Mono.StatementAxiom d -> goAxiom d
-      Mono.StatementForeign {} -> return []
-      Mono.StatementFunction {} -> return []
-
-genCTypes :: forall r. Member (Reader Mono.InfoTable) r => Mono.Module -> Sem r [CCode]
-genCTypes Mono.Module {..} =
-  concatMapM go (_moduleBody ^. Mono.moduleStatements)
+      Micro.StatementInductive {} -> return []
+      Micro.StatementAxiom d -> goAxiom d
+      Micro.StatementForeign {} -> return []
+      Micro.StatementFunction {} -> return []
+      Micro.StatementInclude i ->
+        concatMapM go (i ^. Micro.includeModule . Micro.moduleBody . Micro.moduleStatements)
+
+genCTypes :: forall r. Member (Reader Micro.InfoTable) r => Micro.Module -> Sem r [CCode]
+genCTypes Micro.Module {..} =
+  concatMapM go (_moduleBody ^. Micro.moduleStatements)
   where
-    go :: Mono.Statement -> Sem r [CCode]
+    go :: Micro.Statement -> Sem r [CCode]
     go = \case
-      Mono.StatementInductive d -> goInductiveDef d
-      Mono.StatementAxiom {} -> return []
-      Mono.StatementForeign d -> return (goForeign d)
-      Mono.StatementFunction {} -> return []
+      Micro.StatementInductive d -> goInductiveDef d
+      Micro.StatementAxiom {} -> return []
+      Micro.StatementForeign d -> return (goForeign d)
+      Micro.StatementFunction {} -> return []
+      Micro.StatementInclude i ->
+        concatMapM go (i ^. Micro.includeModule . Micro.moduleBody . Micro.moduleStatements)
 
-genFunctionSigs :: forall r. Member (Reader Mono.InfoTable) r => Mono.Module -> Sem r [CCode]
-genFunctionSigs Mono.Module {..} =
-  concatMapM (applyOnFunStatement genFunctionSig) (_moduleBody ^. Mono.moduleStatements)
+genFunctionSigs :: forall r. Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r => Micro.Module -> Sem r [CCode]
+genFunctionSigs Micro.Module {..} =
+  concatMapM (applyOnFunStatement genFunctionSig) (_moduleBody ^. Micro.moduleStatements)
 
 genFunctionDefs ::
-  Members '[Reader Mono.InfoTable, Builtins] r =>
-  Mono.Module ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Builtins] r =>
+  Micro.Module ->
   Sem r [CCode]
-genFunctionDefs Mono.Module {..} = genFunctionDefsBody _moduleBody
+genFunctionDefs Micro.Module {..} = genFunctionDefsBody _moduleBody
 
 genFunctionDefsBody ::
-  Members '[Reader Mono.InfoTable, Builtins] r =>
-  Mono.ModuleBody ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Builtins] r =>
+  Micro.ModuleBody ->
   Sem r [CCode]
-genFunctionDefsBody Mono.ModuleBody {..} =
+genFunctionDefsBody Micro.ModuleBody {..} =
   concatMapM (applyOnFunStatement goFunctionDef) _moduleStatements
 
 isNullary :: Text -> CFunType -> Bool
 isNullary funName funType = null (funType ^. cFunArgTypes) && funName /= Str.main_
 
-mkFunctionSig :: forall r. Member (Reader Mono.InfoTable) r => Mono.FunctionDef -> Sem r FunctionSig
-mkFunctionSig Mono.FunctionDef {..} =
+mkFunctionSig :: forall r. Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r => Micro.FunctionDef -> Sem r FunctionSig
+mkFunctionSig Micro.FunctionDef {..} =
   cFunTypeToFunSig <$> funName <*> funType
   where
-    -- Assumption: All clauses have the same number of patterns
-    nPatterns :: Int
-    nPatterns = length (head _funDefClauses ^. Mono.clausePatterns)
-
     baseFunType :: Sem r CFunType
-    baseFunType = typeToFunType _funDefType
+    baseFunType = typeToFunType (mkPolyType' _funDefType)
 
     funType :: Sem r CFunType
     funType = do
+      -- Assumption: All clauses have the same number of patterns
+      pats <- getClausePatterns (head _funDefClauses)
+      let nPatterns = length pats
       typ <- baseFunType
       return
         ( if nPatterns == length (typ ^. cFunArgTypes)
@@ -143,8 +172,8 @@ mkFunctionSig Mono.FunctionDef {..} =
     funName :: Sem r Text
     funName = bool funcBasename (asNullary funcBasename) <$> funIsNullary
 
-genFunctionSig :: forall r. Member (Reader Mono.InfoTable) r => Mono.FunctionDef -> Sem r [CCode]
-genFunctionSig d@(Mono.FunctionDef {..}) = do
+genFunctionSig :: forall r. Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r => Micro.FunctionDef -> Sem r [CCode]
+genFunctionSig d@(Micro.FunctionDef {..}) = do
   sig <- mkFunctionSig d
   nullaryDefine' <- nullaryDefine
   return
@@ -152,14 +181,13 @@ genFunctionSig d@(Mono.FunctionDef {..}) = do
         <> (ExternalMacro . CppDefineParens <$> toList nullaryDefine')
     )
   where
-    nPatterns :: Int
-    nPatterns = length (head _funDefClauses ^. Mono.clausePatterns)
-
     baseFunType :: Sem r CFunType
-    baseFunType = typeToFunType _funDefType
+    baseFunType = typeToFunType (mkPolyType' _funDefType)
 
     funType :: Sem r CFunType
     funType = do
+      pats <- getClausePatterns (head _funDefClauses)
+      let nPatterns = length pats
       typ <- baseFunType
       return
         ( if nPatterns == length (typ ^. cFunArgTypes)
@@ -194,16 +222,16 @@ genFunctionSig d@(Mono.FunctionDef {..}) = do
         <$> funIsNullary
 
 goFunctionDef ::
-  Members '[Reader Mono.InfoTable, Builtins] r =>
-  Mono.FunctionDef ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Builtins] r =>
+  Micro.FunctionDef ->
   Sem r [CCode]
-goFunctionDef d@(Mono.FunctionDef {..})
+goFunctionDef d@(Micro.FunctionDef {..})
   | isJust _funDefBuiltin = return []
   | otherwise = do
-      fc <- mapM (goFunctionClause (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
+      funSig <- mkFunctionSig d
+      fc <- mapM (goFunctionClause funSig (fst (unfoldFunType (mkPolyType' _funDefType)))) (toList _funDefClauses)
       let bodySpec = fst <$> fc
       let preDecls :: [Function] = snd =<< fc
-      funSig <- mkFunctionSig d
       return $
         (ExternalFunc <$> preDecls)
           <> [ ExternalFunc $
@@ -242,7 +270,7 @@ goFunctionDef d@(Mono.FunctionDef {..})
                     ( LiteralString
                         ( "Error: Pattern match(es) are non-exhaustive in "
                             <> _funDefName
-                            ^. Mono.nameText
+                            ^. Micro.nameText
                         )
                     )
                 ]
@@ -257,37 +285,41 @@ goFunctionDef d@(Mono.FunctionDef {..})
 
 goFunctionClause ::
   forall r.
-  Members '[Reader Mono.InfoTable, Builtins] r =>
-  [Mono.Type] ->
-  Mono.FunctionClause ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Builtins] r =>
+  FunctionSig ->
+  [Micro.PolyType] ->
+  Micro.FunctionClause ->
   Sem r ((Maybe Expression, Statement), [Function])
-goFunctionClause argTyps clause = do
+goFunctionClause funSig argTyps clause = do
   (stmt, decls) <- returnStmt
   cond <- clauseCondition
   return ((cond, stmt), decls)
   where
     conditions :: Sem r [Expression]
-    conditions =
+    conditions = do
+      pats <- getClausePatterns clause
       concat
         <$> sequence
           [ patternCondition (ExpressionVar arg) p
-            | (p, arg) <- zip (clause ^. Mono.clausePatterns) funArgs
+            | (p, arg) <- zip pats funArgs
           ]
 
-    patternCondition :: Expression -> Mono.Pattern -> Sem r [Expression]
+    patternCondition :: Expression -> Micro.Pattern -> Sem r [Expression]
     patternCondition arg = \case
-      Mono.PatternConstructorApp Mono.ConstructorApp {..} -> do
+      Micro.PatternConstructorApp Micro.ConstructorApp {..} -> do
         ctorName <- getConstructorCName _constrAppConstructor
+        ty <- typeOfConstructor _constrAppConstructor
 
         let isCtor :: Expression
-            isCtor = functionCall (ExpressionVar (asIs ctorName)) [arg]
+            isCtor = functionCall (ExpressionVar (asIs ctorName)) [castToType ty arg]
             projCtor :: Text -> Expression
-            projCtor ctorArg = functionCall (ExpressionVar (asProjName ctorArg ctorName)) [arg]
+            projCtor ctorArg = functionCall (ExpressionVar (asProjName ctorArg ctorName)) [castToType ty arg]
             subConditions :: Sem r [Expression]
             subConditions = fmap concat (zipWithM patternCondition (map projCtor ctorArgs) _constrAppParameters)
         fmap (isCtor :) subConditions
-      Mono.PatternVariable {} -> return []
-      Mono.PatternWildcard {} -> return []
+      Micro.PatternVariable {} -> return []
+      Micro.PatternWildcard {} -> return []
+      Micro.PatternBraces b -> patternCondition arg b
 
     clauseCondition :: Sem r (Maybe Expression)
     clauseCondition = fmap (foldr1 f) . nonEmpty <$> conditions
@@ -304,113 +336,114 @@ goFunctionClause argTyps clause = do
     returnStmt :: Sem r (Statement, [Function])
     returnStmt = do
       bindings <- buildPatternInfoTable argTyps clause
-      (decls :: [Function], clauseResult) <- runOutputList (runReader bindings (goExpression (clause ^. Mono.clauseBody)))
-      return (StatementReturn (Just clauseResult), decls)
+      (decls :: [Function], clauseResult) <- runOutputList (runReader bindings (goExpression (clause ^. Micro.clauseBody)))
+      return (StatementReturn (Just (castClause clauseResult)), decls)
+      where
+        castClause clauseResult =
+          castToType (CDeclType {_typeDeclType = funSig ^. funcReturnType, _typeIsPtr = funSig ^. funcIsPtr}) clauseResult
 
-goExpression :: Members '[Reader Mono.InfoTable, Builtins, Reader PatternInfoTable] r => Mono.Expression -> Sem r Expression
+goExpression :: Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Builtins, Reader PatternInfoTable] r => Micro.Expression -> Sem r Expression
 goExpression = \case
-  Mono.ExpressionIden i -> do
-    let rootFunMonoName = Mono.getName i
-        rootFunName = mkName rootFunMonoName
+  Micro.ExpressionIden i -> do
+    let rootFunMicroName = Micro.getName i
+        rootFunName = mkName rootFunMicroName
         evalFunName = asEval (rootFunName <> "_0")
     case i of
-      Mono.IdenVar {} -> goIden i
+      Micro.IdenVar {} -> goIden i
       _ -> do
         (t, _) <- getType i
         let argTyps = t ^. cFunArgTypes
         (if null argTyps then goIden i else return $ functionCall (ExpressionVar evalFunName) [])
-  Mono.ExpressionApplication a -> goApplication a
-  Mono.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l))
+  Micro.ExpressionApplication a -> goApplication a
+  Micro.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l))
+  Micro.ExpressionFunction {} -> impossible
+  Micro.ExpressionHole {} -> impossible
+  Micro.ExpressionUniverse {} -> impossible
 
-goIden :: Members '[Reader PatternInfoTable, Builtins, Reader Mono.InfoTable] r => Mono.Iden -> Sem r Expression
+goIden :: Members '[Reader PatternInfoTable, Builtins, Reader Micro.InfoTable] r => Micro.Iden -> Sem r Expression
 goIden = \case
-  Mono.IdenFunction n -> do
-    funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
-    let varName = case funInfo ^. Mono.functionInfoBuiltin of
+  Micro.IdenFunction n -> do
+    funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoFunctions)
+    let varName = case funInfo ^. Micro.functionInfoDef . Micro.funDefBuiltin of
           Just builtin -> fromJust (builtinFunctionName builtin)
           Nothing -> mkName n
     return (ExpressionVar varName)
-  Mono.IdenConstructor n -> ExpressionVar <$> getConstructorCName n
-  Mono.IdenVar n ->
-    (^. bindingInfoExpr) . HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
-  Mono.IdenAxiom n -> ExpressionVar <$> getAxiomCName n
+  Micro.IdenConstructor n -> ExpressionVar <$> getConstructorCName n
+  Micro.IdenVar n ->
+    (^. bindingInfoExpr) . HashMap.lookupDefault impossible (n ^. Micro.nameText) <$> asks (^. patternBindings)
+  Micro.IdenAxiom n -> ExpressionVar <$> getAxiomCName n
+  Micro.IdenInductive {} -> impossible
 
-goApplication :: forall r. Members '[Reader PatternInfoTable, Builtins, Reader Mono.InfoTable] r => Mono.Application -> Sem r Expression
+goApplication :: forall r. Members '[Reader PatternInfoTable, Reader Micro.TypesTable, Builtins, Reader Micro.InfoTable] r => Micro.Application -> Sem r Expression
 goApplication a = do
-  (iden, fArgs) <- f
-
-  case iden of
-    Mono.IdenVar n -> do
-      BindingInfo {..} <- HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
-      return $ juvixFunctionCall _bindingInfoType _bindingInfoExpr (reverse fArgs)
-    Mono.IdenFunction n -> do
-      nPatterns <- (^. Mono.functionInfoPatterns) . HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
-      (idenType, _) <- getType iden
-      let nArgTyps = length (idenType ^. cFunArgTypes)
-      if
-          | length fArgs < nArgTyps -> do
-              let name = mkName (Mono.getName iden)
-                  evalName = asEval (name <> "_" <> show (length fArgs))
-              return $ functionCall (ExpressionVar evalName) (reverse fArgs)
-          | nPatterns < nArgTyps -> do
-              idenExp <- goIden iden
-              let callTyp = idenType {_cFunArgTypes = drop nPatterns (idenType ^. cFunArgTypes)}
-                  args = reverse fArgs
-                  patternArgs = take nPatterns args
-                  funCall =
-                    (if null patternArgs then idenExp else functionCall idenExp patternArgs)
-              return $ juvixFunctionCall callTyp funCall (drop nPatterns args)
-          | otherwise -> do
-              idenExp <- goIden iden
-              return $ functionCall idenExp (reverse fArgs)
-    Mono.IdenConstructor n -> returnFunCall iden fArgs n
-    Mono.IdenAxiom n -> returnFunCall iden fArgs n
+  tab <- ask
+  let (f, args0) = unfoldPolyApp tab a
+  if null args0
+    then goExpression f
+    else case f of
+      Micro.ExpressionLiteral {} -> goExpression f
+      Micro.ExpressionIden iden -> do
+        fArgs <- toList <$> mapM goExpression args0
+        case iden of
+          Micro.IdenVar n -> do
+            BindingInfo {..} <- HashMap.lookupDefault impossible (n ^. Micro.nameText) <$> asks (^. patternBindings)
+            return $ juvixFunctionCall _bindingInfoType _bindingInfoExpr fArgs
+          Micro.IdenFunction n -> do
+            info <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoFunctions)
+            nPatterns <- functionInfoPatternsNum info
+            (idenType, _) <- getType iden
+            let nArgTyps = length (idenType ^. cFunArgTypes)
+            if
+                | length fArgs < nArgTyps -> do
+                    let name = mkName (Micro.getName iden)
+                        evalName = asEval (name <> "_" <> show (length fArgs))
+                    return $ functionCallCasted idenType (ExpressionVar evalName) fArgs
+                | nPatterns < nArgTyps -> do
+                    idenExp <- goIden iden
+                    let callTyp = idenType {_cFunArgTypes = drop nPatterns (idenType ^. cFunArgTypes)}
+                        patternArgs = take nPatterns fArgs
+                        funCall =
+                          (if null patternArgs then idenExp else functionCallCasted idenType idenExp patternArgs)
+                    return $ juvixFunctionCall callTyp funCall (drop nPatterns fArgs)
+                | otherwise -> do
+                    idenExp <- goIden iden
+                    return $ functionCallCasted idenType idenExp fArgs
+          Micro.IdenConstructor n -> returnFunCall iden fArgs n
+          Micro.IdenAxiom n -> returnFunCall iden fArgs n
+          Micro.IdenInductive {} -> impossible
+      _ -> impossible
   where
-    f :: Sem r (Mono.Iden, [Expression])
-    f = unfoldApp a
-
-    returnFunCall :: Mono.Iden -> [Expression] -> Mono.Name -> Sem r Expression
+    returnFunCall :: Micro.Iden -> [Expression] -> Micro.Name -> Sem r Expression
     returnFunCall iden fArgs name = do
       (idenType, _) <- getType iden
       ( if length fArgs < length (idenType ^. cFunArgTypes)
           then
             ( do
                 let evalName = asEval (mkName name <> "_" <> show (length fArgs))
-                return $ functionCall (ExpressionVar evalName) (reverse fArgs)
+                return $ functionCallCasted idenType (ExpressionVar evalName) fArgs
             )
           else
             ( do
                 idenExp <- goIden iden
-                return $ functionCall idenExp (reverse fArgs)
+                return $ functionCallCasted idenType idenExp fArgs
             )
         )
 
-    unfoldApp :: Mono.Application -> Sem r (Mono.Iden, [Expression])
-    unfoldApp Mono.Application {..} = case _appLeft of
-      Mono.ExpressionApplication x -> do
-        fName <- goExpression _appRight
-        uf <- unfoldApp x
-        return (second (fName :) uf)
-      Mono.ExpressionIden i -> do
-        fArg <- goExpression _appRight
-        return (i, [fArg])
-      Mono.ExpressionLiteral {} -> impossible
-
 goLiteral :: C.LiteralLoc -> Literal
 goLiteral l = case l ^. C.withLocParam of
   C.LitString s -> LiteralString s
   C.LitInteger i -> LiteralInt i
 
 goAxiom ::
-  Member (Reader Mono.CompileInfoTable) r =>
-  Mono.AxiomDef ->
+  Member (Reader CompileInfoTable) r =>
+  Micro.AxiomDef ->
   Sem r [CCode]
 goAxiom a
-  | isJust (a ^. Mono.axiomBuiltin) = return []
+  | isJust (a ^. Micro.axiomBuiltin) = return []
   | otherwise = do
-      backends <- lookupBackends (axiomName ^. Mono.nameId)
+      backends <- lookupBackends (axiomName ^. Micro.nameId)
       case firstJust getCode backends of
-        Nothing -> error ("C backend does not support this axiom:" <> show (axiomName ^. Mono.nameText))
+        Nothing -> error ("C backend does not support this axiom:" <> show (axiomName ^. Micro.nameText))
         Just defineBody ->
           return
             [ ExternalMacro
@@ -423,8 +456,8 @@ goAxiom a
                 )
             ]
   where
-    axiomName :: Mono.Name
-    axiomName = a ^. Mono.axiomName
+    axiomName :: Micro.Name
+    axiomName = a ^. Micro.axiomName
     defineName :: Text
     defineName = mkName axiomName
     getCode :: BackendItem -> Maybe Text
@@ -433,23 +466,23 @@ goAxiom a
         $> b
         ^. backendItemCode
     lookupBackends ::
-      Member (Reader Mono.CompileInfoTable) r =>
+      Member (Reader CompileInfoTable) r =>
       NameId ->
       Sem r [BackendItem]
-    lookupBackends f = (^. S.compileInfoBackendItems) . HashMap.lookupDefault (error (show (a ^. Mono.axiomName))) f <$> ask
+    lookupBackends f = (^. Scoper.compileInfoBackendItems) . HashMap.lookupDefault impossible f <$> ask
 
 goForeign :: ForeignBlock -> [CCode]
 goForeign b = case b ^. foreignBackend of
   BackendC -> [Verbatim (b ^. foreignCode)]
   _ -> []
 
-mkInductiveName :: Mono.InductiveDef -> Text
-mkInductiveName i = mkName (i ^. Mono.inductiveName)
+mkInductiveName :: Micro.InductiveDef -> Text
+mkInductiveName i = mkName (i ^. Micro.inductiveName)
 
-mkInductiveConstructorNames :: Mono.InductiveDef -> [Text]
-mkInductiveConstructorNames i = mkName . view Mono.constructorName <$> i ^. Mono.inductiveConstructors
+mkInductiveConstructorNames :: Micro.InductiveDef -> [Text]
+mkInductiveConstructorNames i = mkName . view Micro.constructorName <$> i ^. Micro.inductiveConstructors
 
-mkInductiveTypeDef :: Mono.InductiveDef -> [CCode]
+mkInductiveTypeDef :: Micro.InductiveDef -> [CCode]
 mkInductiveTypeDef i =
   [ExternalDecl structTypeDef]
   where
@@ -467,15 +500,15 @@ mkInductiveTypeDef i =
         )
 
     baseName :: Text
-    baseName = mkName (i ^. Mono.inductiveName)
+    baseName = mkName (i ^. Micro.inductiveName)
 
-goInductiveDef :: Members '[Reader Mono.InfoTable] r => Mono.InductiveDef -> Sem r [CCode]
+goInductiveDef :: Members '[Reader Micro.InfoTable] r => Micro.InductiveDef -> Sem r [CCode]
 goInductiveDef i
-  | isJust (i ^. Mono.inductiveBuiltin) = return []
+  | isJust (i ^. Micro.inductiveBuiltin) = return []
   | otherwise = do
-      ctorDefs <- concatMapM goInductiveConstructorDef (i ^. Mono.inductiveConstructors)
-      ctorNews <- concatMapM (goInductiveConstructorNew i) (i ^. Mono.inductiveConstructors)
-      projections <- concatMapM (goProjections inductiveTypeDef) (i ^. Mono.inductiveConstructors)
+      ctorDefs <- concatMapM goInductiveConstructorDef (i ^. Micro.inductiveConstructors)
+      ctorNews <- concatMapM (goInductiveConstructorNew i) (i ^. Micro.inductiveConstructors)
+      projections <- concatMapM (goProjections inductiveTypeDef) (i ^. Micro.inductiveConstructors)
       return
         ( [ExternalDecl tagsType]
             <> ctorDefs
@@ -487,7 +520,7 @@ goInductiveDef i
         )
   where
     baseName :: Text
-    baseName = mkName (i ^. Mono.inductiveName)
+    baseName = mkName (i ^. Micro.inductiveName)
 
     constructorNames :: [Text]
     constructorNames = mkInductiveConstructorNames i
@@ -590,9 +623,9 @@ goInductiveDef i
 
 goInductiveConstructorNew ::
   forall r.
-  Members '[Reader Mono.InfoTable] r =>
-  Mono.InductiveDef ->
-  Mono.InductiveConstructorDef ->
+  Members '[Reader Micro.InfoTable] r =>
+  Micro.InductiveDef ->
+  Micro.InductiveConstructorDef ->
   Sem r [CCode]
 goInductiveConstructorNew i ctor = ctorNewFun
   where
@@ -600,13 +633,13 @@ goInductiveConstructorNew i ctor = ctorNewFun
     ctorNewFun = if null ctorParams then return ctorNewNullary else ctorNewNary
 
     baseName :: Text
-    baseName = mkName (ctor ^. Mono.constructorName)
+    baseName = mkName (ctor ^. Micro.constructorName)
 
     inductiveName :: Text
     inductiveName = mkInductiveName i
 
-    ctorParams :: [Mono.Type]
-    ctorParams = ctor ^. Mono.constructorParameters
+    ctorParams :: [Micro.PolyType]
+    ctorParams = map mkPolyType' (ctor ^. Micro.constructorParameters)
 
     ctorNewNullary :: [CCode]
     ctorNewNullary =
@@ -752,16 +785,21 @@ goInductiveConstructorNew i ctor = ctorNewFun
             )
         )
 
-inductiveCtorParams :: Members '[Reader Mono.InfoTable] r => Mono.InductiveConstructorDef -> Sem r [CDeclType]
-inductiveCtorParams ctor = mapM goType (ctor ^. Mono.constructorParameters)
+inductiveCtorParams :: Members '[Reader Micro.InfoTable] r => Micro.InductiveConstructorDef -> Sem r [CDeclType]
+inductiveCtorParams ctor = mapM (goType . mkPolyType') (ctor ^. Micro.constructorParameters)
 
-inductiveCtorArgs :: Members '[Reader Mono.InfoTable] r => Mono.InductiveConstructorDef -> Sem r [Declaration]
+inductiveCtorArgs :: Members '[Reader Micro.InfoTable] r => Micro.InductiveConstructorDef -> Sem r [Declaration]
 inductiveCtorArgs ctor = namedArgs asCtorArg <$> inductiveCtorParams ctor
 
+inductiveCtorTypes :: Members '[Reader Micro.InfoTable] r => Micro.Name -> Sem r [CDeclType]
+inductiveCtorTypes ctor = do
+  info <- Micro.lookupConstructor ctor
+  mapM (goType . mkPolyType') (snd (Micro.constructorArgTypes info))
+
 goInductiveConstructorDef ::
   forall r.
-  Members '[Reader Mono.InfoTable] r =>
-  Mono.InductiveConstructorDef ->
+  Members '[Reader Micro.InfoTable] r =>
+  Micro.InductiveConstructorDef ->
   Sem r [CCode]
 goInductiveConstructorDef ctor = do
   d <- ctorDecl
@@ -771,10 +809,10 @@ goInductiveConstructorDef ctor = do
     ctorDecl = if null ctorParams then return ctorBool else ctorStruct
 
     baseName :: Text
-    baseName = mkName (ctor ^. Mono.constructorName)
+    baseName = mkName (ctor ^. Micro.constructorName)
 
-    ctorParams :: [Mono.Type]
-    ctorParams = ctor ^. Mono.constructorParameters
+    ctorParams :: [Micro.PolyType]
+    ctorParams = map mkPolyType' (ctor ^. Micro.constructorParameters)
 
     ctorBool :: Declaration
     ctorBool = typeDefWrap (asTypeDef baseName) BoolType
@@ -796,16 +834,16 @@ goInductiveConstructorDef ctor = do
         )
 
 goProjections ::
-  Members '[Reader Mono.InfoTable] r =>
+  Members '[Reader Micro.InfoTable] r =>
   DeclType ->
-  Mono.InductiveConstructorDef ->
+  Micro.InductiveConstructorDef ->
   Sem r [CCode]
 goProjections inductiveTypeDef ctor = do
   params <- inductiveCtorParams ctor
   return (ExternalFunc <$> zipWith projFunction [0 ..] params)
   where
     baseName :: Text
-    baseName = mkName (ctor ^. Mono.constructorName)
+    baseName = mkName (ctor ^. Micro.constructorName)
 
     localName :: Text
     localName = "a"
diff --git a/src/Juvix/Translation/MicroJuvixToMiniC/Base.hs b/src/Juvix/Translation/MicroJuvixToMiniC/Base.hs
new file mode 100644
index 0000000000..d8960bd27b
--- /dev/null
+++ b/src/Juvix/Translation/MicroJuvixToMiniC/Base.hs
@@ -0,0 +1,257 @@
+module Juvix.Translation.MicroJuvixToMiniC.Base
+  ( module Juvix.Translation.MicroJuvixToMiniC.Base,
+    module Juvix.Translation.MicroJuvixToMiniC.Types,
+    module Juvix.Translation.MicroJuvixToMiniC.CNames,
+    module Juvix.Translation.MicroJuvixToMiniC.CBuilder,
+  )
+where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.Text qualified as T
+import Juvix.Internal.Strings qualified as Str
+import Juvix.Prelude
+import Juvix.Syntax.MicroJuvix.InfoTable qualified as Micro
+import Juvix.Syntax.MicroJuvix.Language.Extra (mkPolyType')
+import Juvix.Syntax.MicroJuvix.Language.Extra qualified as Micro
+import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
+import Juvix.Syntax.MiniC.Language
+import Juvix.Translation.MicroJuvixToMiniC.BuiltinTable
+import Juvix.Translation.MicroJuvixToMiniC.CBuilder
+import Juvix.Translation.MicroJuvixToMiniC.CNames
+import Juvix.Translation.MicroJuvixToMiniC.Types
+
+unsupported :: Text -> a
+unsupported msg = error (msg <> " Micro to C: not yet supported")
+
+unfoldFunType :: Micro.PolyType -> ([Micro.PolyType], Micro.PolyType)
+unfoldFunType t = case t ^. Micro.unpolyType of
+  Micro.ExpressionFunction (Micro.Function l r) ->
+    first (mkPolyType' (l ^. Micro.paramType) :) (unfoldFunType (mkPolyType' r))
+  -- TODO: mkPolyType' does redundant work here
+  _ -> ([], t)
+
+unfoldPolyApp :: Micro.TypesTable -> Micro.Application -> (Micro.Expression, [Micro.Expression])
+unfoldPolyApp tab a =
+  let (f, args) = Micro.unfoldApplication a
+   in case f of
+        Micro.ExpressionLiteral {} -> (f, toList args)
+        Micro.ExpressionIden iden -> (f, filterCompileTimeArgs tab (Micro.getName iden) (toList args))
+        _ -> impossible
+
+filterCompileTimeArgs :: Micro.TypesTable -> Micro.Name -> [a] -> [a]
+filterCompileTimeArgs tab idenName lst =
+  map fst $
+    filter (not . isUniverse . snd) $
+      zip lst (map (^. Micro.paramType) params)
+  where
+    ty = HashMap.lookupDefault impossible idenName tab
+    (params, _) = Micro.unfoldFunType ty
+    isUniverse :: Micro.Expression -> Bool
+    isUniverse (Micro.ExpressionUniverse _) = True
+    isUniverse _ = False
+
+mkName :: Micro.Name -> Text
+mkName n =
+  adaptFirstLetter lexeme <> nameTextSuffix
+  where
+    lexeme
+      | T.null lexeme' = "v"
+      | otherwise = lexeme'
+      where
+        lexeme' = T.filter isValidChar (n ^. Micro.nameText)
+    isValidChar :: Char -> Bool
+    isValidChar c = isLetter c && isAscii c
+    adaptFirstLetter :: Text -> Text
+    adaptFirstLetter t = case T.uncons t of
+      Nothing -> impossible
+      Just (h, r) -> T.cons (capitalize h) r
+      where
+        capitalize :: Char -> Char
+        capitalize
+          | capital = toUpper
+          | otherwise = toLower
+        capital = case n ^. Micro.nameKind of
+          Micro.KNameConstructor -> True
+          Micro.KNameInductive -> True
+          Micro.KNameTopModule -> True
+          Micro.KNameLocalModule -> True
+          _ -> False
+    nameTextSuffix :: Text
+    nameTextSuffix = case n ^. Micro.nameKind of
+      Micro.KNameTopModule -> mempty
+      Micro.KNameFunction ->
+        if n ^. Micro.nameText == Str.main then mempty else idSuffix
+      _ -> idSuffix
+    idSuffix :: Text
+    idSuffix = "_" <> show (n ^. Micro.nameId . Micro.unNameId)
+
+goType :: forall r. Member (Reader Micro.InfoTable) r => Micro.PolyType -> Sem r CDeclType
+goType t = case t ^. Micro.unpolyType of
+  Micro.ExpressionIden ti -> getMicroType ti
+  Micro.ExpressionFunction {} -> return declFunctionPtrType
+  Micro.ExpressionUniverse {} -> unsupported "TypeUniverse"
+  Micro.ExpressionApplication a -> goType (mkPolyType' (fst (Micro.unfoldApplication a)))
+  Micro.ExpressionLiteral {} -> impossible
+  Micro.ExpressionHole {} -> impossible
+  where
+    getMicroType :: Micro.Iden -> Sem r CDeclType
+    getMicroType = \case
+      Micro.IdenInductive mn -> getInductiveCType mn
+      Micro.IdenAxiom mn -> do
+        axiomName <- getAxiomCName mn
+        return
+          CDeclType
+            { _typeDeclType = DeclTypeDefType axiomName,
+              _typeIsPtr = False
+            }
+      Micro.IdenVar {} ->
+        return
+          CDeclType
+            { _typeDeclType = uIntPtrType,
+              _typeIsPtr = False
+            }
+      _ -> impossible
+
+typeToFunType :: Member (Reader Micro.InfoTable) r => Micro.PolyType -> Sem r CFunType
+typeToFunType t = do
+  let (args, ret) = unfoldFunType t
+  _cFunArgTypes <- mapM goType args
+  _cFunReturnType <- goType ret
+  return CFunType {..}
+
+applyOnFunStatement ::
+  forall a. Monoid a => (Micro.FunctionDef -> a) -> Micro.Statement -> a
+applyOnFunStatement f = \case
+  Micro.StatementFunction x -> f x
+  Micro.StatementForeign {} -> mempty
+  Micro.StatementAxiom {} -> mempty
+  Micro.StatementInductive {} -> mempty
+  Micro.StatementInclude i -> mconcat $ map (applyOnFunStatement f) (i ^. Micro.includeModule . Micro.moduleBody . Micro.moduleStatements)
+
+getConstructorCName :: Members '[Reader Micro.InfoTable] r => Micro.Name -> Sem r Text
+getConstructorCName n = do
+  ctorInfo <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoConstructors)
+  return
+    ( case ctorInfo ^. Micro.constructorInfoBuiltin of
+        Just builtin -> fromJust (builtinConstructorName builtin)
+        Nothing -> mkName n
+    )
+
+getAxiomCName :: Members '[Reader Micro.InfoTable] r => Micro.Name -> Sem r Text
+getAxiomCName n = do
+  axiomInfo <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoAxioms)
+  return
+    ( case axiomInfo ^. Micro.axiomInfoBuiltin of
+        Just builtin -> fromJust (builtinAxiomName builtin)
+        Nothing -> mkName n
+    )
+
+getInductiveCName :: Members '[Reader Micro.InfoTable] r => Micro.Name -> Sem r (Bool, Text)
+getInductiveCName n = do
+  inductiveInfo <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoInductives)
+  return
+    ( case inductiveInfo ^. (Micro.inductiveInfoDef . Micro.inductiveBuiltin) of
+        Just builtin -> (False, fromJust (builtinInductiveName builtin))
+        Nothing -> (True, asTypeDef (mkName n))
+    )
+
+getInductiveCType :: Member (Reader Micro.InfoTable) r => Micro.Name -> Sem r CDeclType
+getInductiveCType n = do
+  (isPtr, name) <- getInductiveCName n
+  return
+    ( CDeclType
+        { _typeDeclType = DeclTypeDefType name,
+          _typeIsPtr = isPtr
+        }
+    )
+
+typeOfConstructor :: Member (Reader Micro.InfoTable) r => Micro.Name -> Sem r CDeclType
+typeOfConstructor name = do
+  info <- Micro.lookupConstructor name
+  getInductiveCType (info ^. Micro.constructorInfoInductive)
+
+getClausePatterns :: Member (Reader Micro.TypesTable) r => Micro.FunctionClause -> Sem r [Micro.Pattern]
+getClausePatterns c = do
+  tab <- ask
+  return $ filterCompileTimeArgs tab (c ^. Micro.clauseName) (c ^. Micro.clausePatterns)
+
+functionInfoPatternsNum :: Member (Reader Micro.TypesTable) r => Micro.FunctionInfo -> Sem r Int
+functionInfoPatternsNum fInfo = do
+  let c = head (fInfo ^. (Micro.functionInfoDef . Micro.funDefClauses))
+  pats <- getClausePatterns c
+  return (length pats)
+
+buildPatternInfoTable :: forall r. Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r => [Micro.PolyType] -> Micro.FunctionClause -> Sem r PatternInfoTable
+buildPatternInfoTable argTyps c =
+  PatternInfoTable . HashMap.fromList <$> patBindings
+  where
+    funArgBindings :: Sem r [(Expression, CFunType)]
+    funArgBindings = mapM (bimapM (return . ExpressionVar) typeToFunType) (zip funArgs argTyps)
+
+    patArgBindings :: Sem r [(Micro.Pattern, (Expression, CFunType))]
+    patArgBindings = do
+      pats <- getClausePatterns c
+      zip pats <$> funArgBindings
+
+    patBindings :: Sem r [(Text, BindingInfo)]
+    patBindings = patArgBindings >>= concatMapM go
+
+    go :: (Micro.Pattern, (Expression, CFunType)) -> Sem r [(Text, BindingInfo)]
+    go (p, (exp, typ)) = case p of
+      Micro.PatternVariable v ->
+        return
+          [(v ^. Micro.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})]
+      Micro.PatternConstructorApp Micro.ConstructorApp {..} ->
+        goConstructorApp exp _constrAppConstructor _constrAppParameters
+      Micro.PatternWildcard {} -> return []
+      Micro.PatternBraces b -> go (b, (exp, typ))
+
+    goConstructorApp :: Expression -> Micro.Name -> [Micro.Pattern] -> Sem r [(Text, BindingInfo)]
+    goConstructorApp exp constructorName ps = do
+      ctorInfo' <- ctorInfo
+      let ctorArgBindings :: Sem r [(Expression, CFunType)] =
+            mapM (bimapM asConstructor typeToFunType) (zip ctorArgs ctorInfo')
+          patternCtorArgBindings :: Sem r [(Micro.Pattern, (Expression, CFunType))] = zip ps <$> ctorArgBindings
+      patternCtorArgBindings >>= concatMapM go
+      where
+        ctorInfo :: Sem r [Micro.PolyType]
+        ctorInfo = do
+          p' :: HashMap Micro.Name Micro.ConstructorInfo <- asks (^. Micro.infoConstructors)
+          let fInfo = HashMap.lookupDefault impossible constructorName p'
+          return $ map mkPolyType' (fInfo ^. Micro.constructorInfoArgs)
+
+        asConstructor :: Text -> Sem r Expression
+        asConstructor ctorArg = do
+          name <- getConstructorCName constructorName
+          ty <- typeOfConstructor constructorName
+          return (functionCall (ExpressionVar (asProjName ctorArg name)) [castToType ty exp])
+
+getType ::
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Reader PatternInfoTable] r =>
+  Micro.Iden ->
+  Sem r (CFunType, CArity)
+getType = \case
+  Micro.IdenFunction n -> do
+    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoFunctions)
+    funTyp <- typeToFunType (mkPolyType' (fInfo ^. (Micro.functionInfoDef . Micro.funDefType)))
+    nPatterns <- functionInfoPatternsNum fInfo
+    return (funTyp, nPatterns)
+  Micro.IdenConstructor n -> do
+    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoConstructors)
+    argTypes <- mapM (goType . mkPolyType') (fInfo ^. Micro.constructorInfoArgs)
+    typ <- goType $ mkPolyType' (Micro.ExpressionIden (Micro.IdenInductive (fInfo ^. Micro.constructorInfoInductive)))
+    return
+      ( CFunType
+          { _cFunArgTypes = argTypes,
+            _cFunReturnType = typ
+          },
+        length argTypes
+      )
+  Micro.IdenAxiom n -> do
+    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Micro.infoAxioms)
+    t <- typeToFunType (mkPolyType' (fInfo ^. Micro.axiomInfoType))
+    return (t, length (t ^. cFunArgTypes))
+  Micro.IdenVar n -> do
+    t <- (^. bindingInfoType) . HashMap.lookupDefault impossible (n ^. Micro.nameText) <$> asks (^. patternBindings)
+    return (t, length (t ^. cFunArgTypes))
+  Micro.IdenInductive _ -> impossible
diff --git a/src/Juvix/Translation/MonoJuvixToMiniC/BuiltinTable.hs b/src/Juvix/Translation/MicroJuvixToMiniC/BuiltinTable.hs
similarity index 88%
rename from src/Juvix/Translation/MonoJuvixToMiniC/BuiltinTable.hs
rename to src/Juvix/Translation/MicroJuvixToMiniC/BuiltinTable.hs
index 318c722fdf..977508c801 100644
--- a/src/Juvix/Translation/MonoJuvixToMiniC/BuiltinTable.hs
+++ b/src/Juvix/Translation/MicroJuvixToMiniC/BuiltinTable.hs
@@ -1,8 +1,8 @@
-module Juvix.Translation.MonoJuvixToMiniC.BuiltinTable where
+module Juvix.Translation.MicroJuvixToMiniC.BuiltinTable where
 
 import Juvix.Prelude
 import Juvix.Syntax.Concrete.Builtins
-import Juvix.Translation.MonoJuvixToMiniC.CNames
+import Juvix.Translation.MicroJuvixToMiniC.CNames
 
 builtinConstructorName :: BuiltinConstructor -> Maybe Text
 builtinConstructorName = \case
diff --git a/src/Juvix/Translation/MonoJuvixToMiniC/CBuilder.hs b/src/Juvix/Translation/MicroJuvixToMiniC/CBuilder.hs
similarity index 82%
rename from src/Juvix/Translation/MonoJuvixToMiniC/CBuilder.hs
rename to src/Juvix/Translation/MicroJuvixToMiniC/CBuilder.hs
index 3f51d9f2b9..fdf42d0dba 100644
--- a/src/Juvix/Translation/MonoJuvixToMiniC/CBuilder.hs
+++ b/src/Juvix/Translation/MicroJuvixToMiniC/CBuilder.hs
@@ -1,9 +1,9 @@
-module Juvix.Translation.MonoJuvixToMiniC.CBuilder where
+module Juvix.Translation.MicroJuvixToMiniC.CBuilder where
 
 import Juvix.Internal.Strings qualified as Str
 import Juvix.Prelude
 import Juvix.Syntax.MiniC.Language
-import Juvix.Translation.MonoJuvixToMiniC.CNames
+import Juvix.Translation.MicroJuvixToMiniC.CNames
 
 namedArgs :: (Text -> Text) -> [CDeclType] -> [Declaration]
 namedArgs prefix = zipWith namedCDecl argLabels
@@ -51,9 +51,13 @@ mallocSizeOf :: Text -> Expression
 mallocSizeOf typeName =
   functionCall (ExpressionVar Str.malloc) [functionCall (ExpressionVar Str.sizeof) [ExpressionVar typeName]]
 
+functionCallCasted :: CFunType -> Expression -> [Expression] -> Expression
+functionCallCasted fType fExpr args =
+  functionCall fExpr (zipWith castToType (fType ^. cFunArgTypes) args)
+
 juvixFunctionCall :: CFunType -> Expression -> [Expression] -> Expression
 juvixFunctionCall funType funParam args =
-  functionCall (castToType (funPtrType fTyp) (memberAccess Pointer funParam "fun")) (funParam : args)
+  functionCallCasted fTyp (castToType (funPtrType fTyp) (memberAccess Pointer funParam "fun")) (funParam : args)
   where
     fTyp :: CFunType
     fTyp = funType {_cFunArgTypes = declFunctionPtrType : (funType ^. cFunArgTypes)}
diff --git a/src/Juvix/Translation/MonoJuvixToMiniC/CNames.hs b/src/Juvix/Translation/MicroJuvixToMiniC/CNames.hs
similarity index 96%
rename from src/Juvix/Translation/MonoJuvixToMiniC/CNames.hs
rename to src/Juvix/Translation/MicroJuvixToMiniC/CNames.hs
index 034c48f938..ccd5d5499f 100644
--- a/src/Juvix/Translation/MonoJuvixToMiniC/CNames.hs
+++ b/src/Juvix/Translation/MicroJuvixToMiniC/CNames.hs
@@ -1,4 +1,4 @@
-module Juvix.Translation.MonoJuvixToMiniC.CNames where
+module Juvix.Translation.MicroJuvixToMiniC.CNames where
 
 import Juvix.Prelude
 
diff --git a/src/Juvix/Translation/MonoJuvixToMiniC/Closure.hs b/src/Juvix/Translation/MicroJuvixToMiniC/Closure.hs
similarity index 65%
rename from src/Juvix/Translation/MonoJuvixToMiniC/Closure.hs
rename to src/Juvix/Translation/MicroJuvixToMiniC/Closure.hs
index 121e4b1f64..cfbc13e0d4 100644
--- a/src/Juvix/Translation/MonoJuvixToMiniC/Closure.hs
+++ b/src/Juvix/Translation/MicroJuvixToMiniC/Closure.hs
@@ -1,19 +1,21 @@
-module Juvix.Translation.MonoJuvixToMiniC.Closure where
+module Juvix.Translation.MicroJuvixToMiniC.Closure where
 
 import Juvix.Prelude
 import Juvix.Syntax.Concrete.Builtins (IsBuiltin (toBuiltinPrim))
+import Juvix.Syntax.MicroJuvix.InfoTable qualified as Micro
+import Juvix.Syntax.MicroJuvix.Language.Extra (mkPolyType')
+import Juvix.Syntax.MicroJuvix.Language.Extra qualified as Micro
+import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
 import Juvix.Syntax.MiniC.Language
-import Juvix.Syntax.MonoJuvix.InfoTable qualified as Mono
-import Juvix.Syntax.MonoJuvix.Language qualified as Mono
-import Juvix.Translation.MonoJuvixToMiniC.Base
+import Juvix.Translation.MicroJuvixToMiniC.Base
 
 genClosures ::
   forall r.
-  Member (Reader Mono.InfoTable) r =>
-  Mono.Module ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r =>
+  Micro.Module ->
   Sem r [CCode]
-genClosures Mono.Module {..} = do
-  closureInfos <- concatMapM (applyOnFunStatement functionDefClosures) (_moduleBody ^. Mono.moduleStatements)
+genClosures Micro.Module {..} = do
+  closureInfos <- concatMapM (applyOnFunStatement functionDefClosures) (_moduleBody ^. Micro.moduleStatements)
   return (genCClosure =<< nub closureInfos)
 
 genCClosure :: ClosureInfo -> [CCode]
@@ -24,33 +26,34 @@ genCClosure c =
   ]
 
 functionDefClosures ::
-  Member (Reader Mono.InfoTable) r =>
-  Mono.FunctionDef ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r =>
+  Micro.FunctionDef ->
   Sem r [ClosureInfo]
-functionDefClosures Mono.FunctionDef {..} =
-  concatMapM (clauseClosures (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
+functionDefClosures Micro.FunctionDef {..} =
+  concatMapM (clauseClosures (fst (unfoldFunType (mkPolyType' _funDefType)))) (toList _funDefClauses)
 
-lookupBuiltinIden :: Members '[Reader Mono.InfoTable] r => Mono.Iden -> Sem r (Maybe Mono.BuiltinPrim)
+lookupBuiltinIden :: Members '[Reader Micro.InfoTable] r => Micro.Iden -> Sem r (Maybe Micro.BuiltinPrim)
 lookupBuiltinIden = \case
-  Mono.IdenFunction f -> fmap toBuiltinPrim . (^. Mono.functionInfoBuiltin) <$> Mono.lookupFunction f
-  Mono.IdenConstructor c -> fmap toBuiltinPrim . (^. Mono.constructorInfoBuiltin) <$> Mono.lookupConstructor c
-  Mono.IdenAxiom a -> fmap toBuiltinPrim . (^. Mono.axiomInfoBuiltin) <$> Mono.lookupAxiom a
-  Mono.IdenVar {} -> return Nothing
+  Micro.IdenFunction f -> fmap toBuiltinPrim . (^. Micro.functionInfoDef . Micro.funDefBuiltin) <$> Micro.lookupFunction f
+  Micro.IdenConstructor c -> fmap toBuiltinPrim . (^. Micro.constructorInfoBuiltin) <$> Micro.lookupConstructor c
+  Micro.IdenAxiom a -> fmap toBuiltinPrim . (^. Micro.axiomInfoBuiltin) <$> Micro.lookupAxiom a
+  Micro.IdenVar {} -> return Nothing
+  Micro.IdenInductive {} -> impossible
 
 genClosureExpression ::
   forall r.
-  Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
-  [Mono.Type] ->
-  Mono.Expression ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Reader PatternInfoTable] r =>
+  [Micro.PolyType] ->
+  Micro.Expression ->
   Sem r [ClosureInfo]
 genClosureExpression funArgTyps = \case
-  Mono.ExpressionIden i -> do
-    let rootFunMonoName = Mono.getName i
-        rootFunNameId = rootFunMonoName ^. Mono.nameId
-        rootFunName = mkName rootFunMonoName
+  Micro.ExpressionIden i -> do
+    let rootFunMicroName = Micro.getName i
+        rootFunNameId = rootFunMicroName ^. Micro.nameId
+        rootFunName = mkName rootFunMicroName
     builtin <- lookupBuiltinIden i
     case i of
-      Mono.IdenVar {} -> return []
+      Micro.IdenVar {} -> return []
       _ -> do
         (t, patterns) <- getType i
         let argTyps = t ^. cFunArgTypes
@@ -67,42 +70,43 @@ genClosureExpression funArgTyps = \case
                         _closureCArity = patterns
                       }
                   ]
-  Mono.ExpressionApplication a -> exprApplication a
-  Mono.ExpressionLiteral {} -> return []
+  Micro.ExpressionApplication a -> exprApplication a
+  Micro.ExpressionLiteral {} -> return []
+  Micro.ExpressionFunction {} -> impossible
+  Micro.ExpressionHole {} -> impossible
+  Micro.ExpressionUniverse {} -> impossible
   where
-    exprApplication :: Mono.Application -> Sem r [ClosureInfo]
+    exprApplication :: Micro.Application -> Sem r [ClosureInfo]
     exprApplication a = do
-      (f, appArgs) <- unfoldApp a
-      let rootFunMonoName = Mono.getName f
-          rootFunNameId = rootFunMonoName ^. Mono.nameId
-          rootFunName = mkName rootFunMonoName
-      builtin <- lookupBuiltinIden f
-      (fType, patterns) <- getType f
-      closureArgs <- concatMapM (genClosureExpression funArgTyps) appArgs
-      if
-          | length appArgs < length (fType ^. cFunArgTypes) ->
-              return
-                ( [ ClosureInfo
-                      { _closureNameId = rootFunNameId,
-                        _closureRootName = rootFunName,
-                        _closureBuiltin = builtin,
-                        _closureMembers = take (length appArgs) (fType ^. cFunArgTypes),
-                        _closureFunType = fType,
-                        _closureCArity = patterns
-                      }
-                  ]
-                    <> closureArgs
-                )
-          | otherwise -> return closureArgs
-
-    unfoldApp :: Mono.Application -> Sem r (Mono.Iden, [Mono.Expression])
-    unfoldApp Mono.Application {..} = case _appLeft of
-      Mono.ExpressionApplication x -> do
-        uf <- unfoldApp x
-        return (second (_appRight :) uf)
-      Mono.ExpressionIden i -> do
-        return (i, [_appRight])
-      Mono.ExpressionLiteral {} -> impossible
+      tab <- ask
+      let (f0, appArgs) = unfoldPolyApp tab a
+      if null appArgs
+        then genClosureExpression funArgTyps f0
+        else case f0 of
+          Micro.ExpressionLiteral {} -> return []
+          Micro.ExpressionIden f -> do
+            let rootFunMicroName = Micro.getName f
+                rootFunNameId = rootFunMicroName ^. Micro.nameId
+                rootFunName = mkName rootFunMicroName
+            builtin <- lookupBuiltinIden f
+            (fType, patterns) <- getType f
+            closureArgs <- concatMapM (genClosureExpression funArgTyps) (toList appArgs)
+            if
+                | length appArgs < length (fType ^. cFunArgTypes) ->
+                    return
+                      ( [ ClosureInfo
+                            { _closureNameId = rootFunNameId,
+                              _closureRootName = rootFunName,
+                              _closureBuiltin = builtin,
+                              _closureMembers = take (length appArgs) (fType ^. cFunArgTypes),
+                              _closureFunType = fType,
+                              _closureCArity = patterns
+                            }
+                        ]
+                          <> closureArgs
+                      )
+                | otherwise -> return closureArgs
+          _ -> impossible
 
 genClosureEnv :: ClosureInfo -> Declaration
 genClosureEnv c =
@@ -159,13 +163,18 @@ genClosureApply c =
         (c ^. closureFunType)
           { _cFunArgTypes = drop nPatterns (c ^. closureFunType . cFunArgTypes)
           }
+      localFunType :: CFunType
+      localFunType =
+        (c ^. closureFunType)
+          { _cFunArgTypes = take nPatterns (c ^. closureFunType . cFunArgTypes)
+          }
       funName :: Expression
       funName = ExpressionVar (c ^. closureRootName)
       funCall :: Expression
       funCall =
         if
             | null patternArgs -> funName
-            | otherwise -> functionCall funName patternArgs
+            | otherwise -> functionCallCasted localFunType funName patternArgs
       juvixFunCall :: [BodyItem]
       juvixFunCall =
         if
@@ -182,7 +191,7 @@ genClosureApply c =
                 ]
             | otherwise ->
                 [ BodyStatement . StatementReturn . Just $
-                    functionCall (ExpressionVar (closureRootFunction c)) args
+                    functionCallCasted (c ^. closureFunType) (ExpressionVar (closureRootFunction c)) args
                 ]
       envArg :: BodyItem
       envArg =
@@ -269,10 +278,10 @@ genClosureEval c =
         }
 
 clauseClosures ::
-  Members '[Reader Mono.InfoTable] r =>
-  [Mono.Type] ->
-  Mono.FunctionClause ->
+  Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r =>
+  [Micro.PolyType] ->
+  Micro.FunctionClause ->
   Sem r [ClosureInfo]
 clauseClosures argTyps clause = do
   bindings <- buildPatternInfoTable argTyps clause
-  runReader bindings (genClosureExpression argTyps (clause ^. Mono.clauseBody))
+  runReader bindings (genClosureExpression argTyps (clause ^. Micro.clauseBody))
diff --git a/src/Juvix/Translation/MonoJuvixToMiniC/Types.hs b/src/Juvix/Translation/MicroJuvixToMiniC/Types.hs
similarity index 80%
rename from src/Juvix/Translation/MonoJuvixToMiniC/Types.hs
rename to src/Juvix/Translation/MicroJuvixToMiniC/Types.hs
index b05ea844eb..7df6dd4966 100644
--- a/src/Juvix/Translation/MonoJuvixToMiniC/Types.hs
+++ b/src/Juvix/Translation/MicroJuvixToMiniC/Types.hs
@@ -1,9 +1,9 @@
-module Juvix.Translation.MonoJuvixToMiniC.Types where
+module Juvix.Translation.MicroJuvixToMiniC.Types where
 
 import Juvix.Prelude
+import Juvix.Syntax.MicroJuvix.Language qualified as Micro
 import Juvix.Syntax.MiniC.Language
-import Juvix.Syntax.MonoJuvix.Language qualified as Mono
-import Juvix.Translation.MonoJuvixToMiniC.BuiltinTable
+import Juvix.Translation.MicroJuvixToMiniC.BuiltinTable
 
 newtype MiniCResult = MiniCResult
   { _resultCCode :: Text
@@ -20,9 +20,9 @@ newtype PatternInfoTable = PatternInfoTable
 type CArity = Int
 
 data ClosureInfo = ClosureInfo
-  { _closureNameId :: Mono.NameId,
+  { _closureNameId :: Micro.NameId,
     _closureRootName :: Text,
-    _closureBuiltin :: Maybe Mono.BuiltinPrim,
+    _closureBuiltin :: Maybe Micro.BuiltinPrim,
     _closureMembers :: [CDeclType],
     _closureFunType :: CFunType,
     _closureCArity :: CArity
diff --git a/src/Juvix/Translation/MonoJuvixToMiniC/Base.hs b/src/Juvix/Translation/MonoJuvixToMiniC/Base.hs
deleted file mode 100644
index 3fa93fb62a..0000000000
--- a/src/Juvix/Translation/MonoJuvixToMiniC/Base.hs
+++ /dev/null
@@ -1,198 +0,0 @@
-module Juvix.Translation.MonoJuvixToMiniC.Base
-  ( module Juvix.Translation.MonoJuvixToMiniC.Base,
-    module Juvix.Translation.MonoJuvixToMiniC.Types,
-    module Juvix.Translation.MonoJuvixToMiniC.CNames,
-    module Juvix.Translation.MonoJuvixToMiniC.CBuilder,
-  )
-where
-
-import Data.HashMap.Strict qualified as HashMap
-import Data.Text qualified as T
-import Juvix.Internal.Strings qualified as Str
-import Juvix.Prelude
-import Juvix.Syntax.MicroJuvix.Language qualified as Micro
-import Juvix.Syntax.MiniC.Language
-import Juvix.Syntax.MonoJuvix.Language qualified as Mono
-import Juvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
-import Juvix.Translation.MonoJuvixToMiniC.BuiltinTable
-import Juvix.Translation.MonoJuvixToMiniC.CBuilder
-import Juvix.Translation.MonoJuvixToMiniC.CNames
-import Juvix.Translation.MonoJuvixToMiniC.Types
-
-unsupported :: Text -> a
-unsupported msg = error (msg <> " Mono to C: not yet supported")
-
-unfoldFunType :: Mono.Type -> ([Mono.Type], Mono.Type)
-unfoldFunType t = case t of
-  Mono.TypeFunction (Mono.Function l r) -> first (l :) (unfoldFunType r)
-  _ -> ([], t)
-
-mkName :: Mono.Name -> Text
-mkName n =
-  adaptFirstLetter lexeme <> nameTextSuffix
-  where
-    lexeme
-      | T.null lexeme' = "v"
-      | otherwise = lexeme'
-      where
-        lexeme' = T.filter isValidChar (n ^. Mono.nameText)
-    isValidChar :: Char -> Bool
-    isValidChar c = isLetter c && isAscii c
-    adaptFirstLetter :: Text -> Text
-    adaptFirstLetter t = case T.uncons t of
-      Nothing -> impossible
-      Just (h, r) -> T.cons (capitalize h) r
-      where
-        capitalize :: Char -> Char
-        capitalize
-          | capital = toUpper
-          | otherwise = toLower
-        capital = case n ^. Mono.nameKind of
-          Mono.KNameConstructor -> True
-          Mono.KNameInductive -> True
-          Mono.KNameTopModule -> True
-          Mono.KNameLocalModule -> True
-          _ -> False
-    nameTextSuffix :: Text
-    nameTextSuffix = case n ^. Mono.nameKind of
-      Mono.KNameTopModule -> mempty
-      Mono.KNameFunction ->
-        if n ^. Mono.nameText == Str.main then mempty else idSuffix
-      _ -> idSuffix
-    idSuffix :: Text
-    idSuffix = "_" <> show (n ^. Mono.nameId . Micro.unNameId)
-
-goType :: forall r. Member (Reader Mono.InfoTable) r => Mono.Type -> Sem r CDeclType
-goType t = case t of
-  Mono.TypeIden ti -> getMonoType ti
-  Mono.TypeFunction {} -> return declFunctionPtrType
-  Mono.TypeUniverse {} -> unsupported "TypeUniverse"
-  where
-    getMonoType :: Mono.TypeIden -> Sem r CDeclType
-    getMonoType = \case
-      Mono.TypeIdenInductive mn -> do
-        (isPtr, name) <- getInductiveCName mn
-        return
-          ( CDeclType
-              { _typeDeclType = DeclTypeDefType name,
-                _typeIsPtr = isPtr
-              }
-          )
-      Mono.TypeIdenAxiom mn -> do
-        axiomName <- getAxiomCName mn
-        return
-          CDeclType
-            { _typeDeclType = DeclTypeDefType axiomName,
-              _typeIsPtr = False
-            }
-
-typeToFunType :: Member (Reader Mono.InfoTable) r => Mono.Type -> Sem r CFunType
-typeToFunType t = do
-  let (args, ret) = unfoldFunType t
-  _cFunArgTypes <- mapM goType args
-  _cFunReturnType <- goType ret
-  return CFunType {..}
-
-applyOnFunStatement ::
-  forall a. Monoid a => (Mono.FunctionDef -> a) -> Mono.Statement -> a
-applyOnFunStatement f = \case
-  Mono.StatementFunction x -> f x
-  Mono.StatementForeign {} -> mempty
-  Mono.StatementAxiom {} -> mempty
-  Mono.StatementInductive {} -> mempty
-
-getConstructorCName :: Members '[Reader Mono.InfoTable] r => Mono.Name -> Sem r Text
-getConstructorCName n = do
-  ctorInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoConstructors)
-  return
-    ( case ctorInfo ^. Mono.constructorInfoBuiltin of
-        Just builtin -> fromJust (builtinConstructorName builtin)
-        Nothing -> mkName n
-    )
-
-getAxiomCName :: Members '[Reader Mono.InfoTable] r => Mono.Name -> Sem r Text
-getAxiomCName n = do
-  axiomInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoAxioms)
-  return
-    ( case axiomInfo ^. Mono.axiomInfoBuiltin of
-        Just builtin -> fromJust (builtinAxiomName builtin)
-        Nothing -> mkName n
-    )
-
-getInductiveCName :: Members '[Reader Mono.InfoTable] r => Mono.Name -> Sem r (Bool, Text)
-getInductiveCName n = do
-  inductiveInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoInductives)
-  return
-    ( case inductiveInfo ^. Mono.inductiveInfoBuiltin of
-        Just builtin -> (False, fromJust (builtinInductiveName builtin))
-        Nothing -> (True, asTypeDef (mkName n))
-    )
-
-buildPatternInfoTable :: forall r. Member (Reader Mono.InfoTable) r => [Mono.Type] -> Mono.FunctionClause -> Sem r PatternInfoTable
-buildPatternInfoTable argTyps Mono.FunctionClause {..} =
-  PatternInfoTable . HashMap.fromList <$> patBindings
-  where
-    funArgBindings :: Sem r [(Expression, CFunType)]
-    funArgBindings = mapM (bimapM (return . ExpressionVar) typeToFunType) (zip funArgs argTyps)
-
-    patArgBindings :: Sem r [(Mono.Pattern, (Expression, CFunType))]
-    patArgBindings = zip _clausePatterns <$> funArgBindings
-
-    patBindings :: Sem r [(Text, BindingInfo)]
-    patBindings = patArgBindings >>= concatMapM go
-
-    go :: (Mono.Pattern, (Expression, CFunType)) -> Sem r [(Text, BindingInfo)]
-    go (p, (exp, typ)) = case p of
-      Mono.PatternVariable v ->
-        return
-          [(v ^. Mono.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})]
-      Mono.PatternConstructorApp Mono.ConstructorApp {..} ->
-        goConstructorApp exp _constrAppConstructor _constrAppParameters
-      Mono.PatternWildcard {} -> return []
-
-    goConstructorApp :: Expression -> Mono.Name -> [Mono.Pattern] -> Sem r [(Text, BindingInfo)]
-    goConstructorApp exp constructorName ps = do
-      ctorInfo' <- ctorInfo
-      let ctorArgBindings :: Sem r [(Expression, CFunType)] =
-            mapM (bimapM asConstructor typeToFunType) (zip ctorArgs ctorInfo')
-          patternCtorArgBindings :: Sem r [(Mono.Pattern, (Expression, CFunType))] = zip ps <$> ctorArgBindings
-      patternCtorArgBindings >>= concatMapM go
-      where
-        ctorInfo :: Sem r [Mono.Type]
-        ctorInfo = do
-          p' :: HashMap Mono.Name Mono.ConstructorInfo <- asks (^. Mono.infoConstructors)
-          let fInfo = HashMap.lookupDefault impossible constructorName p'
-          return $ fInfo ^. Mono.constructorInfoArgs
-
-        asConstructor :: Text -> Sem r Expression
-        asConstructor ctorArg = do
-          name <- getConstructorCName constructorName
-          return (functionCall (ExpressionVar (asProjName ctorArg name)) [exp])
-
-getType ::
-  Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
-  Mono.Iden ->
-  Sem r (CFunType, CArity)
-getType = \case
-  Mono.IdenFunction n -> do
-    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
-    funTyp <- typeToFunType (fInfo ^. Mono.functionInfoType)
-    return (funTyp, fInfo ^. Mono.functionInfoPatterns)
-  Mono.IdenConstructor n -> do
-    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoConstructors)
-    argTypes <- mapM goType (fInfo ^. Mono.constructorInfoArgs)
-    typ <- goType (Mono.TypeIden (Mono.TypeIdenInductive (fInfo ^. Mono.constructorInfoInductive)))
-    return
-      ( CFunType
-          { _cFunArgTypes = argTypes,
-            _cFunReturnType = typ
-          },
-        length argTypes
-      )
-  Mono.IdenAxiom n -> do
-    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoAxioms)
-    t <- typeToFunType (fInfo ^. Mono.axiomInfoType)
-    return (t, length (t ^. cFunArgTypes))
-  Mono.IdenVar n -> do
-    t <- (^. bindingInfoType) . HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
-    return (t, length (t ^. cFunArgTypes))
diff --git a/test/BackendC/Base.hs b/test/BackendC/Base.hs
index a4f4a21fa8..634b3593ba 100644
--- a/test/BackendC/Base.hs
+++ b/test/BackendC/Base.hs
@@ -4,7 +4,7 @@ import Base
 import Data.FileEmbed
 import Data.Text.IO qualified as TIO
 import Juvix.Pipeline
-import Juvix.Translation.MonoJuvixToMiniC as MiniC
+import Juvix.Translation.MicroJuvixToMiniC as MiniC
 import System.IO.Extra (withTempDir)
 import System.Process qualified as P