-- |
-- This module implements the type checker
--
module Language.PureScript.TypeChecker.Types
  ( BindingGroupType(..)
  , typesOf
  , checkTypeKind
  ) where

{-
  The following functions represent the corresponding type checking judgements:

    infer
      Synthesize a type for a value

    check
      Check a value has a given type

    checkProperties
      Check an object with a given type contains specified properties

    checkFunctionApplication
      Check a function of a given type returns a value of another type when applied to its arguments
-}

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, 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)

-- | The result of a successful type check.
data TypedValue' = TypedValue' Bool Expr SourceType

-- | Convert an type checked value into an expression.
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

-- | Lookup data about a type class in the @Environment@
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)

-- | Infer the types of multiple mutually-recursive values, and return elaborated values including
-- type class dictionaries and type annotations.
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
      -- Replace type class dictionary placeholders with actual dictionaries
      (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
      -- Generalize and constrain the type
      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
        -- Show the inferred type in a warning
        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
        -- For non-recursive binding groups, can generalize over constraints.
        -- For recursive binding groups, we throw an error here for now.
        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
        -- We need information about functional dependencies, since we allow
        -- ambiguous types to be inferred if they can be solved by some functional
        -- dependency.
        [([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
            -- The set of unknowns mentioned in each argument.
            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)
        -- Make sure any unsolved type constraints are determined by the
        -- type variables which appear unknown in the inferred type.
        let
          -- Take the closure of fundeps across constraints, to get more
          -- and more solved variables until reaching a fixpoint.
          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
            -- If all of the determining arguments of a particular fundep are
            -- already determined, add the determined arguments from the fundep
            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)
        -- These unknowns can be determined from the body of the inferred
        -- type (i.e. excluding the unknowns mentioned in the constraints)
        let determinedFromType :: Set Int
determinedFromType = forall a. Ord a => [a] -> Set a
S.fromList [Int]
unsolvedTypeVars
        -- These are all the unknowns mentioned in the constraints
        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

      -- Check skolem variables did not escape their scope
      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)

    -- Show warnings here, since types in wildcards might have been solved during
    -- instance resolution (by functional dependencies).
    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)

    -- Run type search to complete any typed hole error messages
    runTypeSearch
      :: Maybe [(Ident, InstanceContext, SourceConstraint)]
           -- Any unsolved constraints which we need to continue to satisfy
      -> CheckState
           -- The final type checker state
      -> 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

    -- Add any unsolved constraints
    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)

    -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values

    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

-- | A binding group contains multiple value definitions, some of which are typed
-- and some which are not.
--
-- This structure breaks down a binding group into typed and untyped parts.
data SplitBindingGroup = SplitBindingGroup
  { SplitBindingGroup -> [((SourceAnn, Ident), (Expr, SourceType))]
_splitBindingGroupUntyped :: [((SourceAnn, Ident), (Expr, SourceType))]
  -- ^ The untyped expressions
  , SplitBindingGroup
-> [((SourceAnn, Ident),
     (Expr, [(Text, SourceType)], SourceType, Bool))]
_splitBindingGroupTyped :: [((SourceAnn, Ident), (Expr, [(Text, SourceType)], SourceType, Bool))]
  -- ^ The typed expressions, along with their type annotations
  , SplitBindingGroup
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
_splitBindingGroupNames :: M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
  -- ^ A map containing all expressions and their assigned types (which might be
  -- fresh unification variables). These will be added to the 'Environment' after
  -- the binding group is checked, so the value type of the 'Map' is chosen to be
  -- compatible with the type of 'bindNames'.
  }

-- | This function breaks a binding group down into two sets of declarations:
-- those which contain type annotations, and those which don't.
-- This function also generates fresh unification variables for the types of
-- declarations without type annotations, returned in the 'UntypedData' structure.
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
    -- Filter the typed and untyped declarations and make a map of names to typed declarations.
    -- Replace type wildcards here so that the resulting dictionary of types contains the
    -- fully expanded types.
    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)))
    -- Create fresh unification variables for the types of untyped declarations
    ([((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)))
    -- Create the dictionary of all name/type pairs, which will be added to the
    -- environment during type checking
    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
    -- Check if a value contains a type annotation, and if so, separate it
    -- from the value itself.
    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)

