Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]

[James Deikun]

On Mon, 2012-04-23 at 16:34 +0200, Nils Anders Danielsson wrote:
> On 2012-04-23 15:37, James Deikun wrote:
> > The current stdlib implementation is clever, but thanks to depending
> > on optimizations Agda still doesn't implement, it can take about 25
> > seconds to reduce the product of two rationals (involving no more than
> > 2-digit arithmetic).
> 
> I think you refer to the following comment:
> 
>    -- Note that Induction.Nat.<-rec is used to establish termination of
>    -- division. The run-time complexity of this implementation of integer
>    -- division should be linear in the size of the dividend, assuming
>    -- that well-founded recursion and the equality type are optimised
>    -- properly (see "Inductive Families Need Not Store Their Indices"
>    -- (Brady, McBride, McKinna, TYPES 2003)).
> 
> Note that at least one of these optimisations (collapsing) is a
> /run-time/ optimisation.

I knew full collapsing was only available at runtime, but I wasn't aware
that division was depending on it for its time bound; that certainly
strengthens my point.

The typechecking-time optimizations from that paper could already make
asymptotic improvements on a lot of uses of Fin and the comparator
types, as well as Vecs and so forth; are there known bad interactions
with things like metavariable inference that exclude them, or does it
seem more like the proverbial Small Matter of Programming?