Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,264
    • Issues 5,264
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 568
    • Merge requests 568
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #13972
Closed
Open
Issue created Jul 13, 2017 by Ryan Scott@RyanGlScottMaintainer

GHC 8.2 error message around indexes for associated type instances is baffling

This program doesn't typecheck (only in GHC 8.2 and later):

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

class C (a :: k) where
  type T k :: Type

instance C Left where
  type T (a -> Either a b) = Int
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:12:8: error:
    • Type indexes must match class instance head
      Expected: T (a -> Either a b)
        Actual: T (a -> Either a b)
    • In the type instance declaration for ‘T’
      In the instance declaration for ‘C Left’
   |
12 |   type T (a -> Either a b) = Int
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^

Well those expected and actual types look pretty darn similar to me!

Note that the problem can be worked around by giving an explicit kind annotation for Left:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

class C (a :: k) where
  type T k :: Type

instance C (Left :: a -> Either a b) where
  type T (a -> Either a b) = Int

I see two things we could do here:

  1. Relax the "Type indexes must match class instance head" check so that it doesn't apply to invisible kind variables like a and b.
  2. Clarify the error message. At the very least, we could say Expected: T (a1 -> Either a1 b1) as a hint that a and b aren't the same type variables as a1 and b1. In an ideal world, we'd even indicate where a1 and b1 should be coming from (the kind of Left).
Trac metadata
Trac field Value
Version 8.2.1-rc2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking