thanks, pretty useful! But it doesn't work, maybe it's only a my silly error.

Couldn't match type ‘[Char]’
                  with ‘StateT VarState Data.Functor.Identity.Identity Name’
    Expected type: (VarState -> VarState)
                   -> (VarState -> VarState -> Name)
                   -> VarState
                   -> State VarState Name
      Actual type: (VarState -> VarState)
                   -> (VarState -> VarState -> Name) -> VarState -> Name
    In a stmt of a 'do' block: state <- get
    In the expression:
      do { state <- get;
           if (Map.member name (getEnvironment state)) then
               return name
           else
               do { put
                      (VarState
                         (getCounter state + 1)
                         (Map.insert
                            name (show (getCounter state)) (getEnvironment state)));
                    .... } }
    In an equation for ‘queryandupdate’:
        queryandupdate name
          = do { state <- get;
                 if (Map.member name (getEnvironment state)) then
                     return name
                 else
                     do { ... } }

With the code code:

queryandupdate :: Name -> VarState -> State VarState Name
queryandupdate name = do
  state <- get
  if  (Map.member name (getEnvironment state))
   then return name
   else do
    put (VarState (getCounter state +1)
                  (Map.insert name (show (getCounter state))
                              (getEnvironment state)))
    return $ show (getCounter state)

refreshing :: Expr -> State VarState Expr
refreshing expr =
 case expr of
  (Var n) -> do
   nome <- queryandupdate n
   return (Var nome)
  _ -> error "not implemented"

renamingFresh :: Expr -> Expr
renamingFresh e = evalState (refreshing e) emptystate