You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
(
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,[],[])}
The text was updated successfully, but these errors were encountered:
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?
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).
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:
Files
large.ml
amdlarger.ml
only differ in that some declarations have been removed.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 thetypedecl.ml
module of type checker
(
ocaml/typing/typedecl.ml
Line 579 in 4132d38
it seems that the Ctype.matches fails when the level gets above the fixed
100000000
constant:The same instrumentation in version 4.06.0 of the compiler shows very different levels:
The text was updated successfully, but these errors were encountered: