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.

10 files changed, 110 insertions, 113 deletions

diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs
index 88212415c4..572874b875 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 1305437786..5725e09293 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 b5d7d2ea1d..3397b0836a 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 a40a93df16..2bed04c81c 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 ab6d7bd40c..0c8c09d54a 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 703e59dca4..94ee199d30 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 a7442fdbee..9b58b4c7d9 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 37358c9bdf..387d49c3ad 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 0000000000..1a2a01f329
--- /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 a5f853cac0..35b5dd2e90 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, [''])