Search code examples
coq

What are the rules of Coq implicit types deduction in Inductive definitions?


Consider this type that has X as an implicit type.

Inductive list' {X:Type} : Type :=
  | nil'
  | cons' (x : X) (l : list').

Coq deduced that type of the second argument of cons' is @list' A:

Fail Check cons' a (cons' b nil'). (* "cons' b nil'" expected to have type "@list' A"*)

But how was this type deduced unambiguously? We can create another type:

Inductive list'' {X:Type} : Type :=
  | nil''
  | cons'' (x : X) (l : @list'' B).

Check cons'' a (cons'' b nil'').

It shows that l could also be @list' B.


Solution

  • To be precise, Coq inferred the type of cons' to be forall {X}, X -> @list' X -> @list' X. Then when you write cons a, Coq works out that you must be building a @list' A, and fills in X with A, thus constraining the second argument to be again of type @list' A.

    However, the choice of X over some other type is not the only possible choice, as you noticed. In your second example, cons'' gets type forall {X}, X -> @list'' B -> @list'' X. However, when it is left unspecified, most people most of the time intend their parameters (things on the left side of the colon) to be uniform, that is, the same in the arguments as in the conclusion, which heuristic leads to the choice of X here. In general, Coq doesn't worry too much about making sure it's solutions are unique for things the user left unspecified.

    In recent enough versions of Coq, you can use the option Uniform Inductive Parameters to specify that all parameters are uniform, or use a | to separate the uniform from the non-uniform parameters. In the case of lists, that would look like

    Inductive list' (X:Type) | : Type :=
      | nil'
      | cons' (x : X) (l : list').
    

    Note that with the |, in the declaration of constructors list' has type Type, while without the |, list' has type Type -> Type, and there is a constraint that the conclusion of the constructor has to be list X (while the arguments can use list other_type freely).