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.

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 => 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

Types

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

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

newtype X

Like Void, except with a shorter inferred type

Constructors

X

Fields

• absurd :: forall a. a

Instances

Eq X

Methods

(==) :: X -> X -> Bool

(/=) :: X -> X -> Bool

Show X

Methods

showsPrec :: Int -> X -> ShowS

show :: X -> String

showList :: [X] -> ShowS

Buildable X

Methods

build :: X -> Builder

Pretty X

Methods

pretty :: X -> Doc ann

prettyList :: [X] -> Doc ann

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

(Buildable a, Buildable s) => Show (TypeError s a)

Methods

showsPrec :: Int -> TypeError s a -> ShowS

show :: TypeError s a -> String

showList :: [TypeError s a] -> ShowS

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

Methods

toException :: TypeError s a -> SomeException

fromException :: SomeException -> Maybe (TypeError s a)

displayException :: TypeError s a -> String

(Buildable a, Buildable s) => Buildable (TypeError s a)

Methods

build :: TypeError s a -> Builder

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

(Buildable a, Buildable s) => Show (DetailedTypeError s a)

Methods

showsPrec :: Int -> DetailedTypeError s a -> ShowS

show :: DetailedTypeError s a -> String

showList :: [DetailedTypeError s a] -> ShowS

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

Methods

toException :: DetailedTypeError s a -> SomeException

fromException :: SomeException -> Maybe (DetailedTypeError s a)

displayException :: DetailedTypeError s a -> String

(Buildable a, Buildable s) => Buildable (DetailedTypeError s a)

Methods

build :: DetailedTypeError s a -> Builder

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)

InvalidOptionalElement (Expr s a) (Expr s a) (Expr s a)

InvalidOptionalType (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)

InvalidField Text (Expr s a)

InvalidFieldType Text (Expr s a)

InvalidAlternative Text (Expr s a)

InvalidAlternativeType Text (Expr s a)

ListAppendMismatch (Expr s a) (Expr s a)

DuplicateAlternative Text

MustCombineARecord Char (Expr s a) (Expr s a)

FieldCollision Text

MustMergeARecord (Expr s a) (Expr s a)

MustMergeUnion (Expr s a) (Expr s a)

UnusedHandler (Set Text)

MissingHandler (Set Text)

HandlerInputTypeMismatch Text (Expr s a) (Expr s a)

HandlerOutputTypeMismatch Text (Expr s a) Text (Expr s a)

InvalidHandlerOutputType Text (Expr s a) (Expr s a)

MissingMergeType

HandlerNotAFunction Text (Expr s a)

ConstructorsRequiresAUnionType (Expr s a) (Expr s a)

NotARecord Text (Expr s a) (Expr s a)

MissingField Text (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)

NoDependentTypes (Expr s a) (Expr s a)

Instances

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

Methods

showsPrec :: Int -> TypeMessage s a -> ShowS

show :: TypeMessage s a -> String

showList :: [TypeMessage s a] -> ShowS