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

-- | The initial seeds, used when checking a fresh program.
-- XXX: why does this start at 10?
nameSeeds :: NameSeeds
nameSeeds :: NameSeeds
nameSeeds = 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
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
showList :: [InferOutput a] -> ShowS
$cshowList :: forall a. Show a => [InferOutput a] -> ShowS
show :: InferOutput a -> String
$cshow :: forall a. Show a => InferOutput a -> String
showsPrec :: Int -> InferOutput a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> InferOutput a -> ShowS
Show

bumpCounter :: InferM ()
bumpCounter :: InferM ()
bumpCounter = do RO { Bool
[TParam]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iCallStacks :: RO -> Bool
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iExtScope :: RO -> ModuleG ScopeName
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iCallStacks :: Bool
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iExtScope :: ModuleG ScopeName
iExtSignatures :: ModName -> Maybe ModParamNames
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
.. } <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
                 forall a. IO a -> InferM a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
iSolveCounter (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 = forall a. InferM a -> InferM a
selectorScope InferM a
m0
     IORef Int
counter <- forall a. a -> IO (IORef a)
newIORef Int
0
     let allPs :: ModParamNames
allPs = InferInput -> ModParamNames
inpParams InferInput
info

     let env :: Map Name VarType
env = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Schema -> VarType
ExtVar (InferInput -> Map Name Schema
inpVars InferInput
info)
            forall a. Semigroup a => a -> a -> a
<> 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 <- forall k a. Map k a -> [a]
Map.elems (InferInput -> Map Name Newtype
inpNewtypes InferInput
info)
              ]
            forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Schema -> VarType
