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.

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)

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)

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

Defined in Dhall.TypeCheck

Methods

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

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

Data X

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

Defined in Dhall.TypeCheck

Methods

showsPrec :: Int -> X -> ShowS

show :: X -> String

showList :: [X] -> ShowS

Pretty X

Defined in Dhall.TypeCheck

Methods

pretty :: X -> Doc ann

prettyList :: [X] -> Doc ann

FromTerm X

Defined in Dhall.TypeCheck

Methods

decode :: Term -> Maybe X

ToTerm X

Defined in Dhall.TypeCheck

Methods

encode :: X -> Term

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

(Eq a, Pretty s, Pretty a, ToTerm a) => Show (TypeError s a)

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)

Defined in Dhall.TypeCheck

Methods

toException :: TypeError s a -> SomeException

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

displayException :: TypeError s a -> String

(Eq a, Pretty s, Pretty a, ToTerm a) => Pretty (TypeError s a)

Defined in Dhall.TypeCheck

Methods

pretty :: TypeError s a -> Doc ann

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

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

(Eq a, Pretty s, Pretty a, ToTerm a) => Show (DetailedTypeError s a)

Defined in Dhall.TypeCheck

Methods

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

show :: DetailedTypeError s a -> String

showList :: [DetailedTypeError s a] -> ShowS

(Eq a, Pretty s, Pretty a, ToTerm a, Typeable s, Typeable a) => Exception (DetailedTypeError s a)

Defined in Dhall.TypeCheck

Methods

toException :: DetailedTypeError s a -> SomeException

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

displayException :: DetailedTypeError s a -> String

(Eq a, Pretty s, Pretty a, ToTerm a) => Pretty (DetailedTypeError s a)

Defined in Dhall.TypeCheck

Methods

pretty :: DetailedTypeError s a -> Doc ann

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

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)

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)

Defined in Dhall.TypeCheck

Methods

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

show :: TypeMessage s a -> String

showList :: [TypeMessage s a] -> ShowS