Question about the typing of rewrite rules

[francoisthire]

In the following example, only the first rewrite is well-typed by Dedukti (and lambdapi) but not the second.

A : Type.

a : A.

def T : A -> Type.

[] T a --> A -> A.

True : Type.

def eq : A -> A -> Type.
[x] eq x x --> True.
true : True.
def f : x : A -> y : A -> eq x y -> T x ->  A.

(; OK ;)
[] f a _ true (x => x) --> a.

(; Not OK ;)
[] f _ a true (x => x) --> a.

However, the typing forces that the joker is convertible to a, hence the rewrite rule should be well-typed. In that simple example, writing the first or the second rule does not matter. But is it possible to have an example where it does? Also, is this behavior the one expected?

[fblanqui]

Even without checking what is the structure of the LHS, one immediatly sees that, if it is typable, then it is of type A, and the RHS is of typa A too, whatever the LHS is. So, this rule should be accepted, whatever the structure of the LHS is. Perhaps the problem comes from the fact that the 4th argument is of type T x where x is the first argument and fails here because the 1st argument is _. Le 16/04/2018 à 16:21, fthire a écrit :

…

In the following example, only the first rewrite is well-typed by Dedukti (and lambdapi) but not the second. |A : Type. a : A. def T : A -> Type. [] T a --> A -> A. True : Type. def eq : A -> A -> Type. [x] eq x x --> True. true : True. def f : x : A -> y : A -> eq x y -> T x -> A. (; OK ;) [] f a _ true (x => x) --> a. (; Not OK ;) [] f _ a true (x => x) --> a. | However, the typing forces that the joker is convertible to |a|, hence the rewrite rule should be well-typed. In that simple example, writing the first or the second rule does not matter. But is it possible to have an example where it does? Also, is this behavior the one expected? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#72>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AKWYmYaWvSRISLKjWqCjiXFRSvI0Duzfks5tpKjdgaJpZM4TWnwS>.

[francoisthire]

@Gaspi should we do something? Or we leave it as it is now since it is fixed in lambdapi?