Opened 2 years ago

Closed 2 years ago

#6020 closed feature request (fixed)

"Couldn't match kind" with free type variables and PolyKinds

Reported by: atnnn Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.5
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: polykinds/T6020, T6020a Blocked By:
Blocking: Related Tickets:

Description

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

Change History (5)

comment:1 Changed 2 years ago by atnnn

Pinning the kind makes the instance work:

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

But using kind variables doesn't:

instance (Id x (y :: k), Id y z) => Test x (z :: k)
Not in scope: type variable `k'

comment:2 Changed 2 years ago by simonpj@…

commit 6b0537a13b101755d9f2b807e32751845ada6c4f

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Sun Apr 22 17:52:55 2012 +0100

    Respect kind-variable scoping when instantiating dfuns
    
    Fixes Trac #6020

 compiler/typecheck/TcInteract.lhs |   17 +++++---------
 compiler/typecheck/TcSMonad.lhs   |   44 +++++++++++++++++++++---------------
 compiler/types/InstEnv.lhs        |   34 +++++++++++++---------------
 3 files changed, 48 insertions(+), 47 deletions(-)

comment:3 Changed 2 years ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to polykinds/T6020

Thanks. Fixed.

comment:4 Changed 2 years ago by atnnn

  • Resolution fixed deleted
  • Status changed from closed to new

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]

comment:5 Changed 2 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case changed from polykinds/T6020 to polykinds/T6020, T6020a

Urgh. A one-character typo! Fixed by

commit 4cc882650af6a4fadb30706f21e987edb846bcc3
Author: Simon Peyton Jones <simonpj@microsoft.com>
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!

Note: See TracTickets for help on using tickets.