Strict implicit arguments in Coq

Question

In the following code

Set Implicit Arguments.
Unset Strict Implicit.

Record graph := {
  obj :> Type;
  arrows : Type;
  s : arrows -> obj;
  t : arrows -> obj;
}.

the first argument of s (of type graph) is implicit but if I remove Unset Strict Implicit. (and I add, just for clarity, Set Strongly Strict Implicit.) the first argument of s is not implicit anymore, which shows that this argument is considered as implicit but not as strict implicit. For which reason isn't it strict implicit? Indeed, from the type of the second argument of s (which is arrows g, where g is the first argument of s), we can deduce the first argument of s. It seems to me that the situation is similar to the one described here:

For instance, the first argument of

cons: forall A:Set, A -> list A -> list A

in module List.v is strict because list is an inductive type and A will always be inferable from the type list A of the third argument of cons.

What is the fundamental difference between the two situations that makes the first argument of s non-strict implicit?

Answer 1

The type of s is forall g, arrows g -> obj g. You can't infer g from arrows g and obj g.

For example g1 := {| obj := nat ; arrows := nat ; s := fun _ => 0 ; t := fun _ => 0 |} and g2 := {| obj := nat ; arrows := nat ; s := fun _ => 1 ; t := fun _ => 1 |}, then obj g1 = obj g2 and arrows g1 = arrows g2 but g1 and g2 are not definitionally equal.

In other words, obj and arrows are not injective, whereas list is injective (with respect to definitional equality) because it is a type constructor. list A and list B are definitionally equal only if A and B are definitionally equal.