Dotty: Inline givens can't specialize, inline implicit defs can

[milessabin]

I've just run across the following limitation of inline given instances as compared with inline implicit defs ...

shapeless's Annotations type class is of the form,

trait Annotations[A, T] {
  type Out <: Tuple
  def apply(): Out
}

Given an annotation Annot and a case class CC,

case class Annot() extends scala.annotation.Annotation
case class C(i: Int, @Annot s: String)

the instances Annotations[Annot, CC] is a term of the form,

new Annotations[Annot, CC] {
  type Out = (None.type, Some[Annot])
  def apply(): Out = (None, Some(Annot()))
}

This term is materialized via a Dotty macro.

Ideally we would like to be able to provide the instance as a given,

inline given mkAnnotations[A, T] as Annotations[A, T] =
  ${ AnnotationMacros.mkAnnotations[A, T] }

However, this doesn't work because the the result type of the given, Annotations[A, T], omits the refinement { type Out = ... }. We can't provide the refinement explicitly because it's computed by the macro expansion on the RHS.

We _can_ provide the instance as an inline implicit def, however, using specializing inline,

inline implicit def mkAnnotations[A, T] <: Annotations[A, T] =
  ${ AnnotationMacros.mkAnnotations[A, T] }

Here the result type is refined to be as precise as the expansion on the RHS. The reason we can't do this in the given case is because we have no way to indicate that we want the refined type rather than the explicitly annotated type.

This is going to be an issue for any type class which computes both a type and a term as is done by shapeless.Annotations.

At least while we continue to have implicit defs and specializing inline we have a mechanism to do what needs to be done here, but it would be nice to be able to express this using givens, if only for syntactic consistency.

[LPTK]

IMHO this is another good reason to drop the idiosyncratic as and just use extends for new instances and :/<: for aliases, which have the advantage of making the semantics of given declarations clearer:

given IntSemigroup extends Semigroup[Int] { ... }

// anonymous:
given _ extends Semigroup[Int] { ... }
// alternatively:
given Semigroup[Int] { ... }

given theContext: ExecutionContext = ...

// anonymous:
given _: ExecutionContext = ...

inline given mkAnnotations[A, T] <: Annotations[A, T] =
  ${ AnnotationMacros.mkAnnotations[A, T] }

[milessabin]

Another slightly less drastic change would be to use : and <: in place of as. We could even keep as as an alternative to :.

[milessabin]

After sleeping on this for a few days, I've come to the conclusion that this is another piece of evidence in favour of _permanently_ preserving normal val and def-like syntax for givens (nb. I still support the use of given to replace implicit and I'm still prepared to live with the given construct for params/arguments).

Having spent some time working with the new syntax now, It's pretty clear to me that we need to be able to express every one of the existing val and def forms of definition for givens. That means that we need to be able to express all of the distinctions syntactically. And if we're going to do that it surely makes sense to simply use the existing syntax rather than try and invent something which is both new _and_ equivalent.

Also nb. that I'm _not_ objecting to the concise syntax for introducing type class instances. But I think that should be thought of as a syntactic addition to the val and def forms rather than as replacement.

Concretely, I think we need to support given def given val and given lazy val forms. I think we should also only apply any caching logic to instances defined using the new given ... as form.