Simplify kind generalisation, and fix Trac #7916
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 21 May 2013 11:29:54 +0000 (12:29 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 21 May 2013 11:30:43 +0000 (12:30 +0100)
A buglet that exposed an opportunity for some welcome refactoring
and simplification.  Main changes

* TcMType.zonkQuantifiedTyVars is replaced by quantifyTyVars, which
  does a bit more zonking (so that its clients do not need to)

* TcHsType.kindGeneralise becomes a bit simpler, and hands off
  to quantifyTyVars

* A bit of simplification of the hacky code in TcTyClsDcls.tcConDecl,
  where we figure out how to generalise the data constructor's type

* Improve the error message from badExistential when a constructor
  has an existential type, by printing the offending type

* Some consequential simplification in simplifyInfer.

compiler/basicTypes/VarSet.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcRules.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/utils/UniqSet.lhs

index 5c71db9..2c334d4 100644 (file)
@@ -24,7 +24,7 @@ module VarSet (
        isEmptyVarSet, delVarSet, delVarSetList, delVarSetByKey,
        minusVarSet, foldVarSet, filterVarSet, fixVarSet,
        lookupVarSet, mapVarSet, sizeVarSet, seqVarSet,
-       elemVarSetByKey
+       elemVarSetByKey, partitionVarSet
     ) where
 
 #include "HsVersions.h"
@@ -72,6 +72,7 @@ extendVarSet_C  :: (Var->Var->Var) -> VarSet -> Var -> VarSet
 delVarSetByKey :: VarSet -> Unique -> VarSet
 elemVarSetByKey :: Unique -> VarSet -> Bool
 fixVarSet       :: (VarSet -> VarSet) -> VarSet -> VarSet
+partitionVarSet :: (Var -> Bool) -> VarSet -> (VarSet, VarSet)
 
 emptyVarSet    = emptyUniqSet
 unitVarSet     = unitUniqSet
@@ -102,6 +103,7 @@ filterVarSet        = filterUniqSet
 extendVarSet_C = addOneToUniqSet_C
 delVarSetByKey = delOneFromUniqSet_Directly
 elemVarSetByKey        = elemUniqSet_Directly
+partitionVarSet = partitionUniqSet
 \end{code}
 
 \begin{code}
index dd0155e..38718ea 100644 (file)
@@ -196,7 +196,7 @@ tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty)
   = setSrcSpan loc $    -- The "In the type..." context comes from the caller
     do { inst_ty <- tc_inst_head hs_ty
        ; kvs     <- zonkTcTypeAndFV inst_ty
-       ; kvs     <- kindGeneralize kvs []
+       ; kvs     <- kindGeneralize kvs
        ; inst_ty <- zonkTcType (mkForAllTys kvs inst_ty)
        ; checkValidInstance user_ctxt lhs_ty inst_ty }
 
@@ -308,7 +308,7 @@ tcCheckHsTypeAndGen hs_ty kind
        ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
        ; traceTc "tcCheckHsTypeAndGen" (ppr ty)
        ; kvs <- zonkTcTypeAndFV ty 
-       ; kvs <- kindGeneralize kvs []
+       ; kvs <- kindGeneralize kvs
        ; return (mkForAllTys kvs ty) }
 \end{code}
 
@@ -947,11 +947,10 @@ tcHsTyVarBndr (L _ hs_tv)
        ; return (mkTcTyVar name kind (SkolemTv False)) } } }
 
 ------------------
-kindGeneralize :: TyVarSet -> [Name] -> TcM [KindVar]
-kindGeneralize tkvs _names_to_avoid
+kindGeneralize :: TyVarSet -> TcM [KindVar]
+kindGeneralize tkvs
   = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
-       ; tkvs    <- zonkTyVarsAndFV tkvs
-       ; let kvs_to_quantify = filter isKindVar (varSetElems (tkvs `minusVarSet` gbl_tvs))
+       ; quantifyTyVars gbl_tvs (filterVarSet isKindVar tkvs) }
                 -- ToDo: remove the (filter isKindVar)
                 -- Any type variables in tkvs will be in scope,
                 -- and hence in gbl_tvs, so after removing gbl_tvs
