Re: [Caml-list] Option to fully expand types in error messages?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

I see.
This is a problem with mismatching signatures.
This is much less well supported than unification errors (internally, the function called is moregeneral, which does not rely on unification).
This has already been much improved by tracking the mismatching item better, and -short-paths helps also by normalizing some types, but we should also track mismatches inside type schemes.

As you suggest, another solution would be full expansion.
This is a bad idea with objects, but may make sense for programs not using recursive types.
Note however that there is no function doing this kind of expansion inside the compiler...

Jacques

On 2016/06/04 00:42, "Carette, Jacques" wrote:
> 
> So here is an actual example.  The error I get is
> ocamlc -short-paths -c reproduce.ml 
> File "reproduce.ml", line 148, characters 21-25:
> Error: Signature mismatch:
>       ...
>       Values do not match:
>         val traverseexercise :
>           'a container PseudoCode.abstract ->
>           ('a PseudoCode.abstract ->
>            'b PseudoCode.abstract -> ('c * 'b) PseudoCode.abstract) ->
>           'b PseudoCode.abstract ->
>           'd container ->
>           ('d container -> 'c container PseudoCode.abstract -> 'e) -> 'e
>       is not included in
>         val traverseexercise :
>           loopdata container PseudoCode.abstract ->
>           (loopdata PseudoCode.abstract ->
>            loopdata PseudoCode.abstract ->
>            (loopdata * loopdata) PseudoCode.abstract) ->
>           loopdata PseudoCode.abstract ->
>           (< answer : 'a; state : 'b; .. >, loopdata) PseudoCode.cmonad
>       File "reproduce.ml", line 111, characters 6-206: Expected declaration
>       File "reproduce.ml", line 125, characters 8-24: Actual declaration
> 
> I can't tell from the above error what the actual cause is.  The full code is attached.  [This code is quite reduced already.  It is kept at this size to show in more detail the kinds of errors we're seeing.]
> 
> Any 'hint' from OCaml as to the precise nature of the non-match would sure be appreciated.
> 
> Jacques
> 
> ________________________________________
> From: Jacques Garrigue [garrigue@math.nagoya-u.ac.jp]
> Sent: June 2, 2016 19:59
> To: Carette, Jacques
> Cc: OCaML List Mailing
> Subject: Re: [Caml-list] Option to fully expand types in error messages?
> 
> On 2016/06/03 04:18, "Carette, Jacques" wrote:
>> 
>> In writing some code which uses a lot of monads with underlying types which use constraints, even simple errors can lead to extremely hard to read error messages.  The main reason is that the two types given in errors are partially expanded, to different levels.  This frequently means that the part where the type checker detects a mismatch is (extremely) opaque to human eyes.
>> 
>> In that case, it would actually be preferable to fully expand the types.  Yes, that will produce wallpaper.  But at least the mismatch should be considerably easier to catch.
>> 
>> Does this already exist, or should I submit a feature request?
>> 
>> Jacques
> 
> In the error message, types are expanded just enough to get down to the conflict.
> If the conflict is not visible at that point, this is probably a scoping error (and there should be an extra line stating that);
> otherwise this should be seen as a bug.
> As Yaron pointed, -short-paths can help by at least giving a normal form for paths (which may not be the expansion, but should be unique in the error context). But it will not expand a type if the expansion is not a type constructor, or if the parameters are different.
> 
> Jacques