ExtVar 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 = (forall mname. mname -> ModuleG mname
emptyModule ScopeName
ExternalScope)
                             { mTySyns :: Map Name TySyn
mTySyns           = InferInput -> Map Name TySyn
inpTSyns InferInput
info 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 = 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 <- forall i (m :: * -> *) a. ExceptionT i m a -> m (Either i a)
runExceptionT (forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT RW
rw (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 -> 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    = forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (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 -> 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)
                                         (forall t. TVars t => Subst -> t -> t
apSubst Subst
defSu a
result)
                  Goals
cts ->
                     forall {f :: * -> *} {a}.
Applicative f =>
[(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
inferFailed [(Range, Warning)]
warns
                       [ ( Goal -> Range
goalRange Goal
g
                         , [Goal] -> Error
UnsolvedGoals [forall t. TVars t => Subst -> t -> t
apSubst Subst
theSu Goal
g]
                         ) | Goal
g <- Goals -> [Goal]
fromGoals Goals
cts
                       ]

              [(Range, Error)]
errs -> forall {f :: * -> *} {a}.
Applicative f =>
[(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
inferFailed [(Range, Warning)]
warns [(Range
r,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  = forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 forall (f :: * -> *) a. Applicative f => a -> f a
pure (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  = 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  = 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) = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM
  do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
     RW
rw <- forall (m :: * -> *) i. StateM m i => m i
get
     Either [(Range, Error)] (a, RW)
mb <- 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 = [] forall a. a -> [a] -> [a]
: RW -> [[HasGoal]]
iHasCts RW
rw }
                  Either [(Range, Error)] (a, RW)
mb <- forall i (m :: * -> *) a. ExceptionT i m a -> m (Either i a)
runExceptionT (forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT RW
rw1 (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 {} -> forall k a. Map k a
Map.empty
                                 Right (a
_,RW
rw2) -> RW -> Map Int HasGoalSln
iSolvedHas RW
rw2
              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      -> 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 <- forall a b. (a -> b) -> [a] -> [b]
map HasGoal -> Goal
hasGoal [HasGoal]
us ]
                forall (m :: * -> *) i. StateM m i => i -> m ()
set RW
rw1 { iErrors :: [(Range, Error)]
iErrors = [(Range, Error)]
errs forall a. [a] -> [a] -> [a]
++ RW -> [(Range, Error)]
iErrors RW
rw1, iHasCts :: [[HasGoal]]
iHasCts = [[HasGoal]]
cs }
                forall a.
InferM a
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
unIM (InferM ()
abortIfErrors)
                forall (f :: * -> *) a. Applicative f => a -> f a
pure a
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) = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
  <*> :: forall a 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        = 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    = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a.
InferM a
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
unIM 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        = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (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        = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (forall a.
InferM a
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
unIM 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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$
    do RW
rw <- forall (m :: * -> *) i. StateM m i => m i
get
       let (a
a,Supply
s') = Supply -> (a, Supply)
f (RW -> Supply
iSupply RW
rw)
       forall (m :: * -> *) i. StateM m i => i -> m ()
set RW
rw { iSupply :: Supply
iSupply = Supply
s' }
       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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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) = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 = 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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 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  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Range
r
            Maybe Range
Nothing -> case Error
e of
                         AmbiguousSize TVarInfo
d Maybe Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (TVarInfo -> Range
tvarSource TVarInfo
d)
                         Error
_                 -> InferM Range
curRange
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iErrors :: [(Range, Error)]
iErrors = (Range
r,Error
e) 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 <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
     case RW -> [(Range, Error)]
iErrors RW
rw of
       [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
       [(Range, Error)]
es ->
         do [(Range, Error)]
es1 <- 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 <- forall t. TVars t => t -> InferM t
applySubst Error
e
                         forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range
l,Error
e1)
            forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise [(Range, Error)]
es1)

recordWarning :: Warning -> InferM ()
recordWarning :: Warning -> InferM ()
recordWarning Warning
w =
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ignore forall a b. (a -> b) -> a -> b
$
  do Range
r <- case Warning
w of
            DefaultingTo TVarInfo
d Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (TVarInfo -> Range
tvarSource TVarInfo
d)
            Warning
_ -> InferM Range
curRange
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iWarnings :: [(Range, Warning)]
iWarnings = (Range
r,Warning
w) 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]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iCallStacks :: Bool
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iExtScope :: ModuleG ScopeName
iExtSignatures :: ModName -> Maybe ModParamNames
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iCallStacks :: RO -> Bool
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iExtScope :: RO -> ModuleG ScopeName
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
.. } <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
     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]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iCallStacks :: Bool
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iExtScope :: ModuleG ScopeName
iExtSignatures :: ModName -> Maybe ModParamNames
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iCallStacks :: RO -> Bool
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iExtScope :: RO -> ModuleG ScopeName
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
.. } <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
     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
     forall (m :: * -> *) a. Monad m => a -> m a
return Goal { Range
Type
ConstraintSource
goal :: Type
goalSource :: ConstraintSource
goalRange :: Range
goal :: Type
goalSource :: ConstraintSource
goalRange :: Range
.. }

-- | 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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 <- forall t. TVars t => t -> InferM t
applySubst forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                  forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets forall a b. (a -> b) -> a -> b
$ \RW
s -> (RW -> Goals
iCts RW
s, RW
s { iCts :: Goals
iCts = Goals
emptyGoals }))
     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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Goal] -> InferM [Goal]
simpGoals [Goal]
gs0
  where
  doAdd :: [Goal] -> InferM ()
doAdd [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  doAdd [Goal]
gs = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iCts :: Goals
iCts = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (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 <- forall t. TVars t => t -> InferM t
applySubst 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
     forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, [Goal]
newGs)

  where

  -- retrieve the type map only
  getGoals' :: InferM Goals
getGoals'    = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets 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
iSupply :: Supply
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iHasCts :: [[HasGoal]]
iCts :: Goals
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Type]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
iBindTypes :: RW -> Map Name Schema
iScope :: RW -> [ModuleG ScopeName]
iSolvedHas :: RW -> Map Int HasGoalSln
iHasCts :: RW -> [[HasGoal]]
iExistTVars :: RW -> [Map Name Type]
iSupply :: RW -> Supply
iNameSeeds :: RW -> NameSeeds
iCts :: RW -> Goals
iErrors :: RW -> [(Range, Error)]
iWarnings :: RW -> [(Range, Warning)]
iSubst :: RW -> Subst
.. } -> (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
iSupply :: Supply
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iHasCts :: [[HasGoal]]
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Type]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iSolvedHas :: Map Int HasGoalSln
iHasCts :: [[HasGoal]]
iExistTVars :: [Map Name Type]
iSupply :: Supply
iNameSeeds :: NameSeeds
iErrors :: [(Range, Error)]
iWarnings :: [(Range, Warning)]
iSubst :: Subst
.. })

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

simpGoal :: Goal -> InferM [Goal]
simpGoal :: Goal -> InferM [Goal]
simpGoal Goal
g =
  case Ctxt -> Type -> Type
Simple.simplify 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 forall a b. (a -> b) -> a -> b
$ [Goal] -> Error
UnsolvableGoals [Goal
g { goal :: Type
goal = Type
t }]
           forall (m :: * -> *) a. Monad m => a -> m a
return []
      | [Type]
ps <- Type -> [Type]
pSplitAnd Type
p -> 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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Goal -> InferM [Goal]
simpGoal [Goal]
gs



{- | Record a constraint that when we select from the first type,
we should get a value of the second type.
The returned function should be used to wrap the expression from
which we are selecting (i.e., the record or tuple).  Plese note
that the resulting expression should not be forced before the
constraint is solved.
-}
newHasGoal :: P.Selector -> Type -> Type -> InferM HasGoalSln
newHasGoal :: Selector -> 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)
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 forall a. a -> [a] -> [a]
: [HasGoal]
cs) forall a. a -> [a] -> [a]
: [[HasGoal]]
more }
                        [] -> forall a. HasCallStack => String -> [String] -> a
