-- |
-- Module      :  Cryptol.TypeCheck.Monad
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# LANGUAGE Safe #-}
{-# 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 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,mkParameter
                    , nameInfo, NameInfo(..),NameSource(..))
import           Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.Subst
import           Cryptol.TypeCheck.Interface(genIface)
import           Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
import           Cryptol.TypeCheck.InferTypes
import           Cryptol.TypeCheck.Error( Warning(..),Error(..)
                                        , cleanupErrors, computeFreeVarNames
                                        )
import qualified Cryptol.TypeCheck.SimpleSolver as Simple
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
import           Cryptol.TypeCheck.PP(NameMap)
import           Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets)
import           Cryptol.Utils.Ident(Ident,Namespace(..))
import           Cryptol.Utils.Panic(panic)

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

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


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

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

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

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

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

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

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

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

runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM :: InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
info (IM ReaderT RO (StateT RW IO) a
m) =
  do IORef Int
counter <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
     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
<> (Newtype -> VarType) -> Map Name Newtype -> Map Name VarType
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Schema -> VarType
ExtVar (Schema -> VarType) -> (Newtype -> Schema) -> Newtype -> VarType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Newtype -> Schema
newtypeConType) (InferInput -> Map Name Newtype
inpNewtypes InferInput
info)

     rec RO
ro <- RO -> IO RO
forall (m :: * -> *) a. Monad m => a -> m a
return RO :: Range
-> Map Name VarType
-> [TParam]
-> ModuleG ScopeName
-> Map Int HasGoalSln
-> Bool
-> Bool
-> Solver
-> PrimMap
-> IORef Int
-> RO
RO { iRange :: Range
iRange     = InferInput -> Range
inpRange InferInput
info
                         , iVars :: Map Name VarType
iVars      = Map Name VarType
env
                         , iExtScope :: ModuleG ScopeName
iExtScope = (ScopeName -> ModuleG ScopeName
forall mname. mname -> ModuleG mname
emptyModule ScopeName
ExternalScope)
                             { mTySyns :: Map Name TySyn
mTySyns           = InferInput -> Map Name TySyn
inpTSyns InferInput
info
                             , mNewtypes :: Map Name Newtype
mNewtypes         = InferInput -> Map Name Newtype
inpNewtypes InferInput
info
                             , mPrimTypes :: Map Name AbstractType
mPrimTypes        = InferInput -> Map Name AbstractType
inpAbstractTypes InferInput
info
                             , mParamTypes :: Map Name ModTParam
mParamTypes       = InferInput -> Map Name ModTParam
inpParamTypes InferInput
info
                             , mParamFuns :: Map Name ModVParam
mParamFuns        = InferInput -> Map Name ModVParam
inpParamFuns InferInput
info
                             , mParamConstraints :: [Located Prop]
mParamConstraints = InferInput -> [Located Prop]
inpParamConstraints InferInput
info
                             }

                         , iTVars :: [TParam]
iTVars         = []
                         , iSolvedHasLazy :: Map Int HasGoalSln
iSolvedHasLazy = RW -> Map Int HasGoalSln
iSolvedHas RW
finalRW     -- RECURSION
                         , 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
                         }

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

     let theSu :: Subst
theSu    = RW -> Subst
iSubst RW
finalRW
         defSu :: Subst
defSu    = Subst -> Subst
defaultingSubst Subst
theSu
         warns :: [(Range, Warning)]
