Implement full co/contra-variant subsumption checking (fixes Trac #9569)
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 21 Nov 2014 10:58:10 +0000 (10:58 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 21 Nov 2014 11:35:24 +0000 (11:35 +0000)
This is a pretty big patch, but which substantially iproves the subsumption
check.  Trac #9569 was the presenting example, showing how type inference could
depend rather delicately on eta expansion.  But there are other less exotic
examples; see Note [Co/contra-variance of subsumption checking] in TcUnify.

The driving change is to TcUnify.tcSubType.  But also

* HsWrapper gets a new constructor WpFun, which behaves very like CoFun:
       if     wrap1 :: exp_arg <= act_arg
              wrap2 :: act_res <= exp_res
       then   WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)

* I generalised TcExp.tcApp to call tcSubType on the result,
  rather than tcUnifyType.  I think this just makes it consistent
  with everything else, notably tcWrapResult.

As usual I ended up doing some follow-on refactoring

* AmbigOrigin is gone (in favour of TypeEqOrigin)
* Combined BindPatSigCtxt and PatSigCxt into one
* Improved a bit of error message generation

15 files changed:
compiler/deSugar/DsBinds.lhs
compiler/deSugar/Match.lhs
compiler/typecheck/Inst.lhs
compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcEvidence.lhs
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs
compiler/typecheck/TcValidity.lhs

index a3aac1b..bc1b352 100644 (file)
@@ -820,12 +820,17 @@ dsHsWrapper WpHole            e = return e
 dsHsWrapper (WpTyApp ty)      e = return $ App e (Type ty)
 dsHsWrapper (WpLet ev_binds)  e = do bs <- dsTcEvBinds ev_binds
                                      return (mkCoreLets bs e)
-dsHsWrapper (WpCompose c1 c2) e = dsHsWrapper c1 =<< dsHsWrapper c2 e
+dsHsWrapper (WpCompose c1 c2) e = do { e1 <- dsHsWrapper c2 e
+                                     ; dsHsWrapper c1 e1 }
+dsHsWrapper (WpFun c1 c2 t1 _) e = do { x <- newSysLocalDs t1
+                                      ; e1 <- dsHsWrapper c1 (Var x)
+                                      ; e2 <- dsHsWrapper c2 (e `mkCoreAppDs` e1)
+                                      ; return (Lam x e2) }
 dsHsWrapper (WpCast co)       e = ASSERT(tcCoercionRole co == Representational)
                                   dsTcCoercion co (mkCast e)
 dsHsWrapper (WpEvLam ev)      e = return $ Lam ev e
 dsHsWrapper (WpTyLam tv)      e = return $ Lam tv e
-dsHsWrapper (WpEvApp evtrm)   e = liftM (App e) (dsEvTerm evtrm)
+dsHsWrapper (WpEvApp    tm)   e = liftM (App e) (dsEvTerm tm)
 
 --------------------------------------
 dsTcEvBinds :: TcEvBinds -> DsM [CoreBind]
index a140278..ddcd089 100644 (file)
@@ -987,6 +987,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
     --        equating different ways of writing a coercion)
     wrap WpHole WpHole = True
     wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2'
+    wrap (WpFun w1 w2 _ _) (WpFun w1' w2' _ _) = wrap w1 w1' && wrap w2 w2'
     wrap (WpCast co)       (WpCast co')        = co `eq_co` co'
     wrap (WpEvApp et1)     (WpEvApp et2)       = et1 `ev_term` et2
     wrap (WpTyApp t)       (WpTyApp t')        = eqType t t'
index f2aec6f..3fd8e64 100644 (file)
@@ -23,8 +23,6 @@ module Inst (
        -- Simple functions over evidence variables
        tyVarsOfWC, tyVarsOfBag,
        tyVarsOfCt, tyVarsOfCts,
-
-       tidyEvVar, tidyCt, tidySkolemInfo
     ) where
 
 #include "HsVersions.h"
@@ -49,7 +47,7 @@ import Class( Class )
 import MkId( mkDictFunId )
 import Id
 import Name
-import Var      ( EvVar, varType, setVarType )
+import Var      ( EvVar )
 import VarEnv
 import VarSet
 import PrelNames
@@ -59,7 +57,6 @@ import Bag
 import Util
 import Outputable
 import Control.Monad( unless )
-import Data.List( mapAccumL )
 import Data.Maybe( isJust )
 \end{code}
 
@@ -175,10 +172,11 @@ deeplyInstantiate orig ty
        ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
        ; let theta' = substTheta subst theta
        ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
-       ; traceTc "Instantiating (deply)" (vcat [ ppr ty
-                                               , text "with" <+> ppr tvs'
-                                               , text "args:" <+> ppr ids1
-                                               , text "theta:" <+>  ppr theta' ])
+       ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig
+                                                , text "type" <+> ppr ty
+                                                , text "with" <+> ppr tvs'
+                                                , text "args:" <+> ppr ids1
+                                                , text "theta:" <+>  ppr theta' ])
        ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
        ; return (mkWpLams ids1
                     <.> wrap2
index b44762e..00f9f62 100644 (file)
@@ -669,7 +669,7 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
         -- See Note [Impedence matching]
         ; (wrap, wanted) <- addErrCtxtM (mk_bind_msg inferred True poly_name (idType poly_id)) $
                             captureConstraints $
-                            tcSubType origin sig_ctxt sel_poly_ty (idType poly_id)
+                            tcSubType_NC sig_ctxt sel_poly_ty (idType poly_id)
         ; ev_binds <- simplifyTop wanted
 
         ; return (ABE { abe_wrap = mkWpLet (EvBinds ev_binds) <.> wrap
@@ -679,7 +679,6 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
   where
     inferred = isNothing mb_sig
     prag_sigs = prag_fn poly_name
-    origin    = AmbigOrigin sig_ctxt
     sig_ctxt  = InfSigCtxt poly_name
 
 mkInferredPolyId :: Name -> [TyVar] -> TcThetaType -> TcType -> TcM Id
@@ -705,20 +704,21 @@ mkInferredPolyId poly_name qtvs theta mono_ty
 
        ; addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
          checkValidType (InfSigCtxt poly_name) inferred_poly_ty
+
        ; return (mkLocalId poly_name inferred_poly_ty) }
 
 mk_bind_msg :: Bool -> Bool -> Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
 mk_bind_msg inferred want_ambig poly_name poly_ty tidy_env
- = return (tidy_env', msg)
+ = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env poly_ty
+      ; return (tidy_env', mk_msg tidy_ty) }
  where
-   msg = vcat [ ptext (sLit "When checking that") <+> quotes (ppr poly_name)
-                <+> ptext (sLit "has the") <+> what <+> ptext (sLit "type")
-              , nest 2 (ppr poly_name <+> dcolon <+> ppr tidy_ty)
-              , ppWhen want_ambig $
-                ptext (sLit "Probable cause: the inferred type is ambiguous") ]
+   mk_msg ty = vcat [ ptext (sLit "When checking that") <+> quotes (ppr poly_name)
+                      <+> ptext (sLit "has the") <+> what <+> ptext (sLit "type")
+                    , nest 2 (ppr poly_name <+> dcolon <+> ppr ty)
+                    , ppWhen want_ambig $
+                      ptext (sLit "Probable cause: the inferred type is ambiguous") ]
    what | inferred  = ptext (sLit "inferred")
         | otherwise = ptext (sLit "specified")
-   (tidy_env', tidy_ty) = tidyOpenType tidy_env poly_ty
 \end{code}
 
 Note [Validity of inferred types]
@@ -846,12 +846,11 @@ tcSpec poly_id prag@(SpecSig fun_name hs_ty inl)
                  (ptext (sLit "SPECIALISE pragma for non-overloaded function")
                   <+> quotes (ppr fun_name))
                   -- Note [SPECIALISE pragmas]
-        ; wrap <- tcSubType origin sig_ctxt (idType poly_id) spec_ty
+        ; wrap <- tcSubType sig_ctxt (idType poly_id) spec_ty
         ; return (SpecPrag poly_id wrap inl) }
   where
     name      = idName poly_id
     poly_ty   = idType poly_id
-    origin    = SpecPragOrigin name
     sig_ctxt  = FunSigCtxt name
     spec_ctxt prag = hang (ptext (sLit "In the SPECIALISE pragma")) 2 (ppr prag)
 
@@ -1326,7 +1325,7 @@ tcTySig (L loc (PatSynSig (L _ name) (_, qtvs) prov req ty))
 
        ; qtvs' <- mapM zonkQuantifiedTyVar qtvs'
 
-       ; let (_, pat_ty) = splitFunTys ty'
+       ; let (_, pat_ty) = tcSplitFunTys ty'
              univ_set = tyVarsOfType pat_ty
              (univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs'
 
index a1cbbd6..84a2c16 100644 (file)
@@ -1066,8 +1066,8 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell))
 
     -- Report "potential instances" only when the constraint arises
     -- directly from the user's use of an overloaded function
-    want_potential (AmbigOrigin {})   = False
-    want_potential _                  = True
+    want_potential (TypeEqOrigin {}) = False
+    want_potential _                 = True
 
     add_to_ctxt_fixes has_ambig_tvs
       | not has_ambig_tvs && all_tyvars
index 3b2a3d6..83f6596 100644 (file)
@@ -10,7 +10,7 @@ module TcEvidence (
   -- HsWrapper
   HsWrapper(..),
   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCast,
-  idHsWrapper, isIdHsWrapper, pprHsWrapper,
+  mkWpFun, idHsWrapper, isIdHsWrapper, pprHsWrapper,
 
   -- Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
@@ -142,6 +142,9 @@ mkTcReflCo = TcRefl
 mkTcNomReflCo :: TcType -> TcCoercion
 mkTcNomReflCo = TcRefl Nominal
 
+mkTcRepReflCo :: TcType -> TcCoercion
+mkTcRepReflCo = TcRefl Representational
+
 mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
 mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
 
@@ -441,14 +444,22 @@ data HsWrapper
        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
 
+  | WpFun HsWrapper HsWrapper TcType TcType
+       -- (WpFun wrap1 wrap2 t1 t2)[e] = \(x:t1). wrap2[ e wrap1[x] ] :: t2
+       -- So note that if  wrap1 :: exp_arg <= act_arg
+       --                  wrap2 :: act_res <= exp_res
+       --           then   WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
+       -- This isn't the same as for mkTcFunCo, but it has to be this way
+       -- because we can't use 'sym' to flip around these HsWrappers
+
   | WpCast TcCoercion         -- A cast:  [] `cast` co
                               -- Guaranteed not the identity coercion
                               -- At role Representational
 
         -- Evidence abstraction and application
         -- (both dictionaries and coercions)
-  | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
-  | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
+  | WpEvLam  EvVar               -- \d. []       the 'd' is an evidence variable
+  | WpEvApp  EvTerm              -- [] d         the 'd' is evidence for a constraint
 
         -- Kind and Type abstraction and application
   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
@@ -465,9 +476,18 @@ WpHole <.> c = c
 c <.> WpHole = c
 c1 <.> c2    = c1 `WpCompose` c2
 
+mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper
+mkWpFun WpHole       WpHole       _  _  = WpHole 
+mkWpFun WpHole       (WpCast co2) t1 _  = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
+mkWpFun (WpCast co1) WpHole       _  t2 = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
+mkWpFun (WpCast co1) (WpCast co2) _  _  = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
+mkWpFun co1          co2          t1 t2 = WpFun co1 co2 t1 t2
+
 mkWpCast :: TcCoercion -> HsWrapper
-mkWpCast co = ASSERT2(tcCoercionRole co == Representational, ppr co)
-              WpCast co
+mkWpCast co 
+  | isTcReflCo co = WpHole
+  | otherwise     = ASSERT2(tcCoercionRole co == Representational, ppr co)
+                    WpCast co
 
 mkWpTyApps :: [Type] -> HsWrapper
 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
@@ -746,13 +766,15 @@ pprHsWrapper doc wrap
     -- False <=> appears as body of let or lambda
     help it WpHole             = it
     help it (WpCompose f1 f2)  = help (help it f2) f1
+    help it (WpFun f1 f2 t1 _) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+> 
+                                              help (\_ -> it True <+> help (\_ -> ptext (sLit "x")) f1 True) f2 False
     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
                                               <+> pprParendTcCo co)]
-    help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
-    help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
-    help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
-    help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
-    help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
+    help it (WpEvApp id)    = no_parens  $ sep [it True, nest 2 (ppr id)]
+    help it (WpTyApp ty)    = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
+    help it (WpEvLam id)    = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
+    help it (WpTyLam tv)    = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
+    help it (WpLet binds)   = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
 
     pp_bndr v = pprBndr LambdaBind v <> dot
 
index 05a53d6..1a2deba 100644 (file)
@@ -914,15 +914,17 @@ tcApp fun args res_ty
         -- Typecheck the result, thereby propagating
         -- info (if any) from result into the argument types
         -- Both actual_res_ty and res_ty are deeply skolemised
-        ; co_res <- addErrCtxtM (funResCtxt True (unLoc fun) actual_res_ty res_ty) $
-                    unifyType actual_res_ty res_ty
+        -- Rather like tcWrapResult, but (perhaps for historical reasons)
+        -- we do this before typechecking the arguments
+        ; wrap_res <- addErrCtxtM (funResCtxt True (unLoc fun) actual_res_ty res_ty) $
+                      tcSubTypeDS_NC GenSigCtxt actual_res_ty res_ty
 
         -- Typecheck the arguments
         ; args1 <- tcArgs fun args expected_arg_tys
 
         -- Assemble the result
         ; let fun2 = mkLHsWrapCo co_fun fun1
-              app  = mkLHsWrapCo co_res (foldl mkHsApp fun2 args1)
+              app  = mkLHsWrap wrap_res (foldl mkHsApp fun2 args1)
 
         ; return (unLoc app) }
 
index 27d2648..d5dfd8e 100644 (file)
@@ -838,6 +838,11 @@ zonkCoFn env WpHole   = return (env, WpHole)
 zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                     ; (env2, c2') <- zonkCoFn env1 c2
                                     ; return (env2, WpCompose c1' c2') }
+zonkCoFn env (WpFun c1 c2 t1 t2) = do { (env1, c1') <- zonkCoFn env c1
+                                      ; (env2, c2') <- zonkCoFn env1 c2
+                                      ; t1'         <- zonkTcTypeToType env2 t1
+                                      ; t2'         <- zonkTcTypeToType env2 t2
+                                      ; return (env2, WpFun c1' c2' t1' t2') }
 zonkCoFn env (WpCast co) = do { co' <- zonkTcCoToCo env co
                               ; return (env, WpCast co') }
 zonkCoFn env (WpEvLam ev)   = do { (env', ev') <- zonkEvBndrX env ev
index d6f237f..722d162 100644 (file)
@@ -161,7 +161,7 @@ tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
   --     HsForAllTy in hs_ty occur *first* in the returned type.
   --     See Note [Scoped] with TcSigInfo
 tcHsSigType ctxt hs_ty
-  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
+  = addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
     tcHsSigTypeNC ctxt hs_ty
 
 tcHsSigTypeNC ctxt (L loc hs_ty)
@@ -1240,7 +1240,7 @@ tcHsPatSigType :: UserTypeCtxt
 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
 
 tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig_tvs })
-  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
+  = addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
     do  { kvs <- mapM new_kv sig_kvs
         ; tvs <- mapM new_tv sig_tvs
         ; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
@@ -1259,7 +1259,7 @@ tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig
           RuleSigCtxt {} -> return (mkTcTyVar name kind (SkolemTv False))
           _              -> newSigTyVar name kind  -- See Note [Unifying SigTvs]
 
-tcPatSig :: UserTypeCtxt
+tcPatSig :: Bool                    -- True <=> pattern binding
          -> HsWithBndrs Name (LHsType Name)
          -> TcSigmaType
          -> TcM (TcType,            -- The type to use for "inside" the signature
@@ -1267,15 +1267,16 @@ tcPatSig :: UserTypeCtxt
                                     -- the scoped type variables
                  HsWrapper)         -- Coercion due to unification with actual ty
                                     -- Of shape:  res_ty ~ sig_ty
-tcPatSig ctxt sig res_ty
-  = do  { (sig_ty, sig_tvs) <- tcHsPatSigType ctxt sig
+tcPatSig in_pat_bind sig res_ty
+  = do  { (sig_ty, sig_tvs) <- tcHsPatSigType PatSigCtxt sig
         -- sig_tvs are the type variables free in 'sig',
         -- and not already in scope. These are the ones
         -- that should be brought into scope
 
         ; if null sig_tvs then do {
                 -- Just do the subsumption check and return
-                  wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
+                  wrap <- addErrCtxtM (mk_msg sig_ty) $
+                          tcSubType_NC PatSigCtxt res_ty sig_ty
                 ; return (sig_ty, [], wrap)
         } else do
                 -- Type signature binds at least one scoped type variable
@@ -1283,10 +1284,7 @@ tcPatSig ctxt sig res_ty
                 -- A pattern binding cannot bind scoped type variables
                 -- It is more convenient to make the test here
                 -- than in the renamer
-        { let in_pat_bind = case ctxt of
-                                BindPatSigCtxt -> True
-                                _              -> False
-        ; when in_pat_bind (addErr (patBindSigErr sig_tvs))
+        { when in_pat_bind (addErr (patBindSigErr sig_tvs))
 
                 -- Check that all newly-in-scope tyvars are in fact
                 -- constrained by the pattern.  This catches tiresome
@@ -1300,11 +1298,21 @@ tcPatSig ctxt sig res_ty
         ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
 
         -- Now do a subsumption check of the pattern signature against res_ty
-        ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
+        ; wrap <- addErrCtxtM (mk_msg sig_ty) $
+                  tcSubType_NC PatSigCtxt res_ty sig_ty
 
         -- Phew!
         ; return (sig_ty, sig_tvs, wrap)
         } }
+  where
+    mk_msg sig_ty tidy_env
+       = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
+            ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
+            ; let msg = vcat [ hang (ptext (sLit "When checking that the pattern signature:"))
+                                  4 (ppr sig_ty)
+                             , nest 2 (hang (ptext (sLit "fits the type of its context:"))
+                                          2 (ppr res_ty)) ]
+            ; return (tidy_env, msg) }
 
 patBindSigErr :: [(Name, TcTyVar)] -> SDoc
 patBindSigErr sig_tvs
@@ -1628,17 +1636,6 @@ promotionErr name err
 %************************************************************************
 
 \begin{code}
-pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon,
-                                 nest 2 (pp_sig ctxt) ]
-  where
-    pp_sig (FunSigCtxt n)  = pp_n_colon n
-    pp_sig (ConArgCtxt n)  = pp_n_colon n
-    pp_sig (ForSigCtxt n)  = pp_n_colon n
-    pp_sig _               = ppr (unLoc hs_ty)
-
-    pp_n_colon n = pprPrefixOcc n <+> dcolon <+> ppr (unLoc hs_ty)
-
 badPatSigTvs :: TcType -> [TyVar] -> SDoc
 badPatSigTvs sig_ty bad_tvs
   = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
index 3a6cca0..215aa2d 100644 (file)
@@ -1141,12 +1141,10 @@ Note that
 tcSpecInst :: Id -> Sig Name -> TcM TcSpecPrag
 tcSpecInst dfun_id prag@(SpecInstSig hs_ty)
   = addErrCtxt (spec_ctxt prag) $
-    do  { let name = idName dfun_id
-        ; (tyvars, theta, clas, tys) <- tcHsInstHead SpecInstCtxt hs_ty
+    do  { (tyvars, theta, clas, tys) <- tcHsInstHead SpecInstCtxt hs_ty
         ; let (_, spec_dfun_ty) = mkDictFunTy tyvars theta clas tys
 
-        ; co_fn <- tcSubType (SpecPragOrigin name) SpecInstCtxt
-                             (idType dfun_id) spec_dfun_ty
+        ; co_fn <- tcSubType SpecInstCtxt (idType dfun_id) spec_dfun_ty
         ; return (SpecPrag dfun_id co_fn defaultInlinePragma) }
   where
     spec_ctxt prag = hang (ptext (sLit "In the SPECIALISE pragma")) 2 (ppr prag)
index b18ab7e..cfa995d 100644 (file)
@@ -129,9 +129,9 @@ data LetBndrSpec
 makeLazy :: PatEnv -> PatEnv
 makeLazy penv = penv { pe_lazy = True }
 
-patSigCtxt :: PatEnv -> UserTypeCtxt
-patSigCtxt (PE { pe_ctxt = LetPat {} }) = BindPatSigCtxt
-patSigCtxt (PE { pe_ctxt = LamPat {} }) = LamPatSigCtxt
+inPatBind :: PatEnv -> Bool
+inPatBind (PE { pe_ctxt = LetPat {} }) = True
+inPatBind (PE { pe_ctxt = LamPat {} }) = False
 
 ---------------
 type TcPragFun = Name -> [LSig Name]
@@ -505,7 +505,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
 -- Type signatures in patterns
 -- See Note [Pattern coercions] below
 tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
-  = do  { (inner_ty, tv_binds, wrap) <- tcPatSig (patSigCtxt penv) sig_ty pat_ty
+  = do  { (inner_ty, tv_binds, wrap) <- tcPatSig (inPatBind penv) sig_ty pat_ty
         ; (pat', res) <- tcExtendTyVarEnv2 tv_binds $
                          tc_lpat pat inner_ty penv thing_inside
 
index 6f00b86..9ec9395 100644 (file)
@@ -1861,7 +1861,6 @@ data CtOrigin
   | PArrSeqOrigin  (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
   | SectionOrigin
   | TupleOrigin                        -- (..,..)
-  | AmbigOrigin UserTypeCtxt    -- Will be FunSigCtxt, InstDeclCtxt, or SpecInstCtxt
   | ExprSigOrigin       -- e :: ty
   | PatSigOrigin        -- p :: ty
   | PatOrigin           -- Instantiating a polytyped pattern at a constructor
@@ -1930,13 +1929,6 @@ pprCtOrigin (DerivOriginDC dc n)
   where
     ty = dataConOrigArgTys dc !! (n-1)
 
-pprCtOrigin (AmbigOrigin ctxt)
-  = ctoHerald <+> ptext (sLit "the ambiguity check for")
-    <+> case ctxt of
-           FunSigCtxt name -> quotes (ppr name)
-           InfSigCtxt name -> quotes (ppr name)
-           _               -> pprUserTypeCtxt ctxt
-
 pprCtOrigin (DerivOriginCoerce meth ty1 ty2)
   = hang (ctoHerald <+> ptext (sLit "the coercion of the method") <+> quotes (ppr meth))
        2 (sep [ ptext (sLit "from type") <+> quotes (ppr ty1)
index 74406c0..a9b44ab 100644 (file)
@@ -29,7 +29,7 @@ module TcType (
 
   --------------------------------
   -- MetaDetails
-  UserTypeCtxt(..), pprUserTypeCtxt,
+  UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt,
   TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
   MetaDetails(Flexi, Indirect), MetaInfo(..),
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
@@ -63,7 +63,7 @@ module TcType (
   -- Again, newtypes are opaque
   eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
   pickyEqType, tcEqType, tcEqKind,
-  isSigmaTy, isOverloadedTy,
+  isSigmaTy, isRhoTy, isOverloadedTy,
   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
@@ -232,12 +232,20 @@ type TcType = Type      -- A TcType can have mutable type variables
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
 type TcSigmaType    = TcType
-type TcRhoType      = TcType
+type TcRhoType      = TcType  -- Note [TcRhoType]
 type TcTauType      = TcType
 type TcKind         = Kind
 type TcTyVarSet     = TyVarSet
 \end{code}
 
+Note [TcRhoType]
+~~~~~~~~~~~~~~~~
+A TcRhoType has no foralls or contexts at the top, or to the right of an arrow
+  YES    (forall a. a->a) -> Int
+  NO     forall a. a ->  Int
+  NO     Eq a => a -> a
+  NO     Int -> forall a. a -> Int
+
 
 %************************************************************************
 %*                                                                      *
@@ -361,10 +369,9 @@ data UserTypeCtxt
   | ExprSigCtxt         -- Expression type signature
   | ConArgCtxt Name     -- Data constructor argument
   | TySynCtxt Name      -- RHS of a type synonym decl
-  | LamPatSigCtxt               -- Type sig in lambda pattern
-                        --      f (x::t) = ...
-  | BindPatSigCtxt      -- Type sig in pattern binding pattern
-                        --      (x::t, y) = e
+  | PatSigCtxt          -- Type sig in pattern
+                        --   eg  f (x::t) = ...
+                        --   or  (x::t, y) = e
   | RuleSigCtxt Name    -- LHS of a RULE forall
                         --    RULE "foo" forall (x :: a -> a). f (Just x) = ...
   | ResSigCtxt          -- Result type sig
@@ -511,7 +518,7 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_untch = untch })
   = pp_info <> colon <> ppr untch
   where
     pp_info = case info of
-                ReturnTv   -> ptext (sLit "return")
+                ReturnTv   -> ptext (sLit "ret")
                 TauTv      -> ptext (sLit "tau")
                 SigTv      -> ptext (sLit "sig")
                 FlatMetaTv -> ptext (sLit "fuv")
@@ -524,8 +531,7 @@ pprUserTypeCtxt ExprSigCtxt       = ptext (sLit "an expression type signature")
 pprUserTypeCtxt (ConArgCtxt c)    = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
 pprUserTypeCtxt (TySynCtxt c)     = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
 pprUserTypeCtxt ThBrackCtxt       = ptext (sLit "a Template Haskell quotation [t|...|]")
-pprUserTypeCtxt LamPatSigCtxt     = ptext (sLit "a pattern type signature")
-pprUserTypeCtxt BindPatSigCtxt    = ptext (sLit "a pattern type signature")
+pprUserTypeCtxt PatSigCtxt        = ptext (sLit "a pattern type signature")
 pprUserTypeCtxt ResSigCtxt        = ptext (sLit "a result type signature")
 pprUserTypeCtxt (ForSigCtxt n)    = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
 pprUserTypeCtxt DefaultDeclCtxt   = ptext (sLit "a type in a `default' declaration")
@@ -536,6 +542,22 @@ pprUserTypeCtxt GhciCtxt          = ptext (sLit "a type in a GHCi command")
 pprUserTypeCtxt (ClassSCCtxt c)   = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
 pprUserTypeCtxt SigmaCtxt         = ptext (sLit "the context of a polymorphic type")
 pprUserTypeCtxt (DataTyCtxt tc)   = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
+
+pprSigCtxt :: UserTypeCtxt -> SDoc -> SDoc -> SDoc
+-- (pprSigCtxt ctxt <extra> <type>)
+-- prints    In <extra> the type signature for 'f':
+--              f :: <type>
+-- The <extra> is either empty or "the ambiguity check for"
+pprSigCtxt ctxt extra pp_ty
+  = sep [ ptext (sLit "In") <+> extra <+> pprUserTypeCtxt ctxt <> colon
+        , nest 2 (pp_sig ctxt) ]
+  where
+    pp_sig (FunSigCtxt n)  = pp_n_colon n
+    pp_sig (ConArgCtxt n)  = pp_n_colon n
+    pp_sig (ForSigCtxt n)  = pp_n_colon n
+    pp_sig _               = pp_ty
+
+    pp_n_colon n = pprPrefixOcc n <+> dcolon <+> pp_ty
 \end{code}
 
 
@@ -1310,17 +1332,23 @@ immSuperClasses cls tys
 %*                                                                      *
 %************************************************************************
 
-isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have
-any foralls.  E.g.
-        f :: (?x::Int) => Int -> Int
 
 \begin{code}
-isSigmaTy :: Type -> Bool
+isSigmaTy :: TcType -> Bool
+-- isSigmaTy returns true of any qualified type.  It doesn't
+-- *necessarily* have any foralls.  E.g
+--        f :: (?x::Int) => Int -> Int
 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
 isSigmaTy (ForAllTy _ _) = True
 isSigmaTy (FunTy a _)    = isPredTy a
 isSigmaTy _              = False
 
+isRhoTy :: TcType -> Bool   -- True of TcRhoTypes; see Note [TcRhoType]
+isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
+isRhoTy (ForAllTy {}) = False
+isRhoTy (FunTy a r)   = not (isPredTy a) && isRhoTy r
+isRhoTy _             = True
+
 isOverloadedTy :: Type -> Bool
 -- Yes for a type of a function that might require evidence-passing
 -- Used only by bindLocalMethods
index f103fd7..eb39038 100644 (file)
@@ -10,7 +10,8 @@ Type subsumption and unification
 
 module TcUnify (
   -- Full-blown subsumption
-  tcWrapResult, tcSubType, tcGen,
+  tcWrapResult, tcGen,
+  tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC,
   checkConstraints, newImplication,
 
   -- Various unifications
@@ -161,11 +162,10 @@ matchExpectedFunTys herald arity orig_ty
 
     ------------
     mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
-    mk_ctxt env = do { orig_ty1 <- zonkTcType orig_ty
-                     ; let (env', orig_ty2) = tidyOpenType env orig_ty1
-                           (args, _) = tcSplitFunTys orig_ty2
+    mk_ctxt env = do { (env', orig_ty) <- zonkTidyTcType env orig_ty
+                     ; let (args, _) = tcSplitFunTys orig_ty
                            n_actual = length args
-                     ; return (env', mk_msg orig_ty2 n_actual) }
+                     ; return (env', mk_msg orig_ty n_actual) }
 
     mk_msg ty n_args
       = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
@@ -198,7 +198,7 @@ matchExpectedPArrTy exp_ty
   = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
        ; return (co, elt_ty) }
 
-----------------------
+---------------------
 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
                       -> TcRhoType            -- orig_ty
                       -> TcM (TcCoercion,     -- T k1 k2 k3 a b c ~ orig_ty
@@ -297,74 +297,175 @@ matchExpectedAppTy orig_ty
 %*                                                                      *
 %************************************************************************
 
-All the tcSub calls have the form
-                tcSub actual_ty expected_ty
+Note [Subsumption checking: tcSubType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+All the tcSubType calls have the form
+                tcSubType actual_ty expected_ty
 which checks
                 actual_ty <= expected_ty
 
 That is, that a value of type actual_ty is acceptable in
-a place expecting a value of type expected_ty.
+a place expecting a value of type expected_ty.  I.e. that
+
+    actual ty   is more polymorphic than   expected_ty
 
 It returns a coercion function
         co_fn :: actual_ty ~ expected_ty
 which takes an HsExpr of type actual_ty into one of type
 expected_ty.
 
+There are a number of wrinkles (below).
+
+Notice that Wrinkle 1 and 2 both require eta-expansion, which technically
+may increase termination.  We just put up with this, in exchange for getting
+more predicatble type inference.
+
+Wrinkle 1: Note [Deep skolemisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want   (forall a. Int -> a -> a)  <=  (Int -> forall a. a->a)
+(see section 4.6 of "Practical type inference for higher rank types")
+So we must deeply-skolemise the RHS before we instantiate the LHS.
+
+That is why tc_sub_type starts with a call to tcGen (which does the
+deep skolemisation), and then calls the DS variant (which assumes
+that expected_ty is deeply skolemised)
+
+Wrinkle 2: Note [Co/contra-variance of subsumption checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider  g :: (Int -> Int) -> Int
+  f1 :: (forall a. a -> a) -> Int
+  f1 = g
+
+  f2 :: (forall a. a -> a) -> Int
+  f2 x = g x
+f2 will typecheck, and it would be odd/fragile if f1 did not.
+But f1 will only typecheck if we have that
+    (Int->Int) -> Int  <=  (forall a. a->a) -> Int
+And that is only true if we do the full co/contravariant thing
+in the subsumption check.  That happens in the FunTy case of
+tc_sub_type_ds, and is the sole reason for the WpFun form of
+HsWrapper.
+
+Another powerful reason for doing this co/contra stuff is visible
+in Trac #9569, involving instantiation of constraint variables,
+and again involving eta-expansion.
+
+Wrinkle 3: Note [Higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider tc150:
+  f y = \ (x::forall a. a->a). blah
+The following happens:
+* We will infer the type of the RHS, ie with a res_ty = alpha.
+* Then the lambda will split  alpha := beta -> gamma.
+* And then we'll check tcSubType IsSwapped beta (forall a. a->a)
+
+So it's important that we unify beta := forall a. a->a, rather than
+skolemising the type.
+
+
 \begin{code}
-tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
--- Check that ty_actual is more polymorphic than ty_expected
--- Both arguments might be polytypes, so we must instantiate and skolemise
--- Returns a wrapper of shape   ty_actual ~ ty_expected
-tcSubType origin ctxt ty_actual ty_expected
-  | isSigmaTy ty_actual
-  = do { (sk_wrap, inst_wrap)
-            <- tcGen ctxt ty_expected $ \ _ sk_rho -> do
-            { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
-            ; 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 <- unify ty_actual ty_expected
-       ; return (coToHsWrapper cow) }
+tcSubType :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- Checks that actual <= expected
+-- Returns HsWrapper :: actual ~ expected
+tcSubType ctxt ty_actual ty_expected
+  = addSubTypeCtxt ty_actual ty_expected $
+    tcSubType_NC ctxt ty_actual ty_expected
+
+tcSubTypeDS :: UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
+-- Just like tcSubType, but with the additional precondition that
+-- ty_expected is deeply skolemised (hence "DS")
+tcSubTypeDS ctxt ty_actual ty_expected
+  = addSubTypeCtxt ty_actual ty_expected $
+    tcSubTypeDS_NC ctxt ty_actual ty_expected
+
+
+addSubTypeCtxt :: TcType -> TcType -> TcM a -> TcM a
+addSubTypeCtxt ty_actual ty_expected thing_inside
+ | isRhoTy ty_actual     -- If there is no polymorphism involved, the
+ , isRhoTy ty_expected   -- TypeEqOrigin stuff (added by the _NC functions)
+ = thing_inside          -- gives enough context by itself
+ | otherwise
+ = addErrCtxtM mk_msg thing_inside
   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 }
+    mk_msg tidy_env
+      = do { (tidy_env, ty_actual)   <- zonkTidyTcType tidy_env ty_actual
+           ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
+           ; let msg = vcat [ hang (ptext (sLit "When checking that:"))
+                                 4 (ppr ty_actual)
+                            , nest 2 (hang (ptext (sLit "is more polymorphic than:"))
+                                         2 (ppr ty_expected)) ]
+           ; return (tidy_env, msg) }
 
--- | Infer a type using a type "checking" function by passing in a ReturnTv,
--- which can unify with *anything*. See also Note [ReturnTv] in TcType
-tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_check
-  = do { tv  <- newReturnTyVar openTypeKind
-       ; let ty = mkTyVarTy tv
-       ; res <- tc_check ty
-       ; whenM (isUnfilledMetaTyVar tv) $  -- checking was uninformative
-         do { traceTc "Defaulting an un-filled ReturnTv to a TauTv" empty
-            ; tau_ty <- newFlexiTyVarTy openTypeKind
-            ; writeMetaTyVar tv tau_ty }
-       ; return (res, ty) }
+---------------
+-- The "_NC" variants do not add a typechecker-error context;
+-- the caller is assumed to do that
+
+tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+tcSubType_NC ctxt ty_actual ty_expected
+  = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
+       ; tc_sub_type origin ctxt ty_actual ty_expected }
+  where
+    origin = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty_expected }
+
+tcSubTypeDS_NC :: UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
+tcSubTypeDS_NC ctxt ty_actual ty_expected
+  = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
+       ; tc_sub_type_ds origin ctxt ty_actual ty_expected }
   where
+    origin = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty_expected }
+
+---------------
+tc_sub_type :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+tc_sub_type origin ctxt ty_actual ty_expected
+  | isTyVarTy ty_actual  -- See Note [Higher rank types]
+  = do { cow <- uType origin ty_actual ty_expected
+       ; return (coToHsWrapper cow) }
+
+  | otherwise  -- See Note [Deep skolemisation]
+  = do { (sk_wrap, inner_wrap) <- tcGen ctxt ty_expected $ \ _ sk_rho ->
+                                  tc_sub_type_ds origin ctxt ty_actual sk_rho
+       ; return (sk_wrap <.> inner_wrap) }
+
+---------------
+tc_sub_type_ds :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
+-- Just like tcSubType, but with the additional precondition that
+-- ty_expected is deeply skolemised
+tc_sub_type_ds origin ctxt ty_actual ty_expected
+  | Just (act_arg, act_res) <- tcSplitFunTy_maybe ty_actual
+  , Just (exp_arg, exp_res) <- tcSplitFunTy_maybe ty_expected
+  = -- See Note [Co/contra-variance of subsumption checking]
+    do { res_wrap <- tc_sub_type_ds origin ctxt act_res exp_res
+       ; arg_wrap <- tc_sub_type    origin ctxt exp_arg act_arg
+       ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
+           -- arg_wrap :: exp_arg ~ act_arg
+           -- res_wrap :: act-res ~ exp_res
+
+  | (tvs, theta, in_rho) <- tcSplitSigmaTy ty_actual
+  , not (null tvs && null theta)
+  = do { (subst, tvs') <- tcInstTyVars tvs
+       ; let tys'    = mkTyVarTys tvs'
+             theta'  = substTheta subst theta
+             in_rho' = substTy subst in_rho
+       ; in_wrap   <- instCall origin tys' theta'
+       ; body_wrap <- tcSubTypeDS_NC ctxt in_rho' ty_expected
+       ; return (body_wrap <.> in_wrap) }
+
+  | otherwise   -- Revert to unification
+  = do { cow <- uType origin ty_actual ty_expected
+       ; return (coToHsWrapper cow) }
 
 -----------------
 tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId)
 tcWrapResult expr actual_ty res_ty
-  = do { cow <- unifyType actual_ty res_ty
+  = do { cow <- tcSubTypeDS GenSigCtxt actual_ty res_ty
                 -- Both types are deeply skolemised
-       ; return (mkHsWrapCo cow expr) }
+       ; return (mkHsWrap cow expr) }
 
 -----------------------------------
 wrapFunResCoercion
-        :: [TcType]     -- Type of args
-        -> HsWrapper    -- HsExpr a -> HsExpr b
-        -> TcM HsWrapper        -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
+        :: [TcType]        -- Type of args
+        -> HsWrapper       -- HsExpr a -> HsExpr b
+        -> TcM HsWrapper   -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
 wrapFunResCoercion arg_tys co_fn_res
   | isIdHsWrapper co_fn_res
   = return idHsWrapper
@@ -373,8 +474,24 @@ wrapFunResCoercion arg_tys co_fn_res
   | otherwise
   = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
         ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
-\end{code}
 
+-----------------------------------
+-- | Infer a type using a type "checking" function by passing in a ReturnTv,
+-- which can unify with *anything*. See also Note [ReturnTv] in TcType
+tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
+tcInfer tc_check
+  = do { ret_tv  <- newReturnTyVar openTypeKind
+       ; res <- tc_check (mkTyVarTy ret_tv)
+       ; details <- readMetaTyVar ret_tv
+       ; res_ty <- case details of
+            Indirect ty -> return ty
+            Flexi ->    -- Checking was uninformative
+                     do { traceTc "Defaulting un-filled ReturnTv to a TauTv" (ppr ret_tv)
+                        ; tau_ty <- newFlexiTyVarTy openTypeKind
+                        ; writeMetaTyVar ret_tv tau_ty
+                        ; return tau_ty }
+       ; return (res, res_ty) }
+\end{code}
 
 
 %************************************************************************
index 97d62d1..123f030 100644 (file)
@@ -19,7 +19,7 @@ module TcValidity (
 #include "HsVersions.h"
 
 -- friends:
-import TcUnify    ( tcSubType )
+import TcUnify    ( tcSubType_NC )
 import TcSimplify ( simplifyAmbiguityCheck )
 import TypeRep
 import TcType
@@ -89,18 +89,17 @@ checkAmbiguity ctxt ty
          -- tyvars are skolemised, we can safely use tcSimplifyTop
        ; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $
                             captureConstraints $
-                            tcSubType (AmbigOrigin ctxt) ctxt ty' ty'
+                            tcSubType_NC ctxt ty' ty'
        ; simplifyAmbiguityCheck ty wanted
 
        ; traceTc "Done ambiguity check for" (ppr ty) }
  where
    mk_msg ty tidy_env
      = do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
-          ; return (tidy_env', msg $$ ppWhen (not allow_ambiguous) ambig_msg) }
+          ; (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env ty
+          ; return (tidy_env', mk_msg tidy_ty $$ ppWhen (not allow_ambiguous) ambig_msg) }
      where
-       (tidy_env', tidy_ty) = tidyOpenType tidy_env ty
-       msg = hang (ptext (sLit "In the ambiguity check for:"))
-                2 (ppr tidy_ty)
+       mk_msg ty = pprSigCtxt ctxt (ptext (sLit "the ambiguity check for")) (ppr ty)
        ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")
 \end{code}
 
@@ -160,8 +159,7 @@ checkValidType ctxt ty
                = case ctxt of
                  DefaultDeclCtxt-> MustBeMonoType
                  ResSigCtxt     -> MustBeMonoType
-                 LamPatSigCtxt  -> rank0
-                 BindPatSigCtxt -> rank0
+                 PatSigCtxt     -> rank0
                  RuleSigCtxt _  -> rank1
                  TySynCtxt _    -> rank0