Despite the fact this post may appear critical, this is in the spirit of feedback to a young language, not a mean spirit.

One of the things I'm not sure you're looking at, and that you really ought to decide sooner rather than later, is how much interaction with Go itself you want. You very much do not want to leave the Go FFI interactions until the end.

In fact I daresay this is a critical decision that needs to be the next thing you really spend a lot of time thinking about, because a Kashmir that has a very poor Go FFI leaves me little reason to prefer it to Haskell, or Liskell if you want to get closer to Lisp. (Truthfully, reading over your goals & features, this sounds closer to Haskell than a Lisp, except in syntax, so I'm going to use Haskell as my benchmark.)

However, many of those goals and things in the type system will be at odds with having a simple Go FFI. If all functions in Kashmir are auto-curried, then Go has a hard time calling in to them, with a clumsy syntax and probably slow performance. If Kashmir's type system ends up complicated enough that the Go type system can't express Kashmir function types at all, then Go can't call into Kashmir at all, or some complicated "generic instantiation" step will be required. On the other side, you have to worry about data structure compatibility, too; if Kashmir data structures don't have a nice mapping to Go data structures then Kashmir is going to have a hard time calling into Go code.

Also, I'd suggest before proceeding much farther that you are very, very sure that you understand Hindley-Milner deeply, including what can break it. It offers a lot of inferring power, but at the corresponding cost of laying a lot of very specialized restrictions on your program. These carefully mathematically-specified things often have a way of breaking down the instant you put a toe outside their specified line. (The Haskell community has added things to it that have good bang/buck, but it's always something they have to be careful about.) Go's native type system, for instance, has one huge difference with Haskell that would have me a bit nervous, which is the difference between:

    (+) :: Num a => a -> a -> a

    type Num interface {
        Add(Num, Num) Num
    }

Haskell's type there guarantees all the a's are the same Num type. The Num typeclass does not promise that all "Num"s can be added together, only that a Num can be added to other same type things. Go's type system can not guarantee this; that interface in Go is promising that either A: You can hand it any two things that implement Num and it will return yet something else that implements Num which may or may not have any particular relationship to the original types or B: it will panic at runtime. (Or loop forever, I suppose, but it seems strange to be seriously discussing "bottom" in Go at all....)

Where in practice you can turn to a programmer and say "Hey, obviously, it makes no sense to add a rational and a Peano integer together, and if you did, you obviously wouldn't expect a BigInt back. So just don't do that.", your type inferencer will not be able to make such assumptions, and if it does, you're right back to the problem that that will raise all sorts of hell in your FFI.

These are not necessarily unsolvable problems! For one thing, there's the sort of degenerate solution of simply not permitting any FFI, and only permitting Kashmir->Go in a very restricted, stereotypical manner that requires a specialized binding step. You could also write off calling Kashmir from Go, if that helps, which is not a bad decision, but is one you should be deliberate about. But I would suggest it is deserving of being the very next issue you tackle, and spend a lot of time thinking about. Go's type system is really, really weak for a static type system, in the sense of what guarantees it is capable of expressing, and trying to cozy that up to a Hindley-Milner system without giving up on a lot on one side or the other is going to be a challenge.