module Language.PureScript.TypeChecker.Types (
typesOf
) where
import Prelude ()
import Prelude.Compat
import Data.Either (lefts, rights)
import Data.List (transpose, nub, (\\), partition, delete)
import Data.Maybe (fromMaybe)
import qualified Data.Map as M
import Control.Monad
import Control.Monad.State.Class (MonadState(..), gets)
import Control.Monad.Supply.Class (MonadSupply)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.Writer.Class (MonadWriter(..))
import Language.PureScript.Crash
import Language.PureScript.AST
import Language.PureScript.Environment
import Language.PureScript.Errors
import Language.PureScript.Kinds
import Language.PureScript.Names
import Language.PureScript.Traversals
import Language.PureScript.TypeChecker.Entailment
import Language.PureScript.TypeChecker.Kinds
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Rows
import Language.PureScript.TypeChecker.Skolems
import Language.PureScript.TypeChecker.Subsumption
import Language.PureScript.TypeChecker.Synonyms
import Language.PureScript.TypeChecker.Unify
import Language.PureScript.TypeClassDictionaries
import Language.PureScript.Types
typesOf ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
ModuleName ->
[(Ident, Expr)] ->
m [(Ident, (Expr, Type))]
typesOf moduleName vals = do
tys <- fmap tidyUp . liftUnifyWarnings replace $ do
(untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals
ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
ds2 <- forM untyped $ \e -> typeForBindingGroupElement True e dict untypedDict
return $ ds1 ++ ds2
forM tys $ \(ident, (val, ty)) -> do
val' <- replaceTypeClassDictionaries moduleName val
skolemEscapeCheck val'
checkDuplicateLabels val'
return (ident, (val', varIfUnknown ty))
where
tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (substituteType sub) val, substituteType sub ty))) ts
replace sub (ErrorMessage hints (WildcardInferredType ty)) = ErrorMessage hints . WildcardInferredType $ substituteType sub ty
replace sub (ErrorMessage hints (MissingTypeDeclaration name ty)) = ErrorMessage hints $ MissingTypeDeclaration name (varIfUnknown (substituteType sub ty))
replace _ em = em
type TypeData = M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility)
type UntypedData = [(Ident, Type)]
typeDictionaryForBindingGroup ::
(Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
ModuleName ->
[(Ident, Expr)] ->
m ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)
typeDictionaryForBindingGroup moduleName vals = do
let
es = map isTyped vals
untyped = lefts es
typed = rights es
typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed
untypedNames <- replicateM (length untyped) freshType
let
untypedDict = zip (map fst untyped) untypedNames
dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, Private, Undefined))) $ typedDict ++ untypedDict)
return (untyped, typed, dict, untypedDict)
checkTypedBindingGroupElement ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
ModuleName ->
(Ident, (Expr, Type, Bool)) ->
TypeData ->
m (Ident, (Expr, Type))
checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
ty' <- replaceTypeWildcards ty
(kind, args) <- kindOfWithScopedVars ty
checkTypeKind ty kind
ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'
val'' <- if checkType
then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''
else return (TypedValue False val' ty'')
return (ident, (val'', ty''))
typeForBindingGroupElement ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Bool ->
(Ident, Expr) ->
TypeData ->
UntypedData ->
m (Ident, (Expr, Type))
typeForBindingGroupElement warn (ident, val) dict untypedDict = do
TypedValue _ val' ty <- bindNames dict $ infer val
unifyTypes ty $ fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)
when warn . tell . errorMessage $ MissingTypeDeclaration ident ty
return (ident, (TypedValue True val' ty, ty))
isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
isTyped (name, value) = Left (name, value)
overTypes :: (Type -> Type) -> Expr -> Expr
overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
where
g :: Expr -> Expr
g (TypedValue checkTy val t) = TypedValue checkTy val (f t)
g (TypeClassDictionary (nm, tys) sco) = TypeClassDictionary (nm, map f tys) sco
g other = other
replaceTypeClassDictionaries ::
(Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
ModuleName ->
Expr ->
m Expr
replaceTypeClassDictionaries mn =
let (_, f, _) = everywhereOnValuesTopDownM return go return
in f
where
go (TypeClassDictionary constraint dicts) = entails mn dicts constraint
go other = return other
checkTypeKind ::
(Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>
Type ->
Kind ->
m ()
checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind == Star
instantiatePolyTypeWithUnknowns ::
(Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>
Expr ->
Type ->
m (Expr, Type)
instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
ty' <- replaceVarWithUnknown ident ty
instantiatePolyTypeWithUnknowns val ty'
instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do
dicts <- getTypeClassDictionaries
instantiatePolyTypeWithUnknowns (foldl App val (map (flip TypeClassDictionary dicts) constraints)) ty
instantiatePolyTypeWithUnknowns val ty = return (val, ty)
infer ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr ->
m Expr
infer val = rethrow (addHint (ErrorInferringType val)) $ infer' val
infer' ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr ->
m Expr
infer' v@(NumericLiteral (Left _)) = return $ TypedValue True v tyInt
infer' v@(NumericLiteral (Right _)) = return $ TypedValue True v tyNumber
infer' v@(StringLiteral _) = return $ TypedValue True v tyString
infer' v@(CharLiteral _) = return $ TypedValue True v tyChar
infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean
infer' (ArrayLiteral vals) = do
ts <- traverse infer vals
els <- freshType
forM_ ts $ \(TypedValue _ _ t) -> unifyTypes els t
return $ TypedValue True (ArrayLiteral ts) (TypeApp tyArray els)
infer' (ObjectLiteral ps) = do
ensureNoDuplicateProperties ps
ts <- traverse (infer . snd) ps
let fields = zipWith (\name (TypedValue _ _ t) -> (name, t)) (map fst ps) ts
ty = TypeApp tyObject $ rowFromList (fields, REmpty)
return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty
infer' (ObjectUpdate o ps) = do
ensureNoDuplicateProperties ps
row <- freshType
newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> traverse (infer . snd) ps
let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
oldTys <- zip (map fst ps) <$> replicateM (length ps) freshType
let oldTy = TypeApp tyObject $ rowFromList (oldTys, row)
o' <- TypedValue True <$> check o oldTy <*> pure oldTy
return $ TypedValue True (ObjectUpdate o' newVals) $ TypeApp tyObject $ rowFromList (newTys, row)
infer' (Accessor prop val) = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do
field <- freshType
rest <- freshType
typed <- check val (TypeApp tyObject (RCons prop field rest))
return $ TypedValue True (Accessor prop typed) field
infer' (Abs (Left arg) ret) = do
ty <- freshType
Just moduleName <- checkCurrentModule <$> get
withBindingGroupVisible $ bindLocalVariables moduleName [(arg, ty, Defined)] $ do
body@(TypedValue _ _ bodyTy) <- infer' ret
return $ TypedValue True (Abs (Left arg) body) $ function ty bodyTy
infer' (Abs (Right _) _) = internalError "Binder was not desugared"
infer' (App f arg) = do
f'@(TypedValue _ _ ft) <- infer f
(ret, app) <- checkFunctionApplication f' ft arg Nothing
return $ TypedValue True app ret
infer' (Var var) = do
Just moduleName <- checkCurrentModule <$> get
checkVisibility moduleName var
ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards <=< lookupVariable moduleName $ var
case ty of
ConstrainedType constraints ty' -> do
dicts <- getTypeClassDictionaries
return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) constraints)) ty'
_ -> return $ TypedValue True (Var var) ty
infer' v@(Constructor c) = do
env <- getEnv
case M.lookup c (dataConstructors env) of
Nothing -> throwError . errorMessage $ UnknownDataConstructor c Nothing
Just (_, _, ty, _) -> do (v', ty') <- sndM (introduceSkolemScope <=< replaceAllTypeSynonyms) <=< instantiatePolyTypeWithUnknowns v $ ty
return $ TypedValue True v' ty'
infer' (Case vals binders) = do
(vals', ts) <- instantiateForBinders vals binders
ret <- freshType
binders' <- checkBinders ts ret binders
return $ TypedValue True (Case vals' binders') ret
infer' (IfThenElse cond th el) = do
cond' <- check cond tyBoolean
v2@(TypedValue _ _ t2) <- infer th
v3@(TypedValue _ _ t3) <- infer el
(v2', v3', t) <- meet v2 v3 t2 t3
return $ TypedValue True (IfThenElse cond' v2' v3') t
infer' (Let ds val) = do
(ds', val'@(TypedValue _ _ valTy)) <- inferLetBinding [] ds val infer
return $ TypedValue True (Let ds' val') valTy
infer' (SuperClassDictionary className tys) = do
dicts <- getTypeClassDictionaries
return $ TypeClassDictionary (className, tys) dicts
infer' (TypedValue checkType val ty) = do
Just moduleName <- checkCurrentModule <$> get
(kind, args) <- kindOfWithScopedVars ty
checkTypeKind ty kind
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val
return $ TypedValue True val' ty'
infer' (PositionedValue pos c val) = warnAndRethrowWithPosition pos $ do
TypedValue t v ty <- infer' val
return $ TypedValue t (PositionedValue pos c v) ty
infer' _ = internalError "Invalid argument to infer"
inferLetBinding ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Declaration] ->
[Declaration] ->
Expr ->
(Expr -> m Expr) ->
m ([Declaration], Expr)
inferLetBinding seen [] ret j = (,) seen <$> withBindingGroupVisible (j ret)
inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
Just moduleName <- checkCurrentModule <$> get
(kind, args) <- kindOfWithScopedVars ty
checkTypeKind ty kind
let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv
bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j
inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do
valTy <- freshType
Just moduleName <- checkCurrentModule <$> get
let dict = M.singleton (moduleName, ident) (valTy, nameKind, Undefined)
TypedValue _ val' valTy' <- bindNames dict $ infer val
unifyTypes valTy valTy'
bindNames (M.singleton (moduleName, ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j
inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
Just moduleName <- checkCurrentModule <$> get
(untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName (map (\(i, _, v) -> (i, v)) ds)
ds1' <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
ds2' <- forM untyped $ \e -> typeForBindingGroupElement False e dict untypedDict
let ds' = [(ident, Private, val') | (ident, (val', _)) <- ds1' ++ ds2']
bindNames dict $ do
makeBindingGroupVisible
inferLetBinding (seen ++ [BindingGroupDeclaration ds']) rest ret j
inferLetBinding seen (PositionedDeclaration pos com d : ds) ret j = warnAndRethrowWithPosition pos $ do
(d' : ds', val') <- inferLetBinding seen (d : ds) ret j
return (PositionedDeclaration pos com d' : ds', val')
inferLetBinding _ _ _ _ = internalError "Invalid argument to inferLetBinding"
inferBinder :: forall m.
(Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Type ->
Binder ->
m (M.Map Ident Type)
inferBinder _ NullBinder = return M.empty
inferBinder val (StringBinder _) = unifyTypes val tyString >> return M.empty
inferBinder val (CharBinder _) = unifyTypes val tyChar >> return M.empty
inferBinder val (NumberBinder (Left _)) = unifyTypes val tyInt >> return M.empty
inferBinder val (NumberBinder (Right _)) = unifyTypes val tyNumber >> return M.empty
inferBinder val (BooleanBinder _) = unifyTypes val tyBoolean >> return M.empty
inferBinder val (VarBinder name) = return $ M.singleton name val
inferBinder val (ConstructorBinder ctor binders) = do
env <- getEnv
case M.lookup ctor (dataConstructors env) of
Just (_, _, ty, _) -> do
(_, fn) <- instantiatePolyTypeWithUnknowns (internalError "Data constructor types cannot contain constraints") ty
fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn
let (args, ret) = peelArgs fn'
unless (length args == length binders) . throwError . errorMessage $ IncorrectConstructorArity ctor
unifyTypes ret val
M.unions <$> zipWithM inferBinder (reverse args) binders
_ -> throwError . errorMessage $ UnknownDataConstructor ctor Nothing
where
peelArgs :: Type -> ([Type], Type)
peelArgs = go []
where
go args (TypeApp (TypeApp fn arg) ret) | fn == tyFunction = go (arg : args) ret
go args ret = (args, ret)
inferBinder val (ObjectBinder props) = do
row <- freshType
rest <- freshType
m1 <- inferRowProperties row rest props
unifyTypes val (TypeApp tyObject row)
return m1
where
inferRowProperties :: Type -> Type -> [(String, Binder)] -> m (M.Map Ident Type)
inferRowProperties nrow row [] = unifyTypes nrow row >> return M.empty
inferRowProperties nrow row ((name, binder):binders) = do
propTy <- freshType
m1 <- inferBinder propTy binder
m2 <- inferRowProperties nrow (RCons name propTy row) binders
return $ m1 `M.union` m2
inferBinder val (ArrayBinder binders) = do
el <- freshType
m1 <- M.unions <$> traverse (inferBinder el) binders
unifyTypes val (TypeApp tyArray el)
return m1
inferBinder val (NamedBinder name binder) = do
m <- inferBinder val binder
return $ M.insert name val m
inferBinder val (PositionedBinder pos _ binder) =
warnAndRethrowWithPosition pos $ inferBinder val binder
inferBinder val (TypedBinder ty binder) = do
kind <- kindOf ty
checkTypeKind ty kind
ty1 <- replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
unifyTypes val ty1
inferBinder val binder
inferBinder _ OpBinder{} =
internalError "OpBinder should have been desugared before inferBinder"
inferBinder _ BinaryNoParensBinder{} =
internalError "BinaryNoParensBinder should have been desugared before inferBinder"
inferBinder _ ParensInBinder{} =
internalError "ParensInBinder should have been desugared before inferBinder"
binderRequiresMonotype :: Binder -> Bool
binderRequiresMonotype NullBinder = False
binderRequiresMonotype (VarBinder _) = False
binderRequiresMonotype (NamedBinder _ b) = binderRequiresMonotype b
binderRequiresMonotype (PositionedBinder _ _ b) = binderRequiresMonotype b
binderRequiresMonotype _ = True
instantiateForBinders ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Expr] ->
[CaseAlternative] ->
m ([Expr], [Type])
instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do
TypedValue _ val' ty <- infer val
if inst
then instantiatePolyTypeWithUnknowns val' ty
else return (val', ty)) vals shouldInstantiate
where
shouldInstantiate :: [Bool]
shouldInstantiate = map (any binderRequiresMonotype) . transpose . map caseAlternativeBinders $ cas
checkBinders ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Type] ->
Type ->
[CaseAlternative] ->
m [CaseAlternative]
checkBinders _ _ [] = return []
checkBinders nvals ret (CaseAlternative binders result : bs) = do
guardWith (errorMessage $ OverlappingArgNames Nothing) $
let ns = concatMap binderNames binders in length (nub ns) == length ns
Just moduleName <- checkCurrentModule <$> get
m1 <- M.unions <$> zipWithM inferBinder nvals binders
r <- bindLocalVariables moduleName [ (name, ty, Defined) | (name, ty) <- M.toList m1 ] $
CaseAlternative binders <$>
case result of
Left gs -> do
gs' <- forM gs $ \(grd, val) -> do
grd' <- rethrow (addHint ErrorCheckingGuard) $ check grd tyBoolean
val' <- TypedValue True <$> check val ret <*> pure ret
return (grd', val')
return $ Left gs'
Right val -> do
val' <- TypedValue True <$> check val ret <*> pure ret
return $ Right val'
rs <- checkBinders nvals ret bs
return $ r : rs
check ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr ->
Type ->
m Expr
check val ty = rethrow (addHint (ErrorCheckingType val ty)) $ check' val ty
check'
:: forall m
. (Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> Type
-> m Expr
check' val (ForAll ident ty _) = do
scope <- newSkolemScope
sko <- newSkolemConstant
let ss = case val of
PositionedValue pos _ _ -> Just pos
_ -> Nothing
sk = skolemize ident sko scope ss ty
skVal = skolemizeTypesInValue ident sko scope ss val
val' <- check skVal sk
return $ TypedValue True val' (ForAll ident ty (Just scope))
check' val t@(ConstrainedType constraints ty) = do
dictNames <- forM constraints $ \(Qualified _ (ProperName className), _) ->
freshIdent ("dict" ++ className)
dicts <- join <$> zipWithM (newDictionaries []) (map (Qualified Nothing) dictNames) constraints
val' <- withBindingGroupVisible $ withTypeClassDictionaries dicts $ check val ty
return $ TypedValue True (foldr (Abs . Left) val' dictNames) t
where
newDictionaries
:: [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified Ident
-> (Qualified (ProperName 'ClassName), [Type])
-> m [TypeClassDictionaryInScope]
newDictionaries path name (className, instanceTy) = do
tcs <- gets (typeClasses . checkEnv)
let (args, _, superclasses) = fromMaybe (internalError "newDictionaries: type class lookup failed") $ M.lookup className tcs
supDicts <- join <$> zipWithM (\(supName, supArgs) index ->
newDictionaries ((supName, index) : path)
name
(supName, instantiateSuperclass (map fst args) supArgs instanceTy)
) superclasses [0..]
return (TypeClassDictionaryInScope name path className instanceTy Nothing : supDicts)
instantiateSuperclass :: [String] -> [Type] -> [Type] -> [Type]
instantiateSuperclass args supArgs tys = map (replaceAllTypeVars (zip args tys)) supArgs
check' val u@(TUnknown _) = do
val'@(TypedValue _ _ ty) <- infer val
(val'', ty') <- instantiatePolyTypeWithUnknowns val' ty
unifyTypes ty' u
return $ TypedValue True val'' ty'
check' v@(NumericLiteral (Left _)) t | t == tyInt =
return $ TypedValue True v t
check' v@(NumericLiteral (Right _)) t | t == tyNumber =
return $ TypedValue True v t
check' v@(StringLiteral _) t | t == tyString =
return $ TypedValue True v t
check' v@(CharLiteral _) t | t == tyChar =
return $ TypedValue True v t
check' v@(BooleanLiteral _) t | t == tyBoolean =
return $ TypedValue True v t
check' (ArrayLiteral vals) t@(TypeApp a ty) = do
unifyTypes a tyArray
array <- ArrayLiteral <$> forM vals (`check` ty)
return $ TypedValue True array t
check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) = do
unifyTypes t tyFunction
Just moduleName <- checkCurrentModule <$> get
ret' <- withBindingGroupVisible $ bindLocalVariables moduleName [(arg, argTy, Defined)] $ check ret retTy
return $ TypedValue True (Abs (Left arg) ret') ty
check' (Abs (Right _) _) _ = internalError "Binder was not desugared"
check' (App f arg) ret = do
f'@(TypedValue _ _ ft) <- infer f
(_, app) <- checkFunctionApplication f' ft arg (Just ret)
return $ TypedValue True app ret
check' v@(Var var) ty = do
Just moduleName <- checkCurrentModule <$> get
checkVisibility moduleName var
repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
v' <- subsumes (Just v) repl ty'
case v' of
Nothing -> internalError "check: unable to check the subsumes relation."
Just v'' -> return $ TypedValue True v'' ty'
check' (SuperClassDictionary className tys) _ = do
dicts <- getTypeClassDictionaries
return $ TypeClassDictionary (className, tys) dicts
check' (TypedValue checkType val ty1) ty2 = do
Just moduleName <- checkCurrentModule <$> get
(kind, args) <- kindOfWithScopedVars ty1
checkTypeKind ty1 kind
ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1
ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2
val' <- subsumes (Just val) ty1' ty2'
case val' of
Nothing -> internalError "check: unable to check the subsumes relation."
Just _ -> do
val''' <- if checkType then withScopedTypeVars moduleName args (check val ty2') else return val
return $ TypedValue checkType val''' ty2'
check' (Case vals binders) ret = do
(vals', ts) <- instantiateForBinders vals binders
binders' <- checkBinders ts ret binders
return $ TypedValue True (Case vals' binders') ret
check' (IfThenElse cond th el) ty = do
cond' <- check cond tyBoolean
th' <- check th ty
el' <- check el ty
return $ TypedValue True (IfThenElse cond' th' el') ty
check' e@(ObjectLiteral ps) t@(TypeApp obj row) | obj == tyObject = do
ensureNoDuplicateProperties ps
ps' <- checkProperties e ps row False
return $ TypedValue True (ObjectLiteral ps') t
check' (TypeClassDictionaryConstructorApp name ps) t = do
ps' <- check' ps t
return $ TypedValue True (TypeClassDictionaryConstructorApp name ps') t
check' e@(ObjectUpdate obj ps) t@(TypeApp o row) | o == tyObject = do
ensureNoDuplicateProperties ps
let (propsToCheck, rest) = rowToList row
(removedProps, remainingProps) = partition (\(p, _) -> p `elem` map fst ps) propsToCheck
us <- zip (map fst removedProps) <$> replicateM (length ps) freshType
obj' <- check obj (TypeApp tyObject (rowFromList (us ++ remainingProps, rest)))
ps' <- checkProperties e ps row True
return $ TypedValue True (ObjectUpdate obj' ps') t
check' (Accessor prop val) ty = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do
rest <- freshType
val' <- check val (TypeApp tyObject (RCons prop ty rest))
return $ TypedValue True (Accessor prop val') ty
check' v@(Constructor c) ty = do
env <- getEnv
case M.lookup c (dataConstructors env) of
Nothing -> throwError . errorMessage $ UnknownDataConstructor c Nothing
Just (_, _, ty1, _) -> do
repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
mv <- subsumes (Just v) repl ty
case mv of
Nothing -> internalError "check: unable to check the subsumes relation."
Just v' -> return $ TypedValue True v' ty
check' (Let ds val) ty = do
(ds', val') <- inferLetBinding [] ds val (`check` ty)
return $ TypedValue True (Let ds' val') ty
check' val kt@(KindedType ty kind) = do
checkTypeKind ty kind
val' <- check' val ty
return $ TypedValue True val' kt
check' (PositionedValue pos c val) ty = warnAndRethrowWithPosition pos $ do
TypedValue t v ty' <- check' val ty
return $ TypedValue t (PositionedValue pos c v) ty'
check' val ty = do
TypedValue _ val' ty' <- infer val
mt <- subsumes (Just val') ty' ty
case mt of
Nothing -> internalError "check: unable to check the subsumes relation."
Just v' -> return $ TypedValue True v' ty
checkProperties ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr ->
[(String, Expr)] ->
Type ->
Bool ->
m [(String, Expr)]
checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' where
go [] [] REmpty = return []
go [] [] u@(TUnknown _)
| lax = return []
| otherwise = do unifyTypes u REmpty
return []
go [] [] Skolem{} | lax = return []
go [] ((p, _): _) _ | lax = return []
| otherwise = throwError . errorMessage $ PropertyIsMissing p
go ((p,_):_) [] REmpty = throwError . errorMessage $ AdditionalProperty p
go ((p,v):ps') ts r =
case lookup p ts of
Nothing -> do
v'@(TypedValue _ _ ty) <- infer v
rest <- freshType
unifyTypes r (RCons p ty rest)
ps'' <- go ps' ts rest
return $ (p, v') : ps''
Just ty -> do
v' <- check v ty
ps'' <- go ps' (delete (p, ty) ts) r
return $ (p, v') : ps''
go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyObject row)
checkFunctionApplication ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr ->
Type ->
Expr ->
Maybe Type ->
m (Type, Expr)
checkFunctionApplication fn fnTy arg ret = rethrow (addHint (ErrorInApplication fn fnTy arg)) $ do
subst <- gets checkSubstitution
checkFunctionApplication' fn (substituteType subst fnTy) arg (substituteType subst <$> ret)
checkFunctionApplication' ::
(Functor m, Applicative m, MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr ->
Type ->
Expr ->
Maybe Type ->
m (Type, Expr)
checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
unifyTypes tyFunction' tyFunction
arg' <- check arg argTy
case ret of
Nothing -> return (retTy, App fn arg')
Just ret' -> do
Just app' <- subsumes (Just (App fn arg')) retTy ret'
return (retTy, app')
checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
replaced <- replaceVarWithUnknown ident ty
checkFunctionApplication fn replaced arg ret
checkFunctionApplication' fn u@(TUnknown _) arg ret = do
arg' <- do
TypedValue _ arg' t <- infer arg
(arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
return $ TypedValue True arg'' t'
let ty = (\(TypedValue _ _ t) -> t) arg'
ret' <- maybe freshType return ret
unifyTypes u (function ty ret')
return (ret', App fn arg')
checkFunctionApplication' fn (KindedType ty _) arg ret =
checkFunctionApplication fn ty arg ret
checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
dicts <- getTypeClassDictionaries
checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) constraints)) fnTy arg ret
checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} _ =
return (fnTy, App fn dict)
checkFunctionApplication' _ fnTy arg _ = throwError . errorMessage $ CannotApplyFunction fnTy arg
meet ::
(Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>
Expr ->
Expr ->
Type ->
Type ->
m (Expr, Expr, Type)
meet e1 e2 (ForAll ident t1 _) t2 = do
t1' <- replaceVarWithUnknown ident t1
meet e1 e2 t1' t2
meet e1 e2 t1 (ForAll ident t2 _) = do
t2' <- replaceVarWithUnknown ident t2
meet e1 e2 t1 t2'
meet e1 e2 t1 t2 = do
unifyTypes t1 t2
return (e1, e2, t1)
ensureNoDuplicateProperties :: (MonadError MultipleErrors m) => [(String, Expr)] -> m ()
ensureNoDuplicateProperties ps =
let ls = map fst ps in
case ls \\ nub ls of
l : _ -> throwError . errorMessage $ DuplicateLabel l Nothing
_ -> return ()