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 => 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) ()
type Typer a = forall s. a -> Expr s a
newtype X = X {
- absurd :: forall a. 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 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)
- | 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)
- | 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)

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 => 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 absurd :: forall a. a

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 #

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) => 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 Methods toException :: TypeError s a -> SomeException # fromException :: SomeException -> Maybe (TypeError s a) # displayException :: TypeError s a -> String #
(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 Methods showsPrec :: Int -> DetailedTypeError s a -> ShowS # show :: DetailedTypeError s a -> String # showList :: [DetailedTypeError s a] -> ShowS #
(Eq a, Pretty s, Pretty 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) => 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)
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 #