never executed always true always false
    1 {-# LANGUAGE CPP #-}
    2 {-# LANGUAGE FlexibleContexts #-}
    3 {-# LANGUAGE TypeFamilies #-}
    4 
    5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
    6 
    7 {-
    8 (c) The University of Glasgow 2006
    9 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   10 
   11 -}
   12 
   13 -- | Typechecking pattern synonym declarations
   14 module GHC.Tc.TyCl.PatSyn
   15    ( tcPatSynDecl
   16    , tcPatSynBuilderBind
   17    , patSynBuilderOcc
   18    )
   19 where
   20 
   21 import GHC.Prelude
   22 
   23 import GHC.Hs
   24 import GHC.Tc.Gen.Pat
   25 import GHC.Core.Multiplicity
   26 import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType, isManyDataConTy )
   27 import GHC.Core.TyCo.Subst( extendTvSubstWithClone )
   28 import GHC.Tc.Errors.Types
   29 import GHC.Tc.Utils.Monad
   30 import GHC.Tc.Gen.Sig ( TcPragEnv, emptyPragEnv, completeSigFromId, lookupPragEnv, addInlinePrags )
   31 import GHC.Tc.Utils.Env
   32 import GHC.Tc.Utils.TcMType
   33 import GHC.Tc.Utils.Zonk
   34 import GHC.Builtin.Types.Prim
   35 import GHC.Types.Error
   36 import GHC.Types.Name
   37 import GHC.Types.Name.Set
   38 import GHC.Types.SrcLoc
   39 import GHC.Core.PatSyn
   40 import GHC.Utils.Panic
   41 import GHC.Utils.Outputable
   42 import GHC.Data.FastString
   43 import GHC.Types.Var
   44 import GHC.Types.Var.Env( emptyTidyEnv, mkInScopeSet )
   45 import GHC.Types.Id
   46 import GHC.Types.Id.Info( RecSelParent(..), setLevityInfoWithType )
   47 import GHC.Tc.Gen.Bind
   48 import GHC.Types.Basic
   49 import GHC.Tc.Solver
   50 import GHC.Tc.Utils.Unify
   51 import GHC.Core.Predicate
   52 import GHC.Builtin.Types
   53 import GHC.Tc.Utils.TcType
   54 import GHC.Tc.Types.Evidence
   55 import GHC.Tc.Types.Origin
   56 import GHC.Tc.TyCl.Build
   57 import GHC.Types.Var.Set
   58 import GHC.Types.Id.Make
   59 import GHC.Tc.TyCl.Utils
   60 import GHC.Core.ConLike
   61 import GHC.Types.FieldLabel
   62 import GHC.Rename.Env
   63 import GHC.Rename.Utils (wrapGenSpan)
   64 import GHC.Data.Bag
   65 import GHC.Utils.Misc
   66 import GHC.Driver.Session ( getDynFlags, xopt_FieldSelectors )
   67 import Data.Maybe( mapMaybe )
   68 import Control.Monad ( zipWithM )
   69 import Data.List( partition, mapAccumL )
   70 
   71 {-
   72 ************************************************************************
   73 *                                                                      *
   74                     Type checking a pattern synonym
   75 *                                                                      *
   76 ************************************************************************
   77 -}
   78 
   79 tcPatSynDecl :: PatSynBind GhcRn GhcRn
   80              -> Maybe TcSigInfo
   81              -> TcPragEnv -- See Note [Pragmas for pattern synonyms]
   82              -> TcM (LHsBinds GhcTc, TcGblEnv)
   83 tcPatSynDecl psb mb_sig prag_fn
   84   = recoverM (recoverPSB psb) $
   85     case mb_sig of
   86       Nothing                 -> tcInferPatSynDecl psb prag_fn
   87       Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi prag_fn
   88       _                       -> panic "tcPatSynDecl"
   89 
   90 recoverPSB :: PatSynBind GhcRn GhcRn
   91            -> TcM (LHsBinds GhcTc, TcGblEnv)
   92 -- See Note [Pattern synonym error recovery]
   93 recoverPSB (PSB { psb_id = L _ name
   94                 , psb_args = details })
   95  = do { matcher_name <- newImplicitBinder name mkMatcherOcc
   96       ; let placeholder = AConLike $ PatSynCon $
   97                           mk_placeholder matcher_name
   98       ; gbl_env <- tcExtendGlobalEnv [placeholder] getGblEnv
   99       ; return (emptyBag, gbl_env) }
  100   where
  101     (_arg_names, is_infix) = collectPatSynArgInfo details
  102     mk_placeholder matcher_name
  103       = mkPatSyn name is_infix
  104                         ([mkTyVarBinder SpecifiedSpec alphaTyVar], []) ([], [])
  105                         [] -- Arg tys
  106                         alphaTy
  107                         (matcher_name, matcher_ty, True) Nothing
  108                         []  -- Field labels
  109        where
  110          -- The matcher_id is used only by the desugarer, so actually
  111          -- and error-thunk would probably do just as well here.
  112          matcher_ty = mkSpecForAllTys [alphaTyVar] alphaTy
  113 
  114 {- Note [Pattern synonym error recovery]
  115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  116 If type inference for a pattern synonym fails, we can't continue with
  117 the rest of tc_patsyn_finish, because we may get knock-on errors, or
  118 even a crash.  E.g. from
  119    pattern What = True :: Maybe
  120 we get a kind error; and we must stop right away (#15289).
  121 
  122 We stop if there are /any/ unsolved constraints, not just insoluble
  123 ones; because pattern synonyms are top-level things, we will never
  124 solve them later if we can't solve them now.  And if we were to carry
  125 on, tc_patsyn_finish does zonkTcTypeToType, which defaults any
  126 unsolved unificatdion variables to Any, which confuses the error
  127 reporting no end (#15685).
  128 
  129 So we use simplifyTop to completely solve the constraint, report
  130 any errors, throw an exception.
  131 
  132 Even in the event of such an error we can recover and carry on, just
  133 as we do for value bindings, provided we plug in placeholder for the
  134 pattern synonym: see recoverPSB.  The goal of the placeholder is not
  135 to cause a raft of follow-on errors.  I've used the simplest thing for
  136 now, but we might need to elaborate it a bit later.  (e.g.  I've given
  137 it zero args, which may cause knock-on errors if it is used in a
  138 pattern.) But it'll do for now.
  139 
  140 -}
  141 
  142 tcInferPatSynDecl :: PatSynBind GhcRn GhcRn
  143                   -> TcPragEnv
  144                   -> TcM (LHsBinds GhcTc, TcGblEnv)
  145 tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
  146                        , psb_def = lpat, psb_dir = dir })
  147                   prag_fn
  148   = addPatSynCtxt lname $
  149     do { traceTc "tcInferPatSynDecl {" $ ppr name
  150 
  151        ; let (arg_names, is_infix) = collectPatSynArgInfo details
  152        ; (tclvl, wanted, ((lpat', args), pat_ty))
  153             <- pushLevelAndCaptureConstraints  $
  154                tcInferPat PatSyn lpat          $
  155                mapM tcLookupId arg_names
  156 
  157        ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
  158 
  159              named_taus = (name, pat_ty) : map mk_named_tau args
  160              mk_named_tau arg
  161                = (getName arg, mkSpecForAllTys ex_tvs (varType arg))
  162                -- The mkSpecForAllTys is important (#14552), albeit
  163                -- slightly artificial (there is no variable with this funny type).
  164                -- We do not want to quantify over variable (alpha::k)
  165                -- that mention the existentially-bound type variables
  166                -- ex_tvs in its kind k.
  167                -- See Note [Type variables whose kind is captured]
  168 
  169        ; ((univ_tvs, req_dicts, ev_binds, _), residual)
  170                <- captureConstraints $
  171                   simplifyInfer tclvl NoRestrictions [] named_taus wanted
  172        ; top_ev_binds <- checkNoErrs (simplifyTop residual)
  173        ; addTopEvBinds top_ev_binds $
  174 
  175     do { prov_dicts <- mapM zonkId prov_dicts
  176        ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
  177              -- Filtering: see Note [Remove redundant provided dicts]
  178              (prov_theta, prov_evs)
  179                  = unzip (mapMaybe mkProvEvidence filtered_prov_dicts)
  180              req_theta = map evVarPred req_dicts
  181 
  182        -- Report coercions that escape
  183        -- See Note [Coercions that escape]
  184        ; args <- mapM zonkId args
  185        ; let bad_args = [ (arg, bad_cos) | arg <- args ++ prov_dicts
  186                               , let bad_cos = filterDVarSet isId $
  187                                               (tyCoVarsOfTypeDSet (idType arg))
  188                               , not (isEmptyDVarSet bad_cos) ]
  189        ; mapM_ dependentArgErr bad_args
  190 
  191        ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
  192        ; rec_fields <- lookupConstructorFields name
  193        ; tc_patsyn_finish lname dir is_infix lpat' prag_fn
  194                           (mkTyVarBinders InferredSpec univ_tvs
  195                             , req_theta,  ev_binds, req_dicts)
  196                           (mkTyVarBinders InferredSpec ex_tvs
  197                             , mkTyVarTys ex_tvs, prov_theta, prov_evs)
  198                           (map nlHsVar args, map idType args)
  199                           pat_ty rec_fields } }
  200 
  201 mkProvEvidence :: EvId -> Maybe (PredType, EvTerm)
  202 -- See Note [Equality evidence in pattern synonyms]
  203 mkProvEvidence ev_id
  204   | EqPred r ty1 ty2 <- classifyPredType pred
  205   , let k1 = tcTypeKind ty1
  206         k2 = tcTypeKind ty2
  207         is_homo = k1 `tcEqType` k2
  208         homo_tys   = [k1, ty1, ty2]
  209         hetero_tys = [k1, k2, ty1, ty2]
  210   = case r of
  211       ReprEq | is_homo
  212              -> Just ( mkClassPred coercibleClass    homo_tys
  213                      , evDataConApp coercibleDataCon homo_tys eq_con_args )
  214              | otherwise -> Nothing
  215       NomEq  | is_homo
  216              -> Just ( mkClassPred eqClass    homo_tys
  217                      , evDataConApp eqDataCon homo_tys eq_con_args )
  218              | otherwise
  219              -> Just ( mkClassPred heqClass    hetero_tys
  220                      , evDataConApp heqDataCon hetero_tys eq_con_args )
  221 
  222   | otherwise
  223   = Just (pred, EvExpr (evId ev_id))
  224   where
  225     pred = evVarPred ev_id
  226     eq_con_args = [evId ev_id]
  227 
  228 dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
  229 -- See Note [Coercions that escape]
  230 dependentArgErr (arg, bad_cos)
  231   = failWithTc $  -- fail here: otherwise we get downstream errors
  232     TcRnUnknownMessage $ mkPlainError noHints $
  233     vcat [ text "Iceland Jack!  Iceland Jack! Stop torturing me!"
  234          , hang (text "Pattern-bound variable")
  235               2 (ppr arg <+> dcolon <+> ppr (idType arg))
  236          , nest 2 $
  237            hang (text "has a type that mentions pattern-bound coercion"
  238                  <> plural bad_co_list <> colon)
  239               2 (pprWithCommas ppr bad_co_list)
  240          , text "Hint: use -fprint-explicit-coercions to see the coercions"
  241          , text "Probable fix: add a pattern signature" ]
  242   where
  243     bad_co_list = dVarSetElems bad_cos
  244 
  245 {- Note [Type variables whose kind is captured]
  246 ~~-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  247 Consider
  248   data AST a = Sym [a]
  249   class Prj s where { prj :: [a] -> Maybe (s a) }
  250   pattern P x <= Sym (prj -> Just x)
  251 
  252 Here we get a matcher with this type
  253   $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r
  254 
  255 No problem.  But note that 's' is not fixed by the type of the
  256 pattern (AST a), nor is it existentially bound.  It's really only
  257 fixed by the type of the continuation.
  258 
  259 #14552 showed that this can go wrong if the kind of 's' mentions
  260 existentially bound variables.  We obviously can't make a type like
  261   $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r)
  262                                    -> r -> r
  263 But neither is 's' itself existentially bound, so the forall (s::k->*)
  264 can't go in the inner forall either.  (What would the matcher apply
  265 the continuation to?)
  266 
  267 Solution: do not quantiify over any unification variable whose kind
  268 mentions the existentials.  We can conveniently do that by making the
  269 "taus" passed to simplifyInfer look like
  270    forall ex_tvs. arg_ty
  271 
  272 After that, Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType takes
  273 over and errors.
  274 
  275 Note [Remove redundant provided dicts]
  276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  277 Recall that
  278    HRefl :: forall k1 k2 (a1:k1) (a2:k2). (k1 ~ k2, a1 ~ a2)
  279                                        => a1 :~~: a2
  280 (NB: technically the (k1~k2) existential dictionary is not necessary,
  281 but it's there at the moment.)
  282 
  283 Now consider (#14394):
  284    pattern Foo = HRefl
  285 in a non-poly-kinded module.  We don't want to get
  286     pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
  287 with that redundant (* ~ *).  We'd like to remove it; hence the call to
  288 mkMinimalWithSCs.
  289 
  290 Similarly consider
  291   data S a where { MkS :: Ord a => a -> S a }
  292   pattern Bam x y <- (MkS (x::a), MkS (y::a)))
  293 
  294 The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
  295 need one.  Again mkMimimalWithSCs removes the redundant one.
  296 
  297 Note [Equality evidence in pattern synonyms]
  298 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  299 Consider
  300   data X a where
  301      MkX :: Eq a => [a] -> X (Maybe a)
  302   pattern P x = MkG x
  303 
  304 Then there is a danger that GHC will infer
  305   P :: forall a.  () =>
  306        forall b. (a ~# Maybe b, Eq b) => [b] -> X a
  307 
  308 The 'builder' for P, which is called in user-code, will then
  309 have type
  310   $bP :: forall a b. (a ~# Maybe b, Eq b) => [b] -> X a
  311 
  312 and that is bad because (a ~# Maybe b) is not a predicate type
  313 (see Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
  314 and is not implicitly instantiated.
  315 
  316 So in mkProvEvidence we lift (a ~# b) to (a ~ b).  Tiresome, and
  317 marginally less efficient, if the builder/martcher are not inlined.
  318 
  319 See also Note [Lift equality constraints when quantifying] in GHC.Tc.Utils.TcType
  320 
  321 Note [Coercions that escape]
  322 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  323 #14507 showed an example where the inferred type of the matcher
  324 for the pattern synonym was something like
  325    $mSO :: forall (r :: TYPE rep) kk (a :: k).
  326            TypeRep k a
  327            -> ((Bool ~ k) => TypeRep Bool (a |> co_a2sv) -> r)
  328            -> (Void# -> r)
  329            -> r
  330 
  331 What is that co_a2sv :: Bool ~# *??  It was bound (via a superclass
  332 selection) by the pattern being matched; and indeed it is implicit in
  333 the context (Bool ~ k).  You could imagine trying to extract it like
  334 this:
  335    $mSO :: forall (r :: TYPE rep) kk (a :: k).
  336            TypeRep k a
  337            -> ( co :: ((Bool :: *) ~ (k :: *)) =>
  338                   let co_a2sv = sc_sel co
  339                   in TypeRep Bool (a |> co_a2sv) -> r)
  340            -> (Void# -> r)
  341            -> r
  342 
  343 But we simply don't allow that in types.  Maybe one day but not now.
  344 
  345 How to detect this situation?  We just look for free coercion variables
  346 in the types of any of the arguments to the matcher.  The error message
  347 is not very helpful, but at least we don't get a Lint error.
  348 -}
  349 
  350 tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
  351                   -> TcPatSynInfo
  352                   -> TcPragEnv
  353                   -> TcM (LHsBinds GhcTc, TcGblEnv)
  354 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
  355                          , psb_def = lpat, psb_dir = dir }
  356                   TPSI{ patsig_implicit_bndrs = implicit_bndrs
  357                       , patsig_univ_bndrs = explicit_univ_bndrs, patsig_req  = req_theta
  358                       , patsig_ex_bndrs   = explicit_ex_bndrs,   patsig_prov = prov_theta
  359                       , patsig_body_ty    = sig_body_ty }
  360                   prag_fn
  361   = addPatSynCtxt lname $
  362     do { traceTc "tcCheckPatSynDecl" $
  363          vcat [ ppr implicit_bndrs, ppr explicit_univ_bndrs, ppr req_theta
  364               , ppr explicit_ex_bndrs, ppr prov_theta, ppr sig_body_ty ]
  365 
  366        ; let decl_arity = length arg_names
  367              (arg_names, is_infix) = collectPatSynArgInfo details
  368 
  369        ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
  370                                  Right stuff  -> return stuff
  371                                  Left missing -> wrongNumberOfParmsErr name decl_arity missing
  372 
  373        -- Complain about:  pattern P :: () => forall x. x -> P x
  374        -- The existential 'x' should not appear in the result type
  375        -- Can't check this until we know P's arity (decl_arity above)
  376        ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) $ binderVars explicit_ex_bndrs
  377        ; checkTc (null bad_tvs) $ TcRnUnknownMessage $ mkPlainError noHints $
  378          hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
  379                    , text "namely" <+> quotes (ppr pat_ty) ])
  380             2 (text "mentions existential type variable" <> plural bad_tvs
  381                <+> pprQuotedList bad_tvs)
  382 
  383          -- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.Gen.Sig
  384        ; let univ_fvs = closeOverKinds $
  385                         (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` (binderVars explicit_univ_bndrs))
  386              (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_bndrs
  387              univ_bndrs = extra_univ ++ explicit_univ_bndrs
  388              ex_bndrs   = extra_ex   ++ explicit_ex_bndrs
  389              univ_tvs   = binderVars univ_bndrs
  390              ex_tvs     = binderVars ex_bndrs
  391 
  392          -- Pattern synonyms currently cannot be linear (#18806)
  393        ; checkTc (all (isManyDataConTy . scaledMult) arg_tys) $
  394            TcRnLinearPatSyn sig_body_ty
  395 
  396          -- Skolemise the quantified type variables. This is necessary
  397          -- in order to check the actual pattern type against the
  398          -- expected type. Even though the tyvars in the type are
  399          -- already skolems, this step changes their TcLevels,
  400          -- avoiding level-check errors when unifying.
  401        ; (skol_subst0, skol_univ_bndrs) <- skolemiseTvBndrsX emptyTCvSubst univ_bndrs
  402        ; (skol_subst, skol_ex_bndrs)    <- skolemiseTvBndrsX skol_subst0   ex_bndrs
  403        ; let skol_univ_tvs   = binderVars skol_univ_bndrs
  404              skol_ex_tvs     = binderVars skol_ex_bndrs
  405              skol_req_theta  = substTheta skol_subst0 req_theta
  406              skol_prov_theta = substTheta skol_subst  prov_theta
  407              skol_arg_tys    = substTys   skol_subst  (map scaledThing arg_tys)
  408              skol_pat_ty     = substTy    skol_subst  pat_ty
  409 
  410              univ_tv_prs     = [ (getName orig_univ_tv, skol_univ_tv)
  411                                | (orig_univ_tv, skol_univ_tv) <- univ_tvs `zip` skol_univ_tvs ]
  412 
  413        -- Right!  Let's check the pattern against the signature
  414        -- See Note [Checking against a pattern signature]
  415        ; req_dicts <- newEvVars skol_req_theta
  416        ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
  417            assertPpr (equalLength arg_names arg_tys) (ppr name $$ ppr arg_names $$ ppr arg_tys) $
  418            pushLevelAndCaptureConstraints   $
  419            tcExtendNameTyVarEnv univ_tv_prs $
  420            tcCheckPat PatSyn lpat (unrestricted skol_pat_ty)   $
  421            do { let in_scope    = mkInScopeSet (mkVarSet skol_univ_tvs)
  422                     empty_subst = mkEmptyTCvSubst in_scope
  423               ; (inst_subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst skol_ex_tvs
  424                     -- newMetaTyVarX: see the "Existential type variables"
  425                     -- part of Note [Checking against a pattern signature]
  426               ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
  427               ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
  428               ; let prov_theta' = substTheta inst_subst skol_prov_theta
  429                   -- Add univ_tvs to the in_scope set to
  430                   -- satisfy the substitution invariant. There's no need to
  431                   -- add 'ex_tvs' as they are already in the domain of the
  432                   -- substitution.
  433                   -- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst.
  434               ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
  435               ; args'      <- zipWithM (tc_arg inst_subst) arg_names
  436                                        skol_arg_tys
  437               ; return (ex_tvs', prov_dicts, args') }
  438 
  439        ; let skol_info = SigSkol (PatSynCtxt name) pat_ty []
  440                          -- The type here is a bit bogus, but we do not print
  441                          -- the type for PatSynCtxt, so it doesn't matter
  442                          -- See Note [Skolem info for pattern synonyms] in "GHC.Tc.Types.Origin"
  443        ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_univ_tvs
  444                                                     req_dicts wanted
  445 
  446        -- Solve the constraints now, because we are about to make a PatSyn,
  447        -- which should not contain unification variables and the like (#10997)
  448        ; simplifyTopImplic implics
  449 
  450        -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
  451        -- Otherwise we may get a type error when typechecking the builder,
  452        -- when that should be impossible
  453 
  454        ; traceTc "tcCheckPatSynDecl }" $ ppr name
  455 
  456        ; rec_fields <- lookupConstructorFields name
  457        ; tc_patsyn_finish lname dir is_infix lpat' prag_fn
  458                           (skol_univ_bndrs, skol_req_theta, ev_binds, req_dicts)
  459                           (skol_ex_bndrs, mkTyVarTys ex_tvs', skol_prov_theta, prov_dicts)
  460                           (args', skol_arg_tys)
  461                           skol_pat_ty rec_fields }
  462   where
  463     tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTc)
  464      -- Look up the variable actually bound by lpat
  465      -- and check that it has the expected type
  466     tc_arg subst arg_name arg_ty
  467       = setSrcSpan (nameSrcSpan arg_name) $
  468            -- Set the SrcSpan to be the binding site of the Id (#18856)
  469            -- e.g.  pattern P :: Int -> Maybe (Int,Bool)
  470            --       pattern P x = Just (x,True)
  471            -- Before unifying x's actual type with its expected type, in tc_arg, set
  472            -- location to x's binding site in lpat, namely the 'x' in Just (x,True).
  473            -- Else the error message location is wherever tcCheckPat finished,
  474            -- namely the right-hand corner of the pattern
  475         do { arg_id <- tcLookupId arg_name
  476            ; wrap <- tcSubTypeSigma GenSigCtxt
  477                                     (idType arg_id)
  478                                     (substTy subst arg_ty)
  479                 -- Why do we need tcSubType here?
  480                 -- See Note [Pattern synonyms and higher rank types]
  481            ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
  482 
  483 skolemiseTvBndrsX :: TCvSubst -> [VarBndr TyVar flag]
  484                   -> TcM (TCvSubst, [VarBndr TcTyVar flag])
  485 -- Make new TcTyVars, all skolems with levels, but do not clone
  486 -- The level is one level deeper than the current level
  487 -- See Note [Skolemising when checking a pattern synonym]
  488 skolemiseTvBndrsX orig_subst tvs
  489   = do { tc_lvl <- getTcLevel
  490        ; let pushed_lvl = pushTcLevel tc_lvl
  491              details    = SkolemTv pushed_lvl False
  492 
  493              mk_skol_tv_x :: TCvSubst -> VarBndr TyVar flag
  494                           -> (TCvSubst, VarBndr TcTyVar flag)
  495              mk_skol_tv_x subst (Bndr tv flag)
  496                = (subst', Bndr new_tv flag)
  497                where
  498                  new_kind = substTyUnchecked subst (tyVarKind tv)
  499                  new_tv   = mkTcTyVar (tyVarName tv) new_kind details
  500                  subst'   = extendTvSubstWithClone subst tv new_tv
  501 
  502        ; return (mapAccumL mk_skol_tv_x orig_subst tvs) }
  503 
  504 {- Note [Skolemising when checking a pattern synonym]
  505 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  506 Consider
  507    pattern P1 :: forall a. a -> Maybe a
  508    pattern P1 x <- Just x where
  509       P1 x = Just (x :: a)
  510 
  511 The scoped type variable 'a' scopes over the builder RHS, Just (x::a).
  512 But the builder RHS is typechecked much later in tcPatSynBuilderBind,
  513 and gets its scoped type variables from the type of the builder_id.
  514 The easiest way to achieve this is not to clone when skolemising.
  515 
  516 Hence a special-purpose skolemiseTvBndrX here, similar to
  517 GHC.Tc.Utils.Instantiate.tcInstSkolTyVarsX except that the latter
  518 does cloning.
  519 
  520 Note [Pattern synonyms and higher rank types]
  521 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  522 Consider
  523   data T = MkT (forall a. a->a)
  524 
  525   pattern P :: (Int -> Int) -> T
  526   pattern P x <- MkT x
  527 
  528 This should work.  But in the matcher we must match against MkT, and then
  529 instantiate its argument 'x', to get a function of type (Int -> Int).
  530 Equality is not enough!  #13752 was an example.
  531 
  532 
  533 Note [The pattern-synonym signature splitting rule]
  534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  535 Given a pattern signature, we must split
  536      the kind-generalised variables, and
  537      the implicitly-bound variables
  538 into universal and existential.  The rule is this
  539 (see discussion on #11224):
  540 
  541      The universal tyvars are the ones mentioned in
  542           - univ_tvs: the user-specified (forall'd) universals
  543           - req_theta
  544           - res_ty
  545      The existential tyvars are all the rest
  546 
  547 For example
  548 
  549    pattern P :: () => b -> T a
  550    pattern P x = ...
  551 
  552 Here 'a' is universal, and 'b' is existential.  But there is a wrinkle:
  553 how do we split the arg_tys from req_ty?  Consider
  554 
  555    pattern Q :: () => b -> S c -> T a
  556    pattern Q x = ...
  557 
  558 This is an odd example because Q has only one syntactic argument, and
  559 so presumably is defined by a view pattern matching a function.  But
  560 it can happen (#11977, #12108).
  561 
  562 We don't know Q's arity from the pattern signature, so we have to wait
  563 until we see the pattern declaration itself before deciding res_ty is,
  564 and hence which variables are existential and which are universal.
  565 
  566 And that in turn is why TcPatSynInfo has a separate field,
  567 patsig_implicit_bndrs, to capture the implicitly bound type variables,
  568 because we don't yet know how to split them up.
  569 
  570 It's a slight compromise, because it means we don't really know the
  571 pattern synonym's real signature until we see its declaration.  So,
  572 for example, in hs-boot file, we may need to think what to do...
  573 (eg don't have any implicitly-bound variables).
  574 
  575 
  576 Note [Checking against a pattern signature]
  577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  578 When checking the actual supplied pattern against the pattern synonym
  579 signature, we need to be quite careful.
  580 
  581 ----- Provided constraints
  582 Example
  583 
  584     data T a where
  585       MkT :: Ord a => a -> T a
  586 
  587     pattern P :: () => Eq a => a -> [T a]
  588     pattern P x = [MkT x]
  589 
  590 We must check that the (Eq a) that P claims to bind (and to
  591 make available to matches against P), is derivable from the
  592 actual pattern.  For example:
  593     f (P (x::a)) = ...here (Eq a) should be available...
  594 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
  595 
  596 ----- Existential type variables
  597 Unusually, we instantiate the existential tyvars of the pattern with
  598 *meta* type variables.  For example
  599 
  600     data S where
  601       MkS :: Eq a => [a] -> S
  602 
  603     pattern P :: () => Eq x => x -> S
  604     pattern P x <- MkS x
  605 
  606 The pattern synonym conceals from its client the fact that MkS has a
  607 list inside it.  The client just thinks it's a type 'x'.  So we must
  608 unify x := [a] during type checking, and then use the instantiating type
  609 [a] (called ex_tys) when building the matcher.  In this case we'll get
  610 
  611    $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
  612    $mP x k = case x of
  613                MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
  614                                               dl = $dfunEqList d
  615                                           in k [a] dl ys
  616 
  617 All this applies when type-checking the /matching/ side of
  618 a pattern synonym.  What about the /building/ side?
  619 
  620 * For Unidirectional, there is no builder
  621 
  622 * For ExplicitBidirectional, the builder is completely separate
  623   code, typechecked in tcPatSynBuilderBind
  624 
  625 * For ImplicitBidirectional, the builder is still typechecked in
  626   tcPatSynBuilderBind, by converting the pattern to an expression and
  627   typechecking it.
  628 
  629   At one point, for ImplicitBidirectional I used TyVarTvs (instead of
  630   TauTvs) in tcCheckPatSynDecl.  But (a) strengthening the check here
  631   is redundant since tcPatSynBuilderBind does the job, (b) it was
  632   still incomplete (TyVarTvs can unify with each other), and (c) it
  633   didn't even work (#13441 was accepted with
  634   ExplicitBidirectional, but rejected if expressed in
  635   ImplicitBidirectional form.  Conclusion: trying to be too clever is
  636   a bad idea.
  637 -}
  638 
  639 collectPatSynArgInfo :: HsPatSynDetails GhcRn
  640                      -> ([Name], Bool)
  641 collectPatSynArgInfo details =
  642   case details of
  643     PrefixCon _ names    -> (map unLoc names, False)
  644     InfixCon name1 name2 -> (map unLoc [name1, name2], True)
  645     RecCon names         -> (map (unLoc . recordPatSynPatVar) names, False)
  646 
  647 addPatSynCtxt :: LocatedN Name -> TcM a -> TcM a
  648 addPatSynCtxt (L loc name) thing_inside
  649   = setSrcSpanA loc $
  650     addErrCtxt (text "In the declaration for pattern synonym"
  651                 <+> quotes (ppr name)) $
  652     thing_inside
  653 
  654 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
  655 wrongNumberOfParmsErr name decl_arity missing
  656   = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
  657     hang (text "Pattern synonym" <+> quotes (ppr name) <+> text "has"
  658           <+> speakNOf decl_arity (text "argument"))
  659        2 (text "but its type signature has" <+> int missing <+> text "fewer arrows")
  660 
  661 -------------------------
  662 -- Shared by both tcInferPatSyn and tcCheckPatSyn
  663 tc_patsyn_finish :: LocatedN Name   -- ^ PatSyn Name
  664                  -> HsPatSynDir GhcRn -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
  665                  -> Bool              -- ^ Whether infix
  666                  -> LPat GhcTc        -- ^ Pattern of the PatSyn
  667                  -> TcPragEnv
  668                  -> ([TcInvisTVBinder], [PredType], TcEvBinds, [EvVar])
  669                  -> ([TcInvisTVBinder], [TcType], [PredType], [EvTerm])
  670                  -> ([LHsExpr GhcTc], [TcType])  -- ^ Pattern arguments and types
  671                  -> TcType            -- ^ Pattern type
  672                  -> [FieldLabel]      -- ^ Selector names
  673                  -- ^ Whether fields, empty if not record PatSyn
  674                  -> TcM (LHsBinds GhcTc, TcGblEnv)
  675 tc_patsyn_finish lname dir is_infix lpat' prag_fn
  676                  (univ_tvs, req_theta, req_ev_binds, req_dicts)
  677                  (ex_tvs,   ex_tys,    prov_theta,   prov_dicts)
  678                  (args, arg_tys)
  679                  pat_ty field_labels
  680   = do { -- Zonk everything.  We are about to build a final PatSyn
  681          -- so there had better be no unification variables in there
  682 
  683        ; ze              <- mkEmptyZonkEnv NoFlexi
  684        ; (ze, univ_tvs') <- zonkTyVarBindersX   ze univ_tvs
  685        ; req_theta'      <- zonkTcTypesToTypesX ze req_theta
  686        ; (ze, ex_tvs')   <- zonkTyVarBindersX   ze ex_tvs
  687        ; prov_theta'     <- zonkTcTypesToTypesX ze prov_theta
  688        ; pat_ty'         <- zonkTcTypeToTypeX   ze pat_ty
  689        ; arg_tys'        <- zonkTcTypesToTypesX ze arg_tys
  690 
  691        ; let (env1, univ_tvs) = tidyTyCoVarBinders emptyTidyEnv univ_tvs'
  692              (env2, ex_tvs)   = tidyTyCoVarBinders env1 ex_tvs'
  693              req_theta  = tidyTypes env2 req_theta'
  694              prov_theta = tidyTypes env2 prov_theta'
  695              arg_tys    = tidyTypes env2 arg_tys'
  696              pat_ty     = tidyType  env2 pat_ty'
  697 
  698        ; traceTc "tc_patsyn_finish {" $
  699            ppr (unLoc lname) $$ ppr (unLoc lpat') $$
  700            ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
  701            ppr (ex_tvs, prov_theta, prov_dicts) $$
  702            ppr args $$
  703            ppr arg_tys $$
  704            ppr pat_ty
  705 
  706        -- Make the 'matcher'
  707        ; (matcher, matcher_bind) <- tcPatSynMatcher lname lpat' prag_fn
  708                                          (binderVars univ_tvs, req_theta, req_ev_binds, req_dicts)
  709                                          (binderVars ex_tvs, ex_tys, prov_theta, prov_dicts)
  710                                          (args, arg_tys)
  711                                          pat_ty
  712 
  713        -- Make the 'builder'
  714        ; builder <- mkPatSynBuilder dir lname
  715                                     univ_tvs req_theta
  716                                     ex_tvs   prov_theta
  717                                     arg_tys pat_ty
  718 
  719        -- Make the PatSyn itself
  720        ; let patSyn = mkPatSyn (unLoc lname) is_infix
  721                         (univ_tvs, req_theta)
  722                         (ex_tvs, prov_theta)
  723                         arg_tys
  724                         pat_ty
  725                         matcher builder
  726                         field_labels
  727 
  728        -- Selectors
  729        ; has_sel <- xopt_FieldSelectors <$> getDynFlags
  730        ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn) has_sel
  731              tything = AConLike (PatSynCon patSyn)
  732        ; tcg_env <- tcExtendGlobalEnv [tything] $
  733                     tcRecSelBinds rn_rec_sel_binds
  734 
  735        ; traceTc "tc_patsyn_finish }" empty
  736        ; return (matcher_bind, tcg_env) }
  737 
  738 {-
  739 ************************************************************************
  740 *                                                                      *
  741          Constructing the "matcher" Id and its binding
  742 *                                                                      *
  743 ************************************************************************
  744 -}
  745 
  746 tcPatSynMatcher :: LocatedN Name
  747                 -> LPat GhcTc
  748                 -> TcPragEnv
  749                 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
  750                 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
  751                 -> ([LHsExpr GhcTc], [TcType])
  752                 -> TcType
  753                 -> TcM (PatSynMatcher, LHsBinds GhcTc)
  754 -- See Note [Matchers and builders for pattern synonyms] in GHC.Core.PatSyn
  755 tcPatSynMatcher (L loc name) lpat prag_fn
  756                 (univ_tvs, req_theta, req_ev_binds, req_dicts)
  757                 (ex_tvs, ex_tys, prov_theta, prov_dicts)
  758                 (args, arg_tys) pat_ty
  759   = do { let loc' = locA loc
  760        ; rr_name <- newNameAt (mkTyVarOcc "rep") loc'
  761        ; tv_name <- newNameAt (mkTyVarOcc "r")   loc'
  762        ; let rr_tv  = mkTyVar rr_name runtimeRepTy
  763              rr     = mkTyVarTy rr_tv
  764              res_tv = mkTyVar tv_name (tYPE rr)
  765              res_ty = mkTyVarTy res_tv
  766              is_unlifted = null args && null prov_dicts
  767              (cont_args, cont_arg_tys)
  768                | is_unlifted = ([nlHsVar voidPrimId], [unboxedUnitTy])
  769                | otherwise   = (args,                 arg_tys)
  770              cont_ty = mkInfSigmaTy ex_tvs prov_theta $
  771                        mkVisFunTysMany cont_arg_tys res_ty
  772 
  773              fail_ty  = mkVisFunTyMany unboxedUnitTy res_ty
  774 
  775        ; matcher_name <- newImplicitBinder name mkMatcherOcc
  776        ; scrutinee    <- newSysLocalId (fsLit "scrut") Many pat_ty
  777        ; cont         <- newSysLocalId (fsLit "cont")  Many cont_ty
  778        ; fail         <- newSysLocalId (fsLit "fail")  Many fail_ty
  779 
  780        ; dflags       <- getDynFlags
  781        ; let matcher_tau   = mkVisFunTysMany [pat_ty, cont_ty, fail_ty] res_ty
  782              matcher_sigma = mkInfSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
  783              matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
  784              patsyn_id     = mkExportedVanillaId name matcher_sigma
  785                              -- See Note [Exported LocalIds] in GHC.Types.Id
  786 
  787              inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
  788              cont' = foldl' nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
  789 
  790              fail' = nlHsApps fail [nlHsVar voidPrimId]
  791 
  792              args = map nlVarPat [scrutinee, cont, fail]
  793              lwpat = noLocA $ WildPat pat_ty
  794              cases = if isIrrefutableHsPat dflags lpat
  795                      then [mkHsCaseAlt lpat  cont']
  796                      else [mkHsCaseAlt lpat  cont',
  797                            mkHsCaseAlt lwpat fail']
  798              body = mkLHsWrap (mkWpLet req_ev_binds) $
  799                     L (getLoc lpat) $
  800                     HsCase noExtField (nlHsVar scrutinee) $
  801                     MG{ mg_alts = L (l2l $ getLoc lpat) cases
  802                       , mg_ext = MatchGroupTc [unrestricted pat_ty] res_ty
  803                       , mg_origin = Generated
  804                       }
  805              body' = noLocA $
  806                      HsLam noExtField $
  807                      MG{ mg_alts = noLocA [mkSimpleMatch LambdaExpr
  808                                                          args body]
  809                        , mg_ext = MatchGroupTc (map unrestricted [pat_ty, cont_ty, fail_ty]) res_ty
  810                        , mg_origin = Generated
  811                        }
  812              match = mkMatch (mkPrefixFunRhs (L loc patsyn_id)) []
  813                              (mkHsLams (rr_tv:res_tv:univ_tvs)
  814                                        req_dicts body')
  815                              (EmptyLocalBinds noExtField)
  816              mg :: MatchGroup GhcTc (LHsExpr GhcTc)
  817              mg = MG{ mg_alts = L (l2l $ getLoc match) [match]
  818                     , mg_ext = MatchGroupTc [] res_ty
  819                     , mg_origin = Generated
  820                     }
  821              prags = lookupPragEnv prag_fn name
  822              -- See Note [Pragmas for pattern synonyms]
  823 
  824        ; matcher_prag_id <- addInlinePrags matcher_id prags
  825        ; let bind = FunBind{ fun_id = L loc matcher_prag_id
  826                            , fun_matches = mg
  827                            , fun_ext = idHsWrapper
  828                            , fun_tick = [] }
  829              matcher_bind = unitBag (noLocA bind)
  830        ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
  831        ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
  832 
  833        ; return ((matcher_name, matcher_sigma, is_unlifted), matcher_bind) }
  834 
  835 mkPatSynRecSelBinds :: PatSyn
  836                     -> [FieldLabel]  -- ^ Visible field labels
  837                     -> FieldSelectors
  838                     -> [(Id, LHsBind GhcRn)]
  839 mkPatSynRecSelBinds ps fields has_sel
  840   = [ mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl has_sel
  841     | fld_lbl <- fields ]
  842 
  843 isUnidirectional :: HsPatSynDir a -> Bool
  844 isUnidirectional Unidirectional          = True
  845 isUnidirectional ImplicitBidirectional   = False
  846 isUnidirectional ExplicitBidirectional{} = False
  847 
  848 {-
  849 ************************************************************************
  850 *                                                                      *
  851          Constructing the "builder" Id
  852 *                                                                      *
  853 ************************************************************************
  854 -}
  855 
  856 mkPatSynBuilder :: HsPatSynDir a -> LocatedN Name
  857                 -> [InvisTVBinder] -> ThetaType
  858                 -> [InvisTVBinder] -> ThetaType
  859                 -> [Type] -> Type
  860                 -> TcM PatSynBuilder
  861 mkPatSynBuilder dir (L _ name)
  862                   univ_bndrs req_theta ex_bndrs prov_theta
  863                   arg_tys pat_ty
  864   | isUnidirectional dir
  865   = return Nothing
  866   | otherwise
  867   = do { builder_name <- newImplicitBinder name mkBuilderOcc
  868        ; let theta          = req_theta ++ prov_theta
  869              need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
  870              builder_sigma  = add_void need_dummy_arg $
  871                               mkInvisForAllTys univ_bndrs $
  872                               mkInvisForAllTys ex_bndrs $
  873                               mkPhiTy theta $
  874                               mkVisFunTysMany arg_tys $
  875                               pat_ty
  876        ; return (Just (builder_name, builder_sigma, need_dummy_arg)) }
  877 
  878 tcPatSynBuilderBind :: TcPragEnv
  879                     -> PatSynBind GhcRn GhcRn
  880                     -> TcM (LHsBinds GhcTc)
  881 -- See Note [Matchers and builders for pattern synonyms] in GHC.Core.PatSyn
  882 tcPatSynBuilderBind prag_fn (PSB { psb_id = ps_lname@(L loc ps_name)
  883                                  , psb_def = lpat
  884                                  , psb_dir = dir
  885                                  , psb_args = details })
  886   | isUnidirectional dir
  887   = return emptyBag
  888 
  889   | Left why <- mb_match_group       -- Can't invert the pattern
  890   = setSrcSpan (getLocA lpat) $ failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
  891     vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
  892                  <+> quotes (ppr ps_name) <> colon)
  893               2 why
  894          , text "RHS pattern:" <+> ppr lpat ]
  895 
  896   | Right match_group <- mb_match_group  -- Bidirectional
  897   = do { patsyn <- tcLookupPatSyn ps_name
  898        ; case patSynBuilder patsyn of {
  899            Nothing -> return emptyBag ;
  900              -- This case happens if we found a type error in the
  901              -- pattern synonym, recovered, and put a placeholder
  902              -- with patSynBuilder=Nothing in the environment
  903 
  904            Just (builder_name, builder_ty, need_dummy_arg) ->  -- Normal case
  905     do { -- Bidirectional, so patSynBuilder returns Just
  906          let pat_ty = patSynResultType patsyn
  907              builder_id = modifyIdInfo (`setLevityInfoWithType` pat_ty) $
  908                           mkExportedVanillaId builder_name builder_ty
  909                          -- See Note [Exported LocalIds] in GHC.Types.Id
  910              prags = lookupPragEnv prag_fn ps_name
  911              -- See Note [Pragmas for pattern synonyms]
  912              -- Keyed by the PatSyn Name, not the (internal) builder name
  913 
  914        ; builder_id <- addInlinePrags builder_id prags
  915 
  916        ; let match_group' | need_dummy_arg = add_dummy_arg match_group
  917                           | otherwise      = match_group
  918 
  919              bind = FunBind { fun_id      = L loc (idName builder_id)
  920                             , fun_matches = match_group'
  921                             , fun_ext     = emptyNameSet
  922                             , fun_tick    = [] }
  923 
  924              sig = completeSigFromId (PatSynCtxt ps_name) builder_id
  925 
  926        ; traceTc "tcPatSynBuilderBind {" $
  927          vcat [ ppr patsyn
  928               , ppr builder_id <+> dcolon <+> ppr (idType builder_id)
  929               , ppr prags ]
  930        ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLocA bind)
  931        ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
  932        ; return builder_binds } } }
  933 
  934 #if __GLASGOW_HASKELL__ <= 810
  935   | otherwise = panic "tcPatSynBuilderBind"  -- Both cases dealt with
  936 #endif
  937   where
  938     mb_match_group
  939        = case dir of
  940            ExplicitBidirectional explicit_mg -> Right explicit_mg
  941            ImplicitBidirectional -> fmap mk_mg (tcPatToExpr ps_name args lpat)
  942            Unidirectional -> panic "tcPatSynBuilderBind"
  943 
  944     mk_mg :: LHsExpr GhcRn -> MatchGroup GhcRn (LHsExpr GhcRn)
  945     mk_mg body = mkMatchGroup Generated (noLocA [builder_match])
  946           where
  947             builder_args  = [L (na2la loc) (VarPat noExtField (L loc n))
  948                             | L loc n <- args]
  949             builder_match = mkMatch (mkPrefixFunRhs ps_lname)
  950                                     builder_args body
  951                                     (EmptyLocalBinds noExtField)
  952 
  953     args = case details of
  954               PrefixCon _ args   -> args
  955               InfixCon arg1 arg2 -> [arg1, arg2]
  956               RecCon args        -> map recordPatSynPatVar args
  957 
  958     add_dummy_arg :: MatchGroup GhcRn (LHsExpr GhcRn)
  959                   -> MatchGroup GhcRn (LHsExpr GhcRn)
  960     add_dummy_arg mg@(MG { mg_alts =
  961                            (L l [L loc match@(Match { m_pats = pats })]) })
  962       = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
  963     add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
  964                              pprMatches other_mg
  965 
  966 patSynBuilderOcc :: PatSyn -> Maybe (HsExpr GhcTc, TcSigmaType)
  967 patSynBuilderOcc ps
  968   | Just (_, builder_ty, add_void_arg) <- patSynBuilder ps
  969   , let builder_expr = mkConLikeTc (PatSynCon ps)
  970   = Just $
  971     if add_void_arg
  972     then ( builder_expr   -- still just return builder_expr; the void# arg
  973                           -- is added by dsConLike in the desugarer
  974          , tcFunResultTy builder_ty )
  975     else (builder_expr, builder_ty)
  976 
  977   | otherwise  -- Unidirectional
  978   = Nothing
  979 
  980 add_void :: Bool -> Type -> Type
  981 add_void need_dummy_arg ty
  982   | need_dummy_arg = mkVisFunTyMany unboxedUnitTy ty
  983   | otherwise      = ty
  984 
  985 tcPatToExpr :: Name -> [LocatedN Name] -> LPat GhcRn
  986             -> Either SDoc (LHsExpr GhcRn)
  987 -- Given a /pattern/, return an /expression/ that builds a value
  988 -- that matches the pattern.  E.g. if the pattern is (Just [x]),
  989 -- the expression is (Just [x]).  They look the same, but the
  990 -- input uses constructors from HsPat and the output uses constructors
  991 -- from HsExpr.
  992 --
  993 -- Returns (Left r) if the pattern is not invertible, for reason r.
  994 -- See Note [Builder for a bidirectional pattern synonym]
  995 tcPatToExpr name args pat = go pat
  996   where
  997     lhsVars = mkNameSet (map unLoc args)
  998 
  999     -- Make a prefix con for prefix and infix patterns for simplicity
 1000     mkPrefixConExpr :: LocatedN Name -> [LPat GhcRn]
 1001                     -> Either SDoc (HsExpr GhcRn)
 1002     mkPrefixConExpr lcon@(L loc _) pats
 1003       = do { exprs <- mapM go pats
 1004            ; let con = L (l2l loc) (HsVar noExtField lcon)
 1005            ; return (unLoc $ mkHsApps con exprs)
 1006            }
 1007 
 1008     mkRecordConExpr :: LocatedN Name -> HsRecFields GhcRn (LPat GhcRn)
 1009                     -> Either SDoc (HsExpr GhcRn)
 1010     mkRecordConExpr con (HsRecFields fields dd)
 1011       = do { exprFields <- mapM go' fields
 1012            ; return (RecordCon noExtField con (HsRecFields exprFields dd)) }
 1013 
 1014     go' :: LHsRecField GhcRn (LPat GhcRn) -> Either SDoc (LHsRecField GhcRn (LHsExpr GhcRn))
 1015     go' (L l rf) = L l <$> traverse go rf
 1016 
 1017     go :: LPat GhcRn -> Either SDoc (LHsExpr GhcRn)
 1018     go (L loc p) = L loc <$> go1 p
 1019 
 1020     go1 :: Pat GhcRn -> Either SDoc (HsExpr GhcRn)
 1021     go1 (ConPat NoExtField con info)
 1022       = case info of
 1023           PrefixCon _ ps -> mkPrefixConExpr con ps
 1024           InfixCon l r   -> mkPrefixConExpr con [l,r]
 1025           RecCon fields  -> mkRecordConExpr con fields
 1026 
 1027     go1 (SigPat _ pat _) = go1 (unLoc pat)
 1028         -- See Note [Type signatures and the builder expression]
 1029 
 1030     go1 (VarPat _ (L l var))
 1031         | var `elemNameSet` lhsVars
 1032         = return $ HsVar noExtField (L l var)
 1033         | otherwise
 1034         = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
 1035     go1 (ParPat _ lpar pat rpar) = fmap (\e -> HsPar noAnn lpar e rpar) $ go pat
 1036     go1 (ListPat _ pats)
 1037       = do { exprs <- mapM go pats
 1038            ; return $ ExplicitList noExtField exprs }
 1039     go1 (TuplePat _ pats box)       = do { exprs <- mapM go pats
 1040                                          ; return $ ExplicitTuple noExtField
 1041                                            (map (Present noAnn) exprs) box }
 1042     go1 (SumPat _ pat alt arity)    = do { expr <- go1 (unLoc pat)
 1043                                          ; return $ ExplicitSum noExtField alt arity
 1044                                                                    (noLocA expr)
 1045                                          }
 1046     go1 (LitPat _ lit)              = return $ HsLit noComments lit
 1047     go1 (NPat _ (L _ n) mb_neg _)
 1048         | Just (SyntaxExprRn neg) <- mb_neg
 1049                                     = return $ unLoc $ foldl' nlHsApp (noLocA neg)
 1050                                                        [noLocA (HsOverLit noAnn n)]
 1051         | otherwise                 = return $ HsOverLit noAnn n
 1052     go1 (SplicePat _ (HsSpliced _ _ (HsSplicedPat pat)))
 1053                                     = go1 pat
 1054     go1 (SplicePat _ (HsSpliced{})) = panic "Invalid splice variety"
 1055     go1 (XPat (HsPatExpanded _ pat))= go1 pat
 1056 
 1057     -- See Note [Invertible view patterns]
 1058     go1 p@(ViewPat mbInverse _ pat) = case mbInverse of
 1059       Nothing      -> notInvertible p
 1060       Just inverse ->
 1061         fmap
 1062           (\ expr -> HsApp noAnn (wrapGenSpan inverse) (wrapGenSpan expr))
 1063           (go1 (unLoc pat))
 1064 
 1065     -- The following patterns are not invertible.
 1066     go1 p@(BangPat {})                       = notInvertible p -- #14112
 1067     go1 p@(LazyPat {})                       = notInvertible p
 1068     go1 p@(WildPat {})                       = notInvertible p
 1069     go1 p@(AsPat {})                         = notInvertible p
 1070     go1 p@(NPlusKPat {})                     = notInvertible p
 1071     go1 p@(SplicePat _ (HsTypedSplice {}))   = notInvertible p
 1072     go1 p@(SplicePat _ (HsUntypedSplice {})) = notInvertible p
 1073     go1 p@(SplicePat _ (HsQuasiQuote {}))    = notInvertible p
 1074 
 1075     notInvertible p = Left (not_invertible_msg p)
 1076 
 1077     not_invertible_msg p
 1078       =   text "Pattern" <+> quotes (ppr p) <+> text "is not invertible"
 1079       $+$ hang (text "Suggestion: instead use an explicitly bidirectional"
 1080                 <+> text "pattern synonym, e.g.")
 1081              2 (hang (text "pattern" <+> pp_name <+> pp_args <+> larrow
 1082                       <+> ppr pat <+> text "where")
 1083                    2 (pp_name <+> pp_args <+> equals <+> text "..."))
 1084       where
 1085         pp_name = ppr name
 1086         pp_args = hsep (map ppr args)
 1087 
 1088 
 1089 {- Note [Builder for a bidirectional pattern synonym]
 1090 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1091 For a bidirectional pattern synonym, the function 'tcPatToExpr'
 1092 needs to produce an /expression/ that matches the supplied /pattern/,
 1093 given values for the arguments of the pattern synonym. For example:
 1094   pattern F x y = (Just x, [y])
 1095 The 'builder' for F looks like
 1096   $builderF x y = (Just x, [y])
 1097 
 1098 We can't always do this:
 1099  * Some patterns aren't invertible; e.g. general view patterns
 1100       pattern F x = (f -> x)
 1101    as we don't have the ability to write down an expression that matches
 1102    the view pattern specified by an arbitrary view function `f`.
 1103    It is however sometimes possible to write down an inverse;
 1104      see Note [Invertible view patterns].
 1105 
 1106  * The RHS pattern might bind more variables than the pattern
 1107    synonym, so again we can't invert it
 1108       pattern F x = (x,y)
 1109 
 1110  * Ditto wildcards
 1111       pattern F x = (x,_)
 1112 
 1113 Note [Invertible view patterns]
 1114 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1115 For some view patterns, such as those that arise from expansion of overloaded
 1116 patterns (as detailed in Note [Handling overloaded and rebindable patterns]),
 1117 we are able to explicitly write out an inverse (in the sense of the previous
 1118 Note [Builder for a bidirectional pattern synonym]).
 1119 For instance, the inverse to the pattern
 1120 
 1121   (toList -> [True, False])
 1122 
 1123 is the expression
 1124 
 1125   (fromListN 2 [True,False])
 1126 
 1127 Keeping track of the inverse for such view patterns fixed #14380.
 1128 
 1129 Note [Redundant constraints for builder]
 1130 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1131 The builder can have redundant constraints, which are awkward to eliminate.
 1132 Consider
 1133    pattern P = Just 34
 1134 To match against this pattern we need (Eq a, Num a).  But to build
 1135 (Just 34) we need only (Num a).  Fortunately instTcSigFromId sets
 1136 sig_warn_redundant to False.
 1137 
 1138 ************************************************************************
 1139 *                                                                      *
 1140          Helper functions
 1141 *                                                                      *
 1142 ************************************************************************
 1143 
 1144 Note [As-patterns in pattern synonym definitions]
 1145 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1146 The rationale for rejecting as-patterns in pattern synonym definitions
 1147 is that an as-pattern would introduce nonindependent pattern synonym
 1148 arguments, e.g. given a pattern synonym like:
 1149 
 1150         pattern K x y = x@(Just y)
 1151 
 1152 one could write a nonsensical function like
 1153 
 1154         f (K Nothing x) = ...
 1155 
 1156 or
 1157         g (K (Just True) False) = ...
 1158 
 1159 Note [Type signatures and the builder expression]
 1160 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1161 Consider
 1162    pattern L x = Left x :: Either [a] [b]
 1163 
 1164 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
 1165 specified type.  We check the pattern *as a pattern*, so the type
 1166 signature is a pattern signature, and so brings 'a' and 'b' into
 1167 scope.  But we don't have a way to bind 'a, b' in the LHS, as we do
 1168 'x', say.  Nevertheless, the signature may be useful to constrain
 1169 the type.
 1170 
 1171 When making the binding for the *builder*, though, we don't want
 1172   $buildL x = Left x :: Either [a] [b]
 1173 because that wil either mean (forall a b. Either [a] [b]), or we'll
 1174 get a complaint that 'a' and 'b' are out of scope. (Actually the
 1175 latter; #9867.)  No, the job of the signature is done, so when
 1176 converting the pattern to an expression (for the builder RHS) we
 1177 simply discard the signature.
 1178 
 1179 Note [Record PatSyn Desugaring]
 1180 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1181 It is important that prov_theta comes before req_theta as this ordering is used
 1182 when desugaring record pattern synonym updates.
 1183 
 1184 Any change to this ordering should make sure to change GHC.HsToCore.Expr if you
 1185 want to avoid difficult to decipher core lint errors!
 1186 
 1187 Note [Pragmas for pattern synonyms]
 1188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1189 INLINE and NOINLINE pragmas are supported for pattern synonyms. They affect both
 1190 the matcher and the builder.
 1191 (See Note [Matchers and builders for pattern synonyms] in PatSyn)
 1192 
 1193 For example:
 1194     pattern InlinedPattern x = [x]
 1195     {-# INLINE InlinedPattern #-}
 1196     pattern NonInlinedPattern x = [x]
 1197     {-# NOINLINE NonInlinedPattern #-}
 1198 
 1199 For pattern synonyms with explicit builders, only pragma for the entire pattern
 1200 synonym is supported. For example:
 1201     pattern HeadC x <- x:xs where
 1202       HeadC x = [x]
 1203       -- This wouldn't compile: {-# INLINE HeadC #-}
 1204     {-# INLINE HeadC #-} -- But this works
 1205 
 1206 When no pragma is provided for a pattern, the inlining decision might change
 1207 between different versions of GHC.
 1208  -}
 1209 
 1210 
 1211 -- Walk the whole pattern and for all ConPatOuts, collect the
 1212 -- existentially-bound type variables and evidence binding variables.
 1213 --
 1214 -- These are used in computing the type of a pattern synonym and also
 1215 -- in generating matcher functions, since success continuations need
 1216 -- to be passed these pattern-bound evidences.
 1217 tcCollectEx
 1218   :: LPat GhcTc
 1219   -> ( [TyVar]        -- Existentially-bound type variables
 1220                       -- in correctly-scoped order; e.g. [ k:*, x:k ]
 1221      , [EvVar] )      -- and evidence variables
 1222 
 1223 tcCollectEx pat = go pat
 1224   where
 1225     go :: LPat GhcTc -> ([TyVar], [EvVar])
 1226     go = go1 . unLoc
 1227 
 1228     go1 :: Pat GhcTc -> ([TyVar], [EvVar])
 1229     go1 (LazyPat _ p)      = go p
 1230     go1 (AsPat _ _ p)      = go p
 1231     go1 (ParPat _ _ p _)   = go p
 1232     go1 (BangPat _ p)      = go p
 1233     go1 (ListPat _ ps)     = mergeMany . map go $ ps
 1234     go1 (TuplePat _ ps _)  = mergeMany . map go $ ps
 1235     go1 (SumPat _ p _ _)   = go p
 1236     go1 (ViewPat _ _ p)    = go p
 1237     go1 con@ConPat{ pat_con_ext = con' }
 1238                            = merge (cpt_tvs con', cpt_dicts con') $
 1239                               goConDetails $ pat_args con
 1240     go1 (SigPat _ p _)     = go p
 1241     go1 (XPat ext) = case ext of
 1242       CoPat _ p _      -> go1 p
 1243       ExpansionPat _ p -> go1 p
 1244     go1 (NPlusKPat _ n k _ geq subtract)
 1245       = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
 1246     go1 _                   = empty
 1247 
 1248     goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
 1249     goConDetails (PrefixCon _ ps) = mergeMany . map go $ ps
 1250     goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
 1251     goConDetails (RecCon HsRecFields{ rec_flds = flds })
 1252       = mergeMany . map goRecFd $ flds
 1253 
 1254     goRecFd :: LHsRecField GhcTc (LPat GhcTc) -> ([TyVar], [EvVar])
 1255     goRecFd (L _ HsFieldBind{ hfbRHS = p }) = go p
 1256 
 1257     merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2)
 1258     mergeMany = foldr merge empty
 1259     empty     = ([], [])