Type Hole De-Elaboration?

[solomon-b]

Type holes can get really gnarly, such as:

+ P : Poly
+ d : Σ (_ : base (fst C)), fib (fst C) _ ⇒ Σ (<2> : Σ (pbase : base (fst C)), Π (<196> : fib (fst C) pbase), base (fst C)), Σ (pfib : fib (fst C) (fst <2>)), fib (fst C) (snd <2> pfib)

Sometimes we know the unelaborated form of the type of some term and we annotate it in the code:

    let P : Poly := fst C in
    let d : P ⇒ tensor-◁ P P := fst (snd (snd C)) in

It would be really nice if the type hole reflected that un-elaborated (and thus easier to read) type.