dhall-1.30.0: A configuration language guaranteed to terminate

Safe HaskellNone
LanguageHaskell2010

Dhall.TypeCheck

Contents

Description

This module contains the logic for type checking Dhall code

Synopsis

Type-checking

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.

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

messageExpressions :: Applicative f => (Expr s a -> f (Expr t b)) -> TypeMessage s a -> f (TypeMessage t b) Source #

Traversal that traverses every Expr in a TypeMessage

Types

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

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

type X = Void Source #

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 Source #

A structured type error that includes context

Constructors

TypeError 

Fields

Instances
(Eq a, Pretty s, Pretty a) => Show (TypeError s a) Source # 
Instance details

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) Source # 
Instance details

Defined in Dhall.TypeCheck

(Eq a, Pretty s, Pretty a) => Pretty (TypeError s a) Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

pretty :: TypeError s a -> Doc ann #

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

newtype DetailedTypeError s a Source #

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) Source # 
Instance details

Defined in Dhall.TypeCheck

(Eq a, Pretty s, Pretty a, Typeable s, Typeable a) => Exception (DetailedTypeError s a) Source # 
Instance details

Defined in Dhall.TypeCheck

(Eq a, Pretty s, Pretty a) => Pretty (DetailedTypeError s a) Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

pretty :: DetailedTypeError s a -> Doc ann #

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

data Censored Source #

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

Instances
Show Censored Source # 
Instance details

Defined in Dhall.TypeCheck

Exception Censored Source # 
Instance details

Defined in Dhall.TypeCheck

Pretty Censored Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

pretty :: Censored -> Doc ann #

prettyList :: [Censored] -> Doc ann #

data TypeMessage s a Source #

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) 
AlternativeAnnotationMismatch Text (Expr s a) Const Text (Expr s a) Const 
ListAppendMismatch (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) Source # 
Instance details

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 Source #

Convert a TypeMessage to short- and long-form ErrorMessages

data ErrorMessages Source #

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