[mjdv]

I would say we have a problem when people who write compilers can't read type theory papers, but then our backgrounds might differ. ;-)