Two fixes to kind unification

* Don't unify a kind signature-variable with non-tyvar kind
* Don't allow a kind variable to appear in a type
  (Trac #7224)

2 files changed, 21 insertions, 8 deletions

diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 1f61e378d8..9650b059e9 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -570,7 +570,12 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
        ; thing <- tcLookup name
        ; traceTc "lk2" (ppr name <+> ppr thing)
        ; case thing of
-           ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
+           ATyVar _ tv 
+              | isKindVar tv
+              -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv)
+                             <+> ptext (sLit "used as a type"))
+              | otherwise
+              -> return (mkTyVarTy tv, tyVarKind tv)
 
            AThing kind -> do { tc <- get_loopy_tc name
                              ; inst_tycon (mkNakedTyConApp tc) kind }
@@ -1352,7 +1357,7 @@ tc_lhs_kind (L span ki) = setSrcSpan span (tc_hs_kind ki)
 
 -- The main worker
 tc_hs_kind :: HsKind Name -> TcM Kind
-tc_hs_kind k@(HsTyVar _)   = tc_kind_app k []
+tc_hs_kind (HsTyVar tc)    = tc_kind_var_app tc []
 tc_hs_kind k@(HsAppTy _ _) = tc_kind_app k []
 
 tc_hs_kind (HsParTy ki) = tc_lhs_kind ki
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 29f46f629c..6f92ccbd35 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -1162,17 +1162,20 @@ uUnboundKVar kv1 k2@(TyVarTy kv2)
 
 uUnboundKVar kv1 non_var_k2
   = do  { k2' <- zonkTcKind non_var_k2
-        ; kindOccurCheck kv1 k2'
         ; let k2'' = defaultKind k2'
                 -- MetaKindVars must be bound only to simple kinds
+        ; kindUnifCheck kv1 k2''
         ; writeMetaTyVar kv1 k2'' }
 
 ----------------
-kindOccurCheck :: TyVar -> Type -> TcM ()
-kindOccurCheck kv1 k2   -- k2 is zonked
-  = if elemVarSet kv1 (tyVarsOfType k2)
-    then failWithTc (kindOccurCheckErr kv1 k2)
-    else return ()
+kindUnifCheck :: TyVar -> Type -> TcM ()
+kindUnifCheck kv1 k2   -- k2 is zonked
+  | elemVarSet kv1 (tyVarsOfType k2)
+  = failWithTc (kindOccurCheckErr kv1 k2)
+  | isSigTyVar kv1
+  = failWithTc (kindSigVarErr kv1 k2)
+  | otherwise
+  = return ()
 
 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
 mkKindErrorCtxt ty1 ty2 k1 k2 env0
@@ -1204,4 +1207,9 @@ kindOccurCheckErr :: Var -> Type -> SDoc
 kindOccurCheckErr tyvar ty
   = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
        2 (sep [ppr tyvar, char '=', ppr ty])
+
+kindSigVarErr :: Var -> Type -> SDoc
+kindSigVarErr tv ty
+  = hang (ptext (sLit "Cannot unify the kind variable") <+> quotes (ppr tv))
+       2 (ptext (sLit "with the kind") <+> quotes (ppr ty))
 \end{code}