+
+\begin{code}
+tcTySig :: RenamedSig -> TcM s TcSigInfo
+
+tcTySig (Sig v ty src_loc)
+ = tcAddSrcLoc src_loc $
+ tcHsType ty `thenTc` \ sigma_tc_ty ->
+ mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
+ returnTc sig
+
+mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
+mkTcSig poly_id src_loc
+ = -- Instantiate this type
+ -- It's important to do this even though in the error-free case
+ -- we could just split the sigma_tc_ty (since the tyvars don't
+ -- unified with anything). But in the case of an error, when
+ -- the tyvars *do* get unified with something, we want to carry on
+ -- typechecking the rest of the program with the function bound
+ -- to a pristine type, namely sigma_tc_ty
+ let
+ (tyvars, rho) = splitForAllTys (idType poly_id)
+ in
+ mapNF_Tc tcInstSigVar tyvars `thenNF_Tc` \ tyvars' ->
+ -- Make *signature* type variables
+
+ let
+ tyvar_tys' = mkTyVarTys tyvars'
+ rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
+ -- mkTopTyVarSubst because the tyvars' are fresh
+ (theta', tau') = splitRhoTy rho'
+ -- This splitRhoTy tries hard to make sure that tau' is a type synonym
+ -- wherever possible, which can improve interface files.
+ in
+ newMethodWithGivenTy SignatureOrigin
+ poly_id
+ tyvar_tys'
+ theta' tau' `thenNF_Tc` \ inst ->
+ -- We make a Method even if it's not overloaded; no harm
+
+ returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
+ where
+ name = idName poly_id
+\end{code}
+
+
+
+%************************************************************************
+%* *
+\subsection{Checking signature type variables}
+%* *
+%************************************************************************
+
+@checkSigTyVars@ is used after the type in a type signature has been unified with
+the actual type found. It then checks that the type variables of the type signature
+are
+ (a) Still all type variables
+ eg matching signature [a] against inferred type [(p,q)]
+ [then a will be unified to a non-type variable]
+
+ (b) Still all distinct
+ eg matching signature [(a,b)] against inferred type [(p,p)]
+ [then a and b will be unified together]
+
+ (c) Not mentioned in the environment
+ eg the signature for f in this:
+
+ g x = ... where
+ f :: a->[a]
+ f y = [x,y]
+
+ Here, f is forced to be monorphic by the free occurence of x.
+
+ (d) Not (unified with another type variable that is) in scope.
+ eg f x :: (r->r) = (\y->y) :: forall a. a->r
+ when checking the expression type signature, we find that
+ even though there is nothing in scope whose type mentions r,
+ nevertheless the type signature for the expression isn't right.
+
+ Another example is in a class or instance declaration:
+ class C a where
+ op :: forall b. a -> b
+ op x = x
+ Here, b gets unified with a
+
+Before doing this, the substitution is applied to the signature type variable.
+
+We used to have the notion of a "DontBind" type variable, which would
+only be bound to itself or nothing. Then points (a) and (b) were
+self-checking. But it gave rise to bogus consequential error messages.
+For example:
+
+ f = (*) -- Monomorphic
+
+ g :: Num a => a -> a
+ g x = f x x
+
+Here, we get a complaint when checking the type signature for g,
+that g isn't polymorphic enough; but then we get another one when
+dealing with the (Num x) context arising from f's definition;
+we try to unify x with Int (to default it), but find that x has already
+been unified with the DontBind variable "a" from g's signature.
+This is really a problem with side-effecting unification; we'd like to
+undo g's effects when its type signature fails, but unification is done
+by side effect, so we can't (easily).
+
+So we revert to ordinary type variables for signatures, and try to
+give a helpful message in checkSigTyVars.
+