GitLab

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

A simple example from the HList package:

{-# 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:

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