Type Inference and Generalization
There are a few things to realize:

First, top level declarations are implicitly let-bound, so your code is equivalent to the following:

let
  x :: Int
  x = id 1

  y :: Char
  y = id 'a'

  id :: a -&gt; a
  id x = x


Secondly, as was mentioned in the comments, Haskell will sort the let statements topologically, nesting them when it can, and any recursive uses are monotyped unless annotated.

Finally, the types of let-variables are generalized at their definition, but specialized at their use. So now we have (something close to):

let
  id :: a -&gt; a
  id x = x
in let
  x :: Int
  x = id 1

  y :: Char
  y = id 'a'


Finally, we need to see that while variable types are generalized at their definition, they are specialized at their use.

So, this is roughly what inference does:


The checker infers the type $id : \alpha \to \alpha$, then generalizes this to $\forall a \ldotp a \to a$.
The checker puts $id : \forall a \ldotp a \to a$ into the environment for checking $x$ and $y$
While checking the definitions of $x$, at the use of $id$, 
the type $\forall a \ldotp a \to a$ is instantiated to $\beta \to \beta$, where $\beta$ is a fresh unification variable.
While checking the definitions of $y$, at the use of $id$, 
the type $\forall a \ldotp a \to a$ is instantiated to $\gamma \to \gamma$, where $\gamma$ is a different fresh unification variable.


Because the polymorphic type scheme is instantiated with unique variables at each use, the inference is able proceed without error.