[Agda] Agda crash caused by excessive unfolding

[takeyama]

Dear Thomas,

Thank you very much for the bug report.

  > I enclose an example where Agda's does too much unfolding when it 
  > displays types of meta variables.

This is a long-standing problem that Agda does not know how to fold an
expression to a constant name, even when something obvious is in scope.
(It knows how not to unfold constants in scope, but the problem here
is not helped by that.)

Unsatisfactory workarounds are  
  1.  Make i abstract if that's appropriate, or
  2.  Make dependency of A on i explicit, like 

      package P2 where
         ....
         A(i'::E B)::Set
           = (p::B) -> PredT (f B i' p)
         proofA0 ::A i
           =  \(p::B) -> {! !}

      package P3 where
         open P1  use  B,  f, E, B
         open P2  use  i,  A
         proofA1 ::A i
           =  \(p::P1.B) -> {! !}

In Agda, all defined constants are given unique names and kept
at the top-level, together with the info on free variables at the
points of their definitions (in a sense lambda-lifted).

In the example, the type of the meta in proofA1 is something like
  (PredT#86 {}) ((f#88 {}) (B#85 {}) (i#90 {}) p#108)
Except for p#108 (the nearest bound var), all others are constants
defined in P2.  i#90, as opposed to i#103
defined in P3, is not in scope.  So Agda unfolds it, trying not to
print out-of-scope i#90.  This is not the matter of how not to unfold i#103.

Incidentally, PredT#86 prints out as P1.PredT not because PredT is
defined so in P3, but because it is defined so in P2.  If you merge P1
and P2, you will see the type of meta in proofA1 printed as just PredT
p despite PredT is not in scope.  Agda tries to unfold PredT, but it
results in a stuck case-expression, which is not allowed as a form of
values, and backtrack to plain PredT.  This is another of
long-standing problem.)

   > 1. If the unfolded definition is recursive, Agda can crash with a
   >    stack overflow. To see this in the enclosed example, complete the
   >    definition of P1.i by instantiating the meta variable to i.

Yes, crashing is a bug.  I have just now commited Imitate.hs that
uses the termination counter.

   > The version of Agda that I used is from October 2004, so perhaps this 
   > problem has been solved already? I tried to repeat the test with 

I haven't tried the Midsummer version yet, but the situation would be
the same, I believe.  The Midsummer version has big changes in the
concrete syntax, like f(x::A)::B = e and f(|x::A)::B = e have their
meaning switched.

Best Wishes,
Makoto


  > X-Original-To: agda at lists.chalmers.se
  > Date: Fri, 22 Jul 2005 15:46:28 -0700
  > From: Thomas Hallgren <hallgren at cse.ogi.edu>
  > X-Scanned-By: MIMEDefang 2.25 (www . roaringpenguin . com / mimedefang)
  > Sender: agda-bounces at lists.chalmers.se
  > 
  > This is a multi-part message in MIME format.
  > --------------050109000700030301090807
  > Content-Type: text/plain; charset=ISO-8859-1; format=flowed
  > Content-Transfer-Encoding: 7bit
  > 
  > Hi,
  > 
  > I enclose an example where Agda's does too much unfolding when it 
  > displays types of meta variables.
  > 
  > The problem seems to occur only when packages are involved. The meta 
  > variable in P2.proofA0 has the same type as the meta variable in 
  > P3.proofA1, but when Agda displays the type of the latter, the 
  > definition of P2.i is unfolded. The problem goes away if P1 and P2 (or 
  > P2 and P3) are combined into one package.
  > 
  > There are two reasons why this excessive unfolding is a problem:
  > 
  >    1. If the unfolded definition is recursive, Agda can crash with a
  >       stack overflow. To see this in the enclosed example, complete the
  >       definition of P1.i by instantiating the meta variable to i.
  >    2. Even if Agda doesn't crash, the unfolding can cause a code size
  >       explosion. In one proof I worked on in Alfa, I had to turn off
  >       automatic constraint solving, and fill in a lot of type arguments
  >       manually to avoid getting copies of large function definitions at
  >       every proof step.
  > 
  > The version of Agda that I used is from October 2004, so perhaps this 
  > problem has been solved already? I tried to repeat the test with 
  > Agda-1.1-Midsummer-i386-Linux.tgz, but after working around some syntax 
  > problems, I got a type error that I didn't understand...
  > 
  > ---  ("info" ("* Agda version *" "Agda with idata and implicit 
  > arguments\n\n[ghc604; built Jun 24 2005 10:53:00]")) +++
  >  >> load bug.alfa
  > ---  ("error" ("At: \"bug.alfa\", line 10, column 16\nError in the 
  > telescope of f because:\nMore function arguments than the function type 
  > specifies: E")) +++
  > 
  > -- 
  > Thomas H
  > 
  > 
  > --------------050109000700030301090807
  > Content-Type: text/plain;
  >  name="bug.alfa"
  > Content-Transfer-Encoding: 7bit
  > Content-Disposition: inline;
  >  filename="bug.alfa"
  > 
  > package P1 where
  >   Triviality ::Set
  >     = sig {}
  >   data B   = T
  >   PredT (b::B) :: Set
  >     = case b of { (T) -> Triviality;}
  >   E (a::Set) :: Set
  >     = sig{f :: a -> B;
  >           g :: a -> B;}
  >   f (a::Set)(d::E a) :: a -> B
  >     = d.f
  >   default_g (a::Set)(d::E a) :: a -> B
  >     = f a d
  > 
  > package P2 where
  >   open P1  use  Triviality,  B,  PredT,  E,  f,  default_g
  >   i ::E B
  >     = struct {
  >         f ::B -> B
  >           =  \(h::B) -> h;
  >         g ::B -> B
  >           = default_g B ?;}
  >   A ::Set
  >     = (p::B) -> PredT (f B i p)
  >   proofA0 ::A
  >     =  \(p::B) -> ?
  > 
  > package P3 where
  >   open P1  use  B,  f
  >   open P2  use  i,  A
  >   proofA1 ::A
  >     =  \(p::P1.B) -> ?
  > {-# Alfa unfoldgoals off
  > brief on
  > hidetypeannots off
  > wide
  > 
  > nd
  > hiding on
  >  #-}
  > 
  > --------------050109000700030301090807
  > Content-Type: text/plain; charset="us-ascii"
  > MIME-Version: 1.0
  > Content-Transfer-Encoding: 7bit
  > Content-Disposition: inline
  > 
  > _______________________________________________
  > Agda mailing list
  > Agda at lists.chalmers.se
  > https://lists.chalmers.se/mailman/listinfo/agda
  > 
  > --------------050109000700030301090807--
  >