+[Pattern matching indexed data types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following declarations:
+
+ data family Map k :: * -> *
+ data instance Map (a, b) v = MapPair (Map a (Pair b v))
+
+and a case expression
+
+ case x :: Map (Int, c) w of MapPair m -> ...
+
+As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
+worker/wrapper types for MapPair are
+
+ $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
+ $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
+
+So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
+:R123Map, which means the straight use of boxySplitTyConApp would give a type
+error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
+boxySplitTyConApp with the family tycon Map instead, which gives us the family
+type list {(Int, c), w}. To get the correct split for :R123Map, we need to
+unify the family type list {(Int, c), w} with the instance types {(a, b), v}
+(provided by tyConFamInst_maybe together with the family tycon). This
+unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
+the split arguments for the representation tycon :R123Map as {Int, c, w}
+
+In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
+
+ Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+
+moving between representation and family type into account. To produce type
+correct Core, this coercion needs to be used to case the type of the scrutinee
+from the family to the representation type. This is achieved by
+unwrapFamInstScrutinee using a CoPat around the result pattern.
+
+Now it might appear seem as if we could have used the existing GADT type
+refinement infrastructure of refineAlt and friends instead of the explicit
+unification and CoPat generation. However, that would be wrong. Why? The
+whole point of GADT refinement is that the refinement is local to the case
+alternative. In contrast, the substitution generated by the unification of
+the family type list and instance types needs to be propagated to the outside.
+Imagine that in the above example, the type of the scrutinee would have been
+(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
+substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the
+instantiation of x with (a, b) must be global; ie, it must be valid in *all*
+alternatives of the case expression, whereas in the GADT case it might vary
+between alternatives.
+
+In fact, if we have a data instance declaration defining a GADT, eq_spec will
+be non-empty and we will get a mixture of global instantiations and local
+refinement from a single match. This neatly reflects that, as soon as we
+have constrained the type of the scrutinee to the required type index, all
+further type refinement is local to the alternative.
+