And of course, Haskell has equivalent too:

    case eqT @a @String of
      Just Refl -> ...