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

False typing error when using pre-compiled .cmi through -intf-suffix option #7629

Open
vicuna opened this issue Sep 18, 2017 · 8 comments
Open

Comments

@vicuna
Copy link

vicuna commented Sep 18, 2017

Original bug ID: 7629
Reporter: jacquev6
Status: acknowledged (set by @xavierleroy on 2017-09-30T08:40:50Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.02.3
Category: typing
Monitored by: jacquev6 @yakobowski

Bug description

Compiling the attached code in two steps, using -intf-suffix .ml to re-use the .cmi produced in the first step, leads to a false typing error:

Values do not match:
 val g : ([< `Poly of 'b M'.t & 'a M'.t ] as 'a) -> int
is not included in
 val g : ([< `Poly of 'b M'.t & 'a M'.t ] as 'a) -> int

Note that the expected and the actual type for g are exactly the same. And that there is only a .ml file, so there can't be any inconsistency between .ml and .mli file.

The code to exhibit this issue is rather complex: it contains a module alias, a recursive function, and uses a dynamic variant to make a recursive type from a parametric type. I think all are needed to exhibit the issue.

Context:

I was porting some code to jbuilder. After reducing my code to a minimal example, I reported the issue to jbuilder in ocaml/dune#254 and after investigation, Xavier Clerc says it's a compiler issue.

Jbuilder uses -intf-suffix to compile a .ml-only module to native after compiling it byte, in order to to re-use the .cmi file, as explained in this comment: ocaml/dune#254 (comment)

Steps to reproduce

  1. Download test.ml (attached to this Mantis issue)

  2. Create test.cmi:

    ocamlc -c test.ml

  3. Compile:

    ocamlc -intf-suffix .ml test.ml -o test

  4. Observe:

    File "test.ml", line 1:
    Error: The implementation test.ml does not match the interface test.cmi:
           Values do not match:
             val g : ([< `Poly of 'b M'.t & 'a M'.t ] as 'a) -> int
           is not included in
             val g : ([< `Poly of 'b M'.t & 'a M'.t ] as 'a) -> int
           File "test.ml", line 13, characters 8-9: Actual declaration
    

Additional information

Possible workaround:

(suggested by Leo White in this comment: ocaml/dune#254 (comment))

Add a polymorphic type annotation to g:

let rec g : 'a . ([< `Poly of 'a M'.t ] as 'a) -> int =

Versions tested:

Same behavior in 4.02.3 and 4.05.0+flambda, both on Linux and macOS.

File attachments

@vicuna
Copy link
Author

vicuna commented Sep 18, 2017

Comment author: @lpw25

I had a brief look at this and it seemed like it was another failure of reflexivity for type equality with polymorphic variant conjunctions. It seems to rely on both a module alias and a recursive type, so I suspect something around the type expansion code.

@vicuna
Copy link
Author

vicuna commented Feb 19, 2018

Comment author: @Octachron

I found another example of this issue (or something quite similar) using polymorphic variant but neither module aliases nor recursive type:

type 'a one = [`one of 'a]
type 'a two = [`two of 'a]
type 'a three = [`three of 'a]
type ( 'dim, 'res, 'p1 ) cross =
  [< `two of 'res & 'p1 one | `three of 'res &  'p1 three ] as 'dim
type 'dim t
let cross:('dim, 'dim2, _ ) cross t ->
  'dim t -> 'dim2 t = fun _ _ -> assert false
let fn v w = cross v w

@github-actions
Copy link

github-actions bot commented Aug 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 Aug 7, 2020
@Octachron Octachron removed the Stale label Sep 3, 2020
@Octachron
Copy link
Member

The issue still exists, and is exotic enough to warrant being recorded.

@github-actions
Copy link

github-actions bot commented Sep 6, 2021

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 Sep 6, 2021
@gasche
Copy link
Member

gasche commented Sep 6, 2021

I reproduced @Octachron's example in the current trunk, now with a much longer error message.

File "test.ml", line 1:
Error: The implementation test.ml does not match the interface test.cmi: 
       Values do not match:
         val cross :
           ([< `three of 'dim2 & 'b three & 'c three
             | `two of 'dim2 & 'b one & 'c one ]
            as 'a, 'dim2, 'b)
           cross t -> 'a t -> 'dim2 t
       is not included in
         val cross :
           ([< `three of 'dim2 & 'b three & 'c three
             | `two of 'dim2 & 'b one & 'c one ]
            as 'a, 'dim2, 'b)
           cross t -> 'a t -> 'dim2 t
       The type
         ([< `three of 'b & 'c three & 'd three
           | `two of 'b & 'c one & 'd one ]
          as 'a, 'b, 'c)
         cross t -> 'a t -> 'b t
       is not compatible with the type
         ([< `three of 'b & 'f three & 'g three
           | `two of 'b & 'f one & 'g one ]
          as 'e, 'b, 'f)
         cross t -> 'e t -> 'b t
       Type ('a, 'b, 'c) cross = 'a is not compatible with type
         ('e, 'b, 'f) cross = 'e 
       Type 'c one = [ `one of 'c ] is not compatible with type 'b 
       Types for tag `two are incompatible
       File "test.ml", line 7, characters 4-9: Expected declaration
       File "test.ml", line 7, characters 4-9: Actual declaration

@gasche gasche removed the Stale label Sep 6, 2021
@github-actions
Copy link

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.

@Octachron
Copy link
Member

The bug still exists and is still a witness of an exotic type system corner case.

@Octachron Octachron reopened this Oct 21, 2022
@github-actions github-actions bot removed the Stale label Oct 26, 2022
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

3 participants