-- | Check the type annotation of a typed value in a binding group.
checkTypedBindingGroupElement
  :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
  => ModuleName
  -> ((SourceAnn, Ident), (Expr, [(Text, SourceType)], SourceType, Bool))
  -- ^ The identifier we are trying to define, along with the expression and its type annotation
  -> M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
  -- ^ Names brought into scope in this binding group
  -> 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
  -- We replace type synonyms _after_ kind-checking, since we don't want type
  -- synonym expansion to bring type variables into scope. See #2542.
  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
  -- Check the type with the new names in scope
  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'))

-- | Infer a type for a value in a binding group which lacks an annotation.
typeForBindingGroupElement
  :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
  => ((SourceAnn, Ident), (Expr, SourceType))
  -- ^ The identifier we are trying to define, along with the expression and its assigned type
  -- (at this point, this should be a unification variable)
  -> M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
  -- ^ Names brought into scope in this binding group
  -> 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
  -- Infer the type with the new names in scope
  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
  -- Unify the type with the unification variable we chose for this definition
  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'))

-- | Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
-- or TypeClassDictionary values.
--
-- This is necessary during type checking to avoid unifying a polymorphic type with a
-- unification variable.
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
_ 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)

-- | Match against TUnknown and call insertUnkName, failing otherwise.
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 a type for a value, rethrowing any error to provide a more useful error message
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 a type for a value
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
  -- This "tail" holds all other fields not being updated.
  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
  -- Generate unification variables for each field in ps.
  --
  -- Given:
  --
  -- ob { a = 0, b = 0 }
  --
  -- Then:
  --
  -- obTypes = [(a, ?0), (b, ?1)]
  [(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
      -- Create a record type that contains the unification variables.
      --
      -- obRecordType = Record ( a :: ?0, b :: ?1 | rowType )
      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)
  -- Check ob against obRecordType.
  --
  -- Given:
  --
  -- ob : { a :: Int, b :: Int }
  --
  -- Then:
  --
  -- ?0  ~  Int
  -- ?1  ~  Int
  -- ob' : { a :: ?0, b :: ?1 }
  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
  -- Infer the types of the values used for the record update.
  [(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' (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

-- |
-- Infer the types of named record fields.
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)

-- |
-- Infer the type of a value when used as a record field.
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)

-- |
-- Determines if a value's type needs to be monomorphized when
-- used inside of a record.
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"

-- | Infer the types of variables brought into scope by a binder
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"

-- | Returns true if a binder requires its argument type to be a monotype.
-- | If this is the case, we need to instantiate any polymorphic types before checking binders.
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

-- | Instantiate polytypes only when necessitated by a binder.
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

-- |
-- Check the types of the return values in a set of binders in a case statement
--
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 the type of a value, rethrowing errors to provide a better error message
--
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 the type of a value
--
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 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
      -- We should only skolemize types in values when the type variable
      -- was actually brought into scope. Otherwise we can end up skolemizing
      -- an undefined type variable that happens to clash with the variable we
      -- want to skolemize. This can happen due to synonym expansion (see 2542).
      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
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll SourceAnn
ann 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
  -- An empty class dictionary is never used; see code in `TypeChecker.Entailment`
  -- that wraps empty dictionary solutions in `Unused`.
  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
  -- Don't unify an unknown with an inferred polytype
  (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
  {-
  -- Here, we replace a placeholder for a superclass dictionary with a regular
  -- TypeClassDictionary placeholder. The reason we do this is that it is necessary to have the
  -- correct super instance dictionaries in scope, and these are not available when the type class
  -- declaration gets desugared.
  -}
  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
  -- We need to be careful to avoid duplicate labels here.
  -- We check _obj_ against the type _t_ with the types in _ps_ replaced with unknowns.
  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

-- |
-- Check the type of a collection of named record fields
--
-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.
--
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)

-- | Check the type of a function application, rethrowing errors to provide a better error message.
--
-- This judgment takes three inputs:
--
-- * The expression of the function we are applying
-- * The type of that function
-- * The expression we are applying it to
--
-- and synthesizes two outputs:
--
-- * The return type
-- * The elaborated expression for the function application (since we might need to
--   insert type class dictionaries, etc.)
checkFunctionApplication
  :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
  => Expr
  -- ^ The function expression
  -> SourceType
  -- ^ The type of the function
  -> Expr
  -- ^ The argument expression
  -> m (SourceType, Expr)
  -- ^ The result type, and the elaborated term
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

-- | Check the type of a function application
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
_ 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))

-- |
-- Ensure a set of property names and value does not contain duplicate labels
--
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 ()

-- | Test if this is an internal value to be excluded from error hints
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

-- | Introduce a hint only if the given expression is not internal
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