Do not instantiate unification variables with polytypes
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 31 Oct 2012 09:08:39 +0000 (09:08 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 31 Oct 2012 09:08:39 +0000 (09:08 +0000)
Without -XImpredicativeTypes, the typing rules say that a function
should be instantiated only at a *monotype*.  In implementation terms,
that means that a unification variable should not unify with a type
involving foralls.  But we were not enforcing that rule, and that
gave rise to some confusing error messages, such as
  Trac #7264, #6069

This patch adds the test for foralls.  There are consequences

 * I put the test in occurCheckExpand, since that is where we see if a
   type can unify with a given unification variable.  So
   occurCheckExpand has to get DynFlags, so it can test for
   -XImpredicativeTypes

 * We want this to work
      foo :: (forall a. a -> a) -> Int
      foo = error "foo"
   But that means instantiating error at a polytype!  But error is special
   already because you can instantiate it at an unboxed type like Int#.
   So I extended the specialness to allow type variables of openTypeKind
   to unify with polytypes, regardless of -XImpredicativeTypes.

   Conveniently, this works in TcUnify.matchExpectedFunTys, which generates
   unification variable for the function arguments, which can be polymorphic.

 * GHC has a special typing rule for ($) (see Note [Typing rule
   for ($)] in TcExpr).  It unifies the argument and result with a
   unification variable to exclude unboxed types -- but that means I
   now need a kind of unificatdion variable that *can* unify with a
   polytype.

   So for this sole case I added PolyTv to the data type TcType.MetaInfo.
   I suspect we'll find mor uses for this, and the changes are tiny,
   but it still feel a bit of a hack.  Well the special rule for ($)
   is a hack!

There were some consequential changes in error reporting (TcErrors).

compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs

index 3309e12..3dd8844 100644 (file)
@@ -1150,17 +1150,12 @@ canEqLeafTyVarEq loc ev tv s2              -- ev :: tv ~ s2
                       setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo xi1)) co)
                     ; return Stop } ;
 
-           (Just tv1', _) ->
+           (Just tv1', _) -> do
 
          -- LHS rewrote to a type variable, RHS to something else
-         case occurCheckExpand tv1' xi2 of
-           Nothing ->  -- Occurs check error
-                       do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
-                          ; case mb of
-                              Nothing     -> return Stop
-                              Just new_ev -> canEqFailure loc new_ev xi1 xi2 }
-
-           Just xi2' -> -- No occurs check, so we can continue; but make sure
+       { dflags <- getDynFlags
+       ; case occurCheckExpand dflags tv1' xi2 of
+           OC_OK xi2' -> -- No occurs check, so we can continue; but make sure
                         -- that the new goal has enough type synonyms expanded by 
                         -- by the occurCheckExpand
                         do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2') co
@@ -1169,7 +1164,13 @@ canEqLeafTyVarEq loc ev tv s2              -- ev :: tv ~ s2
                                Just new_ev -> continueWith $
                                               CTyEqCan { cc_ev = new_ev, cc_loc = loc
                                                        , cc_tyvar  = tv1', cc_rhs = xi2' } }
-    } }
+           _bad ->  -- Occurs check error
+                       do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
+                          ; case mb of
+                              Nothing     -> return Stop
+                              Just new_ev -> canEqFailure loc new_ev xi1 xi2 }
+
+    } } }
 
 mkHdEqPred :: Type -> TcCoercion -> TcCoercion -> TcCoercion
 -- Make a higher-dimensional equality
index 6ac8793..5fe27f7 100644 (file)
@@ -548,7 +548,8 @@ mkEqErr1 ctxt ct
   | isGiven ev
   = do { (ctxt, binds_msg) <- relevantBindings ctxt ct
        ; let (given_loc, given_msg) = mk_given (cec_encl ctxt)
-       ; mkEqErr_help ctxt (given_msg $$ binds_msg) 
+       ; dflags <- getDynFlags
+       ; mkEqErr_help dflags ctxt (given_msg $$ binds_msg) 
                       (ct { cc_loc = given_loc}) -- Note [Inaccessible code]
                       Nothing ty1 ty2 }
 
