From 935dc721cf02e3778615d3a40d04bdae17bfef0e Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 7 Mar 2014 16:50:17 +0000
Subject: [PATCH] Fix the treatment of lexically scoped kind variables (Trac
#8856)
The issue here is described in Note [Binding scoped type variables] in
TcPat. When implementing this fix I was able to make things quite a
bit simpler:
* The type variables in a type signature now never unify
with each other, and so can be straightfoward skolems.
* We only need the SigTv stuff for signatures in patterns,
and for kind variables.
(cherry picked from commit cf1a0f971966af633fbd932ad012ce716680465b)
---
compiler/typecheck/FamInst.lhs | 2 +-
compiler/typecheck/TcBinds.lhs | 49 ++++-----------
compiler/typecheck/TcExpr.lhs | 9 ++-
compiler/typecheck/TcMType.lhs | 51 ++++++----------
compiler/typecheck/TcPat.lhs | 60 +++++++++++++++----
compiler/typecheck/TcPatSyn.lhs | 2 +-
compiler/typecheck/TcType.lhs | 36 ++++-------
compiler/vectorise/Vectorise/Generic/PData.hs | 2 +-
.../tests/typecheck/should_compile/MutRec.hs | 11 ++++
.../tests/typecheck/should_compile/all.T | 1 +
10 files changed, 110 insertions(+), 113 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_compile/MutRec.hs
diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs
index 88212415c44b..572874b875a9 100644
--- a/compiler/typecheck/FamInst.lhs
+++ b/compiler/typecheck/FamInst.lhs
@@ -60,7 +60,7 @@ newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
-- Called from the vectoriser monad too, hence the rather general type
newFamInst flavor axiom@(CoAxiom { co_ax_branches = FirstBranch branch
, co_ax_tc = fam_tc })
- = do { (subst, tvs') <- tcInstSkolTyVarsLoc loc tvs
+ = do { (subst, tvs') <- tcInstSigTyVarsLoc loc tvs
; return (FamInst { fi_fam = fam_tc_name
, fi_flavor = flavor
, fi_tcs = roughMatchTcs lhs
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 6819de01566b..4fe95a4f7559 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -9,7 +9,7 @@ module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
tcHsBootSigs, tcPolyCheck,
PragFun, tcSpecPrags, tcVectDecls, mkPragFun,
TcSigInfo(..), TcSigFun,
- instTcTySig, instTcTySigFromId,
+ instTcTySig, instTcTySigFromId, findScopedTyVars,
badBootDeclErr ) where
import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
@@ -520,7 +520,7 @@ tcPolyCheck rec_tc prag_fn
= do { ev_vars <- newEvVars theta
; let skol_info = SigSkol (FunSigCtxt (idName poly_id)) (mkPhiTy theta tau)
prag_sigs = prag_fn (idName poly_id)
- ; tvs <- mapM (skolemiseSigTv . snd) tvs_w_scoped
+ tvs = map snd tvs_w_scoped
; (ev_binds, (binds', [mono_info]))
<- setSrcSpan loc $
checkConstraints skol_info tvs ev_vars $
@@ -1162,18 +1162,6 @@ However, we do *not* support this
f :: forall a. a->a
(f,g) = e
-Note [More instantiated than scoped]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There may be more instantiated type variables than lexically-scoped
-ones. For example:
- type T a = forall b. b -> (a,b)
- f :: forall c. T c
-Here, the signature for f will have one scoped type variable, c,
-but two instantiated type variables, c' and b'.
-
-We assume that the scoped ones are at the *front* of sig_tvs,
-and remember the names from the original HsForAllTy in the TcSigFun.
-
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
When instantiating a type signature, we do so with either skolems or
@@ -1248,42 +1236,25 @@ tcTySig _ = return []
instTcTySigFromId :: SrcSpan -> Id -> TcM TcSigInfo
instTcTySigFromId loc id
- = do { (tvs, theta, tau) <- tcInstType inst_sig_tyvars (idType id)
+ = do { (tvs, theta, tau) <- tcInstType (tcInstSigTyVarsLoc loc)
+ (idType id)
; return (TcSigInfo { sig_id = id, sig_loc = loc
, sig_tvs = [(Nothing, tv) | tv <- tvs]
, sig_theta = theta, sig_tau = tau }) }
where
-- Hack: in an instance decl we use the selector id as
- -- the template; but we do *not* want the SrcSpan on the Name of
+ -- the template; but we do *not* want the SrcSpan on the Name of
-- those type variables to refer to the class decl, rather to
- -- the instance decl
- inst_sig_tyvars tvs = tcInstSigTyVars (map set_loc tvs)
- set_loc tv = setTyVarName tv (mkInternalName (nameUnique n) (nameOccName n) loc)
- where
- n = tyVarName tv
+ -- the instance decl
instTcTySig :: LHsType Name -> TcType -- HsType and corresponding TcType
-> Name -> TcM TcSigInfo
instTcTySig hs_ty@(L loc _) sigma_ty name
= do { (inst_tvs, theta, tau) <- tcInstType tcInstSigTyVars sigma_ty
- ; return (TcSigInfo { sig_id = poly_id, sig_loc = loc
- , sig_tvs = zipEqual "instTcTySig" scoped_tvs inst_tvs
+ ; return (TcSigInfo { sig_id = mkLocalId name sigma_ty
+ , sig_loc = loc
+ , sig_tvs = findScopedTyVars hs_ty sigma_ty inst_tvs
, sig_theta = theta, sig_tau = tau }) }
- where
- poly_id = mkLocalId name sigma_ty
-
- scoped_names = hsExplicitTvs hs_ty
- (sig_tvs,_) = tcSplitForAllTys sigma_ty
-
- scoped_tvs :: [Maybe Name]
- scoped_tvs = mk_scoped scoped_names sig_tvs
-
- mk_scoped :: [Name] -> [TyVar] -> [Maybe Name]
- mk_scoped [] tvs = [Nothing | _ <- tvs]
- mk_scoped (n:ns) (tv:tvs)
- | n == tyVarName tv = Just n : mk_scoped ns tvs
- | otherwise = Nothing : mk_scoped (n:ns) tvs
- mk_scoped (n:ns) [] = pprPanic "mk_scoped" (ppr name $$ ppr (n:ns) $$ ppr hs_ty $$ ppr sigma_ty)
-------------------------------
data GeneralisationPlan
@@ -1449,6 +1420,8 @@ strictBindErr flavour unlifted_bndrs binds
| otherwise = ptext (sLit "bang-pattern or unboxed-tuple bindings")
\end{code}
+Note [Binding scoped type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%************************************************************************
%* *
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index b5d7d2ea1d2f..3397b0836ab6 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -221,11 +221,14 @@ tcExpr e@(HsLamCase _ matches) res_ty
tcExpr (ExprWithTySig expr sig_ty) res_ty
= do { sig_tc_ty <- tcHsSigType ExprSigCtxt sig_ty
- -- Remember to extend the lexical type-variable environment
; (gen_fn, expr')
<- tcGen ExprSigCtxt sig_tc_ty $ \ skol_tvs res_ty ->
- tcExtendTyVarEnv2 (hsExplicitTvs sig_ty `zip` skol_tvs) $
- -- See Note [More instantiated than scoped] in TcBinds
+
+ -- Remember to extend the lexical type-variable environment
+ -- See Note [More instantiated than scoped] in TcBinds
+ tcExtendTyVarEnv2
+ [(n,tv) | (Just n, tv) <- findScopedTyVars sig_ty sig_tc_ty skol_tvs] $
+
tcMonoExprNC expr res_ty
; let inner_expr = ExprWithTySigOut (mkLHsWrap gen_fn expr') sig_ty
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index a40a93df1605..2bed04c81cb2 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -1,4 +1,4 @@
-%
+o%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
@@ -40,17 +40,17 @@ module TcMType (
--------------------------------
-- Instantiation
- tcInstTyVars, tcInstSigTyVars, newSigTyVar,
- tcInstType,
- tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVars,
- tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
+ tcInstTyVars, newSigTyVar,
+ tcInstType,
+ tcInstSkolTyVars, tcInstSuperSkolTyVars,tcInstSuperSkolTyVarsX,
+ tcInstSigTyVarsLoc, tcInstSigTyVars,
tcInstSkolTyVar, tcInstSkolType,
tcSkolDFunType, tcSuperSkolTyVars,
--------------------------------
-- Zonking
zonkTcPredType,
- skolemiseSigTv, skolemiseUnboundMetaTyVar,
+ skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
zonkQuantifiedTyVar, quantifyTyVars,
zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
@@ -238,9 +238,6 @@ tcInstSkolTyVar loc overlappable subst tyvar
-- Wrappers
-- we need to be able to do this from outside the TcM monad:
-tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
-tcInstSkolTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])
-
tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])
@@ -255,29 +252,26 @@ tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
+-- Get the location from the monad; this is a complete freshening operation
tcInstSkolTyVars' isSuperSkol subst tvs
= do { loc <- getSrcSpanM
; mapAccumLM (tcInstSkolTyVar loc isSuperSkol) subst tvs }
+tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
+-- We specify the location
+tcInstSigTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])
+
+tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
+-- Get the location from the TyVar itself, not the monad
+tcInstSigTyVars = mapAccumLM inst_tv (mkTopTvSubst [])
+ where
+ inst_tv subst tv = tcInstSkolTyVar (getSrcSpan tv) False subst tv
+
tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
-tcInstSigTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
--- Make meta SigTv type variables for patten-bound scoped type varaibles
--- We use SigTvs for them, so that they can't unify with arbitrary types
--- Precondition: tyvars should be ordered (kind vars first)
--- see Note [Kind substitution when instantiating]
-tcInstSigTyVars = mapAccumLM tcInstSigTyVar (mkTopTvSubst [])
- -- The tyvars are freshly made, by tcInstSigTyVar
- -- So mkTopTvSubst [] is ok
-
-tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
-tcInstSigTyVar subst tv
- = do { new_tv <- newSigTyVar (tyVarName tv) (substTy subst (tyVarKind tv))
- ; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }
-
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
= do { uniq <- newUnique
@@ -598,17 +592,6 @@ skolemiseUnboundMetaTyVar tv details
; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
-
-skolemiseSigTv :: TcTyVar -> TcM TcTyVar
--- In TcBinds we create SigTvs for type signatures
--- but for singleton groups we want them to really be skolems
--- which do not unify with each other
-skolemiseSigTv tv
- = ASSERT2( isSigTyVar tv, ppr tv )
- do { writeMetaTyVarRef tv (metaTvRef tv) (mkTyVarTy skol_tv)
- ; return skol_tv }
- where
- skol_tv = setTcTyVarDetails tv (SkolemTv False)
\end{code}
Note [Zonking to Skolem]
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index ab6d7bd40c42..0c8c09d54af5 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -13,7 +13,8 @@ TcPat: Typechecking patterns
-- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details
-module TcPat ( tcLetPat, TcSigFun, TcSigInfo(..), TcPragFun
+module TcPat ( tcLetPat, TcSigFun, TcPragFun
+ , TcSigInfo(..), findScopedTyVars
, LetBndrSpec(..), addInlinePrags, warnPrags
, tcPat, tcPats, newNoSigLetBndr
, addDataConStupidTheta, badFieldCon, polyPatSig ) where
@@ -29,6 +30,7 @@ import Inst
import Id
import Var
import Name
+import NameSet
import TcEnv
--import TcExpr
import TcMType
@@ -146,8 +148,7 @@ data TcSigInfo
sig_tvs :: [(Maybe Name, TcTyVar)],
-- Instantiated type and kind variables
-- Just n <=> this skolem is lexically in scope with name n
- -- See Note [Kind vars in sig_tvs]
- -- See Note [More instantiated than scoped] in TcBinds
+ -- See Note [Binding scoped type variables]
sig_theta :: TcThetaType, -- Instantiated theta
@@ -157,21 +158,56 @@ data TcSigInfo
sig_loc :: SrcSpan -- The location of the signature
}
+findScopedTyVars -- See Note [Binding scoped type variables]
+ :: LHsType Name -- The HsType
+ -> TcType -- The corresponding Type:
+ -- uses same Names as the HsType
+ -> [TcTyVar] -- The instantiated forall variables of the Type
+ -> [(Maybe Name, TcTyVar)] -- In 1-1 correspondence with the instantiated vars
+findScopedTyVars hs_ty sig_ty inst_tvs
+ = zipWith find sig_tvs inst_tvs
+ where
+ find sig_tv inst_tv
+ | tv_name `elemNameSet` scoped_names = (Just tv_name, inst_tv)
+ | otherwise = (Nothing, inst_tv)
+ where
+ tv_name = tyVarName sig_tv
+
+ scoped_names = mkNameSet (hsExplicitTvs hs_ty)
+ (sig_tvs,_) = tcSplitForAllTys sig_ty
+
instance Outputable TcSigInfo where
ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
= ppr id <+> dcolon <+> vcat [ pprSigmaType (mkSigmaTy (map snd tyvars) theta tau)
, ppr (map fst tyvars) ]
\end{code}
-Note [Kind vars in sig_tvs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-With kind polymorphism a signature like
- f :: forall f a. f a -> f a
-may actuallly give rise to
- f :: forall k. forall (f::k -> *) (a:k). f a -> f a
-So the sig_tvs will be [k,f,a], but only f,a are scoped.
-So the scoped ones are not necessarily the *inital* ones!
-
+Note [Binding scoped type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type variables *brought into lexical scope* by a type signature may
+be a subset of the *quantified type variables* of the signatures, for two reasons:
+
+* With kind polymorphism a signature like
+ f :: forall f a. f a -> f a
+ may actuallly give rise to
+ f :: forall k. forall (f::k -> *) (a:k). f a -> f a
+ So the sig_tvs will be [k,f,a], but only f,a are scoped.
+ NB: the scoped ones are not necessarily the *inital* ones!
+
+* Even aside from kind polymorphism, tere may be more instantiated
+ type variables than lexically-scoped ones. For example:
+ type T a = forall b. b -> (a,b)
+ f :: forall c. T c
+ Here, the signature for f will have one scoped type variable, c,
+ but two instantiated type variables, c' and b'.
+
+The function findScopedTyVars takes
+ * hs_ty: the original HsForAllTy
+ * sig_ty: the corresponding Type (which is guaranteed to use the same Names
+ as the HsForAllTy)
+ * inst_tvs: the skolems instantiated from the forall's in sig_ty
+It returns a [(Maybe Name, TcTyVar)], in 1-1 correspondence with inst_tvs
+but with a (Just n) for the lexically scoped name of each in-scope tyvar.
Note [sig_tau may be polymorphic]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcPatSyn.lhs b/compiler/typecheck/TcPatSyn.lhs
index 703e59dca4af..94ee199d3076 100644
--- a/compiler/typecheck/TcPatSyn.lhs
+++ b/compiler/typecheck/TcPatSyn.lhs
@@ -199,7 +199,7 @@ tc_pat_syn_wrapper_from_expr :: Located Name
-> TcM (Id, LHsBinds Id)
tc_pat_syn_wrapper_from_expr (L loc name) lexpr args univ_tvs ex_tvs theta pat_ty
= do { let qtvs = univ_tvs ++ ex_tvs
- ; (subst, qtvs') <- tcInstSigTyVars qtvs
+ ; (subst, qtvs') <- tcInstSkolTyVars qtvs
; let theta' = substTheta subst theta
pat_ty' = substTy subst pat_ty
args' = map (\arg -> setVarType arg $ substTy subst (varType arg)) args
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 55c37b9506c8..cc4ded499fa5 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -250,29 +250,19 @@ Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
- x :: [a]
- y :: b
- (x,y,z) = ([y,z], z, head x)
-
-Here, x and y have type sigs, which go into the environment. We used to
-instantiate their types with skolem constants, and push those types into
-the RHS, so we'd typecheck the RHS with type
- ( [a*], b*, c )
-where a*, b* are skolem constants, and c is an ordinary meta type varible.
-
-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
-with each other. Alas.
-
-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 alternative (currently implemented) is to have a special kind of skolem
-constant, SigTv, which can unify with other SigTvs. These are *not* treated
-as rigid 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.
-
+ f :: forall a. [a] -> Int
+ f (x::b : xs) = 3
+
+Here 'b' is a lexically scoped type variable, but it turns out to be
+the same as the skolem 'a'. So we have a special kind of skolem
+constant, SigTv, which can unify with other SigTvs. They are used
+*only* for pattern type signatures.
+
+Similarly consider
+ data T (a:k1) = MkT (S a)
+ data S (b:k2) = MkS (T b)
+When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
+because they end up unifying; we want those SigTvs again.
\begin{code}
-- A TyVarDetails is inside a TyVar
diff --git a/compiler/vectorise/Vectorise/Generic/PData.hs b/compiler/vectorise/Vectorise/Generic/PData.hs
index 37358c9bdf74..387d49c3ad91 100644
--- a/compiler/vectorise/Vectorise/Generic/PData.hs
+++ b/compiler/vectorise/Vectorise/Generic/PData.hs
@@ -45,7 +45,7 @@ buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM FamInst
buildDataFamInst name' fam_tc vect_tc rhs
= do { axiom_name <- mkDerivedName mkInstTyCoOcc name'
- ; (_, tyvars') <- liftDs $ tcInstSkolTyVarsLoc (getSrcSpan name') tyvars
+ ; (_, tyvars') <- liftDs $ tcInstSigTyVarsLoc (getSrcSpan name') tyvars
; let ax = mkSingleCoAxiom axiom_name tyvars' fam_tc pat_tys rep_ty
tys' = mkTyVarTys tyvars'
rep_ty = mkTyConApp rep_tc tys'
diff --git a/testsuite/tests/typecheck/should_compile/MutRec.hs b/testsuite/tests/typecheck/should_compile/MutRec.hs
new file mode 100644
index 000000000000..1a2a01f3291e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/MutRec.hs
@@ -0,0 +1,11 @@
+module MutRec where
+
+-- Mutual recursion with different
+-- names for the same type variable
+f t = x
+ where
+ x :: [a]
+ y :: b
+ (x,y,z,r) = ([y,z], z, head x, t)
+
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a5f853cac036..35b5dd2e9006 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -416,3 +416,4 @@ test('T8563', normal, compile, [''])
test('T8565', normal, compile, [''])
test('T8644', normal, compile, [''])
test('T8762', normal, compile, [''])
+test('MutRec', normal, compile, [''])
--
GitLab