diff options
author | Tom Kelly <ctk21@cl.cam.ac.uk> | 2021-10-01 12:19:35 +0100 |
---|---|---|
committer | Tom Kelly <ctk21@cl.cam.ac.uk> | 2021-10-01 12:19:35 +0100 |
commit | d85f4d8efd39ca4094930c179d233dbf85f44451 (patch) | |
tree | 6ce479f7abd09db85412345a467da95e01b4089d | |
parent | ec296cb5f2d62b56c73197d71e60ec7850363bba (diff) | |
parent | 099b86a046e304fe15e2bb37557bffc6aafaab15 (diff) | |
download | ocaml-d85f4d8efd39ca4094930c179d233dbf85f44451.tar.gz |
Merge commit '099b86a046e304fe15e2bb37557bffc6aafaab15' into parallel_minor_gc_4_13
87 files changed, 3766 insertions, 1291 deletions
@@ -506,6 +506,7 @@ typing/ctype.cmo : \ parsing/location.cmi \ utils/local_store.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ utils/clflags.cmi \ typing/btype.cmi \ @@ -522,6 +523,7 @@ typing/ctype.cmx : \ parsing/location.cmx \ utils/local_store.cmx \ typing/ident.cmx \ + typing/errortrace.cmx \ typing/env.cmx \ utils/clflags.cmx \ typing/btype.cmx \ @@ -534,6 +536,7 @@ typing/ctype.cmi : \ parsing/longident.cmi \ parsing/location.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ parsing/asttypes.cmi typing/datarepr.cmo : \ @@ -632,6 +635,20 @@ typing/envaux.cmi : \ typing/subst.cmi \ typing/path.cmi \ typing/env.cmi +typing/errortrace.cmo : \ + typing/types.cmi \ + typing/path.cmi \ + parsing/asttypes.cmi \ + typing/errortrace.cmi +typing/errortrace.cmx : \ + typing/types.cmx \ + typing/path.cmx \ + parsing/asttypes.cmi \ + typing/errortrace.cmi +typing/errortrace.cmi : \ + typing/types.cmi \ + typing/path.cmi \ + parsing/asttypes.cmi typing/ident.cmo : \ utils/misc.cmi \ utils/local_store.cmi \ @@ -670,8 +687,10 @@ typing/includecore.cmo : \ typing/typedtree.cmi \ typing/type_immediacy.cmi \ typing/printtyp.cmi \ + typing/primitive.cmi \ typing/path.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ typing/ctype.cmi \ parsing/builtin_attributes.cmi \ @@ -683,8 +702,10 @@ typing/includecore.cmx : \ typing/typedtree.cmx \ typing/type_immediacy.cmx \ typing/printtyp.cmx \ + typing/primitive.cmx \ typing/path.cmx \ typing/ident.cmx \ + typing/errortrace.cmx \ typing/env.cmx \ typing/ctype.cmx \ parsing/builtin_attributes.cmx \ @@ -698,8 +719,8 @@ typing/includecore.cmi : \ typing/path.cmi \ parsing/location.cmi \ typing/ident.cmi \ - typing/env.cmi \ - typing/ctype.cmi + typing/errortrace.cmi \ + typing/env.cmi typing/includemod.cmo : \ typing/types.cmi \ typing/typedtree.cmi \ @@ -1024,6 +1045,7 @@ typing/printtyp.cmo : \ parsing/longident.cmi \ parsing/location.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ typing/ctype.cmi \ utils/clflags.cmi \ @@ -1044,6 +1066,7 @@ typing/printtyp.cmx : \ parsing/longident.cmx \ parsing/location.cmx \ typing/ident.cmx \ + typing/errortrace.cmx \ typing/env.cmx \ typing/ctype.cmx \ utils/clflags.cmx \ @@ -1057,8 +1080,8 @@ typing/printtyp.cmi : \ parsing/longident.cmi \ parsing/location.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ - typing/ctype.cmi \ parsing/asttypes.cmi typing/printtyped.cmo : \ typing/types.cmi \ @@ -1211,6 +1234,7 @@ typing/typeclass.cmo : \ parsing/location.cmi \ typing/includeclass.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ typing/ctype.cmi \ file_formats/cmt_format.cmi \ @@ -1238,6 +1262,7 @@ typing/typeclass.cmx : \ parsing/location.cmx \ typing/includeclass.cmx \ typing/ident.cmx \ + typing/errortrace.cmx \ typing/env.cmx \ typing/ctype.cmx \ file_formats/cmt_format.cmx \ @@ -1254,6 +1279,7 @@ typing/typeclass.cmi : \ parsing/longident.cmi \ parsing/location.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ typing/ctype.cmi \ parsing/asttypes.cmi @@ -1278,6 +1304,7 @@ typing/typecore.cmo : \ parsing/longident.cmi \ parsing/location.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ typing/ctype.cmi \ file_formats/cmt_format.cmi \ @@ -1308,6 +1335,7 @@ typing/typecore.cmx : \ parsing/longident.cmx \ parsing/location.cmx \ typing/ident.cmx \ + typing/errortrace.cmx \ typing/env.cmx \ typing/ctype.cmx \ file_formats/cmt_format.cmx \ @@ -1325,8 +1353,8 @@ typing/typecore.cmi : \ parsing/longident.cmi \ parsing/location.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ - typing/ctype.cmi \ parsing/asttypes.cmi typing/typedecl.cmo : \ utils/warnings.cmi \ @@ -1351,6 +1379,7 @@ typing/typedecl.cmo : \ parsing/location.cmi \ typing/includecore.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ typing/ctype.cmi \ utils/config.cmi \ @@ -1385,6 +1414,7 @@ typing/typedecl.cmx : \ parsing/location.cmx \ typing/includecore.cmx \ typing/ident.cmx \ + typing/errortrace.cmx \ typing/env.cmx \ typing/ctype.cmx \ utils/config.cmx \ @@ -1408,8 +1438,8 @@ typing/typedecl.cmi : \ parsing/location.cmi \ typing/includecore.cmi \ typing/ident.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ - typing/ctype.cmi \ parsing/asttypes.cmi typing/typedecl_immediacy.cmo : \ typing/types.cmi \ @@ -1712,6 +1742,7 @@ typing/typetexp.cmo : \ utils/misc.cmi \ parsing/longident.cmi \ parsing/location.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ typing/ctype.cmi \ utils/clflags.cmi \ @@ -1732,6 +1763,7 @@ typing/typetexp.cmx : \ utils/misc.cmx \ parsing/longident.cmx \ parsing/location.cmx \ + typing/errortrace.cmx \ typing/env.cmx \ typing/ctype.cmx \ utils/clflags.cmx \ @@ -1747,8 +1779,8 @@ typing/typetexp.cmi : \ parsing/parsetree.cmi \ parsing/longident.cmi \ parsing/location.cmi \ + typing/errortrace.cmi \ typing/env.cmi \ - typing/ctype.cmi \ parsing/asttypes.cmi typing/untypeast.cmo : \ typing/typedtree.cmi \ @@ -2142,6 +2174,7 @@ asmcomp/asmgen.cmo : \ asmcomp/comballoc.cmi \ asmcomp/coloring.cmi \ asmcomp/cmmgen.cmi \ + asmcomp/cmm_invariants.cmi \ asmcomp/cmm_helpers.cmi \ asmcomp/cmm.cmi \ utils/clflags.cmi \ @@ -2184,6 +2217,7 @@ asmcomp/asmgen.cmx : \ asmcomp/comballoc.cmx \ asmcomp/coloring.cmx \ asmcomp/cmmgen.cmx \ + asmcomp/cmm_invariants.cmx \ asmcomp/cmm_helpers.cmx \ asmcomp/cmm.cmx \ utils/clflags.cmx \ @@ -2422,6 +2456,16 @@ asmcomp/cmm_helpers.cmi : \ middle_end/clambda_primitives.cmi \ middle_end/clambda.cmi \ parsing/asttypes.cmi +asmcomp/cmm_invariants.cmo : \ + utils/numbers.cmi \ + asmcomp/cmm.cmi \ + asmcomp/cmm_invariants.cmi +asmcomp/cmm_invariants.cmx : \ + utils/numbers.cmx \ + asmcomp/cmm.cmx \ + asmcomp/cmm_invariants.cmi +asmcomp/cmm_invariants.cmi : \ + asmcomp/cmm.cmi asmcomp/cmmgen.cmo : \ typing/types.cmi \ middle_end/printclambda_primitives.cmi \ diff --git a/.gitattributes b/.gitattributes index fe589028be..1b193afe2b 100644 --- a/.gitattributes +++ b/.gitattributes @@ -72,7 +72,7 @@ tools/mantis2gh_stripped.csv typo.missing-header /.depend.menhir typo.prune # Makefiles may contain tabs -Makefile* typo.tab=may +Makefile* typo.makefile-whitespace=may asmcomp/*/emit.mlp typo.tab=may typo.long-line=may @@ -111,6 +111,11 @@ Working version - #10349: Fix destroyed_at_c_call on RISC-V (Mark Shinwell, review by Nicolás Ojeda Bär) +- #1400: Add an optional invariants check on Cmm, which can be activated + with the -dcmm-invariants flag + (Vincent Laviron, with help from Sebastien Hinderer, review by Stephen Dolan + and David Allsopp) + ### Type system: * #10081: Typecheck `x |> f` and `f @@ x` as `(f x)` @@ -157,6 +162,9 @@ Working version - #882: Add fold_left, fold_right, exists and for_all to String/Bytes (Yotam Barnoy, review by Alain Frisch and Jeremy Yallop) +- #4070, #10398: small optimization of Stdlib.{frexp,modf}. + (Markus Mottl, Nicolás Ojeda Bär, review by Gabriel Scherer) + ### Other libraries: - #10047: Add `Unix.realpath` @@ -329,8 +337,18 @@ Working version - #8936: Per-function environment for Emit (Greta Yorsh, review by Vincent Laviron and Florian Angeletti) +- #10170: Maintain more structural information in type-checking errors + A mostly-internal change that preserves more information in errors + during type checking; most significantly, it split the errors from + unification, moregen, and type equality into three different types. + (Antal Spector-Zabusky and Mekhrubon Tuarev, review by Leo White, + Florian Angeletti, and Jacques Garrigue) + ### Build system: +- #10289: Do not print option documentation in usage messages. + (Pavlo Khrystenko, review by Gabriel Scherer) + - #9191, #10091, #10182: take the LDFLAGS variable into account, except on flexlink-using systems. (Gabriel Scherer, review by Sébastien Hinderer and David Allsopp, @@ -359,6 +377,9 @@ Working version ### Bug fixes: +- #6985, #10385: remove all ghost row types from included modules + (Florian Angeletti, review by Gabriel Scherer) + * #8857, #10220: Don't clobber GetLastError() in caml_leave_blocking_section when the systhreads library is loaded. (David Allsopp, report by Anton Bachin, review by Xavier Leroy) @@ -371,10 +392,6 @@ Working version in presence of a name collision. (Florian Angeletti, report by Thomas Refis, review by Gabriel Scherer) -- #9936: Make sure that `List.([1;2;3])` is printed `[1;2;3]` in the toplevel - by identifying lists by their types. - (Florian Angeletti, review by Gabriel Scherer) - - #10005: Try expanding aliases in Ctype.nondep_type_rec (Stephen Dolan, review by Gabriel Scherer, Leo White and Xavier Leroy) @@ -405,8 +422,9 @@ Working version or record fields in type-directed disambiguation (Florian Angeletti, report by Hongbo Zhang, review by Gabriel Scherer) -- #10277: Need to detect ambiguity recursively inside types - (Jacques Garrigue, review by Thomas Refis and Leo White) +* #10277, #10383: Need to detect ambiguity recursively inside types to + guarantee principality (affects only principal mode) + (Jacques Garrigue, review by Thomas Refis, Leo White and Kate Deplaix) - #10283, #10284: Enforce right-to-left evaluation order for Lstaticraise (Vincent Laviron, report by Github user Ngoguey42, review by Gabriel Scherer) @@ -425,10 +443,12 @@ Working version - #10351: Fix DLL loading with binutils 2.36+ on mingw-w64 (David Allsopp, review by Nicolás Ojeda Bär) -- #10339, #10354: Fix handling of exception-raising specific - operations during spilling. (This bug affects ARM and ARM64.) - In passing, refactor Proc.op_is_pure and Mach.operation_can_raise. - (Xavier Leroy, report by Richard Bornat, review by Stephen Dolan) +- #10339, #10354, #10387: Fix handling of exception-raising specific + operations during spilling and liveness analysis. + (This bug affects ARM and ARM64.) + In passing, refactor Proc.op_is_pure and Mach.operation_can_raise. + (Xavier Leroy, report by Richard Bornat, review by Stephen Dolan + and Mark Shinwell) - #10371: no longer generatd useless `.cds` file when using `-output-complete-exe`. @@ -48,7 +48,7 @@ INCLUDES=-I utils -I parsing -I typing -I bytecomp -I file_formats \ COMPFLAGS=-strict-sequence -principal -absname \ -w +a-4-9-40-41-42-44-45-48-66-70 \ - -warn-error +a \ + -warn-error +a \ -bin-annot -safe-string -strict-formats $(INCLUDES) LINKFLAGS= @@ -852,7 +852,7 @@ parsing/parser.mli: boot/menhir/parser.mli beforedepend:: parsing/camlinternalMenhirLib.ml \ parsing/camlinternalMenhirLib.mli \ - parsing/parser.ml parsing/parser.mli + parsing/parser.ml parsing/parser.mli partialclean:: partialclean-menhir @@ -1109,8 +1109,8 @@ config.status: @echo "- In file README.win32.adoc for Windows systems." @echo "On Unix systems, if you've just unpacked the distribution," @echo "something like" - @echo " ./configure" - @echo " make" - @echo " make install" + @echo " ./configure" + @echo " make" + @echo " make install" @echo "should work." @false diff --git a/Makefile.common b/Makefile.common index 61fd2e93bf..bd99f70dc0 100644 --- a/Makefile.common +++ b/Makefile.common @@ -50,10 +50,12 @@ endif OCAMLRUN ?= $(ROOTDIR)/boot/ocamlrun$(EXE) NEW_OCAMLRUN ?= $(ROOTDIR)/runtime/ocamlrun$(EXE) -# Use boot/ocamlc.opt if available -ifeq (0,$(shell \ +TEST_BOOT_OCAMLC_OPT = $(shell \ test $(ROOTDIR)/boot/ocamlc.opt -nt $(ROOTDIR)/boot/ocamlc; \ - echo $$?)) + echo $$?) + +# Use boot/ocamlc.opt if available +ifeq "$(TEST_BOOT_OCAMLC_OPT)" "0" BOOT_OCAMLC = $(ROOTDIR)/boot/ocamlc.opt else BOOT_OCAMLC = $(OCAMLRUN) $(ROOTDIR)/boot/ocamlc diff --git a/Makefile.config.in b/Makefile.config.in index d386ceb426..590db7d87e 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -239,6 +239,7 @@ HOST=@host@ FLAMBDA=@flambda@ WITH_FLAMBDA_INVARIANTS=@flambda_invariants@ FORCE_INSTRUMENTED_RUNTIME=@force_instrumented_runtime@ +WITH_CMM_INVARIANTS=@cmm_invariants@ FORCE_SAFE_STRING=@force_safe_string@ DEFAULT_SAFE_STRING=@default_safe_string@ WINDOWS_UNICODE=@windows_unicode@ diff --git a/Makefile.dev b/Makefile.dev index 9ad90a572e..1e1eab9ae8 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -27,8 +27,8 @@ build-all-asts: @$(MAKE) --no-print-directory $(AST_FILES) CAMLC_DPARSETREE := \ - $(OCAMLRUN) ./ocamlc -nostdlib -nopervasives \ - -stop-after parsing -dparsetree + $(OCAMLRUN) ./ocamlc -nostdlib -nopervasives \ + -stop-after parsing -dparsetree %.ml.ast: %.ml ocamlc $(CAMLC_DPARSETREE) $< 2> $@ || exit 0 diff --git a/api_docgen/Makefile.docfiles b/api_docgen/Makefile.docfiles index 49e30be58f..d0c7bda7cb 100644 --- a/api_docgen/Makefile.docfiles +++ b/api_docgen/Makefile.docfiles @@ -43,16 +43,16 @@ STDLIB=$(filter-out stdlib__Pervasives, $(STDLIB_MODULES)) stdlib_UNPREFIXED=$(filter-out pervasives, $(STDLIB_MODULE_BASENAMES)) otherlibref= \ - $(str_MLIS:%.mli=%) \ - $(unix_MLIS:%.mli=%) \ - $(dynlink_MLIS:%.mli=%) \ - $(thread_MLIS:%.mli=%) + $(str_MLIS:%.mli=%) \ + $(unix_MLIS:%.mli=%) \ + $(dynlink_MLIS:%.mli=%) \ + $(thread_MLIS:%.mli=%) libref_EXTRA=stdlib__pervasives libref_TEXT=Ocaml_operators Format_tutorial libref_C=$(call capitalize,$(libref) $(libref_EXTRA)) PARSING_MLIS := $(call sort, \ - $(notdir $(wildcard $(ROOTDIR)/parsing/*.mli))\ + $(notdir $(wildcard $(ROOTDIR)/parsing/*.mli))\ ) UTILS_MLIS := $(call sort,$(notdir $(wildcard $(ROOTDIR)/utils/*.mli))) DRIVER_MLIS := pparse.mli diff --git a/api_docgen/ocamldoc/Makefile b/api_docgen/ocamldoc/Makefile index 0ad2b08038..87cd9cdb85 100644 --- a/api_docgen/ocamldoc/Makefile +++ b/api_docgen/ocamldoc/Makefile @@ -27,8 +27,8 @@ texi: build/texi/stdlib.texi DOC_STDLIB_INCLUDES= $(addprefix -I , $(DOC_STDLIB_DIRS)) DOC_ALL_INCLUDES = \ - $(DOC_STDLIB_INCLUDES) \ - $(addprefix -I ,$(DOC_COMPILERLIBS_DIRS)) + $(DOC_STDLIB_INCLUDES) \ + $(addprefix -I ,$(DOC_COMPILERLIBS_DIRS)) libref=$(stdlib_UNPREFIXED) $(otherlibref) diff --git a/api_docgen/odoc/Makefile b/api_docgen/odoc/Makefile index 4693eb2102..5c22a15b46 100644 --- a/api_docgen/odoc/Makefile +++ b/api_docgen/odoc/Makefile @@ -27,13 +27,13 @@ libref = $(STDLIB) $(otherlibref) # odoc needs a "page-" prefix for a mld documentation file define page_name - $(dir $1)page-$(notdir $1) + $(dir $1)page-$(notdir $1) endef define stdlib_prefix - $(if $(filter-out stdlib camlinternal%,$1),\ - Stdlib.$(call capitalize,$1),\ - $(call capitalize, $1)) + $(if $(filter-out stdlib camlinternal%,$1),\ + Stdlib.$(call capitalize,$1),\ + $(call capitalize, $1)) endef # define the right conditional for the manual @@ -86,9 +86,9 @@ build/compilerlibref/%.odoc: %.cmti $(libref:%=build/libref/%.odoc) \ ALL_TEXT = $(libref_TEXT:%=libref/%) $(compilerlibref_TEXT:%=compilerlibref/%) ALL_PAGE_TEXT=$(foreach mld,$(ALL_TEXT),$(call page_name,$(mld))) TARGET_UNITS= \ - $(compilerlibref:%=compilerlibref/%) \ - libref/stdlib $(otherlibref:%=libref/%) \ - $(addprefix libref/,$(filter camlinternal%,$(STDLIB))) + $(compilerlibref:%=compilerlibref/%) \ + libref/stdlib $(otherlibref:%=libref/%) \ + $(addprefix libref/,$(filter camlinternal%,$(STDLIB))) ALL_UNITS = $(compilerlibref:%=compilerlibref/%) $(libref:%=libref/%) ALL_PAGED_DOC = $(TARGET_UNITS) $(ALL_PAGE_TEXT) @@ -96,11 +96,11 @@ ALL_PAGED_DOC = $(TARGET_UNITS) $(ALL_PAGE_TEXT) # Note that we are using a dependency on the whole phase 1 rather than tracking # the individual file dependencies $(ALL_UNITS:%=build/%.odocl):%.odocl:%.odoc \ - | $(ALL_PAGED_DOC:%=build/%.odoc) + | $(ALL_PAGED_DOC:%=build/%.odoc) $(odoc) link -I build/libref -I build/compilerlibref $< $(ALL_PAGE_TEXT:%=build/%.odocl):%.odocl:%.odoc \ - | $(ALL_PAGED_DOC:%=build/%.odoc) + | $(ALL_PAGED_DOC:%=build/%.odoc) $(odoc) link -I build/libref -I build/compilerlibref $< # Rules for all three backends: @@ -134,8 +134,8 @@ $(build/libref.html.stamp build/compilerlibref.html.stamp): # The stdlib index is generated from the list of stdlib modules. stdlib_INDEX=\ - $(foreach m,$(stdlib_UNPREFIXED),$(call stdlib_prefix,$m))\ - $(call capitalize, $(otherlibref)) + $(foreach m,$(stdlib_UNPREFIXED),$(call stdlib_prefix,$m))\ + $(call capitalize, $(otherlibref)) build/libref.mld: echo {0 OCaml standard library} {!modules:$(stdlib_INDEX)} > $@ diff --git a/asmcomp/asmgen.ml b/asmcomp/asmgen.ml index 54f9bf2354..92379799dc 100644 --- a/asmcomp/asmgen.ml +++ b/asmcomp/asmgen.ml @@ -30,6 +30,16 @@ type error = exception Error of error +let cmm_invariants ppf fd_cmm = + let print_fundecl = + if !Clflags.dump_cmm then Printcmm.fundecl + else fun ppf fdecl -> Format.fprintf ppf "%s" fdecl.fun_name + in + if !Clflags.cmm_invariants && Cmm_invariants.run ppf fd_cmm then + Misc.fatal_errorf "Cmm invariants failed on following fundecl:@.%a@." + print_fundecl fd_cmm; + fd_cmm + let liveness phrase = Liveness.fundecl phrase; phrase let dump_if ppf flag message phrase = @@ -127,8 +137,8 @@ let compile_fundecl ~ppf_dump ~funcnames fd_cmm = Proc.init (); Reg.reset(); fd_cmm - ++ Profile.record ~accumulate:true "selection" - (Selection.fundecl ~future_funcnames:funcnames) + ++ Profile.record ~accumulate:true "cmm_invariants" (cmm_invariants ppf_dump) + ++ Profile.record ~accumulate:true "selection" (Selection.fundecl ~future_funcnames:funcnames) ++ pass_dump_if ppf_dump dump_selection "After instruction selection" ++ Profile.record ~accumulate:true "comballoc" Comballoc.fundecl ++ pass_dump_if ppf_dump dump_combine "After allocation combining" diff --git a/asmcomp/cmm_invariants.ml b/asmcomp/cmm_invariants.ml new file mode 100644 index 0000000000..df102df718 --- /dev/null +++ b/asmcomp/cmm_invariants.ml @@ -0,0 +1,180 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Vincent Laviron, OCamlPro *) +(* *) +(* Copyright 2017 OCamlPro SAS *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +[@@@ocaml.warning "-40"] + +module Int = Numbers.Int + +(* Check a number of continuation-related invariants *) + +module Env : sig + type t + + val init : unit -> t + + val handler : t -> cont:int -> arg_num:int -> t + + val jump : t -> cont:int -> arg_num:int -> unit + + val report : Format.formatter -> bool +end = struct + type t = { + bound_handlers : int Int.Map.t; + } + + type error = + | Unbound_handler of { cont: int } + | Multiple_handlers of { cont: int; } + | Wrong_arguments_number of + { cont: int; handler_args: int; jump_args: int; } + + module Error = struct + type t = error + + let compare = Stdlib.compare + end + + module ErrorSet = Set.Make(Error) + + type persistent_state = { + mutable all_handlers : Int.Set.t; + mutable errors : ErrorSet.t; + } + + let state = { + all_handlers = Int.Set.empty; + errors = ErrorSet.empty; + } + + let record_error error = + state.errors <- ErrorSet.add error state.errors + + let unbound_handler cont = + record_error (Unbound_handler { cont; }) + + let multiple_handler cont = + record_error (Multiple_handlers { cont; }) + + let wrong_arguments cont handler_args jump_args = + record_error (Wrong_arguments_number { cont; handler_args; jump_args; }) + + let init () = + state.all_handlers <- Int.Set.empty; + state.errors <- ErrorSet.empty; + { + bound_handlers = Int.Map.empty; + } + + let handler t ~cont ~arg_num = + if Int.Set.mem cont state.all_handlers then multiple_handler cont; + state.all_handlers <- Int.Set.add cont state.all_handlers; + let bound_handlers = Int.Map.add cont arg_num t.bound_handlers in + { bound_handlers; } + + let jump t ~cont ~arg_num = + match Int.Map.find cont t.bound_handlers with + | handler_args -> + if arg_num <> handler_args then + wrong_arguments cont handler_args arg_num + | exception Not_found -> unbound_handler cont + + let print_error ppf error = + match error with + | Unbound_handler { cont } -> + if Int.Set.mem cont state.all_handlers then + Format.fprintf ppf + "Continuation %d was used outside the scope of its handler" + cont + else + Format.fprintf ppf + "Continuation %d was used but never bound" + cont + | Multiple_handlers { cont; } -> + Format.fprintf ppf + "Continuation %d was declared in more than one handler" + cont + | Wrong_arguments_number { cont; handler_args; jump_args } -> + Format.fprintf ppf + "Continuation %d was declared with %d arguments but called with %d" + cont + handler_args + jump_args + + let print_error_newline ppf error = + Format.fprintf ppf "%a@." print_error error + + let report ppf = + if ErrorSet.is_empty state.errors then false + else begin + ErrorSet.iter (fun err -> print_error_newline ppf err) state.errors; + true + end +end + +let rec check env (expr : Cmm.expression) = + match expr with + | Cconst_int _ | Cconst_natint _ | Cconst_float _ | Cconst_symbol _ + | Cvar _ -> + () + | Clet (_, expr, body) + | Clet_mut (_, _, expr, body) -> + check env expr; + check env body + | Cphantom_let (_, _, expr) -> + check env expr + | Cassign (_, expr) -> + check env expr + | Ctuple exprs -> + List.iter (check env) exprs + | Cop (_, args, _) -> + List.iter (check env) args; + | Csequence (expr1, expr2) -> + check env expr1; + check env expr2 + | Cifthenelse (test, _, ifso, _, ifnot, _) -> + check env test; + check env ifso; + check env ifnot + | Cswitch (body, _, branches, _) -> + check env body; + Array.iter (fun (expr, _) -> check env expr) branches + | Ccatch (rec_flag, handlers, body) -> + let env_extended = + List.fold_left + (fun env (cont, args, _, _) -> + Env.handler env ~cont ~arg_num:(List.length args)) + env + handlers + in + check env_extended body; + let env_handler = + match rec_flag with + | Recursive -> env_extended + | Nonrecursive -> env + in + List.iter (fun (_, _, handler, _) -> check env_handler handler) handlers + | Cexit (cont, args) -> + Env.jump env ~cont ~arg_num:(List.length args) + | Ctrywith (body, _, handler, _) -> + (* Jumping from inside a trywith body to outside isn't very nice, + but it's handled correctly by Linearize, as it happens + when compiling match ... with exception ..., for instance, so it is + not reported as an error. *) + check env body; + check env handler + +let run ppf (fundecl : Cmm.fundecl) = + let env = Env.init () in + check env fundecl.fun_body; + Env.report ppf diff --git a/asmcomp/cmm_invariants.mli b/asmcomp/cmm_invariants.mli new file mode 100644 index 0000000000..4d1ffa91a4 --- /dev/null +++ b/asmcomp/cmm_invariants.mli @@ -0,0 +1,36 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Vincent Laviron, OCamlPro *) +(* *) +(* Copyright 2017 OCamlPro SAS *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +(* Check a number of continuation-related invariants *) + +(* Currently, this checks that : + - Every use of a continuation occurs within the scope of its handler + - Exit instructions take the same number of arguments as their handler. + - In every function declaration, a given continuation can only be + declared in a single handler. + + This is intended to document what invariants the backend can rely upon. + The first two would trigger errors later, and the last one, while + harmless for now, is not that hard to ensure, could be useful for + future work on the backend, and helped detect a code duplication bug. + + These invariants are not checked by default, but the check can be turned + on with the -dcmm-invariants compilation flag. +*) + +(** [run ppf fundecl] analyses the given function, and returns whether + any errors were encountered (with corresponding error messages printed + on the given formatter). *) + +val run : Format.formatter -> Cmm.fundecl -> bool diff --git a/asmcomp/liveness.ml b/asmcomp/liveness.ml index cbb93cf3da..b7f549bd7e 100644 --- a/asmcomp/liveness.ml +++ b/asmcomp/liveness.ml @@ -55,18 +55,14 @@ let rec live i finally = end else begin let across_after = Reg.diff_set_array after i.res in let across = - match op with - | Icall_ind | Icall_imm _ | Iextcall _ | Ialloc _ - | Iintop (Icheckbound) | Iintop_imm(Icheckbound, _) -> - (* The function call may raise an exception, branching to the - nearest enclosing try ... with. Similarly for bounds checks - and allocation (for the latter: finalizers may throw - exceptions, as may signal handlers). - Hence, everything that must be live at the beginning of - the exception handler must also be live across this instr. *) - Reg.Set.union across_after !live_at_raise - | _ -> - across_after in + (* Operations that can raise an exception (function calls, + bounds checks, allocations) can branch to the + nearest enclosing try ... with. + Hence, everything that must be live at the beginning of + the exception handler must also be live across this instr. *) + if operation_can_raise op + then Reg.Set.union across_after !live_at_raise + else across_after in i.live <- across; Reg.add_set_array across i.arg end diff --git a/compilerlibs/Makefile.compilerlibs b/compilerlibs/Makefile.compilerlibs index 3630f0ebc3..34e843efec 100644 --- a/compilerlibs/Makefile.compilerlibs +++ b/compilerlibs/Makefile.compilerlibs @@ -24,153 +24,236 @@ # linked in the archive, but they are marked as dependencies to ensure # that they are consistent with the interface digests in the archives. -UTILS=utils/config.cmo utils/build_path_prefix_map.cmo utils/misc.cmo \ - utils/identifiable.cmo utils/numbers.cmo utils/arg_helper.cmo \ - utils/clflags.cmo utils/profile.cmo utils/local_store.cmo \ - utils/load_path.cmo \ - utils/terminfo.cmo utils/ccomp.cmo utils/warnings.cmo \ - utils/consistbl.cmo utils/strongly_connected_components.cmo \ - utils/targetint.cmo utils/int_replace_polymorphic_compare.cmo \ - utils/domainstate.cmo utils/binutils.cmo utils/lazy_backtrack.cmo \ - utils/diffing.cmo -UTILS_CMI= - -PARSING=parsing/location.cmo parsing/longident.cmo \ - parsing/docstrings.cmo parsing/syntaxerr.cmo \ +UTILS = \ + utils/config.cmo \ + utils/build_path_prefix_map.cmo \ + utils/misc.cmo \ + utils/identifiable.cmo \ + utils/numbers.cmo \ + utils/arg_helper.cmo \ + utils/clflags.cmo \ + utils/profile.cmo \ + utils/local_store.cmo \ + utils/load_path.cmo \ + utils/terminfo.cmo \ + utils/ccomp.cmo \ + utils/warnings.cmo \ + utils/consistbl.cmo \ + utils/strongly_connected_components.cmo \ + utils/targetint.cmo \ + utils/int_replace_polymorphic_compare.cmo \ + utils/domainstate.cmo \ + utils/binutils.cmo \ + utils/lazy_backtrack.cmo \ + utils/diffing.cmo +UTILS_CMI = + +PARSING = \ + parsing/location.cmo \ + parsing/longident.cmo \ + parsing/docstrings.cmo \ + parsing/syntaxerr.cmo \ parsing/ast_helper.cmo \ parsing/pprintast.cmo \ - parsing/camlinternalMenhirLib.cmo parsing/parser.cmo \ - parsing/lexer.cmo parsing/parse.cmo parsing/printast.cmo \ - parsing/ast_mapper.cmo parsing/ast_iterator.cmo parsing/attr_helper.cmo \ - parsing/builtin_attributes.cmo parsing/ast_invariants.cmo parsing/depend.cmo -PARSING_CMI=\ + parsing/camlinternalMenhirLib.cmo \ + parsing/parser.cmo \ + parsing/lexer.cmo \ + parsing/parse.cmo \ + parsing/printast.cmo \ + parsing/ast_mapper.cmo \ + parsing/ast_iterator.cmo \ + parsing/attr_helper.cmo \ + parsing/builtin_attributes.cmo \ + parsing/ast_invariants.cmo \ + parsing/depend.cmo +PARSING_CMI = \ parsing/asttypes.cmi \ parsing/parsetree.cmi -TYPING=typing/ident.cmo typing/path.cmo \ - typing/primitive.cmo typing/type_immediacy.cmo typing/types.cmo \ - typing/btype.cmo typing/oprint.cmo \ - typing/subst.cmo typing/predef.cmo \ - typing/datarepr.cmo file_formats/cmi_format.cmo \ - typing/persistent_env.cmo typing/env.cmo \ - typing/typedtree.cmo typing/printtyped.cmo typing/ctype.cmo \ - typing/printtyp.cmo typing/includeclass.cmo \ - typing/mtype.cmo typing/envaux.cmo typing/includecore.cmo \ - typing/tast_iterator.cmo typing/tast_mapper.cmo typing/stypes.cmo \ - file_formats/cmt_format.cmo typing/cmt2annot.cmo typing/untypeast.cmo \ - typing/includemod.cmo typing/includemod_errorprinter.cmo \ - typing/typetexp.cmo typing/printpat.cmo \ - typing/patterns.cmo typing/parmatch.cmo \ - typing/typedecl_properties.cmo typing/typedecl_variance.cmo \ - typing/typedecl_unboxed.cmo typing/typedecl_immediacy.cmo \ +TYPING = \ + typing/ident.cmo \ + typing/path.cmo \ + typing/primitive.cmo \ + typing/type_immediacy.cmo \ + typing/types.cmo \ + typing/btype.cmo \ + typing/oprint.cmo \ + typing/subst.cmo \ + typing/predef.cmo \ + typing/datarepr.cmo \ + file_formats/cmi_format.cmo \ + typing/persistent_env.cmo \ + typing/env.cmo \ + typing/errortrace.cmo \ + typing/typedtree.cmo \ + typing/printtyped.cmo \ + typing/ctype.cmo \ + typing/printtyp.cmo \ + typing/includeclass.cmo \ + typing/mtype.cmo \ + typing/envaux.cmo \ + typing/includecore.cmo \ + typing/tast_iterator.cmo \ + typing/tast_mapper.cmo \ + typing/stypes.cmo \ + file_formats/cmt_format.cmo \ + typing/cmt2annot.cmo \ + typing/untypeast.cmo \ + typing/includemod.cmo \ + typing/includemod_errorprinter.cmo \ + typing/typetexp.cmo \ + typing/printpat.cmo \ + typing/patterns.cmo \ + typing/parmatch.cmo \ + typing/typedecl_properties.cmo \ + typing/typedecl_variance.cmo \ + typing/typedecl_unboxed.cmo \ + typing/typedecl_immediacy.cmo \ typing/typedecl_separability.cmo \ - typing/typedecl.cmo typing/typeopt.cmo \ - typing/rec_check.cmo typing/typecore.cmo typing/typeclass.cmo \ + typing/typedecl.cmo \ + typing/typeopt.cmo \ + typing/rec_check.cmo \ + typing/typecore.cmo \ + typing/typeclass.cmo \ typing/typemod.cmo -TYPING_CMI=\ +TYPING_CMI = \ typing/annot.cmi \ typing/outcometree.cmi -LAMBDA=lambda/debuginfo.cmo \ - lambda/lambda.cmo lambda/printlambda.cmo \ - lambda/switch.cmo lambda/matching.cmo \ - lambda/translobj.cmo lambda/translattribute.cmo \ - lambda/translprim.cmo lambda/translcore.cmo \ - lambda/translclass.cmo lambda/translmod.cmo \ - lambda/simplif.cmo lambda/runtimedef.cmo -LAMBDA_CMI= - -COMP=\ - bytecomp/meta.cmo bytecomp/opcodes.cmo \ - bytecomp/bytesections.cmo bytecomp/dll.cmo \ +LAMBDA = \ + lambda/debuginfo.cmo \ + lambda/lambda.cmo \ + lambda/printlambda.cmo \ + lambda/switch.cmo \ + lambda/matching.cmo \ + lambda/translobj.cmo \ + lambda/translattribute.cmo \ + lambda/translprim.cmo \ + lambda/translcore.cmo \ + lambda/translclass.cmo \ + lambda/translmod.cmo \ + lambda/simplif.cmo \ + lambda/runtimedef.cmo +LAMBDA_CMI = + +COMP = \ + bytecomp/meta.cmo \ + bytecomp/opcodes.cmo \ + bytecomp/bytesections.cmo \ + bytecomp/dll.cmo \ bytecomp/symtable.cmo \ - driver/pparse.cmo driver/compenv.cmo \ - driver/main_args.cmo driver/compmisc.cmo \ + driver/pparse.cmo \ + driver/compenv.cmo \ + driver/main_args.cmo \ + driver/compmisc.cmo \ driver/makedepend.cmo \ driver/compile_common.cmo -COMP_CMI=\ +COMP_CMI = \ file_formats/cmo_format.cmi \ file_formats/cmx_format.cmi \ file_formats/cmxs_format.cmi # All file format descriptions (including cmx{,s}) are in the # ocamlcommon library so that ocamlobjinfo can depend on them. -COMMON_CMI=$(UTILS_CMI) $(PARSING_CMI) $(TYPING_CMI) $(LAMBDA_CMI) $(COMP_CMI) +COMMON_CMI = $(UTILS_CMI) $(PARSING_CMI) $(TYPING_CMI) $(LAMBDA_CMI) $(COMP_CMI) -COMMON=$(UTILS) $(PARSING) $(TYPING) $(LAMBDA) $(COMP) +COMMON = $(UTILS) $(PARSING) $(TYPING) $(LAMBDA) $(COMP) -BYTECOMP=bytecomp/instruct.cmo bytecomp/bytegen.cmo \ - bytecomp/printinstr.cmo bytecomp/emitcode.cmo \ - bytecomp/bytelink.cmo bytecomp/bytelibrarian.cmo bytecomp/bytepackager.cmo \ - driver/errors.cmo driver/compile.cmo driver/maindriver.cmo -BYTECOMP_CMI= +BYTECOMP = \ + bytecomp/instruct.cmo \ + bytecomp/bytegen.cmo \ + bytecomp/printinstr.cmo \ + bytecomp/emitcode.cmo \ + bytecomp/bytelink.cmo \ + bytecomp/bytelibrarian.cmo \ + bytecomp/bytepackager.cmo \ + driver/errors.cmo \ + driver/compile.cmo \ + driver/maindriver.cmo +BYTECOMP_CMI = -INTEL_ASM=\ +INTEL_ASM = \ asmcomp/x86_proc.cmo \ asmcomp/x86_dsl.cmo \ asmcomp/x86_gas.cmo \ asmcomp/x86_masm.cmo -INTEL_ASM_CMI=\ +INTEL_ASM_CMI = \ asmcomp/x86_ast.cmi -ARCH_SPECIFIC_ASMCOMP= -ARCH_SPECIFIC_ASMCOMP_CMI= +ARCH_SPECIFIC_ASMCOMP = +ARCH_SPECIFIC_ASMCOMP_CMI = ifeq ($(ARCH),i386) -ARCH_SPECIFIC_ASMCOMP=$(INTEL_ASM) -ARCH_SPECIFIC_ASMCOMP_CMI=$(INTEL_ASM_CMI) +ARCH_SPECIFIC_ASMCOMP = $(INTEL_ASM) +ARCH_SPECIFIC_ASMCOMP_CMI = $(INTEL_ASM_CMI) endif ifeq ($(ARCH),amd64) -ARCH_SPECIFIC_ASMCOMP=$(INTEL_ASM) -ARCH_SPECIFIC_ASMCOMP_CMI=$(INTEL_ASM_CMI) +ARCH_SPECIFIC_ASMCOMP = $(INTEL_ASM) +ARCH_SPECIFIC_ASMCOMP_CMI = $(INTEL_ASM_CMI) endif -ASMCOMP=\ +ASMCOMP = \ $(ARCH_SPECIFIC_ASMCOMP) \ asmcomp/arch.cmo \ - asmcomp/cmm.cmo asmcomp/printcmm.cmo \ - asmcomp/reg.cmo asmcomp/mach.cmo asmcomp/proc.cmo \ + asmcomp/cmm.cmo \ + asmcomp/printcmm.cmo \ + asmcomp/reg.cmo \ + asmcomp/mach.cmo \ + asmcomp/proc.cmo \ asmcomp/afl_instrument.cmo \ asmcomp/strmatch.cmo \ asmcomp/cmmgen_state.cmo \ asmcomp/cmm_helpers.cmo \ asmcomp/cmmgen.cmo \ + asmcomp/cmm_invariants.cmo \ asmcomp/interval.cmo \ asmcomp/printmach.cmo \ - asmcomp/dataflow.cmo \ asmcomp/polling.cmo \ asmcomp/selectgen.cmo \ asmcomp/selection.cmo \ asmcomp/comballoc.cmo \ - asmcomp/CSEgen.cmo asmcomp/CSE.cmo \ + asmcomp/CSEgen.cmo \ + asmcomp/CSE.cmo \ asmcomp/liveness.cmo \ - asmcomp/spill.cmo asmcomp/split.cmo \ - asmcomp/interf.cmo asmcomp/coloring.cmo \ + asmcomp/spill.cmo \ + asmcomp/split.cmo \ + asmcomp/interf.cmo \ + asmcomp/coloring.cmo \ asmcomp/linscan.cmo \ - asmcomp/reloadgen.cmo asmcomp/reload.cmo \ + asmcomp/reloadgen.cmo \ + asmcomp/reload.cmo \ asmcomp/deadcode.cmo \ - asmcomp/linear.cmo asmcomp/printlinear.cmo asmcomp/linearize.cmo \ + asmcomp/linear.cmo \ + asmcomp/printlinear.cmo \ + asmcomp/linearize.cmo \ file_formats/linear_format.cmo \ - asmcomp/schedgen.cmo asmcomp/scheduling.cmo \ + asmcomp/schedgen.cmo \ + asmcomp/scheduling.cmo \ asmcomp/branch_relaxation_intf.cmo \ asmcomp/branch_relaxation.cmo \ - asmcomp/emitaux.cmo asmcomp/emit.cmo asmcomp/asmgen.cmo \ - asmcomp/asmlink.cmo asmcomp/asmlibrarian.cmo asmcomp/asmpackager.cmo \ - driver/opterrors.cmo driver/optcompile.cmo driver/optmaindriver.cmo -ASMCOMP_CMI=$(ARCH_SPECIFIC_ASMCOMP_CMI) + asmcomp/emitaux.cmo \ + asmcomp/emit.cmo \ + asmcomp/asmgen.cmo \ + asmcomp/asmlink.cmo \ + asmcomp/asmlibrarian.cmo \ + asmcomp/asmpackager.cmo \ + driver/opterrors.cmo \ + driver/optcompile.cmo \ + driver/optmaindriver.cmo +ASMCOMP_CMI = $(ARCH_SPECIFIC_ASMCOMP_CMI) # Files under middle_end/ are not to reference files under asmcomp/. # This ensures that the middle end can be linked (e.g. for objinfo) even when # the native code compiler is not present for some particular target. -MIDDLE_END_CLOSURE=\ +MIDDLE_END_CLOSURE = \ middle_end/closure/closure.cmo \ middle_end/closure/closure_middle_end.cmo -MIDDLE_END_CLOSURE_CMI= +MIDDLE_END_CLOSURE_CMI = # Owing to dependencies through [Compilenv], which would be # difficult to remove, some of the lower parts of Flambda (anything that is # saved in a .cmx file) have to be included in the [MIDDLE_END] stanza, below. -MIDDLE_END_FLAMBDA=\ +MIDDLE_END_FLAMBDA = \ middle_end/flambda/import_approx.cmo \ middle_end/flambda/lift_code.cmo \ middle_end/flambda/closure_conversion_aux.cmo \ @@ -209,11 +292,11 @@ MIDDLE_END_FLAMBDA=\ middle_end/flambda/un_anf.cmo \ middle_end/flambda/flambda_to_clambda.cmo \ middle_end/flambda/flambda_middle_end.cmo -MIDDLE_END_FLAMBDA_CMI=\ +MIDDLE_END_FLAMBDA_CMI = \ middle_end/flambda/inlining_decision_intf.cmi \ middle_end/flambda/simplify_boxed_integer_ops_intf.cmi -MIDDLE_END=\ +MIDDLE_END = \ middle_end/internal_variable_names.cmo \ middle_end/linkage_name.cmo \ middle_end/compilation_unit.cmo \ @@ -253,26 +336,44 @@ MIDDLE_END=\ middle_end/compilenv.cmo \ $(MIDDLE_END_CLOSURE) \ $(MIDDLE_END_FLAMBDA) -MIDDLE_END_CMI=\ +MIDDLE_END_CMI = \ middle_end/backend_intf.cmi \ $(MIDDLE_END_CLOSURE_CMI) \ $(MIDDLE_END_FLAMBDA_CMI) -OPTCOMP=$(MIDDLE_END) $(ASMCOMP) -OPTCOMP_CMI=$(MIDDLE_END_CMI) $(ASMCOMP_CMI) - -TOPLEVEL=toplevel/genprintval.cmo toplevel/topcommon.cmo \ - toplevel/byte/topeval.cmo toplevel/byte/trace.cmo toplevel/toploop.cmo \ - toplevel/topdirs.cmo toplevel/byte/topmain.cmo -TOPLEVEL_CMI=toplevel/topcommon.cmi toplevel/byte/topeval.cmi \ - toplevel/byte/trace.cmi toplevel/toploop.cmi toplevel/topdirs.cmi \ +OPTCOMP = $(MIDDLE_END) $(ASMCOMP) +OPTCOMP_CMI = $(MIDDLE_END_CMI) $(ASMCOMP_CMI) + +TOPLEVEL = \ + toplevel/genprintval.cmo \ + toplevel/topcommon.cmo \ + toplevel/byte/topeval.cmo \ + toplevel/byte/trace.cmo \ + toplevel/toploop.cmo \ + toplevel/topdirs.cmo \ + toplevel/byte/topmain.cmo +TOPLEVEL_CMI = \ + toplevel/topcommon.cmi \ + toplevel/byte/topeval.cmi \ + toplevel/byte/trace.cmi \ + toplevel/toploop.cmi \ + toplevel/topdirs.cmi \ toplevel/byte/topmain.cmi -OPTTOPLEVEL=toplevel/genprintval.cmo toplevel/topcommon.cmo \ - toplevel/native/topeval.cmo toplevel/native/trace.cmo toplevel/toploop.cmo \ - toplevel/topdirs.cmo toplevel/native/topmain.cmo -OPTTOPLEVEL_CMI=toplevel/topcommon.cmi toplevel/native/topeval.cmi \ - toplevel/native/trace.cmi toplevel/toploop.cmi toplevel/topdirs.cmi \ +OPTTOPLEVEL = \ + toplevel/genprintval.cmo \ + toplevel/topcommon.cmo \ + toplevel/native/topeval.cmo \ + toplevel/native/trace.cmo \ + toplevel/toploop.cmo \ + toplevel/topdirs.cmo \ + toplevel/native/topmain.cmo +OPTTOPLEVEL_CMI = \ + toplevel/topcommon.cmi \ + toplevel/native/topeval.cmi \ + toplevel/native/trace.cmi \ + toplevel/toploop.cmi \ + toplevel/topdirs.cmi \ toplevel/native/topmain.cmi TOPLEVEL_SHARED_MLIS = topeval.mli trace.mli topmain.mli @@ -760,6 +760,7 @@ afl function_sections flat_float_array windows_unicode +cmm_invariants flambda_invariants flambda frame_pointers @@ -902,6 +903,7 @@ enable_native_compiler enable_flambda enable_flambda_invariants enable_force_instrumented_runtime +enable_cmm_invariants with_target_bindir enable_reserved_header_bits enable_stdlib_manpages @@ -1577,6 +1579,7 @@ Optional Features: enable invariants checks in flambda --force-instrumented-runtime force the usage of the instrumented runtime + --enable-cmm-invariants enable invariants checks in Cmm --enable-reserved-header-bits=BITS reserve BITS (between 0 and 31) bits in block headers for profiling info @@ -2936,6 +2939,7 @@ VERSION=4.13.0+domains+dev + ## Generated files ac_config_files="$ac_config_files Makefile.build_config" @@ -3251,6 +3255,12 @@ if test "${enable_force_instrumented_runtime+set}" = set; then : fi +# Check whether --enable-cmm-invariants was given. +if test "${enable_cmm_invariants+set}" = set; then : + enableval=$enable_cmm_invariants; +fi + + # Check whether --with-target-bindir was given. if test "${with_target_bindir+set}" = set; then : @@ -17128,6 +17138,12 @@ else flambda_invariants=false fi +if test x"$enable_cmm_invariants" = "xyes"; then : + cmm_invariants=true +else + cmm_invariants=false +fi + if test x"$enable_flat_float_array" = "xno"; then : flat_float_array=false else diff --git a/configure.ac b/configure.ac index 0fe3f9e45e..3c1e731c1d 100644 --- a/configure.ac +++ b/configure.ac @@ -157,6 +157,7 @@ AC_SUBST([profinfo_width]) AC_SUBST([frame_pointers]) AC_SUBST([flambda]) AC_SUBST([flambda_invariants]) +AC_SUBST([cmm_invariants]) AC_SUBST([windows_unicode]) AC_SUBST([flat_float_array]) AC_SUBST([function_sections]) @@ -322,6 +323,10 @@ AC_ARG_ENABLE([force-instrumented-runtime], [AS_HELP_STRING([--force-instrumented-runtime], [force the usage of the instrumented runtime])]) +AC_ARG_ENABLE([cmm-invariants], + [AS_HELP_STRING([--enable-cmm-invariants], + [enable invariants checks in Cmm])]) + AC_ARG_WITH([target-bindir], [AS_HELP_STRING([--with-target-bindir], [location of binary programs on target system])]) @@ -1782,6 +1787,10 @@ AS_IF([test x"$enable_flambda" = "xyes"], [flambda=false flambda_invariants=false]) +AS_IF([test x"$enable_cmm_invariants" = "xyes"], + [cmm_invariants=true], + [cmm_invariants=false]) + AS_IF([test x"$enable_flat_float_array" = "xno"], [flat_float_array=false], [AC_DEFINE([FLAT_FLOAT_ARRAY]) diff --git a/driver/compenv.ml b/driver/compenv.ml index 144509a7c7..f1e167d520 100644 --- a/driver/compenv.ml +++ b/driver/compenv.ml @@ -371,6 +371,8 @@ let read_one_param ppf position name v = set "flambda-verbose" [ dump_flambda_verbose ] v | "flambda-invariants" -> set "flambda-invariants" [ flambda_invariant_checks ] v + | "cmm-invariants" -> + set "cmm-invariants" [ cmm_invariants ] v | "linscan" -> set "linscan" [ use_linscan ] v | "insn-sched" -> set "insn-sched" [ insn_sched ] v @@ -719,4 +721,33 @@ let process_deferred_actions env = !print_types || match !stop_after with | None -> false - | Some p -> Clflags.Compiler_pass.is_compilation_pass p; + | Some p -> Clflags.Compiler_pass.is_compilation_pass p + +(* This function is almost the same as [Arg.parse_expand], except + that [Arg.parse_expand] could not be used because it does not take a + reference for [arg_spec]. + We use a marker \000 for Arg.parse_and_expand_argv_dynamic + so we can split out error message from usage options, because + it always concatenates + error message with usage options *) +let parse_arguments ?(current=ref 0) argv f program = + try + Arg.parse_and_expand_argv_dynamic current argv Clflags.arg_spec f "\000" + with + | Arg.Bad err_msg -> + let usage_msg = create_usage_msg program in + let err_msg = err_msg + |> String.split_on_char '\000' + |> List.hd + |> String.trim in + Printf.eprintf "%s\n%s\n" err_msg usage_msg; + raise (Exit_with_status 2) + | Arg.Help msg -> + let err_msg = + msg + |> String.split_on_char '\000' + |> String.concat "" in + let help_msg = + Printf.sprintf "Usage: %s <options> <files>\nOptions are:" program in + Printf.printf "%s\n%s" help_msg err_msg; + raise (Exit_with_status 0) diff --git a/driver/compenv.mli b/driver/compenv.mli index 3ed6e11819..f849a9ce8d 100644 --- a/driver/compenv.mli +++ b/driver/compenv.mli @@ -80,3 +80,8 @@ val process_deferred_actions : string * (* ocaml module extension *) string -> (* ocaml library extension *) unit +(* [parse_arguments ?current argv anon_arg program] will parse the arguments, + using the arguments provided in [Clflags.arg_spec]. +*) +val parse_arguments : ?current:(int ref) + -> string array ref -> Arg.anon_fun -> string -> unit diff --git a/driver/main_args.ml b/driver/main_args.ml index afa1a44a0e..18badefa5b 100644 --- a/driver/main_args.ml +++ b/driver/main_args.ml @@ -779,6 +779,10 @@ let mk_dcamlprimc f = "-dcamlprimc", Arg.Unit f, " (undocumented)" ;; +let mk_dcmm_invariants f = + "-dcmm-invariants", Arg.Unit f, " Extra sanity checks on Cmm" +;; + let mk_dcmm f = "-dcmm", Arg.Unit f, " (undocumented)" ;; @@ -1077,6 +1081,7 @@ module type Optcommon_options = sig val _dflambda_verbose : unit -> unit val _drawclambda : unit -> unit val _dclambda : unit -> unit + val _dcmm_invariants : unit -> unit val _dcmm : unit -> unit val _dsel : unit -> unit val _dcombine : unit -> unit @@ -1433,6 +1438,7 @@ struct mk_dlambda F._dlambda; mk_drawclambda F._drawclambda; mk_dclambda F._dclambda; + mk_dcmm_invariants F._dcmm_invariants; mk_dflambda F._dflambda; mk_drawflambda F._drawflambda; mk_dflambda_invariants F._dflambda_invariants; @@ -1541,6 +1547,7 @@ module Make_opttop_options (F : Opttop_options) = struct mk_drawlambda F._drawlambda; mk_drawclambda F._drawclambda; mk_dclambda F._dclambda; + mk_dcmm_invariants F._dcmm_invariants; mk_drawflambda F._drawflambda; mk_dflambda F._dflambda; mk_dcmm F._dcmm; @@ -1722,6 +1729,7 @@ module Default = struct let _dalloc = set dump_regalloc let _dclambda = set dump_clambda let _dcmm = set dump_cmm + let _dcmm_invariants = set cmm_invariants let _dcombine = set dump_combine let _dcse = set dump_cse let _dflambda = set dump_flambda diff --git a/driver/main_args.mli b/driver/main_args.mli index 6f77a29708..2e814ca0ac 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -203,6 +203,7 @@ module type Optcommon_options = sig val _dflambda_verbose : unit -> unit val _drawclambda : unit -> unit val _dclambda : unit -> unit + val _dcmm_invariants : unit -> unit val _dcmm : unit -> unit val _dsel : unit -> unit val _dcombine : unit -> unit diff --git a/driver/maindriver.ml b/driver/maindriver.ml index 81d7edfd29..c0d2e8e515 100644 --- a/driver/maindriver.ml +++ b/driver/maindriver.ml @@ -15,18 +15,18 @@ open Clflags -let usage = "Usage: ocamlc <options> <files>\nOptions are:" module Options = Main_args.Make_bytecomp_options (Main_args.Default.Main) let main argv ppf = + let program = "ocamlc" in Clflags.add_arguments __LOC__ Options.list; Clflags.add_arguments __LOC__ ["-depend", Arg.Unit Makedepend.main_from_option, "<options> Compute dependencies (use 'ocamlc -depend -help' for details)"]; match Compenv.readenv ppf Before_args; - Clflags.parse_arguments argv Compenv.anonymous usage; + Compenv.parse_arguments (ref argv) Compenv.anonymous program; Compmisc.read_clflags_from_env (); if !Clflags.plugin then Compenv.fatal "-plugin is only supported up to OCaml 4.08.0"; @@ -40,7 +40,7 @@ let main argv ppf = with Arg.Bad msg -> begin prerr_endline msg; - Clflags.print_arguments usage; + Clflags.print_arguments program; exit 2 end end; diff --git a/driver/makedepend.ml b/driver/makedepend.ml index 481b6507cc..d9e70bb3db 100644 --- a/driver/makedepend.ml +++ b/driver/makedepend.ml @@ -653,17 +653,16 @@ let run_main argv = "<file> Read additional NUL separated command line arguments from \n\ \ <file>" ]; - let usage = - Printf.sprintf "Usage: %s [options] <source files>\nOptions are:" - (Filename.basename Sys.argv.(0)) - in - Clflags.parse_arguments argv (add_dep_arg (fun f -> Src (f, None))) usage; + let program = Filename.basename Sys.argv.(0) in + Compenv.parse_arguments (ref argv) + (add_dep_arg (fun f -> Src (f, None))) program; process_dep_args (List.rev !dep_args_rev); Compenv.readenv ppf Before_link; if !sort_files then sort_files_by_dependencies !files else List.iter print_file_dependencies (List.sort compare !files); exit (if Error_occurred.get () then 2 else 0) + let main () = run_main Sys.argv diff --git a/driver/optmaindriver.ml b/driver/optmaindriver.ml index 3ead11643d..30c5cb1da4 100644 --- a/driver/optmaindriver.ml +++ b/driver/optmaindriver.ml @@ -33,11 +33,11 @@ module Backend = struct end let backend = (module Backend : Backend_intf.S) -let usage = "Usage: ocamlopt <options> <files>\nOptions are:" module Options = Main_args.Make_optcomp_options (Main_args.Default.Optmain) let main argv ppf = native_code := true; + let program = "ocamlopt" in match Compenv.readenv ppf Before_args; Clflags.add_arguments __LOC__ (Arch.command_line_options @ Options.list); @@ -45,7 +45,7 @@ let main argv ppf = ["-depend", Arg.Unit Makedepend.main_from_option, "<options> Compute dependencies \ (use 'ocamlopt -depend -help' for details)"]; - Clflags.parse_arguments argv Compenv.anonymous usage; + Compenv.parse_arguments (ref argv) Compenv.anonymous program; Compmisc.read_clflags_from_env (); if !Clflags.plugin then Compenv.fatal "-plugin is only supported up to OCaml 4.08.0"; @@ -59,7 +59,7 @@ let main argv ppf = with Arg.Bad msg -> begin prerr_endline msg; - Clflags.print_arguments usage; + Clflags.print_arguments program; exit 2 end end; @@ -26,7 +26,6 @@ (copy_files# bytecomp/*.ml{,i}) (copy_files# driver/*.ml{,i}) (copy_files# asmcomp/*.ml{,i}) -(copy_files# asmcomp/debug/*.ml{,i}) (copy_files# file_formats/*.ml{,i}) (copy_files# lambda/*.ml{,i}) (copy_files# middle_end/*.ml{,i}) @@ -146,13 +145,15 @@ (wrapped false) (flags (:standard -principal -nostdlib)) (libraries stdlib ocamlcommon ocamlmiddleend) - (modules_without_implementation x86_ast) + (modules_without_implementation x86_ast emitenv) (modules ;; asmcomp/ afl_instrument arch asmgen asmlibrarian asmlink asmpackager branch_relaxation branch_relaxation_intf cmm_helpers cmm cmmgen cmmgen_state coloring comballoc + cmm_invariants CSE CSEgen deadcode domainstate emit emitaux interf interval linear linearize linscan + emitenv liveness mach printcmm printlinear printmach proc reg reload reloadgen schedgen scheduling selectgen selection spill split strmatch x86_ast x86_dsl x86_gas x86_masm x86_proc diff --git a/lambda/lambda.ml b/lambda/lambda.ml index dd958e3786..622d20eacb 100644 --- a/lambda/lambda.ml +++ b/lambda/lambda.ml @@ -194,14 +194,7 @@ and raise_kind = | Raise_reraise | Raise_notrace -let equal_boxed_integer x y = - match x, y with - | Pnativeint, Pnativeint - | Pint32, Pint32 - | Pint64, Pint64 -> - true - | (Pnativeint | Pint32 | Pint64), _ -> - false +let equal_boxed_integer = Primitive.equal_boxed_integer let equal_primitive = (* Should be implemented like [equal_value_kind] of [equal_boxed_integer], diff --git a/ocamltest/builtin_actions.ml b/ocamltest/builtin_actions.ml index 2cee238016..0f2974d12a 100644 --- a/ocamltest/builtin_actions.ml +++ b/ocamltest/builtin_actions.ml @@ -298,6 +298,7 @@ let _ = arch64; has_symlink; setup_build_env; + setup_simple_build_env; run; script; check_program_output; diff --git a/ocamltest/ocaml_actions.ml b/ocamltest/ocaml_actions.ml index ce3798a3ed..9ff809fe5c 100644 --- a/ocamltest/ocaml_actions.ml +++ b/ocamltest/ocaml_actions.ml @@ -724,7 +724,10 @@ let run_codegen log env = flags env; "-S " ^ testfile ] in - let expected_exit_status = 0 in + let expected_exit_status = + Actions_helpers.exit_status_of_variable env + Ocaml_variables.codegen_exit_status + in let exit_status = Actions_helpers.run_cmd ~environment:default_ocaml_env @@ -734,12 +737,15 @@ let run_codegen log env = log env commandline in if exit_status=expected_exit_status then begin - let finalise = - if Ocamltest_config.ccomptype="msvc" - then finalise_codegen_msvc - else finalise_codegen_cc - in - finalise testfile_basename log env + if exit_status=0 + then begin + let finalise = + if Ocamltest_config.ccomptype="msvc" + then finalise_codegen_msvc + else finalise_codegen_cc + in + finalise testfile_basename log env + end else (Result.pass, env) end else begin let reason = (Actions_helpers.mkreason diff --git a/ocamltest/ocaml_variables.ml b/ocamltest/ocaml_variables.ml index 616b03e433..e6a251ebba 100644 --- a/ocamltest/ocaml_variables.ml +++ b/ocamltest/ocaml_variables.ml @@ -62,6 +62,9 @@ let caml_ld_library_path = ("ld_library_path", "List of paths to lookup for loading dynamic libraries") +let codegen_exit_status = make ("codegen_exit_status", + "Expected exit status of codegen") + let compare_programs = make ("compare_programs", "Set to \"false\" to disable program comparison") @@ -243,6 +246,7 @@ let _ = List.iter register_variable bytecc_libs; c_preprocessor; caml_ld_library_path; + codegen_exit_status; compare_programs; compiler_directory_suffix; compiler_reference; diff --git a/ocamltest/ocaml_variables.mli b/ocamltest/ocaml_variables.mli index 3346c433b3..8bd31b4fc7 100644 --- a/ocamltest/ocaml_variables.mli +++ b/ocamltest/ocaml_variables.mli @@ -32,6 +32,8 @@ val cc : Variables.t val caml_ld_library_path : Variables.t +val codegen_exit_status : Variables.t + val compare_programs : Variables.t val compiler_directory_suffix : Variables.t diff --git a/ocamltest/tsl_lexer.mll b/ocamltest/tsl_lexer.mll index 21a2038dcf..1258c88fd4 100644 --- a/ocamltest/tsl_lexer.mll +++ b/ocamltest/tsl_lexer.mll @@ -33,8 +33,10 @@ rule token = parse | blank * { token lexbuf } | newline { Lexing.new_line lexbuf; token lexbuf } | "/*" blank* "TEST" { TSL_BEGIN_C_STYLE } + | "/*" blank* "TEST_BELOW" _ * "/*" blank* "TEST" { TSL_BEGIN_C_STYLE } | "*/" { TSL_END_C_STYLE } | "(*" blank* "TEST" { TSL_BEGIN_OCAML_STYLE } + | "(*" blank* "TEST_BELOW" _ * "(*" blank* "TEST" { TSL_BEGIN_OCAML_STYLE } | "*)" { TSL_END_OCAML_STYLE } | "," { COMMA } | '*'+ { TEST_DEPTH (String.length (Lexing.lexeme lexbuf)) } diff --git a/otherlibs/dynlink/Makefile b/otherlibs/dynlink/Makefile index 41e33d5449..644ab12199 100644 --- a/otherlibs/dynlink/Makefile +++ b/otherlibs/dynlink/Makefile @@ -30,7 +30,7 @@ OCAMLOPT=$(BEST_OCAMLOPT) -g -nostdlib -I $(ROOTDIR)/stdlib # COMPFLAGS should be in sync with the toplevel Makefile's COMPFLAGS. COMPFLAGS=-strict-sequence -principal -absname \ -w +a-4-9-40-41-42-44-45-48-66-70 \ - -warn-error +A \ + -warn-error +A \ -bin-annot -safe-string -strict-formats ifeq "$(FLAMBDA)" "true" OPTCOMPFLAGS += -O3 diff --git a/runtime/Makefile b/runtime/Makefile index 0ab006e9ab..2b63ff1df4 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -249,11 +249,11 @@ prims.c : primitives echo '#include "caml/prims.h"'; \ sed -e 's/.*/extern value &();/' primitives; \ echo 'c_primitive caml_builtin_cprim[] = {'; \ - sed -e 's/.*/ &,/' primitives; \ - echo ' 0 };'; \ + sed -e 's/.*/ &,/' primitives; \ + echo ' 0 };'; \ echo 'char * caml_names_of_builtin_cprim[] = {'; \ - sed -e 's/.*/ "&",/' primitives; \ - echo ' 0 };') > prims.c + sed -e 's/.*/ "&",/' primitives; \ + echo ' 0 };') > prims.c caml/opnames.h : caml/instruct.h tr -d '\r' < $< | \ diff --git a/runtime/floats.c b/runtime/floats.c index 1f6680476f..b24e0be00f 100644 --- a/runtime/floats.c +++ b/runtime/floats.c @@ -742,12 +742,13 @@ CAMLprim value caml_fmod_float(value f1, value f2) CAMLprim value caml_frexp_float(value f) { - CAMLparam1 (f); - CAMLlocal2 (res, mantissa); + CAMLparam0 (); + CAMLlocal1 (mantissa); + value res; int exponent; mantissa = caml_copy_double(frexp (Double_val(f), &exponent)); - res = caml_alloc_tuple(2); + res = caml_alloc_small(2, 0); Field(res, 0) = mantissa; Field(res, 1) = Val_int(exponent); CAMLreturn (res); @@ -777,14 +778,14 @@ CAMLprim value caml_log10_float(value f) CAMLprim value caml_modf_float(value f) { + CAMLparam0 (); + CAMLlocal2 (quo, rem); + value res; double frem; - CAMLparam1 (f); - CAMLlocal3 (res, quo, rem); - quo = caml_copy_double(modf (Double_val(f), &frem)); rem = caml_copy_double(frem); - res = caml_alloc_tuple(2); + res = caml_alloc_small(2, 0); Field(res, 0) = quo; Field(res, 1) = rem; CAMLreturn (res); diff --git a/testsuite/tests/asmgen/invariants.cmm b/testsuite/tests/asmgen/invariants.cmm new file mode 100644 index 0000000000..6e93a46e69 --- /dev/null +++ b/testsuite/tests/asmgen/invariants.cmm @@ -0,0 +1,24 @@ +(* TEST +* native-compiler +** setup-simple-build-env +*** codegen +codegen_exit_status = "2" +*) + +(* +This test is here to ensure that the Cmm invariant checks +correctly catch broken Cmm programs. +*) + +(function "bad_continuations" (x:int) + (* Bad arity *) + (catch + (exit cont 0) + with (cont) 1) + (* Multiple handler definition *) + (catch + (exit cont 0) + with (cont y:int) y) + (* Exit out of scope of its handler *) + (exit cont 0) +) diff --git a/testsuite/tests/backtrace/backtrace.ml b/testsuite/tests/backtrace/backtrace.ml index f3683751df..5f41e8631a 100644 --- a/testsuite/tests/backtrace/backtrace.ml +++ b/testsuite/tests/backtrace/backtrace.ml @@ -1,7 +1,7 @@ -(* TEST - flags = "-g" - ocamlrunparam += ",b=1" -*) +(* TEST_BELOW *) + + + (* A test for stack backtraces *) @@ -19,3 +19,8 @@ let g msg = let _ = ignore (g Sys.argv.(1)) + +(* TEST + flags = "-g" + ocamlrunparam += ",b=1" +*) diff --git a/testsuite/tests/basic/eval_order_7.ml b/testsuite/tests/basic/eval_order_7.ml new file mode 100644 index 0000000000..70689e0673 --- /dev/null +++ b/testsuite/tests/basic/eval_order_7.ml @@ -0,0 +1,11 @@ +(* TEST *) + +let p i x = + print_int i; + print_newline (); + x + +let _ = + for i = (p 13 0) to (p 25 3) do + p i () + done diff --git a/testsuite/tests/basic/eval_order_7.reference b/testsuite/tests/basic/eval_order_7.reference new file mode 100644 index 0000000000..7e088b6d5c --- /dev/null +++ b/testsuite/tests/basic/eval_order_7.reference @@ -0,0 +1,6 @@ +13 +25 +0 +1 +2 +3 diff --git a/testsuite/tests/tool-toplevel/exotic_lists.compilers.reference b/testsuite/tests/tool-toplevel/exotic_lists.compilers.reference index e7885856f2..957052bafb 100644 --- a/testsuite/tests/tool-toplevel/exotic_lists.compilers.reference +++ b/testsuite/tests/tool-toplevel/exotic_lists.compilers.reference @@ -5,6 +5,10 @@ L.(::) ([1; 2], - : (int, string) L.t = (::) (1, (::) ("2", (::) (3, (::) ("4", (::) (5, []))))) module L : sig type 'a t = 'a list = [] | (::) of 'a * 'a t end -- : int L.t L.t = [[1]; [2]; [3]; [4]; [5]] -- : int L.t = [1; 2; 3; 4; 5] +- : int L.t L.t = +L.(::) (L.(::) (1, L.[]), + L.(::) (L.(::) (2, L.[]), + L.(::) (L.(::) (3, L.[]), + L.(::) (L.(::) (4, L.[]), L.(::) (L.(::) (5, L.[]), L.[]))))) +- : int L.t = (::) (1, (::) (2, (::) (3, (::) (4, (::) (5, []))))) diff --git a/testsuite/tests/typing-gadts/ambivalent_apply.ml b/testsuite/tests/typing-gadts/ambivalent_apply.ml index 294660cd16..e334db0da7 100644 --- a/testsuite/tests/typing-gadts/ambivalent_apply.ml +++ b/testsuite/tests/typing-gadts/ambivalent_apply.ml @@ -22,6 +22,8 @@ Error: This expression has type b = int let f (type a b) (w1 : (a, b -> b) eq) (w2 : (a, int -> int) eq) (g : a) = let Refl = w2 in let Refl = w1 in g 3;; [%%expect{| +val f : ('a, 'b -> 'b) eq -> ('a, int -> int) eq -> 'a -> int = <fun> +|}, Principal{| Line 2, characters 37-40: 2 | let Refl = w2 in let Refl = w1 in g 3;; ^^^ diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml index 8136430865..1f6d718606 100644 --- a/testsuite/tests/typing-gadts/test.ml +++ b/testsuite/tests/typing-gadts/test.ml @@ -1088,6 +1088,13 @@ Line 3, characters 2-26: ^^^^^^^^^^^^^^^^^^^^^^^^ Error: This expression has type < bar : int; foo : int; .. > but an expression was expected of type 'a + The type constructor $1 would escape its scope +|}, Principal{| +Line 3, characters 2-26: +3 | (x:<foo:int;bar:int;..>) + ^^^^^^^^^^^^^^^^^^^^^^^^ +Error: This expression has type < bar : int; foo : int; .. > + but an expression was expected of type 'a This instance of $1 is ambiguous: it would escape the scope of its equation |}];; @@ -1105,6 +1112,8 @@ let g (type t) (x:t) (e : t int_foo) (e' : t int_bar) = x, x#foo, x#bar ;; [%%expect{| +val g : 't -> 't int_foo -> 't int_bar -> 't * int * int = <fun> +|}, Principal{| Line 3, characters 5-10: 3 | x, x#foo, x#bar ^^^^^ diff --git a/testsuite/tests/typing-misc/constraints.ml b/testsuite/tests/typing-misc/constraints.ml index 9e9c079eb2..1faab200e1 100644 --- a/testsuite/tests/typing-misc/constraints.ml +++ b/testsuite/tests/typing-misc/constraints.ml @@ -156,7 +156,6 @@ Here is an example of a case that is not matched: Exception: Match_failure ("", 6, 23). |}] - (* #9866, #9873 *) type 'a t = 'b constraint 'a = 'b t;; @@ -214,7 +213,7 @@ Line 1, characters 0-59: 1 | type 'a t = <a : 'a; b : 'b> constraint <a : 'a; ..> = 'b t;; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: A type variable is unbound in this type declaration. -In method b: 'b the variable 'b is unbound + In method b: 'b the variable 'b is unbound |}] module rec M : sig type 'a t = 'b constraint 'a = 'b t end = M;; @@ -259,3 +258,41 @@ struct type !'a t = 'b constraint 'a = 'b s end *) + +type 'a t = T + constraint 'a = int + constraint 'a = float +[%%expect{| +Line 3, characters 13-23: +3 | constraint 'a = float + ^^^^^^^^^^ +Error: The type constraints are not consistent. + Type int is not compatible with type float +|}] + +type ('a,'b) t = T + constraint 'a = int -> float + constraint 'b = bool -> char + constraint 'a = 'b +[%%expect{| +Line 4, characters 13-20: +4 | constraint 'a = 'b + ^^^^^^^ +Error: The type constraints are not consistent. + Type int -> float is not compatible with type bool -> char + Type int is not compatible with type bool +|}] + +class type ['a, 'b] a = object + constraint 'a = 'b + constraint 'a = int * int + constraint 'b = float * float +end;; +[%%expect{| +Line 4, characters 2-31: +4 | constraint 'b = float * float + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The class constraints are not consistent. + Type int * int is not compatible with type float * float + Type int is not compatible with type float +|}] diff --git a/testsuite/tests/typing-misc/pr6416.ml b/testsuite/tests/typing-misc/pr6416.ml index af9cf7157b..7464356b6d 100644 --- a/testsuite/tests/typing-misc/pr6416.ml +++ b/testsuite/tests/typing-misc/pr6416.ml @@ -309,7 +309,7 @@ Error: Signature mismatch: does not match class type c = object method m : t/1 end The method m has type t/2 but is expected to have type t/1 - Type t/2 is not compatible with type t/1 = K.t + Type t/2 is not equal to type t/1 = K.t Line 12, characters 4-10: Definition of type t/1 Line 9, characters 2-8: diff --git a/testsuite/tests/typing-misc/pr7937.ml b/testsuite/tests/typing-misc/pr7937.ml index 3c1063a201..1b6a6e9e0b 100644 --- a/testsuite/tests/typing-misc/pr7937.ml +++ b/testsuite/tests/typing-misc/pr7937.ml @@ -12,7 +12,6 @@ Line 3, characters 35-39: ^^^^ Error: This expression has type bool but an expression was expected of type ([< `X of int & 'a ] as 'a) r - Types for tag `X are incompatible |}, Principal{| type 'a r = 'a constraint 'a = [< `X of int & 'a ] Line 3, characters 35-39: @@ -20,7 +19,6 @@ Line 3, characters 35-39: ^^^^ Error: This expression has type bool but an expression was expected of type ([< `X of 'b & 'a & 'c ] as 'a) r - Types for tag `X are incompatible |}] let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };; @@ -30,7 +28,6 @@ Line 1, characters 35-51: ^^^^^^^^^^^^^^^^ Error: This expression has type int ref but an expression was expected of type ([< `X of int & 'a ] as 'a) r - Types for tag `X are incompatible |}, Principal{| Line 1, characters 35-51: 1 | let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };; @@ -38,7 +35,6 @@ Line 1, characters 35-51: Error: This expression has type int ref but an expression was expected of type ([< `X of 'b & 'a & 'c ] as 'a) r - Types for tag `X are incompatible |}] let h: 'a. 'a r -> _ = function true | false -> ();; diff --git a/testsuite/tests/typing-misc/unbound_type_variables.ml b/testsuite/tests/typing-misc/unbound_type_variables.ml new file mode 100644 index 0000000000..c00d036079 --- /dev/null +++ b/testsuite/tests/typing-misc/unbound_type_variables.ml @@ -0,0 +1,61 @@ +(* TEST + * expect +*) + +type synonym = 'a -> 'a + +[%%expect{| +Line 1, characters 15-17: +1 | type synonym = 'a -> 'a + ^^ +Error: The type variable 'a is unbound in this type declaration. +|}] + +type record = { contents: 'a } + +[%%expect{| +Line 1, characters 26-28: +1 | type record = { contents: 'a } + ^^ +Error: The type variable 'a is unbound in this type declaration. +|}] + +type wrapper = Wrapper of 'a + +[%%expect{| +Line 1, characters 26-28: +1 | type wrapper = Wrapper of 'a + ^^ +Error: The type variable 'a is unbound in this type declaration. +|}] + +(* This type secretly has a type variable in it *) +type polyvariant = [> `C] + +[%%expect{| +Line 1, characters 0-25: +1 | type polyvariant = [> `C] + ^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: A type variable is unbound in this type declaration. + In type [> `C ] as 'a the variable 'a is unbound +|}] + +type 'a only_one = 'a * 'b + +[%%expect{| +Line 1, characters 24-26: +1 | type 'a only_one = 'a * 'b + ^^ +Error: The type variable 'b is unbound in this type declaration. +|}] + +type extensible = .. +type extensible += Extension of 'a + +[%%expect{| +type extensible = .. +Line 2, characters 32-34: +2 | type extensible += Extension of 'a + ^^ +Error: The type variable 'a is unbound in this type declaration. +|}] diff --git a/testsuite/tests/typing-modules-bugs/pr6985_extended.ml b/testsuite/tests/typing-modules-bugs/pr6985_extended.ml new file mode 100644 index 0000000000..01faa3fe04 --- /dev/null +++ b/testsuite/tests/typing-modules-bugs/pr6985_extended.ml @@ -0,0 +1,30 @@ +(* TEST + * expect +*) + + + +module Root = struct + type u + and t = private < .. > +end + +module Trunk = struct + include Root + type t = A + type u +end + +module M: sig + module type s = module type of Trunk +end = struct + module type s = sig + type t = A + type u + end +end +[%%expect {| +module Root : sig type u and t = private < .. > end +module Trunk : sig type t = A type u end +module M : sig module type s = sig type t = A type u end end +|}] diff --git a/testsuite/tests/typing-modules/inclusion_errors.ml b/testsuite/tests/typing-modules/inclusion_errors.ml new file mode 100644 index 0000000000..a20566f559 --- /dev/null +++ b/testsuite/tests/typing-modules/inclusion_errors.ml @@ -0,0 +1,1174 @@ +(* TEST + * expect +*) + +(********************************** Equality **********************************) + +module M : sig + type ('a, 'b) t = 'a * 'b +end = struct + type ('a, 'b) t = 'a * 'a +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type ('a, 'b) t = 'a * 'a +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type ('a, 'b) t = 'a * 'a end + is not included in + sig type ('a, 'b) t = 'a * 'b end + Type declarations do not match: + type ('a, 'b) t = 'a * 'a + is not included in + type ('a, 'b) t = 'a * 'b +|}];; + +module M : sig + type ('a, 'b) t = 'a * 'a +end = struct + type ('a, 'b) t = 'a * 'b +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type ('a, 'b) t = 'a * 'b +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type ('a, 'b) t = 'a * 'b end + is not included in + sig type ('a, 'b) t = 'a * 'a end + Type declarations do not match: + type ('a, 'b) t = 'a * 'b + is not included in + type ('a, 'b) t = 'a * 'a +|}];; + +module M : sig + type t = <m : 'b. 'b * ('b * <m:'c. 'c * 'bar> as 'bar)> +end = struct + type t = <m : 'a. 'a * ('a * 'foo)> as 'foo +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = <m : 'a. 'a * ('a * 'foo)> as 'foo +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = < m : 'a. 'a * ('a * 'b) > as 'b end + is not included in + sig type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > end + Type declarations do not match: + type t = < m : 'a. 'a * ('a * 'b) > as 'b + is not included in + type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > +|}];; + +type s = private < m : int; .. >;; +[%%expect{| +type s = private < m : int; .. > +|}];; + +module M : sig + type t = s +end = struct + type t = <m : int> +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = <m : int> +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = < m : int > end + is not included in + sig type t = s end + Type declarations do not match: + type t = < m : int > + is not included in + type t = s +|}];; + +module M : sig + type t = <m : int> +end = struct + type t = s +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = s +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = s end + is not included in + sig type t = < m : int > end + Type declarations do not match: + type t = s + is not included in + type t = < m : int > +|}];; + +module M : sig + type t = + | Foo of (int)*float +end = struct + type t = + | Foo of (int*int)*float +end;; +[%%expect{| +Lines 4-7, characters 6-3: +4 | ......struct +5 | type t = +6 | | Foo of (int*int)*float +7 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = Foo of (int * int) * float end + is not included in + sig type t = Foo of int * float end + Type declarations do not match: + type t = Foo of (int * int) * float + is not included in + type t = Foo of int * float + Constructors do not match: + Foo of (int * int) * float + is not compatible with: + Foo of int * float + The types are not equal. +|}];; + +module M : sig + type t = (int * float) +end = struct + type t = (int * float * int) +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = (int * float * int) +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = int * float * int end + is not included in + sig type t = int * float end + Type declarations do not match: + type t = int * float * int + is not included in + type t = int * float +|}];; + +module M : sig + type t = <n : int; m : float> +end = struct + type t = <n : int; f : float> +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = <n : int; f : float> +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = < f : float; n : int > end + is not included in + sig type t = < m : float; n : int > end + Type declarations do not match: + type t = < f : float; n : int > + is not included in + type t = < m : float; n : int > +|}];; + +module M : sig + type t = <n : int; m : float> +end = struct + type t = <n : int> +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = <n : int> +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = < n : int > end + is not included in + sig type t = < m : float; n : int > end + Type declarations do not match: + type t = < n : int > + is not included in + type t = < m : float; n : int > +|}];; + +module M4 : sig + type t = <n : int; m : float * int> +end = struct + type t = <n : int; m : int> +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = <n : int; m : int> +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = < m : int; n : int > end + is not included in + sig type t = < m : float * int; n : int > end + Type declarations do not match: + type t = < m : int; n : int > + is not included in + type t = < m : float * int; n : int > +|}];; + +module M4 : sig + type t = + | Foo of [`Foo of string | `Bar of string] +end = struct + type t = + | Foo of [`Bar of string] +end;; +[%%expect{| +Lines 4-7, characters 6-3: +4 | ......struct +5 | type t = +6 | | Foo of [`Bar of string] +7 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = Foo of [ `Bar of string ] end + is not included in + sig type t = Foo of [ `Bar of string | `Foo of string ] end + Type declarations do not match: + type t = Foo of [ `Bar of string ] + is not included in + type t = Foo of [ `Bar of string | `Foo of string ] + Constructors do not match: + Foo of [ `Bar of string ] + is not compatible with: + Foo of [ `Bar of string | `Foo of string ] + The types are not equal. +|}];; + +module M : sig + type t = private [`C of int] +end = struct + type t = private [`C] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [`C] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [ `C ] end + is not included in + sig type t = private [ `C of int ] end + Type declarations do not match: + type t = private [ `C ] + is not included in + type t = private [ `C of int ] +|}];; + +module M : sig + type t = private [`C] +end = struct + type t = private [`C of int] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [`C of int] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [ `C of int ] end + is not included in + sig type t = private [ `C ] end + Type declarations do not match: + type t = private [ `C of int ] + is not included in + type t = private [ `C ] +|}];; + +module M : sig + type t = [`C of [< `A] | `C of [`A]] +end = struct + type t = [`C of [< `A | `B] | `C of [`A]] +end;; +[%%expect{| +module M : sig type t = [ `C of [ `A ] ] end +|}];; + +module M : sig + type t = private [> `A of int] +end = struct + type t = private [`A of int] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [`A of int] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [ `A of int ] end + is not included in + sig type t = private [> `A of int ] end + Type declarations do not match: + type t = private [ `A of int ] + is not included in + type t = private [> `A of int ] +|}];; + +module M : sig + type t = private [`A of int] +end = struct + type t = private [> `A of int] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [> `A of int] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [> `A of int ] end + is not included in + sig type t = private [ `A of int ] end + Type declarations do not match: + type t = private [> `A of int ] + is not included in + type t = private [ `A of int ] +|}];; + +module M : sig + type 'a t = [> `A of int | `B of int] as 'a +end = struct + type 'a t = [> `A of int] as 'a +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type 'a t = [> `A of int] as 'a +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type 'a t = 'a constraint 'a = [> `A of int ] end + is not included in + sig type 'a t = 'a constraint 'a = [> `A of int | `B of int ] end + Type declarations do not match: + type 'a t = 'a constraint 'a = [> `A of int ] + is not included in + type 'a t = 'a constraint 'a = [> `A of int | `B of int ] +|}];; + +module M : sig + type 'a t = [> `A of int] as 'a +end = struct + type 'a t = [> `A of int | `C of float] as 'a +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type 'a t = [> `A of int | `C of float] as 'a +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type 'a t = 'a constraint 'a = [> `A of int | `C of float ] end + is not included in + sig type 'a t = 'a constraint 'a = [> `A of int ] end + Type declarations do not match: + type 'a t = 'a constraint 'a = [> `A of int | `C of float ] + is not included in + type 'a t = 'a constraint 'a = [> `A of int ] +|}];; + +module M : sig + type t = [`C of [< `A | `B] | `C of [`A]] +end = struct + type t = [`C of [< `A] | `C of [`A]] +end;; +[%%expect{| +module M : sig type t = [ `C of [ `A ] ] end +|}];; + +module M : sig + type t = private [< `C] +end = struct + type t = private [< `C of int&float] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [< `C of int&float] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [< `C of int & float ] end + is not included in + sig type t = private [< `C ] end + Type declarations do not match: + type t = private [< `C of int & float ] + is not included in + type t = private [< `C ] +|}];; + +(********************************** Moregen ***********************************) + +module type T = sig + type t +end +module Int = struct + type t = int +end +module type S = sig + module Choice : T + val r : Choice.t list ref ref +end +module Force (X : functor () -> S) = struct end +module Choose () = struct + module Choice = + (val (module Int : T)) + let r = ref (ref []) +end +module Ignore = Force(Choose) +[%%expect{| +module type T = sig type t end +module Int : sig type t = int end +module type S = sig module Choice : T val r : Choice.t list ref ref end +module Force : functor (X : functor () -> S) -> sig end +module Choose : + functor () -> sig module Choice : T val r : '_weak1 list ref ref end +Line 17, characters 16-29: +17 | module Ignore = Force(Choose) + ^^^^^^^^^^^^^ +Error: Modules do not match: + functor () -> sig module Choice : T val r : '_weak1 list ref ref end + is not included in functor () -> S + Modules do not match: + sig module Choice : T val r : '_weak1 list ref ref end + is not included in + S + Values do not match: + val r : '_weak1 list ref ref + is not included in + val r : Choice.t list ref ref +|}];; + +module O = struct + module type s + module M: sig + val f: (module s) -> unit + end = struct + module type s + let f (module X:s) = () + end +end;; +[%%expect{| +Lines 5-8, characters 8-5: +5 | ........struct +6 | module type s +7 | let f (module X:s) = () +8 | end +Error: Signature mismatch: + Modules do not match: + sig module type s val f : (module s) -> unit end + is not included in + sig val f : (module s) -> unit end + Values do not match: + val f : (module s/1) -> unit + is not included in + val f : (module s/2) -> unit + Line 6, characters 4-17: + Definition of module type s/1 + Line 2, characters 2-15: + Definition of module type s/2 +|}];; + +module M : sig + val f : (<m : 'b. ('b * <m: 'c. 'c * 'bar> as 'bar)>) -> unit +end = struct + let f (x : <m : 'a. ('a * 'foo)> as 'foo) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : <m : 'a. ('a * 'foo)> as 'foo) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : (< m : 'a. 'a * 'b > as 'b) -> unit end + is not included in + sig val f : < m : 'b. 'b * < m : 'c. 'c * 'a > as 'a > -> unit end + Values do not match: + val f : (< m : 'a. 'a * 'b > as 'b) -> unit + is not included in + val f : < m : 'b. 'b * < m : 'c. 'c * 'a > as 'a > -> unit +|}];; + +type s = private < m : int; .. >;; + +module M : sig + val f : s -> s +end = struct + let f (x : <m : int>) = x +end;; +[%%expect{| +type s = private < m : int; .. > +Lines 5-7, characters 6-3: +5 | ......struct +6 | let f (x : <m : int>) = x +7 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : < m : int > -> < m : int > end + is not included in + sig val f : s -> s end + Values do not match: + val f : < m : int > -> < m : int > + is not included in + val f : s -> s +|}];; + +module M : sig + val x : 'a list ref +end = struct + let x = ref [] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let x = ref [] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val x : '_weak2 list ref end + is not included in + sig val x : 'a list ref end + Values do not match: + val x : '_weak2 list ref + is not included in + val x : 'a list ref +|}];; + +module M = struct let r = ref [] end;; +type t;; +module N : sig val r : t list ref end = M;; +[%%expect{| +module M : sig val r : '_weak3 list ref end +type t +Line 3, characters 40-41: +3 | module N : sig val r : t list ref end = M;; + ^ +Error: Signature mismatch: + Modules do not match: + sig val r : '_weak3 list ref end + is not included in + sig val r : t list ref end + Values do not match: + val r : '_weak3 list ref + is not included in + val r : t list ref +|}];; + +type (_, _) eq = Refl : ('a, 'a) eq;; + +module T : sig + type t + type s + val eq : (t, s) eq +end = struct + type t = int + type s = int + let eq = Refl +end;; + +module M = struct let r = ref [] end;; + +let foo p (e : (T.t, T.s) eq) (x : T.t) (y : T.s) = + match e with + | Refl -> + let z = if p then x else y in + let module N = struct + module type S = module type of struct let r = ref [z] end + end in + let module O : N.S = M in + ();; +[%%expect{| +type (_, _) eq = Refl : ('a, 'a) eq +module T : sig type t type s val eq : (t, s) eq end +module M : sig val r : '_weak4 list ref end +Line 22, characters 25-26: +22 | let module O : N.S = M in + ^ +Error: Signature mismatch: + Modules do not match: + sig val r : '_weak4 list ref end + is not included in + N.S + Values do not match: + val r : '_weak4 list ref + is not included in + val r : T.s list ref +|}];; + +module M: sig + val f : int -> float +end = struct + let f (x : 'a) = x +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : 'a) = x +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : 'a -> 'a end + is not included in + sig val f : int -> float end + Values do not match: + val f : 'a -> 'a + is not included in + val f : int -> float +|}];; + +module M: sig + val f : (int * float * int) -> (int -> int) +end = struct + let f (x : (int * int)) = x +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : (int * int)) = x +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : int * int -> int * int end + is not included in + sig val f : int * float * int -> int -> int end + Values do not match: + val f : int * int -> int * int + is not included in + val f : int * float * int -> int -> int +|}];; + +module M: sig + val f : <m : int; n : float> -> <m : int; n : float> +end = struct + let f (x : <m : int; f : float>) = x +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : <m : int; f : float>) = x +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : < f : float; m : int > -> < f : float; m : int > end + is not included in + sig val f : < m : int; n : float > -> < m : int; n : float > end + Values do not match: + val f : < f : float; m : int > -> < f : float; m : int > + is not included in + val f : < m : int; n : float > -> < m : int; n : float > +|}];; + +module M : sig + val f : [`Foo] -> unit +end = struct + let f (x : [ `Foo | `Bar]) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : [ `Foo | `Bar]) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : [ `Bar | `Foo ] -> unit end + is not included in + sig val f : [ `Foo ] -> unit end + Values do not match: + val f : [ `Bar | `Foo ] -> unit + is not included in + val f : [ `Foo ] -> unit +|}];; + +module M : sig + val f : [>`Foo] -> unit +end = struct + let f (x : [< `Foo]) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : [< `Foo]) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : [< `Foo ] -> unit end + is not included in + sig val f : [> `Foo ] -> unit end + Values do not match: + val f : [< `Foo ] -> unit + is not included in + val f : [> `Foo ] -> unit +|}];; + +module M : sig + val f : [< `Foo | `Bar] -> unit +end = struct + let f (x : [< `Foo]) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : [< `Foo]) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : [< `Foo ] -> unit end + is not included in + sig val f : [< `Bar | `Foo ] -> unit end + Values do not match: + val f : [< `Foo ] -> unit + is not included in + val f : [< `Bar | `Foo ] -> unit +|}];; + +module M : sig + val f : < m : [< `Foo]> -> unit +end = struct + let f (x : < m : 'a. [< `Foo] as 'a >) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : < m : 'a. [< `Foo] as 'a >) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : < m : 'a. [< `Foo ] as 'a > -> unit end + is not included in + sig val f : < m : [< `Foo ] > -> unit end + Values do not match: + val f : < m : 'a. [< `Foo ] as 'a > -> unit + is not included in + val f : < m : [< `Foo ] > -> unit +|}];; + +module M : sig + val f : < m : 'a. [< `Foo] as 'a > -> unit +end = struct + let f (x : < m : [`Foo]>) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : < m : [`Foo]>) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : < m : [ `Foo ] > -> unit end + is not included in + sig val f : < m : 'a. [< `Foo ] as 'a > -> unit end + Values do not match: + val f : < m : [ `Foo ] > -> unit + is not included in + val f : < m : 'a. [< `Foo ] as 'a > -> unit +|}];; + +module M : sig + val f : [< `C] -> unit +end = struct + let f (x : [< `C of int&float]) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : [< `C of int&float]) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : [< `C of int & float ] -> unit end + is not included in + sig val f : [< `C ] -> unit end + Values do not match: + val f : [< `C of int & float ] -> unit + is not included in + val f : [< `C ] -> unit +|}];; + +module M : sig + val f : [`Foo] -> unit +end = struct + let f (x : [`Foo of int]) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : [`Foo of int]) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : [ `Foo of int ] -> unit end + is not included in + sig val f : [ `Foo ] -> unit end + Values do not match: + val f : [ `Foo of int ] -> unit + is not included in + val f : [ `Foo ] -> unit +|}];; + +module M : sig + val f : [`Foo of int] -> unit +end = struct + let f (x : [`Foo]) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : [`Foo]) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : [ `Foo ] -> unit end + is not included in + sig val f : [ `Foo of int ] -> unit end + Values do not match: + val f : [ `Foo ] -> unit + is not included in + val f : [ `Foo of int ] -> unit +|}];; + +module M : sig + val f : [< `Foo | `Bar | `Baz] -> unit +end = struct + let f (x : [< `Foo | `Bar | `Baz]) = () +end;; +[%%expect{| +module M : sig val f : [< `Bar | `Baz | `Foo ] -> unit end +|}];; + +module M : sig + val f : [< `Foo | `Bar | `Baz] -> unit +end = struct + let f (x : [> `Foo | `Bar]) = () +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | let f (x : [> `Foo | `Bar]) = () +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig val f : [> `Bar | `Foo ] -> unit end + is not included in + sig val f : [< `Bar | `Baz | `Foo ] -> unit end + Values do not match: + val f : [> `Bar | `Foo ] -> unit + is not included in + val f : [< `Bar | `Baz | `Foo ] -> unit +|}];; + +(******************************* Type manifests *******************************) + +module M : sig + type t = private [< `A | `B] +end = struct + type t = [`C] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = [`C] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = [ `C ] end + is not included in + sig type t = private [< `A | `B ] end + Type declarations do not match: + type t = [ `C ] + is not included in + type t = private [< `A | `B ] +|}];; + +module M : sig + type t = private [< `A | `B] +end = struct + type t = private [> `A] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [> `A] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [> `A ] end + is not included in + sig type t = private [< `A | `B ] end + Type declarations do not match: + type t = private [> `A ] + is not included in + type t = private [< `A | `B ] +|}];; + +module M : sig + type t = private [< `A | `B > `A] +end = struct + type t = [`B] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = [`B] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = [ `B ] end + is not included in + sig type t = private [< `A | `B > `A ] end + Type declarations do not match: + type t = [ `B ] + is not included in + type t = private [< `A | `B > `A ] +|}];; + +module M : sig + type t = private [> `A of int] +end = struct + type t = [`A] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = [`A] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = [ `A ] end + is not included in + sig type t = private [> `A of int ] end + Type declarations do not match: + type t = [ `A ] + is not included in + type t = private [> `A of int ] +|}];; + +module M : sig + type t = private [< `A of int] +end = struct + type t = private [< `A of & int] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [< `A of & int] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [< `A of & int ] end + is not included in + sig type t = private [< `A of int ] end + Type declarations do not match: + type t = private [< `A of & int ] + is not included in + type t = private [< `A of int ] +|}];; + + +module M : sig + type t = private [< `A of int] +end = struct + type t = private [< `A] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [< `A] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [< `A ] end + is not included in + sig type t = private [< `A of int ] end + Type declarations do not match: + type t = private [< `A ] + is not included in + type t = private [< `A of int ] +|}];; + + +module M : sig + type t = private [< `A of int & float] +end = struct + type t = private [< `A] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = private [< `A] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private [< `A ] end + is not included in + sig type t = private [< `A of int & float ] end + Type declarations do not match: + type t = private [< `A ] + is not included in + type t = private [< `A of int & float ] +|}];; + +module M : sig + type t = private [> `A of int] +end = struct + type t = [`A of float] +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = [`A of float] +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = [ `A of float ] end + is not included in + sig type t = private [> `A of int ] end + Type declarations do not match: + type t = [ `A of float ] + is not included in + type t = private [> `A of int ] +|}];; + +module M : sig + type t = private <a : int; ..> +end = struct + type t = <b : int> +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = <b : int> +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = < b : int > end + is not included in + sig type t = private < a : int; .. > end + Type declarations do not match: + type t = < b : int > + is not included in + type t = private < a : int; .. > +|}];; + +module M : sig + type t = private <a : float; ..> +end = struct + type t = <a : int> +end;; +[%%expect{| +Lines 3-5, characters 6-3: +3 | ......struct +4 | type t = <a : int> +5 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = < a : int > end + is not included in + sig type t = private < a : float; .. > end + Type declarations do not match: + type t = < a : int > + is not included in + type t = private < a : float; .. > +|}];; + +type w = private float +type q = private (int * w) +type u = private (int * q) +module M : sig (* Confussing error message :( *) + type t = private (int * (int * int)) +end = struct + type t = private u +end;; +[%%expect{| +type w = private float +type q = private int * w +type u = private int * q +Lines 6-8, characters 6-3: +6 | ......struct +7 | type t = private u +8 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private u end + is not included in + sig type t = private int * (int * int) end + Type declarations do not match: + type t = private u + is not included in + type t = private int * (int * int) +|}];; + +type w = float +type q = (int * w) +type u = private (int * q) +module M : sig (* Confussing error message :( *) + type t = private (int * (int * int)) +end = struct + type t = private u +end;; +[%%expect{| +type w = float +type q = int * w +type u = private int * q +Lines 6-8, characters 6-3: +6 | ......struct +7 | type t = private u +8 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private u end + is not included in + sig type t = private int * (int * int) end + Type declarations do not match: + type t = private u + is not included in + type t = private int * (int * int) +|}];; + +type s = private int + +module M : sig + type t = private float +end = struct + type t = private s +end;; +[%%expect{| +type s = private int +Lines 5-7, characters 6-3: +5 | ......struct +6 | type t = private s +7 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = private s end + is not included in + sig type t = private float end + Type declarations do not match: + type t = private s + is not included in + type t = private float +|}];; diff --git a/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference b/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference index a5685448b5..9bf6524d6b 100644 --- a/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference +++ b/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference @@ -47,3 +47,4 @@ Error: The class type Type exp = < eval : (string, exp) Hashtbl.t -> expr > is not compatible with type expr = [ `Abs of string * expr | `App of expr * expr ] + Types for tag `App are incompatible diff --git a/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference b/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference index 68b176658e..ad3ea965b4 100644 --- a/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference +++ b/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference @@ -16,25 +16,5 @@ Error: This type entity = < destroy_subject : id subject; entity_id : id > Type (id subject, id) observer = < notify : id subject -> id -> unit > is not compatible with type 'a entity_container = - < add_entity : (< destroy_subject : < add_observer : 'a - entity_container -> - 'f; - .. > - as 'e; - .. > - as 'd) -> - 'f; - notify : 'd -> id -> unit > - Type entity = < destroy_subject : id subject; entity_id : id > - is not compatible with type < destroy_subject : 'e; .. > as 'd - Type - id subject = - < add_observer : (id subject, id) observer -> unit; - notify_observers : id -> unit > - is not compatible with type - < add_observer : 'a entity_container -> 'f; .. > as 'e - Type (id subject, id) observer = < notify : id subject -> id -> unit > - is not compatible with type - 'a entity_container = - < add_entity : 'd -> 'f; notify : 'd -> id -> unit > - The first object type has no method add_entity + < add_entity : 'a -> 'c; notify : 'a -> id -> unit > + Types for method add_observer are incompatible diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml index 85e43bd3a2..dcc954e438 100644 --- a/testsuite/tests/typing-poly/poly.ml +++ b/testsuite/tests/typing-poly/poly.ml @@ -966,6 +966,19 @@ Error: Constraints are not satisfied in this type. Type 'a u t should be an instance of g t |}];; +(* Full unification trace reported for "Constraints are not satisfied in this type" *) +type ('a,'b) t constraint 'a = 'b + constraint 'a = int + and 'a u = (float,string) t;; +[%%expect {| +Line 3, characters 13-29: +3 | and 'a u = (float,string) t;; + ^^^^^^^^^^^^^^^^ +Error: Constraints are not satisfied in this type. + Type (float, string) t should be an instance of (int, int) t + Type float is not compatible with type int +|}] + (* Example of wrong expansion *) type 'a u = < m : 'a v > and 'a v = 'a list u;; [%%expect {| @@ -1006,14 +1019,14 @@ type u = 'a t as 'a (* pass typetexp, but fails during Typedecl.check_recursion *) -type ('a, 'b) a = 'a -> unit constraint 'a = [> `B of ('a, 'b) b as 'b] -and ('a, 'b) b = 'b -> unit constraint 'b = [> `A of ('a, 'b) a as 'a];; -[%%expect {| -Line 1, characters 0-71: -1 | type ('a, 'b) a = 'a -> unit constraint 'a = [> `B of ('a, 'b) b as 'b] - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: The definition of a contains a cycle: - [> `B of ('a, 'b) b as 'b ] as 'a +type ('a1, 'b1) ty1 = 'a1 -> unit constraint 'a1 = [> `V1 of ('a1, 'b1) ty2 as 'b1] +and ('a2, 'b2) ty2 = 'b2 -> unit constraint 'b2 = [> `V2 of ('a2, 'b2) ty1 as 'a2];; +[%%expect {| +Line 1, characters 0-83: +1 | type ('a1, 'b1) ty1 = 'a1 -> unit constraint 'a1 = [> `V1 of ('a1, 'b1) ty2 as 'b1] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The definition of ty1 contains a cycle: + [> `V1 of ('a, 'b) ty2 as 'b ] as 'a |}];; (* PR#8359: expanding may change original in Ctype.unify2 *) diff --git a/testsuite/tests/typing-poly/pr9603.ml b/testsuite/tests/typing-poly/pr9603.ml index 9052a1a43f..02f1e921b9 100644 --- a/testsuite/tests/typing-poly/pr9603.ml +++ b/testsuite/tests/typing-poly/pr9603.ml @@ -29,8 +29,5 @@ Error: This expression has type < m : 'left 'right. < left : 'left; right : 'right > pair > but an expression was expected of type < m : 'left 'right. < left : 'left; right : 'right > pair > - Type < left : 'left; right : 'right > pair = 'a * 'b - is not compatible with type < left : 'left0; right : 'right0 > pair - The method left has type 'a, but the expected method type was 'left - The universal variable 'left would escape its scope + Types for method m are incompatible |}] diff --git a/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference b/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference index 411578cf64..82ba615155 100644 --- a/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference +++ b/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference @@ -1,6 +1,5 @@ File "pr3918c.ml", line 24, characters 11-12: 24 | let f x = (x : 'a vlist :> 'b vlist) ^ -Error: This expression has type 'b Pr3918b.vlist = 'a +Error: This expression has type 'b Pr3918b.vlist but an expression was expected of type 'b Pr3918b.vlist - The type variable 'a occurs inside ('d * 'c) Pr3918a.voption as 'c diff --git a/testsuite/tools/codegen_main.ml b/testsuite/tools/codegen_main.ml index d0b3d40434..cb2200d499 100644 --- a/testsuite/tools/codegen_main.ml +++ b/testsuite/tools/codegen_main.ml @@ -22,6 +22,7 @@ let compile_file filename = Emitaux.output_channel := open_out out_name end; (* otherwise, stdout *) Compilenv.reset "test"; + Clflags.cmm_invariants := true; Emit.begin_assembly(); let ic = open_in filename in let lb = Lexing.from_channel ic in diff --git a/tools/Makefile b/tools/Makefile index 800aab48f9..c7c62be91e 100644 --- a/tools/Makefile +++ b/tools/Makefile @@ -143,7 +143,7 @@ installopt:: # To help building mixed-mode libraries (OCaml + C) $(call byte_and_opt,ocamlmklib,config.cmo \ - build_path_prefix_map.cmo misc.cmo ocamlmklib.cmo,) + build_path_prefix_map.cmo misc.cmo ocamlmklib.cmo,) # To make custom toplevels @@ -273,8 +273,8 @@ $(call byte_and_opt,primreq,$(primreq),) LINTAPIDIFF=$(ROOTDIR)/compilerlibs/ocamlcommon.cmxa \ $(ROOTDIR)/compilerlibs/ocamlbytecomp.cmxa \ $(ROOTDIR)/compilerlibs/ocamlmiddleend.cmxa \ - $(ROOTDIR)/otherlibs/str/str.cmxa \ - lintapidiff.cmx + $(ROOTDIR)/otherlibs/str/str.cmxa \ + lintapidiff.cmx lintapidiff.opt$(EXE): INCLUDES+= -I $(ROOTDIR)/otherlibs/str lintapidiff.opt$(EXE): $(LINTAPIDIFF) diff --git a/tools/check-typo b/tools/check-typo index 6bd5b3840d..c5bf8eb951 100755 --- a/tools/check-typo +++ b/tools/check-typo @@ -303,9 +303,48 @@ EXIT_CODE=0 } } - BEGIN { state = "(first line)"; } + BEGIN { state = "(first line)"; in_recipe = 0; in_continuation = 0; } - match($0, /\t/) { + # Makefile recipe automaton + + # in_continuation == 1 if the line ends with a backslash + # in_recipe is: + # 0 - not in a recipe + # 1 - target line scanned, but not yet seen first recipe line + # 2 - scanning recipe lines + + # Non-recipe line + match($0, /^[^\t#] *[^# ]/) { + if (!in_continuation) { + if (!match($0, /^(ifn?eq|else|endif)/)) { + in_recipe = 0; + } + } + } + + # target: or target:: line + match($0, /^[^#]*[^:#]::?($|[^=])/) { + if (!in_continuation) { + in_recipe = 1; + } + } + + match($0, /^\t[^\t]+$/) { + if (in_recipe == 0 \ + || in_recipe == 1 && in_continuation \ + || is_err("makefile-whitespace")) { + err("tab", "TAB character(s)"); + } else { + ++ counts["makefile-whitespace"]; + in_recipe = 2; + } + } + + match($0, /.$/) { + in_continuation = (substr($0, length($0)) == "\\"); + } + + match($0, /.\t/) { err("tab", "TAB character(s)"); t = utf8_decode($0); if (more_columns(t, 80)){ diff --git a/toplevel/byte/topmain.ml b/toplevel/byte/topmain.ml index 0fdc12136e..3052796086 100644 --- a/toplevel/byte/topmain.ml +++ b/toplevel/byte/topmain.ml @@ -119,9 +119,6 @@ let _ = Topcommon.add_directive "untrace_all" (* --- *) -let usage = "Usage: ocaml <options> <object-files> [script-file [arguments]]\n\ - options are:" - let preload_objects = ref [] (* Position of the first non expanded argument *) @@ -209,15 +206,10 @@ let () = let main () = let ppf = Format.err_formatter in + let program = "ocaml" in Compenv.readenv ppf Before_args; - let list = ref Options.list in - begin - try - Arg.parse_and_expand_argv_dynamic current argv list file_argument usage; - with - | Arg.Bad msg -> Printf.eprintf "%s" msg; raise (Compenv.Exit_with_status 2) - | Arg.Help msg -> Printf.printf "%s" msg; raise (Compenv.Exit_with_status 0) - end; + Clflags.add_arguments __LOC__ Options.list; + Compenv.parse_arguments ~current argv file_argument program; Compenv.readenv ppf Before_link; Compmisc.read_clflags_from_env (); if not (prepare ppf) then raise (Compenv.Exit_with_status 2); diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml index 22cda7a271..f54d897c8e 100644 --- a/toplevel/genprintval.ml +++ b/toplevel/genprintval.ml @@ -253,9 +253,6 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct let nest f = nest_gen (Oval_stuff "<cycle>") f in - let is_list ty = - Ctype.matches env ty (Predef.type_list (Ctype.newvar ())) in - let rec tree_of_val depth obj ty = decr printer_steps; if !printer_steps < 0 || depth < 0 then Oval_ellipsis @@ -270,7 +267,8 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct Oval_stuff "<fun>" | Ttuple(ty_list) -> Oval_tuple (tree_of_val_list 0 depth obj ty_list) - | Tconstr(_, [ty_arg], _) when is_list ty -> + | Tconstr(path, [ty_arg], _) + when Path.same path Predef.path_list -> if O.is_block obj then match check_depth depth obj ty with Some x -> x @@ -590,7 +588,7 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct let rec find = function | [] -> raise Not_found | (_name, Simple (sch, printer)) :: remainder -> - if Ctype.moregeneral env false sch ty + if Ctype.is_moregeneral env false sch ty then printer else find remainder | (_name, Generic (path, fn)) :: remainder -> diff --git a/toplevel/native/topmain.ml b/toplevel/native/topmain.ml index 10feb68ea7..26ff8d51ef 100644 --- a/toplevel/native/topmain.ml +++ b/toplevel/native/topmain.ml @@ -13,9 +13,6 @@ (* *) (**************************************************************************) -let usage = "Usage: ocamlnat <options> <object-files> [script-file]\n\ - options are:" - let preload_objects = ref [] (* Position of the first non expanded argument *) @@ -99,17 +96,12 @@ let () = Clflags.include_dirs := List.rev_append extra_paths !Clflags.include_dirs let main () = + let ppf = Format.err_formatter in Clflags.native_code := true; - let list = ref Options.list in - begin - try - Arg.parse_and_expand_argv_dynamic current argv list file_argument usage; - with - | Arg.Bad msg -> Format.fprintf Format.err_formatter "%s%!" msg; - raise (Compenv.Exit_with_status 2) - | Arg.Help msg -> Format.fprintf Format.std_formatter "%s%!" msg; - raise (Compenv.Exit_with_status 0) - end; + let program = "ocamlnat" in + Compenv.readenv ppf Before_args; + Clflags.add_arguments __LOC__ Options.list; + Compenv.parse_arguments ~current argv file_argument program; Compmisc.read_clflags_from_env (); if not (prepare Format.err_formatter) then raise (Compenv.Exit_with_status 2); Compmisc.init_path (); diff --git a/toplevel/topdirs.ml b/toplevel/topdirs.ml index 65339d09bf..125051680b 100644 --- a/toplevel/topdirs.ml +++ b/toplevel/topdirs.ml @@ -398,7 +398,7 @@ let () = * one for exception constructors and another for * non-exception constructors (normal and extensible variants). *) let is_exception_constructor env type_expr = - Ctype.equal env true [type_expr] [Predef.type_exn] + Ctype.is_equal env true [type_expr] [Predef.type_exn] let is_extension_constructor = function | Cstr_extension _ -> true diff --git a/typing/ctype.ml b/typing/ctype.ml index 81615c4030..827b433b7f 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -19,6 +19,7 @@ open Misc open Asttypes open Types open Btype +open Errortrace open Local_store @@ -56,109 +57,46 @@ open Local_store (**** Errors ****) -module Unification_trace = struct - - type position = First | Second - let swap_position = function - | First -> Second - | Second -> First - - type desc = { t: type_expr; expanded: type_expr option } - type 'a diff = { got: 'a; expected: 'a} - - type 'a escape = - | Constructor of Path.t - | Univ of type_expr - (* The type_expr argument of [Univ] is always a [Tunivar _], - we keep a [type_expr] to track renaming in {!Printtyp} *) - | Self - | Module_type of Path.t - | Equation of 'a - - type fixed_row_case = - | Cannot_be_closed - | Cannot_add_tags of string list - - type variant = - | No_intersection - | No_tags of position * (Asttypes.label * row_field) list - | Incompatible_types_for of string - | Fixed_row of position * fixed_row_case * fixed_explanation - - - type obj = - | Missing_field of position * string - | Abstract_row of position - | Self_cannot_be_closed - - type 'a elt = - | Diff of 'a diff - | Variant of variant - | Obj of obj - | Escape of {context:type_expr option; kind: 'a escape} - | Incompatible_fields of {name:string; diff:type_expr diff } - | Rec_occur of type_expr * type_expr - - type t = desc elt list - let short t = { t; expanded = None } - let map_diff f r = - (* ordering is often meaningful when dealing with type_expr *) - let got = f r.got in - let expected = f r.expected in - { got; expected} - let diff got expected = Diff (map_diff short {got;expected}) - - let map_elt f = function - | Diff x -> Diff (map_diff f x) - | Escape {kind=Equation x; context} -> Escape {kind=Equation(f x); context} - | Rec_occur (_,_) - | Escape {kind=(Univ _ | Self|Constructor _ | Module_type _ ); _} - | Variant _ | Obj _ - | Incompatible_fields _ as x -> x - let map f = List.map (map_elt f) - - - (* Convert desc to type_expr * type_expr *) - let flatten_desc f x = match x.expanded with - | None -> f x.t x.t - | Some expanded -> f x.t expanded - let flatten f = map (flatten_desc f) - - (* Permute the expected and actual values *) - let swap_diff x = { got = x.expected; expected = x.got } - let swap_elt = function - | Diff x -> Diff (swap_diff x) - | Incompatible_fields {name;diff} -> - Incompatible_fields { name; diff = swap_diff diff} - | Obj (Missing_field(pos,s)) -> Obj(Missing_field(swap_position pos,s)) - | Obj (Abstract_row pos) -> Obj(Abstract_row (swap_position pos)) - | Variant (Fixed_row(pos,k,f)) -> Variant (Fixed_row(swap_position pos,k,f)) - | Variant (No_tags(pos,f)) -> Variant (No_tags(swap_position pos,f)) - | x -> x - let swap x = List.map swap_elt x - - exception Unify of t - - let escape kind = Escape { kind; context = None} - let scope_escape x = Unify[escape (Equation (short x))] - let rec_occur x y = Unify[Rec_occur(x, y)] - let incompatible_fields name got expected = - Incompatible_fields {name; diff={got; expected} } - - let explain trace f = - let rec explain = function - | [] -> None - | [h] -> f ~prev:None h - | h :: (prev :: _ as rem) -> - match f ~prev:(Some prev) h with - | Some _ as m -> m - | None -> explain rem in - explain (List.rev trace) - -end -module Trace = Unification_trace - -exception Unify = Trace.Unify +exception Unify of unification Errortrace.t +exception Equality of comparison Errortrace.t +exception Moregen of comparison Errortrace.t +exception Subtype of Errortrace.Subtype.t * unification Errortrace.t + +exception Escape of desc Errortrace.escape + +(* For local use: throw the appropriate exception. Can be passed into local + functions as a parameter *) +type _ trace_exn = +| Unify : unification trace_exn +| Moregen : comparison trace_exn +| Equality : comparison trace_exn + +let raise_trace_for + (type variant) + (tr_exn : variant trace_exn) + (tr : variant Errortrace.t) : 'a = + match tr_exn with + | Unify -> raise (Unify tr) + | Equality -> raise (Equality tr) + | Moregen -> raise (Moregen tr) + +(* Uses of this function are a bit suspicious, as we usually want to maintain + trace information; sometimes it makes sense, however, since we're maintaining + the trace at an outer exception handler. *) +let raise_unexplained_for tr_exn = + raise_trace_for tr_exn [] + +let raise_for tr_exn e = + raise_trace_for tr_exn [e] + +(* Thrown from [moregen_kind] *) +exception Public_method_to_private_method + +let escape kind = {kind; context = None} +let escape_exn kind = Escape (escape kind) +let scope_escape_exn ty = escape_exn (Equation (short ty)) +let raise_escape_exn kind = raise (escape_exn kind) +let raise_scope_escape_exn ty = raise (scope_escape_exn ty) exception Tags of label * label @@ -175,12 +113,18 @@ let () = | _ -> None ) -exception Subtype of Unification_trace.t * Unification_trace.t - exception Cannot_expand exception Cannot_apply +exception Cannot_subst + +exception Cannot_unify_universal_variables + +exception Matches_failure of Env.t * unification Errortrace.t + +exception Incompatible + (**** Type level management ****) let current_level = s_ref 0 @@ -790,8 +734,8 @@ let rec generalize_spine ty = List.iter generalize_spine tyl | _ -> () -let forward_try_expand_once = (* Forward declaration *) - ref (fun _env _ty -> raise Cannot_expand) +let forward_try_expand_safe = (* Forward declaration *) + ref (fun _env _ty -> assert false) (* Lower the levels of a type (assume [level] is not @@ -819,18 +763,18 @@ let rec check_scope_escape env level ty = let orig_level = ty.level in if try_logged_mark_node ty then begin if level < ty.scope then - raise(Trace.scope_escape ty); + raise_scope_escape_exn ty; begin match ty.desc with | Tconstr (p, _, _) when level < Path.scope p -> - begin match !forward_try_expand_once env ty with + begin match !forward_try_expand_safe env ty with | ty' -> check_scope_escape env level ty' | exception Cannot_expand -> - raise Trace.(Unify [escape (Constructor p)]) + raise_escape_exn (Constructor p) end | Tpackage (p, fl) when level < Path.scope p -> let p' = normalize_package_path env p in - if Path.same p p' then raise Trace.(Unify [escape (Module_type p)]); + if Path.same p p' then raise_escape_exn (Module_type p); check_scope_escape env level (Btype.newty2 orig_level (Tpackage (p', fl))) | _ -> @@ -841,18 +785,24 @@ let rec check_scope_escape env level ty = let check_scope_escape env level ty = let snap = snapshot () in try check_scope_escape env level ty; backtrack snap - with Unify [Trace.Escape x] -> + with Escape e -> backtrack snap; - raise Trace.(Unify[Escape { x with context = Some ty }]) + raise (Escape { e with context = Some ty }) let rec update_scope scope ty = let ty = repr ty in if ty.scope < scope then begin - if ty.level < scope then raise (Trace.scope_escape ty); - set_scope ty scope; - iter_type_expr (update_scope scope) ty + if ty.level < scope then raise_scope_escape_exn ty; + set_scope ty scope; + (* Only recurse in principal mode as this is not necessary for soundness *) + if !Clflags.principal then iter_type_expr (update_scope scope) ty end +let update_scope_for tr_exn scope ty = + try + update_scope scope ty + with Escape e -> raise_for tr_exn (Escape e) + (* Note: the level of a type constructor must be greater than its binding time. That way, a type constructor cannot escape the scope of its definition, as would be the case in @@ -864,15 +814,15 @@ let rec update_scope scope ty = let rec update_level env level expand ty = let ty = repr ty in if ty.level > level then begin - if level < ty.scope then raise (Trace.scope_escape ty); + if level < ty.scope then raise_scope_escape_exn ty; match ty.desc with Tconstr(p, _tl, _abbrev) when level < Path.scope p -> (* Try first to replace an abbreviation by its expansion. *) begin try - link_type ty (!forward_try_expand_once env ty); + link_type ty (!forward_try_expand_safe env ty); update_level env level expand ty with Cannot_expand -> - raise Trace.(Unify [escape(Constructor p)]) + raise_escape_exn (Constructor p) end | Tconstr(p, (_ :: _ as tl), _) -> let variance = @@ -886,7 +836,7 @@ let rec update_level env level expand ty = in begin try if not needs_expand then raise Cannot_expand; - link_type ty (!forward_try_expand_once env ty); + link_type ty (!forward_try_expand_safe env ty); update_level env level expand ty with Cannot_expand -> set_level ty level; @@ -894,7 +844,7 @@ let rec update_level env level expand ty = end | Tpackage (p, fl) when level < Path.scope p -> let p' = normalize_package_path env p in - if Path.same p p' then raise Trace.(Unify [escape (Module_type p)]); + if Path.same p p' then raise_escape_exn (Module_type p); set_type_desc ty (Tpackage (p', fl)); update_level env level expand ty | Tobject(_, ({contents=Some(p, _tl)} as nm)) @@ -912,7 +862,7 @@ let rec update_level env level expand ty = iter_type_expr (update_level env level expand) ty | Tfield(lab, _, ty1, _) when lab = dummy_method && (repr ty1).level > level -> - raise Trace.(Unify [escape Self]) + raise_escape_exn Self | _ -> set_level ty level; (* XXX what about abbreviations in Tconstr ? *) @@ -927,11 +877,16 @@ let update_level env level ty = let snap = snapshot () in try update_level env level false ty - with Unify _ -> + with Escape _ -> backtrack snap; update_level env level true ty end +let update_level_for tr_exn env level ty = + try + update_level env level ty + with Escape e -> raise_for tr_exn (Escape e) + (* Lower level of type variables inside contravariant branches *) let rec lower_contravariant env var_level visited contra ty = @@ -969,7 +924,7 @@ let rec lower_contravariant env var_level visited contra ty = else lower_rec contra t) variance tyl in if maybe_expand then (* we expand cautiously to avoid missing cmis *) - match !forward_try_expand_once env ty with + match !forward_try_expand_safe env ty with | ty -> lower_rec contra ty | exception Cannot_expand -> not_expanded () else not_expanded () @@ -1513,32 +1468,36 @@ let instance_label fixed lbl = (**** Instantiation with parameter substitution ****) let unify' = (* Forward declaration *) - ref (fun _env _ty1 _ty2 -> raise (Unify [])) + ref (fun _env _ty1 _ty2 -> assert false) + let subst env level priv abbrev ty params args body = - if List.length params <> List.length args then raise (Unify []); + if List.length params <> List.length args then raise Cannot_subst; let old_level = !current_level in current_level := level; - try - let body0 = newvar () in (* Stub *) - begin match ty with - None -> () + let body0 = newvar () in (* Stub *) + let undo_abbrev = + match ty with + | None -> fun () -> () (* No abbreviation added *) | Some ({desc = Tconstr (path, tl, _)} as ty) -> let abbrev = proper_abbrevs path tl abbrev in - memorize_abbrev abbrev priv path ty body0 + memorize_abbrev abbrev priv path ty body0; + fun () -> forget_abbrev abbrev path | _ -> assert false - end; - abbreviations := abbrev; - let (params', body') = instance_parameterized_type params body in - abbreviations := ref Mnil; + in + abbreviations := abbrev; + let (params', body') = instance_parameterized_type params body in + abbreviations := ref Mnil; + try !unify' env body0 body'; List.iter2 (!unify' env) params' args; current_level := old_level; body' - with Unify _ as exn -> + with Unify _ -> current_level := old_level; - raise exn + undo_abbrev (); + raise Cannot_subst (* Only the shape of the type matters, not whether it is generic or @@ -1550,7 +1509,7 @@ let apply env params body args = try subst env generic_level Public (ref Mnil) None params args body with - Unify _ -> raise Cannot_apply + Cannot_subst -> raise Cannot_apply let () = Subst.ctype_apply_env_empty := apply Env.empty @@ -1604,7 +1563,7 @@ let expand_abbrev_gen kind find_type_expansion env ty = if level <> generic_level then begin try update_level env level ty' - with Unify _ -> + with Escape _ -> (* XXX This should not happen. However, levels are not correctly restored after a typing error *) @@ -1612,7 +1571,7 @@ let expand_abbrev_gen kind find_type_expansion env ty = end; begin try update_scope scope ty'; - with Unify _ -> + with Escape _ -> (* XXX This should not happen. However, levels are not correctly restored after a typing error *) @@ -1631,7 +1590,11 @@ let expand_abbrev_gen kind find_type_expansion env ty = | (params, body, lv) -> (* prerr_endline ("add a "^string_of_kind kind^" expansion for "^Path.name path);*) - let ty' = subst env level kind abbrev (Some ty) params args body in + let ty' = + try + subst env level kind abbrev (Some ty) params args body + with Cannot_subst -> raise_escape_exn Constraint + in (* For gadts, remember type as non exportable *) (* The ambiguous level registered for ty' should be the highest *) (* if !trace_gadt_instances then begin *) @@ -1649,7 +1612,9 @@ let expand_abbrev env ty = (* Expand once the head of a type *) let expand_head_once env ty = - try expand_abbrev env (repr ty) with Cannot_expand -> assert false + try + expand_abbrev env (repr ty) + with Cannot_expand | Escape _ -> assert false (* Check whether a type can be expanded *) let safe_abbrev env ty = @@ -1658,14 +1623,14 @@ let safe_abbrev env ty = Cannot_expand -> Btype.backtrack snap; false - | Unify _ -> + | Escape _ -> Btype.backtrack snap; cleanup_abbrev (); false (* Expand the head of a type once. Raise Cannot_expand if the type cannot be expanded. - May raise Unify, if a recursion was hidden in the type. *) + May raise Escape, if a recursion was hidden in the type. *) let try_expand_once env ty = let ty = repr ty in match ty.desc with @@ -1676,7 +1641,7 @@ let try_expand_once env ty = let try_expand_safe env ty = let snap = Btype.snapshot () in try try_expand_once env ty - with Unify _ -> + with Escape _ -> Btype.backtrack snap; cleanup_abbrev (); raise Cannot_expand (* Fully expand the head of a type. *) @@ -1685,15 +1650,19 @@ let rec try_expand_head try_once env ty = try try_expand_head try_once env ty' with Cannot_expand -> ty' -(* Unsafe full expansion, may raise Unify. *) +(* Unsafe full expansion, may raise [Unify [Escape _]]. *) let expand_head_unif env ty = - try try_expand_head try_expand_once env ty with Cannot_expand -> repr ty + try + try_expand_head try_expand_once env ty + with + | Cannot_expand -> repr ty + | Escape e -> raise_for Unify (Escape e) (* Safe version of expand_head, never fails *) let expand_head env ty = try try_expand_head try_expand_safe env ty with Cannot_expand -> repr ty -let _ = forward_try_expand_once := try_expand_safe +let _ = forward_try_expand_safe := try_expand_safe (* Expand until we find a non-abstract type declaration, @@ -1721,8 +1690,15 @@ let rec extract_concrete_typedecl env ty = normally hidden to the type-checker out of the implementation module of the private abbreviation. *) -let expand_abbrev_opt = - expand_abbrev_gen Private Env.find_type_expansion_opt +let expand_abbrev_opt env ty = + expand_abbrev_gen Private Env.find_type_expansion_opt env ty + +let safe_abbrev_opt env ty = + let snap = Btype.snapshot () in + try ignore (expand_abbrev_opt env ty); true + with Cannot_expand | Escape _ -> + Btype.backtrack snap; + false let try_expand_once_opt env ty = let ty = repr ty in @@ -1730,23 +1706,20 @@ let try_expand_once_opt env ty = Tconstr _ -> repr (expand_abbrev_opt env ty) | _ -> raise Cannot_expand -let rec try_expand_head_opt env ty = - let ty' = try_expand_once_opt env ty in - begin try - try_expand_head_opt env ty' - with Cannot_expand -> - ty' - end +let try_expand_safe_opt env ty = + let snap = Btype.snapshot () in + try try_expand_once_opt env ty + with Escape _ -> + Btype.backtrack snap; raise Cannot_expand let expand_head_opt env ty = - let snap = Btype.snapshot () in - try try_expand_head_opt env ty - with Cannot_expand | Unify _ -> (* expand_head shall never fail *) - Btype.backtrack snap; - repr ty + try try_expand_head try_expand_safe_opt env ty with Cannot_expand -> repr ty (* Recursively expand the head of a type. - Also expand #-types. *) + Also expand #-types. + + Error printing relies on [full_expand] returning exactly its input (i.e., a + physically equal type) when nothing changes. *) let full_expand ~may_forget_scope env ty = let ty = if may_forget_scope then @@ -1755,7 +1728,12 @@ let full_expand ~may_forget_scope env ty = (* #10277: forget scopes when printing trace *) begin_def (); init_def ty.level; - let ty = expand_head env (correct_levels ty) in + let ty = + (* The same as [expand_head], except in the failing case we return the + *original* type, not [correct_levels ty].*) + try try_expand_head try_expand_safe env (correct_levels ty) with + | Cannot_expand -> repr ty + in end_def (); ty else expand_head env ty @@ -1849,12 +1827,15 @@ let occur env ty0 ty = merge type_changed old with exn -> merge type_changed old; - match exn with - | Occur -> raise (Trace.rec_occur ty0 ty) - | _ -> raise exn + raise exn + +let occur_for tr_exn env t1 t2 = + try + occur env t1 t2 + with Occur -> raise_for tr_exn (Rec_occur(t1, t2)) let occur_in env ty0 t = - try occur env ty0 t; false with Unify _ -> true + try occur env ty0 t; false with Occur -> true (* Check that a local constraint is well-founded *) (* PR#6405: not needed since we allow recursion and work on normalized types *) @@ -1873,7 +1854,7 @@ let rec local_non_recursive_abbrev ~allow_rec strict visited env p ty = begin try (* try expanding, since [p] could be hidden *) local_non_recursive_abbrev ~allow_rec strict visited env p - (try_expand_head try_expand_once_opt env ty) + (try_expand_head try_expand_safe_opt env ty) with Cannot_expand -> let params = try (Env.find_type p' env).type_params @@ -1927,9 +1908,15 @@ let rec unify_univar t1 t2 = function | None, None -> unify_univar t1 t2 rem | _ -> - raise (Unify []) + raise Cannot_unify_universal_variables end - | [] -> raise (Unify []) + | [] -> raise Cannot_unify_universal_variables + +(* The same as [unify_univar], but raises the appropriate exception instead of + [Cannot_unify_universal_variables] *) +let unify_univar_for tr_exn t1 t2 univar_pairs = + try unify_univar t1 t2 univar_pairs + with Cannot_unify_universal_variables -> raise_unexplained_for tr_exn (* Test the occurrence of free univars in a type *) (* That's way too expensive. Must do some kind of caching *) @@ -1954,7 +1941,7 @@ let occur_univar ?(inj_only=false) env ty = match ty.desc with Tunivar _ -> if not (TypeSet.mem ty bound) then - raise Trace.(Unify [escape (Univ ty)]) + raise_escape_exn (Univ ty) | Tpoly (ty, tyl) -> let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in occur_rec bound ty @@ -1985,9 +1972,14 @@ let occur_univar ?(inj_only=false) env ty = ~always:(fun () -> unmark_type ty) let has_free_univars env ty = - try occur_univar ~inj_only:false env ty; false with Unify _ -> true + try occur_univar ~inj_only:false env ty; false with Escape _ -> true let has_injective_univars env ty = - try occur_univar ~inj_only:true env ty; false with Unify _ -> true + try occur_univar ~inj_only:true env ty; false with Escape _ -> true + +let occur_univar_for tr_exn env ty = + try + occur_univar env ty + with Escape e -> raise_for tr_exn (Escape e) (* Grouping univars by families according to their binders *) let add_univars = @@ -2017,8 +2009,7 @@ let univars_escape env univar_pairs vl ty = Tpoly (t, tl) -> if List.exists (fun t -> TypeSet.mem (repr t) family) tl then () else occur t - | Tunivar _ -> - if TypeSet.mem t family then raise Trace.(Unify [escape(Univ t)]) + | Tunivar _ -> if TypeSet.mem t family then raise_escape_exn (Univ t) | Tconstr (_, [], _) -> () | Tconstr (p, tl, _) -> begin try @@ -2054,6 +2045,11 @@ let enter_poly env univar_pairs t1 tl1 t2 tl2 f = Misc.try_finally (fun () -> f t1 t2) ~always:(fun () -> univar_pairs := old_univars) +let enter_poly_for tr_exn env univar_pairs t1 tl1 t2 tl2 f = + try + enter_poly env univar_pairs t1 tl1 t2 tl2 f + with Escape e -> raise_for tr_exn (Escape e) + let univar_pairs = ref [] (**** Instantiate a generic type into a poly type ***) @@ -2101,16 +2097,19 @@ let rec has_cached_expansion p abbrev = (**** Transform error trace ****) (* +++ Move it to some other place ? *) -let expand_trace env trace = - let expand_desc x = - let open Trace in - match x.expanded with +let expand_any_trace map env trace = + let expand_desc x = match x.Errortrace.expanded with | None -> - let expanded = full_expand ~may_forget_scope:true env x.t in - { t = repr x.t; expanded = Some expanded } - | Some _ -> x - in - Unification_trace.map expand_desc trace + let expanded = full_expand ~may_forget_scope:true env x.t in + Errortrace.{ t = repr x.t; expanded = Some expanded } + | Some _ -> x in + map expand_desc trace + +let expand_trace env trace = + expand_any_trace Errortrace.map env trace + +let expand_subtype_trace env trace = + expand_any_trace Subtype.map env trace (**** Unification ****) @@ -2162,7 +2161,7 @@ let reify env t = let path, t = create_fresh_constr ty.level o in link_type ty t; if ty.level < fresh_constr_scope then - raise Trace.(Unify [escape (Constructor path)]) + raise_for Unify (Escape (escape (Constructor path))) | Tvariant r -> let r = row_repr r in if not (static_row r) then begin @@ -2176,7 +2175,7 @@ let reify env t = {r with row_fields=[]; row_fixed; row_more = t} in link_type m (newty2 m.level (Tvariant row)); if m.level < fresh_constr_scope then - raise Trace.(Unify [escape (Constructor path)]) + raise_for Unify (Escape (escape (Constructor path))) | _ -> assert false end; iter_row iterator r @@ -2225,11 +2224,16 @@ let rec expands_to_datatype env ty = Tconstr (p, _, _) -> begin try is_datatype (Env.find_type p env) || - expands_to_datatype env (try_expand_once env ty) + expands_to_datatype env (try_expand_safe env ty) with Not_found | Cannot_expand -> false end | _ -> false +(* [mcomp] tests if two types are "compatible" -- i.e., if they could ever + unify. (This is distinct from [eqtype], which checks if two types *are* + exactly the same.) This is used to decide whether GADT cases are + unreachable. It is broadly part of unification. *) + (* mcomp type_pairs subst env t1 t2 does not raise an exception if it is possible that t1 and t2 are actually equal, assuming the types in type_pairs are equal and @@ -2277,7 +2281,8 @@ let rec mcomp type_pairs env t1 t2 = | (Tconstr (p, _, _), _) | (_, Tconstr (p, _, _)) -> begin try let decl = Env.find_type p env in - if non_aliasable p decl || is_datatype decl then raise (Unify []) + if non_aliasable p decl || is_datatype decl then + raise Incompatible with Not_found -> () end (* @@ -2296,17 +2301,20 @@ let rec mcomp type_pairs env t1 t2 = | (Tpoly (t1, []), Tpoly (t2, [])) -> mcomp type_pairs env t1 t2 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) -> - enter_poly env univar_pairs t1 tl1 t2 tl2 - (mcomp type_pairs env) + (try + enter_poly env univar_pairs + t1 tl1 t2 tl2 (mcomp type_pairs env) + with Escape _ -> raise Incompatible) | (Tunivar _, Tunivar _) -> - unify_univar t1' t2' !univar_pairs + (try unify_univar t1' t2' !univar_pairs + with Cannot_unify_universal_variables -> raise Incompatible) | (_, _) -> - raise (Unify []) + raise Incompatible end and mcomp_list type_pairs env tl1 tl2 = if List.length tl1 <> List.length tl2 then - raise (Unify []); + raise Incompatible; List.iter2 (mcomp type_pairs env) tl1 tl2 and mcomp_fields type_pairs env ty1 ty2 = @@ -2318,7 +2326,7 @@ and mcomp_fields type_pairs env ty1 ty2 = List.exists (fun (_, k, _) -> field_kind_repr k = Fpresent) in mcomp type_pairs env rest1 rest2; if has_present miss1 && (object_row ty2).desc = Tnil - || has_present miss2 && (object_row ty1).desc = Tnil then raise (Unify []); + || has_present miss2 && (object_row ty1).desc = Tnil then raise Incompatible; List.iter (function (_n, k1, t1, k2, t2) -> mcomp_kind k1 k2; @@ -2330,7 +2338,7 @@ and mcomp_kind k1 k2 = let k2 = field_kind_repr k2 in match k1, k2 with (Fpresent, Fabsent) - | (Fabsent, Fpresent) -> raise (Unify []) + | (Fabsent, Fpresent) -> raise Incompatible | _ -> () and mcomp_row type_pairs env row1 row2 = @@ -2342,7 +2350,7 @@ and mcomp_row type_pairs env row1 row2 = | Rabsent | Reither _ -> false in if row1.row_closed && List.exists cannot_erase r2 - || row2.row_closed && List.exists cannot_erase r1 then raise (Unify []); + || row2.row_closed && List.exists cannot_erase r1 then raise Incompatible; List.iter (fun (_,f1,f2) -> match row_field_repr f1, row_field_repr f2 with @@ -2350,7 +2358,7 @@ and mcomp_row type_pairs env row1 row2 = | Rpresent (Some _), (Rpresent None | Reither (true, _, _, _) | Rabsent) | (Reither (_, _::_, _, _) | Rabsent), Rpresent None | (Reither (true, _, _, _) | Rabsent), Rpresent (Some _) -> - raise (Unify []) + raise Incompatible | Rpresent(Some t1), Rpresent(Some t2) -> mcomp type_pairs env t1 t2 | Rpresent(Some t1), Reither(false, tl2, _, _) -> @@ -2373,7 +2381,7 @@ and mcomp_type_decl type_pairs env p1 p2 tl1 tl2 = (fun i (t1,t2) -> if i then mcomp type_pairs env t1 t2) inj (List.combine tl1 tl2) end else if non_aliasable p1 decl && non_aliasable p2 decl' then - raise (Unify []) + raise Incompatible else match decl.type_kind, decl'.type_kind with | Type_record (lst,r), Type_record (lst',r') when r = r' -> @@ -2387,14 +2395,14 @@ and mcomp_type_decl type_pairs env p1 p2 tl1 tl2 = | Type_abstract, Type_abstract -> () | Type_abstract, _ when not (non_aliasable p1 decl)-> () | _, Type_abstract when not (non_aliasable p2 decl') -> () - | _ -> raise (Unify []) + | _ -> raise Incompatible with Not_found -> () and mcomp_type_option type_pairs env t t' = match t, t' with None, None -> () | Some t, Some t' -> mcomp type_pairs env t t' - | _ -> raise (Unify []) + | _ -> raise Incompatible and mcomp_variant_description type_pairs env xs ys = let rec iter = fun x y -> @@ -2405,13 +2413,13 @@ and mcomp_variant_description type_pairs env xs ys = | Cstr_tuple l1, Cstr_tuple l2 -> mcomp_list type_pairs env l1 l2 | Cstr_record l1, Cstr_record l2 -> mcomp_record_description type_pairs env l1 l2 - | _ -> raise (Unify []) + | _ -> raise Incompatible end; if Ident.name c1.cd_id = Ident.name c2.cd_id then iter xs ys - else raise (Unify []) + else raise Incompatible | [],[] -> () - | _ -> raise (Unify []) + | _ -> raise Incompatible in iter xs ys @@ -2423,15 +2431,20 @@ and mcomp_record_description type_pairs env = if Ident.name l1.ld_id = Ident.name l2.ld_id && l1.ld_mutable = l2.ld_mutable then iter xs ys - else raise (Unify []) + else raise Incompatible | [], [] -> () - | _ -> raise (Unify []) + | _ -> raise Incompatible in iter let mcomp env t1 t2 = mcomp (TypePairs.create 4) env t1 t2 +let mcomp_for tr_exn env t1 t2 = + try + mcomp env t1 t2 + with Incompatible -> raise_unexplained_for tr_exn + (* Real unification *) let find_lowest_level ty = @@ -2565,11 +2578,16 @@ let unify_eq t1 t2 = let unify1_var env t1 t2 = assert (is_Tvar t1); - occur env t1 t2; - match occur_univar env t2 with + occur_for Unify env t1 t2; + match occur_univar_for Unify env t2 with | () -> - update_level env t1.level t2; - update_scope t1.scope t2; + begin + try + update_level env t1.level t2; + update_scope t1.scope t2 + with Escape e -> + raise_for Unify (Escape e) + end; link_type t1 t2; true | exception Unify _ when !umode = Pattern -> @@ -2583,8 +2601,8 @@ let record_equation t1 t2 = (* Called from unify3 *) let unify3_var env t1' t2 t2' = - occur !env t1' t2; - match occur_univar !env t2 with + occur_for Unify !env t1' t2; + match occur_univar_for Unify !env t2 with | () -> link_type t1' t2 | exception Unify _ when !umode = Pattern -> reify env t1'; @@ -2638,9 +2656,9 @@ let rec unify (env:Env.t ref) t1 t2 = | (_, Tvar _) -> if unify1_var !env t2 t1 then () else unify2 env t1 t2 | (Tunivar _, Tunivar _) -> - unify_univar t1 t2 !univar_pairs; - update_level !env t1.level t2; - update_scope t1.scope t2; + unify_univar_for Unify t1 t2 !univar_pairs; + update_level_for Unify !env t1.level t2; + update_scope_for Unify t1.scope t2; link_type t1 t2 | (Tconstr (p1, [], a1), Tconstr (p2, [], a2)) when Path.same p1 p2 (* && actual_mode !env = Old *) @@ -2649,8 +2667,8 @@ let rec unify (env:Env.t ref) t1 t2 = when any of the types has a cached expansion. *) && not (has_cached_expansion p1 !a1 || has_cached_expansion p2 !a2) -> - update_level !env t1.level t2; - update_scope t1.scope t2; + update_level_for Unify !env t1.level t2; + update_scope_for Unify t1.scope t2; link_type t1 t2 | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Env.has_local_constraints !env @@ -2658,9 +2676,9 @@ let rec unify (env:Env.t ref) t1 t2 = (* Do not use local constraints more than necessary *) begin try if find_expansion_scope !env p1 > find_expansion_scope !env p2 then - unify env t1 (try_expand_once !env t2) + unify env t1 (try_expand_safe !env t2) else - unify env (try_expand_once !env t1) t2 + unify env (try_expand_safe !env t1) t2 with Cannot_expand -> unify2 env t1 t2 end @@ -2670,7 +2688,7 @@ let rec unify (env:Env.t ref) t1 t2 = reset_trace_gadt_instances reset_tracing; with Unify trace -> reset_trace_gadt_instances reset_tracing; - raise( Unify (Trace.diff t1 t2 :: trace) ) + raise( Unify (Errortrace.diff t1 t2 :: trace) ) and unify2 env t1 t2 = (* Second step: expansion of abbreviations *) @@ -2681,10 +2699,10 @@ and unify2 env t1 t2 = let t2' = expand_head_unif !env t2 in let lv = min t1'.level t2'.level in let scope = max t1'.scope t2'.scope in - update_level !env lv t2; - update_level !env lv t1; - update_scope scope t2; - update_scope scope t1; + update_level_for Unify !env lv t2; + update_level_for Unify !env lv t1; + update_scope_for Unify scope t2; + update_scope_for Unify scope t1; if unify_eq t1' t2' then () else let t1 = repr t1 and t2 = repr t2 in @@ -2701,7 +2719,7 @@ and unify2 env t1 t2 = unify3 env t1 t1' t2 t2' else try unify3 env t2 t2' t1 t1' with Unify trace -> - raise (Unify (Trace.swap trace)) + raise_trace_for Unify (swap_trace trace) and unify3 env t1 t1' t2 t2' = (* Third step: truly unification *) @@ -2711,7 +2729,7 @@ and unify3 env t1 t1' t2 t2' = begin match (d1, d2) with (* handle vars and univars specially *) (Tunivar _, Tunivar _) -> - unify_univar t1' t2' !univar_pairs; + unify_univar_for Unify t1' t2' !univar_pairs; link_type t1' t2' | (Tvar _, _) -> unify3_var env t1' t2 t2' @@ -2722,7 +2740,7 @@ and unify3 env t1 t1' t2 t2' = | _ -> begin match !umode with | Expression -> - occur !env t1' t2'; + occur_for Unify !env t1' t2'; if is_self_type d1 (* PR#7711: do not abbreviate self type *) then link_type t1' t2' else link_type t1' t2 @@ -2750,7 +2768,8 @@ and unify3 env t1 t1' t2 t2' = ~allow_recursive:!allow_recursive_equation (fun () -> unify_list env tl1 tl2) else if in_current_module p1 (* || in_pervasives p1 *) - || List.exists (expands_to_datatype !env) [t1'; t1; t2] then + || List.exists (expands_to_datatype !env) [t1'; t1; t2] + then unify_list env tl1 tl2 else let inj = @@ -2767,7 +2786,8 @@ and unify3 env t1 t1' t2 t2' = let snap = snapshot () in try unify env t1 t2 with Unify _ -> backtrack snap; - reify env t1; reify env t2 + reify env t1; + reify env t2 end) inj (List.combine tl1 tl2) | (Tconstr (path,[],_), @@ -2795,7 +2815,7 @@ and unify3 env t1 t1' t2 t2' = reify env t1'; reify env t2'; if can_generate_equations () then ( - mcomp !env t1' t2'; + mcomp_for Unify !env t1' t2'; record_equation t1' t2' ) | (Tobject (fi1, nm1), Tobject (fi2, _)) -> @@ -2820,7 +2840,7 @@ and unify3 env t1 t1' t2 t2' = reify env t1'; reify env t2'; if can_generate_equations () then ( - mcomp !env t1' t2'; + mcomp_for Unify !env t1' t2'; record_equation t1' t2' ) end @@ -2832,30 +2852,32 @@ and unify3 env t1 t1' t2 t2' = else unify env (newty2 rem.level Tnil) rem | _ -> if f = dummy_method then - raise (Unify Trace.[Obj Self_cannot_be_closed]) + raise_for Unify (Obj Self_cannot_be_closed) else if d1 = Tnil then - raise (Unify Trace.[Obj(Missing_field (First, f))]) + raise_for Unify (Obj (Missing_field(First, f))) else - raise (Unify Trace.[Obj(Missing_field (Second, f))]) + raise_for Unify (Obj (Missing_field(Second, f))) end | (Tnil, Tnil) -> () | (Tpoly (t1, []), Tpoly (t2, [])) -> unify env t1 t2 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) -> - enter_poly !env univar_pairs t1 tl1 t2 tl2 (unify env) + enter_poly_for Unify !env univar_pairs t1 tl1 t2 tl2 (unify env) | (Tpackage (p1, fl1), Tpackage (p2, fl2)) -> begin try unify_package !env (unify_list env) t1.level p1 fl1 t2.level p2 fl2 with Not_found -> - if !umode = Expression then raise (Unify []); + if !umode = Expression then raise_unexplained_for Unify; List.iter (fun (_n, ty) -> reify env ty) (fl1 @ fl2); (* if !generate_equations then List.iter2 (mcomp !env) tl1 tl2 *) end - | (Tnil, Tconstr _ ) -> raise (Unify Trace.[Obj(Abstract_row Second)]) - | (Tconstr _, Tnil ) -> raise (Unify Trace.[Obj(Abstract_row First)]) - | (_, _) -> raise (Unify []) + | (Tnil, Tconstr _ ) -> + raise (Unify Errortrace.[Obj(Abstract_row Second)]) + | (Tconstr _, Tnil ) -> + raise (Unify Errortrace.[Obj(Abstract_row First)]) + | (_, _) -> raise_unexplained_for Unify end; (* XXX Commentaires + changer "create_recursion" ||| Comments + change "create_recursion" *) @@ -2870,12 +2892,12 @@ and unify3 env t1 t1' t2 t2' = () (* t2 has already been expanded by update_level *) with Unify trace -> Private_type_expr.set_desc t1' d1; - raise (Unify trace) + raise_trace_for Unify trace end and unify_list env tl1 tl2 = if List.length tl1 <> List.length tl2 then - raise (Unify []); + raise_unexplained_for Unify; List.iter2 (unify env) tl1 tl2 (* Build a fresh row variable for unification *) @@ -2913,12 +2935,12 @@ and unify_fields env ty1 ty2 = (* Optimization *) unify_kind k1 k2; try if !trace_gadt_instances then begin - update_level !env va.level t1; - update_scope va.scope t1 + update_level_for Unify !env va.level t1; + update_scope_for Unify va.scope t1 end; unify env t1 t2 with Unify trace -> - raise( Unify (Trace.incompatible_fields n t1 t2 :: trace) ) + raise( Unify (Errortrace.incompatible_fields n t1 t2 :: trace) ) ) pairs with exn -> @@ -2974,7 +2996,7 @@ and unify_row env row1 row2 = (fun (_,f1,f2) -> row_field_repr f1 = Rabsent || row_field_repr f2 = Rabsent) pairs - then raise Trace.( Unify [Variant No_intersection] ); + then raise_for Unify (Variant No_intersection); let name = if row1.row_name <> None && (row1.row_closed || empty r2) && (not row2.row_closed || keep (fun f1 f2 -> f1, f2) && empty r1) @@ -2994,28 +3016,28 @@ and unify_row env row1 row2 = begin match fixed_explanation row with | None -> if rest <> [] && row.row_closed then - let pos = if row == row1 then Trace.First else Trace.Second in - raise Trace.(Unify [Variant (No_tags(pos,rest))]) + let pos = if row == row1 then First else Second in + raise_for Unify (Variant (No_tags(pos,rest))) | Some fixed -> - let pos = if row == row1 then Trace.First else Trace.Second in + let pos = if row == row1 then First else Second in if closed && not row.row_closed then - raise Trace.(Unify [Variant(Fixed_row(pos,Cannot_be_closed,fixed))]) + raise_for Unify (Variant (Fixed_row(pos,Cannot_be_closed,fixed))) else if rest <> [] then - let case = Trace.Cannot_add_tags (List.map fst rest) in - raise Trace.(Unify [Variant(Fixed_row(pos,case,fixed))]) + let case = Cannot_add_tags (List.map fst rest) in + raise_for Unify (Variant (Fixed_row(pos,case,fixed))) end; (* The following test is not principal... should rather use Tnil *) let rm = row_more row in (*if !trace_gadt_instances && rm.desc = Tnil then () else*) if !trace_gadt_instances then - update_level !env rm.level (newgenty (Tvariant row)); + update_level_for Unify !env rm.level (newgenty (Tvariant row)); if row_fixed row then if more == rm then () else if is_Tvar rm then link_type rm more else unify env rm more else let ty = newgenty (Tvariant {row0 with row_fields = rest}) in - update_level !env rm.level ty; - update_scope rm.scope ty; + update_level_for Unify !env rm.level ty; + update_scope_for Unify rm.scope ty; link_type rm ty in let md1 = rm1.desc and md2 = rm2.desc in @@ -3026,7 +3048,7 @@ and unify_row env row1 row2 = (fun (l,f1,f2) -> try unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2 with Unify trace -> - raise Trace.( Unify( Variant (Incompatible_types_for l) :: trace )) + raise_trace_for Unify (Variant (Incompatible_types_for l) :: trace) ) pairs; if static_row row1 then begin @@ -3043,9 +3065,9 @@ and unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2 = match fixed with | None -> f () | Some fix -> - let tr = Trace.[ Variant (Fixed_row (pos,Cannot_add_tags [l],fix)) ] in - raise (Unify tr) in - let first = Trace.First, fixed1 and second = Trace.Second, fixed2 in + let tr = [Variant(Fixed_row(pos,Cannot_add_tags [l],fix))] in + raise_trace_for Unify tr in + let first = First, fixed1 and second = Second, fixed2 in let either_fixed = match fixed1, fixed2 with | None, None -> false | _ -> true in @@ -3067,7 +3089,7 @@ and unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2 = !rigid_variants && (List.length tl1 = 1 || List.length tl2 = 1)) && begin match tl1 @ tl2 with [] -> false | t1 :: tl -> - if c1 || c2 then raise (Unify []); + if c1 || c2 then raise_unexplained_for Unify; List.iter (unify env t1) tl; !e1 <> None || !e2 <> None end in @@ -3086,18 +3108,19 @@ and unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2 = | (tu1::tlu1), _ :: _ -> (* Attempt to merge all the types containing univars *) List.iter (unify env tu1) (tlu1@tlu2) - | (tu::_, []) | ([], tu::_) -> occur_univar !env tu + | (tu::_, []) | ([], tu::_) -> + occur_univar_for Unify !env tu end; (* Is this handling of levels really principal? *) List.iter (fun ty -> let rm = repr rm2 in - update_level !env rm.level ty; - update_scope rm.scope ty; + update_level_for Unify !env rm.level ty; + update_scope_for Unify rm.scope ty; ) tl1'; List.iter (fun ty -> let rm = repr rm1 in - update_level !env rm.level ty; - update_scope rm.scope ty; + update_level_for Unify !env rm.level ty; + update_scope_for Unify rm.scope ty; ) tl2'; let e = ref None in let f1' = Reither(c1 || c2, tl2', m1 || m2, e) @@ -3112,8 +3135,8 @@ and unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2 = if_not_fixed first (fun () -> set_row_field e1 f2; let rm = repr rm1 in - update_level !env rm.level t2; - update_scope rm.scope t2; + update_level_for Unify !env rm.level t2; + update_scope_for Unify rm.scope t2; (try List.iter (fun t1 -> unify env t1 t2) tl with exn -> e1 := None; raise exn) ) @@ -3121,8 +3144,8 @@ and unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2 = if_not_fixed second (fun () -> set_row_field e2 f1; let rm = repr rm2 in - update_level !env rm.level t1; - update_scope rm.scope t1; + update_level_for Unify !env rm.level t1; + update_scope_for Unify rm.scope t1; (try List.iter (unify env t1) tl with exn -> e2 := None; raise exn) ) @@ -3130,7 +3153,7 @@ and unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2 = if_not_fixed first (fun () -> set_row_field e1 f2) | Rpresent None, Reither(true, [], _, e2) -> if_not_fixed second (fun () -> set_row_field e2 f1) - | _ -> raise (Unify []) + | _ -> raise_unexplained_for Unify let unify env ty1 ty2 = let snap = Btype.snapshot () in @@ -3168,15 +3191,17 @@ let unify_var env t1 t2 = | Tvar _, _ -> let reset_tracing = check_trace_gadt_instances env in begin try - occur env t1 t2; - update_level env t1.level t2; - update_scope t1.scope t2; + occur_for Unify env t1 t2; + update_level_for Unify env t1.level t2; + update_scope_for Unify t1.scope t2; link_type t1 t2; reset_trace_gadt_instances reset_tracing; with Unify trace -> reset_trace_gadt_instances reset_tracing; - let expanded_trace = expand_trace env @@ Trace.diff t1 t2 :: trace in - raise (Unify expanded_trace) + let expanded_trace = + expand_trace env @@ Errortrace.diff t1 t2 :: trace + in + raise_trace_for Unify expanded_trace end | _ -> unify (ref env) t1 t2 @@ -3220,7 +3245,7 @@ let filter_arrow env t l = when l = l' || !Clflags.classic && l = Nolabel && not (is_optional l') -> (t1, t2) | _ -> - raise (Unify []) + raise_unexplained_for Unify (* Used by [filter_method]. *) let rec filter_method_field env name priv ty = @@ -3247,7 +3272,7 @@ let rec filter_method_field env name priv ty = end else filter_method_field env name priv ty2 | _ -> - raise (Unify []) + raise_unexplained_for Unify (* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *) let filter_method env name priv ty = @@ -3256,14 +3281,14 @@ let filter_method env name priv ty = Tvar _ -> let ty1 = newvar () in let ty' = newobj ty1 in - update_level env ty.level ty'; - update_scope ty.scope ty'; + update_level_for Unify env ty.level ty'; + update_scope_for Unify ty.scope ty'; link_type ty ty'; filter_method_field env name priv ty1 | Tobject(f, _) -> filter_method_field env name priv f | _ -> - raise (Unify []) + raise_unexplained_for Unify let check_filter_method env name priv ty = ignore(filter_method env name priv ty) @@ -3296,11 +3321,11 @@ let moregen_occur env level ty = begin try occur ty; unmark_type ty with Occur -> - unmark_type ty; raise (Unify []) + unmark_type ty; raise_unexplained_for Moregen end; (* also check for free univars *) - occur_univar env ty; - update_level env level ty + occur_univar_for Moregen env ty; + update_level_for Moregen env level ty let may_instantiate inst_nongen t1 = if inst_nongen then t1.level <> generic_level - 1 @@ -3311,13 +3336,12 @@ let rec moregen inst_nongen type_pairs env t1 t2 = let t1 = repr t1 in let t2 = repr t2 in if t1 == t2 then () else - try match (t1.desc, t2.desc) with - (Tvar _, _) when may_instantiate inst_nongen t1 -> + | (Tvar _, _) when may_instantiate inst_nongen t1 -> moregen_occur env t1.level t2; - update_scope t1.scope t2; - occur env t1 t2; + update_scope_for Moregen t1.scope t2; + occur_for Moregen env t1 t2; link_type t1 t2 | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 -> () @@ -3334,7 +3358,7 @@ let rec moregen inst_nongen type_pairs env t1 t2 = match (t1'.desc, t2'.desc) with (Tvar _, _) when may_instantiate inst_nongen t1' -> moregen_occur env t1'.level t2; - update_scope t1'.scope t2; + update_scope_for Moregen t1'.scope t2; link_type t1' t2 | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2 || !Clflags.classic && not (is_optional l1 || is_optional l2) -> @@ -3349,8 +3373,10 @@ let rec moregen inst_nongen type_pairs env t1 t2 = begin try unify_package env (moregen_list inst_nongen type_pairs env) t1'.level p1 fl1 t2'.level p2 fl2 - with Not_found -> raise (Unify []) + with Not_found -> raise_unexplained_for Moregen end + | (Tnil, Tconstr _ ) -> raise_for Moregen (Obj (Abstract_row Second)) + | (Tconstr _, Tnil ) -> raise_for Moregen (Obj (Abstract_row First)) | (Tvariant row1, Tvariant row2) -> moregen_row inst_nongen type_pairs env row1 row2 | (Tobject (fi1, _nm1), Tobject (fi2, _nm2)) -> @@ -3362,35 +3388,39 @@ let rec moregen inst_nongen type_pairs env t1 t2 = | (Tpoly (t1, []), Tpoly (t2, [])) -> moregen inst_nongen type_pairs env t1 t2 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) -> - enter_poly env univar_pairs t1 tl1 t2 tl2 + enter_poly_for Moregen env univar_pairs t1 tl1 t2 tl2 (moregen inst_nongen type_pairs env) | (Tunivar _, Tunivar _) -> - unify_univar t1' t2' !univar_pairs + unify_univar_for Moregen t1' t2' !univar_pairs | (_, _) -> - raise (Unify []) + raise_unexplained_for Moregen end - with Unify trace -> raise( Unify ( Trace.diff t1 t2 :: trace ) ) + with Moregen trace -> raise ( Moregen ( Errortrace.diff t1 t2 :: trace ) ); + and moregen_list inst_nongen type_pairs env tl1 tl2 = if List.length tl1 <> List.length tl2 then - raise (Unify []); + raise_unexplained_for Moregen; List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2 and moregen_fields inst_nongen type_pairs env ty1 ty2 = let (fields1, rest1) = flatten_fields ty1 and (fields2, rest2) = flatten_fields ty2 in let (pairs, miss1, miss2) = associate_fields fields1 fields2 in - if miss1 <> [] then raise (Unify []); + begin + match miss1 with + | (n, _, _) :: _ -> raise_for Moregen (Obj (Missing_field (Second, n))) + | [] -> () + end; moregen inst_nongen type_pairs env rest1 (build_fields (repr ty2).level miss2 rest2); + List.iter (fun (n, k1, t1, k2, t2) -> + (* The below call should never throw [Public_method_to_private_method] *) moregen_kind k1 k2; - try moregen inst_nongen type_pairs env t1 t2 with Unify trace -> - let e = Trace.diff - (newty (Tfield(n, k1, t1, rest2))) - (newty (Tfield(n, k2, t2, rest2))) in - raise( Unify ( e :: trace ) ) + try moregen inst_nongen type_pairs env t1 t2 with Moregen trace -> + raise( Moregen ( Errortrace.incompatible_fields n t1 t2 :: trace ) ) ) pairs @@ -3401,7 +3431,8 @@ and moregen_kind k1 k2 = match k1, k2 with (Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2 | (Fpresent, Fpresent) -> () - | _ -> raise (Unify []) + | (Fpresent, Fvar _) -> raise Public_method_to_private_method + | (Fabsent, _) | (_, Fabsent) -> assert false and moregen_row inst_nongen type_pairs env row1 row2 = let row1 = row_repr row1 and row2 = row_repr row2 in @@ -3415,55 +3446,67 @@ and moregen_row inst_nongen type_pairs env row1 row2 = filter_row_fields may_inst r1, filter_row_fields false r2 else r1, r2 in - if r1 <> [] || row1.row_closed && (not row2.row_closed || r2 <> []) - then raise (Unify []); + begin + if r1 <> [] then raise_for Moregen (Variant (No_tags (Second, r1))) + end; + if row1.row_closed then begin + match row2.row_closed, r2 with + | false, _ -> raise_for Moregen (Variant (Openness Second)) + | _, _ :: _ -> raise_for Moregen (Variant (No_tags (First, r2))) + | _, [] -> () + end; begin match rm1.desc, rm2.desc with Tunivar _, Tunivar _ -> - unify_univar rm1 rm2 !univar_pairs + unify_univar_for Moregen rm1 rm2 !univar_pairs | Tunivar _, _ | _, Tunivar _ -> - raise (Unify []) + raise_unexplained_for Moregen | _ when static_row row1 -> () | _ when may_inst -> let ext = newgenty (Tvariant {row2 with row_fields = r2; row_name = None}) in moregen_occur env rm1.level ext; - update_scope rm1.scope ext; + update_scope_for Moregen rm1.scope ext; link_type rm1 ext | Tconstr _, Tconstr _ -> moregen inst_nongen type_pairs env rm1 rm2 - | _ -> raise (Unify []) + | _ -> raise_unexplained_for Moregen end; List.iter - (fun (_l,f1,f2) -> - let f1 = row_field_repr f1 and f2 = row_field_repr f2 in - if f1 == f2 then () else - match f1, f2 with - Rpresent(Some t1), Rpresent(Some t2) -> - moregen inst_nongen type_pairs env t1 t2 - | Rpresent None, Rpresent None -> () - | Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst -> - set_row_field e1 f2; - List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1 - | Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) -> - if e1 != e2 then begin - if c1 && not c2 then raise(Unify []); - set_row_field e1 (Reither (c2, [], m2, e2)); - if List.length tl1 = List.length tl2 then - List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2 - else match tl2 with - t2 :: _ -> - List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) - tl1 - | [] -> - if tl1 <> [] then raise (Unify []) - end - | Reither(true, [], _, e1), Rpresent None when may_inst -> - set_row_field e1 f2 - | Reither(_, _, _, e1), Rabsent when may_inst -> - set_row_field e1 f2 - | Rabsent, Rabsent -> () - | _ -> raise (Unify [])) + (fun (l,f1,f2) -> + try + let f1 = row_field_repr f1 and f2 = row_field_repr f2 in + if f1 == f2 then () else + match f1, f2 with + | Rpresent(Some t1), Rpresent(Some t2) -> + moregen inst_nongen type_pairs env t1 t2 + | Rpresent None, Rpresent None -> () + | Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst -> + set_row_field e1 f2; + List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1 + | Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) -> + if e1 != e2 then begin + if c1 && not c2 then raise_unexplained_for Moregen; + set_row_field e1 (Reither (c2, [], m2, e2)); + if List.length tl1 = List.length tl2 then + List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2 + else match tl2 with + | t2 :: _ -> + List.iter + (fun t1 -> moregen inst_nongen type_pairs env t1 t2) + tl1 + | [] -> if tl1 <> [] then raise_unexplained_for Moregen + end + | Reither(true, [], _, e1), Rpresent None when may_inst -> + set_row_field e1 f2 + | Reither(_, _, _, e1), Rabsent when may_inst -> set_row_field e1 f2 + | Rabsent, Rabsent -> () + | Rpresent (Some _), Rpresent None -> raise_unexplained_for Moregen + | Rpresent None, Rpresent (Some _) -> raise_unexplained_for Moregen + | Rpresent _, Reither _ -> raise_unexplained_for Moregen + | _ -> raise_unexplained_for Moregen + with Moregen err -> + raise (Moregen (Variant (Incompatible_types_for l) :: err))) pairs (* Must empty univar_pairs first *) @@ -3492,13 +3535,15 @@ let moregeneral env inst_nongen pat_sch subj_sch = current_level := generic_level; (* Duplicate generic variables *) let patt = instance pat_sch in - let res = - try moregen inst_nongen (TypePairs.create 13) env patt subj; true with - Unify _ -> false - in - current_level := old_level; - res + Misc.try_finally + (fun () -> moregen inst_nongen (TypePairs.create 13) env patt subj) + ~always:(fun () -> current_level := old_level) + +let is_moregeneral env inst_nongen pat_sch subj_sch = + match moregeneral env inst_nongen pat_sch subj_sch with + | () -> true + | exception Moregen _ -> false (* Alternative approach: "rigidify" a type scheme, and check validity after unification *) @@ -3545,13 +3590,21 @@ let matches env ty ty' = let snap = snapshot () in let vars = rigidify ty in cleanup_abbrev (); - let ok = - try unify env ty ty'; all_distinct_vars env vars - with Unify _ -> false - in - backtrack snap; - ok + match unify env ty ty' with + | () -> + if not (all_distinct_vars env vars) then begin + backtrack snap; + raise (Matches_failure (env, [Errortrace.diff ty ty'])) + end; + backtrack snap + | exception Unify trace -> + backtrack snap; + raise (Matches_failure (env, trace)) +let does_match env ty ty' = + match matches env ty ty' with + | () -> true + | exception Matches_failure (_, _) -> false (*********************************************) (* Equivalence between parameterized types *) @@ -3577,12 +3630,13 @@ let rec eqtype rename type_pairs subst env t1 t2 = try match (t1.desc, t2.desc) with - (Tvar _, Tvar _) when rename -> + | (Tvar _, Tvar _) when rename -> begin try normalize_subst subst; - if List.assq t1 !subst != t2 then raise (Unify []) + if List.assq t1 !subst != t2 then raise_unexplained_for Equality with Not_found -> - if List.exists (fun (_, t) -> t == t2) !subst then raise (Unify []); + if List.exists (fun (_, t) -> t == t2) !subst then + raise_unexplained_for Equality; subst := (t1, t2) :: !subst end | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 -> @@ -3598,13 +3652,14 @@ let rec eqtype rename type_pairs subst env t1 t2 = with Not_found -> TypePairs.add type_pairs (t1', t2') (); match (t1'.desc, t2'.desc) with - (Tvar _, Tvar _) when rename -> + | (Tvar _, Tvar _) when rename -> begin try normalize_subst subst; - if List.assq t1' !subst != t2' then raise (Unify []) + if List.assq t1' !subst != t2' then + raise_unexplained_for Equality with Not_found -> - if List.exists (fun (_, t) -> t == t2') !subst - then raise (Unify []); + if List.exists (fun (_, t) -> t == t2') !subst then + raise_unexplained_for Equality; subst := (t1', t2') :: !subst end | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2 @@ -3620,8 +3675,12 @@ let rec eqtype rename type_pairs subst env t1 t2 = begin try unify_package env (eqtype_list rename type_pairs subst env) t1'.level p1 fl1 t2'.level p2 fl2 - with Not_found -> raise (Unify []) + with Not_found -> raise_unexplained_for Equality end + | (Tnil, Tconstr _ ) -> + raise_for Equality (Obj (Abstract_row Second)) + | (Tconstr _, Tnil ) -> + raise_for Equality (Obj (Abstract_row First)) | (Tvariant row1, Tvariant row2) -> eqtype_row rename type_pairs subst env row1 row2 | (Tobject (fi1, _nm1), Tobject (fi2, _nm2)) -> @@ -3633,18 +3692,18 @@ let rec eqtype rename type_pairs subst env t1 t2 = | (Tpoly (t1, []), Tpoly (t2, [])) -> eqtype rename type_pairs subst env t1 t2 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) -> - enter_poly env univar_pairs t1 tl1 t2 tl2 + enter_poly_for Equality env univar_pairs t1 tl1 t2 tl2 (eqtype rename type_pairs subst env) | (Tunivar _, Tunivar _) -> - unify_univar t1' t2' !univar_pairs + unify_univar_for Equality t1' t2' !univar_pairs | (_, _) -> - raise (Unify []) + raise_unexplained_for Equality end - with Unify trace -> raise ( Unify (Trace.diff t1 t2 :: trace) ) + with Equality trace -> raise ( Equality (Errortrace.diff t1 t2 :: trace) ) and eqtype_list rename type_pairs subst env tl1 tl2 = if List.length tl1 <> List.length tl2 then - raise (Unify []); + raise_unexplained_for Equality; List.iter2 (eqtype rename type_pairs subst env) tl1 tl2 and eqtype_fields rename type_pairs subst env ty1 ty2 = @@ -3662,25 +3721,26 @@ and eqtype_fields rename type_pairs subst env ty1 ty2 = | _ -> let (pairs, miss1, miss2) = associate_fields fields1 fields2 in eqtype rename type_pairs subst env rest1 rest2; - if (miss1 <> []) || (miss2 <> []) then raise (Unify []); - List.iter - (function (n, k1, t1, k2, t2) -> - eqtype_kind k1 k2; - try eqtype rename type_pairs subst env t1 t2 with Unify trace -> - let e = Trace.diff - (newty (Tfield(n, k1, t1, rest2))) - (newty (Tfield(n, k2, t2, rest2))) in - raise ( Unify ( e :: trace ) ) - ) - pairs + match miss1, miss2 with + | ((n, _, _)::_, _) -> raise_for Equality (Obj (Missing_field (Second, n))) + | (_, (n, _, _)::_) -> raise_for Equality (Obj (Missing_field (First, n))) + | [], [] -> + List.iter + (function (n, k1, t1, k2, t2) -> + eqtype_kind k1 k2; + try + eqtype rename type_pairs subst env t1 t2; + with Equality trace -> + raise (Equality (Errortrace.incompatible_fields n t1 t2 :: trace))) + pairs and eqtype_kind k1 k2 = let k1 = field_kind_repr k1 in let k2 = field_kind_repr k2 in match k1, k2 with - (Fvar _, Fvar _) + | (Fvar _, Fvar _) | (Fpresent, Fpresent) -> () - | _ -> raise (Unify []) + | _ -> raise_unexplained_for Equality and eqtype_row rename type_pairs subst env row1 row2 = (* Try expansion, needed when called from Includecore.type_manifest *) @@ -3689,32 +3749,56 @@ and eqtype_row rename type_pairs subst env row1 row2 = | _ -> let row1 = row_repr row1 and row2 = row_repr row2 in let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in - if row1.row_closed <> row2.row_closed - || not row1.row_closed && (r1 <> [] || r2 <> []) - || filter_row_fields false (r1 @ r2) <> [] - then raise (Unify []); + if row1.row_closed <> row2.row_closed then begin + raise_for Equality + (Variant (Openness (if row2.row_closed then First else Second))) + end; + if not row1.row_closed then begin + match r1, r2 with + | _::_, _ -> raise_for Equality (Variant (No_tags (Second, r1))) + | _, _::_ -> raise_for Equality (Variant (No_tags (First, r2))) + | _, _ -> () + end; + begin + match filter_row_fields false r1 with + | [] -> (); + | _ :: _ as r1 -> raise_for Equality (Variant (No_tags (Second, r1))) + end; + begin + match filter_row_fields false r2 with + | [] -> () + | _ :: _ as r2 -> raise_for Equality (Variant (No_tags (First, r2))) + end; if not (static_row row1) then eqtype rename type_pairs subst env row1.row_more row2.row_more; List.iter - (fun (_,f1,f2) -> - match row_field_repr f1, row_field_repr f2 with - Rpresent(Some t1), Rpresent(Some t2) -> - eqtype rename type_pairs subst env t1 t2 - | Reither(c1, [], _, _), Reither(c2, [], _, _) when c1 = c2 -> - () - | Reither(c1, t1::tl1, _, _), Reither(c2, t2::tl2, _, _) when c1 = c2 -> - eqtype rename type_pairs subst env t1 t2; - if List.length tl1 = List.length tl2 then - (* if same length allow different types (meaning?) *) - List.iter2 (eqtype rename type_pairs subst env) tl1 tl2 - else begin - (* otherwise everything must be equal *) - List.iter (eqtype rename type_pairs subst env t1) tl2; - List.iter (fun t1 -> eqtype rename type_pairs subst env t1 t2) tl1 - end - | Rpresent None, Rpresent None -> () - | Rabsent, Rabsent -> () - | _ -> raise (Unify [])) + (fun (l,f1,f2) -> + try + match row_field_repr f1, row_field_repr f2 with + | Rpresent(Some t1), Rpresent(Some t2) -> + eqtype rename type_pairs subst env t1 t2 + | Reither(c1, [], _, _), Reither(c2, [], _, _) when c1 = c2 -> () + | Reither(c1, t1::tl1, _, _), Reither(c2, t2::tl2, _, _) + when c1 = c2 -> + eqtype rename type_pairs subst env t1 t2; + if List.length tl1 = List.length tl2 then + (* if same length allow different types (meaning?) *) + List.iter2 (eqtype rename type_pairs subst env) tl1 tl2 + else begin + (* otherwise everything must be equal *) + List.iter (eqtype rename type_pairs subst env t1) tl2; + List.iter + (fun t1 -> eqtype rename type_pairs subst env t1 t2) tl1 + end + | Rpresent None, Rpresent None -> () + | Rabsent, Rabsent -> () + | Rpresent (Some _), Rpresent None -> raise_unexplained_for Equality + | Rpresent None, Rpresent (Some _) -> raise_unexplained_for Equality + | Rpresent _, Reither _ -> raise_unexplained_for Equality + | Reither _, Rpresent _ -> raise_unexplained_for Equality + | _ -> raise_unexplained_for Equality + with Equality err -> + raise (Equality (Variant (Incompatible_types_for l):: err))) pairs (* Must empty univar_pairs first *) @@ -3730,25 +3814,39 @@ let eqtype rename type_pairs subst env t1 t2 = (* Two modes: with or without renaming of variables *) let equal env rename tyl1 tyl2 = - try - eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2; true - with - Unify _ -> false + eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2 + +let is_equal env rename tyl1 tyl2 = + match equal env rename tyl1 tyl2 with + | () -> true + | exception Equality _ -> false +let rec equal_private env params1 ty1 params2 ty2 = + match equal env true (params1 @ [ty1]) (params2 @ [ty2]) with + | () -> () + | exception (Equality _ as err) -> + match try_expand_safe_opt env (expand_head env ty1) with + | ty1' -> equal_private env params1 ty1' params2 ty2 + | exception Cannot_expand -> raise err (*************************) (* Class type matching *) (*************************) +type class_match_failure_trace_type = + | CM_Equality + | CM_Moregen type class_match_failure = CM_Virtual_class | CM_Parameter_arity_mismatch of int * int - | CM_Type_parameter_mismatch of Env.t * Unification_trace.t + | CM_Type_parameter_mismatch of Env.t * comparison Errortrace.t (* Equality *) | CM_Class_type_mismatch of Env.t * class_type * class_type - | CM_Parameter_mismatch of Env.t * Unification_trace.t - | CM_Val_type_mismatch of string * Env.t * Unification_trace.t - | CM_Meth_type_mismatch of string * Env.t * Unification_trace.t + | CM_Parameter_mismatch of Env.t * comparison Errortrace.t (* Moregen *) + | CM_Val_type_mismatch of + class_match_failure_trace_type * string * Env.t * comparison Errortrace.t + | CM_Meth_type_mismatch of + class_match_failure_trace_type * string * Env.t * comparison Errortrace.t | CM_Non_mutable_value of string | CM_Non_concrete_value of string | CM_Missing_value of string @@ -3769,7 +3867,7 @@ let rec moregen_clty trace type_pairs env cty1 cty2 = | _, Cty_constr (_, _, cty2) -> moregen_clty true type_pairs env cty1 cty2 | Cty_arrow (l1, ty1, cty1'), Cty_arrow (l2, ty2, cty2') when l1 = l2 -> - begin try moregen true type_pairs env ty1 ty2 with Unify trace -> + begin try moregen true type_pairs env ty1 ty2 with Moregen trace -> raise (Failure [CM_Parameter_mismatch (env, expand_trace env trace)]) end; moregen_clty false type_pairs env cty1' cty2' @@ -3781,17 +3879,18 @@ let rec moregen_clty trace type_pairs env cty1 cty2 = let (pairs, _miss1, _miss2) = associate_fields fields1 fields2 in List.iter (fun (lab, _k1, t1, _k2, t2) -> - begin try moregen true type_pairs env t1 t2 with Unify trace -> - raise (Failure [CM_Meth_type_mismatch - (lab, env, expand_trace env trace)]) - end) - pairs; + try moregen true type_pairs env t1 t2 with Moregen trace -> + raise (Failure [ + CM_Meth_type_mismatch + (CM_Moregen, lab, env, expand_trace env trace)])) + pairs; Vars.iter (fun lab (_mut, _v, ty) -> let (_mut', _v', ty') = Vars.find lab sign1.csig_vars in - try moregen true type_pairs env ty' ty with Unify trace -> - raise (Failure [CM_Val_type_mismatch - (lab, env, expand_trace env trace)])) + try moregen true type_pairs env ty' ty with Moregen trace -> + raise (Failure [ + CM_Val_type_mismatch + (CM_Moregen, lab, env, expand_trace env trace)])) sign2.csig_vars | _ -> raise (Failure []) @@ -3846,8 +3945,10 @@ let match_class_types ?(trace=true) env pat_sch subj_sch = let error = List.fold_right (fun (lab, k1, _t1, k2, _t2) err -> - try moregen_kind k1 k2; err with - Unify _ -> CM_Public_method lab::err) + match moregen_kind k1 k2 with + | () -> err + | exception Public_method_to_private_method -> + CM_Public_method lab :: err) pairs error in let error = @@ -3894,48 +3995,32 @@ let match_class_types ?(trace=true) env pat_sch subj_sch = current_level := old_level; res -let rec equal_clty trace type_pairs subst env cty1 cty2 = +let equal_clsig trace type_pairs subst env sign1 sign2 = try - match cty1, cty2 with - Cty_constr (_, _, cty1), Cty_constr (_, _, cty2) -> - equal_clty true type_pairs subst env cty1 cty2 - | Cty_constr (_, _, cty1), _ -> - equal_clty true type_pairs subst env cty1 cty2 - | _, Cty_constr (_, _, cty2) -> - equal_clty true type_pairs subst env cty1 cty2 - | Cty_arrow (l1, ty1, cty1'), Cty_arrow (l2, ty2, cty2') when l1 = l2 -> - begin try eqtype true type_pairs subst env ty1 ty2 with Unify trace -> - raise (Failure [CM_Parameter_mismatch (env, expand_trace env trace)]) - end; - equal_clty false type_pairs subst env cty1' cty2' - | Cty_signature sign1, Cty_signature sign2 -> - let ty1 = object_fields (repr sign1.csig_self) in - let ty2 = object_fields (repr sign2.csig_self) in - let (fields1, _rest1) = flatten_fields ty1 - and (fields2, _rest2) = flatten_fields ty2 in - let (pairs, _miss1, _miss2) = associate_fields fields1 fields2 in - List.iter - (fun (lab, _k1, t1, _k2, t2) -> - begin try eqtype true type_pairs subst env t1 t2 with - Unify trace -> - raise (Failure [CM_Meth_type_mismatch - (lab, env, expand_trace env trace)]) - end) - pairs; - Vars.iter - (fun lab (_, _, ty) -> - let (_, _, ty') = Vars.find lab sign1.csig_vars in - try eqtype true type_pairs subst env ty' ty with Unify trace -> - raise (Failure [CM_Val_type_mismatch - (lab, env, expand_trace env trace)])) - sign2.csig_vars - | _ -> - raise - (Failure (if trace then [] - else [CM_Class_type_mismatch (env, cty1, cty2)])) + let ty1 = object_fields (repr sign1.csig_self) in + let ty2 = object_fields (repr sign2.csig_self) in + let (fields1, _rest1) = flatten_fields ty1 + and (fields2, _rest2) = flatten_fields ty2 in + let (pairs, _miss1, _miss2) = associate_fields fields1 fields2 in + List.iter + (fun (lab, _k1, t1, _k2, t2) -> + begin try eqtype true type_pairs subst env t1 t2 with + Equality trace -> + raise (Failure [CM_Meth_type_mismatch + (CM_Equality, lab, env, expand_trace env trace)]) + end) + pairs; + Vars.iter + (fun lab (_, _, ty) -> + let (_, _, ty') = Vars.find lab sign1.csig_vars in + try eqtype true type_pairs subst env ty' ty with Equality trace -> + raise (Failure [CM_Val_type_mismatch + (CM_Equality, lab, env, expand_trace env trace)])) + sign2.csig_vars with Failure error when trace -> - raise (Failure (CM_Class_type_mismatch (env, cty1, cty2)::error)) + raise (Failure (CM_Class_type_mismatch + (env, Cty_signature sign1, Cty_signature sign2)::error)) let match_class_declarations env patt_params patt_type subj_params subj_type = let type_pairs = TypePairs.create 53 in @@ -4019,13 +4104,12 @@ let match_class_declarations env patt_params patt_type subj_params subj_type = if lp <> ls then raise (Failure [CM_Parameter_arity_mismatch (lp, ls)]); List.iter2 (fun p s -> - try eqtype true type_pairs subst env p s with Unify trace -> + try eqtype true type_pairs subst env p s with Equality trace -> raise (Failure [CM_Type_parameter_mismatch (env, expand_trace env trace)])) patt_params subj_params; (* old code: equal_clty false type_pairs subst env patt_type subj_type; *) - equal_clty false type_pairs subst env - (Cty_signature sign1) (Cty_signature sign2); + equal_clsig false type_pairs subst env sign1 sign2; (* Use moregeneral for class parameters, need to recheck everything to keeps relationships (PR#4824) *) let clty_params = @@ -4121,8 +4205,10 @@ let rec build_subtype env visited loops posi level t = Tobject _ when posi && not (opened_object t') -> let cl_abbr, body = find_cltype_for_path env p in let ty = - subst env !current_level Public abbrev None - cl_abbr.type_params tl body in + try + subst env !current_level Public abbrev None + cl_abbr.type_params tl body + with Cannot_subst -> assert false in let ty = repr ty in let ty1, tl1 = match ty.desc with @@ -4268,7 +4354,7 @@ let enlarge_type env ty = let subtypes = TypePairs.create 17 let subtype_error env trace = - raise (Subtype (expand_trace env (List.rev trace), [])) + raise (Subtype (expand_subtype_trace env (List.rev trace), [])) let rec subtype_rec env trace t1 t2 cstrs = let t1 = repr t1 in @@ -4285,8 +4371,8 @@ let rec subtype_rec env trace t1 t2 cstrs = (trace, t1, t2, !univar_pairs)::cstrs | (Tarrow(l1, t1, u1, _), Tarrow(l2, t2, u2, _)) when l1 = l2 || !Clflags.classic && not (is_optional l1 || is_optional l2) -> - let cstrs = subtype_rec env (Trace.diff t2 t1::trace) t2 t1 cstrs in - subtype_rec env (Trace.diff u1 u2::trace) u1 u2 cstrs + let cstrs = subtype_rec env (Subtype.diff t2 t1::trace) t2 t1 cstrs in + subtype_rec env (Subtype.diff u1 u2::trace) u1 u2 cstrs | (Ttuple tl1, Ttuple tl2) -> subtype_list env trace tl1 tl2 cstrs | (Tconstr(p1, [], _), Tconstr(p2, [], _)) when Path.same p1 p2 -> @@ -4307,15 +4393,17 @@ let rec subtype_rec env trace t1 t2 cstrs = if cn then (trace, newty2 t1.level (Ttuple[t1]), newty2 t2.level (Ttuple[t2]), !univar_pairs) :: cstrs - else subtype_rec env (Trace.diff t1 t2::trace) t1 t2 cstrs + else subtype_rec env (Subtype.diff t1 t2::trace) t1 t2 cstrs else - if cn then subtype_rec env (Trace.diff t2 t1::trace) t2 t1 cstrs + if cn + then subtype_rec env (Subtype.diff t2 t1::trace) t2 t1 cstrs else cstrs) cstrs decl.type_variance (List.combine tl1 tl2) with Not_found -> (trace, t1, t2, !univar_pairs)::cstrs end - | (Tconstr(p1, _, _), _) when generic_private_abbrev env p1 -> + | (Tconstr(p1, _, _), _) + when generic_private_abbrev env p1 && safe_abbrev_opt env t1 -> subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs (* | (_, Tconstr(p2, _, _)) when generic_private_abbrev false env p2 -> subtype_rec env trace t1 (expand_abbrev_opt env t2) cstrs *) @@ -4340,7 +4428,7 @@ let rec subtype_rec env trace t1 t2 cstrs = begin try enter_poly env univar_pairs u1 tl1 u2 tl2 (fun t1 t2 -> subtype_rec env trace t1 t2 cstrs) - with Unify _ -> + with Escape _ -> (trace, t1, t2, !univar_pairs)::cstrs end | (Tpackage (p1, fl1), Tpackage (p2, fl2)) -> @@ -4357,12 +4445,10 @@ let rec subtype_rec env trace t1 t2 cstrs = else begin (* need to check module subtyping *) let snap = Btype.snapshot () in - try - List.iter (fun (_, t1, t2, _) -> unify env t1 t2) cstrs'; - if !package_subtype env p1 fl1 p2 fl2 - then (Btype.backtrack snap; cstrs' @ cstrs) - else raise (Unify []) - with Unify _ -> + match List.iter (fun (_, t1, t2, _) -> unify env t1 t2) cstrs' with + | () when !package_subtype env p1 fl1 p2 fl2 -> + Btype.backtrack snap; cstrs' @ cstrs + | () | exception Unify _ -> Btype.backtrack snap; raise Not_found end with Not_found -> @@ -4376,7 +4462,7 @@ and subtype_list env trace tl1 tl2 cstrs = if List.length tl1 <> List.length tl2 then subtype_error env trace; List.fold_left2 - (fun cstrs t1 t2 -> subtype_rec env (Trace.diff t1 t2::trace) t1 t2 cstrs) + (fun cstrs t1 t2 -> subtype_rec env (Subtype.diff t1 t2::trace) t1 t2 cstrs) cstrs tl1 tl2 and subtype_fields env trace ty1 ty2 cstrs = @@ -4387,7 +4473,7 @@ and subtype_fields env trace ty1 ty2 cstrs = let cstrs = if rest2.desc = Tnil then cstrs else if miss1 = [] then - subtype_rec env (Trace.diff rest1 rest2::trace) rest1 rest2 cstrs + subtype_rec env (Subtype.diff rest1 rest2::trace) rest1 rest2 cstrs else (trace, build_fields (repr ty1).level miss1 rest1, rest2, !univar_pairs) :: cstrs @@ -4400,7 +4486,7 @@ and subtype_fields env trace ty1 ty2 cstrs = List.fold_left (fun cstrs (_, _k1, t1, _k2, t2) -> (* These fields are always present *) - subtype_rec env (Trace.diff t1 t2::trace) t1 t2 cstrs) + subtype_rec env (Subtype.diff t1 t2::trace) t1 t2 cstrs) cstrs pairs and subtype_row env trace row1 row2 cstrs = @@ -4413,7 +4499,7 @@ and subtype_row env trace row1 row2 cstrs = and more2 = repr row2.row_more in match more1.desc, more2.desc with Tconstr(p1,_,_), Tconstr(p2,_,_) when Path.same p1 p2 -> - subtype_rec env (Trace.diff more1 more2::trace) more1 more2 cstrs + subtype_rec env (Subtype.diff more1 more2::trace) more1 more2 cstrs | (Tvar _|Tconstr _|Tnil), (Tvar _|Tconstr _|Tnil) when row1.row_closed && r1 = [] -> List.fold_left @@ -4422,16 +4508,16 @@ and subtype_row env trace row1 row2 cstrs = (Rpresent None|Reither(true,_,_,_)), Rpresent None -> cstrs | Rpresent(Some t1), Rpresent(Some t2) -> - subtype_rec env (Trace.diff t1 t2::trace) t1 t2 cstrs + subtype_rec env (Subtype.diff t1 t2::trace) t1 t2 cstrs | Reither(false, t1::_, _, _), Rpresent(Some t2) -> - subtype_rec env (Trace.diff t1 t2::trace) t1 t2 cstrs + subtype_rec env (Subtype.diff t1 t2::trace) t1 t2 cstrs | Rabsent, _ -> cstrs | _ -> raise Exit) cstrs pairs | Tunivar _, Tunivar _ when row1.row_closed = row2.row_closed && r1 = [] && r2 = [] -> let cstrs = - subtype_rec env (Trace.diff more1 more2::trace) more1 more2 cstrs in + subtype_rec env (Subtype.diff more1 more2::trace) more1 more2 cstrs in List.fold_left (fun cstrs (_,f1,f2) -> match row_field_repr f1, row_field_repr f2 with @@ -4441,7 +4527,7 @@ and subtype_row env trace row1 row2 cstrs = cstrs | Rpresent(Some t1), Rpresent(Some t2) | Reither(false,[t1],_,_), Reither(false,[t2],_,_) -> - subtype_rec env (Trace.diff t1 t2::trace) t1 t2 cstrs + subtype_rec env (Subtype.diff t1 t2::trace) t1 t2 cstrs | _ -> raise Exit) cstrs pairs | _ -> @@ -4451,14 +4537,14 @@ let subtype env ty1 ty2 = TypePairs.clear subtypes; univar_pairs := []; (* Build constraint set. *) - let cstrs = subtype_rec env [Trace.diff ty1 ty2] ty1 ty2 [] in + let cstrs = subtype_rec env [Subtype.diff ty1 ty2] ty1 ty2 [] in TypePairs.clear subtypes; (* Enforce constraints. *) function () -> List.iter (function (trace0, t1, t2, pairs) -> try unify_pairs (ref env) t1 t2 pairs with Unify trace -> - raise (Subtype (expand_trace env (List.rev trace0), + raise (Subtype (expand_subtype_trace env (List.rev trace0), List.tl trace))) (List.rev cstrs) @@ -4569,8 +4655,12 @@ let rec normalize_type_rec visited ty = List.fold_left (fun tyl ty -> if List.exists - (fun ty' -> equal Env.empty false [ty] [ty']) tyl - then tyl else ty::tyl) + (fun ty' -> + match equal Env.empty false [ty] [ty'] with + | () -> true + | exception Equality _ -> false) + tyl + then tyl else ty::tyl) [ty] tyl in if f != f0 || List.length tyl' < List.length tyl then @@ -4632,8 +4722,9 @@ let clear_hash () = TypeHash.clear nondep_hash; TypeHash.clear nondep_variants let rec nondep_type_rec ?(expand_private=false) env ids ty = - let expand_abbrev env t = - if expand_private then expand_abbrev_opt env t else expand_abbrev env t + let try_expand env t = + if expand_private then try_expand_safe_opt env t + else try_expand_safe env t in match ty.desc with Tvar _ | Tunivar _ -> ty @@ -4655,14 +4746,14 @@ let rec nondep_type_rec ?(expand_private=false) env ids ty = with (Nondep_cannot_erase _) as exn -> (* If that doesn't work, try expanding abbrevs *) try Tlink (nondep_type_rec ~expand_private env ids - (expand_abbrev env (newty2 ty.level ty.desc))) + (try_expand env (newty2 ty.level ty.desc))) (* The [Tlink] is important. The expanded type may be a variable, or may not be completely copied yet (recursive type), so one cannot just take its description. *) - with Cannot_expand | Unify _ -> raise exn + with Cannot_expand -> raise exn end | Tpackage(p, fl) when Path.exists_free ids p -> let p' = normalize_package_path env p in diff --git a/typing/ctype.mli b/typing/ctype.mli index 9d92f7f6ad..7185cdb7e0 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -20,80 +20,19 @@ open Types module TypePairs : Hashtbl.S with type key = type_expr * type_expr -module Unification_trace: sig - (** Unification traces are used to explain unification errors - when printing error messages *) - - type position = First | Second - type desc = { t: type_expr; expanded: type_expr option } - type 'a diff = { got: 'a; expected: 'a} - - (** Scope escape related errors *) - type 'a escape = - | Constructor of Path.t - | Univ of type_expr - (** The type_expr argument of [Univ] is always a [Tunivar _], - we keep a [type_expr] to track renaming in {!Printtyp} *) - | Self - | Module_type of Path.t - | Equation of 'a - - (** Errors for polymorphic variants *) - - type fixed_row_case = - | Cannot_be_closed - | Cannot_add_tags of string list - - type variant = - | No_intersection - | No_tags of position * (Asttypes.label * row_field) list - | Incompatible_types_for of string - | Fixed_row of position * fixed_row_case * fixed_explanation - (** Fixed row types, e.g. ['a. [> `X] as 'a] *) - - type obj = - | Missing_field of position * string - | Abstract_row of position - | Self_cannot_be_closed - - type 'a elt = - | Diff of 'a diff - | Variant of variant - | Obj of obj - | Escape of {context: type_expr option; kind:'a escape} - | Incompatible_fields of {name:string; diff: type_expr diff } - | Rec_occur of type_expr * type_expr - - type t = desc elt list - - val diff: type_expr -> type_expr -> desc elt - - (** [map_diff f {expected;got}] is [{expected=f expected; got=f got}] *) - val map_diff: ('a -> 'b) -> 'a diff -> 'b diff - - (** [flatten f trace] flattens all elements of type {!desc} in - [trace] to either [f x.t expanded] if [x.expanded=Some expanded] - or [f x.t x.t] otherwise *) - val flatten: (type_expr -> type_expr -> 'a) -> t -> 'a elt list - - (** Switch [expected] and [got] *) - val swap: t -> t - - (** [explain trace f] calls [f] on trace elements starting from the end - until [f ~prev elt] is [Some _], returns that - or [None] if the end of the trace is reached. *) - val explain: - 'a elt list -> - (prev:'a elt option -> 'a elt -> 'b option) -> - 'b option - -end - -exception Unify of Unification_trace.t +exception Unify of Errortrace.unification Errortrace.t +exception Equality of Errortrace.comparison Errortrace.t +exception Moregen of Errortrace.comparison Errortrace.t +exception Subtype of Errortrace.Subtype.t * Errortrace.unification Errortrace.t +exception Escape of Errortrace.desc Errortrace.escape + exception Tags of label * label -exception Subtype of Unification_trace.t * Unification_trace.t exception Cannot_expand exception Cannot_apply +exception Matches_failure of Env.t * Errortrace.unification Errortrace.t + (* Raised from [matches], hence the odd name *) +exception Incompatible + (* Raised from [mcomp] *) val init_def: int -> unit (* Set the initial variable level *) @@ -197,7 +136,7 @@ val fully_generic: type_expr -> bool val check_scope_escape : Env.t -> int -> type_expr -> unit (* [check_scope_escape env lvl ty] ensures that [ty] could be raised to the level [lvl] without any scope escape. - Raises [Unify] otherwise *) + Raises [Escape] otherwise *) val instance: ?partial:bool -> type_expr -> type_expr (* Take an instance of a type scheme *) @@ -241,9 +180,11 @@ val apply: the parameters [pi] and returns the corresponding instance of [t]. Exception [Cannot_apply] is raised in case of failure. *) +val try_expand_once_opt: Env.t -> type_expr -> type_expr +val try_expand_safe_opt: Env.t -> type_expr -> type_expr + val expand_head_once: Env.t -> type_expr -> type_expr val expand_head: Env.t -> type_expr -> type_expr -val try_expand_once_opt: Env.t -> type_expr -> type_expr val expand_head_opt: Env.t -> type_expr -> type_expr (** The compiler's own version of [expand_head] necessary for type-based optimisations. *) @@ -277,28 +218,38 @@ val deep_occur: type_expr -> type_expr -> bool val filter_self_method: Env.t -> string -> private_flag -> (Ident.t * type_expr) Meths.t ref -> type_expr -> Ident.t * type_expr -val moregeneral: Env.t -> bool -> type_expr -> type_expr -> bool +val moregeneral: Env.t -> bool -> type_expr -> type_expr -> unit (* Check if the first type scheme is more general than the second. *) - +val is_moregeneral: Env.t -> bool -> type_expr -> type_expr -> bool val rigidify: type_expr -> type_expr list (* "Rigidify" a type and return its type variable *) val all_distinct_vars: Env.t -> type_expr list -> bool (* Check those types are all distinct type variables *) -val matches: Env.t -> type_expr -> type_expr -> bool +val matches: Env.t -> type_expr -> type_expr -> unit (* Same as [moregeneral false], implemented using the two above functions and backtracking. Ignore levels *) +val does_match: Env.t -> type_expr -> type_expr -> bool + (* Same as [matches], but returns a [bool] *) val reify_univars : Env.t -> Types.type_expr -> Types.type_expr (* Replaces all the variables of a type by a univar. *) +type class_match_failure_trace_type = + | CM_Equality + | CM_Moregen + type class_match_failure = CM_Virtual_class | CM_Parameter_arity_mismatch of int * int - | CM_Type_parameter_mismatch of Env.t * Unification_trace.t + | CM_Type_parameter_mismatch of Env.t * Errortrace.comparison Errortrace.t | CM_Class_type_mismatch of Env.t * class_type * class_type - | CM_Parameter_mismatch of Env.t * Unification_trace.t - | CM_Val_type_mismatch of string * Env.t * Unification_trace.t - | CM_Meth_type_mismatch of string * Env.t * Unification_trace.t + | CM_Parameter_mismatch of Env.t * Errortrace.comparison Errortrace.t + | CM_Val_type_mismatch of + class_match_failure_trace_type * + string * Env.t * Errortrace.comparison Errortrace.t + | CM_Meth_type_mismatch of + class_match_failure_trace_type * + string * Env.t * Errortrace.comparison Errortrace.t | CM_Non_mutable_value of string | CM_Non_concrete_value of string | CM_Missing_value of string @@ -311,10 +262,18 @@ type class_match_failure = val match_class_types: ?trace:bool -> Env.t -> class_type -> class_type -> class_match_failure list (* Check if the first class type is more general than the second. *) -val equal: Env.t -> bool -> type_expr list -> type_expr list -> bool +val equal: Env.t -> bool -> type_expr list -> type_expr list -> unit (* [equal env [x1...xn] tau [y1...yn] sigma] checks whether the parameterized types [/\x1.../\xn.tau] and [/\y1.../\yn.sigma] are equivalent. *) +val is_equal : Env.t -> bool -> type_expr list -> type_expr list -> bool +val equal_private : + Env.t -> type_expr list -> type_expr -> + type_expr list -> type_expr -> unit +(* [equal_private env t1 params1 t2 params2] checks that [t1::params1] + equals [t2::params2] but it is allowed to expand [t1] if it is a + private abbreviations. *) + val match_class_declarations: Env.t -> type_expr list -> class_type -> type_expr list -> class_type -> class_match_failure list @@ -391,4 +350,5 @@ val package_subtype : (Env.t -> Path.t -> (Longident.t * type_expr) list -> Path.t -> (Longident.t * type_expr) list -> bool) ref +(* Raises [Incompatible] *) val mcomp : Env.t -> type_expr -> type_expr -> unit diff --git a/typing/errortrace.ml b/typing/errortrace.ml new file mode 100644 index 0000000000..eca74088de --- /dev/null +++ b/typing/errortrace.ml @@ -0,0 +1,158 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Florian Angeletti, projet Cambium, Inria Paris *) +(* Antal Spector-Zabusky, Jane Street, New York *) +(* *) +(* Copyright 2018 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* Copyright 2021 Jane Street Group LLC *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +open Types +open Format + +type position = First | Second + +let swap_position = function + | First -> Second + | Second -> First + +let print_pos ppf = function + | First -> fprintf ppf "first" + | Second -> fprintf ppf "second" + +type desc = { t: type_expr; expanded: type_expr option } +type 'a diff = { got: 'a; expected: 'a} + +let short t = { t; expanded = None } +let map_diff f r = + (* ordering is often meaningful when dealing with type_expr *) + let got = f r.got in + let expected = f r.expected in + { got; expected} + +let flatten_desc f x = match x.expanded with + | None -> f x.t x.t + | Some expanded -> f x.t expanded + +let swap_diff x = { got = x.expected; expected = x.got } + +type 'a escape_kind = + | Constructor of Path.t + | Univ of type_expr + (* The type_expr argument of [Univ] is always a [Tunivar _], + we keep a [type_expr] to track renaming in {!Printtyp} *) + | Self + | Module_type of Path.t + | Equation of 'a + | Constraint + +type 'a escape = + { kind : 'a escape_kind; + context : type_expr option } + +let explain trace f = + let rec explain = function + | [] -> None + | [h] -> f ~prev:None h + | h :: (prev :: _ as rem) -> + match f ~prev:(Some prev) h with + | Some _ as m -> m + | None -> explain rem in + explain (List.rev trace) + +(* Type indices *) +type unification = private Unification +type comparison = private Comparison + +type fixed_row_case = + | Cannot_be_closed + | Cannot_add_tags of string list + +type 'variety variant = + (* Common *) + | Incompatible_types_for : string -> _ variant + | No_tags : position * (Asttypes.label * row_field) list -> _ variant + (* Unification *) + | No_intersection : unification variant + | Fixed_row : + position * fixed_row_case * fixed_explanation -> unification variant + (* Equality & Moregen *) + | Openness : position (* Always [Second] for Moregen *) -> comparison variant + +type 'variety obj = + (* Common *) + | Missing_field : position * string -> _ obj + | Abstract_row : position -> _ obj + (* Unification *) + | Self_cannot_be_closed : unification obj + +type ('a, 'variety) elt = + (* Common *) + | Diff : 'a diff -> ('a, _) elt + | Variant : 'variety variant -> ('a, 'variety) elt + | Obj : 'variety obj -> ('a, 'variety) elt + | Escape : 'a escape -> ('a, _) elt + | Incompatible_fields : { name:string; diff: type_expr diff } -> ('a, _) elt + (* Could move [Incompatible_fields] into [obj] *) + (* Unification & Moregen; included in Equality for simplicity *) + | Rec_occur : type_expr * type_expr -> ('a, _) elt + +type 'variety t = + (desc, 'variety) elt list + +let diff got expected = Diff (map_diff short { got; expected }) + +let map_elt (type variety) f : ('a, variety) elt -> ('b, variety) elt = function + | Diff x -> Diff (map_diff f x) + | Escape {kind = Equation x; context} -> + Escape { kind = Equation (f x); context } + | Escape {kind = (Univ _ | Self | Constructor _ | Module_type _ | Constraint); + _} + | Variant _ | Obj _ | Incompatible_fields _ | Rec_occur (_, _) as x -> x + +let map f t = List.map (map_elt f) t + +(* Convert desc to type_expr * type_expr *) +let flatten f = map (flatten_desc f) + +let incompatible_fields name got expected = + Incompatible_fields { name; diff={got; expected} } + + +let swap_elt (type variety) : ('a, variety) elt -> ('a, variety) elt = function + | Diff x -> Diff (swap_diff x) + | Incompatible_fields { name; diff } -> + Incompatible_fields { name; diff = swap_diff diff} + | Obj (Missing_field(pos,s)) -> Obj (Missing_field(swap_position pos,s)) + | Obj (Abstract_row pos) -> Obj (Abstract_row (swap_position pos)) + | Variant (Fixed_row(pos,k,f)) -> + Variant (Fixed_row(swap_position pos,k,f)) + | Variant (No_tags(pos,f)) -> + Variant (No_tags(swap_position pos,f)) + | x -> x + +let swap_trace e = List.map swap_elt e + +module Subtype = struct + type 'a elt = + | Diff of 'a diff + + type t = desc elt list + + let diff got expected = Diff (map_diff short {got;expected}) + + let map_elt f = function + | Diff x -> Diff (map_diff f x) + + let map f t = List.map (map_elt f) t + + let flatten f t = map (flatten_desc f) t +end diff --git a/typing/errortrace.mli b/typing/errortrace.mli new file mode 100644 index 0000000000..be6000ed10 --- /dev/null +++ b/typing/errortrace.mli @@ -0,0 +1,116 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Florian Angeletti, projet Cambium, Inria Paris *) +(* Antal Spector-Zabusky, Jane Street, New York *) +(* *) +(* Copyright 2018 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* Copyright 2021 Jane Street Group LLC *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +open Types + +type position = First | Second + +val swap_position : position -> position +val print_pos : Format.formatter -> position -> unit + +type desc = { t: type_expr; expanded: type_expr option } +type 'a diff = { got: 'a; expected: 'a} + +(** [map_diff f {expected;got}] is [{expected=f expected; got=f got}] *) +val map_diff: ('a -> 'b) -> 'a diff -> 'b diff + +(** Scope escape related errors *) +type 'a escape_kind = + | Constructor of Path.t + | Univ of type_expr + (* The type_expr argument of [Univ] is always a [Tunivar _], + we keep a [type_expr] to track renaming in {!Printtyp} *) + | Self + | Module_type of Path.t + | Equation of 'a + | Constraint + +type 'a escape = + { kind : 'a escape_kind; + context : type_expr option } + +val short : type_expr -> desc + +val explain: 'a list -> + (prev:'a option -> 'a -> 'b option) -> + 'b option + +(* Type indices *) +type unification = private Unification +type comparison = private Comparison + +type fixed_row_case = + | Cannot_be_closed + | Cannot_add_tags of string list + +type 'variety variant = + (* Common *) + | Incompatible_types_for : string -> _ variant + | No_tags : position * (Asttypes.label * row_field) list -> _ variant + (* Unification *) + | No_intersection : unification variant + | Fixed_row : + position * fixed_row_case * fixed_explanation -> unification variant + (* Equality & Moregen *) + | Openness : position (* Always [Second] for Moregen *) -> comparison variant + +type 'variety obj = + (* Common *) + | Missing_field : position * string -> _ obj + | Abstract_row : position -> _ obj + (* Unification *) + | Self_cannot_be_closed : unification obj + +type ('a, 'variety) elt = + (* Common *) + | Diff : 'a diff -> ('a, _) elt + | Variant : 'variety variant -> ('a, 'variety) elt + | Obj : 'variety obj -> ('a, 'variety) elt + | Escape : 'a escape -> ('a, _) elt + | Incompatible_fields : { name:string; diff: type_expr diff } -> ('a, _) elt + (* Unification & Moregen; included in Equality for simplicity *) + | Rec_occur : type_expr * type_expr -> ('a, _) elt + +type 'variety t = + (desc, 'variety) elt list + +val diff : type_expr -> type_expr -> (desc, _) elt + +(** [flatten f trace] flattens all elements of type {!desc} in + [trace] to either [f x.t expanded] if [x.expanded=Some expanded] + or [f x.t x.t] otherwise *) +val flatten : + (type_expr -> type_expr -> 'a) -> 'variety t -> ('a, 'variety) elt list + +val map : ('a -> 'b) -> ('a, 'variety) elt list -> ('b, 'variety) elt list + +val incompatible_fields : string -> type_expr -> type_expr -> (desc, _) elt + +val swap_trace : 'variety t -> 'variety t + +module Subtype : sig + type 'a elt = + | Diff of 'a diff + + type t = desc elt list + + val diff: type_expr -> type_expr -> desc elt + + val flatten : (type_expr -> type_expr -> 'a) -> t -> 'a elt list + + val map : (desc -> desc) -> desc elt list -> desc elt list +end diff --git a/typing/includeclass.ml b/typing/includeclass.ml index 483088d6fe..2f0c057ff9 100644 --- a/typing/includeclass.ml +++ b/typing/includeclass.ml @@ -49,6 +49,10 @@ let rec hide_params = function | cty -> cty *) +let report_error_for = function + | CM_Equality -> Printtyp.report_equality_error + | CM_Moregen -> Printtyp.report_moregen_error + let include_err ppf = function | CM_Virtual_class -> @@ -57,7 +61,7 @@ let include_err ppf = fprintf ppf "The classes do not have the same number of type parameters" | CM_Type_parameter_mismatch (env, trace) -> - Printtyp.report_unification_error ppf env trace + Printtyp.report_equality_error ppf env trace (function ppf -> fprintf ppf "A type parameter has type") (function ppf -> @@ -70,19 +74,19 @@ let include_err ppf = "is not matched by the class type" Printtyp.class_type cty2) | CM_Parameter_mismatch (env, trace) -> - Printtyp.report_unification_error ppf env trace + Printtyp.report_moregen_error ppf env trace (function ppf -> fprintf ppf "A parameter has type") (function ppf -> fprintf ppf "but is expected to have type") - | CM_Val_type_mismatch (lab, env, trace) -> - Printtyp.report_unification_error ppf env trace + | CM_Val_type_mismatch (trace_type, lab, env, trace) -> + report_error_for trace_type ppf env trace (function ppf -> fprintf ppf "The instance variable %s@ has type" lab) (function ppf -> fprintf ppf "but is expected to have type") - | CM_Meth_type_mismatch (lab, env, trace) -> - Printtyp.report_unification_error ppf env trace + | CM_Meth_type_mismatch (trace_type, lab, env, trace) -> + report_error_for trace_type ppf env trace (function ppf -> fprintf ppf "The method %s@ has type" lab) (function ppf -> diff --git a/typing/includecore.ml b/typing/includecore.ml index 50b58445d1..20aa7493bf 100644 --- a/typing/includecore.ml +++ b/typing/includecore.ml @@ -20,9 +20,55 @@ open Path open Types open Typedtree +type position = Errortrace.position = First | Second + (* Inclusion between value descriptions *) -exception Dont_match +type primitive_mismatch = + | Name + | Arity + | No_alloc of position + | Native_name + | Result_repr + | Argument_repr of int + +let native_repr_args nra1 nra2 = + let rec loop i nra1 nra2 = + match nra1, nra2 with + | [], [] -> None + | [], _ :: _ -> assert false + | _ :: _, [] -> assert false + | nr1 :: nra1, nr2 :: nra2 -> + if not (Primitive.equal_native_repr nr1 nr2) then Some (Argument_repr i) + else loop (i+1) nra1 nra2 + in + loop 1 nra1 nra2 + +let primitive_descriptions pd1 pd2 = + let open Primitive in + if not (String.equal pd1.prim_name pd2.prim_name) then + Some Name + else if not (Int.equal pd1.prim_arity pd2.prim_arity) then + Some Arity + else if (not pd1.prim_alloc) && pd2.prim_alloc then + Some (No_alloc First) + else if pd1.prim_alloc && (not pd2.prim_alloc) then + Some (No_alloc Second) + else if not (String.equal pd1.prim_native_name pd2.prim_native_name) then + Some Native_name + else if not + (Primitive.equal_native_repr + pd1.prim_native_repr_res pd2.prim_native_repr_res) then + Some Result_repr + else + native_repr_args pd1.prim_native_repr_args pd2.prim_native_repr_args + +type value_mismatch = + | Primitive_mismatch of primitive_mismatch + | Not_a_primitive + | Type of Env.t * Errortrace.comparison Errortrace.t + +exception Dont_match of value_mismatch let value_descriptions ~loc env name (vd1 : Types.value_description) @@ -33,18 +79,24 @@ let value_descriptions ~loc env name loc vd1.val_attributes vd2.val_attributes name; - if Ctype.moregeneral env true vd1.val_type vd2.val_type then begin - match (vd1.val_kind, vd2.val_kind) with - (Val_prim p1, Val_prim p2) -> - if p1 = p2 then Tcoerce_none else raise Dont_match + match Ctype.moregeneral env true vd1.val_type vd2.val_type with + | exception Ctype.Moregen trace -> raise (Dont_match (Type (env, trace))) + | () -> begin + match (vd1.val_kind, vd2.val_kind) with + | (Val_prim p1, Val_prim p2) -> begin + match primitive_descriptions p1 p2 with + | None -> Tcoerce_none + | Some err -> raise (Dont_match (Primitive_mismatch err)) + end | (Val_prim p, _) -> - let pc = {pc_desc = p; pc_type = vd2.Types.val_type; - pc_env = env; pc_loc = vd1.Types.val_loc; } in + let pc = + { pc_desc = p; pc_type = vd2.Types.val_type; + pc_env = env; pc_loc = vd1.Types.val_loc; } + in Tcoerce_primitive pc - | (_, Val_prim _) -> raise Dont_match + | (_, Val_prim _) -> raise (Dont_match Not_a_primitive) | (_, _) -> Tcoerce_none - end else - raise Dont_match + end (* Inclusion between "private" annotations *) @@ -59,71 +111,15 @@ let private_flags decl1 decl2 = let is_absrow env ty = match ty.desc with - Tconstr(Pident _, _, _) -> - begin match Ctype.expand_head env ty with - {desc=Tobject _|Tvariant _} -> true + | Tconstr(Pident _, _, _) -> begin + match Ctype.expand_head env ty with + | {desc=Tobject _|Tvariant _} -> true | _ -> false end | _ -> false -let type_manifest env ty1 params1 ty2 params2 priv2 = - let ty1' = Ctype.expand_head env ty1 and ty2' = Ctype.expand_head env ty2 in - match ty1'.desc, ty2'.desc with - Tvariant row1, Tvariant row2 when is_absrow env (Btype.row_more row2) -> - let row1 = Btype.row_repr row1 and row2 = Btype.row_repr row2 in - Ctype.equal env true (ty1::params1) (row2.row_more::params2) && - begin match row1.row_more with - {desc=Tvar _|Tconstr _|Tnil} -> true - | _ -> false - end && - let r1, r2, pairs = - Ctype.merge_row_fields row1.row_fields row2.row_fields in - (not row2.row_closed || - row1.row_closed && Ctype.filter_row_fields false r1 = []) && - List.for_all - (fun (_,f) -> match Btype.row_field_repr f with - Rabsent | Reither _ -> true | Rpresent _ -> false) - r2 && - let to_equal = ref (List.combine params1 params2) in - List.for_all - (fun (_, f1, f2) -> - match Btype.row_field_repr f1, Btype.row_field_repr f2 with - Rpresent(Some t1), - (Rpresent(Some t2) | Reither(false, [t2], _, _)) -> - to_equal := (t1,t2) :: !to_equal; true - | Rpresent None, (Rpresent None | Reither(true, [], _, _)) -> true - | Reither(c1,tl1,_,_), Reither(c2,tl2,_,_) - when List.length tl1 = List.length tl2 && c1 = c2 -> - to_equal := List.combine tl1 tl2 @ !to_equal; true - | Rabsent, (Reither _ | Rabsent) -> true - | _ -> false) - pairs && - let tl1, tl2 = List.split !to_equal in - Ctype.equal env true tl1 tl2 - | Tobject (fi1, _), Tobject (fi2, _) - when is_absrow env (snd(Ctype.flatten_fields fi2)) -> - let (fields2,rest2) = Ctype.flatten_fields fi2 in - Ctype.equal env true (ty1::params1) (rest2::params2) && - let (fields1,rest1) = Ctype.flatten_fields fi1 in - (match rest1 with {desc=Tnil|Tvar _|Tconstr _} -> true | _ -> false) && - let pairs, _miss1, miss2 = Ctype.associate_fields fields1 fields2 in - miss2 = [] && - let tl1, tl2 = - List.split (List.map (fun (_,_,t1,_,t2) -> t1, t2) pairs) in - Ctype.equal env true (params1 @ tl1) (params2 @ tl2) - | _ -> - let rec check_super ty1 = - Ctype.equal env true (ty1 :: params1) (ty2 :: params2) || - priv2 = Private && - try check_super - (Ctype.try_expand_once_opt env (Ctype.expand_head env ty1)) - with Ctype.Cannot_expand -> false - in check_super ty1 - (* Inclusion between type declarations *) -type position = Ctype.Unification_trace.position = First | Second - let choose ord first second = match ord with | First -> first @@ -135,7 +131,7 @@ let choose_other ord first second = | Second -> choose First first second type label_mismatch = - | Type + | Type of Env.t * Errortrace.comparison Errortrace.t | Mutability of position type record_mismatch = @@ -147,7 +143,7 @@ type record_mismatch = | Unboxed_float_representation of position type constructor_mismatch = - | Type + | Type of Env.t * Errortrace.comparison Errortrace.t | Arity | Inline_record of record_mismatch | Kind of position @@ -167,12 +163,25 @@ type extension_constructor_mismatch = * Types.extension_constructor * constructor_mismatch +type private_variant_mismatch = + | Openness + | Missing of position * string + | Presence of string + | Incompatible_types_for of string + | Types of Env.t * Errortrace.comparison Errortrace.t + +type private_object_mismatch = + | Missing of string + | Types of Env.t * Errortrace.comparison Errortrace.t + type type_mismatch = | Arity | Privacy | Kind - | Constraint - | Manifest + | Constraint of Env.t * Errortrace.comparison Errortrace.t + | Manifest of Env.t * Errortrace.comparison Errortrace.t + | Private_variant of type_expr * type_expr * private_variant_mismatch + | Private_object of type_expr * type_expr * private_object_mismatch | Variance | Record_mismatch of record_mismatch | Variant_mismatch of variant_mismatch @@ -182,7 +191,7 @@ type type_mismatch = let report_label_mismatch first second ppf err = let pr fmt = Format.fprintf ppf fmt in match (err : label_mismatch) with - | Type -> pr "The types are not equal." + | Type _ -> pr "The types are not equal." | Mutability ord -> pr "%s is mutable and %s is not." (String.capitalize_ascii (choose ord first second)) @@ -212,7 +221,7 @@ let report_record_mismatch first second decl ppf err = let report_constructor_mismatch first second decl ppf err = let pr fmt = Format.fprintf ppf fmt in match (err : constructor_mismatch) with - | Type -> pr "The types are not equal." + | Type _ -> pr "The types are not equal." | Arity -> pr "They have different arities." | Inline_record err -> report_record_mismatch first second decl ppf err | Kind ord -> @@ -258,8 +267,10 @@ let report_type_mismatch0 first second decl ppf err = | Arity -> pr "They have different arities." | Privacy -> pr "A private type would be revealed." | Kind -> pr "Their kinds differ." - | Constraint -> pr "Their constraints differ." - | Manifest -> () + | Constraint _ -> pr "Their constraints differ." + | Manifest _ -> () + | Private_variant _ -> () + | Private_object _ -> () | Variance -> pr "Their variances do not agree." | Record_mismatch err -> report_record_mismatch first second decl ppf err | Variant_mismatch err -> report_variant_mismatch first second decl ppf err @@ -277,18 +288,23 @@ let report_type_mismatch0 first second decl ppf err = first let report_type_mismatch first second decl ppf err = - if err = Manifest then () else - Format.fprintf ppf "@ %a" (report_type_mismatch0 first second decl) err + match err with + | Manifest _ -> () + | Private_variant _ -> () + | Private_object _ -> () + | _ -> Format.fprintf ppf "@ %a" (report_type_mismatch0 first second decl) err let rec compare_constructor_arguments ~loc env params1 params2 arg1 arg2 = match arg1, arg2 with | Types.Cstr_tuple arg1, Types.Cstr_tuple arg2 -> if List.length arg1 <> List.length arg2 then Some (Arity : constructor_mismatch) - else if + else begin (* Ctype.equal must be called on all arguments at once, cf. PR#7378 *) - Ctype.equal env true (params1 @ arg1) (params2 @ arg2) - then None else Some Type + match Ctype.equal env true (params1 @ arg1) (params2 @ arg2) with + | exception Ctype.Equality trace -> Some (Type (env, trace)) + | () -> None + end | Types.Cstr_record l1, Types.Cstr_record l2 -> Option.map (fun rec_err -> Inline_record rec_err) @@ -298,10 +314,11 @@ let rec compare_constructor_arguments ~loc env params1 params2 arg1 arg2 = and compare_constructors ~loc env params1 params2 res1 res2 args1 args2 = match res1, res2 with - | Some r1, Some r2 -> - if Ctype.equal env true [r1] [r2] then - compare_constructor_arguments ~loc env [r1] [r2] args1 args2 - else Some Type + | Some r1, Some r2 -> begin + match Ctype.equal env true [r1] [r2] with + | exception Ctype.Equality trace -> Some (Type (env, trace)) + | () -> compare_constructor_arguments ~loc env [r1] [r2] args1 args2 + end | Some _, None -> Some (Explicit_return_type First) | None, Some _ -> Some (Explicit_return_type Second) | None, None -> @@ -332,16 +349,18 @@ and compare_variants ~loc env params1 params2 n end and compare_labels env params1 params2 - (ld1 : Types.label_declaration) - (ld2 : Types.label_declaration) = - if ld1.ld_mutable <> ld2.ld_mutable - then - let ord = if ld1.ld_mutable = Asttypes.Mutable then First else Second in - Some (Mutability ord) - else - if Ctype.equal env true (ld1.ld_type::params1) (ld2.ld_type::params2) - then None - else Some (Type : label_mismatch) + (ld1 : Types.label_declaration) (ld2 : Types.label_declaration) = + if ld1.ld_mutable <> ld2.ld_mutable then begin + let ord = if ld1.ld_mutable = Asttypes.Mutable then First else Second in + Some (Mutability ord) + end else begin + let tl1 = params1 @ [ld1.ld_type] in + let tl2 = params2 @ [ld2.ld_type] in + match Ctype.equal env true tl1 tl2 with + | exception Ctype.Equality trace -> + Some (Type (env, trace) : label_mismatch) + | () -> None + end and compare_records ~loc env params1 params2 n (labels1 : Types.label_declaration list) @@ -378,6 +397,125 @@ let compare_records_with_representation ~loc env params1 params2 n Some (Unboxed_float_representation pos) | err -> err +let private_variant env row1 params1 row2 params2 = + let r1, r2, pairs = + Ctype.merge_row_fields row1.row_fields row2.row_fields + in + let err = + if row2.row_closed && not row1.row_closed then Some Openness + else begin + match row2.row_closed, Ctype.filter_row_fields false r1 with + | true, (s, _) :: _ -> + Some (Missing (Second, s) : private_variant_mismatch) + | _, _ -> None + end + in + if err <> None then err else + let err = + let missing = + List.find_opt + (fun (_,f) -> + match Btype.row_field_repr f with + | Rabsent | Reither _ -> false + | Rpresent _ -> true) + r2 + in + match missing with + | None -> None + | Some (s, _) -> Some (Missing (First, s) : private_variant_mismatch) + in + if err <> None then err else + let rec loop tl1 tl2 pairs = + match pairs with + | [] -> begin + match Ctype.equal env true tl1 tl2 with + | exception Ctype.Equality trace -> + Some (Types (env, trace) : private_variant_mismatch) + | () -> None + end + | (s, f1, f2) :: pairs -> begin + match Btype.row_field_repr f1, Btype.row_field_repr f2 with + | Rpresent to1, Rpresent to2 -> begin + match to1, to2 with + | Some t1, Some t2 -> + loop (t1 :: tl1) (t2 :: tl2) pairs + | None, None -> + loop tl1 tl2 pairs + | Some _, None | None, Some _ -> + Some (Incompatible_types_for s) + end + | Rpresent to1, Reither(const2, tl2, _, _) -> begin + match to1, const2, tl2 with + | Some t1, false, [t2] -> loop (t1 :: tl1) (t2 :: tl2) pairs + | None, true, [] -> loop tl1 tl2 pairs + | _, _, _ -> Some (Incompatible_types_for s) + end + | Rpresent _, Rabsent -> + Some (Missing (Second, s) : private_variant_mismatch) + | Reither(const1, ts1, _, _), Reither(const2, ts2, _, _) -> + if const1 = const2 && List.length ts1 = List.length ts2 then + loop (ts1 @ tl1) (ts2 @ tl2) pairs + else + Some (Incompatible_types_for s) + | Reither _, Rpresent _ -> + Some (Presence s) + | Reither _, Rabsent -> + Some (Missing (Second, s) : private_variant_mismatch) + | Rabsent, (Reither _ | Rabsent) -> + loop tl1 tl2 pairs + | Rabsent, Rpresent _ -> + Some (Missing (First, s) : private_variant_mismatch) + end + in + loop params1 params2 pairs + +let private_object env fields1 params1 fields2 params2 = + let pairs, _miss1, miss2 = Ctype.associate_fields fields1 fields2 in + let err = + match miss2 with + | [] -> None + | (f, _, _) :: _ -> Some (Missing f) + in + if err <> None then err else + let tl1, tl2 = + List.split (List.map (fun (_,_,t1,_,t2) -> t1, t2) pairs) + in + begin + match Ctype.equal env true (params1 @ tl1) (params2 @ tl2) with + | exception Ctype.Equality trace -> Some (Types (env, trace)) + | () -> None + end + +let type_manifest env ty1 params1 ty2 params2 priv2 = + let ty1' = Ctype.expand_head env ty1 and ty2' = Ctype.expand_head env ty2 in + match ty1'.desc, ty2'.desc with + | Tvariant row1, Tvariant row2 + when is_absrow env (Btype.row_more row2) -> begin + let row1 = Btype.row_repr row1 and row2 = Btype.row_repr row2 in + assert (Ctype.is_equal env true (ty1::params1) (row2.row_more::params2)); + match private_variant env row1 params1 row2 params2 with + | None -> None + | Some err -> Some (Private_variant(ty1, ty2, err)) + end + | Tobject (fi1, _), Tobject (fi2, _) + when is_absrow env (snd (Ctype.flatten_fields fi2)) -> begin + let (fields2,rest2) = Ctype.flatten_fields fi2 in + let (fields1,_) = Ctype.flatten_fields fi1 in + assert (Ctype.is_equal env true (ty1::params1) (rest2::params2)); + match private_object env fields1 params1 fields2 params2 with + | None -> None + | Some err -> Some (Private_object(ty1, ty2, err)) + end + | _ -> begin + match + match priv2 with + | Private -> Ctype.equal_private env params1 ty1 params2 ty2 + | Public -> Ctype.equal env true (params1 @ [ty1]) (params2 @ [ty2]) + with + | exception Ctype.Equality trace -> Some (Manifest (env, trace)) + | () -> None + end + let type_declarations ?(equality = false) ~loc env ~mark name decl1 path decl2 = Builtin_attributes.check_alerts_inclusion @@ -390,20 +528,24 @@ let type_declarations ?(equality = false) ~loc env ~mark name if not (private_flags decl1 decl2) then Some Privacy else let err = match (decl1.type_manifest, decl2.type_manifest) with (_, None) -> - if Ctype.equal env true decl1.type_params decl2.type_params - then None else Some Constraint + begin + match Ctype.equal env true decl1.type_params decl2.type_params with + | exception Ctype.Equality trace -> Some (Constraint(env, trace)) + | () -> None + end | (Some ty1, Some ty2) -> - if type_manifest env ty1 decl1.type_params ty2 decl2.type_params - decl2.type_private - then None else Some Manifest + type_manifest env ty1 decl1.type_params ty2 decl2.type_params + decl2.type_private | (None, Some ty2) -> let ty1 = Btype.newgenty (Tconstr(path, decl2.type_params, ref Mnil)) in - if Ctype.equal env true decl1.type_params decl2.type_params then - if Ctype.equal env false [ty1] [ty2] then None - else Some Manifest - else Some Constraint + match Ctype.equal env true decl1.type_params decl2.type_params with + | exception Ctype.Equality trace -> Some (Constraint(env, trace)) + | () -> + match Ctype.equal env false [ty1] [ty2] with + | exception Ctype.Equality trace -> Some (Manifest(env, trace)) + | () -> None in if err <> None then err else let err = @@ -503,17 +645,21 @@ let extension_constructors ~loc env ~mark id ext1 ext2 = let ty2 = Btype.newgenty (Tconstr(ext2.ext_type_path, ext2.ext_type_params, ref Mnil)) in - if not (Ctype.equal env true (ty1 :: ext1.ext_type_params) - (ty2 :: ext2.ext_type_params)) - then Some (Constructor_mismatch (id, ext1, ext2, Type)) - else + let tl1 = ty1 :: ext1.ext_type_params in + let tl2 = ty2 :: ext2.ext_type_params in + match Ctype.equal env true tl1 tl2 with + | exception Ctype.Equality trace -> + Some (Constructor_mismatch (id, ext1, ext2, Type(env, trace))) + | () -> let r = - compare_constructors ~loc env ext1.ext_type_params ext2.ext_type_params + compare_constructors ~loc env + ext1.ext_type_params ext2.ext_type_params ext1.ext_ret_type ext2.ext_ret_type ext1.ext_args ext2.ext_args in match r with | Some r -> Some (Constructor_mismatch (id, ext1, ext2, r)) - | None -> match ext1.ext_private, ext2.ext_private with - Private, Public -> Some Constructor_privacy + | None -> + match ext1.ext_private, ext2.ext_private with + | Private, Public -> Some Constructor_privacy | _, _ -> None diff --git a/typing/includecore.mli b/typing/includecore.mli index 560d0ac193..95bcbb23cb 100644 --- a/typing/includecore.mli +++ b/typing/includecore.mli @@ -18,12 +18,25 @@ open Typedtree open Types -exception Dont_match +type position = Errortrace.position = First | Second -type position = Ctype.Unification_trace.position = First | Second +type primitive_mismatch = + | Name + | Arity + | No_alloc of position + | Native_name + | Result_repr + | Argument_repr of int + +type value_mismatch = + | Primitive_mismatch of primitive_mismatch + | Not_a_primitive + | Type of Env.t * Errortrace.comparison Errortrace.t + +exception Dont_match of value_mismatch type label_mismatch = - | Type + | Type of Env.t * Errortrace.comparison Errortrace.t | Mutability of position type record_mismatch = @@ -33,7 +46,7 @@ type record_mismatch = | Unboxed_float_representation of position type constructor_mismatch = - | Type + | Type of Env.t * Errortrace.comparison Errortrace.t | Arity | Inline_record of record_mismatch | Kind of position @@ -53,12 +66,25 @@ type extension_constructor_mismatch = * extension_constructor * constructor_mismatch +type private_variant_mismatch = + | Openness + | Missing of position * string + | Presence of string + | Incompatible_types_for of string + | Types of Env.t * Errortrace.comparison Errortrace.t + +type private_object_mismatch = + | Missing of string + | Types of Env.t * Errortrace.comparison Errortrace.t + type type_mismatch = | Arity | Privacy | Kind - | Constraint - | Manifest + | Constraint of Env.t * Errortrace.comparison Errortrace.t + | Manifest of Env.t * Errortrace.comparison Errortrace.t + | Private_variant of type_expr * type_expr * private_variant_mismatch + | Private_object of type_expr * type_expr * private_object_mismatch | Variance | Record_mismatch of record_mismatch | Variant_mismatch of variant_mismatch diff --git a/typing/includemod.ml b/typing/includemod.ml index 9cfb8ebde4..1b542d5f5d 100644 --- a/typing/includemod.ml +++ b/typing/includemod.ml @@ -22,6 +22,7 @@ open Types type symptom = Missing_field of Ident.t * Location.t * string (* kind *) | Value_descriptions of Ident.t * value_description * value_description + * Includecore.value_mismatch | Type_declarations of Ident.t * type_declaration * type_declaration * Includecore.type_mismatch | Extension_constructors of Ident.t * extension_constructor @@ -158,7 +159,7 @@ let value_descriptions ~loc env ~mark subst id vd1 vd2 = let vd2 = Subst.value_description subst vd2 in try Ok (Includecore.value_descriptions ~loc env (Ident.name id) vd1 vd2) - with Includecore.Dont_match -> + with Includecore.Dont_match _err -> Error Error.(Core (Value_descriptions (sdiff vd1 vd2))) (* Inclusion between type declarations *) @@ -983,7 +984,6 @@ module Functor_app_diff = struct end - (* Hide the context and substitution parameters to the outside world *) let modtypes ~loc env ~mark mty1 mty2 = diff --git a/typing/includemod.mli b/typing/includemod.mli index 060ed0cc4e..f4bd3a6f11 100644 --- a/typing/includemod.mli +++ b/typing/includemod.mli @@ -178,7 +178,9 @@ val print_coercion: Format.formatter -> module_coercion -> unit type symptom = Missing_field of Ident.t * Location.t * string (* kind *) - | Value_descriptions of Ident.t * value_description * value_description + | Value_descriptions of + Ident.t * value_description * value_description + * Includecore.value_mismatch | Type_declarations of Ident.t * type_declaration * type_declaration * Includecore.type_mismatch | Extension_constructors of Ident.t * extension_constructor diff --git a/typing/mtype.ml b/typing/mtype.ml index 07b28b34ae..3af072e876 100644 --- a/typing/mtype.ml +++ b/typing/mtype.ml @@ -54,9 +54,8 @@ and strengthen_sig ~aliasable env sg p = [] -> [] | (Sig_value(_, _, _) as sigelt) :: rem -> sigelt :: strengthen_sig ~aliasable env rem p - | Sig_type(id, {type_kind=Type_abstract}, _, _) :: - (Sig_type(id', {type_private=Private}, _, _) :: _ as rem) - when Ident.name id = Ident.name id' ^ "#row" -> + | Sig_type(id, {type_kind=Type_abstract}, _, _) :: rem + when Btype.is_row_name (Ident.name id) -> strengthen_sig ~aliasable env rem p | Sig_type(id, decl, rs, vis) :: rem -> let newdecl = @@ -236,11 +235,14 @@ let enrich_typedecl env p id decl = match decl.type_manifest with Some _ -> decl | None -> - try - let orig_decl = Env.find_type p env in + match Env.find_type p env with + | exception Not_found -> decl + (* Type which was not present in the signature, so we don't have + anything to do. *) + | orig_decl -> if decl.type_arity <> orig_decl.type_arity then decl - else + else begin let orig_ty = Ctype.reify_univars env (Btype.newgenty(Tconstr(p, orig_decl.type_params, ref Mnil))) @@ -250,19 +252,18 @@ let enrich_typedecl env p id decl = (Btype.newgenty(Tconstr(Pident id, decl.type_params, ref Mnil))) in let env = Env.add_type ~check:false id decl env in - Ctype.mcomp env orig_ty new_ty; - let orig_ty = - Btype.newgenty(Tconstr(p, decl.type_params, ref Mnil)) - in - {decl with type_manifest = Some orig_ty} - with Not_found | Ctype.Unify _ -> - (* - Not_found: type which was not present in the signature, so we don't - have anything to do. - - Unify: the current declaration is not compatible with the one we - got from the signature. We should just fail now, but then, we could - also have failed if the arities of the two decls were different, - which we didn't. *) - decl + match Ctype.mcomp env orig_ty new_ty with + | exception Ctype.Incompatible -> decl + (* The current declaration is not compatible with the one we got + from the signature. We should just fail now, but then, we could + also have failed if the arities of the two decls were + different, which we didn't. *) + | () -> + let orig_ty = + Btype.newgenty(Tconstr(p, decl.type_params, ref Mnil)) + in + {decl with type_manifest = Some orig_ty} + end let rec enrich_modtype env p mty = match mty with diff --git a/typing/primitive.ml b/typing/primitive.ml index 0c3372b98e..bf4fe83248 100644 --- a/typing/primitive.ml +++ b/typing/primitive.ml @@ -200,6 +200,30 @@ let native_name p = let byte_name p = p.prim_name +let equal_boxed_integer bi1 bi2 = + match bi1, bi2 with + | Pnativeint, Pnativeint + | Pint32, Pint32 + | Pint64, Pint64 -> + true + | (Pnativeint | Pint32 | Pint64), _ -> + false + +let equal_native_repr nr1 nr2 = + match nr1, nr2 with + | Same_as_ocaml_repr, Same_as_ocaml_repr -> true + | Same_as_ocaml_repr, + (Unboxed_float | Unboxed_integer _ | Untagged_int) -> false + | Unboxed_float, Unboxed_float -> true + | Unboxed_float, + (Same_as_ocaml_repr | Unboxed_integer _ | Untagged_int) -> false + | Unboxed_integer bi1, Unboxed_integer bi2 -> equal_boxed_integer bi1 bi2 + | Unboxed_integer _, + (Same_as_ocaml_repr | Unboxed_float | Untagged_int) -> false + | Untagged_int, Untagged_int -> true + | Untagged_int, + (Same_as_ocaml_repr | Unboxed_float | Unboxed_integer _) -> false + let native_name_is_external p = let nat_name = native_name p in nat_name <> "" && nat_name.[0] <> '%' diff --git a/typing/primitive.mli b/typing/primitive.mli index ddd3977964..e8376ad552 100644 --- a/typing/primitive.mli +++ b/typing/primitive.mli @@ -63,6 +63,9 @@ val print val native_name: description -> string val byte_name: description -> string +val equal_boxed_integer : boxed_integer -> boxed_integer -> bool +val equal_native_repr : native_repr -> native_repr -> bool + (** [native_name_is_externa] returns [true] iff the [native_name] for the given primitive identifies that the primitive is not implemented in the compiler itself. *) diff --git a/typing/printtyp.ml b/typing/printtyp.ml index 69b424278b..8668af77f4 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -1974,9 +1974,7 @@ let type_expansion ppf = function | Diff(t,t') -> fprintf ppf "@[<2>%a@ =@ %a@]" !Oprint.out_type t !Oprint.out_type t' -module Trace = Ctype.Unification_trace - -let trees_of_trace = List.map (Trace.map_diff trees_of_type_expansion) +let trees_of_trace = List.map (Errortrace.map_diff trees_of_type_expansion) let trees_of_type_path_expansion (tp,tp') = if Path.same tp tp' then Same(tree_of_path Type tp) else @@ -1990,14 +1988,13 @@ let type_path_expansion ppf = function !Oprint.out_ident p' let rec trace fst txt ppf = function - | {Trace.got; expected} :: rem -> + | {Errortrace.got; expected} :: rem -> if not fst then fprintf ppf "@,"; fprintf ppf "@[Type@;<1 2>%a@ %s@;<1 2>%a@] %a" type_expansion got txt type_expansion expected (trace false txt) rem | _ -> () - type printing_status = | Discard | Keep @@ -2010,36 +2007,60 @@ type printing_status = type error. *) -let printing_status = function - | Trace.(Diff { got=t1, t1'; expected=t2, t2'}) -> - if is_constr_row ~allow_ident:true t1' - || is_constr_row ~allow_ident:true t2' - then Discard - else if same_path t1 t1' && same_path t2 t2' then Optional_refinement - else Keep +let diff_printing_status { Errortrace.got=t1, t1'; expected=t2, t2'} = + if is_constr_row ~allow_ident:true t1' + || is_constr_row ~allow_ident:true t2' + then Discard + else if same_path t1 t1' && same_path t2 t2' then Optional_refinement + else Keep + +(* A configuration type that controls which trace we print. This could be + exposed, but we instead expose three separate + [report_{unification,equality,moregen}_error] functions. This also lets us + give the unification case an extra optional argument without adding it to the + equality and moregen cases. *) +type 'variety trace_format = + | Unification : Errortrace.unification trace_format + | Equality : Errortrace.comparison trace_format + | Moregen : Errortrace.comparison trace_format + +let incompatibility_phrase (type variety) : variety trace_format -> string = + function + | Unification -> "is not compatible with type" + | Equality -> "is not equal to type" + | Moregen -> "is not compatible with type" + +let printing_status = function + | Errortrace.Diff d -> diff_printing_status d + | Errortrace.Escape {kind = Constraint} -> Keep | _ -> Keep (** Flatten the trace and remove elements that are always discarded during printing *) -let prepare_trace f tr = + +(* Takes [printing_status] to change behavior for [Subtype] *) +let prepare_any_trace printing_status tr = let clean_trace x l = match printing_status x with | Keep -> x :: l | Optional_refinement when l = [] -> [x] | Optional_refinement | Discard -> l in - match Trace.flatten f tr with + match tr with | [] -> [] - | elt :: rem -> (* the first element is always kept *) - elt :: List.fold_right clean_trace rem [] + | elt :: rem -> elt :: List.fold_right clean_trace rem [] + +let prepare_trace f tr = + prepare_any_trace printing_status (Errortrace.flatten f tr) (** Keep elements that are not [Diff _ ] and take the decision for the last element, require a prepared trace *) -let rec filter_trace keep_last = function +let rec filter_trace trace_format keep_last = function | [] -> [] - | [Trace.Diff d as elt] when printing_status elt = Optional_refinement -> - if keep_last then [d] else [] - | Trace.Diff d :: rem -> d :: filter_trace keep_last rem - | _ :: rem -> filter_trace keep_last rem + | [Errortrace.Diff d as elt] + when printing_status elt = Optional_refinement -> + if keep_last then [d] else [] + | Errortrace.Diff d :: rem -> d :: filter_trace trace_format keep_last rem + | _ :: rem -> filter_trace trace_format keep_last rem let type_path_list = Format.pp_print_list ~pp_sep:(fun ppf () -> Format.pp_print_break ppf 2 0) @@ -2066,6 +2087,8 @@ let may_prepare_expansion compact (t, t') = mark_loops t; (t, t) | _ -> prepare_expansion (t, t') +let print_path p = Format.dprintf "%a" !Oprint.out_ident (tree_of_path Type p) + let print_tag ppf = fprintf ppf "`%s" let print_tags = @@ -2102,118 +2125,129 @@ let explanation_diff env t3 t4 : (Format.formatter -> unit) option = | _ -> None -let print_pos ppf = function - | Trace.First -> fprintf ppf "first" - | Trace.Second -> fprintf ppf "second" - let explain_fixed_row_case ppf = function - | Trace.Cannot_be_closed -> Format.fprintf ppf "it cannot be closed" - | Trace.Cannot_add_tags tags -> - Format.fprintf ppf "it may not allow the tag(s) %a" - print_tags tags + | Errortrace.Cannot_be_closed -> + fprintf ppf "it cannot be closed" + | Errortrace.Cannot_add_tags tags -> + fprintf ppf "it may not allow the tag(s) %a" print_tags tags let explain_fixed_row pos expl = match expl with - | Types.Fixed_private -> - dprintf "The %a variant type is private" print_pos pos - | Types.Univar x -> - dprintf "The %a variant type is bound to the universal type variable %a" - print_pos pos type_expr x - | Types.Reified p -> - let p = tree_of_path Type p in - dprintf "The %a variant type is bound to %a" print_pos pos - !Oprint.out_ident p - | Types.Rigid -> ignore - -let explain_variant = function - | Trace.No_intersection -> + | Fixed_private -> + dprintf "The %a variant type is private" Errortrace.print_pos pos + | Univar x -> + dprintf "The %a variant type is bound to the universal type variable %a" + Errortrace.print_pos pos type_expr x + | Reified p -> + dprintf "The %a variant type is bound to %t" + Errortrace.print_pos pos (print_path p) + | Rigid -> ignore + +let explain_variant (type variety) : variety Errortrace.variant -> _ = function + (* Common *) + | Errortrace.Incompatible_types_for s -> + Some(dprintf "@,Types for tag `%s are incompatible" s) + (* Unification *) + | Errortrace.No_intersection -> Some(dprintf "@,These two variant types have no intersection") - | Trace.No_tags(pos,fields) -> Some( + | Errortrace.No_tags(pos,fields) -> Some( dprintf "@,@[The %a variant type does not allow tag(s)@ @[<hov>%a@]@]" - print_pos pos + Errortrace.print_pos pos print_tags (List.map fst fields) ) - | Trace.Incompatible_types_for s -> - Some(dprintf "@,Types for tag `%s are incompatible" s) - | Trace.Fixed_row (pos, k, (Univar _ | Reified _ | Fixed_private as e)) -> + | Errortrace.Fixed_row (pos, + k, + (Univar _ | Reified _ | Fixed_private as e)) -> Some ( dprintf "@,@[%t,@ %a@]" (explain_fixed_row pos e) explain_fixed_row_case k ) - | Trace.Fixed_row (_,_, Rigid) -> + | Errortrace.Fixed_row (_,_, Rigid) -> (* this case never happens *) None - - -let explain_escape intro prev ctx e = - let pre = match ctx with - | Some ctx -> dprintf "@[%t@;<1 2>%a@]" intro type_expr ctx - | None -> match e, prev with - | Trace.Univ _, Some(Trace.Incompatible_fields {name; diff}) -> - dprintf "@,@[The method %s has type@ %a,@ \ - but the expected method type was@ %a@]" name - type_expr diff.Trace.got type_expr diff.Trace.expected - | _ -> ignore in - match e with - | Trace.Univ u -> Some( + (* Equality & Moregen *) + | Errortrace.Openness pos -> + Some(dprintf "@,The %a variant type is open and the %a is not" + Errortrace.print_pos pos + Errortrace.print_pos (Errortrace.swap_position pos)) + +let explain_escape pre = function + | Errortrace.Univ u -> Some( dprintf "%t@,The universal variable %a would escape its scope" pre type_expr u) - | Trace.Constructor p -> Some( + | Errortrace.Constructor p -> Some( dprintf "%t@,@[The type constructor@;<1 2>%a@ would escape its scope@]" pre path p ) - | Trace.Module_type p -> Some( + | Errortrace.Module_type p -> Some( dprintf "%t@,@[The module type@;<1 2>%a@ would escape its scope@]" pre path p ) - | Trace.Equation (_,t) -> Some( + | Errortrace.Equation (_,t) -> Some( dprintf "%t @,@[<hov>This instance of %a is ambiguous:@ %s@]" pre type_expr t "it would escape the scope of its equation" ) - | Trace.Self -> + | Errortrace.Self -> Some (dprintf "%t@,Self type cannot escape its class" pre) + | Errortrace.Constraint -> + None - -let explain_object = function - | Trace.Self_cannot_be_closed -> - Some (dprintf "@,Self type cannot be unified with a closed object type") - | Trace.Missing_field (pos,f) -> - Some(dprintf "@,@[The %a object type has no method %s@]" print_pos pos f) - | Trace.Abstract_row pos -> Some( +let explain_object (type variety) : variety Errortrace.obj -> _ = function + | Errortrace.Missing_field (pos,f) -> Some( + dprintf "@,@[The %a object type has no method %s@]" + Errortrace.print_pos pos f + ) + | Errortrace.Abstract_row pos -> Some( dprintf "@,@[The %a object type has an abstract row, it cannot be closed@]" - print_pos pos + Errortrace.print_pos pos ) + | Errortrace.Self_cannot_be_closed -> + Some (dprintf "@,Self type cannot be unified with a closed object type") - -let explanation intro prev env = function - | Trace.Diff { Trace.got = _, s; expected = _,t } -> explanation_diff env s t - | Trace.Escape {kind;context} -> explain_escape intro prev context kind - | Trace.Incompatible_fields { name; _ } -> - Some(dprintf "@,Types for method %s are incompatible" name) - | Trace.Variant v -> explain_variant v - | Trace.Obj o -> explain_object o - | Trace.Rec_occur(x,y) -> - reset_and_mark_loops y; - begin match x.desc with - | Tvar _ | Tunivar _ -> - Some(dprintf "@,@[<hov>The type variable %a occurs inside@ %a@]" - marked_type_expr x marked_type_expr y) - | _ -> - (* We had a delayed unification of the type variable with - a non-variable after the occur check. *) - Some ignore - (* There is no need to search further for an explanation, but - we don't want to print a message of the form: - {[ The type int occurs inside int list -> 'a |} - *) - end +let explanation (type variety) intro prev env + : ('a, variety) Errortrace.elt -> _ = function + | Errortrace.Diff { Errortrace.got = _,s; expected = _,t } -> + explanation_diff env s t + | Errortrace.Escape {kind;context} -> + let pre = + match context, kind, prev with + | Some ctx, _, _ -> + dprintf "@[%t@;<1 2>%a@]" intro type_expr ctx + | None, Univ _, Some(Errortrace.Incompatible_fields {name; diff}) -> + dprintf "@,@[The method %s has type@ %a,@ \ + but the expected method type was@ %a@]" + name type_expr diff.got type_expr diff.expected + | _ -> ignore + in + explain_escape pre kind + | Errortrace.Incompatible_fields { name; _ } -> + Some(dprintf "@,Types for method %s are incompatible" name) + | Errortrace.Variant v -> + explain_variant v + | Errortrace.Obj o -> + explain_object o + | Errortrace.Rec_occur(x,y) -> + reset_and_mark_loops y; + begin match x.desc with + | Tvar _ | Tunivar _ -> + Some(dprintf "@,@[<hov>The type variable %a occurs inside@ %a@]" + type_expr x type_expr y) + | _ -> + (* We had a delayed unification of the type variable with + a non-variable after the occur check. *) + Some ignore + (* There is no need to search further for an explanation, but + we don't want to print a message of the form: + {[ The type int occurs inside int list -> 'a |} + *) + end let mismatch intro env trace = - Trace.explain trace (fun ~prev h -> explanation intro prev env h) + Errortrace.explain trace (fun ~prev h -> explanation intro prev env h) let explain mis ppf = match mis with @@ -2233,27 +2267,26 @@ let warn_on_missing_def env ppf t = end | _ -> () - let prepare_expansion_head empty_tr = function - | Trace.Diff d -> - Some(Trace.map_diff (may_prepare_expansion empty_tr) d) + | Errortrace.Diff d -> + Some (Errortrace.map_diff (may_prepare_expansion empty_tr) d) | _ -> None let head_error_printer txt_got txt_but = function | None -> ignore | Some d -> - let d = Trace.map_diff trees_of_type_expansion d in + let d = Errortrace.map_diff trees_of_type_expansion d in dprintf "%t@;<1 2>%a@ %t@;<1 2>%a" - txt_got type_expansion d.Trace.got - txt_but type_expansion d.Trace.expected + txt_got type_expansion d.Errortrace.got + txt_but type_expansion d.Errortrace.expected let warn_on_missing_defs env ppf = function | None -> () - | Some {Trace.got=te1,_; expected=te2,_ } -> + | Some {Errortrace.got=te1,_; expected=te2,_ } -> warn_on_missing_def env ppf te1; warn_on_missing_def env ppf te2 -let unification_error env tr txt1 ppf txt2 ty_expect_explanation = +let error trace_format env tr txt1 ppf txt2 ty_expect_explanation = reset (); let tr = prepare_trace (fun t t' -> t, hide_variant_name t') tr in let mis = mismatch txt1 env tr in @@ -2262,9 +2295,9 @@ let unification_error env tr txt1 ppf txt2 ty_expect_explanation = | elt :: tr -> try print_labels := not !Clflags.classic; - let tr = filter_trace (mis = None) tr in + let tr = filter_trace trace_format (mis = None) tr in let head = prepare_expansion_head (tr=[]) elt in - let tr = List.map (Trace.map_diff prepare_expansion) tr in + let tr = List.map (Errortrace.map_diff prepare_expansion) tr in let head_error = head_error_printer txt1 txt2 head in let tr = trees_of_trace tr in fprintf ppf @@ -2273,7 +2306,7 @@ let unification_error env tr txt1 ppf txt2 ty_expect_explanation = @]" head_error ty_expect_explanation - (trace false "is not compatible with type") tr + (trace false (incompatibility_phrase trace_format)) tr (explain mis); if env <> Env.empty then warn_on_missing_defs env ppf head; @@ -2283,51 +2316,98 @@ let unification_error env tr txt1 ppf txt2 ty_expect_explanation = print_labels := true; raise exn -let report_unification_error ppf env tr - ?(type_expected_explanation = fun _ -> ()) - txt1 txt2 = - wrap_printing_env env (fun () -> unification_error env tr txt1 ppf txt2 - type_expected_explanation) +let report_error trace_format ppf env tr + ?(type_expected_explanation = fun _ -> ()) + txt1 txt2 = + wrap_printing_env env (fun () -> error trace_format env tr txt1 ppf txt2 + type_expected_explanation) ~error:true -;; - -(** [trace] requires the trace to be prepared *) -let trace fst keep_last txt ppf tr = - print_labels := not !Clflags.classic; - try match tr with - | elt :: tr' -> - let elt = match elt with - | Trace.Diff diff -> [Trace.map_diff trees_of_type_expansion diff] - | _ -> [] in + +let report_unification_error = + report_error Unification +let report_equality_error = + report_error Equality ?type_expected_explanation:None +let report_moregen_error = + report_error Moregen ?type_expected_explanation:None + +module Subtype = struct + (* There's a frustrating amount of code duplication between this module and + the outside code, particularly in [prepare_trace] and [filter_trace]. + Unfortunately, [Subtype] is *just* similar enough to have code duplication, + while being *just* different enough (it's only [Diff]) for the abstraction + to be nonobvious. Someday, perhaps... *) + + let printing_status = function + | Errortrace.Subtype.Diff d -> diff_printing_status d + + let prepare_unification_trace = prepare_trace + + let prepare_trace f tr = + prepare_any_trace printing_status (Errortrace.Subtype.flatten f tr) + + let trace filter_trace get_diff fst keep_last txt ppf tr = + print_labels := not !Clflags.classic; + try match tr with + | elt :: tr' -> + let diffed_elt = get_diff elt in let tr = trees_of_trace - @@ List.map (Trace.map_diff prepare_expansion) + @@ List.map (Errortrace.map_diff prepare_expansion) @@ filter_trace keep_last tr' in - if fst then trace fst txt ppf (elt @ tr) - else trace fst txt ppf tr; - print_labels := true - | _ -> () - with exn -> - print_labels := true; - raise exn - -let report_subtyping_error ppf env tr1 txt1 tr2 = - wrap_printing_env ~error:true env (fun () -> - reset (); - let tr1 = prepare_trace (fun t t' -> prepare_expansion (t, t')) tr1 in - let tr2 = prepare_trace (fun t t' -> prepare_expansion (t, t')) tr2 in - let keep_first = match tr2 with - | Trace.[Obj _ | Variant _ | Escape _ ] | [] -> true - | _ -> false in - fprintf ppf "@[<v>%a" (trace true keep_first txt1) tr1; - if tr2 = [] then fprintf ppf "@]" else - let mis = mismatch (dprintf "Within this type") env tr2 in - fprintf ppf "%a%t%t@]" - (trace false (mis = None) "is not compatible with type") tr2 - (explain mis) - Conflicts.print_explanations - ) + let tr = + match fst, diffed_elt with + | true, Some elt -> elt :: tr + | _, _ -> tr + in + trace fst txt ppf tr; + print_labels := true + | _ -> () + with exn -> + print_labels := true; + raise exn + let filter_unification_trace = filter_trace Unification + + let rec filter_subtype_trace keep_last = function + | [] -> [] + | [Errortrace.Subtype.Diff d as elt] + when printing_status elt = Optional_refinement -> + if keep_last then [d] else [] + | Errortrace.Subtype.Diff d :: rem -> + d :: filter_subtype_trace keep_last rem + + let unification_get_diff = function + | Errortrace.Diff diff -> + Some (Errortrace.map_diff trees_of_type_expansion diff) + | _ -> None + + let subtype_get_diff = function + | Errortrace.Subtype.Diff diff -> + Some (Errortrace.map_diff trees_of_type_expansion diff) + + let report_error ppf env tr1 txt1 tr2 = + wrap_printing_env ~error:true env (fun () -> + reset (); + let tr1 = + prepare_trace (fun t t' -> prepare_expansion (t, t')) tr1 + in + let tr2 = + prepare_unification_trace (fun t t' -> prepare_expansion (t, t')) tr2 + in + let keep_first = match tr2 with + | [Obj _ | Variant _ | Escape _ ] | [] -> true + | _ -> false in + fprintf ppf "@[<v>%a" + (trace filter_subtype_trace subtype_get_diff true keep_first txt1) tr1; + if tr2 = [] then fprintf ppf "@]" else + let mis = mismatch (dprintf "Within this type") env tr2 in + fprintf ppf "%a%t%t@]" + (trace filter_unification_trace unification_get_diff false + (mis = None) "is not compatible with type") tr2 + (explain mis) + Conflicts.print_explanations + ) +end let report_ambiguous_type_error ppf env tp0 tpl txt1 txt2 txt3 = wrap_printing_env ~error:true env (fun () -> diff --git a/typing/printtyp.mli b/typing/printtyp.mli index 03fcb5ee5b..01c76c89c7 100644 --- a/typing/printtyp.mli +++ b/typing/printtyp.mli @@ -173,22 +173,39 @@ val tree_of_cltype_declaration: val cltype_declaration: Ident.t -> formatter -> class_type_declaration -> unit val type_expansion: type_expr -> Format.formatter -> type_expr -> unit val prepare_expansion: type_expr * type_expr -> type_expr * type_expr -val trace: - bool -> bool-> string -> formatter - -> (type_expr * type_expr) Ctype.Unification_trace.elt list -> unit -val report_unification_error: - formatter -> Env.t -> - Ctype.Unification_trace.t -> - ?type_expected_explanation:(formatter -> unit) -> - (formatter -> unit) -> (formatter -> unit) -> - unit -val report_subtyping_error: - formatter -> Env.t -> Ctype.Unification_trace.t -> string - -> Ctype.Unification_trace.t -> unit val report_ambiguous_type_error: formatter -> Env.t -> (Path.t * Path.t) -> (Path.t * Path.t) list -> (formatter -> unit) -> (formatter -> unit) -> (formatter -> unit) -> unit +val report_unification_error : + formatter -> Env.t -> + Errortrace.unification Errortrace.t -> + ?type_expected_explanation:(formatter -> unit) -> + (formatter -> unit) -> (formatter -> unit) -> + unit + +val report_equality_error : + formatter -> Env.t -> + Errortrace.comparison Errortrace.t -> + (formatter -> unit) -> (formatter -> unit) -> + unit + +val report_moregen_error : + formatter -> Env.t -> + Errortrace.comparison Errortrace.t -> + (formatter -> unit) -> (formatter -> unit) -> + unit + +module Subtype : sig + val report_error : + formatter -> + Env.t -> + Errortrace.Subtype.t -> + string -> + Errortrace.unification Errortrace.t -> + unit +end + (* for toploop *) val print_items: (Env.t -> signature_item -> 'a option) -> Env.t -> signature_item list -> (out_sig_item * 'a option) list diff --git a/typing/typeclass.ml b/typing/typeclass.ml index 7bcdc59de5..8d76f5343b 100644 --- a/typing/typeclass.ml +++ b/typing/typeclass.ml @@ -66,8 +66,8 @@ type 'a full_class = { type class_env = { val_env : Env.t; met_env : Env.t; par_env : Env.t } type error = - Unconsistent_constraint of Ctype.Unification_trace.t - | Field_type_mismatch of string * string * Ctype.Unification_trace.t + | Unconsistent_constraint of Errortrace.unification Errortrace.t + | Field_type_mismatch of string * string * Errortrace.unification Errortrace.t | Structure_expected of class_type | Cannot_apply of class_type | Apply_wrong_label of arg_label @@ -76,10 +76,10 @@ type error = | Unbound_class_2 of Longident.t | Unbound_class_type_2 of Longident.t | Abbrev_type_clash of type_expr * type_expr * type_expr - | Constructor_type_mismatch of string * Ctype.Unification_trace.t + | Constructor_type_mismatch of string * Errortrace.unification Errortrace.t | Virtual_class of bool * bool * string list * string list | Parameter_arity_mismatch of Longident.t * int * int - | Parameter_mismatch of Ctype.Unification_trace.t + | Parameter_mismatch of Errortrace.unification Errortrace.t | Bad_parameters of Ident.t * type_expr * type_expr | Class_match_failure of Ctype.class_match_failure list | Unbound_val of string @@ -87,8 +87,8 @@ type error = | Non_generalizable_class of Ident.t * Types.class_declaration | Cannot_coerce_self of type_expr | Non_collapsable_conjunction of - Ident.t * Types.class_declaration * Ctype.Unification_trace.t - | Final_self_clash of Ctype.Unification_trace.t + Ident.t * Types.class_declaration * Errortrace.unification Errortrace.t + | Final_self_clash of Errortrace.unification Errortrace.t | Mutability_mismatch of string * mutable_flag | No_overriding of string * string | Duplicate of string * string @@ -309,7 +309,6 @@ let inheritance self_type env ovf concr_meths warn_vals loc parent = begin try Ctype.unify env self_type cl_sig.csig_self with Ctype.Unify trace -> - let open Ctype.Unification_trace in match trace with | Diff _ :: Incompatible_fields {name = n; _ } :: rem -> raise(Error(loc, env, Field_type_mismatch ("method", n, rem))) @@ -1889,10 +1888,11 @@ let report_error env ppf = function | Repeated_parameter -> fprintf ppf "A type parameter occurs several times" | Unconsistent_constraint trace -> - fprintf ppf "The class constraints are not consistent.@."; + fprintf ppf "@[<v>The class constraints are not consistent.@ "; Printtyp.report_unification_error ppf env trace (fun ppf -> fprintf ppf "Type") - (fun ppf -> fprintf ppf "is not compatible with type") + (fun ppf -> fprintf ppf "is not compatible with type"); + fprintf ppf "@]" | Field_type_mismatch (k, m, trace) -> Printtyp.report_unification_error ppf env trace (function ppf -> diff --git a/typing/typeclass.mli b/typing/typeclass.mli index c3503526ae..ac8eb06ec5 100644 --- a/typing/typeclass.mli +++ b/typing/typeclass.mli @@ -90,8 +90,8 @@ val type_classes : *) type error = - Unconsistent_constraint of Ctype.Unification_trace.t - | Field_type_mismatch of string * string * Ctype.Unification_trace.t + | Unconsistent_constraint of Errortrace.unification Errortrace.t + | Field_type_mismatch of string * string * Errortrace.unification Errortrace.t | Structure_expected of class_type | Cannot_apply of class_type | Apply_wrong_label of arg_label @@ -100,10 +100,10 @@ type error = | Unbound_class_2 of Longident.t | Unbound_class_type_2 of Longident.t | Abbrev_type_clash of type_expr * type_expr * type_expr - | Constructor_type_mismatch of string * Ctype.Unification_trace.t + | Constructor_type_mismatch of string * Errortrace.unification Errortrace.t | Virtual_class of bool * bool * string list * string list | Parameter_arity_mismatch of Longident.t * int * int - | Parameter_mismatch of Ctype.Unification_trace.t + | Parameter_mismatch of Errortrace.unification Errortrace.t | Bad_parameters of Ident.t * type_expr * type_expr | Class_match_failure of Ctype.class_match_failure list | Unbound_val of string @@ -111,8 +111,8 @@ type error = | Non_generalizable_class of Ident.t * Types.class_declaration | Cannot_coerce_self of type_expr | Non_collapsable_conjunction of - Ident.t * Types.class_declaration * Ctype.Unification_trace.t - | Final_self_clash of Ctype.Unification_trace.t + Ident.t * Types.class_declaration * Errortrace.unification Errortrace.t + | Final_self_clash of Errortrace.unification Errortrace.t | Mutability_mismatch of string * mutable_flag | No_overriding of string * string | Duplicate of string * string diff --git a/typing/typecore.ml b/typing/typecore.ml index bcc48a01fc..dd7d34b36e 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -76,14 +76,14 @@ type existential_restriction = type error = | Constructor_arity_mismatch of Longident.t * int * int - | Label_mismatch of Longident.t * Ctype.Unification_trace.t + | Label_mismatch of Longident.t * Errortrace.unification Errortrace.t | Pattern_type_clash : - Ctype.Unification_trace.t * _ pattern_desc option -> error - | Or_pattern_type_clash of Ident.t * Ctype.Unification_trace.t + Errortrace.unification Errortrace.t * _ pattern_desc option -> error + | Or_pattern_type_clash of Ident.t * Errortrace.unification Errortrace.t | Multiply_bound_variable of string | Orpat_vars of Ident.t * Ident.t list | Expr_type_clash of - Ctype.Unification_trace.t * type_forcing_context option + Errortrace.unification Errortrace.t * type_forcing_context option * expression_desc option | Apply_non_function of type_expr | Apply_wrong_label of arg_label * type_expr * bool @@ -102,17 +102,17 @@ type error = | Private_constructor of constructor_description * type_expr | Unbound_instance_variable of string * string list | Instance_variable_not_mutable of string - | Not_subtype of Ctype.Unification_trace.t * Ctype.Unification_trace.t + | Not_subtype of Errortrace.Subtype.t * Errortrace.unification Errortrace.t | Outside_class | Value_multiply_overridden of string | Coercion_failure of - type_expr * type_expr * Ctype.Unification_trace.t * bool + type_expr * type_expr * Errortrace.unification Errortrace.t * bool | Too_many_arguments of bool * type_expr * type_forcing_context option | Abstract_wrong_label of arg_label * type_expr * type_forcing_context option | Scoping_let_module of string * type_expr | Not_a_variant_type of Longident.t | Incoherent_label_order - | Less_general of string * Ctype.Unification_trace.t + | Less_general of string * Errortrace.unification Errortrace.t | Modules_not_allowed | Cannot_infer_signature | Not_a_packed_module of type_expr @@ -134,9 +134,9 @@ type error = | Illegal_letrec_pat | Illegal_letrec_expr | Illegal_class_expr - | Letop_type_clash of string * Ctype.Unification_trace.t - | Andop_type_clash of string * Ctype.Unification_trace.t - | Bindings_type_clash of Ctype.Unification_trace.t + | Letop_type_clash of string * Errortrace.unification Errortrace.t + | Andop_type_clash of string * Errortrace.unification Errortrace.t + | Bindings_type_clash of Errortrace.unification Errortrace.t | Unbound_existential of Ident.t list * type_expr | Missing_type_constraint @@ -1294,8 +1294,8 @@ let rec has_literal_pattern p = match p.ppat_desc with 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))) + with Escape trace -> + raise(Error(loc, env, Pattern_type_clash([Escape trace], None))) type pattern_checking_mode = | Normal @@ -2482,7 +2482,7 @@ let check_univars env kind exp ty_expected vars = if not complete then let ty_expected = instance ty_expected in raise (Error (exp.exp_loc, env, - Less_general(kind, [Unification_trace.diff ty ty_expected]))) + Less_general(kind, [Errortrace.diff ty ty_expected]))) let generalize_and_check_univars env kind exp ty_expected vars = generalize exp.exp_type; @@ -5351,7 +5351,7 @@ let longident = Printtyp.longident (* Returns the first diff of the trace *) let type_clash_of_trace trace = - Ctype.Unification_trace.(explain trace (fun ~prev:_ -> function + Errortrace.(explain trace (fun ~prev:_ -> function | Diff diff -> Some diff | _ -> None )) @@ -5383,8 +5383,7 @@ let report_literal_type_constraint expected_type const = | _, _ -> [] let report_literal_type_constraint const = function - | Some Unification_trace. - { expected = { t = { desc = Tconstr (typ, [], _) } } } -> + | Some Errortrace.{ expected = { t = { desc = Tconstr (typ, [], _) } } } -> report_literal_type_constraint typ const | Some _ | None -> [] @@ -5451,14 +5450,12 @@ let report_error ~loc env = function | Pattern_type_clash (trace, pat) -> let diff = type_clash_of_trace trace in let sub = report_pattern_type_clash_hints pat diff in - Location.error_of_printer ~loc ~sub (fun ppf () -> - Printtyp.report_unification_error ppf env trace - (function ppf -> - fprintf ppf "This pattern matches values of type") - (function ppf -> - fprintf ppf "but a pattern was expected which matches values of \ - type"); - ) () + report_unification_error ~loc ~sub env trace + (function ppf -> + fprintf ppf "This pattern matches values of type") + (function ppf -> + fprintf ppf "but a pattern was expected which matches values of \ + type"); | Or_pattern_type_clash (id, trace) -> report_unification_error ~loc env trace (function ppf -> @@ -5480,15 +5477,13 @@ let report_error ~loc env = function | Expr_type_clash (trace, explanation, exp) -> let diff = type_clash_of_trace trace in let sub = report_expr_type_clash_hints exp diff in - Location.error_of_printer ~loc ~sub (fun ppf () -> - Printtyp.report_unification_error ppf env trace - ~type_expected_explanation: - (report_type_expected_explanation_opt explanation) - (function ppf -> - fprintf ppf "This expression has type") - (function ppf -> - fprintf ppf "but an expression was expected of type"); - ) () + report_unification_error ~loc ~sub env trace + ~type_expected_explanation: + (report_type_expected_explanation_opt explanation) + (function ppf -> + fprintf ppf "This expression has type") + (function ppf -> + fprintf ppf "but an expression was expected of type"); | Apply_non_function typ -> begin match (repr typ).desc with Tarrow _ -> @@ -5594,7 +5589,7 @@ let report_error ~loc env = function Location.errorf ~loc "The instance variable %s is not mutable" v | Not_subtype(tr1, tr2) -> Location.error_of_printer ~loc (fun ppf () -> - Printtyp.report_subtyping_error ppf env tr1 "is not a subtype of" tr2 + Printtyp.Subtype.report_error ppf env tr1 "is not a subtype of" tr2 ) () | Outside_class -> Location.errorf ~loc diff --git a/typing/typecore.mli b/typing/typecore.mli index f3f187d1f9..2038bb81c6 100644 --- a/typing/typecore.mli +++ b/typing/typecore.mli @@ -127,14 +127,15 @@ val self_coercion : (Path.t * Location.t list ref) list ref type error = | Constructor_arity_mismatch of Longident.t * int * int - | Label_mismatch of Longident.t * Ctype.Unification_trace.t + | Label_mismatch of Longident.t * Errortrace.unification Errortrace.t | Pattern_type_clash : - Ctype.Unification_trace.t * _ Typedtree.pattern_desc option -> error - | Or_pattern_type_clash of Ident.t * Ctype.Unification_trace.t + Errortrace.unification Errortrace.t * _ Typedtree.pattern_desc option + -> error + | Or_pattern_type_clash of Ident.t * Errortrace.unification Errortrace.t | Multiply_bound_variable of string | Orpat_vars of Ident.t * Ident.t list | Expr_type_clash of - Ctype.Unification_trace.t * type_forcing_context option + Errortrace.unification Errortrace.t * type_forcing_context option * Typedtree.expression_desc option | Apply_non_function of type_expr | Apply_wrong_label of arg_label * type_expr * bool @@ -153,17 +154,17 @@ type error = | Private_constructor of constructor_description * type_expr | Unbound_instance_variable of string * string list | Instance_variable_not_mutable of string - | Not_subtype of Ctype.Unification_trace.t * Ctype.Unification_trace.t + | Not_subtype of Errortrace.Subtype.t * Errortrace.unification Errortrace.t | Outside_class | Value_multiply_overridden of string | Coercion_failure of - type_expr * type_expr * Ctype.Unification_trace.t * bool + type_expr * type_expr * Errortrace.unification Errortrace.t * bool | Too_many_arguments of bool * type_expr * type_forcing_context option | Abstract_wrong_label of arg_label * type_expr * type_forcing_context option | Scoping_let_module of string * type_expr | Not_a_variant_type of Longident.t | Incoherent_label_order - | Less_general of string * Ctype.Unification_trace.t + | Less_general of string * Errortrace.unification Errortrace.t | Modules_not_allowed | Cannot_infer_signature | Not_a_packed_module of type_expr @@ -185,9 +186,9 @@ type error = | Illegal_letrec_pat | Illegal_letrec_expr | Illegal_class_expr - | Letop_type_clash of string * Ctype.Unification_trace.t - | Andop_type_clash of string * Ctype.Unification_trace.t - | Bindings_type_clash of Ctype.Unification_trace.t + | Letop_type_clash of string * Errortrace.unification Errortrace.t + | Andop_type_clash of string * Errortrace.unification Errortrace.t + | Bindings_type_clash of Errortrace.unification Errortrace.t | Unbound_existential of Ident.t list * type_expr | Missing_type_constraint diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 9104ee55dd..eaf8ef84b4 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -34,9 +34,9 @@ type error = | Recursive_abbrev of string | Cycle_in_def of string * type_expr | Definition_mismatch of type_expr * Includecore.type_mismatch option - | Constraint_failed of type_expr * type_expr - | Inconsistent_constraint of Env.t * Ctype.Unification_trace.t - | Type_clash of Env.t * Ctype.Unification_trace.t + | Constraint_failed of Env.t * Errortrace.unification Errortrace.t + | Inconsistent_constraint of Env.t * Errortrace.unification Errortrace.t + | Type_clash of Env.t * Errortrace.unification Errortrace.t | Non_regular of { definition: Path.t; used_as: type_expr; @@ -49,7 +49,8 @@ type error = | Cannot_extend_private_type of Path.t | Not_extensible_type of Path.t | Extension_mismatch of Path.t * Includecore.type_mismatch - | Rebind_wrong_type of Longident.t * Env.t * Ctype.Unification_trace.t + | Rebind_wrong_type of + Longident.t * Env.t * Errortrace.unification Errortrace.t | Rebind_mismatch of Longident.t * Path.t * Path.t | Rebind_private of Longident.t | Variance of Typedecl_variance.error @@ -277,8 +278,11 @@ let make_constructor env type_path type_params sargs sret_type = begin match (Ctype.repr ret_type).desc with | Tconstr (p', _, _) when Path.same type_path p' -> () | _ -> - raise (Error (sret_type.ptyp_loc, Constraint_failed - (ret_type, Ctype.newconstr type_path type_params))) + raise (Error (sret_type.ptyp_loc, + Constraint_failed + (env, [Errortrace.diff + ret_type + (Ctype.newconstr type_path type_params)]))) end; widen z; targs, Some tret_type, args, Some ret_type @@ -480,8 +484,11 @@ let rec check_constraints_rec env loc visited ty = with Not_found -> raise (Error(loc, Unavailable_type_constructor path)) in let ty' = Ctype.newconstr path (Ctype.instance_list decl.type_params) in - if not (Ctype.matches env ty ty') then - raise (Error(loc, Constraint_failed (ty, ty'))); + begin + try Ctype.matches env ty ty' + with Ctype.Matches_failure (env, trace) -> + raise (Error(loc, Constraint_failed (env, trace))) + end; List.iter (check_constraints_rec env loc visited) args | Tpoly (ty, tl) -> let _, ty = Ctype.instance_poly false tl ty in @@ -576,16 +583,19 @@ let check_coherence env loc dpath decl = let err = if List.length args <> List.length decl.type_params then Some Includecore.Arity - else if not (Ctype.equal env false args decl.type_params) - then Some Includecore.Constraint - else - Includecore.type_declarations ~loc ~equality:true env - ~mark:true - (Path.last path) - decl' - dpath - (Subst.type_declaration - (Subst.add_type_path dpath path Subst.identity) decl) + else begin + match Ctype.equal env false args decl.type_params with + | exception Ctype.Equality trace -> + Some (Includecore.Constraint (env, trace)) + | () -> + Includecore.type_declarations ~loc ~equality:true env + ~mark:true + (Path.last path) + decl' + dpath + (Subst.type_declaration + (Subst.add_type_path dpath path Subst.identity) decl) + end in if err <> None then raise(Error(loc, Definition_mismatch (ty, err))) @@ -655,7 +665,7 @@ let check_well_founded env loc path to_check ty = in let snap = Btype.snapshot () in try Ctype.wrap_trace_gadt_instances env (check ty TypeSet.empty) ty - with Ctype.Unify _ -> + with Ctype.Escape _ -> (* Will be detected by check_recursion *) Btype.backtrack snap @@ -688,7 +698,7 @@ let check_recursion ~orig_env env loc path decl to_check = match ty.desc with | Tconstr(path', args', _) -> if Path.same path path' then begin - if not (Ctype.equal orig_env false args args') then + if not (Ctype.is_equal orig_env false args args') then raise (Error(loc, Non_regular { definition=path; @@ -711,9 +721,8 @@ let check_recursion ~orig_env env loc path decl to_check = Ctype.instance_parameterized_type params0 body0 in begin try List.iter2 (Ctype.unify orig_env) params args' - with Ctype.Unify _ -> - raise (Error(loc, Constraint_failed - (ty, Ctype.newconstr path' params0))); + with Ctype.Unify trace -> + raise (Error(loc, Constraint_failed (orig_env, trace))); end; check_regular path' args (path' :: prev_exp) ((ty,body) :: prev_expansions) @@ -1014,7 +1023,7 @@ let transl_extension_constructor ~scope env type_path type_params (Tconstr(type_path, type_params, ref Mnil))) :: type_params in - if not (Ctype.equal env true cstr_types ext_types) then + if not (Ctype.is_equal env true cstr_types ext_types) then raise (Error(lid.loc, Rebind_mismatch(lid.txt, cstr_type_path, type_path))); (* Disallow rebinding private constructors to non-private *) @@ -1604,7 +1613,7 @@ let explain_unbound_gen ppf tv tl typ kwd pr = Btype.newgenty (Tobject(tv, ref None)) in Printtyp.reset_and_mark_loops_list [typ ti; ty0]; fprintf ppf - ".@.@[<hov2>In %s@ %a@;<1 -2>the variable %a is unbound@]" + ".@ @[<hov2>In %s@ %a@;<1 -2>the variable %a is unbound@]" kwd pr ti Printtyp.marked_type_expr tv with Not_found -> () @@ -1666,14 +1675,12 @@ let report_error ppf = function Printtyp.type_expr ty (Includecore.report_type_mismatch "the original" "this" "definition") err - | Constraint_failed (ty, ty') -> - Printtyp.reset_and_mark_loops ty; - Printtyp.mark_loops ty'; - Printtyp.Naming_context.reset (); - fprintf ppf "@[%s@ @[<hv>Type@ %a@ should be an instance of@ %a@]@]" - "Constraints are not satisfied in this type." - !Oprint.out_type (Printtyp.tree_of_typexp false ty) - !Oprint.out_type (Printtyp.tree_of_typexp false ty') + | Constraint_failed (env, trace) -> + fprintf ppf "@[<v>Constraints are not satisfied in this type.@ "; + Printtyp.report_unification_error ppf env trace + (fun ppf -> fprintf ppf "Type") + (fun ppf -> fprintf ppf "should be an instance of"); + fprintf ppf "@]" | Non_regular { definition; used_as; defined_as; expansions } -> let pp_expansion ppf (ty,body) = Format.fprintf ppf "%a = %a" @@ -1710,10 +1717,11 @@ let report_error ppf = function pp_expansions expansions end | Inconsistent_constraint (env, trace) -> - fprintf ppf "The type constraints are not consistent.@."; + fprintf ppf "@[<v>The type constraints are not consistent.@ "; Printtyp.report_unification_error ppf env trace (fun ppf -> fprintf ppf "Type") - (fun ppf -> fprintf ppf "is not compatible with type") + (fun ppf -> fprintf ppf "is not compatible with type"); + fprintf ppf "@]" | Type_clash (env, trace) -> Printtyp.report_unification_error ppf env trace (function ppf -> @@ -1727,7 +1735,7 @@ let report_error ppf = function requires a second stub function@ \ for native-code compilation@]" | Unbound_type_var (ty, decl) -> - fprintf ppf "A type variable is unbound in this type declaration"; + fprintf ppf "@[A type variable is unbound in this type declaration"; let ty = Ctype.repr ty in begin match decl.type_kind, decl.type_manifest with | Type_variant tl, _ -> @@ -1745,11 +1753,13 @@ let report_error ppf = function | Type_abstract, Some ty' -> explain_unbound_single ppf ty ty' | _ -> () - end + end; + fprintf ppf "@]" | Unbound_type_var_ext (ty, ext) -> - fprintf ppf "A type variable is unbound in this extension constructor"; + fprintf ppf "@[A type variable is unbound in this extension constructor"; let args = tys_of_constr_args ext.ext_args in - explain_unbound ppf ty args (fun c -> c) "type" (fun _ -> "") + explain_unbound ppf ty args (fun c -> c) "type" (fun _ -> ""); + fprintf ppf "@]" | Cannot_extend_private_type path -> fprintf ppf "@[%s@ %a@]" "Cannot extend private type definition" diff --git a/typing/typedecl.mli b/typing/typedecl.mli index 7ffabe7278..2ec3fef337 100644 --- a/typing/typedecl.mli +++ b/typing/typedecl.mli @@ -71,9 +71,9 @@ type error = | Recursive_abbrev of string | Cycle_in_def of string * type_expr | Definition_mismatch of type_expr * Includecore.type_mismatch option - | Constraint_failed of type_expr * type_expr - | Inconsistent_constraint of Env.t * Ctype.Unification_trace.t - | Type_clash of Env.t * Ctype.Unification_trace.t + | Constraint_failed of Env.t * Errortrace.unification Errortrace.t + | Inconsistent_constraint of Env.t * Errortrace.unification Errortrace.t + | Type_clash of Env.t * Errortrace.unification Errortrace.t | Non_regular of { definition: Path.t; used_as: type_expr; @@ -86,7 +86,8 @@ type error = | Cannot_extend_private_type of Path.t | Not_extensible_type of Path.t | Extension_mismatch of Path.t * Includecore.type_mismatch - | Rebind_wrong_type of Longident.t * Env.t * Ctype.Unification_trace.t + | Rebind_wrong_type of + Longident.t * Env.t * Errortrace.unification Errortrace.t | Rebind_mismatch of Longident.t * Path.t * Path.t | Rebind_private of Longident.t | Variance of Typedecl_variance.error diff --git a/typing/typedecl_variance.ml b/typing/typedecl_variance.ml index 4125868711..edc97191bc 100644 --- a/typing/typedecl_variance.ml +++ b/typing/typedecl_variance.ml @@ -219,7 +219,7 @@ let compute_variance_type env ~check (required, loc) decl tyl = let v2 = TypeMap.fold (fun t vt v -> - if Ctype.equal env false [ty] [t] then union vt v else v) + if Ctype.is_equal env false [ty] [t] then union vt v else v) !tvl2 null in Btype.backtrack snap; let (c1,n1) = get_upper v1 and (c2,n2,_,i2) = get_lower v2 in diff --git a/typing/typetexp.ml b/typing/typetexp.ml index 196264206e..b1a908a411 100644 --- a/typing/typetexp.ml +++ b/typing/typetexp.ml @@ -33,8 +33,8 @@ type error = | Bound_type_variable of string | Recursive_type | Unbound_row_variable of Longident.t - | Type_mismatch of Ctype.Unification_trace.t - | Alias_type_mismatch of Ctype.Unification_trace.t + | Type_mismatch of Errortrace.unification Errortrace.t + | Alias_type_mismatch of Errortrace.unification Errortrace.t | Present_has_conjunction of string | Present_has_no_type of string | Constructor_mismatch of type_expr * type_expr @@ -235,7 +235,7 @@ and transl_type_aux env policy styp = List.iter2 (fun (sty, cty) ty' -> try unify_param env ty' cty.ctyp_type with Unify trace -> - let trace = Unification_trace.swap trace in + let trace = Errortrace.swap_trace trace in raise (Error(sty.ptyp_loc, env, Type_mismatch trace)) ) (List.combine stl args) params; @@ -285,7 +285,7 @@ and transl_type_aux env policy styp = List.iter2 (fun (sty, cty) ty' -> try unify_var env ty' cty.ctyp_type with Unify trace -> - let trace = Unification_trace.swap trace in + let trace = Errortrace.swap_trace trace in raise (Error(sty.ptyp_loc, env, Type_mismatch trace)) ) (List.combine stl args) params; @@ -337,7 +337,7 @@ and transl_type_aux env policy styp = in let ty = transl_type env policy st in begin try unify_var env t ty.ctyp_type with Unify trace -> - let trace = Unification_trace.swap trace in + let trace = Errortrace.swap_trace trace in raise(Error(styp.ptyp_loc, env, Alias_type_mismatch trace)) end; ty @@ -348,7 +348,7 @@ and transl_type_aux env policy styp = TyVarMap.add alias (t, styp.ptyp_loc) !used_variables; let ty = transl_type env policy st in begin try unify_var env t ty.ctyp_type with Unify trace -> - let trace = Unification_trace.swap trace in + let trace = Errortrace.swap_trace trace in raise(Error(styp.ptyp_loc, env, Alias_type_mismatch trace)) end; if !Clflags.principal then begin @@ -379,7 +379,7 @@ and transl_type_aux env policy styp = (* Check for tag conflicts *) if l <> l' then raise(Error(styp.ptyp_loc, env, Variant_tags(l, l'))); let ty = mkfield l f and ty' = mkfield l f' in - if equal env false [ty] [ty'] then () else + if is_equal env false [ty] [ty'] then () else try unify env ty ty' with Unify _trace -> raise(Error(loc, env, Constructor_mismatch (ty,ty'))) @@ -526,7 +526,7 @@ and transl_fields env policy o fields = let add_typed_field loc l ty = try let ty' = Hashtbl.find hfields l in - if equal env false [ty] [ty'] then () else + if is_equal env false [ty] [ty'] then () else try unify env ty ty' with Unify _trace -> raise(Error(loc, env, Method_mismatch (l, ty, ty'))) diff --git a/typing/typetexp.mli b/typing/typetexp.mli index 602b7c7afd..609305ba06 100644 --- a/typing/typetexp.mli +++ b/typing/typetexp.mli @@ -50,8 +50,8 @@ type error = | Bound_type_variable of string | Recursive_type | Unbound_row_variable of Longident.t - | Type_mismatch of Ctype.Unification_trace.t - | Alias_type_mismatch of Ctype.Unification_trace.t + | Type_mismatch of Errortrace.unification Errortrace.t + | Alias_type_mismatch of Errortrace.unification Errortrace.t | Present_has_conjunction of string | Present_has_no_type of string | Constructor_mismatch of type_expr * type_expr diff --git a/utils/Makefile b/utils/Makefile index 94207230ab..1db3fc02ce 100644 --- a/utils/Makefile +++ b/utils/Makefile @@ -58,6 +58,7 @@ config.ml: config.mlp $(ROOTDIR)/Makefile.config Makefile $(call SUBST_STRING,EXT_OBJ) \ $(call SUBST,FLAMBDA) \ $(call SUBST,WITH_FLAMBDA_INVARIANTS) \ + $(call SUBST,WITH_CMM_INVARIANTS) \ $(call SUBST_STRING,FLEXLINK_FLAGS) \ $(call SUBST_QUOTE,FLEXDLL_DIR) \ $(call SUBST,HOST) \ diff --git a/utils/clflags.ml b/utils/clflags.ml index 3be20189aa..7afd612186 100644 --- a/utils/clflags.ml +++ b/utils/clflags.ml @@ -136,6 +136,8 @@ let native_code = ref false (* set to true under ocamlopt *) let force_slash = ref false (* for ocamldep *) let clambda_checks = ref false (* -clambda-checks *) +let cmm_invariants = + ref Config.with_cmm_invariants (* -dcmm-invariants *) let flambda_invariant_checks = ref Config.with_flambda_invariants (* -flambda-(no-)invariants *) @@ -567,17 +569,10 @@ let add_arguments loc args = arg_names := String.Map.add arg_name loc !arg_names ) args -let print_arguments usage = - Arg.usage !arg_spec usage - -(* This function is almost the same as [Arg.parse_expand], except - that [Arg.parse_expand] could not be used because it does not take a - reference for [arg_spec].*) -let parse_arguments argv f msg = - try - let argv = ref argv in - let current = ref 0 in - Arg.parse_and_expand_argv_dynamic current argv arg_spec f msg - with - | Arg.Bad msg -> Printf.eprintf "%s" msg; exit 2 - | Arg.Help msg -> Printf.printf "%s" msg; exit 0 +let create_usage_msg program = + Printf.sprintf "Usage: %s <options> <files>\n\ + Try '%s --help' for more information." program program + + +let print_arguments program = + Arg.usage !arg_spec (create_usage_msg program) diff --git a/utils/clflags.mli b/utils/clflags.mli index 6e45e3125c..06b478d3b6 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -13,6 +13,8 @@ (* *) (**************************************************************************) + + (** Command line flags *) (** Optimization parameters represented as ints indexed by round number. *) @@ -199,6 +201,7 @@ val default_unbox_closures_factor : int val unbox_free_vars_of_closures : bool ref val unbox_specialised_args : bool ref val clambda_checks : bool ref +val cmm_invariants : bool ref val default_inline_max_depth : int val inline_max_depth : Int_arg_helper.parsed ref val remove_unused_arguments : bool ref @@ -258,11 +261,8 @@ val arg_spec : (string * Arg.spec * string) list ref added. *) val add_arguments : string -> (string * Arg.spec * string) list -> unit -(* [parse_arguments argv anon_arg usage] will parse the arguments, using - the arguments provided in [Clflags.arg_spec]. -*) -val parse_arguments : string array -> Arg.anon_fun -> string -> unit - +(* [create_usage_msg program] creates a usage message for [program] *) +val create_usage_msg: string -> string (* [print_arguments usage] print the standard usage message *) val print_arguments : string -> unit diff --git a/utils/config.mli b/utils/config.mli index dccf88345a..980bc164e5 100644 --- a/utils/config.mli +++ b/utils/config.mli @@ -211,6 +211,9 @@ val flambda : bool val with_flambda_invariants : bool (** Whether the invariants checks for flambda are enabled *) +val with_cmm_invariants : bool +(** Whether the invariants checks for Cmm are enabled *) + val profinfo : bool (** Whether the compiler was configured for profiling *) diff --git a/utils/config.mlp b/utils/config.mlp index 9585c89c98..92ab232051 100644 --- a/utils/config.mlp +++ b/utils/config.mlp @@ -79,6 +79,7 @@ let mkdll, mkexe, mkmaindll = let flambda = %%FLAMBDA%% let with_flambda_invariants = %%WITH_FLAMBDA_INVARIANTS%% +let with_cmm_invariants = %%WITH_CMM_INVARIANTS%% let safe_string = %%FORCE_SAFE_STRING%% let default_safe_string = %%DEFAULT_SAFE_STRING%% let windows_unicode = %%WINDOWS_UNICODE%% != 0 |