coerce package:Agda
coerce v a b coerces v : a to type b,
returning a v' : b with maybe extra hidden applications or
hidden abstractions.
In principle, this function can host coercive subtyping, but currently
it only tries to fix problems with hidden function types.
Expose the format coerce f args.
We fuse coercions, even if interleaving with applications. We assume
that coercion is powerful enough to satisfy coerce (coerce f a) b
= coerce f a b
Strip leading coercions and indicate whether there were some.
Account for situations like k : (Size< j) <= (Size< k +
1)
Actually, the semantics is (Size<= k) ∩ (Size< j) ⊆ rhs
which gives a disjunctive constraint. Mmmh, looks like stuff TODO.
For now, we do a cheap heuristics.