-Note [GADT type refinement]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we come to a GADT pattern match that refines the in-scope types, we
- a) Refine the types of the Ids in the in-scope set, seInScope.
- For exmaple, consider
- data T a where
- Foo :: T (Bool -> Bool)
-
- (\ (x::T a) (y::a) -> case x of { Foo -> y True }
-
- Technically this is well-typed, but exprType will barf on the
- (y True) unless we refine the type on y's occurrence.
-
- b) Refine the range of the type substitution, seTvSubst.
- Very similar reason to (a).
-
- NB: we don't refine the range of the SimplIdSubst, because it's always
- interpreted relative to the seInScope (see substId)
-
-For (b) we need to be a little careful. Specifically, we compose the refinement
-with the type substitution. Suppose
- The substitution was [a->b, b->a]
- and the refinement was [b->Int]
- Then we want [a->Int, b->a]
-
-But also if
- The substitution was [a->b]
- and the refinement was [b->Int]
- Then we want [a->Int, b->Int]
- becuase b might be both an InTyVar and OutTyVar
-
-