dhall-1.19.1: A configuration language guaranteed to terminate

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)
  - | 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 Source # (/=) :: X -> X -> Bool Source #
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 Source #

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

toConstr :: X -> Constr Source #

dataTypeOf :: X -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show X Source # |
Instance details Defined in Dhall.TypeCheck Methods showsPrec :: Int -> X -> ShowS Source # show :: X -> String Source # showList :: [X] -> ShowS Source #
Pretty X Source # |
Instance details Defined in Dhall.TypeCheck Methods pretty :: X -> Doc ann Source # prettyList :: [X] -> Doc ann Source #

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 Source # show :: TypeError s a -> String Source # showList :: [TypeError s a] -> ShowS Source #
(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 Source # fromException :: SomeException -> Maybe (TypeError s a) Source # displayException :: TypeError s a -> String Source #
(Eq a, Pretty s, Pretty a) => Pretty (TypeError s a) Source # |
Instance details Defined in Dhall.TypeCheck Methods pretty :: TypeError s a -> Doc ann Source # prettyList :: [TypeError s a] -> Doc ann Source #

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 Source # show :: DetailedTypeError s a -> String Source # showList :: [DetailedTypeError s a] -> ShowS Source #
(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 Source # fromException :: SomeException -> Maybe (DetailedTypeError s a) Source # displayException :: DetailedTypeError s a -> String Source #
(Eq a, Pretty s, Pretty a) => Pretty (DetailedTypeError s a) Source # |
Instance details Defined in Dhall.TypeCheck Methods pretty :: DetailedTypeError s a -> Doc ann Source # prettyList :: [DetailedTypeError s a] -> Doc ann Source #

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) |
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 Source # show :: TypeMessage s a -> String Source # showList :: [TypeMessage s a] -> ShowS Source #