title: Is it possible to mix dynamic and static types in a setting such as System F or CoC?
body: <p>I have a quite big codebase of untyped λ-terms. I think it could be fun trying to this codebase to the Calculus of Constructions, but I'd not like to implement everything from scratch. Instead, I'd like the type system to accept my untyped terms. I'd slowly add type annotations in a progressive manner. </p>
  
  <p>My idea is to extend CoC with a "unknown" type annotation, <code>?</code>, that would always typecheck, but I'm not sure that would work. Is there any known, principled way to do this?</p>