Zonk before calling splitDepVarsOfType.

It was Utterly Wrong before.

Note to self: Never, ever take the free vars of an unzonked type.

7 files changed, 91 insertions, 46 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 34c214435d..4b61501a4b 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1442,7 +1442,7 @@ kindGeneralize :: TcType -> TcM [KindVar]
 kindGeneralize ty
   = do { gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
        ; kvs <- zonkTcTypeAndFV ty
-       ; quantifyTyVars gbl_tvs (Pair kvs emptyVarSet) }
+       ; quantifyZonkedTyVars gbl_tvs (Pair kvs emptyVarSet) }
 
 {-
 Note [Kind generalisation]
@@ -1746,6 +1746,7 @@ tcTyClTyVars :: Name -> LHsQTyVars Name      -- LHS of the type or class decl
 -- ^ Used for the type variables of a type or class decl
 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
+-- Accordingly, everything passed to the continuation is fully zonked.
 --
 -- (tcTyClTyVars T [a,b] thing_inside)
 --   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 58ff3c4042..628c9e307a 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -68,7 +68,9 @@ module TcMType (
   tidyEvVar, tidyCt, tidySkolemInfo,
   skolemiseUnboundMetaTyVar,
   zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
-  zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
+  zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
+  zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType,
+  quantifyTyVars, quantifyZonkedTyVars,
   defaultKindVar,
   zonkTcTyCoVarBndr, zonkTcTyBinder, zonkTcType, zonkTcTypes, zonkCo,
   zonkTyCoVarKind, zonkTcTypeMapper,
@@ -827,22 +829,27 @@ Note that this function can accept covars, but will never return them.
 This is because we never want to infer a quantified covar!
 -}
 
-quantifyTyVars :: TcTyCoVarSet   -- global tvs
-               -> Pair TcTyCoVarSet    -- dependent tvs       We only distinguish
-                                       -- nondependent tvs    between these for
-                                       --                     -XNoPolyKinds
-               -> TcM [TcTyVar]
+quantifyTyVars, quantifyZonkedTyVars
+  :: TcTyCoVarSet   -- global tvs
+  -> Pair TcTyCoVarSet    -- dependent tvs       We only distinguish
+                          -- nondependent tvs    between these for
+                          --                     -XNoPolyKinds
+  -> TcM [TcTyVar]
 -- See Note [quantifyTyVars]
 -- Can be given a mixture of TcTyVars and TyVars, in the case of
 --   associated type declarations. Also accepts covars, but *never* returns any.
 
+-- The zonked variant assumes everything is already zonked.
+
 quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
   = do { dep_tkvs    <- zonkTyCoVarsAndFV dep_tkvs
        ; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
                         zonkTyCoVarsAndFV nondep_tkvs
        ; gbl_tvs     <- zonkTyCoVarsAndFV gbl_tvs
+       ; quantifyZonkedTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs) }
 
-       ; let all_cvs    = filterVarSet isCoVar $
+quantifyZonkedTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
+  = do { let all_cvs    = filterVarSet isCoVar $
                           dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
              dep_kvs    = varSetElemsWellScoped $
                           dep_tkvs `minusVarSet` gbl_tvs
@@ -1137,6 +1144,11 @@ tcGetGlobalTyCoVars
        ; writeMutVar gtv_var gbl_tvs'
        ; return gbl_tvs' }
 
+-- | Zonk a type without using the smart constructors; the result type
+-- is available for inspection within the type-checking knot.
+zonkTcTypeInKnot :: TcType -> TcM TcType
+zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
+
 zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
 -- Zonk a type and take its free variables
 -- With kind polymorphism it can be essential to zonk *first*
@@ -1147,7 +1159,17 @@ zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
 -- NB: This might be called from within the knot, so don't use
 -- smart constructors. See Note [Zonking within the knot] in TcHsType
 zonkTcTypeAndFV ty
-  = tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
+  = tyCoVarsOfType <$> zonkTcTypeInKnot ty
+
+-- | Zonk a type and call 'splitDepVarsOfType' on it.
+-- Works within the knot.
+zonkTcTypeAndSplitDepVars :: TcType -> TcM (Pair TyCoVarSet)
+zonkTcTypeAndSplitDepVars ty
+  = splitDepVarsOfType <$> zonkTcTypeInKnot ty
+
+zonkTcTypesAndSplitDepVars :: [TcType] -> TcM (Pair TyCoVarSet)
+zonkTcTypesAndSplitDepVars tys
+  = splitDepVarsOfTypes <$> mapM zonkTcTypeInKnot tys
 
 zonkTyCoVar :: TyCoVar -> TcM TcType
 -- Works on TyVars and TcTyVars
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 6536b676e9..cdc4ca007a 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -121,10 +121,15 @@ tcPatSynSig name sig_ty
                           , bound_tvs) }
 
        -- Kind generalisation; c.f. kindGeneralise
-       ; let free_kvs = tyCoVarsOfTelescope (implicit_tvs ++ univ_tvs ++ ex_tvs) $
-                        tyCoVarsOfTypes (body_ty : req ++ prov ++ arg_tys)
-
-       ; kvs <- quantifyTyVars emptyVarSet (Pair free_kvs emptyVarSet)
+       ; free_kvs <- zonkTcTypeAndFV $
+                     mkSpecForAllTys (implicit_tvs ++ univ_tvs) $
+                     mkFunTys req $
+                     mkSpecForAllTys ex_tvs $
+                     mkFunTys prov $
+                     mkFunTys arg_tys $
+                     body_ty
+
+       ; kvs <- quantifyZonkedTyVars emptyVarSet (Pair free_kvs emptyVarSet)
 
        -- These are /signatures/ so we zonk to squeeze out any kind
        -- unification variables.  Do this after quantifyTyVars which may
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index 55c8446da1..1b4826e1cd 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -101,11 +101,11 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
         -- during zonking (see TcHsSyn.zonkRule)
 
        ; let tpl_ids     = lhs_evs ++ id_bndrs
-             forall_tkvs = splitDepVarsOfTypes $
-                           rule_ty : map idType tpl_ids
+       ; forall_tkvs <- zonkTcTypesAndSplitDepVars $
+                        rule_ty : map idType tpl_ids
        ; gbls  <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
                                       -- monomorphic bindings from the MR; test tc111
-       ; qtkvs <- quantifyTyVars gbls forall_tkvs
+       ; qtkvs <- quantifyZonkedTyVars gbls forall_tkvs
        ; traceTc "tcRule" (vcat [ pprFullRuleName name
                                 , ppr forall_tkvs
                                 , ppr qtkvs
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 0d1e75454f..96338981e8 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -517,8 +517,8 @@ simplifyInfer :: TcLevel               -- Used when generating the constraints
 simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyCoVars
-       ; qtkvs <- quantify_tvs sigs gbl_tvs $
-                  splitDepVarsOfTypes (map snd name_taus)
+       ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
+       ; qtkvs <- quantify_tvs sigs gbl_tvs dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
        ; return (qtkvs, [], emptyTcEvBinds) }
 
@@ -796,6 +796,8 @@ quantify_tvs :: [TcIdSigInfo]
              -> TcM [TcTyVar]
 -- See Note [Which type variables to quantify]
 quantify_tvs sigs mono_tvs (Pair tau_kvs tau_tvs)
+   -- NB: don't use quantifyZonkedTyVars because the sig stuff might
+   -- be unzonked
   = quantifyTyVars (mono_tvs `delVarSetList` sig_qtvs)
                    (Pair tau_kvs
                          (tau_tvs `extendVarSetList` sig_qtvs
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index ffabeb319e..429c4b815d 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1244,8 +1244,8 @@ tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
             -- them into skolems, so that we don't subsequently
             -- replace a meta kind var with (Any *)
             -- Very like kindGeneralize
-       ; qtkvs <- quantifyTyVars emptyVarSet $
-                                 splitDepVarsOfTypes typats
+       ; vars  <- zonkTcTypesAndSplitDepVars typats
+       ; qtkvs <- quantifyZonkedTyVars emptyVarSet vars
 
        ; MASSERT( isEmptyVarSet $ coVarsOfTypes typats )
            -- This should be the case, because otherwise the solveEqualities
@@ -1437,11 +1437,10 @@ tcConDecl new_or_data rep_tycon tmpl_tvs tmpl_bndrs res_tmpl
 
              -- Kind generalisation
        ; let all_user_tvs = imp_tvs ++ exp_tvs
-       ; kvs <- quantifyTyVars (mkVarSet tmpl_tvs)
-                               (splitDepVarsOfType (mkSpecForAllTys all_user_tvs $
-                                                    mkFunTys ctxt $
-                                                    mkFunTys arg_tys $
-                                                    unitTy))
+       ; vars <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys all_user_tvs $
+                                            mkFunTys ctxt $
+                                            mkFunTys arg_tys $
+                                            unitTy)
                  -- That type is a lie, of course. (It shouldn't end in ()!)
                  -- And we could construct a proper result type from the info
                  -- at hand. But the result would mention only the tmpl_tvs,
@@ -1449,6 +1448,8 @@ tcConDecl new_or_data rep_tycon tmpl_tvs tmpl_bndrs res_tmpl
                  -- we're doing this to get the right behavior around removing
                  -- any vars bound in exp_binders.
 
+       ; kvs <- quantifyZonkedTyVars (mkVarSet tmpl_tvs) vars
+
              -- Zonk to Types
        ; (ze, qkvs)      <- zonkTyBndrsX emptyZonkEnv kvs
        ; (ze, user_qtvs) <- zonkTyBndrsX ze all_user_tvs
@@ -1487,11 +1488,12 @@ tcConDecl _new_or_data rep_tycon tmpl_tvs _tmpl_bndrs res_tmpl
     do { traceTc "tcConDecl 1" (ppr names)
        ; (user_tvs, ctxt, stricts, field_lbls, arg_tys, res_ty,hs_details)
            <- tcGadtSigType (ppr names) (unLoc $ head names) ty
-       ; tkvs <- quantifyTyVars emptyVarSet
-                                (splitDepVarsOfType (mkSpecForAllTys user_tvs $
-                                                     mkFunTys ctxt $
-                                                     mkFunTys arg_tys $
-                                                     res_ty))
+
+       ; vars <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys user_tvs $
+                                            mkFunTys ctxt $
+                                            mkFunTys arg_tys $
+                                            res_ty)
+       ; tkvs <- quantifyZonkedTyVars emptyVarSet vars
 
              -- Zonk to Types
        ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (tkvs ++ user_tvs)
@@ -2160,11 +2162,13 @@ checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
 -- produces the appropriate error message.
 checkValidTyConTyVars :: TyCon -> TcM ()
 checkValidTyConTyVars tc
-  = when duplicate_vars $
-    do { -- strip off the duplicates and look for ill-scoped things
+  = do { -- strip off the duplicates and look for ill-scoped things
          -- but keep the *last* occurrence of each variable, as it's
          -- most likely the one the user wrote
-         let stripped_tvs = reverse $ nub $ reverse tvs
+         let stripped_tvs | duplicate_vars
+                          = reverse $ nub $ reverse tvs
+                          | otherwise
+                          = tvs
              vis_tvs      = filterOutInvisibleTyVars tc tvs
              extra | not (vis_tvs `equalLength` stripped_tvs)
                    = text "NB: Implicitly declared kind variables are put first."
@@ -2174,11 +2178,12 @@ checkValidTyConTyVars tc
          `and_if_that_doesn't_error`
            -- This triggers on test case dependent/should_fail/InferDependency
            -- It reports errors around Note [Dependent LHsQTyVars] in TcHsType
-         addErr (vcat [ text "Invalid declaration for" <+>
-                        quotes (ppr tc) <> semi <+> text "you must explicitly"
-                      , text "declare which variables are dependent on which others."
-                      , hang (text "Inferred variable kinds:")
-                        2 (vcat (map pp_tv stripped_tvs)) ]) }
+         when duplicate_vars (
+          addErr (vcat [ text "Invalid declaration for" <+>
+                         quotes (ppr tc) <> semi <+> text "you must explicitly"
+                       , text "declare which variables are dependent on which others."
+                       , hang (text "Inferred variable kinds:")
+                         2 (vcat (map pp_tv stripped_tvs)) ])) }
   where
     tvs = tyConTyVars tc
     duplicate_vars = sizeVarSet (mkVarSet tvs) < length tvs
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index fa62765239..d78c7f7c7e 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -2302,13 +2302,27 @@ synTyConResKind :: TyCon -> Kind
 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
 
 -- | Retrieve the free variables in this type, splitting them based
--- on whether the variable was used in a dependent context. It's possible
--- for a variable to be reported twice, if it's used both dependently
--- and non-dependently. (This isn't the most precise analysis, because
+-- on whether the variable was used in a dependent context.
+-- (This isn't the most precise analysis, because
 -- it's used in the typechecking knot. It might list some dependent
 -- variables as also non-dependent.)
 splitDepVarsOfType :: Type -> Pair TyCoVarSet
-splitDepVarsOfType = go
+splitDepVarsOfType ty = Pair dep_vars final_nondep_vars
+  where
+    Pair dep_vars nondep_vars = split_dep_vars ty
+    final_nondep_vars = nondep_vars `minusVarSet` dep_vars
+
+-- | Like 'splitDepVarsOfType', but over a list of types
+splitDepVarsOfTypes :: [Type] -> Pair TyCoVarSet
+splitDepVarsOfTypes tys = Pair dep_vars final_nondep_vars
+  where
+    Pair dep_vars nondep_vars = foldMap split_dep_vars tys
+    final_nondep_vars = nondep_vars `minusVarSet` dep_vars
+
+-- | Worker for 'splitDepVarsOfType'. This might output the same var
+-- in both sets, if it's used in both a type and a kind.
+split_dep_vars :: Type -> Pair TyCoVarSet
+split_dep_vars = go
   where
     go (TyVarTy tv)              = Pair (tyCoVarsOfType $ tyVarKind tv)
                                         (unitVarSet tv)
@@ -2328,10 +2342,6 @@ splitDepVarsOfType = go
                go ty1 `mappend` go ty2  -- NB: the Pairs separate along different
                                         -- dimensions here. Be careful!
 
--- | Like 'splitDepVarsOfType', but over a list of types
-splitDepVarsOfTypes :: [Type] -> Pair TyCoVarSet
-splitDepVarsOfTypes = foldMap splitDepVarsOfType
-
 -- | Retrieve the free variables in this type, splitting them based
 -- on whether they are used visibly or invisibly. Invisible ones come
 -- first.