module Language.PureScript.TypeChecker.Types
( BindingGroupType(..)
, typesOf
, checkTypeKind
) where
import Prelude
import Protolude (ordNub, fold, atMay)
import Control.Arrow (first, second, (***))
import Control.Monad (forM, forM_, guard, replicateM, unless, when, zipWithM, (<=<))
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..), gets)
import Control.Monad.Supply.Class (MonadSupply)
import Control.Monad.Writer.Class (MonadWriter(..))
import Data.Bifunctor (bimap)
import Data.Either (partitionEithers)
import Data.Functor (($>))
import Data.List (transpose, (\\), partition, delete)
import Data.Maybe (fromMaybe)
import Data.Text (Text)
import Data.Traversable (for)
import Data.List.NonEmpty qualified as NEL
import Data.Map qualified as M
import Data.Set qualified as S
import Data.IntSet qualified as IS
import Language.PureScript.AST
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment
import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors, SimpleErrorMessage(..), errorMessage, errorMessage', escalateWarningWhen, internalCompilerError, onErrorMessages, onTypesInErrorMessage, parU)
import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName, Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), byMaybeModuleName, coerceProperName, freshIdent)
import Language.PureScript.TypeChecker.Deriving (deriveInstance)
import Language.PureScript.TypeChecker.Entailment (InstanceContext, newDictionaries, replaceTypeClassDictionaries)
import Language.PureScript.TypeChecker.Kinds (checkConstraint, checkKind, checkTypeKind, kindOf, kindOfWithScopedVars, unifyKinds', unknownsWithKinds)
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Skolems (introduceSkolemScope, newSkolemConstant, newSkolemScope, skolemEscapeCheck, skolemize, skolemizeTypesInValue)
import Language.PureScript.TypeChecker.Subsumption (subsumes)
import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
import Language.PureScript.TypeChecker.TypeSearch (typeSearch)
import Language.PureScript.TypeChecker.Unify (freshTypeWithKind, replaceTypeWildcards, substituteType, unifyTypes, unknownsInType, varIfUnknown)
import Language.PureScript.Types
import Language.PureScript.Label (Label(..))
import Language.PureScript.PSString (PSString)
data BindingGroupType
= RecursiveBindingGroup
| NonRecursiveBindingGroup
deriving (Int -> BindingGroupType -> ShowS
[BindingGroupType] -> ShowS
BindingGroupType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BindingGroupType] -> ShowS
$cshowList :: [BindingGroupType] -> ShowS
show :: BindingGroupType -> String
$cshow :: BindingGroupType -> String
showsPrec :: Int -> BindingGroupType -> ShowS
$cshowsPrec :: Int -> BindingGroupType -> ShowS
Show, BindingGroupType -> BindingGroupType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BindingGroupType -> BindingGroupType -> Bool
$c/= :: BindingGroupType -> BindingGroupType -> Bool
== :: BindingGroupType -> BindingGroupType -> Bool
$c== :: BindingGroupType -> BindingGroupType -> Bool
Eq, Eq BindingGroupType
BindingGroupType -> BindingGroupType -> Bool
BindingGroupType -> BindingGroupType -> Ordering
BindingGroupType -> BindingGroupType -> BindingGroupType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BindingGroupType -> BindingGroupType -> BindingGroupType
$cmin :: BindingGroupType -> BindingGroupType -> BindingGroupType
max :: BindingGroupType -> BindingGroupType -> BindingGroupType
$cmax :: BindingGroupType -> BindingGroupType -> BindingGroupType
>= :: BindingGroupType -> BindingGroupType -> Bool
$c>= :: BindingGroupType -> BindingGroupType -> Bool
> :: BindingGroupType -> BindingGroupType -> Bool
$c> :: BindingGroupType -> BindingGroupType -> Bool
<= :: BindingGroupType -> BindingGroupType -> Bool
$c<= :: BindingGroupType -> BindingGroupType -> Bool
< :: BindingGroupType -> BindingGroupType -> Bool
$c< :: BindingGroupType -> BindingGroupType -> Bool
compare :: BindingGroupType -> BindingGroupType -> Ordering
$ccompare :: BindingGroupType -> BindingGroupType -> Ordering
Ord)
data TypedValue' = TypedValue' Bool Expr SourceType
tvToExpr :: TypedValue' -> Expr
tvToExpr :: TypedValue' -> Expr
tvToExpr (TypedValue' Bool
c Expr
e SourceType
t) = Bool -> Expr -> SourceType -> Expr
TypedValue Bool
c Expr
e SourceType
t
lookupTypeClass :: MonadState CheckState m => Qualified (ProperName 'ClassName) -> m TypeClassData
lookupTypeClass :: forall (m :: * -> *).
MonadState CheckState m =>
Qualified (ProperName 'ClassName) -> m TypeClassData
lookupTypeClass Qualified (ProperName 'ClassName)
name =
let findClass :: Map (Qualified (ProperName 'ClassName)) TypeClassData
-> TypeClassData
findClass = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"entails: type class not found in environment") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ClassName)
name
in forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Map (Qualified (ProperName 'ClassName)) TypeClassData
-> TypeClassData
findClass forall b c a. (b -> c) -> (a -> b) -> a -> c
. Environment
-> Map (Qualified (ProperName 'ClassName)) TypeClassData
typeClasses forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckState -> Environment
checkEnv)
typesOf
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> BindingGroupType
-> ModuleName
-> [((SourceAnn, Ident), Expr)]
-> m [((SourceAnn, Ident), (Expr, SourceType))]
typesOf :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
BindingGroupType
-> ModuleName
-> [((SourceAnn, Ident), Expr)]
-> m [((SourceAnn, Ident), (Expr, SourceType))]
typesOf BindingGroupType
bindingGroupType ModuleName
moduleName [((SourceAnn, Ident), Expr)]
vals = forall (m :: * -> *) a. MonadState CheckState m => m a -> m a
withFreshSubstitution forall a b. (a -> b) -> a -> b
$ do
([(Bool,
(((SourceAnn, Ident), (Expr, SourceType)), MultipleErrors))]
tys, MultipleErrors
wInfer) <- forall (m :: * -> *) a b.
MonadState CheckState m =>
(a -> Substitution -> b) -> m a -> m b
capturingSubstitution forall {d} {d} {d} {d}.
([(d, ((d, (Expr, SourceType)), d))], d)
-> Substitution -> ([(d, ((d, (Expr, SourceType)), d))], d)
tidyUp forall a b. (a -> b) -> a -> b
$ do
(SplitBindingGroup [((SourceAnn, Ident), (Expr, SourceType))]
untyped [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
typed Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict, MultipleErrors
w) <- forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
withoutWarnings forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
Maybe ModuleName
-> [((SourceAnn, Ident), Expr)] -> m SplitBindingGroup
typeDictionaryForBindingGroup (forall a. a -> Maybe a
Just ModuleName
moduleName) [((SourceAnn, Ident), Expr)]
vals
[(((SourceAnn, Ident), (Expr, SourceType)), MultipleErrors)]
ds1 <- forall (m :: * -> *) a b.
MonadError MultipleErrors m =>
[a] -> (a -> m b) -> m [b]
parU [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
typed forall a b. (a -> b) -> a -> b
$ \((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))
e -> forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
withoutWarnings forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
ModuleName
-> ((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
checkTypedBindingGroupElement ModuleName
moduleName ((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))
e Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict
[(((SourceAnn, Ident), (Expr, SourceType)), MultipleErrors)]
ds2 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [((SourceAnn, Ident), (Expr, SourceType))]
untyped forall a b. (a -> b) -> a -> b
$ \((SourceAnn, Ident), (Expr, SourceType))
e -> forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
withoutWarnings forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
((SourceAnn, Ident), (Expr, SourceType))
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
typeForBindingGroupElement ((SourceAnn, Ident), (Expr, SourceType))
e Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map (Bool
False, ) [(((SourceAnn, Ident), (Expr, SourceType)), MultipleErrors)]
ds1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Bool
True, ) [(((SourceAnn, Ident), (Expr, SourceType)), MultipleErrors)]
ds2, MultipleErrors
w)
[(((SourceAnn, Ident), (Expr, SourceType)),
[(Ident, InstanceContext, SourceConstraint)])]
inferred <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Bool,
(((SourceAnn, Ident), (Expr, SourceType)), MultipleErrors))]
tys forall a b. (a -> b) -> a -> b
$ \(Bool
shouldGeneralize, ((sai :: (SourceAnn, Ident)
sai@((SourceSpan
ss, [Comment]
_), Ident
ident), (Expr
val, SourceType
ty)), MultipleErrors
_)) -> do
(Expr
val', [(Ident, InstanceContext, SourceConstraint)]
unsolved) <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m, MonadSupply m) =>
Bool
-> Expr -> m (Expr, [(Ident, InstanceContext, SourceConstraint)])
replaceTypeClassDictionaries Bool
shouldGeneralize Expr
val
Substitution
currentSubst <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
let ty' :: SourceType
ty' = Substitution -> SourceType -> SourceType
substituteType Substitution
currentSubst SourceType
ty
ty'' :: SourceType
ty'' = forall {a} {b}.
[(a, b, SourceConstraint)] -> SourceType -> SourceType
constrain [(Ident, InstanceContext, SourceConstraint)]
unsolved SourceType
ty'
[(Int, SourceType)]
unsolvedTypeVarsWithKinds <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> IntSet
unknowns forall a b. (a -> b) -> a -> b
$ forall {a} {b}.
[(a, b, SourceConstraint)] -> SourceType -> SourceType
constrain [(Ident, InstanceContext, SourceConstraint)]
unsolved SourceType
ty''
let unsolvedTypeVars :: [Int]
unsolvedTypeVars = IntSet -> [Int]
IS.toList forall a b. (a -> b) -> a -> b
$ forall a. Type a -> IntSet
unknowns SourceType
ty'
SourceType
generalized <- forall (m :: * -> *).
MonadState CheckState m =>
[(Int, SourceType)] -> SourceType -> m SourceType
varIfUnknown [(Int, SourceType)]
unsolvedTypeVarsWithKinds SourceType
ty''
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
shouldGeneralize forall a b. (a -> b) -> a -> b
$ do
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss
forall a b. (a -> b) -> a -> b
$ Ident -> SourceType -> SimpleErrorMessage
MissingTypeDeclaration Ident
ident SourceType
generalized
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BindingGroupType
bindingGroupType forall a. Eq a => a -> a -> Bool
== BindingGroupType
RecursiveBindingGroup Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Ident, InstanceContext, SourceConstraint)]
unsolved))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss
forall a b. (a -> b) -> a -> b
$ Ident -> SourceType -> SimpleErrorMessage
CannotGeneralizeRecursiveFunction Ident
ident SourceType
generalized
[([FunctionalDependency], [Set Int])]
conData <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ident, InstanceContext, SourceConstraint)]
unsolved forall a b. (a -> b) -> a -> b
$ \(Ident
_, InstanceContext
_, SourceConstraint
con) -> do
TypeClassData{ [FunctionalDependency]
typeClassDependencies :: TypeClassData -> [FunctionalDependency]
typeClassDependencies :: [FunctionalDependency]
typeClassDependencies } <- forall (m :: * -> *).
MonadState CheckState m =>
Qualified (ProperName 'ClassName) -> m TypeClassData
lookupTypeClass forall a b. (a -> b) -> a -> b
$ forall a. Constraint a -> Qualified (ProperName 'ClassName)
constraintClass SourceConstraint
con
let
unknownsForArg :: [S.Set Int]
unknownsForArg :: [Set Int]
unknownsForArg =
forall a b. (a -> b) -> [a] -> [b]
map (forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> [(a, Int)]
unknownsInType) (forall a. Constraint a -> [Type a]
constraintArgs SourceConstraint
con)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FunctionalDependency]
typeClassDependencies, [Set Int]
unknownsForArg)
let
solveFrom :: S.Set Int -> S.Set Int
solveFrom :: Set Int -> Set Int
solveFrom Set Int
determined = do
let solved :: Set Int
solved = Set Int -> Set Int
solve1 Set Int
determined
if Set Int
solved forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Int
determined
then Set Int
determined
else Set Int -> Set Int
solveFrom (Set Int
determined forall a. Semigroup a => a -> a -> a
<> Set Int
solved)
solve1 :: S.Set Int -> S.Set Int
solve1 :: Set Int -> Set Int
solve1 Set Int
determined = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$ do
([FunctionalDependency]
tcDeps, [Set Int]
conArgUnknowns) <- [([FunctionalDependency], [Set Int])]
conData
let
lookupUnknowns :: Int -> Maybe (S.Set Int)
lookupUnknowns :: Int -> Maybe (Set Int)
lookupUnknowns = forall a. [a] -> Int -> Maybe a
atMay [Set Int]
conArgUnknowns
unknownsDetermined :: Maybe (S.Set Int) -> Bool
unknownsDetermined :: Maybe (Set Int) -> Bool
unknownsDetermined Maybe (Set Int)
Nothing = Bool
False
unknownsDetermined (Just Set Int
unks) =
Set Int
unks forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Int
determined
FunctionalDependency
tcDep <- [FunctionalDependency]
tcDeps
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe (Set Int) -> Bool
unknownsDetermined forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe (Set Int)
lookupUnknowns) (FunctionalDependency -> [Int]
fdDeterminers FunctionalDependency
tcDep)
forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. Set a
S.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe (Set Int)
lookupUnknowns) (FunctionalDependency -> [Int]
fdDetermined FunctionalDependency
tcDep)
let determinedFromType :: Set Int
determinedFromType = forall a. Ord a => [a] -> Set a
S.fromList [Int]
unsolvedTypeVars
let constraintTypeVars :: Set Int
constraintTypeVars = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([([FunctionalDependency], [Set Int])]
conData forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b. (a, b) -> b
snd)
let solved :: Set Int
solved = Set Int -> Set Int
solveFrom Set Int
determinedFromType
let unsolvedVars :: Set Int
unsolvedVars = forall a. Ord a => Set a -> Set a -> Set a
S.difference Set Int
constraintTypeVars Set Int
solved
let lookupUnkName' :: Int -> m (Text, Int)
lookupUnkName' Int
i = do
Maybe Text
mn <- forall (m :: * -> *).
MonadState CheckState m =>
Int -> m (Maybe Text)
lookupUnkName Int
i
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a -> a
fromMaybe Text
"t" Maybe Text
mn, Int
i)
[(Text, Int)]
unsolvedVarNames <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {m :: * -> *}.
MonadState CheckState m =>
Int -> m (Text, Int)
lookupUnkName' (forall a. Set a -> [a]
S.toList Set Int
unsolvedVars)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Set a -> Bool
S.null Set Int
unsolvedVars) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorMessage -> ErrorMessage) -> MultipleErrors -> MultipleErrors
onErrorMessages (Substitution -> ErrorMessage -> ErrorMessage
replaceTypes Substitution
currentSubst)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss
forall a b. (a -> b) -> a -> b
$ SourceType -> [(Text, Int)] -> SimpleErrorMessage
AmbiguousTypeVariables SourceType
generalized [(Text, Int)]
unsolvedVarNames
forall (m :: * -> *). MonadError MultipleErrors m => Expr -> m ()
skolemEscapeCheck Expr
val'
forall (m :: * -> *) a. Monad m => a -> m a
return (((SourceAnn, Ident)
sai, (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Binder -> Expr -> Expr
Abs forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> Ident -> Binder
VarBinder SourceSpan
nullSourceSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Ident
x, InstanceContext
_, SourceConstraint
_) -> Ident
x)) Expr
val' [(Ident, InstanceContext, SourceConstraint)]
unsolved, SourceType
generalized)), [(Ident, InstanceContext, SourceConstraint)]
unsolved)
CheckState
finalState <- forall s (m :: * -> *). MonadState s m => m s
get
let replaceTypes' :: ErrorMessage -> ErrorMessage
replaceTypes' = Substitution -> ErrorMessage -> ErrorMessage
replaceTypes (CheckState -> Substitution
checkSubstitution CheckState
finalState)
runTypeSearch' :: Bool -> ErrorMessage -> ErrorMessage
runTypeSearch' Bool
gen = Maybe [(Ident, InstanceContext, SourceConstraint)]
-> CheckState -> ErrorMessage -> ErrorMessage
runTypeSearch (forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
gen forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a b. (a, b) -> b
snd [(((SourceAnn, Ident), (Expr, SourceType)),
[(Ident, InstanceContext, SourceConstraint)])]
inferred) CheckState
finalState
raisePreviousWarnings :: Bool -> MultipleErrors -> m ()
raisePreviousWarnings Bool
gen = forall (m :: * -> *) a.
(MonadWriter MultipleErrors m, MonadError MultipleErrors m) =>
(ErrorMessage -> Bool) -> m a -> m a
escalateWarningWhen ErrorMessage -> Bool
isHoleError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorMessage -> ErrorMessage) -> MultipleErrors -> MultipleErrors
onErrorMessages (Bool -> ErrorMessage -> ErrorMessage
runTypeSearch' Bool
gen forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorMessage -> ErrorMessage
replaceTypes')
Bool -> MultipleErrors -> m ()
raisePreviousWarnings Bool
False MultipleErrors
wInfer
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Bool,
(((SourceAnn, Ident), (Expr, SourceType)), MultipleErrors))]
tys forall a b. (a -> b) -> a -> b
$ \(Bool
shouldGeneralize, (((SourceAnn, Ident)
_, (Expr
_, SourceType
_)), MultipleErrors
w)) ->
Bool -> MultipleErrors -> m ()
raisePreviousWarnings Bool
shouldGeneralize MultipleErrors
w
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(((SourceAnn, Ident), (Expr, SourceType)),
[(Ident, InstanceContext, SourceConstraint)])]
inferred)
where
replaceTypes
:: Substitution
-> ErrorMessage
-> ErrorMessage
replaceTypes :: Substitution -> ErrorMessage -> ErrorMessage
replaceTypes Substitution
subst = (SourceType -> SourceType) -> ErrorMessage -> ErrorMessage
onTypesInErrorMessage (Substitution -> SourceType -> SourceType
substituteType Substitution
subst)
runTypeSearch
:: Maybe [(Ident, InstanceContext, SourceConstraint)]
-> CheckState
-> ErrorMessage
-> ErrorMessage
runTypeSearch :: Maybe [(Ident, InstanceContext, SourceConstraint)]
-> CheckState -> ErrorMessage -> ErrorMessage
runTypeSearch Maybe [(Ident, InstanceContext, SourceConstraint)]
cons CheckState
st = \case
ErrorMessage [ErrorMessageHint]
hints (HoleInferredType Text
x SourceType
ty Context
y (Just (TSBefore Environment
env))) ->
let subst :: Substitution
subst = CheckState -> Substitution
checkSubstitution CheckState
st
searchResult :: TypeSearch
searchResult = (SourceType -> SourceType) -> TypeSearch -> TypeSearch
onTypeSearchTypes
(Substitution -> SourceType -> SourceType
substituteType Substitution
subst)
(forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [(Qualified Text, SourceType)]
-> Maybe [(Label, SourceType)] -> TypeSearch
TSAfter (Maybe [(Ident, InstanceContext, SourceConstraint)]
-> Environment
-> CheckState
-> SourceType
-> ([(Qualified Text, SourceType)], Maybe [(Label, SourceType)])
typeSearch Maybe [(Ident, InstanceContext, SourceConstraint)]
cons Environment
env CheckState
st (Substitution -> SourceType -> SourceType
substituteType Substitution
subst SourceType
ty)))
in [ErrorMessageHint] -> SimpleErrorMessage -> ErrorMessage
ErrorMessage [ErrorMessageHint]
hints (Text
-> SourceType -> Context -> Maybe TypeSearch -> SimpleErrorMessage
HoleInferredType Text
x SourceType
ty Context
y (forall a. a -> Maybe a
Just TypeSearch
searchResult))
ErrorMessage
other -> ErrorMessage
other
constrain :: [(a, b, SourceConstraint)] -> SourceType -> SourceType
constrain [(a, b, SourceConstraint)]
cs SourceType
ty = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SourceConstraint -> SourceType -> SourceType
srcConstrainedType SourceType
ty (forall a b. (a -> b) -> [a] -> [b]
map (\(a
_, b
_, SourceConstraint
x) -> SourceConstraint
x) [(a, b, SourceConstraint)]
cs)
tidyUp :: ([(d, ((d, (Expr, SourceType)), d))], d)
-> Substitution -> ([(d, ((d, (Expr, SourceType)), d))], d)
tidyUp ([(d, ((d, (Expr, SourceType)), d))], d)
ts Substitution
sub = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((SourceType -> SourceType) -> Expr -> Expr
overTypes (Substitution -> SourceType -> SourceType
substituteType Substitution
sub) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Substitution -> SourceType -> SourceType
substituteType Substitution
sub))))) ([(d, ((d, (Expr, SourceType)), d))], d)
ts
isHoleError :: ErrorMessage -> Bool
isHoleError :: ErrorMessage -> Bool
isHoleError (ErrorMessage [ErrorMessageHint]
_ HoleInferredType{}) = Bool
True
isHoleError ErrorMessage
_ = Bool
False
data SplitBindingGroup = SplitBindingGroup
{ SplitBindingGroup -> [((SourceAnn, Ident), (Expr, SourceType))]
_splitBindingGroupUntyped :: [((SourceAnn, Ident), (Expr, SourceType))]
, SplitBindingGroup
-> [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
_splitBindingGroupTyped :: [((SourceAnn, Ident), (Expr, [(Text, SourceType)], SourceType, Bool))]
, SplitBindingGroup
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
_splitBindingGroupNames :: M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
}
typeDictionaryForBindingGroup
:: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Maybe ModuleName
-> [((SourceAnn, Ident), Expr)]
-> m SplitBindingGroup
typeDictionaryForBindingGroup :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
Maybe ModuleName
-> [((SourceAnn, Ident), Expr)] -> m SplitBindingGroup
typeDictionaryForBindingGroup Maybe ModuleName
moduleName [((SourceAnn, Ident), Expr)]
vals = do
let ([((SourceAnn, Ident), Expr)]
untyped, [((SourceAnn, Ident), (Expr, SourceType, Bool))]
typed) = forall a b. [Either a b] -> ([a], [b])
partitionEithers (forall a b. (a -> b) -> [a] -> [b]
map forall a.
(a, Expr) -> Either (a, Expr) (a, (Expr, SourceType, Bool))
splitTypeAnnotation [((SourceAnn, Ident), Expr)]
vals)
([((SourceAnn, Ident), SourceType)]
typedDict, [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
typed') <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. [(a, b)] -> ([a], [b])
unzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [((SourceAnn, Ident), (Expr, SourceType, Bool))]
typed forall a b. (a -> b) -> a -> b
$ \((SourceAnn, Ident)
sai, (Expr
expr, SourceType
ty, Bool
checkType)) -> do
(([(Text, SourceType)]
args, SourceType
elabTy), SourceType
kind) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (([(Text, SourceType)], SourceType), SourceType)
kindOfWithScopedVars SourceType
ty
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
ty SourceType
kind
SourceType
elabTy' <- forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards SourceType
elabTy
forall (m :: * -> *) a. Monad m => a -> m a
return (((SourceAnn, Ident)
sai, SourceType
elabTy'), ((SourceAnn, Ident)
sai, (Expr
expr, [(Text, SourceType)]
args, SourceType
elabTy', Bool
checkType)))
([((SourceAnn, Ident), SourceType)]
untypedDict, [((SourceAnn, Ident), (Expr, SourceType))]
untyped') <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. [(a, b)] -> ([a], [b])
unzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [((SourceAnn, Ident), Expr)]
untyped forall a b. (a -> b) -> a -> b
$ \((SourceAnn, Ident)
sai, Expr
expr) -> do
SourceType
ty <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
forall (m :: * -> *) a. Monad m => a -> m a
return (((SourceAnn, Ident)
sai, SourceType
ty), ((SourceAnn, Ident)
sai, (Expr
expr, SourceType
ty)))
let dict :: Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (forall a. QualifiedBy -> a -> Qualified a
Qualified (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SourcePos -> QualifiedBy
BySourcePos forall a b. (a -> b) -> a -> b
$ SourceSpan -> SourcePos
spanStart SourceSpan
ss) ModuleName -> QualifiedBy
ByModuleName Maybe ModuleName
moduleName) Ident
ident, (SourceType
ty, NameKind
Private, NameVisibility
Undefined))
| (((SourceSpan
ss, [Comment]
_), Ident
ident), SourceType
ty) <- [((SourceAnn, Ident), SourceType)]
typedDict forall a. Semigroup a => a -> a -> a
<> [((SourceAnn, Ident), SourceType)]
untypedDict
]
forall (m :: * -> *) a. Monad m => a -> m a
return ([((SourceAnn, Ident), (Expr, SourceType))]
-> [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> SplitBindingGroup
SplitBindingGroup [((SourceAnn, Ident), (Expr, SourceType))]
untyped' [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
typed' Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict)
where
splitTypeAnnotation :: (a, Expr) -> Either (a, Expr) (a, (Expr, SourceType, Bool))
splitTypeAnnotation :: forall a.
(a, Expr) -> Either (a, Expr) (a, (Expr, SourceType, Bool))
splitTypeAnnotation (a
a, TypedValue Bool
checkType Expr
value SourceType
ty) = forall a b. b -> Either a b
Right (a
a, (Expr
value, SourceType
ty, Bool
checkType))
splitTypeAnnotation (a
a, PositionedValue SourceSpan
pos [Comment]
c Expr
value) =
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (SourceSpan -> [Comment] -> Expr -> Expr
PositionedValue SourceSpan
pos [Comment]
c))
(forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (\(Expr
e, SourceType
t, Bool
b) -> (SourceSpan -> [Comment] -> Expr -> Expr
PositionedValue SourceSpan
pos [Comment]
c Expr
e, SourceType
t, Bool
b)))
(forall a.
(a, Expr) -> Either (a, Expr) (a, (Expr, SourceType, Bool))
splitTypeAnnotation (a
a, Expr
value))
splitTypeAnnotation (a
a, Expr
value) = forall a b. a -> Either a b
Left (a
a, Expr
value)
checkTypedBindingGroupElement
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> ModuleName
-> ((SourceAnn, Ident), (Expr, [(Text, SourceType)], SourceType, Bool))
-> M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
checkTypedBindingGroupElement :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
ModuleName
-> ((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
checkTypedBindingGroupElement ModuleName
mn ((SourceAnn, Ident)
ident, (Expr
val, [(Text, SourceType)]
args, SourceType
ty, Bool
checkType)) Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict = do
SourceType
ty' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall a b. (a -> b) -> a -> b
$ SourceType
ty
TypedValue'
val' <- if Bool
checkType
then forall (m :: * -> *) a.
(MonadState CheckState m, MonadWriter MultipleErrors m) =>
ModuleName -> [(Text, SourceType)] -> m a -> m a
withScopedTypeVars ModuleName
mn [(Text, SourceType)]
args forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadState CheckState m =>
Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m a -> m a
bindNames Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val SourceType
ty'
else forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
False Expr
val SourceType
ty')
forall (m :: * -> *) a. Monad m => a -> m a
return ((SourceAnn, Ident)
ident, (TypedValue' -> Expr
tvToExpr TypedValue'
val', SourceType
ty'))
typeForBindingGroupElement
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> ((SourceAnn, Ident), (Expr, SourceType))
-> M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
typeForBindingGroupElement :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
((SourceAnn, Ident), (Expr, SourceType))
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
typeForBindingGroupElement ((SourceAnn, Ident)
ident, (Expr
val, SourceType
ty)) Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict = do
TypedValue' Bool
_ Expr
val' SourceType
ty' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m a -> m a
bindNames Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
val
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
ty SourceType
ty'
forall (m :: * -> *) a. Monad m => a -> m a
return ((SourceAnn, Ident)
ident, (Bool -> Expr -> SourceType -> Expr
TypedValue Bool
True Expr
val' SourceType
ty', SourceType
ty'))
instantiatePolyTypeWithUnknowns
:: (MonadState CheckState m, MonadError MultipleErrors m)
=> Expr
-> SourceType
-> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns Expr
val (ForAll SourceAnn
_ TypeVarVisibility
_ Text
ident Maybe SourceType
mbK SourceType
ty Maybe SkolemScope
_) = do
SourceType
u <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError Text
"Unelaborated forall") forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind Maybe SourceType
mbK
forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
SourceType -> Text -> m ()
insertUnkName' SourceType
u Text
ident
forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns Expr
val forall a b. (a -> b) -> a -> b
$ forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
ident SourceType
u SourceType
ty
instantiatePolyTypeWithUnknowns Expr
val (ConstrainedType SourceAnn
_ SourceConstraint
con SourceType
ty) = do
InstanceContext
dicts <- forall (m :: * -> *). MonadState CheckState m => m InstanceContext
getTypeClassDictionaries
[ErrorMessageHint]
hints <- forall (m :: * -> *).
MonadState CheckState m =>
m [ErrorMessageHint]
getHints
forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns (Expr -> Expr -> Expr
App Expr
val (SourceConstraint -> InstanceContext -> [ErrorMessageHint] -> Expr
TypeClassDictionary SourceConstraint
con InstanceContext
dicts [ErrorMessageHint]
hints)) SourceType
ty
instantiatePolyTypeWithUnknowns Expr
val SourceType
ty = forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
val, SourceType
ty)
instantiatePolyTypeWithUnknownsUntilVisible
:: (MonadState CheckState m, MonadError MultipleErrors m)
=> Expr
-> SourceType
-> m (Expr, SourceType)
instantiatePolyTypeWithUnknownsUntilVisible :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknownsUntilVisible Expr
val (ForAll SourceAnn
_ TypeVarVisibility
TypeVarInvisible Text
ident Maybe SourceType
mbK SourceType
ty Maybe SkolemScope
_) = do
SourceType
u <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError Text
"Unelaborated forall") forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind Maybe SourceType
mbK
forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
SourceType -> Text -> m ()
insertUnkName' SourceType
u Text
ident
forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknownsUntilVisible Expr
val forall a b. (a -> b) -> a -> b
$ forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
ident SourceType
u SourceType
ty
instantiatePolyTypeWithUnknownsUntilVisible Expr
val SourceType
ty = forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
val, SourceType
ty)
instantiateConstraint :: MonadState CheckState m => Expr -> Type SourceAnn -> m (Expr, Type SourceAnn)
instantiateConstraint :: forall (m :: * -> *).
MonadState CheckState m =>
Expr -> SourceType -> m (Expr, SourceType)
instantiateConstraint Expr
val (ConstrainedType SourceAnn
_ SourceConstraint
con SourceType
ty) = do
InstanceContext
dicts <- forall (m :: * -> *). MonadState CheckState m => m InstanceContext
getTypeClassDictionaries
[ErrorMessageHint]
hints <- forall (m :: * -> *).
MonadState CheckState m =>
m [ErrorMessageHint]
getHints
forall (m :: * -> *).
MonadState CheckState m =>
Expr -> SourceType -> m (Expr, SourceType)
instantiateConstraint (Expr -> Expr -> Expr
App Expr
val (SourceConstraint -> InstanceContext -> [ErrorMessageHint] -> Expr
TypeClassDictionary SourceConstraint
con InstanceContext
dicts [ErrorMessageHint]
hints)) SourceType
ty
instantiateConstraint Expr
val SourceType
ty = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
val, SourceType
ty)
insertUnkName' :: (MonadState CheckState m, MonadError MultipleErrors m) => SourceType -> Text -> m ()
insertUnkName' :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
SourceType -> Text -> m ()
insertUnkName' (TUnknown SourceAnn
_ Int
i) Text
n = forall (m :: * -> *).
MonadState CheckState m =>
Int -> Text -> m ()
insertUnkName Int
i Text
n
insertUnkName' SourceType
_ Text
_ = forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError Text
"type is not TUnknown"
infer
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> m TypedValue'
infer :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
val = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (Expr -> ErrorMessageHint
ErrorInferringType Expr
val) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer' Expr
val
infer'
:: forall m
. (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> m TypedValue'
infer' :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer' v :: Expr
v@(Literal SourceSpan
_ (NumericLiteral (Left Integer
_))) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
tyInt
infer' v :: Expr
v@(Literal SourceSpan
_ (NumericLiteral (Right Double
_))) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
tyNumber
infer' v :: Expr
v@(Literal SourceSpan
_ (StringLiteral PSString
_)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
tyString
infer' v :: Expr
v@(Literal SourceSpan
_ (CharLiteral Char
_)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
tyChar
infer' v :: Expr
v@(Literal SourceSpan
_ (BooleanLiteral Bool
_)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
tyBoolean
infer' (Literal SourceSpan
ss (ArrayLiteral [Expr]
vals)) = do
[TypedValue']
ts <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer [Expr]
vals
SourceType
els <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
[Expr]
ts' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TypedValue']
ts forall a b. (a -> b) -> a -> b
$ \(TypedValue' Bool
ch Expr
val SourceType
t) -> do
(Expr
val', SourceType
t') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns Expr
val SourceType
t
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
els SourceType
t'
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Expr -> SourceType -> Expr
TypedValue Bool
ch Expr
val' SourceType
t')
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
ss (forall a. [a] -> Literal a
ArrayLiteral [Expr]
ts')) (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyArray SourceType
els)
infer' (Literal SourceSpan
ss (ObjectLiteral [(PSString, Expr)]
ps)) = do
forall (m :: * -> *).
MonadError MultipleErrors m =>
[(PSString, Expr)] -> m ()
ensureNoDuplicateProperties [(PSString, Expr)]
ps
[(PSString, (Expr, SourceType))]
typedFields <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[(PSString, Expr)] -> m [(PSString, (Expr, SourceType))]
inferProperties [(PSString, Expr)]
ps
let
toRowListItem :: (PSString, (Expr, SourceType)) -> RowListItem SourceAnn
toRowListItem :: (PSString, (Expr, SourceType)) -> RowListItem SourceAnn
toRowListItem (PSString
l, (Expr
_, SourceType
t)) = Label -> SourceType -> RowListItem SourceAnn
srcRowListItem (PSString -> Label
Label PSString
l) SourceType
t
recordType :: SourceType
recordType :: SourceType
recordType = SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ((PSString, (Expr, SourceType)) -> RowListItem SourceAnn
toRowListItem forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(PSString, (Expr, SourceType))]
typedFields, SourceType -> SourceType -> SourceType
srcKindApp SourceType
srcREmpty SourceType
kindType)
typedProperties :: [(PSString, Expr)]
typedProperties :: [(PSString, Expr)]
typedProperties = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Bool -> Expr -> SourceType -> Expr
TypedValue Bool
True))) [(PSString, (Expr, SourceType))]
typedFields
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
ss (forall a. [(PSString, a)] -> Literal a
ObjectLiteral [(PSString, Expr)]
typedProperties)) SourceType
recordType
infer' (ObjectUpdate Expr
ob [(PSString, Expr)]
ps) = do
forall (m :: * -> *).
MonadError MultipleErrors m =>
[(PSString, Expr)] -> m ()
ensureNoDuplicateProperties [(PSString, Expr)]
ps
SourceType
rowType <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind (SourceType -> SourceType
kindRow SourceType
kindType)
let updateLabels :: [Label]
updateLabels = PSString -> Label
Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(PSString, Expr)]
ps
[(Label, SourceType)]
obTypes <- forall a b. [a] -> [b] -> [(a, b)]
zip [Label]
updateLabels forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Label]
updateLabels) (forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType)
let obItems :: [RowListItem SourceAnn]
obItems :: [RowListItem SourceAnn]
obItems = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Label -> SourceType -> RowListItem SourceAnn
srcRowListItem forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Label, SourceType)]
obTypes
obRecordType :: SourceType
obRecordType :: SourceType
obRecordType = SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
obItems, SourceType
rowType)
Expr
ob' <- Bool -> Expr -> SourceType -> Expr
TypedValue Bool
True forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
ob SourceType
obRecordType) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
obRecordType
[(PSString, (Expr, SourceType))]
typedFields <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[(PSString, Expr)] -> m [(PSString, (Expr, SourceType))]
inferProperties [(PSString, Expr)]
ps
let newItems :: [RowListItem SourceAnn]
newItems :: [RowListItem SourceAnn]
newItems = (\(PSString
l, (Expr
_, SourceType
t)) -> Label -> SourceType -> RowListItem SourceAnn
srcRowListItem (PSString -> Label
Label PSString
l) SourceType
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(PSString, (Expr, SourceType))]
typedFields
ps' :: [(PSString, Expr)]
ps' :: [(PSString, Expr)]
ps' = (\(PSString
l, (Expr
e, SourceType
t)) -> (PSString
l, Bool -> Expr -> SourceType -> Expr
TypedValue Bool
True Expr
e SourceType
t)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(PSString, (Expr, SourceType))]
typedFields
newRecordType :: SourceType
newRecordType :: SourceType
newRecordType = SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
newItems, SourceType
rowType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> [(PSString, Expr)] -> Expr
ObjectUpdate Expr
ob' [(PSString, Expr)]
ps') SourceType
newRecordType
infer' (Accessor PSString
prop Expr
val) = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (Expr -> PSString -> ErrorMessageHint
ErrorCheckingAccessor Expr
val PSString
prop) forall a b. (a -> b) -> a -> b
$ do
SourceType
field <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
SourceType
rest <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind (SourceType -> SourceType
kindRow SourceType
kindType)
Expr
typed <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord (Label -> SourceType -> SourceType -> SourceType
srcRCons (PSString -> Label
Label PSString
prop) SourceType
field SourceType
rest))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (PSString -> Expr -> Expr
Accessor PSString
prop Expr
typed) SourceType
field
infer' (Abs Binder
binder Expr
ret)
| VarBinder SourceSpan
ss Ident
arg <- Binder
binder = do
SourceType
ty <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
forall (m :: * -> *) a. MonadState CheckState m => m a -> m a
withBindingGroupVisible forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadState CheckState m =>
[(SourceSpan, Ident, SourceType, NameVisibility)] -> m a -> m a
bindLocalVariables [(SourceSpan
ss, Ident
arg, SourceType
ty, NameVisibility
Defined)] forall a b. (a -> b) -> a -> b
$ do
body :: TypedValue'
body@(TypedValue' Bool
_ Expr
_ SourceType
bodyTy) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer' Expr
ret
(Expr
body', SourceType
bodyTy') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns (TypedValue' -> Expr
tvToExpr TypedValue'
body) SourceType
bodyTy
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Binder -> Expr -> Expr
Abs (SourceSpan -> Ident -> Binder
VarBinder SourceSpan
ss Ident
arg) Expr
body') (SourceType -> SourceType -> SourceType
function SourceType
ty SourceType
bodyTy')
| Bool
otherwise = forall a. HasCallStack => String -> a
internalError String
"Binder was not desugared"
infer' (App Expr
f Expr
arg) = do
f' :: TypedValue'
f'@(TypedValue' Bool
_ Expr
_ SourceType
ft) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
f
(SourceType
ret, Expr
app) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication (TypedValue' -> Expr
tvToExpr TypedValue'
f') SourceType
ft Expr
arg
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
app SourceType
ret
infer' (VisibleTypeApp Expr
valFn (TypeWildcard SourceAnn
_ WildcardData
_)) = do
TypedValue' Bool
_ Expr
valFn' SourceType
valTy <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
valFn
(Expr
valFn'', SourceType
valTy') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknownsUntilVisible Expr
valFn' SourceType
valTy
case SourceType
valTy' of
ForAll SourceAnn
qAnn TypeVarVisibility
_ Text
qName Maybe SourceType
qKind SourceType
qBody Maybe SkolemScope
qSko -> do
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
valFn'' (forall a.
a
-> TypeVarVisibility
-> Text
-> Maybe (Type a)
-> Type a
-> Maybe SkolemScope
-> Type a
ForAll SourceAnn
qAnn TypeVarVisibility
TypeVarInvisible Text
qName Maybe SourceType
qKind SourceType
qBody Maybe SkolemScope
qSko)
SourceType
_ ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SourceType -> SimpleErrorMessage
CannotSkipTypeApplication SourceType
valTy'
infer' (VisibleTypeApp Expr
valFn SourceType
tyArg) = do
TypedValue' Bool
_ Expr
valFn' SourceType
valTy <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
valFn
SourceType
tyArg' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall a b. (a -> b) -> a -> b
$ SourceType
tyArg
(Expr
valFn'', SourceType
valTy') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknownsUntilVisible Expr
valFn' SourceType
valTy
case SourceType
valTy' of
ForAll SourceAnn
_ TypeVarVisibility
_ Text
qName (Just SourceType
qKind) SourceType
qBody Maybe SkolemScope
_ -> do
SourceType
tyArg'' <- forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
tyArg' forall a b. (a -> b) -> a -> b
$ SourceType
qKind
let resTy :: SourceType
resTy = forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
qName SourceType
tyArg'' SourceType
qBody
(Expr
valFn''', SourceType
resTy') <- forall (m :: * -> *).
MonadState CheckState m =>
Expr -> SourceType -> m (Expr, SourceType)
instantiateConstraint Expr
valFn'' SourceType
resTy
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
valFn''' SourceType
resTy'
SourceType
_ ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SimpleErrorMessage
CannotApplyExpressionOfTypeOnType SourceType
valTy SourceType
tyArg
infer' (Var SourceSpan
ss Qualified Ident
var) = do
forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
Qualified Ident -> m ()
checkVisibility Qualified Ident
var
SourceType
ty <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
Qualified Ident -> m SourceType
lookupVariable forall a b. (a -> b) -> a -> b
$ Qualified Ident
var
case SourceType
ty of
ConstrainedType SourceAnn
_ SourceConstraint
con SourceType
ty' -> do
InstanceContext
dicts <- forall (m :: * -> *). MonadState CheckState m => m InstanceContext
getTypeClassDictionaries
[ErrorMessageHint]
hints <- forall (m :: * -> *).
MonadState CheckState m =>
m [ErrorMessageHint]
getHints
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> Expr -> Expr
App (SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
ss Qualified Ident
var) (SourceConstraint -> InstanceContext -> [ErrorMessageHint] -> Expr
TypeClassDictionary SourceConstraint
con InstanceContext
dicts [ErrorMessageHint]
hints)) SourceType
ty'
SourceType
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
ss Qualified Ident
var) SourceType
ty
infer' v :: Expr
v@(Constructor SourceSpan
_ Qualified (ProperName 'ConstructorName)
c) = do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ConstructorName)
c (Environment
-> Map
(Qualified (ProperName 'ConstructorName))
(DataDeclType, ProperName 'TypeName, SourceType, [Ident])
dataConstructors Environment
env) of
Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'ConstructorName -> Name
DctorName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ConstructorName)
c
Just (DataDeclType
_, ProperName 'TypeName
_, SourceType
ty, [Ident]
_) -> Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall a b. (a -> b) -> a -> b
$ SourceType
ty)
infer' (Case [Expr]
vals [CaseAlternative]
binders) = do
([Expr]
vals', [SourceType]
ts) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Expr] -> [CaseAlternative] -> m ([Expr], [SourceType])
instantiateForBinders [Expr]
vals [CaseAlternative]
binders
SourceType
ret <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
[CaseAlternative]
binders' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[SourceType]
-> SourceType -> [CaseAlternative] -> m [CaseAlternative]
checkBinders [SourceType]
ts SourceType
ret [CaseAlternative]
binders
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True ([Expr] -> [CaseAlternative] -> Expr
Case [Expr]
vals' [CaseAlternative]
binders') SourceType
ret
infer' (IfThenElse Expr
cond Expr
th Expr
el) = do
Expr
cond' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
cond SourceType
tyBoolean
th' :: TypedValue'
th'@(TypedValue' Bool
_ Expr
_ SourceType
thTy) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
th
el' :: TypedValue'
el'@(TypedValue' Bool
_ Expr
_ SourceType
elTy) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
el
(Expr
th'', SourceType
thTy') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns (TypedValue' -> Expr
tvToExpr TypedValue'
th') SourceType
thTy
(Expr
el'', SourceType
elTy') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns (TypedValue' -> Expr
tvToExpr TypedValue'
el') SourceType
elTy
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
thTy' SourceType
elTy'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> Expr -> Expr -> Expr
IfThenElse Expr
cond' Expr
th'' Expr
el'') SourceType
thTy'
infer' (Let WhereProvenance
w [Declaration]
ds Expr
val) = do
([Declaration]
ds', tv :: TypedValue'
tv@(TypedValue' Bool
_ Expr
_ SourceType
valTy)) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Declaration]
-> [Declaration]
-> Expr
-> (Expr -> m TypedValue')
-> m ([Declaration], TypedValue')
inferLetBinding [] [Declaration]
ds Expr
val forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (WhereProvenance -> [Declaration] -> Expr -> Expr
Let WhereProvenance
w [Declaration]
ds' (TypedValue' -> Expr
tvToExpr TypedValue'
tv)) SourceType
valTy
infer' (DeferredDictionary Qualified (ProperName 'ClassName)
className [SourceType]
tys) = do
InstanceContext
dicts <- forall (m :: * -> *). MonadState CheckState m => m InstanceContext
getTypeClassDictionaries
[ErrorMessageHint]
hints <- forall (m :: * -> *).
MonadState CheckState m =>
m [ErrorMessageHint]
getHints
SourceConstraint
con <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceConstraint -> m SourceConstraint
checkConstraint (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
className [] [SourceType]
tys forall a. Maybe a
Nothing)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
False
(SourceConstraint -> InstanceContext -> [ErrorMessageHint] -> Expr
TypeClassDictionary SourceConstraint
con InstanceContext
dicts [ErrorMessageHint]
hints)
(forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SourceType -> SourceType -> SourceType
srcTypeApp (Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName Qualified (ProperName 'ClassName)
className)) [SourceType]
tys)
infer' (TypedValue Bool
checkType Expr
val SourceType
ty) = do
ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
(([(Text, SourceType)]
args, SourceType
elabTy), SourceType
kind) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (([(Text, SourceType)], SourceType), SourceType)
kindOfWithScopedVars SourceType
ty
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
ty SourceType
kind
SourceType
ty' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall a b. (a -> b) -> a -> b
$ SourceType
elabTy
TypedValue'
tv <- if Bool
checkType then forall (m :: * -> *) a.
(MonadState CheckState m, MonadWriter MultipleErrors m) =>
ModuleName -> [(Text, SourceType)] -> m a -> m a
withScopedTypeVars ModuleName
moduleName [(Text, SourceType)]
args (forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val SourceType
ty') else forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
False Expr
val SourceType
ty)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (TypedValue' -> Expr
tvToExpr TypedValue'
tv) SourceType
ty'
infer' (Hole Text
name) = do
SourceType
ty <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
Context
ctx <- forall (m :: * -> *). MonadState CheckState m => m Context
getLocalContext
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Text
-> SourceType -> Context -> Maybe TypeSearch -> SimpleErrorMessage
HoleInferredType Text
name SourceType
ty Context
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Environment -> TypeSearch
TSBefore Environment
env
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Text -> Expr
Hole Text
name) SourceType
ty
infer' (PositionedValue SourceSpan
pos [Comment]
c Expr
val) = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceSpan -> m a -> m a
warnAndRethrowWithPositionTC SourceSpan
pos forall a b. (a -> b) -> a -> b
$ do
TypedValue' Bool
t Expr
v SourceType
ty <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer' Expr
val
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
t (SourceSpan -> [Comment] -> Expr -> Expr
PositionedValue SourceSpan
pos [Comment]
c Expr
v) SourceType
ty
infer' Expr
v = forall a. HasCallStack => String -> a
internalError forall a b. (a -> b) -> a -> b
$ String
"Invalid argument to infer: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Expr
v
inferProperties
:: ( MonadSupply m
, MonadState CheckState m
, MonadError MultipleErrors m
, MonadWriter MultipleErrors m
)
=> [(PSString, Expr)]
-> m [(PSString, (Expr, SourceType))]
inferProperties :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[(PSString, Expr)] -> m [(PSString, (Expr, SourceType))]
inferProperties = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m (Expr, SourceType)
inferWithinRecord)
inferWithinRecord
:: ( MonadSupply m
, MonadState CheckState m
, MonadError MultipleErrors m
, MonadWriter MultipleErrors m
)
=> Expr
-> m (Expr, SourceType)
inferWithinRecord :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m (Expr, SourceType)
inferWithinRecord Expr
e = do
TypedValue' Bool
_ Expr
v SourceType
t <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
e
if Expr -> Bool
propertyShouldInstantiate Expr
e
then forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns Expr
v SourceType
t
else forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
v, SourceType
t)
propertyShouldInstantiate :: Expr -> Bool
propertyShouldInstantiate :: Expr -> Bool
propertyShouldInstantiate = \case
Var{} -> Bool
True
Constructor{} -> Bool
True
PositionedValue SourceSpan
_ [Comment]
_ Expr
e -> Expr -> Bool
propertyShouldInstantiate Expr
e
Expr
_ -> Bool
False
inferLetBinding
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> [Declaration]
-> [Declaration]
-> Expr
-> (Expr -> m TypedValue')
-> m ([Declaration], TypedValue')
inferLetBinding :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Declaration]
-> [Declaration]
-> Expr
-> (Expr -> m TypedValue')
-> m ([Declaration], TypedValue')
inferLetBinding [Declaration]
seen [] Expr
ret Expr -> m TypedValue'
j = ([Declaration]
seen, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadState CheckState m => m a -> m a
withBindingGroupVisible (Expr -> m TypedValue'
j Expr
ret)
inferLetBinding [Declaration]
seen (ValueDecl sa :: SourceAnn
sa@(SourceSpan
ss, [Comment]
_) Ident
ident NameKind
nameKind [] [MkUnguarded (TypedValue Bool
checkType Expr
val SourceType
ty)] : [Declaration]
rest) Expr
ret Expr -> m TypedValue'
j = do
ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
TypedValue' Bool
_ Expr
val' SourceType
ty'' <- forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceSpan -> m a -> m a
warnAndRethrowWithPositionTC SourceSpan
ss forall a b. (a -> b) -> a -> b
$ do
(([(Text, SourceType)]
args, SourceType
elabTy), SourceType
kind) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (([(Text, SourceType)], SourceType), SourceType)
kindOfWithScopedVars SourceType
ty
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
ty SourceType
kind
let dict :: Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict = forall k a. k -> a -> Map k a
M.singleton (forall a. QualifiedBy -> a -> Qualified a
Qualified (SourcePos -> QualifiedBy
BySourcePos forall a b. (a -> b) -> a -> b
$ SourceSpan -> SourcePos
spanStart SourceSpan
ss) Ident
ident) (SourceType
elabTy, NameKind
nameKind, NameVisibility
Undefined)
SourceType
ty' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall a b. (a -> b) -> a -> b
$ SourceType
elabTy
if Bool
checkType
then forall (m :: * -> *) a.
(MonadState CheckState m, MonadWriter MultipleErrors m) =>
ModuleName -> [(Text, SourceType)] -> m a -> m a
withScopedTypeVars ModuleName
moduleName [(Text, SourceType)]
args (forall (m :: * -> *) a.
MonadState CheckState m =>
Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m a -> m a
bindNames Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict (forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val SourceType
ty'))
else forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
checkType Expr
val SourceType
elabTy)
forall (m :: * -> *) a.
MonadState CheckState m =>
Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m a -> m a
bindNames (forall k a. k -> a -> Map k a
M.singleton (forall a. QualifiedBy -> a -> Qualified a
Qualified (SourcePos -> QualifiedBy
BySourcePos forall a b. (a -> b) -> a -> b
$ SourceSpan -> SourcePos
spanStart SourceSpan
ss) Ident
ident) (SourceType
ty'', NameKind
nameKind, NameVisibility
Defined))
forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Declaration]
-> [Declaration]
-> Expr
-> (Expr -> m TypedValue')
-> m ([Declaration], TypedValue')
inferLetBinding ([Declaration]
seen forall a. [a] -> [a] -> [a]
++ [SourceAnn
-> Ident -> NameKind -> [Binder] -> [GuardedExpr] -> Declaration
ValueDecl SourceAnn
sa Ident
ident NameKind
nameKind [] [Expr -> GuardedExpr
MkUnguarded (Bool -> Expr -> SourceType -> Expr
TypedValue Bool
checkType Expr
val' SourceType
ty'')]]) [Declaration]
rest Expr
ret Expr -> m TypedValue'
j
inferLetBinding [Declaration]
seen (ValueDecl sa :: SourceAnn
sa@(SourceSpan
ss, [Comment]
_) Ident
ident NameKind
nameKind [] [MkUnguarded Expr
val] : [Declaration]
rest) Expr
ret Expr -> m TypedValue'
j = do
SourceType
valTy <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
TypedValue' Bool
_ Expr
val' SourceType
valTy' <- forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceSpan -> m a -> m a
warnAndRethrowWithPositionTC SourceSpan
ss forall a b. (a -> b) -> a -> b
$ do
let dict :: Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict = forall k a. k -> a -> Map k a
M.singleton (forall a. QualifiedBy -> a -> Qualified a
Qualified (SourcePos -> QualifiedBy
BySourcePos forall a b. (a -> b) -> a -> b
$ SourceSpan -> SourcePos
spanStart SourceSpan
ss) Ident
ident) (SourceType
valTy, NameKind
nameKind, NameVisibility
Undefined)
forall (m :: * -> *) a.
MonadState CheckState m =>
Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m a -> m a
bindNames Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
val
forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceSpan -> m a -> m a
warnAndRethrowWithPositionTC SourceSpan
ss forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
valTy SourceType
valTy'
forall (m :: * -> *) a.
MonadState CheckState m =>
Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m a -> m a
bindNames (forall k a. k -> a -> Map k a
M.singleton (forall a. QualifiedBy -> a -> Qualified a
Qualified (SourcePos -> QualifiedBy
BySourcePos forall a b. (a -> b) -> a -> b
$ SourceSpan -> SourcePos
spanStart SourceSpan
ss) Ident
ident) (SourceType
valTy', NameKind
nameKind, NameVisibility
Defined))
forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Declaration]
-> [Declaration]
-> Expr
-> (Expr -> m TypedValue')
-> m ([Declaration], TypedValue')
inferLetBinding ([Declaration]
seen forall a. [a] -> [a] -> [a]
++ [SourceAnn
-> Ident -> NameKind -> [Binder] -> [GuardedExpr] -> Declaration
ValueDecl SourceAnn
sa Ident
ident NameKind
nameKind [] [Expr -> GuardedExpr
MkUnguarded Expr
val']]) [Declaration]
rest Expr
ret Expr -> m TypedValue'
j
inferLetBinding [Declaration]
seen (BindingGroupDeclaration NonEmpty ((SourceAnn, Ident), NameKind, Expr)
ds : [Declaration]
rest) Expr
ret Expr -> m TypedValue'
j = do
ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
SplitBindingGroup [((SourceAnn, Ident), (Expr, SourceType))]
untyped [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
typed Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
Maybe ModuleName
-> [((SourceAnn, Ident), Expr)] -> m SplitBindingGroup
typeDictionaryForBindingGroup forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
NEL.toList forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((SourceAnn, Ident)
i, NameKind
_, Expr
v) -> ((SourceAnn, Ident)
i, Expr
v)) NonEmpty ((SourceAnn, Ident), NameKind, Expr)
ds
[((SourceAnn, Ident), (Expr, SourceType))]
ds1' <- forall (m :: * -> *) a b.
MonadError MultipleErrors m =>
[a] -> (a -> m b) -> m [b]
parU [((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))]
typed forall a b. (a -> b) -> a -> b
$ \((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))
e -> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
ModuleName
-> ((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
checkTypedBindingGroupElement ModuleName
moduleName ((SourceAnn, Ident),
(Expr, [(Text, SourceType)], SourceType, Bool))
e Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict
[((SourceAnn, Ident), (Expr, SourceType))]
ds2' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [((SourceAnn, Ident), (Expr, SourceType))]
untyped forall a b. (a -> b) -> a -> b
$ \((SourceAnn, Ident), (Expr, SourceType))
e -> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
((SourceAnn, Ident), (Expr, SourceType))
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m ((SourceAnn, Ident), (Expr, SourceType))
typeForBindingGroupElement ((SourceAnn, Ident), (Expr, SourceType))
e Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict
let ds' :: NonEmpty ((SourceAnn, Ident), NameKind, Expr)
ds' = forall a. [a] -> NonEmpty a
NEL.fromList [((SourceAnn, Ident)
ident, NameKind
Private, Expr
val') | ((SourceAnn, Ident)
ident, (Expr
val', SourceType
_)) <- [((SourceAnn, Ident), (Expr, SourceType))]
ds1' forall a. [a] -> [a] -> [a]
++ [((SourceAnn, Ident), (Expr, SourceType))]
ds2']
forall (m :: * -> *) a.
MonadState CheckState m =>
Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-> m a -> m a
bindNames Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
dict forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *). MonadState CheckState m => m ()
makeBindingGroupVisible
forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Declaration]
-> [Declaration]
-> Expr
-> (Expr -> m TypedValue')
-> m ([Declaration], TypedValue')
inferLetBinding ([Declaration]
seen forall a. [a] -> [a] -> [a]
++ [NonEmpty ((SourceAnn, Ident), NameKind, Expr) -> Declaration
BindingGroupDeclaration NonEmpty ((SourceAnn, Ident), NameKind, Expr)
ds']) [Declaration]
rest Expr
ret Expr -> m TypedValue'
j
inferLetBinding [Declaration]
_ [Declaration]
_ Expr
_ Expr -> m TypedValue'
_ = forall a. HasCallStack => String -> a
internalError String
"Invalid argument to inferLetBinding"
inferBinder
:: forall m
. (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> SourceType
-> Binder
-> m (M.Map Ident (SourceSpan, SourceType))
inferBinder :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder SourceType
_ Binder
NullBinder = forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
inferBinder SourceType
val (LiteralBinder SourceSpan
_ (StringLiteral PSString
_)) = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val SourceType
tyString forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
inferBinder SourceType
val (LiteralBinder SourceSpan
_ (CharLiteral Char
_)) = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val SourceType
tyChar forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
inferBinder SourceType
val (LiteralBinder SourceSpan
_ (NumericLiteral (Left Integer
_))) = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val SourceType
tyInt forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
inferBinder SourceType
val (LiteralBinder SourceSpan
_ (NumericLiteral (Right Double
_))) = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val SourceType
tyNumber forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
inferBinder SourceType
val (LiteralBinder SourceSpan
_ (BooleanLiteral Bool
_)) = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val SourceType
tyBoolean forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
inferBinder SourceType
val (VarBinder SourceSpan
ss Ident
name) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
M.singleton Ident
name (SourceSpan
ss, SourceType
val)
inferBinder SourceType
val (ConstructorBinder SourceSpan
ss Qualified (ProperName 'ConstructorName)
ctor [Binder]
binders) = do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ConstructorName)
ctor (Environment
-> Map
(Qualified (ProperName 'ConstructorName))
(DataDeclType, ProperName 'TypeName, SourceType, [Ident])
dataConstructors Environment
env) of
Just (DataDeclType
_, ProperName 'TypeName
_, SourceType
ty, [Ident]
_) -> do
(Expr
_, SourceType
fn) <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns (forall a. HasCallStack => String -> a
internalError String
"Data constructor types cannot contain constraints") SourceType
ty
SourceType
fn' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall a b. (a -> b) -> a -> b
$ SourceType
fn
let ([SourceType]
args, SourceType
ret) = forall a. Type a -> ([Type a], Type a)
peelArgs SourceType
fn'
expected :: Int
expected = forall (t :: * -> *) a. Foldable t => t a -> Int
length [SourceType]
args
actual :: Int
actual = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binder]
binders
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
expected forall a. Eq a => a -> a -> Bool
== Int
actual) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ConstructorName)
-> Int -> Int -> SimpleErrorMessage
IncorrectConstructorArity Qualified (ProperName 'ConstructorName)
ctor Int
expected Int
actual
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
ret SourceType
val
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder (forall a. [a] -> [a]
reverse [SourceType]
args) [Binder]
binders
Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'ConstructorName -> Name
DctorName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ConstructorName)
ctor
where
peelArgs :: Type a -> ([Type a], Type a)
peelArgs :: forall a. Type a -> ([Type a], Type a)
peelArgs = forall {a}. [Type a] -> Type a -> ([Type a], Type a)
go []
where
go :: [Type a] -> Type a -> ([Type a], Type a)
go [Type a]
args (TypeApp a
_ (TypeApp a
_ Type a
fn Type a
arg) Type a
ret) | forall a b. Type a -> Type b -> Bool
eqType Type a
fn SourceType
tyFunction = [Type a] -> Type a -> ([Type a], Type a)
go (Type a
arg forall a. a -> [a] -> [a]
: [Type a]
args) Type a
ret
go [Type a]
args Type a
ret = ([Type a]
args, Type a
ret)
inferBinder SourceType
val (LiteralBinder SourceSpan
_ (ObjectLiteral [(PSString, Binder)]
props)) = do
SourceType
row <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind (SourceType -> SourceType
kindRow SourceType
kindType)
SourceType
rest <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind (SourceType -> SourceType
kindRow SourceType
kindType)
Map Ident (SourceSpan, SourceType)
m1 <- SourceType
-> SourceType
-> [(PSString, Binder)]
-> m (Map Ident (SourceSpan, SourceType))
inferRowProperties SourceType
row SourceType
rest [(PSString, Binder)]
props
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord SourceType
row)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident (SourceSpan, SourceType)
m1
where
inferRowProperties :: SourceType -> SourceType -> [(PSString, Binder)] -> m (M.Map Ident (SourceSpan, SourceType))
inferRowProperties :: SourceType
-> SourceType
-> [(PSString, Binder)]
-> m (Map Ident (SourceSpan, SourceType))
inferRowProperties SourceType
nrow SourceType
row [] = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
nrow SourceType
row forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
inferRowProperties SourceType
nrow SourceType
row ((PSString
name, Binder
binder):[(PSString, Binder)]
binders) = do
SourceType
propTy <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
Map Ident (SourceSpan, SourceType)
m1 <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder SourceType
propTy Binder
binder
Map Ident (SourceSpan, SourceType)
m2 <- SourceType
-> SourceType
-> [(PSString, Binder)]
-> m (Map Ident (SourceSpan, SourceType))
inferRowProperties SourceType
nrow (Label -> SourceType -> SourceType -> SourceType
srcRCons (PSString -> Label
Label PSString
name) SourceType
propTy SourceType
row) [(PSString, Binder)]
binders
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map Ident (SourceSpan, SourceType)
m1 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map Ident (SourceSpan, SourceType)
m2
inferBinder SourceType
val (LiteralBinder SourceSpan
_ (ArrayLiteral [Binder]
binders)) = do
SourceType
el <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
Map Ident (SourceSpan, SourceType)
m1 <- forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder SourceType
el) [Binder]
binders
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyArray SourceType
el)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident (SourceSpan, SourceType)
m1
inferBinder SourceType
val (NamedBinder SourceSpan
ss Ident
name Binder
binder) =
forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceSpan -> m a -> m a
warnAndRethrowWithPositionTC SourceSpan
ss forall a b. (a -> b) -> a -> b
$ do
Map Ident (SourceSpan, SourceType)
m <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder SourceType
val Binder
binder
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Ident
name (SourceSpan
ss, SourceType
val) Map Ident (SourceSpan, SourceType)
m
inferBinder SourceType
val (PositionedBinder SourceSpan
pos [Comment]
_ Binder
binder) =
forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceSpan -> m a -> m a
warnAndRethrowWithPositionTC SourceSpan
pos forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder SourceType
val Binder
binder
inferBinder SourceType
val (TypedBinder SourceType
ty Binder
binder) = do
(SourceType
elabTy, SourceType
kind) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
kindOf SourceType
ty
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
ty SourceType
kind
SourceType
ty1 <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall a b. (a -> b) -> a -> b
$ SourceType
elabTy
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
val SourceType
ty1
forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder SourceType
ty1 Binder
binder
inferBinder SourceType
_ OpBinder{} =
forall a. HasCallStack => String -> a
internalError String
"OpBinder should have been desugared before inferBinder"
inferBinder SourceType
_ BinaryNoParensBinder{} =
forall a. HasCallStack => String -> a
internalError String
"BinaryNoParensBinder should have been desugared before inferBinder"
inferBinder SourceType
_ ParensInBinder{} =
forall a. HasCallStack => String -> a
internalError String
"ParensInBinder should have been desugared before inferBinder"
binderRequiresMonotype :: Binder -> Bool
binderRequiresMonotype :: Binder -> Bool
binderRequiresMonotype Binder
NullBinder = Bool
False
binderRequiresMonotype (VarBinder SourceSpan
_ Ident
_) = Bool
False
binderRequiresMonotype (NamedBinder SourceSpan
_ Ident
_ Binder
b) = Binder -> Bool
binderRequiresMonotype Binder
b
binderRequiresMonotype (PositionedBinder SourceSpan
_ [Comment]
_ Binder
b) = Binder -> Bool
binderRequiresMonotype Binder
b
binderRequiresMonotype (TypedBinder SourceType
ty Binder
b) = forall a. Type a -> Bool
isMonoType SourceType
ty Bool -> Bool -> Bool
|| Binder -> Bool
binderRequiresMonotype Binder
b
binderRequiresMonotype Binder
_ = Bool
True
instantiateForBinders
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> [Expr]
-> [CaseAlternative]
-> m ([Expr], [SourceType])
instantiateForBinders :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Expr] -> [CaseAlternative] -> m ([Expr], [SourceType])
instantiateForBinders [Expr]
vals [CaseAlternative]
cas = forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Expr
val Bool
inst -> do
TypedValue' Bool
_ Expr
val' SourceType
ty <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
val
if Bool
inst
then forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns Expr
val' SourceType
ty
else forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
val', SourceType
ty)) [Expr]
vals [Bool]
shouldInstantiate
where
shouldInstantiate :: [Bool]
shouldInstantiate :: [Bool]
shouldInstantiate = forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binder -> Bool
binderRequiresMonotype) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [[a]] -> [[a]]
transpose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map CaseAlternative -> [Binder]
caseAlternativeBinders forall a b. (a -> b) -> a -> b
$ [CaseAlternative]
cas
checkBinders
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> [SourceType]
-> SourceType
-> [CaseAlternative]
-> m [CaseAlternative]
checkBinders :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[SourceType]
-> SourceType -> [CaseAlternative] -> m [CaseAlternative]
checkBinders [SourceType]
_ SourceType
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
checkBinders [SourceType]
nvals SourceType
ret (CaseAlternative [Binder]
binders [GuardedExpr]
result : [CaseAlternative]
bs) = do
forall e (m :: * -> *). MonadError e m => e -> Bool -> m ()
guardWith (SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Maybe Ident -> SimpleErrorMessage
OverlappingArgNames forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$
let ns :: [Ident]
ns = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Binder -> [Ident]
binderNames [Binder]
binders in forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Ord a => [a] -> [a]
ordNub [Ident]
ns) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
ns
Map Ident (SourceSpan, SourceType)
m1 <- forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder [SourceType]
nvals [Binder]
binders
CaseAlternative
r <- forall (m :: * -> *) a.
MonadState CheckState m =>
[(SourceSpan, Ident, SourceType, NameVisibility)] -> m a -> m a
bindLocalVariables [ (SourceSpan
ss, Ident
name, SourceType
ty, NameVisibility
Defined) | (Ident
name, (SourceSpan
ss, SourceType
ty)) <- forall k a. Map k a -> [(k, a)]
M.toList Map Ident (SourceSpan, SourceType)
m1 ] forall a b. (a -> b) -> a -> b
$
[Binder] -> [GuardedExpr] -> CaseAlternative
CaseAlternative [Binder]
binders forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [GuardedExpr]
result (\GuardedExpr
ge -> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
GuardedExpr -> SourceType -> m GuardedExpr
checkGuardedRhs GuardedExpr
ge SourceType
ret)
[CaseAlternative]
rs <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[SourceType]
-> SourceType -> [CaseAlternative] -> m [CaseAlternative]
checkBinders [SourceType]
nvals SourceType
ret [CaseAlternative]
bs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CaseAlternative
r forall a. a -> [a] -> [a]
: [CaseAlternative]
rs
checkGuardedRhs
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> GuardedExpr
-> SourceType
-> m GuardedExpr
checkGuardedRhs :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
GuardedExpr -> SourceType -> m GuardedExpr
checkGuardedRhs (GuardedExpr [] Expr
rhs) SourceType
ret = do
Expr
rhs' <- Bool -> Expr -> SourceType -> Expr
TypedValue Bool
True forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
rhs SourceType
ret) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ret
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Guard] -> Expr -> GuardedExpr
GuardedExpr [] Expr
rhs'
checkGuardedRhs (GuardedExpr (ConditionGuard Expr
cond : [Guard]
guards) Expr
rhs) SourceType
ret = do
TypedValue'
cond' <- forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint ErrorMessageHint
ErrorCheckingGuard forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
cond SourceType
tyBoolean
GuardedExpr [Guard]
guards' Expr
rhs' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
GuardedExpr -> SourceType -> m GuardedExpr
checkGuardedRhs ([Guard] -> Expr -> GuardedExpr
GuardedExpr [Guard]
guards Expr
rhs) SourceType
ret
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Guard] -> Expr -> GuardedExpr
GuardedExpr (Expr -> Guard
ConditionGuard (TypedValue' -> Expr
tvToExpr TypedValue'
cond') forall a. a -> [a] -> [a]
: [Guard]
guards') Expr
rhs'
checkGuardedRhs (GuardedExpr (PatternGuard Binder
binder Expr
expr : [Guard]
guards) Expr
rhs) SourceType
ret = do
tv :: TypedValue'
tv@(TypedValue' Bool
_ Expr
_ SourceType
ty) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
expr
Map Ident (SourceSpan, SourceType)
variables <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceType -> Binder -> m (Map Ident (SourceSpan, SourceType))
inferBinder SourceType
ty Binder
binder
GuardedExpr [Guard]
guards' Expr
rhs' <- forall (m :: * -> *) a.
MonadState CheckState m =>
[(SourceSpan, Ident, SourceType, NameVisibility)] -> m a -> m a
bindLocalVariables [ (SourceSpan
ss, Ident
name, SourceType
bty, NameVisibility
Defined)
| (Ident
name, (SourceSpan
ss, SourceType
bty)) <- forall k a. Map k a -> [(k, a)]
M.toList Map Ident (SourceSpan, SourceType)
variables
] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
GuardedExpr -> SourceType -> m GuardedExpr
checkGuardedRhs ([Guard] -> Expr -> GuardedExpr
GuardedExpr [Guard]
guards Expr
rhs) SourceType
ret
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Guard] -> Expr -> GuardedExpr
GuardedExpr (Binder -> Expr -> Guard
PatternGuard Binder
binder (TypedValue' -> Expr
tvToExpr TypedValue'
tv) forall a. a -> [a] -> [a]
: [Guard]
guards') Expr
rhs'
check
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> SourceType
-> m TypedValue'
check :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val SourceType
ty = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> ErrorMessageHint -> m a -> m a
withErrorMessageHint' Expr
val (Expr -> SourceType -> ErrorMessageHint
ErrorCheckingType Expr
val SourceType
ty) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check' Expr
val SourceType
ty
check'
:: forall m
. (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> SourceType
-> m TypedValue'
check' :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check' Expr
val (ForAll SourceAnn
ann TypeVarVisibility
vis Text
ident Maybe SourceType
mbK SourceType
ty Maybe SkolemScope
_) = do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
Maybe ModuleName
mn <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Maybe ModuleName
checkCurrentModule
SkolemScope
scope <- forall (m :: * -> *). MonadState CheckState m => m SkolemScope
newSkolemScope
Int
sko <- forall (m :: * -> *). MonadState CheckState m => m Int
newSkolemConstant
let ss :: SourceAnn
ss = case Expr
val of
PositionedValue SourceSpan
pos [Comment]
c Expr
_ -> (SourceSpan
pos, [Comment]
c)
Expr
_ -> SourceAnn
NullSourceAnn
sk :: SourceType
sk = forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ss Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope SourceType
ty
skVal :: Expr
skVal
| Just (SourceType, TypeKind)
_ <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a. QualifiedBy -> a -> Qualified a
Qualified (Maybe ModuleName -> QualifiedBy
byMaybeModuleName Maybe ModuleName
mn) (forall (a :: ProperNameType). Text -> ProperName a
ProperName Text
ident)) forall a b. (a -> b) -> a -> b
$ Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
types Environment
env =
SourceAnn
-> Text -> Maybe SourceType -> Int -> SkolemScope -> Expr -> Expr
skolemizeTypesInValue SourceAnn
ss Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope Expr
val
| Bool
otherwise = Expr
val
Expr
val' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
skVal SourceType
sk
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
val' (forall a.
a
-> TypeVarVisibility
-> Text
-> Maybe (Type a)
-> Type a
-> Maybe SkolemScope
-> Type a
ForAll SourceAnn
ann TypeVarVisibility
vis Text
ident Maybe SourceType
mbK SourceType
ty (forall a. a -> Maybe a
Just SkolemScope
scope))
check' Expr
val t :: SourceType
t@(ConstrainedType SourceAnn
_ con :: SourceConstraint
con@(Constraint SourceAnn
_ cls :: Qualified (ProperName 'ClassName)
cls@(Qualified QualifiedBy
_ (ProperName Text
className)) [SourceType]
_ [SourceType]
_ Maybe ConstraintData
_) SourceType
ty) = do
TypeClassData{ Bool
typeClassIsEmpty :: TypeClassData -> Bool
typeClassIsEmpty :: Bool
typeClassIsEmpty } <- forall (m :: * -> *).
MonadState CheckState m =>
Qualified (ProperName 'ClassName) -> m TypeClassData
lookupTypeClass Qualified (ProperName 'ClassName)
cls
Ident
dictName <- if Bool
typeClassIsEmpty then forall (f :: * -> *) a. Applicative f => a -> f a
pure Ident
UnusedIdent else forall (m :: * -> *). MonadSupply m => Text -> m Ident
freshIdent (Text
"dict" forall a. Semigroup a => a -> a -> a
<> Text
className)
[NamedDict]
dicts <- forall (m :: * -> *).
MonadState CheckState m =>
[(Qualified (ProperName 'ClassName), Integer)]
-> Qualified Ident -> SourceConstraint -> m [NamedDict]
newDictionaries [] (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos Ident
dictName) SourceConstraint
con
TypedValue'
val' <- forall (m :: * -> *) a. MonadState CheckState m => m a -> m a
withBindingGroupVisible forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadState CheckState m =>
[NamedDict] -> m a -> m a
withTypeClassDictionaries [NamedDict]
dicts forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val SourceType
ty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Binder -> Expr -> Expr
Abs (SourceSpan -> Ident -> Binder
VarBinder SourceSpan
nullSourceSpan Ident
dictName) (TypedValue' -> Expr
tvToExpr TypedValue'
val')) SourceType
t
check' Expr
val u :: SourceType
u@(TUnknown SourceAnn
_ Int
_) = do
val' :: TypedValue'
val'@(TypedValue' Bool
_ Expr
_ SourceType
ty) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
val
(Expr
val'', SourceType
ty') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns (TypedValue' -> Expr
tvToExpr TypedValue'
val') SourceType
ty
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
ty' SourceType
u
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
val'' SourceType
ty'
check' v :: Expr
v@(Literal SourceSpan
_ (NumericLiteral (Left Integer
_))) SourceType
t | SourceType
t forall a. Eq a => a -> a -> Bool
== SourceType
tyInt =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
t
check' v :: Expr
v@(Literal SourceSpan
_ (NumericLiteral (Right Double
_))) SourceType
t | SourceType
t forall a. Eq a => a -> a -> Bool
== SourceType
tyNumber =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
t
check' v :: Expr
v@(Literal SourceSpan
_ (StringLiteral PSString
_)) SourceType
t | SourceType
t forall a. Eq a => a -> a -> Bool
== SourceType
tyString =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
t
check' v :: Expr
v@(Literal SourceSpan
_ (CharLiteral Char
_)) SourceType
t | SourceType
t forall a. Eq a => a -> a -> Bool
== SourceType
tyChar =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
t
check' v :: Expr
v@(Literal SourceSpan
_ (BooleanLiteral Bool
_)) SourceType
t | SourceType
t forall a. Eq a => a -> a -> Bool
== SourceType
tyBoolean =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v SourceType
t
check' (Literal SourceSpan
ss (ArrayLiteral [Expr]
vals)) t :: SourceType
t@(TypeApp SourceAnn
_ SourceType
a SourceType
ty) = do
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
a SourceType
tyArray
Expr
array <- SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Literal a
ArrayLiteral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Expr]
vals (forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
`check` SourceType
ty)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
array SourceType
t
check' (Abs Binder
binder Expr
ret) ty :: SourceType
ty@(TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
t SourceType
argTy) SourceType
retTy)
| VarBinder SourceSpan
ss Ident
arg <- Binder
binder = do
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
t SourceType
tyFunction
TypedValue'
ret' <- forall (m :: * -> *) a. MonadState CheckState m => m a -> m a
withBindingGroupVisible forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadState CheckState m =>
[(SourceSpan, Ident, SourceType, NameVisibility)] -> m a -> m a
bindLocalVariables [(SourceSpan
ss, Ident
arg, SourceType
argTy, NameVisibility
Defined)] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
ret SourceType
retTy
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Binder -> Expr -> Expr
Abs (SourceSpan -> Ident -> Binder
VarBinder SourceSpan
ss Ident
arg) (TypedValue' -> Expr
tvToExpr TypedValue'
ret')) SourceType
ty
| Bool
otherwise = forall a. HasCallStack => String -> a
internalError String
"Binder was not desugared"
check' (App Expr
f Expr
arg) SourceType
ret = do
f' :: TypedValue'
f'@(TypedValue' Bool
_ Expr
_ SourceType
ft) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
f
(SourceType
retTy, Expr
app) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication (TypedValue' -> Expr
tvToExpr TypedValue'
f') SourceType
ft Expr
arg
Expr -> Expr
elaborate <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
retTy SourceType
ret
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> Expr
elaborate Expr
app) SourceType
ret
check' v :: Expr
v@(Var SourceSpan
_ Qualified Ident
var) SourceType
ty = do
forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
Qualified Ident -> m ()
checkVisibility Qualified Ident
var
SourceType
repl <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
Qualified Ident -> m SourceType
lookupVariable forall a b. (a -> b) -> a -> b
$ Qualified Ident
var
SourceType
ty' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall a b. (a -> b) -> a -> b
$ SourceType
ty
Expr -> Expr
elaborate <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
repl SourceType
ty'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> Expr
elaborate Expr
v) SourceType
ty'
check' (DeferredDictionary Qualified (ProperName 'ClassName)
className [SourceType]
tys) SourceType
ty = do
InstanceContext
dicts <- forall (m :: * -> *). MonadState CheckState m => m InstanceContext
getTypeClassDictionaries
[ErrorMessageHint]
hints <- forall (m :: * -> *).
MonadState CheckState m =>
m [ErrorMessageHint]
getHints
SourceConstraint
con <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceConstraint -> m SourceConstraint
checkConstraint (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
className [] [SourceType]
tys forall a. Maybe a
Nothing)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
False
(SourceConstraint -> InstanceContext -> [ErrorMessageHint] -> Expr
TypeClassDictionary SourceConstraint
con InstanceContext
dicts [ErrorMessageHint]
hints)
SourceType
ty
check' (TypedValue Bool
checkType Expr
val SourceType
ty1) SourceType
ty2 = do
ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
(([(Text, SourceType)]
args, SourceType
elabTy1), SourceType
kind1) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (([(Text, SourceType)], SourceType), SourceType)
kindOfWithScopedVars SourceType
ty1
(SourceType
elabTy2, SourceType
kind2) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
kindOf SourceType
ty2
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds' SourceType
kind1 SourceType
kind2
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
ty1 SourceType
kind1
SourceType
ty1' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall a b. (a -> b) -> a -> b
$ SourceType
elabTy1
SourceType
ty2' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards forall a b. (a -> b) -> a -> b
$ SourceType
elabTy2
Expr -> Expr
elaborate <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
ty1' SourceType
ty2'
Expr
val' <- if Bool
checkType
then forall (m :: * -> *) a.
(MonadState CheckState m, MonadWriter MultipleErrors m) =>
ModuleName -> [(Text, SourceType)] -> m a -> m a
withScopedTypeVars ModuleName
moduleName [(Text, SourceType)]
args forall a b. (a -> b) -> a -> b
$ TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val SourceType
ty1'
else forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
val
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Bool -> Expr -> SourceType -> Expr
TypedValue Bool
checkType (Expr -> Expr
elaborate Expr
val') SourceType
ty1') SourceType
ty2'
check' (Case [Expr]
vals [CaseAlternative]
binders) SourceType
ret = do
([Expr]
vals', [SourceType]
ts) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Expr] -> [CaseAlternative] -> m ([Expr], [SourceType])
instantiateForBinders [Expr]
vals [CaseAlternative]
binders
[CaseAlternative]
binders' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[SourceType]
-> SourceType -> [CaseAlternative] -> m [CaseAlternative]
checkBinders [SourceType]
ts SourceType
ret [CaseAlternative]
binders
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True ([Expr] -> [CaseAlternative] -> Expr
Case [Expr]
vals' [CaseAlternative]
binders') SourceType
ret
check' (IfThenElse Expr
cond Expr
th Expr
el) SourceType
ty = do
Expr
cond' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
cond SourceType
tyBoolean
Expr
th' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
th SourceType
ty
Expr
el' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
el SourceType
ty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> Expr -> Expr -> Expr
IfThenElse Expr
cond' Expr
th' Expr
el') SourceType
ty
check' e :: Expr
e@(Literal SourceSpan
ss (ObjectLiteral [(PSString, Expr)]
ps)) t :: SourceType
t@(TypeApp SourceAnn
_ SourceType
obj SourceType
row) | SourceType
obj forall a. Eq a => a -> a -> Bool
== SourceType
tyRecord = do
forall (m :: * -> *).
MonadError MultipleErrors m =>
[(PSString, Expr)] -> m ()
ensureNoDuplicateProperties [(PSString, Expr)]
ps
[(PSString, Expr)]
ps' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr
-> [(PSString, Expr)] -> SourceType -> Bool -> m [(PSString, Expr)]
checkProperties Expr
e [(PSString, Expr)]
ps SourceType
row Bool
False
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
ss (forall a. [(PSString, a)] -> Literal a
ObjectLiteral [(PSString, Expr)]
ps')) SourceType
t
check' (DerivedInstancePlaceholder Qualified (ProperName 'ClassName)
name InstanceDerivationStrategy
strategy) SourceType
t = do
Expr
d <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
MonadSupply m, MonadWriter MultipleErrors m) =>
SourceType
-> Qualified (ProperName 'ClassName)
-> InstanceDerivationStrategy
-> m Expr
deriveInstance SourceType
t Qualified (ProperName 'ClassName)
name InstanceDerivationStrategy
strategy
Expr
d' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check' Expr
d SourceType
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
d' SourceType
t
check' e :: Expr
e@(ObjectUpdate Expr
obj [(PSString, Expr)]
ps) t :: SourceType
t@(TypeApp SourceAnn
_ SourceType
o SourceType
row) | SourceType
o forall a. Eq a => a -> a -> Bool
== SourceType
tyRecord = do
forall (m :: * -> *).
MonadError MultipleErrors m =>
[(PSString, Expr)] -> m ()
ensureNoDuplicateProperties [(PSString, Expr)]
ps
let ([RowListItem SourceAnn]
propsToCheck, SourceType
rest) = forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
row
([RowListItem SourceAnn]
removedProps, [RowListItem SourceAnn]
remainingProps) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(RowListItem SourceAnn
_ Label
p SourceType
_) -> Label
p forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map (PSString -> Label
Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(PSString, Expr)]
ps) [RowListItem SourceAnn]
propsToCheck
[RowListItem SourceAnn]
us <- forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Label -> SourceType -> RowListItem SourceAnn
srcRowListItem (forall a b. (a -> b) -> [a] -> [b]
map forall a. RowListItem a -> Label
rowListLabel [RowListItem SourceAnn]
removedProps) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(PSString, Expr)]
ps) (forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType)
Expr
obj' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
obj (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
us forall a. [a] -> [a] -> [a]
++ [RowListItem SourceAnn]
remainingProps, SourceType
rest)))
[(PSString, Expr)]
ps' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr
-> [(PSString, Expr)] -> SourceType -> Bool -> m [(PSString, Expr)]
checkProperties Expr
e [(PSString, Expr)]
ps SourceType
row Bool
True
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> [(PSString, Expr)] -> Expr
ObjectUpdate Expr
obj' [(PSString, Expr)]
ps') SourceType
t
check' (Accessor PSString
prop Expr
val) SourceType
ty = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (Expr -> PSString -> ErrorMessageHint
ErrorCheckingAccessor Expr
val PSString
prop) forall a b. (a -> b) -> a -> b
$ do
SourceType
rest <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind (SourceType -> SourceType
kindRow SourceType
kindType)
Expr
val' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
val (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord (Label -> SourceType -> SourceType -> SourceType
srcRCons (PSString -> Label
Label PSString
prop) SourceType
ty SourceType
rest))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (PSString -> Expr -> Expr
Accessor PSString
prop Expr
val') SourceType
ty
check' v :: Expr
v@(Constructor SourceSpan
_ Qualified (ProperName 'ConstructorName)
c) SourceType
ty = do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ConstructorName)
c (Environment
-> Map
(Qualified (ProperName 'ConstructorName))
(DataDeclType, ProperName 'TypeName, SourceType, [Ident])
dataConstructors Environment
env) of
Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'ConstructorName -> Name
DctorName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ConstructorName)
c
Just (DataDeclType
_, ProperName 'TypeName
_, SourceType
ty1, [Ident]
_) -> do
SourceType
repl <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall a b. (a -> b) -> a -> b
$ SourceType
ty1
SourceType
ty' <- forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall a b. (a -> b) -> a -> b
$ SourceType
ty
Expr -> Expr
elaborate <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
repl SourceType
ty'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> Expr
elaborate Expr
v) SourceType
ty'
check' (Let WhereProvenance
w [Declaration]
ds Expr
val) SourceType
ty = do
([Declaration]
ds', TypedValue'
val') <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
[Declaration]
-> [Declaration]
-> Expr
-> (Expr -> m TypedValue')
-> m ([Declaration], TypedValue')
inferLetBinding [] [Declaration]
ds Expr
val (forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
`check` SourceType
ty)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (WhereProvenance -> [Declaration] -> Expr -> Expr
Let WhereProvenance
w [Declaration]
ds' (TypedValue' -> Expr
tvToExpr TypedValue'
val')) SourceType
ty
check' Expr
val kt :: SourceType
kt@(KindedType SourceAnn
_ SourceType
ty SourceType
kind) = do
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
ty SourceType
kind
Expr
val' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check' Expr
val SourceType
ty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
val' SourceType
kt
check' (PositionedValue SourceSpan
pos [Comment]
c Expr
val) SourceType
ty = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m) =>
SourceSpan -> m a -> m a
warnAndRethrowWithPositionTC SourceSpan
pos forall a b. (a -> b) -> a -> b
$ do
TypedValue' Bool
t Expr
v SourceType
ty' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check' Expr
val SourceType
ty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
t (SourceSpan -> [Comment] -> Expr -> Expr
PositionedValue SourceSpan
pos [Comment]
c Expr
v) SourceType
ty'
check' Expr
val SourceType
ty = do
TypedValue' Bool
_ Expr
val' SourceType
ty' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
val
Expr -> Expr
elaborate <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
ty' SourceType
ty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True (Expr -> Expr
elaborate Expr
val') SourceType
ty
checkProperties
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> [(PSString, Expr)]
-> SourceType
-> Bool
-> m [(PSString, Expr)]
checkProperties :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr
-> [(PSString, Expr)] -> SourceType -> Bool -> m [(PSString, Expr)]
checkProperties Expr
expr [(PSString, Expr)]
ps SourceType
row Bool
lax = [(PSString, TypedValue')] -> [(PSString, Expr)]
convert forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(PSString, Expr)]
-> [(Label, SourceType)]
-> SourceType
-> m [(PSString, TypedValue')]
go [(PSString, Expr)]
ps (forall {a}. RowListItem a -> (Label, Type a)
toRowPair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RowListItem SourceAnn]
ts') SourceType
r' where
convert :: [(PSString, TypedValue')] -> [(PSString, Expr)]
convert = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypedValue' -> Expr
tvToExpr)
([RowListItem SourceAnn]
ts', SourceType
r') = forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
row
toRowPair :: RowListItem a -> (Label, Type a)
toRowPair (RowListItem a
_ Label
lbl Type a
ty) = (Label
lbl, Type a
ty)
go :: [(PSString, Expr)]
-> [(Label, SourceType)]
-> SourceType
-> m [(PSString, TypedValue')]
go [] [] (REmptyKinded SourceAnn
_ Maybe SourceType
_) = forall (m :: * -> *) a. Monad m => a -> m a
return []
go [] [] u :: SourceType
u@(TUnknown SourceAnn
_ Int
_)
| Bool
lax = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
u SourceType
srcREmpty
forall (m :: * -> *) a. Monad m => a -> m a
return []
go [] [] Skolem{} | Bool
lax = forall (m :: * -> *) a. Monad m => a -> m a
return []
go [] ((Label
p, SourceType
_): [(Label, SourceType)]
_) SourceType
_ | Bool
lax = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Label -> SimpleErrorMessage
PropertyIsMissing Label
p
go ((PSString
p,Expr
_):[(PSString, Expr)]
_) [] (REmptyKinded SourceAnn
_ Maybe SourceType
_) = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Label -> SimpleErrorMessage
AdditionalProperty forall a b. (a -> b) -> a -> b
$ PSString -> Label
Label PSString
p
go ((PSString
p,Expr
v):[(PSString, Expr)]
ps') [(Label, SourceType)]
ts SourceType
r =
case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (PSString -> Label
Label PSString
p) [(Label, SourceType)]
ts of
Maybe SourceType
Nothing -> do
(Expr
v', SourceType
ty) <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m (Expr, SourceType)
inferWithinRecord Expr
v
SourceType
rest <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind (SourceType -> SourceType
kindRow SourceType
kindType)
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
r (Label -> SourceType -> SourceType -> SourceType
srcRCons (PSString -> Label
Label PSString
p) SourceType
ty SourceType
rest)
[(PSString, TypedValue')]
ps'' <- [(PSString, Expr)]
-> [(Label, SourceType)]
-> SourceType
-> m [(PSString, TypedValue')]
go [(PSString, Expr)]
ps' [(Label, SourceType)]
ts SourceType
rest
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (PSString
p, Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
v' SourceType
ty) forall a. a -> [a] -> [a]
: [(PSString, TypedValue')]
ps''
Just SourceType
ty -> do
TypedValue'
v' <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
v SourceType
ty
[(PSString, TypedValue')]
ps'' <- [(PSString, Expr)]
-> [(Label, SourceType)]
-> SourceType
-> m [(PSString, TypedValue')]
go [(PSString, Expr)]
ps' (forall a. Eq a => a -> [a] -> [a]
delete (PSString -> Label
Label PSString
p, SourceType
ty) [(Label, SourceType)]
ts) SourceType
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (PSString
p, TypedValue'
v') forall a. a -> [a] -> [a]
: [(PSString, TypedValue')]
ps''
go [(PSString, Expr)]
_ [(Label, SourceType)]
_ SourceType
_ = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Expr -> SourceType -> SimpleErrorMessage
ExprDoesNotHaveType Expr
expr (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord SourceType
row)
checkFunctionApplication
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> SourceType
-> Expr
-> m (SourceType, Expr)
checkFunctionApplication :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication Expr
fn SourceType
fnTy Expr
arg = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> ErrorMessageHint -> m a -> m a
withErrorMessageHint' Expr
fn (Expr -> SourceType -> Expr -> ErrorMessageHint
ErrorInApplication Expr
fn SourceType
fnTy Expr
arg) forall a b. (a -> b) -> a -> b
$ do
Substitution
subst <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication' Expr
fn (Substitution -> SourceType -> SourceType
substituteType Substitution
subst SourceType
fnTy) Expr
arg
checkFunctionApplication'
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> SourceType
-> Expr
-> m (SourceType, Expr)
checkFunctionApplication' :: forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication' Expr
fn (TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
tyFunction' SourceType
argTy) SourceType
retTy) Expr
arg = do
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
tyFunction' SourceType
tyFunction
Expr
arg' <- TypedValue' -> Expr
tvToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> m TypedValue'
check Expr
arg SourceType
argTy
forall (m :: * -> *) a. Monad m => a -> m a
return (SourceType
retTy, Expr -> Expr -> Expr
App Expr
fn Expr
arg')
checkFunctionApplication' Expr
fn (ForAll SourceAnn
_ TypeVarVisibility
_ Text
ident Maybe SourceType
mbK SourceType
ty Maybe SkolemScope
_) Expr
arg = do
SourceType
u <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError Text
"Unelaborated forall") forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind Maybe SourceType
mbK
forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
SourceType -> Text -> m ()
insertUnkName' SourceType
u Text
ident
let replaced :: SourceType
replaced = forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
ident SourceType
u SourceType
ty
forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication Expr
fn SourceType
replaced Expr
arg
checkFunctionApplication' Expr
fn (KindedType SourceAnn
_ SourceType
ty SourceType
_) Expr
arg =
forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication Expr
fn SourceType
ty Expr
arg
checkFunctionApplication' Expr
fn (ConstrainedType SourceAnn
_ SourceConstraint
con SourceType
fnTy) Expr
arg = do
InstanceContext
dicts <- forall (m :: * -> *). MonadState CheckState m => m InstanceContext
getTypeClassDictionaries
[ErrorMessageHint]
hints <- forall (m :: * -> *).
MonadState CheckState m =>
m [ErrorMessageHint]
getHints
forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> SourceType -> Expr -> m (SourceType, Expr)
checkFunctionApplication' (Expr -> Expr -> Expr
App Expr
fn (SourceConstraint -> InstanceContext -> [ErrorMessageHint] -> Expr
TypeClassDictionary SourceConstraint
con InstanceContext
dicts [ErrorMessageHint]
hints)) SourceType
fnTy Expr
arg
checkFunctionApplication' Expr
fn SourceType
fnTy dict :: Expr
dict@TypeClassDictionary{} =
forall (m :: * -> *) a. Monad m => a -> m a
return (SourceType
fnTy, Expr -> Expr -> Expr
App Expr
fn Expr
dict)
checkFunctionApplication' Expr
fn SourceType
u Expr
arg = do
tv :: TypedValue'
tv@(TypedValue' Bool
_ Expr
_ SourceType
ty) <- do
TypedValue' Bool
_ Expr
arg' SourceType
t <- forall (m :: * -> *).
(MonadSupply m, MonadState CheckState m,
MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
Expr -> m TypedValue'
infer Expr
arg
(Expr
arg'', SourceType
t') <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> SourceType -> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns Expr
arg' SourceType
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> SourceType -> TypedValue'
TypedValue' Bool
True Expr
arg'' SourceType
t'
SourceType
ret <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kindType
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
u (SourceType -> SourceType -> SourceType
function SourceType
ty SourceType
ret)
forall (m :: * -> *) a. Monad m => a -> m a
return (SourceType
ret, Expr -> Expr -> Expr
App Expr
fn (TypedValue' -> Expr
tvToExpr TypedValue'
tv))
ensureNoDuplicateProperties :: (MonadError MultipleErrors m) => [(PSString, Expr)] -> m ()
ensureNoDuplicateProperties :: forall (m :: * -> *).
MonadError MultipleErrors m =>
[(PSString, Expr)] -> m ()
ensureNoDuplicateProperties [(PSString, Expr)]
ps =
let ls :: [PSString]
ls = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(PSString, Expr)]
ps in
case [PSString]
ls forall a. Eq a => [a] -> [a] -> [a]
\\ forall a. Ord a => [a] -> [a]
ordNub [PSString]
ls of
PSString
l : [PSString]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Label -> Maybe Expr -> SimpleErrorMessage
DuplicateLabel (PSString -> Label
Label PSString
l) forall a. Maybe a
Nothing
[PSString]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
isInternal :: Expr -> Bool
isInternal :: Expr -> Bool
isInternal = \case
PositionedValue SourceSpan
_ [Comment]
_ Expr
v -> Expr -> Bool
isInternal Expr
v
TypedValue Bool
_ Expr
v SourceType
_ -> Expr -> Bool
isInternal Expr
v
Constructor SourceSpan
_ (Qualified QualifiedBy
_ ProperName 'ConstructorName
name) -> forall (a :: ProperNameType). ProperName a -> Bool
isDictTypeName ProperName 'ConstructorName
name
DerivedInstancePlaceholder{} -> Bool
True
Expr
_ -> Bool
False
withErrorMessageHint'
:: (MonadState CheckState m, MonadError MultipleErrors m)
=> Expr
-> ErrorMessageHint
-> m a
-> m a
withErrorMessageHint' :: forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
Expr -> ErrorMessageHint -> m a -> m a
withErrorMessageHint' Expr
expr = if Expr -> Bool
isInternal Expr
expr then forall a b. a -> b -> a
const forall a. a -> a
id else forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint