"Couldn't match kind" with free type variables and PolyKinds
In the following code, I was hoping that GHC could infer the more specific kind of the free variable y and the class Id in the head of the instance for Test.
Also, the error message is confusing:
-
It says that 'True has kind k0 (maybe it's an impredicative kind?)
-
It refers to k0 as a type variable
{-# LANGUAGE DataKinds, FunctionalDependencies, FlexibleInstances,
UndecidableInstances, PolyKinds, KindSignatures,
ConstraintKinds, FlexibleContexts #-}
import GHC.Prim (Constraint)
class Id (a :: k) (b :: k) | a -> b
instance Id a a
class Test (x :: a) (y :: a) | x -> y
instance (Id x y, Id y z) => Test x z
test :: Test True True => ()
test = ()
>>> test
<interactive>:54:1:
Couldn't match kind `k0' with `Bool'
`k0' is an unknown type variable
Kind incompatibility when matching types:
'True :: k0
'True :: Bool
When using functional dependencies to combine
Id k0 a a,
arising from the dependency `a -> b'
in the instance declaration at /home/atnnn/code/type-prelude/testfoldl.hs:8:10
Id Bool 'True 'True,
arising from a use of `test' at <interactive>:54:1-4
In the expression: test
Trac metadata
Trac field | Value |
---|---|
Version | 7.5 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |