Implement type applications in patterns

The haddock submodule is also updated so that it understands the changes
to patterns.

4 files changed, 129 insertions, 31 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index f41f99be2d..6748e8a4c4 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -66,6 +66,7 @@ module GHC.Tc.Gen.HsType (
 
         -- Pattern type signatures
         tcHsPatSigType,
+        HoleMode(..),
 
         -- Error messages
         funAppCtxt, addTyConFlavCtxt
@@ -819,6 +820,9 @@ data HoleMode = HM_Sig      -- Partial type signatures: f :: _ -> Int
               | HM_VTA      -- Visible type and kind application:
                             --   f @(Maybe _)
                             --   Maybe @(_ -> _)
+              | HM_TyAppPat -- Visible type applications in patterns:
+                            --   foo (Con @_ @t x) = ...
+                            --   case x of Con @_ @t v -> ...
 
 mkMode :: TypeOrKind -> TcTyMode
 mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing }
@@ -835,9 +839,10 @@ mkHoleMode tyki hm
                           , mode_holes = Just (lvl,hm) }) }
 
 instance Outputable HoleMode where
-  ppr HM_Sig     = text "HM_Sig"
-  ppr HM_FamPat  = text "HM_FamPat"
-  ppr HM_VTA     = text "HM_VTA"
+  ppr HM_Sig      = text "HM_Sig"
+  ppr HM_FamPat   = text "HM_FamPat"
+  ppr HM_VTA      = text "HM_VTA"
+  ppr HM_TyAppPat = text "HM_TyAppPat"
 
 instance Outputable TcTyMode where
   ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm })
@@ -2103,14 +2108,16 @@ tcAnonWildCardOcc is_extra (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) }
   where
      -- See Note [Wildcard names]
      wc_nm = case hole_mode of
-               HM_Sig     -> "w"
-               HM_FamPat  -> "_"
-               HM_VTA     -> "w"
+               HM_Sig      -> "w"
+               HM_FamPat   -> "_"
+               HM_VTA      -> "w"
+               HM_TyAppPat -> "_"
 
      emit_holes = case hole_mode of
                      HM_Sig     -> True
                      HM_FamPat  -> False
                      HM_VTA     -> False
+                     HM_TyAppPat -> False
 
 tcAnonWildCardOcc _ mode ty _
 -- mode_holes is Nothing.  Should not happen, because renamer
@@ -3931,7 +3938,9 @@ information about how these are printed.
 ********************************************************************* -}
 
 tcHsPatSigType :: UserTypeCtxt
+               -> HoleMode -- HM_Sig when in a SigPat, HM_TyAppPat when in a ConPat checking type applications.
                -> HsPatSigType GhcRn          -- The type signature
+               -> ContextKind                -- What kind is expected
                -> TcM ( [(Name, TcTyVar)]     -- Wildcards
                       , [(Name, TcTyVar)]     -- The new bit of type environment, binding
                                               -- the scoped type variables
@@ -3943,12 +3952,13 @@ tcHsPatSigType :: UserTypeCtxt
 --
 -- This may emit constraints
 -- See Note [Recipe for checking a signature]
-tcHsPatSigType ctxt
+tcHsPatSigType ctxt hole_mode
   (HsPS { hsps_ext  = HsPSRn { hsps_nwcs = sig_wcs, hsps_imp_tvs = sig_ns }
         , hsps_body = hs_ty })
+  ctxt_kind
   = addSigCtxt ctxt hs_ty $
     do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
-       ; mode <- mkHoleMode TypeLevel HM_Sig
+       ; mode <- mkHoleMode TypeLevel hole_mode
        ; (wcs, sig_ty)
             <- addTypeCtxt hs_ty                     $
                solveEqualities "tcHsPatSigType" $
@@ -3956,7 +3966,7 @@ tcHsPatSigType ctxt
                  -- and c.f #16033
                bindNamedWildCardBinders sig_wcs $ \ wcs ->
                tcExtendNameTyVarEnv sig_tkv_prs $
-               do { ek     <- newOpenTypeKind
+               do { ek     <- newExpectedKind ctxt_kind
                   ; sig_ty <- tc_lhs_type mode hs_ty ek
                   ; return (wcs, sig_ty) }
 
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 5500c7692c..8507c0d7ff 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -53,6 +53,7 @@ import GHC.Builtin.Types
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Origin
 import GHC.Core.TyCon
+import GHC.Core.Type
 import GHC.Core.DataCon
 import GHC.Core.PatSyn
 import GHC.Core.ConLike
@@ -66,7 +67,7 @@ import GHC.Utils.Outputable as Outputable
 import GHC.Utils.Panic
 import qualified GHC.LanguageExtensions as LangExt
 import Control.Arrow  ( second )
-import Control.Monad  ( when )
+import Control.Monad
 import GHC.Data.List.SetOps ( getNth )
 
 {-
@@ -554,7 +555,7 @@ Fortunately that's what matchExpectedFunTySigma returns anyway.
 
 ------------------------
 -- Data constructors
-  ConPat NoExtField con arg_pats ->
+  ConPat _ con arg_pats ->
     tcConPat penv con pat_ty arg_pats thing_inside
 
 ------------------------
@@ -736,7 +737,7 @@ tcPatSig :: Bool                    -- True <=> pattern binding
                  HsWrapper)         -- Coercion due to unification with actual ty
                                     -- Of shape:  res_ty ~ sig_ty
 tcPatSig in_pat_bind sig res_ty
- = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
+ = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt HM_Sig sig OpenKind
         -- sig_tvs are the type variables free in 'sig',
         -- and not already in scope. These are the ones
         -- that should be brought into scope
@@ -890,22 +891,18 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
         ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys)
         ; checkExistentials ex_tvs all_arg_tys penv
 
-        ; tenv <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
+        ; tenv1 <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
                   -- NB: Do not use zipTvSubst!  See #14154
                   -- We want to create a well-kinded substitution, so
                   -- that the instantiated type is well-kinded
 
-        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv ex_tvs
+        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv1 ex_tvs
                      -- Get location from monad, not from ex_tvs
                      -- This freshens: See Note [Freshen existentials]
                      -- Why "super"? See Note [Binding when lookup up instances]
                      -- in GHC.Core.InstEnv.
 
-        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
-              -- pat_ty' is type of the actual constructor application
-              -- pat_ty' /= pat_ty iff coi /= IdCo
-
-              arg_tys' = substScaledTys tenv arg_tys
+        ; let arg_tys' = substScaledTys tenv arg_tys
               pat_mult = scaledMult pat_ty_scaled
               arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
 
@@ -922,7 +919,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
           then do { -- The common case; no class bindings etc
                     -- (see Note [Arrows and patterns])
                     (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys_scaled
-                                                  penv arg_pats thing_inside
+                                                  tenv penv arg_pats thing_inside
                   ; let res_pat = ConPat { pat_con = header
                                          , pat_args = arg_pats'
                                          , pat_con_ext = ConPatTc
@@ -958,7 +955,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
         ; given <- newEvVars theta'
         ; (ev_binds, (arg_pats', res))
              <- checkConstraints skol_info ex_tvs' given $
-                tcConArgs (RealDataCon data_con) arg_tys_scaled penv arg_pats thing_inside
+                tcConArgs (RealDataCon data_con) arg_tys_scaled tenv penv arg_pats thing_inside
 
         ; let res_pat = ConPat
                 { pat_con   = header
@@ -1019,7 +1016,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
         ; traceTc "checkConstraints {" Outputable.empty
         ; (ev_binds, (arg_pats', res))
              <- checkConstraints skol_info ex_tvs' prov_dicts' $
-                tcConArgs (PatSynCon pat_syn) arg_tys_scaled penv arg_pats thing_inside
+                tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside
 
         ; traceTc "checkConstraints }" (ppr ev_binds)
         ; let res_pat = ConPat { pat_con   = L con_span $ PatSynCon pat_syn
@@ -1125,17 +1122,84 @@ Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
    error messages; it's a purely internal thing
 -}
 
-tcConArgs :: ConLike -> [Scaled TcSigmaType]
-          -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
+{-
+Note [Typechecking type applications in patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+How should we typecheck type applications in patterns, such as
+   f :: Either (Maybe a) [b] -> blah
+   f (Left @x @[y] (v::Maybe x)) = blah
+
+It's quite straightforward, and very similar to the treatment of
+pattern signatures.
+
+* Step 1: bind the newly-in-scope type variables x and y to fresh
+  unification variables, say x0 and y0.
+
+* Step 2: typecheck those type arguments, @x and @[y], to get the
+  types x0 and [y0].
+
+* Step 3: Unify those types with the type arguments we expect,
+  in this case (Maybe a) and [b].  These unifications will
+  (perhaps after the constraint solver has done its work)
+  unify   x0 := Maybe a
+          y0 := b
+  Thus we learn that x stands for (Maybe a) and y for b.
+
+Wrinkles:
+
+* Surprisingly, we can discard the coercions arising from
+  these unifications.  The *only* thing the unification does is
+  to side-effect those unification variables, so that we know
+  what type x and y stand for; and cause an error if the equality
+  is not soluble.  It's a bit like a Derived constraint arising
+  from a functional dependency.
+
+* Exactly the same works for existential arguments
+     data T where
+        MkT :: a -> a -> T
+     f :: T -> blah
+     f (MkT @x v w) = ...
+   Here we create a fresh unification variable x0 for x, and
+   unify it with the fresh existential variable bound by the pattern.
+
+* Note that both here and in pattern signatures the unification may
+  not even end up unifying the variable.  For example
+     type S a b = a
+     f :: Maybe a -> Bool
+     f (Just @(S a b) x) = True :: b
+   In Step 3 we will unify (S a0 b0 ~ a), which succeeds, but has no
+   effect on the unification variable b0, to which 'b' is bound.
+   Later, in the RHS, we find that b0 must be Bool, and unify it there.
+   All is fine.
+-}
 
-tcConArgs con_like arg_tys penv con_args thing_inside = case con_args of
-  PrefixCon arg_pats -> do
+tcConArgs :: ConLike
+          -> [Scaled TcSigmaType]
+          -> TCvSubst            -- Instantiating substitution for constructor type
+          -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
+tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
+  PrefixCon type_args arg_pats -> do
         { checkTc (con_arity == no_of_args)     -- Check correct arity
                   (arityErr (text "constructor") con_like con_arity no_of_args)
+
+        ; let con_binders = conLikeUserTyVarBinders con_like
+        ; checkTc (type_args `leLength` con_binders)
+                  (conTyArgArityErr con_like (length con_binders) (length type_args))
+
         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
-        ; (arg_pats', res) <- tcMultiple tcConArg penv pats_w_tys
-                                              thing_inside
-        ; return (PrefixCon arg_pats', res) }
+        ; (type_args', (arg_pats', res))
+            <- tcMultiple tcConTyArg penv type_args $
+               tcMultiple tcConArg penv pats_w_tys thing_inside
+
+          -- This unification is straight from Figure 7 of
+          -- "Type Variables in Patterns", Haskell'18
+        ; _ <- zipWithM (unifyType Nothing) type_args' (substTyVars tenv $
+                                                        binderVars con_binders)
+          -- OK to drop coercions here. These unifications are all about
+          -- guiding inference based on a user-written type annotation
+          -- See Note [Typechecking type applications in patterns]
+
+        ; return (PrefixCon type_args arg_pats', res) }
     where
       con_arity  = conLikeArity con_like
       no_of_args = length arg_pats
@@ -1190,6 +1254,22 @@ tcConArgs con_like arg_tys penv con_args thing_inside = case con_args of
           -- dataConFieldLabels will be empty (and each field in the pattern
           -- will generate an error below).
 
+tcConTyArg :: Checker (HsPatSigType GhcRn) TcType
+tcConTyArg penv rn_ty thing_inside
+  = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsPatSigType TypeAppCtxt HM_TyAppPat rn_ty AnyKind
+               -- AnyKind is a bit suspect: it really should be the kind gotten
+               -- from instantiating the constructor type. But this would be
+               -- hard to get right, because earlier type patterns might influence
+               -- the kinds of later patterns. In any case, it all gets checked
+               -- by the calls to unifyType in tcConArgs, which will also unify
+               -- kinds.
+       ; when (not (null sig_ibs) && inPatBind penv) $
+           addErr (text "Binding type variables is not allowed in pattern bindings")
+       ; result <- tcExtendNameTyVarEnv sig_wcs $
+                   tcExtendNameTyVarEnv sig_ibs $
+                   thing_inside
+       ; return (arg_ty, result) }
+
 tcConArg :: Checker (LPat GhcRn, Scaled TcSigmaType) (LPat GhcTc)
 tcConArg penv (arg_pat, Scaled arg_mult arg_ty)
   = tc_lpat (Scaled arg_mult (mkCheckExpType arg_ty)) penv arg_pat
@@ -1211,6 +1291,14 @@ addDataConStupidTheta data_con inst_tys
          --     because the constructor might have existentials
     inst_theta = substTheta tenv stupid_theta
 
+conTyArgArityErr :: ConLike
+                 -> Int   -- expected # of arguments
+                 -> Int   -- actual # of arguments
+                 -> SDoc
+conTyArgArityErr con_like expected_number actual_number
+  = text "Too many type arguments in constructor pattern for" <+> quotes (ppr con_like) $$
+    text "Expected no more than" <+> ppr expected_number <> semi <+> text "got" <+> ppr actual_number
+
 {-
 Note [Arrows and patterns]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index ec9d1da5e9..bbbd528830 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -229,7 +229,7 @@ tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs)
 --  If there's an explicit forall, the renamer would have already reported an
 --   error for each out-of-scope type variable used
   = do  { let ctxt = RuleSigCtxt name
-        ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt rn_ty
+        ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt HM_Sig rn_ty OpenKind
         ; let id  = mkLocalId name Many id_ty
                     -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType
 
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 468410400f..dfb6e4fe3e 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -1443,7 +1443,7 @@ reifyInstances th_nm th_tys
                              -- must error before proceeding to typecheck the
                              -- renamed type, as that will result in GHC
                              -- internal errors (#13837).
-               rnImplicitBndrs Nothing tv_rdrs $ \ tv_names ->
+               rnImplicitTvOccs Nothing tv_rdrs $ \ tv_names ->
                do { (rn_ty, fvs) <- rnLHsType doc rdr_ty
                   ; return ((tv_names, rn_ty), fvs) }