Safe Haskell	None
Language	Haskell2010

Dhall.TypeCheck

Contents

Type-checking
Types

Description

This module contains the logic for type checking Dhall code

Synopsis

typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X)
typeOf :: Expr s X -> Either (TypeError s X) (Expr s X)
typeWithA :: (Eq a, Pretty a) => Typer a -> Context (Expr s a) -> Expr s a -> Either (TypeError s a) (Expr s a)
checkContext :: Context (Expr s X) -> Either (TypeError s X) ()
messageExpressions :: Applicative f => (Expr s a -> f (Expr t b)) -> TypeMessage s a -> f (TypeMessage t b)
type Typer a = forall s. a -> Expr s a
type X = Void
absurd :: Void -> a
data TypeError s a = TypeError {
- context :: Context (Expr s a)
- current :: Expr s a
- typeMessage :: TypeMessage s a
}
newtype DetailedTypeError s a = DetailedTypeError (TypeError s a)
data Censored
- = CensoredDetailed (DetailedTypeError Src X)
- | Censored (TypeError Src X)
data TypeMessage s a
- = 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)
- | 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)
- | 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 (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)

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

Constructors

CensoredDetailed (DetailedTypeError Src X)
Censored (TypeError Src X)

Instances

Show Censored Source #
Instance details Defined in Dhall.TypeCheck Methods showsPrec :: Int -> Censored -> ShowS # show :: Censored -> String # showList :: [Censored] -> ShowS #
Exception Censored Source #
Instance details Defined in Dhall.TypeCheck Methods toException :: Censored -> SomeException # fromException :: SomeException -> Maybe Censored # displayException :: Censored -> String #
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)
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)
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 (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 #