[Agda-dev] Signature in Closure type

[Jesper Cockx]

I would guess that we don't restore the signature because we are
expecting/hoping some kind of monotonicity property to hold, i.e. adding
new things to the signature doesn't change which definitions typecheck that
don't mention these new things. But I'm not sure why we need to store it at
all, it seems it goes back a very long way. Feel free to experiment with
what happens if you remove it.

-- Jesper

On Thu, Mar 7, 2019 at 11:19 AM Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> Hi,
>
> I was looking at the Closure type in .Base and saw that it stores a
> signature.
>
> data Closure a = Closure
>   { clSignature        :: Signature
>   , clEnv              :: TCEnv
>   , clScope            :: ScopeInfo
>   , clModuleCheckpoints :: Map ModuleName CheckpointId
>   , clValue            :: a
>   }
>     deriving (Data, Functor, Foldable)
>
> However `enterClosure` does not use it, in fact no code ever looks at
> it, you can change the field type to `()`, adapt `buildClosure`, and
> remove `getMetaSig` and everything still compiles.
>
> For my use-case not restoring the `Signature` is what I want anyway,
> so things work fine.
>
> However, should we remove this field to avoid retaining useless signatures?
> Or should we be worried that signatures are not being restored when
> they ought to be?
>
> -- Andrea
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20190310/79ae3b29/attachment.html>