How does the Haskell `do` notation know which value to take when it isn't defined by a return?

I have this monadic object.

data Parser a = Parser (String -> Maybe (a, String))

instance Functor Parser where
  -- fmap :: (a -> b) -> Parser a -> Parser b
  fmap f (Parser pa) =  Parser $ \input -> case pa input of
                                             Nothing -> Nothing
                                             Just (a, rest) -> Just (f a, rest)

instance Applicative Parser where
  pure = return
  (<*>) = ap

instance Monad Parser where
  --return :: a -> Parser a
  return a =  Parser $ \input -> Just (a, input)

  --(>>=) :: Parser a -> (a -> Parser b) -> Parser b
  (Parser pa) >>= f  = Parser $ \input -> case pa input of
                                            Nothing -> Nothing
                                            Just (a,rest) -> parse (f a) rest

And I have this definition of an item which I am told "reads in a character" but I don't really see any reading going on.

item :: Parser Char
item = Parser $ \ input -> case input of ""    -> Nothing
                                         (h:t) -> Just (h, t)

But ok, fine, maybe I should just relax about how literal to take the word "read" and jibe with it. Moving on, I have

failParse :: Parser a
failParse = Parser $ \ input -> Nothing

sat :: (Char -> Bool) -> Parser Char
sat p = do c <- item
           if p c
           then return c
           else failParse

And this is where I get pretty confused. What is getting stored in the variable c? Since item is a Parser with parameter Char, my first guess is that c is storing such an object. But after a second of thought I know that's not now the do notation works, you don't get the monad, you get the contents of the monad. Great, but then that tells me c is then the function

\ input -> case input of ""    -> Nothing
                         (h:t) -> Just (h, t)

But clearly that's wrong since the next line of the definition of sat treats c like a character. Not only is that not what I expect, but it's about three levels of structure down from what I expected! It's not the function, it's not the Maybe object, and it's not the tuple, but it's the left coordinate of the Just tuple buried inside the function! How is that little character working all that way outside? What is instructing the <- to extract this part of the monad?

Solution

As comment mentioned, <- just be do notation syntax sugar and equivalent to:

item >>= (\c->if p c 
              then return c 
              else failParse)

Okay, let see what is c? consider the definition of (>>=)

(>>=) :: Parser a -> (a -> Parser b) -> Parser b

or more readable way:

Parser a >>= (a -> Parser b)

And Now, matches it with above expression item >>= (\c->if p c then return c else failParse) give:

Parer a = item

and

(a->Parser b) = (\c->if p c then return c else failParse)

and item has type:

item :: Parser Char

so, we can now replace a in (>>=) by Char, gives

Parser Char >>= (Char -> Parser b)

and now \c->if p c then return c else failParse also have type: (Char -> Parser b)

and so c is a Char, and the whole expression can be extended to:

sat p =
item >>= (\c->...) = 
Parser pa >= (\c->...) = Parser $ \input -> case pa input of
                                            Nothing -> Nothing
                                            Just (a,rest) -> parse (f a) rest
                         where f c =  if p c
                                      then return c
                                      else failParse
                               pa input = case input of ""   -> Nothing
                                                       (h:t) -> Just (h, t)