Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007348OCamltypingpublic2016-09-09 11:432017-06-12 16:31
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.03.0 
Target Version4.06.0 +dev/beta1/beta2/rc1Fixed in Version4.05.0 +dev/beta1/beta2/beta3/rc1 
Summary0007348: Private row variables can escape their scope
DescriptionThe following functor:

  module F (X : sig type t = private < foo:int; ..> val x : t end) = struct
    let x : < foo: int; ..> = X.x
  end

has a return type that includes the private row variable from X:
    
  module F :
    functor (X : sig type t = private < foo : int; .. > val x : t end) ->
      sig val x : < foo : int; .. > end

This variable remains abstract even when the functor is applied:

  module M = struct
      type t = < foo: int; bar: int>
      let x = object
        method foo = 0
        method bar = 0
      end
   end

  module N = F(M)

which has type:

  module N : sig val x : < foo : int; .. > end

To see that the variable is still abstract:

 # module L : sig val x : < foo : int; bar : int> end = N;;

  Characters 53-54:
    module L : sig val x : < foo : int; bar : int> end = N;;
                                                         ^
  Error: Signature mismatch:
         Modules do not match:
           sig val x : < foo : int; .. > end
         is not included in
           sig val x : < bar : int; foo : int > end
         Values do not match:
           val x : < foo : int; .. >
         is not included in
           val x : < bar : int; foo : int >

  # let x : < foo : int; bar : int> = N.x;;
  Characters 34-37:
    let x : < foo : int; bar : int> = N.x;;
                                      ^^^
  Error: This expression has type < foo : int; .. >
         but an expression was expected of type < bar : int; foo : int >
         The first object type has no method bar

I suspect that the type is called something like X.t#row and is being substituted to M.t#row which does not exist. This could possibly be
a soundness bug since different functors would produce the same
M.t#row even though they would be different types.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0016280)
garrigue (manager)
2016-09-10 03:01

The bug was introduced between 3.12 and 4.04, probably with the introduction of GADTs.
I will look into that.
(0017871)
garrigue (manager)
2017-06-12 11:11

Indeed the code for abstract rows assumes that they are never visible outside of their scope.
This should be true, as an abstract row can only belong to one type, but the above code reveals an expanded form.
I hope to be able to solve this through the name abbreviation mechanism, but leave it alone for now.
(0017873)
garrigue (manager)
2017-06-12 11:54

Note: printing the internal types show that the path of the (inexistent) row is correctly propagated, so at least there does not seem to be a soundness problem.
(0017874)
garrigue (manager)
2017-06-12 16:31

Fixed in 4.05 and trunk by commits 42fb9ffc0 and 02c4df6de.

Exploit the fact that inside a module the same type name cannot be used twice, so that the type definition corresponding to a row name is unambiguous.
Ctype.normalize_type fixes printing, Subst,type_expr fixes functor application (both needed).

- Issue History
Date Modified Username Field Change
2016-09-09 11:43 lpw25 New Issue
2016-09-10 03:01 garrigue Note Added: 0016280
2016-09-10 03:01 garrigue Assigned To => garrigue
2016-09-10 03:01 garrigue Status new => confirmed
2016-09-10 03:02 garrigue Target Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-06-12 11:08 garrigue Target Version 4.05.0 +dev/beta1/beta2/beta3/rc1 => 4.06.0 +dev/beta1/beta2/rc1
2017-06-12 11:11 garrigue Note Added: 0017871
2017-06-12 11:54 garrigue Note Added: 0017873
2017-06-12 16:31 garrigue Note Added: 0017874
2017-06-12 16:31 garrigue Status confirmed => resolved
2017-06-12 16:31 garrigue Fixed in Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2017-06-12 16:31 garrigue Resolution open => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker