error defining vs directly using a Pi type

[pnwamk]

I understand that Pie has a trivial universe heirarchy... but I was surprised that simply whether or not I used a variable vs the expression that variable was defined to be affected whether or not Pie accepted the program.

i.e. in the code at the bottom of this issue, this snippet works without issue:

(claim dblneg->pem-works
  (-> (Π ([P U])
        (-> (Not (Not P)) P))
    (Π ([P U])
      (Either P (Not P)))))

but this snippet does not:

(claim dblneg->pem-works
  (-> (Π ([P U])
        (-> (Not (Not P)) P))
    (Π ([P U])
      (Either P (Not P)))))

even though the two are the same (modulo defines/names).

Here's the full example:

#lang pie

(claim Not (-> U U))
(define Not
  (λ (P) (-> P Absurd)))

(claim dblneg
  (Π ([P U])
    (-> (Not (Not P)) P)))
(define dblneg TODO)

(claim pem
  (Π ([P U])
    (Either P (Not P))))
(define pem TODO)

; this should work, right?
(claim dblneg->pem-broken
  (-> dblneg pem))
; currently it just errors with the following message:
; Expected U but given
;   (Π ((P U))
;    (→ (→ (→ P
;              Absurd)
;          Absurd)
;      P))

(claim dblneg->pem-works
  (-> (Π ([P U])
        (-> (Not (Not P)) P))
    (Π ([P U])
      (Either P (Not P)))))

[david-christiansen]

It looks to me like both of your snippets are identical at the top of the issue. Was that a mistake?

Later on, when checking the judgment

`(-> dblneg pem)` is a type

Pie will first check that dblneg is a type. dblneg is not a type constructor, so it has a fallback: check that it's a U. But dblneg is not a U, it is a (Pi ((P U)) (-> (Not (Not P)) U)). So the check fails.

It looks to me like you're expecting a defined variable's value to be its type, but in Pie, the value is the definition. dblneg's value is TODO, not (Pi ((P U)) (-> (Not (Not P)) U)).

Make sense?

[pnwamk]

Yes -- now it seems obvious. Thanks for the clear explanation ;-)