bug when duplicate arg names present

[pnwamk]

This definition of pair is accepted when it should error (i.e. in terms of the Π's identifiers, we are supposed to provide a function which returns a (Pair A D), we instead return a (Pair D D) and pie doesn't complain):

#lang pie
(claim pair (Π ([A U]
                [D U])
              (-> A D (Pair A D))))
(define pair
  (λ (_ _ a d)
    (cons d d)))

This seems to be an incorrect handling of shadowing while type checking a λ. Here is a equivalent definition of pair that may help illustrate:

(define pair (λ (X)
               (λ (X)
                 (λ (a)
                   (λ (d)
                     (cons d d))))))

With this definition accepted, usages of pair lead to internal errors, e.g.:

(pair Nat Atom 42 'batman)

produces the error:

...pkgs/pie/normalize.rkt:458:2: match*: no matching clause for (list 'NAT (QUOTE 'batman))

But perhaps this latter error is just an artifact of things already being cattywampus and it isn't a "separate issue".

[david-christiansen]

I see why this is happening. I don't have time to fix it this morning, but I think I can do it this evening.

Thanks for catching it!

[david-christiansen]

OK, fixed. Thanks!