Stream: Elpi users & devs

Topic: cut type error


view this post on Zulip Enzo Crance (Jun 01 2021 at 13:21):

I am having trouble understanding some type errors around cuts in elpi. Whereas the following code works at the beginning of one of my predicates:

!, std.map.make cmp_term EmptyMap,
% ...

The following snippet does not typecheck.

f A B.
a X Y :-
  !, f X Y.

Here is the type error:

Error:
At least one of the following errors holds:
File "./preprocessing.elpi", line 111: (preprocessing., ! (preprocessing.f X Y)) has type (prop -> prop) but is used with type prop
File "./preprocessing.elpi", line 111: (preprocessing., ! (preprocessing.f X Y)) has type (prop -> prop) but is used with type goal-ctx

Adding true before the cut makes it typecheck. It would mean the cut needs at least one predicate before it. But this is strange considering I have been executing some working code containing cuts at the beginning of some predicates.

Does this have something to do with namespacing? Thanks.

view this post on Zulip Cyril Cohen (Jun 01 2021 at 14:21):

I'm not an elpi expert, but I could help, can you point me to the whole file?

view this post on Zulip Enzo Crance (Jun 01 2021 at 14:47):

Unfortunately not, at the moment. And my files are linked one to another, so the bug might come from somewhere else... But thanks a lot for proposing!
Anyway, it looks like it is linked to namespacing because removing the namespace solves the problem. I think I will go on with this solution for now and maybe try to minimise the bug and file an issue if it remains.


Last updated: Feb 04 2023 at 02:03 UTC