+\begin{code}
+data TyVarDetails
+ = SigTv -- Introduced when instantiating a type signature,
+ -- prior to checking that the defn of a fn does
+ -- have the expected type. Should not be instantiated.
+ --
+ -- f :: forall a. a -> a
+ -- f = e
+ -- When checking e, with expected type (a->a), we
+ -- should not instantiate a
+
+ | ClsTv -- Scoped type variable introduced by a class decl
+ -- class C a where ...
+
+ | InstTv -- Ditto, but instance decl
+
+ | PatSigTv -- Scoped type variable, introduced by a pattern
+ -- type signature
+ -- \ x::a -> e
+
+ | VanillaTv -- Everything else
+
+isUserTyVar :: TyVarDetails -> Bool -- Avoid unifying these if possible
+isUserTyVar VanillaTv = False
+isUserTyVar other = True
+
+isSkolemTyVar :: TyVarDetails -> Bool
+isSkolemTyVar SigTv = True
+isSkolemTyVar other = False
+
+instance Outputable TyVarDetails where
+ ppr SigTv = ptext SLIT("type signature")
+ ppr ClsTv = ptext SLIT("class declaration")
+ ppr InstTv = ptext SLIT("instance declaration")
+ ppr PatSigTv = ptext SLIT("pattern type signature")
+ ppr VanillaTv = ptext SLIT("???")
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Tau, sigma and rho}
+%* *
+%************************************************************************
+
+\begin{code}