Some bugfixing
authorRichard Eisenberg <eir@cis.upenn.edu>
Wed, 8 Jul 2015 02:05:59 +0000 (22:05 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Wed, 8 Jul 2015 02:05:59 +0000 (22:05 -0400)
compiler/typecheck/Inst.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcMatches.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRules.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcUnify.hs

index 6d66a8e..7c4db34 100644 (file)
@@ -242,8 +242,9 @@ top_instantiate inst_all orig ty
                                              mkFunTys leave_theta rho)
 
        ; wrap1 <- instCall orig (mkTyVarTys inst_tvs') inst_theta'
-       ; traceTc "Instantiating (inferred only)"
-                 (vcat [ text "origin" <+> pprCtOrigin orig
+       ; 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' ])
index 239c7b0..84af8f7 100644 (file)
@@ -93,14 +93,7 @@ tcPolyExprNC (L loc expr) res_ty
 
 ---------------
 tcInferSigma, tcInferSigmaNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcSigmaType)
--- Infer an *sigma*-type.  This is, in effect, a special case
--- for ids and partial applications, so that if
---     f :: Int -> forall b. (forall a. a -> a -> b) -> b
--- then we can infer
---     f 3 :: forall b. (forall a. a -> a -> b) -> b
--- And that in turn is useful
---  (a) for the function part of any application (see tcApp)
---  (b) for the special rule for '$'
+-- Infer a *sigma*-type.
 tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr)
 
 tcInferSigmaNC (L loc expr)
@@ -108,24 +101,17 @@ tcInferSigmaNC (L loc expr)
     do { (expr', sigma) <- tcInfer (tcExpr Up expr)
        ; return (L loc expr', sigma) }
 
-tcUnboundId :: OccName -> TcSigmaType -> 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
-      ; let can = CHoleCan { cc_ev = CtWanted ty ev loc, cc_occ = occ
-                           , cc_hole = ExprHole }
-      ; emitInsoluble can
-      ; tcWrapResult (HsVar ev) ty res_ty }
+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
+                    -- TODO (RAE): Fix origin stuff
+       ; (wrap, rho) <- topInstantiate AppOrigin sigma
+       ; return (L loc (mkHsWrap wrap expr'), rho) }
+
 
 {-
 ************************************************************************
@@ -1221,6 +1207,25 @@ srcSpanPrimLit dflags span
     = HsLit (HsStringPrim "" (unsafeMkByteString
                              (showSDocOneLine dflags (ppr span))))
 
+tcUnboundId :: OccName -> TcM (HsExpr TcId, TcSigmaType)
+-- 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
+ = do { ty <- newFlexiTyVarTy liftedTypeKind
+      ; name <- newSysName occ
+      ; let ev = mkLocalId name ty
+      ; loc <- getCtLocM HoleOrigin
+      ; let can = CHoleCan { cc_ev = CtWanted ty ev loc, cc_occ = occ
+                           , cc_hole = ExprHole }
+      ; emitInsoluble can
+      ; return (HsVar ev, ty) }
+
 {-
 Note [Adding the implicit parameter to 'assert']
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index c7df7a5..3071473 100644 (file)
@@ -175,18 +175,22 @@ 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) <-
-             -- we skolemise the result type
+    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 { matches' <- mapM (tcMatch ctxt pat_tys rhs_rho) matches
+             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
-                             , mg_origin  = origin }) }
-        ; return (wrap_group wrap group) }
+                             , 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
index 4c76ccc..288f93f 100644 (file)
@@ -39,6 +39,7 @@ import TidyPgm    ( globaliseAndTidyId )
 import TysWiredIn ( unitTy, mkListTy )
 import DynamicLoading ( loadPlugins )
 import Plugins ( tcPlugin )
+import Inst   ( topInstantiate )
 #endif
 
 import DynFlags
@@ -65,7 +66,6 @@ import TcForeign
 import TcInstDcls
 import TcIface
 import TcMType
-import Inst   ( topInstantiate )
 import MkIface
 import TcSimplify
 import TcTyClsDecls
index cadac7d..afaa8bc 100644 (file)
@@ -18,6 +18,7 @@ import TcExpr
 import TcEnv
 import TcEvidence( TcEvBinds(..) )
 import Type
+import Inst   ( topInstantiate )
 import Id
 import Var              ( EvVar )
 import Name
@@ -31,6 +32,8 @@ 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:
@@ -72,7 +75,14 @@ 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 (tcInferSigma lhs)
+                    ((lhs', rule_ty), lhs_wanted) <- captureConstraints $
+                      do { (lhs', lhs_sigma) <- tcInferSigma lhs
+                         ; (lhs_wrap, lhs_rho) <- topInstantiate AppOrigin lhs_sigma  -- TODO (RAE): Fix origin
+                                -- could theoretically do deeplyInstantiate,
+                                -- but the resulting wrapper would be too complex
+                                -- for a RULE LHS.
+                         ; return (mkLHsWrap lhs_wrap lhs', lhs_rho) }
+
                   ; (rhs', rhs_wanted) <- captureConstraints (tcPolyExpr rhs rule_ty)
                   ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
 
index ffa1620..309f371 100644 (file)
@@ -41,6 +41,7 @@ import FastString
 import THNames
 import TcUnify
 import TcEnv
+import Inst
 
 #ifdef GHCI
 import HscMain
@@ -73,7 +74,6 @@ import Var
 import Module
 import LoadIface
 import Class
-import Inst
 import TyCon
 import CoAxiom
 import PatSyn ( patSynName )
index 889fbd0..8254882 100644 (file)
@@ -11,7 +11,7 @@ Type subsumption and unification
 module TcUnify (
   -- Full-blown subsumption
   tcWrapResult, tcSkolemise, SkolemiseMode(..),
-  tcSubTypeHR, tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC,
+  tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC,
   checkConstraints,
 
   -- Various unifications
@@ -216,7 +216,6 @@ match_fun_tys ea herald orig_fun orig_args orig_ty = go orig_args orig_ty
       | Just (Just hs_ty_arg) <- fmap isLHsTypeExpr_maybe arg
       = do { let origin = case ea of Expected    -> panic "match_fun_tys"
                                      Actual orig -> orig
-           ; traceTc "RAE1" (ppr arg $$ ppr args $$ ppr ty)
            ; (wrap1, upsilon_ty) <- topInstantiateInferred origin ty
                -- wrap1 :: ty "->" upsilon_ty
            ; case tcSplitForAllTy_maybe upsilon_ty of
@@ -225,7 +224,6 @@ match_fun_tys ea herald orig_fun orig_args orig_ty = go orig_args orig_ty
                  do { let kind = tyVarKind tv
                     ; ty_arg <- tcCheckLHsType hs_ty_arg kind
                     ; let insted_ty = substTyWith [tv] [ty_arg] inner_ty
-                    ; traceTc "RAE3" (ppr upsilon_ty $$ ppr tv $$ ppr inner_ty $$ ppr insted_ty $$ ppr ty_arg)
                     ; (inner_wrap, arg_tys, res_ty) <- go args insted_ty
                         -- inner_wrap :: insted_ty "->" arg_tys -> res_ty
                     ; let inst_wrap = mkWpTyApps [ty_arg]
@@ -236,8 +234,7 @@ match_fun_tys ea herald orig_fun orig_args orig_ty = go orig_args orig_ty
 
     go args ty
       | not (null tvs && null theta)
-      = do { traceTc "RAE2" (ppr args $$ ppr ty)
-           ; (wrap, (arg_tys, res_ty)) <- exposeRhoType ea ty $ \rho ->
+      = do { (wrap, (arg_tys, res_ty)) <- exposeRhoType ea ty $ \rho ->
              do { (inner_wrap, arg_tys, res_ty) <- go args rho
                 ; return (inner_wrap, (arg_tys, res_ty)) }
            ; return (wrap, arg_tys, res_ty) }
@@ -601,10 +598,6 @@ So it's important that we unify beta := forall a. a->a, rather than
 skolemising the type.
 -}
 
--- | Use this wrapper for 'tcSubType' in higher-rank situations.
-tcSubTypeHR :: TcSigmaType -> TcSigmaType -> TcM HsWrapper
-tcSubTypeHR = tcSubType GenSigCtxt
-
 tcSubType :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
 -- Checks that actual <= expected
 -- Returns HsWrapper :: actual ~ expected
@@ -675,21 +668,26 @@ tc_sub_type_ds :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM Hs
 tc_sub_type_ds origin ctxt ty_actual ty_expected
   | Just tv_expected <- tcGetTyVar_maybe ty_expected
   , isMetaTyVar tv_expected
-  = do { dflags <- getDynFlags
-       ; (in_wrap, in_rho) <- case metaTyVarInfo tv_expected of
-                                TauTv _
-                                  | not (xopt Opt_ImpredicativeTypes dflags)
-                                  -> deeplyInstantiate origin ty_actual
+  = 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
      -- 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.
 
-                                _ -> return (idHsWrapper, ty_actual)
-
          -- 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