[Agda] Agda bug

[Sergei Meshveliani]

On Wed, 2013-11-06 at 15:14 -0200, Carlos Camarao wrote:
> I am trying to write in Agda the simplest piece of code I can for
> proving soundness and completeness of a most general unification
> function; I think this is a good, instructive example of a problem
> that
> should have a simple but non-structurally recursive solution.
> 
> In Unif.agda (all Agda files are annexed) I restricted the problem
> first to a function, mgu2, that is supposed to give the most general
> unifier of only two simple types, if it exists, together with the
> proofs that they are the least unifiers. Types are in Ty.agda and
> substitutions in Subst_list.agda.
> 
> When Unif.agda is compiled (question marks are used in places to be
> filled latter), the compiler inserts holes, starting with { }₀ (do
> this, if you want, after copying all agda files into a subdirectory). 
> When the cursor is placed inside { }₀, and Cntrl-c Cntrl-a is typed 
> (meaning 'try to automatically fill the hole yourself if you can'), 
> the compiler inserts "nothing" in the place of { }₀.
> 
> That is a bug (I think).
> 
> Furthermore, if I delete the inserted "nothing" and insert "just ?"
> the program is accepted by the compiler. The compiler replaces "?" by
> "{ }₀": 
> an inconsistency, since "nothing" was considered before the
> only possibility ("just ?" should thus not be accepted).
> 
> Trying to continue, if the "case-of" piece of code below is inserted
> (instead of a question mark):
> 
>    case mgu2 (Var v) (Con c) of λ
>      { nothing → nothing ; 
>        (just (s , _ , p₁)) → just ?
> 
> then the compiler again replaces the question mark inside the case-of
> by a hole, say { }₀ (it becomes { }₀ by loading the file, i.e. by
> typing 
> Cntrl-c Cntrl-l). By refining { }₀ (by typing Cntrl-c Cntrol-r), it
> becomes:
> 
>    case mgu2 (Var v) (Con c) of λ
>      { nothing → nothing ; 
>        (just (s , _ , p₁)) → just ({ }₀ , { }₁) 
> 
> Now, if I type Cntrl-c Cntrl-a inside the new hole { }₀,
> created by the compiler, the case-of becomes:
> 
>    case mgu2 (Var v) (Con c) of λ
>      { nothing → nothing ; 
>        (just (s , _ , p₁)) → just (proj₁ (p₁ .proj₁) , {!!}₁) 
> 
> But this code, inserted by the compiler itself, does not
> compile: typing Cntrl-c Cntrl-l gives the error message:
> 

So far, my impression is that using interactive help with holes of {?}
and such, cannot give an essential help in developing a program.

(Though, I am a newbie, I may mistake).

Instead, I proceed this way:

    ... → just v1   where
                    postulate v1 : Foo
                    
and set for  Foo  the type which I guess is needed.
If the type checker rejects this, I try to improve Foo.
After Foo is done, I remove `postulate', and start with defining  
v1 = ...
After everything is checked, I remove some declarations like  v1 : Foo
-- the ones that do not essentially help with readability.

The idea is that if I do not know where and what is the error, I split
the code into the type declaration for its parts. Then, run the checker 
by  C-c C-l,  and split each part further -- until I find which type
needs improvement.  

Regards,

-------
Sergei