I'm still pretty new to Haskell, but I think there are several ways. The equivalent to your addone3 would be some sort of Template Haskell incantation. Template Haskell gives you lisp-style hygienic macros that are expanded and type checked at compile time (except more complicated because of the more complicated semantics and AST).

Haskell also provides a ton of options for generic programming that provide similar power (still statically typed). GADTs (Generalized Algebraic Data Types) might be of use here. There are also existential types and type classes.

What you probably really want though is a dependently typed language like Idris or Agda. If you're not familiar, here's the one liner: Java generics are types that depend on types (like a List of Bools). Dependent types are types that can depend on values (like a List of exactly 3 Bools). So in theory you should be able to define the type you're looking for here, but I don't know what the concrete syntax would be.

The problem with dependently typed languages right now is that the surface languages and concepts tend to be hard for people to grok. Personally I think meta-programming facilities and DSLs will help with this. Ther are lots of languages heading in that direction.