-- Can we define the Y combinator in pi-forall?
-- Yes! See below.
-- Note: pi-forall allows recursive definitions,
-- so this is not necessary at all.

module Fix where

-- To type check the Y combinator, we need to have a type
-- D such that D ~~ D -> D


data D (A : Type) : Type where
   F of (_ : D A -> D A)
   V of (_ : A)

unV : [A:Type] -> D A -> A
unV = \[A] v.
        case v of
          V y -> y
          F f -> TRUSTME

unF :[A:Type] -> D A -> D A -> D A
unF = \[A] v x .
   case v of
     F f -> f x
     V y -> TRUSTME

-- Here's the Y-combinator. To make it type
-- check, we need to add the appropriate conversions
-- into and out of the D type.

fix : [A:Type] -> (A -> A) -> A
fix = \ [A] g.
   let omega =
      ( \x. V (g (unV [A] (unF [A] x x)))
      : D A -> D A) in
      unV [A] (omega (F omega))

-- Example use case


data Nat : Type where
   Zero
   Succ of ( _ : Nat)

fix_add : Nat -> Nat -> Nat
fix_add = fix [Nat -> Nat -> Nat]
        \radd. \x. \y.
            case x of
              Zero   -> y
              Succ n -> Succ (radd n y)

test : fix_add 5 2 = 7
test = Refl