Haskell › Haskell - Glasgow-haskell-bugs

[GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

Classic

List

Threaded

6 messages Options

GHC

[GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

#6020: "Couldn't match kind" with free type variables and PolyKinds
---------------------------------------+------------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler
Version: 7.5 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------------+------------------------------------
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
}}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

GHC

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

In reply to this post by GHC

GHC

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

In reply to this post by GHC

GHC

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

In reply to this post by GHC

#6020: "Couldn't match kind" with free type variables and PolyKinds
----------------------------------------+-----------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.5
Resolution: | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: polykinds/T6020 | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------
Changes (by atnnn):

* status: closed => new
* resolution: fixed =>

Comment:

If I switch to equality constraints and reverse the functional dependency
of Id, I get the same error as above ({{{Couldn't match kind `k0' with
`Bool'}}}):

{{{
{-# LANGUAGE DataKinds, FunctionalDependencies, FlexibleInstances,
UndecidableInstances, PolyKinds, KindSignatures,
ConstraintKinds, FlexibleContexts, GADTs #-}

class Id (a :: k) (b :: k) | b -> a
instance a ~ b => Id a b

class Test (x :: a) (y :: a)
instance (Id x y, Id y z) => Test x z

test :: Test True True => ()
test = ()

main = print test
}}}

If I comment out `main`, it loads fine but GHC now panics when I use
`test`:

{{{
>>> :load "testid.hs"
>>> test
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 7.5.20120425 for x86_64-unknown-linux):
tcTyVarDetails k0{tv alS} [tv]
}}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

In reply to this post by GHC

#6020: "Couldn't match kind" with free type variables and PolyKinds
----------------------------------------+-----------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.5
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: polykinds/T6020, T6020a | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------
Changes (by simonpj):

* status: new => closed
* testcase: polykinds/T6020 => polykinds/T6020, T6020a
* resolution: => fixed

Comment:

Urgh. A one-character typo! Fixed by
{{{
commit 4cc882650af6a4fadb30706f21e987edb846bcc3
Author: Simon Peyton Jones <[hidden email]>
Date: Thu Apr 26 09:29:15 2012 +0100

Fix a one-character typo (kv1 should be kv2!)

Fixes Trac #6020, #6044
>---------------------------------------------------------------

compiler/typecheck/TcUnify.lhs | 2 +-
1 files changed, 1 insertions(+), 1 deletions(-)

diff --git a/compiler/typecheck/TcUnify.lhs
b/compiler/typecheck/TcUnify.lhs index 1729dcd..6e4d128 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -1119,7 +1119,7 @@ uKVar isFlipped unify_kind eq_res kv1 k2
| TyVarTy kv2 <- k2, kv1 == kv2
= return eq_res

- | TyVarTy kv2 <- k2, isTcTyVar kv1, isMetaTyVar kv2
+ | TyVarTy kv2 <- k2, isTcTyVar kv2, isMetaTyVar kv2
= uKVar (not isFlipped) unify_kind eq_res kv2 (TyVarTy kv1)

| otherwise = if isFlipped
}}}
I added a new regression test too!

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs