<div style="line-height:1.7;color:#000000;font-size:14px;font-family:Arial"><div>We know that the type system is now a second language where you spec formal requirements and let the compiler solve it, kinda like logic programming.<br>But sometimes I knew something is correct or at least willing to take the risk of runtime errors, but the typechecker is not (yet) able to figure it out.<br>In this case is it possible to somehow insert (regular haskell) code into the typechecker and force the compiler to think some values are of some types,<br>rather than waiting for or inventing some formally correct solution, which may be fundamentally very difficult?<br><br></div></div>