it seems like the clean syntax makes the type checker's life harder and so performance is unacceptable. would you rather have clean syntax or acceptable compile times?
Edit: I'm no expert in this topic, but Prolog interpreters (compilers?) have some fascinating machinery to solve complex constraints. Maybe a similar approach could help here?