[GHC] #14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary

GHC ghc-devs at haskell.org
Mon Jul 31 08:29:56 UTC 2017


#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


More information about the ghc-tickets mailing list