Cedille Core Elaboration Bug with Phi

[amarmaduke]

The elaborated output of the following code:

data Unit : ★ =
  | unit : Unit.

bug : Unit ➔ Unit
= λ u. μ rec. u {
  | unit ➔ u
  }.

Will elaborate Phi casts without required parenthesis.
Here is a (relatively) small snippet of the problem:

(φ (β <y> {|λ x . x|}) - IndF-Unit ·Type-rec1 y {| y |})
            ·(λ y1 : F-Unit ·Type-rec1 .
                ∀ y' : Unit .
                 ∀ e : { Unit-inFix y1 ≃ y' } .
                  (λ _ : Unit . Unit)
                    (φ e -
                       Unit-inFix
                         ·F-Unit
                         -fmap-Unit
                         (Unit-cast
                            ·(F-Unit ·Type-rec1)
                            ·(F-Unit ·Unit)
                            -(fmap-Unit ·Type-rec1 ·Unit -to)
                            y1)
                       {| y' |}))

If you check this with Cedille Core itself then it works, but if you attempt to check it with Cedille Proper it will complain about the first line, specifically ·Type-rec1.

[cwjnkins]

Looks like the change to require the second subterm of phi to be a Pterm goes back to 3e9579f