@@ -962,17 +961,6 @@ kindGeneralize tkvs _names_to_avoid
                 -- When typechecking the body of the bracket, we typecheck $t to a
                 -- unification variable 'alpha', with no biding forall.  We don't
                 -- want to kind-quantify it!
-
-       ; traceTc "kindGeneralise" (vcat [ppr kvs_to_quantify])
-       ; ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify $$ ppr tkvs)
-             -- 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
-
-             -- 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]
index 09e307a..cce760d 100644 (file)
@@ -52,7 +52,7 @@ module TcMType (
   zonkTcPredType, 
   skolemiseSigTv, skolemiseUnboundMetaTyVar,
   zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
-  zonkQuantifiedTyVar, zonkQuantifiedTyVars,
+  zonkQuantifiedTyVar, quantifyTyVars,
   zonkTcType, zonkTcTypes, zonkTcThetaType, 
 
   zonkTcKind, defaultKindVarToStar,
@@ -482,99 +482,60 @@ tcInstTyVarX subst tyvar
 
 %************************************************************************
 %*                                                                     *
-\subsection{Zonking -- the exernal interfaces}
+             Quantification
 %*                                                                     *
 %************************************************************************
 
-@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
-To improve subsequent calls to the same function it writes the zonked set back into
-the environment.
-
-\begin{code}
-tcGetGlobalTyVars :: TcM TcTyVarSet
-tcGetGlobalTyVars
-  = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
-       ; gbl_tvs  <- readMutVar gtv_var
-       ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
-       ; writeMutVar gtv_var gbl_tvs'
-       ; return gbl_tvs' }
-  where
-\end{code}
-
------------------  Type variables
-
-\begin{code}
-zonkTcTypeAndFV :: TcType -> TcM TyVarSet
--- Zonk a type and take its free variables
--- With kind polymorphism it can be essential to zonk *first*
--- so that we find the right set of free variables.  Eg
---    forall k1. forall (a:k2). a
--- where k2:=k1 is in the substitution.  We don't want
--- k2 to look free in this type!
-zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
-
-zonkTyVar :: TyVar -> TcM TcType
--- Works on TyVars and TcTyVars
-zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
-             | otherwise    = return (mkTyVarTy tv)
-   -- Hackily, when typechecking type and class decls
-   -- we have TyVars in scopeadded (only) in 
-   -- TcHsType.tcTyClTyVars, but it seems
-   -- painful to make them into TcTyVars there
+Note [quantifyTyVars]
+~~~~~~~~~~~~~~~~~~~~~
+quantifyTyVars is give the free vars of a type that we
+are about to wrap in a forall.
 
-zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
-zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
+It takes these free type/kind variables and 
+  1. Zonks them and remove globals
+  2. Partitions into type and kind variables (kvs1, tvs)
+  3. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
+  4. Calls zonkQuantifiedTyVar on each
 
-zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
-zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
-
------------------  Types
-zonkTyVarKind :: TyVar -> TcM TyVar
-zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
-                      ; return (setTyVarKind tv kind') }
-
-zonkTcTypes :: [TcType] -> TcM [TcType]
-zonkTcTypes tys = mapM zonkTcType tys
-
-zonkTcThetaType :: TcThetaType -> TcM TcThetaType
-zonkTcThetaType theta = mapM zonkTcPredType theta
-
-zonkTcPredType :: TcPredType -> TcM TcPredType
-zonkTcPredType = zonkTcType
-\end{code}
-
--------------------  These ...ToType, ...ToKind versions
-                    are used at the end of type checking
+Step (3) is often unimportant, because the kind variable is often
+also free in the type.  Eg
+     Typeable k (a::k)
+has free vars {k,a}.  But the type (see Trac #7916)
+    (f::k->*) (a::k)
+has free vars {f,a}, but we must add 'k' as well! Hence step (3).
 
 \begin{code}
-defaultKindVarToStar :: TcTyVar -> TcM Kind
--- We have a meta-kind: unify it with '*'
-defaultKindVarToStar kv 
-  = do { ASSERT ( isKindVar kv && isMetaTyVar kv )
-         writeMetaTyVar kv liftedTypeKind
-       ; return liftedTypeKind }
-
-zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
--- A kind variable k may occur *after* a tyvar mentioning k in its kind
+quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
+-- See Note [quantifyTyVars]
+-- The input is a mixture of type and kind variables; a kind variable k 
+--   may occur *after* a tyvar mentioning k in its kind
 -- Can be given a mixture of TcTyVars and TyVars, in the case of
--- associated type declarations
-zonkQuantifiedTyVars tyvars
-  = do { let (kvs, tvs) = partition isKindVar tyvars
-             (meta_kvs, skolem_kvs) 
-                  = partition (\kv -> isTcTyVar kv && isMetaTyVar kv) kvs
+--   associated type declarations
+
+quantifyTyVars gbl_tvs tkvs
+  = do { tkvs    <- zonkTyVarsAndFV tkvs
+       ; gbl_tvs <- zonkTyVarsAndFV gbl_tvs
+       ; let (kvs1, tvs) = partitionVarSet isKindVar (tkvs `minusVarSet` gbl_tvs)
+             kvs2 = varSetElems (foldVarSet add_kvs kvs1 tvs
+                                 `minusVarSet` gbl_tvs )
+             add_kvs tv kvs = tyVarsOfType (tyVarKind tv) `unionVarSet` kvs 
+                              -- NB kinds of tvs are zonked by zonkTyVarsAndFV
+             qtvs = varSetElems tvs                       
 
              -- In the non-PolyKinds case, default the kind variables
              -- to *, and zonk the tyvars as usual.  Notice that this
-             -- may make zonkQuantifiedTyVars return a shorter list
+             -- may make quantifyTyVars return a shorter list
              -- than it was passed, but that's ok
        ; poly_kinds <- xoptM Opt_PolyKinds
        ; qkvs <- if poly_kinds 
-                 then return kvs
-                 else WARN ( not (null skolem_kvs), ppr skolem_kvs )
-                      do { mapM_ defaultKindVarToStar meta_kvs
-                         ; return skolem_kvs }  -- Should be empty
-
-       ; mapM zonk_quant (qkvs ++ tvs) }
+                 then return kvs2
+                 else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
+                               is_meta kv = isTcTyVar kv && isMetaTyVar kv
+                         ; mapM_ defaultKindVarToStar meta_kvs
+                         ; WARN ( not (null skolem_kvs), ppr skolem_kvs )
+                           return skolem_kvs }  -- Should be empty
+
+       ; mapM zonk_quant (qkvs ++ qtvs) } 
            -- Because of the order, any kind variables
            -- mentioned in the kinds of the type variables refer to
            -- the now-quantified versions
@@ -618,6 +579,13 @@ zonkQuantifiedTyVar tv
              skolemiseUnboundMetaTyVar tv vanillaSkolemTv
       _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
 
+defaultKindVarToStar :: TcTyVar -> TcM Kind
+-- We have a meta-kind: unify it with '*'
+defaultKindVarToStar kv 
+  = do { ASSERT ( isKindVar kv && isMetaTyVar kv )
+         writeMetaTyVar kv liftedTypeKind
+       ; return liftedTypeKind }
+
 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
 -- Skolemise it, including giving it a new Name, so that
@@ -649,6 +617,137 @@ skolemiseSigTv tv
     skol_tv = setTcTyVarDetails tv (SkolemTv False)
 \end{code}
 
+Note [Zonking to Skolem]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We used to zonk quantified type variables to regular TyVars.  However, this
+leads to problems.  Consider this program from the regression test suite:
+
+  eval :: Int -> String -> String -> String
+  eval 0 root actual = evalRHS 0 root actual
+
+  evalRHS :: Int -> a
+  evalRHS 0 root actual = eval 0 root actual
+
+It leads to the deferral of an equality (wrapped in an implication constraint)
+
+  forall a. () => ((String -> String -> String) ~ a)
+
+which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
+In the meantime `a' is zonked and quantified to form `evalRHS's signature.
+This has the *side effect* of also zonking the `a' in the deferred equality
+(which at this point is being handed around wrapped in an implication
+constraint).
+
+Finally, the equality (with the zonked `a') will be handed back to the
+simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
+If we zonk `a' with a regular type variable, we will have this regular type
+variable now floating around in the simplifier, which in many places assumes to
+only see proper TcTyVars.
+
+We can avoid this problem by zonking with a skolem.  The skolem is rigid
+(which we require for a quantified variable), but is still a TcTyVar that the
+simplifier knows how to deal with.
+
+Note [Silly Type Synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+       type C u a = u  -- Note 'a' unused
+
+       foo :: (forall a. C u a -> C u a) -> u
+       foo x = ...
+
+       bar :: Num u => u
+       bar = foo (\t -> t + t)
+
+* From the (\t -> t+t) we get type  {Num d} =>  d -> d
+  where d is fresh.
+
+* Now unify with type of foo's arg, and we get:
+       {Num (C d a)} =>  C d a -> C d a
+  where a is fresh.
+
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+  because it does not 'really' mention a.  (see exactTyVarsOfType)
+  The arg to foo becomes
+       \/\a -> \t -> t+t
+
+* So we get a dict binding for Num (C d a), which is zonked to give
+       a = ()
+  [Note Sept 04: now that we are zonking quantified type variables
+  on construction, the 'a' will be frozen as a regular tyvar on
+  quantification, so the floated dict will still have type (C d a).
+  Which renders this whole note moot; happily!]
+
+* Then the \/\a abstraction has a zonked 'a' in it.
+
+All very silly.   I think its harmless to ignore the problem.  We'll end up with
+a \/\a in the final result but all the occurrences of a will be zonked to ()
+
+%************************************************************************
+%*                                                                     *
+              Zonking
+%*                                                                     *
+%************************************************************************
+
+@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
+To improve subsequent calls to the same function it writes the zonked set back into
+the environment.
+
+\begin{code}
+tcGetGlobalTyVars :: TcM TcTyVarSet
+tcGetGlobalTyVars
+  = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
+       ; gbl_tvs  <- readMutVar gtv_var
+       ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
+       ; writeMutVar gtv_var gbl_tvs'
+       ; return gbl_tvs' }
+  where
+\end{code}
+
+-----------------  Type variables
+
+\begin{code}
+zonkTcTypeAndFV :: TcType -> TcM TyVarSet
+-- Zonk a type and take its free variables
+-- With kind polymorphism it can be essential to zonk *first*
+-- so that we find the right set of free variables.  Eg
+--    forall k1. forall (a:k2). a
+-- where k2:=k1 is in the substitution.  We don't want
+-- k2 to look free in this type!
+zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
+
+zonkTyVar :: TyVar -> TcM TcType
+-- Works on TyVars and TcTyVars
+zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
+             | otherwise    = return (mkTyVarTy tv)
+   -- Hackily, when typechecking type and class decls
+   -- we have TyVars in scopeadded (only) in 
+   -- TcHsType.tcTyClTyVars, but it seems
+   -- painful to make them into TcTyVars there
+
+zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
+zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
+
+zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
+zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
+
+-----------------  Types
+zonkTyVarKind :: TyVar -> TcM TyVar
+zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
+                      ; return (setTyVarKind tv kind') }
+
+zonkTcTypes :: [TcType] -> TcM [TcType]
+zonkTcTypes tys = mapM zonkTcType tys
+
+zonkTcThetaType :: TcThetaType -> TcM TcThetaType
+zonkTcThetaType theta = mapM zonkTcPredType theta
+
+zonkTcPredType :: TcPredType -> TcM TcPredType
+zonkTcPredType = zonkTcType
+\end{code}
+
+---------------  Constraints
+
 \begin{code}
 zonkImplication :: Implication -> TcM (Bag Implication)
 zonkImplication implic@(Implic { ic_untch  = untch
@@ -806,71 +905,6 @@ zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
 zonkSkolemInfo skol_info = return skol_info
 \end{code}
 
-Note [Silly Type Synonyms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this:
-       type C u a = u  -- Note 'a' unused
-
-       foo :: (forall a. C u a -> C u a) -> u
-       foo x = ...
-
-       bar :: Num u => u
-       bar = foo (\t -> t + t)
-
-* From the (\t -> t+t) we get type  {Num d} =>  d -> d
-  where d is fresh.
-
-* Now unify with type of foo's arg, and we get:
-       {Num (C d a)} =>  C d a -> C d a
-  where a is fresh.
-
-* Now abstract over the 'a', but float out the Num (C d a) constraint
-  because it does not 'really' mention a.  (see exactTyVarsOfType)
-  The arg to foo becomes
-       \/\a -> \t -> t+t
-
-* So we get a dict binding for Num (C d a), which is zonked to give
-       a = ()
-  [Note Sept 04: now that we are zonking quantified type variables
-  on construction, the 'a' will be frozen as a regular tyvar on
-  quantification, so the floated dict will still have type (C d a).
-  Which renders this whole note moot; happily!]
-
-* Then the \/\a abstraction has a zonked 'a' in it.
-
-All very silly.   I think its harmless to ignore the problem.  We'll end up with
-a \/\a in the final result but all the occurrences of a will be zonked to ()
-
-Note [Zonking to Skolem]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We used to zonk quantified type variables to regular TyVars.  However, this
-leads to problems.  Consider this program from the regression test suite:
-
-  eval :: Int -> String -> String -> String
-  eval 0 root actual = evalRHS 0 root actual
-
-  evalRHS :: Int -> a
-  evalRHS 0 root actual = eval 0 root actual
-
-It leads to the deferral of an equality (wrapped in an implication constraint)
-
-  forall a. () => ((String -> String -> String) ~ a)
-
-which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
-In the meantime `a' is zonked and quantified to form `evalRHS's signature.
-This has the *side effect* of also zonking the `a' in the deferred equality
-(which at this point is being handed around wrapped in an implication
-constraint).
-
-Finally, the equality (with the zonked `a') will be handed back to the
-simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
-If we zonk `a' with a regular type variable, we will have this regular type
-variable now floating around in the simplifier, which in many places assumes to
-only see proper TcTyVars.
-
-We can avoid this problem by zonking with a skolem.  The skolem is rigid
-(which we require for a quantified variable), but is still a TcTyVar that the
-simplifier knows how to deal with.
 
 
 %************************************************************************
index db56540..2ef209c 100644 (file)
@@ -27,8 +27,6 @@ import TcEvidence( TcEvBinds(..) )
 import Type
 import Id
 import Name
-import Var
-import VarSet
 import SrcLoc
 import Outputable
 import FastString
@@ -162,16 +160,12 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
 
        ; let tpl_ids    = lhs_evs ++ id_bndrs
              forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
-       ; 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))
-                                (map getName tvs_to_quantify)
-       ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
-       ; let qtkvs = qkvs ++ qtvs
+       ; gbls  <- tcGetGlobalTyVars   -- Even though top level, there might be top-level
+                                      -- monomorphic bindings from the MR; test tc111
+       ; qtkvs <- quantifyTyVars gbls forall_tvs
        ; traceTc "tcRule" (vcat [ doubleQuotes (ftext name)
                                 , ppr forall_tvs
-                                , ppr qtvs
+                                , ppr qtkvs
                                 , ppr rule_ty
                                 , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] 
                   ])
index fbca878..226b486 100644 (file)
@@ -184,18 +184,6 @@ simplifyDefault theta
 *                                                                                 *
 ***********************************************************************************
 
-Note [Which variables to quantify]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose the inferred type of a function is
-   T kappa (alpha:kappa) -> Int
-where alpha is a type unification variable and 
-      kappa is a kind unification variable
-Then we want to quantify over *both* alpha and kappa.  But notice that
-kappa appears "at top level" of the type, as well as inside the kind
-of alpha.  So it should be fine to just look for the "top level"
-kind/type variables of the type, without looking transitively into the
-kinds of those type variables.
-
 \begin{code}
 simplifyInfer :: Bool
               -> Bool                  -- Apply monomorphism restriction
@@ -210,13 +198,9 @@ simplifyInfer :: Bool
                       TcEvBinds)    -- ... binding these evidence variables
 simplifyInfer _top_lvl apply_mr name_taus wanteds
   | isEmptyWC wanteds
-  = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
-       ; zonked_taus <- zonkTcTypes (map snd name_taus)
-       ; let tvs_to_quantify = varSetElems (tyVarsOfTypes zonked_taus `minusVarSet` gbl_tvs)
-                                      -- tvs_to_quantify can contain both kind and type vars
-                                      -- See Note [Which variables to quantify]
-       ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
-       ; return (qtvs, [], False, emptyTcEvBinds) }
+  = do { gbl_tvs <- tcGetGlobalTyVars
+       ; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
+       ; return (qtkvs, [], False, emptyTcEvBinds) }
 
   | otherwise
   = do { traceTc "simplifyInfer {"  $ vcat
@@ -258,7 +242,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
 
        ; tc_lcl_env <- TcRnMonad.getLclEnv
        ; let untch = tcl_untch tc_lcl_env
-       ; quant_pred_candidates   
+       ; quant_pred_candidates   -- Fully zonked
            <- if insolubleWC wanted_transformed 
               then return []   -- See Note [Quantification with errors]
               else do { gbl_tvs <- tcGetGlobalTyVars
@@ -280,52 +264,50 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
        --     unifications that may have happened
        ; gbl_tvs        <- tcGetGlobalTyVars
        ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
-       ; let init_tvs  = zonked_tau_tvs `minusVarSet` gbl_tvs
-             poly_qtvs = growThetaTyVars quant_pred_candidates init_tvs 
+       ; let poly_qtvs = growThetaTyVars quant_pred_candidates zonked_tau_tvs
                          `minusVarSet` gbl_tvs
              pbound    = filter (quantifyPred poly_qtvs) quant_pred_candidates
              
             -- Monomorphism restriction
-             mr_qtvs        = init_tvs `minusVarSet` constrained_tvs
-             constrained_tvs = tyVarsOfTypes quant_pred_candidates
+             constrained_tvs = tyVarsOfTypes pbound `unionVarSet` gbl_tvs
             mr_bites        = apply_mr && not (null pbound)
 
-             (qtvs, bound) | mr_bites  = (mr_qtvs,   [])
-                           | otherwise = (poly_qtvs, pbound)
+       ; (qtvs, bound) <- if mr_bites 
+                          then do { qtvs <- quantifyTyVars constrained_tvs zonked_tau_tvs
+                                  ; return (qtvs, []) }
+                          else do { qtvs <- quantifyTyVars gbl_tvs poly_qtvs
+                                  ; return (qtvs, pbound) }
              
        ; traceTc "simplifyWithApprox" $
          vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
               , ptext (sLit "pbound =") <+> ppr pbound
-              , ptext (sLit "init_qtvs =") <+> ppr init_tvs 
-              , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs ]
-
-       ; if isEmptyVarSet qtvs && null bound
-         then do { traceTc "} simplifyInfer/no quantification" empty                   
+              , ptext (sLit "bbound =") <+> ppr bound
+              , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs
+              , ptext (sLit "constrained_tvs =") <+> ppr constrained_tvs
+              , ptext (sLit "mr_bites =") <+> ppr mr_bites
+              , ptext (sLit "qtvs =") <+> ppr qtvs ]
+
+       ; if null qtvs && null bound
+         then do { traceTc "} simplifyInfer/no implication needed" empty                   
                  ; emitConstraints wanted_transformed
                     -- Includes insolubles (if -fdefer-type-errors)
                     -- as well as flats and implications
                  ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
          else do
 
-       { traceTc "simplifyApprox" $ 
-         ptext (sLit "bound are =") <+> ppr bound 
-         
-            -- Step 4, zonk quantified variables 
-       ; let minimal_flat_preds = mkMinimalBySCs bound
+      {     -- Step 7) Emit an implication
+         let minimal_flat_preds = mkMinimalBySCs bound
              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
                                    | (name, ty) <- name_taus ]
                         -- Don't add the quantified variables here, because
                         -- they are also bound in ic_skols and we want them to be
                         -- tidied uniformly
 
-       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
-
-            -- Step 7) Emit an implication
        ; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_flat_preds
        ; let implic = Implic { ic_untch    = pushUntouchables untch
-                             , ic_skols    = qtvs_to_return
+                             , ic_skols    = qtvs
                              , ic_fsks     = []  -- wanted_tansformed arose only from solveWanteds
                                                  -- hence no flatten-skolems (which come from givens)
                              , ic_given    = minimal_bound_ev_vars
@@ -339,11 +321,11 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
              vcat [ ptext (sLit "implic =") <+> ppr implic
                        -- ic_skols, ic_given give rest of result
-                  , ptext (sLit "qtvs =") <+> ppr qtvs_to_return
+                  , ptext (sLit "qtvs =") <+> ppr qtvs
                   , ptext (sLit "spb =") <+> ppr quant_pred_candidates
                   , ptext (sLit "bound =") <+> ppr bound ]
 
-       ; return ( qtvs_to_return, minimal_bound_ev_vars
+       ; return ( qtvs, minimal_bound_ev_vars
                 , mr_bites,  TcEvBinds ev_binds_var) } }
 
 quantifyPred :: TyVarSet           -- Quantifying over these
index d20c6ff..2561bd9 100644 (file)
@@ -398,8 +398,13 @@ tc_bracket _ (TypBr typ)
         -- Result type is Type (= Q Typ)
 
 tc_bracket _ (DecBrG decls)
-  = do  { _ <- tcTopSrcDecls emptyModDetails decls
-               -- Typecheck the declarations, dicarding the result
+  = do  { _ <- setXOptM Opt_ExistentialQuantification $
+                   -- This is an EGREGIOUS HACK to make T5737 work.  That test splices
+                   -- in a type in a data constructor arg type, and then we try to 
+                   -- check validity for the data type decl, which fails because of
+                   -- the pseudo-existential.  Stupid.  Will go away after the TH reorg
+               tcTopSrcDecls emptyModDetails decls
+               -- Typecheck the declarations, discarding the result
                -- We'll get all that stuff later, when we splice it in
 
                -- Top-level declarations in the bracket get unqualified names
index fd614f3..ed1c4a9 100644 (file)
@@ -286,13 +286,13 @@ kcTyClGroup decls
         ; return res }
 
   where
-    generalise :: TcTypeEnv -> Name -> LHsTyVarBndrs Name -> TcM (Name, Kind)
+    generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
     -- For polymorphic things this is a no-op
-    generalise kind_env name tvs
+    generalise kind_env name
       = do { 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) (hsLTyVarNames tvs)
+           ; kvs <- kindGeneralize (tyVarsOfType kc_kind)
            ; 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' ])
@@ -300,8 +300,8 @@ kcTyClGroup decls
 
     generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [(Name, Kind)]
     generaliseTCD kind_env (L _ decl)
-      | ClassDecl { tcdLName = (L _ name), tcdTyVars = tyvars, tcdATs = ats } <- decl
-      = do { first <- generalise kind_env name tyvars
+      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
+      = do { first <- generalise kind_env name
            ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
            ; return (first : rest) }
 
@@ -314,12 +314,12 @@ kcTyClGroup decls
 
       | otherwise
       -- Note: tcdTyVars is safe here because we've eliminated FamDecl and ForeignType
-      = do { res <- generalise kind_env (tcdName decl) (tcdTyVars decl)
+      = do { res <- generalise kind_env (tcdName decl)
            ; return [res] }
 
     generaliseFamDecl :: TcTypeEnv -> FamilyDecl Name -> TcM (Name, Kind)
-    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name, fdTyVars = tyvars })
-      = generalise kind_env name tyvars
+    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
+      = generalise kind_env name
 
 mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
 mk_thing_env [] = []
@@ -895,8 +895,7 @@ tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tva
             -- them into skolems, so that we don't subsequently
             -- replace a meta kind var with AnyK
             -- Very like kindGeneralize
-       ; tkvs <- zonkTyVarsAndFV (tyVarsOfTypes all_args)
-       ; qtkvs <- zonkQuantifiedTyVars (varSetElems tkvs)
+       ; qtkvs <- quantifyTyVars emptyVarSet (tyVarsOfTypes all_args)
 
             -- Zonk the patterns etc into the Type world
        ; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
@@ -997,8 +996,9 @@ tcConDecls new_or_data rep_tycon res_tmpl cons
   = mapM (addLocM (tcConDecl new_or_data rep_tycon res_tmpl)) cons
 
 tcConDecl :: NewOrData
-          -> TyCon              -- Representation tycon
-          -> ([TyVar], Type)    -- Return type template (with its template tyvars)
+          -> TyCon            -- Representation tycon
+          -> ([TyVar], Type)  -- Return type template (with its template tyvars)
+                              --    (tvs, T tys), where T is the family TyCon
           -> ConDecl Name
           -> TcM DataCon
 
@@ -1017,30 +1017,29 @@ tcConDecl new_or_data rep_tycon res_tmpl        -- Data types
                        (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 quantify the type variables (substiting their kinds)
-       ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty) (map getName tvs)
-       ; tvs <- zonkQuantifiedTyVars tvs
+             -- and quantify the type variables (substituting their kinds)
+             -- REMEMBER: 'tvs' and 'tkvs' are:
+             --    ResTyH98:  the *existential* type variables only
+             --    ResTyGADT: *all* the quantified type variables
+             -- c.f. the comment on con_qvars in HsDecls
+       ; tkvs <- case (res_ty, res_tmpl) of 
+                   (ResTyH98, (tvs, _)) -> quantifyTyVars (mkVarSet tvs) (tyVarsOfTypes arg_tys)
+                   (ResTyGADT ty, _)    -> quantifyTyVars emptyVarSet (tyVarsOfTypes (ty:arg_tys))
+                   
+       ; traceTc "tcConDecl" (ppr name $$ ppr arg_tys $$ ppr tvs $$ ppr tkvs)
 
              -- Zonk to Types
-       ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (kvs ++ tvs)
+       ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
        ; 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
 
-       ; let (univ_tvs, ex_tvs, eq_preds, res_ty')
-                = rejigConRes res_tmpl qtkvs res_ty
+       ; let (univ_tvs, ex_tvs, eq_preds, res_ty') = rejigConRes res_tmpl qtkvs res_ty
 
-       ; traceTc "tcConDecl 3" (ppr name)
+       ; traceTc "tcConDecl 3" (vcat [ppr name, ppr tkvs, ppr qtkvs, ppr univ_tvs, ppr ex_tvs])
        ; fam_envs <- tcGetFamInstEnvs
        ; buildDataCon fam_envs (unLoc name) is_infix
                       stricts field_lbls
@@ -1798,10 +1797,11 @@ badGadtDecl tc_name
          , nest 2 (parens $ ptext (sLit "Use -XGADTs to allow GADTs")) ]
 
 badExistential :: DataCon -> SDoc
-badExistential con_name
-  = hang (ptext (sLit "Data constructor") <+> quotes (ppr con_name) <+>
+badExistential con
+  = hang (ptext (sLit "Data constructor") <+> quotes (ppr con) <+>
                 ptext (sLit "has existential type variables, a context, or a specialised result type"))
-       2 (parens $ ptext (sLit "Use -XExistentialQuantification or -XGADTs to allow this"))
+       2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
+               , parens $ ptext (sLit "Use -XExistentialQuantification or -XGADTs to allow this") ]) 
 
 badStupidTheta :: Name -> SDoc
 badStupidTheta tc_name
index ccbd25a..1653f2d 100644 (file)
@@ -31,6 +31,7 @@ module UniqSet (
         isEmptyUniqSet,
         lookupUniqSet,
         uniqSetToList,
+        partitionUniqSet
     ) where
 
 import UniqFM
@@ -67,6 +68,7 @@ mapUniqSet :: (a -> b) -> UniqSet a -> UniqSet b
 elementOfUniqSet :: Uniquable a => a -> UniqSet a -> Bool
 elemUniqSet_Directly :: Unique -> UniqSet a -> Bool
 filterUniqSet :: (a -> Bool) -> UniqSet a -> UniqSet a
+partitionUniqSet :: (a -> Bool) -> UniqSet a -> (UniqSet a, UniqSet a)
 
 sizeUniqSet :: UniqSet a -> Int
 isEmptyUniqSet :: UniqSet a -> Bool
@@ -106,6 +108,7 @@ mapUniqSet = mapUFM
 elementOfUniqSet = elemUFM
 elemUniqSet_Directly = elemUFM_Directly
 filterUniqSet = filterUFM
+partitionUniqSet = partitionUFM
 
 sizeUniqSet = sizeUFM
 isEmptyUniqSet = isNullUFM