Opened 15 months ago

Closed 2 weeks ago

Last modified 2 weeks ago

#14230 closed bug (fixed)

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: indexed-types/should_fail/T14230{,a}
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 (8)

comment:1 Changed 15 months ago by Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 15 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 7 months ago by RyanGlScott

Milestone: 8.4.18.6.1

comment:4 Changed 6 months ago by bgamari

Milestone: 8.6.18.8.1

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

comment:5 Changed 2 weeks ago by RyanGlScott

By gum, this might just be fixed. On GHC HEAD (commit 2257a86daa72db382eb927df12a718669d5491f8), we get the following error message for the first program:

$ inplace/bin/ghc-stage2 --interactive ../Bug.hs
GHCi, version 8.7.20181129: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( ../Bug.hs, interpreted )

../Bug.hs:11:3: error:
    • Type indexes must match class instance head
      Expected: CD @(Maybe a)
        Actual: CD @(k -> *) -- Defined at ../Bug.hs:11:8
    • In the data instance declaration for ‘CD’
      In the instance declaration for ‘C (Maybe a)’
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |   ^^^^^^^

And the following error message for the second program:

GHCi, version 8.7.20181129: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( ../Bug.hs, interpreted )

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

Both of those look like pretty cromulent error messages to me. Should we check in test cases and declare victory?

comment:6 Changed 2 weeks ago by Simon Peyton Jones <simonpj@…>

In 80d665a/ghc:

Two tests for Trac #14230

comment:7 Changed 2 weeks ago by RyanGlScott

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_fail/T14230{,a}

comment:8 Changed 2 weeks ago by simonpj

Thanks for identifying this one Ryan. It had completely slipped off my radar.

Note: See TracTickets for help on using tickets.