{-# LANGUAGE
    ConstraintKinds
  , DeriveGeneric
  , FlexibleContexts
  #-}

module LText.Type where

import Application.Types (Env (..))
import LText.Expr (Expr (..))
import LText.Document (fetchDocument)

import           Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HM
import           Data.HashSet        (HashSet)
import qualified Data.HashSet        as HS
import Data.Maybe (fromMaybe)
import Text.PrettyPrint (text, (<+>), parens, render)
import Control.Monad (foldM)
import Control.Monad.State (StateT, MonadState, modify', get, put, evalStateT)
import Control.Monad.Reader (ReaderT (runReaderT), MonadReader, ask)
import Control.Monad.Catch (Exception, MonadThrow, throwM)
import Control.Monad.IO.Class (MonadIO, liftIO)

import System.Directory (doesFileExist)
import System.IO (hPutStrLn, stderr)
import System.Exit (exitFailure)
import GHC.Generics (Generic)



-- * Type Grammar

-- | We're working in an implicitly quantified prenex-polymorphic type
--   system, so trivial type expressions are also type schemes.
data Type
  = Text
  | TVar String
  | TArrow Type Type
  deriving (Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, Type -> Type -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq)

ppType :: Type -> String
ppType :: Type -> String
ppType = Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Doc
go
  where
    go :: Type -> Doc
go Type
t =
      case Type
t of
        Type
Text   -> String -> Doc
text String
"Text"
        TVar String
n -> String -> Doc
text String
n
        TArrow Type
t1 Type
t2 ->
          let t1Hat :: Doc
t1Hat = case Type
t1 of
                TArrow Type
_ Type
_ -> Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ Type -> Doc
go Type
t1
                Type
_          -> Type -> Doc
go Type
t1
          in  Doc
t1Hat Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> Type -> Doc
go Type
t2



-- * Kit Effects

data TypeError
  = CantUnify
      { TypeError -> Type
expectedType :: Type
      , TypeError -> Type
givenType    :: Type
      }
  | UnboundVariable String
  | OccursCheckFailure String Type
  deriving (Int -> TypeError -> ShowS
[TypeError] -> ShowS
TypeError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeError] -> ShowS
$cshowList :: [TypeError] -> ShowS
show :: TypeError -> String
$cshow :: TypeError -> String
showsPrec :: Int -> TypeError -> ShowS
$cshowsPrec :: Int -> TypeError -> ShowS
Show, TypeError -> TypeError -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeError -> TypeError -> Bool
$c/= :: TypeError -> TypeError -> Bool
== :: TypeError -> TypeError -> Bool
$c== :: TypeError -> TypeError -> Bool
Eq, forall x. Rep TypeError x -> TypeError
forall x. TypeError -> Rep TypeError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypeError x -> TypeError
$cfrom :: forall x. TypeError -> Rep TypeError x
Generic)

instance Exception TypeError

handleTypeError :: TypeError -> IO a
handleTypeError :: forall a. TypeError -> IO a
handleTypeError TypeError
e = do
  Handle -> String -> IO ()
hPutStrLn Handle
stderr forall a b. (a -> b) -> a -> b
$
    case TypeError
e of
      CantUnify Type
t1 Type
t2 ->
        String
"[Type Error] Can't unify type " forall a. [a] -> [a] -> [a]
++ Type -> String
ppType Type
t1 forall a. [a] -> [a] -> [a]
++ String
" with " forall a. [a] -> [a] -> [a]
++ Type -> String
ppType Type
t2
      UnboundVariable String
n ->
        String
"[Type Error] Unbound variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
n
      OccursCheckFailure String
n Type
t ->
        String
"[Type Error] Occurs check failure: type variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
n forall a. [a] -> [a] -> [a]
++ String
" in "
        forall a. [a] -> [a] -> [a]
++ Type -> String
ppType Type
t forall a. [a] -> [a] -> [a]
++ String
". Note: recursion is forbidden"
  forall a. IO a
exitFailure



data TypeEnv = TypeEnv
  { TypeEnv -> HashSet String
plaintextFiles :: HashSet FilePath
  } deriving (Int -> TypeEnv -> ShowS
[TypeEnv] -> ShowS
TypeEnv -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeEnv] -> ShowS
$cshowList :: [TypeEnv] -> ShowS
show :: TypeEnv -> String
$cshow :: TypeEnv -> String
showsPrec :: Int -> TypeEnv -> ShowS
$cshowsPrec :: Int -> TypeEnv -> ShowS
Show, TypeEnv -> TypeEnv -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeEnv -> TypeEnv -> Bool
$c/= :: TypeEnv -> TypeEnv -> Bool
== :: TypeEnv -> TypeEnv -> Bool
$c== :: TypeEnv -> TypeEnv -> Bool
Eq)

toTypeEnv :: Env -> TypeEnv
toTypeEnv :: Env -> TypeEnv
toTypeEnv (Env Expr
_ Bool
_ HashSet String
r Maybe (String, String)
_) = HashSet String -> TypeEnv
TypeEnv HashSet String
r

emptyTypeEnv :: TypeEnv
emptyTypeEnv :: TypeEnv
emptyTypeEnv = HashSet String -> TypeEnv
TypeEnv forall a. HashSet a
HS.empty


type MonadTypecheck m =
  ( MonadState Context m
  , MonadReader TypeEnv m
  , MonadThrow m
  , MonadIO m
  )

type TypeCheckM = StateT Context (ReaderT TypeEnv IO)

runTypeCheckM :: TypeEnv -> TypeCheckM a -> IO a
runTypeCheckM :: forall a. TypeEnv -> TypeCheckM a -> IO a
runTypeCheckM TypeEnv
te TypeCheckM a
x =
  forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT TypeCheckM a
x Context
initContext) TypeEnv
te


-- * TypeChecking

newtype Subst = Subst
  { Subst -> HashMap String Type
getSubst :: HashMap String Type
  } deriving (Int -> Subst -> ShowS
[Subst] -> ShowS
Subst -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Subst] -> ShowS
$cshowList :: [Subst] -> ShowS
show :: Subst -> String
$cshow :: Subst -> String
showsPrec :: Int -> Subst -> ShowS
$cshowsPrec :: Int -> Subst -> ShowS
Show, Subst -> Subst -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c== :: Subst -> Subst -> Bool
Eq)

instance Semigroup Subst where
  (Subst HashMap String Type
f) <> :: Subst -> Subst -> Subst
<> (Subst HashMap String Type
g) = HashMap String Type -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. IsType t => Subst -> t -> t
applySubst (HashMap String Type -> Subst
Subst HashMap String Type
f)) HashMap String Type
g forall a. Semigroup a => a -> a -> a
<> HashMap String Type
f

instance Monoid Subst where
  mempty :: Subst
mempty  = HashMap String Type -> Subst
Subst forall a. Monoid a => a
mempty
  mappend :: Subst -> Subst -> Subst
mappend = forall a. Semigroup a => a -> a -> a
(<>)


class IsType t where
  freeTVars  :: t -> HashSet String
  applySubst :: Subst -> t -> t

instance IsType a => IsType [a] where
  freeTVars :: [a] -> HashSet String
freeTVars    = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall t. IsType t => t -> HashSet String
freeTVars
  applySubst :: Subst -> [a] -> [a]
applySubst Subst
s = forall a b. (a -> b) -> [a] -> [b]
map (forall t. IsType t => Subst -> t -> t
applySubst Subst
s)

instance IsType Type where
  freeTVars :: Type -> HashSet String
freeTVars Type
t =
    case Type
t of
      Type
Text         -> forall a. HashSet a
HS.empty
      TVar String
n       -> forall a. Hashable a => a -> HashSet a
HS.singleton String
n
      TArrow Type
t1 Type
t2 -> forall t. IsType t => t -> HashSet String
freeTVars Type
t1 forall a. Semigroup a => a -> a -> a
<> forall t. IsType t => t -> HashSet String
freeTVars Type
t2
  applySubst :: Subst -> Type -> Type
applySubst Subst
s Type
t =
    case Type
t of
      Type
Text         -> Type
Text
      TVar String
n       -> forall a. a -> Maybe a -> a
fromMaybe (String -> Type
TVar String
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup String
n forall a b. (a -> b) -> a -> b
$ Subst -> HashMap String Type
getSubst Subst
s
      TArrow Type
t1 Type
t2 -> Type -> Type -> Type
TArrow (forall t. IsType t => Subst -> t -> t
applySubst Subst
s Type
t1) (forall t. IsType t => Subst -> t -> t
applySubst Subst
s Type
t2)

data Scheme = Scheme
  { Scheme -> HashSet String
schemeQuant :: HashSet String
  , Scheme -> Type
schemeType  :: Type
  } deriving (Int -> Scheme -> ShowS
[Scheme] -> ShowS
Scheme -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Scheme] -> ShowS
$cshowList :: [Scheme] -> ShowS
show :: Scheme -> String
$cshow :: Scheme -> String
showsPrec :: Int -> Scheme -> ShowS
$cshowsPrec :: Int -> Scheme -> ShowS
Show, Scheme -> Scheme -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Scheme -> Scheme -> Bool
$c/= :: Scheme -> Scheme -> Bool
== :: Scheme -> Scheme -> Bool
$c== :: Scheme -> Scheme -> Bool
Eq)

instance IsType Scheme where
  freeTVars :: Scheme -> HashSet String
freeTVars (Scheme HashSet String
qs Type
t) =
    forall t. IsType t => t -> HashSet String
freeTVars Type
t forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HS.difference` HashSet String
qs
  applySubst :: Subst -> Scheme -> Scheme
applySubst (Subst HashMap String Type
s) (Scheme HashSet String
qs Type
t) =
    HashSet String -> Type -> Scheme
Scheme HashSet String
qs forall a b. (a -> b) -> a -> b
$ forall t. IsType t => Subst -> t -> t
applySubst (HashMap String Type -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HM.delete HashMap String Type
s HashSet String
qs) Type
t



freshTVar :: MonadTypecheck m => m Type
freshTVar :: forall (m :: * -> *). MonadTypecheck m => m Type
freshTVar = forall (m :: * -> *). MonadTypecheck m => String -> m Type
somewhatFreshTVar String
"a"


somewhatFreshTVar :: MonadTypecheck m => String -> m Type
somewhatFreshTVar :: forall (m :: * -> *). MonadTypecheck m => String -> m Type
somewhatFreshTVar String
s = do
  (Context HashMap String Scheme
cs Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap String Scheme -> Int -> Context
Context HashMap String Scheme
cs forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
1
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Type
TVar forall a b. (a -> b) -> a -> b
$ String
s forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i


mostGeneralUnifier :: MonadTypecheck m => Type -> Type -> m Subst
mostGeneralUnifier :: forall (m :: * -> *). MonadTypecheck m => Type -> Type -> m Subst
mostGeneralUnifier (TArrow Type
tl1 Type
tl2) (TArrow Type
tr1 Type
tr2) = do
  Subst
s1 <- forall (m :: * -> *). MonadTypecheck m => Type -> Type -> m Subst
mostGeneralUnifier Type
tl1 Type
tr1
  Subst
s2 <- forall (m :: * -> *). MonadTypecheck m => Type -> Type -> m Subst
mostGeneralUnifier (forall t. IsType t => Subst -> t -> t
applySubst Subst
s1 Type
tl2) (forall t. IsType t => Subst -> t -> t
applySubst Subst
s1 Type
tr2)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Subst
s1 forall a. Semigroup a => a -> a -> a
<> Subst
s2
mostGeneralUnifier (TVar String
n) Type
t = forall (m :: * -> *). MonadTypecheck m => String -> Type -> m Subst
varBind String
n Type
t
mostGeneralUnifier Type
t (TVar String
n) = forall (m :: * -> *). MonadTypecheck m => String -> Type -> m Subst
varBind String
n Type
t
mostGeneralUnifier Type
Text Type
Text  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
mostGeneralUnifier Type
t1 Type
t2      = forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
CantUnify Type
t1 Type
t2

-- | Substitute n for t, given there's no collision
varBind :: MonadTypecheck m => String -> Type -> m Subst
varBind :: forall (m :: * -> *). MonadTypecheck m => String -> Type -> m Subst
varBind String
n Type
t
  | Type
t forall a. Eq a => a -> a -> Bool
== String -> Type
TVar String
n               = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
  | String
n forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HS.member` forall t. IsType t => t -> HashSet String
freeTVars Type
t = forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM forall a b. (a -> b) -> a -> b
$ String -> Type -> TypeError
OccursCheckFailure String
n Type
t
  | Bool
otherwise                 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ HashMap String Type -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall k v. Hashable k => k -> v -> HashMap k v
HM.singleton String
n Type
t


data Context = Context
  { Context -> HashMap String Scheme
contextMap   :: HashMap String Scheme
  , Context -> Int
contextFresh :: Int
  } deriving (Int -> Context -> ShowS
[Context] -> ShowS
Context -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Context] -> ShowS
$cshowList :: [Context] -> ShowS
show :: Context -> String
$cshow :: Context -> String
showsPrec :: Int -> Context -> ShowS
$cshowsPrec :: Int -> Context -> ShowS
Show, Context -> Context -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Context -> Context -> Bool
$c/= :: Context -> Context -> Bool
== :: Context -> Context -> Bool
$c== :: Context -> Context -> Bool
Eq)

initContext :: Context
initContext :: Context
initContext = Context
  { contextMap :: HashMap String Scheme
contextMap   = forall k v. HashMap k v
HM.empty
  , contextFresh :: Int
contextFresh = Int
0
  }


removeTVar :: String -> Context -> Context
removeTVar :: String -> Context -> Context
removeTVar String
n (Context HashMap String Scheme
cs Int
f) = HashMap String Scheme -> Int -> Context
Context (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HM.delete String
n HashMap String Scheme
cs) Int
f

instance IsType Context where
  freeTVars :: Context -> HashSet String
freeTVars (Context HashMap String Scheme
cs Int
_)    = forall t. IsType t => t -> HashSet String
freeTVars forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [v]
HM.elems HashMap String Scheme
cs
  applySubst :: Subst -> Context -> Context
applySubst Subst
s (Context HashMap String Scheme
cs Int
f) = HashMap String Scheme -> Int -> Context
Context (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. IsType t => Subst -> t -> t
applySubst Subst
s) HashMap String Scheme
cs) Int
f

-- | Where we don't want to include variables bound by our context
quantify :: MonadTypecheck m => Type -> m Scheme
quantify :: forall (m :: * -> *). MonadTypecheck m => Type -> m Scheme
quantify Type
t = do
  Context
c <- forall s (m :: * -> *). MonadState s m => m s
get
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ HashSet String -> Type -> Scheme
Scheme (forall t. IsType t => t -> HashSet String
freeTVars Type
t forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HS.difference` forall t. IsType t => t -> HashSet String
freeTVars Context
c) Type
t

-- | Replaces bound variables with fresh ones
unQuantify :: MonadTypecheck m => Scheme -> m Type
unQuantify :: forall (m :: * -> *). MonadTypecheck m => Scheme -> m Type
unQuantify (Scheme HashSet String
qs Type
t) = do
  Subst
s <- HashMap String Type -> Subst
Subst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\HashMap String Type
s String
q -> do Type
n <- forall (m :: * -> *). MonadTypecheck m => m Type
freshTVar
                                   forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert String
q Type
n HashMap String Type
s) forall k v. HashMap k v
HM.empty HashSet String
qs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall t. IsType t => Subst -> t -> t
applySubst Subst
s Type
t


-- ** Actual Typechecking

typeOfTopLevel :: MonadTypecheck m => Expr -> m Type
typeOfTopLevel :: forall (m :: * -> *). MonadTypecheck m => Expr -> m Type
typeOfTopLevel Expr
e = do
  (Subst
s,Type
t) <- forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
TopLevel Expr
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall t. IsType t => Subst -> t -> t
applySubst Subst
s Type
t


data ExprType = TopLevel | DocLevel


-- TODO: Add a flag for free variable checking or not checking for documents
typeInfer :: MonadTypecheck m => ExprType -> Expr -> m (Subst, Type)
typeInfer :: forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
mode' Expr
e =
  case Expr
e of
    Lit [Text]
_ String
_ Bool
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, Type
Text)
    Concat Expr
e1 Expr
e2 String
_ Bool
_ -> do
      -- FIXME: Probably wasteful :\
      (Subst
s1,Type
t1) <- forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
mode' Expr
e1
      (Subst
s2,Type
t2) <- forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
mode' Expr
e2
      Subst
s3 <- forall (m :: * -> *). MonadTypecheck m => Type -> Type -> m Subst
mostGeneralUnifier Type
t1 Type
t2
      Subst
s4 <- forall (m :: * -> *). MonadTypecheck m => Type -> Type -> m Subst
mostGeneralUnifier (forall t. IsType t => Subst -> t -> t
applySubst Subst
s3 Type
t1) Type
Text
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s4 forall a. Semigroup a => a -> a -> a
<> Subst
s3 forall a. Semigroup a => a -> a -> a
<> Subst
s2 forall a. Semigroup a => a -> a -> a
<> Subst
s1, Type
Text)
    Var String
x -> do
      HashMap String Scheme
ctx <- Context -> HashMap String Scheme
contextMap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
      case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup String
x HashMap String Scheme
ctx of
        Maybe Scheme
Nothing ->
          case ExprType
mode' of
            ExprType
TopLevel -> do
              Bool
exists <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
x
              if Bool
exists
              then do
                Bool
isRaw <- (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member String
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeEnv -> HashSet String
plaintextFiles) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask
                if Bool
isRaw
                then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, Type
Text)
                else do
                  Expr
d <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO Expr
fetchDocument String
x
                  forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
DocLevel Expr
d
              else forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM forall a b. (a -> b) -> a -> b
$ String -> TypeError
UnboundVariable String
x
            ExprType
DocLevel -> forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM forall a b. (a -> b) -> a -> b
$ String -> TypeError
UnboundVariable String
x
        Just Scheme
s -> do
          Type
t <- forall (m :: * -> *). MonadTypecheck m => Scheme -> m Type
unQuantify Scheme
s
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, Type
t)
    Abs String
n Expr
e' -> do
      Type
t <- forall (m :: * -> *). MonadTypecheck m => m Type
freshTVar
      (Context HashMap String Scheme
cs Int
f) <- forall s (m :: * -> *). MonadState s m => m s
get
      let ctx :: Context
ctx = HashMap String Scheme -> Int -> Context
Context (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert String
n (HashSet String -> Type -> Scheme
Scheme forall a. HashSet a
HS.empty Type
t) forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HM.delete String
n HashMap String Scheme
cs) Int
f
      forall s (m :: * -> *). MonadState s m => s -> m ()
put Context
ctx
      (Subst
s',Type
t') <- forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
mode' Expr
e'
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s', Type -> Type -> Type
TArrow (forall t. IsType t => Subst -> t -> t
applySubst Subst
s' Type
t) Type
t')
    App Expr
e1 Expr
e2 -> do
      Type
t <- forall (m :: * -> *). MonadTypecheck m => m Type
freshTVar
      (Subst
s1,Type
t1) <- forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
mode' Expr
e1
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (forall t. IsType t => Subst -> t -> t
applySubst Subst
s1)
      (Subst
s2,Type
t2) <- forall (m :: * -> *).
MonadTypecheck m =>
ExprType -> Expr -> m (Subst, Type)
typeInfer ExprType
mode' Expr
e2
      Subst
s3 <- forall (m :: * -> *). MonadTypecheck m => Type -> Type -> m Subst
mostGeneralUnifier (forall t. IsType t => Subst -> t -> t
applySubst Subst
s2 Type
t1) (Type -> Type -> Type
TArrow Type
t2 Type
t)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s3 forall a. Semigroup a => a -> a -> a
<> Subst
s2 forall a. Semigroup a => a -> a -> a
<> Subst
s1, forall t. IsType t => Subst -> t -> t
applySubst Subst
s3 Type
t)