-- |
-- 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           Cryptol.ModuleSystem.NamingEnv.Types
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, cleanupWarnings
                                        )
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 NominalType
inpNominalTypes :: Map Name NominalType -- ^ Nominal types in scope
  , InferInput -> Map Name ModParamNames
inpSignatures :: !(Map Name ModParamNames)  -- ^ Signatures in scope

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

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

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

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

  , InferInput -> [String]
inpSearchPath :: [FilePath]
    -- ^ Where to look for Cryptol theory file.

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

  , InferInput -> Supply
inpSupply :: !Supply              -- ^ The supply for fresh name generation

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

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

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


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

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


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

bumpCounter :: InferM ()
bumpCounter :: InferM ()
bumpCounter = do RO { Bool
[TParam]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iRange :: Range
iVars :: Map Name VarType
iTVars :: [TParam]
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iExtSignatures :: ModName -> Maybe ModParamNames
iExtScope :: ModuleG ScopeName
iSolvedHasLazy :: Map Int HasGoalSln
iMonoBinds :: Bool
iCallStacks :: Bool
iSolver :: Solver
iPrimNames :: PrimMap
iSolveCounter :: IORef Int
iRange :: RO -> Range
iVars :: RO -> Map Name VarType
iTVars :: RO -> [TParam]
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtScope :: RO -> ModuleG ScopeName
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iMonoBinds :: RO -> Bool
iCallStacks :: RO -> Bool
iSolver :: RO -> Solver
iPrimNames :: RO -> PrimMap
iSolveCounter :: RO -> IORef Int
.. } <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
-> InferM RO
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
                 IO () -> InferM ()
forall a. IO a -> InferM a
io (IO () -> InferM ()) -> IO () -> InferM ()
forall a b. (a -> b) -> a -> b
$ IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
iSolveCounter (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

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

     let env :: Map Name VarType
env = (Schema -> VarType) -> Map Name Schema -> Map Name VarType
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Schema -> VarType
ExtVar (InferInput -> Map Name Schema
inpVars InferInput
info)
            Map Name VarType -> Map Name VarType -> Map Name VarType
forall a. Semigroup a => a -> a -> a
<> [(Name, VarType)] -> Map Name VarType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
              [ (Name
c, Schema -> VarType
ExtVar Schema
t)
              | NominalType
nt <- Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems (InferInput -> Map Name NominalType
inpNominalTypes InferInput
info)
              , (Name
c,Schema
t) <- NominalType -> [(Name, Schema)]
nominalTypeConTypes NominalType
nt
              ]
            Map Name VarType -> Map Name VarType -> Map Name VarType
forall a. Semigroup a => a -> a -> a
<> (ModVParam -> VarType) -> Map Name ModVParam -> Map Name VarType
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Schema -> VarType
ExtVar (Schema -> VarType)
-> (ModVParam -> Schema) -> ModVParam -> VarType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModVParam -> Schema
mvpType) (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
allPs)

     let ro :: RO
