:: a typeCtrl KGHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05
Moduledhall-1.42.3Haskell2010
This module contains the logic for type checking Dhall code
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.
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
Traversal that traverses every Expr in a TypeMessage
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
A structured type error that includes context
TypeErrorcontext :: Context (Expr s a)current :: Expr s atypeMessage :: TypeMessage s a(Eq a, Pretty s, Pretty a) => Show (TypeError s a)Defined in dhall-1.42.3 · Dhall.TypeCheck(Eq a, Pretty s, Pretty a, Typeable s, Typeable a) => Exception (TypeError s a)Defined in dhall-1.42.3 · Dhall.TypeCheck(Eq a, Pretty s, Pretty a) => Pretty (TypeError s a)Defined in dhall-1.42.3 · Dhall.TypeCheckNewtype used to wrap error messages so that they render with a more detailed explanation of what went wrong
DetailedTypeError (TypeError s a)(Eq a, Pretty s, Pretty a) => Show (DetailedTypeError s a)Defined in dhall-1.42.3 · Dhall.TypeCheck(Eq a, Pretty s, Pretty a, Typeable s, Typeable a) => Exception (DetailedTypeError s a)Defined in dhall-1.42.3 · Dhall.TypeCheck(Eq a, Pretty s, Pretty a) => Pretty (DetailedTypeError s a)Defined in dhall-1.42.3 · Dhall.TypeCheckWrap a type error in this exception type to censor source code and Text literals from the error message
The specific type error
UnboundVariable TextInvalidInputType (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)UntypedMissingListTypeMismatchedListElements Int (Expr s a) (Expr s a) (Expr s a)InvalidListType (Expr s a)ListLitInvariantInvalidSome (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)InvalidFieldType Text (Expr s a)InvalidAlternativeType Text (Expr s a)ListAppendMismatch (Expr s a) (Expr s a)MustCombineARecord Char (Expr s a) (Expr s a)InvalidDuplicateField Text (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)DuplicateFieldCannotBeMerged (NonEmpty Text)FieldCollision (NonEmpty Text)FieldTypeCollision (NonEmpty Text)MustMergeARecord (Expr s a) (Expr s a)MustMergeUnionOrOptional (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)MissingToMapTypeUnusedHandler (Set Text)MissingHandler Text (Set Text)HandlerInputTypeMismatch Text (Expr s a) (Expr s a)DisallowedHandlerType Text (Expr s a) (Expr s a) TextHandlerOutputTypeMismatch Text (Expr s a) Text (Expr s a)MissingMergeTypeHandlerNotAFunction Text (Expr s a)CantAccess Text (Expr s a) (Expr s a)CantProject Text (Expr s a) (Expr s a)CantProjectByExpression (Expr s a)DuplicateProjectionLabel TextMissingField 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)NotWithARecord (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)OptionalWithTypeMismatchNotALabelPathNotAQuestionPath TextShowConstructorNotOnUnion(Show s, Show a) => Show (TypeMessage s a)Defined in dhall-1.42.3 · Dhall.TypeCheckConvert a TypeMessage to short- and long-form ErrorMessages
Output of prettyTypeMessage, containing short- and long-form error messages