Annoying typechecker error on polymorphic symbol `:-`

[FissoreD]

In the following code I obtain a typechecking error:

pred q.

pred p i:list prop, o:prop.
p P (q :- Body) :-
  std.rev P Body.

From what I understand, the typechecker sees q :- Body and infers that
Body has type prop. However, the operator :- also accepts a list of
prop on its right-hand side, which is the expected type of Body in
this example.

It seems that the typechecker only considers the prop case and does not
account for the possibility that the right-hand side may be list prop.

I have not tested it, but I suspect that a similar error occurs for the
operators => and =!=>.

[FissoreD]

I think the problem comes from here?