What is different between Set and Type in Coq?
Coq has 3 "big" types:


Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if $p_1, p_2 : P$ then $p_1 = p_2$. This allows terms that are only used for proof to be erased in any code generated by Coq.
Set is meant for computation. It's predicative, and doesn't have proof irrelevance, which lets you do nice things like not assuming $1 = 2$. The Set parts remain during code extraction. 
Type is a supertype of both of these, allowing you to write code once that works with either


I'm pretty sure your error is because you're defining a Set whose parameters can be Type, which means they can be Prop, which isn't allowed. If you change to this:

Inductive prod (X Y: Set) : Set := 
| pair: X -&gt; Y -&gt; prod X Y. 


your code should work.