More changes to kind inference for type and class declarations
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 10 Jul 2012 15:02:03 +0000 (16:02 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 10 Jul 2012 15:02:03 +0000 (16:02 +0100)
These should fix #7024 and #7022, among others.

The main difficulty was that we were getting occ-name clashes
between kind and type variables in TyCons, when spat into an
interface file. The new scheme is to tidy TyCons during the
conversoin into IfaceSyn, rather than trying to generate them
pre-tidied, which was the already-unsatisfactory previous plan.

There is the usual wave of refactorig as well.

compiler/iface/MkIface.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcRules.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/types/Kind.lhs

index 7420dd8..d51fdd4 100644 (file)
@@ -1433,19 +1433,45 @@ checkList (check:checks) = do recompile <- check
 
 \begin{code}
 tyThingToIfaceDecl :: TyThing -> IfaceDecl
--- Assumption: the thing is already tidied, so that locally-bound names
---             (lambdas, for-alls) already have non-clashing OccNames
--- Reason: Iface stuff uses OccNames, and the conversion here does
---         not do tidying on the way
-tyThingToIfaceDecl (AnId id)
+tyThingToIfaceDecl (AnId id)      = idToIfaceDecl id
+tyThingToIfaceDecl (ATyCon tycon) = tyConToIfaceDecl emptyTidyEnv tycon
+tyThingToIfaceDecl (ACoAxiom ax)  = coAxiomToIfaceDecl ax
+tyThingToIfaceDecl (ADataCon dc)  = pprPanic "toIfaceDecl" (ppr dc)
+                                    -- Should be trimmed out earlier
+
+--------------------------
+idToIfaceDecl :: Id -> IfaceDecl
+-- The Id is already tidied, so that locally-bound names
+-- (lambdas, for-alls) already have non-clashing OccNames
+-- We can't tidy it here, locally, because it may have
+-- free variables in its type or IdInfo
+idToIfaceDecl id
   = IfaceId { ifName      = getOccName id,
               ifType      = toIfaceType (idType id),
               ifIdDetails = toIfaceIdDetails (idDetails id),
               ifIdInfo    = toIfaceIdInfo (idInfo id) }
 
-tyThingToIfaceDecl (ATyCon tycon)
+
+--------------------------
+coAxiomToIfaceDecl :: CoAxiom -> IfaceDecl
+-- We *do* tidy Axioms, because they are not (and cannot 
+-- conveniently be) built in tidy form
+coAxiomToIfaceDecl ax
+ = IfaceAxiom { ifName = name
+              , ifTyVars = toIfaceTvBndrs tv_bndrs
+              , ifLHS    = tidyToIfaceType env (coAxiomLHS ax)
+              , ifRHS    = tidyToIfaceType env (coAxiomRHS ax) }
+ where
+   name = getOccName ax
+   (env, tv_bndrs) = tidyTyVarBndrs emptyTidyEnv (coAxiomTyVars ax)
+
+-----------------
+tyConToIfaceDecl :: TidyEnv -> TyCon -> IfaceDecl
+-- We *do* tidy TyCons, because they are not (and cannot 
+-- conveniently be) built in tidy form
+tyConToIfaceDecl env tycon
   | Just clas <- tyConClass_maybe tycon
-  = classToIfaceDecl clas
+  = classToIfaceDecl env clas
 
   | isSynTyCon tycon
   = IfaceSyn {  ifName    = getOccName tycon,
@@ -1457,7 +1483,7 @@ tyThingToIfaceDecl (ATyCon tycon)
   = IfaceData { ifName    = getOccName tycon,
                 ifCType   = tyConCType tycon,
                 ifTyVars  = toIfaceTvBndrs tyvars,
-                ifCtxt    = toIfaceContext (tyConStupidTheta tycon),
+                ifCtxt    = tidyToIfaceContext env1 (tyConStupidTheta tycon),
                 ifCons    = ifaceConDecls (algTyConRhs tycon),
                 ifRec     = boolToRecFlag (isRecursiveTyCon tycon),
                 ifGadtSyntax = isGadtSyntaxTyCon tycon,
@@ -1469,16 +1495,15 @@ tyThingToIfaceDecl (ATyCon tycon)
 
   | otherwise = pprPanic "toIfaceDecl" (ppr tycon)
   where
-    tyvars = tyConTyVars tycon
+    (env1, tyvars) = tidyTyVarBndrs env (tyConTyVars tycon)
+
     (syn_rhs, syn_ki) 
        = case synTyConRhs tycon of
-            SynFamilyTyCon  -> (Nothing,               toIfaceType (synTyConResKind tycon))
-            SynonymTyCon ty -> (Just (toIfaceType ty), toIfaceType (typeKind ty))
+            SynFamilyTyCon  -> (Nothing,               tidyToIfaceType env1 (synTyConResKind tycon))
+            SynonymTyCon ty -> (Just (toIfaceType ty), tidyToIfaceType env1 (typeKind ty))
 
-    ifaceConDecls (NewTyCon { data_con = con })     = 
-      IfNewTyCon  (ifaceConDecl con)
-    ifaceConDecls (DataTyCon { data_cons = cons })  = 
-      IfDataTyCon (map ifaceConDecl cons)
+    ifaceConDecls (NewTyCon { data_con = con })     = IfNewTyCon  (ifaceConDecl con)
+    ifaceConDecls (DataTyCon { data_cons = cons })  = IfDataTyCon (map ifaceConDecl cons)
     ifaceConDecls DataFamilyTyCon {}                = IfDataFamTyCon
     ifaceConDecls (AbstractTyCon distinct)          = IfAbstractTyCon distinct
         -- The last case happens when a TyCon has been trimmed during tidying
@@ -1490,39 +1515,27 @@ tyThingToIfaceDecl (ATyCon tycon)
         = IfCon   { ifConOcc     = getOccName (dataConName data_con),
                     ifConInfix   = dataConIsInfix data_con,
                     ifConWrapper = isJust (dataConWrapId_maybe data_con),
-                    ifConUnivTvs = toIfaceTvBndrs univ_tvs,
-                    ifConExTvs   = toIfaceTvBndrs ex_tvs,
+                    ifConUnivTvs = toIfaceTvBndrs univ_tvs',
+                    ifConExTvs   = toIfaceTvBndrs ex_tvs',
                     ifConEqSpec  = to_eq_spec eq_spec,
-                    ifConCtxt    = toIfaceContext theta,
-                    ifConArgTys  = map toIfaceType arg_tys,
+                    ifConCtxt    = tidyToIfaceContext env3 theta,
+                    ifConArgTys  = map (tidyToIfaceType env3) arg_tys,
                     ifConFields  = map getOccName 
                                        (dataConFieldLabels data_con),
                     ifConStricts = dataConStrictMarks data_con }
         where
           (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) = dataConFullSig data_con
+          (env2, univ_tvs') = tidyTyClTyVarBndrs env1 univ_tvs
+          (env3, ex_tvs')   = tidyTyVarBndrs env2 ex_tvs
+          to_eq_spec spec = [ (getOccName (tidyTyVar env3 tv), tidyToIfaceType env3 ty) 
+                            | (tv,ty) <- spec]
 
-    to_eq_spec spec = [(getOccName tv, toIfaceType ty) | (tv,ty) <- spec]
 
-tyThingToIfaceDecl (ACoAxiom ax)
- = IfaceAxiom { ifName = name
-              , ifTyVars = tv_bndrs
-              , ifLHS = lhs
-              , ifRHS = rhs }
- where
-   name = getOccName ax
-   tv_bndrs = toIfaceTvBndrs (coAxiomTyVars ax)
-   lhs = toIfaceType (coAxiomLHS ax)
-   rhs = toIfaceType (coAxiomRHS ax)
-
-tyThingToIfaceDecl (ADataCon dc)
- = pprPanic "toIfaceDecl" (ppr dc)      -- Should be trimmed out earlier
-
-
-classToIfaceDecl :: Class -> IfaceDecl
-classToIfaceDecl clas
-  = IfaceClass { ifCtxt   = toIfaceContext sc_theta,
+classToIfaceDecl :: TidyEnv -> Class -> IfaceDecl
+classToIfaceDecl env clas
+  = IfaceClass { ifCtxt   = tidyToIfaceContext env1 sc_theta,
                  ifName   = getOccName (classTyCon clas),
-                 ifTyVars = toIfaceTvBndrs clas_tyvars,
+                 ifTyVars = toIfaceTvBndrs clas_tyvars',
                  ifFDs    = map toIfaceFD clas_fds,
                  ifATs    = map toIfaceAT clas_ats,
                  ifSigs   = map toIfaceClassOp op_stuff,
@@ -1532,17 +1545,23 @@ classToIfaceDecl clas
       = classExtraBigSig clas
     tycon = classTyCon clas
 
+    (env1, clas_tyvars') = tidyTyVarBndrs env clas_tyvars
+    
     toIfaceAT :: ClassATItem -> IfaceAT
     toIfaceAT (tc, defs)
-      = IfaceAT (tyThingToIfaceDecl (ATyCon tc))
-                (map to_if_at_def defs)
+      = IfaceAT (tyConToIfaceDecl env1 tc) (map to_if_at_def defs)
       where
         to_if_at_def (ATD tvs pat_tys ty _loc)
-          = IfaceATD (toIfaceTvBndrs tvs) (map toIfaceType pat_tys) (toIfaceType ty)
+          = IfaceATD (toIfaceTvBndrs tvs') 
+                     (map (tidyToIfaceType env2) pat_tys) 
+                     (tidyToIfaceType env2 ty)
+          where
+            (env2, tvs') = tidyTyClTyVarBndrs env1 tvs
 
     toIfaceClassOp (sel_id, def_meth)
         = ASSERT(sel_tyvars == clas_tyvars)
-          IfaceClassOp (getOccName sel_id) (toDmSpec def_meth) (toIfaceType op_ty)
+          IfaceClassOp (getOccName sel_id) (toDmSpec def_meth) 
+                       (tidyToIfaceType env1 op_ty)
         where
                 -- Be careful when splitting the type, because of things
                 -- like         class Foo a where
@@ -1556,8 +1575,30 @@ classToIfaceDecl clas
     toDmSpec (GenDefMeth _) = GenericDM
     toDmSpec (DefMeth _)    = VanillaDM
 
-    toIfaceFD (tvs1, tvs2) = (map getFS tvs1, map getFS tvs2)
+    toIfaceFD (tvs1, tvs2) = (map (getFS . tidyTyVar env1) tvs1, 
+                              map (getFS . tidyTyVar env1) tvs2)
 
+--------------------------
+tidyToIfaceType :: TidyEnv -> Type -> IfaceType
+tidyToIfaceType env ty = toIfaceType (tidyType env ty)
+
+tidyToIfaceContext :: TidyEnv -> ThetaType -> IfaceContext
+tidyToIfaceContext env theta = map (tidyToIfaceType env) theta
+
+tidyTyClTyVarBndrs :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
+tidyTyClTyVarBndrs env tvs = mapAccumL tidyTyClTyVarBndr env tvs
+
+tidyTyClTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
+-- If the type variable "binder" is in scope, don't re-bind it
+-- In a class decl, for example, the ATD binders mention 
+-- (amd must mention) the class tyvars
+tidyTyClTyVarBndr env@(_, subst) tv
+ | Just tv' <- lookupVarEnv subst tv = (env, tv')
+ | otherwise                         = tidyTyVarBndr env tv
+
+tidyTyVar :: TidyEnv -> TyVar -> TyVar
+tidyTyVar (_, subst) tv = lookupVarEnv subst tv `orElse` tv
+   -- TcType.tidyTyVarOcc messes around with FlatSkols
 
 getFS :: NamedThing a => a -> FastString
 getFS x = occNameFS (getOccName x)
index 7808c6b..1e30d7c 100644 (file)
@@ -30,7 +30,7 @@ module TcHsType (
         tcHsContext, tcInferApps, tcHsArgTys,
 
         ExpKind(..), ekConstraint, expArgKind, checkExpectedKind,
-        bindScopedKindVars, kindGeneralize,
+        kindGeneralize,
 
                -- Sort-checking kinds
        tcLHsKind, 
@@ -292,7 +292,7 @@ tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
 -- The result is not necessarily zonked, and has not been checked for validity
 tcCheckHsTypeAndGen hs_ty kind
   = do { ty  <- tc_hs_type hs_ty (EK kind (ptext (sLit "Expected")))
-       ; kvs <- kindGeneralize (tyVarsOfType ty)
+       ; kvs <- kindGeneralize (tyVarsOfType ty) []
        ; return (mkForAllTys kvs ty) }
 \end{code}
 
@@ -583,16 +583,10 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
                ty = dataConUserType dc
                tc = buildPromotedDataCon dc
 
-           AFamDataCon -> bad_promote (ptext (sLit "it comes from a data family instance"))
-           ARecDataCon -> bad_promote (ptext (sLit "it is defined and used in the same recursive group"))
+           APromotionErr err -> promotionErr name err
 
            _  -> wrongThingErr "type" thing name }
   where
-    bad_promote reason
-      = failWithTc (hang (ptext (sLit "You can't use data constructor") <+> quotes (ppr name)
-                          <+> ptext (sLit "here")) 
-                       2 (parens reason))
-
     get_loopy_tc name
       = do { env <- getGblEnv
            ; case lookupNameEnv (tcg_type_env env) name of
@@ -793,42 +787,53 @@ then we'd also need
                           since we only have BOX for a super kind)
 
 \begin{code}
-bindScopedKindVars :: [Name] -> ([KindVar] -> TcM a) -> TcM a
+kcScopedKindVars :: [Name] -> TcM a -> TcM a
 -- Given some tyvar binders like [a (b :: k -> *) (c :: k)]
 -- bind each scoped kind variable (k in this case) to a fresh
 -- kind skolem variable
-bindScopedKindVars kv_ns thing_inside 
-  = tcExtendTyVarEnv kvs (thing_inside kvs)
-  where
-    kvs = map mkKindSigVar kv_ns
+kcScopedKindVars kv_ns thing_inside 
+  = do { kvs <- mapM (\n -> newSigTyVar n superKind) kv_ns
+                     -- NB: use mutable signature variables
+       ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside } 
 
 kcHsTyVarBndrs :: Bool    -- Default UserTyVar to *
+                          -- and use KindVars not meta kind vars
                -> LHsTyVarBndrs Name 
               -> ([TcKind] -> TcM r)
               -> TcM r
-kcHsTyVarBndrs default_to_star (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
-  = bindScopedKindVars kvs $ \ _ -> 
+kcHsTyVarBndrs full_kind_sig (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
+  = do { kvs <- if full_kind_sig 
+                then return (map mkKindSigVar kv_ns)
+                else mapM (\n -> newSigTyVar n superKind) kv_ns
+       ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
     do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs
-       ; tcExtendKindEnv nks (thing_inside (map snd nks)) }
+       ; tcExtendKindEnv nks (thing_inside (map snd nks)) } }
   where
     kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind)
     kc_hs_tv (UserTyVar n)     
       = do { mb_thing <- tcLookupLcl_maybe n
            ; kind <- case mb_thing of
-                              Just (AThing k) -> return k
-                              _ | default_to_star -> return liftedTypeKind
-                                | otherwise       -> newMetaKindVar
+                              Just (AThing k)   -> return k
+                              _ | full_kind_sig -> return liftedTypeKind
+                                | otherwise     -> newMetaKindVar
            ; return (n, kind) }
     kc_hs_tv (KindedTyVar n k) 
       = do { kind <- tcLHsKind k
            ; return (n, kind) }
 
+tcScopedKindVars :: [Name] -> TcM a -> TcM a
+-- Given some tyvar binders like [a (b :: k -> *) (c :: k)]
+-- bind each scoped kind variable (k in this case) to a fresh
+-- kind skolem variable
+tcScopedKindVars kv_ns thing_inside 
+  = tcExtendTyVarEnv (map mkKindSigVar kv_ns) thing_inside
+
 tcHsTyVarBndrs :: LHsTyVarBndrs Name 
               -> ([TyVar] -> TcM r)
               -> TcM r
 -- Bind the type variables to skolems, each with a meta-kind variable kind
 tcHsTyVarBndrs (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
-  = bindScopedKindVars kvs $ \ _ -> 
+  = tcScopedKindVars kvs $
     do { tvs <- mapM tcHsTyVarBndr hs_tvs
        ; traceTc "tcHsTyVarBndrs" (ppr hs_tvs $$ ppr tvs)
        ; tcExtendTyVarEnv tvs (thing_inside tvs) }
@@ -857,13 +862,13 @@ tcHsTyVarBndr (L _ hs_tv)
        ; return (mkTcTyVar name kind (SkolemTv False)) } } }
 
 ------------------
-kindGeneralize :: TyVarSet -> TcM [KindVar]
-kindGeneralize tkvs
-  = do { gbl_tvs  <- tcGetGlobalTyVars -- Already zonked
-       ; tidy_env <- tcInitTidyEnv
-       ; tkvs     <- zonkTyVarsAndFV tkvs
+kindGeneralize :: TyVarSet -> [Name] -> TcM [KindVar]
+kindGeneralize tkvs _names_to_avoid
+  = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
+       ; tkvs    <- zonkTyVarsAndFV tkvs
        ; let kvs_to_quantify = filter isKindVar (varSetElems (tkvs `minusVarSet` gbl_tvs))
-                -- Any type varaibles in tkvs will be in scope,
+                -- ToDo: remove the (filter isKindVar)
+                -- Any type variables in tkvs will be in scope,
                 -- and hence in gbl_tvs, so after removing gbl_tvs
                 -- we should only have kind variables left
                --
@@ -873,14 +878,16 @@ kindGeneralize tkvs
                 -- unification variable 'alpha', with no biding forall.  We don't
                 -- want to kind-quantify it!
 
-             (_, tidy_kvs_to_quantify) = tidyTyVarBndrs tidy_env kvs_to_quantify
-                           -- We do not get a later chance to tidy!
-
+       ; traceTc "kindGeneralise" (vcat [ppr kvs_to_quantify])
        ; ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify $$ ppr tkvs)
-             -- This assertion is obviosy true because of the filter isKindVar
+             -- This assertion is obviosly true because of the filter isKindVar
              -- but we'll remove that when reorganising TH, and then the assertion
              -- will mean something
-         zonkQuantifiedTyVars tidy_kvs_to_quantify }
+
+             -- If we tidied the kind variables, which should all be mutable,
+             -- this 'zonkQuantifiedTyVars' update the original TyVar to point to
+             -- the tided and skolemised one
+         zonkQuantifiedTyVars kvs_to_quantify }
 \end{code}
 
 Note [Kind generalisation]
@@ -937,7 +944,7 @@ kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> (TcKind -> TcM a) -> TcM a
 -- Used for the type variables of a type or class decl,
 -- when doing the initial kind-check.  
 kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
-  = bindScopedKindVars kvs $ \ _ -> 
+  = kcScopedKindVars kvs $
     do         { tc_kind <- kcLookupKind name
        ; let (arg_ks, res_k) = splitKindFunTysN (length hs_tvs) tc_kind
                      -- There should be enough arrows, because
@@ -980,21 +987,24 @@ tcTyClTyVars :: Name -> LHsTyVarBndrs Name        -- LHS of the type or class decl
 --
 -- No need to freshen the k's because they are just skolem 
 -- constants here, and we are at top level anyway.
-tcTyClTyVars tycon tyvars thing_inside
-  = do { thing <- tcLookup tycon
+tcTyClTyVars tycon (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
+  = kcScopedKindVars kvs $
+    do { thing <- tcLookup tycon
        ; let { kind = case thing of
                         AThing kind -> kind
                         _ -> panic "tcTyClTyVars"
                      -- We only call tcTyClTyVars during typechecking in
                      -- TcTyClDecls, where the local env is extended with
                      -- the generalized_env (mapping Names to AThings).
-             ; (kvs, body) = splitForAllTys kind
-             ; (kinds, res) = splitKindFunTysN (length names) body
-             ; names = hsLTyVarNames tyvars
-             ; tvs = zipWith mkTyVar names kinds
-             ; all_vs = kvs ++ tvs }
-       ; tcExtendTyVarEnv all_vs (thing_inside all_vs res) }
-
+             ; (kvs, body)  = splitForAllTys kind
+             ; (kinds, res) = splitKindFunTysN (length hs_tvs) body }
+       ; tvs <- zipWithM tc_hs_tv hs_tvs kinds
+       ; tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs) res) }
+  where
+    tc_hs_tv (L _ (UserTyVar n))        kind = return (mkTyVar n kind)
+    tc_hs_tv (L _ (KindedTyVar n hs_k)) kind = do { tc_kind <- tcLHsKind hs_k
+                                                  ; _ <- unifyKind kind tc_kind
+                                                  ; return (mkTyVar n kind) }
 
 -----------------------------------
 tcDataKindSig :: Kind -> TcM [TyVar]
@@ -1384,19 +1394,19 @@ tc_kind_var_app name arg_kis
 
 -- General case
 tc_kind_var_app name arg_kis
-  = do { (_errs, mb_thing) <- tryTc (tcLookup name)
-       ;  case mb_thing of
-          Just (AGlobal (ATyCon tc))
+  = do { thing <- tcLookup name
+       ; case thing of
+          AGlobal (ATyCon tc)
             -> do { data_kinds <- xoptM Opt_DataKinds
                   ; unless data_kinds $ addErr (dataKindsErr name)
                   ; case isPromotableTyCon tc of
                       Just n | n == length arg_kis ->
                         return (mkTyConApp (buildPromotedTyCon tc) arg_kis)
-                      Just _  -> err tc "is not fully applied"
-                      Nothing -> err tc "is not promotable" }
+                      Just _  -> tycon_err tc "is not fully applied"
+                      Nothing -> tycon_err tc "is not promotable" }
 
           -- A lexically scoped kind variable
-          Just (ATyVar _ kind_var) 
+          ATyVar _ kind_var 
              | not (isKindVar kind_var) 
              -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr kind_var)
                             <+> ptext (sLit "used as a kind"))
@@ -1408,19 +1418,32 @@ tc_kind_var_app name arg_kis
              -> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
 
           -- It is in scope, but not what we expected
-          Just thing -> wrongThingErr "promoted type" thing name
-
-          -- It is not in scope, but it passed the renamer: staging error
-          Nothing    
-             -> -- ASSERT2 ( isTyConName name, ppr name )
-               do { env <- getLclEnv
-                  ; 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")) } }
+          AThing _ 
+             | isTyVarName name 
+             -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr name)
+                            <+> ptext (sLit "used in a kind"))
+             | otherwise 
+             -> failWithTc (hang (ptext (sLit "Type constructor") <+> quotes (ppr name)
+                                  <+> ptext (sLit "used in a kind"))
+                              2 (ptext (sLit "inside its own recursive group"))) 
+
+           APromotionErr err -> promotionErr name err
+
+          _ -> wrongThingErr "promoted type" thing name
+                -- This really should not happen
+     }
   where 
