More fixes to kind polymorphism, fixes Trac #6035, #6036
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 25 Apr 2012 11:56:44 +0000 (12:56 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 25 Apr 2012 11:56:44 +0000 (12:56 +0100)
* Significant refactoring in tcFamPats and tcConDecl

* It seems that we have to allow KindVars (not just
  TcKindVars during kind unification.  See
  Note [Unifying kind variables] in TcUnify.

* Be consistent about zonkQuantifiedTyVars

* Split the TcType->TcType zonker (in TcMType)
   from the TcType->Type   zonker (in TcHsSyn)
  The clever parameterisation was doing my head in,
  and it's only a small function

* Remove some dead code (tcTyVarBndrsGen)

compiler/ghci/RtClosureInspect.hs
compiler/typecheck/FamInst.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/typecheck/TcUnify.lhs

index f140c8f..121b269 100644 (file)
@@ -45,7 +45,7 @@ import Var
 import TcRnMonad
 import TcType
 import TcMType
-import TcHsSyn ( mkZonkTcTyVar )
+import TcHsSyn ( zonkTcTypeToType, mkEmptyZonkEnv )
 import TcUnify
 import TcEnv
 
@@ -1131,7 +1131,7 @@ zonkTerm = foldTermM (TermFoldM
 zonkRttiType :: TcType -> TcM Type
 -- Zonk the type, replacing any unbound Meta tyvars
 -- by skolems, safely out of Meta-tyvar-land
-zonkRttiType = zonkType (mkZonkTcTyVar zonk_unbound_meta mkTyVarTy)
+zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta)
   where
     zonk_unbound_meta tv 
       = ASSERT( isTcTyVar tv )
index 9662fae..c43450c 100644 (file)
@@ -254,14 +254,15 @@ addLocalFamInst :: (FamInstEnv,[FamInst]) -> FamInst -> TcM (FamInstEnv, [FamIns
 addLocalFamInst (home_fie, my_fis) fam_inst 
         -- home_fie includes home package and this module
         -- my_fies is just the ones from this module
-  = do { isGHCi <- getIsGHCi
+  = do { traceTc "addLocalFamInst" (ppr fam_inst)
+       ; isGHCi <- getIsGHCi
  
            -- In GHCi, we *override* any identical instances
            -- that are also defined in the interactive context
-      ; let (home_fie', my_fis') 
-              | isGHCi    = (deleteFromFamInstEnv home_fie fam_inst, 
-                             filterOut (identicalFamInst fam_inst) my_fis)
-              | otherwise = (home_fie, my_fis)
+       ; let (home_fie', my_fis') 
+               | isGHCi    = ( deleteFromFamInstEnv home_fie fam_inst 
+                             filterOut (identicalFamInst fam_inst) my_fis)
+               | otherwise = (home_fie, my_fis)
 
            -- Load imported instances, so that we report
            -- overlaps correctly
index 75dedd0..a4af0ce 100644 (file)
@@ -26,9 +26,10 @@ module TcHsSyn (
        -- re-exported from TcMonad
        TcId, TcIdSet, 
 
-       zonkTopDecls, zonkTopExpr, zonkTopLExpr, mkZonkTcTyVar,
-       zonkId, zonkTopBndrs,
-        emptyZonkEnv, mkTyVarZonkEnv, zonkTcTypeToType, zonkTcTypeToTypes
+       zonkTopDecls, zonkTopExpr, zonkTopLExpr, 
+       zonkTopBndrs, zonkTyBndrsX,
+        emptyZonkEnv, mkEmptyZonkEnv, mkTyVarZonkEnv, 
+        zonkTcTypeToType, zonkTcTypeToTypes
   ) where
 
 #include "HsVersions.h"
@@ -37,8 +38,9 @@ import HsSyn
 import Id
 import TcRnMonad
 import PrelNames
+import TypeRep     -- We can see the representation of types
 import TcType
-import TcMType
+import TcMType ( defaultKindVarToStar, zonkQuantifiedTyVar, writeMetaTyVar )
 import TcEvidence
 import TysPrim
 import TysWiredIn
@@ -161,14 +163,6 @@ hsOverLitName (HsIsString {})   = fromStringName
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
--- zonkId is used *during* typechecking just to zonk the Id's type
-zonkId :: TcId -> TcM TcId
-zonkId id
-  = zonkTcType (idType id) `thenM` \ ty' ->
-    returnM (Id.setIdType id ty')
-\end{code}
-
 The rest of the zonking is done *after* typechecking.
 The main zonking pass runs over the bindings
 
@@ -195,7 +189,7 @@ data ZonkEnv
   = ZonkEnv 
       UnboundTyVarZonker
       (TyVarEnv TyVar)          -- 
-      (IdEnv Var)              -- What variables are in scope
+      (IdEnv    Var)           -- What variables are in scope
        -- Maps an Id or EvVar to its zonked version; both have the same Name
        -- Note that all evidence (coercion variables as well as dictionaries)
        --      are kept in the ZonkEnv
@@ -207,7 +201,10 @@ instance Outputable ZonkEnv where
 
 
 emptyZonkEnv :: ZonkEnv
-emptyZonkEnv = ZonkEnv zonkTypeZapping emptyVarEnv emptyVarEnv
+emptyZonkEnv = mkEmptyZonkEnv zonkTypeZapping
+
+mkEmptyZonkEnv :: UnboundTyVarZonker -> ZonkEnv
+mkEmptyZonkEnv zonker = ZonkEnv zonker emptyVarEnv emptyVarEnv
 
 extendIdZonkEnv :: ZonkEnv -> [Var] -> ZonkEnv
 extendIdZonkEnv (ZonkEnv zonk_ty ty_env id_env) ids 
@@ -1041,7 +1038,7 @@ zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
 
        ; let final_bndrs :: [RuleBndr Var]
              final_bndrs = map (RuleBndr . noLoc)
-                             (varSetElemsKvsFirst unbound_tkvs)
+                               (varSetElemsKvsFirst unbound_tkvs)
                            ++ new_bndrs
 
        ; return $ 
@@ -1249,37 +1246,58 @@ DV, TODO: followup on this note mentioning new examples I will add to perf/
 
 
 \begin{code}
-mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
-             -> (TcTyVar -> Type)      -- What to do for an immutable var
-             -> TcTyVar -> TcM TcType
-mkZonkTcTyVar unbound_mvar_fn unbound_ivar_fn
-  = zonk_tv
-  where
-    zonk_tv tv 
-     = ASSERT( isTcTyVar tv )
-       case tcTyVarDetails tv of
-         SkolemTv {}    -> return (unbound_ivar_fn tv)
-         RuntimeUnk {}  -> return (unbound_ivar_fn tv)
-         FlatSkol ty    -> zonkType zonk_tv ty
+zonkTyVarOcc :: ZonkEnv -> TyVar -> TcM TcType
+zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
+  | isTcTyVar tv
+  = case tcTyVarDetails tv of
+         SkolemTv {}    -> lookup_in_env
+         RuntimeUnk {}  -> lookup_in_env
+         FlatSkol ty    -> zonkTcTypeToType env ty
          MetaTv _ ref   -> do { cts <- readMutVar ref
                              ; case cts of    
                                   Flexi -> do { kind <- {-# SCC "zonkKind1" #-}
-                                                         zonkType zonk_tv (tyVarKind tv)
-                                               ; unbound_mvar_fn (setTyVarKind tv kind) }
-                                  Indirect ty -> do { zty <- zonkType zonk_tv ty 
+                                                         zonkTcTypeToType env (tyVarKind tv)
+                                               ; zonk_unbound_tyvar (setTyVarKind tv kind) }
+                                  Indirect ty -> do { zty <- zonkTcTypeToType env ty 
                                                      -- Small optimisation: shortern-out indirect steps
                                                      -- so that the old type may be more easily collected.
                                                      ; writeMutVar ref (Indirect zty)
                                                      ; return zty } }
+  | otherwise
+  = lookup_in_env
+  where
+    lookup_in_env    -- Look up in the env just as we do for Ids
+      = case lookupVarEnv tv_env tv of
+          Nothing  -> return (mkTyVarTy tv)
+          Just tv' -> return (mkTyVarTy tv')
 
 zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
-zonkTcTypeToType (ZonkEnv zonk_unbound_tyvar tv_env _id_env)
-  = zonkType (mkZonkTcTyVar zonk_unbound_tyvar zonk_bound_tyvar)
+zonkTcTypeToType env ty
+  = go ty
   where
-    zonk_bound_tyvar tv    -- Look up in the env just as we do for Ids
-      = case lookupVarEnv tv_env tv of
-          Nothing  -> mkTyVarTy tv
-          Just tv' -> mkTyVarTy tv'
+    go (TyConApp tc tys) = do tys' <- mapM go tys
+                              return (TyConApp tc tys')
+
+    go (LitTy n)         = return (LitTy n)
+
+    go (FunTy arg res)   = do arg' <- go arg
+                              res' <- go res
+                              return (FunTy arg' res')
+
+    go (AppTy fun arg)   = do fun' <- go fun
+                              arg' <- go arg
+                              return (mkAppTy fun' arg')
+               -- NB the mkAppTy; we might have instantiated a
+               -- type variable to a type constructor, so we need
+               -- to pull the TyConApp to the top.
+
+       -- The two interesting cases!
+    go (TyVarTy tv) = zonkTyVarOcc env tv
+
+    go (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv ) do
+                          do { (env', tv') <- zonkTyBndrX env tv
+                             ; ty' <- zonkTcTypeToType env' ty
+                             ; return (ForAllTy tv' ty') }
 
 zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
 zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
index 2f8d743..536772a 100644 (file)
@@ -24,7 +24,7 @@ module TcHsType (
 
                -- Kind-checking types
                 -- No kind generalisation, no checkValidType
-       tcHsTyVarBndrs, tcHsTyVarBndrsGen ,
+       tcHsTyVarBndrs, 
         tcHsLiftedType, 
        tcLHsType, tcCheckLHsType, 
         tcHsContext, tcInferApps, tcHsArgTys,
@@ -177,8 +177,8 @@ tcHsSigTypeNC ctxt (L loc hs_ty)
           -- The kind is checked by checkValidType, and isn't necessarily
           -- of kind * in a Template Haskell quote eg [t| Maybe |]
 
+          -- Generalise here: see Note [ generalisation]
         ; ty <- tcCheckHsTypeAndGen hs_ty kind
-                -- Generalise here: see Note [Kind generalisation]
 
           -- Zonk to expose kind information to checkValidType
         ; ty <- zonkTcType ty
@@ -826,28 +826,9 @@ tcHsTyVarBndr (L _ hs_tv)
        { kind <- case hs_tv of
                    UserTyVar {} -> newMetaKindVar
                    KindedTyVar _ (HsBSig kind _) -> tcLHsKind kind
-       ; return (mkTyVar name kind) } } }
+       ; return (mkTcTyVar name kind (SkolemTv False)) } } }
 
 ------------------
-tcHsTyVarBndrsGen :: [LHsTyVarBndr Name] 
-                 -> TcM (TcTyVarSet, r)  -- Result + free tyvars of thing inside
-                 -> TcM ([TyVar], r)     -- Generalised kind variables 
-                                          -- + zonked tyvars + result result
--- tcHsTyVarBndrsGen [(f :: ?k -> *), (a :: ?k)] thing_inside
--- Returns with tyvars [(k :: BOX), (f :: k -> *), (a :: k)]
-tcHsTyVarBndrsGen hs_tvs thing_inside
-  = do { traceTc "tcHsTyVarBndrsGen" (ppr hs_tvs) 
-       ; (tvs, (ftvs, res)) <- tcHsTyVarBndrs hs_tvs $ \ tvs ->
-                       do { res <- thing_inside
-                          ; return (tvs, res) }
-       ; let kinds = map tyVarKind tvs
-       ; kvs' <- kindGeneralize (tyVarsOfTypes kinds `unionVarSet` 
-                                        (ftvs `delVarSetList` tvs))
-       ; zonked_kinds <- mapM zonkTcKind kinds
-       ; let tvs' = zipWith setTyVarKind tvs zonked_kinds
-                     -- See Note [Kinds of quantified type variables]
-       ; traceTc "tcTyVarBndrsGen" (ppr (hs_tvs, kvs', tvs))
-       ; return (kvs' ++ tvs', res) }
 
 -------------------
 kindGeneralize :: TyVarSet -> TcM [KindVar]
@@ -856,6 +837,9 @@ kindGeneralize tkvs
        ; tidy_env <- tcInitTidyEnv
        ; tkvs     <- zonkTyVarsAndFV tkvs
        ; let kvs_to_quantify = varSetElems (tkvs `minusVarSet` gbl_tvs)
+                -- Any type varaibles in tkvs will be in scope,
+                -- and hence in gbl_tvs, so after removing gbl_tvs
+                -- we should only have kind variables left
 
              (_, tidy_kvs_to_quantify) = tidyTyVarBndrs tidy_env kvs_to_quantify
                            -- We do not get a later chance to tidy!
@@ -1317,8 +1301,8 @@ tc_lhs_kind (L span ki) = setSrcSpan span (tc_hs_kind ki)
 
 -- The main worker
 tc_hs_kind :: HsKind Name -> TcM Kind
-tc_hs_kind k@(HsTyVar _)   = tc_app k []
-tc_hs_kind k@(HsAppTy _ _) = tc_app k []
+tc_hs_kind k@(HsTyVar _)   = tc_kind_app k []
+tc_hs_kind k@(HsAppTy _ _) = tc_kind_app k []
 
 tc_hs_kind (HsParTy ki) = tc_lhs_kind ki
 
@@ -1343,17 +1327,17 @@ tc_hs_kind (HsTupleTy _ kis) =
 tc_hs_kind k = panic ("tc_hs_kind: " ++ showPpr k)
 
 -- Special case for kind application
-tc_app :: HsKind Name -> [LHsKind Name] -> TcM Kind
-tc_app (HsAppTy ki1 ki2) kis = tc_app (unLoc ki1) (ki2:kis)
-tc_app (HsTyVar tc)      kis = do { arg_kis <- mapM tc_lhs_kind kis
-                                  ; tc_var_app tc arg_kis }
-tc_app ki                _   = failWithTc (quotes (ppr ki) <+> 
+tc_kind_app :: HsKind Name -> [LHsKind Name] -> TcM Kind
+tc_kind_app (HsAppTy ki1 ki2) kis = tc_kind_app (unLoc ki1) (ki2:kis)
+tc_kind_app (HsTyVar tc)      kis = do { arg_kis <- mapM tc_lhs_kind kis
+                                       ; tc_kind_var_app tc arg_kis }
+tc_kind_app ki                _   = failWithTc (quotes (ppr ki) <+> 
                                     ptext (sLit "is not a kind constructor"))
 
-tc_var_app :: Name -> [Kind] -> TcM Kind
+tc_kind_var_app :: Name -> [Kind] -> TcM Kind
 -- Special case for * and Constraint kinds
 -- They are kinds already, so we don't need to promote them
-tc_var_app name arg_kis
+tc_kind_var_app name arg_kis
   |  name == liftedTypeKindTyConName
   || name == constraintKindTyConName
   = do { unless (null arg_kis)
@@ -1361,10 +1345,10 @@ tc_var_app name arg_kis
        ; thing <- tcLookup name
        ; case thing of
            AGlobal (ATyCon tc) -> return (mkTyConApp tc [])
-           _                   -> panic "tc_var_app 1" }
+           _                   -> panic "tc_kind_var_app 1" }
 
 -- General case
-tc_var_app name arg_kis
+tc_kind_var_app name arg_kis
   = do { (_errs, mb_thing) <- tryTc (tcLookup name)
        ;  case mb_thing of
           Just (AGlobal (ATyCon tc))
@@ -1378,11 +1362,16 @@ tc_var_app name arg_kis
                       Nothing -> err tc "is not promotable" }
 
           -- A lexically scoped kind variable
-           -- Kind variables always have kind BOX, so cannot be applied to anything
           Just (ATyVar _ kind_var) 
-             | null arg_kis -> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
-             | otherwise    -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr name)
-                                           <+> ptext (sLit "cannot appear in a function position"))
+             | not (isKindVar kind_var) 
+             -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr kind_var)
+                            <+> ptext (sLit "used bas a kind"))
+             | not (null arg_kis) -- Kind variables always have kind BOX, 
+                                  -- so cannot be applied to anything
+             -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr name)
+                            <+> ptext (sLit "cannot appear in a function position"))
+             | otherwise 
+             -> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
 
           -- It is in scope, but not what we expected
           Just thing -> wrongThingErr "promoted type" thing name
@@ -1391,7 +1380,7 @@ tc_var_app name arg_kis
           Nothing    
              -> -- ASSERT2 ( isTyConName name, ppr name )
                do { env <- getLclEnv
-                  ; traceTc "tc_var_app" (ppr name $$ ppr (tcl_env env))
+                  ; traceTc "tc_kind_var_app" (ppr name $$ ppr (tcl_env env))
                   ; failWithTc (ptext (sLit "Promoted kind") <+> 
                                  quotes (ppr name) <+>
                                  ptext (sLit "used in a mutually recursive group")) } }
index d4d4952..3ba80e3 100644 (file)
@@ -59,16 +59,15 @@ module TcMType (
 
   --------------------------------
   -- Zonking
-  zonkType, zonkKind, zonkTcPredType, 
+  zonkTcPredType, 
   skolemiseSigTv, skolemiseUnboundMetaTyVar,
   zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, 
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
   zonkTcType, zonkTcTypes, zonkTcThetaType,
 
   zonkTcKind, defaultKindVarToStar, zonkCt, zonkCts,
-  zonkImplication, zonkEvVar, zonkWC, 
+  zonkImplication, zonkEvVar, zonkWC, zonkId,
 
-  zonkTcTypeAndSubst,
   tcGetGlobalTyVars, 
   ) where
 
@@ -491,50 +490,10 @@ zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
 
 -----------------  Types
-zonkTcType :: TcType -> TcM TcType
--- Simply look through all Flexis
-zonkTcType ty = zonkType zonkTcTyVar ty
-
-zonkTcTyVar :: TcTyVar -> TcM TcType
--- Simply look through all Flexis
-zonkTcTyVar tv
-  = ASSERT2( isTcTyVar tv, ppr tv ) do
-    case tcTyVarDetails tv of
-      SkolemTv {}   -> zonk_kind_and_return
-      RuntimeUnk {} -> zonk_kind_and_return
-      FlatSkol ty   -> zonkTcType ty
-      MetaTv _ ref  -> do { cts <- readMutVar ref
-                          ; case cts of
-                              Flexi       -> zonk_kind_and_return
-                              Indirect ty -> zonkTcType ty }
-  where
-    zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
-                              ; return (TyVarTy z_tv) }
-
 zonkTyVarKind :: TyVar -> TcM TyVar
 zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
                       ; return (setTyVarKind tv kind') }
 
-zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
--- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
-zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
-  where
-    zonk_tv tv
-      = do { z_tv <- updateTyVarKindM zonkTcKind tv
-           ; ASSERT ( isTcTyVar tv )
-             case tcTyVarDetails tv of
-                SkolemTv {}   -> return (TyVarTy z_tv)
-                RuntimeUnk {} -> return (TyVarTy z_tv)
-                FlatSkol ty   -> zonkType zonk_tv ty
-                MetaTv _ ref  -> do { cts <- readMutVar ref
-                                    ; case cts of
-                                  Flexi       -> zonk_flexi z_tv
-                                  Indirect ty -> zonkType zonk_tv ty } }
-    zonk_flexi tv
-      = case lookupTyVar subst tv of
-          Just ty -> zonkType zonk_tv ty
-          Nothing -> return (TyVarTy tv)
-
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mapM zonkTcType tys
 
@@ -777,23 +736,25 @@ simplifier knows how to deal with.
 
 %************************************************************************
 %*                                                                     *
-\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
+\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
 %*                                                                     *
 %*             For internal use only!                                  *
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
+-- zonkId is used *during* typechecking just to zonk the Id's type
+zonkId :: TcId -> TcM TcId
+zonkId id
+  = do { ty' <- zonkTcType (idType id)
+       ; return (Id.setIdType id ty') }
+
 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
-zonkKind :: (TcTyVar -> TcM Kind) -> TcKind -> TcM Kind
-zonkKind = zonkType
-
-zonkType :: (TcTyVar -> TcM Type)  -- What to do with TcTyVars
-         -> TcType -> TcM Type
-zonkType zonk_tc_tyvar ty
+zonkTcType :: TcType -> TcM TcType
+zonkTcType ty
   = go ty
   where
     go (TyConApp tc tys) = do tys' <- mapM go tys
@@ -813,7 +774,7 @@ zonkType zonk_tc_tyvar ty
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
-    go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
+    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
                       | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
                -- Ordinary (non Tc) tyvars occur inside quantified types
 
@@ -821,6 +782,22 @@ zonkType zonk_tc_tyvar ty
                              ty' <- go ty
                              tyvar' <- updateTyVarKindM go tyvar
                              return (ForAllTy tyvar' ty')
+
+zonkTcTyVar :: TcTyVar -> TcM TcType
+-- Simply look through all Flexis
+zonkTcTyVar tv
+  = ASSERT2( isTcTyVar tv, ppr tv ) do
+    case tcTyVarDetails tv of
+      SkolemTv {}   -> zonk_kind_and_return
+      RuntimeUnk {} -> zonk_kind_and_return
+      FlatSkol ty   -> zonkTcType ty
+      MetaTv _ ref  -> do { cts <- readMutVar ref
+                          ; case cts of
+                              Flexi       -> zonk_kind_and_return
+                              Indirect ty -> zonkTcType ty }
+  where
+    zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
+                              ; return (TyVarTy z_tv) }
 \end{code}
 
 
index 93981f3..350f0d2 100644 (file)
@@ -757,17 +757,27 @@ tcFamTyPats fam_tc (HsBSig arg_pats (kvars, tvars)) kind_checker thing_inside
 
          -- Kind-check and quantify
          -- See Note [Quantifying over family patterns]
-        ; (tkvs, typats) <- tcExtendTyVarEnv (map mkKindSigVar kvars) $
-                            tcHsTyVarBndrsGen (map (noLoc . UserTyVar) tvars) $ 
-             do { typats <- tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds
-                ; kind_checker res_kind
-                ; return (tyVarsOfTypes typats, typats) }
-
-       ; all_args' <- zonkTcTypeToTypes emptyZonkEnv (fam_arg_kinds ++ typats)
-       ; res_kind' <- zonkTcTypeToType emptyZonkEnv res_kind
-       ; traceTc "tcFamPats" (ppr tkvs $$ ppr all_args' $$ ppr res_kind')
-       ; tcExtendTyVarEnv tkvs $
-         thing_inside tkvs all_args' res_kind' }
+       ; typats <- tcExtendTyVarEnv (map mkKindSigVar kvars)      $
+                   tcHsTyVarBndrs (map (noLoc . UserTyVar) tvars) $ \ _ ->
+                   do { kind_checker res_kind
+                      ; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds }
+       ; let all_args = fam_arg_kinds ++ typats
+
+            -- Find free variables (after zonking)
+       ; tkvs <- zonkTyVarsAndFV (tyVarsOfTypes all_args)
+
+            -- Turn them into skolems, so that we don't subsequently 
+            -- replace a meta kind var with AnyK
+       ; qtkvs <- zonkQuantifiedTyVars (varSetElems tkvs)
+
+            -- Zonk the patterns etc into the Type world
+       ; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
+       ; all_args'    <- zonkTcTypeToTypes ze all_args
+       ; res_kind'    <- zonkTcTypeToType  ze res_kind
+
+       ; traceTc "tcFamPats" (ppr qtkvs' $$ ppr all_args' $$ ppr res_kind')
+       ; tcExtendTyVarEnv qtkvs' $
+         thing_inside qtkvs' all_args' res_kind' }
 \end{code}
 
 Note [Quantifying over family patterns]
@@ -810,7 +820,7 @@ Then in the family instance we want to
 Notice that in the third step we quantify over all the visibly-mentioned
 type variables (a,b), but also over the implicitly mentioned kind varaibles
 (k, k').  In this case one is bound explicitly but often there will be 
-none. The rold of the kind signature (a :: Maybe k) is to add a constraint
+none. The role of the kind signature (a :: Maybe k) is to add a constraint
 that 'a' must have that kind, and to bring 'k' into scope.
 
 Note [Associated type instances]
@@ -867,18 +877,18 @@ dataDeclChecks tc_name new_or_data stupid_theta cons
           -- Check that the stupid theta is empty for a GADT-style declaration
        ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
 
-       -- Check that a newtype has exactly one constructor
-       -- Do this before checking for empty data decls, so that
-       -- we don't suggest -XEmptyDataDecls for newtypes
-      ; checkTc (new_or_data == DataType || isSingleton cons) 
+        -- Check that a newtype has exactly one constructor
+        -- Do this before checking for empty data decls, so that
+        -- we don't suggest -XEmptyDataDecls for newtypes
+       ; checkTc (new_or_data == DataType || isSingleton cons) 
                (newtypeConError tc_name (length cons))
 
-       -- Check that there's at least one condecl,
-       -- or else we're reading an hs-boot file, or -XEmptyDataDecls
-      ; empty_data_decls <- xoptM Opt_EmptyDataDecls
-      ; is_boot <- tcIsHsBoot  -- Are we compiling an hs-boot file?
-      ; checkTc (not (null cons) || empty_data_decls || is_boot)
-                (emptyConDeclsErr tc_name) }
+               -- Check that there's at least one condecl,
+         -- or else we're reading an hs-boot file, or -XEmptyDataDecls
+       ; empty_data_decls <- xoptM Opt_EmptyDataDecls
+       ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
+       ; checkTc (not (null cons) || empty_data_decls || is_boot)
+                 (emptyConDeclsErr tc_name) }
     
 -----------------------------------
 tcConDecls :: NewOrData -> Bool -> TyCon -> ([TyVar], Type)
@@ -895,46 +905,50 @@ tcConDecl :: NewOrData
 
 tcConDecl new_or_data existential_ok rep_tycon res_tmpl        -- Data types
          con@(ConDecl { con_name = name
-                       , con_qvars = tvs, con_cxt = ctxt
-                       , con_details = details, con_res = res_ty })
+                       , con_qvars = hs_tvs, con_cxt = hs_ctxt
+                       , con_details = details, con_res = hs_res_ty })
   = addErrCtxt (dataConCtxt name) $
     do { traceTc "tcConDecl 1" (ppr name)
-       ; (tvs', (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)
-           <- tcHsTyVarBndrsGen tvs $ 
-              do { ctxt'    <- tcHsContext ctxt
+       ; (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts
+           <- tcHsTyVarBndrs hs_tvs $ \ tvs ->
+              do { ctxt    <- tcHsContext hs_ctxt
                  ; details' <- tcConArgs new_or_data details
-                 ; res_ty'  <- tcConRes res_ty
+                 ; res_ty   <- tcConRes hs_res_ty
                  ; let (is_infix, field_lbls, btys') = details'
-                       (arg_tys', stricts)           = unzip btys'
-                       ftvs = tyVarsOfTypes ctxt'     `unionVarSet`
-                              tyVarsOfTypes arg_tys'  `unionVarSet`
-                              case res_ty' of
-                                 ResTyH98     -> emptyVarSet
-                                 ResTyGADT ty -> tyVarsOfType ty
-                 ; return (ftvs, (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)) }
-
-
-             -- Substitute, to account for the kind 
-             -- unifications done by tcHsTyVarBndrsGen
-       ; traceTc "tcConDecl 2" (ppr name)
-       ; let ze = mkTyVarZonkEnv tvs'
-       ; arg_tys' <- zonkTcTypeToTypes ze arg_tys'
-       ; ctxt'    <- zonkTcTypeToTypes ze ctxt'
-       ; res_ty'  <- case res_ty' of
-                           ResTyH98     -> return ResTyH98
-                           ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
+                       (arg_tys, stricts)           = unzip btys'
+                 ; return (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) }
+
+       ; let pretend_res_ty = case res_ty of
+                                ResTyH98     -> unitTy
+                                ResTyGADT ty -> ty
+             pretend_con_ty = mkSigmaTy tvs ctxt (mkFunTys arg_tys pretend_res_ty)
+                -- This pretend_con_ty stuff is just a convenient way to get the
+                -- free kind variables of the type, for kindGeneralize to work on
+
+             -- Generalise the kind variables (returning quantifed TcKindVars)
+             -- and quanify the type variables (substiting their kinds)
+       ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty)
+       ; tvs <- zonkQuantifiedTyVars tvs
+
+             -- Zonk to Types
+       ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (kvs ++ tvs)
+       ; arg_tys <- zonkTcTypeToTypes ze arg_tys
+       ; ctxt    <- zonkTcTypeToTypes ze ctxt
+       ; res_ty  <- case res_ty of
+                      ResTyH98     -> return ResTyH98
+                      ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
 
        ; checkTc (existential_ok || conRepresentibleWithH98Syntax con)
                 (badExistential name)
 
-       ; let (univ_tvs, ex_tvs, eq_preds, res_ty'')
-                = rejigConRes res_tmpl tvs' res_ty'
+       ; let (univ_tvs, ex_tvs, eq_preds, res_ty')
+                = rejigConRes res_tmpl qtkvs res_ty
 
        ; traceTc "tcConDecl 3" (ppr name)
        ; buildDataCon (unLoc name) is_infix
                      stricts field_lbls
-                     univ_tvs ex_tvs eq_preds ctxt' arg_tys'
-                     res_ty'' rep_tycon
+                     univ_tvs ex_tvs eq_preds ctxt arg_tys
+                     res_ty' rep_tycon
                -- NB:  we put data_tc, the type constructor gotten from the
                --      constructor type signature into the data constructor;
                --      that way checkValidDataCon can complain if it's wrong.
@@ -1418,9 +1432,9 @@ checkValidClass cls
                -- type variable.  What a mess!
 
     check_at_defs (fam_tc, defs)
-      = do mapM_ (\(ATD _tvs pats rhs _loc) -> checkValidFamInst pats rhs) defs
-           tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $ 
-             mapM_ (check_loc_at_def fam_tc) defs
+      = do mapM_ (\(ATD _tvs pats rhs _loc) -> checkValidFamInst pats rhs) defs
+           tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $ 
+             mapM_ (check_loc_at_def fam_tc) defs }
 
     check_loc_at_def fam_tc (ATD _tvs pats _rhs loc)
       -- Set the location for each of the default declarations
index d22fbda..1729dcd 100644 (file)
@@ -1087,8 +1087,12 @@ unifyKind :: TcKind           -- k1 (actual)
           -> TcM Ordering     -- Returns the relation between the kinds
                               -- LT <=> k1 is a sub-kind of k2
 
-unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
-unifyKind k1 (TyVarTy kv2) = uKVar True  kv2 k1
+-- unifyKind deals with the top-level sub-kinding story
+-- but recurses into the simpler unifyKindEq for any sub-terms
+-- The sub-kinding stuff only applies at top level
+
+unifyKind (TyVarTy kv1) k2 = uKVar False unifyKind EQ kv1 k2
+unifyKind k1 (TyVarTy kv2) = uKVar True  unifyKind EQ kv2 k1
 
 unifyKind k1 k2       -- See Note [Expanding synonyms during unification]
   | Just k1' <- tcView k1 = unifyKind k1' k2
@@ -1103,24 +1107,44 @@ unifyKind k1@(TyConApp kc1 []) k2@(TyConApp kc2 [])
 unifyKind k1 k2 = do { unifyKindEq k1 k2; return EQ }
   -- In all other cases, let unifyKindEq do the work
 
-uKVar :: Bool -> MetaKindVar -> TcKind -> TcM Ordering
-uKVar isFlipped kv1 k2
-  | isMetaTyVar kv1
+uKVar :: Bool -> (TcKind -> TcKind -> TcM a) -> a
+      -> MetaKindVar -> TcKind -> TcM a
+uKVar isFlipped unify_kind eq_res kv1 k2
+  | isTcTyVar kv1, isMetaTyVar kv1       -- See Note [Unifying kind variables]
   = do  { mb_k1 <- readMetaTyVar kv1
         ; case mb_k1 of
-            Flexi -> uUnboundKVar kv1 k2 >> return EQ
-            Indirect k1 -> unifyKind k1 k2 }
-  | TyVarTy kv2 <- k2, isMetaTyVar kv2
-  = uKVar (not isFlipped) kv2 (TyVarTy kv1)
-  | TyVarTy kv2 <- k2, kv1 == kv2 = return EQ
+            Flexi -> do { uUnboundKVar kv1 k2; return eq_res }
+            Indirect k1 -> if isFlipped then unify_kind k2 k1
+                                        else unify_kind k1 k2 }
+  | TyVarTy kv2 <- k2, kv1 == kv2 
+  = return eq_res
+
+  | TyVarTy kv2 <- k2, isTcTyVar kv1, isMetaTyVar kv2
+  = uKVar (not isFlipped) unify_kind eq_res kv2 (TyVarTy kv1)
+
   | otherwise = if isFlipped 
                 then unifyKindMisMatch k2 (TyVarTy kv1)
                 else unifyKindMisMatch (TyVarTy kv1) k2
 
+{- Note [Unifying kind variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Rather hackily, kind variables can be TyVars not just TcTyVars.
+Main reason is in 
+   data instance T (D (x :: k)) = ...con-decls...
+Here we bring into scope a kind variable 'k', and use it in the 
+con-decls.  BUT the con-decls will be finished and frozen, and
+are not amenable to subsequent substitution, so it makes sense
+to have the *final* kind-variable (a KindVar, not a TcKindVar) in 
+scope.  So at least during kind unification we can encounter a
+KindVar. 
+
+Hence the isTcTyVar tests before using isMetaTyVar.
+-}
+
 ---------------------------
 unifyKindEq :: TcKind -> TcKind -> TcM ()
-unifyKindEq (TyVarTy kv1) k2 = uKVarEq False kv1 k2
-unifyKindEq k1 (TyVarTy kv2) = uKVarEq True  kv2 k1
+unifyKindEq (TyVarTy kv1) k2 = uKVar False unifyKindEq () kv1 k2
+unifyKindEq k1 (TyVarTy kv2) = uKVar True  unifyKindEq () kv2 k1
 
 unifyKindEq (FunTy a1 r1) (FunTy a2 r2)
   = do { unifyKindEq a1 a2; unifyKindEq r1 r2 }
@@ -1135,27 +1159,10 @@ unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
 unifyKindEq k1 k2 = unifyKindMisMatch k1 k2
 
 ----------------
--- For better error messages, we record whether we've flipped the kinds
--- during the process.
-uKVarEq :: Bool -> MetaKindVar -> TcKind -> TcM ()
-uKVarEq isFlipped kv1 k2
-  | isMetaTyVar kv1
-  = do  { mb_k1 <- readMetaTyVar kv1
-        ; case mb_k1 of
-            Flexi -> uUnboundKVar kv1 k2
-            Indirect k1 -> unifyKindEq k1 k2 }
-  | TyVarTy kv2 <- k2, isMetaTyVar kv2
-  = uKVarEq (not isFlipped) kv2 (TyVarTy kv1)
-  | TyVarTy kv2 <- k2, kv1 == kv2 = return ()
-  | otherwise = if isFlipped 
-                then unifyKindMisMatch k2 (TyVarTy kv1)
-                else unifyKindMisMatch (TyVarTy kv1) k2
-
-----------------
 uUnboundKVar :: MetaKindVar -> TcKind -> TcM ()
 uUnboundKVar kv1 k2@(TyVarTy kv2)
   | kv1 == kv2 = return ()
-  | isMetaTyVar kv2   -- Distinct kind variables
+  | isTcTyVar kv2, isMetaTyVar kv2   -- Distinct kind variables
   = do  { mb_k2 <- readMetaTyVar kv2
         ; case mb_k2 of
             Indirect k2 -> uUnboundKVar kv1 k2