Safe Haskell	Safe-Inferred
Language	Haskell2010

Dhall.TypeCheck

Contents

Type-checking
Types

Description

This module contains the logic for type checking Dhall code

Synopsis

typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X)
typeOf :: Expr s X -> Either (TypeError s X) (Expr s X)
typeWithA :: (Eq a, Pretty a) => Typer a -> Context (Expr s a) -> Expr s a -> Either (TypeError s a) (Expr s a)
checkContext :: Context (Expr s X) -> Either (TypeError s X) ()
messageExpressions :: Applicative f => (Expr s a -> f (Expr t b)) -> TypeMessage s a -> f (TypeMessage t b)
type Typer a = forall s. a -> Expr s a
type X = Void
absurd :: Void -> a
data TypeError s a = TypeError {
- context :: Context (Expr s a)
- current :: Expr s a
- typeMessage :: TypeMessage s a
}
newtype DetailedTypeError s a = DetailedTypeError (TypeError s a)
data Censored
- = CensoredDetailed (DetailedTypeError Src X)
- | Censored (TypeError Src X)
data TypeMessage s a
- = UnboundVariable Text
- | InvalidInputType (Expr s a)
- | InvalidOutputType (Expr s a)
- | NotAFunction (Expr s a) (Expr s a)
- | TypeMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
- | AnnotMismatch (Expr s a) (Expr s a) (Expr s a)
- | Untyped
- | MissingListType
- | MismatchedListElements Int (Expr s a) (Expr s a) (Expr s a)
- | InvalidListElement Int (Expr s a) (Expr s a) (Expr s a)
- | InvalidListType (Expr s a)
- | ListLitInvariant
- | InvalidSome (Expr s a) (Expr s a) (Expr s a)
- | InvalidPredicate (Expr s a) (Expr s a)
- | IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
- | InvalidFieldType Text (Expr s a)
- | InvalidAlternativeType Text (Expr s a)
- | ListAppendMismatch (Expr s a) (Expr s a)
- | MustUpdateARecord (Expr s a) (Expr s a) (Expr s a)
- | MustCombineARecord Char (Expr s a) (Expr s a)
- | InvalidDuplicateField Text (Expr s a) (Expr s a)
- | InvalidRecordCompletion Text (Expr s a)
- | CompletionSchemaMustBeARecord (Expr s a) (Expr s a)
- | CombineTypesRequiresRecordType (Expr s a) (Expr s a)
- | RecordTypeMismatch Const Const (Expr s a) (Expr s a)
- | DuplicateFieldCannotBeMerged (NonEmpty Text)
- | FieldCollision (NonEmpty Text)
- | FieldTypeCollision (NonEmpty Text)
- | MustMergeARecord (Expr s a) (Expr s a)
- | MustMergeUnionOrOptional (Expr s a) (Expr s a)
- | MustMapARecord (Expr s a) (Expr s a)
- | InvalidToMapRecordKind (Expr s a) (Expr s a)
- | HeterogenousRecordToMap (Expr s a) (Expr s a) (Expr s a)
- | InvalidToMapType (Expr s a)
- | MapTypeMismatch (Expr s a) (Expr s a)
- | MissingToMapType
- | UnusedHandler (Set Text)
- | MissingHandler Text (Set Text)
- | HandlerInputTypeMismatch Text (Expr s a) (Expr s a)
- | DisallowedHandlerType Text (Expr s a) (Expr s a) Text
- | HandlerOutputTypeMismatch Text (Expr s a) Text (Expr s a)
- | InvalidHandlerOutputType Text (Expr s a) (Expr s a)
- | MissingMergeType
- | HandlerNotAFunction Text (Expr s a)
- | CantAccess Text (Expr s a) (Expr s a)
- | CantProject Text (Expr s a) (Expr s a)
- | CantProjectByExpression (Expr s a)
- | DuplicateProjectionLabel Text
- | MissingField Text (Expr s a)
- | MissingConstructor Text (Expr s a)
- | ProjectionTypeMismatch Text (Expr s a) (Expr s a) (Expr s a) (Expr s a)
- | AssertionFailed (Expr s a) (Expr s a)
- | NotAnEquivalence (Expr s a)
- | IncomparableExpression (Expr s a)
- | EquivalenceTypeMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
- | NotWithARecord (Expr s a) (Expr s a)
- | CantAnd (Expr s a) (Expr s a)
- | CantOr (Expr s a) (Expr s a)
- | CantEQ (Expr s a) (Expr s a)
- | CantNE (Expr s a) (Expr s a)
- | CantInterpolate (Expr s a) (Expr s a)
- | CantTextAppend (Expr s a) (Expr s a)
- | CantListAppend (Expr s a) (Expr s a)
- | CantAdd (Expr s a) (Expr s a)
- | CantMultiply (Expr s a) (Expr s a)
- | OptionalWithTypeMismatch
- | NotALabelPath
- | NotAQuestionPath Text
- | ShowConstructorNotOnUnion
prettyTypeMessage :: (Eq a, Pretty a) => TypeMessage s a -> ErrorMessages
data ErrorMessages = ErrorMessages {
- short :: Doc Ann
- hints :: [Doc Ann]
- long :: Doc Ann
}

Type-checking

typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X) Source #

Type-check an expression and return the expression's type if type-checking succeeds or an error if type-checking fails

typeWith does not necessarily normalize the type since full normalization is not necessary for just type-checking. If you actually care about the returned type then you may want to normalize it afterwards.

The supplied Context records the types of the names in scope. If these are ill-typed, the return value may be ill-typed.

typeOf :: Expr s X -> Either (TypeError s X) (Expr s X) Source #

typeOf is the same as typeWith with an empty context, meaning that the expression must be closed (i.e. no free variables), otherwise type-checking will fail.

typeWithA :: (Eq a, Pretty a) => Typer a -> Context (Expr s a) -> Expr s a -> Either (TypeError s a) (Expr s a) Source #

Generalization of typeWith that allows type-checking the Embed constructor with custom logic

checkContext :: Context (Expr s X) -> Either (TypeError s X) () Source #

This function verifies that a custom context is well-formed so that type-checking will not loop

Note that typeWith already calls checkContext for you on the Context that you supply

messageExpressions :: Applicative f => (Expr s a -> f (Expr t b)) -> TypeMessage s a -> f (TypeMessage t b) Source #

Traversal that traverses every Expr in a TypeMessage

Types

type Typer a = forall s. a -> Expr s a Source #

Function that converts the value inside an Embed constructor into a new expression

type X = Void Source #

Deprecated: Use Data.Void.Void instead

A type synonym for Void

This is provided for backwards compatibility, since Dhall used to use its own X type instead of Data.Void.Void. You should use Void instead of X now

absurd :: Void -> a #

Since Void values logically don't exist, this witnesses the logical reasoning tool of "ex falso quodlibet".

>>> let x :: Either Void Int; x = Right 5
>>> :{
case x of
    Right r -> r
    Left l  -> absurd l
:}
5

Since: base-4.8.0.0

data TypeError s a Source #

A structured type error that includes context

Constructors

TypeError
Fields context :: Context (Expr s a) current :: Expr s a typeMessage :: TypeMessage s a

Instances

Instances details

(Eq a, Pretty s, Pretty a, Typeable s, Typeable a) => Exception (TypeError s a) Source #
Instance details Defined in Dhall.TypeCheck Methods toException :: TypeError s a -> SomeException # fromException :: SomeException -> Maybe (TypeError s a) # displayException :: TypeError s a -> String #
(Eq a, Pretty s, Pretty a) => Show (TypeError s a) Source #
Instance details Defined in Dhall.TypeCheck Methods showsPrec :: Int -> TypeError s a -> ShowS # show :: TypeError s a -> String # showList :: [TypeError s a] -> ShowS #
(Eq a, Pretty s, Pretty a) => Pretty (TypeError s a) Source #
Instance details Defined in Dhall.TypeCheck Methods pretty :: TypeError s a -> Doc ann # prettyList :: [TypeError s a] -> Doc ann #

newtype DetailedTypeError s a Source #

Newtype used to wrap error messages so that they render with a more detailed explanation of what went wrong

Constructors

DetailedTypeError (TypeError s a)

Instances

Instances details

(Eq a, Pretty s, Pretty a, Typeable s, Typeable a) => Exception (DetailedTypeError s a) Source #
Instance details Defined in Dhall.TypeCheck Methods toException :: DetailedTypeError s a -> SomeException # fromException :: SomeException -> Maybe (DetailedTypeError s a) # displayException :: DetailedTypeError s a -> String #
(Eq a, Pretty s, Pretty a) => Show (DetailedTypeError s a) Source #
Instance details Defined in Dhall.TypeCheck Methods showsPrec :: Int -> DetailedTypeError s a -> ShowS # show :: DetailedTypeError s a -> String # showList :: [DetailedTypeError s a] -> ShowS #
(Eq a, Pretty s, Pretty a) => Pretty (DetailedTypeError s a) Source #
Instance details Defined in Dhall.TypeCheck Methods pretty :: DetailedTypeError s a -> Doc ann # prettyList :: [DetailedTypeError s a] -> Doc ann #

data Censored Source #

Wrap a type error in this exception type to censor source code and Text literals from the error message

Constructors

CensoredDetailed (DetailedTypeError Src X)
Censored (TypeError Src X)

Instances

Instances details

Exception Censored Source #
Instance details Defined in Dhall.TypeCheck Methods toException :: Censored -> SomeException # fromException :: SomeException -> Maybe Censored # displayException :: Censored -> String #
Show Censored Source #
Instance details Defined in Dhall.TypeCheck Methods showsPrec :: Int -> Censored -> ShowS # show :: Censored -> String # showList :: [Censored] -> ShowS #
Pretty Censored Source #
Instance details Defined in Dhall.TypeCheck Methods pretty :: Censored -> Doc ann # prettyList :: [Censored] -> Doc ann #

data TypeMessage s a Source #

The specific type error

Constructors

UnboundVariable Text
InvalidInputType (Expr s a)
InvalidOutputType (Expr s a)
NotAFunction (Expr s a) (Expr s a)
TypeMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
AnnotMismatch (Expr s a) (Expr s a) (Expr s a)
Untyped
MissingListType
MismatchedListElements Int (Expr s a) (Expr s a) (Expr s a)
InvalidListElement Int (Expr s a) (Expr s a) (Expr s a)
InvalidListType (Expr s a)
ListLitInvariant
InvalidSome (Expr s a) (Expr s a) (Expr s a)
InvalidPredicate (Expr s a) (Expr s a)
IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
InvalidFieldType Text (Expr s a)
InvalidAlternativeType Text (Expr s a)
ListAppendMismatch (Expr s a) (Expr s a)
MustUpdateARecord (Expr s a) (Expr s a) (Expr s a)
MustCombineARecord Char (Expr s a) (Expr s a)
InvalidDuplicateField Text (Expr s a) (Expr s a)
InvalidRecordCompletion Text (Expr s a)
CompletionSchemaMustBeARecord (Expr s a) (Expr s a)
CombineTypesRequiresRecordType (Expr s a) (Expr s a)
RecordTypeMismatch Const Const (Expr s a) (Expr s a)
DuplicateFieldCannotBeMerged (NonEmpty Text)
FieldCollision (NonEmpty Text)
FieldTypeCollision (NonEmpty Text)
MustMergeARecord (Expr s a) (Expr s a)
MustMergeUnionOrOptional (Expr s a) (Expr s a)
MustMapARecord (Expr s a) (Expr s a)
InvalidToMapRecordKind (Expr s a) (Expr s a)
HeterogenousRecordToMap (Expr s a) (Expr s a) (Expr s a)
InvalidToMapType (Expr s a)
MapTypeMismatch (Expr s a) (Expr s a)
MissingToMapType
UnusedHandler (Set Text)
MissingHandler Text (Set Text)
HandlerInputTypeMismatch Text (Expr s a) (Expr s a)
DisallowedHandlerType Text (Expr s a) (Expr s a) Text
HandlerOutputTypeMismatch Text (Expr s a) Text (Expr s a)
InvalidHandlerOutputType Text (Expr s a) (Expr s a)
MissingMergeType
HandlerNotAFunction Text (Expr s a)
CantAccess Text (Expr s a) (Expr s a)
CantProject Text (Expr s a) (Expr s a)
CantProjectByExpression (Expr s a)
DuplicateProjectionLabel Text
MissingField Text (Expr s a)
MissingConstructor Text (Expr s a)
ProjectionTypeMismatch Text (Expr s a) (Expr s a) (Expr s a) (Expr s a)
AssertionFailed (Expr s a) (Expr s a)
NotAnEquivalence (Expr s a)
IncomparableExpression (Expr s a)
EquivalenceTypeMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
NotWithARecord (Expr s a) (Expr s a)
CantAnd (Expr s a) (Expr s a)
CantOr (Expr s a) (Expr s a)
CantEQ (Expr s a) (Expr s a)
CantNE (Expr s a) (Expr s a)
CantInterpolate (Expr s a) (Expr s a)
CantTextAppend (Expr s a) (Expr s a)
CantListAppend (Expr s a) (Expr s a)
CantAdd (Expr s a) (Expr s a)
CantMultiply (Expr s a) (Expr s a)
OptionalWithTypeMismatch
NotALabelPath
NotAQuestionPath Text
ShowConstructorNotOnUnion

Instances

Instances details

(Show s, Show a) => Show (TypeMessage s a) Source #
Instance details Defined in Dhall.TypeCheck Methods showsPrec :: Int -> TypeMessage s a -> ShowS # show :: TypeMessage s a -> String # showList :: [TypeMessage s a] -> ShowS #

prettyTypeMessage :: (Eq a, Pretty a) => TypeMessage s a -> ErrorMessages Source #

Convert a TypeMessage to short- and long-form ErrorMessages

data ErrorMessages Source #

Output of prettyTypeMessage, containing short- and long-form error messages

Constructors

ErrorMessages
Fields short :: Doc Ann Default succinct 1-line explanation of what went wrong hints :: [Doc Ann] Possibly-empty hints based on specific types involved in the error long :: Doc Ann Longer and more detailed explanation of the error