-- |
-- Module      :  Cryptol.TypeCheck.Monad
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# LANGUAGE Safe #-}
{-# 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)
import           Cryptol.TypeCheck.PP (brackets, commaSep)
import qualified Cryptol.TypeCheck.SimpleSolver as Simple
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
import           Cryptol.Utils.PP(pp, (<+>), text, quotes)
import           Cryptol.Utils.Ident(Ident)
import           Cryptol.Utils.Panic(panic)

import qualified Control.Applicative as A
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

import Prelude ()
import Prelude.Compat


-- | 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 = $WNameSeeds :: Int -> Int -> NameSeeds
NameSeeds { seedTVar :: Int
seedTVar = 10, seedGoal :: Int
seedGoal = 0 }


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

  | InferOK [(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 { .. } <- 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
+1)

runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM :: InferInput -> InferM a -> IO (InferOutput a)
runInferM info :: InferInput
info (IM m :: 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
solver ->
  do IORef Int
coutner <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef 0
     rec RO
ro <- RO -> IO RO
forall (m :: * -> *) a. Monad m => a -> m a
return $WRO :: 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
coutner
                         }

         (result :: a
result, finalRW :: 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
r,Subst -> Warning -> Warning
forall t. TVars t => Subst -> t -> t
apSubst Subst
theSu Warning
w) | (r :: Range
r,w :: Warning
w) <- 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
           (cts :: Goals
cts,[])
             | Goals -> Bool
nullGoals Goals
cts
                   -> InferOutput a -> IO (InferOutput a)
forall (m :: * -> *) a. Monad m => a -> m a
return (InferOutput a -> IO (InferOutput a))
-> InferOutput a -> IO (InferOutput a)
forall a b. (a -> b) -> a -> b
$ [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
forall a.
[(Range, Warning)] -> NameSeeds -> Supply -> a -> 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)
           (cts :: Goals
cts,has :: [HasGoal]
has) -> InferOutput a -> IO (InferOutput a)
forall (m :: * -> *) a. Monad m => a -> m a
return (InferOutput a -> IO (InferOutput a))
-> InferOutput a -> IO (InferOutput a)
forall a b. (a -> b) -> a -> b
$ [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
forall a. [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
InferFailed [(Range, Warning)]
warns
                ([(Range, Error)] -> InferOutput a)
-> [(Range, Error)] -> InferOutput a
forall a b. (a -> b) -> a -> b
$ [(Range, Error)] -> [(Range, Error)]
cleanupErrors
                [ ( Goal -> Range
goalRange Goal
g
                  , Bool -> [Goal] -> Error
UnsolvedGoals Bool
False [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
                ]
       errs :: [(Range, Error)]
errs -> InferOutput a -> IO (InferOutput a)
forall (m :: * -> *) a. Monad m => a -> m a
return (InferOutput a -> IO (InferOutput a))
-> InferOutput a -> IO (InferOutput a)
forall a b. (a -> b) -> a -> b
$ [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
forall a. [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
InferFailed [(Range, Warning)]
warns
                      ([(Range, Error)] -> InferOutput a)
-> [(Range, Error)] -> InferOutput a
forall a b. (a -> b) -> a -> b
$ [(Range, Error)] -> [(Range, Error)]
cleanupErrors [(Range
r,Subst -> Error -> Error
forall t. TVars t => Subst -> t -> t
apSubst Subst
theSu Error
e) | (r :: Range
r,e :: Error
e) <- [(Range, Error)]
errs]

  where
  mkExternal :: b -> (DefLoc, b)
mkExternal x :: b
x = (DefLoc
IsExternal, b
x)
  rw :: RW
rw = $WRW :: [(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 it solution properly. -}

  , RW -> Supply
iSupply :: !Supply
  }

instance Functor InferM where
  fmap :: (a -> b) -> InferM a -> InferM b
fmap f :: a -> b
f (IM m :: 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 x :: 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 m :: ReaderT RO (StateT RW IO) a
m >>= :: InferM a -> (a -> InferM b) -> InferM b
>>= f :: 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 MonadFail InferM where
  fail :: FilePath -> InferM a
fail x :: 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 f :: 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 f :: 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
a,s' :: 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 m :: 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 r :: Range
r (IM m :: 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
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 Nothing m :: InferM a
m  = InferM a
m
inRangeMb (Just r :: Range
r) m :: 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 e :: Error
e =
  do Range
r <- 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
$ \s :: 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 w :: 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 d :: TVarInfo
d _ -> Range -> InferM Range
forall (m :: * -> *) a. Monad m => a -> m a
return (TVarInfo -> Range
tvarSource TVarInfo
d)
            _ -> 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
$ \s :: 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 d :: TVarInfo
d _ <- Warning
w
    , Just n :: Name
n <- TVarSource -> Maybe Name
tvSourceName (TVarInfo -> TVarSource
tvarDesc TVarInfo
d)
    , Declared _ SystemName <- Name -> NameInfo
nameInfo Name
n
      = Bool
True
    | Bool
otherwise = Bool
False

getSolver :: InferM SMT.Solver
getSolver :: InferM Solver
getSolver =
  do 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
     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 { .. } <- 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 goalSource :: ConstraintSource
goalSource goal :: 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 { .. }

-- | 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 src :: ConstraintSource
src ps :: [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
$ \s :: 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 gs0 :: [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 gs :: [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
$ \s :: 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 m :: 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 { .. } -> (Goals
iCts, $WRW :: [(Range, Error)]
-> [(Range, Warning)]
-> Subst
-> [Map Name Prop]
-> Map Int HasGoalSln
-> NameSeeds
-> Goals
-> [HasGoal]
-> Supply
-> RW
RW { iCts :: Goals
iCts = Goals
emptyGoals, .. })

  -- set the type map directly
  setGoals' :: Goals -> InferM ()
setGoals' gs :: 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 { .. } -> ((),   $WRW :: [(Range, Error)]
-> [(Range, Warning)]
-> Subst
-> [Map Name Prop]
-> Map Int HasGoalSln
-> NameSeeds
-> Goals
-> [HasGoal]
-> Supply
-> RW
RW { iCts :: Goals
iCts = Goals
gs, .. })

simpGoal :: Goal -> InferM [Goal]
simpGoal :: Goal -> InferM [Goal]
simpGoal g :: Goal
g =
  case Ctxt -> Prop -> Prop
Simple.simplify Ctxt
forall k a. Map k a
Map.empty (Goal -> Prop
goal Goal
g) of
    p :: Prop
p | Just e :: TCErrorMessage
e <- Prop -> Maybe TCErrorMessage
tIsError Prop
p ->
        do Error -> InferM ()
recordError (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$ Doc -> Error
ErrorMsg (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ TCErrorMessage -> FilePath
tcErrorMessage TCErrorMessage
e
           [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 gs :: [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 l :: Selector
l ty :: Prop
ty f :: 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
$ \s :: 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 e1 :: HasGoalSln
e1 -> HasGoalSln
e1
                Nothing -> FilePath -> [FilePath] -> HasGoalSln
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "newHasGoal" ["Unsolved has goal in result"]


-- | Add a previously generate has constrained
addHasGoal :: HasGoal -> InferM ()
addHasGoal :: HasGoal -> InferM ()
addHasGoal g :: 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
$ \s :: 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
$ \s :: 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 n :: Int
n e :: 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
$ \s :: 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 x :: 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 upd :: 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
$ \s :: RW
s -> let (x :: a
x,seeds :: 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
$ \s :: 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
+ 1})

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



-- | Generate a new free type variable.
newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam
newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam
newTParam nm :: TParam Name
nm flav :: TPFlavor
flav k :: 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
$ \s :: NameSeeds
s ->
  let x :: Int
x = NameSeeds -> Int
seedTVar NameSeeds
s
  in ($WTParam :: 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
+ 1 })
  where desc :: TVarInfo
desc = TVarInfo :: Range -> TVarSource -> TVarInfo
TVarInfo { tvarDesc :: TVarSource
tvarDesc = Name -> TVarSource
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 :: TVarSource -> Kind -> InferM Type
newType :: TVarSource -> Kind -> InferM Prop
newType src :: TVarSource
src k :: Kind
k = TVar -> Prop
TVar (TVar -> Prop) -> InferM TVar -> InferM Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` TVarSource -> Kind -> InferM TVar
newTVar TVarSource
src Kind
k



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


-- | Record that the two types should be syntactically equal.
unify :: Type -> Type -> InferM [Prop]
unify :: Prop -> Prop -> InferM [Prop]
unify t1 :: Prop
t1 t2 :: 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 ((su1 :: Subst
su1, ps :: [Prop]
ps), errs :: [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 err :: UnificationError
err =
           case UnificationError
err of
             UniTypeLenMismatch _ _ -> Prop -> Prop -> Error
TypeMismatch Prop
t1' Prop
t2'
             UniTypeMismatch s1 :: Prop
s1 s2 :: Prop
s2  -> Prop -> Prop -> Error
TypeMismatch Prop
s1 Prop
s2
             UniKindMismatch k1 :: Kind
k1 k2 :: Kind
k2  -> Kind -> Kind -> Error
KindMismatch Kind
k1 Kind
k2
             UniRecursive x :: TVar
x t :: Prop
t       -> Prop -> Prop -> Error
RecursiveType (TVar -> Prop
TVar TVar
x) Prop
t
             UniNonPolyDepends x :: TVar
x vs :: [TParam]
vs -> Prop -> [TParam] -> Error
TypeVariableEscaped (TVar -> Prop
TVar TVar
x) [TParam]
vs
             UniNonPoly x :: TVar
x t :: Prop
t         -> TVar -> Prop -> Error
NotForAll TVar
x Prop
t
     case [UnificationError]
errs of
       [] -> [Prop] -> InferM [Prop]
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
ps
       _  -> 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
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 ps :: [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 gs :: [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 su :: 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
$ \s :: 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 (v :: TVar
v, ty :: Prop
ty) =
      case TVar
v of
        TVBound _ ->
          FilePath -> [FilePath] -> InferM ()
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "Cryptol.TypeCheck.Monad.extendSubst"
            [ "Substitution instantiates bound variable:"
            , "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)
            , "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 _ _ tvs :: Set TParam
tvs _ ->
          do let bounds :: TVar -> Set TParam
bounds tv :: TVar
tv =
                   case TVar
tv of
                     TVBound tp :: TParam
tp -> TParam -> Set TParam
forall a. a -> Set a
Set.singleton TParam
tp
                     TVFree _ _ tps :: Set TParam
tps _ -> Set TParam
tps
             let vars :: Set TParam
vars = [Set TParam] -> Set TParam
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((TVar -> Set TParam) -> [TVar] -> [Set TParam]
forall a b. (a -> b) -> [a] -> [b]
map TVar -> Set TParam
bounds (Set TVar -> [TVar]
forall a. Set a -> [a]
Set.elems (Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Prop
ty)))
                 -- (Set.filter isBoundTV (fvs ty))
             let escaped :: Set TParam
escaped = Set TParam -> Set TParam -> Set TParam
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TParam
vars 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 "Cryptol.TypeCheck.Monad.extendSubst"
                 [ "Escaped quantified variables:"
                 , "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 ":=" Doc -> Doc -> Doc
<+> Prop -> Doc
forall a. PP a => a -> Doc
pp Prop
ty)
                 , "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))))
                 , "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
$ \v :: VarType
v ->
                  case VarType
v of
                    ExtVar sch :: Schema
sch  -> Schema -> InferM (Set TVar)
forall t. (FVS t, TVars t) => t -> InferM (Set TVar)
getVars Schema
sch
                    CurSCC _ t :: 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 x :: 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 x :: 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 t :: VarType
t  -> VarType -> InferM VarType
forall (m :: * -> *) a. Monad m => a -> m a
return VarType
t
       Nothing ->
         do Maybe Newtype
mbNT <- Name -> InferM (Maybe Newtype)
lookupNewtype Name
x
            case Maybe Newtype
mbNT of
              Just nt :: Newtype
nt -> VarType -> InferM VarType
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> VarType
ExtVar (Newtype -> Schema
newtypeConType Newtype
nt))
              Nothing ->
                do Maybe ModVParam
mbParamFun <- Name -> InferM (Maybe ModVParam)
lookupParamFun Name
x
                   case Maybe ModVParam
mbParamFun of
                     Just pf :: ModVParam
pf -> VarType -> InferM VarType
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> VarType
ExtVar (ModVParam -> Schema
mvpType ModVParam
pf))
                     Nothing -> FilePath -> [FilePath] -> InferM VarType
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "lookupVar" [ "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 x :: 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 tp :: 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 x :: 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 x :: 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 x :: 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 x :: 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 x :: 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 x :: Name
x k :: 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 ty :: Prop
ty -> Prop -> InferM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
ty
       Nothing ->
         case [Map Name Prop]
scopes of
           [] ->
              do Error -> InferM ()
recordError (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$ Doc -> Error
ErrorMsg
                             (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text "Undefined type" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
x)
                                    Doc -> Doc -> Doc
<+> FilePath -> Doc
text (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
x)
                 TVarSource -> Kind -> InferM Prop
newType TVarSource
TypeErrorPlaceHolder Kind
k

           sc :: Map Name Prop
sc : more :: [Map Name Prop]
more ->
             do Prop
ty <- TVarSource -> Kind -> InferM Prop
newType TVarSource
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
$ \s :: 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 this :: FilePath
this new :: 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 "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 "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 "type"

     case Maybe FilePath
shadowed of
       Nothing -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       Just that :: FilePath
that ->
          Error -> InferM ()
recordError (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$ Doc -> Error
ErrorMsg (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$
             FilePath -> Doc
text "Type" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
this Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
new) Doc -> Doc -> Doc
<+>
             FilePath -> Doc
text "shadows an existing" Doc -> Doc -> Doc
<+>
             FilePath -> Doc
text FilePath
that Doc -> Doc -> Doc
<+> FilePath -> Doc
text "with the same name."



-- | 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 p :: TParam
p (IM m :: ReaderT RO (StateT RW IO) a
m) =
  do case TParam -> Maybe Name
tpName TParam
p of
       Just x :: Name
x  -> FilePath -> Name -> InferM ()
checkTShadowing "variable" Name
x
       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 (\r :: 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 ps :: [TParam]
ps m :: 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 t :: TySyn
t (IM m :: ReaderT RO (StateT RW IO) a
m) =
  do let x :: Name
x = TySyn -> Name
tsName TySyn
t
     FilePath -> Name -> InferM ()
checkTShadowing "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 (\r :: 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 t :: Newtype
t (IM m :: 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
        (\r :: 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 t :: AbstractType
t (IM m :: 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
      (\r :: 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 a :: ModTParam
a (IM m :: 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
        (\r :: 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 x :: Name
x s :: VarType
s (IM m :: 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 (\r :: 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 xs :: [(Name, VarType)]
xs m :: 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 x :: Name
x s :: 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 xs :: [ModVParam]
xs (IM m :: 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 (\r :: 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 x :: 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 ps :: [Located Prop]
ps (IM m :: 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 (\r :: 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 (x :: Name
x,lt :: 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 xs :: Map Name (Located Prop)
xs m :: 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 (ts :: [TySyn]
ts,vs :: Map Name Schema
vs) m :: 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 (x :: Name
x,t :: 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 m :: 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
$ \s :: 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
$ \s :: 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 f :: a -> b
f (KM m :: 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 x :: 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 m :: ReaderT KRO (StateT KRW InferM) a
m >>= :: KindM a -> (a -> KindM b) -> KindM b
>>= k :: 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 MonadFail KindM where
  fail :: FilePath -> KindM a
fail x :: 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 wildOK :: AllowWildCards
wildOK vs :: [(Name, Maybe Kind, TParam)]
vs (KM m :: ReaderT KRO (StateT KRW InferM) a
m) =
  do (a :: a
a,kw :: 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) | (x :: Name
x,_,t :: 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) | (x :: Name
x,Just k :: Kind
k,_) <- [(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 x :: 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 t :: 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
       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 e :: 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 w :: 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 m :: 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 :: TVarSource -> Kind -> KindM Type
kNewType :: TVarSource -> Kind -> KindM Prop
kNewType src :: TVarSource
src k :: 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` TVarSource -> Set TParam -> Kind -> InferM TVar
newTVar' TVarSource
src Set TParam
tps Kind
k

-- | Lookup the definition of a type synonym.
kLookupTSyn :: Name -> KindM (Maybe TySyn)
kLookupTSyn :: Name -> KindM (Maybe TySyn)
kLookupTSyn x :: 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 x :: 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 x :: 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 x :: 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 x :: Name
x k :: 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 t :: Prop
t as :: [(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 v :: Name
v k :: 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
$ \s :: 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 r :: Range
r (KM m :: 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
a,s1 :: 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 _ [] = () -> KindM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
kNewGoals c :: ConstraintSource
c ps :: [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
$ \s :: 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 m :: 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