#13972: GHC 8.2 error message around indexes for associated type instances is baffling -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 (Type checker) | Keywords: TypeFamilies, | Operating System: Unknown/Multiple TypeInType | Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This program doesn't typecheck (only in GHC 8.2 and later): {{{#!hs {-# 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`: {{{#!hs {-# 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`). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13972> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler