-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Unification with an explicit substitution}
-%* *
-%************************************************************************
-
-(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 tcGetTyVar_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.
-
-\begin{code}
-type MySubst
- = (TyVarSet, -- Set of template tyvars
- TyVarSubstEnv) -- Not necessarily idempotent
-
-unifyTysX :: TyVarSet -- Template tyvars
- -> Type
- -> Type
- -> Maybe TyVarSubstEnv
-unifyTysX tmpl_tyvars ty1 ty2
- = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
-
-unifyExtendTysX :: TyVarSet -- Template tyvars
- -> TyVarSubstEnv -- Substitution to start with
- -> Type
- -> Type
- -> Maybe TyVarSubstEnv -- Extended substitution
-unifyExtendTysX tmpl_tyvars subst ty1 ty2
- = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
-
-unifyTyListsX :: TyVarSet -> [Type] -> [Type]
- -> Maybe TyVarSubstEnv
-unifyTyListsX tmpl_tyvars tys1 tys2
- = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
-
-
-uTysX :: Type
- -> Type
- -> (MySubst -> Maybe result)
- -> MySubst
- -> Maybe result
-
-uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
-uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
-
- -- Variables; go for uVar
-uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
- | tyvar1 == tyvar2
- = k subst
-uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
- | tyvar1 `elemVarSet` tmpls
- = uVarX tyvar1 ty2 k subst
-uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
- | tyvar2 `elemVarSet` tmpls
- = uVarX tyvar2 ty1 k subst
-
- -- Predicates
-uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
- | n1 == n2 = uTysX t1 t2 k subst
-uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
- | c1 == c2 = uTyListsX tys1 tys2 k subst
-uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
- | tc1 == tc2 = uTyListsX tys1 tys2 k subst
-
- -- Functions; just check the two parts
-uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
- = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
-
- -- Type constructors must match
-uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
- | (con1 == con2 && equalLength tys1 tys2)
- = uTyListsX tys1 tys2 k subst
-
- -- Applications need a bit of care!
- -- They can match FunTy and TyConApp, so use splitAppTy_maybe
- -- NB: we've already dealt with type variables and Notes,
- -- so if one type is an App the other one jolly well better be too
-uTysX (AppTy s1 t1) ty2 k subst
- = case tcSplitAppTy_maybe ty2 of
- Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
- Nothing -> Nothing -- Fail
-
-uTysX ty1 (AppTy s2 t2) k subst
- = case tcSplitAppTy_maybe ty1 of
- Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
- Nothing -> Nothing -- Fail
-
- -- Not expecting for-alls in unification
-#ifdef DEBUG
-uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
-uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
-#endif
-
- -- Ignore usages
-uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
-uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
-
- -- Anything else fails
-uTysX ty1 ty2 k subst = Nothing
-
-
-uTyListsX [] [] k subst = k subst
-uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
-uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
-\end{code}