Closed eparejatobes closed 7 years ago
There's some casting here due to higher-kinded type members being not checked correctly in refinements. For example, for the Identity functor below:
final
class Identity[Cat <: Category](val cat: Category.is[Cat]) extends Functor {
type Source = Cat
val source = cat
type Target = Cat
val target = cat
type F[Z <: Source#Objects] = Z
def at[X <: Source#Objects, Y <: Source#Objects]: Source#C[X,Y] -> Target#C[F[X], F[Y]] =
Scala.identity
}
We should have that Identity[Cat] <: Functor.is[Identity[Cat]]
, as everything is bound at this point; we don't:
// full snippet
type is[functor <: Functor] =
functor {
type Source = functor#Source
type Target = functor#Target
type F[Z <: Source#Objects] = functor#F[Z]
}
type weakIs[F0 <: Functor] =
F0 {
type Source = F0#Source
type Target = F0#Target
}
import scala.Predef.<:<
// compiles
def z[Cat <: Category] =
scala.Predef.implicitly[Identity[Cat] <:< weakIs[Identity[Cat]]]
// nonono
// def z0[Cat <: Category] =
// scala.Predef.implicitly[Identity[Cat] <:< is[Identity[Cat]]]
Looking good, will review later and merge.
@agarciamontoro I'm requesting a review from you just to be sure that you understand this.
Tomorrow I'll try to reduce the number of X.is[_] here.
Done. LGTM.
(monoid in an endofunctor category, if possible)