[Agda] question about instance arguments

[Peter Selinger]

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=3DReferenceManual.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 =3D true
> >   eq false false =3D true
> >   eq _ _ =3D false
> >
> >   record Eq (t : Set) : Set where
> >     field
> >       _=3D=3D_ : t -> t -> Bool
> >
> >   open Eq {{...}}
> >
> >   eqBool : Eq Bool
> >   eqBool =3D record { _=3D=3D_ =3D eq }
> 
> Essentially, you need to change this to
>    instance eqBool : Eq Bool
>    eqBool =3D record { _=3D=3D_ =3D eq }
> 
> >   test1 =3D true =3D=3D 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}} =E2=86=92 t =E2=86=92 t =E2=86=92 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 =3D let e =3D eqBool in true =3D=3D 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 =3D true =3D=3D true
> >     where e =3D 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
>