hydra-kernel-0.17.2: src/main/haskell/Hydra/Checking.hs
-- Note: this is an automatically generated file. Do not edit.
-- | Type checking and type reconstruction (type-of) for the results of Hydra unification and inference
module Hydra.Checking where
import qualified Hydra.Ast as Ast
import qualified Hydra.Coders as Coders
import qualified Hydra.Constants as Constants
import qualified Hydra.Core as Core
import qualified Hydra.Dependencies as Dependencies
import qualified Hydra.Docs as Docs
import qualified Hydra.Error.Checking as Checking
import qualified Hydra.Error.Core as ErrorCore
import qualified Hydra.Error.File as ErrorFile
import qualified Hydra.Error.Packaging as ErrorPackaging
import qualified Hydra.Error.System as ErrorSystem
import qualified Hydra.Errors as Errors
import qualified Hydra.Extract.Core as ExtractCore
import qualified Hydra.File as File
import qualified Hydra.Formatting as Formatting
import qualified Hydra.Graph as Graph
import qualified Hydra.Json.Model as Model
import qualified Hydra.Lexical as Lexical
import qualified Hydra.Overlay.Haskell.Lib.Eithers as Eithers
import qualified Hydra.Overlay.Haskell.Lib.Equality as Equality
import qualified Hydra.Overlay.Haskell.Lib.Lists as Lists
import qualified Hydra.Overlay.Haskell.Lib.Literals as Literals
import qualified Hydra.Overlay.Haskell.Lib.Logic as Logic
import qualified Hydra.Overlay.Haskell.Lib.Maps as Maps
import qualified Hydra.Overlay.Haskell.Lib.Optionals as Optionals
import qualified Hydra.Overlay.Haskell.Lib.Pairs as Pairs
import qualified Hydra.Overlay.Haskell.Lib.Sets as Sets
import qualified Hydra.Overlay.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.Print.Core as PrintCore
import qualified Hydra.Print.Errors as PrintErrors
import qualified Hydra.Print.Variants as PrintVariants
import qualified Hydra.Query as Query
import qualified Hydra.Reflect as Reflect
import qualified Hydra.Regex as Regex
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.Strip as Strip
import qualified Hydra.Substitution as Substitution
import qualified Hydra.System as System
import qualified Hydra.Tabular as Tabular
import qualified Hydra.Testing as Testing
import qualified Hydra.Time as Time
import qualified Hydra.Topology as Topology
import qualified Hydra.Typed as Typed
import qualified Hydra.Typing as Typing
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
-- | True if every element of the list is equal to every other element (vacuously true for the empty list)
allEqual :: Eq t0 => ([t0] -> Bool)
allEqual els =
Optionals.cases (Lists.uncons els) True (\uc ->
let h = Pairs.first uc
t = Pairs.second uc
in (Lists.foldl (\b -> \x -> Logic.and b (Equality.equal x h)) True t))
-- | Apply type arguments to a type, substituting forall-bound variables. Paper: inference.tex, 'Checking the witness' (consuming the pending-type-argument stack).
applyTypeArgumentsToType :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Type -> Either Errors.Error Core.Type
applyTypeArgumentsToType cx tx typeArgs t =
Optionals.cases (Lists.uncons typeArgs) (Right t) (\uc ->
let ah = Pairs.first uc
at = Pairs.second uc
in case t of
Core.TypeForall v0 ->
let v = Core.forallTypeParameter v0
tbody = Core.forallTypeBody v0
in (applyTypeArgumentsToType cx tx at (Substitution.substInType (Typing.TypeSubst (Maps.singleton v ah)) tbody))
Core.TypeVariable v0 -> Eithers.either (\_ -> Left (Errors.ErrorExtraction (Errors.ExtractionErrorUnexpectedShape (Errors.UnexpectedShapeError {
Errors.unexpectedShapeErrorExpected = "forall type",
Errors.unexpectedShapeErrorActual = (Strings.cat [
PrintCore.type_ t,
". Trying to apply ",
(Literals.showInt32 (Lists.length typeArgs)),
" type args: ",
(Formatting.showList PrintCore.type_ typeArgs)])})))) (\schemaRes ->
let schemaType = Pairs.first schemaRes
schemaBody = Strip.deannotateType (Core.typeSchemeBody schemaType)
in case schemaBody of
Core.TypeForall _ -> applyTypeArgumentsToType cx tx typeArgs schemaBody
_ -> Right t) (Resolution.requireSchemaType cx (Graph.graphSchemaTypes tx) v0)
_ -> Left (Errors.ErrorExtraction (Errors.ExtractionErrorUnexpectedShape (Errors.UnexpectedShapeError {
Errors.unexpectedShapeErrorExpected = "forall type",
Errors.unexpectedShapeErrorActual = (Strings.cat [
PrintCore.type_ t,
". Trying to apply ",
(Literals.showInt32 (Lists.length typeArgs)),
" type args: ",
(Formatting.showList PrintCore.type_ typeArgs),
". Context has vars: {",
(Strings.intercalate ", " (Lists.map Core.unName (Maps.keys (Graph.graphBoundTypes tx)))),
"}"])}))))
-- | Check that a term has no unbound type variables (Either version). Paper: inference.tex, 'Checking the witness' (always-on finalization invariant).
checkForUnboundTypeVariables :: t0 -> Graph.Graph -> Core.Term -> Either Errors.Error ()
checkForUnboundTypeVariables cx tx term0 =
let svars = Sets.fromList (Maps.keys (Graph.graphSchemaTypes tx))
checkRecursive =
\vars -> \trace -> \lbinding -> \term ->
let recurse = checkRecursive vars trace lbinding
dflt = Eithers.bind (Eithers.mapList recurse (Rewriting.subterms term)) (\_ -> Right ())
check =
\typ ->
let freevars = Variables.freeVariablesInType typ
badvars = Sets.difference (Sets.difference freevars vars) svars
in (Logic.ifElse (Sets.null badvars) (Right ()) (Left (Errors.ErrorChecking (Checking.CheckingErrorUnboundTypeVariables (Checking.UnboundTypeVariablesError {
Checking.unboundTypeVariablesErrorVariables = badvars,
Checking.unboundTypeVariablesErrorType = typ})))))
checkOptional = \m -> Eithers.bind (Eithers.mapOptional check m) (\_ -> Right ())
in case term of
Core.TermLambda v0 -> Eithers.bind (checkOptional (Core.lambdaDomain v0)) (\_ -> recurse (Core.lambdaBody v0))
Core.TermLet v0 ->
let forBinding =
\b ->
let bterm = Core.bindingTerm b
newVars =
Optionals.cases (Core.bindingTypeScheme b) vars (\ts -> Sets.union vars (Sets.fromList (Core.typeSchemeVariables ts)))
newTrace = Lists.cons (Core.unName (Core.bindingName b)) trace
in (checkRecursive newVars newTrace (Just b) bterm)
in (Eithers.bind (Eithers.mapList forBinding (Core.letBindings v0)) (\_ -> recurse (Core.letBody v0)))
Core.TermTypeApplication v0 -> Eithers.bind (check (Core.typeApplicationTermType v0)) (\_ -> recurse (Core.typeApplicationTermBody v0))
Core.TermTypeLambda v0 -> Eithers.bind (check (Core.TypeVariable (Core.typeLambdaParameter v0))) (\_ -> recurse (Core.typeLambdaBody v0))
_ -> dflt
in (checkRecursive Sets.empty [
"top level"] Nothing term0)
-- | Ensure all types in a list are equal and return the common type
checkSameType :: t0 -> Graph.Graph -> String -> [Core.Type] -> Either Errors.Error Core.Type
checkSameType cx tx desc types =
let unequalErr =
Left (Errors.ErrorChecking (Checking.CheckingErrorUnequalTypes (Checking.UnequalTypesError {
Checking.unequalTypesErrorTypes = types,
Checking.unequalTypesErrorDescription = desc})))
in (Logic.ifElse (typesAllEffectivelyEqual tx types) (Optionals.cases (Lists.maybeHead types) unequalErr (\t -> Right t)) unequalErr)
-- | Sanity-check a type substitution arising from unification. Specifically, check that schema types have not been inappropriately unified with type variables inferred from terms. Paper: inference.tex, 'Checking the witness' (always-on invariant: a substitution may not bind a type name as if it were an inference variable).
checkTypeSubst :: t0 -> Graph.Graph -> Typing.TypeSubst -> Either Errors.Error Typing.TypeSubst
checkTypeSubst cx tx subst =
let s = Typing.unTypeSubst subst
vars = Sets.fromList (Maps.keys s)
suspectVars = Sets.intersection vars (Sets.fromList (Maps.keys (Graph.graphSchemaTypes tx)))
isNominal =
\ts -> case (Strip.deannotateType (Core.typeSchemeBody ts)) of
Core.TypeRecord _ -> True
Core.TypeUnion _ -> True
Core.TypeWrap _ -> True
_ -> False
badVars =
Sets.fromList (Lists.filter (\v -> Optionals.cases (Lexical.dereferenceSchemaType v (Graph.graphSchemaTypes tx)) False isNominal) (Sets.toList suspectVars))
badPairs = Lists.filter (\p -> Sets.member (Pairs.first p) badVars) (Maps.toList s)
printPair = \p -> Strings.cat2 (Strings.cat2 (Core.unName (Pairs.first p)) " --> ") (PrintCore.type_ (Pairs.second p))
in (Logic.ifElse (Sets.null badVars) (Right subst) (Left (Errors.ErrorChecking (Checking.CheckingErrorIncorrectUnification (Checking.IncorrectUnificationError {
Checking.incorrectUnificationErrorSubstitution = subst})))))
-- | Check if a type contains any type variable from the current scope
containsInScopeTypeVars :: Graph.Graph -> Core.Type -> Bool
containsInScopeTypeVars tx t =
let vars = Graph.graphTypeVariables tx
freeVars = Variables.freeVariablesInTypeSimple t
in (Logic.not (Sets.null (Sets.intersection vars freeVars)))
-- | Normalize free type variables in a type to canonical names based on order of first occurrence. This allows comparing types that differ only in the naming of free type variables. Paper: inference.tex, 'Checking the witness' (effective equality).
normalizeTypeFreeVars :: Core.Type -> Core.Type
normalizeTypeFreeVars typ =
let collectVars =
\acc -> \t -> case t of
Core.TypeVariable v0 -> Logic.ifElse (Maps.member v0 acc) acc (Maps.insert v0 (Core.Name (Strings.cat2 "_tv" (Literals.showInt32 (Maps.size acc)))) acc)
_ -> acc
subst = Rewriting.foldOverType Coders.TraversalOrderPre collectVars Maps.empty typ
in (Variables.substituteTypeVariables subst typ)
-- | Get the bound types from a graph as a type environment
toFContext :: Graph.Graph -> M.Map Core.Name Core.Type
toFContext cx = Maps.map Scoping.typeSchemeToFType (Graph.graphBoundTypes cx)
-- | Check whether two lists of types are effectively equal, disregarding type aliases
typeListsEffectivelyEqual :: Graph.Graph -> [Core.Type] -> [Core.Type] -> Bool
typeListsEffectivelyEqual tx tlist1 tlist2 =
Logic.ifElse (Equality.equal (Lists.length tlist1) (Lists.length tlist2)) (Lists.foldl Logic.and True (Lists.zipWith (typesEffectivelyEqual tx) tlist1 tlist2)) False
-- | Given a type context, reconstruct the type of a System F term. Paper: inference.tex, 'Checking the witness' -- the executable form of the System F typing judgment in the soundness theorem.
typeOf :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Term -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOf cx tx typeArgs term =
let cx1 = cx
in case term of
Core.TermAnnotated v0 -> typeOfAnnotatedTerm cx1 tx typeArgs v0
Core.TermApplication v0 -> typeOfApplication cx1 tx typeArgs v0
Core.TermCases v0 -> typeOfCaseStatement cx1 tx typeArgs v0
Core.TermEither v0 -> typeOfEither cx1 tx typeArgs v0
Core.TermLambda v0 -> typeOfLambda cx1 tx typeArgs v0
Core.TermLet v0 -> typeOfLet cx1 tx typeArgs v0
Core.TermList v0 -> typeOfList cx1 tx typeArgs v0
Core.TermLiteral v0 -> typeOfLiteral cx1 tx typeArgs v0
Core.TermMap v0 -> typeOfMap cx1 tx typeArgs v0
Core.TermOptional v0 -> typeOfMaybe cx1 tx typeArgs v0
Core.TermPair v0 -> typeOfPair cx1 tx typeArgs v0
Core.TermProject v0 -> typeOfProjection cx1 tx typeArgs v0
Core.TermRecord v0 -> typeOfRecord cx1 tx typeArgs v0
Core.TermSet v0 -> typeOfSet cx1 tx typeArgs v0
Core.TermTypeApplication v0 -> typeOfTypeApplication cx1 tx typeArgs v0
Core.TermTypeLambda v0 -> typeOfTypeLambda cx1 tx typeArgs v0
Core.TermInject v0 -> typeOfInjection cx1 tx typeArgs v0
Core.TermUnit -> typeOfUnit cx1 tx typeArgs
Core.TermUnwrap v0 -> typeOfUnwrap cx1 tx typeArgs v0
Core.TermVariable v0 -> typeOfVariable cx1 tx typeArgs v0
Core.TermWrap v0 -> typeOfWrappedTerm cx1 tx typeArgs v0
_ -> Left (Errors.ErrorChecking (Checking.CheckingErrorUnsupportedTermVariant (Checking.UnsupportedTermVariantError {
Checking.unsupportedTermVariantErrorTermVariant = (Reflect.termVariant term)})))
-- | Reconstruct the type of an annotated term (Either/InferenceContext version). Paper: inference.tex, rule Ann (checking side).
typeOfAnnotatedTerm :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.AnnotatedTerm -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfAnnotatedTerm cx tx typeArgs at = typeOf cx tx typeArgs (Core.annotatedTermBody at)
-- | Reconstruct the type of an application term (Either/InferenceContext version). Paper: inference.tex, rule App (checking side).
typeOfApplication :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Application -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfApplication cx tx typeArgs app =
let fun = Core.applicationFunction app
arg = Core.applicationArgument app
tryType =
\cx0 -> \tfun -> \targ -> case tfun of
Core.TypeForall v0 -> tryType cx0 (Core.forallTypeBody v0) targ
Core.TypeFunction v0 ->
let dom = Core.functionTypeDomain v0
cod = Core.functionTypeCodomain v0
in (Logic.ifElse (typesEffectivelyEqual tx dom targ) (Right (cod, cx0)) (Left (Errors.ErrorChecking (Checking.CheckingErrorTypeMismatch (Checking.TypeMismatchError {
Checking.typeMismatchErrorExpectedType = dom,
Checking.typeMismatchErrorActualType = targ})))))
Core.TypeVariable _ ->
let nameResult = Names.freshName cx0
freshN = Pairs.first nameResult
cx1 = Pairs.second nameResult
in (Right (Core.TypeVariable freshN, cx1))
_ -> Left (Errors.ErrorChecking (Checking.CheckingErrorNotAFunctionType (Checking.NotAFunctionTypeError {
Checking.notAFunctionTypeErrorType = tfun})))
in (Eithers.bind (typeOf cx tx [] fun) (\result1 ->
let tfun = Pairs.first result1
cx2 = Pairs.second result1
in (Eithers.bind (typeOf cx2 tx [] arg) (\result2 ->
let targ = Pairs.first result2
cx3 = Pairs.second result2
in (Eithers.bind (tryType cx3 tfun targ) (\result3 ->
let t = Pairs.first result3
cx4 = Pairs.second result3
in (Eithers.bind (applyTypeArgumentsToType cx4 tx typeArgs t) (\applied -> Right (applied, cx4)))))))))
-- | Reconstruct the type of a case statement (Either/InferenceContext version). Paper: inference.tex, rules Case and Case_d (checking side).
typeOfCaseStatement :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.CaseStatement -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfCaseStatement cx tx typeArgs cs =
let tname = Core.caseStatementTypeName cs
dflt = Core.caseStatementDefault cs
cases = Core.caseStatementCases cs
cterms = Lists.map Core.caseAlternativeHandler cases
in (Eithers.bind (Eithers.mapOptional (\e -> typeOf cx tx [] e) dflt) (\dfltResult ->
let tdflt = Optionals.map Pairs.first dfltResult
cx2 = Optionals.cases dfltResult cx Pairs.second
foldResult =
Lists.foldl (\acc -> \term -> Eithers.bind acc (\accR ->
let types = Pairs.first accR
cxA = Pairs.second accR
in (Eithers.bind (typeOf cxA tx [] term) (\tResult ->
let t = Pairs.first tResult
cxB = Pairs.second tResult
in (Right (Lists.concat2 types (Lists.pure t), cxB)))))) (Right ([], cx2)) cterms
in (Eithers.bind foldResult (\foldR ->
let tcterms = Pairs.first foldR
cx3 = Pairs.second foldR
fcodsResult =
Lists.foldl (\acc -> \t -> Eithers.bind acc (\accR ->
let cods = Pairs.first accR
in (Eithers.bind (ExtractCore.functionType t) (\ft -> Right (Lists.concat2 cods (Lists.pure (Core.functionTypeCodomain ft)), cx3))))) (Right ([], cx3)) tcterms
in (Eithers.bind fcodsResult (\fcodsR ->
let fcods = Pairs.first fcodsR
cods = Optionals.cat (Lists.cons tdflt (Lists.map Optionals.pure fcods))
in (Eithers.bind (checkSameType cx3 tx "case branches" cods) (\cod -> Right (
Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Resolution.nominalApplication tname typeArgs),
Core.functionTypeCodomain = cod}),
cx3)))))))))
-- | Reconstruct the type of an either value (Either/InferenceContext version). Paper: inference.tex, rules Eith_L and Eith_R (checking side).
typeOfEither :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Either Core.Term Core.Term -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfEither cx tx typeArgs et =
let n = Lists.length typeArgs
arityErr =
Left (Errors.ErrorChecking (Checking.CheckingErrorTypeArityMismatch (Checking.TypeArityMismatchError {
Checking.typeArityMismatchErrorType = (Core.TypeEither (Core.EitherType {
Core.eitherTypeLeft = Core.TypeUnit,
Core.eitherTypeRight = Core.TypeUnit})),
Checking.typeArityMismatchErrorExpectedArity = 2,
Checking.typeArityMismatchErrorActualArity = n,
Checking.typeArityMismatchErrorTypeArguments = typeArgs})))
in (Optionals.cases (Lists.uncons typeArgs) arityErr (\uc0 ->
let ta0 = Pairs.first uc0
in (Optionals.cases (Lists.uncons (Pairs.second uc0)) arityErr (\uc1 ->
let ta1 = Pairs.first uc1
in (Logic.ifElse (Equality.equal n 2) (Eithers.either (\leftTerm -> Eithers.bind (typeOf cx tx [] leftTerm) (\result ->
let leftType = Pairs.first result
cx2 = Pairs.second result
in (Right (
Core.TypeEither (Core.EitherType {
Core.eitherTypeLeft = leftType,
Core.eitherTypeRight = ta1}),
cx2)))) (\rightTerm -> Eithers.bind (typeOf cx tx [] rightTerm) (\result ->
let rightType = Pairs.first result
cx2 = Pairs.second result
in (Right (
Core.TypeEither (Core.EitherType {
Core.eitherTypeLeft = ta0,
Core.eitherTypeRight = rightType}),
cx2)))) et) arityErr)))))
-- | Reconstruct the type of a union injection (Either/InferenceContext version). Paper: inference.tex, rule Inj (checking side).
typeOfInjection :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Injection -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfInjection cx tx typeArgs injection =
let tname = Core.injectionTypeName injection
field = Core.injectionField injection
fname = Core.fieldName field
fterm = Core.fieldTerm field
in (Eithers.bind (Resolution.requireSchemaType cx (Graph.graphSchemaTypes tx) tname) (\schemaResult ->
let schemaType = Pairs.first schemaResult
cx2 = Pairs.second schemaResult
svars = Core.typeSchemeVariables schemaType
sbody = Core.typeSchemeBody schemaType
in (Eithers.bind (ExtractCore.unionType tname sbody) (\sfields -> Eithers.bind (Resolution.findFieldType cx2 fname sfields) (\ftyp -> Right (Resolution.nominalApplication tname typeArgs, cx2))))))
-- | Reconstruct the type of a lambda function (Either/InferenceContext version). Paper: inference.tex, rule Abs (checking side).
typeOfLambda :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Lambda -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfLambda cx tx typeArgs l =
let v = Core.lambdaParameter l
mdom = Core.lambdaDomain l
body = Core.lambdaBody l
in (Eithers.bind (Optionals.cases mdom (Left (Errors.ErrorChecking (Checking.CheckingErrorUntypedLambda (Checking.UntypedLambdaError {
})))) (\dom ->
let types2 = Maps.insert v (Scoping.fTypeToTypeScheme dom) (Graph.graphBoundTypes tx)
in (Eithers.bind (typeOf cx (Graph.Graph {
Graph.graphBoundTerms = (Graph.graphBoundTerms tx),
Graph.graphBoundTypes = types2,
Graph.graphClassConstraints = (Graph.graphClassConstraints tx),
Graph.graphLambdaVariables = (Graph.graphLambdaVariables tx),
Graph.graphMetadata = (Graph.graphMetadata tx),
Graph.graphPrimitives = (Graph.graphPrimitives tx),
Graph.graphSchemaTypes = (Graph.graphSchemaTypes tx),
Graph.graphTypeVariables = (Graph.graphTypeVariables tx)}) [] body) (\codResult ->
let cod = Pairs.first codResult
cx2 = Pairs.second codResult
in (Right (
Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = dom,
Core.functionTypeCodomain = cod}),
cx2)))))) (\tbodyResult ->
let tbody = Pairs.first tbodyResult
cx3 = Pairs.second tbodyResult
in (Eithers.bind (applyTypeArgumentsToType cx3 tx typeArgs tbody) (\applied -> Right (applied, cx3)))))
-- | Reconstruct the type of a let binding (Either/InferenceContext version). Paper: inference.tex, rule Let (checking side).
typeOfLet :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Let -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfLet cx tx typeArgs letTerm =
let bs = Core.letBindings letTerm
body = Core.letBody letTerm
bnames = Lists.map Core.bindingName bs
bindingType =
\b -> Optionals.cases (Core.bindingTypeScheme b) (Left (Errors.ErrorChecking (Checking.CheckingErrorUntypedLetBinding (Checking.UntypedLetBindingError {
Checking.untypedLetBindingErrorBinding = b})))) (\ts -> Right (Scoping.typeSchemeToFType ts))
btypesResult =
Lists.foldl (\acc -> \b -> Eithers.bind acc (\accR ->
let types = Pairs.first accR
in (Eithers.bind (bindingType b) (\btype -> Right (Lists.concat2 types (Lists.pure btype), ()))))) (Right ([], ())) bs
in (Eithers.bind btypesResult (\btypesR ->
let btypes = Pairs.first btypesR
tx2 =
Graph.Graph {
Graph.graphBoundTerms = (Graph.graphBoundTerms tx),
Graph.graphBoundTypes = (Maps.union (Maps.fromList (Lists.zip bnames (Lists.map Scoping.fTypeToTypeScheme btypes))) (Graph.graphBoundTypes tx)),
Graph.graphClassConstraints = (Graph.graphClassConstraints tx),
Graph.graphLambdaVariables = (Graph.graphLambdaVariables tx),
Graph.graphMetadata = (Graph.graphMetadata tx),
Graph.graphPrimitives = (Graph.graphPrimitives tx),
Graph.graphSchemaTypes = (Graph.graphSchemaTypes tx),
Graph.graphTypeVariables = (Graph.graphTypeVariables tx)}
in (Eithers.bind (typeOf cx tx2 [] body) (\tResult ->
let t = Pairs.first tResult
cx2 = Pairs.second tResult
in (Eithers.bind (applyTypeArgumentsToType cx2 tx typeArgs t) (\applied -> Right (applied, cx2)))))))
-- | Reconstruct the type of a list (Either/InferenceContext version). Paper: inference.tex, rules Lst_0 and Lst_+ (checking side).
typeOfList :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> [Core.Term] -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfList cx tx typeArgs els =
let listArityErr =
Left (Errors.ErrorChecking (Checking.CheckingErrorTypeArityMismatch (Checking.TypeArityMismatchError {
Checking.typeArityMismatchErrorType = (Core.TypeList Core.TypeUnit),
Checking.typeArityMismatchErrorExpectedArity = 1,
Checking.typeArityMismatchErrorActualArity = (Lists.length typeArgs),
Checking.typeArityMismatchErrorTypeArguments = typeArgs})))
in (Logic.ifElse (Lists.null els) (Logic.ifElse (Equality.equal (Lists.length typeArgs) 1) (Optionals.cases (Lists.maybeHead typeArgs) listArityErr (\ta0 -> Right (Core.TypeList ta0, cx))) listArityErr) (
let foldResult =
Lists.foldl (\acc -> \term -> Eithers.bind acc (\accR ->
let types = Pairs.first accR
cxA = Pairs.second accR
in (Eithers.bind (typeOf cxA tx [] term) (\tResult ->
let t = Pairs.first tResult
cxB = Pairs.second tResult
in (Right (Lists.concat2 types (Lists.pure t), cxB)))))) (Right ([], cx)) els
in (Eithers.bind foldResult (\foldR ->
let eltypes = Pairs.first foldR
cx2 = Pairs.second foldR
in (Eithers.bind (checkSameType cx2 tx "list elements" eltypes) (\unifiedType -> Right (Core.TypeList unifiedType, cx2)))))))
-- | Reconstruct the type of a literal (Either/InferenceContext version). Paper: inference.tex, rule Lit (checking side).
typeOfLiteral :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Literal -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfLiteral cx tx typeArgs lit =
let t = Core.TypeLiteral (Reflect.literalType lit)
in (Eithers.bind (applyTypeArgumentsToType cx tx typeArgs t) (\applied -> Right (applied, cx)))
-- | Reconstruct the type of a map (Either/InferenceContext version). Paper: inference.tex, rules Map_0 and Map_+ (checking side).
typeOfMap :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> M.Map Core.Term Core.Term -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfMap cx tx typeArgs m =
let mapArityErr =
Left (Errors.ErrorChecking (Checking.CheckingErrorTypeArityMismatch (Checking.TypeArityMismatchError {
Checking.typeArityMismatchErrorType = (Core.TypeMap (Core.MapType {
Core.mapTypeKeys = Core.TypeUnit,
Core.mapTypeValues = Core.TypeUnit})),
Checking.typeArityMismatchErrorExpectedArity = 2,
Checking.typeArityMismatchErrorActualArity = (Lists.length typeArgs),
Checking.typeArityMismatchErrorTypeArguments = typeArgs})))
in (Logic.ifElse (Maps.null m) (Logic.ifElse (Equality.equal (Lists.length typeArgs) 2) (Optionals.cases (Lists.uncons typeArgs) mapArityErr (\uc0 ->
let ta0 = Pairs.first uc0
in (Optionals.cases (Lists.uncons (Pairs.second uc0)) mapArityErr (\uc1 ->
let ta1 = Pairs.first uc1
in (Right (
Core.TypeMap (Core.MapType {
Core.mapTypeKeys = ta0,
Core.mapTypeValues = ta1}),
cx)))))) mapArityErr) (
let pairs = Maps.toList m
keyFoldResult =
Lists.foldl (\acc -> \p -> Eithers.bind acc (\accR ->
let types = Pairs.first accR
cxA = Pairs.second accR
in (Eithers.bind (typeOf cxA tx [] (Pairs.first p)) (\tResult ->
let t = Pairs.first tResult
cxB = Pairs.second tResult
in (Right (Lists.concat2 types (Lists.pure t), cxB)))))) (Right ([], cx)) pairs
in (Eithers.bind keyFoldResult (\keyFoldR ->
let keyTypes = Pairs.first keyFoldR
cx2 = Pairs.second keyFoldR
in (Eithers.bind (checkSameType cx2 tx "map keys" keyTypes) (\kt ->
let valFoldResult =
Lists.foldl (\acc -> \p -> Eithers.bind acc (\accR ->
let types = Pairs.first accR
cxA = Pairs.second accR
in (Eithers.bind (typeOf cxA tx [] (Pairs.second p)) (\tResult ->
let t = Pairs.first tResult
cxB = Pairs.second tResult
in (Right (Lists.concat2 types (Lists.pure t), cxB)))))) (Right ([], cx2)) pairs
in (Eithers.bind valFoldResult (\valFoldR ->
let valTypes = Pairs.first valFoldR
cx3 = Pairs.second valFoldR
in (Eithers.bind (checkSameType cx3 tx "map values" valTypes) (\vt -> Eithers.bind (applyTypeArgumentsToType cx3 tx typeArgs (Core.TypeMap (Core.MapType {
Core.mapTypeKeys = kt,
Core.mapTypeValues = vt}))) (\applied -> Right (applied, cx3))))))))))))
-- | Reconstruct the type of an optional value (Either/InferenceContext version). Paper: inference.tex, rules Opt_0 and Opt_1 (checking side).
typeOfMaybe :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Maybe Core.Term -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfMaybe cx tx typeArgs mt =
let forNothing =
let n = Lists.length typeArgs
maybeArityErr =
Left (Errors.ErrorChecking (Checking.CheckingErrorTypeArityMismatch (Checking.TypeArityMismatchError {
Checking.typeArityMismatchErrorType = (Core.TypeOptional Core.TypeUnit),
Checking.typeArityMismatchErrorExpectedArity = 1,
Checking.typeArityMismatchErrorActualArity = n,
Checking.typeArityMismatchErrorTypeArguments = typeArgs})))
in (Logic.ifElse (Equality.equal n 1) (Optionals.cases (Lists.maybeHead typeArgs) maybeArityErr (\ta0 -> Right (Core.TypeOptional ta0, cx))) maybeArityErr)
forJust =
\term -> Eithers.bind (typeOf cx tx [] term) (\tResult ->
let termType = Pairs.first tResult
cx2 = Pairs.second tResult
t = Core.TypeOptional termType
in (Eithers.bind (applyTypeArgumentsToType cx2 tx typeArgs t) (\applied -> Right (applied, cx2))))
in (Optionals.cases mt forNothing forJust)
-- | Reconstruct the type of a pair (Either/InferenceContext version). Paper: inference.tex, rule Pair (checking side).
typeOfPair :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> (Core.Term, Core.Term) -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfPair cx tx typeArgs p =
let n = Lists.length typeArgs
in (Logic.ifElse (Equality.equal n 2) (
let pairFst = Pairs.first p
pairSnd = Pairs.second p
in (Eithers.bind (typeOf cx tx [] pairFst) (\result1 ->
let firstType = Pairs.first result1
cx2 = Pairs.second result1
in (Eithers.bind (typeOf cx2 tx [] pairSnd) (\result2 ->
let secondType = Pairs.first result2
cx3 = Pairs.second result2
in (Right (
Core.TypePair (Core.PairType {
Core.pairTypeFirst = firstType,
Core.pairTypeSecond = secondType}),
cx3))))))) (Left (Errors.ErrorChecking (Checking.CheckingErrorTypeArityMismatch (Checking.TypeArityMismatchError {
Checking.typeArityMismatchErrorType = (Core.TypePair (Core.PairType {
Core.pairTypeFirst = Core.TypeUnit,
Core.pairTypeSecond = Core.TypeUnit})),
Checking.typeArityMismatchErrorExpectedArity = 2,
Checking.typeArityMismatchErrorActualArity = n,
Checking.typeArityMismatchErrorTypeArguments = typeArgs})))))
-- | Reconstruct the type of a primitive function (Either/InferenceContext version). Paper: inference.tex, rule Prim (checking side).
typeOfPrimitive :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Name -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfPrimitive cx tx typeArgs name =
let rawTs =
Optionals.map (\_p -> Scoping.termSignatureToTypeScheme (Packaging.primitiveDefinitionSignature (Graph.primitiveDefinition _p))) (Maps.lookup name (Graph.graphPrimitives tx))
in (Optionals.cases rawTs (Left (Errors.ErrorUndefinedTermVariable (ErrorCore.UndefinedTermVariableError {
ErrorCore.undefinedTermVariableErrorLocation = (Paths.SubtermPath []),
ErrorCore.undefinedTermVariableErrorName = name}))) (\tsRaw ->
let instResult = Resolution.instantiateTypeScheme cx tsRaw
ts = Pairs.first instResult
cx2 = Pairs.second instResult
t = Scoping.typeSchemeToFType ts
in (Eithers.bind (applyTypeArgumentsToType cx2 tx typeArgs t) (\applied -> Right (applied, cx2)))))
-- | Reconstruct the type of a record projection (Either/InferenceContext version). Paper: inference.tex, rule Proj (checking side).
typeOfProjection :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Projection -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfProjection cx tx typeArgs p =
let tname = Core.projectionTypeName p
fname = Core.projectionFieldName p
in (Eithers.bind (Resolution.requireSchemaType cx (Graph.graphSchemaTypes tx) tname) (\schemaResult ->
let schemaType = Pairs.first schemaResult
cx2 = Pairs.second schemaResult
svars = Core.typeSchemeVariables schemaType
sbody = Core.typeSchemeBody schemaType
in (Eithers.bind (ExtractCore.recordType tname sbody) (\sfields -> Eithers.bind (Resolution.findFieldType cx2 fname sfields) (\ftyp ->
let subst = Typing.TypeSubst (Maps.fromList (Lists.zip svars typeArgs))
sftyp = Substitution.substInType subst ftyp
in (Right (
Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Resolution.nominalApplication tname typeArgs),
Core.functionTypeCodomain = sftyp}),
cx2)))))))
-- | Reconstruct the type of a record (Either/InferenceContext version). Paper: inference.tex, rule Rec (checking side).
typeOfRecord :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Record -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfRecord cx tx typeArgs record =
let tname = Core.recordTypeName record
fields = Core.recordFields record
foldResult =
Lists.foldl (\acc -> \term -> Eithers.bind acc (\accR ->
let types = Pairs.first accR
cxA = Pairs.second accR
in (Eithers.bind (typeOf cxA tx [] term) (\tResult ->
let t = Pairs.first tResult
cxB = Pairs.second tResult
in (Right (Lists.concat2 types (Lists.pure t), cxB)))))) (Right ([], cx)) (Lists.map Core.fieldTerm fields)
in (Eithers.bind foldResult (\foldR ->
let cx2 = Pairs.second foldR
in (Right (Resolution.nominalApplication tname typeArgs, cx2))))
-- | Reconstruct the type of a set (Either/InferenceContext version). Paper: inference.tex, rules Set_0 and Set_+ (checking side).
typeOfSet :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> S.Set Core.Term -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfSet cx tx typeArgs els =
let setArityErr =
Left (Errors.ErrorChecking (Checking.CheckingErrorTypeArityMismatch (Checking.TypeArityMismatchError {
Checking.typeArityMismatchErrorType = (Core.TypeSet Core.TypeUnit),
Checking.typeArityMismatchErrorExpectedArity = 1,
Checking.typeArityMismatchErrorActualArity = (Lists.length typeArgs),
Checking.typeArityMismatchErrorTypeArguments = typeArgs})))
in (Logic.ifElse (Sets.null els) (Logic.ifElse (Equality.equal (Lists.length typeArgs) 1) (Optionals.cases (Lists.maybeHead typeArgs) setArityErr (\ta0 -> Right (Core.TypeSet ta0, cx))) setArityErr) (
let foldResult =
Lists.foldl (\acc -> \term -> Eithers.bind acc (\accR ->
let types = Pairs.first accR
cxA = Pairs.second accR
in (Eithers.bind (typeOf cxA tx [] term) (\tResult ->
let t = Pairs.first tResult
cxB = Pairs.second tResult
in (Right (Lists.concat2 types (Lists.pure t), cxB)))))) (Right ([], cx)) (Sets.toList els)
in (Eithers.bind foldResult (\foldR ->
let eltypes = Pairs.first foldR
cx2 = Pairs.second foldR
in (Eithers.bind (checkSameType cx2 tx "set elements" eltypes) (\unifiedType -> Right (Core.TypeSet unifiedType, cx2)))))))
-- | Check the type of a term
typeOfTerm :: Typing.InferenceContext -> Graph.Graph -> Core.Term -> Either Errors.Error Core.Type
typeOfTerm cx g term = Eithers.map Pairs.first (typeOf cx g [] term)
-- | Reconstruct the type of a type application term (Either/InferenceContext version). Paper: inference.tex, 'Checking the witness' (pushes onto the pending-type-argument stack).
typeOfTypeApplication :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.TypeApplicationTerm -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfTypeApplication cx tx typeArgs tyapp =
let body = Core.typeApplicationTermBody tyapp
t = Core.typeApplicationTermType tyapp
in (typeOf cx tx (Lists.cons t typeArgs) body)
-- | Reconstruct the type of a type lambda (type abstraction) term (Either/InferenceContext version). Paper: inference.tex, type abstraction terms in the elaborated Term grammar.
typeOfTypeLambda :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.TypeLambda -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfTypeLambda cx tx typeArgs tl =
let v = Core.typeLambdaParameter tl
body = Core.typeLambdaBody tl
vars = Graph.graphTypeVariables tx
tx2 =
Graph.Graph {
Graph.graphBoundTerms = (Graph.graphBoundTerms tx),
Graph.graphBoundTypes = (Graph.graphBoundTypes tx),
Graph.graphClassConstraints = (Graph.graphClassConstraints tx),
Graph.graphLambdaVariables = (Graph.graphLambdaVariables tx),
Graph.graphMetadata = (Graph.graphMetadata tx),
Graph.graphPrimitives = (Graph.graphPrimitives tx),
Graph.graphSchemaTypes = (Graph.graphSchemaTypes tx),
Graph.graphTypeVariables = (Sets.insert v vars)}
in (Eithers.bind (typeOf cx tx2 [] body) (\result1 ->
let t1 = Pairs.first result1
cx2 = Pairs.second result1
in (Eithers.bind (applyTypeArgumentsToType cx2 tx typeArgs (Core.TypeForall (Core.ForallType {
Core.forallTypeParameter = v,
Core.forallTypeBody = t1}))) (\applied -> Right (applied, cx2)))))
-- | Reconstruct the type of the unit term (Either/InferenceContext version). Paper: inference.tex, rule Unit (checking side).
typeOfUnit :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfUnit cx tx typeArgs =
Eithers.bind (applyTypeArgumentsToType cx tx typeArgs Core.TypeUnit) (\applied -> Right (applied, cx))
-- | Reconstruct the type of an unwrap operation (Either/InferenceContext version). Paper: inference.tex, rule Unwr (checking side).
typeOfUnwrap :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Name -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfUnwrap cx tx typeArgs tname =
Eithers.bind (Resolution.requireSchemaType cx (Graph.graphSchemaTypes tx) tname) (\schemaResult ->
let schemaType = Pairs.first schemaResult
cx2 = Pairs.second schemaResult
svars = Core.typeSchemeVariables schemaType
sbody = Core.typeSchemeBody schemaType
in (Eithers.bind (ExtractCore.wrappedType tname sbody) (\wrapped ->
let subst = Typing.TypeSubst (Maps.fromList (Lists.zip svars typeArgs))
swrapped = Substitution.substInType subst wrapped
in (Right (
Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Resolution.nominalApplication tname typeArgs),
Core.functionTypeCodomain = swrapped}),
cx2)))))
-- | Reconstruct the type of a variable (Either/InferenceContext version). Paper: inference.tex, rules Var and Prim (checking side); note the primitives-first lookup order, the reverse of inference.
typeOfVariable :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.Name -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfVariable cx tx typeArgs name =
let forScheme =
\ts ->
let tResult =
Logic.ifElse (Lists.null typeArgs) (Resolution.instantiateType cx (Scoping.typeSchemeToFType ts)) (Scoping.typeSchemeToFType ts, cx)
t = Pairs.first tResult
cx2 = Pairs.second tResult
in (Eithers.bind (applyTypeArgumentsToType cx2 tx typeArgs t) (\applied -> Right (applied, cx2)))
primScheme =
Optionals.map (\_p -> Scoping.termSignatureToTypeScheme (Packaging.primitiveDefinitionSignature (Graph.primitiveDefinition _p))) (Maps.lookup name (Graph.graphPrimitives tx))
in (Optionals.cases primScheme (Optionals.cases (Maps.lookup name (Graph.graphBoundTypes tx)) (Left (Errors.ErrorUntypedTermVariable (ErrorCore.UntypedTermVariableError {
ErrorCore.untypedTermVariableErrorLocation = (Paths.SubtermPath []),
ErrorCore.untypedTermVariableErrorName = name}))) forScheme) forScheme)
-- | Reconstruct the type of a wrapped term (Either/InferenceContext version). Paper: inference.tex, rule Wrp (checking side).
typeOfWrappedTerm :: Typing.InferenceContext -> Graph.Graph -> [Core.Type] -> Core.WrappedTerm -> Either Errors.Error (Core.Type, Typing.InferenceContext)
typeOfWrappedTerm cx tx typeArgs wt =
let tname = Core.wrappedTermTypeName wt
body = Core.wrappedTermBody wt
in (Eithers.bind (typeOf cx tx [] body) (\result ->
let cx2 = Pairs.second result
in (Right (Resolution.nominalApplication tname typeArgs, cx2))))
-- | Check whether a list of types are effectively equal, disregarding type aliases and free type variable naming. Also treats free type variables (not in schema) as wildcards, since inference has already verified consistency.
typesAllEffectivelyEqual :: Graph.Graph -> [Core.Type] -> Bool
typesAllEffectivelyEqual tx tlist =
let types = Graph.graphSchemaTypes tx
containsFreeVar =
\t ->
let allVars = Variables.freeVariablesInTypeSimple t
schemaNames = Sets.fromList (Maps.keys types)
in (Logic.not (Sets.null (Sets.difference allVars schemaNames)))
anyContainsFreeVar = Lists.foldl (\acc -> \t -> Logic.or acc (containsFreeVar t)) False tlist
in (Logic.ifElse anyContainsFreeVar True (Logic.ifElse (allEqual (Lists.map (\t -> normalizeTypeFreeVars t) tlist)) True (allEqual (Lists.map (\t -> normalizeTypeFreeVars (Strip.deannotateTypeRecursive (Dependencies.replaceTypedefs types t))) tlist))))
-- | Check whether two types are effectively equal, disregarding type aliases, forall quantifiers, and treating in-scope type variables as wildcards. Paper: inference.tex, 'Checking the witness' (effective equality, the type-level analogue of the referential-transparency equality of terms).
typesEffectivelyEqual :: Graph.Graph -> Core.Type -> Core.Type -> Bool
typesEffectivelyEqual tx t1 t2 =
Logic.or (containsInScopeTypeVars tx t1) (Logic.or (containsInScopeTypeVars tx t2) (typesAllEffectivelyEqual tx [
Resolution.fullyStripAndNormalizeType t1,
(Resolution.fullyStripAndNormalizeType t2)]))