[Agda] Bugs

[Pierre Hyvernat]

Hello,


I now have a shiny new Agda working correctly, and I can do some
dependent typing for fun and profit...


I stumbled upon 2 small bugs:


(1) the first one is easily replicable and only concerns the emacs
interface. The string "--" inside a comment seems to have strange
effects in Emacs: goals do not show up as goals, even if
they exist (ie "show goals" works, but "next goal" doesn't)...

Minimal example: toto.agda
====
module toto where

{- BU--G -}
X : Set
X = ?
=====EOF=====

(A comment {-- ... -} is fine, but a comment {- ... --} is not.)



(2) the second is probably more important: I managed to get the
following message:

  An internal error has occurred. Please report this as a bug.
  Location of the error: src/full/Agda/TypeChecking/Substitute.hs:130

I attach a file exhibiting the problem, but I haven't really been able
to reduce it to a minimal case.

The problem comes from the module EquivalenceSimulation, more precisely
from lines 115/116 (let open ... in). If those two lines are moved out
of the definition, everything typechecks.


If one of the Agda hackers can spot the problem, good. Otherwise, I can
try to find a minimal example...
(It seems to be quite subtle: it depends on being inside the module,
having some "let ... in" in two different places.)




Pierre
-- 
Reality is that which, when you stop believing in it,
doesn't go away.
    -- Philip K. Dick
-------------- next part --------------
module toto where

{- ? type -}
data ? (X : Set) (Y : X ? Set) : Set where
 <_,_> : (x : X) ? Y x ? ? X Y

_?_ : (A : Set) ? (B : Set) ? Set
_?_ A B = ? A (? _ ? B)

{- simple elimination rules -}
?1 : {X : Set} ? {Y : X ? Set} ? (? X Y) ? X
?1 < x , _ > = x

?2 : {X : Set} ? {Y : X ? Set} ? (p : ? X Y) ? Y (?1 p)
?2 < _ , y > = y


{- ? type -}
data ? (X : Set) (Y : X ? Set) : Set where
 fun :  ((x : X) ? Y x) ? ? X Y
app : {X : Set} ? {Y : X ? Set} ? (? X Y) ? (x : X) ? Y x
app (fun f) x = f x


Pow : Set ? Set1
Pow S = S ? Set

Rel : Set ? Set ? Set1
Rel S T = S ? T ? Set

{- "predicate transformers" from S to T (those correspond to functors
   from ?/S to ?/T) -}
PT : Set ? Set ? Set1
PT S T = Pow S ? Pow T


{- direct image of a relation -}
?_? : {S : Set} ? {T : Set} ? Rel S T ? PT S T
?_? {S} {T} R  =  \U ? \t ? ? S (\s ? R s t ? U s)


{- composition of predicate transformers -}
_?_ : {S1 : Set} ? {S2 : Set} ? {S3 : Set} ? PT S2 S3 ? PT S1 S2 ? PT S1 S3
_?_ P Q = \U ? P (Q U)


{- order on predicate transformers (natural transformations between
   the corresponding functors) -}
_?_ : {S : Set} ? {T : Set} ? PT S T ? PT S T ? Set1
_?_ {S} {T} P Q = (U : S ? Set) ? ? T (? t ? P U t ? Q U t)



{- Simulations on PT -}
SimProofPT : {S1 : Set} ? {S2 : Set} ? (Rel S1 S2) ? (P1 : PT S1 S1) ? (P2 : PT S2 S2) ? Set1
SimProofPT R P Q = (? R ? ? P) ? (Q ? ? R ?)

record SimPT {S : Set} {T : Set} (P : PT S S) (Q : PT T T) : Set1 where
  field
    R : Rel S T
    sim : SimProofPT R P Q



{-=====================-}
{- Polynomial functors -}
{-=====================-}


{- type for polynomial endofunctors over S -}
record PF (T : Set) (S : Set) : Set1 where
  field
    A     : S ? Set
    D     : {s : S} ? (A s) ? Set
    n     : {s : S} ? {a : A s} ? (D a) ? T


{- going from PF to PT -}
PFtoPT : {S : Set} {T : Set} ? (PF S T) ? (PT S T)
PFtoPT P = let open PF P in
           ? U ? ? t ? ? (A t) (? a ? ? (D a) (? d ? U (n d)))


{- Simulations on polynomial functors -}
SimProofPF : {S1 : Set} ? {S2 : Set} ? (Rel S1 S2) ? (P1 : PF S1 S1) ? (P2 : PF S2 S2) ? Set
SimProofPF {S1} {S2} R P1 P2 = (s1 : S1) ?
                               (s2 : S2) ?
                               (R s1 s2) ?
                                 ? (PF.A P1 s1)      (? a1 ?
                                 ? (PF.A P2 s2)      (? a2 ?
                                 ? (PF.D P2 a2)      (? d2 ?
                                 ? (PF.D P1 a1)      (? d1 ?
                                   R (PF.n P1 d1) (PF.n P2 d2)))))

record SimPF {S : Set} {T : Set} (P : PF S S) (Q : PF T T) : Set1 where
  field
    R : Rel S T
    sim : SimProofPF R P Q




{-=================================================-}
{- transforming between the 2 kinds of simulations -}
{-=================================================-}

module EquivalenceSimulation (S1 : Set) (S2 : Set)
 (P1 : PF S1 S1)
 (P2 : PF S2 S2)
 (R : Rel S1 S2)
 where

  SimPFtoPT : SimProofPF R P1 P2 ? SimProofPT R (PFtoPT P1) (PFtoPT P2)
  SimPFtoPT sim =
    let open PF P1 renaming (A to A1 ; D to D1 ; n to n1) in
    let open PF P2 renaming (A to A2 ; D to D2 ; n to n2) in
    ? U ?
    fun (? s2 ?
    ? p ?    let s1 = ?1 p in
             let r = ?1 (?2 p) in
             let a1 = ?1 (?2 (?2 p)) in
             let f1 = app (?2 (?2 (?2 p))) in
             let a2 = ?1 (app (sim s1 s2 r) a1) in
             let f2 = app (?2 (app (sim s1 s2 r) a1)) in
      <
        a2 ,
        fun (? d2 ?    let d1 : D1 a1
                           d1 = ?1 (f2 d2) in
                       let nr : R (n1 d1) (n2 d2)
                           nr = ?2 (f2 d2) in
          < n1 d1 , < nr , f1 d1 > >)
      >)