The way I was envisioning it, there needn't be any down-casting at the language level. Particularly if you want to close the sum type (which you need anyway if you want exhaustiveness checks):

   public static void test(MaybeFoo mf) {
      switch(mf.type) {
         case MaybeFoo.NOTHING:
             /* ... */
             break;
         case MaybeFoo.JUST:
             Foo f = mf.getFoo();

             /* ... */
             break;
      }
   }

Still has exhaustiveness checking and no downcasts. Still can throw if you use the wrong get* under one of those branches, so I'm certainly not saying it's ideal, but I think it legitimately expresses a sum type and can be implemented in most any language with small adjustments.