[Agda-dev] Signature in Closure type

[Andrea Vezzosi]

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