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

[GHC]

#9974: Allow more general structural recursion without UndecidableInstances
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      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:                    |
-------------------------------------+-------------------------------------

Old description:

> 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
> }}}

New description:

 I bet this is a duplicate, but I couldn't find it.

 A simple example from the `HList` package:

 {{{#!hs
 {-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
 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
 }}}

--

Comment (by thomie):

 Added language pragma to example.

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