{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {α : Type u_1} → [inst_3 : AddCommMonoid α] → [Module A α] → (S : Subalgebra R A) → Module (↥S) α