{-# 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)
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
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
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
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
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
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
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
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
(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)