\begin{code}
module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
- unifyFunTy, unifyListTy, unifyTupleTy, unifyUnboxedTupleTy,
+ unifyFunTy, unifyListTy, unifyTupleTy,
unifyKind, unifyKinds, unifyTypeKind
) where
-- friends:
import TcMonad
-import Type ( Type(..), tyVarsOfType, funTyCon,
- mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+import TypeRep ( Type(..), funTyCon,
Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
+ ) -- friend
+import Type ( tyVarsOfType,
+ mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+ isNotUsgTy,
splitAppTy_maybe,
tidyOpenType, tidyOpenTypes, tidyTyVar
)
-import TyCon ( TyCon, isTupleTyCon, isUnboxedTupleTyCon,
- tyConArity )
-import Name ( isSysLocalName )
-import Var ( TyVar, tyVarKind, varName )
-import VarEnv
+import TyCon ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
+import Name ( hasBetterProv )
+import Var ( TyVar, tyVarKind, varName, isSigTyVar )
import VarSet ( varSetElems )
import TcType ( TcType, TcTauType, TcTyVar, TcKind,
newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
)
+
-- others:
-import BasicTypes ( Arity )
-import TysWiredIn ( listTyCon, mkListTy, mkTupleTy, mkUnboxedTupleTy )
-import PprType () -- Instances
-import Util
+import BasicTypes ( Arity, Boxity, isBoxed )
+import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
import Outputable
\end{code}
-> TcM s ()
-- Always expand synonyms (see notes at end)
+ -- (this also throws away FTVs and usage annots)
uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
-- Type constructors must match
uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
= checkTcM (cons_match && length tys1 == length tys2)
- (failWithTcM (unifyMisMatch ps_ty1 ps_ty2)) `thenTc_`
+ (unifyMisMatch ps_ty1 ps_ty2) `thenTc_`
unifyTauTyLists tys1 tys2
where
-- The AnyBox wild card matches anything
uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
= case splitAppTy_maybe ty2 of
Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
- Nothing -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
+ Nothing -> unifyMisMatch ps_ty1 ps_ty2
-- Now the same, but the other way round
-- Don't swap the types, because the error messages get worse
uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
= case splitAppTy_maybe ty1 of
Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
- Nothing -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
+ Nothing -> unifyMisMatch ps_ty1 ps_ty2
-- Not expecting for-alls in unification
-- ... but the error message from the unifyMisMatch more informative
-- than a panic message!
-- Anything else fails
-uTys ps_ty1 ty1 ps_ty2 ty2 = failWithTcM (unifyMisMatch ps_ty1 ps_ty2)
+uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
\end{code}
Notes on synonyms
| otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
- -- Expand synonyms
+ -- Expand synonyms; ignore FTVs; ignore usage annots
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
= uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
Nothing -> checkKinds swapped tv1 ty2 `thenTc_`
- -- Try to update sys-y type variables in preference to sig-y ones
- -- (the latter respond False to isSysLocalName)
- if isSysLocalName (varName tv2) then
- tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
+ if tv1 `dominates` tv2 then
+ tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
returnTc ()
else
- tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
+ ASSERT( isNotUsgTy ps_ty2 )
+ tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
returnTc ()
+ where
+ tv1 `dominates` tv2 = isSigTyVar tv1
+ -- Don't unify a signature type variable if poss
+ || varName tv1 `hasBetterProv` varName tv2
+ -- Try to update sys-y type variables in preference to sig-y ones
-- Second one isn't a type variable
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
= returnTc ()
| otherwise
- = checkKinds swapped tv1 non_var_ty2 `thenTc_`
- occur_check non_var_ty2 `thenTc_`
- tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
+ = checkKinds swapped tv1 non_var_ty2 `thenTc_`
+ occur_check non_var_ty2 `thenTc_`
+ ASSERT( isNotUsgTy ps_ty2 )
+ checkTcM (not (isSigTyVar tv1))
+ (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
+
+ tcPutTyVar tv1 non_var_ty2 `thenNF_Tc_`
+ -- This used to say "ps_ty2" instead of "non_var_ty2"
+
+ -- But that led to an infinite loop in the type checker!
+ -- Consider
+ -- type A a = ()
+ --
+ -- f :: (A a -> a -> ()) -> ()
+ -- f = \ _ -> ()
+ --
+ -- x :: ()
+ -- x = f (\ x p -> p x)
+ --
+ -- Here, we try to match "t" with "A t", and succeed
+ -- because the unifier looks through synonyms. The occurs
+ -- check doesn't kick in because we are "really" binding "t" to "()",
+ -- but we *actually* bind "t" to "A t" if we store ps_ty2.
+ -- That leads the typechecker into an infinite loop later.
+
returnTc ()
where
occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_`
\end{code}
\begin{code}
-unifyTupleTy :: Arity -> TcType -> TcM s [TcType]
-unifyTupleTy arity ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyTupleTy arity ty'
- other -> unify_tuple_ty_help arity ty
-
-unifyTupleTy arity ty
- = case splitTyConApp_maybe ty of
- Just (tycon, arg_tys) | isTupleTyCon tycon
- && tyConArity tycon == arity
- -> returnTc arg_tys
- other -> unify_tuple_ty_help arity ty
-
-unify_tuple_ty_help arity ty
- = mapNF_Tc (\ _ -> newTyVarTy boxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys ->
- unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_`
- returnTc arg_tys
-\end{code}
-
-\begin{code}
-unifyUnboxedTupleTy :: Arity -> TcType -> TcM s [TcType]
-unifyUnboxedTupleTy arity ty@(TyVarTy tyvar)
+unifyTupleTy :: Boxity -> Arity -> TcType -> TcM s [TcType]
+unifyTupleTy boxity arity ty@(TyVarTy tyvar)
= tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
- Just ty' -> unifyUnboxedTupleTy arity ty'
- other -> unify_unboxed_tuple_ty_help arity ty
+ Just ty' -> unifyTupleTy boxity arity ty'
+ other -> unify_tuple_ty_help boxity arity ty
-unifyUnboxedTupleTy arity ty
+unifyTupleTy boxity arity ty
= case splitTyConApp_maybe ty of
- Just (tycon, arg_tys) | isUnboxedTupleTyCon tycon
- && tyConArity tycon == arity
- -> returnTc arg_tys
- other -> unify_tuple_ty_help arity ty
-
-unify_unboxed_tuple_ty_help arity ty
- = mapNF_Tc (\ _ -> newTyVarTy_OpenKind) [1..arity] `thenNF_Tc` \ arg_tys ->
- unifyTauTy ty (mkUnboxedTupleTy arity arg_tys) `thenTc_`
+ Just (tycon, arg_tys)
+ | isTupleTyCon tycon
+ && tyConArity tycon == arity
+ && tupleTyConBoxity tycon == boxity
+ -> returnTc arg_tys
+ other -> unify_tuple_ty_help boxity arity ty
+
+unify_tuple_ty_help boxity arity ty
+ = mapNF_Tc new_tyvar [1..arity] `thenNF_Tc` \ arg_tys ->
+ unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
returnTc arg_tys
+ where
+ new_tyvar _ | isBoxed boxity = newTyVarTy boxedTypeKind
+ | otherwise = newTyVarTy_OpenKind
\end{code}
Make sure a kind is of the form (Type b) for some boxity b.
pp2 = ppr ty2'
unifyMisMatch ty1 ty2
- = (env2, hang (ptext SLIT("Couldn't match"))
- 4 (sep [quotes (ppr tidy_ty1), ptext SLIT("against"), quotes (ppr tidy_ty2)]))
+ = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
+ zonkTcType ty2 `thenNF_Tc` \ ty2' ->
+ let
+ (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
+ msg = hang (ptext SLIT("Couldn't match"))
+ 4 (sep [quotes (ppr tidy_ty1),
+ ptext SLIT("against"),
+ quotes (ppr tidy_ty2)])
+ in
+ failWithTcM (env, msg)
+
+unifyWithSigErr tyvar ty
+ = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
+ 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
where
- (env1, tidy_ty1) = tidyOpenType emptyTidyEnv ty1
- (env2, tidy_ty2) = tidyOpenType env1 ty2
+ (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
+ (env2, tidy_ty) = tidyOpenType env1 ty
unifyOccurCheck tyvar ty
= (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
projects / ghc-hetmet.git / blobdiff