ro =         RO { iRange :: Range
iRange     = InferInput -> Range
inpRange InferInput
info
                         , iVars :: Map Name VarType
iVars      = Map Name VarType
env
                         , iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iExtModules = InferInput -> ModName -> Maybe (ModuleG (), IfaceG ())
inpTopModules InferInput
info
                         , iExtSignatures :: ModName -> Maybe ModParamNames
iExtSignatures = InferInput -> ModName -> Maybe ModParamNames
inpTopSignatures InferInput
info
                         , iExtScope :: ModuleG ScopeName
iExtScope = (ScopeName -> ModuleG ScopeName
forall mname. mname -> ModuleG mname
emptyModule ScopeName
ExternalScope)
                             { mTySyns           = inpTSyns info <>
                                                   mpnTySyn allPs
                             , mNominalTypes     = inpNominalTypes info
                             , mParamTypes       = mpnTypes allPs
                             , mParamFuns        = mpnFuns  allPs
                             , mParamConstraints = mpnConstraints allPs
                             , mSignatures       = inpSignatures info
                             }

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

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

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

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

  where
  inferOk :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> f (InferOutput a)
inferOk [(Range, Warning)]
ws NameSeeds
a Supply
b a
c  = 
    let ws1 :: [(Range, Warning)]
ws1 = [(Range, Warning)] -> [(Range, Warning)]
cleanupWarnings [(Range, Warning)]
ws
    in InferOutput a -> f (InferOutput a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NameMap
-> [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
forall a.
NameMap
-> [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
InferOK ([(Range, Warning)] -> [(Range, Error)] -> NameMap
computeFreeVarNames [(Range, Warning)]
ws1 []) [(Range, Warning)]
ws1 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
        ws1 :: [(Range, Warning)]
ws1 = [(Range, Warning)] -> [(Range, Warning)]
cleanupWarnings [(Range, Warning)]
ws
    in InferOutput a -> f (InferOutput a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NameMap -> [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
forall a.
NameMap -> [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
InferFailed ([(Range, Warning)] -> [(Range, Error)] -> NameMap
computeFreeVarNames [(Range, Warning)]
ws1 [(Range, Error)]
es1) [(Range, Warning)]
ws1 [(Range, Error)]
es1)


  rw :: RW
rw = RW { iErrors :: [(Range, Error)]
iErrors     = []
          , iWarnings :: [(Range, Warning)]
iWarnings   = []
          , iSubst :: Subst
iSubst      = Subst
emptySubst
          , iExistTVars :: [Map Name Type]
iExistTVars = []

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

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

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

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

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

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



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


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

-- | Read-only component of the monad.
data RO = RO
  { RO -> Range
iRange    :: Range       -- ^ Source code being analysed
  , RO -> Map Name VarType
iVars     :: Map Name VarType
    -- ^ Type of variable that are in scope
    -- These are only parameters vars that are in recursive component we
    -- are checking at the moment.  If a var is not there, keep looking in
    -- the 'iScope'


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

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

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

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

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

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

  , RO -> Bool
iCallStacks :: Bool
    -- ^ When this flag is true, retain source location information
    --   in typechecked terms

  , RO -> Solver
iSolver :: SMT.Solver

  , RO -> PrimMap
iPrimNames :: !PrimMap

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

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

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

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

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

  -- Constraints that need solving
  , RW -> Goals
iCts      :: !Goals                -- ^ Ordinary constraints
  , RW -> [[HasGoal]]
iHasCts   :: ![[HasGoal]]
    {- ^ Tuple/record projection constraints.  These are separate from
       the other constraints because solving them results in actual elaboration
       of the term, indicating how to do the projection.  The modification
       of the term is done using lazyness, by looking up a thunk ahead of time
       (@iSolvedHasLazy@ in RO), which is filled in when the constrait is
       solved (@iSolvedHas@).  See also `selectorScope`.
    -}

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

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

  , RW -> Supply
iSupply :: !Supply
  }


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

instance A.Applicative InferM where
  pure :: forall a. a -> InferM a
pure a
x = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
forall a.
a -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
  <*> :: forall a b. InferM (a -> b) -> InferM a -> InferM b
(<*>) = InferM (a -> b) -> InferM a -> InferM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

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

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

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

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


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


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

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

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

-- | Report an error.
recordError :: Error -> InferM ()
recordError :: Error -> InferM ()
recordError = Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
forall a. Maybe a
Nothing

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


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

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

-- | Retrieve the mapping between identifiers and declarations in the prelude.
getPrimMap :: InferM PrimMap
getPrimMap :: InferM PrimMap
getPrimMap  =
  do RO { Bool
[TParam]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iRange :: RO -> Range
iVars :: RO -> Map Name VarType
iTVars :: RO -> [TParam]
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtScope :: RO -> ModuleG ScopeName
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iMonoBinds :: RO -> Bool
iCallStacks :: RO -> Bool
iSolver :: RO -> Solver
iPrimNames :: RO -> PrimMap
iSolveCounter :: RO -> IORef Int
iRange :: Range
iVars :: Map Name VarType
iTVars :: [TParam]
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iExtSignatures :: ModName -> Maybe ModParamNames
iExtScope :: ModuleG ScopeName
iSolvedHasLazy :: Map Int HasGoalSln
iMonoBinds :: Bool
iCallStacks :: Bool
iSolver :: Solver
iPrimNames :: PrimMap
iSolveCounter :: IORef Int
.. } <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
-> InferM RO
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     PrimMap -> InferM PrimMap
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return PrimMap
iPrimNames


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

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

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

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


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

  where

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

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

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

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



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


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

-- | Get the @Has@ constraints.  Each of this should either be solved,
-- or added back using 'addHasGoal'.
getHasGoals :: InferM [HasGoal]
getHasGoals :: InferM [HasGoal]
getHasGoals =
  do [HasGoal]
gs <- ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) [HasGoal]
-> InferM [HasGoal]
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) [HasGoal]
 -> InferM [HasGoal])
-> ReaderT
     RO (StateT RW (ExceptionT [(Range, Error)] IO)) [HasGoal]
-> InferM [HasGoal]
forall a b. (a -> b) -> a -> b
$ (RW -> ([HasGoal], RW))
-> ReaderT
     RO (StateT RW (ExceptionT [(Range, Error)] IO)) [HasGoal]
forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets \RW
s -> case RW -> [[HasGoal]]
iHasCts RW
s of
                             [HasGoal]
cs : [[HasGoal]]
more -> ([HasGoal]
cs, RW
s { iHasCts = [] : more })
                             [] -> String -> [String] -> ([HasGoal], RW)
forall a. HasCallStack => String -> [String] -> a
panic String
"getHasGoals" [String
"No selector scope"]
     [HasGoal] -> InferM [HasGoal]
forall t. TVars t => t -> InferM t
applySubst [HasGoal]
gs

-- | Specify the solution (@Expr -> Expr@) for the given constraint ('Int').
solveHasGoal :: Int -> HasGoalSln -> InferM ()
solveHasGoal :: Int -> HasGoalSln -> InferM ()
solveHasGoal Int
n HasGoalSln
e =
  ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
 -> InferM ())
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW)
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ ((RW -> RW)
 -> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ())
-> (RW -> RW)
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iSolvedHas = Map.insert n e (iSolvedHas s) }


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

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

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


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

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

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

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

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

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

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

-- | Generate a new version of a type parameter.  We use this when
-- instantiating module parameters (the "backtick" imports)
freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam
freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam
freshTParam Name -> TPFlavor
mkF TParam
tp = (NameSeeds -> (TParam, NameSeeds)) -> InferM TParam
forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName \NameSeeds
s ->
  let u :: Int
u = NameSeeds -> Int
seedTVar NameSeeds
s
  in ( TParam
tp { tpUnique = u
          , tpFlav   = case tpName 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 = u + 1 }
     )


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



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


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

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

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


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

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

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


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

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


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

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

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

-- | Lookup the definition of a nominal type
lookupNominal :: Name -> InferM (Maybe NominalType)
lookupNominal :: Name -> InferM (Maybe NominalType)
lookupNominal Name
x = Name -> Map Name NominalType -> Maybe NominalType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Map Name NominalType -> Maybe NominalType)
-> InferM (Map Name NominalType) -> InferM (Maybe NominalType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name NominalType)
getNominalTypes

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

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

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

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

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


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

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

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



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


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

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

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


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

-- | Returns the nominal type declarations that are in scope.
getNominalTypes :: InferM (Map Name NominalType)
getNominalTypes :: InferM (Map Name NominalType)
getNominalTypes = (ModuleG ScopeName -> Map Name NominalType)
-> InferM (Map Name NominalType)
forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope ModuleG ScopeName -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes

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

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

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

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

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

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

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



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

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

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


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

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


-- | Execute the given computation in a new top scope.
-- The sub-computation would typically be validating a module.
newScope :: ScopeName -> InferM ()
newScope :: ScopeName -> InferM ()
newScope ScopeName
nm = ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
 -> InferM ())
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW)
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iScope = emptyModule nm : iScope 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.insert x (mNested 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 -> [Text] -> ExportSpec Name -> NamingEnv -> InferM ()
newSubmoduleScope :: Name -> [Text] -> ExportSpec Name -> NamingEnv -> InferM ()
newSubmoduleScope Name
x [Text]
docs ExportSpec Name
e NamingEnv
inScope =
  do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
o -> ModuleG ScopeName
o { mNested = Set.insert x (mNested o) }
     ScopeName -> InferM ()
newScope (Name -> ScopeName
SubModule Name
x)
     (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
m -> ModuleG ScopeName
m { mDoc = docs, mExports = e, mInScope = inScope }

newModuleScope :: [Text] -> P.ModName -> ExportSpec Name -> NamingEnv -> InferM ()
newModuleScope :: [Text] -> ModName -> ExportSpec Name -> NamingEnv -> InferM ()
newModuleScope [Text]
docs ModName
x ExportSpec Name
e NamingEnv
inScope =
  do ScopeName -> InferM ()
newScope (ModName -> ScopeName
MTopModule ModName
x)
     (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
m -> ModuleG ScopeName
m { mDoc = docs, mExports = e, mInScope = inScope }

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

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

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

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

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

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

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

                 , mTySyns :: Map Name TySyn
mTySyns      = (ModuleG ScopeName -> Map Name TySyn) -> Map Name TySyn
forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add ModuleG ScopeName -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns
                 , mNominalTypes :: Map Name NominalType
mNominalTypes = (ModuleG ScopeName -> Map Name NominalType) -> Map Name NominalType
forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add ModuleG ScopeName -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes
                 , mDecls :: [DeclGroup]
mDecls       = (ModuleG ScopeName -> [DeclGroup]) -> [DeclGroup]
forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add ModuleG ScopeName -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls
                 , mSignatures :: Map Name ModParamNames
mSignatures  = (ModuleG ScopeName -> Map Name ModParamNames)
-> Map Name ModParamNames
forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add ModuleG ScopeName -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures
                 , mSubmodules :: Map Name Submodule
mSubmodules  = if Bool
isFun
                                    then ModuleG ScopeName -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG ScopeName
y
                                    else let sm :: Submodule
sm = Submodule
                                                    { smIface :: IfaceNames Name
smIface = ModuleG Name -> IfaceNames Name
forall name. ModuleG name -> IfaceNames name
genIfaceNames ModuleG Name
x1
                                                    , smInScope :: NamingEnv
smInScope = ModuleG ScopeName -> NamingEnv
forall mname. ModuleG mname -> NamingEnv
mInScope ModuleG ScopeName
x }
                                         in Name -> Submodule -> Map Name Submodule -> Map Name Submodule
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
m Submodule
sm
                                               (ModuleG ScopeName -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG ScopeName
x Map Name Submodule -> Map Name Submodule -> Map Name Submodule
forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG ScopeName
y)
                 , mFunctors :: Map Name (ModuleG Name)
mFunctors    = if Bool
isFun
                                    then Name
-> ModuleG Name
-> Map Name (ModuleG Name)
-> Map Name (ModuleG Name)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
m ModuleG Name
x1 (ModuleG ScopeName -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ScopeName
y)
                                    else ModuleG ScopeName -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ScopeName
x Map Name (ModuleG Name)
-> Map Name (ModuleG Name) -> Map Name (ModuleG Name)
forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ScopeName
y
                 }

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


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

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

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



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

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

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

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

      , mTySyns :: Map Name TySyn
mTySyns           = (ModuleG mname -> Map Name TySyn) -> Map Name TySyn
forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni ModuleG mname -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns
      , mNominalTypes :: Map Name NominalType
mNominalTypes     = (ModuleG mname -> Map Name NominalType) -> Map Name NominalType
forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni ModuleG mname -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes
      , mDecls :: [DeclGroup]
mDecls            = (ModuleG mname -> [DeclGroup]) -> [DeclGroup]
forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni ModuleG mname -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls
      , mSubmodules :: Map Name Submodule
mSubmodules       = (ModuleG mname -> Map Name Submodule) -> Map Name Submodule
forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni ModuleG mname -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules
      , mFunctors :: Map Name (ModuleG Name)
mFunctors         = (ModuleG mname -> Map Name (ModuleG Name))
-> Map Name (ModuleG Name)
forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni ModuleG mname -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors
      , mSignatures :: Map Name ModParamNames
mSignatures       = (ModuleG mname -> Map Name ModParamNames) -> Map Name ModParamNames
forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni ModuleG mname -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures

      , mInScope :: NamingEnv
mInScope          = (ModuleG mname -> NamingEnv) -> NamingEnv
forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni ModuleG mname -> NamingEnv
forall mname. ModuleG mname -> NamingEnv
mInScope
      }
    where
    uni :: (ModuleG mname -> a) -> a
uni ModuleG mname -> a
f = ModuleG mname -> a
f ModuleG mname
m1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> ModuleG mname -> a
f ModuleG mname
m2


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

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

addNominal :: NominalType -> InferM ()
addNominal :: NominalType -> InferM ()
addNominal NominalType
t =
  do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mNominalTypes = Map.insert (ntName t) t (mNominalTypes r) }
     let cons :: [(Name, Schema)]