@@ -556,7 +557,8 @@ mkEqErr1 ctxt ct
   = do { (ctxt, binds_msg) <- relevantBindings ctxt ct
        ; (ctxt, tidy_orig) <- zonkTidyOrigin ctxt (ctLocOrigin (cc_loc ct))
        ; let (is_oriented, wanted_msg) = mk_wanted_extra tidy_orig
-       ; mkEqErr_help ctxt (wanted_msg $$ binds_msg) 
+       ; dflags <- getDynFlags
+       ; mkEqErr_help dflags ctxt (wanted_msg $$ binds_msg) 
                       ct is_oriented ty1 ty2 }
   where
     ev         = cc_ev ct
@@ -587,45 +589,66 @@ mkEqErr1 ctxt ct
 
     mk_wanted_extra _ = (Nothing, empty)
 
-mkEqErr_help, reportEqErr 
-   :: ReportErrCtxt -> SDoc
-   -> Ct
-   -> Maybe SwapFlag   -- Nothing <=> not sure
-   -> TcType -> TcType -> TcM ErrMsg
-mkEqErr_help ctxt extra ct oriented ty1 ty2
-  | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-  | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt extra ct swapped  tv2 ty1
+mkEqErr_help :: DynFlags -> ReportErrCtxt -> SDoc
+             -> Ct          
+             -> Maybe SwapFlag   -- Nothing <=> not sure
+             -> TcType -> TcType -> TcM ErrMsg
+mkEqErr_help dflags ctxt extra ct oriented ty1 ty2
+  | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
+  | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr dflags ctxt extra ct swapped  tv2 ty1
   | otherwise                        = reportEqErr  ctxt extra ct oriented ty1 ty2
   where
     swapped = fmap flipSwap oriented
 
+reportEqErr :: ReportErrCtxt -> SDoc
+            -> Ct    
+            -> Maybe SwapFlag   -- Nothing <=> not sure
+            -> TcType -> TcType -> TcM ErrMsg
 reportEqErr ctxt extra1 ct oriented ty1 ty2
   = do { (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
        ; mkErrorMsg ctxt' ct (vcat [ misMatchOrCND ctxt' ct oriented ty1 ty2
                                    , extra2, extra1]) }
 
-mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
+mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> SDoc -> Ct 
+             -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
-mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-  -- Occurs check
-  |  isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
-                            -- be oriented the other way round; see TcCanonical.reOrient
-  || isSigTyVar tv1 && not (isTyVarTy ty2)
+mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
+  | isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
+                            -- be oriented the other way round; see TcCanonical.reOrient
   = mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
                              , extraTyVarInfo ctxt ty1 ty2
                              , extra ])
 
-  -- So tv is a meta tyvar, and presumably it is
-  -- an *untouchable* meta tyvar, else it'd have been unified
+  -- So tv is a meta tyvar (or started that way before we 
+  -- generalised it).  So presumably it is an *untouchable* 
+  -- meta tyvar or a SigTv, else it'd have been unified
   | not (k2 `tcIsSubKind` k1)           -- Kind error
   = mkErrorMsg ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
 
