[GHC] #14592: Totality checking

[GHC]

#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