cons = NominalType -> [(Name, Schema)]
nominalTypeConTypes NominalType
t
         ins :: (Name, b) -> Map Name b -> Map Name b
ins  = (Name -> b -> Map Name b -> Map Name b)
-> (Name, b) -> Map Name b -> Map Name b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> b -> Map Name b -> Map Name b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
     ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
 -> InferM ())
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW)
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes = foldr ins (iBindTypes rw) cons }

addParamType :: ModTParam -> InferM ()
addParamType :: ModTParam -> InferM ()
addParamType ModTParam
a =
  (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mParamTypes = Map.insert (mtpName a) a (mParamTypes 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.union mp (mSignatures r) }

addSubmodules :: Map Name Submodule -> InferM ()
addSubmodules :: Map Name Submodule -> InferM ()
addSubmodules Map Name Submodule
mp =
  (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mSubmodules = Map.union mp (mSubmodules 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.union mp (mFunctors r) }

setNested :: Set Name -> InferM ()
setNested :: Set Name -> InferM ()
setNested Set Name
names =
  (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mNested = names }


-- | 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.insert (mvpName x) x (mParamFuns r) }
     ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
 -> InferM ())
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
-> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW)
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes = Map.insert (mvpName x) (mvpType x)
                                                    (iBindTypes 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 = ps ++ mParamConstraints r }

