Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006348OCamlOCaml typingpublic2014-03-18 12:282014-04-04 06:18
Reporteryallop 
Assigned Togarrigue 
PrioritynormalSeverityfeatureReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.02.0+dev 
Summary0006348: Consider replication definitions when refining types
DescriptionI'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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0011054)
garrigue (manager)
2014-03-19 02:55

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.
(0011055)
garrigue (manager)
2014-03-19 03:34

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.
(0011056)
lpw25 (developer)
2014-03-19 10:16
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.

(0011221)
garrigue (manager)
2014-04-04 06:18

Fixed in trunk at revision 14528.

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

- Issue History
Date Modified Username Field Change
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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker