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

Closed
vicuna opened this issue Jun 1, 2018 · 10 comments
Closed

Type constructors observably change sharing of types #7800

vicuna opened this issue Jun 1, 2018 · 10 comments
Assignees

Comments

@vicuna
Copy link

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

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

@github-actions
Copy link

github-actions bot commented May 7, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 7, 2020
@lpw25
Copy link
Contributor

lpw25 commented May 7, 2020

I'm not sure what to do with issues like this. The problem still exists but we're not going to fix it with the current type checker implementation. However, we'd probably want to look at it as part of the "high road" work on a new type checker implementation.

@xavierleroy
Copy link
Contributor

The problem still exists but we're not going to fix it with the current type checker implementation

Then I'm taking the liberty to close. The resolution is too far in the future.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants