%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-\section{Type subsumption and unification}
+
+Type subsumption and unification
\begin{code}
module TcUnify (
#include "HsVersions.h"
-import HsSyn ( HsWrapper(..), idHsWrapper, isIdHsWrapper, (<.>),
- mkWpLams, mkWpTyLams, mkWpApps )
-import TypeRep ( Type(..), PredType(..) )
-
-import TcMType ( lookupTcTyVar, LookupTyVarResult(..),
- tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar,
- newBoxyTyVar, newBoxyTyVarTys, readFilledBox,
- readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy,
- tcInstSkolTyVars, tcInstTyVar,
- zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
- readKindVar, writeKindVar )
-import TcSimplify ( tcSimplifyCheck )
-import TcEnv ( tcGetGlobalTyVars, findGlobals )
-import TcIface ( checkWiredInTyCon )
+import HsSyn
+import TypeRep
+
+import TcMType
+import TcSimplify
+import TcEnv
+import TcIface
import TcRnMonad -- TcType, amongst others
-import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType,
- BoxySigmaType, BoxyRhoType, BoxyType,
- TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..),
- SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar,
- pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy,
- mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar,
- tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
- tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
- typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
- tcView, exactTyVarsOfType,
- tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
- pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar,
- TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst,
- substTy, substTheta,
- lookupTyVar, extendTvSubst )
-import Type ( Kind, SimpleKind, KindVar,
- openTypeKind, liftedTypeKind, unliftedTypeKind,
- mkArrowKind, defaultKind,
- argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
- isSubKind, pprKind, splitKindFunTys, isSubKindCon,
- isOpenTypeKind, isArgTypeKind )
-import TysPrim ( alphaTy, betaTy )
-import Inst ( newDictBndrsO, instCall, instToId )
-import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
-import TysWiredIn ( listTyCon )
-import Id ( Id )
-import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails )
+import TcType
+import Type
+import TysPrim
+import Inst
+import TyCon
+import TysWiredIn
+import Var
import VarSet
import VarEnv
-import Name ( Name, isSystemName )
-import ErrUtils ( Message )
-import Maybes ( expectJust, isNothing )
-import BasicTypes ( Arity )
-import Util ( notNull, equalLength )
+import Name
+import ErrUtils
+import Maybes
+import BasicTypes
+import Util
import Outputable
-
--- Assertion imports
-#ifdef DEBUG
-import TcType ( isBoxyTy, isFlexi )
-#endif
\end{code}
%************************************************************************
loop n args_so_far res_ty
| isSigmaTy res_ty -- Do this before checking n==0, because we
-- guarantee to return a BoxyRhoType, not a BoxySigmaType
- = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' ->
+ = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
loop n args_so_far res_ty'
; return (gen_fn <.> co_fn, res) }
tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
| not exp_ib, -- SKOL does not apply if exp_ty is inside a box
isSigmaTy exp_ty
- = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty ->
+ = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
where
-> TcTyVarSet -- Extra tyvars that the universally
-- quantified tyvars of expected_ty
-- must not be unified
- -> (BoxyRhoType -> TcM result) -- spec_ty
+ -> ([TcTyVar] -> BoxyRhoType -> TcM result)
-> TcM (HsWrapper, result)
-- The expression has type: spec_ty -> expected_ty
-- mention the *instantiated* tyvar names, so that we get a
-- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
-- Hence the tiresome but innocuous fixM
- ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
+ ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
- ; span <- getSrcSpanM
- ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
+ -- Get loation from monad, not from expected_ty
+ ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
; return ((forall_tvs, theta, rho_ty), skol_info) })
#ifdef DEBUG
; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
text "expected_ty" <+> ppr expected_ty,
- text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
- text "free_tvs" <+> ppr free_tvs,
- text "forall_tvs" <+> ppr forall_tvs])
+ text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho',
+ text "free_tvs" <+> ppr free_tvs])
#endif
-- Type-check the arg and unify with poly type
- ; (result, lie) <- getLIE (thing_inside rho_ty)
+ ; (result, lie) <- getLIE (thing_inside tvs' rho')
-- Check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
-- Conclusion: include the free vars of the expected_ty in the
-- list of "free vars" for the signature check.
- ; dicts <- newDictBndrsO (SigOrigin skol_info) theta
- ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
+ ; loc <- getInstLoc (SigOrigin skol_info)
+ ; dicts <- newDictBndrs loc theta'
+ ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
- ; checkSigTyVarsWrt free_tvs forall_tvs
+ ; checkSigTyVarsWrt free_tvs tvs'
; traceTc (text "tcGen:done")
; let
-- The WpLet binds any Insts which came out of the simplification.
dict_ids = map instToId dicts
- co_fn = mkWpTyLams forall_tvs <.> mkWpLams dict_ids <.> WpLet inst_binds
+ co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds
; returnM (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
- sig_msg = ptext SLIT("expected type of an expression")
\end{code}
go _ ty1@(ForAllTy _ _) ty2@(ForAllTy _ _)
| length tvs1 == length tvs2
= do { tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
+ -- Get location from monad, not from tvs1
; let tys = mkTyVarTys tvs
in_scope = mkInScopeSet (mkVarSet tvs)
subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys)
k1_sub_k2 = k1 `isSubKind` k2
k2_sub_k1 = k2 `isSubKind` k1
- nicer_to_update_tv1 = isSystemName (varName tv1)
+ nicer_to_update_tv1 = isSystemName (Var.varName tv1)
-- Try to update sys-y type variables in preference to ones
-- gotten (say) by instantiating a polymorphic function with
-- a user-written type sig
unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') }
+unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }
\end{code}
projects / ghc-hetmet.git / blobdiff