[Agda] The impossible happened.

[Dan Doel]

Hello,

I've been playing a bit with translating into Agda a category theory example 
Conor McBride posted to the Epigram list a while back, and believe I have 
stumbled into a bug. The code in question is as follows:

data Eq {a : Set} : a -> a -> Set where
  refl : {x : a} -> Eq x x

record Category (O : Set1)
                (_-->_ : O -> O -> Set) : Set1 where
  field
    id     : forall {a} -> a --> a
    _comp_ : forall {a b c} -> (b --> c) -> (a --> b) -> (a --> c)
    -- laws
    left-id  : forall {a b}{f : a --> b} -> Eq (id comp f) f
    right-id : forall {a b}{f : a --> b} -> Eq (f comp id) f
    comp-assoc : forall {a b c d}
                        {h : c --> d}
                        {g : b --> c}
                        {f : a --> b}
                        -> Eq ((h comp g) comp f) (h comp (g comp f))

record Functor {O1 : Set1}
               {_-1>_ : O1 -> O1 -> Set}
               {O2 : Set1}
               {_-2>_ : O2 -> O2 -> Set}
               (Cat1 : Category O1 _-1>_)
               (Cat2 : Category O2 _-2>_) : Set1 where
  open Category Cat1 renaming (id to id1 ; _comp_ to _comp1_)
  open Category Cat2 renaming (id to id2 ; _comp_ to _comp2_)
  field
    F   : O1 -> O2
    map : forall {a b} -> (a -1> b) -> (F a -2> F b)
    -- laws
    map-id : Eq (map id1) id2
    map-comp : forall {a b c}{f : a -> b}{g : b -> c}
                -> Eq (map (g comp1 f)) (map g comp2 map f)

If I comment out the functor laws (map-id and map-comp), everything works 
fine, but Agda seems to die if it tries to type check either of them. In the 
emacs mode, this is detectable by colors not updating (if you comment them, 
check, uncomment and then check again, they'll stay red). If I try to load 
the file using 'agda -I' I get a message "agda: 
src/full/TypeChecking/Substitute.hs:115: the impossible happened".

I believe my install is up-to-date from darcs as of a day or two ago (although 
the impossible macro in Substitute.hs seems a few lines lower than that error 
message indicates, so perhaps I did something wrong when rebuilding).

Thanks for your time.
-- Dan Doel