Move zonking out of tcFamTyPats

In tcFamTyPats we were zonking from the TcType world to the
Type world, ready to build the results into a CoAxiom (which
should have no TcType stuff.  But the 'thing_inside' for
tcFamTyPats also must be zonked, and that zonking must have
the ZonkEnv from the binders zonked tcFamTyPats.

Ugh.  This caused an assertion failure (with DEBUG on) in
RaeBlobPost and TypeLevelVec, both in tests/dependent, as
shown in Trac #12682.  Why it hasn't shown up before now
is obscure to me.

So I moved the zonking stuff out of tcFamTyPats to its
three call sites, where we can do it all together. Very
slightly longer, but much more robust.

2 files changed, 47 insertions, 31 deletions

diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 2e7104cef8..a0bbb836fd 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -21,7 +21,8 @@ import TcClassDcl( tcClassDecl2, tcATDefault,
 import TcSigs
 import TcRnMonad
 import TcValidity
-import TcHsSyn    ( zonkTcTypeToTypes, emptyZonkEnv )
+import TcHsSyn    ( zonkTyBndrsX, emptyZonkEnv
+                  , zonkTcTypeToTypes, zonkTcTypeToType )
 import TcMType
 import TcType
 import BuildTyCl
@@ -623,22 +624,21 @@ tcDataFamInstDecl mb_clsinfo
          -- Kind check type patterns
        ; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
                      (kcDataDefn (unLoc fam_tc_name) pats defn) $
-           \tvs' pats' res_kind -> do
-       {
-         -- Check that left-hand sides are ok (mono-types, no type families,
-         -- consistent instantiations, etc)
-       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats'
+             \tvs pats res_kind ->
+    do { stupid_theta <- solveEqualities $ tcHsContext ctxt
 
-         -- Result kind must be '*' (otherwise, we have too few patterns)
-       ; checkTc (isLiftedTypeKind res_kind) $ tooFewParmsErr (tyConArity fam_tc)
+            -- Zonk the patterns etc into the Type world
+       ; (ze, tvs')    <- zonkTyBndrsX emptyZonkEnv tvs
+       ; pats'         <- zonkTcTypeToTypes ze pats
+       ; res_kind'     <- zonkTcTypeToType  ze res_kind
+       ; stupid_theta' <- zonkTcTypeToTypes ze stupid_theta
 
-       ; stupid_theta <- solveEqualities $ tcHsContext ctxt
-       ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv stupid_theta
-       ; gadt_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
+       ; gadt_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta' cons
 
          -- Construct representation tycon
        ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
        ; axiom_name  <- newFamInstAxiomName fam_tc_name [pats']
+
        ; let (eta_pats, etad_tvs) = eta_reduce pats'
              eta_tvs              = filterOut (`elem` etad_tvs) tvs'
              full_tvs             = eta_tvs ++ etad_tvs
@@ -680,6 +680,14 @@ tcDataFamInstDecl mb_clsinfo
               ; return (rep_tc, axiom) }
 
          -- Remember to check validity; no recursion to worry about here
+         -- Check that left-hand sides are ok (mono-types, no type families,
+         -- consistent instantiations, etc)
+       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats'
+
+         -- Result kind must be '*' (otherwise, we have too few patterns)
+       ; checkTc (isLiftedTypeKind res_kind') $
+         tooFewParmsErr (tyConArity fam_tc)
+
        ; checkValidTyCon rep_tc
 
        ; let m_deriv_info = case derivs of
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 04da5f21e7..155396f4b7 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -954,6 +954,7 @@ tcDataDefn roles_info
                                   stupid_theta tc_rhs
                                   (VanillaAlgTyCon tc_rep_nm)
                                   gadt_syntax) }
+       ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
        ; return tycon }
   where
     mk_tc_rhs is_boot tycon data_cons
@@ -1056,16 +1057,19 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
           -- are different.
        ; (pats', rhs_ty)
            <- tcFamTyPats shape Nothing pats
-              (discardResult . tcCheckLHsType rhs) $ \_ pats' rhs_kind ->
+              (discardResult . tcCheckLHsType rhs) $ \tvs pats rhs_kind ->
               do { rhs_ty <- solveEqualities $
                              tcCheckLHsType rhs rhs_kind
-                 ; return (pats', rhs_ty) }
-       -- pats' is fully zonked already
-       ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
+
+                     -- Zonk the patterns etc into the Type world
+                 ; (ze, _) <- zonkTyBndrsX emptyZonkEnv tvs
+                 ; pats'   <- zonkTcTypeToTypes ze pats
+                 ; rhs_ty'  <- zonkTcTypeToType ze rhs_ty
+                 ; return (pats', rhs_ty') }
 
          -- See Note [Type-checking default assoc decls]
        ; case tcMatchTys pats' (mkTyVarTys (tyConTyVars fam_tc)) of
-           Just subst -> return ( Just (substTyUnchecked subst rhs_ty, loc) )
+           Just subst -> return (Just (substTyUnchecked subst rhs_ty, loc) )
            Nothing    -> failWithTc (defaultAssocKindErr fam_tc)
            -- We check for well-formedness and validity later,
            -- in checkValidClass
@@ -1114,13 +1118,17 @@ tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo
                      , tfe_rhs   = hs_ty }))
   = ASSERT( fam_tc_name == eqn_tc_name )
     setSrcSpan loc $
-    tcFamTyPats fam_tc_shape mb_clsinfo pats (discardResult . (tcCheckLHsType hs_ty)) $
-       \tvs' pats' res_kind ->
+    tcFamTyPats fam_tc_shape mb_clsinfo pats
+                (discardResult . (tcCheckLHsType hs_ty)) $
+                    \tvs pats res_kind ->
     do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
-       ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
+
+       ; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
+       ; pats'      <- zonkTcTypeToTypes ze pats
+       ; rhs_ty'    <- zonkTcTypeToType ze rhs_ty
        ; traceTc "tcTyFamInstEqn" (ppr fam_tc_name <+> pprTvBndrs tvs')
           -- don't print out the pats here, as they might be zonked inside the knot
-       ; return (mkCoAxBranch tvs' [] pats' rhs_ty
+       ; return (mkCoAxBranch tvs' [] pats' rhs_ty'
                               (map (const Nominal) tvs')
                               loc) }
 
@@ -1239,11 +1247,12 @@ tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo
 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
 tcFamTyPats :: FamTyConShape
             -> Maybe ClsInstInfo
-            -> HsTyPats Name          -- patterns
+            -> HsTyPats Name         -- patterns
             -> (TcKind -> TcM ())    -- kind-checker for RHS
-            -> (   [TyVar]           -- Kind and type variables
+            -> (   [TcTyVar]         -- Kind and type variables
                 -> [TcType]          -- Kind and type arguments
-                -> Kind -> TcM a)  -- NB: You can use solveEqualities here.
+                -> TcKind
+                -> TcM a)            -- NB: You can use solveEqualities here.
             -> TcM a
 tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
   = do { (typats, res_kind)
@@ -1279,15 +1288,14 @@ tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
            -- above would fail. TODO (RAE): Update once the solveEqualities
            -- bit is cleverer.
 
-            -- Zonk the patterns etc into the Type world
-       ; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
-       ; typats'      <- zonkTcTypeToTypes ze typats
-       ; res_kind'    <- zonkTcTypeToType  ze res_kind
+       ; traceTc "tcFamTyPats" (ppr name $$ ppr typats $$ ppr qtkvs)
+            -- Don't print out too much, as we might be in the knot
 
-       ; traceTc "tcFamTyPats" (ppr name $$ ppr typats)
-            -- don't print out too much, as we might be in the knot
-       ; tcExtendTyVarEnv qtkvs' $
-         thing_inside qtkvs' typats' res_kind' }
+       ; tcExtendTyVarEnv qtkvs $
+            -- Extend envt with TcTyVars not TyVars, because the
+            -- kind checking etc done by thing_inside does not expect
+            -- to encounter TyVars; it expects TcTyVars
+         thing_inside qtkvs typats res_kind }
 
 {-
 Note [Constraints in patterns]