diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,27 @@
+# 0.2.0.0
+
+## Main updates
+
+- New top-level module for each lambda calculus is added.  
+  It make easier to use one specific lambda calculus under a qualified name.
+- Quasiquoter now supports splicing-in.
+- Change the type of elaborator and type checker for composability.  
+  Currently they are less type-safe. However, monad to make them type-safe will be added in the future.
+
+## Breaking changes
+
+- Move lifters and substitutions into dedicated modules.
+- Rename pretty printers.
+- Rename elaborators.
+- Rename quasiquoter.
+- Remove elaborated quasiquoter.
+- Change the type of elaborator and type checker.
+
+# 0.1.0.0
+
+The first release including support for following 4 lambda calculi.
+
+- Simply Typed Lambda Calculus
+- System F
+- System F omega underbar
+- System F omega
diff --git a/lambda-cube.cabal b/lambda-cube.cabal
--- a/lambda-cube.cabal
+++ b/lambda-cube.cabal
@@ -5,16 +5,17 @@
 -- see: https://github.com/sol/hpack
 
 name:           lambda-cube
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Haskell implementation of (some of) lambda cube calculi
 description:    Haskell implementation of the following 4 lambda calculi:
+                .
                 1. Simply typed lambda calculus
                 2. System F
                 3. System F omega underbar
                 4. System F omega
 category:       Utilities
-homepage:       https://github.com/Ailrun/LambdaCube#readme
-bug-reports:    https://github.com/Ailrun/LambdaCube/issues
+homepage:       https://github.com/Ailrun/lambda-cube#readme
+bug-reports:    https://github.com/Ailrun/lambda-cube/issues
 author:         Junyoung Clare Jang
 maintainer:     jjc9310@gmail.com
 copyright:      2021 Junyoung Clare Jang
@@ -22,46 +23,59 @@
 license-file:   LICENSE
 build-type:     Simple
 extra-source-files:
+    CHANGELOG.md
     README.md
 
 source-repository head
   type: git
-  location: https://github.com/Ailrun/LambdaCube
+  location: https://github.com/Ailrun/lambda-cube
 
 library
   exposed-modules:
       LambdaCube.Common.Parser
       LambdaCube.Common.PrettyPrinter
+      LambdaCube.STLC
       LambdaCube.STLC.Ast
       LambdaCube.STLC.Elaborator
       LambdaCube.STLC.Evaluator
+      LambdaCube.STLC.Lifter
       LambdaCube.STLC.Normalizer
       LambdaCube.STLC.Parser
       LambdaCube.STLC.PrettyPrinter
+      LambdaCube.STLC.Substitution
       LambdaCube.STLC.TH
       LambdaCube.STLC.TypeChecker
+      LambdaCube.SystemF
       LambdaCube.SystemF.Ast
       LambdaCube.SystemF.Elaborator
       LambdaCube.SystemF.Evaluator
+      LambdaCube.SystemF.Lifter
       LambdaCube.SystemF.Normalizer
       LambdaCube.SystemF.Parser
       LambdaCube.SystemF.PrettyPrinter
+      LambdaCube.SystemF.Substitution
       LambdaCube.SystemF.TH
       LambdaCube.SystemF.TypeChecker
+      LambdaCube.SystemFw
       LambdaCube.SystemFw.Ast
       LambdaCube.SystemFw.Elaborator
       LambdaCube.SystemFw.Evaluator
+      LambdaCube.SystemFw.Lifter
       LambdaCube.SystemFw.Normalizer
       LambdaCube.SystemFw.Parser
       LambdaCube.SystemFw.PrettyPrinter
+      LambdaCube.SystemFw.Substitution
       LambdaCube.SystemFw.TH
       LambdaCube.SystemFw.TypeChecker
+      LambdaCube.SystemFw_
       LambdaCube.SystemFw_.Ast
       LambdaCube.SystemFw_.Elaborator
       LambdaCube.SystemFw_.Evaluator
+      LambdaCube.SystemFw_.Lifter
       LambdaCube.SystemFw_.Normalizer
       LambdaCube.SystemFw_.Parser
       LambdaCube.SystemFw_.PrettyPrinter
+      LambdaCube.SystemFw_.Substitution
       LambdaCube.SystemFw_.TH
       LambdaCube.SystemFw_.TypeChecker
   other-modules:
@@ -116,8 +130,9 @@
   build-depends:
       base >=4.12 && <5
     , megaparsec >=9.0.1 && <9.1
+    , syb
     , template-haskell
-    , text
+    , text >=1.2.4.0
   default-language: Haskell2010
 
 test-suite lambda-cube-test
diff --git a/src/LambdaCube/Common/Parser.hs b/src/LambdaCube/Common/Parser.hs
--- a/src/LambdaCube/Common/Parser.hs
+++ b/src/LambdaCube/Common/Parser.hs
@@ -21,7 +21,7 @@
 rightArrow = lex $ string "->"
 atsignBackslash = lex $ string "@\\"
 
-backslash, atsign, sharp, colon, dot, openParenthesis, closeParenthesis, exclamationMark, comma, asterisk :: Parser Char
+backslash, atsign, sharp, colon, dot, openParenthesis, closeParenthesis, exclamationMark, comma, asterisk, dollarsign :: Parser Char
 backslash        = lex $ char '\\'
 atsign           = lex $ char '@'
 sharp            = lex $ char '#'
@@ -32,6 +32,7 @@
 exclamationMark  = lex $ char '!'
 comma            = lex $ char ','
 asterisk         = lex $ char '*'
+dollarsign       = lex $ char '$'
 
 identifier :: Parser Text
 identifier = lex $ (Text.pack .) . (:) <$> letterChar <*> many alphaNumChar
diff --git a/src/LambdaCube/STLC.hs b/src/LambdaCube/STLC.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC.hs
@@ -0,0 +1,22 @@
+module LambdaCube.STLC
+  ( module LambdaCube.STLC.Ast
+  , module LambdaCube.STLC.Elaborator
+  , module LambdaCube.STLC.Lifter
+  , module LambdaCube.STLC.Normalizer
+  , module LambdaCube.STLC.Parser
+  , module LambdaCube.STLC.PrettyPrinter
+  , module LambdaCube.STLC.Substitution
+  , module LambdaCube.STLC.TH
+  , module LambdaCube.STLC.TypeChecker
+  ) where
+
+import LambdaCube.STLC.Ast
+
+import LambdaCube.STLC.Elaborator
+import LambdaCube.STLC.Lifter
+import LambdaCube.STLC.Normalizer
+import LambdaCube.STLC.Parser
+import LambdaCube.STLC.PrettyPrinter
+import LambdaCube.STLC.Substitution
+import LambdaCube.STLC.TH
+import LambdaCube.STLC.TypeChecker
diff --git a/src/LambdaCube/STLC/Ast.hs b/src/LambdaCube/STLC/Ast.hs
--- a/src/LambdaCube/STLC/Ast.hs
+++ b/src/LambdaCube/STLC/Ast.hs
@@ -1,39 +1,48 @@
 module LambdaCube.STLC.Ast where
 
+import           Data.Data                  (Data)
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
+data ExtLCType
+  = ExtLCBase
+  | ExtLCArr ExtLCType ExtLCType
+  | ExtLCMTVar String
+  deriving stock (Eq, Show, Data, Lift)
+infixr 5 `ExtLCArr`
+
 data ExtLCTerm
   = ExtLCVar Text
-  | ExtLCLam Text LCType ExtLCTerm
+  | ExtLCLam Text ExtLCType ExtLCTerm
   | ExtLCApp ExtLCTerm ExtLCTerm
-  deriving stock (Eq, Show, Lift)
+  | ExtLCMVar String
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `ExtLCApp`
 
 data LCType
   = LCBase
   | LCArr LCType LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `LCArr`
 
 data LCTerm
   = LCVar Int
   | LCLam LCType LCTerm
   | LCApp LCTerm LCTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCApp`
 
 data LCValue
   = LCValLam LCType LCTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNormalTerm
   = LCNormLam LCType LCNormalTerm
   | LCNormNeut LCNeutralTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNeutralTerm
   = LCNeutVar Int
   | LCNeutApp LCNeutralTerm LCNormalTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCNeutApp`
diff --git a/src/LambdaCube/STLC/Elaborator.hs b/src/LambdaCube/STLC/Elaborator.hs
--- a/src/LambdaCube/STLC/Elaborator.hs
+++ b/src/LambdaCube/STLC/Elaborator.hs
@@ -4,13 +4,21 @@
 import qualified Data.Text           as Text
 import           LambdaCube.STLC.Ast
 
