+\begin{code}
+checkSigMatch []
+ = returnTc (error "checkSigMatch")
+
+checkSigMatch tc_ty_sigs@( sig1@(TySigInfo _ id1 _ theta1 _ _) : all_sigs_but_first )
+ = -- CHECK THAT THE SIGNATURE TYVARS AND TAU_TYPES ARE OK
+ -- Doesn't affect substitution
+ mapTc check_one_sig tc_ty_sigs `thenTc_`
+
+ -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
+ -- The type signatures on a mutually-recursive group of definitions
+ -- must all have the same context (or none).
+ --
+ -- We unify them because, with polymorphic recursion, their types
+ -- might not otherwise be related. This is a rather subtle issue.
+ -- ToDo: amplify
+ mapTc check_one_cxt all_sigs_but_first `thenTc_`
+
+ returnTc theta1
+ where
+ sig1_dict_tys = mk_dict_tys theta1
+ n_sig1_dict_tys = length sig1_dict_tys
+
+ check_one_cxt sig@(TySigInfo _ id _ theta _ src_loc)
+ = tcAddSrcLoc src_loc $
+ tcAddErrCtxt (sigContextsCtxt id1 id) $
+ checkTc (length this_sig_dict_tys == n_sig1_dict_tys)
+ sigContextsErr `thenTc_`
+ unifyTauTyLists sig1_dict_tys this_sig_dict_tys
+ where
+ this_sig_dict_tys = mk_dict_tys theta
+
+ check_one_sig (TySigInfo name id sig_tyvars _ sig_tau src_loc)
+ = tcAddSrcLoc src_loc $
+ tcAddErrCtxt (sigCtxt id) $
+ checkSigTyVars sig_tyvars sig_tau
+
+ mk_dict_tys theta = [mkDictTy c ts | (c,ts) <- theta]
+\end{code}
+
+
+@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.
+
+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.
+
+\begin{code}
+checkSigTyVars :: [TcTyVar s] -- The original signature type variables
+ -> TcType s -- signature type (for err msg)
+ -> TcM s [TcTyVar s] -- Zonked signature type variables
+
+checkSigTyVars sig_tyvars sig_tau
+ = mapNF_Tc zonkTcTyVar sig_tyvars `thenNF_Tc` \ sig_tys ->
+ let
+ sig_tyvars' = map (getTyVar "checkSigTyVars") sig_tys
+ in
+
+ -- Check points (a) and (b)
+ checkTcM (all isTyVarTy sig_tys && hasNoDups sig_tyvars')
+ (zonkTcType sig_tau `thenNF_Tc` \ sig_tau' ->
+ failWithTc (badMatchErr sig_tau sig_tau')
+ ) `thenTc_`
+
+ -- Check point (c)
+ -- We want to report errors in terms of the original signature tyvars,
+ -- ie sig_tyvars, NOT sig_tyvars'. sig_tyvars' correspond
+ -- 1-1 with sig_tyvars, so we can just map back.
+ tcGetGlobalTyVars `thenNF_Tc` \ globals ->
+ let
+ mono_tyvars' = [sig_tv' | sig_tv' <- sig_tyvars',
+ sig_tv' `elementOfTyVarSet` globals]
+
+ mono_tyvars = map (assoc "checkSigTyVars" (sig_tyvars' `zip` sig_tyvars)) mono_tyvars'
+ in
+ checkTcM (null mono_tyvars')
+ (failWithTc (notAsPolyAsSigErr sig_tau mono_tyvars)) `thenTc_`
+
+ returnTc sig_tyvars'