Lambda the Ultimate

I am trying to build a simple DSL in scheme. I would like this DSL to use type inference to constrain s-expressions to only those that are provably type correct. My type scheme is fairly simple. I would like to have the following basic polymorphic types (at least for starters. This will likely expand later):

datum
  number
    real
      int
  char
  bool

In addition, I would like to support functions (all curried to a single param), lists and intersections of types, so that types like (-> int char) and (intersection (list-of int) char) can be supported. Strings will be lists of char for my DSL.

I know the way to do this is to use a type unification algorithm. Unfortunately, all the docs I can find on this subject seem to be very much research oriented and way over my head since I do not grasp the basic concepts here. I am wondering if anyone has some pointers to some good type inference tutorial level stuff that I might be able to get a good grasp of the basic principles and algorithm from.