Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Anomaly "Uncaught exception Not_found." when destructing an inductive type as a resolvable opaque reference #19994

Open
radrow opened this issue Jan 8, 2025 · 1 comment
Labels
kind: anomaly An uncaught exception has been raised. kind: bug An error, flaw, fault or unintended behaviour.

Comments

@radrow
Copy link

radrow commented Jan 8, 2025

Description of the problem

  1. Create a module type that wraps a type
  2. Create a module type that declares an inner module of that wrapper
  3. Extend the module (with <+) by an empty module or module type
  4. Implement the wrapper module type so the wrapped type is an internally defined inductive type
  5. Specialize the combined module with that instantiation
  6. Destruct a value of the wrapped type.

Kaboom.

Even though the wrapped type is the same as the inductive type (one eq another by exact eq_refl), it cannot be destructured (or even pattern matched by hand) this way. A workaround is to make an explicit type cast.

Small Rocq / Coq file to reproduce the bug

Module Type WRAP.
  Parameter t : Set.
End WRAP.

Module Type PARAMS.
  Declare Module Arg : WRAP.
End PARAMS.

Module Type JOKER. (* also breaks if you remove `Type` *) 
End JOKER.

Module Type COMBINED := PARAMS <+ JOKER. (* Fix 1: Remove `<+ JOKER` *)

Module Inst <: WRAP.
  Inductive t_ := Q | R. (* Fix 2: Move this definition away *)
  Definition t := t_.
End Inst.

Module Type RECOMBINED := COMBINED with Module Arg := Inst.

Module Type LOCK_DEFS(Mod : RECOMBINED). (* also breaks if you remove `Type` *) 
  Goal Mod.Arg.t -> False.
    intros.
    (* Fix 3: run `destruct (H : Inst.t)` instead *)
    destruct H. (* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)

Version of Rocq / Coq where this bug occurs

8.20

Last version of Rocq / Coq where the bug did not occur

No response

@radrow radrow added kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Jan 8, 2025
@SkySkimmer
Copy link
Contributor

Mod.Arg.t is syntactically equal to Inst.t, but it is also defined to := Mod.Arg.t_ which does not exist.

@SkySkimmer SkySkimmer added kind: anomaly An uncaught exception has been raised. and removed needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Jan 8, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: anomaly An uncaught exception has been raised. kind: bug An error, flaw, fault or unintended behaviour.
Projects
None yet
Development

No branches or pull requests

2 participants