invalid type ascription

Stream: maths

[Ashvni Narayanan]

import linear_algebra.finite_dimensional
import ring_theory.ideal.basic
import algebra.field
import ring_theory.subring
import ring_theory.integral_closure
import ring_theory.fractional_ideal

class number_field (K : Type*) [field K] :=
(vector_space' : vector_space ℚ K)
(is_algebra' : algebra ℚ K)
(finite_dim : finite_dimensional ℚ K)

variables (K : Type*) [field K] [number_field K]
def ring_of_integers : subring K :=  {}
instance : integral_domain (ring_of_integers : subring K) :=

gives me the error

invalid type ascription, term has type
  Π (K : Type ?) [_inst_1 : field K] [_inst_2 : number_field K], subring K : Type (?+1)
but is expected to have type
  subring K : Type u_1

I don't know how to resolve this. Any help is appreciated, thank you!

[Reid Barton]

It looks like you just need to say ring_of_integers K (and then you can drop : subring K)

[Ashvni Narayanan]

Oops, that makes sense, sorry about that. Thank you!