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) (Expr s X)

Type-check an expression and return the expression's type if type-checking suceeds 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.

typeOf :: Expr s X -> Either (TypeError s) (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.

Types

newtype X

Like Void, except with a shorter inferred type

Constructors

X

Fields

absurd :: forall a. a

Instances

Show X

Buildable X

data TypeError s

A structured type error that includes context

Constructors

TypeError

Fields

context :: Context (Expr s X)

current :: Expr s X

typeMessage :: TypeMessage s

Instances

Buildable s => Show (TypeError s)

(Buildable s, Typeable * s) => Exception (TypeError s)

Buildable s => Buildable (TypeError s)

newtype DetailedTypeError s

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

Constructors

DetailedTypeError (TypeError s)

Instances

Buildable s => Show (DetailedTypeError s)

(Buildable s, Typeable * s) => Exception (DetailedTypeError s)

Buildable s => Buildable (DetailedTypeError s)

data TypeMessage s

The specific type error

Constructors

UnboundVariable

InvalidInputType (Expr s X)

InvalidOutputType (Expr s X)

NotAFunction (Expr s X) (Expr s X)

TypeMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X)

AnnotMismatch (Expr s X) (Expr s X) (Expr s X)

Untyped

InvalidListElement Int (Expr s X) (Expr s X) (Expr s X)

InvalidListType (Expr s X)

InvalidOptionalElement (Expr s X) (Expr s X) (Expr s X)

InvalidOptionalLiteral Int

InvalidOptionalType (Expr s X)

InvalidPredicate (Expr s X) (Expr s X)

IfBranchMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X)

IfBranchMustBeTerm Bool (Expr s X) (Expr s X) (Expr s X)

InvalidField Text (Expr s X)

InvalidFieldType Text (Expr s X)

InvalidAlternative Text (Expr s X)

InvalidAlternativeType Text (Expr s X)

DuplicateAlternative Text

MustCombineARecord (Expr s X) (Expr s X)

FieldCollision Text

MustMergeARecord (Expr s X) (Expr s X)

MustMergeUnion (Expr s X) (Expr s X)

UnusedHandler (Set Text)

MissingHandler (Set Text)

HandlerInputTypeMismatch Text (Expr s X) (Expr s X)

HandlerOutputTypeMismatch Text (Expr s X) (Expr s X)

HandlerNotAFunction Text (Expr s X)

NotARecord Text (Expr s X) (Expr s X)

MissingField Text (Expr s X)

CantAnd (Expr s X) (Expr s X)

CantOr (Expr s X) (Expr s X)

CantEQ (Expr s X) (Expr s X)

CantNE (Expr s X) (Expr s X)

CantTextAppend (Expr s X) (Expr s X)

CantAdd (Expr s X) (Expr s X)

CantMultiply (Expr s X) (Expr s X)

NoDependentLet (Expr s X) (Expr s X)

NoDependentTypes (Expr s X) (Expr s X)

Instances

Show s => Show (TypeMessage s)