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 |