compiler/typecheck/TcGenDeriv.lhs

@@ -97,7 +97,7 @@ data DerivStuff     -- Please add this auxiliary stuff
   | DerivFamInst (FamInst)             -- New type family instances
 
   -- New top-level auxiliary bindings
-  | DerivHsBind ((Origin, LHsBind RdrName), LSig RdrName) -- Also used for SYB
+  | DerivHsBind (LHsBind RdrName, LSig RdrName) -- Also used for SYB
   | DerivInst (InstInfo RdrName)                -- New, auxiliary instances
 \end{code}
 
@@ -360,7 +360,7 @@ gen_Ord_binds loc tycon
     (nullary_cons, non_nullary_cons) = partition isNullarySrcDataCon tycon_data_cons
 
 
-    mkOrdOp :: OrdOp -> (Origin, LHsBind RdrName)
+    mkOrdOp :: OrdOp -> LHsBind RdrName
     -- Returns a binding   op a b = ... compares a and b according to op ....
     mkOrdOp op = mk_easy_FunBind loc (ordMethRdr op) [a_Pat, b_Pat] (mkOrdOpRhs op)
 
@@ -1352,7 +1352,7 @@ gen_Data_binds dflags loc tycon
     n_cons     = length data_cons
     one_constr = n_cons == 1
 
-    genDataTyCon :: ((Origin, LHsBind RdrName), LSig RdrName)
+    genDataTyCon :: (LHsBind RdrName, LSig RdrName)
     genDataTyCon        --  $dT
       = (mkHsVarBind loc rdr_name rhs,
          L loc (TypeSig [L loc rdr_name] sig_ty))
@@ -1364,7 +1364,7 @@ gen_Data_binds dflags loc tycon
               `nlHsApp` nlHsLit (mkHsString (showSDocOneLine dflags (ppr tycon)))
               `nlHsApp` nlList constrs
 
-    genDataDataCon :: DataCon -> ((Origin, LHsBind RdrName), LSig RdrName)
+    genDataDataCon :: DataCon -> (LHsBind RdrName, LSig RdrName)
     genDataDataCon dc       --  $cT1 etc
       = (mkHsVarBind loc rdr_name rhs,
          L loc (TypeSig [L loc rdr_name] sig_ty))
@@ -1943,7 +1943,7 @@ gen_Newtype_binds loc cls inst_tvs cls_tys rhs_ty
         (map (mkCoerceClassMethEqn cls inst_tvs cls_tys rhs_ty) (classMethods cls))
   where
     coerce_RDR = getRdrName coerceId
-    mk_bind :: Id -> Pair Type -> (Origin, LHsBind RdrName)
+    mk_bind :: Id -> Pair Type -> LHsBind RdrName
     mk_bind id (Pair tau_ty user_ty)
       = mkRdrFunBind (L loc meth_RDR) [mkSimpleMatch [] rhs_expr]
       where
