[GHC] #9974: Allow more general structural recursion without UndecidableInstances

[GHC]

#9974: Allow more general structural recursion without UndecidableInstances
-------------------------------------+-------------------------------------
              Reporter:  dfeuer      |             Owner:
                  Type:  feature     |            Status:  new
  request                            |         Milestone:
              Priority:  normal      |           Version:  7.11
             Component:  Compiler    |  Operating System:  Unknown/Multiple
  (Type checker)                     |   Type of failure:  None/Unknown
              Keywords:              |        Blocked By:
          Architecture:              |   Related Tickets:
  Unknown/Multiple                   |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 I bet this is a duplicate, but I couldn't find it.

 A simple example from the `HList` package:

 {{{#!hs
 type family HRevApp (l1 :: [k]) (l2 :: [k]) :: [k]
 type instance HRevApp '[] l = l
 type instance HRevApp (e ': l) l' = HRevApp l (e ': l')
 }}}

 GHC 7.8.3 and 7.11 both complain about the second instance if
 `UndecidableInstances` is turned off, because the application is no
 smaller than the index head. Moreover, the same error occurs when the type
 family is closed. However, GHC already knows how to separate term-level
 definitions into recursive groups; applying this same analysis to the type
 family above would reveal that `HRevApp` is structurally recursive, and
 therefore decidable. It is key, in this case, that the instance for `[]`
 is visible from the instance declaration for `e ': l`, so such an analysis
 could only be done in module dependency order for open type families.

 Side note: there is a (nasty) workaround available for the problem in this
 case:

 {{{#!hs
 type family HRevApp' (l1 :: [k]) (l1' :: [k])  (l2 :: [k]) :: [k]
 type instance HRevApp' t '[] l = l
 type instance HRevApp' (e ': l) (e' ': l') l'' = HRevApp' l l' (e ': l'')

 type HRevApp l1 l2 = HRevApp' l1 l1 l2
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9974>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler