+ -- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
+ -- Reason: less confusing, and easier to generate IfaceSyn
+
+ dcEqSpec :: [(TyVar,Type)], -- Equalities derived from the result type,
+ -- *as written by the programmer*
+ -- This field allows us to move conveniently between the two ways
+ -- of representing a GADT constructor's type:
+ -- MkT :: forall a b. (a :=: [b]) => b -> T a
+ -- MkT :: forall b. b -> T [b]
+ -- Each equality is of the form (a :=: ty), where 'a' is one of
+ -- the universally quantified type variables
+
+ dcTheta :: ThetaType, -- The context of the constructor
+ -- In GADT form, this is *exactly* what the programmer writes, even if
+ -- the context constrains only universally quantified variables
+ -- MkT :: forall a. Eq a => a -> T a
+ -- It may contain user-written equality predicates too
+
+ dcStupidTheta :: ThetaType, -- The context of the data type declaration
+ -- data Eq a => T a = ...
+ -- or, rather, a "thinned" version thereof