Original bug ID: 5888
Reporter: @edwintorok
Assigned to: @garrigue
Status: acknowledged (set by @garrigue on 2013-02-04T10:20:56Z)
Resolution: open
Priority: normal
Severity: feature
Platform: Linux
OS: Debian GNU/Linux
OS Version: wheezy
Version: 4.00.1
Target version: undecided
Category: typing
Tags: patch
Related to: #5889
Child of: #7338
Monitored by: @Drup @bobzhang @gasche @edwintorok @yakobowski

Bug description

ML discussion: https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00023.html

I'm fine with how the language works, but the type error generated by the compiler could be improved, currently it only tells me that the values do not match.

Attached is an example patch that implements some improved type error messages.

With polymorphic types it may not be immediately obvious what is wrong, so it'd be good if the compiler would be more explicit about the error.
It already gives helpful hints when polymorphic types lack a tag or the tags' type do not match. Unfortunately when module signatures are checked it doesn't
even give those errors.

Steps to reproduce

module Bad3 : sig
val copy: [< A of a | B of a ] -> [< A of a | C of a] -> unit
end = struct
let generic (a: [< A of a | B of a]) (b: [< A of a | C of a]) = ()
let specific a b = false
let copy a b = match a, b with
| A x, A y ->
if not (specific (A x) (A y)) then
generic a b
| _, _ ->
generic a b
end

Error: Signature mismatch:
...
Values do not match:
val copy :
[< A of a | B of a > A ] -> [< A of a | C of a > A ] -> unit
is not included in
val copy : [< A of a | B of a ] -> [< A of a | C of a ] -> unit

Additional information

Would be good to have more detailed errors for:

• module signature vs implementation: inspect arrows,tuples, etc. and report
  exactly what causes the type error (like it is already done when signatures are not invovled)
• mandatory vs optional tags in polymorphic variants: [< A] vs [> A]
• tuples with different lengths
• different order of function parameter labels

Would also good to have (I didn't implement it):

• origin/trace of type inference (i.e. wildcard match case, etc.)
• remove "impossible" tags (i.e. A of string&int or A of ) when expanding types in error messages
• warn when intersection of polymorphic variants is empty, i.e. [< A of [< B] & [< C]) or [< A of string&int], etc.

I've attached 3 patches, and also a combined diff of the 3 patches. There are probably easier/more elegant ways to implement it, consider them a draft.
Also I've only updated testsuite/tests/typing-misc, some of the others might have to be updated in light of the new error messages.

Also please improve the documentation using the very good explanations/examples by Leo White and Jacques Garrigue, in particular the part about
why [> `A] is inferred for matches with wildcard branches:

http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.html#toc36
http://caml.inria.fr/pub/docs/manual-ocaml-4.00/types.html#polymorphic-variant-type
https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00019.html
https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00019.html

Note: the manual006.html#toc36 should probably have a link to types.html#polymorphic-variant-type.

File attachments

• 0001-Propagate-details-about-type-unification-error-for-m.patch
• 0002-Better-type-error-reporting-for-polymorphic-variants.patch
• 0003-Improve-type-error-messages-when-dealing-with-labels.patch
• 0004-Fix-order-of-types-in-message.patch
• better-type-errors-unified.patch
• temp1.ml