[Agda] Agda crash caused by excessive unfolding

[Thomas Hallgren]

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

-------------- next part --------------
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
 #-}