The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 16 Jan 2013 19:34:00 -0500,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> Hi,
> Can someone explain to me why the following code generates a stack
> overflow, and whether or not this is a bug?
> 
> Set Implicit Arguments.
> 
> Generalizable All Variables.
> 
> Set Printing Universes.
> 
> Record SpecializedCategory (obj : Type) :=
> Build_SpecializedCategory' { Object :> _ := obj;
>   Morphism' : obj -> obj -> Type;
> 
>   Identity' : forall o, Morphism' o o;
>   Compose' : forall s d d', Morphism' d d' -> Morphism' s d ->
> Morphism' s d';
> 
>   Associativity' : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 :
> Morphism' o2 o3) (m3 : Morphism' o3 o4),
>     Compose' (Compose' m3 m2) m1 = Compose' m3 (Compose' m2 m1);
>   (* ask for [eq_sym (Associativity' ...)], so that C^{op}^{op} is
> convertible with C *)
>   Associativity'_sym : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 :
> Morphism' o2 o3) (m3 : Morphism' o3 o4),
>     Compose' m3 (Compose' m2 m1) = Compose' (Compose' m3 m2) m1
> }.
> 
> Definition CatO : SpecializedCategory Empty_set.
>   exact (@Build_SpecializedCategory' Empty_set
>                                      (fun x => match x with end)
>                                      (fun x => match x with end)
>                                      (fun x => match x with end)
>                                      (fun x => match x with end)
>                                      (fun x => match x with end)).
> Defined.
> 
> 
> 
> Thanks!
> 
> -Jason

  exact (let Empty_set := Empty_set in
         @Build_SpecializedCategory' Empty_set
                                     (fun x => match x with end)
                                     (fun x => match x with end)
                                     (fun x => match x with end)
                                     (fun x => match x with end)
                                     (fun x => match x with end)).

works :) (really, it does!)

More seriously, I think it is due to the fact that Empty_set is of type
Set and not of type Type. The work around "let Empty_set := Empty_set
in" declares a new binder (Empty_set) which is inferred being of type
Type and not of type Set, thanks to cumulativity. So for the why your
version does a stack overflow, I would answer "coq's black magic". It
is the type inference which has some hard work to do to guess the types
right, and fails.

  exact (@Build_SpecializedCategory' (Empty_set : Type)
                                     (fun x => match x with end)
                                     (fun x => match x with end)
                                     (fun x => match x with end)
                                     (fun x => match x with end)
                                     (fun x => match x with end)).

does not work either. I do not really understand Coq mechanics.
But mixing Set and Type is almost never good (though you may have no
choice).

My guess may also be wrong, as some other tricks I try (like Definition
empty : Type := Empty_set. then use empty instead of Empty_set) do not
work either.