Weird error caused by instance

Stream: mathlib4

[Michail Karatarakis]

Hi, I ported a file to Lean4 and noticed the following. Although I work around this, adding instance : NormedField (AlgebraicClosure ℚ_[p]) causes an error (which also happens in Lean3). How do I find out what's going on?

Here's an mwe :

import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.NumberTheory.Padics.PadicNumbers

open Polynomial

variable {K : Type} [Field K] (p : ℕ) [Fact (Nat.Prime p)] (x y : (AlgebraicClosure ℚ_[p])[X])

instance : NormedField (AlgebraicClosure ℚ_[p]) := sorry

variable {K : Type} [Field K] (p : ℕ) [Fact (Nat.Prime p)] (x y : (AlgebraicClosure ℚ_[p])[X])

#check x - y -- Fails after the instance above is added.

[Kevin Buzzard]

Hi Michail! Nothing is failing for me in your code. However I suspect the instance is a bad one anyway, because NormedField extends Field so in particular you'll now have two field structures on the alg closure (one of them sorry and one of them the correct one)