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

Methods

showsPrec :: Int -> X -> ShowS

show :: X -> String

showList :: [X] -> ShowS

Buildable X

Methods

build :: X -> Builder

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)

Methods

showsPrec :: Int -> TypeError s -> ShowS

show :: TypeError s -> String

showList :: [TypeError s] -> ShowS

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

Methods

toException :: TypeError s -> SomeException

fromException :: SomeException -> Maybe (TypeError s)

displayException :: TypeError s -> String

Buildable s => Buildable (TypeError s)

Methods

build :: TypeError s -> Builder

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)

Methods

showsPrec :: Int -> DetailedTypeError s -> ShowS

show :: DetailedTypeError s -> String

showList :: [DetailedTypeError s] -> ShowS

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

Methods

toException :: DetailedTypeError s -> SomeException

fromException :: SomeException -> Maybe (DetailedTypeError s)

displayException :: DetailedTypeError s -> String

Buildable s => Buildable (DetailedTypeError s)

Methods

build :: DetailedTypeError s -> Builder

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)

Methods

showsPrec :: Int -> TypeMessage s -> ShowS

show :: TypeMessage s -> String

showList :: [TypeMessage s] -> ShowS