Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007800OCamltypingpublic2018-06-01 12:312018-06-11 03:17
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0007800: Type constructors observably change sharing of types
DescriptionThe following code type checks without issue:

    type 'a ty = Int : int ty | Float : float ty

    type 'a pair = 'a * 'a

    let iter_fst_return_snd f (x, y) = f x; y

    let ints : int * int = 1, 2

    let foo (type a) (t : a ty) (x : a) (p : bool) =
      match t with
      | Int ->
          iter_fst_return_snd
            (fun y -> print_int (if p then x else y))
            ints
      | Float -> 0

However, if the type annotation on `ints` is changed from `int * int` to `int pair` then we get an error:

    let ints : int pair = 1, 2

    let foo (type a) (t : a ty) (x : a) (p : bool) =
      match t with
      | Int ->
          iter_fst_return_snd
            (fun y -> print_int (if p then x else y))
            ints
      | Float -> 0

File "sharing.ml", line 22, characters 6-88:
Error: This expression has type a = int
       but an expression was expected of type 'a
       This instance of int is ambiguous:
       it would escape the scope of its equation

Since these two types are equal this obviously shouldn't happen, and it is also easy to show that this is not principal.

The underlying issue is that when we instantiate the type `int pair` we only create a single copy of the `int` types, and so the expansion to `int * int` shares the same type for both `int`s. Even though `int` is "structure" (i.e. not a variable) it is still a mutable piece of state due to its level and scope. So anything which depends on these pieces of state (e.g. GADT ambiguity detection) is affected by the difference in sharing.

This is a fairly fundamental issue. Much like 0007636 the theoretical fix is just to always expand out aliases, but obviously we don't want to do that. An alternative would be to delay instantiation of type constructor parameters until after expansion. I think this is a viable fix and may even improve performance on average by avoiding unnecessary instantiation.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019152)
stedolan (developer)
2018-06-01 13:10

Wow, this looks tricky. Here's a slightly simpler (but essentially the same) example that I found helpful in trying to understand the problem:

    let inc : int -> int = (+) 1
    type 'a is_int = Int : int is_int
    let foo (type a) (Int : a is_int) (x : a) = inc x

This typechecks, but it breaks if inc is redefined as follows:

    type 'a fn = 'a -> 'a
    let inc : int fn = (+) 1
(0019153)
garrigue (manager)
2018-06-01 16:03

Indeed, interactions between sharing and type abbreviations are an open issue since the introduction of polymorphic methods (more than 15 years ago), and I have no good solution.
In practice, I don't think that the impact is that big.

By the way, the problem is actually the other way round: the specification says that if a type is shared then the levels should go down simultaneously, so what you describe is actually the correct behavior.
However, if you unify a type containing some sharing with a type abbreviation where the types are not shared, you might undo the sharing, which in theory should never happen through unification.
(0019154)
garrigue (manager)
2018-06-01 16:06

To make it clearer, the behavior of the compiler here is the correct one (read the formal specification).
However, there are other issues with sharing, which do not appear in this example.
(0019155)
garrigue (manager)
2018-06-01 16:09

And this is of course principal: if you add typing constraints, you increase the risk of failure.
What is more surprising from the point of view of principality is that adding type annotations could make a program type: this is where the theoretical tricks enter the game.
(0019156)
lpw25 (developer)
2018-06-01 16:42

Just to be clear, the current behaviour is not principal:

  # type 'a ty = Int : int ty | Float : float ty
    type 'a pair = 'a * 'a
    type ints = int * int
    let iter_fst_return_snd f (x, y) = f x; y;;
  type 'a ty = Int : int ty | Float : float ty
  type 'a pair = 'a * 'a
  type ints = int * int
  val iter_fst_return_snd : ('a -> 'b) -> 'a * 'c -> 'c = <fun>

  # let ints1 =
     if true then
       (1, 2 : int pair)
     else
       (1, 2 : ints);;
  val ints1 : int pair = (1, 2)

  # let ints2 =
     if true then
       (1, 2 : ints)
     else
       (1, 2 : int pair);;
  val ints2 : ints = (1, 2)

  # let foo (type a) (t : a ty) (x : a) (p : bool) =
      match t with
      | Int ->
          iter_fst_return_snd
            (fun y -> print_int (if p then x else y))
            ints1
      | Float -> 0;;
  Characters 93-184:
    ..........iter_fst_return_snd
                (fun y -> print_int (if p then x else y))
                ints1
  Error: This expression has type a = int
         but an expression was expected of type 'a
         This instance of int is ambiguous:
         it would escape the scope of its equation

  # let foo (type a) (t : a ty) (x : a) (p : bool) =
      match t with
      | Int ->
          iter_fst_return_snd
            (fun y -> print_int (if p then x else y))
            ints2
      | Float -> 0;;
  val foo : 'a ty -> 'a -> bool -> int = <fun>

but you're saying that the problem should actually be fixed by enforcing the hidden sharing, since that is what the formal specification does (which one by the way? The semi-implicit polymorphism one?).

I would suggest that this just shows that it is a bad formal specification. You have two types which are equal under type equality but which cannot be substituted one for another without breaking typing. The types don't even necessarily print differently! This example is just terrible:

  # type 'a is_int = Int : int is_int
    type ('a, 'b) fn = 'a -> 'b
    type 'a id = 'a -> 'a;;

  type 'a is_int = Int : int is_int
  type ('a, 'b) fn = 'a -> 'b
  type 'a id = 'a -> 'a

  # let inc1 =
      if true then (fun x -> x + 1 : (int, int) fn)
      else (fun x -> x + 1 : int id)
    let inc2 = (fun x -> x + 1 : (int, int) fn);;

  val inc1 : (int, int) fn = <fun>
  val inc2 : (int, int) fn = <fun>

  # let foo (type a) (Int : a is_int) (x : a) = inc1 x;;

  Characters 44-50:
    let foo (type a) (Int : a is_int) (x : a) = inc1 x;;
                                                ^^^^^^
  Error: This expression has type a = int
         but an expression was expected of type 'a
         This instance of int is ambiguous:
         it would escape the scope of its equation

  # let foo (type a) (Int : a is_int) (x : a) = inc2 x;;

  val foo : 'a is_int -> 'a -> int = <fun>
(0019176)
garrigue (manager)
2018-06-10 16:53

This is exactly what I said in my previous answer: a type abbreviation which is not shared inside will hide the sharing, which of course loses the principality of sharing-tracking.
We could try to fix this, but I think we are really talking of a corner case.
(Note that the soundness of GADT inference depends on tracking the exported sharing, so this lack of principality has no effect on it.)

The problem is that the specification was written without considering type abbreviations :-(

Now, if you have a better specification that guarantees principality (at least in theory), then I'm interested.
In the midtime, I think we will keep what we have.

The fact the sharing is not printed is another problem. Printing it by default would confuse people. We could have a switch to do that, if debugging this really becomes a problem.
(0019178)
garrigue (manager)
2018-06-11 03:17

Actually, there is a reasonably simple way to fix the hiding of sharing: in Tconstr, keep the expanded version of the abbreviation, at least until it is fully generalized. It is actually already there, in the memo field (to allow building regular types), but gets erased every time the environment is updated, and also by generalize_structure.

- Issue History
Date Modified Username Field Change
2018-06-01 12:31 lpw25 New Issue
2018-06-01 12:32 lpw25 Description Updated View Revisions
2018-06-01 13:10 stedolan Note Added: 0019152
2018-06-01 16:03 garrigue Note Added: 0019153
2018-06-01 16:06 garrigue Note Added: 0019154
2018-06-01 16:09 garrigue Note Added: 0019155
2018-06-01 16:42 lpw25 Note Added: 0019156
2018-06-10 16:38 garrigue Assigned To => garrigue
2018-06-10 16:38 garrigue Status new => assigned
2018-06-10 16:53 garrigue Note Added: 0019176
2018-06-11 03:17 garrigue Note Added: 0019178


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker