Checkpoint in bugfixing
authorRichard Eisenberg <eir@cis.upenn.edu>
Wed, 1 Jul 2015 21:14:37 +0000 (17:14 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Wed, 1 Jul 2015 21:14:37 +0000 (17:14 -0400)
12 files changed:
compiler/deSugar/DsExpr.hs
compiler/hsSyn/HsExpr.hs
compiler/hsSyn/HsUtils.hs
compiler/typecheck/Inst.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs-boot [new file with mode: 0644]
compiler/typecheck/TcMatches.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/typecheck/should_compile/Vta1.hs

index abc2eea..e202eb7 100644 (file)
@@ -215,7 +215,9 @@ dsExpr (HsLamCase arg matches)
        ; return $ Lam arg_var $ bindNonRec discrim_var (Var arg_var) matching_code }
 
 dsExpr (HsApp fun arg)
-  = mkCoreAppDs <$> dsLExpr fun <*>  dsLExpr arg
+    -- ignore type arguments here; they're in the wrappers instead at this point
+  | isLHsTypeExpr arg = dsLExpr fun
+  | otherwise         = mkCoreAppDs <$> dsLExpr fun <*>  dsLExpr arg
 
 
 {-
@@ -681,6 +683,7 @@ dsExpr (EAsPat        {})  = panic "dsExpr:EAsPat"
 dsExpr (EViewPat      {})  = panic "dsExpr:EViewPat"
 dsExpr (ELazyPat      {})  = panic "dsExpr:ELazyPat"
 dsExpr (HsType        {})  = panic "dsExpr:HsType" -- removed by typechecker
+dsExpr (HsTypeOut     {})  = panic "dsExpr:HsTypeOut" -- handled in HsApp case
 dsExpr (HsDo          {})  = panic "dsExpr:HsDo"
 
 
index 9b6b6c6..5fe90f6 100644 (file)
@@ -496,6 +496,7 @@ data HsExpr id
 
   -- For details on above see note [Api annotations] in ApiAnnotation
   | HsType      (LHsType id) -- Explicit type argument; e.g  f @Int x y
+  | HsTypeOut   (LHsType Name)  -- just for pretty-printing
 
   ---------------------------------------
   -- Finally, HsWrap appears only in typechecker output
@@ -726,6 +727,7 @@ ppr_expr (HsSCC _ (_,lbl) expr)
 
 ppr_expr (HsWrap co_fn e) = pprHsWrapper (pprExpr e) co_fn
 ppr_expr (HsType ty)      = char '@' <> pprParendHsType (unLoc ty)
+ppr_expr (HsTypeOut ty)   = char '@' <> pprParendHsType (unLoc ty)
 
 ppr_expr (HsSpliceE s)         = pprSplice s
 ppr_expr (HsBracket b)         = pprHsBracket b
@@ -820,6 +822,8 @@ hsExprNeedsParens (HsRnBracketOut {}) = False
 hsExprNeedsParens (HsTcBracketOut {}) = False
 hsExprNeedsParens (HsDo sc _ _)
        | isListCompExpr sc            = False
+hsExprNeedsParens (HsType {})         = False
+hsExprNeedsParens (HsTypeOut {})      = False
 hsExprNeedsParens _ = True
 
 
index 26fc8a6..09ff208 100644 (file)
@@ -25,7 +25,7 @@ module HsUtils(
   mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo,
   coToHsWrapper, coToHsWrapperR, mkHsDictLet, mkHsLams,
   mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo,
-  mkLHsPar, mkHsCmdCast,
+  mkLHsPar, mkHsCmdCast, isLHsTypeExpr_maybe, isLHsTypeExpr,
   WrappableThing(..),
 
   nlHsTyApp, nlHsTyApps, nlHsVar, nlHsLit, nlHsApp, nlHsApps, nlHsIntLit, nlHsVarApps,
@@ -407,6 +407,20 @@ 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
+isLHsTypeExpr_maybe :: LHsExpr name -> Maybe (LHsType 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.
index f6dd1ff..bc98be8 100644 (file)
@@ -10,7 +10,7 @@ The @Inst@ type: dictionaries or method instances
 
 module Inst (
        skolemise, SkolemiseMode(..),
-       topInstantiate,
+       topInstantiate, topInstantiateInferred, deeplyInstantiate,
        instCall, instDFunType, instStupidTheta,
        newWanted, newWanteds,
        emitWanted, emitWanteds,
@@ -216,24 +216,84 @@ topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 -- if    topInstantiate ty = (wrap, rho)
 -- and   e :: ty
 -- then  wrap e :: rho
+topInstantiate = top_instantiate True
 
-topInstantiate orig ty
+-- | Instantiate all outer *inferred* type variables
+-- 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 tvs && null theta)
-  = do { (subst, tvs') <- tcInstTyVars tvs
-       ; let theta' = substTheta subst theta
-       ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
-       ; traceTc "Instantiating" (vcat [ text "origin" <+> pprCtOrigin orig
-                                       , text "type" <+> ppr ty
-                                       , text "with" <+> ppr tvs'
-                                       , text "theta:" <+>  ppr theta' ])
+  = do { let (inst_tvs, leave_tvs) = span should_inst tvs
+             inst_theta
+               | null leave_tvs = theta
+               | otherwise      = []
+       ; (subst, inst_tvs') <- tcInstTyVars inst_tvs
+       ; let inst_theta' = substTheta subst inst_theta
+             sigma'      = substTy    subst (mkForAllTys leave_tvs rho)
+
+       ; wrap1 <- instCall orig (mkTyVarTys inst_tvs') inst_theta'
+       ; traceTc "Instantiating (inferred only)"
+                 (vcat [ text "origin" <+> pprCtOrigin orig
+                       , text "type" <+> ppr ty
+                       , text "with" <+> ppr inst_tvs'
+                       , text "theta:" <+>  ppr inst_theta' ])
+
+       ; (wrap2, rho2) <-
+           if null leave_tvs
+
          -- account for types like forall a. Num a => forall b. Ord b => ...
-       ; (wrap2, rho2) <- topInstantiate orig (substTy subst rho)
+           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
     (tvs, theta, rho) = tcSplitSigmaTy ty
 
+    should_inst
+      | inst_all  = const True
+      | otherwise = isInferredTyVar
+
+deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
+--   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
+-- In general if
+-- if    deeplyInstantiate ty = (wrap, rho)
+-- and   e :: ty
+-- then  wrap e :: rho
+
+deeplyInstantiate orig ty
+  | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
+  = do { (subst, tvs') <- tcInstTyVars tvs
+       ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
+       ; let theta' = substTheta subst theta
+       ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
+       ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig
+                                                , text "type" <+> ppr ty
+                                                , text "with" <+> ppr tvs'
+                                                , text "args:" <+> ppr ids1
+                                                , text "theta:" <+>  ppr theta' ])
+       ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
+       ; return (mkWpLams ids1
+                    <.> wrap2
+                    <.> wrap1
+                    <.> mkWpEvVarApps ids1,
+                 mkFunTys arg_tys rho2) }
+
+  | otherwise = return (idHsWrapper, ty)
+
+
 {-
 ************************************************************************
 *                                                                      *
index 9edd5de..239c7b0 100644 (file)
@@ -231,12 +231,8 @@ tcExpr Up (ExprWithTySig expr sig_ty wcs) res_ty
       ; tcWrapResult inner_expr sig_tc_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 ])
 
 {-
 ************************************************************************
@@ -927,44 +923,44 @@ tcApp :: Maybe SDoc  -- like "The function `f' is applied to"
            -- But OpApp is slightly different, so that's why the caller
            -- must assemble
 
-tcApp m_herald orig (L _ (HsPar e)) args res_ty
-  = tcApp m_herald orig e args res_ty
-
-tcApp m_herald orig (L _ (HsApp e1 e2)) args res_ty
-  = tcApp m_herald orig e1 (e2:args) res_ty   -- Accumulate the arguments
-
-tcApp _ _ (L loc (HsVar 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
-
-tcApp m_herald orig fun args res_ty
-  = do  {   -- Type-check the function
-        ; (fun1, fun_sigma) <- tcInferFun fun
-
-            -- Extract its argument types
-        ; (wrap_fun, expected_arg_tys, actual_res_ty)
-              <- matchExpectedFunTys (Actual orig)
-                   (m_herald `orElse` mk_app_msg fun)
-                   (length args) fun_sigma
-
-        -- 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 actual_res_ty res_ty
-
-        -- Typecheck the arguments
-        ; args1 <- tcArgs fun args expected_arg_tys
-
-        -- Assemble the result
-        ; return (wrap_res, mkLHsWrap wrap_fun fun1, args1) }
+tcApp m_herald orig 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 fun)) args
+      | fun `hasKey` tagToEnumKey
+      , count (not . isLHsTypeExpr) args == 1
+      = tcTagToEnum loc fun args res_ty
+
+      | fun `hasKey` seqIdKey
+      , count (not . isLHsTypeExpr) args == 2
+      = tcSeq loc fun args res_ty
+
+    go fun args
+      = do {   -- Type-check the function
+           ; (fun1, fun_sigma) <- tcInferFun fun
+
+               -- Extract its argument types
+           ; (wrap_fun, expected_arg_tys, actual_res_ty)
+                 <- matchExpectedFunTys_Args orig
+                      (m_herald `orElse` mk_app_msg fun)
+                      fun args fun_sigma
+
+           -- 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 actual_res_ty res_ty
+
+           -- Typecheck the arguments
+           ; args1 <- tcArgs fun args expected_arg_tys
+
+           -- Assemble the result
+           ; 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)
@@ -996,8 +992,20 @@ tcArgs :: LHsExpr Name                          -- The function (for error messa
        -> [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..])
+tcArgs fun orig_args orig_arg_tys = go 1 orig_args orig_arg_tys
+  where
+    go _ [] [] = return []
+    go n (arg:args) all_arg_tys
+      | Just hs_ty <- isLHsTypeExpr_maybe arg
+      = do { args' <- go (n+1) args all_arg_tys
+           ; return (L (getLoc arg) (HsTypeOut hs_ty) : args') }
+
+    go n (arg:args) (arg_ty:arg_tys)
+      = do { arg'  <- tcArg fun (arg, arg_ty, n)
+           ; args' <- go (n+1) args arg_tys
+           ; return (arg':args') }
+
+    go _ _ _ = pprPanic "tcArgs" (ppr fun $$ ppr orig_args $$ ppr orig_arg_tys)
 
 ----------------
 tcArg :: LHsExpr Name                           -- The function (for error messages)
@@ -1139,7 +1147,9 @@ tcInferIdWithOrig orig id_name
          else tc_infer_assert dflags orig }
 
   | otherwise
-  = tc_infer_id orig id_name
+  = do { (expr, ty) <- tc_infer_id orig id_name
+       ; traceTc "tcInferIdWithOrig" (ppr id_name <+> dcolon <+> ppr ty)
+       ; return (expr, ty) }
 
 tc_infer_assert :: DynFlags -> CtOrigin -> TcM (HsExpr TcId, TcSigmaType)
 -- Deal with an occurrence of 'assert'
@@ -1261,24 +1271,64 @@ the users that complain.
 
 -}
 
-tcSeq :: SrcSpan -> Name -> LHsExpr Name -> LHsExpr Name
+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
-tcSeq loc fun_name arg1 arg2 res_ty
+tcSeq loc fun_name args res_ty
   = do  { fun <- tcLookupId fun_name
-        ; (arg1', arg1_ty) <- tcInfer (tcPolyExpr arg1)
+        ; (arg1_ty, args1) <- case args of
+            (ty_arg_expr1 : args1)
+              | Just hs_ty_arg1 <- isLHsTypeExpr_maybe ty_arg_expr1
+              -> do { ty_arg1 <- tcHsLiftedType hs_ty_arg1
+                    ; return (ty_arg1, args1) }
+
+            _ -> do { arg_ty1 <- newReturnTyVarTy 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 { ty_arg2 <- tcHsOpenType hs_ty_arg2
+                    ; _ <- unifyType ty_arg2 res_ty
+                    ; return (term_arg1, term_arg2) }
+            [term_arg1, term_arg2] -> return (term_arg1, term_arg2)
+            _ -> too_many_args
+
+        ; arg1' <- tcPolyExpr arg1 arg1_ty
+        ; res_ty <- zonkTcType res_ty   -- just in case we learned something
+                                        -- interesting about it
         ; arg2' <- tcPolyExpr arg2 res_ty
         ; let fun'    = L loc (HsWrap ty_args (HsVar fun))
               ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty
         ; 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
+
+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
+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 <- tcHsLiftedType hs_ty_arg
+                   ; _ <- unifyType 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
@@ -1313,6 +1363,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))
+
 {-
 ************************************************************************
 *                                                                      *
index ff79391..1bdfe4f 100644 (file)
@@ -768,6 +768,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)
 
 -------------------------------------------------------------------------
diff --git a/compiler/typecheck/TcHsType.hs-boot b/compiler/typecheck/TcHsType.hs-boot
new file mode 100644 (file)
index 0000000..e3df0ba
--- /dev/null
@@ -0,0 +1,8 @@
+module TcHsType where
+
+import HsTypes   ( LHsType )
+import Name      ( Name )
+import TcType    ( TcKind, Type )
+import TcRnMonad ( TcM )
+
+tcCheckLHsType :: LHsType Name -> TcKind -> TcM Type
index cfee67c..c7df7a5 100644 (file)
@@ -174,19 +174,12 @@ data TcMatchCtxt body   -- c.f. TcStmtCtxt, also in this module
                  -> TcM (Located (body TcId)) }
 
 tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = matches, mg_origin = origin })
-  | [match] <- matches
-  = do { match' <- tcMatch ctxt pat_tys rhs_ty match
-       ; return (MG { mg_alts    = [match']
-                    , mg_arg_tys = pat_tys
-                    , mg_res_ty  = rhs_ty
-                    , mg_origin  = origin }) }
-
-  | otherwise
   = ASSERT( not (null matches) )        -- Ensure that rhs_ty is filled in
     do  { (wrap, group) <-
-             -- if there are several matches, we skolemise the result type,
+             -- we skolemise the result type
              -- 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
                 ; return (MG { mg_alts    = matches'
index 57ed460..7f85568 100644 (file)
@@ -1704,7 +1704,7 @@ checkValidClass cls
                 -- Here, MonadState has a fundep m->b, so newBoard is fine
 
         ; unless constrained_class_methods $
-          mapM_ check_constraint (tail (theta1 ++ theta2)) 
+          mapM_ check_constraint (tail (theta1 ++ theta2))
 
         ; case dm of
             GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
@@ -1949,11 +1949,12 @@ mkRecSelBind (tycon, sel_name)
     is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)
     (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
-           | otherwise  = mkForAllTys (varSetElemsKvsFirst $
-                                       data_tvs `extendVarSetList` field_tvs) $
+           | otherwise  = mkForAllTys (varSetElemsKvsFirst data_tvs) $
                           mkPhiTy (dataConStupidTheta con1) $   -- Urgh!
-                          mkPhiTy field_theta               $   -- Urgh!
-                          mkFunTy data_ty field_tau
+                          mkFunTy data_ty                   $
+                          mkForAllTys field_tvs             $
+                          mkPhiTy field_theta               $
+                          field_tau
 
     -- Make the binding: sel (C2 { fld = x }) = x
     --                   sel (C7 { fld = x }) = x
@@ -2005,14 +2006,14 @@ tyConFields tc
 {-
 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
+We take care to build the type of a polymorphic selector in the right
+order, so that visible type application works.
 
-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!
+  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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2164,7 +2165,7 @@ classFunDepsErr cls
 
 badMethPred :: Id -> TcPredType -> SDoc
 badMethPred sel_id pred
-  = vcat [ hang (ptext (sLit "Constraint") <+> quotes (ppr pred) 
+  = vcat [ hang (ptext (sLit "Constraint") <+> quotes (ppr pred)
                  <+> ptext (sLit "in the type of") <+> quotes (ppr sel_id))
               2 (ptext (sLit "constrains only the class type variables"))
          , ptext (sLit "Use ConstrainedClassMethods to allow it") ]
index 37bf470..0c036b9 100644 (file)
@@ -38,6 +38,7 @@ module TcType (
   isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
   isFlexi, isIndirect, isRuntimeUnkSkol,
   isTypeVar, isKindVar,
+  isInferredTyVar, isSpecifiedTyVar,
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
   isTouchableMetaTyVar, isTouchableOrFmv,
   isFloatedTouchableMetaTyVar,
@@ -51,6 +52,7 @@ module TcType (
   -- Splitters
   -- These are important because they do not look through newtypes
   tcView,
+  tcSplitForAllTy_maybe,
   tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
@@ -82,7 +84,7 @@ module TcType (
 
   ---------------------------------
   -- Predicate types
-  mkMinimalBySCs, transSuperClasses, transSuperClassesPred, 
+  mkMinimalBySCs, transSuperClasses, transSuperClassesPred,
   immSuperClasses,
   isImprovementPred,
 
@@ -818,6 +820,14 @@ isRuntimeUnkSkol x
   | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True
   | otherwise                                   = False
 
+-- | Is this TyVar inferred by GHC? (Used with visible type application)
+isInferredTyVar :: TyVar -> Bool
+isInferredTyVar = isSystemName . tyVarName
+
+-- | Is this TyVar specified by the user? (Used with visible type application)
+isSpecifiedTyVar :: TyVar -> Bool
+isSpecifiedTyVar = isInternalName . tyVarName
+
 {-
 ************************************************************************
 *                                                                      *
@@ -908,6 +918,11 @@ However, they are non-monadic and do not follow through mutable type
 variables.  It's up to you to make sure this doesn't matter.
 -}
 
+tcSplitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
+tcSplitForAllTy_maybe ty | Just ty' <- tcView ty = tcSplitForAllTy_maybe ty'
+tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
+tcSplitForAllTy_maybe _                = Nothing
+
 tcSplitForAllTys :: Type -> ([TyVar], Type)
 tcSplitForAllTys ty = split ty ty []
    where
@@ -1271,8 +1286,8 @@ occurCheckExpand dflags tv ty
     -- it and try again.
     go ty@(TyConApp tc tys)
       = case do { tys <- mapM go tys; return (mkTyConApp tc tys) } of
-          OC_OK ty 
-              | impredicative || isTauTyCon tc 
+          OC_OK ty
+              | impredicative || isTauTyCon tc
               -> return ty  -- First try to eliminate the tyvar from the args
               | otherwise
               -> OC_Forall  -- A type synonym with a forall on the RHS
@@ -1322,7 +1337,7 @@ Note [Kind polymorphic type classes]
     class C f where...   -- C :: forall k. k -> Constraint
     g :: forall (f::*). C f => f -> f
 
-Here the (C f) in the signature is really (C * f), and we 
+Here the (C f) in the signature is really (C * f), and we
 don't want to complain that the * isn't a type variable!
 -}
 
@@ -1343,7 +1358,7 @@ checkValidClsArgs flexible_contexts kts
   | otherwise         = all hasTyVarHead tys
   where
     (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
-   
+
 hasTyVarHead :: Type -> Bool
 -- Returns true of (a t1 .. tn), where 'a' is a type variable
 hasTyVarHead ty                 -- Haskell 98 allows predicates of form
@@ -1401,7 +1416,7 @@ immSuperClasses cls tys
 
 isImprovementPred :: PredType -> Bool
 -- Either it's an equality, or has some functional dependency
-isImprovementPred ty 
+isImprovementPred ty
   = case classifyPredType ty of
       EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
       EqPred ReprEq _ _  -> False
@@ -1891,4 +1906,3 @@ size_type (ForAllTy _ ty)   = size_type ty
 
 sizeTypes :: [Type] -> TypeSize
 sizeTypes tys = sum (map sizeType tys)
-
index 3b153a6..e74dab0 100644 (file)
@@ -26,7 +26,7 @@ module TcUnify (
   matchExpectedPArrTy,
   matchExpectedTyConApp,
   matchExpectedAppTys,
-  matchExpectedFunTys,
+  matchExpectedFunTys, matchExpectedFunTys_Args,
   matchExpectedFunKind,
   newOverloadedLit,
   wrapFunResCoercion
@@ -35,6 +35,8 @@ module TcUnify (
 
 #include "HsVersions.h"
 
+import {-# SOURCE #-} TcHsType ( tcCheckLHsType )
+
 import HsSyn
 import TypeRep
 import TcMType
@@ -54,7 +56,7 @@ import VarSet
 import ErrUtils
 import DynFlags
 import BasicTypes
-import Maybes ( isJust )
+import Maybes ( isJust, expectJust )
 import Util
 import Outputable
 import FastString
@@ -162,11 +164,35 @@ ignoring the quantification. In App, we want to instantiate.
 
 -}
 
+-- | Wrapper for 'match_fun_tys', to be used unless you have visible
+-- type arguments to pass in.
 matchExpectedFunTys :: ExpOrAct
-                    -> SDoc     -- See Note [Herald for matchExpectedFunTys]
+                    -> SDoc   -- See Note [Herald for matchExpectedFunTys]
                     -> Arity
                     -> TcSigmaType
                     -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+matchExpectedFunTys ea herald n orig_ty
+  = match_fun_tys ea herald (panic "matchExpectedFunTys")
+                  (nOfThem n Nothing) orig_ty
+
+-- | Wrapper for 'match_fun_tys', to be used when you do have visible
+-- type arugments to pass in.
+matchExpectedFunTys_Args :: CtOrigin
+                         -> SDoc  -- See Note [Herald for matchExpectedFunTys]
+                         -> LHsExpr Name  -- the function (for errors)
+                         -> [LHsExpr Name]
+                         -> TcSigmaType
+                         -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+matchExpectedFunTys_Args orig herald orig_fun args orig_ty
+  = match_fun_tys (Actual orig) herald orig_fun (map Just args) orig_ty
+
+match_fun_tys
+  :: ExpOrAct
+  -> SDoc          -- See Note [Herald for matchExpectedFunTys]
+  -> LHsExpr Name  -- the function expression; only used when there are type args
+  -> [Maybe (LHsExpr Name)]
+  -> TcSigmaType
+  -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
 
 -- If    matchExpectFunTys n ty = (wrap, [t1,..,tn], ty_r)
 -- then  wrap : ty "->" (t1 -> ... -> tn -> ty_r)
@@ -178,42 +204,61 @@ matchExpectedFunTys :: ExpOrAct
 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
 -- hide the forall inside a meta-variable
 
-matchExpectedFunTys ea herald arity orig_ty = go arity orig_ty
+match_fun_tys ea herald orig_fun orig_args orig_ty = go orig_args orig_ty
   where
     -- If     go n ty = (co, [t1,..,tn], ty_r)
     -- then   Actual:   wrap : ty "->" (t1 -> .. -> tn -> ty_r)
     --        Expected: wrap : (t1 -> .. -> tn -> ty_r) "->" ty
 
-    go n_req ty
-      | n_req == 0 = return (idHsWrapper, [], ty)
-
-    go n_req ty
+    go [] ty = return (idHsWrapper, [], ty)
+
+    go (arg:args) ty
+      | Just (Just hs_ty_arg) <- fmap isLHsTypeExpr_maybe arg
+      = do { let origin = case ea of Expected    -> panic "match_fun_tys"
+                                     Actual orig -> orig
+           ; (wrap1, upsilon_ty) <- topInstantiateInferred origin ty
+               -- wrap1 :: ty "->" upsilon_ty
+           ; case tcSplitForAllTy_maybe upsilon_ty of
+               Just (tv, inner_ty) ->
+                 ASSERT( isSpecifiedTyVar tv )
+                 do { let kind = tyVarKind tv
+                    ; ty_arg <- tcCheckLHsType hs_ty_arg kind
+                    ; let insted_ty = substTyWith [tv] [ty_arg] inner_ty
+                    ; (inner_wrap, arg_tys, res_ty) <- go args insted_ty
+                        -- inner_wrap :: insted_ty "->" arg_tys -> res_ty
+                    ; let inst_wrap = mkWpTyApps [ty_arg]
+                        -- inst_wrap :: upsilon_ty "->" insted_ty
+                    ; return ( inner_wrap <.> inst_wrap <.> wrap1
+                             , arg_tys, res_ty ) }
+               Nothing -> ty_app_err upsilon_ty hs_ty_arg }
+
+    go args ty
       | not (null tvs && null theta)
       = do { (wrap, (arg_tys, res_ty)) <- exposeRhoType ea ty $ \rho ->
-             do { (inner_wrap, arg_tys, res_ty) <- go n_req rho
+             do { (inner_wrap, arg_tys, res_ty) <- go args rho
                 ; return (inner_wrap, (arg_tys, res_ty)) }
            ; return (wrap, arg_tys, res_ty) }
       where
         (tvs, theta, _) = tcSplitSigmaTy ty
 
-    go n_req ty
-      | Just ty' <- tcView ty = go n_req ty'
+    go args ty
+      | Just ty' <- tcView ty = go args ty'
 
-    go n_req (FunTy arg_ty res_ty)
+    go (_arg:args) (FunTy arg_ty res_ty)
       | not (isPredTy arg_ty)
-      = do { (wrap_res, tys, ty_r) <- go (n_req-1) res_ty
+      = do { (wrap_res, tys, ty_r) <- go args res_ty
            ; let rhs_ty = case ea of
                    Expected -> res_ty
                    Actual _ -> mkFunTys tys ty_r
            ; return ( mkWpFun idHsWrapper wrap_res arg_ty rhs_ty
                     , arg_ty:tys, ty_r ) }
 
-    go n_req ty@(TyVarTy tv)
+    go 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 args ty'
+               Flexi        -> defer args ty (isReturnTyVar tv) }
 
        -- In all other cases we bale out into ordinary unification
        -- However unlike the meta-tyvar case, we are sure that the
@@ -230,15 +275,16 @@ matchExpectedFunTys ea herald arity orig_ty = go 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 args ty = addErrCtxtM mk_ctxt $
+                 defer args 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 <- mapM new_ty_var_ty (nOfThem n_req openTypeKind)
+    defer args fun_ty is_return
+      = do { check_for_type_args args  -- fails if there are any type args
+           ; arg_tys <- mapM new_ty_var_ty (map (const openTypeKind) args)
                         -- See Note [Foralls to left of arrow]
            ; res_ty  <- new_ty_var_ty openTypeKind
            ; let unif_fun_ty = mkFunTys arg_tys res_ty
@@ -249,6 +295,16 @@ matchExpectedFunTys ea herald arity orig_ty = go arity orig_ty
                       | otherwise = newFlexiTyVarTy
 
     ------------
+    check_for_type_args args
+      = when (any (maybe False isLHsTypeExpr) args) $
+        failWith $
+        vcat [ text "Cannot apply" <+> quotes (ppr orig_fun) <+>
+                 text "to arguments"
+             , nest 4 (sep (map (pprParendExpr .
+                                 expectJust "check_for_type_args") orig_args))
+             , hang (text "I do not know enough about the function's type")
+                  2 (ppr orig_ty) ]
+
     mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
     mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_ty
                      ; let (args, _) = tcSplitFunTys ty
@@ -256,8 +312,9 @@ matchExpectedFunTys ea herald arity orig_ty = go arity orig_ty
                            (env'', orig_ty') = tidyOpenType env' orig_ty
                      ; return (env'', mk_msg orig_ty' ty n_actual) }
 
+    arity = length orig_args
     mk_msg orig_ty ty n_args
-      = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
+      = herald <+> speakNOf arity (text "argument") <> comma $$
         if n_args == arity
           then ptext (sLit "its type is") <+> quotes (pprType orig_ty) <>
                comma $$
@@ -266,6 +323,11 @@ matchExpectedFunTys ea herald arity orig_ty = go arity orig_ty
                     if n_args == 0 then ptext (sLit "has none")
                     else ptext (sLit "has only") <+> speakN n_args]
 
+    ty_app_err ty arg
+      = failWith $
+        text "Cannot not apply expression of type" <+> quotes (ppr ty) $$
+        text "to a visible type argument" <+> quotes (ppr arg)
+
 {-
 Note [Foralls to left of arrow]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -608,6 +670,25 @@ tc_sub_type_ds :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM Hs
 -- 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 { dflags <- getDynFlags
+       ; (in_wrap, in_rho) <- case metaTyVarInfo tv_expected of
+                                TauTv _
+                                  | not (xopt Opt_ImpredicativeTypes dflags)
+                                  -> 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
+       ; cow <- uType origin in_rho ty_expected
+       ; 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]
@@ -617,14 +698,10 @@ tc_sub_type_ds origin ctxt ty_actual ty_expected
            -- arg_wrap :: exp_arg ~ act_arg
            -- res_wrap :: act-res ~ exp_res
 
-  | (tvs, theta, in_rho) <- tcSplitSigmaTy ty_actual
+  | (tvs, theta, _) <- tcSplitSigmaTy ty_actual
   , not (null tvs && null theta)
-  = do { (subst, tvs') <- tcInstTyVars tvs
-       ; let tys'    = mkTyVarTys tvs'
-             theta'  = substTheta subst theta
-             in_rho' = substTy subst in_rho
-       ; in_wrap   <- instCall origin tys' theta'
-       ; body_wrap <- tcSubTypeDS_NC ctxt in_rho' ty_expected
+  = 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
index 7c41b21..6f7fc04 100644 (file)
@@ -1,4 +1,5 @@
-{-# LANGUAGE TypeApplications, ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications, ScopedTypeVariables, PolyKinds,
+             TypeFamilies, RankNTypes #-}
 
 -- tests about visible type application
 
@@ -7,8 +8,8 @@ module Vta1 where
 quad :: a -> b -> c -> d -> (a, b, c, d)
 quad = (,,,)
 
-silly :: (a, Bool, Char, b)
-silly = quad @_ @Bool @Char @_ 5 True 'a' "Hello"
+-- silly :: (a, Bool, Char, b)
+-- silly = quad @_ @Bool @Char @_ 5 True 'a' "Hello"
 
 pairup_nosig x y = (x, y)
 
@@ -48,7 +49,6 @@ mapSame fun (x:xs) = fun @b x : (mapSame @b fun xs)
 pair :: forall a. a-> (forall b. b -> (a, b))
 pair x y = (x, y)
 
-a = pair @Int @Bool 3 True
 b = pair @Int 3 @Bool True
 c = mapSame id [1,2,3]
 d = pair 3 @Bool True
@@ -87,10 +87,10 @@ newtype N = MkN { unMkN :: forall a. Show a => a -> String }
 
 n = MkN show
 
-boo = unMkN @Bool n
+boo = unMkN n @Bool
 
 boo2 :: forall (a :: * -> *) . Proxy a -> Bool
 boo2 _ = False
 
-base = boo2 Proxy
-bar'= boo2 @Maybe Proxy -- should work
+base = boo2 P
+bar'= boo2 @Maybe P -- should work