Unclear specification and correctness of TypeChecking/DeadCode

[AndrasKovacs]

Unclear specification and correctness of TypeChecking/DeadCode

[nad]

If we don't have --save-metas, then none of bs, sigRewriteRules and disp are instantiated and traversed for reachability. Hence, the metas which only occur in these will be eliminated, and should become dangling in the interface. As I see now, the only way this could work correctly in practice is if the mentioned things are already fully instantiated (which may well be the case in the current codebase).

Perhaps @UlfNorell knows why this is supposed to work.

Also, sigSections looks puzzling in rootMetas. The public sections are already traversed for reachability, in reachableFrom. This leaves the non-public sections here as additionally traversed, but I don't understand why the metas there should be roots.

@andreasabel seems to have done some work on this recently (d12ad84).

[UlfNorell]

The rootMetas was added by @nad in b52a21d when --save-metas was added. I don't know why those particular root sets where chosen. The basic specification should be straightforward though: don't delete things that may be referenced from a module importing this module, and delete everything else.

[AndrasKovacs]

After testing the current implementation a bit, I can point out more concrete problems:

• Rewrite rules and module parameters can cause crash.
• I could not produce a crash with display forms, but IMO they behave weirdly.
• Rewrite rules and pattern synonyms are never pruned, but they could be.

Rewrite rule crash. b is eliminated but it's reachable through a rewrite rule.

-- A.agda
{-# OPTIONS --rewriting #-}
module A where

postulate Rel : ∀{i}{A : Set i}(x y : A) → Set
{-# BUILTIN REWRITE Rel #-}

postulate a : Set₁

private
  b : Set₁
  b = Set
  postulate a~> : Rel a b
  {-# REWRITE a~> #-}

-- B.agda
{-# OPTIONS --rewriting #-}

module B where
open import A

_ : a
_ = Set

Module param crash. P is eliminated but it's reachable through M.

-- A.agda
module A where
private P = Set₁
module M (x : P) where

-- B.agda
module B where
open import A
module M' = M Set

Display form behavior which I don't think is desirable:

-- A.agda
module A where

postulate a : Set
private postulate b : Set
c : Set
c = b
{-# DISPLAY a = b #-}

-- B.agda
module B where
open import A

_ : Set
_ = {!!}

Here, if I print the normal form of c in the B.agda hole, I get A.b. But if I print the nf of a, I get a.

Based on the above, I have this proposal for liveness:

• Public definitions and pattern synonyms are alive.
• Any definition which is a primitive or has a COMPILE pragma is alive.
• Display forms whose LHS-es only contain live symbols are alive, and so are their RHS-es.
• Rewrite rules whose LHS-es only contain live symbols are alive, and so are their RHS-es.
• Parameters of public modules are alive.

Questions and comments:

• I don't think currently there is a way to detect whether a rewrite rule or a display pragma was defined in a private block. Is this correct? If there was a way, it would make sense to always consider "private" rewrites and displays dead.
• I don't understand this comment in Interaction/Imports.

[AndrasKovacs]

I realized that checking my previous liveness proposal is rather hard, and right now I don't know any efficient way to do it. The problem is the LHS liveness conditions plus the arbitrary mutual dependencies in rewrite rules and display forms.

The following looks efficiently decidable: we only pick a single LHS head symbol for each rewrite rule and display form. If the head symbol is alive, every other symbol involved in the rewrite/display is alive.

This can be checked by first building a map from symbols to lists of rewrites/displays, and in the next phase, when we traverse a symbol for reachability, we also traverse the rewrites/displays headed by the symbol.

[AndrasKovacs]

Discovered another issue while working on this: make std-lib-compiler-test crashes with --save-metas, apparently hitting a meta that's not defined anywhere.