Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Consider replication definitions when refining types #6348

Closed
vicuna opened this issue Mar 18, 2014 · 4 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link

commented Mar 18, 2014

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Mar 19, 2014

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Mar 19, 2014

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Mar 19, 2014

Comment author: @lpw25

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 4, 2014

Comment author: @garrigue

Fixed in trunk at revision 14528.

Be more careful when checking for datatypes.
(Thanks lpw25 for pinpointing the cause)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.