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

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

[Carette, Jacques]

[-- Attachment #1: Type: text/html, Size: 1013 bytes --]

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

[Gabriel Scherer]

This does not exist to my knowledge. I think that in a bug report, it
would be interesting if you could include some reproducible code and
an example of the error messages that are not readable. I would expect
that a better solution exists, that expands enough of the paths to
clarify the error, without expanding constraints that are not related
to the type error.

One thing you might try to play with is the -short-paths options, that
tries to print shorter types (but is also possibly less predictable);
it can  expand more if that can result in showing a shorter path, so
for types that are synonyms of existing paths plus constraints it
might result in constraint expansion. (I suspect it will not solve
your problem, but that it may be of interest to other people with
unclear type error messages.)

On Thu, Jun 2, 2016 at 3:18 PM, Carette, Jacques <carette@mcmaster.ca> 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

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

[Yaron Minsky]

Have you tired using the short-paths flag?  This doesn't completely
expand the types, but it does a good job of picking the "right" type:
the heuristic is (roughly) to pick the type alias with the fewest
number of dots, and amongst those, pick the one defined most recently.
It tends to make type errors quite a lot better, but I admit I'm not
sure it would help in the case you describe.

y



On Thu, Jun 2, 2016 at 3:44 PM, Gabriel Scherer
<gabriel.scherer@gmail.com> wrote:
> This does not exist to my knowledge. I think that in a bug report, it
> would be interesting if you could include some reproducible code and
> an example of the error messages that are not readable. I would expect
> that a better solution exists, that expands enough of the paths to
> clarify the error, without expanding constraints that are not related
> to the type error.
>
> One thing you might try to play with is the -short-paths options, that
> tries to print shorter types (but is also possibly less predictable);
> it can  expand more if that can result in showing a shorter path, so
> for types that are synonyms of existing paths plus constraints it
> might result in constraint expansion. (I suspect it will not solve
> your problem, but that it may be of interest to other people with
> unclear type error messages.)
>
> On Thu, Jun 2, 2016 at 3:18 PM, Carette, Jacques <carette@mcmaster.ca> 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
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

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

[Carette, Jacques]

I will try the ``short-paths'' flag and report back.  We're also trying to produce a reasonably-sized self-contained example.

(I did not know about short-paths, so that is definitely worth a try)

Jacques

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

[Jacques Garrigue]

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

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

[Carette, Jacques]

[-- Attachment #1: Type: text/plain, Size: 2875 bytes --]

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

[-- Attachment #2: reproduce.ml --]
[-- Type: application/octet-stream, Size: 4358 bytes --]

type ('p,'v) monad = 's -> ('s -> 'v -> 'w) -> 'w
  constraint 'p = <state : 's; answer : 'w; ..>

let ret (a :'v) : ('p,'v) monad = fun s k -> k s a

let (let!) (m : ('p,'v) monad) (f : 'v -> ('p,'u) monad) : ('p,'u) monad
  = fun s k -> m s (fun s' b -> f b s' k)

let k0 _ v = v

module type T = sig
  type 'b abstract

  type ('pc,'p) cmonad_constraint = unit
    constraint
      'p = <state : 's list; answer : 'w abstract>
    constraint
      'pc = <answer : 'w; state : 's; ..>

  type ('pc,'v) cmonad = ('p, 'v abstract) monad
    constraint _ = ('pc,'p) cmonad_constraint

  val genrecloop :
    (('b -> 'c) abstract ->
    'b abstract -> 'd -> ('e -> 'c abstract -> 'c abstract) -> 'c abstract) ->
    'b abstract -> 'd -> ('d -> 'c abstract -> 'g) -> 'g
  val applyM :
    ('b -> 'c) abstract -> 'b abstract -> 'd -> ('d -> 'c abstract -> 'e) -> 'e
  module Pair :
    sig
      val unpair : ('b * 'c) abstract -> 'b abstract * 'c abstract
    end
  module Idx :
    sig
      val zero : int abstract
      val succ : int abstract -> int abstract
    end
  module Tuple :
    sig
      val tup2 : 'b abstract -> 'c abstract -> ('b * 'c) abstract
    end
  module CList :
    sig
      val nil : 'b list abstract
      val cons : 'b abstract -> 'b list abstract -> 'b list abstract
      val matchListM :
        'b list abstract ->
        ('p, 'c) cmonad ->
        ('b abstract -> 'b list abstract -> ('p, 'c) cmonad) ->
        ('p, 'c) cmonad
    end
end

module PseudoCode = struct

  type 'b abstract = unit -> 'b

  type ('pc,'p) cmonad_constraint = unit
    constraint
      'p = <state : 's list; answer : 'w abstract>
    constraint
      'pc = <answer : 'w; state : 's; ..>

  type ('pc,'v) cmonad = ('p, 'v abstract) monad
    constraint _ = ('pc,'p) cmonad_constraint
  let genrecloop gen rtarg = fun s k -> k s
    (fun () -> let rec loop j = gen (fun () -> loop) (fun () -> j) s k0 () in
    loop (rtarg ()))
  let apply  f x = fun () -> (f ()) (x ())
  let applyM  f x = ret (apply f x)
  module Pair = struct
  (* To be able to deconstruct pairs in monadic code:
    perform (a,b) <-- ret (unpair pv) *)
    let unpair x = ((fun () -> fst (x ())), fun () -> snd (x ()))
    let fst x = (fun () -> fst (x ()))
    let snd x = (fun () -> snd (x ()))
  end

  module Idx = struct
    let zero = fun () -> 0
    let succ a = fun () -> (a ()) + 1
  end
  module Tuple = struct
    let tup2 a b = fun () -> ( (a ()), (b ()) )
  end
  module CList = struct
    let nil = fun () -> []
    let cons a b = fun () -> (a ()) :: (b ())
    let matchListM l empty nonempty = fun s k -> (fun () ->
      match l () with
        | []   -> empty s k ()
        | h::t -> nonempty (fun () -> h) (fun () -> t) s k ())
  end
end

module type Value = sig
  type value
end

module IntV = struct
  type value = int
end

module Traverse (CODE: T) = struct
  open CODE

  module ContainerLib (V:Value) (L:Value) = struct
    module type Sig = sig
      type value = V.value
      type 'a container
      type eltdesc
      type loopdata = L.value
      val traverseexercise :
        value container abstract ->
        (eltdesc abstract -> loopdata abstract -> (value * loopdata) abstract) ->
        loopdata abstract ->
(*         ('a, value container) cmonad *)
        ('a, value) cmonad
    end
  end

  module ListContainerLib (V : Value) (L : Value) = struct
    type value = V.value
    type 'a container = 'a list
    type eltdesc = value
    type loopdata = L.value

    let traverseexercise lst f data  =
      let gen self tup =
      let (lst, i) = Pair.unpair tup in
      CList.matchListM lst
        (ret CList.nil)
        (fun h t ->
        let (v, i2) = Pair.unpair (f (h) i) in
        let! r = (applyM self (Tuple.tup2 t i2)) in
        ret (CList.cons v r))
      in genrecloop gen (Tuple.tup2 lst data)
  end

  module Ex (Container : ContainerLib (IntV) (IntV).Sig) = struct
    let traverseexercise container =
      let body = fun _ n -> Tuple.tup2 n (Idx.succ n) in
      Container.traverseexercise container body Idx.zero
  end

end

module Test = struct
  module TC = Traverse(PseudoCode)
  module LCII = TC.ListContainerLib (IntV) (IntV)
  module LT = TC.Ex (LCII)
end

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

[Yaron Minsky]

[-- Attachment #1: Type: text/plain, Size: 4173 bytes --]

Diffs are often useful in visualizing such things.  not sure how helpful it
is in this case, but it does at least make it a bit clearer what's lined
up.  This was generated with our patdiff tool.

@@@@@@@@@@ -1,7 +1,7 @@@@@@@@@@
           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*+|           loopdata container
PseudoCode.abstract ->+|           (loopdata PseudoCode.abstract ->+|
          loopdata PseudoCode.abstract ->+|            (loopdata *
loopdata) PseudoCode.abstract) ->+|           loopdata
PseudoCode.abstract ->+|           (< answer : 'a; state : 'b; .. >,
loopdata) PseudoCode.cmonad


On Fri, Jun 3, 2016 at 11:42 AM, Carette, Jacques <carette@mcmaster.ca>
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
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 8511 bytes --]

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

[Jacques Garrigue]

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