-unify_tc_app use_refinement tc (NoteTy _ ty)
- = unify_tc_app use_refinement tc ty
-
-unify_tc_app use_refinement tc ty@(TyVarTy tyvar)
- = do { details <- condLookupTcTyVar use_refinement tyvar
+unify_tc_app n_args use_refinement tc (NoteTy _ ty)
+ = unify_tc_app n_args use_refinement tc ty
+
+unify_tc_app n_args use_refinement tc (TyConApp tycon arg_tys)
+ | tycon == tc
+ = ASSERT( n_args == length arg_tys ) -- ty::*
+ mapM (wobblify use_refinement) arg_tys
+
+unify_tc_app n_args use_refinement tc (AppTy fun_ty arg_ty)
+ = do { arg_ty' <- wobblify use_refinement arg_ty
+ ; arg_tys <- unify_tc_app (n_args - 1) use_refinement tc fun_ty
+ ; return (arg_tys ++ [arg_ty']) }
+
+unify_tc_app n_args use_refinement tc ty@(TyVarTy tyvar)
+ = do { traceTc (text "unify_tc_app: tyvar" <+> pprTcTyVar tyvar)
+ ; details <- condLookupTcTyVar use_refinement tyvar