Don't treat types as theorem provers, treat them as formalized docs - getting dirty with dynamic under the hood is perfectly acceptable to me (say you're doing some metaprogramming - typing that out is usually a lot of effort for low gain) - the types just help define intended use.

In code consuming types I relie on inference 80% of the time, sometimes I need to specify generics, if it fails I do dirty casts, if that fails I do dynamic blocks.