<div dir="ltr">I know there's an INLINE-pragma for Agda (though it's not documented here [1]). This pragma affects compilation. I wonder if there was something akin to this for type-checking.<div><br></div><div>When I want to close a goal with a complex type I usually spend a considerable time defining helper functions and in particular figuring out what type these should have. Agda of course can help me here, but often it doesn't display the type that I want. The best type is rarely the non-normalized *nor* fully normalized type. Ideally I would like to be able to step up and down these types interactively. But something perhaps easier to implement and also super helpful would be if I could e.g. mark a "type synonym" as being completely transparent, so that it's definition would be inlined when I ask for goal and context.</div><div><br></div><div>As a super small example of what I'm looking for is:</div><div><br></div><div>Assume I have a type-synonym `P T = A × T' and I want to close a hole of type `P T` then `C-c C-,` should give me `Goal: A <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">× T`. Incidentally if I issue `C-u C-u C-c C-,` the hole will be displayed as `Σ A (λ x → T)` which is less helpful. Granted in this case the type is easily understood - but this is rarely the case.</span></div><div><div><div><div><br></div><div>[1]: <a href="http://agda.readthedocs.io/en/latest/language/pragmas.html">http://agda.readthedocs.io/en/latest/language/pragmas.html</a><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div></div></div></div>