[Agda] instance argument problems

[Andreas Abel]

Hi Andy,

I complained about this a while ago:

   https://code.google.com/p/agda/issues/detail?id=1273

Cheers,
Andreas

On 30.05.2015 16:50, Andrew Pitts wrote:
> {-
> I'm struggling to get instance arguments are they provided by the
> latest versions of Agda (> v2.4.2) to work how I would like. For
> example, taking the "simulate Haskell type class" example from the
> documentation
> -}
> data Bool : Set where
>    true : Bool
>    false : Bool
>
> record Eq (t : Set) : Set where
>     field _==_ : t → t → Bool
>
> open Eq {{...}}
>
> -- Now package this into a record type for "sets with boolean equality":
> record EqSet : Set₁ where
>    field
>      set : Set
>      eq  : Eq set
>
> open EqSet
>
> {-
> I'd hope that every time I had identifiers (A : EqSet)(x y set A) in
> scope, I could use the expression x == y and have Agda figure out that
> this was the eq A instance of _==_. However eq A is not a "candidate
> expression" according to
> <http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.InstanceArguments>.
> For
> example
>
> bad-equality : (A : EqSet)(x y : set A) → Bool
> bad-equality A x y =  x == y
>
> fails to check, with the message
>
> No variable of type Eq (set A) was found in scope.
> when checking that x y are valid arguments to a function of type
> {t : Set} {{r : Eq t}} → t → t → Bool
>
> One can get round this by binding eq A to a variable, for example...
> -}
>
> good-equality : (A : EqSet)(x y : set A) → Bool
> good-equality A x y = let _ = eq A in x == y
>
> {-
> ...but that seems inelegant. Is there some way of redefining the
> record type EqSet so that when we have a value A of type EqSet we
> automatically get access to the eq A instance of _==_ ?
>
> Andy
> -}
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/