panic String
"newHasGoal" [String
"no selector scope"]
     Map Int HasGoalSln
solns    <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RO -> Map Int HasGoalSln
iSolvedHasLazy forall (m :: * -> *) i. ReaderM m i => m i
ask
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case 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 -> 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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 forall a. a -> [a] -> [a]
: [HasGoal]
cs) forall a. a -> [a] -> [a]
: [[HasGoal]]
more }
                                  [] -> 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 <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 = [] forall a. a -> [a] -> [a]
: [[HasGoal]]
more })
                             [] -> forall a. HasCallStack => String -> [String] -> a
panic String
"getHasGoals" [String
"No selector scope"]
     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 =
  forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iSolvedHas :: Map Int HasGoalSln
iSolvedHas = 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
     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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets 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 = forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName 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 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 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 = 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 }
     forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName 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 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  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Kind
KType -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Kind
KProp -> 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  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Kind
KType -> 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 (forall n. TParam n -> n
P.tpName TParam Name
nm)
                         , tvarSource :: Range
tvarSource = forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange (forall n. TParam n -> Maybe Range
P.tpRange TParam Name
nm)
                         }
     TParam
tp <- forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName 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 forall a. Num a => a -> a -> a
+ Int
1 })

     TParam -> TPFlavor -> Kind -> InferM ()
checkParamKind TParam
tp TPFlavor
flav Kind
k
     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 = 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 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 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' <- forall t. TVars t => t -> InferM t
applySubst Type
t1
     Type
t2' <- forall t. TVars t => t -> InferM t
applySubst Type
t2
     let ((Subst
su1, [Type]
ps), [(Path, UnificationError)]
errs) = 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 (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
       [] -> forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ps
       [(Path, UnificationError)]
_  -> do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Path, UnificationError) -> Error
toError) [(Path, UnificationError)]
errs
                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
     forall (m :: * -> *) a. Monad m => a -> m a
return (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 <- forall t. TVars t => t -> InferM t
applySubst [Type]
ps
     forall (m :: * -> *) a. Monad m => a -> m a
return (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 <- forall t. TVars t => t -> InferM t
applySubst [Goal]
gs
     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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RW -> Subst
iSubst 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 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)
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ 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
_ ->
          forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.Monad.extendSubst"
            [ String
"Substitution instantiates bound variable:"
            , String
"Variable: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp TVar
v)
            , String
"Type:     " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp Type
ty)
            ]
        TVFree Int
_ Kind
_ Set TParam
tvs TVarInfo
_ ->
          do let escaped :: Set TParam
escaped = forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall t. FVS t => t -> Set TParam
freeParams Type
ty) Set TParam
tvs
             if forall a. Set a -> Bool
Set.null Set TParam
escaped then forall (m :: * -> *) a. Monad m => a -> m a
return () else
               forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.Monad.extendSubst"
                 [ String
"Escaped quantified variables:"
                 , String
"Substitution:  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp TVar
v Doc -> Doc -> Doc
<+> String -> Doc
text String
":=" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Type
ty)
                 , String
"Vars in scope: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Doc -> Doc
brackets ([Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (forall a. Set a -> [a]
Set.toList Set TParam
tvs))))
                 , String
"Escaped:       " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Doc -> Doc
brackets ([Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (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     <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k a. Map k a -> [a]
Map.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. RO -> Map Name VarType
iVars) forall (m :: * -> *) i. ReaderM m i => m i
ask
     [Set TVar]
fromEnv <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VarType]
env forall a b. (a -> b) -> a -> b
$ \VarType
v ->
                  case VarType
v of
                    ExtVar Schema
sch  -> forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars Schema
sch
                    CurSCC Expr
_ Type
t  -> forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars Type
t
     [[HasGoal]]
hasCts <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (RW -> [[HasGoal]]
iHasCts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) i. StateM m i => m i
get)
     let sels :: [Type]
sels = forall a b. (a -> b) -> [a] -> [b]
map (Goal -> Type
goal forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasGoal -> Goal
hasGoal) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[HasGoal]]
hasCts)
     [Set TVar]
fromSels <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars [Type]
sels
     Set TVar
fromEx   <- (forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall k a. Map k a -> [a]
Map.elems) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RW -> [Map Name Type]
iExistTVars forall (m :: * -> *) i. StateM m i => m i
get)
     forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set TVar]
fromEnv forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set TVar]
fromSels
                                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TVar
fromEx)
  where
  getVars :: a -> InferM (Set TVar)
getVars a
x = forall t. FVS t => t -> Set TVar
fvs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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 <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. RO -> Map Name VarType
iVars
     case Maybe VarType
mb of
       Just VarType
a  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure VarType
a
       Maybe VarType
Nothing ->
         do Maybe Schema
mb1 <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> Map Name Schema
iBindTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
            case Maybe Schema
mb1 of
              Just Schema
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Schema -> VarType
ExtVar Schema
a)
              Maybe Schema
Nothing ->
                do Map Name VarType
mp <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Map Name VarType
iVars
                   forall a. HasCallStack => String -> [String] -> a
