Implement type checker with polymorphism (#62)

2025-01-04 13:42:04 +03:00 · 2022-04-22 10:06:34 +02:00 · 2022-04-22 10:06:34 +02:00 · ba47f11189
commit ba47f11189
parent c99c1825d1
31 changed files with 1743 additions and 315 deletions
--- a/.hlint.yaml
+++ b/.hlint.yaml
@ -76,3 +76,5 @@
 - ignore: {name: Use let, within: [Test.All]}
 - ignore: {name: Use String}
 - ignore: {name: Avoid restricted qualification}
+- ignore: {name: Redundant multi-way if}
+- ignore: {name: Eta reduce}
--- a/app/Main.hs
+++ b/app/Main.hs
@ -22,14 +22,13 @@ import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoper
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
 import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
-import MiniJuvix.Syntax.MicroJuvix.Error qualified as Micro
 import MiniJuvix.Syntax.MicroJuvix.Pretty qualified as Micro
 import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroTyped
 import MiniJuvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell
 import MiniJuvix.Termination qualified as T
 import MiniJuvix.Termination.CallGraph qualified as A
 import MiniJuvix.Translation.AbstractToMicroJuvix qualified as Micro
-import MiniJuvix.Translation.MicroJuvixToMiniHaskell qualified as MiniHaskell
+import MiniJuvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
 import MiniJuvix.Translation.ScopedToAbstract qualified as Abstract
 import MiniJuvix.Utils.Version (runDisplayVersion)
 import Options.Applicative
@ -283,9 +282,6 @@ mkScopePrettyOptions ScopeOptions {..} =
 parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
 parseModuleIO = fromRightIO id . Parser.runModuleParserIO

-- parseModuleIO' :: FilePath -> IO Parser.ParserResult
-- parseModuleIO' = fromRightIO id . Parser.runModuleParserIO'
-
 minijuvixYamlFile :: FilePath
 minijuvixYamlFile = "minijuvix.yaml"

@ -377,13 +373,7 @@ runCLI cli = do
      micro <- head . (^. MicroTyped.resultModules) <$> runIO (upToMicroJuvixTyped (getEntryPoint root opts))
      case MicroTyped.checkModule micro of
        Right _ -> putStrLn "Well done! It type checks"
-        Left (Micro.TypeCheckerErrors es) ->
-          sequence_
-            ( intersperse
-                (putStrLn "")
-                (printErrorAnsi <$> toList es)
-            )
-            >> exitFailure
+        Left err -> printErrorAnsi err >> exitFailure
    MiniHaskell o -> do
      minihaskell <- head . (^. MiniHaskell.resultModules) <$> runIO (upToMiniHaskell (getEntryPoint root o))
      supportsAnsi <- Ansi.hSupportsANSI IO.stdout
--- a/notes/Monomorphization.org
+++ b/notes/Monomorphization.org
@ -0,0 +1,92 @@
+* Monomorphization
+ Monomorphization refers to the process of converting polymorphic code to
+ monomorphic code (no type variables) through static analysis.
+
+ Example:
+ #+begin_src minijuvix
+ id : (A : Type) → A → A;
+ id _ a ≔ a;
+
+ b : Bool;
+ b ≔ id Bool true;
+
+ n : Nat;
+ n ≔ id Nat zero;
+ #+end_src
+
+ Is translated into:
+ #+begin_src minijuvix
+ id_Bool : Bool → Bool;
+ id_Bool a ≔ a;
+
+ id_Nat : Nat → Nat;
+ id_Nat a ≔ a;
+ #+end_src
+
+* More examples
+** Mutual recursion
+#+begin_src minijuvix
+inductive List (A : Type) {
+  nil : List A;
+  cons : A → List A → List A;
+};
+
+even : (A : Type) → List A → Bool;
+even A nil ≔ true ;
+even A (cons _ xs) ≔ not (odd A xs) ;
+
+odd : (A : Type) → List A → Bool;
+odd A nil ≔ false ;
+odd A (cons _ xs) ≔ not (even A xs) ;
+
+-- main ≔ even Bool ..  odd Nat;
+#+end_src
+
+* Algorithm
+** Assumptions:
+1. Type abstractions only appear at the leftmost part of a type signature.
+2. All functions and constructors are fully type-applied: i.e. currying for
+   types is not supported.
+3. The =main= function is the entry point and has a concrete type.
+4. All axioms are monomorphic.
+
+** Definitions
+1. *Application*. An application is an expression of the form =t₁ t₂ … tₙ= with n > 0.
+
+2. *Sub application*. If =t₁ t₂ … tₙ= is an application then for every =0<i<n=
+ =t₁ t₂ … tᵢ= is a sub application.
+
+Fix a minijuvix program =P=. Let =𝒲= be the set of all applications that appear in =P=.
+1. *Proper application*. A proper application is an application =A∈𝒲= such that
+   for every =A'∈𝒲= we have that =A= is *not* a sub application of =A'=.
+
+2. *Type application*. If =t a₁ a₂ … aₙ= is a proper application and =a₁, …, aₘ=
+   and =aₘ₊₁= is not a type or =m=n= are types, then =t a₁, …, aₘ= is a type
+   application.
+
+3. *Concrete type*. A type is concrete if it involves no type variables.
+
+4. *Concrete type application*. A type application =t a₁ a₂ … aₙ= if =a₁, a₂, …,
+   aₙ= are concrete types.
+
+** Option 1
+  Gather all type applications in =main=. Since =main= type is concrete, these
+  type applications are all concrete. We now have a stack =c₁, c₂, …, cₙ= of
+  concrete type applications.
+  1. If the stack is empty, we are done.
+  2. Otherwise pop =c₁= from the stack. It will be of the form =t a₁ … aₘ=,
+     where =t= is either a constructor or a function and =a₁, …, aₘ= are
+     concrete types.
+  3. If the instantiation =t a₁ … aₘ= has already been registered go to step 1.
+     Otherwise continue to the next step.
+  4. Register the instantiation =t a₁ … aₘ=.
+  5. If =t= is a constructor continue to step 1.
+  6. If =t= is a function, then it has type variables =v₁, …, vₘ=.
+     Consider the substitution =σ = {v₁ ↦ a₁, …, vₘ ↦ aₘ}=.
+     Consider the list of type applications in the body of =t=: =d₁, …,dᵣ=.
+     Add =σ(d₁), …, σ(dᵣ)= to the stack and continue to step 1.
+     It is easy to see that for any =i=, =σ(dᵢ)= is a concrete type application.
+
+*** Correctness
+   It should be clear that the algorithm terminates and registers all
+   instantiations of constructors and functions.
--- a/package.yaml
+++ b/package.yaml
@ -78,6 +78,7 @@ default-extensions:
 - GeneralizedNewtypeDeriving
 - ImportQualifiedPost
 - LambdaCase
+- MultiWayIf
 - NoImplicitPrelude
 - OverloadedStrings
 - QuasiQuotes
--- a/src/MiniJuvix/Pipeline.hs
+++ b/src/MiniJuvix/Pipeline.hs
@ -17,7 +17,8 @@ import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult qualified as MicroJuvix
 import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroJuvix
 import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroJuvix
 import MiniJuvix.Translation.AbstractToMicroJuvix qualified as MicroJuvix
-import MiniJuvix.Translation.MicroJuvixToMiniHaskell qualified as MiniHaskell
+import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as MonoJuvix
+import MiniJuvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
 import MiniJuvix.Translation.ScopedToAbstract qualified as Abstract

 type StageInput :: Pipe -> GHC.Type
@ -64,9 +65,13 @@ upToMicroJuvix = upToAbstract >=> pipelineMicroJuvix
 upToMicroJuvixTyped :: Members '[Files, Error AJuvixError] r => EntryPoint -> Sem r MicroJuvix.MicroJuvixTypedResult
 upToMicroJuvixTyped = upToMicroJuvix >=> pipelineMicroJuvixTyped

+upToMonoJuvix ::
+  Members '[Files, Error AJuvixError] r => EntryPoint -> Sem r MonoJuvix.MonoJuvixResult
+upToMonoJuvix = upToMicroJuvixTyped >=> pipelineMonoJuvix
+
 upToMiniHaskell ::
  Members '[Files, Error AJuvixError] r => EntryPoint -> Sem r MiniHaskell.MiniHaskellResult
-upToMiniHaskell = upToMicroJuvixTyped >=> pipelineMiniHaskell
+upToMiniHaskell = upToMonoJuvix >=> pipelineMiniHaskell

 --------------------------------------------------------------------------------

@ -92,10 +97,16 @@ pipelineMicroJuvixTyped ::
  Members '[Files, Error AJuvixError] r =>
  MicroJuvix.MicroJuvixResult ->
  Sem r MicroJuvix.MicroJuvixTypedResult
-pipelineMicroJuvixTyped = mapError (toAJuvixError @MicroJuvix.TypeCheckerErrors) . MicroJuvix.entryMicroJuvixTyped
+pipelineMicroJuvixTyped = mapError (toAJuvixError @MicroJuvix.TypeCheckerError) . MicroJuvix.entryMicroJuvixTyped
+
+pipelineMonoJuvix ::
+  Members '[Files, Error AJuvixError] r =>
+  MicroJuvix.MicroJuvixTypedResult ->
+  Sem r MonoJuvix.MonoJuvixResult
+pipelineMonoJuvix = mapError (toAJuvixError @Text) . MonoJuvix.entryMonoJuvix

 pipelineMiniHaskell ::
  Members '[Files, Error AJuvixError] r =>
-  MicroJuvix.MicroJuvixTypedResult ->
+  MonoJuvix.MonoJuvixResult ->
  Sem r MiniHaskell.MiniHaskellResult
 pipelineMiniHaskell = mapError (toAJuvixError @Text) . MiniHaskell.entryMiniHaskell
--- a/src/MiniJuvix/Prelude/Pretty.hs
+++ b/src/MiniJuvix/Prelude/Pretty.hs
@ -4,15 +4,11 @@ module MiniJuvix.Prelude.Pretty
  )
 where

------------------------------------------------------------------------------
-
 import MiniJuvix.Prelude.Base
 import Prettyprinter
 import Prettyprinter.Render.Terminal qualified as Ansi
 import Prettyprinter.Render.Text qualified as Text

------------------------------------------------------------------------------
-
 class HasAnsiBackend a where
  toAnsi :: a -> SimpleDocStream Ansi.AnsiStyle

@ -31,3 +27,6 @@ toAnsiText :: (HasAnsiBackend a, HasTextBackend a) => Bool -> a -> Text
 toAnsiText useColors
  | useColors = Ansi.renderStrict . toAnsi
  | otherwise = Text.renderStrict . toText
