diff --git a/Makefile b/Makefile
index 5422fd76a..faae4800e 100644
--- a/Makefile
+++ b/Makefile
@@ -51,7 +51,13 @@ stan :
 setup:
 	stack build --only-dependencies --jobs $(THREADS)
 
-stack:
+test:
+	stack test --fast --jobs $(THREADS)
+
+install:
+	stack install --fast --jobs $(THREADS)
+
+build:
 	stack build --fast --jobs $(THREADS)
 
 stack-build-watch:
@@ -94,4 +100,4 @@ install-agda2hs:
 .PHONY : agda
 agda :
 	agda2hs ./src/MiniJuvix/Syntax/Core.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
-	agda2hs ./src/MiniJuvix/Syntax/Eval.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
\ No newline at end of file
+	agda2hs ./src/MiniJuvix/Syntax/Eval.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
diff --git a/app/Main.hs b/app/Main.hs
index 35c957902..cbf8f5a18 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -5,7 +5,6 @@ import Control.Monad.Extra
 import qualified MiniJuvix.Syntax.Concrete.Language as M
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
-import qualified MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi as H
 import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro
 import qualified MiniJuvix.Termination as T
 import qualified MiniJuvix.Translation.ScopedToAbstract as A
@@ -239,7 +238,8 @@ go c = do
     MiniHaskell MiniHaskellOptions {..} -> do
       m <- parseModuleIO _mhaskellInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
-      a <- fromRightIO' putStrLn (return $ A.translateModule s)
+      -- a <- fromRightIO' putStrLn (return $ A.translateModule s)
+      fromRightIO' putStrLn (return $ A.translateModule s)
       -- let mini = Micro.translateModule a
       -- Micro.printPrettyCodeDefault mini
       -- TODO
diff --git a/package.yaml b/package.yaml
index d25ad6217..9433245e7 100644
--- a/package.yaml
+++ b/package.yaml
@@ -78,6 +78,7 @@ default-extensions:
 - OverloadedStrings
 - PolyKinds
 - QuasiQuotes
+- RankNTypes
 - RecordWildCards
 - ScopedTypeVariables
 - StandaloneDeriving
diff --git a/src/MiniJuvix/Prelude.hs b/src/MiniJuvix/Prelude.hs
index 7c9d9e49f..4efadf90d 100644
--- a/src/MiniJuvix/Prelude.hs
+++ b/src/MiniJuvix/Prelude.hs
@@ -1,7 +1,8 @@
-module MiniJuvix.Prelude (
-  module MiniJuvix.Prelude.Base,
-  module MiniJuvix.Prelude.Error
-  ) where
+module MiniJuvix.Prelude
+  ( module MiniJuvix.Prelude.Base,
+    module MiniJuvix.Prelude.Error,
+  )
+where
 
 import MiniJuvix.Prelude.Base
 import MiniJuvix.Prelude.Error
diff --git a/src/MiniJuvix/Prelude/Base.hs b/src/MiniJuvix/Prelude/Base.hs
index 17fcc12b6..a0795c826 100644
--- a/src/MiniJuvix/Prelude/Base.hs
+++ b/src/MiniJuvix/Prelude/Base.hs
@@ -2,6 +2,7 @@ module MiniJuvix.Prelude.Base
   ( module MiniJuvix.Prelude.Base,
     module Control.Monad.Extra,
     module Data.Char,
+    module Control.Monad.Fix,
     module Data.Typeable,
     module Data.Either.Extra,
     module Data.Function,
@@ -30,6 +31,7 @@ module MiniJuvix.Prelude.Base
     module Polysemy.Reader,
     module Data.Text.IO,
     module Polysemy.State,
+    module Polysemy.Fixpoint,
     module Polysemy.Error,
     module Polysemy.Embed,
     module Text.Show,
@@ -62,8 +64,8 @@ where
 --------------------------------------------------------------------------------
 
 import Control.Applicative
-import Data.Typeable hiding (TyCon)
 import Control.Monad.Extra
+import Control.Monad.Fix
 import Data.Bool
 import Data.ByteString.Lazy (ByteString)
 import Data.Char
@@ -74,27 +76,28 @@ import Data.Eq
 import Data.Foldable hiding (minimum, minimumBy)
 import Data.Function
 import Data.Functor
-import Prettyprinter (Doc, (<+>))
 import Data.HashMap.Strict (HashMap)
 import Data.HashSet (HashSet)
 import Data.Hashable
 import Data.Int
 import Data.List.Extra hiding (head, last)
-import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, nonEmpty, minimum1, minimumOn1, maximum1, maximumOn1, some1)
 import qualified Data.List.NonEmpty as NonEmpty
+import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, maximum1, maximumOn1, minimum1, minimumOn1, nonEmpty, some1)
 import Data.Maybe
-import Data.Singletons.Sigma
 import Data.Monoid
 import Data.Ord
 import Data.Semigroup (Semigroup, (<>))
 import Data.Singletons
+import Data.Singletons.Sigma
 import Data.Singletons.TH (genSingletons)
 import Data.Stream (Stream)
 import Data.String
 import Data.Text (Text, pack, strip, unpack)
 import Data.Text.Encoding
+import Data.Text.IO
 import Data.Traversable
 import Data.Tuple.Extra
+import Data.Typeable hiding (TyCon)
 import Data.Void
 import Data.Word
 import GHC.Enum
@@ -107,15 +110,16 @@ import Lens.Micro.Platform hiding (both)
 import Polysemy
 import Polysemy.Embed
 import Polysemy.Error hiding (fromEither)
+import Polysemy.Fixpoint
 import Polysemy.Reader
 import Polysemy.State
 import Polysemy.View
+import Prettyprinter (Doc, (<+>))
 import System.Directory
 import System.Exit
 import System.FilePath
