use an explicit substitution
\begin{code}
-module Unify ( unifyTysX, unifyTyListsX,
- match, matchTy, matchTys
+module Unify ( unifyTysX, unifyTyListsX, allDistinctTyVars,
+ match, matchTy, matchTys,
) where
#include "HsVersions.h"
import TypeRep ( Type(..) ) -- friend
-import Type ( typeKind, tyVarsOfType, splitAppTy_maybe,
+import Type ( typeKind, tyVarsOfType, splitAppTy_maybe, getTyVar_maybe,
splitUTy, isUTy, deNoteType
)
%* *
%************************************************************************
+(allDistinctTyVars tys tvs) = True
+ iff
+all the types tys are type variables,
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables. For example, if the type sig is
+ f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't
+ (a) been unified with a non-tyvar type
+ (b) been unified with each other (all distinct)
+ (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars [] acc
+ = True
+allDistinctTyVars (ty:tys) acc
+ = case getTyVar_maybe ty of
+ Nothing -> False -- (a)
+ Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
+ | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Unification with an explicit substitution}
+%* *
+%************************************************************************
+
Unify types with an explicit substitution and no monad.
Ignore usage annotations.