diff options
| -rw-r--r-- | .depend | 24 | ||||
| -rw-r--r-- | Changes | 13 | ||||
| -rw-r--r-- | VERSION | 2 | ||||
| -rw-r--r-- | dune | 3 | ||||
| -rw-r--r-- | man/ocamlc.m | 2 | ||||
| -rw-r--r-- | ocamltest/dune | 2 | ||||
| -rw-r--r-- | runtime/.depend | 52 | ||||
| -rw-r--r-- | testsuite/tests/typing-implicit_unpack/implicit_unpack.ml | 9 | ||||
| -rw-r--r-- | testsuite/tests/typing-short-paths/pr7543.compilers.reference | 7 | ||||
| -rw-r--r-- | typing/parmatch.mli | 8 | ||||
| -rw-r--r-- | typing/typecore.ml | 353 | ||||
| -rw-r--r-- | typing/typemod.ml | 110 | ||||
| -rw-r--r-- | utils/warnings.ml | 2 |
13 files changed, 403 insertions, 184 deletions
@@ -5613,30 +5613,6 @@ asmcomp/debug/reg_with_debug_info.cmx : \ asmcomp/debug/reg_with_debug_info.cmi : \ asmcomp/reg.cmi \ middle_end/backend_var.cmi -driver/compdynlink.cmi : -driver/compdynlink_common.cmo : \ - driver/compdynlink_types.cmi \ - driver/compdynlink_platform_intf.cmi \ - driver/compdynlink_common.cmi -driver/compdynlink_common.cmx : \ - driver/compdynlink_types.cmx \ - driver/compdynlink_platform_intf.cmx \ - driver/compdynlink_common.cmi -driver/compdynlink_common.cmi : \ - driver/compdynlink_platform_intf.cmi -driver/compdynlink_platform_intf.cmo : \ - driver/compdynlink_types.cmi \ - driver/compdynlink_platform_intf.cmi -driver/compdynlink_platform_intf.cmx : \ - driver/compdynlink_types.cmx \ - driver/compdynlink_platform_intf.cmi -driver/compdynlink_platform_intf.cmi : \ - driver/compdynlink_types.cmi -driver/compdynlink_types.cmo : \ - driver/compdynlink_types.cmi -driver/compdynlink_types.cmx : \ - driver/compdynlink_types.cmi -driver/compdynlink_types.cmi : driver/compenv.cmo : \ utils/warnings.cmi \ utils/profile.cmi \ @@ -99,6 +99,10 @@ Working version (Gabriel Scherer and Florian Angeletti, review by Thomas Refis and Gabriel Scherer) +- #9030: clarify and document the parameter space of type_pat + (Gabriel Scherer and Florian Angeletti and Jacques Garrigue, + review by Florian Angeletti and Thomas Refis) + - #8975: "ocamltests" files are no longer required or used by "ocamltest". Instead, any text file in the testsuite directory containing a valid "TEST" block will be automatically included in the testsuite. @@ -299,6 +303,15 @@ Working version - #8891: Warn about unused functor parameters (Thomas Refis, review by Gabriel Radanne) +- #8903: Improve errors for first-class modules + (Leo White, review by Jacques Garrigue) + +- #9046: disable warning 30 by default + This outdated warning complained on label/constructor name conflicts + within a mutually-recursive type declarations; there is now no need + to complain thanks to type-based disambiguation. + (Gabriel Scherer) + ### Build system: - #8840: use ocaml{c,opt}.opt when available to build internal tools @@ -1,4 +1,4 @@ -4.10.0+multicore+dev0 +4.10.0+multicore+dev1 # The version string is the first line of this file. # It must be in the format described in stdlib/sys.mli @@ -147,7 +147,8 @@ (modules ;; asmcomp/ afl_instrument arch asmgen asmlibrarian asmlink asmpackager branch_relaxation - branch_relaxation_intf cmm cmmgen cmmgen_state coloring comballoc CSE CSEgen + branch_relaxation_intf cmm_helpers cmm cmmgen cmmgen_state coloring comballoc + CSE CSEgen deadcode domainstate emit emitaux interf interval linear linearize linscan liveness mach printcmm printlinear printmach proc reg reload reloadgen schedgen scheduling selectgen selection spacetime_profiling spill split diff --git a/man/ocamlc.m b/man/ocamlc.m index 3fdaf6f1cb..6b8530095a 100644 --- a/man/ocamlc.m +++ b/man/ocamlc.m @@ -1018,7 +1018,7 @@ mentioned here corresponds to the empty set. .IP The default setting is -.BR \-w\ +a\-4\-6\-7\-9\-27\-29\-32..42\-44\-45\-48\-50\-60\-66 . +.BR \-w\ +a\-4\-6\-7\-9\-27\-29\-30\-32..42\-44\-45\-48\-50\-60\-66 . Note that warnings .BR 5 \ and \ 10 are not always triggered, depending on the internals of the type checker. diff --git a/ocamltest/dune b/ocamltest/dune index 9d3361a298..ff6cb83085 100644 --- a/ocamltest/dune +++ b/ocamltest/dune @@ -22,7 +22,7 @@ (rule (targets ocamltest_config.ml) - (deps ../Makefile.config ../Makefile.common Makefile + (deps ../Makefile.config ../Makefile.common ../Makefile.best_binaries Makefile ./ocamltest_config.ml.in ./getocamloptdefaultflags) (action (run make %{targets}))) diff --git a/runtime/.depend b/runtime/.depend index c38fa9b0a0..1143113f8b 100644 --- a/runtime/.depend +++ b/runtime/.depend @@ -104,9 +104,9 @@ extern_b.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/domain.h caml/md5.h caml/reverse.h fail_byt_b.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/byte_domain_state.tbl caml/fail.h caml/io.h \ - caml/platform.h caml/memory.h caml/gc.h caml/major_gc.h \ - caml/minor_gc.h caml/addrmap.h caml/domain.h caml/printexc.h \ + caml/domain_state.tbl caml/byte_domain_state.tbl caml/callback.h \ + caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ + caml/domain.h caml/fail.h caml/io.h caml/platform.h caml/printexc.h \ caml/signals.h caml/fiber.h caml/roots.h fail_nat_b.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ @@ -472,9 +472,9 @@ extern_bd.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/domain.h caml/md5.h caml/reverse.h fail_byt_bd.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/byte_domain_state.tbl caml/fail.h caml/io.h \ - caml/platform.h caml/memory.h caml/gc.h caml/major_gc.h \ - caml/minor_gc.h caml/addrmap.h caml/domain.h caml/printexc.h \ + caml/domain_state.tbl caml/byte_domain_state.tbl caml/callback.h \ + caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ + caml/domain.h caml/fail.h caml/io.h caml/platform.h caml/printexc.h \ caml/signals.h caml/fiber.h caml/roots.h fail_nat_bd.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ @@ -846,9 +846,9 @@ extern_bi.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/domain.h caml/md5.h caml/reverse.h fail_byt_bi.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/byte_domain_state.tbl caml/fail.h caml/io.h \ - caml/platform.h caml/memory.h caml/gc.h caml/major_gc.h \ - caml/minor_gc.h caml/addrmap.h caml/domain.h caml/printexc.h \ + caml/domain_state.tbl caml/byte_domain_state.tbl caml/callback.h \ + caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ + caml/domain.h caml/fail.h caml/io.h caml/platform.h caml/printexc.h \ caml/signals.h caml/fiber.h caml/roots.h fail_nat_bi.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ @@ -1214,9 +1214,9 @@ extern_bpic.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/domain.h caml/md5.h caml/reverse.h fail_byt_bpic.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/byte_domain_state.tbl caml/fail.h caml/io.h \ - caml/platform.h caml/memory.h caml/gc.h caml/major_gc.h \ - caml/minor_gc.h caml/addrmap.h caml/domain.h caml/printexc.h \ + caml/domain_state.tbl caml/byte_domain_state.tbl caml/callback.h \ + caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ + caml/domain.h caml/fail.h caml/io.h caml/platform.h caml/printexc.h \ caml/signals.h caml/fiber.h caml/roots.h fail_nat_bpic.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ @@ -1575,9 +1575,10 @@ extern_n.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/minor_gc.h caml/addrmap.h caml/domain.h caml/md5.h caml/reverse.h fail_byt_n.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ - caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ - caml/domain.h caml/printexc.h caml/signals.h caml/fiber.h caml/roots.h + caml/domain_state.tbl caml/callback.h caml/memory.h caml/gc.h \ + caml/major_gc.h caml/minor_gc.h caml/addrmap.h caml/domain.h \ + caml/fail.h caml/io.h caml/platform.h caml/printexc.h caml/signals.h \ + caml/fiber.h caml/roots.h fail_nat_n.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ @@ -1923,9 +1924,10 @@ extern_nd.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/minor_gc.h caml/addrmap.h caml/domain.h caml/md5.h caml/reverse.h fail_byt_nd.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ - caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ - caml/domain.h caml/printexc.h caml/signals.h caml/fiber.h caml/roots.h + caml/domain_state.tbl caml/callback.h caml/memory.h caml/gc.h \ + caml/major_gc.h caml/minor_gc.h caml/addrmap.h caml/domain.h \ + caml/fail.h caml/io.h caml/platform.h caml/printexc.h caml/signals.h \ + caml/fiber.h caml/roots.h fail_nat_nd.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ @@ -2277,9 +2279,10 @@ extern_ni.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/minor_gc.h caml/addrmap.h caml/domain.h caml/md5.h caml/reverse.h fail_byt_ni.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ - caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ - caml/domain.h caml/printexc.h caml/signals.h caml/fiber.h caml/roots.h + caml/domain_state.tbl caml/callback.h caml/memory.h caml/gc.h \ + caml/major_gc.h caml/minor_gc.h caml/addrmap.h caml/domain.h \ + caml/fail.h caml/io.h caml/platform.h caml/printexc.h caml/signals.h \ + caml/fiber.h caml/roots.h fail_nat_ni.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ @@ -2625,9 +2628,10 @@ extern_npic.$(O): extern.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/minor_gc.h caml/addrmap.h caml/domain.h caml/md5.h caml/reverse.h fail_byt_npic.$(O): fail_byt.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ - caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ - caml/memory.h caml/gc.h caml/major_gc.h caml/minor_gc.h caml/addrmap.h \ - caml/domain.h caml/printexc.h caml/signals.h caml/fiber.h caml/roots.h + caml/domain_state.tbl caml/callback.h caml/memory.h caml/gc.h \ + caml/major_gc.h caml/minor_gc.h caml/addrmap.h caml/domain.h \ + caml/fail.h caml/io.h caml/platform.h caml/printexc.h caml/signals.h \ + caml/fiber.h caml/roots.h fail_nat_npic.$(O): fail_nat.c caml/alloc.h caml/misc.h caml/config.h caml/m.h \ caml/s.h caml/camlatomic.h caml/mlvalues.h caml/domain_state.h \ caml/domain_state.tbl caml/fail.h caml/io.h caml/platform.h \ diff --git a/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml b/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml index 8dbdadbe2e..bd256f2c0b 100644 --- a/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml +++ b/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml @@ -468,7 +468,7 @@ Line 4, characters 10-51: 4 | (module struct type elt = A type t = elt list end : S with type t = _ list) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The type t in this module cannot be exported. - Its type contains local dependencies: %M.elt list + Its type contains local dependencies: elt list |}];; type 'a s = (module S with type t = 'a);; @@ -487,7 +487,7 @@ Line 1, characters 23-44: 1 | let x : 'a s = (module struct type t = A end);; ^^^^^^^^^^^^^^^^^^^^^ Error: The type t in this module cannot be exported. - Its type contains local dependencies: %M.t + Its type contains local dependencies: t |}];; let x : 'a s = (module struct end);; @@ -495,6 +495,7 @@ let x : 'a s = (module struct end);; Line 1, characters 23-33: 1 | let x : 'a s = (module struct end);; ^^^^^^^^^^ -Error: The type t in this module cannot be exported. - Its type contains local dependencies: %M.t +Error: Signature mismatch: + Modules do not match: sig end is not included in S + The type `t' is required but not provided |}];; diff --git a/testsuite/tests/typing-short-paths/pr7543.compilers.reference b/testsuite/tests/typing-short-paths/pr7543.compilers.reference index ee55eef11f..67c42e5c82 100644 --- a/testsuite/tests/typing-short-paths/pr7543.compilers.reference +++ b/testsuite/tests/typing-short-paths/pr7543.compilers.reference @@ -5,13 +5,10 @@ Line 1, characters 19-20: 1 | let () = f (module N);; ^ Error: Signature mismatch: - Modules do not match: - sig type 'a t = 'a end - is not included in - sig type t = N.t end + Modules do not match: sig type 'a t = 'a end is not included in S Type declarations do not match: type 'a t = 'a is not included in - type t = N.t + type t They have different arities. diff --git a/typing/parmatch.mli b/typing/parmatch.mli index 72d2ffe3eb..e7778fdfb8 100644 --- a/typing/parmatch.mli +++ b/typing/parmatch.mli @@ -91,6 +91,14 @@ val ppat_of_type : (string, label_description) Hashtbl.t val pressure_variants: Env.t -> pattern list -> unit + +(** [check_partial pred loc caselist] and [check_unused refute pred caselist] + are called with a function [pred] which will be given counter-example + candidates: they may be partially ill-typed, and have to be type-checked + to extract a valid counter-example. + [pred] returns a valid counter-example or [None]. + [refute] indicates that [check_unused] was called on a refutation clause. + *) val check_partial: ((string, constructor_description) Hashtbl.t -> (string, label_description) Hashtbl.t -> diff --git a/typing/typecore.ml b/typing/typecore.ml index df9a0a66e1..6ff90a7ed2 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -946,28 +946,6 @@ let type_continuation_pat env expected_ty sp = raise (Error_forward (Builtin_attributes.error_of_extension ext)) | _ -> raise (Error (loc, env, Invalid_continuation_pattern)) -(* Remember current state for backtracking. - No variable information, as we only backtrack on - patterns without variables (cf. assert statements). *) -type state = - { snapshot: Btype.snapshot; - levels: Ctype.levels; - env: Env.t; } -let save_state env = - { snapshot = Btype.snapshot (); - levels = Ctype.save_levels (); - env = !env; } -let set_state s env = - Btype.backtrack s.snapshot; - Ctype.set_levels s.levels; - env := s.env - -(* type_pat does not generate local constraints inside or patterns *) -type type_pat_mode = - | Normal - | Inside_or (* inside a non-split or-pattern *) - | Split_or (* always split or-patterns *) - (* "half typed" cases are produced in [type_cases] when we've just typechecked the pattern but haven't type-checked the body yet. At this point we might have added some type equalities to the environment, @@ -1010,13 +988,151 @@ let rec has_literal_pattern p = match p.ppat_desc with | Ppat_or (p, q) -> has_literal_pattern p || has_literal_pattern q -exception Need_backtrack - let check_scope_escape loc env level ty = try Ctype.check_scope_escape env level ty with Unify trace -> raise(Error(loc, env, Pattern_type_clash(trace, None))) +type pattern_checking_mode = + | Normal + (** We are checking user code. *) + | Counter_example of counter_example_checking_info + (** In [Counter_example] mode, we are checking a counter-example + candidate produced by Parmatch. This is a syntactic pattern that + represents a set of values by using or-patterns (p_1 | ... | p_n) + to enumerate all alternatives in the counter-example + search. These or-patterns occur at every choice point, possibly + deep inside the pattern. + + Parmatch does not use type information, so this pattern may + exhibit two issues: + - some parts of the pattern may be ill-typed due to GADTs, and + - some wildcard patterns may not match any values: their type is + empty. + + The aim of [type_pat] in the [Counter_example] mode is to refine + this syntactic pattern into a well-typed pattern, and ensure + that it matches at least one concrete value. + - It filters ill-typed branches of or-patterns. + (see {!splitting_mode} below) + - It tries to check that wildcard patterns are non-empty. + (see {!explosion_fuel}) + *) + +and counter_example_checking_info = { + explosion_fuel: int; + splitting_mode: splitting_mode; + constrs: (string, Types.constructor_description) Hashtbl.t; + labels: (string, Types.label_description) Hashtbl.t; + } +(** + [explosion_fuel] controls the checking of wildcard patterns. We + eliminate potentially-empty wildcard patterns by exploding them + into concrete sub-patterns, for example (K1 _ | K2 _) or + { l1: _; l2: _ }. [explosion_fuel] is the depth limit on wildcard + explosion. Such depth limit is required to avoid non-termination + and compilation-time blowups. + + [splitting_mode] controls the handling of or-patterns. In + [Counter_example] mode, we only need to select one branch that + leads to a well-typed pattern. Checking all branches is expensive, + we use different search strategies (see {!splitting_mode}) to + reduce the number of explored alternatives. + + [constrs] and [labels] contain metadata produced by [Parmatch] to + type-check the given syntactic pattern. [Parmatch] produces + counter-examples by turning typed patterns into + [Parsetree.pattern]. In this process, constructor and label paths + are lost, and are replaced by generated strings. [constrs] and + [labels] map those synthetic names back to the typed descriptions + of the original names. + *) + +(** Due to GADT constraints, an or-pattern produced within + a counter-example may have ill-typed branches. Consider for example + + type _ tag = Int : int tag | Bool : bool tag + + then [Parmatch] will propose the or-pattern [Int | Bool] whenever + a pattern of type [tag] is required to form a counter-example. For + example, a function expects a (int tag option) and only [None] is + handled by the user-written pattern. [Some (Int | Bool)] is not + well-typed in this context, only the sub-pattern [Some Int] is. + In this example, the expected type coming from the context + suffices to know which or-pattern branch must be chosen. + + In the general case, choosing a branch can have non-local effects + on the typability of the term. For example, consider a tuple type + ['a tag * ...'a...], where the first component is a GADT. All + constructor choices for this GADT lead to a well-typed branch in + isolation (['a] is unconstrained), but choosing one of them adds + a constraint on ['a] that may make the other tuple elements + ill-typed. + + In general, after choosing each possible branch of the or-pattern, + [type_pat] has to check the rest of the pattern to tell if this + choice leads to a well-typed term. This may lead to an explosion + of typing/search work -- the rest of the term may in turn contain + alternatives. + + We use careful strategies to try to limit counterexample-checking + time; [splitting_mode] represents those strategies. +*) +and splitting_mode = + | Backtrack_or + (** Always backtrack in or-patterns. + + [Backtrack_or] selects a single alternative from an or-pattern + by using backtracking, trying to choose each branch in turn, and + to complete it into a valid sub-pattern. We call this + "splitting" the or-pattern. + + We use this mode when looking for unused patterns or sub-patterns, + in particular to check a refutation clause (p -> .). + *) + | Refine_or of { inside_nonsplit_or: bool; } + (** Only backtrack when needed. + + [Refine_or] tries another approach for refining or-pattern. + + Instead of always splitting each or-pattern, It first attempts to + find branches that do not introduce new constraints (because they + do not contain GADT constructors). Those branches are such that, + if they fail, all other branches will fail. + + If we find one such branch, we attempt to complete the subpattern + (checking what's outside the or-pattern), ignoring other + branches -- we never consider another branch choice again. If all + branches are constrained, it falls back to splitting the + or-pattern. + + We use this mode when checking exhaustivity of pattern matching. + *) + +(** This exception is only used internally within [type_pat_aux], to jump + back to the parent or-pattern in the [Refine_or] strategy. + + Such a parent exists precisely when [inside_nonsplit_or = true]; + it's an invariant that we always setup an exception handler for + [Need_backtrack] when we set this flag. *) + exception Need_backtrack + +(** Remember current typing state for backtracking. + No variable information, as we only backtrack on + patterns without variables (cf. assert statements). *) +type state = + { snapshot: Btype.snapshot; + levels: Ctype.levels; + env: Env.t; } +let save_state env = + { snapshot = Btype.snapshot (); + levels = Ctype.save_levels (); + env = !env; } +let set_state s env = + Btype.backtrack s.snapshot; + Ctype.set_levels s.levels; + env := s.env + (** Find the first alternative in the tree of or-patterns for which [f] does not raise an error. If all fail, the last error is propagated *) @@ -1027,35 +1143,52 @@ let rec find_valid_alternative f pat = with Error _ -> find_valid_alternative f p2) | _ -> f pat -(* type_pat propagates the expected type as well as maps for - constructors and labels. - Unification may update the typing environment. *) -(* constrs <> None => called from parmatch: backtrack on or-patterns - explode > 0 => explode Ppat_any for gadts *) -(* Need_backtrack exceptions are raised in the [Inside_or] mode to backtrack - to the outermost or-pattern *) -let rec type_pat ?(exception_allowed=false) ~constrs ~labels ~no_existentials - ~mode ~explode ~env sp expected_ty k = +let no_explosion = function + | Normal -> Normal + | Counter_example info -> + Counter_example { info with explosion_fuel = 0 } + +let get_splitting_mode = function + | Normal -> None + | Counter_example {splitting_mode} -> Some splitting_mode + +let enter_nonsplit_or mode = match mode with + | Normal -> Normal + | Counter_example info -> + let splitting_mode = match info.splitting_mode with + | Backtrack_or -> + (* in Backtrack_or mode, or-patterns are always split *) + assert false + | Refine_or _ -> + Refine_or {inside_nonsplit_or = true} + in Counter_example { info with splitting_mode } + +let rec type_pat ?(exception_allowed=false) ~no_existentials ~mode + ~env sp expected_ty k = Builtin_attributes.warning_scope sp.ppat_attributes (fun () -> - type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode - ~explode ~env sp expected_ty k + type_pat_aux ~exception_allowed ~no_existentials ~mode + ~env sp expected_ty k ) -and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode - ~explode ~env sp expected_ty k = - let type_pat ?(exception_allowed=false) ?(constrs=constrs) ?(labels=labels) - ?(mode=mode) ?(explode=explode) ?(env=env) = - type_pat ~exception_allowed ~constrs ~labels ~no_existentials ~mode ~explode - ~env +and type_pat_aux ~exception_allowed ~no_existentials ~mode + ~env sp expected_ty k = + let type_pat ?(exception_allowed=false) ?(mode=mode) ?(env=env) = + type_pat ~exception_allowed ~no_existentials ~mode ~env in let loc = sp.ppat_loc in let rup k x = - if constrs = None then (ignore (rp x)); + if mode = Normal then (ignore (rp x)); unify_pat !env x (instance expected_ty); k x in - let rp k x : pattern = if constrs = None then k (rp x) else k x in + let rp k x : pattern = if mode = Normal then k (rp x) else k x in + let construction_not_used_in_counterexamples = (mode = Normal) in + let must_backtrack_on_gadt = match get_splitting_mode mode with + | None -> false + | Some Backtrack_or -> false + | Some (Refine_or {inside_nonsplit_or}) -> inside_nonsplit_or + in match sp.ppat_desc with Ppat_any -> let k' d = rp k { @@ -1065,22 +1198,27 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode pat_attributes = sp.ppat_attributes; pat_env = !env } in - if explode > 0 then - let (sp, constrs, labels) = - try - Parmatch.ppat_of_type !env expected_ty - with Parmatch.Empty -> raise (Error (loc, !env, Empty_pattern)) - in - if sp.ppat_desc = Parsetree.Ppat_any then k' Tpat_any else - if mode = Inside_or then raise Need_backtrack else - let explode = - match sp.ppat_desc with - Parsetree.Ppat_or _ -> explode - 5 - | _ -> explode - 1 - in - type_pat ~constrs:(Some constrs) ~labels:(Some labels) - ~explode sp expected_ty k - else k' Tpat_any + begin match mode with + | Normal -> k' Tpat_any + | Counter_example {explosion_fuel; _} when explosion_fuel <= 0 -> + k' Tpat_any + | Counter_example ({explosion_fuel; _} as info) -> + begin match Parmatch.ppat_of_type !env expected_ty with + | exception Parmatch.Empty -> raise (Error (loc, !env, Empty_pattern)) + | (sp, constrs, labels) -> + if sp.ppat_desc = Parsetree.Ppat_any then k' Tpat_any else + if must_backtrack_on_gadt then raise Need_backtrack else + let explosion_fuel = + match sp.ppat_desc with + Parsetree.Ppat_or _ -> explosion_fuel - 5 + | _ -> explosion_fuel - 1 + in + let mode = + Counter_example { info with explosion_fuel; constrs; labels } + in + type_pat ~mode sp expected_ty k + end + end | Ppat_var name -> let ty = instance expected_ty in let id = (* PR#7330 *) @@ -1096,7 +1234,7 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode pat_attributes = sp.ppat_attributes; pat_env = !env } | Ppat_unpack name -> - assert (constrs = None); + assert construction_not_used_in_counterexamples; let t = instance expected_ty in begin match name.txt with | None -> @@ -1122,7 +1260,7 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode {ppat_desc=Ppat_var name; ppat_loc=lloc; ppat_attributes = attrs}, ({ptyp_desc=Ptyp_poly _} as sty)) -> (* explicitly polymorphic type *) - assert (constrs = None); + assert construction_not_used_in_counterexamples; let cty, force = Typetexp.transl_simple_type_delayed !env sty in let ty = cty.ctyp_type in unify_pat_types lloc !env ty (instance expected_ty); @@ -1145,7 +1283,7 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode | _ -> assert false end | Ppat_alias(sq, name) -> - assert (constrs = None); + assert construction_not_used_in_counterexamples; type_pat sq expected_ty (fun q -> begin_def (); let ty_var = build_as_type !env q in @@ -1180,7 +1318,7 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode in let p = if c1 <= c2 then loop c1 c2 else loop c2 c1 in let p = {p with ppat_loc=loc} in - type_pat ~explode:0 p expected_ty k + type_pat ~mode:(no_explosion mode) p expected_ty k (* TODO: record 'extra' to remember about interval *) | Ppat_interval _ -> raise (Error (loc, !env, Invalid_interval)) @@ -1208,9 +1346,11 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode with Not_found -> None in let constr = - match lid.txt, constrs with - Longident.Lident s, Some constrs -> - assert (Hashtbl.mem constrs s); Hashtbl.find constrs s + match lid.txt, mode with + | Longident.Lident s, Counter_example {constrs; _} -> + (* assert: cf. {!counter_example_checking_info} documentation *) + assert (Hashtbl.mem constrs s); + Hashtbl.find constrs s | _ -> let candidates = Env.lookup_all_constructors Env.Pattern ~loc:lid.loc lid.txt !env in @@ -1218,8 +1358,8 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode (mk_expected expected_ty) (Constructor.disambiguate Env.Pattern lid !env opath) candidates in - if constr.cstr_generalized && constrs <> None && mode = Inside_or - then raise Need_backtrack; + if constr.cstr_generalized && must_backtrack_on_gadt then + raise Need_backtrack; begin match no_existentials, constr.cstr_existentials with | None, _ | _, [] -> () | Some r, (_ :: _ as exs) -> @@ -1305,7 +1445,8 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode generalize_structure expected_ty; (* PR#7404: allow some_private_tag blindly, as it would not unify with the abstract row variable *) - if l = Parmatch.some_private_tag then assert (constrs <> None) + if l = Parmatch.some_private_tag + then assert (match mode with Normal -> false | Counter_example _ -> true) else unify_pat_types loc !env (newgenty (Tvariant row)) expected_ty; let k arg = rp k { @@ -1356,15 +1497,17 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode pat_attributes = sp.ppat_attributes; pat_env = !env } in - if constrs = None then - k (wrap_disambiguate "This record pattern is expected to have" - (mk_expected expected_ty) - (type_label_a_list ?labels loc false !env type_label_pat opath - lid_sp_list) - (k' (fun x -> x))) - else - type_label_a_list ?labels loc false !env type_label_pat opath - lid_sp_list (k' k) + begin match mode with + | Normal -> + k (wrap_disambiguate "This record pattern is expected to have" + (mk_expected expected_ty) + (type_label_a_list loc false !env type_label_pat opath + lid_sp_list) + (k' (fun x -> x))) + | Counter_example {labels; _} -> + type_label_a_list ~labels loc false !env type_label_pat opath + lid_sp_list (k' k) + end | Ppat_array spl -> let ty_elt = newgenvar() in begin_def (); @@ -1381,12 +1524,17 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode pat_attributes = sp.ppat_attributes; pat_env = !env }) | Ppat_or(sp1, sp2) -> + let may_split, must_split = + match get_splitting_mode mode with + | None -> false, false + | Some Backtrack_or -> true, true + | Some (Refine_or _) -> true, false in let state = save_state env in let split_or sp = - assert (constrs <> None); + assert may_split; let typ pat = type_pat ~exception_allowed pat expected_ty k in find_valid_alternative (fun pat -> set_state state env; typ pat) sp in - if mode = Split_or then split_or sp else begin + if must_split then split_or sp else begin let initial_pattern_variables = !pattern_variables in let initial_module_variables = !module_variables in let equation_level = !gadt_equations_level in @@ -1396,9 +1544,10 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode let lev = get_current_level () in gadt_equations_level := Some lev; let env1 = ref !env in + let inside_or = enter_nonsplit_or mode in let p1 = - try Some (type_pat ~exception_allowed ~mode:Inside_or sp1 expected_ty - ~env:env1 (fun x -> x)) + try Some (type_pat ~exception_allowed ~mode:inside_or + sp1 expected_ty ~env:env1 (fun x -> x)) with Need_backtrack -> None in let p1_variables = !pattern_variables in let p1_module_variables = !module_variables in @@ -1406,8 +1555,8 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode module_variables := initial_module_variables; let env2 = ref !env in let p2 = - try Some (type_pat ~exception_allowed ~mode:Inside_or sp2 expected_ty - ~env:env2 (fun x -> x)) + try Some (type_pat ~exception_allowed ~mode:inside_or + sp2 expected_ty ~env:env2 (fun x -> x)) with Need_backtrack -> None in end_def (); gadt_equations_level := equation_level; @@ -1422,7 +1571,13 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode ) p2_variables; begin match p1, p2 with | None, None -> - if mode = Inside_or then raise Need_backtrack else split_or sp + let inside_nonsplit_or = + match get_splitting_mode mode with + | None | Some Backtrack_or -> false + | Some (Refine_or {inside_nonsplit_or}) -> inside_nonsplit_or in + if inside_nonsplit_or + then raise Need_backtrack + else split_or sp | Some p, None | None, Some p -> rp k p (* no variables in this case *) | Some p1, Some p2 -> let alpha_env = @@ -1441,7 +1596,7 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode let nv = newgenvar () in unify_pat_types loc !env (Predef.type_lazy_t nv) expected_ty; (* do not explode under lazy: PR#7421 *) - type_pat ~explode:0 sp1 nv (fun p1 -> + type_pat ~mode:(no_explosion mode) sp1 nv (fun p1 -> rp k { pat_desc = Tpat_lazy p1; pat_loc = loc; pat_extra=[]; @@ -1507,12 +1662,12 @@ and type_pat_aux ~exception_allowed ~constrs ~labels ~no_existentials ~mode | Ppat_extension ext -> raise (Error_forward (Builtin_attributes.error_of_extension ext)) -let type_pat ?exception_allowed ?no_existentials ?constrs ?labels ?(mode=Normal) - ?(explode=0) ?(lev=get_current_level()) env sp expected_ty = +let type_pat ?exception_allowed ?no_existentials ?(mode=Normal) + ?(lev=get_current_level()) env sp expected_ty = Misc.protect_refs [Misc.R (gadt_equations_level, Some lev)] (fun () -> let r = - type_pat ?exception_allowed ~no_existentials ~constrs ~labels ~mode - ~explode ~env sp expected_ty (fun x -> x) + type_pat ?exception_allowed ~no_existentials ~mode + ~env sp expected_ty (fun x -> x) in iter_pattern (fun p -> p.pat_env <- !env) r; r @@ -1520,15 +1675,20 @@ let type_pat ?exception_allowed ?no_existentials ?constrs ?labels ?(mode=Normal) (* this function is passed to Partial.parmatch to type check gadt nonexhaustiveness *) -let partial_pred ~lev ?mode ?explode env expected_ty constrs labels p = +let partial_pred ~lev ~splitting_mode ?(explode=0) + env expected_ty constrs labels p = let env = ref env in let state = save_state env in + let mode = + Counter_example { + splitting_mode; + explosion_fuel = explode; + constrs; labels; + } in try reset_pattern None true; let typed_p = - Ctype.with_passive_variants - (type_pat ~lev ~constrs ~labels ?mode ?explode env p) - expected_ty + Ctype.with_passive_variants (type_pat ~lev ~mode env p) expected_ty in set_state state env; (* types are invalidated but we don't need them here *) @@ -1539,14 +1699,15 @@ let partial_pred ~lev ?mode ?explode env expected_ty constrs labels p = let check_partial ?(lev=get_current_level ()) env expected_ty loc cases = let explode = match cases with [_] -> 5 | _ -> 0 in + let splitting_mode = Refine_or {inside_nonsplit_or = false} in Parmatch.check_partial - (partial_pred ~lev ~explode env expected_ty) loc cases + (partial_pred ~lev ~splitting_mode ~explode env expected_ty) loc cases let check_unused ?(lev=get_current_level ()) env expected_ty cases = Parmatch.check_unused (fun refute constrs labels spat -> match - partial_pred ~lev ~mode:Split_or ~explode:5 + partial_pred ~lev ~splitting_mode:Backtrack_or ~explode:5 env expected_ty constrs labels spat with Some pat when refute -> diff --git a/typing/typemod.ml b/typing/typemod.ml index 64bcf5fc1d..b1800f1f30 100644 --- a/typing/typemod.ml +++ b/typing/typemod.ml @@ -2485,6 +2485,42 @@ let type_module_type_of env smod = (* For Typecore *) +(* Graft a longident onto a path *) +let rec extend_path path = + fun lid -> + match lid with + | Lident name -> Pdot(path, name) + | Ldot(m, name) -> Pdot(extend_path path m, name) + | Lapply _ -> assert false + +(* Lookup a type's longident within a signature *) +let lookup_type_in_sig sg = + let types, modules = + List.fold_left + (fun acc item -> + match item with + | Sig_type(id, _, _, _) -> + let types, modules = acc in + let types = String.Map.add (Ident.name id) id types in + types, modules + | Sig_module(id, _, _, _, _) -> + let types, modules = acc in + let modules = String.Map.add (Ident.name id) id modules in + types, modules + | _ -> acc) + (String.Map.empty, String.Map.empty) sg + in + let rec module_path = function + | Lident name -> Pident (String.Map.find name modules) + | Ldot(m, name) -> Pdot(module_path m, name) + | Lapply _ -> assert false + in + fun lid -> + match lid with + | Lident name -> Pident (String.Map.find name types) + | Ldot(m, name) -> Pdot(module_path m, name) + | Lapply _ -> assert false + let type_package env m p nl = (* Same as Pexp_letmodule *) (* remember original level *) @@ -2493,40 +2529,62 @@ let type_package env m p nl = let modl = type_module env m in let scope = Ctype.create_scope () in Typetexp.widen context; - let (mp, env) = - match modl.mod_desc with - | Tmod_ident (mp,_) -> (mp, env) - | Tmod_constraint ({mod_desc=Tmod_ident (mp,_)}, _, Tmodtype_implicit, _) - -> (mp, env) (* PR#6982 *) - | _ -> - let (id, new_env) = - Env.enter_module ~scope "%M" Mp_present modl.mod_type env + let nl', tl', env = + match nl with + | [] -> [], [], env + | nl -> + let type_path, env = + match modl.mod_desc with + | Tmod_ident (mp,_) + | Tmod_constraint + ({mod_desc=Tmod_ident (mp,_)}, _, Tmodtype_implicit, _) -> + (* We special case these because interactions between + strengthening of module types and packages can cause + spurious escape errors. See examples from PR#6982 in the + testsuite. This can be removed when such issues are + fixed. *) + extend_path mp, env + | _ -> + let sg = extract_sig_open env modl.mod_loc modl.mod_type in + let sg, env = Env.enter_signature ~scope sg env in + lookup_type_in_sig sg, env in - (Pident id, new_env) - in - let rec mkpath mp = function - | Lident name -> Pdot(mp, name) - | Ldot (m, name) -> Pdot(mkpath mp m, name) - | _ -> assert false + let nl', tl' = + List.fold_right + (fun lid (nl, tl) -> + match type_path lid with + | exception Not_found -> (nl, tl) + | path -> begin + match Env.find_type path env with + | exception Not_found -> (nl, tl) + | decl -> + if decl.type_arity > 0 then begin + (nl, tl) + end else begin + let t = Btype.newgenty (Tconstr (path,[],ref Mnil)) in + (lid :: nl, t :: tl) + end + end) + nl ([], []) + in + nl', tl', env in - let tl' = - List.map - (fun name -> Btype.newgenty (Tconstr (mkpath mp name,[],ref Mnil))) - (* beware of interactions with Printtyp and short-path: - mp.name may have an arity > 0, cf. PR#7534 *) - nl in (* go back to original level *) Ctype.end_def (); - if nl = [] then - (wrap_constraint env true modl (Mty_ident p) Tmodtype_implicit, []) - else let mty = modtype_of_package env modl.mod_loc p nl tl' in + let mty = + if nl = [] then (Mty_ident p) + else modtype_of_package env modl.mod_loc p nl' tl' + in List.iter2 (fun n ty -> try Ctype.unify env ty (Ctype.newvar ()) with Ctype.Unify _ -> - raise (Error(m.pmod_loc, env, Scoping_pack (n,ty)))) - nl tl'; - (wrap_constraint env true modl mty Tmodtype_implicit, tl') + raise (Error(modl.mod_loc, env, Scoping_pack (n,ty)))) + nl' tl'; + let modl = wrap_constraint env true modl mty Tmodtype_implicit in + (* Dropped exports should have produced an error above *) + assert (List.length nl = List.length tl'); + modl, tl' (* Fill in the forward declarations *) diff --git a/utils/warnings.ml b/utils/warnings.ml index 2b335d3c60..9c83485453 100644 --- a/utils/warnings.ml +++ b/utils/warnings.ml @@ -393,7 +393,7 @@ let parse_options errflag s = current := {(!current) with error; active} (* If you change these, don't forget to change them in man/ocamlc.m *) -let defaults_w = "+a-4-6-7-9-27-29-32..42-44-45-48-50-60-66-67";; +let defaults_w = "+a-4-6-7-9-27-29-30-32..42-44-45-48-50-60-66-67";; let defaults_warn_error = "-a+31";; let () = parse_options false defaults_w;; |