| 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
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)
\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}