+Note [Type matching]
+~~~~~~~~~~~~~~~~~~~~
+This little function @refineTyVars@ is a little tricky. Suppose we have a pattern type
+signature
+ f = \(x :: Term a) -> body
+Then 'a' should be bound to a wobbly type. But if we have
+ f :: Term b -> some-type
+ f = \(x :: Term a) -> body
+then 'a' should be bound to the rigid type 'b'. So we want to
+ * instantiate the type sig with fresh meta tyvars (e.g. \alpha)
+ * unify with the type coming from the context
+ * read out whatever information has been gleaned
+ from that unificaiton (e.g. unifying \alpha with 'b')
+ * and replace \alpha by 'b' in the type, when typechecking the
+ pattern inside the type sig (x in this case)
+It amounts to combining rigid info from the context and from the sig.
+
+Exactly the same thing happens for 'smart function application'.
+
+\begin{code}
+refineTyVars :: [TcTyVar] -- Newly instantiated meta-tyvars of the function
+ -> TcM TvSubst -- Substitution mapping any of the meta-tyvars that
+ -- has been unifies to what it was instantiated to
+-- Just one level of de-wobblification though. What a hack!
+refineTyVars tvs
+ = do { mb_prs <- mapM mk_pr tvs
+ ; return (mkTvSubst (mkVarEnv (catMaybes mb_prs))) }
+ where
+ mk_pr tv = do { details <- readMetaTyVar tv
+ ; case details of
+ Indirect ty -> return (Just (tv,ty))
+ other -> return Nothing
+ }
+\end{code}
+