Odd `failed to compile definition` error

Stream: lean4

[Geoffrey Irving]

I'm not sure what's going on here:

import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real  -- Removing this import fixes things

class Approx (A : Type) (R : outParam Type) where

class ApproxAddGroup (A : Type) (R : outParam Type) [AddGroup R] extends
  Neg A, Approx A R where

structure Box where

instance : Approx Box ℂ where
instance : Neg Box where neg x := sorry

/-- Bails with `consider marking it as noncomputable` if we do the `...Pow.Real` import -/
instance : ApproxAddGroup Box ℂ where

What's noncomputable about ApproxAddGroup, given that it declares no code? It also seems odd that removing the Mathlib.Analysis.SpecialFunctions.Pow.Real import fixes things.

[Geoffrey Irving]

This isn't blocking me because I can in fact just mark the instances noncomputable, but it was surprising.

[Alex J. Best]

Yeah I agree this is surprising / annoying, but it does make sense, docs#Complex.instNormedAddCommGroupComplex is noncomputable and that is on the instance path that is used to infer [AddGroup Complex] as long as Mathlib.Analysis.Complex.Basic is imported (transitively). So even though the structure is projected to a bunch of things that are computable the viral noncomputable marker tricks lean. Maybe we need a computable! keyword or something for such cases. docs#Complex.Complex.addGroupWithOne is what is used without the import

[Geoffrey Irving]

Ah, that makes sense.