[Agda] invert pattern matching

[Ulf Norell]

For functions with distinct rigid right-hand sides Agda can invert the
function when solving constraints.
For instance, given

F : Bool → Set
F false = Nat
F true  = Bool

Agda can solve α := false when faced with a constraint F α == Nat. This is
not guaranteed
to terminate however, so there's a maximum number of times a meta variable
can be solved
by inversion before we give up.

Here's a simple way to trigger the cutoff:

f : Nat → Nat
f zero    = zero
f (suc n) = suc (suc (f n))

test : let X = _ in f X ≡ suc (f X)
test = refl

/ Ulf


On Fri, Dec 14, 2018 at 8:41 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> What does Agda mean when it says
>
> "
> Refusing to invert pattern matching of transport because the
> maximum depth (50) has been reached. Most likely this means you
> have an unsatisfiable constraint, but it could also mean that you
> need to increase the maximum depth using the flag
> --inversion-max-depth=N
> "
>
> What does it mean to "invert pattern matching of transport"?
>
> (I like this error message.)
>
> Thanks,
> Martin
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181214/b2fc4ef4/attachment.html>