Regression error: Kind variables don't work inside of kind constructors in type families

[goldfire]

Many thanks for the quick bug fixes around kind variables recently.

With the newest build (7.5.20120425), the following code fails:

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures #-}

type family Foo (a :: k) :: Maybe k
type instance Foo a = Just a

The error is:

    Kind mis-match
    The first argument of `Just' should have kind `k0',
    but `a' has kind `k'
    In the type `Just a'
    In the type instance declaration for `Foo'

The above code compiles without error on, e.g., 7.5.20120329.

I think it's worth noting that the following compiles fine, which surprised me given the error above:

type family Id (a :: k) :: k
type instance Id a = a

[simonpj]

Turns out to be the same trivial bug as #6020. 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