#14592: Totality checking -------------------------------------+------------------------------------- Reporter: varosi | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree with your first sentence -- it is of a similar impact to more types. The problem is that Haskell's type system is so flexible at the moment that I'm not sure we could prove any function that contains a function call as terminating. (Kind polymorphism and `Type :: Type` both introduce ways of writing very sneakily non-terminating functions.) So, essentially, I agree with you: we can verify totality only for certain functions, but those functions are (currently) very trivial: just case matches and returned constants. To expand this set would take ground- breaking research. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14592#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler