diff options
| -rw-r--r-- | doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst | 5 | ||||
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12418.v | 29 |
3 files changed, 35 insertions, 1 deletions
diff --git a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst new file mode 100644 index 0000000000..8f126c5b6f --- /dev/null +++ b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match` + (`#12422 <https://github.com/coq/coq/pull/12422>`_, + fixes `#12418 <https://github.com/coq/coq/pull/12418>`_, + by Hugo Herbelin). diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5e3fb9dae3..25353b7c12 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1716,7 +1716,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = let flags = (default_flags_of TransparentState.full) in match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with | Success evd -> evdref := evd - | UnifFailure _ -> assert false + | UnifFailure _ -> evdref := add_conv_pb (Reduction.CONV,!!env,substl inst ev',t) sigma end; ev' | _ -> diff --git a/test-suite/bugs/closed/bug_12418.v b/test-suite/bugs/closed/bug_12418.v new file mode 100644 index 0000000000..cf11ea627b --- /dev/null +++ b/test-suite/bugs/closed/bug_12418.v @@ -0,0 +1,29 @@ +(* The second "match" below used to raise an anomaly *) + +Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type := + { ret : forall {t : Type@{d}}, t -> m t }. + +Record state {S : Type} (t : Type) : Type := mkState { runState : t }. + +Global Declare Instance Monad_state : forall S, Monad (@state S). + +Class Cava := { + constant : bool -> unit; + constant_vec : unit; +}. + +Axiom F : forall {A : Type}, (bool -> A) -> Datatypes.unit. + +Fail Instance T : Cava := { + + constant b := match b with + | true => ret tt + | false => ret tt + end; + + constant_vec := @F _ (fun b => match b with + | true => tt + | false => tt + end); + +}. |