Data family instances must list all patterns of family, despite documentation's claims to the contrary

(Originally spun off from #12369 (closed).)

The documentation for data families currently 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 (42392383) cites this particular example:

    data family Sing (a :: k)
    data instance Sing :: Bool -> Type where ...

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

{-# 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
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Trac metadata

Trac field	Value
Version	8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture