Finite Set elimination not computing fully when typechecking

[solomon-b]

def maybe→list : Maybeₚ ⇒ Listₚ :=
  λ p⁺ ⇜ p⁻ ⇝
    let n+ := { .just = 1 , .nothing = 0 } p⁺;
    return n+ ⇜ p⁻ ∘ (absurd (fib Maybeₚ p⁺))

     🭁 std-lib/Tutorial.poly
     │
 187 │     return n+ ⇜ p⁻ ∘ (absurd (fib Maybeₚ p⁺))
     │
     █ [E006] Could not solve ℕ = { .just = ℕ, .nothing = ℕ } p⁺