[Agda] Type checker changes its mind

[Peter G. Hancock]

Hello,

Here's a small piece of agda where the type-checker seems
to change its mind.  

If you go to the first hole, and do cases on Gamma, it
expands to something reasonable.  But if you then re-check
the buffer, the type-checker no longer thinks it makes
sense.  This seems inconsistent.

Shouldn't the type-checker accept it? 

One thing I would dearly like some over-worked employee of Chalmers to
produce is a written explanation of the type-checking of mutual recursions
such as these (and other IR) definitions, at least `what goes on'.  (I
vaguely remember Thierry saying (sometime in the late 20'th century)
that it is in two passes, where first you check the types of the
definitions, and then second you check the bodies -- but I would like
something to refer to when I run into the issue.)

Peter

mutual
   Sort :: Set = data Cxt
                    | Cm (Delta :: ElCxt) (Gamma :: ElCxt)
                    | Ty (Gamma :: ElCxt)

   El (s :: Sort) :: Set
        = case s of
            (Cxt) -> data Cxt0
                        | Ext (Gamma :: ElCxt) (A :: ElTy Gamma)
            (Cm Delta Gamma) -> {! !}
            (Ty Gamma) -> {! !}

   ElCxt :: Set = El Cxt at Sort

   ElTy (Gamma :: ElCxt) :: Set = El (Ty at Sort Gamma)