RefineErrorData.Data
type t =
| UnboundVariable of Ident.t
| FieldNameMismatches of Ident.user list * Ident.user list
| ExpectedField of Basis.Pp.env * S.tele * S.t * Ident.t
| ExpectedEqual of Basis.Pp.env * S.tp * S.t * S.t * Conversion.Error.t
| ExpectedEqualTypes of Basis.Pp.env * S.tp * S.tp * Conversion.Error.t
| ExpectedConnective of connective * Basis.Pp.env * S.tp
| ExpectedDimensionLiteral of int
| ExpectedTrue of Basis.Pp.env * S.t
| VirtualType
| HoleNotPermitted of Basis.Pp.env * S.tp
| BindingNotFound of Ident.user
| UnexpectedShadowing of Ident.user
| CyclicImport of CodeUnit.CodeUnitID.t
| ErrorsInSection
| UnsolvedHoles of int
| ExpectedSignature of Basis.Pp.env * S.tp
| ExpectedKanSignature of Basis.Pp.env * S.t
| ExpectedStructure of Basis.Pp.env * S.t