The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi,

I have an example where I'm confused about the rules regarding types.

I have a function GiT of the following type

ljt_dec < Check GiT.
GiT : list PropF -> PropF -> nat -> Prop

ljt_dec < Check (GiT Γ P 0).
GiT Γ P 0 : Prop

The following is accepted without a type error

ljt_dec < Check (existsT2 d : nat, GiT Γ P d).
existsT2 d : nat, GiT Γ P d : Set

existsT2 is notation for sigT ...

ljt_dec < Check (sigT (fun d : nat => GiT Γ P d)).
existsT2 d : nat, GiT Γ P d : Set

ljt_dec < Check sigT.
sigT : forall A : Type, (A -> Type) -> Type

but sigT wants a body of type Type (ie nat -> Type)
but in the example works with a body of type
(nat -> Prop)

and sigT should return result type of Type, but here
returns a result of type Type

Sometimes (often) coq objects when you get Prop, Set and
Type mixed up, and use the wrong one, here not at all.

I'd like to understand why this is so

Thanks

Jeremy