[Agda] INLINE-pragma

[Frederik Hanghøj Iversen]

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.

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?

MWE:

module _ where

open import Data.Product

module _ {C O M P L E X : Set} where
  private
    T = C × O × M × P × L × E × X
  ex : T → X
  ex (c , o , m , p , l , e , x) = x

x : {X : Set} → X
x = ex {!!}

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.

On Wed, Feb 21, 2018 at 3:40 PM, Frederik Hanghøj Iversen <
fhi.1990 at gmail.com> wrote:

> 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.
>
> 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.
>
> As a super small example of what I'm looking for is:
>
> 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 × 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.
>
> [1]: http://agda.readthedocs.io/en/latest/language/pragmas.html
>
> --
> Regards
> *Frederik Hanghøj Iversen*
>



-- 
Regards
*Frederik Hanghøj Iversen*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180302/ca92224f/attachment.html>