+
+prettyText :: Pretty a => a -> Text
+prettyText = Text.renderStrict . layoutPretty defaultLayoutOptions . pretty
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
@ -455,8 +455,11 @@ instance PrettyCode n => PrettyCode (S.Name' n) where
  ppCode S.Name' {..} = do
    nameConcrete' <- annotateKind _nameKind <$> ppCode _nameConcrete
    showNameId <- asks _optShowNameId
-    uid <- if showNameId then ("@" <>) <$> ppCode _nameId else return mempty
-    return $ annSRef (nameConcrete' <> uid)
+    uid <-
+      if
+          | showNameId -> Just . ("@" <>) <$> ppCode _nameId
+          | otherwise -> return Nothing
+    return $ annSRef (nameConcrete' <?> uid)
    where
      annSRef :: Doc Ann -> Doc Ann
      annSRef = annotate (AnnRef (S.absTopModulePath _nameDefinedIn) _nameId)
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
@ -5,9 +5,6 @@ module MiniJuvix.Syntax.MicroJuvix.Error
  )
 where

--------------------------------------------------------------------------------
-
-import Data.Text qualified as Text
 import MiniJuvix.Prelude qualified as Prelude
 import MiniJuvix.Prelude.Base
 import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
@ -15,8 +12,6 @@ import MiniJuvix.Syntax.MicroJuvix.Error.Pretty qualified as P
 import MiniJuvix.Syntax.MicroJuvix.Error.Types
 import Prettyprinter

--------------------------------------------------------------------------------
-
 data TypeCheckerError
  = ErrTooManyPatterns TooManyPatterns
  | ErrWrongConstructorType WrongConstructorType
@ -25,13 +20,6 @@ data TypeCheckerError
  | ErrExpectedFunctionType ExpectedFunctionType
  deriving stock (Show)

-newtype TypeCheckerErrors = TypeCheckerErrors
-  { _unTypeCheckerErrors :: NonEmpty TypeCheckerError
-  }
-  deriving stock (Show)
-
-makeLenses ''TypeCheckerErrors
-
 ppTypeCheckerError :: TypeCheckerError -> Doc Eann
 ppTypeCheckerError = \case
  ErrWrongConstructorType e -> ppError e
@ -49,10 +37,3 @@ instance Prelude.JuvixError TypeCheckerError where

  renderText :: TypeCheckerError -> Text
  renderText = P.renderText . docStream
-
-instance Prelude.JuvixError TypeCheckerErrors where
-  renderAnsiText :: TypeCheckerErrors -> Text
-  renderAnsiText TypeCheckerErrors {..} = (Text.unlines . toList) (fmap Prelude.renderAnsiText _unTypeCheckerErrors)
-
-  renderText :: TypeCheckerErrors -> Text
-  renderText TypeCheckerErrors {..} = (Text.unlines . toList) (fmap Prelude.renderText _unTypeCheckerErrors)
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
@ -7,8 +7,8 @@ import MiniJuvix.Syntax.MicroJuvix.Language
 -- not match the type of the inductive being matched
 data WrongConstructorType = WrongConstructorType
  { _wrongCtorTypeName :: Name,
-    _wrongCtorTypeExpected :: Type,
-    _wrongCtorTypeActual :: Type,
+    _wrongCtorTypeExpected :: InductiveName,
+    _wrongCtorTypeActual :: InductiveName,
    _wrongCtorTypeFunname :: Name
  }
  deriving stock (Show)
@ -17,7 +17,7 @@ data WrongConstructorType = WrongConstructorType
 -- the expected arguments of the constructor
 data WrongConstructorAppArgs = WrongConstructorAppArgs
  { _wrongCtorAppApp :: ConstructorApp,
-    _wrongCtorAppTypes :: [Type],
+    _wrongCtorAppTypes :: [FunctionArgType],
    _wrongCtorAppName :: Name
  }
  deriving stock (Show)
@ -42,7 +42,7 @@ data ExpectedFunctionType = ExpectedFunctionType
 -- | A function definition clause matches too many arguments
 data TooManyPatterns = TooManyPatterns
  { _tooManyPatternsClause :: FunctionClause,
-    _tooManyPatternsTypes :: [Type]
+    _tooManyPatternsTypes :: [FunctionArgType]
  }
  deriving stock (Show)

--- a/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs
@ -6,7 +6,8 @@ import MiniJuvix.Syntax.Backends
 import MiniJuvix.Syntax.MicroJuvix.Language

 data ConstructorInfo = ConstructorInfo
-  { _constructorInfoArgs :: [Type],
+  { _constructorInfoInductiveParameters :: [InductiveParameter],
+    _constructorInfoArgs :: [Type],
    _constructorInfoInductive :: InductiveName
  }

@ -19,22 +20,34 @@ data AxiomInfo = AxiomInfo
    _axiomInfoBackends :: [BackendItem]
  }

+newtype InductiveInfo = InductiveInfo
+  { _inductiveInfoDef :: InductiveDef
+  }
+
 data InfoTable = InfoTable
  { _infoConstructors :: HashMap Name ConstructorInfo,
    _infoAxioms :: HashMap Name AxiomInfo,
-    _infoFunctions :: HashMap Name FunctionInfo
+    _infoFunctions :: HashMap Name FunctionInfo,
+    _infoInductives :: HashMap Name InductiveInfo
  }

 -- TODO temporary function.
 buildTable :: Module -> InfoTable
 buildTable m = InfoTable {..}
  where
+    _infoInductives :: HashMap Name InductiveInfo
+    _infoInductives =
+      HashMap.fromList
+        [ (d ^. inductiveName, InductiveInfo d)
+          | StatementInductive d <- ss
+        ]
    _infoConstructors :: HashMap Name ConstructorInfo
    _infoConstructors =
      HashMap.fromList
-        [ (c ^. constructorName, ConstructorInfo args ind)
+        [ (c ^. constructorName, ConstructorInfo params args ind)
          | StatementInductive d <- ss,
            let ind = d ^. inductiveName,
+            let params = d ^. inductiveParameters,
            c <- d ^. inductiveConstructors,
            let args = c ^. constructorParameters
        ]
@ -56,3 +69,4 @@ makeLenses ''InfoTable
 makeLenses ''FunctionInfo
 makeLenses ''ConstructorInfo
 makeLenses ''AxiomInfo
+makeLenses ''InductiveInfo
--- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
@ -52,7 +52,10 @@ instance HasNameKind Name where
  getNameKind = _nameKind

 instance Pretty Name where
-  pretty = pretty . _nameText
+  pretty n =
+    pretty (n ^. nameText)
+      <> "@"
+      <> pretty (n ^. nameId)

 data Module = Module
  { _moduleName :: Name,
@ -93,6 +96,7 @@ data Iden
  | IdenConstructor Name
  | IdenVar VarName
  | IdenAxiom Name
+  | IdenInductive Name
  deriving stock (Show)

 data TypedExpression = TypedExpression
@ -118,7 +122,7 @@ data Function = Function
  { _funLeft :: Type,
    _funRight :: Type
  }
-  deriving stock (Show, Eq)
+  deriving stock (Show)

 -- | Fully applied constructor in a pattern.
 data ConstructorApp = ConstructorApp
@ -133,8 +137,14 @@ data Pattern
  | PatternWildcard
  deriving stock (Show)

+newtype InductiveParameter = InductiveParameter
+  { _inductiveParamName :: VarName
+  }
+  deriving stock (Show, Eq)
+
 data InductiveDef = InductiveDef
  { _inductiveName :: InductiveName,
+    _inductiveParameters :: [InductiveParameter],
    _inductiveConstructors :: [InductiveConstructorDef]
  }

@ -146,14 +156,34 @@ data InductiveConstructorDef = InductiveConstructorDef
 data TypeIden
  = TypeIdenInductive InductiveName
  | TypeIdenAxiom AxiomName
+  | TypeIdenVariable VarName
  deriving stock (Show, Eq)

+data TypeApplication = TypeApplication
+  { _typeAppLeft :: Type,
+    _typeAppRight :: Type
+  }
+  deriving stock (Show)
+
+data TypeAbstraction = TypeAbstraction
+  { _typeAbsVar :: VarName,
+    _typeAbsBody :: Type
+  }
+  deriving stock (Show)
+
 data Type
  = TypeIden TypeIden
+  | TypeApp TypeApplication
  | TypeFunction Function
+  | TypeAbs TypeAbstraction
  | TypeUniverse
  | TypeAny
-  deriving stock (Show, Eq)
+  deriving stock (Show)
+
+data FunctionArgType
+  = FunctionArgTypeAbstraction VarName
+  | FunctionArgTypeType Type
+  deriving stock (Show)

 makeLenses ''Module
 makeLenses ''Function
@ -164,12 +194,21 @@ makeLenses ''AxiomDef
 makeLenses ''ModuleBody
 makeLenses ''Application
 makeLenses ''TypedExpression
+makeLenses ''TypeAbstraction
+makeLenses ''TypeApplication
+makeLenses ''InductiveParameter
 makeLenses ''InductiveConstructorDef
 makeLenses ''ConstructorApp

+instance HasAtomicity Name where
+  atomicity = const Atom
+
 instance HasAtomicity Application where
  atomicity = const (Aggregate appFixity)

+instance HasAtomicity TypeApplication where
+  atomicity = const (Aggregate appFixity)
+
 instance HasAtomicity Expression where
  atomicity e = case e of
    ExpressionIden {} -> Atom
@ -180,12 +219,17 @@ instance HasAtomicity Expression where
 instance HasAtomicity Function where
  atomicity = const (Aggregate funFixity)

+instance HasAtomicity TypeAbstraction where
+  atomicity = const (Aggregate funFixity)
+
 instance HasAtomicity Type where
  atomicity t = case t of
    TypeIden {} -> Atom
    TypeFunction f -> atomicity f
    TypeUniverse -> Atom
    TypeAny -> Atom
+    TypeAbs a -> atomicity a
+    TypeApp a -> atomicity a

 instance HasAtomicity ConstructorApp where
  atomicity (ConstructorApp _ args)
@ -211,3 +255,4 @@ instance HasLoc Iden where
    IdenConstructor c -> C.getLoc c
    IdenVar v -> C.getLoc v
    IdenAxiom a -> C.getLoc a
+    IdenInductive a -> C.getLoc a
--- a/src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs
@ -1,11 +1,23 @@
 module MiniJuvix.Syntax.MicroJuvix.LocalVars where

+import Data.HashMap.Strict qualified as HashMap
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MicroJuvix.Language

-newtype LocalVars = LocalVars
-  { _localTypes :: HashMap VarName Type
+data LocalVars = LocalVars
+  { _localTypes :: HashMap VarName Type,
+    _localTyMap :: HashMap VarName VarName
  }
-  deriving newtype (Semigroup, Monoid)
+  deriving stock (Show)

 makeLenses ''LocalVars
+
+addType :: VarName -> Type -> LocalVars -> LocalVars
+addType v t = over localTypes (HashMap.insert v t)
+
+emptyLocalVars :: LocalVars
+emptyLocalVars =
+  LocalVars
+    { _localTypes = mempty,
+      _localTyMap = mempty
+    }
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@ -9,14 +9,16 @@ import MiniJuvix.Syntax.MicroJuvix.Language
 import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
 import Prettyprinter

-newtype Options = Options
-  { _optIndent :: Int
+data Options = Options
+  { _optIndent :: Int,
+    _optShowNameId :: Bool
  }

 defaultOptions :: Options
 defaultOptions =
  Options
-    { _optIndent = 2
+    { _optIndent = 2,
+      _optShowNameId = True
    }

 docStream :: PrettyCode c => Options -> c -> SimpleDocStream Ann
@ -32,11 +34,19 @@ class PrettyCode c where
 runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
 runPrettyCode opts = run . runReader opts . ppCode

+instance PrettyCode NameId where
+  ppCode (NameId k) = return (pretty k)
+
 instance PrettyCode Name where
-  ppCode n =
+  ppCode n = do
+    showNameId <- asks _optShowNameId
+    uid <-
+      if
+          | showNameId -> Just . ("@" <>) <$> ppCode (n ^. nameId)
+          | otherwise -> return Nothing
    return $
      annotate (AnnKind (n ^. nameKind)) $
-        pretty (n ^. nameText) <> "_" <> pretty (n ^. nameId)
+        pretty (n ^. nameText) <?> uid

 instance PrettyCode Iden where
  ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
@ -45,6 +55,13 @@ instance PrettyCode Iden where
    IdenConstructor na -> ppCode na
    IdenVar na -> ppCode na
    IdenAxiom a -> ppCode a
+    IdenInductive a -> ppCode a
+
+instance PrettyCode TypeApplication where
+  ppCode (TypeApplication l r) = do
+    l' <- ppLeftExpression appFixity l
+    r' <- ppRightExpression appFixity r
+    return $ l' <+> r'

 instance PrettyCode Application where
  ppCode a = do
@ -119,6 +136,13 @@ instance PrettyCode BackendItem where
    return $
      backend <+> kwMapsto <+> pretty _backendItemCode

+instance PrettyCode TypeAbstraction where
+  ppCode (TypeAbstraction v r) = do
+    v' <- ppCode v
+    let l' = parens (v' <+> colon <+> kwType)
+    r' <- ppRightExpression funFixity r
+    return $ l' <+> kwArrow <+> r'
+
 instance PrettyCode Function where
  ppCode (Function l r) = do
    l' <- ppLeftExpression funFixity l
@ -129,6 +153,12 @@ instance PrettyCode TypeIden where
  ppCode = \case
    TypeIdenInductive i -> ppCode i
    TypeIdenAxiom i -> ppCode i
+    TypeIdenVariable i -> ppCode i
+
+instance PrettyCode FunctionArgType where
+  ppCode = \case
+    FunctionArgTypeType t -> ppCode t
+    FunctionArgTypeAbstraction v -> ppCode v

 instance PrettyCode Type where
  ppCode = \case
@ -136,11 +166,13 @@ instance PrettyCode Type where
    TypeFunction f -> ppCode f
    TypeUniverse -> return kwType
    TypeAny -> return kwAny
+    TypeApp a -> ppCode a
+    TypeAbs a -> ppCode a

 instance PrettyCode InductiveConstructorDef where
  ppCode c = do
    constructorName' <- ppCode (c ^. constructorName)
-    constructorParameters' <- mapM ppCode (c ^. constructorParameters)
+    constructorParameters' <- mapM ppCodeAtom (c ^. constructorParameters)
    return (hsep $ constructorName' : constructorParameters')

 indent' :: Member (Reader Options) r => Doc a -> Sem r (Doc a)
@ -156,12 +188,22 @@ bracesIndent d = do
  d' <- indent' d
  return $ braces (line <> d' <> line)

+instance PrettyCode InductiveParameter where
+  ppCode (InductiveParameter v) = do
+    v' <- ppCode v
+    return $ parens (v' <+> kwColon <+> kwType)
+
 instance PrettyCode InductiveDef where
  ppCode d = do
    inductiveName' <- ppCode (d ^. inductiveName)
+    params <- hsep' <$> mapM ppCode (d ^. inductiveParameters)
    inductiveConstructors' <- mapM ppCode (d ^. inductiveConstructors)
    rhs <- indent' $ align $ concatWith (\a b -> a <> line <> kwPipe <+> b) inductiveConstructors'
-    return $ kwData <+> inductiveName' <+> kwEquals <> line <> rhs
+    return $ kwData <+> inductiveName' <+?> params <+> kwEquals <> line <> rhs
+    where
+      hsep' l
+        | null l = Nothing
+        | otherwise = Just (hsep l)

 instance PrettyCode ConstructorApp where
  ppCode c = do
--- a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
@ -17,7 +17,7 @@ import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult
 import Polysemy.Error (fromEither)

 entryMicroJuvixTyped ::
-  (Member (Error TypeCheckerErrors) r) =>
+  (Member (Error TypeCheckerError) r) =>
  MicroJuvixResult ->
  Sem r MicroJuvixTypedResult
 entryMicroJuvixTyped res@MicroJuvixResult {..} = do
@ -28,15 +28,12 @@ entryMicroJuvixTyped res@MicroJuvixResult {..} = do
        _resultModules = r
      }

-checkModule :: Module -> Either TypeCheckerErrors Module
-checkModule m = run $ do
-  (es, checkedModule) <- runOutputList $ runReader (buildTable m) (checkModule' m)
-  return $ case nonEmpty es of
-    Nothing -> Right checkedModule
-    Just xs -> Left (TypeCheckerErrors {_unTypeCheckerErrors = xs})
+checkModule :: Module -> Either TypeCheckerError Module
+checkModule m =
+  run $ runError $ runReader (buildTable m) (checkModule' m)

 checkModule' ::
-  Members '[Reader InfoTable, Output TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
  Module ->
  Sem r Module
 checkModule' Module {..} = do
@ -48,7 +45,7 @@ checkModule' Module {..} = do
      }

 checkModuleBody ::
-  Members '[Reader InfoTable, Output TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
  ModuleBody ->
  Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@ -59,7 +56,7 @@ checkModuleBody ModuleBody {..} = do
      }

 checkStatement ::
-  Members '[Reader InfoTable, Output TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
  Statement ->
  Sem r Statement
 checkStatement s = case s of
@ -69,7 +66,7 @@ checkStatement s = case s of
  StatementAxiom {} -> return s

 checkFunctionDef ::
-  Members '[Reader InfoTable, Output TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
  FunctionDef ->
  Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
@ -87,10 +84,10 @@ checkExpression ::
  Expression ->
  Sem r Expression
 checkExpression t e = do
-  t' <- inferExpression' e
-  let inferredType = t' ^. typedType
+  e' <- inferExpression' e
+  let inferredType = e' ^. typedType
  unlessM (matchTypes t inferredType) (throw (err inferredType))
-  return (ExpressionTyped t')
+  return (ExpressionTyped e')
  where
    err infTy =
      ErrWrongType
@ -102,15 +99,58 @@ checkExpression t e = do
        )

 matchTypes ::
-  Members '[Reader InfoTable] r =>
+  Members '[Reader InfoTable, Reader LocalVars] r =>
  Type ->
  Type ->
  Sem r Bool
 matchTypes a b = do
-  a' <- normalizeType a
-  b' <- normalizeType b
+  areAlphaEq <- alphaEq a b
  return $
-    a' == TypeAny || b' == TypeAny || a' == b'
+    isAny a || isAny b || areAlphaEq
+  where
+    isAny = \case
+      TypeAny -> True
+      _ -> False
+
+-- | Alpha equivalence
+alphaEq :: Type -> Type -> Sem r Bool
+alphaEq ty = runReader ini . go ty
+  where
+    ini :: HashMap VarName VarName
+    ini = mempty
+    go ::
+      forall r.
+      Members '[Reader (HashMap VarName VarName)] r =>
+      Type ->
+      Type ->
+      Sem r Bool
+    go a' b' = case (a', b') of
+      (TypeIden a, TypeIden b) -> goIden a b
+      (TypeApp a, TypeApp b) -> goApp a b
+      (TypeAbs a, TypeAbs b) -> goAbs a b
+      (TypeFunction a, TypeFunction b) -> goFunction a b
+      (TypeUniverse, TypeUniverse) -> return True
+      -- TODO TypeAny should match anything?
+      (TypeAny, TypeAny) -> return True
+      -- TODO is the final wildcard bad style?
+      -- what if more Type constructors are added
+      _ -> return False
+      where
+        goIden :: TypeIden -> TypeIden -> Sem r Bool
+        goIden ia ib = case (ia, ib) of
+          (TypeIdenInductive a, TypeIdenInductive b) -> return (a == b)
+          (TypeIdenAxiom a, TypeIdenAxiom b) -> return (a == b)
+          (TypeIdenVariable a, TypeIdenVariable b) -> do
+            mappedEq <- (== Just b) . HashMap.lookup a <$> ask
+            return (a == b || mappedEq)
+          _ -> return False
+        goApp :: TypeApplication -> TypeApplication -> Sem r Bool
+        goApp (TypeApplication f x) (TypeApplication f' x') = andM [go f f', go x x']
+        goFunction :: Function -> Function -> Sem r Bool
+        goFunction (Function l r) (Function l' r') = andM [go l l', go r r']
+        goAbs :: TypeAbstraction -> TypeAbstraction -> Sem r Bool
+        goAbs (TypeAbstraction v1 r) (TypeAbstraction v2 r') =
+          local (HashMap.insert v1 v2) (go r r')

 inferExpression ::
  Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
@ -121,6 +161,9 @@ inferExpression = fmap ExpressionTyped . inferExpression'
 lookupConstructor :: Member (Reader InfoTable) r => Name -> Sem r ConstructorInfo
 lookupConstructor f = HashMap.lookupDefault impossible f <$> asks _infoConstructors

+lookupInductive :: Member (Reader InfoTable) r => InductiveName -> Sem r InductiveInfo
+lookupInductive f = HashMap.lookupDefault impossible f <$> asks _infoInductives
+
 lookupFunction :: Member (Reader InfoTable) r => Name -> Sem r FunctionInfo
 lookupFunction f = HashMap.lookupDefault impossible f <$> asks _infoFunctions

@ -133,23 +176,49 @@ lookupVar v = HashMap.lookupDefault impossible v <$> asks _localTypes
 constructorType :: Member (Reader InfoTable) r => Name -> Sem r Type
 constructorType c = do
  info <- lookupConstructor c
-  let r = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
-  return (foldFunType (info ^. constructorInfoArgs) r)
+  let (as, bs) = constructorArgTypes info
+      args =
+        map FunctionArgTypeAbstraction as
+          ++ map FunctionArgTypeType bs
+      ind = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
+      saturatedTy =
+        foldl'
+          ( \t v ->
+              TypeApp
+                ( TypeApplication
+                    t
+                    (TypeIden (TypeIdenVariable v))
+                )
+          )
+          ind
+          as
+  return (foldFunType args saturatedTy)
+
+constructorArgTypes :: ConstructorInfo -> ([VarName], [Type])
+constructorArgTypes i =
+  ( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters),
+    i ^. constructorInfoArgs
+  )

 -- | [a, b] c ==> a -> (b -> c)
-foldFunType :: [Type] -> Type -> Type
+foldFunType :: [FunctionArgType] -> Type -> Type
 foldFunType l r = case l of
  [] -> r
-  (a : as) -> TypeFunction (Function a (foldFunType as r))
+  (a : as) ->
+    let r' = foldFunType as r
+     in case a of
+          FunctionArgTypeAbstraction v -> TypeAbs (TypeAbstraction v r')
+          FunctionArgTypeType t -> TypeFunction (Function t r')

 -- | a -> (b -> c)  ==> ([a, b], c)
-unfoldFunType :: Type -> ([Type], Type)
+unfoldFunType :: Type -> ([FunctionArgType], Type)
 unfoldFunType t = case t of
-  TypeFunction (Function l r) -> first (l :) (unfoldFunType r)
+  TypeFunction (Function l r) -> first (FunctionArgTypeType l :) (unfoldFunType r)
+  TypeAbs (TypeAbstraction var r) -> first (FunctionArgTypeAbstraction var :) (unfoldFunType r)
  _ -> ([], t)

 checkFunctionClause ::
-  Members '[Reader InfoTable, Output TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
  FunctionInfo ->
  FunctionClause ->
  Sem r FunctionClause
@ -157,24 +226,27 @@ checkFunctionClause info clause@FunctionClause {..} = do
  let (argTys, rty) = unfoldFunType (info ^. functionInfoType)
      (patTys, restTys) = splitAt (length _clausePatterns) argTys
      bodyTy = foldFunType restTys rty
-  if length patTys /= length _clausePatterns
-    then output (tyErr patTys) $> clause
-    else do
-      eLocals <- checkPatterns _clauseName patTys _clausePatterns
-      _clauseBody' <- case eLocals of
-        Left err -> output err $> _clauseBody
-        Right locals -> do
-          eclauseBody <- runError @TypeCheckerError $ runReader locals (checkExpression bodyTy _clauseBody)
-          case eclauseBody of
-            Left err -> output err $> _clauseBody
-            Right r -> return r
-      return
-        FunctionClause
-          { _clauseBody = _clauseBody',
-            ..
-          }
+  if
+      -- TODO consider zip exact
+      | length patTys /= length _clausePatterns -> throw (tyErr patTys)
+      | otherwise -> do
+          locals <- checkPatterns _clauseName (zip patTys _clausePatterns)
+          let bodyTy' =
+                substitution
+                  ( fmap
+                      (TypeIden . TypeIdenVariable)
+                      (locals ^. localTyMap)
+                  )
+                  bodyTy
+          _clauseBody' <-
+            runReader locals (checkExpression bodyTy' _clauseBody)
+          return
+            FunctionClause
+              { _clauseBody = _clauseBody',
+                ..
+              }
  where
-    tyErr :: [Type] -> TypeCheckerError
+    tyErr :: [FunctionArgType] -> TypeCheckerError
    tyErr patTys =
      ErrTooManyPatterns
        ( TooManyPatterns
@ -184,39 +256,104 @@ checkFunctionClause info clause@FunctionClause {..} = do
        )

 checkPatterns ::
-  Members '[Reader InfoTable, Output TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
  FunctionName ->
-  [Type] ->
-  [Pattern] ->
-  Sem r (Either TypeCheckerError LocalVars)
-checkPatterns name ctorTys ctorPs =
-  runError @TypeCheckerError (mconcat <$> zipWithM (checkPattern name) ctorTys ctorPs)
+  [(FunctionArgType, Pattern)] ->
+  Sem r LocalVars
+checkPatterns name = execState emptyLocalVars . go
+  where
+    go ::
+      Members '[Error TypeCheckerError, Reader InfoTable, State LocalVars] r =>
+      [(FunctionArgType, Pattern)] ->
+      Sem r ()
+    go = mapM_ (uncurry (checkPattern name))
+
+typeOfArg :: FunctionArgType -> Type
+typeOfArg a = case a of
+  FunctionArgTypeAbstraction {} -> TypeUniverse
+  FunctionArgTypeType ty -> ty
+
+substitutionArg :: VarName -> VarName -> FunctionArgType -> FunctionArgType
+substitutionArg from v a = case a of
+  FunctionArgTypeAbstraction {} -> a
+  FunctionArgTypeType ty ->
+    FunctionArgTypeType
+      (substitution1 (from, TypeIden (TypeIdenVariable v)) ty)
+
+substitution1 :: (VarName, Type) -> Type -> Type
+substitution1 = substitution . uncurry HashMap.singleton
+
+substitution :: HashMap VarName Type -> Type -> Type
+substitution m = go
+  where
+    go :: Type -> Type
+    go = \case
+      TypeIden i -> goIden i
+      TypeApp a -> TypeApp (goApp a)
+      TypeAbs a -> TypeAbs (goAbs a)
+      TypeFunction f -> TypeFunction (goFunction f)
+      TypeUniverse -> TypeUniverse
+      TypeAny -> TypeAny
+    goApp :: TypeApplication -> TypeApplication
+    goApp (TypeApplication l r) = TypeApplication (go l) (go r)
+    goAbs :: TypeAbstraction -> TypeAbstraction
+    goAbs (TypeAbstraction v b) = TypeAbstraction v (go b)
+    goFunction :: Function -> Function
+    goFunction (Function l r) = Function (go l) (go r)
+    goIden :: TypeIden -> Type
+    goIden i = case i of
+      TypeIdenInductive {} -> TypeIden i
+      TypeIdenAxiom {} -> TypeIden i
+      TypeIdenVariable v -> case HashMap.lookup v m of
+        Just ty -> ty
+        Nothing -> TypeIden i
+
+substituteIndParams :: [(InductiveParameter, Type)] -> Type -> Type
+substituteIndParams = substitution . HashMap.fromList . map (first (^. inductiveParamName))

 checkPattern ::
  forall r.
-  Members '[Reader InfoTable, Output TypeCheckerError, Error TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars] r =>
  FunctionName ->
-  Type ->
+  FunctionArgType ->
  Pattern ->
-  Sem r LocalVars
-checkPattern funName type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
+  Sem r ()
+checkPattern funName type_ pat = go type_ pat
  where
-    go :: Type -> Pattern -> Sem r [(VarName, Type)]
-    go ty p = case p of
-      PatternWildcard -> return []
-      PatternVariable v -> return [(v, ty)]
-      PatternConstructorApp a -> do
-        info <- lookupConstructor (a ^. constrAppConstructor)
-        let inductiveTy = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
-        when (inductiveTy /= ty) (output (ErrWrongConstructorType (WrongConstructorType (a ^. constrAppConstructor) ty inductiveTy funName)))
-        goConstr a
+    go :: FunctionArgType -> Pattern -> Sem r ()
+    go argTy p = do
+      tyVarMap <- fmap (TypeIden . TypeIdenVariable) . (^. localTyMap) <$> get
+      let ty = substitution tyVarMap (typeOfArg argTy)
+      case p of
+        PatternWildcard -> return ()
+        PatternVariable v -> do
+          modify (addType v ty)
+          case argTy of
+            FunctionArgTypeAbstraction v' -> do
+              modify (over localTyMap (HashMap.insert v' v))
+            _ -> return ()
+        PatternConstructorApp a -> do
+          (ind, tyArgs) <- checkSaturatedInductive ty
+          info <- lookupConstructor (a ^. constrAppConstructor)
+          let constrInd = info ^. constructorInfoInductive
+          when
+            (ind /= constrInd)
+            ( throw
+                ( ErrWrongConstructorType
+                    (WrongConstructorType (a ^. constrAppConstructor) ind constrInd funName)
+                )
+            )
+          goConstr a tyArgs
      where
-        goConstr :: ConstructorApp -> Sem r [(VarName, Type)]
-        goConstr app@(ConstructorApp c ps) = do
-          tys <- (^. constructorInfoArgs) <$> lookupConstructor c
-          when (length tys /= length ps) (throw (appErr app tys))
-          concat <$> zipWithM go tys ps
-        appErr :: ConstructorApp -> [Type] -> TypeCheckerError
+        goConstr :: ConstructorApp -> [(InductiveParameter, Type)] -> Sem r ()
+        goConstr app@(ConstructorApp c ps) ctx = do
+          (_, psTys) <- constructorArgTypes <$> lookupConstructor c
+          let psTys' = map (substituteIndParams ctx) psTys
+              expectedNum = length psTys
+          let w = map FunctionArgTypeType psTys'
+          when (expectedNum /= length ps) (throw (appErr app w))
+          zipWithM_ go w ps
+        appErr :: ConstructorApp -> [FunctionArgType] -> TypeCheckerError
        appErr app tys =
          ErrWrongConstructorAppArgs
            ( WrongConstructorAppArgs
@ -225,24 +362,37 @@ checkPattern funName type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
                  _wrongCtorAppName = funName
                }
            )
+    checkSaturatedInductive :: Type -> Sem r (InductiveName, [(InductiveParameter, Type)])
+    checkSaturatedInductive t = do
+      (ind, args) <- viewInductiveApp t
+      params <-
+        (^. inductiveInfoDef . inductiveParameters)
+          <$> lookupInductive ind
+      let numArgs = length args
+          numParams = length params
+      when (numArgs < numParams) (error "unsaturated inductive type")
+      when (numArgs > numParams) (error "too many arguments to inductive type")
+      return (ind, zip params args)

-- TODO currently equivalent to id
-normalizeType :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Type
-normalizeType t = case t of
-  TypeAny -> return TypeAny
-  TypeUniverse -> return TypeUniverse
-  TypeFunction f -> TypeFunction <$> normalizeFunction f
-  TypeIden i -> normalizeIden i
+-- | The expression is assumed to be of type TypeUniverse.
+-- If the assumption holds, it should never fail.
+expressionAsType :: Expression -> Type
+expressionAsType = go
  where
-    normalizeIden :: TypeIden -> Sem r Type
-    normalizeIden i = case i of
-      TypeIdenInductive {} -> return (TypeIden i)
-      TypeIdenAxiom {} -> return (TypeIden i)
-    normalizeFunction :: Function -> Sem r Function
-    normalizeFunction (Function l r) = do
-      l' <- normalizeType l
-      r' <- normalizeType r
-      return (Function l' r')
+    go = \case
+      ExpressionIden i -> TypeIden (goIden i)
+      ExpressionApplication a -> TypeApp (goApp a)
+      ExpressionLiteral {} -> impossible
+      ExpressionTyped e -> go (e ^. typedExpression)
+    goIden :: Iden -> TypeIden
+    goIden = \case
+      IdenFunction {} -> impossible
+      IdenConstructor {} -> impossible
+      IdenVar v -> TypeIdenVariable v
+      IdenAxiom a -> TypeIdenAxiom a
+      IdenInductive i -> TypeIdenInductive i
+    goApp :: Application -> TypeApplication
+    goApp (Application l r) = TypeApplication (go l) (go r)

 inferExpression' ::
  forall r.
@ -252,7 +402,7 @@ inferExpression' ::
 inferExpression' e = case e of
  ExpressionIden i -> inferIden i
  ExpressionApplication a -> inferApplication a
-  ExpressionTyped {} -> impossible
+  ExpressionTyped t -> return t
  ExpressionLiteral l -> goLiteral l
  where
    goLiteral :: LiteralLoc -> Sem r TypedExpression
@ -271,26 +421,51 @@ inferExpression' e = case e of
      IdenAxiom v -> do
        info <- lookupAxiom v
        return (TypedExpression (info ^. axiomInfoType) (ExpressionIden i))
+      IdenInductive v -> do
+        info <- lookupInductive v
+        let ps = info ^. inductiveInfoDef . inductiveParameters
+            kind =
+              foldr
+                (\p k -> TypeAbs (TypeAbstraction (p ^. inductiveParamName) k))
+                TypeUniverse
+                ps
+        return (TypedExpression kind (ExpressionIden i))
    inferApplication :: Application -> Sem r TypedExpression
    inferApplication a = do
      let leftExp = a ^. appLeft
      l <- inferExpression' leftExp
      fun <- getFunctionType leftExp (l ^. typedType)
-      r <- checkExpression (fun ^. funLeft) (a ^. appRight)
-      return
-        TypedExpression
-          { _typedExpression =
-              ExpressionApplication
-                Application
-                  { _appLeft = ExpressionTyped l,
-                    _appRight = r
-                  },
-            _typedType = fun ^. funRight
-          }
+      case fun of
+        Left ta -> do
+          r <- checkExpression TypeUniverse (a ^. appRight)
+          let tr = expressionAsType r
+          return
+            TypedExpression
+              { _typedExpression =
+                  ExpressionApplication
+                    Application
+                      { _appLeft = ExpressionTyped l,
+                        _appRight = r
+                      },
+                _typedType = substitution1 (ta ^. typeAbsVar, tr) (ta ^. typeAbsBody)
+              }
+        Right f -> do
+          r <- checkExpression (f ^. funLeft) (a ^. appRight)
+          return
+            TypedExpression
+              { _typedExpression =
+                  ExpressionApplication
+                    Application
+                      { _appLeft = ExpressionTyped l,
+                        _appRight = r
+                      },
+                _typedType = f ^. funRight
+              }
      where
-        getFunctionType :: Expression -> Type -> Sem r Function
+        getFunctionType :: Expression -> Type -> Sem r (Either TypeAbstraction Function)
        getFunctionType appExp t = case t of
-          TypeFunction f -> return f
+          TypeFunction f -> return (Right f)
+          TypeAbs f -> return (Left f)
          _ -> throw tyErr
          where
            tyErr :: TypeCheckerError
@ -302,3 +477,23 @@ inferExpression' e = case e of
                      _expectedFunctionTypeType = t
                    }
                )
+
+viewInductiveApp ::
+  Member (Error TypeCheckerError) r =>
+  Type ->
+  Sem r (InductiveName, [Type])
+viewInductiveApp ty = case t of
+  TypeIden (TypeIdenInductive n) -> return (n, as)
+  _ -> throw @TypeCheckerError (error "only inductive types can be pattern matched")
+  where
+    (t, as) = viewTypeApp ty
+
+viewTypeApp :: Type -> (Type, [Type])
+viewTypeApp t = case t of
+  TypeApp (TypeApplication l r) ->
+    second (`snoc` r) (viewTypeApp l)
+  TypeAny {} -> (t, [])
+  TypeUniverse {} -> (t, [])
+  TypeAbs {} -> (t, [])
+  TypeFunction {} -> (t, [])
+  TypeIden {} -> (t, [])
--- a/src/MiniJuvix/Syntax/MiniHaskell/MiniHaskellResult.hs
+++ b/src/MiniJuvix/Syntax/MiniHaskell/MiniHaskellResult.hs
@ -1,11 +1,11 @@
 module MiniJuvix.Syntax.MiniHaskell.MiniHaskellResult where

 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
 import MiniJuvix.Syntax.MiniHaskell.Language
+import MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult qualified as Mono

 data MiniHaskellResult = MiniHaskellResult
-  { _resultMicroJuvixTyped :: Micro.MicroJuvixTypedResult,
+  { _resultMonoJuvix :: Mono.MonoJuvixResult,
    _resultModules :: NonEmpty Module
  }

--- a/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs
@ -0,0 +1,58 @@
+module MiniJuvix.Syntax.MonoJuvix.InfoTable where
+
+import Data.HashMap.Strict qualified as HashMap
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.MonoJuvix.Language
+
+data ConstructorInfo = ConstructorInfo
+  { _constructorInfoArgs :: [Type],
+    _constructorInfoInductive :: InductiveName
+  }
+
+newtype FunctionInfo = FunctionInfo
+  { _functionInfoType :: Type
+  }
+
+data AxiomInfo = AxiomInfo
+  { _axiomInfoType :: Type,
+    _axiomInfoBackends :: [BackendItem]
+  }
+
+data InfoTable = InfoTable
+  { _infoConstructors :: HashMap Name ConstructorInfo,
+    _infoAxioms :: HashMap Name AxiomInfo,
+    _infoFunctions :: HashMap Name FunctionInfo
+  }
+
+-- TODO temporary function.
+buildTable :: Module -> InfoTable
+buildTable m = InfoTable {..}
+  where
+    _infoConstructors :: HashMap Name ConstructorInfo
+    _infoConstructors =
+      HashMap.fromList
+        [ (c ^. constructorName, ConstructorInfo args ind)
+          | StatementInductive d <- ss,
+            let ind = d ^. inductiveName,
+            c <- d ^. inductiveConstructors,
+            let args = c ^. constructorParameters
+        ]
+    _infoFunctions :: HashMap Name FunctionInfo
+    _infoFunctions =
+      HashMap.fromList
+        [ (f ^. funDefName, FunctionInfo (f ^. funDefType))
+          | StatementFunction f <- ss
+        ]
+    _infoAxioms :: HashMap Name AxiomInfo
+    _infoAxioms =
+      HashMap.fromList
+        [ (d ^. axiomName, AxiomInfo (d ^. axiomType) (d ^. axiomBackendItems))
+          | StatementAxiom d <- ss
+        ]
+    ss = m ^. (moduleBody . moduleStatements)
+
+makeLenses ''InfoTable
+makeLenses ''FunctionInfo
+makeLenses ''ConstructorInfo
+makeLenses ''AxiomInfo
--- a/src/MiniJuvix/Syntax/MonoJuvix/Language.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Language.hs
@ -0,0 +1,195 @@
+module MiniJuvix.Syntax.MonoJuvix.Language
+  ( module MiniJuvix.Syntax.MonoJuvix.Language,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name,
+  )
+where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.Concrete.Language qualified as C
+import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.ForeignBlock
+import Prettyprinter
+
+type FunctionName = Name
+
+type AxiomName = Name
+
+type VarName = Name
+
+type ConstrName = Name
+
+type InductiveName = Name
+
+data Name = Name
+  { _nameText :: Text,
+    _nameId :: NameId,
+    _nameKind :: NameKind,
+    _nameDefined :: Maybe C.Interval,
+    _nameLoc :: Maybe C.Interval
+  }
+  deriving stock (Show)
+
+makeLenses ''Name
+
+instance Eq Name where
+  (==) = (==) `on` _nameId
+
+instance Ord Name where
+  compare = compare `on` _nameId
+
+instance Hashable Name where
+  hashWithSalt salt = hashWithSalt salt . _nameId
+
+instance HasNameKind Name where
+  getNameKind = _nameKind
+
+instance Pretty Name where
+  pretty = pretty . _nameText
+
+data Module = Module
+  { _moduleName :: Name,
+    _moduleBody :: ModuleBody
+  }
+
+newtype ModuleBody = ModuleBody
+  { _moduleStatements :: [Statement]
+  }
+
+data Statement
+  = StatementInductive InductiveDef
+  | StatementFunction FunctionDef
+  | StatementForeign ForeignBlock
+  | StatementAxiom AxiomDef
+
+data AxiomDef = AxiomDef
+  { _axiomName :: AxiomName,
+    _axiomType :: Type,
+    _axiomBackendItems :: [BackendItem]
+  }
+
+data FunctionDef = FunctionDef
+  { _funDefName :: FunctionName,
+    _funDefType :: Type,
+    _funDefClauses :: NonEmpty FunctionClause
+  }
+
+data FunctionClause = FunctionClause
+  { _clauseName :: FunctionName,
+    _clausePatterns :: [Pattern],
+    _clauseBody :: Expression
+  }
+  deriving stock (Show)
+
+data Iden
+  = IdenFunction Name
+  | IdenConstructor Name
+  | IdenVar VarName
+  | IdenAxiom Name
+  deriving stock (Show)
+
+data TypedExpression = TypedExpression
+  { _typedType :: Type,
+    _typedExpression :: Expression
+  }
+  deriving stock (Show)
+
+data Expression
+  = ExpressionIden Iden
+  | ExpressionApplication Application
+  | ExpressionLiteral C.LiteralLoc
+  | ExpressionTyped TypedExpression
+  deriving stock (Show)
+
+data Application = Application
+  { _appLeft :: Expression,
+    _appRight :: Expression
+  }
+  deriving stock (Show)
+
+data Function = Function
+  { _funLeft :: Type,
+    _funRight :: Type
+  }
+  deriving stock (Show, Eq)
+
+-- | Fully applied constructor in a pattern.
+data ConstructorApp = ConstructorApp
+  { _constrAppConstructor :: Name,
+    _constrAppParameters :: [Pattern]
+  }
+  deriving stock (Show)
+
+data Pattern
+  = PatternVariable VarName
+  | PatternConstructorApp ConstructorApp
+  | PatternWildcard
+  deriving stock (Show)
+
+data InductiveDef = InductiveDef
+  { _inductiveName :: InductiveName,
+    _inductiveConstructors :: [InductiveConstructorDef]
+  }
+
+data InductiveConstructorDef = InductiveConstructorDef
+  { _constructorName :: ConstrName,
+    _constructorParameters :: [Type]
+  }
+
+data TypeIden
+  = TypeIdenInductive InductiveName
+  | TypeIdenAxiom AxiomName
+  deriving stock (Show, Eq)
+
+data Type
+  = TypeIden TypeIden
+  | TypeFunction Function
+  | TypeUniverse
+  | TypeAny
+  deriving stock (Show, Eq)
+
+makeLenses ''Module
+makeLenses ''Function
+makeLenses ''FunctionDef
+makeLenses ''FunctionClause
+makeLenses ''InductiveDef
+makeLenses ''AxiomDef
+makeLenses ''ModuleBody
+makeLenses ''Application
+makeLenses ''TypedExpression
+makeLenses ''InductiveConstructorDef
+makeLenses ''ConstructorApp
+
+instance HasAtomicity Application where
+  atomicity = const (Aggregate appFixity)
+
+instance HasAtomicity Expression where
+  atomicity e = case e of
+    ExpressionIden {} -> Atom
+    ExpressionApplication a -> atomicity a
+    ExpressionTyped t -> atomicity (t ^. typedExpression)
+    ExpressionLiteral l -> atomicity l
+
+instance HasAtomicity Function where
+  atomicity = const (Aggregate funFixity)
+
+instance HasAtomicity Type where
+  atomicity t = case t of
+    TypeIden {} -> Atom
+    TypeFunction f -> atomicity f
+    TypeUniverse -> Atom
+    TypeAny -> Atom
+
+instance HasAtomicity ConstructorApp where
+  atomicity (ConstructorApp _ args)
+    | null args = Atom
+    | otherwise = Aggregate appFixity
+
+instance HasAtomicity Pattern where
+  atomicity p = case p of
+    PatternConstructorApp a -> atomicity a
+    PatternVariable {} -> Atom
+    PatternWildcard {} -> Atom
--- a/src/MiniJuvix/Syntax/MonoJuvix/LocalVars.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/LocalVars.hs
@ -0,0 +1,11 @@
+module MiniJuvix.Syntax.MonoJuvix.LocalVars where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MonoJuvix.Language
+
+newtype LocalVars = LocalVars
+  { _localTypes :: HashMap VarName Type
+  }
+  deriving newtype (Semigroup, Monoid)
+
+makeLenses ''LocalVars
--- a/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs
@ -0,0 +1,17 @@
+module MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult
+  ( module MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult,
+    module MiniJuvix.Syntax.MonoJuvix.InfoTable,
+  )
+where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
+import MiniJuvix.Syntax.MonoJuvix.InfoTable
+import MiniJuvix.Syntax.MonoJuvix.Language
+
+data MonoJuvixResult = MonoJuvixResult
+  { _resultMicroTyped :: Micro.MicroJuvixTypedResult,
+    _resultModules :: NonEmpty Module
+  }
+
+makeLenses ''MonoJuvixResult
--- a/src/MiniJuvix/Syntax/MonoJuvix/Pretty.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Pretty.hs
@ -0,0 +1,21 @@
+module MiniJuvix.Syntax.MonoJuvix.Pretty where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
+import MiniJuvix.Syntax.MonoJuvix.Pretty.Ann
+import MiniJuvix.Syntax.MonoJuvix.Pretty.Ansi qualified as Ansi
+import MiniJuvix.Syntax.MonoJuvix.Pretty.Base
+
+newtype PPOutput = PPOutput (SimpleDocStream Ann)
+
+ppOut :: PrettyCode c => c -> PPOutput
+ppOut = PPOutput . docStream defaultOptions
+
+ppOut' :: PrettyCode c => Options -> c -> PPOutput
+ppOut' o = PPOutput . docStream o
+
+instance HasAnsiBackend PPOutput where
+  toAnsi (PPOutput o) = reAnnotateS Ansi.stylize o
+
+instance HasTextBackend PPOutput where
+  toText (PPOutput o) = unAnnotateS o
--- a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Ann.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Ann.hs
@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MonoJuvix.Pretty.Ann where
+
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+
+data Ann
+  = AnnKind NameKind
+  | AnnKeyword
+  | AnnLiteralString
+  | AnnLiteralInteger
--- a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Ansi.hs
@ -0,0 +1,31 @@
+module MiniJuvix.Syntax.MonoJuvix.Pretty.Ansi where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MonoJuvix.Language
+import MiniJuvix.Syntax.MonoJuvix.Pretty.Ann
+import MiniJuvix.Syntax.MonoJuvix.Pretty.Base
+import Prettyprinter
+import Prettyprinter.Render.Terminal
+
+printPrettyCodeDefault :: PrettyCode c => c -> IO ()
+printPrettyCodeDefault = printPrettyCode defaultOptions
+
+printPrettyCode :: PrettyCode c => Options -> c -> IO ()
+printPrettyCode = hPrintPrettyCode stdout
+
+hPrintPrettyCode :: PrettyCode c => Handle -> Options -> c -> IO ()
+hPrintPrettyCode h opts = renderIO h . docStream' opts
+
+renderPrettyCode :: PrettyCode c => Options -> c -> Text
+renderPrettyCode opts = renderStrict . docStream' opts
+
+docStream' :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
+docStream' opts =
+  reAnnotateS stylize . docStream opts
+
+stylize :: Ann -> AnsiStyle
+stylize a = case a of
+  AnnKind k -> nameKindAnsi k
+  AnnKeyword -> colorDull Blue
+  AnnLiteralString -> colorDull Red
+  AnnLiteralInteger -> colorDull Cyan
--- a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
@ -0,0 +1,279 @@
+module MiniJuvix.Syntax.MonoJuvix.Pretty.Base where
+
+import MiniJuvix.Internal.Strings qualified as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.ForeignBlock
+import MiniJuvix.Syntax.MonoJuvix.Language
+import MiniJuvix.Syntax.MonoJuvix.Pretty.Ann
+import Prettyprinter
+
+newtype Options = Options
+  { _optIndent :: Int
+  }
+
+defaultOptions :: Options
+defaultOptions =
+  Options
+    { _optIndent = 2
+    }
+
+docStream :: PrettyCode c => Options -> c -> SimpleDocStream Ann
+docStream opts =
+  layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
+
+class PrettyCode c where
+  ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
+
+runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
+runPrettyCode opts = run . runReader opts . ppCode
+
+instance PrettyCode Name where
+  ppCode n =
+    return $
+      annotate (AnnKind (n ^. nameKind)) $
+        pretty (n ^. nameText) <> "_" <> pretty (n ^. nameId)
+
+instance PrettyCode Iden where
+  ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
+  ppCode i = case i of
+    IdenFunction na -> ppCode na
+    IdenConstructor na -> ppCode na
+    IdenVar na -> ppCode na
+    IdenAxiom a -> ppCode a
+
+instance PrettyCode Application where
+  ppCode a = do
+    l' <- ppLeftExpression appFixity (a ^. appLeft)
+    r' <- ppRightExpression appFixity (a ^. appRight)
+    return $ l' <+> r'
+
+instance PrettyCode TypedExpression where
+  ppCode e = ppCode (e ^. typedExpression)
+
+instance PrettyCode Expression where
+  ppCode = \case
+    ExpressionIden i -> ppCode i
+    ExpressionApplication a -> ppCode a
+    ExpressionTyped a -> ppCode a
+    ExpressionLiteral l -> return (pretty l)
+
+keyword :: Text -> Doc Ann
+keyword = annotate AnnKeyword . pretty
+
+kwArrow :: Doc Ann
+kwArrow = keyword Str.toAscii
+
+kwMapsto :: Doc Ann
+kwMapsto = keyword Str.mapstoUnicode
+
+kwForeign :: Doc Ann
+kwForeign = keyword Str.foreign_
+
+kwAgda :: Doc Ann
+kwAgda = keyword Str.agda
+
+kwGhc :: Doc Ann
+kwGhc = keyword Str.ghc
+
+kwColon :: Doc Ann
+kwColon = keyword Str.colon
+
+kwData :: Doc Ann
+kwData = keyword Str.data_
+
+kwEquals :: Doc Ann
+kwEquals = keyword Str.equal
+
+kwColonColon :: Doc Ann
+kwColonColon = keyword (Str.colon <> Str.colon)
+
+kwPipe :: Doc Ann
+kwPipe = keyword Str.pipe
+
+kwAxiom :: Doc Ann
+kwAxiom = keyword Str.axiom
+
+kwWhere :: Doc Ann
+kwWhere = keyword Str.where_
+
+kwModule :: Doc Ann
+kwModule = keyword Str.module_
+
+kwAny :: Doc Ann
+kwAny = keyword Str.any
+
+kwType :: Doc Ann
+kwType = keyword Str.type_
+
+kwWildcard :: Doc Ann
+kwWildcard = keyword Str.underscore
+
+instance PrettyCode BackendItem where
+  ppCode BackendItem {..} = do
+    backend <- ppCode _backendItemBackend
+    return $
+      backend <+> kwMapsto <+> pretty _backendItemCode
+
+instance PrettyCode Function where
+  ppCode (Function l r) = do
+    l' <- ppLeftExpression funFixity l
+    r' <- ppRightExpression funFixity r
+    return $ l' <+> kwArrow <+> r'
+
+instance PrettyCode TypeIden where
+  ppCode = \case
+    TypeIdenInductive i -> ppCode i
+    TypeIdenAxiom i -> ppCode i
+
+instance PrettyCode Type where
+  ppCode = \case
+    TypeIden i -> ppCode i
+    TypeFunction f -> ppCode f
+    TypeUniverse -> return kwType
+    TypeAny -> return kwAny
+
+instance PrettyCode InductiveConstructorDef where
+  ppCode c = do
+    constructorName' <- ppCode (c ^. constructorName)
+    constructorParameters' <- mapM ppCode (c ^. constructorParameters)
+    return (hsep $ constructorName' : constructorParameters')
+
+indent' :: Member (Reader Options) r => Doc a -> Sem r (Doc a)
+indent' d = do
+  i <- asks _optIndent
+  return $ indent i d
+
+ppBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
+ppBlock items = mapM ppCode items >>= bracesIndent . vsep . toList
+
+bracesIndent :: Members '[Reader Options] r => Doc Ann -> Sem r (Doc Ann)
+bracesIndent d = do
+  d' <- indent' d
+  return $ braces (line <> d' <> line)
+
+instance PrettyCode InductiveDef where
+  ppCode d = do
+    inductiveName' <- ppCode (d ^. inductiveName)
+    inductiveConstructors' <- mapM ppCode (d ^. inductiveConstructors)
+    rhs <- indent' $ align $ concatWith (\a b -> a <> line <> kwPipe <+> b) inductiveConstructors'
+    return $ kwData <+> inductiveName' <+> kwEquals <> line <> rhs
+
+instance PrettyCode ConstructorApp where
+  ppCode c = do
+    constr' <- ppCode (c ^. constrAppConstructor)
+    params' <- mapM ppCodeAtom (c ^. constrAppParameters)
+    return $ hsep $ constr' : params'
+
+instance PrettyCode Pattern where
+  ppCode p = case p of
+    PatternVariable v -> ppCode v
+    PatternConstructorApp a -> ppCode a
+    PatternWildcard -> return kwWildcard
+
+instance PrettyCode FunctionDef where
+  ppCode f = do
+    funDefName' <- ppCode (f ^. funDefName)
+    funDefType' <- ppCode (f ^. funDefType)
+    clauses' <- mapM ppCode (f ^. funDefClauses)
+    return $
+      funDefName' <+> kwColonColon <+> funDefType' <> line
+        <> vsep (toList clauses')
+
+instance PrettyCode FunctionClause where
+  ppCode c = do
+    funName <- ppCode (c ^. clauseName)
+    clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+    clauseBody' <- ppCode (c ^. clauseBody)
+    return $ funName <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+
+instance PrettyCode Backend where
+  ppCode = \case
+    BackendGhc -> return kwGhc
+    BackendAgda -> return kwAgda
+
+instance PrettyCode ForeignBlock where
+  ppCode ForeignBlock {..} = do
+    _foreignBackend' <- ppCode _foreignBackend
+    return $
+      kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode
+        <> line
+        <> rbrace
+
+instance PrettyCode AxiomDef where
+  ppCode AxiomDef {..} = do
+    axiomName' <- ppCode _axiomName
+    axiomType' <- ppCode _axiomType
+    axiomBackendItems' <- case _axiomBackendItems of
+      [] -> return Nothing
+      bs -> Just <$> ppBlock bs
+    return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType' <+?> axiomBackendItems'
+
+instance PrettyCode Statement where
+  ppCode = \case
+    StatementForeign f -> ppCode f
+    StatementFunction f -> ppCode f
+    StatementInductive f -> ppCode f
+    StatementAxiom f -> ppCode f
+
+instance PrettyCode ModuleBody where
+  ppCode m = do
+    everything <- mapM ppCode (m ^. moduleStatements)
+    return $ vsep2 everything
+    where
+      vsep2 = concatWith (\a b -> a <> line <> line <> b)
+
+instance PrettyCode Module where
+  ppCode m = do
+    name' <- ppCode (m ^. moduleName)
+    body' <- ppCode (m ^. moduleBody)
+    return $
+      kwModule <+> name' <+> kwWhere
+        <> line
+        <> line
+        <> body'
+        <> line
+
+parensCond :: Bool -> Doc Ann -> Doc Ann
+parensCond t d = if t then parens d else d
+
+ppPostExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppPostExpression = ppLRExpression isPostfixAssoc
+
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppRightExpression = ppLRExpression isRightAssoc
+
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppLeftExpression = ppLRExpression isLeftAssoc
+
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppLRExpression associates fixlr e =
+  parensCond (atomParens associates (atomicity e) fixlr)
+    <$> ppCode e
+
+ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
+ppCodeAtom c = do
+  p' <- ppCode c
+  return $ if isAtomic c then p' else parens p'
--- a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Text.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Text.hs
@ -0,0 +1,20 @@
+module MiniJuvix.Syntax.MonoJuvix.Pretty.Text where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MonoJuvix.Pretty.Base
+import Prettyprinter.Render.Text
+
+printPrettyCodeDefault :: PrettyCode c => c -> IO ()
+printPrettyCodeDefault = printPrettyCode defaultOptions
+
+printPrettyCode :: PrettyCode c => Options -> c -> IO ()
+printPrettyCode = hPrintPrettyCode stdout
+
+hPrintPrettyCode :: PrettyCode c => Handle -> Options -> c -> IO ()
+hPrintPrettyCode h opts = renderIO h . docStream opts
+
+renderPrettyCodeDefault :: PrettyCode c => c -> Text
+renderPrettyCodeDefault = renderStrict . docStream defaultOptions
+
+renderPrettyCode :: PrettyCode c => Options -> c -> Text
+renderPrettyCode opts = renderStrict . docStream opts
--- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
+++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
@ -17,19 +17,22 @@ import MiniJuvix.Syntax.Usage qualified as A
 entryMicroJuvix ::
  Abstract.AbstractResult ->
  Sem r MicroJuvixResult
-entryMicroJuvix ares =
+entryMicroJuvix ares = do
+  _resultModules' <- mapM translateModule (ares ^. Abstract.resultModules)
  return
    MicroJuvixResult
      { _resultAbstract = ares,
-        _resultModules = fmap translateModule (ares ^. Abstract.resultModules)
+        _resultModules = _resultModules'
      }

-translateModule :: A.TopModule -> Module
-translateModule m =
-  Module
-    { _moduleName = goTopModuleName (m ^. A.moduleName),
-      _moduleBody = goModuleBody (m ^. A.moduleBody)
-    }
+translateModule :: A.TopModule -> Sem r Module
+translateModule m = do
+  _moduleBody' <- goModuleBody (m ^. A.moduleBody)
+  return
+    Module
+      { _moduleName = goTopModuleName (m ^. A.moduleName),
+        _moduleBody = _moduleBody'
+      }

 goTopModuleName :: A.TopModuleName -> Name
 goTopModuleName = goSymbol . S.topModulePathName
@ -50,94 +53,128 @@ goSymbol s =
 unsupported :: Text -> a
 unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing)

-goImport :: A.TopModule -> ModuleBody
+goImport :: A.TopModule -> Sem r ModuleBody
 goImport m = goModuleBody (m ^. A.moduleBody)

-goModuleBody :: A.ModuleBody -> ModuleBody
-goModuleBody b = ModuleBody (map goStatement (b ^. A.moduleStatements))
+goModuleBody :: A.ModuleBody -> Sem r ModuleBody
+goModuleBody b = ModuleBody <$> mapM goStatement (b ^. A.moduleStatements)

-goStatement :: A.Statement -> Statement
+goStatement :: A.Statement -> Sem r Statement
 goStatement = \case
-  A.StatementAxiom d -> StatementAxiom (goAxiomDef d)
-  A.StatementForeign f -> StatementForeign f
-  A.StatementFunction f -> StatementFunction (goFunctionDef f)
+  A.StatementAxiom d -> StatementAxiom <$> goAxiomDef d
+  A.StatementForeign f -> return (StatementForeign f)
+  A.StatementFunction f -> StatementFunction <$> goFunctionDef f
  A.StatementImport {} -> unsupported "imports"
  A.StatementLocalModule {} -> unsupported "local modules"
-  A.StatementInductive i -> StatementInductive (goInductiveDef i)
+  A.StatementInductive i -> StatementInductive <$> goInductiveDef i

 goTypeIden :: A.Iden -> TypeIden
 goTypeIden i = case i of
  A.IdenFunction {} -> unsupported "functions in types"
  A.IdenConstructor {} -> unsupported "constructors in types"
-  A.IdenVar {} -> unsupported "type variables"
+  A.IdenVar v -> TypeIdenVariable (goSymbol v)
  A.IdenInductive d -> TypeIdenInductive (goName (d ^. A.inductiveRefName))
  A.IdenAxiom a -> TypeIdenAxiom (goName (a ^. A.axiomRefName))

-goAxiomDef :: A.AxiomDef -> AxiomDef
-goAxiomDef a =
-  AxiomDef
-    { _axiomName = goSymbol (a ^. A.axiomName),
-      _axiomType = goType (a ^. A.axiomType),
-      _axiomBackendItems = a ^. A.axiomBackendItems
-    }
+goAxiomDef :: A.AxiomDef -> Sem r AxiomDef
+goAxiomDef a = do
+  _axiomType' <- goType (a ^. A.axiomType)
+  return
+    AxiomDef
+      { _axiomName = goSymbol (a ^. A.axiomName),
+        _axiomType = _axiomType',
+        _axiomBackendItems = a ^. A.axiomBackendItems
+      }

-goFunctionParameter :: A.FunctionParameter -> Type
+goFunctionParameter :: A.FunctionParameter -> Sem r (Either VarName Type)
 goFunctionParameter f = case f ^. A.paramName of
-  Just {} -> unsupported "named function arguments"
-  _ -> case f ^. A.paramUsage of
-    A.UsageOmega -> goType (f ^. A.paramType)
-    _ -> unsupported "usages"
+  Just var
+    | isSmallType (f ^. A.paramType) && isOmegaUsage (f ^. A.paramUsage) -> return (Left (goSymbol var))
+    | otherwise -> unsupported "named function arguments only for small types without usages"
+  Nothing
+    | isOmegaUsage (f ^. A.paramUsage) -> Right <$> goType (f ^. A.paramType)
+    | otherwise -> unsupported "usages"

-goFunction :: A.Function -> Function
-goFunction (A.Function l r) = Function (goFunctionParameter l) (goType r)
+isOmegaUsage :: A.Usage -> Bool
+isOmegaUsage u = case u of
+  A.UsageOmega -> True
+  _ -> False

-goFunctionDef :: A.FunctionDef -> FunctionDef
-goFunctionDef f =
-  FunctionDef
-    { _funDefName = _funDefName',
-      _funDefType = goType (f ^. A.funDefTypeSig),
-      _funDefClauses = fmap (goFunctionClause _funDefName') (f ^. A.funDefClauses)
-    }
+goFunction :: A.Function -> Sem r Type
+goFunction (A.Function l r) = do
+  l' <- goFunctionParameter l
+  r' <- goType r
+  return $ case l' of
+    Left tyvar -> TypeAbs (TypeAbstraction tyvar r')
+    Right ty -> TypeFunction (Function ty r')
+
+goFunctionDef :: A.FunctionDef -> Sem r FunctionDef
+goFunctionDef f = do
+  _funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. A.funDefClauses)
+  _funDefType' <- goType (f ^. A.funDefTypeSig)
+  return
+    FunctionDef
+      { _funDefName = _funDefName',
+        _funDefType = _funDefType',
+        _funDefClauses = _funDefClauses'
+      }
  where
    _funDefName' :: Name
    _funDefName' = goSymbol (f ^. A.funDefName)

-goFunctionClause :: Name -> A.FunctionClause -> FunctionClause
-goFunctionClause n c =
-  FunctionClause
-    { _clauseName = n,
-      _clausePatterns = map goPattern (c ^. A.clausePatterns),
-      _clauseBody = goExpression (c ^. A.clauseBody)
-    }
+goFunctionClause :: Name -> A.FunctionClause -> Sem r FunctionClause
+goFunctionClause n c = do
+  _clauseBody' <- goExpression (c ^. A.clauseBody)
+  _clausePatterns' <- mapM goPattern (c ^. A.clausePatterns)
+  return
+    FunctionClause
+      { _clauseName = n,
+        _clausePatterns = _clausePatterns',
+        _clauseBody = _clauseBody'
+      }

-goPattern :: A.Pattern -> Pattern
+goPattern :: A.Pattern -> Sem r Pattern
 goPattern p = case p of
-  A.PatternVariable v -> PatternVariable (goSymbol v)
-  A.PatternConstructorApp c -> PatternConstructorApp (goConstructorApp c)
-  A.PatternWildcard -> PatternWildcard
+  A.PatternVariable v -> return (PatternVariable (goSymbol v))
+  A.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c
+  A.PatternWildcard -> return PatternWildcard
  A.PatternEmpty -> unsupported "pattern empty"

-goConstructorApp :: A.ConstructorApp -> ConstructorApp
-goConstructorApp c =
-  ConstructorApp
-    (goName (c ^. A.constrAppConstructor . A.constructorRefName))
-    (map goPattern (c ^. A.constrAppParameters))
+goConstructorApp :: A.ConstructorApp -> Sem r ConstructorApp
+goConstructorApp c = do
+  _constrAppParameters' <- mapM goPattern (c ^. A.constrAppParameters)
+  return
+    ConstructorApp
+      { _constrAppConstructor = goName (c ^. A.constrAppConstructor . A.constructorRefName),
+        _constrAppParameters = _constrAppParameters'
+      }
+
+isSmallType :: A.Expression -> Bool
+isSmallType e = case e of
+  A.ExpressionUniverse u -> isSmallUni u
+  _ -> False
+
+isSmallUni :: Universe -> Bool
+isSmallUni u = 0 == fromMaybe 0 (u ^. universeLevel)

 goTypeUniverse :: Universe -> Type
 goTypeUniverse u
-  | 0 == fromMaybe 0 (u ^. universeLevel) = TypeUniverse
+  | isSmallUni u = TypeUniverse
  | otherwise = unsupported "big universes"

-goType :: A.Expression -> Type
+goType :: A.Expression -> Sem r Type
 goType e = case e of
-  A.ExpressionIden i -> TypeIden (goTypeIden i)
-  A.ExpressionUniverse u -> goTypeUniverse u
-  A.ExpressionApplication {} -> unsupported "application in types"
-  A.ExpressionFunction f -> TypeFunction (goFunction f)
+  A.ExpressionIden i -> return (TypeIden (goTypeIden i))
+  A.ExpressionUniverse u -> return (goTypeUniverse u)
+  A.ExpressionApplication a -> TypeApp <$> goTypeApplication a
+  A.ExpressionFunction f -> goFunction f
  A.ExpressionLiteral {} -> unsupported "literals in types"

-goApplication :: A.Application -> Application
-goApplication (A.Application f x) = Application (goExpression f) (goExpression x)
+goApplication :: A.Application -> Sem r Application
+goApplication (A.Application f x) = do
+  f' <- goExpression f
+  x' <- goExpression x
+  return (Application f' x')

 goIden :: A.Iden -> Iden
 goIden i = case i of
@ -145,45 +182,78 @@ goIden i = case i of
  A.IdenConstructor c -> IdenConstructor (goName (c ^. A.constructorRefName))
  A.IdenVar v -> IdenVar (goSymbol v)
  A.IdenAxiom a -> IdenAxiom (goName (a ^. A.axiomRefName))
-  A.IdenInductive {} -> unsupported "inductive identifier"
+  A.IdenInductive a -> IdenInductive (goName (a ^. A.inductiveRefName))

-goExpression :: A.Expression -> Expression
+goExpression :: A.Expression -> Sem r Expression
 goExpression e = case e of
-  A.ExpressionIden i -> ExpressionIden (goIden i)
+  A.ExpressionIden i -> return (ExpressionIden (goIden i))
  A.ExpressionUniverse {} -> unsupported "universes in expression"
  A.ExpressionFunction {} -> unsupported "function type in expressions"
-  A.ExpressionApplication a -> ExpressionApplication (goApplication a)
-  A.ExpressionLiteral l -> ExpressionLiteral l
+  A.ExpressionApplication a -> ExpressionApplication <$> goApplication a
+  A.ExpressionLiteral l -> return (ExpressionLiteral l)

-goInductiveDef :: A.InductiveDef -> InductiveDef
+goInductiveParameter :: A.FunctionParameter -> Sem r InductiveParameter
+goInductiveParameter f =
+  case (f ^. A.paramName, f ^. A.paramUsage, f ^. A.paramType) of
+    (Just var, A.UsageOmega, A.ExpressionUniverse u)
+      | isSmallUni u ->
+          return
+            InductiveParameter
+              { _inductiveParamName = goSymbol var
+              }
+    (Just {}, _, _) -> unsupported "only type variables of small types are allowed"
+    (Nothing, _, _) -> unsupported "unnamed inductive parameters"
+
+goInductiveDef :: forall r. A.InductiveDef -> Sem r InductiveDef
 goInductiveDef i = case i ^. A.inductiveType of
  Just {} -> unsupported "inductive indices"
-  _ ->
-    InductiveDef
-      { _inductiveName = indName,
-        _inductiveConstructors = map goConstructorDef (i ^. A.inductiveConstructors)
-      }
+  _ -> do
+    _inductiveParameters' <- mapM goInductiveParameter (i ^. A.inductiveParameters)
+    _inductiveConstructors' <- mapM goConstructorDef (i ^. A.inductiveConstructors)
+    return
+      InductiveDef
+        { _inductiveName = indName,
+          _inductiveParameters = _inductiveParameters',
+          _inductiveConstructors = _inductiveConstructors'
+        }
  where
    indName = goSymbol (i ^. A.inductiveName)
-    goConstructorDef :: A.InductiveConstructorDef -> InductiveConstructorDef
-    goConstructorDef c =
-      InductiveConstructorDef
-        { _constructorName = goSymbol (c ^. A.constructorName),
-          _constructorParameters = goConstructorType (c ^. A.constructorType)
-        }
-    goConstructorType :: A.Expression -> [Type]
-    goConstructorType = fst . viewExpressionFunctionType
+    goConstructorDef :: A.InductiveConstructorDef -> Sem r InductiveConstructorDef
+    goConstructorDef c = do
+      _constructorParameters' <- goConstructorType (c ^. A.constructorType)
+      return
+        InductiveConstructorDef
+          { _constructorName = goSymbol (c ^. A.constructorName),
+            _constructorParameters = _constructorParameters'
+          }
+    -- TODO check that the return type corresponds with the inductive type
+    goConstructorType :: A.Expression -> Sem r [Type]
+    goConstructorType = fmap fst . viewConstructorType

-- TODO: add docs or an example
-viewExpressionFunctionType :: A.Expression -> ([Type], Type)
-viewExpressionFunctionType e = case e of
-  A.ExpressionFunction f -> first toList (viewFunctionType f)
-  A.ExpressionIden i -> ([], TypeIden (goTypeIden i))
-  A.ExpressionApplication {} -> unsupported "application in a type"
-  A.ExpressionUniverse {} -> ([], TypeUniverse)
+goTypeApplication :: A.Application -> Sem r TypeApplication
+goTypeApplication (A.Application l r) = do
+  l' <- goType l
+  r' <- goType r
+  return
+    TypeApplication
+      { _typeAppLeft = l',
+        _typeAppRight = r'
+      }
+
+viewConstructorType :: A.Expression -> Sem r ([Type], Type)
+viewConstructorType e = case e of
+  A.ExpressionFunction f -> first toList <$> viewFunctionType f
+  A.ExpressionIden i -> return ([], TypeIden (goTypeIden i))
+  A.ExpressionApplication a -> do
+    a' <- goTypeApplication a
+    return ([], TypeApp a')
+  A.ExpressionUniverse {} -> return ([], TypeUniverse)
  A.ExpressionLiteral {} -> unsupported "literal in a type"
-
-viewFunctionType :: A.Function -> (NonEmpty Type, Type)
-viewFunctionType (A.Function p r) = (goFunctionParameter p :| args, ret)
  where
-    (args, ret) = viewExpressionFunctionType r
+    viewFunctionType :: A.Function -> Sem r (NonEmpty Type, Type)
+    viewFunctionType (A.Function p r) = do
+      (args, ret) <- viewConstructorType r
+      p' <- goFunctionParameter p
+      return $ case p' of
+        Left {} -> unsupported "type abstraction in constructor type"
+        Right ty -> (ty :| args, ret)
--- a/src/MiniJuvix/Translation/MicroJuvixToMiniHaskell.hs
+++ b/src/MiniJuvix/Translation/MicroJuvixToMiniHaskell.hs
@ -1,29 +1,27 @@
-module MiniJuvix.Translation.MicroJuvixToMiniHaskell
-  ( module MiniJuvix.Translation.MicroJuvixToMiniHaskell,
-    module MiniJuvix.Syntax.MiniHaskell.MiniHaskellResult,
+module MiniJuvix.Translation.MicroJuvixToMonoJuvix
+  ( module MiniJuvix.Translation.MicroJuvixToMonoJuvix,
+    module MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult,
  )
 where

 import Data.Text qualified as Text
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Backends
-import MiniJuvix.Syntax.ForeignBlock
 import MiniJuvix.Syntax.MicroJuvix.InfoTable qualified as Micro
 import MiniJuvix.Syntax.MicroJuvix.Language qualified as Micro
 import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro
-import MiniJuvix.Syntax.MiniHaskell.Language
-import MiniJuvix.Syntax.MiniHaskell.MiniHaskellResult
-import Prettyprinter
+import MiniJuvix.Syntax.MonoJuvix.Language
+import MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult
+import MiniJuvix.Syntax.NameId

-entryMiniHaskell ::
+entryMonoJuvix ::
  Member (Error Err) r =>
  Micro.MicroJuvixTypedResult ->
-  Sem r MiniHaskellResult
-entryMiniHaskell i = do
+  Sem r MonoJuvixResult
+entryMonoJuvix i = do
  _resultModules <- mapM goModule' (i ^. Micro.resultModules)
-  return MiniHaskellResult {..}
+  return MonoJuvixResult {..}
  where
-    _resultMicroJuvixTyped = i
+    _resultMicroTyped = i
    goModule' m = runReader table (goModule m)
      where
        table = Micro.buildTable m
@ -52,53 +50,46 @@ goModuleBody ::
  Micro.ModuleBody ->
  Sem r ModuleBody
 goModuleBody Micro.ModuleBody {..} =
-  ModuleBody <$> mapMaybeM goStatement _moduleStatements
+  ModuleBody <$> mapM goStatement _moduleStatements

-goStatement :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.Statement -> Sem r (Maybe Statement)
+goStatement :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.Statement -> Sem r Statement
 goStatement = \case
-  Micro.StatementInductive d -> Just . StatementInductive <$> goInductive d
-  Micro.StatementFunction d -> Just . StatementFunction <$> goFunctionDef d
-  Micro.StatementForeign d -> return (goForeign d)
-  Micro.StatementAxiom {} -> return Nothing
+  Micro.StatementInductive d -> StatementInductive <$> goInductive d
+  Micro.StatementFunction d -> StatementFunction <$> goFunctionDef d
+  Micro.StatementForeign d -> return (StatementForeign d)
+  Micro.StatementAxiom a -> StatementAxiom <$> goAxiomDef a

-goForeign :: ForeignBlock -> Maybe Statement
-goForeign b = case b ^. foreignBackend of
-  BackendGhc -> Just (StatementVerbatim (b ^. foreignCode))
-  _ -> Nothing
+goAxiomDef :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.AxiomDef -> Sem r AxiomDef
+goAxiomDef Micro.AxiomDef {..} = do
+  _axiomType' <- goType _axiomType
+  return
+    AxiomDef
+      { _axiomName = goName _axiomName,
+        _axiomType = _axiomType',
+        _axiomBackendItems = _axiomBackendItems
+      }

 lookupAxiom :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.Name -> Sem r Micro.AxiomInfo
 lookupAxiom n =
  fromMaybe impossible . (^. Micro.infoAxioms . at n) <$> ask

-goIden :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.Iden -> Sem r Expression
+goIden :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.Iden -> Sem r Iden
 goIden = \case
-  Micro.IdenFunction fun -> return (goName' fun)
-  Micro.IdenConstructor c -> return (goName' c)
-  Micro.IdenVar v -> return (goName' v)
-  Micro.IdenAxiom a -> ExpressionVerbatim <$> goAxiomIden a
+  Micro.IdenFunction fun -> return (IdenFunction (goName fun))
+  Micro.IdenConstructor c -> return (IdenConstructor (goName c))
+  Micro.IdenVar v -> return (IdenVar (goName v))
+  Micro.IdenAxiom a -> return (IdenAxiom (goName a))

 throwErr :: Member (Error Err) r => Text -> Sem r a
 throwErr = throw

-goAxiomIden :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.Name -> Sem r Text
-goAxiomIden n = do
-  backends <- (^. Micro.axiomInfoBackends) <$> lookupAxiom n
-  case firstJust getCode backends of
-    Nothing -> throwErr ("ghc does not support this primitive:" <> show (pretty n))
-    Just t -> return t
-  where
-    getCode :: BackendItem -> Maybe Text
-    getCode b =
-      guard (BackendGhc == b ^. backendItemBackend)
-        $> b ^. backendItemCode
-
-goName' :: Micro.Name -> Expression
-goName' = ExpressionIden . goName
-
 goName :: Micro.Name -> Name
 goName n =
  Name
    { _nameText = goNameText n,
+      _nameId = n ^. Micro.nameId,
+      _nameDefined = Just (n ^. Micro.nameDefined),
+      _nameLoc = Just (n ^. Micro.nameLoc),
      _nameKind = n ^. Micro.nameKind
    }

@ -168,7 +159,7 @@ goExpression ::
  Micro.Expression ->
  Sem r Expression
 goExpression = \case
-  Micro.ExpressionIden i -> goIden i
+  Micro.ExpressionIden i -> ExpressionIden <$> goIden i
  Micro.ExpressionTyped t -> goExpression (t ^. Micro.typedExpression)
  Micro.ExpressionApplication a -> ExpressionApplication <$> goApplication a
  Micro.ExpressionLiteral l -> return (ExpressionLiteral l)
@ -196,6 +187,7 @@ goFunctionClause Micro.FunctionClause {..} = do
  return
    FunctionClause
      { _clauseBody = _clauseBody',
+        _clauseName = goName _clauseName,
        _clausePatterns = _clausePatterns'
      }

@ -236,11 +228,11 @@ goFunction Micro.Function {..} = do
 goTypeIden :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.TypeIden -> Sem r Type
 goTypeIden = \case
  Micro.TypeIdenInductive n -> return (TypeIden (TypeIdenInductive (goName n)))
-  Micro.TypeIdenAxiom n -> TypeVerbatim <$> goAxiomIden n
+  Micro.TypeIdenAxiom n -> return (TypeIden (TypeIdenAxiom (goName n)))

 goType :: Members '[Error Err, Reader Micro.InfoTable] r => Micro.Type -> Sem r Type
 goType = \case
  Micro.TypeIden t -> goTypeIden t
  Micro.TypeFunction f -> TypeFunction <$> goFunction f
-  Micro.TypeUniverse -> throwErr "MiniHaskell: universes in types not supported"
+  Micro.TypeUniverse -> throwErr "MonoJuvix: universes in types not supported"
  Micro.TypeAny -> impossible
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniHaskell.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniHaskell.hs
@ -0,0 +1,246 @@
+module MiniJuvix.Translation.MonoJuvixToMiniHaskell
+  ( module MiniJuvix.Translation.MonoJuvixToMiniHaskell,
+    module MiniJuvix.Syntax.MiniHaskell.MiniHaskellResult,
+  )
+where
+
+import Data.Text qualified as Text
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.ForeignBlock
+import MiniJuvix.Syntax.MiniHaskell.Language
+import MiniJuvix.Syntax.MiniHaskell.MiniHaskellResult
+import MiniJuvix.Syntax.MonoJuvix.InfoTable qualified as Mono
+import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
+import MiniJuvix.Syntax.MonoJuvix.MonoJuvixResult qualified as Mono
+import Prettyprinter
+
+entryMiniHaskell ::
+  Member (Error Err) r =>
+  Mono.MonoJuvixResult ->
+  Sem r MiniHaskellResult
+entryMiniHaskell i = do
+  _resultModules <- mapM goModule' (i ^. Mono.resultModules)
+  return MiniHaskellResult {..}
+  where
+    _resultMonoJuvix = i
+    goModule' m = runReader table (goModule m)
+      where
+        table = Mono.buildTable m
+
+translateModule :: Mono.Module -> Either Err Module
+translateModule m = run (runError (runReader table (goModule m)))
+  where
+    table = Mono.buildTable m
+
+type Err = Text
+
+goModule :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Module -> Sem r Module
+goModule Mono.Module {..} = do
+  _moduleBody' <- goModuleBody _moduleBody
+  return
+    Module
+      { _moduleName = goName _moduleName,
+        _moduleBody = _moduleBody'
+      }
+
+unsupported :: Text -> a
+unsupported msg = error $ msg <> " not yet supported"
+
+goModuleBody ::
+  Members '[Error Err, Reader Mono.InfoTable] r =>
+  Mono.ModuleBody ->
+  Sem r ModuleBody
+goModuleBody Mono.ModuleBody {..} =
+  ModuleBody <$> mapMaybeM goStatement _moduleStatements
+
+goStatement :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Statement -> Sem r (Maybe Statement)
+goStatement = \case
+  Mono.StatementInductive d -> Just . StatementInductive <$> goInductive d
+  Mono.StatementFunction d -> Just . StatementFunction <$> goFunctionDef d
+  Mono.StatementForeign d -> return (goForeign d)
+  Mono.StatementAxiom {} -> return Nothing
+
+goForeign :: ForeignBlock -> Maybe Statement
+goForeign b = case b ^. foreignBackend of
+  BackendGhc -> Just (StatementVerbatim (b ^. foreignCode))
+  _ -> Nothing
+
+lookupAxiom :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Name -> Sem r Mono.AxiomInfo
+lookupAxiom n =
+  fromMaybe impossible . (^. Mono.infoAxioms . at n) <$> ask
+
+goIden :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Iden -> Sem r Expression
+goIden = \case
+  Mono.IdenFunction fun -> return (goName' fun)
+  Mono.IdenConstructor c -> return (goName' c)
+  Mono.IdenVar v -> return (goName' v)
+  Mono.IdenAxiom a -> ExpressionVerbatim <$> goAxiomIden a
+
+throwErr :: Member (Error Err) r => Text -> Sem r a
+throwErr = throw
+
+goAxiomIden :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Name -> Sem r Text
+goAxiomIden n = do
+  backends <- (^. Mono.axiomInfoBackends) <$> lookupAxiom n
+  case firstJust getCode backends of
+    Nothing -> throwErr ("ghc does not support this primitive:" <> show (pretty n))
+    Just t -> return t
+  where
+    getCode :: BackendItem -> Maybe Text
+    getCode b =
+      guard (BackendGhc == b ^. backendItemBackend)
+        $> b ^. backendItemCode
+
+goName' :: Mono.Name -> Expression
+goName' = ExpressionIden . goName
+
+goName :: Mono.Name -> Name
+goName n =
+  Name
+    { _nameText = goNameText n,
+      _nameKind = n ^. Mono.nameKind
+    }
+
+goNameText :: Mono.Name -> Text
+goNameText n =
+  adaptFirstLetter lexeme <> nameTextSuffix
+  where
+    lexeme
+      | Text.null lexeme' = "v"
+      | otherwise = lexeme'
+      where
+        lexeme' = Text.filter isValidChar (n ^. Mono.nameText)
+    isValidChar :: Char -> Bool
+    isValidChar c = isLetter c && isAscii c
+    adaptFirstLetter :: Text -> Text
+    adaptFirstLetter t = case Text.uncons t of
+      Nothing -> impossible
+      Just (h, r) -> Text.cons (capitalize h) r
+      where
+        capitalize :: Char -> Char
+        capitalize
+          | capital = toUpper
+          | otherwise = toLower
+        capital = case n ^. Mono.nameKind of
+          KNameConstructor -> True
+          KNameInductive -> True
+          KNameTopModule -> True
+          KNameLocalModule -> True
+          _ -> False
+    nameTextSuffix :: Text
+    nameTextSuffix = case n ^. Mono.nameKind of
+      KNameTopModule -> mempty
+      KNameFunction ->
+        if n ^. Mono.nameText == haskellMainName then mempty else idSuffix
+      _ -> idSuffix
+    idSuffix :: Text
+    idSuffix = "_" <> show (n ^. Mono.nameId . unNameId)
+    haskellMainName :: Text
+    haskellMainName = "main"
+
+goFunctionDef :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.FunctionDef -> Sem r FunctionDef
+goFunctionDef Mono.FunctionDef {..} = do
+  _funDefType' <- goType _funDefType
+  _funDefClauses' <- mapM goFunctionClause _funDefClauses
+  return
+    FunctionDef
+      { _funDefName = goName _funDefName,
+        _funDefType = _funDefType',
+        _funDefClauses = _funDefClauses'
+      }
+
+goPattern :: Mono.Pattern -> Pattern
+goPattern = \case
+  Mono.PatternVariable v -> PatternVariable (goName v)
+  Mono.PatternConstructorApp a -> PatternConstructorApp (goConstructorApp a)
+  Mono.PatternWildcard -> PatternWildcard
+
+goConstructorApp :: Mono.ConstructorApp -> ConstructorApp
+goConstructorApp c =
+  ConstructorApp
+    { _constrAppConstructor = goName (c ^. Mono.constrAppConstructor),
+      _constrAppParameters = map goPattern (c ^. Mono.constrAppParameters)
+    }
+
+goExpression ::
+  Members '[Error Err, Reader Mono.InfoTable] r =>
+  Mono.Expression ->
+  Sem r Expression
+goExpression = \case
+  Mono.ExpressionIden i -> goIden i
+  Mono.ExpressionTyped t -> goExpression (t ^. Mono.typedExpression)
+  Mono.ExpressionApplication a -> ExpressionApplication <$> goApplication a
+  Mono.ExpressionLiteral l -> return (ExpressionLiteral l)
+
+goApplication ::
+  Members '[Error Err, Reader Mono.InfoTable] r =>
+  Mono.Application ->
+  Sem r Application
+goApplication Mono.Application {..} = do
+  _appLeft' <- goExpression _appLeft
+  _appRight' <- goExpression _appRight
+  return
+    Application
+      { _appLeft = _appLeft',
+        _appRight = _appRight'
+      }
+
+goFunctionClause ::
+  Members '[Error Err, Reader Mono.InfoTable] r =>
+  Mono.FunctionClause ->
+  Sem r FunctionClause
+goFunctionClause Mono.FunctionClause {..} = do
+  _clauseBody' <- goExpression _clauseBody
+  let _clausePatterns' = map goPattern _clausePatterns
+  return
+    FunctionClause
+      { _clauseBody = _clauseBody',
+        _clausePatterns = _clausePatterns'
+      }
+
+goInductive ::
+  Members '[Error Err, Reader Mono.InfoTable] r =>
+  Mono.InductiveDef ->
+  Sem r InductiveDef
+goInductive Mono.InductiveDef {..} = do
+  _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
+  return
+    InductiveDef
+      { _inductiveName = goName _inductiveName,
+        _inductiveConstructors = _inductiveConstructors'
+      }
+
+goConstructorDef ::
+  Members '[Error Err, Reader Mono.InfoTable] r =>
+  Mono.InductiveConstructorDef ->
+  Sem r InductiveConstructorDef
+goConstructorDef Mono.InductiveConstructorDef {..} = do
+  _constructorParameters' <- mapM goType _constructorParameters
+  return
+    InductiveConstructorDef
+      { _constructorName = goName _constructorName,
+        _constructorParameters = _constructorParameters'
+      }
+
+goFunction :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Function -> Sem r Function
+goFunction Mono.Function {..} = do
+  _funLeft' <- goType _funLeft
+  _funRight' <- goType _funRight
+  return
+    Function
+      { _funLeft = _funLeft',
+        _funRight = _funRight'
+      }
+
+goTypeIden :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.TypeIden -> Sem r Type
+goTypeIden = \case
+  Mono.TypeIdenInductive n -> return (TypeIden (TypeIdenInductive (goName n)))
+  Mono.TypeIdenAxiom n -> TypeVerbatim <$> goAxiomIden n
+
+goType :: Members '[Error Err, Reader Mono.InfoTable] r => Mono.Type -> Sem r Type
+goType = \case
+  Mono.TypeIden t -> goTypeIden t
+  Mono.TypeFunction f -> TypeFunction <$> goFunction f
+  Mono.TypeUniverse -> throwErr "MiniHaskell: universes in types not supported"
+  Mono.TypeAny -> impossible
--- a/test/TypeCheck.hs
+++ b/test/TypeCheck.hs
@ -5,4 +5,4 @@ import TypeCheck.Negative qualified as N
 import TypeCheck.Positive qualified as P

 allTests :: TestTree
-allTests = testGroup "TypeCheck tests" [P.allTests, N.allTests]
+allTests = testGroup "Type checker tests" [P.allTests, N.allTests]
--- a/test/TypeCheck/Negative.hs
+++ b/test/TypeCheck/Negative.hs
@ -2,6 +2,7 @@ module TypeCheck.Negative (allTests) where

 import Base
 import MiniJuvix.Pipeline
+import MiniJuvix.Prelude.Error as Error
 import MiniJuvix.Syntax.MicroJuvix.Error

 type FailMsg = String
@ -10,7 +11,7 @@ data NegTest = NegTest
  { _name :: String,
    _relDir :: FilePath,
    _file :: FilePath,
-    _checkErr :: TypeCheckerErrors -> Maybe FailMsg
+    _checkErr :: TypeCheckerError -> Maybe FailMsg
  }

 testDescr :: NegTest -> TestDescr
@ -21,14 +22,12 @@ testDescr NegTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = EntryPoint "." (pure _file)
-
            result <- runIOEither (upToMicroJuvixTyped entryPoint)
-            let msg1 = "The type checker did not find an error."
-            let msg2 = "An error ocurred but it was not in the type checker."
-            case mapLeft fromAJuvixError result of
-              Left (Just err) -> whenJust (_checkErr err) assertFailure
-              Left Nothing -> assertFailure msg1
-              Right _ -> assertFailure msg2
+            case result of
+              Left err -> case fromAJuvixError err of
+                Just tyError -> whenJust (_checkErr tyError) assertFailure
+                Nothing -> assertFailure ("The type checker did not find an error.\nThere is another error:\n" <> unpack (Error.renderText err))
+              Right _ -> assertFailure "An error ocurred but it was not in the type checker."
        }

 allTests :: TestTree
@ -50,48 +49,48 @@ tests =
      "MicroJuvix"
      "PatternConstructor.mjuvix"
      $ \case
-        (TypeCheckerErrors (ErrWrongConstructorType {} :| [])) -> Nothing
+        ErrWrongConstructorType {} -> Nothing
        _ -> wrongError,
    NegTest
      "Constructor pattern length mismatch"
      "MicroJuvix"
      "PatternConstructorApp.mjuvix"
      $ \case
-        (TypeCheckerErrors (ErrWrongConstructorAppArgs {} :| [])) -> Nothing
+        ErrWrongConstructorAppArgs {} -> Nothing
        _ -> wrongError,
    NegTest
      "Type vs inferred type mismatch"
      "MicroJuvix"
      "WrongType.mjuvix"
      $ \case
-        (TypeCheckerErrors (ErrWrongType {} :| [])) -> Nothing
+        ErrWrongType {} -> Nothing
        _ -> wrongError,
    NegTest
      "Function application with non-function type"
      "MicroJuvix"
      "ExpectedFunctionType.mjuvix"
      $ \case
-        (TypeCheckerErrors (ErrExpectedFunctionType {} :| [])) -> Nothing
+        ErrExpectedFunctionType {} -> Nothing
        _ -> wrongError,
    NegTest
      "Function definition clause with two many match patterns"
      "MicroJuvix"
      "TooManyPatterns.mjuvix"
      $ \case
-        (TypeCheckerErrors (ErrTooManyPatterns {} :| [])) -> Nothing
+        ErrTooManyPatterns {} -> Nothing
        _ -> wrongError,
    NegTest
      "Multiple type errors are captured"
      "MicroJuvix"
      "MultiWrongType.mjuvix"
      $ \case
-        (TypeCheckerErrors (ErrWrongType {} :| [ErrWrongType {}])) -> Nothing
+        ErrWrongType {} -> Nothing
        _ -> wrongError,
    NegTest
      "Constructor pattern with arity greater than the constructor"
      "MicroJuvix"
      "WrongConstructorArity.mjuvix"
      $ \case
-        (TypeCheckerErrors (ErrWrongConstructorAppArgs {} :| [])) -> Nothing
+        ErrWrongConstructorAppArgs {} -> Nothing
        _ -> wrongError
  ]
--- a/test/TypeCheck/Positive.hs
+++ b/test/TypeCheck/Positive.hs
@ -62,5 +62,9 @@ tests =
    PosTest
      "Operators"
      "."
-      "Operators.mjuvix"
+      "Operators.mjuvix",
+    PosTest
+      "Polymorphism and higher rank functions"
+      "."
+      "Polymorphism.mjuvix"
  ]
--- a/tests/positive/Polymorphism.mjuvix
+++ b/tests/positive/Polymorphism.mjuvix
@ -0,0 +1,89 @@
+module Polymorphism;
+
+inductive Pair (A : Type) (B : Type) {
+ mkPair : A → B → Pair A B;
+};
+
+inductive Nat {
+ zero : Nat;
+ suc : Nat → Nat;
+};
+
+inductive List (A : Type) {
+ nil : List A;
+ -- TODO check that the return type is saturated with the proper variable
+ cons : A → List A → Nat;
+};
+
+inductive Bool {
+ false : Bool;
+ true : Bool;
+};
+
+id : (A : Type) → A → A;
+id _ a ≔ a;
+
+undefined : (A : Type) → A;
+undefined A ≔ undefined A;
+
+nil' : (E : Type) → List E;
+nil' A ≔ nil A;
+
+-- currying
+nil'' : (E : Type) → List E;
+nil'' ≔ nil;
+
+l1 : List Nat;
+l1 ≔ cons Nat zero (nil Nat);
+
+fst : (A : Type) → (B : Type) → Pair A B → A;
+fst _ _ (mkPair a b) ≔ a;
+
+p : Pair Bool Bool;
+p ≔ mkPair Bool Bool true false;
+
+swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
+swap A B (mkPair a b) ≔ mkPair B A b a;
+
+curry : (A : Type) → (B : Type) → (C : Type)
+  → (Pair A B → C) → A → B → C;
+curry A B C f a b ≔ f (mkPair A B a b) ;
+
+ap : (A : Type) → (B : Type)
+  → (A → B) → A → B;
+ap A B f a ≔ f a;
+
+ite : (A : Type) → Bool → A → A → A;
+ite _ true tt _ ≔ tt;
+ite _ false _ ff ≔ ff;
+
+filter : (A : Type) → (A → Bool) → List A → List A;
+filter A f nil ≔ nil A;
+filter A f (cons x xs) ≔ ite (List A) (f x) (cons A x (filter A f xs)) (filter A f xs);
+
+map : (A : Type) → (B : Type) →
+  (A → B) → List A → List B;
+map A B f nil ≔ nil B ;
+map A B f (cons x xs) ≔ cons B (f x) (map A B f xs);
+
+zip : (A : Type) → (B : Type)
+    → List A → List B → List (Pair A B);
+zip A B nil _ ≔ nil (Pair A B);
+zip A B _ nil ≔ nil (Pair A B);
+zip A B (cons a as) (cons b bs) ≔ nil (Pair A B);
+
+zipWith : (A : Type) → (B : Type) → (C : Type)
+  → (A → B → C)
+  → List A → List B → List C;
+zipWith A B C f nil _ ≔ nil C;
+zipWith A B C f _ nil ≔ nil C;
+zipWith A B C f (cons a as) (cons b bs) ≔ cons C (f a b) (zipWith A B C f as bs);
+
+rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
+rankn f b n ≔ mkPair Bool Nat (f Bool b) (f Nat n);
+
+-- currying
+trankn : Pair Bool Nat;
+trankn ≔ rankn id false zero;
+
+end;