-\begin{code}
-tcTySig :: (Name -> PragmaInfo)
- -> RenamedSig
- -> TcM s (TcSigInfo s)
-
-tcTySig prag_info_fn (Sig v ty src_loc)
- = tcAddSrcLoc src_loc $
- tcHsType ty `thenTc` \ sigma_ty ->
-
- -- Convert from Type to TcType
- tcInstSigType sigma_ty `thenNF_Tc` \ sigma_tc_ty ->
- let
- poly_id = mkUserId v sigma_tc_ty (prag_info_fn v)
- in
- -- Instantiate this type
- -- It's important to do this even though in the error-free case
- -- we could just split the sigma_tc_ty (since the tyvars don't
- -- unified with anything). But in the case of an error, when
- -- the tyvars *do* get unified with something, we want to carry on
- -- typechecking the rest of the program with the function bound
- -- to a pristine type, namely sigma_tc_ty
- tcInstSigTcType sigma_tc_ty `thenNF_Tc` \ (tyvars, rho) ->
- let
- (theta, tau) = splitRhoTy rho
- -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
- -- wherever possible, which can improve interface files.
- in
- returnTc (TySigInfo v poly_id tyvars theta tau src_loc)
-\end{code}
-
-@checkSigMatch@ does the next step in checking signature matching.
-The tau-type part has already been unified. What we do here is to
-check that this unification has not over-constrained the (polymorphic)
-type variables of the original signature type.
-
-The error message here is somewhat unsatisfactory, but it'll do for
-now (ToDo).
-
-\begin{code}
-checkSigMatch []
- = returnTc (error "checkSigMatch")
-
-checkSigMatch tc_ty_sigs@( sig1@(TySigInfo _ id1 _ theta1 _ _) : all_sigs_but_first )
- = -- CHECK THAT THE SIGNATURE TYVARS AND TAU_TYPES ARE OK
- -- Doesn't affect substitution
- mapTc check_one_sig tc_ty_sigs `thenTc_`
-
- -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
- -- 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.
- -- ToDo: amplify
- mapTc check_one_cxt all_sigs_but_first `thenTc_`
-
- returnTc theta1
- where
- sig1_dict_tys = mk_dict_tys theta1
- n_sig1_dict_tys = length sig1_dict_tys
-
- check_one_cxt sig@(TySigInfo _ id _ theta _ src_loc)
- = tcAddSrcLoc src_loc $
- tcAddErrCtxt (sigContextsCtxt id1 id) $
- checkTc (length this_sig_dict_tys == n_sig1_dict_tys)
- sigContextsErr `thenTc_`
- unifyTauTyLists sig1_dict_tys this_sig_dict_tys
- where
- this_sig_dict_tys = mk_dict_tys theta
-
- check_one_sig (TySigInfo name id sig_tyvars _ sig_tau src_loc)
- = tcAddSrcLoc src_loc $
- tcAddErrCtxt (sigCtxt id) $
- checkSigTyVars sig_tyvars sig_tau
-
- mk_dict_tys theta = [mkDictTy c ts | (c,ts) <- theta]
-\end{code}
-
-
-@checkSigTyVars@ is used after the type in a type signature has been unified with
-the actual type found. It then checks that the type variables of the type signature
-are
- (a) still all type variables
- eg matching signature [a] against inferred type [(p,q)]
- [then a will be unified to a non-type variable]
-
- (b) still all distinct
- eg matching signature [(a,b)] against inferred type [(p,p)]
- [then a and b will be unified together]
-
- (c) not mentioned in the environment
- eg the signature for f in this:
-
- g x = ... where
- f :: a->[a]
- f y = [x,y]
-
- Here, f is forced to be monorphic by the free occurence of x.
-
-Before doing this, the substitution is applied to the signature type variable.
-
-We used to have the notion of a "DontBind" type variable, which would
-only be bound to itself or nothing. Then points (a) and (b) were
-self-checking. But it gave rise to bogus consequential error messages.
-For example:
-
- f = (*) -- Monomorphic
-
- g :: Num a => a -> a
- g x = f x x
-
-Here, we get a complaint when checking the type signature for g,
-that g isn't polymorphic enough; but then we get another one when
-dealing with the (Num x) context arising from f's definition;
-we try to unify x with Int (to default it), but find that x has already
-been unified with the DontBind variable "a" from g's signature.
-This is really a problem with side-effecting unification; we'd like to
-undo g's effects when its type signature fails, but unification is done
-by side effect, so we can't (easily).
-
-So we revert to ordinary type variables for signatures, and try to
-give a helpful message in checkSigTyVars.
-
-\begin{code}
-checkSigTyVars :: [TcTyVar s] -- The original signature type variables
- -> TcType s -- signature type (for err msg)
- -> TcM s [TcTyVar s] -- Zonked signature type variables
+ tc_mb_pats (AndMonoBinds mb1 mb2)
+ = tc_mb_pats mb1 `thenM` \ (complete_it1, xve1) ->
+ tc_mb_pats mb2 `thenM` \ (complete_it2, xve2) ->
+ let
+ complete_it = complete_it1 `thenM` \ (mb1', bs1) ->
+ complete_it2 `thenM` \ (mb2', bs2) ->
+ returnM (AndMonoBinds mb1' mb2', bs1 `unionBags` bs2)
+ in
+ returnM (complete_it, xve1 `unionBags` xve2)
+
+ tc_mb_pats (FunMonoBind name inf matches locn)
+ -- Three cases:
+ -- a) Type sig supplied
+ -- b) No type sig and recursive
+ -- c) No type sig and non-recursive
+
+ | Just sig <- maybeSig tc_ty_sigs name
+ = let -- (a) There is a type signature
+ -- Use it for the environment extension, and check
+ -- the RHS has the appropriate type (with outer for-alls stripped off)
+ mono_id = tcSigMonoId sig
+ mono_ty = idType mono_id
+ complete_it = addSrcLoc locn $
+ tcMatchesFun name matches (Check mono_ty) `thenM` \ matches' ->
+ returnM (FunMonoBind mono_id inf matches' locn,
+ unitBag (name, mono_id))
+ in
+ returnM (complete_it, if isRec is_rec then unitBag (name,tcSigPolyId sig)
+ else emptyBag)
+
+ | isRec is_rec
+ = -- (b) No type signature, and recursive
+ -- So we must use an ordinary H-M type variable
+ -- which means the variable gets an inferred tau-type
+ newLocalName name `thenM` \ mono_name ->
+ newTyVarTy openTypeKind `thenM` \ mono_ty ->
+ let
+ mono_id = mkLocalId mono_name mono_ty
+ complete_it = addSrcLoc locn $
+ tcMatchesFun name matches (Check mono_ty) `thenM` \ matches' ->
+ returnM (FunMonoBind mono_id inf matches' locn,
+ unitBag (name, mono_id))
+ in
+ returnM (complete_it, unitBag (name, mono_id))
+
+ | otherwise -- (c) No type signature, and non-recursive
+ = let -- So we can use a 'hole' type to infer a higher-rank type
+ complete_it
+ = addSrcLoc locn $
+ newHole `thenM` \ hole ->
+ tcMatchesFun name matches (Infer hole) `thenM` \ matches' ->
+ readMutVar hole `thenM` \ fun_ty ->
+ newLocalName name `thenM` \ mono_name ->
+ let
+ mono_id = mkLocalId mono_name fun_ty
+ in
+ returnM (FunMonoBind mono_id inf matches' locn,
+ unitBag (name, mono_id))
+ in
+ returnM (complete_it, emptyBag)
+
+ tc_mb_pats bind@(PatMonoBind pat grhss locn)
+ = addSrcLoc locn $