Trying to express a GADT in Scala

Nat.scala

/*

Trying to express the following GADTs in Scala. It's taken from
http://eb.host.cs.st-andrews.ac.uk/drafts/tfp08.pdf (page 5)

data Z
data S n
data Nat :: * -> * where
  Zero :: Nat Z
  Succ :: Nat n -> Nat (S n)

class Plus m n s | m n -> s where
  plus :: Nat m -> Nat n -> Nat s

instance Plus Z b b where
  plus Zero y = y

instance Plus a b c => Plus (S a) b (S c) where
  plus (Succ x) y = Succ (plus x y)

*/

object Nat {
  
  sealed trait Nat
  trait Zero extends Nat
  case class Succ[A <: Nat](x: A) extends Nat

  trait Plus[X <: Nat, Y <: Nat, S <: Nat] {
    def plus(x: X, y: Y): S
  }

  implicit def plusZero[S <: Nat] = new Plus[Zero, S, S] {
    override def plus(zero: Zero, y: S): S = y
  }

  // This is the one I can't get to compile.
  implicit def plusSucc[A <: Nat, B <: Nat, C <: Nat] = new Plus[Succ[A], B, Succ[C]] {
    override def plus(x: Succ[A], y: B): Succ[C] = (x,y) match {
      case (Succ(q), _) =>  Succ(plus(q,y))
    }
  }
 
  /*
    [error] /Users/hartmann/Desktop/dependent types talk/code/./src/main/Nat.scala:39: type mismatch;
    [error]  found   : A
    [error]  required: Nat.Succ[A]
    [error]  Note: implicit method plusSucc is not applicable here because it comes after the application point and it lacks an explicit result type
    [error]       case (Succ(q), _) =>  Succ(plus(q,y))
    [error]                                       ^
  */
 
}

Miles has already implemented this in a much nicer way here: https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/ops/nat.scala#L41