hydra-kernel-0.16.0: src/main/haskell/Hydra/Inference.hs
-- Note: this is an automatically generated file. Do not edit.
-- | Type inference for Hydra: Hindley-Milner with elaboration to System F. Extends textbook Algorithm W with nominal types, explicit type abstraction and application, and class constraints. See the Inference wiki page for the full picture.
module Hydra.Inference where
import qualified Hydra.Annotations as Annotations
import qualified Hydra.Ast as Ast
import qualified Hydra.Checking as Checking
import qualified Hydra.Coders as Coders
import qualified Hydra.Core as Core
import qualified Hydra.Error.Checking as ErrorChecking
import qualified Hydra.Error.Core as ErrorCore
import qualified Hydra.Error.Packaging as ErrorPackaging
import qualified Hydra.Errors as Errors
import qualified Hydra.Extract.Core as ExtractCore
import qualified Hydra.Graph as Graph
import qualified Hydra.Json.Model as Model
import qualified Hydra.Lexical as Lexical
import qualified Hydra.Haskell.Lib.Eithers as Eithers
import qualified Hydra.Haskell.Lib.Equality as Equality
import qualified Hydra.Haskell.Lib.Lists as Lists
import qualified Hydra.Haskell.Lib.Literals as Literals
import qualified Hydra.Haskell.Lib.Logic as Logic
import qualified Hydra.Haskell.Lib.Maps as Maps
import qualified Hydra.Haskell.Lib.Math as Math
import qualified Hydra.Haskell.Lib.Optionals as Optionals
import qualified Hydra.Haskell.Lib.Pairs as Pairs
import qualified Hydra.Haskell.Lib.Sets as Sets
import qualified Hydra.Haskell.Lib.Strings as Strings
import qualified Hydra.Names as Names
import qualified Hydra.Packaging as Packaging
import qualified Hydra.Parsing as Parsing
import qualified Hydra.Paths as Paths
import qualified Hydra.Query as Query
import qualified Hydra.Reflect as Reflect
import qualified Hydra.Relational as Relational
import qualified Hydra.Resolution as Resolution
import qualified Hydra.Rewriting as Rewriting
import qualified Hydra.Scoping as Scoping
import qualified Hydra.Show.Core as ShowCore
import qualified Hydra.Show.Errors as ShowErrors
import qualified Hydra.Show.Typing as ShowTyping
import qualified Hydra.Sorting as Sorting
import qualified Hydra.Substitution as Substitution
import qualified Hydra.Tabular as Tabular
import qualified Hydra.Testing as Testing
import qualified Hydra.Topology as Topology
import qualified Hydra.Typed as Typed
import qualified Hydra.Typing as Typing
import qualified Hydra.Unification as Unification
import qualified Hydra.Util as Util
import qualified Hydra.Validation as Validation
import qualified Hydra.Variables as Variables
import qualified Hydra.Variants as Variants
import Prelude hiding (Enum, Ordering, decodeFloat, encodeFloat, fail, map, pure, sum)
import qualified Data.Scientific as Sci
import qualified Data.Map as M
import qualified Data.Set as S
-- | Return the element at the given index, or Left(Other) with the given description if out of range
atOrFail :: Int -> String -> [t0] -> Either Errors.Error t0
atOrFail i desc xs =
Optionals.cases (Lists.maybeAt i xs) (Left (Errors.ErrorOther (Errors.OtherError (Strings.cat2 "atOrFail: " desc)))) (\x -> Right x)
-- | Unify type constraints and check the substitution
bindConstraints :: Typing.InferenceContext -> Graph.Graph -> [Typing.TypeConstraint] -> Either Errors.Error Typing.TypeSubst
bindConstraints flowCx cx constraints =
Eithers.bind (Eithers.bimap (\_e -> Errors.ErrorInference (Errors.InferenceErrorUnification (Errors.UnificationInferenceError {
Errors.unificationInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace flowCx))),
Errors.unificationInferenceErrorCause = _e}))) (\_a -> _a) (Unification.unifyTypeConstraints flowCx (Graph.graphSchemaTypes cx) constraints)) (\s -> Eithers.bind (Checking.checkTypeSubst flowCx cx s) (\_ -> Right s))
-- | Handle unbound type variables under a typed let binding. Variables appearing free in the binding's declared type (but not in schema types or the scheme's own quantified variables) are added to the scheme and the term is wrapped in matching TypeLambdas. Variables appearing only in the term body (at type-application or lambda-domain positions) are phantom — they have no external effect on the binding's type — and are substituted with hydra.core.Unit in the body rather than generalized. This keeps downstream stages from seeing vacuous foralls that target languages with non-polymorphic value bindings (e.g. Scala val) cannot express.
bindUnboundTypeVariables :: Graph.Graph -> Core.Term -> Core.Term
bindUnboundTypeVariables cx term0 =
let svars = Sets.fromList (Maps.keys (Graph.graphSchemaTypes cx))
rewrite =
\recurse -> \term -> case term of
Core.TermLet v0 ->
let forBinding =
\b ->
let bname = Core.bindingName b
bterm = Core.bindingTerm b
in (Optionals.cases (Core.bindingTypeScheme b) (Core.Binding {
Core.bindingName = bname,
Core.bindingTerm = (bindUnboundTypeVariables cx bterm),
Core.bindingTypeScheme = Nothing}) (\ts ->
let bvars = Sets.fromList (Core.typeSchemeVariables ts)
excluded = Sets.union svars bvars
inType = Sets.difference (Variables.freeVariablesInType (Core.typeSchemeBody ts)) excluded
phantoms = Sets.difference (Variables.freeTypeVariablesInTerm bterm) (Sets.union excluded inType)
phantomSubst = Typing.TypeSubst (Maps.fromList (Lists.map (\v -> (v, Core.TypeUnit)) (Sets.toList phantoms)))
bterm1 = Substitution.substTypesInTerm phantomSubst bterm
unbound = Sets.toList inType
ts2 =
Core.TypeScheme {
Core.typeSchemeVariables = (Lists.concat2 (Core.typeSchemeVariables ts) unbound),
Core.typeSchemeBody = (Core.typeSchemeBody ts),
Core.typeSchemeConstraints = (Core.typeSchemeConstraints ts)}
bterm2 =
Lists.foldl (\t -> \v -> Core.TermTypeLambda (Core.TypeLambda {
Core.typeLambdaParameter = v,
Core.typeLambdaBody = t})) bterm1 unbound
in Core.Binding {
Core.bindingName = bname,
Core.bindingTerm = bterm2,
Core.bindingTypeScheme = (Just ts2)}))
in (Core.TermLet (Core.Let {
Core.letBindings = (Lists.map forBinding (Core.letBindings v0)),
Core.letBody = (bindUnboundTypeVariables cx (Core.letBody v0))}))
_ -> recurse term
in (Rewriting.rewriteTerm rewrite term0)
-- | Fold a list of type variables over a term to build a type application term
buildTypeApplicationTerm :: [Core.Name] -> Core.Term -> Core.Term
buildTypeApplicationTerm tvars body =
Lists.foldl (\t -> \v -> Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = t,
Core.typeApplicationTermType = (Core.TypeVariable v)})) body tvars
-- | Add (term variable, type scheme) pairs to the graph's bound types
extendContext :: [(Core.Name, Core.TypeScheme)] -> Graph.Graph -> Graph.Graph
extendContext pairs cx =
Graph.Graph {
Graph.graphBoundTerms = (Graph.graphBoundTerms cx),
Graph.graphBoundTypes = (Maps.union (Maps.fromList pairs) (Graph.graphBoundTypes cx)),
Graph.graphClassConstraints = (Graph.graphClassConstraints cx),
Graph.graphLambdaVariables = (Graph.graphLambdaVariables cx),
Graph.graphMetadata = (Graph.graphMetadata cx),
Graph.graphPrimitives = (Graph.graphPrimitives cx),
Graph.graphSchemaTypes = (Graph.graphSchemaTypes cx),
Graph.graphTypeVariables = (Graph.graphTypeVariables cx)}
-- | Finalize an inferred term by checking for unbound type variables, then normalizing type variables
finalizeInferredTerm :: t0 -> Graph.Graph -> Core.Term -> Either Errors.Error Core.Term
finalizeInferredTerm flowCx cx term =
let term2 = bindUnboundTypeVariables cx term
in (Eithers.bind (Checking.checkForUnboundTypeVariables flowCx cx term2) (\_ -> Right (Variables.normalizeTypeVariablesInTerm term2)))
-- | Infer a term's type and map over the result
forInferredTerm :: Typing.InferenceContext -> Graph.Graph -> Core.Term -> String -> (Typing.InferenceResult -> t0) -> Either Errors.Error (t0, Typing.InferenceContext)
forInferredTerm fcx cx term desc f =
Eithers.bind (inferTypeOfTerm fcx cx term desc) (\rp -> Right (f rp, (Typing.inferenceResultContext rp)))
-- | Get all free variables in a graph's bound types
freeVariablesInContext :: Graph.Graph -> S.Set Core.Name
freeVariablesInContext cx =
Lists.foldl Sets.union Sets.empty (Lists.map Variables.freeVariablesInTypeSchemeSimple (Maps.elems (Graph.graphBoundTypes cx)))
-- | Generate a fresh type variable
freshVariableType :: Typing.InferenceContext -> (Core.Type, Typing.InferenceContext)
freshVariableType cx =
let result = Names.freshName cx
name = Pairs.first result
cx2 = Pairs.second result
in (Core.TypeVariable name, cx2)
-- | Generalize a type to a type scheme
generalize :: Graph.Graph -> Core.Type -> Core.TypeScheme
generalize cx typ =
let isTypeVarName =
\name ->
let parts = Strings.splitOn "." (Core.unName name)
in (Equality.lte (Lists.length parts) 1)
vars =
Lists.nub (Lists.filter (\v -> Logic.and (isUnbound cx v) (isTypeVarName v)) (Variables.freeVariablesInTypeOrdered typ))
allConstraints = Graph.graphClassConstraints cx
relevantConstraints =
Maps.fromList (Optionals.cat (Lists.map (\v -> Optionals.map (\meta -> (v, meta)) (Maps.lookup v allConstraints)) vars))
constraintsMaybe = Logic.ifElse (Maps.null relevantConstraints) Nothing (Just relevantConstraints)
in Core.TypeScheme {
Core.typeSchemeVariables = vars,
Core.typeSchemeBody = typ,
Core.typeSchemeConstraints = constraintsMaybe}
-- | Return the first element of a list, or Left(Other) with the given description if the list is empty
headOrFail :: String -> [t0] -> Either Errors.Error t0
headOrFail desc xs =
Optionals.cases (Lists.maybeHead xs) (Left (Errors.ErrorOther (Errors.OtherError (Strings.cat2 "headOrFail: " desc)))) (\x -> Right x)
-- | Infer types for all elements in a graph, using the provided ordered bindings. Returns both the inferred graph and the ordered inferred bindings.
inferGraphTypes :: Typing.InferenceContext -> [Core.Binding] -> Graph.Graph -> Either Errors.Error ((Graph.Graph, [Core.Binding]), Typing.InferenceContext)
inferGraphTypes fcx0 bindings0 g0 =
let fcx = fcx0
let0 =
Core.Let {
Core.letBindings = bindings0,
Core.letBody = Core.TermUnit}
fromLetTerm =
\l ->
let bindings = Core.letBindings l
prims = Graph.graphPrimitives g0
schemaTypes = Graph.graphSchemaTypes g0
rawG = Lexical.buildGraph bindings Maps.empty prims
g =
Graph.Graph {
Graph.graphBoundTerms = (Graph.graphBoundTerms rawG),
Graph.graphBoundTypes = (Graph.graphBoundTypes rawG),
Graph.graphClassConstraints = (Graph.graphClassConstraints rawG),
Graph.graphLambdaVariables = (Graph.graphLambdaVariables rawG),
Graph.graphMetadata = (Graph.graphMetadata rawG),
Graph.graphPrimitives = (Graph.graphPrimitives rawG),
Graph.graphSchemaTypes = schemaTypes,
Graph.graphTypeVariables = (Graph.graphTypeVariables rawG)}
in (g, bindings)
in (Eithers.bind (inferTypeOfTerm fcx g0 (Core.TermLet let0) "graph term") (\result ->
let fcx2 = Typing.inferenceResultContext result
term = Typing.inferenceResultTerm result
in (Eithers.bind (finalizeInferredTerm fcx2 g0 term) (\finalized -> case finalized of
Core.TermLet v0 -> Right (fromLetTerm v0, fcx2)
Core.TermVariable _ -> Left (Errors.ErrorInference (Errors.InferenceErrorOther (Errors.OtherInferenceError {
Errors.otherInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace fcx2))),
Errors.otherInferenceErrorMessage = "Expected inferred graph as let term"})))))))
-- | Infer the type of a term in a given inference context
inferInGraphContext :: Typing.InferenceContext -> Graph.Graph -> Core.Term -> Either Errors.Error Typing.InferenceResult
inferInGraphContext fcx cx term = inferTypeOfTerm fcx cx term "single term"
-- | Infer types for multiple terms, propagating class constraints from sub-expressions
inferMany :: Typing.InferenceContext -> Graph.Graph -> [(Core.Term, String)] -> Either Errors.Error (
([Core.Term], ([Core.Type], (Typing.TypeSubst, (M.Map Core.Name Core.TypeVariableConstraints)))),
Typing.InferenceContext)
inferMany fcx cx pairs =
let emptyResult = Right (([], ([], (Substitution.idTypeSubst, Maps.empty))), fcx)
in (Optionals.cases (Lists.uncons pairs) emptyResult (\pairsUc ->
let headPair = Pairs.first pairsUc
tl = Pairs.second pairsUc
e = Pairs.first headPair
desc = Pairs.second headPair
in (Eithers.bind (inferTypeOfTerm fcx cx e desc) (\result1 ->
let fcx2 = Typing.inferenceResultContext result1
e1 = Typing.inferenceResultTerm result1
t1 = Typing.inferenceResultType result1
s1 = Typing.inferenceResultSubst result1
c1 = Typing.inferenceResultClassConstraints result1
in (Eithers.bind (inferMany fcx2 (Substitution.substInContext s1 cx) tl) (\rp2 ->
let result2 = Pairs.first rp2
fcx3 = Pairs.second rp2
e2 = Pairs.first result2
t2 = Pairs.first (Pairs.second result2)
s2 = Pairs.first (Pairs.second (Pairs.second result2))
c2 = Pairs.second (Pairs.second (Pairs.second result2))
c1Subst = Substitution.substInClassConstraints s2 c1
mergedConstraints = mergeClassConstraints c1Subst c2
in (Right (
(
Lists.cons (Substitution.substTypesInTerm s2 e1) e2,
(Lists.cons (Substitution.substInType s2 t1) t2, (Substitution.composeTypeSubst s1 s2, mergedConstraints))),
fcx3))))))))
-- | Map a possibly untyped term to a fully typed term and its type
inferTypeOf :: Typing.InferenceContext -> Graph.Graph -> Core.Term -> Either Errors.Error ((Core.Term, Core.TypeScheme), Typing.InferenceContext)
inferTypeOf fcx cx term =
let letTerm =
Core.TermLet (Core.Let {
Core.letBindings = [
Core.Binding {
Core.bindingName = (Core.Name "ignoredVariableName"),
Core.bindingTerm = term,
Core.bindingTypeScheme = Nothing}],
Core.letBody = (Core.TermLiteral (Core.LiteralString "ignoredBody"))})
in (Eithers.bind (inferTypeOfTerm fcx cx letTerm "infer type of term") (\result ->
let fcx2 = Typing.inferenceResultContext result
in (Eithers.bind (finalizeInferredTerm fcx2 cx (Typing.inferenceResultTerm result)) (\finalized -> Eithers.bind (ExtractCore.let_ cx finalized) (\letResult ->
let bindings = Core.letBindings letResult
in (Logic.ifElse (Equality.equal 1 (Lists.length bindings)) (Eithers.bind (headOrFail "inferTypeOf: single binding expected" bindings) (\binding ->
let term1 = Core.bindingTerm binding
mts = Core.bindingTypeScheme binding
in (Optionals.cases mts (Left (Errors.ErrorInference (Errors.InferenceErrorOther (Errors.OtherInferenceError {
Errors.otherInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace fcx2))),
Errors.otherInferenceErrorMessage = "Expected a type scheme"})))) (\ts -> Right ((term1, ts), fcx2))))) (Left (Errors.ErrorInference (Errors.InferenceErrorOther (Errors.OtherInferenceError {
Errors.otherInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace fcx2))),
Errors.otherInferenceErrorMessage = (Strings.cat [
"Expected a single binding with a type scheme, but got: ",
(Literals.showInt32 (Lists.length bindings)),
" bindings"])}))))))))))
-- | Infer the type of an annotated term (Either version)
inferTypeOfAnnotatedTerm :: Typing.InferenceContext -> Graph.Graph -> Core.AnnotatedTerm -> Either Errors.Error Typing.InferenceResult
inferTypeOfAnnotatedTerm fcx cx at =
let term = Core.annotatedTermBody at
ann = Core.annotatedTermAnnotation at
fcxBody = Names.pushSubtermStep Paths.SubtermStepAnnotatedBody fcx
in (Eithers.bind (inferTypeOfTerm fcxBody cx term "annotated term") (\result ->
let fcx2 = Names.restoreTrace fcx (Typing.inferenceResultContext result)
iterm = Typing.inferenceResultTerm result
itype = Typing.inferenceResultType result
isubst = Typing.inferenceResultSubst result
iconstraints = Typing.inferenceResultClassConstraints result
in (Right (Typing.InferenceResult {
Typing.inferenceResultTerm = (Core.TermAnnotated (Core.AnnotatedTerm {
Core.annotatedTermBody = iterm,
Core.annotatedTermAnnotation = ann})),
Typing.inferenceResultType = itype,
Typing.inferenceResultSubst = isubst,
Typing.inferenceResultClassConstraints = iconstraints,
Typing.inferenceResultContext = fcx2}))))
-- | Infer the type of a function application (Either version)
inferTypeOfApplication :: Typing.InferenceContext -> Graph.Graph -> Core.Application -> Either Errors.Error Typing.InferenceResult
inferTypeOfApplication fcx0 cx app =
let e0 = Core.applicationFunction app
e1 = Core.applicationArgument app
fcxFun = Names.pushSubtermStep Paths.SubtermStepApplicationFunction fcx0
in (Eithers.bind (inferTypeOfTerm fcxFun cx e0 "lhs") (\lhsResult ->
let fcx2 = Names.restoreTrace fcx0 (Typing.inferenceResultContext lhsResult)
a = Typing.inferenceResultTerm lhsResult
t0 = Typing.inferenceResultType lhsResult
s0 = Typing.inferenceResultSubst lhsResult
c0 = Typing.inferenceResultClassConstraints lhsResult
fcxArg = Names.pushSubtermStep Paths.SubtermStepApplicationArgument fcx2
in (Eithers.bind (inferTypeOfTerm fcxArg (Substitution.substInContext s0 cx) e1 "rhs") (\rhsResult ->
let fcx3 = Names.restoreTrace fcx0 (Typing.inferenceResultContext rhsResult)
b = Typing.inferenceResultTerm rhsResult
t1 = Typing.inferenceResultType rhsResult
s1 = Typing.inferenceResultSubst rhsResult
c1 = Typing.inferenceResultClassConstraints rhsResult
vResult = Names.freshName fcx3
v = Pairs.first vResult
fcx4 = Pairs.second vResult
in (Eithers.bind (Eithers.bimap (\_e -> Errors.ErrorInference (Errors.InferenceErrorUnification (Errors.UnificationInferenceError {
Errors.unificationInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace fcx4))),
Errors.unificationInferenceErrorCause = _e}))) (\_a -> _a) (Unification.unifyTypes fcx4 (Graph.graphSchemaTypes cx) (Substitution.substInType s1 t0) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = t1,
Core.functionTypeCodomain = (Core.TypeVariable v)})) "application lhs")) (\s2 -> Eithers.bind (Checking.checkTypeSubst fcx4 cx s2) (\_ ->
let rExpr =
Core.TermApplication (Core.Application {
Core.applicationFunction = (Substitution.substTypesInTerm (Substitution.composeTypeSubst s1 s2) a),
Core.applicationArgument = (Substitution.substTypesInTerm s2 b)})
rType = Substitution.substInType s2 (Core.TypeVariable v)
rSubst =
Substitution.composeTypeSubstList [
s0,
s1,
s2]
c0Subst = Substitution.substInClassConstraints s2 (Substitution.substInClassConstraints s1 c0)
c1Subst = Substitution.substInClassConstraints s2 c1
rConstraints = mergeClassConstraints c0Subst c1Subst
in (Right (Typing.InferenceResult {
Typing.inferenceResultTerm = rExpr,
Typing.inferenceResultType = rType,
Typing.inferenceResultSubst = rSubst,
Typing.inferenceResultClassConstraints = rConstraints,
Typing.inferenceResultContext = fcx4})))))))))
-- | Infer the type of a case statement (Either version)
inferTypeOfCaseStatement :: Typing.InferenceContext -> Graph.Graph -> Core.CaseStatement -> Either Errors.Error Typing.InferenceResult
inferTypeOfCaseStatement fcx cx caseStmt =
let tname = Core.caseStatementTypeName caseStmt
dflt = Core.caseStatementDefault caseStmt
cases = Core.caseStatementCases caseStmt
fnames = Lists.map Core.caseAlternativeName cases
in (Eithers.bind (Resolution.requireSchemaType fcx (Graph.graphSchemaTypes cx) tname) (\stRp ->
let schemaType = Pairs.first stRp
fcx2 = Pairs.second stRp
svars = Core.typeSchemeVariables schemaType
stype = Core.typeSchemeBody schemaType
in (Eithers.bind (ExtractCore.unionType tname stype) (\sfields ->
let fcxDflt = Names.pushSubtermStep Paths.SubtermStepUnionCasesDefault fcx2
in (Eithers.bind (Eithers.mapOptional (\t -> inferTypeOfTerm fcxDflt cx t (Strings.cat [
"case ",
(Core.unName tname),
".<default>"])) dflt) (\dfltRp ->
let dfltResult = dfltRp
fcx3 =
Optionals.fromOptional fcx2 (Optionals.map (\_r -> Names.restoreTrace fcx2 (Typing.inferenceResultContext _r)) dfltRp)
in (Eithers.bind (inferMany fcx3 cx (Lists.map (\f -> (
Core.caseAlternativeHandler f,
(Strings.cat [
"case ",
(Core.unName tname),
".",
(Core.unName (Core.caseAlternativeName f))]))) cases)) (\caseRp ->
let caseResults = Pairs.first caseRp
fcx4 = Pairs.second caseRp
iterms = Pairs.first caseResults
itypes = Pairs.first (Pairs.second caseResults)
isubst = Pairs.first (Pairs.second (Pairs.second caseResults))
caseElemConstraints = Pairs.second (Pairs.second (Pairs.second caseResults))
codvResult = Names.freshName fcx4
codv = Pairs.first codvResult
fcx5 = Pairs.second codvResult
cod = Core.TypeVariable codv
caseMap = Maps.fromList (Lists.map (\ft -> (Core.fieldTypeName ft, (Core.fieldTypeType ft))) sfields)
dfltConstraints =
Optionals.toList (Optionals.map (\r -> Typing.TypeConstraint {
Typing.typeConstraintLeft = cod,
Typing.typeConstraintRight = (Substitution.substInType isubst (Typing.inferenceResultType r)),
Typing.typeConstraintComment = "match default"}) dfltResult)
caseConstraints =
Optionals.cat (Lists.zipWith (\fname -> \itype -> Optionals.map (\ftype -> Typing.TypeConstraint {
Typing.typeConstraintLeft = itype,
Typing.typeConstraintRight = (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = ftype,
Core.functionTypeCodomain = cod})),
Typing.typeConstraintComment = "case type"}) (Maps.lookup fname caseMap)) fnames itypes)
dfltClassConstraints = Optionals.fromOptional Maps.empty (Optionals.map Typing.inferenceResultClassConstraints dfltResult)
allElemConstraints = mergeClassConstraints caseElemConstraints dfltClassConstraints
in (Eithers.bind (mapConstraints fcx5 cx (\subst -> yieldWithConstraints fcx5 (buildTypeApplicationTerm svars (Core.TermCases (Core.CaseStatement {
Core.caseStatementTypeName = tname,
Core.caseStatementDefault = (Optionals.map Typing.inferenceResultTerm dfltResult),
Core.caseStatementCases = (Lists.zipWith (\n -> \t -> Core.CaseAlternative {
Core.caseAlternativeName = n,
Core.caseAlternativeHandler = t}) fnames iterms)}))) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Resolution.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)),
Core.functionTypeCodomain = cod})) (Substitution.composeTypeSubstList (Lists.concat [
Optionals.toList (Optionals.map Typing.inferenceResultSubst dfltResult),
[
isubst,
subst]])) (Substitution.substInClassConstraints subst allElemConstraints)) (Lists.concat [
dfltConstraints,
caseConstraints])) (\mcResult -> Right mcResult))))))))))
-- | Infer the type of a collection. The classNames parameter specifies type classes (e.g. ordering) that the element type variable must satisfy.
inferTypeOfCollection :: Typing.InferenceContext -> Graph.Graph -> (Core.Type -> Core.Type) -> ([Core.Term] -> Core.Term) -> String -> S.Set Core.Name -> [Core.Term] -> Either Errors.Error Typing.InferenceResult
inferTypeOfCollection fcx cx typCons trmCons desc classNames els =
let varResult = Names.freshName fcx
var = Pairs.first varResult
fcx2 = Pairs.second varResult
classConstraints =
Logic.ifElse (Sets.null classNames) Maps.empty (Maps.singleton var (Core.TypeVariableConstraints {
Core.typeVariableConstraintsClasses = (Lists.map (\n -> Core.TypeClassConstraintSimple n) (Sets.toList classNames))}))
in (Logic.ifElse (Lists.null els) (Right (yieldWithConstraints fcx2 (buildTypeApplicationTerm [
var] (trmCons [])) (typCons (Core.TypeVariable var)) Substitution.idTypeSubst classConstraints)) (Eithers.bind (inferMany fcx2 cx (Lists.zip els (Lists.map (\i -> Strings.cat [
"#",
(Literals.showInt32 i)]) (Math.range 1 (Math.add (Lists.length els) 1))))) (\resultsRp ->
let results = Pairs.first resultsRp
fcx3 = Pairs.second resultsRp
terms = Pairs.first results
types = Pairs.first (Pairs.second results)
subst1 = Pairs.first (Pairs.second (Pairs.second results))
elemConstraints = Pairs.second (Pairs.second (Pairs.second results))
constraints =
Lists.map (\t -> Typing.TypeConstraint {
Typing.typeConstraintLeft = (Core.TypeVariable var),
Typing.typeConstraintRight = t,
Typing.typeConstraintComment = desc}) types
allConstraints = mergeClassConstraints classConstraints elemConstraints
in (Eithers.bind (mapConstraints fcx3 cx (\subst2 ->
let iterm = trmCons terms
itype = typCons (Core.TypeVariable var)
isubst = Substitution.composeTypeSubst subst1 subst2
in (yieldWithConstraints fcx3 iterm itype isubst (Substitution.substInClassConstraints subst2 allConstraints))) constraints) (\mcResult -> Right mcResult)))))
-- | Infer the type of an either value (Either version)
inferTypeOfEither :: Typing.InferenceContext -> Graph.Graph -> Either Core.Term Core.Term -> Either Errors.Error Typing.InferenceResult
inferTypeOfEither fcx cx e =
Eithers.either (\l -> Eithers.bind (inferTypeOfTerm fcx cx l "either left value") (\r1 ->
let fcx2 = Typing.inferenceResultContext r1
iterm = Typing.inferenceResultTerm r1
leftType = Typing.inferenceResultType r1
subst = Typing.inferenceResultSubst r1
fvResult = freshVariableType fcx2
rightType = Pairs.first fvResult
fcx3 = Pairs.second fvResult
eitherTerm = Core.TermEither (Left iterm)
termWithLeftType =
Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = eitherTerm,
Core.typeApplicationTermType = leftType})
termWithBothTypes =
Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = termWithLeftType,
Core.typeApplicationTermType = rightType})
eitherType =
Core.TypeEither (Core.EitherType {
Core.eitherTypeLeft = leftType,
Core.eitherTypeRight = rightType})
in (Right (yieldChecked fcx3 termWithBothTypes eitherType subst)))) (\r -> Eithers.bind (inferTypeOfTerm fcx cx r "either right value") (\r1 ->
let fcx2 = Typing.inferenceResultContext r1
iterm = Typing.inferenceResultTerm r1
rightType = Typing.inferenceResultType r1
subst = Typing.inferenceResultSubst r1
fvResult = freshVariableType fcx2
leftType = Pairs.first fvResult
fcx3 = Pairs.second fvResult
eitherTerm = Core.TermEither (Right iterm)
termWithLeftType =
Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = eitherTerm,
Core.typeApplicationTermType = leftType})
termWithBothTypes =
Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = termWithLeftType,
Core.typeApplicationTermType = rightType})
eitherType =
Core.TypeEither (Core.EitherType {
Core.eitherTypeLeft = leftType,
Core.eitherTypeRight = rightType})
in (Right (yieldChecked fcx3 termWithBothTypes eitherType subst)))) e
-- | Infer the type of a union injection (Either version)
inferTypeOfInjection :: Typing.InferenceContext -> Graph.Graph -> Core.Injection -> Either Errors.Error Typing.InferenceResult
inferTypeOfInjection fcx cx injection =
let tname = Core.injectionTypeName injection
field = Core.injectionField injection
fname = Core.fieldName field
term = Core.fieldTerm field
fcxInj = Names.pushSubtermStep Paths.SubtermStepSumTerm fcx
in (Eithers.bind (inferTypeOfTerm fcxInj cx term "injected term") (\result ->
let fcx2 = Names.restoreTrace fcx (Typing.inferenceResultContext result)
in (Eithers.bind (Resolution.requireSchemaType fcx2 (Graph.graphSchemaTypes cx) tname) (\stRp ->
let schemaType = Pairs.first stRp
fcx3 = Pairs.second stRp
svars = Core.typeSchemeVariables schemaType
stype = Core.typeSchemeBody schemaType
iterm = Typing.inferenceResultTerm result
ityp = Typing.inferenceResultType result
isubst = Typing.inferenceResultSubst result
in (Eithers.bind (ExtractCore.unionType tname stype) (\sfields -> Eithers.bind (Resolution.findFieldType fcx3 fname sfields) (\ftyp -> Eithers.bind (mapConstraints fcx3 cx (\subst -> yield fcx3 (buildTypeApplicationTerm svars (Core.TermInject (Core.Injection {
Core.injectionTypeName = tname,
Core.injectionField = Core.Field {
Core.fieldName = fname,
Core.fieldTerm = iterm}}))) (Resolution.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)) (Substitution.composeTypeSubst isubst subst)) [
Typing.TypeConstraint {
Typing.typeConstraintLeft = ftyp,
Typing.typeConstraintRight = ityp,
Typing.typeConstraintComment = "schema type of injected field"}]) (\mcResult -> Right mcResult))))))))
-- | Infer the type of a lambda function (Either version)
inferTypeOfLambda :: Typing.InferenceContext -> Graph.Graph -> Core.Lambda -> Either Errors.Error Typing.InferenceResult
inferTypeOfLambda fcx cx lambda =
let var = Core.lambdaParameter lambda
body = Core.lambdaBody lambda
vdomResult = Names.freshName fcx
vdom = Pairs.first vdomResult
fcx2 = Pairs.second vdomResult
dom = Core.TypeVariable vdom
cx2 =
extendContext [
(
var,
Core.TypeScheme {
Core.typeSchemeVariables = [],
Core.typeSchemeBody = dom,
Core.typeSchemeConstraints = Nothing})] cx
fcxBody = Names.pushSubtermStep Paths.SubtermStepLambdaBody fcx2
in (Eithers.bind (inferTypeOfTerm fcxBody cx2 body "lambda body") (\result ->
let fcx3 = Names.restoreTrace fcx2 (Typing.inferenceResultContext result)
iterm = Typing.inferenceResultTerm result
icod = Typing.inferenceResultType result
isubst = Typing.inferenceResultSubst result
rdom = Substitution.substInType isubst dom
rterm =
Core.TermLambda (Core.Lambda {
Core.lambdaParameter = var,
Core.lambdaDomain = (Just rdom),
Core.lambdaBody = iterm})
rtype =
Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = rdom,
Core.functionTypeCodomain = icod})
vars =
Sets.unions [
Variables.freeVariablesInType rdom,
(Variables.freeVariablesInType icod),
(freeVariablesInContext (Substitution.substInContext isubst cx2))]
cx3 = Substitution.substInContext isubst cx
iconstraints = Substitution.substInClassConstraints isubst (Typing.inferenceResultClassConstraints result)
in (Right (Typing.InferenceResult {
Typing.inferenceResultTerm = rterm,
Typing.inferenceResultType = rtype,
Typing.inferenceResultSubst = isubst,
Typing.inferenceResultClassConstraints = iconstraints,
Typing.inferenceResultContext = fcx3}))))
-- | Normalize a let term before inferring its type (Either version). The bindings are partitioned into strongly connected components and reorganized as nested lets, one let per SCC, in dependency order. This is the standard Hindley-Milner treatment of mutual recursion: each SCC is generalized once at its boundary (sound, because nothing inside the cluster sees a polymorphic instance of its siblings), and acyclic bindings generalize individually as usual.
inferTypeOfLet :: Typing.InferenceContext -> Graph.Graph -> Core.Let -> Either Errors.Error Typing.InferenceResult
inferTypeOfLet fcx0 cx let0 =
let fcx = fcx0
bindings0 = Core.letBindings let0
body0 = Core.letBody let0
names = Lists.map Core.bindingName bindings0
nameSet = Sets.fromList names
toPair =
\binding ->
let name = Core.bindingName binding
term = Core.bindingTerm binding
in (name, (Lists.filter (\n -> Sets.member n nameSet) (Sets.toList (Variables.freeVariablesInTerm term))))
adjList = Lists.map toPair bindings0
groups = Sorting.topologicalSortComponents adjList
bindingMap = Maps.fromList (Lists.zip names bindings0)
createLet =
\e -> \group -> Core.TermLet (Core.Let {
Core.letBindings = (Optionals.cat (Lists.map (\n -> Maps.lookup n bindingMap) group)),
Core.letBody = e})
rewrittenLet = Lists.foldl createLet body0 (Lists.reverse groups)
restoreLet =
\iterm ->
let helper =
\level -> \bins -> \term ->
let nonzero =
\term2 -> case term2 of
Core.TermLet v0 ->
let bs = Core.letBindings v0
letBody = Core.letBody v0
in (helper (Math.sub level 1) (Lists.concat [
bs,
bins]) letBody)
in (Logic.ifElse (Equality.equal level 0) (bins, term) (nonzero term))
result = helper (Lists.length groups) [] iterm
bindingList = Pairs.first result
e = Pairs.second result
bindingMap2 = Maps.fromList (Lists.map (\b -> (Core.bindingName b, b)) bindingList)
in (Core.TermLet (Core.Let {
Core.letBindings = (Optionals.cat (Lists.map (\n -> Maps.lookup n bindingMap2) names)),
Core.letBody = e}))
rewriteResult =
\iresult ->
let fcxR = Typing.inferenceResultContext iresult
iterm = Typing.inferenceResultTerm iresult
itype = Typing.inferenceResultType iresult
isubst = Typing.inferenceResultSubst iresult
iconstraints = Typing.inferenceResultClassConstraints iresult
in Typing.InferenceResult {
Typing.inferenceResultTerm = (restoreLet iterm),
Typing.inferenceResultType = itype,
Typing.inferenceResultSubst = isubst,
Typing.inferenceResultClassConstraints = iconstraints,
Typing.inferenceResultContext = fcxR}
res =
case rewrittenLet of
Core.TermLet v0 -> inferTypeOfLetNormalized fcx cx v0
_ -> inferTypeOfTerm fcx cx rewrittenLet "empty let term"
in (Eithers.map rewriteResult res)
-- | Infer the type of a let (letrec) term which is already in a normal form (Either version)
inferTypeOfLetNormalized :: Typing.InferenceContext -> Graph.Graph -> Core.Let -> Either Errors.Error Typing.InferenceResult
inferTypeOfLetNormalized fcx0 cx0 letTerm =
let fcx = fcx0
bins0 = Core.letBindings letTerm
body0 = Core.letBody letTerm
bnames = Lists.map Core.bindingName bins0
bvarsResult = Names.freshNames (Lists.length bins0) fcx
bvars = Pairs.first bvarsResult
fcx2 = Pairs.second bvarsResult
tbins0 = Lists.map (\x -> Core.TypeVariable x) bvars
cx1 =
extendContext (Lists.zip bnames (Lists.map (\t -> Core.TypeScheme {
Core.typeSchemeVariables = [],
Core.typeSchemeBody = t,
Core.typeSchemeConstraints = Nothing}) tbins0)) cx0
in (Eithers.bind (inferTypesOfTemporaryBindings fcx2 cx1 bins0) (\irRp ->
let inferredResult = Pairs.first irRp
fcx3 = Pairs.second irRp
bterms1 = Pairs.first inferredResult
tbins1 = Pairs.first (Pairs.second inferredResult)
substAndConstraints = Pairs.second (Pairs.second inferredResult)
s1 = Pairs.first substAndConstraints
inferredConstraints = Pairs.second substAndConstraints
in (Eithers.bind (Eithers.bimap (\_e -> Errors.ErrorInference (Errors.InferenceErrorUnification (Errors.UnificationInferenceError {
Errors.unificationInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace fcx3))),
Errors.unificationInferenceErrorCause = _e}))) (\_a -> _a) (Unification.unifyTypeLists fcx3 (Graph.graphSchemaTypes cx0) (Lists.map (Substitution.substInType s1) tbins0) tbins1 "temporary type bindings")) (\s2 -> Eithers.bind (Checking.checkTypeSubst fcx3 cx0 s2) (\_ ->
let g2base = Substitution.substInContext (Substitution.composeTypeSubst s1 s2) cx0
constraintsWithS2 = Substitution.substInClassConstraints s2 inferredConstraints
composedSubst = Substitution.composeTypeSubst s1 s2
originalBindingConstraints =
Lists.foldl (\acc -> \b -> Optionals.cases (Core.bindingTypeScheme b) acc (\ts -> Optionals.cases (Core.typeSchemeConstraints ts) acc (\c -> mergeClassConstraints acc c))) Maps.empty bins0
originalConstraintsSubst = Substitution.substInClassConstraints composedSubst originalBindingConstraints
allInferredConstraints = mergeClassConstraints constraintsWithS2 originalConstraintsSubst
mergedConstraints = mergeClassConstraints (Graph.graphClassConstraints g2base) allInferredConstraints
g2 =
Graph.Graph {
Graph.graphBoundTerms = (Graph.graphBoundTerms g2base),
Graph.graphBoundTypes = (Graph.graphBoundTypes g2base),
Graph.graphClassConstraints = mergedConstraints,
Graph.graphLambdaVariables = (Graph.graphLambdaVariables g2base),
Graph.graphMetadata = (Graph.graphMetadata g2base),
Graph.graphPrimitives = (Graph.graphPrimitives g2base),
Graph.graphSchemaTypes = (Graph.graphSchemaTypes g2base),
Graph.graphTypeVariables = (Graph.graphTypeVariables g2base)}
bterms1Subst = Lists.map (Substitution.substTypesInTerm s2) bterms1
tsbins1 = Lists.zip bnames (Lists.map (\t -> generalize g2 (Substitution.substInType s2 t)) tbins1)
fcx3Body = Names.pushSubtermStep Paths.SubtermStepLetBody fcx3
in (Eithers.bind (inferTypeOfTerm fcx3Body (extendContext tsbins1 g2) body0 "let body") (\bodyResult ->
let fcx4 = Names.restoreTrace fcx3 (Typing.inferenceResultContext bodyResult)
body1 = Typing.inferenceResultTerm bodyResult
tbody = Typing.inferenceResultType bodyResult
sbody = Typing.inferenceResultSubst bodyResult
st1 =
Typing.TermSubst (Maps.fromList (Lists.map (\pair ->
let name = Pairs.first pair
ts = Pairs.second pair
in (name, (buildTypeApplicationTerm (Core.typeSchemeVariables ts) (Core.TermVariable name)))) tsbins1))
createBinding =
\bindingPair ->
let nameTsPair = Pairs.first bindingPair
term = Pairs.second bindingPair
name = Pairs.first nameTsPair
ts = Pairs.second nameTsPair
finalTs = Substitution.substInTypeScheme sbody ts
typeLambdaTerm =
Lists.foldl (\b -> \v -> Core.TermTypeLambda (Core.TypeLambda {
Core.typeLambdaParameter = v,
Core.typeLambdaBody = b})) (Substitution.substituteInTerm st1 term) (Lists.reverse (Core.typeSchemeVariables finalTs))
in Core.Binding {
Core.bindingName = name,
Core.bindingTerm = (Substitution.substTypesInTerm (Substitution.composeTypeSubst sbody s2) typeLambdaTerm),
Core.bindingTypeScheme = (Just finalTs)}
bins1 = Lists.map createBinding (Lists.zip tsbins1 bterms1Subst)
bodyConstraints = Substitution.substInClassConstraints sbody (Typing.inferenceResultClassConstraints bodyResult)
bindingConstraintsSubst = Substitution.substInClassConstraints sbody constraintsWithS2
allConstraints = mergeClassConstraints bindingConstraintsSubst bodyConstraints
in (Right (Typing.InferenceResult {
Typing.inferenceResultTerm = (Core.TermLet (Core.Let {
Core.letBindings = bins1,
Core.letBody = body1})),
Typing.inferenceResultType = tbody,
Typing.inferenceResultSubst = (Substitution.composeTypeSubstList [
s1,
s2,
sbody]),
Typing.inferenceResultClassConstraints = allConstraints,
Typing.inferenceResultContext = fcx4})))))))))
-- | Infer the type of a list (Either version)
inferTypeOfList :: Typing.InferenceContext -> Graph.Graph -> [Core.Term] -> Either Errors.Error Typing.InferenceResult
inferTypeOfList fcx cx =
inferTypeOfCollection fcx cx (\x -> Core.TypeList x) (\x -> Core.TermList x) "list element" Sets.empty
-- | Infer the type of a literal
inferTypeOfLiteral :: Typing.InferenceContext -> Core.Literal -> Typing.InferenceResult
inferTypeOfLiteral fcx lit =
Typing.InferenceResult {
Typing.inferenceResultTerm = (Core.TermLiteral lit),
Typing.inferenceResultType = (Core.TypeLiteral (Reflect.literalType lit)),
Typing.inferenceResultSubst = Substitution.idTypeSubst,
Typing.inferenceResultClassConstraints = Maps.empty,
Typing.inferenceResultContext = fcx}
-- | Infer the type of a map (Either version)
inferTypeOfMap :: Typing.InferenceContext -> Graph.Graph -> M.Map Core.Term Core.Term -> Either Errors.Error Typing.InferenceResult
inferTypeOfMap fcx cx m =
let kvarResult = Names.freshName fcx
kvar = Pairs.first kvarResult
fcx2 = Pairs.second kvarResult
vvarResult = Names.freshName fcx2
vvar = Pairs.first vvarResult
fcx3 = Pairs.second vvarResult
keyConstraints =
Maps.singleton kvar (Core.TypeVariableConstraints {
Core.typeVariableConstraintsClasses = [
Core.TypeClassConstraintSimple (Core.Name "ordering")]})
in (Logic.ifElse (Maps.null m) (Right (yieldWithConstraints fcx3 (buildTypeApplicationTerm [
kvar,
vvar] (Core.TermMap Maps.empty)) (Core.TypeMap (Core.MapType {
Core.mapTypeKeys = (Core.TypeVariable kvar),
Core.mapTypeValues = (Core.TypeVariable vvar)})) Substitution.idTypeSubst keyConstraints)) (Eithers.bind (inferMany fcx3 cx (Lists.map (\k -> (k, "map key")) (Maps.keys m))) (\kRp ->
let kResults = Pairs.first kRp
fcx4 = Pairs.second kRp
kterms = Pairs.first kResults
ktypes = Pairs.first (Pairs.second kResults)
ksubst = Pairs.first (Pairs.second (Pairs.second kResults))
kElemConstraints = Pairs.second (Pairs.second (Pairs.second kResults))
in (Eithers.bind (inferMany fcx4 (Substitution.substInContext ksubst cx) (Lists.map (\v -> (v, "map value")) (Maps.elems m))) (\vRp ->
let vResults = Pairs.first vRp
fcx5 = Pairs.second vRp
vterms = Pairs.first vResults
vtypes = Pairs.first (Pairs.second vResults)
vsubst = Pairs.first (Pairs.second (Pairs.second vResults))
vElemConstraints = Pairs.second (Pairs.second (Pairs.second vResults))
kcons =
Lists.map (\t -> Typing.TypeConstraint {
Typing.typeConstraintLeft = (Core.TypeVariable kvar),
Typing.typeConstraintRight = t,
Typing.typeConstraintComment = "map key"}) ktypes
vcons =
Lists.map (\t -> Typing.TypeConstraint {
Typing.typeConstraintLeft = (Core.TypeVariable vvar),
Typing.typeConstraintRight = t,
Typing.typeConstraintComment = "map value"}) vtypes
allMapConstraints = mergeClassConstraints keyConstraints (mergeClassConstraints kElemConstraints vElemConstraints)
in (Eithers.bind (mapConstraints fcx5 cx (\subst -> yieldWithConstraints fcx5 (Core.TermMap (Maps.fromList (Lists.zip kterms vterms))) (Core.TypeMap (Core.MapType {
Core.mapTypeKeys = (Core.TypeVariable kvar),
Core.mapTypeValues = (Core.TypeVariable vvar)})) (Substitution.composeTypeSubstList [
ksubst,
vsubst,
subst]) (Substitution.substInClassConstraints subst allMapConstraints)) (Lists.concat [
kcons,
vcons])) (\mcResult -> Right mcResult)))))))
-- | Infer the type of a Maybe value
inferTypeOfOptional :: Typing.InferenceContext -> Graph.Graph -> Maybe Core.Term -> Either Errors.Error Typing.InferenceResult
inferTypeOfOptional fcx cx m =
let trmCons = \terms -> Core.TermOptional (Lists.maybeHead terms)
in (inferTypeOfCollection fcx cx (\x -> Core.TypeOptional x) trmCons "optional element" Sets.empty (Optionals.cases m [] Lists.singleton))
-- | Infer the type of a pair (Either version)
inferTypeOfPair :: Typing.InferenceContext -> Graph.Graph -> (Core.Term, Core.Term) -> Either Errors.Error Typing.InferenceResult
inferTypeOfPair fcx cx p =
Eithers.bind (inferMany fcx cx [
(Pairs.first p, "pair first element"),
(Pairs.second p, "pair second element")]) (\rp ->
let results = Pairs.first rp
fcx2 = Pairs.second rp
iterms = Pairs.first results
itypes = Pairs.first (Pairs.second results)
isubst = Pairs.first (Pairs.second (Pairs.second results))
pairElemConstraints = Pairs.second (Pairs.second (Pairs.second results))
in (Eithers.bind (atOrFail 0 "inferTypeOfPair ifst" iterms) (\ifst -> Eithers.bind (atOrFail 1 "inferTypeOfPair isnd" iterms) (\isnd -> Eithers.bind (atOrFail 0 "inferTypeOfPair tyFst" itypes) (\tyFst -> Eithers.bind (atOrFail 1 "inferTypeOfPair tySnd" itypes) (\tySnd ->
let pairTerm = Core.TermPair (ifst, isnd)
termWithTypes =
Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = (Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = pairTerm,
Core.typeApplicationTermType = tyFst})),
Core.typeApplicationTermType = tySnd})
in (Right (yieldWithConstraints fcx2 termWithTypes (Core.TypePair (Core.PairType {
Core.pairTypeFirst = tyFst,
Core.pairTypeSecond = tySnd})) isubst pairElemConstraints))))))))
-- | Infer the type of a primitive function (Either version)
inferTypeOfPrimitive :: Typing.InferenceContext -> Graph.Graph -> Core.Name -> Either Errors.Error Typing.InferenceResult
inferTypeOfPrimitive fcx cx name =
Optionals.cases (Optionals.map (\_p -> Scoping.termSignatureToTypeScheme (Packaging.primitiveDefinitionSignature (Graph.primitiveDefinition _p))) (Maps.lookup name (Graph.graphPrimitives cx))) (Left (Errors.ErrorResolution (Errors.ResolutionErrorNoSuchPrimitive (Errors.NoSuchPrimitiveError {
Errors.noSuchPrimitiveErrorName = name})))) (\scheme ->
let tsResult = Resolution.instantiateTypeScheme fcx scheme
ts = Pairs.first tsResult
fcx2 = Pairs.second tsResult
constraints = Optionals.fromOptional Maps.empty (Core.typeSchemeConstraints ts)
in (Right (yieldCheckedWithConstraints fcx2 (buildTypeApplicationTerm (Core.typeSchemeVariables ts) (Core.TermVariable name)) (Core.typeSchemeBody ts) Substitution.idTypeSubst constraints)))
-- | Infer the type of a record projection (Either version)
inferTypeOfProjection :: Typing.InferenceContext -> Graph.Graph -> Core.Projection -> Either Errors.Error Typing.InferenceResult
inferTypeOfProjection fcx cx proj =
let tname = Core.projectionTypeName proj
fname = Core.projectionFieldName proj
in (Eithers.bind (Resolution.requireSchemaType fcx (Graph.graphSchemaTypes cx) tname) (\stRp ->
let schemaType = Pairs.first stRp
fcx2 = Pairs.second stRp
svars = Core.typeSchemeVariables schemaType
stype = Core.typeSchemeBody schemaType
in (Eithers.bind (ExtractCore.recordType tname stype) (\sfields -> Eithers.bind (Resolution.findFieldType fcx2 fname sfields) (\ftyp -> Right (yield fcx2 (buildTypeApplicationTerm svars (Core.TermProject (Core.Projection {
Core.projectionTypeName = tname,
Core.projectionFieldName = fname}))) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Resolution.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)),
Core.functionTypeCodomain = ftyp})) Substitution.idTypeSubst))))))
-- | Infer the type of a record (Either version)
inferTypeOfRecord :: Typing.InferenceContext -> Graph.Graph -> Core.Record -> Either Errors.Error Typing.InferenceResult
inferTypeOfRecord fcx cx record =
let tname = Core.recordTypeName record
fields = Core.recordFields record
fnames = Lists.map Core.fieldName fields
in (Eithers.bind (Resolution.requireSchemaType fcx (Graph.graphSchemaTypes cx) tname) (\stRp ->
let schemaType = Pairs.first stRp
fcx2 = Pairs.second stRp
in (Eithers.bind (inferMany fcx2 cx (Lists.map (\f -> (Core.fieldTerm f, (Strings.cat2 "field " (Core.unName (Core.fieldName f))))) fields)) (\rp ->
let results = Pairs.first rp
fcx3 = Pairs.second rp
svars = Core.typeSchemeVariables schemaType
stype = Core.typeSchemeBody schemaType
iterms = Pairs.first results
itypes = Pairs.first (Pairs.second results)
isubst = Pairs.first (Pairs.second (Pairs.second results))
recElemConstraints = Pairs.second (Pairs.second (Pairs.second results))
ityp =
Core.TypeRecord (Lists.zipWith (\n -> \t -> Core.FieldType {
Core.fieldTypeName = n,
Core.fieldTypeType = t}) fnames itypes)
in (Eithers.bind (mapConstraints fcx3 cx (\subst -> yieldWithConstraints fcx3 (buildTypeApplicationTerm svars (Core.TermRecord (Core.Record {
Core.recordTypeName = tname,
Core.recordFields = (Lists.zipWith (\n -> \t -> Core.Field {
Core.fieldName = n,
Core.fieldTerm = t}) fnames iterms)}))) (Resolution.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)) (Substitution.composeTypeSubst isubst subst) (Substitution.substInClassConstraints subst recElemConstraints)) [
Typing.TypeConstraint {
Typing.typeConstraintLeft = stype,
Typing.typeConstraintRight = ityp,
Typing.typeConstraintComment = "schema type of record"}]) (\mcResult -> Right mcResult))))))
-- | Infer the type of a set (Either version)
inferTypeOfSet :: Typing.InferenceContext -> Graph.Graph -> S.Set Core.Term -> Either Errors.Error Typing.InferenceResult
inferTypeOfSet fcx cx s =
inferTypeOfCollection fcx cx (\x -> Core.TypeSet x) (\terms -> Core.TermSet (Sets.fromList terms)) "set element" (Sets.singleton (Core.Name "ordering")) (Sets.toList s)
-- | Infer the type of a given term (Either version)
inferTypeOfTerm :: Typing.InferenceContext -> Graph.Graph -> Core.Term -> String -> Either Errors.Error Typing.InferenceResult
inferTypeOfTerm fcx cx term desc =
let fcx2 = fcx
in case term of
Core.TermAnnotated v0 -> inferTypeOfAnnotatedTerm fcx2 cx v0
Core.TermApplication v0 -> inferTypeOfApplication fcx2 cx v0
Core.TermCases v0 -> inferTypeOfCaseStatement fcx2 cx v0
Core.TermEither v0 -> inferTypeOfEither fcx2 cx v0
Core.TermLambda v0 -> inferTypeOfLambda fcx2 cx v0
Core.TermLet v0 -> inferTypeOfLet fcx2 cx v0
Core.TermList v0 -> inferTypeOfList fcx2 cx v0
Core.TermLiteral v0 -> Right (inferTypeOfLiteral fcx2 v0)
Core.TermMap v0 -> inferTypeOfMap fcx2 cx v0
Core.TermOptional v0 -> inferTypeOfOptional fcx2 cx v0
Core.TermPair v0 -> inferTypeOfPair fcx2 cx v0
Core.TermProject v0 -> inferTypeOfProjection fcx2 cx v0
Core.TermRecord v0 -> inferTypeOfRecord fcx2 cx v0
Core.TermSet v0 -> inferTypeOfSet fcx2 cx v0
Core.TermTypeApplication v0 -> inferTypeOfTypeApplication fcx2 cx v0
Core.TermTypeLambda v0 -> inferTypeOfTypeLambda fcx2 cx v0
Core.TermInject v0 -> inferTypeOfInjection fcx2 cx v0
Core.TermUnit -> Right (inferTypeOfUnit fcx2)
Core.TermUnwrap v0 -> inferTypeOfUnwrap fcx2 cx v0
Core.TermVariable v0 -> inferTypeOfVariable fcx2 cx v0
Core.TermWrap v0 -> inferTypeOfWrappedTerm fcx2 cx v0
-- | Infer the type of a type application (Either version)
inferTypeOfTypeApplication :: Typing.InferenceContext -> Graph.Graph -> Core.TypeApplicationTerm -> Either Errors.Error Typing.InferenceResult
inferTypeOfTypeApplication fcx cx tt =
let fcxBody = Names.pushSubtermStep Paths.SubtermStepTypeApplicationTerm fcx
in (Eithers.bind (inferTypeOfTerm fcxBody cx (Core.typeApplicationTermBody tt) "type application term") (\result ->
let fcx2 = Names.restoreTrace fcx (Typing.inferenceResultContext result)
in (Right (Typing.InferenceResult {
Typing.inferenceResultTerm = (Typing.inferenceResultTerm result),
Typing.inferenceResultType = (Typing.inferenceResultType result),
Typing.inferenceResultSubst = (Typing.inferenceResultSubst result),
Typing.inferenceResultClassConstraints = (Typing.inferenceResultClassConstraints result),
Typing.inferenceResultContext = fcx2}))))
-- | Infer the type of a type abstraction (Either version)
inferTypeOfTypeLambda :: Typing.InferenceContext -> Graph.Graph -> Core.TypeLambda -> Either Errors.Error Typing.InferenceResult
inferTypeOfTypeLambda fcx cx ta =
let fcxBody = Names.pushSubtermStep Paths.SubtermStepTypeLambdaBody fcx
in (Eithers.bind (inferTypeOfTerm fcxBody cx (Core.typeLambdaBody ta) "type abstraction") (\result ->
let fcx2 = Names.restoreTrace fcx (Typing.inferenceResultContext result)
in (Right (Typing.InferenceResult {
Typing.inferenceResultTerm = (Typing.inferenceResultTerm result),
Typing.inferenceResultType = (Typing.inferenceResultType result),
Typing.inferenceResultSubst = (Typing.inferenceResultSubst result),
Typing.inferenceResultClassConstraints = (Typing.inferenceResultClassConstraints result),
Typing.inferenceResultContext = fcx2}))))
-- | The trivial inference rule for the unit term
inferTypeOfUnit :: Typing.InferenceContext -> Typing.InferenceResult
inferTypeOfUnit fcx =
Typing.InferenceResult {
Typing.inferenceResultTerm = Core.TermUnit,
Typing.inferenceResultType = Core.TypeUnit,
Typing.inferenceResultSubst = Substitution.idTypeSubst,
Typing.inferenceResultClassConstraints = Maps.empty,
Typing.inferenceResultContext = fcx}
-- | Infer the type of an unwrap operation (Either version)
inferTypeOfUnwrap :: Typing.InferenceContext -> Graph.Graph -> Core.Name -> Either Errors.Error Typing.InferenceResult
inferTypeOfUnwrap fcx cx tname =
Eithers.bind (Resolution.requireSchemaType fcx (Graph.graphSchemaTypes cx) tname) (\stRp ->
let schemaType = Pairs.first stRp
fcx2 = Pairs.second stRp
svars = Core.typeSchemeVariables schemaType
stype = Core.typeSchemeBody schemaType
in (Eithers.bind (ExtractCore.wrappedType tname stype) (\wtyp -> Right (yield fcx2 (buildTypeApplicationTerm svars (Core.TermUnwrap tname)) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Resolution.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)),
Core.functionTypeCodomain = wtyp})) Substitution.idTypeSubst))))
-- | Infer the type of a variable (Either version)
inferTypeOfVariable :: Typing.InferenceContext -> Graph.Graph -> Core.Name -> Either Errors.Error Typing.InferenceResult
inferTypeOfVariable fcx cx name =
Optionals.cases (Maps.lookup name (Graph.graphBoundTypes cx)) (Optionals.cases (Optionals.map (\_p -> Scoping.termSignatureToTypeScheme (Packaging.primitiveDefinitionSignature (Graph.primitiveDefinition _p))) (Maps.lookup name (Graph.graphPrimitives cx))) (Left (Errors.ErrorResolution (Errors.ResolutionErrorNoSuchBinding (Errors.NoSuchBindingError {
Errors.noSuchBindingErrorName = name})))) (\scheme ->
let tsResult = Resolution.instantiateTypeScheme fcx scheme
ts = Pairs.first tsResult
fcx2 = Pairs.second tsResult
constraints = Optionals.fromOptional Maps.empty (Core.typeSchemeConstraints ts)
in (Right (yieldCheckedWithConstraints fcx2 (buildTypeApplicationTerm (Core.typeSchemeVariables ts) (Core.TermVariable name)) (Core.typeSchemeBody ts) Substitution.idTypeSubst constraints)))) (\scheme ->
let tsResult = Resolution.instantiateTypeScheme fcx scheme
ts = Pairs.first tsResult
fcx2 = Pairs.second tsResult
constraints = Optionals.fromOptional Maps.empty (Core.typeSchemeConstraints ts)
in (Right (Typing.InferenceResult {
Typing.inferenceResultTerm = (buildTypeApplicationTerm (Core.typeSchemeVariables ts) (Core.TermVariable name)),
Typing.inferenceResultType = (Core.typeSchemeBody ts),
Typing.inferenceResultSubst = Substitution.idTypeSubst,
Typing.inferenceResultClassConstraints = constraints,
Typing.inferenceResultContext = fcx2})))
-- | Infer the type of a wrapped term (Either version)
inferTypeOfWrappedTerm :: Typing.InferenceContext -> Graph.Graph -> Core.WrappedTerm -> Either Errors.Error Typing.InferenceResult
inferTypeOfWrappedTerm fcx cx wt =
let tname = Core.wrappedTermTypeName wt
term = Core.wrappedTermBody wt
in (Eithers.bind (Resolution.requireSchemaType fcx (Graph.graphSchemaTypes cx) tname) (\stRp ->
let schemaType = Pairs.first stRp
fcx2 = Pairs.second stRp
fcxBody = Names.pushSubtermStep Paths.SubtermStepWrappedTerm fcx2
in (Eithers.bind (inferTypeOfTerm fcxBody cx term "wrapped term") (\result ->
let fcx3 = Names.restoreTrace fcx2 (Typing.inferenceResultContext result)
svars = Core.typeSchemeVariables schemaType
stype = Core.typeSchemeBody schemaType
iterm = Typing.inferenceResultTerm result
itype = Typing.inferenceResultType result
isubst = Typing.inferenceResultSubst result
ityp = Core.TypeWrap itype
in (Eithers.bind (mapConstraints fcx3 cx (\subst -> yield fcx3 (buildTypeApplicationTerm svars (Core.TermWrap (Core.WrappedTerm {
Core.wrappedTermTypeName = tname,
Core.wrappedTermBody = iterm}))) (Resolution.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)) (Substitution.composeTypeSubst isubst subst)) [
Typing.TypeConstraint {
Typing.typeConstraintLeft = stype,
Typing.typeConstraintRight = ityp,
Typing.typeConstraintComment = "schema type of wrapper"}]) (\mcResult -> Right mcResult))))))
-- | Infer types for temporary let bindings (Either version)
inferTypesOfTemporaryBindings :: Typing.InferenceContext -> Graph.Graph -> [Core.Binding] -> Either Errors.Error (
([Core.Term], ([Core.Type], (Typing.TypeSubst, (M.Map Core.Name Core.TypeVariableConstraints)))),
Typing.InferenceContext)
inferTypesOfTemporaryBindings fcx cx bins =
let emptyResult = Right (([], ([], (Substitution.idTypeSubst, Maps.empty))), fcx)
in (Optionals.cases (Lists.uncons bins) emptyResult (\binsUc ->
let binding = Pairs.first binsUc
tl = Pairs.second binsUc
k = Core.bindingName binding
v = Core.bindingTerm binding
fcxBind = Names.pushSubtermStep (Paths.SubtermStepLetBinding k) fcx
in (Eithers.bind (inferTypeOfTerm fcxBind cx v (Strings.cat [
"temporary let binding '",
(Core.unName k),
"'"])) (\result1 ->
let fcx2 = Names.restoreTrace fcx (Typing.inferenceResultContext result1)
j = Typing.inferenceResultTerm result1
u_prime = Typing.inferenceResultType result1
u = Typing.inferenceResultSubst result1
c1Inferred = Typing.inferenceResultClassConstraints result1
in (Eithers.bind (Optionals.cases (Core.bindingTypeScheme binding) (Right Maps.empty) (\ts ->
let tsResult = Resolution.instantiateTypeScheme fcx2 ts
instantiatedTs = Pairs.first tsResult
freshConstraints = Optionals.fromOptional Maps.empty (Core.typeSchemeConstraints instantiatedTs)
in (Eithers.bind (Eithers.bimap (\_e -> Errors.ErrorInference (Errors.InferenceErrorUnification (Errors.UnificationInferenceError {
Errors.unificationInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace fcx2))),
Errors.unificationInferenceErrorCause = _e}))) (\_a -> _a) (Unification.unifyTypes fcx2 (Graph.graphSchemaTypes cx) (Core.typeSchemeBody instantiatedTs) u_prime "original binding type")) (\unifySubst -> Right (Substitution.substInClassConstraints unifySubst freshConstraints))))) (\originalBindingConstraints ->
let c1 = mergeClassConstraints c1Inferred originalBindingConstraints
in (Eithers.bind (inferTypesOfTemporaryBindings fcx2 (Substitution.substInContext u cx) tl) (\rp2 ->
let result2 = Pairs.first rp2
fcx3 = Pairs.second rp2
h = Pairs.first result2
r_prime = Pairs.first (Pairs.second result2)
restPair = Pairs.second (Pairs.second result2)
r = Pairs.first restPair
c2 = Pairs.second restPair
c1Subst = Substitution.substInClassConstraints r c1
mergedConstraints = mergeClassConstraints c1Subst c2
in (Right (
(
Lists.cons (Substitution.substTypesInTerm r j) h,
(Lists.cons (Substitution.substInType r u_prime) r_prime, (Substitution.composeTypeSubst u r, mergedConstraints))),
fcx3))))))))))
-- | Check if a variable is unbound in context
isUnbound :: Graph.Graph -> Core.Name -> Bool
isUnbound cx v =
Logic.and (Logic.not (Sets.member v (freeVariablesInContext cx))) (Logic.not (Maps.member v (Graph.graphSchemaTypes cx)))
-- | Map over type constraints after unification
mapConstraints :: Typing.InferenceContext -> Graph.Graph -> (Typing.TypeSubst -> t0) -> [Typing.TypeConstraint] -> Either Errors.Error t0
mapConstraints flowCx cx f constraints =
Eithers.bind (Eithers.bimap (\_e -> Errors.ErrorInference (Errors.InferenceErrorUnification (Errors.UnificationInferenceError {
Errors.unificationInferenceErrorPath = (Paths.SubtermPath (Lists.reverse (Typing.inferenceContextTrace flowCx))),
Errors.unificationInferenceErrorCause = _e}))) (\_a -> _a) (Unification.unifyTypeConstraints flowCx (Graph.graphSchemaTypes cx) constraints)) (\s -> Eithers.bind (Checking.checkTypeSubst flowCx cx s) (\_ -> Right (f s)))
-- | Merge two maps of class constraints. When both maps have constraints for the same variable, union the class sets.
mergeClassConstraints :: Ord t0 => (M.Map t0 Core.TypeVariableConstraints -> M.Map t0 Core.TypeVariableConstraints -> M.Map t0 Core.TypeVariableConstraints)
mergeClassConstraints m1 m2 =
Lists.foldl (\acc -> \pair ->
let k = Pairs.first pair
v = Pairs.second pair
in (Optionals.cases (Maps.lookup k acc) (Maps.insert k v acc) (\existing ->
let merged =
Core.TypeVariableConstraints {
Core.typeVariableConstraintsClasses = (Lists.nub (Lists.concat2 (Core.typeVariableConstraintsClasses existing) (Core.typeVariableConstraintsClasses v)))}
in (Maps.insert k merged acc)))) m1 (Maps.toList m2)
-- | Show an inference result for debugging
showInferenceResult :: Typing.InferenceResult -> String
showInferenceResult result =
let term = Typing.inferenceResultTerm result
typ = Typing.inferenceResultType result
subst = Typing.inferenceResultSubst result
in (Strings.cat [
"{term=",
(ShowCore.term term),
", type=",
(ShowCore.type_ typ),
", subst=",
(ShowTyping.typeSubst subst),
"}"])
-- | Create an inference result with no class constraints
yield :: Typing.InferenceContext -> Core.Term -> Core.Type -> Typing.TypeSubst -> Typing.InferenceResult
yield fcx term typ subst =
Typing.InferenceResult {
Typing.inferenceResultTerm = (Substitution.substTypesInTerm subst term),
Typing.inferenceResultType = (Substitution.substInType subst typ),
Typing.inferenceResultSubst = subst,
Typing.inferenceResultClassConstraints = Maps.empty,
Typing.inferenceResultContext = fcx}
-- | Create a checked inference result
yieldChecked :: Typing.InferenceContext -> Core.Term -> Core.Type -> Typing.TypeSubst -> Typing.InferenceResult
yieldChecked fcx term typ subst =
let iterm = Substitution.substTypesInTerm subst term
itype = Substitution.substInType subst typ
in Typing.InferenceResult {
Typing.inferenceResultTerm = iterm,
Typing.inferenceResultType = itype,
Typing.inferenceResultSubst = subst,
Typing.inferenceResultClassConstraints = Maps.empty,
Typing.inferenceResultContext = fcx}
-- | Create a checked inference result with class constraints
yieldCheckedWithConstraints :: Typing.InferenceContext -> Core.Term -> Core.Type -> Typing.TypeSubst -> M.Map Core.Name Core.TypeVariableConstraints -> Typing.InferenceResult
yieldCheckedWithConstraints fcx term typ subst constraints =
let iterm = Substitution.substTypesInTerm subst term
itype = Substitution.substInType subst typ
iconstraints = Substitution.substInClassConstraints subst constraints
in Typing.InferenceResult {
Typing.inferenceResultTerm = iterm,
Typing.inferenceResultType = itype,
Typing.inferenceResultSubst = subst,
Typing.inferenceResultClassConstraints = iconstraints,
Typing.inferenceResultContext = fcx}
-- | Create an inference result with class constraints
yieldWithConstraints :: Typing.InferenceContext -> Core.Term -> Core.Type -> Typing.TypeSubst -> M.Map Core.Name Core.TypeVariableConstraints -> Typing.InferenceResult
yieldWithConstraints fcx term typ subst constraints =
Typing.InferenceResult {
Typing.inferenceResultTerm = (Substitution.substTypesInTerm subst term),
Typing.inferenceResultType = (Substitution.substInType subst typ),
Typing.inferenceResultSubst = subst,
Typing.inferenceResultClassConstraints = constraints,
Typing.inferenceResultContext = fcx}