Handle implicit suspension in a more consistent way #35
Description
For now implicit suspensions are handled before the constraint typing algorithm, and very hackish heuristics are used to determine how what to suspend.
This leads to some limitations, for instance, the type comp (assoc f g h) (id _)) -> id _ fails. The reason is that the identity on the RHS cannot infer that it needs a suspension.
#33 introduces constraint typing with meta type variables consistently. We could use this to determine how to implicitly supend in a more consistent way:
If the implicit suspension is activated, when we type by constraint a term of the form coh (ps,ty)[s], instead of giving the result to be ty[s], we change the base * for a meta type variable. Upon resolving, if we find this meta variable to stand for a type dimension k, we suspend the corresponding coherence k times.