Massive simplification: always deeply skolemise
authorRichard Eisenberg <eir@cis.upenn.edu>
Wed, 8 Jul 2015 13:12:34 +0000 (09:12 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Wed, 8 Jul 2015 13:12:34 +0000 (09:12 -0400)
compiler/hsSyn/HsUtils.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcExpr.hs-boot
compiler/typecheck/TcMatches.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRules.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcUnify.hs

index 09ff208..9aba6c9 100644 (file)
@@ -26,7 +26,6 @@ module HsUtils(
   coToHsWrapper, coToHsWrapperR, mkHsDictLet, mkHsLams,
   mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo,
   mkLHsPar, mkHsCmdCast, isLHsTypeExpr_maybe, isLHsTypeExpr,
-  WrappableThing(..),
 
   nlHsTyApp, nlHsTyApps, nlHsVar, nlHsLit, nlHsApp, nlHsApps, nlHsIntLit, nlHsVarApps,
   nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList,
@@ -528,35 +527,6 @@ mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id
 mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr
 
 {-
-************************************************************************
-*                                                                      *
-   WrappableThing
-*                                                                      *
-************************************************************************
-
-This class is used in one place, but it's quite hard to refactor away
-from using a class. The one place is in tcMatches, where we sometimes
-have an HsExpr and sometimes have a HsCmd. We need to wrap one of these
-things, but only if its an HsExpr. Suggestions for refactoring are
-welcome.
-
--}
-
--- | Can this be wrapped by an 'HsWrapper'?
-class WrappableThing thing where
-  wrapThing :: HsWrapper -> thing id -> thing id
-
-instance WrappableThing HsExpr where
-  wrapThing = mkHsWrap
-
--- So, this is a lie. But the whole arrow thing uses only tau-types, and wrappers
--- will come up only in higher-rank situations. So this is safe.
-instance WrappableThing HsCmd where
-  wrapThing wrap cmd
-    = ASSERT( isIdHsWrapper wrap )
-      cmd
-
-{-
 l
 ************************************************************************
 *                                                                      *
index e329e5b..3995f50 100644 (file)
@@ -123,12 +123,11 @@ tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
 -- 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', sigma) <- tcInferSigmaNC expr
+tcInferRhoNC expr
+  = do { (expr', sigma) <- tcInferSigmaNC expr
                     -- TODO (RAE): Fix origin stuff
        ; (wrap, rho) <- topInstantiate AppOrigin sigma
-       ; return (L loc (mkHsWrap wrap expr'), rho) }
+       ; return (mkLHsWrap wrap expr', rho) }
 
 
 {-
@@ -343,7 +342,7 @@ tcExpr (OpApp arg1 op fix arg2) res_ty
                op' fix
                (mkLHsWrapCo co_a arg2') }
 
-tcExpr (OpApp arg1 op fix arg2) res_ty
+  | otherwise
   = do { traceTc "Non Application rule" (ppr op)
        ; (wrap, op', [arg1', arg2']) <- tcApp (Just $ mk_op_msg op) AppOrigin
                                         op [arg1, arg2] res_ty
@@ -412,14 +411,14 @@ tcExpr (ExplicitList _ witness exprs) res_ty
                      ; (coi, elt_ty) <- matchExpectedListTy list_ty
                      ; exprs' <- mapM (tc_elt elt_ty) exprs
                      ; return $ mkHsWrapCo coi (ExplicitList elt_ty (Just fln') exprs') }
-     where tc_elt elt_ty expr = tcMonoExpr expr elt_ty
+     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') }
   where
-    tc_elt elt_ty expr = tcMonoExpr expr elt_ty
+    tc_elt elt_ty expr = tcPolyExpr expr elt_ty
 
 {-
 ************************************************************************
@@ -486,7 +485,7 @@ tcExpr (HsStatic expr) res_ty
             addErrCtxt (hang (ptext (sLit "In the body of a static form:"))
                              2 (ppr expr)
                        ) $
-            tcMonoExprNC expr expr_ty
+            tcPolyExprNC expr expr_ty
         -- Require the type of the argument to be Typeable.
         -- The evidence is not used, but asking the constraint ensures that
         -- the current implementation is as restrictive as future versions
@@ -788,8 +787,8 @@ tcExpr (ArithSeq _ witness seq) res_ty
 
 tcExpr (PArrSeq _ seq@(FromTo expr1 expr2)) res_ty
   = do  { (coi, elt_ty) <- matchExpectedPArrTy res_ty
-        ; expr1' <- tcMonoExpr expr1 elt_ty
-        ; expr2' <- tcMonoExpr expr2 elt_ty
+        ; expr1' <- tcPolyExpr expr1 elt_ty
+        ; expr2' <- tcPolyExpr expr2 elt_ty
         ; enumFromToP <- initDsTc $ dsDPHBuiltin enumFromToPVar
         ; enum_from_to <- newMethodFromName (PArrSeqOrigin seq)
                                  (idName enumFromToP) elt_ty
@@ -797,10 +796,10 @@ tcExpr (PArrSeq _ seq@(FromTo expr1 expr2)) res_ty
                      (PArrSeq enum_from_to (FromTo expr1' expr2')) }
 
 tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
-  = do  { (coi, elt_ty) <- matchExpectedPArrTy Expected res_ty
-        ; expr1' <- tcMonoExpr expr1 elt_ty
-        ; expr2' <- tcMonoExpr expr2 elt_ty
-        ; expr3' <- tcMonoExpr expr3 elt_ty
+  = do  { (coi, elt_ty) <- matchExpectedPArrTy res_ty
+        ; expr1' <- tcPolyExpr expr1 elt_ty
+        ; expr2' <- tcPolyExpr expr2 elt_ty
+        ; expr3' <- tcPolyExpr expr3 elt_ty
         ; enumFromThenToP <- initDsTc $ dsDPHBuiltin enumFromThenToPVar
         ; eft <- newMethodFromName (PArrSeqOrigin seq)
                       (idName enumFromThenToP) elt_ty        -- !!!FIXME: chak
@@ -849,32 +848,32 @@ tcArithSeq :: Maybe (SyntaxExpr Name) -> ArithSeqInfo Name -> TcRhoType
 
 tcArithSeq witness seq@(From expr) res_ty
   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
-       ; expr' <- tcMonoExpr expr elt_ty
+       ; expr' <- tcPolyExpr expr elt_ty
        ; enum_from <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromName elt_ty
        ; return $ mkHsWrapCo coi (ArithSeq enum_from wit' (From expr')) }
 
 tcArithSeq witness seq@(FromThen expr1 expr2) res_ty
   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
-       ; expr1' <- tcMonoExpr expr1 elt_ty
-       ; expr2' <- tcMonoExpr expr2 elt_ty
+       ; expr1' <- tcPolyExpr expr1 elt_ty
+       ; expr2' <- tcPolyExpr expr2 elt_ty
        ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromThenName elt_ty
        ; return $ mkHsWrapCo coi (ArithSeq enum_from_then wit' (FromThen expr1' expr2')) }
 
 tcArithSeq witness seq@(FromTo expr1 expr2) res_ty
   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
-       ; expr1' <- tcMonoExpr expr1 elt_ty
-       ; expr2' <- tcMonoExpr expr2 elt_ty
+       ; expr1' <- tcPolyExpr expr1 elt_ty
+       ; expr2' <- tcPolyExpr expr2 elt_ty
        ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromToName elt_ty
        ; return $ mkHsWrapCo coi (ArithSeq enum_from_to wit' (FromTo expr1' expr2')) }
 
 tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty
   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
-        ; expr1' <- tcMonoExpr expr1 elt_ty
-        ; expr2' <- tcMonoExpr expr2 elt_ty
-        ; expr3' <- tcMonoExpr expr3 elt_ty
+        ; expr1' <- tcPolyExpr expr1 elt_ty
+        ; expr2' <- tcPolyExpr expr2 elt_ty
+        ; expr3' <- tcPolyExpr expr3 elt_ty
         ; eft <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromThenToName elt_ty
         ; return $ mkHsWrapCo coi (ArithSeq eft wit' (FromThenTo expr1' expr2' expr3')) }
@@ -883,7 +882,7 @@ tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty
 arithSeqEltType :: Maybe (SyntaxExpr Name) -> TcRhoType
                 -> TcM (TcCoercionN, TcType, Maybe (SyntaxExpr Id))
 arithSeqEltType Nothing res_ty
-  = do { (coi, elt_ty) <- matchExpectedListTy Expected res_ty
+  = do { (coi, elt_ty) <- matchExpectedListTy res_ty
        ; return (coi, elt_ty, Nothing) }
 arithSeqEltType (Just fl) res_ty
   = do { list_ty <- newFlexiTyVarTy liftedTypeKind
@@ -964,7 +963,7 @@ tcInferFun (L loc (HsVar name))
        ; 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)
@@ -1006,17 +1005,17 @@ tcTupArgs args tys
   = ASSERT( equalLength args tys ) mapM go (args `zip` tys)
   where
     go (L l (Missing {}),   arg_ty) = return (L l (Missing arg_ty))
-    go (L l (Present expr), arg_ty) = do { expr' <- tcMonoExpr expr arg_ty
+    go (L l (Present expr), arg_ty) = do { expr' <- tcPolyExpr expr arg_ty
                                          ; return (L l (Present expr')) }
 
 ---------------------------
-tcSyntaxOp :: CtOrigin -> HsExpr Name -> TcSigmaType -> TcM (HsExpr TcId)
+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 op) res_ty = do { (expr, ty) <- tcInferIdWithOrig orig op
-                                       ; wrap <- tcSubType GenSigCtxt ty res_ty
-                                       ; return (mkHsWrap wrap expr) }
+tcSyntaxOp orig (HsVar op) res_ty = do { (expr, rho) <- tcInferIdWithOrig orig op
+                                       ; tcWrapResult expr rho res_ty }
+
 tcSyntaxOp _ other         _      = pprPanic "tcSyntaxOp" (ppr other)
 
 {-
@@ -1207,7 +1206,7 @@ srcSpanPrimLit dflags span
     = HsLit (HsStringPrim "" (unsafeMkByteString
                              (showSDocOneLine dflags (ppr span))))
 
-tcUnboundId :: OccName -> TcM (HsExpr TcId, TcSigmaType)
+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
@@ -1216,7 +1215,7 @@ tcUnboundId :: OccName -> TcM (HsExpr TcId, TcSigmaType)
 -- 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
+tcUnboundId occ res_ty
  = do { ty <- newFlexiTyVarTy liftedTypeKind
       ; name <- newSysName occ
       ; let ev = mkLocalId name ty
@@ -1224,7 +1223,7 @@ tcUnboundId occ
       ; let can = CHoleCan { cc_ev = CtWanted ty ev loc, cc_occ = occ
                            , cc_hole = ExprHole }
       ; emitInsoluble can
-      ; return (HsVar ev, ty) }
+      ; tcWrapResult (HsVar ev) ty res_ty }
 
 {-
 Note [Adding the implicit parameter to 'assert']
index 7f335b6..7d9319f 100644 (file)
@@ -1,9 +1,14 @@
 module TcExpr where
 import HsSyn    ( HsExpr, LHsExpr )
 import Name     ( Name )
-import TcType   ( TcType, TcRhoType )
+import TcType   ( TcType, TcRhoType, TcSigmaType )
 import TcRnTypes( TcM, TcId, CtOrigin )
 
+tcPolyExpr ::
+          LHsExpr Name
+       -> TcSigmaType
+       -> TcM (LHsExpr TcId)
+
 tcMonoExpr, tcMonoExprNC ::
           LHsExpr Name
        -> TcRhoType
@@ -13,9 +18,13 @@ tcInferSigma, tcInferSigmaNC ::
           LHsExpr Name
        -> TcM (LHsExpr TcId, TcSigmaType)
 
+tcInferRho, tcInferRhoNC ::
+          LHsExpr Name
+       -> TcM (LHsExpr TcId, TcRhoType)
+
 tcSyntaxOp :: CtOrigin
            -> HsExpr Name
            -> TcType
            -> TcM (HsExpr TcId)
 
-tcCheckId :: Name -> TcSigmaType -> TcM (HsExpr TcId)
+tcCheckId :: Name -> TcRhoType -> TcM (HsExpr TcId)
index 5a92c16..0018343 100644 (file)
@@ -14,8 +14,8 @@ module TcMatches ( tcMatchesFun, tcGRHS, tcGRHSsPat, tcMatchesCase, tcMatchLambd
                    tcDoStmt, tcGuardStmt
        ) where
 
-import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferSigmaNC, tcInferSigma,
-                                tcCheckId, tcPolyExpr, tcPolyExprNC )
+import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferSigmaNC, tcInferSigma
+                              , tcCheckId, tcMonoExpr, tcMonoExprNC, tcPolyExpr )
 
 import HsSyn
 import BasicTypes
@@ -56,6 +56,11 @@ import Control.Monad
 is used in error messages.  It checks that all the equations have the
 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 tcSkolemise to skolemise it.
+See Note [sig_tau may be polymorphic] in TcPat.
 -}
 
 tcMatchesFun :: Name -> Bool
@@ -73,8 +78,13 @@ tcMatchesFun fun_name inf matches exp_ty
           traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty)
         ; checkArgs fun_name matches
 
-        ; matchFunTys herald arity exp_ty $ \ pat_tys rhs_ty ->
-          tcMatches match_ctxt pat_tys rhs_ty matches }
+        ; (wrap_gen, (wrap_fun, group))
+            <- tcSkolemise SkolemiseDeeply (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
+        ; return (wrap_gen <.> wrap_fun, group) }
   where
     arity = matchGroupArity matches
     herald = ptext (sLit "The equation(s) for")
@@ -86,11 +96,11 @@ tcMatchesFun fun_name inf matches exp_ty
 parser guarantees that each equation has exactly one argument.
 -}
 
-tcMatchesCase :: (Outputable (body Name), WrappableThing body) =>
+tcMatchesCase :: (Outputable (body Name)) =>
                  TcMatchCtxt body                             -- Case context
               -> TcSigmaType                                  -- Type of scrutinee
               -> MatchGroup Name (Located (body Name))        -- The case alternatives
-              -> TcSigmaType                                  -- Type of whole case expressions
+              -> TcRhoType                                    -- Type of whole case expressions
               -> TcM (MatchGroup TcId (Located (body TcId)))  -- Translated alternatives
 
 tcMatchesCase ctxt scrut_ty matches res_ty
@@ -100,7 +110,7 @@ tcMatchesCase ctxt scrut_ty matches res_ty
   | otherwise
   = tcMatches ctxt [scrut_ty] res_ty matches
 
-tcMatchLambda :: MatchGroup Name (LHsExpr Name) -> TcSigmaType
+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 ->
@@ -125,31 +135,21 @@ 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
-            -> TcSigmaType
-            -> ([TcSigmaType] -> TcSigmaType -> TcM a)
-            -> TcM (HsWrapper, a)
+matchFunTys
+  :: SDoc       -- See Note [Herald for matchExpecteFunTys] in TcUnify
+  -> Arity
+  -> TcRhoType
+  -> ([TcSigmaType] -> TcRhoType -> TcM a)
+  -> TcM (HsWrapper, a)
 
-matchFunTys _herald 0 res_ty thing_inside
- = do { result <- thing_inside [] res_ty
-      ; return (idHsWrapper, result) }
+-- Written in CPS style for historical reasons;
+-- could probably be un-CPSd, like matchExpectedTyConApp
 
 matchFunTys herald arity res_ty thing_inside
-  = do { (wrap1, (wrap2, result)) <-
-           tcSkolemise SkolemiseTop GenSigCtxt res_ty $ \_ res_ty ->
-       do { (fun_wrap, [arg_ty], inner_res_ty) <-
-               matchExpectedFunTys Expected herald 1 res_ty
-               -- fun_wrap :: (arg_ty -> inner_res_ty) "->" res_ty
-          ; (inner_wrap, result) <-
-              matchFunTys herald (arity-1) inner_res_ty $ \arg_tys final_res_ty ->
-              thing_inside (arg_ty:arg_tys) final_res_ty
-              -- inner_wrap ::
-              --   (arg_ty1 ... arg_ty2 -> final_res_ty) "->" inner_res_ty
-          ; return ( fun_wrap <.>
-                     (mkWpFun idHsWrapper inner_wrap arg_ty inner_res_ty)
-                   , result ) }
-       ; return (wrap1 <.> wrap2, result) }
+  = do  { (wrap, pat_tys, res_ty)
+            <- matchExpectedFunTys Expected herald arity res_ty
+        ; res <- thing_inside pat_tys res_ty
+        ; return (wrap, res) }
 
 {-
 ************************************************************************
@@ -159,10 +159,9 @@ matchFunTys herald arity res_ty thing_inside
 ************************************************************************
 -}
 
-tcMatches :: (Outputable (body Name), WrappableThing body)
-          => TcMatchCtxt body
+tcMatches :: (Outputable (body Name)) => TcMatchCtxt body
           -> [TcSigmaType]      -- Expected pattern types
-          -> TcSigmaType        -- Expected result-type of the Match.
+          -> TcRhoType          -- Expected result-type of the Match.
           -> MatchGroup Name (Located (body Name))
           -> TcM (MatchGroup TcId (Located (body TcId)))
 
@@ -175,38 +174,13 @@ data TcMatchCtxt body   -- c.f. TcStmtCtxt, also in this module
 
 tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = matches, mg_origin = origin })
   = ASSERT( not (null matches) )        -- Ensure that rhs_ty is filled in
-    do  { (wrap, (group, tau_co)) <-
-             -- we skolemise the result type and unify it with a TauTv
-             -- so that no one branch takes precedence over others in
-             -- higher-rank situations
-             -- (this is also needed for e.g. typecheck/should_compile/T700)
-             tcSkolemise SkolemiseDeeply GenSigCtxt rhs_ty $ \_ rhs_rho ->
-             do { tau_ty <- newFlexiTyVarTy openTypeKind
-                ; tau_co <- unifyType tau_ty rhs_rho
-                ; tau_ty <- zonkTcType tau_ty
-                ; matches' <- mapM (tcMatch ctxt pat_tys tau_ty) matches
-                ; return (MG { mg_alts    = matches'
-                             , mg_arg_tys = pat_tys
-                             , mg_res_ty  = rhs_ty -- applying the wrapper
-                                                   -- will make this right
-                             , mg_origin  = origin }, tau_co) }
-        ; return (wrap_group (wrap <.> coToHsWrapper tau_co) group) }
-
-  where
-    wrap_group wrap mg
-      | isIdHsWrapper wrap = mg
-      | otherwise          = mg { mg_alts = map (wrap_alt wrap) (mg_alts mg) }
-    wrap_alt wrap (L loc alt)
-      = L loc (alt { m_grhss = wrap_grhss wrap (m_grhss alt) })
-    wrap_grhss wrap grhss
-      = grhss { grhssGRHSs = map (wrap_grhs wrap) (grhssGRHSs grhss) }
-    wrap_grhs wrap (L loc (GRHS guards (L loc' rhs)))
-      = L loc (GRHS guards (L loc' (wrapThing wrap rhs)))
+    do  { matches' <- mapM (tcMatch ctxt pat_tys rhs_ty) matches
+        ; return (MG { mg_alts = matches', mg_arg_tys = pat_tys, mg_res_ty = rhs_ty, mg_origin = origin }) }
 
 -------------
 tcMatch :: (Outputable (body Name)) => TcMatchCtxt body
         -> [TcSigmaType]        -- Expected pattern types
-        -> TcSigmaType          -- Expected result-type of the Match.
+        -> TcRhoType            -- Expected result-type of the Match.
         -> LMatch Name (Located (body Name))
         -> TcM (LMatch TcId (Located (body TcId)))
 
@@ -234,7 +208,7 @@ tcMatch ctxt pat_tys rhs_ty match
             m_ctxt     -> addErrCtxt (pprMatchInCtxt m_ctxt match) thing_inside
 
 -------------
-tcGRHSs :: TcMatchCtxt body -> GRHSs Name (Located (body Name)) -> TcSigmaType
+tcGRHSs :: TcMatchCtxt body -> GRHSs Name (Located (body Name)) -> TcRhoType
         -> TcM (GRHSs TcId (Located (body TcId)))
 
 -- Notice that we pass in the full res_ty, so that we get
@@ -250,7 +224,7 @@ tcGRHSs ctxt (GRHSs grhss binds) res_ty
         ; return (GRHSs grhss' binds') }
 
 -------------
-tcGRHS :: TcMatchCtxt body -> TcSigmaType -> GRHS Name (Located (body Name))
+tcGRHS :: TcMatchCtxt body -> TcRhoType -> GRHS Name (Located (body Name))
        -> TcM (GRHS TcId (Located (body TcId)))
 
 tcGRHS ctxt res_ty (GRHS guards rhs)
@@ -298,10 +272,10 @@ tcDoStmts MonadComp stmts res_ty
 
 tcDoStmts ctxt _ _ = pprPanic "tcDoStmts" (pprStmtContext ctxt)
 
-tcBody :: LHsExpr Name -> TcSigmaType -> TcM (LHsExpr TcId)
+tcBody :: LHsExpr Name -> TcRhoType -> TcM (LHsExpr TcId)
 tcBody body res_ty
   = do  { traceTc "tcBody" (ppr res_ty)
-        ; body' <- tcPolyExpr body res_ty
+        ; body' <- tcMonoExpr body res_ty
         ; return body'
         }
 
@@ -319,8 +293,8 @@ type TcCmdStmtChecker  = TcStmtChecker HsCmd
 type TcStmtChecker body
   =  forall thing. HsStmtContext Name
                 -> Stmt Name (Located (body Name))
-                -> TcSigmaType                    -- Result type for comprehension
-                -> (TcSigmaType -> TcM thing)     -- Checker for what follows the stmt
+                -> TcRhoType                    -- Result type for comprehension
+                -> (TcRhoType -> TcM thing)     -- Checker for what follows the stmt
                 -> TcM (Stmt TcId (Located (body TcId)), thing)
 
 tcStmts :: (Outputable (body Name)) => HsStmtContext Name
@@ -336,8 +310,8 @@ tcStmts ctxt stmt_chk stmts res_ty
 tcStmtsAndThen :: (Outputable (body Name)) => HsStmtContext Name
                -> TcStmtChecker body    -- NB: higher-rank type
                -> [LStmt Name (Located (body Name))]
-               -> TcSigmaType
-               -> (TcSigmaType -> TcM thing)
+               -> TcRhoType
+               -> (TcRhoType -> TcM thing)
                -> TcM ([LStmt TcId (Located (body TcId))], thing)
 
 -- Note the higher-rank type.  stmt_chk is applied at different
@@ -370,7 +344,7 @@ tcStmtsAndThen ctxt stmt_chk (L loc stmt : stmts) res_ty thing_inside
 
 tcGuardStmt :: TcExprStmtChecker
 tcGuardStmt _ (BodyStmt guard _ _ _) res_ty thing_inside
-  = do  { guard' <- tcPolyExpr guard boolTy
+  = do  { guard' <- tcMonoExpr guard boolTy
         ; thing  <- thing_inside res_ty
         ; return (BodyStmt guard' noSyntaxExpr noSyntaxExpr boolTy, thing) }
 
@@ -402,21 +376,21 @@ tcLcStmt :: TyCon       -- The list/Parray type constructor ([] or PArray)
          -> TcExprStmtChecker
 
 tcLcStmt _ _ (LastStmt body _) elt_ty thing_inside
-  = do { body' <- tcPolyExprNC body elt_ty
+  = do { body' <- tcMonoExprNC body elt_ty
        ; thing <- thing_inside (panic "tcLcStmt: thing_inside")
        ; return (LastStmt body' noSyntaxExpr, thing) }
 
 -- A generator, pat <- rhs
 tcLcStmt m_tc ctxt (BindStmt pat rhs _ _) elt_ty thing_inside
  = do   { pat_ty <- newFlexiTyVarTy liftedTypeKind
-        ; rhs'   <- tcPolyExpr rhs (mkTyConApp m_tc [pat_ty])
+        ; rhs'   <- tcMonoExpr rhs (mkTyConApp m_tc [pat_ty])
         ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat pat_ty $
                             thing_inside elt_ty
         ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
 
 -- A boolean guard
 tcLcStmt _ _ (BodyStmt rhs _ _ _) elt_ty thing_inside
-  = do  { rhs'  <- tcPolyExpr rhs boolTy
+  = do  { rhs'  <- tcMonoExpr rhs boolTy
         ; thing <- thing_inside elt_ty
         ; return (BodyStmt rhs' noSyntaxExpr noSyntaxExpr boolTy, thing) }
 
@@ -448,8 +422,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
             <- tcStmtsAndThen (TransStmtCtxt ctxt) (tcLcStmt m_tc) stmts unused_ty $ \_ -> do
                { by' <- case by of
                            Nothing -> return Nothing
-                           Just e  -> do { e_ty <- tcInferSigma e
-                                         ; return (Just e_ty) }
+                           Just e  -> do { e_ty <- tcInferSigma e; return (Just e_ty) }
                ; bndr_ids <- tcLookupLocalIds bndr_names
                ; return (bndr_ids, by') }
 
@@ -513,7 +486,7 @@ tcMcStmt _ (LastStmt body return_op) res_ty thing_inside
   = do  { a_ty       <- newFlexiTyVarTy liftedTypeKind
         ; return_op' <- tcSyntaxOp MCompOrigin return_op
                                    (a_ty `mkFunTy` res_ty)
-        ; body'      <- tcPolyExprNC body a_ty
+        ; body'      <- tcMonoExprNC body a_ty
         ; thing      <- thing_inside (panic "tcMcStmt: thing_inside")
         ; return (LastStmt body' return_op', thing) }
 
@@ -537,7 +510,7 @@ tcMcStmt ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
                       then return noSyntaxExpr
                       else tcSyntaxOp MCompOrigin fail_op (mkFunTy stringTy new_res_ty)
 
-        ; rhs' <- tcPolyExprNC rhs rhs_ty
+        ; rhs' <- tcMonoExprNC rhs rhs_ty
         ; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty $
                            thing_inside new_res_ty
 
@@ -555,7 +528,7 @@ tcMcStmt _ (BodyStmt rhs then_op guard_op _) res_ty thing_inside
           test_ty    <- newFlexiTyVarTy liftedTypeKind
         ; rhs_ty     <- newFlexiTyVarTy liftedTypeKind
         ; new_res_ty <- newFlexiTyVarTy liftedTypeKind
-        ; rhs'       <- tcPolyExpr rhs test_ty
+        ; rhs'       <- tcMonoExpr rhs test_ty
         ; guard_op'  <- tcSyntaxOp MCompOrigin guard_op
                                    (mkFunTy test_ty rhs_ty)
         ; then_op'   <- tcSyntaxOp MCompOrigin then_op
@@ -617,7 +590,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
             tcStmtsAndThen (TransStmtCtxt ctxt) tcMcStmt stmts using_arg_ty $ \res_ty' -> do
                 { by' <- case by of
                            Nothing -> return Nothing
-                           Just e  -> do { e' <- tcPolyExpr e by_e_ty; return (Just e') }
+                           Just e  -> do { e' <- tcMonoExpr e by_e_ty; return (Just e') }
 
                 -- Find the Ids (and hence types) of all old binders
                 ; bndr_ids <- tcLookupLocalIds bndr_names
@@ -759,7 +732,7 @@ tcMcStmt _ stmt _ _
 tcDoStmt :: TcExprStmtChecker
 
 tcDoStmt _ (LastStmt body _) res_ty thing_inside
-  = do { body' <- tcPolyExprNC body res_ty
+  = do { body' <- tcMonoExprNC body res_ty
        ; thing <- thing_inside (panic "tcDoStmt: thing_inside")
        ; return (LastStmt body' noSyntaxExpr, thing) }
 
@@ -785,7 +758,7 @@ tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
                       then return noSyntaxExpr
                       else tcSyntaxOp DoOrigin fail_op (mkFunTy stringTy new_res_ty)
 
-        ; rhs' <- tcPolyExprNC rhs rhs_ty
+        ; rhs' <- tcMonoExprNC rhs rhs_ty
         ; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty $
                            thing_inside new_res_ty
 
@@ -801,7 +774,7 @@ tcDoStmt _ (BodyStmt rhs then_op _ _) res_ty thing_inside
         ; then_op' <- tcSyntaxOp DoOrigin then_op
                            (mkFunTys [rhs_ty, new_res_ty] res_ty)
 
-        ; rhs' <- tcPolyExprNC rhs rhs_ty
+        ; rhs' <- tcMonoExprNC rhs rhs_ty
         ; thing <- thing_inside new_res_ty
         ; return (BodyStmt rhs' then_op' noSyntaxExpr rhs_ty, thing) }
 
@@ -855,7 +828,7 @@ When typechecking
         do { bar; ... } :: IO ()
 we want to typecheck 'bar' in the knowledge that it should be an IO thing,
 pushing info from the context into the RHS.  To do this, we check the
-rebindable syntax first, and push that information into (tcPolyExprNC rhs).
+rebindable syntax first, and push that information into (tcMonoExprNC rhs).
 Otherwise the error shows up when cheking the rebindable syntax, and
 the expected/inferred stuff is back to front (see Trac #3613).
 
index 5699697..8bcbe85 100644 (file)
@@ -18,7 +18,7 @@ module TcPat ( tcLetPat, TcSigFun, TcPragFun
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferSigma )
+import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferRho )
 
 import HsSyn
 import TcHsSyn
@@ -541,11 +541,6 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
         ; (expr',expr'_inferred) <- tcInferRho 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_wrap, pat_ty) <- tcInfer $ \ pat_ty ->
                 tcSubTypeDS GenSigCtxt expr'_inferred
                             (mkFunTy overall_pat_ty pat_ty)
@@ -911,7 +906,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
 
 ----------------------------
 -- | Convenient wrapper for calling a matchExpectedXXX function
-matchExpectedPatTy :: (TcRhoType -> TcM (HsWrapper, a))
+matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
                     -> TcSigmaType -> TcM (HsWrapper, a)
 -- See Note [Matching polytyped patterns]
 -- Returns a wrapper : pat_ty ~R inner_ty
@@ -955,7 +950,7 @@ matchExpectedConTy data_tc pat_ty
 
   | otherwise
   = do { (wrap, pat_rho) <- topInstantiate PatOrigin pat_ty
-       ; (coi, tys) <- matchExpectedTyConApp (Actual PatOrigin) data_tc pat_rho
+       ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho
        ; return (coToHsWrapper (mkTcSymCo coi) <.> wrap, tys) }
 
 {-
index fc8d535..b01d0a2 100644 (file)
@@ -1299,7 +1299,7 @@ check_main dflags tcg_env
         ; res_ty <- newFlexiTyVarTy liftedTypeKind
         ; main_expr
                 <- addErrCtxt mainCtxt    $
-                   tcPolyExpr (L loc (HsVar main_name)) (mkTyConApp ioTyCon [res_ty])
+                   tcMonoExpr (L loc (HsVar main_name)) (mkTyConApp ioTyCon [res_ty])
 
                 -- See Note [Root-main Id]
                 -- Construct the binding
@@ -1809,7 +1809,7 @@ tcRnExpr hsc_env rdr_expr
     -- Ignore the dictionary bindings
     _ <- simplifyInteractive (andWC stWC lie_top) ;
 
-    let { all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_tau) } ;
+    let { all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_ty) } ;
     ty <- zonkTcType all_expr_ty ;
 
     -- We normalise type families, so that the type of an expression is the
index 555e88b..3625db1 100644 (file)
@@ -18,7 +18,6 @@ import TcExpr
 import TcEnv
 import TcEvidence( TcEvBinds(..) )
 import Type
-import Inst   ( topInstantiate )
 import Id
 import Var              ( EvVar )
 import Name
@@ -32,8 +31,6 @@ import Data.List( partition )
 {-
 Note [Typechecking rules]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
-TODO (RAE): Update note.
-
 We *infer* the typ of the LHS, and use that type to *check* the type of
 the RHS.  That means that higher-rank rules work reasonably well. Here's
 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
@@ -75,10 +72,8 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
             <- tcExtendTyVarEnv tv_bndrs $
                tcExtendIdEnv    id_bndrs $
                do { -- See Note [Solve order for RULES]
-                    ((lhs', rule_ty), lhs_wanted) <- captureConstraints $
-                                                     tcInferRho lhs
-
-                  ; (rhs', rhs_wanted) <- captureConstraints (tcPolyExpr rhs rule_ty)
+                    ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
+                  ; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
                   ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
 
        ; (lhs_evs, other_lhs_wanted) <- simplifyRule (snd $ unLoc name)
@@ -335,3 +330,4 @@ simplifyRule name lhs_wanted rhs_wanted
 
        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
                 , lhs_wanted { wc_simple = non_q_cts }) }
+
index 2d81627..040bab9 100644 (file)
@@ -41,7 +41,6 @@ import FastString
 import THNames
 import TcUnify
 import TcEnv
-import Inst
 
 #ifdef GHCI
 import HscMain
@@ -186,7 +185,7 @@ tcBrackTy (TExpBr _)  = panic "tcUntypedBracket: Unexpected TExpBr"
 tcPendingSplice :: PendingRnSplice -> TcM PendingTcSplice
 tcPendingSplice (PendingRnSplice flavour splice_name expr)
   = do { res_ty <- tcMetaTy meta_ty_name
-       ; expr' <- tcPolyExpr expr res_ty
+       ; expr' <- tcMonoExpr expr res_ty
        ; return (PendingTcSplice splice_name expr') }
   where
      meta_ty_name = case flavour of
@@ -431,7 +430,7 @@ tcNestedSplice pop_stage (TcPending ps_var lie_var) splice_name expr res_ty
   = do { meta_exp_ty <- tcTExpTy res_ty
        ; expr' <- setStage pop_stage $
                   setConstraintVar lie_var $
-                  tcPolyExpr expr meta_exp_ty
+                  tcMonoExpr expr meta_exp_ty
        ; untypeq <- tcLookupId unTypeQName
        ; let expr'' = mkHsApp (nlHsTyApp untypeq [res_ty]) expr'
        ; ps <- readMutVar ps_var
@@ -449,7 +448,7 @@ tcTopSplice expr res_ty
          -- making sure it has type Q (T res_ty)
          meta_exp_ty <- tcTExpTy res_ty
        ; zonked_q_expr <- tcTopSpliceExpr True $
-                          tcPolyExpr expr meta_exp_ty
+                          tcMonoExpr expr meta_exp_ty
 
          -- Run the expression
        ; expr2 <- runMetaE zonked_q_expr
@@ -463,7 +462,7 @@ tcTopSplice expr res_ty
          -- These steps should never fail; this is a *typed* splice
        ; addErrCtxt (spliceResultDoc expr) $ do
        { (exp3, _fvs) <- rnLExpr expr2
-       ; exp4 <- tcPolyExpr exp3 res_ty
+       ; exp4 <- tcMonoExpr exp3 res_ty
        ; return (unLoc exp4) } }
 
 {-
@@ -541,8 +540,7 @@ runAnnotation target expr = do
               ; wrapper <- instCall AnnOrigin [expr_ty] [mkClassPred data_class [expr_ty]]
               ; let specialised_to_annotation_wrapper_expr
                       = L loc (HsWrap wrapper (HsVar to_annotation_wrapper_id))
-              ; return (L loc (HsApp specialised_to_annotation_wrapper_expr
-                                     expr')) }
+              ; return (L loc (HsApp specialised_to_annotation_wrapper_expr expr')) }
 
     -- Run the appropriately wrapped expression to get the value of
     -- the annotation and its dictionaries. The return value is of
index 9ca4aff..482ed30 100644 (file)
@@ -628,9 +628,20 @@ tcSubTypeDS_NC ctxt ty_actual ty_expected
 ---------------
 tc_sub_type :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
 tc_sub_type origin ctxt ty_actual ty_expected
-  | isTyVarTy ty_actual  -- See Note [Higher rank types]
-  = do { cow <- uType origin ty_actual ty_expected
-       ; return (coToHsWrapper cow) }
+  | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types]
+  = do { lookup_res <- lookupTcTyVar tv_actual
+       ; case lookup_res of
+           Filled ty_actual' -> tc_sub_type origin ctxt ty_actual' ty_expected
+
+             -- It's tempting to see if tv_actual can unify with a polytype
+             -- and, if so, call uType; otherwise, skolemise first. But this
+             -- is wrong, because skolemising will bump the TcLevel and the
+             -- unification will fail anyway.
+             -- It's also tempting to call uUnfilledVar directly, but calling
+             -- uType seems safer in the presence of possible refactoring
+             -- later.
+           Unfilled _        -> coToHsWrapper <$>
+                                uType origin ty_actual ty_expected }
 
   | otherwise  -- See Note [Deep skolemisation]
   = do { (sk_wrap, inner_wrap) <- tcSkolemise SkolemiseDeeply ctxt ty_expected $
@@ -642,49 +653,53 @@ tc_sub_type origin ctxt ty_actual ty_expected
 tc_sub_type_ds :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
 -- Just like tcSubType, but with the additional precondition that
 -- ty_expected is deeply skolemised
-tc_sub_type_ds origin ctxt ty_actual ty_expected
-  | Just tv_expected <- tcGetTyVar_maybe ty_expected
-  , isMetaTyVar tv_expected
-  = do { traceTc "RAE1" (ppr ty_actual $$ ppr ty_expected $$
-                         pprTcTyVarDetails (tcTyVarDetails tv_expected))
-       ; dflags <- getDynFlags
-       ; let details = tcTyVarDetails tv_expected
-             kind    = tyVarKind tv_expected
-       ; (in_wrap, in_rho) <- if canUnifyWithPolyType dflags details kind
-                              then traceTc "RAE3" empty >>
-                                   return (idHsWrapper, ty_actual)
-                              else traceTc "RAE2" empty >>
-                                   deeplyInstantiate origin ty_actual
+tc_sub_type_ds origin ctxt ty_actual ty_expected = go ty_actual ty_expected
+  where
+    go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
+                 | Just ty_e' <- tcView ty_e = go ty_a  ty_e'
+
+    go ty_a@(TyVarTy tv_a) ty_e
+      = do { lookup_res <- lookupTcTyVar tv_a
+           ; case lookup_res of
+               Filled ty_a' -> tc_sub_type_ds origin ctxt ty_a' ty_e
+               Unfilled _   -> coToHsWrapper <$> uType origin ty_a ty_e }
+
+    go ty_a ty_e@(TyVarTy tv_e)
+      = do { dflags <- getDynFlags
+           ; lookup_res <- lookupTcTyVar tv_e
+           ; case lookup_res of
+               Filled ty_e'     -> tc_sub_type origin ctxt ty_a ty_e'
+               Unfilled details
+                 |  canUnifyWithPolyType dflags details (tyVarKind tv_e)
+                 -> coToHsWrapper <$> uType origin ty_a ty_e
+
      -- We've avoided instantiating ty_actual just in case ty_expected is
      -- polymorphic. But we've now assiduously determined that it is *not*
      -- polymorphic. So instantiate away. This is needed for e.g. test
      -- typecheck/should_compile/T4284.
-
-         -- Even if it's not a TauTv, we want to go straight to
-         -- uType, so that a ReturnTv can unify with a polytype
-       ; traceTc "RAE4" (ppr in_wrap $$ ppr in_rho)
-       ; cow <- uType origin in_rho ty_expected
-       ; traceTc "RAE5" (ppr cow)
-       ; return (coToHsWrapper cow <.> in_wrap) }
-
-  | Just (act_arg, act_res) <- tcSplitFunTy_maybe ty_actual
-  , Just (exp_arg, exp_res) <- tcSplitFunTy_maybe ty_expected
-  = -- See Note [Co/contra-variance of subsumption checking]
-    do { res_wrap <- tc_sub_type_ds origin ctxt act_res exp_res
-       ; arg_wrap <- tc_sub_type    origin ctxt exp_arg act_arg
-       ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
-           -- arg_wrap :: exp_arg ~ act_arg
-           -- res_wrap :: act-res ~ exp_res
-
-  | (tvs, theta, _) <- tcSplitSigmaTy ty_actual
-  , not (null tvs && null theta)
-  = do { (in_wrap, in_rho) <- topInstantiate origin ty_actual
-       ; body_wrap <- tcSubTypeDS_NC ctxt in_rho ty_expected
-       ; return (body_wrap <.> in_wrap) }
-
-  | otherwise   -- Revert to unification
-  = do { cow <- uType origin ty_actual ty_expected
-       ; return (coToHsWrapper cow) }
+                 |  otherwise
+                 -> do { (wrap, rho_a) <- deeplyInstantiate origin ty_a
+                       ; cow <- uType origin rho_a ty_e
+                       ; return (coToHsWrapper cow <.> wrap) } }
+
+    go (FunTy act_arg act_res) (FunTy exp_arg exp_res)
+      = -- See Note [Co/contra-variance of subsumption checking]
+        do { res_wrap <- tc_sub_type_ds origin ctxt act_res exp_res
+           ; arg_wrap <- tc_sub_type    origin ctxt exp_arg act_arg
+           ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
+               -- arg_wrap :: exp_arg ~ act_arg
+               -- res_wrap :: act-res ~ exp_res
+
+    go ty_a ty_e
+      | let (tvs, theta, _) = tcSplitSigmaTy ty_a
+      , not (null tvs && null theta)
+      = do { (in_wrap, in_rho) <- topInstantiate origin ty_a
+           ; body_wrap <- tcSubTypeDS_NC ctxt in_rho ty_e
+           ; return (body_wrap <.> in_wrap) }
+
+      | otherwise   -- Revert to unification
+      = do { cow <- uType origin ty_a ty_e
+           ; return (coToHsWrapper cow) }
 
 -----------------
 tcWrapResult :: HsExpr TcId -> TcSigmaType -> TcRhoType -> TcM (HsExpr TcId)