`Nothing` does not conform to arbitrary type parameter

[scabug]

trait Stuff[A]
def take[A](st: Stuff[A]): Stuff[A] = st

take(??? : Stuff[Nothing])

Result:

<console>:13: error: type mismatch;
 found   : Stuff[Nothing]
 required: Stuff[A]
Note: Nothing <: A, but trait Stuff is invariant in type A.
You may wish to define A as +A instead. (SLS 4.5)
       take(??? : Stuff[Nothing])
                ^

The error goes away if either:

• type parameter is explicit (i.e. take[Nothing](??? : Stuff[Nothing]))
• A is covariant
• A occurs in covariant position in return type of take or does not occur at all

Original SO question: http://stackoverflow.com/questions/32097291/bizzare-type-inference-limitation-multiple-type-params

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-9453?orig=1
Reporter: @ghik
Affected Versions: 2.11.7

[scabug]

@retronym said:
This is a known limitation with type inference: you have to specify the type argument of Nothing explicitly in this case, as the typer retracts the solutions to the local type inference problem that instantiated type variables to Nothing. I'll leave this bug open as I'm not sure if another one directly touches on this problem, but I don't think we'll be able to make this example work without major surgery to inference.

[scabug]

@milessabin said (edited on Sep 1, 2015 3:02:26 PM UTC):
As an aside, it's possible to synthesize a type equivalent to Nothing which won't cause the typer to retract the solution,

type ReallyNothing = Nothing { type T = Unit }

ie. Nothing with a dummy refinement. Repl session ...

scala> :paste
// Entering paste mode (ctrl-D to finish)

trait Stuff[A]
def take[A](st: Stuff[A]): Stuff[A] = st
 
take(??? : Stuff[ReallyNothing])

// Exiting paste mode, now interpreting.

scala.NotImplementedError: an implementation is missing
  at scala.Predef$.$qmark$qmark$qmark(Predef.scala:225)
  ... 37 elided

[scabug]

@pchiusano said (edited on Oct 13, 2015 8:26:37 PM UTC):
I have hit this issue also, though my situation is a bit different so I thought I'd add a bit more.

I have a trait Stream[+F[_],+O], where a Stream[Nothing,A] represents a pure stream which uses no effects, and a Stream[F,A] may request evaluation of F[_] effects in between emitting values to the output. The advantage of using Nothing to represent pure streams is that normal subtyping will promote that to whatever F[_] the context requires, no need for explicit lifting.

The problem is when calling a function like this one:

def pull[F[_],A,B](s: Stream[F,A])(using: Handle[F,A] => Pull[F,B,Any]): Stream[F,B]

in conjunction with a polymorphic function like

def take[F[_],I]: Handle[F,I] => Pull[F,I,Handle[F,I]]

The issue is that Scala won't infer Nothing for the argument to take or the pull type parameter, which leads to needing to write:

val purePull = Stream.pull[Nothing,Int,Int](Stream(1,2,3,4))(process1.take[Nothing,Int](2))

Both those annotations are needed. Not very good. :(

What stops me from directly using the dummy refinement trick Miles mentions above is that I am relying on the fact that Nothing is polykinded, but for any type alias one must pick a single kind for it.

[joroKr21]

This bug is on the second to last page 😄 #1570