Type family stopped compiling on upgrade from GHC 7.6.3 to 7.8.3

cheater00 . cheater00 at gmail.com
Wed Jul 23 14:49:14 UTC 2014


Dear all,
while still not understanding kinds and type families well enough, my
random explorations have led me to finding syntax which currently is
accepted in 7.8.3 but seems to be surprising as well. This is to mean
the code is probably bogus, but GHC somehow manages not to notice.

If I write:

data Cmp a where
  Inf ::      Cmp a
  Sup ::      Cmp a
  V   :: a -> Cmp a
  deriving (Show, Eq)

data family   CmpInterval (a :: Cmp k) (b :: Cmp k) :: *
data instance CmpInterval  Inf          Sup          = Always
data instance CmpInterval (V c)         Sup          = Starting c
data instance CmpInterval  Inf         (V d)         = Ending d
data instance CmpInterval (V c)        (V d)         = c `Interval` d

that compiles without complaint. However, if I add deriving (Show) to
any instance but the first one:

data family   CmpInterval (a :: Cmp k) (b :: Cmp k) :: *
data instance CmpInterval  Inf          Sup          = Always
data instance CmpInterval (V c)         Sup          = Starting c
data instance CmpInterval  Inf         (V d)         = Ending d
data instance CmpInterval (V c)        (V d)         = c `Interval` d
  deriving (Show)

then I get:

src/Parser.hs:864:13:
    Can't make a derived instance of
      ‘Show (CmpInterval ('V c) ('V d))’:
      No family instance for ‘CmpInterval ('V c) ('V d)’
    In the data instance declaration for ‘CmpInterval’

Which is surprising, because the instance gets accepted without error,
whereas if we actually try to use it then it turns out not to be
there.

I was wondering if I again did something wrong (I'm still negotiating
with type families whether they'll let me understand them) and if so,
whether GHC would normally be expected to tell me of that - or do I
need to populate the type families with types and/or values in order
to let GHC finally figure out the code I'm writing is bogus?

Thanks!

On Tue, Jul 22, 2014 at 11:20 AM, cheater00 . <cheater00 at gmail.com> wrote:
> Indeed, I hadn't come to use that at the type level; the original code used
> my own types which ended up holding LocalTime; I used Float as a
> simplification as it displayed the same weird behaviour.
>
> I guess in the act of randomly walking parseable type family code I have
> inadvertently unearthed a bug, which someone else inadvertently fixed,
> making me a sort of human QuickCheck.
>
> On 22 Jul 2014 10:57, "Simon Peyton Jones" <simonpj at microsoft.com> wrote:
>>
>> I don't know why 7.6.3 accepts it.  'Float' is a valid type but not a
>> valid kind.  For it to be a useful kind we'd need float literal at the type
>> level, and we have no such thing.  You can use Nat instead, which does exist
>> at the type level.
>>
>> Simon
>>
>> | -----Original Message-----
>> | From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
>> | bounces at haskell.org] On Behalf Of cheater00 .
>> | Sent: 21 July 2014 18:51
>> | To: glasgow-haskell-users at haskell.org
>> | Subject: Type family stopped compiling on upgrade from GHC 7.6.3 to
>> | 7.8.3
>> |
>> | Hi, I was experimenting a bit with type families recently and ran into
>> | a bit of an issue. Given that I don't know type families that well yet,
>> | I was wondering if I made an error somewhere. One thing is that I can't
>> | find any relevant changes in the GHC release notes for 7.8.1, .2 or .3.
>> |
>> | Maybe this code contains an error which 7.6.3 simply wasn't able to
>> | find?
>> |
>> | Thanks.
>> |
>> | --------
>> |
>> | -- this code compiles in 7.6.3, but breaks in 7.8.3 with the following
>> | message:
>> | -- TypeFamilies.hs:14:31:
>> | --     ‘End’ of kind ‘*’ is not promotable
>> | --     In the kind ‘End’
>> | -- In 7.6.3, using :kind!, I can see that the type synonyms contained
>> | in the family do work the way I intend them to.
>> |
>> |
>> | {-# Language
>> |     GADTs
>> |   , TypeFamilies
>> |   , DataKinds
>> |    #-}
>> | module TypeFamilies where
>> |
>> | data End = Least | Spot Float | Most
>> |   deriving (Eq, Show)
>> |
>> | data Interval = IntervalCons { left :: End, right :: End }
>> |   deriving (Eq, Show)
>> |
>> | type family   Interval2 (a :: End) (b :: End) :: Interval
>> | type instance Interval2  Least      Most      =  IntervalCons  Least
>> | Most
>> | type instance Interval2 (Spot l)    Most      =  IntervalCons (Spot l)
>> | Most
>> | type instance Interval2  Least     (Spot r)   =  IntervalCons  Least
>> | (Spot r)
>> | type instance Interval2 (Spot l)   (Spot r)   =  IntervalCons (Spot l)
>> | (Spot r)
>> | _______________________________________________
>> | Glasgow-haskell-users mailing list
>> | Glasgow-haskell-users at haskell.org
>> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


More information about the Glasgow-haskell-users mailing list