Opened 4 months ago

Closed 3 months ago

#13972 closed bug (fixed)

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1-rc2
Keywords: TypeFamilies, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case: indexed-types/should_fail/T13972
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3820
Wiki Page:

Description

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).

Change History (3)

comment:1 Changed 4 months ago by RyanGlScott

Differential Rev(s): Phab:D3820
Status: newpatch

I decided to go with approach (2) in Phab:D3820.

comment:2 Changed 3 months ago by Ryan Scott <ryan.gl.scott@…>

In 38260a9/ghc:

Fix #13972 by producing tidier errors

Summary:
Previously, one could experience an error message like this:

```
Expected: T (a -> Either a b)
  Actual: T (a -> Either a b)
```

This makes the error message an iota clearer by tidying it first, which will
instead produce:

```
Expected: T (a1 -> Either a1 b1)
  Actual: T (a -> Either a b)
```

Which steers users towards the understanding that the two sets of tyvars are
actually different.

Test Plan: make test TEST=T13972

Reviewers: simonpj, austin, bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, thomie

GHC Trac Issues: #13972

Differential Revision: https://phabricator.haskell.org/D3820

comment:3 Changed 3 months ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Test Case: indexed-types/should_fail/T13972
Note: See TracTickets for help on using tickets.