Commit b8c98e4e authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

Improve error reporting for SigTvs, and add comments

parent 39fd94e2
...@@ -1041,9 +1041,15 @@ tcInstSig_maybe sig_fn name ...@@ -1041,9 +1041,15 @@ tcInstSig_maybe sig_fn name
tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo
-- Instantiate the signature, with either skolems or meta-type variables -- Instantiate the signature, with either skolems or meta-type variables
-- depending on the use_skols boolean -- depending on the use_skols boolean. This variable is set True
-- when we are typechecking a single function binding; and False for
-- pattern bindigs and a group of several function bindings.
-- Reason: in the latter cases, the "skolems" can be unified together,
-- so they aren't properly rigid in the type-refinement sense.
-- NB: unless we are doing H98, each function with a sig will be done
-- separately, even if it's mutually recursive, so use_skols will be True
-- --
-- We always instantiate with freshs uniques, -- We always instantiate with fresh uniques,
-- although we keep the same print-name -- although we keep the same print-name
-- --
-- type T = forall a. [a] -> [a] -- type T = forall a. [a] -> [a]
......
...@@ -284,14 +284,14 @@ The trouble is that the occurrences of z in the RHS force a* and b* to ...@@ -284,14 +284,14 @@ The trouble is that the occurrences of z in the RHS force a* and b* to
be the *same*, so we can't make them into skolem constants that don't unify be the *same*, so we can't make them into skolem constants that don't unify
with each other. Alas. with each other. Alas.
On the other hand, we *must* use skolems for signature type variables,
becuase GADT type refinement refines skolems only.
One solution would be insist that in the above defn the programmer uses One solution would be insist that in the above defn the programmer uses
the same type variable in both type signatures. But that takes explanation. the same type variable in both type signatures. But that takes explanation.
The alternative (currently implemented) is to have a special kind of skolem The alternative (currently implemented) is to have a special kind of skolem
constant, SigSkokTv, which can unify with other SigSkolTvs. constant, SigTv, which can unify with other SigTvs. These are *not* treated
as righd for the purposes of GADTs. And they are used *only* for pattern
bindings and mutually recursive function bindings. See the function
TcBinds.tcInstSig, and its use_skols parameter.
\begin{code} \begin{code}
...@@ -420,15 +420,23 @@ pprUserTypeCtxt SpecInstCtxt = ptext SLIT("a SPECIALISE instance pragma") ...@@ -420,15 +420,23 @@ pprUserTypeCtxt SpecInstCtxt = ptext SLIT("a SPECIALISE instance pragma")
tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar) tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
-- Tidy the type inside a GenSkol, preparatory to printing it -- Tidy the type inside a GenSkol, preparatory to printing it
tidySkolemTyVar env tv tidySkolemTyVar env tv
= ASSERT( isSkolemTyVar tv ) = ASSERT( isSkolemTyVar tv || isSigTyVar tv )
(env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1) (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
where where
(env1, info1) = case tcTyVarDetails tv of (env1, info1) = case tcTyVarDetails tv of
SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc)) SkolemTv info -> (env1, SkolemTv info')
where
(env1, info') = tidy_skol_info env info
MetaTv (SigTv info) box -> (env1, MetaTv (SigTv info') box)
where
(env1, info') = tidy_skol_info env info
info -> (env, info)
tidy_skol_info env (GenSkol tvs ty loc) = (env2, GenSkol tvs1 ty1 loc)
where where
(env1, tvs1) = tidyOpenTyVars env tvs (env1, tvs1) = tidyOpenTyVars env tvs
(env2, ty1) = tidyOpenType env1 ty (env2, ty1) = tidyOpenType env1 ty
info -> (env, info) tidy_skol_info env info = (env, info)
pprSkolTvBinding :: TcTyVar -> SDoc pprSkolTvBinding :: TcTyVar -> SDoc
-- Print info about the binding of a skolem tyvar, -- Print info about the binding of a skolem tyvar,
......
...@@ -48,9 +48,9 @@ import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType, ...@@ -48,9 +48,9 @@ import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType,
tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys, tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
typeKind, mkForAllTys, mkAppTy, isBoxyTyVar, typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
exactTyVarsOfType, tcView, exactTyVarsOfType,
tidyOpenType, tidyOpenTyVar, tidyOpenTyVars, tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView, pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar,
TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst,
substTy, substTheta, substTy, substTheta,
lookupTyVar, extendTvSubst ) lookupTyVar, extendTvSubst )
...@@ -1501,8 +1501,8 @@ ppr_ty env ty ...@@ -1501,8 +1501,8 @@ ppr_ty env ty
simple_result = (env1, quotes (ppr tidy_ty), empty) simple_result = (env1, quotes (ppr tidy_ty), empty)
; case tidy_ty of ; case tidy_ty of
TyVarTy tv TyVarTy tv
| isSkolemTyVar tv -> return (env2, pp_rigid tv', | isSkolemTyVar tv || isSigTyVar tv
pprSkolTvBinding tv') -> return (env2, pp_rigid tv', pprSkolTvBinding tv')
| otherwise -> return simple_result | otherwise -> return simple_result
where where
(env2, tv') = tidySkolemTyVar env1 tv (env2, tv') = tidySkolemTyVar env1 tv
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment