I have some similar goals. Have you considered leaning more into inference than gradual typing? One pattern I like is allowing the compiler to develop a more complex mental model, but keeping it straightforward for users -- you can do that with inference, ownership, purity, effect types, etc. What I actually think is really tantalizing is using tooling to fill in some of those gaps -- for instance, the editor could know types, required capabilities etc, without the user ever needing to type anything, but when the user needs it, they can find it, query it, test against it.
Cool - it sounds pretty similar. It's interesting that it looks so different. I'll have to investigate more.
WRT to inference, yes. I infer everything in EASY mode.
And the compiler give the user autofix via choice when a type is ambiguous (I don't default to huge union types - I assume no one wants to do that and make them choose a type - may potentially allow AutoUnion to allow that).
I couldn't tell if you're using affine ownership, but I assume so if you don't have a GC. If they try to create an alias - they get a use after move error, and the compiler tells them they need to either COPY (auto-fix) or create a RefCount (usually auto-fix) - they pick.