Performance: Instantiated meta-variables in interface files

[nad]

I'm currently working on some code for which Agda fails to create the interface. I think my code should be optimised, but I want to document the problem. Agda spends a lot of time instantiating meta-variables when eliminating dead code, before running out of memory:

agda/src/full/Agda/TypeChecking/DeadCode.hs

Lines 23 to 29 in ff89beb

	-- | Run before serialisation to remove any definitions that are not reachable
	-- from the public interface to the module.
	eliminateDeadCode :: DisplayForms -> Signature -> TCM (DisplayForms, Signature)
	eliminateDeadCode disp sig = Bench.billTo [Bench.DeadCode] $ do
	patsyn <- getPatternSyns
	public <- Set.mapMonotonic anameName . publicNames <$> getScope
	defs <- traverse instantiateFull $ sig ^. sigDefinitions

Note that meta-variables are also instantiated before the interface is stored (presumably this piece of code could be optimised):

agda/src/full/Agda/Interaction/Imports.hs

Lines 1198 to 1200 in ff89beb

	reportSLn "import.iface" 7 " instantiating all meta variables"
	i <- instantiateFull Interface
	{ iSourceHash = hashText source

Would it make sense to have instantiated meta-variables in interfaces? Could this lead to any problems? I can imagine that the problem with the freezing code (#5388) could be made worse.

[nad]

Note that meta-variables are also instantiated before the interface is stored (presumably this piece of code could be optimised):

I have optimised this piece of code. However, the main problem remains.

[nad]

Would it make sense to have instantiated meta-variables in interfaces? Could this lead to any problems?

One should at least also include bindings for the instantiated meta-variables in the interfaces.

Are meta-variable identifiers only unique within a single module? In that case that should also be addressed in some way.

[jespercockx]

Yes, metavariables are currently only unique within the same top-level module, so they should be qualified properly.

One more advantage of allowing metas in interfaces would be that it would allow us to get rid of the current ugly hack in the implementation of --allow-unsolved-metas, which is turning unsolved metavariables into postulates.

[nad]

I was wondering how much of the MetaStore we need to include in the interfaces. If we restrict ourselves to instantiated meta-variables, then I guess it would suffice to have only the instantiations:

agda/src/full/Agda/TypeChecking/Monad/Base.hs

Line 1312 in 1fe6beb

= InstV [Arg String] Term -- ^ solved by term (abstracted over some free variables)

A MetaStore contains a number of other things:

agda/src/full/Agda/TypeChecking/Monad/Base.hs

Lines 1272 to 1284 in 1fe6beb

	data MetaVariable =
	MetaVar { mvInfo :: MetaInfo
	, mvPriority :: MetaPriority -- ^ some metavariables are more eager to be instantiated
	, mvPermutation :: Permutation
	-- ^ a metavariable doesn't have to depend on all variables
	-- in the context, this "permutation" will throw away the
	-- ones it does not depend on
	, mvJudgement :: Judgement MetaId
	, mvInstantiation :: MetaInstantiation
	, mvListeners :: Set Listener -- ^ meta variables scheduled for eta-expansion but blocked by this one
	, mvFrozen :: Frozen -- ^ are we past the point where we can instantiate this meta variable?
	, mvTwin :: Maybe MetaId -- ^ @Just m@ means this meta will be equated to @m@ when the latter is unblocked. See @blockedTermOnProblem@.
	}

Do we need any of this, except for the instantiation, for instantiated meta-variables from other modules? Such meta-variables could be seen as shorthand notation for their instantiations, and the code that replaces instantiated meta-variables with their instantiations only uses mvInstantiation:

agda/src/full/Agda/TypeChecking/Reduce.hs

Lines 142 to 172 in 1fe6beb

	instance Instantiate Term where
	instantiate' t@(MetaV x es) = do
	blocking <- view stInstantiateBlocking <$> getTCState
	mv <- lookupMeta x
	let mi = mvInstantiation mv
	case mi of
	InstV tel v -> instantiate' inst
	where
	-- A slight complication here is that the meta might be underapplied,
	-- in which case we have to build the lambda abstraction before
	-- applying the substitution, or overapplied in which case we need to
	-- fall back to applyE.
	(es1, es2) = splitAt (length tel) es
	vs1 = reverse $ map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es1
	rho = vs1 ++# wkS (length vs1) idS
	-- really should be .. ++# emptyS but using wkS makes it reduce to idS
	-- when applicable
	-- specification: inst == foldr mkLam v tel `applyE` es
	inst = applySubst rho (foldr mkLam v $ drop (length es1) tel) `applyE` es2
	_ | Just m' <- mvTwin mv, blocking -> do
	instantiate' (MetaV m' es)
	Open -> return t
	OpenInstance -> return t
	BlockedConst u | blocking -> instantiate' . unBrave $ BraveTerm u `applyE` es
	| otherwise -> return t
	PostponedTypeCheckingProblem _ -> return t
	instantiate' (Level l) = levelTm <$> instantiate' l
	instantiate' (Sort s) = Sort <$> instantiate' s
	instantiate' t = return t

It might be easier to just store the entire MetaStore in the interface, but from a performance perspective that could be suboptimal. Furthermore I guess that meta-variables from other modules should be treated differently from meta-variables from the current module. For instance, the following code in createInterface should presumably not unfreeze meta-variables from other modules (I don't know if this would have any effect, but with the current implementation of unfreezeMetas it could be costly):

agda/src/full/Agda/Interaction/Imports.hs

Line 1006 in 1fe6beb

unfreezeMetas

An alternative might be to treat instantiated meta-variables differently from other ones.

[nad]

I located some pieces of code that are at least linear in the size of the meta-store (if everything is evaluated strictly).

• The following four pieces could be improved by having separate meta-stores for open and closed meta-variables:

  agda/src/full/Agda/Interaction/BasicOps.hs

  Lines 822 to 825 in e204c14

  	typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
  	typesOfHiddenMetas norm = liftTCM $ do
  	is <- getInteractionMetas
  	store <- IntMap.filterWithKey (openAndImplicit is . MetaId) <$> getMetaStore

  agda/src/full/Agda/TypeChecking/MetaVars.hs

  Lines 1663 to 1670 in e204c14

  	openMetasToPostulates :: TCM ()
  	openMetasToPostulates = do
  	m <- asksTC envCurrentModule
  	-- Go through all open metas.
  	ms <- IntMap.assocs <$> useTC stMetaStore
  	forM_ ms $ \ (x, mv) -> do
  	when (isOpenMeta $ mvInstantiation mv) $ do

  agda/src/full/Agda/TypeChecking/Monad/MetaVars.hs

  Lines 550 to 556 in e204c14

  	getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
  	getMetaVariables p = do
  	store <- getMetaStore
  	return [ MetaId i | (i, mv) <- IntMap.assocs store, p mv ]
  	getOpenMetas :: ReadTCState m => m [MetaId]
  	getOpenMetas = getMetaVariables (isOpenMeta . mvInstantiation)

  Note that getMetaVariables is now only used by getOpenMetas.

  agda/src/full/Agda/TypeChecking/Monad/MetaVars.hs

  Lines 608 to 609 in e204c14

  	unfreezeMetas :: TCM ()
  	unfreezeMetas = modifyMetaStore $ IntMap.map unfreeze

  I guess there is no point in unfreezing instantiated meta-variables.

• I wonder if it would suffice for metasCreatedBy to return open metas:

  agda/src/full/Agda/TypeChecking/Monad/MetaVars.hs

  Lines 129 to 135 in e204c14

  	-- | Run a computation and record which new metas it created.
  	metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet)
  	metasCreatedBy m = do
  	before <- IntMap.keysSet <$> useTC stMetaStore
  	a <- m
  	after <- IntMap.keysSet <$> useTC stMetaStore
  	return (a, after IntSet.\\ before)

  I think the answer is yes if it suffices to have open metas in the argument allmetas to computeGeneralization:

  agda/src/full/Agda/TypeChecking/Generalize.hs

  Lines 149 to 154 in e204c14

  	-- | Compute the generalized telescope from metas created when checking the type/telescope to be
  	-- generalized. Called in the context extended with the telescope record variable (whose type is
  	-- the first argument). Returns the telescope of generalized variables and a substitution from
  	-- this telescope to the current context.
  	computeGeneralization :: Type -> Map MetaId name -> IntSet -> TCM (Telescope, [Maybe name], Substitution)
  	computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints $ do

  @UlfNorell, @jespercockx: Does that suffice?

• The following piece of code could be removed (note that conversion of a map to a set takes time):

  agda/src/full/Agda/TypeChecking/Monad/MetaVars.hs

  Lines 547 to 548 in e204c14

  	getMetaVariableSet :: ReadTCState m => m IntSet
  	getMetaVariableSet = IntMap.keysSet <$> getMetaStore

[jespercockx]

I think the answer is yes if it suffices to have open metas in the argument allmetas to computeGeneralization: [...]
@UlfNorell, @jespercockx: Does that suffice?

In general, no: the closed metas are used in that function (grep for generalizableClosed) for finding metavariables that should be transitively generalized because they occur in the solution of a generalizable meta. However, perhaps this could be done more eagerly by marking all metas in the solution of a generalizable meta as being generalizable when solving that meta. But I'm not 100% that this wouldn't have unintended side effects.

[nad]

OK, perhaps one could replace (the relevant instance of) metasCreatedBy by a mechanism that records created meta-variables as they are created. Then one could perhaps also address the following TODO note:

agda/src/full/Agda/TypeChecking/Generalize.hs

Lines 161 to 164 in 3a63943

	-- Issue 4727: filter out metavariables that were created before the
	-- current checkpoint, since they are too old to be generalized.
	-- TODO: make metasCreatedBy smarter so it doesn't see pruned
	-- versions of old metas as new metas.

Do you know if createMetasAndTypeCheck is ever invoked recursively?

agda/src/full/Agda/TypeChecking/Generalize.hs

Lines 129 to 136 in 3a63943

	-- | Create metas for the generalizable variables and run the type check action.
	createMetasAndTypeCheck :: Set QName -> TCM a -> TCM (a, Map MetaId QName, IntSet)
	createMetasAndTypeCheck s typecheckAction = do
	((namedMetas, x), allmetas) <- metasCreatedBy $ do
	(metamap, genvals) <- createGenValues s
	x <- locallyTC eGeneralizedVars (const genvals) typecheckAction
	return (metamap, x)
	return (x, namedMetas, allmetas)

Given code like the following (inside isType_) the answer might be yes (the argument to generalizeType s is supplied as part of the typecheckAction argument to createMetasAndTypeCheck):

agda/src/full/Agda/TypeChecking/Rules/Term.hs

Lines 131 to 132 in 3a63943

	A.Generalized s e -> do
	(_, t') <- generalizeType s $ isType_ e

Another question: Is all the information in MetaVariable needed for instantiated meta-variables, or would it suffice with only the instantiation?

[nad]

OK, perhaps one could replace (the relevant instance of) metasCreatedBy by a mechanism that records created meta-variables as they are created.

I found a simple way to optimise metasCreatedBy, making use of the fact that MetaIds are always increasing (as long as they do not wrap around).

[UlfNorell]

Don't forget to add a test case to test what happens when they wrap around!

[nad]

Some things that remain to be done:

• Have a separate meta-store for closed meta-variables.
• Optimise the pieces of code listed above. (One could also add openMetasCreatedBy, and use that in some cases.)
• Make it possible to refer to meta-variables from other modules without ambiguity.
• Store meta-variables in interfaces.
• Stop using instantiateFull when eliminating dead code, and when creating interfaces.

[nad]

Another question: Is all the information in MetaVariable needed for instantiated meta-variables, or would it suffice with only the instantiation?

Sometimes there are interaction points corresponding to solved meta-variables. I guess that getInteractionScope can be invoked for such meta-variables.

[nad]

Make it possible to refer to meta-variables from other modules without ambiguity.

I'm thinking of changing the representation of MetaId so that it contains two Word64 values, like NameId:

agda/src/full/Agda/Syntax/Common.hs

Lines 2331 to 2333 in 382861b

	-- | The unique identifier of a name. Second argument is the top-level module
	-- identifier.
	data NameId = NameId {-# UNPACK #-} !Word64 {-# UNPACK #-} !ModuleNameHash

What promises do we make about the results of the following functions?

agda/src/data/lib/prim/Agda/Builtin/Reflection.agda

Lines 83 to 84 in 382861b

	primShowMeta : Meta → String
	primMetaToNat : Meta → Nat

[nad]

@jespercockx, @UlfNorell: Do we not make any promises (other than injectivity)?

[jespercockx]

I think the "promise" (if you want to call it that) is that the TC primitives do roughly the same as the actual Agda typechecker itself, so the numbers/names ought to correspond to what the user sees in error messages and such. I am not sure how important it is to keep this promise, though.

[UlfNorell]

I think it would be good if you could still use those functions to implement a pretty printer for Term that matches (more or less) how Agda prints terms.

[nad]

I suppose that the implementations should match the implementations in Agda.Compiler.MAlonzo.Primitives (but I don't know if you can construct a Meta that can be used at runtime without using the FFI).

[jespercockx]

Well, about that...

open import Agda.Builtin.IO
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.String
open import Agda.Builtin.Unit

macro
  getMeta : Term → TC ⊤
  getMeta hole@(meta m _) = quoteTC m >>= unify hole
  getMeta _ = typeError []

myMeta : Meta
myMeta = getMeta

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}

main : IO ⊤
main = putStrLn (primShowMeta myMeta)

Trying to compile this with the GHC backend this produces an internal error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Compiler/MAlonzo/Compiler.hs:1097:18 in Agda-2.6.3-2GgStRv6exQAe2hnultIdP:Agda.Compiler.MAlonzo.Compiler

[nad]

Please open a separate issue for that bug.

[nad]

Is it a problem if the numbers created by primMetaToNat are large (2^64 times the module name hash plus the sequential meta-variable number)? Are there any reasonable tactics that do something recursive with the natural numbers that you obtain from this function? Using the equality and ordering tests from Agda.Builtin.Nat should be fine.

[jespercockx]

Are there any reasonable tactics that do something recursive with the natural numbers that you obtain from this function?

I think they're just meant to be unique identifiers, so I would really hope no-one ever recurses on them.

[nad]

• I am especially uncertain about the code under Agda.Auto, which I have mostly ignored, and which we have few tests for.

I can add some comments to the relevant files.

I opted to replace the calls to lookupLocalMeta with a variant that notes that the auto command does not support remote meta-variables, and that suggests the use of --no-save-metas.

I can add a note to the documentation of lookupMeta.

Done.

[andreasabel]

AIMXXXVII: @AndrasKovacs is working on sharing metas and, to this end, printing of interfaces, and noticed that there are no metas in definitions even with --save-metas. Maybe not surprising because the clauses are fully instantiated:

agda/src/full/Agda/TypeChecking/Rules/Def.hs

Lines 357 to 362 in 4460544

	cs <- instantiateFull {- =<< mapM rebindClause -} cs
	-- Andreas, 2010-11-12
	-- rebindClause is the identity, and instantiateFull eta-contracts
	-- removing this eta-contraction fixes issue 361
	-- however, Data.Star.Decoration.gmapAll no longer type-checks
	-- possibly due to missing eta-contraction!?

The absence of metas would explain the lack of performance gain by --save-metas, and the slight increase of the size of the interface files. Meta solutions are then stored, taking some space, but since no meta solutions are reused, there are no savings.

[nad]

AIMXXXVII: @AndrasKovacs is working on sharing metas and, to this end, printing of interfaces, and noticed that there are no metas in definitions even with --save-metas. Maybe not surprising because the clauses are fully instantiated:

@UlfNorell and I added that call to instantiateFull in 2010. The commit message contains some motivation: d6d50f4.