Many compilers for typed languages accept options which affect type checking, and to ensure soundness, some care must be taken if mixing files typechecked with different options.
Options which enable or disable new type system features are relatively unproblematic, but trouble can occur if options affect existing types: if two types are considered equal with the option but are provably distinct without it, then it is unsound to combine two files compiled with and without the option.
This has caused a soundness bug in Agda1, by mixing code
compiled with the
--cubical option (which permits multiple proofs of
equality) and the
--with-K option (which assumes equalities have
unique proofs). Similar bugs arose several times in OCaml, based on
various options that affect type equality:
--rectypes, which permits
--safe-string, which makes the immutable
bytes type distinct3, and
--nolabels, which coarsens
equality of function types with named parameters4.
(* Counterexample by Gabriel Scherer and Benoît Vaugon *) (* blah.ml, compiled without -rectypes *) type ('a, 'b, 'c) eqtest = | Refl : ('a, 'a, float) eqtest | Diff : ('a, 'b, int) eqtest let test : type a b . (unit -> a, a, b) eqtest -> b = function | Diff -> 42 (* bluh.ml, compiled with -rectypes *) let () = print_float Blah.(test (Refl : (unit -> 'a as 'a, 'a, _) eqtest))
These sorts of issues are conspicuously absent from GHC Haskell, which supports an unusually large number of options that affect typechecking. A reason for this is that internally, GHC compiles Haskell with any set of extensions to the same typed intermediate language, Core. Since the Core language is unaffected by options, incompatibilities between options would cause one of them to generate ill-typed Core, which can be detected locally.