A constraint system for a SML type error slicer
Vincent Rahli, J. B. Wells, Fairouz Kamareddine · Open Repository and Bibliography (University of Luxembourg) · 2010
Existing compilers for many languages have confusing type error messages.Type error slicing (TES) helps the programmer by isolating the part of a program contributing to a type error, but unfortunately TES was initially done for a tiny toy language.Extending TES to a full programming language is extremely challenging, and for SML we needed a number of innovations and generalisations.Some issues would be faced for any language, and some are SMLspecific but representative of the complexity of language-specific issues likely to be faced for other languages.We solve both kinds of issues and present a simple, general constraint system for providing type error slices for ill-typed programs.Our constraint system elegantly and efficiently handles features like the intricate open SML feature.We show how the simple clarity of type error slices can demystify language features known to confuse users.We also provide in an appendix a case study on how to use our TES to help modifying user data types, and extend the core language presented in the main body of this report to handle more of the implementation of our system.These extensions allow handling local declarations, type declarations and some uses of signatures.Finally, if m is true then we return 1 otherwise we return x.Unfortunately, this piece of code is untypable and SML/NJ reports the following error message which blames y's body:Error: types of if branches do not agree [literal] then branch: int else branch: bool in expression: if m then 1 else xThe programming error here, as our type error slice explains clearly, is that opening S causes S's declarations to shadow the current typing environment.Because Y is opened in S, the three structures A, X and M are part of S's declarations.Hence, when opening S in T, the structure X which was in our current typing environment is shadowed by the one defined in Y.One can solve this programming error by replacing "open S open X" by "open S X".Our type error slice rules out x's declarations in X and S and clearly shows why x does not have the expected type.SML/NJ's report leaves us to track down x's binding by hand. Merged minimal error slices.We have found cases needing the display of many minimal errors at once.One important case is in record field name clashes where, e.g., the highlighting val {foo,bar} = {fool=0,bar=1} reports two minimal errors at once: that fool is not in {foo, bar} and foo is not in {fool, bar}.This merged error is preferable over the minimal errors beca use of the explosion in the number of minimal slices.Green highlights the fields that are common to different minimal slices.For merged slices minimality is understood as follows: retain a single blue/purple field name in one of the two clashing records and all field names in the other. Mathematical definitions and notationsLet i, j, n, m be metavariables ranging over N, the set of natural numbers.If a metavariable v ranges over a class C , then the metavariables vx (where x can be anything) and the metavariables v ′ , v ′′ , etc., also range over C .Let s range over sets.If v ranges over s, then let v range over P(s), the power set of s.Let dj(s1, . . ., sn) ("disjoint") hold iff for all i, j ∈ {1, . . ., n}, if i = j then si ∩sj = ∅.Let s1 ⊎s2 be s1∪s2 if dj(s1, s2) and undefined otherwise.Let R range over binary relations (we write x , y for a pair).Given a relation R let dom(R) = {x | x, y ∈ R} and ran(R) = {y | x, y ∈ R}.Let s ⊳ -R = { x , y ∈ R | x ∈ s}.Let f range over functions, let s → s ′ = {f | dom(f ) ⊆ s ∧ ran(f ) ⊆ s ′ }, and let x → y be an alternative notation for x , y used when writing some functions.A tuple t is a function such that dom(t) ⊂ N and if 1 ≤ k ∈ dom(t) then k -1 ∈ dom(t).Let t range over tuples.We write the tuple {0 → x0, . . ., n → xn } as x0, . . ., xn .We define the appending x1, . . ., xi @ y1, . . ., yj of two tuples as the tuple x1, . . ., xi, y1, . . ., yj .If v ranges over s, -→ v is defined to range over tuple(s) = {t | ran(t) ⊆ s}.