In my experience, though of course yours may differ, there are very often still many plausibly correct implementations of functions working with those types and many ways to combine them that might make sense and that would satisfy the type checker. The idea that specifying the types alone is a viable substitute for proper documentation of the real meaning of the functions just falls apart at that point.
Not if your logic is primarily in terms of domain types, invariants encoded in those domain types as is necessary and economical.
> And at that point, all the power you get from saying things like there's only one possible implementation of a function f :: a -> a immediately go out of the window, because you don't have a value of type a, you have a value of type SomeConcreteTypeThatIKnowThingsAbout.
Can you give an example? I can only see this being the case if your logic is done at the concrete type level.
But, on the gripping hand, using types unspecific enough that that is the case is often a sign of underusing the type system. E.g., very few domains actually deal with bare numbers as domain values, and when you express concrete types specific enough, there may be more than one possible correct function, Bru very often the one actually correct function will be much more obvious, and the mistakes possible by omitting a step when using less-robust sets of types become impossible because you effectively have statically verified dimensional analysis.