[Agda] Odd `with' desugaring?

Daniel Peebles pumpkingod at gmail.com
Sun Dec 20 02:26:12 CET 2009 

Hi all,

I notice that Nils has kindly made the changes to the standard library to
make Relation.Unary and Induction.* universe-polymorphic! Thanks Nils! So
now I have a bit of time, I'm moving ahead with my attempt to make
Data.Graph.Acyclic universe-polymorphic too, and have mostly succeeded.
However I encountered this strange behavior for the auxiliary function p in
the preds function.

The original version is as follows:

preds <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032>
: ∀ {E <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6043>
N <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6045>
n <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6047>}
→ Graph <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#1779>
N <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6045>
E <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6043>
n <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6047>
→ (i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6067>
: Fin <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#740> n
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6047>)
→ List <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#672>
(Fin′ <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#967> i
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6067>
× <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#792> E
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6043>)preds
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032>
g <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6104>
      zero <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#762>
   = [] <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#709>preds
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032>
(c <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6132>
& <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#1847>
g <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6136>)
(suc <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#793> i
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6144>)
=
  List <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1009>._++_
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1009> (List
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#6139>.gfilter
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#6139> (p
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260>
i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6144>)
$ <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#1474>
successors <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#1366>
c <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6132>)
            (List
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1321>.map
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1321> (Prod
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#1699>.map
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#1699>
suc id <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#1007>)
$ <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#1474>
preds <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032>
g <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6136>
i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6144>)
  where
  p <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260>
: ∀ {E <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6267>
: Set} {n <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6277>}
(i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6281>
: Fin <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#740> n
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6277>)
→ E <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6267>
× <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#792>
Fin <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#740> n
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6277>
→ Maybe <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Maybe.Core.html#323>
(Fin′ <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#967>
(suc <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#793> i
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6281>)
× <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#792> E
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6267>)
  p <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260>
i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6335>
(e <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6338>
, <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509> j
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6342>)
 with i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6335>
≟ <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.Props.html#2176>
j <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6342>
  p <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260>
i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6361>
(e <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6364>
, <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509>
.i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6361>)
| yes <http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.Core.html#513>
refl <http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Binary.Core.html#4468>
= just <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Maybe.Core.html#361>
(zero , <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509>
e <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6364>)
  p <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260>
i <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6405>
(e <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6408>
, <http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509> j
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6412>)
 | no <http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.Core.html#540>
_     = nothing
<http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Maybe.Core.html#391>

So I modified it to put E and N in an arbitrary universe, and thus had
to modify the p function to put E in the arbitrary universe too:

  p : ∀ {e} {E : Set e} {n} → (i : Fin n) → E × Fin n → Maybe (Fin′
(suc i) × E)  p i (e , j)  with i ≟ j  p i (e , .i) | yes refl = just
(zero , e)  p i (e , j)  | no _     = nothing

y attemp which is identical to the original p, with an additional implicit
argument for the level of E in its type. This fails with:

Dec (i' ≡ j) !=< Level of type Set

on the i ≟ j line, supposedly in the `w' expression. I'm not really
sure where `w' came from so I'm assuming it's from the desugaring of
the with construct. As a workaround, if I manually make a q function
that takes the Dec result of i ≟ j and matches on it, the whole thing
works fine.

Am I missing something?

Thanks,

Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091219/28e36d2c/attachment-0001.html

More information about the Agda mailing list