panic String
"lookupVar" forall a b. (a -> b) -> a -> b
$ [ String
"Undefined vairable"
                                     , forall a. Show a => a -> String
show Name
x
                                     , String
"IVARS"
                                     ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
debugShowUniques forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> Doc
pp) (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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find TParam -> Bool
this 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 forall a. Eq a => a -> a -> Bool
== 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x 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 forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Map Name ModParamNames
sigs of
           Just ModParamNames
ips -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModParamNames
ips
           Maybe ModParamNames
Nothing  -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupSignature"
                        [ String
"Missing signature", forall a. Show a => a -> String
show Name
x ]

    P.ImpTop ModName
t ->
      do ModName -> Maybe ModParamNames
loaded <- RO -> ModName -> Maybe ModParamNames
iExtSignatures forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
         case ModName -> Maybe ModParamNames
loaded ModName
t of
           Just ModParamNames
ps -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModParamNames
ps
           Maybe ModParamNames
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupSignature"
                        [ String
"Top level signature is not loaded", forall a. Show a => a -> String
show (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
     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 -> forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Maybe a -> a
fromMb 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 <- forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors
         case 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 -> 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)
                forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {a}. Maybe a -> a
fromMb do ModuleG ()
a <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ModuleG (), IfaceG ())
mbTop
                                ModuleG Name
b <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
m (forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ()
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 -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupFunctor"
                                  [ String
"Missing functor", 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 -> forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Maybe a -> a
fromMb 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 <- forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules
         case 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 <- forall name ignored.
IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames IfaceNames Name
names forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (ModuleG ())
getCurDecls
                 forall (f :: * -> *) a. Applicative f => a -> f a
pure (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)
                forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {a}. Maybe a -> a
fromMb
                         do IfaceG ()
iface <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ModuleG (), IfaceG ())
mb
                            IfaceNames Name
names <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
m
                                        (IfaceDecls -> Map Name (IfaceNames Name)
If.ifModules (forall name. IfaceG name -> IfaceDecls
If.ifDefines IfaceG ()
iface))
                            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 -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupModule"
                                  [ String
"Missing module", 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 <- forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> FunctorParams
mParams
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
     case forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x) [Map Name Type]
scopes) of
       Just Type
ty -> 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
                forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s{ iExistTVars :: [Map Name Type]
iExistTVars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type
ty Map Name Type
sc forall a. a -> [a] -> [a]
: [Map Name Type]
more }
                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 = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope 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 = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope 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 = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes

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

-- | Constraints on the module's parameters.
getParamConstraints :: InferM [Located Prop]
getParamConstraints :: InferM [Located Type]
getParamConstraints = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope 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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName 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 <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
     Set TParam
params <- forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
     let bound :: Set TParam
bound  = forall a. Ord a => [a] -> Set a
Set.fromList (RO -> [TParam]
iTVars RO
ro)
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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  = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Bool
iMonoBinds)

getCallStacks :: InferM Bool
getCallStacks :: InferM Bool
getCallStacks = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (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 = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope 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 <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
     RW
rw <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
     let shadowed :: Maybe String
shadowed =
           do TySyn
_ <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
new Map Name TySyn
tsyns
              forall (m :: * -> *) a. Monad m => a -> m a
return String
"type synonym"
           forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
           do forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Name
new forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName (RO -> [TParam]
iTVars RO
ro))
              forall (m :: * -> *) a. Monad m => a -> m a
return String
"type variable"
           forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
           do Type
_ <- forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
new) (RW -> [Map Name Type]
iExistTVars RW
rw))
              forall (m :: * -> *) a. Monad m => a -> m a
return String
"type"

     case Maybe String
shadowed of
       Maybe String
