You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 6348 Reporter:@yallop Assigned to:@garrigue Status: closed (set by @xavierleroy on 2015-12-11T18:26:32Z) Resolution: fixed Priority: normal Severity: feature Fixed in version: 4.02.0+dev Category: typing Monitored by:@hcarty
Bug description
I'm not sure whether this use case is intended to be supported, so I've marked the issue as 'feature'.
It's sometimes useful to make interfaces (cmis) visible only when building a library, excluding them from the installation. The distinction between the build-time interfaces and the installed interfaces makes it possible for the library to use type equalities that are not available to clients. Installing only a subset of the cmi files for a library seems to work pretty well, but sometimes breaks down in some cases involving type refinement and type replication. Here's a working piece of code that involves replicating a GADT definition from the module A in the module B:
$ cat a.mli
type _ t = T : int t
$ cat b.mli
type 'a t = 'a A.t = T : int t
$ cat c.ml
let f : type a. a B.t -> a = fun B.T -> 0
$ ocamlc -c a.mli b.mli c.ml
$
However, if we hide A's interface when compiling C, the type checker doesn't use the replicated GADT for refinement:
$ rm a.cmi
$ ocamlc -c c.ml
File "c.ml", line 1, characters 40-41:
Error: This expression has type int but an expression was expected of type a
$
Of course, refinement starts working again if we remove the type equality from the definition of B.t:
$ sed -i 's!=.*=!=!' b.mli
$ cat b.mli
type 'a t = T : int t
$ ocamlc -c b.mli c.ml
$
It'd be useful to have refinement use whichever definitions are visible, not just the last definition in a chain of replications.
The text was updated successfully, but these errors were encountered:
You are striking a dark corner of the type system: what happens when one removes a .cmi.
There is nothing about that in the specification, but the type checker attempts to handle that case by seeing the absent definition as a row abstract type. Unfortunately, this doesn't keep the invariants of the original definition...
This should be fixed, but this is not so easy, as one would need some kind of back mapping relating expanded types to their original form. This is what is done for the -short-paths option, but this is costly in general.
Looking more carefully, your case is a bit strange, since this is about a GADT value constructor, not a type constructor. I do not see where the information could be lost. Need to investigate.
Without investigating the issue fully, I suspect the problem is that during pattern unification the type is being expanded to the (now abstract) A.t, and so is failing the is_datatype test to check that the type is injective in unify3.
The same issue can happen with open types, since you can have GADT constructors in scope for types which are abstract. I fixed this in my open types patch, and indeed Jeremy's examples compile without error using that patch.
Original bug ID: 6348
Reporter: @yallop
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:26:32Z)
Resolution: fixed
Priority: normal
Severity: feature
Fixed in version: 4.02.0+dev
Category: typing
Monitored by: @hcarty
Bug description
I'm not sure whether this use case is intended to be supported, so I've marked the issue as 'feature'.
It's sometimes useful to make interfaces (cmis) visible only when building a library, excluding them from the installation. The distinction between the build-time interfaces and the installed interfaces makes it possible for the library to use type equalities that are not available to clients. Installing only a subset of the cmi files for a library seems to work pretty well, but sometimes breaks down in some cases involving type refinement and type replication. Here's a working piece of code that involves replicating a GADT definition from the module A in the module B:
$ cat a.mli
type _ t = T : int t
$ cat b.mli
type 'a t = 'a A.t = T : int t
$ cat c.ml
let f : type a. a B.t -> a = fun B.T -> 0
$ ocamlc -c a.mli b.mli c.ml
$
However, if we hide A's interface when compiling C, the type checker doesn't use the replicated GADT for refinement:
$ rm a.cmi
$ ocamlc -c c.ml
File "c.ml", line 1, characters 40-41:
Error: This expression has type int but an expression was expected of type a
$
Of course, refinement starts working again if we remove the type equality from the definition of B.t:
$ sed -i 's!=.*=!=!' b.mli
$ cat b.mli
type 'a t = T : int t
$ ocamlc -c b.mli c.ml
$
It'd be useful to have refinement use whichever definitions are visible, not just the last definition in a chain of replications.
The text was updated successfully, but these errors were encountered: