-- |
-- 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 #-}
module Cryptol.TypeCheck.Monad
  ( module Cryptol.TypeCheck.Monad
  , module Cryptol.TypeCheck.InferTypes
  ) where

import           Cryptol.ModuleSystem.Name
                    (FreshM(..),Supply,mkParameter
                    , nameInfo, NameInfo(..),NameSource(..))
import           Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.Subst
import           Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
import           Cryptol.TypeCheck.InferTypes
import           Cryptol.TypeCheck.Error( Warning(..),Error(..)
                                        , cleanupErrors, 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)
import           Cryptol.Utils.Panic(panic)

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.Maybe(mapMaybe,fromMaybe)
import           MonadLib hiding (mapM)

import           Data.IORef


import GHC.Generics (Generic)
import Control.DeepSeq

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

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


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

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

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

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


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

-- | The initial seeds, used when checking a fresh program.
-- XXX: why does this start at 10?
nameSeeds :: NameSeeds
nameSeeds :: NameSeeds
nameSeeds = 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
[Located Prop]
[TParam]
IORef Int
Map Int HasGoalSln
Map Name (DefLoc, AbstractType)
Map Name (DefLoc, Newtype)
Map Name (DefLoc, TySyn)
Map Name ModVParam
Map Name ModTParam
Map Name VarType
Range
PrimMap
Solver
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iParamFuns :: RO -> Map Name ModVParam
iParamConstraints :: RO -> [Located Prop]
iParamTypes :: RO -> Map Name ModTParam
iAbstractTypes :: RO -> Map Name (DefLoc, AbstractType)
iNewtypes :: RO -> Map Name (DefLoc, Newtype)
iTSyns :: RO -> Map Name (DefLoc, TySyn)
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iParamFuns :: Map Name ModVParam
iParamConstraints :: [Located Prop]
iParamTypes :: Map Name ModTParam
iAbstractTypes :: Map Name (DefLoc, AbstractType)
iNewtypes :: Map Name (DefLoc, Newtype)
iTSyns :: Map Name (DefLoc, TySyn)
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) = SolverConfig
-> (Solver -> IO (InferOutput a)) -> IO (InferOutput a)
forall a. SolverConfig -> (Solver -> IO a) -> IO a
SMT.withSolver (InferInput -> SolverConfig
inpSolverConfig InferInput
info) ((Solver -> IO (InferOutput a)) -> IO (InferOutput a))
-> (Solver -> IO (InferOutput a)) -> IO (InferOutput a)
forall a b. (a -> b) -> a -> b
$ \Solver
solver ->
  do IORef Int
counter <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
     rec RO
ro <- RO -> IO RO
forall (m :: * -> *) a. Monad m => a -> m a
return RO :: Range
-> Map Name VarType
-> [TParam]
-> Map Name (DefLoc, TySyn)
-> Map Name (DefLoc, Newtype)
-> Map Name (DefLoc, AbstractType)
-> Map Name ModTParam
-> [Located Prop]
-> Map Name ModVParam
-> Map Int HasGoalSln
-> Bool
-> Solver
-> PrimMap
-> IORef Int
-> RO
RO { iRange :: Range
iRange     = InferInput -> Range
inpRange InferInput
info
                         , iVars :: Map Name VarType
iVars          = (Schema -> VarType) -> Map Name Schema -> Map Name VarType
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Schema -> VarType
ExtVar (InferInput -> Map Name Schema
inpVars InferInput
info)
                         , iTVars :: [TParam]
iTVars         = []
                         , iTSyns :: Map Name (DefLoc, TySyn)
iTSyns         = (TySyn -> (DefLoc, TySyn))
-> Map Name TySyn -> Map Name (DefLoc, TySyn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TySyn -> (DefLoc, TySyn)
forall b. b -> (DefLoc, b)
mkExternal (InferInput -> Map Name TySyn
inpTSyns InferInput
info)
                         , iNewtypes :: Map Name (DefLoc, Newtype)
iNewtypes      = (Newtype -> (DefLoc, Newtype))
-> Map Name Newtype -> Map Name (DefLoc, Newtype)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Newtype -> (DefLoc, Newtype)
forall b. b -> (DefLoc, b)
mkExternal (InferInput -> Map Name Newtype
inpNewtypes InferInput
info)
                         , iAbstractTypes :: Map Name (DefLoc, AbstractType)
iAbstractTypes = AbstractType -> (DefLoc, AbstractType)
forall b. b -> (DefLoc, b)
mkExternal (AbstractType -> (DefLoc, AbstractType))
-> Map Name AbstractType -> Map Name (DefLoc, AbstractType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferInput -> Map Name AbstractType
inpAbstractTypes InferInput
info
                         , iParamTypes :: Map Name ModTParam
iParamTypes    = InferInput -> Map Name ModTParam
inpParamTypes InferInput
info
                         , iParamFuns :: Map Name ModVParam
iParamFuns     = InferInput -> Map Name ModVParam
inpParamFuns InferInput
info
                         , iParamConstraints :: [Located Prop]
iParamConstraints = InferInput -> [Located Prop]
inpParamConstraints InferInput
info

                         , iSolvedHasLazy :: Map Int HasGoalSln
iSolvedHasLazy = RW -> Map Int HasGoalSln
iSolvedHas RW
finalRW     -- RECURSION
                         , iMonoBinds :: Bool
iMonoBinds     = InferInput -> Bool
inpMonoBinds InferInput
info
                         , iSolver :: Solver
iSolver        = Solver
solver
                         , iPrimNames :: PrimMap
iPrimNames     = InferInput -> PrimMap
inpPrimNames InferInput
info
                         , iSolveCounter :: IORef Int
iSolveCounter  = IORef Int
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)


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

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

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

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







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

data DefLoc = IsLocal | IsExternal

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

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

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

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

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

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


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

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

  , RO -> Solver
iSolver :: SMT.Solver

  , RO -> PrimMap
iPrimNames :: !PrimMap

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

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

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

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

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

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

  , 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 ModName
_ NameSource
SystemName <- Name -> NameInfo
nameInfo Name
n
      = Bool
True
    | Bool
otherwise = Bool
False

getSolver :: InferM SMT.Solver
getSolver :: InferM Solver
getSolver =
  do RO { Bool
[Located Prop]
[TParam]
IORef Int
Map Int HasGoalSln
Map Name (DefLoc, AbstractType)
Map Name (DefLoc, Newtype)
Map Name (DefLoc, TySyn)
Map Name ModVParam
Map Name ModTParam
Map Name VarType
Range
PrimMap
Solver
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iParamFuns :: Map Name ModVParam
iParamConstraints :: [Located Prop]
iParamTypes :: Map Name ModTParam
iAbstractTypes :: Map Name (DefLoc, AbstractType)
iNewtypes :: Map Name (DefLoc, Newtype)
iTSyns :: Map Name (DefLoc, TySyn)
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iParamFuns :: RO -> Map Name ModVParam
iParamConstraints :: RO -> [Located Prop]
iParamTypes :: RO -> Map Name ModTParam
iAbstractTypes :: RO -> Map Name (DefLoc, AbstractType)
iNewtypes :: RO -> Map Name (DefLoc, Newtype)
iTSyns :: RO -> Map Name (DefLoc, TySyn)
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
[Located Prop]
[TParam]
IORef Int
Map Int HasGoalSln
Map Name (DefLoc, AbstractType)
Map Name (DefLoc, Newtype)
Map Name (DefLoc, TySyn)
Map Name ModVParam
Map Name ModTParam
Map Name VarType
Range
PrimMap
Solver
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iParamFuns :: Map Name ModVParam
iParamConstraints :: [Located Prop]
iParamTypes :: Map Name ModTParam
iAbstractTypes :: Map Name (DefLoc, AbstractType)
iNewtypes :: Map Name (DefLoc, Newtype)
iTSyns :: Map Name (DefLoc, TySyn)
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iParamFuns :: RO -> Map Name ModVParam
iParamConstraints :: RO -> [Located Prop]
iParamTypes :: RO -> Map Name ModTParam
iAbstractTypes :: RO -> Map Name (DefLoc, AbstractType)
iNewtypes :: RO -> Map Name (DefLoc, Newtype)
iTSyns :: RO -> Map Name (DefLoc, TySyn)
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]
[HasGoal]
Map Int HasGoalSln
Supply
Subst
Goals
NameSeeds
iSupply :: Supply
iHasCts :: [HasGoal]
iCts :: Goals
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Prop]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
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]
-> Supply
-> RW
RW { iCts :: Goals
iCts = Goals
emptyGoals, [(Range, Error)]
[(Range, Warning)]
[Map Name Prop]
[HasGoal]
Map Int HasGoalSln
Supply
Subst
NameSeeds
iSupply :: Supply
iHasCts :: [HasGoal]
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Prop]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
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]
[HasGoal]
Map Int HasGoalSln
Supply
Subst
Goals
NameSeeds
iSupply :: Supply
iHasCts :: [HasGoal]
iCts :: Goals
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Prop]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
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]
-> Supply
-> RW
RW { iCts :: Goals
iCts = Goals
gs, [(Range, Error)]
[(Range, Warning)]
[Map Name Prop]
[HasGoal]
Map Int HasGoalSln
Supply
Subst
NameSeeds
iSupply :: Supply
iHasCts :: [HasGoal]
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Prop]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
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 :: Ident -> InferM Name
newParamName :: Ident -> InferM Name
newParamName Ident
x =
  do Range
r <- InferM Range
curRange
     (Supply -> (Name, Supply)) -> InferM Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (Ident -> Range -> Supply -> (Name, Supply)
mkParameter Ident
x Range
r)

newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a
newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a
newName 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 })



-- | 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 = (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 })
  where 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)
                        }


-- | 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
t  -> VarType -> InferM VarType
forall (m :: * -> *) a. Monad m => a -> m a
return VarType
t
       Maybe VarType
Nothing ->
         do Maybe Newtype
mbNT <- Name -> InferM (Maybe Newtype)
lookupNewtype Name
x
            case Maybe Newtype
mbNT of
              Just Newtype
nt -> VarType -> InferM VarType
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> VarType
ExtVar (Newtype -> Schema
newtypeConType Newtype
nt))
              Maybe Newtype
Nothing ->
                do Maybe ModVParam
mbParamFun <- Name -> InferM (Maybe ModVParam)
lookupParamFun Name
x
                   case Maybe ModVParam
mbParamFun of
                     Just ModVParam
pf -> VarType -> InferM VarType
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> VarType
ExtVar (ModVParam -> Schema
mvpType ModVParam
pf))
                     Maybe ModVParam
Nothing -> FilePath -> [FilePath] -> InferM VarType
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"lookupVar" [ FilePath
"Undefined type variable"
                                                  , Name -> FilePath
forall a. Show a => a -> FilePath
show Name
x]

-- | Lookup a type variable.  Return `Nothing` if there is no such variable
-- in scope, in which case we must be dealing with a type constant.
lookupTParam :: Name -> InferM (Maybe TParam)
lookupTParam :: Name -> InferM (Maybe TParam)
lookupTParam 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 = (Map Name (DefLoc, TySyn) -> Maybe TySyn)
-> InferM (Map Name (DefLoc, TySyn)) -> InferM (Maybe TySyn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((DefLoc, TySyn) -> TySyn) -> Maybe (DefLoc, TySyn) -> Maybe TySyn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DefLoc, TySyn) -> TySyn
forall a b. (a, b) -> b
snd (Maybe (DefLoc, TySyn) -> Maybe TySyn)
-> (Map Name (DefLoc, TySyn) -> Maybe (DefLoc, TySyn))
-> Map Name (DefLoc, TySyn)
-> Maybe TySyn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Map Name (DefLoc, TySyn) -> Maybe (DefLoc, TySyn)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x) InferM (Map Name (DefLoc, TySyn))
getTSyns

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

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

-- | Lookup the kind of a parameter type
lookupParamType :: Name -> InferM (Maybe ModTParam)
lookupParamType :: Name -> InferM (Maybe ModTParam)
lookupParamType 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 (DefLoc,TySyn))
getTSyns :: InferM (Map Name (DefLoc, TySyn))
getTSyns = ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
-> InferM (Map Name (DefLoc, TySyn))
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM (ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
 -> InferM (Map Name (DefLoc, TySyn)))
-> ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
-> InferM (Map Name (DefLoc, TySyn))
forall a b. (a -> b) -> a -> b
$ (RO -> Map Name (DefLoc, TySyn))
-> ReaderT RO (StateT RW IO) (Map Name (DefLoc, TySyn))
forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Map Name (DefLoc, TySyn)
iTSyns

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

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

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

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

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

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

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

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

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

checkTShadowing :: String -> Name -> InferM ()
checkTShadowing :: FilePath -> Name -> InferM ()
checkTShadowing FilePath
this Name
new =
  do RO
ro <- ReaderT RO (StateT RW IO) RO -> InferM RO
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM ReaderT RO (StateT RW IO) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     RW
rw <- ReaderT RO (StateT RW IO) RW -> InferM RW
forall a. ReaderT RO (StateT RW IO) a -> InferM a
IM ReaderT RO (StateT RW IO) RW
forall (m :: * -> *) i. StateM m i => m i
get
     let shadowed :: Maybe FilePath
shadowed =
           do (DefLoc, TySyn)
_ <- Name -> Map Name (DefLoc, TySyn) -> Maybe (DefLoc, TySyn)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
new (RO -> Map Name (DefLoc, TySyn)
iTSyns RO
ro)
              FilePath -> Maybe FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return 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

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

withNewtype :: Newtype -> InferM a -> InferM a
withNewtype :: Newtype -> InferM a -> InferM a
withNewtype Newtype
t (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 { iNewtypes :: Map Name (DefLoc, Newtype)
iNewtypes = Name
-> (DefLoc, Newtype)
-> Map Name (DefLoc, Newtype)
-> Map Name (DefLoc, Newtype)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Newtype -> Name
ntName Newtype
t) (DefLoc
IsLocal,Newtype
t)
                                                     (RO -> Map Name (DefLoc, Newtype)
iNewtypes RO
r) }) ReaderT RO (StateT RW IO) a
m

withPrimType :: AbstractType -> InferM a -> InferM a
withPrimType :: AbstractType -> InferM a -> InferM a
withPrimType AbstractType
t (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 { iAbstractTypes :: Map Name (DefLoc, AbstractType)
iAbstractTypes = Name
-> (DefLoc, AbstractType)
-> Map Name (DefLoc, AbstractType)
-> Map Name (DefLoc, AbstractType)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (AbstractType -> Name
atName AbstractType
t) (DefLoc
IsLocal,AbstractType
t)
                                                        (RO -> Map Name (DefLoc, AbstractType)
iAbstractTypes RO
r) }) ReaderT RO (StateT RW IO) a
m


withParamType :: ModTParam -> InferM a -> InferM a
withParamType :: ModTParam -> InferM a -> InferM a
withParamType ModTParam
a (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 { iParamTypes :: Map Name ModTParam
iParamTypes = Name -> ModTParam -> Map Name ModTParam -> Map Name ModTParam
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModTParam -> Name
mtpName ModTParam
a) ModTParam
a (RO -> Map Name ModTParam
iParamTypes RO
r) })
        ReaderT RO (StateT RW IO) a
m

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

-- | Add some assumptions for an entire module
withParameterConstraints :: [Located Prop] -> InferM a -> InferM a
withParameterConstraints :: [Located Prop] -> InferM a -> InferM a
withParameterConstraints [Located Prop]
ps (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 { iParamConstraints :: [Located Prop]
iParamConstraints = [Located Prop]
ps [Located Prop] -> [Located Prop] -> [Located Prop]
forall a. [a] -> [a] -> [a]
++ RO -> [Located Prop]
iParamConstraints RO
r }) ReaderT RO (StateT RW IO) a
m


-- | The sub-computation is performed with the given variables in scope.
withMonoType :: (Name,Located Type) -> InferM a -> InferM a
withMonoType :: (Name, Located Prop) -> InferM a -> InferM a
withMonoType (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)

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

-- | Perform the given computation in a new scope (i.e., the subcomputation
-- may use existential type variables).
inNewScope :: InferM a -> InferM a
inNewScope :: InferM a -> InferM a
inNewScope 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



--------------------------------------------------------------------------------
-- 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