Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- 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)
- | InvalidRecordCompletion Text (Expr s a)
- | CompletionSchemaMustBeARecord (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 Text (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.
typeWithA :: (Eq a, Pretty a) => Typer a -> Context (Expr s a) -> Expr s a -> Either (TypeError s a) (Expr s a) Source #
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
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
A structured type error that includes context
TypeError | |
|
Instances
(Eq a, Pretty s, Pretty a) => Show (TypeError s a) Source # | |
(Eq a, Pretty s, Pretty a, Typeable s, Typeable a) => Exception (TypeError s a) Source # | |
Defined in Dhall.TypeCheck 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 # | |
Defined in Dhall.TypeCheck |
newtype DetailedTypeError s a Source #
Newtype used to wrap error messages so that they render with a more detailed explanation of what went wrong
DetailedTypeError (TypeError s a) |
Instances
(Eq a, Pretty s, Pretty a) => Show (DetailedTypeError s a) Source # | |
Defined in Dhall.TypeCheck 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 # | |
Defined in Dhall.TypeCheck 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 # | |
Defined in Dhall.TypeCheck pretty :: DetailedTypeError s a -> Doc ann # prettyList :: [DetailedTypeError s a] -> Doc ann # |
Wrap a type error in this exception type to censor source code and
Expr
literals from the error message
Instances
Show Censored Source # | |
Exception Censored Source # | |
Defined in Dhall.TypeCheck toException :: Censored -> SomeException # fromException :: SomeException -> Maybe Censored # displayException :: Censored -> String # | |
Pretty Censored Source # | |
Defined in Dhall.TypeCheck |
data TypeMessage s a Source #
The specific type error
Instances
(Show s, Show a) => Show (TypeMessage s a) Source # | |
Defined in Dhall.TypeCheck showsPrec :: Int -> TypeMessage s a -> ShowS # show :: TypeMessage s a -> String # showList :: [TypeMessage s a] -> ShowS # |