I mean it must employ gradual typing, right? So that it can interface with existing code that is untyped
Code that is outside of the purview of Coalton—raw Common Lisp code—is run in explicit (LISP ...) forms [0] which require the user to annotate the type and they add dynamic type checks to ensure the enclosed code meets the contract the programmer specified (unless UNSAFE is used [1]).
But there are definite advantages to having Coalton know your types, which is why they give you a `(declare foo Integer)` form. This doesn't compile to any code, it's a compiler hint that tells Coalton that it can assume `foo` is an int, not a float64/double, which allows it to pick at compile time which implementation of + gets used in `(+ foo 5)`.
The 2025 video introducing Coalton at https://www.youtube.com/watch?v=of92m4XNgrM gives an example of what Coalton can do with knowing types. Robert Smith (the presenter, and the primary creator of Coalton) gives an example of a Fast Fourier Transform function that uses generic numeric types so you can call it on any number type: float32, float64, int-modulo-a-prime, whatever. He then benchmarks it, and it takes about 1 second to run 2 million times. Then he adds the single compiler hint `(monomorphize)` above the function declaration. This tells Coalton "Hey, instead of doing a dispatch table lookup in this function and calling different + implementations based on the type of the parameters, I want you to create two different copies of this function, one that will call the specialized float32 math functions, and the other one that will call the specialized float64 math functions." (Or three copies if you also called it with your int-modulo-prime number type). This eliminates a dispatch-table lookup and allows the compiler to produce much more specialized code. It comes at the expense of larger binaries, of course: he's explicit about how this is trading speed for size, so it's an opt-in choice you make (by adding a `(monomorphize)` declaration above the function definition) rather than something that Coalton defaults to.
But I've digressed. Yes, I believe (though note my caveat about not having used Coalton yet) that it would use dynamic types for code whose types it can't infer. But I'm pretty sure it would also give you a warning. If it gives you an error, the solution is to add a `(declare [name] [type])` line in the appropriate place.