addModParam :: ModParam -> InferM ()
addModParam :: ModParam -> InferM ()
addModParam ModParam
p =
  (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mParams = Map.insert (mpName p) p (mParams r) }




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


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

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

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

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

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

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


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

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

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

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

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

instance A.Applicative KindM where
  pure :: forall a. a -> KindM a
pure a
x = ReaderT KRO (StateT KRW InferM) a -> KindM a
forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (a -> ReaderT KRO (StateT KRW InferM) a
forall a. a -> ReaderT KRO (StateT KRW InferM) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
  <*> :: forall a b. KindM (a -> b) -> KindM a -> KindM b
(<*>) = KindM (a -> b) -> KindM a -> KindM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

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

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


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

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

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

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

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

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

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

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

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

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

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

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

-- | Lookup the definition of a nominal type.
kLookupNominal :: Name -> KindM (Maybe NominalType)
kLookupNominal :: Name -> KindM (Maybe NominalType)
kLookupNominal = InferM (Maybe NominalType) -> KindM (Maybe NominalType)
forall a. InferM a -> KindM a
kInInferM (InferM (Maybe NominalType) -> KindM (Maybe NominalType))
-> (Name -> InferM (Maybe NominalType))
-> Name
-> KindM (Maybe NominalType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> InferM (Maybe NominalType)
lookupNominal

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

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

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

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

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

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

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