From f5508fa36798675379ad40200202ffe86e43fa7e Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Thu, 13 May 2021 22:38:13 +0300
Subject: [PATCH 01/19] Type.Type: add docs

---
 src/Nix/Type/Type.hs | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

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"

From 91ec0a11223b491d563495f484fe432c383cc8d8 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Thu, 13 May 2021 22:39:47 +0300
Subject: [PATCH 02/19] Type.Assumption: clean-up; add docs

---
 src/Nix/Type/Assumption.hs | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

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

From 7bc44fe3665f4fde2dfd53e6639f9206ef670cbc Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Thu, 13 May 2021 22:41:24 +0300
Subject: [PATCH 03/19] Type.Infer: clean-up; docs; qualified As(->ssumption)

---
 src/Nix/Type/Infer.hs | 266 ++++++++++++++++++++++++++----------------
 1 file changed, 165 insertions(+), 101 deletions(-)

diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs
index 7bad7652d..e3a9f6dc4 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
@@ -116,6 +116,7 @@ data Constraint
   | ImpInstConst Type (Set.Set TVar) Type
   deriving (Show, Eq, Ord)
 
+-- | Substitution of the basic type definition by a type variable.
 newtype Subst = Subst (Map TVar Type)
   deriving (Eq, Ord, Show, Semigroup, Monoid)
 
@@ -130,21 +131,31 @@ instance Substitutable TVar where
 
 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 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)
+  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
+   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 (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)
+    ImpInstConst
+      (apply s t1)
+      (apply s ms)
+      (apply s t2)
 
 instance Substitutable a => Substitutable [a] where
   apply = fmap . apply
@@ -159,10 +170,10 @@ class FreeTypeVars a where
 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 (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)
+  ftv (TMany ts ) = Set.unions $ ftv <$> ts
 
 instance FreeTypeVars TVar where
   ftv = Set.singleton
@@ -232,29 +243,35 @@ runInfer m = runST $ do
 
 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
+inferType env ex =
+  do
+    Judgment as cs t <- infer ex
+    let
+      unbounds =
+        Set.difference
+          (Set.fromList $ Assumption.keys as )
+          (Set.fromList $ 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
 
 -- | Solve for the toplevel type of an expression in a given environment
 inferExpr :: Env -> NExpr -> Either InferError [Scheme]
@@ -281,7 +298,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
@@ -326,7 +343,7 @@ binops u1 op =
   gate          = eqCnst [typeBool, typeBool, typeBool]
   concatenation = eqCnst [typeList, typeList, typeList]
 
-  eqCnst l = [EqConst u1 (typeFun l)]
+  eqCnst l = [EqConst u1 $ typeFun l]
 
   inequality =
     eqCnstMtx
@@ -362,7 +379,7 @@ binops u1 op =
       , [typeString, typeString, typePath  ]
       ]
 
-  eqCnstMtx mtx = [EqConst u1 (TMany (typeFun <$> mtx))]
+  eqCnstMtx mtx = [EqConst u1 $ TMany $ typeFun <$> mtx]
 
 liftInfer :: Monad m => m a -> InferT s m a
 liftInfer = InferT . lift . lift . lift
@@ -378,7 +395,7 @@ 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))
@@ -394,7 +411,7 @@ 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
@@ -450,32 +467,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
+  attrMissing _ _ = Judgment Assumption.empty mempty <$> fresh
 
   evaledSym _ = pure
 
-  evalCurPos = pure $ Judgment As.empty mempty $ TSet False $ M.fromList
-    [("file", typePath), ("line", typeInt), ("col", typeInt)]
+  evalCurPos =
+    pure $
+    Judgment
+      Assumption.empty
+      mempty
+      (TSet False $
+        M.fromList
+          [ ("file", typePath)
+          , ("line", typeInt )
+          , ("col" , typeInt )
+          ]
+      )
 
-  evalConstant c = pure $ Judgment As.empty mempty (go c)
+  evalConstant c = pure $ Judgment Assumption.empty mempty $ go c
    where
     go = \case
       NURI   _ -> typeString