-  | isNothing (occurCheckExpand tv1 ty2)
+  | OC_Occurs <- occ_check_expand
   = do { let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:")
                               2 (sep [ppr ty1, char '~', ppr ty2])
        ; (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
        ; mkErrorMsg ctxt' ct (occCheckMsg $$ extra2 $$ extra) }
 
+  | OC_Forall <- occ_check_expand
+  = do { let msg = vcat [ ptext (sLit "Cannot instantiate unification variable")
+                          <+> quotes (ppr tv1)
+                        , hang (ptext (sLit "with a type involving foralls:")) 2 (ppr ty2)
+                        , nest 2 (ptext (sLit "Perhaps you want -XImpredicativeTypes")) ]
+       ; mkErrorMsg ctxt ct msg }
+
+  -- If the immediately-enclosing implication has 'tv' a skolem, and
+  -- we know by now its an InferSkol kind of skolem, then presumably
+  -- it started life as a SigTv, else it'd have been unified.
+  -- So just report a mis-match here, without gettin into occurs-checks etc
+  | (implic:_) <- cec_encl ctxt
+  , Implic { ic_skols = skols } <- implic
+  , tv1 `elem` skols
+  = mkErrorMsg ctxt ct (vcat [ misMatchMsg oriented ty1 ty2
+                             , extraTyVarInfo ctxt ty1 ty2
+                             , extra ])
+
   -- Check for skolem escape
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
   , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
@@ -665,6 +688,7 @@ mkTyVarEqErr ctxt extra ct oriented tv1 ty2
         -- Consider an ambiguous top-level constraint (a ~ F a)
         -- Not an occurs check, becuase F is a type function.
   where         
+    occ_check_expand = occurCheckExpand dflags tv1 ty2
     k1         = tyVarKind tv1
     k2         = typeKind ty2
     ty1 = mkTyVarTy tv1
index 9075033..d554588 100644 (file)
@@ -318,10 +318,13 @@ tcExpr (OpApp arg1 op fix arg2) res_ty
 
        -- Make sure that the argument and result types have kind '*'
        -- Eg we do not want to allow  (D#  $  4.0#)   Trac #5570
-       -- ($) :: forall ab. (a->b) -> a -> b
-       ; a_ty <- newFlexiTyVarTy liftedTypeKind
-       ; b_ty <- newFlexiTyVarTy liftedTypeKind
+       --    (which gives a seg fault)
+       -- We do this by unifying with a MetaTv; but of course
+       -- it must allow foralls in the type it unifies with (hence PolyTv)!
 
+       -- ($) :: forall ab. (a->b) -> a -> b
+       ; a_ty <- newPolyFlexiTyVarTy
+       ; b_ty <- newPolyFlexiTyVarTy
        ; arg2' <- tcArg op (arg2, arg2_ty, 2)
 
        ; co_res <- unifyType b_ty res_ty        -- b ~ res
index 70559f7..36762b9 100644 (file)
@@ -67,14 +67,13 @@ import NameEnv
 import TysWiredIn
 import BasicTypes
 import SrcLoc
-import DynFlags ( ExtensionFlag( Opt_DataKinds ) )
+import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags )
 import Unique
 import UniqSupply
 import Outputable
 import FastString
 import Util
 
-import Data.Maybe
 import Control.Monad ( unless, when, zipWithM )
 import PrelNames( ipClassName, funTyConKey )
 \end{code}
@@ -1229,7 +1228,8 @@ Here
 
  * Then unificaiton makes a_sig := a_sk
 
-That's why we must make a_sig a SigTv, not a SkolemTv, so that it can unify to a_sk.
+That's why we must make a_sig a MetaTv (albeit a SigTv), 
+not a SkolemTv, so that it can unify to a_sk.
 
 For RULE binders, though, things are a bit different (yuk).  
   RULE "foo" forall (x::a) (y::[a]).  f x y = ...
@@ -1340,6 +1340,7 @@ checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
       ; act_kind <- zonkTcKind act_kind
       ; traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr exp_kind)
       ; env0 <- tcInitTidyEnv
+      ; dflags <- getDynFlags
       ; let (exp_as, _) = splitKindFunTys exp_kind
             (act_as, _) = splitKindFunTys act_kind
             n_exp_as  = length exp_as
@@ -1351,12 +1352,16 @@ checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
 
             occurs_check 
                | Just act_tv <- tcGetTyVar_maybe act_kind
-               = isNothing (occurCheckExpand act_tv exp_kind)
+               = check_occ act_tv exp_kind
                | Just exp_tv <- tcGetTyVar_maybe exp_kind
-               = isNothing (occurCheckExpand exp_tv act_kind)
+               = check_occ exp_tv act_kind
                | otherwise 
                = False
 
+            check_occ tv k = case occurCheckExpand dflags tv k of
+                                OC_Occurs -> True
+                                _bad      -> False
+
             err | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
                 = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
                     <+> ptext (sLit "is unlifted")
index afc575c..f45519b 100644 (file)
@@ -24,6 +24,7 @@ module TcMType (
   newFlexiTyVar,
   newFlexiTyVarTy,             -- Kind -> TcM TcType
   newFlexiTyVarTys,            -- Int -> Kind -> TcM [TcType]
+  newPolyFlexiTyVarTy,
   newMetaKindVar, newMetaKindVars, mkKindSigVar,
   mkTcTyVarName, cloneMetaTyVar, 
 
@@ -318,8 +319,9 @@ newMetaTyVar meta_info kind
   = do { uniq <- newUnique
         ; let name = mkTcTyVarName uniq s
               s = case meta_info of
-                        TauTv -> fsLit "t"
-                        SigTv -> fsLit "a"
+                        PolyTv -> fsLit "s"
+                        TauTv  -> fsLit "t"
+                        SigTv  -> fsLit "a"
         ; details <- newMetaDetails meta_info
        ; return (mkTcTyVar name kind details) }
 
@@ -438,6 +440,10 @@ newFlexiTyVarTy kind = do
 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 
+newPolyFlexiTyVarTy :: TcM TcType
+newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind
+                         ; return (TyVarTy tv) }
+
 tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 -- Instantiate with META type variables
 -- Note that this works for a sequence of kind and type
index aa69d75..73565e0 100644 (file)
@@ -74,7 +74,7 @@ module TcType (
   
   ---------------------------------
   -- Misc type manipulators
-  deNoteType, occurCheckExpand,
+  deNoteType, occurCheckExpand, OccCheckResult(..),
   orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo,
   getDFunTyKey,
   evVarPred_maybe, evVarPred,
@@ -331,6 +331,8 @@ data MetaInfo
                   -- A TauTv is always filled in with a tau-type, which
                   -- never contains any ForAlls 
 
+   | PolyTv        -- Like TauTv, but can unify with a sigma-type
+
    | SigTv        -- A variant of TauTv, except that it should not be
                   -- unified with a type, only with a type variable
                   -- SigTvs are only distinguished to improve error messages
@@ -488,8 +490,9 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_untch = untch })
   = pp_info <> brackets (ppr untch)
   where
     pp_info = case info of
-                TauTv -> ptext (sLit "tau")
-                SigTv -> ptext (sLit "sig")
+                PolyTv -> ptext (sLit "poly")
+                TauTv  -> ptext (sLit "tau")
+                SigTv  -> ptext (sLit "sig")
 
 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
 pprUserTypeCtxt (InfSigCtxt n)    = ptext (sLit "the inferred type for") <+> quotes (ppr n)
@@ -1187,57 +1190,98 @@ even though we could also expand F to get rid of b.
 See also Note [Type synonyms and canonicalization] in TcCanonical
 
 \begin{code}
-occurCheckExpand :: TcTyVar -> Type -> Maybe Type
+data OccCheckResult a
+  = OC_OK a
+  | OC_Forall 
+  | OC_NonTyVar
+  | OC_Occurs
+
+instance Monad OccCheckResult where
+  return x = OC_OK x
+  OC_OK x     >>= k = k x
+  OC_Forall   >>= _ = OC_Forall
+  OC_NonTyVar >>= _ = OC_NonTyVar
+  OC_Occurs   >>= _ = OC_Occurs
+  
+occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
 -- See Note [Occurs check expansion]
--- Check whether the given variable occurs in the given type.  We may
--- have needed to do some type synonym unfolding in order to get rid
--- of the variable, so we also return the unfolded version of the
--- type, which is guaranteed to be syntactically free of the given
--- type variable.  If the type is already syntactically free of the
--- variable, then the same type is returned.
-
-occurCheckExpand tv ty
-  | not (tv `elemVarSet` tyVarsOfType ty) = Just ty
-  | otherwise                             = go ty
+-- Check whether 
+--   a) the given variable occurs in the given type.  
+--   b) there is a forall in the type (unless we have -XImpredicativeTypes
+--                                     or it's a PolyTv
+--   c) if it's a SigTv, ty should be a tyvar
+--
+-- We may have needed to do some type synonym unfolding in order to
+-- get rid of the variable (or forall), so we also return the unfolded
+-- version of the type, which is guaranteed to be syntactically free 
+-- of the given type variable.  If the type is already syntactically 
+-- free of the variable, then the same type is returned.
+
+occurCheckExpand dflags tv ty
+  | MetaTv { mtv_info = SigTv } <- details
+                  = go_sig_tv ty
+  | fast_check ty = return ty
+  | otherwise     = go ty
   where
