[TYPES] I: On Dependent types and Subtyping's consistency

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello Everyone,

          I am trying to check if it is possible to do reflection (as in Java) using "type safe" languages and, therefore, I am wondering if there is a language having dependent types with subtyping (in particular, I'm not talking of subtyping as in types' universes, but as in record subtyping). All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since then, it seems that whether the type system is consistent or not is still an open problem ( http://lucacardelli.name/Papers/Dependent%20Typechecking.US.pdf ).
           Therefore, I'm wondering if there are any advances on this regard: moreover, it seems to be that no proof assistant supports this technology.
           Thanks in advance for any reply,

     Giacomo Bergami
     Ph.D Student
     University of Bologna
     https://jackbergus.github.io/