dhall-1.12.0: A configuration language guaranteed to terminate

Safe HaskellNone




This module contains the logic for type checking Dhall code



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.

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


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

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

newtype X Source #

Like Void, except with a shorter inferred type





Eq X Source # 


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

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

Show X Source # 


showsPrec :: Int -> X -> ShowS #

show :: X -> String #

showList :: [X] -> ShowS #

Buildable X Source # 


build :: X -> Builder #

Pretty X Source # 


pretty :: X -> Doc ann #

prettyList :: [X] -> Doc ann #

data TypeError s a Source #

A structured type error that includes context




newtype DetailedTypeError s a Source #

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


DetailedTypeError (TypeError s a) 

data TypeMessage s a Source #

The specific type error


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


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


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

show :: TypeMessage s a -> String #

showList :: [TypeMessage s a] -> ShowS #