Internal error when using REWRITE in private block

[HarrisonGrodin]

After moving a local module Foo to a new file Data/Nat/Foo.agda, I encountered the following error message:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/Monad/Signature.hs:703:32 in Agda-2.6.2-2KH299XtsFY3naRbMMwQRG:Agda.TypeChecking.Monad.Signature

The new file typechecks on its own, but when I add open import Data.Nat.Foo to my existing file, the given error is produced.

(I'm using --rewriting in both files - not sure if that's relevant.)

[HarrisonGrodin]

Aha - got a MWE! Looks like it has to do with defining REWRITEs under a private block, and then using the rewrite in conjunction with another function.

-- Bar.agda

{-# OPTIONS --prop --without-K --rewriting #-}

module Bar where

open import Data.Nat
open import Data.Nat.Properties

open import Relation.Binary.PropositionalEquality

open import Agda.Builtin.Equality.Rewrite

private
  foo : ℕ → ℕ
  foo zero    = zero
  foo (suc n) = suc (foo n + zero)

bar : ℕ → ℕ
bar n = foo n

private
  lemma : ∀ n → foo n ≡ n
  lemma zero    = refl
  lemma (suc n) = cong suc (trans (+-identityʳ (foo n)) (lemma n))
  {-# REWRITE lemma #-}

-- Example.agda

{-# OPTIONS --prop --rewriting #-}

module Example where

open import Data.Nat
open import Data.Nat.Properties
open import Bar
open import Data.List

example : ∀ l → 0 ≤ bar (length l)
example l =
  let open ≤-Reasoning in
  begin
    {!   !}
  ≡⟨ {!   !} ⟩
    {!   !}
  ∎

Bar.agda is fine, but loading Example.agda produces the error. (In the short term, I can solve the issue by moving the rewrite out of a private block.)

[HarrisonGrodin]

(Possible that #5451 is related.)

[andreasabel]

Thanks for the small example.
Here is a version without the standard library:

{-# OPTIONS --rewriting #-}

module Issue5470Import where

open import Agda.Builtin.Nat

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

private
  postulate
    foo : Nat → Nat

bar : Nat → Nat
bar n = foo n

private
  postulate
    lemma : ∀ n → foo n ≡ n
  {-# REWRITE lemma #-}

{-# OPTIONS --rewriting #-}
{-# OPTIONS -v impossible:10 #-}

module Issue5470 where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

open import Issue5470Import

postulate
  _≤_ : (n m : Nat) → Set
  ≤-refl : ∀{n} → n ≤ n

infix 4 _IsRelatedTo_

data _IsRelatedTo_ (x : Nat) : (y : Nat) → Set where
  equals : x IsRelatedTo x

begin : ∀ {x y} → x IsRelatedTo y → x ≤ y
begin equals = ≤-refl

example : ∀ n → 0 ≤ bar n
example n = begin equals

-- Unbound name: Issue5470Import.lemma[0,10]@ModuleNameHash 8608063155492000951

That's what I call a MWE! ;-)
(Well, I am sure this isn't yet minimal...)

[andreasabel]

The problem is that instantiateRewriteRule calls freeVarsToApply which calls getConstInfo, expecting the QName to be in scope:

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

Lines 1100 to 1106 in ef433be

	instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m,
	ReadTCState m, MonadTCEnv m, MonadDebug m)
	=> RewriteRule -> m RewriteRule
	instantiateRewriteRule rew = do
	traceSDoc "rewriting" 95 ("instantiating rewrite rule" <+> pretty (rewName rew) <+> "to the local context.") $ do
	vs <- freeVarsToApply $ rewName rew
	let rew' = rew `apply` vs

I wonder whether this is the golden way to instantiate a rewrite rule, given that rewrite rules live in their own structure in the interface. Maybe the desired information should be added to this record so that rewrite rules remain independent from the signature, @jespercockx ?

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

Lines 1709 to 1718 in ef433be

	data RewriteRule = RewriteRule
	{ rewName :: QName -- ^ Name of rewrite rule @q : Γ → f ps ≡ rhs@
	-- where @≡@ is the rewrite relation.
	, rewContext :: Telescope -- ^ @Γ@.
	, rewHead :: QName -- ^ @f@.
	, rewPats :: PElims -- ^ @Γ ⊢ f ps : t@.
	, rewRHS :: Term -- ^ @Γ ⊢ rhs : t@.
	, rewType :: Type -- ^ @Γ ⊢ t@.
	, rewFromClause :: Bool -- ^ Was this rewrite rule created from a clause in the definition of the function?
	}

[jespercockx]

freeVarsToApply is just the current value of the module parameters for a given definition, right? I don't see why we should duplicate this information just because rewrite rules happen to live in a different part of the signature. Perhaps we could instead just forbid private rewrite rules until #2335 is implemented?

[andreasabel]

For a QName imported from another file, freeVarsToApply should be 0. But isn't it more generally, that if a QName is not in scope because it is private, it is not in a child module of its defining module, so there are no free vars to apply?

Setting freeVarsToApply to 0 for not-in-scope rewrite rules would then fix this problem. (Rewrite rules are never private then for the sake of subject reduction...)

I am trying out a simple fix of freeVarsToApply now...