-import System.IO hiding (putStr, putStrLn, hPutStr, hPutStrLn, writeFile, hGetContents, interact, readFile, getContents, getLine, appendFile, hGetLine, readFile')
+import System.IO hiding (appendFile, getContents, getLine, hGetContents, hGetLine, hPutStr, hPutStrLn, interact, putStr, putStrLn, readFile, readFile', writeFile)
 import Text.Show (Show)
-import Data.Text.IO
 import qualified Text.Show as Show
 
 --------------------------------------------------------------------------------
@@ -209,16 +213,18 @@ impossible = Err.error "impossible"
 --------------------------------------------------------------------------------
 
 infixl 7 <+?>
+
 (<+?>) :: Doc ann -> Maybe (Doc ann) -> Doc ann
 (<+?>) a = maybe a (a <+>)
 
 infixl 7 <?>
+
 (<?>) :: Semigroup m => m -> Maybe m -> m
 (<?>) a = maybe a (a <>)
 
-data Indexed a = Indexed {
-  _indexedIx :: Int,
-  _indexedThing :: a
+data Indexed a = Indexed
+  { _indexedIx :: Int,
+    _indexedThing :: a
   }
   deriving stock (Show, Eq, Ord, Foldable, Traversable)
 
diff --git a/src/MiniJuvix/Prelude/Error.hs b/src/MiniJuvix/Prelude/Error.hs
index bebae9966..603f8c10a 100644
--- a/src/MiniJuvix/Prelude/Error.hs
+++ b/src/MiniJuvix/Prelude/Error.hs
@@ -9,20 +9,20 @@ data AJuvixError = forall e. JuvixError e => AJuvixError e
 
 -- | Minimal interface of an minijuvix error.
 class Typeable e => JuvixError e where
-   -- | Print the to stderr with Ansi formatting.
-   printErrorAnsi :: e -> IO ()
-   printErrorAnsi = hPutStrLn stderr . renderAnsiText
+  -- | Print the to stderr with Ansi formatting.
+  printErrorAnsi :: e -> IO ()
+  printErrorAnsi = hPutStrLn stderr . renderAnsiText
 
-   -- | Print the to stderr without formatting.
-   printErrorText :: e -> IO ()
-   printErrorText = hPutStrLn stderr . renderText
+  -- | Print the to stderr without formatting.
+  printErrorText :: e -> IO ()
+  printErrorText = hPutStrLn stderr . renderText
 
-   -- | Render the error to Text.
-   renderText :: e -> Text
+  -- | Render the error to Text.
+  renderText :: e -> Text
 
-   -- | Render the error with Ansi formatting (if any).
-   renderAnsiText :: e -> Text
-   renderAnsiText = renderText
+  -- | Render the error with Ansi formatting (if any).
+  renderAnsiText :: e -> Text
+  renderAnsiText = renderText
 
 toAJuvixError :: JuvixError e => e -> AJuvixError
 toAJuvixError = AJuvixError
diff --git a/src/MiniJuvix/Syntax/Abstract/Language.hs b/src/MiniJuvix/Syntax/Abstract/Language.hs
index 3766eb901..2ad1a6478 100644
--- a/src/MiniJuvix/Syntax/Abstract/Language.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Language.hs
@@ -1,11 +1,11 @@
 module MiniJuvix.Syntax.Abstract.Language
   ( module MiniJuvix.Syntax.Abstract.Language,
-    module MiniJuvix.Syntax.Concrete.Language
+    module MiniJuvix.Syntax.Concrete.Language,
   )
 where
 
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language (Usage, Literal(..), ForeignBlock(..))
+import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..), Literal (..), Usage)
 import qualified MiniJuvix.Syntax.Concrete.Name as C
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Fixity
@@ -41,7 +41,7 @@ data ModuleBody = ModuleBody
   { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
     _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
     _moduleImports :: [Indexed TopModule],
-    _moduleForeign :: [Indexed ForeignBlock],
+    _moduleForeigns :: [Indexed ForeignBlock],
     _moduleLocalModules :: HashMap LocalModuleName (Indexed LocalModule)
   }
   deriving stock (Show, Eq)
@@ -60,7 +60,7 @@ data FunctionClause = FunctionClause
   deriving stock (Show, Eq)
 
 data Iden
-  = IdenDefined Name
+  = IdenFunction Name
   | IdenConstructor Name
   | IdenVar VarName
   | IdenInductive Name
diff --git a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
index 001ab200d..f4b2d4c47 100644
--- a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
@@ -1,10 +1,11 @@
-module MiniJuvix.Syntax.Abstract.Language.Extra (
-  module MiniJuvix.Syntax.Abstract.Language,
-  module MiniJuvix.Syntax.Abstract.Language.Extra
-                                       ) where
+module MiniJuvix.Syntax.Abstract.Language.Extra
+  ( module MiniJuvix.Syntax.Abstract.Language,
+    module MiniJuvix.Syntax.Abstract.Language.Extra,
+  )
+where
 
-import MiniJuvix.Syntax.Abstract.Language
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language
 
 smallerPatternVariables :: Pattern -> [VarName]
 smallerPatternVariables p = case p of
@@ -13,15 +14,15 @@ smallerPatternVariables p = case p of
   PatternEmpty {} -> []
   PatternConstructorApp app -> appVariables app
   where
-  appVariables :: ConstructorApp -> [VarName]
-  appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
+    appVariables :: ConstructorApp -> [VarName]
+    appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
 
-  patternVariables :: Pattern -> [VarName]
-  patternVariables pat = case pat of
-    PatternVariable v -> [v]
-    PatternWildcard {} -> []
-    PatternEmpty {} -> []
-    PatternConstructorApp app -> appVariables app
+    patternVariables :: Pattern -> [VarName]
+    patternVariables pat = case pat of
+      PatternVariable v -> [v]
+      PatternWildcard {} -> []
+      PatternEmpty {} -> []
+      PatternConstructorApp app -> appVariables app
 
 viewApp :: Expression -> (Expression, [Expression])
 viewApp e = case e of
@@ -35,18 +36,18 @@ viewApp e = case e of
 viewExpressionAsPattern :: Expression -> Maybe Pattern
 viewExpressionAsPattern e = case viewApp e of
   (f, args)
-   | Just c <- getConstructor f -> do
-        args' <- mapM viewExpressionAsPattern args
-        Just $ PatternConstructorApp (ConstructorApp c args')
+    | Just c <- getConstructor f -> do
+      args' <- mapM viewExpressionAsPattern args
+      Just $ PatternConstructorApp (ConstructorApp c args')
   (f, [])
-   | Just v <- getVariable f -> Just (PatternVariable v)
+    | Just v <- getVariable f -> Just (PatternVariable v)
   _ -> Nothing
   where
-  getConstructor :: Expression -> Maybe Name
-  getConstructor f = case f of
-    ExpressionIden (IdenConstructor n) -> Just n
-    _ -> Nothing
-  getVariable :: Expression -> Maybe VarName
-  getVariable f = case f of
-    ExpressionIden (IdenVar n) -> Just n
-    _ -> Nothing
+    getConstructor :: Expression -> Maybe Name
+    getConstructor f = case f of
+      ExpressionIden (IdenConstructor n) -> Just n
+      _ -> Nothing
+    getVariable :: Expression -> Maybe VarName
+    getVariable f = case f of
+      ExpressionIden (IdenVar n) -> Just n
+      _ -> Nothing
diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty/Ann.hs b/src/MiniJuvix/Syntax/Abstract/Pretty/Ann.hs
index 4177b5f8e..0013c0d72 100644
--- a/src/MiniJuvix/Syntax/Abstract/Pretty/Ann.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Pretty/Ann.hs
@@ -1,12 +1,11 @@
 module MiniJuvix.Syntax.Abstract.Pretty.Ann where
 
-
+import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as S
-import MiniJuvix.Prelude
 
-data Ann =
-  AnnKind S.NameKind
+data Ann
+  = AnnKind S.NameKind
   | AnnKeyword
   | AnnImportant
   | AnnLiteralString
diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/Abstract/Pretty/Ansi.hs
index 19556054f..1c8683250 100644
--- a/src/MiniJuvix/Syntax/Abstract/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Pretty/Ansi.hs
@@ -1,11 +1,12 @@
-module MiniJuvix.Syntax.Abstract.Pretty.Ansi (
-module MiniJuvix.Syntax.Abstract.Pretty.Base,
 module MiniJuvix.Syntax.Abstract.Pretty.Ansi
-                                             ) where
+  ( module MiniJuvix.Syntax.Abstract.Pretty.Base,
+    module MiniJuvix.Syntax.Abstract.Pretty.Ansi,
+  )
+where
 
-import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Abstract.Pretty.Base
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Pretty.Base
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -22,8 +23,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of
diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
index fbe3a709d..2d9b3be4c 100644
--- a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
@@ -1,23 +1,21 @@
-module MiniJuvix.Syntax.Abstract.Pretty.Base (
-  module MiniJuvix.Syntax.Abstract.Pretty.Base,
-  module MiniJuvix.Syntax.Abstract.Pretty.Ann
-                                             ) where
-
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.Usage
-import MiniJuvix.Syntax.Universe
-import Prettyprinter
-import MiniJuvix.Prelude
-
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as S
-import MiniJuvix.Syntax.Abstract.Language
-import MiniJuvix.Syntax.Abstract.Pretty.Ann
+module MiniJuvix.Syntax.Abstract.Pretty.Base
+  ( module MiniJuvix.Syntax.Abstract.Pretty.Base,
+    module MiniJuvix.Syntax.Abstract.Pretty.Ann,
+  )
+where
 
 import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language
+import MiniJuvix.Syntax.Abstract.Pretty.Ann
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as S
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.Universe
+import MiniJuvix.Syntax.Usage
+import Prettyprinter
 
 data Options = Options
-  {
-    _optShowNameId :: Bool,
+  { _optShowNameId :: Bool,
     _optIndent :: Int,
     _optShowDecreasingArgs :: ShowDecrArgs
   }
@@ -25,10 +23,11 @@ data Options = Options
 data ShowDecrArgs = OnlyArg | OnlyRel | ArgRel
 
 toSOptions :: Options -> S.Options
-toSOptions Options {..} = S.defaultOptions {
-  S._optShowNameId = _optShowNameId,
-  S._optIndent = _optIndent
-  }
+toSOptions Options {..} =
+  S.defaultOptions
+    { S._optShowNameId = _optShowNameId,
+      S._optIndent = _optIndent
+    }
 
 class PrettyCode c where
   ppCode :: Members '[Reader Options] r => c -> Sem r (Doc Ann)
@@ -41,8 +40,7 @@ ppSCode c = do
 defaultOptions :: Options
 defaultOptions =
   Options
-    {
-      _optShowNameId = False,
+    { _optShowNameId = False,
       _optIndent = 2,
       _optShowDecreasingArgs = OnlyRel
     }
@@ -55,7 +53,7 @@ runPrettyCode opts = run . runReader opts . ppCode
 
 instance PrettyCode Iden where
   ppCode i = case i of
-    IdenDefined n -> ppSCode n
+    IdenFunction n -> ppSCode n
     IdenConstructor n -> ppSCode n
     IdenInductive n -> ppSCode n
     IdenVar n -> ppSCode n
@@ -101,9 +99,9 @@ kwColonOmega = keyword Str.colonOmegaUnicode
 
 instance PrettyCode Usage where
   ppCode u = return $ case u of
-     UsageNone -> kwColonZero
-     UsageOnce -> kwColonOne
-     UsageOmega -> kwColon
+    UsageNone -> kwColonZero
+    UsageOnce -> kwColonOne
+    UsageOmega -> kwColon
 
 instance PrettyCode FunctionParameter where
   ppCode FunctionParameter {..} = do
@@ -124,24 +122,36 @@ instance PrettyCode Function where
 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 ::
+  (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 ::
+  (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 ::
+  (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 ::
+  (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
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do
diff --git a/src/MiniJuvix/Syntax/Concrete/Base.hs b/src/MiniJuvix/Syntax/Concrete/Base.hs
index 96ac3c9e7..a8c953f01 100644
--- a/src/MiniJuvix/Syntax/Concrete/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Base.hs
@@ -8,8 +8,8 @@ module MiniJuvix.Syntax.Concrete.Base
 where
 
 import Control.Monad.Combinators.Expr
-import Control.Monad.Combinators.NonEmpty (sepBy1, some, sepEndBy1)
+import Control.Monad.Combinators.NonEmpty (sepBy1, sepEndBy1, some)
 import Data.List.NonEmpty (NonEmpty)
 import MiniJuvix.Prelude hiding (some)
-import Text.Megaparsec hiding (sepBy1, some, sepEndBy1)
+import Text.Megaparsec hiding (sepBy1, sepEndBy1, some)
 import Text.Megaparsec.Char
diff --git a/src/MiniJuvix/Syntax/Concrete/Language.hs b/src/MiniJuvix/Syntax/Concrete/Language.hs
index bdf1ffa07..b3e6c8d63 100644
--- a/src/MiniJuvix/Syntax/Concrete/Language.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Language.hs
@@ -1,40 +1,57 @@
 {-# LANGUAGE UndecidableInstances #-}
+
 module MiniJuvix.Syntax.Concrete.Language
   ( module MiniJuvix.Syntax.Concrete.Language,
     module MiniJuvix.Syntax.Concrete.Name,
     module MiniJuvix.Syntax.Concrete.Loc,
     module MiniJuvix.Syntax.Concrete.PublicAnn,
+    module MiniJuvix.Syntax.Concrete.ModuleIsTop,
     module MiniJuvix.Syntax.Concrete.Language.Stage,
     module MiniJuvix.Syntax.Fixity,
     module MiniJuvix.Syntax.Usage,
-    module MiniJuvix.Syntax.Universe
+    module MiniJuvix.Syntax.Universe,
   )
 where
 
 --------------------------------------------------------------------------------
 
 import qualified Data.Kind as GHC
-import MiniJuvix.Syntax.Universe
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.Usage
-import MiniJuvix.Syntax.Concrete.Name
-import MiniJuvix.Syntax.Concrete.Loc
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Prelude hiding (show)
 import MiniJuvix.Syntax.Concrete.Language.Stage
-import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Loc
+import MiniJuvix.Syntax.Concrete.ModuleIsTop
+import MiniJuvix.Syntax.Concrete.Name
+import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.Universe
+import MiniJuvix.Syntax.Usage
+import Prelude (show)
 
 --------------------------------------------------------------------------------
 -- Parsing stages
 --------------------------------------------------------------------------------
+type family RefNameType (c :: S.IsConcrete) :: (res :: GHC.Type) | res -> c where
+  RefNameType 'S.Concrete = S.Name
+  RefNameType 'S.NotConcrete = S.Name' ()
 
 type family SymbolType (s :: Stage) :: (res :: GHC.Type) | res -> s where
   SymbolType 'Parsed = Symbol
   SymbolType 'Scoped = S.Symbol
 
-type family NameType (s :: Stage) :: (res :: GHC.Type) | res -> s where
-  NameType 'Parsed = Name
-  NameType 'Scoped = S.Name
+type family ModuleRefType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+  ModuleRefType 'Parsed = Name
+  ModuleRefType 'Scoped = ModuleRef
+
+type family IdentifierType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+  IdentifierType 'Parsed = Name
+  IdentifierType 'Scoped = ScopedIden
+
+type family PatternAtomIdenType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+  PatternAtomIdenType 'Parsed = Name
+  PatternAtomIdenType 'Scoped = PatternScopedIden
 
 type family ExpressionType (s :: Stage) :: (res :: GHC.Type) | res -> s where
   ExpressionType 'Parsed = ExpressionAtoms 'Parsed
@@ -80,7 +97,8 @@ deriving stock instance
     Show (ModulePathType s 'ModuleLocal),
     Show (PatternType s),
     Show (SymbolType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (ExpressionType s)
   ) =>
   Show (Statement s)
@@ -90,7 +108,8 @@ deriving stock instance
     Eq (PatternType s),
     Eq (ModulePathType s 'ModuleLocal),
     Eq (SymbolType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (ExpressionType s)
   ) =>
   Eq (Statement s)
@@ -100,23 +119,27 @@ deriving stock instance
     Ord (PatternType s),
     Ord (ModulePathType s 'ModuleLocal),
     Ord (SymbolType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (ExpressionType s)
   ) =>
   Ord (Statement s)
 
-data CompileDef (s :: Stage) = CompileDef {
-  _compileAxiom :: SymbolType s,
-  _compileBackend :: Backend,
-  _compileCode :: Text
+data CompileDef (s :: Stage) = CompileDef
+  { _compileAxiom :: SymbolType s,
+    _compileBackend :: Backend,
+    _compileCode :: Text
   }
+
 deriving stock instance (Eq (SymbolType s)) => Eq (CompileDef s)
+
 deriving stock instance (Ord (SymbolType s)) => Ord (CompileDef s)
+
 deriving stock instance (Show (SymbolType s)) => Show (CompileDef s)
 
-data ForeignBlock = ForeignBlock {
-  _foreignBackend :: Backend,
-  _foreignCode :: Text
+data ForeignBlock = ForeignBlock
+  { _foreignBackend :: Backend,
+    _foreignCode :: Text
   }
   deriving stock (Eq, Ord, Show)
 
@@ -228,37 +251,33 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Ind
 --------------------------------------------------------------------------------
 
 data PatternApp = PatternApp
-  {
-    patAppLeft :: Pattern,
+  { patAppLeft :: Pattern,
     patAppRight :: Pattern
   }
   deriving stock (Show, Eq, Ord)
 
-
 data PatternInfixApp = PatternInfixApp
-  {
-    patInfixLeft :: Pattern,
-    patInfixConstructor :: NameType 'Scoped,
+  { patInfixLeft :: Pattern,
+    patInfixConstructor :: ConstructorRef,
     patInfixRight :: Pattern
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternInfixApp where
-  getFixity (PatternInfixApp  _ op _) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (_constructorRefName op ^. S.nameFixity)
 
 data PatternPostfixApp = PatternPostfixApp
-  {
-    patPostfixParameter :: Pattern,
-    patPostfixConstructor :: NameType 'Scoped
+  { patPostfixParameter :: Pattern,
+    patPostfixConstructor :: ConstructorRef
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternPostfixApp where
-  getFixity (PatternPostfixApp  _ op) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PatternPostfixApp _ op) = fromMaybe impossible (_constructorRefName op ^. S.nameFixity)
 
 data Pattern
   = PatternVariable (SymbolType 'Scoped)
-  | PatternConstructor (NameType 'Scoped)
+  | PatternConstructor ConstructorRef
   | PatternApplication PatternApp
   | PatternInfixApplication PatternInfixApp
   | PatternPostfixApplication PatternPostfixApp
@@ -267,7 +286,7 @@ data Pattern
   deriving stock (Show, Eq, Ord)
 
 instance HasAtomicity Pattern where
- atomicity e = case e of
+  atomicity e = case e of
     PatternVariable {} -> Atom
     PatternConstructor {} -> Atom
     PatternApplication {} -> Aggregate appFixity
@@ -280,8 +299,13 @@ instance HasAtomicity Pattern where
 -- Pattern section
 --------------------------------------------------------------------------------
 
+data PatternScopedIden
+  = PatternScopedVar S.Symbol
+  | PatternScopedConstructor ConstructorRef
+  deriving stock (Show, Ord, Eq)
+
 data PatternAtom (s :: Stage)
-  = PatternAtomName (NameType s)
+  = PatternAtomIden (PatternAtomIdenType s)
   | PatternAtomWildcard
   | PatternAtomEmpty
   | PatternAtomParens (PatternAtoms s)
@@ -291,21 +315,24 @@ instance HasAtomicity (PatternAtom 'Parsed) where
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (PatternAtomIdenType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtom s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (PatternAtomIdenType s),
     Eq (PatternType s)
   ) =>
   Eq (PatternAtom s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (PatternAtomIdenType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtom s)
@@ -315,21 +342,24 @@ newtype PatternAtoms (s :: Stage)
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (PatternAtomIdenType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtoms s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (PatternAtomIdenType s),
     Eq (PatternType s)
   ) =>
   Eq (PatternAtoms s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (PatternAtomIdenType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtoms s)
@@ -349,7 +379,8 @@ data FunctionClause (s :: Stage) = FunctionClause
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -357,7 +388,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -365,7 +397,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -375,22 +408,6 @@ deriving stock instance
 -- Module declaration
 --------------------------------------------------------------------------------
 
-data ModuleIsTop = ModuleTop | ModuleLocal
-
--- The following Singleton related definitions could be scrapped if we depended
--- on the singletons-th library.
-data SModuleIsTop (t :: ModuleIsTop) where
-  SModuleTop :: SModuleIsTop 'ModuleTop
-  SModuleLocal :: SModuleIsTop 'ModuleLocal
-
-type instance Sing = SModuleIsTop
-
-instance SingI 'ModuleTop where
-  sing = SModuleTop
-
-instance SingI 'ModuleLocal where
-  sing = SModuleLocal
-
 type LocalModuleName s = SymbolType s
 
 data Module (s :: Stage) (t :: ModuleIsTop) = Module
@@ -404,7 +421,8 @@ deriving stock instance
     Show (ModulePathType s 'ModuleLocal),
     Show (ImportType s),
     Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -415,7 +433,8 @@ deriving stock instance
     Eq (ModulePathType s 'ModuleLocal),
     Eq (ImportType s),
     Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -426,7 +445,8 @@ deriving stock instance
     Ord (ModulePathType s 'ModuleLocal),
     Ord (ImportType s),
     Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -437,31 +457,92 @@ data UsingHiding
   | Hiding (NonEmpty Symbol)
   deriving stock (Show, Eq, Ord)
 
+type ModuleRef = ModuleRef' 'S.Concrete
+
+newtype ModuleRef' (c :: S.IsConcrete) = ModuleRef'
+  { _unModuleRef' :: Σ ModuleIsTop (TyCon1 (ModuleRef'' c))
+  }
+
+-- | TODO can this be derived?
+instance SingI c => Show (ModuleRef' c) where
+  show (ModuleRef' (isTop :&: r)) = case isTop of
+    SModuleLocal -> case sing :: S.SIsConcrete c of
+      S.SConcrete -> show r
+      S.SNotConcrete -> show r
+    SModuleTop -> case sing :: S.SIsConcrete c of
+      S.SConcrete -> show r
+      S.SNotConcrete -> show r
+
+getNameRefId :: forall c. SingI c => RefNameType c -> S.NameId
+getNameRefId = case sing :: S.SIsConcrete c of
+  S.SConcrete -> S._nameId
+  S.SNotConcrete -> S._nameId
+
+getModuleExportInfo :: ModuleRef' c -> ExportInfo
+getModuleExportInfo = projSigma2 _moduleExportInfo . _unModuleRef'
+
+getModuleRefNameType :: ModuleRef' c -> RefNameType c
+getModuleRefNameType = projSigma2 _moduleRefName . _unModuleRef'
+
+instance SingI c => Eq (ModuleRef' c) where
+  (==) = (==) `on` (getNameRefId . getModuleRefNameType)
+
+instance SingI c => Ord (ModuleRef' c) where
+  compare = compare `on` (getNameRefId . getModuleRefNameType)
+
+-- TODO find a better name
+data ModuleRef'' (c :: S.IsConcrete) (t :: ModuleIsTop) = ModuleRef''
+  { _moduleRefName :: RefNameType c,
+    _moduleExportInfo :: ExportInfo,
+    _moduleRefModule :: Module 'Scoped t
+  }
+
+instance Show (RefNameType s) => Show (ModuleRef'' s t) where
+  show = show . _moduleRefName
+
+data SymbolEntry
+  = EntryAxiom (AxiomRef' 'S.NotConcrete)
+  | EntryInductive (InductiveRef' 'S.NotConcrete)
+  | EntryFunction (FunctionRef' 'S.NotConcrete)
+  | EntryConstructor (ConstructorRef' 'S.NotConcrete)
+  | -- | TODO does this ever contain top modules?
+    EntryModule (ModuleRef' 'S.NotConcrete)
+  deriving stock (Show)
+
+-- | Symbols that a module exports
+newtype ExportInfo = ExportInfo
+  { _exportSymbols :: HashMap Symbol SymbolEntry
+  }
+  deriving stock (Show)
+
 data OpenModule (s :: Stage) = OpenModule
-  { openModuleName :: NameType s,
+  { openModuleName :: ModuleRefType s,
     openParameters :: [ExpressionType s],
     openUsingHiding :: Maybe UsingHiding,
     openPublic :: PublicAnn
   }
+
 deriving stock instance
-  (
-    Eq (NameType s),
+  ( Eq (IdentifierType s),
     Eq (SymbolType s),
+    Eq (ModuleRefType s),
     Eq (PatternType s),
     Eq (ExpressionType s)
   ) =>
   Eq (OpenModule s)
+
 deriving stock instance
-  (
-    Ord (NameType s),
+  ( Ord (IdentifierType s),
     Ord (SymbolType s),
     Ord (PatternType s),
+    Ord (ModuleRefType s),
     Ord (ExpressionType s)
   ) =>
   Ord (OpenModule s)
+
 deriving stock instance
-  (
-    Show (NameType s),
+  ( Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (ExpressionType s)
   ) =>
   Show (OpenModule s)
@@ -470,41 +551,105 @@ deriving stock instance
 -- Expression
 --------------------------------------------------------------------------------
 
-data AxiomRef = AxiomRef {
-  _axiomRefName :: NameType 'Scoped,
-  _axiomRefBackends :: HashMap Backend Text
-  }
-  deriving stock (Show, Eq, Ord)
+type AxiomRef = AxiomRef' 'S.Concrete
 
-data InductiveRef = InductiveRef {
-  _inductiveRefName :: NameType 'Scoped,
-  _inductiveRefDef :: InductiveDef 'Scoped
+data AxiomRef' (n :: S.IsConcrete) = AxiomRef'
+  { _axiomRefName :: RefNameType n,
+    _axiomRefType :: Expression,
+    _axiomRefBackends :: HashMap Backend Text
   }
-  deriving stock (Show, Eq, Ord)
 
-data FunctionRef = FunctionRef {
-  _functionRefName :: NameType 'Scoped,
-  _functionRefSig :: Expression
+instance Eq (RefNameType s) => Eq (AxiomRef' s) where
+  (==) = (==) `on` _axiomRefName
+
+instance Ord (RefNameType s) => Ord (AxiomRef' s) where
+  compare = compare `on` _axiomRefName
+
+instance Show (RefNameType s) => Show (AxiomRef' s) where
+  show = show . _axiomRefName
+
+type InductiveRef = InductiveRef' 'S.Concrete
+
+data InductiveRef' (n :: S.IsConcrete) = InductiveRef'
+  { _inductiveRefName :: RefNameType n,
+    _inductiveRefDef :: InductiveDef 'Scoped
   }
-  deriving stock (Show, Eq, Ord)
 
-data ConstructorRef = ConstructorRef {
-  _constructorRefName :: NameType 'Scoped,
-  _constructorSig :: Expression
+instance Eq (RefNameType s) => Eq (InductiveRef' s) where
+  (==) = (==) `on` _inductiveRefName
+
+instance Ord (RefNameType s) => Ord (InductiveRef' s) where
+  compare = compare `on` _inductiveRefName
+
+instance Show (RefNameType s) => Show (InductiveRef' s) where
+  show = show . _inductiveRefName
+
+type FunctionRef = FunctionRef' 'S.Concrete
+
+data FunctionRef' (n :: S.IsConcrete) = FunctionRef'
+  { _functionRefName :: RefNameType n,
+    _functionRefSig :: Expression
   }
-  deriving stock (Show, Eq, Ord)
 
-data ScopedIden =
-  ScopedAxiom AxiomRef
-  | ScopedInductive InductiveRef
-  | ScopedVar (NameType 'Scoped)
-  | ScopedFunction FunctionRef
-  | ScopedConstructor ConstructorRef
-  deriving stock (Show, Eq, Ord)
+instance Eq (RefNameType s) => Eq (FunctionRef' s) where
+  (==) = (==) `on` _functionRefName
+
+instance Ord (RefNameType s) => Ord (FunctionRef' s) where
+  compare = compare `on` _functionRefName
+
+instance Show (RefNameType s) => Show (FunctionRef' s) where
+  show = show . _functionRefName
+
+type ConstructorRef = ConstructorRef' 'S.Concrete
+
+data ConstructorRef' (n :: S.IsConcrete) = ConstructorRef'
+  { _constructorRefName :: RefNameType n,
+    _constructorSig :: Expression
+  }
+
+instance Eq (RefNameType s) => Eq (ConstructorRef' s) where
+  (==) = (==) `on` _constructorRefName
+
+instance Ord (RefNameType s) => Ord (ConstructorRef' s) where
+  compare = compare `on` _constructorRefName
+
+instance Show (RefNameType s) => Show (ConstructorRef' s) where
+  show = show . _constructorRefName
+
+type ScopedIden = ScopedIden' 'S.Concrete
+
+data ScopedIden' (n :: S.IsConcrete)
+  = ScopedAxiom (AxiomRef' n)
+  | ScopedInductive (InductiveRef' n)
+  | ScopedVar S.Symbol
+  | ScopedFunction (FunctionRef' n)
+  | ScopedConstructor (ConstructorRef' n)
+
+deriving stock instance
+  (Eq (RefNameType s)) => Eq (ScopedIden' s)
+
+deriving stock instance
+  (Ord (RefNameType s)) => Ord (ScopedIden' s)
+
+deriving stock instance
+  (Show (RefNameType s)) => Show (ScopedIden' s)
+
+identifierName :: forall n. SingI n => ScopedIden' n -> RefNameType n
+identifierName = \case
+  ScopedAxiom a -> _axiomRefName a
+  ScopedInductive i -> _inductiveRefName i
+  ScopedVar v ->
+    ( case sing :: S.SIsConcrete n of
+        S.SConcrete -> id
+        S.SNotConcrete -> set S.nameConcrete ()
+    )
+      (unqualifiedSymbol v)
+  ScopedFunction f -> _functionRefName f
+  ScopedConstructor c -> _constructorRefName c
 
 data Expression
   = ExpressionIdentifier ScopedIden
-  | ExpressionParensIdentifier (NameType 'Scoped)
+  | ExpressionParensIdentifier ScopedIden
   | ExpressionApplication Application
   | ExpressionInfixApplication InfixApplication
   | ExpressionPostfixApplication PostfixApplication
@@ -522,7 +667,7 @@ instance HasAtomicity Literal where
     LitString {} -> Atom
 
 instance HasAtomicity Expression where
- atomicity e = case e of
+  atomicity e = case e of
     ExpressionIdentifier {} -> Atom
     ExpressionParensIdentifier {} -> Atom
     ExpressionApplication {} -> Aggregate appFixity
@@ -539,14 +684,14 @@ instance HasAtomicity Expression where
 -- Expression atom
 --------------------------------------------------------------------------------
 
-data Literal =
-  LitString Text
+data Literal
+  = LitString Text
   | LitInteger Integer
   deriving stock (Show, Eq, Ord)
 
 -- | Expressions without application
 data ExpressionAtom (s :: Stage)
-  = AtomIdentifier (NameType s)
+  = AtomIdentifier (IdentifierType s)
   | AtomLambda (Lambda s)
   | AtomLetBlock (LetBlock s)
   | AtomUniverse Universe
@@ -558,7 +703,8 @@ data ExpressionAtom (s :: Stage)
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -566,7 +712,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
@@ -574,7 +721,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
@@ -586,14 +734,15 @@ newtype ExpressionAtoms (s :: Stage)
 
 instance HasAtomicity (ExpressionAtoms 'Parsed) where
   atomicity (ExpressionAtoms l) = case l of
-    (_  :| []) -> Atom
-    (_  :| _)
+    (_ :| []) -> Atom
+    (_ :| _)
       | AtomFunArrow `elem` l -> Aggregate funFixity
       | otherwise -> Aggregate appFixity
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -601,7 +750,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
@@ -609,7 +759,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
@@ -702,7 +853,8 @@ newtype WhereBlock (s :: Stage) = WhereBlock
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -710,7 +862,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -718,7 +871,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -731,7 +885,8 @@ data WhereClause (s :: Stage)
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -739,7 +894,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -747,7 +903,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -816,24 +973,22 @@ data Application = Application
 
 data InfixApplication = InfixApplication
   { infixAppLeft :: ExpressionType 'Scoped,
-    infixAppOperator :: NameType 'Scoped,
+    infixAppOperator :: IdentifierType 'Scoped,
     infixAppRight :: ExpressionType 'Scoped
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity InfixApplication where
-  getFixity (InfixApplication  _ op _) = fromMaybe impossible (op ^. S.nameFixity)
-
+  getFixity (InfixApplication _ op _) = fromMaybe impossible (identifierName op ^. S.nameFixity)
 
 data PostfixApplication = PostfixApplication
-  {
-    postfixAppParameter :: ExpressionType 'Scoped,
-    postfixAppOperator :: NameType 'Scoped
+  { postfixAppParameter :: ExpressionType 'Scoped,
+    postfixAppOperator :: IdentifierType 'Scoped
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PostfixApplication where
-  getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PostfixApplication _ op) = fromMaybe impossible (identifierName op ^. S.nameFixity)
 
 --------------------------------------------------------------------------------
 -- Let block expression
@@ -846,7 +1001,8 @@ data LetBlock (s :: Stage) = LetBlock
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -854,7 +1010,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -862,7 +1019,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -874,7 +1032,8 @@ data LetClause (s :: Stage)
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -882,7 +1041,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -890,7 +1050,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -950,3 +1111,45 @@ makeLenses ''FunctionClause
 makeLenses ''InductiveParameter
 makeLenses ''CompileDef
 makeLenses ''ForeignBlock
+makeLenses ''AxiomRef'
+makeLenses ''InductiveRef'
+makeLenses ''ModuleRef'
+makeLenses ''ModuleRef''
+makeLenses ''FunctionRef'
+makeLenses ''ConstructorRef'
+
+idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
+idenOverName f = \case
+  ScopedAxiom a -> ScopedAxiom (over axiomRefName f a)
+  ScopedInductive i -> ScopedInductive (over inductiveRefName f i)
+  ScopedVar v -> ScopedVar (f v)
+  ScopedFunction fun -> ScopedFunction (over functionRefName f fun)
+  ScopedConstructor c -> ScopedConstructor (over constructorRefName f c)
+
+entryPrism :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> (S.Name' (), SymbolEntry)
+entryPrism f = \case
+  EntryAxiom a -> (a ^. axiomRefName, EntryAxiom (over axiomRefName f a))
+  EntryInductive i -> (i ^. inductiveRefName, EntryInductive (over inductiveRefName f i))
+  EntryFunction fun -> (fun ^. functionRefName, EntryFunction (over functionRefName f fun))
+  EntryConstructor c -> (c ^. constructorRefName, EntryConstructor (over constructorRefName f c))
+  EntryModule m -> (getModuleRefNameType m, EntryModule (overModuleRef'' (over moduleRefName f) m))
+
+entryOverName :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> SymbolEntry
+entryOverName f = snd . entryPrism f
+
+entryName :: SymbolEntry -> S.Name' ()
+entryName = fst . entryPrism id
+
+overModuleRef'' :: forall s s'. (forall t. ModuleRef'' s t -> ModuleRef'' s' t) -> ModuleRef' s -> ModuleRef' s'
+overModuleRef'' f = over unModuleRef' (\(t :&: m'') -> t :&: f m'')
+
+symbolEntryToSName :: SymbolEntry -> S.Name' ()
+symbolEntryToSName = \case
+  EntryAxiom a -> a ^. axiomRefName
+  EntryInductive i -> i ^. inductiveRefName
+  EntryFunction f -> f ^. functionRefName
+  EntryConstructor c -> c ^. constructorRefName
+  EntryModule m -> getModuleRefNameType m
+
+instance HasNameKind SymbolEntry where
+  getNameKind = getNameKind . entryName
diff --git a/src/MiniJuvix/Syntax/Concrete/Language/Stage.hs b/src/MiniJuvix/Syntax/Concrete/Language/Stage.hs
index 64d5028e7..3ad649e41 100644
--- a/src/MiniJuvix/Syntax/Concrete/Language/Stage.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Language/Stage.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE StandaloneKindSignatures #-}
+
 module MiniJuvix.Syntax.Concrete.Language.Stage where
 
 import MiniJuvix.Prelude
diff --git a/src/MiniJuvix/Syntax/Concrete/Lexer.hs b/src/MiniJuvix/Syntax/Concrete/Lexer.hs
index 0940668d5..f9d185958 100644
--- a/src/MiniJuvix/Syntax/Concrete/Lexer.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Lexer.hs
@@ -2,14 +2,14 @@ module MiniJuvix.Syntax.Concrete.Lexer where
 
 --------------------------------------------------------------------------------
 
-import GHC.Unicode
-import MiniJuvix.Syntax.Concrete.Base hiding (space, Pos)
-import qualified MiniJuvix.Syntax.Concrete.Base as P
-import MiniJuvix.Prelude
-import qualified Text.Megaparsec.Char.Lexer as L
-import MiniJuvix.Syntax.Concrete.Loc
-import qualified MiniJuvix.Internal.Strings as Str
 import qualified Data.Text as Text
+import GHC.Unicode
+import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Base hiding (Pos, space)
+import qualified MiniJuvix.Syntax.Concrete.Base as P
+import MiniJuvix.Syntax.Concrete.Loc
+import qualified Text.Megaparsec.Char.Lexer as L
 
 --------------------------------------------------------------------------------
 
@@ -45,7 +45,7 @@ integer = do
   nat <- lexeme L.decimal
   case minus of
     Nothing -> return nat
-    _ -> return (- nat)
+    _ -> return (-nat)
 
 -- | TODO allow escaping { inside the string using \{
 bracedString :: MonadParsec e Text m => m Text
@@ -58,11 +58,11 @@ string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
 mkLoc :: SourcePos -> Loc
 mkLoc SourcePos {..} = Loc {..}
   where
-  _locFile = sourceName
-  _locFileLoc = FileLoc {..}
-    where
-    _locLine = fromPos sourceLine
-    _locCol = fromPos sourceColumn
+    _locFile = sourceName
+    _locFileLoc = FileLoc {..}
+      where
+        _locLine = fromPos sourceLine
+        _locCol = fromPos sourceColumn
 
 curLoc :: MonadParsec e Text m => m Loc
 curLoc = mkLoc <$> getSourcePos
@@ -99,9 +99,9 @@ bareIdentifier = interval $ do
           c `elem` extraAllowedChars
         ]
       where
-      extraAllowedChars :: [Char]
-      extraAllowedChars = "_'-*,&"
-      cat = generalCategory c
+        extraAllowedChars :: [Char]
+        extraAllowedChars = "_'-*,&"
+        cat = generalCategory c
 
 dot :: forall e m. MonadParsec e Text m => m Char
 dot = P.char '.'
diff --git a/src/MiniJuvix/Syntax/Concrete/Loc.hs b/src/MiniJuvix/Syntax/Concrete/Loc.hs
index 0810870cd..bb0c5f956 100644
--- a/src/MiniJuvix/Syntax/Concrete/Loc.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Loc.hs
@@ -12,8 +12,8 @@ instance Semigroup Pos where
 instance Monoid Pos where
   mempty = Pos 0
 
-data FileLoc = FileLoc {
-  -- | Line number
+data FileLoc = FileLoc
+  { -- | Line number
     _locLine :: !Pos,
     -- | Column number
     _locCol :: !Pos
@@ -32,10 +32,10 @@ data Loc = Loc
   deriving stock (Show, Eq, Ord)
 
 -- | Inclusive interval
-data Interval = Interval {
-  _intFile :: FilePath,
-  _intStart :: FileLoc,
-  _intEnd :: FileLoc
+data Interval = Interval
+  { _intFile :: FilePath,
+    _intStart :: FileLoc,
+    _intEnd :: FileLoc
   }
   deriving stock (Show, Ord, Eq)
 
@@ -56,7 +56,7 @@ instance Pretty Pos where
 
 instance Pretty FileLoc where
   pretty :: FileLoc -> Doc a
-  pretty FileLoc {..}  =
+  pretty FileLoc {..} =
     pretty _locLine <> colon <> pretty _locCol
 
 instance Pretty Loc where
@@ -68,14 +68,15 @@ instance Pretty Interval where
   pretty :: Interval -> Doc a
   pretty Interval {..} =
     pretty _intFile <> colon
-    <> ppPosRange (_locLine _intStart, _locLine _intEnd) <> colon
-    <> ppPosRange (_locCol _intStart, _locCol _intEnd)
+      <> ppPosRange (_locLine _intStart, _locLine _intEnd)
+      <> colon
+      <> ppPosRange (_locCol _intStart, _locCol _intEnd)
     where
-    hyphen = pretty '-'
-    ppPosRange :: (Pos, Pos) -> Doc a
-    ppPosRange (s, e)
-      | s == e = pretty s
-      | otherwise = pretty s <> hyphen <> pretty e
+      hyphen = pretty '-'
+      ppPosRange :: (Pos, Pos) -> Doc a
+      ppPosRange (s, e)
+        | s == e = pretty s
+        | otherwise = pretty s <> hyphen <> pretty e
 
 makeLenses ''Interval
 makeLenses ''Loc
diff --git a/src/MiniJuvix/Syntax/Concrete/ModuleIsTop.hs b/src/MiniJuvix/Syntax/Concrete/ModuleIsTop.hs
new file mode 100644
index 000000000..c17733c2f
--- /dev/null
+++ b/src/MiniJuvix/Syntax/Concrete/ModuleIsTop.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module MiniJuvix.Syntax.Concrete.ModuleIsTop where
+
+import MiniJuvix.Prelude
+
+data ModuleIsTop = ModuleTop | ModuleLocal
+  deriving stock (Eq, Ord, Show)
+
+$(genSingletons [''ModuleIsTop])
diff --git a/src/MiniJuvix/Syntax/Concrete/Name.hs b/src/MiniJuvix/Syntax/Concrete/Name.hs
index 13e4bd900..6b0c0b4ca 100644
--- a/src/MiniJuvix/Syntax/Concrete/Name.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Name.hs
@@ -1,14 +1,15 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
 module MiniJuvix.Syntax.Concrete.Name where
 
+import qualified Data.List.NonEmpty.Extra as NonEmpty
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Loc
-import qualified Data.List.NonEmpty.Extra as NonEmpty
 import Prettyprinter
 
-data Symbol = Symbol {
-  _symbolText :: Text,
-  _symbolLoc :: Interval
+data Symbol = Symbol
+  { _symbolText :: Text,
+    _symbolLoc :: Interval
   }
   deriving stock (Show)
 
@@ -77,16 +78,16 @@ instance HasLoc TopModulePath where
 topModulePathToFilePath :: FilePath -> TopModulePath -> FilePath
 topModulePathToFilePath = topModulePathToFilePath' (Just ".mjuvix")
 
-topModulePathToFilePath'
-  :: Maybe String -> FilePath -> TopModulePath -> FilePath
+topModulePathToFilePath' ::
+  Maybe String -> FilePath -> TopModulePath -> FilePath
 topModulePathToFilePath' ext root mp = absPath
   where
-  relDirPath = foldr ((</>) . toPath) mempty (_modulePathDir mp)
-  relFilePath = relDirPath </> toPath (_modulePathName mp)
-  absPath = case ext of
-    Nothing -> root </> relFilePath
-    Just e -> root </> relFilePath <.> e
-  toPath :: Symbol -> FilePath
-  toPath Symbol{..} = unpack _symbolText
+    relDirPath = foldr ((</>) . toPath) mempty (_modulePathDir mp)
+    relFilePath = relDirPath </> toPath (_modulePathName mp)
+    absPath = case ext of
+      Nothing -> root </> relFilePath
+      Just e -> root </> relFilePath <.> e
+    toPath :: Symbol -> FilePath
+    toPath Symbol {..} = unpack _symbolText
 
 instance Hashable TopModulePath
diff --git a/src/MiniJuvix/Syntax/Concrete/Parser.hs b/src/MiniJuvix/Syntax/Concrete/Parser.hs
index a589dce5b..ed16effa1 100644
--- a/src/MiniJuvix/Syntax/Concrete/Parser.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs
@@ -6,11 +6,11 @@ import qualified Data.List.NonEmpty.Extra as NonEmpty
 import Data.Singletons
 import qualified Data.Text as Text
 import qualified Data.Text.IO as Text
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Base (MonadParsec)
 import qualified MiniJuvix.Syntax.Concrete.Base as P
 import MiniJuvix.Syntax.Concrete.Language
 import MiniJuvix.Syntax.Concrete.Lexer hiding (symbol)
-import MiniJuvix.Prelude
 
 --------------------------------------------------------------------------------
 -- Running the parser
@@ -147,7 +147,7 @@ import_ = do
 expressionAtom :: MonadParsec e Text m => m (ExpressionAtom 'Parsed)
 expressionAtom =
   do
-     AtomLiteral <$> P.try literal
+    AtomLiteral <$> P.try literal
     <|> AtomIdentifier <$> name
     <|> (AtomUniverse <$> universe)
     <|> (AtomLambda <$> lambda)
@@ -166,8 +166,8 @@ expressionAtoms = ExpressionAtoms <$> P.some expressionAtom
 
 literal :: MonadParsec e Text m => m Literal
 literal =
-      LitInteger <$> integer
-  <|> LitString <$> string
+  LitInteger <$> integer
+    <|> LitString <$> string
 
 --------------------------------------------------------------------------------
 -- Match expression
@@ -319,7 +319,7 @@ lambdaClause = do
 lambda :: MonadParsec e Text m => m (Lambda 'Parsed)
 lambda = do
   kwLambda
-  lambdaClauses ← braces (P.sepEndBy lambdaClause kwSemicolon)
+  lambdaClauses <- braces (P.sepEndBy lambdaClause kwSemicolon)
   return Lambda {..}
 
 -------------------------------------------------------------------------------
@@ -355,7 +355,7 @@ constructorDef = do
 
 patternAtom :: forall e m. MonadParsec e Text m => m (PatternAtom 'Parsed)
 patternAtom =
-  PatternAtomName <$> name
+  PatternAtomIden <$> name
     <|> PatternAtomWildcard <$ kwWildcard
     <|> (PatternAtomParens <$> parens patternAtoms)
 
@@ -421,10 +421,10 @@ openModule = do
   openPublic <- maybe NoPublic (const Public) <$> optional kwPublic
   return OpenModule {..}
   where
-  usingOrHiding :: m UsingHiding
-  usingOrHiding =
-    (kwUsing >> (Using <$> symbolList))
-     <|> (kwHiding >> (Hiding <$> symbolList))
+    usingOrHiding :: m UsingHiding
+    usingOrHiding =
+      (kwUsing >> (Using <$> symbolList))
+        <|> (kwHiding >> (Hiding <$> symbolList))
 
 --------------------------------------------------------------------------------
 -- Debugging statements
diff --git a/src/MiniJuvix/Syntax/Concrete/PublicAnn.hs b/src/MiniJuvix/Syntax/Concrete/PublicAnn.hs
index 7f945891f..e36252fc9 100644
--- a/src/MiniJuvix/Syntax/Concrete/PublicAnn.hs
+++ b/src/MiniJuvix/Syntax/Concrete/PublicAnn.hs
@@ -2,9 +2,9 @@ module MiniJuvix.Syntax.Concrete.PublicAnn where
 
 import MiniJuvix.Prelude
 
-data PublicAnn =
-  -- | Explicit public annotation
-  Public
-  -- | No annotation. Do not confuse this with 'not public' or 'private'.
-  | NoPublic
+data PublicAnn
+  = -- | Explicit public annotation
+    Public
+  | -- | No annotation. Do not confuse this with 'not public' or 'private'.
+    NoPublic
   deriving stock (Show, Eq, Ord)
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs
index 2c35b1ebb..4391a2202 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs
@@ -1,13 +1,14 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Error (
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Types,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty
-  ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Error
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Error.Types,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty,
+  )
+where
 
-import MiniJuvix.Syntax.Concrete.Scoped.Error.Types
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty as P
+import MiniJuvix.Syntax.Concrete.Scoped.Error.Types
 import Prettyprinter
 
 -- | An error that happens during scope checking. Note that it is defined here
@@ -30,8 +31,8 @@ data ScopeError
   | ErrAmbiguousModuleSym AmbiguousModuleSym
   | ErrUnusedOperatorDef UnusedOperatorDef
   | ErrWrongTopModuleName WrongTopModuleName
-  -- | Eventually this needs to go away
-  | ErrGeneric Text
+  | -- | Eventually this needs to go away
+    ErrGeneric Text
   deriving stock (Show)
 
 ppScopeError :: ScopeError -> Doc Eann
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty.hs
index b445cd1d6..fcbdc3fa1 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty.hs
@@ -1,10 +1,10 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty (
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text
-  ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text,
+  )
+where
 
+import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text
-import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi
-
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs
index 66188ec0b..51e1ed0a5 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs
@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi where
 
-import Prettyprinter
 import MiniJuvix.Prelude
-import Prettyprinter.Render.Terminal
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 renderAnsi :: SimpleDocStream Eann -> Text
 renderAnsi = renderStrict . reAnnotateS stylize
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs
index 4f53b305c..1296afaf8 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs
@@ -1,15 +1,16 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base where
 
-import Prettyprinter
+import qualified Data.HashMap.Strict as HashMap
+import qualified Data.HashSet as HashSet
+import qualified Data.List.NonEmpty.Extra as NonEmpty
 import MiniJuvix.Prelude
+import qualified MiniJuvix.Syntax.Concrete.Language as L
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Types
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as P
 import MiniJuvix.Syntax.Concrete.Scoped.Scope
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import Prettyprinter
 import Text.EditDistance
-import qualified Data.HashSet as HashSet
-import qualified Data.HashMap.Strict as HashMap
-import qualified Data.List.NonEmpty.Extra as NonEmpty
 
 data Eann = Highlight
 
@@ -27,8 +28,10 @@ indent' = indent 2
 
 textDistance :: Text -> Text -> Int
 textDistance a b =
-  restrictedDamerauLevenshteinDistance defaultEditCosts
-  (unpack a) (unpack b)
+  restrictedDamerauLevenshteinDistance
+    defaultEditCosts
+    (unpack a)
+    (unpack b)
 
 class PrettyError e where
   ppError :: e -> Doc Eann
@@ -36,9 +39,9 @@ class PrettyError e where
 instance PrettyError MultipleDeclarations where
   ppError MultipleDeclarations {..} =
     "Multiple declarations of" <+> ppSymbolT _multipleDeclSymbol <> line
-    <> "Declared at:" <+> align (vsep ints)
+      <> "Declared at:" <+> align (vsep ints)
     where
-    ints = map pretty [S._nameDefined _multipleDeclEntry, _multipleDeclSecond]
+      ints = map pretty [S._nameDefined (L.symbolEntryToSName _multipleDeclEntry), _multipleDeclSecond]
 
 instance PrettyError InfixError where
   ppError InfixError {..} =
@@ -55,69 +58,74 @@ infixErrorAux kind pp =
 
 instance PrettyError LacksFunctionClause where
   ppError LacksFunctionClause {..} =
-     pretty loc <> line <>
-     "There is a type signature with no function clause:" <> line
-     <> indent' (highlight (ppCode _lacksFunctionClause))
+    pretty loc <> line
+      <> "There is a type signature with no function clause:"
+      <> line
+      <> indent' (highlight (ppCode _lacksFunctionClause))
     where
-    loc = getLoc $ _sigName _lacksFunctionClause
+      loc = getLoc $ _sigName _lacksFunctionClause
 
 instance PrettyError LacksTypeSig where
   ppError LacksTypeSig {..} =
-     pretty loc <> line <>
-     "There is a declaration with a missing type signature:" <> line
-     <> indent' (highlight (ppCode _lacksTypeSigClause))
+    pretty loc <> line
+      <> "There is a declaration with a missing type signature:"
+      <> line
+      <> indent' (highlight (ppCode _lacksTypeSigClause))
     where
-    loc = getLoc $ _clauseOwnerFunction _lacksTypeSigClause
+      loc = getLoc $ _clauseOwnerFunction _lacksTypeSigClause
 
 instance PrettyError ImportCycle where
   ppError ImportCycle {..} =
     "There is an import cycle:" <> line
-    <> indent' lst
+      <> indent' lst
     where
-    lst = vsep $ intersperse "⇓" (map pp (toList (tie _importCycleImports)))
-    pp :: Import 'Parsed -> Doc Eann
-    pp t = ppCode t <+> parens ("at" <+> pretty (getLoc t))
-    tie :: NonEmpty a -> NonEmpty a
-    tie x = x <> pure (NonEmpty.head x)
+      lst = vsep $ intersperse "⇓" (map pp (toList (tie _importCycleImports)))
+      pp :: Import 'Parsed -> Doc Eann
+      pp t = ppCode t <+> parens ("at" <+> pretty (getLoc t))
+      tie :: NonEmpty a -> NonEmpty a
+      tie x = x <> pure (NonEmpty.head x)
 
 instance PrettyError NotInScope where
   ppError NotInScope {..} =
-    pretty loc <> line <>
-    "Symbol not in scope:" <+> highlight (ppCode _notInScopeSymbol)  <?>
-    ((line <>) <$> suggestion)
+    pretty loc <> line
+      <> "Symbol not in scope:" <+> highlight (ppCode _notInScopeSymbol)
+      <?> ((line <>) <$> suggestion)
     where
-    suggestion
-       | null suggestions = Nothing
-       | otherwise = Just $ "Perhaps you meant:" <+> align (vsep suggestions)
-    loc = getLoc _notInScopeSymbol
-    sym = _symbolText _notInScopeSymbol
-    maxDist :: Int
-    maxDist = 2
-    suggestions :: [Doc a]
-    suggestions =
+      suggestion
+        | null suggestions = Nothing
+        | otherwise = Just $ "Perhaps you meant:" <+> align (vsep suggestions)
+      loc = getLoc _notInScopeSymbol
+      sym = _symbolText _notInScopeSymbol
+      maxDist :: Int
+      maxDist = 2
+      suggestions :: [Doc a]
+      suggestions =
         map (pretty . fst) $
-        sortOn snd
-        [ (c, dist)  | c <- toList candidates
-          , let dist =  textDistance sym c, dist <= maxDist ]
-    candidates :: HashSet Text
-    candidates = HashSet.fromList (map _symbolText (HashMap.keys $ _localVars _notInScopeLocal)) <>
-      HashSet.fromList (map _symbolText (HashMap.keys $ _scopeSymbols _notInScopeScope))
+          sortOn
+            snd
+            [ (c, dist) | c <- toList candidates, let dist = textDistance sym c, dist <= maxDist
+            ]
+      candidates :: HashSet Text
+      candidates =
+        HashSet.fromList (map _symbolText (HashMap.keys $ _localVars _notInScopeLocal))
+          <> HashSet.fromList (map _symbolText (HashMap.keys $ _scopeSymbols _notInScopeScope))
 
 instance PrettyError BindGroupConflict where
   ppError BindGroupConflict {..} =
     "The symbol" <+> highlight (ppCode _bindGroupFirst)
-      <+> "appears twice in the same binding group:" <> line
-    <> indent' (align locs)
+      <+> "appears twice in the same binding group:"
+      <> line
+      <> indent' (align locs)
     where
-      locs = vsep $ map (pretty . getLoc) [_bindGroupFirst , _bindGroupSecond]
+      locs = vsep $ map (pretty . getLoc) [_bindGroupFirst, _bindGroupSecond]
 
 instance PrettyError DuplicateFixity where
   ppError DuplicateFixity {..} =
     "Multiple fixity declarations for symbol" <+> highlight (ppCode sym) <> ":" <> line
-     <> indent' (align locs)
+      <> indent' (align locs)
     where
       sym = opSymbol _dupFixityFirst
-      locs = vsep $ map (pretty . getLoc) [_dupFixityFirst , _dupFixityFirst]
+      locs = vsep $ map (pretty . getLoc) [_dupFixityFirst, _dupFixityFirst]
 
 instance PrettyError MultipleExportConflict where
   ppError MultipleExportConflict {..} =
@@ -134,14 +142,16 @@ instance PrettyError MegaParsecError where
 instance PrettyError WrongTopModuleName where
   ppError WrongTopModuleName {..} =
     "The top module" <+> ppCode _wrongTopModuleNameActualName <+> "is defined in the file:" <> line
-    <> highlight (pretty _wrongTopModuleNameActualPath) <> line
-    <> "But it should be in the file:" <> line
-    <> pretty _wrongTopModuleNameExpectedPath
+      <> highlight (pretty _wrongTopModuleNameActualPath)
+      <> line
+      <> "But it should be in the file:"
+      <> line
+      <> pretty _wrongTopModuleNameExpectedPath
 
 instance PrettyError UnusedOperatorDef where
   ppError UnusedOperatorDef {..} =
     "Unused operator syntax definition:" <> line
-    <> ppCode _unusedOperatorDef
+      <> ppCode _unusedOperatorDef
 
 instance PrettyError AmbiguousSym where
   ppError AmbiguousSym {} =
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Text.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Text.hs
index 812caa58f..d6e75e2a6 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Text.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Text.hs
@@ -1,8 +1,8 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text where
 
-import Prettyprinter
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
+import Prettyprinter
 import Prettyprinter.Render.Text
 
 renderText :: SimpleDocStream Eann -> Text
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
index 38a111bb8..4d8b73976 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
@@ -1,104 +1,105 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Error.Types (
-  module MiniJuvix.Syntax.Concrete.Language,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Types
-                                                    ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Error.Types
+  ( module MiniJuvix.Syntax.Concrete.Language,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Types,
+  )
+where
 
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Language
-import MiniJuvix.Syntax.Concrete.Scoped.Scope
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Scope
 
-data MultipleDeclarations = MultipleDeclarations {
-  _multipleDeclEntry :: SymbolEntry,
-  _multipleDeclSymbol :: Text,
-  _multipleDeclSecond :: Interval
+data MultipleDeclarations = MultipleDeclarations
+  { _multipleDeclEntry :: SymbolEntry,
+    _multipleDeclSymbol :: Text,
+    _multipleDeclSecond :: Interval
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | megaparsec error while resolving infixities.
-newtype InfixError = InfixError {
-  _infixErrAtoms :: ExpressionAtoms 'Scoped
+newtype InfixError = InfixError
+  { _infixErrAtoms :: ExpressionAtoms 'Scoped
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | megaparsec error while resolving infixities of patterns.
-newtype InfixErrorP = InfixErrorP {
-  _infixErrAtomsP :: PatternAtom 'Scoped
+newtype InfixErrorP = InfixErrorP
+  { _infixErrAtomsP :: PatternAtom 'Scoped
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | function clause without a type signature.
-newtype LacksTypeSig = LacksTypeSig {
-  _lacksTypeSigClause :: FunctionClause 'Parsed
+newtype LacksTypeSig = LacksTypeSig
+  { _lacksTypeSigClause :: FunctionClause 'Parsed
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | type signature without a function clause
-newtype LacksFunctionClause = LacksFunctionClause {
-  _lacksFunctionClause :: TypeSignature 'Scoped
+newtype LacksFunctionClause = LacksFunctionClause
+  { _lacksFunctionClause :: TypeSignature 'Scoped
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype ImportCycle = ImportCycle {
-  -- | If we have [a, b, c] it means that a import b imports c imports a.
-  _importCycleImports :: NonEmpty (Import 'Parsed)
+newtype ImportCycle = ImportCycle
+  { -- | If we have [a, b, c] it means that a import b imports c imports a.
+    _importCycleImports :: NonEmpty (Import 'Parsed)
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-data BindGroupConflict = BindGroupConflict {
- _bindGroupFirst :: Symbol,
- _bindGroupSecond :: Symbol
- }
- deriving stock (Show)
-
-data DuplicateFixity = DuplicateFixity {
- _dupFixityFirst :: OperatorSyntaxDef,
- _dupFixitySecond :: OperatorSyntaxDef
- }
- deriving stock (Show)
-
-data MultipleExportConflict = MultipleExportConflict {
-  _multipleExportModule :: S.AbsModulePath,
-  _multipleExportSymbol :: Symbol,
-  _multipleExportEntries :: NonEmpty SymbolEntry
+data BindGroupConflict = BindGroupConflict
+  { _bindGroupFirst :: Symbol,
+    _bindGroupSecond :: Symbol
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-data NotInScope = NotInScope {
- _notInScopeSymbol :: Symbol,
- _notInScopeLocal :: LocalVars,
- _notInScopeScope :: Scope
- }
- deriving stock (Show)
-
-newtype ModuleNotInScope = ModuleNotInScope {
-  _moduleNotInScopeName :: Name
+data DuplicateFixity = DuplicateFixity
+  { _dupFixityFirst :: OperatorSyntaxDef,
+    _dupFixitySecond :: OperatorSyntaxDef
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype MegaParsecError = MegaParsecError {
-  _megaParsecError :: Text
+data MultipleExportConflict = MultipleExportConflict
+  { _multipleExportModule :: S.AbsModulePath,
+    _multipleExportSymbol :: Symbol,
+    _multipleExportEntries :: NonEmpty SymbolEntry
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype UnusedOperatorDef = UnusedOperatorDef {
-  _unusedOperatorDef :: OperatorSyntaxDef
+data NotInScope = NotInScope
+  { _notInScopeSymbol :: Symbol,
+    _notInScopeLocal :: LocalVars,
+    _notInScopeScope :: Scope
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-data WrongTopModuleName = WrongTopModuleName {
-  _wrongTopModuleNameExpectedPath :: FilePath,
-  _wrongTopModuleNameActualPath :: FilePath,
-  _wrongTopModuleNameActualName :: TopModulePath
+newtype ModuleNotInScope = ModuleNotInScope
+  { _moduleNotInScopeName :: Name
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype AmbiguousSym = AmbiguousSym {
-  _ambiguousSymEntires :: [SymbolEntry]
+newtype MegaParsecError = MegaParsecError
+  { _megaParsecError :: Text
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype AmbiguousModuleSym = AmbiguousModuleSym {
-  _ambiguousModSymEntires :: [SymbolEntry]
+newtype UnusedOperatorDef = UnusedOperatorDef
+  { _unusedOperatorDef :: OperatorSyntaxDef
   }
- deriving stock (Show)
+  deriving stock (Show)
+
+data WrongTopModuleName = WrongTopModuleName
+  { _wrongTopModuleNameExpectedPath :: FilePath,
+    _wrongTopModuleNameActualPath :: FilePath,
+    _wrongTopModuleNameActualName :: TopModulePath
+  }
+  deriving stock (Show)
+
+newtype AmbiguousSym = AmbiguousSym
+  { _ambiguousSymEntires :: [SymbolEntry]
+  }
+  deriving stock (Show)
+
+newtype AmbiguousModuleSym = AmbiguousModuleSym
+  { _ambiguousModSymEntires :: [SymbolEntry]
+  }
+  deriving stock (Show)
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs
index c1a781b66..955f0af32 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs
@@ -1,22 +1,29 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Name (
-module MiniJuvix.Syntax.Concrete.Scoped.Name,
-module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-                                             ) where
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module MiniJuvix.Syntax.Concrete.Scoped.Name
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Name,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+  )
+where
 
 import Data.Stream (Stream (Cons))
 import Lens.Micro.Platform
-import qualified MiniJuvix.Syntax.Fixity as C
-import qualified MiniJuvix.Syntax.Concrete.Name as C
-import MiniJuvix.Syntax.Concrete.Loc
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Concrete.Loc
+import qualified MiniJuvix.Syntax.Concrete.Name as C
 import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import qualified MiniJuvix.Syntax.Fixity as C
 import Prettyprinter
 
 --------------------------------------------------------------------------------
 -- Names
 --------------------------------------------------------------------------------
 
+data IsConcrete = NotConcrete | Concrete
+
+$(genSingletons [''IsConcrete])
+
 newtype NameId = NameId Word64
   deriving stock (Show, Eq, Ord, Generic)
 
@@ -58,13 +65,13 @@ allNameIds = NameId <$> ids
 instance Hashable NameId
 
 -- | Why a symbol is in scope.
-data WhyInScope =
-  -- | Inherited from the parent module.
-  BecauseInherited WhyInScope
-  -- | Opened or imported in this module.
-  | BecauseImportedOpened
-  -- | Defined in this module.
-  | BecauseDefined
+data WhyInScope
+  = -- | Inherited from the parent module.
+    BecauseInherited WhyInScope
+  | -- | Opened or imported in this module.
+    BecauseImportedOpened
+  | -- | Defined in this module.
+    BecauseDefined
   deriving stock (Show)
 
 type Name = Name' C.Name
@@ -76,8 +83,7 @@ type TopModulePath = Name' C.TopModulePath
 type ModuleNameId = NameId
 
 data Name' n = Name'
-  {
-    _nameConcrete :: n,
+  { _nameConcrete :: n,
     _nameId :: NameId,
     _nameDefined :: Interval,
     _nameKind :: NameKind,
@@ -87,6 +93,7 @@ data Name' n = Name'
     _namePublicAnn :: PublicAnn
   }
   deriving stock (Show)
+
 makeLenses ''Name'
 
 instance HasNameKind (Name' n) where
@@ -112,12 +119,15 @@ topModulePathName = over nameConcrete C._modulePathName
 symbolText :: Symbol -> Text
 symbolText = C._symbolText . _nameConcrete
 
+unqualifiedSymbol :: Symbol -> Name
+unqualifiedSymbol = over nameConcrete C.NameUnqualified
+
 nameUnqualify :: Name -> Symbol
 nameUnqualify Name' {..} = Name' {_nameConcrete = unqual, ..}
   where
-  unqual = case _nameConcrete of
-       C.NameUnqualified s -> s
-       C.NameQualified q -> fromQualifiedName q
+    unqual = case _nameConcrete of
+      C.NameUnqualified s -> s
+      C.NameQualified q -> fromQualifiedName q
 
 instance Eq (Name' n) where
   (==) = (==) `on` _nameId
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
index dd3b9a740..0515ded90 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
@@ -28,13 +28,13 @@ instance HasNameKind NameKind where
 
 isExprKind :: HasNameKind a => a -> Bool
 isExprKind k = case getNameKind k of
-    KNameConstructor -> True
-    KNameInductive -> True
-    KNameFunction -> True
-    KNameLocal -> True
-    KNameAxiom -> True
-    KNameLocalModule -> False
-    KNameTopModule -> False
+  KNameConstructor -> True
+  KNameInductive -> True
+  KNameFunction -> True
+  KNameLocal -> True
+  KNameAxiom -> True
+  KNameLocalModule -> False
+  KNameTopModule -> False
 
 isModuleKind :: HasNameKind a => a -> Bool
 isModuleKind k = case getNameKind k of
@@ -54,10 +54,10 @@ canHaveFixity k = case getNameKind k of
 
 nameKindAnsi :: NameKind -> AnsiStyle
 nameKindAnsi k = case k of
-    KNameConstructor -> colorDull Magenta
-    KNameInductive -> colorDull Green
-    KNameAxiom -> colorDull Red
-    KNameLocalModule -> mempty
-    KNameFunction -> colorDull Yellow
-    KNameLocal -> mempty
-    KNameTopModule -> mempty
+  KNameConstructor -> colorDull Magenta
+  KNameInductive -> colorDull Green
+  KNameAxiom -> colorDull Red
+  KNameLocalModule -> mempty
+  KNameFunction -> colorDull Yellow
+  KNameLocal -> mempty
+  KNameTopModule -> mempty
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ann.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ann.hs
index a26ce4a3b..171dd2b1b 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ann.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ann.hs
@@ -1,7 +1,7 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann where
 
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Concrete.Language (TopModulePath)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 
 data Ann
   = AnnKind S.NameKind
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs
index 277a3f633..0031594cf 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs
@@ -1,8 +1,8 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi where
 
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
-import MiniJuvix.Prelude
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -19,8 +19,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
index c0fe054d6..2d1706839 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
@@ -1,20 +1,20 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (
-  module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base,
-  module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
-                                                    ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base,
+    module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann,
+  )
+where
 
-import MiniJuvix.Syntax.Concrete.Language
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Prelude
 import qualified Data.List.NonEmpty.Extra as NonEmpty
-import Prettyprinter hiding (braces, parens)
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
-import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
 import MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language
+import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
+import Prettyprinter hiding (braces, parens)
 
 data Options = Options
-  {
-    _optShowNameId :: Bool,
+  { _optShowNameId :: Bool,
     _optInlineImports :: Bool,
     _optIndent :: Int
   }
@@ -22,8 +22,7 @@ data Options = Options
 defaultOptions :: Options
 defaultOptions =
   Options
-    {
-      _optShowNameId = False,
+    { _optShowNameId = False,
       _optInlineImports = False,
       _optIndent = 2
     }
@@ -176,15 +175,18 @@ parens = enclose kwParenL kwParenR
 doubleQuotes :: Doc Ann -> Doc Ann
 doubleQuotes = enclose kwDQuote kwDQuote
 
-ppModulePathType :: forall t s r. (SingI t, SingI s, Members '[Reader Options] r) =>
-  ModulePathType s t -> Sem r (Doc Ann)
+ppModulePathType ::
+  forall t s r.
+  (SingI t, SingI s, Members '[Reader Options] r) =>
+  ModulePathType s t ->
+  Sem r (Doc Ann)
 ppModulePathType x = case sing :: SStage s of
   SParsed -> case sing :: SModuleIsTop t of
     SModuleLocal -> ppCode x
     SModuleTop -> ppCode x
   SScoped -> case sing :: SModuleIsTop t of
     SModuleLocal -> annSDef x <$> ppCode x
-    SModuleTop ->  annSDef x <$> ppCode x
+    SModuleTop -> annSDef x <$> ppCode x
 
 ppUnkindedSymbol :: Members '[Reader Options] r => Symbol -> Sem r (Doc Ann)
 ppUnkindedSymbol = fmap (annotate AnnUnkindedSym) . ppSymbol
@@ -197,63 +199,66 @@ ppSymbol = case sing :: SStage s of
 groupStatements :: forall s. SingI s => [Statement s] -> [[Statement s]]
 groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
   where
-  aux :: ([Statement s], [[Statement s]]) -> Statement s
-      -> ([Statement s], [[Statement s]])
-  aux ([], acc) s = ([s], acc)
-  aux (gr@(a : _), acc) b
-    | g a b = (b : gr, acc)
-    | otherwise = ([b], gr : acc)
-  -- | Decides if statements a and b should be next to each other without a
-  -- blank line
-  g :: Statement s -> Statement s -> Bool
-  g a b = case (a, b) of
-    (StatementCompile _, StatementCompile _) -> True
-    (StatementCompile _, _) -> False
-    (StatementForeign _, _) -> False
-    (StatementOperator _, StatementOperator _) -> True
-    (StatementOperator o, s) -> definesSymbol (opSymbol o) s
-    (StatementImport _, StatementImport _) -> True
-    (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
-      SParsed -> True
-      SScoped ->
-        S._nameId (_modulePath (importModule i)) ==
-        S._nameId (openModuleName o)
-    (StatementImport _, _) -> False
-    (StatementOpenModule {}, StatementOpenModule {}) -> True
-    (StatementOpenModule {}, _) -> False
-    (StatementInductive {}, _) -> False
-    (StatementModule {}, _) -> False
-    (StatementAxiom {}, StatementAxiom {}) -> True
-    (StatementAxiom {}, _) -> False
-    (StatementEval {}, StatementEval {}) -> True
-    (StatementEval {}, _) -> False
-    (StatementPrint {}, StatementPrint {}) -> True
-    (StatementPrint {}, _) -> False
-    (StatementTypeSignature sig, StatementFunctionClause fun) ->
-      case sing :: SStage s of
-        SParsed -> _sigName sig == _clauseOwnerFunction fun
-        SScoped -> _sigName sig == _clauseOwnerFunction fun
-    (StatementTypeSignature {}, _) -> False
-    (StatementFunctionClause fun1, StatementFunctionClause fun2) ->
-      case sing :: SStage s of
-        SParsed -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
-        SScoped -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
-    (StatementFunctionClause {}, _) -> False
-  definesSymbol :: Symbol -> Statement s -> Bool
-  definesSymbol n s = case s of
-    StatementTypeSignature sig ->
-      let sym = case sing :: SStage s of
-            SParsed -> _sigName sig
-            SScoped -> S._nameConcrete $ _sigName sig
-      in n == sym
-    StatementInductive d -> n `elem` syms d
-    _ -> False
-    where
-    syms :: InductiveDef s -> [Symbol]
-    syms InductiveDef {..} = case sing :: SStage s of
-      SParsed -> _inductiveName : map constructorName _inductiveConstructors
-      SScoped -> S._nameConcrete _inductiveName :
-          map (S._nameConcrete . constructorName) _inductiveConstructors
+    aux ::
+      ([Statement s], [[Statement s]]) ->
+      Statement s ->
+      ([Statement s], [[Statement s]])
+    aux ([], acc) s = ([s], acc)
+    aux (gr@(a : _), acc) b
+      | g a b = (b : gr, acc)
+      | otherwise = ([b], gr : acc)
+    -- Decides if statements a and b should be next to each other without a
+    -- blank line
+    g :: Statement s -> Statement s -> Bool
+    g a b = case (a, b) of
+      (StatementCompile _, StatementCompile _) -> True
+      (StatementCompile _, _) -> False
+      (StatementForeign _, _) -> False
+      (StatementOperator _, StatementOperator _) -> True
+      (StatementOperator o, s) -> definesSymbol (opSymbol o) s
+      (StatementImport _, StatementImport _) -> True
+      (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
+        SParsed -> True
+        SScoped ->
+          S._nameId (_modulePath (importModule i))
+            == S._nameId (projSigma2 _moduleRefName (openModuleName o ^. unModuleRef'))
+      (StatementImport _, _) -> False
+      (StatementOpenModule {}, StatementOpenModule {}) -> True
+      (StatementOpenModule {}, _) -> False
+      (StatementInductive {}, _) -> False
+      (StatementModule {}, _) -> False
+      (StatementAxiom {}, StatementAxiom {}) -> True
+      (StatementAxiom {}, _) -> False
+      (StatementEval {}, StatementEval {}) -> True
+      (StatementEval {}, _) -> False
+      (StatementPrint {}, StatementPrint {}) -> True
+      (StatementPrint {}, _) -> False
+      (StatementTypeSignature sig, StatementFunctionClause fun) ->
+        case sing :: SStage s of
+          SParsed -> _sigName sig == _clauseOwnerFunction fun
+          SScoped -> _sigName sig == _clauseOwnerFunction fun
+      (StatementTypeSignature {}, _) -> False
+      (StatementFunctionClause fun1, StatementFunctionClause fun2) ->
+        case sing :: SStage s of
+          SParsed -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
+          SScoped -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
+      (StatementFunctionClause {}, _) -> False
+    definesSymbol :: Symbol -> Statement s -> Bool
+    definesSymbol n s = case s of
+      StatementTypeSignature sig ->
+        let sym = case sing :: SStage s of
+              SParsed -> _sigName sig
+              SScoped -> S._nameConcrete $ _sigName sig
+         in n == sym
+      StatementInductive d -> n `elem` syms d
+      _ -> False
+      where
+        syms :: InductiveDef s -> [Symbol]
+        syms InductiveDef {..} = case sing :: SStage s of
+          SParsed -> _inductiveName : map constructorName _inductiveConstructors
+          SScoped ->
+            S._nameConcrete _inductiveName :
+            map (S._nameConcrete . constructorName) _inductiveConstructors
 
 instance SingI s => PrettyCode [Statement s] where
   ppCode ss = joinGroups <$> mapM (fmap mkGroup . mapM (fmap endSemicolon . ppCode)) (groupStatements ss)
@@ -283,8 +288,11 @@ instance PrettyCode Backend where
 instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
-    return $ kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty _foreignCode <> line <> rbrace
+    return $
+      kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode
+        <> line
+        <> rbrace
 
 instance SingI s => PrettyCode (CompileDef s) where
   ppCode CompileDef {..} = do
@@ -296,8 +304,11 @@ instance SingI s => PrettyCode (CompileDef s) where
 ppStringLit :: Text -> Doc Ann
 ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty
 
-ppTopModulePath :: forall s r. (SingI s, Members '[Reader Options] r) =>
-  ModulePathType s 'ModuleTop -> Sem r (Doc Ann)
+ppTopModulePath ::
+  forall s r.
+  (SingI s, Members '[Reader Options] r) =>
+  ModulePathType s 'ModuleTop ->
+  Sem r (Doc Ann)
 ppTopModulePath = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
@@ -322,27 +333,29 @@ instance PrettyCode AbsModulePath where
     absTopModulePath' <- ppCode absTopModulePath
     return $ dotted (absTopModulePath' : absLocalPath')
 
-ppInductiveParameters :: (SingI s, Members '[Reader Options] r)
-    => [InductiveParameter s] -> Sem r (Maybe (Doc Ann))
+ppInductiveParameters ::
+  (SingI s, Members '[Reader Options] r) =>
+  [InductiveParameter s] ->
+  Sem r (Maybe (Doc Ann))
 ppInductiveParameters ps
   | null ps = return Nothing
   | otherwise = Just <$> ppCode ps
 
 instance (SingI s, SingI t) => PrettyCode (Module s t) where
   ppCode Module {..} = do
-      moduleBody' <- ppCode _moduleBody >>= indented
-      modulePath' <- ppModulePathType _modulePath
-      moduleParameters' <- ppInductiveParameters _moduleParameters
-      return $
-        kwModule <+> modulePath' <+?> moduleParameters' <> kwSemicolon <> line
-          <> moduleBody'
-          <> line
-          <> kwEnd
-          <?> lastSemicolon
-      where
-        lastSemicolon = case sing :: SModuleIsTop t of
-          SModuleLocal -> Nothing
-          SModuleTop -> Just kwSemicolon
+    moduleBody' <- ppCode _moduleBody >>= indented
+    modulePath' <- ppModulePathType _modulePath
+    moduleParameters' <- ppInductiveParameters _moduleParameters
+    return $
+      kwModule <+> modulePath' <+?> moduleParameters' <> kwSemicolon <> line
+        <> moduleBody'
+        <> line
+        <> kwEnd
+        <?> lastSemicolon
+    where
+      lastSemicolon = case sing :: SModuleIsTop t of
+        SModuleLocal -> Nothing
+        SModuleTop -> Just kwSemicolon
 
 instance PrettyCode Precedence where
   ppCode p = return $ case p of
@@ -358,11 +371,11 @@ instance PrettyCode Fixity where
 
 instance PrettyCode OperatorArity where
   ppCode fixityArity = return $ case fixityArity of
-   Unary {} -> kwPostfix
-   Binary p -> case p of
-     AssocRight -> kwInfixr
-     AssocLeft -> kwInfixl
-     AssocNone -> kwInfix
+    Unary {} -> kwPostfix
+    Binary p -> case p of
+      AssocRight -> kwInfixr
+      AssocLeft -> kwInfixl
+      AssocNone -> kwInfix
 
 instance PrettyCode OperatorSyntaxDef where
   ppCode OperatorSyntaxDef {..} = do
@@ -400,7 +413,7 @@ instance PrettyCode QualifiedName where
     let symbols = pathParts _qualifiedPath NonEmpty.|> _qualifiedSymbol
     dotted <$> mapM ppSymbol symbols
 
-ppName :: forall s r. (SingI s, Members '[Reader Options] r) => NameType s -> Sem r (Doc Ann)
+ppName :: forall s r. (SingI s, Members '[Reader Options] r) => IdentifierType s -> Sem r (Doc Ann)
 ppName = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
@@ -434,39 +447,45 @@ instance PrettyCode n => PrettyCode (S.Name' n) where
     showNameId <- asks _optShowNameId
     uid <- if showNameId then ("@" <>) <$> ppCode _nameId else return mempty
     return $ annSRef (nameConcrete' <> uid)
-      where
+    where
       annSRef :: Doc Ann -> Doc Ann
       annSRef = annotate (AnnRef (S.absTopModulePath _nameDefinedIn) _nameId)
 
+instance PrettyCode ModuleRef where
+  ppCode = ppCode . projSigma2 _moduleRefName . (^. unModuleRef')
+
 instance SingI s => PrettyCode (OpenModule s) where
   ppCode :: forall r. Members '[Reader Options] r => OpenModule s -> Sem r (Doc Ann)
   ppCode OpenModule {..} = do
-    openModuleName' <- ppName openModuleName
+    openModuleName' <- case sing :: SStage s of
+      SParsed -> ppCode openModuleName
+      SScoped -> ppCode openModuleName
     openUsingHiding' <- sequence $ ppUsingHiding <$> openUsingHiding
     openParameters' <- ppOpenParams
     let openPublic' = ppPublic
     return $ keyword "open" <+> openModuleName' <+?> openParameters' <+?> openUsingHiding' <+?> openPublic'
     where
-    ppAtom' = case sing :: SStage s of
-      SParsed -> ppCodeAtom
-      SScoped -> ppCodeAtom
-    ppOpenParams :: Sem r (Maybe (Doc Ann))
-    ppOpenParams = case openParameters of
-      [] -> return Nothing
-      _ -> Just . hsep <$> mapM ppAtom' openParameters
-    ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
-    ppUsingHiding uh = do
-      bracedList <- encloseSep kwBraceL kwBraceR kwSemicolon . toList
-        <$> mapM ppUnkindedSymbol syms
-      return $ kw <+> bracedList
-      where
-        (kw, syms) = case uh of
-          Using s -> (kwUsing, s)
-          Hiding s -> (kwHiding, s)
-    ppPublic :: Maybe (Doc Ann)
-    ppPublic = case openPublic of
-      Public -> Just kwPublic
-      NoPublic -> Nothing
+      ppAtom' = case sing :: SStage s of
+        SParsed -> ppCodeAtom
+        SScoped -> ppCodeAtom
+      ppOpenParams :: Sem r (Maybe (Doc Ann))
+      ppOpenParams = case openParameters of
+        [] -> return Nothing
+        _ -> Just . hsep <$> mapM ppAtom' openParameters
+      ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
+      ppUsingHiding uh = do
+        bracedList <-
+          encloseSep kwBraceL kwBraceR kwSemicolon . toList
+            <$> mapM ppUnkindedSymbol syms
+        return $ kw <+> bracedList
+        where
+          (kw, syms) = case uh of
+            Using s -> (kwUsing, s)
+            Hiding s -> (kwHiding, s)
+      ppPublic :: Maybe (Doc Ann)
+      ppPublic = case openPublic of
+        Public -> Just kwPublic
+        NoPublic -> Nothing
 
 instance SingI s => PrettyCode (TypeSignature s) where
   ppCode TypeSignature {..} = do
@@ -587,22 +606,30 @@ instance SingI s => PrettyCode (Import s) where
     inlineImport' <- inlineImport
     return $ kwImport <+> modulePath' <+?> inlineImport'
     where
-    ppModulePath = case sing :: SStage s of
-      SParsed -> ppCode m
-      SScoped -> ppTopModulePath (m ^. modulePath)
-    jumpLines :: Doc Ann -> Doc Ann
-    jumpLines x = line <> x <> line
-    inlineImport :: Sem r (Maybe (Doc Ann))
-    inlineImport = do
-      b <- asks _optInlineImports
-      if b then case sing :: SStage s of
-        SParsed -> return Nothing
-        SScoped -> ppCode m >>= fmap (Just . braces . jumpLines) . indented
-        else return Nothing
+      ppModulePath = case sing :: SStage s of
+        SParsed -> ppCode m
+        SScoped -> ppTopModulePath (m ^. modulePath)
+      jumpLines :: Doc Ann -> Doc Ann
+      jumpLines x = line <> x <> line
+      inlineImport :: Sem r (Maybe (Doc Ann))
+      inlineImport = do
+        b <- asks _optInlineImports
+        if b
+          then case sing :: SStage s of
+            SParsed -> return Nothing
+            SScoped -> ppCode m >>= fmap (Just . braces . jumpLines) . indented
+          else return Nothing
+
+instance PrettyCode PatternScopedIden where
+  ppCode = \case
+    PatternScopedVar v -> ppCode v
+    PatternScopedConstructor c -> ppCode c
 
 instance SingI s => PrettyCode (PatternAtom s) where
   ppCode a = case a of
-    PatternAtomName n -> ppName n
+    PatternAtomIden n -> case sing :: SStage s of
+      SParsed -> ppCode n
+      SScoped -> ppCode n
     PatternAtomWildcard -> return kwWildcard
     PatternAtomEmpty -> return $ parens mempty
     PatternAtomParens p -> parens <$> ppCode p
@@ -610,12 +637,12 @@ instance SingI s => PrettyCode (PatternAtom s) where
 instance SingI s => PrettyCode (PatternAtoms s) where
   ppCode (PatternAtoms ps) = hsep . toList <$> mapM ppCode ps
 
-ppPattern :: forall s r. (SingI s,  Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
+ppPattern :: forall s r. (SingI s, Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
 ppPattern = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
 
-ppPatternAtom :: forall s r. (SingI s,  Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
+ppPatternAtom :: forall s r. (SingI s, Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
 ppPatternAtom = case sing :: SStage s of
   SParsed -> ppCodeAtom
   SScoped -> ppCodeAtom
@@ -644,6 +671,26 @@ instance PrettyCode Literal where
     LitInteger n -> return $ annotate AnnLiteralInteger (pretty n)
     LitString s -> return $ ppStringLit s
 
+instance PrettyCode AxiomRef where
+  ppCode a = ppCode (a ^. axiomRefName)
+
+instance PrettyCode InductiveRef where
+  ppCode a = ppCode (a ^. inductiveRefName)
+
+instance PrettyCode FunctionRef where
+  ppCode a = ppCode (a ^. functionRefName)
+
+instance PrettyCode ConstructorRef where
+  ppCode a = ppCode (a ^. constructorRefName)
+
+instance PrettyCode ScopedIden where
+  ppCode = \case
+    ScopedAxiom a -> ppCode a
+    ScopedInductive i -> ppCode i
+    ScopedVar n -> ppCode n
+    ScopedFunction f -> ppCode f
+    ScopedConstructor c -> ppCode c
+
 instance PrettyCode Expression where
   ppCode e = case e of
     ExpressionIdentifier n -> ppCode n
@@ -672,40 +719,52 @@ instance PrettyCode Pattern where
     PatternInfixApplication i -> ppPatternInfixApp i
     PatternPostfixApplication i -> ppPatternPostfixApp i
     where
-    ppPatternInfixApp :: PatternInfixApp -> Sem r (Doc Ann)
-    ppPatternInfixApp p@PatternInfixApp {..} = do
-      patInfixConstructor' <- ppCode patInfixConstructor
-      patInfixLeft' <- ppLeftExpression (getFixity p) patInfixLeft
-      patInfixRight' <- ppRightExpression (getFixity p) patInfixRight
-      return $ patInfixLeft' <+> patInfixConstructor' <+> patInfixRight'
+      ppPatternInfixApp :: PatternInfixApp -> Sem r (Doc Ann)
+      ppPatternInfixApp p@PatternInfixApp {..} = do
+        patInfixConstructor' <- ppCode patInfixConstructor
+        patInfixLeft' <- ppLeftExpression (getFixity p) patInfixLeft
+        patInfixRight' <- ppRightExpression (getFixity p) patInfixRight
+        return $ patInfixLeft' <+> patInfixConstructor' <+> patInfixRight'
 
-    ppPatternPostfixApp :: PatternPostfixApp -> Sem r (Doc Ann)
-    ppPatternPostfixApp p@PatternPostfixApp {..} = do
-      patPostfixConstructor' <- ppCode patPostfixConstructor
-      patPostfixParameter' <- ppLeftExpression (getFixity p) patPostfixParameter
-      return $ patPostfixParameter' <+> patPostfixConstructor'
+      ppPatternPostfixApp :: PatternPostfixApp -> Sem r (Doc Ann)
+      ppPatternPostfixApp p@PatternPostfixApp {..} = do
+        patPostfixConstructor' <- ppCode patPostfixConstructor
+        patPostfixParameter' <- ppLeftExpression (getFixity p) patPostfixParameter
+        return $ patPostfixParameter' <+> patPostfixConstructor'
 
 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 ::
+  (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 ::
+  (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 ::
+  (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 ::
+  (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
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
index 4d85e2033..58ec223ee 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
@@ -1,22 +1,22 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html (genHtml, Theme(..)) where
+module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html (genHtml, Theme (..)) where
 
-import MiniJuvix.Syntax.Concrete.Language
-import MiniJuvix.Syntax.Concrete.Scoped.Utils
-import           Prettyprinter.Render.Util.SimpleDocTree
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
-import MiniJuvix.Prelude
-import Prettyprinter
-import qualified Text.Blaze.Html.Renderer.Text           as Html
-import           Text.Blaze.Html5                       as Html hiding (map)
-import qualified Text.Blaze.Html5.Attributes             as Attr
 import qualified Data.Text as Text
 import qualified Data.Text.IO as Text
 import Data.Text.Lazy (toStrict)
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
+import MiniJuvix.Syntax.Concrete.Scoped.Utils
 import MiniJuvix.Utils.Paths
+import Prettyprinter
+import Prettyprinter.Render.Util.SimpleDocTree
+import qualified Text.Blaze.Html.Renderer.Text as Html
+import Text.Blaze.Html5 as Html hiding (map)
+import qualified Text.Blaze.Html5.Attributes as Attr
 
-data Theme =
-  Nord
+data Theme
+  = Nord
   | Ayu
   deriving stock (Show)
 
@@ -27,58 +27,65 @@ genHtml opts recursive theme entry = do
   withCurrentDirectory htmlPath $ do
     mapM_ outputModule allModules
   where
-  allModules
-    | recursive = toList $ getAllModules entry
-    | otherwise = pure entry
-  htmlPath = "html"
+    allModules
+      | recursive = toList $ getAllModules entry
+      | otherwise = pure entry
+    htmlPath = "html"
 
-  copyAssetFiles :: IO ()
-  copyAssetFiles = do
-    createDirectoryIfMissing True toAssetsDir
-    mapM_ cpFile assetFiles
-    where
-    fromAssetsDir = $(assetsDir)
-    toAssetsDir = htmlPath </> "assets"
-    cpFile (fromDir, name, toDir) = copyFile (fromDir </> name) (toDir </> name)
-    assetFiles = [ (fromAssetsDir, name, toAssetsDir)
-                | name <- ["highlight.js"
-                          , "source-ayu-light.css"
-                          , "source-nord.css"]]
+    copyAssetFiles :: IO ()
+    copyAssetFiles = do
+      createDirectoryIfMissing True toAssetsDir
+      mapM_ cpFile assetFiles
+      where
+        fromAssetsDir = $(assetsDir)
+        toAssetsDir = htmlPath </> "assets"
+        cpFile (fromDir, name, toDir) = copyFile (fromDir </> name) (toDir </> name)
+        assetFiles =
+          [ (fromAssetsDir, name, toAssetsDir)
+            | name <-
+                [ "highlight.js",
+                  "source-ayu-light.css",
+                  "source-nord.css"
+                ]
+          ]
 
-  outputModule :: Module 'Scoped 'ModuleTop -> IO ()
-  outputModule m = do
-    createDirectoryIfMissing True (takeDirectory htmlFile)
-    putStrLn $ "Writing " <> pack htmlFile
-    Text.writeFile htmlFile (genModule opts theme m)
-   where
-   htmlFile = dottedPath (S._nameConcrete (_modulePath m)) <.> ".html"
+    outputModule :: Module 'Scoped 'ModuleTop -> IO ()
+    outputModule m = do
+      createDirectoryIfMissing True (takeDirectory htmlFile)
+      putStrLn $ "Writing " <> pack htmlFile
+      Text.writeFile htmlFile (genModule opts theme m)
+      where
+        htmlFile = dottedPath (S._nameConcrete (_modulePath m)) <.> ".html"
 
 genModule :: Options -> Theme -> Module 'Scoped 'ModuleTop -> Text
 genModule opts theme m =
-  toStrict $ Html.renderHtml $
-  docTypeHtml ! Attr.xmlns "http://www.w3.org/1999/xhtml" $
-  mhead
-  <> mbody
+  toStrict $
+    Html.renderHtml $
+      docTypeHtml ! Attr.xmlns "http://www.w3.org/1999/xhtml" $
+        mhead
+          <> mbody
   where
-  themeCss = case theme of
-    Ayu -> ayuCss
-    Nord -> nordCss
-  prettySrc = (pre ! Attr.id "src-content")
-    $ renderTree $ treeForm $ docStream opts m
+    themeCss = case theme of
+      Ayu -> ayuCss
+      Nord -> nordCss
+    prettySrc =
+      (pre ! Attr.id "src-content") $
+        renderTree $ treeForm $ docStream opts m
 
-  mheader :: Html
-  mheader = Html.div ! Attr.id "package-header"
-    $ (Html.span ! Attr.class_ "caption" $ "")
+    mheader :: Html
+    mheader =
+      Html.div ! Attr.id "package-header" $
+        (Html.span ! Attr.class_ "caption" $ "")
 
-  mhead :: Html
-  mhead =
-    metaUtf8
-    <> themeCss
-    <> highlightJs
-  mbody :: Html
-  mbody =
-    mheader
-    <> prettySrc
+    mhead :: Html
+    mhead =
+      metaUtf8
+        <> themeCss
+        <> highlightJs
+    mbody :: Html
+    mbody =
+      mheader
+        <> prettySrc
 
 docStream :: Options -> Module 'Scoped 'ModuleTop -> SimpleDocStream Ann
 docStream opts m = layoutPretty defaultLayoutOptions (runPrettyCode opts m)
@@ -88,13 +95,13 @@ renderTree = go
 
 go :: SimpleDocTree Ann -> Html
 go sdt = case sdt of
-    STEmpty -> mempty
-    STChar c -> toHtml c
-    STText _ t -> toHtml t
-    STLine s -> "\n" <> toHtml (textSpaces s)
-    STAnn ann content -> putTag ann (go content)
-    STConcat l -> mconcatMap go l
-    where
+  STEmpty -> mempty
+  STChar c -> toHtml c
+  STText _ t -> toHtml t
+  STLine s -> "\n" <> toHtml (textSpaces s)
+  STAnn ann content -> putTag ann (go content)
+  STConcat l -> mconcatMap go l
+  where
     textSpaces :: Int -> Text
     textSpaces n = Text.replicate n (Text.singleton ' ')
 
@@ -103,38 +110,42 @@ fromText = fromString . unpack
 
 putTag :: Ann -> Html -> Html
 putTag ann x = case ann of
-   AnnKind k -> tagKind k x
-   AnnLiteralInteger -> Html.span ! Attr.class_ "ju-number" $ x
-   AnnLiteralString -> Html.span ! Attr.class_ "ju-string" $ x
-   AnnKeyword -> Html.span ! Attr.class_ "ju-keyword" $ x
-   AnnUnkindedSym -> Html.span ! Attr.class_ "ju-var" $ x
-   AnnDelimiter -> Html.span ! Attr.class_ "ju-delimiter" $ x
-   AnnDef tmp ni -> tagDef tmp ni
-   AnnRef tmp ni -> tagRef tmp ni
-
+  AnnKind k -> tagKind k x
+  AnnLiteralInteger -> Html.span ! Attr.class_ "ju-number" $ x
+  AnnLiteralString -> Html.span ! Attr.class_ "ju-string" $ x
+  AnnKeyword -> Html.span ! Attr.class_ "ju-keyword" $ x
+  AnnUnkindedSym -> Html.span ! Attr.class_ "ju-var" $ x
+  AnnDelimiter -> Html.span ! Attr.class_ "ju-delimiter" $ x
+  AnnDef tmp ni -> tagDef tmp ni
+  AnnRef tmp ni -> tagRef tmp ni
   where
-  tagDef :: TopModulePath -> S.NameId -> Html
-  tagDef tmp nid = Html.span ! Attr.id (nameIdAttr nid)
-    $ tagRef tmp nid
+    tagDef :: TopModulePath -> S.NameId -> Html
+    tagDef tmp nid =
+      Html.span ! Attr.id (nameIdAttr nid) $
+        tagRef tmp nid
 
-  tagRef tmp ni = Html.span ! Attr.class_ "annot"
-                  $ a ! Attr.href (nameIdAttrRef tmp ni)
-                  $ x
-  tagKind k = Html.span ! Attr.class_
-     (case k of
-      S.KNameConstructor -> "ju-constructor"
-      S.KNameInductive -> "ju-inductive"
-      S.KNameFunction -> "ju-function"
-      S.KNameLocal -> "ju-var"
-      S.KNameAxiom -> "ju-axiom"
-      S.KNameLocalModule -> "ju-var"
-      S.KNameTopModule -> "ju-var")
+    tagRef tmp ni =
+      Html.span ! Attr.class_ "annot" $
+        a ! Attr.href (nameIdAttrRef tmp ni) $
+          x
+    tagKind k =
+      Html.span
+        ! Attr.class_
+          ( case k of
+              S.KNameConstructor -> "ju-constructor"
+              S.KNameInductive -> "ju-inductive"
+              S.KNameFunction -> "ju-function"
+              S.KNameLocal -> "ju-var"
+              S.KNameAxiom -> "ju-axiom"
+              S.KNameLocalModule -> "ju-var"
+              S.KNameTopModule -> "ju-var"
+          )
 
 dottedPath :: IsString s => TopModulePath -> s
 dottedPath (TopModulePath l r) =
   fromText $ mconcat $ intersperse "." $ map fromSymbol $ l ++ [r]
   where
-  fromSymbol Symbol {..} = _symbolText
+    fromSymbol Symbol {..} = _symbolText
 
 nameIdAttr :: S.NameId -> AttributeValue
 nameIdAttr (S.NameId k) = fromString . show $ k
@@ -144,9 +155,10 @@ nameIdAttrRef tp s =
   dottedPath tp <> ".html" <> preEscapedToValue '#' <> nameIdAttr s
 
 cssLink :: AttributeValue -> Html
-cssLink css = link ! Attr.href css
-        ! Attr.rel "stylesheet"
-        ! Attr.type_ "text/css"
+cssLink css =
+  link ! Attr.href css
+    ! Attr.rel "stylesheet"
+    ! Attr.type_ "text/css"
 
 ayuCss :: Html
 ayuCss = cssLink "assets/source-ayu-light.css"
@@ -155,9 +167,10 @@ nordCss :: Html
 nordCss = cssLink "assets/source-nord.css"
 
 highlightJs :: Html
-highlightJs = script ! Attr.src "assets/highlight.js"
-        ! Attr.type_ "text/javascript"
-        $ mempty
+highlightJs =
+  script ! Attr.src "assets/highlight.js"
+    ! Attr.type_ "text/javascript"
+    $ mempty
 
 metaUtf8 :: Html
 metaUtf8 = meta ! Attr.charset "UTF-8"
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Text.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Text.hs
index b9ad191b1..aabb0afe7 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Text.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Text.hs
@@ -1,7 +1,7 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text where
 
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
 import Prettyprinter
 import Prettyprinter.Render.Text
 
@@ -21,5 +21,8 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream Ann
-docStream opts = layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs
index 139be090e..9c4c7d084 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs
@@ -22,45 +22,25 @@ newtype SymbolInfo = SymbolInfo
   }
   deriving newtype (Show, Semigroup, Monoid)
 
-type SymbolEntry = S.Name' ()
-
--- data SymbolEntry' = SymbolEntry' {
---   _entryNameInfo :: NameInfo
-
---   }
-
--- | Symbols that a module exports
-newtype ExportInfo = ExportInfo {
-   _exportSymbols :: HashMap Symbol SymbolEntry
-  }
-
--- | A module entry for either a local or a top module.
-type ModuleEntry = Σ ModuleIsTop (TyCon1 ModuleEntry')
-
-mkModuleEntry :: SingI t => ModuleEntry' t -> ModuleEntry
-mkModuleEntry = (sing :&:)
-
-data ModuleEntry' (t :: ModuleIsTop) = ModuleEntry' {
-  _moduleEntryExport :: ExportInfo,
-  _moduleEntryScoped :: Module 'Scoped t
-  }
+mkModuleRef' :: SingI t => ModuleRef'' 'S.NotConcrete t -> ModuleRef' 'S.NotConcrete
+mkModuleRef' m = ModuleRef' (sing :&: m)
 
 data Scope = Scope
   { _scopePath :: S.AbsModulePath,
     _scopeFixities :: HashMap Symbol OperatorSyntaxDef,
     _scopeSymbols :: HashMap Symbol SymbolInfo,
-    _scopeTopModules :: HashMap TopModulePath S.ModuleNameId,
+    _scopeTopModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop),
     _scopeBindGroup :: HashMap Symbol LocalVariable
   }
- deriving stock (Show)
+  deriving stock (Show)
+
 makeLenses ''ExportInfo
 makeLenses ''SymbolInfo
 makeLenses ''LocalVars
 makeLenses ''Scope
-makeLenses ''ModuleEntry'
 
 newtype ModulesCache = ModulesCache
-  { _cachedModules :: HashMap TopModulePath (ModuleEntry' 'ModuleTop)
+  { _cachedModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop)
   }
 
 makeLenses ''ModulesCache
@@ -73,20 +53,23 @@ data ScopeParameters = ScopeParameters
     -- | Used for import cycle detection.
     _scopeTopParents :: [Import 'Parsed]
   }
+
 makeLenses ''ScopeParameters
 
 data ScoperState = ScoperState
   { _scoperModulesCache :: ModulesCache,
     _scoperFreeNames :: Stream S.NameId,
-    _scoperModules :: HashMap S.ModuleNameId ModuleEntry
+    _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete)
   }
+
 makeLenses ''ScoperState
 
 emptyScope :: S.AbsModulePath -> Scope
-emptyScope absPath = Scope
-        { _scopePath = absPath,
-          _scopeFixities = mempty,
-          _scopeSymbols = mempty,
-          _scopeTopModules = mempty,
-          _scopeBindGroup = mempty
-        }
+emptyScope absPath =
+  Scope
+    { _scopePath = absPath,
+      _scopeFixities = mempty,
+      _scopeSymbols = mempty,
+      _scopeTopModules = mempty,
+      _scopeBindGroup = mempty
+    }
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
index 9a50762b6..3f375e3b3 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
@@ -6,39 +6,46 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Scoper where
 
 import qualified Control.Monad.Combinators.Expr as P
+import Data.Functor.Identity
 import qualified Data.HashMap.Strict as HashMap
 import qualified Data.HashSet as HashSet
+import qualified Data.List.NonEmpty as NonEmpty
 import qualified Data.Stream as Stream
 import Lens.Micro.Platform
+import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Concrete.Base as P
 import MiniJuvix.Syntax.Concrete.Language
 import MiniJuvix.Syntax.Concrete.Parser (runModuleParser)
+import MiniJuvix.Syntax.Concrete.Scoped.Error
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Concrete.Scoped.Scope
-import MiniJuvix.Syntax.Concrete.Scoped.Error
-import MiniJuvix.Prelude
-import qualified Data.List.NonEmpty as NonEmpty
 import MiniJuvix.Syntax.Concrete.Scoped.Scoper.Files
 
 --------------------------------------------------------------------------------
 
 scopeCheck1IO :: FilePath -> Module 'Parsed 'ModuleTop -> IO (Either ScopeError (Module 'Scoped 'ModuleTop))
-scopeCheck1IO root = runM . runFilesIO . scopeCheck1 root
+scopeCheck1IO root = runFinal . embedToFinal @IO . runFilesIO . fixpointToFinal @IO . scopeCheck1 root
 
-scopeCheck1Pure :: HashMap FilePath Text -> FilePath -> Module 'Parsed 'ModuleTop -> IO (Either ScopeError (Module 'Scoped 'ModuleTop))
-scopeCheck1Pure fs root = runM . runFilesPure fs . scopeCheck1 root
+scopeCheck1Pure :: HashMap FilePath Text -> FilePath -> Module 'Parsed 'ModuleTop -> Either ScopeError (Module 'Scoped 'ModuleTop)
+scopeCheck1Pure fs root = runIdentity . runFinal . runFilesPure fs . fixpointToFinal @Identity . scopeCheck1 root
 
-scopeCheck1 :: Member Files r =>
-  FilePath -> Module 'Parsed 'ModuleTop -> Sem r (Either ScopeError (Module 'Scoped 'ModuleTop))
+scopeCheck1 ::
+  Members [Files, Fixpoint] r =>
+  FilePath ->
+  Module 'Parsed 'ModuleTop ->
+  Sem r (Either ScopeError (Module 'Scoped 'ModuleTop))
 scopeCheck1 root m = fmap head <$> scopeCheck root (pure m)
 
-scopeCheck :: Member Files r =>
-    FilePath -> NonEmpty (Module 'Parsed 'ModuleTop) -> Sem r (Either ScopeError (NonEmpty (Module 'Scoped 'ModuleTop)))
+scopeCheck ::
+  Members [Files, Fixpoint] r =>
+  FilePath ->
+  NonEmpty (Module 'Parsed 'ModuleTop) ->
+  Sem r (Either ScopeError (NonEmpty (Module 'Scoped 'ModuleTop)))
 scopeCheck root modules =
-    runError $
-      runReader scopeParameters $
-        evalState iniScoperState $
-          mapM checkTopModule_ modules
+  runError $
+    runReader scopeParameters $
+      evalState iniScoperState $
+        mapM checkTopModule_ modules
   where
     iniScoperState :: ScoperState
     iniScoperState =
@@ -97,34 +104,32 @@ reserveSymbolOf k s = do
   checkNotBound
   freshSymbol k s
   where
-  checkNotBound :: Sem r ()
-  checkNotBound = do
-    path <- gets _scopePath
-    syms <- gets _scopeSymbols
-    let exists = HashMap.lookup s syms >>= HashMap.lookup path . _symbolInfo
-    whenJust exists $
-      \ e -> throw (ErrMultipleDeclarations
-         MultipleDeclarations {
-         _multipleDeclEntry = e,
-         _multipleDeclSymbol = _symbolText s,
-         _multipleDeclSecond = getLoc s
-         })
-
-symbolEntry :: S.Name' a -> SymbolEntry
-symbolEntry S.Name' {..} = S.Name'
-  { _nameConcrete = (), ..}
+    checkNotBound :: Sem r ()
+    checkNotBound = do
+      path <- gets _scopePath
+      syms <- gets _scopeSymbols
+      let exists = HashMap.lookup s syms >>= HashMap.lookup path . _symbolInfo
+      whenJust exists $
+        \e ->
+          throw
+            ( ErrMultipleDeclarations
+                MultipleDeclarations
+                  { _multipleDeclEntry = e,
+                    _multipleDeclSymbol = _symbolText s,
+                    _multipleDeclSecond = getLoc s
+                  }
+            )
 
 bindReservedSymbol ::
   Members '[State Scope] r =>
   S.Symbol ->
+  SymbolEntry ->
   Sem r ()
-bindReservedSymbol s' = do
+bindReservedSymbol s' entry = do
   path <- gets _scopePath
   modify (over scopeSymbols (HashMap.alter (Just . addS path) s))
   where
     s = S._nameConcrete s'
-    entry :: SymbolEntry
-    entry = symbolEntry s'
     addS :: S.AbsModulePath -> Maybe SymbolInfo -> SymbolInfo
     addS path m = case m of
       Nothing -> symbolInfoSingle entry
@@ -133,70 +138,93 @@ bindReservedSymbol s' = do
 bindSymbolOf ::
   Members '[Error ScopeError, State ScoperState, State Scope] r =>
   S.NameKind ->
+  (S.Name' () -> SymbolEntry) ->
   Symbol ->
   Sem r S.Symbol
-bindSymbolOf k s = do
+bindSymbolOf k e s = do
   s' <- reserveSymbolOf k s
-  bindReservedSymbol s'
+  bindReservedSymbol s' (e (set S.nameConcrete () s'))
   return s'
 
 bindFunctionSymbol ::
   Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Expression ->
   Symbol ->
   Sem r S.Symbol
-bindFunctionSymbol = bindSymbolOf S.KNameFunction
+bindFunctionSymbol sig =
+  bindSymbolOf
+    S.KNameFunction
+    (\s' -> EntryFunction (FunctionRef' s' sig))
 
 bindInductiveSymbol ::
   Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  InductiveDef 'Scoped ->
   Symbol ->
   Sem r S.Symbol
-bindInductiveSymbol = bindSymbolOf S.KNameInductive
+bindInductiveSymbol def =
+  bindSymbolOf
+    S.KNameInductive
+    (\s' -> EntryInductive (InductiveRef' s' def))
 
 bindAxiomSymbol ::
   Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  HashMap Backend Text ->
+  Expression ->
   Symbol ->
   Sem r S.Symbol
-bindAxiomSymbol = bindSymbolOf S.KNameAxiom
-
-bindLocalModuleSymbol ::
-  Members '[Error ScopeError, State ScoperState, State Scope] r =>
-  Symbol ->
-  Sem r S.Symbol
-bindLocalModuleSymbol = bindSymbolOf S.KNameLocalModule
+bindAxiomSymbol backends ty =
+  bindSymbolOf
+    S.KNameAxiom
+    (\s' -> EntryAxiom (AxiomRef' s' ty backends))
 
 bindConstructorSymbol ::
   Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Expression ->
   Symbol ->
   Sem r S.Symbol
-bindConstructorSymbol = bindSymbolOf S.KNameConstructor
+bindConstructorSymbol sig =
+  bindSymbolOf
+    S.KNameConstructor
+    (\s' -> EntryConstructor (ConstructorRef' s' sig))
+
+bindLocalModuleSymbol ::
+  Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  ExportInfo ->
+  Module 'Scoped 'ModuleLocal ->
+  Symbol ->
+  Sem r S.Symbol
+bindLocalModuleSymbol _moduleExportInfo _moduleRefModule =
+  bindSymbolOf
+    S.KNameLocalModule
+    (\_moduleRefName -> EntryModule (mkModuleRef' (ModuleRef'' {..})))
 
 checkImport ::
   forall r.
-  Members '[Error ScopeError, State Scope, Reader ScopeParameters, Files, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, Reader ScopeParameters, Files, State ScoperState, Fixpoint] r =>
   Import 'Parsed ->
   Sem r (Import 'Scoped)
 checkImport import_@(Import path) = do
   checkCycle
   cache <- gets (_cachedModules . _scoperModulesCache)
-  entry' <- maybe (readParseModule path >>= local addImport . checkTopModule) return (cache ^. at path)
-  let checked = entry' ^. moduleEntryScoped
+  moduleRef <- maybe (readParseModule path >>= local addImport . checkTopModule) return (cache ^. at path)
+  let checked = moduleRef ^. moduleRefModule
       sname = checked ^. modulePath
       moduleId = sname ^. S.nameId
-  modify (over scopeTopModules (HashMap.insert path moduleId))
-  let entry = mkModuleEntry entry'
-  modify (over scoperModules (HashMap.insert moduleId entry))
+  modify (over scopeTopModules (HashMap.insert path moduleRef))
+  let moduleRef' = mkModuleRef' moduleRef
+  modify (over scoperModules (HashMap.insert moduleId moduleRef'))
   return (Import checked)
   where
-  addImport :: ScopeParameters -> ScopeParameters
-  addImport = over scopeTopParents (cons import_)
-  checkCycle :: Sem r ()
-  checkCycle = do
-    topp <- asks _scopeTopParents
-    case span (/= import_) topp of
-      (_, []) -> return ()
-      (c, _) -> let cyc = NonEmpty.reverse (import_ :| c)
-                in throw (ErrImportCycle (ImportCycle cyc))
-
+    addImport :: ScopeParameters -> ScopeParameters
+    addImport = over scopeTopParents (cons import_)
+    checkCycle :: Sem r ()
+    checkCycle = do
+      topp <- asks _scopeTopParents
+      case span (/= import_) topp of
+        (_, []) -> return ()
+        (c, _) ->
+          let cyc = NonEmpty.reverse (import_ :| c)
+           in throw (ErrImportCycle (ImportCycle cyc))
 
 getTopModulePath :: Module 'Parsed 'ModuleTop -> S.AbsModulePath
 getTopModulePath Module {..} =
@@ -206,118 +234,111 @@ getTopModulePath Module {..} =
     }
 
 -- | Do not call directly. Looks for a symbol in (possibly) nested local modules
-lookupSymbolAux :: forall r. (Members '[State Scope, Error ScopeError, State ScoperState] r) =>
-   [Symbol] -> Symbol -> Sem r [SymbolEntry]
+lookupSymbolAux ::
+  forall r.
+  (Members '[State Scope, Error ScopeError] r) =>
+  [Symbol] ->
+  Symbol ->
+  Sem r [SymbolEntry]
 lookupSymbolAux modules final = do
   local' <- hereOrInLocalModule
   import' <- importedTopModule
   return $ local' ++ maybeToList import'
   where
-  hereOrInLocalModule :: Sem r [SymbolEntry] =
-    case modules of
-      [] -> do
-         r <- HashMap.lookup final <$> gets _scopeSymbols
-         case r of
-          Nothing -> return []
-          Just SymbolInfo {..} -> case toList _symbolInfo of
-            [] -> return []
-            [e] -> return [e]
-            es -> throw (ErrAmbiguousSym (AmbiguousSym es))
-      (p : ps) -> do
-        r <- fmap (filter S.isModuleKind . toList . _symbolInfo)
-          . HashMap.lookup p <$> gets _scopeSymbols
-        case r of
-          Just [x] -> do
-            export <- getExportInfo (S._nameId x)
-            maybeToList <$> lookInExport final ps export
-          Just [] -> return []
-          Just es -> throw $ ErrAmbiguousSym (AmbiguousSym es)
-          Nothing -> return []
-  importedTopModule :: Sem r (Maybe SymbolEntry)
-  importedTopModule = do
-    fmap mkEntry . HashMap.lookup path <$> gets _scopeTopModules
-    where
-    mkEntry modId = S.Name' {
-         _nameConcrete = (),
-         _nameKind = S.KNameTopModule,
-         _nameDefinedIn = S.topModulePathToAbsPath path,
-         _nameDefined = getLoc final,
-         _nameId = modId,
-         _nameFixity = Nothing,
-         _nameWhyInScope = S.BecauseImportedOpened,
-         _namePublicAnn = NoPublic}
-    path = TopModulePath modules final
+    hereOrInLocalModule :: Sem r [SymbolEntry] =
+      case modules of
+        [] -> do
+          r <- HashMap.lookup final <$> gets _scopeSymbols
+          case r of
+            Nothing -> return []
+            Just SymbolInfo {..} -> case toList _symbolInfo of
+              [] -> return []
+              [e] -> return [e]
+              es -> throw (ErrAmbiguousSym (AmbiguousSym es))
+        (p : ps) ->
+          mapMaybe (lookInExport final ps . getModuleExportInfo) . concat . maybeToList . fmap (mapMaybe getModuleRef . toList . _symbolInfo)
+            . HashMap.lookup p
+            <$> gets _scopeSymbols
+    importedTopModule :: Sem r (Maybe SymbolEntry)
+    importedTopModule = do
+      fmap (EntryModule . mkModuleRef') . HashMap.lookup path <$> gets _scopeTopModules
+      where
+        path = TopModulePath modules final
 
-lookInExport :: forall r. Members '[State Scope, State ScoperState] r =>
-  Symbol -> [Symbol] -> ExportInfo -> Sem r (Maybe SymbolEntry)
+lookInExport :: Symbol -> [Symbol] -> ExportInfo -> Maybe SymbolEntry
 lookInExport sym remaining e = case remaining of
-  [] -> return (HashMap.lookup sym (_exportSymbols e))
+  [] -> HashMap.lookup sym (_exportSymbols e)
   (s : ss) -> do
-    mexport <- mayModule e s
-    case mexport of
-      Nothing -> return Nothing
-      Just e' -> lookInExport sym ss e'
- where
-  mayModule :: ExportInfo -> Symbol -> Sem r (Maybe ExportInfo)
-  mayModule ExportInfo {..} s =
-    case do
+    export <- mayModule e s
+    lookInExport sym ss export
+  where
+    mayModule :: ExportInfo -> Symbol -> Maybe ExportInfo
+    mayModule ExportInfo {..} s = do
       entry <- HashMap.lookup s _exportSymbols
-      guard (S.isModuleKind entry)
-      return entry of
-        Just entry -> Just <$> getExportInfo (S._nameId entry)
-        Nothing -> return Nothing
+      case entry of
+        EntryModule m -> Just (getModuleExportInfo m)
+        _ -> Nothing
 
 -- | We return a list of entries because qualified names can point to different
 -- modules due to nesting.
-lookupQualifiedSymbol :: forall r. Members '[State Scope, Error ScopeError, State ScoperState] r =>
-   ([Symbol], Symbol) -> Sem r [SymbolEntry]
+lookupQualifiedSymbol ::
+  forall r.
+  Members '[State Scope, Error ScopeError, State ScoperState] r =>
+  ([Symbol], Symbol) ->
+  Sem r [SymbolEntry]
 lookupQualifiedSymbol (path, sym) = do
   here' <- here
   there' <- there
   return (here' ++ there')
   where
-  -- | Current module.
-  here :: Sem r [SymbolEntry]
-  here = lookupSymbolAux path sym
-  -- | Looks for a top level modules
-  there :: Sem r [SymbolEntry]
-  there = concatMapM (fmap maybeToList . uncurry lookInTopModule) allTopPaths
-    where
-    allTopPaths :: [(TopModulePath, [Symbol])]
-    allTopPaths = map (first nonEmptyToTopPath) raw
+    -- Current module.
+    here :: Sem r [SymbolEntry]
+    here = lookupSymbolAux path sym
+    -- Looks for a top level modules
+    there :: Sem r [SymbolEntry]
+    there = concatMapM (fmap maybeToList . uncurry lookInTopModule) allTopPaths
       where
-      lpath = toList path
-      raw :: [(NonEmpty Symbol, [Symbol])]
-      raw = [  (l, r) | i <- [1..length path],
-              (Just l, r) <- [ first nonEmpty (splitAt i lpath) ]]
-      nonEmptyToTopPath :: NonEmpty Symbol -> TopModulePath
-      nonEmptyToTopPath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
-    lookInTopModule :: TopModulePath -> [Symbol] -> Sem r (Maybe SymbolEntry)
-    lookInTopModule topPath remaining = do
-      r <- HashMap.lookup topPath <$> gets _scopeTopModules
-      case r of
-        Nothing -> return Nothing
-        Just i -> getExportInfo i >>= lookInExport sym remaining
+        allTopPaths :: [(TopModulePath, [Symbol])]
+        allTopPaths = map (first nonEmptyToTopPath) raw
+          where
+            lpath = toList path
+            raw :: [(NonEmpty Symbol, [Symbol])]
+            raw =
+              [ (l, r) | i <- [1 .. length path], (Just l, r) <- [first nonEmpty (splitAt i lpath)]
+              ]
+            nonEmptyToTopPath :: NonEmpty Symbol -> TopModulePath
+            nonEmptyToTopPath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
+        lookInTopModule :: TopModulePath -> [Symbol] -> Sem r (Maybe SymbolEntry)
+        lookInTopModule topPath remaining =
+          ((fmap (^. moduleExportInfo) . HashMap.lookup topPath) >=> lookInExport sym remaining) <$> gets _scopeTopModules
 
 checkQualifiedExpr ::
   Members '[Error ScopeError, State Scope, State ScoperState] r =>
   QualifiedName ->
-  Sem r S.Name
+  Sem r ScopedIden
 checkQualifiedExpr q@(QualifiedName (Path p) sym) = do
-   es <- lookupQualifiedSymbol (toList p, sym)
-   case es of
-     [] -> notInScope
-     [e] -> return (entryToSName q' e)
-     _ -> throw (ErrAmbiguousSym (AmbiguousSym es))
+  es <- lookupQualifiedSymbol (toList p, sym)
+  case es of
+    [] -> notInScope
+    [e] -> return (entryToScopedIden q' e)
+    _ -> throw (ErrAmbiguousSym (AmbiguousSym es))
   where
-  q' = NameQualified q
-  notInScope = throw (ErrQualSymNotInScope q)
+    q' = NameQualified q
+    notInScope = throw (ErrQualSymNotInScope q)
 
 unqualifiedSName :: S.Symbol -> S.Name
 unqualifiedSName = over S.nameConcrete NameUnqualified
 
-entryToSName :: s -> SymbolEntry -> S.Name' s
-entryToSName s S.Name' {..} = S.Name' {_nameConcrete = s, ..}
+entryToScopedIden :: Name -> SymbolEntry -> ScopedIden
+entryToScopedIden name = \case
+  EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref)
+  EntryInductive ref ->
+    ScopedInductive (set (inductiveRefName . S.nameConcrete) name ref)
+  EntryConstructor ref ->
+    ScopedConstructor (set (constructorRefName . S.nameConcrete) name ref)
+  EntryFunction ref ->
+    ScopedFunction (set (functionRefName . S.nameConcrete) name ref)
+  EntryModule {} -> impossible
 
 -- | We gather all symbols which have been defined or marked to be public in the given scope.
 exportScope :: forall r. Members '[State Scope, Error ScopeError] r => Scope -> Sem r ExportInfo
@@ -329,16 +350,22 @@ exportScope Scope {..} = do
     getExportSymbols = HashMap.fromList <$> mapMaybeM entry (HashMap.toList _scopeSymbols)
       where
         shouldExport :: SymbolEntry -> Bool
-        shouldExport S.Name' {..} =
+        shouldExport ent =
           _nameDefinedIn == _scopePath
             || _namePublicAnn == Public
+          where
+            S.Name' {..} = entryName ent
+
         entry :: (Symbol, SymbolInfo) -> Sem r (Maybe (Symbol, SymbolEntry))
         entry (s, SymbolInfo {..}) =
           case filter shouldExport (toList _symbolInfo) of
             [] -> return Nothing
             [e] -> return $ Just (s, e)
-            (e:es) -> throw (ErrMultipleExport
-                       (MultipleExportConflict _scopePath  s (e :| es)))
+            (e : es) ->
+              throw
+                ( ErrMultipleExport
+                    (MultipleExportConflict _scopePath s (e :| es))
+                )
 
 readParseModule ::
   Members '[Error ScopeError, Reader ScopeParameters, Files] r =>
@@ -381,7 +408,7 @@ checkTypeSignature ::
   Sem r (TypeSignature 'Scoped)
 checkTypeSignature TypeSignature {..} = do
   sigType' <- checkParseExpressionAtoms _sigType
-  sigName' <- bindFunctionSymbol _sigName
+  sigName' <- bindFunctionSymbol sigType' _sigName
   return
     TypeSignature
       { _sigName = sigName',
@@ -394,104 +421,119 @@ checkConstructorDef ::
   Sem r (InductiveConstructorDef 'Scoped)
 checkConstructorDef InductiveConstructorDef {..} = do
   constructorType' <- checkParseExpressionAtoms constructorType
-  constructorName' <- bindConstructorSymbol constructorName
+  constructorName' <- bindConstructorSymbol constructorType' constructorName
   return
     InductiveConstructorDef
       { constructorName = constructorName',
         constructorType = constructorType'
       }
 
-withParams :: forall r a. Members '[Reader LocalVars, Error ScopeError, State Scope, State ScoperState] r
-  => [InductiveParameter 'Parsed] -> ([InductiveParameter 'Scoped] -> Sem r a) -> Sem r a
+withParams ::
+  forall r a.
+  Members '[Reader LocalVars, Error ScopeError, State Scope, State ScoperState] r =>
+  [InductiveParameter 'Parsed] ->
+  ([InductiveParameter 'Scoped] -> Sem r a) ->
+  Sem r a
 withParams xs a = go [] xs
   where
-  go :: [InductiveParameter 'Scoped] -> [InductiveParameter 'Parsed] -> Sem r a
-  go inductiveParameters' params =
-    case params of
-      -- More params to check
-      (InductiveParameter {..} : ps) -> do
-        inductiveParameterType' <- checkParseExpressionAtoms _inductiveParameterType
-        inductiveParameterName' <- freshVariable _inductiveParameterName
-        let param' =
-              InductiveParameter
-                { _inductiveParameterType = inductiveParameterType',
-                  _inductiveParameterName = inductiveParameterName'
-                }
-        withBindLocalVariable (LocalVariable inductiveParameterName') $
-          go (inductiveParameters' ++ [param']) ps
-      -- All params have been checked
-      [] -> a inductiveParameters'
+    go :: [InductiveParameter 'Scoped] -> [InductiveParameter 'Parsed] -> Sem r a
+    go inductiveParameters' params =
+      case params of
+        -- More params to check
+        (InductiveParameter {..} : ps) -> do
+          inductiveParameterType' <- checkParseExpressionAtoms _inductiveParameterType
+          inductiveParameterName' <- freshVariable _inductiveParameterName
+          let param' =
+                InductiveParameter
+                  { _inductiveParameterType = inductiveParameterType',
+                    _inductiveParameterName = inductiveParameterName'
+                  }
+          withBindLocalVariable (LocalVariable inductiveParameterName') $
+            go (inductiveParameters' ++ [param']) ps
+        -- All params have been checked
+        [] -> a inductiveParameters'
 
-checkInductiveDef :: forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+checkInductiveDef ::
+  forall r.
+  Members '[Error ScopeError, State Scope, State ScoperState, Fixpoint, Reader LocalVars] r =>
   InductiveDef 'Parsed ->
   Sem r (InductiveDef 'Scoped)
 checkInductiveDef InductiveDef {..} = do
   withParams _inductiveParameters $ \inductiveParameters' -> do
     inductiveType' <- sequence (checkParseExpressionAtoms <$> _inductiveType)
-    inductiveName' <- bindInductiveSymbol _inductiveName
-    inductiveConstructors' <- mapM checkConstructorDef _inductiveConstructors
-    return InductiveDef
-      { _inductiveName = inductiveName',
-        _inductiveParameters = inductiveParameters',
-        _inductiveType = inductiveType',
-        _inductiveConstructors = inductiveConstructors'
-      }
+    mfix $ \scopedDef -> do
+      inductiveName' <- bindInductiveSymbol scopedDef _inductiveName
+      inductiveConstructors' <- mapM checkConstructorDef _inductiveConstructors
+      return
+        InductiveDef
+          { _inductiveName = inductiveName',
+            _inductiveParameters = inductiveParameters',
+            _inductiveType = inductiveType',
+            _inductiveConstructors = inductiveConstructors'
+          }
 
 checkTopModule_ ::
   forall r.
-  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState] r =>
+  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint] r =>
   Module 'Parsed 'ModuleTop ->
   Sem r (Module 'Scoped 'ModuleTop)
-checkTopModule_ = fmap _moduleEntryScoped . checkTopModule
+checkTopModule_ = fmap (^. moduleRefModule) . checkTopModule
 
 checkTopModule ::
   forall r.
-  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState] r =>
+  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint] r =>
   Module 'Parsed 'ModuleTop ->
-  Sem r (ModuleEntry' 'ModuleTop)
+  Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
 checkTopModule m@(Module path params body) = do
   checkPath
   r <- checkedModule
   modify (over (scoperModulesCache . cachedModules) (HashMap.insert path r))
   return r
   where
-  checkPath :: Members '[Files, Reader ScopeParameters, Error ScopeError] s => Sem s ()
-  checkPath = do
-    expectedPath <- modulePathToFilePath path
-    let actualPath = getLoc path ^. intFile
-    unlessM (fromMaybe True <$> equalPaths' expectedPath actualPath) $
-      throw (ErrWrongTopModuleName
-      WrongTopModuleName {
-       _wrongTopModuleNameActualName = path,
-       _wrongTopModuleNameExpectedPath = expectedPath,
-       _wrongTopModuleNameActualPath = actualPath
-      })
-  freshTopModulePath :: forall s. Members '[State ScoperState] s =>
-     Sem s S.TopModulePath
-  freshTopModulePath = do
-    _nameId <- freshNameId
-    let _nameDefinedIn = S.topModulePathToAbsPath path
-        _nameConcrete = path
-        _nameDefined = getLoc (_modulePathName path)
-        _nameKind = S.KNameTopModule
-        _nameFixity = Nothing
-        _namePublicAnn = NoPublic
-        _nameWhyInScope = S.BecauseDefined
-    return S.Name' {..}
-  iniScope :: Scope
-  iniScope = emptyScope (getTopModulePath m)
-  checkedModule :: Sem r (ModuleEntry' 'ModuleTop)
-  checkedModule = do
-    evalState iniScope $ do
-      path' <- freshTopModulePath
-      localScope $ withParams params $ \params' -> do
-        (_moduleEntryExport, body') <- checkModuleBody body
-        let _moduleEntryScoped = Module {
-          _modulePath = path',
-          _moduleParameters = params',
-          _moduleBody = body' }
-        return ModuleEntry' {..}
+    checkPath :: Members '[Files, Reader ScopeParameters, Error ScopeError] s => Sem s ()
+    checkPath = do
+      expectedPath <- modulePathToFilePath path
+      let actualPath = getLoc path ^. intFile
+      unlessM (fromMaybe True <$> equalPaths' expectedPath actualPath) $
+        throw
+          ( ErrWrongTopModuleName
+              WrongTopModuleName
+                { _wrongTopModuleNameActualName = path,
+                  _wrongTopModuleNameExpectedPath = expectedPath,
+                  _wrongTopModuleNameActualPath = actualPath
+                }
+          )
+    freshTopModulePath ::
+      forall s.
+      Members '[State ScoperState] s =>
+      Sem s S.TopModulePath
+    freshTopModulePath = do
+      _nameId <- freshNameId
+      let _nameDefinedIn = S.topModulePathToAbsPath path
+          _nameConcrete = path
+          _nameDefined = getLoc (_modulePathName path)
+          _nameKind = S.KNameTopModule
+          _nameFixity = Nothing
+          _namePublicAnn = NoPublic
+          _nameWhyInScope = S.BecauseDefined
+      return S.Name' {..}
+    iniScope :: Scope
+    iniScope = emptyScope (getTopModulePath m)
+    checkedModule :: Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
+    checkedModule = do
+      evalState iniScope $ do
+        path' <- freshTopModulePath
+        localScope $
+          withParams params $ \params' -> do
+            (_moduleExportInfo, body') <- checkModuleBody body
+            let _moduleRefModule =
+                  Module
+                    { _modulePath = path',
+                      _moduleParameters = params',
+                      _moduleBody = body'
+                    }
+                _moduleRefName = set S.nameConcrete () path'
+            return ModuleRef'' {..}
 
 withScope :: Members '[State Scope] r => Sem r a -> Sem r a
 withScope ma = do
@@ -500,8 +542,9 @@ withScope ma = do
   put before
   return x
 
-checkModuleBody :: forall r.
-  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars] r =>
+checkModuleBody ::
+  forall r.
+  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint] r =>
   [Statement 'Parsed] ->
   Sem r (ExportInfo, [Statement 'Scoped])
 checkModuleBody body = do
@@ -513,44 +556,52 @@ checkModuleBody body = do
 
 checkLocalModule ::
   forall r.
-  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint] r =>
   Module 'Parsed 'ModuleLocal ->
   Sem r (Module 'Scoped 'ModuleLocal)
 checkLocalModule Module {..} = do
-  (_moduleEntryExport, moduleBody', moduleParameters') <-
-      withScope $ withParams _moduleParameters $ \p' -> do
-    inheritScope
-    (e, b) <- checkModuleBody _moduleBody
-    return (e, b, p')
-  modulePath' <- bindLocalModuleSymbol _modulePath
-  let moduleId = S._nameId modulePath'
-      _moduleEntryScoped = Module
-        { _modulePath = modulePath',
-          _moduleParameters = moduleParameters',
-          _moduleBody = moduleBody'
-        }
-      entry = mkModuleEntry ModuleEntry' {..}
-  modify (over scoperModules (HashMap.insert moduleId entry))
-  return _moduleEntryScoped
+  (_moduleExportInfo, moduleBody', moduleParameters') <-
+    withScope $
+      withParams _moduleParameters $ \p' -> do
+        inheritScope
+        (e, b) <- checkModuleBody _moduleBody
+        return (e, b, p')
+  mfix $ \scopedModule -> do
+    modulePath' <- bindLocalModuleSymbol _moduleExportInfo scopedModule _modulePath
+    let moduleId = S._nameId modulePath'
+        _moduleRefName = set S.nameConcrete () modulePath'
+        _moduleRefModule =
+          Module
+            { _modulePath = modulePath',
+              _moduleParameters = moduleParameters',
+              _moduleBody = moduleBody'
+            }
+        entry :: ModuleRef' 'S.NotConcrete
+        entry = mkModuleRef' @'ModuleLocal ModuleRef'' {..}
+    modify (over scoperModules (HashMap.insert moduleId entry))
+    return _moduleRefModule
   where
-  inheritScope :: Sem r ()
-  inheritScope = do
-    absPath <- (S.<.> _modulePath) <$> gets _scopePath
-    modify (set scopePath absPath)
-    modify (over scopeSymbols (fmap inheritSymbol))
-    modify (set scopeFixities mempty) -- do not inherit fixity declarations
-    where
-    inheritSymbol :: SymbolInfo -> SymbolInfo
-    inheritSymbol (SymbolInfo s) = SymbolInfo (fmap inheritEntry s)
-    inheritEntry :: SymbolEntry -> SymbolEntry
-    inheritEntry = over S.nameWhyInScope S.BecauseInherited
+    inheritScope :: Sem r ()
+    inheritScope = do
+      absPath <- (S.<.> _modulePath) <$> gets _scopePath
+      modify (set scopePath absPath)
+      modify (over scopeSymbols (fmap inheritSymbol))
+      modify (set scopeFixities mempty) -- do not inherit fixity declarations
+      where
+        inheritSymbol :: SymbolInfo -> SymbolInfo
+        inheritSymbol (SymbolInfo s) = SymbolInfo (fmap inheritEntry s)
+        inheritEntry :: SymbolEntry -> SymbolEntry
+        inheritEntry = entryOverName (over S.nameWhyInScope S.BecauseInherited)
 
 checkClausesExist :: forall r. Members '[Error ScopeError, State Scope] r => [Statement 'Scoped] -> Sem r ()
 checkClausesExist ss = whenJust msig (throw . ErrLacksFunctionClause . LacksFunctionClause)
   where
-  msig = listToMaybe [ ts | StatementTypeSignature ts <- ss,
-          null [ c | StatementFunctionClause c <- ss ,
-                 c ^. clauseOwnerFunction == ts ^. sigName]]
+    msig =
+      listToMaybe
+        [ ts | StatementTypeSignature ts <- ss, null
+                                                  [ c | StatementFunctionClause c <- ss, c ^. clauseOwnerFunction == ts ^. sigName
+                                                  ]
+        ]
 
 checkOrphanFixities :: forall r. Members '[Error ScopeError, State Scope] r => Sem r ()
 checkOrphanFixities = do
@@ -563,29 +614,40 @@ checkOrphanFixities = do
     (x : _) -> throw (ErrUnusedOperatorDef (UnusedOperatorDef x))
 
 symbolInfoSingle :: SymbolEntry -> SymbolInfo
-symbolInfoSingle p = SymbolInfo $ HashMap.singleton (S._nameDefinedIn p) p
+symbolInfoSingle p = SymbolInfo $ HashMap.singleton (entryName p ^. S.nameDefinedIn) p
 
-lookupModuleSymbol :: Members '[Error ScopeError, State Scope, State ScoperState] r =>
-  Name -> Sem r S.Name
+lookupModuleSymbol ::
+  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Name ->
+  Sem r ModuleRef
 lookupModuleSymbol n = do
   es <- lookupQualifiedSymbol (path, sym)
-  case filter S.isModuleKind es of
+  case mapMaybe getModuleRef es of
     [] -> notInScope
-    [x] -> return $ entryToSName n x
+    [x] -> return (overModuleRef'' (set (moduleRefName . S.nameConcrete) n) x)
     _ -> throw (ErrAmbiguousModuleSym (AmbiguousModuleSym es))
   where
-  notInScope = throw (ErrModuleNotInScope (ModuleNotInScope n))
-  (path, sym) = case n of
-    NameUnqualified s -> ([], s)
-    NameQualified (QualifiedName (Path p) s) -> (toList p, s)
+    notInScope = throw (ErrModuleNotInScope (ModuleNotInScope n))
+    (path, sym) = case n of
+      NameUnqualified s -> ([], s)
+      NameQualified (QualifiedName (Path p) s) -> (toList p, s)
 
-getExportInfo :: forall r. Members '[State ScoperState] r =>
- S.ModuleNameId -> Sem r ExportInfo
+getModuleRef :: SymbolEntry -> Maybe (ModuleRef' 'S.NotConcrete)
+getModuleRef = \case
+  EntryModule m -> Just m
+  _ -> Nothing
+
+getExportInfo ::
+  forall r.
+  Members '[State ScoperState] r =>
+  S.ModuleNameId ->
+  Sem r ExportInfo
 getExportInfo modId = do
-  l <- HashMap.lookupDefault impossible modId
-        <$> gets _scoperModules
-  case l of
-    _ :&: ent -> return $ _moduleEntryExport ent
+  l <-
+    HashMap.lookupDefault impossible modId
+      <$> gets _scoperModules
+  return $ case l ^. unModuleRef' of
+    _ :&: ent -> ent ^. moduleExportInfo
 
 checkOpenModule ::
   forall r.
@@ -593,16 +655,16 @@ checkOpenModule ::
   OpenModule 'Parsed ->
   Sem r (OpenModule 'Scoped)
 checkOpenModule OpenModule {..} = do
+  openModuleName'@(ModuleRef' (_ :&: moduleRef'')) <- lookupModuleSymbol openModuleName
   openParameters' <- mapM checkParseExpressionAtoms openParameters
-  openModuleName' <- lookupModuleSymbol openModuleName
-  exported <- getExportInfo (S._nameId openModuleName')
-  mergeScope (alterScope exported)
-  return OpenModule {
-    openModuleName = openModuleName',
-    openParameters = openParameters',
-    openUsingHiding = openUsingHiding,
-    openPublic = openPublic
-    }
+  mergeScope (alterScope (moduleRef'' ^. moduleExportInfo))
+  return
+    OpenModule
+      { openModuleName = openModuleName',
+        openParameters = openParameters',
+        openUsingHiding = openUsingHiding,
+        openPublic = openPublic
+      }
   where
     mergeScope :: ExportInfo -> Sem r ()
     mergeScope ExportInfo {..} =
@@ -621,7 +683,7 @@ checkOpenModule OpenModule {..} = do
     alterScope = alterEntries . filterScope
       where
         alterEntry :: SymbolEntry -> SymbolEntry
-        alterEntry = set S.nameWhyInScope S.BecauseImportedOpened . set S.namePublicAnn openPublic
+        alterEntry = entryOverName (set S.nameWhyInScope S.BecauseImportedOpened . set S.namePublicAnn openPublic)
         alterEntries :: ExportInfo -> ExportInfo
         alterEntries = over exportSymbols (fmap alterEntry)
         filterScope :: ExportInfo -> ExportInfo
@@ -679,25 +741,17 @@ checkFunctionClause clause@FunctionClause {..} = do
     checkTypeSigInScope :: Sem r S.Symbol
     checkTypeSigInScope = do
       e <- fromMaybeM err (lookupLocalEntry fun)
-      when (S._nameKind e /= S.KNameFunction) err
-      return (entryToSName fun e)
+      case e of
+        EntryFunction ref -> return (set S.nameConcrete fun (ref ^. functionRefName))
+        _ -> err
       where
         err :: Sem r a
         err = throw (ErrLacksTypeSig (LacksTypeSig clause))
 
-lookupAxiom :: forall r.  Members '[Error ScopeError, State Scope, State ScoperState] r =>
-  Symbol -> Sem r S.Symbol
-lookupAxiom ax = do
-  e <- fromMaybeM err (lookupLocalEntry ax)
-  when (S._nameKind e /= S.KNameAxiom) err
-  return (entryToSName ax e)
-  where
-    -- TODO generate proper error
-    err :: Sem r a
-    err = throw (ErrGeneric "Axiom not in scope")
-
-lookupLocalEntry :: Members '[Error ScopeError, State Scope, State ScoperState] r =>
-  Symbol -> Sem r (Maybe SymbolEntry)
+lookupLocalEntry ::
+  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Symbol ->
+  Sem r (Maybe SymbolEntry)
 lookupLocalEntry sym = do
   ms <- HashMap.lookup sym <$> gets _scopeSymbols
   path <- gets _scopePath
@@ -706,13 +760,13 @@ lookupLocalEntry sym = do
     SymbolInfo {..} <- ms
     HashMap.lookup path _symbolInfo
 
-checkAxiom ::
+checkAxiomDef ::
   Members '[Error ScopeError, State Scope, State ScoperState] r =>
   AxiomDef 'Parsed ->
   Sem r (AxiomDef 'Scoped)
-checkAxiom AxiomDef {..} = do
-  axiomName' <- bindAxiomSymbol _axiomName
+checkAxiomDef AxiomDef {..} = do
   axiomType' <- localScope $ checkParseExpressionAtoms _axiomType
+  axiomName' <- bindAxiomSymbol undefined axiomType' _axiomName
   return
     AxiomDef
       { _axiomName = axiomName',
@@ -820,51 +874,53 @@ checkLambdaClause LambdaClause {..} = do
 checkUnqualified ::
   Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r =>
   Symbol ->
-  Sem r S.Name
+  Sem r ScopedIden
 checkUnqualified s = do
   -- Local vars have scope priority
   l <- HashMap.lookup s <$> asks _localVars
   case l of
-    Just LocalVariable {..} -> return (unqualifiedSName variableName)
+    Just LocalVariable {..} -> return (ScopedVar variableName)
     Nothing -> do
       scope <- get
       locals <- ask
       -- Lookup at the global scope
       let err = throw (ErrSymNotInScope (NotInScope s locals scope))
-      entries <- filter S.isExprKind <$>
-         lookupQualifiedSymbol ([], s)
+      entries <-
+        filter S.isExprKind
+          <$> lookupQualifiedSymbol ([], s)
       case entries of
         [] -> err
-        [x] -> return (entryToSName (NameUnqualified s) x)
+        [x] -> return (entryToScopedIden (NameUnqualified s) x)
         es -> throw (ErrAmbiguousSym (AmbiguousSym es))
 
 checkPatternName ::
   forall r.
   Members '[Error ScopeError, State Scope, State ScoperState] r =>
   Name ->
-  Sem r S.Name
+  Sem r PatternScopedIden
 checkPatternName n = do
-  c <- isConstructor
+  c <- getConstructorRef
   case c of
-    Just constr -> return constr -- the symbol is a constructor
-    Nothing -> unqualifiedSName <$> groupBindLocalVariable sym -- the symbol is a variable
+    Just constr -> return (PatternScopedConstructor constr) -- the symbol is a constructor
+    Nothing -> PatternScopedVar <$> groupBindLocalVariable sym -- the symbol is a variable
   where
     (path, sym) = case n of
       NameQualified (QualifiedName (Path p) s) -> (toList p, s)
       NameUnqualified s -> ([], s)
     -- check whether the symbol is a constructor in scope
-    isConstructor :: Sem r (Maybe S.Name)
-    isConstructor = do
-      entries <- filter (isConstructorKind . S._nameKind) <$>
-          lookupQualifiedSymbol (path, sym)
+    getConstructorRef :: Sem r (Maybe ConstructorRef)
+    getConstructorRef = do
+      entries <- mapMaybe getConstructor <$> lookupQualifiedSymbol (path, sym)
       case entries of
-            [] -> case Path <$> nonEmpty path of
-              Nothing -> return Nothing -- There is no constructor with such a name
-              Just pth -> throw (ErrQualSymNotInScope (QualifiedName pth sym))
-            [e] -> return (Just (entryToSName n e)) -- There is one constructor with such a name
-            _ -> throw $ ErrGeneric "There is more than one constructor with such a name"
-    isConstructorKind :: S.NameKind -> Bool
-    isConstructorKind = (== S.KNameConstructor)
+        [] -> case Path <$> nonEmpty path of
+          Nothing -> return Nothing -- There is no constructor with such a name
+          Just pth -> throw (ErrQualSymNotInScope (QualifiedName pth sym))
+        [e] -> return (Just (set (constructorRefName . S.nameConcrete) n e)) -- There is one constructor with such a name
+        _ -> throw $ ErrGeneric "There is more than one constructor with such a name"
+    getConstructor :: SymbolEntry -> Maybe (ConstructorRef' 'S.NotConcrete)
+    getConstructor = \case
+      EntryConstructor r -> Just r
+      _ -> Nothing
 
 withBindCurrentGroup ::
   Members '[State Scope, Reader LocalVars] r =>
@@ -901,11 +957,15 @@ groupBindLocalVariable s = do
     checkNotInGroup =
       whenJustM
         (HashMap.lookup s <$> gets _scopeBindGroup)
-        (\x -> throw (ErrBindGroup
-            BindGroupConflict {
-                _bindGroupFirst = S._nameConcrete (variableName x),
-                _bindGroupSecond =  s
-                }))
+        ( \x ->
+            throw
+              ( ErrBindGroup
+                  BindGroupConflict
+                    { _bindGroupFirst = S._nameConcrete (variableName x),
+                      _bindGroupSecond = s
+                    }
+              )
+        )
     addToGroup :: Sem r S.Symbol
     addToGroup = do
       n <- freshVariable s
@@ -926,12 +986,12 @@ checkPatternAtom p = case p of
   PatternAtomWildcard -> return PatternAtomWildcard
   PatternAtomEmpty -> return PatternAtomEmpty
   PatternAtomParens e -> PatternAtomParens <$> checkPatternAtoms e
-  PatternAtomName n -> PatternAtomName <$> checkPatternName n
+  PatternAtomIden n -> PatternAtomIden <$> checkPatternName n
 
 checkName ::
   Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r =>
   Name ->
-  Sem r S.Name
+  Sem r ScopedIden
 checkName n = case n of
   NameQualified q -> checkQualifiedExpr q
   NameUnqualified s -> checkUnqualified s
@@ -951,10 +1011,15 @@ checkExpressionAtom e = case e of
   AtomLiteral l -> return (AtomLiteral l)
   AtomMatch match -> AtomMatch <$> checkMatch match
 
-checkParens :: Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
-  ExpressionAtoms 'Parsed -> Sem r Expression
+checkParens ::
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  ExpressionAtoms 'Parsed ->
+  Sem r Expression
 checkParens e@(ExpressionAtoms as) = case as of
-  AtomIdentifier s :| [] -> ExpressionParensIdentifier . set S.nameFixity Nothing <$> checkName s
+  AtomIdentifier s :| [] -> do
+    scopedId <- checkName s
+    let scopedIdenNoFix = idenOverName (set S.nameFixity Nothing) scopedId
+    return (ExpressionParensIdentifier scopedIdenNoFix)
   _ -> checkParseExpressionAtoms e
 
 checkMatchAlt ::
@@ -1001,18 +1066,8 @@ checkParsePatternAtom ::
   Sem r Pattern
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
 
-checkCompileDef ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
-  CompileDef 'Parsed ->
-  Sem r (CompileDef 'Scoped)
-checkCompileDef CompileDef {..} = do
-  _compileAxiom' <- lookupAxiom _compileAxiom
-  return CompileDef {
-    _compileAxiom = _compileAxiom', ..
-    }
-
 checkStatement ::
-  Members '[Error ScopeError, Reader ScopeParameters, Files, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, Reader ScopeParameters, Files, State Scope, State ScoperState, Reader LocalVars, Fixpoint] r =>
   Statement 'Parsed ->
   Sem r (Statement 'Scoped)
 checkStatement s = case s of
@@ -1023,10 +1078,10 @@ checkStatement s = case s of
   StatementModule dt -> StatementModule <$> checkLocalModule dt
   StatementOpenModule open -> StatementOpenModule <$> checkOpenModule open
   StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause
-  StatementAxiom ax -> StatementAxiom <$> checkAxiom ax
+  StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax
   StatementEval e -> StatementEval <$> checkEval e
   StatementPrint e -> StatementPrint <$> checkPrint e
-  StatementCompile d -> StatementCompile <$> checkCompileDef d
+  StatementCompile {} -> undefined
   StatementForeign d -> return $ StatementForeign d
 
 -------------------------------------------------------------------------------
@@ -1036,75 +1091,77 @@ makeExpressionTable2 ::
   ExpressionAtoms 'Scoped -> [[P.Operator Parse Expression]]
 makeExpressionTable2 (ExpressionAtoms atoms) = [appOp] : operators ++ [[functionOp]]
   where
-  operators = mkSymbolTable names
-  names :: [S.Name]
-  names = mapMaybe getName (toList atoms)
-    where
-      getName :: ExpressionAtom 'Scoped -> Maybe S.Name
-      getName a = case a of
-        AtomIdentifier nm -> Just nm
-        _ -> Nothing
-  mkSymbolTable :: [S.Name] -> [[P.Operator Parse Expression]]
-  mkSymbolTable = reverse . map (map snd) . groupSortOn fst . mapMaybe mkOperator
-    where
-      mkOperator :: S.Name -> Maybe (Precedence, P.Operator Parse Expression)
-      mkOperator S.Name' {..}
-        | Just Fixity {..} <- _nameFixity = Just $
-          case fixityArity of
-            Unary u -> (fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
-              where
-                unaryApp :: S.Name -> Expression -> Expression
-                unaryApp funName arg = case u of
-                  AssocPostfix -> ExpressionPostfixApplication (PostfixApplication arg funName)
-            Binary b -> (fixityPrecedence, infixLRN (binaryApp <$> parseSymbolId _nameId))
-              where
-                binaryApp :: S.Name -> Expression -> Expression -> Expression
-                binaryApp infixAppOperator infixAppLeft infixAppRight =
-                  ExpressionInfixApplication InfixApplication {..}
-                infixLRN :: Parse (Expression -> Expression -> Expression) -> P.Operator Parse Expression
-                infixLRN = case b of
-                  AssocLeft -> P.InfixL
-                  AssocRight -> P.InfixR
-                  AssocNone -> P.InfixN
-        | otherwise = Nothing
-      parseSymbolId :: S.NameId -> Parse S.Name
-      parseSymbolId uid = P.token getName mempty
-        where
-          getName :: ExpressionAtom 'Scoped -> Maybe S.Name
-          getName s = case s of
-            AtomIdentifier n'
-              | uid == S._nameId n' -> Just n'
-            _ -> Nothing
+    operators = mkSymbolTable idens
+    idens :: [ScopedIden]
+    idens = mapMaybe getIden (toList atoms)
+      where
+        getIden :: ExpressionAtom 'Scoped -> Maybe ScopedIden
+        getIden a = case a of
+          AtomIdentifier nm -> Just nm
+          _ -> Nothing
+    mkSymbolTable :: [ScopedIden] -> [[P.Operator Parse Expression]]
+    mkSymbolTable = reverse . map (map snd) . groupSortOn fst . mapMaybe mkOperator
+      where
+        mkOperator :: ScopedIden -> Maybe (Precedence, P.Operator Parse Expression)
+        mkOperator iden
+          | Just Fixity {..} <- _nameFixity = Just $
+            case fixityArity of
+              Unary u -> (fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
+                where
+                  unaryApp :: ScopedIden -> Expression -> Expression
+                  unaryApp funName arg = case u of
+                    AssocPostfix -> ExpressionPostfixApplication (PostfixApplication arg funName)
+              Binary b -> (fixityPrecedence, infixLRN (binaryApp <$> parseSymbolId _nameId))
+                where
+                  binaryApp :: ScopedIden -> Expression -> Expression -> Expression
+                  binaryApp infixAppOperator infixAppLeft infixAppRight =
+                    ExpressionInfixApplication InfixApplication {..}
+                  infixLRN :: Parse (Expression -> Expression -> Expression) -> P.Operator Parse Expression
+                  infixLRN = case b of
+                    AssocLeft -> P.InfixL
+                    AssocRight -> P.InfixR
+                    AssocNone -> P.InfixN
+          | otherwise = Nothing
+          where
+            S.Name' {..} = identifierName iden
+        parseSymbolId :: S.NameId -> Parse ScopedIden
+        parseSymbolId uid = P.token getIdentifierWithId mempty
+          where
+            getIdentifierWithId :: ExpressionAtom 'Scoped -> Maybe ScopedIden
+            getIdentifierWithId s = case s of
+              AtomIdentifier iden
+                | uid == identifierName iden ^. S.nameId -> Just iden
+              _ -> Nothing
 
-  -- Application by juxtaposition.
-  appOp :: P.Operator Parse Expression
-  appOp = P.InfixL (return app)
-    where
-      app :: Expression -> Expression -> Expression
-      app f x =
-        ExpressionApplication
-          Application
-            { applicationFunction = f,
-              applicationParameter = x
-            }
-  -- Non-dependent function type: A → B
-  functionOp :: P.Operator Parse Expression
-  functionOp = P.InfixR (nonDepFun <$ P.single AtomFunArrow)
-    where
-      nonDepFun :: Expression -> Expression -> Expression
-      nonDepFun a b =
-        ExpressionFunction
-          Function
-            { funParameter = param,
-              funReturn = b
-            }
-        where
-          param =
-            FunctionParameter
-              { paramName = Nothing,
-                paramUsage = Nothing,
-                paramType = a
+    -- Application by juxtaposition.
+    appOp :: P.Operator Parse Expression
+    appOp = P.InfixL (return app)
+      where
+        app :: Expression -> Expression -> Expression
+        app f x =
+          ExpressionApplication
+            Application
+              { applicationFunction = f,
+                applicationParameter = x
               }
+    -- Non-dependent function type: A → B
+    functionOp :: P.Operator Parse Expression
+    functionOp = P.InfixR (nonDepFun <$ P.single AtomFunArrow)
+      where
+        nonDepFun :: Expression -> Expression -> Expression
+        nonDepFun a b =
+          ExpressionFunction
+            Function
+              { funParameter = param,
+                funReturn = b
+              }
+          where
+            param =
+              FunctionParameter
+                { paramName = Nothing,
+                  paramUsage = Nothing,
+                  paramType = a
+                }
 
 parseExpressionAtoms ::
   Members '[Error ScopeError, State Scope] r =>
@@ -1112,15 +1169,18 @@ parseExpressionAtoms ::
   Sem r Expression
 parseExpressionAtoms a@(ExpressionAtoms sections) = do
   case res of
-    Left {} -> throw (ErrInfixParser
-                       InfixError {_infixErrAtoms = a})
+    Left {} ->
+      throw
+        ( ErrInfixParser
+            InfixError {_infixErrAtoms = a}
+        )
     Right r -> return r
   where
-  parser :: Parse Expression
-  parser = runM (mkExpressionParser tbl) <* P.eof
-  res = P.parse parser filePath (toList sections)
-  tbl = makeExpressionTable2 a
-  filePath = ""
+    parser :: Parse Expression
+    parser = runM (mkExpressionParser tbl) <* P.eof
+    res = P.parse parser filePath (toList sections)
+    tbl = makeExpressionTable2 a
+    filePath = ""
 
 -- | Monad for parsing expression sections.
 type Parse = P.Parsec () [ExpressionAtom 'Scoped]
@@ -1147,7 +1207,7 @@ parseTerm =
   where
     parseLiteral :: Parse Expression
     parseLiteral = ExpressionLiteral <$> P.token lit mempty
-       where
+      where
         lit :: ExpressionAtom 'Scoped -> Maybe Literal
         lit s = case s of
           AtomLiteral l -> Just l
@@ -1196,10 +1256,10 @@ parseTerm =
     parseNoInfixIdentifier :: Parse Expression
     parseNoInfixIdentifier = ExpressionIdentifier <$> P.token identifierNoFixity mempty
       where
-        identifierNoFixity :: ExpressionAtom 'Scoped -> Maybe S.Name
+        identifierNoFixity :: ExpressionAtom 'Scoped -> Maybe ScopedIden
         identifierNoFixity s = case s of
-          AtomIdentifier n
-            | not (S.hasFixity n) -> Just n
+          AtomIdentifier iden
+            | not (S.hasFixity (identifierName iden)) -> Just iden
           _ -> Nothing
 
     parseParens :: Parse Expression
@@ -1220,32 +1280,33 @@ makePatternTable ::
   PatternAtom 'Scoped -> [[P.Operator ParsePat Pattern]]
 makePatternTable atom = [appOp] : operators
   where
-    operators = mkSymbolTable names
-    names :: [S.Name]
-    names = case atom of
-      PatternAtomParens (PatternAtoms atoms) -> mapMaybe getName (toList atoms)
+    getConstructorRef :: PatternAtom 'Scoped -> Maybe ConstructorRef
+    getConstructorRef s = case s of
+      PatternAtomIden iden -> case iden of
+        PatternScopedConstructor r -> Just r
+        PatternScopedVar {} -> Nothing
+      _ -> Nothing
+    operators = mkSymbolTable constructorRefs
+    constructorRefs :: [ConstructorRef]
+    constructorRefs = case atom of
+      PatternAtomParens (PatternAtoms atoms) -> mapMaybe getConstructorRef (toList atoms)
       _ -> []
-      where
-        getName :: PatternAtom 'Scoped -> Maybe S.Name
-        getName a = case a of
-          PatternAtomName nm -> Just nm
-          _ -> Nothing
-    mkSymbolTable :: [S.Name] -> [[P.Operator ParsePat Pattern]]
+    mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat Pattern]]
     mkSymbolTable = reverse . map (map snd) . groupSortOn fst . mapMaybe unqualifiedSymbolOp
       where
-        unqualifiedSymbolOp :: S.Name -> Maybe (Precedence, P.Operator ParsePat Pattern)
-        unqualifiedSymbolOp S.Name' {..}
+        unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat Pattern)
+        unqualifiedSymbolOp (ConstructorRef' (S.Name' {..}) _)
           | Just Fixity {..} <- _nameFixity,
             _nameKind == S.KNameConstructor = Just $
             case fixityArity of
               Unary u -> (fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
                 where
-                  unaryApp :: S.Name -> Pattern -> Pattern
+                  unaryApp :: ConstructorRef -> Pattern -> Pattern
                   unaryApp funName = case u of
                     AssocPostfix -> PatternPostfixApplication . (`PatternPostfixApp` funName)
               Binary b -> (fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId))
                 where
-                  binaryInfixApp :: S.Name -> Pattern -> Pattern -> Pattern
+                  binaryInfixApp :: ConstructorRef -> Pattern -> Pattern -> Pattern
                   binaryInfixApp name argLeft = PatternInfixApplication . PatternInfixApp argLeft name
                   infixLRN :: ParsePat (Pattern -> Pattern -> Pattern) -> P.Operator ParsePat Pattern
                   infixLRN = case b of
@@ -1253,14 +1314,14 @@ makePatternTable atom = [appOp] : operators
                     AssocRight -> P.InfixR
                     AssocNone -> P.InfixN
           | otherwise = Nothing
-        parseSymbolId :: S.NameId -> ParsePat S.Name
-        parseSymbolId uid = P.token getName mempty
+        parseSymbolId :: S.NameId -> ParsePat ConstructorRef
+        parseSymbolId uid = P.token getConstructorRefWithId mempty
           where
-            getName :: PatternAtom 'Scoped -> Maybe S.Name
-            getName s = case s of
-              PatternAtomName n'
-                | uid == S._nameId n' -> Just n'
-              _ -> Nothing
+            getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe ConstructorRef
+            getConstructorRefWithId s = do
+              ref <- getConstructorRef s
+              guard (ref ^. constructorRefName . S.nameId == uid)
+              return ref
 
     -- Application by juxtaposition.
     appOp :: P.Operator ParsePat Pattern
@@ -1287,10 +1348,12 @@ parsePatternTerm = do
       PatternConstructor
         <$> P.token constructorNoFixity mempty
       where
-        constructorNoFixity :: PatternAtom 'Scoped -> Maybe S.Name
+        constructorNoFixity :: PatternAtom 'Scoped -> Maybe ConstructorRef
         constructorNoFixity s = case s of
-          PatternAtomName n
-            | not (S.hasFixity n), S.isConstructor n -> Just n
+          PatternAtomIden (PatternScopedConstructor ref)
+            | not (S.hasFixity n) -> Just ref
+            where
+              n = ref ^. constructorRefName
           _ -> Nothing
 
     parseWildcard :: ParsePat Pattern
@@ -1314,14 +1377,7 @@ parsePatternTerm = do
       where
         var :: PatternAtom 'Scoped -> Maybe S.Symbol
         var s = case s of
-          PatternAtomName S.Name' {..}
-            | NameUnqualified sym <- _nameConcrete,
-              S.KNameLocal <- _nameKind ->
-              Just
-                S.Name'
-                  { S._nameConcrete = sym,
-                    ..
-                  }
+          PatternAtomIden (PatternScopedVar sym) -> Just sym
           _ -> Nothing
 
     parseParens :: ParsePat Pattern -> ParsePat Pattern
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/Files.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/Files.hs
index 933e8409f..64795486f 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/Files.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/Files.hs
@@ -1,7 +1,7 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Scoper.Files where
 
-import MiniJuvix.Prelude
 import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Prelude
 
 data Files m a where
   ReadFile' :: FilePath -> Files m Text
@@ -20,8 +20,11 @@ runFilesIO = interpret $ \case
 runFilesPure :: HashMap FilePath Text -> Sem (Files ': r) a -> Sem r a
 runFilesPure fs = interpret $ \case
   (ReadFile' f) -> case HashMap.lookup f fs of
-      Nothing -> error $ pack $ "file " <> f <> " does not exist." <>
-        "\nThe contents of the mocked file system are:\n" <>
-        unlines (HashMap.keys fs)
-      Just c -> return c
+    Nothing ->
+      error $
+        pack $
+          "file " <> f <> " does not exist."
+            <> "\nThe contents of the mocked file system are:\n"
+            <> unlines (HashMap.keys fs)
+    Just c -> return c
   (EqualPaths' _ _) -> return Nothing
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Utils.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Utils.hs
index 6481fb82d..65e6b61e0 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Utils.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Utils.hs
@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Utils where
 
+import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Prelude
-import qualified Data.HashMap.Strict as HashMap
 
 data ScopedModule = forall t. MkScopedModule (SModuleIsTop t) (Module 'Scoped t)
 
@@ -12,14 +12,14 @@ mkScopedModule = MkScopedModule sing
 
 getAllModules :: Module 'Scoped 'ModuleTop -> HashMap S.NameId (Module 'Scoped 'ModuleTop)
 getAllModules m =
-   HashMap.fromList $ singl m : [ singl n | Import n <- allImports (mkScopedModule m) ]
+  HashMap.fromList $ singl m : [singl n | Import n <- allImports (mkScopedModule m)]
   where
-  allImports :: ScopedModule -> [Import 'Scoped]
-  allImports (MkScopedModule _ w) =
-    concat [ i : allImports (mkScopedModule t) | StatementImport i@(Import t) <- _moduleBody w ]
-    <> concatMap (allImports . mkScopedModule ) [ l | StatementModule l <- _moduleBody w]
-  singl :: Module 'Scoped 'ModuleTop -> (S.NameId, Module 'Scoped 'ModuleTop)
-  singl n = (S._nameId (_modulePath n), n)
+    allImports :: ScopedModule -> [Import 'Scoped]
+    allImports (MkScopedModule _ w) =
+      concat [i : allImports (mkScopedModule t) | StatementImport i@(Import t) <- _moduleBody w]
+        <> concatMap (allImports . mkScopedModule) [l | StatementModule l <- _moduleBody w]
+    singl :: Module 'Scoped 'ModuleTop -> (S.NameId, Module 'Scoped 'ModuleTop)
+    singl n = (S._nameId (_modulePath n), n)
 
 getModuleFilePath :: Module 'Scoped 'ModuleTop -> FilePath
 getModuleFilePath = _intFile . getLoc . _modulePath
diff --git a/src/MiniJuvix/Syntax/Core.hs b/src/MiniJuvix/Syntax/Core.hs
index 4cb4e5d5e..fd54f84cc 100644
--- a/src/MiniJuvix/Syntax/Core.hs
+++ b/src/MiniJuvix/Syntax/Core.hs
@@ -6,9 +6,9 @@ module MiniJuvix.Syntax.Core where
 
 --------------------------------------------------------------------------------
 
+import Algebra.Graph.Label (Semiring (..))
 import MiniJuvix.Prelude hiding (Local)
 import Numeric.Natural (Natural)
-import Algebra.Graph.Label (Semiring(..))
 
 --------------------------------------------------------------------------------
 -- Quantity (a.k.a. Usage)
diff --git a/src/MiniJuvix/Syntax/Eval.hs b/src/MiniJuvix/Syntax/Eval.hs
index 0916ae922..b2c78d8dc 100644
--- a/src/MiniJuvix/Syntax/Eval.hs
+++ b/src/MiniJuvix/Syntax/Eval.hs
@@ -2,8 +2,8 @@
 
 module MiniJuvix.Syntax.Eval where
 
-import MiniJuvix.Syntax.Core
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Core
 
 --------------------------------------------------------------------------------
 -- Values and neutral terms
diff --git a/src/MiniJuvix/Syntax/Fixity.hs b/src/MiniJuvix/Syntax/Fixity.hs
index 7fe9925e3..1f741cfeb 100644
--- a/src/MiniJuvix/Syntax/Fixity.hs
+++ b/src/MiniJuvix/Syntax/Fixity.hs
@@ -3,8 +3,8 @@ module MiniJuvix.Syntax.Fixity where
 import Language.Haskell.TH.Syntax (Lift)
 import MiniJuvix.Prelude
 
-data Precedence =
-  PrecMinusOmega
+data Precedence
+  = PrecMinusOmega
   | PrecNat Natural
   | PrecOmega
   deriving stock (Show, Eq, Lift)
@@ -40,8 +40,8 @@ data Fixity = Fixity
   }
   deriving stock (Show, Eq, Ord, Lift)
 
-data Atomicity =
-  Atom
+data Atomicity
+  = Atom
   | Aggregate Fixity
 
 class HasAtomicity a where
@@ -52,18 +52,18 @@ class HasFixity a where
 
 isLeftAssoc :: Fixity -> Bool
 isLeftAssoc opInf = case fixityArity opInf of
-    Binary AssocLeft -> True
-    _ -> False
+  Binary AssocLeft -> True
+  _ -> False
 
 isRightAssoc :: Fixity -> Bool
 isRightAssoc opInf = case fixityArity opInf of
-    Binary AssocRight -> True
-    _ -> False
+  Binary AssocRight -> True
+  _ -> False
 
 isPostfixAssoc :: Fixity -> Bool
 isPostfixAssoc opInf = case fixityArity opInf of
-    Unary AssocPostfix -> True
-    _ -> False
+  Unary AssocPostfix -> True
+  _ -> False
 
 appFixity :: Fixity
 appFixity = Fixity PrecOmega (Binary AssocLeft)
@@ -75,10 +75,10 @@ atomParens :: (Fixity -> Bool) -> Atomicity -> Fixity -> Bool
 atomParens associates argAtom opInf = case argAtom of
   Atom -> False
   Aggregate argInf
-   | argInf > opInf -> False
-   | argInf < opInf -> True
-   | associates opInf -> False
-   | otherwise -> True
+    | argInf > opInf -> False
+    | argInf < opInf -> True
+    | associates opInf -> False
+    | otherwise -> True
 
 isAtomic :: HasAtomicity a => a -> Bool
 isAtomic x = case atomicity x of
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
index bb863c7eb..5d3fba9fe 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
@@ -1,25 +1,30 @@
-module MiniJuvix.Syntax.MicroJuvix.Language (
-  module MiniJuvix.Syntax.MicroJuvix.Language,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name
-   ) where
+module MiniJuvix.Syntax.MicroJuvix.Language
+  ( module MiniJuvix.Syntax.MicroJuvix.Language,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name,
+  )
+where
 
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..))
+import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Concrete.Language (ForeignBlock(..))
-import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId(..))
 import MiniJuvix.Syntax.Fixity
 
 type FunctionName = Name
+
 type VarName = Name
+
 type ConstrName = Name
+
 type InductiveName = Name
 
-data Name = Name {
-    _nameText :: Text,
+data Name = Name
+  { _nameText :: Text,
     _nameId :: NameId,
     _nameKind :: NameKind
-    }
+  }
+
 makeLenses ''Name
 
 instance Eq Name where
@@ -39,25 +44,25 @@ data Module = Module
     _moduleBody :: ModuleBody
   }
 
-data ModuleBody = ModuleBody {
-  _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
-  _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
-  _moduleForeign :: [Indexed ForeignBlock]
+data ModuleBody = ModuleBody
+  { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
+    _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
+    _moduleForeigns :: [Indexed ForeignBlock]
   }
 
-data FunctionDef = FunctionDef {
-   _funDefName :: FunctionName,
-   _funDefTypeSig :: Type,
-   _funDefClauses :: NonEmpty FunctionClause
+data FunctionDef = FunctionDef
+  { _funDefName :: FunctionName,
+    _funDefTypeSig :: Type,
+    _funDefClauses :: NonEmpty FunctionClause
   }
 
-data FunctionClause = FunctionClause {
-    _clausePatterns :: [Pattern],
+data FunctionClause = FunctionClause
+  { _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
 
-data Iden =
-  IdenDefined Name
+data Iden
+  = IdenFunction Name
   | IdenConstructor Name
   | IdenVar VarName
 
@@ -65,20 +70,20 @@ data Expression
   = ExpressionIden Iden
   | ExpressionApplication Application
 
-data Application = Application {
-  _appLeft :: Expression,
-  _appRight :: Expression
+data Application = Application
+  { _appLeft :: Expression,
+    _appRight :: Expression
   }
 
-data Function = Function {
-  _funLeft :: Type,
-  _funRight :: Type
+data Function = Function
+  { _funLeft :: Type,
+    _funRight :: Type
   }
 
 -- | Fully applied constructor in a pattern.
-data ConstructorApp = ConstructorApp {
-  _constrAppConstructor :: Name,
-  _constrAppParameters :: [Pattern]
+data ConstructorApp = ConstructorApp
+  { _constrAppConstructor :: Name,
+    _constrAppParameters :: [Pattern]
   }
 
 data Pattern
@@ -96,12 +101,12 @@ data InductiveConstructorDef = InductiveConstructorDef
     _constructorParameters :: [Type]
   }
 
-newtype TypeIden =
-  TypeIdenInductive InductiveName
+newtype TypeIden
+  = TypeIdenInductive InductiveName
 
-data Type =
-  TypeIden TypeIden
- | TypeFunction Function
+data Type
+  = TypeIden TypeIden
+  | TypeFunction Function
 
 makeLenses ''Module
 makeLenses ''Function
@@ -114,18 +119,20 @@ makeLenses ''InductiveConstructorDef
 makeLenses ''ConstructorApp
 
 instance Semigroup ModuleBody where
-  a <> b = ModuleBody {
-    _moduleInductives = a ^. moduleInductives <> b ^. moduleInductives,
-    _moduleFunctions = a ^. moduleFunctions <> b ^. moduleFunctions,
-    _moduleForeign = a ^. moduleForeign <> b ^. moduleForeign
-    }
+  a <> b =
+    ModuleBody
+      { _moduleInductives = a ^. moduleInductives <> b ^. moduleInductives,
+        _moduleFunctions = a ^. moduleFunctions <> b ^. moduleFunctions,
+        _moduleForeigns = a ^. moduleForeigns <> b ^. moduleForeigns
+      }
 
 instance Monoid ModuleBody where
-  mempty = ModuleBody {
-    _moduleInductives = mempty,
-    _moduleForeign = mempty,
-    _moduleFunctions = mempty
-    }
+  mempty =
+    ModuleBody
+      { _moduleInductives = mempty,
+        _moduleForeigns = mempty,
+        _moduleFunctions = mempty
+      }
 
 instance HasAtomicity Application where
   atomicity = const (Aggregate appFixity)
@@ -145,8 +152,8 @@ instance HasAtomicity Type where
 
 instance HasAtomicity ConstructorApp where
   atomicity (ConstructorApp _ args)
-   | null args = Atom
-   | otherwise = Aggregate appFixity
+    | null args = Atom
+    | otherwise = Aggregate appFixity
 
 instance HasAtomicity Pattern where
   atomicity p = case p of
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ann.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ann.hs
index debab056d..5371bb6a6 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ann.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ann.hs
@@ -2,8 +2,8 @@ module MiniJuvix.Syntax.MicroJuvix.Pretty.Ann where
 
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 
-data Ann =
-  AnnKind NameKind
+data Ann
+  = AnnKind NameKind
   | AnnKeyword
   | AnnLiteralString
   | AnnLiteralInteger
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ansi.hs
index dd6a86e6f..7981e004c 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ansi.hs
@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi where
 
-import MiniJuvix.Syntax.MicroJuvix.Language
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -20,8 +20,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
index b77a3b2ca..57c96eb5b 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@@ -1,39 +1,39 @@
 -- TODO handle capital letters and characters not supported by Haskell.
 module MiniJuvix.Syntax.MicroJuvix.Pretty.Base where
 
-
-import MiniJuvix.Prelude
-import Prettyprinter
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
-import MiniJuvix.Syntax.MicroJuvix.Language
-import MiniJuvix.Syntax.Concrete.Language (ForeignBlock(..))
 import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language (Backend (..), ForeignBlock (..))
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
+import Prettyprinter
 
 newtype Options = Options
-  {
-    _optIndent :: Int
+  { _optIndent :: Int
   }
 
 defaultOptions :: Options
-defaultOptions = Options {
-  _optIndent = 2
-  }
+defaultOptions =
+  Options
+    { _optIndent = 2
+    }
 
 class PrettyCode c where
   ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
 
 instance PrettyCode Name where
   ppCode n =
-    return $ annotate (AnnKind (n ^. nameKind))
-           $ pretty (n ^. nameText) <> "_" <> pretty (n ^. nameId)
+    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
-   IdenDefined na -> ppCode na
-   IdenConstructor na -> ppCode na
-   IdenVar na -> ppCode na
+    IdenFunction na -> ppCode na
+    IdenConstructor na -> ppCode na
+    IdenVar na -> ppCode na
 
 instance PrettyCode Application where
   ppCode a = do
@@ -52,6 +52,12 @@ keyword = annotate AnnKeyword . pretty
 kwArrow :: Doc Ann
 kwArrow = keyword Str.toAscii
 
+kwForeign :: Doc Ann
+kwForeign = keyword Str.foreign_
+
+kwGhc :: Doc Ann
+kwGhc = keyword Str.ghc
+
 kwData :: Doc Ann
 kwData = keyword Str.data_
 
@@ -119,60 +125,83 @@ instance PrettyCode FunctionDef where
     funDefName' <- ppCode (f ^. funDefName)
     funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
     clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
-    return $ funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
-      <> vsep (toList clauses')
-     where
-     ppClause fun c = do
-       clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
-       clauseBody' <- ppCode (c ^. clauseBody)
-       return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+    return $
+      funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
+        <> vsep (toList clauses')
+    where
+      ppClause fun c = do
+        clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+        clauseBody' <- ppCode (c ^. clauseBody)
+        return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+
+instance PrettyCode Backend where
+  ppCode = \case
+    BackendGhc -> return kwGhc
 
 instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
-    return $ kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty _foreignCode <> line <> rbrace
-
+    return $
+      kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode
+        <> line
+        <> rbrace
 
 -- TODO Jonathan review
 instance PrettyCode ModuleBody where
   ppCode m = do
     types' <- mapM (mapM ppCode) (toList (m ^. moduleInductives))
     funs' <- mapM (mapM ppCode) (toList (m ^. moduleFunctions))
-    let foreigns' = m ^. moduleForeign
-    let everything = map (^. indexedThing) (sortOn (^. indexedIx) (types' ++ funs'))
+    foreigns' <- mapM (mapM ppCode) (toList (m ^. moduleForeigns))
+    let everything = map (^. indexedThing) (sortOn (^. indexedIx) (types' ++ funs' ++ foreigns'))
     return $ vsep2 everything
     where
-    vsep2 = concatWith (\a b -> a <> line <> line <> b)
+      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
+    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 ::
+  (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 ::
+  (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 ::
+  (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 ::
+  (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
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do
diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Language.hs b/src/MiniJuvix/Syntax/MiniHaskell/Language.hs
index c01ff1ddf..87b6dbc24 100644
--- a/src/MiniJuvix/Syntax/MiniHaskell/Language.hs
+++ b/src/MiniJuvix/Syntax/MiniHaskell/Language.hs
@@ -1,23 +1,28 @@
-module MiniJuvix.Syntax.MiniHaskell.Language (
-  module MiniJuvix.Syntax.MiniHaskell.Language,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name
-   ) where
+module MiniJuvix.Syntax.MiniHaskell.Language
+  ( module MiniJuvix.Syntax.MiniHaskell.Language,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name,
+  )
+where
 
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId(..))
 import MiniJuvix.Syntax.Fixity
 
 type FunctionName = Name
+
 type VarName = Name
+
 type ConstrName = Name
+
 type InductiveName = Name
 
-data Name = Name {
-    _nameText :: Text,
+data Name = Name
+  { _nameText :: Text,
     _nameKind :: NameKind
-    }
+  }
+
 makeLenses ''Name
 
 instance HasNameKind Name where
@@ -28,23 +33,23 @@ data Module = Module
     _moduleBody :: ModuleBody
   }
 
-newtype ModuleBody = ModuleBody {
-  _moduleStatements :: [Statement]
+newtype ModuleBody = ModuleBody
+  { _moduleStatements :: [Statement]
   }
   deriving newtype (Monoid, Semigroup)
 
-data Statement =
-  StatementInductiveDef InductiveDef
+data Statement
+  = StatementInductiveDef InductiveDef
   | StatementFunctionDef FunctionDef
 
-data FunctionDef = FunctionDef {
-   _funDefName :: FunctionName,
-   _funDefTypeSig :: Type,
-   _funDefClauses :: NonEmpty FunctionClause
+data FunctionDef = FunctionDef
+  { _funDefName :: FunctionName,
+    _funDefTypeSig :: Type,
+    _funDefClauses :: NonEmpty FunctionClause
   }
 
-data FunctionClause = FunctionClause {
-    _clausePatterns :: [Pattern],
+data FunctionClause = FunctionClause
+  { _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
 
@@ -53,22 +58,23 @@ type Iden = Name
 data Expression
   = ExpressionIden Iden
   | ExpressionApplication Application
-  -- TODO Add a constructor for literals
 
-data Application = Application {
-  _appLeft :: Expression,
-  _appRight :: Expression
+-- TODO Add a constructor for literals
+
+data Application = Application
+  { _appLeft :: Expression,
+    _appRight :: Expression
   }
 
-data Function = Function {
-  _funLeft :: Type,
-  _funRight :: Type
+data Function = Function
+  { _funLeft :: Type,
+    _funRight :: Type
   }
 
 -- | Fully applied constructor in a pattern.
-data ConstructorApp = ConstructorApp {
-  _constrAppConstructor :: Name,
-  _constrAppParameters :: [Pattern]
+data ConstructorApp = ConstructorApp
+  { _constrAppConstructor :: Name,
+    _constrAppParameters :: [Pattern]
   }
 
 data Pattern
@@ -88,9 +94,9 @@ data InductiveConstructorDef = InductiveConstructorDef
 
 type TypeIden = InductiveName
 
-data Type =
-  TypeIden TypeIden
- | TypeFunction Function
+data Type
+  = TypeIden TypeIden
+  | TypeFunction Function
 
 makeLenses ''Module
 makeLenses ''Function
@@ -120,8 +126,8 @@ instance HasAtomicity Type where
 
 instance HasAtomicity ConstructorApp where
   atomicity (ConstructorApp _ args)
-   | null args = Atom
-   | otherwise = Aggregate appFixity
+    | null args = Atom
+    | otherwise = Aggregate appFixity
 
 instance HasAtomicity Pattern where
   atomicity p = case p of
diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ann.hs b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ann.hs
index ef8266edd..2932a42df 100644
--- a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ann.hs
+++ b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ann.hs
@@ -2,8 +2,8 @@ module MiniJuvix.Syntax.MiniHaskell.Pretty.Ann where
 
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 
-data Ann =
-  AnnKind NameKind
+data Ann
+  = AnnKind NameKind
   | AnnKeyword
   | AnnLiteralString
   | AnnLiteralInteger
diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ansi.hs
index cead3f8e9..f1de2cd6c 100644
--- a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ansi.hs
@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi where
 
-import MiniJuvix.Syntax.MiniHaskell.Language
-import MiniJuvix.Syntax.MiniHaskell.Pretty.Base
-import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MiniHaskell.Language
+import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
+import MiniJuvix.Syntax.MiniHaskell.Pretty.Base
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -20,8 +20,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of
diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
index 900d8c896..3b6cec309 100644
--- a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
@@ -1,31 +1,31 @@
 -- TODO handle capital letters and characters not supported by Haskell.
 module MiniJuvix.Syntax.MiniHaskell.Pretty.Base where
 
-
-import MiniJuvix.Prelude
-import Prettyprinter
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
-import MiniJuvix.Syntax.MiniHaskell.Language
 import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.MiniHaskell.Language
+import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
+import Prettyprinter
 
 newtype Options = Options
-  {
-    _optIndent :: Int
+  { _optIndent :: Int
   }
 
 defaultOptions :: Options
-defaultOptions = Options {
-  _optIndent = 2
-  }
+defaultOptions =
+  Options
+    { _optIndent = 2
+    }
 
 class PrettyCode c where
   ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
 
 instance PrettyCode Name where
   ppCode n =
-    return $ annotate (AnnKind (n ^. nameKind))
-           $ pretty (n ^. nameText)
+    return $
+      annotate (AnnKind (n ^. nameKind)) $
+        pretty (n ^. nameText)
 
 instance PrettyCode Application where
   ppCode a = do
@@ -111,13 +111,14 @@ instance PrettyCode FunctionDef where
     funDefName' <- ppCode (f ^. funDefName)
     funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
     clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
-    return $ funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
-      <> vsep (toList clauses')
-     where
-     ppClause fun c = do
-       clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
-       clauseBody' <- ppCode (c ^. clauseBody)
-       return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+    return $
+      funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
+        <> vsep (toList clauses')
+    where
+      ppClause fun c = do
+        clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+        clauseBody' <- ppCode (c ^. clauseBody)
+        return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
 
 instance PrettyCode Statement where
   ppCode = \case
@@ -129,36 +130,52 @@ instance PrettyCode ModuleBody where
     statements' <- mapM ppCode (m ^. moduleStatements)
     return $ vsep2 statements'
     where
-    vsep2 = concatWith (\a b -> a <> line <> line <> b)
+      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
+    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 ::
+  (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 ::
+  (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 ::
+  (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 ::
+  (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
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do
diff --git a/src/MiniJuvix/Termination.hs b/src/MiniJuvix/Termination.hs
index f6e0be662..9c18aa4ac 100644
--- a/src/MiniJuvix/Termination.hs
+++ b/src/MiniJuvix/Termination.hs
@@ -1,9 +1,10 @@
-module MiniJuvix.Termination (
-  module MiniJuvix.Termination.Types,
-  module MiniJuvix.Termination.CallMap,
-  module MiniJuvix.Termination.CallGraph
-  ) where
+module MiniJuvix.Termination
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallMap,
+    module MiniJuvix.Termination.CallGraph,
+  )
+where
 
-import MiniJuvix.Termination.Types
-import MiniJuvix.Termination.CallMap
 import MiniJuvix.Termination.CallGraph
+import MiniJuvix.Termination.CallMap
+import MiniJuvix.Termination.Types
diff --git a/src/MiniJuvix/Termination/CallGraph.hs b/src/MiniJuvix/Termination/CallGraph.hs
index edd1f32fe..3c9eb5dfe 100644
--- a/src/MiniJuvix/Termination/CallGraph.hs
+++ b/src/MiniJuvix/Termination/CallGraph.hs
@@ -1,35 +1,35 @@
-module MiniJuvix.Termination.CallGraph (
-  module MiniJuvix.Termination.Types,
-  module MiniJuvix.Termination.CallGraph
-                                       ) where
+module MiniJuvix.Termination.CallGraph
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallGraph,
+  )
+where
 
+import qualified Data.HashMap.Strict as HashMap
+import qualified Data.HashSet as HashSet
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Language.Extra
-import qualified Data.HashMap.Strict as HashMap
-import MiniJuvix.Termination.Types
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import Prettyprinter as PP
 import MiniJuvix.Syntax.Abstract.Pretty.Base
-import qualified Data.HashSet as HashSet
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Termination.Types
+import Prettyprinter as PP
 
 type Edges = HashMap (FunctionName, FunctionName) Edge
 
-data Edge = Edge {
-  _edgeFrom :: FunctionName,
-  _edgeTo :: FunctionName,
-  _edgeMatrices :: HashSet CallMatrix
+data Edge = Edge
+  { _edgeFrom :: FunctionName,
+    _edgeTo :: FunctionName,
+    _edgeMatrices :: HashSet CallMatrix
   }
 
 newtype CompleteCallGraph = CompleteCallGraph Edges
 
-data ReflexiveEdge = ReflexiveEdge {
-  _redgeFun :: FunctionName,
-  _redgeMatrices :: HashSet CallMatrix
+data ReflexiveEdge = ReflexiveEdge
+  { _redgeFun :: FunctionName,
+    _redgeMatrices :: HashSet CallMatrix
   }
 
 data RecursiveBehaviour = RecursiveBehaviour
-  {
-    _recBehaviourFunction :: FunctionName,
+  { _recBehaviourFunction :: FunctionName,
     _recBehaviourMatrix :: [[Rel]]
   }
 
@@ -40,168 +40,179 @@ makeLenses ''ReflexiveEdge
 multiply :: CallMatrix -> CallMatrix -> CallMatrix
 multiply a b = map sumProdRow a
   where
-  rowB :: Int -> CallRow
-  rowB i = CallRow $ case b !? i of
-    Just (CallRow (Just c)) -> Just c
-    _ -> Nothing
-  sumProdRow :: CallRow -> CallRow
-  sumProdRow (CallRow mr) = CallRow $ do
-    (ki, ra) <- mr
-    (j, rb) <- _callRow (rowB ki)
-    return (j, mul' ra rb)
+    rowB :: Int -> CallRow
+    rowB i = CallRow $ case b !? i of
+      Just (CallRow (Just c)) -> Just c
+      _ -> Nothing
+    sumProdRow :: CallRow -> CallRow
+    sumProdRow (CallRow mr) = CallRow $ do
+      (ki, ra) <- mr
+      (j, rb) <- _callRow (rowB ki)
+      return (j, mul' ra rb)
 
 multiplyMany :: HashSet CallMatrix -> HashSet CallMatrix -> HashSet CallMatrix
-multiplyMany r s = HashSet.fromList [ multiply a b | a <- toList r, b <- toList s]
+multiplyMany r s = HashSet.fromList [multiply a b | a <- toList r, b <- toList s]
 
 composeEdge :: Edge -> Edge -> Maybe Edge
 composeEdge a b = do
   guard (a ^. edgeTo == b ^. edgeFrom)
-  return Edge {
-    _edgeFrom = a ^. edgeFrom,
-    _edgeTo = b ^. edgeTo,
-    _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
-    }
+  return
+    Edge
+      { _edgeFrom = a ^. edgeFrom,
+        _edgeTo = b ^. edgeTo,
+        _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
+      }
 
 fromFunCall :: FunctionName -> FunCall -> Call
 fromFunCall caller fc =
-  Call {_callFrom = caller,
-          _callTo = fc ^. callName,
-          _callMatrix = map fst (fc ^. callArgs)
-       }
+  Call
+    { _callFrom = caller,
+      _callTo = fc ^. callName,
+      _callMatrix = map fst (fc ^. callArgs)
+    }
 
 -- | IMPORTANT: the resulting call graph is not complete. Use this function
 -- only to filter the pretty printed graph
 unsafeFilterGraph :: Foldable f => f Text -> CompleteCallGraph -> CompleteCallGraph
 unsafeFilterGraph funNames (CompleteCallGraph g) =
-  CompleteCallGraph (HashMap.filterWithKey  (\(f , _) _ -> S.symbolText f `elem`funNames) g)
+  CompleteCallGraph (HashMap.filterWithKey (\(f, _) _ -> S.symbolText f `elem` funNames) g)
 
 completeCallGraph :: CallMap -> CompleteCallGraph
 completeCallGraph cm = CompleteCallGraph (go startingEdges)
   where
-  startingEdges :: Edges
-  startingEdges = foldr insertCall mempty allCalls
-    where
-    insertCall :: Call -> Edges -> Edges
-    insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
+    startingEdges :: Edges
+    startingEdges = foldr insertCall mempty allCalls
       where
-      aux :: Maybe Edge -> Edge
-      aux me = case me of
-        Nothing -> Edge _callFrom _callTo (HashSet.singleton _callMatrix)
-        Just e -> over edgeMatrices (HashSet.insert _callMatrix) e
-  allCalls :: [Call]
-  allCalls = [ fromFunCall caller funCall
-               | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
-               (_, funCalls) <- HashMap.toList callerMap,
-               funCall <- funCalls ]
+        insertCall :: Call -> Edges -> Edges
+        insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
+          where
+            aux :: Maybe Edge -> Edge
+            aux me = case me of
+              Nothing -> Edge _callFrom _callTo (HashSet.singleton _callMatrix)
+              Just e -> over edgeMatrices (HashSet.insert _callMatrix) e
+    allCalls :: [Call]
+    allCalls =
+      [ fromFunCall caller funCall
+        | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
+          (_, funCalls) <- HashMap.toList callerMap,
+          funCall <- funCalls
+      ]
 
-  go :: Edges -> Edges
-  go m
-    | edgesCount m == edgesCount m' = m
-    | otherwise = go m'
-    where
-    m' = step m
+    go :: Edges -> Edges
+    go m
+      | edgesCount m == edgesCount m' = m
+      | otherwise = go m'
+      where
+        m' = step m
 
-  step :: Edges -> Edges
-  step s = edgesUnion (edgesCompose s startingEdges) s
+    step :: Edges -> Edges
+    step s = edgesUnion (edgesCompose s startingEdges) s
 
-  fromEdgeList :: [Edge] -> Edges
-  fromEdgeList l = HashMap.fromList [ ((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
+    fromEdgeList :: [Edge] -> Edges
+    fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
 
-  edgesCompose :: Edges -> Edges -> Edges
-  edgesCompose a b = fromEdgeList $ catMaybes
-     [ composeEdge ea eb | ea <- toList a, eb <- toList b ]
+    edgesCompose :: Edges -> Edges -> Edges
+    edgesCompose a b =
+      fromEdgeList $
+        catMaybes
+          [composeEdge ea eb | ea <- toList a, eb <- toList b]
 
-  edgeUnion :: Edge -> Edge -> Edge
-  edgeUnion a b
-   | a ^. edgeFrom == b ^. edgeFrom,
-     a ^. edgeTo == b ^. edgeTo =
-       Edge (a ^. edgeFrom) (a ^. edgeTo)
-       (HashSet.union (a ^. edgeMatrices) (b ^. edgeMatrices))
-   | otherwise = impossible
+    edgeUnion :: Edge -> Edge -> Edge
+    edgeUnion a b
+      | a ^. edgeFrom == b ^. edgeFrom,
+        a ^. edgeTo == b ^. edgeTo =
+        Edge
+          (a ^. edgeFrom)
+          (a ^. edgeTo)
+          (HashSet.union (a ^. edgeMatrices) (b ^. edgeMatrices))
+      | otherwise = impossible
 
-  edgesUnion :: Edges -> Edges -> Edges
-  edgesUnion = HashMap.unionWith edgeUnion
+    edgesUnion :: Edges -> Edges -> Edges
+    edgesUnion = HashMap.unionWith edgeUnion
 
-  edgesCount :: Edges -> Int
-  edgesCount es = sum [ HashSet.size (e ^. edgeMatrices) | e <- toList es ]
+    edgesCount :: Edges -> Int
+    edgesCount es = sum [HashSet.size (e ^. edgeMatrices) | e <- toList es]
 
 reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
 reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
   where
-  reflexive :: Edge -> Maybe ReflexiveEdge
-  reflexive e
-   | e ^. edgeFrom == e ^. edgeTo
-    = Just $ ReflexiveEdge (e ^.edgeFrom) (e ^. edgeMatrices)
-   | otherwise = Nothing
+    reflexive :: Edge -> Maybe ReflexiveEdge
+    reflexive e
+      | e ^. edgeFrom == e ^. edgeTo =
+        Just $ ReflexiveEdge (e ^. edgeFrom) (e ^. edgeMatrices)
+      | otherwise = Nothing
 
 callMatrixDiag :: CallMatrix -> [Rel]
-callMatrixDiag m = [ col i r | (i, r) <- zip [0 :: Int ..] m]
+callMatrixDiag m = [col i r | (i, r) <- zip [0 :: Int ..] m]
   where
-  col :: Int -> CallRow -> Rel
-  col i (CallRow row) = case row of
-    Nothing -> RNothing
-    Just (j, r')
-      | i == j -> RJust r'
-      | otherwise -> RNothing
+    col :: Int -> CallRow -> Rel
+    col i (CallRow row) = case row of
+      Nothing -> RNothing
+      Just (j, r')
+        | i == j -> RJust r'
+        | otherwise -> RNothing
 
 recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
 recursiveBehaviour re =
-  RecursiveBehaviour  (re ^. redgeFun )
-  (map callMatrixDiag (toList $ re ^. redgeMatrices))
+  RecursiveBehaviour
+    (re ^. redgeFun)
+    (map callMatrixDiag (toList $ re ^. redgeMatrices))
 
 findOrder :: RecursiveBehaviour -> Maybe LexOrder
 findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
   where
-  b0 :: [[Rel]]
-  b0 = rb ^. recBehaviourMatrix
-  indexed = map (zip [0 :: Int ..] . take minLength) b0
-    where
-    minLength =  minimum (map length b0)
-
-  startB = removeUselessColumns indexed
-
-    -- | removes columns that don't have at least one ≺ in them
-  removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
-  removeUselessColumns = transpose . filter (any (isLess . snd) ) . transpose
-
-  isLexOrder :: [Int] -> Maybe [Int]
-  isLexOrder = go startB
-    where
-    go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
-    go [] _   = Just []
-    go b perm = case perm of
-      [] -> error "The permutation should have one element at least!"
-      (p0 : ptail)
-        | Just r <- find (isLess . snd . (!! p0)) b ,
-          all (notNothing . snd . (!! p0)) b ,
-          Just perm' <- go (b' p0) (map pred ptail)
-          -> Just ( fst (r !! p0) : perm')
-        | otherwise -> Nothing
+    b0 :: [[Rel]]
+    b0 = rb ^. recBehaviourMatrix
+    indexed = map (zip [0 :: Int ..] . take minLength) b0
       where
-      b' i = map r' (filter (not . isLess . snd . (!!i)) b)
-        where
-        r' r = case splitAt i r of
-          (x, y) -> x ++ drop 1 y
+        minLength = minimum (map length b0)
 
-  notNothing = (RNothing /=)
-  isLess = (RJust RLe ==)
+    startB = removeUselessColumns indexed
 
-  allPerms :: [[Int]]
-  allPerms = case nonEmpty startB of
-    Nothing -> []
-    Just s -> permutations [0 .. length (head s) - 1]
+    -- removes columns that don't have at least one ≺ in them
+    removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
+    removeUselessColumns = transpose . filter (any (isLess . snd)) . transpose
+
+    isLexOrder :: [Int] -> Maybe [Int]
+    isLexOrder = go startB
+      where
+        go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
+        go [] _ = Just []
+        go b perm = case perm of
+          [] -> error "The permutation should have one element at least!"
+          (p0 : ptail)
+            | Just r <- find (isLess . snd . (!! p0)) b,
+              all (notNothing . snd . (!! p0)) b,
+              Just perm' <- go (b' p0) (map pred ptail) ->
+              Just (fst (r !! p0) : perm')
+            | otherwise -> Nothing
+          where
+            b' i = map r' (filter (not . isLess . snd . (!! i)) b)
+              where
+                r' r = case splitAt i r of
+                  (x, y) -> x ++ drop 1 y
+
+    notNothing = (RNothing /=)
+    isLess = (RJust RLe ==)
+
+    allPerms :: [[Int]]
+    allPerms = case nonEmpty startB of
+      Nothing -> []
+      Just s -> permutations [0 .. length (head s) - 1]
 
 instance PrettyCode Edge where
   ppCode Edge {..} = do
     fromFun <- ppSCode _edgeFrom
     toFun <- ppSCode _edgeTo
     matrices <- indent 2 . ppMatrices . zip [0 :: Int ..] <$> mapM ppCode (toList _edgeMatrices)
-    return $ pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
-      <> matrices
+    return $
+      pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
+        <> matrices
     where
-    ppMatrices = vsep2 . map ppMatrix
-    ppMatrix (i, t) = pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
-      <> t
+      ppMatrices = vsep2 . map ppMatrix
+      ppMatrix (i, t) =
+        pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
+          <> t
 
 instance PrettyCode CompleteCallGraph where
   ppCode :: forall r. Members '[Reader Options] r => CompleteCallGraph -> Sem r (Doc Ann)
@@ -214,7 +225,8 @@ instance PrettyCode RecursiveBehaviour where
   ppCode (RecursiveBehaviour f m0) = do
     f' <- ppSCode f
     let m' = vsep (map (PP.list . map pretty) m)
-    return $ pretty ("Recursive behaviour of " :: Text)  <> f' <> colon <> line
-      <> indent 2 (align m')
+    return $
+      pretty ("Recursive behaviour of " :: Text) <> f' <> colon <> line
+        <> indent 2 (align m')
     where
-    m = toList (HashSet.fromList m0)
+      m = toList (HashSet.fromList m0)
diff --git a/src/MiniJuvix/Termination/CallGraphOld.hs b/src/MiniJuvix/Termination/CallGraphOld.hs
index 07ba12ee5..cb15ba8df 100644
--- a/src/MiniJuvix/Termination/CallGraphOld.hs
+++ b/src/MiniJuvix/Termination/CallGraphOld.hs
@@ -1,33 +1,33 @@
-module MiniJuvix.Termination.CallGraphOld (
-  module MiniJuvix.Termination.Types,
-  module MiniJuvix.Termination.CallGraphOld
-                                       ) where
+module MiniJuvix.Termination.CallGraphOld
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallGraphOld,
+  )
+where
 
+import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Language.Extra
-import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Syntax.Abstract.Pretty.Base
 import MiniJuvix.Termination.Types
 import Prettyprinter as PP
-import MiniJuvix.Syntax.Abstract.Pretty.Base
 
 type Edges = HashMap (FunctionName, FunctionName) Edge
 
-data Edge = Edge {
-  _edgeFrom :: FunctionName,
-  _edgeTo :: FunctionName,
-  _edgeMatrices :: [CallMatrix]
+data Edge = Edge
+  { _edgeFrom :: FunctionName,
+    _edgeTo :: FunctionName,
+    _edgeMatrices :: [CallMatrix]
   }
 
 newtype CompleteCallGraph = CompleteCallGraph Edges
 
-data ReflexiveEdge = ReflexiveEdge {
-  _redgeFun :: FunctionName,
-  _redgeMatrices :: [CallMatrix]
+data ReflexiveEdge = ReflexiveEdge
+  { _redgeFun :: FunctionName,
+    _redgeMatrices :: [CallMatrix]
   }
 
 data RecursiveBehaviour = RecursiveBehaviour
-  {
-    _recBehaviourFunction :: FunctionName,
+  { _recBehaviourFunction :: FunctionName,
     _recBehaviourMatrix :: [[Rel]]
   }
 
@@ -38,152 +38,161 @@ makeLenses ''ReflexiveEdge
 multiply :: CallMatrix -> CallMatrix -> CallMatrix
 multiply a b = map sumProdRow a
   where
-  rowB :: Int -> CallRow
-  rowB i = CallRow $ case b !? i of
-    Just (CallRow (Just c)) -> Just c
-    _ -> Nothing
-  sumProdRow :: CallRow -> CallRow
-  sumProdRow (CallRow mr) = CallRow $ do
-    (ki, ra) <- mr
-    (j, rb) <- _callRow (rowB ki)
-    return (j, mul' ra rb)
+    rowB :: Int -> CallRow
+    rowB i = CallRow $ case b !? i of
+      Just (CallRow (Just c)) -> Just c
+      _ -> Nothing
+    sumProdRow :: CallRow -> CallRow
+    sumProdRow (CallRow mr) = CallRow $ do
+      (ki, ra) <- mr
+      (j, rb) <- _callRow (rowB ki)
+      return (j, mul' ra rb)
 
 multiplyMany :: [CallMatrix] -> [CallMatrix] -> [CallMatrix]
-multiplyMany r s = [ multiply a b | a <- r, b <- s]
+multiplyMany r s = [multiply a b | a <- r, b <- s]
 
 composeEdge :: Edge -> Edge -> Maybe Edge
 composeEdge a b = do
   guard (a ^. edgeTo == b ^. edgeFrom)
-  return Edge {
-    _edgeFrom = a ^. edgeFrom,
-    _edgeTo = b ^. edgeTo,
-    _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
-    }
+  return
+    Edge
+      { _edgeFrom = a ^. edgeFrom,
+        _edgeTo = b ^. edgeTo,
+        _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
+      }
 
 fromFunCall :: FunctionName -> FunCall -> Call
 fromFunCall caller fc =
-  Call {_callFrom = caller,
-          _callTo = fc ^. callName,
-          _callMatrix = map fst (fc ^. callArgs)
-       }
+  Call
+    { _callFrom = caller,
+      _callTo = fc ^. callName,
+      _callMatrix = map fst (fc ^. callArgs)
+    }
 
 completeCallGraph :: CallMap -> CompleteCallGraph
 completeCallGraph cm = CompleteCallGraph (go startingEdges)
   where
-  startingEdges :: Edges
-  startingEdges = foldr insertCall mempty allCalls
-    where
-    insertCall :: Call -> Edges -> Edges
-    insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
+    startingEdges :: Edges
+    startingEdges = foldr insertCall mempty allCalls
       where
-      aux :: Maybe Edge -> Edge
-      aux me = case me of
-        Nothing -> Edge _callFrom _callTo [_callMatrix]
-        Just e -> over edgeMatrices (_callMatrix : ) e
-  allCalls :: [Call]
-  allCalls = [ fromFunCall caller funCall
-               | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
-               (_, funCalls) <- HashMap.toList callerMap,
-               funCall <- funCalls ]
+        insertCall :: Call -> Edges -> Edges
+        insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
+          where
+            aux :: Maybe Edge -> Edge
+            aux me = case me of
+              Nothing -> Edge _callFrom _callTo [_callMatrix]
+              Just e -> over edgeMatrices (_callMatrix :) e
+    allCalls :: [Call]
+    allCalls =
+      [ fromFunCall caller funCall
+        | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
+          (_, funCalls) <- HashMap.toList callerMap,
+          funCall <- funCalls
+      ]
 
-  go :: Edges -> Edges
-  go m
-    | edgesCount m == edgesCount m' = m
-    | otherwise = go m'
-    where
-    m' = step m
+    go :: Edges -> Edges
+    go m
+      | edgesCount m == edgesCount m' = m
+      | otherwise = go m'
+      where
+        m' = step m
 
-  step :: Edges -> Edges
-  step s = edgesUnion (edgesCompose s startingEdges) s
+    step :: Edges -> Edges
+    step s = edgesUnion (edgesCompose s startingEdges) s
 
-  fromEdgeList :: [Edge] -> Edges
-  fromEdgeList l = HashMap.fromList [ ((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
+    fromEdgeList :: [Edge] -> Edges
+    fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
 
-  edgesCompose :: Edges -> Edges -> Edges
-  edgesCompose a b = fromEdgeList $ catMaybes
-     [ composeEdge ea eb | ea <- toList a, eb <- toList b ]
-  edgesUnion :: Edges -> Edges -> Edges
-  edgesUnion = HashMap.union
-  edgesCount :: Edges -> Int
-  edgesCount = HashMap.size
+    edgesCompose :: Edges -> Edges -> Edges
+    edgesCompose a b =
+      fromEdgeList $
+        catMaybes
+          [composeEdge ea eb | ea <- toList a, eb <- toList b]
+    edgesUnion :: Edges -> Edges -> Edges
+    edgesUnion = HashMap.union
+    edgesCount :: Edges -> Int
+    edgesCount = HashMap.size
 
 reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
 reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
   where
-  reflexive :: Edge -> Maybe ReflexiveEdge
-  reflexive e
-   | e ^. edgeFrom == e ^. edgeTo
-    = Just $ ReflexiveEdge (e ^.edgeFrom) (e ^. edgeMatrices)
-   | otherwise = Nothing
+    reflexive :: Edge -> Maybe ReflexiveEdge
+    reflexive e
+      | e ^. edgeFrom == e ^. edgeTo =
+        Just $ ReflexiveEdge (e ^. edgeFrom) (e ^. edgeMatrices)
+      | otherwise = Nothing
 
 callMatrixDiag :: CallMatrix -> [Rel]
-callMatrixDiag m = [ col i r | (i, r) <- zip [0 :: Int ..] m]
+callMatrixDiag m = [col i r | (i, r) <- zip [0 :: Int ..] m]
   where
-  col :: Int -> CallRow -> Rel
-  col i (CallRow row) = case row of
-    Nothing -> RNothing
-    Just (j, r')
-      | i == j -> RJust r'
-      | otherwise -> RNothing
+    col :: Int -> CallRow -> Rel
+    col i (CallRow row) = case row of
+      Nothing -> RNothing
+      Just (j, r')
+        | i == j -> RJust r'
+        | otherwise -> RNothing
 
 recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
 recursiveBehaviour re =
-  RecursiveBehaviour  (re ^. redgeFun )
-  (map callMatrixDiag (re ^. redgeMatrices))
+  RecursiveBehaviour
+    (re ^. redgeFun)
+    (map callMatrixDiag (re ^. redgeMatrices))
 
 findOrder :: RecursiveBehaviour -> Maybe LexOrder
 findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
   where
-  b0 :: [[Rel]]
-  b0 = rb ^. recBehaviourMatrix
-  indexed = map (zip [0 :: Int ..] . take minLength) b0
-    where
-    minLength =  minimum (map length b0)
-
-  startB = removeUselessColumns indexed
-
-    -- | removes columns that don't have at least one ≺ in them
-  removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
-  removeUselessColumns = transpose . filter (any (isLess . snd) ) . transpose
-
-  isLexOrder :: [Int] -> Maybe [Int]
-  isLexOrder = go startB
-    where
-    go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
-    go [] _   = Just []
-    go b perm = case perm of
-      [] -> error "The permutation should have one element at least!"
-      (p0 : ptail)
-        | Just r <- find (isLess . snd . (!! p0)) b ,
-          all (notNothing . snd . (!! p0)) b ,
-          Just perm' <- go (b' p0) (map pred ptail)
-          -> Just ( fst (r !! p0) : perm')
-        | otherwise -> Nothing
+    b0 :: [[Rel]]
+    b0 = rb ^. recBehaviourMatrix
+    indexed = map (zip [0 :: Int ..] . take minLength) b0
       where
-      b' i = map r' (filter (not . isLess . snd . (!!i)) b)
-        where
-        r' r = case splitAt i r of
-          (x, y) -> x ++ drop 1 y
+        minLength = minimum (map length b0)
 
-  notNothing = (RNothing /=)
-  isLess = (RJust RLe ==)
+    startB = removeUselessColumns indexed
 
-  allPerms :: [[Int]]
-  allPerms = case nonEmpty startB of
-    Nothing -> []
-    Just s -> permutations [0 .. length (head s) - 1]
+    -- removes columns that don't have at least one ≺ in them
+    removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
+    removeUselessColumns = transpose . filter (any (isLess . snd)) . transpose
+
+    isLexOrder :: [Int] -> Maybe [Int]
+    isLexOrder = go startB
+      where
+        go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
+        go [] _ = Just []
+        go b perm = case perm of
+          [] -> error "The permutation should have one element at least!"
+          (p0 : ptail)
+            | Just r <- find (isLess . snd . (!! p0)) b,
+              all (notNothing . snd . (!! p0)) b,
+              Just perm' <- go (b' p0) (map pred ptail) ->
+              Just (fst (r !! p0) : perm')
+            | otherwise -> Nothing
+          where
+            b' i = map r' (filter (not . isLess . snd . (!! i)) b)
+              where
+                r' r = case splitAt i r of
+                  (x, y) -> x ++ drop 1 y
+
+    notNothing = (RNothing /=)
+    isLess = (RJust RLe ==)
+
+    allPerms :: [[Int]]
+    allPerms = case nonEmpty startB of
+      Nothing -> []
+      Just s -> permutations [0 .. length (head s) - 1]
 
 instance PrettyCode Edge where
   ppCode Edge {..} = do
     fromFun <- ppSCode _edgeFrom
     toFun <- ppSCode _edgeTo
     matrices <- indent 2 . ppMatrices . zip [0 :: Int ..] <$> mapM ppCode _edgeMatrices
-    return $ pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
-      <> matrices
+    return $
+      pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
+        <> matrices
     where
-    ppMatrices = vsep2 . map ppMatrix
-    ppMatrix (i, t) = pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
-      <> t
+      ppMatrices = vsep2 . map ppMatrix
+      ppMatrix (i, t) =
+        pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
+          <> t
 
 instance PrettyCode CompleteCallGraph where
   ppCode :: forall r. Members '[Reader Options] r => CompleteCallGraph -> Sem r (Doc Ann)
@@ -196,5 +205,6 @@ instance PrettyCode RecursiveBehaviour where
   ppCode (RecursiveBehaviour f m) = do
     f' <- ppSCode f
     let m' = vsep (map (PP.list . map pretty) m)
-    return $ pretty ("Recursive behaviour of " :: Text)  <> f' <> colon <> line
-      <> indent 2 (align m')
+    return $
+      pretty ("Recursive behaviour of " :: Text) <> f' <> colon <> line
+        <> indent 2 (align m')
diff --git a/src/MiniJuvix/Termination/CallMap.hs b/src/MiniJuvix/Termination/CallMap.hs
index 00ae3d1a1..d023f28b2 100644
--- a/src/MiniJuvix/Termination/CallMap.hs
+++ b/src/MiniJuvix/Termination/CallMap.hs
@@ -1,74 +1,79 @@
-module MiniJuvix.Termination.CallMap (
-  module MiniJuvix.Termination.Types,
-  module MiniJuvix.Termination.CallMap
-                                       ) where
+module MiniJuvix.Termination.CallMap
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallMap,
+  )
+where
 
+import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Language.Extra
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Termination.Types
 
-
 -- | i = SizeInfo [v] ⇔ v is smaller than argument i of the caller function.
 -- Indexes are 0 based
-data SizeInfo = SizeInfo {
-  _sizeSmaller :: HashMap VarName Int,
-  _sizeEqual :: [Pattern]
-       }
+data SizeInfo = SizeInfo
+  { _sizeSmaller :: HashMap VarName Int,
+    _sizeEqual :: [Pattern]
+  }
 
-viewCall :: forall r. Members '[Reader SizeInfo] r
-   => Expression -> Sem r (Maybe FunCall)
+viewCall ::
+  forall r.
+  Members '[Reader SizeInfo] r =>
+  Expression ->
+  Sem r (Maybe FunCall)
 viewCall e = case e of
   ExpressionApplication (Application f x) -> do
     c <- viewCall f
     x' <- callArg
-    return $ over callArgs (`snoc`x') <$> c
+    return $ over callArgs (`snoc` x') <$> c
     where
-    callArg :: Sem r (CallRow, Expression)
-    callArg =  do
-      lt <- lessThan
-      eq <- equalTo
-      return (CallRow (_callRow lt `mplus` _callRow eq), x)
-      where
-      lessThan :: Sem r CallRow
-      lessThan = case x of
-        ExpressionIden (IdenVar v) -> do
-          s <- asks (HashMap.lookup v . _sizeSmaller)
-          return $ case s of
-            Nothing -> CallRow Nothing
-            Just s' -> CallRow (Just (s', RLe) )
-        _ -> return (CallRow Nothing)
-      equalTo :: Sem r CallRow
-      equalTo = do
-        case viewExpressionAsPattern x of
-          Just x' -> do
-            s <- asks (elemIndex x' . _sizeEqual)
-            return $ case s of
-              Nothing -> CallRow Nothing
-              Just s' -> CallRow (Just (s', REq) )
-          _ -> return (CallRow Nothing)
-  ExpressionIden (IdenDefined x) ->
-     return (Just (singletonCall x))
+      callArg :: Sem r (CallRow, Expression)
+      callArg = do
+        lt <- lessThan
+        eq <- equalTo
+        return (CallRow (_callRow lt `mplus` _callRow eq), x)
+        where
+          lessThan :: Sem r CallRow
+          lessThan = case x of
+            ExpressionIden (IdenVar v) -> do
+              s <- asks (HashMap.lookup v . _sizeSmaller)
+              return $ case s of
+                Nothing -> CallRow Nothing
+                Just s' -> CallRow (Just (s', RLe))
+            _ -> return (CallRow Nothing)
+          equalTo :: Sem r CallRow
+          equalTo = do
+            case viewExpressionAsPattern x of
+              Just x' -> do
+                s <- asks (elemIndex x' . _sizeEqual)
+                return $ case s of
+                  Nothing -> CallRow Nothing
+                  Just s' -> CallRow (Just (s', REq))
+              _ -> return (CallRow Nothing)
+  ExpressionIden (IdenFunction x) ->
+    return (Just (singletonCall x))
   _ -> return Nothing
   where
-  singletonCall :: Name -> FunCall
-  singletonCall n = FunCall (S.nameUnqualify n) []
+    singletonCall :: Name -> FunCall
+    singletonCall n = FunCall (S.nameUnqualify n) []
 
 addCall :: FunctionName -> FunCall -> CallMap -> CallMap
 addCall fun c = over callMap (HashMap.alter (Just . insertCall c) fun)
   where
-  insertCall :: FunCall -> Maybe (HashMap FunctionName [FunCall]) -> HashMap FunctionName [FunCall]
-  insertCall f m = case m of
-    Nothing -> singl f
-    Just m' -> addFunCall f m'
-  singl :: FunCall -> HashMap FunctionName [FunCall]
-  singl f = HashMap.singleton (f ^. callName) [f]
-  addFunCall :: FunCall -> HashMap FunctionName [FunCall] -> HashMap FunctionName [FunCall]
-  addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callName) [fc]
+    insertCall :: FunCall -> Maybe (HashMap FunctionName [FunCall]) -> HashMap FunctionName [FunCall]
+    insertCall f m = case m of
+      Nothing -> singl f
+      Just m' -> addFunCall f m'
+    singl :: FunCall -> HashMap FunctionName [FunCall]
+    singl f = HashMap.singleton (f ^. callName) [f]
+    addFunCall :: FunCall -> HashMap FunctionName [FunCall] -> HashMap FunctionName [FunCall]
+    addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callName) [fc]
 
-registerCall :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-   => FunCall -> Sem r ()
+registerCall ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  FunCall ->
+  Sem r ()
 registerCall c = do
   fun <- ask
   modify (addCall fun c)
@@ -96,30 +101,36 @@ checkTypeSignature :: Members '[State CallMap, Reader FunctionName] r => Express
 checkTypeSignature = runReader (emptySizeInfo :: SizeInfo) . checkExpression
 
 emptySizeInfo :: SizeInfo
-emptySizeInfo = SizeInfo {
-  _sizeEqual = mempty,
-  _sizeSmaller = mempty
-  }
+emptySizeInfo =
+  SizeInfo
+    { _sizeEqual = mempty,
+      _sizeSmaller = mempty
+    }
 
 mkSizeInfo :: [Pattern] -> SizeInfo
 mkSizeInfo ps = SizeInfo {..}
   where
-  _sizeEqual = ps
-  _sizeSmaller = HashMap.fromList
-    [ (v, i) | (i, p) <- zip [0..] ps,
-      v <- smallerPatternVariables p]
+    _sizeEqual = ps
+    _sizeSmaller =
+      HashMap.fromList
+        [ (v, i) | (i, p) <- zip [0 ..] ps, v <- smallerPatternVariables p
+        ]
 
-checkFunctionClause :: Members '[State CallMap, Reader FunctionName] r =>
-  FunctionClause -> Sem r ()
-checkFunctionClause cl = runReader (mkSizeInfo (cl ^. clausePatterns))
-  $ checkExpression (cl ^. clauseBody)
+checkFunctionClause ::
+  Members '[State CallMap, Reader FunctionName] r =>
+  FunctionClause ->
+  Sem r ()
+checkFunctionClause cl =
+  runReader (mkSizeInfo (cl ^. clausePatterns)) $
+    checkExpression (cl ^. clauseBody)
 
 checkExpression :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r => Expression -> Sem r ()
 checkExpression e = do
   mc <- viewCall e
   case mc of
-    Just c -> do registerCall c
-                 mapM_ (checkExpression . snd) (c ^. callArgs)
+    Just c -> do
+      registerCall c
+      mapM_ (checkExpression . snd) (c ^. callArgs)
     Nothing -> case e of
       ExpressionApplication a -> checkApplication a
       ExpressionIden {} -> return ()
@@ -127,18 +138,24 @@ checkExpression e = do
       ExpressionFunction f -> checkFunction f
       ExpressionLiteral {} -> return ()
 
-checkApplication :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-  => Application -> Sem r ()
+checkApplication ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Application ->
+  Sem r ()
 checkApplication (Application l r) = do
   checkExpression l
   checkExpression r
 
-checkFunction :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-  => Function -> Sem r ()
+checkFunction ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Function ->
+  Sem r ()
 checkFunction (Function l r) = do
   checkFunctionParameter l
   checkExpression r
 
-checkFunctionParameter :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-   => FunctionParameter -> Sem r ()
+checkFunctionParameter ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  FunctionParameter ->
+  Sem r ()
 checkFunctionParameter p = checkExpression (p ^. paramType)
diff --git a/src/MiniJuvix/Termination/Types.hs b/src/MiniJuvix/Termination/Types.hs
index 3d9af024a..294e52698 100644
--- a/src/MiniJuvix/Termination/Types.hs
+++ b/src/MiniJuvix/Termination/Types.hs
@@ -1,28 +1,29 @@
-module MiniJuvix.Termination.Types (
-  module MiniJuvix.Termination.Types.SizeRelation,
-  module MiniJuvix.Termination.Types
-                                             ) where
+module MiniJuvix.Termination.Types
+  ( module MiniJuvix.Termination.Types.SizeRelation,
+    module MiniJuvix.Termination.Types,
+  )
+where
 
+import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language as A
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified Data.HashMap.Strict as HashMap
-import Prettyprinter as PP
-import MiniJuvix.Termination.Types.SizeRelation
 import MiniJuvix.Syntax.Abstract.Pretty.Base
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Termination.Types.SizeRelation
+import Prettyprinter as PP
 
-newtype CallMap = CallMap {
-  _callMap :: HashMap A.FunctionName (HashMap A.FunctionName [FunCall]) }
+newtype CallMap = CallMap
+  { _callMap :: HashMap A.FunctionName (HashMap A.FunctionName [FunCall])
+  }
   deriving newtype (Semigroup, Monoid)
 
-
-data FunCall = FunCall {
-  _callName :: A.FunctionName,
-  _callArgs :: [(CallRow, A.Expression)]
+data FunCall = FunCall
+  { _callName :: A.FunctionName,
+    _callArgs :: [(CallRow, A.Expression)]
   }
 
-newtype CallRow = CallRow {
-  _callRow :: Maybe (Int, Rel')
+newtype CallRow = CallRow
+  { _callRow :: Maybe (Int, Rel')
   }
   deriving stock (Eq, Show, Generic)
 
@@ -30,11 +31,12 @@ instance Hashable CallRow
 
 type CallMatrix = [CallRow]
 
-data Call = Call {
-  _callFrom :: A.FunctionName,
-  _callTo :: A.FunctionName,
-  _callMatrix :: CallMatrix
+data Call = Call
+  { _callFrom :: A.FunctionName,
+    _callTo :: A.FunctionName,
+    _callMatrix :: CallMatrix
   }
+
 newtype LexOrder = LexOrder (NonEmpty Int)
 
 makeLenses ''FunCall
@@ -47,36 +49,36 @@ instance PrettyCode FunCall where
     f' <- ppSCode f
     return $ f' <+> hsep args'
     where
-    ppArg :: (CallRow, A.Expression) -> Sem r (Doc Ann)
-    ppArg (CallRow mi, a) =
-      case mi of
-        Just (i, r) -> relAux (Just i) (RJust r)
-        Nothing -> relAux Nothing RNothing
-      where
-      relAux mayIx r = do
-        showDecr <- asks _optShowDecreasingArgs
-        let pi = annotate AnnImportant . pretty <$> mayIx
-            pr = annotate AnnKeyword (pretty r)
-        case showDecr of
-          OnlyArg -> ppCodeAtom a
-          OnlyRel -> return $ dbrackets (pr <+?> pi)
-          ArgRel -> do
-            a' <- ppCode a
-            return $ dbrackets (a' <+> pr <+?> pi)
-    dbrackets :: Doc a -> Doc a
-    dbrackets x = pretty '⟦' <> x <> pretty '⟧'
+      ppArg :: (CallRow, A.Expression) -> Sem r (Doc Ann)
+      ppArg (CallRow mi, a) =
+        case mi of
+          Just (i, r) -> relAux (Just i) (RJust r)
+          Nothing -> relAux Nothing RNothing
+        where
+          relAux mayIx r = do
+            showDecr <- asks _optShowDecreasingArgs
+            let pi = annotate AnnImportant . pretty <$> mayIx
+                pr = annotate AnnKeyword (pretty r)
+            case showDecr of
+              OnlyArg -> ppCodeAtom a
+              OnlyRel -> return $ dbrackets (pr <+?> pi)
+              ArgRel -> do
+                a' <- ppCode a
+                return $ dbrackets (a' <+> pr <+?> pi)
+      dbrackets :: Doc a -> Doc a
+      dbrackets x = pretty '⟦' <> x <> pretty '⟧'
 
 instance PrettyCode CallMap where
   ppCode :: forall r. Members '[Reader Options] r => CallMap -> Sem r (Doc Ann)
   ppCode (CallMap m) = vsep <$> mapM ppEntry (HashMap.toList m)
     where
-    ppEntry :: (A.FunctionName, HashMap A.FunctionName [FunCall]) -> Sem r (Doc Ann)
-    ppEntry (fun, mcalls) = do
-      fun' <- annotate AnnImportant <$> ppSCode fun
-      calls' <- vsep <$> mapM ppCode calls
-      return $ fun' <+> waveFun <+> align calls'
-      where
-      calls = concat (HashMap.elems mcalls)
+      ppEntry :: (A.FunctionName, HashMap A.FunctionName [FunCall]) -> Sem r (Doc Ann)
+      ppEntry (fun, mcalls) = do
+        fun' <- annotate AnnImportant <$> ppSCode fun
+        calls' <- vsep <$> mapM ppCode calls
+        return $ fun' <+> waveFun <+> align calls'
+        where
+          calls = concat (HashMap.elems mcalls)
 
 kwQuestion :: Doc Ann
 kwQuestion = annotate AnnKeyword "?"
diff --git a/src/MiniJuvix/Termination/Types/SizeRelation.hs b/src/MiniJuvix/Termination/Types/SizeRelation.hs
index 696bed791..55b8edea5 100644
--- a/src/MiniJuvix/Termination/Types/SizeRelation.hs
+++ b/src/MiniJuvix/Termination/Types/SizeRelation.hs
@@ -1,20 +1,21 @@
 module MiniJuvix.Termination.Types.SizeRelation where
 
-import MiniJuvix.Prelude
 import Algebra.Graph.Label
+import MiniJuvix.Prelude
 import Prettyprinter
 
-data Rel =
-  RJust Rel'
+data Rel
+  = RJust Rel'
   | RNothing
   deriving stock (Eq, Show, Generic)
 
-data Rel' =
-  REq
+data Rel'
+  = REq
   | RLe
   deriving stock (Eq, Show, Generic)
 
 instance Hashable Rel'
+
 instance Hashable Rel
 
 toRel :: Rel' -> Rel
diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
index 5879ac35f..e49d4dfc4 100644
--- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
+++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
@@ -1,17 +1,18 @@
 module MiniJuvix.Translation.AbstractToMicroJuvix where
 
+import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language.Extra as A
-import qualified MiniJuvix.Syntax.Usage as A
-import MiniJuvix.Syntax.MicroJuvix.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Syntax.MicroJuvix.Language
+import qualified MiniJuvix.Syntax.Usage as A
 
 translateModule :: A.TopModule -> Module
-translateModule m = Module {
-  _moduleName = goTopModuleName (m ^. A.moduleName),
-  _moduleBody = goModuleBody (m ^. A.moduleBody)
-  }
+translateModule m =
+  Module
+    { _moduleName = goTopModuleName (m ^. A.moduleName),
+      _moduleBody = goModuleBody (m ^. A.moduleBody)
+    }
 
 goTopModuleName :: A.TopModuleName -> Name
 goTopModuleName = goSymbol . S.topModulePathName
@@ -20,11 +21,12 @@ goName :: S.Name -> Name
 goName = goSymbol . S.nameUnqualify
 
 goSymbol :: S.Symbol -> Name
-goSymbol s = Name {
-  _nameText = S.symbolText s,
-  _nameId = S._nameId s,
-  _nameKind = getNameKind s
- }
+goSymbol s =
+  Name
+    { _nameText = S.symbolText s,
+      _nameId = S._nameId s,
+      _nameKind = getNameKind s
+    }
 
 unsupported :: Text -> a
 unsupported thing = error ("Not yet supported: " <> thing)
@@ -34,21 +36,27 @@ goImport m = goModuleBody (m ^. A.moduleBody)
 
 goModuleBody :: A.ModuleBody -> ModuleBody
 goModuleBody b
- | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules"
- | otherwise = ModuleBody {
-     _moduleInductives = HashMap.fromList
-       [ (d ^. indexedThing . inductiveName, d)
-        | d <- map (fmap goInductiveDef) (toList (b ^. A.moduleInductives))],
-     _moduleFunctions = HashMap.fromList
-        [ (f ^. indexedThing . funDefName, f) |
-          f <- map (fmap goFunctionDef) (toList (b ^. A.moduleFunctions)) ],
-     _moduleForeign = b ^. A.moduleForeign
-     }
-     -- <> mconcatMap goImport (b ^. A.moduleImports)
+  | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules"
+  | otherwise =
+    ModuleBody
+      { _moduleInductives =
+          HashMap.fromList
+            [ (d ^. indexedThing . inductiveName, d)
+              | d <- map (fmap goInductiveDef) (toList (b ^. A.moduleInductives))
+            ],
+        _moduleFunctions =
+          HashMap.fromList
+            [ (f ^. indexedThing . funDefName, f)
+              | f <- map (fmap goFunctionDef) (toList (b ^. A.moduleFunctions))
+            ],
+        _moduleForeigns = b ^. A.moduleForeigns
+      }
+
+-- <> mconcatMap goImport (b ^. A.moduleImports)
 
 goTypeIden :: A.Iden -> TypeIden
 goTypeIden i = case i of
-  A.IdenDefined {} -> unsupported "functions in types"
+  A.IdenFunction {} -> unsupported "functions in types"
   A.IdenConstructor {} -> unsupported "constructors in types"
   A.IdenVar {} -> unsupported "type variables"
   A.IdenInductive d -> TypeIdenInductive (goName d)
@@ -65,17 +73,19 @@ goFunction :: A.Function -> Function
 goFunction (A.Function l r) = Function (goFunctionParameter l) (goType r)
 
 goFunctionDef :: A.FunctionDef -> FunctionDef
-goFunctionDef f = FunctionDef {
-  _funDefName = goSymbol (f ^. A.funDefName),
-  _funDefTypeSig = goType (f ^. A.funDefTypeSig),
-  _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses)
-  }
+goFunctionDef f =
+  FunctionDef
+    { _funDefName = goSymbol (f ^. A.funDefName),
+      _funDefTypeSig = goType (f ^. A.funDefTypeSig),
+      _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses)
+    }
 
 goFunctionClause :: A.FunctionClause -> FunctionClause
-goFunctionClause c = FunctionClause {
-  _clausePatterns = map goPattern (c ^. A.clausePatterns),
-  _clauseBody = goExpression (c ^. A.clauseBody)
-  }
+goFunctionClause c =
+  FunctionClause
+    { _clausePatterns = map goPattern (c ^. A.clausePatterns),
+      _clauseBody = goExpression (c ^. A.clauseBody)
+    }
 
 goPattern :: A.Pattern -> Pattern
 goPattern p = case p of
@@ -85,8 +95,10 @@ goPattern p = case p of
   A.PatternEmpty -> unsupported "pattern empty"
 
 goConstructorApp :: A.ConstructorApp -> ConstructorApp
-goConstructorApp c = ConstructorApp (goName (c ^. A.constrAppConstructor))
-  (map goPattern (c ^. A.constrAppParameters))
+goConstructorApp c =
+  ConstructorApp
+    (goName (c ^. A.constrAppConstructor))
+    (map goPattern (c ^. A.constrAppParameters))
 
 goType :: A.Expression -> Type
 goType e = case e of
@@ -101,7 +113,7 @@ goApplication (A.Application f x) = Application (goExpression f) (goExpression x
 
 goIden :: A.Iden -> Iden
 goIden i = case i of
-  A.IdenDefined n -> IdenDefined (goName n)
+  A.IdenFunction n -> IdenFunction (goName n)
   A.IdenConstructor c -> IdenConstructor (goName c)
   A.IdenVar v -> IdenVar (goSymbol v)
   A.IdenAxiom {} -> unsupported "axiom identifier"
@@ -118,19 +130,21 @@ goExpression e = case e of
 goInductiveDef :: A.InductiveDef -> InductiveDef
 goInductiveDef i = case i ^. A.inductiveType of
   Just {} -> unsupported "inductive indices"
-  _ -> InductiveDef {
-    _inductiveName = indName,
-    _inductiveConstructors = map goConstructorDef (i ^. A.inductiveConstructors)
-  }
+  _ ->
+    InductiveDef
+      { _inductiveName = indName,
+        _inductiveConstructors = map goConstructorDef (i ^. A.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
+    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
 
 -- TODO: add docs or an example
 viewExpressionFunctionType :: A.Expression -> ([Type], Type)
@@ -143,4 +157,5 @@ viewExpressionFunctionType e = case e of
 
 viewFunctionType :: A.Function -> (NonEmpty Type, Type)
 viewFunctionType (A.Function p r) = (goFunctionParameter p :| args, ret)
-  where (args, ret) = viewExpressionFunctionType r
+  where
+    (args, ret) = viewExpressionFunctionType r
diff --git a/src/MiniJuvix/Translation/ScopedToAbstract.hs b/src/MiniJuvix/Translation/ScopedToAbstract.hs
index f30edca46..9cc890403 100644
--- a/src/MiniJuvix/Translation/ScopedToAbstract.hs
+++ b/src/MiniJuvix/Translation/ScopedToAbstract.hs
@@ -1,11 +1,11 @@
 module MiniJuvix.Translation.ScopedToAbstract where
 
-import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified MiniJuvix.Syntax.Abstract.Language as A
 import qualified Data.HashMap.Strict as HashMap
-
+import MiniJuvix.Prelude
+import qualified MiniJuvix.Syntax.Abstract.Language as A
+import MiniJuvix.Syntax.Concrete.Language
+import qualified MiniJuvix.Syntax.Concrete.Language as C
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 
 type Err = Text
 
@@ -32,85 +32,102 @@ goModuleBody ss' = do
   _moduleLocalModules <- locals
   _moduleFunctions <- functions
   _moduleImports <- imports
-  _moduleForeign <- foreigns
+  _moduleForeigns <- foreigns
   return A.ModuleBody {..}
   where
-  ss :: [Indexed (Statement 'Scoped)]
-  ss = zipWith Indexed [0 ..] ss'
-  inductives :: Sem r (HashMap A.InductiveName (Indexed A.InductiveDef))
-  inductives = sequence $ HashMap.fromList
-    [ (def ^. inductiveName, Indexed i <$> goInductive def)
-    | Indexed i (StatementInductive def) <- ss ]
-  locals :: Sem r (HashMap A.InductiveName (Indexed A.LocalModule))
-  locals = sequence $ HashMap.fromList
-    [ (m ^. modulePath, Indexed i <$> goLocalModule m)
-    | Indexed i (StatementModule m) <- ss ]
-  foreigns :: Sem r [Indexed ForeignBlock]
-  foreigns = return
-    [ Indexed i f
-    | Indexed i (StatementForeign f) <- ss ]
-  imports :: Sem r [Indexed A.TopModule]
-  imports = sequence $
-    [ Indexed i <$> goModule m
-    | Indexed i (StatementImport (Import m)) <- ss ]
-  functions :: Sem r (HashMap A.FunctionName (Indexed A.FunctionDef))
-  functions = do
-    sequence $ HashMap.fromList
-     [ (name, Indexed i <$> funDef)
-     | Indexed i sig <- sigs,
-       let name = sig ^. sigName,
-       let clauses = mapM goFunctionClause (getClauses name),
-       let funDef = liftA2 (A.FunctionDef name) (goExpression (sig ^. sigType)) clauses ]
-    where
-    getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped)
-    getClauses name = fromMaybe impossible $
-       nonEmpty [ c | StatementFunctionClause c <- ss',
-                  name == c ^.clauseOwnerFunction ]
-    sigs :: [Indexed (TypeSignature 'Scoped)]
-    sigs = [ Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss ]
-
+    ss :: [Indexed (Statement 'Scoped)]
+    ss = zipWith Indexed [0 ..] ss'
+    inductives :: Sem r (HashMap A.InductiveName (Indexed A.InductiveDef))
+    inductives =
+      sequence $
+        HashMap.fromList
+          [ (def ^. inductiveName, Indexed i <$> goInductive def)
+            | Indexed i (StatementInductive def) <- ss
+          ]
+    locals :: Sem r (HashMap A.InductiveName (Indexed A.LocalModule))
+    locals =
+      sequence $
+        HashMap.fromList
+          [ (m ^. modulePath, Indexed i <$> goLocalModule m)
+            | Indexed i (StatementModule m) <- ss
+          ]
+    foreigns :: Sem r [Indexed ForeignBlock]
+    foreigns =
+      return
+        [ Indexed i f
+          | Indexed i (StatementForeign f) <- ss
+        ]
+    imports :: Sem r [Indexed A.TopModule]
+    imports =
+      sequence $
+        [ Indexed i <$> goModule m
+          | Indexed i (StatementImport (Import m)) <- ss
+        ]
+    functions :: Sem r (HashMap A.FunctionName (Indexed A.FunctionDef))
+    functions = do
+      sequence $
+        HashMap.fromList
+          [ (name, Indexed i <$> funDef)
+            | Indexed i sig <- sigs,
+              let name = sig ^. sigName,
+              let clauses = mapM goFunctionClause (getClauses name),
+              let funDef = liftA2 (A.FunctionDef name) (goExpression (sig ^. sigType)) clauses
+          ]
+      where
+        getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped)
+        getClauses name =
+          fromMaybe impossible $
+            nonEmpty
+              [ c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction
+              ]
+        sigs :: [Indexed (TypeSignature 'Scoped)]
+        sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss]
 
 goFunctionClause :: forall r. Members '[Error Err] r => FunctionClause 'Scoped -> Sem r A.FunctionClause
 goFunctionClause FunctionClause {..} = do
   _clausePatterns' <- mapM goPattern _clausePatterns
   _clauseBody' <- goExpression _clauseBody
   goWhereBlock _clauseWhere
-  return A.FunctionClause {
-    _clausePatterns = _clausePatterns',
-    _clauseBody = _clauseBody'
-    }
+  return
+    A.FunctionClause
+      { _clausePatterns = _clausePatterns',
+        _clauseBody = _clauseBody'
+      }
 
 goWhereBlock :: forall r. Members '[Error Err] r => Maybe (WhereBlock 'Scoped) -> Sem r ()
 goWhereBlock w = case w of
- Just _ ->  unsupported "where block"
- Nothing -> return ()
+  Just _ -> unsupported "where block"
+  Nothing -> return ()
 
 goInductiveParameter :: Members '[Error Err] r => InductiveParameter 'Scoped -> Sem r A.FunctionParameter
 goInductiveParameter InductiveParameter {..} = do
   paramType' <- goExpression _inductiveParameterType
-  return A.FunctionParameter {
-    _paramType = paramType',
-    _paramName = Just _inductiveParameterName,
-    _paramUsage = UsageOmega
-    }
+  return
+    A.FunctionParameter
+      { _paramType = paramType',
+        _paramName = Just _inductiveParameterName,
+        _paramUsage = UsageOmega
+      }
 
 goInductive :: Members '[Error Err] r => InductiveDef 'Scoped -> Sem r A.InductiveDef
 goInductive InductiveDef {..} = do
   _inductiveParameters' <- mapM goInductiveParameter _inductiveParameters
   _inductiveType' <- sequence $ goExpression <$> _inductiveType
   _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
-  return A.InductiveDef {
-    _inductiveParameters = _inductiveParameters',
-    _inductiveName = _inductiveName,
-    _inductiveType = _inductiveType',
-    _inductiveConstructors = _inductiveConstructors'
-    }
+  return
+    A.InductiveDef
+      { _inductiveParameters = _inductiveParameters',
+        _inductiveName = _inductiveName,
+        _inductiveType = _inductiveType',
+        _inductiveConstructors = _inductiveConstructors'
+      }
 
 goConstructorDef :: Members '[Error Err] r => InductiveConstructorDef 'Scoped -> Sem r A.InductiveConstructorDef
 goConstructorDef (InductiveConstructorDef c ty) = A.InductiveConstructorDef c <$> goExpression ty
 
 goExpression :: forall r. Members '[Error Err] r => Expression -> Sem r A.Expression
 goExpression e = case e of
+  -- TODO: Continue here
   ExpressionIdentifier nt -> return (goIden nt)
   ExpressionParensIdentifier nt -> return (goIden nt)
   ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
@@ -123,41 +140,32 @@ goExpression e = case e of
   ExpressionUniverse uni -> return $ A.ExpressionUniverse (goUniverse uni)
   ExpressionFunction func -> A.ExpressionFunction <$> goFunction func
   where
-  goIden :: S.Name -> A.Expression
-  goIden = A.ExpressionIden . goName
-  goName :: S.Name -> A.Iden
-  goName nm = case nm ^. S.nameKind of
-     S.KNameConstructor -> A.IdenConstructor nm
-     S.KNameFunction -> A.IdenDefined nm
-     S.KNameInductive -> A.IdenInductive nm
-     S.KNameLocal -> A.IdenVar (fromUnqualified nm)
-     S.KNameAxiom -> A.IdenAxiom nm
-     S.KNameLocalModule -> impossible
-     S.KNameTopModule -> impossible
-    where
-    fromUnqualified :: S.Name -> S.Symbol
-    fromUnqualified = over S.nameConcrete (\c -> case c of
-      NameQualified {} -> impossible
-      NameUnqualified u -> u)
+    goIden :: C.ScopedIden -> A.Expression
+    goIden x = A.ExpressionIden $ case x of
+      ScopedAxiom a -> A.IdenAxiom (a ^. C.axiomRefName)
+      ScopedInductive i -> A.IdenInductive (i ^. C.inductiveRefName)
+      ScopedVar v -> A.IdenVar v
+      ScopedFunction fun -> A.IdenFunction (fun ^. C.functionRefName)
+      ScopedConstructor c -> A.IdenConstructor (c ^. C.constructorRefName)
 
-  goApplication :: Application -> Sem r A.Application
-  goApplication (Application l r) = do
-    l' <- goExpression l
-    r' <- goExpression r
-    return (A.Application l' r')
+    goApplication :: Application -> Sem r A.Application
+    goApplication (Application l r) = do
+      l' <- goExpression l
+      r' <- goExpression r
+      return (A.Application l' r')
 
-  goPostfix :: PostfixApplication -> Sem r A.Application
-  goPostfix (PostfixApplication l op) = do
-    l' <- goExpression l
-    let op' = goIden op
-    return (A.Application op' l')
+    goPostfix :: PostfixApplication -> Sem r A.Application
+    goPostfix (PostfixApplication l op) = do
+      l' <- goExpression l
+      let op' = goIden op
+      return (A.Application op' l')
 
-  goInfix :: InfixApplication -> Sem r A.Application
-  goInfix (InfixApplication l op r) = do
-    l' <- goExpression l
-    let op' = goIden op
-    r' <- goExpression r
-    return $ A.Application (A.ExpressionApplication (A.Application op' l')) r'
+    goInfix :: InfixApplication -> Sem r A.Application
+    goInfix (InfixApplication l op r) = do
+      l' <- goExpression l
+      let op' = goIden op
+      r' <- goExpression r
+      return $ A.Application (A.ExpressionApplication (A.Application op' l')) r'
 
 goUniverse :: Universe -> Universe
 goUniverse = id
@@ -183,7 +191,7 @@ goFunctionParameter (FunctionParameter _paramName u ty) = do
 goPatternApplication :: forall r. Members '[Error Err] r => PatternApp -> Sem r A.ConstructorApp
 goPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternApplication a)
 
-goPatternConstructor :: forall r. Members '[Error Err] r => S.Name -> Sem r A.ConstructorApp
+goPatternConstructor :: forall r. Members '[Error Err] r => ConstructorRef -> Sem r A.ConstructorApp
 goPatternConstructor a = uncurry A.ConstructorApp <$> viewApp (PatternConstructor a)
 
 goInfixPatternApplication :: forall r. Members '[Error Err] r => PatternInfixApp -> Sem r A.ConstructorApp
@@ -194,27 +202,23 @@ goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPos
 
 viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.Name, [A.Pattern])
 viewApp p = case p of
-  PatternConstructor c -> checkConstructorKind c $> (c, [])
+  PatternConstructor c -> return (c ^. constructorRefName, [])
   PatternApplication (PatternApp l r) -> do
     r' <- goPattern r
     second (`snoc` r') <$> viewApp l
   PatternInfixApplication (PatternInfixApp l c r) -> do
-    checkConstructorKind c
     l' <- goPattern l
     r' <- goPattern r
-    return (c, [l', r'])
-  PatternPostfixApplication  (PatternPostfixApp l c) -> do
-    checkConstructorKind c
+    return (c ^. constructorRefName, [l', r'])
+  PatternPostfixApplication (PatternPostfixApp l c) -> do
     l' <- goPattern l
-    return (c, [l'])
+    return (c ^. constructorRefName, [l'])
   PatternVariable {} -> err
   PatternWildcard {} -> err
   PatternEmpty {} -> err
   where
-  err :: Sem r a
-  err = throw ("constructor expected on the left of a pattern application" :: Err)
-  checkConstructorKind :: S.Name -> Sem r ()
-  checkConstructorKind n = unless (S.isConstructor n) err
+    err :: Sem r a
+    err = throw ("constructor expected on the left of a pattern application" :: Err)
 
 goPattern :: forall r. Members '[Error Err] r => Pattern -> Sem r A.Pattern
 goPattern p = case p of
diff --git a/src/MiniJuvix/Utils/Paths.hs b/src/MiniJuvix/Utils/Paths.hs
index a87f66f90..bc7ad1410 100644
--- a/src/MiniJuvix/Utils/Paths.hs
+++ b/src/MiniJuvix/Utils/Paths.hs
@@ -1,8 +1,8 @@
 module MiniJuvix.Utils.Paths where
 
+import Language.Haskell.TH.Syntax as TH
 import MiniJuvix.Prelude
 import TH.RelativePaths
-import Language.Haskell.TH.Syntax as TH
 
 assetsDir :: Q Exp
 assetsDir = pathRelativeToCabalPackage "assets" >>= TH.lift
diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs
index d07a59102..e61e42d7f 100644
--- a/test/Scope/Positive.hs
+++ b/test/Scope/Positive.hs
@@ -41,7 +41,7 @@ testDescr PosTest {..} = TestDescr {
     parsedPretty' <- parseTextModuleIO parsedPretty
 
     step "Scope again"
-    s' <- fromRightIO' printErrorAnsi $ M.scopeCheck1Pure fs "." p'
+    s' <- fromRightIO' printErrorAnsi $ return (M.scopeCheck1Pure fs "." p')
 
     step "Checks"
     assertBool "check: scope . parse . pretty . scope . parse = scope . parse" (s == s')