-- structure (ie, the class or family from which they derive) using a type of
-- the following form.
--
-data AlgTyConParent = -- An ordinary type constructor has no parent.
- NoParentTyCon
-
- -- Type constructors representing a class dictionary.
- | ClassTyCon Class
-
- -- Type constructors representing an instances of a type
- -- family.
- | FamilyTyCon TyCon -- the type family
- [Type] -- instance types
- TyCon -- a *coercion* identifying
- -- the representation type
- -- with the type instance
+data AlgTyConParent
+ = 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
+ 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 T77 a = ...
+ -- axiom co a :: T [a] ~ T77 a
+ -- with T77's algTcParent = FamilyTyCon T [a] co
data SynTyConRhs
= OpenSynTyCon Kind -- Type family: *result* kind given
CoT @ s
which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
-But in GHC we instead make CoT into a new piece of type syntax
+But in GHC we instead make CoT into a new piece of type syntax, CoercionTyCon,
(like instCoercionTyCon, symCoercionTyCon etc), which must always
be saturated, but which encodes as
TyConApp CoT [s]