Nothing -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
mapReader (\RO
r -> RO
r { iTVars :: [TParam]
iTVars = TParam
p 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr 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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = forall mname. mname -> ModuleG mname
emptyModule ScopeName
nm 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 = forall a. Ord a => a -> Set a -> Set a
Set.insert Name
x (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 = forall a. Ord a => a -> Set a -> Set a
Set.insert Name
x (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 = 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 = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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
      []       -> 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 forall a. a -> [a] -> [a]
: [ModuleG ScopeName]
more

endLocalScope :: InferM ([DeclGroup], Map Name TySyn)
endLocalScope :: InferM ([DeclGroup], Map Name TySyn)
endLocalScope =
  forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 <- forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
x ->
                    ( (forall a. [a] -> [a]
reverse (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
x), forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x), RW
rw { iScope :: [ModuleG ScopeName]
iScope = [ModuleG ScopeName]
xs })

         [ModuleG ScopeName]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"endLocalScope" [String
"Missing local scope"]

endSubmodule :: InferM ()
endSubmodule :: InferM ()
endSubmodule =
  forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 forall a. a -> [a] -> [a]
: [ModuleG ScopeName]
more }
           where
           x1 :: ModuleG Name
x1    = ModuleG ScopeName
x { mName :: Name
mName = Name
m, mDecls :: [DeclGroup]
mDecls = forall a. [a] -> [a]
reverse (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
x) }

           isFun :: Bool
isFun = 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 forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> a
f ModuleG ScopeName
y

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

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

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


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

endSignature :: InferM ()
endSignature :: InferM ()
endSignature =
  forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 forall a. a -> [a] -> [a]
: [ModuleG ScopeName]
more }
        where
        z :: ModuleG ScopeName
z   = ModuleG ScopeName
y { mSignatures :: Map Name ModParamNames
mSignatures = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
m ModParamNames
sig (forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG ScopeName
y) }
        sig :: ModParamNames
sig = ModParamNames
                { mpnTypes :: Map Name ModTParam
mpnTypes       = forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG ScopeName
x
                , mpnConstraints :: [Located Type]
mpnConstraints = forall mname. ModuleG mname -> [Located Type]
mParamConstraints ModuleG ScopeName
x
                , mpnFuns :: Map Name ModVParam
mpnFuns        = forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG ScopeName
x
                , mpnTySyn :: Map Name TySyn
mpnTySyn       = forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x
                , mpnDoc :: Maybe Text
mpnDoc         = Maybe Text
doc
                }
      [ModuleG ScopeName]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"endSignature" [ String
"Not a signature scope" ]

endTopSignature :: InferM TCTopEntity
endTopSignature :: InferM TCTopEntity
endTopSignature =
  forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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 <- forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
x ->
        ( ModName -> ModParamNames -> TCTopEntity
TCTopSignature ModName
m ModParamNames
                             { mpnTypes :: Map Name ModTParam
mpnTypes       = forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG ScopeName
x
                             , mpnConstraints :: [Located Type]
mpnConstraints = forall mname. ModuleG mname -> [Located Type]
mParamConstraints ModuleG ScopeName
x
                             , mpnFuns :: Map Name ModVParam
mpnFuns        = forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG ScopeName
x
                             , mpnTySyn :: Map Name TySyn
mpnTySyn       = forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x
                             , mpnDoc :: Maybe Text
mpnDoc         = forall a. Maybe a
Nothing
                             }
        , RW
rw { iScope :: [ModuleG ScopeName]
iScope = [] }
        )
      [ModuleG ScopeName]
_ -> 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 <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
     RW
rw <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Semigroup a => NonEmpty a -> a
sconcat (ModuleG ScopeName -> a
f (RO -> ModuleG ScopeName
iExtScope RO
ro) forall a. a -> [a] -> NonEmpty 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 <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
     RW
rw <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ModuleG ScopeName
m1 ModuleG ()
m2 -> forall {mname}. ModuleG mname -> ModuleG mname -> ModuleG ()
mergeDecls (forall {mname}. ModuleG mname -> ModuleG ()
forget ModuleG ScopeName
m1) ModuleG ()
m2)
                (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              = forall a. Maybe a
Nothing
      , mExports :: ExportSpec Name
mExports          = forall a. Monoid a => a
mempty
      , mParams :: FunctorParams
mParams           = forall a. Monoid a => a
mempty
      , mParamTypes :: Map Name ModTParam
mParamTypes       = forall a. Monoid a => a
mempty
      , mParamConstraints :: [Located Type]
mParamConstraints = forall a. Monoid a => a
mempty
      , mParamFuns :: Map Name ModVParam
mParamFuns        = forall a. Monoid a => a
mempty
      , mNested :: Set Name
mNested           = forall a. Monoid a => a
mempty

      , mTySyns :: Map Name TySyn
mTySyns           = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name TySyn
mTySyns
      , mNewtypes :: Map Name Newtype
mNewtypes         = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name Newtype
mNewtypes
      , mPrimTypes :: Map Name AbstractType
mPrimTypes        = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes
      , mDecls :: [DeclGroup]
mDecls            = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> [DeclGroup]
mDecls
      , mSubmodules :: Map Name (IfaceNames Name)
mSubmodules       = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules
      , mFunctors :: Map Name (ModuleG Name)
mFunctors         = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors
      , mSignatures :: Map Name ModParamNames
mSignatures       = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni 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 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 forall a. a -> [a] -> [a]
: forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
r }
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ 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   = 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  = 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 = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x TySyn
t (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 = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Newtype -> Name
ntName Newtype
t) Newtype
t (forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG ScopeName
r) }
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes :: Map Name Schema
iBindTypes = 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 = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (AbstractType -> Name
atName AbstractType
t) AbstractType
t (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 = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModTParam -> Name
mtpName ModTParam
a) ModTParam
a (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 = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name ModParamNames
mp (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 = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name (IfaceNames Name)
mp (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 = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name (ModuleG Name)
mp (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 = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModVParam -> Name
mvpName ModVParam
x) ModVParam
x (forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG ScopeName
r) }
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes :: Map Name Schema
iBindTypes = 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 forall a. [a] -> [a] -> [a]
++ 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 = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModParam -> Ident
mpName ModParam
p) ModParam
p (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iExistTVars :: [Map Name Type]
iExistTVars = forall k a. Map k a
Map.empty forall a. a -> [a] -> [a]
: [Map Name Type]
curScopes }
     a
a <- InferM a
m
     forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iExistTVars :: [Map Name Type]
iExistTVars = [Map Name Type]
curScopes }
     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) =
  forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
mapReader (\RO
r -> RO
r { iVars :: Map Name VarType
iVars = 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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 = 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) = forall a. Name -> Schema -> InferM a -> InferM a
withVar Name
x ([TParam] -> [Type] -> Type -> Schema
Forall [] [] (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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Name, Located Type) -> InferM a -> InferM a
withMonoType InferM a
m (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) = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (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 = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
  <*> :: forall a 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        = 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    = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (ReaderT KRO (StateT KRW InferM) a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. KindM a -> ReaderT KRO (StateT KRW InferM) a
unKM 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        = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (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) <- forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT KRW
krw (forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT KRO
kro ReaderT KRO (StateT KRW InferM) a
m)
     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  = 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 = 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 = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$
  do Map Name TParam
vs <- KRO -> Map Name TParam
lazyTParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall (m :: * -> *) i. ReaderM m i => m i
ask
     KRW
ss <- forall (m :: * -> *) i. StateM m i => m i
get
     case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Map Name TParam
vs of
       Just TParam
t  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ TParam -> Maybe Kind -> LkpTyVar
TLocalVar TParam
t forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall a b. (a -> b) -> a -> b
$ KRW -> Map Name Kind
typeParams KRW
ss
       Maybe TParam
Nothing -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do Maybe TParam
t <- Name -> InferM (Maybe TParam)
lookupTParam Name
x
                                   forall (m :: * -> *) a. Monad m => a -> m a
return (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 = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap KRO -> AllowWildCards
allowWild forall (m :: * -> *) i. ReaderM m i => m i
ask

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

kRecordWarning :: Warning -> KindM ()
kRecordWarning :: Warning -> KindM ()
kRecordWarning Warning
w = forall a. InferM a -> KindM a
kInInferM 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 = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ do Map Name TParam
vs <- forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks KRO -> Map Name TParam
lazyTParams
                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map Name TParam
vs)
     forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ TVar -> Type
TVar 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 = forall a. InferM a -> KindM a
kInInferM 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 = forall a. InferM a -> KindM a
kInInferM 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 = 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 = forall a. InferM a -> KindM a
kInInferM 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 = forall a. InferM a -> KindM a
kInInferM 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (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 = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \KRW
s -> KRW
s{ typeParams :: Map Name Kind
typeParams = 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) = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$
  do KRO
e <- forall (m :: * -> *) i. ReaderM m i => m i
ask
     KRW
s <- forall (m :: * -> *) i. StateM m i => m i
get
     (a
a,KRW
s1) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Range -> InferM a -> InferM a
inRange Range
r forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT KRW
s forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT KRO
e ReaderT KRO (StateT KRW InferM) a
m
     forall (m :: * -> *) i. StateM m i => i -> m ()
set KRW
s1
     forall (m :: * -> *) a. Monad m => a -> m a
return a
a

kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
kNewGoals :: ConstraintSource -> [Type] -> KindM ()
kNewGoals ConstraintSource
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
kNewGoals ConstraintSource
c [Type]
ps = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \KRW
s -> KRW
s { kCtrs :: [(ConstraintSource, [Type])]
kCtrs = (ConstraintSource
c,[Type]
ps) 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 = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift InferM a
m