hnix/src/Nix/Type/Infer.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

module Nix.Type.Infer
  ( Constraint(..)
  , TypeError(..)
  , InferError(..)
  , Subst(..)
  , inferTop
  )
where

import           Control.Applicative
import           Control.Arrow
import           Control.Monad.Catch
import           Control.Monad.Except
import           Control.Monad.Fail
import           Control.Monad.Logic
import           Control.Monad.Reader
import           Control.Monad.Ref
import           Control.Monad.ST
import           Control.Monad.State.Strict
import           Data.Fix
import           Data.Foldable
import qualified Data.HashMap.Lazy             as M
import           Data.List                      ( delete
                                                , find
                                                , nub
                                                , intersect
                                                , (\\)
                                                )
import           Data.Map                       ( Map )
import qualified Data.Map                      as Map
import           Data.Maybe                     ( fromJust )
import qualified Data.Set                      as Set
import           Data.Text                      ( Text )
import           Nix.Atoms
import           Nix.Convert
import           Nix.Eval                       ( MonadEval(..) )
import qualified Nix.Eval                      as Eval
import           Nix.Expr.Types
import           Nix.Expr.Types.Annotated
import           Nix.Fresh
import           Nix.String
import           Nix.Scope
import           Nix.Thunk
import           Nix.Thunk.Basic
import qualified Nix.Type.Assumption           as As
import           Nix.Type.Env
import qualified Nix.Type.Env                  as Env
import           Nix.Type.Type
import           Nix.Utils
import           Nix.Var

-------------------------------------------------------------------------------
-- Classes
-------------------------------------------------------------------------------

-- | Inference monad
newtype InferT s m a = InferT
    { getInfer ::
        ReaderT (Set.Set TVar, Scopes (InferT s m) (JThunkT s m))
            (StateT InferState (ExceptT InferError m)) a
    }
    deriving
        ( Functor
        , Applicative
        , Alternative
        , Monad
        , MonadPlus
        , MonadFix
        , MonadReader (Set.Set TVar, Scopes (InferT s m) (JThunkT s m))
        , MonadFail
        , MonadState InferState
        , MonadError InferError
        )

instance MonadTrans (InferT s) where
  lift = InferT . lift . lift . lift

instance MonadThunkId m => MonadThunkId (InferT s m) where
  type ThunkId (InferT s m) = ThunkId m

-- | Inference state
newtype InferState = InferState { count :: Int }

-- | Initial inference state
initInfer :: InferState
initInfer = InferState { count = 0 }

data Constraint
    = EqConst Type Type
    | ExpInstConst Type Scheme
    | ImpInstConst Type (Set.Set TVar) Type
    deriving (Show, Eq, Ord)

newtype Subst = Subst (Map TVar Type)
  deriving (Eq, Ord, Show, Semigroup, Monoid)

class Substitutable a where
  apply :: Subst -> a -> a

instance Substitutable TVar where
  apply (Subst s) a = tv
   where
    t         = TVar a
    (TVar tv) = Map.findWithDefault t a s

