Opened 2 months ago

Closed 6 weeks 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:

Description

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 2 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 2 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 2 months ago by goldfire

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

comment:4 Changed 2 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
  where
    ...
    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 2 months ago by goldfire

Yes, comment:4 seems right to me.

comment:6 Changed 2 months ago by RyanGlScott

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

comment:7 Changed 6 weeks ago by Krzysztof Gogolewski <krz.gogolewski@…>

In 6dea7c1/ghc:

Reject class instances with type families in kinds

Summary:
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: https://phabricator.haskell.org/D5068

comment:8 Changed 6 weeks ago by monoidal

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