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

Type constructors observably change sharing of types #7800

Open
vicuna opened this issue Jun 1, 2018 · 7 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link

commented Jun 1, 2018

Original bug ID: 7800
Reporter: @lpw25
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2018-06-10T14:38:41Z)
Resolution: open
Priority: normal
Severity: minor
Category: typing
Monitored by: @hhugo @yakobowski

Bug description

The 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 ints. 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 #7636 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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 1, 2018

Comment author: @stedolan

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
@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 1, 2018

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 1, 2018

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 1, 2018

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 1, 2018

Comment author: @lpw25

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>
@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 10, 2018

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 11, 2018

Comment author: @garrigue

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.

@vicuna vicuna added the typing label Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

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.