Stream: Coq users

Topic: Metavariable fails to unify with return type

Kevin Orr (Mar 17 2021 at 18:59):

Hi, in this example, I would expect elaboration/inference to figure out what the implicit parameter b is:

Inductive T : bool -> Type :=
| C {b : bool} (v : if b then unit else unit) : T b.

Check C _ : T true.
(* C ?v : T true *)
(*      : T true *)
(* where *)
(* ?v : [ |- if true then unit else unit] *)

Check @C true tt : T true.
Check tt : if true then unit else unit.
Fail Check C tt : T true.  (* Error: The term "tt" has type "unit" while it is expected to have type "if ?b then unit else unit". *)
Fail Definition x : T true := C tt.  (* Same error *)

Should ?b unify with true? Based on the output of Check C _ : T true, it seems to unify there, but not in the two Failing commands.

Jasper Hugunin (Mar 17 2021 at 19:08):

Arguments C {b} & v. fixes this; documentation is at https://coq.inria.fr/distrib/current/refman/language/extensions/arguments-command.html#bidirectionality-hints

Kevin Orr (Mar 17 2021 at 19:15):

Oh that is perfect. I've run into this or similar bidirectionality issues many times but never tried making a MRE until now. Thanks so much!

Last updated: Oct 01 2023 at 18:01 UTC