comp doesn't work for several common uses
I believe I have some similar problem, but I'm not sure if it's related. I'm not that into type theory so forgive me for any weird explanations. Hope this might add some value to the discussion though.
For better readability see this gist: https://gist.github.com/owickstrom/5695e0591ef245305f27
I've hit a similar issue:
This will type-check correctly:
whereas this fails:
At least one of these problems requires a complete overhaul of the constraint generation algorithm.
Huge job, no current work towards this.