import TcRnMonad
import Inst ( InstOrigin(..), newDictsAtLoc, newIPDict, instToId )
-import TcEnv ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, newLocalName, tcLookupLocalIds )
-import TcUnify ( Expected(..), tcInfer, checkSigTyVars, sigCtxt )
+import TcEnv ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2,
+ newLocalName, tcLookupLocalIds, pprBinders,
+ tcGetGlobalTyVars )
+import TcUnify ( Expected(..), tcInfer, unifyTheta,
+ bleatEscapedTvs, sigCtxt )
import TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted,
tcSimplifyToDicts, tcSimplifyIPs )
import TcHsType ( tcHsSigType, UserTypeCtxt(..), tcAddLetBoundTyVars,
)
import TcPat ( tcPat, PatCtxt(..) )
import TcSimplify ( bindInstsOfLocalFuns )
-import TcMType ( newTyFlexiVarTy, tcSkolType, zonkQuantifiedTyVar, zonkTcTypes )
+import TcMType ( newTyFlexiVarTy, zonkQuantifiedTyVar,
+ tcInstSigType, zonkTcTypes, zonkTcTyVar )
import TcType ( TcTyVar, SkolemInfo(SigSkol),
TcTauType, TcSigmaType,
- TvSubstEnv, mkTvSubst, substTheta, substTy,
mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType,
- mkForAllTy, isUnLiftedType, tcGetTyVar_maybe,
- mkTyVarTys )
-import Unify ( tcMatchPreds )
+ mkForAllTy, isUnLiftedType, tcGetTyVar,
+ mkTyVarTys, tidyOpenTyVar, tidyOpenType )
import Kind ( argTypeKind )
-import VarEnv ( lookupVarEnv )
+import VarEnv ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv )
import TysPrim ( alphaTyVar )
import Id ( mkLocalId, mkSpecPragmaId, setInlinePragma )
import Var ( idType, idName )
import SrcLoc ( Located(..), unLoc, noLoc, getLoc )
import Bag
import Util ( isIn )
-import Maybes ( orElse )
import BasicTypes ( TopLevelFlag(..), RecFlag(..), isNonRec, isRec,
isNotTopLevel, isAlwaysActive )
import FiniteMap ( listToFM, lookupFM )
-- TODO: location a bit awkward, but the mbinds have been
-- dependency analysed and may no longer be adjacent
addErrCtxt (genCtxt (bndrNames mono_bind_infos)) $
- generalise is_unres mono_bind_infos tc_ty_sigs lie_req
+ generalise top_lvl is_unres mono_bind_infos tc_ty_sigs lie_req
-- FINALISE THE QUANTIFIED TYPE VARIABLES
-- The quantified type variables often include meta type variables
; binds' <- tcExtendTyVarEnv2 rhs_tvs $
tcExtendIdEnv2 rhs_id_env $
+ traceTc (text "tcMonoBinds" <+> vcat [ppr n <+> ppr id <+> ppr (idType id) | (n,id) <- rhs_id_env]) `thenM_`
mapBagM (wrapLocM tcRhs) tc_binds
; return (binds', mono_info) }
where
%* *
%************************************************************************
+Type signatures are tricky. See Note [Signature skolems] in TcType
+
\begin{code}
tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
-- The trick here is that all the signatures should have the same
tcTySigs sigs
= do { (tc_sig1 : tc_sigs) <- mappM tcTySig sigs
- ; tc_sigs' <- mapM (checkSigCtxt tc_sig1) tc_sigs
- ; return (tc_sig1 : tc_sigs') }
+ ; mapM (check_ctxt tc_sig1) tc_sigs
+ ; return (tc_sig1 : tc_sigs) }
+ where
+ -- Check tha all the signature contexts are the same
+ -- The type signatures on a mutually-recursive group of definitions
+ -- must all have the same context (or none).
+ --
+ -- We unify them because, with polymorphic recursion, their types
+ -- might not otherwise be related. This is a rather subtle issue.
+ check_ctxt :: TcSigInfo -> TcSigInfo -> TcM ()
+ check_ctxt sig1@(TcSigInfo { sig_theta = theta1 }) sig@(TcSigInfo { sig_theta = theta })
+ = setSrcSpan (instLocSrcSpan (sig_loc sig)) $
+ addErrCtxt (sigContextsCtxt sig1 sig) $
+ unifyTheta theta1 theta
+
tcTySig :: LSig Name -> TcM TcSigInfo
tcTySig (L span (Sig (L _ name) ty))
= setSrcSpan span $
do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty
- ; let rigid_info = SigSkol name
- poly_id = mkLocalId name sigma_ty
+ ; (tvs, theta, tau) <- tcInstSigType name sigma_ty
+ ; loc <- getInstLoc (SigOrigin (SigSkol name))
+
+ ; let poly_id = mkLocalId name sigma_ty
-- The scoped names are the ones explicitly mentioned
-- in the HsForAll. (There may be more in sigma_ty, because
L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
other -> []
- ; (tvs, theta, tau) <- tcSkolType rigid_info sigma_ty
- ; loc <- getInstLoc (SigOrigin rigid_info)
; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
sig_tvs = tvs, sig_theta = theta, sig_tau = tau,
sig_loc = loc }) }
-
-checkSigCtxt :: TcSigInfo -> TcSigInfo -> TcM TcSigInfo
-checkSigCtxt sig1 sig@(TcSigInfo { sig_tvs = tvs, sig_theta = theta, sig_tau = tau })
- = -- Try to match the context of this signature with
- -- that of the first signature
- case tcMatchPreds (sig_tvs sig) (sig_theta sig) (sig_theta sig1) of {
- Nothing -> bale_out ;
- Just tenv ->
-
- case check_tvs tenv tvs of {
- Nothing -> bale_out ;
- Just tvs' ->
-
- let
- subst = mkTvSubst tenv
- in
- return (sig { sig_tvs = tvs',
- sig_theta = substTheta subst theta,
- sig_tau = substTy subst tau }) }}
-
- where
- bale_out = setSrcSpan (instLocSrcSpan (sig_loc sig)) $
- failWithTc $
- sigContextsErr (sig_id sig1) (sig_id sig)
-
- -- Rather tedious check that the type variables
- -- have been matched only with another type variable,
- -- and that two type variables have not been matched
- -- with the same one
- -- A return of Nothing indicates that one of the bad
- -- things has happened
- check_tvs :: TvSubstEnv -> [TcTyVar] -> Maybe [TcTyVar]
- check_tvs tenv [] = Just []
- check_tvs tenv (tv:tvs)
- = do { let ty = lookupVarEnv tenv tv `orElse` mkTyVarTy tv
- ; tv' <- tcGetTyVar_maybe ty
- ; tvs' <- check_tvs tenv tvs
- ; if tv' `elem` tvs'
- then Nothing
- else Just (tv':tvs') }
\end{code}
\begin{code}
-generalise :: Bool -> [MonoBindInfo] -> [TcSigInfo] -> [Inst]
+generalise :: TopLevelFlag -> Bool -> [MonoBindInfo] -> [TcSigInfo] -> [Inst]
-> TcM ([TcTyVar], TcDictBinds, [TcId])
-generalise is_unrestricted mono_infos sigs lie_req
+generalise top_lvl is_unrestricted mono_infos sigs lie_req
| not is_unrestricted -- RESTRICTED CASE
= -- Check signature contexts are empty
do { checkTc (all is_mono_sig sigs)
-- Now simplify with exactly that set of tyvars
-- We have to squash those Methods
- ; (qtvs, binds) <- tcSimplifyRestricted doc tau_tvs lie_req
+ ; (qtvs, binds) <- tcSimplifyRestricted doc top_lvl bndr_names
+ tau_tvs lie_req
-- Check that signature type variables are OK
; final_qtvs <- checkSigsTyVars qtvs sigs
is_mono_sig sig = null (sig_theta sig)
doc = ptext SLIT("type signature(s) for") <+> pprBinders bndr_names
-mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs,
- sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id
- = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc
+ mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs,
+ sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id
+ = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc
checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
checkSigsTyVars qtvs sigs
- = mappM check_one sigs `thenM` \ sig_tvs_s ->
- let
- -- Sigh. Make sure that all the tyvars in the type sigs
- -- appear in the returned ty var list, which is what we are
- -- going to generalise over. Reason: we occasionally get
- -- silly types like
- -- type T a = () -> ()
- -- f :: T a
- -- f () = ()
- -- Here, 'a' won't appear in qtvs, so we have to add it
-
- sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
- all_tvs = extendVarSetList sig_tvs qtvs
- in
- returnM (varSetElems all_tvs)
+ = do { gbl_tvs <- tcGetGlobalTyVars
+ ; sig_tvs_s <- mappM (check_sig gbl_tvs) sigs
+
+ ; let -- Sigh. Make sure that all the tyvars in the type sigs
+ -- appear in the returned ty var list, which is what we are
+ -- going to generalise over. Reason: we occasionally get
+ -- silly types like
+ -- type T a = () -> ()
+ -- f :: T a
+ -- f () = ()
+ -- Here, 'a' won't appear in qtvs, so we have to add it
+ sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
+ all_tvs = varSetElems (extendVarSetList sig_tvs qtvs)
+ ; returnM all_tvs }
where
- check_one (TcSigInfo {sig_id = id, sig_tvs = tvs, sig_theta = theta, sig_tau = tau})
- = addErrCtxt (ptext SLIT("In the type signature for")
- <+> quotes (ppr id)) $
- addErrCtxtM (sigCtxt id tvs theta tau) $
- do { checkSigTyVars tvs; return tvs }
-\end{code}
+ check_sig gbl_tvs (TcSigInfo {sig_id = id, sig_tvs = tvs,
+ sig_theta = theta, sig_tau = tau})
+ = addErrCtxt (ptext SLIT("In the type signature for") <+> quotes (ppr id)) $
+ addErrCtxtM (sigCtxt id tvs theta tau) $
+ do { tvs' <- checkDistinctTyVars tvs
+ ; ifM (any (`elemVarSet` gbl_tvs) tvs')
+ (bleatEscapedTvs gbl_tvs tvs tvs')
+ ; return tvs' }
+
+checkDistinctTyVars :: [TcTyVar] -> TcM [TcTyVar]
+-- (checkDistinctTyVars tvs) checks that the tvs from one type signature
+-- are still all type variables, and all distinct from each other.
+-- It returns a zonked set of type variables.
+-- For example, if the type sig is
+-- f :: forall a b. a -> b -> b
+-- we want to check that 'a' and 'b' haven't
+-- (a) been unified with a non-tyvar type
+-- (b) been unified with each other (all distinct)
+
+checkDistinctTyVars sig_tvs
+ = do { zonked_tvs <- mapM zonk_one sig_tvs
+ ; foldlM check_dup emptyVarEnv (sig_tvs `zip` zonked_tvs)
+ ; return zonked_tvs }
+ where
+ zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv
+ ; return (tcGetTyVar "checkDistinctTyVars" ty) }
+ -- 'ty' is bound to be a type variable, because SigSkolTvs
+ -- can only be unified with type variables
+
+ check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
+ -- The TyVarEnv maps each zonked type variable back to its
+ -- corresponding user-written signature type variable
+ check_dup acc (sig_tv, zonked_tv)
+ = case lookupVarEnv acc zonked_tv of
+ Just sig_tv' -> bomb_out sig_tv sig_tv'
+
+ Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
+
+ bomb_out sig_tv1 sig_tv2
+ = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1)
+ <+> ptext SLIT("is unified with another quantified type variable")
+ <+> ppr tidy_tv2)
+ where
+ (env1, tidy_tv1) = tidyOpenTyVar emptyTidyEnv sig_tv1
+ (_env2, tidy_tv2) = tidyOpenTyVar env1 sig_tv2
+\end{code}
+
@getTyVarsToGen@ decides what type variables to generalise over.
nest 4 (ppr v <+> dcolon <+> ppr ty)]
-----------------------------------------------
-sigContextsErr id1 id2
- = vcat [ptext SLIT("Mis-match between the contexts of the signatures for"),
+sigContextsCtxt sig1 sig2
+ = vcat [ptext SLIT("When matching the contexts of the signatures for"),
nest 2 (vcat [ppr id1 <+> dcolon <+> ppr (idType id1),
ppr id2 <+> dcolon <+> ppr (idType id2)]),
ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
+ where
+ id1 = sig_id sig1
+ id2 = sig_id sig2
-----------------------------------------------
genCtxt binder_names
= ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names
-
--- Used in error messages
--- Use quotes for a single one; they look a bit "busy" for several
-pprBinders [bndr] = quotes (ppr bndr)
-pprBinders bndrs = pprWithCommas ppr bndrs
\end{code}
projects / ghc-hetmet.git / blobdiff