[Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)

[Dan Licata]

On Mar23, Ulf Norell wrote:
> Defining True to be the record type with no fields is what's going to make
> this possible. Records support eta equality, which means that any record
> element "r" is equal to the record build by projecting the fields of "r". In
> the case of True this means that any element of True is equal to any other
> element of True. In particular, if the type checker is trying to find
> something of type True there's only one choice. 

I've sometimes wished term inference would exploit a similar eta-like
rule for identity types.  I.e., if you see a goal (a == a), fill it in
with Refl {a}.  Here's a stab at a more general way of phrasing this,
which stops short of having the type checker do arbitrary logic
programming: if you have a goal whose type is an inductive family
instance that can be satisfied by exactly one constructor, all of whose
arguments are determined by the goal type, then fill it in.  Because any
term of the goal type will be eta-equivalent to what the type checker
guesses, the guess is irrelevant to the execution behavior of the
program.

Most of the time, I'm happy to just write the Refl myself.  Where this
bit of proof search would be nice is when you have an equality
constraint in the syntax of a DSEL, so writing the Refl's all over the
place clutters things up relative to the concrete syntax you have in
mind.  A minor issue, I know, but I thought I'd bring it up and see if
it's on anyone else's wish lists.

-Dan