Commit 2020-04-19 07:58 11d89a2f
View on Github →chore(algebra/module): replace typeclass arguments with inferred arguments (#2444)
This doesn't change the explicit type signature of any functions, but makes some inferable typeclass arguments implicit.
Beyond the potential performance improvement, my motivation for doing this was that in monoid_algebra
we currently have two possible module k (monoid_algebra k G)
instances: one directly from monoid_algebra.module
, and another one via restrict_scalars
. These are equal, but not definitionally. In another experimental branch, I couldn't even express the isomorphism between these module structures, because type inference was filling in the monoid_algebra.module
instance in composition of linear maps, and then failing because one of the linear maps was actually using the other module structure...
This change fixes this.