#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I don't see in the patch where an arity check is omitted. And I'd love a Note somewhere giving examples of "Data families aren't as particular about their arity as type families are (because data families can be undersaturated)", at some relevant point in the type checker. The point is, I guess, that {{{ data instance Sing :: Bool -> Type where SFalse :: Sing False STrue :: Sing True }}} and {{{ data instance Sing (a :: Bool) :: Type where SFalse :: Sing False STrue :: Sing True }}} are similar, but not quite the same. Moreover, different instances can make different choices. Moreover you can't to that for type families. We should call that out somewhere, and explain why it's different (data families can be decomposed, type families can't). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler