Opened 4 months ago

Closed 3 months ago

#15515 closed bug (fixed)

Bogus "No instance" error when type families appear in kinds

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: TypeInType, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5068
Wiki Page:


The following code typechecks:

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

import Data.Kind
import Data.Proxy

class C a where
  c :: Proxy a

type family F

data D :: F -> Type

instance C (D :: F -> Type) where
  c = undefined

However, if we try to actually use that C D instance, like so:

c' :: Proxy (D :: F -> Type)
c' = c @(D :: F -> Type)

Then GHC gives a rather flummoxing error message:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:20:6: error:
    • No instance for (C D) arising from a use of ‘c’
    • In the expression: c @(D :: F -> Type)
      In an equation for ‘c'’: c' = c @(D :: F -> Type)
20 | c' = c @(D :: F -> Type)
   |      ^^^^^^^^^^^^^^^^^^^

But that error is clearly misleading, as we defined such a C D instance directly above it!

The use of the type family F in the kind of D appears to play an important role in this bug. If I change F to be a data type (e.g., data F), then c' is accepted.

Change History (8)

comment:1 Changed 4 months ago by goldfire

The class instance should be rejected -- indeed, I'm quite surprised it's not.

Let's write with explicit kinds:

class C k a where ...
instance C (F -> Type) D where ...

That instance mentions a type family in one of its arguments, which should be rejected.

I would love to come up with a way where we ignore determined dependent arguments during matching, which would then allow this instance to work, but we're not there yet.

comment:2 Changed 4 months ago by RyanGlScott

Darn, I was afraid you were going to say that.

Is there any relationship between this ticket and #12564?

comment:3 Changed 4 months ago by goldfire

Yes -- fixing that ticket will allow this one to make forward (as opposed to backward) progress.

comment:4 Changed 4 months ago by RyanGlScott

Blocked By: 12564 added

So as far as why GHC doesn't simply error when you define instance C (D :: F -> Type), I think it might be due to these lines in check_valid_inst_head:

  | otherwise
  = mapM_ checkValidTypePat ty_args
    ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args

Where checkValidTypePat is what throws the Illegal type synonym family application in instance error seen in #12564. Because ty_args has filtered out kinds, it won't catch any type families in kinds, like in the original program.

I think we could extend this error message to kinds by simply mapping checkValidTypePat over all cls_args, and not just ty_args. Do you agree?

comment:5 Changed 4 months ago by goldfire

Yes, comment:4 seems right to me.

comment:6 Changed 4 months ago by RyanGlScott

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

comment:7 Changed 3 months ago by Krzysztof Gogolewski <krz.gogolewski@…>

In 6dea7c1/ghc:

Reject class instances with type families in kinds

GHC doesn't know how to handle type families that appear in
class instances. Unfortunately, GHC didn't reject instances where
type families appear in //kinds//, leading to #15515. This is easily
rectified by calling `checkValidTypePat` on all arguments to a class
in an instance (and not just the type arguments).

Test Plan: make test TEST=T15515

Reviewers: bgamari, goldfire, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, carter

GHC Trac Issues: #15515

Differential Revision:

comment:8 Changed 3 months ago by monoidal

Blocked By: 12564 removed
Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.