Visible type application
authorRichard Eisenberg <eir@cis.upenn.edu>
Thu, 24 Dec 2015 19:33:19 +0000 (14:33 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Thu, 24 Dec 2015 19:37:39 +0000 (14:37 -0500)
This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.

This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.

This patch addresses tickets #10619, #5296, #10589.

257 files changed:
compiler/basicTypes/DataCon.hs
compiler/basicTypes/MkId.hs
compiler/basicTypes/PatSyn.hs
compiler/coreSyn/MkCore.hs
compiler/deSugar/Coverage.hs
compiler/deSugar/DsArrows.hs
compiler/deSugar/DsBinds.hs
compiler/deSugar/DsExpr.hs
compiler/deSugar/Match.hs
compiler/hsSyn/HsBinds.hs
compiler/hsSyn/HsExpr.hs
compiler/hsSyn/HsUtils.hs
compiler/hsSyn/PlaceHolder.hs
compiler/iface/IfaceSyn.hs
compiler/iface/IfaceType.hs
compiler/main/DynFlags.hs
compiler/main/PprTyThing.hs
compiler/parser/Lexer.x
compiler/parser/Parser.y
compiler/prelude/PrimOp.hs
compiler/prelude/TysPrim.hs
compiler/prelude/TysWiredIn.hs
compiler/rename/RnExpr.hs
compiler/rename/RnSplice.hs
compiler/rename/RnTypes.hs
compiler/typecheck/Inst.hs
compiler/typecheck/TcArrows.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcClassDcl.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcExpr.hs-boot
compiler/typecheck/TcGenDeriv.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcMatches.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/TyCoRep.hs
compiler/types/Type.hs
docs/users_guide/7.12.1-notes.rst
docs/users_guide/glasgow_exts.rst
libraries/base/tests/T9681.stderr
libraries/ghc-boot/GHC/LanguageExtensions.hs
testsuite/tests/ado/ado002.stderr
testsuite/tests/annotations/should_fail/annfail08.stderr
testsuite/tests/arrows/should_fail/T5380.stderr
testsuite/tests/boxy/all.T
testsuite/tests/deSugar/should_compile/T2431.stderr
testsuite/tests/driver/T2182.stderr
testsuite/tests/driver/T4437.hs
testsuite/tests/driver/werror.stderr
testsuite/tests/gadt/T3169.stderr
testsuite/tests/gadt/gadt-escape1.stderr
testsuite/tests/gadt/gadt13.stderr
testsuite/tests/gadt/gadt7.stderr
testsuite/tests/gadt/rw.stderr
testsuite/tests/ghc-api/annotations/T10280.stderr
testsuite/tests/ghc-api/annotations/T10357.stderr
testsuite/tests/ghci.debugger/scripts/break003.stderr
testsuite/tests/ghci.debugger/scripts/break003.stdout
testsuite/tests/ghci.debugger/scripts/break005.stdout
testsuite/tests/ghci.debugger/scripts/break006.stderr
testsuite/tests/ghci.debugger/scripts/break006.stdout
testsuite/tests/ghci.debugger/scripts/hist001.stdout
testsuite/tests/ghci/scripts/Defer02.stderr
testsuite/tests/ghci/scripts/T10122.stdout
testsuite/tests/ghci/scripts/T10508.stderr
testsuite/tests/ghci/scripts/T7627.stdout
testsuite/tests/ghci/scripts/T8649.stderr
testsuite/tests/ghci/scripts/T8959b.stderr
testsuite/tests/ghci/scripts/ghci013.stdout
testsuite/tests/ghci/scripts/ghci025.stdout
testsuite/tests/ghci/scripts/ghci047.stderr
testsuite/tests/ghci/scripts/ghci050.stderr
testsuite/tests/ghci/scripts/ghci052.stderr
testsuite/tests/ghci/scripts/ghci053.stderr
testsuite/tests/ghci/scripts/ghci055.stdout
testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
testsuite/tests/indexed-types/should_fail/T2544.stderr
testsuite/tests/indexed-types/should_fail/T2693.stderr
testsuite/tests/indexed-types/should_fail/T3330a.stderr
testsuite/tests/indexed-types/should_fail/T3330c.stderr
testsuite/tests/indexed-types/should_fail/T3440.stderr
testsuite/tests/indexed-types/should_fail/T4099.stderr
testsuite/tests/indexed-types/should_fail/T4179.stderr
testsuite/tests/indexed-types/should_fail/T4485.stderr
testsuite/tests/indexed-types/should_fail/T5439.stderr
testsuite/tests/indexed-types/should_fail/T7010.stderr
testsuite/tests/indexed-types/should_fail/T7194.stderr
testsuite/tests/indexed-types/should_fail/T7354.stderr
testsuite/tests/indexed-types/should_fail/T7354a.stderr
testsuite/tests/indexed-types/should_fail/T7729.stderr
testsuite/tests/indexed-types/should_fail/T7729a.stderr
testsuite/tests/indexed-types/should_fail/T7788.stderr
testsuite/tests/indexed-types/should_fail/T8227.stderr
testsuite/tests/indexed-types/should_fail/T8518.stderr
testsuite/tests/indexed-types/should_fail/T9554.stderr
testsuite/tests/indexed-types/should_fail/T9662.stderr
testsuite/tests/module/mod121.stderr
testsuite/tests/module/mod147.stderr
testsuite/tests/module/mod160.stderr
testsuite/tests/module/mod69.stderr
testsuite/tests/module/mod70.stderr
testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr
testsuite/tests/parser/should_compile/T2245.stderr
testsuite/tests/parser/should_compile/VtaParse.hs [new file with mode: 0644]
testsuite/tests/parser/should_compile/all.T
testsuite/tests/parser/should_compile/read014.stderr
testsuite/tests/parser/should_fail/readFail003.stderr
testsuite/tests/partial-sigs/should_compile/T10403.stderr
testsuite/tests/partial-sigs/should_compile/T10438.stderr
testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr
testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSignature.stderr
testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotEnabled.stderr
testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr
testsuite/tests/patsyn/should_fail/records-poly-update.stderr
testsuite/tests/perf/compiler/all.T
testsuite/tests/polykinds/T10503.stderr
testsuite/tests/polykinds/T6068.stdout
testsuite/tests/polykinds/T7438.stderr
testsuite/tests/polykinds/T7594.stderr
testsuite/tests/polykinds/T9144.stderr
testsuite/tests/polykinds/TidyClassKinds.hs [new file with mode: 0644]
testsuite/tests/polykinds/TidyClassKinds.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T
testsuite/tests/rename/should_compile/T3823.stderr
testsuite/tests/rename/should_fail/T10618.stderr
testsuite/tests/rename/should_fail/T2993.stderr
testsuite/tests/rename/should_fail/T7937.stderr
testsuite/tests/rename/should_fail/mc13.stderr
testsuite/tests/rename/should_fail/rnfail016.stderr
testsuite/tests/rename/should_fail/rnfail051.stderr
testsuite/tests/roles/should_compile/Roles1.stderr
testsuite/tests/roles/should_compile/T8958.stderr
testsuite/tests/rts/T9045.hs
testsuite/tests/safeHaskell/ghci/p16.stderr
testsuite/tests/safeHaskell/ghci/p6.stderr
testsuite/tests/simplCore/should_compile/T7360.stderr
testsuite/tests/simplCore/should_compile/simpl017.stderr
testsuite/tests/th/T10945.stderr
testsuite/tests/th/T8577.stderr
testsuite/tests/typecheck/bug1465/bug1465.stderr
testsuite/tests/typecheck/should_compile/FD1.stderr
testsuite/tests/typecheck/should_compile/FD2.stderr
testsuite/tests/typecheck/should_compile/PushHRIf.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/T10072.stderr
testsuite/tests/typecheck/should_compile/T10971a.stderr
testsuite/tests/typecheck/should_compile/T2494.stderr
testsuite/tests/typecheck/should_compile/Vta1.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/Vta2.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_compile/holes.stderr
testsuite/tests/typecheck/should_compile/holes3.stderr
testsuite/tests/typecheck/should_compile/tc141.stderr
testsuite/tests/typecheck/should_compile/tc168.stderr
testsuite/tests/typecheck/should_compile/tc211.stderr
testsuite/tests/typecheck/should_compile/tc243.stderr
testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr
testsuite/tests/typecheck/should_fail/T10495.stderr
testsuite/tests/typecheck/should_fail/T10971d.stderr
testsuite/tests/typecheck/should_fail/T11274.stderr
testsuite/tests/typecheck/should_fail/T1899.stderr
testsuite/tests/typecheck/should_fail/T2414.stderr
testsuite/tests/typecheck/should_fail/T2534.stderr
testsuite/tests/typecheck/should_fail/T2688.stderr
testsuite/tests/typecheck/should_fail/T2846b.stderr
testsuite/tests/typecheck/should_fail/T3102.stderr
testsuite/tests/typecheck/should_fail/T3613.stderr
testsuite/tests/typecheck/should_fail/T3950.stderr
testsuite/tests/typecheck/should_fail/T5095.stderr
testsuite/tests/typecheck/should_fail/T5689.stderr
testsuite/tests/typecheck/should_fail/T5853.stderr
testsuite/tests/typecheck/should_fail/T6069.stderr
testsuite/tests/typecheck/should_fail/T7264.stderr
testsuite/tests/typecheck/should_fail/T7368.stderr
testsuite/tests/typecheck/should_fail/T7453.stderr
testsuite/tests/typecheck/should_fail/T7734.stderr
testsuite/tests/typecheck/should_fail/T7851.stderr
testsuite/tests/typecheck/should_fail/T8142.stderr
testsuite/tests/typecheck/should_fail/T8428.stderr
testsuite/tests/typecheck/should_fail/T8603.stderr
testsuite/tests/typecheck/should_fail/T9109.stderr
testsuite/tests/typecheck/should_fail/T9774.stderr
testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
testsuite/tests/typecheck/should_fail/TcStaticPointersFail01.stderr
testsuite/tests/typecheck/should_fail/VtaFail.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/VtaFail.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_fail/mc19.stderr
testsuite/tests/typecheck/should_fail/mc21.stderr
testsuite/tests/typecheck/should_fail/mc22.stderr
testsuite/tests/typecheck/should_fail/mc23.stderr
testsuite/tests/typecheck/should_fail/mc24.stderr
testsuite/tests/typecheck/should_fail/mc25.stderr
testsuite/tests/typecheck/should_fail/tcfail001.stderr
testsuite/tests/typecheck/should_fail/tcfail002.stderr
testsuite/tests/typecheck/should_fail/tcfail004.stderr
testsuite/tests/typecheck/should_fail/tcfail005.stderr
testsuite/tests/typecheck/should_fail/tcfail007.stderr
testsuite/tests/typecheck/should_fail/tcfail010.stderr
testsuite/tests/typecheck/should_fail/tcfail013.stderr
testsuite/tests/typecheck/should_fail/tcfail014.stderr
testsuite/tests/typecheck/should_fail/tcfail016.stderr
testsuite/tests/typecheck/should_fail/tcfail018.stderr
testsuite/tests/typecheck/should_fail/tcfail029.stderr
testsuite/tests/typecheck/should_fail/tcfail032.stderr
testsuite/tests/typecheck/should_fail/tcfail033.stderr
testsuite/tests/typecheck/should_fail/tcfail034.stderr
testsuite/tests/typecheck/should_fail/tcfail065.stderr
testsuite/tests/typecheck/should_fail/tcfail068.stderr
testsuite/tests/typecheck/should_fail/tcfail076.stderr
testsuite/tests/typecheck/should_fail/tcfail099.stderr
testsuite/tests/typecheck/should_fail/tcfail103.stderr
testsuite/tests/typecheck/should_fail/tcfail104.stderr
testsuite/tests/typecheck/should_fail/tcfail131.stderr
testsuite/tests/typecheck/should_fail/tcfail133.stderr
testsuite/tests/typecheck/should_fail/tcfail140.stderr
testsuite/tests/typecheck/should_fail/tcfail143.stderr
testsuite/tests/typecheck/should_fail/tcfail153.stderr
testsuite/tests/typecheck/should_fail/tcfail165.hs
testsuite/tests/typecheck/should_fail/tcfail165.stderr [deleted file]
testsuite/tests/typecheck/should_fail/tcfail168.stderr
testsuite/tests/typecheck/should_fail/tcfail174.hs
testsuite/tests/typecheck/should_fail/tcfail174.stderr
testsuite/tests/typecheck/should_fail/tcfail175.stderr
testsuite/tests/typecheck/should_fail/tcfail178.stderr
testsuite/tests/typecheck/should_fail/tcfail179.stderr
testsuite/tests/typecheck/should_fail/tcfail181.stderr
testsuite/tests/typecheck/should_fail/tcfail185.stderr
testsuite/tests/typecheck/should_fail/tcfail189.stderr
testsuite/tests/typecheck/should_fail/tcfail191.stderr
testsuite/tests/typecheck/should_fail/tcfail193.stderr
testsuite/tests/typecheck/should_fail/tcfail198.stderr
testsuite/tests/typecheck/should_fail/tcfail201.stderr
testsuite/tests/typecheck/should_fail/tcfail204.stderr
testsuite/tests/typecheck/should_fail/tcfail206.stderr
testsuite/tests/typecheck/should_fail/tcfail208.stderr
testsuite/tests/typecheck/should_run/all.T
testsuite/tests/typecheck/should_run/tcrun035.stderr [deleted file]
testsuite/tests/warnings/should_compile/PluralS.stderr
testsuite/tests/warnings/should_compile/T11077.stderr

index 712a9b2..466e3c1 100644 (file)
@@ -768,7 +768,7 @@ mkDataCon name declared_infix prom_info
 
     tag = assoc "mkDataCon" (tyConDataCons rep_tycon `zip` [fIRST_TAG..]) con
     rep_arg_tys = dataConRepArgTys con
-    rep_ty = mkInvForAllTys univ_tvs $ mkInvForAllTys ex_tvs $
+    rep_ty = mkSpecForAllTys univ_tvs $ mkInvForAllTys ex_tvs $
              mkFunTys rep_arg_tys $
              mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
 
@@ -1024,8 +1024,8 @@ dataConUserType (MkData { dcUnivTyVars = univ_tvs,
                           dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
                           dcOtherTheta = theta, dcOrigArgTys = arg_tys,
                           dcOrigResTy = res_ty })
-  = mkInvForAllTys ((univ_tvs `minusList` map eqSpecTyVar eq_spec) ++
-                    ex_tvs) $
+  = mkSpecForAllTys ((univ_tvs `minusList` map eqSpecTyVar eq_spec) ++
+                      ex_tvs) $
     mkFunTys theta $
     mkFunTys arg_tys $
     res_ty
index 691e087..f690732 100644 (file)
@@ -281,8 +281,8 @@ mkDictSelId name clas
     arg_tys        = dataConRepArgTys data_con  -- Includes the dictionary superclasses
     val_index      = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name
 
-    sel_ty = mkInvForAllTys tyvars (mkFunTy (mkClassPred clas (mkTyVarTys tyvars))
-                                            (getNth arg_tys val_index))
+    sel_ty = mkSpecForAllTys tyvars (mkFunTy (mkClassPred clas (mkTyVarTys tyvars))
+                                             (getNth arg_tys val_index))
 
     base_info = noCafIdInfo
                 `setArityInfo`         1
@@ -930,7 +930,7 @@ mkPrimOpId prim_op
   = id
   where
     (tyvars,arg_tys,res_ty, arity, strict_sig) = primOpSig prim_op
-    ty   = mkInvForAllTys tyvars (mkFunTys arg_tys res_ty)
+    ty   = mkSpecForAllTys tyvars (mkFunTys arg_tys res_ty)
     name = mkWiredInName gHC_PRIM (primOpOcc prim_op)
                          (mkPrimOpIdUnique (primOpTag prim_op))
                          (AnId id) UserSyntax
@@ -1014,7 +1014,7 @@ mkDictFunId dfun_name tvs theta clas tys
 
 mkDictFunTy :: [TyVar] -> ThetaType -> Class -> [Type] -> Type
 mkDictFunTy tvs theta clas tys
- = mkInvSigmaTy tvs theta (mkClassPred clas tys)
+ = mkSpecSigmaTy tvs theta (mkClassPred clas tys)
 
 {-
 ************************************************************************
@@ -1062,7 +1062,7 @@ dollarId = pcMiscPrelId dollarName ty
              (noCafIdInfo `setUnfoldingInfo` unf)
   where
     fun_ty = mkFunTy alphaTy openBetaTy
-    ty     = mkInvForAllTys [levity2TyVar, alphaTyVar, openBetaTyVar] $
+    ty     = mkSpecForAllTys [levity2TyVar, alphaTyVar, openBetaTyVar] $
              mkFunTy fun_ty fun_ty
     unf    = mkInlineUnfolding (Just 2) rhs
     [f,x]  = mkTemplateLocals [fun_ty, alphaTy]
@@ -1076,7 +1076,7 @@ proxyHashId
   = pcMiscPrelId proxyName ty
        (noCafIdInfo `setUnfoldingInfo` evaldUnfolding) -- Note [evaldUnfoldings]
   where
-    ty      = mkInvForAllTys [kv, tv] (mkProxyPrimTy k t)
+    ty      = mkSpecForAllTys [kv, tv] (mkProxyPrimTy k t)
     kv      = kKiVar
     k       = mkTyVarTy kv
     [tv]    = mkTemplateTyVars [k]
@@ -1091,9 +1091,9 @@ unsafeCoerceId
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
 
-    ty  = mkInvForAllTys [ levity1TyVar, levity2TyVar
-                         , openAlphaTyVar, openBetaTyVar ]
-                         (mkFunTy openAlphaTy openBetaTy)
+    ty  = mkSpecForAllTys [ levity1TyVar, levity2TyVar
+                          , openAlphaTyVar, openBetaTyVar ]
+                          (mkFunTy openAlphaTy openBetaTy)
 
     [x] = mkTemplateLocals [openAlphaTy]
     rhs = mkLams [ levity1TyVar, levity2TyVar
@@ -1125,8 +1125,8 @@ seqId = pcMiscPrelId seqName ty info
                   -- LHS of rules.  That way we can have rules for 'seq';
                   -- see Note [seqId magic]
 
-    ty  = mkInvForAllTys [alphaTyVar,betaTyVar]
-                         (mkFunTy alphaTy (mkFunTy betaTy betaTy))
+    ty  = mkSpecForAllTys [alphaTyVar,betaTyVar]
+                          (mkFunTy alphaTy (mkFunTy betaTy betaTy))
 
     [x,y] = mkTemplateLocals [alphaTy, betaTy]
     rhs = mkLams [alphaTyVar,betaTyVar,x,y] (Case (Var x) x betaTy [(DEFAULT, [], Var y)])
@@ -1158,16 +1158,16 @@ lazyId :: Id    -- See Note [lazyId magic]
 lazyId = pcMiscPrelId lazyIdName ty info
   where
     info = noCafIdInfo
-    ty  = mkInvForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
+    ty  = mkSpecForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
 
 oneShotId :: Id -- See Note [The oneShot function]
 oneShotId = pcMiscPrelId oneShotName ty info
   where
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
-    ty  = mkInvForAllTys [ levity1TyVar, levity2TyVar
-                         , openAlphaTyVar, openBetaTyVar ]
-                         (mkFunTy fun_ty fun_ty)
+    ty  = mkSpecForAllTys [ levity1TyVar, levity2TyVar
+                          , openAlphaTyVar, openBetaTyVar ]
+                          (mkFunTy fun_ty fun_ty)
     fun_ty = mkFunTy alphaTy betaTy
     [body, x] = mkTemplateLocals [fun_ty, openAlphaTy]
     x' = setOneShotLambda x
@@ -1188,7 +1188,7 @@ runRWId = pcMiscPrelId runRWName ty info
     arg_ty  = stateRW `mkFunTy` ret_ty
     -- (State# RealWorld -> (# State# RealWorld, o #))
     --   -> (# State# RealWorld, o #)
-    ty      = mkInvForAllTys [levity1TyVar, openAlphaTyVar] $
+    ty      = mkSpecForAllTys [levity1TyVar, openAlphaTyVar] $
               arg_ty `mkFunTy` ret_ty
 
 --------------------------------------------------------------------------------
@@ -1196,7 +1196,7 @@ magicDictId :: Id  -- See Note [magicDictId magic]
 magicDictId = pcMiscPrelId magicDictName ty info
   where
   info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
-  ty   = mkInvForAllTys [alphaTyVar] alphaTy
+  ty   = mkSpecForAllTys [alphaTyVar] alphaTy
 
 --------------------------------------------------------------------------------
 
@@ -1210,7 +1210,7 @@ coerceId = pcMiscPrelId coerceName ty info
     eqRPrimTy = mkTyConApp eqReprPrimTyCon [ liftedTypeKind
                                            , liftedTypeKind
                                            , alphaTy, betaTy ]
-    ty        = mkInvForAllTys [alphaTyVar, betaTyVar] $
+    ty        = mkSpecForAllTys [alphaTyVar, betaTyVar] $
                 mkFunTys [eqRTy, alphaTy] betaTy
 
     [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy, eqRPrimTy]
index c35bcf3..a884e96 100644 (file)
@@ -25,7 +25,7 @@ module PatSyn (
 #include "HsVersions.h"
 
 import Type
-import TcType( mkInvSigmaTy )
+import TcType( mkSpecSigmaTy )
 import Name
 import Outputable
 import Unique
@@ -328,8 +328,8 @@ patSynType :: PatSyn -> Type
 patSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
                      , psExTyVars   = ex_tvs,   psProvTheta = prov_theta
                      , psArgs = orig_args, psOrigResTy = orig_res_ty })
-  = mkInvSigmaTy univ_tvs req_theta $
-    mkInvSigmaTy ex_tvs prov_theta $
+  = mkSpecSigmaTy univ_tvs req_theta $  -- use mkSpecSigmaTy because it
+    mkSpecSigmaTy ex_tvs prov_theta $   -- prints better
     mkFunTys orig_args orig_res_ty
 
 -- | Should the 'PatSyn' be presented infix?
index 07db78a..2f1b67f 100644 (file)
@@ -62,7 +62,7 @@ import TysWiredIn
 import PrelNames
 
 import HsUtils          ( mkChunkified, chunkify )
-import TcType           ( mkInvSigmaTy )
+import TcType           ( mkSpecSigmaTy )
 import Type
 import Coercion         ( isCoVar )
 import TysPrim
@@ -684,8 +684,8 @@ mkRuntimeErrorId name = pc_bottoming_Id1 name runtimeErrorTy
 
 runtimeErrorTy :: Type
 -- The runtime error Ids take a UTF8-encoded string as argument
-runtimeErrorTy = mkInvSigmaTy [levity1TyVar, openAlphaTyVar] []
-                              (mkFunTy addrPrimTy openAlphaTy)
+runtimeErrorTy = mkSpecSigmaTy [levity1TyVar, openAlphaTyVar] []
+                               (mkFunTy addrPrimTy openAlphaTy)
 
 errorName :: Name
 errorName = mkWiredInIdName gHC_ERR (fsLit "error") errorIdKey eRROR_ID
@@ -694,7 +694,7 @@ eRROR_ID :: Id
 eRROR_ID = pc_bottoming_Id2 errorName errorTy
 
 errorTy  :: Type   -- See Note [Error and friends have an "open-tyvar" forall]
-errorTy  = mkInvSigmaTy [levity1TyVar, openAlphaTyVar] []
+errorTy  = mkSpecSigmaTy [levity1TyVar, openAlphaTyVar] []
              (mkFunTys [ mkClassPred
                            ipClass
                            [ mkStrLitTy (fsLit "callStack")
@@ -709,7 +709,7 @@ uNDEFINED_ID :: Id
 uNDEFINED_ID = pc_bottoming_Id1 undefinedName undefinedTy
 
 undefinedTy  :: Type   -- See Note [Error and friends have an "open-tyvar" forall]
-undefinedTy  = mkInvSigmaTy [levity1TyVar, openAlphaTyVar] []
+undefinedTy  = mkSpecSigmaTy [levity1TyVar, openAlphaTyVar] []
                  (mkFunTy (mkClassPred
                              ipClass
                              [ mkStrLitTy (fsLit "callStack")
@@ -727,7 +727,7 @@ Notice the levity polymophism. This ensures that
   * unboxed as well as boxed types
   * polymorphic types
 This is OK because it never returns, so the return type is irrelevant.
-See Note [Sort-polymorphic tyvars accept foralls] in TcUnify.
+See Note [Sort-polymorphic tyvars accept foralls] in TcMType.
 
 
 ************************************************************************
index 57d77c7..2711925 100644 (file)
@@ -632,7 +632,7 @@ addTickHsExpr (ExprWithTySigOut e ty) =
                (addTickLHsExprNever e) -- No need to tick the inner expression
                (return ty)             -- for expressions with signatures
 
-addTickHsExpr e@(HsType _) = return e
+addTickHsExpr e@(HsTypeOut _) = return e
 
 -- Others should never happen in expression content.
 addTickHsExpr e  = pprPanic "addTickHsExpr" (ppr e)
@@ -870,8 +870,8 @@ addTickHsCmd (HsCmdArrForm e fix cmdtop) =
                (return fix)
                (mapM (liftL (addTickHsCmdTop)) cmdtop)
 
-addTickHsCmd (HsCmdCast co cmd)
-  = liftM2 HsCmdCast (return co) (addTickHsCmd cmd)
+addTickHsCmd (HsCmdWrap w cmd)
+  = liftM2 HsCmdWrap (return w) (addTickHsCmd cmd)
 
 -- Others should never happen in a command context.
 --addTickHsCmd e  = pprPanic "addTickHsCmd" (ppr e)
index 56c44c5..cc831d7 100644 (file)
@@ -614,9 +614,9 @@ dsCmd _ids local_vars _stack_ty _res_ty (HsCmdArrForm op _ args) env_ids = do
     return (mkApps (App core_op (Type env_ty)) core_args,
             unionVarSets fv_sets)
 
-dsCmd ids local_vars stack_ty res_ty (HsCmdCast coercion cmd) env_ids = do
+dsCmd ids local_vars stack_ty res_ty (HsCmdWrap wrap cmd) env_ids = do
     (core_cmd, env_ids') <- dsCmd ids local_vars stack_ty res_ty cmd env_ids
-    wrapped_cmd <- dsHsWrapper (mkWpCastN coercion) core_cmd
+    wrapped_cmd <- dsHsWrapper wrap core_cmd
     return (wrapped_cmd, env_ids')
 
 dsCmd _ _ _ _ _ c = pprPanic "dsCmd" (ppr c)
index 7bc12cb..a79e9fa 100644 (file)
@@ -160,20 +160,23 @@ dsHsBind dflags
          (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
                    , abs_exports = [export]
                    , abs_ev_binds = ev_binds, abs_binds = binds })
-  | ABE { abe_wrap = wrap, abe_poly = global
+  | ABE { abe_inst_wrap = inst_wrap, abe_wrap = wrap, abe_poly = global
         , abe_mono = local, abe_prags = prags } <- export
   , not (xopt LangExt.Strict dflags)             -- handle strict binds
   , not (anyBag (isBangedPatBind . unLoc) binds) -- in the next case
   = -- push type constraints deeper for pattern match check
+    -- See Note [AbsBinds wrappers] in HsBinds
     addDictsDs (toTcTypeBag (listToBag dicts)) $
      do { (_, bind_prs) <- ds_lhs_binds binds
         ; let core_bind = Rec bind_prs
         ; ds_binds <- dsTcEvBinds_s ev_binds
+        ; inner_rhs <- dsHsWrapper inst_wrap $
+                       Let core_bind $
+                       Var local
         ; rhs <- dsHsWrapper wrap $  -- Usually the identity
                  mkLams tyvars $ mkLams dicts $
                  mkCoreLets ds_binds $
-                 Let core_bind $
-                 Var local
+                 inner_rhs
 
         ; (spec_binds, rules) <- dsSpecs rhs prags
 
@@ -212,13 +215,17 @@ dsHsBind dflags
         -- Note [Desugar Strict binds]
         ; (exported_force_vars, extra_exports) <- get_exports local_force_vars
 
-        ; let mk_bind (ABE { abe_wrap = wrap, abe_poly = global
+        ; let mk_bind (ABE { abe_inst_wrap = inst_wrap, abe_wrap = wrap
+                           , abe_poly = global
                            , abe_mono = local, abe_prags = spec_prags })
+                         -- See Note [AbsBinds wrappers] in HsBinds
                 = do { tup_id  <- newSysLocalDs tup_ty
+                     ; inner_rhs <- dsHsWrapper inst_wrap $
+                                    mkTupleSelector all_locals local tup_id $
+                                    mkVarApps (Var poly_tup_id) (tyvars ++ dicts)
                      ; rhs <- dsHsWrapper wrap $
-                                 mkLams tyvars $ mkLams dicts $
-                                 mkTupleSelector all_locals local tup_id $
-                                 mkVarApps (Var poly_tup_id) (tyvars ++ dicts)
+                              mkLams tyvars $ mkLams dicts $
+                              inner_rhs
                      ; let rhs_for_spec = Let (NonRec poly_tup_id poly_tup_rhs) rhs
                      ; (spec_binds, rules) <- dsSpecs rhs_for_spec spec_prags
                      ; let global' = (global `setInlinePragma` defaultInlinePragma)
@@ -277,6 +284,7 @@ dsHsBind dflags
          return (ABE {abe_poly = global
                      ,abe_mono = local
                      ,abe_wrap = WpHole
+                     ,abe_inst_wrap = WpHole
                      ,abe_prags = SpecPrags []})
 
 dsHsBind _ (PatSynBind{}) = panic "dsHsBind: PatSynBind"
@@ -963,10 +971,10 @@ dsHsWrapper (WpLet ev_binds)  e = do bs <- dsTcEvBinds ev_binds
                                      return (mkCoreLets bs 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 (mkCoreAppDs (text "dsHsWrapper") e e1)
-                                      ; return (Lam x e2) }
+dsHsWrapper (WpFun c1 c2 t1 e = do { x <- newSysLocalDs t1
+                                     ; e1 <- dsHsWrapper c1 (Var x)
+                                     ; e2 <- dsHsWrapper c2 (mkCoreAppDs (text "dsHsWrapper") e e1)
+                                     ; return (Lam x e2) }
 dsHsWrapper (WpCast co)       e = ASSERT(coercionRole co == Representational)
                                   return $ mkCastDs e co
 dsHsWrapper (WpEvLam ev)      e = return $ Lam ev e
index 3b9a4cf..999b945 100644 (file)
@@ -222,7 +222,10 @@ dsExpr (HsLamCase arg matches)
        ; return $ Lam arg_var $ bindNonRec discrim_var (Var arg_var) matching_code }
 
 dsExpr e@(HsApp fun arg)
-  = mkCoreAppDs (text "HsApp" <+> ppr e) <$> dsLExpr fun <*>  dsLExpr arg
+    -- ignore type arguments here; they're in the wrappers instead at this point
+  | isLHsTypeExpr arg = dsLExpr fun
+  | otherwise         = mkCoreAppDs (text "HsApp" <+> ppr e)
+                        <$> dsLExpr fun <*>  dsLExpr arg
 
 
 {-
@@ -718,7 +721,8 @@ dsExpr (EWildPat      {})  = panic "dsExpr:EWildPat"
 dsExpr (EAsPat        {})  = panic "dsExpr:EAsPat"
 dsExpr (EViewPat      {})  = panic "dsExpr:EViewPat"
 dsExpr (ELazyPat      {})  = panic "dsExpr:ELazyPat"
-dsExpr (HsType        {})  = panic "dsExpr:HsType"
+dsExpr (HsType        {})  = panic "dsExpr:HsType" -- removed by typechecker
+dsExpr (HsTypeOut     {})  = panic "dsExpr:HsTypeOut" -- handled in HsApp case
 dsExpr (HsDo          {})  = panic "dsExpr:HsDo"
 dsExpr (HsRecFld      {})  = panic "dsExpr:HsRecFld"
 
index b5a50e7..7530a0a 100644 (file)
@@ -956,7 +956,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 (WpFun w1 w2 _)   (WpFun w1' w2' _)   = wrap w1 w1' && wrap w2 w2'
     wrap (WpCast co)       (WpCast co')        = co `eqCoercion` co'
     wrap (WpEvApp et1)     (WpEvApp et2)       = et1 `ev_term` et2
     wrap (WpTyApp t)       (WpTyApp t')        = eqType t t'
index 7a11463..93dc5a9 100644 (file)
@@ -236,11 +236,13 @@ deriving instance (DataId idL, DataId idR)
         -- See Note [AbsBinds]
 
 data ABExport id
-  = ABE { abe_poly  :: id           -- ^ Any INLINE pragmas is attached to this Id
-        , abe_mono  :: id
-        , abe_wrap  :: HsWrapper    -- ^ See Note [AbsBinds wrappers]
-             -- Shape: (forall abs_tvs. abs_ev_vars => abe_mono) ~ abe_poly
-        , abe_prags :: TcSpecPrags  -- ^ SPECIALISE pragmas
+  = ABE { abe_poly      :: id    -- ^ Any INLINE pragmas is attached to this Id
+        , abe_mono      :: id
+        , abe_inst_wrap :: HsWrapper    -- ^ See Note [AbsBinds wrappers]
+             -- ^ Shape: abe_mono ~ abe_insted
+        , abe_wrap      :: HsWrapper    -- ^ See Note [AbsBinds wrappers]
+             -- Shape: (forall abs_tvs. abs_ev_vars => abe_insted) ~ abe_poly
+        , abe_prags     :: TcSpecPrags  -- ^ SPECIALISE pragmas
   } deriving (Data, Typeable)
 
 -- | - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnPattern',
@@ -375,6 +377,27 @@ The abe_wrap field deals with impedance-matching between
 and the thing we really want, which may have fewer type
 variables.  The action happens in TcBinds.mkExport.
 
+For abe_inst_wrap, consider this:
+  x = (*)
+The abe_mono type will be  forall a. Num a => a -> a -> a
+because no instantiation happens during typechecking. Before inferring
+a final type, we must instantiate this. See Note [Instantiate when inferring
+a type] in TcBinds. The abe_inst_wrap takes the uninstantiated abe_mono type
+to a proper instantiated type. In this case, the "abe_insted" is
+(b -> b -> b). Note that the value of "abe_insted" isn't important; it's
+just an intermediate form as we're going from abe_mono to abe_poly. See also
+the desugaring code in DsBinds.
+
+It's conceivable that we could combine the two wrappers, but note that there
+is a gap: neither wrapper tacks on the tvs and dicts from the outer AbsBinds.
+These bits are added manually in desugaring. (See DsBinds.dsHsBind.) A problem
+that would arise in combining them is that zonking becomes more challenging:
+we want to zonk the tvs and dicts in the AbsBinds, but then we end up re-zonking
+when we zonk the ABExport. And -- worse -- the combined wrapper would have
+the tvs and dicts in binding positions, so they would shadow the original
+tvs and dicts. This is all resolvable with some plumbing, but it seems simpler
+just to keep the two wrappers distinct.
+
 Note [Bind free vars]
 ~~~~~~~~~~~~~~~~~~~~~
 The bind_fvs field of FunBind and PatBind records the free variables
@@ -548,10 +571,12 @@ ppr_monobind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dictvars
       pprLHsBinds val_binds
 
 instance (OutputableBndr id) => Outputable (ABExport id) where
-  ppr (ABE { abe_wrap = wrap, abe_poly = gbl, abe_mono = lcl, abe_prags = prags })
+  ppr (ABE { abe_wrap = wrap, abe_inst_wrap = inst_wrap
+           , abe_poly = gbl, abe_mono = lcl, abe_prags = prags })
     = vcat [ ppr gbl <+> ptext (sLit "<=") <+> ppr lcl
            , nest 2 (pprTcSpecPrags prags)
-           , nest 2 (ppr wrap)]
+           , nest 2 (ppr wrap)
+           , nest 2 (ppr inst_wrap)]
 
 instance (OutputableBndr idL, OutputableBndr idR) => Outputable (PatSynBind idL idR) where
   ppr (PSB{ psb_id = L _ psyn, psb_args = details, psb_def = pat, psb_dir = dir })
index 6e02df7..158993e 100644 (file)
@@ -502,7 +502,14 @@ data HsExpr id
   -- For details on above see note [Api annotations] in ApiAnnotation
   | ELazyPat    (LHsExpr id) -- ~ pattern
 
-  | HsType      (LHsType id) -- Explicit type argument; e.g  f {| Int |} x y
+  -- | Use for type application in expressions.
+  -- 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnAt'
+
+  -- For details on above see note [Api annotations] in ApiAnnotation
+  | HsType      (LHsWcType id) -- Explicit type argument; e.g  f @Int x y
+                               -- NB: Has wildcards, but no implicit quant.
+
+  | HsTypeOut   (LHsWcType Name)  -- just for pretty-printing
 
   ---------------------------------------
   -- Finally, HsWrap appears only in typechecker output
@@ -762,7 +769,10 @@ ppr_expr (HsSCC _ (StringLiteral _ lbl) expr)
           pprParendExpr expr ]
 
 ppr_expr (HsWrap co_fn e) = pprHsWrapper (pprExpr e) co_fn
-ppr_expr (HsType id)      = ppr id
+ppr_expr (HsType (HsWC { hswc_body = ty }))
+  = char '@' <> pprParendHsType (unLoc ty)
+ppr_expr (HsTypeOut (HsWC { hswc_body = ty }))
+  = char '@' <> pprParendHsType (unLoc ty)
 
 ppr_expr (HsSpliceE s)         = pprSplice s
 ppr_expr (HsBracket b)         = pprHsBracket b
@@ -864,6 +874,8 @@ hsExprNeedsParens (HsTcBracketOut {}) = False
 hsExprNeedsParens (HsDo sc _ _)
        | isListCompExpr sc            = False
 hsExprNeedsParens (HsRecFld{})        = False
+hsExprNeedsParens (HsType {})         = False
+hsExprNeedsParens (HsTypeOut {})      = False
 hsExprNeedsParens _ = True
 
 
@@ -970,10 +982,10 @@ data HsCmd id
 
     -- For details on above see note [Api annotations] in ApiAnnotation
 
-  | HsCmdCast   TcCoercionN    -- A simpler version of HsWrap in HsExpr
+  | HsCmdWrap   HsWrapper
                 (HsCmd id)     -- If   cmd :: arg1 --> res
-                               --       co :: arg1 ~ arg2
-                               -- Then (HsCmdCast co cmd) :: arg2 --> res
+                               --      wrap :: arg1 "->" arg2
+                               -- Then (HsCmdWrap wrap cmd) :: arg2 --> res
   deriving (Typeable)
 deriving instance (DataId id) => Data (HsCmd id)
 
@@ -1054,9 +1066,9 @@ ppr_cmd (HsCmdLet (L _ binds) cmd)
   = sep [hang (ptext (sLit "let")) 2 (pprBinds binds),
          hang (ptext (sLit "in"))  2 (ppr cmd)]
 
-ppr_cmd (HsCmdDo (L  _ stmts) _)  = pprDo ArrowExpr stmts
-ppr_cmd (HsCmdCast co cmd) = sep [ ppr_cmd cmd
-                                 , ptext (sLit "|>") <+> ppr co ]
+ppr_cmd (HsCmdDo (L _ stmts) _)  = pprDo ArrowExpr stmts
+
+ppr_cmd (HsCmdWrap w cmd) = pprHsWrapper (ppr_cmd cmd) w
 
 ppr_cmd (HsCmdArrApp arrow arg _ HsFirstOrderApp True)
   = hsep [ppr_lexpr arrow, larrowt, ppr_lexpr arg]
@@ -1186,6 +1198,13 @@ isInfixMatch match = case m_fixity match of
 isEmptyMatchGroup :: MatchGroup id body -> Bool
 isEmptyMatchGroup (MG { mg_alts = ms }) = null $ unLoc ms
 
+-- | Is there only one RHS in this group?
+isSingletonMatchGroup :: MatchGroup id body -> Bool
+isSingletonMatchGroup (MG { mg_alts = L _ [match] })
+  | L _ (Match { m_grhss = GRHSs { grhssGRHSs = [_] } }) <- match
+  = True
+isSingletonMatchGroup _ = False
+
 matchGroupArity :: MatchGroup id body -> Arity
 -- Precondition: MatchGroup is non-empty
 -- This is called before type checking, when mg_arg_tys is not set
index 9e8ea9a..9576197 100644 (file)
@@ -25,7 +25,7 @@ module HsUtils(
   mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo,
   mkHsDictLet, mkHsLams,
   mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo,
-  mkLHsPar, mkHsCmdCast,
+  mkLHsPar, mkHsCmdWrap, mkLHsCmdWrap, isLHsTypeExpr_maybe, isLHsTypeExpr,
 
   nlHsTyApp, nlHsTyApps, nlHsVar, nlHsLit, nlHsApp, nlHsApps, nlHsIntLit, nlHsVarApps,
   nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList,
@@ -445,6 +445,21 @@ nlHsFunTy a b           = noLoc (HsFunTy a b)
 nlHsTyConApp :: name -> [LHsType name] -> LHsType name
 nlHsTyConApp tycon tys  = foldl nlHsAppTy (nlHsTyVar tycon) tys
 
+-- | Extract a type argument from an HsExpr, with the list of wildcards in
+-- the type
+isLHsTypeExpr_maybe :: LHsExpr name -> Maybe (LHsWcType name)
+isLHsTypeExpr_maybe (L _ (HsPar e))       = isLHsTypeExpr_maybe e
+isLHsTypeExpr_maybe (L _ (HsType ty))     = Just ty
+  -- the HsTypeOut case is ill-typed. We never need it here anyway.
+isLHsTypeExpr_maybe _                     = Nothing
+
+-- | Is an expression a visible type application?
+isLHsTypeExpr :: LHsExpr name -> Bool
+isLHsTypeExpr (L _ (HsPar e))     = isLHsTypeExpr e
+isLHsTypeExpr (L _ (HsType _))    = True
+isLHsTypeExpr (L _ (HsTypeOut _)) = True
+isLHsTypeExpr _                   = False
+
 {-
 Tuples.  All these functions are *pre-typechecker* because they lack
 types on the tuple.
@@ -609,9 +624,12 @@ mkHsWrapCoR co e = mkHsWrap (mkWpCastR co) e
 mkLHsWrapCo :: TcCoercionN -> LHsExpr id -> LHsExpr id
 mkLHsWrapCo co (L loc e) = L loc (mkHsWrapCo co e)
 
-mkHsCmdCast :: TcCoercion -> HsCmd id -> HsCmd id
-mkHsCmdCast co cmd | isTcReflCo co = cmd
-                   | otherwise     = HsCmdCast co cmd
+mkHsCmdWrap :: HsWrapper -> HsCmd id -> HsCmd id
+mkHsCmdWrap w cmd | isIdHsWrapper w = cmd
+                  | otherwise       = HsCmdWrap w cmd
+
+mkLHsCmdWrap :: HsWrapper -> LHsCmd id -> LHsCmd id
+mkLHsCmdWrap w (L loc c) = L loc (mkHsCmdWrap w c)
 
 mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
 mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
index 8e3b9a3..004f465 100644 (file)
@@ -15,9 +15,9 @@ import RdrName
 import Var
 import Coercion
 import {-# SOURCE #-} ConLike (ConLike)
-import TcEvidence (HsWrapper)
 import FieldLabel
 import SrcLoc (Located)
+import TcEvidence ( HsWrapper )
 
 import Data.Data hiding ( Fixity )
 import BasicTypes       (Fixity)
@@ -65,6 +65,9 @@ placeHolderNames = PlaceHolder
 placeHolderNamesTc :: NameSet
 placeHolderNamesTc = emptyNameSet
 
+placeHolderHsWrapper :: PlaceHolder
+placeHolderHsWrapper = PlaceHolder
+
 {-
 
 Note [Pass sensitive types]
index 503653d..6f26e23 100644 (file)
@@ -963,7 +963,7 @@ ppr_rough Nothing   = dot
 ppr_rough (Just tc) = ppr tc
 
 tv_to_forall_bndr :: IfaceTvBndr -> IfaceForAllBndr
-tv_to_forall_bndr tv = IfaceTv tv Invisible
+tv_to_forall_bndr tv = IfaceTv tv Specified
 
 {-
 Note [Result type of a data family GADT]
index 640d104..154b7c4 100644 (file)
@@ -696,8 +696,9 @@ pprIfaceForAll bndrs@(IfaceTv _ vis : _)
     (bndrs', doc) = ppr_itv_bndrs bndrs vis
 
     add_separator stuff = case vis of
-                            Invisible -> stuff <>  dot
                             Visible   -> stuff <+> arrow
+                            _inv      -> stuff <>  dot
+
 
 -- | Render the ... in @(forall ... .)@ or @(forall ... ->)@.
 -- Returns both the list of not-yet-rendered binders and the doc.
@@ -705,9 +706,9 @@ pprIfaceForAll bndrs@(IfaceTv _ vis : _)
 ppr_itv_bndrs :: [IfaceForAllBndr]
              -> VisibilityFlag  -- ^ visibility of the first binder in the list
              -> ([IfaceForAllBndr], SDoc)
-ppr_itv_bndrs all_bndrs@(IfaceTv tv vis : bndrs) vis1
-  | vis == vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
-                  (bndrs', pprIfaceTvBndr tv <+> doc)
+ppr_itv_bndrs all_bndrs@(bndr@(IfaceTv _ vis) : bndrs) vis1
+  | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
+                         (bndrs', pprIfaceForAllBndr bndr <+> doc)
   | otherwise   = (all_bndrs, empty)
 ppr_itv_bndrs [] _ = ([], empty)
 
@@ -719,7 +720,11 @@ pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
 
 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
-pprIfaceForAllBndr (IfaceTv tv _) = pprIfaceTvBndr tv
+pprIfaceForAllBndr (IfaceTv tv Invisible) = sdocWithDynFlags $ \dflags ->
+                                            if gopt Opt_PrintExplicitForalls dflags
+                                            then braces $ pprIfaceTvBndr tv
+                                            else pprIfaceTvBndr tv
+pprIfaceForAllBndr (IfaceTv tv _)         = pprIfaceTvBndr tv
 
 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
 pprIfaceForAllCoBndr (tv, kind_co)
index 5efe8b3..55260db 100644 (file)
@@ -3210,6 +3210,7 @@ xFlags = [
   flagSpec "TraditionalRecordSyntax"          LangExt.TraditionalRecordSyntax,
   flagSpec "TransformListComp"                LangExt.TransformListComp,
   flagSpec "TupleSections"                    LangExt.TupleSections,
+  flagSpec "TypeApplications"                 LangExt.TypeApplications,
   flagSpec "TypeInType"                       LangExt.TypeInType,
   flagSpec "TypeFamilies"                     LangExt.TypeFamilies,
   flagSpec "TypeOperators"                    LangExt.TypeOperators,
@@ -3324,6 +3325,7 @@ impliedXFlags
 
     , (LangExt.TemplateHaskell, turnOn, LangExt.TemplateHaskellQuotes)
     , (LangExt.Strict, turnOn, LangExt.StrictData)
+    , (LangExt.TypeApplications, turnOn, LangExt.AllowAmbiguousTypes)
   ]
 
 -- Note [Documenting optimisation flags]
index 365a57c..d55b508 100644 (file)
@@ -147,18 +147,10 @@ ppr_ty_thing hdr_only path ty_thing
                  -- Nothing is unexpected here; TyThings have External names
 
 pprTypeForUser :: Type -> SDoc
--- We do two things here.
--- a) We tidy the type, regardless
--- b) Swizzle the foralls to the top, so that without
---    -fprint-explicit-foralls we'll suppress all the foralls
--- Prime example: a class op might have type
---      forall a. C a => forall b. Ord b => stuff
--- Then we want to display
---      (C a, Ord b) => stuff
+-- The type is tidied
 pprTypeForUser ty
-  = pprSigmaType (mkInvSigmaTy tvs ctxt tau)
+  = pprSigmaType tidy_ty
   where
-    (tvs, ctxt, tau) = tcSplitSigmaTy tidy_ty
     (_, tidy_ty)     = tidyOpenType emptyTidyEnv ty
      -- Often the types/kinds we print in ghci are fully generalised
      -- and have no free variables, but it turns out that we sometimes
index cee8540..1bbbfbf 100644 (file)
@@ -394,6 +394,14 @@ $tab          { warnTab }
                      { lex_qquasiquote_tok }
 }
 
+  -- See Note [Lexing type applications]
+<0> {
+    [^ $idchar \) ] ^
+  "@"
+    / { ifExtension typeApplicationEnabled `alexAndPred` notFollowedBySymbol }
+    { token ITtypeApp }
+}
+
 <0> {
   "(|" / { ifExtension arrowsEnabled `alexAndPred` notFollowedBySymbol }
                                         { special IToparenbar }
@@ -507,6 +515,32 @@ $tab          { warnTab }
   \"                            { lex_string_tok }
 }
 
+-- Note [Lexing type applications]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- The desired syntax for type applications is to prefix the type application
+-- with '@', like this:
+--
+--   foo @Int @Bool baz bum
+--
+-- This, of course, conflicts with as-patterns. The conflict arises because
+-- expressions and patterns use the same parser, and also because we want
+-- to allow type patterns within expression patterns.
+--
+-- Disambiguation is accomplished by requiring *something* to appear betwen
+-- type application and the preceding token. This something must end with
+-- a character that cannot be the end of the variable bound in an as-pattern.
+-- Currently (June 2015), this means that the something cannot end with a
+-- $idchar or a close-paren. (The close-paren is necessary if the as-bound
+-- identifier is symbolic.)
+--
+-- Note that looking for whitespace before the '@' is insufficient, because
+-- of this pathological case:
+--
+--   foo {- hi -}@Int
+--
+-- This design is predicated on the fact that as-patterns are generally
+-- whitespace-free, and also that this whole thing is opt-in, with the
+-- TypeApplications extension.
 
 -- -----------------------------------------------------------------------------
 -- Alex "Haskell code fragment bottom"
@@ -686,8 +720,13 @@ data Token
   | ITLarrowtail IsUnicodeSyntax --  -<<
   | ITRarrowtail IsUnicodeSyntax --  >>-
 
-  | ITunknown String             -- Used when the lexer can't make sense of it
-  | ITeof                        -- end of file token
+  -- type application '@' (lexed differently than as-pattern '@',
+  -- due to checking for preceding whitespace)
+  | ITtypeApp
+
+
+  | ITunknown String            -- Used when the lexer can't make sense of it
+  | ITeof                       -- end of file token
 
   -- Documentation annotations
   | ITdocCommentNext  String     -- something beginning '-- |'
@@ -2023,6 +2062,7 @@ data ExtBits
   | LambdaCaseBit
   | BinaryLiteralsBit
   | NegativeLiteralsBit
+  | TypeApplicationsBit
   deriving Enum
 
 
@@ -2083,6 +2123,8 @@ negativeLiteralsEnabled :: ExtsBitmap -> Bool
 negativeLiteralsEnabled = xtest NegativeLiteralsBit
 patternSynonymsEnabled :: ExtsBitmap -> Bool
 patternSynonymsEnabled = xtest PatternSynonymsBit
+typeApplicationEnabled :: ExtsBitmap -> Bool
+typeApplicationEnabled = xtest TypeApplicationsBit
 
 -- PState for parsing options pragmas
 --
@@ -2153,6 +2195,8 @@ mkPState flags buf loc =
                .|. BinaryLiteralsBit           `setBitIf` xopt LangExt.BinaryLiterals           flags
                .|. NegativeLiteralsBit         `setBitIf` xopt LangExt.NegativeLiterals         flags
                .|. PatternSynonymsBit          `setBitIf` xopt LangExt.PatternSynonyms          flags
+               .|. TypeApplicationsBit         `setBitIf` xopt LangExt.TypeApplications         flags
+
       --
       setBitIf :: ExtBits -> Bool -> ExtsBitmap
       b `setBitIf` cond | cond      = xbit b
index ead81ac..11dc84f 100644 (file)
@@ -414,6 +414,7 @@ output it generates.
  '-<<'          { L _ (ITLarrowtail _) }            -- for arrow notation
  '>>-'          { L _ (ITRarrowtail _) }            -- for arrow notation
  '.'            { L _ ITdot }
+ TYPEAPP        { L _ ITtypeApp }
 
  '{'            { L _ ITocurly }                        -- special symbols
  '}'            { L _ ITccurly }
@@ -2237,7 +2238,11 @@ fexp    :: { LHsExpr RdrName }
 
 aexp    :: { LHsExpr RdrName }
         : qvar '@' aexp         {% ams (sLL $1 $> $ EAsPat $1 $3) [mj AnnAt $2] }
+            -- If you change the parsing, make sure to understand
+            -- Note [Lexing type applications] in Lexer.x
+
         | '~' aexp              {% ams (sLL $1 $> $ ELazyPat $2) [mj AnnTilde $1] }
+        | TYPEAPP atype         {% ams (sLL $1 $> $ HsType (mkHsWildCardBndrs $2)) [mj AnnAt $1] }
         | aexp1                 { $1 }
 
 aexp1   :: { LHsExpr RdrName }
@@ -2954,6 +2959,10 @@ var     :: { Located RdrName }
         | '(' varsym ')'        {% ams (sLL $1 $> (unLoc $2))
                                        [mop $1,mj AnnVal $2,mcp $3] }
 
+ -- Lexing type applications depends subtly on what characters can possibly
+ -- end a qvar. Currently (June 2015), only $idchars and ")" can end a qvar.
+ -- If you're changing this, please see Note [Lexing type applications] in
+ -- Lexer.x.
 qvar    :: { Located RdrName }
         : qvarid                { $1 }
         | '(' varsym ')'        {% ams (sLL $1 $> (unLoc $2))
index 67a44cc..66172ac 100644 (file)
@@ -536,7 +536,7 @@ primOpType op
     Compare _occ ty -> compare_fun_ty ty
 
     GenPrimOp _occ tyvars arg_tys res_ty ->
-        mkInvForAllTys tyvars (mkFunTys arg_tys res_ty)
+        mkSpecForAllTys tyvars (mkFunTys arg_tys res_ty)
 
 primOpOcc :: PrimOp -> OccName
 primOpOcc op = case primOpInfo op of
index a4715df..1450585 100644 (file)
@@ -648,7 +648,7 @@ mkProxyPrimTy k ty = TyConApp proxyPrimTyCon [k, ty]
 
 proxyPrimTyCon :: TyCon
 proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep
-  where kind = ForAllTy (Named kv Invisible) $
+  where kind = ForAllTy (Named kv Specified) $
                mkFunTy k unliftedTypeKind
         kv   = kKiVar
         k    = mkTyVarTy kv
@@ -664,8 +664,8 @@ proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep
 eqPrimTyCon :: TyCon  -- The representation type for equality predicates
                       -- See Note [The equality types story]
 eqPrimTyCon  = mkPrimTyCon eqPrimTyConName kind roles VoidRep
-  where kind = ForAllTy (Named kv1 Invisible) $
-               ForAllTy (Named kv2 Invisible) $
+  where kind = ForAllTy (Named kv1 Specified) $
+               ForAllTy (Named kv2 Specified) $
                mkFunTys [k1, k2] unliftedTypeKind
         [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
         k1 = mkTyVarTy kv1
@@ -678,8 +678,8 @@ eqPrimTyCon  = mkPrimTyCon eqPrimTyConName kind roles VoidRep
 eqReprPrimTyCon :: TyCon   -- See Note [The equality types story]
 eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName kind
                               roles VoidRep
-  where kind = ForAllTy (Named kv1 Invisible) $
-               ForAllTy (Named kv2 Invisible) $
+  where kind = ForAllTy (Named kv1 Specified) $
+               ForAllTy (Named kv2 Specified) $
                mkFunTys [k1, k2] unliftedTypeKind
         [kv1, kv2]    = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
         k1            = mkTyVarTy kv1
@@ -693,8 +693,8 @@ eqPhantPrimTyCon :: TyCon
 eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName kind
                                [Nominal, Nominal, Phantom, Phantom]
                                VoidRep
-  where kind = ForAllTy (Named kv1 Invisible) $
-               ForAllTy (Named kv2 Invisible) $
+  where kind = ForAllTy (Named kv1 Specified) $
+               ForAllTy (Named kv2 Specified) $
                mkFunTys [k1, k2] unliftedTypeKind
         [kv1, kv2]    = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
         k1            = mkTyVarTy kv1
@@ -925,7 +925,7 @@ anyTyCon = mkFamilyTyCon anyTyConName kind [kKiVar] Nothing
                          Nothing
                          NotInjective
   where
-    kind = ForAllTy (Named kKiVar Invisible) (mkTyVarTy kKiVar)
+    kind = ForAllTy (Named kKiVar Specified) (mkTyVarTy kKiVar)
 
 anyTypeOfKind :: Kind -> Type
 anyTypeOfKind kind = TyConApp anyTyCon [kind]
index 3c3eab6..02e693d 100644 (file)
@@ -573,7 +573,7 @@ mk_tuple boxity arity = (tycon, tuple_con)
             in
             ( UnboxedTuple
             , gHC_PRIM
-            , mkInvForAllTys lev_tvs $
+            , mkSpecForAllTys lev_tvs $
               mkFunTys (map tyVarKind open_tvs) $
               unliftedTypeKind
             , arity * 2
@@ -633,7 +633,7 @@ heqSCSelId, coercibleSCSelId :: Id
     klass     = mkClass tvs [] [sc_pred] [sc_sel_id] [] [] (mkAnd []) tycon
     datacon   = pcDataCon heqDataConName tvs [sc_pred] tycon
 
-    kind      = mkInvForAllTys [kv1, kv2] $ mkFunTys [k1, k2] constraintKind
+    kind      = mkSpecForAllTys [kv1, kv2] $ mkFunTys [k1, k2] constraintKind
     kv1:kv2:_ = drop 9 alphaTyVars -- gets "j" and "k"
     k1        = mkTyVarTy kv1
     k2        = mkTyVarTy kv2
@@ -654,7 +654,7 @@ heqSCSelId, coercibleSCSelId :: Id
     klass     = mkClass tvs [] [sc_pred] [sc_sel_id] [] [] (mkAnd []) tycon
     datacon   = pcDataCon coercibleDataConName tvs [sc_pred] tycon
 
-    kind      = mkInvForAllTys [kKiVar] $ mkFunTys [k, k] constraintKind
+    kind      = mkSpecForAllTys [kKiVar] $ mkFunTys [k, k] constraintKind
     k         = mkTyVarTy kKiVar
     [av,bv]   = mkTemplateTyVars [k, k]
     tvs       = [kKiVar, av, bv]
index c4e5bb2..03f4b62 100644 (file)
@@ -298,9 +298,9 @@ rnExpr (HsMultiIf _ty alts)
        -- ; return (HsMultiIf ty alts', fvs) }
        ; return (HsMultiIf placeHolderType alts', fvs) }
 
-rnExpr (HsType a)
-  = do { (t, fvT) <- rnLHsType HsTypeCtx a
-       ; return (HsType t, fvT) }
+rnExpr (HsType ty)
+  = do { (ty', fvT) <- rnHsWcType HsTypeCtx ty
+       ; return (HsType ty', fvT) }
 
 rnExpr (ArithSeq _ _ seq)
   = do { opt_OverloadedLists <- xoptM LangExt.OverloadedLists
@@ -524,7 +524,7 @@ rnCmd (HsCmdDo (L l stmts) _)
             rnStmts ArrowExpr rnLCmd stmts (\ _ -> return ((), emptyFVs))
         ; return ( HsCmdDo (L l stmts') placeHolderType, fvs ) }
 
-rnCmd cmd@(HsCmdCast {}) = pprPanic "rnCmd" (ppr cmd)
+rnCmd cmd@(HsCmdWrap {}) = pprPanic "rnCmd" (ppr cmd)
 
 ---------------------------------------------------
 type CmdNeeds = FreeVars        -- Only inhabitants are
@@ -541,7 +541,7 @@ methodNamesCmd (HsCmdArrApp _arrow _arg _ HsFirstOrderApp _rtl)
 methodNamesCmd (HsCmdArrApp _arrow _arg _ HsHigherOrderApp _rtl)
   = unitFV appAName
 methodNamesCmd (HsCmdArrForm {}) = emptyFVs
-methodNamesCmd (HsCmdCast _ cmd) = methodNamesCmd cmd
+methodNamesCmd (HsCmdWrap _ cmd) = methodNamesCmd cmd
 
 methodNamesCmd (HsCmdPar c) = methodNamesLCmd c
 
@@ -1819,7 +1819,8 @@ sectionErr expr
 
 patSynErr :: HsExpr RdrName -> RnM (HsExpr Name, FreeVars)
 patSynErr e = do { addErr (sep [ptext (sLit "Pattern syntax in expression context:"),
-                                nest 4 (ppr e)])
+                                nest 4 (ppr e)] $$
+                           text "Did you mean to enable TypeApplications?")
                  ; return (EWildPat, emptyFVs) }
 
 badIpBinds :: Outputable a => SDoc -> a -> SDoc
index 8f87d73..9ddf132 100644 (file)
@@ -45,7 +45,7 @@ import Var              ( Id )
 import THNames          ( quoteExpName, quotePatName, quoteDecName, quoteTypeName
                         , decsQTyConName, expQTyConName, patQTyConName, typeQTyConName, )
 
-import {-# SOURCE #-} TcExpr   ( tcMonoExpr )
+import {-# SOURCE #-} TcExpr   ( tcPolyExpr )
 import {-# SOURCE #-} TcSplice ( runMetaD, runMetaE, runMetaP, runMetaT, tcTopSpliceExpr )
 #endif
 
@@ -295,7 +295,7 @@ runRnSplice flavour run_meta ppr_res splice
              -- Typecheck the expression
        ; meta_exp_ty   <- tcMetaTy meta_ty_name
        ; zonked_q_expr <- tcTopSpliceExpr Untyped $
-                          tcMonoExpr the_expr meta_exp_ty
+                          tcPolyExpr the_expr meta_exp_ty
 
              -- Run the expression
        ; result <- run_meta zonked_q_expr
index 52a164f..5a58148 100644 (file)
@@ -751,7 +751,7 @@ checkExtraConstraintWildCard env wc
   = checkWildCard env mb_bad
   where
     mb_bad | not (extraConstraintWildCardsAllowed env)
-           = Just (ptext (sLit "Extra-contraint wildcard") <+> quotes (ppr wc)
+           = Just (ptext (sLit "Extra-constraint wildcard") <+> quotes (ppr wc)
                    <+> ptext (sLit "not allowed"))
            | otherwise
            = Nothing
@@ -774,6 +774,7 @@ wildCardsAllowed env
        RuleCtx {}          -> True
        FamPatCtx {}        -> True   -- Not named wildcards though
        GHCiCtx {}          -> True
+       HsTypeCtx {}        -> True
        _                   -> False
 
 rnAnonWildCard :: HsWildCardInfo RdrName -> RnM (HsWildCardInfo Name)
index 22f16b1..8878ba6 100644 (file)
@@ -6,14 +6,15 @@
 The @Inst@ type: dictionaries or method instances
 -}
 
-{-# LANGUAGE CPP, MultiWayIf #-}
+{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
 
 module Inst (
-       deeplySkolemise, deeplyInstantiate,
+       deeplySkolemise,
+       topInstantiate, topInstantiateInferred, deeplyInstantiate,
        instCall, instDFunType, instStupidTheta,
        newWanted, newWanteds,
 
-       newOverloadedLit, mkOverLit,
+       newOverloadedLit, newNonTrivialOverloadedLit, mkOverLit,
 
        newClsInst,
        tcGetInsts, tcGetInstEnvs, getOverlapFlag,
@@ -149,6 +150,65 @@ deeplySkolemise ty
   | otherwise
   = return (idHsWrapper, [], [], ty)
 
+-- | Instantiate all outer type variables
+-- and any context. Never looks through arrows.
+topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
+-- if    topInstantiate ty = (wrap, rho)
+-- and   e :: ty
+-- then  wrap e :: rho
+topInstantiate = top_instantiate True
+
+-- | Instantiate all outer 'Invisible' binders
+-- and any context. Never looks through arrows or specified type variables.
+-- Used for visible type application.
+topInstantiateInferred :: CtOrigin -> TcSigmaType
+                       -> TcM (HsWrapper, TcSigmaType)
+-- if    topInstantiate ty = (wrap, rho)
+-- and   e :: ty
+-- then  wrap e :: rho
+topInstantiateInferred = top_instantiate False
+
+top_instantiate :: Bool   -- True <=> instantiate *all* variables
+                -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
+top_instantiate inst_all orig ty
+  | not (null binders && null theta)
+  = do { let (inst_bndrs, leave_bndrs) = span should_inst binders
+             (inst_theta, leave_theta)
+               | null leave_bndrs = (theta, [])
+               | otherwise        = ([], theta)
+       ; (subst, inst_tvs') <- newMetaTyVars (map (binderVar "top_inst") inst_bndrs)
+       ; let inst_theta' = substTheta subst inst_theta
+             sigma'      = substTy    subst (mkForAllTys leave_bndrs $
+                                             mkFunTys leave_theta rho)
+
+       ; wrap1 <- instCall orig (mkTyVarTys inst_tvs') inst_theta'
+       ; traceTc "Instantiating"
+                 (vcat [ text "all tyvars?" <+> ppr inst_all
+                       , text "origin" <+> pprCtOrigin orig
+                       , text "type" <+> ppr ty
+                       , text "with" <+> ppr inst_tvs'
+                       , text "theta:" <+>  ppr inst_theta' ])
+
+       ; (wrap2, rho2) <-
+           if null leave_bndrs
+
+         -- account for types like forall a. Num a => forall b. Ord b => ...
+           then top_instantiate inst_all orig sigma'
+
+         -- but don't loop if there were any un-inst'able tyvars
+           else return (idHsWrapper, sigma')
+
+       ; return (wrap2 <.> wrap1, rho2) }
+
+  | otherwise = return (idHsWrapper, ty)
+  where
+    (binders, phi) = tcSplitNamedPiTys ty
+    (theta, rho)   = tcSplitPhiTy phi
+
+    should_inst bndr
+      | inst_all  = True
+      | otherwise = binderVisibility bndr == Invisible
+
 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 --   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
 -- In general if
@@ -176,6 +236,7 @@ deeplyInstantiate orig ty
 
   | otherwise = return (idHsWrapper, ty)
 
+
 {-
 ************************************************************************
 *                                                                      *
@@ -269,39 +330,54 @@ instStupidTheta orig theta
 *                                                                      *
 ************************************************************************
 
+-}
+
+{-
 In newOverloadedLit we convert directly to an Int or Integer if we
 know that's what we want.  This may save some time, by not
 temporarily generating overloaded literals, but it won't catch all
 cases (the rest are caught in lookupInst).
--}
 
-newOverloadedLit :: CtOrigin
-                 -> HsOverLit Name
-                 -> TcRhoType
-                 -> TcM (HsOverLit TcId)
-newOverloadedLit orig lit res_ty
-    = do dflags <- getDynFlags
-         newOverloadedLit' dflags orig lit res_ty
-
-newOverloadedLit' :: DynFlags
-                  -> CtOrigin
-                  -> HsOverLit Name
-                  -> TcRhoType
-                  -> TcM (HsOverLit TcId)
-newOverloadedLit' dflags orig
-  lit@(OverLit { ol_val = val, ol_rebindable = rebindable
-               , ol_witness = meth_name }) res_ty
+-}
 
+newOverloadedLit :: HsOverLit Name
+                 -> TcSigmaType  -- if nec'y, this type is instantiated...
+                 -> CtOrigin     -- ... using this CtOrigin
+                 -> TcM (HsWrapper, HsOverLit TcId)
+                   -- wrapper :: input type "->" type of result
+newOverloadedLit
+  lit@(OverLit { ol_val = val, ol_rebindable = rebindable }) res_ty res_orig
   | not rebindable
-  , Just expr <- shortCutLit dflags val res_ty
+    -- all built-in overloaded lits are not higher-rank, so skolemise.
+    -- this is necessary for shortCutLit.
+  = do { (wrap, insted_ty) <- deeplyInstantiate res_orig res_ty
+       ; dflags <- getDynFlags
+       ; case shortCutLit dflags val insted_ty of
         -- Do not generate a LitInst for rebindable syntax.
         -- Reason: If we do, tcSimplify will call lookupInst, which
         --         will call tcSyntaxName, which does unification,
         --         which tcSimplify doesn't like
-  = return (lit { ol_witness = expr, ol_type = res_ty
-                , ol_rebindable = rebindable })
+           Just expr -> return ( wrap
+                               , lit { ol_witness = expr, ol_type = insted_ty
+                                     , ol_rebindable = False } )
+           Nothing   -> (wrap, ) <$>
+                        newNonTrivialOverloadedLit orig lit insted_ty }
 
   | otherwise
+  = do { lit' <- newNonTrivialOverloadedLit orig lit res_ty
+       ; return (idHsWrapper, lit') }
+  where
+    orig = LiteralOrigin lit
+
+-- Does not handle things that 'shortCutLit' can handle. See also
+-- newOverloadedLit in TcUnify
+newNonTrivialOverloadedLit :: CtOrigin
+                           -> HsOverLit Name
+                           -> TcSigmaType
+                           -> TcM (HsOverLit TcId)
+newNonTrivialOverloadedLit orig
+  lit@(OverLit { ol_val = val, ol_witness = meth_name
+               , ol_rebindable = rebindable }) res_ty
   = do  { hs_lit <- mkOverLit val
         ; let lit_ty = hsLitType hs_lit
         ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
@@ -310,8 +386,8 @@ newOverloadedLit' dflags orig
                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
                 -- However this'll be picked up by tcSyntaxOp if necessary
         ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
-        ; return (lit { ol_witness = witness, ol_type = res_ty
-                      , ol_rebindable = rebindable }) }
+        ; return (lit { ol_witness = witness, ol_type = res_ty,
+                        ol_rebindable = rebindable }) }
 
 ------------
 mkOverLit :: OverLitVal -> TcM HsLit
index 444b148..dac6aed 100644 (file)
@@ -5,7 +5,7 @@
 Typecheck arrow notation
 -}
 
-{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RankNTypes, TupleSections #-}
 
 module TcArrows ( tcProc ) where
 
@@ -250,7 +250,7 @@ tc_cmd env
               arg_tys = map hsLPatType pats'
               cmd' = HsCmdLam (MG { mg_alts = L l [match'], mg_arg_tys = arg_tys
                                   , mg_res_ty = res_ty, mg_origin = origin })
-        ; return (mkHsCmdCast co cmd') }
+        ; return (mkHsCmdWrap (mkWpCastN co) cmd') }
   where
     n_pats     = length pats
     match_ctxt = (LambdaExpr :: HsMatchContext Name)    -- Maybe KappaExpr?
@@ -272,7 +272,7 @@ tc_cmd env
 tc_cmd env (HsCmdDo (L l stmts) _) (cmd_stk, res_ty)
   = do  { co <- unifyType noThing unitTy cmd_stk  -- Expecting empty argument stack
         ; stmts' <- tcStmts ArrowExpr (tcArrDoStmt env) stmts res_ty
-        ; return (mkHsCmdCast co (HsCmdDo (L l stmts') res_ty)) }
+        ; return (mkHsCmdWrap (mkWpCastN co) (HsCmdDo (L l stmts') res_ty)) }
 
 
 -----------------------------------------------------------------
index 83f2eb9..113a561 100644 (file)
@@ -15,7 +15,7 @@ module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
                  TcPragEnv, mkPragEnv,
                  tcUserTypeSig, instTcTySig, chooseInferredQuantifiers,
                  instTcTySigFromId, tcExtendTyVarEnvFromSig,
-                 badBootDeclErr, mkExport ) where
+                 badBootDeclErr ) where
 
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
@@ -32,7 +32,7 @@ import TcEvidence
 import TcHsType
 import TcPat
 import TcMType
-import Inst( deeplyInstantiate )
+import Inst( topInstantiate, deeplyInstantiate )
 import FamInstEnv( normaliseType )
 import FamInst( tcGetFamInstEnvs )
 import TyCon
@@ -556,7 +556,7 @@ tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
        ; mono_ids' <- mapM tc_mono_info mono_infos
        ; return (binds', mono_ids') }
   where
-    tc_mono_info (name, _, mono_id)
+    tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id })
       = do { mono_ty' <- zonkTcType (idType mono_id)
              -- Zonk, mainly to expose unboxed types to checkStrictBinds
            ; let mono_id' = setIdType mono_id mono_ty'
@@ -601,11 +601,11 @@ tcPolyCheck rec_tc prag_fn
        ; spec_prags <- tcSpecPrags poly_id prag_sigs
        ; poly_id    <- addInlinePrags poly_id prag_sigs
 
-       ; let (_, _, mono_id) = mono_info
-             export = ABE { abe_wrap = idHsWrapper
-                          , abe_poly = poly_id
-                          , abe_mono = mono_id
-                          , abe_prags = SpecPrags spec_prags }
+       ; let export = ABE { abe_wrap      = idHsWrapper
+                          , abe_inst_wrap = idHsWrapper
+                          , abe_poly      = poly_id
+                          , abe_mono      = mbi_mono_id mono_info
+                          , abe_prags     = SpecPrags spec_prags }
              abs_bind = L loc $ AbsBinds
                         { abs_tvs = skol_tvs
                         , abs_ev_vars = ev_vars, abs_ev_binds = [ev_binds]
@@ -616,6 +616,54 @@ tcPolyCheck _rec_tc _prag_fn sig _bind
   = pprPanic "tcPolyCheck" (ppr sig)
 
 ------------------
+{-
+Note [Instantiate when inferring a type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f = (*)
+As there is no incentive to instantiate the RHS, tcMonoBinds will
+produce a type of forall a. Num a => a -> a -> a for `f`. This will then go
+through simplifyInfer and such, remaining unchanged.
+
+There are two problems with this:
+ 1) If the definition were `g _ = (*)`, we get a very unusual type of
+    `forall {a}. a -> forall b. Num b => b -> b -> b` for `g`. This is
+    surely confusing for users.
+
+ 2) The monomorphism restriction can't work. The MR is dealt with in
+    simplifyInfer, and simplifyInfer has no way of instantiating. This
+    could perhaps be worked around, but it may be hard to know even
+    when instantiation should happen.
+
+There is an easy solution to all three problems: instantiate (deeply) when
+inferring a type. So that's what we do. Note that this decision is
+user-facing.
+
+Here are the details:
+ * tcMonoBinds produces the "monomorphic" ids to be put in the AbsBinds.
+   It is inconvenient to instantiate in this function or below. So the
+   monomorphic ids will be uninstantiated (and hence actually polymorphic,
+   but that doesn't ruin anyone's day).
+
+ * In the same captureConstraints as the tcMonoBinds, we instantiate all
+   the types of the monomorphic ids. Instantiating will produce constraints
+   to solve and instantiated types. These constraints and the instantiated
+   types go into simplifyInfer. HsWrappers are produced that go from
+   the "mono" types to the instantiated ones.
+
+ * simplifyInfer does its magic, figuring out how to regeneralize.
+
+ * mkExport then does the impedence matching and needs to connect the
+   monomorphic ids to the polymorphic types as decided by simplifyInfer.
+   Because the instantiation happens before simplifyInfer, we also pass in
+   the HsWrappers obtained via instantiating so that mkExport can connect
+   all the pieces.
+
+ * We produce an AbsBinds with the right (instantiated and then, perhaps,
+   regeneralized) polytypes and the not-yet-instantiated "monomorphic" ids,
+   using the built HsWrappers to connect. Done!
+-}
+
 tcPolyInfer
   :: RecFlag       -- Whether it's recursive after breaking
                    -- dependencies based on type signatures
@@ -624,19 +672,36 @@ tcPolyInfer
   -> [LHsBind Name]
   -> TcM (LHsBinds TcId, [TcId])
 tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
-  = do { (tclvl, wanted, (binds', mono_infos))
+  = do { (tclvl, wanted, (binds', mono_infos, wrappers, insted_tys))
              <- pushLevelAndCaptureConstraints  $
-                tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
+             do { (binds', mono_infos)
+                    <- tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
+                  -- See Note [Instantiate when inferring a type]
+                ; traceTc "Note [Instantiate when inferring a type]" $
+                    vcat (map (pprBndr LetBind . mbi_mono_id) mono_infos)
+                ; (wrappers, insted_tys)
+                    <- tcExtendIdBndrs
+                         [ TcIdBndr mono_id NotTopLevel
+                         | MBI { mbi_mono_id = mono_id } <- mono_infos ] $
+                       mapAndUnzipM deeply_instantiate mono_infos
+                     -- during instantiation, we might encounter an error
+                     -- whose message will want to list these binders as
+                     -- relevant.
+
+                ; return (binds', mono_infos, wrappers, insted_tys) }
+
+       ; let name_taus = [ (mbi_poly_name info, tau)
+                         | (info, tau) <- zip mono_infos insted_tys]
+             sigs      = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ]
 
-       ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
-             sigs      = [ sig | (_, Just sig, _) <- mono_infos ]
        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
        ; (qtvs, givens, ev_binds)
                  <- simplifyInfer tclvl mono sigs name_taus wanted
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
-                    mapM (mkExport prag_fn qtvs inferred_theta) mono_infos
+                    zipWith3M (mkExport prag_fn qtvs inferred_theta)
+                              mono_infos wrappers insted_tys
 
        ; loc <- getSrcSpanM
        ; let poly_ids = map abe_poly exports
@@ -649,12 +714,23 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
        ; return (unitBag abs_bind, poly_ids) }
          -- poly_ids are guaranteed zonked by mkExport
 
+  where
+    deeply_instantiate :: MonoBindInfo -> TcM (HsWrapper, TcRhoType)
+    deeply_instantiate (MBI { mbi_mono_id = mono_id, mbi_orig = orig })
+      = do { mono_ty <- zonkTcType (idType mono_id)
+              -- NB: zonk to uncover any foralls
+           ; addErrCtxtM (instErrCtxt mono_id mono_ty) $
+             deeplyInstantiate orig mono_ty }
+
 --------------
 mkExport :: TcPragEnv
          -> [TyVar] -> TcThetaType      -- Both already zonked
          -> MonoBindInfo
+         -> HsWrapper -- the instantiation wrapper;
+                      -- see Note [Instantiate when inferring a type]
+         -> TcTauType -- the instantiated type
          -> TcM (ABExport Id)
--- Only called for generalisation plan IferGen, not by CheckGen or NoGen
+-- Only called for generalisation plan InferGen, not by CheckGen or NoGen
 --
 -- mkExport generates exports with
 --      zonked type variables,
@@ -667,14 +743,19 @@ mkExport :: TcPragEnv
 
 -- Pre-condition: the qtvs and theta are already zonked
 
-mkExport prag_fn qtvs theta mono_info@(poly_name, mb_sig, mono_id)
-  = do  { mono_ty  <- zonkTcType (idType mono_id)
+mkExport prag_fn qtvs theta
+         mono_info@(MBI { mbi_poly_name = poly_name
+                        , mbi_sig       = mb_sig
+                        , mbi_mono_id   = mono_id })
+         inst_wrap inst_ty
+  = do  { inst_ty <- zonkTcType inst_ty
+
         ; poly_id <- case mb_sig of
               Just sig | Just poly_id <- completeIdSigPolyId_maybe sig
                        -> return poly_id
               _other   -> checkNoErrs $
                           mkInferredPolyId qtvs theta
-                                           poly_name mb_sig mono_ty
+                                           poly_name mb_sig inst_ty
               -- The checkNoErrs ensures that if the type is ambiguous
               -- we don't carry on to the impedence matching, and generate
               -- a duplicate ambiguity error.  There is a similar
@@ -688,9 +769,12 @@ mkExport prag_fn qtvs theta mono_info@(poly_name, mb_sig, mono_id)
         -- See Note [Impedence matching]
         -- NB: we have already done checkValidType, including an ambiguity check,
         --     on the type; either when we checked the sig or in mkInferredPolyId
-        ; let sel_poly_ty = mkInvSigmaTy qtvs theta mono_ty
+        ; let sel_poly_ty = mkInvSigmaTy qtvs theta inst_ty
+                -- this type is just going into tcSubType, so Inv vs. Spec doesn't
+                -- matter
+
               poly_ty     = idType poly_id
-        ; wrap <- if sel_poly_ty `eqType` poly_ty
+        ; wrap <- if sel_poly_ty `eqType` poly_ty  -- NB: eqType ignores visibility
                   then return idHsWrapper  -- Fast path; also avoids complaint when we infer
                                            -- an ambiguouse type and have AllowAmbiguousType
                                            -- e..g infer  x :: forall a. F a -> Int
@@ -701,7 +785,8 @@ mkExport prag_fn qtvs theta mono_info@(poly_name, mb_sig, mono_id)
         ; when warn_missing_sigs $ localSigWarn poly_id mb_sig
 
         ; return (ABE { abe_wrap = wrap
-                        -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => mono_ty)
+                        -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => inst_ty)
+                      , abe_inst_wrap = inst_wrap
                       , abe_poly = poly_id
                       , abe_mono = mono_id
                       , abe_prags = SpecPrags spec_prags}) }
@@ -724,13 +809,12 @@ mkInferredPolyId qtvs inferred_theta poly_name mb_sig mono_ty
                -- We can discard the coercion _co, because we'll reconstruct
                -- it in the call to tcSubType below
 
-       ; (my_tvs, theta') <- chooseInferredQuantifiers
-                                inferred_theta (tyCoVarsOfType mono_ty') mb_sig
+       ; (binders, theta') <- chooseInferredQuantifiers inferred_theta
+                                (tyCoVarsOfType mono_ty') qtvs mb_sig
 
-       ; let qtvs' = filter (`elemVarSet` my_tvs) qtvs   -- Maintain original order
-             inferred_poly_ty = mkInvSigmaTy qtvs' theta' mono_ty'
+       ; let inferred_poly_ty = mkForAllTys binders (mkPhiTy theta' mono_ty')
 
-       ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr my_tvs, ppr theta'
+       ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
                                           , ppr inferred_poly_ty])
        ; addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
          checkValidType (InfSigCtxt poly_name) inferred_poly_ty
@@ -739,25 +823,32 @@ mkInferredPolyId qtvs inferred_theta poly_name mb_sig mono_ty
        ; return (mkLocalIdOrCoVar poly_name inferred_poly_ty) }
 
 
-chooseInferredQuantifiers :: TcThetaType -> TcTyVarSet -> Maybe TcIdSigInfo
-                          -> TcM (TcTyVarSet, TcThetaType)
-chooseInferredQuantifiers inferred_theta tau_tvs Nothing
+chooseInferredQuantifiers :: TcThetaType   -- inferred
+                          -> TcTyVarSet    -- tvs free in tau type
+                          -> [TcTyVar]     -- inferred quantified tvs
+                          -> Maybe TcIdSigInfo
+                          -> TcM ([TcTyBinder], TcThetaType)
+chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
   = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
                         -- Include kind variables!  Trac #7916
              my_theta = pickQuantifiablePreds free_tvs inferred_theta
-       ; return (free_tvs, my_theta) }
+             binders  = [ mkNamedBinder tv Invisible
+                        | tv <- qtvs
+                        , tv `elemVarSet` free_tvs ]
+       ; return (binders, my_theta) }
 
-chooseInferredQuantifiers inferred_theta tau_tvs
+chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                           (Just (TISI { sig_bndr = bndr_info
                                       , sig_ctxt = ctxt
-                                      , sig_theta = annotated_theta }))
+                                      , sig_theta = annotated_theta
+                                      , sig_skols = annotated_tvs }))
   | PartialSig { sig_cts = extra } <- bndr_info
   , Nothing <- extra
   = do { annotated_theta <- zonkTcTypes annotated_theta
        ; let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
                                         `unionVarSet` tau_tvs)
        ; traceTc "ciq" (vcat [ ppr bndr_info, ppr annotated_theta, ppr free_tvs])
-       ; return (free_tvs, annotated_theta) }
+       ; return (mk_binders free_tvs, annotated_theta) }
 
   | PartialSig { sig_cts = extra } <- bndr_info
   , Just loc <- extra
@@ -786,7 +877,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs
                 | otherwise         -> return ()
            False                    -> reportError msg
 
-       ; return (free_tvs, final_theta) }
+       ; return (mk_binders free_tvs, final_theta) }
 
   | otherwise = pprPanic "chooseInferredQuantifiers" (ppr bndr_info)
 
@@ -798,12 +889,21 @@ chooseInferredQuantifiers inferred_theta tau_tvs
               , if suppress_hint then empty else pts_hint
               , typeSigCtxt ctxt bndr_info ]
 
+    spec_tv_set = mkVarSet $ map snd annotated_tvs
+    mk_binders free_tvs
+      = [ mkNamedBinder tv vis
+        | tv <- qtvs
+        , tv `elemVarSet` free_tvs
+        , let vis | tv `elemVarSet` spec_tv_set = Specified
+                  | otherwise                   = Invisible ]
+                          -- Pulling from qtvs maintains original order
 
 mk_impedence_match_msg :: MonoBindInfo
                        -> TcType -> TcType
                        -> TidyEnv -> TcM (TidyEnv, SDoc)
 -- This is a rare but rather awkward error messages
-mk_impedence_match_msg (name, mb_sig, _) inf_ty sig_ty tidy_env
+mk_impedence_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
+                       inf_ty sig_ty tidy_env
  = do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env  inf_ty
       ; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty
       ; let msg = vcat [ ptext (sLit "When checking that the inferred type")
@@ -911,14 +1011,13 @@ We can get these by "impedance matching":
 
 Suppose the shared quantified tyvars are qtvs and constraints theta.
 Then we want to check that
-   f's final inferred polytype is more polymorphic than
-      forall qtvs. theta => f_mono_ty
+     forall qtvs. theta => f_mono_ty   is more polymorphic than   f's polytype
 and the proof is the impedance matcher.
 
 Notice that the impedance matcher may do defaulting.  See Trac #7173.
 
 It also cleverly does an ambiguity check; for example, rejecting
-   f :: F a -> a
+   f :: F a -> a
 where F is a non-injective type function.
 -}
 
@@ -940,7 +1039,7 @@ recoveryCode binder_names sig_fn
       = mkLocalId name forall_a_a
 
 forall_a_a :: TcType
-forall_a_a = mkInvForAllTys [levity1TyVar, openAlphaTyVar] openAlphaTy
+forall_a_a = mkSpecForAllTys [levity1TyVar, openAlphaTyVar] openAlphaTy
 
 {- *********************************************************************
 *                                                                      *
@@ -952,13 +1051,13 @@ Note [Handling SPECIALISE pragmas]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The basic idea is this:
 
-   f:: Num a => a -> b -> a
+   foo :: Num a => a -> b -> a
    {-# SPECIALISE foo :: Int -> b -> Int #-}
 
 We check that
-   (forall a. Num a => a -> a)
+   (forall a b. Num a => a -> b -> a)
       is more polymorphic than
-   Int -> Int
+   forall b. Int -> b -> Int
 (for which we could use tcSubType, but see below), generating a HsWrapper
 to connect the two, something like
       wrap = /\b. <hole> Int b dNumInt
@@ -1009,8 +1108,8 @@ Some wrinkles
 
 1. We don't use full-on tcSubType, because that does co and contra
    variance and that in turn will generate too complex a LHS for the
-   RULE.  So we use a single invocation of deeplySkolemise /
-   deeplyInstantiate in tcSpecWrapper.  (Actually I think that even
+   RULE.  So we use a single invocation of skolemise /
+   topInstantiate in tcSpecWrapper.  (Actually I think that even
    the "deeply" stuff may be too much, because it introduces lambdas,
    though I think it can be made to work without too much trouble.)
 
@@ -1142,8 +1241,8 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
 -- See Note [Handling SPECIALISE pragmas], wrinkle 1
 tcSpecWrapper ctxt poly_ty spec_ty
   = do { (sk_wrap, inst_wrap)
-               <- tcGen ctxt spec_ty $ \ _ spec_tau ->
-                  do { (inst_wrap, tau) <- deeplyInstantiate orig poly_ty
+               <- tcSkolemise ctxt spec_ty $ \ _ spec_tau ->
+                  do { (inst_wrap, tau) <- topInstantiate orig poly_ty
                      ; _ <- unifyType noThing spec_tau tau
                             -- Deliberately ignore the evidence
                             -- See Note [Handling SPECIALISE pragmas],
@@ -1377,24 +1476,31 @@ tcMonoBinds is_rec sig_fn no_gen
                          -- use ReturnTv to allow impredicativity
         ; let rhs_ty = mkTyVarTy rhs_tv
         ; mono_id <- newNoSigLetBndr no_gen name rhs_ty
-        ; (co_fn, matches') <- tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel] $
-                                 -- We extend the error context even for a non-recursive
-                                 -- function so that in type error messages we show the
-                                 -- type of the thing whose rhs we are type checking
-                               tcMatchesFun name matches rhs_ty
+        ; (co_fn, matches')
+            <- tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel] $
+                  -- We extend the error context even for a non-recursive
+                  -- function so that in type error messages we show the
+                  -- type of the thing whose rhs we are type checking
+               tcMatchesFun name matches rhs_ty
 
         ; return (unitBag $ L b_loc $
                      FunBind { fun_id = L nm_loc mono_id,
                                fun_matches = matches', bind_fvs = fvs,
                                fun_co_fn = co_fn, fun_tick = [] },
-                  [(name, Nothing, mono_id)]) }
+                  [MBI { mbi_poly_name = name
+                       , mbi_sig       = Nothing
+                       , mbi_mono_id   = mono_id
+                       , mbi_orig      = matchesCtOrigin matches }]) }
 
 tcMonoBinds _ sig_fn no_gen binds
   = do  { tc_binds <- mapM (wrapLocM (tcLhs sig_fn no_gen)) binds
 
         -- Bring the monomorphic Ids, into scope for the RHSs
         ; let mono_info  = getMonoBindInfo tc_binds
-              rhs_id_env = [(name, mono_id) | (name, mb_sig, mono_id) <- mono_info
+              rhs_id_env = [(name, mono_id) | MBI { mbi_poly_name = name
+                                                  , mbi_sig       = mb_sig
+                                                  , mbi_mono_id   = mono_id }
+                                                    <- mono_info
                                             , case mb_sig of
                                                 Just sig -> isPartialSig sig
                                                 Nothing  -> True ]
@@ -1403,9 +1509,9 @@ tcMonoBinds _ sig_fn no_gen binds
 
         ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
                                        | (n,id) <- rhs_id_env]
-        ; binds' <- tcExtendLetEnvIds NotTopLevel rhs_id_env $
-                    mapM (wrapLocM tcRhs) tc_binds
-        ; return (listToBag binds', mono_info) }
+        ; (binds', mono_infos') <- tcExtendLetEnvIds NotTopLevel rhs_id_env $
+                                  mapAndUnzipM (wrapLocFstM tcRhs) tc_binds
+        ; return (listToBag binds', concat mono_infos') }
 
 ------------------------
 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
@@ -1427,9 +1533,11 @@ data TcMonoBind         -- Half completed; LHS done, RHS not done
   = TcFunBind  MonoBindInfo  SrcSpan (MatchGroup Name (LHsExpr Name))
   | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name (LHsExpr Name)) TcSigmaType
 
-type MonoBindInfo = (Name, Maybe TcIdSigInfo, TcId)
-        -- Type signature (if any), and
-        -- the monomorphic bound things
+data MonoBindInfo = MBI { mbi_poly_name :: Name
+                        , mbi_sig       :: Maybe TcIdSigInfo
+                        , mbi_mono_id   :: TcId
+                        , mbi_orig      :: CtOrigin }
+                            -- origin associated with RHS
 
 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind
 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches })
@@ -1443,12 +1551,22 @@ tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches })
        -- Both InferGen and CheckGen gives rise to LetLclBndr
     do  { mono_name <- newLocalName name
         ; let mono_id = mkLocalIdOrCoVar mono_name tau
-        ; return (TcFunBind (name, Just sig, mono_id) nm_loc matches) }
+        ; return (TcFunBind (MBI { mbi_poly_name = name
+                                 , mbi_sig       = Just sig
+                                 , mbi_mono_id   = mono_id
+                                 , mbi_orig      =
+                                     Shouldn'tHappenOrigin "FunBind sig" })
+                            nm_loc matches) }
 
   | otherwise
   = do  { mono_ty <- newOpenFlexiTyVarTy
         ; mono_id <- newNoSigLetBndr no_gen name mono_ty
-        ; return (TcFunBind (name, Nothing, mono_id) nm_loc matches) }
+        ; return (TcFunBind (MBI { mbi_poly_name = name
+                                 , mbi_sig       = Nothing
+                                 , mbi_mono_id   = mono_id
+                                 , mbi_orig      =
+                                     Shouldn'tHappenOrigin "FunBind nosig" })
+                            nm_loc matches) }
 
 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
   = do  { let tc_pat exp_ty = tcLetPat sig_fn no_gen pat exp_ty $
@@ -1458,11 +1576,15 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
                 -- names, which the pattern has brought into scope.
               lookup_info :: Name -> TcM MonoBindInfo
               lookup_info name
-                 = do { mono_id <- tcLookupId name
-                      ; let mb_sig = case sig_fn name of
-                                       Just (TcIdSig sig) -> Just sig
-                                       _                  -> Nothing
-                     ; return (name, mb_sig, mono_id) }
+                = do { mono_id <- tcLookupId name
+                     ; let mb_sig = case sig_fn name of
+                                      Just (TcIdSig sig) -> Just sig
+                                      _                  -> Nothing
+                     ; return (MBI { mbi_poly_name = name
+                                   , mbi_sig       = mb_sig
+                                   , mbi_mono_id   = mono_id
+                                   , mbi_orig      =
+                                       Shouldn'tHappenOrigin "PatBind" }) }
 
         ; ((pat', infos), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $
                                      tcInfer tc_pat
@@ -1473,18 +1595,20 @@ tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
         -- AbsBind, VarBind impossible
 
 -------------------
-tcRhs :: TcMonoBind -> TcM (HsBind TcId)
-tcRhs (TcFunBind info@(_, mb_sig, mono_id) loc matches)
+tcRhs :: TcMonoBind -> TcM (HsBind TcId, [MonoBindInfo])  -- fills in the mbi_orig
+tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
+                 loc matches)
   = tcExtendIdBinderStackForRhs [info]  $
     tcExtendTyVarEnvForRhs mb_sig       $
     do  { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
         ; (co_fn, matches') <- tcMatchesFun (idName mono_id)
-                                            matches (idType mono_id)
-        ; return (FunBind { fun_id = L loc mono_id
-                          , fun_matches = matches'
-                          , fun_co_fn = co_fn
-                          , bind_fvs = placeHolderNamesTc
-                          , fun_tick = [] }) }
+                                 matches (idType mono_id)
+        ; return ( FunBind { fun_id = L loc mono_id
+                           , fun_matches = matches'
+                           , fun_co_fn = co_fn
+                           , bind_fvs = placeHolderNamesTc
+                           , fun_tick = [] }
+                 , [info { mbi_orig = matchesCtOrigin matches }] ) }
 
 -- TODO: emit Hole Constraints for wildcards
 tcRhs (TcPatBind infos pat' grhss pat_ty)
@@ -1496,9 +1620,13 @@ tcRhs (TcPatBind infos pat' grhss pat_ty)
     do  { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
         ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
                     tcGRHSsPat grhss pat_ty
-        ; return (PatBind { pat_lhs = pat', pat_rhs = grhss', pat_rhs_ty = pat_ty
-                          , bind_fvs = placeHolderNamesTc
-                          , pat_ticks = ([],[]) }) }
+        ; let orig   = grhssCtOrigin grhss
+              infos' = [ info { mbi_orig = orig } | info <- infos ]
+        ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
+                           , pat_rhs_ty = pat_ty
+                           , bind_fvs = placeHolderNamesTc
+                           , pat_ticks = ([],[]) }
+                 , infos' ) }
 
 tcExtendTyVarEnvForRhs :: Maybe TcIdSigInfo -> TcM a -> TcM a
 tcExtendTyVarEnvForRhs Nothing thing_inside
@@ -1531,7 +1659,9 @@ tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
 -- If we had the *polymorphic* version of f in the TcIdBinderStack, it
 -- would not be reported as relevant, because its type is closed
 tcExtendIdBinderStackForRhs infos thing_inside
-  = tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel | (_, _, mono_id) <- infos] thing_inside
+  = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
+                    | MBI { mbi_mono_id = mono_id } <- infos ]
+                    thing_inside
     -- NotTopLevel: it's a monomorphic binding
 
 ---------------------
@@ -1998,3 +2128,17 @@ typeSigCtxt ctxt (PartialSig { sig_hs_ty = hs_ty })
   = pprSigCtxt ctxt empty (ppr hs_ty)
 typeSigCtxt ctxt (CompleteSig id)
   = pprSigCtxt ctxt empty (ppr (idType id))
+
+instErrCtxt :: TcId -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
+instErrCtxt id ty env
+  = do { let (env', ty') = tidyOpenType env ty
+       ; return (env', hang (text "When instantiating" <+> quotes (ppr id) <>
+                             text ", initially inferred to have" $$
+                             text "this overly-general type:")
+                          2 (ppr ty') $$
+                       extra) }
+  where
+    extra = sdocWithDynFlags $ \dflags ->
+            ppWhen (xopt LangExt.MonomorphismRestriction dflags) $
+            text "NB: This instantiation can be caused by the" <+>
+            text "monomorphism restriction."
index 64bf2d5..6411fa9 100644 (file)
@@ -247,13 +247,14 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn
                   tcPolyCheck NonRecursive no_prag_fn local_dm_sig
                               (L bind_loc lm_bind)
 
-        ; let export = ABE { abe_poly  = global_dm_id
+        ; let export = ABE { abe_poly      = global_dm_id
                            -- We have created a complete type signature in
                            -- instTcTySig, hence it is safe to call
                            -- completeSigPolyId
-                           , abe_mono  = completeIdSigPolyId local_dm_sig
-                           , abe_wrap  = idHsWrapper
-                           , abe_prags = IsDefaultMethod }
+                           , abe_mono      = completeIdSigPolyId local_dm_sig
+                           , abe_wrap      = idHsWrapper
+                           , abe_inst_wrap = idHsWrapper
+                           , abe_prags     = IsDefaultMethod }
               full_bind = AbsBinds { abs_tvs      = tyvars
                                    , abs_ev_vars  = [this_dict]
                                    , abs_exports  = [export]
index b54d5f5..d480dee 100644 (file)
@@ -1239,7 +1239,8 @@ mkEqInfoMsg ct ty1 ty2
               = snd (mkAmbigMsg False ct)
               | otherwise = empty
 
-    invis_msg | Just Invisible <- tcEqTypeVis ty1 ty2
+    invis_msg | Just vis <- tcEqTypeVis ty1 ty2
+              , vis /= Visible
               = sdocWithDynFlags $ \dflags ->
                 if gopt Opt_PrintExplicitKinds dflags
                 then text "Use -fprint-explicit-kinds to see the kind arguments"
@@ -2111,7 +2112,7 @@ pprSkol implics tv
   = case skol_info of
       UnkSkol         -> pp_tv <+> ptext (sLit "is an unknown type variable")
       SigSkol ctxt ty -> ppr_rigid (pprSigSkolInfo ctxt
-                                      (mkInvForAllTys skol_tvs ty))
+                                      (mkSpecForAllTys skol_tvs ty))
       _               -> ppr_rigid (pprSkolInfo skol_info)
   where
     pp_tv = quotes (ppr tv)
@@ -2167,7 +2168,8 @@ relevantBindings want_filtering ctxt ct
            vcat [ ppr ct
                 , pprCtOrigin (ctLocOrigin loc)
                 , ppr ct_tvs
-                , ppr [id | TcIdBndr id _ <- tcl_bndrs lcl_env] ]
+                , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
+                                   | TcIdBndr id _ <- tcl_bndrs lcl_env ] ]
 
        ; (tidy_env', docs, discards)
               <- go env1 ct_tvs (maxRelevantBinds dflags)
index 7890115..184aa16 100644 (file)
@@ -8,7 +8,8 @@ module TcEvidence (
   HsWrapper(..),
   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
   mkWpLams, mkWpLet, mkWpCastN, mkWpCastR,
-  mkWpFun, idHsWrapper, isIdHsWrapper, pprHsWrapper,
+  mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,
+  symWrapper_maybe,
 
   -- Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
@@ -63,6 +64,10 @@ import FastString
 import SrcLoc
 import Data.IORef( IORef )
 
+#if __GLASGOW_HASKELL__ < 709
+import Control.Applicative ( (<*>), (<$>) )
+#endif
+
 {-
 Note [TcCoercions]
 ~~~~~~~~~~~~~~~~~~
@@ -161,13 +166,14 @@ 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
+  | WpFun HsWrapper HsWrapper TcType
+       -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ]
        -- 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 mkFunCo, but it has to be this way
        -- because we can't use 'sym' to flip around these HsWrappers
+       -- The TcType is the "from" type of the first wrapper
 
   | WpCast TcCoercionR        -- A cast:  [] `cast` co
                               -- Guaranteed not the identity coercion
@@ -192,12 +198,26 @@ WpHole <.> c = c
 c <.> WpHole = c
 c1 <.> c2    = c1 `WpCompose` c2
 
-mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper
+mkWpFun :: HsWrapper -> HsWrapper
+        -> TcType    -- the "from" type of the first wrapper
+        -> TcType    -- either type of the second wrapper (used only when the
+                     -- second wrapper is the identity)
+        -> HsWrapper
+        -- NB: These optimisations are important, because we need
+        -- symWrapper_maybe to work in TcUnify.matchExpectedFunTys
+        -- See that function for more info.
 mkWpFun WpHole       WpHole       _  _  = WpHole
-mkWpFun WpHole       (WpCast co2) t1 _  = WpCast (mkFunCo Representational (mkRepReflCo t1) co2)
-mkWpFun (WpCast co1) WpHole       _  t2 = WpCast (mkFunCo Representational (mkSymCo co1) (mkRepReflCo t2))
-mkWpFun (WpCast co1) (WpCast co2) _  _  = WpCast (mkFunCo Representational (mkSymCo co1) co2)
-mkWpFun co1          co2          t1 t2 = WpFun co1 co2 t1 t2
+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 _  = WpFun co1 co2 t1
+
+-- | @mkWpFuns arg_tys wrap@, where @wrap :: a "->" b@, gives a wrapper from
+-- @arg_tys -> a@ to @arg_tys -> b@.
+mkWpFuns :: [TcType] -> HsWrapper -> HsWrapper
+mkWpFuns []                 res_wrap = res_wrap
+mkWpFuns (arg_ty : arg_tys) res_wrap
+  = WpFun idHsWrapper (mkWpFuns arg_tys res_wrap) arg_ty
 
 mkWpCastR :: TcCoercionR -> HsWrapper
 mkWpCastR co
@@ -212,6 +232,21 @@ mkWpCastN co
                     WpCast (mkTcSubCo co)
     -- The mkTcSubCo converts Nominal to Representational
 
+-- | In a few limited cases, it is possible to reverse the direction
+-- of an HsWrapper. This tries to do so.
+symWrapper_maybe :: HsWrapper -> Maybe HsWrapper
+symWrapper_maybe = go
+  where
+    go WpHole              = return WpHole
+    go (WpCompose wp1 wp2) = WpCompose <$> go wp2 <*> go wp1
+    go (WpFun {})          = Nothing
+    go (WpCast co)         = return (WpCast (mkTcSymCo co))
+    go (WpEvLam {})        = Nothing
+    go (WpEvApp {})        = Nothing
+    go (WpTyLam {})        = Nothing
+    go (WpTyApp {})        = Nothing
+    go (WpLet {})          = Nothing
+
 mkWpTyApps :: [Type] -> HsWrapper
 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
 
@@ -710,7 +745,7 @@ 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 (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 "|>")
                                               <+> pprParendCo co)]
index f299e9d..93ba3db 100644 (file)
@@ -6,11 +6,10 @@
 \section[TcExpr]{Typecheck an expression}
 -}
 
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables #-}
 
 module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC,
-                tcInferRho, tcInferRhoNC,
+                tcInferSigma, tcInferSigmaNC, tcInferRho, tcInferRhoNC,
                 tcSyntaxOp, tcCheckId,
                 addExprErrCtxt,
                 getFixedTyVars ) where
@@ -51,9 +50,9 @@ import Name
 import RdrName
 import TyCon
 import Type
+import TysPrim        ( tYPE )
 import TcEvidence
 import VarSet
-import VarEnv
 import TysWiredIn
 import TysPrim( intPrimTy )
 import PrimOp( tagToEnumKey )
@@ -62,9 +61,9 @@ import MkId ( proxyHashId )
 import DynFlags
 import SrcLoc
 import Util
+import VarEnv  ( emptyTidyEnv )
 import ListSetOps
 import Maybes
-import ErrUtils
 import Outputable
 import FastString
 import Control.Monad
@@ -97,11 +96,15 @@ tcPolyExpr expr res_ty
   = addExprErrCtxt expr $
     do { traceTc "tcPolyExpr" (ppr res_ty); tcPolyExprNC expr res_ty }
 
-tcPolyExprNC expr res_ty
-  = do { traceTc "tcPolyExprNC" (ppr res_ty)
-       ; (gen_fn, expr') <- tcGen GenSigCtxt res_ty $ \ _ rho ->
-                            tcMonoExprNC expr rho
-       ; return (mkLHsWrap gen_fn expr') }
+tcPolyExprNC (L loc expr) res_ty
+  = do { traceTc "tcPolyExprNC_O" (ppr res_ty)
+       ; (wrap, expr')
+           <- tcSkolemise GenSigCtxt res_ty $ \ _ res_ty ->
+              setSrcSpan loc $
+                -- NB: setSrcSpan *after* skolemising, so we get better
+                -- skolem locations
+              tcExpr expr res_ty
+       ; return $ L loc (mkHsWrap wrap expr') }
 
 ---------------
 tcMonoExpr, tcMonoExprNC
@@ -121,43 +124,25 @@ tcMonoExprNC (L loc expr) res_ty
         ; return (L loc expr') }
 
 ---------------
+tcInferSigma, tcInferSigmaNC :: LHsExpr Name -> TcM ( LHsExpr TcId
+                                                    , TcSigmaType )
+-- Infer a *sigma*-type.
+tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr)
+
+tcInferSigmaNC (L loc expr)
+  = setSrcSpan loc $
+    do { (expr', sigma) <- tcInfer (tcExpr expr)
+       ; return (L loc expr', sigma) }
+
 tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
--- Infer a *rho*-type.  This is, in effect, a special case
--- for ids and partial applications, so that if
---     f :: Int -> (forall a. a -> a) -> Int
--- then we can infer
---     f 3 :: (forall a. a -> a) -> Int
--- And that in turn is useful
---  (a) for the function part of any application (see tcApp)
---  (b) for the special rule for '$'
+-- Infer a *rho*-type. The return type is always (shallowly) instantiated.
 tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr)
 
-tcInferRhoNC (L loc expr)
-  = setSrcSpan loc $
-    do { (expr', rho) <- tcInfer (tcExpr expr)
-       ; return (L loc expr', rho) }
+tcInferRhoNC expr
+  = do { (expr', sigma) <- tcInferSigmaNC expr
+       ; (wrap, rho) <- topInstantiate (exprCtOrigin (unLoc expr)) sigma
+       ; return (mkLHsWrap wrap expr', rho) }
 
-tcUnboundId :: OccName -> TcRhoType -> TcM (HsExpr TcId)
--- Typechedk an occurrence of an unbound Id
---
--- Some of these started life as a true hole "_".  Others might simply
--- be variables that accidentally have no binding site
---
--- We turn all of them into HsVar, since HsUnboundVar can't contain an
--- Id; and indeed the evidence for the CHoleCan does bind it, so it's
--- not unbound any more!
-tcUnboundId occ res_ty
- = do { ty <- newFlexiTyVarTy liftedTypeKind
-      ; name <- newSysName occ
-      ; let ev = mkLocalId name ty
-      ; loc <- getCtLocM HoleOrigin Nothing
-      ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty
-                                              , ctev_dest = EvVarDest ev
-                                              , ctev_loc  = loc}
-                           , cc_occ = occ
-                           , cc_hole = ExprHole }
-      ; emitInsoluble can
-      ; tcWrapResult (HsVar (noLoc ev)) ty res_ty }
 
 {-
 ************************************************************************
@@ -165,22 +150,23 @@ tcUnboundId occ res_ty
         tcExpr: the main expression typechecker
 *                                                                      *
 ************************************************************************
+
+NB: The res_ty is always deeply skolemised.
 -}
 
 tcExpr :: HsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
-tcExpr e res_ty | debugIsOn && isSigmaTy res_ty     -- Sanity check
-                = pprPanic "tcExpr: sigma" (ppr res_ty $$ ppr e)
-
 tcExpr (HsVar (L _ name)) res_ty = tcCheckId name res_ty
 tcExpr (HsUnboundVar v)   res_ty = tcUnboundId v res_ty
 
-tcExpr (HsApp e1 e2) res_ty = tcApp e1 [e2] res_ty
+tcExpr (HsApp e1 e2) res_ty
+  = do { (wrap, fun, args) <- tcApp Nothing e1 [e2] res_ty
+       ; return (mkHsWrap wrap $ unLoc $ foldl mkHsApp fun args) }
 
-tcExpr (HsLit lit)   res_ty = do { let lit_ty = hsLitType lit
-                                 ; tcWrapResult (HsLit lit) lit_ty res_ty }
+tcExpr e@(HsLit lit) res_ty = do { let lit_ty = hsLitType lit
+                                 ; tcWrapResult (HsLit lit) lit_ty res_ty }
 
-tcExpr (HsPar expr)  res_ty = do { expr' <- tcMonoExprNC expr res_ty
-                                 ; return (HsPar expr') }
+tcExpr (HsPar expr)   res_ty = do { expr' <- tcMonoExprNC expr res_ty
+                                  ; return (HsPar expr') }
 
 tcExpr (HsSCC src lbl expr) res_ty
   = do { expr' <- tcMonoExpr expr res_ty
@@ -195,7 +181,9 @@ tcExpr (HsCoreAnn src lbl expr) res_ty
         ; return (HsCoreAnn src lbl expr') }
 
 tcExpr (HsOverLit lit) res_ty
-  = do  { lit' <- newOverloadedLit (LiteralOrigin lit) lit res_ty
+  = do  { (_wrap,  lit') <- newOverloadedLit lit res_ty
+                                            (Shouldn'tHappenOrigin "HsOverLit")
+        ; MASSERT( isIdHsWrapper _wrap )
         ; return (HsOverLit lit') }
 
 tcExpr (NegApp expr neg_expr) res_ty
@@ -204,25 +192,24 @@ tcExpr (NegApp expr neg_expr) res_ty
         ; expr' <- tcMonoExpr expr res_ty
         ; return (NegApp expr' neg_expr') }
 
-tcExpr (HsIPVar x) res_ty
-  = do { let origin = IPOccOrigin x
-           {- Implicit parameters must have a *tau-type* not a.
+tcExpr e@(HsIPVar x) res_ty
+  = do {   {- Implicit parameters must have a *tau-type* not a
               type scheme.  We enforce this by creating a fresh
               type variable as its type.  (Because res_ty may not
               be a tau-type.) -}
-       ; ip_ty <- newOpenFlexiTyVarTy
+         ip_ty <- newOpenFlexiTyVarTy
        ; let ip_name = mkStrLitTy (hsIPNameFS x)
        ; ip_var <- emitWantedEvVar origin (mkClassPred ipClass [ip_name, ip_ty])
-       ; tcWrapResult (fromDict ipClass ip_name ip_ty (HsVar (noLoc ip_var)))
+       ; tcWrapResult (fromDict ipClass ip_name ip_ty (HsVar (noLoc ip_var)))
                       ip_ty res_ty }
   where
   -- Coerces a dictionary for `IP "x" t` into `t`.
   fromDict ipClass x ty = HsWrap $ mkWpCastR $
                           unwrapIP $ mkClassPred ipClass [x,ty]
+  origin = IPOccOrigin x
 
-tcExpr (HsOverLabel l) res_ty  -- See Note [Type-checking overloaded labels]
-  = do { let origin = OverLabelOrigin l
-       ; isLabelClass <- tcLookupClass isLabelClassName
+tcExpr e@(HsOverLabel l) res_ty  -- See Note [Type-checking overloaded labels]
+  = do { isLabelClass <- tcLookupClass isLabelClassName
        ; alpha <- newOpenFlexiTyVarTy
        ; let lbl = mkStrLitTy l
              pred = mkClassPred isLabelClass [lbl, alpha]
@@ -231,39 +218,43 @@ tcExpr (HsOverLabel l) res_ty  -- See Note [Type-checking overloaded labels]
        ; let proxy_arg = L loc (mkHsWrap (mkWpTyApps [typeSymbolKind, lbl])
                                          (HsVar (L loc proxyHashId)))
              tm = L loc (fromDict pred (HsVar (L loc var))) `HsApp` proxy_arg
-       ; tcWrapResult tm alpha res_ty }
+       ; tcWrapResult tm alpha res_ty }
   where
   -- Coerces a dictionary for `IsLabel "x" t` into `Proxy# x -> t`.
   fromDict pred = HsWrap $ mkWpCastR $ unwrapIP pred
+  origin = OverLabelOrigin l
 
 tcExpr (HsLam match) res_ty
-  = do  { (co_fn, match') <- tcMatchLambda match res_ty
+  = do  { (co_fn, _, match') <- tcMatchLambda herald match_ctxt match res_ty
         ; return (mkHsWrap co_fn (HsLam match')) }
+  where
+    match_ctxt = MC { mc_what = LambdaExpr, mc_body = tcBody }
+    herald = sep [ ptext (sLit "The lambda expression") <+>
+                   quotes (pprSetDepth (PartWay 1) $
+                           pprMatches (LambdaExpr :: HsMatchContext Name) match),
+                        -- The pprSetDepth makes the abstraction print briefly
+                   ptext (sLit "has")]
 
 tcExpr e@(HsLamCase _ matches) res_ty
-  = do  { (co_fn, [arg_ty], body_ty) <- matchExpectedFunTys msg 1 res_ty
-        ; matches' <- tcMatchesCase match_ctxt arg_ty matches body_ty
-        ; return $ mkHsWrapCo co_fn $ HsLamCase arg_ty matches' }
+  = do { (co_fn, ~[arg_ty], matches')
+           <- tcMatchLambda msg match_ctxt matches res_ty
+           -- The laziness annotation is because we don't want to fail here
+           -- if there are multiple arguments
+       ; return (mkHsWrap co_fn $ HsLamCase arg_ty matches') }
   where msg = sep [ ptext (sLit "The function") <+> quotes (ppr e)
                   , ptext (sLit "requires")]
         match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }
 
-tcExpr (ExprWithTySig expr sig_ty) res_ty
+tcExpr e@(ExprWithTySig expr sig_ty) res_ty
   = do { sig_info <- checkNoErrs $  -- Avoid error cascade
                      tcUserTypeSig sig_ty Nothing
        ; (expr', poly_ty) <- tcExprSig expr sig_info
-       ; (inst_wrap, rho) <- deeplyInstantiate ExprSigOrigin poly_ty
-       ; let expr'' = mkHsWrap inst_wrap $
-                      ExprWithTySigOut expr' sig_ty
-       ; tcWrapResult expr'' rho res_ty }
+       ; let expr'' = ExprWithTySigOut expr' sig_ty
+       ; tcWrapResult e expr'' poly_ty res_ty }
 
 tcExpr (HsType ty) _
-  = failWithTc (text "Can't handle type argument:" <+> ppr ty)
-        -- This is the syntax for type applications that I was planning
-        -- but there are difficulties (e.g. what order for type args)
-        -- so it's not enabled yet.
-        -- Can't eliminate it altogether from the parser, because the
-        -- same parser parses *patterns*.
+  = failWithTc (sep [ text "Type argument used outside of a function argument:"
+                    , ppr ty ])
 
 
 {-
@@ -331,7 +322,7 @@ only going to work when it's fully applied, so it turns into
 So it seems more uniform to treat 'seq' as it it was a language
 construct.
 
-See Note [seqId magic] in MkId, and
+See also Note [seqId magic] in MkId
 -}
 
 tcExpr expr@(OpApp arg1 op fix arg2) res_ty
@@ -349,17 +340,18 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
   | (L loc (HsVar (L lv op_name))) <- op
   , op_name `hasKey` dollarIdKey        -- Note [Typing rule for ($)]
   = do { traceTc "Application rule" (ppr op)
-       ; (arg1', arg1_ty) <- tcInferRho arg1
+       ; (arg1', arg1_ty) <- tcInferSigma arg1
 
-       ; let doc = ptext (sLit "The first argument of ($) takes")
-       ; (co_arg1, [arg2_ty], op_res_ty) <- matchExpectedFunTys doc 1 arg1_ty
+       ; let doc   = ptext (sLit "The first argument of ($) takes")
+             orig1 = exprCtOrigin (unLoc arg1)
+       ; (wrap_arg1, [arg2_sigma], op_res_ty) <-
+           matchActualFunTys doc orig1 1 arg1_ty
 
          -- We have (arg1 $ arg2)
          -- So: arg1_ty = arg2_ty -> op_res_ty
-         -- where arg2_ty maybe polymorphic; that's the point
+         -- where arg2_sigma maybe polymorphic; that's the point
 
-       ; arg2'  <- tcArg op (arg2, arg2_ty, 2)
-       ; co_b   <- unifyType (Just expr) op_res_ty res_ty    -- op_res ~ res
+       ; arg2'  <- tcArg op (arg2, arg2_sigma, 2)
 
        -- Make sure that the argument type has kind '*'
        --   ($) :: forall (v:Levity) (a:*) (b:TYPE v). (a->b) -> a -> b
@@ -372,19 +364,31 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
        -- so we don't need to check anything for that
        ; a2_tv <- newReturnTyVar liftedTypeKind
        ; let a2_ty = mkTyVarTy a2_tv
-       ; co_a <- unifyType (Just arg2) arg2_ty a2_ty     -- arg2 ~ a2
+       ; co_a <- unifyType (Just arg2) arg2_sigma a2_ty    -- arg2_sigma ~N a2_ty
 
-       ; op_id  <- tcLookupId op_name
+       ; wrap_res <- tcSubTypeHR orig1 (Just expr) op_res_ty res_ty
+                       -- op_res -> res
 
+       ; op_id  <- tcLookupId op_name
        ; let op' = L loc (HsWrap (mkWpTyApps [ getLevity "tcExpr ($)" res_ty
                                              , a2_ty
-                                             , res_ty ])
+                                             , res_ty])
                                  (HsVar (L lv op_id)))
-       ; return $
-         OpApp (mkLHsWrapCo (mkTcFunCo Nominal co_a co_b) $
-                mkLHsWrapCo co_arg1 arg1')
-               op' fix
-               (mkLHsWrapCo co_a arg2') }
+             -- arg1' :: arg1_ty
+             -- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty)
+             -- wrap_res :: op_res_ty "->" res_ty
+             -- co_a :: arg2_sigma ~N a2_ty
+             -- op' :: (a2_ty -> res_ty) -> a2_ty -> res_ty
+
+             -- wrap1 :: arg1_ty "->" (a2_ty -> res_ty)
+             wrap1 = mkWpFun (mkWpCastN (mkTcSymCo co_a))
+                       wrap_res a2_ty res_ty <.> wrap_arg1
+
+             -- arg2' :: arg2_sigma
+             -- wrap_a :: a2_ty "->" arg2_sigma
+       ; return (OpApp (mkLHsWrap wrap1 arg1')
+                       op' fix
+                       (mkLHsWrapCo co_a arg2')) }
 
   | (L loc (HsRecFld (Ambiguous lbl _))) <- op
   , Just sig_ty <- obviousSig (unLoc arg1)
@@ -397,23 +401,23 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
 
   | otherwise
   = do { traceTc "Non Application rule" (ppr op)
-       ; (op', op_ty) <- tcInferFun op
-       ; (co_fn, arg_tys, op_res_ty) <- unifyOpFunTysWrap op 2 op_ty
-       ; co_res <- unifyType (Just expr) op_res_ty res_ty
-       ; [arg1', arg2'] <- tcArgs op [arg1, arg2] arg_tys
-       ; return $ mkHsWrapCo co_res $
-         OpApp arg1' (mkLHsWrapCo co_fn op') fix arg2' }
+       ; (wrap, op', [arg1', arg2'])
+           <- tcApp (Just $ mk_op_msg op)
+                     op [arg1, arg2] res_ty
+       ; return (mkHsWrap wrap $ OpApp arg1' op' fix arg2') }
 
 -- Right sections, equivalent to \ x -> x `op` expr, or
 --      \ x -> op x expr
 
 tcExpr expr@(SectionR op arg2) res_ty
   = do { (op', op_ty) <- tcInferFun op
-       ; (co_fn, [arg1_ty, arg2_ty], op_res_ty) <- unifyOpFunTysWrap op 2 op_ty
-       ; co_res <- unifyType (Just expr) (mkFunTy arg1_ty op_res_ty) res_ty
+       ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) <-
+           matchActualFunTys (mk_op_msg op) SectionOrigin 2 op_ty
+       ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
+                                 (mkFunTy arg1_ty op_res_ty) res_ty
        ; arg2' <- tcArg op (arg2, arg2_ty, 2)
-       ; return $ mkHsWrapCo co_res $
-         SectionR (mkLHsWrapCo co_fn op') arg2' }
+       ; return ( mkHsWrap wrap_res $
+                  SectionR (mkLHsWrap wrap_fun op') arg2' ) }
 
 tcExpr expr@(SectionL arg1 op) res_ty
   = do { (op', op_ty) <- tcInferFun op
@@ -421,11 +425,13 @@ tcExpr expr@(SectionL arg1 op) res_ty
        ; let n_reqd_args | xopt LangExt.PostfixOperators dflags = 1
                          | otherwise                            = 2
 
-       ; (co_fn, (arg1_ty:arg_tys), op_res_ty) <- unifyOpFunTysWrap op n_reqd_args op_ty
-       ; co_res <- unifyType (Just expr) (mkFunTys arg_tys op_res_ty) res_ty
+       ; (wrap_fn, (arg1_ty:arg_tys), op_res_ty)
+           <- matchActualFunTys (mk_op_msg op) SectionOrigin n_reqd_args op_ty
+       ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
+                                 (mkFunTys arg_tys op_res_ty) res_ty
        ; arg1' <- tcArg op (arg1, arg1_ty, 1)
-       ; return $ mkHsWrapCo co_res $
-         SectionL arg1' (mkLHsWrapCo co_fn op') }
+       ; return ( mkHsWrap wrap_res $
+                  SectionL arg1' (mkLHsWrap wrap_fn op') ) }
 
 tcExpr expr@(ExplicitTuple tup_args boxity) res_ty
   | all tupArgPresent tup_args
@@ -451,30 +457,35 @@ tcExpr expr@(ExplicitTuple tup_args boxity) res_ty
                  = mkFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args]
                             (mkTupleTy boxity arg_tys)
 
-       ; coi <- unifyType (Just expr) actual_res_ty res_ty
+       ; wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "ExpTuple")
+                             (Just expr)
+                             actual_res_ty res_ty
 
        -- Handle tuple sections where
        ; tup_args1 <- tcTupArgs tup_args arg_tys
 
-       ; return $ mkHsWrapCo coi (ExplicitTuple tup_args1 boxity) }
+       ; return $ mkHsWrap wrap (ExplicitTuple tup_args1 boxity) }
 
 tcExpr (ExplicitList _ witness exprs) res_ty
   = case witness of
       Nothing   -> do  { (coi, elt_ty) <- matchExpectedListTy res_ty
                        ; exprs' <- mapM (tc_elt elt_ty) exprs
-                       ; return $ mkHsWrapCo coi (ExplicitList elt_ty Nothing exprs') }
+                       ; return $
+                         mkHsWrapCo coi $ ExplicitList elt_ty Nothing exprs' }
 
-      Just fln -> do  { list_ty <- newFlexiTyVarTy liftedTypeKind
+      Just fln -> do { list_ty <- newFlexiTyVarTy liftedTypeKind
                      ; fln' <- tcSyntaxOp ListOrigin fln (mkFunTys [intTy, list_ty] res_ty)
                      ; (coi, elt_ty) <- matchExpectedListTy list_ty
                      ; exprs' <- mapM (tc_elt elt_ty) exprs
-                     ; return $ mkHsWrapCo coi (ExplicitList elt_ty (Just fln') exprs') }
+                     ; return $
+                       mkHsWrapCo coi $ ExplicitList elt_ty (Just fln') exprs' }
      where tc_elt elt_ty expr = tcPolyExpr expr elt_ty
 
 tcExpr (ExplicitPArr _ exprs) res_ty    -- maybe empty
   = do  { (coi, elt_ty) <- matchExpectedPArrTy res_ty
         ; exprs' <- mapM (tc_elt elt_ty) exprs
-        ; return $ mkHsWrapCo coi (ExplicitPArr elt_ty exprs') }
+        ; return $
+          mkHsWrapCo coi $ ExplicitPArr elt_ty exprs' }
   where
     tc_elt elt_ty expr = tcPolyExpr expr elt_ty
 
@@ -512,33 +523,30 @@ tcExpr (HsCase scrut matches) exp_ty
 
 tcExpr (HsIf Nothing pred b1 b2) res_ty    -- Ordinary 'if'
   = do { pred' <- tcMonoExpr pred boolTy
+            -- this forces the branches to be fully instantiated
+            -- (See #10619)
+       ; res_ty <- tauTvForReturnTv res_ty
        ; b1' <- tcMonoExpr b1 res_ty
        ; b2' <- tcMonoExpr b2 res_ty
        ; return (HsIf Nothing pred' b1' b2') }
 
-tcExpr (HsIf (Just fun) pred b1 b2) res_ty   -- Note [Rebindable syntax for if]
-  = do { pred_ty <- newOpenFlexiTyVarTy
-       ; b1_ty   <- newOpenFlexiTyVarTy
-       ; b2_ty   <- newOpenFlexiTyVarTy
-       ; let if_ty = mkFunTys [pred_ty, b1_ty, b2_ty] res_ty
-       ; fun'  <- tcSyntaxOp IfOrigin fun if_ty
-       ; pred' <- tcMonoExpr pred pred_ty
-       ; b1'   <- tcMonoExpr b1 b1_ty
-       ; b2'   <- tcMonoExpr b2 b2_ty
-       -- Fundamentally we are just typing (ifThenElse e1 e2 e3)
-       -- so maybe we should use the code for function applications
-       -- (which would allow ifThenElse to be higher rank).
-       -- But it's a little awkward, so I'm leaving it alone for now
-       -- and it maintains uniformity with other rebindable syntax
-       ; return (HsIf (Just fun') pred' b1' b2') }
+tcExpr (HsIf (Just fun) pred b1 b2) res_ty
+  -- Note [Rebindable syntax for if]
+  = do { (wrap, fun', [pred', b1', b2'])
+           <- tcApp (Just herald) (noLoc fun) [pred, b1, b2] res_ty
+       ; return ( mkHsWrap wrap $
+                  HsIf (Just (unLoc fun')) pred' b1' b2' ) }
+  where
+    herald = text "Rebindable" <+> quotes (text "if") <+> text "takes"
 
 tcExpr (HsMultiIf _ alts) res_ty
   = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
-       ; return $ HsMultiIf res_ty alts' }
+       ; return (HsMultiIf res_ty alts') }
   where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody }
 
 tcExpr (HsDo do_or_lc stmts _) res_ty
-  = tcDoStmts do_or_lc stmts res_ty
+  = do { expr' <- tcDoStmts do_or_lc stmts res_ty
+       ; return expr' }
 
 tcExpr (HsProc pat cmd) res_ty
   = do  { (pat', cmd', coi) <- tcProc pat cmd res_ty
@@ -598,19 +606,25 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name
         -- Check for missing fields
         ; checkMissingFields con_like rbinds
 
-        ; (con_expr, con_tau) <- tcInferId con_name
+        ; (con_expr, con_sigma) <- tcInferId con_name
+        ; (con_wrap, con_tau) <-
+            topInstantiate (OccurrenceOf con_name) con_sigma
+              -- a shallow instantiation should really be enough for
+              -- a data constructor.
         ; let arity = conLikeArity con_like
               (arg_tys, actual_res_ty) = tcSplitFunTysN con_tau arity
         ; case conLikeWrapId_maybe con_like of
                Nothing -> nonBidirectionalErr (conLikeName con_like)
                Just con_id -> do {
-                  co_res <- unifyType (Just expr) actual_res_ty res_ty
+                  res_wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "RecordCon")
+                                          (Just expr) actual_res_ty res_ty
                 ; rbinds' <- tcRecordBinds con_like arg_tys rbinds
-                ; return $ mkHsWrapCo co_res $
-                    RecordCon { rcon_con_name = L loc con_id
-                              , rcon_con_expr = con_expr
-                              , rcon_con_like = con_like
-                              , rcon_flds = rbinds' } } }
+                ; return $
+                  mkHsWrap res_wrap $
+                  RecordCon { rcon_con_name = L loc con_id
+                            , rcon_con_expr = mkHsWrap con_wrap con_expr
+                            , rcon_con_like = con_like
+                            , rcon_flds = rbinds' } } }
 
 {-
 Note [Type of a record update]
@@ -749,12 +763,12 @@ following.
 
 tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
   = ASSERT( notNull rbnds )
-    do  { -- STEP -2: typecheck the record_expr, the record to bd updated
-          (record_expr', record_tau) <- tcInferFun record_expr
+    do  { -- STEP -2: typecheck the record_expr, the record to be updated
+          (record_expr', record_rho) <- tcInferRho record_expr
 
         -- STEP -1  See Note [Disambiguating record fields]
         -- After this we know that rbinds is unambiguous
-        ; rbinds <- disambiguateRecordBinds record_expr record_tau rbnds res_ty
+        ; rbinds <- disambiguateRecordBinds record_expr record_rho rbnds res_ty
         ; let upd_flds = map (unLoc . hsRecFieldLbl . unLoc) rbinds
               upd_fld_occs = map (occNameFS . rdrNameOcc . rdrNameAmbiguousFieldOcc) upd_flds
               sel_ids      = map selectorAmbiguousFieldOcc upd_flds
@@ -860,8 +874,12 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
               scrut_ty      = TcType.substTy scrut_subst  con1_res_ty
               con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
 
-        ; co_res   <- unifyType (Just expr) rec_res_ty res_ty
-        ; co_scrut <- unifyType (Just record_expr) record_tau scrut_ty
+        ; wrap_res <- tcSubTypeHR (exprCtOrigin expr)
+                                  (Just expr) rec_res_ty res_ty
+        ; co_scrut <- unifyType (Just record_expr) record_rho scrut_ty
+                -- NB: normal unification is OK here (as opposed to subsumption),
+                -- because for this to work out, both record_rho and scrut_ty have
+                -- to be normal datatypes -- no contravariant stuff can go on
 
         -- STEP 5
         -- Typecheck the bindings
@@ -887,7 +905,8 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
         ; req_wrap <- instCallConstraints RecordUpdOrigin req_theta'
 
         -- Phew!
-        ; return $ mkHsWrapCo co_res $
+        ; return $
+          mkHsWrap wrap_res $
           RecordUpd { rupd_expr = mkLHsWrap fam_co (mkLHsWrapCo co_scrut record_expr')
                     , rupd_flds = rbinds'
                     , rupd_cons = relevant_cons, rupd_in_tys = scrut_inst_tys
@@ -916,8 +935,8 @@ tcExpr (PArrSeq _ seq@(FromTo expr1 expr2)) res_ty
         ; enumFromToP <- initDsTc $ dsDPHBuiltin enumFromToPVar
         ; enum_from_to <- newMethodFromName (PArrSeqOrigin seq)
                                  (idName enumFromToP) elt_ty
-        ; return $ mkHsWrapCo coi
-                     (PArrSeq enum_from_to (FromTo expr1' expr2')) }
+        ; return $
+          mkHsWrapCo coi $ PArrSeq enum_from_to (FromTo expr1' expr2') }
 
 tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
   = do  { (coi, elt_ty) <- matchExpectedPArrTy res_ty
@@ -927,8 +946,9 @@ tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
         ; enumFromThenToP <- initDsTc $ dsDPHBuiltin enumFromThenToPVar
         ; eft <- newMethodFromName (PArrSeqOrigin seq)
                       (idName enumFromThenToP) elt_ty        -- !!!FIXME: chak
-        ; return $ mkHsWrapCo coi
-                     (PArrSeq eft (FromThenTo expr1' expr2' expr3')) }
+        ; return $
+          mkHsWrapCo coi $
+          PArrSeq eft (FromThenTo expr1' expr2' expr3') }
 
 tcExpr (PArrSeq _ _) _
   = panic "TcExpr.tcExpr: Infinite parallel array!"
@@ -943,9 +963,12 @@ tcExpr (PArrSeq _ _) _
 ************************************************************************
 -}
 
-tcExpr (HsSpliceE splice)        res_ty = tcSpliceExpr splice res_ty
-tcExpr (HsBracket brack)         res_ty = tcTypedBracket   brack res_ty
-tcExpr (HsRnBracketOut brack ps) res_ty = tcUntypedBracket brack ps res_ty
+tcExpr (HsSpliceE splice)        res_ty
+  = tcSpliceExpr splice res_ty
+tcExpr (HsBracket brack)         res_ty
+  = tcTypedBracket   brack res_ty
+tcExpr (HsRnBracketOut brack ps) res_ty
+  = tcUntypedBracket brack ps res_ty
 
 {-
 ************************************************************************
@@ -1004,7 +1027,7 @@ tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty
 
 -----------------
 arithSeqEltType :: Maybe (SyntaxExpr Name) -> TcRhoType
-              -> TcM (TcCoercion, TcType, Maybe (SyntaxExpr Id))
+                -> TcM (TcCoercionN, TcType, Maybe (SyntaxExpr Id))
 arithSeqEltType Nothing res_ty
   = do { (coi, elt_ty) <- matchExpectedListTy res_ty
        ; return (coi, elt_ty, Nothing) }
@@ -1022,66 +1045,66 @@ arithSeqEltType (Just fl) res_ty
 ************************************************************************
 -}
 
-tcApp :: LHsExpr Name -> [LHsExpr Name] -- Function and args
-      -> TcRhoType -> TcM (HsExpr TcId) -- Translated fun and args
-
-tcApp (L _ (HsPar e)) args res_ty
-  = tcApp e args res_ty
-
-tcApp (L _ (HsApp e1 e2)) args res_ty
-  = tcApp e1 (e2:args) res_ty   -- Accumulate the arguments
-
-tcApp (L loc (HsVar (L _ fun))) args res_ty
-  | fun `hasKey` tagToEnumKey
-  , [arg] <- args
-  = tcTagToEnum loc fun arg res_ty
-
-  | fun `hasKey` seqIdKey
-  , [arg1,arg2] <- args
-  = tcSeq loc fun arg1 arg2 res_ty
-
--- Look for applications of ambiguous record selectors to arguments
--- with type signatures, see Note [Disambiguating record fields]
-tcApp (L loc (HsRecFld (Ambiguous lbl _))) args@(L _ arg:_) res_ty
-  | Just sig_ty <- obviousSig arg
-  = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty
-       ; sel_name <- disambiguateSelector lbl sig_tc_ty
-       ; tcApp (L loc (HsRecFld (Unambiguous lbl sel_name))) args res_ty }
-
-tcApp fun args res_ty
-  = do  {   -- Type-check the function
-        ; (fun1, fun_tau) <- tcInferFun fun
-
-            -- Extract its argument types
-        ; (co_fun, expected_arg_tys, actual_res_ty)
-              <- matchExpectedFunTys (mk_app_msg fun) (length args) fun_tau
-
-        -- Typecheck the result, thereby propagating
-        -- info (if any) from result into the argument types
-        -- Both actual_res_ty and res_ty are deeply skolemised
-        -- 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 (Just $ foldl mkHsApp fun args)
-                                     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  = mkLHsWrap wrap_res (foldl mkHsApp fun2 args1)
-
-        ; return (unLoc app) }
-
+tcApp :: Maybe SDoc  -- like "The function `f' is applied to"
+                     -- or leave out to get exactly that message
+      -> LHsExpr Name -> [LHsExpr Name] -- Function and args
+      -> TcRhoType -> TcM (HsWrapper, LHsExpr TcId, [LHsExpr TcId])
+           -- (wrap, fun, args). For an ordinary function application,
+           -- these should be assembled as (wrap (fun args)).
+           -- But OpApp is slightly different, so that's why the caller
+           -- must assemble
+
+tcApp m_herald orig_fun orig_args res_ty
+  = go orig_fun orig_args
+  where
+    go (L _ (HsPar e))     args = go e  args
+    go (L _ (HsApp e1 e2)) args = go e1 (e2:args)
+
+    go (L loc (HsVar (L _ fun))) args
+      | fun `hasKey` tagToEnumKey
+      , count (not . isLHsTypeExpr) args == 1
+      = do { (wrap, expr, args) <- tcTagToEnum loc fun args res_ty
+           ; return (wrap, expr, args) }
+
+      | fun `hasKey` seqIdKey
+      , count (not . isLHsTypeExpr) args == 2
+      = do { (wrap, expr, args) <- tcSeq loc fun args res_ty
+           ; return (wrap, expr, args) }
+
+    go (L loc (HsRecFld (Ambiguous lbl _))) args@(L _ arg : _)
+      | Just sig_ty <- obviousSig arg
+      = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty
+           ; sel_name  <- disambiguateSelector lbl sig_tc_ty
+           ; go (L loc (HsRecFld (Unambiguous lbl sel_name))) args }
+
+    go fun args
+      = do {   -- Type-check the function
+           ; (fun1, fun_sigma) <- tcInferFun fun
+           ; let orig = exprCtOrigin (unLoc fun)
+
+           ; (wrap_fun, args1, actual_res_ty)
+               <- tcArgs fun fun_sigma orig args
+                         (m_herald `orElse` mk_app_msg fun)
+
+                -- this is just like tcWrapResult, but the types don't line
+                -- up to call that function
+           ; wrap_res <- addFunResCtxt True (unLoc fun) actual_res_ty res_ty $
+                         tcSubTypeDS_NC_O orig GenSigCtxt
+                           (Just $ foldl mkHsApp fun args)
+                           actual_res_ty res_ty
+
+           ; return (wrap_res, mkLHsWrap wrap_fun fun1, args1) }
 
 mk_app_msg :: LHsExpr Name -> SDoc
 mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun)
                      , ptext (sLit "is applied to")]
 
+mk_op_msg :: LHsExpr Name -> SDoc
+mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
+
 ----------------
-tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
--- Infer and instantiate the type of a function
+tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcSigmaType)
+-- Infer type of a function
 tcInferFun (L loc (HsVar (L _ name)))
   = do { (fun, ty) <- setSrcSpan loc (tcInferId name)
                -- Don't wrap a context around a plain Id
@@ -1093,23 +1116,70 @@ tcInferFun (L loc (HsRecFld f))
        ; return (L loc fun, ty) }
 
 tcInferFun fun
-  = do { (fun, fun_ty) <- tcInfer (tcMonoExpr fun)
+  = do { (fun, fun_ty) <- tcInferSigma fun
 
          -- Zonk the function type carefully, to expose any polymorphism
          -- E.g. (( \(x::forall a. a->a). blah ) e)
          -- We can see the rank-2 type of the lambda in time to generalise e
        ; fun_ty' <- zonkTcType fun_ty
 
-       ; (wrap, rho) <- deeplyInstantiate AppOrigin fun_ty'
-       ; return (mkLHsWrap wrap fun, rho) }
+       ; return (fun, fun_ty') }
 
 ----------------
-tcArgs :: LHsExpr Name                          -- The function (for error messages)
-       -> [LHsExpr Name] -> [TcSigmaType]       -- Actual arguments and expected arg types
-       -> TcM [LHsExpr TcId]                    -- Resulting args
-
-tcArgs fun args expected_arg_tys
-  = mapM (tcArg fun) (zip3 args expected_arg_tys [1..])
+-- | Type-check the arguments to a function, possibly including visible type
+-- applications
+tcArgs :: LHsExpr Name   -- ^ The function itself (for err msgs only)
+       -> TcSigmaType    -- ^ the (uninstantiated) type of the function
+       -> CtOrigin       -- ^ the origin for the function's type
+       -> [LHsExpr Name] -- ^ the args
+       -> SDoc           -- ^ the herald for matchActualFunTys
+       -> TcM (HsWrapper, [LHsExpr TcId], TcSigmaType)
+          -- ^ (a wrapper for the function, the tc'd args, result type)
+tcArgs fun orig_fun_ty fun_orig orig_args herald
+  = go [] 1 orig_fun_ty orig_args
+  where
+    orig_arity = length orig_args
+
+    go _ _ fun_ty [] = return (idHsWrapper, [], fun_ty)
+
+    go acc_args n fun_ty (arg:args)
+      | Just hs_ty_arg <- isLHsTypeExpr_maybe arg
+      = do { (wrap1, upsilon_ty) <- topInstantiateInferred fun_orig fun_ty
+               -- wrap1 :: fun_ty "->" upsilon_ty
+           ; case tcSplitForAllTy_maybe upsilon_ty of
+               Just (binder, inner_ty)
+                 | Just tv <- binderVar_maybe binder ->
+                 ASSERT( binderVisibility binder == Specified )
+                 do { let kind = tyVarKind tv
+                    ; ty_arg <- tcHsTypeApp hs_ty_arg kind
+                    ; let insted_ty = substTyWith [tv] [ty_arg] inner_ty
+                    ; (inner_wrap, args', res_ty)
+                        <- go acc_args (n+1) insted_ty args
+                   -- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty
+                    ; let inst_wrap = mkWpTyApps [ty_arg]
+                    ; return ( inner_wrap <.> inst_wrap <.> wrap1
+                             , L (getLoc arg) (HsTypeOut hs_ty_arg) : args'
+                             , res_ty ) }
+               _ -> ty_app_err upsilon_ty hs_ty_arg }
+
+      | otherwise   -- not a type application.
+      = do { (wrap, [arg_ty], res_ty)
+               <- matchActualFunTysPart herald fun_orig 1 fun_ty
+                                        acc_args orig_arity
+               -- wrap :: fun_ty "->" arg_ty -> res_ty
+           ; arg' <- tcArg fun (arg, arg_ty, n)
+           ; (inner_wrap, args', inner_res_ty)
+               <- go (arg_ty : acc_args) (n+1) res_ty args
+               -- inner_wrap :: res_ty "->" (map typeOf args') -> inner_res_ty
+           ; return ( mkWpFun idHsWrapper inner_wrap arg_ty res_ty <.> wrap
+                    , arg' : args'
+                    , inner_res_ty ) }
+
+    ty_app_err ty arg
+      = do { (_, ty) <- zonkTidyTcType emptyTidyEnv ty
+           ; failWith $
+               text "Cannot not apply expression of type" <+> quotes (ppr ty) $$
+               text "to a visible type argument" <+> quotes (ppr arg) }
 
 ----------------
 tcArg :: LHsExpr Name                           -- The function (for error messages)
@@ -1127,23 +1197,16 @@ tcTupArgs args tys
     go (L l (Present expr), arg_ty) = do { expr' <- tcPolyExpr expr arg_ty
                                          ; return (L l (Present expr')) }
 
-----------------
-unifyOpFunTysWrap :: LHsExpr Name -> Arity -> TcRhoType
-                  -> TcM (TcCoercion, [TcSigmaType], TcRhoType)
--- A wrapper for matchExpectedFunTys
-unifyOpFunTysWrap op arity ty = matchExpectedFunTys herald arity ty
-  where
-    herald = ptext (sLit "The operator") <+> quotes (ppr op) <+> ptext (sLit "takes")
-
 ---------------------------
 tcSyntaxOp :: CtOrigin -> HsExpr Name -> TcType -> TcM (HsExpr TcId)
 -- Typecheck a syntax operator, checking that it has the specified type
 -- The operator is always a variable at this stage (i.e. renamer output)
 -- This version assumes res_ty is a monotype
 tcSyntaxOp orig (HsVar (L _ op)) res_ty
-  = do { (expr, rho) <- tcInferIdWithOrig orig (nameRdrName op) op
-       ; tcWrapResult expr rho res_ty }
-tcSyntaxOp _ other _ = pprPanic "tcSyntaxOp" (ppr other)
+  = do { (expr, rho) <- tcInferId op
+       ; tcWrapResultO orig expr rho res_ty }
+
+tcSyntaxOp _ other         _      = pprPanic "tcSyntaxOp" (ppr other)
 
 {-
 Note [Push result type in]
@@ -1170,7 +1233,6 @@ With the change, f1 will type-check, because the 'Char' info from
 the signature is propagated into MkQ's argument. With the check
 in the other order, the extra signature in f2 is reqd.
 
-
 ************************************************************************
 *                                                                      *
                 Expressions with a type signature
@@ -1209,11 +1271,11 @@ tcExprSig expr sig@(TISI { sig_bndr  = s_bndr
        ; tau <- zonkTcType tau
        ; let inferred_theta = map evVarPred givens
              tau_tvs        = tyCoVarsOfType tau
-       ; (my_tv_set, my_theta) <- chooseInferredQuantifiers inferred_theta tau_tvs (Just sig)
-       ; let my_tvs = filter (`elemVarSet` my_tv_set) qtvs   -- Maintain original order
-             inferred_sigma = mkInvSigmaTy qtvs   inferred_theta tau
-             my_sigma       = mkInvSigmaTy my_tvs my_theta       tau
-       ; wrap <- if inferred_sigma `eqType` my_sigma
+       ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta
+                                   tau_tvs qtvs (Just sig)
+       ; let inferred_sigma = mkInvSigmaTy qtvs inferred_theta tau
+             my_sigma       = mkForAllTys binders (mkPhiTy  my_theta tau)
+       ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis.
                  then return idHsWrapper  -- Fast path; also avoids complaint when we infer
                                           -- an ambiguouse type and have AllowAmbiguousType
                                           -- e..g infer  x :: forall a. F a -> Int
@@ -1223,7 +1285,7 @@ tcExprSig expr sig@(TISI { sig_bndr  = s_bndr
                          <.> mkWpTyLams qtvs
                          <.> mkWpLams givens
                          <.> mkWpLet  ev_binds
-       ; return (mkLHsWrap poly_wrap expr', mkInvSigmaTy qtvs theta tau) }
+       ; return (mkLHsWrap poly_wrap expr', my_sigma) }
 
   | otherwise = panic "tcExprSig"   -- Can't happen
   where
@@ -1240,15 +1302,14 @@ tcCheckId :: Name -> TcRhoType -> TcM (HsExpr TcId)
 tcCheckId name res_ty
   = do { (expr, actual_res_ty) <- tcInferId name
        ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
-       ; addErrCtxtM (funResCtxt False (HsVar (noLoc name))
-                                 actual_res_ty res_ty) $
-         tcWrapResult expr actual_res_ty res_ty }
+       ; addFunResCtxt False (HsVar (noLoc name)) actual_res_ty res_ty $
+         tcWrapResultO (OccurrenceOf name)  expr actual_res_ty res_ty }
 
 tcCheckRecSelId :: AmbiguousFieldOcc Name -> TcRhoType -> TcM (HsExpr TcId)
-tcCheckRecSelId f@(Unambiguous _ _) res_ty
+tcCheckRecSelId f@(Unambiguous (L _ lbl) _) res_ty
   = do { (expr, actual_res_ty) <- tcInferRecSelId f
-       ; addErrCtxtM (funResCtxt False (HsRecFld f) actual_res_ty res_ty) $
-         tcWrapResult expr actual_res_ty res_ty }
+       ; addFunResCtxt False (HsRecFld f) actual_res_ty res_ty $
+         tcWrapResultO (OccurrenceOfRecSel lbl) expr actual_res_ty res_ty }
 tcCheckRecSelId (Ambiguous lbl _) res_ty
   = case tcSplitFunTy_maybe res_ty of
       Nothing       -> ambiguousSelector lbl
@@ -1256,21 +1317,17 @@ tcCheckRecSelId (Ambiguous lbl _) res_ty
                           ; tcCheckRecSelId (Unambiguous lbl sel_name) res_ty }
 
 ------------------------
-tcInferId :: Name -> TcM (HsExpr TcId, TcRhoType)
--- Infer type, and deeply instantiate
-tcInferId n = tcInferIdWithOrig (OccurrenceOf n) (nameRdrName n) n
-
 tcInferRecSelId :: AmbiguousFieldOcc Name -> TcM (HsExpr TcId, TcRhoType)
 tcInferRecSelId (Unambiguous (L _ lbl) sel)
-  = tcInferIdWithOrig (OccurrenceOfRecSel lbl) lbl sel
+  = do { (expr', ty) <- tc_infer_id lbl sel
+       ; return (expr', ty) }
 tcInferRecSelId (Ambiguous lbl _)
   = ambiguousSelector lbl
 
 ------------------------
-tcInferIdWithOrig :: CtOrigin -> RdrName -> Name ->
-                         TcM (HsExpr TcId, TcRhoType)
--- Look up an occurrence of an Id, and instantiate it (deeply)
-tcInferIdWithOrig orig lbl id_name
+tcInferId :: Name -> TcM (HsExpr TcId, TcSigmaType)
+-- Look up an occurrence of an Id
+tcInferId id_name
   | id_name `hasKey` tagToEnumKey
   = failWithTc (ptext (sLit "tagToEnum# must appear applied to one argument"))
         -- tcApp catches the case (tagToEnum# arg)
@@ -1278,67 +1335,97 @@ tcInferIdWithOrig orig lbl id_name
   | id_name `hasKey` assertIdKey
   = do { dflags <- getDynFlags
        ; if gopt Opt_IgnoreAsserts dflags
-         then tc_infer_id orig lbl id_name
-         else tc_infer_assert orig }
+         then tc_infer_id (nameRdrName id_name) id_name
+         else tc_infer_assert id_name }
 
   | otherwise
-  = tc_infer_id orig lbl id_name
+  = do { (expr, ty) <- tc_infer_id (nameRdrName id_name) id_name
+       ; traceTc "tcInferId" (ppr id_name <+> dcolon <+> ppr ty)
+       ; return (expr, ty) }
 
-tc_infer_assert :: CtOrigin -> TcM (HsExpr TcId, TcRhoType)
+tc_infer_assert :: Name -> TcM (HsExpr TcId, TcSigmaType)
 -- Deal with an occurrence of 'assert'
 -- See Note [Adding the implicit parameter to 'assert']
-tc_infer_assert orig
+tc_infer_assert assert_name
   = do { assert_error_id <- tcLookupId assertErrorName
-       ; (wrap, id_rho) <- deeplyInstantiate orig (idType assert_error_id)
+       ; (wrap, id_rho) <- topInstantiate (OccurrenceOf assert_name)
+                                          (idType assert_error_id)
        ; return (mkHsWrap wrap (HsVar (noLoc assert_error_id)), id_rho)
        }
 
-tc_infer_id :: CtOrigin -> RdrName -> Name -> TcM (HsExpr TcId, TcRhoType)
--- Return type is deeply instantiated
-tc_infer_id orig lbl id_name
+tc_infer_id :: RdrName -> Name -> TcM (HsExpr TcId, TcSigmaType)
+tc_infer_id lbl id_name
  = do { thing <- tcLookup id_name
       ; case thing of
              ATcId { tct_id = id }
                -> do { check_naughty id        -- Note [Local record selectors]
                      ; checkThLocalId id
-                     ; inst_normal_id id }
+                     ; return_id id }
 
              AGlobal (AnId id)
                -> do { check_naughty id
-                     ; inst_normal_id id }
+                     ; return_id id }
                     -- A global cannot possibly be ill-staged
                     -- nor does it need the 'lifting' treatment
                     -- hence no checkTh stuff here
 
              AGlobal (AConLike cl) -> case cl of
-                 RealDataCon con -> inst_data_con con
-                 PatSynCon ps    -> tcPatSynBuilderOcc orig ps
+                 RealDataCon con -> return_data_con con
+                 PatSynCon ps    -> tcPatSynBuilderOcc ps
 
              _ -> failWithTc $
                   ppr thing <+> ptext (sLit "used where a value identifier was expected") }
   where
-    inst_normal_id id
-      = do { (wrap, rho) <- deeplyInstantiate orig (idType id)
-           ; return (mkHsWrap wrap (HsVar (noLoc id)), rho) }
-
-    inst_data_con con
-       -- For data constructors,
-       --   * Must perform the stupid-theta check
-       --   * No need to deeply instantiate because type has all foralls at top
-       = do { let wrap_id           = dataConWrapId con
-                  (tvs, theta, rho) = tcSplitSigmaTy (idType wrap_id)
-            ; (subst, tvs') <- newMetaTyVars tvs
-            ; let tys'   = mkTyVarTys tvs'
-                  theta' = substTheta subst theta
-                  rho'   = substTy subst rho
-            ; wrap <- instCall orig tys' theta'
-            ; addDataConStupidTheta con tys'
-            ; return (mkHsWrap wrap (HsVar (noLoc wrap_id)), rho') }
+    return_id id = return (HsVar (noLoc id), idType id)
+
+    return_data_con con
+       -- For data constructors, must perform the stupid-theta check
+      | null stupid_theta
+      = return_id con_wrapper_id
+
+      | otherwise
+       -- See Note [Instantiating stupid theta]
+      = do { let (tvs, theta, rho) = tcSplitSigmaTy (idType con_wrapper_id)
+           ; (subst, tvs') <- newMetaTyVars tvs
+           ; let tys'   = mkTyVarTys tvs'
+                 theta' = substTheta subst theta
+                 rho'   = substTy subst rho
+           ; wrap <- instCall (OccurrenceOf id_name) tys' theta'
+           ; addDataConStupidTheta con tys'
+           ; return (mkHsWrap wrap (HsVar (noLoc con_wrapper_id)), rho') }
+
+      where
+        con_wrapper_id = dataConWrapId con
+        stupid_theta   = dataConStupidTheta con
 
     check_naughty id
       | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl)
       | otherwise                  = return ()
 
+
+tcUnboundId :: OccName -> TcRhoType -> TcM (HsExpr TcId)
+-- Typechedk an occurrence of an unbound Id
+--
+-- Some of these started life as a true hole "_".  Others might simply
+-- be variables that accidentally have no binding site
+--
+-- We turn all of them into HsVar, since HsUnboundVar can't contain an
+-- Id; and indeed the evidence for the CHoleCan does bind it, so it's
+-- not unbound any more!
+tcUnboundId occ res_ty
+ = do { ty <- newFlexiTyVarTy liftedTypeKind
+      ; name <- newSysName occ
+      ; let ev = mkLocalId name ty
+      ; loc <- getCtLocM HoleOrigin Nothing
+      ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty
+                                              , ctev_dest = EvVarDest ev
+                                              , ctev_loc  = loc}
+                           , cc_occ = occ
+                           , cc_hole = ExprHole }
+      ; emitInsoluble can
+      ; tcWrapResultO (UnboundOccurrenceOf occ) (HsVar (noLoc ev)) ty res_ty }
+
+
 {-
 Note [Adding the implicit parameter to 'assert']
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1374,48 +1461,105 @@ Usually that coercion is hidden inside the wrappers for
 constructors of F [Int] but here we have to do it explicitly.
 
 It's all grotesquely complicated.
+
+Note [Instantiating stupid theta]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Normally, when we infer the type of an Id, we don't instantiate,
+because we wish to allow for visible type application later on.
+But if a datacon has a stupid theta, we're a bit stuck. We need
+to emit the stupid theta constraints with instantiated types. It's
+difficult to defer this to the lazy instantiation, because a stupid
+theta has no spot to put it in a type. So we just instantiate eagerly
+in this case. Thus, users cannot use visible type application with
+a data constructor sporting a stupid theta. I won't feel so bad for
+the users that complain.
+
 -}
 
-tcSeq :: SrcSpan -> Name -> LHsExpr Name -> LHsExpr Name
-      -> TcRhoType -> TcM (HsExpr TcId)
+tcSeq :: SrcSpan -> Name -> [LHsExpr Name]
+      -> TcRhoType -> TcM (HsWrapper, LHsExpr TcId, [LHsExpr TcId])
 -- (seq e1 e2) :: res_ty
 -- We need a special typing rule because res_ty can be unboxed
 -- See Note [Typing rule for seq]
-tcSeq loc fun_name arg1 arg2 res_ty
+tcSeq loc fun_name args res_ty
   = do  { fun <- tcLookupId fun_name
-        ; (arg1', arg1_ty) <- tcInfer (tcMonoExpr arg1)
+        ; (arg1_ty, args1) <- case args of
+            (ty_arg_expr1 : args1)
+              | Just hs_ty_arg1 <- isLHsTypeExpr_maybe ty_arg_expr1
+              -> do { ty_arg1 <- tcHsTypeApp hs_ty_arg1 liftedTypeKind
+                    ; return (ty_arg1, args1) }
+
+            _ -> do { arg_ty1 <- newFlexiTyVarTy liftedTypeKind
+                    ; return (arg_ty1, args) }
+
+        ; (arg1, arg2) <- case args1 of
+            [ty_arg_expr2, term_arg1, term_arg2]
+              | Just hs_ty_arg2 <- isLHsTypeExpr_maybe ty_arg_expr2
+              -> do { lev_ty <- newFlexiTyVarTy levityTy
+                    ; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE lev_ty)
+                                   -- see Note [Typing rule for seq]
+                    ; _ <- unifyType noThing ty_arg2 res_ty
+                    ; return (term_arg1, term_arg2) }
+            [term_arg1, term_arg2] -> return (term_arg1, term_arg2)
+            _ -> too_many_args
+
+        ; arg1' <- tcMonoExpr arg1 arg1_ty
+        ; res_ty <- zonkTcType res_ty   -- just in case we learned something
+                                        -- interesting about it
         ; arg2' <- tcMonoExpr arg2 res_ty
         ; let fun'    = L loc (HsWrap ty_args (HsVar (L loc fun)))
               ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty
-        ; return (HsApp (L loc (HsApp fun' arg1')) arg2') }
+        ; return (idHsWrapper, fun', [arg1', arg2']) }
+  where
+    too_many_args :: TcM a
+    too_many_args
+      = failWith $
+        hang (text "Too many type arguments to seq:")
+           2 (sep (map pprParendExpr args))
 
-tcTagToEnum :: SrcSpan -> Name -> LHsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
+
+tcTagToEnum :: SrcSpan -> Name -> [LHsExpr Name] -> TcRhoType
+            -> TcM (HsWrapper, LHsExpr TcId, [LHsExpr TcId])
 -- tagToEnum# :: forall a. Int# -> a
 -- See Note [tagToEnum#]   Urgh!
-tcTagToEnum loc fun_name arg res_ty
-  = do  { fun <- tcLookupId fun_name
-        ; ty' <- zonkTcType res_ty
-
-        -- Check that the type is algebraic
-        ; let mb_tc_app = tcSplitTyConApp_maybe ty'
-              Just (tc, tc_args) = mb_tc_app
-        ; checkTc (isJust mb_tc_app)
-                  (mk_error ty' doc1)
-
-        -- Look through any type family
-        ; fam_envs <- tcGetFamInstEnvs
-        ; let (rep_tc, rep_args, coi) = tcLookupDataFamInst fam_envs tc tc_args
-             -- coi :: tc tc_args ~R rep_tc rep_args
-
-        ; checkTc (isEnumerationTyCon rep_tc)
-                  (mk_error ty' doc2)
-
-        ; arg' <- tcMonoExpr arg intPrimTy
-        ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar (L loc fun)))
-              rep_ty = mkTyConApp rep_tc rep_args
-
-        ; return (mkHsWrapCoR (mkTcSymCo coi) $ HsApp fun' arg') }
-                  -- coi is a Representational coercion
+tcTagToEnum loc fun_name args res_ty
+  = do { fun <- tcLookupId fun_name
+
+       ; arg <- case args of
+           [ty_arg_expr, term_arg]
+             | Just hs_ty_arg <- isLHsTypeExpr_maybe ty_arg_expr
+             -> do { ty_arg <- tcHsTypeApp hs_ty_arg liftedTypeKind
+                   ; _ <- unifyType noThing ty_arg res_ty
+                     -- other than influencing res_ty, we just
+                     -- don't care about a type arg passed in.
+                     -- So drop the evidence.
+                   ; return term_arg }
+           [term_arg] -> return term_arg
+           _          -> too_many_args
+
+       ; ty' <- zonkTcType res_ty
+
+       -- Check that the type is algebraic
+       ; let mb_tc_app = tcSplitTyConApp_maybe ty'
+             Just (tc, tc_args) = mb_tc_app
+       ; checkTc (isJust mb_tc_app)
+                 (mk_error ty' doc1)
+
+       -- Look through any type family
+       ; fam_envs <- tcGetFamInstEnvs
+       ; let (rep_tc, rep_args, coi)
+               = tcLookupDataFamInst fam_envs tc tc_args
+            -- coi :: tc tc_args ~R rep_tc rep_args
+
+       ; checkTc (isEnumerationTyCon rep_tc)
+                 (mk_error ty' doc2)
+
+       ; arg' <- tcMonoExpr arg intPrimTy
+       ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar (L loc fun)))
+             rep_ty = mkTyConApp rep_tc rep_args
+
+       ; return (mkWpCastR (mkTcSymCo coi), fun', [arg']) }
+                 -- coi is a Representational coercion
   where
     doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature")
                 , ptext (sLit "e.g. (tagToEnum# x) :: Bool") ]
@@ -1427,6 +1571,12 @@ tcTagToEnum loc fun_name arg res_ty
                <+> ptext (sLit "at type") <+> ppr ty)
            2 what
 
+    too_many_args :: TcM a
+    too_many_args
+      = failWith $
+        hang (text "Too many type arguments to tagToEnum#:")
+           2 (sep (map pprParendExpr args))
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1643,7 +1793,7 @@ See also Note [HsRecField and HsRecUpdField] in HsPat.
 -- Given a RdrName that refers to multiple record fields, and the type
 -- of its argument, try to determine the name of the selector that is
 -- meant.
-disambiguateSelector :: Located RdrName -> Type -> RnM Name
+disambiguateSelector :: Located RdrName -> Type -> TcM Name
 disambiguateSelector lr@(L _ rdr) parent_type
  = do { fam_inst_envs <- tcGetFamInstEnvs
       ; case tyConOf fam_inst_envs parent_type of
@@ -1658,7 +1808,7 @@ disambiguateSelector lr@(L _ rdr) parent_type
 
 -- This field name really is ambiguous, so add a suitable "ambiguous
 -- occurrence" error, then give up.
-ambiguousSelector :: Located RdrName -> RnM a
+ambiguousSelector :: Located RdrName -> TcM a
 ambiguousSelector (L _ rdr)
   = do { env <- getGlobalRdrEnv
        ; let gres = lookupGRE_RdrName rdr env
@@ -1667,10 +1817,10 @@ ambiguousSelector (L _ rdr)
 
 -- Disambiguate the fields in a record update.
 -- See Note [Disambiguating record fields]
-disambiguateRecordBinds :: LHsExpr Name -> TcType
+disambiguateRecordBinds :: LHsExpr Name -> TcRhoType
                         -> [LHsRecUpdField Name] -> Type
                         -> TcM [LHsRecField' (AmbiguousFieldOcc Id) (LHsExpr Name)]
-disambiguateRecordBinds record_expr record_tau rbnds res_ty
+disambiguateRecordBinds record_expr record_rho rbnds res_ty
     -- Are all the fields unambiguous?
   = case mapM isUnambiguous rbnds of
                      -- If so, just skip to looking up the Ids
@@ -1718,7 +1868,7 @@ disambiguateRecordBinds record_expr record_tau rbnds res_ty
         -- Does the expression being updated have a type signature?
         -- If so, try to extract a parent TyCon from it
             | Just {} <- obviousSig (unLoc record_expr)
-            , Just tc <- tyConOf fam_inst_envs record_tau
+            , Just tc <- tyConOf fam_inst_envs record_rho
             -> return (RecSelData tc)
 
         -- Nothing else we can try...
@@ -1946,36 +2096,47 @@ fieldCtxt :: FieldLabelString -> SDoc
 fieldCtxt field_name
   = ptext (sLit "In the") <+> quotes (ppr field_name) <+> ptext (sLit "field of a record")
 
-funResCtxt :: Bool  -- There is at least one argument
-           -> HsExpr Name -> TcType -> TcType
-           -> TidyEnv -> TcM (TidyEnv, MsgDoc)
+addFunResCtxt :: Bool  -- There is at least one argument
+              -> HsExpr Name -> TcType -> TcType
+              -> TcM a -> TcM a
 -- When we have a mis-match in the return type of a function
 -- try to give a helpful message about too many/few arguments
 --
 -- Used for naked variables too; but with has_args = False
-funResCtxt has_args fun fun_res_ty env_ty tidy_env
-  = do { fun_res' <- zonkTcType fun_res_ty
-       ; env'     <- zonkTcType env_ty
-       ; let (args_fun, res_fun) = tcSplitFunTys fun_res'
-             (args_env, res_env) = tcSplitFunTys env'
-             n_fun = length args_fun
-             n_env = length args_env
-             info  | n_fun == n_env = Outputable.empty
-                   | n_fun > n_env
-                   , not_fun res_env = ptext (sLit "Probable cause:") <+> quotes (ppr fun)
-                                       <+> ptext (sLit "is applied to too few arguments")
-                   | has_args
-                   , not_fun res_fun = ptext (sLit "Possible cause:") <+> quotes (ppr fun)
-                                       <+> ptext (sLit "is applied to too many arguments")
-                   | otherwise       = Outputable.empty  -- Never suggest that a naked variable is
-                                                         -- applied to too many args!
-       ; return (tidy_env, info) }
+addFunResCtxt has_args fun fun_res_ty env_ty
+  = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg)
+      -- NB: use a landmark error context, so that an empty context
+      -- doesn't suppress some more useful context
   where
-    not_fun ty   -- ty is definitely not an arrow type,
-                 -- and cannot conceivably become one
-      = case tcSplitTyConApp_maybe ty of
-          Just (tc, _) -> isAlgTyCon tc
-          Nothing      -> False
+    mk_msg
+      = do { fun_res' <- zonkTcType fun_res_ty
+           ; env'     <- zonkTcType env_ty
+           ; let (_, _, fun_tau) = tcSplitSigmaTy fun_res'
+                 (_, _, env_tau) = tcSplitSigmaTy env'
+                 (args_fun, res_fun) = tcSplitFunTys fun_tau
+                 (args_env, res_env) = tcSplitFunTys env_tau
+                 n_fun = length args_fun
+                 n_env = length args_env
+                 info  | n_fun == n_env = Outputable.empty
+                       | n_fun > n_env
+                       , not_fun res_env
+                       = ptext (sLit "Probable cause:") <+> quotes (ppr fun)
+                         <+> ptext (sLit "is applied to too few arguments")
+
+                       | has_args
+                       , not_fun res_fun
+                       = ptext (sLit "Possible cause:") <+> quotes (ppr fun)
+                         <+> ptext (sLit "is applied to too many arguments")
+
+                       | otherwise
+                       = Outputable.empty  -- Never suggest that a naked variable is                                         -- applied to too many args!
+           ; return info }
+      where
+        not_fun ty   -- ty is definitely not an arrow type,
+                     -- and cannot conceivably become one
+          = case tcSplitTyConApp_maybe ty of
+              Just (tc, _) -> isAlgTyCon tc
+              Nothing      -> False
 
 badFieldTypes :: [(FieldLabelString,TcType)] -> SDoc
 badFieldTypes prs
index acd5d8a..8d60ba4 100644 (file)
@@ -14,7 +14,11 @@ tcMonoExpr, tcMonoExprNC ::
        -> TcRhoType
        -> TcM (LHsExpr TcId)
 
-tcInferRho, tcInferRhoNC ::
+tcInferSigma, tcInferSigmaNC ::
+          LHsExpr Name
+       -> TcM (LHsExpr TcId, TcSigmaType)
+
+tcInferRho ::
           LHsExpr Name
        -> TcM (LHsExpr TcId, TcRhoType)
 
index 009d203..ad36167 100644 (file)
@@ -1639,10 +1639,10 @@ functorLikeTraverse var (FT { ft_triv = caseTrivial,     ft_var = caseVar
        | otherwise        = (caseWrongArg, True)   -- Non-decomposable (eg type function)
        where
          (xrs,xcs) = unzip (map (go co) args)
-    go co (ForAllTy (Named v Invisible) x) | v /= var && xc = (caseForAll v xr,True)
+    go _  (ForAllTy (Named _ Visible) _) = panic "unexpected visible binder"
+    go co (ForAllTy (Named v _)       x) | v /= var && xc = (caseForAll v xr,True)
         where (xr,xc) = go co x
 
-    go _ (ForAllTy (Named _ Visible) _) = panic "unexpected visible binder"
     go _ _ = (caseTrivial,False)
 
 -- Return all syntactic subterms of ty that contain var somewhere
@@ -2052,7 +2052,7 @@ genAuxBindSpec loc (DerivCon2Tag tycon)
     rdr_name = con2tag_RDR tycon
 
     sig_ty = mkLHsSigWcType $ L loc $ HsCoreTy $
-             mkInvSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $
+             mkSpecSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $
              mkParentType tycon `mkFunTy` intPrimTy
 
     lots_of_constructors = tyConFamilySize tycon > 8
@@ -2076,7 +2076,7 @@ genAuxBindSpec loc (DerivTag2Con tycon)
      L loc (TypeSig [L loc rdr_name] sig_ty))
   where
     sig_ty = mkLHsSigWcType $ L loc $
-             HsCoreTy $ mkInvForAllTys (tyConTyVars tycon) $
+             HsCoreTy $ mkSpecForAllTys (tyConTyVars tycon) $
              intTy `mkFunTy` mkParentType tycon
 
     rdr_name = tag2con_RDR tycon
index ee7038d..210b179 100644 (file)
@@ -320,6 +320,7 @@ zonkTyBndrX :: ZonkEnv -> TyVar -> TcM (ZonkEnv, TyVar)
 zonkTyBndrX env tv
   = ASSERT( isImmutableTyVar tv )
     do { ki <- zonkTcTypeToType env (tyVarKind tv)
+               -- Internal names tidy up better, for iface files.
        ; let tv' = mkTyVar (tyVarName tv) ki
        ; return (extendTyZonkEnv1 env tv', tv') }
 
@@ -433,12 +434,15 @@ zonk_bind env (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs
                           , abs_ev_binds = new_ev_binds
                           , abs_exports = new_exports, abs_binds = new_val_bind }) }
   where
-    zonkExport env (ABE{ abe_wrap = wrap, abe_poly = poly_id
+    zonkExport env (ABE{ abe_wrap = wrap, abe_inst_wrap = inst_wrap
+                       , abe_poly = poly_id
                        , abe_mono = mono_id, abe_prags = prags })
         = do new_poly_id <- zonkIdBndr env poly_id
              (_, new_wrap) <- zonkCoFn env wrap
+             (_, new_inst_wrap) <- zonkCoFn env inst_wrap
              new_prags <- zonkSpecPrags env prags
-             return (ABE{ abe_wrap = new_wrap, abe_poly = new_poly_id
+             return (ABE{ abe_wrap = new_wrap, abe_inst_wrap = new_inst_wrap
+                        , abe_poly = new_poly_id
                         , abe_mono = zonkIdOcc env mono_id
                         , abe_prags = new_prags })
 
@@ -731,6 +735,9 @@ zonkExpr env (HsWrap co_fn expr)
 zonkExpr _ (HsUnboundVar v)
   = return (HsUnboundVar v)
 
+  -- nothing to do here. The payload is an LHsType, not a Type.
+zonkExpr _ e@(HsTypeOut {}) = return e
+
 zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr)
 
 -------------------------------------------------------------------------
@@ -740,10 +747,10 @@ zonkCmd   :: ZonkEnv -> HsCmd TcId    -> TcM (HsCmd Id)
 
 zonkLCmd  env cmd  = wrapLocM (zonkCmd env) cmd
 
-zonkCmd env (HsCmdCast co cmd)
-  = do { co' <- zonkCoToCo env co
-       ; cmd' <- zonkCmd env cmd
-       ; return (HsCmdCast co' cmd') }
+zonkCmd env (HsCmdWrap w cmd)
+  = do { (env1, w') <- zonkCoFn env w
+       ; cmd' <- zonkCmd env1 cmd
+       ; return (HsCmdWrap w' cmd') }
 zonkCmd env (HsCmdArrApp e1 e2 ty ho rl)
   = do new_e1 <- zonkLExpr env e1
        new_e2 <- zonkLExpr env e2
@@ -811,11 +818,10 @@ 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 (WpFun c1 c2 t1) = do { (env1, c1') <- zonkCoFn env c1
+                                   ; (env2, c2') <- zonkCoFn env1 c2
+                                   ; t1'         <- zonkTcTypeToType env2 t1
+                                   ; return (env2, WpFun c1' c2' t1') }
 zonkCoFn env (WpCast co) = do { co' <- zonkCoToCo env co
                               ; return (env, WpCast co') }
 zonkCoFn env (WpEvLam ev)   = do { (env', ev') <- zonkEvBndrX env ev
index 769c45f..6214a8a 100644 (file)
@@ -15,6 +15,7 @@ module TcHsType (
 
         tcHsClsInstType,
         tcHsDeriv, tcHsVectInst,
+        tcHsTypeApp,
         UserTypeCtxt(..),
         tcImplicitTKBndrs, tcImplicitTKBndrsType, tcHsTyVarBndrs,
 
@@ -202,7 +203,7 @@ tc_hs_sig_type (HsIB { hsib_body = hs_ty
   = do { (tkvs, ty) <- solveEqualities $
                        tcImplicitTKBndrsType sig_vars $
                        tc_lhs_type typeLevelMode hs_ty kind
-       ; return (mkInvForAllTys tkvs ty) }
+       ; return (mkSpecForAllTys tkvs ty) }
 
 -----------------
 tcHsDeriv :: LHsSigType Name -> TcM ([TyVar], Class, [Type], Kind)
@@ -244,7 +245,7 @@ tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_vars = sig_vars
                        ; head_ty' <- tc_lhs_type typeLevelMode
                                                  head_ty constraintKind
                        ; return (mkPhiTy theta head_ty') }
-       ; let inst_ty = mkInvForAllTys tkvs phi_ty
+       ; let inst_ty = mkSpecForAllTys tkvs phi_ty
        ; inst_ty <- kindGeneralizeType inst_ty
        ; inst_ty <- zonkTcType inst_ty
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
@@ -267,6 +268,21 @@ tcHsVectInst ty
   | otherwise
   = failWithTc $ ptext (sLit "Malformed instance type")
 
+----------------------------------------------
+-- | Type-check a visible type application
+tcHsTypeApp :: LHsWcType Name -> Kind -> TcM Type
+tcHsTypeApp wc_ty kind
+  | HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty
+  = ASSERT( isNothing extra )  -- handled in RnTypes.rnExtraConstraintWildCard
+    tcWildCardBinders sig_wcs $ \ _ ->
+    do { ty <- tcCheckLHsType hs_ty kind
+       ; ty <- zonkTcType ty
+       ; checkValidType TypeAppCtxt ty
+       ; return ty }
+        -- NB: we don't call emitWildcardHoleConstraints here, because
+        -- we want any holes in visible type applications to be used
+        -- without fuss. No errors, warnings, extensions, etc.
+
 {-
         These functions are used during knot-tying in
         type and class declarations, when we have to
@@ -504,7 +520,7 @@ tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kin
     -- Why exp_kind?  See Note [Body kind of forall]
     do { ty' <- tc_lhs_type mode ty exp_kind
        ; let bound_vars = allBoundVariables ty'
-       ; return (mkNakedInvSigmaTy tvs' [] ty', bound_vars) }
+       ; return (mkNakedSpecSigmaTy tvs' [] ty', bound_vars) }
 
 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
   = do { ctxt' <- tc_hs_context mode ctxt
@@ -1275,12 +1291,15 @@ kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
     do { (full_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs)
        ; let qkvs = filter (not . isMetaTyVar) $
                     tyCoVarsOfTypeWellScoped full_kind
+                      -- these have to be the vars made with new_skolem_tv
+                      -- above. Thus, they are known to the user and should
+                      -- be Specified, not Invisible, when kind-generalizing
 
                 -- the free non-meta variables in the returned kind will
                 -- contain both *mentioned* kind vars and *unmentioned* kind
                 -- vars (See case (1) under Note [Typechecking telescopes])
              gen_kind  = if cusk
-                         then mkInvForAllTys qkvs $ full_kind
+                         then mkSpecForAllTys qkvs $ full_kind
                          else full_kind
        ; return (gen_kind, stuff) } }
   where
index 3b93171..007abf0 100644 (file)
@@ -872,7 +872,8 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                 | otherwise
                 = SpecPrags spec_inst_prags
 
-             export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id
+             export = ABE { abe_wrap = idHsWrapper, abe_inst_wrap = idHsWrapper
+                          , abe_poly = dfun_id
                           , abe_mono = self_dict, abe_prags = dfun_spec_prags }
                           -- NB: see Note [SPECIALISE instance pragmas]
              main_bind = AbsBinds { abs_tvs = inst_tyvars
@@ -986,7 +987,9 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds _fam_envs sc_t
            ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
            ; let sc_top_ty = mkInvForAllTys tyvars (mkPiTypes dfun_evs sc_pred)
                  sc_top_id = mkLocalId sc_top_name sc_top_ty
-                 export = ABE { abe_wrap = idHsWrapper, abe_poly = sc_top_id
+                 export = ABE { abe_wrap = idHsWrapper
+                              , abe_inst_wrap = idHsWrapper
+                              , abe_poly = sc_top_id
                               , abe_mono = sc_ev_id
                               , abe_prags = SpecPrags [] }
                  local_ev_binds = TcEvBinds ev_binds_var
@@ -1318,7 +1321,8 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                         -- method to this version. Note [INLINE and default methods]
 
 
-                 export = ABE { abe_wrap = hs_wrap, abe_poly = meth_id1
+                 export = ABE { abe_wrap = hs_wrap, abe_inst_wrap = idHsWrapper
+                              , abe_poly = meth_id1
                               , abe_mono = local_meth_id
                               , abe_prags = mk_meth_spec_prags meth_id1 spec_inst_prags [] }
                  bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
@@ -1374,10 +1378,11 @@ tcMethodBody clas tyvars dfun_ev_vars inst_tys
                               (L bind_loc lm_bind)
 
         ; let specs  = mk_meth_spec_prags global_meth_id spec_inst_prags spec_prags
-              export = ABE { abe_poly  = global_meth_id
-                           , abe_mono  = local_meth_id
-                           , abe_wrap  = hs_wrap
-                           , abe_prags = specs }
+              export = ABE { abe_poly      = global_meth_id
+                           , abe_mono      = local_meth_id
+                           , abe_wrap      = hs_wrap
+                           , abe_inst_wrap = idHsWrapper
+                           , abe_prags     = specs }
 
               local_ev_binds = TcEvBinds ev_binds_var
               full_bind = AbsBinds { abs_tvs      = tyvars
@@ -1417,7 +1422,7 @@ mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
                   do { inst_sigs <- xoptM LangExt.InstanceSigs
                      ; checkTc inst_sigs (misplacedInstSig sel_name lhs_ty)
                      ; sig_ty  <- tcHsSigType (FunSigCtxt sel_name False) lhs_ty
-                     ; let poly_sig_ty = mkInvSigmaTy tyvars theta sig_ty
+                     ; let poly_sig_ty = mkSpecSigmaTy tyvars theta sig_ty
                            ctxt = FunSigCtxt sel_name True
                      ; tc_sig  <- instTcTySig ctxt lhs_ty sig_ty local_meth_name
                      ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name poly_sig_ty poly_meth_ty) $
@@ -1438,7 +1443,7 @@ mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
     sel_name      = idName sel_id
     sel_occ       = nameOccName sel_name
     local_meth_ty = instantiateMethod clas sel_id inst_tys
-    poly_meth_ty  = mkInvSigmaTy tyvars theta local_meth_ty
+    poly_meth_ty  = mkSpecSigmaTy tyvars theta local_meth_ty
     theta         = map idType dfun_ev_vars
 
 methSigCtxt :: Name -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
index 9285f9a..cacaab2 100644 (file)
@@ -21,11 +21,11 @@ module TcMType (
   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
   newOpenFlexiTyVarTy,
   newReturnTyVar, newReturnTyVarTy,
-  newMaybeReturnTyVarTy,
   newOpenReturnTyVar,
   newMetaKindVar, newMetaKindVars,
   cloneMetaTyVar,
   newFmvTyVar, newFskTyVar,
+  tauTvForReturnTv,
 
   readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
   newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
@@ -632,12 +632,6 @@ newReturnTyVar kind = newAnonMetaTyVar ReturnTv kind
 newReturnTyVarTy :: Kind -> TcM TcType
 newReturnTyVarTy kind = mkTyVarTy <$> newReturnTyVar kind
 
--- | Either makes a normal Flexi or a ReturnTv Flexi
-newMaybeReturnTyVarTy :: Bool  -- True <=> make a ReturnTv
-                      -> Kind -> TcM TcType
-newMaybeReturnTyVarTy True  = newReturnTyVarTy
-newMaybeReturnTyVarTy False = newFlexiTyVarTy
-
 -- | Create a tyvar that can be a lifted or unlifted type.
 newOpenFlexiTyVarTy :: TcM TcType
 newOpenFlexiTyVarTy
@@ -652,6 +646,23 @@ newOpenReturnTyVar
        ; tv <- newReturnTyVar k
        ; return (tv, k) }
 
+-- | If the type is a ReturnTv, fill it with a new meta-TauTv. Otherwise,
+-- no change. This function can look through ReturnTvs and returns a partially
+-- zonked type as an optimisation.
+tauTvForReturnTv :: TcType -> TcM TcType
+tauTvForReturnTv ty
+  | Just tv <- tcGetTyVar_maybe ty
+  , isReturnTyVar tv
+  = do { contents <- readMetaTyVar tv
+       ; case contents of
+           Flexi -> do { tau_ty <- newFlexiTyVarTy (tyVarKind tv)
+                       ; writeMetaTyVar tv tau_ty
+                       ; return tau_ty }
+           Indirect ty -> tauTvForReturnTv ty }
+  | otherwise
+  = ASSERT( all (not . isReturnTyVar) (tyCoVarsOfTypeList ty) )
+    return ty
+
 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
 
@@ -671,9 +682,8 @@ newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 newMetaTyVarX subst tyvar
   = do  { uniq <- newUnique
                -- See Note [Levity polymorphic variables accept foralls]
-        ; let info = if isLevityPolymorphic (tyVarKind tyvar)
-                     then ReturnTv
-                     else TauTv
+        ; let info | isLevityPolymorphic (tyVarKind tyvar) = ReturnTv
+                   | otherwise                             = TauTv
         ; details <- newMetaDetails info
         ; let name   = mkSystemName uniq (getOccName tyvar)
                        -- See Note [Name of an instantiated type variable]
index 323adce..2e4078b 100644 (file)
@@ -9,6 +9,7 @@ TcMatches: Typecheck some @Matches@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TupleSections #-}
 
 module TcMatches ( tcMatchesFun, tcGRHS, tcGRHSsPat, tcMatchesCase, tcMatchLambda,
                    TcMatchCtxt(..), TcStmtChecker, TcExprStmtChecker, TcCmdStmtChecker,
@@ -16,11 +17,10 @@ module TcMatches ( tcMatchesFun, tcGRHS, tcGRHSsPat, tcMatchesCase, tcMatchLambd
                    tcDoStmt, tcGuardStmt
        ) where
 
-import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferRhoNC, tcInferRho, tcCheckId,
-                                tcMonoExpr, tcMonoExprNC, tcPolyExpr )
+import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferSigmaNC, tcInferSigma
+                              , tcCheckId, tcMonoExpr, tcMonoExprNC, tcPolyExpr )
 
 import HsSyn
-import BasicTypes
 import TcRnMonad
 import TcEnv
 import TcPat
@@ -47,6 +47,10 @@ import MkCore
 
 import Control.Monad
 
+#if __GLASGOW_HASKELL__ < 709
+import Data.Traversable ( traverse )
+#endif
+
 #include "HsVersions.h"
 
 {-
@@ -64,7 +68,7 @@ same number of arguments before using @tcMatches@ to do the work.
 Note [Polymorphic expected type for tcMatchesFun]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 tcMatchesFun may be given a *sigma* (polymorphic) type
-so it must be prepared to use tcGen to skolemise it.
+so it must be prepared to use tcSkolemise to skolemise it.
 See Note [sig_tau may be polymorphic] in TcPat.
 -}
 
@@ -83,11 +87,14 @@ tcMatchesFun fun_name matches exp_ty
           traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty)
         ; checkArgs fun_name matches
 
+        ; exp_ty <- tauifyMultipleMatches matches exp_ty
         ; (wrap_gen, (wrap_fun, group))
-            <- tcGen (FunSigCtxt fun_name True) exp_ty $ \ _ exp_rho ->
+            <- tcSkolemise (FunSigCtxt fun_name True) exp_ty $ \ _ exp_rho ->
                   -- Note [Polymorphic expected type for tcMatchesFun]
-               matchFunTys herald arity exp_rho $ \ pat_tys rhs_ty ->
-               tcMatches match_ctxt pat_tys rhs_ty matches
+               do { (wrap_fun, pat_tys, rhs_ty)
+                       <- matchExpectedFunTys herald arity exp_rho
+                  ; matches' <- tcMatches match_ctxt pat_tys rhs_ty matches
+                  ; return (wrap_fun, matches') }
         ; return (wrap_gen <.> wrap_fun, group) }
   where
     arity = matchGroupArity matches
@@ -102,33 +109,38 @@ parser guarantees that each equation has exactly one argument.
 
 tcMatchesCase :: (Outputable (body Name)) =>
                  TcMatchCtxt body                             -- Case context
-              -> TcRhoType                                    -- Type of scrutinee
+              -> TcSigmaType                                  -- Type of scrutinee
               -> MatchGroup Name (Located (body Name))        -- The case alternatives
               -> TcRhoType                                    -- Type of whole case expressions
-              -> TcM (MatchGroup TcId (Located (body TcId)))  -- Translated alternatives
+              -> TcM (MatchGroup TcId (Located (body TcId)))
+                 -- Translated alternatives
+                 -- wrapper goes from MatchGroup's ty to expected ty
 
 tcMatchesCase ctxt scrut_ty matches res_ty
   | isEmptyMatchGroup matches   -- Allow empty case expressions
-  = return (MG { mg_alts = noLoc [], mg_arg_tys = [scrut_ty]
-               , mg_res_ty = res_ty, mg_origin = mg_origin matches })
+  = return (MG { mg_alts = noLoc []
+               , mg_arg_tys = [scrut_ty]
+               , mg_res_ty = res_ty
+               , mg_origin = mg_origin matches })
 
   | otherwise
-  = tcMatches ctxt [scrut_ty] res_ty matches
-
-tcMatchLambda :: MatchGroup Name (LHsExpr Name) -> TcRhoType
-              -> TcM (HsWrapper, MatchGroup TcId (LHsExpr TcId))
-tcMatchLambda match res_ty
-  = matchFunTys herald n_pats res_ty  $ \ pat_tys rhs_ty ->
-    tcMatches match_ctxt pat_tys rhs_ty match
+  = do { res_ty <- tauifyMultipleMatches matches res_ty
+       ; tcMatches ctxt [scrut_ty] res_ty matches }
+
+tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in TcUnify
+              -> TcMatchCtxt HsExpr
+              -> MatchGroup Name (LHsExpr Name)
+              -> TcRhoType   -- deeply skolemised
+              -> TcM (HsWrapper, [TcSigmaType], MatchGroup TcId (LHsExpr TcId))
+                     -- also returns the argument types
+tcMatchLambda herald match_ctxt match res_ty
+  = do { res_ty <- tauifyMultipleMatches match res_ty
+       ; (wrap, pat_tys, rhs_ty) <- matchExpectedFunTys herald n_pats res_ty
+       ; match' <- tcMatches match_ctxt pat_tys rhs_ty match
+       ; return (wrap, pat_tys, match') }
   where
-    n_pats = matchGroupArity match
-    herald = sep [ ptext (sLit "The lambda expression")
-                         <+> quotes (pprSetDepth (PartWay 1) $
-                             pprMatches (LambdaExpr :: HsMatchContext Name) match),
-                        -- The pprSetDepth makes the abstraction print briefly
-                ptext (sLit "has")]
-    match_ctxt = MC { mc_what = LambdaExpr,
-                      mc_body = tcBody }
+    n_pats | isEmptyMatchGroup match = 1   -- must be lambda-case
+           | otherwise               = matchGroupArity match
 
 -- @tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@.
 
@@ -140,29 +152,59 @@ tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss res_ty
     match_ctxt = MC { mc_what = PatBindRhs,
                       mc_body = tcBody }
 
-matchFunTys
-  :: SDoc       -- See Note [Herald for matchExpecteFunTys] in TcUnify
-  -> Arity
-  -> TcRhoType
-  -> ([TcSigmaType] -> TcRhoType -> TcM a)
-  -> TcM (HsWrapper, a)
-
--- Written in CPS style for historical reasons;
--- could probably be un-CPSd, like matchExpectedTyConApp
-
-matchFunTys herald arity res_ty thing_inside
-  = do  { (co, pat_tys, res_ty) <- matchExpectedFunTys herald arity res_ty
-        ; res <- thing_inside pat_tys res_ty
-        ; return (mkWpCastN (mkTcSymCo co), res) }
-
 {-
 ************************************************************************
 *                                                                      *
 \subsection{tcMatch}
 *                                                                      *
 ************************************************************************
+
+Note [Case branches must be taus]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  case ... of
+    ... -> \(x :: forall a. a -> a) -> x
+    ... -> \y -> y
+
+Should that type-check? The problem is that, if we check the second branch
+first, then we'll get a type (b -> b) for the branches, which won't unify
+with the polytype in the first branch. If we check the first branch first,
+then everything is OK. This order-dependency is terrible. So we want only
+proper tau-types in branches. This is what tauTvForReturnsTv ensures:
+it gets rid of those pesky ReturnTvs that might unify with polytypes.
+
+An even trickier case looks like
+
+  f x True  = x undefined
+  f x False = x ()
+
+Here, we see that the arguments must also be non-ReturnTvs. Thus, we must
+tauify before calling matchFunTys.
+
+But we make a special case for a one-branch case. This is so that
+
+  f = \(x :: forall a. a -> a) -> x
+
+still gets assigned a polytype.
 -}
 
+-- | When the MatchGroup has multiple RHSs, convert any ReturnTvs in the
+-- expected type into TauTvs.
+-- See Note [Case branches must be taus]
+tauifyMultipleMatches :: MatchGroup id body
+                      -> TcType
+                      -> TcM TcType
+tauifyMultipleMatches group exp_ty
+  | isSingletonMatchGroup group
+  = return exp_ty
+
+  | otherwise
+  = tauTvForReturnTv exp_ty
+
+-- | Type-check a MatchGroup. If there are multiple RHSs, the expected type
+-- must already be tauified. See Note [Case branches must be taus] and
+-- tauifyMultipleMatches
 tcMatches :: (Outputable (body Name)) => TcMatchCtxt body
           -> [TcSigmaType]      -- Expected pattern types
           -> TcRhoType          -- Expected result-type of the Match.
@@ -176,11 +218,14 @@ data TcMatchCtxt body   -- c.f. TcStmtCtxt, also in this module
                  -> TcRhoType
                  -> TcM (Located (body TcId)) }
 
-tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches, mg_origin = origin })
+tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
+                                  , mg_origin = origin })
   = ASSERT( not (null matches) )        -- Ensure that rhs_ty is filled in
-    do  { matches' <- mapM (tcMatch ctxt pat_tys rhs_ty) matches
-        ; return (MG { mg_alts = L l matches', mg_arg_tys = pat_tys
-                     , mg_res_ty = rhs_ty, mg_origin = origin }) }
+    do { matches' <- mapM (tcMatch ctxt pat_tys rhs_ty) matches
+       ; return (MG { mg_alts = L l matches'
+                    , mg_arg_tys = pat_tys
+                    , mg_res_ty = rhs_ty
+                    , mg_origin = origin }) }
 
 -------------
 tcMatch :: (Outputable (body Name)) => TcMatchCtxt body
@@ -223,8 +268,9 @@ tcGRHSs :: TcMatchCtxt body -> GRHSs Name (Located (body Name)) -> TcRhoType
 -- but we don't need to do that any more
 
 tcGRHSs ctxt (GRHSs grhss (L l binds)) res_ty
-  = do  { (binds', grhss') <- tcLocalBinds binds $
-                              mapM (wrapLocM (tcGRHS ctxt res_ty)) grhss
+  = do  { (binds', grhss')
+            <- tcLocalBinds binds $
+               mapM (wrapLocM (tcGRHS ctxt res_ty)) grhss
 
         ; return (GRHSs grhss' (L l binds')) }
 
@@ -233,8 +279,9 @@ tcGRHS :: TcMatchCtxt body -> TcRhoType -> GRHS Name (Located (body Name))
        -> TcM (GRHS TcId (Located (body TcId)))
 
 tcGRHS ctxt res_ty (GRHS guards rhs)
-  = do  { (guards', rhs') <- tcStmtsAndThen stmt_ctxt tcGuardStmt guards res_ty $
-                             mc_body ctxt rhs
+  = do  { (guards', rhs')
+            <- tcStmtsAndThen stmt_ctxt tcGuardStmt guards res_ty $
+               mc_body ctxt rhs
         ; return (GRHS guards' rhs') }
   where
     stmt_ctxt  = PatGuard (mc_what ctxt)
@@ -280,8 +327,7 @@ tcDoStmts ctxt _ _ = pprPanic "tcDoStmts" (pprStmtContext ctxt)
 tcBody :: LHsExpr Name -> TcRhoType -> TcM (LHsExpr TcId)
 tcBody body res_ty
   = do  { traceTc "tcBody" (ppr res_ty)
-        ; body' <- tcMonoExpr body res_ty
-        ; return body'
+        ; tcMonoExpr body res_ty
         }
 
 {-
@@ -348,9 +394,9 @@ tcStmtsAndThen ctxt stmt_chk (L loc stmt : stmts) res_ty thing_inside
   | otherwise
   = do  { (stmt', (stmts', thing)) <-
                 setSrcSpan loc                              $
-                addErrCtxt (pprStmtInCtxt ctxt stmt)   $
+                addErrCtxt (pprStmtInCtxt ctxt stmt)        $
                 stmt_chk ctxt stmt res_ty                   $ \ res_ty' ->
-                popErrCtxt                             $
+                popErrCtxt                                  $
                 tcStmtsAndThen ctxt stmt_chk stmts res_ty'  $
                 thing_inside
         ; return (L loc stmt' : stmts', thing) }
@@ -366,8 +412,10 @@ tcGuardStmt _ (BodyStmt guard _ _ _) res_ty thing_inside
         ; return (BodyStmt guard' noSyntaxExpr noSyntaxExpr boolTy, thing) }
 
 tcGuardStmt ctxt (BindStmt pat rhs _ _) res_ty thing_inside
-  = do  { (rhs', rhs_ty) <- tcInferRhoNC rhs    -- Stmt has a context already
-        ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat rhs_ty $
+  = do  { (rhs', rhs_ty) <- tcInferSigmaNC rhs
+                                   -- Stmt has a context already
+        ; (pat', thing)  <- tcPat_O (StmtCtxt ctxt) (exprCtOrigin (unLoc rhs))
+                                    pat rhs_ty $
                             thing_inside res_ty
         ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
 
@@ -437,9 +485,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
              --  passed in to tcStmtsAndThen is never looked at
        ; (stmts', (bndr_ids, by'))
             <- tcStmtsAndThen (TransStmtCtxt ctxt) (tcLcStmt m_tc) stmts unused_ty $ \_ -> do
-               { by' <- case by of
-                           Nothing -> return Nothing
-                           Just e  -> do { e_ty <- tcInferRho e; return (Just e_ty) }
+               { by' <- traverse tcInferSigma by
                ; bndr_ids <- tcLookupLocalIds bndr_names
                ; return (bndr_ids, by') }
 
index b951ad2..a5da75c 100644 (file)
@@ -11,12 +11,12 @@ TcPat: Typechecking patterns
 module TcPat ( tcLetPat, TcSigFun
              , TcPragEnv, lookupPragEnv, emptyPragEnv
              , LetBndrSpec(..), addInlinePrags
-             , tcPat, tcPats, newNoSigLetBndr
+             , tcPat, tcPat_O, tcPats, newNoSigLetBndr
              , addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferRho)
+import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferSigma )
 
 import HsSyn
 import TcHsSyn
@@ -67,7 +67,8 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
   = tc_lpat pat pat_ty penv thing_inside
   where
     penv = PE { pe_lazy = True
-              , pe_ctxt = LetPat sig_fn no_gen }
+              , pe_ctxt = LetPat sig_fn no_gen
+              , pe_orig = PatOrigin }
 
 -----------------
 tcPats :: HsMatchContext Name
@@ -90,23 +91,31 @@ tcPats :: HsMatchContext Name
 tcPats ctxt pats pat_tys thing_inside
   = tc_lpats penv pats pat_tys thing_inside
   where
-    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
+    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
 
 tcPat :: HsMatchContext Name
       -> LPat Name -> TcSigmaType
-      -> TcM a                 -- Checker for body, given
-                               -- its result type
+      -> TcM a                     -- Checker for body
       -> TcM (LPat TcId, a)
-tcPat ctxt pat pat_ty thing_inside
+tcPat ctxt = tcPat_O ctxt PatOrigin
+
+-- | A variant of 'tcPat' that takes a custom origin
+tcPat_O :: HsMatchContext Name
+        -> CtOrigin              -- ^ origin to use if the type needs inst'ing
+        -> LPat Name -> TcSigmaType
+        -> TcM a                 -- Checker for body
+        -> TcM (LPat TcId, a)
+tcPat_O ctxt orig pat pat_ty thing_inside
   = tc_lpat pat pat_ty penv thing_inside
   where
-    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
+    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
 
 
 -----------------
 data PatEnv
   = PE { pe_lazy :: Bool        -- True <=> lazy context, so no existentials allowed
        , pe_ctxt :: PatCtxt     -- Context in which the whole pattern appears
+       , pe_orig :: CtOrigin    -- origin to use if the pat_ty needs inst'ing
        }
 
 data PatCtxt
@@ -171,6 +180,8 @@ tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty
 
 tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
   = return (mkTcNomReflCo pat_ty, mkLocalId bndr_name pat_ty)
+               -- whether or not there is a sig is irrelevant, as this
+               -- is local
 
 ------------
 newNoSigLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
@@ -369,26 +380,20 @@ tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside
 
 tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
   = do  {
-         -- Morally, expr must have type `forall a1...aN. OPT' -> B`
+         -- Expr must have type `forall a1...aN. OPT' -> B`
          -- where overall_pat_ty is an instance of OPT'.
-         -- Here, we infer a rho type for it,
-         -- which replaces the leading foralls and constraints
-         -- with fresh unification variables.
-        ; (expr',expr'_inferred) <- tcInferRho expr
+        ; (expr',expr'_inferred) <- tcInferSigma expr
 
          -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
-         -- NOTE: this forces pat_ty to be a monotype (because we use a unification
-         -- variable to find it).  this means that in an example like
-         -- (view -> f)    where view :: _ -> forall b. b
-         -- we will only be able to use view at one instantation in the
-         -- rest of the view
-        ; (expr_co, pat_ty) <- tcInfer $ \ pat_ty ->
-                unifyType (Just expr) expr'_inferred (mkFunTy overall_pat_ty pat_ty)
+        ; (expr_wrap, pat_ty) <- tcInfer $ \ pat_ty ->
+                tcSubTypeDS_O (exprCtOrigin (unLoc expr)) GenSigCtxt (Just expr)
+                              expr'_inferred
+                              (mkFunTy overall_pat_ty pat_ty)
 
          -- pattern must have pat_ty
         ; (pat', res) <- tc_lpat pat pat_ty penv thing_inside
 
-        ; return (ViewPat (mkLHsWrapCo expr_co expr') pat' overall_pat_ty, res) }
+        ; return (ViewPat (mkLHsWrap expr_wrap expr') pat' overall_pat_ty, res) }
 
 -- Type signatures in patterns
 -- See Note [Pattern coercions] below
@@ -403,7 +408,7 @@ tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
 ------------------------
 -- Lists, tuples, arrays
 tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside
-  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTyR pat_ty
+  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv pat_ty
         ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                      pats penv thing_inside
         ; return (mkHsWrapPat coi (ListPat pats' elt_ty Nothing) pat_ty, res)
@@ -412,14 +417,14 @@ tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside
 tc_pat penv (ListPat pats _ (Just (_,e))) pat_ty thing_inside
   = do  { list_pat_ty <- newFlexiTyVarTy liftedTypeKind
         ; e' <- tcSyntaxOp ListOrigin e (mkFunTy pat_ty list_pat_ty)
-        ; (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTyR list_pat_ty
+        ; (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv list_pat_ty
         ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                      pats penv thing_inside
         ; return (mkHsWrapPat coi (ListPat pats' elt_ty (Just (pat_ty,e'))) list_pat_ty, res)
         }
 
 tc_pat penv (PArrPat pats _) pat_ty thing_inside
-  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTyR pat_ty
+  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy penv pat_ty
         ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                      pats penv thing_inside
         ; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res)
@@ -428,7 +433,8 @@ tc_pat penv (PArrPat pats _) pat_ty thing_inside
 tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
   = do  { let arity = length pats
               tc = tupleTyCon boxity arity
-        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConAppR tc) pat_ty
+        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
+                                               penv pat_ty
                      -- Unboxed tuples have levity vars, which we discard:
                      -- See Note [Unboxed tuple levity vars] in TyCon
         ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
@@ -470,9 +476,10 @@ tc_pat _ (LitPat simple_lit) pat_ty thing_inside
 
 ------------------------
 -- Overloaded patterns: n, and n+k
-tc_pat _ (NPat (L l over_lit) mb_neg eq) pat_ty thing_inside
+tc_pat (PE { pe_orig = pat_orig })
+       (NPat (L l over_lit) mb_neg eq) pat_ty thing_inside
   = do  { let orig = LiteralOrigin over_lit
-        ; lit'    <- newOverloadedLit orig over_lit pat_ty
+        ; (wrap, lit') <- newOverloadedLit over_lit pat_ty pat_orig
         ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
         ; mb_neg' <- case mb_neg of
                         Nothing  -> return Nothing      -- Positive literal
@@ -481,18 +488,22 @@ tc_pat _ (NPat (L l over_lit) mb_neg eq) pat_ty thing_inside
                             do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
                                ; return (Just neg') }
         ; res <- thing_inside
-        ; return (NPat (L l lit') mb_neg' eq', res) }
+        ; return (mkHsWrapPat wrap (NPat (L l lit') mb_neg' eq') pat_ty, res) }
 
 tc_pat penv (NPlusKPat (L nm_loc name) (L loc lit) ge minus) pat_ty thing_inside
   = do  { (co, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
         ; let pat_ty' = idType bndr_id
               orig    = LiteralOrigin lit
-        ; lit' <- newOverloadedLit orig lit pat_ty'
+        ; (wrap_lit, lit') <- newOverloadedLit lit pat_ty' (pe_orig penv)
 
         -- The '>=' and '-' parts are re-mappable syntax
         ; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
         ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
-        ; let pat' = NPlusKPat (L nm_loc bndr_id) (L loc lit') ge' minus'
+        ; let pat' = mkHsWrapPat wrap_lit
+                                 (NPlusKPat (L nm_loc bndr_id)
+                                            (L loc lit')
+                                            ge' minus')
+                                 pat_ty
 
         -- The Report says that n+k patterns must be in Integral
         -- We may not want this when using re-mappable syntax, though (ToDo?)
@@ -630,7 +641,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
           -- Instantiate the constructor type variables [a->ty]
           -- This may involve doing a family-instance coercion,
           -- and building a wrapper
-        ; (wrap, ctxt_res_tys) <- matchExpectedPatTy (matchExpectedConTy tycon) pat_ty
+        ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
 
           -- Add the stupid theta
         ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
@@ -750,57 +761,36 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
         ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
 
 ----------------------------
-downgrade :: (TcRhoType -> TcM (TcCoercionN, a))
-          -> TcRhoType -> TcM (TcCoercionR, a)
-downgrade f a = do { (co,res) <- f a; return (mkTcSubCo co, res) }
-
-matchExpectedListTyR :: TcRhoType -> TcM (TcCoercionR, TcRhoType)
-matchExpectedListTyR = downgrade matchExpectedListTy
-matchExpectedPArrTyR :: TcRhoType -> TcM (TcCoercionR, TcRhoType)
-matchExpectedPArrTyR = downgrade matchExpectedPArrTy
-matchExpectedTyConAppR :: TyCon -> TcRhoType -> TcM (TcCoercionR, [TcSigmaType])
-matchExpectedTyConAppR tc = downgrade (matchExpectedTyConApp tc)
-
-----------------------------
-matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionR, a))
-                    -> TcRhoType            -- Type of the pattern
-                    -> TcM (HsWrapper, a)
+-- | Convenient wrapper for calling a matchExpectedXXX function
+matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
+                    -> PatEnv -> TcSigmaType -> TcM (HsWrapper, a)
 -- See Note [Matching polytyped patterns]
 -- Returns a wrapper : pat_ty ~R inner_ty
-matchExpectedPatTy inner_match pat_ty
-  | null tvs && null theta
-  = do { (co, res) <- inner_match pat_ty   -- 'co' is Representational
-       ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr co $$ ppr (isTcReflCo co))
-       ; return (mkWpCastR (mkTcSymCo co), res) }
-         -- The Sym is because the inner_match returns a coercion
-         -- that is the other way round to matchExpectedPatTy
-
-  | otherwise
-  = do { (subst, tvs') <- newMetaTyVars tvs
-       ; wrap1 <- instCall PatOrigin (mkTyVarTys tvs') (substTheta subst theta)
-       ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau)
-       ; return (wrap2 <.> wrap1, arg_tys) }
-  where
-    (tvs, theta, tau) = tcSplitSigmaTy pat_ty
+matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
+  = do { (wrap, pat_rho) <- topInstantiate orig pat_ty
+       ; (co, res) <- inner_match pat_rho
+       ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr wrap)
+       ; return (mkWpCastN (mkTcSymCo co) <.> wrap, res) }
 
 ----------------------------
-matchExpectedConTy :: TyCon      -- The TyCon that this data
+matchExpectedConTy :: PatEnv
+                   -> TyCon      -- The TyCon that this data
                                  -- constructor actually returns
                                  -- In the case of a data family this is
                                  -- the /representation/ TyCon
-                   -> TcRhoType  -- The type of the pattern; in the case
-                                 -- of a data family this would mention
-                                 -- the /family/ TyCon
-                   -> TcM (TcCoercionR, [TcSigmaType])
+                   -> TcSigmaType  -- The type of the pattern; in the case
+                                   -- of a data family this would mention
+                                   -- the /family/ TyCon
+                   -> TcM (HsWrapper, [TcSigmaType])
 -- See Note [Matching constructor patterns]
--- Returns a coercion : T ty1 ... tyn ~R pat_ty
--- This is the same way round as matchExpectedListTy etc
--- but the other way round to matchExpectedPatTy
-matchExpectedConTy data_tc pat_ty
+-- Returns a wrapper : pat_ty "->" T ty1 ... tyn
+matchExpectedConTy (PE { pe_orig = orig }) data_tc pat_ty
   | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
          -- Comments refer to Note [Matching constructor patterns]
          -- co_tc :: forall a. T [a] ~ T7 a
-  = do { (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc)
+  = do { (wrap, pat_ty) <- topInstantiate orig pat_ty
+
+       ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc)
              -- tys = [ty1,ty2]
 
        ; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
@@ -808,16 +798,21 @@ matchExpectedConTy data_tc pat_ty
                                              ppr fam_tc, ppr fam_args])
        ; co1 <- unifyType noThing (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
              -- co1 : T (ty1,ty2) ~N pat_ty
+             -- could use tcSubType here... but it's the wrong way round
+             -- for actual vs. expected in error messages.
 
        ; let tys' = mkTyVarTys tvs'
              co2 = mkTcUnbranchedAxInstCo co_tc tys' []
              -- co2 : T (ty1,ty2) ~R T7 ty1 ty2
 
-       ; return (mkTcSymCo co2 `mkTcTransCo` mkTcSubCo co1, tys') }
+       ; return ( wrap <.> (mkWpCastR $
+                            mkTcSubCo (mkTcSymCo co1) `mkTcTransCo` co2)
+                , tys') }
 
   | otherwise
-  = matchExpectedTyConAppR data_tc pat_ty
-             -- coi : T tys ~R pat_ty
+  = do { (wrap, pat_rho) <- topInstantiate orig pat_ty
+       ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho
+       ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) }
 
 {-
 Note [Matching constructor patterns]
index 5f92250..9444ef2 100644 (file)
@@ -39,7 +39,6 @@ import TcEvidence
 import BuildTyCl
 import VarSet
 import MkId
-import Inst
 import TcTyDecls
 import ConLike
 import FieldLabel
@@ -209,7 +208,7 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
              req_theta  = map evVarPred req_dicts
 
        ; traceTc "tcInferPatSynDecl }" $ ppr name
-       ; tc_patsyn_finish lname dir is_infix lpat'
+       ; tc_patsyn_finish lname dir False {- no sig -} is_infix lpat'
                           (univ_tvs, req_theta,  ev_binds, req_dicts)
                           (ex_tvs,   mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
                           (map nlHsVar args, map idType args)
@@ -268,7 +267,7 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
        -- when that should be impossible
 
        ; traceTc "tcCheckPatSynDecl }" $ ppr name
-       ; tc_patsyn_finish lname dir is_infix lpat'
+       ; tc_patsyn_finish lname dir True {- has a sig -} is_infix lpat'
                           (univ_tvs, req_theta, ev_binds, req_dicts)
                           (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
                           (args', arg_tys)
@@ -365,6 +364,7 @@ wrongNumberOfParmsErr name decl_arity ty_arity
 -- Shared by both tcInferPatSyn and tcCheckPatSyn
 tc_patsyn_finish :: Located Name  -- ^ PatSyn Name
                  -> HsPatSynDir Name  -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
+                 -> Bool              -- ^ True <=> signature provided
                  -> Bool              -- ^ Whether infix
                  -> LPat Id           -- ^ Pattern of the PatSyn
                  -> ([TcTyVar], [PredType], TcEvBinds, [EvVar])
@@ -374,7 +374,7 @@ tc_patsyn_finish :: Located Name  -- ^ PatSyn Name
                  -> [Name]              -- ^ Selector names
                  -- ^ Whether fields, empty if not record PatSyn
                  -> TcM (LHsBinds Id, TcGblEnv)
-tc_patsyn_finish lname dir is_infix lpat'
+tc_patsyn_finish lname dir has_sig is_infix lpat'
                  (univ_tvs, req_theta, req_ev_binds, req_dicts)
                  (ex_tvs, ex_tys, prov_theta, prov_dicts)
                  (args, arg_tys)
@@ -402,7 +402,7 @@ tc_patsyn_finish lname dir is_infix lpat'
            ppr pat_ty
 
        -- Make the 'matcher'
-       ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
+       ; (matcher_id, matcher_bind) <- tcPatSynMatcher has_sig lname lpat'
                                          (univ_tvs, req_theta, req_ev_binds, req_dicts)
                                          (ex_tvs, ex_tys, prov_theta, prov_dicts)
                                          (args, arg_tys)
@@ -410,7 +410,7 @@ tc_patsyn_finish lname dir is_infix lpat'
 
 
        -- Make the 'builder'
-       ; builder_id <- mkPatSynBuilderId dir lname qtvs theta
+       ; builder_id <- mkPatSynBuilderId has_sig dir lname qtvs theta
                                          arg_tys pat_ty
 
          -- TODO: Make this have the proper information
@@ -447,7 +447,8 @@ tc_patsyn_finish lname dir is_infix lpat'
 ************************************************************************
 -}
 
-tcPatSynMatcher :: Located Name
+tcPatSynMatcher :: Bool  -- True <=> signature provided
+                -> Located Name
                 -> LPat Id
                 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
                 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
@@ -455,7 +456,7 @@ tcPatSynMatcher :: Located Name
                 -> TcType
                 -> TcM ((Id, Bool), LHsBinds Id)
 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
-tcPatSynMatcher (L loc name) lpat
+tcPatSynMatcher has_sig (L loc name) lpat
                 (univ_tvs, req_theta, req_ev_binds, req_dicts)
                 (ex_tvs, ex_tys, prov_theta, prov_dicts)
                 (args, arg_tys) pat_ty
@@ -471,10 +472,11 @@ tcPatSynMatcher (L loc name) lpat
              (cont_args, cont_arg_tys)
                | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
                | otherwise   = (args,                 arg_tys)
-             cont_ty = mkInvSigmaTy ex_tvs prov_theta $
+             mk_sigma = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
+             cont_ty = mk_sigma ex_tvs prov_theta $
                        mkFunTys cont_arg_tys res_ty
 
-             fail_ty = mkFunTy voidPrimTy res_ty
+             fail_ty  = mkFunTy voidPrimTy res_ty
 
        ; matcher_name <- newImplicitBinder name mkMatcherOcc
        ; scrutinee    <- newSysLocalId (fsLit "scrut") pat_ty
@@ -555,22 +557,25 @@ isUnidirectional ExplicitBidirectional{} = False
 ************************************************************************
 -}
 
-mkPatSynBuilderId :: HsPatSynDir a -> Located Name
+mkPatSynBuilderId :: Bool  -- True <=> signature provided
+                  -> HsPatSynDir a -> Located Name
                   -> [TyVar] -> ThetaType -> [Type] -> Type
                   -> TcM (Maybe (Id, Bool))
-mkPatSynBuilderId dir  (L _ name) qtvs theta arg_tys pat_ty
+mkPatSynBuilderId has_sig dir  (L _ name) qtvs theta arg_tys pat_ty
   | isUnidirectional dir
   = return Nothing
   | otherwise
   = do { builder_name <- newImplicitBinder name mkBuilderOcc
-       ; let builder_sigma = mkInvSigmaTy qtvs theta (mkFunTys builder_arg_tys pat_ty)
+       ; let mk_sigma      = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
+             builder_sigma = add_void $
+                             mk_sigma qtvs theta (mkFunTys arg_tys pat_ty)
              builder_id    =
               -- See Note [Exported LocalIds] in Id
               mkExportedLocalId VanillaId builder_name builder_sigma
        ; return (Just (builder_id, need_dummy_arg)) }
   where
-    builder_arg_tys | need_dummy_arg = [voidPrimTy]
-                    | otherwise = arg_tys
+    add_void | need_dummy_arg = mkFunTy voidPrimTy
+             | otherwise      = id
     need_dummy_arg = isUnLiftedType pat_ty && null arg_tys && null theta
 
 tcPatSynBuilderBind :: PatSynBind Name Name
@@ -626,7 +631,8 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat
               InfixPatSyn arg1 arg2 -> [arg1, arg2]
               RecordPatSyn args     -> map recordPatSynPatVar args
 
-    add_dummy_arg :: MatchGroup Name (LHsExpr Name) -> MatchGroup Name (LHsExpr Name)
+    add_dummy_arg :: MatchGroup Name (LHsExpr Name)
+                  -> MatchGroup Name (LHsExpr Name)
     add_dummy_arg mg@(MG { mg_alts
                             = L l [L loc (Match NonFunBindMatch [] ty grhss)] })
       = mg { mg_alts
@@ -634,19 +640,20 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat
     add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
                              pprMatches (PatSyn :: HsMatchContext Name) other_mg
 
-tcPatSynBuilderOcc :: CtOrigin -> PatSyn -> TcM (HsExpr TcId, TcRhoType)
--- The result type should be fully instantiated
-tcPatSynBuilderOcc orig ps
+tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
+-- monadic only for failure
+tcPatSynBuilderOcc ps
   | Just (builder_id, add_void_arg) <- builder
-  = do { (wrap, rho) <- deeplyInstantiate orig (idType builder_id)
-       ; let inst_fun = mkHsWrap wrap (HsVar (noLoc builder_id))
-       ; if add_void_arg
-         then return ( HsApp (noLoc inst_fun) (nlHsVar voidPrimId)
-                     , tcFunResultTy rho )
-         else return ( inst_fun, rho ) }
+  , let builder_expr = HsVar (noLoc builder_id)
+        builder_ty   = idType builder_id
+  = return $
+    if add_void_arg
+    then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId)
+         , tcFunResultTy builder_ty )
+    else (builder_expr, builder_ty)
 
   | otherwise  -- Unidirectional
-    = nonBidirectionalErr name
+  = nonBidirectionalErr name
   where
     name    = patSynName ps
     builder = patSynBuilder ps
@@ -836,4 +843,3 @@ tcCollectEx pat = go pat
 
     goRecFd :: LHsRecField Id (LPat Id) -> (TyVarSet, [EvVar])
     goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
-
index 8764c33..823bd38 100644 (file)
@@ -1974,7 +1974,7 @@ tcRnExpr hsc_env rdr_expr
     uniq <- newUnique ;
     let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
     (tclvl, lie, (_tc_expr, res_ty)) <- pushLevelAndCaptureConstraints $
-                                        tcInferRho rn_expr ;
+                                        tcInferSigma rn_expr ;
     ((qtvs, dicts, _), lie_top) <- captureConstraints $
                                    {-# SCC "simplifyInfer" #-}
                                    simplifyInfer tclvl
index f5d5ed5..7ce60bc 100644 (file)
@@ -972,14 +972,26 @@ getErrCtxt = do { env <- getLclEnv; return (tcl_ctxt env) }
 setErrCtxt :: [ErrCtxt] -> TcM a -> TcM a
 setErrCtxt ctxt = updLclEnv (\ env -> env { tcl_ctxt = ctxt })
 
+-- | Add a fixed message to the error context. This message should not
+-- do any tidying.
 addErrCtxt :: MsgDoc -> TcM a -> TcM a
 addErrCtxt msg = addErrCtxtM (\env -> return (env, msg))
 
+-- | Add a message to the error context. This message may do tidying.
 addErrCtxtM :: (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a
 addErrCtxtM ctxt = updCtxt (\ ctxts -> (False, ctxt) : ctxts)
 
+-- | Add a fixed landmark message to the error context. A landmark
+-- message is always sure to be reported, even if there is a lot of
+-- context. It also doesn't count toward the maximum number of contexts
+-- reported.
 addLandmarkErrCtxt :: MsgDoc -> TcM a -> TcM a
-addLandmarkErrCtxt msg = updCtxt (\ctxts -> (True, \env -> return (env,msg)) : ctxts)
+addLandmarkErrCtxt msg = addLandmarkErrCtxtM (\env -> return (env, msg))
+
+-- | Variant of 'addLandmarkErrCtxt' that allows for monadic operations
+-- and tidying.
+addLandmarkErrCtxtM :: (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a
+addLandmarkErrCtxtM ctxt = updCtxt (\ctxts -> (True, ctxt) : ctxts)
 
 -- Helper function for the above
 updCtxt :: ([ErrCtxt] -> [ErrCtxt]) -> TcM a -> TcM a
index 5275f90..d0cf737 100644 (file)
@@ -91,7 +91,8 @@ module TcRnTypes(
         ctLocTypeOrKind_maybe,
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin, setCtLocEnv, setCtLocSpan,
-        CtOrigin(..), ErrorThing(..), mkErrorThing, errorThingNumArgs_maybe,
+        CtOrigin(..), exprCtOrigin, matchesCtOrigin, grhssCtOrigin,
+        ErrorThing(..), mkErrorThing, errorThingNumArgs_maybe,
         TypeOrKind(..), isTypeLevel, isKindLevel,
         pprCtOrigin, pprCtLoc,
         pushErrCtxt, pushErrCtxtSameOrigin,
@@ -164,6 +165,7 @@ import Outputable
 import ListSetOps
 import FastString
 import GHC.Fingerprint
+import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad (ap, liftM, msum)
 #if __GLASGOW_HASKELL__ > 710
@@ -1211,7 +1213,7 @@ instance Outputable TcIdSigInfo where
     ppr (TISI { sig_bndr = bndr, sig_skols = tyvars
               , sig_theta = theta, sig_tau = tau })
         = ppr (tcIdSigBndrName bndr) <+> dcolon <+>
-          vcat [ pprSigmaType (mkInvSigmaTy (map snd tyvars) theta tau)
+          vcat [ pprSigmaType (mkSpecSigmaTy (map snd tyvars) theta tau)
                , ppr (map fst tyvars) ]
 
 instance Outputable TcIdSigBndr where
@@ -2648,12 +2650,16 @@ data CtOrigin
         -- is pinned on the entire error message
 
   | HoleOrigin
-  | UnboundOccurrenceOf RdrName
+  | UnboundOccurrenceOf OccName
   | ListOrigin          -- An overloaded list
   | StaticOrigin        -- A static form
   | FailablePattern (LPat TcId) -- A failable pattern in do-notation for the
                                 -- MonadFail Proposal (MFP). Obsolete when
                                 -- actual desugaring to MonadFail.fail is live.
+  | Shouldn'tHappenOrigin String
+                            -- the user should never see this one,
+                            -- unlesss ImpredicativeTypes is on, where all
+                            -- bets are off
 
 -- | A thing that can be stored for error message generation only.
 -- It is stored with a function to zonk and tidy the thing.
@@ -2695,6 +2701,78 @@ instance Outputable ErrorThing where
 ctoHerald :: SDoc
 ctoHerald = ptext (sLit "arising from")
 
+-- | Extract a suitable CtOrigin from a HsExpr
+exprCtOrigin :: HsExpr Name -> CtOrigin
+exprCtOrigin (HsVar (L _ name)) = OccurrenceOf name
+exprCtOrigin (HsUnboundVar occ) = UnboundOccurrenceOf occ
+exprCtOrigin (HsRecFld f)       = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f)
+exprCtOrigin (HsOverLabel l)    = OverLabelOrigin l
+exprCtOrigin (HsIPVar ip)       = IPOccOrigin ip
+exprCtOrigin (HsOverLit lit)    = LiteralOrigin lit
+exprCtOrigin (HsLit {})         = Shouldn'tHappenOrigin "concrete literal"
+exprCtOrigin (HsLam matches)    = matchesCtOrigin matches
+exprCtOrigin (HsLamCase _ ms)   = matchesCtOrigin ms
+exprCtOrigin (HsApp (L _ e1) _) = exprCtOrigin e1
+exprCtOrigin (OpApp _ (L _ op) _ _) = exprCtOrigin op
+exprCtOrigin (NegApp (L _ e) _) = exprCtOrigin e
+exprCtOrigin (HsPar (L _ e))    = exprCtOrigin e
+exprCtOrigin (SectionL _ _)     = SectionOrigin
+exprCtOrigin (SectionR _ _)     = SectionOrigin
+exprCtOrigin (ExplicitTuple {}) = Shouldn'tHappenOrigin "explicit tuple"
+exprCtOrigin (HsCase _ matches) = matchesCtOrigin matches
+exprCtOrigin (HsIf (Just syn) _ _ _) = exprCtOrigin syn
+exprCtOrigin (HsIf {})          = Shouldn'tHappenOrigin "if expression"
+exprCtOrigin (HsMultiIf _ rhs)  = lGRHSCtOrigin rhs
+exprCtOrigin (HsLet _ (L _ e))  = exprCtOrigin e
+exprCtOrigin (HsDo _ _ _)       = DoOrigin
+exprCtOrigin (ExplicitList {})  = Shouldn'tHappenOrigin "list"
+exprCtOrigin (ExplicitPArr {})  = Shouldn'tHappenOrigin "parallel array"
+exprCtOrigin (RecordCon {})     = Shouldn'tHappenOrigin "record construction"
+exprCtOrigin (RecordUpd {})     = Shouldn'tHappenOrigin "record update"
+exprCtOrigin (ExprWithTySig {}) = ExprSigOrigin
+exprCtOrigin (ExprWithTySigOut {}) = panic "exprCtOrigin ExprWithTySigOut"
+exprCtOrigin (ArithSeq {})      = Shouldn'tHappenOrigin "arithmetic sequence"
+exprCtOrigin (PArrSeq {})       = Shouldn'tHappenOrigin "parallel array sequence"
+exprCtOrigin (HsSCC _ _ (L _ e))= exprCtOrigin e
+exprCtOrigin (HsCoreAnn _ _ (L _ e)) = exprCtOrigin e
+exprCtOrigin (HsBracket {})     = Shouldn'tHappenOrigin "TH bracket"
+exprCtOrigin (HsRnBracketOut {})= Shouldn'tHappenOrigin "HsRnBracketOut"
+exprCtOrigin (HsTcBracketOut {})= panic "exprCtOrigin HsTcBracketOut"
+exprCtOrigin (HsSpliceE {})     = Shouldn'tHappenOrigin "TH splice"
+exprCtOrigin (HsProc {})        = Shouldn'tHappenOrigin "proc"
+exprCtOrigin (HsStatic {})      = Shouldn'tHappenOrigin "static expression"
+exprCtOrigin (HsArrApp {})      = panic "exprCtOrigin HsArrApp"
+exprCtOrigin (HsArrForm {})     = panic "exprCtOrigin HsArrForm"
+exprCtOrigin (HsTick _ (L _ e)) = exprCtOrigin e
+exprCtOrigin (HsBinTick _ _ (L _ e)) = exprCtOrigin e
+exprCtOrigin (HsTickPragma _ _ (L _ e)) = exprCtOrigin e
+exprCtOrigin EWildPat           = panic "exprCtOrigin EWildPat"
+exprCtOrigin (EAsPat {})        = panic "exprCtOrigin EAsPat"
+exprCtOrigin (EViewPat {})      = panic "exprCtOrigin EViewPat"
+exprCtOrigin (ELazyPat {})      = panic "exprCtOrigin ELazyPat"
+exprCtOrigin (HsType {})        = Shouldn'tHappenOrigin "type application"
+exprCtOrigin (HsTypeOut {})     = panic "exprCtOrigin HsTypeOut"
+exprCtOrigin (HsWrap {})        = panic "exprCtOrigin HsWrap"
+
+-- | Extract a suitable CtOrigin from a MatchGroup
+matchesCtOrigin :: MatchGroup Name (LHsExpr Name) -> CtOrigin
+matchesCtOrigin (MG { mg_alts = alts })
+  | L _ [L _ match] <- alts
+  , Match { m_grhss = grhss } <- match
+  = grhssCtOrigin grhss
+
+  | otherwise
+  = Shouldn'tHappenOrigin "multi-way match"
+
+-- | Extract a suitable CtOrigin from guarded RHSs
+grhssCtOrigin :: GRHSs Name (LHsExpr Name) -> CtOrigin
+grhssCtOrigin (GRHSs { grhssGRHSs = lgrhss }) = lGRHSCtOrigin lgrhss
+
+-- | Extract a suitable CtOrigin from a list of guarded RHSs
+lGRHSCtOrigin :: [LGRHS Name (LHsExpr Name)] -> CtOrigin
+lGRHSCtOrigin [L _ (GRHS _ (L _ e))] = exprCtOrigin e
+lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS"
+
 pprCtLoc :: CtLoc -> SDoc
 -- "arising from ... at ..."
 -- Not an instance of Outputable because of the "arising from" prefix
@@ -2758,6 +2836,15 @@ pprCtOrigin (FailablePattern pat)
       $$
       text "(this will become an error a future GHC release)"
 
+pprCtOrigin (Shouldn'tHappenOrigin note)
+  = sdocWithDynFlags $ \dflags ->
+    if xopt LangExt.ImpredicativeTypes dflags
+    then text "a situation created by impredicative types"
+    else
+    vcat [ text "<< This should not appear in error messages. If you see this"
+         , text "in an error message, please report a bug mentioning" <+> quotes (text note) <+> text "at"
+         , text "https://ghc.haskell.org/trac/ghc/wiki/ReportABug >>" ]
+
 pprCtOrigin simple_origin
   = ctoHerald <+> pprCtO simple_origin
 
@@ -2774,7 +2861,7 @@ pprCtO ExprSigOrigin         = ptext (sLit "an expression type signature")
 pprCtO PatSigOrigin          = ptext (sLit "a pattern type signature")
 pprCtO PatOrigin             = ptext (sLit "a pattern")
 pprCtO ViewPatOrigin         = ptext (sLit "a view pattern")
-pprCtO IfOrigin              = ptext (sLit "an if statement")
+pprCtO IfOrigin              = ptext (sLit "an if expression")
 pprCtO (LiteralOrigin lit)   = hsep [ptext (sLit "the literal"), quotes (ppr lit)]
 pprCtO (ArithSeqOrigin seq)  = hsep [ptext (sLit "the arithmetic sequence"), quotes (ppr seq)]
 pprCtO (PArrSeqOrigin seq)   = hsep [ptext (sLit "the parallel array sequence"), quotes (ppr seq)]
index e3b4fa8..bf967ae 100644 (file)
@@ -75,6 +75,7 @@ import TyCoRep
 import FamInst
 import FamInstEnv
 import InstEnv
+import Inst
 import NameEnv
 import PrelNames
 import TysWiredIn
@@ -84,7 +85,6 @@ import Var
 import Module
 import LoadIface
 import Class
-import Inst
 import TyCon
 import CoAxiom
 import PatSyn ( patSynName )
@@ -174,11 +174,12 @@ tcTypedBracket brack@(TExpBr expr) res_ty
                                 -- NC for no context; tcBracket does that
 
        ; meta_ty <- tcTExpTy expr_ty
-       ; co <- unifyType (Just expr) meta_ty res_ty
        ; ps' <- readMutVar ps_ref
        ; texpco <- tcLookupId unsafeTExpCoerceName
-       ; return (mkHsWrapCo co (unLoc (mkHsApp (nlHsTyApp texpco [expr_ty])
-                                               (noLoc (HsTcBracketOut brack ps'))))) }
+       ; tcWrapResultO (Shouldn'tHappenOrigin "TExpBr")
+                       (unLoc (mkHsApp (nlHsTyApp texpco [expr_ty])
+                                              (noLoc (HsTcBracketOut brack ps'))))
+                       meta_ty res_ty }
 tcTypedBracket other_brack _
   = pprPanic "tcTypedBracket" (ppr other_brack)
 
@@ -187,9 +188,9 @@ tcUntypedBracket brack ps res_ty
   = do { traceTc "tc_bracket untyped" (ppr brack $$ ppr ps)
        ; ps' <- mapM tcPendingSplice ps
        ; meta_ty <- tcBrackTy brack
-       ; co <- unifyType (Just brack) meta_ty res_ty
        ; traceTc "tc_bracket done untyped" (ppr meta_ty)
-       ; return (mkHsWrapCo co (HsTcBracketOut brack ps'))  }
+       ; tcWrapResultO (Shouldn'tHappenOrigin "untyped bracket")
+                       (HsTcBracketOut brack ps') meta_ty res_ty }
 
 ---------------
 tcBrackTy :: HsBracket Name -> TcM TcType
@@ -512,7 +513,7 @@ tcTopSpliceExpr :: SpliceType -> TcM (LHsExpr Id) -> TcM (LHsExpr Id)
 -- Note that set the level to Splice, regardless of the original level,
 -- before typechecking the expression.  For example:
 --      f x = $( ...$(g 3) ... )
--- The recursive call to tcMonoExpr will simply expand the
+-- The recursive call to tcPolyExpr will simply expand the
 -- inner escape before dealing with the outer one
 
 tcTopSpliceExpr isTypedSplice tc_action
index 51d6fc7..c17d78b 100644 (file)
@@ -626,10 +626,10 @@ initialRoleEnv1 is_boot annots_env tc
               _                              -> replicate num_exps Nothing
         default_roles = build_default_roles visflags role_annots
 
-        build_default_roles (Invisible : viss) ras
-          = Nominal : build_default_roles viss ras
         build_default_roles (Visible : viss) (m_annot : ras)
           = (m_annot `orElse` default_role) : build_default_roles viss ras
+        build_default_roles (_inv    : viss) ras
+          = Nominal : build_default_roles viss ras
         build_default_roles [] [] = []
         build_default_roles _ _ = pprPanic "initialRoleEnv1 (2)"
                                            (vcat [ppr tc, ppr role_annots])
@@ -885,7 +885,7 @@ mkDefaultMethodIds tycons
   where
     mk_dm_ty :: Class -> Id -> DefMethSpec Type -> Type
     mk_dm_ty _ sel_id VanillaDM        = idType sel_id
-    mk_dm_ty cls _   (GenericDM dm_ty) = mkInvSigmaTy cls_tvs [pred] dm_ty
+    mk_dm_ty cls _   (GenericDM dm_ty) = mkSpecSigmaTy cls_tvs [pred] dm_ty
        where
          cls_tvs = classTyVars cls
          pred    = mkClassPred cls (mkTyVarTys cls_tvs)
@@ -960,18 +960,19 @@ mkOneRecordSelector all_cons idDetails fl
 
     -- Selector type; Note [Polymorphic selectors]
     field_ty   = conLikeFieldType con1 lbl
-    data_tvs   = tyCoVarsOfType data_ty
-    is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tvs)
+    data_tvs   = tyCoVarsOfTypeWellScoped data_ty
+    data_tv_set= mkVarSet data_tvs
+    is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
     (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
-    all_tvs    = varSetElemsWellScoped $ data_tvs `extendVarSetList` field_tvs
     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
-           | otherwise  = ASSERT( all isTyVar all_tvs )
-                          mkInvForAllTys all_tvs            $
+           | otherwise  = mkSpecForAllTys data_tvs          $
                           mkPhiTy (conLikeStupidTheta con1) $   -- Urgh!
-                          mkPhiTy field_theta               $   -- Urgh!
+                          mkFunTy data_ty                   $
+                          mkSpecForAllTys field_tvs         $
+                          mkPhiTy field_theta               $
                           -- req_theta is empty for normal DataCon
                           mkPhiTy req_theta                 $
-                          mkFunTy data_ty field_tau
+                          field_tau
 
     -- Make the binding: sel (C2 { fld = x }) = x
     --                   sel (C7 { fld = x }) = x
@@ -1017,7 +1018,8 @@ mkOneRecordSelector all_cons idDetails fl
 
     (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
 
-    inst_tys = substTyVars (mkTopTCvSubst (map eqSpecPair eq_spec)) univ_tvs
+    eq_subst = mkTopTCvSubst (map eqSpecPair eq_spec)
+    inst_tys = substTyVars eq_subst univ_tvs
 
     unit_rhs = mkLHsTupleExpr []
     msg_lit = HsStringPrim "" (fastStringToByteString lbl)
@@ -1025,14 +1027,14 @@ mkOneRecordSelector all_cons idDetails fl
 {-
 Note [Polymorphic selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When a record has a polymorphic field, we pull the foralls out to the front.
-   data T = MkT { f :: forall a. [a] -> a }
-Then f :: forall a. T -> [a] -> a
-NOT  f :: T -> forall a. [a] -> a
-
-This is horrid.  It's only needed in deeply obscure cases, which I hate.
-The only case I know is test tc163, which is worth looking at.  It's far
-from clear that this test should succeed at all!
+We take care to build the type of a polymorphic selector in the right
+order, so that visible type application works.
+
+  data Ord a => T a = MkT { field :: forall b. (Num a, Show b) => (a, b) }
+
+We want
+
+  field :: forall a. Ord a => T a -> forall b. (Num a, Show b) => (a, b)
 
 Note [Naughty record selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index 879f977..97865f4 100644 (file)
@@ -32,9 +32,8 @@ module TcType (
   -- MetaDetails
   UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt, isSigMaybe,
   TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
-  MetaDetails(Flexi, Indirect), MetaInfo(..),
-  isImmutableTyVar, isSkolemTyVar,
-  isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
+  MetaDetails(Flexi, Indirect), MetaInfo(..), TauTvFlavour(..),
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
   isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
   isFskTyVar, isFmvTyVar, isFlattenTyVar, isReturnTyVar,
   isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
@@ -46,14 +45,15 @@ module TcType (
 
   --------------------------------
   -- Builders
-  mkPhiTy, mkInvSigmaTy, mkSigmaTy,
+  mkPhiTy, mkInvSigmaTy, mkSpecSigmaTy, mkSigmaTy,
   mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy, mkNakedFunTy,
-  mkNakedInvSigmaTy, mkNakedCastTy, mkNakedPhiTy,
+  mkNakedSpecSigmaTy, mkNakedCastTy, mkNakedPhiTy,
 
   --------------------------------
   -- Splitters
   -- These are important because they do not look through newtypes
   getTyVar,
+  tcSplitForAllTy_maybe,
   tcSplitForAllTys, tcSplitPiTys, tcSplitNamedPiTys,
   tcSplitPhiTy, tcSplitPredFunTy_maybe,
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
@@ -126,11 +126,12 @@ module TcType (
   -- Rexported from Type
   Type, PredType, ThetaType, TyBinder, VisibilityFlag(..),
 
-  mkForAllTy, mkForAllTys, mkInvForAllTys, mkNamedForAllTy,
+  mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, mkNamedForAllTy,
   mkFunTy, mkFunTys,
   mkTyConApp, mkAppTy, mkAppTys, applyTys,
   mkTyConTy, mkTyVarTy,
   mkTyVarTys,
+  mkNamedBinder,
 
   isClassPred, isEqPred, isNomEqPred, isIPPred,
   mkClassPred,
@@ -389,6 +390,10 @@ instance Outputable MetaDetails where
   ppr Flexi         = ptext (sLit "Flexi")
   ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
 
+data TauTvFlavour
+  = VanillaTau
+  | WildcardTau    -- ^ A tyvar that originates from a type wildcard.
+
 data MetaInfo
    = TauTv         -- This MetaTv is an ordinary unification variable
                    -- A TauTv is always filled in with a tau-type, which
@@ -428,7 +433,7 @@ data UserTypeCtxt
 
   | InfSigCtxt Name     -- Inferred type for function
   | ExprSigCtxt         -- Expression type signature
-
+  | TypeAppCtxt         -- Visible type application
   | ConArgCtxt Name     -- Data constructor argument
   | TySynCtxt Name      -- RHS of a type synonym decl
   | PatSynCtxt Name     -- Type sig for a pattern synonym
@@ -615,6 +620,7 @@ pprUserTypeCtxt (FunSigCtxt n _)  = ptext (sLit "the type signature for") <+> qu
 pprUserTypeCtxt (InfSigCtxt n)    = ptext (sLit "the inferred type for") <+> quotes (ppr n)
 pprUserTypeCtxt (RuleSigCtxt n)   = ptext (sLit "a RULE for") <+> quotes (ppr n)
 pprUserTypeCtxt ExprSigCtxt       = ptext (sLit "an expression type signature")
+pprUserTypeCtxt TypeAppCtxt       = ptext (sLit "a type argument")
 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 (PatSynCtxt c)    = ptext (sLit "the type signature for pattern synonym") <+> quotes (ppr c)
@@ -967,6 +973,12 @@ mkInvSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 mkInvSigmaTy tyvars
   = mkSigmaTy (zipWith mkNamedBinder tyvars (repeat Invisible))
 
+-- | Make a sigma ty where all type variables are "specified". That is,
+-- they can be used with visible type application
+mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
+mkSpecSigmaTy tyvars
+  = mkSigmaTy (zipWith mkNamedBinder tyvars (repeat Specified))
+
 mkPhiTy :: [PredType] -> Type -> Type
 mkPhiTy = mkFunTys
 
@@ -974,10 +986,10 @@ mkNakedSigmaTy :: [TyBinder] -> [PredType] -> Type -> Type
 -- See Note [Type-checking inside the knot] in TcHsType
 mkNakedSigmaTy bndrs theta tau = mkForAllTys bndrs (mkNakedPhiTy theta tau)
 
-mkNakedInvSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
+mkNakedSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 -- See Note [Type-checking inside the knot] in TcHsType
-mkNakedInvSigmaTy tyvars
-  = mkNakedSigmaTy (zipWith mkNamedBinder tyvars (repeat Invisible))
+mkNakedSpecSigmaTy tyvars
+  = mkNakedSigmaTy (zipWith mkNamedBinder tyvars (repeat Specified))
 
 mkNakedPhiTy :: [PredType] -> Type -> Type
 -- See Note [Type-checking inside the knot] in TcHsType
@@ -1063,6 +1075,11 @@ variables.  It's up to you to make sure this doesn't matter.
 tcSplitPiTys :: Type -> ([TyBinder], Type)
 tcSplitPiTys = splitPiTys
 
+tcSplitForAllTy_maybe :: Type -> Maybe (TyBinder, Type)
+tcSplitForAllTy_maybe ty | Just ty' <- coreView ty = tcSplitForAllTy_maybe ty'
+tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
+tcSplitForAllTy_maybe _                = Nothing
+
 -- | Like 'tcSplitPiTys', but splits off only named binders, returning
 -- just the tycovars.
 tcSplitForAllTys :: Type -> ([TyVar], Type)
@@ -1310,8 +1327,8 @@ tcEqTypeVis ty1 ty2
 (<!>) :: Maybe VisibilityFlag -> Maybe VisibilityFlag -> Maybe VisibilityFlag
 Nothing        <!> x            = x
 Just Visible   <!> _            = Just Visible
-Just Invisible <!> Just Visible = Just Visible
-Just Invisible <!> _            = Just Invisible
+Just _inv      <!> Just Visible = Just Visible
+Just inv       <!> _            = Just inv
 infixr 3 <!>
 
 -- | Real worker for 'tcEqType'. No kind check!
@@ -1578,7 +1595,7 @@ occurCheckExpand dflags tv ty
 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
 canUnifyWithPolyType dflags details
   = case details of
-      MetaTv { mtv_info = ReturnTv } -> True      -- See Note [ReturnTv]
+      MetaTv { mtv_info = ReturnTv } -> True   -- See Note [ReturnTv]
       MetaTv { mtv_info = SigTv }    -> False
       MetaTv { mtv_info = TauTv }    -> xopt LangExt.ImpredicativeTypes dflags
       _other                         -> True
@@ -1992,6 +2009,40 @@ to_tc_type = mapType to_tc_mapper
 \subsection{Misc}
 *                                                                      *
 ************************************************************************
+
+Note [Visible type application]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC implements a generalisation of the algorithm described in the
+"Visible Type Application" paper (available from
+http://www.cis.upenn.edu/~sweirich/publications.html). A key part
+of that algorithm is to distinguish user-specified variables from inferred
+variables. For example, the following should typecheck:
+
+  f :: forall a b. a -> b -> b
+  f = const id
+
+  g = const id
+
+  x = f @Int @Bool 5 False
+  y = g 5 @Bool False
+
+The idea is that we wish to allow visible type application when we are
+instantiating a specified, fixed variable. In practice, specified, fixed
+variables are either written in a type signature (or
+annotation), OR are imported from another module. (We could do better here,
+for example by doing SCC analysis on parts of a module and considering any
+type from outside one's SCC to be fully specified, but this is very confusing to
+users. The simple rule above is much more straightforward and predictable.)
+
+So, both of f's quantified variables are specified and may be instantiated.
+But g has no type signature, so only id's variable is specified (because id
+is imported). We write the type of g as forall {a}. a -> forall b. b -> b.
+Note that the a is in braces, meaning it cannot be instantiated with
+visible type application.
+
+Tracking specified vs. inferred variables is done conveniently by a field
+in TyBinder.
+
 -}
 
 deNoteType :: Type -> Type
index 51a1eee..b7bc77d 100644 (file)
@@ -6,12 +6,13 @@
 Type subsumption and unification
 -}
 
-{-# LANGUAGE CPP, MultiWayIf #-}
+{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
 
 module TcUnify (
   -- Full-blown subsumption
-  tcWrapResult, tcGen,
-  tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC,
+  tcWrapResult, tcWrapResultO, tcSkolemise,
+  tcSubTypeHR, tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O,
+  tcSubTypeDS_NC, tcSubTypeDS_NC_O,
   checkConstraints, buildImplication, buildImplicationFor,
 
   -- Various unifications
@@ -26,7 +27,7 @@ module TcUnify (
   matchExpectedTyConApp,
   matchExpectedAppTy,
   matchExpectedFunTys,
-
+  matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
   wrapFunResCoercion
@@ -92,7 +93,7 @@ This is used to construct a message of form
 
 Note [matchExpectedFunTys]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
-matchExpectedFunTys checks that an (Expected rho) has the form
+matchExpectedFunTys checks that a sigma has the form
 of an n-ary function.  It passes the decomposed type to the
 thing_inside, and returns a wrapper to coerce between the two types
 
@@ -102,18 +103,77 @@ namely:
         A function definition
      An operator section
 
-This is not (currently) where deep skolemisation occurs;
-matchExpectedFunTys does not skolmise nested foralls in the
-expected type, because it expects that to have been done already
 -}
 
-matchExpectedFunTys :: SDoc     -- See Note [Herald for matchExpectedFunTys]
+-- Use this one when you have an "expected" type.
+matchExpectedFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
                     -> Arity
-                    -> TcRhoType
-                    -> TcM (TcCoercionN, [TcSigmaType], TcRhoType)
-
--- If    matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
--- then  co : ty ~N (t1 -> ... -> tn -> ty_r)
+                    -> TcSigmaType  -- deeply skolemised
+                    -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+-- If    matchExpectedFunTys n ty = (wrap, [t1,..,tn], ty_r)
+-- then  wrap : (t1 -> ... -> tn -> ty_r) "->" ty
+
+-- This function is always called with a deeply skolemised expected result
+-- type. This means that matchActualFunTys will never actually instantiate,
+-- and the returned HsWrapper will be reversible (that is, just a coercion).
+-- So we just piggyback on matchActualFunTys. This is just a bit dodgy, but
+-- it's much better than duplicating all the logic in matchActualFunTys.
+-- To keep expected/actual working out properly, we tell matchActualFunTys
+-- to swap the arguments to unifyType.
+matchExpectedFunTys herald arity ty
+  = ASSERT( is_deeply_skolemised ty )
+    do { (wrap, arg_tys, res_ty)
+           <- match_fun_tys True herald
+                            (Shouldn'tHappenOrigin "matchExpectedFunTys")
+                            arity ty [] arity
+       ; return $
+         case symWrapper_maybe wrap of
+           Just wrap' -> (wrap', arg_tys, res_ty)
+           Nothing    -> pprPanic "matchExpectedFunTys" (ppr wrap $$ ppr ty) }
+  where
+    is_deeply_skolemised (TyVarTy {})    = True
+    is_deeply_skolemised (AppTy {})      = True
+    is_deeply_skolemised (TyConApp {})   = True
+    is_deeply_skolemised (LitTy {})      = True
+    is_deeply_skolemised (CastTy ty _)   = is_deeply_skolemised ty
+    is_deeply_skolemised (CoercionTy {}) = True
+
+    is_deeply_skolemised (ForAllTy (Anon _) res) = is_deeply_skolemised res
+    is_deeply_skolemised (ForAllTy (Named {}) _) = False
+
+matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
+                  -> CtOrigin
+                  -> Arity
+                  -> TcSigmaType
+                  -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+matchActualFunTys herald ct_orig arity ty
+  = matchActualFunTysPart herald ct_orig arity ty [] arity
+
+-- | Variant of 'matchActualFunTys' that works when supplied only part
+-- (that is, to the right of some arrows) of the full function type
+matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
+                      -> CtOrigin
+                      -> Arity
+                      -> TcSigmaType
+                      -> [TcSigmaType] -- reversed args. See (*) below.
+                      -> Arity   -- overall arity of the function, for errs
+                      -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+matchActualFunTysPart = match_fun_tys False
+
+match_fun_tys :: Bool -- True <=> swap the args when unifying,
+                      -- for better expected/actual in error messages;
+                      -- see comments with matchExpectedFunTys
+              -> SDoc
+              -> CtOrigin
+              -> Arity
+              -> TcSigmaType
+              -> [TcSigmaType]
+              -> Arity
+              -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+match_fun_tys swap_tys herald ct_orig arity orig_ty orig_old_args full_arity
+  = go arity orig_old_args orig_ty
+-- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
+-- then  wrap : ty "->" (t1 -> ... -> tn -> ty_r)
 --
 -- Does not allocate unnecessary meta variables: if the input already is
 -- a function, we just take it apart.  Not only is this efficient,
@@ -122,29 +182,54 @@ matchExpectedFunTys :: SDoc     -- See Note [Herald for matchExpectedFunTys]
 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
 -- hide the forall inside a meta-variable
 
-matchExpectedFunTys herald arity orig_ty
-  = go arity orig_ty
-  where
-    -- If     go n ty = (co, [t1,..,tn], ty_r)
-    -- then   co : ty ~ t1 -> .. -> tn -> ty_r
+-- (*) Sometimes it's necessary to call matchActualFunTys with only part
+-- (that is, to the right of some arrows) of the type of the function in
+-- question. (See TcExpr.tcArgs.) This argument is the reversed list of
+-- arguments already seen (that is, not part of the TcSigmaType passed
+-- in elsewhere).
 
-    go n_req ty
-      | n_req == 0 = return (mkTcNomReflCo ty, [], ty)
+  where
+    -- This function has a bizarre mechanic: it accumulates arguments on
+    -- the way down and also builds an argument list on the way up. Why:
+    -- 1. The returns args list and the accumulated args list might be different.
+    --    The accumulated args include all the arg types for the function,
+    --    including those from before this function was called. The returned
+    --    list should include only those arguments produced by this call of
+    --    matchActualFunTys
+    --
+    -- 2. The HsWrapper can be built only on the way up. It seems (more)
+    --    bizarre to build the HsWrapper but not the arg_tys.
+    --
+    -- Refactoring is welcome.
+    go :: Arity
+       -> [TcSigmaType] -- accumulator of arguments (reversed)
+       -> TcSigmaType   -- the remainder of the type as we're processing
+       -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+    go 0 _ ty = return (idHsWrapper, [], ty)
+
+    go n acc_args ty
+      | not (null tvs && null theta)
+      = do { (wrap1, rho) <- topInstantiate ct_orig ty
+           ; (wrap2, arg_tys, res_ty) <- go n acc_args rho
+           ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
+      where
+        (tvs, theta, _) = tcSplitSigmaTy ty
 
-    go n_req ty
-      | Just ty' <- coreView ty = go n_req ty'
+    go n acc_args ty
+      | Just ty' <- coreView ty = go n acc_args ty'
 
-    go n_req (ForAllTy (Anon arg_ty) res_ty)
-      | not (isPredTy arg_ty)
-      = do { (co, tys, ty_r) <- go (n_req-1) res_ty
-           ; return (mkTcFunCo Nominal (mkTcNomReflCo arg_ty) co, arg_ty:tys, ty_r) }
+    go n acc_args (ForAllTy (Anon arg_ty) res_ty)
+      = ASSERT( not (isPredTy arg_ty) )
+        do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
+           ; return ( mkWpFun idHsWrapper wrap_res arg_ty (mkFunTys tys ty_r)
+                    , arg_ty:tys, ty_r ) }
 
-    go n_req ty@(TyVarTy tv)
+    go n acc_args ty@(TyVarTy tv)
       | ASSERT( isTcTyVar tv) isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
-               Indirect ty' -> go n_req ty'
-               Flexi        -> defer n_req ty (isReturnTyVar tv) }
+               Indirect ty' -> go n acc_args ty'
+               Flexi        -> defer n ty (isReturnTyVar tv) }
 
        -- In all other cases we bale out into ordinary unification
        -- However unlike the meta-tyvar case, we are sure that the
@@ -161,19 +246,21 @@ matchExpectedFunTys herald arity orig_ty
        --
        -- But in that case we add specialized type into error context
        -- anyway, because it may be useful. See also Trac #9605.
-    go n_req ty = addErrCtxtM mk_ctxt $
-                  defer n_req ty False
+    go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $
+                       defer n ty False
 
     ------------
     -- If we decide that a ReturnTv (see Note [ReturnTv] in TcType) should
-    -- really be a function type, then we need to allow the argument and
-    -- result types also to be ReturnTvs.
-    defer n_req fun_ty is_return
-      = do { arg_tys <- replicateM n_req new_flexi
-                        -- See Note [Foralls to left of arrow]
+    -- really be a function type, then we need to allow the
+    -- result types also to be a ReturnTv.
+    defer n fun_ty is_return
+      = do { arg_tys <- replicateM n new_flexi
            ; res_ty  <- new_flexi
-           ; co   <- unifyType noThing fun_ty (mkFunTys arg_tys res_ty)
-           ; return (co, arg_tys, res_ty) }
+           ; let unif_fun_ty = mkFunTys arg_tys res_ty
+           ; co <- if swap_tys
+                   then mkTcSymCo <$> unifyType noThing unif_fun_ty fun_ty
+                   else               unifyType noThing fun_ty unif_fun_ty
+           ; return (mkWpCastN co, arg_tys, res_ty) }
       where
         -- preserve ReturnTv-ness
         new_flexi :: TcM TcType
@@ -181,35 +268,26 @@ matchExpectedFunTys herald arity orig_ty
                   | otherwise = newOpenFlexiTyVarTy
 
     ------------
-    mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
-    mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_ty
-                     ; let (args, _) = tcSplitFunTys ty
-                           n_actual = length args
-                           (env'', orig_ty') = tidyOpenType env' orig_ty
-                     ; return (env'', mk_msg orig_ty' ty n_actual) }
-
-    mk_msg orig_ty ty n_args
-      = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
-        if n_args == arity
-          then ptext (sLit "its type is") <+> quotes (pprType orig_ty) <>
+    mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
+    mk_ctxt arg_tys res_ty env
+      = do { let ty = mkFunTys arg_tys res_ty
+           ; (env1, zonked) <- zonkTidyTcType env ty
+                   -- zonking might change # of args
+           ; let (zonked_args, _) = tcSplitFunTys zonked
+                 n_actual         = length zonked_args
+                 (env2, unzonked) = tidyOpenType env1 ty
+           ; return (env2, mk_msg unzonked zonked n_actual) }
+
+    mk_msg full_ty ty n_args
+      = herald <+> speakNOf full_arity (text "argument") <> comma $$
+        if n_args == full_arity
+          then ptext (sLit "its type is") <+> quotes (pprType full_ty) <>
                comma $$
                ptext (sLit "it is specialized to") <+> quotes (pprType ty)
           else sep [ptext (sLit "but its type") <+> quotes (pprType ty),
                     if n_args == 0 then ptext (sLit "has none")
                     else ptext (sLit "has only") <+> speakN n_args]
 
-{-
-Note [Foralls to left of arrow]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-  f (x :: forall a. a -> a) = x
-We give 'f' the type (alpha -> beta), and then want to unify
-the alpha with (forall a. a->a).  We want to the arg and result
-of (->) to be sort-polymorphic, and this also permits foralls, so
-we are ok. See Note [Sort-polymorphic tyvars accept foralls] in TcUnify
-and Note [TYPE] in TysPrim.
--}
-
 ----------------------
 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
 -- Special case for lists
@@ -251,9 +329,9 @@ matchExpectedTyConApp tc orig_ty
        = do { cts <- readMetaTyVar tv
             ; case cts of
                 Indirect ty -> go ty
-                Flexi       -> defer (isReturnTyVar tv) }
+                Flexi       -> defer }
 
-    go _ = defer False
+    go _ = defer
 
     -- If the common case does not occur, instantiate a template
     -- T k1 .. kn t1 .. tm, and unify with the original type
@@ -265,12 +343,12 @@ matchExpectedTyConApp tc orig_ty
     --    (a::*) ~ Maybe
     -- because that'll make types that are utterly ill-kinded.
     -- This happened in Trac #7368
-    defer is_return
+    defer
       = ASSERT2( classifiesTypeWithValues res_kind, ppr tc )
         do { (k_subst, kvs') <- newMetaTyVars kvs
            ; let arg_kinds' = substTys k_subst arg_kinds
                  kappa_tys  = mkTyVarTys kvs'
-           ; tau_tys <- mapM (newMaybeReturnTyVarTy is_return) arg_kinds'
+           ; tau_tys <- mapM newFlexiTyVarTy arg_kinds'
            ; co <- unifyType noThing (mkTyConApp tc (kappa_tys ++ tau_tys)) orig_ty
            ; return (co, kappa_tys ++ tau_tys) }
 
@@ -298,14 +376,14 @@ matchExpectedAppTy orig_ty
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty -> go ty
-               Flexi       -> defer (isReturnTyVar tv) }
+               Flexi       -> defer }
 
-    go _ = defer False
+    go _ = defer
 
     -- Defer splitting by generating an equality constraint
-    defer is_return
-      = do { ty1 <- newMaybeReturnTyVarTy is_return kind1
-           ; ty2 <- newMaybeReturnTyVarTy is_return kind2
+    defer
+      = do { ty1 <- newFlexiTyVarTy kind1
+           ; ty2 <- newFlexiTyVarTy kind2
            ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
@@ -338,11 +416,26 @@ It returns a coercion function
 which takes an HsExpr of type actual_ty into one of type
 expected_ty.
 
+These functions do not actually check for subsumption. They check if
+expected_ty is an appropriate annotation to use for something of type
+actual_ty. This difference matters when thinking about visible type
+application. For example,
+
+   forall a. a -> forall b. b -> b
+      DOES NOT SUBSUME
+   forall a b. a -> b -> b
+
+because the type arguments appear in a different order. (Neither does
+it work the other way around.) BUT, these types are appropriate annotations
+for one another. Because the user directs annotations, it's OK if some
+arguments shuffle around -- after all, it's what the user wants.
+Bottom line: none of this changes with visible type application.
+
 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.
+more predictable type inference.
 
 Wrinkle 1: Note [Deep skolemisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -350,7 +443,7 @@ 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
+That is why tc_sub_type starts with a call to tcSkolemise (which does the
 deep skolemisation), and then calls the DS variant (which assumes
 that expected_ty is deeply skolemised)
 
@@ -367,7 +460,7 @@ 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
+tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of
 HsWrapper.
 
 Another powerful reason for doing this co/contra stuff is visible
@@ -387,30 +480,53 @@ So it's important that we unify beta := forall a. a->a, rather than
 skolemising the type.
 -}
 
-tcSubType :: UserTypeCtxt -> Maybe Id  -- ^ If present, it has type ty_actual
+
+-- | Call this variant when you are in a higher-rank situation and
+-- you know the right-hand type is deeply skolemised.
+tcSubTypeHR :: Outputable a
+            => CtOrigin    -- ^ of the actual type
+            -> Maybe a     -- ^ If present, it has type ty_actual
+            -> TcSigmaType -> TcRhoType -> TcM HsWrapper
+tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
+
+tcSubType :: Outputable a
+          => UserTypeCtxt -> Maybe a  -- ^ If present, it has type ty_actual
           -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
 -- Checks that actual <= expected
 -- Returns HsWrapper :: actual ~ expected
-tcSubType ctxt maybe_id ty_actual ty_expected
+tcSubType ctxt maybe_thing ty_actual ty_expected
   = addSubTypeCtxt ty_actual ty_expected $
     do { traceTc "tcSubType" (vcat [ pprUserTypeCtxt ctxt
-                                   , ppr maybe_id
+                                   , ppr maybe_thing
                                    , ppr ty_actual
                                    , ppr ty_expected ])
-       ; tc_sub_type origin ctxt ty_actual ty_expected }
+       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
   where
     origin = TypeEqOrigin { uo_actual   = ty_actual
                           , uo_expected = ty_expected
-                          , uo_thing    = mkErrorThing <$> maybe_id }
+                          , uo_thing    = mkErrorThing <$> maybe_thing }
 
-tcSubTypeDS :: Outputable a => UserTypeCtxt -> a  -- ^ has type ty_actual
+tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a  -- ^ has type ty_actual
             -> TcSigmaType -> TcRhoType -> TcM HsWrapper
 -- Just like tcSubType, but with the additional precondition that
 -- ty_expected is deeply skolemised (hence "DS")
-tcSubTypeDS ctxt expr ty_actual ty_expected
+tcSubTypeDS ctxt m_expr ty_actual ty_expected
   = addSubTypeCtxt ty_actual ty_expected $
-    tcSubTypeDS_NC ctxt (Just expr) ty_actual ty_expected
-
+    tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected
+
+-- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating
+-- the "actual" type
+tcSubTypeDS_O :: Outputable a
+              => CtOrigin -> UserTypeCtxt
+              -> Maybe a -> TcSigmaType -> TcRhoType
+              -> TcM HsWrapper
+tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected
+  = addSubTypeCtxt ty_actual ty_expected $
+    do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
+                                       , pprUserTypeCtxt ctxt
+                                       , ppr ty_actual
+                                       , ppr ty_expected ])
+       ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected }
 
 addSubTypeCtxt :: TcType -> TcType -> TcM a -> TcM a
 addSubTypeCtxt ty_actual ty_expected thing_inside
@@ -436,7 +552,7 @@ addSubTypeCtxt ty_actual ty_expected thing_inside
 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 }
+       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
   where
     origin = TypeEqOrigin { uo_actual   = ty_actual
                           , uo_expected = ty_expected
@@ -448,57 +564,157 @@ tcSubTypeDS_NC&nbs