Commit cf1a0f97 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent cdac487b
......@@ -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
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%************************************************************************
%* *
......
......@@ -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
......
%
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]
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -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
......
......@@ -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
......
......@@ -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'
......
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)
......@@ -416,3 +416,4 @@ test('T8563', normal, compile, [''])
test('T8565', normal, compile, [''])
test('T8644', normal, compile, [''])
test('T8762', normal, compile, [''])
test('MutRec', normal, compile, [''])
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