summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2014-11-21 10:58:10 +0000
committerSimon Peyton Jones <simonpj@microsoft.com>2014-11-21 11:35:24 +0000
commitb6855422fd532e5988fc98764c5cc47acbefbfb8 (patch)
treefdf442b66c2a0f4599bfd8418fabef90f8fe9be1 /compiler
parent76f5f11af42700e3a452c5e03e4ee0235cb08bf6 (diff)
downloadhaskell-b6855422fd532e5988fc98764c5cc47acbefbfb8.tar.gz
Implement full co/contra-variant subsumption checking (fixes Trac #9569)
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
Diffstat (limited to 'compiler')
-rw-r--r--compiler/deSugar/DsBinds.lhs9
-rw-r--r--compiler/deSugar/Match.lhs1
-rw-r--r--compiler/typecheck/Inst.lhs14
-rw-r--r--compiler/typecheck/TcBinds.lhs23
-rw-r--r--compiler/typecheck/TcErrors.lhs4
-rw-r--r--compiler/typecheck/TcEvidence.lhs42
-rw-r--r--compiler/typecheck/TcExpr.lhs8
-rw-r--r--compiler/typecheck/TcHsSyn.lhs5
-rw-r--r--compiler/typecheck/TcHsType.lhs41
-rw-r--r--compiler/typecheck/TcInstDcls.lhs6
-rw-r--r--compiler/typecheck/TcPat.lhs8
-rw-r--r--compiler/typecheck/TcRnTypes.lhs8
-rw-r--r--compiler/typecheck/TcType.lhs56
-rw-r--r--compiler/typecheck/TcUnify.lhs223
-rw-r--r--compiler/typecheck/TcValidity.lhs14
15 files changed, 312 insertions, 150 deletions
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index a3aac1b5a3..bc1b3528ca 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -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]
diff --git a/compiler/deSugar/Match.lhs b/compiler/deSugar/Match.lhs
index a14027862a..ddcd089546 100644
--- a/compiler/deSugar/Match.lhs
+++ b/compiler/deSugar/Match.lhs
@@ -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'
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index f2aec6ff20..3fd8e647f0 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -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
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index b44762e091..00f9f628f9 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -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'
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index a1cbbd606d..84a2c16d05 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -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
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 3b2a3d6727..83f6596e3d 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -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
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index 05a53d6ddd..1a2deba879 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -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) }
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 27d2648be3..d5dfd8e07c 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -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
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index d6f237f64f..722d162ecb 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -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,
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 3a6cca091b..215aa2d175 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -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)
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index b18ab7e148..cfa995d9d0 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -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
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 6f00b8609d..9ec93955ee 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -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)
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 74406c0033..a9b44ab1e6 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -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
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index f103fd7128..eb390384c8 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -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}
%************************************************************************
diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index 97d62d1f4f..123f030105 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -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
View Lorry Controller Status