Printing of types

Printing of types

[Jacques Carette]

When looking at inferred types in the presence of modules and 
combinations of abstract and concrete types, the results are often quite 
puzzling.  For small pieces of code, it is not a big issue.  When one is 
using 4th-order functors (!), with a mixture of abstract and concrete 
types, a fair amount of type synonyms, error message become extremely 
difficult to interpret! 

Below is some (largish for an email) code that demonstrates this.  It 
seems difficult to show how puzzling this gets with much smaller code, 
although one can indeed reproduce the behaviour with smaller code.  
Consider first
module Sig = struct
  type domain_is_field
  type domain_is_ring
  module type DOMAIN = sig
    type kind
    type v
    val z : v
  end
  module type COLL = sig
    module Dom : DOMAIN
    type coll
  end
end

module Doms = struct
  open Sig
  module FDomain = struct
    type kind = domain_is_field
    type v = float
    let z = 0.0
  end
  module IDomain = struct
    type kind = domain_is_ring
    type v = int
    let z = 0
  end
  module GColl(Dom:DOMAIN) =
    struct
      module Dom = Dom
      type coll = Dom.v list
    end
end ;;

In the above, the printed types all seem quite reasonable.
Now we start with some more complex stuff:
module GEF = struct
  open Sig
  module DivisionUpdate
      (C:COLL with type Dom.kind = domain_is_field) = struct
    let update x = x
  end
  module Gen(C: COLL)
      (Update: functor(C:COLL with type Dom.kind = C.Dom.kind)
               -> sig val update : C.Dom.v -> C.Dom.v end) =
    struct
      module U = Update(C)
      let foo = U.update(C.Dom.z)
    end
end;;

where the printed type is
#                             module GEF :
  sig
    module DivisionUpdate :
      functor
        (C : sig
               module Dom :
                 sig type kind = Sig.domain_is_field type v val z : v end
               type coll
             end) ->
        sig val update : 'a -> 'a end
    module Gen :
      functor (C : Sig.COLL) ->
        functor
          (Update : functor
                      (C : sig
                             module Dom :
                               sig
                                 type kind = C.Dom.kind
                                 type v
                                 val z : v
                               end
                             type coll
                           end) ->
                      sig val update : C.Dom.v -> C.Dom.v end) ->
          sig
            module U : sig val update : C.Dom.v -> C.Dom.v end
            val foo : C.Dom.v
          end
  end
which seems fair enough.  When we start to "test" this, we get:
module Test = GEF.Gen(Doms.GColl(Doms.FDomain))(GEF.DivisionUpdate);;
let test = Test.foo;;

#   module Test :
  sig
    module U :
      sig
        val update :
          Doms.GColl(Doms.FDomain).Dom.v -> Doms.GColl(Doms.FDomain).Dom.v
      end
    val foo : Doms.GColl(Doms.FDomain).Dom.v
  end
# val test : Doms.GColl(Doms.FDomain).Dom.v = 0.

Note how the type of update and foo look very "complex", even though the 
typechecker seems to know quite well that 'test' is actually of type 
float.  How is one supposed to know that the typechecker knows this and 
that ...Dom.v is not abstract?

If we continue in that vein, contrast the following:
module C_F = Doms.GColl(Doms.FDomain);;
module Test1 = GEF.Gen(C_F)(GEF.DivisionUpdate);; (* works *)

module C_I = Doms.GColl(Doms.IDomain);;
module Test2 = GEF.Gen(C_I)(GEF.DivisionUpdate);; (* throws an error, as 
expected *)

The biggest difference is that FDomain has kind = domain_is_field while 
IDomain has kind = domain_is_ring. 
Let's look at the printed type of C_F and Test1:
#   module C_F :
  sig
    module Dom :
      sig type kind = Doms.FDomain.kind type v = Doms.FDomain.v val z : 
v end
    type coll = Dom.v list
  end
# module Test1 :
  sig
    module U : sig val update : C_F.Dom.v -> C_F.Dom.v end
    val foo : C_F.Dom.v
  end

Why Doms.FDomain.kind instead of Sigs.domain_is_field for the kind?  
Since test1 *works*, clearly these are known to be the same.
Also, not how foo has type C_F.Dom.v -- which one has to chase to Dom.v, 
to Doms.FDomain.v, and finally to float.  When this occurs in an error 
message, having to do 4 (or more) levels of type-expansions can be quite 
difficult.  (And misleading too, but that is a different issue).

Now let's look at what we get for the rest:
#   module C_I :
  sig
    module Dom :
      sig type kind = Doms.IDomain.kind type v = Doms.IDomain.v val z : 
v end
    type coll = Dom.v list
  end

and then a long error message for Test2, which ends with
Modules do not match:
  sig type kind = C_I.Dom.kind type v = Dom.v val z : v end
is not included in
  sig type kind = Sig.domain_is_field type v val z : v end
Type declarations do not match:
  type kind = C_I.Dom.kind
is not included in
  type kind = Sig.domain_is_field

Now, C_I.Dom.kind is actually Sig.domain_is_ring -- why wasn't that 
printed?  That would have been SO much more informative!  In similar 
situations, one can take a long time chasing down why it seems that 
C_I.Dom.kind was somehow abstract when it should have been concrete, and 
so on.

Would it be possible to get some switches to optionally ask for all 
types to be fully expanded?  Also, it would be nice to be able to 
visually distinguish between an abstract type and a concrete but elided 
type even when not asking for types to be expanded.

Note that in other situations (the code is even larger), one can get a 
strange mixture of non-expanded, partially-expanded and fully-expanded 
types all for essentially the same situation, although it seems that 
this latter part may be due to MetaOCaml rather than OCaml.  But it is 
rather difficult to be certain...

Jacques

PS: the work that led up to this email is joint work with Oleg Kiselyov.