Commit b6855422 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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
parent 76f5f11a
...@@ -820,12 +820,17 @@ dsHsWrapper WpHole e = return e ...@@ -820,12 +820,17 @@ dsHsWrapper WpHole e = return e
dsHsWrapper (WpTyApp ty) e = return $ App e (Type ty) dsHsWrapper (WpTyApp ty) e = return $ App e (Type ty)
dsHsWrapper (WpLet ev_binds) e = do bs <- dsTcEvBinds ev_binds dsHsWrapper (WpLet ev_binds) e = do bs <- dsTcEvBinds ev_binds
return (mkCoreLets bs e) 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) dsHsWrapper (WpCast co) e = ASSERT(tcCoercionRole co == Representational)
dsTcCoercion co (mkCast e) dsTcCoercion co (mkCast e)
dsHsWrapper (WpEvLam ev) e = return $ Lam ev e dsHsWrapper (WpEvLam ev) e = return $ Lam ev e
dsHsWrapper (WpTyLam tv) e = return $ Lam tv 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] dsTcEvBinds :: TcEvBinds -> DsM [CoreBind]
......
...@@ -987,6 +987,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2 ...@@ -987,6 +987,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
-- equating different ways of writing a coercion) -- equating different ways of writing a coercion)
wrap WpHole WpHole = True wrap WpHole WpHole = True
wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2' 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 (WpCast co) (WpCast co') = co `eq_co` co'
wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2 wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2
wrap (WpTyApp t) (WpTyApp t') = eqType t t' wrap (WpTyApp t) (WpTyApp t') = eqType t t'
......
...@@ -23,8 +23,6 @@ module Inst ( ...@@ -23,8 +23,6 @@ module Inst (
-- Simple functions over evidence variables -- Simple functions over evidence variables
tyVarsOfWC, tyVarsOfBag, tyVarsOfWC, tyVarsOfBag,
tyVarsOfCt, tyVarsOfCts, tyVarsOfCt, tyVarsOfCts,
tidyEvVar, tidyCt, tidySkolemInfo
) where ) where
#include "HsVersions.h" #include "HsVersions.h"
...@@ -49,7 +47,7 @@ import Class( Class ) ...@@ -49,7 +47,7 @@ import Class( Class )
import MkId( mkDictFunId ) import MkId( mkDictFunId )
import Id import Id
import Name import Name
import Var ( EvVar, varType, setVarType ) import Var ( EvVar )
import VarEnv import VarEnv
import VarSet import VarSet
import PrelNames import PrelNames
...@@ -59,7 +57,6 @@ import Bag ...@@ -59,7 +57,6 @@ import Bag
import Util import Util
import Outputable import Outputable
import Control.Monad( unless ) import Control.Monad( unless )
import Data.List( mapAccumL )
import Data.Maybe( isJust ) import Data.Maybe( isJust )
\end{code} \end{code}
...@@ -175,10 +172,11 @@ deeplyInstantiate orig ty ...@@ -175,10 +172,11 @@ deeplyInstantiate orig ty
; ids1 <- newSysLocalIds (fsLit "di") (substTys subst arg_tys) ; ids1 <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
; let theta' = substTheta subst theta ; let theta' = substTheta subst theta
; wrap1 <- instCall orig (mkTyVarTys tvs') theta' ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
; traceTc "Instantiating (deply)" (vcat [ ppr ty ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig
, text "with" <+> ppr tvs' , text "type" <+> ppr ty
, text "args:" <+> ppr ids1 , text "with" <+> ppr tvs'
, text "theta:" <+> ppr theta' ]) , text "args:" <+> ppr ids1
, text "theta:" <+> ppr theta' ])
; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho) ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
; return (mkWpLams ids1 ; return (mkWpLams ids1
<.> wrap2 <.> wrap2
......
...@@ -669,7 +669,7 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id) ...@@ -669,7 +669,7 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
-- See Note [Impedence matching] -- See Note [Impedence matching]
; (wrap, wanted) <- addErrCtxtM (mk_bind_msg inferred True poly_name (idType poly_id)) $ ; (wrap, wanted) <- addErrCtxtM (mk_bind_msg inferred True poly_name (idType poly_id)) $
captureConstraints $ 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 ; ev_binds <- simplifyTop wanted
; return (ABE { abe_wrap = mkWpLet (EvBinds ev_binds) <.> wrap ; return (ABE { abe_wrap = mkWpLet (EvBinds ev_binds) <.> wrap
...@@ -679,7 +679,6 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id) ...@@ -679,7 +679,6 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
where where
inferred = isNothing mb_sig inferred = isNothing mb_sig
prag_sigs = prag_fn poly_name prag_sigs = prag_fn poly_name
origin = AmbigOrigin sig_ctxt
sig_ctxt = InfSigCtxt poly_name sig_ctxt = InfSigCtxt poly_name
mkInferredPolyId :: Name -> [TyVar] -> TcThetaType -> TcType -> TcM Id mkInferredPolyId :: Name -> [TyVar] -> TcThetaType -> TcType -> TcM Id
...@@ -705,20 +704,21 @@ mkInferredPolyId poly_name qtvs theta mono_ty ...@@ -705,20 +704,21 @@ mkInferredPolyId poly_name qtvs theta mono_ty
; addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $ ; addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
checkValidType (InfSigCtxt poly_name) inferred_poly_ty checkValidType (InfSigCtxt poly_name) inferred_poly_ty
; return (mkLocalId 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 :: Bool -> Bool -> Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_bind_msg inferred want_ambig poly_name poly_ty tidy_env 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 where
msg = vcat [ ptext (sLit "When checking that") <+> quotes (ppr poly_name) mk_msg ty = vcat [ ptext (sLit "When checking that") <+> quotes (ppr poly_name)
<+> ptext (sLit "has the") <+> what <+> ptext (sLit "type") <+> ptext (sLit "has the") <+> what <+> ptext (sLit "type")
, nest 2 (ppr poly_name <+> dcolon <+> ppr tidy_ty) , nest 2 (ppr poly_name <+> dcolon <+> ppr ty)
, ppWhen want_ambig $ , ppWhen want_ambig $
ptext (sLit "Probable cause: the inferred type is ambiguous") ] ptext (sLit "Probable cause: the inferred type is ambiguous") ]
what | inferred = ptext (sLit "inferred") what | inferred = ptext (sLit "inferred")
| otherwise = ptext (sLit "specified") | otherwise = ptext (sLit "specified")
(tidy_env', tidy_ty) = tidyOpenType tidy_env poly_ty
\end{code} \end{code}
Note [Validity of inferred types] Note [Validity of inferred types]
...@@ -846,12 +846,11 @@ tcSpec poly_id prag@(SpecSig fun_name hs_ty inl) ...@@ -846,12 +846,11 @@ tcSpec poly_id prag@(SpecSig fun_name hs_ty inl)
(ptext (sLit "SPECIALISE pragma for non-overloaded function") (ptext (sLit "SPECIALISE pragma for non-overloaded function")
<+> quotes (ppr fun_name)) <+> quotes (ppr fun_name))
-- Note [SPECIALISE pragmas] -- 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) } ; return (SpecPrag poly_id wrap inl) }
where where
name = idName poly_id name = idName poly_id
poly_ty = idType poly_id poly_ty = idType poly_id
origin = SpecPragOrigin name
sig_ctxt = FunSigCtxt name sig_ctxt = FunSigCtxt name
spec_ctxt prag = hang (ptext (sLit "In the SPECIALISE pragma")) 2 (ppr prag) 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)) ...@@ -1326,7 +1325,7 @@ tcTySig (L loc (PatSynSig (L _ name) (_, qtvs) prov req ty))
; qtvs' <- mapM zonkQuantifiedTyVar qtvs' ; qtvs' <- mapM zonkQuantifiedTyVar qtvs'
; let (_, pat_ty) = splitFunTys ty' ; let (_, pat_ty) = tcSplitFunTys ty'
univ_set = tyVarsOfType pat_ty univ_set = tyVarsOfType pat_ty
(univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs' (univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs'
......
...@@ -1066,8 +1066,8 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell)) ...@@ -1066,8 +1066,8 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell))
-- Report "potential instances" only when the constraint arises -- Report "potential instances" only when the constraint arises
-- directly from the user's use of an overloaded function -- directly from the user's use of an overloaded function
want_potential (AmbigOrigin {}) = False want_potential (TypeEqOrigin {}) = False
want_potential _ = True want_potential _ = True
add_to_ctxt_fixes has_ambig_tvs add_to_ctxt_fixes has_ambig_tvs
| not has_ambig_tvs && all_tyvars | not has_ambig_tvs && all_tyvars
......
...@@ -10,7 +10,7 @@ module TcEvidence ( ...@@ -10,7 +10,7 @@ module TcEvidence (
-- HsWrapper -- HsWrapper
HsWrapper(..), HsWrapper(..),
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCast, (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCast,
idHsWrapper, isIdHsWrapper, pprHsWrapper, mkWpFun, idHsWrapper, isIdHsWrapper, pprHsWrapper,
-- Evidence bindings -- Evidence bindings
TcEvBinds(..), EvBindsVar(..), TcEvBinds(..), EvBindsVar(..),
...@@ -142,6 +142,9 @@ mkTcReflCo = TcRefl ...@@ -142,6 +142,9 @@ mkTcReflCo = TcRefl
mkTcNomReflCo :: TcType -> TcCoercion mkTcNomReflCo :: TcType -> TcCoercion
mkTcNomReflCo = TcRefl Nominal mkTcNomReflCo = TcRefl Nominal
mkTcRepReflCo :: TcType -> TcCoercion
mkTcRepReflCo = TcRefl Representational
mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2] mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
...@@ -441,14 +444,22 @@ data HsWrapper ...@@ -441,14 +444,22 @@ data HsWrapper
-- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
-- But ([] a) `WpCompose` ([] b) = ([] b a) -- 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 | WpCast TcCoercion -- A cast: [] `cast` co
-- Guaranteed not the identity coercion -- Guaranteed not the identity coercion
-- At role Representational -- At role Representational
-- Evidence abstraction and application -- Evidence abstraction and application
-- (both dictionaries and coercions) -- (both dictionaries and coercions)
| WpEvLam EvVar -- \d. [] the 'd' is an evidence variable | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable
| WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint
-- Kind and Type abstraction and application -- Kind and Type abstraction and application
| WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var) | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var)
...@@ -465,9 +476,18 @@ WpHole <.> c = c ...@@ -465,9 +476,18 @@ WpHole <.> c = c
c <.> WpHole = c c <.> WpHole = c
c1 <.> c2 = c1 `WpCompose` c2 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 :: TcCoercion -> HsWrapper
mkWpCast co = ASSERT2(tcCoercionRole co == Representational, ppr co) mkWpCast co
WpCast co | isTcReflCo co = WpHole
| otherwise = ASSERT2(tcCoercionRole co == Representational, ppr co)
WpCast co
mkWpTyApps :: [Type] -> HsWrapper mkWpTyApps :: [Type] -> HsWrapper
mkWpTyApps tys = mk_co_app_fn WpTyApp tys mkWpTyApps tys = mk_co_app_fn WpTyApp tys
...@@ -746,13 +766,15 @@ pprHsWrapper doc wrap ...@@ -746,13 +766,15 @@ pprHsWrapper doc wrap
-- False <=> appears as body of let or lambda -- False <=> appears as body of let or lambda
help it WpHole = it help it WpHole = it
help it (WpCompose f1 f2) = help (help it f2) f1 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 "|>") help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
<+> pprParendTcCo co)] <+> pprParendTcCo co)]
help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)] 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 (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 (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 (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 (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
pp_bndr v = pprBndr LambdaBind v <> dot pp_bndr v = pprBndr LambdaBind v <> dot
......
...@@ -914,15 +914,17 @@ tcApp fun args res_ty ...@@ -914,15 +914,17 @@ tcApp fun args res_ty
-- Typecheck the result, thereby propagating -- Typecheck the result, thereby propagating
-- info (if any) from result into the argument types -- info (if any) from result into the argument types
-- Both actual_res_ty and res_ty are deeply skolemised -- Both actual_res_ty and res_ty are deeply skolemised
; co_res <- addErrCtxtM (funResCtxt True (unLoc fun) actual_res_ty res_ty) $ -- Rather like tcWrapResult, but (perhaps for historical reasons)
unifyType actual_res_ty res_ty -- 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 -- Typecheck the arguments
; args1 <- tcArgs fun args expected_arg_tys ; args1 <- tcArgs fun args expected_arg_tys
-- Assemble the result -- Assemble the result
; let fun2 = mkLHsWrapCo co_fun fun1 ; 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) } ; return (unLoc app) }
......
...@@ -838,6 +838,11 @@ zonkCoFn env WpHole = return (env, WpHole) ...@@ -838,6 +838,11 @@ zonkCoFn env WpHole = return (env, WpHole)
zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1 zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
; (env2, c2') <- zonkCoFn env1 c2 ; (env2, c2') <- zonkCoFn env1 c2
; return (env2, WpCompose c1' 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 zonkCoFn env (WpCast co) = do { co' <- zonkTcCoToCo env co
; return (env, WpCast co') } ; return (env, WpCast co') }
zonkCoFn env (WpEvLam ev) = do { (env', ev') <- zonkEvBndrX env ev zonkCoFn env (WpEvLam ev) = do { (env', ev') <- zonkEvBndrX env ev
......
...@@ -161,7 +161,7 @@ tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type ...@@ -161,7 +161,7 @@ tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
-- HsForAllTy in hs_ty occur *first* in the returned type. -- HsForAllTy in hs_ty occur *first* in the returned type.
-- See Note [Scoped] with TcSigInfo -- See Note [Scoped] with TcSigInfo
tcHsSigType ctxt hs_ty tcHsSigType ctxt hs_ty
= addErrCtxt (pprHsSigCtxt ctxt hs_ty) $ = addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
tcHsSigTypeNC ctxt hs_ty tcHsSigTypeNC ctxt hs_ty
tcHsSigTypeNC ctxt (L loc hs_ty) tcHsSigTypeNC ctxt (L loc hs_ty)
...@@ -1240,7 +1240,7 @@ tcHsPatSigType :: UserTypeCtxt ...@@ -1240,7 +1240,7 @@ tcHsPatSigType :: UserTypeCtxt
-- (c) RULE forall bndrs e.g. forall (x::Int). f x = x -- (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 }) 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 do { kvs <- mapM new_kv sig_kvs
; tvs <- mapM new_tv sig_tvs ; tvs <- mapM new_tv sig_tvs
; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` 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 ...@@ -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)) RuleSigCtxt {} -> return (mkTcTyVar name kind (SkolemTv False))
_ -> newSigTyVar name kind -- See Note [Unifying SigTvs] _ -> newSigTyVar name kind -- See Note [Unifying SigTvs]
tcPatSig :: UserTypeCtxt tcPatSig :: Bool -- True <=> pattern binding
-> HsWithBndrs Name (LHsType Name) -> HsWithBndrs Name (LHsType Name)
-> TcSigmaType -> TcSigmaType
-> TcM (TcType, -- The type to use for "inside" the signature -> TcM (TcType, -- The type to use for "inside" the signature
...@@ -1267,15 +1267,16 @@ tcPatSig :: UserTypeCtxt ...@@ -1267,15 +1267,16 @@ tcPatSig :: UserTypeCtxt
-- the scoped type variables -- the scoped type variables
HsWrapper) -- Coercion due to unification with actual ty HsWrapper) -- Coercion due to unification with actual ty
-- Of shape: res_ty ~ sig_ty -- Of shape: res_ty ~ sig_ty
tcPatSig ctxt sig res_ty tcPatSig in_pat_bind sig res_ty
= do { (sig_ty, sig_tvs) <- tcHsPatSigType ctxt sig = do { (sig_ty, sig_tvs) <- tcHsPatSigType PatSigCtxt sig
-- sig_tvs are the type variables free in 'sig', -- sig_tvs are the type variables free in 'sig',
-- and not already in scope. These are the ones -- and not already in scope. These are the ones
-- that should be brought into scope -- that should be brought into scope
; if null sig_tvs then do { ; if null sig_tvs then do {
-- Just do the subsumption check and return -- 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) ; return (sig_ty, [], wrap)
} else do } else do
-- Type signature binds at least one scoped type variable -- Type signature binds at least one scoped type variable
...@@ -1283,10 +1284,7 @@ tcPatSig ctxt sig res_ty ...@@ -1283,10 +1284,7 @@ tcPatSig ctxt sig res_ty
-- A pattern binding cannot bind scoped type variables -- A pattern binding cannot bind scoped type variables
-- It is more convenient to make the test here -- It is more convenient to make the test here
-- than in the renamer -- than in the renamer
{ let in_pat_bind = case ctxt of { when in_pat_bind (addErr (patBindSigErr sig_tvs))
BindPatSigCtxt -> True
_ -> False
; when in_pat_bind (addErr (patBindSigErr sig_tvs))
-- Check that all newly-in-scope tyvars are in fact -- Check that all newly-in-scope tyvars are in fact
-- constrained by the pattern. This catches tiresome -- constrained by the pattern. This catches tiresome
...@@ -1300,11 +1298,21 @@ tcPatSig ctxt sig res_ty ...@@ -1300,11 +1298,21 @@ tcPatSig ctxt sig res_ty
; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs) ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
-- Now do a subsumption check of the pattern signature against res_ty -- 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! -- Phew!
; return (sig_ty, sig_tvs, wrap) ; 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 :: [(Name, TcTyVar)] -> SDoc
patBindSigErr sig_tvs patBindSigErr sig_tvs
...@@ -1628,17 +1636,6 @@ promotionErr name err ...@@ -1628,17 +1636,6 @@ promotionErr name err
%************************************************************************ %************************************************************************
\begin{code} \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 :: TcType -> [TyVar] -> SDoc
badPatSigTvs sig_ty bad_tvs badPatSigTvs sig_ty bad_tvs
= vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
......
...@@ -1141,12 +1141,10 @@ Note that ...@@ -1141,12 +1141,10 @@ Note that
tcSpecInst :: Id -> Sig Name -> TcM TcSpecPrag tcSpecInst :: Id -> Sig Name -> TcM TcSpecPrag
tcSpecInst dfun_id prag@(SpecInstSig hs_ty) tcSpecInst dfun_id prag@(SpecInstSig hs_ty)
= addErrCtxt (spec_ctxt prag) $ = addErrCtxt (spec_ctxt prag) $
do { let name = idName dfun_id do { (tyvars, theta, clas, tys) <- tcHsInstHead SpecInstCtxt hs_ty
; (tyvars, theta, clas, tys) <- tcHsInstHead SpecInstCtxt hs_ty
; let (_, spec_dfun_ty) = mkDictFunTy tyvars theta clas tys ; let (_, spec_dfun_ty) = mkDictFunTy tyvars theta clas tys
; co_fn <- tcSubType (SpecPragOrigin name) SpecInstCtxt ; co_fn <- tcSubType SpecInstCtxt (idType dfun_id) spec_dfun_ty
(idType dfun_id) spec_dfun_ty
; return (SpecPrag dfun_id co_fn defaultInlinePragma) } ; return (SpecPrag dfun_id co_fn defaultInlinePragma) }
where where
spec_ctxt prag = hang (ptext (sLit "In the SPECIALISE pragma")) 2 (ppr prag) spec_ctxt prag = hang (ptext (sLit "In the SPECIALISE pragma")) 2 (ppr prag)
......
...@@ -129,9 +129,9 @@ data LetBndrSpec ...@@ -129,9 +129,9 @@ data LetBndrSpec
makeLazy :: PatEnv -> PatEnv makeLazy :: PatEnv -> PatEnv
makeLazy penv = penv { pe_lazy = True } makeLazy penv = penv { pe_lazy = True }
patSigCtxt :: PatEnv -> UserTypeCtxt inPatBind :: PatEnv -> Bool
patSigCtxt (PE { pe_ctxt = LetPat {} }) = BindPatSigCtxt inPatBind (PE { pe_ctxt = LetPat {} }) = True
patSigCtxt (PE { pe_ctxt = LamPat {} }) = LamPatSigCtxt inPatBind (PE { pe_ctxt = LamPat {} }) = False
--------------- ---------------
type TcPragFun = Name -> [LSig Name] type TcPragFun = Name -> [LSig Name]
...@@ -505,7 +505,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside ...@@ -505,7 +505,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
-- Type signatures in patterns -- Type signatures in patterns
-- See Note [Pattern coercions] below -- See Note [Pattern coercions] below
tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside 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 $ ; (pat', res) <- tcExtendTyVarEnv2 tv_binds $
tc_lpat pat inner_ty penv thing_inside tc_lpat pat inner_ty penv thing_inside
......
...@@ -1861,7 +1861,6 @@ data CtOrigin ...@@ -1861,7 +1861,6 @@ data CtOrigin
| PArrSeqOrigin (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:] | PArrSeqOrigin (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
| SectionOrigin | SectionOrigin
| TupleOrigin -- (..,..) | TupleOrigin -- (..,..)
| AmbigOrigin UserTypeCtxt -- Will be FunSigCtxt, InstDeclCtxt, or SpecInstCtxt
| ExprSigOrigin -- e :: ty | ExprSigOrigin -- e :: ty
| PatSigOrigin -- p :: ty | PatSigOrigin -- p :: ty
| PatOrigin -- Instantiating a polytyped pattern at a constructor | PatOrigin -- Instantiating a polytyped pattern at a constructor
...@@ -1930,13 +1929,6 @@ pprCtOrigin (DerivOriginDC dc n) ...@@ -1930,13 +1929,6 @@ pprCtOrigin (DerivOriginDC dc n)
where where
ty = dataConOrigArgTys dc !! (n-1) 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) pprCtOrigin (DerivOriginCoerce meth ty1 ty2)
= hang (ctoHerald <+> ptext (sLit "the coercion of the method") <+> quotes (ppr meth)) = hang (ctoHerald <+> ptext (sLit "the coercion of the method") <+> quotes (ppr meth))
2 (sep [ ptext (sLit "from type") <+> quotes (ppr ty1) 2 (sep [ ptext (sLit "from type") <+> quotes (ppr ty1)
......
...@@ -29,7 +29,7 @@ module TcType ( ...@@ -29,7 +29,7 @@ module TcType (
-------------------------------- --------------------------------
-- MetaDetails -- MetaDetails
UserTypeCtxt(..), pprUserTypeCtxt, UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt,
TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv, TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
MetaDetails(Flexi, Indirect), MetaInfo(..), MetaDetails(Flexi, Indirect), MetaInfo(..),
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
...@@ -63,7 +63,7 @@ module TcType ( ...@@ -63,7 +63,7 @@ module TcType (
-- Again, newtypes are opaque -- Again, newtypes are opaque
eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX, eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
pickyEqType, tcEqType, tcEqKind, pickyEqType, tcEqType, tcEqKind,
isSigmaTy, isOverloadedTy, isSigmaTy, isRhoTy, isOverloadedTy,
isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy, isIntegerTy, isBoolTy, isUnitTy, isCharTy,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
...@@ -232,12 +232,20 @@ type TcType = Type -- A TcType can have mutable type variables ...@@ -232,12 +232,20 @@ type TcType = Type -- A TcType can have mutable type variables
type TcPredType = PredType type TcPredType = PredType
type TcThetaType = ThetaType type TcThetaType = ThetaType
type TcSigmaType = TcType type TcSigmaType = TcType
type TcRhoType = TcType type TcRhoType = TcType -- Note [TcRhoType]
type TcTauType = TcType type TcTauType = TcType
type TcKind = Kind type TcKind = Kind
type TcTyVarSet = TyVarSet type TcTyVarSet = TyVarSet
\end{code} \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 ...@@ -361,10 +369,9 @@ data UserTypeCtxt
| ExprSigCtxt -- Expression type signature | ExprSigCtxt -- Expression type signature
| ConArgCtxt Name -- Data constructor argument | ConArgCtxt Name -- Data constructor argument