RFC: new versus old code generator issue

Since nightly-2025-06-21 the file CoreM.lean changed line 670 to defValue := true.

The new code generator does not want to generate code any more for the some of my code.

I am referring to https://github.com/LucDuponcheelAtGitHub/PSBP

Agreed, I am using the unsafe keyword because the type system cannot infer termination.

The mwe code below contains sequentialFibonacci and parallelFibonacci.
Both are written in terms of declarations. Their materializations
(according to implementations that define the declarations) come later.

sequentialFibonacci is not impacted, but parallelFibonacci is impacted.

Therefore I guess that the difference is, somehow, related to Task.

Here are some possibilities to solve this

1. have two releases : one with the old code generator one with the new code generator
   (this does not look to me like the right way to proceed)
2. somehow provide a compiler/interpreter option to choose between the old one and the new one
   (also sub-optimal, but workable for me)
3. look into the issue and find out where and why the new one does not want to generate code

All comments are welcome

class Functional
    (program : Type → Type → Type) where
  asProgram {α β : Type} :
    (α → β) → program α β

export Functional (asProgram)

class Functorial
    (program : Type → Type → Type) where
  andThenF {α β γ : Type} :
    program α β → (β → γ) → program α γ

export Functorial (andThenF)

infixl:50 " >-> " => andThenF

class Sequential
    (program : Type → Type → Type) where
  andThenP {α β γ : Type} :
    program α β → program β γ → program α γ

export Sequential (andThenP)

infixl:50 " >=> " => andThenP

class Creational
    (program : Type → Type → Type) where
  sequentialProduct {α β γ : Type} :
    program α β → program α γ → program α (β × γ)

export Creational (sequentialProduct)

infixl:60 " &&& " => sequentialProduct

class Conditional
    (program : Type → Type → Type) where
  sum {α β γ : Type} :
    program γ α → program β α → program (γ ⊕ β) α

export Conditional (sum)

infixl:55 " ||| " => sum

class Parallel (program : Type → Type → Type) where
  parallel {α β γ δ : Type} :
  program α γ → program β δ → program (α × β) (γ × δ)

export Parallel (parallel)

infixl:60 " |&| " => parallel

def identity
    [Functional program] :
  program α α :=
    asProgram λ α => α

def let_
    [Functional program]
    [Sequential program]
    [Creational program] :
  program α β → program (α × β) γ → program α γ :=
    λ αpβ αaβpγ => identity &&& αpβ >=> αaβpγ

 def if_
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program] :
  program α Bool →
  program α β →
  program α β →
  program α β :=
    λ αpb t_apβ f_apβ =>
      let_ αpb $
        asProgram (
          λ αab => match αab with
            | ⟨α, true⟩ => .inl α
            | ⟨α, false⟩ => .inr α
        ) >=>
        t_apβ ||| f_apβ

def dup
    [Functional program] :
  program α (α × α) :=
    asProgram λ α => (α, α)

def parallelProduct {α β γ : Type}
    [Functional program]
    [Sequential program]
    [Parallel program] :
  program α β → program α γ → program α (β × γ) :=
   λ αpβ αpγ => dup >=> αpβ |&| αpγ

infixl:60 " &|& " => parallelProduct

def isZeroF: Nat → Bool := (. == 0)

def isOneF : Nat → Bool := (. == 1)

def oneF : Nat → Nat := λ _ => 1

def minusOneF : Nat → Nat := λ n => n - 1

def minusTwoF : Nat → Nat := λ n => n - 2

def addF : Nat × Nat → Nat :=
  λ ⟨n, m⟩ => n + m

def multiplyF : Nat × Nat → Nat := λ ⟨n, m⟩ => n * m

def isZero
    [Functional program] :
  program Nat Bool :=
    asProgram isZeroF

def isOne
    [Functional program] :
  program Nat Bool :=
    asProgram isOneF

def one
    [Functional program] :
  program Nat Nat :=
    asProgram oneF

def minusOne
    [Functional program] :
  program Nat Nat :=
    asProgram minusOneF

def minusTwo
    [Functional program] :
  program Nat Nat :=
    asProgram minusTwoF

def add
    [Functional program] :
  program (Nat × Nat) Nat :=
    asProgram addF

unsafe def sequentialFibonacci
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program] :
  program Nat Nat :=
    if_ isZero one $
      if_ isOne one $
        (minusOne >=> sequentialFibonacci) &&&
        (minusTwo >=> sequentialFibonacci) >=>
        add

unsafe def parallelFibonacci
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program]
    [Parallel program] :
  program Nat Nat :=
    if_ isZero one $
      if_ isOne one $
        (minusOne >=> parallelFibonacci) &|&
        (minusTwo >=> parallelFibonacci) >=>
        add

structure FromComputationValuedFunction
    (computation : (Type → Type)) (α β : Type) where
  toComputationValuedFunction : α → computation β

instance [Applicative computation] :
    Functional
      (FromComputationValuedFunction computation) where
  asProgram :=
    λ αfβ => ⟨λ α => pure $ αfβ α⟩

instance [Functor computation] :
    Functorial
      (FromComputationValuedFunction computation) where
  andThenF :=
    λ ⟨αfcβ⟩ βfγ => ⟨λ α => βfγ <$> αfcβ α⟩

instance [Applicative computation] :
    Creational
      (FromComputationValuedFunction computation) where
  sequentialProduct :=
    λ ⟨αfcβ⟩ ⟨αfcγ⟩ =>
      ⟨λ α => .mk <$> αfcβ α <*> αfcγ α⟩

instance [Monad computation] :
    Sequential
      (FromComputationValuedFunction computation) where
  andThenP :=
    λ ⟨αfcβ⟩ ⟨βfcγ⟩ =>
      ⟨λ α => αfcβ α >>= βfcγ⟩

def foldSum {γ β α : Type}
    (γfα : γ → α)
    (βfα : β → α)
    (sum : γ ⊕ β) : α :=
  match sum with
  | .inl tc => γfα tc
  | .inr tb => βfα tb

instance :
    Conditional
      (FromComputationValuedFunction computation) where
  sum :=
    λ ⟨γfγα⟩ ⟨βfγα⟩ =>
      ⟨foldSum γfγα βfγα⟩

class MonadAsync
    (computation : Type → Type) where
  async {α : Type} (ufα : Unit → α) : computation α
  result {α : Type} (cα : computation α) : α

export MonadAsync (async result)

abbrev Sync := Id

abbrev SyncProgram := FromComputationValuedFunction Sync

def materializeSync : SyncProgram α β → (α → β) :=
  λ ⟨αfaβ⟩ α => αfaβ α

abbrev Async := Task

instance : Monad Async where
  pure := Task.pure
  bind := Task.bind

instance : MonadAsync Async where
  async := Task.spawn
  result := λ tα => tα.get

abbrev AsyncProgram :=
  FromComputationValuedFunction Async

def materializeAsync {α β : Type} :
  AsyncProgram α β → (α → β) :=
    λ ⟨αftβ⟩ α => (αftβ α).get

def combine
    {γ δ : Type}
    [Applicative computation] :
  computation γ → computation δ → computation (γ × δ) :=
    λ cγ cδ => Prod.mk <$> cγ <*> cδ

infixl:50 " <×> " => combine

instance
    [Monad computation]
    [MonadAsync computation] :
  Parallel (FromComputationValuedFunction computation) where
    parallel := λ ⟨αfcγ⟩ ⟨βfcδ⟩ =>
      ⟨λ ⟨α, β⟩ =>
        async (λ (_: Unit) => αfcγ α) >>=
          λ cγ =>
            async (λ (_: Unit) => βfcδ β) >>=
              λ cδ =>
                cγ <×> cδ⟩

unsafe def syncFibonacci :=
  materializeSync sequentialFibonacci

unsafe def asyncFibonacci :=
  materializeAsync parallelFibonacci

#eval syncFibonacci 10

-- #eval asyncFibonacci 10