-elaborate :: ExtLCTerm -> Either String LCTerm
+elaborateType :: ExtLCType -> LCType
+elaborateType = go
+  where
+    go ExtLCBase = LCBase
+    go (ExtLCArr a b) = go a `LCArr` go b
+    go (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
+
+elaborate :: ExtLCTerm -> LCTerm
 elaborate = go []
   where
     go l (ExtLCVar v)
       | Just idx <- v `elemIndex` l
-      = Right $ LCVar idx
+      = LCVar idx
       | otherwise
-      = Left $ "Variable " <> Text.unpack v <> " is not in scope"
-    go l (ExtLCLam v t b) = LCLam t <$> go (v : l) b
-    go l (ExtLCApp f a) = LCApp <$> go l f <*> go l a
+      = error $ "Variable " <> Text.unpack v <> " is not in scope"
+    go l (ExtLCLam v t b) = LCLam (elaborateType t) $ go (v : l) b
+    go l (ExtLCApp f a) = go l f `LCApp` go l a
+    go _ (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
diff --git a/src/LambdaCube/STLC/Evaluator.hs b/src/LambdaCube/STLC/Evaluator.hs
--- a/src/LambdaCube/STLC/Evaluator.hs
+++ b/src/LambdaCube/STLC/Evaluator.hs
@@ -1,16 +1,7 @@
 module LambdaCube.STLC.Evaluator where
 
 import           LambdaCube.STLC.Ast
-
-liftLCValue :: LCValue -> LCTerm
-liftLCValue (LCValLam t b) = LCLam t b
-
-substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
-substituteValue n v = go n
-  where
-    go m e@(LCVar l) = if m == l then liftLCValue v else e
-    go m (LCLam t b) = LCLam t $ go (m + 1) b
-    go m (LCApp f a) = go m f `LCApp` go m a
+import           LambdaCube.STLC.Substitution
 
 evaluate :: LCTerm -> LCValue
 evaluate = go
diff --git a/src/LambdaCube/STLC/Lifter.hs b/src/LambdaCube/STLC/Lifter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/Lifter.hs
@@ -0,0 +1,14 @@
+module LambdaCube.STLC.Lifter where
+
+import           LambdaCube.STLC.Ast
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b) = LCLam t b
+
+liftLCNormal :: LCNormalTerm -> LCTerm
+liftLCNormal (LCNormLam t b) = LCLam t $ liftLCNormal b
+liftLCNormal (LCNormNeut nt) = liftLCNeutral nt
+
+liftLCNeutral :: LCNeutralTerm -> LCTerm
+liftLCNeutral (LCNeutVar n) = LCVar n
+liftLCNeutral (LCNeutApp f a) = liftLCNeutral f `LCApp` liftLCNormal a
diff --git a/src/LambdaCube/STLC/Normalizer.hs b/src/LambdaCube/STLC/Normalizer.hs
--- a/src/LambdaCube/STLC/Normalizer.hs
+++ b/src/LambdaCube/STLC/Normalizer.hs
@@ -1,23 +1,7 @@
 module LambdaCube.STLC.Normalizer where
 
 import           LambdaCube.STLC.Ast
-
-substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormal n nv = go n
-  where
-    go m (LCNormLam t b)   = LCNormLam t $ go (m + 1) b
-    go m (LCNormNeut neut) = substituteNeutral m nv neut
-
-substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNeutral n nv = go n
-  where
-    go m e@(LCNeutVar l) = if m == l then nv else LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b   -> substituteNormal 0 a' b
-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
-      where
-        a' = substituteNormal m nv a
+import           LambdaCube.STLC.Substitution
 
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
@@ -26,7 +10,7 @@
     go (LCLam t b) = LCNormLam t $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam t b   -> LCNormLam t $ substituteNormal 0 a' b
+        LCNormLam t b   -> LCNormLam t $ substituteNormalInNormal 0 a' b
         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
       where
         a' = go a
diff --git a/src/LambdaCube/STLC/Parser.hs b/src/LambdaCube/STLC/Parser.hs
--- a/src/LambdaCube/STLC/Parser.hs
+++ b/src/LambdaCube/STLC/Parser.hs
@@ -2,6 +2,7 @@
 
 import           Data.Foldable            (Foldable (foldl'))
 import           Data.Functor             (($>))
+import qualified Data.Text                as Text
 import           LambdaCube.Common.Parser
 import           LambdaCube.STLC.Ast
 import           Text.Megaparsec
@@ -10,7 +11,7 @@
 pTopLC = topParser pLC
 
 pLC :: Parser ExtLCTerm
-pLC = pLam <|> pApp
+pLC = pLam<|> pApp
 
 pLam :: Parser ExtLCTerm
 pLam =
@@ -23,10 +24,22 @@
 pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pLC
 
-pType :: Parser LCType
-pType = foldr1 LCArr <$> sepBy1 pAType rightArrow
+pVar :: Parser ExtLCTerm
+pVar = ExtLCVar <$> identifier
 
-pAType :: Parser LCType
-pAType = (sharp $> LCBase) <|> parenthesized pType
+pMVar :: Parser ExtLCTerm
+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
+
+pType :: Parser ExtLCType
+pType = foldr1 ExtLCArr <$> sepBy1 pAType rightArrow
+
+pAType :: Parser ExtLCType
+pAType = pBase <|> pMTVar <|> parenthesized pType
+
+pBase :: Parser ExtLCType
+pBase = sharp $> ExtLCBase
+
+pMTVar :: Parser ExtLCType
+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
diff --git a/src/LambdaCube/STLC/PrettyPrinter.hs b/src/LambdaCube/STLC/PrettyPrinter.hs
--- a/src/LambdaCube/STLC/PrettyPrinter.hs
+++ b/src/LambdaCube/STLC/PrettyPrinter.hs
@@ -9,22 +9,22 @@
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.STLC.Ast
 
-prettyType :: LCType -> Text
-prettyType = prettyTypePrec 0
+prettyUnnamedType :: LCType -> Text
+prettyUnnamedType = prettyUnnamedTypePrec 0
 
-prettyTerm :: LCTerm -> Text
-prettyTerm = prettyTermPrec 0
+prettyUnnamedTerm :: LCTerm -> Text
+prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
-prettyTypePrec :: Int -> LCType -> Text
-prettyTypePrec = go
+prettyUnnamedTypePrec :: Int -> LCType -> Text
+prettyUnnamedTypePrec = go
   where
     go _ LCBase      = "#"
     go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
 
-prettyTermPrec :: Int -> LCTerm -> Text
-prettyTermPrec = go
+prettyUnnamedTermPrec :: Int -> LCTerm -> Text
+prettyUnnamedTermPrec = go
   where
-    pTP = prettyTypePrec
+    pTP = prettyUnnamedTypePrec
 
     go _ (LCVar n)   = Text.pack $ show n
     go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
diff --git a/src/LambdaCube/STLC/Substitution.hs b/src/LambdaCube/STLC/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/STLC/Substitution.hs
@@ -0,0 +1,28 @@
+module LambdaCube.STLC.Substitution where
+
+import           LambdaCube.STLC.Ast
+import           LambdaCube.STLC.Lifter
+
+substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
+substituteValue n v = go n
+  where
+    go m e@(LCVar l) = if m == l then liftLCValue v else e
+    go m (LCLam t b) = LCLam t $ go (m + 1) b
+    go m (LCApp f a) = go m f `LCApp` go m a
+
+substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal n nv = go n
+  where
+    go m (LCNormLam t b)   = LCNormLam t $ go (m + 1) b
+    go m (LCNormNeut neut) = substituteNormalInNeutral m nv neut
+
+substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNormalInNeutral n nv = go n
+  where
+    go m e@(LCNeutVar l) = if m == l then nv else LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
+        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
+      where
+        a' = substituteNormalInNormal m nv a
diff --git a/src/LambdaCube/STLC/TH.hs b/src/LambdaCube/STLC/TH.hs
--- a/src/LambdaCube/STLC/TH.hs
+++ b/src/LambdaCube/STLC/TH.hs
@@ -1,43 +1,45 @@
-module LambdaCube.STLC.TH where
+module LambdaCube.STLC.TH
+  ( lc
+  ) where
 
-import           Control.Monad              ((<=<))
+import           Data.Data                  (Data)
+import           Data.Generics              (extQ)
+import           Data.Text                  (Text)
 import qualified Data.Text                  as Text
 import           LambdaCube.STLC.Ast
-import           LambdaCube.STLC.Elaborator
 import           LambdaCube.STLC.Parser
+import           Language.Haskell.TH.Lib    (ExpQ, varE)
 import           Language.Haskell.TH.Quote  (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax (Loc (loc_start), Q, lift, location)
+import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,
+                                             location, mkName)
 import qualified Text.Megaparsec            as P
 import qualified Text.Megaparsec.Error      as PE
 
-stlc :: QuasiQuoter
-stlc =
+lc :: QuasiQuoter
+lc =
   QuasiQuoter
-    { quoteExp = lift <=< stlcQuoteExp
+    { quoteExp = expLc
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-stlcQuoteExp :: String -> Q ExtLCTerm
-stlcQuoteExp str = do
+expLc :: String -> ExpQ
+expLc str = do
   l <- location
   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> pure e
+    Right e  -> dataToExpQ converter e
     Left err -> fail $ PE.errorBundlePretty err
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      const Nothing
+      `extQ` quotedMVar
+      `extQ` quotedMTVar
+      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
-elaboratedStlc :: QuasiQuoter
-elaboratedStlc =
-  QuasiQuoter
-    { quoteExp = lift <=< elaboratedStlcQuoteExp
-    , quotePat = undefined
-    , quoteType = undefined
-    , quoteDec = undefined
-    }
+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
+    quotedMVar _             = Nothing
 
-elaboratedStlcQuoteExp :: String -> Q LCTerm
-elaboratedStlcQuoteExp str = do
-  e <- stlcQuoteExp str
-  case elaborate e of
-    Right e' -> pure e'
-    Left err -> fail err
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
diff --git a/src/LambdaCube/STLC/TypeChecker.hs b/src/LambdaCube/STLC/TypeChecker.hs
--- a/src/LambdaCube/STLC/TypeChecker.hs
+++ b/src/LambdaCube/STLC/TypeChecker.hs
@@ -3,15 +3,14 @@
 import           Data.List           (uncons)
 import           LambdaCube.STLC.Ast
 
-infer :: LCTerm -> Maybe LCType
+infer :: LCTerm -> LCType
 infer = go []
   where
-    go l (LCVar n) = fmap fst . uncons $ drop n l
-    go l (LCLam t b) = LCArr t <$> go (t : l) b
+    go l (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n l
+    go l (LCLam t b) = t `LCArr` go (t : l) b
     go l (LCApp f a)
-      | Just (LCArr at' rt) <- go l f
-      , Just at <- go l a
-      , at == at'
-      = Just rt
+      | LCArr at rt <- go l f
+      , at == go l a
+      = rt
       | otherwise
-      = Nothing
+      = error "Function argument type mismatch"
diff --git a/src/LambdaCube/SystemF.hs b/src/LambdaCube/SystemF.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF.hs
@@ -0,0 +1,22 @@
+module LambdaCube.SystemF
+  ( module LambdaCube.SystemF.Ast
+  , module LambdaCube.SystemF.Elaborator
+  , module LambdaCube.SystemF.Lifter
+  , module LambdaCube.SystemF.Normalizer
+  , module LambdaCube.SystemF.Parser
+  , module LambdaCube.SystemF.PrettyPrinter
+  , module LambdaCube.SystemF.Substitution
+  , module LambdaCube.SystemF.TH
+  , module LambdaCube.SystemF.TypeChecker
+  ) where
+
+import LambdaCube.SystemF.Ast
+
+import LambdaCube.SystemF.Elaborator
+import LambdaCube.SystemF.Lifter
+import LambdaCube.SystemF.Normalizer
+import LambdaCube.SystemF.Parser
+import LambdaCube.SystemF.PrettyPrinter
+import LambdaCube.SystemF.Substitution
+import LambdaCube.SystemF.TH
+import LambdaCube.SystemF.TypeChecker
diff --git a/src/LambdaCube/SystemF/Ast.hs b/src/LambdaCube/SystemF/Ast.hs
--- a/src/LambdaCube/SystemF/Ast.hs
+++ b/src/LambdaCube/SystemF/Ast.hs
@@ -1,5 +1,6 @@
 module LambdaCube.SystemF.Ast where
 
+import           Data.Data                  (Data)
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
@@ -8,7 +9,8 @@
   | ExtLCTVar Text
   | ExtLCArr ExtLCType ExtLCType
   | ExtLCUniv Text ExtLCType
-  deriving stock (Eq, Show, Lift)
+  | ExtLCMTVar String
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `ExtLCArr`
 
 data ExtLCTerm
@@ -17,7 +19,8 @@
   | ExtLCApp ExtLCTerm ExtLCTerm
   | ExtLCTLam Text ExtLCTerm
   | ExtLCTApp ExtLCTerm ExtLCType
-  deriving stock (Eq, Show, Lift)
+  | ExtLCMVar String
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `ExtLCApp`
 infixl 6 `ExtLCTApp`
 
@@ -26,7 +29,7 @@
   | LCTVar Int
   | LCArr LCType LCType
   | LCUniv LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `LCArr`
 
 data LCTerm
@@ -35,25 +38,25 @@
   | LCApp LCTerm LCTerm
   | LCTLam LCTerm
   | LCTApp LCTerm LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCApp`
 infixl 6 `LCTApp`
 
 data LCValue
   = LCValLam LCType LCTerm
   | LCValTLam LCTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNormalTerm
   = LCNormLam LCType LCNormalTerm
   | LCNormTLam LCNormalTerm
   | LCNormNeut LCNeutralTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNeutralTerm
   = LCNeutVar Int
   | LCNeutApp LCNeutralTerm LCNormalTerm
   | LCNeutTApp LCNeutralTerm LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCNeutApp`
 infixl 6 `LCNeutTApp`
diff --git a/src/LambdaCube/SystemF/Elaborator.hs b/src/LambdaCube/SystemF/Elaborator.hs
--- a/src/LambdaCube/SystemF/Elaborator.hs
+++ b/src/LambdaCube/SystemF/Elaborator.hs
@@ -5,27 +5,29 @@
 import qualified Data.Text              as Text
 import           LambdaCube.SystemF.Ast
 
-elaborate :: ExtLCTerm -> Either String LCTerm
+elaborate :: ExtLCTerm -> LCTerm
 elaborate = go [] []
   where
     go _  vl (ExtLCVar x)
       | Just n <- x `elemIndex` vl
-      = Right $ LCVar n
+      = LCVar n
       | otherwise
-      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"
-    go tl vl (ExtLCLam x t b) = LCLam <$> typeElaborate tl t <*> go tl (x : vl) b
-    go tl vl (ExtLCApp f a) = LCApp <$> go tl vl f <*> go tl vl a
-    go tl vl (ExtLCTLam x b) = LCTLam <$> go (x : tl) vl b
-    go tl vl (ExtLCTApp f t) = LCTApp <$> go tl vl f <*> typeElaborate tl t
+      = error $ "Term variable " <> Text.unpack x <> " is not in scope"
+    go tl vl (ExtLCLam x t b) = LCLam (elaborateType tl t) $ go tl (x : vl) b
+    go tl vl (ExtLCApp f a) = go tl vl f `LCApp` go tl vl a
+    go tl vl (ExtLCTLam x b) = LCTLam $ go (x : tl) vl b
+    go tl vl (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t
+    go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
 
-typeElaborate :: [Text] -> ExtLCType -> Either String LCType
-typeElaborate = go
+elaborateType :: [Text] -> ExtLCType -> LCType
+elaborateType = go
   where
-    go _ ExtLCBase = Right LCBase
+    go _ ExtLCBase = LCBase
     go l (ExtLCTVar x)
       | Just n <- x `elemIndex` l
-      = Right $ LCTVar n
+      = LCTVar n
       | otherwise
-      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"
-    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b
-    go l (ExtLCUniv x a) = LCUniv <$> go (x : l) a
+      = error $ "Type variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCArr a b) = go l a `LCArr` go l b
+    go l (ExtLCUniv x a) = LCUniv $ go (x : l) a
+    go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
diff --git a/src/LambdaCube/SystemF/Evaluator.hs b/src/LambdaCube/SystemF/Evaluator.hs
--- a/src/LambdaCube/SystemF/Evaluator.hs
+++ b/src/LambdaCube/SystemF/Evaluator.hs
@@ -1,20 +1,7 @@
 module LambdaCube.SystemF.Evaluator where
 
 import           LambdaCube.SystemF.Ast
-import           LambdaCube.SystemF.TypeChecker (substituteType)
-
-liftLCValue :: LCValue -> LCTerm
-liftLCValue (LCValLam t b) = LCLam t b
-liftLCValue (LCValTLam b)  = LCTLam b
-
-substitute :: Int -> LCValue -> LCTerm -> LCTerm
-substitute n v = go n
-  where
-    go m e@(LCVar l)  = if m == l then liftLCValue v else e
-    go m (LCLam t b)  = LCLam t $ go (m + 1) b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam b)   = LCTLam $ go m b
-    go m (LCTApp f t) = go m f `LCTApp` t
+import           LambdaCube.SystemF.Substitution
 
 evaluate :: LCTerm -> LCValue
 evaluate = go
@@ -24,7 +11,7 @@
     go (LCApp f a)
       | LCValLam _ b <- go f
       , v <- go a
-      = go $ substitute 0 v b
+      = go $ substituteValue 0 v b
       | otherwise
       = error "Did you really type check this?"
     go (LCTLam b) = LCValTLam b
diff --git a/src/LambdaCube/SystemF/Lifter.hs b/src/LambdaCube/SystemF/Lifter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/Lifter.hs
@@ -0,0 +1,17 @@
+module LambdaCube.SystemF.Lifter where
+
+import           LambdaCube.SystemF.Ast
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b) = LCLam t b
+liftLCValue (LCValTLam b)  = LCTLam b
+
+liftLCNormal :: LCNormalTerm -> LCTerm
+liftLCNormal (LCNormLam t b) = LCLam t $ liftLCNormal b
+liftLCNormal (LCNormTLam b)  = LCTLam $ liftLCNormal b
+liftLCNormal (LCNormNeut nt) = liftLCNeutral nt
+
+liftLCNeutral :: LCNeutralTerm -> LCTerm
+liftLCNeutral (LCNeutVar n)    = LCVar n
+liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a
+liftLCNeutral (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
diff --git a/src/LambdaCube/SystemF/Normalizer.hs b/src/LambdaCube/SystemF/Normalizer.hs
--- a/src/LambdaCube/SystemF/Normalizer.hs
+++ b/src/LambdaCube/SystemF/Normalizer.hs
@@ -1,59 +1,7 @@
 module LambdaCube.SystemF.Normalizer where
 
 import           LambdaCube.SystemF.Ast
-import           LambdaCube.SystemF.TypeChecker (substituteTypeInType)
-
-substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormal n v = go n
-  where
-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
-    go m (LCNormTLam b)  = LCNormTLam $ go m b
-    go m (LCNormNeut nt) = substituteNeutral m v nt
-
-substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNeutral n v = go n
-  where
-    go m e@(LCNeutVar l)
-      | m == l = v
-      | otherwise = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b -> substituteNormal 0 a' b
-        LCNormTLam _  -> error "Did you really type check this?"
-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
-      where
-        a' = substituteNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
-        LCNormLam _ _ -> error "Did you really type check this?"
-        LCNormTLam b  -> substituteTypeNormal 0 t b
-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t
-
-substituteTypeNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
-substituteTypeNormal n v = go n
-  where
-    go m (LCNormLam t b) = LCNormLam (substituteTypeInType m v t) $ go m b
-    go m (LCNormTLam b)  = LCNormTLam $ go (m + 1) b
-    go m (LCNormNeut nt) = substituteTypeNeutral m v nt
-
-substituteTypeNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
-substituteTypeNeutral n v = go n
-  where
-    go _ e@(LCNeutVar _) = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b -> substituteNormal 0 a' b
-        LCNormTLam _  -> error "Did you really type check this?"
-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
-      where
-        a' = substituteTypeNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
-        LCNormLam _ _ -> error "Did you really type check this?"
-        LCNormTLam b  -> substituteTypeNormal 0 t' b
-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t'
-      where
-        t' = substituteTypeInType m v t
+import           LambdaCube.SystemF.Substitution
 
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
@@ -63,7 +11,7 @@
     go (LCTLam b) = LCNormTLam $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam _ b   -> substituteNormal 0 a' b
+        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
         LCNormTLam _    -> error "Did you really type check this?"
         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
       where
@@ -71,5 +19,5 @@
     go (LCTApp f t) =
       case go f of
         LCNormLam _ _   -> error "Did you really type check this?"
-        LCNormTLam b    -> substituteTypeNormal 0 t b
+        LCNormTLam b    -> substituteTypeInNormal 0 t b
         LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
diff --git a/src/LambdaCube/SystemF/Parser.hs b/src/LambdaCube/SystemF/Parser.hs
--- a/src/LambdaCube/SystemF/Parser.hs
+++ b/src/LambdaCube/SystemF/Parser.hs
@@ -7,6 +7,7 @@
 import           LambdaCube.Common.Parser
 import           LambdaCube.SystemF.Ast
 import           Text.Megaparsec
+import qualified Data.Text as Text
 
 pTopLC :: Parser ExtLCTerm
 pTopLC = topParser pLC
@@ -38,8 +39,14 @@
     else flip ExtLCApp <$> pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pLC
 
+pVar :: Parser ExtLCTerm
+pVar = ExtLCVar <$> identifier
+
+pMVar :: Parser ExtLCTerm
+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
+
 pType :: Parser ExtLCType
 pType = pUniv <|> pArr
 
@@ -53,4 +60,13 @@
 pArr = foldr1 ExtLCArr <$> sepBy1 pAType rightArrow
 
 pAType :: Parser ExtLCType
-pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType
+pAType = pBase <|> pTVar <|> pMTVar <|> parenthesized pType
+
+pBase :: Parser ExtLCType
+pBase = sharp $> ExtLCBase
+
+pTVar :: Parser ExtLCType
+pTVar = ExtLCTVar <$> identifier
+
+pMTVar :: Parser ExtLCType
+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
diff --git a/src/LambdaCube/SystemF/PrettyPrinter.hs b/src/LambdaCube/SystemF/PrettyPrinter.hs
--- a/src/LambdaCube/SystemF/PrettyPrinter.hs
+++ b/src/LambdaCube/SystemF/PrettyPrinter.hs
@@ -9,24 +9,24 @@
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.SystemF.Ast
 
-prettyType :: LCType -> Text
-prettyType = prettyTypePrec 0
+prettyUnnamedType :: LCType -> Text
+prettyUnnamedType = prettyUnnamedTypePrec 0
 
-prettyTerm :: LCTerm -> Text
-prettyTerm = prettyTermPrec 0
+prettyUnnamedTerm :: LCTerm -> Text
+prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
-prettyTypePrec :: Int -> LCType -> Text
-prettyTypePrec = go
+prettyUnnamedTypePrec :: Int -> LCType -> Text
+prettyUnnamedTypePrec = go
   where
     go _ LCBase      = "#"
     go _ (LCTVar i)  = Text.pack $ show i
     go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
     go p (LCUniv b)  = wrapIfSpaced (p > 0) ["! : * ,", go 0 b]
 
-prettyTermPrec :: Int -> LCTerm -> Text
-prettyTermPrec = go
+prettyUnnamedTermPrec :: Int -> LCTerm -> Text
+prettyUnnamedTermPrec = go
   where
-    pTP = prettyTypePrec
+    pTP = prettyUnnamedTypePrec
 
     go _ (LCVar i)    = Text.pack $ show i
     go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
diff --git a/src/LambdaCube/SystemF/Substitution.hs b/src/LambdaCube/SystemF/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemF/Substitution.hs
@@ -0,0 +1,82 @@
+module LambdaCube.SystemF.Substitution where
+
+import           LambdaCube.SystemF.Ast
+import           LambdaCube.SystemF.Lifter
+
+substituteType :: Int -> LCType -> LCTerm -> LCTerm
+substituteType n v = go n
+  where
+    go _ e@(LCVar _)  = e
+    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam b)   = LCTLam $ go (m + 1) b
+    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
+
+substituteTypeInType :: Int -> LCType -> LCType -> LCType
+substituteTypeInType n v = go n
+  where
+    go _ LCBase       = LCBase
+    go m e@(LCTVar l) = if m == l then v else e
+    go m (LCArr a b)  = go m a `LCArr` go m b
+    go m (LCUniv a)   = LCUniv $ go (m + 1) a
+
+substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
+substituteValue n v = go n
+  where
+    go m e@(LCVar l)  = if m == l then liftLCValue v else e
+    go m (LCLam t b)  = LCLam t $ go (m + 1) b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam b)   = LCTLam $ go m b
+    go m (LCTApp f t) = go m f `LCTApp` t
+
+substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal n v = go n
+  where
+    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
+    go m (LCNormTLam b)  = LCNormTLam $ go m b
+    go m (LCNormNeut nt) = substituteNormalInNeutral m v nt
+
+substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNormalInNeutral n v = go n
+  where
+    go m e@(LCNeutVar l)
+      | m == l = v
+      | otherwise = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b -> substituteNormalInNormal 0 a' b
+        LCNormTLam _  -> error "Did you really type check this?"
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteNormalInNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _ -> error "Did you really type check this?"
+        LCNormTLam b  -> substituteTypeInNormal 0 t b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t
+
+substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
+substituteTypeInNormal n v = go n
+  where
+    go m (LCNormLam t b) = LCNormLam (substituteTypeInType m v t) $ go m b
+    go m (LCNormTLam b)  = LCNormTLam $ go (m + 1) b
+    go m (LCNormNeut nt) = substituteTypeInNeutral m v nt
+
+substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
+substituteTypeInNeutral n v = go n
+  where
+    go _ e@(LCNeutVar _) = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b -> substituteNormalInNormal 0 a' b
+        LCNormTLam _  -> error "Did you really type check this?"
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteTypeInNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _ -> error "Did you really type check this?"
+        LCNormTLam b  -> substituteTypeInNormal 0 t' b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t'
+      where
+        t' = substituteTypeInType m v t
diff --git a/src/LambdaCube/SystemF/TH.hs b/src/LambdaCube/SystemF/TH.hs
--- a/src/LambdaCube/SystemF/TH.hs
+++ b/src/LambdaCube/SystemF/TH.hs
@@ -1,44 +1,45 @@
-module LambdaCube.SystemF.TH where
+module LambdaCube.SystemF.TH
+  ( lc
+  ) where
 
-import           Control.Monad                 ((<=<))
-import qualified Data.Text                     as Text
+import           Data.Data                  (Data)
+import           Data.Generics              (extQ)
+import           Data.Text                  (Text)
+import qualified Data.Text                  as Text
 import           LambdaCube.SystemF.Ast
-import           LambdaCube.SystemF.Elaborator
 import           LambdaCube.SystemF.Parser
-import           Language.Haskell.TH.Quote     (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax    (Loc (loc_start), Q, lift,
-                                                location)
-import qualified Text.Megaparsec               as P
-import qualified Text.Megaparsec.Error         as PE
+import           Language.Haskell.TH.Lib    (ExpQ, varE)
+import           Language.Haskell.TH.Quote  (QuasiQuoter (..))
+import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,
+                                             location, mkName)
+import qualified Text.Megaparsec            as P
+import qualified Text.Megaparsec.Error      as PE
 
-systemF :: QuasiQuoter
-systemF =
+lc :: QuasiQuoter
+lc =
   QuasiQuoter
-    { quoteExp = lift <=< systemFQuoteExp
+    { quoteExp = expLc
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-systemFQuoteExp :: String -> Q ExtLCTerm
-systemFQuoteExp str = do
+expLc :: String -> ExpQ
+expLc str = do
   l <- location
   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> pure e
+    Right e  -> dataToExpQ converter e
     Left err -> fail $ PE.errorBundlePretty err
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      const Nothing
+      `extQ` quotedMVar
+      `extQ` quotedMTVar
+      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
-elaboratedSystemF :: QuasiQuoter
-elaboratedSystemF =
-  QuasiQuoter
-    { quoteExp = lift <=< elaboratedSystemFQuoteExp
-    , quotePat = undefined
-    , quoteType = undefined
-    , quoteDec = undefined
-    }
+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
+    quotedMVar _             = Nothing
 
-elaboratedSystemFQuoteExp :: String -> Q LCTerm
-elaboratedSystemFQuoteExp str = do
-  e <- systemFQuoteExp str
-  case elaborate e of
-    Right e' -> pure e'
-    Left err -> fail err
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
diff --git a/src/LambdaCube/SystemF/TypeChecker.hs b/src/LambdaCube/SystemF/TypeChecker.hs
--- a/src/LambdaCube/SystemF/TypeChecker.hs
+++ b/src/LambdaCube/SystemF/TypeChecker.hs
@@ -1,40 +1,23 @@
 module LambdaCube.SystemF.TypeChecker where
 
-import           Data.List              (uncons)
+import           Data.List                       (uncons)
 import           LambdaCube.SystemF.Ast
-
-substituteType :: Int -> LCType -> LCTerm -> LCTerm
-substituteType n v = go n
-  where
-    go _ e@(LCVar _)  = e
-    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam b)   = LCTLam $ go (m + 1) b
-    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
-
-substituteTypeInType :: Int -> LCType -> LCType -> LCType
-substituteTypeInType n v = go n
-  where
-    go _ LCBase       = LCBase
-    go m e@(LCTVar l) = if m == l then v else e
-    go m (LCArr a b)  = go m a `LCArr` go m b
-    go m (LCUniv a)   = LCUniv $ go (m + 1) a
+import           LambdaCube.SystemF.Substitution
 
-infer :: LCTerm -> Maybe LCType
+infer :: LCTerm -> LCType
 infer = go []
   where
-    go tl (LCVar n) = fmap fst . uncons $ drop n tl
-    go tl (LCLam t b) = LCArr t <$> go (t : tl) b
+    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl
+    go tl (LCLam t b) = t `LCArr` go (t : tl) b
     go tl (LCApp f a)
-      | Just (LCArr at' rt) <- go tl f
-      , Just at <- go tl a
-      , at == at'
-      = Just rt
+      | LCArr at rt <- go tl f
+      , at == go tl a
+      = rt
       | otherwise
-      = Nothing
-    go tl (LCTLam b) = LCUniv <$> go tl b
+      = error "Function argument type mismatch"
+    go tl (LCTLam b) = LCUniv $ go tl b
     go tl (LCTApp f t)
-      | Just (LCUniv rt) <- go tl f
-      = Just $ substituteTypeInType 0 t rt
+      | LCUniv rt <- go tl f
+      = substituteTypeInType 0 t rt
       | otherwise
-      = Nothing
+      = error "Function argument type mismatch"
diff --git a/src/LambdaCube/SystemFw.hs b/src/LambdaCube/SystemFw.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw.hs
@@ -0,0 +1,22 @@
+module LambdaCube.SystemFw
+  ( module LambdaCube.SystemFw.Ast
+  , module LambdaCube.SystemFw.Elaborator
+  , module LambdaCube.SystemFw.Lifter
+  , module LambdaCube.SystemFw.Normalizer
+  , module LambdaCube.SystemFw.Parser
+  , module LambdaCube.SystemFw.PrettyPrinter
+  , module LambdaCube.SystemFw.Substitution
+  , module LambdaCube.SystemFw.TH
+  , module LambdaCube.SystemFw.TypeChecker
+  ) where
+
+import LambdaCube.SystemFw.Ast
+
+import LambdaCube.SystemFw.Elaborator
+import LambdaCube.SystemFw.Lifter
+import LambdaCube.SystemFw.Normalizer
+import LambdaCube.SystemFw.Parser
+import LambdaCube.SystemFw.PrettyPrinter
+import LambdaCube.SystemFw.Substitution
+import LambdaCube.SystemFw.TH
+import LambdaCube.SystemFw.TypeChecker
diff --git a/src/LambdaCube/SystemFw/Ast.hs b/src/LambdaCube/SystemFw/Ast.hs
--- a/src/LambdaCube/SystemFw/Ast.hs
+++ b/src/LambdaCube/SystemFw/Ast.hs
@@ -1,16 +1,25 @@
 module LambdaCube.SystemFw.Ast where
 
+import           Data.Data                  (Data)
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
+data ExtLCKind
+  = ExtLCStar
+  | ExtLCKArr ExtLCKind ExtLCKind
+  | ExtLCMKVar String
+  deriving stock (Eq, Show, Data, Lift)
+infixr 5 `ExtLCKArr`
+
 data ExtLCType
   = ExtLCBase
   | ExtLCTVar Text
   | ExtLCArr ExtLCType ExtLCType
-  | ExtLCUniv Text LCKind ExtLCType
-  | ExtLCTTLam Text LCKind ExtLCType
+  | ExtLCUniv Text ExtLCKind ExtLCType
+  | ExtLCTTLam Text ExtLCKind ExtLCType
   | ExtLCTTApp ExtLCType ExtLCType
-  deriving stock (Eq, Show, Lift)
+  | ExtLCMTVar String
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `ExtLCArr`
 infixl 6 `ExtLCTTApp`
 
@@ -18,16 +27,17 @@
   = ExtLCVar Text
   | ExtLCLam Text ExtLCType ExtLCTerm
   | ExtLCApp ExtLCTerm ExtLCTerm
-  | ExtLCTLam Text LCKind ExtLCTerm
+  | ExtLCTLam Text ExtLCKind ExtLCTerm
   | ExtLCTApp ExtLCTerm ExtLCType
-  deriving stock (Eq, Show, Lift)
+  | ExtLCMVar String
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `ExtLCApp`
 infixl 6 `ExtLCTApp`
 
 data LCKind
   = LCStar
   | LCKArr LCKind LCKind
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `LCKArr`
 
 data LCType
@@ -37,7 +47,7 @@
   | LCUniv LCKind LCType
   | LCTTLam LCKind LCType
   | LCTTApp LCType LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `LCArr`
 infixl 6 `LCTTApp`
 
@@ -47,25 +57,25 @@
   | LCApp LCTerm LCTerm
   | LCTLam LCKind LCTerm
   | LCTApp LCTerm LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCApp`
 infixl 6 `LCTApp`
 
 data LCValue
   = LCValLam LCType LCTerm
   | LCValTLam LCKind LCTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNormalTerm
   = LCNormLam LCType LCNormalTerm
   | LCNormTLam LCKind LCNormalTerm
   | LCNormNeut LCNeutralTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNeutralTerm
   = LCNeutVar Int
   | LCNeutApp LCNeutralTerm LCNormalTerm
   | LCNeutTApp LCNeutralTerm LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCNeutApp`
 infixl 6 `LCNeutTApp`
diff --git a/src/LambdaCube/SystemFw/Elaborator.hs b/src/LambdaCube/SystemFw/Elaborator.hs
--- a/src/LambdaCube/SystemFw/Elaborator.hs
+++ b/src/LambdaCube/SystemFw/Elaborator.hs
@@ -5,29 +5,38 @@
 import qualified Data.Text               as Text
 import           LambdaCube.SystemFw.Ast
 
-elaborate :: ExtLCTerm -> Either String LCTerm
+elaborate :: ExtLCTerm -> LCTerm
 elaborate = go [] []
   where
     go _  vl (ExtLCVar x)
       | Just n <- x `elemIndex` vl
-      = Right $ LCVar n
+      = LCVar n
       | otherwise
-      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"
-    go tl vl (ExtLCLam x t b) = LCLam <$> typeElaborate tl t <*> go tl (x : vl) b
-    go tl vl (ExtLCApp f a) = LCApp <$> go tl vl f <*> go tl vl a
-    go tl vl (ExtLCTLam x k b) = LCTLam k <$> go (x : tl) vl b
-    go tl vl (ExtLCTApp f t) = LCTApp <$> go tl vl f <*> typeElaborate tl t
+      = error $ "Term variable " <> Text.unpack x <> " is not in scope"
+    go tl vl (ExtLCLam x t b) = LCLam (elaborateType tl t) $ go tl (x : vl) b
+    go tl vl (ExtLCApp f a) = go tl vl f `LCApp` go tl vl a
+    go tl vl (ExtLCTLam x k b) = LCTLam (elaborateKind k) $ go (x : tl) vl b
+    go tl vl (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t
+    go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
 
-typeElaborate :: [Text] -> ExtLCType -> Either String LCType
-typeElaborate = go
+elaborateType :: [Text] -> ExtLCType -> LCType
+elaborateType = go
   where
-    go _ ExtLCBase = Right LCBase
+    go _ ExtLCBase = LCBase
     go l (ExtLCTVar x)
       | Just n <- x `elemIndex` l
-      = Right $ LCTVar n
+      = LCTVar n
       | otherwise
-      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"
-    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b
-    go l (ExtLCUniv x k a) = LCUniv k <$> go (x : l) a
-    go l (ExtLCTTLam x k b) = LCTTLam k <$> go (x : l) b
-    go l (ExtLCTTApp f a) = LCTTApp <$> go l f <*> go l a
+      = error $ "Type variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCArr a b) = go l a `LCArr` go l b
+    go l (ExtLCUniv x k a) = LCUniv (elaborateKind k) $ go (x : l) a
+    go l (ExtLCTTLam x k b) = LCTTLam (elaborateKind k) $ go (x : l) b
+    go l (ExtLCTTApp f a) = go l f `LCTTApp` go l a
+    go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
+
+elaborateKind :: ExtLCKind -> LCKind
+elaborateKind = go
+  where
+    go ExtLCStar = LCStar
+    go (ExtLCKArr a b) = go a `LCKArr` go b
+    go (ExtLCMKVar _) = error "invalid TemplateHaskell code splicer"
diff --git a/src/LambdaCube/SystemFw/Evaluator.hs b/src/LambdaCube/SystemFw/Evaluator.hs
--- a/src/LambdaCube/SystemFw/Evaluator.hs
+++ b/src/LambdaCube/SystemFw/Evaluator.hs
@@ -1,20 +1,7 @@
 module LambdaCube.SystemFw.Evaluator where
 
 import           LambdaCube.SystemFw.Ast
-import           LambdaCube.SystemFw.TypeChecker (substituteType)
-
-liftLCValue :: LCValue -> LCTerm
-liftLCValue (LCValLam t b)  = LCLam t b
-liftLCValue (LCValTLam k b) = LCTLam k b
-
-substitute :: Int -> LCValue -> LCTerm -> LCTerm
-substitute n v = go n
-  where
-    go m e@(LCVar l)  = if m == l then liftLCValue v else e
-    go m (LCLam t b)  = LCLam t $ go (m + 1) b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam k b) = LCTLam k $ go m b
-    go m (LCTApp f t) = go m f `LCTApp` t
+import           LambdaCube.SystemFw.Substitution
 
 evaluate :: LCTerm -> LCValue
 evaluate = go
@@ -24,7 +11,7 @@
     go (LCApp f a)
       | LCValLam _ b <- go f
       , v <- go a
-      = go $ substitute 0 v b
+      = go $ substituteValue 0 v b
       | otherwise
       = error "Did you really type check this?"
     go (LCTLam k b) = LCValTLam k b
diff --git a/src/LambdaCube/SystemFw/Lifter.hs b/src/LambdaCube/SystemFw/Lifter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/Lifter.hs
@@ -0,0 +1,17 @@
+module LambdaCube.SystemFw.Lifter where
+
+import           LambdaCube.SystemFw.Ast
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b)  = LCLam t b
+liftLCValue (LCValTLam k b) = LCTLam k b
+
+liftLCNormal :: LCNormalTerm -> LCTerm
+liftLCNormal (LCNormLam t b)  = LCLam t $ liftLCNormal b
+liftLCNormal (LCNormTLam k b) = LCTLam k $ liftLCNormal b
+liftLCNormal (LCNormNeut nt)  = liftLCNeutral nt
+
+liftLCNeutral :: LCNeutralTerm -> LCTerm
+liftLCNeutral (LCNeutVar n)    = LCVar n
+liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a
+liftLCNeutral (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
diff --git a/src/LambdaCube/SystemFw/Normalizer.hs b/src/LambdaCube/SystemFw/Normalizer.hs
--- a/src/LambdaCube/SystemFw/Normalizer.hs
+++ b/src/LambdaCube/SystemFw/Normalizer.hs
@@ -1,59 +1,7 @@
 module LambdaCube.SystemFw.Normalizer where
 
 import           LambdaCube.SystemFw.Ast
-import           LambdaCube.SystemFw.TypeChecker (substituteTypeInType)
-
-substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormal n v = go n
-  where
-    go m (LCNormLam t b)  = LCNormLam t $ go (m + 1) b
-    go m (LCNormTLam k b) = LCNormTLam k $ go m b
-    go m (LCNormNeut nt)  = substituteNeutral m v nt
-
-substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNeutral n v = go n
-  where
-    go m e@(LCNeutVar l)
-      | m == l = v
-      | otherwise = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b  -> substituteNormal 0 a' b
-        LCNormTLam _ _ -> error "Did you really type check this?"
-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
-      where
-        a' = substituteNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
-        LCNormLam _ _  -> error "Did you really type check this?"
-        LCNormTLam _ b -> substituteTypeNormal 0 t b
-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t
-
-substituteTypeNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
-substituteTypeNormal n v = go n
-  where
-    go m (LCNormLam t b)  = LCNormLam (substituteTypeInType m v t) $ go m b
-    go m (LCNormTLam k b) = LCNormTLam k $ go (m + 1) b
-    go m (LCNormNeut nt)  = substituteTypeNeutral m v nt
-
-substituteTypeNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
-substituteTypeNeutral n v = go n
-  where
-    go _ e@(LCNeutVar _) = LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b  -> substituteNormal 0 a' b
-        LCNormTLam _ _ -> error "Did you really type check this?"
-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
-      where
-        a' = substituteTypeNormal m v a
-    go m (LCNeutTApp f t) =
-      case go m f of
-        LCNormLam _ _  -> error "Did you really type check this?"
-        LCNormTLam _ b -> substituteTypeNormal 0 t' b
-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t'
-      where
-        t' = substituteTypeInType m v t
+import           LambdaCube.SystemFw.Substitution
 
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
@@ -63,7 +11,7 @@
     go (LCTLam k b) = LCNormTLam k $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam _ b   -> substituteNormal 0 a' b
+        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
         LCNormTLam _ _  -> error "Did you really type check this?"
         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
       where
@@ -71,5 +19,5 @@
     go (LCTApp f t) =
       case go f of
         LCNormLam _ _   -> error "Did you really type check this?"
-        LCNormTLam _ b  -> substituteTypeNormal 0 t b
+        LCNormTLam _ b  -> substituteTypeInNormal 0 t b
         LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
diff --git a/src/LambdaCube/SystemFw/Parser.hs b/src/LambdaCube/SystemFw/Parser.hs
--- a/src/LambdaCube/SystemFw/Parser.hs
+++ b/src/LambdaCube/SystemFw/Parser.hs
@@ -4,6 +4,7 @@
 import           Data.Function            ((&))
 import           Data.Functor             (($>))
 import           Data.Maybe               (isJust)
+import qualified Data.Text                as Text
 import           LambdaCube.Common.Parser
 import           LambdaCube.SystemFw.Ast
 import           Text.Megaparsec
@@ -39,8 +40,14 @@
     else flip ExtLCApp <$> pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pLC
 
+pVar :: Parser ExtLCTerm
+pVar = ExtLCVar <$> identifier
+
+pMVar :: Parser ExtLCTerm
+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
+
 pType :: Parser ExtLCType
 pType = pTTLam <|> pUniv <|> pArr
 
@@ -65,10 +72,25 @@
 pTTApp = foldl' ExtLCTTApp <$> pAType <*> many pAType
 
 pAType :: Parser ExtLCType
-pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType
+pAType = pBase <|> pTVar <|> pMTVar <|> parenthesized pType
 
-pKind :: Parser LCKind
-pKind = foldr1 LCKArr <$> sepBy1 pAKind rightArrow
+pBase :: Parser ExtLCType
+pBase = sharp $> ExtLCBase
 
-pAKind :: Parser LCKind
-pAKind = (asterisk $> LCStar) <|> parenthesized pKind
+pTVar :: Parser ExtLCType
+pTVar = ExtLCTVar <$> identifier
+
+pMTVar :: Parser ExtLCType
+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
+
+pKind :: Parser ExtLCKind
+pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow
+
+pAKind :: Parser ExtLCKind
+pAKind = pStar <|> pMKVar <|> parenthesized pKind
+
+pStar :: Parser ExtLCKind
+pStar = asterisk $> ExtLCStar
+
+pMKVar :: Parser ExtLCKind
+pMKVar = ExtLCMKVar <$> (dollarsign *> fmap Text.unpack identifier)
diff --git a/src/LambdaCube/SystemFw/PrettyPrinter.hs b/src/LambdaCube/SystemFw/PrettyPrinter.hs
--- a/src/LambdaCube/SystemFw/PrettyPrinter.hs
+++ b/src/LambdaCube/SystemFw/PrettyPrinter.hs
@@ -9,25 +9,25 @@
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.SystemFw.Ast
 
-prettyKind :: LCKind -> Text
-prettyKind = prettyKindPrec 0
+prettyUnnamedKind :: LCKind -> Text
+prettyUnnamedKind = prettyUnnamedKindPrec 0
 
-prettyType :: LCType -> Text
-prettyType = prettyTypePrec 0
+prettyUnnamedType :: LCType -> Text
+prettyUnnamedType = prettyUnnamedTypePrec 0
 
-prettyTerm :: LCTerm -> Text
-prettyTerm = prettyTermPrec 0
+prettyUnnamedTerm :: LCTerm -> Text
+prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
-prettyKindPrec :: Int -> LCKind -> Text
-prettyKindPrec = go
+prettyUnnamedKindPrec :: Int -> LCKind -> Text
+prettyUnnamedKindPrec = go
   where
     go _ LCStar       = "*"
     go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
 
-prettyTypePrec :: Int -> LCType -> Text
-prettyTypePrec = go
+prettyUnnamedTypePrec :: Int -> LCType -> Text
+prettyUnnamedTypePrec = go
   where
-    pKP = prettyKindPrec
+    pKP = prettyUnnamedKindPrec
 
     go _ LCBase        = "#"
     go _ (LCTVar i)    = Text.pack $ show i
@@ -36,11 +36,11 @@
     go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]
     go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
 
-prettyTermPrec :: Int -> LCTerm -> Text
-prettyTermPrec = go
+prettyUnnamedTermPrec :: Int -> LCTerm -> Text
+prettyUnnamedTermPrec = go
   where
-    pKP = prettyKindPrec
-    pTP = prettyTypePrec
+    pKP = prettyUnnamedKindPrec
+    pTP = prettyUnnamedTypePrec
 
     go _ (LCVar i)    = Text.pack $ show i
     go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
diff --git a/src/LambdaCube/SystemFw/Substitution.hs b/src/LambdaCube/SystemFw/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw/Substitution.hs
@@ -0,0 +1,84 @@
+module LambdaCube.SystemFw.Substitution where
+
+import           LambdaCube.SystemFw.Ast
+import           LambdaCube.SystemFw.Lifter
+
+substituteType :: Int -> LCType -> LCTerm -> LCTerm
+substituteType n v = go n
+  where
+    go _ e@(LCVar _)  = e
+    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam k b) = LCTLam k $ go (m + 1) b
+    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
+
+substituteTypeInType :: Int -> LCType -> LCType -> LCType
+substituteTypeInType n v = go n
+  where
+    go _ LCBase        = LCBase
+    go m e@(LCTVar l)  = if m == l then v else e
+    go m (LCArr a b)   = go m a `LCArr` go m b
+    go m (LCUniv k a)  = LCUniv k $ go (m + 1) a
+    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
+    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+
+substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
+substituteValue n v = go n
+  where
+    go m e@(LCVar l)  = if m == l then liftLCValue v else e
+    go m (LCLam t b)  = LCLam t $ go (m + 1) b
+    go m (LCApp f a)  = go m f `LCApp` go m a
+    go m (LCTLam k b) = LCTLam k $ go m b
+    go m (LCTApp f t) = go m f `LCTApp` t
+
+substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal n v = go n
+  where
+    go m (LCNormLam t b)  = LCNormLam t $ go (m + 1) b
+    go m (LCNormTLam k b) = LCNormTLam k $ go m b
+    go m (LCNormNeut nt)  = substituteNormalInNeutral m v nt
+
+substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNormalInNeutral n v = go n
+  where
+    go m e@(LCNeutVar l)
+      | m == l = v
+      | otherwise = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b  -> substituteNormalInNormal 0 a' b
+        LCNormTLam _ _ -> error "Did you really type check this?"
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteNormalInNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _  -> error "Did you really type check this?"
+        LCNormTLam _ b -> substituteTypeInNormal 0 t b
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t
+
+substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm
+substituteTypeInNormal n v = go n
+  where
+    go m (LCNormLam t b)  = LCNormLam (substituteTypeInType m v t) $ go m b
+    go m (LCNormTLam k b) = LCNormTLam k $ go (m + 1) b
+    go m (LCNormNeut nt)  = substituteTypeInNeutral m v nt
+
+substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm
+substituteTypeInNeutral n v = go n
+  where
+    go _ e@(LCNeutVar _) = LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b  -> substituteNormalInNormal 0 a' b
+        LCNormTLam _ _ -> error "Did you really type check this?"
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteTypeInNormal m v a
+    go m (LCNeutTApp f t) =
+      case go m f of
+        LCNormLam _ _  -> error "Did you really type check this?"
+        LCNormTLam _ b -> substituteTypeInNormal 0 t' b
+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t'
+      where
+        t' = substituteTypeInType m v t
diff --git a/src/LambdaCube/SystemFw/TH.hs b/src/LambdaCube/SystemFw/TH.hs
--- a/src/LambdaCube/SystemFw/TH.hs
+++ b/src/LambdaCube/SystemFw/TH.hs
@@ -1,44 +1,49 @@
-module LambdaCube.SystemFw.TH where
+module LambdaCube.SystemFw.TH
+  ( lc
+  ) where
 
-import           Control.Monad                  ((<=<))
-import qualified Data.Text                      as Text
+import           Data.Data                  (Data)
+import           Data.Generics              (extQ)
+import           Data.Text                  (Text)
+import qualified Data.Text                  as Text
 import           LambdaCube.SystemFw.Ast
-import           LambdaCube.SystemFw.Elaborator
 import           LambdaCube.SystemFw.Parser
-import           Language.Haskell.TH.Quote      (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax     (Loc (loc_start), Q, lift,
-                                                 location)
-import qualified Text.Megaparsec                as P
-import qualified Text.Megaparsec.Error          as PE
+import           Language.Haskell.TH.Lib    (ExpQ, varE)
+import           Language.Haskell.TH.Quote  (QuasiQuoter (..))
+import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,
+                                             location, mkName)
+import qualified Text.Megaparsec            as P
+import qualified Text.Megaparsec.Error      as PE
 
-systemFw :: QuasiQuoter
-systemFw =
+lc :: QuasiQuoter
+lc =
   QuasiQuoter
-    { quoteExp = lift <=< systemFwQuoteExp
+    { quoteExp = expLc
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-systemFwQuoteExp :: String -> Q ExtLCTerm
-systemFwQuoteExp str = do
+expLc :: String -> ExpQ
+expLc str = do
   l <- location
   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> pure e
+    Right e  -> dataToExpQ converter e
     Left err -> fail $ PE.errorBundlePretty err
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      const Nothing
+      `extQ` quotedMVar
+      `extQ` quotedMTVar
+      `extQ` quotedMKVar
+      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
-elaboratedSystemFw :: QuasiQuoter
-elaboratedSystemFw =
-  QuasiQuoter
-    { quoteExp = lift <=< elaboratedSystemFwQuoteExp
-    , quotePat = undefined
-    , quoteType = undefined
-    , quoteDec = undefined
-    }
+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
+    quotedMVar _             = Nothing
 
-elaboratedSystemFwQuoteExp :: String -> Q LCTerm
-elaboratedSystemFwQuoteExp str = do
-  e <- systemFwQuoteExp str
-  case elaborate e of
-    Right e' -> pure e'
-    Left err -> fail err
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
+
+    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
+    quotedMKVar _              = Nothing
diff --git a/src/LambdaCube/SystemFw/TypeChecker.hs b/src/LambdaCube/SystemFw/TypeChecker.hs
--- a/src/LambdaCube/SystemFw/TypeChecker.hs
+++ b/src/LambdaCube/SystemFw/TypeChecker.hs
@@ -1,26 +1,8 @@
 module LambdaCube.SystemFw.TypeChecker where
 
-import           Data.List               (uncons)
+import           Data.List                        (uncons)
 import           LambdaCube.SystemFw.Ast
-
-substituteType :: Int -> LCType -> LCTerm -> LCTerm
-substituteType n v = go n
-  where
-    go _ e@(LCVar _)  = e
-    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b
-    go m (LCApp f a)  = go m f `LCApp` go m a
-    go m (LCTLam k b) = LCTLam k $ go (m + 1) b
-    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t
-
-substituteTypeInType :: Int -> LCType -> LCType -> LCType
-substituteTypeInType n v = go n
-  where
-    go _ LCBase        = LCBase
-    go m e@(LCTVar l)  = if m == l then v else e
-    go m (LCArr a b)   = go m a `LCArr` go m b
-    go m (LCUniv k a)  = LCUniv k $ go (m + 1) a
-    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
-    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+import           LambdaCube.SystemFw.Substitution
 
 reduceType :: LCType -> LCType
 reduceType = go
@@ -37,50 +19,47 @@
       | otherwise
       = error "Did you really kind check this?"
 
-infer :: LCTerm -> Maybe LCType
+infer :: LCTerm -> LCType
 infer = go []
   where
-    go tl (LCVar n) = fmap fst . uncons $ drop n tl
+    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl
     go tl (LCLam t b)
-      | Just LCStar <- inferKind t
-      = LCArr v <$> go (v : tl) b
+      | LCStar <- inferKind t
+      = v `LCArr` go (v : tl) b
       | otherwise
-      = Nothing
+      = error "Function argument kind mismatch"
       where
         v = reduceType t
     go tl (LCApp f a)
-      | Just (LCArr at' rt) <- go tl f
-      , Just at <- go tl a
-      , at == at'
-      = Just rt
+      | LCArr at rt <- go tl f
+      , at == go tl a
+      = rt
       | otherwise
-      = Nothing
-    go tl (LCTLam k b) = LCUniv k <$> go tl b
+      = error "Function argument type mismatch"
+    go tl (LCTLam k b) = LCUniv k $ go tl b
     go tl (LCTApp f t)
-      | Just (LCUniv tk' rt) <- go tl f
-      , Just tk <- inferKind t
-      , tk == tk'
-      = Just $ substituteTypeInType 0 t rt
+      | LCUniv tk rt <- go tl f
+      , tk == inferKind t
+      = substituteTypeInType 0 t rt
       | otherwise
-      = Nothing
+      = error "Function argument kind mismatch"
 
-inferKind :: LCType -> Maybe LCKind
+inferKind :: LCType -> LCKind
 inferKind = go []
   where
-    go _  LCBase = Just LCStar
-    go kl (LCTVar n) = fmap fst . uncons $ drop n kl
+    go _  LCBase = LCStar
+    go kl (LCTVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n kl
     go kl (LCArr a b)
-      | Just LCStar <- go kl a
-      , Just LCStar <- go kl b
-      = Just LCStar
+      | LCStar <- go kl a
+      , LCStar <- go kl b
+      = LCStar
       | otherwise
-      = Nothing
+      = error "Arrow kind mismatch"
     go kl (LCUniv k a) = go (k : kl) a
-    go kl (LCTTLam k b) = LCKArr k <$> go (k : kl) b
+    go kl (LCTTLam k b) = LCKArr k $ go (k : kl) b
     go kl (LCTTApp f a)
-      | Just (LCKArr ak' rk) <- go kl f
-      , Just ak <- go kl a
-      , ak == ak'
-      = Just rk
+      | LCKArr ak rk <- go kl f
+      , ak == go kl a
+      = rk
       | otherwise
-      = Nothing
+      = error "Function argument kind mismatch"
diff --git a/src/LambdaCube/SystemFw_.hs b/src/LambdaCube/SystemFw_.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_.hs
@@ -0,0 +1,22 @@
+module LambdaCube.SystemFw_
+  ( module LambdaCube.SystemFw_.Ast
+  , module LambdaCube.SystemFw_.Elaborator
+  , module LambdaCube.SystemFw_.Lifter
+  , module LambdaCube.SystemFw_.Normalizer
+  , module LambdaCube.SystemFw_.Parser
+  , module LambdaCube.SystemFw_.PrettyPrinter
+  , module LambdaCube.SystemFw_.Substitution
+  , module LambdaCube.SystemFw_.TH
+  , module LambdaCube.SystemFw_.TypeChecker
+  ) where
+
+import LambdaCube.SystemFw_.Ast
+
+import LambdaCube.SystemFw_.Elaborator
+import LambdaCube.SystemFw_.Lifter
+import LambdaCube.SystemFw_.Normalizer
+import LambdaCube.SystemFw_.Parser
+import LambdaCube.SystemFw_.PrettyPrinter
+import LambdaCube.SystemFw_.Substitution
+import LambdaCube.SystemFw_.TH
+import LambdaCube.SystemFw_.TypeChecker
diff --git a/src/LambdaCube/SystemFw_/Ast.hs b/src/LambdaCube/SystemFw_/Ast.hs
--- a/src/LambdaCube/SystemFw_/Ast.hs
+++ b/src/LambdaCube/SystemFw_/Ast.hs
@@ -1,15 +1,24 @@
 module LambdaCube.SystemFw_.Ast where
 
+import           Data.Data                  (Data)
 import           Data.Text                  (Text)
 import           Language.Haskell.TH.Syntax (Lift)
 
+data ExtLCKind
+  = ExtLCStar
+  | ExtLCKArr ExtLCKind ExtLCKind
+  | ExtLCMKVar String
+  deriving stock (Eq, Show, Data, Lift)
+infixr 5 `ExtLCKArr`
+
 data ExtLCType
   = ExtLCBase
   | ExtLCTVar Text
   | ExtLCArr ExtLCType ExtLCType
-  | ExtLCTTLam Text LCKind ExtLCType
+  | ExtLCTTLam Text ExtLCKind ExtLCType
   | ExtLCTTApp ExtLCType ExtLCType
-  deriving stock (Eq, Show, Lift)
+  | ExtLCMTVar String
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `ExtLCArr`
 infixl 6 `ExtLCTTApp`
 
@@ -17,13 +26,14 @@
   = ExtLCVar Text
   | ExtLCLam Text ExtLCType ExtLCTerm
   | ExtLCApp ExtLCTerm ExtLCTerm
-  deriving stock (Eq, Show, Lift)
+  | ExtLCMVar String
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `ExtLCApp`
 
 data LCKind
   = LCStar
   | LCKArr LCKind LCKind
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `LCKArr`
 
 data LCType
@@ -32,7 +42,7 @@
   | LCArr LCType LCType
   | LCTTLam LCKind LCType
   | LCTTApp LCType LCType
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixr 5 `LCArr`
 infixl 6 `LCTTApp`
 
@@ -40,20 +50,20 @@
   = LCVar Int
   | LCLam LCType LCTerm
   | LCApp LCTerm LCTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCApp`
 
 data LCValue
   = LCValLam LCType LCTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNormalTerm
   = LCNormLam LCType LCNormalTerm
   | LCNormNeut LCNeutralTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 
 data LCNeutralTerm
   = LCNeutVar Int
   | LCNeutApp LCNeutralTerm LCNormalTerm
-  deriving stock (Eq, Show, Lift)
+  deriving stock (Eq, Show, Data, Lift)
 infixl 6 `LCNeutApp`
diff --git a/src/LambdaCube/SystemFw_/Elaborator.hs b/src/LambdaCube/SystemFw_/Elaborator.hs
--- a/src/LambdaCube/SystemFw_/Elaborator.hs
+++ b/src/LambdaCube/SystemFw_/Elaborator.hs
@@ -4,26 +4,35 @@
 import qualified Data.Text                as Text
 import           LambdaCube.SystemFw_.Ast
 
-elaborate :: ExtLCTerm -> Either String LCTerm
+elaborate :: ExtLCTerm -> LCTerm
 elaborate = go []
   where
     go l (ExtLCVar x)
       | Just n <- x `elemIndex` l
-      = Right $ LCVar n
+      = LCVar n
       | otherwise
-      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"
-    go l (ExtLCLam x t b) = LCLam <$> typeElaborate t <*> go (x : l) b
-    go l (ExtLCApp f a) = LCApp <$> go l f <*> go l a
+      = error $ "Term variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCLam x t b) = LCLam (elaborateType t) $ go (x : l) b
+    go l (ExtLCApp f a) = go l f `LCApp` go l a
+    go _ (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
 
-typeElaborate :: ExtLCType -> Either String LCType
-typeElaborate = go []
+elaborateType :: ExtLCType -> LCType
+elaborateType = go []
   where
-    go _ ExtLCBase = Right LCBase
+    go _ ExtLCBase = LCBase
     go l (ExtLCTVar x)
       | Just n <- x `elemIndex` l
-      = Right $ LCTVar n
+      = LCTVar n
       | otherwise
-      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"
-    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b
-    go l (ExtLCTTLam x k b) = LCTTLam k <$> go (x : l) b
-    go l (ExtLCTTApp f a) = LCTTApp <$> go l f <*> go l a
+      = error $ "Type variable " <> Text.unpack x <> " is not in scope"
+    go l (ExtLCArr a b) = go l a `LCArr` go l b
+    go l (ExtLCTTLam x k b) = LCTTLam (elaborateKind k) $ go (x : l) b
+    go l (ExtLCTTApp f a) = go l f `LCTTApp` go l a
+    go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
+
+elaborateKind :: ExtLCKind -> LCKind
+elaborateKind = go
+  where
+    go ExtLCStar = LCStar
+    go (ExtLCKArr a b) = go a `LCKArr` go b
+    go (ExtLCMKVar _) = error "invalid TemplateHaskell code splicer"
diff --git a/src/LambdaCube/SystemFw_/Evaluator.hs b/src/LambdaCube/SystemFw_/Evaluator.hs
--- a/src/LambdaCube/SystemFw_/Evaluator.hs
+++ b/src/LambdaCube/SystemFw_/Evaluator.hs
@@ -1,16 +1,7 @@
 module LambdaCube.SystemFw_.Evaluator where
 
 import           LambdaCube.SystemFw_.Ast
-
-liftLCValue :: LCValue -> LCTerm
-liftLCValue (LCValLam t b) = LCLam t b
-
-substitute :: Int -> LCValue -> LCTerm -> LCTerm
-substitute n v = go n
-  where
-    go m e@(LCVar l) = if m == l then liftLCValue v else e
-    go m (LCLam t b) = LCLam t (substitute (m + 1) v b)
-    go m (LCApp f a) = LCApp (go m f) (go m a)
+import           LambdaCube.SystemFw_.Substitution
 
 evaluate :: LCTerm -> LCValue
 evaluate = go
@@ -20,6 +11,6 @@
     go (LCApp f a)
       | LCValLam _ b <- go f
       , v <- go a
-      = go (substitute 0 v b)
+      = go (substituteValue 0 v b)
       | otherwise
       = error "Did you really type check this?"
diff --git a/src/LambdaCube/SystemFw_/Lifter.hs b/src/LambdaCube/SystemFw_/Lifter.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/Lifter.hs
@@ -0,0 +1,14 @@
+module LambdaCube.SystemFw_.Lifter where
+
+import LambdaCube.SystemFw_.Ast
+
+liftLCValue :: LCValue -> LCTerm
+liftLCValue (LCValLam t b) = LCLam t b
+
+liftLCNormal :: LCNormalTerm -> LCTerm
+liftLCNormal (LCNormLam t b)  = LCLam t $ liftLCNormal b
+liftLCNormal (LCNormNeut nt)  = liftLCNeutral nt
+
+liftLCNeutral :: LCNeutralTerm -> LCTerm
+liftLCNeutral (LCNeutVar n)    = LCVar n
+liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a
diff --git a/src/LambdaCube/SystemFw_/Normalizer.hs b/src/LambdaCube/SystemFw_/Normalizer.hs
--- a/src/LambdaCube/SystemFw_/Normalizer.hs
+++ b/src/LambdaCube/SystemFw_/Normalizer.hs
@@ -1,24 +1,8 @@
 module LambdaCube.SystemFw_.Normalizer where
 
 import           LambdaCube.SystemFw_.Ast
-import           LambdaCube.SystemFw_.TypeChecker (reduceType)
-
-substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
-substituteNormal n v = go n
-  where
-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
-    go m (LCNormNeut nt) = substituteNeutral m v nt
-
-substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
-substituteNeutral n v = go n
-  where
-    go m e@(LCNeutVar l) = if m == l then v else LCNormNeut e
-    go m (LCNeutApp f a) =
-      case go m f of
-        LCNormLam _ b -> substituteNormal 0 a' b
-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
-      where
-        a' = substituteNormal m v a
+import           LambdaCube.SystemFw_.Substitution
+import           LambdaCube.SystemFw_.TypeChecker  (reduceType)
 
 normalize :: LCTerm -> LCNormalTerm
 normalize = go
@@ -27,7 +11,7 @@
     go (LCLam t b) = LCNormLam (reduceType t) $ go b
     go (LCApp f a) =
       case go f of
-        LCNormLam _ b   -> substituteNormal 0 a' b
+        LCNormLam _ b   -> substituteNormalInNormal 0 a' b
         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
       where
         a' = go a
diff --git a/src/LambdaCube/SystemFw_/Parser.hs b/src/LambdaCube/SystemFw_/Parser.hs
--- a/src/LambdaCube/SystemFw_/Parser.hs
+++ b/src/LambdaCube/SystemFw_/Parser.hs
@@ -2,6 +2,7 @@
 
 import           Data.Foldable            (Foldable (foldl'))
 import           Data.Functor             (($>))
+import qualified Data.Text                as Text
 import           LambdaCube.Common.Parser
 import           LambdaCube.SystemFw_.Ast
 import           Text.Megaparsec
@@ -23,8 +24,14 @@
 pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm
 
 pATerm :: Parser ExtLCTerm
-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC
+pATerm = pVar <|> pMVar <|> parenthesized pLC
 
+pVar :: Parser ExtLCTerm
+pVar = ExtLCVar <$> identifier
+
+pMVar :: Parser ExtLCTerm
+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)
+
 pType :: Parser ExtLCType
 pType = pTTLam <|> pArr
 
@@ -42,10 +49,25 @@
 pTTApp = foldl' ExtLCTTApp <$> pAType <*> many pAType
 
 pAType :: Parser ExtLCType
-pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType
+pAType = pBase <|> pTVar <|> pMTVar <|> parenthesized pType
 
-pKind :: Parser LCKind
-pKind = foldr1 LCKArr <$> sepBy1 pAKind rightArrow
+pBase :: Parser ExtLCType
+pBase = sharp $> ExtLCBase
 
-pAKind :: Parser LCKind
-pAKind = (asterisk $> LCStar) <|> parenthesized pKind
+pTVar :: Parser ExtLCType
+pTVar = ExtLCTVar <$> identifier
+
+pMTVar :: Parser ExtLCType
+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
+
+pKind :: Parser ExtLCKind
+pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow
+
+pAKind :: Parser ExtLCKind
+pAKind = pStar <|> pMKVar <|> parenthesized pKind
+
+pStar :: Parser ExtLCKind
+pStar = asterisk $> ExtLCStar
+
+pMKVar :: Parser ExtLCKind
+pMKVar = ExtLCMKVar <$> (dollarsign *> fmap Text.unpack identifier)
diff --git a/src/LambdaCube/SystemFw_/PrettyPrinter.hs b/src/LambdaCube/SystemFw_/PrettyPrinter.hs
--- a/src/LambdaCube/SystemFw_/PrettyPrinter.hs
+++ b/src/LambdaCube/SystemFw_/PrettyPrinter.hs
@@ -9,25 +9,25 @@
 import           LambdaCube.Common.PrettyPrinter
 import           LambdaCube.SystemFw_.Ast
 
-prettyKind :: LCKind -> Text
-prettyKind = prettyKindPrec 0
+prettyUnnamedKind :: LCKind -> Text
+prettyUnnamedKind = prettyUnnamedKindPrec 0
 
-prettyType :: LCType -> Text
-prettyType = prettyTypePrec 0
+prettyUnnamedType :: LCType -> Text
+prettyUnnamedType = prettyUnnamedTypePrec 0
 
-prettyTerm :: LCTerm -> Text
-prettyTerm = prettyTermPrec 0
+prettyUnnamedTerm :: LCTerm -> Text
+prettyUnnamedTerm = prettyUnnamedTermPrec 0
 
-prettyKindPrec :: Int -> LCKind -> Text
-prettyKindPrec = go
+prettyUnnamedKindPrec :: Int -> LCKind -> Text
+prettyUnnamedKindPrec = go
   where
     go _ LCStar       = "*"
     go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
 
-prettyTypePrec :: Int -> LCType -> Text
-prettyTypePrec = go
+prettyUnnamedTypePrec :: Int -> LCType -> Text
+prettyUnnamedTypePrec = go
   where
-    pKP = prettyKindPrec
+    pKP = prettyUnnamedKindPrec
 
     go _ LCBase        = "#"
     go _ (LCTVar i)    = Text.pack $ show i
@@ -35,10 +35,10 @@
     go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]
     go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]
 
-prettyTermPrec :: Int -> LCTerm -> Text
-prettyTermPrec = go
+prettyUnnamedTermPrec :: Int -> LCTerm -> Text
+prettyUnnamedTermPrec = go
   where
-    pTP = prettyTypePrec
+    pTP = prettyUnnamedTypePrec
 
     go _ (LCVar i)   = Text.pack $ show i
     go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
diff --git a/src/LambdaCube/SystemFw_/Substitution.hs b/src/LambdaCube/SystemFw_/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/LambdaCube/SystemFw_/Substitution.hs
@@ -0,0 +1,37 @@
+module LambdaCube.SystemFw_.Substitution where
+
+import           LambdaCube.SystemFw_.Ast
+import           LambdaCube.SystemFw_.Lifter
+
+substituteTypeInType :: Int -> LCType -> LCType -> LCType
+substituteTypeInType n v = go n
+  where
+    go _ LCBase        = LCBase
+    go m e@(LCTVar l)  = if m == l then v else e
+    go m (LCArr a b)   = go m a `LCArr` go m b
+    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
+    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+
+substituteValue :: Int -> LCValue -> LCTerm -> LCTerm
+substituteValue n v = go n
+  where
+    go m e@(LCVar l) = if m == l then liftLCValue v else e
+    go m (LCLam t b) = LCLam t (go (m + 1) b)
+    go m (LCApp f a) = LCApp (go m f) (go m a)
+
+substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
+substituteNormalInNormal n v = go n
+  where
+    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
+    go m (LCNormNeut nt) = substituteNormalInNeutral m v nt
+
+substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
+substituteNormalInNeutral n v = go n
+  where
+    go m e@(LCNeutVar l) = if m == l then v else LCNormNeut e
+    go m (LCNeutApp f a) =
+      case go m f of
+        LCNormLam _ b -> substituteNormalInNormal 0 a' b
+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
+      where
+        a' = substituteNormalInNormal m v a
diff --git a/src/LambdaCube/SystemFw_/TH.hs b/src/LambdaCube/SystemFw_/TH.hs
--- a/src/LambdaCube/SystemFw_/TH.hs
+++ b/src/LambdaCube/SystemFw_/TH.hs
@@ -1,44 +1,49 @@
-module LambdaCube.SystemFw_.TH where
+module LambdaCube.SystemFw_.TH
+  ( lc
+  ) where
 
-import           Control.Monad                   ((<=<))
-import qualified Data.Text                       as Text
+import           Data.Data                   (Data)
+import           Data.Generics               (extQ)
+import           Data.Text                   (Text)
+import qualified Data.Text                   as Text
 import           LambdaCube.SystemFw_.Ast
-import           LambdaCube.SystemFw_.Elaborator
 import           LambdaCube.SystemFw_.Parser
-import           Language.Haskell.TH.Quote       (QuasiQuoter (..))
-import           Language.Haskell.TH.Syntax      (Loc (loc_start), Q, lift,
-                                                  location)
-import qualified Text.Megaparsec                 as P
-import qualified Text.Megaparsec.Error           as PE
+import           Language.Haskell.TH.Lib     (ExpQ, varE)
+import           Language.Haskell.TH.Quote   (QuasiQuoter (..))
+import           Language.Haskell.TH.Syntax  (Loc (loc_start), dataToExpQ, lift,
+                                              location, mkName)
+import qualified Text.Megaparsec             as P
+import qualified Text.Megaparsec.Error       as PE
 
-systemFw_ :: QuasiQuoter
-systemFw_ =
+lc :: QuasiQuoter
+lc =
   QuasiQuoter
-    { quoteExp = lift <=< systemFw_QuoteExp
+    { quoteExp = expLc
     , quotePat = undefined
     , quoteType = undefined
     , quoteDec = undefined
     }
 
-systemFw_QuoteExp :: String -> Q ExtLCTerm
-systemFw_QuoteExp str = do
+expLc :: String -> ExpQ
+expLc str = do
   l <- location
   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of
-    Right e  -> pure e
+    Right e  -> dataToExpQ converter e
     Left err -> fail $ PE.errorBundlePretty err
+  where
+    converter :: Data b => b -> Maybe ExpQ
+    converter =
+      const Nothing
+      `extQ` quotedMVar
+      `extQ` quotedMTVar
+      `extQ` quotedMKVar
+      `extQ` (Just . lift :: Text -> Maybe ExpQ)
 
-elaboratedSystemFw_ :: QuasiQuoter
-elaboratedSystemFw_ =
-  QuasiQuoter
-    { quoteExp = lift <=< elaboratedSystemFw_QuoteExp
-    , quotePat = undefined
-    , quoteType = undefined
-    , quoteDec = undefined
-    }
+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x
+    quotedMVar _             = Nothing
 
-elaboratedSystemFw_QuoteExp :: String -> Q LCTerm
-elaboratedSystemFw_QuoteExp str = do
-  e <- systemFw_QuoteExp str
-  case elaborate e of
-    Right e' -> pure e'
-    Left err -> fail err
+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x
+    quotedMTVar _              = Nothing
+
+    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x
+    quotedMKVar _              = Nothing
diff --git a/src/LambdaCube/SystemFw_/TypeChecker.hs b/src/LambdaCube/SystemFw_/TypeChecker.hs
--- a/src/LambdaCube/SystemFw_/TypeChecker.hs
+++ b/src/LambdaCube/SystemFw_/TypeChecker.hs
@@ -1,16 +1,8 @@
 module LambdaCube.SystemFw_.TypeChecker where
 
-import           Data.List                (uncons)
+import           Data.List                         (uncons)
 import           LambdaCube.SystemFw_.Ast
-
-substituteTypeInType :: Int -> LCType -> LCType -> LCType
-substituteTypeInType n v = go n
-  where
-    go _ LCBase        = LCBase
-    go m e@(LCTVar l)  = if m == l then v else e
-    go m (LCArr a b)   = go m a `LCArr` go m b
-    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b
-    go m (LCTTApp f a) = go m f `LCTTApp` go m a
+import           LambdaCube.SystemFw_.Substitution
 
 reduceType :: LCType -> LCType
 reduceType = go
@@ -26,41 +18,39 @@
       | otherwise
       = error "Did you really kind check this?"
 
-infer :: LCTerm -> Maybe LCType
+infer :: LCTerm -> LCType
 infer = go []
   where
-    go tl (LCVar n) = fmap fst . uncons $ drop n tl
+    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl
     go tl (LCLam t b)
-      | Just LCStar <- inferKind t
-      = LCArr v <$> go (v : tl) b
+      | LCStar <- inferKind t
+      = v `LCArr` go (v : tl) b
       | otherwise
-      = Nothing
+      = error "Function argument kind mismatch"
       where
         v = reduceType t
     go tl (LCApp f a)
-      | Just (LCArr at' rt) <- go tl f
-      , Just at <- go tl a
-      , at == at'
-      = Just rt
+      | LCArr at rt <- go tl f
+      , at == go tl a
+      = rt
       | otherwise
-      = Nothing
+      = error "Function argument type mismatch"
 
-inferKind :: LCType -> Maybe LCKind
+inferKind :: LCType -> LCKind
 inferKind = go []
   where
-    go _  LCBase = Just LCStar
-    go kl (LCTVar n) = fmap fst . uncons $ drop n kl
+    go _  LCBase = LCStar
+    go kl (LCTVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n kl
     go kl (LCArr a b)
-      | Just LCStar <- go kl a
-      , Just LCStar <- go kl b
-      = Just LCStar
+      | LCStar <- go kl a
+      , LCStar <- go kl b
+      = LCStar
       | otherwise
-      = Nothing
-    go kl (LCTTLam k b) = LCKArr k <$> go (k : kl) b
+      = error "Arrow kind mismatch"
+    go kl (LCTTLam k b) = k `LCKArr` go (k : kl) b
     go kl (LCTTApp f a)
-      | Just (LCKArr ak' rk) <- go kl f
-      , Just ak <- go kl a
-      , ak == ak'
-      = Just rk
+      | LCKArr ak rk <- go kl f
+      , ak == go kl a
+      = rk
       | otherwise
-      = Nothing
+      = error "Function argument kind mismatch"