instance Substitutable Type where
  apply _         (  TCon a   ) = TCon a
  apply s         (  TSet b a ) = TSet b (M.map (apply s) a)
  apply s         (  TList a  ) = TList (map (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 (map (apply s) ts)

instance Substitutable Scheme where
  apply (Subst s) (Forall as t) = Forall as $ apply s' t
    where s' = Subst $ foldr Map.delete s as

instance Substitutable Constraint where
  apply s (EqConst      t1 t2) = EqConst (apply s t1) (apply s t2)
  apply s (ExpInstConst t  sc) = ExpInstConst (apply s t) (apply s sc)
  apply s (ImpInstConst t1 ms t2) =
    ImpInstConst (apply s t1) (apply s ms) (apply s t2)

instance Substitutable a => Substitutable [a] where
  apply = map . apply

instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
  apply = Set.map . apply


class FreeTypeVars a where
  ftv :: a -> Set.Set TVar

instance FreeTypeVars Type where
  ftv TCon{}      = Set.empty
  ftv (TVar a   ) = Set.singleton a
  ftv (TSet _ a ) = Set.unions (map ftv (M.elems a))
  ftv (TList a  ) = Set.unions (map ftv a)
  ftv (t1 :~> t2) = ftv t1 `Set.union` ftv t2
  ftv (TMany ts ) = Set.unions (map 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) Set.empty

instance (Ord a, FreeTypeVars a) => FreeTypeVars (Set.Set a) where
  ftv = foldr (Set.union . ftv) Set.empty


class ActiveTypeVars a where
  atv :: a -> Set.Set TVar

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) Set.empty

data TypeError
  = UnificationFail Type Type
  | InfiniteType TVar Type
  | UnboundVariables [Text]
  | Ambigious [Constraint]
  | UnificationMismatch [Type] [Type]
  deriving (Eq, Show)

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
runInfer' :: MonadInfer m => InferT s m a -> m (Either InferError a)
runInfer' =
  runExceptT
    . (`evalStateT` initInfer)
    . (`runReaderT` (Set.empty, emptyScopes))
    . getInfer

runInfer :: (forall s . InferT s (FreshIdT Int (ST s)) a) -> Either InferError a
runInfer m = runST $ do
  i <- newVar (1 :: Int)
  runFreshIdT i (runInfer' m)

inferType
  :: forall s m . MonadInfer m => Env -> NExpr -> InferT s m [(Subst, Type)]
inferType env ex = do
  Judgment as cs t <- infer ex
  let unbounds =
        Set.fromList (As.keys as) `Set.difference` Set.fromList (Env.keys env)
  unless (Set.null unbounds) $ typeError $ UnboundVariables
    (nub (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')
        return (subst, subst `apply` t)
  case eres of
    Left  errs -> throwError $ TypeInferenceErrors errs
    Right xs   -> pure xs

-- | Solve for the toplevel type of an expression in a given environment
inferExpr :: Env -> NExpr -> Either InferError [Scheme]
inferExpr env ex = case runInfer (inferType env ex) of
  Left  err -> Left err
  Right xs  -> Right $ map (\(subst, ty) -> closeOver (subst `apply` ty)) xs

-- | Canonicalize and return the polymorphic toplevel type.
closeOver :: Type -> Scheme
closeOver = normalize . generalize Set.empty

extendMSet :: Monad m => TVar -> InferT s m a -> InferT s m a
extendMSet x = InferT . local (first (Set.insert x)) . getInfer

letters :: [String]
letters = [1 ..] >>= flip replicateM ['a' .. 'z']

freshTVar :: MonadState InferState m => m TVar
freshTVar = do
  s <- get
  put s { count = count s + 1 }
  return $ TV (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' <- mapM (const fresh) as
  let s = Subst $ Map.fromList $ zip as as'
  return $ apply s t

generalize :: Set.Set TVar -> Type -> Scheme
generalize free t = Forall as t
  where as = Set.toList $ ftv t `Set.difference` free

unops :: Type -> NUnaryOp -> [Constraint]
unops u1 = \case
  NNot -> [EqConst u1 (typeFun [typeBool, typeBool])]
  NNeg ->
    [ EqConst
        u1
        (TMany [typeFun [typeInt, typeInt], typeFun [typeFloat, typeFloat]])
    ]

binops :: Type -> NBinaryOp -> [Constraint]
binops u1 = \case
  NApp  -> []                -- this is handled separately

  -- Equality tells you nothing about the types, because any two types are
  -- allowed.
  NEq   -> []
  NNEq  -> []

  NGt   -> inequality
  NGte  -> inequality
  NLt   -> inequality
  NLte  -> inequality

  NAnd  -> [EqConst u1 (typeFun [typeBool, typeBool, typeBool])]
  NOr   -> [EqConst u1 (typeFun [typeBool, typeBool, typeBool])]
  NImpl -> [EqConst u1 (typeFun [typeBool, typeBool, typeBool])]

  NConcat ->
    [ EqConst
        u1
        (TMany
          [ typeFun [typeList, typeList, typeList]
          , typeFun [typeList, typeNull, typeList]
          , typeFun [typeNull, typeList, typeList]
          ]
        )
    ]

  NUpdate ->
    [ EqConst
        u1
        (TMany
          [ typeFun [typeSet, typeSet, typeSet]
          , typeFun [typeSet, typeNull, typeSet]
          , typeFun [typeNull, typeSet, typeSet]
          ]
        )
    ]

  NPlus ->
    [ EqConst
        u1
        (TMany
          [ typeFun [typeInt, typeInt, typeInt]
          , typeFun [typeFloat, typeFloat, typeFloat]
          , typeFun [typeInt, typeFloat, typeFloat]
          , typeFun [typeFloat, typeInt, typeFloat]
          , typeFun [typeString, typeString, typeString]
          , typeFun [typePath, typePath, typePath]
          , typeFun [typeString, typeString, typePath]
          ]
        )
    ]
  NMinus -> arithmetic
  NMult  -> arithmetic
  NDiv   -> arithmetic
 where
  inequality =
    [ EqConst
        u1
        (TMany
          [ typeFun [typeInt, typeInt, typeBool]
          , typeFun [typeFloat, typeFloat, typeBool]
          , typeFun [typeInt, typeFloat, typeBool]
          , typeFun [typeFloat, typeInt, typeBool]
          ]
        )
    ]

  arithmetic =
    [ EqConst
        u1
        (TMany
          [ typeFun [typeInt, typeInt, typeInt]
          , typeFun [typeFloat, typeFloat, typeFloat]
          , typeFun [typeInt, typeFloat, typeFloat]
          , typeFun [typeFloat, typeInt, typeFloat]
          ]
        )
    ]

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)
    return 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)

instance MonadInfer m
  => MonadThunk (JThunkT s m) (InferT s m) (Judgment s) where
  thunk = fmap JThunk . thunk
  thunkId (JThunk x) = thunkId x

  query (JThunk x) b f = query x b f
  queryM (JThunk x) b f = queryM x b f

  force (JThunk t) f = catch (force t f)
    $ \(_ :: ThunkLoop) ->
-- If we have a thunk loop, we just don't know the type.
                           f =<< Judgment As.empty [] <$> fresh
  forceEff (JThunk t) f = catch (forceEff t f)
    $ \(_ :: ThunkLoop) ->
-- If we have a thunk loop, we just don't know the type.
                           f =<< Judgment As.empty [] <$> fresh

  wrapValue = JThunk . wrapValue
  getValue (JThunk x) = getValue x

instance MonadInfer m => MonadEval (Judgment s) (InferT s m) where
  freeVariable var = do
    tv <- fresh
    return $ Judgment (As.singleton var tv) [] tv

  synHole var = do
    tv <- fresh
    return $ Judgment (As.singleton var tv) [] tv

-- If we fail to look up an attribute, we just don't know the type.
  attrMissing _ _ = Judgment As.empty [] <$> fresh

  evaledSym _ = pure

  evalCurPos = return $ Judgment As.empty [] $ TSet False $ M.fromList
    [("file", typePath), ("line", typeInt), ("col", typeInt)]

  evalConstant c = return $ Judgment As.empty [] (go c)
   where
    go = \case
      NInt   _ -> typeInt
      NFloat _ -> typeFloat
      NBool  _ -> typeBool
      NNull    -> typeNull

  evalString      = const $ return $ Judgment As.empty [] typeString
  evalLiteralPath = const $ return $ Judgment As.empty [] typePath
  evalEnvPath     = const $ return $ Judgment As.empty [] typePath

  evalUnary op (Judgment as1 cs1 t1) = do
    tv <- fresh
    return $ Judgment as1 (cs1 ++ unops (t1 :~> tv) op) tv

  evalBinary op (Judgment as1 cs1 t1) e2 = do
    Judgment as2 cs2 t2 <- e2
    tv                  <- fresh
    return $ Judgment (as1 `As.merge` as2)
                      (cs1 ++ cs2 ++ binops (t1 :~> t2 :~> tv) op)
                      tv

  evalWith = Eval.evalWithAttrSet

  evalIf (Judgment as1 cs1 t1) t f = do
    Judgment as2 cs2 t2 <- t
    Judgment as3 cs3 t3 <- f
    return $ Judgment
      (as1 `As.merge` as2 `As.merge` as3)
      (cs1 ++ cs2 ++ cs3 ++ [EqConst t1 typeBool, EqConst t2 t3])
      t2

  evalAssert (Judgment as1 cs1 t1) body = do
    Judgment as2 cs2 t2 <- body
    return
      $ Judgment (as1 `As.merge` as2) (cs1 ++ cs2 ++ [EqConst t1 typeBool]) t2

  evalApp (Judgment as1 cs1 t1) e2 = do
    Judgment as2 cs2 t2 <- e2
    tv                  <- fresh
    return $ Judgment (as1 `As.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) [] tv)) (\_ b -> ((), ) <$> b))
    return $ Judgment (as `As.remove` x)
                      (cs ++ [ EqConst t' tv | t' <- As.lookup x as ])
                      (tv :~> t)

  evalAbs (ParamSet ps variadic _mname) k = do
    js <- fmap concat $ forM ps $ \(name, _) -> do
      tv <- fresh
      pure [(name, tv)]

    let (env, tys) =
          (\f -> foldl' f (As.empty, M.empty) js) $ \(as1, t1) (k, t) ->
            (as1 `As.merge` As.singleton k t, M.insert k t t1)
        arg   = pure $ Judgment env [] (TSet True tys)
        call  = k arg $ \args b -> (args, ) <$> b
        names = map fst js

    (args, Judgment as cs t) <- foldr (\(_, TVar a) -> extendMSet a) call js

    ty <- TSet variadic <$> traverse (inferredType <$>) args

    return $ Judgment
      (foldl' As.remove as names)
      (cs ++ [ EqConst t' (tys M.! x) | x <- names, t' <- As.lookup x as ])
      (ty :~> t)

  evalError = throwError . EvaluationError

data Judgment s = Judgment
    { assumptions     :: As.Assumption
    , typeConstraints :: [Constraint]
    , inferredType    :: Type
    }
    deriving Show

instance Monad m => FromValue NixString (InferT s m) (Judgment s) where
  fromValueMay _ = return Nothing
  fromValue _ = error "Unused"

instance MonadInfer m
  => FromValue (AttrSet (JThunkT s m), AttrSet SourcePos)
              (InferT s m) (Judgment s) where
  fromValueMay (Judgment _ _ (TSet _ xs)) = do
    let sing _ = Judgment As.empty []
    pure $ Just (M.mapWithKey (\k v -> wrapValue (sing k v)) xs, M.empty)
  fromValueMay _ = pure Nothing
  fromValue = fromValueMay >=> \case
    Just v  -> pure v
    Nothing -> pure (M.empty, M.empty)

instance MonadInfer m
  => ToValue (AttrSet (JThunkT s m), AttrSet SourcePos)
            (InferT s m) (Judgment s) where
  toValue (xs, _) =
    Judgment
      <$> foldrM go As.empty xs
      <*> (concat <$> traverse (`force` (pure . typeConstraints)) xs)
      <*> (TSet True <$> traverse (`force` (pure . inferredType)) xs)
    where go x rest = force x $ \x' -> pure $ As.merge (assumptions x') rest

instance MonadInfer m => ToValue [JThunkT s m] (InferT s m) (Judgment s) where
  toValue xs =
    Judgment
      <$> foldrM go As.empty xs
      <*> (concat <$> traverse (`force` (pure . typeConstraints)) xs)
      <*> (TList <$> traverse (`force` (pure . inferredType)) xs)
    where go x rest = force x $ \x' -> pure $ As.merge (assumptions x') rest

instance MonadInfer m => ToValue Bool (InferT s m) (Judgment s) where
  toValue _ = pure $ Judgment As.empty [] typeBool

infer :: MonadInfer m => NExpr -> InferT s m (Judgment s)
infer = cata Eval.eval

inferTop :: Env -> [(Text, NExpr)] -> Either InferError Env
inferTop env []                = Right env
inferTop env ((name, ex) : xs) = case inferExpr env ex of
  Left  err -> Left err
  Right ty  -> inferTop (extend env (name, ty)) xs

normalize :: Scheme -> Scheme
normalize (Forall _ body) = Forall (map snd ord) (normtype body)
 where
  ord = zip (nub $ fv body) (map TV letters)

  fv (TVar a  ) = [a]
  fv (a :~> b ) = fv a ++ fv b
  fv (TCon _  ) = []
  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 (map normtype a)
  normtype (TMany ts) = TMany (map normtype ts)
  normtype (TVar  a ) = case Prelude.lookup a ord of
    Just x  -> TVar x
    Nothing -> error "type variable not in signature"

-------------------------------------------------------------------------------
-- Constraint Solver
-------------------------------------------------------------------------------

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 :)) >> mzero
  catchError _ _ = error "This is never used"

runSolver :: Monad m => Solver m a -> m (Either [TypeError] [a])
runSolver (Solver s) = do
  res <- runStateT (observeAllT s) []
  pure $ case res of
    (x : xs, _ ) -> Right (x : xs)
    (_     , es) -> Left (nub es)

-- | The empty substitution
emptySubst :: Subst
emptySubst = mempty

-- | Compose substitutions
compose :: Subst -> Subst -> Subst
Subst s1 `compose` Subst s2 =
  Subst $ Map.map (apply (Subst s1)) s2 `Map.union` s1

unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst
unifyMany []         []         = return emptySubst
unifyMany (t1 : ts1) (t2 : ts2) = do
  su1 <- unifies t1 t2
  su2 <- unifyMany (apply su1 ts1) (apply su1 ts2)
  return (su2 `compose` su1)
unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2

allSameType :: [Type] -> Bool
allSameType []           = True
allSameType [_         ] = True
allSameType (x : y : ys) = x == y && allSameType (y : ys)

unifies :: Monad m => Type -> Type -> Solver m Subst
unifies t1 t2 | t1 == t2  = return 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
    _              -> return emptySubst
  | length xs == length ys = unifyMany xs ys
-- We assume that lists of different lengths containing various types cannot
-- be unified.
unifies t1@(TList _    ) t2@(TList _    ) = throwError $ UnificationFail t1 t2
unifies (   TSet True _) (   TSet True _) = return emptySubst
unifies (TSet False b) (TSet True s)
  | M.keys b `intersect` M.keys s == M.keys s = return emptySubst
unifies (TSet True s) (TSet False b)
  | M.keys b `intersect` M.keys s == M.keys b = return emptySubst
unifies (TSet False s) (TSet False b) | null (M.keys b \\ M.keys s) =
  return emptySubst
unifies (t1 :~> t2) (t3 :~> t4) = unifyMany [t1, t2] [t3, t4]
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     = return emptySubst
         | occursCheck a t = throwError $ InfiniteType a t
         | otherwise       = return (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))
 where
  chooseOne xs = [ (x, ys) | x <- xs, let ys = delete x xs ]

  solvable (EqConst{}     , _) = True
  solvable (ExpInstConst{}, _) = True
  solvable (ImpInstConst _t1 ms t2, cs) =
    Set.null ((ftv t2 `Set.difference` ms) `Set.intersection` atv cs)

considering :: [a] -> Solver m a
considering xs = Solver $ LogicT $ \c n -> foldr c n xs

solve :: MonadState InferState m => [Constraint] -> Solver m Subst
solve [] = return emptySubst
solve cs = solve' (nextSolvable cs)
 where
  solve' (EqConst t1 t2, cs) = unifies t1 t2
    >>- \su1 -> solve (apply su1 cs) >>- \su2 -> return (su2 `compose` su1)

  solve' (ImpInstConst t1 ms t2, cs) =
    solve (ExpInstConst t1 (generalize ms t2) : cs)

  solve' (ExpInstConst t s, cs) = do
    s' <- lift $ instantiate s
    solve (EqConst t s' : cs)

instance Monad m => Scoped (JThunkT s m) (InferT s m) where
  currentScopes = currentScopesReader
  clearScopes   = clearScopesReader @(InferT s m) @(JThunkT s m)
  pushScopes    = pushScopesReader
  lookupVar     = lookupVarReader