[Agda] question about instance arguments

[Peter Selinger]

Oops, I just read further in the Changelog, and I believe I found the
answer to my question:

 * Constructors of records and datatypes are automatically added to
   the instance table.

Also:

  Instance search takes into account all local bindings and all global
  'instance' bindings and the search is recursive.

This explains why "let e = eqBool in true == true" worked in my
previous example. I may have a shot of making some updates to the
reference manual. -- Peter

Peter Selinger wrote:
> 
> Hi Dominique and Andreas,
> 
> thanks for the replies. The actual behavior from Agda I experience is
> a bit erratic. Sometimes it will recognize identifiers in scope even
> without the "instance" keyword, and sometimes it won't. 
> 
> What is the syntax for using an "instance" keyword with data type
> definitions? Do you make the whole data type an instance, or just
> individual constructors? Consider the following example:
> 
> module InstanceTest where
>  
>   -- Zero is the empty set.
>   data Zero : Set where
> 
>   -- Succ A = A + 1. In other words, Succ, zero, and succ are what is
>   -- usually called Maybe, nothing, and just.
>   data Succ A : Set where
>     zero : Succ A
>     succ : A -> Succ A
> 
>   -- A subtyping relation: less-than-or-equal with respect to Succ.
>   data _<:_ : Set -> Set -> Set₁ where
>     <:-base : {A : Set} -> A <: A
>     <:-step : {A B : Set} -> {{p : A <: B}} -> A <: Succ B
> 
>   -- Cast from a smaller to a larger type.
>   cast : {A B : Set} -> {{p : A <: B}} -> A -> B
>   cast {{<:-base}} a = a
>   cast {{<:-step}} a = succ (cast a)
> 
>   test : {A : Set} -> A -> Succ (Succ (Succ A))
>   test x = cast x
> 
> The point about the subtyping relation <: is that if it exists, it is
> uniquely inhabited; however, with ordinary implicit arguments, Agda's
> type checker would not be able to infer this. With instance arguments,
> this works handsomely. Note how the subtyping was automatically
> inferred in the definition of "test".
> 
> However, I have not used any "instance" keywords here. Does this
> contradict the stated behavior of Agda 2.4.2? Also, putting an
> "instance" keyword before either "data" or "<:-base" or "<:-step"
> gives a parsing error in all cases. So is the above syntax still
> considered correct for Agda 2.4.2? If not, what is the alternative?
> 
> Thanks, -- Peter
> 
> Dominique Devriese wrote:
> > 
> > Peter,
> > 
> > Firstly, the problem you're having is a result of the changes to
> > instance argument semantics that have been made in Agda 2.4.2, which
> > are not yet reflected in the reference manual and some of the error
> > messages.  You can look at
> > 
> > https://github.com/agda/agda/blob/2.4.2.2/CHANGELOG
> > 
> > (look for "Instance search") to see what has been changed.
> > 
> > 2014-12-04 2:28 GMT+01:00 Peter Selinger <selinger at mathstat.dal.ca>:
> > > I'm trying to learn to use instance arguments, and I tried a first
> > > example, essentially taken from the reference manual:
> > >
> > > http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Modell> ingTypeClassesWithInstanceArguments
> > >
> > > Unfortunately, I cannot get it to work. Probably I am overlooking
> > > something terribly simple. I am using Agda version 2.4.2.2, freshly
> > > installed via Cabal.
> > 
> > Yes, the reference manual needs updating.
> > 
> > > Here's my file:
> > >
> > > module EqTest where
> > >
> > >   data Bool : Set where
> > >     true : Bool
> > >     false : Bool
> > >
> > >   eq : Bool -> Bool -> Bool
> > >   eq true true = true
> > >   eq false false = true
> > >   eq _ _ = false
> > >
> > >   record Eq (t : Set) : Set where
> > >     field
> > >       _==_ : t -> t -> Bool
> > >
> > >   open Eq {{...}}
> > >
> > >   eqBool : Eq Bool
> > >   eqBool = record { _==_ = eq }
> > 
> > Essentially, you need to change this to
> >    instance eqBool : Eq Bool
> >    eqBool = record { _==_ = eq }
> > 
> > >   test1 = true == true
> > 
> > > The error message I receive, in the test1 line, is:
> > >
> > > /home/selinger/projects/lang/agda/EqTest.agda:21,16-18
> > > No variable of type Eq Bool was found in scope.
> > > when checking that true true are valid arguments to a function of
> > > type {t : Set} {{r : Eq t}} → t → t → Bool
> > >
> > > This seems contradictory, since the variable eqBool is indeed in
> > > scope.
> > 
> > It would probably be a good idea to change this error message to
> > something like "... was found using the instances in scope"?
> > 
> > > If I replace the eqBool definition by a postulate, as in the
> > > reference manual,
> > >
> > >   postulate eqBool : Eq Bool
> > >
> > > I get the same error message.
> > 
> > Yes, this makes no difference.
> > 
> > > On the other hand, if I write
> > >
> > >   test1 = let e = eqBool in true == true
> > >
> > > the error disappears in both cases.
> > 
> > Ah, this surprises me, I thought you had to annotate let-bound
> > variables as well using instance under the new schem.
> > 
> > > On the other hand, this does not
> > > work:
> > >
> > >   test1 = true == true
> > >     where e = eqBool
> > 
> > This is expected under the new semantics.
> > 
> > > The reference manual says:
> > >
> > > "A candidate expression is any identifier (possibly applied to a
> > > hidden argument) in scope (either imported or defined previously in
> > > the file) or in the context (e.g. section arguments or arguments of
> > > the current function)."
> > >
> > > My example seems to contradict that. Is it a bug?
> > 
> > Yes, it is a bug in the reference manual :).  It should be updated to
> > reflect the new semantics.
> > 
> > Dominique
> > 
> 
>