-    go t@(TyVarTy tv') | tv == tv' = Nothing
-                       | otherwise = Just t
+    details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
+
+    impredicative 
+      = case details of
+          MetaTv { mtv_info = PolyTv } -> True
+          MetaTv { mtv_info = SigTv }  -> False
+          MetaTv { mtv_info = TauTv }  -> xopt Opt_ImpredicativeTypes dflags
+                                       || isOpenTypeKind (tyVarKind tv)
+                                          -- Note [OpenTypeKind accepts foralls]
+                                          -- in TcUnify
+          _other                       -> True
+          -- We can have non-meta tyvars in given constraints
+
+    -- Check 'ty' is a tyvar, or can be expanded into one
+    go_sig_tv ty@(TyVarTy {})            = OC_OK ty
+    go_sig_tv ty | Just ty' <- tcView ty = go_sig_tv ty'
+    go_sig_tv _                          = OC_NonTyVar
+
+    -- True => fine
+    fast_check (LitTy {})        = True
+    fast_check (TyVarTy tv')     = tv /= tv'
+    fast_check (TyConApp _ tys)  = all fast_check tys
+    fast_check (FunTy arg res)   = fast_check arg && fast_check res
+    fast_check (AppTy fun arg)   = fast_check fun && fast_check arg
+    fast_check (ForAllTy tv' ty) = impredicative 
+                                && fast_check (tyVarKind tv')
+                                && (tv == tv' || fast_check ty)
+
+    go t@(TyVarTy tv') | tv == tv' = OC_Occurs
+                       | otherwise = return t
     go ty@(LitTy {}) = return ty
     go (AppTy ty1 ty2) = do { ty1' <- go ty1
                            ; ty2' <- go ty2  
                            ; return (mkAppTy ty1' ty2') }
-    -- mkAppTy <$> go ty1 <*> go ty2
     go (FunTy ty1 ty2) = do { ty1' <- go ty1 
                            ; ty2' <- go ty2 
                            ; return (mkFunTy ty1' ty2') } 
-    -- mkFunTy <$> go ty1 <*> go ty2
-    go ty@(ForAllTy {})
-       | tv `elemVarSet` tyVarsOfTypes tvs_knds = Nothing
+    go ty@(ForAllTy tv' body_ty)
+       | not impredicative                = OC_Forall
+       | not (fast_check (tyVarKind tv')) = OC_Occurs
            -- Can't expand away the kinds unless we create 
            -- fresh variables which we don't want to do at this point.
-       | otherwise = do { rho' <- go rho
-                        ; return (mkForAllTys tvs rho') }
-       where
-         (tvs,rho) = splitForAllTys ty
-         tvs_knds  = map tyVarKind tvs 
+           -- In principle fast_check might fail because of a for-all
+           -- but we don't yet have poly-kinded tyvars so I'm not
+           -- going to worry about that now
+       | tv == tv' = return ty
+       | otherwise = do { body' <- go body_ty
+                        ; return (ForAllTy tv' body') }
 
     -- For a type constructor application, first try expanding away the
     -- offending variable from the arguments.  If that doesn't work, next
     -- see if the type constructor is a type synonym, and if so, expand
     -- it and try again.
     go ty@(TyConApp tc tys)
-{-
-      | isSynFamilyTyCon tc    -- It's ok for tv to occur under a type family application
-       = return ty             -- Eg.  (a ~ F a) is not an occur-check error
-                               -- NB This case can't occur during canonicalisation,
-                               --    because the arg is a Xi-type, but can occur in the
-                               --    call from TcErrors
-      | otherwise
--}
-      = do { tys <- mapM go tys; return (mkTyConApp tc tys) }
-        `firstJust` -- First try to eliminate the tyvar from the args
-        do { ty <- tcView ty; go ty }
-                    -- Failing that, try to expand a synonym
+      = case do { tys <- mapM go tys; return (mkTyConApp tc tys) } of
+          OC_OK ty -> return ty  -- First try to eliminate the tyvar from the args
+          bad | Just ty' <- tcView ty -> go ty'
+              | otherwise             -> bad
+                      -- Failing that, try to expand a synonym
 \end{code}
 
 %************************************************************************
index 999575b..04f1acc 100644 (file)
@@ -160,6 +160,7 @@ matchExpectedFunTys herald arity orig_ty
     defer n_req fun_ty 
       = addErrCtxtM mk_ctxt $
         do { arg_tys <- newFlexiTyVarTys n_req openTypeKind
+                        -- See Note [Foralls to left of arrow]
            ; res_ty  <- newFlexiTyVarTy openTypeKind
            ; co   <- unifyType fun_ty (mkFunTys arg_tys res_ty)
            ; return (co, arg_tys, res_ty) }
@@ -179,6 +180,14 @@ matchExpectedFunTys herald arity orig_ty
             else ptext (sLit "has only") <+> speakN n_args]
 \end{code}
 
+Note [Foralls to left of arrow]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f (x :: forall a. a -> a) = x
+We give 'f' the type (alpha -> beta), and then want to unify
+the alpha with (forall a. a->a).  We want to the arg and result
+of (->) to have openTypeKind, and this also permits foralls, so
+we are ok.
 
 \begin{code}
 ----------------------
@@ -317,15 +326,24 @@ tcSubType origin ctxt ty_actual ty_expected
   = do { (sk_wrap, inst_wrap) 
             <- tcGen ctxt ty_expected $ \ _ sk_rho -> do
             { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
-            ; cow <- unifyType in_rho sk_rho
+            ; cow <- unify in_rho sk_rho
             ; return (coToHsWrapper cow <.> in_wrap) }
        ; return (sk_wrap <.> inst_wrap) }
 
   | otherwise  -- Urgh!  It seems deeply weird to have equality
                -- when actual is not a polytype, and it makes a big 
                -- difference e.g. tcfail104
-  = do { cow <- unifyType ty_actual ty_expected
+  = do { cow <- unify ty_actual ty_expected
        ; return (coToHsWrapper cow) }
+  where
+    -- In the case of patterns we call tcSubType with (expected, actual)
+    -- rather than (actual, expected).   To get error messages the 
+    -- right way round we have to fiddle with the origin
+    unify ty1 ty2 = uType u_origin ty1 ty2
+      where
+         u_origin = case origin of 
+                      PatSigOrigin -> TypeEqOrigin { uo_actual = ty2, uo_expected = ty1 }
+                      _other       -> TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
   
 tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
 tcInfer tc_infer = do { ty  <- newFlexiTyVarTy openTypeKind
@@ -763,8 +781,9 @@ uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
 
 uUnfilledVar origin swapped tv1 details1 non_var_ty2  -- ty2 is not a type variable
   = case details1 of
-      MetaTv { mtv_info = TauTv, mtv_ref = ref1 }
-        -> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2
+      MetaTv { mtv_ref = ref1 }
+        -> do { dflags <- getDynFlags
+              ; mb_ty2' <- checkTauTvUpdate dflags tv1 non_var_ty2
               ; case mb_ty2' of
                   Just ty2' -> updateMeta tv1 ref1 ty2'
                   Nothing   -> do { traceTc "Occ/kind defer" 
@@ -830,9 +849,9 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
         -- type sig
 
 ----------------
-checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
+checkTauTvUpdate :: DynFlags -> TcTyVar -> TcType -> TcM (Maybe TcType)
 --    (checkTauTvUpdate tv ty)
--- We are about to update the TauTv tv with ty.
+-- We are about to update the TauTv/PolyTv tv with ty.
 -- Check (a) that tv doesn't occur in ty (occurs check)
 --       (b) that kind(ty) is a sub-kind of kind(tv)
 -- 
@@ -851,7 +870,11 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 -- we return Nothing, leaving it to the later constraint simplifier to
 -- sort matters out.
 
-checkTauTvUpdate tv ty
+checkTauTvUpdate dflags tv ty
+  | SigTv <- info
+  = ASSERT( not (isTyVarTy ty) )
+    return Nothing
+  | otherwise
   = do { ty1   <- zonkTcType ty
        ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty1)
        ; case sub_k of
@@ -859,12 +882,19 @@ checkTauTvUpdate tv ty
            Just LT           -> return Nothing
            _  | defer_me ty1   -- Quick test
               -> -- Failed quick test so try harder
-                 case occurCheckExpand tv ty1 of 
-                   Nothing -> return Nothing
-                   Just ty2 | defer_me ty2 -> return Nothing
-                            | otherwise    -> return (Just ty2)
+                 case occurCheckExpand dflags tv ty1 of 
+                   OC_OK ty2 | defer_me ty2 -> return Nothing
+                             | otherwise    -> return (Just ty2)
+                   _ -> return Nothing
               | otherwise   -> return (Just ty1) }
   where 
+    info = ASSERT2( isMetaTyVar tv, ppr tv ) metaTyVarInfo tv
+
+    impredicative = xopt Opt_ImpredicativeTypes dflags
+                 || isOpenTypeKind (tyVarKind tv)  
+                       -- Note [OpenTypeKind accepts foralls]
+                 || case info of { PolyTv -> True;  _ -> False }
+
     defer_me :: TcType -> Bool
     -- Checks for (a) occurrence of tv
     --            (b) type family applicatios
@@ -874,9 +904,27 @@ checkTauTvUpdate tv ty
     defer_me (TyConApp tc tys) = isSynFamilyTyCon tc || any defer_me tys
     defer_me (FunTy arg res)   = defer_me arg || defer_me res
     defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
-    defer_me (ForAllTy _ ty)   = defer_me ty
+    defer_me (ForAllTy _ ty)   = not impredicative || defer_me ty
 \end{code}
 
+Note [OpenTypeKind accepts foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is a common paradigm:
+   foo :: (forall a. a -> a) -> Int
+   foo = error "urk"
+To make this work we need to instantiate 'error' with a polytype.
+A similar case is
+   bar :: Bool -> (forall a. a->a) -> Int
+   bar True = \x. (x 3)
+   bar False = error "urk"
+Here we need to instantiate 'error' with a polytype. 
+
+But 'error' has an OpenTypeKind type variable, precisely so that
+we can instantiate it with Int#.  So we also allow such type variables
+to be instantiate with foralls.  It's a bit of a hack, but seems
+straightforward.
+
+
 Note [Conservative unification check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When unifying (tv ~ rhs), w try to avoid creating deferred constraints
@@ -1146,9 +1194,10 @@ uUnboundKVar kv1 non_var_k2
        ; let k2b = defaultKind k2a
                 -- MetaKindVars must be bound only to simple kinds
 
-       ; case occurCheckExpand kv1 k2b of
-           Just k2c -> do { writeMetaTyVar kv1 k2c; return (Just EQ) }
-           _        -> return Nothing }
+       ; dflags <- getDynFlags 
+       ; case occurCheckExpand dflags kv1 k2b of
+           OC_OK k2c -> do { writeMetaTyVar kv1 k2c; return (Just EQ) }
+           _         -> return Nothing }
 
 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
 mkKindErrorCtxt ty1 ty2 k1 k2 env0