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

27 Jul 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:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.3
  (Type checker)                     |
           Keywords:  TypeFamilies   |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #12369
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 (Originally spun off from #12369.)

 The documentation for data families currently
 [http://git.haskell.org/ghc.git/blob/791947db6db32ef7d4772a821a0823e558e3c05b...
 claims]:

 {{{
 - Data families have been generalised a bit: a data family declaration can
 now
   end with a kind variable ``k`` instead of ``Type``. Additionally,
 data/newtype
   instance no longer need to list all the patterns of the family if they
 don't
   wish to; this is quite like how regular datatypes with a kind signature
 can omit
   some type variables.
 }}}

 Moreover, the commit which added this
 (4239238306e911803bf61fdda3ad356fd0b42e05) cites this particular example:

 {{{#!hs
     data family Sing (a :: k)
     data instance Sing :: Bool -> Type where ...
 }}}

 However, in practice, this does //not// typecheck on GHC HEAD:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}

 import Data.Kind

 data family Sing (a :: k)
 data instance Sing :: Bool -> Type where
   SFalse :: Sing False
   STrue  :: Sing True
 }}}

 {{{
 $ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
 GHCi, version 8.3.20170725: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:8:1: error:
     • Number of parameters must match family declaration; expected 0
     • In the data instance declaration for ‘Sing’
   |
 8 | data instance Sing :: Bool -> Type where
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler