Opened 9 months ago

Last modified 4 days ago

#14230 new bug

Gruesome kind mismatch errors for associated data family instances

Reported by: RyanGlScott Owned by: goldfire
Priority: high Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.3
Keywords: TypeInType Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: #14175 Differential Rev(s):
Wiki Page:

Description

Spun off from https://ghc.haskell.org/trac/ghc/ticket/14175#comment:9. This program, which can only really be compiled on GHC HEAD at the moment:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class C k where
  data CD :: k -> k -> *

instance C (Maybe a) where
  data CD :: (k -> *) -> (k -> *) -> *

Gives a heinous error message:

Bug.hs:11:3: error:
    • Expected kind ‘(k -> *) -> (k -> *) -> *’,
        but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a
                                                        -> Maybe a -> *’
    • In the data instance declaration for ‘CD’
      In the instance declaration for ‘C (Maybe a)’
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |   ^^^^^^^
  • We shouldn't be expecting kind (k -> *) -> (k -> *) -> *, but rather kind Maybe a -> Maybe a -> *, due to the instance head itself.
  • The phrase ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’ is similarly confusing. This doesn't point out that the real issue is the use of (k -> *).

Another program in a similar vein:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

class C a where
  data CD k (a :: k) :: k -> *

instance C (Maybe a) where
  data CD k (a :: k -> *) :: (k -> *) -> *
Bug.hs:13:3: error:
    • Expected kind ‘(k -> *) -> *’,
        but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’
    • In the data instance declaration for ‘CD’
      In the instance declaration for ‘C (Maybe a)’
   |
13 |   data CD k (a :: k -> *) :: (k -> *) -> *
   |   ^^^^^^^^^^^^^^^^^^^^^^^

This error message is further muddled by the incorrect use of k as the first type pattern (instead of k -> *, as subsequent kind signatures would suggest).

Change History (4)

comment:1 Changed 9 months ago by Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 9 months ago by simonpj

Milestone: 8.4.1
Owner: set to goldfire
Priority: normalhigh

Richard and I discussed this. It's firmly on his radar.

comment:3 Changed 4 weeks ago by RyanGlScott

Milestone: 8.4.18.6.1

comment:4 Changed 4 days ago by bgamari

Milestone: 8.6.18.8.1

This won't be fixed in 8.6. Bumping to 8.8.

Note: See TracTickets for help on using tickets.