[Agda] Type checker changes its mind

[anton setzer]

Peter G. Hancock wrote:

> 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)
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>  
>
I agree that it is odd that the system creates a case distinction and then
rejects it. I have come across this myself before, and it is very odd.

A rule of thumb to get around this problem is:
- never have any data ... construct after a case distinction.
 Always define this data... construct separately

 (By the way has anybody a good name for the data... construct?
  I am always confused about the terminology at this point.  Or is it 
one of
   {data type, algebraic data type, algebraic type} ?
  (for me algebraic data type is something defined strictly positively 
inductively,
   but maybe I am wrong).

Maybe one should make this something which is to be checked 
(syntactically),
or look into, why this principle has to hold, and whether one cannot
modify the type checker so that it is no longer necessary.

In this example the solution looks like this:
mutual
  Sort :: Set = data Cxt
                   | Cm (Delta :: ElCxt) (Gamma :: ElCxt)
                   | Ty (Gamma :: ElCxt)

  El (s :: Sort) :: Set
       = case s of
           (Cxt) -> ElCxt
           (Cm Delta Gamma) -> ElCm Delta Gamma
           (Ty Gamma) -> ElTy Gamma

  ElCxt :: Set = data Cxt0
                       | Ext (Gamma :: ElCxt) (A :: ElTy Gamma)

  ElCm (Delta, Gamma:: ElCxt) :: Set = case Gamma of
                                       (Cxt0        )->
                                         {!!}
                                       (Ext Gamma' A)->
                                         {!!}

  ElTy (Gamma :: ElCxt) :: Set = {! !}



Anton

-- 
-----------------------------------------------------------------------------
Anton Setzer                            Telephone:
Department of Computer Science          (national)        (01792) 513368 
University of Wales Swansea             (international) +44 1792  513368
Singleton Park                          Fax:
Swansea SA2 8PP                         (national)        (01792) 295708
UK                                      (international) +44 1792  295708
                                        
Visiting address:                       Email: a.g.setzer at swan.ac.uk
Faraday Building,                       WWW:
Computer Science Dept.            http://www.cs.swan.ac.uk/~csetzer/ 
2nd floor, room 211.      ------------------------------------------------------------------------------