Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007833OCamltypingpublic2018-07-28 16:002018-10-03 16:40
Reporterjsimeon 
Assigned To 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSmacOSOS Version
Product Version4.07.0 
Target Version4.07.1+dev/rc1Fixed in Version4.07.1+dev/rc1 
Summary0007833: Type unification failure in large OCaml modules
DescriptionThe type checker fails when compiling a large OCaml file/module. The
failure is dependent on how long the file (how many type declarations
are in the module).

This is a regression in OCaml 4.07.0:

```
bash-3.2$ ~/.opam/4.06.1/bin/ocamlopt -c large.ml
bash-3.2$ ~/.opam/4.06.1/bin/ocamlopt -c larger.ml
bash-3.2$ ~/.opam/4.07.0/bin/ocamlopt -c large.ml
bash-3.2$ ~/.opam/4.07.0/bin/ocamlopt -c larger.ml
File "larger.ml", line 80844, characters 24-58:
Error: Constraints are not satisfied in this type.
       Type constant_config should be an instance of constant_config
```
Files `large.ml` amd `larger.ml` only differ in that some declarations have been removed.

```
bash-3.2$ ls -la *large*.ml
-rw-r--r-- 1 jeromesimeon staff 5707725 Jul 28 09:25 large.ml
-rw-r--r-- 1 jeromesimeon staff 5724307 Jul 28 09:25 larger.ml
bash-3.2$ tail large.ml

let constant_localization _ _ x = x.constant_localization

(** val constant_type :
    foreign_type -> brand_model -> constant_config -> rtype **)

let constant_type _ _ x = x.constant_type

type constants_config = (char list * constant_config) list

bash-3.2$ tail larger.ml

let constant_localization _ _ x = x.constant_localization

(** val constant_type :
    foreign_type -> brand_model -> constant_config -> rtype **)

let constant_type _ _ x = x.constant_type

type constants_config = (char list * constant_config) list
                                     ^^^^^^^^^^^^^^^ Type error here

```
Steps To ReproduceSince this is size-dependent, it's a bit difficult to reproduce. The problem was notice when compiling an OCaml module obtained through extraction from Coq for the qcert project (https://github.com/querycert/qcert [^]).

I attach the `larger.ml` file below.
Additional InformationIn case this is useful, a little bit of investigation and a lot of second guessing:

I'm wondering if this has to do with the notion of `level` in the OCaml types/typechecker.

When instrumenting the `check_constraints_rec` in the `typedecl.ml`
module of type checker
(https://github.com/ocaml/ocaml/blob/4132d38ec5da4874688b957c28d0fcba2e8bbb9e/typing/typedecl.ml#L579 [^]) as follows:
```
      with Ctype.Unify _ -> assert false
      | Not_found -> raise (Error(loc, Unavailable_type_constructor path))
      end;
      begin
        begin match ty.desc with
        | Tconstr (p, _, _) ->
            if ((Printtyp.string_of_path p) = "constant_config")
            then
              begin
                Format.eprintf "TY @[%a@]@." Printtyp.raw_type_expr ty;
                Format.eprintf "TY' @[%a@]@." Printtyp.raw_type_expr ty'
              end;
        | _ -> ()
        end;
        if not (Ctype.matches env ty ty') then
          raise (Error(loc, Constraint_failed (ty, ty')))
      end;
      List.iter (check_constraints_rec env loc visited) args
```
it seems that the Ctype.matches fails when the level gets above the fixed `100000000` constant:

```
bash-3.2$ /usr/local/bin/ocamlopt -version
4.07.0
bash-3.2$ /usr/local/bin/ocamlopt -c large.ml
TY {id=722337;level=100000000;desc=Tconstr(constant_config,[],[])}
TY' {id=722372;level=95814902;desc=Tconstr(constant_config,[],[])}
bash-3.2$ /usr/local/bin/ocamlopt -c larger.ml
TY {id=729061;level=100000000;desc=Tconstr(constant_config,[],[])}
TY' {id=729096;level=100115003;desc=Tconstr(constant_config,[],[])}
File "larger.ml", line 80844, characters 24-58:
Error: Constraints are not satisfied in this type.
       Type constant_config should be an instance of constant_config
```

The same instrumentation in version 4.06.0 of the compiler shows very different levels:
```
bash-3.2$ /usr/local/bin/ocamlopt -version
4.06.0
bash-3.2$ /usr/local/bin/ocamlopt -c large.ml
TY {id=574607;level=100000000;desc=Tconstr(constant_config,[],[])}
TY' {id=574642;level=18593;desc=Tconstr(constant_config,[],[])}
bash-3.2$ /usr/local/bin/ocamlopt -c larger.ml
TY {id=580482;level=100000000;desc=Tconstr(constant_config,[],[])}
TY' {id=580517;level=18724;desc=Tconstr(constant_config,[],[])}
```
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019276)
jsimeon (reporter)
2018-07-28 16:05

I can't actually upload the file due to size limitation in Mantis...
(0019277)
garrigue (manager)
2018-07-29 05:56

With a very large file, it might be a consequence of https://github.com/ocaml/ocaml/pull/1648 [^] (Allow type-based selection of GADTs constructors).
It causes all pattern-matchings to do a two-way synchronization between levels and ids. Levels go down when you leave an expression, but ids never go down, so repeating this a sufficient number of times could cause ids to go over generic_level, which is supposed to never happen...
At least we should check that Ident.currentstamp never goes over generic_level.

Could you put your file somewhere, for us to access?
(0019278)
garrigue (manager)
2018-07-29 06:55

It also seems that the allowed number of existentials was lifted from 1000 to 100_000, which means that 1000 pattern-matchings including any constructor is sufficient to reach generic_level (before it was 100_000 pattern-matchings containing GADT constructors).
(0019283)
jsimeon (reporter)
2018-07-30 16:03

@guarrigue I've placed the files here: https://github.com/querycert/bug0007833 [^]
thanks!
(0019400)
doligez (administrator)
2018-10-03 14:06
edited on: 2018-10-03 14:09

Fixed by GPR#1946 (https://github.com/ocaml/ocaml/pull/1946 [^]) and GPR#1997 (https://github.com/ocaml/ocaml/pull/1997 [^])


- Issue History
Date Modified Username Field Change
2018-07-28 16:00 jsimeon New Issue
2018-07-28 16:05 jsimeon Note Added: 0019276
2018-07-29 05:56 garrigue Note Added: 0019277
2018-07-29 06:55 garrigue Note Added: 0019278
2018-07-29 18:10 xleroy Status new => acknowledged
2018-07-29 18:10 xleroy Target Version => 4.07.1+dev/rc1
2018-07-30 16:03 jsimeon Note Added: 0019283
2018-10-03 14:06 doligez Note Added: 0019400
2018-10-03 14:09 doligez Note Edited: 0019400 View Revisions
2018-10-03 16:40 doligez Status acknowledged => resolved
2018-10-03 16:40 doligez Resolution open => fixed
2018-10-03 16:40 doligez Fixed in Version => 4.07.1+dev/rc1


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker