There are ways (for example, https://jeltsch.wordpress.com/2012/04/30/dependently-typed-programming-and-theorem-proving-in-haskell/, PromotedDataKinds extension) to fake dependent types in haskell, and this makes it possible to prove some code properties in haskell itself.
Examples of properties I may want proved include totality of some function or monad laws for somr Monad typeclass instance.
Such a proof would be a value (a::T) where T represents the statement we've proved. Unfortunately, in haskell we can write terms of false type, e. g. (fix id::forall a.a), so we can actually prove everything. Is there a tool to check proof correctness or monad laws satisfaction in haskell? Does anybody include proofs in source code?