#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