-zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
-zonkTcTyVars tyvars
- = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars) `thenNF_Tc` \ tys ->
- returnNF_Tc (tyVarsOfTypes tys)
-
-zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
-zonkTcTyVar tyvar
- = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty -- tcReadTyVar never returns a bound tyvar
- BoundTo other -> zonkTcType other
- other -> returnNF_Tc (TyVarTy tyvar)
-
--- Signature type variables only get bound to each other,
--- never to a type
-zonkSigTyVar :: TcTyVar s -> NF_TcM s (TcTyVar s)
-zonkSigTyVar tyvar
- = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc tyvar' -- tcReadTyVar never returns a bound tyvar
- BoundTo other -> panic "zonkSigTyVar" -- Should only be bound to another tyvar
- other -> returnNF_Tc tyvar
-
-zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
-zonkTcTypes tys = mapNF_Tc zonkTcType tys
-
-zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
-zonkTcThetaType theta = mapNF_Tc zonk theta
- where
- zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
- returnNF_Tc (c, new_ts)
-
-zonkTcType :: TcType s -> NF_TcM s (TcType s)
-
-zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
-
-zonkTcType (AppTy ty1 ty2)
- = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
- zonkTcType ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (mkAppTy ty1' ty2')
-
-zonkTcType (TyConApp tc tys)
- = mapNF_Tc zonkTcType tys `thenNF_Tc` \ tys' ->
- returnNF_Tc (TyConApp tc tys')
-
-zonkTcType (SynTy ty1 ty2)
- = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
- zonkTcType ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (SynTy ty1' ty2')
-
-zonkTcType (ForAllTy tv ty)
- = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
- zonkTcType ty `thenNF_Tc` \ ty' ->
- case tv_ty of -- Should be a tyvar!
- TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
- _ -> panic "zonkTcType"
- -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
- -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
-
-zonkTcType (FunTy ty1 ty2)
- = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
- zonkTcType ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (FunTy ty1' ty2')
+legalFEArgTyCon :: TyCon -> Bool
+-- It's illegal to return foreign objects and (mutable)
+-- bytearrays from a _ccall_ / foreign declaration
+-- (or be passed them as arguments in foreign exported functions).
+legalFEArgTyCon tc
+ | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ]
+ = False
+ -- It's also illegal to make foreign exports that take unboxed
+ -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
+ | otherwise
+ = boxedMarshalableTyCon tc
+
+legalFIResultTyCon :: DynFlags -> TyCon -> Bool
+legalFIResultTyCon dflags tc
+ | getUnique tc `elem`
+ [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
+ | tc == unitTyCon = True
+ | otherwise = marshalableTyCon dflags tc
+
+legalFEResultTyCon :: TyCon -> Bool
+legalFEResultTyCon tc
+ | getUnique tc `elem`
+ [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
+ | tc == unitTyCon = True
+ | otherwise = boxedMarshalableTyCon tc
+
+legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
+-- Checks validity of types going from Haskell -> external world
+legalOutgoingTyCon dflags safety tc
+ | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
+ = False
+ | otherwise
+ = marshalableTyCon dflags tc
+
+marshalableTyCon dflags tc
+ = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
+ || boxedMarshalableTyCon tc
+
+boxedMarshalableTyCon tc
+ = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
+ , int32TyConKey, int64TyConKey
+ , wordTyConKey, word8TyConKey, word16TyConKey
+ , word32TyConKey, word64TyConKey
+ , floatTyConKey, doubleTyConKey
+ , addrTyConKey, ptrTyConKey, funPtrTyConKey
+ , charTyConKey
+ , stablePtrTyConKey
+ , byteArrayTyConKey, mutableByteArrayTyConKey
+ , boolTyConKey
+ ]
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Unification with an explicit substitution}
+%* *
+%************************************************************************
+
+Unify types with an explicit substitution and no monad.
+Ignore usage annotations.
+
+\begin{code}
+type MySubst
+ = (TyVarSet, -- Set of template tyvars
+ TyVarSubstEnv) -- Not necessarily idempotent
+
+unifyTysX :: TyVarSet -- Template tyvars
+ -> Type
+ -> Type
+ -> Maybe TyVarSubstEnv
+unifyTysX tmpl_tyvars ty1 ty2
+ = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
+
+unifyExtendTysX :: TyVarSet -- Template tyvars
+ -> TyVarSubstEnv -- Substitution to start with
+ -> Type
+ -> Type
+ -> Maybe TyVarSubstEnv -- Extended substitution
+unifyExtendTysX tmpl_tyvars subst ty1 ty2
+ = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
+
+unifyTyListsX :: TyVarSet -> [Type] -> [Type]
+ -> Maybe TyVarSubstEnv
+unifyTyListsX tmpl_tyvars tys1 tys2
+ = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
+
+
+uTysX :: Type
+ -> Type
+ -> (MySubst -> Maybe result)
+ -> MySubst
+ -> Maybe result
+
+uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
+uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
+
+ -- Variables; go for uVar
+uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
+ | tyvar1 == tyvar2
+ = k subst
+uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
+ | tyvar1 `elemVarSet` tmpls
+ = uVarX tyvar1 ty2 k subst
+uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
+ | tyvar2 `elemVarSet` tmpls
+ = uVarX tyvar2 ty1 k subst
+
+ -- Predicates
+uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
+ | n1 == n2 = uTysX t1 t2 k subst
+uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
+ | c1 == c2 = uTyListsX tys1 tys2 k subst
+uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
+ | tc1 == tc2 = uTyListsX tys1 tys2 k subst
+
+ -- Functions; just check the two parts
+uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
+ = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
+
+ -- Type constructors must match
+uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
+ | (con1 == con2 && equalLength tys1 tys2)
+ = uTyListsX tys1 tys2 k subst
+
+ -- Applications need a bit of care!
+ -- They can match FunTy and TyConApp, so use splitAppTy_maybe
+ -- NB: we've already dealt with type variables and Notes,
+ -- so if one type is an App the other one jolly well better be too
+uTysX (AppTy s1 t1) ty2 k subst
+ = case tcSplitAppTy_maybe ty2 of
+ Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
+ Nothing -> Nothing -- Fail
+
+uTysX ty1 (AppTy s2 t2) k subst
+ = case tcSplitAppTy_maybe ty1 of
+ Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
+ Nothing -> Nothing -- Fail
+
+ -- Not expecting for-alls in unification
+#ifdef DEBUG
+uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
+uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
+#endif
+
+ -- Anything else fails
+uTysX ty1 ty2 k subst = Nothing
+
+
+uTyListsX [] [] k subst = k subst
+uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
+uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
+\end{code}
+
+\begin{code}
+-- Invariant: tv1 is a unifiable variable
+uVarX tv1 ty2 k subst@(tmpls, env)
+ = case lookupSubstEnv env tv1 of
+ Just (DoneTy ty1) -> -- Already bound
+ uTysX ty1 ty2 k subst
+
+ Nothing -- Not already bound
+ | typeKind ty2 `eqKind` tyVarKind tv1
+ && occur_check_ok ty2
+ -> -- No kind mismatch nor occur check
+ k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
+
+ | otherwise -> Nothing -- Fail if kind mis-match or occur check
+ where
+ occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
+ occur_check_ok_tv tv | tv1 == tv = False
+ | otherwise = case lookupSubstEnv env tv of
+ Nothing -> True
+ Just (DoneTy ty) -> occur_check_ok ty
+\end{code}
+
+
+
+%************************************************************************
+%* *
+\subsection{Matching on types}
+%* *
+%************************************************************************
+
+Matching is a {\em unidirectional} process, matching a type against a
+template (which is just a type with type variables in it). The
+matcher assumes that there are no repeated type variables in the
+template, so that it simply returns a mapping of type variables to
+types. It also fails on nested foralls.
+
+@matchTys@ matches corresponding elements of a list of templates and
+types. It and @matchTy@ both ignore usage annotations, unlike the
+main function @match@.
+
+\begin{code}
+matchTy :: TyVarSet -- Template tyvars
+ -> Type -- Template
+ -> Type -- Proposed instance of template
+ -> Maybe TyVarSubstEnv -- Matching substitution
+
+
+matchTys :: TyVarSet -- Template tyvars
+ -> [Type] -- Templates
+ -> [Type] -- Proposed instance of template
+ -> Maybe (TyVarSubstEnv, -- Matching substitution
+ [Type]) -- Left over instance types
+
+matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
+
+matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
+ (\ (senv,tys) -> Just (senv,tys))
+ emptySubstEnv
+\end{code}
+
+@match@ is the main function. It takes a flag indicating whether
+usage annotations are to be respected.
+
+\begin{code}
+match :: Type -> Type -- Current match pair
+ -> TyVarSet -- Template vars
+ -> (TyVarSubstEnv -> Maybe result) -- Continuation
+ -> TyVarSubstEnv -- Current subst
+ -> Maybe result
+
+-- When matching against a type variable, see if the variable
+-- has already been bound. If so, check that what it's bound to
+-- is the same as ty; if not, bind it and carry on.
+
+match (TyVarTy v) ty tmpls k senv
+ | v `elemVarSet` tmpls
+ = -- v is a template variable
+ case lookupSubstEnv senv v of
+ 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
+
+ | otherwise
+ = -- v is not a template variable; ty had better match
+ -- Can't use (==) because types differ
+ case tcGetTyVar_maybe ty of
+ Just v' | v == v' -> k senv -- Success
+ other -> Nothing -- Failure
+ -- This tcGetTyVar_maybe is *required* because it must strip Notes.
+ -- I guess the reason the Note-stripping case is *last* rather than first
+ -- is to preserve type synonyms etc., so I'm not moving it to the
+ -- top; but this means that (without the deNotetype) a type
+ -- variable may not match the pattern (TyVarTy v') as one would
+ -- expect, due to an intervening Note. KSW 2000-06.
+
+ -- Predicates
+match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
+ | n1 == n2 = match t1 t2 tmpls k senv
+match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
+ | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
+match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
+ | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
+
+ -- Functions; just check the two parts
+match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
+ = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
+
+match (AppTy fun1 arg1) ty2 tmpls k senv
+ = case tcSplitAppTy_maybe ty2 of
+ Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
+ Nothing -> Nothing -- Fail
+
+match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
+ | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
+
+-- Newtypes are opaque; other source types should not happen
+match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
+ | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
+
+ -- With type synonyms, we have to be careful for the exact
+ -- same reasons as in the unifier. Please see the
+ -- considerable commentary there before changing anything
+ -- here! (WDP 95/05)
+match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
+match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
+
+-- Catch-all fails
+match _ _ _ _ _ = Nothing
+
+match_list_exactly tys1 tys2 tmpls k senv
+ = match_list tys1 tys2 tmpls k' senv
+ where
+ k' (senv', tys2') | null tys2' = k senv' -- Succeed
+ | otherwise = Nothing -- Fail
+
+match_list [] tys2 tmpls k senv = k (senv, tys2)
+match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
+match_list (ty1:tys1) (ty2:tys2) tmpls k senv
+ = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv