#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): There's a downside to totality checking: it means that the language needs to be simple enough to support it. GHC has several features making totality checking hard: * `Type :: Type` (whereas Idris has `Type :: Type 1`, `Type 1 :: Type 2`, etc.) * The `Type.Reflection` library (a.k.a. `Typeable`). Section 7 of the recent [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1002&context=compsci_pubs paper] shows how `Typeable` can lead to non-termination without recursion. * Non-strictly-positive datatypes (sorry, I don't know how Idris handles these, nor do I have a good reference for more information) * Pattern synonyms (should we trust `COMPLETE` pragmas here?) * Probably more... I agree that having a totality checker would be wonderful. But writing one with GHC's current feature set is a major research undertaking, and then maintaining it might force GHC to slow down its innovation in other areas. This isn't really an argument against it, but I just wanted to highlight that there are major tradeoffs here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14592#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler