    -- |
    -- Module      :  Cryptol.TypeCheck.Monad
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    {-# LANGUAGE Safe #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE RecursiveDo #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE OverloadedStrings #-}
    module Cryptol.TypeCheck.Monad
      ( module Cryptol.TypeCheck.Monad
      , module Cryptol.TypeCheck.InferTypes
      ) where

    import           Cryptol.ModuleSystem.Name
                        (FreshM(..),Supply,mkParameter
                        , nameInfo, NameInfo(..),NameSource(..))
    import           Cryptol.Parser.Position
    import qualified Cryptol.Parser.AST as P
    import           Cryptol.TypeCheck.AST
    import           Cryptol.TypeCheck.Subst
    import           Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
    import           Cryptol.TypeCheck.InferTypes
    import           Cryptol.TypeCheck.Error(Warning(..),Error(..),cleanupErrors)
    import           Cryptol.TypeCheck.PP (brackets, commaSep)
    import qualified Cryptol.TypeCheck.SimpleSolver as Simple
    import qualified Cryptol.TypeCheck.Solver.SMT as SMT
    import           Cryptol.Utils.PP(pp, (<+>), text, quotes)
    import           Cryptol.Utils.Ident(Ident)
    import           Cryptol.Utils.Panic(panic)

    import qualified Control.Applicative as A
    import           Control.Monad.Fix(MonadFix(..))
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import           Data.Map (Map)
    import           Data.Set (Set)
    import           Data.List(find, foldl')
    import           Data.Maybe(mapMaybe,fromMaybe)
    import           MonadLib hiding (mapM)

    import           Data.IORef

    import GHC.Generics (Generic)
    import Control.DeepSeq

    import Prelude ()
    import Prelude.Compat

    -- | Information needed for type inference.
    data InferInput = InferInput
      { InferInput -> Range
    inpRange     :: Range             -- ^ Location of program source
      , InferInput -> Map Name Schema
    inpVars      :: Map Name Schema   -- ^ Variables that are in scope
      , InferInput -> Map Name TySyn
    inpTSyns     :: Map Name TySyn    -- ^ Type synonyms that are in scope
      , InferInput -> Map Name Newtype
    inpNewtypes  :: Map Name Newtype  -- ^ Newtypes in scope
      , InferInput -> Map Name AbstractType
    inpAbstractTypes :: Map Name AbstractType -- ^ Abstract types in scope

        -- When typechecking a module these start off empty.
        -- We need them when type-checking an expression at the command
        -- line, for example.
      , InferInput -> Map Name ModTParam
    inpParamTypes       :: !(Map Name ModTParam)  -- ^ Type parameters
      , InferInput -> [Located Prop]
    inpParamConstraints :: !([Located Prop])      -- ^ Constraints on parameters
      , InferInput -> Map Name ModVParam
    inpParamFuns        :: !(Map Name ModVParam)  -- ^ Value parameters

      , InferInput -> NameSeeds
    inpNameSeeds :: NameSeeds         -- ^ Private state of type-checker
      , InferInput -> Bool
    inpMonoBinds :: Bool              -- ^ Should local bindings without
                                          --   signatures be monomorphized?

      , InferInput -> SolverConfig
    inpSolverConfig :: SolverConfig   -- ^ Options for the constraint solver
      , InferInput -> [FilePath]
    inpSearchPath :: [FilePath]
        -- ^ Where to look for Cryptol theory file.

      , InferInput -> PrimMap
    inpPrimNames :: !PrimMap
        -- ^ This is used when the type-checker needs to refer to a predefined
        -- identifier (e.g., @number@).

      , InferInput -> Supply
    inpSupply :: !Supply              -- ^ The supply for fresh name generation
      } deriving Int -> InferInput -> ShowS
    [InferInput] -> ShowS
    InferInput -> FilePath
    (Int -> InferInput -> ShowS)
    -> (InferInput -> FilePath)
    -> ([InferInput] -> ShowS)
    -> Show InferInput
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [InferInput] -> ShowS
    $cshowList :: [InferInput] -> ShowS
    show :: InferInput -> FilePath
    $cshow :: InferInput -> FilePath
    showsPrec :: Int -> InferInput -> ShowS
    $cshowsPrec :: Int -> InferInput -> ShowS
    Show

    -- | This is used for generating various names.
    data NameSeeds = NameSeeds
      { NameSeeds -> Int
    seedTVar    :: !Int
      , NameSeeds -> Int
    seedGoal    :: !Int
      } deriving (Int -> NameSeeds -> ShowS
    [NameSeeds] -> ShowS
    NameSeeds -> FilePath
    (Int -> NameSeeds -> ShowS)
    -> (NameSeeds -> FilePath)
    -> ([NameSeeds] -> ShowS)
    -> Show NameSeeds
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [NameSeeds] -> ShowS
    $cshowList :: [NameSeeds] -> ShowS
    show :: NameSeeds -> FilePath
    $cshow :: NameSeeds -> FilePath
    showsPrec :: Int -> NameSeeds -> ShowS
    $cshowsPrec :: Int -> NameSeeds -> ShowS
    Show, (forall x. NameSeeds -> Rep NameSeeds x)
    -> (forall x. Rep NameSeeds x -> NameSeeds) -> Generic NameSeeds
    forall x. Rep NameSeeds x -> NameSeeds
    forall x. NameSeeds -> Rep NameSeeds x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep NameSeeds x -> NameSeeds
    $cfrom :: forall x. NameSeeds -> Rep NameSeeds x
    Generic, NameSeeds -> ()
    (NameSeeds -> ()) -> NFData NameSeeds
    forall a. (a -> ()) -> NFData a
    rnf :: NameSeeds -> ()
    $crnf :: NameSeeds -> ()
    NFData)

    -- | The initial seeds, used when checking a fresh program.
    -- XXX: why does this start at 10?
    nameSeeds :: NameSeeds
    nameSeeds :: NameSeeds
    nameSeeds = $WNameSeeds :: Int -> Int -> NameSeeds
    NameSeeds { seedTVar :: Int
    seedTVar = 10, seedGoal :: Int
    seedGoal = 0 }

    -- | The results of type inference.
    data InferOutput a
      = InferFailed [(Range,Warning)] [(Range,Error)]
        -- ^ We found some errors

      | InferOK [(Range,Warning)] NameSeeds Supply a
        -- ^ Type inference was successful.

        deriving Int -> InferOutput a -> ShowS
    [InferOutput a] -> ShowS
    InferOutput a -> FilePath
    (Int -> InferOutput a -> ShowS)
    -> (InferOutput a -> FilePath)
    -> ([InferOutput a] -> ShowS)
    -> Show (InferOutput a)
    forall a. Show a => Int -> InferOutput a -> ShowS
    forall a. Show a => [InferOutput a] -> ShowS
    forall a. Show a => InferOutput a -> FilePath
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [InferOutput a] -> ShowS
    $cshowList :: forall a. Show a => [InferOutput a] -> ShowS
    show :: InferOutput a -> FilePath
    $cshow :: forall a. Show a => InferOutput a -> FilePath
    showsPrec :: Int -> InferOutput a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> InferOutput a -> ShowS
    Show

    bumpCounter :: InferM ()
    bumpCounter :: InferM ()
    bumpCounter = do RO { .. } <- ReaderT RO (StateT RW IO) RO -> InferM RO
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
                     IO () -> InferM ()
    forall a. IO a -> InferM a
    io (IO () -> InferM ()) -> IO () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ IORef Int -> (Int -> Int) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    modifyIORef' IORef Int
    iSolveCounter (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +1)

    runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
    runInferM :: InferInput -> InferM a -> IO (InferOutput a)
    runInferM info :: InferInput
    info (IM m :: ReaderT RO (StateT RW IO) a
    m) = SolverConfig
    -> (Solver -> IO (InferOutput a)) -> IO (InferOutput a)
    forall a. SolverConfig -> (Solver -> IO a) -> IO a
    SMT.withSolver (InferInput -> SolverConfig
    inpSolverConfig InferInput
    info) ((Solver -> IO (InferOutput a)) -> IO (InferOutput a))
    -> (Solver -> IO (InferOutput a)) -> IO (InferOutput a)
    forall a b. (a -> b) -> a -> b
    $ \solver :: Solver
    solver ->
      do IORef Int
    coutner <- Int -> IO (IORef Int)
    forall a. a -> IO (IORef a)
    newIORef 0
         rec RO
    ro <- RO -> IO RO
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WRO :: Range
    -> Map Name VarType
    -> [TParam]
    -> Map Name (DefLoc, TySyn)
    -> Map Name (DefLoc, Newtype)
    -> Map Name (DefLoc, AbstractType)
    -> Map Name ModTParam
    -> [Located Prop]
    -> Map Name ModVParam
    -> Map Int HasGoalSln
    -> Bool
    -> Solver
    -> PrimMap
    -> IORef Int
    -> RO
    RO { iRange :: Range
    iRange     = InferInput -> Range
    inpRange InferInput
    info
                             , iVars :: Map Name VarType
    iVars          = (Schema -> VarType) -> Map Name Schema -> Map Name VarType
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map Schema -> VarType
    ExtVar (InferInput -> Map Name Schema
    inpVars InferInput
    info)
                             , iTVars :: [TParam]
    iTVars         = []
                             , iTSyns :: Map Name (DefLoc, TySyn)
    iTSyns         = (TySyn -> (DefLoc, TySyn))
    -> Map Name TySyn -> Map Name (DefLoc, TySyn)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap TySyn -> (DefLoc, TySyn)
    forall b. b -> (DefLoc, b)
    mkExternal (InferInput -> Map Name TySyn
    inpTSyns InferInput
    info)
                             , iNewtypes :: Map Name (DefLoc, Newtype)
    iNewtypes      = (Newtype -> (DefLoc, Newtype))
    -> Map Name Newtype -> Map Name (DefLoc, Newtype)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Newtype -> (DefLoc, Newtype)
    forall b. b -> (DefLoc, b)
    mkExternal (InferInput -> Map Name Newtype
    inpNewtypes InferInput
    info)
                             , iAbstractTypes :: Map Name (DefLoc, AbstractType)
    iAbstractTypes = AbstractType -> (DefLoc, AbstractType)
    forall b. b -> (DefLoc, b)
    mkExternal (AbstractType -> (DefLoc, AbstractType))
    -> Map Name AbstractType -> Map Name (DefLoc, AbstractType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferInput -> Map Name AbstractType
    inpAbstractTypes InferInput
    info
                             , iParamTypes :: Map Name ModTParam
    iParamTypes    = InferInput -> Map Name ModTParam
    inpParamTypes InferInput
    info
                             , iParamFuns :: Map Name ModVParam
    iParamFuns     = InferInput -> Map Name ModVParam
    inpParamFuns InferInput
    info
                             , iParamConstraints :: [Located Prop]
    iParamConstraints = InferInput -> [Located Prop]
    inpParamConstraints InferInput
    info

                             , iSolvedHasLazy :: Map Int HasGoalSln
    iSolvedHasLazy = RW -> Map Int HasGoalSln
    iSolvedHas RW
    finalRW     -- RECURSION
                             , iMonoBinds :: Bool
    iMonoBinds     = InferInput -> Bool
    inpMonoBinds InferInput
    info
                             , iSolver :: Solver
    iSolver        = Solver
    solver
                             , iPrimNames :: PrimMap
    iPrimNames     = InferInput -> PrimMap
    inpPrimNames InferInput
    info
                             , iSolveCounter :: IORef Int
    iSolveCounter  = IORef Int
    coutner
                             }

             (result :: a
    result, finalRW :: RW
    finalRW) <- RW -> StateT RW IO a -> IO (a, RW)
    forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
    runStateT RW
    rw
                                (StateT RW IO a -> IO (a, RW)) -> StateT RW IO a -> IO (a, RW)
    forall a b. (a -> b) -> a -> b
    $ RO -> ReaderT RO (StateT RW IO) a -> StateT RW IO a
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
    runReaderT RO
    ro ReaderT RO (StateT RW IO) a
    m  -- RECURSION

         let theSu :: Subst
    theSu    = RW -> Subst
    iSubst RW
    finalRW
             defSu :: Subst
    defSu    = Subst -> Subst
    defaultingSubst Subst
    theSu
             warns :: [(Range, Warning)]
    warns    = [(Range
    r,Subst -> Warning -> Warning
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    theSu Warning
    w) | (r :: Range
    r,w :: Warning
    w) <- RW -> [(Range, Warning)]
    iWarnings RW
    finalRW ]

         case RW -> [(Range, Error)]
    iErrors RW
    finalRW of
           [] ->
             case (RW -> Goals
    iCts RW
    finalRW, RW -> [HasGoal]
    iHasCts RW
    finalRW) of
               (cts :: Goals
    cts,[])
                 | Goals -> Bool
    nullGoals Goals
    cts
                       -> InferOutput a -> IO (InferOutput a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (InferOutput a -> IO (InferOutput a))
    -> InferOutput a -> IO (InferOutput a)
    forall a b. (a -> b) -> a -> b
    $ [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
    forall a.
    [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
    InferOK [(Range, Warning)]
    warns
                                      (RW -> NameSeeds
    iNameSeeds RW
    finalRW)
                                      (RW -> Supply
    iSupply RW
    finalRW)
                                      (Subst -> a -> a
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    defSu a
    result)
               (cts :: Goals
    cts,has :: [HasGoal]
    has) -> InferOutput a -> IO (InferOutput a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (InferOutput a -> IO (InferOutput a))
    -> InferOutput a -> IO (InferOutput a)
    forall a b. (a -> b) -> a -> b
    $ [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
    forall a. [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
    InferFailed [(Range, Warning)]
    warns
                    ([(Range, Error)] -> InferOutput a)
    -> [(Range, Error)] -> InferOutput a
    forall a b. (a -> b) -> a -> b
    $ [(Range, Error)] -> [(Range, Error)]
    cleanupErrors
                    [ ( Goal -> Range
    goalRange Goal
    g
                      , Bool -> [Goal] -> Error
    UnsolvedGoals Bool
    False [Subst -> Goal -> Goal
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    theSu Goal
    g]
                      ) | Goal
    g <- Goals -> [Goal]
    fromGoals Goals
    cts [Goal] -> [Goal] -> [Goal]
    forall a. [a] -> [a] -> [a]
    ++ (HasGoal -> Goal) -> [HasGoal] -> [Goal]
    forall a b. (a -> b) -> [a] -> [b]
    map HasGoal -> Goal
    hasGoal [HasGoal]
    has
                    ]
           errs :: [(Range, Error)]
    errs -> InferOutput a -> IO (InferOutput a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (InferOutput a -> IO (InferOutput a))
    -> InferOutput a -> IO (InferOutput a)
    forall a b. (a -> b) -> a -> b
    $ [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
    forall a. [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
    InferFailed [(Range, Warning)]
    warns
                          ([(Range, Error)] -> InferOutput a)
    -> [(Range, Error)] -> InferOutput a
    forall a b. (a -> b) -> a -> b
    $ [(Range, Error)] -> [(Range, Error)]
    cleanupErrors [(Range
    r,Subst -> Error -> Error
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    theSu Error
    e) | (r :: Range
    r,e :: Error
    e) <- [(Range, Error)]
    errs]

      where
      mkExternal :: b -> (DefLoc, b)
    mkExternal x :: b
    x = (DefLoc
    IsExternal, b
    x)
      rw :: RW
    rw = $WRW :: [(Range, Error)]
    -> [(Range, Warning)]
    -> Subst
    -> [Map Name Prop]
    -> Map Int HasGoalSln
    -> NameSeeds
    -> Goals
    -> [HasGoal]
    -> Supply
    -> RW
    RW { iErrors :: [(Range, Error)]
    iErrors     = []
              , iWarnings :: [(Range, Warning)]
    iWarnings   = []
              , iSubst :: Subst
    iSubst      = Subst
    emptySubst
              , iExistTVars :: [Map Name Prop]
    iExistTVars = []

              , iNameSeeds :: NameSeeds
    iNameSeeds  = InferInput -> NameSeeds
    inpNameSeeds InferInput
    info

              , iCts :: Goals
    iCts        = Goals
    emptyGoals
              , iHasCts :: [HasGoal]
    iHasCts     = []
              , iSolvedHas :: Map Int HasGoalSln
    iSolvedHas  = Map Int HasGoalSln
    forall k a. Map k a
    Map.empty

              , iSupply :: Supply
    iSupply     = InferInput -> Supply
    inpSupply InferInput
    info
              }

    newtype InferM a = IM { InferM a -> ReaderT RO (StateT RW IO) a
    unIM :: ReaderT RO (StateT RW IO) a }

    data DefLoc = IsLocal | IsExternal

    -- | Read-only component of the monad.
    data RO = RO
      { RO -> Range
    iRange    :: Range                  -- ^ Source code being analysed
      , RO -> Map Name VarType
    iVars     :: Map Name VarType      -- ^ Type of variable that are in scope

      {- NOTE: We assume no shadowing between these two, so it does not matter
      where we look first. Similarly, we assume no shadowing with
      the existential type variable (in RW).  See `checkTShadowing`. -}

      , RO -> [TParam]
    iTVars    :: [TParam]                  -- ^ Type variable that are in scope
      , RO -> Map Name (DefLoc, TySyn)
    iTSyns    :: Map Name (DefLoc, TySyn) -- ^ Type synonyms that are in scope
      , RO -> Map Name (DefLoc, Newtype)
    iNewtypes :: Map Name (DefLoc, Newtype)
       -- ^ Newtype declarations in scope
       --
       -- NOTE: type synonyms take precedence over newtype.  The reason is
       -- that we can define local type synonyms, but not local newtypes.
       -- So, either a type-synonym shadows a newtype, or it was declared
       -- at the top-level, but then there can't be a newtype with the
       -- same name (this should be caught by the renamer).
      , RO -> Map Name (DefLoc, AbstractType)
    iAbstractTypes :: Map Name (DefLoc, AbstractType)

      , RO -> Map Name ModTParam
    iParamTypes :: Map Name ModTParam
        -- ^ Parameter types

      , RO -> [Located Prop]
    iParamConstraints :: [Located Prop]
        -- ^ Constraints on the type parameters

      , RO -> Map Name ModVParam
    iParamFuns :: Map Name ModVParam
        -- ^ Parameter functions

      , RO -> Map Int HasGoalSln
    iSolvedHasLazy :: Map Int HasGoalSln
        -- ^ NOTE: This field is lazy in an important way!  It is the
        -- final version of `iSolvedHas` in `RW`, and the two are tied
        -- together through recursion.  The field is here so that we can
        -- look thing up before they are defined, which is OK because we
        -- don't need to know the results until everything is done.

      , RO -> Bool
    iMonoBinds :: Bool
        -- ^ When this flag is set to true, bindings that lack signatures
        -- in where-blocks will never be generalized. Bindings with type
        -- signatures, and all bindings at top level are unaffected.

      , RO -> Solver
    iSolver :: SMT.Solver

      , RO -> PrimMap
    iPrimNames :: !PrimMap

      , RO -> IORef Int
    iSolveCounter :: !(IORef Int)
      }

    -- | Read-write component of the monad.
    data RW = RW
      { RW -> [(Range, Error)]
    iErrors   :: ![(Range,Error)]       -- ^ Collected errors
      , RW -> [(Range, Warning)]
    iWarnings :: ![(Range,Warning)]     -- ^ Collected warnings
      , RW -> Subst
    iSubst    :: !Subst                 -- ^ Accumulated substitution

      , RW -> [Map Name Prop]
    iExistTVars  :: [Map Name Type]
        -- ^ These keeps track of what existential type variables are available.
        -- When we start checking a function, we push a new scope for
        -- its arguments, and we pop it when we are done checking the function
        -- body. The front element of the list is the current scope, which is
        -- the only thing that will be modified, as follows.  When we encounter
        -- a existential type variable:
        --     1. we look in all scopes to see if it is already defined.
        --     2. if it was not defined, we create a fresh type variable,
        --        and we add it to the current scope.
        --     3. it is an error if we encounter an existential variable but we
        --        have no current scope.

      , RW -> Map Int HasGoalSln
    iSolvedHas :: Map Int HasGoalSln
        -- ^ Selector constraints that have been solved (ref. iSolvedSelectorsLazy)

      -- Generating names
      , RW -> NameSeeds
    iNameSeeds :: !NameSeeds

      -- Constraints that need solving
      , RW -> Goals
    iCts      :: !Goals                -- ^ Ordinary constraints
      , RW -> [HasGoal]
    iHasCts   :: ![HasGoal]
        {- ^ Tuple/record projection constraints.  The `Int` is the "name"
             of the constraint, used so that we can name it solution properly. -}

      , RW -> Supply
    iSupply :: !Supply
      }

    instance Functor InferM where
      fmap :: (a -> b) -> InferM a -> InferM b
    fmap f :: a -> b
    f (IM m :: ReaderT RO (StateT RW IO) a
    m) = ReaderT RO (StateT RW IO) b -> InferM b
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ((a -> b)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f ReaderT RO (StateT RW IO) a
    m)

    instance A.Applicative InferM where
      pure :: a -> InferM a
    pure  = a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      <*> :: InferM (a -> b) -> InferM a -> InferM b
    (<*>) = InferM (a -> b) -> InferM a -> InferM b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad InferM where
      return :: a -> InferM a
    return x :: a
    x      = ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x)
      IM m :: ReaderT RO (StateT RW IO) a
    m >>= :: InferM a -> (a -> InferM b) -> InferM b
    >>= f :: a -> InferM b
    f    = ReaderT RO (StateT RW IO) b -> InferM b
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a
    m ReaderT RO (StateT RW IO) a
    -> (a -> ReaderT RO (StateT RW IO) b)
    -> ReaderT RO (StateT RW IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= InferM b -> ReaderT RO (StateT RW IO) b
    forall a. InferM a -> ReaderT RO (StateT RW IO) a
    unIM (InferM b -> ReaderT RO (StateT RW IO) b)
    -> (a -> InferM b) -> a -> ReaderT RO (StateT RW IO) b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> InferM b
    f)

    instance MonadFail InferM where
      fail :: FilePath -> InferM a
    fail x :: FilePath
    x        = ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (FilePath -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) a. MonadFail m => FilePath -> m a
    fail FilePath
    x)

    instance MonadFix InferM where
      mfix :: (a -> InferM a) -> InferM a
    mfix f :: a -> InferM a
    f        = ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ((a -> ReaderT RO (StateT RW IO) a) -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
    mfix (InferM a -> ReaderT RO (StateT RW IO) a
    forall a. InferM a -> ReaderT RO (StateT RW IO) a
    unIM (InferM a -> ReaderT RO (StateT RW IO) a)
    -> (a -> InferM a) -> a -> ReaderT RO (StateT RW IO) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> InferM a
    f))

    instance FreshM InferM where
      liftSupply :: (Supply -> (a, Supply)) -> InferM a
    liftSupply f :: Supply -> (a, Supply)
    f = ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $
        do RW
    rw <- ReaderT RO (StateT RW IO) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
           let (a :: a
    a,s' :: Supply
    s') = Supply -> (a, Supply)
    f (RW -> Supply
    iSupply RW
    rw)
           RW -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) i. StateM m i => i -> m ()
    set RW
    rw { iSupply :: Supply
    iSupply = Supply
    s' }
           a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    io :: IO a -> InferM a
    io :: IO a -> InferM a
    io m :: IO a
    m = ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ IO a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
    inBase IO a
    m

    -- | The monadic computation is about the given range of source code.
    -- This is useful for error reporting.
    inRange :: Range -> InferM a -> InferM a
    inRange :: Range -> InferM a -> InferM a
    inRange r :: Range
    r (IM m :: ReaderT RO (StateT RW IO) a
    m) = ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\ro :: RO
    ro -> RO
    ro { iRange :: Range
    iRange = Range
    r }) ReaderT RO (StateT RW IO) a
    m

    inRangeMb :: Maybe Range -> InferM a -> InferM a
    inRangeMb :: Maybe Range -> InferM a -> InferM a
    inRangeMb Nothing m :: InferM a
    m  = InferM a
    m
    inRangeMb (Just r :: Range
    r) m :: InferM a
    m = Range -> InferM a -> InferM a
    forall a. Range -> InferM a -> InferM a
    inRange Range
    r InferM a
    m

    -- | This is the current range that we are working on.
    curRange :: InferM Range
    curRange :: InferM Range
    curRange = ReaderT RO (StateT RW IO) Range -> InferM Range
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) Range -> InferM Range)
    -> ReaderT RO (StateT RW IO) Range -> InferM Range
    forall a b. (a -> b) -> a -> b
    $ (RO -> Range) -> ReaderT RO (StateT RW IO) Range
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Range
    iRange

    -- | Report an error.
    recordError :: Error -> InferM ()
    recordError :: Error -> InferM ()
    recordError e :: Error
    e =
      do Range
    r <- InferM Range
    curRange
         ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iErrors :: [(Range, Error)]
    iErrors = (Range
    r,Error
    e) (Range, Error) -> [(Range, Error)] -> [(Range, Error)]
    forall a. a -> [a] -> [a]
    : RW -> [(Range, Error)]
    iErrors RW
    s }

    recordWarning :: Warning -> InferM ()
    recordWarning :: Warning -> InferM ()
    recordWarning w :: Warning
    w =
      Bool -> InferM () -> InferM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    ignore (InferM () -> InferM ()) -> InferM () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $
      do Range
    r <- case Warning
    w of
                DefaultingTo d :: TVarInfo
    d _ -> Range -> InferM Range
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVarInfo -> Range
    tvarSource TVarInfo
    d)
                _ -> InferM Range
    curRange
         ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iWarnings :: [(Range, Warning)]
    iWarnings = (Range
    r,Warning
    w) (Range, Warning) -> [(Range, Warning)] -> [(Range, Warning)]
    forall a. a -> [a] -> [a]
    : RW -> [(Range, Warning)]
    iWarnings RW
    s }
      where
      ignore :: Bool
    ignore
        | DefaultingTo d :: TVarInfo
    d _ <- Warning
    w
        , Just n :: Name
    n <- TVarSource -> Maybe Name
    tvSourceName (TVarInfo -> TVarSource
    tvarDesc TVarInfo
    d)
        , Declared _ SystemName <- Name -> NameInfo
    nameInfo Name
    n
          = Bool
    True
        | Bool
    otherwise = Bool
    False

    getSolver :: InferM SMT.Solver
    getSolver :: InferM Solver
    getSolver =
      do RO { .. } <- ReaderT RO (StateT RW IO) RO -> InferM RO
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         Solver -> InferM Solver
    forall (m :: * -> *) a. Monad m => a -> m a
    return Solver
    iSolver

    -- | Retrieve the mapping between identifiers and declarations in the prelude.
    getPrimMap :: InferM PrimMap
    getPrimMap :: InferM PrimMap
    getPrimMap  =
      do RO { .. } <- ReaderT RO (StateT RW IO) RO -> InferM RO
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         PrimMap -> InferM PrimMap
    forall (m :: * -> *) a. Monad m => a -> m a
    return PrimMap
    iPrimNames

    --------------------------------------------------------------------------------
    newGoal :: ConstraintSource -> Prop -> InferM Goal
    newGoal :: ConstraintSource -> Prop -> InferM Goal
    newGoal goalSource :: ConstraintSource
    goalSource goal :: Prop
    goal =
      do Range
    goalRange <- InferM Range
    curRange
         Goal -> InferM Goal
    forall (m :: * -> *) a. Monad m => a -> m a
    return Goal :: ConstraintSource -> Range -> Prop -> Goal
    Goal { .. }

    -- | Record some constraints that need to be solved.
    -- The string explains where the constraints came from.
    newGoals :: ConstraintSource -> [Prop] -> InferM ()
    newGoals :: ConstraintSource -> [Prop] -> InferM ()
    newGoals src :: ConstraintSource
    src ps :: [Prop]
    ps = [Goal] -> InferM ()
    addGoals ([Goal] -> InferM ()) -> InferM [Goal] -> InferM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Prop -> InferM Goal) -> [Prop] -> InferM [Goal]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (ConstraintSource -> Prop -> InferM Goal
    newGoal ConstraintSource
    src) [Prop]
    ps

    {- | The constraints are removed, and returned to the caller.
    The substitution IS applied to them. -}
    getGoals :: InferM [Goal]
    getGoals :: InferM [Goal]
    getGoals =
      do Goals
    goals <- Goals -> InferM Goals
    forall t. TVars t => t -> InferM t
    applySubst (Goals -> InferM Goals) -> InferM Goals -> InferM Goals
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                      ReaderT RO (StateT RW IO) Goals -> InferM Goals
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ((RW -> (Goals, RW)) -> ReaderT RO (StateT RW IO) Goals
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> (Goals, RW)) -> ReaderT RO (StateT RW IO) Goals)
    -> (RW -> (Goals, RW)) -> ReaderT RO (StateT RW IO) Goals
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> (RW -> Goals
    iCts RW
    s, RW
    s { iCts :: Goals
    iCts = Goals
    emptyGoals }))
         [Goal] -> InferM [Goal]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Goals -> [Goal]
    fromGoals Goals
    goals)

    -- | Add a bunch of goals that need solving.
    addGoals :: [Goal] -> InferM ()
    addGoals :: [Goal] -> InferM ()
    addGoals gs0 :: [Goal]
    gs0 = [Goal] -> InferM ()
    doAdd ([Goal] -> InferM ()) -> InferM [Goal] -> InferM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Goal] -> InferM [Goal]
    simpGoals [Goal]
    gs0
      where
      doAdd :: [Goal] -> InferM ()
    doAdd [] = () -> InferM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      doAdd gs :: [Goal]
    gs = ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iCts :: Goals
    iCts = (Goals -> Goal -> Goals) -> Goals -> [Goal] -> Goals
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' ((Goal -> Goals -> Goals) -> Goals -> Goal -> Goals
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Goal -> Goals -> Goals
    insertGoal) (RW -> Goals
    iCts RW
    s) [Goal]
    gs }

    -- | Collect the goals emitted by the given sub-computation.
    -- Does not emit any new goals.
    collectGoals :: InferM a -> InferM (a, [Goal])
    collectGoals :: InferM a -> InferM (a, [Goal])
    collectGoals m :: InferM a
    m =
      do Goals
    origGs <- Goals -> InferM Goals
    forall t. TVars t => t -> InferM t
    applySubst (Goals -> InferM Goals) -> InferM Goals -> InferM Goals
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InferM Goals
    getGoals'
         a
    a      <- InferM a
    m
         [Goal]
    newGs  <- InferM [Goal]
    getGoals
         Goals -> InferM ()
    setGoals' Goals
    origGs
         (a, [Goal]) -> InferM (a, [Goal])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    a, [Goal]
    newGs)

      where

      -- retrieve the type map only
      getGoals' :: InferM Goals
    getGoals'    = ReaderT RO (StateT RW IO) Goals -> InferM Goals
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) Goals -> InferM Goals)
    -> ReaderT RO (StateT RW IO) Goals -> InferM Goals
    forall a b. (a -> b) -> a -> b
    $ (RW -> (Goals, RW)) -> ReaderT RO (StateT RW IO) Goals
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> (Goals, RW)) -> ReaderT RO (StateT RW IO) Goals)
    -> (RW -> (Goals, RW)) -> ReaderT RO (StateT RW IO) Goals
    forall a b. (a -> b) -> a -> b
    $ \ RW { .. } -> (Goals
    iCts, $WRW :: [(Range, Error)]
    -> [(Range, Warning)]
    -> Subst
    -> [Map Name Prop]
    -> Map Int HasGoalSln
    -> NameSeeds
    -> Goals
    -> [HasGoal]
    -> Supply
    -> RW
    RW { iCts :: Goals
    iCts = Goals
    emptyGoals, .. })

      -- set the type map directly
      setGoals' :: Goals -> InferM ()
    setGoals' gs :: Goals
    gs = ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> ((), RW)) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> ((), RW)) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> ((), RW)) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \ RW { .. } -> ((),   $WRW :: [(Range, Error)]
    -> [(Range, Warning)]
    -> Subst
    -> [Map Name Prop]
    -> Map Int HasGoalSln
    -> NameSeeds
    -> Goals
    -> [HasGoal]
    -> Supply
    -> RW
    RW { iCts :: Goals
    iCts = Goals
    gs, .. })

    simpGoal :: Goal -> InferM [Goal]
    simpGoal :: Goal -> InferM [Goal]
    simpGoal g :: Goal
    g =
      case Ctxt -> Prop -> Prop
    Simple.simplify Ctxt
    forall k a. Map k a
    Map.empty (Goal -> Prop
    goal Goal
    g) of
        p :: Prop
    p | Just e :: TCErrorMessage
    e <- Prop -> Maybe TCErrorMessage
    tIsError Prop
    p ->
            do Error -> InferM ()
    recordError (Error -> InferM ()) -> Error -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> Error
    ErrorMsg (Doc -> Error) -> Doc -> Error
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ TCErrorMessage -> FilePath
    tcErrorMessage TCErrorMessage
    e
               [Goal] -> InferM [Goal]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          | [Prop]
    ps <- Prop -> [Prop]
    pSplitAnd Prop
    p -> [Goal] -> InferM [Goal]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Goal
    g { goal :: Prop
    goal = Prop
    pr } | Prop
    pr <- [Prop]
    ps ]

    simpGoals :: [Goal] -> InferM [Goal]
    simpGoals :: [Goal] -> InferM [Goal]
    simpGoals gs :: [Goal]
    gs = [[Goal]] -> [Goal]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Goal]] -> [Goal]) -> InferM [[Goal]] -> InferM [Goal]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Goal -> InferM [Goal]) -> [Goal] -> InferM [[Goal]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Goal -> InferM [Goal]
    simpGoal [Goal]
    gs

    {- | Record a constraint that when we select from the first type,
    we should get a value of the second type.
    The returned function should be used to wrap the expression from
    which we are selecting (i.e., the record or tuple).  Plese note
    that the resulting expression should not be forced before the
    constraint is solved.
    -}
    newHasGoal :: P.Selector -> Type -> Type -> InferM HasGoalSln
    newHasGoal :: Selector -> Prop -> Prop -> InferM HasGoalSln
    newHasGoal l :: Selector
    l ty :: Prop
    ty f :: Prop
    f =
      do Int
    goalName <- InferM Int
    newGoalName
         Goal
    g        <- ConstraintSource -> Prop -> InferM Goal
    newGoal ConstraintSource
    CtSelector (Selector -> Prop -> Prop -> Prop
    pHas Selector
    l Prop
    ty Prop
    f)
         ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iHasCts :: [HasGoal]
    iHasCts = Int -> Goal -> HasGoal
    HasGoal Int
    goalName Goal
    g HasGoal -> [HasGoal] -> [HasGoal]
    forall a. a -> [a] -> [a]
    : RW -> [HasGoal]
    iHasCts RW
    s }
         Map Int HasGoalSln
    solns    <- ReaderT RO (StateT RW IO) (Map Int HasGoalSln)
    -> InferM (Map Int HasGoalSln)
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Map Int HasGoalSln)
     -> InferM (Map Int HasGoalSln))
    -> ReaderT RO (StateT RW IO) (Map Int HasGoalSln)
    -> InferM (Map Int HasGoalSln)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Int HasGoalSln)
    -> ReaderT RO (StateT RW IO) RO
    -> ReaderT RO (StateT RW IO) (Map Int HasGoalSln)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RO -> Map Int HasGoalSln
    iSolvedHasLazy ReaderT RO (StateT RW IO) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         HasGoalSln -> InferM HasGoalSln
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HasGoalSln -> InferM HasGoalSln)
    -> HasGoalSln -> InferM HasGoalSln
    forall a b. (a -> b) -> a -> b
    $ case Int -> Map Int HasGoalSln -> Maybe HasGoalSln
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Int
    goalName Map Int HasGoalSln
    solns of
                    Just e1 :: HasGoalSln
    e1 -> HasGoalSln
    e1
                    Nothing -> FilePath -> [FilePath] -> HasGoalSln
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "newHasGoal" ["Unsolved has goal in result"]

    -- | Add a previously generate has constrained
    addHasGoal :: HasGoal -> InferM ()
    addHasGoal :: HasGoal -> InferM ()
    addHasGoal g :: HasGoal
    g = ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iHasCts :: [HasGoal]
    iHasCts = HasGoal
    g HasGoal -> [HasGoal] -> [HasGoal]
    forall a. a -> [a] -> [a]
    : RW -> [HasGoal]
    iHasCts RW
    s }

    -- | Get the `Has` constraints.  Each of this should either be solved,
    -- or added back using `addHasGoal`.
    getHasGoals :: InferM [HasGoal]
    getHasGoals :: InferM [HasGoal]
    getHasGoals = do [HasGoal]
    gs <- ReaderT RO (StateT RW IO) [HasGoal] -> InferM [HasGoal]
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) [HasGoal] -> InferM [HasGoal])
    -> ReaderT RO (StateT RW IO) [HasGoal] -> InferM [HasGoal]
    forall a b. (a -> b) -> a -> b
    $ (RW -> ([HasGoal], RW)) -> ReaderT RO (StateT RW IO) [HasGoal]
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> ([HasGoal], RW)) -> ReaderT RO (StateT RW IO) [HasGoal])
    -> (RW -> ([HasGoal], RW)) -> ReaderT RO (StateT RW IO) [HasGoal]
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> (RW -> [HasGoal]
    iHasCts RW
    s, RW
    s { iHasCts :: [HasGoal]
    iHasCts = [] })
                     [HasGoal] -> InferM [HasGoal]
    forall t. TVars t => t -> InferM t
    applySubst [HasGoal]
    gs

    -- | Specify the solution (`Expr -> Expr`) for the given constraint (`Int`).
    solveHasGoal :: Int -> HasGoalSln -> InferM ()
    solveHasGoal :: Int -> HasGoalSln -> InferM ()
    solveHasGoal n :: Int
    n e :: HasGoalSln
    e =
      ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iSolvedHas :: Map Int HasGoalSln
    iSolvedHas = Int -> HasGoalSln -> Map Int HasGoalSln -> Map Int HasGoalSln
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Int
    n HasGoalSln
    e (RW -> Map Int HasGoalSln
    iSolvedHas RW
    s) }

    --------------------------------------------------------------------------------

    -- | Generate a fresh variable name to be used in a local binding.
    newParamName :: Ident -> InferM Name
    newParamName :: Ident -> InferM Name
    newParamName x :: Ident
    x =
      do Range
    r <- InferM Range
    curRange
         (Supply -> (Name, Supply)) -> InferM Name
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply (Ident -> Range -> Supply -> (Name, Supply)
    mkParameter Ident
    x Range
    r)

    newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a
    newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a
    newName upd :: NameSeeds -> (a, NameSeeds)
    upd = ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RW -> (a, RW)) -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> (a, RW)) -> ReaderT RO (StateT RW IO) a)
    -> (RW -> (a, RW)) -> ReaderT RO (StateT RW IO) a
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> let (x :: a
    x,seeds :: NameSeeds
    seeds) = NameSeeds -> (a, NameSeeds)
    upd (RW -> NameSeeds
    iNameSeeds RW
    s)
                                    in (a
    x, RW
    s { iNameSeeds :: NameSeeds
    iNameSeeds = NameSeeds
    seeds })

    -- | Generate a new name for a goal.
    newGoalName :: InferM Int
    newGoalName :: InferM Int
    newGoalName = (NameSeeds -> (Int, NameSeeds)) -> InferM Int
    forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
    newName ((NameSeeds -> (Int, NameSeeds)) -> InferM Int)
    -> (NameSeeds -> (Int, NameSeeds)) -> InferM Int
    forall a b. (a -> b) -> a -> b
    $ \s :: NameSeeds
    s -> let x :: Int
    x = NameSeeds -> Int
    seedGoal NameSeeds
    s
                                  in (Int
    x, NameSeeds
    s { seedGoal :: Int
    seedGoal = Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1})

    -- | Generate a new free type variable.
    newTVar :: TVarSource -> Kind -> InferM TVar
    newTVar :: TVarSource -> Kind -> InferM TVar
    newTVar src :: TVarSource
    src k :: Kind
    k = TVarSource -> Set TParam -> Kind -> InferM TVar
    newTVar' TVarSource
    src Set TParam
    forall a. Set a
    Set.empty Kind
    k

    -- | Generate a new free type variable that depends on these additional
    -- type parameters.
    newTVar' :: TVarSource -> Set TParam -> Kind -> InferM TVar
    newTVar' :: TVarSource -> Set TParam -> Kind -> InferM TVar
    newTVar' src :: TVarSource
    src extraBound :: Set TParam
    extraBound k :: Kind
    k =
      do Range
    r <- InferM Range
    curRange
         Set TParam
    bound <- InferM (Set TParam)
    getBoundInScope
         let vs :: Set TParam
    vs = Set TParam -> Set TParam -> Set TParam
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set TParam
    extraBound Set TParam
    bound
             msg :: TVarInfo
    msg = TVarInfo :: Range -> TVarSource -> TVarInfo
    TVarInfo { tvarDesc :: TVarSource
    tvarDesc = TVarSource
    src, tvarSource :: Range
    tvarSource = Range
    r }
         (NameSeeds -> (TVar, NameSeeds)) -> InferM TVar
    forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
    newName ((NameSeeds -> (TVar, NameSeeds)) -> InferM TVar)
    -> (NameSeeds -> (TVar, NameSeeds)) -> InferM TVar
    forall a b. (a -> b) -> a -> b
    $ \s :: NameSeeds
    s -> let x :: Int
    x = NameSeeds -> Int
    seedTVar NameSeeds
    s
                         in (Int -> Kind -> Set TParam -> TVarInfo -> TVar
    TVFree Int
    x Kind
    k Set TParam
    vs TVarInfo
    msg, NameSeeds
    s { seedTVar :: Int
    seedTVar = Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 })

    -- | Generate a new free type variable.
    newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam
    newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam
    newTParam nm :: TParam Name
    nm flav :: TPFlavor
    flav k :: Kind
    k = (NameSeeds -> (TParam, NameSeeds)) -> InferM TParam
    forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
    newName ((NameSeeds -> (TParam, NameSeeds)) -> InferM TParam)
    -> (NameSeeds -> (TParam, NameSeeds)) -> InferM TParam
    forall a b. (a -> b) -> a -> b
    $ \s :: NameSeeds
    s ->
      let x :: Int
    x = NameSeeds -> Int
    seedTVar NameSeeds
    s
      in ($WTParam :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
    TParam { tpUnique :: Int
    tpUnique = Int
    x
                , tpKind :: Kind
    tpKind   = Kind
    k
                , tpFlav :: TPFlavor
    tpFlav   = TPFlavor
    flav
                , tpInfo :: TVarInfo
    tpInfo   = TVarInfo
    desc
                }
         , NameSeeds
    s { seedTVar :: Int
    seedTVar = Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 })
      where desc :: TVarInfo
    desc = TVarInfo :: Range -> TVarSource -> TVarInfo
    TVarInfo { tvarDesc :: TVarSource
    tvarDesc = Name -> TVarSource
    TVFromSignature (TParam Name -> Name
    forall n. TParam n -> n
    P.tpName TParam Name
    nm)
                            , tvarSource :: Range
    tvarSource = Range -> Maybe Range -> Range
    forall a. a -> Maybe a -> a
    fromMaybe Range
    emptyRange (TParam Name -> Maybe Range
    forall n. TParam n -> Maybe Range
    P.tpRange TParam Name
    nm)
                            }

    -- | Generate an unknown type.  The doc is a note about what is this type about.
    newType :: TVarSource -> Kind -> InferM Type
    newType :: TVarSource -> Kind -> InferM Prop
    newType src :: TVarSource
    src k :: Kind
    k = TVar -> Prop
    TVar (TVar -> Prop) -> InferM TVar -> InferM Prop
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` TVarSource -> Kind -> InferM TVar
    newTVar TVarSource
    src Kind
    k

    --------------------------------------------------------------------------------

    -- | Record that the two types should be syntactically equal.
    unify :: Type -> Type -> InferM [Prop]
    unify :: Prop -> Prop -> InferM [Prop]
    unify t1 :: Prop
    t1 t2 :: Prop
    t2 =
      do Prop
    t1' <- Prop -> InferM Prop
    forall t. TVars t => t -> InferM t
    applySubst Prop
    t1
         Prop
    t2' <- Prop -> InferM Prop
    forall t. TVars t => t -> InferM t
    applySubst Prop
    t2
         let ((su1 :: Subst
    su1, ps :: [Prop]
    ps), errs :: [UnificationError]
    errs) = Result (Subst, [Prop]) -> ((Subst, [Prop]), [UnificationError])
    forall a. Result a -> (a, [UnificationError])
    runResult (Prop -> Prop -> Result (Subst, [Prop])
    mgu Prop
    t1' Prop
    t2')
         Subst -> InferM ()
    extendSubst Subst
    su1
         let toError :: UnificationError -> Error
             toError :: UnificationError -> Error
    toError err :: UnificationError
    err =
               case UnificationError
    err of
                 UniTypeLenMismatch _ _ -> Prop -> Prop -> Error
    TypeMismatch Prop
    t1' Prop
    t2'
                 UniTypeMismatch s1 :: Prop
    s1 s2 :: Prop
    s2  -> Prop -> Prop -> Error
    TypeMismatch Prop
    s1 Prop
    s2
                 UniKindMismatch k1 :: Kind
    k1 k2 :: Kind
    k2  -> Kind -> Kind -> Error
    KindMismatch Kind
    k1 Kind
    k2
                 UniRecursive x :: TVar
    x t :: Prop
    t       -> Prop -> Prop -> Error
    RecursiveType (TVar -> Prop
    TVar TVar
    x) Prop
    t
                 UniNonPolyDepends x :: TVar
    x vs :: [TParam]
    vs -> Prop -> [TParam] -> Error
    TypeVariableEscaped (TVar -> Prop
    TVar TVar
    x) [TParam]
    vs
                 UniNonPoly x :: TVar
    x t :: Prop
    t         -> TVar -> Prop -> Error
    NotForAll TVar
    x Prop
    t
         case [UnificationError]
    errs of
           [] -> [Prop] -> InferM [Prop]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Prop]
    ps
           _  -> do (UnificationError -> InferM ()) -> [UnificationError] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Error -> InferM ()
    recordError (Error -> InferM ())
    -> (UnificationError -> Error) -> UnificationError -> InferM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . UnificationError -> Error
    toError) [UnificationError]
    errs
                    [Prop] -> InferM [Prop]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    -- | Apply the accumulated substitution to something with free type variables.
    applySubst :: TVars t => t -> InferM t
    applySubst :: t -> InferM t
    applySubst t :: t
    t =
      do Subst
    su <- InferM Subst
    getSubst
         t -> InferM t
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Subst -> t -> t
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su t
    t)

    applySubstPreds :: [Prop] -> InferM [Prop]
    applySubstPreds :: [Prop] -> InferM [Prop]
    applySubstPreds ps :: [Prop]
    ps =
      do [Prop]
    ps1 <- [Prop] -> InferM [Prop]
    forall t. TVars t => t -> InferM t
    applySubst [Prop]
    ps
         [Prop] -> InferM [Prop]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Prop -> [Prop]) -> [Prop] -> [Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Prop -> [Prop]
    pSplitAnd [Prop]
    ps1)

    applySubstGoals :: [Goal] -> InferM [Goal]
    applySubstGoals :: [Goal] -> InferM [Goal]
    applySubstGoals gs :: [Goal]
    gs =
      do [Goal]
    gs1 <- [Goal] -> InferM [Goal]
    forall t. TVars t => t -> InferM t
    applySubst [Goal]
    gs
         [Goal] -> InferM [Goal]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Goal
    g { goal :: Prop
    goal = Prop
    p } | Goal
    g <- [Goal]
    gs1, Prop
    p <- Prop -> [Prop]
    pSplitAnd (Goal -> Prop
    goal Goal
    g) ]

    -- | Get the substitution that we have accumulated so far.
    getSubst :: InferM Subst
    getSubst :: InferM Subst
    getSubst = ReaderT RO (StateT RW IO) Subst -> InferM Subst
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) Subst -> InferM Subst)
    -> ReaderT RO (StateT RW IO) Subst -> InferM Subst
    forall a b. (a -> b) -> a -> b
    $ (RW -> Subst)
    -> ReaderT RO (StateT RW IO) RW -> ReaderT RO (StateT RW IO) Subst
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RW -> Subst
    iSubst ReaderT RO (StateT RW IO) RW
    forall (m :: * -> *) i. StateM m i => m i
    get

    -- | Add to the accumulated substitution, checking that the datatype
    -- invariant for `Subst` is maintained.
    extendSubst :: Subst -> InferM ()
    extendSubst :: Subst -> InferM ()
    extendSubst su :: Subst
    su =
      do ((TVar, Prop) -> InferM ()) -> [(TVar, Prop)] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (TVar, Prop) -> InferM ()
    check (Subst -> [(TVar, Prop)]
    substToList Subst
    su)
         ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iSubst :: Subst
    iSubst = Subst
    su Subst -> Subst -> Subst
    @@ RW -> Subst
    iSubst RW
    s }
      where
        check :: (TVar, Type) -> InferM ()
        check :: (TVar, Prop) -> InferM ()
    check (v :: TVar
    v, ty :: Prop
    ty) =
          case TVar
    v of
            TVBound _ ->
              FilePath -> [FilePath] -> InferM ()
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "Cryptol.TypeCheck.Monad.extendSubst"
                [ "Substitution instantiates bound variable:"
                , "Variable: " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (TVar -> Doc
    forall a. PP a => a -> Doc
    pp TVar
    v)
                , "Type:     " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (Prop -> Doc
    forall a. PP a => a -> Doc
    pp Prop
    ty)
                ]
            TVFree _ _ tvs :: Set TParam
    tvs _ ->
              do let bounds :: TVar -> Set TParam
    bounds tv :: TVar
    tv =
                       case TVar
    tv of
                         TVBound tp :: TParam
    tp -> TParam -> Set TParam
    forall a. a -> Set a
    Set.singleton TParam
    tp
                         TVFree _ _ tps :: Set TParam
    tps _ -> Set TParam
    tps
                 let vars :: Set TParam
    vars = [Set TParam] -> Set TParam
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ((TVar -> Set TParam) -> [TVar] -> [Set TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map TVar -> Set TParam
    bounds (Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.elems (Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Prop
    ty)))
                     -- (Set.filter isBoundTV (fvs ty))
                 let escaped :: Set TParam
    escaped = Set TParam -> Set TParam -> Set TParam
    forall a. Ord a => Set a -> Set a -> Set a
    Set.difference Set TParam
    vars Set TParam
    tvs
                 if Set TParam -> Bool
    forall a. Set a -> Bool
    Set.null Set TParam
    escaped then () -> InferM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return () else
                   FilePath -> [FilePath] -> InferM ()
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "Cryptol.TypeCheck.Monad.extendSubst"
                     [ "Escaped quantified variables:"
                     , "Substitution:  " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (TVar -> Doc
    forall a. PP a => a -> Doc
    pp TVar
    v Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ":=" Doc -> Doc -> Doc
    <+> Prop -> Doc
    forall a. PP a => a -> Doc
    pp Prop
    ty)
                     , "Vars in scope: " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (Doc -> Doc
    brackets ([Doc] -> Doc
    commaSep ((TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> Doc
    forall a. PP a => a -> Doc
    pp (Set TParam -> [TParam]
    forall a. Set a -> [a]
    Set.toList Set TParam
    tvs))))
                     , "Escaped:       " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (Doc -> Doc
    brackets ([Doc] -> Doc
    commaSep ((TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> Doc
    forall a. PP a => a -> Doc
    pp (Set TParam -> [TParam]
    forall a. Set a -> [a]
    Set.toList Set TParam
    escaped))))
                     ]

    -- | Variables that are either mentioned in the environment or in
    -- a selector constraint.
    varsWithAsmps :: InferM (Set TVar)
    varsWithAsmps :: InferM (Set TVar)
    varsWithAsmps =
      do [VarType]
    env     <- ReaderT RO (StateT RW IO) [VarType] -> InferM [VarType]
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) [VarType] -> InferM [VarType])
    -> ReaderT RO (StateT RW IO) [VarType] -> InferM [VarType]
    forall a b. (a -> b) -> a -> b
    $ (RO -> [VarType])
    -> ReaderT RO (StateT RW IO) RO
    -> ReaderT RO (StateT RW IO) [VarType]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Map Name VarType -> [VarType]
    forall k a. Map k a -> [a]
    Map.elems (Map Name VarType -> [VarType])
    -> (RO -> Map Name VarType) -> RO -> [VarType]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RO -> Map Name VarType
    iVars) ReaderT RO (StateT RW IO) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         [Set TVar]
    fromEnv <- [VarType] -> (VarType -> InferM (Set TVar)) -> InferM [Set TVar]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [VarType]
    env ((VarType -> InferM (Set TVar)) -> InferM [Set TVar])
    -> (VarType -> InferM (Set TVar)) -> InferM [Set TVar]
    forall a b. (a -> b) -> a -> b
    $ \v :: VarType
    v ->
                      case VarType
    v of
                        ExtVar sch :: Schema
    sch  -> Schema -> InferM (Set TVar)
    forall t. (FVS t, TVars t) => t -> InferM (Set TVar)
    getVars Schema
    sch
                        CurSCC _ t :: Prop
    t  -> Prop -> InferM (Set TVar)
    forall t. (FVS t, TVars t) => t -> InferM (Set TVar)
    getVars Prop
    t
         [Prop]
    sels <- ReaderT RO (StateT RW IO) [Prop] -> InferM [Prop]
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) [Prop] -> InferM [Prop])
    -> ReaderT RO (StateT RW IO) [Prop] -> InferM [Prop]
    forall a b. (a -> b) -> a -> b
    $ (RW -> [Prop])
    -> ReaderT RO (StateT RW IO) RW -> ReaderT RO (StateT RW IO) [Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((HasGoal -> Prop) -> [HasGoal] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Goal -> Prop
    goal (Goal -> Prop) -> (HasGoal -> Goal) -> HasGoal -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HasGoal -> Goal
    hasGoal) ([HasGoal] -> [Prop]) -> (RW -> [HasGoal]) -> RW -> [Prop]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RW -> [HasGoal]
    iHasCts) ReaderT RO (StateT RW IO) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         [Set TVar]
    fromSels <- (Prop -> InferM (Set TVar)) -> [Prop] -> InferM [Set TVar]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Prop -> InferM (Set TVar)
    forall t. (FVS t, TVars t) => t -> InferM (Set TVar)
    getVars [Prop]
    sels
         Set TVar
    fromEx   <- ([Prop] -> InferM (Set TVar)
    forall t. (FVS t, TVars t) => t -> InferM (Set TVar)
    getVars ([Prop] -> InferM (Set TVar))
    -> ([Map Name Prop] -> [Prop])
    -> [Map Name Prop]
    -> InferM (Set TVar)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Map Name Prop -> [Prop]) -> [Map Name Prop] -> [Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Map Name Prop -> [Prop]
    forall k a. Map k a -> [a]
    Map.elems) ([Map Name Prop] -> InferM (Set TVar))
    -> InferM [Map Name Prop] -> InferM (Set TVar)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT RO (StateT RW IO) [Map Name Prop] -> InferM [Map Name Prop]
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ((RW -> [Map Name Prop])
    -> ReaderT RO (StateT RW IO) RW
    -> ReaderT RO (StateT RW IO) [Map Name Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RW -> [Map Name Prop]
    iExistTVars ReaderT RO (StateT RW IO) RW
    forall (m :: * -> *) i. StateM m i => m i
    get)
         Set TVar -> InferM (Set TVar)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Set TVar] -> Set TVar
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions [Set TVar]
    fromEnv Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` [Set TVar] -> Set TVar
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions [Set TVar]
    fromSels
                                    Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set TVar
    fromEx)
      where
      getVars :: t -> InferM (Set TVar)
    getVars x :: t
    x = t -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (t -> Set TVar) -> InferM t -> InferM (Set TVar)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` t -> InferM t
    forall t. TVars t => t -> InferM t
    applySubst t
    x

    --------------------------------------------------------------------------------

    -- | Lookup the type of a variable.
    lookupVar :: Name -> InferM VarType
    lookupVar :: Name -> InferM VarType
    lookupVar x :: Name
    x =
      do Maybe VarType
    mb <- ReaderT RO (StateT RW IO) (Maybe VarType) -> InferM (Maybe VarType)
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Maybe VarType)
     -> InferM (Maybe VarType))
    -> ReaderT RO (StateT RW IO) (Maybe VarType)
    -> InferM (Maybe VarType)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Maybe VarType) -> ReaderT RO (StateT RW IO) (Maybe VarType)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks ((RO -> Maybe VarType)
     -> ReaderT RO (StateT RW IO) (Maybe VarType))
    -> (RO -> Maybe VarType)
    -> ReaderT RO (StateT RW IO) (Maybe VarType)
    forall a b. (a -> b) -> a -> b
    $ Name -> Map Name VarType -> Maybe VarType
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name VarType -> Maybe VarType)
    -> (RO -> Map Name VarType) -> RO -> Maybe VarType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RO -> Map Name VarType
    iVars
         case Maybe VarType
    mb of
           Just t :: VarType
    t  -> VarType -> InferM VarType
    forall (m :: * -> *) a. Monad m => a -> m a
    return VarType
    t
           Nothing ->
             do Maybe Newtype
    mbNT <- Name -> InferM (Maybe Newtype)
    lookupNewtype Name
    x
                case Maybe Newtype
    mbNT of
                  Just nt :: Newtype
    nt -> VarType -> InferM VarType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> VarType
    ExtVar (Newtype -> Schema
    newtypeConType Newtype
    nt))
                  Nothing ->
                    do Maybe ModVParam
    mbParamFun <- Name -> InferM (Maybe ModVParam)
    lookupParamFun Name
    x
                       case Maybe ModVParam
    mbParamFun of
                         Just pf :: ModVParam
    pf -> VarType -> InferM VarType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> VarType
    ExtVar (ModVParam -> Schema
    mvpType ModVParam
    pf))
                         Nothing -> FilePath -> [FilePath] -> InferM VarType
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "lookupVar" [ "Undefined type variable"
                                                      , Name -> FilePath
    forall a. Show a => a -> FilePath
    show Name
    x]

    -- | Lookup a type variable.  Return `Nothing` if there is no such variable
    -- in scope, in which case we must be dealing with a type constant.
    lookupTParam :: Name -> InferM (Maybe TParam)
    lookupTParam :: Name -> InferM (Maybe TParam)
    lookupTParam x :: Name
    x = ReaderT RO (StateT RW IO) (Maybe TParam) -> InferM (Maybe TParam)
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Maybe TParam) -> InferM (Maybe TParam))
    -> ReaderT RO (StateT RW IO) (Maybe TParam)
    -> InferM (Maybe TParam)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Maybe TParam) -> ReaderT RO (StateT RW IO) (Maybe TParam)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks ((RO -> Maybe TParam) -> ReaderT RO (StateT RW IO) (Maybe TParam))
    -> (RO -> Maybe TParam) -> ReaderT RO (StateT RW IO) (Maybe TParam)
    forall a b. (a -> b) -> a -> b
    $ (TParam -> Bool) -> [TParam] -> Maybe TParam
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find TParam -> Bool
    this ([TParam] -> Maybe TParam)
    -> (RO -> [TParam]) -> RO -> Maybe TParam
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RO -> [TParam]
    iTVars
      where this :: TParam -> Bool
    this tp :: TParam
    tp = TParam -> Maybe Name
    tpName TParam
    tp Maybe Name -> Maybe Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x

    -- | Lookup the definition of a type synonym.
    lookupTSyn :: Name -> InferM (Maybe TySyn)
    lookupTSyn :: Name -> InferM (Maybe TySyn)
    lookupTSyn x :: Name
    x = (Map Name (DefLoc, TySyn) -> Maybe TySyn)
    -> InferM (Map Name (DefLoc, TySyn)) -> InferM (Maybe TySyn)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((DefLoc, TySyn) -> TySyn) -> Maybe (DefLoc, TySyn) -> Maybe TySyn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (DefLoc, TySyn) -> TySyn
    forall a b. (a, b) -> b
    snd (Maybe (DefLoc, TySyn) -> Maybe TySyn)
    -> (Map Name (DefLoc, TySyn) -> Maybe (DefLoc, TySyn))
    -> Map Name (DefLoc, TySyn)
    -> Maybe TySyn
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Map Name (DefLoc, TySyn) -> Maybe (DefLoc, TySyn)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x) InferM (Map Name (DefLoc, TySyn))
    getTSyns

    -- | Lookup the definition of a newtype
    lookupNewtype :: Name -> InferM (Maybe Newtype)
    lookupNewtype :: Name -> InferM (Maybe Newtype)
    lookupNewtype x :: Name
    x = (Map Name (DefLoc, Newtype) -> Maybe Newtype)
    -> InferM (Map Name (DefLoc, Newtype)) -> InferM (Maybe Newtype)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((DefLoc, Newtype) -> Newtype)
    -> Maybe (DefLoc, Newtype) -> Maybe Newtype
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (DefLoc, Newtype) -> Newtype
    forall a b. (a, b) -> b
    snd (Maybe (DefLoc, Newtype) -> Maybe Newtype)
    -> (Map Name (DefLoc, Newtype) -> Maybe (DefLoc, Newtype))
    -> Map Name (DefLoc, Newtype)
    -> Maybe Newtype
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Map Name (DefLoc, Newtype) -> Maybe (DefLoc, Newtype)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x) InferM (Map Name (DefLoc, Newtype))
    getNewtypes

    lookupAbstractType :: Name -> InferM (Maybe AbstractType)
    lookupAbstractType :: Name -> InferM (Maybe AbstractType)
    lookupAbstractType x :: Name
    x = (Map Name (DefLoc, AbstractType) -> Maybe AbstractType)
    -> InferM (Map Name (DefLoc, AbstractType))
    -> InferM (Maybe AbstractType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((DefLoc, AbstractType) -> AbstractType)
    -> Maybe (DefLoc, AbstractType) -> Maybe AbstractType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (DefLoc, AbstractType) -> AbstractType
    forall a b. (a, b) -> b
    snd (Maybe (DefLoc, AbstractType) -> Maybe AbstractType)
    -> (Map Name (DefLoc, AbstractType)
        -> Maybe (DefLoc, AbstractType))
    -> Map Name (DefLoc, AbstractType)
    -> Maybe AbstractType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name
    -> Map Name (DefLoc, AbstractType) -> Maybe (DefLoc, AbstractType)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x) InferM (Map Name (DefLoc, AbstractType))
    getAbstractTypes

    -- | Lookup the kind of a parameter type
    lookupParamType :: Name -> InferM (Maybe ModTParam)
    lookupParamType :: Name -> InferM (Maybe ModTParam)
    lookupParamType x :: Name
    x = Name -> Map Name ModTParam -> Maybe ModTParam
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name ModTParam -> Maybe ModTParam)
    -> InferM (Map Name ModTParam) -> InferM (Maybe ModTParam)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (Map Name ModTParam)
    getParamTypes

    -- | Lookup the schema for a parameter function.
    lookupParamFun :: Name -> InferM (Maybe ModVParam)
    lookupParamFun :: Name -> InferM (Maybe ModVParam)
    lookupParamFun x :: Name
    x = Name -> Map Name ModVParam -> Maybe ModVParam
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name ModVParam -> Maybe ModVParam)
    -> InferM (Map Name ModVParam) -> InferM (Maybe ModVParam)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (Map Name ModVParam)
    getParamFuns

    -- | Check if we already have a name for this existential type variable and,
    -- if so, return the definition.  If not, try to create a new definition,
    -- if this is allowed.  If not, returns nothing.

    existVar :: Name -> Kind -> InferM Type
    existVar :: Name -> Kind -> InferM Prop
    existVar x :: Name
    x k :: Kind
    k =
      do [Map Name Prop]
    scopes <- RW -> [Map Name Prop]
    iExistTVars (RW -> [Map Name Prop]) -> InferM RW -> InferM [Map Name Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT RO (StateT RW IO) RW -> InferM RW
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         case [Maybe Prop] -> Maybe Prop
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ((Map Name Prop -> Maybe Prop) -> [Map Name Prop] -> [Maybe Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Map Name Prop -> Maybe Prop
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x) [Map Name Prop]
    scopes) of
           Just ty :: Prop
    ty -> Prop -> InferM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    ty
           Nothing ->
             case [Map Name Prop]
    scopes of
               [] ->
                  do Error -> InferM ()
    recordError (Error -> InferM ()) -> Error -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> Error
    ErrorMsg
                                 (Doc -> Error) -> Doc -> Error
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Doc
    text "Undefined type" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x)
                                        Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text (Name -> FilePath
    forall a. Show a => a -> FilePath
    show Name
    x)
                     TVarSource -> Kind -> InferM Prop
    newType TVarSource
    TypeErrorPlaceHolder Kind
    k

               sc :: Map Name Prop
    sc : more :: [Map Name Prop]
    more ->
                 do Prop
    ty <- TVarSource -> Kind -> InferM Prop
    newType TVarSource
    TypeErrorPlaceHolder Kind
    k
                    ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s{ iExistTVars :: [Map Name Prop]
    iExistTVars = Name -> Prop -> Map Name Prop -> Map Name Prop
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    x Prop
    ty Map Name Prop
    sc Map Name Prop -> [Map Name Prop] -> [Map Name Prop]
    forall a. a -> [a] -> [a]
    : [Map Name Prop]
    more }
                    Prop -> InferM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    ty

    -- | Returns the type synonyms that are currently in scope.
    getTSyns :: InferM (Map Name (DefLoc,TySyn))
    getTSyns :: InferM (Map Name (DefLoc, TySyn))
    getTSyns = ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
    -> InferM (Map Name (DefLoc, TySyn))
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
     -> InferM (Map Name (DefLoc, TySyn)))
    -> ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
    -> InferM (Map Name (DefLoc, TySyn))
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Name (DefLoc, TySyn))
    -> ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Map Name (DefLoc, TySyn)
    iTSyns

    -- | Returns the newtype declarations that are in scope.
    getNewtypes :: InferM (Map Name (DefLoc,Newtype))
    getNewtypes :: InferM (Map Name (DefLoc, Newtype))
    getNewtypes = ReaderT RO (StateT RW IO) (Map Name (DefLoc, Newtype))
    -> InferM (Map Name (DefLoc, Newtype))
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Map Name (DefLoc, Newtype))
     -> InferM (Map Name (DefLoc, Newtype)))
    -> ReaderT RO (StateT RW IO) (Map Name (DefLoc, Newtype))
    -> InferM (Map Name (DefLoc, Newtype))
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Name (DefLoc, Newtype))
    -> ReaderT RO (StateT RW IO) (Map Name (DefLoc, Newtype))
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Map Name (DefLoc, Newtype)
    iNewtypes

    -- | Returns the abstract type declarations that are in scope.
    getAbstractTypes :: InferM (Map Name (DefLoc,AbstractType))
    getAbstractTypes :: InferM (Map Name (DefLoc, AbstractType))
    getAbstractTypes = ReaderT RO (StateT RW IO) (Map Name (DefLoc, AbstractType))
    -> InferM (Map Name (DefLoc, AbstractType))
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Map Name (DefLoc, AbstractType))
     -> InferM (Map Name (DefLoc, AbstractType)))
    -> ReaderT RO (StateT RW IO) (Map Name (DefLoc, AbstractType))
    -> InferM (Map Name (DefLoc, AbstractType))
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Name (DefLoc, AbstractType))
    -> ReaderT RO (StateT RW IO) (Map Name (DefLoc, AbstractType))
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Map Name (DefLoc, AbstractType)
    iAbstractTypes

    -- | Returns the parameter functions declarations
    getParamFuns :: InferM (Map Name ModVParam)
    getParamFuns :: InferM (Map Name ModVParam)
    getParamFuns = ReaderT RO (StateT RW IO) (Map Name ModVParam)
    -> InferM (Map Name ModVParam)
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Map Name ModVParam)
     -> InferM (Map Name ModVParam))
    -> ReaderT RO (StateT RW IO) (Map Name ModVParam)
    -> InferM (Map Name ModVParam)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Name ModVParam)
    -> ReaderT RO (StateT RW IO) (Map Name ModVParam)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Map Name ModVParam
    iParamFuns

    -- | Returns the abstract function declarations
    getParamTypes :: InferM (Map Name ModTParam)
    getParamTypes :: InferM (Map Name ModTParam)
    getParamTypes = ReaderT RO (StateT RW IO) (Map Name ModTParam)
    -> InferM (Map Name ModTParam)
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Map Name ModTParam)
     -> InferM (Map Name ModTParam))
    -> ReaderT RO (StateT RW IO) (Map Name ModTParam)
    -> InferM (Map Name ModTParam)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Name ModTParam)
    -> ReaderT RO (StateT RW IO) (Map Name ModTParam)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Map Name ModTParam
    iParamTypes

    -- | Constraints on the module's parameters.
    getParamConstraints :: InferM [Located Prop]
    getParamConstraints :: InferM [Located Prop]
    getParamConstraints = ReaderT RO (StateT RW IO) [Located Prop] -> InferM [Located Prop]
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) [Located Prop] -> InferM [Located Prop])
    -> ReaderT RO (StateT RW IO) [Located Prop]
    -> InferM [Located Prop]
    forall a b. (a -> b) -> a -> b
    $ (RO -> [Located Prop]) -> ReaderT RO (StateT RW IO) [Located Prop]
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> [Located Prop]
    iParamConstraints

    -- | Get the set of bound type variables that are in scope.
    getTVars :: InferM (Set Name)
    getTVars :: InferM (Set Name)
    getTVars = ReaderT RO (StateT RW IO) (Set Name) -> InferM (Set Name)
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) (Set Name) -> InferM (Set Name))
    -> ReaderT RO (StateT RW IO) (Set Name) -> InferM (Set Name)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Set Name) -> ReaderT RO (StateT RW IO) (Set Name)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks ((RO -> Set Name) -> ReaderT RO (StateT RW IO) (Set Name))
    -> (RO -> Set Name) -> ReaderT RO (StateT RW IO) (Set Name)
    forall a b. (a -> b) -> a -> b
    $ [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Name] -> Set Name) -> (RO -> [Name]) -> RO -> Set Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TParam -> Maybe Name) -> [TParam] -> [Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe TParam -> Maybe Name
    tpName ([TParam] -> [Name]) -> (RO -> [TParam]) -> RO -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RO -> [TParam]
    iTVars

    -- | Return the keys of the bound variables that are in scope.
    getBoundInScope :: InferM (Set TParam)
    getBoundInScope :: InferM (Set TParam)
    getBoundInScope =
      do RO
    ro <- ReaderT RO (StateT RW IO) RO -> InferM RO
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         let params :: Set TParam
    params = [TParam] -> Set TParam
    forall a. Ord a => [a] -> Set a
    Set.fromList ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> TParam
    mtpParam (Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems (RO -> Map Name ModTParam
    iParamTypes RO
    ro)))
             bound :: Set TParam
    bound  = [TParam] -> Set TParam
    forall a. Ord a => [a] -> Set a
    Set.fromList (RO -> [TParam]
    iTVars RO
    ro)
         Set TParam -> InferM (Set TParam)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set TParam -> InferM (Set TParam))
    -> Set TParam -> InferM (Set TParam)
    forall a b. (a -> b) -> a -> b
    $! Set TParam -> Set TParam -> Set TParam
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set TParam
    params Set TParam
    bound

    -- | Retrieve the value of the `mono-binds` option.
    getMonoBinds :: InferM Bool
    getMonoBinds :: InferM Bool
    getMonoBinds  = ReaderT RO (StateT RW IO) Bool -> InferM Bool
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ((RO -> Bool) -> ReaderT RO (StateT RW IO) Bool
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Bool
    iMonoBinds)

    {- | We disallow shadowing between type synonyms and type variables
    because it is confusing.  As a bonus, in the implementation we don't
    need to worry about where we lookup things (i.e., in the variable or
    type synonym environment. -}

    checkTShadowing :: String -> Name -> InferM ()
    checkTShadowing :: FilePath -> Name -> InferM ()
    checkTShadowing this :: FilePath
    this new :: Name
    new =
      do RO
    ro <- ReaderT RO (StateT RW IO) RO -> InferM RO
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RW
    rw <- ReaderT RO (StateT RW IO) RW -> InferM RW
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         let shadowed :: Maybe FilePath
    shadowed =
               do (DefLoc, TySyn)
    _ <- Name -> Map Name (DefLoc, TySyn) -> Maybe (DefLoc, TySyn)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    new (RO -> Map Name (DefLoc, TySyn)
    iTSyns RO
    ro)
                  FilePath -> Maybe FilePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return "type synonym"
               Maybe FilePath -> Maybe FilePath -> Maybe FilePath
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus`
               do Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Name
    new Name -> [Name] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` (TParam -> Maybe Name) -> [TParam] -> [Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe TParam -> Maybe Name
    tpName (RO -> [TParam]
    iTVars RO
    ro))
                  FilePath -> Maybe FilePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return "type variable"
               Maybe FilePath -> Maybe FilePath -> Maybe FilePath
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus`
               do Prop
    _ <- [Maybe Prop] -> Maybe Prop
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ((Map Name Prop -> Maybe Prop) -> [Map Name Prop] -> [Maybe Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Map Name Prop -> Maybe Prop
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    new) (RW -> [Map Name Prop]
    iExistTVars RW
    rw))
                  FilePath -> Maybe FilePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return "type"

         case Maybe FilePath
    shadowed of
           Nothing -> () -> InferM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
           Just that :: FilePath
    that ->
              Error -> InferM ()
    recordError (Error -> InferM ()) -> Error -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> Error
    ErrorMsg (Doc -> Error) -> Doc -> Error
    forall a b. (a -> b) -> a -> b
    $
                 FilePath -> Doc
    text "Type" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    this Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    new) Doc -> Doc -> Doc
    <+>
                 FilePath -> Doc
    text "shadows an existing" Doc -> Doc -> Doc
    <+>
                 FilePath -> Doc
    text FilePath
    that Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "with the same name."

    -- | The sub-computation is performed with the given type parameter in scope.
    withTParam :: TParam -> InferM a -> InferM a
    withTParam :: TParam -> InferM a -> InferM a
    withTParam p :: TParam
    p (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      do case TParam -> Maybe Name
    tpName TParam
    p of
           Just x :: Name
    x  -> FilePath -> Name -> InferM ()
    checkTShadowing "variable" Name
    x
           Nothing -> () -> InferM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
         ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\r :: RO
    r -> RO
    r { iTVars :: [TParam]
    iTVars = TParam
    p TParam -> [TParam] -> [TParam]
    forall a. a -> [a] -> [a]
    : RO -> [TParam]
    iTVars RO
    r }) ReaderT RO (StateT RW IO) a
    m

    withTParams :: [TParam] -> InferM a -> InferM a
    withTParams :: [TParam] -> InferM a -> InferM a
    withTParams ps :: [TParam]
    ps m :: InferM a
    m = (TParam -> InferM a -> InferM a)
    -> InferM a -> [TParam] -> InferM a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> InferM a -> InferM a
    forall a. TParam -> InferM a -> InferM a
    withTParam InferM a
    m [TParam]
    ps

    -- | The sub-computation is performed with the given type-synonym in scope.
    withTySyn :: TySyn -> InferM a -> InferM a
    withTySyn :: TySyn -> InferM a -> InferM a
    withTySyn t :: TySyn
    t (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      do let x :: Name
    x = TySyn -> Name
    tsName TySyn
    t
         FilePath -> Name -> InferM ()
    checkTShadowing "synonym" Name
    x
         ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\r :: RO
    r -> RO
    r { iTSyns :: Map Name (DefLoc, TySyn)
    iTSyns = Name
    -> (DefLoc, TySyn)
    -> Map Name (DefLoc, TySyn)
    -> Map Name (DefLoc, TySyn)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    x (DefLoc
    IsLocal,TySyn
    t) (RO -> Map Name (DefLoc, TySyn)
    iTSyns RO
    r) }) ReaderT RO (StateT RW IO) a
    m

    withNewtype :: Newtype -> InferM a -> InferM a
    withNewtype :: Newtype -> InferM a -> InferM a
    withNewtype t :: Newtype
    t (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader
            (\r :: RO
    r -> RO
    r { iNewtypes :: Map Name (DefLoc, Newtype)
    iNewtypes = Name
    -> (DefLoc, Newtype)
    -> Map Name (DefLoc, Newtype)
    -> Map Name (DefLoc, Newtype)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (Newtype -> Name
    ntName Newtype
    t) (DefLoc
    IsLocal,Newtype
    t)
                                                         (RO -> Map Name (DefLoc, Newtype)
    iNewtypes RO
    r) }) ReaderT RO (StateT RW IO) a
    m

    withPrimType :: AbstractType -> InferM a -> InferM a
    withPrimType :: AbstractType -> InferM a -> InferM a
    withPrimType t :: AbstractType
    t (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader
          (\r :: RO
    r -> RO
    r { iAbstractTypes :: Map Name (DefLoc, AbstractType)
    iAbstractTypes = Name
    -> (DefLoc, AbstractType)
    -> Map Name (DefLoc, AbstractType)
    -> Map Name (DefLoc, AbstractType)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (AbstractType -> Name
    atName AbstractType
    t) (DefLoc
    IsLocal,AbstractType
    t)
                                                            (RO -> Map Name (DefLoc, AbstractType)
    iAbstractTypes RO
    r) }) ReaderT RO (StateT RW IO) a
    m

    withParamType :: ModTParam -> InferM a -> InferM a
    withParamType :: ModTParam -> InferM a -> InferM a
    withParamType a :: ModTParam
    a (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader
            (\r :: RO
    r -> RO
    r { iParamTypes :: Map Name ModTParam
    iParamTypes = Name -> ModTParam -> Map Name ModTParam -> Map Name ModTParam
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (ModTParam -> Name
    mtpName ModTParam
    a) ModTParam
    a (RO -> Map Name ModTParam
    iParamTypes RO
    r) })
            ReaderT RO (StateT RW IO) a
    m

    -- | The sub-computation is performed with the given variable in scope.
    withVarType :: Name -> VarType -> InferM a -> InferM a
    withVarType :: Name -> VarType -> InferM a -> InferM a
    withVarType x :: Name
    x s :: VarType
    s (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\r :: RO
    r -> RO
    r { iVars :: Map Name VarType
    iVars = Name -> VarType -> Map Name VarType -> Map Name VarType
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    x VarType
    s (RO -> Map Name VarType
    iVars RO
    r) }) ReaderT RO (StateT RW IO) a
    m

    withVarTypes :: [(Name,VarType)] -> InferM a -> InferM a
    withVarTypes :: [(Name, VarType)] -> InferM a -> InferM a
    withVarTypes xs :: [(Name, VarType)]
    xs m :: InferM a
    m = ((Name, VarType) -> InferM a -> InferM a)
    -> InferM a -> [(Name, VarType)] -> InferM a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Name -> VarType -> InferM a -> InferM a)
    -> (Name, VarType) -> InferM a -> InferM a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> VarType -> InferM a -> InferM a
    forall a. Name -> VarType -> InferM a -> InferM a
    withVarType) InferM a
    m [(Name, VarType)]
    xs

    withVar :: Name -> Schema -> InferM a -> InferM a
    withVar :: Name -> Schema -> InferM a -> InferM a
    withVar x :: Name
    x s :: Schema
    s = Name -> VarType -> InferM a -> InferM a
    forall a. Name -> VarType -> InferM a -> InferM a
    withVarType Name
    x (Schema -> VarType
    ExtVar Schema
    s)

    -- | The sub-computation is performed with the given abstract function in scope.
    withParamFuns :: [ModVParam] -> InferM a -> InferM a
    withParamFuns :: [ModVParam] -> InferM a -> InferM a
    withParamFuns xs :: [ModVParam]
    xs (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\r :: RO
    r -> RO
    r { iParamFuns :: Map Name ModVParam
    iParamFuns = (ModVParam -> Map Name ModVParam -> Map Name ModVParam)
    -> Map Name ModVParam -> [ModVParam] -> Map Name ModVParam
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ModVParam -> Map Name ModVParam -> Map Name ModVParam
    add (RO -> Map Name ModVParam
    iParamFuns RO
    r) [ModVParam]
    xs }) ReaderT RO (StateT RW IO) a
    m
      where
      add :: ModVParam -> Map Name ModVParam -> Map Name ModVParam
    add x :: ModVParam
    x = Name -> ModVParam -> Map Name ModVParam -> Map Name ModVParam
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (ModVParam -> Name
    mvpName ModVParam
    x) ModVParam
    x

    -- | Add some assumptions for an entire module
    withParameterConstraints :: [Located Prop] -> InferM a -> InferM a
    withParameterConstraints :: [Located Prop] -> InferM a -> InferM a
    withParameterConstraints ps :: [Located Prop]
    ps (IM m :: ReaderT RO (StateT RW IO) a
    m) =
      ReaderT RO (StateT RW IO) a -> InferM a
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) a -> InferM a)
    -> ReaderT RO (StateT RW IO) a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\r :: RO
    r -> RO
    r { iParamConstraints :: [Located Prop]
    iParamConstraints = [Located Prop]
    ps [Located Prop] -> [Located Prop] -> [Located Prop]
    forall a. [a] -> [a] -> [a]
    ++ RO -> [Located Prop]
    iParamConstraints RO
    r }) ReaderT RO (StateT RW IO) a
    m

    -- | The sub-computation is performed with the given variables in scope.
    withMonoType :: (Name,Located Type) -> InferM a -> InferM a
    withMonoType :: (Name, Located Prop) -> InferM a -> InferM a
    withMonoType (x :: Name
    x,lt :: Located Prop
    lt) = Name -> Schema -> InferM a -> InferM a
    forall a. Name -> Schema -> InferM a -> InferM a
    withVar Name
    x ([TParam] -> [Prop] -> Prop -> Schema
    Forall [] [] (Located Prop -> Prop
    forall a. Located a -> a
    thing Located Prop
    lt))

    -- | The sub-computation is performed with the given variables in scope.
    withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a
    withMonoTypes :: Map Name (Located Prop) -> InferM a -> InferM a
    withMonoTypes xs :: Map Name (Located Prop)
    xs m :: InferM a
    m = ((Name, Located Prop) -> InferM a -> InferM a)
    -> InferM a -> [(Name, Located Prop)] -> InferM a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Name, Located Prop) -> InferM a -> InferM a
    forall a. (Name, Located Prop) -> InferM a -> InferM a
    withMonoType InferM a
    m (Map Name (Located Prop) -> [(Name, Located Prop)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Name (Located Prop)
    xs)

    -- | The sub-computation is performed with the given type synonyms
    -- and variables in scope.
    withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a
    withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a
    withDecls (ts :: [TySyn]
    ts,vs :: Map Name Schema
    vs) m :: InferM a
    m = (TySyn -> InferM a -> InferM a) -> InferM a -> [TySyn] -> InferM a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TySyn -> InferM a -> InferM a
    forall a. TySyn -> InferM a -> InferM a
    withTySyn (((Name, Schema) -> InferM a -> InferM a)
    -> InferM a -> [(Name, Schema)] -> InferM a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Name, Schema) -> InferM a -> InferM a
    forall a. (Name, Schema) -> InferM a -> InferM a
    add InferM a
    m (Map Name Schema -> [(Name, Schema)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Name Schema
    vs)) [TySyn]
    ts
      where
      add :: (Name, Schema) -> InferM a -> InferM a
    add (x :: Name
    x,t :: Schema
    t) = Name -> Schema -> InferM a -> InferM a
    forall a. Name -> Schema -> InferM a -> InferM a
    withVar Name
    x Schema
    t

    -- | Perform the given computation in a new scope (i.e., the subcomputation
    -- may use existential type variables).
    inNewScope :: InferM a -> InferM a
    inNewScope :: InferM a -> InferM a
    inNewScope m :: InferM a
    m =
      do [Map Name Prop]
    curScopes <- RW -> [Map Name Prop]
    iExistTVars (RW -> [Map Name Prop]) -> InferM RW -> InferM [Map Name Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT RO (StateT RW IO) RW -> InferM RW
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM ReaderT RO (StateT RW IO) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iExistTVars :: [Map Name Prop]
    iExistTVars = Map Name Prop
    forall k a. Map k a
    Map.empty Map Name Prop -> [Map Name Prop] -> [Map Name Prop]
    forall a. a -> [a] -> [a]
    : [Map Name Prop]
    curScopes }
         a
    a <- InferM a
    m
         ReaderT RO (StateT RW IO) () -> InferM ()
    forall a. ReaderT RO (StateT RW IO) a -> InferM a
    IM (ReaderT RO (StateT RW IO) () -> InferM ())
    -> ReaderT RO (StateT RW IO) () -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
    -> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> RW
    s { iExistTVars :: [Map Name Prop]
    iExistTVars = [Map Name Prop]
    curScopes }
         a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    --------------------------------------------------------------------------------
    -- Kind checking

    newtype KindM a = KM { KindM a -> ReaderT KRO (StateT KRW InferM) a
    unKM :: ReaderT KRO (StateT KRW InferM)  a }

    data KRO = KRO { KRO -> Map Name TParam
    lazyTParams :: Map Name TParam -- ^ lazy map, with tparams.
                   , KRO -> AllowWildCards
    allowWild   :: AllowWildCards  -- ^ are type-wild cards allowed?
                   }

    -- | Do we allow wild cards in the given context.
    data AllowWildCards = AllowWildCards | NoWildCards

    data KRW = KRW { KRW -> Map Name Kind
    typeParams :: Map Name Kind -- ^ kinds of (known) vars.
                   , KRW -> [(ConstraintSource, [Prop])]
    kCtrs      :: [(ConstraintSource,[Prop])]
                   }

    instance Functor KindM where
      fmap :: (a -> b) -> KindM a -> KindM b
    fmap f :: a -> b
    f (KM m :: ReaderT KRO (StateT KRW InferM) a
    m) = ReaderT KRO (StateT KRW InferM) b -> KindM b
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM ((a -> b)
    -> ReaderT KRO (StateT KRW InferM) a
    -> ReaderT KRO (StateT KRW InferM) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f ReaderT KRO (StateT KRW InferM) a
    m)

    instance A.Applicative KindM where
      pure :: a -> KindM a
    pure  = a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      <*> :: KindM (a -> b) -> KindM a -> KindM b
    (<*>) = KindM (a -> b) -> KindM a -> KindM b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad KindM where
      return :: a -> KindM a
    return x :: a
    x      = ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (a -> ReaderT KRO (StateT KRW InferM) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x)
      KM m :: ReaderT KRO (StateT KRW InferM) a
    m >>= :: KindM a -> (a -> KindM b) -> KindM b
    >>= k :: a -> KindM b
    k    = ReaderT KRO (StateT KRW InferM) b -> KindM b
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) a
    m ReaderT KRO (StateT KRW InferM) a
    -> (a -> ReaderT KRO (StateT KRW InferM) b)
    -> ReaderT KRO (StateT KRW InferM) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= KindM b -> ReaderT KRO (StateT KRW InferM) b
    forall a. KindM a -> ReaderT KRO (StateT KRW InferM) a
    unKM (KindM b -> ReaderT KRO (StateT KRW InferM) b)
    -> (a -> KindM b) -> a -> ReaderT KRO (StateT KRW InferM) b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> KindM b
    k)

    instance MonadFail KindM where
      fail :: FilePath -> KindM a
    fail x :: FilePath
    x        = ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (FilePath -> ReaderT KRO (StateT KRW InferM) a
    forall (m :: * -> *) a. MonadFail m => FilePath -> m a
    fail FilePath
    x)

    {- | The arguments to this function are as follows:

    (type param. name, kind signature (opt.), type parameter)

    The type parameter is just a thunk that we should not force.
    The reason is that the parameter depends on the kind that we are
    in the process of computing.

    As a result we return the value of the sub-computation and the computed
    kinds of the type parameters. -}
    runKindM :: AllowWildCards               -- Are type-wild cards allowed?
             -> [(Name, Maybe Kind, TParam)] -- ^ See comment
             -> KindM a -> InferM (a, Map Name Kind, [(ConstraintSource,[Prop])])
    runKindM :: AllowWildCards
    -> [(Name, Maybe Kind, TParam)]
    -> KindM a
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
    runKindM wildOK :: AllowWildCards
    wildOK vs :: [(Name, Maybe Kind, TParam)]
    vs (KM m :: ReaderT KRO (StateT KRW InferM) a
    m) =
      do (a :: a
    a,kw :: KRW
    kw) <- KRW -> StateT KRW InferM a -> InferM (a, KRW)
    forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
    runStateT KRW
    krw (KRO -> ReaderT KRO (StateT KRW InferM) a -> StateT KRW InferM a
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
    runReaderT KRO
    kro ReaderT KRO (StateT KRW InferM) a
    m)
         (a, Map Name Kind, [(ConstraintSource, [Prop])])
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    a, KRW -> Map Name Kind
    typeParams KRW
    kw, KRW -> [(ConstraintSource, [Prop])]
    kCtrs KRW
    kw)
      where
      tps :: Map Name TParam
    tps  = [(Name, TParam)] -> Map Name TParam
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Name
    x,TParam
    t) | (x :: Name
    x,_,t :: TParam
    t)      <- [(Name, Maybe Kind, TParam)]
    vs ]
      kro :: KRO
    kro  = KRO :: Map Name TParam -> AllowWildCards -> KRO
    KRO { allowWild :: AllowWildCards
    allowWild = AllowWildCards
    wildOK, lazyTParams :: Map Name TParam
    lazyTParams = Map Name TParam
    tps }
      krw :: KRW
    krw  = KRW :: Map Name Kind -> [(ConstraintSource, [Prop])] -> KRW
    KRW { typeParams :: Map Name Kind
    typeParams = [(Name, Kind)] -> Map Name Kind
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Name
    x,Kind
    k) | (x :: Name
    x,Just k :: Kind
    k,_) <- [(Name, Maybe Kind, TParam)]
    vs ]
                 , kCtrs :: [(ConstraintSource, [Prop])]
    kCtrs = []
                 }

    -- | This is what's returned when we lookup variables during kind checking.
    data LkpTyVar = TLocalVar TParam (Maybe Kind) -- ^ Locally bound variable.
                  | TOuterVar TParam              -- ^ An outer binding.

    -- | Check if a name refers to a type variable.
    kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)
    kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)
    kLookupTyVar x :: Name
    x = ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    -> KindM (Maybe LkpTyVar)
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
     -> KindM (Maybe LkpTyVar))
    -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    -> KindM (Maybe LkpTyVar)
    forall a b. (a -> b) -> a -> b
    $
      do Map Name TParam
    vs <- KRO -> Map Name TParam
    lazyTParams (KRO -> Map Name TParam)
    -> ReaderT KRO (StateT KRW InferM) KRO
    -> ReaderT KRO (StateT KRW InferM) (Map Name TParam)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ReaderT KRO (StateT KRW InferM) KRO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         KRW
    ss <- ReaderT KRO (StateT KRW InferM) KRW
    forall (m :: * -> *) i. StateM m i => m i
    get
         case Name -> Map Name TParam -> Maybe TParam
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x Map Name TParam
    vs of
           Just t :: TParam
    t  -> Maybe LkpTyVar -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe LkpTyVar
     -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar))
    -> Maybe LkpTyVar
    -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    forall a b. (a -> b) -> a -> b
    $ LkpTyVar -> Maybe LkpTyVar
    forall a. a -> Maybe a
    Just (LkpTyVar -> Maybe LkpTyVar) -> LkpTyVar -> Maybe LkpTyVar
    forall a b. (a -> b) -> a -> b
    $ TParam -> Maybe Kind -> LkpTyVar
    TLocalVar TParam
    t (Maybe Kind -> LkpTyVar) -> Maybe Kind -> LkpTyVar
    forall a b. (a -> b) -> a -> b
    $ Name -> Map Name Kind -> Maybe Kind
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name Kind -> Maybe Kind) -> Map Name Kind -> Maybe Kind
    forall a b. (a -> b) -> a -> b
    $ KRW -> Map Name Kind
    typeParams KRW
    ss
           Nothing -> StateT KRW InferM (Maybe LkpTyVar)
    -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (StateT KRW InferM (Maybe LkpTyVar)
     -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar))
    -> StateT KRW InferM (Maybe LkpTyVar)
    -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    forall a b. (a -> b) -> a -> b
    $ InferM (Maybe LkpTyVar) -> StateT KRW InferM (Maybe LkpTyVar)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (InferM (Maybe LkpTyVar) -> StateT KRW InferM (Maybe LkpTyVar))
    -> InferM (Maybe LkpTyVar) -> StateT KRW InferM (Maybe LkpTyVar)
    forall a b. (a -> b) -> a -> b
    $ do Maybe TParam
    t <- Name -> InferM (Maybe TParam)
    lookupTParam Name
    x
                                       Maybe LkpTyVar -> InferM (Maybe LkpTyVar)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TParam -> LkpTyVar) -> Maybe TParam -> Maybe LkpTyVar
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap TParam -> LkpTyVar
    TOuterVar Maybe TParam
    t)

    -- | Are type wild-cards OK in this context?
    kWildOK :: KindM AllowWildCards
    kWildOK :: KindM AllowWildCards
    kWildOK = ReaderT KRO (StateT KRW InferM) AllowWildCards
    -> KindM AllowWildCards
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) AllowWildCards
     -> KindM AllowWildCards)
    -> ReaderT KRO (StateT KRW InferM) AllowWildCards
    -> KindM AllowWildCards
    forall a b. (a -> b) -> a -> b
    $ (KRO -> AllowWildCards)
    -> ReaderT KRO (StateT KRW InferM) KRO
    -> ReaderT KRO (StateT KRW InferM) AllowWildCards
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap KRO -> AllowWildCards
    allowWild ReaderT KRO (StateT KRW InferM) KRO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask

    -- | Reports an error.
    kRecordError :: Error -> KindM ()
    kRecordError :: Error -> KindM ()
    kRecordError e :: Error
    e = InferM () -> KindM ()
    forall a. InferM a -> KindM a
    kInInferM (InferM () -> KindM ()) -> InferM () -> KindM ()
    forall a b. (a -> b) -> a -> b
    $ Error -> InferM ()
    recordError Error
    e

    kRecordWarning :: Warning -> KindM ()
    kRecordWarning :: Warning -> KindM ()
    kRecordWarning w :: Warning
    w = InferM () -> KindM ()
    forall a. InferM a -> KindM a
    kInInferM (InferM () -> KindM ()) -> InferM () -> KindM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> InferM ()
    recordWarning Warning
    w

    kIO :: IO a -> KindM a
    kIO :: IO a -> KindM a
    kIO m :: IO a
    m = ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) a -> KindM a)
    -> ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a b. (a -> b) -> a -> b
    $ StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a)
    -> StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a
    forall a b. (a -> b) -> a -> b
    $ InferM a -> StateT KRW InferM a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (InferM a -> StateT KRW InferM a)
    -> InferM a -> StateT KRW InferM a
    forall a b. (a -> b) -> a -> b
    $ IO a -> InferM a
    forall a. IO a -> InferM a
    io IO a
    m

    -- | Generate a fresh unification variable of the given kind.
    -- NOTE:  We do not simplify these, because we end up with bottom.
    -- See `Kind.hs`
    -- XXX: Perhaps we can avoid the recursion?
    kNewType :: TVarSource -> Kind -> KindM Type
    kNewType :: TVarSource -> Kind -> KindM Prop
    kNewType src :: TVarSource
    src k :: Kind
    k =
      do Set TParam
    tps <- ReaderT KRO (StateT KRW InferM) (Set TParam) -> KindM (Set TParam)
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) (Set TParam)
     -> KindM (Set TParam))
    -> ReaderT KRO (StateT KRW InferM) (Set TParam)
    -> KindM (Set TParam)
    forall a b. (a -> b) -> a -> b
    $ do Map Name TParam
    vs <- (KRO -> Map Name TParam)
    -> ReaderT KRO (StateT KRW InferM) (Map Name TParam)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks KRO -> Map Name TParam
    lazyTParams
                        Set TParam -> ReaderT KRO (StateT KRW InferM) (Set TParam)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set TParam -> ReaderT KRO (StateT KRW InferM) (Set TParam))
    -> Set TParam -> ReaderT KRO (StateT KRW InferM) (Set TParam)
    forall a b. (a -> b) -> a -> b
    $ [TParam] -> Set TParam
    forall a. Ord a => [a] -> Set a
    Set.fromList (Map Name TParam -> [TParam]
    forall k a. Map k a -> [a]
    Map.elems Map Name TParam
    vs)
         InferM Prop -> KindM Prop
    forall a. InferM a -> KindM a
    kInInferM (InferM Prop -> KindM Prop) -> InferM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $ TVar -> Prop
    TVar (TVar -> Prop) -> InferM TVar -> InferM Prop
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` TVarSource -> Set TParam -> Kind -> InferM TVar
    newTVar' TVarSource
    src Set TParam
    tps Kind
    k

    -- | Lookup the definition of a type synonym.
    kLookupTSyn :: Name -> KindM (Maybe TySyn)
    kLookupTSyn :: Name -> KindM (Maybe TySyn)
    kLookupTSyn x :: Name
    x = InferM (Maybe TySyn) -> KindM (Maybe TySyn)
    forall a. InferM a -> KindM a
    kInInferM (InferM (Maybe TySyn) -> KindM (Maybe TySyn))
    -> InferM (Maybe TySyn) -> KindM (Maybe TySyn)
    forall a b. (a -> b) -> a -> b
    $ Name -> InferM (Maybe TySyn)
    lookupTSyn Name
    x

    -- | Lookup the definition of a newtype.
    kLookupNewtype :: Name -> KindM (Maybe Newtype)
    kLookupNewtype :: Name -> KindM (Maybe Newtype)
    kLookupNewtype x :: Name
    x = InferM (Maybe Newtype) -> KindM (Maybe Newtype)
    forall a. InferM a -> KindM a
    kInInferM (InferM (Maybe Newtype) -> KindM (Maybe Newtype))
    -> InferM (Maybe Newtype) -> KindM (Maybe Newtype)
    forall a b. (a -> b) -> a -> b
    $ Name -> InferM (Maybe Newtype)
    lookupNewtype Name
    x

    kLookupParamType :: Name -> KindM (Maybe ModTParam)
    kLookupParamType :: Name -> KindM (Maybe ModTParam)
    kLookupParamType x :: Name
    x = InferM (Maybe ModTParam) -> KindM (Maybe ModTParam)
    forall a. InferM a -> KindM a
    kInInferM (Name -> InferM (Maybe ModTParam)
    lookupParamType Name
    x)

    kLookupAbstractType :: Name -> KindM (Maybe AbstractType)
    kLookupAbstractType :: Name -> KindM (Maybe AbstractType)
    kLookupAbstractType x :: Name
    x = InferM (Maybe AbstractType) -> KindM (Maybe AbstractType)
    forall a. InferM a -> KindM a
    kInInferM (InferM (Maybe AbstractType) -> KindM (Maybe AbstractType))
    -> InferM (Maybe AbstractType) -> KindM (Maybe AbstractType)
    forall a b. (a -> b) -> a -> b
    $ Name -> InferM (Maybe AbstractType)
    lookupAbstractType Name
    x

    kExistTVar :: Name -> Kind -> KindM Type
    kExistTVar :: Name -> Kind -> KindM Prop
    kExistTVar x :: Name
    x k :: Kind
    k = InferM Prop -> KindM Prop
    forall a. InferM a -> KindM a
    kInInferM (InferM Prop -> KindM Prop) -> InferM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $ Name -> Kind -> InferM Prop
    existVar Name
    x Kind
    k

    -- | Replace the given bound variables with concrete types.
    kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
    kInstantiateT :: Prop -> [(TParam, Prop)] -> KindM Prop
    kInstantiateT t :: Prop
    t as :: [(TParam, Prop)]
    as = Prop -> KindM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Subst -> Prop -> Prop
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Prop
    t)
      where su :: Subst
    su = [(TParam, Prop)] -> Subst
    listParamSubst [(TParam, Prop)]
    as

    {- | Record the kind for a local type variable.
    This assumes that we already checked that there was no other valid
    kind for the variable (if there was one, it gets over-written). -}
    kSetKind :: Name -> Kind -> KindM ()
    kSetKind :: Name -> Kind -> KindM ()
    kSetKind v :: Name
    v k :: Kind
    k = ReaderT KRO (StateT KRW InferM) () -> KindM ()
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) () -> KindM ())
    -> ReaderT KRO (StateT KRW InferM) () -> KindM ()
    forall a b. (a -> b) -> a -> b
    $ (KRW -> KRW) -> ReaderT KRO (StateT KRW InferM) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((KRW -> KRW) -> ReaderT KRO (StateT KRW InferM) ())
    -> (KRW -> KRW) -> ReaderT KRO (StateT KRW InferM) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: KRW
    s -> KRW
    s{ typeParams :: Map Name Kind
    typeParams = Name -> Kind -> Map Name Kind -> Map Name Kind
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    v Kind
    k (KRW -> Map Name Kind
    typeParams KRW
    s)}

    -- | The sub-computation is about the given range of the source code.
    kInRange :: Range -> KindM a -> KindM a
    kInRange :: Range -> KindM a -> KindM a
    kInRange r :: Range
    r (KM m :: ReaderT KRO (StateT KRW InferM) a
    m) = ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) a -> KindM a)
    -> ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a b. (a -> b) -> a -> b
    $
      do KRO
    e <- ReaderT KRO (StateT KRW InferM) KRO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         KRW
    s <- ReaderT KRO (StateT KRW InferM) KRW
    forall (m :: * -> *) i. StateM m i => m i
    get
         (a :: a
    a,s1 :: KRW
    s1) <- StateT KRW InferM (a, KRW)
    -> ReaderT KRO (StateT KRW InferM) (a, KRW)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (StateT KRW InferM (a, KRW)
     -> ReaderT KRO (StateT KRW InferM) (a, KRW))
    -> StateT KRW InferM (a, KRW)
    -> ReaderT KRO (StateT KRW InferM) (a, KRW)
    forall a b. (a -> b) -> a -> b
    $ InferM (a, KRW) -> StateT KRW InferM (a, KRW)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (InferM (a, KRW) -> StateT KRW InferM (a, KRW))
    -> InferM (a, KRW) -> StateT KRW InferM (a, KRW)
    forall a b. (a -> b) -> a -> b
    $ Range -> InferM (a, KRW) -> InferM (a, KRW)
    forall a. Range -> InferM a -> InferM a
    inRange Range
    r (InferM (a, KRW) -> InferM (a, KRW))
    -> InferM (a, KRW) -> InferM (a, KRW)
    forall a b. (a -> b) -> a -> b
    $ KRW -> StateT KRW InferM a -> InferM (a, KRW)
    forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
    runStateT KRW
    s (StateT KRW InferM a -> InferM (a, KRW))
    -> StateT KRW InferM a -> InferM (a, KRW)
    forall a b. (a -> b) -> a -> b
    $ KRO -> ReaderT KRO (StateT KRW InferM) a -> StateT KRW InferM a
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
    runReaderT KRO
    e ReaderT KRO (StateT KRW InferM) a
    m
         KRW -> ReaderT KRO (StateT KRW InferM) ()
    forall (m :: * -> *) i. StateM m i => i -> m ()
    set KRW
    s1
         a -> ReaderT KRO (StateT KRW InferM) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
    kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
    kNewGoals _ [] = () -> KindM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    kNewGoals c :: ConstraintSource
    c ps :: [Prop]
    ps = ReaderT KRO (StateT KRW InferM) () -> KindM ()
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) () -> KindM ())
    -> ReaderT KRO (StateT KRW InferM) () -> KindM ()
    forall a b. (a -> b) -> a -> b
    $ (KRW -> KRW) -> ReaderT KRO (StateT KRW InferM) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((KRW -> KRW) -> ReaderT KRO (StateT KRW InferM) ())
    -> (KRW -> KRW) -> ReaderT KRO (StateT KRW InferM) ()
    forall a b. (a -> b) -> a -> b
    $ \s :: KRW
    s -> KRW
    s { kCtrs :: [(ConstraintSource, [Prop])]
    kCtrs = (ConstraintSource
    c,[Prop]
    ps) (ConstraintSource, [Prop])
    -> [(ConstraintSource, [Prop])] -> [(ConstraintSource, [Prop])]
    forall a. a -> [a] -> [a]
    : KRW -> [(ConstraintSource, [Prop])]
    kCtrs KRW
    s }

    kInInferM :: InferM a -> KindM a
    kInInferM :: InferM a -> KindM a
    kInInferM m :: InferM a
    m = ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (ReaderT KRO (StateT KRW InferM) a -> KindM a)
    -> ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a b. (a -> b) -> a -> b
    $ StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a)
    -> StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a
    forall a b. (a -> b) -> a -> b
    $ InferM a -> StateT KRW InferM a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift InferM a
    m