Re: [Caml-list] question on type checking

["Derek Dreyer" <dreyer.publicity@gmail.com>]

This appears to be a bug in the typechecker.  Perhaps a more obvious
instance of the problem is if, after the (top-level) definition of S
in your first example you write:

module T = S
let x = if true then T.A else S.A

This clearly should typecheck, but instead you get the error message:

> This expression has type S.t = F(S.Z).t but is here used with type
>   T.t = F(T.Z).t

Huh?  You mean S.t does not equal T.t when I just defined T = S?

The problem is precisely that the typechecker is not properly
selfifying (strengthening) the signature of S in processing "module T
= S".  When properly selfified, the signature of S (and thus also T)
should be

sig
  module Z : sig end
  module M : sig type t = F(S.Z) = A end
  type t = F(S.Z) = A end
end

but instead of F(S.Z), it's just doing F(Z).  This wouldn't be an
issue if the language tracked structure identities across renamings
(since S.Z and T.Z are clearly the same structure), but it doesn't.

In your second example, this bug didn't pop up because Z was not
named, so M.t could not be characterized precisely through an
applicative functor type of the form F(<something>).t.

In your third example, this bug didn't pop up because you didn't
rename the structure S (and hence tickle the signature strengthening
bug).

I'm guessing this bug should be easy to fix.

Derek

On 3/20/07, Stephen Weeks <sweeks@sweeks.com> wrote:
> Why does one of the programs below fail to type check while the other two minor
> variants succeed?  I would expect all three to succeed.
>
> ----------------------------------------------------------------------
> (* FAILS *)
> module F (Z : sig end) = struct
>  type t = A
> end
>
> module S = struct
>  module Z = struct end
>  module M = F (Z)
>  include M
> end
>
> let f x =
>  let module S = S in
>  match x with
>  | S.A -> ()
> ----------------------------------------------------------------------
> (* WORKS *)
> module F (Z : sig end) = struct
>  type t = A
> end
>
> module S = struct
>  module M = F (struct end)
>  include M
> end
>
> let f x =
>  let module S = S in
>  match x with
>  | S.A -> ()
> ----------------------------------------------------------------------
> (* WORKS *)
> module F (Z : sig end) = struct
>  type t = A
> end
>
> module S = struct
>  module Z = struct end
>  module M = F (Z)
>  include M
> end
>
> let f x =
>  match x with
>  | S.A -> ()
> ----------------------------------------------------------------------
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>