Coercions / subtyping is a big one, because mathematics is full of quotient types and identifications. This is a very practical issue, that comes up many many t

Coercions / subtyping is a big one, because mathematics is full of quotient types and identifications. This is a very practical issue, that comes up many many times. Not necessarily if you "program" in Coq, but if you try to do math in Coq. Another one is that there is no good treatment of undefinedness. An "option" type doesn't cut it, because it pollutes everything. The question is, how can you enable undefinedness everywhere, without polluting everything? That is only possible by adjusting your logic.