+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
+-- context, and we want to share type variables for that context, so that
+-- all the right hand sides agree a common vocabulary for their type
+-- constraints
+tcTySigs [] = return []
+
+tcTySigs sigs
+ = do { (tc_sig1 : tc_sigs) <- mappM tcTySig 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
+ ; (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
+ -- of nested type synonyms. See Note [Scoped] with TcSigInfo.)
+ scoped_names = case ty of
+ L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
+ other -> []
+
+ ; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
+ sig_tvs = tvs, sig_theta = theta, sig_tau = tau,
+ sig_loc = loc }) }
+\end{code}
+
+\begin{code}
+generalise :: TopLevelFlag -> Bool -> [MonoBindInfo] -> [TcSigInfo] -> [Inst]
+ -> TcM ([TcTyVar], TcDictBinds, [TcId])
+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)
+ (restrictedBindCtxtErr bndr_names)
+
+ -- Now simplify with exactly that set of tyvars
+ -- We have to squash those Methods
+ ; (qtvs, binds) <- tcSimplifyRestricted doc top_lvl bndr_names
+ tau_tvs lie_req
+
+ -- Check that signature type variables are OK
+ ; final_qtvs <- checkSigsTyVars qtvs sigs
+
+ ; return (final_qtvs, binds, []) }
+
+ | null sigs -- UNRESTRICTED CASE, NO TYPE SIGS
+ = tcSimplifyInfer doc tau_tvs lie_req
+
+ | otherwise -- UNRESTRICTED CASE, WITH TYPE SIGS
+ = do { let sig1 = head sigs
+ ; sig_lie <- newDictsAtLoc (sig_loc sig1) (sig_theta sig1)
+ ; let -- The "sig_avails" is the stuff available. We get that from
+ -- the context of the type signature, BUT ALSO the lie_avail
+ -- so that polymorphic recursion works right (see comments at end of fn)
+ local_meths = [mkMethInst sig mono_id | (_, Just sig, mono_id) <- mono_infos]
+ sig_avails = sig_lie ++ local_meths
+
+ -- Check that the needed dicts can be
+ -- expressed in terms of the signature ones
+ ; (forall_tvs, dict_binds) <- tcSimplifyInferCheck doc tau_tvs sig_avails lie_req
+
+ -- Check that signature type variables are OK
+ ; final_qtvs <- checkSigsTyVars forall_tvs sigs
+
+ ; returnM (final_qtvs, dict_binds, map instToId sig_lie) }
+
+ where
+ bndr_names = bndrNames mono_infos
+ tau_tvs = foldr (unionVarSet . tyVarsOfType . getMonoType) emptyVarSet mono_infos
+ 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
+
+checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
+checkSigsTyVars qtvs sigs
+ = 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_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.
projects / ghc-hetmet.git / blobdiff