[Agda] invert pattern matching

[Martin Escardo]

Thanks for explanation, Ulf. I understand what the error message means 
now. I had never got this error message before, and today I got it for 
the first time and then many times following this (when trying to give a 
term in a hole). Martin

On 14/12/2018 20:39, ulf.norell at gmail.com wrote:
> 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 
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe