Dhall.TypeCheck

This module contains the logic for type checking Dhall code

Type-checking

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

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)

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)

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

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

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)

Traversal that traverses every Expr in a TypeMessage

Types

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

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

type X = Void

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

A structured type error that includes context

Constructors

TypeError

Fields

• context :: Context (Expr s a)
• current :: Expr s a
• typeMessage :: TypeMessage s a

Instances

(Eq a, Pretty s, Pretty a) => Show (TypeError s a)

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, Typeable s, Typeable a) => Exception (TypeError s a)

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) => Pretty (TypeError s a)

Defined in Dhall.TypeCheck

Methods

pretty :: TypeError s a -> Doc ann

prettyList :: [TypeError s a] -> Doc ann

newtype DetailedTypeError s a

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

(Eq a, Pretty s, Pretty a) => Show (DetailedTypeError s a)

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, Typeable s, Typeable a) => Exception (DetailedTypeError s a)

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) => Pretty (DetailedTypeError s a)

Defined in Dhall.TypeCheck

Methods

pretty :: DetailedTypeError s a -> Doc ann

prettyList :: [DetailedTypeError s a] -> Doc ann

data Censored

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

Constructors

CensoredDetailed (DetailedTypeError Src X)

Censored (TypeError Src X)

Instances

Show Censored

Defined in Dhall.TypeCheck

Methods

showsPrec :: Int -> Censored -> ShowS

show :: Censored -> String

showList :: [Censored] -> ShowS

Exception Censored

Defined in Dhall.TypeCheck

Methods

toException :: Censored -> SomeException

fromException :: SomeException -> Maybe Censored

displayException :: Censored -> String

Pretty Censored

Defined in Dhall.TypeCheck

Methods

pretty :: Censored -> Doc ann

prettyList :: [Censored] -> Doc ann

data TypeMessage s a

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)

IfBranchMustBeTerm Bool (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)

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)

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)

Instances

(Show s, Show a) => Show (TypeMessage s a)

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

Convert a TypeMessage to short- and long-form ErrorMessages

data ErrorMessages

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

• long :: Doc Ann

  Longer and more detailed explanation of the error