dhall-1.24.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

Types

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

Constructors

X 

Fields

Instances
Eq X Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

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

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

Data X Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> X -> c X #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c X #

toConstr :: X -> Constr #

dataTypeOf :: X -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c X) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c X) #

gmapT :: (forall b. Data b => b -> b) -> X -> X #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> X -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> X -> r #

gmapQ :: (forall d. Data d => d -> u) -> X -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> X -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> X -> m X #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> X -> m X #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> X -> m X #

Show X Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

showsPrec :: Int -> X -> ShowS #

show :: X -> String #

showList :: [X] -> ShowS #

Pretty X Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

pretty :: X -> Doc ann #

prettyList :: [X] -> Doc ann #

FromTerm X Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

decode :: Term -> Maybe X Source #

ToTerm X Source # 
Instance details

Defined in Dhall.TypeCheck

Methods

encode :: X -> Term Source #

data TypeError s a Source #

A structured type error that includes context

Constructors

TypeError 

Fields

Instances
(Eq a, Pretty s, Pretty a, ToTerm 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, ToTerm a, Typeable s, Typeable a) => Exception (TypeError s a) Source # 
Instance details

Defined in Dhall.TypeCheck

(Eq a, Pretty s, Pretty a, ToTerm 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, ToTerm a) => Show (DetailedTypeError s a) Source # 
Instance details

Defined in Dhall.TypeCheck

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

Defined in Dhall.TypeCheck

(Eq a, Pretty s, Pretty a, ToTerm 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 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) 
InvalidOptionalElement (Expr s a) (Expr s a) (Expr s a) 
InvalidOptionalType (Expr s a) 
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) 
InvalidField Text (Expr s a) 
InvalidFieldType Text (Expr s a) 
FieldAnnotationMismatch Text (Expr s a) Const Text (Expr s a) Const 
FieldMismatch Text (Expr s a) Const Text (Expr s a) Const 
InvalidAlternative 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) 
DuplicateAlternative Text 
MustCombineARecord Char (Expr s a) (Expr s a) 
RecordMismatch Char (Expr s a) (Expr s a) Const Const 
CombineTypesRequiresRecordType (Expr s a) (Expr s a) 
RecordTypeMismatch Const Const (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) 
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) 
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 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 #