Commit 77b63e74 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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)
parent c32bb5d0
......@@ -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
......
......@@ -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}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment