[GHC] #14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary
GHC
ghc-devs at haskell.org
Thu Jul 27 19:02:36 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: 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:/docs/users_guide/8.4.1-notes.rst#l24
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
More information about the ghc-tickets
mailing list