Get rid of TcTyVars more assiduously

* I found a bug in 'generalize' in TcTyClsDecls.kcTyClGroup, where
  the kind variables weren't being turned into proper TyVars, so
  we got (skolem) TcTyVars in TyCons, which shouldn't happen.  Fix
  was easy.

* Similarly TcHsType.kindGeneralizeType wasn't turning the forall'd
  TcTyVars into TyVars.  To achieve this I defined TcHsTyn.zonkSigType.

* All this allowed me to remove awkward and ill-explained bit of
  footwork on DFunIds in Inst.newClsInst

This is just refactoring, but it does make the printout from
-ddump-deriv make a bit more sense by not grautuitiously cloning
type variables.  In the display I was seeing

   instance C [a_df4] where
      f x = ...a_dx5...

where actually the d_df4 and a_dx5 were the same.

4 files changed, 35 insertions, 16 deletions

diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index e5b802063b..0a50de48b0 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -638,13 +638,15 @@ newClsInst overlap_mode dfun_name tvs theta clas tys
   = do { (subst, tvs') <- freshenTyVarBndrs tvs
              -- Be sure to freshen those type variables,
              -- so they are sure not to appear in any lookup
-       ; let tys'   = substTys subst tys
-             theta' = substTheta subst theta
-             dfun   = mkDictFunId dfun_name tvs' theta' clas tys'
-             -- Substituting in the DFun type just makes sure that
-             -- we are using TyVars rather than TcTyVars
-             -- Not sure if this is really the right place to do so,
-             -- but it'll do fine
+       ; let tys' = substTys subst tys
+
+             dfun = mkDictFunId dfun_name tvs theta clas tys
+             -- The dfun uses the original 'tvs' because
+             -- (a) they don't need to be fresh
+             -- (b) they may be mentioned in the ib_binds field of
+             --     an InstInfo, and in TcEnv.pprInstInfoDetails it's
+             --     helpful to use the same names
+
        ; oflag <- getOverlapFlag overlap_mode
        ; let inst = mkLocalInstance dfun oflag tvs' clas tys'
        ; warnIf (Reason Opt_WarnOrphans)
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 618c3c067b..2589576910 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -30,7 +30,7 @@ module TcHsSyn (
         zonkTyConBinders,
         emptyZonkEnv, mkEmptyZonkEnv,
         zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
-        zonkCoToCo,
+        zonkCoToCo, zonkSigType,
         zonkEvBinds,
 
         -- * Validity checking
@@ -187,6 +187,8 @@ the environment manipulation is tiresome.
 -- Confused by zonking? See Note [What is zonking?] in TcMType.
 type UnboundTyVarZonker = TcTyVar -> TcM Type
         -- How to zonk an unbound type variable
+        -- The TcTyVar is (a) a MetaTv (b) Flexi and
+        --     (c) its kind is alrady zonked
         -- Note [Zonking the LHS of a RULE]
 
 -- | A ZonkEnv carries around several bits.
@@ -1595,6 +1597,19 @@ zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
 zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion
 zonkCoToCo = mapCoercion zonk_tycomapper
 
+zonkSigType :: TcType -> TcM Type
+-- Zonk the type obtained from a user type signature
+-- We want to turn any quantified (forall'd) variables into TyVars
+-- but we may find some free TcTyVars, and we want to leave them
+-- completely alone.  They may even have unification variables inside
+-- e.g.  f (x::a) = ...(e :: a -> a)....
+-- The type sig for 'e' mentions a free 'a' which will be a
+-- unification SigTv variable.
+zonkSigType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_tv)
+  where
+    zonk_unbound_tv :: UnboundTyVarZonker
+    zonk_unbound_tv tv = return (mkTyVarTy tv)
+
 zonkTvSkolemising :: UnboundTyVarZonker
 -- This variant is used for the LHS of rules
 -- See Note [Zonking the LHS of a RULE].
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 17bac58469..a9d90f2e3e 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -55,6 +55,7 @@ import TcUnify
 import TcIface
 import TcSimplify ( solveEqualities )
 import TcType
+import TcHsSyn( zonkSigType )
 import Inst   ( tcInstBinders, tcInstBindersX, tcInstBinderX )
 import Type
 import Kind
@@ -1543,7 +1544,9 @@ kindGeneralizeType :: Type -> TcM Type
 -- Result is zonked
 kindGeneralizeType ty
   = do { kvs <- kindGeneralize ty
-       ; zonkTcType (mkInvForAllTys kvs ty) }
+       ; ty <- zonkSigType (mkInvForAllTys kvs ty)
+       ; traceTc "kindGen" (ppr (mkInvForAllTys kvs ty) $$ ppr ty)
+       ; return ty  }
 
 kindGeneralize :: TcType -> TcM [KindVar]
 -- Quantify the free kind variables of a kind or type
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index aa6d44f65e..fefe1e9c7b 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -350,19 +350,18 @@ kcTyClGroup decls
                  kc_res_kind = tyConResKind tc
                  kc_tyvars   = tyConTyVars tc
            ; kvs <- kindGeneralize (mkTyConKind kc_binders kc_res_kind)
+           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ kc_binders
 
-           ; (env, kc_binders') <- zonkTyConBinders emptyZonkEnv kc_binders
-           ; kc_res_kind' <- zonkTcTypeToType env kc_res_kind
+           ; (env, all_binders') <- zonkTyConBinders emptyZonkEnv all_binders
+           ; kc_res_kind'        <- zonkTcTypeToType env kc_res_kind
 
                       -- Make sure kc_kind' has the final, zonked kind variables
            ; traceTc "Generalise kind" $
-             vcat [ ppr name, ppr kc_binders, ppr kc_res_kind
-                  , ppr kvs, ppr kc_binders', ppr kc_res_kind'
+             vcat [ ppr name, ppr kc_binders, ppr kvs, ppr all_binders, ppr kc_res_kind
+                  , ppr all_binders', ppr kc_res_kind'
                   , ppr kc_tyvars, ppr (tcTyConScopedTyVars tc)]
 
-           ; return (mkTcTyCon name
-                               (mkNamedTyConBinders Inferred kvs ++ kc_binders')
-                               kc_res_kind'
+           ; return (mkTcTyCon name all_binders' kc_res_kind'
                                (mightBeUnsaturatedTyCon tc)
                                (tcTyConScopedTyVars tc)) }