Type unification failure in large OCaml modules

[vicuna]

Original bug ID: 7833
Reporter: jsimeon
Status: resolved (set by @damiendoligez on 2018-10-03T14:40:00Z)
Resolution: fixed
Priority: normal
Severity: major
OS: macOS
Version: 4.07.0
Target version: 4.07.1+dev/rc1
Fixed in version: 4.07.1+dev/rc1
Category: typing
Monitored by: @nojb @gasche bacam

Bug description

The 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 reproduce

Since 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 information

In 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
(

ocaml/typing/typedecl.ml

Line 579 in 4132d38

let rec check_constraints_rec env loc visited ty =

) 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,[],[])}

[vicuna]

Comment author: jsimeon

I can't actually upload the file due to size limitation in Mantis...

[vicuna]

Comment author: @garrigue

With a very large file, it might be a consequence of #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?

[vicuna]

Comment author: @garrigue

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

[vicuna]

Comment author: jsimeon

@guarrigue I've placed the files here: https://github.com/querycert/bug0007833
thanks!

[vicuna]

Comment author: @damiendoligez

Fixed by #1946 (#1946) and #1997 (#1997)