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

Ambiguous type escaping its scope #8862

Closed
lpw25 opened this issue Aug 6, 2019 · 1 comment

Comments

@lpw25
Copy link
Contributor

commented Aug 6, 2019

The following example is ambiguous but does not error:

# type (_, _) eq = Refl : ('a, 'a) eq;;
type (_, _) eq = Refl : ('a, 'a) eq

# module T : sig
    type t
    type s
    val eq : (t, s) eq
  end = struct
    type t = int
    type s = int
    let eq = Refl
  end;;
module T : sig type t type s val eq : (t, s) eq end

# module M = struct let r = ref [] end;;
module M : sig val r : '_weak5 list ref end

# let foo p (e : (T.t, T.s) eq) (x : T.t) (y : T.s) =
    match e with
    | Refl ->
        let z = if p then x else y in
        let module N = struct
          module type S = module type of struct let r = ref [z] end
        end in
        let module O : N.S = M in
        ();;
val foo : bool -> (T.t, T.s) eq -> T.t -> T.s -> unit = <fun>

# #show M;;
module M : sig val r : T.s list ref end

If you reverse the order of the types in the equality then the ambiguity resolves the other way:

# module M = struct let r = ref [] end;;
module M : sig val r : '_weak9 list ref end
# let foo p (e : (T.s, T.t) eq) (x : T.t) (y : T.s) =
    match e with
    | Refl ->
        let z = if p then y else x in
        let module N = struct
          module type S = module type of struct let r = ref [z] end
        end in
        let module O : N.S = M in
        ();;
val foo : bool -> (T.s, T.t) eq -> T.t -> T.s -> unit = <fun>

# #show M;;
module M : sig val r : T.t list ref end

@trefis is already having a look at this.

@trefis

This comment has been minimized.

Copy link
Contributor

commented Aug 6, 2019

I believe that subst is losing some scopes, indeed if you apply the following patch:

diff --git a/typing/subst.ml b/typing/subst.ml
index e1643eced..fd790f669 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -172,7 +172,11 @@ let rec typexp copy_scope s ty =
     let has_fixed_row =
       not (is_Tconstr ty) && is_constr_row ~allow_ident:false tm in
     (* Make a stub *)
-    let ty' = if s.for_saving then newpersty (Tvar None) else newgenvar () in
+    let ty' =
+      if s.for_saving
+      then newpersty (Tvar None)
+      else { (newgenvar ()) with scope = ty.scope }
+    in
     ty.desc <- Tsubst ty';
     ty'.desc <-
       begin if has_fixed_row then

Then the example is rejected with:

Line 8, characters 29-30:
8 |         let module O : N.S = M in
                                 ^
Error: Signature mismatch:
       Modules do not match:
         sig val r : '_weak1 list ref end
       is not included in
         N.S
       Values do not match:
         val r : '_weak1 list ref
       is not included in
         val r : T.s list ref

I'll give it a deeper look in the next few days, to see if it is indeed the right way to fix this, and to check whether there are other places in subst that might be problematic.

trefis added a commit to trefis/ocaml that referenced this issue Aug 13, 2019

@trefis trefis closed this in f532be5 Aug 16, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.