warns    = ((Range, 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, RW -> [HasGoal]
iHasCts 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,[HasGoal]
has) ->
              [(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 [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ (HasGoal -> Goal) -> [HasGoal] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map HasGoal -> Goal
hasGoal [HasGoal]
has
                ]

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

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


  rw :: RW
rw = RW :: [(Range, Error)]
-> [(Range, Warning)]
-> Subst
-> [Map Name Prop]
-> Map Int HasGoalSln
-> NameSeeds
-> Goals
-> [HasGoal]
-> [ModuleG ScopeName]
-> Map Name Schema
-> Supply
-> RW
RW { iErrors :: [(Range, Error)]
iErrors     = []
          , iWarnings :: [(Range, Warning)]
iWarnings   = []
          , iSubst :: Subst
iSubst      = Subst
emptySubst
          , iExistTVars :: [Map Name Prop]
iExistTVars = []

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

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

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

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







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


data ScopeName = ExternalScope
               | LocalScope
               | SubModule Name
               | 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 -> 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

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

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

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

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

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

  , 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 :: (a -> b) -> InferM a -> InferM b
fmap a -> b
f (IM ReaderT RO (StateT RW IO) a
m) = ReaderT RO (StateT RW IO) b -> InferM b
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM ((a -> b)
-> ReaderT RO (StateT RW IO) a -> ReaderT RO (StateT RW IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ReaderT RO (StateT RW IO) a
m)

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

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

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

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

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


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

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

inRangeMb :: Maybe Range -> InferM a -> InferM a
inRangeMb :: Maybe Range -> InferM a -> InferM a
inRangeMb 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 IO) Range -> InferM Range
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) Range -> InferM Range)
-> ReaderT RO (StateT RW IO) Range -> InferM Range
forall a b. (a -> b) -> a -> b
$ (RO -> Range) -> ReaderT RO (StateT RW IO) Range
forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Range
iRange

-- | Report an error.
recordError :: Error -> InferM ()
recordError :: Error -> InferM ()
recordError Error
e =
  do Range
r <- case Error
e of
            AmbiguousSize TVarInfo
d Maybe Prop
_ -> Range -> InferM Range
forall (m :: * -> *) a. Monad m => a -> m a
return (TVarInfo -> Range
tvarSource TVarInfo
d)
            Error
_ -> InferM Range
curRange
     ReaderT RO (StateT RW IO) () -> InferM ()
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) () -> InferM ())
-> ReaderT RO (StateT RW IO) () -> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ ((RW -> RW) -> ReaderT RO (StateT RW IO) ())
-> (RW -> RW) -> ReaderT RO (StateT RW IO) ()
forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iErrors :: [(Range, Error)]
iErrors = (Range
r,Error
e) (Range, Error) -> [(Range, Error)] -> [(Range, Error)]
forall a. a -> [a] -> [a]
: RW -> [(Range, Error)]
iErrors RW
s }

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

getSolver :: InferM SMT.Solver
getSolver :: InferM Solver
getSolver =
  do RO { Bool
[TParam]
IORef Int
Map Int HasGoalSln
Map Name VarType
Range
PrimMap
ModuleG ScopeName
Solver
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iCallStacks :: Bool
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iExtScope :: ModuleG ScopeName
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iCallStacks :: RO -> Bool
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iExtScope :: RO -> ModuleG ScopeName
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
.. } <- ReaderT RO (StateT RW IO) RO -> InferM RO
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM ReaderT RO (StateT RW IO) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     Solver -> InferM Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
iSolver

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


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

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

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

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


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

  where

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

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

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

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



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


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

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

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


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

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

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


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

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

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


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

checkParamKind :: TParam -> TPFlavor -> Kind -> InferM ()
checkParamKind TParam
tp TPFlavor
flav Kind
k =
    case TPFlavor
flav of
      TPModParam Name
_     -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- All kinds allowed as module parameters
      TPPropSynParam Name
_ -> InferM ()
starOrHashOrProp
      TPTySynParam Name
_   -> InferM ()
starOrHash
      TPSchemaParam Name
_  -> InferM ()
starOrHash
      TPNewtypeParam Name
_ -> InferM ()
starOrHash
      TPPrimParam Name
_    -> InferM ()
starOrHash
      TPFlavor
TPUnifyVar       -> InferM ()
starOrHash

  where
    starOrHashOrProp :: InferM ()
starOrHashOrProp =
      case Kind
k of
        Kind
KNum  -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Kind
KType -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Kind
KProp -> () -> InferM ()
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 (m :: * -> *) a. Monad m => a -> m a
return ()
        Kind
KType -> () -> InferM ()
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 :: Range -> TypeSource -> TVarInfo
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 :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
TParam { tpUnique :: Int
tpUnique = Int
x
                        , tpKind :: Kind
tpKind   = Kind
k
                        , tpFlav :: TPFlavor
tpFlav   = TPFlavor
flav
                        , tpInfo :: TVarInfo
tpInfo   = TVarInfo
desc
                        }
                , NameSeeds
s { seedTVar :: Int
seedTVar = Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 })

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


-- | Generate an unknown type.  The doc is a note about what is this type about.
newType :: TypeSource -> Kind -> InferM Type
newType :: TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
k = TVar -> Prop
TVar (TVar -> Prop) -> InferM TVar -> InferM Prop
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 -> Prop -> InferM [Prop]
unify (WithSource Prop
t1 TypeSource
src) Prop
t2 =
  do Prop
t1' <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
t1
     Prop
t2' <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
t2
     let ((Subst
su1, [Prop]
ps), [UnificationError]
errs) = Result (Subst, [Prop]) -> ((Subst, [Prop]), [UnificationError])
forall a. Result a -> (a, [UnificationError])
runResult (Prop -> Prop -> Result (Subst, [Prop])
mgu Prop
t1' Prop
t2')
     Subst -> InferM ()
extendSubst Subst
su1
     let toError :: UnificationError -> Error
         toError :: UnificationError -> Error
toError UnificationError
err =
           case UnificationError
err of
             UniTypeLenMismatch Int
_ Int
_ -> TypeSource -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Prop
t1' Prop
t2'
             UniTypeMismatch Prop
s1 Prop
s2  -> TypeSource -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Prop
s1 Prop
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 Prop
t       -> TypeSource -> Prop -> Prop -> Error
RecursiveType TypeSource
src (TVar -> Prop
TVar TVar
x) Prop
t
             UniNonPolyDepends TVar
x [TParam]
vs -> TypeSource -> Prop -> [TParam] -> Error
TypeVariableEscaped TypeSource
src (TVar -> Prop
TVar TVar
x) [TParam]
vs
             UniNonPoly TVar
x Prop
t         -> TypeSource -> TVar -> Prop -> Error
NotForAll TypeSource
src TVar
x Prop
t
     case [UnificationError]
errs of
       [] -> [Prop] -> InferM [Prop]
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
ps
       [UnificationError]
_  -> do (UnificationError -> InferM ()) -> [UnificationError] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Error -> InferM ()
recordError (Error -> InferM ())
-> (UnificationError -> Error) -> UnificationError -> InferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnificationError -> Error
toError) [UnificationError]
errs
                [Prop] -> InferM [Prop]
forall (m :: * -> *) a. Monad m => a -> m a
return []

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

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


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

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

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


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

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


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

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

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

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

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

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

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

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

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

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


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

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

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

-- | Returns the parameter functions declarations
getParamFuns :: InferM (Map Name ModVParam)
getParamFuns :: InferM (Map Name ModVParam)
getParamFuns = (ModuleG ScopeName -> Map Name ModVParam)
-> InferM (Map Name ModVParam)
forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope ModuleG ScopeName -> Map Name ModVParam
forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns

-- | 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 Prop]
getParamConstraints = (ModuleG ScopeName -> [Located Prop]) -> InferM [Located Prop]
forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope ModuleG ScopeName -> [Located Prop]
forall mname. ModuleG mname -> [Located Prop]
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 IO) (Set Name) -> InferM (Set Name)
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) (Set Name) -> InferM (Set Name))
-> ReaderT RO (StateT RW IO) (Set Name) -> InferM (Set Name)
forall a b. (a -> b) -> a -> b
$ (RO -> Set Name) -> ReaderT RO (StateT RW IO) (Set Name)
forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks ((RO -> Set Name) -> ReaderT RO (StateT RW IO) (Set Name))
-> (RO -> Set Name) -> ReaderT RO (StateT RW IO) (Set Name)
forall a b. (a -> b) -> a -> b
$ [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList ([Name] -> Set Name) -> (RO -> [Name]) -> RO -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TParam -> Maybe Name) -> [TParam] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName ([TParam] -> [Name]) -> (RO -> [TParam]) -> RO -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RO -> [TParam]
iTVars

-- | Return the keys of the bound variables that are in scope.
getBoundInScope :: InferM (Set TParam)
getBoundInScope :: InferM (Set TParam)
getBoundInScope =
  do RO
ro <- ReaderT RO (StateT RW IO) RO -> InferM RO
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM ReaderT RO (StateT RW IO) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     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 (m :: * -> *) a. Monad m => a -> m a
return (Set TParam -> InferM (Set TParam))
-> Set TParam -> InferM (Set TParam)
forall a b. (a -> b) -> a -> b
$! Set TParam -> Set TParam -> Set TParam
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TParam
params Set TParam
bound

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

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

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

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


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

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


-- | 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 IO) () -> InferM ()
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) () -> InferM ())
-> ReaderT RO (StateT RW IO) () -> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = ScopeName -> ModuleG ScopeName
forall mname. mname -> ModuleG mname
emptyModule ScopeName
nm ModuleG ScopeName -> [ModuleG ScopeName] -> [ModuleG ScopeName]
forall a. a -> [a] -> [a]
: RW -> [ModuleG ScopeName]
iScope RW
rw }

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

newSubmoduleScope :: Name -> [Import] -> ExportSpec Name -> InferM ()
newSubmoduleScope :: Name -> [Import] -> ExportSpec Name -> InferM ()
newSubmoduleScope Name
x [Import]
is ExportSpec Name
e =
  do ScopeName -> InferM ()
newScope (Name -> ScopeName
SubModule Name
x)
     (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
m -> ModuleG ScopeName
m { mImports :: [Import]
mImports = [Import]
is, mExports :: ExportSpec Name
mExports = ExportSpec Name
e }

newModuleScope :: P.ModName -> [Import] -> ExportSpec Name -> InferM ()
newModuleScope :: ModName -> [Import] -> ExportSpec Name -> InferM ()
newModuleScope ModName
x [Import]
is ExportSpec Name
e =
  do ScopeName -> InferM ()
newScope (ModName -> ScopeName
MTopModule ModName
x)
     (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
m -> ModuleG ScopeName
m { mImports :: [Import]
mImports = [Import]
is, mExports :: ExportSpec Name
mExports = ExportSpec Name
e }

-- | Update the current scope (first in the list). Assumes there is one.
updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope ModuleG ScopeName -> ModuleG ScopeName
f = ReaderT RO (StateT RW IO) () -> InferM ()
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) () -> InferM ())
-> ReaderT RO (StateT RW IO) () -> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = [ModuleG ScopeName] -> [ModuleG ScopeName]
upd (RW -> [ModuleG ScopeName]
iScope RW
rw) }
  where
  upd :: [ModuleG ScopeName] -> [ModuleG ScopeName]
upd [ModuleG ScopeName]
r =
    case [ModuleG ScopeName]
r of
      []       -> FilePath -> [FilePath] -> [ModuleG ScopeName]
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"updTopScope" [ FilePath
"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 IO) ([DeclGroup], Map Name TySyn)
-> InferM ([DeclGroup], Map Name TySyn)
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) ([DeclGroup], Map Name TySyn)
 -> InferM ([DeclGroup], Map Name TySyn))
-> ReaderT RO (StateT RW 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 IO) ([DeclGroup], Map Name TySyn)
forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets \RW
rw ->
       case RW -> [ModuleG ScopeName]
iScope RW
rw of
         ModuleG ScopeName
x : [ModuleG ScopeName]
xs | ScopeName
LocalScope <- ModuleG ScopeName -> ScopeName
forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
x ->
                    ( ([DeclGroup] -> [DeclGroup]
forall a. [a] -> [a]
reverse (ModuleG ScopeName -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
x), ModuleG ScopeName -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x), RW
rw { iScope :: [ModuleG ScopeName]
iScope = [ModuleG ScopeName]
xs })

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

endSubmodule :: InferM ()
endSubmodule :: InferM ()
endSubmodule =
  ReaderT RO (StateT RW IO) () -> InferM ()
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) () -> InferM ())
-> ReaderT RO (StateT RW IO) () -> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw ->
       case RW -> [ModuleG ScopeName]
iScope RW
rw of
         x :: ModuleG ScopeName
x@Module { mName :: forall mname. ModuleG mname -> mname
mName = SubModule Name
m } : ModuleG ScopeName
y : [ModuleG ScopeName]
more -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = ModuleG ScopeName
z ModuleG ScopeName -> [ModuleG ScopeName] -> [ModuleG ScopeName]
forall a. a -> [a] -> [a]
: [ModuleG ScopeName]
more }
           where
           x1 :: ModuleG Name
x1    = ModuleG ScopeName
x { mName :: Name
mName = Name
m }
           iface :: IfaceG Name
iface = ModuleG Name -> IfaceG Name
forall mname. ModuleG mname -> IfaceG mname
genIface ModuleG Name
x1
           me :: Map Name (ModuleG Name)
me = if ModuleG Name -> Bool
forall mname. ModuleG mname -> Bool
isParametrizedModule ModuleG Name
x1 then Name -> ModuleG Name -> Map Name (ModuleG Name)
forall k a. k -> a -> Map k a
Map.singleton Name
m ModuleG Name
x1 else Map Name (ModuleG Name)
forall a. Monoid a => a
mempty
           z :: ModuleG ScopeName
z = ModuleG ScopeName
y { mImports :: [Import]
mImports     = ModuleG ScopeName -> [Import]
forall mname. ModuleG mname -> [Import]
mImports ModuleG ScopeName
x [Import] -> [Import] -> [Import]
forall a. [a] -> [a] -> [a]
++ ModuleG ScopeName -> [Import]
forall mname. ModuleG mname -> [Import]
mImports ModuleG ScopeName
y -- just for deps
                 , mSubModules :: Map Name (IfaceG Name)
mSubModules  = Name
-> IfaceG Name -> Map Name (IfaceG Name) -> Map Name (IfaceG Name)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
m IfaceG Name
iface (ModuleG ScopeName -> Map Name (IfaceG Name)
forall mname. ModuleG mname -> Map Name (IfaceG Name)
mSubModules ModuleG ScopeName
y)

                 , mTySyns :: Map Name TySyn
mTySyns      = ModuleG ScopeName -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x Map Name TySyn -> Map Name TySyn -> Map Name TySyn
forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
y
                 , mNewtypes :: Map Name Newtype
mNewtypes    = ModuleG ScopeName -> Map Name Newtype
forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG ScopeName
x Map Name Newtype -> Map Name Newtype -> Map Name Newtype
forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> Map Name Newtype
forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG ScopeName
y
                 , mPrimTypes :: Map Name AbstractType
mPrimTypes   = ModuleG ScopeName -> Map Name AbstractType
forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG ScopeName
x Map Name AbstractType
-> Map Name AbstractType -> Map Name AbstractType
forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> Map Name AbstractType
forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG ScopeName
y
                 , mDecls :: [DeclGroup]
mDecls       = ModuleG ScopeName -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
x [DeclGroup] -> [DeclGroup] -> [DeclGroup]
forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
y
                 , mFunctors :: Map Name (ModuleG Name)
mFunctors    = Map Name (ModuleG Name)
me 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
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]
_ -> FilePath -> [FilePath] -> RW
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"endSubmodule" [ FilePath
"Not a submodule" ]


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

endModuleInstance :: InferM ()
endModuleInstance :: InferM ()
endModuleInstance =
  ReaderT RO (StateT RW IO) () -> InferM ()
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) () -> InferM ())
-> ReaderT RO (StateT RW IO) () -> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw ->
    case RW -> [ModuleG ScopeName]
iScope RW
rw of
      [ ModuleG ScopeName
x ] | MTopModule ModName
_ <- ModuleG ScopeName -> ScopeName
forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
x -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = [] }
      [ModuleG ScopeName]
_ -> FilePath -> [FilePath] -> RW
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"endModuleInstance" [ FilePath
"Not single top module" ]


-- | Get an environment combining all nested scopes.
getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope :: (ModuleG ScopeName -> a) -> InferM a
getScope ModuleG ScopeName -> a
f =
  do RO
ro <- ReaderT RO (StateT RW IO) RO -> InferM RO
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM ReaderT RO (StateT RW IO) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     RW
rw <- ReaderT RO (StateT RW IO) RW -> InferM RW
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM ReaderT RO (StateT RW IO) RW
forall (m :: * -> *) i. StateM m i => m i
get
     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)))

addDecls :: DeclGroup -> InferM ()
addDecls :: DeclGroup -> InferM ()
addDecls DeclGroup
ds =
  do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mDecls :: [DeclGroup]
mDecls = DeclGroup
ds DeclGroup -> [DeclGroup] -> [DeclGroup]
forall a. a -> [a] -> [a]
: ModuleG ScopeName -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
r }
     ReaderT RO (StateT RW IO) () -> InferM ()
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) () -> InferM ())
-> ReaderT RO (StateT RW IO) () -> InferM ()
forall a b. (a -> b) -> a -> b
$ (RW -> RW) -> ReaderT RO (StateT RW IO) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes :: Map Name Schema
iBindTypes = RW -> Map Name Schema
new RW
rw }
  where
  add :: Decl -> Map Name Schema -> Map Name Schema
add Decl
d   = Name -> Schema -> Map Name Schema -> Map Name Schema
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Decl -> Name
dName Decl
d) (Decl -> Schema
dSignature Decl
d)
  new :: RW -> Map Name Schema
new RW
rw  = (Decl -> Map Name Schema -> Map Name Schema)
-> Map Name Schema -> [Decl] -> Map Name Schema
forall (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
     FilePath -> Name -> InferM ()
checkTShadowing FilePath
"synonym" Name
x
     (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mTySyns :: Map Name TySyn
mTySyns = Name -> TySyn -> Map Name TySyn -> Map Name TySyn
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x TySyn
t (ModuleG ScopeName -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
r) }

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

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

addParamType :: ModTParam -> InferM ()
addParamType :: ModTParam -> InferM ()
addParamType ModTParam
a =
  (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mParamTypes :: Map Name ModTParam
mParamTypes = Name -> ModTParam -> Map Name ModTParam -> Map Name ModTParam
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModTParam -> Name
mtpName ModTParam
a) ModTParam
a (ModuleG ScopeName -> Map Name ModTParam
forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG ScopeName
r) }

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

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




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


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

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

withVar :: Name -> Schema -> InferM a -> InferM a
withVar :: Name -> Schema -> InferM a -> InferM a
withVar 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 :: (Name, Located Prop) -> InferM a -> InferM a
withMonoType (Name
x,Located Prop
lt) = Name -> Schema -> InferM a -> InferM a
forall a. Name -> Schema -> InferM a -> InferM a
withVar Name
x ([TParam] -> [Prop] -> Prop -> Schema
Forall [] [] (Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
lt))

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

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


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

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

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

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

instance Functor KindM where
  fmap :: (a -> b) -> KindM a -> KindM b
fmap 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ReaderT KRO (StateT KRW InferM) a
m)

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

instance Monad KindM where
  return :: a -> KindM a
return a
x      = ReaderT KRO (StateT KRW InferM) a -> KindM a
forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (a -> ReaderT KRO (StateT KRW InferM) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x)
  KM ReaderT KRO (StateT KRW InferM) a
m >>= :: 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 (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 :: FilePath -> KindM a
fail FilePath
x        = ReaderT KRO (StateT KRW InferM) a -> KindM a
forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (FilePath -> ReaderT KRO (StateT KRW InferM) a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail FilePath
x)


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

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

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

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

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

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

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

-- | Reports an error.
kRecordError :: Error -> KindM ()
kRecordError :: Error -> KindM ()
kRecordError 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 :: 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 (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a)
-> StateT KRW InferM a -> ReaderT KRO (StateT KRW InferM) a
forall a b. (a -> b) -> a -> b
$ InferM a -> StateT KRW InferM a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (InferM a -> StateT KRW InferM a)
-> InferM a -> StateT KRW InferM a
forall a b. (a -> b) -> a -> b
$ IO a -> InferM a
forall a. IO a -> InferM a
io IO a
m

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

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

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

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

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

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

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

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

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

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

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