@@ -1978,7 +1978,7 @@ The `tags' here start at zero, hence the @fIRST_TAG@ (currently one)
 fiddling around.
 
 \begin{code}
-genAuxBindSpec :: SrcSpan -> AuxBindSpec -> ((Origin, LHsBind RdrName), LSig RdrName)
+genAuxBindSpec :: SrcSpan -> AuxBindSpec -> (LHsBind RdrName, LSig RdrName)
 genAuxBindSpec loc (DerivCon2Tag tycon)
   = (mk_FunBind loc rdr_name eqns,
      L loc (TypeSig [L loc rdr_name] (L loc sig_ty)))
@@ -2024,7 +2024,7 @@ genAuxBindSpec loc (DerivMaxTag tycon)
                  data_cons -> toInteger ((length data_cons) - fIRST_TAG)
 
 type SeparateBagsDerivStuff = -- AuxBinds and SYB bindings
-                              ( Bag ((Origin, LHsBind RdrName), LSig RdrName)
+                              ( Bag (LHsBind RdrName, LSig RdrName)
                                 -- Extra bindings (used by Generic only)
                               , Bag TyCon   -- Extra top-level datatypes
                               , Bag (FamInst)           -- Extra family instances
@@ -2079,14 +2079,14 @@ mkParentType tc
 \begin{code}
 mk_FunBind :: SrcSpan -> RdrName
            -> [([LPat RdrName], LHsExpr RdrName)]
-           -> (Origin, LHsBind RdrName)
+           -> LHsBind RdrName
 mk_FunBind loc fun pats_and_exprs
   = mkRdrFunBind (L loc fun) matches
   where
     matches = [mkMatch p e emptyLocalBinds | (p,e) <-pats_and_exprs]
 
-mkRdrFunBind :: Located RdrName -> [LMatch RdrName (LHsExpr RdrName)] -> (Origin, LHsBind RdrName)
-mkRdrFunBind fun@(L loc fun_rdr) matches = (Generated, L loc (mkFunBind fun matches'))
+mkRdrFunBind :: Located RdrName -> [LMatch RdrName (LHsExpr RdrName)] -> LHsBind RdrName
+mkRdrFunBind fun@(L loc fun_rdr) matches = L loc (mkFunBind fun matches')
  where
    -- Catch-all eqn looks like
    --     fmap = error "Void fmap"

compiler/typecheck/TcGenGenerics.lhs

@@ -141,6 +141,7 @@ metaTyConsToDerivStuff tc metaDts =
         d_inst   = mk_inst dClas d_metaTycon d_dfun_name
         d_binds  = InstBindings { ib_binds = dBinds
                                 , ib_pragmas = []
+                                , ib_extensions = []
                                 , ib_standalone_deriving = False }
         d_mkInst = DerivInst (InstInfo { iSpec = d_inst, iBinds = d_binds })
         
@@ -150,6 +151,7 @@ metaTyConsToDerivStuff tc metaDts =
                   | (c, ds) <- myZip1 c_metaTycons c_dfun_names ]
         c_binds = [ InstBindings { ib_binds = c
                                  , ib_pragmas = []
+                                 , ib_extensions = []
                                  , ib_standalone_deriving = False }
                   | c <- cBinds ]
         c_mkInst = [ DerivInst (InstInfo { iSpec = is, iBinds = bs })
@@ -161,6 +163,7 @@ metaTyConsToDerivStuff tc metaDts =
                       (myZip2 s_metaTycons s_dfun_names)
         s_binds = [ [ InstBindings { ib_binds = s
                                    , ib_pragmas = []
+                                   , ib_extensions = []
                                    , ib_standalone_deriving = False }
                     | s <- ss ] | ss <- sBinds ]
         s_mkInst = map (map (\(is,bs) -> DerivInst (InstInfo { iSpec  = is
@@ -186,14 +189,13 @@ metaTyConsToDerivStuff tc metaDts =
 %************************************************************************
 
 \begin{code}
-get_gen1_constrained_tys :: TyVar -> [Type] -> [Type]
+get_gen1_constrained_tys :: TyVar -> Type -> [Type]
 -- called by TcDeriv.inferConstraints; generates a list of types, each of which
 -- must be a Functor in order for the Generic1 instance to work.
-get_gen1_constrained_tys argVar =
-  concatMap $ argTyFold argVar $ ArgTyAlg {
-    ata_rec0 = const [],
-    ata_par1 = [], ata_rec1 = const [],
-    ata_comp = (:)}
+get_gen1_constrained_tys argVar
+  = argTyFold argVar $ ArgTyAlg { ata_rec0 = const []
+                                , ata_par1 = [], ata_rec1 = const []
+                                , ata_comp = (:) }
 
 {-
 

compiler/typecheck/TcHsSyn.lhs

@@ -405,10 +405,8 @@ warnMissingSig msg id
 zonkMonoBinds :: ZonkEnv -> SigWarn -> LHsBinds TcId -> TcM (LHsBinds Id)
 zonkMonoBinds env sig_warn binds = mapBagM (zonk_lbind env sig_warn) binds
 
-zonk_lbind :: ZonkEnv -> SigWarn -> (Origin, LHsBind TcId) -> TcM (Origin, LHsBind Id)
-zonk_lbind env sig_warn (origin, lbind)
-  = do  { lbind' <- wrapLocM (zonk_bind env sig_warn) lbind
-        ; return (origin, lbind') }
+zonk_lbind :: ZonkEnv -> SigWarn -> LHsBind TcId -> TcM (LHsBind Id)
+zonk_lbind env sig_warn = wrapLocM (zonk_bind env sig_warn)
 
 zonk_bind :: ZonkEnv -> SigWarn -> HsBind TcId -> TcM (HsBind Id)
 zonk_bind env sig_warn bind@(PatBind { pat_lhs = pat, pat_rhs = grhss, pat_rhs_ty = ty})
@@ -506,11 +504,11 @@ zonkLTcSpecPrags env ps
 zonkMatchGroup :: ZonkEnv
                -> (ZonkEnv -> Located (body TcId) -> TcM (Located (body Id)))
                -> MatchGroup TcId (Located (body TcId)) -> TcM (MatchGroup Id (Located (body Id)))
-zonkMatchGroup env zBody (MG { mg_alts = ms, mg_arg_tys = arg_tys, mg_res_ty = res_ty })
+zonkMatchGroup env zBody (MG { mg_alts = ms, mg_arg_tys = arg_tys, mg_res_ty = res_ty, mg_origin = origin })
   = do  { ms' <- mapM (zonkMatch env zBody) ms
         ; arg_tys' <- zonkTcTypeToTypes env arg_tys
         ; res_ty'  <- zonkTcTypeToType env res_ty
-        ; return (MG { mg_alts = ms', mg_arg_tys = arg_tys', mg_res_ty = res_ty' }) }
+        ; return (MG { mg_alts = ms', mg_arg_tys = arg_tys', mg_res_ty = res_ty', mg_origin = origin }) }
 
 zonkMatch :: ZonkEnv
           -> (ZonkEnv -> Located (body TcId) -> TcM (Located (body Id)))

compiler/typecheck/TcHsType.lhs

@@ -207,18 +207,22 @@ tc_inst_head hs_ty
   = tc_hs_type hs_ty ekConstraint
 
 -----------------
-tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
--- Like tcHsSigTypeNC, but for the ...deriving( ty ) clause
-tcHsDeriv hs_ty 
-  = do { kind <- newMetaKindVar
-       ; ty   <- tcCheckHsTypeAndGen hs_ty kind
-                 -- Funny newtype deriving form
-                 -- 	forall a. C [a]
-                 -- where C has arity 2. Hence any-kinded result
-       ; ty   <- zonkSigType ty
+tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type], Kind)
+-- Like tcHsSigTypeNC, but for the ...deriving( C t1 ty2 ) clause
+-- Returns the C, [ty1, ty2, and the kind of C's *next* argument
+-- E.g.    class C (a::*) (b::k->k)
+--         data T a b = ... deriving( C Int )
+--    returns ([k], C, [k, Int],  k->k)
+-- Also checks that (C ty1 ty2 arg) :: Constraint
+-- if arg has a suitable kind
+tcHsDeriv hs_ty
+  = do { arg_kind <- newMetaKindVar
+       ; ty <- tcCheckHsTypeAndGen hs_ty (mkArrowKind arg_kind constraintKind)
+       ; ty       <- zonkSigType ty
+       ; arg_kind <- zonkSigType arg_kind
        ; let (tvs, pred) = splitForAllTys ty
        ; case getClassPredTys_maybe pred of
-           Just (cls, tys) -> return (tvs, cls, tys)
+           Just (cls, tys) -> return (tvs, cls, tys, arg_kind)
            Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
 
 -- Used for 'VECTORISE [SCALAR] instance' declarations
@@ -724,17 +728,17 @@ mkNakedAppTys ty1                tys2 = foldl AppTy ty1 tys2
 
 zonkSigType :: TcType -> TcM TcType
 -- Zonk the result of type-checking a user-written type signature
--- It may have kind varaibles in it, but no meta type variables
+-- It may have kind variables in it, but no meta type variables
 -- Because of knot-typing (see Note [Zonking inside the knot])
--- it may need to establish the Type invariants; 
+-- it may need to establish the Type invariants;
 -- hence the use of mkTyConApp and mkAppTy
 zonkSigType ty
   = go ty
   where
     go (TyConApp tc tys) = do tys' <- mapM go tys
                               return (mkTyConApp tc tys')
-                -- Key point: establish Type invariants! 
-                -- See Note [Zonking inside the knot] 
+                -- Key point: establish Type invariants!
+                -- See Note [Zonking inside the knot]
 
     go (LitTy n)         = return (LitTy n)
 

compiler/typecheck/TcInstDcls.lhs

@@ -572,6 +572,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                                    , iBinds = InstBindings
                                      { ib_binds = binds
                                      , ib_pragmas = uprags
+                                     , ib_extensions = []
                                      , ib_standalone_deriving = False } }
 
         ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts) }
@@ -628,10 +629,9 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
        ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname
 
          -- (0) Check it's an open type family
-       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
-       ; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
-       ; checkTc (isOpenSynFamilyTyCon fam_tc)
-                 (notOpenFamily fam_tc)
+       ; checkTc (isFamilyTyCon fam_tc)        (notFamily fam_tc)
+       ; checkTc (isSynFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
+       ; checkTc (isOpenSynFamilyTyCon fam_tc) (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym group
        ; co_ax_branch <- tcSynFamInstDecl fam_tc decl
@@ -887,9 +887,9 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                                   , abs_ev_vars = dfun_ev_vars
                                   , abs_exports = [export]
                                   , abs_ev_binds = sc_binds
-                                  , abs_binds = unitBag (Generated, dict_bind) }
+                                  , abs_binds = unitBag dict_bind }
 
-       ; return (unitBag (Generated, L loc main_bind) `unionBags`
+       ; return (unitBag (L loc main_bind) `unionBags`
                  listToBag meth_binds)
        }
  where
@@ -1168,22 +1168,26 @@ tcInstanceMethods :: DFunId -> Class -> [TcTyVar]
                   -> ([Located TcSpecPrag], PragFun)
                   -> [(Id, DefMeth)]
                   -> InstBindings Name
-                  -> TcM ([Id], [(Origin, LHsBind Id)])
+                  -> TcM ([Id], [LHsBind Id])
         -- The returned inst_meth_ids all have types starting
         --      forall tvs. theta => ...
 tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                   (spec_inst_prags, prag_fn)
                   op_items (InstBindings { ib_binds = binds
                                          , ib_pragmas = sigs
+                                         , ib_extensions = exts
                                          , ib_standalone_deriving
                                               = standalone_deriv })
   = do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
        ; let hs_sig_fn = mkHsSigFun sigs
        ; checkMinimalDefinition
-       ; mapAndUnzipM (tc_item hs_sig_fn) op_items }
+       ; set_exts exts $ mapAndUnzipM (tc_item hs_sig_fn) op_items }
   where
+    set_exts :: [ExtensionFlag] -> TcM a -> TcM a
+    set_exts es thing = foldr setXOptM thing es
+    
     ----------------------
-    tc_item :: HsSigFun -> (Id, DefMeth) -> TcM (Id, (Origin, LHsBind Id))
+    tc_item :: HsSigFun -> (Id, DefMeth) -> TcM (Id, LHsBind Id)
     tc_item sig_fn (sel_id, dm_info)
       = case findMethodBind (idName sel_id) binds of
             Just (user_bind, bndr_loc) 
@@ -1192,10 +1196,10 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                            ; tc_default sig_fn sel_id dm_info }
 
     ----------------------
-    tc_body :: HsSigFun -> Id -> Bool -> (Origin, LHsBind Name)
-            -> SrcSpan -> TcM (TcId, (Origin, LHsBind Id))
+    tc_body :: HsSigFun -> Id -> Bool -> LHsBind Name
+            -> SrcSpan -> TcM (TcId, LHsBind Id)
     tc_body sig_fn sel_id generated_code rn_bind bndr_loc
-      = add_meth_ctxt sel_id generated_code (snd rn_bind) $
+      = add_meth_ctxt sel_id generated_code rn_bind $
         do { traceTc "tc_item" (ppr sel_id <+> ppr (idType sel_id))
            ; (meth_id, local_meth_sig) <- setSrcSpan bndr_loc $
                                           mkMethIds sig_fn clas tyvars dfun_ev_vars
@@ -1211,12 +1215,12 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
            ; return (meth_id1, bind) }
 
     ----------------------
-    tc_default :: HsSigFun -> Id -> DefMeth -> TcM (TcId, (Origin, LHsBind Id))
+    tc_default :: HsSigFun -> Id -> DefMeth -> TcM (TcId, LHsBind Id)
 
     tc_default sig_fn sel_id (GenDefMeth dm_name)
       = do { meth_bind <- mkGenericDefMethBind clas inst_tys sel_id dm_name
            ; tc_body sig_fn sel_id False {- Not generated code? -} 
-                     (Generated, meth_bind) inst_loc }
+                     meth_bind inst_loc }
 
     tc_default sig_fn sel_id NoDefMeth     -- No default method at all
       = do { traceTc "tc_def: warn" (ppr sel_id)
@@ -1224,8 +1228,8 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                                        inst_tys sel_id
            ; dflags <- getDynFlags
            ; return (meth_id,
-                     (Generated, mkVarBind meth_id $
-                                 mkLHsWrap lam_wrapper (error_rhs dflags))) }
+                     mkVarBind meth_id $
+                       mkLHsWrap lam_wrapper (error_rhs dflags)) }
       where
         error_rhs dflags = L inst_loc $ HsApp error_fun (error_msg dflags)
         error_fun    = L inst_loc $ wrapId (WpTyApp meth_tau) nO_METHOD_BINDING_ERROR_ID
@@ -1267,13 +1271,13 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                  bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
                                  , abs_exports = [export]
                                  , abs_ev_binds = EvBinds (unitBag self_ev_bind)
-                                 , abs_binds    = unitBag (Generated, meth_bind) }
+                                 , abs_binds    = unitBag meth_bind }
              -- Default methods in an instance declaration can't have their own
              -- INLINE or SPECIALISE pragmas. It'd be possible to allow them, but
              -- currently they are rejected with
              --           "INLINE pragma lacks an accompanying binding"
 
-           ; return (meth_id1, (Generated, L inst_loc bind)) }
+           ; return (meth_id1, L inst_loc bind) }
 
     ----------------------
     mk_meth_spec_prags :: Id -> [LTcSpecPrag] -> TcSpecPrags
@@ -1324,7 +1328,7 @@ mkGenericDefMethBind clas inst_tys sel_id dm_name
 		   (vcat [ppr clas <+> ppr inst_tys,
 			  nest 2 (ppr sel_id <+> equals <+> ppr rhs)]))
 
-        ; return (noLoc $ mkTopFunBind (noLoc (idName sel_id))
+        ; return (noLoc $ mkTopFunBind Generated (noLoc (idName sel_id))
                                        [mkSimpleMatch [] rhs]) }
   where
     rhs = nlHsVar dm_name

compiler/typecheck/TcInteract.lhs

@@ -1922,11 +1922,10 @@ getCoercibleInst loc ty1 ty2 = do
       -- Get some global stuff in scope, for nice pattern-guard based code in `go`
       rdr_env <- getGlobalRdrEnvTcS
       famenv <- getFamInstEnvs
-      safeMode <- safeLanguageOn `fmap` getDynFlags
-      go safeMode famenv rdr_env
+      go famenv rdr_env
   where
-  go :: Bool -> FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult
-  go safeMode famenv rdr_env
+  go :: FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult
+  go famenv rdr_env
     -- Coercible a a                             (see case 1 in [Coercible Instances])
     | ty1 `tcEqType` ty2
     = do return $ GenInst []
@@ -1946,11 +1945,8 @@ getCoercibleInst loc ty1 ty2 = do
     | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
       Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
       tc1 == tc2,
-      nominalArgsAgree tc1 tyArgs1 tyArgs2,
-      not safeMode || all (dataConsInScope rdr_env) (tyConsOfTyCon tc1)
-    = do -- Mark all used data constructors as used
-         when safeMode $ mapM_ (markDataConsAsUsed rdr_env) (tyConsOfTyCon tc1)
-         -- We want evidence for all type arguments of role R
+      nominalArgsAgree tc1 tyArgs1 tyArgs2
+    = do -- We want evidence for all type arguments of role R
          arg_stuff <- forM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \(r,ta1,ta2) ->
            case r of Nominal -> do
                           return
@@ -2060,13 +2056,6 @@ air, in getCoercibleInst. The following “instances” are present:
     The type constructor can be used undersaturated; then the Coercible
     instance is at a higher kind. This does not cause problems.
 
-    Furthermore in Safe Haskell code, we check that
-     * the data constructors of C are in scope and
-     * the data constructors of all type constructors used in the definition of
-     * C are in scope.
-       This is required as otherwise the previous check can be circumvented by
-       just adding a local data type around C.
-
  4. instance Coercible r b => Coercible (NT t1 t2 ...) b
     instance Coercible a r => Coercible a (NT t1 t2 ...)
     for a newtype constructor NT (or data family instance that resolves to a

compiler/typecheck/TcMType.lhs

-%
+o%
 % (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
@@ -40,23 +40,23 @@ module TcMType (
 
   --------------------------------
   -- Instantiation
-  tcInstTyVars, tcInstSigTyVars, newSigTyVar,
-  tcInstType, 
-  tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVars,
-  tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
+  tcInstTyVars, newSigTyVar,
+  tcInstType,
+  tcInstSkolTyVars, tcInstSuperSkolTyVars,tcInstSuperSkolTyVarsX,
+  tcInstSigTyVarsLoc, tcInstSigTyVars,
   tcInstSkolTyVar, tcInstSkolType,
   tcSkolDFunType, tcSuperSkolTyVars,
 
   --------------------------------
   -- Zonking
   zonkTcPredType, 
-  skolemiseSigTv, skolemiseUnboundMetaTyVar,
+  skolemiseUnboundMetaTyVar,
   zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
   zonkQuantifiedTyVar, quantifyTyVars,
   zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType, 
 
   zonkTcKind, defaultKindVarToStar,
-  zonkEvVar, zonkWC, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
+  zonkEvVar, zonkWC, zonkFlats, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
 
   tcGetGlobalTyVars, 
   ) where
@@ -238,9 +238,6 @@ tcInstSkolTyVar loc overlappable subst tyvar
 
 -- Wrappers
 -- we need to be able to do this from outside the TcM monad:
-tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
-tcInstSkolTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])
-
 tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
 tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])
 
@@ -255,29 +252,26 @@ tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True  subst
 tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
 -- Precondition: tyvars should be ordered (kind vars first)
 -- see Note [Kind substitution when instantiating]
+-- Get the location from the monad; this is a complete freshening operation
 tcInstSkolTyVars' isSuperSkol subst tvs
   = do { loc <- getSrcSpanM
        ; mapAccumLM (tcInstSkolTyVar loc isSuperSkol) subst tvs }
 
+tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
+-- We specify the location
+tcInstSigTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])
+
+tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
+-- Get the location from the TyVar itself, not the monad
+tcInstSigTyVars = mapAccumLM inst_tv (mkTopTvSubst [])
+  where
+    inst_tv subst tv = tcInstSkolTyVar (getSrcSpan tv) False subst tv
+
 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 -- Binding location comes from the monad
 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
 
-tcInstSigTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
--- Make meta SigTv type variables for patten-bound scoped type varaibles
--- We use SigTvs for them, so that they can't unify with arbitrary types
--- Precondition: tyvars should be ordered (kind vars first)
--- see Note [Kind substitution when instantiating]
-tcInstSigTyVars = mapAccumLM tcInstSigTyVar (mkTopTvSubst [])
-	-- The tyvars are freshly made, by tcInstSigTyVar
-        -- So mkTopTvSubst [] is ok
-
-tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
-tcInstSigTyVar subst tv
-  = do { new_tv <- newSigTyVar (tyVarName tv) (substTy subst (tyVarKind tv))
-       ; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }
-
 newSigTyVar :: Name -> Kind -> TcM TcTyVar
 newSigTyVar name kind
   = do { uniq <- newUnique
@@ -598,17 +592,6 @@ skolemiseUnboundMetaTyVar tv details
 
         ; writeMetaTyVar tv (mkTyVarTy final_tv)
         ; return final_tv }
-
-skolemiseSigTv :: TcTyVar -> TcM TcTyVar
--- In TcBinds we create SigTvs for type signatures
--- but for singleton groups we want them to really be skolems
--- which do not unify with each other
-skolemiseSigTv tv  
-  = ASSERT2( isSigTyVar tv, ppr tv )
-    do { writeMetaTyVarRef tv (metaTvRef tv) (mkTyVarTy skol_tv)
-       ; return skol_tv }
-  where
-    skol_tv = setTcTyVarDetails tv (SkolemTv False)
 \end{code}
 
 Note [Zonking to Skolem]

compiler/typecheck/TcMatches.lhs

@@ -109,7 +109,7 @@ tcMatchesCase :: (Outputable (body Name)) =>
 
 tcMatchesCase ctxt scrut_ty matches res_ty
   | isEmptyMatchGroup matches   -- Allow empty case expressions
-  = return (MG { mg_alts = [], mg_arg_tys = [scrut_ty], mg_res_ty = res_ty }) 
+  = return (MG { mg_alts = [], mg_arg_tys = [scrut_ty], mg_res_ty = res_ty, mg_origin = mg_origin matches })
 
   | otherwise
   = tcMatches ctxt [scrut_ty] res_ty matches
@@ -180,10 +180,10 @@ data TcMatchCtxt body   -- c.f. TcStmtCtxt, also in this module
                  -> TcRhoType
                  -> TcM (Located (body TcId)) }
 
-tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = matches })
+tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = matches, mg_origin = origin })
   = ASSERT( not (null matches) )	-- Ensure that rhs_ty is filled in
     do	{ matches' <- mapM (tcMatch ctxt pat_tys rhs_ty) matches
-	; return (MG { mg_alts = matches', mg_arg_tys = pat_tys, mg_res_ty = rhs_ty }) }
+	; return (MG { mg_alts = matches', mg_arg_tys = pat_tys, mg_res_ty = rhs_ty, mg_origin = origin }) }
 
 -------------
 tcMatch :: (Outputable (body Name)) => TcMatchCtxt body

compiler/typecheck/TcPat.lhs

@@ -13,7 +13,8 @@ TcPat: Typechecking patterns
 --     http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
 -- for details
 
-module TcPat ( tcLetPat, TcSigFun, TcSigInfo(..), TcPragFun 
+module TcPat ( tcLetPat, TcSigFun, TcPragFun
+             , TcSigInfo(..), findScopedTyVars
              , LetBndrSpec(..), addInlinePrags, warnPrags
              , tcPat, tcPats, newNoSigLetBndr
 	     , addDataConStupidTheta, badFieldCon, polyPatSig ) where
@@ -29,6 +30,7 @@ import Inst
 import Id
 import Var
 import Name
+import NameSet
 import TcEnv
 --import TcExpr
 import TcMType
@@ -146,8 +148,7 @@ data TcSigInfo
         sig_tvs    :: [(Maybe Name, TcTyVar)],    
                            -- Instantiated type and kind variables
                            -- Just n <=> this skolem is lexically in scope with name n
-                           -- See Note [Kind vars in sig_tvs]
-                     	   -- See Note [More instantiated than scoped] in TcBinds
+                           -- See Note [Binding scoped type variables]
 
         sig_theta  :: TcThetaType,  -- Instantiated theta
 
@@ -157,21 +158,56 @@ data TcSigInfo
         sig_loc    :: SrcSpan       -- The location of the signature
     }
 
+findScopedTyVars  -- See Note [Binding scoped type variables]
+  :: LHsType Name             -- The HsType
+  -> TcType                   -- The corresponding Type:
+                              --   uses same Names as the HsType
+  -> [TcTyVar]                -- The instantiated forall variables of the Type
+  -> [(Maybe Name, TcTyVar)]  -- In 1-1 correspondence with the instantiated vars
+findScopedTyVars hs_ty sig_ty inst_tvs
+  = zipWith find sig_tvs inst_tvs
+  where
+    find sig_tv inst_tv
+      | tv_name `elemNameSet` scoped_names = (Just tv_name, inst_tv)
+      | otherwise                          = (Nothing,      inst_tv)
+      where
+        tv_name = tyVarName sig_tv
+
+    scoped_names = mkNameSet (hsExplicitTvs hs_ty)
+    (sig_tvs,_)  = tcSplitForAllTys sig_ty
+
 instance Outputable TcSigInfo where
     ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
         = ppr id <+> dcolon <+> vcat [ pprSigmaType (mkSigmaTy (map snd tyvars) theta tau)
                                      , ppr (map fst tyvars) ]
 \end{code}
 
-Note [Kind vars in sig_tvs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-With kind polymorphism a signature like
-  f :: forall f a. f a -> f a
-may actuallly give rise to 
-  f :: forall k. forall (f::k -> *) (a:k). f a -> f a
-So the sig_tvs will be [k,f,a], but only f,a are scoped.
-So the scoped ones are not necessarily the *inital* ones!
-
+Note [Binding scoped type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type variables *brought into lexical scope* by a type signature may
+be a subset of the *quantified type variables* of the signatures, for two reasons:
+
+* With kind polymorphism a signature like
+    f :: forall f a. f a -> f a
+  may actuallly give rise to
+    f :: forall k. forall (f::k -> *) (a:k). f a -> f a
+  So the sig_tvs will be [k,f,a], but only f,a are scoped.
+  NB: the scoped ones are not necessarily the *inital* ones!
+
+* Even aside from kind polymorphism, tere may be more instantiated
+  type variables than lexically-scoped ones.  For example:
+        type T a = forall b. b -> (a,b)
+        f :: forall c. T c
+  Here, the signature for f will have one scoped type variable, c,
+  but two instantiated type variables, c' and b'.
+
+The function findScopedTyVars takes
+  * hs_ty:    the original HsForAllTy
+  * sig_ty:   the corresponding Type (which is guaranteed to use the same Names
+              as the HsForAllTy)
+  * inst_tvs: the skolems instantiated from the forall's in sig_ty
+It returns a [(Maybe Name, TcTyVar)], in 1-1 correspondence with inst_tvs
+but with a (Just n) for the lexically scoped name of each in-scope tyvar.
 
 Note [sig_tau may be polymorphic]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -753,8 +789,8 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn
 	    -> HsConPatDetails Name -> TcM a
 	    -> TcM (Pat TcId, a)
 tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
-  = do	{ let (univ_tvs, ex_tvs, (prov_theta, req_theta)) = patSynSig pat_syn
-              arg_tys = patSynArgTys pat_syn
+  = do	{ let (univ_tvs, ex_tvs, prov_theta, req_theta) = patSynSig pat_syn
+              arg_tys = patSynArgs pat_syn
               ty = patSynType pat_syn
 
         ; (_univ_tvs', inst_tys, subst) <- tcInstTyVars univ_tvs
@@ -777,14 +813,12 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
 
         ; prov_dicts' <- newEvVars prov_theta'
 
-          {-
+        -- Using a pattern synonym requires the PatternSynonyms
+        -- language flag to keep consistent with #2905
         ; patsyns_on <- xoptM Opt_PatternSynonyms
 	; checkTc patsyns_on
                   (ptext (sLit "A pattern match on a pattern synonym requires PatternSynonyms"))
-		  -- Trac #2905 decided that a *pattern-match* of a GADT
-		  -- should require the GADT language flag.
-                  -- Re TypeFamilies see also #7156
--}
+
         ; let skol_info = case pe_ctxt penv of
                             LamPat mc -> PatSkol (PatSynCon pat_syn) mc
                             LetPat {} -> UnkSkol -- Doesn't matter

compiler/typecheck/TcPatSyn.lhs

@@ -16,7 +16,6 @@ import TysPrim
 import Name
 import SrcLoc
 import PatSyn
-import Maybes
 import NameSet
 import Panic
 import Outputable
@@ -32,6 +31,7 @@ import Data.Monoid
 import Bag
 import TcEvidence
 import BuildTyCl
+import TypeRep
 
 #include "HsVersions.h"
 \end{code}
@@ -44,31 +44,32 @@ tcPatSynDecl :: Located Name
              -> TcM (PatSyn, LHsBinds Id)
 tcPatSynDecl lname@(L _ name) details lpat dir
   = do { traceTc "tcPatSynDecl {" $ ppr name $$ ppr lpat
+       ; tcCheckPatSynPat lpat
        ; pat_ty <- newFlexiTyVarTy openTypeKind
 
        ; let (arg_names, is_infix) = case details of
-                 PrefixPatSyn names -> (map unLoc names, False)
+                 PrefixPatSyn names      -> (map unLoc names, False)
                  InfixPatSyn name1 name2 -> (map unLoc [name1, name2], True)
-       ; ((lpat', args), wanted) <- captureConstraints $
-                                      tcPat PatSyn lpat pat_ty $ mapM tcLookupId arg_names
+       ; ((lpat', args), wanted) <- captureConstraints       $
+                                    tcPat PatSyn lpat pat_ty $
+                                    mapM tcLookupId arg_names
        ; let named_taus = (name, pat_ty):map (\arg -> (getName arg, varType arg)) args
 
        ; traceTc "tcPatSynDecl::wanted" (ppr named_taus $$ ppr wanted)
-       ; (qtvs, given_dicts, _mr_bites, ev_binds) <- simplifyInfer True False named_taus wanted
-       ; let req_dicts = given_dicts
+       ; (qtvs, req_dicts, _mr_bites, ev_binds) <- simplifyInfer True False named_taus wanted
 
        ; (ex_vars, prov_dicts) <- tcCollectEx lpat'
-       ; let univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs
-             ex_tvs = varSetElems ex_vars
+       ; let univ_tvs   = filter (not . (`elemVarSet` ex_vars)) qtvs
+             ex_tvs     = varSetElems ex_vars
+             prov_theta = map evVarPred prov_dicts
+             req_theta  = map evVarPred req_dicts
 
-       ; pat_ty <- zonkTcType pat_ty
-       ; args <- mapM zonkId args
-
-       ; univ_tvs <- mapM zonkQuantifiedTyVar univ_tvs
-       ; let prov_theta = map evVarPred prov_dicts
-             req_theta = map evVarPred req_dicts
+       ; univ_tvs   <- mapM zonkQuantifiedTyVar univ_tvs
+       ; ex_tvs     <- mapM zonkQuantifiedTyVar ex_tvs
        ; prov_theta <- zonkTcThetaType prov_theta
-       ; req_theta <- zonkTcThetaType req_theta
+       ; req_theta  <- zonkTcThetaType req_theta
+       ; pat_ty     <- zonkTcType pat_ty
+       ; args       <- mapM zonkId args
 
        ; traceTc "tcPatSynDecl: ex" (ppr ex_tvs $$
                                      ppr prov_theta $$
@@ -92,18 +93,22 @@ tcPatSynDecl lname@(L _ name) details lpat dir
                                          prov_theta req_theta
                                          pat_ty
        ; m_wrapper <- tcPatSynWrapper lname lpat dir args
-                        univ_tvs ex_tvs theta pat_ty
+                                      univ_tvs ex_tvs theta pat_ty
        ; let binds = matcher_bind `unionBags` maybe emptyBag snd m_wrapper
 
        ; traceTc "tcPatSynDecl }" $ ppr name
        ; let patSyn = mkPatSyn name is_infix
-                        args
+                        (map varType args)
                         univ_tvs ex_tvs
                         prov_theta req_theta
                         pat_ty
                         matcher_id (fmap fst m_wrapper)
        ; return (patSyn, binds) }
 
+\end{code}
+
+
+\begin{code}
 tcPatSynMatcher :: Located Name
                 -> LPat Id
                 -> [Var]
@@ -113,12 +118,18 @@ tcPatSynMatcher :: Located Name
                 -> ThetaType -> ThetaType
                 -> TcType
                 -> TcM (Id, LHsBinds Id)
+-- See Note [Matchers and wrappers for pattern synonyms] in PatSyn
 tcPatSynMatcher (L loc name) lpat args univ_tvs ex_tvs ev_binds prov_dicts req_dicts prov_theta req_theta pat_ty
   = do { res_tv <- zonkQuantifiedTyVar =<< newFlexiTyVar liftedTypeKind
-       ; (matcher_id, res_ty, cont_ty) <- mkPatSynMatcherId name args
-                                            univ_tvs ex_tvs
-                                            prov_theta req_theta
-                                            pat_ty res_tv
+       ; matcher_name <- newImplicitBinder name mkMatcherOcc
+       ; let res_ty = TyVarTy res_tv
+             cont_ty = mkSigmaTy ex_tvs prov_theta $
+                       mkFunTys (map varType args) res_ty
+
+       ; let matcher_tau = mkFunTys [pat_ty, cont_ty, res_ty] res_ty
+             matcher_sigma = mkSigmaTy (res_tv:univ_tvs) req_theta matcher_tau
+             matcher_id = mkVanillaGlobal matcher_name matcher_sigma
+
        ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
        ; let matcher_lid = L loc matcher_id
 
@@ -141,18 +152,21 @@ tcPatSynMatcher (L loc name) lpat args univ_tvs ex_tvs ev_binds prov_dicts req_d
                     MG{ mg_alts = cases
                       , mg_arg_tys = [pat_ty]
                       , mg_res_ty = res_ty
+                      , mg_origin = Generated
                       }
              body' = noLoc $
                      HsLam $
                      MG{ mg_alts = [mkSimpleMatch args body]
                        , mg_arg_tys = [pat_ty, cont_ty, res_ty]
                        , mg_res_ty = res_ty
+                       , mg_origin = Generated
                        }
 
              match = mkMatch [] (mkHsLams (res_tv:univ_tvs) req_dicts body') EmptyLocalBinds
              mg = MG{ mg_alts = [match]
                     , mg_arg_tys = []
                     , mg_res_ty = res_ty
+                    , mg_origin = Generated
                     }
 
        ; let bind = FunBind{ fun_id = matcher_lid
@@ -161,7 +175,7 @@ tcPatSynMatcher (L loc name) lpat args univ_tvs ex_tvs ev_binds prov_dicts req_d
                            , fun_co_fn = idHsWrapper
                            , bind_fvs = emptyNameSet
                            , fun_tick = Nothing }
-             matcher_bind = unitBag (Generated, noLoc bind)
+             matcher_bind = unitBag (noLoc bind)
 
        ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
 
@@ -179,14 +193,14 @@ tcPatSynWrapper :: Located Name
                 -> ThetaType
                 -> TcType
                 -> TcM (Maybe (Id, LHsBinds Id))
+-- See Note [Matchers and wrappers for pattern synonyms] in PatSyn
 tcPatSynWrapper lname lpat dir args univ_tvs ex_tvs theta pat_ty
   = do { let argNames = mkNameSet (map Var.varName args)
-       ; m_expr <- runMaybeT $ tcPatToExpr argNames lpat
-       ; case (dir, m_expr) of
+       ; case (dir, tcPatToExpr argNames lpat) of
            (Unidirectional, _) ->
                return Nothing
            (ImplicitBidirectional, Nothing) ->
-               cannotInvertPatSynErr (unLoc lpat)
+               cannotInvertPatSynErr lpat
            (ImplicitBidirectional, Just lexpr) ->
                fmap Just $ tc_pat_syn_wrapper_from_expr lname lexpr args univ_tvs ex_tvs theta pat_ty }
 
@@ -199,22 +213,20 @@ tc_pat_syn_wrapper_from_expr :: Located Name
                              -> TcM (Id, LHsBinds Id)
 tc_pat_syn_wrapper_from_expr (L loc name) lexpr args univ_tvs ex_tvs theta pat_ty
   = do { let qtvs = univ_tvs ++ ex_tvs
-       ; (subst, qtvs') <- tcInstSigTyVars qtvs
-       ; let theta' = substTheta subst theta
+       ; (subst, wrapper_tvs) <- tcInstSkolTyVars qtvs
+       ; let wrapper_theta = substTheta subst theta
              pat_ty' = substTy subst pat_ty
              args' = map (\arg -> setVarType arg $ substTy subst (varType arg)) args
-
-       ; wrapper_id <- mkPatSynWrapperId name args qtvs theta pat_ty
-       ; let wrapper_name = getName wrapper_id
-             wrapper_lname = L loc wrapper_name
-             -- (wrapper_tvs, wrapper_theta, wrapper_tau) = tcSplitSigmaTy (idType wrapper_id)
-             wrapper_tvs = qtvs'
-             wrapper_theta = theta'
              wrapper_tau = mkFunTys (map varType args') pat_ty'
+             wrapper_sigma = mkSigmaTy wrapper_tvs wrapper_theta wrapper_tau
+
+       ; wrapper_name <- newImplicitBinder name mkDataConWrapperOcc
+       ; let wrapper_lname = L loc wrapper_name
+             wrapper_id = mkVanillaGlobal wrapper_name wrapper_sigma
 
        ; let wrapper_args = map (noLoc . VarPat . Var.varName) args'
              wrapper_match = mkMatch wrapper_args lexpr EmptyLocalBinds
-             bind = mkTopFunBind wrapper_lname [wrapper_match]
+             bind = mkTopFunBind Generated wrapper_lname [wrapper_match]
              lbind = noLoc bind
        ; let sig = TcSigInfo{ sig_id = wrapper_id
                             , sig_tvs = map (\tv -> (Nothing, tv)) wrapper_tvs
@@ -222,72 +234,127 @@ tc_pat_syn_wrapper_from_expr (L loc name) lexpr args univ_tvs ex_tvs theta pat_t
                             , sig_tau = wrapper_tau
                             , sig_loc = loc
                             }
-       ; (wrapper_binds, _, _) <- tcPolyCheck NonRecursive (const []) sig (Generated, lbind)
+       ; (wrapper_binds, _, _) <- tcPolyCheck NonRecursive (const []) sig lbind
        ; traceTc "tcPatSynDecl wrapper" $ ppr wrapper_binds
        ; traceTc "tcPatSynDecl wrapper type" $ ppr (varType wrapper_id)
        ; return (wrapper_id, wrapper_binds) }
 
-tcNothing :: MaybeT TcM a
-tcNothing = MaybeT (return Nothing)
+\end{code}
+
+Note [As-patterns in pattern synonym definitions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The rationale for rejecting as-patterns in pattern synonym definitions
+is that an as-pattern would introduce nonindependent pattern synonym
+arguments, e.g. given a pattern synonym like:
+
+        pattern K x y = x@(Just y)
 
-withLoc :: (a -> MaybeT TcM b) -> Located a -> MaybeT TcM (Located b)
-withLoc fn (L loc x) = MaybeT $ setSrcSpan loc $
-    do { y <- runMaybeT $ fn x
-       ; return (fmap (L loc) y) }
+one could write a nonsensical function like
 
-tcPatToExpr :: NameSet -> LPat Name -> MaybeT TcM (LHsExpr Name)
+        f (K Nothing x) = ...
+
+or
+        g (K (Just True) False) = ...
+
+\begin{code}
+tcCheckPatSynPat :: LPat Name -> TcM ()
+tcCheckPatSynPat = go
+  where
+    go :: LPat Name -> TcM ()
+    go = addLocM go1
+
+    go1 :: Pat Name -> TcM ()
+    go1   (ConPatIn _ info)   = mapM_ go (hsConPatArgs info)
+    go1   VarPat{}            = return ()
+    go1   WildPat{}           = return ()
+    go1 p@(AsPat _ _)         = asPatInPatSynErr p
+    go1   (LazyPat pat)       = go pat
+    go1   (ParPat pat)        = go pat
+    go1   (BangPat pat)       = go pat
+    go1   (PArrPat pats _)    = mapM_ go pats
+    go1   (ListPat pats _ _)  = mapM_ go pats
+    go1   (TuplePat pats _ _) = mapM_ go pats
+    go1   LitPat{}            = return ()
+    go1   NPat{}              = return ()
+    go1   (SigPatIn pat _)    = go pat
+    go1   (ViewPat _ pat _)   = go pat
+    go1 p@SplicePat{}         = thInPatSynErr p
+    go1 p@QuasiQuotePat{}     = thInPatSynErr p
+    go1 p@NPlusKPat{}         = nPlusKPatInPatSynErr p
+    go1   ConPatOut{}         = panic "ConPatOut in output of renamer"
+    go1   SigPatOut{}         = panic "SigPatOut in output of renamer"
+    go1   CoPat{}             = panic "CoPat in output of renamer"
+
+asPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
+asPatInPatSynErr pat
+  = failWithTc $
+    hang (ptext (sLit "Pattern synonym definition cannot contain as-patterns (@):"))
+       2 (ppr pat)
+
+thInPatSynErr :: OutputableBndr name => Pat name -> TcM a
+thInPatSynErr pat
+  = failWithTc $
+    hang (ptext (sLit "Pattern synonym definition cannot contain Template Haskell:"))
+       2 (ppr pat)
+
+nPlusKPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
+nPlusKPatInPatSynErr pat
+  = failWithTc $
+    hang (ptext (sLit "Pattern synonym definition cannot contain n+k-pattern:"))
+       2 (ppr pat)
+
+tcPatToExpr :: NameSet -> LPat Name -> Maybe (LHsExpr Name)
 tcPatToExpr lhsVars = go
   where
-    go :: LPat Name -> MaybeT TcM (LHsExpr Name)
+    go :: LPat Name -> Maybe (LHsExpr Name)
     go (L loc (ConPatIn conName info))
-      = MaybeT . setSrcSpan loc . runMaybeT $ do
+      = do
           { let con = L loc (HsVar (unLoc conName))
           ; exprs <- mapM go (hsConPatArgs info)
           ; return $ foldl (\x y -> L loc (HsApp x y)) con exprs }
-    go p = withLoc go1 p
+    go (L loc p) = fmap (L loc) $ go1 p
 
-    go1 :: Pat Name -> MaybeT TcM (HsExpr Name)
+    go1 :: Pat Name -> Maybe (HsExpr Name)
     go1   (VarPat var)
-      | var `elemNameSet` lhsVars  = return (HsVar var)
-      | otherwise                  = tcNothing
-    go1 p@(AsPat _ _)              = asPatInPatSynErr p
-    go1   (LazyPat pat)            = fmap HsPar (go pat)
-    go1   (ParPat pat)             = fmap HsPar (go pat)
-    go1   (BangPat pat)            = fmap HsPar (go pat)
+      | var `elemNameSet` lhsVars  = return $ HsVar var
+      | otherwise                  = Nothing
+    go1   (LazyPat pat)            = fmap HsPar $ go pat
+    go1   (ParPat pat)             = fmap HsPar $ go pat
+    go1   (BangPat pat)            = fmap HsPar $ go pat
     go1   (PArrPat pats ptt)
       = do { exprs <- mapM go pats
-           ; return (ExplicitPArr ptt exprs) }
+           ; return $ ExplicitPArr ptt exprs }
     go1   (ListPat pats ptt reb)
       = do { exprs <- mapM go pats
-           ; return (ExplicitList ptt (fmap snd reb) exprs) }
+           ; return $ ExplicitList ptt (fmap snd reb) exprs }
     go1   (TuplePat pats box _)
       = do { exprs <- mapM go pats
            ; return (ExplicitTuple (map Present exprs) box)
            }
-    go1   (LitPat lit)  = return (HsLit lit)
-    go1   (NPat n Nothing _)       = return (HsOverLit n)
-    go1   (NPat n (Just neg) _)    = return (noLoc neg `HsApp` noLoc (HsOverLit n))
+    go1   (LitPat lit)             = return $ HsLit lit
+    go1   (NPat n Nothing _)       = return $ HsOverLit n
+    go1   (NPat n (Just neg) _)    = return $ noLoc neg `HsApp` noLoc (HsOverLit n)
     go1   (SigPatIn pat (HsWB ty _ _))
       = do { expr <- go pat
-           ; return (ExprWithTySig expr ty) }
+           ; return $ ExprWithTySig expr ty }
     go1   (ConPatOut{})            = panic "ConPatOut in output of renamer"
     go1   (SigPatOut{})            = panic "SigPatOut in output of renamer"
     go1   (CoPat{})                = panic "CoPat in output of renamer"
-    go1   _                        = tcNothing
-
-asPatInPatSynErr :: OutputableBndr name => Pat name -> MaybeT TcM a
-asPatInPatSynErr pat
-  = MaybeT . failWithTc $
-    hang (ptext (sLit "Pattern synonym definition cannot contain as-patterns (@):"))
-       2 (ppr pat)
+    go1   _                        = Nothing
 
--- TODO: Highlight sub-pattern that causes the problem
-cannotInvertPatSynErr :: OutputableBndr name => Pat name -> TcM a
-cannotInvertPatSynErr pat
-  = failWithTc $
+cannotInvertPatSynErr :: OutputableBndr name => LPat name -> TcM a
+cannotInvertPatSynErr (L loc pat)
+  = setSrcSpan loc $ failWithTc $
     hang (ptext (sLit "Right-hand side of bidirectional pattern synonym cannot be used as an expression"))
        2 (ppr pat)
 
+-- Walk the whole pattern and for all ConPatOuts, collect the
+-- existentially-bound type variables and evidence binding variables.
+--
+-- These are used in computing the type of a pattern synonym and also
+-- in generating matcher functions, since success continuations need
+-- to be passed these pattern-bound evidences.
 tcCollectEx :: LPat Id -> TcM (TyVarSet, [EvVar])
 tcCollectEx = return . go
   where

compiler/typecheck/TcRnDriver.lhs

@@ -13,6 +13,7 @@ module TcRnDriver (
         getModuleInterface,
         tcRnDeclsi,
         isGHCiMonad,
+        runTcInteractive,    -- Used by GHC API clients (Trac #8878)
 #endif
         tcRnLookupName,
         tcRnGetInfo,
@@ -83,9 +84,7 @@ import Annotations
 import Data.List ( sortBy )
 import Data.IORef ( readIORef )
 import Data.Ord
-#ifndef GHCI
-import BasicTypes ( Origin(..) )
-#else
+#ifdef GHCI
 import BasicTypes hiding( SuccessFlag(..) )
 import TcType   ( isUnitTy, isTauTy )
 import TcHsType
@@ -672,7 +671,7 @@ checkHiBootIface
         ; mb_dfun_prs <- mapM check_inst boot_insts
         ; let dfun_prs   = catMaybes mb_dfun_prs
               boot_dfuns = map fst dfun_prs
-              dfun_binds = listToBag [ (Generated, mkVarBind boot_dfun (nlHsVar dfun))
+              dfun_binds = listToBag [ mkVarBind boot_dfun (nlHsVar dfun)
                                      | (boot_dfun, dfun) <- dfun_prs ]
               type_env'  = extendTypeEnvWithIds local_type_env boot_dfuns
               tcg_env'   = tcg_env { tcg_binds = binds `unionBags` dfun_binds }
@@ -1370,7 +1369,7 @@ check_main dflags tcg_env
 
         ; return (tcg_env { tcg_main  = Just main_name,
                             tcg_binds = tcg_binds tcg_env
-                                        `snocBag` (Generated, main_bind),
+                                        `snocBag` main_bind,
                             tcg_dus   = tcg_dus tcg_env
                                         `plusDU` usesOnly (unitFV main_name)
                         -- Record the use of 'main', so that we don't
@@ -1605,14 +1604,14 @@ tcUserStmt (L loc (BodyStmt expr _ _ _))
         ; let fresh_it  = itName uniq loc
               matches   = [mkMatch [] rn_expr emptyLocalBinds]
               -- [it = expr]
-              the_bind  = L loc $ (mkTopFunBind (L loc fresh_it) matches) { bind_fvs = fvs }
+              the_bind  = L loc $ (mkTopFunBind FromSource (L loc fresh_it) matches) { bind_fvs = fvs }
                           -- Care here!  In GHCi the expression might have
                           -- free variables, and they in turn may have free type variables
                           -- (if we are at a breakpoint, say).  We must put those free vars
 
               -- [let it = expr]
               let_stmt  = L loc $ LetStmt $ HsValBinds $
-                          ValBindsOut [(NonRecursive,unitBag (FromSource, the_bind))] []
+                          ValBindsOut [(NonRecursive,unitBag the_bind)] []
 
               -- [it <- e]
               bind_stmt = L loc $ BindStmt (L loc (VarPat fresh_it))

compiler/typecheck/TcRnMonad.lhs

@@ -24,7 +24,6 @@ import Module
 import RdrName
 import Name
 import Type
-import Kind ( isSuperKind )
 
 import TcType
 import InstEnv
@@ -49,7 +48,7 @@ import FastString
 import Panic
 import Util
 import Annotations
-import BasicTypes( TopLevelFlag, Origin )
+import BasicTypes( TopLevelFlag )
 
 import Control.Exception
 import Data.IORef
@@ -588,11 +587,6 @@ addLocM fn (L loc a) = setSrcSpan loc $ fn a
 wrapLocM :: (a -> TcM b) -> Located a -> TcM (Located b)
 wrapLocM fn (L loc a) = setSrcSpan loc $ do b <- fn a; return (L loc b)
 
-wrapOriginLocM :: (a -> TcM r) -> (Origin, Located a) -> TcM (Origin, Located r)
-wrapOriginLocM fn (origin, lbind)
-  = do  { lbind' <- wrapLocM fn lbind
-        ; return (origin, lbind') }
-
 wrapLocFstM :: (a -> TcM (b,c)) -> Located a -> TcM (Located b, c)
 wrapLocFstM fn (L loc a) =
   setSrcSpan loc $ do
@@ -1136,10 +1130,6 @@ setUntouchables untch thing_inside
 
 isTouchableTcM :: TcTyVar -> TcM Bool
 isTouchableTcM tv
-    -- Kind variables are always touchable
-  | isSuperKind (tyVarKind tv) 
-  = return False
-  | otherwise 
   = do { env <- getLclEnv
        ; return (isTouchableMetaTyVar (tcl_untch env) tv) }
 

compiler/typecheck/TcSMonad.lhs

@@ -1638,14 +1638,10 @@ See Note [Coercion evidence terms] in TcEvidence.
 
 Note [Do not create Given kind equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We do not want to create a Given like
+We do not want to create a Given kind equality like
 
-     kv ~ k            -- kv is a skolem kind variable
-                       -- Reason we don't yet support non-Refl kind equalities
-
-or   t1::k1 ~ t2::k2   -- k1 and k2 are un-equal kinds
-                       -- Reason: (~) is kind-uniform at the moment, and
-                       -- k1/k2 may be distinct kind skolems
+   [G]  kv ~ k   -- kv is a skolem kind variable
+                 -- Reason we don't yet support non-Refl kind equalities
 
 This showed up in Trac #8566, where we had a data type
    data I (u :: U *) (r :: [*]) :: * where
@@ -1656,14 +1652,24 @@ so A has type
         (u ~ AA * k t as) => I u r
 
 There is no direct kind equality, but in a pattern match where 'u' is
-instantiated to, say, (AA * kk t1 as1), we'd decompose to get
+instantiated to, say, (AA * kk (t1:kk) as1), we'd decompose to get
    k ~ kk, t ~ t1, as ~ as1
-This is bad.  We "fix" this by simply ignoring
-  *     the Given kind equality
-  * AND the Given type equality (t:k1) ~ (t1:kk)
-
+This is bad.  We "fix" this by simply ignoring the Given kind equality
 But the Right Thing is to add kind equalities!
 
+But note (Trac #8705) that we *do* create Given (non-canonical) equalities
+with un-equal kinds, e.g.
+   [G]  t1::k1 ~ t2::k2   -- k1 and k2 are un-equal kinds
+Reason: k1 or k2 might be unification variables that have already been
+unified (at this point we have not canonicalised the types), so we want
+to emit this t1~t2 as a (non-canonical) Given in the work-list. If k1/k2 
+have been unified, we'll find that when we canonicalise it, and the 
+t1~t2 information may be crucial (Trac #8705 is an example).
+
+If it turns out that k1 and k2 are really un-equal, then it'll end up
+as an Irreducible (see Note [Equalities with incompatible kinds] in
+TcCanonical), and will do no harm.
+
 \begin{code}
 xCtEvidence :: CtEvidence            -- Original flavor
             -> XEvTerm               -- Instructions about how to manipulate evidence
@@ -1677,8 +1683,8 @@ xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
   where
     -- See Note [Do not create Given kind equalities]
     bad_given_pred (pred_ty, _)
-      | EqPred t1 t2 <- classifyPredType pred_ty
-      = isKind t1 || not (typeKind t1 `tcEqKind` typeKind t2)
+      | EqPred t1 _ <- classifyPredType pred_ty
+      = isKind t1
       | otherwise
       = False
 
@@ -1718,7 +1724,18 @@ Main purpose: create new evidence for new_pred;
 
         Given           Already in inert               Nothing
                         Not                            Just new_evidence
--}
+
+Note [Rewriting with Refl]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the coercion is just reflexivity then you may re-use the same
+variable.  But be careful!  Although the coercion is Refl, new_pred
+may reflect the result of unification alpha := ty, so new_pred might
+not _look_ the same as old_pred, and it's vital to proceed from now on
+using new_pred.
+
+The flattener preserves type synonyms, so they should appear in new_pred
+as well as in old_pred; that is important for good error messages.
+ -}
 
 
 rewriteEvidence (CtDerived { ctev_loc = loc }) new_pred _co
@@ -1732,15 +1749,8 @@ rewriteEvidence (CtDerived { ctev_loc = loc }) new_pred _co
     newDerived loc new_pred
 
 rewriteEvidence old_ev new_pred co
-  | isTcReflCo co -- If just reflexivity then you may re-use the same variable
-  = return (Just (if ctEvPred old_ev `tcEqType` new_pred
-                  then old_ev
-                  else old_ev { ctev_pred = new_pred }))
-       -- Even if the coercion is Refl, it might reflect the result of unification alpha := ty
-       -- so old_pred and new_pred might not *look* the same, and it's vital to proceed from
-       -- now on using new_pred.
-       -- However, if they *do* look the same, we'd prefer to stick with old_pred
-       -- then retain the old type, so that error messages come out mentioning synonyms
+  | isTcReflCo co -- See Note [Rewriting with Refl]
+  = return (Just (old_ev { ctev_pred = new_pred }))
 
 rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
   = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
@@ -1783,12 +1793,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
   = newDerived loc (mkEqPred nlhs nrhs)
 
   | NotSwapped <- swapped
-  , isTcReflCo lhs_co
+  , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
   , isTcReflCo rhs_co
-  , let new_pred = mkTcEqPred nlhs nrhs
-  = return (Just (if ctEvPred old_ev `tcEqType` new_pred
-                  then old_ev
-                  else old_ev { ctev_pred = new_pred }))
+  = return (Just (old_ev { ctev_pred = new_pred }))
 
   | CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
   = do { let new_tm = EvCoercion (lhs_co 

compiler/typecheck/TcSimplify.lhs

@@ -16,7 +16,7 @@ import TcMType as TcM
 import TcType
 import TcSMonad as TcS
 import TcInteract
-import Kind     ( defaultKind_maybe )
+import Kind     ( isKind, defaultKind_maybe )
 import Inst
 import FunDeps  ( growThetaTyVars )
 import Type     ( classifyPredType, PredTree(..), getClassPredTys_maybe )
@@ -253,39 +253,50 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
        ; ev_binds_var <- newTcEvBinds
        ; wanted_transformed_incl_derivs
                <- solveWantedsTcMWithEvBinds ev_binds_var wanteds solve_wanteds
-                               -- Post: wanted_transformed are zonked
+                  -- Post: wanted_transformed_incl_derivs are zonked
 
               -- Step 4) Candidates for quantification are an approximation of wanted_transformed
               -- NB: Already the fixpoint of any unifications that may have happened
               -- NB: We do not do any defaulting when inferring a type, this can lead
               -- to less polymorphic types, see Note [Default while Inferring]
 
-              -- Step 5) Minimize the quantification candidates
-              -- Step 6) Final candidates for quantification
-              -- We discard bindings, insolubles etc, because all we are
-              -- care aout it
-
        ; tc_lcl_env <- TcRnMonad.getLclEnv
        ; let untch = tcl_untch tc_lcl_env
              wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
        ; quant_pred_candidates   -- Fully zonked
            <- if insolubleWC wanted_transformed_incl_derivs
               then return []   -- See Note [Quantification with errors]
-                               -- NB: must include derived errors
-              else do { gbl_tvs <- tcGetGlobalTyVars
-                      ; let quant_cand = approximateWC wanted_transformed
+                               -- NB: must include derived errors in this test, 
+                               --     hence "incl_derivs"
+
+              else do { let quant_cand = approximateWC wanted_transformed
                             meta_tvs   = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand))
-                      ; ((flats, _insols), _extra_binds) <- runTcS $
+                      ; gbl_tvs <- tcGetGlobalTyVars
+                      ; null_ev_binds_var <- newTcEvBinds
+                            -- Miminise quant_cand.  We are not interested in any evidence
+                            -- produced, because we are going to simplify wanted_transformed
+                            -- again later. All we want here is the predicates over which to
+                            -- quantify.  
+                            --
+                            -- If any meta-tyvar unifications take place (unlikely), we'll
+                            -- pick that up later.
+
+                      ; (flats, _insols) <- runTcSWithEvBinds null_ev_binds_var $
                         do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs
                                  -- See Note [Promote _and_ default when inferring]
                            ; _implics <- solveInteract quant_cand
                            ; getInertUnsolved }
-                      ; return (map ctPred $ filter isWantedCt (bagToList flats)) }
-                   -- NB: Dimitrios is slightly worried that we will get
-                   -- family equalities (F Int ~ alpha) in the quantification
-                   -- candidates, as we have performed no further unflattening
-                   -- at this point. Nothing bad, but inferred contexts might
-                   -- look complicated.
+
+                      ; flats' <- zonkFlats null_ev_binds_var untch $
+                                  filterBag isWantedCt flats
+                           -- The quant_cand were already fully zonked, so this zonkFlats
+                           -- really only unflattens the flattening that solveInteract
+                           -- may have done (Trac #8889).  
+                           -- E.g. quant_cand = F a, where F :: * -> Constraint
+                           --      We'll flatten to   (alpha, F a ~ alpha)
+                           -- fail to make any further progress and must unflatten again 
+
+                      ; return (map ctPred $ bagToList flats') }
 
        -- NB: quant_pred_candidates is already the fixpoint of any
        --     unifications that may have happened
@@ -326,6 +337,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
 
       {     -- Step 7) Emit an implication
          let minimal_flat_preds = mkMinimalBySCs bound
+                  -- See Note [Minimize by Superclasses]
              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
                                    | (name, ty) <- name_taus ]
                         -- Don't add the quantified variables here, because
@@ -1237,16 +1249,22 @@ findDefaultableGroups
     -> Cts              -- Unsolved (wanted or derived)
     -> [[(Ct,Class,TcTyVar)]]
 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
-  | null default_tys             = []
-  | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
+  | null default_tys = []
+  | otherwise        = defaultable_groups
   where
+    defaultable_groups = filter is_defaultable_group groups
+    groups             = equivClasses cmp_tv unaries
     unaries     :: [(Ct, Class, TcTyVar)]  -- (C tv) constraints
     non_unaries :: [Ct]             -- and *other* constraints
 
     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
         -- Finds unary type-class constraints
+        -- But take account of polykinded classes like Typeable,
+        -- which may look like (Typeable * (a:*))   (Trac #8931)
     find_unary cc
-        | Just (cls,[ty]) <- getClassPredTys_maybe (ctPred cc)
+        | Just (cls,tys)   <- getClassPredTys_maybe (ctPred cc)
+        , Just (kinds, ty) <- snocView tys
+        , all isKind kinds
         , Just tv <- tcGetTyVar_maybe ty
         , isMetaTyVar tv  -- We might have runtime-skolems in GHCi, and
                           -- we definitely don't want to try to assign to those!

compiler/typecheck/TcSplice.lhs

@@ -70,6 +70,7 @@ import Class
 import Inst
 import TyCon
 import CoAxiom
+import PatSyn ( patSynId )
 import ConLike
 import DataCon
 import TcEvidence( TcEvBinds(..) )
@@ -1173,6 +1174,8 @@ reifyThing (AGlobal (AConLike (RealDataCon dc)))
         ; return (TH.DataConI (reifyName name) ty
                               (reifyName (dataConOrigTyCon dc)) fix)
         }
+reifyThing (AGlobal (AConLike (PatSynCon ps)))
+  = noTH (sLit "pattern synonyms") (ppr $ patSynId ps)
 
 reifyThing (ATcId {tct_id = id})
   = do  { ty1 <- zonkTcType (idType id) -- Make use of all the info we have, even
@@ -1191,7 +1194,8 @@ reifyThing thing = pprPanic "reifyThing" (pprTcTyThingCategory thing)
 -------------------------------------------
 reifyAxBranch :: CoAxBranch -> TcM TH.TySynEqn
 reifyAxBranch (CoAxBranch { cab_lhs = args, cab_rhs = rhs })
-  = do { args' <- mapM reifyType args
+            -- remove kind patterns (#8884)
+  = do { args' <- mapM reifyType (filter (not . isKind) args)
        ; rhs'  <- reifyType rhs
        ; return (TH.TySynEqn args' rhs') }
 
@@ -1207,10 +1211,15 @@ reifyTyCon tc
   = return (TH.PrimTyConI (reifyName tc) (tyConArity tc) (isUnLiftedTyCon tc))
 
   | isFamilyTyCon tc
-  = do { let tvs     = tyConTyVars tc
-             kind    = tyConKind tc
-       ; kind' <- if isLiftedTypeKind kind then return Nothing
-                  else fmap Just (reifyKind kind)
+  = do { let tvs      = tyConTyVars tc
+             kind     = tyConKind tc
+
+             -- we need the *result kind* (see #8884)
+             (kvs, mono_kind) = splitForAllTys kind
+                                -- tyConArity includes *kind* params
+             (_, res_kind)    = splitKindFunTysN (tyConArity tc - length kvs)
+                                                 mono_kind
+       ; kind' <- fmap Just (reifyKind res_kind)
 
        ; tvs' <- reifyTyVars tvs
        ; flav' <- reifyFamFlavour tc
@@ -1312,7 +1321,8 @@ reifyFamilyInstance (FamInst { fi_flavor = flavor
                              , fi_rhs = rhs })
   = case flavor of
       SynFamilyInst ->
-        do { th_lhs <- reifyTypes lhs
+               -- remove kind patterns (#8884)
+        do { th_lhs <- reifyTypes (filter (not . isKind) lhs)
            ; th_rhs <- reifyType  rhs
            ; return (TH.TySynInstD (reifyName fam) (TH.TySynEqn th_lhs th_rhs)) }
 
@@ -1498,13 +1508,14 @@ lookupThAnnLookup (TH.AnnLookupModule (TH.Module pn mn))
     mkModule (stringToPackageId $ TH.pkgString pn) (mkModuleName $ TH.modString mn)
 
 reifyAnnotations :: Data a => TH.AnnLookup -> TcM [a]
-reifyAnnotations th_nm
-  = do { name <- lookupThAnnLookup th_nm
-       ; eps <- getEps
+reifyAnnotations th_name
+  = do { name <- lookupThAnnLookup th_name
+       ; topEnv <- getTopEnv
+       ; epsHptAnns <- liftIO $ prepareAnnotations topEnv Nothing
        ; tcg <- getGblEnv
-       ; let epsAnns = findAnns deserializeWithData (eps_ann_env eps) name
-       ; let envAnns = findAnns deserializeWithData (tcg_ann_env tcg) name
-       ; return (envAnns ++ epsAnns) }
+       ; let selectedEpsHptAnns = findAnns deserializeWithData epsHptAnns name
+       ; let selectedTcgAnns = findAnns deserializeWithData (tcg_ann_env tcg) name
+       ; return (selectedEpsHptAnns ++ selectedTcgAnns) }
 
 ------------------------------
 modToTHMod :: Module -> TH.Module
@@ -1562,4 +1573,4 @@ will appear in TH syntax like this
 
 \begin{code}
 #endif  /* GHCI */
-\end{code}
\ No newline at end of file
+\end{code}

compiler/typecheck/TcTyClsDecls.lhs

@@ -780,7 +780,8 @@ tcDataDefn rec_info tc_name tvs kind
   = do { extra_tvs <- tcDataKindSig kind
        ; let final_tvs  = tvs ++ extra_tvs
              roles      = rti_roles rec_info tc_name
-       ; stupid_theta <- tcHsContext ctxt
+       ; stupid_tc_theta <- tcHsContext ctxt
+       ; stupid_theta    <- zonkTcTypeToTypes emptyZonkEnv stupid_tc_theta
        ; kind_signatures <- xoptM Opt_KindSignatures
        ; is_boot         <- tcIsHsBoot  -- Are we compiling an hs-boot file?
 
@@ -877,7 +878,7 @@ tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM CoAxBranch
 -- Placed here because type family instances appear as
 -- default decls in class declarations
 tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqn = eqn })
-  = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
+  = do { checkTc (isSynFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
        ; tcTyFamInstEqn (tyConName fam_tc) (tyConKind fam_tc) eqn }
 
 -- Checks to make sure that all the names in an instance group are the same
@@ -1463,8 +1464,8 @@ checkValidClosedCoAxiom (CoAxiom { co_ax_branches = branches, co_ax_tc = tc })
                -- ones and hence is inaccessible
      check_accessibility prev_branches cur_branch
        = do { when (cur_branch `isDominatedBy` prev_branches) $
-              setSrcSpan (coAxBranchSpan cur_branch) $
-              addErrTc $ inaccessibleCoAxBranch tc cur_branch
+              addWarnAt (coAxBranchSpan cur_branch) $
+              inaccessibleCoAxBranch tc cur_branch
             ; return (cur_branch : prev_branches) }
 
 checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet
@@ -1669,9 +1670,9 @@ checkValidRoleAnnots :: RoleAnnots -> TyThing -> TcM ()
 checkValidRoleAnnots role_annots thing
   = case thing of
     { ATyCon tc
-        | isSynTyCon tc    -> check_no_roles
-        | isFamilyTyCon tc -> check_no_roles
-        | isAlgTyCon tc    -> check_roles
+        | isTypeSynonymTyCon tc -> check_no_roles
+        | isFamilyTyCon tc      -> check_no_roles
+        | isAlgTyCon tc         -> check_roles
         where
           name                   = tyConName tc
 
@@ -1694,6 +1695,15 @@ checkValidRoleAnnots role_annots thing
                 ; checkTc (type_vars `equalLength` the_role_annots)
                           (wrongNumberOfRoles type_vars decl)
                 ; _ <- zipWith3M checkRoleAnnot type_vars the_role_annots type_roles
+                -- Representational or phantom roles for class parameters
+                -- quickly lead to incoherence. So, we require
+                -- IncoherentInstances to have them. See #8773.
+                ; incoherent_roles_ok <- xoptM Opt_IncoherentInstances
+                ; checkTc (  incoherent_roles_ok
+                          || (not $ isClassTyCon tc)
+                          || (all (== Nominal) type_roles))
+                          incoherentRoles
+                  
                 ; lint <- goptM Opt_DoCoreLinting
                 ; when lint $ checkValidRoles tc }
 
@@ -1823,7 +1833,7 @@ mkRecSelBinds tycons
 
 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, LHsBinds Name)
 mkRecSelBind (tycon, sel_name)
-  = (L loc (IdSig sel_id), unitBag (Generated, L loc sel_bind))
+  = (L loc (IdSig sel_id), unitBag (L loc sel_bind))
   where
     loc    = getSrcSpan sel_name
     sel_id = Var.mkExportedLocalVar rec_details sel_name
@@ -1852,8 +1862,10 @@ mkRecSelBind (tycon, sel_name)
     -- Make the binding: sel (C2 { fld = x }) = x
     --                   sel (C7 { fld = x }) = x
     --    where cons_w_field = [C2,C7]
-    sel_bind | is_naughty = mkTopFunBind sel_lname [mkSimpleMatch [] unit_rhs]
-             | otherwise  = mkTopFunBind sel_lname (map mk_match cons_w_field ++ deflt)
+    sel_bind = mkTopFunBind Generated sel_lname alts
+      where
+        alts | is_naughty = [mkSimpleMatch [] unit_rhs]
+             | otherwise =  map mk_match cons_w_field ++ deflt
     mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
                                  (L loc (HsVar field_var))
     mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
@@ -2151,7 +2163,7 @@ wrongNamesInInstGroup first cur
 
 inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
 inaccessibleCoAxBranch tc fi
-  = ptext (sLit "Inaccessible family instance equation:") $$
+  = ptext (sLit "Overlapped type family instance equation:") $$
       (pprCoAxBranch tc fi)
 
 badRoleAnnot :: Name -> Role -> Role -> SDoc
@@ -2180,6 +2192,11 @@ needXRoleAnnotations tc
   = ptext (sLit "Illegal role annotation for") <+> ppr tc <> char ';' $$
     ptext (sLit "did you intend to use RoleAnnotations?")
 
+incoherentRoles :: SDoc
+incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+>
+                   text "for class parameters can lead to incoherence.") $$
+                  (text "Use IncoherentInstances to allow this; bad role found")
+
 addTyThingCtxt :: TyThing -> TcM a -> TcM a
 addTyThingCtxt thing
   = addErrCtxt ctxt
@@ -2187,12 +2204,12 @@ addTyThingCtxt thing
     name = getName thing
     flav = case thing of
              ATyCon tc
-                | isClassTyCon tc      -> ptext (sLit "class")
-                | isSynFamilyTyCon tc  -> ptext (sLit "type family")
-                | isDataFamilyTyCon tc -> ptext (sLit "data family")
-                | isSynTyCon tc        -> ptext (sLit "type")
-                | isNewTyCon tc        -> ptext (sLit "newtype")
-                | isDataTyCon tc       -> ptext (sLit "data")
+                | isClassTyCon tc       -> ptext (sLit "class")
+                | isSynFamilyTyCon tc   -> ptext (sLit "type family")
+                | isDataFamilyTyCon tc  -> ptext (sLit "data family")
+                | isTypeSynonymTyCon tc -> ptext (sLit "type")
+                | isNewTyCon tc         -> ptext (sLit "newtype")
+                | isDataTyCon tc        -> ptext (sLit "data")
 
              _ -> pprTrace "addTyThingCtxt strange" (ppr thing)
                   empty

compiler/typecheck/TcTyDecls.lhs

@@ -672,10 +672,10 @@ initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
 
 initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
 initialRoleEnv1 is_boot annots_env tc
-  | isFamilyTyCon tc = (name, map (const Nominal) tyvars)
-  |  isAlgTyCon tc
-  || isSynTyCon tc   = (name, default_roles)
-  | otherwise        = pprPanic "initialRoleEnv1" (ppr tc)
+  | isFamilyTyCon tc      = (name, map (const Nominal) tyvars)
+  | isAlgTyCon tc         = (name, default_roles)
+  | isTypeSynonymTyCon tc = (name, default_roles)
+  | otherwise             = pprPanic "initialRoleEnv1" (ppr tc)
   where name         = tyConName tc
         tyvars       = tyConTyVars tc
         (kvs, tvs)   = span isKindVar tyvars
@@ -709,6 +709,8 @@ irTyCon tc
        ; unless (all (== Nominal) old_roles) $  -- also catches data families,
                                                 -- which don't want or need role inference
     do { whenIsJust (tyConClass_maybe tc) (irClass tc_name)
+       ; addRoleInferenceInfo tc_name (tyConTyVars tc) $
+         mapM_ (irType emptyVarSet) (tyConStupidTheta tc)  -- See #8958
        ; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
 
   | Just (SynonymTyCon ty) <- synTyConRhs_maybe tc
@@ -778,7 +780,7 @@ lookupRoles tc
            Just roles -> return roles
            Nothing    -> return $ tyConRoles tc }
 
--- tries to update a role; won't even update a role "downwards"
+-- tries to update a role; won't ever update a role "downwards"
 updateRole :: Role -> TyVar -> RoleM ()
 updateRole role tv
   = do { var_ns <- getVarNs

compiler/typecheck/TcType.lhs

@@ -245,34 +245,23 @@ checking.  It's attached to mutable type variables only.
 It's knot-tied back to Var.lhs.  There is no reason in principle
 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 
-
 Note [Signature skolems]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this
 
-  x :: [a]
-  y :: b
-  (x,y,z) = ([y,z], z, head x)
-
-Here, x and y have type sigs, which go into the environment.  We used to
-instantiate their types with skolem constants, and push those types into
-the RHS, so we'd typecheck the RHS with type
-        ( [a*], b*, c )
-where a*, b* are skolem constants, and c is an ordinary meta type varible.
-
-The trouble is that the occurrences of z in the RHS force a* and b* to
-be the *same*, so we can't make them into skolem constants that don't unify
-with each other.  Alas.
-
-One solution would be insist that in the above defn the programmer uses
-the same type variable in both type signatures.  But that takes explanation.
+  f :: forall a. [a] -> Int
+  f (x::b : xs) = 3
 
-The alternative (currently implemented) is to have a special kind of skolem
-constant, SigTv, which can unify with other SigTvs.  These are *not* treated
-as rigid for the purposes of GADTs.  And they are used *only* for pattern
-bindings and mutually recursive function bindings.  See the function
-TcBinds.tcInstSig, and its use_skols parameter.
+Here 'b' is a lexically scoped type variable, but it turns out to be
+the same as the skolem 'a'.  So we have a special kind of skolem
+constant, SigTv, which can unify with other SigTvs. They are used
+*only* for pattern type signatures.
 
+Similarly consider
+  data T (a:k1) = MkT (S a)
+  data S (b:k2) = MkS (T b)
+When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
+because they end up unifying; we want those SigTvs again.
 
 \begin{code}
 -- A TyVarDetails is inside a TyVar
@@ -972,7 +961,7 @@ tcInstHeadTyNotSynonym :: Type -> Bool
 -- are transparent, so we need a special function here
 tcInstHeadTyNotSynonym ty
   = case ty of
-        TyConApp tc _ -> not (isSynTyCon tc)
+        TyConApp tc _ -> not (isTypeSynonymTyCon tc)
         _ -> True
 
 tcInstHeadTyAppAllTyVars :: Type -> Bool
@@ -1018,7 +1007,8 @@ tcEqType ty1 ty2
                  | Just t2' <- tcView t2 = go env t1 t2'
     go env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
     go _   (LitTy lit1)        (LitTy lit2)      = lit1 == lit2
-    go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go (rnBndr2 env tv1 tv2) t1 t2
+    go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go env (tyVarKind tv1) (tyVarKind tv2)
+                                                && go (rnBndr2 env tv1 tv2) t1 t2
     go env (AppTy s1 t1)       (AppTy s2 t2)     = go env s1 s2 && go env t1 t2
     go env (FunTy s1 t1)       (FunTy s2 t2)     = go env s1 s2 && go env t1 t2
     go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
@@ -1037,7 +1027,8 @@ pickyEqType ty1 ty2
     init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
     go env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
     go _   (LitTy lit1)        (LitTy lit2)      = lit1 == lit2
-    go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go (rnBndr2 env tv1 tv2) t1 t2
+    go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go env (tyVarKind tv1) (tyVarKind tv2)
+                                                && go (rnBndr2 env tv1 tv2) t1 t2
     go env (AppTy s1 t1)       (AppTy s2 t2)     = go env s1 s2 && go env t1 t2
     go env (FunTy s1 t1)       (FunTy s2 t2)     = go env s1 s2 && go env t1 t2
     go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2

compiler/typecheck/TcTypeNats.hs

@@ -12,9 +12,14 @@ import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi )
 import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..) )
 import Name       ( Name, BuiltInSyntax(..) )
-import TysWiredIn ( typeNatKind, mkWiredInTyConName
+import TysWiredIn ( typeNatKind, typeSymbolKind
+                  , mkWiredInTyConName
                   , promotedBoolTyCon
                   , promotedFalseDataCon, promotedTrueDataCon
+                  , promotedOrderingTyCon
+                  , promotedLTDataCon
+                  , promotedEQDataCon
+                  , promotedGTDataCon
                   )
 import TysPrim    ( tyVarList, mkArrowKinds )
 import PrelNames  ( gHC_TYPELITS
@@ -23,6 +28,8 @@ import PrelNames  ( gHC_TYPELITS
                   , typeNatExpTyFamNameKey
                   , typeNatLeqTyFamNameKey
                   , typeNatSubTyFamNameKey
+                  , typeNatCmpTyFamNameKey
+                  , typeSymbolCmpTyFamNameKey
                   )
 import FastString ( FastString, fsLit )
 import qualified Data.Map as Map
@@ -39,6 +46,8 @@ typeNatTyCons =
   , typeNatExpTyCon
   , typeNatLeqTyCon
   , typeNatSubTyCon
+  , typeNatCmpTyCon
+  , typeSymbolCmpTyCon
   ]
 
 typeNatAddTyCon :: TyCon
@@ -103,6 +112,45 @@ typeNatLeqTyCon =
     , sfInteractInert = interactInertLeq
     }
 
+typeNatCmpTyCon :: TyCon
+typeNatCmpTyCon =
+  mkSynTyCon name
+    (mkArrowKinds [ typeNatKind, typeNatKind ] orderingKind)
+    (take 2 $ tyVarList typeNatKind)
+    [Nominal,Nominal]
+    (BuiltInSynFamTyCon ops)
+    NoParentTyCon
+
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpNat")
+                typeNatCmpTyFamNameKey typeNatCmpTyCon
+  ops = BuiltInSynFamily
+    { sfMatchFam      = matchFamCmpNat
+    , sfInteractTop   = interactTopCmpNat
+    , sfInteractInert = \_ _ _ _ -> []
+    }
+
+typeSymbolCmpTyCon :: TyCon
+typeSymbolCmpTyCon =
+  mkSynTyCon name
+    (mkArrowKinds [ typeSymbolKind, typeSymbolKind ] orderingKind)
+    (take 2 $ tyVarList typeSymbolKind)
+    [Nominal,Nominal]
+    (BuiltInSynFamTyCon ops)
+    NoParentTyCon
+
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpSymbol")
+                typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon
+  ops = BuiltInSynFamily
+    { sfMatchFam      = matchFamCmpSymbol
+    , sfInteractTop   = interactTopCmpSymbol
+    , sfInteractInert = \_ _ _ _ -> []
+    }
+
+
+
+
 
 -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
 mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
@@ -127,6 +175,8 @@ axAddDef
   , axMulDef
   , axExpDef
   , axLeqDef
+  , axCmpNatDef
+  , axCmpSymbolDef
   , axAdd0L
   , axAdd0R
   , axMul0L
@@ -137,6 +187,8 @@ axAddDef
   , axExp0R
   , axExp1R
   , axLeqRefl
+  , axCmpNatRefl
+  , axCmpSymbolRefl
   , axLeq0L
   , axSubDef
   , axSub0R
@@ -154,6 +206,25 @@ axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
 axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
               \x y -> Just $ bool (x <= y)
 
+axCmpNatDef   = mkBinAxiom "CmpNatDef" typeNatCmpTyCon
+              $ \x y -> Just $ ordering (compare x y)
+
+axCmpSymbolDef =
+  CoAxiomRule
+    { coaxrName      = fsLit "CmpSymbolDef"
+    , coaxrTypeArity = 2
+    , coaxrAsmpRoles = []
+    , coaxrRole      = Nominal
+    , coaxrProves    = \ts cs ->
+        case (ts,cs) of
+          ([s,t],[]) ->
+            do x <- isStrLitTy s
+               y <- isStrLitTy t
+               return (mkTyConApp typeSymbolCmpTyCon [s,t] ===
+                      ordering (compare x y))
+          _ -> Nothing
+    }
+
 axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
               \x y -> fmap num (minus x y)
 
@@ -168,6 +239,10 @@ axExp1L     = mkAxiom1 "Exp1L"    $ \t -> (num 1 .^. t) === num 1
 axExp0R     = mkAxiom1 "Exp0R"    $ \t -> (t .^. num 0) === num 1
 axExp1R     = mkAxiom1 "Exp1R"    $ \t -> (t .^. num 1) === t
 axLeqRefl   = mkAxiom1 "LeqRefl"  $ \t -> (t <== t) === bool True
+axCmpNatRefl    = mkAxiom1 "CmpNatRefl"
+                $ \t -> (cmpNat t t) === ordering EQ
+axCmpSymbolRefl = mkAxiom1 "CmpSymbolRefl"
+                $ \t -> (cmpSymbol t t) === ordering EQ
 axLeq0L     = mkAxiom1 "Leq0L"    $ \t -> (num 0 <== t) === bool True
 
 typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
@@ -176,6 +251,8 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axMulDef
   , axExpDef
   , axLeqDef
+  , axCmpNatDef
+  , axCmpSymbolDef
   , axAdd0L
   , axAdd0R
   , axMul0L
@@ -186,6 +263,8 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axExp0R
   , axExp1R
   , axLeqRefl
+  , axCmpNatRefl
+  , axCmpSymbolRefl
   , axLeq0L
   , axSubDef
   ]
@@ -211,6 +290,12 @@ s .^. t = mkTyConApp typeNatExpTyCon [s,t]
 (<==) :: Type -> Type -> Type
 s <== t = mkTyConApp typeNatLeqTyCon [s,t]
 
+cmpNat :: Type -> Type -> Type
+cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]
+
+cmpSymbol :: Type -> Type -> Type
+cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t]
+
 (===) :: Type -> Type -> Pair Type
 x === y = Pair x y
 
@@ -232,6 +317,25 @@ isBoolLitTy tc =
          | tc == promotedTrueDataCon  -> return True
          | otherwise                   -> Nothing
 
+orderingKind :: Kind
+orderingKind = mkTyConApp promotedOrderingTyCon []
+
+ordering :: Ordering -> Type
+ordering o =
+  case o of
+    LT -> mkTyConApp promotedLTDataCon []
+    EQ -> mkTyConApp promotedEQDataCon []
+    GT -> mkTyConApp promotedGTDataCon []
+
+isOrderingLitTy :: Type -> Maybe Ordering
+isOrderingLitTy tc =
+  do (tc1,[]) <- splitTyConApp_maybe tc
+     case () of
+       _ | tc1 == promotedLTDataCon -> return LT
+         | tc1 == promotedEQDataCon -> return EQ
+         | tc1 == promotedGTDataCon -> return GT
+         | otherwise                -> Nothing
+
 known :: (Integer -> Bool) -> TcType -> Bool
 known p x = case isNumLitTy x of
               Just a  -> p a
@@ -258,6 +362,8 @@ mkBinAxiom str tc f =
           _ -> Nothing
     }
 
+
+
 mkAxiom1 :: String -> (Type -> Pair Type) -> CoAxiomRule
 mkAxiom1 str f =
   CoAxiomRule
@@ -328,6 +434,25 @@ matchFamLeq [s,t]
         mbY = isNumLitTy t
 matchFamLeq _ = Nothing
 
+matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamCmpNat [s,t]
+  | Just x <- mbX, Just y <- mbY =
+    Just (axCmpNatDef, [s,t], ordering (compare x y))
+  | tcEqType s t = Just (axCmpNatRefl, [s], ordering EQ)
+  where mbX = isNumLitTy s
+        mbY = isNumLitTy t
+matchFamCmpNat _ = Nothing
+
+matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamCmpSymbol [s,t]
+  | Just x <- mbX, Just y <- mbY =
+    Just (axCmpSymbolDef, [s,t], ordering (compare x y))
+  | tcEqType s t = Just (axCmpSymbolRefl, [s], ordering EQ)
+  where mbX = isStrLitTy s
+        mbY = isStrLitTy t
+matchFamCmpSymbol _ = Nothing
+
+
 {-------------------------------------------------------------------------------
 Interact with axioms
 -------------------------------------------------------------------------------}
@@ -415,6 +540,17 @@ interactTopLeq [s,t] r
   mbZ = isBoolLitTy r
 interactTopLeq _ _ = []
 
+interactTopCmpNat :: [Xi] -> Xi -> [Pair Type]
+interactTopCmpNat [s,t] r
+  | Just EQ <- isOrderingLitTy r = [ s === t ]
+interactTopCmpNat _ _ = []
+
+interactTopCmpSymbol :: [Xi] -> Xi -> [Pair Type]
+interactTopCmpSymbol [s,t] r
+  | Just EQ <- isOrderingLitTy r = [ s === t ]
+interactTopCmpSymbol _ _ = []
+
+
 
 
 {-------------------------------------------------------------------------------
@@ -466,6 +602,10 @@ interactInertLeq _ _ _ _ = []
 
 
 
+
+
+
+
 {- -----------------------------------------------------------------------------
 These inverse functions are used for simplifying propositions using
 concrete natural numbers.

compiler/typecheck/TcUnify.lhs

@@ -824,8 +824,8 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
 	   -- k1 = k2, so we are free to update either way
            (EQ, MetaTv { mtv_info = i1, mtv_ref = ref1 }, 
                 MetaTv { mtv_info = i2, mtv_ref = ref2 })
-                | nicer_to_update_tv1 i1 i2 -> updateMeta tv1 ref1 ty2
-                | otherwise                 -> updateMeta tv2 ref2 ty1
+                | nicer_to_update_tv1 tv1 i1 i2 -> updateMeta tv1 ref1 ty2
+                | otherwise                     -> updateMeta tv2 ref2 ty1
            (EQ, MetaTv { mtv_ref = ref1 }, _) -> updateMeta tv1 ref1 ty2
            (EQ, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
 
@@ -838,9 +838,10 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
     ty1 = mkTyVarTy tv1
     ty2 = mkTyVarTy tv2
 
-    nicer_to_update_tv1 _     SigTv = True
-    nicer_to_update_tv1 SigTv _     = False
-    nicer_to_update_tv1 _         _ = isSystemName (Var.varName tv1)
+nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool
+nicer_to_update_tv1 _   _     SigTv = True
+nicer_to_update_tv1 _   SigTv _     = False
+nicer_to_update_tv1 tv1 _     _     = isSystemName (Var.varName tv1)
         -- Try not to update SigTvs; and try to update sys-y type
         -- variables in preference to ones gotten (say) by
         -- instantiating a polymorphic function with a user-written
@@ -1069,6 +1070,31 @@ one of argTypeKind or openTypeKind.
 The situation is different in the core of the compiler, where we are perfectly
 happy to have types of kind Constraint on either end of an arrow.
 
+Note [Kind variables can be untouchable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We must use the careful function lookupTcTyVar to see if a kind
+variable is filled or unifiable.  It checks for touchablity, and kind
+variables can certainly be untouchable --- for example the variable
+might be bound outside an enclosing existental pattern match that
+binds an inner kind variable, which we don't want ot escape outside.
+
+This, or something closely related, was teh cause of Trac #8985.
+
+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 calling lookupTcTyVar.
+
+
 \begin{code}
 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
 -- Like unifyFunTy, but does not fail; instead just returns Nothing
@@ -1117,37 +1143,66 @@ unifyKindX (TyConApp kc1 []) (TyConApp kc2 [])
 unifyKindX k1 k2 = unifyKindEq k1 k2
   -- In all other cases, let unifyKindEq do the work
 
+-------------------
 uKVar :: SwapFlag -> (TcKind -> TcKind -> TcM (Maybe Ordering))
       -> MetaKindVar -> TcKind -> TcM (Maybe Ordering)
 uKVar swapped unify_kind kv1 k2
-  | isTcTyVar kv1, isMetaTyVar kv1       -- See Note [Unifying kind variables]
-  = do  { mb_k1 <- readMetaTyVar kv1
-        ; case mb_k1 of
-            Flexi -> uUnboundKVar kv1 k2
-            Indirect k1 -> unSwap swapped unify_kind k1 k2 }
-  | TyVarTy kv2 <- k2, kv1 == kv2 
+  | isTcTyVar kv1
+  = do { lookup_res <- lookupTcTyVar kv1  -- See Note [Kind variables can be untouchable]
+       ; case lookup_res of
+           Filled k1    -> unSwap swapped unify_kind k1 k2
+           Unfilled ds1 -> uUnfilledKVar kv1 ds1 k2 }
+
+  | otherwise   -- See Note [Unifying kind variables]
+  = uUnfilledKVar kv1 vanillaSkolemTv k2
+
+-------------------
+uUnfilledKVar :: MetaKindVar -> TcTyVarDetails -> TcKind -> TcM (Maybe Ordering)
+uUnfilledKVar kv1 ds1 (TyVarTy kv2)
+  | kv1 == kv2
   = return (Just EQ)
 
-  | TyVarTy kv2 <- k2, isTcTyVar kv2, isMetaTyVar kv2
-  = uKVar (flipSwap swapped) unify_kind kv2 (TyVarTy kv1)
+  | isTcTyVar kv2
+  = do { lookup_res <- lookupTcTyVar kv2
+       ; case lookup_res of
+           Filled k2    -> uUnfilledKVar  kv1 ds1 k2
+           Unfilled ds2 -> uUnfilledKVars kv1 ds1 kv2 ds2 }
 
-  | otherwise 
-  = return Nothing
+  | otherwise  -- See Note [Unifying kind variables]
+  = uUnfilledKVars kv1 ds1 kv2 vanillaSkolemTv
 
-{- 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.
--}
+uUnfilledKVar kv1 ds1 non_var_k2
+  = case ds1 of
+      MetaTv { mtv_info = SigTv }
+        -> return Nothing
+      MetaTv { mtv_ref = ref1 }
+        -> do { k2a <- zonkTcKind non_var_k2
+              ; let k2b = defaultKind k2a
+                     -- MetaKindVars must be bound only to simple kinds
+
+              ; dflags <- getDynFlags
+              ; case occurCheckExpand dflags kv1 k2b of
+                   OC_OK k2c -> do { writeMetaTyVarRef kv1 ref1 k2c; return (Just EQ) }
+                   _         -> return Nothing }
+      _ -> return Nothing
+
+-------------------
+uUnfilledKVars :: MetaKindVar -> TcTyVarDetails
+               -> MetaKindVar -> TcTyVarDetails
+               -> TcM (Maybe Ordering)
+-- kv1 /= kv2
+uUnfilledKVars kv1 ds1 kv2 ds2
+  = case (ds1, ds2) of
+      (MetaTv { mtv_info = i1, mtv_ref = r1 },
+       MetaTv { mtv_info = i2, mtv_ref = r2 })
+              | nicer_to_update_tv1 kv1 i1 i2 -> do_update kv1 r1 kv2
+              | otherwise                     -> do_update kv2 r2 kv1
+      (MetaTv { mtv_ref = r1 }, _) -> do_update kv1 r1 kv2
+      (_, MetaTv { mtv_ref = r2 }) -> do_update kv2 r2 kv1
+      _ -> return Nothing
+  where
+    do_update kv1 r1 kv2
+      = do { writeMetaTyVarRef kv1 r1 (mkTyVarTy kv2); return (Just EQ) }
 
 ---------------------------
 unifyKindEq :: TcKind -> TcKind -> TcM (Maybe Ordering)
@@ -1159,41 +1214,16 @@ unifyKindEq k1 (TyVarTy kv2) = uKVar IsSwapped  unifyKindEq kv2 k1
 unifyKindEq (FunTy a1 r1) (FunTy a2 r2)
   = do { mb1 <- unifyKindEq a1 a2; mb2 <- unifyKindEq r1 r2
        ; return (if isJust mb1 && isJust mb2 then Just EQ else Nothing) }
-  
+
 unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
   | kc1 == kc2
   = ASSERT(length k1s == length k2s)
-       -- Should succeed since the kind constructors are the same, 
+       -- Should succeed since the kind constructors are the same,
        -- and the kinds are sort-checked, thus fully applied
     do { mb_eqs <- zipWithM unifyKindEq k1s k2s
-       ; return (if all isJust mb_eqs 
-                 then Just EQ 
+       ; return (if all isJust mb_eqs
+                 then Just EQ
                  else Nothing) }
 
 unifyKindEq _ _ = return Nothing
-
-----------------
-uUnboundKVar :: MetaKindVar -> TcKind -> TcM (Maybe Ordering)
-uUnboundKVar kv1 k2@(TyVarTy kv2)
-  | kv1 == kv2 = return (Just EQ)
-  | isTcTyVar kv2, isMetaTyVar kv2   -- Distinct kind variables
-  = do  { mb_k2 <- readMetaTyVar kv2
-        ; case mb_k2 of
-            Indirect k2 -> uUnboundKVar kv1 k2
-            Flexi       -> do { writeMetaTyVar kv1 k2; return (Just EQ) } }
-  | otherwise 
-  = do { writeMetaTyVar kv1 k2; return (Just EQ) }
-
-uUnboundKVar kv1 non_var_k2
-  | isSigTyVar kv1
-  = return Nothing
-  | otherwise
-  = do { k2a <- zonkTcKind non_var_k2
-       ; let k2b = defaultKind k2a
-                -- MetaKindVars must be bound only to simple kinds
-
-       ; dflags <- getDynFlags 
-       ; case occurCheckExpand dflags kv1 k2b of
-           OC_OK k2c -> do { writeMetaTyVar kv1 k2c; return (Just EQ) }
-           _         -> return Nothing }
 \end{code}