lack of bidirectionality in type checking

LPCIC / elpi

Embeddable Lambda Prolog Interpreter

GNU Lesser General Public License v2.1

290 stars 36 forks source link

lack of bidirectionality in type checking #250

Closed gares closed 1 week ago

gares commented 4 months ago

type p tm -> prop.
type q prop.
main :- std.do! [ p, q ].

complains that [q] has type list prop rather than list (tm -> prop), but since std.do! takes a list prop it should fail earlier, saying that p has type tm -> prop instead of the expected prop.

CC @ybertot

gares commented 1 week ago

fixed by the new backend/type checker