[Agda] Again, a question on records

[Dan Doel]

On Sunday 19 September 2010 9:24:58 pm David Leduc wrote:
> Sorry, my previous question was stupid. Here it is again, hopefully
> not so stupid:
> 
> In the code below, from the type of x and y (T.carrier t), shouldn't
> the type checker infer the implicit argument marked as an underscore?
> Even if I put explicitly t instead of the underscore, my definition is
> rejected. What is going on? What is the right way to do in Agda?
> 
> module test where
> 
> record T : Set1 where
>   field carrier : Set
>         op : carrier -> carrier -> carrier
> 
> [_] : T -> Set
> [ t ] = T.carrier t
> 
> _$_ : {t : T} -> T.carrier t -> T.carrier t -> T.carrier t
> x $ y = T.op _ x y

While it's obvious to you and us that you mean for t to be filled in there, 
it's not obvious to the type checker, and it isn't the only legal thing that 
could go in there. There are infinitely many things that could go there, in 
fact:

  _$_ {t} = T.op (record { carrier = T.carrier t
                         ; op = \x y -> T.op t x (T.op t x y) })
  -- etc.

All those records have the same carrier as the record passed in, so the result 
will type check properly. And even if there weren't infinitely many examples 
that could be constructed locally, I wouldn't expect it to fill in t (nothing 
really *determines* that t is the only valid thing to fill in there).

Anyhow, you can manually write what you want via:

  _$_ {t} = T.op t

or, if you're feeling fancy, you could write:

  open module T' {t} = T t hiding (carrier) renaming (op to _$_)

-- Dan