Bogus "No instance" error when type families appear in kinds
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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.4.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |