Commit 20f50b2a authored by simonpj's avatar simonpj
Browse files

[project @ 2002-02-07 12:51:34 by simonpj]

----------------------------------------------------
	Make TcType.match and TcUnify.uUnboundVar kind-aware
	----------------------------------------------------

George Russel had apparently-overlapping (ha) instance decls like

	instance .. => C (a b) where
	instance .. => C (x y) where

But the a,b and x,y were different kinds!  Turned out that TcType.unify
was kind-aware (so we didn't report a duplicate instance decl, but TcType.match
was not (so we simply selected the wrong one, and got a mis-kinded constraint
popping up from the ".."  part.  Very exciting to track down.

I also make the ordinary unification kind-aware in the same way.  It's
quite legitimate to attempt to unify, say,
	(a b)    with     (c d)
but the unification should fail if a's kind differs from c's.
(There was a kind of debug warning before, but it's actually not an error
in the compiler... so it should just make unification fail gracefully.)
parent 35c63bfc
......@@ -1087,7 +1087,15 @@ match (TyVarTy v) ty tmpls k senv
| v `elemVarSet` tmpls
= -- v is a template variable
case lookupSubstEnv senv v of
Nothing -> k (extendSubstEnv senv v (DoneTy ty))
Nothing | typeKind ty `eqKind` tyVarKind v
-- We do a kind check, just as in the uVarX above
-- The kind check is needed to avoid bogus matches
-- of (a b) with (c d), where the kinds don't match
-- An occur check isn't needed when matching.
-> k (extendSubstEnv senv v (DoneTy ty))
| otherwise -> Nothing -- Fails
Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
| otherwise -> Nothing -- Fails
......
......@@ -637,19 +637,18 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
checkKinds swapped tv1 ty2
-- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
-- ty2 has been zonked at this stage
-- ty2 has been zonked at this stage.
| tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
-- Check that we don't unify a lifted type variable with an
-- unlifted type: e.g. (id 3#) is illegal
| tk2 `hasMoreBoxityInfo` tk1 = returnTc ()
| otherwise
-- Either the kinds aren't compatible
-- (can happen if we unify (a b) with (c d))
-- or we are unifying a lifted type variable with an
-- unlifted type: e.g. (id 3#) is illegal
= tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
unifyMisMatch k1 k2
| otherwise
= -- Check that we aren't losing boxity info (shouldn't happen)
WARN (not (tk2 `hasMoreBoxityInfo` tk1),
(ppr tv1 <+> ppr tk1) $$ (ppr ty2 <+> ppr tk2))
returnTc ()
where
(k1,k2) | swapped = (tk2,tk1)
| otherwise = (tk1,tk2)
......
......@@ -119,20 +119,25 @@ import UniqSet ( sizeUniqSet ) -- Should come via VarSet
\begin{code}
hasMoreBoxityInfo :: Kind -> Kind -> Bool
-- (k1 `hasMoreBoxityInfo` k2) checks that k1 <: k2
hasMoreBoxityInfo k1 k2
| k2 `eqKind` openTypeKind = True
| otherwise = k1 `eqType` k2
| k2 `eqKind` openTypeKind = ok k1
| otherwise = k1 `eqKind` k2
where
ok (TyConApp tc _) = tc == typeCon || tc == openKindCon
ok (NoteTy _ k) = ok k
ok other = False
isTypeKind :: Kind -> Bool
-- True of kind * and *#
isTypeKind (TyConApp tc _) = tc == typeCon
isTypeKind (NoteTy _ k) = isTypeKind k
isTypeKind other = False
defaultKind :: Kind -> Kind
-- Used when generalising: default kind '?' to '*'
defaultKind kind | kind `eqKind` openTypeKind = liftedTypeKind
| otherwise = kind
isTypeKind :: Kind -> Bool
-- True of kind * and *#
isTypeKind k = case splitTyConApp_maybe k of
Just (tc,[k]) -> tc == typeCon
other -> False
\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