hydra.error.checking module

Error types for type checking.

class hydra.error.checking.CheckingError

Bases: object

INCORRECT_UNIFICATION = Name(value='incorrectUnification')

NOT_A_FORALL_TYPE = Name(value='notAForallType')

NOT_A_FUNCTION_TYPE = Name(value='notAFunctionType')

OTHER = Name(value='other')

TYPE_ = Name(value='hydra.error.checking.CheckingError')

TYPE_ARITY_MISMATCH = Name(value='typeArityMismatch')

TYPE_MISMATCH = Name(value='typeMismatch')

UNBOUND_TYPE_VARIABLES = Name(value='unboundTypeVariables')

UNDEFINED_TERM_VARIABLE = Name(value='undefinedTermVariable')

UNEQUAL_TYPES = Name(value='unequalTypes')

UNSUPPORTED_TERM_VARIANT = Name(value='unsupportedTermVariant')

UNTYPED_LAMBDA = Name(value='untypedLambda')

UNTYPED_LET_BINDING = Name(value='untypedLetBinding')

UNTYPED_TERM_VARIABLE = Name(value='untypedTermVariable')

class hydra.error.checking.CheckingErrorIncorrectUnification(value: T)

Bases: Node[IncorrectUnificationError]

A post-unification consistency check failure

class hydra.error.checking.CheckingErrorNotAForallType(value: T)

Bases: Node[NotAForallTypeError]

A type that is not a forall type when one was expected

class hydra.error.checking.CheckingErrorNotAFunctionType(value: T)

Bases: Node[NotAFunctionTypeError]

A type that is not a function type when one was expected

class hydra.error.checking.CheckingErrorOther(value: T)

Bases: Node[OtherCheckingError]

A generic checking error

class hydra.error.checking.CheckingErrorTypeArityMismatch(value: T)

Bases: Node[TypeArityMismatchError]

A type constructor applied to the wrong number of arguments

class hydra.error.checking.CheckingErrorTypeMismatch(value: T)

Bases: Node[TypeMismatchError]

A type mismatch between expected and actual types

class hydra.error.checking.CheckingErrorUnboundTypeVariables(value: T)

Bases: Node[UnboundTypeVariablesError]

Type variables that are not bound in scope

class hydra.error.checking.CheckingErrorUndefinedTermVariable(value: T)

Bases: Node[UndefinedTermVariableCheckingError]

A reference to a term variable that is not bound in scope, encountered during checking

class hydra.error.checking.CheckingErrorUnequalTypes(value: T)

Bases: Node[UnequalTypesError]

Multiple types that should be equal but are not

class hydra.error.checking.CheckingErrorUnsupportedTermVariant(value: T)

Bases: Node[UnsupportedTermVariantError]

A term variant that the type checker does not support

class hydra.error.checking.CheckingErrorUntypedLambda(value: T)

Bases: Node[UntypedLambdaError]

A lambda expression without a type annotation on its parameter

class hydra.error.checking.CheckingErrorUntypedLetBinding(value: T)

Bases: Node[UntypedLetBindingError]

A let binding without a type annotation

class hydra.error.checking.CheckingErrorUntypedTermVariable(value: T)

Bases: Node[UntypedTermVariableCheckingError]

A reference to a term variable whose type is not known, encountered during checking

class hydra.error.checking.IncorrectUnificationError(substitution: Annotated[TypeSubst, 'The substitution that failed the consistency check'])

Bases: object

A post-unification consistency check failure.

class Builder(_substitution: 'hydra.typing.TypeSubst' = None)

Bases: object

build()

substitution(substitution)

SUBSTITUTION = Name(value='substitution')

TYPE_ = Name(value='hydra.error.checking.IncorrectUnificationError')

static builder()

substitution: Annotated[TypeSubst, 'The substitution that failed the consistency check']

with_substitution(substitution)

class hydra.error.checking.NotAForallTypeError(type: Annotated[Type, 'The actual type encountered'], type_arguments: Annotated[Sequence[Type], 'The type arguments that were being applied'])

Bases: object

A type that is not a forall type when type arguments are being applied.

class Builder(_type: 'hydra.core.Type' = None, _type_arguments: 'Sequence[hydra.core.Type]' = None)

Bases: object

build()

type(type)

type_arguments(type_arguments)

TYPE = Name(value='type')

TYPE_ = Name(value='hydra.error.checking.NotAForallTypeError')

TYPE_ARGUMENTS = Name(value='typeArguments')

static builder()

type: Annotated[Type, 'The actual type encountered']

type_arguments: Annotated[Sequence[Type], 'The type arguments that were being applied']

with_type(type)

with_type_arguments(type_arguments)

class hydra.error.checking.NotAFunctionTypeError(type: Annotated[Type, 'The actual type encountered'])

Bases: object

A type that is not a function type when one was expected in an application.

class Builder(_type: 'hydra.core.Type' = None)

Bases: object

build()

type(type)

TYPE = Name(value='type')

TYPE_ = Name(value='hydra.error.checking.NotAFunctionTypeError')

static builder()

type: Annotated[Type, 'The actual type encountered']

with_type(type)

class hydra.error.checking.OtherCheckingError(path: Annotated[SubtermPath, 'The subterm path at which the error was observed'], message: Annotated[str, 'A human-readable error message'])

Bases: object

A generic checking error: message + subterm path.

class Builder(_path: 'hydra.paths.SubtermPath' = None, _message: 'str' = None)

Bases: object

build()

message(message)

path(path)

MESSAGE = Name(value='message')

PATH = Name(value='path')

TYPE_ = Name(value='hydra.error.checking.OtherCheckingError')

static builder()

message: Annotated[str, 'A human-readable error message']

path: Annotated[SubtermPath, 'The subterm path at which the error was observed']

with_message(message)

with_path(path)

class hydra.error.checking.TypeArityMismatchError(type: Annotated[Type, 'The type being checked'], expected_arity: Annotated[int, 'The expected number of type arguments'], actual_arity: Annotated[int, 'The actual number of type arguments provided'], type_arguments: Annotated[Sequence[Type], 'The type arguments that were provided'])

Bases: object

A type constructor applied to the wrong number of type arguments.

ACTUAL_ARITY = Name(value='actualArity')

class Builder(_type: 'hydra.core.Type' = None, _expected_arity: 'int' = None, _actual_arity: 'int' = None, _type_arguments: 'Sequence[hydra.core.Type]' = None)

Bases: object

actual_arity(actual_arity)

build()

expected_arity(expected_arity)

type(type)

type_arguments(type_arguments)

EXPECTED_ARITY = Name(value='expectedArity')

TYPE = Name(value='type')

TYPE_ = Name(value='hydra.error.checking.TypeArityMismatchError')

TYPE_ARGUMENTS = Name(value='typeArguments')

actual_arity: Annotated[int, 'The actual number of type arguments provided']

static builder()

expected_arity: Annotated[int, 'The expected number of type arguments']

type: Annotated[Type, 'The type being checked']

type_arguments: Annotated[Sequence[Type], 'The type arguments that were provided']

with_actual_arity(actual_arity)

with_expected_arity(expected_arity)

with_type(type)

with_type_arguments(type_arguments)

class hydra.error.checking.TypeMismatchError(expected_type: Annotated[Type, 'The expected type'], actual_type: Annotated[Type, 'The actual type encountered'])

Bases: object

A type mismatch between expected and actual types.

ACTUAL_TYPE = Name(value='actualType')

class Builder(_expected_type: 'hydra.core.Type' = None, _actual_type: 'hydra.core.Type' = None)

Bases: object

actual_type(actual_type)

build()

expected_type(expected_type)

EXPECTED_TYPE = Name(value='expectedType')

TYPE_ = Name(value='hydra.error.checking.TypeMismatchError')

actual_type: Annotated[Type, 'The actual type encountered']

static builder()

expected_type: Annotated[Type, 'The expected type']

with_actual_type(actual_type)

with_expected_type(expected_type)

class hydra.error.checking.UnboundTypeVariablesError(variables: Annotated[Set[Name], 'The set of unbound type variable names'], type: Annotated[Type, 'The type containing the unbound variables'])

Bases: object

Type variables that appear free in a type but are not bound in scope.

class Builder(_variables: 'Set[hydra.core.Name]' = None, _type: 'hydra.core.Type' = None)

Bases: object

build()

type(type)

variables(variables)

TYPE = Name(value='type')

TYPE_ = Name(value='hydra.error.checking.UnboundTypeVariablesError')

VARIABLES = Name(value='variables')

static builder()

type: Annotated[Type, 'The type containing the unbound variables']

variables: Annotated[Set[Name], 'The set of unbound type variable names']

with_type(type)

with_variables(variables)

class hydra.error.checking.UndefinedTermVariableCheckingError(path: Annotated[SubtermPath, 'The subterm path at which the variable was referenced'], name: Annotated[Name, 'The name of the undefined variable'])

Bases: object

A reference to a term variable that is not bound in scope, encountered during checking.

class Builder(_path: 'hydra.paths.SubtermPath' = None, _name: 'hydra.core.Name' = None)

Bases: object

build()

name(name)

path(path)

NAME = Name(value='name')

PATH = Name(value='path')

TYPE_ = Name(value='hydra.error.checking.UndefinedTermVariableCheckingError')

static builder()

name: Annotated[Name, 'The name of the undefined variable']

path: Annotated[SubtermPath, 'The subterm path at which the variable was referenced']

with_name(name)

with_path(path)

class hydra.error.checking.UnequalTypesError(types: Annotated[Sequence[Type], 'The list of types that are not all equal'], description: Annotated[str, 'A description of the context in which the types were expected to be equal'])

Bases: object

Multiple types that should all be equal but are not.

class Builder(_types: 'Sequence[hydra.core.Type]' = None, _description: 'str' = None)

Bases: object

build()

description(description)

types(types)

DESCRIPTION = Name(value='description')

TYPES = Name(value='types')

TYPE_ = Name(value='hydra.error.checking.UnequalTypesError')

static builder()

description: Annotated[str, 'A description of the context in which the types were expected to be equal']

types: Annotated[Sequence[Type], 'The list of types that are not all equal']

with_description(description)

with_types(types)

class hydra.error.checking.UnsupportedTermVariantError(term_variant: Annotated[TermVariant, 'The unsupported term variant'])

Bases: object

A term variant that the type checker does not support.

class Builder(_term_variant: 'hydra.variants.TermVariant' = None)

Bases: object

build()

term_variant(term_variant)

TERM_VARIANT = Name(value='termVariant')

TYPE_ = Name(value='hydra.error.checking.UnsupportedTermVariantError')

static builder()

term_variant: Annotated[TermVariant, 'The unsupported term variant']

with_term_variant(term_variant)

class hydra.error.checking.UntypedLambdaError

Bases: object

A lambda expression without a type annotation on its parameter.

class Builder

Bases: object

build()

TYPE_ = Name(value='hydra.error.checking.UntypedLambdaError')

static builder()

class hydra.error.checking.UntypedLetBindingError(binding: Annotated[Binding, 'The untyped binding'])

Bases: object

A let binding without a type annotation.

BINDING = Name(value='binding')

class Builder(_binding: 'hydra.core.Binding' = None)

Bases: object

binding(binding)

build()

TYPE_ = Name(value='hydra.error.checking.UntypedLetBindingError')

binding: Annotated[Binding, 'The untyped binding']

static builder()

with_binding(binding)

class hydra.error.checking.UntypedTermVariableCheckingError(path: Annotated[SubtermPath, 'The subterm path at which the variable was referenced'], name: Annotated[Name, 'The name of the untyped variable'])

Bases: object

A reference to a term variable whose type is not known, encountered during checking.

class Builder(_path: 'hydra.paths.SubtermPath' = None, _name: 'hydra.core.Name' = None)

Bases: object

build()

name(name)

path(path)

NAME = Name(value='name')

PATH = Name(value='path')

TYPE_ = Name(value='hydra.error.checking.UntypedTermVariableCheckingError')

static builder()

name: Annotated[Name, 'The name of the untyped variable']

path: Annotated[SubtermPath, 'The subterm path at which the variable was referenced']

with_name(name)

with_path(path)