diff --git a/hnix.cabal b/hnix.cabal
index 2202f8198..cbf8e4432 100644
--- a/hnix.cabal
+++ b/hnix.cabal
@@ -407,7 +407,7 @@ library
     , base >= 4.12 && < 5
     , base16-bytestring >= 0.1.1 && < 1.1
     , binary >= 0.8.5 && < 0.9
-    , bytestring >= 0.10.8 && < 0.11
+    , bytestring >= 0.10.8 && < 0.12
     , comonad >= 5.0.4 && < 5.1
     , containers >= 0.5.11.0 && < 0.7
     , data-fix >= 0.3.0 && < 0.4
diff --git a/src/Nix/Cited/Basic.hs b/src/Nix/Cited/Basic.hs
index 187b1e14f..35d6b485b 100644
--- a/src/Nix/Cited/Basic.hs
+++ b/src/Nix/Cited/Basic.hs
@@ -16,7 +16,6 @@ import           Prelude                 hiding ( force )
 import           Control.Comonad                ( Comonad )
 import           Control.Comonad.Env            ( ComonadEnv )
 import           Control.Monad.Catch     hiding ( catchJust )
-import           Data.Fix
 import           Nix.Cited
 import           Nix.Eval                      as Eval
 import           Nix.Exec
@@ -64,13 +63,12 @@ instance ( Has e Options
 
         -- Gather the current evaluation context at the time of thunk
         -- creation, and record it along with the thunk.
-        let go (fromException ->
-                    Just (EvaluatingExpr scope
-                              (Fix (Compose (Ann s e))))) =
-                let e' = Compose (Ann s (Nothing <$ e))
-                in [Provenance scope e']
-            go _ = mempty
-            ps = concatMap (go . frame) frames
+        let
+          go (fromException -> Just (EvaluatingExpr scope (AnnE s e))) =
+            let e' = Compose (Ann s (Nothing <$ e)) in
+            [Provenance scope e']
+          go _ = mempty
+          ps = concatMap (go . frame) frames
 
         Cited . NCited ps <$> thunk mv
       )
diff --git a/src/Nix/Eval.hs b/src/Nix/Eval.hs
index 876e2a90c..98e197098 100644
--- a/src/Nix/Eval.hs
+++ b/src/Nix/Eval.hs
@@ -15,7 +15,6 @@ module Nix.Eval where
 import           Control.Monad                  ( foldM )
 import           Control.Monad.Fix              ( MonadFix )
 import           Data.Semialign.Indexed         ( ialignWith )
-import           Data.Fix                       ( Fix(Fix) )
 import qualified Data.HashMap.Lazy             as M
 import           Data.List                      ( partition )
 import           Data.These                     ( These(..) )
@@ -496,7 +495,7 @@ buildArgument params arg =
 
 addSourcePositions
   :: (MonadReader e m, Has e SrcSpan) => Transform NExprLocF (m a)
-addSourcePositions f v@(Fix (Compose (Ann ann _))) =
+addSourcePositions f v@(AnnE ann _) =
   local (set hasLens ann) $ f v
 
 addStackFrames
diff --git a/src/Nix/Expr/Types.hs b/src/Nix/Expr/Types.hs
index 52864c506..0688822b5 100644
--- a/src/Nix/Expr/Types.hs
+++ b/src/Nix/Expr/Types.hs
@@ -108,6 +108,8 @@ data Params r
   --
   -- > Param "x"                                  ~  x
   | ParamSet !(ParamSet r) !Bool !(Maybe VarName)
+  --  2021-05-15: NOTE: Seems like we should flip the ParamSet, so partial application kicks in for Bool?
+  --  2021-05-15: NOTE: '...' variadic property probably needs a Bool synonym.
   -- ^ Explicit parameters (argument must be a set). Might specify a name to
   -- bind to the set in the function body. The bool indicates whether it is
   -- variadic or not.
@@ -432,6 +434,8 @@ data NExprF r
   -- > NBinary NPlus x y                           ~  x + y
   -- > NBinary NApp  f x                           ~  f x
   | NSelect !r !(NAttrPath r) !(Maybe r)
+  --  2021-05-15: NOTE: Default value should be first argument to leverage partial application.
+  -- Cascading change diff is not that big.
   -- ^ Dot-reference into an attribute set, optionally providing an
   -- alternative if the key doesn't exist.
   --
diff --git a/src/Nix/Expr/Types/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index e62ba6d3c..2704286e3 100644
--- a/src/Nix/Expr/Types/Annotated.hs
+++ b/src/Nix/Expr/Types/Annotated.hs
@@ -47,17 +47,30 @@ import           Text.Megaparsec.Pos            ( SourcePos(..) )
 import           Text.Read.Deriving
 import           Text.Show.Deriving
 
--- | A location in a source file
+-- * data type @SrcSpan@ - a zone in a source file
+
+-- | Demarcation of a chunk in a source file.
 data SrcSpan = SrcSpan
     { spanBegin :: SourcePos
     , spanEnd   :: SourcePos
     }
     deriving (Ord, Eq, Generic, Typeable, Data, Show, NFData, Hashable)
 
+-- ** Instances
+
+instance Semigroup SrcSpan where
+  s1 <> s2 = SrcSpan ((min `on` spanBegin) s1 s2) ((max `on` spanEnd) s1 s2)
+
+instance Binary SrcSpan
+instance ToJSON SrcSpan
+instance FromJSON SrcSpan
+
 #ifdef MIN_VERSION_serialise
 instance Serialise SrcSpan
 #endif
 
+-- * data type @Ann@
+
 -- | A type constructor applied to a type along with an annotation
 --
 -- Intended to be used with 'Fix':
@@ -69,14 +82,30 @@ data Ann ann a = Ann
     deriving (Ord, Eq, Data, Generic, Generic1, Typeable, Functor, Foldable,
               Traversable, Read, Show, NFData, Hashable)
 
-instance Hashable ann => Hashable1 (Ann ann)
+type AnnF ann f = Compose (Ann ann) f
 
-#ifdef MIN_VERSION_serialise
-instance (Serialise ann, Serialise a) => Serialise (Ann ann a)
-#endif
+-- | Pattern: @Fix (Compose (Ann _ _))@.
+-- Fix composes units of (annotations & the annotated) into one object.
+-- Giving annotated expression.
+pattern AnnE
+  :: forall ann (g :: * -> *)
+  . ann
+  -> g (Fix (Compose (Ann ann) g))
+  -> Fix (Compose (Ann ann) g)
+pattern AnnE ann a = Fix (Compose (Ann ann a))
+{-# complete AnnE #-}
+
+annToAnnF :: Ann ann (f (Fix (AnnF ann f))) -> Fix (AnnF ann f)
+annToAnnF (Ann ann a) = AnnE ann a
+
+-- ** Instances
+
+instance Hashable ann => Hashable1 (Ann ann)
 
 instance NFData ann => NFData1 (Ann ann)
 
+instance (Binary ann, Binary a) => Binary (Ann ann a)
+
 $(deriveEq1   ''Ann)
 $(deriveEq2   ''Ann)
 $(deriveOrd1  ''Ann)
@@ -88,40 +117,32 @@ $(deriveShow2 ''Ann)
 $(deriveJSON1 defaultOptions ''Ann)
 $(deriveJSON2 defaultOptions ''Ann)
 
-instance Semigroup SrcSpan where
-  s1 <> s2 = SrcSpan ((min `on` spanBegin) s1 s2) ((max `on` spanEnd) s1 s2)
+#ifdef MIN_VERSION_serialise
+instance (Serialise ann, Serialise a) => Serialise (Ann ann a)
+#endif
 
-type AnnF ann f = Compose (Ann ann) f
+#ifdef MIN_VERSION_serialise
+instance Serialise r => Serialise (Compose (Ann SrcSpan) NExprF r) where
+  encode (Compose (Ann ann a)) = encode ann <> encode a
+  decode = (Compose .) . Ann <$> decode <*> decode
+#endif
 
-annToAnnF :: Ann ann (f (Fix (AnnF ann f))) -> Fix (AnnF ann f)
-annToAnnF (Ann ann a) = AnnE ann a
+-- ** @NExprLoc{,F}@ - annotated Nix expression
 
 type NExprLocF = AnnF SrcSpan NExprF
 
--- | A nix expression with source location at each subexpression.
+instance Binary r => Binary (NExprLocF r)
+
+-- | Annotated Nix expression (each subexpression direct to its source location).
 type NExprLoc = Fix NExprLocF
 
 #ifdef MIN_VERSION_serialise
 instance Serialise NExprLoc
 #endif
 
-instance Binary SrcSpan
-instance (Binary ann, Binary a) => Binary (Ann ann a)
-instance Binary r => Binary (NExprLocF r)
 instance Binary NExprLoc
 
-instance ToJSON SrcSpan
-instance FromJSON SrcSpan
-
-#ifdef MIN_VERSION_serialise
-instance Serialise r => Serialise (Compose (Ann SrcSpan) NExprF r) where
-  encode (Compose (Ann ann a)) = encode ann <> encode a
-  decode = (Compose .) . Ann <$> decode <*> decode
-#endif
-
-pattern AnnE :: forall ann (g :: * -> *). ann
-             -> g (Fix (Compose (Ann ann) g)) -> Fix (Compose (Ann ann) g)
-pattern AnnE ann a = Fix (Compose (Ann ann a))
+-- * Other
 
 stripAnnotation :: Functor f => Fix (AnnF ann f) -> Fix f
 stripAnnotation = unfoldFix (annotated . getCompose . unFix)
@@ -131,33 +152,32 @@ stripAnn = annotated . getCompose
 
 nUnary :: Ann SrcSpan NUnaryOp -> NExprLoc -> NExprLoc
 nUnary (Ann s1 u) e1@(AnnE s2 _) = AnnE (s1 <> s2) $ NUnary u e1
-nUnary _          _              = error "nUnary: unexpected"
 {-# inline nUnary #-}
 
 nBinary :: Ann SrcSpan NBinaryOp -> NExprLoc -> NExprLoc -> NExprLoc
 nBinary (Ann s1 b) e1@(AnnE s2 _) e2@(AnnE s3 _) =
   AnnE (s1 <> s2 <> s3) $ NBinary b e1 e2
-nBinary _ _ _ = error "nBinary: unexpected"
 
 nSelectLoc
   :: NExprLoc -> Ann SrcSpan (NAttrPath NExprLoc) -> Maybe NExprLoc -> NExprLoc
-nSelectLoc e1@(AnnE s1 _) (Ann s2 ats) d = case d of
-  Nothing               -> AnnE (s1 <> s2) $ NSelect e1 ats Nothing
-  Just e2@(AnnE s3 _) -> AnnE (s1 <> s2 <> s3) $ NSelect e1 ats $ pure e2
-  _                     -> error "nSelectLoc: unexpected"
-nSelectLoc _ _ _ = error "nSelectLoc: unexpected"
+nSelectLoc e1@(AnnE s1 _) (Ann s2 ats) =
+  --  2021-05-16: NOTE: This could been rewritten into function application of @(s3, pure e2)@
+  -- if @SrcSpan@ was Monoid, which requires @SorcePos@ to be a Monoid, and upstream code prevents it.
+  -- Question upstream: https://github.com/mrkkrp/megaparsec/issues/450
+  maybe
+    (                    AnnE  s1s2        $ NSelect e1 ats   Nothing)
+    (\ e2@(AnnE s3 _) -> AnnE (s1s2 <> s3) $ NSelect e1 ats $ pure e2)
+ where
+  s1s2 = s1 <> s2
 
 nHasAttr :: NExprLoc -> Ann SrcSpan (NAttrPath NExprLoc) -> NExprLoc
 nHasAttr e1@(AnnE s1 _) (Ann s2 ats) = AnnE (s1 <> s2) $ NHasAttr e1 ats
-nHasAttr _              _            = error "nHasAttr: unexpected"
 
 nApp :: NExprLoc -> NExprLoc -> NExprLoc
 nApp e1@(AnnE s1 _) e2@(AnnE s2 _) = AnnE (s1 <> s2) $ NBinary NApp e1 e2
-nApp _              _              = error "nApp: unexpected"
 
 nAbs :: Ann SrcSpan (Params NExprLoc) -> NExprLoc -> NExprLoc
 nAbs (Ann s1 ps) e1@(AnnE s2 _) = AnnE (s1 <> s2) $ NAbs ps e1
-nAbs _           _              = error "nAbs: unexpected"
 
 nStr :: Ann SrcSpan (NString NExprLoc) -> NExprLoc
 nStr (Ann s1 s) = AnnE s1 $ NStr s
@@ -175,18 +195,15 @@ nullSpan = SrcSpan nullPos nullPos
 
 -- | Pattern systems for matching on NExprLocF constructions.
 
-pattern NSym_ :: SrcSpan -> VarName -> NExprLocF r
-pattern NSym_ ann x = Compose (Ann ann (NSym x))
-
-pattern NSynHole_ :: SrcSpan -> Text -> NExprLocF r
-pattern NSynHole_ ann x = Compose (Ann ann (NSynHole x))
-
 pattern NConstant_ :: SrcSpan -> NAtom -> NExprLocF r
 pattern NConstant_ ann x = Compose (Ann ann (NConstant x))
 
 pattern NStr_ :: SrcSpan -> NString r -> NExprLocF r
 pattern NStr_ ann x = Compose (Ann ann (NStr x))
 
+pattern NSym_ :: SrcSpan -> VarName -> NExprLocF r
+pattern NSym_ ann x = Compose (Ann ann (NSym x))
+
 pattern NList_ :: SrcSpan -> [r] -> NExprLocF r
 pattern NList_ ann x = Compose (Ann ann (NList x))
 
@@ -199,6 +216,12 @@ pattern NLiteralPath_ ann x = Compose (Ann ann (NLiteralPath x))
 pattern NEnvPath_ :: SrcSpan -> FilePath -> NExprLocF r
 pattern NEnvPath_ ann x = Compose (Ann ann (NEnvPath x))
 
+pattern NUnary_ :: SrcSpan -> NUnaryOp -> r -> NExprLocF r
+pattern NUnary_ ann op x = Compose (Ann ann (NUnary op x))
+
+pattern NBinary_ :: SrcSpan -> NBinaryOp -> r -> r -> NExprLocF r
+pattern NBinary_ ann op x y = Compose (Ann ann (NBinary op x y))
+
 pattern NSelect_ :: SrcSpan -> r -> NAttrPath r -> Maybe r -> NExprLocF r
 pattern NSelect_ ann x p v = Compose (Ann ann (NSelect x p v))
 
@@ -220,8 +243,6 @@ pattern NWith_ ann x y = Compose (Ann ann (NWith x y))
 pattern NAssert_ :: SrcSpan -> r -> r -> NExprLocF r
 pattern NAssert_ ann x y = Compose (Ann ann (NAssert x y))
 
-pattern NUnary_ :: SrcSpan -> NUnaryOp -> r -> NExprLocF r
-pattern NUnary_ ann op x = Compose (Ann ann (NUnary op x))
-
-pattern NBinary_ :: SrcSpan -> NBinaryOp -> r -> r -> NExprLocF r
-pattern NBinary_ ann op x y = Compose (Ann ann (NBinary op x y))
+pattern NSynHole_ :: SrcSpan -> Text -> NExprLocF r
+pattern NSynHole_ ann x = Compose (Ann ann (NSynHole x))
+{-# complete NConstant_, NStr_, NSym_, NList_, NSet_, NLiteralPath_, NEnvPath_, NUnary_, NBinary_, NSelect_, NHasAttr_, NAbs_, NLet_, NIf_, NWith_, NAssert_, NSynHole_ #-}
diff --git a/src/Nix/Parser.hs b/src/Nix/Parser.hs
index c94b820aa..0a820b853 100644
--- a/src/Nix/Parser.hs
+++ b/src/Nix/Parser.hs
@@ -49,9 +49,7 @@ import           Prelude                 hiding ( some
                                                 )
 import           Data.Foldable                  ( foldr1 )
 
-import           Control.Monad                  ( liftM2
-                                                , msum
-                                                )
+import           Control.Monad                  ( msum )
 import           Control.Monad.Combinators.Expr ( makeExprParser
                                                 , Operator( Postfix
                                                           , InfixN
@@ -91,6 +89,11 @@ import           Text.Megaparsec.Char           ( space1
                                                 )
 import qualified Text.Megaparsec.Char.Lexer    as Lexer
 
+-- | Different to @isAlphaNum@
+isAlphanumeric :: Char -> Bool
+isAlphanumeric x = isAlpha x || isDigit x
+{-# inline isAlphanumeric #-}
+
 infixl 3 <+>
 (<+>) :: MonadPlus m => m a -> m a -> m a
 (<+>) = mplus
@@ -100,11 +103,12 @@ infixl 3 <+>
 nixExpr :: Parser NExprLoc
 nixExpr =
   makeExprParser
-    nixTerm $ snd <<$>>
+    nixTerm $
+      snd <<$>>
         nixOperators nixSelector
 
 antiStart :: Parser Text
-antiStart = symbol "${" <?> show ("${" :: String)
+antiStart = symbol "${" <?> "${"
 
 nixAntiquoted :: Parser a -> Parser (Antiquoted a NExprLoc)
 nixAntiquoted p =
@@ -121,19 +125,20 @@ nixSelect :: Parser NExprLoc -> Parser NExprLoc
 nixSelect term =
   do
     res <-
-      build
-      <$> term
-      <*> optional
-        ( (,)
-        <$> (selDot *> nixSelector)
-        <*> optional (reserved "or" *> nixTerm)
+      liftA2 build
+        term
+        (optional $
+          liftA2 (,)
+            (selDot *> nixSelector)
+            (optional $ reserved "or" *> nixTerm)
         )
     continues <- optional $ lookAhead selDot
 
     maybe
-      (pure res)
-      (const $ nixSelect (pure res))
+      id
+      (const nixSelect)
       continues
+      (pure res)
  where
   build
     :: NExprLoc
@@ -143,9 +148,10 @@ nixSelect term =
     -> NExprLoc
   build t mexpr =
     maybe
-      t
-      (uncurry (nSelectLoc t))
+      id
+      (\ expr t -> (uncurry $ nSelectLoc t) expr)
       mexpr
+      t
 
 nixSelector :: Parser (Ann SrcSpan (NAttrPath NExprLoc))
 nixSelector =
@@ -217,7 +223,7 @@ nixList = annotateLocation1 (brackets (NList <$> many nixTerm) <?> "list")
 
 pathChar :: Char -> Bool
 pathChar x =
-  isAlpha x || isDigit x || (`elem` ("._-+~" :: String)) x
+  isAlphanumeric x || (`elem` ("._-+~" :: String)) x
 
 slash :: Parser Char
 slash =
@@ -238,10 +244,17 @@ nixSearchPath =
     )
 
 pathStr :: Parser FilePath
-pathStr = lexeme $ liftM2
-  (<>)
-  (many (satisfy pathChar))
-  (Prelude.concat <$> some (liftM2 (:) slash (some (satisfy pathChar))))
+pathStr =
+  lexeme $
+    liftA2 (<>)
+      (many $ satisfy pathChar)
+      (concat <$>
+        some
+          (liftA2 (:)
+            slash
+            (some $ satisfy pathChar)
+          )
+      )
 
 nixPath :: Parser NExprLoc
 nixPath = annotateLocation1 (try (mkPathF False <$> pathStr) <?> "path")
@@ -251,9 +264,9 @@ nixLet = annotateLocation1
   (reserved "let" *> (letBody <+> letBinders) <?> "let block")
  where
   letBinders =
-    NLet
-    <$> nixBinders
-    <*> (reserved "in" *> nixToplevelForm)
+    liftA2 NLet
+      nixBinders
+      (reserved "in" *> nixToplevelForm)
   -- Let expressions `let {..., body = ...}' are just desugared
   -- into `(rec {..., body = ...}).body'.
   letBody    = (\x -> NSelect x (StaticKey "body" :| mempty) Nothing) <$> aset
@@ -261,31 +274,34 @@ nixLet = annotateLocation1
 
 nixIf :: Parser NExprLoc
 nixIf = annotateLocation1
-  (NIf
-  <$> (reserved "if" *> nixExpr)
-  <*> (reserved "then" *> nixToplevelForm)
-  <*> (reserved "else" *> nixToplevelForm)
+  (liftA3 NIf
+    (reserved "if"   *> nixExpr        )
+    (reserved "then" *> nixToplevelForm)
+    (reserved "else" *> nixToplevelForm)
   <?> "if"
   )
 
 nixAssert :: Parser NExprLoc
 nixAssert = annotateLocation1
-  (NAssert
-  <$> (reserved "assert" *> nixToplevelForm)
-  <*> (semi *> nixToplevelForm)
+  (liftA2 NAssert
+    (reserved "assert" *> nixToplevelForm)
+    (semi              *> nixToplevelForm)
   <?> "assert"
   )
 
 nixWith :: Parser NExprLoc
 nixWith = annotateLocation1
-  (NWith
-  <$> (reserved "with" *> nixToplevelForm)
-  <*> (semi *> nixToplevelForm)
+  (liftA2 NWith
+    (reserved "with" *> nixToplevelForm)
+    (semi            *> nixToplevelForm)
   <?> "with"
   )
 
 nixLambda :: Parser NExprLoc
-nixLambda = nAbs <$> annotateLocation (try argExpr) <*> nixToplevelForm
+nixLambda =
+  liftA2 nAbs
+    (annotateLocation $ try argExpr)
+    nixToplevelForm
 
 nixString :: Parser NExprLoc
 nixString = nStr <$> annotateLocation nixString'
@@ -296,16 +312,14 @@ nixUri = lexeme $ annotateLocation1 $ try $ do
   protocol <- many $
     satisfy $
       \ x ->
-        isAlpha x
-        || isDigit x
+        isAlphanumeric x
         || (`elem` ("+-." :: String)) x
   _       <- string ":"
   address <-
     some $
       satisfy $
         \ x ->
-          isAlpha x
-          || isDigit x
+          isAlphanumeric x
           || (`elem` ("%/?:@&=+$,-_.!~*'" :: String)) x
   pure $ NStr $ DoubleQuoted
     [Plain $ toText $ start : protocol ++ ':' : address]
@@ -324,7 +338,7 @@ nixString' = lexeme (doubleQuoted <+> indented <?> "string")
       )
       <?> "double quoted string"
 
-  doubleQ      = void (char '"')
+  doubleQ      = void $ char '"'
   doubleEscape = Plain . singleton <$> (char '\\' *> escapeCode)
 
   indented :: Parser (NString NExprLoc)
@@ -392,21 +406,18 @@ argExpr =
     try $
       do
         name               <- identifier <* symbol "@"
-        (variadic, params) <- params
-        pure $ ParamSet params variadic (pure name)
+        (params, variadic) <- params
+        pure $ ParamSet params variadic $ pure name
 
   -- Parameters named by an identifier on the right, or none (`{x, y} @ args`)
   atRight =
     do
-      (variadic, params) <- params
+      (params, variadic) <- params
       name               <- optional $ symbol "@" *> identifier
       pure $ ParamSet params variadic name
 
   -- Return the parameters set.
-  params =
-    do
-      (args, dotdots) <- braces getParams
-      pure (dotdots, args)
+  params = braces getParams
 
   -- Collects the parameters within curly braces. Returns the parameters and
   -- a boolean indicating if the parameters are variadic.
@@ -417,17 +428,22 @@ argExpr =
     -- Otherwise, attempt to parse an argument, optionally with a
     -- default. If this fails, then return what has been accumulated
     -- so far.
-    go acc = ((acc, True) <$ symbol "...") <+> getMore acc
+    go acc = ((acc, True) <$ symbol "...") <+> getMore
+     where
+      getMore =
+        -- Could be nothing, in which just return what we have so far.
+        option (acc, False) $
+          do
+            -- Get an argument name and an optional default.
+            pair <-
+              liftA2 (,)
+                identifier
+                (optional $ question *> nixToplevelForm)
 
-    getMore acc =
-      -- Could be nothing, in which just return what we have so far.
-      option (acc, False) $
-        do
-          -- Get an argument name and an optional default.
-          pair <- liftM2 (,) identifier (optional $ question *> nixToplevelForm)
+            let args = acc <> [pair]
 
-          -- Either return this, or attempt to get a comma and restart.
-          option (acc <> [pair], False) $ comma *> go (acc <> [pair])
+            -- Either return this, or attempt to get a comma and restart.
+            option (args, False) $ comma *> go args
 
 nixBinders :: Parser [Binding NExprLoc]
 nixBinders = (inherit <+> namedVar) `endBy` semi where
@@ -438,17 +454,17 @@ nixBinders = (inherit <+> namedVar) `endBy` semi where
       try $ string "inherit" *> lookAhead (void (satisfy reservedEnd))
       p <- getSourcePos
       x <- whiteSpace *> optional scope
-      Inherit x
-        <$> many keyName
-        <*> pure p
+      liftA2 (Inherit x)
+        (many keyName)
+        (pure p)
         <?> "inherited binding"
   namedVar =
     do
       p <- getSourcePos
-      NamedVar
-        <$> (annotated <$> nixSelector)
-        <*> (equals *> nixToplevelForm)
-        <*> pure p
+      liftA3 NamedVar
+        (annotated <$> nixSelector)
+        (equals *> nixToplevelForm)
+        (pure p)
         <?> "variable binding"
   scope = nixParens <?> "inherit scope"
 
@@ -509,13 +525,13 @@ reserved n =
 identifier :: Parser Text
 identifier = lexeme $ try $ do
   ident <-
-    cons
-    <$> satisfy (\x -> isAlpha x || x == '_')
-    <*> takeWhileP mempty identLetter
-  guard (not (ident `HashSet.member` reservedNames))
+    liftA2 cons
+      (satisfy (\x -> isAlpha x || x == '_'))
+      (takeWhileP mempty identLetter)
+  guard $ not $ ident `HashSet.member` reservedNames
   pure ident
  where
-  identLetter x = isAlpha x || isDigit x || x == '_' || x == '\'' || x == '-'
+  identLetter x = isAlphanumeric x || x == '_' || x == '\'' || x == '-'
 
 -- We restrict the type of 'parens' and 'brackets' here because if they were to
 -- take a @Parser NExprLoc@ argument they would parse additional text which
@@ -584,8 +600,8 @@ data NAssoc = NAssocNone | NAssocLeft | NAssocRight
   deriving (Eq, Ord, Generic, Typeable, Data, Show, NFData)
 
 data NOperatorDef
-  = NUnaryDef Text NUnaryOp
-  | NBinaryDef Text NBinaryOp NAssoc
+  = NUnaryDef   Text NUnaryOp
+  | NBinaryDef  Text NBinaryOp  NAssoc
   | NSpecialDef Text NSpecialOp NAssoc
   deriving (Eq, Ord, Generic, Typeable, Data, Show, NFData)
 
@@ -623,20 +639,20 @@ opWithLoc name op f =
         {- dbg (toString name) $ -}
         operator name
 
-    pure $ f (Ann ann op)
+    pure $ f $ Ann ann op
 
 binaryN :: Text -> NBinaryOp -> (NOperatorDef, Operator (ParsecT Void Text (State SourcePos)) NExprLoc)
 binaryN name op =
-  (NBinaryDef name op NAssocNone, InfixN (opWithLoc name op nBinary))
+  (NBinaryDef name op NAssocNone, InfixN $ opWithLoc name op nBinary)
 binaryL :: Text -> NBinaryOp -> (NOperatorDef, Operator (ParsecT Void Text (State SourcePos)) NExprLoc)
 binaryL name op =
-  (NBinaryDef name op NAssocLeft, InfixL (opWithLoc name op nBinary))
+  (NBinaryDef name op NAssocLeft, InfixL $ opWithLoc name op nBinary)
 binaryR :: Text -> NBinaryOp -> (NOperatorDef, Operator (ParsecT Void Text (State SourcePos)) NExprLoc)
 binaryR name op =
-  (NBinaryDef name op NAssocRight, InfixR (opWithLoc name op nBinary))
+  (NBinaryDef name op NAssocRight, InfixR $ opWithLoc name op nBinary)
 prefix :: Text -> NUnaryOp -> (NOperatorDef, Operator (ParsecT Void Text (State SourcePos)) NExprLoc)
 prefix name op =
-  (NUnaryDef name op, Prefix (manyUnaryOp (opWithLoc name op nUnary)))
+  (NUnaryDef name op, Prefix $ manyUnaryOp $ opWithLoc name op nUnary)
 -- postfix name op = (NUnaryDef name op,
 --                    Postfix (opWithLoc name op nUnary))
 
@@ -717,7 +733,7 @@ getUnaryOperator = (m Map.!)
         zipWith
           buildEntry
           [1 ..]
-          (nixOperators (fail "unused"))
+          (nixOperators $ fail "unused")
 
   buildEntry i =
     concatMap $
@@ -734,7 +750,7 @@ getBinaryOperator = (m Map.!)
         zipWith
           buildEntry
           [1 ..]
-          (nixOperators (fail "unused"))
+          (nixOperators $ fail "unused")
 
   buildEntry i =
     concatMap $
@@ -752,7 +768,7 @@ getSpecialOperator o         = m Map.! o
         zipWith
           buildEntry
           [1 ..]
-          (nixOperators (fail "unused"))
+          (nixOperators $ fail "unused")
 
   buildEntry i =
     concatMap $
diff --git a/src/Nix/Reduce.hs b/src/Nix/Reduce.hs
index f4ff1849e..9f5d7a028 100644
--- a/src/Nix/Reduce.hs
+++ b/src/Nix/Reduce.hs
@@ -373,7 +373,7 @@ pruneTree opts =
         (reduceSets opts)  -- Reduce set members that aren't used; breaks if hasAttr is used
         binds
 
-    NLet binds (Just body@(Fix (Compose (Ann _ x)))) ->
+    NLet binds (Just body@(AnnE _ x)) ->
       pure $
         list
           x
@@ -384,8 +384,8 @@ pruneTree opts =
       pure $ NSelect aset (NE.map pruneKeyName attr) (join alt)
 
     -- These are the only short-circuiting binary operators
-    NBinary NAnd (Just (Fix (Compose (Ann _ larg)))) _ -> pure larg
-    NBinary NOr  (Just (Fix (Compose (Ann _ larg)))) _ -> pure larg
+    NBinary NAnd (Just (AnnE _ larg)) _ -> pure larg
+    NBinary NOr  (Just (AnnE _ larg)) _ -> pure larg
 
     -- If the function was never called, it means its argument was in a
     -- thunk that was forced elsewhere.
@@ -399,18 +399,18 @@ pruneTree opts =
     NBinary op (Just larg) Nothing -> pure $ NBinary op larg nNull
 
     -- If the scope of a with was never referenced, it's not needed
-    NWith Nothing (Just (Fix (Compose (Ann _ body)))) -> pure body
+    NWith Nothing (Just (AnnE _ body)) -> pure body
 
     NAssert Nothing _ ->
       fail "How can an assert be used, but its condition not?"
 
-    NAssert _ (Just (Fix (Compose (Ann _ body)))) -> pure body
+    NAssert _ (Just (AnnE _ body)) -> pure body
     NAssert (Just cond) _ -> pure $ NAssert cond nNull
 
     NIf Nothing _ _ -> fail "How can an if be used, but its condition not?"
 
-    NIf _ Nothing (Just (Fix (Compose (Ann _ f)))) -> pure f
-    NIf _ (Just (Fix (Compose (Ann _ t)))) Nothing -> pure t
+    NIf _ Nothing (Just (AnnE _ f)) -> pure f
+    NIf _ (Just (AnnE _ t)) Nothing -> pure t
 
     x                     -> sequence x
 
diff --git a/src/Nix/Render/Frame.hs b/src/Nix/Render/Frame.hs
index de15ebe6a..b3a70acee 100644
--- a/src/Nix/Render/Frame.hs
+++ b/src/Nix/Render/Frame.hs
@@ -72,7 +72,7 @@ framePos
   -> Maybe SourcePos
 framePos (NixFrame _ f)
   | Just (e :: EvalFrame m v) <- fromException f = case e of
-    EvaluatingExpr _ (Fix (Compose (Ann (SrcSpan beg _) _))) -> pure beg
+    EvaluatingExpr _ (AnnE (SrcSpan beg _) _) -> pure beg
     _ -> Nothing
   | otherwise = Nothing
 
@@ -108,7 +108,7 @@ renderEvalFrame level f =
   do
     opts :: Options <- asks (view hasLens)
     case f of
-      EvaluatingExpr scope e@(Fix (Compose (Ann ann _))) ->
+      EvaluatingExpr scope e@(AnnE ann _) ->
         do
           let
             scopeInfo =
@@ -121,7 +121,7 @@ renderEvalFrame level f =
             $ renderLocation ann =<<
                 renderExpr level "While evaluating" "Expression" e
 
-      ForcingExpr _scope e@(Fix (Compose (Ann ann _))) | thunks opts ->
+      ForcingExpr _scope e@(AnnE ann _) | thunks opts ->
         fmap
           (: mempty)
           $ renderLocation ann =<<
@@ -135,7 +135,7 @@ renderEvalFrame level f =
 
       SynHole synfo ->
         sequence $
-          let e@(Fix (Compose (Ann ann _))) = _synHoleInfo_expr synfo in
+          let e@(AnnE ann _) = _synHoleInfo_expr synfo in
 
           [ renderLocation ann =<<
               renderExpr level "While evaluating" "Syntactic Hole" e
@@ -152,7 +152,7 @@ renderExpr
   -> Text
   -> NExprLoc
   -> m (Doc ann)
-renderExpr _level longLabel shortLabel e@(Fix (Compose (Ann _ x))) = do
+renderExpr _level longLabel shortLabel e@(AnnE _ x) = do
   opts :: Options <- asks (view hasLens)
   let rendered
           | verbose opts >= DebugInfo =
diff --git a/src/Nix/Thunk/Basic.hs b/src/Nix/Thunk/Basic.hs
index aeff423dc..9832d2237 100644
--- a/src/Nix/Thunk/Basic.hs
+++ b/src/Nix/Thunk/Basic.hs
@@ -35,7 +35,8 @@ data Deferred m v = Computed v | Deferred (m v)
 
 -- ** Utils
 
--- | @Deferred (Computed|Deferred)@ analog of @either@.
+-- | Apply second if @Deferred@, otherwise (@Computed@) - apply first.
+-- Analog of @either@ for @Deferred = Computed|Deferred@.
 deferred :: (v -> b) -> (m v -> b) -> Deferred m v -> b
 deferred f1 f2 def =
   case def of
@@ -147,26 +148,30 @@ forceMain
   => NThunkF m v
   -> m v
 forceMain (Thunk n thunkRef thunkValRef) =
-  do
-    deferred
-      pure
-      (\ action ->
-        do
-          lockedIt <- lockThunk thunkRef
-          bool
-            (throwM $ ThunkLoop $ show n)
-            (do
-              v <- catch action $ \(e :: SomeException) ->
-                do
-                  _unlockedIt <- unlockThunk thunkRef
-                  throwM e
-              writeVar thunkValRef (Computed v)
-              _unlockedIt <- unlockThunk thunkRef
-              pure v
-            )
-            (not lockedIt)
-      )
-      =<< readVar thunkValRef
+  deferred
+    pure
+    (\ action ->
+      do
+        lockedIt <- lockThunk thunkRef
+        bool
+          lockFailed
+          (do
+            v <- action `catch` actionFailed
+            writeVar thunkValRef (Computed v)
+            _unlockedIt <- unlockThunk thunkRef
+            pure v
+          )
+          (not lockedIt)
+    )
+    =<< readVar thunkValRef
+ where
+  lockFailed = throwM $ ThunkLoop $ show n
+
+  actionFailed (e :: SomeException) =
+    do
+      _unlockedIt <- unlockThunk thunkRef
+      throwM e
+
 {-# inline forceMain #-} -- it is big function, but internal, and look at its use.
 
 
diff --git a/src/Nix/Type/Assumption.hs b/src/Nix/Type/Assumption.hs
index cce0fb3a1..48ded5280 100644
--- a/src/Nix/Type/Assumption.hs
+++ b/src/Nix/Type/Assumption.hs
@@ -1,3 +1,5 @@
+-- | Basing on the Nix (Hindley–Milner) type system (that provides decidable type inference):
+-- gathering assumptions (inference evidence) about polymorphic types.
 module Nix.Type.Assumption
   ( Assumption(..)
   , empty
@@ -24,16 +26,27 @@ empty :: Assumption
 empty = Assumption mempty
 
 extend :: Assumption -> (Name, Type) -> Assumption
-extend (Assumption a) (x, s) = Assumption ((x, s) : a)
+extend (Assumption a) (x, s) =
+  Assumption $
+    (x, s) : a
 
 remove :: Assumption -> Name -> Assumption
-remove (Assumption a) var = Assumption (filter (\(n, _) -> n /= var) a)
+remove (Assumption a) var =
+  Assumption $
+    filter
+      (\(n, _) -> n /= var)
+      a
 
 lookup :: Name -> Assumption -> [Type]
-lookup key (Assumption a) = fmap snd (filter (\(n, _) -> n == key) a)
+lookup key (Assumption a) =
+  snd <$>
+    filter
+      (\(n, _) -> n == key)
+      a
 
 merge :: Assumption -> Assumption -> Assumption
-merge (Assumption a) (Assumption b) = Assumption (a <> b)
+merge (Assumption a) (Assumption b) =
+  Assumption $ a <> b
 
 mergeAssumptions :: [Assumption] -> Assumption
 mergeAssumptions = foldl' merge empty
@@ -42,4 +55,4 @@ singleton :: Name -> Type -> Assumption
 singleton x y = Assumption [(x, y)]
 
 keys :: Assumption -> [Name]
-keys (Assumption a) = fmap fst a
+keys (Assumption a) = fst <$> a
diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs
index 7bad7652d..9b08df8fa 100644
--- a/src/Nix/Type/Infer.hs
+++ b/src/Nix/Type/Infer.hs
@@ -30,17 +30,17 @@ where
 import           Control.Monad.Catch            ( MonadThrow(..)
                                                 , MonadCatch(..)
                                                 )
-import           Control.Monad.Except           ( MonadError(..)
-                                                )
+import           Control.Monad.Except           ( MonadError(..) )
 import           Prelude                 hiding ( Type
                                                 , TVar
                                                 , Constraint
                                                 )
 import           Nix.Utils
 import           Control.Monad.Logic     hiding ( fail )
-import           Control.Monad.Reader           ( MonadFix
+import           Control.Monad.Reader           ( MonadFix )
+import           Control.Monad.Ref              ( MonadAtomicRef(..)
+                                                , MonadRef(..)
                                                 )
-import           Control.Monad.Ref
 import           Control.Monad.ST               ( ST
                                                 , runST
                                                 )
@@ -65,7 +65,7 @@ import           Nix.Expr.Types.Annotated
 import           Nix.Fresh
 import           Nix.String
 import           Nix.Scope
-import qualified Nix.Type.Assumption           as As
+import qualified Nix.Type.Assumption           as Assumption
 import           Nix.Type.Env            hiding ( empty )
 import qualified Nix.Type.Env                  as Env
 import           Nix.Type.Type
@@ -73,120 +73,50 @@ import           Nix.Value.Monad
 import           Nix.Var
 
 
--- * Classes
-
--- | Inference monad
-newtype InferT s m a =
-  InferT
-    { getInfer ::
-        ReaderT
-          (Set.Set TVar, Scopes (InferT s m) (Judgment s))
-          (StateT InferState (ExceptT InferError m))
-          a
-    }
-    deriving
-      ( Functor
-      , Applicative
-      , Alternative
-      , Monad
-      , MonadPlus
-      , MonadFix
-      , MonadReader (Set.Set TVar, Scopes (InferT s m) (Judgment s))
-      , MonadFail
-      , MonadState InferState
-      , MonadError InferError
-      )
-
-instance MonadTrans (InferT s) where
-  lift = InferT . lift . lift . lift
-
--- instance MonadThunkId m => MonadThunkId (InferT s m) where
---   type ThunkId (InferT s m) = ThunkId m
-
--- | Inference state
-newtype InferState = InferState { count :: Int }
-
--- | Initial inference state
-initInfer :: InferState
-initInfer = InferState { count = 0 }
-
-data Constraint
-  = EqConst Type Type
-  | ExpInstConst Type Scheme
-  | ImpInstConst Type (Set.Set TVar) Type
-  deriving (Show, Eq, Ord)
-
-newtype Subst = Subst (Map TVar Type)
-  deriving (Eq, Ord, Show, Semigroup, Monoid)
-
-class Substitutable a where
-  apply :: Subst -> a -> a
-
-instance Substitutable TVar where
-  apply (Subst s) a = tv
-   where
-    t         = TVar a
-    (TVar tv) = Map.findWithDefault t a s
-
-instance Substitutable Type where
-  apply _         (  TCon a   ) = TCon a
-  apply s         (  TSet b a ) = TSet b (M.map (apply s) a)
-  apply s         (  TList a  ) = TList (apply s <$> a)
-  apply (Subst s) t@(TVar  a  ) = Map.findWithDefault t a s
-  apply s         (  t1 :~> t2) = apply s t1 :~> apply s t2
-  apply s         (  TMany ts ) = TMany (apply s <$> ts)
-
-instance Substitutable Scheme where
-  apply (Subst s) (Forall as t) = Forall as $ apply s' t
-    where s' = Subst $ foldr Map.delete s as
-
-instance Substitutable Constraint where
-  apply s (EqConst      t1 t2) = EqConst (apply s t1) (apply s t2)
-  apply s (ExpInstConst t  sc) = ExpInstConst (apply s t) (apply s sc)
-  apply s (ImpInstConst t1 ms t2) =
-    ImpInstConst (apply s t1) (apply s ms) (apply s t2)
-
-instance Substitutable a => Substitutable [a] where
-  apply = fmap . apply
-
-instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
-  apply = Set.map . apply
-
-
-class FreeTypeVars a where
-  ftv :: a -> Set.Set TVar
-
-instance FreeTypeVars Type where
-  ftv TCon{}      = mempty
-  ftv (TVar a   ) = Set.singleton a
-  ftv (TSet _ a ) = Set.unions (ftv <$> M.elems a)
-  ftv (TList a  ) = Set.unions (ftv <$> a)
-  ftv (t1 :~> t2) = ftv t1 `Set.union` ftv t2
-  ftv (TMany ts ) = Set.unions (ftv <$> ts)
-
-instance FreeTypeVars TVar where
-  ftv = Set.singleton
-
-instance FreeTypeVars Scheme where
-  ftv (Forall as t) = ftv t `Set.difference` Set.fromList as
+normalizeScheme :: Scheme -> Scheme
+normalizeScheme (Forall _ body) = Forall (snd <$> ord) (normtype body)
+ where
+  ord =
+    zip
+      (ordNub $ fv body)
+      (TV . toText <$> letters)
 
-instance FreeTypeVars a => FreeTypeVars [a] where
-  ftv = foldr (Set.union . ftv) mempty
+  fv (TVar a  ) = [a]
+  fv (a :~> b ) = fv a <> fv b
+  fv (TCon _  ) = mempty
+  fv (TSet _ a) = concatMap fv $ M.elems a
+  fv (TList a ) = concatMap fv a
+  fv (TMany ts) = concatMap fv ts
 
-instance (Ord a, FreeTypeVars a) => FreeTypeVars (Set.Set a) where
-  ftv = foldr (Set.union . ftv) mempty
+  normtype (a :~> b ) = normtype a :~> normtype b
+  normtype (TCon a  ) = TCon a
+  normtype (TSet b a) = TSet b $ normtype `M.map` a
+  normtype (TList a ) = TList $ normtype <$> a
+  normtype (TMany ts) = TMany $ normtype <$> ts
+  normtype (TVar  a ) =
+    maybe
+      (error "type variable not in signature")
+      TVar
+      (List.lookup a ord)
 
+generalize :: Set.Set TVar -> Type -> Scheme
+generalize free t = Forall as t
+ where
+  as = Set.toList $ free `Set.difference` ftv t
 
-class ActiveTypeVars a where
-  atv :: a -> Set.Set TVar
+-- | Canonicalize and return the polymorphic toplevel type.
+closeOver :: Type -> Scheme
+closeOver = normalizeScheme . generalize mempty
 
-instance ActiveTypeVars Constraint where
-  atv (EqConst      t1 t2   ) = ftv t1 `Set.union` ftv t2
-  atv (ImpInstConst t1 ms t2) = ftv t1 `Set.union` (ftv ms `Set.intersection` ftv t2)
-  atv (ExpInstConst t  s     ) = ftv t  `Set.union` ftv s
+-- | Check if all elements are of the same type.
+allSameType :: [Type] -> Bool
+allSameType = allSame
+ where
+  allSame :: Eq a => [a] -> Bool
+  allSame [] = True
+  allSame (x:xs) = all (x ==) xs
 
-instance ActiveTypeVars a => ActiveTypeVars [a] where
-  atv = foldr (Set.union . atv) mempty
+-- * data type @TypeError@
 
 data TypeError
   = UnificationFail Type Type
@@ -196,6 +126,8 @@ data TypeError
   | UnificationMismatch [Type] [Type]
   deriving (Eq, Show, Ord)
 
+-- * @InferError@
+
 data InferError
   = TypeInferenceErrors [TypeError]
   | TypeInferenceAborted
@@ -204,6 +136,8 @@ data InferError
 typeError :: MonadError InferError m => TypeError -> m ()
 typeError err = throwError $ TypeInferenceErrors [err]
 
+-- ** Instances
+
 deriving instance Show InferError
 instance Exception InferError
 
@@ -214,59 +148,14 @@ instance Monoid InferError where
   mempty  = TypeInferenceAborted
   mappend = (<>)
 
+-- * @InferState@: inference state
 
--- * Inference
-
--- | Run the inference monad
-runInfer' :: MonadInfer m => InferT s m a -> m (Either InferError a)
-runInfer' =
-  runExceptT
-    . (`evalStateT` initInfer)
-    . (`runReaderT` (mempty, emptyScopes))
-    . getInfer
-
-runInfer :: (forall s . InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
-runInfer m = runST $ do
-  i <- newVar (1 :: Int)
-  runFreshIdT i (runInfer' m)
-
-inferType
-  :: forall s m . MonadInfer m => Env -> NExpr -> InferT s m [(Subst, Type)]
-inferType env ex = do
-  Judgment as cs t <- infer ex
-  let unbounds =
-        Set.fromList (As.keys as) `Set.difference` Set.fromList (Env.keys env)
-  unless (Set.null unbounds) $ typeError $ UnboundVariables
-    (ordNub (Set.toList unbounds))
-  let
-    cs' =
-      [ ExpInstConst t s
-          | (x, ss) <- Env.toList env
-          , s       <- ss
-          , t       <- As.lookup x as
-      ]
-  inferState <- get
-  let
-    eres = (`evalState` inferState) $ runSolver $
-      do
-        subst <- solve (cs <> cs')
-        pure (subst, subst `apply` t)
-  either
-    (throwError . TypeInferenceErrors)
-    pure
-    eres
-
--- | Solve for the toplevel type of an expression in a given environment
-inferExpr :: Env -> NExpr -> Either InferError [Scheme]
-inferExpr env ex =
-  (\ (subst, ty) -> closeOver $ subst `apply` ty) <<$>> runInfer (inferType env ex)
-
--- | Canonicalize and return the polymorphic toplevel type.
-closeOver :: Type -> Scheme
-closeOver = normalizeScheme . generalize mempty
+-- | Inference state
+newtype InferState = InferState { count :: Int }
 
-extendMSet :: Monad m => TVar -> InferT s m a -> InferT s m a
-extendMSet x = InferT . local (first (Set.insert x)) . getInfer
+-- | Initial inference state
+initInfer :: InferState
+initInfer = InferState { count = 0 }
 
 letters :: [String]
 letters =
@@ -281,7 +170,7 @@ freshTVar =
   do
     s <- get
     put s { count = count s + 1 }
-    pure $ TV (toText (letters !! count s))
+    pure $ TV $ toText $ letters !! count s
 
 fresh :: MonadState InferState m => m Type
 fresh = TVar <$> freshTVar
@@ -293,79 +182,116 @@ instantiate (Forall as t) =
     let s = Subst $ Map.fromList $ zip as as'
     pure $ apply s t
 
-generalize :: Set.Set TVar -> Type -> Scheme
-generalize free t = Forall as t
- where
-  as = Set.toList $ ftv t `Set.difference` free
+-- * @Constraint@ data type
 
-unops :: Type -> NUnaryOp -> [Constraint]
-unops u1 op =
-  [ EqConst u1
-   (case op of
-      NNot -> typeFun [typeBool                   , typeBool                       ]
-      NNeg -> TMany   [typeFun  [typeInt, typeInt], typeFun  [typeFloat, typeFloat]]
-    )
-  ]
+data Constraint
+  = EqConst Type Type
+  | ExpInstConst Type Scheme
+  | ImpInstConst Type (Set.Set TVar) Type
+  deriving (Show, Eq, Ord)
 
-binops :: Type -> NBinaryOp -> [Constraint]
-binops u1 op =
-  if
-    -- NApp in fact is handled separately
-    -- Equality tells nothing about the types, because any two types are allowed.
-    | op `elem` [ NApp  , NEq  , NNEq        ] -> mempty
-    | op `elem` [ NGt   , NGte , NLt  , NLte ] -> inequality
-    | op `elem` [ NAnd  , NOr  , NImpl       ] -> gate
-    | op ==       NConcat                      -> concatenation
-    | op `elem` [ NMinus, NMult, NDiv        ] -> arithmetic
-    | op ==       NUpdate                      -> rUnion
-    | op ==       NPlus                        -> addition
-    | otherwise -> fail "GHC so far can not infer that this pattern match is full, so make it happy."
+-- * @Subst@ data type
 
- where
+-- | Substitution of the basic type definition by a type variable.
+newtype Subst = Subst (Map TVar Type)
+  deriving (Eq, Ord, Show, Semigroup, Monoid)
 
-  gate          = eqCnst [typeBool, typeBool, typeBool]
-  concatenation = eqCnst [typeList, typeList, typeList]
+-- | Compose substitutions
+compose :: Subst -> Subst -> Subst
+Subst s1 `compose` Subst s2 =
+  Subst $
+    apply (Subst s1) `Map.map`
+      (s2 `Map.union` s1)
 
-  eqCnst l = [EqConst u1 (typeFun l)]
+-- * class @Substitutable@
 
-  inequality =
-    eqCnstMtx
-      [ [typeInt  , typeInt  , typeBool]
-      , [typeFloat, typeFloat, typeBool]
-      , [typeInt  , typeFloat, typeBool]
-      , [typeFloat, typeInt  , typeBool]
-      ]
+class Substitutable a where
+  apply :: Subst -> a -> a
 
-  arithmetic =
-    eqCnstMtx
-      [ [typeInt  , typeInt  , typeInt  ]
-      , [typeFloat, typeFloat, typeFloat]
-      , [typeInt  , typeFloat, typeFloat]
-      , [typeFloat, typeInt  , typeFloat]
-      ]
+-- ** Instances
 
-  rUnion =
-    eqCnstMtx
-      [ [typeSet , typeSet , typeSet]
-      , [typeSet , typeNull, typeSet]
-      , [typeNull, typeSet , typeSet]
-      ]
+instance Substitutable TVar where
+  apply (Subst s) a = tv
+   where
+    t         = TVar a
+    (TVar tv) = Map.findWithDefault t a s
 
-  addition =
-    eqCnstMtx
-      [ [typeInt   , typeInt   , typeInt   ]
-      , [typeFloat , typeFloat , typeFloat ]
-      , [typeInt   , typeFloat , typeFloat ]
-      , [typeFloat , typeInt   , typeFloat ]
-      , [typeString, typeString, typeString]
-      , [typePath  , typePath  , typePath  ]
-      , [typeString, typeString, typePath  ]
-      ]
+instance Substitutable Type where
+  apply _         (  TCon a   ) = TCon a
+  apply s         (  TSet b a ) = TSet b $ apply s `M.map` a
+  apply s         (  TList a  ) = TList $ apply s <$> a
+  apply (Subst s) t@(TVar  a  ) = Map.findWithDefault t a s
+  apply s         (  t1 :~> t2) = apply s t1 :~> apply s t2
+  apply s         (  TMany ts ) = TMany $ apply s <$> ts
 
-  eqCnstMtx mtx = [EqConst u1 (TMany (typeFun <$> mtx))]
+instance Substitutable Scheme where
+  apply (Subst s) (Forall as t) = Forall as $ apply s' t
+   where
+    s' = Subst $ foldr Map.delete s as
 
-liftInfer :: Monad m => m a -> InferT s m a
-liftInfer = InferT . lift . lift . lift
+instance Substitutable Constraint where
+  apply s (EqConst      t1 t2) =
+    EqConst
+      (apply s t1)
+      (apply s t2)
+  apply s (ExpInstConst t  sc) =
+    ExpInstConst
+      (apply s t)
+      (apply s sc)
+  apply s (ImpInstConst t1 ms t2) =
+    ImpInstConst
+      (apply s t1)
+      (apply s ms)
+      (apply s t2)
+
+instance Substitutable a => Substitutable [a] where
+  apply = fmap . apply
+
+instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
+  apply = Set.map . apply
+
+
+-- * data type @Judgement@
+
+data Judgment s =
+  Judgment
+    { assumptions     :: Assumption.Assumption
+    , typeConstraints :: [Constraint]
+    , inferredType    :: Type
+    }
+    deriving Show
+
+-- * @InferT@: inference monad
+
+-- | Inference monad
+newtype InferT s m a =
+  InferT
+    { getInfer ::
+        ReaderT
+          (Set.Set TVar, Scopes (InferT s m) (Judgment s))
+          (StateT InferState (ExceptT InferError m))
+          a
+    }
+    deriving
+      ( Functor
+      , Applicative
+      , Alternative
+      , Monad
+      , MonadPlus
+      , MonadFix
+      , MonadReader (Set.Set TVar, Scopes (InferT s m) (Judgment s))
+      , MonadFail
+      , MonadState InferState
+      , MonadError InferError
+      )
+
+extendMSet :: Monad m => TVar -> InferT s m a -> InferT s m a
+extendMSet x = InferT . local (first $ Set.insert x) . getInfer
+
+-- ** Instances
+
+instance MonadTrans (InferT s) where
+  lift = InferT . lift . lift . lift
 
 instance MonadRef m => MonadRef (InferT s m) where
   type Ref (InferT s m) = Ref m
@@ -378,11 +304,9 @@ instance MonadAtomicRef m => MonadAtomicRef (InferT s m) where
     liftInfer $
       do
         res <- snd . f <$> readRef x
-        _   <- modifyRef x (fst . f)
+        _   <- modifyRef x $ fst . f
         pure res
 
--- newtype JThunkT s m = JThunk (NThunkF (InferT s m) (Judgment s))
-
 instance Monad m => MonadThrow (InferT s m) where
   throwM = throwError . EvaluationError
 
@@ -394,12 +318,76 @@ instance Monad m => MonadCatch (InferT s m) where
           maybe
             (error $ "Exception was not an exception: " <> show e)
             h
-            (fromException (toException e))
+            (fromException $ toException e)
         err -> error $ "Unexpected error: " <> show err
 
-type MonadInfer m
-  = ({- MonadThunkId m,-}
-     MonadVar m, MonadFix m)
+-- instance MonadThunkId m => MonadThunkId (InferT s m) where
+--   type ThunkId (InferT s m) = ThunkId m
+
+instance
+  Monad m
+  => FromValue NixString (InferT s m) (Judgment s)
+ where
+  fromValueMay _ = stub
+  fromValue _ = error "Unused"
+
+instance
+  MonadInfer m
+  => FromValue ( AttrSet (Judgment s)
+              , AttrSet SourcePos
+              ) (InferT s m) (Judgment s)
+ where
+  fromValueMay (Judgment _ _ (TSet _ xs)) =
+    do
+      let sing _ = Judgment Assumption.empty mempty
+      pure $ pure (M.mapWithKey sing xs, mempty)
+  fromValueMay _ = stub
+  fromValue =
+    pure .
+      fromMaybe
+      (mempty, mempty)
+      <=< fromValueMay
+
+instance MonadInfer m
+  => ToValue (AttrSet (Judgment s), AttrSet SourcePos)
+            (InferT s m) (Judgment s) where
+  toValue (xs, _) =
+    liftA3
+      Judgment
+      (foldrM go Assumption.empty xs)
+      (concat <$> traverse ((typeConstraints <$>) . demand) xs)
+      (TSet True <$> traverse ((inferredType <$>) . demand) xs)
+   where
+    go x rest =
+      do
+        x' <- demand x
+        pure $ Assumption.merge (assumptions x') rest
+
+instance MonadInfer m => ToValue [Judgment s] (InferT s m) (Judgment s) where
+  toValue xs =
+    liftA3
+      Judgment
+      (foldrM go Assumption.empty xs)
+      (concat <$> traverse ((typeConstraints <$>) . demand) xs)
+      (TList <$> traverse ((inferredType <$>) . demand) xs)
+   where
+    go x rest =
+      do
+        x' <- demand x
+        pure $ Assumption.merge (assumptions x') rest
+
+instance MonadInfer m => ToValue Bool (InferT s m) (Judgment s) where
+  toValue _ = pure $ Judgment Assumption.empty mempty typeBool
+
+instance
+  Monad m
+  => Scoped (Judgment s) (InferT s m) where
+  currentScopes = currentScopesReader
+  clearScopes   = clearScopesReader @(InferT s m) @(Judgment s)
+  pushScopes    = pushScopesReader
+  lookupVar     = lookupVarReader
+
+-- newtype JThunkT s m = JThunk (NThunkF (InferT s m) (Judgment s))
 
 --  2021-02-22: NOTE: Seems like suporflous instance
 instance Monad m => MonadValue (Judgment s) (InferT s m) where
@@ -450,32 +438,42 @@ instance MonadInfer m
   -- If we have a thunk loop, we just don't know the type.
   force (JThunk t) = catch (force t)
     $ \(_ :: ThunkLoop) ->
-                           f =<< Judgment As.empty mempty <$> fresh
+                           f =<< Judgment Assumption.empty mempty <$> fresh
 
   -- If we have a thunk loop, we just don't know the type.
   forceEff (JThunk t) = catch (forceEff t)
     $ \(_ :: ThunkLoop) ->
-                           f =<< Judgment As.empty mempty <$> fresh
+                           f =<< Judgment Assumption.empty mempty <$> fresh
 -}
 
 instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
   freeVariable var = do
     tv <- fresh
-    pure $ Judgment (As.singleton var tv) mempty tv
+    pure $ Judgment (Assumption.singleton var tv) mempty tv
 
   synHole var = do
     tv <- fresh
-    pure $ Judgment (As.singleton var tv) mempty tv
+    pure $ Judgment (Assumption.singleton var tv) mempty tv
 
--- If we fail to look up an attribute, we just don't know the type.
-  attrMissing _ _ = Judgment As.empty mempty <$> fresh
+  -- If we fail to look up an attribute, we just don't know the type.
+  attrMissing _ _ = Judgment Assumption.empty mempty <$> fresh
 
   evaledSym _ = pure
 
-  evalCurPos = pure $ Judgment As.empty mempty $ TSet False $ M.fromList
-    [("file", typePath), ("line", typeInt), ("col", typeInt)]
-
-  evalConstant c = pure $ Judgment As.empty mempty (go c)
+  evalCurPos =
+    pure $
+      Judgment
+        Assumption.empty
+        mempty
+        (TSet False $
+          M.fromList
+            [ ("file", typePath)
+            , ("line", typeInt )
+            , ("col" , typeInt )
+            ]
+        )
+
+  evalConstant c = pure $ Judgment Assumption.empty mempty $ go c
    where
     go = \case
       NURI   _ -> typeString
@@ -484,20 +482,31 @@ instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
       NBool  _ -> typeBool
       NNull    -> typeNull
 
-  evalString      = const $ pure $ Judgment As.empty mempty typeString
-  evalLiteralPath = const $ pure $ Judgment As.empty mempty typePath
-  evalEnvPath     = const $ pure $ Judgment As.empty mempty typePath
+  evalString      = const $ pure $ Judgment Assumption.empty mempty typeString
+  evalLiteralPath = const $ pure $ Judgment Assumption.empty mempty typePath
+  evalEnvPath     = const $ pure $ Judgment Assumption.empty mempty typePath
 
   evalUnary op (Judgment as1 cs1 t1) = do
     tv <- fresh
-    pure $ Judgment as1 (cs1 <> unops (t1 :~> tv) op) tv
+    pure $
+      Judgment
+        as1
+        (cs1 <> unops (t1 :~> tv) op)
+        tv
 
   evalBinary op (Judgment as1 cs1 t1) e2 = do
     Judgment as2 cs2 t2 <- e2
     tv                  <- fresh
-    pure $ Judgment (as1 `As.merge` as2)
-                      (cs1 <> cs2 <> binops (t1 :~> t2 :~> tv) op)
-                      tv
+    pure $
+      Judgment
+        (as1 `Assumption.merge` as2)
+        ( cs1 <>
+          cs2 <>
+          binops
+            (t1 :~> t2 :~> tv)
+            op
+        )
+        tv
 
   evalWith = Eval.evalWithAttrSet
 
@@ -505,31 +514,47 @@ instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
     Judgment as2 cs2 t2 <- t
     Judgment as3 cs3 t3 <- f
     pure $ Judgment
-      (as1 `As.merge` as2 `As.merge` as3)
+      (as1 `Assumption.merge` as2 `Assumption.merge` as3)
       (cs1 <> cs2 <> cs3 <> [EqConst t1 typeBool, EqConst t2 t3])
       t2
 
   evalAssert (Judgment as1 cs1 t1) body = do
     Judgment as2 cs2 t2 <- body
-    pure
-      $ Judgment (as1 `As.merge` as2) (cs1 <> cs2 <> [EqConst t1 typeBool]) t2
+    pure $
+      Judgment
+        (as1 `Assumption.merge` as2)
+        (cs1 <> cs2 <> [EqConst t1 typeBool])
+        t2
 
   evalApp (Judgment as1 cs1 t1) e2 = do
     Judgment as2 cs2 t2 <- e2
     tv                  <- fresh
-    pure $ Judgment (as1 `As.merge` as2)
-                      (cs1 <> cs2 <> [EqConst t1 (t2 :~> tv)])
-                      tv
+    pure $
+      Judgment
+        (as1 `Assumption.merge` as2)
+        (cs1 <> cs2 <> [EqConst t1 (t2 :~> tv)])
+        tv
 
   evalAbs (Param x) k = do
     a <- freshTVar
     let tv = TVar a
-    ((), Judgment as cs t) <- extendMSet
-      a
-      (k (pure (Judgment (As.singleton x tv) mempty tv)) (\_ b -> ((), ) <$> b))
-    pure $ Judgment (as `As.remove` x)
-                      (cs <> [ EqConst t' tv | t' <- As.lookup x as ])
-                      (tv :~> t)
+    ((), Judgment as cs t) <-
+      extendMSet
+        a
+        (k
+          (pure $
+             Judgment
+               (Assumption.singleton x tv)
+               mempty
+               tv
+          )
+          (\_ b -> ((), ) <$> b)
+        )
+    pure $
+      Judgment
+        (as `Assumption.remove` x)
+        (cs <> [ EqConst t' tv | t' <- Assumption.lookup x as ])
+        (tv :~> t)
 
   evalAbs (ParamSet ps variadic _mname) k = do
     js <-
@@ -544,9 +569,9 @@ instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
 
     let
       (env, tys) =
-        (\f -> foldl' f (As.empty, mempty) js) $ \(as1, t1) (k, t) ->
-          (as1 `As.merge` As.singleton k t, M.insert k t t1)
-      arg   = pure $ Judgment env mempty (TSet True tys)
+        (\f -> foldl' f (Assumption.empty, mempty) js) $ \(as1, t1) (k, t) ->
+          (as1 `Assumption.merge` Assumption.singleton k t, M.insert k t t1)
+      arg   = pure $ Judgment env mempty $ TSet True tys
       call  = k arg $ \args b -> (args, ) <$> b
       names = fst <$> js
 
@@ -556,74 +581,186 @@ instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
 
     pure $
       Judgment
-        (foldl' As.remove as names)
-        (cs <> [ EqConst t' (tys M.! x) | x <- names, t' <- As.lookup x as ])
+        (foldl' Assumption.remove as names)
+        (cs <> [ EqConst t' (tys M.! x) | x <- names, t' <- Assumption.lookup x as ])
         (ty :~> t)
 
   evalError = throwError . EvaluationError
 
-data Judgment s =
-  Judgment
-    { assumptions     :: As.Assumption
-    , typeConstraints :: [Constraint]
-    , inferredType    :: Type
-    }
-    deriving Show
+-- * class @FreeTypeVars@
 
-instance
-  Monad m
-  => FromValue NixString (InferT s m) (Judgment s)
- where
-  fromValueMay _ = stub
-  fromValue _ = error "Unused"
+class FreeTypeVars a where
+  ftv :: a -> Set.Set TVar
 
-instance
-  MonadInfer m
-  => FromValue ( AttrSet (Judgment s)
-              , AttrSet SourcePos
-              ) (InferT s m) (Judgment s)
- where
-  fromValueMay (Judgment _ _ (TSet _ xs)) =
+occursCheck :: FreeTypeVars a => TVar -> a -> Bool
+occursCheck a t = a `Set.member` ftv t
+
+-- ** Instances
+
+instance FreeTypeVars Type where
+  ftv TCon{}      = mempty
+  ftv (TVar a   ) = Set.singleton a
+  ftv (TSet _ a ) = Set.unions $ ftv <$> M.elems a
+  ftv (TList a  ) = Set.unions $ ftv <$> a
+  ftv (t1 :~> t2) = ftv t1 `Set.union` ftv t2
+  ftv (TMany ts ) = Set.unions $ ftv <$> ts
+
+instance FreeTypeVars TVar where
+  ftv = Set.singleton
+
+instance FreeTypeVars Scheme where
+  ftv (Forall as t) = ftv t `Set.difference` Set.fromList as
+
+instance FreeTypeVars a => FreeTypeVars [a] where
+  ftv = foldr (Set.union . ftv) mempty
+
+instance (Ord a, FreeTypeVars a) => FreeTypeVars (Set.Set a) where
+  ftv = foldr (Set.union . ftv) mempty
+
+-- * class @ActiveTypeVars@
+
+class ActiveTypeVars a where
+  atv :: a -> Set.Set TVar
+
+-- ** Instances
+
+instance ActiveTypeVars Constraint where
+  atv (EqConst      t1 t2   ) = ftv t1 `Set.union` ftv t2
+  atv (ImpInstConst t1 ms t2) = ftv t1 `Set.union` (ftv ms `Set.intersection` ftv t2)
+  atv (ExpInstConst t  s     ) = ftv t  `Set.union` ftv s
+
+instance ActiveTypeVars a => ActiveTypeVars [a] where
+  atv = foldr (Set.union . atv) mempty
+
+-- * Other
+
+type MonadInfer m
+  = ({- MonadThunkId m,-}
+     MonadVar m, MonadFix m)
+
+-- | Run the inference monad
+runInfer' :: MonadInfer m => InferT s m a -> m (Either InferError a)
+runInfer' =
+  runExceptT
+    . (`evalStateT` initInfer)
+    . (`runReaderT` (mempty, emptyScopes))
+    . getInfer
+
+runInfer :: (forall s . InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
+runInfer m =
+  runST $
     do
-      let sing _ = Judgment As.empty mempty
-      pure $ pure (M.mapWithKey sing xs, mempty)
-  fromValueMay _ = stub
-  fromValue =
-    pure .
-      fromMaybe
-      (mempty, mempty)
-      <=< fromValueMay
+      i <- newVar (1 :: Int)
+      runFreshIdT i $ runInfer' m
 
-instance MonadInfer m
-  => ToValue (AttrSet (Judgment s), AttrSet SourcePos)
-            (InferT s m) (Judgment s) where
-  toValue (xs, _) =
-    liftA3
-      Judgment
-      (foldrM go As.empty xs)
-      (concat <$> traverse ((typeConstraints <$>) . demand) xs)
-      (TSet True <$> traverse ((inferredType <$>) . demand) xs)
-   where
-    go x rest =
-      do
-        x' <- demand x
-        pure $ As.merge (assumptions x') rest
+inferType
+  :: forall s m . MonadInfer m => Env -> NExpr -> InferT s m [(Subst, Type)]
+inferType env ex =
+  do
+    Judgment as cs t <- infer ex
+    let
+      unbounds =
+        (Set.difference `on` Set.fromList)
+          (Assumption.keys as )
+          (       Env.keys env)
+    unless
+      (Set.null unbounds)
+      $ typeError $ UnboundVariables $ ordNub $ Set.toList unbounds
+
+    inferState <- get
+    let
+      cs' =
+        [ ExpInstConst t s
+            | (x, ss) <- Env.toList env
+            , s       <- ss
+            , t       <- Assumption.lookup x as
+        ]
+      eres = (`evalState` inferState) $ runSolver $
+        do
+          subst <- solve $ cs <> cs'
+          pure (subst, subst `apply` t)
+
+    either
+      (throwError . TypeInferenceErrors)
+      pure
+      eres
 
-instance MonadInfer m => ToValue [Judgment s] (InferT s m) (Judgment s) where
-  toValue xs =
-    liftA3
-      Judgment
-      (foldrM go As.empty xs)
-      (concat <$> traverse ((typeConstraints <$>) . demand) xs)
-      (TList <$> traverse ((inferredType <$>) . demand) xs)
-   where
-    go x rest =
-      do
-        x' <- demand x
-        pure $ As.merge (assumptions x') rest
+-- | Solve for the toplevel type of an expression in a given environment
+inferExpr :: Env -> NExpr -> Either InferError [Scheme]
+inferExpr env ex =
+  (\ (subst, ty) -> closeOver $ subst `apply` ty) <<$>>
+    runInfer (inferType env ex)
 
-instance MonadInfer m => ToValue Bool (InferT s m) (Judgment s) where
-  toValue _ = pure $ Judgment As.empty mempty typeBool
+unops :: Type -> NUnaryOp -> [Constraint]
+unops u1 op =
+  [ EqConst u1
+   (case op of
+      NNot -> typeFun [typeBool                   , typeBool                       ]
+      NNeg -> TMany   [typeFun  [typeInt, typeInt], typeFun  [typeFloat, typeFloat]]
+    )
+  ]
+
+binops :: Type -> NBinaryOp -> [Constraint]
+binops u1 op =
+  if
+    -- NApp in fact is handled separately
+    -- Equality tells nothing about the types, because any two types are allowed.
+    | op `elem` [ NApp  , NEq  , NNEq        ] -> mempty
+    | op `elem` [ NGt   , NGte , NLt  , NLte ] -> inequality
+    | op `elem` [ NAnd  , NOr  , NImpl       ] -> gate
+    | op ==       NConcat                      -> concatenation
+    | op `elem` [ NMinus, NMult, NDiv        ] -> arithmetic
+    | op ==       NUpdate                      -> rUnion
+    | op ==       NPlus                        -> addition
+    | otherwise -> fail "GHC so far can not infer that this pattern match is full, so make it happy."
+
+ where
+
+  gate          = eqCnst [typeBool, typeBool, typeBool]
+  concatenation = eqCnst [typeList, typeList, typeList]
+
+  eqCnst l = [EqConst u1 $ typeFun l]
+
+  inequality =
+    eqCnstMtx
+      [ [typeInt  , typeInt  , typeBool]
+      , [typeFloat, typeFloat, typeBool]
+      , [typeInt  , typeFloat, typeBool]
+      , [typeFloat, typeInt  , typeBool]
+      ]
+
+  arithmetic =
+    eqCnstMtx
+      [ [typeInt  , typeInt  , typeInt  ]
+      , [typeFloat, typeFloat, typeFloat]
+      , [typeInt  , typeFloat, typeFloat]
+      , [typeFloat, typeInt  , typeFloat]
+      ]
+
+  rUnion =
+    eqCnstMtx
+      [ [typeSet , typeSet , typeSet]
+      , [typeSet , typeNull, typeSet]
+      , [typeNull, typeSet , typeSet]
+      ]
+
+  addition =
+    eqCnstMtx
+      [ [typeInt   , typeInt   , typeInt   ]
+      , [typeFloat , typeFloat , typeFloat ]
+      , [typeInt   , typeFloat , typeFloat ]
+      , [typeFloat , typeInt   , typeFloat ]
+      , [typeString, typeString, typeString]
+      , [typePath  , typePath  , typePath  ]
+      , [typeString, typeString, typePath  ]
+      ]
+
+  eqCnstMtx mtx = [EqConst u1 $ TMany $ typeFun <$> mtx]
+
+liftInfer :: Monad m => m a -> InferT s m a
+liftInfer = InferT . lift . lift . lift
+
+-- * Other
 
 infer :: MonadInfer m => NExpr -> InferT s m (Judgment s)
 infer = foldFix Eval.eval
@@ -636,36 +773,22 @@ inferTop env ((name, ex) : xs) =
     (\ ty -> inferTop (extend env (name, ty)) xs)
     (inferExpr env ex)
 
-normalizeScheme :: Scheme -> Scheme
-normalizeScheme (Forall _ body) = Forall (snd <$> ord) (normtype body)
- where
-  ord = zip (ordNub $ fv body) (TV . toText <$> letters)
-
-  fv (TVar a  ) = [a]
-  fv (a :~> b ) = fv a <> fv b
-  fv (TCon _  ) = mempty
-  fv (TSet _ a) = concatMap fv (M.elems a)
-  fv (TList a ) = concatMap fv a
-  fv (TMany ts) = concatMap fv ts
-
-  normtype (a :~> b ) = normtype a :~> normtype b
-  normtype (TCon a  ) = TCon a
-  normtype (TSet b a) = TSet b (M.map normtype a)
-  normtype (TList a ) = TList (normtype <$> a)
-  normtype (TMany ts) = TMany (normtype <$> ts)
-  normtype (TVar  a ) =
-    maybe
-      (error "type variable not in signature")
-      TVar
-      (List.lookup a ord)
-
-
--- * Constraint Solver
+-- * Other
 
 newtype Solver m a = Solver (LogicT (StateT [TypeError] m) a)
     deriving (Functor, Applicative, Alternative, Monad, MonadPlus,
               MonadLogic, MonadState [TypeError])
 
+runSolver :: Monad m => Solver m a -> m (Either [TypeError] [a])
+runSolver (Solver s) = do
+  res <- runStateT (observeAllT s) mempty
+  pure $
+    case res of
+      (x : xs, _ ) -> pure (x : xs)
+      (_     , es) -> Left (ordNub es)
+
+-- ** Instances
+
 instance MonadTrans Solver where
   lift = Solver . lift . lift
 
@@ -673,86 +796,72 @@ instance Monad m => MonadError TypeError (Solver m) where
   throwError err = Solver $ lift (modify (err :)) *> empty
   catchError _ _ = error "This is never used"
 
-runSolver :: Monad m => Solver m a -> m (Either [TypeError] [a])
-runSolver (Solver s) = do
-  res <- runStateT (observeAllT s) mempty
-  pure $ case res of
-    (x : xs, _ ) -> pure (x : xs)
-    (_     , es) -> Left (ordNub es)
-
--- | The empty substitution
-emptySubst :: Subst
-emptySubst = mempty
-
--- | Compose substitutions
-compose :: Subst -> Subst -> Subst
-Subst s1 `compose` Subst s2 =
-  Subst $ Map.map (apply (Subst s1)) s2 `Map.union` s1
+-- * Other
 
-unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst
-unifyMany []         []         = pure emptySubst
-unifyMany (t1 : ts1) (t2 : ts2) = do
-  su1 <- unifies t1 t2
-  su2 <- unifyMany (apply su1 ts1) (apply su1 ts2)
-  pure (su2 `compose` su1)
-unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2
+bind :: Monad m => TVar -> Type -> Solver m Subst
+bind a t | t == TVar a     = stub
+         | occursCheck a t = throwError $ InfiniteType a t
+         | otherwise       = pure $ Subst $ Map.singleton a t
 
-allSameType :: [Type] -> Bool
-allSameType []           = True
-allSameType [_         ] = True
-allSameType (x : y : ys) = x == y && allSameType (y : ys)
+considering :: [a] -> Solver m a
+considering xs = Solver $ LogicT $ \c n -> foldr c n xs
 
 unifies :: Monad m => Type -> Type -> Solver m Subst
-unifies t1 t2 | t1 == t2  = pure emptySubst
+unifies t1 t2 | t1 == t2  = stub
 unifies (TVar v) t        = v `bind` t
 unifies t        (TVar v) = v `bind` t
 unifies (TList xs) (TList ys)
-  | allSameType xs && allSameType ys = case (xs, ys) of
-    (x : _, y : _) -> unifies x y
-    _              -> pure emptySubst
+  | allSameType xs && allSameType ys =
+      case (xs, ys) of
+        (x : _, y : _) -> unifies x y
+        _              -> stub
   | length xs == length ys = unifyMany xs ys
--- We assume that lists of different lengths containing various types cannot
+-- Putting a statement that lists of different lengths containing various types would not
 -- be unified.
 unifies t1@(TList _    ) t2@(TList _    ) = throwError $ UnificationFail t1 t2
-unifies (   TSet True _) (   TSet True _) = pure emptySubst
+unifies (   TSet True _) (   TSet True _) = stub
 unifies (TSet False b) (TSet True s)
-  | M.keys b `intersect` M.keys s == M.keys s = pure emptySubst
+  | M.keys b `intersect` M.keys s == M.keys s = stub
 unifies (TSet True s) (TSet False b)
-  | M.keys b `intersect` M.keys s == M.keys b = pure emptySubst
-unifies (TSet False s) (TSet False b) | null (M.keys b \\ M.keys s) =
-  pure emptySubst
+  | M.keys b `intersect` M.keys s == M.keys b = stub
+unifies (TSet False s) (TSet False b)
+  | null (M.keys b \\ M.keys s) = stub
 unifies (t1 :~> t2) (t3 :~> t4) = unifyMany [t1, t2] [t3, t4]
-unifies (TMany t1s) t2          = considering t1s >>- unifies ?? t2
+unifies (TMany t1s) t2          = considering t1s >>- (`unifies` t2)
 unifies t1          (TMany t2s) = considering t2s >>- unifies t1
 unifies t1          t2          = throwError $ UnificationFail t1 t2
 
-bind :: Monad m => TVar -> Type -> Solver m Subst
-bind a t | t == TVar a     = pure emptySubst
-         | occursCheck a t = throwError $ InfiniteType a t
-         | otherwise       = pure (Subst $ Map.singleton a t)
-
-occursCheck :: FreeTypeVars a => TVar -> a -> Bool
-occursCheck a t = a `Set.member` ftv t
+unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst
+unifyMany []         []         = stub
+unifyMany (t1 : ts1) (t2 : ts2) = do
+  su1 <- unifies t1 t2
+  su2 <-
+    unifyMany
+      (apply su1 ts1)
+      (apply su1 ts2)
+  pure $ su2 `compose` su1
+unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2
 
 nextSolvable :: [Constraint] -> (Constraint, [Constraint])
-nextSolvable xs = fromJust (find solvable (chooseOne xs))
+nextSolvable xs = fromJust $ find solvable $ takeFirstOnes xs
  where
-  chooseOne xs = [ (x, ys) | x <- xs, let ys = delete x xs ]
+  takeFirstOnes :: Eq a => [a] -> [(a, [a])]
+  takeFirstOnes xs = [ (x, ys) | x <- xs, let ys = delete x xs ]
 
+  solvable :: (Constraint, [Constraint]) -> Bool
   solvable (EqConst{}     , _) = True
   solvable (ExpInstConst{}, _) = True
   solvable (ImpInstConst _t1 ms t2, cs) =
-    Set.null ((ftv t2 `Set.difference` ms) `Set.intersection` atv cs)
-
-considering :: [a] -> Solver m a
-considering xs = Solver $ LogicT $ \c n -> foldr c n xs
+    Set.null $ (ms `Set.difference` ftv t2) `Set.intersection` atv cs
 
 solve :: MonadState InferState m => [Constraint] -> Solver m Subst
-solve [] = pure emptySubst
-solve cs = solve' (nextSolvable cs)
+solve [] = stub
+solve cs = solve' $ nextSolvable cs
  where
-  solve' (EqConst t1 t2, cs) = unifies t1 t2
-    >>- \su1 -> solve (apply su1 cs) >>- \su2 -> pure (su2 `compose` su1)
+  solve' (EqConst t1 t2, cs) =
+    unifies t1 t2 >>-
+      \su1 -> solve (apply su1 cs) >>-
+          \su2 -> pure $ su2 `compose` su1
 
   solve' (ImpInstConst t1 ms t2, cs) =
     solve (ExpInstConst t1 (generalize ms t2) : cs)
@@ -760,11 +869,3 @@ solve cs = solve' (nextSolvable cs)
   solve' (ExpInstConst t s, cs) = do
     s' <- lift $ instantiate s
     solve (EqConst t s' : cs)
-
-instance
-  Monad m
-  => Scoped (Judgment s) (InferT s m) where
-  currentScopes = currentScopesReader
-  clearScopes   = clearScopesReader @(InferT s m) @(Judgment s)
-  pushScopes    = pushScopesReader
-  lookupVar     = lookupVarReader
diff --git a/src/Nix/Type/Type.hs b/src/Nix/Type/Type.hs
index 863430d72..b1178f225 100644
--- a/src/Nix/Type/Type.hs
+++ b/src/Nix/Type/Type.hs
@@ -1,3 +1,6 @@
+-- | The basis of the Nix type system (type-level).
+--   Based on the Hindley–Milner type system.
+--   Therefore -> from this the type inference follows.
 module Nix.Type.Type where
 
 import           Prelude                 hiding ( Type, TVar )
@@ -8,19 +11,27 @@ type Name = Text
 
 -- | Hindrey-Milner type interface
 
+-- | Type variable in the Nix type system.
 newtype TVar = TV Text
   deriving (Show, Eq, Ord)
 
+-- | The basic type definitions in the Nix type system (type-level code).
 data Type
-  = TVar TVar                -- type variable
-  | TCon Text                -- known type
-  | TSet Bool (AttrSet Type) -- heterogeneous map, bool if variadic
-  | TList [Type]             -- heterogeneous list
-  | (:~>) Type Type          -- type -> type
-  | TMany [Type]             -- variant type
+  = TVar TVar                -- ^ Type variable in the Nix type system.
+  | TCon Text                -- ^ Concrete (non-polymorphic, constant) type in the Nix type system.
+  | TSet Bool (AttrSet Type) -- ^ Heterogeneous map in the Nix type system. @True@ -> variadic.
+  | TList [Type]             -- ^ Heterogeneous list in the Nix type system.
+  | (:~>) Type Type          -- ^ Type arrow (@Type -> Type@) in the Nix type system.
+  | TMany [Type]             -- ^ Variant type (term). Since relating to Nix type system, more precicely -
+                             --   dynamic types in dynamicly typed language (which is Nix).
   deriving (Show, Eq, Ord)
 
-data Scheme = Forall [TVar] Type -- forall a b. a -> b
+infixr 1 :~>
+
+-- | Hindley–Milner type system uses "scheme" term for "polytypes".
+--   Types containing @forall@ quantifiers: @forall a . a@.
+--   Note: HM allows only top-level @forall@ quantification, so no @RankNTypes@ in it.
+data Scheme = Forall [TVar] Type -- ^ @Forall [TVar] Type@: the Nix type system @forall vars. type@.
   deriving (Show, Eq, Ord)
 
 -- This models a set that unifies with any other set.
@@ -30,12 +41,11 @@ typeSet = TSet True mempty
 typeList :: Type
 typeList = TList mempty
 
-infixr 1 :~>
-
 typeFun :: [Type] -> Type
 -- Please, replace with safe analog to `foldr1`
 typeFun = foldr1 (:~>)
 
+-- | Concrete types in the Nix type system.
 typeInt, typeFloat, typeBool, typeString, typePath, typeNull :: Type
 typeInt    = TCon "integer"
 typeFloat  = TCon "float"
diff --git a/src/Nix/Value.hs b/src/Nix/Value.hs
index afa4adb6b..a8d4f8125 100644
--- a/src/Nix/Value.hs
+++ b/src/Nix/Value.hs
@@ -193,7 +193,7 @@ instance Foldable (NValueF p m) where
 
 -- ** Traversable
 
--- | @traverse@
+-- | @sequence@
 sequenceNValueF
   :: (Functor n, Monad m, Applicative n)
   => (forall x . n x -> m x)
@@ -312,7 +312,7 @@ instance Comonad f => Show1 (NValue' t f m) where
 
 -- ** Traversable
 
--- | @traverse@
+-- | @sequence@
 sequenceNValue'
   :: (Functor n, Traversable f, Monad m, Applicative n)
   => (forall x . n x -> m x)
@@ -534,7 +534,7 @@ iterNValueM
   -> NValue t f m
   -> n r
 iterNValueM transform k f =
-    iterM f <=< go . fmap (\t -> k t (iterNValueM transform k f))
+    iterM f <=< go . ((\t -> k t $ iterNValueM transform k f) <$>)
   where
     go (Pure x) = Pure <$> x
     go (Free fa) = Free <$> bindNValue' transform go fa
@@ -548,7 +548,7 @@ hoistNValue
   -> (forall x . m x -> n x)
   -> NValue t f m
   -> NValue t f n
-hoistNValue run lft = hoistFree (hoistNValue' run lft)
+hoistNValue run lft = hoistFree $ hoistNValue' run lft
 {-# inline hoistNValue #-}
 
 -- ** MonadTrans
diff --git a/src/Nix/Value/Equal.hs b/src/Nix/Value/Equal.hs
index 73e24b966..fa545cf4a 100644
--- a/src/Nix/Value/Equal.hs
+++ b/src/Nix/Value/Equal.hs
@@ -15,8 +15,8 @@ import           Prelude                 hiding ( Comparison
                                                 , force
                                                 )
 import           Nix.Utils
-import           Control.Comonad
-import           Control.Monad.Free
+import           Control.Comonad                ( Comonad(extract))
+import           Control.Monad.Free             ( Free(Pure,Free) )
 import           Control.Monad.Trans.Except     ( throwE )
 import           Data.Semialign                 ( Align
                                                 , Semialign(align)
@@ -156,10 +156,8 @@ compareAttrSetsM f eq lm rm =
         r <- isDerivationM f rm
         case r of
           True
-            | Just lp <- HashMap.Lazy.lookup "outPath" lm, Just rp <- HashMap.Lazy.lookup "outPath" rm ->
-                eq
-                  lp
-                  rp
+            | Just lp <- HashMap.Lazy.lookup "outPath" lm,
+              Just rp <- HashMap.Lazy.lookup "outPath" rm -> eq lp rp
           _ -> compareAttrs
       )
       l
@@ -173,7 +171,7 @@ compareAttrSets
   -> AttrSet t
   -> Bool
 compareAttrSets f eq lm rm = runIdentity
-  $ compareAttrSetsM (Identity . f) (\x y -> Identity (eq x y)) lm rm
+  $ compareAttrSetsM (Identity . f) (\x y -> Identity $ eq x y) lm rm
 
 valueEqM
   :: (MonadThunk t m (NValue t f m), Comonad f)
diff --git a/tests/NixLanguageTests.hs b/tests/NixLanguageTests.hs
index 383b98aa5..3c974318a 100644
--- a/tests/NixLanguageTests.hs
+++ b/tests/NixLanguageTests.hs
@@ -107,17 +107,16 @@ assertParse _opts file =
 assertParseFail :: Options -> FilePath -> Assertion
 assertParseFail opts file = do
   eres <- parseNixFileLoc file
-  catch
-      (either
-        (const pass)
-        (\ expr ->
-          do
-            _ <- pure $! runST $ void $ lint opts expr
-            assertFailure $ "Unexpected success parsing `" <> file <> ":\nParsed value: " <> show expr
-        )
-        eres
+  (`catch` \(_ :: SomeException) -> pass)
+    (either
+      (const pass)
+      (\ expr ->
+        do
+          _ <- pure $! runST $ void $ lint opts expr
+          assertFailure $ "Unexpected success parsing `" <> file <> ":\nParsed value: " <> show expr
       )
-      $ \(_ :: SomeException) -> pass
+      eres
+    )
 
 assertLangOk :: Options -> FilePath -> Assertion
 assertLangOk opts file = do
@@ -168,7 +167,7 @@ assertEval _opts files = do
   fixup []                          = mempty
 
 assertEvalFail :: FilePath -> Assertion
-assertEvalFail file = catch ?? (\(_ :: SomeException) -> pass) $ do
+assertEvalFail file = (`catch` (\(_ :: SomeException) -> pass)) $ do
   time       <- liftIO getCurrentTime
   evalResult <- printNix <$> hnixEvalFile (defaultOptions time) file
   evalResult `seq`