<div dir="ltr">In-line with the above idea I wonder if there is an option to do something in the middle between fully normalizing a goal and not normalizing it.<div><br></div><div>Is it possible to normalize something to the first visible constructors? Say I have declared a function that is not visible in my current scope. The function is defined in terms of other functions that are visible in scope. Can I get Agda to show me the visible type?</div><div><br></div><div>MWE:</div><div><br></div><font face="monospace, monospace">module _ where<br><br>open import Data.Product<br><br>module _ {C O M P L E X : Set} where<br>  private<br>    T = C × O × M × P × L × E × X<br>  ex : T → X<br>  ex (c , o , m , p , l , e , x) = x<br><br>x : {X : Set} → X<br>x = ex {!!}</font><div><br></div><div>In this goal I want to be the type displayed to me to be as if `T` had been inlined in the definition of `ex`. In this case it's a septuple with elements corresponding to the implicit parameters at the usage-site of `ex`. This is just a contrived example but it highlights what I'm after.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 21, 2018 at 3:40 PM, Frederik Hanghøj Iversen <span dir="ltr"><<a href="mailto:fhi.1990@gmail.com" target="_blank">fhi.1990@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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" target="_blank">http://agda.readthedocs.<wbr>io/en/latest/language/pragmas.<wbr>html</a><span class="HOEnZb"><font color="#888888"><br clear="all"><div><br></div>-- <br><div class="m_-6365414665759768004gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</font></span></div></div></div></div></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div>