An unbounded variable is not reported

[chirsz-ever]

I want to simulate the Sigma type by hand:

#lang pie

(claim my-cons (Π ((A U)
                   (B (→ A U))
                   (x A)(y (B x))
                   (E U)
                   (f (Π ((x A)) (→ (B x) E))))
                 E))
(define my-cons (λ (A B x y) (λ (E f) (f x y))))

(claim my-car (Π ((A U)
                  (B (→ A U))
                  (p (Π ((E U)(f (→ A (B x) E))) E)))
                A))
(define my-car (λ (A B p) (p A (λ (a b) a))))

(claim my-car1 (Π ((A U)
                   (B (→ A U))
                   (p (Π ((E U)(f (Π ((x A)) (→ (B x) E)))) E)))
                 A))
(define my-car1 (λ (A B p) (p A (λ (a b) a))))

On line 13 in the definition of my-car the variable x is unbounded, but the pie type checker did not report anything.

the right definition should be my-car1.

[xieyuheng]

@chirsz-ever

This is because, when expending an arrow type to a pi type,
we use x as the base symbol to generate fresh identifier:
https://github.com/the-little-typer/pie/blob/master/typechecker.rkt#L210

If you change your x to z, pie will report an error.

In the implementation of pie, one can use the following ways to avoid your problem:

• (A) using (and documenting) a more ugly naming convention,
  when expending arrow type (and pair type),
  such as __x__, which is less likely to be used by normal users
  • quick but not correct
• (B) to generate random identifier (like uuid)
  • correct but not pure
• (C) to generate identifier based on sub-expressions
  • correct and pure

[david-christiansen]

@xieyuheng You're right! I did option C in #46.