Kernel.TypingSourceType checking/inference
type typing_error = | KindIsNotTypable| ConvertibilityError of Term.term * Term.typed_context * Term.term * Term.term| AnnotConvertibilityError of Basic.loc
* Basic.ident
* Term.typed_context
* Term.term
* Term.term| VariableNotFound of Basic.loc * Basic.ident * int * Term.typed_context| SortExpected of Term.term * Term.typed_context * Term.term| ProductExpected of Term.term * Term.typed_context * Term.term| InexpectedKind of Term.term * Term.typed_context| DomainFreeLambda of Basic.loc| CannotInferTypeOfPattern of Rule.pattern * Term.typed_context| UnsatisfiableConstraints of Rule.partially_typed_rule
* int * Term.term * Term.term| BracketExprBoundVar of Term.term * Term.typed_context| BracketExpectedTypeBoundVar of Term.term * Term.typed_context * Term.term| BracketExpectedTypeRightVar of Term.term * Term.typed_context * Term.term| TypingCircularity of Basic.loc
* Basic.ident
* int
* Term.typed_context
* Term.term| FreeVariableDependsOnBoundVariable of Basic.loc
* Basic.ident
* int
* Term.typed_context
* Term.term| NotImplementedFeature of Basic.loc| Unconvertible of Basic.loc * Term.term * Term.term| Convertible of Basic.loc * Term.term * Term.term| Inhabit of Basic.loc * Term.term * Term.term