|Anonymous | Login | Signup for a new account||2019-02-24 01:40 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006348||OCaml||typing||public||2014-03-18 12:28||2015-12-11 19:26|
|Target Version||Fixed in Version||4.02.0+dev|
|Summary||0006348: Consider replication definitions when refining types|
|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.
|Tags||No tags attached.|
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.|
edited on: 2014-03-19 10:17
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.
Fixed in trunk at revision 14528.
Be more careful when checking for datatypes.
(Thanks lpw25 for pinpointing the cause)
|2014-03-18 12:28||yallop||New Issue|
|2014-03-19 02:55||garrigue||Note Added: 0011054|
|2014-03-19 02:55||garrigue||Assigned To||=> garrigue|
|2014-03-19 02:55||garrigue||Status||new => confirmed|
|2014-03-19 03:34||garrigue||Note Added: 0011055|
|2014-03-19 10:16||lpw25||Note Added: 0011056|
|2014-03-19 10:17||lpw25||Note Edited: 0011056||View Revisions|
|2014-04-04 06:18||garrigue||Note Added: 0011221|
|2014-04-04 06:18||garrigue||Status||confirmed => resolved|
|2014-04-04 06:18||garrigue||Fixed in Version||=> 4.02.0+dev|
|2014-04-04 06:18||garrigue||Resolution||open => fixed|
|2015-12-11 19:26||xleroy||Status||resolved => closed|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|Copyright © 2000 - 2011 MantisBT Group|