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

    import qualified Control.Applicative as A
    import qualified Control.Monad.Fail as Fail
    import           Control.Monad.Fix(MonadFix(..))
    import           Data.Text(Text)
    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.List.NonEmpty(NonEmpty((:|)))
    import           Data.Semigroup(sconcat)
    import           Data.Maybe(mapMaybe,fromMaybe)
    import           Data.IORef

    import           GHC.Generics (Generic)
    import           Control.DeepSeq

    import           MonadLib hiding (mapM)

    import           Cryptol.ModuleSystem.Name
                        (FreshM(..),Supply,mkLocal,asLocal
                        , nameInfo, NameInfo(..),NameSource(..), nameTopModule)
    import qualified Cryptol.ModuleSystem.Interface as If
    import           Cryptol.Parser.Position
    import qualified Cryptol.Parser.AST as P
    import           Cryptol.TypeCheck.AST
    import           Cryptol.TypeCheck.Subst
    import           Cryptol.TypeCheck.Interface(genIfaceWithNames,genIfaceNames)
    import           Cryptol.TypeCheck.Unify(doMGU, runResult, UnificationError(..)
                                            , Path, rootPath)
    import           Cryptol.TypeCheck.InferTypes
    import           Cryptol.TypeCheck.Error( Warning(..),Error(..)
                                            , cleanupErrors, computeFreeVarNames
                                            )
    import qualified Cryptol.TypeCheck.SimpleSolver as Simple
    import qualified Cryptol.TypeCheck.Solver.SMT as SMT
    import           Cryptol.TypeCheck.PP(NameMap)
    import           Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets,debugShowUniques)
    import           Cryptol.Utils.Ident(Ident,Namespace(..),ModName)
    import           Cryptol.Utils.Panic(panic)

    -- | 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
      , InferInput -> Map Name ModParamNames
    inpSignatures :: !(Map Name ModParamNames)  -- ^ Signatures in scope

      , InferInput -> ModName -> Maybe (ModuleG (), IfaceG ())
    inpTopModules    :: ModName -> Maybe (ModuleG (), If.IfaceG ())
      , InferInput -> ModName -> Maybe ModParamNames
    inpTopSignatures :: ModName -> Maybe ModParamNames

        -- When typechecking a module these start off empty.
        -- We need them when type-checking an expression at the command
        -- line, for example.
      , InferInput -> ModParamNames
    inpParams :: !ModParamNames

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

      , InferInput -> Bool
    inpCallStacks :: Bool             -- ^ Are we tracking call stacks?

      , InferInput -> [String]
    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

      , InferInput -> Solver
    inpSolver :: SMT.Solver           -- ^ Solver connection for typechecking
      }

    -- | 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 -> String
    (Int -> NameSeeds -> ShowS)
    -> (NameSeeds -> String)
    -> ([NameSeeds] -> ShowS)
    -> Show NameSeeds
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> NameSeeds -> ShowS
    showsPrec :: Int -> NameSeeds -> ShowS
    $cshow :: NameSeeds -> String
    show :: NameSeeds -> String
    $cshowList :: [NameSeeds] -> ShowS
    showList :: [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
    $cfrom :: forall x. NameSeeds -> Rep NameSeeds x
    from :: forall x. NameSeeds -> Rep NameSeeds x
    $cto :: forall x. Rep NameSeeds x -> NameSeeds
    to :: forall x. Rep NameSeeds x -> NameSeeds
    Generic, NameSeeds -> ()
    (NameSeeds -> ()) -> NFData NameSeeds
    forall a. (a -> ()) -> NFData a
    $crnf :: NameSeeds -> ()
    rnf :: NameSeeds -> ()
    NFData)

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

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

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

        deriving Int -> InferOutput a -> ShowS
    [InferOutput a] -> ShowS
    InferOutput a -> String
    (Int -> InferOutput a -> ShowS)
    -> (InferOutput a -> String)
    -> ([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 -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> InferOutput a -> ShowS
    showsPrec :: Int -> InferOutput a -> ShowS
    $cshow :: forall a. Show a => InferOutput a -> String
    show :: InferOutput a -> String
    $cshowList :: forall a. Show a => [InferOutput a] -> ShowS
    showList :: [InferOutput a] -> ShowS
    Show

    bumpCounter :: InferM ()
    bumpCounter :: InferM ()
    bumpCounter = do RO { Bool
    [TParam]
    IORef Int
    Map Int HasGoalSln
    Map Name VarType
    Range
    PrimMap
    ModuleG ScopeName
    Solver
    ModName -> Maybe (ModuleG (), IfaceG ())
    ModName -> Maybe ModParamNames
    iRange :: Range
    iVars :: Map Name VarType
    iTVars :: [TParam]
    iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
    iExtSignatures :: ModName -> Maybe ModParamNames
    iExtScope :: ModuleG ScopeName
    iSolvedHasLazy :: Map Int HasGoalSln
    iMonoBinds :: Bool
    iCallStacks :: Bool
    iSolver :: Solver
    iPrimNames :: PrimMap
    iSolveCounter :: IORef Int
    iRange :: RO -> Range
    iVars :: RO -> Map Name VarType
    iTVars :: RO -> [TParam]
    iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
    iExtSignatures :: RO -> ModName -> Maybe ModParamNames
    iExtScope :: RO -> ModuleG ScopeName
    iSolvedHasLazy :: RO -> Map Int HasGoalSln
    iMonoBinds :: RO -> Bool
    iCallStacks :: RO -> Bool
    iSolver :: RO -> Solver
    iPrimNames :: RO -> PrimMap
    iSolveCounter :: RO -> IORef Int
    .. } <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] 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
    +Int
    1)

    runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
    runInferM :: forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
    runInferM InferInput
    info InferM a
    m0 =
      do let IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m = InferM a -> InferM a
    forall a. InferM a -> InferM a
    selectorScope InferM a
    m0
         IORef Int
    counter <- Int -> IO (IORef Int)
    forall a. a -> IO (IORef a)
    newIORef Int
    0
         let allPs :: ModParamNames
    allPs = InferInput -> ModParamNames
    inpParams InferInput
    info

         let env :: Map Name VarType
    env = (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)
                Map Name VarType -> Map Name VarType -> Map Name VarType
    forall a. Semigroup a => a -> a -> a
    <> [(Name, VarType)] -> Map Name VarType
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
                  [ (Newtype -> Name
    ntConName Newtype
    nt, Schema -> VarType
    ExtVar (Newtype -> Schema
    newtypeConType Newtype
    nt))
                  | Newtype
    nt <- Map Name Newtype -> [Newtype]
    forall k a. Map k a -> [a]
    Map.elems (InferInput -> Map Name Newtype
    inpNewtypes InferInput
    info)
                  ]
                Map Name VarType -> Map Name VarType -> Map Name VarType
    forall a. Semigroup a => a -> a -> a
    <> (ModVParam -> VarType) -> Map Name ModVParam -> Map Name VarType
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map (Schema -> VarType
    ExtVar (Schema -> VarType)
    -> (ModVParam -> Schema) -> ModVParam -> VarType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModVParam -> Schema
    mvpType) (ModParamNames -> Map Name ModVParam
    mpnFuns ModParamNames
    allPs)

         let ro :: RO
    ro =         RO { iRange :: Range
    iRange     = InferInput -> Range
    inpRange InferInput
    info
                             , iVars :: Map Name VarType
    iVars      = Map Name VarType
    env
                             , iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
    iExtModules = InferInput -> ModName -> Maybe (ModuleG (), IfaceG ())
    inpTopModules InferInput
    info
                             , iExtSignatures :: ModName -> Maybe ModParamNames
    iExtSignatures = InferInput -> ModName -> Maybe ModParamNames
    inpTopSignatures InferInput
    info
                             , iExtScope :: ModuleG ScopeName
    iExtScope = (ScopeName -> ModuleG ScopeName
    forall mname. mname -> ModuleG mname
    emptyModule ScopeName
    ExternalScope)
                                 { mTySyns :: Map Name TySyn
    mTySyns           = InferInput -> Map Name TySyn
    inpTSyns InferInput
    info Map Name TySyn -> Map Name TySyn -> Map Name TySyn
    forall a. Semigroup a => a -> a -> a
    <>
                                                       ModParamNames -> Map Name TySyn
    mpnTySyn ModParamNames
    allPs
                                 , mNewtypes :: Map Name Newtype
    mNewtypes         = InferInput -> Map Name Newtype
    inpNewtypes InferInput
    info
                                 , mPrimTypes :: Map Name AbstractType
    mPrimTypes        = InferInput -> Map Name AbstractType
    inpAbstractTypes InferInput
    info
                                 , mParamTypes :: Map Name ModTParam
    mParamTypes       = ModParamNames -> Map Name ModTParam
    mpnTypes ModParamNames
    allPs
                                 , mParamFuns :: Map Name ModVParam
    mParamFuns        = ModParamNames -> Map Name ModVParam
    mpnFuns  ModParamNames
    allPs
                                 , mParamConstraints :: [Located Type]
    mParamConstraints = ModParamNames -> [Located Type]
    mpnConstraints ModParamNames
    allPs
                                 , mSignatures :: Map Name ModParamNames
    mSignatures       = InferInput -> Map Name ModParamNames
    inpSignatures InferInput
    info
                                 }

                             , iTVars :: [TParam]
    iTVars         = []
                             , iSolvedHasLazy :: Map Int HasGoalSln
    iSolvedHasLazy = Map Int HasGoalSln
    forall k a. Map k a
    Map.empty
                             , iMonoBinds :: Bool
    iMonoBinds     = InferInput -> Bool
    inpMonoBinds InferInput
    info
                             , iCallStacks :: Bool
    iCallStacks    = InferInput -> Bool
    inpCallStacks InferInput
    info
                             , iSolver :: Solver
    iSolver        = InferInput -> Solver
    inpSolver InferInput
    info
                             , iPrimNames :: PrimMap
    iPrimNames     = InferInput -> PrimMap
    inpPrimNames InferInput
    info
                             , iSolveCounter :: IORef Int
    iSolveCounter  = IORef Int
    counter
                             }

         Either [(Range, Error)] (a, RW)
    mb <- ExceptionT [(Range, Error)] IO (a, RW)
    -> IO (Either [(Range, Error)] (a, RW))
    forall i (m :: * -> *) a. ExceptionT i m a -> m (Either i a)
    runExceptionT (RW
    -> StateT RW (ExceptionT [(Range, Error)] IO) a
    -> ExceptionT [(Range, Error)] IO (a, RW)
    forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
    runStateT RW
    rw (RO
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> StateT RW (ExceptionT [(Range, Error)] IO) a
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
    runReaderT RO
    ro ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m))
         case Either [(Range, Error)] (a, RW)
    mb of
           Left [(Range, Error)]
    errs -> [(Range, Warning)] -> [(Range, Error)] -> IO (InferOutput a)
    forall {f :: * -> *} {a}.
    Applicative f =>
    [(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
    inferFailed [] [(Range, Error)]
    errs
           Right (a
    result, RW
    finalRW) ->
             do let theSu :: Subst
    theSu    = RW -> Subst
    iSubst RW
    finalRW
                    defSu :: Subst
    defSu    = Subst -> Subst
    defaultingSubst Subst
    theSu
                    warns :: [(Range, Warning)]
    warns    = ((Range, Warning) -> (Range, Warning))
    -> [(Range, Warning)] -> [(Range, Warning)]
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    fmap' ((Warning -> Warning) -> (Range, Warning) -> (Range, Warning)
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    fmap' (Subst -> Warning -> Warning
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    theSu)) (RW -> [(Range, Warning)]
    iWarnings RW
    finalRW)

                case RW -> [(Range, Error)]
    iErrors RW
    finalRW of
                  [] ->
                    case RW -> Goals
    iCts RW
    finalRW of
                      Goals
    cts
                        | Goals -> Bool
    nullGoals Goals
    cts -> [(Range, Warning)]
    -> NameSeeds -> Supply -> a -> IO (InferOutput a)
    forall {f :: * -> *} {a}.
    Applicative f =>
    [(Range, Warning)] -> NameSeeds -> Supply -> a -> f (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)
                      Goals
    cts ->
                         [(Range, Warning)] -> [(Range, Error)] -> IO (InferOutput a)
    forall {f :: * -> *} {a}.
    Applicative f =>
    [(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
    inferFailed [(Range, Warning)]
    warns
                           [ ( Goal -> Range
    goalRange Goal
    g
                             , [Goal] -> Error
    UnsolvedGoals [Subst -> Goal -> Goal
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    theSu Goal
    g]
                             ) | Goal
    g <- Goals -> [Goal]
    fromGoals Goals
    cts
                           ]

                  [(Range, Error)]
    errs -> [(Range, Warning)] -> [(Range, Error)] -> IO (InferOutput a)
    forall {f :: * -> *} {a}.
    Applicative f =>
    [(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
    inferFailed [(Range, Warning)]
    warns [(Range
    r,Subst -> Error -> Error
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    theSu Error
    e) | (Range
    r,Error
    e) <- [(Range, Error)]
    errs]

      where
      inferOk :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> f (InferOutput a)
    inferOk [(Range, Warning)]
    ws NameSeeds
    a Supply
    b a
    c  = InferOutput a -> f (InferOutput a)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NameMap
    -> [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
    forall a.
    NameMap
    -> [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
    InferOK ([(Range, Warning)] -> [(Range, Error)] -> NameMap
    computeFreeVarNames [(Range, Warning)]
    ws []) [(Range, Warning)]
    ws NameSeeds
    a Supply
    b a
    c)
      inferFailed :: [(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
    inferFailed [(Range, Warning)]
    ws [(Range, Error)]
    es =
        let es1 :: [(Range, Error)]
    es1 = [(Range, Error)] -> [(Range, Error)]
    cleanupErrors [(Range, Error)]
    es
        in InferOutput a -> f (InferOutput a)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NameMap -> [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
    forall a.
    NameMap -> [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
    InferFailed ([(Range, Warning)] -> [(Range, Error)] -> NameMap
    computeFreeVarNames [(Range, Warning)]
    ws [(Range, Error)]
    es1) [(Range, Warning)]
    ws [(Range, Error)]
    es1)

      rw :: RW
    rw = RW { iErrors :: [(Range, Error)]
    iErrors     = []
              , iWarnings :: [(Range, Warning)]
    iWarnings   = []
              , iSubst :: Subst
    iSubst      = Subst
    emptySubst
              , iExistTVars :: [Map Name Type]
    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

              , iScope :: [ModuleG ScopeName]
    iScope      = []
              , iBindTypes :: Map Name Schema
    iBindTypes  = Map Name Schema
    forall a. Monoid a => a
    mempty
              }

    {- | This introduces a new "selector scope" which is currently a module.
    I think that it might be possible to have selectors scopes be groups
    of recursive declarations instead, as we are not going to learn anything
    additional once we are done with the recursive group that generated
    the selectors constraints.   We do it at the module level because this
    allows us to report more errors at once.

    A selector scope does the following:
      * Keep track of the Has constraints generated in this scope
      * Keep track of the solutions for discharged selector constraints:
        - this uses a laziness trick where we build up a map containing the
          solutions for the Has constraints in the state
        - the *final* value for this map (i.e., at the value the end of the scope)
          is passed in as thunk in the reader component of the moment
        - as we type check expressions when we need the solution for a Has
          constraint we look it up from the reader environment; note that
          since the map is not yet built up we just get back a thunk, so we have
          to be carefule to not force it until *after* we've solved the goals
        - all of this happens in the `rec` block below
      * At the end of a selector scope we make sure that all Has constraints were
        discharged.  If not, we *abort* further type checking.  The reason for
        aborting rather than just recording an error is that the expression
        which produce contains thunks that will lead to non-termination if forced,
        and some type-checking operations (e.g., instantiation a functor)
        require us to traverse the expressions.
    -}
    selectorScope :: InferM a -> InferM a
    selectorScope :: forall a. InferM a -> InferM a
    selectorScope (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m1) = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM
      do RO
    ro <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RW
    rw <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         Either [(Range, Error)] (a, RW)
    mb <- IO (Either [(Range, Error)] (a, RW))
    -> ReaderT
         RO
         (StateT RW (ExceptionT [(Range, Error)] IO))
         (Either [(Range, Error)] (a, RW))
    forall a.
    IO a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
    inBase
               do rec let ro1 :: RO
    ro1 = RO
    ro { iSolvedHasLazy :: Map Int HasGoalSln
    iSolvedHasLazy = Map Int HasGoalSln
    solved }
                          rw1 :: RW
    rw1 = RW
    rw { iHasCts :: [[HasGoal]]
    iHasCts = [] [HasGoal] -> [[HasGoal]] -> [[HasGoal]]
    forall a. a -> [a] -> [a]
    : RW -> [[HasGoal]]
    iHasCts RW
    rw }
                      Either [(Range, Error)] (a, RW)
    mb <- ExceptionT [(Range, Error)] IO (a, RW)
    -> IO (Either [(Range, Error)] (a, RW))
    forall i (m :: * -> *) a. ExceptionT i m a -> m (Either i a)
    runExceptionT (RW
    -> StateT RW (ExceptionT [(Range, Error)] IO) a
    -> ExceptionT [(Range, Error)] IO (a, RW)
    forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
    runStateT RW
    rw1 (RO
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> StateT RW (ExceptionT [(Range, Error)] IO) a
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
    runReaderT RO
    ro1 ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m1))
                      let solved :: Map Int HasGoalSln
    solved = case Either [(Range, Error)] (a, RW)
    mb of
                                     Left {} -> Map Int HasGoalSln
    forall k a. Map k a
    Map.empty
                                     Right (a
    _,RW
    rw2) -> RW -> Map Int HasGoalSln
    iSolvedHas RW
    rw2
                  Either [(Range, Error)] (a, RW)
    -> IO (Either [(Range, Error)] (a, RW))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Either [(Range, Error)] (a, RW)
    mb
         case Either [(Range, Error)] (a, RW)
    mb of
           Left [(Range, Error)]
    err      -> [(Range, Error)]
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall a.
    [(Range, Error)]
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise [(Range, Error)]
    err
           Right (a
    a,RW
    rw1) ->
             case RW -> [[HasGoal]]
    iHasCts RW
    rw1 of
               [HasGoal]
    us : [[HasGoal]]
    cs ->
                 do let errs :: [(Range, Error)]
    errs = [ (Goal -> Range
    goalRange Goal
    g, [Goal] -> Error
    UnsolvedGoals [Goal
    g])
                               | Goal
    g <- (HasGoal -> Goal) -> [HasGoal] -> [Goal]
    forall a b. (a -> b) -> [a] -> [b]
    map HasGoal -> Goal
    hasGoal [HasGoal]
    us ]
                    RW -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) i. StateM m i => i -> m ()
    set RW
    rw1 { iErrors :: [(Range, Error)]
    iErrors = [(Range, Error)]
    errs [(Range, Error)] -> [(Range, Error)] -> [(Range, Error)]
    forall a. [a] -> [a] -> [a]
    ++ RW -> [(Range, Error)]
    iErrors RW
    rw1, iHasCts :: [[HasGoal]]
    iHasCts = [[HasGoal]]
    cs }
                    InferM ()
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a.
    InferM a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    unIM (InferM ()
    abortIfErrors)
                    a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall a.
    a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    a
               [] -> String
    -> [String]
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "selectorScope" [String
    "No selector scope"]

    newtype InferM a = IM { forall a.
    InferM a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    unIM :: ReaderT RO
                                  ( StateT  RW
                                  ( ExceptionT [(Range,Error)]
                                    IO
                                  )) a }

    data ScopeName = ExternalScope
                   | LocalScope
                   | SubModule Name
                   | SignatureScope Name (Maybe Text) -- ^ The Text is docs
                   | TopSignatureScope P.ModName
                   | MTopModule P.ModName

    -- | 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
        -- These are only parameters vars that are in recursive component we
        -- are checking at the moment.  If a var is not there, keep looking in
        -- the 'iScope'

      , RO -> [TParam]
    iTVars    :: [TParam]    -- ^ Type variable that are in scope

      , RO -> ModName -> Maybe (ModuleG (), IfaceG ())
    iExtModules :: ModName -> Maybe (ModuleG (), If.IfaceG ())
        -- ^ An exteral top-level module.
        -- We need the actual module when we instantiate functors,
        -- because currently the type-checker desugars such modules.

      , RO -> ModName -> Maybe ModParamNames
    iExtSignatures :: ModName -> Maybe ModParamNames
        -- ^ External top-level signatures.

      , RO -> ModuleG ScopeName
    iExtScope :: ModuleG ScopeName
        -- ^ These are things we know about, but are not part of the
        -- modules we are currently constructing.
        -- XXX: this sould probably be an interface
        -- NOTE: External functors should be looked up in `iExtModules`
        -- and not here, as they may be top-level modules.

      , 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 -> Bool
    iCallStacks :: Bool
        -- ^ When this flag is true, retain source location information
        --   in typechecked terms

      , 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 Type]
    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.  These are separate from
           the other constraints because solving them results in actual elaboration
           of the term, indicating how to do the projection.  The modification
           of the term is done using lazyness, by looking up a thunk ahead of time
           (@iSolvedHasLazy@ in RO), which is filled in when the constrait is
           solved (@iSolvedHas@).  See also `selectorScope`.
        -}

      , RW -> [ModuleG ScopeName]
    iScope :: ![ModuleG ScopeName]
        -- ^ Nested scopes we are currently checking, most nested first.
        -- These are basically partially built modules.

      , RW -> Map Name Schema
    iBindTypes :: !(Map Name Schema)
        -- ^ Types of variables that we know about.  We don't worry about scoping
        -- here because we assume the bindings all have different names.

      , RW -> Supply
    iSupply :: !Supply
      }

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

    instance A.Applicative InferM where
      pure :: forall a. a -> InferM a
    pure a
    x = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall a.
    a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x)
      <*> :: forall a b. 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 :: forall a. a -> InferM a
    return        = a -> InferM a
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m >>= :: forall a b. InferM a -> (a -> InferM b) -> InferM b
    >>= a -> InferM b
    f    = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    -> InferM b
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> (a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    forall a b.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> (a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= InferM b
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    forall a.
    InferM a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    unIM (InferM b
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b)
    -> (a -> InferM b)
    -> a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> InferM b
    f)

    instance Fail.MonadFail InferM where
      fail :: forall a. String -> InferM a
    fail String
    x        = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (String -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall a.
    String -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    x)

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

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

    io :: IO a -> InferM a
    io :: forall a. IO a -> InferM a
    io IO a
    m = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
     -> InferM a)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a b. (a -> b) -> a -> b
    $ IO a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall a.
    IO a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] 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 :: forall a. Range -> InferM a -> InferM a
    inRange Range
    r (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m) = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
     -> InferM a)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\RO
    ro -> RO
    ro { iRange :: Range
    iRange = Range
    r }) ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m

    inRangeMb :: Maybe Range -> InferM a -> InferM a
    inRangeMb :: forall a. Maybe Range -> InferM a -> InferM a
    inRangeMb Maybe Range
    Nothing InferM a
    m  = InferM a
    m
    inRangeMb (Just Range
    r) 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 (ExceptionT [(Range, Error)] IO)) Range
    -> InferM Range
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Range
     -> InferM Range)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Range
    -> InferM Range
    forall a b. (a -> b) -> a -> b
    $ (RO -> Range)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] 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 = Maybe Range -> Error -> InferM ()
    recordErrorLoc Maybe Range
    forall a. Maybe a
    Nothing

    -- | Report an error.
    recordErrorLoc :: Maybe Range -> Error -> InferM ()
    recordErrorLoc :: Maybe Range -> Error -> InferM ()
    recordErrorLoc Maybe Range
    rng Error
    e =
      do Range
    r <- case Maybe Range
    rng of
                Just Range
    r  -> Range -> InferM Range
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Range
    r
                Maybe Range
    Nothing -> case Error
    e of
                             AmbiguousSize TVarInfo
    d Maybe Type
    _ -> Range -> InferM Range
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVarInfo -> Range
    tvarSource TVarInfo
    d)
                             Error
    _                 -> InferM Range
    curRange
         ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW)
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ())
    -> (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a b. (a -> b) -> a -> b
    $ \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 }

    -- | If there are any recoded errors than abort firther type-checking.
    abortIfErrors :: InferM ()
    abortIfErrors :: InferM ()
    abortIfErrors =
      do RW
    rw <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> InferM RW
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         case RW -> [(Range, Error)]
    iErrors RW
    rw of
           [] -> () -> InferM ()
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
           [(Range, Error)]
    es ->
             do [(Range, Error)]
    es1 <- [(Range, Error)]
    -> ((Range, Error) -> InferM (Range, Error))
    -> InferM [(Range, Error)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Range, Error)]
    es \(Range
    l,Error
    e) ->
                          do Error
    e1 <- Error -> InferM Error
    forall t. TVars t => t -> InferM t
    applySubst Error
    e
                             (Range, Error) -> InferM (Range, Error)
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Range
    l,Error
    e1)
                ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ([(Range, Error)]
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a.
    [(Range, Error)]
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise [(Range, Error)]
    es1)

    recordWarning :: Warning -> InferM ()
    recordWarning :: Warning -> InferM ()
    recordWarning 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 TVarInfo
    d Type
    _ -> Range -> InferM Range
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVarInfo -> Range
    tvarSource TVarInfo
    d)
                Warning
    _ -> InferM Range
    curRange
         ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW)
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ())
    -> (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a b. (a -> b) -> a -> b
    $ \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 TVarInfo
    d Type
    _ <- Warning
    w
        , Just Name
    n <- TypeSource -> Maybe Name
    tvSourceName (TVarInfo -> TypeSource
    tvarDesc TVarInfo
    d)
        , GlobalName NameSource
    SystemName OrigName
    _ <- Name -> NameInfo
    nameInfo Name
    n
          = Bool
    True
        | Bool
    otherwise = Bool
    False

    getSolver :: InferM SMT.Solver
    getSolver :: InferM Solver
    getSolver =
      do RO { Bool
    [TParam]
    IORef Int
    Map Int HasGoalSln
    Map Name VarType
    Range
    PrimMap
    ModuleG ScopeName
    Solver
    ModName -> Maybe (ModuleG (), IfaceG ())
    ModName -> Maybe ModParamNames
    iRange :: RO -> Range
    iVars :: RO -> Map Name VarType
    iTVars :: RO -> [TParam]
    iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
    iExtSignatures :: RO -> ModName -> Maybe ModParamNames
    iExtScope :: RO -> ModuleG ScopeName
    iSolvedHasLazy :: RO -> Map Int HasGoalSln
    iMonoBinds :: RO -> Bool
    iCallStacks :: RO -> Bool
    iSolver :: RO -> Solver
    iPrimNames :: RO -> PrimMap
    iSolveCounter :: RO -> IORef Int
    iRange :: Range
    iVars :: Map Name VarType
    iTVars :: [TParam]
    iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
    iExtSignatures :: ModName -> Maybe ModParamNames
    iExtScope :: ModuleG ScopeName
    iSolvedHasLazy :: Map Int HasGoalSln
    iMonoBinds :: Bool
    iCallStacks :: Bool
    iSolver :: Solver
    iPrimNames :: PrimMap
    iSolveCounter :: IORef Int
    .. } <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         Solver -> InferM Solver
    forall a. a -> InferM a
    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 { Bool
    [TParam]
    IORef Int
    Map Int HasGoalSln
    Map Name VarType
    Range
    PrimMap
    ModuleG ScopeName
    Solver
    ModName -> Maybe (ModuleG (), IfaceG ())
    ModName -> Maybe ModParamNames
    iRange :: RO -> Range
    iVars :: RO -> Map Name VarType
    iTVars :: RO -> [TParam]
    iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
    iExtSignatures :: RO -> ModName -> Maybe ModParamNames
    iExtScope :: RO -> ModuleG ScopeName
    iSolvedHasLazy :: RO -> Map Int HasGoalSln
    iMonoBinds :: RO -> Bool
    iCallStacks :: RO -> Bool
    iSolver :: RO -> Solver
    iPrimNames :: RO -> PrimMap
    iSolveCounter :: RO -> IORef Int
    iRange :: Range
    iVars :: Map Name VarType
    iTVars :: [TParam]
    iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
    iExtSignatures :: ModName -> Maybe ModParamNames
    iExtScope :: ModuleG ScopeName
    iSolvedHasLazy :: Map Int HasGoalSln
    iMonoBinds :: Bool
    iCallStacks :: Bool
    iSolver :: Solver
    iPrimNames :: PrimMap
    iSolveCounter :: IORef Int
    .. } <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         PrimMap -> InferM PrimMap
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PrimMap
    iPrimNames

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

    -- | Record some constraints that need to be solved.
    -- The string explains where the constraints came from.
    newGoals :: ConstraintSource -> [Prop] -> InferM ()
    newGoals :: ConstraintSource -> [Type] -> InferM ()
    newGoals ConstraintSource
    src [Type]
    ps = [Goal] -> InferM ()
    addGoals ([Goal] -> InferM ()) -> InferM [Goal] -> InferM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Type -> InferM Goal) -> [Type] -> InferM [Goal]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (ConstraintSource -> Type -> InferM Goal
    newGoal ConstraintSource
    src) [Type]
    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 (ExceptionT [(Range, Error)] IO)) Goals
    -> InferM Goals
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ((RW -> (Goals, RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> (Goals, RW))
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals)
    -> (RW -> (Goals, RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals
    forall a b. (a -> b) -> a -> b
    $ \RW
    s -> (RW -> Goals
    iCts RW
    s, RW
    s { iCts :: Goals
    iCts = Goals
    emptyGoals }))
         [Goal] -> InferM [Goal]
    forall a. a -> InferM a
    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 [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 a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      doAdd [Goal]
    gs = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW)
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ())
    -> (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a b. (a -> b) -> a -> b
    $ \RW
    s -> RW
    s { iCts :: Goals
    iCts = (Goals -> Goal -> Goals) -> Goals -> [Goal] -> Goals
    forall b a. (b -> a -> b) -> b -> [a] -> b
    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 :: forall a. InferM a -> InferM (a, [Goal])
    collectGoals 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 a. a -> InferM a
    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 (ExceptionT [(Range, Error)] IO)) Goals
    -> InferM Goals
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals
     -> InferM Goals)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals
    -> InferM Goals
    forall a b. (a -> b) -> a -> b
    $ (RW -> (Goals, RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> (Goals, RW))
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals)
    -> (RW -> (Goals, RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Goals
    forall a b. (a -> b) -> a -> b
    $ \ RW { [[HasGoal]]
    [(Range, Error)]
    [(Range, Warning)]
    [Map Name Type]
    [ModuleG ScopeName]
    Map Int HasGoalSln
    Map Name Schema
    Supply
    Subst
    Goals
    NameSeeds
    iSubst :: RW -> Subst
    iWarnings :: RW -> [(Range, Warning)]
    iErrors :: RW -> [(Range, Error)]
    iCts :: RW -> Goals
    iNameSeeds :: RW -> NameSeeds
    iSupply :: RW -> Supply
    iExistTVars :: RW -> [Map Name Type]
    iHasCts :: RW -> [[HasGoal]]
    iSolvedHas :: RW -> Map Int HasGoalSln
    iScope :: RW -> [ModuleG ScopeName]
    iBindTypes :: RW -> Map Name Schema
    iErrors :: [(Range, Error)]
    iWarnings :: [(Range, Warning)]
    iSubst :: Subst
    iExistTVars :: [Map Name Type]
    iSolvedHas :: Map Int HasGoalSln
    iNameSeeds :: NameSeeds
    iCts :: Goals
    iHasCts :: [[HasGoal]]
    iScope :: [ModuleG ScopeName]
    iBindTypes :: Map Name Schema
    iSupply :: Supply
    .. } -> (Goals
    iCts, RW { iCts :: Goals
    iCts = Goals
    emptyGoals, [[HasGoal]]
    [(Range, Error)]
    [(Range, Warning)]
    [Map Name Type]
    [ModuleG ScopeName]
    Map Int HasGoalSln
    Map Name Schema
    Supply
    Subst
    NameSeeds
    iSubst :: Subst
    iWarnings :: [(Range, Warning)]
    iErrors :: [(Range, Error)]
    iNameSeeds :: NameSeeds
    iSupply :: Supply
    iExistTVars :: [Map Name Type]
    iHasCts :: [[HasGoal]]
    iSolvedHas :: Map Int HasGoalSln
    iScope :: [ModuleG ScopeName]
    iBindTypes :: Map Name Schema
    iErrors :: [(Range, Error)]
    iWarnings :: [(Range, Warning)]
    iSubst :: Subst
    iExistTVars :: [Map Name Type]
    iSolvedHas :: Map Int HasGoalSln
    iNameSeeds :: NameSeeds
    iHasCts :: [[HasGoal]]
    iScope :: [ModuleG ScopeName]
    iBindTypes :: Map Name Schema
    iSupply :: Supply
    .. })

      -- set the type map directly
      setGoals' :: Goals -> InferM ()
    setGoals' Goals
    gs = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> ((), RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> ((), RW))
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ())
    -> (RW -> ((), RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a b. (a -> b) -> a -> b
    $ \ RW { [[HasGoal]]
    [(Range, Error)]
    [(Range, Warning)]
    [Map Name Type]
    [ModuleG ScopeName]
    Map Int HasGoalSln
    Map Name Schema
    Supply
    Subst
    Goals
    NameSeeds
    iSubst :: RW -> Subst
    iWarnings :: RW -> [(Range, Warning)]
    iErrors :: RW -> [(Range, Error)]
    iCts :: RW -> Goals
    iNameSeeds :: RW -> NameSeeds
    iSupply :: RW -> Supply
    iExistTVars :: RW -> [Map Name Type]
    iHasCts :: RW -> [[HasGoal]]
    iSolvedHas :: RW -> Map Int HasGoalSln
    iScope :: RW -> [ModuleG ScopeName]
    iBindTypes :: RW -> Map Name Schema
    iErrors :: [(Range, Error)]
    iWarnings :: [(Range, Warning)]
    iSubst :: Subst
    iExistTVars :: [Map Name Type]
    iSolvedHas :: Map Int HasGoalSln
    iNameSeeds :: NameSeeds
    iCts :: Goals
    iHasCts :: [[HasGoal]]
    iScope :: [ModuleG ScopeName]
    iBindTypes :: Map Name Schema
    iSupply :: Supply
    .. } -> ((),   RW { iCts :: Goals
    iCts = Goals
    gs, [[HasGoal]]
    [(Range, Error)]
    [(Range, Warning)]
    [Map Name Type]
    [ModuleG ScopeName]
    Map Int HasGoalSln
    Map Name Schema
    Supply
    Subst
    NameSeeds
    iSubst :: Subst
    iWarnings :: [(Range, Warning)]
    iErrors :: [(Range, Error)]
    iNameSeeds :: NameSeeds
    iSupply :: Supply
    iExistTVars :: [Map Name Type]
    iHasCts :: [[HasGoal]]
    iSolvedHas :: Map Int HasGoalSln
    iScope :: [ModuleG ScopeName]
    iBindTypes :: Map Name Schema
    iErrors :: [(Range, Error)]
    iWarnings :: [(Range, Warning)]
    iSubst :: Subst
    iExistTVars :: [Map Name Type]
    iSolvedHas :: Map Int HasGoalSln
    iNameSeeds :: NameSeeds
    iHasCts :: [[HasGoal]]
    iScope :: [ModuleG ScopeName]
    iBindTypes :: Map Name Schema
    iSupply :: Supply
    .. })

    simpGoal :: Goal -> InferM [Goal]
    simpGoal :: Goal -> InferM [Goal]
    simpGoal Goal
    g =
      case Ctxt -> Type -> Type
    Simple.simplify Ctxt
    forall a. Monoid a => a
    mempty (Goal -> Type
    goal Goal
    g) of
        Type
    p | Just Type
    t <- Type -> Maybe Type
    tIsError Type
    p ->
            do Error -> InferM ()
    recordError (Error -> InferM ()) -> Error -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ [Goal] -> Error
    UnsolvableGoals [Goal
    g { goal :: Type
    goal = Type
    t }]
               [Goal] -> InferM [Goal]
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          | [Type]
    ps <- Type -> [Type]
    pSplitAnd Type
    p -> [Goal] -> InferM [Goal]
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Goal
    g { goal :: Type
    goal = Type
    pr } | Type
    pr <- [Type]
    ps ]

    simpGoals :: [Goal] -> InferM [Goal]
    simpGoals :: [Goal] -> InferM [Goal]
    simpGoals [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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> Type -> Type -> InferM HasGoalSln
    newHasGoal Selector
    l Type
    ty Type
    f =
      do Int
    goalName <- InferM Int
    newGoalName
         Goal
    g        <- ConstraintSource -> Type -> InferM Goal
    newGoal ConstraintSource
    CtSelector (Selector -> Type -> Type -> Type
    pHas Selector
    l Type
    ty Type
    f)
         ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    s -> case RW -> [[HasGoal]]
    iHasCts RW
    s of
                            [HasGoal]
    cs : [[HasGoal]]
    more ->
                              RW
    s { iHasCts :: [[HasGoal]]
    iHasCts = (Int -> Goal -> HasGoal
    HasGoal Int
    goalName Goal
    g HasGoal -> [HasGoal] -> [HasGoal]
    forall a. a -> [a] -> [a]
    : [HasGoal]
    cs) [HasGoal] -> [[HasGoal]] -> [[HasGoal]]
    forall a. a -> [a] -> [a]
    : [[HasGoal]]
    more }
                            [] -> String -> [String] -> RW
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "newHasGoal" [String
    "no selector scope"]
         Map Int HasGoalSln
    solns    <- ReaderT
      RO
      (StateT RW (ExceptionT [(Range, Error)] IO))
      (Map Int HasGoalSln)
    -> InferM (Map Int HasGoalSln)
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT
       RO
       (StateT RW (ExceptionT [(Range, Error)] IO))
       (Map Int HasGoalSln)
     -> InferM (Map Int HasGoalSln))
    -> ReaderT
         RO
         (StateT RW (ExceptionT [(Range, Error)] IO))
         (Map Int HasGoalSln)
    -> InferM (Map Int HasGoalSln)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Int HasGoalSln)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> ReaderT
         RO
         (StateT RW (ExceptionT [(Range, Error)] IO))
         (Map Int HasGoalSln)
    forall a b.
    (a -> b)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RO -> Map Int HasGoalSln
    iSolvedHasLazy ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         HasGoalSln -> InferM HasGoalSln
    forall a. a -> InferM a
    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 HasGoalSln
    e1 -> HasGoalSln
    e1
                    Maybe HasGoalSln
    Nothing -> String -> [String] -> HasGoalSln
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "newHasGoal" [String
    "Unsolved has goal in result"]

    -- | Add a previously generated @Has@ constraint
    addHasGoal :: HasGoal -> InferM ()
    addHasGoal :: HasGoal -> InferM ()
    addHasGoal HasGoal
    g = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    s -> case RW -> [[HasGoal]]
    iHasCts RW
    s of
                                      [HasGoal]
    cs : [[HasGoal]]
    more -> RW
    s { iHasCts :: [[HasGoal]]
    iHasCts = (HasGoal
    g HasGoal -> [HasGoal] -> [HasGoal]
    forall a. a -> [a] -> [a]
    : [HasGoal]
    cs) [HasGoal] -> [[HasGoal]] -> [[HasGoal]]
    forall a. a -> [a] -> [a]
    : [[HasGoal]]
    more }
                                      [] -> String -> [String] -> RW
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "addHasGoal" [String
    "No selector scope"]

    -- | 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 (ExceptionT [(Range, Error)] IO)) [HasGoal]
    -> InferM [HasGoal]
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) [HasGoal]
     -> InferM [HasGoal])
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) [HasGoal]
    -> InferM [HasGoal]
    forall a b. (a -> b) -> a -> b
    $ (RW -> ([HasGoal], RW))
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) [HasGoal]
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets \RW
    s -> case RW -> [[HasGoal]]
    iHasCts RW
    s of
                                 [HasGoal]
    cs : [[HasGoal]]
    more -> ([HasGoal]
    cs, RW
    s { iHasCts :: [[HasGoal]]
    iHasCts = [] [HasGoal] -> [[HasGoal]] -> [[HasGoal]]
    forall a. a -> [a] -> [a]
    : [[HasGoal]]
    more })
                                 [] -> String -> [String] -> ([HasGoal], RW)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "getHasGoals" [String
    "No selector scope"]
         [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 Int
    n HasGoalSln
    e =
      ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW)
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ())
    -> (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a b. (a -> b) -> a -> b
    $ \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.
    newLocalName :: Namespace -> Ident -> InferM Name
    newLocalName :: Namespace -> Ident -> InferM Name
    newLocalName Namespace
    ns Ident
    x =
      do Range
    r <- InferM Range
    curRange
         (Supply -> (Name, Supply)) -> InferM Name
    forall a. (Supply -> (a, Supply)) -> InferM a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply (Namespace -> Ident -> Range -> Supply -> (Name, Supply)
    mkLocal Namespace
    ns Ident
    x Range
    r)

    newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a
    newName :: forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
    newName NameSeeds -> (a, NameSeeds)
    upd = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
     -> InferM a)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RW -> (a, RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets ((RW -> (a, RW))
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a)
    -> (RW -> (a, RW))
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall a b. (a -> b) -> a -> b
    $ \RW
    s -> let (a
    x,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
    $ \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
    + Int
    1})

    -- | Generate a new free type variable.
    newTVar :: TypeSource -> Kind -> InferM TVar
    newTVar :: TypeSource -> Kind -> InferM TVar
    newTVar TypeSource
    src Kind
    k = TypeSource -> Set TParam -> Kind -> InferM TVar
    newTVar' TypeSource
    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' :: TypeSource -> Set TParam -> Kind -> InferM TVar
    newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar
    newTVar' TypeSource
    src Set TParam
    extraBound 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 { tvarDesc :: TypeSource
    tvarDesc = TypeSource
    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
    $ \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
    + Int
    1 })

    -- | Check that the given "flavor" of parameter is allowed to
    --   have the given type, and raise an error if not
    checkParamKind :: TParam -> TPFlavor -> Kind -> InferM ()

    checkParamKind :: TParam -> TPFlavor -> Kind -> InferM ()
    checkParamKind TParam
    tp TPFlavor
    flav Kind
    k =
        case TPFlavor
    flav of
          TPModParam Name
    _     -> InferM ()
    starOrHash
          TPPropSynParam Name
    _ -> InferM ()
    starOrHashOrProp
          TPTySynParam Name
    _   -> InferM ()
    starOrHash
          TPSchemaParam Name
    _  -> InferM ()
    starOrHash
          TPNewtypeParam Name
    _ -> InferM ()
    starOrHash
          TPPrimParam Name
    _    -> InferM ()
    starOrHash
          TPFlavor
    TPUnifyVar       -> InferM ()
    starOrHash

      where
        starOrHashOrProp :: InferM ()
    starOrHashOrProp =
          case Kind
    k of
            Kind
    KNum  -> () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Kind
    KType -> () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Kind
    KProp -> () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Kind
    _ -> Error -> InferM ()
    recordError (TParam -> Kind -> Error
    BadParameterKind TParam
    tp Kind
    k)

        starOrHash :: InferM ()
    starOrHash =
          case Kind
    k of
            Kind
    KNum  -> () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Kind
    KType -> () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Kind
    _ -> Error -> InferM ()
    recordError (TParam -> Kind -> Error
    BadParameterKind TParam
    tp Kind
    k)

    -- | Generate a new free type variable.
    newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam
    newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam
    newTParam TParam Name
    nm TPFlavor
    flav Kind
    k =
      do let desc :: TVarInfo
    desc = TVarInfo { tvarDesc :: TypeSource
    tvarDesc = Name -> TypeSource
    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)
                             }
         TParam
    tp <- (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
    $ \NameSeeds
    s ->
                 let x :: Int
    x = NameSeeds -> Int
    seedTVar NameSeeds
    s
                 in (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
    + Int
    1 })

         TParam -> TPFlavor -> Kind -> InferM ()
    checkParamKind TParam
    tp TPFlavor
    flav Kind
    k
         TParam -> InferM TParam
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TParam
    tp

    -- | Generate a new version of a type parameter.  We use this when
    -- instantiating module parameters (the "backtick" imports)
    freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam
    freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam
    freshTParam Name -> TPFlavor
    mkF TParam
    tp = (NameSeeds -> (TParam, NameSeeds)) -> InferM TParam
    forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
    newName \NameSeeds
    s ->
      let u :: Int
    u = NameSeeds -> Int
    seedTVar NameSeeds
    s
      in ( TParam
    tp { tpUnique :: Int
    tpUnique = Int
    u
              , tpFlav :: TPFlavor
    tpFlav   = case TParam -> Maybe Name
    tpName TParam
    tp of
                             Just Name
    n -> Name -> TPFlavor
    mkF (Namespace -> Name -> Name
    asLocal Namespace
    NSType Name
    n)
                             Maybe Name
    Nothing -> TParam -> TPFlavor
    tpFlav TParam
    tp -- shouldn't happen?
              }
         , NameSeeds
    s  { seedTVar :: Int
    seedTVar = Int
    u Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 }
         )

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

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

    -- | Record that the two types should be syntactically equal.
    unify :: TypeWithSource -> Type -> InferM [Prop]
    unify :: TypeWithSource -> Type -> InferM [Type]
    unify (WithSource Type
    t1 TypeSource
    src Maybe Range
    rng) Type
    t2 =
      do Type
    t1' <- Type -> InferM Type
    forall t. TVars t => t -> InferM t
    applySubst Type
    t1
         Type
    t2' <- Type -> InferM Type
    forall t. TVars t => t -> InferM t
    applySubst Type
    t2
         let ((Subst
    su1, [Type]
    ps), [(Path, UnificationError)]
    errs) = Result MGU -> (MGU, [(Path, UnificationError)])
    forall a. Result a -> (a, [(Path, UnificationError)])
    runResult (Type -> Type -> Result MGU
    doMGU Type
    t1' Type
    t2')
         Subst -> InferM ()
    extendSubst Subst
    su1
         let toError :: (Path,UnificationError) -> Error
             toError :: (Path, UnificationError) -> Error
    toError (Path
    pa,UnificationError
    err) =
               case UnificationError
    err of
                 UniTypeLenMismatch Int
    _ Int
    _ -> TypeSource -> Path -> Type -> Type -> Error
    TypeMismatch TypeSource
    src Path
    rootPath Type
    t1' Type
    t2'
                 UniTypeMismatch Type
    s1 Type
    s2  -> TypeSource -> Path -> Type -> Type -> Error
    TypeMismatch TypeSource
    src Path
    pa Type
    s1 Type
    s2
                 UniKindMismatch Kind
    k1 Kind
    k2  -> Maybe TypeSource -> Kind -> Kind -> Error
    KindMismatch (TypeSource -> Maybe TypeSource
    forall a. a -> Maybe a
    Just TypeSource
    src) Kind
    k1 Kind
    k2
                 UniRecursive TVar
    x Type
    t       -> TypeSource -> Path -> Type -> Type -> Error
    RecursiveType TypeSource
    src Path
    pa (TVar -> Type
    TVar TVar
    x) Type
    t
                 UniNonPolyDepends TVar
    x [TParam]
    vs -> TypeSource -> Path -> Type -> [TParam] -> Error
    TypeVariableEscaped TypeSource
    src Path
    pa (TVar -> Type
    TVar TVar
    x) [TParam]
    vs
                 UniNonPoly TVar
    x Type
    t         -> TypeSource -> Path -> TVar -> Type -> Error
    NotForAll TypeSource
    src Path
    pa TVar
    x Type
    t
         case [(Path, UnificationError)]
    errs of
           [] -> [Type] -> InferM [Type]
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Type]
    ps
           [(Path, UnificationError)]
    _  -> do ((Path, UnificationError) -> InferM ())
    -> [(Path, UnificationError)] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Maybe Range -> Error -> InferM ()
    recordErrorLoc Maybe Range
    rng (Error -> InferM ())
    -> ((Path, UnificationError) -> Error)
    -> (Path, UnificationError)
    -> InferM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Path, UnificationError) -> Error
    toError) [(Path, UnificationError)]
    errs
                    [Type] -> InferM [Type]
    forall a. a -> InferM a
    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 :: forall t. TVars t => t -> InferM t
    applySubst t
    t =
      do Subst
    su <- InferM Subst
    getSubst
         t -> InferM t
    forall a. a -> InferM a
    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 :: [Type] -> InferM [Type]
    applySubstPreds [Type]
    ps =
      do [Type]
    ps1 <- [Type] -> InferM [Type]
    forall t. TVars t => t -> InferM t
    applySubst [Type]
    ps
         [Type] -> InferM [Type]
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Type -> [Type]) -> [Type] -> [Type]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Type -> [Type]
    pSplitAnd [Type]
    ps1)

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

    -- | Get the substitution that we have accumulated so far.
    getSubst :: InferM Subst
    getSubst :: InferM Subst
    getSubst = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Subst
    -> InferM Subst
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Subst
     -> InferM Subst)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Subst
    -> InferM Subst
    forall a b. (a -> b) -> a -> b
    $ (RW -> Subst)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Subst
    forall a b.
    (a -> b)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RW -> Subst
    iSubst ReaderT RO (StateT RW (ExceptionT [(Range, Error)] 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 Subst
    su =
      do ((TVar, Type) -> InferM ()) -> [(TVar, Type)] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (TVar, Type) -> InferM ()
    check (Subst -> [(TVar, Type)]
    substToList Subst
    su)
         ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW)
     -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ())
    -> (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall a b. (a -> b) -> a -> b
    $ \RW
    s -> RW
    s { iSubst :: Subst
    iSubst = Subst
    su Subst -> Subst -> Subst
    @@ RW -> Subst
    iSubst RW
    s }
      where
        check :: (TVar, Type) -> InferM ()
        check :: (TVar, Type) -> InferM ()
    check (TVar
    v, Type
    ty) =
          case TVar
    v of
            TVBound TParam
    _ ->
              String -> [String] -> InferM ()
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.TypeCheck.Monad.extendSubst"
                [ String
    "Substitution instantiates bound variable:"
                , String
    "Variable: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (TVar -> Doc
    forall a. PP a => a -> Doc
    pp TVar
    v)
                , String
    "Type:     " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    ty)
                ]
            TVFree Int
    _ Kind
    _ Set TParam
    tvs TVarInfo
    _ ->
              do let escaped :: Set TParam
    escaped = Set TParam -> Set TParam -> Set TParam
    forall a. Ord a => Set a -> Set a -> Set a
    Set.difference (Type -> Set TParam
    forall t. FVS t => t -> Set TParam
    freeParams Type
    ty) Set TParam
    tvs
                 if Set TParam -> Bool
    forall a. Set a -> Bool
    Set.null Set TParam
    escaped then () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () else
                   String -> [String] -> InferM ()
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.TypeCheck.Monad.extendSubst"
                     [ String
    "Escaped quantified variables:"
                     , String
    "Substitution:  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (TVar -> Doc
    forall a. PP a => a -> Doc
    pp TVar
    v Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":=" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    ty)
                     , String
    "Vars in scope: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    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))))
                     , String
    "Escaped:       " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    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 (ExceptionT [(Range, Error)] IO)) [VarType]
    -> InferM [VarType]
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) [VarType]
     -> InferM [VarType])
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) [VarType]
    -> InferM [VarType]
    forall a b. (a -> b) -> a -> b
    $ (RO -> [VarType])
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) [VarType]
    forall a b.
    (a -> b)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    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 (ExceptionT [(Range, Error)] 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
    $ \VarType
    v ->
                      case VarType
    v of
                        ExtVar Schema
    sch  -> Schema -> InferM (Set TVar)
    forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
    getVars Schema
    sch
                        CurSCC Expr
    _ Type
    t  -> Type -> InferM (Set TVar)
    forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
    getVars Type
    t
         [[HasGoal]]
    hasCts <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) [[HasGoal]]
    -> InferM [[HasGoal]]
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (RW -> [[HasGoal]]
    iHasCts (RW -> [[HasGoal]])
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) [[HasGoal]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get)
         let sels :: [Type]
    sels = (HasGoal -> Type) -> [HasGoal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Goal -> Type
    goal (Goal -> Type) -> (HasGoal -> Goal) -> HasGoal -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HasGoal -> Goal
    hasGoal) ([[HasGoal]] -> [HasGoal]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[HasGoal]]
    hasCts)
         [Set TVar]
    fromSels <- (Type -> InferM (Set TVar)) -> [Type] -> InferM [Set TVar]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Type -> InferM (Set TVar)
    forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
    getVars [Type]
    sels
         Set TVar
    fromEx   <- ([Type] -> InferM (Set TVar)
    forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
    getVars ([Type] -> InferM (Set TVar))
    -> ([Map Name Type] -> [Type])
    -> [Map Name Type]
    -> InferM (Set TVar)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Map Name Type -> [Type]) -> [Map Name Type] -> [Type]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Map Name Type -> [Type]
    forall k a. Map k a -> [a]
    Map.elems) ([Map Name Type] -> InferM (Set TVar))
    -> InferM [Map Name Type] -> InferM (Set TVar)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT
      RO (StateT RW (ExceptionT [(Range, Error)] IO)) [Map Name Type]
    -> InferM [Map Name Type]
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ((RW -> [Map Name Type])
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) [Map Name Type]
    forall a b.
    (a -> b)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RW -> [Map Name Type]
    iExistTVars ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get)
         Set TVar -> InferM (Set TVar)
    forall a. a -> InferM a
    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 :: a -> InferM (Set TVar)
    getVars a
    x = a -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (a -> Set TVar) -> InferM a -> InferM (Set TVar)
    forall a b. (a -> b) -> InferM a -> InferM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` a -> InferM a
    forall t. TVars t => t -> InferM t
    applySubst a
    x

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

    -- | Lookup the type of a variable.
    lookupVar :: Name -> InferM VarType
    lookupVar :: Name -> InferM VarType
    lookupVar Name
    x =
      do Maybe VarType
    mb <- ReaderT
      RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe VarType)
    -> InferM (Maybe VarType)
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT
       RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe VarType)
     -> InferM (Maybe VarType))
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe VarType)
    -> InferM (Maybe VarType)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Maybe VarType)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe VarType)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks ((RO -> Maybe VarType)
     -> ReaderT
          RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe VarType))
    -> (RO -> Maybe VarType)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] 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 VarType
    a  -> VarType -> InferM VarType
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure VarType
    a
           Maybe VarType
    Nothing ->
             do Maybe Schema
    mb1 <- Name -> Map Name Schema -> Maybe Schema
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name Schema -> Maybe Schema)
    -> (RW -> Map Name Schema) -> RW -> Maybe Schema
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RW -> Map Name Schema
    iBindTypes (RW -> Maybe Schema) -> InferM RW -> InferM (Maybe Schema)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> InferM RW
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
                case Maybe Schema
    mb1 of
                  Just Schema
    a -> VarType -> InferM VarType
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Schema -> VarType
    ExtVar Schema
    a)
                  Maybe Schema
    Nothing ->
                    do Map Name VarType
    mp <- ReaderT
      RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Map Name VarType)
    -> InferM (Map Name VarType)
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT
       RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Map Name VarType)
     -> InferM (Map Name VarType))
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Map Name VarType)
    -> InferM (Map Name VarType)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Map Name VarType)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Map Name VarType)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Map Name VarType
    iVars
                       String -> [String] -> InferM VarType
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "lookupVar" ([String] -> InferM VarType) -> [String] -> InferM VarType
    forall a b. (a -> b) -> a -> b
    $ [ String
    "Undefined vairable"
                                         , Name -> String
    forall a. Show a => a -> String
    show Name
    x
                                         , String
    "IVARS"
                                         ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (Name -> String) -> [Name] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> (Name -> Doc) -> Name -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> Doc
    debugShowUniques (Doc -> Doc) -> (Name -> Doc) -> Name -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Doc
    forall a. PP a => a -> Doc
    pp) (Map Name VarType -> [Name]
    forall k a. Map k a -> [k]
    Map.keys Map Name VarType
    mp)

    -- | 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 Name
    x = ReaderT
      RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe TParam)
    -> InferM (Maybe TParam)
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT
       RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe TParam)
     -> InferM (Maybe TParam))
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe TParam)
    -> InferM (Maybe TParam)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Maybe TParam)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe TParam)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks ((RO -> Maybe TParam)
     -> ReaderT
          RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Maybe TParam))
    -> (RO -> Maybe TParam)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] 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 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 Name
    x = Name -> Map Name TySyn -> Maybe TySyn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name TySyn -> Maybe TySyn)
    -> InferM (Map Name TySyn) -> InferM (Maybe TySyn)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (Map Name TySyn)
    getTSyns

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

    lookupAbstractType :: Name -> InferM (Maybe AbstractType)
    lookupAbstractType :: Name -> InferM (Maybe AbstractType)
    lookupAbstractType Name
    x = Name -> Map Name AbstractType -> Maybe AbstractType
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name AbstractType -> Maybe AbstractType)
    -> InferM (Map Name AbstractType) -> InferM (Maybe AbstractType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (Map Name AbstractType)
    getAbstractTypes

    -- | Lookup the kind of a parameter type
    lookupParamType :: Name -> InferM (Maybe ModTParam)
    lookupParamType :: Name -> InferM (Maybe ModTParam)
    lookupParamType 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

    lookupSignature :: P.ImpName Name -> InferM ModParamNames
    lookupSignature :: ImpName Name -> InferM ModParamNames
    lookupSignature ImpName Name
    nx =
      case ImpName Name
    nx of
        -- XXX: top
        P.ImpNested Name
    x ->
          do Map Name ModParamNames
    sigs <- InferM (Map Name ModParamNames)
    getSignatures
             case Name -> Map Name ModParamNames -> Maybe ModParamNames
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x Map Name ModParamNames
    sigs of
               Just ModParamNames
    ips -> ModParamNames -> InferM ModParamNames
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModParamNames
    ips
               Maybe ModParamNames
    Nothing  -> String -> [String] -> InferM ModParamNames
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "lookupSignature"
                            [ String
    "Missing signature", Name -> String
    forall a. Show a => a -> String
    show Name
    x ]

        P.ImpTop ModName
    t ->
          do ModName -> Maybe ModParamNames
    loaded <- RO -> ModName -> Maybe ModParamNames
    iExtSignatures (RO -> ModName -> Maybe ModParamNames)
    -> InferM RO -> InferM (ModName -> Maybe ModParamNames)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
             case ModName -> Maybe ModParamNames
    loaded ModName
    t of
               Just ModParamNames
    ps -> ModParamNames -> InferM ModParamNames
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModParamNames
    ps
               Maybe ModParamNames
    Nothing -> String -> [String] -> InferM ModParamNames
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "lookupSignature"
                            [ String
    "Top level signature is not loaded", Doc -> String
    forall a. Show a => a -> String
    show (ImpName Name -> Doc
    forall a. PP a => a -> Doc
    pp ImpName Name
    nx) ]

    -- | Lookup an external (i.e., previously loaded) top module.
    lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), If.IfaceG ()))
    lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
    lookupTopModule ModName
    m =
      do ModName -> Maybe (ModuleG (), IfaceG ())
    ms <- RO -> ModName -> Maybe (ModuleG (), IfaceG ())
    iExtModules (RO -> ModName -> Maybe (ModuleG (), IfaceG ()))
    -> InferM RO -> InferM (ModName -> Maybe (ModuleG (), IfaceG ()))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         Maybe (ModuleG (), IfaceG ())
    -> InferM (Maybe (ModuleG (), IfaceG ()))
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ModName -> Maybe (ModuleG (), IfaceG ())
    ms ModName
    m)

    lookupFunctor :: P.ImpName Name -> InferM (ModuleG ())
    lookupFunctor :: ImpName Name -> InferM (ModuleG ())
    lookupFunctor ImpName Name
    iname =
      case ImpName Name
    iname of
        P.ImpTop ModName
    m -> (ModuleG (), IfaceG ()) -> ModuleG ()
    forall a b. (a, b) -> a
    fst ((ModuleG (), IfaceG ()) -> ModuleG ())
    -> (Maybe (ModuleG (), IfaceG ()) -> (ModuleG (), IfaceG ()))
    -> Maybe (ModuleG (), IfaceG ())
    -> ModuleG ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe (ModuleG (), IfaceG ()) -> (ModuleG (), IfaceG ())
    forall {a}. Maybe a -> a
    fromMb (Maybe (ModuleG (), IfaceG ()) -> ModuleG ())
    -> InferM (Maybe (ModuleG (), IfaceG ())) -> InferM (ModuleG ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
    lookupTopModule ModName
    m
        P.ImpNested Name
    m ->
          do Map Name (ModuleG Name)
    localFuns <- (ModuleG ScopeName -> Map Name (ModuleG Name))
    -> InferM (Map Name (ModuleG Name))
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors
             case Name -> Map Name (ModuleG Name) -> Maybe (ModuleG Name)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    m Map Name (ModuleG Name)
    localFuns of
               Just ModuleG Name
    a -> ModuleG () -> InferM (ModuleG ())
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModuleG Name
    a { mName :: ()
    mName = () }
               Maybe (ModuleG Name)
    Nothing ->
                 do Maybe (ModuleG (), IfaceG ())
    mbTop <- ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
    lookupTopModule (Name -> ModName
    nameTopModule Name
    m)
                    ModuleG () -> InferM (ModuleG ())
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe (ModuleG ()) -> ModuleG ()
    forall {a}. Maybe a -> a
    fromMb do ModuleG ()
    a <- (ModuleG (), IfaceG ()) -> ModuleG ()
    forall a b. (a, b) -> a
    fst ((ModuleG (), IfaceG ()) -> ModuleG ())
    -> Maybe (ModuleG (), IfaceG ()) -> Maybe (ModuleG ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ModuleG (), IfaceG ())
    mbTop
                                    ModuleG Name
    b <- Name -> Map Name (ModuleG Name) -> Maybe (ModuleG Name)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    m (ModuleG () -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors ModuleG ()
    a)
                                    ModuleG () -> Maybe (ModuleG ())
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModuleG Name
    b { mName :: ()
    mName = () })
      where
      fromMb :: Maybe a -> a
    fromMb Maybe a
    mb = case Maybe a
    mb of
                    Just a
    a -> a
    a
                    Maybe a
    Nothing -> String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "lookupFunctor"
                                      [ String
    "Missing functor", ImpName Name -> String
    forall a. Show a => a -> String
    show ImpName Name
    iname ]

    {- | Get information about the things defined in the module.
    Note that, in general, the interface may contain *more* than just the
    definitions in the module, however the `ifNames` should indicate which
    ones are part of the module.
    -}
    lookupModule :: P.ImpName Name -> InferM (If.IfaceG ())
    lookupModule :: ImpName Name -> InferM (IfaceG ())
    lookupModule ImpName Name
    iname =
      case ImpName Name
    iname of
        P.ImpTop ModName
    m -> (ModuleG (), IfaceG ()) -> IfaceG ()
    forall a b. (a, b) -> b
    snd ((ModuleG (), IfaceG ()) -> IfaceG ())
    -> (Maybe (ModuleG (), IfaceG ()) -> (ModuleG (), IfaceG ()))
    -> Maybe (ModuleG (), IfaceG ())
    -> IfaceG ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe (ModuleG (), IfaceG ()) -> (ModuleG (), IfaceG ())
    forall {a}. Maybe a -> a
    fromMb (Maybe (ModuleG (), IfaceG ()) -> IfaceG ())
    -> InferM (Maybe (ModuleG (), IfaceG ())) -> InferM (IfaceG ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
    lookupTopModule ModName
    m
        P.ImpNested Name
    m ->
          do Map Name (IfaceNames Name)
    localMods <- (ModuleG ScopeName -> Map Name (IfaceNames Name))
    -> InferM (Map Name (IfaceNames Name))
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules
             case Name -> Map Name (IfaceNames Name) -> Maybe (IfaceNames Name)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    m Map Name (IfaceNames Name)
    localMods of
               Just IfaceNames Name
    names ->
                  do IfaceG Name
    n <- IfaceNames Name -> ModuleG () -> IfaceG Name
    forall name ignored.
    IfaceNames name -> ModuleG ignored -> IfaceG name
    genIfaceWithNames IfaceNames Name
    names (ModuleG () -> IfaceG Name)
    -> InferM (ModuleG ()) -> InferM (IfaceG Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (ModuleG ())
    getCurDecls
                     IfaceG () -> InferM (IfaceG ())
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (IfaceG Name -> IfaceG ()
    forall name. IfaceG name -> IfaceG ()
    If.ifaceForgetName IfaceG Name
    n)

               Maybe (IfaceNames Name)
    Nothing ->
                 do Maybe (ModuleG (), IfaceG ())
    mb <- ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
    lookupTopModule (Name -> ModName
    nameTopModule Name
    m)
                    IfaceG () -> InferM (IfaceG ())
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe (IfaceG ()) -> IfaceG ()
    forall {a}. Maybe a -> a
    fromMb
                             do IfaceG ()
    iface <- (ModuleG (), IfaceG ()) -> IfaceG ()
    forall a b. (a, b) -> b
    snd ((ModuleG (), IfaceG ()) -> IfaceG ())
    -> Maybe (ModuleG (), IfaceG ()) -> Maybe (IfaceG ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ModuleG (), IfaceG ())
    mb
                                IfaceNames Name
    names <- Name -> Map Name (IfaceNames Name) -> Maybe (IfaceNames Name)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    m
                                            (IfaceDecls -> Map Name (IfaceNames Name)
    If.ifModules (IfaceG () -> IfaceDecls
    forall name. IfaceG name -> IfaceDecls
    If.ifDefines IfaceG ()
    iface))
                                IfaceG () -> Maybe (IfaceG ())
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure IfaceG ()
    iface
                                       { ifNames :: IfaceNames ()
    If.ifNames = IfaceNames Name
    names { ifsName :: ()
    If.ifsName = () } })

      where
      fromMb :: Maybe a -> a
    fromMb Maybe a
    mb = case Maybe a
    mb of
                    Just a
    a -> a
    a
                    Maybe a
    Nothing -> String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "lookupModule"
                                      [ String
    "Missing module", ImpName Name -> String
    forall a. Show a => a -> String
    show ImpName Name
    iname ]

    lookupModParam :: P.Ident -> InferM (Maybe ModParam)
    lookupModParam :: Ident -> InferM (Maybe ModParam)
    lookupModParam Ident
    p =
      do FunctorParams
    scope <- (ModuleG ScopeName -> FunctorParams) -> InferM FunctorParams
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> FunctorParams
    forall mname. ModuleG mname -> FunctorParams
    mParams
         Maybe ModParam -> InferM (Maybe ModParam)
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Ident -> FunctorParams -> Maybe ModParam
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Ident
    p FunctorParams
    scope)

    -- | 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 Type
    existVar Name
    x Kind
    k =
      do [Map Name Type]
    scopes <- RW -> [Map Name Type]
    iExistTVars (RW -> [Map Name Type]) -> InferM RW -> InferM [Map Name Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> InferM RW
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         case [Maybe Type] -> Maybe Type
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ((Map Name Type -> Maybe Type) -> [Map Name Type] -> [Maybe Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Map Name Type -> Maybe Type
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x) [Map Name Type]
    scopes) of
           Just Type
    ty -> Type -> InferM Type
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    ty
           Maybe Type
    Nothing ->
             case [Map Name Type]
    scopes of
               [] ->
                  do Error -> InferM ()
    recordError (Name -> Error
    UndefinedExistVar Name
    x)
                     TypeSource -> Kind -> InferM Type
    newType TypeSource
    TypeErrorPlaceHolder Kind
    k

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

    -- | Returns the type synonyms that are currently in scope.
    getTSyns :: InferM (Map Name TySyn)
    getTSyns :: InferM (Map Name TySyn)
    getTSyns = (ModuleG ScopeName -> Map Name TySyn) -> InferM (Map Name TySyn)
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns

    -- | Returns the newtype declarations that are in scope.
    getNewtypes :: InferM (Map Name Newtype)
    getNewtypes :: InferM (Map Name Newtype)
    getNewtypes = (ModuleG ScopeName -> Map Name Newtype)
    -> InferM (Map Name Newtype)
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes

    -- | Returns the abstract type declarations that are in scope.
    getAbstractTypes :: InferM (Map Name AbstractType)
    getAbstractTypes :: InferM (Map Name AbstractType)
    getAbstractTypes = (ModuleG ScopeName -> Map Name AbstractType)
    -> InferM (Map Name AbstractType)
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes

    -- | Returns the abstract function declarations
    getParamTypes :: InferM (Map Name ModTParam)
    getParamTypes :: InferM (Map Name ModTParam)
    getParamTypes = (ModuleG ScopeName -> Map Name ModTParam)
    -> InferM (Map Name ModTParam)
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> Map Name ModTParam
    forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes

    -- | Constraints on the module's parameters.
    getParamConstraints :: InferM [Located Prop]
    getParamConstraints :: InferM [Located Type]
    getParamConstraints = (ModuleG ScopeName -> [Located Type]) -> InferM [Located Type]
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> [Located Type]
    forall mname. ModuleG mname -> [Located Type]
    mParamConstraints

    -- | Get the set of bound type variables that are in scope.
    getTVars :: InferM (Set Name)
    getTVars :: InferM (Set Name)
    getTVars = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Set Name)
    -> InferM (Set Name)
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Set Name)
     -> InferM (Set Name))
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Set Name)
    -> InferM (Set Name)
    forall a b. (a -> b) -> a -> b
    $ (RO -> Set Name)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Set Name)
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks ((RO -> Set Name)
     -> ReaderT
          RO (StateT RW (ExceptionT [(Range, Error)] IO)) (Set Name))
    -> (RO -> Set Name)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] 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 (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         Set TParam
    params <- [TParam] -> Set TParam
    forall a. Ord a => [a] -> Set a
    Set.fromList ([TParam] -> Set TParam)
    -> (Map Name ModTParam -> [TParam])
    -> Map Name ModTParam
    -> Set TParam
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ModTParam -> TParam) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> TParam
    mtpParam ([ModTParam] -> [TParam])
    -> (Map Name ModTParam -> [ModTParam])
    -> Map Name ModTParam
    -> [TParam]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems (Map Name ModTParam -> Set TParam)
    -> InferM (Map Name ModTParam) -> InferM (Set TParam)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (Map Name ModTParam)
    getParamTypes
         let 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 a. a -> InferM a
    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 (ExceptionT [(Range, Error)] IO)) Bool
    -> InferM Bool
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ((RO -> Bool)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Bool
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Bool
    iMonoBinds)

    getCallStacks :: InferM Bool
    getCallStacks :: InferM Bool
    getCallStacks = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Bool
    -> InferM Bool
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ((RO -> Bool)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) Bool
    forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
    asks RO -> Bool
    iCallStacks)

    getSignatures :: InferM (Map Name ModParamNames)
    getSignatures :: InferM (Map Name ModParamNames)
    getSignatures = (ModuleG ScopeName -> Map Name ModParamNames)
    -> InferM (Map Name ModParamNames)
    forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> Map Name ModParamNames
    forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures

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

    -- XXX: this should be done in renamer
    checkTShadowing :: String -> Name -> InferM ()
    checkTShadowing :: String -> Name -> InferM ()
    checkTShadowing String
    this Name
    new =
      do Map Name TySyn
    tsyns <- InferM (Map Name TySyn)
    getTSyns
         RO
    ro <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RW
    rw <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> InferM RW
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         let shadowed :: Maybe String
    shadowed =
               do TySyn
    _ <- Name -> Map Name TySyn -> Maybe TySyn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    new Map Name TySyn
    tsyns
                  String -> Maybe String
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "type synonym"
               Maybe String -> Maybe String -> Maybe String
    forall a. Maybe a -> Maybe a -> Maybe a
    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 a. Eq a => a -> [a] -> 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))
                  String -> Maybe String
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "type variable"
               Maybe String -> Maybe String -> Maybe String
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus`
               do Type
    _ <- [Maybe Type] -> Maybe Type
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ((Map Name Type -> Maybe Type) -> [Map Name Type] -> [Maybe Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Map Name Type -> Maybe Type
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    new) (RW -> [Map Name Type]
    iExistTVars RW
    rw))
                  String -> Maybe String
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    "type"

         case Maybe String
    shadowed of
           Maybe String
    Nothing -> () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
           Just String
    that ->
              Error -> InferM ()
    recordError (String -> Name -> String -> Error
    TypeShadowing String
    this Name
    new String
    that)

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

    withTParams :: [TParam] -> InferM a -> InferM a
    withTParams :: forall a. [TParam] -> InferM a -> InferM a
    withTParams [TParam]
    ps InferM a
    m = (TParam -> InferM a -> InferM a)
    -> InferM a -> [TParam] -> InferM a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    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

    -- | Execute the given computation in a new top scope.
    -- The sub-computation would typically be validating a module.
    newScope :: ScopeName -> InferM ()
    newScope :: ScopeName -> InferM ()
    newScope ScopeName
    nm = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    rw -> RW
    rw { iScope :: [ModuleG ScopeName]
    iScope = ScopeName -> ModuleG ScopeName
    forall mname. mname -> ModuleG mname
    emptyModule ScopeName
    nm ModuleG ScopeName -> [ModuleG ScopeName] -> [ModuleG ScopeName]
    forall a. a -> [a] -> [a]
    : RW -> [ModuleG ScopeName]
    iScope RW
    rw }

    newLocalScope :: InferM ()
    newLocalScope :: InferM ()
    newLocalScope = ScopeName -> InferM ()
    newScope ScopeName
    LocalScope

    newSignatureScope :: Name -> Maybe Text -> InferM ()
    newSignatureScope :: Name -> Maybe Text -> InferM ()
    newSignatureScope Name
    x Maybe Text
    doc =
      do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    o -> ModuleG ScopeName
    o { mNested :: Set Name
    mNested = Name -> Set Name -> Set Name
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Name
    x (ModuleG ScopeName -> Set Name
    forall mname. ModuleG mname -> Set Name
    mNested ModuleG ScopeName
    o) }
         ScopeName -> InferM ()
    newScope (Name -> Maybe Text -> ScopeName
    SignatureScope Name
    x Maybe Text
    doc)

    newTopSignatureScope :: ModName -> InferM ()
    newTopSignatureScope :: ModName -> InferM ()
    newTopSignatureScope ModName
    x = ScopeName -> InferM ()
    newScope (ModName -> ScopeName
    TopSignatureScope ModName
    x)

    {- | Start a new submodule scope.  The imports and exports are just used
    to initialize an empty module.  As we type check declarations they are
    added to this module's scope. -}
    newSubmoduleScope ::
      Name -> Maybe Text -> ExportSpec Name -> InferM ()
    newSubmoduleScope :: Name -> Maybe Text -> ExportSpec Name -> InferM ()
    newSubmoduleScope Name
    x Maybe Text
    docs ExportSpec Name
    e =
      do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    o -> ModuleG ScopeName
    o { mNested :: Set Name
    mNested = Name -> Set Name -> Set Name
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Name
    x (ModuleG ScopeName -> Set Name
    forall mname. ModuleG mname -> Set Name
    mNested ModuleG ScopeName
    o) }
         ScopeName -> InferM ()
    newScope (Name -> ScopeName
    SubModule Name
    x)
         (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    m -> ModuleG ScopeName
    m { mDoc :: Maybe Text
    mDoc = Maybe Text
    docs, mExports :: ExportSpec Name
    mExports = ExportSpec Name
    e }

    newModuleScope :: P.ModName -> ExportSpec Name -> InferM ()
    newModuleScope :: ModName -> ExportSpec Name -> InferM ()
    newModuleScope ModName
    x ExportSpec Name
    e =
      do ScopeName -> InferM ()
    newScope (ModName -> ScopeName
    MTopModule ModName
    x)
         (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    m -> ModuleG ScopeName
    m { mDoc :: Maybe Text
    mDoc = Maybe Text
    forall a. Maybe a
    Nothing, mExports :: ExportSpec Name
    mExports = ExportSpec Name
    e }

    -- | Update the current scope (first in the list). Assumes there is one.
    updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope ModuleG ScopeName -> ModuleG ScopeName
    f = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    rw -> RW
    rw { iScope :: [ModuleG ScopeName]
    iScope = [ModuleG ScopeName] -> [ModuleG ScopeName]
    upd (RW -> [ModuleG ScopeName]
    iScope RW
    rw) }
      where
      upd :: [ModuleG ScopeName] -> [ModuleG ScopeName]
    upd [ModuleG ScopeName]
    r =
        case [ModuleG ScopeName]
    r of
          []       -> String -> [String] -> [ModuleG ScopeName]
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "updTopScope" [ String
    "No top scope" ]
          ModuleG ScopeName
    s : [ModuleG ScopeName]
    more -> ModuleG ScopeName -> ModuleG ScopeName
    f ModuleG ScopeName
    s ModuleG ScopeName -> [ModuleG ScopeName] -> [ModuleG ScopeName]
    forall a. a -> [a] -> [a]
    : [ModuleG ScopeName]
    more

    endLocalScope :: InferM ([DeclGroup], Map Name TySyn)
    endLocalScope :: InferM ([DeclGroup], Map Name TySyn)
    endLocalScope =
      ReaderT
      RO
      (StateT RW (ExceptionT [(Range, Error)] IO))
      ([DeclGroup], Map Name TySyn)
    -> InferM ([DeclGroup], Map Name TySyn)
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT
       RO
       (StateT RW (ExceptionT [(Range, Error)] IO))
       ([DeclGroup], Map Name TySyn)
     -> InferM ([DeclGroup], Map Name TySyn))
    -> ReaderT
         RO
         (StateT RW (ExceptionT [(Range, Error)] IO))
         ([DeclGroup], Map Name TySyn)
    -> InferM ([DeclGroup], Map Name TySyn)
    forall a b. (a -> b) -> a -> b
    $ (RW -> (([DeclGroup], Map Name TySyn), RW))
    -> ReaderT
         RO
         (StateT RW (ExceptionT [(Range, Error)] IO))
         ([DeclGroup], Map Name TySyn)
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets \RW
    rw ->
           case RW -> [ModuleG ScopeName]
    iScope RW
    rw of
             ModuleG ScopeName
    x : [ModuleG ScopeName]
    xs | ScopeName
    LocalScope <- ModuleG ScopeName -> ScopeName
    forall mname. ModuleG mname -> mname
    mName ModuleG ScopeName
    x ->
                        ( ([DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a]
    reverse (ModuleG ScopeName -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls ModuleG ScopeName
    x), ModuleG ScopeName -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns ModuleG ScopeName
    x), RW
    rw { iScope :: [ModuleG ScopeName]
    iScope = [ModuleG ScopeName]
    xs })

             [ModuleG ScopeName]
    _ -> String -> [String] -> (([DeclGroup], Map Name TySyn), RW)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "endLocalScope" [String
    "Missing local scope"]

    endSubmodule :: InferM ()
    endSubmodule :: InferM ()
    endSubmodule =
      ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    rw ->
           case RW -> [ModuleG ScopeName]
    iScope RW
    rw of
             x :: ModuleG ScopeName
    x@Module { mName :: forall mname. ModuleG mname -> mname
    mName = SubModule Name
    m } : ModuleG ScopeName
    y : [ModuleG ScopeName]
    more -> RW
    rw { iScope :: [ModuleG ScopeName]
    iScope = ModuleG ScopeName
    z ModuleG ScopeName -> [ModuleG ScopeName] -> [ModuleG ScopeName]
    forall a. a -> [a] -> [a]
    : [ModuleG ScopeName]
    more }
               where
               x1 :: ModuleG Name
    x1    = ModuleG ScopeName
    x { mName :: Name
    mName = Name
    m, mDecls :: [DeclGroup]
    mDecls = [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a]
    reverse (ModuleG ScopeName -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls ModuleG ScopeName
    x) }

               isFun :: Bool
    isFun = ModuleG Name -> Bool
    forall mname. ModuleG mname -> Bool
    isParametrizedModule ModuleG Name
    x1

               add :: Monoid a => (ModuleG ScopeName -> a) -> a
               add :: forall a. Monoid a => (ModuleG ScopeName -> a) -> a
    add ModuleG ScopeName -> a
    f = if Bool
    isFun then ModuleG ScopeName -> a
    f ModuleG ScopeName
    y else ModuleG ScopeName -> a
    f ModuleG ScopeName
    x a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> ModuleG ScopeName -> a
    f ModuleG ScopeName
    y

               z :: ModuleG ScopeName
    z = Module
                     { mName :: ScopeName
    mName             = ModuleG ScopeName -> ScopeName
    forall mname. ModuleG mname -> mname
    mName ModuleG ScopeName
    y
                     , mDoc :: Maybe Text
    mDoc              = ModuleG ScopeName -> Maybe Text
    forall mname. ModuleG mname -> Maybe Text
    mDoc ModuleG ScopeName
    y
                     , mExports :: ExportSpec Name
    mExports          = ModuleG ScopeName -> ExportSpec Name
    forall mname. ModuleG mname -> ExportSpec Name
    mExports ModuleG ScopeName
    y
                     , mParamTypes :: Map Name ModTParam
    mParamTypes       = ModuleG ScopeName -> Map Name ModTParam
    forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes ModuleG ScopeName
    y
                     , mParamFuns :: Map Name ModVParam
    mParamFuns        = ModuleG ScopeName -> Map Name ModVParam
    forall mname. ModuleG mname -> Map Name ModVParam
    mParamFuns  ModuleG ScopeName
    y
                     , mParamConstraints :: [Located Type]
    mParamConstraints = ModuleG ScopeName -> [Located Type]
    forall mname. ModuleG mname -> [Located Type]
    mParamConstraints ModuleG ScopeName
    y
                     , mParams :: FunctorParams
    mParams           = ModuleG ScopeName -> FunctorParams
    forall mname. ModuleG mname -> FunctorParams
    mParams ModuleG ScopeName
    y
                     , mNested :: Set Name
    mNested           = ModuleG ScopeName -> Set Name
    forall mname. ModuleG mname -> Set Name
    mNested ModuleG ScopeName
    y

                     , mTySyns :: Map Name TySyn
    mTySyns      = (ModuleG ScopeName -> Map Name TySyn) -> Map Name TySyn
    forall a. Monoid a => (ModuleG ScopeName -> a) -> a
    add ModuleG ScopeName -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns
                     , mNewtypes :: Map Name Newtype
    mNewtypes    = (ModuleG ScopeName -> Map Name Newtype) -> Map Name Newtype
    forall a. Monoid a => (ModuleG ScopeName -> a) -> a
    add ModuleG ScopeName -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes
                     , mPrimTypes :: Map Name AbstractType
    mPrimTypes   = (ModuleG ScopeName -> Map Name AbstractType)
    -> Map Name AbstractType
    forall a. Monoid a => (ModuleG ScopeName -> a) -> a
    add ModuleG ScopeName -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes
                     , mDecls :: [DeclGroup]
    mDecls       = (ModuleG ScopeName -> [DeclGroup]) -> [DeclGroup]
    forall a. Monoid a => (ModuleG ScopeName -> a) -> a
    add ModuleG ScopeName -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls
                     , mSignatures :: Map Name ModParamNames
    mSignatures  = (ModuleG ScopeName -> Map Name ModParamNames)
    -> Map Name ModParamNames
    forall a. Monoid a => (ModuleG ScopeName -> a) -> a
    add ModuleG ScopeName -> Map Name ModParamNames
    forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures
                     , mSubmodules :: Map Name (IfaceNames Name)
    mSubmodules  = if Bool
    isFun
                                        then ModuleG ScopeName -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules ModuleG ScopeName
    y
                                        else Name
    -> IfaceNames Name
    -> Map Name (IfaceNames Name)
    -> Map Name (IfaceNames Name)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    m (ModuleG Name -> IfaceNames Name
    forall name. ModuleG name -> IfaceNames name
    genIfaceNames ModuleG Name
    x1)
                                                   (ModuleG ScopeName -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules ModuleG ScopeName
    x Map Name (IfaceNames Name)
    -> Map Name (IfaceNames Name) -> Map Name (IfaceNames Name)
    forall a. Semigroup a => a -> a -> a
    <> ModuleG ScopeName -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules ModuleG ScopeName
    y)
                     , mFunctors :: Map Name (ModuleG Name)
    mFunctors    = if Bool
    isFun
                                        then Name
    -> ModuleG Name
    -> Map Name (ModuleG Name)
    -> Map Name (ModuleG Name)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    m ModuleG Name
    x1 (ModuleG ScopeName -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors ModuleG ScopeName
    y)
                                        else ModuleG ScopeName -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors ModuleG ScopeName
    x Map Name (ModuleG Name)
    -> Map Name (ModuleG Name) -> Map Name (ModuleG Name)
    forall a. Semigroup a => a -> a -> a
    <> ModuleG ScopeName -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors ModuleG ScopeName
    y
                     }

             [ModuleG ScopeName]
    _ -> String -> [String] -> RW
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "endSubmodule" [ String
    "Not a submodule" ]

    endModule :: InferM TCTopEntity
    endModule :: InferM TCTopEntity
    endModule =
      ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
    -> InferM TCTopEntity
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT
       RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
     -> InferM TCTopEntity)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
    -> InferM TCTopEntity
    forall a b. (a -> b) -> a -> b
    $ (RW -> (TCTopEntity, RW))
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets \RW
    rw ->
        case RW -> [ModuleG ScopeName]
    iScope RW
    rw of
          [ ModuleG ScopeName
    x ] | MTopModule ModName
    m <- ModuleG ScopeName -> ScopeName
    forall mname. ModuleG mname -> mname
    mName ModuleG ScopeName
    x ->
            ( ModuleG ModName -> TCTopEntity
    TCTopModule ModuleG ScopeName
    x { mName :: ModName
    mName = ModName
    m, mDecls :: [DeclGroup]
    mDecls = [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a]
    reverse (ModuleG ScopeName -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls ModuleG ScopeName
    x) }
            , RW
    rw { iScope :: [ModuleG ScopeName]
    iScope = [] }
            )
          [ModuleG ScopeName]
    _ -> String -> [String] -> (TCTopEntity, RW)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "endModule" [ String
    "Not a single top module" ]

    endSignature :: InferM ()
    endSignature :: InferM ()
    endSignature =
      ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    rw ->
        case RW -> [ModuleG ScopeName]
    iScope RW
    rw of
          x :: ModuleG ScopeName
    x@Module { mName :: forall mname. ModuleG mname -> mname
    mName = SignatureScope Name
    m Maybe Text
    doc } : ModuleG ScopeName
    y : [ModuleG ScopeName]
    more ->
            RW
    rw { iScope :: [ModuleG ScopeName]
    iScope = ModuleG ScopeName
    z ModuleG ScopeName -> [ModuleG ScopeName] -> [ModuleG ScopeName]
    forall a. a -> [a] -> [a]
    : [ModuleG ScopeName]
    more }
            where
            z :: ModuleG ScopeName
    z   = ModuleG ScopeName
    y { mSignatures :: Map Name ModParamNames
    mSignatures = Name
    -> ModParamNames
    -> Map Name ModParamNames
    -> Map Name ModParamNames
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    m ModParamNames
    sig (ModuleG ScopeName -> Map Name ModParamNames
    forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures ModuleG ScopeName
    y) }
            sig :: ModParamNames
    sig = ModParamNames
                    { mpnTypes :: Map Name ModTParam
    mpnTypes       = ModuleG ScopeName -> Map Name ModTParam
    forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes ModuleG ScopeName
    x
                    , mpnConstraints :: [Located Type]
    mpnConstraints = ModuleG ScopeName -> [Located Type]
    forall mname. ModuleG mname -> [Located Type]
    mParamConstraints ModuleG ScopeName
    x
                    , mpnFuns :: Map Name ModVParam
    mpnFuns        = ModuleG ScopeName -> Map Name ModVParam
    forall mname. ModuleG mname -> Map Name ModVParam
    mParamFuns ModuleG ScopeName
    x
                    , mpnTySyn :: Map Name TySyn
    mpnTySyn       = ModuleG ScopeName -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns ModuleG ScopeName
    x
                    , mpnDoc :: Maybe Text
    mpnDoc         = Maybe Text
    doc
                    }
          [ModuleG ScopeName]
    _ -> String -> [String] -> RW
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "endSignature" [ String
    "Not a signature scope" ]

    endTopSignature :: InferM TCTopEntity
    endTopSignature :: InferM TCTopEntity
    endTopSignature =
      ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
    -> InferM TCTopEntity
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT
       RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
     -> InferM TCTopEntity)
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
    -> InferM TCTopEntity
    forall a b. (a -> b) -> a -> b
    $ (RW -> (TCTopEntity, RW))
    -> ReaderT
         RO (StateT RW (ExceptionT [(Range, Error)] IO)) TCTopEntity
    forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
    sets \RW
    rw ->
        case RW -> [ModuleG ScopeName]
    iScope RW
    rw of
          [ ModuleG ScopeName
    x ] | TopSignatureScope ModName
    m <- ModuleG ScopeName -> ScopeName
    forall mname. ModuleG mname -> mname
    mName ModuleG ScopeName
    x ->
            ( ModName -> ModParamNames -> TCTopEntity
    TCTopSignature ModName
    m ModParamNames
                                 { mpnTypes :: Map Name ModTParam
    mpnTypes       = ModuleG ScopeName -> Map Name ModTParam
    forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes ModuleG ScopeName
    x
                                 , mpnConstraints :: [Located Type]
    mpnConstraints = ModuleG ScopeName -> [Located Type]
    forall mname. ModuleG mname -> [Located Type]
    mParamConstraints ModuleG ScopeName
    x
                                 , mpnFuns :: Map Name ModVParam
    mpnFuns        = ModuleG ScopeName -> Map Name ModVParam
    forall mname. ModuleG mname -> Map Name ModVParam
    mParamFuns ModuleG ScopeName
    x
                                 , mpnTySyn :: Map Name TySyn
    mpnTySyn       = ModuleG ScopeName -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns ModuleG ScopeName
    x
                                 , mpnDoc :: Maybe Text
    mpnDoc         = Maybe Text
    forall a. Maybe a
    Nothing
                                 }
            , RW
    rw { iScope :: [ModuleG ScopeName]
    iScope = [] }
            )
          [ModuleG ScopeName]
    _ -> String -> [String] -> (TCTopEntity, RW)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "endTopSignature" [ String
    "Not a top-level signature" ]

    -- | Get an environment combining all nested scopes.
    getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope :: forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
    getScope ModuleG ScopeName -> a
    f =
      do RO
    ro <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RW
    rw <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> InferM RW
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         a -> InferM a
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NonEmpty a -> a
    forall a. Semigroup a => NonEmpty a -> a
    sconcat (ModuleG ScopeName -> a
    f (RO -> ModuleG ScopeName
    iExtScope RO
    ro) a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| (ModuleG ScopeName -> a) -> [ModuleG ScopeName] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map ModuleG ScopeName -> a
    f (RW -> [ModuleG ScopeName]
    iScope RW
    rw)))

    getCurDecls :: InferM (ModuleG ())
    getCurDecls :: InferM (ModuleG ())
    getCurDecls =
      do RO
    ro <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    -> InferM RO
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RW
    rw <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    -> InferM RW
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RW
    forall (m :: * -> *) i. StateM m i => m i
    get
         ModuleG () -> InferM (ModuleG ())
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((ModuleG ScopeName -> ModuleG () -> ModuleG ())
    -> ModuleG () -> [ModuleG ScopeName] -> ModuleG ()
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ModuleG ScopeName
    m1 ModuleG ()
    m2 -> ModuleG () -> ModuleG () -> ModuleG ()
    forall {mname}. ModuleG mname -> ModuleG mname -> ModuleG ()
    mergeDecls (ModuleG ScopeName -> ModuleG ()
    forall {mname}. ModuleG mname -> ModuleG ()
    forget ModuleG ScopeName
    m1) ModuleG ()
    m2)
                    (ModuleG ScopeName -> ModuleG ()
    forall {mname}. ModuleG mname -> ModuleG ()
    forget (RO -> ModuleG ScopeName
    iExtScope RO
    ro)) (RW -> [ModuleG ScopeName]
    iScope RW
    rw))

      where
      forget :: ModuleG mname -> ModuleG ()
    forget ModuleG mname
    m = ModuleG mname
    m { mName :: ()
    mName = () }

      mergeDecls :: ModuleG mname -> ModuleG mname -> ModuleG ()
    mergeDecls ModuleG mname
    m1 ModuleG mname
    m2 =
        Module
          { mName :: ()
    mName             = ()
          , mDoc :: Maybe Text
    mDoc              = Maybe Text
    forall a. Maybe a
    Nothing
          , mExports :: ExportSpec Name
    mExports          = ExportSpec Name
    forall a. Monoid a => a
    mempty
          , mParams :: FunctorParams
    mParams           = FunctorParams
    forall a. Monoid a => a
    mempty
          , mParamTypes :: Map Name ModTParam
    mParamTypes       = Map Name ModTParam
    forall a. Monoid a => a
    mempty
          , mParamConstraints :: [Located Type]
    mParamConstraints = [Located Type]
    forall a. Monoid a => a
    mempty
          , mParamFuns :: Map Name ModVParam
    mParamFuns        = Map Name ModVParam
    forall a. Monoid a => a
    mempty
          , mNested :: Set Name
    mNested           = Set Name
    forall a. Monoid a => a
    mempty

          , mTySyns :: Map Name TySyn
    mTySyns           = (ModuleG mname -> Map Name TySyn) -> Map Name TySyn
    forall {a}. Semigroup a => (ModuleG mname -> a) -> a
    uni ModuleG mname -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns
          , mNewtypes :: Map Name Newtype
    mNewtypes         = (ModuleG mname -> Map Name Newtype) -> Map Name Newtype
    forall {a}. Semigroup a => (ModuleG mname -> a) -> a
    uni ModuleG mname -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes
          , mPrimTypes :: Map Name AbstractType
    mPrimTypes        = (ModuleG mname -> Map Name AbstractType) -> Map Name AbstractType
    forall {a}. Semigroup a => (ModuleG mname -> a) -> a
    uni ModuleG mname -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes
          , mDecls :: [DeclGroup]
    mDecls            = (ModuleG mname -> [DeclGroup]) -> [DeclGroup]
    forall {a}. Semigroup a => (ModuleG mname -> a) -> a
    uni ModuleG mname -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls
          , mSubmodules :: Map Name (IfaceNames Name)
    mSubmodules       = (ModuleG mname -> Map Name (IfaceNames Name))
    -> Map Name (IfaceNames Name)
    forall {a}. Semigroup a => (ModuleG mname -> a) -> a
    uni ModuleG mname -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules
          , mFunctors :: Map Name (ModuleG Name)
    mFunctors         = (ModuleG mname -> Map Name (ModuleG Name))
    -> Map Name (ModuleG Name)
    forall {a}. Semigroup a => (ModuleG mname -> a) -> a
    uni ModuleG mname -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors
          , mSignatures :: Map Name ModParamNames
    mSignatures       = (ModuleG mname -> Map Name ModParamNames) -> Map Name ModParamNames
    forall {a}. Semigroup a => (ModuleG mname -> a) -> a
    uni ModuleG mname -> Map Name ModParamNames
    forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures
          }
        where
        uni :: (ModuleG mname -> a) -> a
    uni ModuleG mname -> a
    f = ModuleG mname -> a
    f ModuleG mname
    m1 a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> ModuleG mname -> a
    f ModuleG mname
    m2

    addDecls :: DeclGroup -> InferM ()
    addDecls :: DeclGroup -> InferM ()
    addDecls DeclGroup
    ds =
      do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mDecls :: [DeclGroup]
    mDecls = DeclGroup
    ds DeclGroup -> [DeclGroup] -> [DeclGroup]
    forall a. a -> [a] -> [a]
    : ModuleG ScopeName -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls ModuleG ScopeName
    r }
         ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    rw -> RW
    rw { iBindTypes :: Map Name Schema
    iBindTypes = RW -> Map Name Schema
    new RW
    rw }
      where
      add :: Decl -> Map Name Schema -> Map Name Schema
    add Decl
    d   = Name -> Schema -> Map Name Schema -> Map Name Schema
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (Decl -> Name
    dName Decl
    d) (Decl -> Schema
    dSignature Decl
    d)
      new :: RW -> Map Name Schema
    new RW
    rw  = (Decl -> Map Name Schema -> Map Name Schema)
    -> Map Name Schema -> [Decl] -> Map Name Schema
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Decl -> Map Name Schema -> Map Name Schema
    add (RW -> Map Name Schema
    iBindTypes RW
    rw) (DeclGroup -> [Decl]
    groupDecls DeclGroup
    ds)

    -- | The sub-computation is performed with the given type-synonym in scope.
    addTySyn :: TySyn -> InferM ()
    addTySyn :: TySyn -> InferM ()
    addTySyn TySyn
    t =
      do let x :: Name
    x = TySyn -> Name
    tsName TySyn
    t
         String -> Name -> InferM ()
    checkTShadowing String
    "synonym" Name
    x
         (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mTySyns :: Map Name TySyn
    mTySyns = Name -> TySyn -> Map Name TySyn -> Map Name TySyn
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    x TySyn
    t (ModuleG ScopeName -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns ModuleG ScopeName
    r) }

    addNewtype :: Newtype -> InferM ()
    addNewtype :: Newtype -> InferM ()
    addNewtype Newtype
    t =
      do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mNewtypes :: Map Name Newtype
    mNewtypes = Name -> Newtype -> Map Name Newtype -> Map Name Newtype
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (Newtype -> Name
    ntName Newtype
    t) Newtype
    t (ModuleG ScopeName -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes ModuleG ScopeName
    r) }
         ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    rw -> RW
    rw { iBindTypes :: Map Name Schema
    iBindTypes = Name -> Schema -> Map Name Schema -> Map Name Schema
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (Newtype -> Name
    ntConName Newtype
    t)
                                                        (Newtype -> Schema
    newtypeConType Newtype
    t)
                                                        (RW -> Map Name Schema
    iBindTypes RW
    rw) }

    addPrimType :: AbstractType -> InferM ()
    addPrimType :: AbstractType -> InferM ()
    addPrimType AbstractType
    t =
      (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r ->
        ModuleG ScopeName
    r { mPrimTypes :: Map Name AbstractType
    mPrimTypes = Name
    -> AbstractType -> Map Name AbstractType -> Map Name AbstractType
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (AbstractType -> Name
    atName AbstractType
    t) AbstractType
    t (ModuleG ScopeName -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes ModuleG ScopeName
    r) }

    addParamType :: ModTParam -> InferM ()
    addParamType :: ModTParam -> InferM ()
    addParamType ModTParam
    a =
      (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mParamTypes :: Map Name ModTParam
    mParamTypes = 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 (ModuleG ScopeName -> Map Name ModTParam
    forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes ModuleG ScopeName
    r) }

    addSignatures :: Map Name ModParamNames -> InferM ()
    addSignatures :: Map Name ModParamNames -> InferM ()
    addSignatures Map Name ModParamNames
    mp =
      (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mSignatures :: Map Name ModParamNames
    mSignatures = Map Name ModParamNames
    -> Map Name ModParamNames -> Map Name ModParamNames
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map Name ModParamNames
    mp (ModuleG ScopeName -> Map Name ModParamNames
    forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures ModuleG ScopeName
    r) }

    addSubmodules :: Map Name (If.IfaceNames Name) -> InferM ()
    addSubmodules :: Map Name (IfaceNames Name) -> InferM ()
    addSubmodules Map Name (IfaceNames Name)
    mp =
      (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mSubmodules :: Map Name (IfaceNames Name)
    mSubmodules = Map Name (IfaceNames Name)
    -> Map Name (IfaceNames Name) -> Map Name (IfaceNames Name)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map Name (IfaceNames Name)
    mp (ModuleG ScopeName -> Map Name (IfaceNames Name)
    forall mname. ModuleG mname -> Map Name (IfaceNames Name)
    mSubmodules ModuleG ScopeName
    r) }

    addFunctors :: Map Name (ModuleG Name) -> InferM ()
    addFunctors :: Map Name (ModuleG Name) -> InferM ()
    addFunctors Map Name (ModuleG Name)
    mp =
      (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mFunctors :: Map Name (ModuleG Name)
    mFunctors = Map Name (ModuleG Name)
    -> Map Name (ModuleG Name) -> Map Name (ModuleG Name)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map Name (ModuleG Name)
    mp (ModuleG ScopeName -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors ModuleG ScopeName
    r) }

    -- | The sub-computation is performed with the given abstract function in scope.
    addParamFun :: ModVParam -> InferM ()
    addParamFun :: ModVParam -> InferM ()
    addParamFun ModVParam
    x =
      do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mParamFuns :: Map Name ModVParam
    mParamFuns = 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 (ModuleG ScopeName -> Map Name ModVParam
    forall mname. ModuleG mname -> Map Name ModVParam
    mParamFuns ModuleG ScopeName
    r) }
         ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
     -> InferM ())
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ (RW -> RW)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ \RW
    rw -> RW
    rw { iBindTypes :: Map Name Schema
    iBindTypes = Name -> Schema -> Map Name Schema -> Map Name Schema
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (ModVParam -> Name
    mvpName ModVParam
    x) (ModVParam -> Schema
    mvpType ModVParam
    x)
                                                        (RW -> Map Name Schema
    iBindTypes RW
    rw) }

    -- | Add some assumptions for an entire module
    addParameterConstraints :: [Located Prop] -> InferM ()
    addParameterConstraints :: [Located Type] -> InferM ()
    addParameterConstraints [Located Type]
    ps =
      (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mParamConstraints :: [Located Type]
    mParamConstraints = [Located Type]
    ps [Located Type] -> [Located Type] -> [Located Type]
    forall a. [a] -> [a] -> [a]
    ++ ModuleG ScopeName -> [Located Type]
    forall mname. ModuleG mname -> [Located Type]
    mParamConstraints ModuleG ScopeName
    r }

    addModParam :: ModParam -> InferM ()
    addModParam :: ModParam -> InferM ()
    addModParam ModParam
    p =
      (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
    updScope \ModuleG ScopeName
    r -> ModuleG ScopeName
    r { mParams :: FunctorParams
    mParams = Ident -> ModParam -> FunctorParams -> FunctorParams
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (ModParam -> Ident
    mpName ModParam
    p) ModParam
    p (ModuleG ScopeName -> FunctorParams
    forall mname. ModuleG mname -> FunctorParams
    mParams ModuleG ScopeName
    r) }

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

    -- | The sub-computation is performed with the given variable in scope.
    withVarType :: Name -> VarType -> InferM a -> InferM a
    withVarType :: forall a. Name -> VarType -> InferM a -> InferM a
    withVarType Name
    x VarType
    s (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    m) =
      ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a.
    ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
     -> InferM a)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> InferM a
    forall a b. (a -> b) -> a -> b
    $ (RO -> RO)
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\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 (ExceptionT [(Range, Error)] IO)) a
    m

    withVarTypes :: [(Name,VarType)] -> InferM a -> InferM a
    withVarTypes :: forall a. [(Name, VarType)] -> InferM a -> InferM a
    withVarTypes [(Name, VarType)]
    xs InferM a
    m = ((Name, VarType) -> InferM a -> InferM a)
    -> InferM a -> [(Name, VarType)] -> InferM a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    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 :: forall a. Name -> Schema -> InferM a -> InferM a
    withVar Name
    x 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 variables in scope.
    withMonoType :: (Name,Located Type) -> InferM a -> InferM a
    withMonoType :: forall a. (Name, Located Type) -> InferM a -> InferM a
    withMonoType (Name
    x,Located Type
    lt) = Name -> Schema -> InferM a -> InferM a
    forall a. Name -> Schema -> InferM a -> InferM a
    withVar Name
    x ([TParam] -> [Type] -> Type -> Schema
    Forall [] [] (Located Type -> Type
    forall a. Located a -> a
    thing Located Type
    lt))

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

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

    newtype KindM a = KM { forall a. 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, [Type])]
    kCtrs      :: [(ConstraintSource,[Prop])]
                   }

    instance Functor KindM where
      fmap :: forall a b. (a -> b) -> KindM a -> KindM b
    fmap a -> b
    f (KM 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 a b.
    (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 :: forall a. a -> KindM a
    pure 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 a. a -> ReaderT KRO (StateT KRW InferM) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x)
      <*> :: forall a b. 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 :: forall a. a -> KindM a
    return        = a -> KindM a
    forall a. a -> KindM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      KM ReaderT KRO (StateT KRW InferM) a
    m >>= :: forall a b. KindM a -> (a -> KindM b) -> KindM b
    >>= 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 a b.
    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 Fail.MonadFail KindM where
      fail :: forall a. String -> KindM a
    fail String
    x        = ReaderT KRO (StateT KRW InferM) a -> KindM a
    forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
    KM (String -> ReaderT KRO (StateT KRW InferM) a
    forall a. String -> ReaderT KRO (StateT KRW InferM) a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    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 :: forall a.
    AllowWildCards
    -> [(Name, Maybe Kind, TParam)]
    -> KindM a
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Type])])
    runKindM AllowWildCards
    wildOK [(Name, Maybe Kind, TParam)]
    vs (KM ReaderT KRO (StateT KRW InferM) a
    m) =
      do (a
    a,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, [Type])])
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Type])])
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    a, KRW -> Map Name Kind
    typeParams KRW
    kw, KRW -> [(ConstraintSource, [Type])]
    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) | (Name
    x,Maybe Kind
    _,TParam
    t)      <- [(Name, Maybe Kind, TParam)]
    vs ]
      kro :: KRO
    kro  = KRO { allowWild :: AllowWildCards
    allowWild = AllowWildCards
    wildOK, lazyTParams :: Map Name TParam
    lazyTParams = Map Name TParam
    tps }
      krw :: KRW
    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) | (Name
    x,Just Kind
    k,TParam
    _) <- [(Name, Maybe Kind, TParam)]
    vs ]
                 , kCtrs :: [(ConstraintSource, [Type])]
    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 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 a b.
    (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` 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 TParam
    t  -> Maybe LkpTyVar -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    forall a. a -> ReaderT KRO (StateT KRW InferM) a
    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
           Maybe TParam
    Nothing -> StateT KRW InferM (Maybe LkpTyVar)
    -> ReaderT KRO (StateT KRW InferM) (Maybe LkpTyVar)
    forall (m :: * -> *) a. Monad m => m a -> ReaderT KRO m a
    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 (m :: * -> *) a. Monad m => m a -> StateT KRW m a
    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 a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TParam -> LkpTyVar) -> Maybe TParam -> Maybe LkpTyVar
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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 a b.
    (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 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 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 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 :: forall a. IO a -> KindM a
    kIO 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 (m :: * -> *) a. Monad m => m a -> ReaderT KRO m 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 (m :: * -> *) a. Monad m => m a -> StateT KRW m 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 :: TypeSource -> Kind -> KindM Type
    kNewType :: TypeSource -> Kind -> KindM Type
    kNewType TypeSource
    src 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 a. a -> ReaderT KRO (StateT KRW InferM) a
    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 Type -> KindM Type
    forall a. InferM a -> KindM a
    kInInferM (InferM Type -> KindM Type) -> InferM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $ TVar -> Type
    TVar (TVar -> Type) -> InferM TVar -> InferM Type
    forall a b. (a -> b) -> InferM a -> InferM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` TypeSource -> Set TParam -> Kind -> InferM TVar
    newTVar' TypeSource
    src Set TParam
    tps Kind
    k

    -- | Lookup the definition of a type synonym.
    kLookupTSyn :: Name -> KindM (Maybe TySyn)
    kLookupTSyn :: Name -> KindM (Maybe TySyn)
    kLookupTSyn 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 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 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 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 Type
    kExistTVar Name
    x Kind
    k = InferM Type -> KindM Type
    forall a. InferM a -> KindM a
    kInInferM (InferM Type -> KindM Type) -> InferM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $ Name -> Kind -> InferM Type
    existVar Name
    x Kind
    k

    -- | Replace the given bound variables with concrete types.
    kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
    kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
    kInstantiateT Type
    t [(TParam, Type)]
    as = Type -> KindM Type
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
      where su :: Subst
    su = [(TParam, Type)] -> Subst
    listParamSubst [(TParam, Type)]
    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 Name
    v 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
    $ \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 :: forall a. Range -> KindM a -> KindM a
    kInRange Range
    r (KM 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,KRW
    s1) <- StateT KRW InferM (a, KRW)
    -> ReaderT KRO (StateT KRW InferM) (a, KRW)
    forall (m :: * -> *) a. Monad m => m a -> ReaderT KRO m a
    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 (m :: * -> *) a. Monad m => m a -> StateT KRW m a
    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 a. a -> ReaderT KRO (StateT KRW InferM) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
    kNewGoals :: ConstraintSource -> [Type] -> KindM ()
    kNewGoals ConstraintSource
    _ [] = () -> KindM ()
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    kNewGoals ConstraintSource
    c [Type]
    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
    $ \KRW
    s -> KRW
    s { kCtrs :: [(ConstraintSource, [Type])]
    kCtrs = (ConstraintSource
    c,[Type]
    ps) (ConstraintSource, [Type])
    -> [(ConstraintSource, [Type])] -> [(ConstraintSource, [Type])]
    forall a. a -> [a] -> [a]
    : KRW -> [(ConstraintSource, [Type])]
    kCtrs KRW
    s }

    kInInferM :: InferM a -> KindM a
    kInInferM :: forall a. InferM a -> KindM a
    kInInferM 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 (m :: * -> *) a. Monad m => m a -> ReaderT KRO m 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 (m :: * -> *) a. Monad m => m a -> StateT KRW m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift InferM a
    m