double `with' error

[GoogleCodeExporter]

This is on  Development Agda of August 19, 2014,  library of August 19, 2014.

  unzip repAug12-2014.zip

  agda -c $agdaLibOpt Main.agda

reports

--------------------------------------------------                              
...
...
Checking OfMultiset (/home/mechvel/doconA/0.03/reports/jul12-2014/
                                              OfMultiset.agda).
  Finished OfMultiset.
 Finished AlgClasses5.
 Checking GCD2 (/home/mechvel/doconA/0.03/reports/jul12-2014/GCD2.agda).
  Skipping Data.List.All.Properties
    (/home/mechvel/agda/stLib/july30-2014/src/Data/List/All/Properties.agdai).
  Checking Ring1Properties (/home/mechvel/doconA/0.03/reports/jul12-2014/
                                     Ring1Properties.agda).
  Finished Ring1Properties.
/home/mechvel/doconA/0.03/reports/jul12-2014/GCD2.agda:181,71-77
.w !=
(zip5with ^eq P2 P3 P4 makeItem
 (map
  (Data.Product.uncurry
   (λ cl e →
      fromAsd cl ,
      e ,
      (AlgClasses4.RingWithOne.*monoid
       (AlgClasses4.CommutativeRing.ringWithOne
        (AlgClasses4.IntegralRing.commutativeRing
         (GCDRing.IR (.AlgClasses5.OverGCDRing-pack.gcdRing upGCD))))
       Monoid.^ fromAsd cl)
      e))
  (AssocList-pack.AssocList.pairs aList))
 all^eq-ext exps>'0 allPrime' primaries∣')
of type (List (PrimaryItem a))
when checking that the expression nullFt has type Null primaryItems
--------------------------------------------------                              

This is on the function
    ----------------------------------------------------------                  
    a≉0 : a ≉ 0#
    a≉0   with  primaryItems | null? primaryItems
    ...
        | _ | yes nullFt =  ∣1→≉0 a∣1
                                 where
                                 a∣1 : a ∣ 1#
                                 a∣1 = (proj₁ nullFactorization←→a∣1) nullFt

    ... | [] | no notNullFt =  ⊥-elim $ (>→≢ l>0) l=0
                               where
                               l>0 : length primaryItems > 0
                               l>0 = ¬Null→length>0 primaryItems notNullFt

                               postulate l=0 : length primaryItems ≡ 0

    ... | it ∷ items | _ =  a/=0  where   postulate a/=0 : a ≉ 0#
    ---------------------------------------------------------------             

    ---------------------------------------------------------------             

in  GCD2.agda.

I wonder, what is wrong there.

Changing this to

        with  null? primaryItems     -- this is type-checked                    
    ...
        | yes nullFt = ∣1→≉0 a∣1
                             where
                             a∣1 : a ∣ 1#
                             a∣1 = (proj₁ nullFactorization←→a∣1) nullFt

    ... | no notNullFt =  ⊥-elim $ (>→≢ l>0) l=0
                               where
                               l>0 : length primaryItems > 0
                               l>0 = ¬Null→length>0 primaryItems notNullFt

                               postulate l=0 : length primaryItems ≡ 0

makes it type-checked.
But I need to accomplish the first variant.

-------------------------------------------------------                         
1) Many places in the project are replaced with `postulate',
   in order to make the example smaller.
2) It can be reduced further, many times.

Original issue reported on code.google.com by mech...@botik.ru on 19 Aug 2014 at 5:50

[GoogleCodeExporter]

Original comment by mech...@botik.ru on 19 Aug 2014 at 5:52

Attachments:

• repAug12-2014.zip

[GoogleCodeExporter]

The problem is that you've with-abstracted over primaryItems (calling it w), 
but nullFactorization<->a|1 still talks about primaryItems so it won't accept 
nullFt : Null w. This becomes clear if you put nullFt in a hole (by adding {! 
!} around it) and hit "C-c C-.". That will tell you

  Goal: Null primaryItems
  Have: Null .w

Anyway, this is not the place for these kinds of issues. There are lots of 
helpful people on the mailing list or the IRC channel that can help you when 
your code doesn't work. If you have something that you have good reason to 
believe is a bug in Agda, then please submit it here, but if it's just that you 
can't figure out how to get your program through the type checker the mailing 
list or IRC channel is a better place.

Original comment by ulf.nor...@gmail.com on 20 Aug 2014 at 8:03

• Changed state: Invalid