+\begin{code}
+unifyListTy :: TcType s -- expected list type
+ -> TcM s (TcType s) -- list element type
+
+unifyListTy ty@(TyVarTy tyvar)
+ = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ case maybe_ty of
+ BoundTo ty' -> unifyListTy ty'
+ other -> unify_list_ty_help ty
+
+unifyListTy ty
+ = case splitTyConApp_maybe ty of
+ Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
+ other -> unify_list_ty_help ty
+
+unify_list_ty_help ty -- Revert to ordinary unification
+ = newTyVarTy mkBoxedTypeKind `thenNF_Tc` \ elt_ty ->
+ unifyTauTy ty (mkListTy elt_ty) `thenTc_`
+ returnTc elt_ty
+\end{code}
+
+\begin{code}
+unifyTupleTy :: Arity -> TcType s -> TcM s [TcType s]
+unifyTupleTy arity ty@(TyVarTy tyvar)
+ = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ case maybe_ty of
+ BoundTo ty' -> unifyTupleTy arity ty'
+ other -> unify_tuple_ty_help arity ty
+
+unifyTupleTy arity ty
+ = case splitTyConApp_maybe ty of
+ Just (tycon, arg_tys) | isTupleTyCon tycon
+ && tyConArity tycon == arity
+ -> returnTc arg_tys
+ other -> unify_tuple_ty_help arity ty
+
+unify_tuple_ty_help arity ty
+ = mapNF_Tc (\ _ -> newTyVarTy mkBoxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys ->
+ unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_`
+ returnTc arg_tys
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Unification wih a explicit substitution}
+%* *
+%************************************************************************
+
+Unify types with an explicit substitution and no monad.
+
+\begin{code}
+type Subst = TyVarEnv (GenType Bool) -- Not necessarily idempotent
+
+unifyTysX :: GenType Bool
+ -> GenType Bool
+ -> Maybe Subst
+unifyTysX ty1 ty2 = uTysX ty1 ty2 (\s -> Just s) emptyTyVarEnv
+
+unifyTyListsX :: [GenType Bool] -> [GenType Bool] -> Maybe Subst
+unifyTyListsX tys1 tys2 = uTyListsX tys1 tys2 (\s -> Just s) emptyTyVarEnv
+
+
+uTysX :: GenType Bool
+ -> GenType Bool
+ -> (Subst -> Maybe Subst)
+ -> Subst
+ -> Maybe Subst
+
+uTysX (SynTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
+uTysX ty1 (SynTy _ 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
+ | tyVarFlexi tyvar1
+ = uVarX tyvar1 ty2 k subst
+uTysX ty1 (TyVarTy tyvar2) k subst
+ | tyVarFlexi tyvar2
+ = uVarX tyvar2 ty1 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 && length tys1 == length tys2)
+ = uTyListsX tys1 tys2 k subst
+
+ -- Applications need a bit of care!
+ -- They can match FunTy and TyConApp
+uTysX (AppTy s1 t1) (AppTy s2 t2) k subst
+ = uTysX s1 s2 (uTysX t1 t2 k) subst
+
+uTysX (AppTy s1 t1) (FunTy fun2 arg2) k subst
+ = uTysX s1 s2 (uTysX t1 t2 k) subst
+ where
+ -- Converts a -> b to (->) a b
+ s2 = TyConApp mkFunTyCon [fun2]
+ t2 = arg2
+
+uTysX (AppTy s1 t1) (TyConApp tc tys@(_:_)) k subst
+ = case snocView tys of
+ (ts2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
+ where
+ -- Not efficient, but simple
+ s2 = TyConApp tc ts2
+
+uTysX s1 s2@(AppTy _ _) k subst = uTysX s2 s1 k subst
+ -- Swap arguments if the App is in the second argument
+
+ -- 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
+
+ -- 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}
+
+\begin{code}
+-- Invariant: tv1 is a unifiable variable
+uVarX tv1 ty2 k subst
+ = case lookupTyVarEnv subst tv1 of
+ Just ty1 -> -- Already bound
+ uTysX ty1 ty2 k subst
+
+ Nothing -- Not already bound
+ | typeKind ty2 `hasMoreBoxityInfo` tyVarKind tv1
+ && occur_check_ok ty2
+ -> -- No kind mismatch nor occur check
+ k (addToTyVarEnv subst tv1 ty2)
+
+ | otherwise -> Nothing -- Fail if kind mis-match or occur check
+ where
+ occur_check_ok ty = all occur_check_ok_tv (tyVarSetToList (tyVarsOfType ty))
+ occur_check_ok_tv tv | tv1 == tv = False
+ | otherwise = case lookupTyVarEnv subst tv of
+ Nothing -> True
+ Just ty -> occur_check_ok ty