Stream: Elpi users & devs

Topic: unknown inductive error on match


view this post on Zulip Enzo Crance (Oct 25 2022 at 09:16):

Hello. I got Anomaly "match on unknown, non singleton, inductive" when trying to elaborate a freshly generated term. The error is likely triggered there. It's when Elpi gives the term to Coq before elaboration. The error comes from a match in Elpi, and the only one I have in my term is the following:

match c7
      (prod (X0^3 c3 c4 c5)
        (app [pglobal (indt «list») «Test.783», c3]) c8 \
        app [pglobal (indt «list») «Test.783», c4])
     [ ... ]

idk what is ill-formed in this. c3 c4 are bound types higher in the term, c7 is a term in list c3. I'm just matching a list A and building a list B essentially

view this post on Zulip Enrico Tassi (Oct 25 2022 at 09:32):

The syntax for match is tricky because Elpi must be able to know the name of the inductive type being inspected. It reads it from the return clause, which is a function taking the eliminated term (and its indexes if any) and returning a type. In you case it should be
fun l : list A => list B
but it seems you wrote
list A -> list B

view this post on Zulip Enrico Tassi (Oct 25 2022 at 09:33):

https://github.com/LPCIC/coq-elpi/blob/79176b78987c6f2129fd8c717611813b7dbea2a0/src/coq_elpi_HOAS.ml#L1788

view this post on Zulip Enrico Tassi (Oct 25 2022 at 09:34):

I guess the error message should be more precise, like "I found list A -> list B, but I was expecting a lambda"

view this post on Zulip Enzo Crance (Oct 25 2022 at 09:34):

Ok thanks, I mixed prod and fun


Last updated: Oct 13 2024 at 01:02 UTC