-   err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
-                        <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
+   tycon_err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
+                                  <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
+
+promotionErr :: Name -> PromotionErr -> TcM a
+promotionErr name err
+  = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> ptext (sLit "cannot be used here"))
+                   2 (parens reason))
+  where
+    reason = case err of
+               FamDataConPE -> ptext (sLit "it comes from a data family instance")
+               _ -> ptext (sLit "it is defined and used in the same recursive group")
 \end{code}
 
 %************************************************************************
index d4eb931..778a4b2 100644 (file)
@@ -967,8 +967,8 @@ tcTyClsInstDecls :: ModDetails
                           HsValBinds Name)    -- Supporting bindings for derived instances
 
 tcTyClsInstDecls boot_details tycl_decls inst_decls deriv_decls
- = tcExtendTcTyThingEnv [(con, AFamDataCon) | lid <- inst_decls
-                                            , con <- get_cons lid ] $
+ = tcExtendTcTyThingEnv [(con, APromotionErr FamDataConPE) 
+                        | lid <- inst_decls, con <- get_cons lid ] $
       -- Note [AFamDataCon: not promoting data family constructors]
    do { tcg_env <- tcTyAndClassDecls boot_details tycl_decls ;
       ; setGblEnv tcg_env $
@@ -1890,7 +1890,9 @@ ppr_tydecls tycons
   = vcat (map ppr_tycon (sortLe le_sig tycons))
   where
     le_sig tycon1 tycon2 = getOccName tycon1 <= getOccName tycon2
-    ppr_tycon tycon = ppr (tyThingToIfaceDecl (ATyCon tycon))
+    ppr_tycon tycon = vcat [ ppr (tyConName tycon) <+> dcolon <+> ppr (tyConKind tycon)
+                              -- Temporarily print the kind signature too
+                           , ppr (tyThingToIfaceDecl (ATyCon tycon)) ]
 
 ppr_rules :: [CoreRule] -> SDoc
 ppr_rules [] = empty
index 1ed3d0d..ac35c37 100644 (file)
@@ -38,7 +38,8 @@ module TcRnTypes(
        WhereFrom(..), mkModDeps,
 
        -- Typechecker types
-       TcTypeEnv, TcTyThing(..), pprTcTyThingCategory, 
+       TcTypeEnv, TcTyThing(..), PromotionErr(..), 
+        pprTcTyThingCategory, pprPECategory,
 
        -- Template Haskell
        ThStage(..), topStage, topAnnStage, topSpliceStage,
@@ -580,10 +581,17 @@ data TcTyThing
                      -- Can be a mono-kind or a poly-kind; in TcTyClsDcls see
                      -- Note [Type checking recursive type and class declarations]
 
-  | AFamDataCon      -- Data constructor for a data family
+  | APromotionErr PromotionErr 
+
+data PromotionErr 
+  = TyConPE          -- TyCon used in a kind before we are ready
+                     --     data T :: T -> * where ...
+  | ClassPE          -- Ditto Class
+
+  | FamDataConPE     -- Data constructor for a data family
                      -- See Note [AFamDataCon: not promoting data family constructors] in TcRnDriver
 
-  | ARecDataCon      -- Data constructor in a reuursive loop
+  | RecDataConPE     -- Data constructor in a reuursive loop
                      -- See Note [ARecDataCon: recusion and promoting data constructors] in TcTyClsDecls
 
 instance Outputable TcTyThing where    -- Debugging only
@@ -595,16 +603,26 @@ instance Outputable TcTyThing where       -- Debugging only
                                 <+> ppr (tct_level elt))
    ppr (ATyVar tv _)    = text "Type variable" <+> quotes (ppr tv)
    ppr (AThing k)       = text "AThing" <+> ppr k
-   ppr AFamDataCon      = text "AFamDataCon"
-   ppr ARecDataCon      = text "ARecDataCon"
+   ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
+
+instance Outputable PromotionErr where
+  ppr ClassPE      = text "ClassPE"
+  ppr TyConPE      = text "TyConPE"
+  ppr FamDataConPE = text "FamDataConPE"
+  ppr RecDataConPE = text "RecDataConPE"
 
 pprTcTyThingCategory :: TcTyThing -> SDoc
-pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
-pprTcTyThingCategory (ATyVar {})     = ptext (sLit "Type variable")
-pprTcTyThingCategory (ATcId {})      = ptext (sLit "Local identifier")
-pprTcTyThingCategory (AThing {})     = ptext (sLit "Kinded thing")
-pprTcTyThingCategory AFamDataCon     = ptext (sLit "Family data con")
-pprTcTyThingCategory ARecDataCon     = ptext (sLit "Recursive data con")
+pprTcTyThingCategory (AGlobal thing)    = pprTyThingCategory thing
+pprTcTyThingCategory (ATyVar {})        = ptext (sLit "Type variable")
+pprTcTyThingCategory (ATcId {})         = ptext (sLit "Local identifier")
+pprTcTyThingCategory (AThing {})        = ptext (sLit "Kinded thing")
+pprTcTyThingCategory (APromotionErr pe) = pprPECategory pe
+
+pprPECategory :: PromotionErr -> SDoc
+pprPECategory ClassPE      = ptext (sLit "Class")
+pprPECategory TyConPE      = ptext (sLit "Type constructor")
+pprPECategory FamDataConPE = ptext (sLit "Data constructor")
+pprPECategory RecDataConPE = ptext (sLit "Data constructor")
 \end{code}
 
 
index 4f2dab0..f4f8c96 100644 (file)
@@ -166,7 +166,8 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
        ; zonked_forall_tvs <- zonkTyVarsAndFV forall_tvs
        ; gbl_tvs           <- tcGetGlobalTyVars             -- Already zonked
        ; let tvs_to_quantify = varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
-       ; qkvs <- kindGeneralize $ tyVarsOfTypes (map tyVarKind tvs_to_quantify)
+       ; qkvs <- kindGeneralize (tyVarsOfTypes (map tyVarKind tvs_to_quantify))
+                                (map getName tvs_to_quantify)
        ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
        ; let qtkvs = qkvs ++ qtvs
        ; traceTc "tcRule" (vcat [ doubleQuotes (ftext name)
index a22697d..ab28804 100644 (file)
@@ -129,9 +129,9 @@ tcTyClGroup boot_details tyclds
 
                  -- Populate environment with knot-tied ATyCon for TyCons
                  -- NB: if the decls mention any ill-staged data cons
-                 -- (see Note [ANothing] in typecheck/TcRnTypes.lhs) we
-                 -- will have failed already in kcTyClGroup, so no worries here
-           ; tcExtendRecEnv (zipRecTyClss tyclds rec_tyclss) $
+                 -- (see Note [ARecDataCon: Recusion and promoting data constructors]
+                 -- we will have failed already in kcTyClGroup, so no worries here
+           ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
 
                  -- Also extend the local type envt with bindings giving
                  -- the (polymorphic) kind of each knot-tied TyCon or Class
@@ -147,7 +147,7 @@ tcTyClGroup boot_details tyclds
            -- expects well-formed TyCons
        ; tcExtendGlobalEnv tyclss $ do
        { traceTc "Starting validity check" (ppr tyclss)
-       ; mapM_ (addLocM checkValidTyCl) tyclds
+       ; mapM_ (addLocM checkValidTyCl) (flattenTyClDecls tyclds)
 
            -- Step 4: Add the implicit things;
            -- we want them in the environment because
@@ -163,16 +163,15 @@ tcAddImplicits tyclss
    implicit_things = concatMap implicitTyThings tyclss
    rec_sel_binds   = mkRecSelBinds tyclss
 
-zipRecTyClss :: TyClGroup Name
+zipRecTyClss :: [(Name, Kind)]
              -> [TyThing]           -- Knot-tied
              -> [(Name,TyThing)]
 -- Build a name-TyThing mapping for the things bound by decls
 -- being careful not to look at the [TyThing]
 -- The TyThings in the result list must have a visible ATyCon,
 -- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
-zipRecTyClss decls rec_things
-  = [ (name, ATyCon (get name))
-    | name <- tyClsBinders decls ]
+zipRecTyClss kind_pairs rec_things
+  = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
   where
     rec_type_env :: TypeEnv
     rec_type_env = mkTypeEnv rec_things
@@ -181,13 +180,12 @@ zipRecTyClss decls rec_things
                  Just (ATyCon tc) -> tc
                  other            -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
 
-tyClsBinders :: TyClGroup Name -> [Name]
--- Just the tycon and class binders of a group (not the data constructors)
-tyClsBinders decls
-  = concatMap get decls
-  where
-    get (L _ (ClassDecl { tcdLName = L _ n, tcdATs = ats })) = n : tyClsBinders ats
-    get (L _ d)                                              = [tcdName d]
+flattenTyClDecls :: [LTyClDecl Name] -> [LTyClDecl Name]
+-- Lift out the associated type declaraitons to top level
+flattenTyClDecls [] = []
+flattenTyClDecls (ld@(L _ d) : lds)
+  | isClassDecl d = ld : tcdATs d ++ flattenTyClDecls lds
+  | otherwise     = ld : flattenTyClDecls lds
 \end{code}
 
 
@@ -254,6 +252,7 @@ initial kind environment.  (This is handled by `allDecls').
 \begin{code}
 kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
 -- Kind check this group, kind generalize, and return the resulting local env
+-- This bindds the TyCons and Classes of the group, but not the DataCons
 -- See Note [Kind checking for type and class decls]
 kcTyClGroup decls
   = do { mod <- getModule
@@ -268,39 +267,49 @@ kcTyClGroup decls
 
          -- Step 1: Bind kind variables for non-synonyms
         ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
-       ; initial_kinds <- getInitialKinds TopLevel non_syn_decls
-
+       ; initial_kinds <- 
+                           getInitialKinds TopLevel non_syn_decls
         ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
-       ; tcl_env <- tcExtendTcTyThingEnv initial_kinds $  do
-                     do { -- Step 2: kind-check the synonyms, and extend envt
-                          tcl_env <- kcSynDecls (calcSynCycles syn_decls)
-                            -- Step 3: kind-check the synonyms
-                        ; setLclEnv tcl_env $
-                          do { mapM_ kcLTyClDecl non_syn_decls
-                             ; getLclTypeEnv } }
+
+        -- Step 2: Set initial envt, kind-check the synonyms
+       ; lcl_env <- tcExtendTcTyThingEnv initial_kinds $ 
+                     kcSynDecls (calcSynCycles syn_decls)
+
+        -- Step 3: Set extended envt, kind-check the non-synonyms
+        ; setLclEnv lcl_env $
+          mapM_ kcLTyClDecl non_syn_decls
 
             -- Step 4: generalisation
             -- Kind checking done for this group
              -- Now we have to kind generalize the flexis
-        ; res <- mapM (generalise tcl_env) (tyClsBinders decls) 
+        ; res <- mapM (generalise (tcl_env lcl_env)) (flattenTyClDecls decls)
 
         ; traceTc "kcTyClGroup result" (ppr res)
         ; return res }
 
   where
-    generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
+    generalise :: TcTypeEnv -> LTyClDecl Name -> TcM (Name, Kind)
     -- For polymorphic things this is a no-op
-    generalise kind_env name
-      = do { traceTc "Generalise type of" (ppr name)
+    generalise kind_env (L _ decl)
+      = do { let name = tcdName decl
+                 tvs  = tcdTyVars decl
            ; let kc_kind = case lookupNameEnv kind_env name of
                                Just (AThing k) -> k
                                _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
-           ; kvs <- kindGeneralize (tyVarsOfType kc_kind)
-           ; kc_kind' <- zonkTcKind kc_kind
+           ; kvs <- kindGeneralize (tyVarsOfType kc_kind) (hsLTyVarNames tvs)
+           ; kc_kind' <- zonkTcKind kc_kind    -- Make sure kc_kind' has the final,
+                                               -- skolemised kind variables
+           ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
            ; return (name, mkForAllTys kvs kc_kind') }
 
 getInitialKinds :: TopLevelFlag -> [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
-getInitialKinds top_lvl = concatMapM (addLocM (getInitialKind top_lvl))
+getInitialKinds top_lvl decls
+  = tcExtendTcTyThingEnv [ (tcdName d, APromotionErr (mk_promotion_err d))
+                         | L _ d <- flattenTyClDecls decls] $
+    concatMapM (addLocM (getInitialKind top_lvl)) decls
+  where
+    mk_promotion_err (ClassDecl {}) = ClassPE
+    mk_promotion_err _              = TyConPE
 
 getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
 -- Allocate a fresh kind variable for each TyCon and Class
@@ -311,8 +320,8 @@ getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
 --      Example: data T a b = ...
 --      return (T, kv1 -> kv2 -> kv3)
 --
--- ALSO for each datacon, return (dc, ANothing)
---      See Note [ANothing] in TcRnTypes
+-- ALSO for each datacon, return (dc, ARecDataCon)
+-- Note [ARecDataCon: Recusion and promoting data constructors]
 -- 
 -- No family instances are passed to getInitialKinds
 
@@ -347,14 +356,14 @@ getInitialKind top_lvl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcd
        ; let body_kind = mkArrowKinds arg_kinds res_k
              kvs       = varSetElems (tyVarsOfType body_kind)
              main_pr   = (name, AThing (mkForAllTys kvs body_kind))
-             inner_prs = [(unLoc (con_name con), ARecDataCon) | L _ con <- cons ]
+             inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
              -- See Note [ARecDataCon: Recusion and promoting data constructors]
        ; return (main_pr : inner_prs) }
  
   | TyData { td_cons = cons } <- defn
   = kcHsTyVarBndrs False ktvs $ \ arg_kinds -> 
     do { let main_pr   = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind))
-             inner_prs = [(unLoc (con_name con), ARecDataCon) | L _ con <- cons ]
+             inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
              -- See Note [ARecDataCon: Recusion and promoting data constructors]
        ; return (main_pr : inner_prs) }
 
@@ -622,13 +631,19 @@ tcTyDefn calc_isrec tc_name tvs kind
              final_tvs  = tvs ++ extra_tvs
        ; stupid_theta <- tcHsContext ctxt
        ; kind_signatures <- xoptM Opt_KindSignatures
-       ; existential_ok <- xoptM Opt_ExistentialQuantification
-       ; gadt_ok      <- xoptM Opt_GADTs
+       ; existential_ok  <- xoptM Opt_ExistentialQuantification
+       ; gadt_ok         <- xoptM Opt_GADTs
        ; is_boot        <- tcIsHsBoot  -- Are we compiling an hs-boot file?
        ; let ex_ok = existential_ok || gadt_ok -- Data cons can have existential context
 
              -- Check that we don't use kind signatures without Glasgow extensions
-       ; checkTc (kind_signatures || isNothing mb_ksig) (badSigTyDecl tc_name)
+       ; 
+       ; case mb_ksig of
+           Nothing   -> return ()
+           Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
+                           ; tc_kind <- tcLHsKind hs_k
+                           ; _ <- unifyKind kind tc_kind
+                           ; return () }
 
        ; dataDeclChecks tc_name new_or_data stupid_theta cons
 
@@ -717,7 +732,6 @@ tcSynFamInstDecl :: TyCon -> FamInstDecl Name -> TcM ([TyVar], [Type], Type)
 tcSynFamInstDecl fam_tc 
     (FamInstDecl { fid_pats = pats, fid_defn = defn@(TySynonym { td_synRhs = hs_ty }) })
   = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
-
        ; tcFamTyPats fam_tc pats (kcTyDefn defn) $ \tvs' pats' res_kind -> 
     do { rhs_ty <- tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
@@ -965,7 +979,7 @@ tcConDecl new_or_data existential_ok rep_tycon res_tmpl     -- Data types
 
              -- Generalise the kind variables (returning quantifed TcKindVars)
              -- and quanify the type variables (substiting their kinds)
-       ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty)
+       ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty) (map getName tvs)
        ; tvs <- zonkQuantifiedTyVars tvs
 
              -- Zonk to Types
@@ -1069,7 +1083,7 @@ rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
 
                -- /Lazily/ figure out the univ_tvs etc
                -- Each univ_tv is either a dc_tv or a tmpl_tv
-    (univ_tvs, eq_spec) = foldr choose ([], []) tidy_tmpl_tvs
+    (univ_tvs, eq_spec) = foldr choose ([], []) tmpl_tvs
     choose tmpl (univs, eqs)
       | Just ty <- lookupTyVar subst tmpl 
       = case tcGetTyVar_maybe ty of
@@ -1081,17 +1095,6 @@ rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
       | otherwise = pprPanic "tcResultType" (ppr res_ty)
     ex_tvs = dc_tvs `minusList` univ_tvs
 
-       -- NB: tmpl_tvs and dc_tvs are distinct, but
-       -- we want them to be *visibly* distinct, both for
-       -- interface files and general confusion.  So rename
-       -- the tc_tvs, since they are not used yet (no 
-       -- consequential renaming needed)
-    (_, tidy_tmpl_tvs) = mapAccumL tidy_one init_occ_env tmpl_tvs
-    init_occ_env       = initTidyOccEnv (map getOccName dc_tvs)
-    tidy_one env tv    = (env', setTyVarName tv (tidyNameOcc name occ'))
-             where
-                name = tyVarName tv
-                (env', occ') = tidyOccName env (getOccName name) 
 
 {-
 Note [Substitution in template variables kinds]
@@ -1258,9 +1261,6 @@ checkValidTyCl decl
            ATyCon tc -> do
                 traceTc "  of kind" (ppr (tyConKind tc))
                 checkValidTyCon tc
-                case decl of
-                  ClassDecl { tcdATs = ats } -> mapM_ (addLocM checkValidTyCl) ats
-                  _                          -> return ()
             AnId _    -> return ()  -- Generic default methods are checked
                                    -- with their parent class
             _         -> panic "checkValidTyCl"
index 5f567eb..7318891 100644 (file)
@@ -34,7 +34,8 @@ module Kind (
 
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
-        isConstraintKind, isConstraintOrLiftedKind, isKind, isKindVar,
+        isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
+        isKind, isKindVar,
         isSuperKind, isSuperKindTyCon,
         isLiftedTypeKindCon, isConstraintKindCon,
         isAnyKind, isAnyKindCon,
@@ -135,6 +136,12 @@ isConstraintOrLiftedKind (TyConApp tc _)
   = isConstraintKindCon tc || isLiftedTypeKindCon tc
 isConstraintOrLiftedKind _ = False
 
+returnsConstraintKind :: Kind -> Bool
+returnsConstraintKind (ForAllTy _ k)  = returnsConstraintKind k
+returnsConstraintKind (FunTy _ k)     = returnsConstraintKind k
+returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
+returnsConstraintKind _               = False
+
 --------------------------------------------
 --            Kinding for arrow (->)
 -- Says when a kind is acceptable on lhs or rhs of an arrow