Generalized ADTs are an idle thought which might be a bad idea, so no issue has been created to track it.

What is GADT? In a nutshell, they're like ADTs but more flexible (they generalize ADTs). A GADT is an ADT that allows the constructor cases to be typed. The canonical example of their use is in making an Abstract Syntax Tree enforce type constraints. For example, lets say we had this simple language

Expression = 
    IntLiteral(int value)
  | BooleanLiteral(boolean value)
  | Add(Expression l, Expression r)
  | If(Expression condition, Expression trueCase, Expression falseCase)

Where "if" is an expression as in Scala/ML/Haskell (think ternary operator in Java). That's fine, but the AST allows us to construct expressions that add two booleans or do an if on an int. The normal solution is to do a type check pass over the AST and report errors. But it's also possible to statically prevent it. Here's some hypothetical JADT syntax that would cover it

Expression<A> =
     IntLiteral(int value) extends Expression<IntType>
   | BooleanLiteral(boolean value) extends Expression<BooleanType>
   | Add(Expression<IntType> l, Expression<IntType> r> extends Expression<IntType>
   | If<A>(Expression<Boolean> condition, Expression<A> trueCase, Expression<A> falseCase) extends Expression<A>

Syntax is of course not fixed. But hopefully that expresses the idea. Each constructor case specifies what type of Expression it creates and as in the If example the constructor can take type parameters. In fact, I don't show it, but a constructor could even take type parameters not specified in the datatype, which creates a kind of funky existential type.

Anyway, back to our example, we'd need a little java code to use it (or, maybe better, a way to express phantom types in JADT)

 class IntType { private IntType() {} };
 class BooleanType { private IntType() {} };

The code would generate (with a lot more boilerplate, of course)

abstract class Expression<A> {
   static class IntLiteral extends Expression<A> {
      int value;
   }
   //BooleanLiteral, Add, etc
   static class If<A> extends Expression<A> {
      Expression<Boolean> condition;
      Expression<A> trueCase;
      Expression<A> falseCase;
   }
}

Which is all pretty straight forward.

But.

I'm not sure the utility justifies the complexity of implementation. How often are GADTs that useful? In Java? I mean, the type system of our language above has to be pretty simple or we move past what Java can express.

So the idea will sit and stew for awhile.

One downside to GADTs is that it's impractical to have specialized Visitors that don't need the "impossible" cases. Concretely, given the above language GADT, we might have the following method

boolean isBooleanLiteral(Expression<Boolean> expr) {
   return new Expression.Visitor<Boolean, Boolean>() {
     public Boolean visit(BooleanLiteral x) { return true; }
     public Boolean visit(If<Boolean> x) { return false; }

     // so far so good.  The problem is that the following two cases are impossible but 
     // must still be accounted for. Using getDefault takes away the impossible
     // boilerplate, but also allows potentially important cases to be missed
 
     public Boolean visit(IntLieral x) { return false; } // impossible
     public Boolean visit(Add x) { return false; } // impossible
   };
}

Maybe that's okay, but I find it annoying. Haskell's GADTs, by contrast, allow you to skip impossible patterns while still proving exhaustiveness.