Internal error inocamlc on extreme code: Ctype.Nondep_cannot_erase

[mheiber]

Steps to Reproduce

See "UPDATE" below for a smaller repro

using ocaml 5.0.0, tested on Mac 13.1 (22C65) with M1

ocamlc girard.ml

source: https://github.com/mheiber/girards-paradox/blob/2bbcb77/girard.ml

girard.ml is the same as https://github.com/lpw25/girards-paradox/blob/17ccd5d/girard.ml, with the following line appended: module M = Paradox(struct let one = 1 end)

Here are some relevant definitions in girard.ml:

module type Type = sig module type T end
module type Absurd = functor (X : Type) -> X.T
(* ... a lot of functor stuff *)
module Paradox : Absurd = (* ... *)
module M = Paradox(struct let one = 1 end)   (* this added line is the only difference from lpw25/girards-paradox *)

Actual Behavior

Fatal error

Fatal error: exception Ctype.Nondep_cannot_erase(_)
Raised at Mtype.nondep_mty_with_presence in file "typing/mtype.ml", line 190, characters 14-50
Called from Mtype.nondep_mty in file "typing/mtype.ml" (inlined), line 226, characters 6-58
Called from Mtype.nondep_supertype in file "typing/mtype.ml", line 262, characters 31-52
Called from Stdlib__Option.map in file "option.ml", line 24, characters 57-62
Called from Includemod.Functor_app_diff.update in file "typing/includemod.ml", line 1151, characters 14-68
Called from Diffing.Define.Right_variadic.Internal.update in file "utils/diffing.ml", line 437, characters 25-42
Called from Diffing.Define.Generic.compute_inner_cell in file "utils/diffing.ml", line 351, characters 14-36
Called from Diffing.Define.Generic.compute_matrix.loop in file "utils/diffing.ml", line 379, characters 10-28
Called from Diffing.Define.Right_variadic.diff in file "utils/diffing.ml", line 443, characters 6-39
Called from Includemod_errorprinter.Functor_suberror.App.patch in file "typing/includemod_errorprinter.ml" (inlined), line 460, characters 6-51
Called from Includemod_errorprinter.report_apply_error in file "typing/includemod_errorprinter.ml", line 899, characters 10-55
Called from Misc.try_finally in file "utils/misc.ml", line 31, characters 8-15
Re-raised at Misc.try_finally in file "utils/misc.ml", line 45, characters 10-56
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from Persistent_env.without_cmis in file "typing/persistent_env.ml", line 142, characters 10-109
Called from Includemod_errorprinter.register.(fun) in file "typing/includemod_errorprinter.ml", line 931, characters 15-149
Called from Location.error_of_exn.loop in file "parsing/location.ml", line 940, characters 16-21
Called from Location.report_exception.loop in file "parsing/location.ml", line 958, characters 10-26
Re-raised at Location.report_exception.loop in file "parsing/location.ml", line 959, characters 14-25
Called from Maindriver.main in file "driver/maindriver.ml", line 110, characters 4-35
Called from Main in file "driver/main.ml", line 2, characters 7-54

Expected Behavior

No internal compiler error.

The ideal would be an error like this:

File "girard.ml", line 880, characters 11-42:
848 | module M = Paradox(struct let one = 1 end)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Modules do not match: sig val one : int end is not included in
       Type
     The module type `T' is required but not provided
     File "girard.ml", line 3, characters 23-36: Expected declaration

An error message like this makes sense to me, since the argument to Paradox is wrong. Paradox is a functor expecting a Type, which has a member module type T.

Related behaviors

• ocamlopt girard.ml shows a similar internal compiler error to the one for ocamlc above
• ocaml girard.ml hangs on this code. The code isn't expected to diverge, if I understand @lpw25's comment here correctly: Are you able to extend this to make the type checker diverge? lpw25/girards-paradox#1.

Related issues

• Nondep_cannot_erase appeared in fatals previously due to a since-fixed issue: Compiler fails with Ctype.Nondep_cannot_erase exception. #9858

I could only trigger the fatal with extreme functor shenanigans unlikely to appear in real code. I suspect this issue is low-priority.

Update

This is a smaller repro:

• ocamlc girard.ml or ocamlopt girard.ml with this file https://github.com/mheiber/girards-paradox/blob/1052486/girard.ml produces the same errr stack. ocaml girard.ml with this file does not hang, unlike with the original repro.

[Octachron]

This is the high-level error message that is producing the internal error. I expect that this happens when the diffing algorithm is exploring the possibility that there is a missing argument with the correct type. This is worth some investigation to see if that can be easily corrected.

[lpw25]

ocaml girard.ml hangs on this code.

This is probably the expected behavior. It is presumably looping when evaluating the definition of Paradox which is indeed a definition that does not terminate.

[ccasin]

Although this issue is open, this bug appears to be fixed in 5.1.0 and trunk. I came here to report a simpler program that was triggering the same error (provided by @ceastlund, and copied below). But I was using 4.14, and testing quickly on 5.1.0 and trunk shows that both the smaller program and the above example now give nice type errors rather than crashing the compiler.

Here's the smaller program that was triggering the same issue on 4.14:

module type A = sig
  type t
end

module type B = sig
  type t

  module type A = A with type t := t

  val a : (module A)
end

module F (B : B) : B.A = (val assert false : B.A)

module G (B : B with type t := int) = struct
  let a : (module B.A) = (module F ((val B.a)))
end

[gasche]

Should we consider closing this issue, then, if it was resolved in 5.1.0? (cc @Octachron)

[clementblaudeau]

Just as future reference, a smaller example is given by :

module type Type = sig module type T end
module F(A:Type)(X:A.T) = X
module Crash = F(struct module T = struct end end) (* should be module type T, not module T*)

Note that the name clash can also happen with type constructor, i.e. this also crashes:

module Crash' = F(struct type t = T end)

[yallop]

For the record, I've checked that @Octachron's 670aeb8 fixes @clementblaudeau's example (#12014 (comment)), @ccasin's example (#12014 (comment)) and @joelatschool's example (#12821).

[gasche]

Thanks @yallop! @Octachron, do we want to backport this to the 4.14 branch?

[Octachron]

Backporting #12063 to 4.14 sounds like a sensible option to me, I will open a PR to do so.