-Note [Data type families]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [Wrappers for data instance tycons] in MkId.lhs
-
-Consider
- data family T a
-
- data instance T (b,c) where
- T1 :: b -> c -> T (b,c)
- T2 :: T (Int,Bool)
-
-Notice that the 'data instance' can be a fully-fledged GADT
-
- * T is the "family TyCon". It is a data type
- whose AlgTyConRhs is OpenTyCon
-
- * For each 'data instance' we make "representation TyCon"
- :R1T, thus:
- data :R1T b c where
- T1 :: forall b c. b -> c -> :R1T b c
- T1 :: :R1T Int Bool
- We have a bit of work to do, to unpick the result types of the
- data instance declaration to get the result type in the
- representation; e.g. T (Int,Bool) --> :R1T Int Bool
-
- * We defind a top-level coercion connecting it to the family TyCon
-
- axiom :Co:R1T b c : T (b,c) ~ :R1T b c
-
- * The data contructor T1 has a wrapper (which is what the
- source-level "T1" invokes):
-
- $WT1 :: forall b c. b -> c -> T (b,c)
- $WT1 b c (x::b) (y::c) = T1 b c x y `cast` sym (:Co:R1T b c)
-
- * The representation TyCon, :R1T, has an AlgTyConParent of
-
- FamilyTyCon T [(b,c)] :Co:R1T
-
-
-