Canonical structures in ssreflect

Question

I'm trying to deal with canonical structures in ssreflect. There are 2 pieces of code that I took from here.

I will bring pieces for the bool and the option types.

Section BoolFinType.

  Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed.
  Definition bool_finMixin := Eval hnf in FinMixin bool_enumP.
  Canonical bool_finType := Eval hnf in FinType bool bool_finMixin.
  Lemma card_bool : #|{: bool}| = 2. Proof. by rewrite cardT enumT unlock. Qed.

End BoolFinType.

Section OptionFinType.

  Variable T : finType.
  Notation some := (@Some _) (only parsing).

  Local Notation enumF T := (Finite.enum T).

  Definition option_enum := None :: map some (enumF T).

  Lemma option_enumP : Finite.axiom option_enum.
  Proof. by case => [x|]; rewrite /= count_map (count_pred0, enumP). Qed.

  Definition option_finMixin := Eval hnf in FinMixin option_enumP.
  Canonical option_finType := Eval hnf in FinType (option T) option_finMixin.

  Lemma card_option : #|{: option T}| = #|T|.+1.
  Proof. by rewrite !cardT !enumT {1}unlock /= !size_map. Qed.

End OptionFinType.

Now, suppose I have a function f from finType to Prop.

Variable T: finType.
Variable f: finType -> Prop.

Goal f T. (* Ok *)
Goal f bool. (* Not ok *)
Goal f (option T). (* Not ok *)

In the last two cases I get the following error:

The term "bool/option T" has type "Set/Type" while it is expected to have type "finType".

What am I doing wrong?

Answer 1

The instance search for canonical structures is a bit counter intuitive in these cases. Suppose that you have the following things:

• a structure type S, and a type T;
• a field proj : S -> T of S;
• an element x : T; and
• an element st : S that has been declared as canonical, such that proj st is defined as x.

In your example, we would have:

• S = finType
• T = Type
• proj = Finite.sort
• x = bool
• st = bool_finType.

Canonical structure search is triggered only in the following case: when the type-checking algorithm is trying to find a value to validly fill in the hole in the equation proj _ = x. Then, it will use st : S to fill in this hole. In your example, you expected the algorithm to understand that bool can be used as finType, by transforming it into bool_finType, which is not quite what is described above.

To make Coq infer what you want, you need to use a unification problem of that form. For instance,

Variable P : finType -> Prop.
Check ((fun (T : finType) (x : T) => P T) _ true).

What is going on here? Remember that Finite.sort is declared as a coercion from finType to Type, so x : T really means x : Finite.sort T. When you apply the fun expression to true : bool, Coq has to find a solution for Finite.sort _ = bool. It then finds bool_finType, because it was declared as canonical. So the element of bool is what triggers the search, but not quite bool itself.

As ejgallego pointed out, this pattern is so common that ssreflect provides the special [finType of ...] syntax. But it might still be useful to understand what is going on under the hood.