neither computable nor noncomputable

[kim-em]

(Unfortunately I haven't minimised this to the point we can avoid mathlib.)

import set_theory.ordinal

inductive G : Type 1
| mk : ∀ α : Type, (α → G) → G

noncomputable def N : ordinal → G
| O₁ := ⟨ O₁.out.α,
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁ := sorry,
    N (ordinal.typein O₁.out.r O₂) ⟩
using_well_founded {dec_tac := tactic.assumption}

gives a warning definition 'N' was incorrectly marked as noncomputable, while

import set_theory.ordinal

inductive G : Type 1
| mk : ∀ α : Type, (α → G) → G

def N : ordinal → G
| O₁ := ⟨ O₁.out.α,
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁ := sorry,
    N (ordinal.typein O₁.out.r O₂) ⟩
using_well_founded {dec_tac := tactic.assumption}

gives an error rec_fn_macro only allowed in meta definitions

Zulip thread

[digama0]

Minimized:

def foo := Type
instance : has_lt foo := sorry
instance : has_well_founded foo := ⟨(<), sorry⟩

axiom A : foo → foo
axiom B : ∀ o, A o < o

def N : foo → empty -- rec_fn_macro only allowed in meta definitions
| o := have _ := B o, N (A o)
using_well_founded {dec_tac := tactic.assumption}

Here you will get an error rec_fn_macro only allowed in meta definitions regardless of what foo is, but if foo is a computationally relevant type like nat instead of Type then the noncomputable version gives no errors. This version gives the "incorrectly marked as noncomputable" error if you try to mark N as noncomputable.

[digama0]

Another MWE of the error:

noncomputable theory

constant A : Type
inductive B : Type
| mk : A → B → B

def foo : B → B -- rec_fn_macro only allowed in meta definitions
| (B.mk a b) := B.mk a (foo b)

It compiles if you use noncomputable theory and noncomputable def foo.

[kmill]

If I understand it correctly, if a function is tagged noncomputable then the equation compiler will change how it compiles recursive definitions https://github.com/leanprover-community/lean/blob/master/src/library/equations_compiler/compiler.cpp#L351

All noncomputable theory seems to do is turn off the check that you only put noncomputable exactly when the noncomputability checker agrees it should be there.

Maybe this might point toward an explanation?