Removing a match branch doesn't fall onto a catch-all one

Learning
1

Hello. I got a strange behavior when I was writing a Coq formatter. Here is a MRE.

(* bin/main.ml *)

exception NotImplemented

let pp_constr_expr CAst.{ v; loc = _ } =
  match v with
  | Constrexpr.CLambdaN _ -> raise NotImplemented
  | Constrexpr.CLetIn _ -> raise NotImplemented
  | Constrexpr.CAppExpl _ -> raise NotImplemented
  | Constrexpr.CApp _ -> raise NotImplemented
  | Constrexpr.CProj _ -> raise NotImplemented
  | Constrexpr.CRecord _ -> raise NotImplemented
  | Constrexpr.CCases _ -> raise NotImplemented
  | Constrexpr.CLetTuple _ -> raise NotImplemented
  | Constrexpr.CIf _ -> raise NotImplemented
  | Constrexpr.CHole _ -> raise NotImplemented
  | Constrexpr.CPatVar _ -> raise NotImplemented
  | Constrexpr.CEvar _ -> ()
  | Constrexpr.CSort _ -> raise NotImplemented
  | _ -> raise NotImplemented

let pp_subast CAst.{ v = Vernacexpr.{ control = _; attrs = _; expr }; loc = _ }
    =
  match expr with
  | VernacInductive
      (Inductive_kw, [ (((NoCoercion, (_, None)), ([], None), Some ty, _), []) ])
    ->
      pp_constr_expr ty
  | _ -> raise NotImplemented

let pp_ast ast = List.hd ast |> pp_subast

let generate_from_code code =
  let mode = Ltac_plugin.G_ltac.classic_proof_mode in
  let entry = Pvernac.main_entry (Some mode) in
  let parser = Gramlib.Stream.of_string code |> Pcoq.Parsable.make in
  let rec f acc =
    match Pcoq.Entry.parse entry parser with
    | None -> List.rev acc
    | Some ast -> f (ast :: acc)
  in
  f []

let _ = generate_from_code "Inductive foo:Type:=foo|bar." |> pp_ast

; bin/dune

(executable
 (public_name coqfmt)
 (name main)
 (libraries coq-core.plugins.ltac)
 (ocamlc_flags -g))

; dune-project

(lang dune 3.9)

(generate_opam_files true)

(package
 (name coqfmt)
 (depends coq-core dune ocaml))

When I run the program by OCAMLRUNPARAM=b dune exec bin/main.exe, it fails with an exception raised by the CRef branch.

%dune clean && OCAMLRUNPARAM=b dune exec bin/main.exe
Fatal error: exception Dune__exe__Main.NotImplemented
Raised at Dune__exe__Main.pp_constr_expr in file "bin/main.ml", line 7, characters 25-45
Called from Dune__exe__Main in file "bin/main.ml", line 45, characters 8-67

Then, removing the branch and running it again fails with the CLambdaN branch, despite my expectation that it’d fall onto the last catch-all one.

%dune clean && OCAMLRUNPARAM=b dune exec bin/main.exe
Fatal error: exception Dune__exe__Main.NotImplemented
Raised at Dune__exe__Main.pp_constr_expr in file "bin/main.ml", line 7, characters 29-49
Called from Dune__exe__Main in file "bin/main.ml", line 44, characters 8-67

I thought this was a compiler bug at first, but now I’m not sure because I’m a beginner in OCaml, and actually I found a similar case where the cause turned out to be the evaluation order of a tuple.

I also found another related issue, but here another problem is that my code depends on coq-core which is huge and makes it difficult to examine the actual cause.

Could anyone tell me if it is an expected behavior or a real compiler bug?

I tested the code with Ocaml 4.14.1 and 5.0.0, dune 3.9.2, and coq-core 8.17.1.

2

This is (in my opinion) a real compiler bug, although the bug is about inaccurate location reporting, not about which branch is taken. Could you please report it on the issue tracker?

The compiler is merging the branches with identical code, with the result that the location where the exception is raised is mis-reported in the backtrace.

Here’s a smaller reproduction case:

$ cat -n foo.ml
     1	let () = match Some () with
     2	  | None   -> raise Not_found
     3	  | Some _ -> raise Not_found
$ ocamlopt -o foo.exe -g foo.ml && OCAMLRUNPARAM=b ./foo.exe 
Fatal error: exception Not_found
Raised at Foo in file "foo.ml", line 2, characters 14-29

The exception should be raised in the Some branch on line 3, but the backtrace reports it as originating in the None branch on line 2.

2 Likes
3

Thank you. I confirmed it on my laptop too (both 4.14.4 and 5.0.0) and submitted a bug report.

3 Likes