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 unification failure in large OCaml modules #7833

Closed
vicuna opened this issue Jul 28, 2018 · 5 comments
Closed

Type unification failure in large OCaml modules #7833

vicuna opened this issue Jul 28, 2018 · 5 comments
Milestone

Comments

@vicuna
Copy link

vicuna commented Jul 28, 2018

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
(

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

vicuna commented Jul 28, 2018

Comment author: jsimeon

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

@vicuna
Copy link
Author

vicuna commented Jul 29, 2018

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

vicuna commented Jul 29, 2018

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

vicuna commented Jul 30, 2018

Comment author: jsimeon

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

@vicuna
Copy link
Author

vicuna commented Oct 3, 2018

Comment author: @damiendoligez

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

@vicuna vicuna closed this as completed Oct 3, 2018
@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.07.1 milestone Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
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

1 participant