-data AlgTyConParent = NoParentTyCon -- ordinary data type
- | ClassTyCon Class -- class dictionary
- | FamilyTyCon TyCon -- instance of type family
+-- Both type classes as well as family instances imply implicit type
+-- constructors. These implicit type constructors refer to their parent
+-- structure (ie, the class or family from which they derive) using a type of
+-- the following form. We use `TyConParent' for both algebraic and synonym
+-- types, but the variant `ClassTyCon' will only be used by algebraic tycons.
+--
+data TyConParent
+ = NoParentTyCon -- An ordinary type constructor has no parent.
+
+ | ClassTyCon -- Type constructors representing a class dictionary.
+ Class
+
+ | FamilyTyCon -- Type constructors representing an instance of a type
+ TyCon -- The type family
+ [Type] -- Instance types; free variables are the tyConTyVars
+ -- of this TyCon
+ TyCon -- A CoercionTyCon identifying the representation
+ -- type with the type instance family.
+ -- c.f. Note [Newtype coercions]
+ -- E.g. data intance T [a] = ...
+ -- gives a representation tycon:
+ -- data :R7T a = ...
+ -- axiom co a :: T [a] ~ :R7T a
+ -- with :R7T's algTcParent = FamilyTyCon T [a] co