@@ -484,20 +511,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 +543,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,8 +598,8 @@ 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)
+        (\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,15 +610,15 @@ 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
+    { assumptions     :: Assumption.Assumption
     , typeConstraints :: [Constraint]
     , inferredType    :: Type
     }
@@ -585,7 +639,7 @@ instance
  where
   fromValueMay (Judgment _ _ (TSet _ xs)) =
     do
-      let sing _ = Judgment As.empty mempty
+      let sing _ = Judgment Assumption.empty mempty
       pure $ pure (M.mapWithKey sing xs, mempty)
   fromValueMay _ = stub
   fromValue =
@@ -600,30 +654,30 @@ instance MonadInfer m
   toValue (xs, _) =
     liftA3
       Judgment
-      (foldrM go As.empty xs)
+      (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 $ As.merge (assumptions x') rest
+        pure $ Assumption.merge (assumptions x') rest
 
 instance MonadInfer m => ToValue [Judgment s] (InferT s m) (Judgment s) where
   toValue xs =
     liftA3
       Judgment
-      (foldrM go As.empty xs)
+      (foldrM go Assumption.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
+        pure $ Assumption.merge (assumptions x') rest
 
 instance MonadInfer m => ToValue Bool (InferT s m) (Judgment s) where
-  toValue _ = pure $ Judgment As.empty mempty typeBool
+  toValue _ = pure $ Judgment Assumption.empty mempty typeBool
 
 infer :: MonadInfer m => NExpr -> InferT s m (Judgment s)
 infer = foldFix Eval.eval
@@ -639,20 +693,23 @@ inferTop env ((name, ex) : xs) =
 normalizeScheme :: Scheme -> Scheme
 normalizeScheme (Forall _ body) = Forall (snd <$> ord) (normtype body)
  where
-  ord = zip (ordNub $ fv body) (TV . toText <$> letters)
+  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 (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 (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")
@@ -676,9 +733,10 @@ instance Monad m => MonadError TypeError (Solver m) where
 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)
+  pure $
+    case res of
+      (x : xs, _ ) -> pure (x : xs)
+      (_     , es) -> Left (ordNub es)
 
 -- | The empty substitution
 emptySubst :: Subst
@@ -687,7 +745,7 @@ emptySubst = mempty
 -- | Compose substitutions
 compose :: Subst -> Subst -> Subst
 Subst s1 `compose` Subst s2 =
-  Subst $ Map.map (apply (Subst s1)) s2 `Map.union` s1
+  Subst $ Map.map (apply $ Subst s1) s2 `Map.union` s1
 
 unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst
 unifyMany []         []         = pure emptySubst
@@ -697,6 +755,7 @@ unifyMany (t1 : ts1) (t2 : ts2) = do
   pure (su2 `compose` su1)
 unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2
 
+-- | Check if all elements are of the same type.
 allSameType :: [Type] -> Bool
 allSameType []           = True
 allSameType [_         ] = True
@@ -707,11 +766,12 @@ unifies t1 t2 | t1 == t2  = pure emptySubst
 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
+        _              -> pure emptySubst
   | 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
@@ -729,30 +789,34 @@ 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)
+         | otherwise       = pure $ Subst $ Map.singleton a t
 
 occursCheck :: FreeTypeVars a => TVar -> a -> Bool
 occursCheck a t = a `Set.member` ftv t
 
 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)
+    Set.null $ (ms `Set.difference` ftv t2) `Set.intersection` atv cs
 
 considering :: [a] -> Solver m a
 considering xs = Solver $ LogicT $ \c n -> foldr c n xs
 
 solve :: MonadState InferState m => [Constraint] -> Solver m Subst
 solve [] = pure emptySubst
-solve cs = solve' (nextSolvable cs)
+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)

From 1db8302896bc76871146e6fed18d876303c6ce79 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Thu, 13 May 2021 23:21:15 +0300
Subject: [PATCH 04/19] Type.Infer: reorganize, add headers

---
 src/Nix/Type/Infer.hs | 149 +++++++++++++++++++++++++-----------------
 src/Nix/Value.hs      |   8 +--
 2 files changed, 92 insertions(+), 65 deletions(-)

diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs
index e3a9f6dc4..1873c7a56 100644
--- a/src/Nix/Type/Infer.hs
+++ b/src/Nix/Type/Infer.hs
@@ -73,7 +73,38 @@ import           Nix.Value.Monad
 import           Nix.Var
 
 
--- * Classes
+-- * @InferError@
+
+data InferError
+  = TypeInferenceErrors [TypeError]
+  | TypeInferenceAborted
+  | forall s. Exception s => EvaluationError s
+
+typeError :: MonadError InferError m => TypeError -> m ()
+typeError err = throwError $ TypeInferenceErrors [err]
+
+-- ** Instances
+
+deriving instance Show InferError
+instance Exception InferError
+
+instance Semigroup InferError where
+  x <> _ = x
+
+instance Monoid InferError where
+  mempty  = TypeInferenceAborted
+  mappend = (<>)
+
+-- * @InferState@: inderence state
+
+-- | Inference state
+newtype InferState = InferState { count :: Int }
+
+-- | Initial inference state
+initInfer :: InferState
+initInfer = InferState { count = 0 }
+
+-- * @InferT@: inference monad
 
 -- | Inference monad
 newtype InferT s m a =
@@ -97,18 +128,49 @@ newtype InferT s m a =
       , MonadError InferError
       )
 
+-- ** 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
+  newRef x = liftInfer $ newRef x
+  readRef x = liftInfer $ readRef x
+  writeRef x y = liftInfer $ writeRef x y
+
+instance MonadAtomicRef m => MonadAtomicRef (InferT s m) where
+  atomicModifyRef x f =
+    liftInfer $
+      do
+        res <- snd . f <$> readRef x
+        _   <- modifyRef x $ fst . f
+        pure res
+
+instance Monad m => MonadThrow (InferT s m) where
+  throwM = throwError . EvaluationError
+
+instance Monad m => MonadCatch (InferT s m) where
+  catch m h =
+    catchError m $
+      \case
+        EvaluationError e ->
+          maybe
+            (error $ "Exception was not an exception: " <> show e)
+            h
+            (fromException $ toException e)
+        err -> error $ "Unexpected error: " <> show err
+
 -- instance MonadThunkId m => MonadThunkId (InferT s m) where
 --   type ThunkId (InferT s m) = ThunkId m
 
--- | Inference state
-newtype InferState = InferState { count :: Int }
+-- * @Subst@ data type
 
--- | Initial inference state
-initInfer :: InferState
-initInfer = InferState { count = 0 }
+-- | Substitution of the basic type definition by a type variable.
+newtype Subst = Subst (Map TVar Type)
+  deriving (Eq, Ord, Show, Semigroup, Monoid)
+
+-- * @Constraint@ data type
 
 data Constraint
   = EqConst Type Type
@@ -116,13 +178,13 @@ data Constraint
   | ImpInstConst Type (Set.Set TVar) Type
   deriving (Show, Eq, Ord)
 
--- | Substitution of the basic type definition by a type variable.
-newtype Subst = Subst (Map TVar Type)
-  deriving (Eq, Ord, Show, Semigroup, Monoid)
+-- * class @Substitutable@
 
 class Substitutable a where
   apply :: Subst -> a -> a
 
+-- ** Instances
+
 instance Substitutable TVar where
   apply (Subst s) a = tv
    where
@@ -164,9 +226,13 @@ instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
   apply = Set.map . apply
 
 
+-- * class @FreeTypeVars@
+
 class FreeTypeVars a where
   ftv :: a -> Set.Set TVar
 
+-- ** Instances
+
 instance FreeTypeVars Type where
   ftv TCon{}      = mempty
   ftv (TVar a   ) = Set.singleton a
@@ -187,10 +253,13 @@ instance FreeTypeVars a => FreeTypeVars [a] where
 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)
@@ -207,25 +276,6 @@ data TypeError
   | UnificationMismatch [Type] [Type]
   deriving (Eq, Show, Ord)
 
-data InferError
-  = TypeInferenceErrors [TypeError]
-  | TypeInferenceAborted
-  | forall s. Exception s => EvaluationError s
-
-typeError :: MonadError InferError m => TypeError -> m ()
-typeError err = throwError $ TypeInferenceErrors [err]
-
-deriving instance Show InferError
-instance Exception InferError
-
-instance Semigroup InferError where
-  x <> _ = x
-
-instance Monoid InferError where
-  mempty  = TypeInferenceAborted
-  mappend = (<>)
-
-
 -- * Inference
 
 -- | Run the inference monad
@@ -384,36 +434,8 @@ binops u1 op =
 liftInfer :: Monad m => m a -> InferT s m a
 liftInfer = InferT . lift . lift . lift
 
-instance MonadRef m => MonadRef (InferT s m) where
-  type Ref (InferT s m) = Ref m
-  newRef x = liftInfer $ newRef x
-  readRef x = liftInfer $ readRef x
-  writeRef x y = liftInfer $ writeRef x y
-
-instance MonadAtomicRef m => MonadAtomicRef (InferT s m) where
-  atomicModifyRef x f =
-    liftInfer $
-      do
-        res <- snd . f <$> readRef x
-        _   <- 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
-
-instance Monad m => MonadCatch (InferT s m) where
-  catch m h =
-    catchError m $
-      \case
-        EvaluationError e ->
-          maybe
-            (error $ "Exception was not an exception: " <> show e)
-            h
-            (fromException $ toException e)
-        err -> error $ "Unexpected error: " <> show err
-
 type MonadInfer m
   = ({- MonadThunkId m,-}
      MonadVar m, MonadFix m)
@@ -600,7 +622,7 @@ instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
       (env, 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)
+      arg   = pure $ Judgment env mempty $ TSet True tys
       call  = k arg $ \args b -> (args, ) <$> b
       names = fst <$> js
 
@@ -717,7 +739,7 @@ normalizeScheme (Forall _ body) = Forall (snd <$> ord) (normtype body)
       (List.lookup a ord)
 
 
--- * Constraint Solver
+-- * Constraint solver
 
 newtype Solver m a = Solver (LogicT (StateT [TypeError] m) a)
     deriving (Functor, Applicative, Alternative, Monad, MonadPlus,
@@ -745,14 +767,19 @@ emptySubst = mempty
 -- | Compose substitutions
 compose :: Subst -> Subst -> Subst
 Subst s1 `compose` Subst s2 =
-  Subst $ Map.map (apply $ Subst s1) s2 `Map.union` s1
+  Subst $
+    apply (Subst s1) `Map.map`
+      (s2 `Map.union` s1)
 
 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)
+  su2 <-
+    unifyMany
+      (apply su1 ts1)
+      (apply su1 ts2)
+  pure $ su2 `compose` su1
 unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2
 
 -- | Check if all elements are of the same type.
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

From 84d306c15a9d8748e34c9ef8f40e4ba62af3d931 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sat, 15 May 2021 15:15:37 +0300
Subject: [PATCH 05/19] NixLanguageTests: m clean-up

---
 tests/NixLanguageTests.hs | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

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`

From c233e8a8f914c925c0e1bad38d28c5c2fcc9579c Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sat, 15 May 2021 15:16:15 +0300
Subject: [PATCH 06/19] Value.Equal: m clean-up

---
 src/Nix/Value/Equal.hs | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

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)

From 77906d2d591175d717eedc9d9e8eface97f7b7af Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sat, 15 May 2021 15:16:49 +0300
Subject: [PATCH 07/19] Parser: m clean-up

---
 src/Nix/Parser.hs | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Nix/Parser.hs b/src/Nix/Parser.hs
index c94b820aa..cf8f50d58 100644
--- a/src/Nix/Parser.hs
+++ b/src/Nix/Parser.hs
@@ -623,20 +623,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 +717,7 @@ getUnaryOperator = (m Map.!)
         zipWith
           buildEntry
           [1 ..]
-          (nixOperators (fail "unused"))
+          (nixOperators $ fail "unused")
 
   buildEntry i =
     concatMap $
@@ -734,7 +734,7 @@ getBinaryOperator = (m Map.!)
         zipWith
           buildEntry
           [1 ..]
-          (nixOperators (fail "unused"))
+          (nixOperators $ fail "unused")
 
   buildEntry i =
     concatMap $
@@ -752,7 +752,7 @@ getSpecialOperator o         = m Map.! o
         zipWith
           buildEntry
           [1 ..]
-          (nixOperators (fail "unused"))
+          (nixOperators $ fail "unused")
 
   buildEntry i =
     concatMap $

From 65a35cafee03085fecd0397d6ff40fc585666209 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sat, 15 May 2021 15:17:09 +0300
Subject: [PATCH 08/19] cabal: dep: bytestring: allow 0.11

---
 hnix.cabal | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

From 3280b53c932ac172aff8b382035e83b25a6bf22e Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sat, 15 May 2021 15:18:30 +0300
Subject: [PATCH 09/19] Expr.Types.Annotated: reorder NExprLocF patterns

Just to match constructor definition order.
---
 src/Nix/Expr/Types/Annotated.hs | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Nix/Expr/Types/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index e62ba6d3c..cab123743 100644
--- a/src/Nix/Expr/Types/Annotated.hs
+++ b/src/Nix/Expr/Types/Annotated.hs
@@ -175,18 +175,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 +196,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 +223,5 @@ 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))

From 19de123a6aa0f5148cd569eebea7da5bb02d3197 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sat, 15 May 2021 15:19:51 +0300
Subject: [PATCH 10/19] Expr.Types.Annotated: declare NExprLocF patterns as
 complete

As after reordering it can be seen - they match on all constructors.
---
 src/Nix/Expr/Types/Annotated.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Nix/Expr/Types/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index cab123743..3c7b0a772 100644
--- a/src/Nix/Expr/Types/Annotated.hs
+++ b/src/Nix/Expr/Types/Annotated.hs
@@ -225,3 +225,4 @@ pattern NAssert_ ann x y = Compose (Ann ann (NAssert 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_ #-}

From fc6380825c0092f17058cd0b11313860ab3564a7 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sat, 15 May 2021 15:21:16 +0300
Subject: [PATCH 11/19] Expr.Types.Annotated: declare pattern AnnE complete

As there is only 1 constructor to Ann & as everything is guarded by type code -
there is only 1 possible pattern under that type - so it
is complete.

As a result GHC now sees that buttoms are superflous.
---
 src/Nix/Expr/Types/Annotated.hs | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/Nix/Expr/Types/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index 3c7b0a772..43e2a6bc5 100644
--- a/src/Nix/Expr/Types/Annotated.hs
+++ b/src/Nix/Expr/Types/Annotated.hs
@@ -74,6 +74,13 @@ instance Hashable ann => Hashable1 (Ann ann)
 #ifdef MIN_VERSION_serialise
 instance (Serialise ann, Serialise a) => Serialise (Ann ann a)
 #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))
+{-# complete AnnE #-}
 
 instance NFData ann => NFData1 (Ann ann)
 
@@ -119,9 +126,6 @@ instance Serialise r => Serialise (Compose (Ann SrcSpan) NExprF r) where
   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))
 
 stripAnnotation :: Functor f => Fix (AnnF ann f) -> Fix f
 stripAnnotation = unfoldFix (annotated . getCompose . unFix)
@@ -131,33 +135,26 @@ 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"
 
 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

From 2815371913521bafd4c5f7c03be8f3c2dab22cda Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sun, 16 May 2021 17:55:41 +0300
Subject: [PATCH 12/19] Expr.Types: add notes to data {Params:ParamSet,
 NExprF:NSelect}

Some improvement ideas.

Grew to not like to put such in reports, since they get lost there and one can
implement them while at hand in the topic. (probably would do this during
breakage writing phase).
---
 src/Nix/Expr/Types.hs | 4 ++++
 1 file changed, 4 insertions(+)

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.
   --

From 7211f79735d1392d3932f67fb2afef69ec8b83d2 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sun, 16 May 2021 18:05:04 +0300
Subject: [PATCH 13/19] Expr.Types.Annotated: org: reorg, add headlines, upd
 docs

---
 src/Nix/Expr/Types/Annotated.hs | 60 ++++++++++++++++++++-------------
 1 file changed, 37 insertions(+), 23 deletions(-)

diff --git a/src/Nix/Expr/Types/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index 43e2a6bc5..b547ebd6a 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,11 +82,8 @@ 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 AnnE
   :: forall ann (g :: * -> *)
   . ann
@@ -82,8 +92,17 @@ pattern AnnE
 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)
@@ -95,37 +114,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
-
+-- * Other
 
 stripAnnotation :: Functor f => Fix (AnnF ann f) -> Fix f
 stripAnnotation = unfoldFix (annotated . getCompose . unFix)

From 24094c4de7a72f44e0dbccd0e39b109471badf0a Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sun, 16 May 2021 19:18:30 +0300
Subject: [PATCH 14/19] Expr.Types.Annotated: nSelectLoc: refactor, leave a
 note on Monoid

---
 src/Nix/Expr/Types/Annotated.hs | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Nix/Expr/Types/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index b547ebd6a..a99b6950c 100644
--- a/src/Nix/Expr/Types/Annotated.hs
+++ b/src/Nix/Expr/Types/Annotated.hs
@@ -157,9 +157,15 @@ nBinary (Ann s1 b) e1@(AnnE s2 _) e2@(AnnE s3 _) =
 
 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
+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

From 787156e17580bee96c99f6699b4725f5ab145237 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sun, 16 May 2021 19:20:54 +0300
Subject: [PATCH 15/19] Nix.Type.Infer: org: reorg; TOC; doc

It is not fully finished reorganization, but better then nothing.

There were several minor optimizations made to the code.
---
 src/Nix/Type/Infer.hs | 822 +++++++++++++++++++++---------------------
 1 file changed, 416 insertions(+), 406 deletions(-)

diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs
index 1873c7a56..9b08df8fa 100644
--- a/src/Nix/Type/Infer.hs
+++ b/src/Nix/Type/Infer.hs
@@ -73,6 +73,59 @@ import           Nix.Value.Monad
 import           Nix.Var
 
 
+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 $ 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
+
+-- | Canonicalize and return the polymorphic toplevel type.
+closeOver :: Type -> Scheme
+closeOver = normalizeScheme . generalize mempty
+
+-- | 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
+
+-- * data type @TypeError@
+
+data TypeError
+  = UnificationFail Type Type
+  | InfiniteType TVar Type
+  | UnboundVariables [Text]
+  | Ambigious [Constraint]
+  | UnificationMismatch [Type] [Type]
+  deriving (Eq, Show, Ord)
+
 -- * @InferError@
 
 data InferError
@@ -95,7 +148,7 @@ instance Monoid InferError where
   mempty  = TypeInferenceAborted
   mappend = (<>)
 
--- * @InferState@: inderence state
+-- * @InferState@: inference state
 
 -- | Inference state
 newtype InferState = InferState { count :: Int }
@@ -104,65 +157,38 @@ newtype InferState = InferState { count :: Int }
 initInfer :: InferState
 initInfer = InferState { count = 0 }
 
--- * @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
-      )
-
--- ** Instances
-
-instance MonadTrans (InferT s) where
-  lift = InferT . lift . lift . lift
+letters :: [String]
+letters =
+  do
+    l <- [1 ..]
+    replicateM
+      l
+      ['a' .. 'z']
 
-instance MonadRef m => MonadRef (InferT s m) where
-  type Ref (InferT s m) = Ref m
-  newRef x = liftInfer $ newRef x
-  readRef x = liftInfer $ readRef x
-  writeRef x y = liftInfer $ writeRef x y
+freshTVar :: MonadState InferState m => m TVar
+freshTVar =
+  do
+    s <- get
+    put s { count = count s + 1 }
+    pure $ TV $ toText $ letters !! count s
 
-instance MonadAtomicRef m => MonadAtomicRef (InferT s m) where
-  atomicModifyRef x f =
-    liftInfer $
-      do
-        res <- snd . f <$> readRef x
-        _   <- modifyRef x $ fst . f
-        pure res
+fresh :: MonadState InferState m => m Type
+fresh = TVar <$> freshTVar
 
-instance Monad m => MonadThrow (InferT s m) where
-  throwM = throwError . EvaluationError
+instantiate :: MonadState InferState m => Scheme -> m Type
+instantiate (Forall as t) =
+  do
+    as' <- traverse (const fresh) as
+    let s = Subst $ Map.fromList $ zip as as'
+    pure $ apply s t
 
-instance Monad m => MonadCatch (InferT s m) where
-  catch m h =
-    catchError m $
-      \case
-        EvaluationError e ->
-          maybe
-            (error $ "Exception was not an exception: " <> show e)
-            h
-            (fromException $ toException e)
-        err -> error $ "Unexpected error: " <> show err
+-- * @Constraint@ data type
 
--- instance MonadThunkId m => MonadThunkId (InferT s m) where
---   type ThunkId (InferT s m) = ThunkId m
+data Constraint
+  = EqConst Type Type
+  | ExpInstConst Type Scheme
+  | ImpInstConst Type (Set.Set TVar) Type
+  deriving (Show, Eq, Ord)
 
 -- * @Subst@ data type
 
@@ -170,13 +196,12 @@ instance Monad m => MonadCatch (InferT s m) where
 newtype Subst = Subst (Map TVar Type)
   deriving (Eq, Ord, Show, Semigroup, Monoid)
 
--- * @Constraint@ data type
-
-data Constraint
-  = EqConst Type Type
-  | ExpInstConst Type Scheme
-  | ImpInstConst Type (Set.Set TVar) Type
-  deriving (Show, Eq, Ord)
+-- | Compose substitutions
+compose :: Subst -> Subst -> Subst
+Subst s1 `compose` Subst s2 =
+  Subst $
+    apply (Subst s1) `Map.map`
+      (s2 `Map.union` s1)
 
 -- * class @Substitutable@
 
@@ -226,220 +251,144 @@ instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
   apply = Set.map . apply
 
 
--- * class @FreeTypeVars@
-
-class FreeTypeVars a where
-  ftv :: a -> Set.Set TVar
-
--- ** 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
+-- * data type @Judgement@
 
-instance FreeTypeVars a => FreeTypeVars [a] where
-  ftv = foldr (Set.union . ftv) mempty
+data Judgment s =
+  Judgment
+    { assumptions     :: Assumption.Assumption
+    , typeConstraints :: [Constraint]
+    , inferredType    :: Type
+    }
+    deriving Show
 
-instance (Ord a, FreeTypeVars a) => FreeTypeVars (Set.Set a) where
-  ftv = foldr (Set.union . ftv) mempty
+-- * @InferT@: inference monad
 
--- * class @ActiveTypeVars@
+-- | 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
+      )
 
-class ActiveTypeVars a where
-  atv :: a -> Set.Set TVar
+extendMSet :: Monad m => TVar -> InferT s m a -> InferT s m a
+extendMSet x = InferT . local (first $ Set.insert x) . getInfer
 
 -- ** 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 MonadTrans (InferT s) where
+  lift = InferT . lift . lift . lift
 
-instance ActiveTypeVars a => ActiveTypeVars [a] where
-  atv = foldr (Set.union . atv) mempty
+instance MonadRef m => MonadRef (InferT s m) where
+  type Ref (InferT s m) = Ref m
+  newRef x = liftInfer $ newRef x
+  readRef x = liftInfer $ readRef x
+  writeRef x y = liftInfer $ writeRef x y
 
-data TypeError
-  = UnificationFail Type Type
-  | InfiniteType TVar Type
-  | UnboundVariables [Text]
-  | Ambigious [Constraint]
-  | UnificationMismatch [Type] [Type]
-  deriving (Eq, Show, Ord)
+instance MonadAtomicRef m => MonadAtomicRef (InferT s m) where
+  atomicModifyRef x f =
+    liftInfer $
+      do
+        res <- snd . f <$> readRef x
+        _   <- modifyRef x $ fst . f
+        pure res
 
--- * Inference
+instance Monad m => MonadThrow (InferT s m) where
+  throwM = throwError . EvaluationError
 
--- | Run the inference monad
-runInfer' :: MonadInfer m => InferT s m a -> m (Either InferError a)
-runInfer' =
-  runExceptT
-    . (`evalStateT` initInfer)
-    . (`runReaderT` (mempty, emptyScopes))
-    . getInfer
+instance Monad m => MonadCatch (InferT s m) where
+  catch m h =
+    catchError m $
+      \case
+        EvaluationError e ->
+          maybe
+            (error $ "Exception was not an exception: " <> show e)
+            h
+            (fromException $ toException e)
+        err -> error $ "Unexpected error: " <> show err
 
-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)
+-- instance MonadThunkId m => MonadThunkId (InferT s m) where
+--   type ThunkId (InferT s m) = ThunkId 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.difference
-          (Set.fromList $ Assumption.keys as )
-          (Set.fromList $ 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
-
--- | 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
-
-extendMSet :: Monad m => TVar -> InferT s m a -> InferT s m a
-extendMSet x = InferT . local (first (Set.insert x)) . getInfer
-
-letters :: [String]
-letters =
-  do
-    l <- [1 ..]
-    replicateM
-      l
-      ['a' .. 'z']
-
-freshTVar :: MonadState InferState m => m TVar
-freshTVar =
-  do
-    s <- get
-    put s { count = count s + 1 }
-    pure $ TV $ toText $ letters !! count s
-
-fresh :: MonadState InferState m => m Type
-fresh = TVar <$> freshTVar
-
-instantiate :: MonadState InferState m => Scheme -> m Type
-instantiate (Forall as t) =
-  do
-    as' <- traverse (const fresh) as
-    let s = Subst $ Map.fromList $ zip as as'
-    pure $ apply s t
-
-generalize :: Set.Set TVar -> Type -> Scheme
-generalize free t = Forall as t
+instance
+  Monad m
+  => FromValue NixString (InferT s m) (Judgment s)
  where
-  as = Set.toList $ ftv t `Set.difference` free
-
-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."
+  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
 
-  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]
-      ]
+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
 
-  addition =
-    eqCnstMtx
-      [ [typeInt   , typeInt   , typeInt   ]
-      , [typeFloat , typeFloat , typeFloat ]
-      , [typeInt   , typeFloat , typeFloat ]
-      , [typeFloat , typeInt   , typeFloat ]
-      , [typeString, typeString, typeString]
-      , [typePath  , typePath  , typePath  ]
-      , [typeString, typeString, typePath  ]
-      ]
+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
 
-  eqCnstMtx mtx = [EqConst u1 $ TMany $ typeFun <$> mtx]
+instance MonadInfer m => ToValue Bool (InferT s m) (Judgment s) where
+  toValue _ = pure $ Judgment Assumption.empty mempty typeBool
 
-liftInfer :: Monad m => m a -> InferT s m a
-liftInfer = InferT . lift . lift . lift
+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))
 
-type MonadInfer m
-  = ({- MonadThunkId m,-}
-     MonadVar m, MonadFix m)
-
 --  2021-02-22: NOTE: Seems like suporflous instance
 instance Monad m => MonadValue (Judgment s) (InferT s m) where
   defer
@@ -506,23 +455,23 @@ instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
     tv <- fresh
     pure $ Judgment (Assumption.singleton var tv) mempty tv
 
--- If we fail to look up an attribute, we just don't know the type.
+  -- 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
-      Assumption.empty
-      mempty
-      (TSet False $
-        M.fromList
-          [ ("file", typePath)
-          , ("line", typeInt )
-          , ("col" , typeInt )
-          ]
-      )
+      Judgment
+        Assumption.empty
+        mempty
+        (TSet False $
+          M.fromList
+            [ ("file", typePath)
+            , ("line", typeInt )
+            , ("col" , typeInt )
+            ]
+        )
 
   evalConstant c = pure $ Judgment Assumption.empty mempty $ go c
    where
@@ -638,68 +587,180 @@ instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
 
   evalError = throwError . EvaluationError
 
-data Judgment s =
-  Judgment
-    { assumptions     :: Assumption.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 Assumption.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 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
+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
 
-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
+    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)
 
-instance MonadInfer m => ToValue Bool (InferT s m) (Judgment s) where
-  toValue _ = pure $ Judgment Assumption.empty mempty typeBool
+    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)
+
+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
@@ -712,46 +773,12 @@ 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 $ 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)
-
-
--- * Constraint solver
+-- * Other
 
 newtype Solver m a = Solver (LogicT (StateT [TypeError] m) a)
     deriving (Functor, Applicative, Alternative, Monad, MonadPlus,
               MonadLogic, MonadState [TypeError])
 
-instance MonadTrans Solver where
-  lift = Solver . lift . lift
-
-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
@@ -760,66 +787,60 @@ runSolver (Solver s) = do
       (x : xs, _ ) -> pure (x : xs)
       (_     , es) -> Left (ordNub es)
 
--- | The empty substitution
-emptySubst :: Subst
-emptySubst = mempty
+-- ** Instances
 
--- | Compose substitutions
-compose :: Subst -> Subst -> Subst
-Subst s1 `compose` Subst s2 =
-  Subst $
-    apply (Subst s1) `Map.map`
-      (s2 `Map.union` s1)
+instance MonadTrans Solver where
+  lift = Solver . lift . lift
 
-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
+instance Monad m => MonadError TypeError (Solver m) where
+  throwError err = Solver $ lift (modify (err :)) *> empty
+  catchError _ _ = error "This is never used"
 
--- | Check if all elements are of the same type.
-allSameType :: [Type] -> Bool
-allSameType []           = True
-allSameType [_         ] = True
-allSameType (x : y : ys) = x == y && allSameType (y : ys)
+-- * Other
+
+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
+
+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
+        _              -> stub
   | length xs == length ys = unifyMany xs ys
 -- 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 $ takeFirstOnes xs
@@ -833,11 +854,8 @@ nextSolvable xs = fromJust $ find solvable $ takeFirstOnes xs
   solvable (ImpInstConst _t1 ms t2, cs) =
     Set.null $ (ms `Set.difference` ftv t2) `Set.intersection` atv cs
 
-considering :: [a] -> Solver m a
-considering xs = Solver $ LogicT $ \c n -> foldr c n xs
-
 solve :: MonadState InferState m => [Constraint] -> Solver m Subst
-solve [] = pure emptySubst
+solve [] = stub
 solve cs = solve' $ nextSolvable cs
  where
   solve' (EqConst t1 t2, cs) =
@@ -851,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

From 761e8549bf70c897332a6d148ccd995b31b191ef Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Sun, 16 May 2021 19:24:10 +0300
Subject: [PATCH 16/19] Nix.Parser: org, TOC, use of liftA*, clean-up

---
 src/Nix/Parser.hs | 154 +++++++++++++++++++++++++---------------------
 1 file changed, 85 insertions(+), 69 deletions(-)

diff --git a/src/Nix/Parser.hs b/src/Nix/Parser.hs
index cf8f50d58..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)
 

From ef2700b23fd84acb49f8f0576ba293469e9d5ae3 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Mon, 17 May 2021 12:32:12 +0300
Subject: [PATCH 17/19] Thunk.Basic: forceMain: refact

---
 src/Nix/Thunk/Basic.hs | 47 +++++++++++++++++++++++-------------------
 1 file changed, 26 insertions(+), 21 deletions(-)

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.
 
 

From 46a82e3446eebf74eebbac7358abc0d3ca405dd4 Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Tue, 18 May 2021 13:54:07 +0300
Subject: [PATCH 18/19] treewide: use pattern AnnE, add doc to it

---
 src/Nix/Cited/Basic.hs          | 14 ++++++--------
 src/Nix/Eval.hs                 |  3 +--
 src/Nix/Expr/Types/Annotated.hs |  1 +
 src/Nix/Reduce.hs               | 14 +++++++-------
 src/Nix/Render/Frame.hs         | 10 +++++-----
 5 files changed, 20 insertions(+), 22 deletions(-)

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/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index a99b6950c..57e6cb89c 100644
--- a/src/Nix/Expr/Types/Annotated.hs
+++ b/src/Nix/Expr/Types/Annotated.hs
@@ -84,6 +84,7 @@ data Ann ann a = Ann
 
 type AnnF ann f = Compose (Ann ann) f
 
+-- | Pattern: @Fix (Compose (Ann _ _))@.
 pattern AnnE
   :: forall ann (g :: * -> *)
   . ann
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 =

From 1ed4d13e5bbc9864c84c58b1fa9eed9b56f0093d Mon Sep 17 00:00:00 2001
From: Anton-Latukha <anton.latukha@gmail.com>
Date: Tue, 18 May 2021 14:08:50 +0300
Subject: [PATCH 19/19] Expr.Types.Annotated: AnnE: add explanation

That is my understanding, it can be wrong (but hey, there were no better there)!
---
 src/Nix/Expr/Types/Annotated.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Nix/Expr/Types/Annotated.hs b/src/Nix/Expr/Types/Annotated.hs
index 57e6cb89c..2704286e3 100644
--- a/src/Nix/Expr/Types/Annotated.hs
+++ b/src/Nix/Expr/Types/Annotated.hs
@@ -85,6 +85,8 @@ data Ann ann a = Ann
 type AnnF ann f = Compose (Ann ann) f
 
 -- | Pattern: @Fix (Compose (Ann _ _))@.
+-- Fix composes units of (annotations & the annotated) into one object.
+-- Giving annotated expression.
 pattern AnnE
   :: forall ann (g :: * -> *)
   . ann