{-# LANGUAGE MultiWayIf          #-}
{-# LANGUAGE RecursiveDo         #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]

{-
%
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
-}

module GHC.Tc.Gen.App
       ( tcApp
       , tcExprPrag ) where

import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )

import GHC.Hs

import GHC.Tc.Gen.Head
import GHC.Tc.Errors.Types
import GHC.Tc.Errors.Ppr
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.Instantiate
import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
import GHC.Tc.Gen.HsType
import GHC.Tc.Utils.Concrete  ( unifyConcrete, idConcreteTvs )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.ErrCtxt ( FunAppCtxtFunArg(..) )
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType as TcType
import GHC.Tc.Zonk.TcType

import GHC.Core.ConLike ( ConLike(..) )
import GHC.Core.DataCon ( dataConConcreteTyVars, isNewDataCon, dataConOrigArgTys )
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst ( substTyWithInScope )
import GHC.Core.Type
import GHC.Core.Coercion

import GHC.Builtin.Types ( multiplicityTy, runtimeRepTy )
import GHC.Builtin.PrimOps( tagToEnumKey )
import GHC.Builtin.Names

import GHC.Types.Var
import GHC.Types.Var.FV
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Types.Name.Reader
import GHC.Types.SrcLoc
import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )

import GHC.Data.Maybe
import GHC.Data.FastString

import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic

import qualified GHC.LanguageExtensions as LangExt

import Control.Monad
import Data.Function
import Data.Semigroup

import GHC.Prelude

{- *********************************************************************
*                                                                      *
                 Quick Look overview
*                                                                      *
********************************************************************* -}

{- Note [Quick Look overview]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The implementation of Quick Look closely follows the QL paper
   A quick look at impredicativity, Serrano et al, ICFP 2020
   https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/

All the moving parts are in this module, GHC.Tc.Gen.App, so named
because it deal with n-ary application.  The main workhorse is tcApp.

Some notes relative to the paper

(QL1) The "instantiation variables" of the paper are ordinary unification
  variables.  We keep track of which variables are instantiation variables
  by giving them a TcLevel of QLInstVar, which is like "infinity".

  See Note [QuickLook instantiation variables] in GHC.Tc.Types.TcType.

(QL2) When we learn what an instantiation variable must be, we simply unify
  it with that type; this is done in qlUnify, which is the function mgu_ql(t1,t2)
  of the paper.  This may fill in a (mutable) instantiation variable with
  a polytype.

(QL3) When QL is done, we turn the instantiation variables into ordinary unification
  variables, using qlZonkTcType.  This function fully zonks the type (thereby
  revealing all the polytypes), and updates any instantiation variables with
  ordinary unification variables. See Note [Instantiation variables are short lived].

(QL4) We cleverly avoid the quadratic cost of QL, alluded to in the paper.
  See Note [Quick Look at value arguments]

Note [Instantiation variables are short lived]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* An instantation variable is a mutable meta-type-variable, whose level number
  is QLInstVar.  See Note [QuickLook instantiation variables] in GHC.Tc.Utils.TcType.

* Ordinary unification variables always stand for monotypes; only instantiation
  variables can be unified with a polytype (by `qlUnify`).

* When we start typechecking the arguments of the call, in tcValArgs, we will
  (a) monomorphise any un-filled-in instantiation variables
      (see Note [Monomorphise instantiation variables]),
  (b) zonk the argument type to reveal any polytypes before typechecking that
      argument (see calls to `zonkTcType` and "Crucial step" in tcValArg).
  See Section 4.3 "Applications and instantiation" of the paper.

  TL;DR: instantiation variables are short-lived. So it is fine for them
         to have an infinite level (=QLInstVar) because they are monomorphised
         before we do anything like skolem-escape checks.

* The constraint solver never sees an instantiation variable
  [not quite true; see below]

  However, the constraint solver can see a meta-type-variable filled
  in with a polytype (#18987). Suppose
    f :: forall a. Dict a => [a] -> [a]
    xs :: [forall b. b->b]
  and consider the call (f xs).  QL will
  * Instantiate f, with a := kappa, where kappa is an instantiation variable
  * Emit a constraint (Dict kappa), via instantiateSigma, called from tcInstFun
  * Do QL on the argument, to discover kappa := forall b. b->b

  But by the time the third step has happened, the constraint has been emitted
  into the monad.  The constraint solver will later find it, and rewrite it to
  (Dict (forall b. b->b)). That's fine -- the constraint solver does no implicit
  instantiation (which is what makes it so tricky to have foralls hiding inside
  unification variables), so there is no difficulty with allowing those
  filled-in kappa's to persist.  (We could find them and zonk them away, but
  that would cost code and execution time, for no purpose.)

  Since the constraint solver does not do implicit instantiation (as the
  constraint generator does), the fact that a unification variable might stand
  for a polytype does not matter.

* Actually, sadly the constraint solver /can/ see an instantiation variable.
  Consider this from test VisFlag1_ql:
     f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()

     bad_wild :: ()
     bad_wild = f @_ MkV
  In tcInstFun instantiate f with [k:=k0, a:=a0], and then encounter the `@_`,
  expecting it to have kind (forall j. j->Type).  We make a fresh variable (it'll
  be an instantiation variable since we are in tcInstFun) for the `_`, thus
  (_ : k0) and do `checkExpectedKind` to match up `k0` with `forall j. j->Type`.
  The unifier doesn't solve it (it does not unify instantiation variables) so
  it leaves it for the constraint solver.  Yuk.   It's hard to see what to do
  about this, but it seems to do no harm for the constraint solver to see the
  occasional instantiation variable.
-}


{- *********************************************************************
*                                                                      *
              Typechecking n-ary applications
*                                                                      *
********************************************************************* -}

{- Note [Application chains and heads]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Quick Look treats application chains specially.  What is an
"application chain"?  See Fig 2, of the QL paper: "A quick look at
impredicativity" (ICFP'20). Here's the syntax:

app ::= head
     |  app expr            -- HsApp: ordinary application
     |  app @type           -- HsTypeApp: VTA
     |  expr `head` expr    -- OpApp: infix applications
     |  ( app )             -- HsPar: parens
     |  {-# PRAGMA #-} app  -- HsPragE: pragmas

head ::= f                -- HsVar:    variables
      |  fld              -- HsRecSel: record field selectors
      |  (expr :: ty)     -- ExprWithTySig: expr with user type sig
      |  lit              -- HsOverLit: overloaded literals

* When tcExpr sees something that starts an application chain (namely,
  any of the constructors in 'head' or in 'app'), it invokes tcApp to
  typecheck it: see Note [tcApp: typechecking applications].  However,
  for HsPar and HsPragE, there is no tcWrapResult (which would
  instantiate types, bypassing Quick Look), so nothing is gained by
  using the application chain route, and we can just recurse to tcExpr.

* If tcExpr sees a constructor belonging to app (except HsPar and HsPargE),
  it does not directly call tcApp, it first splits the expression
  into a maximal application chain using splitHsApps (see `GHC.Tc.Gen.Expr.tcCollectApp`), and obtain
  the head of the application chain and a list of arguments.

* A "head" has three special cases (for which we can infer a polytype
  using tcInferAppHead_maybe); otherwise is just any old expression (for
  which we can infer a rho-type (via runInferExpr).

* There is no special treatment for HsHole (HsVar ...), HsOverLit, etc, because
  we can't get a polytype from them.

* Left and right sections (e.g. (x +) and (+ x)) are not yet supported.
  Probably left sections (x +) would be easy to add, since x is the
  first arg of (+); but right sections are not so easy.  For symmetry
  reasons I've left both unchanged, in GHC.Tc.Gen.Expr.

* It may not be immediately obvious why ExprWithTySig (e::ty) should be
  dealt with by tcApp, even when it is not applied to anything. Consider

      f :: [forall a. a->a] -> Int
      ...(f (undefined :: forall b. b))...

  Clearly this should work!  But it will /only/ work because if we
  instantiate that (forall b. b) impredicatively!  And that only happens
  in tcApp.

Note [tcApp: typechecking applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcApp implements the APP-Downarrow/Uparrow rule of
Fig 3, plus the modification in Fig 5, of the QL paper:
"A quick look at impredicativity" (ICFP'20).

It treats application chains (f e1 @ty e2) specially:

* So we can report errors like "in the third argument of a call of f"

* So we can do Visible Type Application (VTA), for which we must not
  eagerly instantiate the function part of the application.

* So that we can do Quick Look impredicativity.

tcApp accepts 4 arguments:
  1. The original expression
  2. The expression at the head of the application
  3. the argument list (types and terms)
  4. The expected result type

PRECONDITION : the head (2) and the list of arguments (3) will
               are the de-constructred version of the expression (1)
POSTCONDITION: The return expression is the typechecked version of (1)

tcApp works on the application chain by:

1. Using `tcInferAppHead` to infer the type of the function,
     as an (uninstantiated) TcSigmaType
   There are special cases for
     HsVar, HsRecSel, and ExprWithTySig
   Otherwise, delegate back to tcExpr, which
     infers an (instantiated) TcRhoType

   This isn't perfect. Consider this (which uses visible type application):
    (let { f :: forall a. a -> a; f x = x } in f) @Int
   Since 'let' is not among the special cases for tcInferAppHead,
   we'll delegate back to tcExpr, which will instantiate f's type
   and the type application to @Int will fail.  Too bad!

2. Using tcInstFun to instantiate the function, Quick-Looking as we go.  This
   implements the |-inst judgement in Fig 4, plus the modification in Fig 5, of
   the QL paper: "A quick look at impredicativity" (ICFP'20).

   In tcInstFun we take a quick look at value arguments, using quickLookArg.
   See Note [Quick Look at value arguments].

   Crucially, `tcInstFun` ensures that all the unification variables
   it allocates, notably by instantiating the function at the head of the
   application, have level QLInstVar, and hence will be "instantiation
   variables", written using \kappa in the paper.
   See Note [Instantiating type variables in QuickLook]

Now we split into two cases:

3. Case NoQL: no Quick Look

   3.1 Use checkResultTy to connect the the result type.
       Do this /before/ checking the arguments; see
       Note [Unify with expected type before typechecking arguments]

   3.2 Check the arguments with `tcValArgs`.

   3.3 Use `finishApp` to wrap up.

4. Case DoQL: use Quick Look

   4.1 Use `quickLookResultType` to take a quick look at the result type,
       when in checking mode.  This is the shaded part of APP-Downarrow
       in Fig 4.  It also implements the key part of
       Note [Unify with expected type before typechecking arguments]

   4.2 Check the arguments with `tcValArgs`. Importantly, this will
       monomorphise all the instantiation variables of the call.
       See Note [Monomorphise instantiation variables].

   4.3 Use `zonkTcType` to expose the polymophism hidden under instantiation
       variables in `app_res_rho`, and the monomorphic versions of any
       un-unified instantiation variables.

   4.4 Use `checkResTy` to do the subsumption check as usual

   4.5 Use `finishApp` to wrap up

The funcion `finishApp` mainly calls `rebuildHsApps` to rebuild the
application; but it also has a horrile special case for `tagToEnum`.

Note [Quick Look for particular Ids]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We switch on Quick Look (regardless of -XImpredicativeTypes) for certain
particular Ids:

* ($): For a long time GHC has had a special typing rule for ($), that
  allows it to type (runST $ foo), which requires impredicative instantiation
  of ($), without language flags.  It's a bit ad-hoc, but it's been that
  way for ages.  Using quickLookKeys is the only special treatment ($) needs
  now, which is a lot better.

* leftSection, rightSection: these are introduced by the expansion step in
  the renamer (Note [Handling overloaded and rebindable constructs] in
  GHC.Rename.Expr), and we want them to be instantiated impredicatively
  so that (f `op`), say, will work OK even if `f` is higher rank.
  See Note [Left and right sections] in GHC.Rename.Expr.

Note [Unify with expected type before typechecking arguments]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#19364)
  data Pair a b = Pair a b
  baz :: MkPair Int Bool
  baz = MkPair "yes" "no"

We instantiate MkPair with `alpha`, `beta`, and push its argument
types (`alpha` and `beta`) into the arguments ("yes" and "no").
But if we first unify the result type (Pair alpha beta) with the expected
type (Pair Int Bool) we will push the much more informative types
`Int` and `Bool` into the arguments.   This makes a difference:

Unify result type /after/ typechecking the args
    • Couldn't match type ‘[Char]’ with ‘Bool’
      Expected type: Pair Foo Bar
        Actual type: Pair [Char] [Char]
    • In the expression: Pair "yes" "no"

Unify result type /before/ typechecking the args
    • Couldn't match type ‘[Char]’ with ‘Bool’
      Expected: Foo
        Actual: String
    • In the first argument of ‘Pair’, namely ‘"yes"’

The latter is much better. That is why we call `checkResultTy` before tcValArgs.
-}

--------------------
tcApp :: HsExpr GhcRn        -- ^ The whole application (For error messages)
      -> HsExpr GhcRn        -- ^ The Function head
      -> [HsExprArg 'TcpRn]  -- ^ The list of arguments
      -> ExpRhoType          -- ^ When checking, -XDeepSubsumption <=> deeply skolemised
      -> TcM (HsExpr GhcTc)
-- See Note [tcApp: typechecking applications]
-- See Note [splitHsApps] in GHC.Tc.Head
tcApp :: HsExpr GhcRn
-> HsExpr GhcRn
-> [HsExprArg 'TcpRn]
-> ExpType
-> TcM (HsExpr GhcTc)
tcApp HsExpr GhcRn
rn_expr HsExpr GhcRn
rn_fun [HsExprArg 'TcpRn]
rn_args ExpType
exp_res_ty
  = do { fun_lspan <- [HsExprArg 'TcpRn] -> TcM SrcSpan
getFunSrcSpan [HsExprArg 'TcpRn]
rn_args
       ; traceTc "tcApp {" $
           vcat [ text "rn_fun:" <+> ppr rn_fun
                , text "fun_lspan:" <+> ppr fun_lspan
                , text "rn_args:" <+> ppr rn_args ]

       ; let rn_head = (HsExpr GhcRn
rn_fun, SrcSpan
fun_lspan)

       -- Step 1: Infer the type of `fun`, the head of the application
       ; (tc_fun, fun_sigma) <- tcInferAppHead rn_head
       ; let tc_head = (HsExpr GhcTc
tc_fun, SrcSpan
fun_lspan)
             -- inst_final: top-instantiate the result type of the application,
             -- EXCEPT if we are trying to infer a sigma-type
             inst_final = case ExpType
exp_res_ty of
                             Check {} -> Bool
True
                             Infer (IR {ir_inst :: InferResult -> InferInstFlag
ir_inst=InferInstFlag
iif}) ->
                                case InferInstFlag
iif of
                                  InferInstFlag
IIF_ShallowRho -> Bool
True
                                  InferInstFlag
IIF_DeepRho    -> Bool
True
                                  InferInstFlag
IIF_Sigma      -> Bool
False

       -- Step 2: Instantiate the function type (taking a quick look at args)
       -- See Note [Quick Look for particular Ids]
       ; do_ql <- wantQuickLook rn_fun

       ; traceTc "tcApp:inferAppHead" $
         vcat [ text "tc_fun:" <+> ppr tc_fun
              , text "fun_sigma:" <+> ppr fun_sigma
              , text "do_ql:" <+> ppr do_ql]
       ; (inst_args, app_res_rho)
              <- tcInstFun do_ql inst_final rn_head tc_fun fun_sigma rn_args
         -- See (TCAPP1) and (TCAPP2) in
         -- Note [tcApp: typechecking applications]

       ; case do_ql of
            QLFlag
NoQL -> do { String -> SDoc -> TcRn ()
traceTc String
"tcApp:NoQL" (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
app_res_rho)

                         -- Step 3.1: subsumption check against expected result type
                         -- See Note [Unify with expected type before typechecking arguments]
                       ; res_wrap <- HsExpr GhcRn
-> (HsExpr GhcTc, SrcSpan)
-> [HsExprArg 'TcpInst]
-> TcType
-> ExpType
-> TcM HsWrapper
forall (p :: TcPass).
HsExpr GhcRn
-> (HsExpr GhcTc, SrcSpan)
-> [HsExprArg p]
-> TcType
-> ExpType
-> TcM HsWrapper
checkResultTy HsExpr GhcRn
rn_expr (HsExpr GhcTc, SrcSpan)
tc_head [HsExprArg 'TcpInst]
inst_args
                                                   TcType
app_res_rho ExpType
exp_res_ty
                         -- Step 3.2: typecheck the  arguments
                       ; tc_args <- tcValArgs NoQL rn_head inst_args

                         -- Step 3.3: wrap up
                       ; finishApp tc_fun tc_args app_res_rho res_wrap }

            QLFlag
DoQL -> do { String -> SDoc -> TcRn ()
traceTc String
"tcApp:DoQL" (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
app_res_rho)

                         -- Step 4.1: Take a quick look at the result type
                       ; TcType -> ExpType -> TcRn ()
quickLookResultType TcType
app_res_rho ExpType
exp_res_ty

                         -- Step 4.2: typecheck the arguments, and monomorphise
                         --           any un-unified instantiation variables
                       ; tc_args <- QLFlag
-> (HsExpr GhcRn, SrcSpan)
-> [HsExprArg 'TcpInst]
-> TcM [HsExprArg 'TcpTc]
tcValArgs QLFlag
DoQL (HsExpr GhcRn, SrcSpan)
rn_head [HsExprArg 'TcpInst]
inst_args

                         -- Step 4.3: zonk to expose the polymorphism hidden under
                         --           QuickLook instantiation variables in `app_res_rho`
                       ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho

                         -- Step 4.4: subsumption check against the expected type
                       ; res_wrap <- checkResultTy rn_expr tc_head inst_args
                                                    app_res_rho exp_res_ty
                         -- Step 4.5: wrap up
                       ; finishApp tc_fun tc_args app_res_rho res_wrap } }

quickLookResultType :: TcRhoType -> ExpRhoType -> TcM ()
-- This function implements the shaded bit of rule APP-Downarrow in
-- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
quickLookResultType :: TcType -> ExpType -> TcRn ()
quickLookResultType TcType
app_res_rho (Check TcType
exp_rho) = TcType -> TcType -> TcRn ()
qlUnify TcType
app_res_rho TcType
exp_rho
quickLookResultType TcType
_           ExpType
_               = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

finishApp :: HsExpr GhcTc -> [HsExprArg 'TcpTc]
          -> TcRhoType -> HsWrapper
          -> TcM (HsExpr GhcTc)
-- Do final checks and wrap up the result
finishApp :: HsExpr GhcTc
-> [HsExprArg 'TcpTc] -> TcType -> HsWrapper -> TcM (HsExpr GhcTc)
finishApp HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args TcType
app_res_rho HsWrapper
res_wrap
  = do {
       -- Reconstruct, with a horrible special case for tagToEnum#.
         res_expr <- if HsExpr GhcTc -> Bool
isTagToEnum HsExpr GhcTc
tc_fun
                     then HsExpr GhcTc -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args TcType
app_res_rho
                     else HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsExpr GhcTc -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args)
       ; traceTc "End tcApp }" (ppr tc_fun)
       ; return (mkHsWrap res_wrap res_expr) }

-- | Connect up the inferred type of an application with the expected type.
-- This is usually just a unification, but with deep subsumption there is more to do.
checkResultTy :: HsExpr GhcRn
              -> (HsExpr GhcTc, SrcSpan)  -- Head
              -> [HsExprArg p]            -- Arguments, just error messages
              -> TcRhoType  -- Inferred type of the application; zonked to
                            --   expose foralls, but maybe not /deeply/ instantiated
              -> ExpRhoType -- Expected type; this is deeply skolemised
              -> TcM HsWrapper
checkResultTy :: forall (p :: TcPass).
HsExpr GhcRn
-> (HsExpr GhcTc, SrcSpan)
-> [HsExprArg p]
-> TcType
-> ExpType
-> TcM HsWrapper
checkResultTy HsExpr GhcRn
rn_expr (HsExpr GhcTc
tc_fun, SrcSpan
fun_loc) [HsExprArg p]
inst_args TcType
app_res_rho ExpType
res_ty
 = TcM HsWrapper -> TcM HsWrapper
perhaps_add_res_ty_ctxt (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
   HsExpr GhcRn -> HsExpr GhcTc -> TcType -> ExpType -> TcM HsWrapper
tcSubTypeApp HsExpr GhcRn
rn_expr HsExpr GhcTc
tc_fun TcType
app_res_rho ExpType
res_ty
  where
    -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
    -- more confusing than helpful because the function at the head isn't in
    -- the source program; it was added by the renamer.  See
    -- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
    perhaps_add_res_ty_ctxt :: TcM HsWrapper -> TcM HsWrapper
perhaps_add_res_ty_ctxt TcM HsWrapper
thing_inside
      | SrcSpan -> Bool
isGeneratedSrcSpan SrcSpan
fun_loc
      = TcM HsWrapper
thing_inside
      | Bool
otherwise
      = HsExpr GhcTc
-> [HsExprArg p]
-> TcType
-> ExpType
-> TcM HsWrapper
-> TcM HsWrapper
forall (p :: TcPass) a.
HasDebugCallStack =>
HsExpr GhcTc
-> [HsExprArg p] -> TcType -> ExpType -> TcM a -> TcM a
addFunResCtxt HsExpr GhcTc
tc_fun [HsExprArg p]
inst_args TcType
app_res_rho ExpType
res_ty (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
        TcM HsWrapper
thing_inside

----------------
tcValArgs :: QLFlag
          -> (HsExpr GhcRn, SrcSpan) -- Head of the application chain (used only for error message generation)
          -> [HsExprArg 'TcpInst]
          -> TcM [HsExprArg 'TcpTc]
-- Importantly, tcValArgs works left-to-right, so that by the time we
-- encounter an argument, we have monomorphised all the instantiation
-- variables that its type contains.  All that is left to do is an ordinary
-- zonkTcType.  See Note [Monomorphise instantiation variables].
tcValArgs :: QLFlag
-> (HsExpr GhcRn, SrcSpan)
-> [HsExprArg 'TcpInst]
-> TcM [HsExprArg 'TcpTc]
tcValArgs QLFlag
do_ql (HsExpr GhcRn, SrcSpan)
rn_head [HsExprArg 'TcpInst]
args = QLFlag -> Int -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
go QLFlag
do_ql Int
0 [HsExprArg 'TcpInst]
args
  where
    go :: QLFlag -> Int -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
go QLFlag
_ Int
_ [] = [HsExprArg 'TcpTc] -> TcM [HsExprArg 'TcpTc]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    go QLFlag
do_ql Int
pos (HsExprArg 'TcpInst
arg : [HsExprArg 'TcpInst]
args)
      = do { arg'  <- QLFlag
-> Int
-> (HsExpr GhcRn, SrcSpan)
-> HsExprArg 'TcpInst
-> TcM (HsExprArg 'TcpTc)
tcValArg QLFlag
do_ql Int
pos' (HsExpr GhcRn, SrcSpan)
rn_head HsExprArg 'TcpInst
arg
           ; args' <- go do_ql pos' args
           ; return (arg' : args') }
      where
        -- Increment position if the argument is user-written type or value argument
        !pos' :: Int
pos' | HsExprArg 'TcpInst -> Bool
forall {p :: TcPass}. HsExprArg p -> Bool
user_visible HsExprArg 'TcpInst
arg = Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
              | Bool
otherwise        = Int
pos

    user_visible :: HsExprArg p -> Bool
user_visible (EValArg{})                   = Bool
True
    user_visible (EValArgQL{})                 = Bool
True
    user_visible (ETypeArg{ ea_loc_span :: forall (p :: TcPass). HsExprArg p -> SrcSpanAnnA
ea_loc_span = SrcSpanAnnA
l }) = Bool -> Bool
not (SrcSpan -> Bool
isGeneratedSrcSpan (SrcSpanAnnA -> SrcSpan
forall a. HasLoc a => a -> SrcSpan
locA SrcSpanAnnA
l))
    user_visible HsExprArg p
_                             = Bool
False

tcValArg :: QLFlag                  -- ^ Are we typechecking with Quick Look turned on?
         -> Int                     -- ^ Argument position (used only for error message generation)
         -> (HsExpr GhcRn, SrcSpan) -- ^ Head of the application chain (used only for error message generation)
         -> HsExprArg 'TcpInst      -- ^ Actual argument
         -> TcM (HsExprArg 'TcpTc)  -- ^ Resulting argument
tcValArg :: QLFlag
-> Int
-> (HsExpr GhcRn, SrcSpan)
-> HsExprArg 'TcpInst
-> TcM (HsExprArg 'TcpTc)
tcValArg QLFlag
_     Int
_ (HsExpr GhcRn, SrcSpan)
_ (EPrag SrcSpanAnnA
l HsPragE (GhcPass (XPass 'TcpInst))
p)         = HsExprArg 'TcpTc -> TcM (HsExprArg 'TcpTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA -> HsPragE (GhcPass (XPass 'TcpTc)) -> HsExprArg 'TcpTc
forall (p :: TcPass).
SrcSpanAnnA -> HsPragE (GhcPass (XPass p)) -> HsExprArg p
EPrag SrcSpanAnnA
l (HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag HsPragE GhcRn
HsPragE (GhcPass (XPass 'TcpInst))
p))
tcValArg QLFlag
_     Int
_ (HsExpr GhcRn, SrcSpan)
_ (ETypeArg SrcSpanAnnA
l LHsWcType GhcRn
hty XETAType 'TcpInst
ty) = HsExprArg 'TcpTc -> TcM (HsExprArg 'TcpTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> LHsWcType GhcRn -> XETAType 'TcpTc -> HsExprArg 'TcpTc
forall (p :: TcPass).
SrcSpanAnnA -> LHsWcType GhcRn -> XETAType p -> HsExprArg p
ETypeArg SrcSpanAnnA
l LHsWcType GhcRn
hty XETAType 'TcpInst
XETAType 'TcpTc
ty)
tcValArg QLFlag
do_ql Int
_ (HsExpr GhcRn, SrcSpan)
_ (EWrap (EHsWrap HsWrapper
w)) = do { QLFlag -> ZonkM () -> TcRn ()
whenQL QLFlag
do_ql (ZonkM () -> TcRn ()) -> ZonkM () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ HsWrapper -> ZonkM ()
qlMonoHsWrapper HsWrapper
w
                                            ; HsExprArg 'TcpTc -> TcM (HsExprArg 'TcpTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (EWrap -> HsExprArg 'TcpTc
forall (p :: TcPass). EWrap -> HsExprArg p
EWrap (HsWrapper -> EWrap
EHsWrap HsWrapper
w)) }
  -- qlMonoHsWrapper: see Note [Monomorphise instantiation variables]
tcValArg QLFlag
_     Int
_ (HsExpr GhcRn, SrcSpan)
_ (EWrap EWrap
ew)          = HsExprArg 'TcpTc -> TcM (HsExprArg 'TcpTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (EWrap -> HsExprArg 'TcpTc
forall (p :: TcPass). EWrap -> HsExprArg p
EWrap EWrap
ew)

tcValArg QLFlag
do_ql Int
pos (HsExpr GhcRn, SrcSpan)
rn_fun_head (EValArg { ea_loc_span :: forall (p :: TcPass). HsExprArg p -> SrcSpanAnnA
ea_loc_span  = SrcSpanAnnA
lspan
                            , ea_arg :: forall (p :: TcPass). HsExprArg p -> LHsExpr (GhcPass (XPass p))
ea_arg    = larg :: LHsExpr (GhcPass (XPass 'TcpInst))
larg@(L SrcSpanAnnA
arg_loc HsExpr GhcRn
arg)
                            , ea_arg_ty :: forall (p :: TcPass). HsExprArg p -> XEVAType p
ea_arg_ty = XEVAType 'TcpInst
sc_arg_ty })
  = Int
-> (HsExpr GhcRn, SrcSpan)
-> LHsExpr GhcRn
-> TcM (HsExprArg 'TcpTc)
-> TcM (HsExprArg 'TcpTc)
forall a.
Int -> (HsExpr GhcRn, SrcSpan) -> LHsExpr GhcRn -> TcM a -> TcM a
addArgCtxt Int
pos (HsExpr GhcRn, SrcSpan)
rn_fun_head LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpInst))
larg (TcM (HsExprArg 'TcpTc) -> TcM (HsExprArg 'TcpTc))
-> TcM (HsExprArg 'TcpTc) -> TcM (HsExprArg 'TcpTc)
forall a b. (a -> b) -> a -> b
$
    do { -- Crucial step: expose QL results before checking exp_arg_ty
         -- So far as the paper is concerned, this step applies
         -- the poly-substitution Theta, learned by QL, so that we
         -- "see" the polymorphism in that argument type. E.g.
         --    (:) e ids, where ids :: [forall a. a->a]
         --                     (:) :: forall p. p->[p]->[p]
         -- Then Theta = [p :-> forall a. a->a], and we want
         -- to check 'e' with expected type (forall a. a->a)
         -- See Note [Instantiation variables are short lived]
         Scaled mult exp_arg_ty <- case QLFlag
do_ql of
              QLFlag
DoQL -> ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (Scaled TcType)
 -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType))
-> ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a b. (a -> b) -> a -> b
$ Scaled TcType -> ZonkM (Scaled TcType)
zonkScaledTcType Scaled TcType
XEVAType 'TcpInst
sc_arg_ty
              QLFlag
NoQL -> Scaled TcType -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Scaled TcType
XEVAType 'TcpInst
sc_arg_ty
       ; traceTc "tcValArg {" $
         vcat [ text "arg lspan:" <+> ppr lspan
              , text "rn_head" <+> ppr rn_fun_head
              , text "sigma_type" <+> ppr (mkCheckExpType exp_arg_ty)
              , text "arg:" <+> ppr larg
              , text "arg_loc:" <+> ppr arg_loc
              ]


         -- Now check the argument
       ; arg' <- tcScalingUsage mult $
                 tcPolyExpr arg (mkCheckExpType exp_arg_ty)
       ; traceTc "tcValArg" $ vcat [ ppr arg'
                                   , text "}" ]
       ; return (EValArg { ea_loc_span = lspan
                         , ea_arg = L arg_loc arg'
                         , ea_arg_ty = noExtField }) }

tcValArg QLFlag
_ Int
pos (HsExpr GhcRn, SrcSpan)
rn_fun_head (EValArgQL {
                        eaql_wanted :: HsExprArg 'TcpInst -> WantedConstraints
eaql_wanted   = WantedConstraints
wanted
                      , eaql_loc_span :: HsExprArg 'TcpInst -> SrcSpanAnnA
eaql_loc_span = SrcSpanAnnA
lspan
                      , eaql_arg_ty :: HsExprArg 'TcpInst -> Scaled TcType
eaql_arg_ty   = Scaled TcType
sc_arg_ty
                      , eaql_larg :: HsExprArg 'TcpInst -> LHsExpr GhcRn
eaql_larg     = larg :: LHsExpr GhcRn
larg@(L SrcSpanAnnA
arg_loc HsExpr GhcRn
rn_expr)
                      , eaql_tc_fun :: HsExprArg 'TcpInst -> (HsExpr GhcTc, SrcSpan)
eaql_tc_fun   = tc_arg_head :: (HsExpr GhcTc, SrcSpan)
tc_arg_head@(HsExpr GhcTc
tc_fun,SrcSpan
arg_head_loc)
                      , eaql_rn_fun :: HsExprArg 'TcpInst -> HsExpr GhcRn
eaql_rn_fun   = HsExpr GhcRn
rn_arg_head
                      , eaql_fun_ue :: HsExprArg 'TcpInst -> UsageEnv
eaql_fun_ue   = UsageEnv
head_ue
                      , eaql_args :: HsExprArg 'TcpInst -> [HsExprArg 'TcpInst]
eaql_args     = [HsExprArg 'TcpInst]
inst_args
                      , eaql_encl :: HsExprArg 'TcpInst -> Bool
eaql_encl     = Bool
arg_influences_enclosing_call
                      , eaql_res_rho :: HsExprArg 'TcpInst -> TcType
eaql_res_rho  = TcType
app_res_rho })
  = Int
-> (HsExpr GhcRn, SrcSpan)
-> LHsExpr GhcRn
-> TcM (HsExprArg 'TcpTc)
-> TcM (HsExprArg 'TcpTc)
forall a.
Int -> (HsExpr GhcRn, SrcSpan) -> LHsExpr GhcRn -> TcM a -> TcM a
addArgCtxt Int
pos (HsExpr GhcRn, SrcSpan)
rn_fun_head LHsExpr GhcRn
larg (TcM (HsExprArg 'TcpTc) -> TcM (HsExprArg 'TcpTc))
-> TcM (HsExprArg 'TcpTc) -> TcM (HsExprArg 'TcpTc)
forall a b. (a -> b) -> a -> b
$
    do { -- Expose QL results to tcSkolemise, as in EValArg case
         Scaled mult exp_arg_ty <- ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (Scaled TcType)
 -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType))
-> ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a b. (a -> b) -> a -> b
$ Scaled TcType -> ZonkM (Scaled TcType)
zonkScaledTcType Scaled TcType
sc_arg_ty

       ; traceTc "tcEValArgQL {" (vcat [ text "app_res_rho:" <+> ppr app_res_rho
                                       , text "exp_arg_ty:" <+> ppr exp_arg_ty
                                       , text "args:" <+> ppr inst_args
                                       , text "mult:" <+> ppr mult
                                       , text "app_lspan" <+> ppr lspan
                                       , text "fun_head" <+> ppr rn_fun_head
                                       , text "tc_arg_head" <+> ppr tc_arg_head])
       ; ds_flag <- getDeepSubsumptionFlag
         -- NB: whether to do deep /skolemisation/ is independent of data constructors
       ; (wrap, arg')
            <- tcScalingUsage mult  $
               tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ TcType
exp_arg_rho ->
               do { -- Emit saved-up constraints, /under/ the tcSkolemise
                    -- See (QLA4) in Note [Quick Look at value arguments]
                    WantedConstraints -> TcRn ()
emitConstraints WantedConstraints
wanted
                    -- Emit saved-up usages /under/ the tcScalingUsage.
                    -- See (QLA5) in Note [Quick Look at value arguments]
                  ; UsageEnv -> TcRn ()
tcEmitBindingUsage UsageEnv
head_ue

                    -- Unify with context if we have not already done so
                    -- See (QLA4) in Note [Quick Look at value arguments]
                  ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
arg_influences_enclosing_call (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$  -- Don't repeat
                    TcType -> TcType -> TcRn ()
qlUnify TcType
app_res_rho TcType
exp_arg_rho         -- the qlUnify

                  ; tc_args <- QLFlag
-> (HsExpr GhcRn, SrcSpan)
-> [HsExprArg 'TcpInst]
-> TcM [HsExprArg 'TcpTc]
tcValArgs QLFlag
DoQL (HsExpr GhcRn
rn_arg_head, SrcSpan
arg_head_loc) [HsExprArg 'TcpInst]
inst_args
                  ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
                  ; res_wrap <- checkResultTy rn_expr tc_arg_head inst_args
                                              app_res_rho (mkCheckExpType exp_arg_rho)
                  ; finishApp tc_fun tc_args app_res_rho res_wrap }

       ; traceTc "tcEValArgQL }" $
           vcat [ text "app_res_rho:" <+> ppr app_res_rho ]

       ; return (EValArg { ea_loc_span   = lspan
                         , ea_arg    = L arg_loc (mkHsWrap wrap arg')
                         , ea_arg_ty = noExtField }) }


--------------------
wantQuickLook :: HsExpr GhcRn -> TcM QLFlag
wantQuickLook :: HsExpr GhcRn -> TcM QLFlag
wantQuickLook (HsVar XVar GhcRn
_ (L SrcSpanAnnN
_ (WithUserRdr RdrName
_ Name
f)))
  | Name -> Unique
forall a. Uniquable a => a -> Unique
getUnique Name
f Unique -> [Unique] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Unique]
quickLookKeys = QLFlag -> TcM QLFlag
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return QLFlag
DoQL
wantQuickLook HsExpr GhcRn
_                      = do { impred <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
                                          ; if impred then return DoQL else return NoQL }

quickLookKeys :: [Unique]
-- See Note [Quick Look for particular Ids]
quickLookKeys :: [Unique]
quickLookKeys = [Unique
dollarIdKey, Unique
leftSectionKey, Unique
rightSectionKey]

{- *********************************************************************
*                                                                      *
              Instantiating the call
*                                                                      *
********************************************************************* -}

tcInstFun :: QLFlag
          -> Bool   -- False <=> Instantiate only /top-level, inferred/ variables;
                    --           so may return a sigma-type
                    -- True  <=> Instantiate /top-level, invisible/ type variables;
                    --           always return a rho-type (but not a deep-rho type)
                    -- Generally speaking we pass in True; in Fig 5 of the paper
                    --    |-inst returns a rho-type
          -> (HsExpr GhcRn, SrcSpan)
          -> HsExpr GhcTc
          -> TcSigmaType -> [HsExprArg 'TcpRn]
          -> TcM ( [HsExprArg 'TcpInst]
                 , TcSigmaType )   -- Does not instantiate trailing invisible foralls
-- This crucial function implements the |-inst judgement in Fig 4,
-- plus the modification in Fig 5, of the QL paper:
-- "A quick look at impredicativity" (ICFP'20).
tcInstFun :: QLFlag
-> Bool
-> (HsExpr GhcRn, SrcSpan)
-> HsExpr GhcTc
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
tcInstFun QLFlag
do_ql Bool
inst_final rn_head :: (HsExpr GhcRn, SrcSpan)
rn_head@(HsExpr GhcRn
_, SrcSpan
fun_lspan) HsExpr GhcTc
tc_fun TcType
fun_sigma [HsExprArg 'TcpRn]
rn_args
  = do { String -> SDoc -> TcRn ()
traceTc String
"tcInstFun" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tc_fun" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcTc
tc_fun
                                   , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rn_fun" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (HsExpr GhcRn, SrcSpan) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HsExpr GhcRn, SrcSpan)
rn_head
                                   , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"fun_sigma" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
fun_sigma
                                   , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"args:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [HsExprArg 'TcpRn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpRn]
rn_args
                                   , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"do_ql" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> QLFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr QLFlag
do_ql])
       ; fun_origin <- (HsExpr GhcRn, SrcSpan) -> TcM CtOrigin
mk_origin (HsExpr GhcRn, SrcSpan)
rn_head
       ; res@(_, fun_ty) <- go fun_origin 1 [] fun_sigma rn_args
       ; traceTc "tcInstFun:ret" (ppr fun_ty)
       ; return res
       }
  where
    -- What should be the origin for this function call?
    -- If the head of the function is user written
    -- then it can be used in the error message
    -- If it is generated code location span, blame it on the
    -- origin that can be retrived from the top of the error ctxt stack.
    -- See Note [Error contexts in generated code]
    mk_origin :: (HsExpr GhcRn, SrcSpan)  -- The head of the application chain and its location
              -> TcM CtOrigin
    mk_origin :: (HsExpr GhcRn, SrcSpan) -> TcM CtOrigin
mk_origin (HsExpr GhcRn
rn_fun, SrcSpan
fun_lspan)
     | Bool -> Bool
not (SrcSpan -> Bool
isGeneratedSrcSpan SrcSpan
fun_lspan)
     = CtOrigin -> TcM CtOrigin
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtOrigin -> TcM CtOrigin) -> CtOrigin -> TcM CtOrigin
forall a b. (a -> b) -> a -> b
$ HsExpr GhcRn -> CtOrigin
exprCtOrigin HsExpr GhcRn
rn_fun

     | Bool
otherwise -- If the location is generated, the best we can do is to
                 -- approximate by looking on top of the error message stack
     = do { err_ctxt_stack <- TcM ErrCtxtStack
getErrCtxt
          ; let hs_ctxt = case ErrCtxtStack
err_ctxt_stack of
                             (HsCtxt
c:ErrCtxtStack
_) -> HsCtxt
c
                             [] -> String -> SDoc -> HsCtxt
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mk_origin" (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun)
          ; traceTc "mk_origin" (pprHsCtxt hs_ctxt)
          ; return $ hsCtxtCtOrigin hs_ctxt
          }

    -- These are the type variables which must be instantiated to concrete
    -- types. See Note [Representation-polymorphic Ids with no binding]
    -- in GHC.Tc.Utils.Concrete
    fun_conc_tvs :: ConcreteTyVars
fun_conc_tvs
      | HsVar XVar GhcTc
_ (L SrcSpanAnnN
_ Id
fun_id) <- HsExpr GhcTc
tc_fun
      = Id -> ConcreteTyVars
idConcreteTvs Id
fun_id
      -- Recall that DataCons are represented using ConLikeTc at GhcTc stage,
      -- see Note [Typechecking data constructors] in GHC.Tc.Gen.Head.
      | XExpr (ConLikeTc (RealDataCon DataCon
dc)) <- HsExpr GhcTc
tc_fun
      = DataCon -> ConcreteTyVars
dataConConcreteTyVars DataCon
dc
      | Bool
otherwise
      = ConcreteTyVars
noConcreteTyVars

    -- Count value args only when complaining about a function
    -- applied to too many value args
    -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
    n_val_args :: Int
n_val_args = (HsExprArg 'TcpRn -> Bool) -> [HsExprArg 'TcpRn] -> Int
forall a. (a -> Bool) -> [a] -> Int
count HsExprArg 'TcpRn -> Bool
forall {p :: TcPass}. HsExprArg p -> Bool
isHsValArg [HsExprArg 'TcpRn]
rn_args

    fun_is_out_of_scope :: Bool
fun_is_out_of_scope  -- See Note [VTA for out-of-scope functions]
      = case HsExpr GhcTc
tc_fun of
          HsHole XHole GhcTc
_        -> Bool
True
          HsExpr GhcTc
_               -> Bool
False

    inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
    -- True <=> instantiate a tyvar that has this ForAllTyFlag
    inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
inst_fun [] | Bool
inst_final  = ForAllTyFlag -> Bool
isInvisibleForAllTyFlag
                | Bool
otherwise   = Bool -> ForAllTyFlag -> Bool
forall a b. a -> b -> a
const Bool
False
    inst_fun (EValArg {} : [HsExprArg 'TcpRn]
_) = ForAllTyFlag -> Bool
isInvisibleForAllTyFlag
    inst_fun [HsExprArg 'TcpRn]
_                = ForAllTyFlag -> Bool
isInferredForAllTyFlag

    -----------
    go, go1 :: CtOrigin                 -- Of the function
            -> Int                      -- Value-argument position of next arg
            -> [HsExprArg 'TcpInst]     -- Accumulator, reversed
            -> TcSigmaType -> [HsExprArg 'TcpRn]
            -> TcM ([HsExprArg 'TcpInst], TcSigmaType)

    -- go: If fun_ty=kappa, look it up in Theta
    go :: CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty [HsExprArg 'TcpRn]
args
      | Just Id
kappa <- TcType -> Maybe Id
getTyVar_maybe TcType
fun_ty
      , Id -> Bool
isQLInstTyVar Id
kappa
      = do { cts <- Id -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => Id -> m MetaDetails
readMetaTyVar Id
kappa
           ; case cts of
                Indirect TcType
fun_ty' -> CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go  CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty' [HsExprArg 'TcpRn]
args
                MetaDetails
Flexi            -> CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty  [HsExprArg 'TcpRn]
args }
     | Bool
otherwise
     = CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty [HsExprArg 'TcpRn]
args

    -- go1: fun_ty is not filled-in instantiation variable
    --      ('go' dealt with that case)

    -- Handle out-of-scope functions gracefully
    go1 :: CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty (HsExprArg 'TcpRn
arg : [HsExprArg 'TcpRn]
rest_args)
      | Bool
fun_is_out_of_scope, HsExprArg 'TcpRn -> Bool
looks_like_type_arg HsExprArg 'TcpRn
arg   -- See Note [VTA for out-of-scope functions]
      = CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty [HsExprArg 'TcpRn]
rest_args

    -- Rule IALL from Fig 4 of the QL paper; applies even if args = []
    -- Instantiate invisible foralls and dictionaries.
    -- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
    go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty [HsExprArg 'TcpRn]
args
      | ([Id]
tvs,   TcType
body1) <- (ForAllTyFlag -> Bool) -> TcType -> ([Id], TcType)
tcSplitSomeForAllTyVars ([HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
inst_fun [HsExprArg 'TcpRn]
args) TcType
fun_ty
      , (TcThetaType
theta, TcType
body2) <- if [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
inst_fun [HsExprArg 'TcpRn]
args ForAllTyFlag
Inferred
                          then TcType -> (TcThetaType, TcType)
tcSplitPhiTy TcType
body1
                          else ([], TcType
body1)
        -- inst_fun args Inferred: dictionary parameters are like Inferred foralls
        -- E.g. #22908: f :: Foo => blah
        -- No foralls!  But if inst_final=False, don't instantiate
      , let no_tvs :: Bool
no_tvs   = [Id] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
tvs
            no_theta :: Bool
no_theta = TcThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null TcThetaType
theta
      , Bool -> Bool
not (Bool
no_tvs Bool -> Bool -> Bool
&& Bool
no_theta)
      = do { (wrap, fun_rho) <-
                -- setSrcSpan of the function: important for the class constraints
                -- that may be emitted from instantiating fun_sigma
                SrcSpan -> TcRn (HsWrapper, TcType) -> TcRn (HsWrapper, TcType)
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
fun_lspan (TcRn (HsWrapper, TcType) -> TcRn (HsWrapper, TcType))
-> TcRn (HsWrapper, TcType) -> TcRn (HsWrapper, TcType)
forall a b. (a -> b) -> a -> b
$
                QLFlag
-> CtOrigin
-> ConcreteTyVars
-> [Id]
-> TcThetaType
-> TcType
-> TcRn (HsWrapper, TcType)
instantiateSigmaQL QLFlag
do_ql CtOrigin
fun_orig ConcreteTyVars
fun_conc_tvs [Id]
tvs TcThetaType
theta TcType
body2

                  -- See Note [Representation-polymorphism checking built-ins]
                  -- in GHC.Tc.Utils.Concrete.
                  -- NB: we are doing this even when "acc" is not empty,
                  -- to handle e.g.
                  --
                  --   badTup :: forall r (a :: TYPE r). a -> (# Int, a #)
                  --   badTup = (# , #) @LiftedRep
                  --
                  -- in which we already have instantiated the first RuntimeRep
                  -- argument of (#,#) to @LiftedRep, but want to rule out the
                  -- second instantiation @r.

           ; go fun_orig pos (addArgWrap wrap acc) fun_rho args }
                -- Going around again means we deal easily with
                -- nested  forall a. Eq a => forall b. Show b => blah

    -- Rule IRESULT from Fig 4 of the QL paper; no more arguments
    go1 CtOrigin
_fun_orig Int
_pos [HsExprArg 'TcpInst]
acc TcType
fun_ty []
       | XExpr (ConLikeTc (RealDataCon DataCon
dc)) <- HsExpr GhcTc
tc_fun
       , DataCon -> Bool
isNewDataCon DataCon
dc
       , [Scaled TcType
_ TcType
orig_arg_ty] <- DataCon -> [Scaled TcType]
dataConOrigArgTys DataCon
dc
       , Int
n_val_args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
       -- If we're dealing with an unsaturated representation-polymorphic
       -- UnliftedNewype, then perform a representation-polymorphism check.
       -- See Note [Representation-polymorphism checks for unsaturated unlifted newtypes]
       -- in GHC.Tc.Utils.Concrete.
       , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => TcType -> Bool
TcType -> Bool
typeHasFixedRuntimeRep TcType
orig_arg_ty
       = do { (wrap_co, arg_ty, res_ty) <-
                  ExpectedFunTyCtxt
-> Maybe TypedThing
-> (Int, TcType)
-> TcType
-> TcM (TcCoercion, Scaled TcType, TcType)
matchActualFunTy (DataCon -> ExpectedFunTyCtxt
FRRRepPolyUnliftedNewtype DataCon
dc)
                    (TypedThing -> Maybe TypedThing
TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (TypedThing -> Maybe TypedThing) -> TypedThing -> Maybe TypedThing
forall a b. (a -> b) -> a -> b
$ HsExpr GhcTc -> TypedThing
HsExprTcThing HsExpr GhcTc
tc_fun)
                    (Int
n_val_args, TcType
fun_sigma) TcType
fun_ty
             ; let acc' = HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall (p :: TcPass). HsWrapper -> [HsExprArg p] -> [HsExprArg p]
addArgWrap (TcCoercion -> HsWrapper
mkWpCastN TcCoercion
wrap_co) [HsExprArg 'TcpInst]
acc
             ; return (reverse acc', tcMkScaledFunTy arg_ty res_ty) }
      | Bool
otherwise
      = ([HsExprArg 'TcpInst], TcType)
-> TcM ([HsExprArg 'TcpInst], TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. [a] -> [a]
reverse [HsExprArg 'TcpInst]
acc, TcType
fun_ty)

    -- Rule ITVDQ from the GHC Proposal #281
    go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty ((EValArg { ea_arg :: forall (p :: TcPass). HsExprArg p -> LHsExpr (GhcPass (XPass p))
ea_arg = LHsExpr (GhcPass (XPass 'TcpRn))
arg }) : [HsExprArg 'TcpRn]
rest_args)
      | Just (TyVarBinder
tvb, TcType
body) <- TcType -> Maybe (TyVarBinder, TcType)
tcSplitForAllTyVarBinder_maybe TcType
fun_ty
      = Bool
-> SDoc
-> TcM ([HsExprArg 'TcpInst], TcType)
-> TcM ([HsExprArg 'TcpInst], TcType)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVarBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag TyVarBinder
tvb ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ForAllTyFlag
Required) (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
fun_ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ GenLocated SrcSpanAnnA (HsExpr GhcRn) -> SDoc
forall a. Outputable a => a -> SDoc
ppr LHsExpr (GhcPass (XPass 'TcpRn))
GenLocated SrcSpanAnnA (HsExpr GhcRn)
arg) (TcM ([HsExprArg 'TcpInst], TcType)
 -> TcM ([HsExprArg 'TcpInst], TcType))
-> TcM ([HsExprArg 'TcpInst], TcType)
-> TcM ([HsExprArg 'TcpInst], TcType)
forall a b. (a -> b) -> a -> b
$
        -- Any invisible binders have been instantiated by IALL above,
        -- so this forall must be visible (i.e. Required)
        do { (ty_arg, inst_body) <- ConcreteTyVars
-> (TyVarBinder, TcType) -> LHsExpr GhcRn -> TcM (TcType, TcType)
tcVDQ ConcreteTyVars
fun_conc_tvs (TyVarBinder
tvb, TcType
body) LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpRn))
arg
           ; let wrap = TcThetaType -> HsWrapper
mkWpTyApps [TcType
ty_arg]
           ; go fun_orig (pos+1) (addArgWrap wrap acc) inst_body rest_args }

    go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty (EWrap EWrap
w : [HsExprArg 'TcpRn]
args)
      = CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go1 CtOrigin
fun_orig Int
pos (EWrap -> HsExprArg 'TcpInst
forall (p :: TcPass). EWrap -> HsExprArg p
EWrap EWrap
w HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) TcType
fun_ty [HsExprArg 'TcpRn]
args

    go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty (EPrag SrcSpanAnnA
sp HsPragE (GhcPass (XPass 'TcpRn))
prag : [HsExprArg 'TcpRn]
args)
      = CtOrigin
-> Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go1 CtOrigin
fun_orig Int
pos (SrcSpanAnnA
-> HsPragE (GhcPass (XPass 'TcpInst)) -> HsExprArg 'TcpInst
forall (p :: TcPass).
SrcSpanAnnA -> HsPragE (GhcPass (XPass p)) -> HsExprArg p
EPrag SrcSpanAnnA
sp HsPragE (GhcPass (XPass 'TcpRn))
HsPragE (GhcPass (XPass 'TcpInst))
prag HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) TcType
fun_ty [HsExprArg 'TcpRn]
args

    -- Rule ITYARG from Fig 4 of the QL paper
    go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty ( ETypeArg { ea_loc_span :: forall (p :: TcPass). HsExprArg p -> SrcSpanAnnA
ea_loc_span = SrcSpanAnnA
ctxt, ea_hs_ty :: forall (p :: TcPass). HsExprArg p -> LHsWcType GhcRn
ea_hs_ty = LHsWcType GhcRn
hs_ty }
                                  : [HsExprArg 'TcpRn]
rest_args )
      = do { (ty_arg, inst_ty) <- ConcreteTyVars -> TcType -> LHsWcType GhcRn -> TcM (TcType, TcType)
tcVTA ConcreteTyVars
fun_conc_tvs TcType
fun_ty LHsWcType GhcRn
hs_ty
           ; let arg' = ETypeArg { ea_loc_span :: SrcSpanAnnA
ea_loc_span = SrcSpanAnnA
ctxt, ea_hs_ty :: LHsWcType GhcRn
ea_hs_ty = LHsWcType GhcRn
hs_ty, ea_ty_arg :: XETAType 'TcpInst
ea_ty_arg = TcType
XETAType 'TcpInst
ty_arg }
           ; go fun_orig pos (arg' : acc) inst_ty rest_args }

    -- Rule IVAR from Fig 4 of the QL paper:
    go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty args :: [HsExprArg 'TcpRn]
args@(EValArg {} : [HsExprArg 'TcpRn]
_)
      | Just Id
kappa <- TcType -> Maybe Id
getTyVar_maybe TcType
fun_ty
      , Id -> Bool
isQLInstTyVar Id
kappa
      = -- Function type was of form   f :: forall a b. t1 -> t2 -> b
        -- with 'b', one of the quantified type variables, in the corner
        -- but the call applies it to three or more value args.
        -- Suppose b is instantiated by kappa.  Then we want to make fresh
        -- instantiation variables nu1, nu2, and set kappa := nu1 -> nu2
        --
        -- In principle what is happening here is not unlike matchActualFunTys
        -- but there are many small differences:
        --   - We know that the function type in unfilled meta-tyvar
        --     matchActualFunTys is much more general, has a loop, etc.
        --   - We must be sure to actually update the variable right now,
        --     not defer in any way, because this is a QL instantiation variable.
        -- It's easier just to do the job directly here.
        do { arg_tys <- (GenLocated SrcSpanAnnA (HsExpr GhcRn)
 -> Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType))
-> [GenLocated SrcSpanAnnA (HsExpr GhcRn)]
-> [Int]
-> IOEnv (Env TcGblEnv TcLclEnv) [Scaled TcType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (CtOrigin
-> LHsExpr GhcRn
-> Int
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
new_arg_ty CtOrigin
fun_orig) ([HsExprArg 'TcpRn] -> [LHsExpr GhcRn]
leadingValArgs [HsExprArg 'TcpRn]
args) [Int
pos..]
           ; res_ty  <- newOpenFlexiTyVarTyQL do_ql TauTv
           ; let fun_ty' = [Scaled TcType] -> TcType -> TcType
HasDebugCallStack => [Scaled TcType] -> TcType -> TcType
mkScaledFunTys [Scaled TcType]
arg_tys TcType
res_ty

           -- Fill in kappa := nu_1 -> .. -> nu_n -> res_nu
           -- NB: kappa is uninstantiated ('go' already checked that)
           ; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
                 -- unifyKind: see (UQL3) in Note [QuickLook unification]
           ; liftZonkM (writeMetaTyVar kappa (mkCastTy fun_ty' kind_co))

           ; let co_wrap = TcCoercion -> HsWrapper
mkWpCastN (Role -> TcType -> TcCoercion -> TcCoercion
mkGReflLeftCo Role
Nominal TcType
fun_ty' TcCoercion
kind_co)
                 acc'    = HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall (p :: TcPass). HsWrapper -> [HsExprArg p] -> [HsExprArg p]
addArgWrap HsWrapper
co_wrap [HsExprArg 'TcpInst]
acc
                 -- Suppose kappa :: kk
                 -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk
                 --      co_wrap :: (fun_ty' |> kind_co) ~ fun_ty'

           ; go fun_orig pos acc' fun_ty' args }

    -- Rule IARG from Fig 4 of the QL paper:
    go1 CtOrigin
fun_orig Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty
        (EValArg { ea_arg :: forall (p :: TcPass). HsExprArg p -> LHsExpr (GhcPass (XPass p))
ea_arg = LHsExpr (GhcPass (XPass 'TcpRn))
arg, ea_loc_span :: forall (p :: TcPass). HsExprArg p -> SrcSpanAnnA
ea_loc_span = SrcSpanAnnA
ctxt } : [HsExprArg 'TcpRn]
rest_args)
      = do { let herald :: ExpectedFunTyCtxt
herald = CtOrigin -> HsExpr GhcTc -> HsExpr GhcRn -> ExpectedFunTyCtxt
mk_herald CtOrigin
fun_orig HsExpr GhcTc
tc_fun (GenLocated SrcSpanAnnA (HsExpr GhcRn) -> HsExpr GhcRn
forall l e. GenLocated l e -> e
unLoc LHsExpr (GhcPass (XPass 'TcpRn))
GenLocated SrcSpanAnnA (HsExpr GhcRn)
arg)
           ; (fun_co, arg_ty, res_ty) <-
                -- NB: matchActualFunTy does the rep-poly check.
                -- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
                -- In an application (f x), we need 'x' to have a fixed runtime
                -- representation; matchActualFunTy checks that when
                -- taking apart the arrow type (a -> Int).
                --
                -- TODO: example from T26072
                ExpectedFunTyCtxt
-> Maybe TypedThing
-> (Int, TcType)
-> TcType
-> TcM (TcCoercion, Scaled TcType, TcType)
matchActualFunTy ExpectedFunTyCtxt
herald
                  (TypedThing -> Maybe TypedThing
TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (TypedThing -> Maybe TypedThing) -> TypedThing -> Maybe TypedThing
forall a b. (a -> b) -> a -> b
$ HsExpr GhcTc -> TypedThing
HsExprTcThing HsExpr GhcTc
tc_fun)
                  (Int
n_val_args, TcType
fun_sigma) TcType
fun_ty
           ; arg' <- quickLookArg do_ql pos ctxt rn_head arg arg_ty
           ; let acc' = HsExprArg 'TcpInst
arg' HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall (p :: TcPass). HsWrapper -> [HsExprArg p] -> [HsExprArg p]
addArgWrap (TcCoercion -> HsWrapper
mkWpCastN TcCoercion
fun_co) [HsExprArg 'TcpInst]
acc
           ; go fun_orig (pos+1) acc' res_ty rest_args }

    new_arg_ty :: CtOrigin -> LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
    -- Make a fresh nus for each argument in rule IVAR
    new_arg_ty :: CtOrigin
-> LHsExpr GhcRn
-> Int
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
new_arg_ty CtOrigin
fun_orig (L SrcSpanAnnA
_ HsExpr GhcRn
arg) Int
i
      = do { arg_nu <- QLFlag -> FixedRuntimeRepContext -> TcM TcType
newArgTyVarTyQL QLFlag
do_ql (FixedRuntimeRepContext -> TcM TcType)
-> FixedRuntimeRepContext -> TcM TcType
forall a b. (a -> b) -> a -> b
$
                       ExpectedFunTyCtxt -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy (CtOrigin -> HsExpr GhcTc -> HsExpr GhcRn -> ExpectedFunTyCtxt
mk_herald CtOrigin
fun_orig HsExpr GhcTc
tc_fun HsExpr GhcRn
arg) Int
i
               -- Following matchActualFunTy, we create nu_i :: TYPE kappa_i[conc],
               -- thereby ensuring that the arguments have concrete runtime representations

            ; mult_ty <- newFlexiTyVarTyQL do_ql (mkTyVarOccFS (fsLit "m")) TauTv multiplicityTy
               -- mult_ty: e need variables for argument multiplicities (#18731)
               -- Otherwise, 'undefined x' wouldn't be linear in x

           ; return (mkScaled mult_ty arg_nu) }

    mk_herald :: CtOrigin -> HsExpr GhcTc -> HsExpr GhcRn -> ExpectedFunTyCtxt
    mk_herald :: CtOrigin -> HsExpr GhcTc -> HsExpr GhcRn -> ExpectedFunTyCtxt
mk_herald CtOrigin
fun_orig HsExpr GhcTc
tc_fun HsExpr GhcRn
arg
      = case CtOrigin
fun_orig of
           CtOrigin
DoStmtOrigin -> CtOrigin -> HsExpr GhcTc -> ExpectedFunTyCtxt
forall (p :: Pass).
OutputableBndrId p =>
CtOrigin -> HsExpr (GhcPass p) -> ExpectedFunTyCtxt
ExpectedFunTySyntaxOp CtOrigin
DoStmtOrigin HsExpr GhcTc
tc_fun
           CtOrigin
_ -> TypedThing -> HsExpr GhcRn -> ExpectedFunTyCtxt
forall (p :: Pass).
Outputable (HsExpr (GhcPass p)) =>
TypedThing -> HsExpr (GhcPass p) -> ExpectedFunTyCtxt
ExpectedFunTyArg (HsExpr GhcTc -> TypedThing
HsExprTcThing HsExpr GhcTc
tc_fun) HsExpr GhcRn
arg


-- Is the argument supposed to instantiate a forall?
--
-- In other words, given a function application `fn arg`,
-- can we look at the `arg` and conclude that `fn :: forall x. t`
-- or `fn :: forall x -> t`?
--
-- This is a conservative heuristic that returns `False` for "don't know".
-- Used to improve error messages only.
-- See Note [VTA for out-of-scope functions].
looks_like_type_arg :: HsExprArg 'TcpRn -> Bool
looks_like_type_arg :: HsExprArg 'TcpRn -> Bool
looks_like_type_arg ETypeArg{} =
  -- The argument is clearly supposed to instantiate an invisible forall,
  -- i.e. when we see `f @a`, we expect `f :: forall x. t`.
  Bool
True
looks_like_type_arg EValArg{ ea_arg :: forall (p :: TcPass). HsExprArg p -> LHsExpr (GhcPass (XPass p))
ea_arg = L SrcSpanAnnA
_ HsExpr GhcRn
e } =
  -- Check if the argument is supposed to instantiate a visible forall,
  -- i.e. when we see `f (type Int)`, we expect `f :: forall x -> t`,
  --      but not if we see `f True`.
  -- We can't say for sure though. Part 2 of GHC Proposal #281 allows
  -- type arguments without the `type` qualifier, so `f True` could
  -- instantiate `forall (b :: Bool) -> t`.
  case HsExpr GhcRn -> HsExpr GhcRn
forall (p :: Pass). HsExpr (GhcPass p) -> HsExpr (GhcPass p)
stripParensHsExpr HsExpr GhcRn
e of
    HsEmbTy XEmbTy GhcRn
_ LHsWcType (NoGhcTc GhcRn)
_ -> Bool
True
    HsExpr GhcRn
_           -> Bool
False
looks_like_type_arg HsExprArg 'TcpRn
_ = Bool
False

addArgCtxt :: Int -> (HsExpr GhcRn, SrcSpan) -> LHsExpr GhcRn
           -> TcM a -> TcM a
-- There are 2 cases:
-- 1. In the normal case, we add an informative context
--     (<=> location span of f or head of application chain is user located)
--     "In the third argument of f, namely blah"
-- 2. If head of the application chain is generated
--    "In the expression: arg"

--  See Note [Rebindable syntax and XXExprGhcRn] in GHC.Hs.Expr
--  See Note [Expanding HsDo with XXExprGhcRn] in GHC.Tc.Gen.Do
addArgCtxt :: forall a.
Int -> (HsExpr GhcRn, SrcSpan) -> LHsExpr GhcRn -> TcM a -> TcM a
addArgCtxt Int
arg_no (HsExpr GhcRn
app_head, SrcSpan
app_head_lspan) (L SrcSpanAnnA
arg_loc HsExpr GhcRn
arg) TcM a
thing_inside
  | Bool -> Bool
not (SrcSpan -> Bool
isGeneratedSrcSpan SrcSpan
app_head_lspan)
  = do { String -> SDoc -> TcRn ()
traceTc String
"addArgCtxt" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"not generated Head"
                                    , HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
app_head
                                    , SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
app_head_lspan
                                    , SrcSpanAnnA -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpanAnnA
arg_loc
                                    , HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
arg
                                    , Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
arg_no])
       ; SrcSpanAnnA -> TcM a -> TcM a
forall ann a. EpAnn ann -> TcRn a -> TcRn a
setSrcSpanA SrcSpanAnnA
arg_loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
         HsCtxt -> TcM a -> TcM a
forall a. HsCtxt -> TcM a -> TcM a
addErrCtxt (FunAppCtxtFunArg -> Int -> HsCtxt
FunAppCtxt (HsExpr GhcRn -> HsExpr GhcRn -> FunAppCtxtFunArg
FunAppCtxtExpr HsExpr GhcRn
app_head HsExpr GhcRn
arg) Int
arg_no) (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
         TcM a
thing_inside
       }
  | Bool
otherwise
  = do { String -> SDoc -> TcRn ()
traceTc String
"addArgCtxt" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"generated Head"
                                    , HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
app_head
                                    , SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
app_head_lspan
                                    , SrcSpanAnnA -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpanAnnA
arg_loc
                                    , HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
arg])
       ; SrcSpanAnnA -> TcM a -> TcM a
forall ann a. EpAnn ann -> TcRn a -> TcRn a
setSrcSpanA SrcSpanAnnA
arg_loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
         HsExpr GhcRn -> TcM a -> TcM a
forall a. HsExpr GhcRn -> TcRn a -> TcRn a
addExprCtxt HsExpr GhcRn
arg (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
         TcM a
thing_inside
       }


{- *********************************************************************
*                                                                      *
              Instantiating fresh type variables

      Functions in here use getTcLevelQL to decide what level
      to put on fresh unification variables.  If do_ql = DoQL, we
      ignore the level in the monad, and use QLInstVar instead,
      thereby giving birth to a Quick Look instantiation varaible
*                                                                      *
********************************************************************* -}

{- Note [Instantiating type variables in QuickLook]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During QuickLook, when we instantiate a function's type (specifically, in
`tcInstFun`), we must instantiate it with so-called "instantiation variables".
See Note [QuickLook instantiation variables] in GHC.Tc.Utils.TcType.

So `tcInstFun` uses a family of specialised functions, defined below, like
   instantiateSigmaQL
   newFlexiTyVarTyQL
   etc
that create fresh instantiation variables rather than regular unification
variables.   But only if QuickLook is on!  So they all take a `QLFlag` to
tell them what to do; that flag is ultimately used in `getTcLevelQL`.

There is some code duplication between these functions and their friends
in GHC.Tc.Utils.TcMType, but that's just too bad.

Note that `tcInstFun` calls `quickLookArg` which calls `tcInstFun` recursively.
Consider (f (g (h x))).`tcApp` instantiates the call to `f`, and in doing so
quick-looks at the argument(s), in this case (g (h x)).  But `quickLookArg` on (g
(h x)) in turn instantiates `g` and quick-looks at /its/ argument(s), in this
case (h x).  And so on recursively.  Key point: all these instantiations make
instantiation variables.
-}

getTcLevelQL :: QLFlag -> TcM TcLevel
-- If Quick Look is on, instantiate all fresh unification variables
-- at level QLInstVar; they are instantiation variables
-- See Note [Instantiating type variables in QuickLook]
getTcLevelQL :: QLFlag -> TcM TcLevel
getTcLevelQL QLFlag
DoQL = TcLevel -> TcM TcLevel
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcLevel
QLInstVar
getTcLevelQL QLFlag
NoQL = TcM TcLevel
getTcLevel

newFlexiTyVarQL :: QLFlag -> OccName -> MetaInfo -> TcKind -> TcM TcTyVar
newFlexiTyVarQL :: QLFlag -> OccName -> MetaInfo -> TcType -> TcM Id
newFlexiTyVarQL QLFlag
do_ql OccName
occ MetaInfo
info TcType
kind
  = do { lvl  <- QLFlag -> TcM TcLevel
getTcLevelQL QLFlag
do_ql
       ; ref  <- newMutVar Flexi
       ; name <- newSysName occ -- See Note [Name of a unification variable]
                                -- in GHC.Tc.Utils.TcMType
       ; let details = MetaTv { mtv_info :: MetaInfo
mtv_info  = MetaInfo
info
                              , mtv_ref :: IORef MetaDetails
mtv_ref   = IORef MetaDetails
ref
                              , mtv_tclvl :: TcLevel
mtv_tclvl = TcLevel
lvl }
       ; return (mkTcTyVar name kind details) }

newFlexiTyVarTyQL :: QLFlag -> OccName -> MetaInfo -> TcKind -> TcM TcType
newFlexiTyVarTyQL :: QLFlag -> OccName -> MetaInfo -> TcType -> TcM TcType
newFlexiTyVarTyQL QLFlag
do_ql OccName
occ MetaInfo
info TcType
kind
  = Id -> TcType
mkTyVarTy (Id -> TcType) -> TcM Id -> TcM TcType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QLFlag -> OccName -> MetaInfo -> TcType -> TcM Id
newFlexiTyVarQL QLFlag
do_ql OccName
occ MetaInfo
info TcType
kind

newOpenFlexiTyVarTyQL :: QLFlag -> MetaInfo -> TcM TcType
newOpenFlexiTyVarTyQL :: QLFlag -> MetaInfo -> TcM TcType
newOpenFlexiTyVarTyQL QLFlag
do_ql MetaInfo
rr_info
  = do { let rr_occ :: OccName
rr_occ = FastString -> OccName
mkTyVarOccFS (String -> FastString
fsLit String
"cx")
             tv_occ :: OccName
tv_occ = FastString -> OccName
mkTyVarOccFS (String -> FastString
fsLit String
"q")
        ; rr_ty  <- QLFlag -> OccName -> MetaInfo -> TcType -> TcM TcType
newFlexiTyVarTyQL QLFlag
do_ql OccName
rr_occ MetaInfo
rr_info TcType
runtimeRepTy
        ; arg_nu <- newFlexiTyVarTyQL do_ql tv_occ TauTv   (mkTYPEapp rr_ty)
        ; return arg_nu }

newArgTyVarTyQL :: QLFlag -> FixedRuntimeRepContext -> TcM TcType
newArgTyVarTyQL :: QLFlag -> FixedRuntimeRepContext -> TcM TcType
newArgTyVarTyQL QLFlag
do_ql FixedRuntimeRepContext
frr_ctxt
  = mdo { let conc_orig = FixedRuntimeRepOrigin -> ConcreteTvOrigin
FixedRuntimeRepOrigin -> ConcreteTvOrigin
ConcreteFRR (FixedRuntimeRepOrigin -> ConcreteTvOrigin)
-> FixedRuntimeRepOrigin -> ConcreteTvOrigin
forall a b. (a -> b) -> a -> b
$
                          FixedRuntimeRepOrigin
                            { frr_context :: FixedRuntimeRepContext
frr_context = FixedRuntimeRepContext
frr_ctxt
                            , frr_type :: TcType
frr_type    = TcType
arg_nu }
        ; rr_info <- mkConcreteInfo conc_orig
        ; arg_nu  <- newOpenFlexiTyVarTyQL do_ql rr_info
        ; return arg_nu }

instantiateSigmaQL :: QLFlag
                   -> CtOrigin
                   -> ConcreteTyVars -- ^ concreteness information
                   -> [TyVar]
                   -> TcThetaType -> TcSigmaType
                   -> TcM (HsWrapper, TcSigmaType)
-- (instantiateSigmaQL orig tvs theta ty)
--     instantiates the type variables tvs, emits the (instantiated)
--     constraints theta, and returns the (instantiated) type ty
-- See Note [Instantiating type variables in QuickLook]
instantiateSigmaQL :: QLFlag
-> CtOrigin
-> ConcreteTyVars
-> [Id]
-> TcThetaType
-> TcType
-> TcRn (HsWrapper, TcType)
instantiateSigmaQL QLFlag
do_ql CtOrigin
orig ConcreteTyVars
concs [Id]
tvs TcThetaType
theta TcType
body_ty
  = do { rec (subst, inst_tvs) <- mapAccumLM (new_meta subst) empty_subst tvs
       ; let inst_theta  = HasDebugCallStack => Subst -> TcThetaType -> TcThetaType
Subst -> TcThetaType -> TcThetaType
substTheta Subst
subst TcThetaType
theta
             inst_body   = HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst TcType
body_ty

       ; wrap <- instCall orig (mkTyVarTys inst_tvs) inst_theta
       ; traceTc "Instantiating"
                 (vcat [ text "origin" <+> pprCtOrigin orig
                       , text "tvs"   <+> ppr tvs
                       , text "theta" <+> ppr theta
                       , text "type" <+> debugPprType body_ty
                       , text "with" <+> ppr inst_tvs
                       , text "theta:" <+> ppr inst_theta ])

      ; return (wrap, inst_body) }
  where
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (TcType -> VarSet
tyCoVarsOfType ([Id] -> TcThetaType -> TcType -> TcType
HasDebugCallStack => [Id] -> TcThetaType -> TcType -> TcType
mkSpecSigmaTy [Id]
tvs TcThetaType
theta TcType
body_ty))
               -- mkSpecSigmaTy: Inferred vs Specified is not important here;
               --                We just want an accurate free-var set
    empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope

    new_meta :: Subst -> Subst -> TyVar -> TcM (Subst, TcTyVar)
    new_meta :: Subst -> Subst -> Id -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, Id)
new_meta Subst
final_subst Subst
subst Id
tv
      = do { let occ :: OccName
occ = Id -> OccName
forall a. NamedThing a => a -> OccName
getOccName Id
tv
                 substd_kind :: TcType
substd_kind = HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst (Id -> TcType
tyVarKind Id
tv)
           ; info   <- Subst -> Id -> TcM MetaInfo
get_info Subst
final_subst Id
tv
           ; new_tv <- newFlexiTyVarQL do_ql occ info substd_kind
           ; let new_subst   = Subst -> Id -> Id -> Subst
extendTvSubstWithClone Subst
subst Id
tv Id
new_tv
           ; return (new_subst, new_tv) }

    get_info :: Subst -> TyVar -> TcM MetaInfo
    get_info :: Subst -> Id -> TcM MetaInfo
get_info Subst
final_subst Id
tv
      -- Is this a type variable that must be instantiated to a concrete type?
      -- If so, create a ConcreteTv metavariable instead of a plain TauTv.
      -- See Note [Representation-polymorphism checking built-ins]
      --     in GHC.Tc.Utils.Concrete.

      | Just ConcreteTvOrigin
conc_orig0 <- ConcreteTyVars -> Name -> Maybe ConcreteTvOrigin
forall a. NameEnv a -> Name -> Maybe a
lookupNameEnv ConcreteTyVars
concs (Id -> Name
tyVarName Id
tv)
      , let conc_orig :: ConcreteTvOrigin
conc_orig = Subst -> TcType -> ConcreteTvOrigin -> ConcreteTvOrigin
substConcreteTvOrigin Subst
final_subst TcType
body_ty ConcreteTvOrigin
conc_orig0
                        -- See Note [substConcreteTvOrigin].
      = ConcreteTvOrigin -> TcM MetaInfo
mkConcreteInfo ConcreteTvOrigin
conc_orig

      -- The vastly common case
      | Bool
otherwise
      = MetaInfo -> TcM MetaInfo
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return MetaInfo
TauTv

{- *********************************************************************
*                                                                      *
              Visible type application
*                                                                      *
********************************************************************* -}

-- See Note [Visible type application and abstraction]
tcVTA :: ConcreteTyVars
         -- ^ Type variables that must be instantiated to concrete types.
         --
         -- See Note [Representation-polymorphism checking built-ins]
         -- in GHC.Tc.Utils.Concrete.
      -> TcType            -- ^ Function type
      -> LHsWcType GhcRn   -- ^ Argument type
      -> TcM (TcType, TcType)
-- Deal with a visible type application
-- The function type has already had its Inferred binders instantiated
tcVTA :: ConcreteTyVars -> TcType -> LHsWcType GhcRn -> TcM (TcType, TcType)
tcVTA ConcreteTyVars
conc_tvs TcType
fun_ty LHsWcType GhcRn
hs_ty
  | Just (TyVarBinder
tvb, TcType
inner_ty) <- TcType -> Maybe (TyVarBinder, TcType)
tcSplitForAllTyVarBinder_maybe TcType
fun_ty
  , TyVarBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag TyVarBinder
tvb ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ForAllTyFlag
Specified
  = do { ConcreteTyVars
-> (TyVarBinder, TcType) -> LHsWcType GhcRn -> TcM (TcType, TcType)
tc_inst_forall_arg ConcreteTyVars
conc_tvs (TyVarBinder
tvb, TcType
inner_ty) LHsWcType GhcRn
hs_ty }

  | Bool
otherwise
  = do { (_, fun_ty) <- ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType))
-> ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType)
forall a b. (a -> b) -> a -> b
$ TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
emptyTidyEnv TcType
fun_ty
       ; failWith $ TcRnInvalidTypeApplication fun_ty hs_ty }

-- See Note [Visible type application and abstraction]
tcVDQ :: ConcreteTyVars              -- See Note [Representation-polymorphism checking built-ins]
      -> (ForAllTyBinder, TcType)    -- Function type
      -> LHsExpr GhcRn               -- Argument type
      -> TcM (TcType, TcType)
tcVDQ :: ConcreteTyVars
-> (TyVarBinder, TcType) -> LHsExpr GhcRn -> TcM (TcType, TcType)
tcVDQ ConcreteTyVars
conc_tvs (TyVarBinder
tvb, TcType
inner_ty) LHsExpr GhcRn
arg
  = do { hs_wc_ty <- LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
expr_to_type LHsExpr GhcRn
arg
       ; tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_wc_ty }

-- Convert a HsExpr into the equivalent HsType.
-- See [RequiredTypeArguments and the T2T mapping]
expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
expr_to_type LHsExpr GhcRn
earg =
  case LHsExpr GhcRn -> LHsExpr GhcRn
forall (p :: Pass). LHsExpr (GhcPass p) -> LHsExpr (GhcPass p)
stripParensLHsExpr LHsExpr GhcRn
earg of
    L SrcSpanAnnA
_ (HsEmbTy XEmbTy GhcRn
_ LHsWcType (NoGhcTc GhcRn)
hs_ty) ->
      -- The entire type argument is guarded with the `type` herald,
      -- e.g. `vfun (type (Maybe Int))`. This special case supports
      -- named wildcards. See Note [Wildcards in the T2T translation]
      HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return LHsWcType (NoGhcTc GhcRn)
HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn))
hs_ty
    LHsExpr GhcRn
e ->
      -- The type argument is not guarded with the `type` herald, or perhaps
      -- only parts of it are, e.g. `vfun (Maybe Int)` or `vfun (Maybe (type Int))`.
      -- Apply a recursive T2T transformation.
      XHsWC GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn))
-> GenLocated SrcSpanAnnA (HsType GhcRn)
-> HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn))
forall pass thing.
XHsWC pass thing -> thing -> HsWildCardBndrs pass thing
HsWC [] (GenLocated SrcSpanAnnA (HsType GhcRn)
 -> HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn)))
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
e
        IOEnv
  (Env TcGblEnv TcLclEnv)
  (HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn)))
-> TcRn ()
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn)))
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
-> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* TcRn ()
failIfErrsM   -- Suppress unhelpful errors that arise after a failed T2T
  where
    go :: LHsExpr GhcRn -> TcM (LHsType GhcRn)
    go :: LHsExpr GhcRn -> TcM (LHsType GhcRn)
go (L SrcSpanAnnA
_ (HsEmbTy XEmbTy GhcRn
_ LHsWcType (NoGhcTc GhcRn)
t)) =
      -- HsEmbTy means there is an explicit `type` herald, e.g. vfun :: forall a -> blah
      -- and the call   vfun (type Int)
      --           or   vfun (Int -> type Int)
      -- The T2T transformation can simply discard the herald and use the embedded type.
      HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn))
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall t. HsWildCardBndrs GhcRn t -> TcM t
unwrap_wc LHsWcType (NoGhcTc GhcRn)
HsWildCardBndrs GhcRn (GenLocated SrcSpanAnnA (HsType GhcRn))
t
    go (L SrcSpanAnnA
l (HsFunArr XFunArr GhcRn
_ HsModifiedFunArrOf (LHsExpr GhcRn) GhcRn
mult LHsExpr GhcRn
arg LHsExpr GhcRn
res)) =
      do { arg' <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
arg
         ; mult' <- go_arrow
         ; res' <- go res
         ; return (L l (HsFunTy noExtField mult' arg' res'))}
         where
          go_arrow :: IOEnv
  (Env TcGblEnv TcLclEnv)
  (HsModifiedFunArrOf (GenLocated SrcSpanAnnA (HsType GhcRn)) GhcRn)
go_arrow = do
            let HsModifiedFunArr XHsModifiedFunArr (LHsExpr GhcRn) GhcRn
_ [LHsModifierOf (LHsExpr GhcRn) GhcRn]
mods HsFunArr GhcRn
arr = HsModifiedFunArrOf (LHsExpr GhcRn) GhcRn
mult
            mods' <- (GenLocated
   SrcSpanAnnA
   (HsModifierOf (GenLocated SrcSpanAnnA (HsExpr GhcRn)) GhcRn)
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (GenLocated
         SrcSpanAnnA
         (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) GhcRn)))
-> [GenLocated
      SrcSpanAnnA
      (HsModifierOf (GenLocated SrcSpanAnnA (HsExpr GhcRn)) GhcRn)]
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     [GenLocated
        SrcSpanAnnA
        (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) GhcRn)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM GenLocated
  SrcSpanAnnA
  (HsModifierOf (GenLocated SrcSpanAnnA (HsExpr GhcRn)) GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated
        SrcSpanAnnA
        (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) GhcRn))
forall {pass} {pass} {l}.
(XModifier pass ~ XModifier pass) =>
GenLocated
  l (HsModifierOf (GenLocated SrcSpanAnnA (HsExpr GhcRn)) pass)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated
        l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass))
go_modifier [LHsModifierOf (LHsExpr GhcRn) GhcRn]
[GenLocated
   SrcSpanAnnA
   (HsModifierOf (GenLocated SrcSpanAnnA (HsExpr GhcRn)) GhcRn)]
mods
            pure $ HsModifiedFunArr noExtField mods' arr
          go_modifier :: GenLocated
  l (HsModifierOf (GenLocated SrcSpanAnnA (HsExpr GhcRn)) pass)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated
        l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass))
go_modifier (L l
l (HsModifier XModifier pass
x GenLocated SrcSpanAnnA (HsExpr GhcRn)
ty)) = l
-> HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass
-> GenLocated
     l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass)
forall l e. l -> e -> GenLocated l e
L l
l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass
 -> GenLocated
      l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass))
-> (GenLocated SrcSpanAnnA (HsType GhcRn)
    -> HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass)
-> GenLocated SrcSpanAnnA (HsType GhcRn)
-> GenLocated
     l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> XModifier pass
-> GenLocated SrcSpanAnnA (HsType GhcRn)
-> HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass
forall ty pass. XModifier pass -> ty -> HsModifierOf ty pass
HsModifier XModifier pass
XModifier pass
x (GenLocated SrcSpanAnnA (HsType GhcRn)
 -> GenLocated
      l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass))
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated
        l (HsModifierOf (GenLocated SrcSpanAnnA (HsType GhcRn)) pass))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
GenLocated SrcSpanAnnA (HsExpr GhcRn)
ty
    go (L SrcSpanAnnA
l (HsForAll XForAll GhcRn
_ HsForAllTelescope GhcRn
tele LHsExpr GhcRn
expr)) =
      do { ty <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
expr
         ; return (L l (HsForAllTy noExtField tele ty))}
    go (L SrcSpanAnnA
l (HsQual XQual GhcRn
_ (L SrcSpanAnnC
ann [GenLocated SrcSpanAnnA (HsExpr GhcRn)]
ctxt) LHsExpr GhcRn
expr)) =
      do { ctxt' <- (GenLocated SrcSpanAnnA (HsExpr GhcRn)
 -> IOEnv
      (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn)))
-> [GenLocated SrcSpanAnnA (HsExpr GhcRn)]
-> IOEnv
     (Env TcGblEnv TcLclEnv) [GenLocated SrcSpanAnnA (HsType GhcRn)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM LHsExpr GhcRn -> TcM (LHsType GhcRn)
GenLocated SrcSpanAnnA (HsExpr GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
go [GenLocated SrcSpanAnnA (HsExpr GhcRn)]
ctxt
         ; ty <- go expr
         ; return (L l (HsQualTy noExtField (L ann ctxt') ty)) }
    go (L SrcSpanAnnA
l (HsVar XVar GhcRn
_ LIdOccP GhcRn
lname)) =
      -- GHC Proposal #281, section 7.5 "T2T-Mapping":
      --   variables and constructors (regardless of their namespace)
      --   are mapped directly, without modification.
      do { GenLocated SrcSpanAnnN (WithUserRdr Name) -> TcRn ()
detect_puns LIdOccP GhcRn
GenLocated SrcSpanAnnN (WithUserRdr Name)
lname
         ; GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType GhcRn -> GenLocated SrcSpanAnnA (HsType GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XTyVar GhcRn -> PromotionFlag -> LIdOccP GhcRn -> HsType GhcRn
forall pass.
XTyVar pass -> PromotionFlag -> LIdOccP pass -> HsType pass
HsTyVar XTyVar GhcRn
EpToken "'"
forall a. NoAnn a => a
noAnn PromotionFlag
NotPromoted LIdOccP GhcRn
lname)) }
    go (L SrcSpanAnnA
l (HsApp XApp GhcRn
_ LHsExpr GhcRn
lhs LHsExpr GhcRn
rhs)) =
      do { lhs' <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
lhs
         ; rhs' <- go rhs
         ; return (L l (HsAppTy noExtField lhs' rhs')) }
    go (L SrcSpanAnnA
l (HsAppType XAppTypeE GhcRn
_ LHsExpr GhcRn
lhs LHsWcType (NoGhcTc GhcRn)
rhs)) =
      do { lhs' <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
lhs
         ; rhs' <- unwrap_wc rhs
         ; return (L l (HsAppKindTy noExtField lhs' rhs')) }
    go (L SrcSpanAnnA
l (OpApp XOpApp GhcRn
_ LHsExpr GhcRn
lhs LHsExpr GhcRn
op LHsExpr GhcRn
rhs)) =
      do { lhs' <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
lhs
         ; op'  <- go op
         ; rhs' <- go rhs
         ; return (L l (HsOpTy noExtField lhs' op' rhs')) }
    go (L SrcSpanAnnA
l (HsOverLit XOverLitE GhcRn
_ HsOverLit GhcRn
ol))
      = do { let lit :: HsLit GhcRn
lit = OverLitVal -> HsLit GhcRn
tyLitFromOverloadedLit (HsOverLit GhcRn -> OverLitVal
forall p. HsOverLit p -> OverLitVal
ol_val HsOverLit GhcRn
ol)
           ; GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType GhcRn -> GenLocated SrcSpanAnnA (HsType GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XTyLit GhcRn -> HsLit GhcRn -> HsType GhcRn
forall pass. XTyLit pass -> HsLit pass -> HsType pass
HsTyLit XTyLit GhcRn
NoExtField
noExtField HsLit GhcRn
lit)) }
    go (L SrcSpanAnnA
l (HsLit XLitE GhcRn
_ HsLit GhcRn
lit))
      = GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType GhcRn -> GenLocated SrcSpanAnnA (HsType GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XTyLit GhcRn -> HsLit GhcRn -> HsType GhcRn
forall pass. XTyLit pass -> HsLit pass -> HsType pass
HsTyLit XTyLit GhcRn
NoExtField
noExtField HsLit GhcRn
lit))
    go (L SrcSpanAnnA
l (ExplicitTuple XExplicitTuple GhcRn
_ [HsTupArg GhcRn]
tup_args Boxity
boxity))
      -- Neither unboxed tuples (#e1,e2#) nor tuple sections (e1,,e2,) can be promoted
      | Boxity -> Bool
isBoxed Boxity
boxity
      , Just [LHsExpr GhcRn]
es <- [HsTupArg GhcRn] -> Maybe [LHsExpr GhcRn]
forall (p :: Pass).
[HsTupArg (GhcPass p)] -> Maybe [LHsExpr (GhcPass p)]
tupArgsPresent_maybe [HsTupArg GhcRn]
tup_args
      = do { ts <- (GenLocated SrcSpanAnnA (HsExpr GhcRn)
 -> IOEnv
      (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn)))
-> [GenLocated SrcSpanAnnA (HsExpr GhcRn)]
-> IOEnv
     (Env TcGblEnv TcLclEnv) [GenLocated SrcSpanAnnA (HsType GhcRn)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse LHsExpr GhcRn -> TcM (LHsType GhcRn)
GenLocated SrcSpanAnnA (HsExpr GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
go [LHsExpr GhcRn]
[GenLocated SrcSpanAnnA (HsExpr GhcRn)]
es
           ; return (L l (HsExplicitTupleTy noExtField NotPromoted ts)) }
    go (L SrcSpanAnnA
l (ExplicitList XExplicitList GhcRn
_ [LHsExpr GhcRn]
es)) =
      do { ts <- (GenLocated SrcSpanAnnA (HsExpr GhcRn)
 -> IOEnv
      (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn)))
-> [GenLocated SrcSpanAnnA (HsExpr GhcRn)]
-> IOEnv
     (Env TcGblEnv TcLclEnv) [GenLocated SrcSpanAnnA (HsType GhcRn)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse LHsExpr GhcRn -> TcM (LHsType GhcRn)
GenLocated SrcSpanAnnA (HsExpr GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
go [LHsExpr GhcRn]
[GenLocated SrcSpanAnnA (HsExpr GhcRn)]
es
         ; return (L l (HsExplicitListTy noExtField NotPromoted ts)) }
    go (L SrcSpanAnnA
l (ExprWithTySig XExprWithTySig GhcRn
_ LHsExpr GhcRn
e LHsSigWcType (NoGhcTc GhcRn)
sig_ty)) =
      do { t <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
e
         ; sig_ki <- (unwrap_sig <=< unwrap_wc) sig_ty
         ; return (L l (HsKindSig noAnn t sig_ki)) }
      where
        unwrap_sig :: LHsSigType GhcRn -> TcM (LHsType GhcRn)
        unwrap_sig :: LHsSigType GhcRn -> TcM (LHsType GhcRn)
unwrap_sig (L SrcSpanAnnA
_ (HsSig XHsSig GhcRn
_ HsOuterImplicit{hso_ximplicit :: forall flag pass.
HsOuterTyVarBndrs flag pass -> XHsOuterImplicit pass
hso_ximplicit=XHsOuterImplicit GhcRn
bndrs} LHsType GhcRn
body))
          | [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
XHsOuterImplicit GhcRn
bndrs = GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return LHsType GhcRn
GenLocated SrcSpanAnnA (HsType GhcRn)
body
          | Bool
otherwise  = [Name]
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall t. [Name] -> TcM t
illegal_implicit_tvs [Name]
XHsOuterImplicit GhcRn
bndrs
        unwrap_sig (L SrcSpanAnnA
l (HsSig XHsSig GhcRn
_ HsOuterExplicit{hso_bndrs :: forall flag pass.
HsOuterTyVarBndrs flag pass -> [LHsTyVarBndr flag (NoGhcTc pass)]
hso_bndrs=[LHsTyVarBndr Specificity (NoGhcTc GhcRn)]
bndrs} LHsType GhcRn
body)) =
          GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (GenLocated SrcSpanAnnA (HsType GhcRn)
 -> IOEnv
      (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn)))
-> GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a b. (a -> b) -> a -> b
$ SrcSpanAnnA
-> HsType GhcRn -> GenLocated SrcSpanAnnA (HsType GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XForAllTy GhcRn
-> HsForAllTelescope GhcRn -> LHsType GhcRn -> HsType GhcRn
forall pass.
XForAllTy pass
-> HsForAllTelescope pass -> LHsType pass -> HsType pass
HsForAllTy XForAllTy GhcRn
NoExtField
noExtField (XHsForAllInvis GhcRn
-> [LHsTyVarBndr Specificity GhcRn] -> HsForAllTelescope GhcRn
forall pass.
XHsForAllInvis pass
-> [LHsTyVarBndr Specificity pass] -> HsForAllTelescope pass
HsForAllInvis XHsForAllInvis GhcRn
forall a. NoAnn a => a
noAnn [LHsTyVarBndr Specificity (NoGhcTc GhcRn)]
[LHsTyVarBndr Specificity GhcRn]
bndrs) LHsType GhcRn
body)
    go (L SrcSpanAnnA
l (HsPar XPar GhcRn
_ LHsExpr GhcRn
e)) =
      do { t <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go LHsExpr GhcRn
e
         ; return (L l (HsParTy noAnn t)) }
    go (L SrcSpanAnnA
l (HsUntypedSplice XUntypedSplice GhcRn
splice_result HsUntypedSplice GhcRn
splice))
      | HsUntypedSpliceTop ThModFinalizers
finalizers HsExpr GhcRn
e <- XUntypedSplice GhcRn
splice_result
      = do { t <- LHsExpr GhcRn -> TcM (LHsType GhcRn)
go (SrcSpanAnnA
-> HsExpr GhcRn -> GenLocated SrcSpanAnnA (HsExpr GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l HsExpr GhcRn
e)
           ; let splice_result' = ThModFinalizers
-> GenLocated SrcSpanAnnA (HsType GhcRn)
-> HsUntypedSpliceResult (GenLocated SrcSpanAnnA (HsType GhcRn))
forall thing.
ThModFinalizers -> thing -> HsUntypedSpliceResult thing
HsUntypedSpliceTop ThModFinalizers
finalizers GenLocated SrcSpanAnnA (HsType GhcRn)
t
           ; return (L l (HsSpliceTy splice_result' splice)) }
    go (L SrcSpanAnnA
l (HsStar XStar GhcRn
x))
      = GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType GhcRn -> GenLocated SrcSpanAnnA (HsType GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XStarTy GhcRn -> HsType GhcRn
forall pass. XStarTy pass -> HsType pass
HsStarTy XStarTy GhcRn
XStar GhcRn
x))
    go (L SrcSpanAnnA
l (HsHole (HoleVar (L SrcSpanAnnN
_ RdrName
rdr))))
      | OccName -> Bool
isUnderscore OccName
occ = GenLocated SrcSpanAnnA (HsType GhcRn)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType GhcRn -> GenLocated SrcSpanAnnA (HsType GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XWildCardTy GhcRn -> HsType GhcRn
forall pass. XWildCardTy pass -> HsType pass
HsWildCardTy XWildCardTy GhcRn
NoExtField
noExtField))
      | OccName -> Bool
startsWithUnderscore OccName
occ =
          -- See Note [Wildcards in the T2T translation]
          do { wildcards_enabled <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.NamedWildCards
             ; if wildcards_enabled
               then illegal_wc rdr
               else not_in_scope }
      | Bool
otherwise = TcM (LHsType GhcRn)
IOEnv
  (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
not_in_scope
      where occ :: OccName
occ = RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName RdrName
rdr
            not_in_scope :: IOEnv
  (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
not_in_scope = TcRnMessage
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a. TcRnMessage -> TcRn a
failWith (TcRnMessage
 -> IOEnv
      (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn)))
-> TcRnMessage
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (HsType GhcRn))
forall a b. (a -> b) -> a -> b
$ NotInScopeError -> RdrName -> TcRnMessage
TcRnNotInScope NotInScopeError
NotInScope RdrName
rdr
    go (L SrcSpanAnnA
l (XExpr (ExpandedThingRn (HSE (ExprCtxt HsExpr GhcRn
orig) LHsExpr GhcRn
_)))) =
      -- Use the original, user-written expression (before expansion).
      -- Example. Say we have   vfun :: forall a -> blah
      --          and the call  vfun (Maybe [1,2,3])
      --          expanded to   vfun (Maybe (fromListN 3 [1,2,3]))
      -- (This happens when OverloadedLists is enabled).
      -- The expanded expression can't be promoted, as there is no type-level
      -- equivalent of fromListN, so we must use the original.
      LHsExpr GhcRn -> TcM (LHsType GhcRn)
go (SrcSpanAnnA
-> HsExpr GhcRn -> GenLocated SrcSpanAnnA (HsExpr GhcRn)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l HsExpr GhcRn
orig)
    go LHsExpr GhcRn
e = TcRnMessage -> TcM (LHsType GhcRn)
forall a. TcRnMessage -> TcRn a
failWith (TcRnMessage -> TcM (LHsType GhcRn))
-> TcRnMessage -> TcM (LHsType GhcRn)
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcRn -> TcRnMessage
TcRnIllformedTypeArgument LHsExpr GhcRn
e

    detect_puns :: LocatedN (WithUserRdr Name) -> TcM ()
      -- GHC Proposal #281, section 7.5 "T2T-Mapping":
      --   there should be no variable of the same name but from
      --   a different namespace, or else raise an ambiguity error
      --   (does not apply to constructors)
    detect_puns :: GenLocated SrcSpanAnnN (WithUserRdr Name) -> TcRn ()
detect_puns (L SrcSpanAnnN
l (WithUserRdr RdrName
rdr Name
_))
      | NameSpace -> Bool
isTermVarOrFieldNameSpace (RdrName -> NameSpace
rdrNameSpace RdrName
rdr)
      , Just RdrName
promoted_rdr <- RdrName -> Maybe RdrName
promoteRdrName RdrName
rdr
      = do { envs <- TcRn (GlobalRdrEnv, LocalRdrEnv)
getRdrEnvs
           ; whenIsJust (lookup_rdr envs rdr) $ \ResolvedNameInfo
unpromoted ->
             Maybe ResolvedNameInfo -> (ResolvedNameInfo -> TcRn ()) -> TcRn ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenIsJust ((GlobalRdrEnv, LocalRdrEnv) -> RdrName -> Maybe ResolvedNameInfo
lookup_rdr (GlobalRdrEnv, LocalRdrEnv)
envs RdrName
promoted_rdr) ((ResolvedNameInfo -> TcRn ()) -> TcRn ())
-> (ResolvedNameInfo -> TcRn ()) -> TcRn ()
forall a b. (a -> b) -> a -> b
$ \ResolvedNameInfo
promoted ->
               SrcSpan -> TcRnMessage -> TcRn ()
addErrAt (SrcSpanAnnN -> SrcSpan
forall a. HasLoc a => a -> SrcSpan
locA SrcSpanAnnN
l) (TcRnMessage -> TcRn ()) -> TcRnMessage -> TcRn ()
forall a b. (a -> b) -> a -> b
$
               TcRnIllegalPunnedVarOccInTypeArgument { illegalPunTermName :: ResolvedNameInfo
illegalPunTermName = ResolvedNameInfo
unpromoted
                                                     , illegalPunTypeName :: ResolvedNameInfo
illegalPunTypeName = ResolvedNameInfo
promoted } }
      | Bool
otherwise = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    lookup_rdr :: (GlobalRdrEnv, LocalRdrEnv) -> RdrName -> Maybe ResolvedNameInfo
    lookup_rdr :: (GlobalRdrEnv, LocalRdrEnv) -> RdrName -> Maybe ResolvedNameInfo
lookup_rdr (GlobalRdrEnv
gbl_env, LocalRdrEnv
lcl_env) RdrName
rdr
      | Just Name
name <- LocalRdrEnv -> RdrName -> Maybe Name
lookupLocalRdrEnv LocalRdrEnv
lcl_env RdrName
rdr
      = ResolvedNameInfo -> Maybe ResolvedNameInfo
forall a. a -> Maybe a
Just ([GlobalRdrElt] -> RdrName -> Name -> ResolvedNameInfo
ResolvedNameInfo [] RdrName
rdr Name
name)
      | gres :: [GlobalRdrElt]
gres@(GlobalRdrElt
gre:[GlobalRdrElt]
_) <- GlobalRdrEnv -> LookupGRE GREInfo -> [GlobalRdrElt]
forall info.
GlobalRdrEnvX info -> LookupGRE info -> [GlobalRdrEltX info]
lookupGRE GlobalRdrEnv
gbl_env (RdrName -> WhichGREs GREInfo -> LookupGRE GREInfo
forall info. RdrName -> WhichGREs info -> LookupGRE info
LookupRdrName RdrName
rdr (FieldsOrSelectors -> WhichGREs GREInfo
RelevantGREsFOS FieldsOrSelectors
WantNormal))
      = ResolvedNameInfo -> Maybe ResolvedNameInfo
forall a. a -> Maybe a
Just ([GlobalRdrElt] -> RdrName -> Name -> ResolvedNameInfo
ResolvedNameInfo [GlobalRdrElt]
gres RdrName
rdr (GlobalRdrElt -> Name
forall info. GlobalRdrEltX info -> Name
gre_name GlobalRdrElt
gre))
      | Bool
otherwise = Maybe ResolvedNameInfo
forall a. Maybe a
Nothing

    unwrap_wc :: HsWildCardBndrs GhcRn t -> TcM t
    unwrap_wc :: forall t. HsWildCardBndrs GhcRn t -> TcM t
unwrap_wc (HsWC XHsWC GhcRn t
wcs t
t)
      = do { (Name -> IOEnv (Env TcGblEnv TcLclEnv) b_0) -> [Name] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (RdrName -> IOEnv (Env TcGblEnv TcLclEnv) b_0
forall t. RdrName -> TcM t
illegal_wc (RdrName -> IOEnv (Env TcGblEnv TcLclEnv) b_0)
-> (Name -> RdrName) -> Name -> IOEnv (Env TcGblEnv TcLclEnv) b_0
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RdrName
nameRdrName) [Name]
XHsWC GhcRn t
wcs
           ; t -> IOEnv (Env TcGblEnv TcLclEnv) t
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return t
t }

    illegal_wc :: RdrName -> TcM t
    illegal_wc :: forall t. RdrName -> TcM t
illegal_wc RdrName
rdr = TcRnMessage -> TcRn t
forall a. TcRnMessage -> TcRn a
failWith (TcRnMessage -> TcRn t) -> TcRnMessage -> TcRn t
forall a b. (a -> b) -> a -> b
$ RdrName -> TcRnMessage
TcRnIllegalNamedWildcardInTypeArgument RdrName
rdr

    illegal_implicit_tvs :: [Name] -> TcM t
    illegal_implicit_tvs :: forall t. [Name] -> TcM t
illegal_implicit_tvs [Name]
tvs
      = do { (Name -> TcRn ()) -> [Name] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TcRnMessage -> TcRn ()
addErr (TcRnMessage -> TcRn ())
-> (Name -> TcRnMessage) -> Name -> TcRn ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RdrName -> TcRnMessage
RdrName -> TcRnMessage
TcRnIllegalImplicitTyVarInTypeArgument (RdrName -> TcRnMessage)
-> (Name -> RdrName) -> Name -> TcRnMessage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RdrName
nameRdrName) [Name]
tvs
           ; IOEnv (Env TcGblEnv TcLclEnv) t
failM }

{- Note [RequiredTypeArguments and the T2T mapping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "T2T-Mapping" section of GHC Proposal #281 introduces a term-to-type transformation
that comes into play when we typecheck function applications to required type arguments.
Say we have a function that expects a required type argument, vfun :: forall a -> ...
then it is possible to call it as follows:

  vfun (Maybe Int)

The Maybe Int argument is parsed and renamed as a term. There is no syntactic marker
to tell GHC that it is actually a type argument.  We only discover this by the time
we get to type checking, where we know that f's type has a visible forall at the front,
so we are expecting a type argument. More precisely, this happens in tcVDQ in GHC/Tc/Gen/App.hs:

  tcVDQ :: ConcreteTyVars              -- See Note [Representation-polymorphism checking built-ins]
        -> (ForAllTyBinder, TcType)    -- Function type
        -> LHsExpr GhcRn               -- Argument type
        -> TcM (TcType, TcType)

What we want is a type to instantiate the forall-bound variable. But what we have is an HsExpr,
and we need to convert it to an HsType in order to reuse the same code paths as we use for
checking f @ty (see tc_inst_forall_arg).

  f (Maybe Int)
  -- ^^^^^^^^^
  -- parsed and renamed as:   HsApp   (HsVar   "Maybe") (HsVar   "Int")  ::  HsExpr GhcRn
  -- must be converted to:    HsTyApp (HsTyVar "Maybe") (HsTyVar "Int")  ::  HsType GhcRn

We do this using a helper function:

  expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)

This conversion is in the TcM monad because
* It can fail, if the expression is not convertible to a type.
      vfun [x | x <- xs]     Can't convert list comprehension to a type
      vfun (\x -> x)         Can't convert a lambda to a type
* It needs to check for LangExt.NamedWildCards to generate an appropriate
  error message for HsHole (HsVar ...).
     vfun _a    Not in scope: ‘_a’
                   (NamedWildCards disabled)
     vfun _a    Illegal named wildcard in a required type argument: ‘_a’
                   (NamedWildCards enabled)

Note [Wildcards in the T2T translation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose f1 :: forall a b. blah
        f2 :: forall a b -> blah

Consider the terms
  f1 @_ @(Either _ _)
  f2 (type _) (type (Either _ _))
Those `_` wildcards are type wildcards, each standing for a monotype.
All good.

Now consider this, with -XNamedWildCards:
  f1 @_a @(Either _a _a)
  f2 (type _a) (type (Either _a _a))
Those `_a` are "named wildcards", specified by the user manual like this: "All
occurrences of the same named wildcard within one type signature will unify to
the same type".  Note "within one signature".  So each type argument is considered
separately, and the examples mean the same as:
  f1 @_a1 @(Either _a2 _a2)
  f2 (type _a1) (type (Either _a2 _a2))
The repeated `_a2` ensures that the two arguments of `Either` are the same type;
but there is no connection with `_a1`.  (NB: `_a1` and `_a2` only scope within
their respective type, no further.)

Now, consider the T2T translation for
   f2 _ (Either _ _)
This is fine: the term wildcard `_` is translated to a type wildcard, so we get
the same as if we had written
   f2 (type _) (type (Either _ _))

But what about /named/ wildcards?
   f2 _a (Either _a _a)
Now we are in difficulties.  The renamer looks for a /term/ variable `_a` in scope,
and won't find one.  Even if it did, the three `_a`'s would not be renamed separately
as above.

Conclusion: we treat a named wildcard in the T2T translation as an error.  If you
want that, use a `(type ty)` argument instead.
-}

tc_inst_forall_arg :: ConcreteTyVars            -- See Note [Representation-polymorphism checking built-ins]
                   -> (ForAllTyBinder, TcType)  -- Function type
                   -> LHsWcType GhcRn           -- Argument type
                   -> TcM (TcType, TcType)
tc_inst_forall_arg :: ConcreteTyVars
-> (TyVarBinder, TcType) -> LHsWcType GhcRn -> TcM (TcType, TcType)
tc_inst_forall_arg ConcreteTyVars
conc_tvs (TyVarBinder
tvb, TcType
inner_ty) LHsWcType GhcRn
hs_ty
  = do { let tv :: Id
tv   = TyVarBinder -> Id
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
tvb
             kind :: TcType
kind = Id -> TcType
tyVarKind Id
tv
             tv_nm :: Name
tv_nm   = Id -> Name
tyVarName Id
tv
             mb_conc :: Maybe ConcreteTvOrigin
mb_conc = ConcreteTyVars -> Name -> Maybe ConcreteTvOrigin
forall a. NameEnv a -> Name -> Maybe a
lookupNameEnv ConcreteTyVars
conc_tvs Name
tv_nm
       ; ty_arg0 <- LHsWcType GhcRn -> TcType -> TcM TcType
tcHsTypeApp LHsWcType GhcRn
hs_ty TcType
kind

       -- Is this type variable required to be instantiated to a concrete type?
       -- If so, ensure that that is the case.
       --
       -- See [Wrinkle: VTA] in Note [Representation-polymorphism checking built-ins]
       -- in GHC.Tc.Utils.Concrete.
       ; th_lvl <- getThLevel
       ; ty_arg <- case mb_conc of
           Maybe ConcreteTvOrigin
Nothing   -> TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
ty_arg0
           Just ConcreteTvOrigin
conc
             -- See [Wrinkle: Typed Template Haskell]
             -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
             | TypedBrack {} <- ThLevel
th_lvl
             -> TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
ty_arg0
             | Bool
otherwise
             ->
             -- Example: user wrote e.g. (#,#) @(F Bool) for a type family F.
             -- Emit [W] F Bool ~ kappa[conc] and pretend the user wrote (#,#) @kappa.
               HasDebugCallStack => TcCoercion -> TcType
TcCoercion -> TcType
coercionRKind (TcCoercion -> TcType) -> TcM TcCoercion -> TcM TcType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FastString -> ConcreteTvOrigin -> TcType -> TcM TcCoercion
unifyConcrete (OccName -> FastString
occNameFS (OccName -> FastString) -> OccName -> FastString
forall a b. (a -> b) -> a -> b
$ Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName (Name -> OccName) -> Name -> OccName
forall a b. (a -> b) -> a -> b
$ Name
tv_nm) ConcreteTvOrigin
conc TcType
ty_arg0

       ; let fun_ty    = TyVarBinder -> TcType -> TcType
mkForAllTy TyVarBinder
tvb TcType
inner_ty
             in_scope  = VarSet -> InScopeSet
mkInScopeSet (TcThetaType -> VarSet
tyCoVarsOfTypes [TcType
fun_ty, TcType
ty_arg])
             insted_ty = HasDebugCallStack =>
InScopeSet -> [Id] -> TcThetaType -> TcType -> TcType
InScopeSet -> [Id] -> TcThetaType -> TcType -> TcType
substTyWithInScope InScopeSet
in_scope [Id
tv] [TcType
ty_arg] TcType
inner_ty
               -- This substitution is well-kinded even when inner_ty
               -- is not fully zonked, because ty_arg is fully zonked.
               -- See Note [Type application substitution].

       ; traceTc "tc_inst_forall_arg (VTA/VDQ)" (
                  vcat [ text "fun_ty" <+> ppr fun_ty
                       , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind
                       , text "ty_arg" <+> debugPprType ty_arg <+> dcolon
                                       <+> debugPprType (typeKind ty_arg)
                       , text "inner_ty" <+> debugPprType inner_ty
                       , text "insted_ty" <+> debugPprType insted_ty ])
       ; return (ty_arg, insted_ty) }

{- Note [Visible type application and abstraction]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC supports the types
    forall {a}.  a -> t     -- ForAllTyFlag is Inferred
    forall  a.   a -> t     -- ForAllTyFlag is Specified
    forall  a -> a -> t     -- ForAllTyFlag is Required

The design of type abstraction and type application for those types has gradually
evolved over time, and is based on the following papers and proposals:
  - "Visible Type Application"
    https://richarde.dev/papers/2016/type-app/visible-type-app.pdf
  - "Type Variables in Patterns"
    https://richarde.dev/papers/2018/pat-tyvars/pat-tyvars.pdf
  - "Modern Scoped Type Variables"
    https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst
  - "Visible forall in types of terms"
    https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst

Here we offer an overview of the design mixed with commentary on the
implementation status. The proposals have not been fully implemented at the
time of writing this Note (see "not implemented" in the rest of this Note).

Now consider functions
    fi :: forall {a}. a -> t     -- Inferred:  type argument cannot be supplied
    fs :: forall a. a -> t       -- Specified: type argument may    be supplied
    fr :: forall a -> a -> t     -- Required:  type argument must   be supplied

At a call site we may have calls looking like this
    fi             True  -- Inferred: no visible type argument
    fs             True  -- Specified: type argument omitted
    fs      @Bool  True  -- Specified: type argument supplied
    fr (type Bool) True  -- Required: type argument is compulsory, `type` qualifier used
    fr       Bool  True  -- Required: type argument is compulsory, `type` qualifier omitted

At definition sites we may have type /patterns/ to abstract over type variables
   fi           x       = rhs   -- Inferred: no type pattern
   fs           x       = rhs   -- Specified: type pattern omitted
   fs @a       (x :: a) = rhs   -- Specified: type pattern supplied
   fr (type a) (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier used
   fr a        (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier omitted

Type patterns in lambdas mostly work the same way as they do in a function LHS,
except for @-binders
   OK:  fs = \           x       -> rhs   -- Specified: type pattern omitted
   Bad: fs = \ @a       (x :: a) -> rhs   -- Specified: type pattern supplied
   OK:  fr = \ (type a) (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier used
   OK:  fr = \ a        (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier omitted

When it comes to @-binders in lambdas, they do work, but only in a limited set
of circumstances:
  * the lambda occurs as an argument to a higher-rank function or constructor
      higher-rank function:  h :: (forall a. blah) -> ...
      call site:             x = h (\ @a -> ... )
  * the lambda is annotated with an inline type signature:
      (\ @a -> ... ) :: forall a. blah
  * the lambda is a field in a data structure, whose type is impredicative
      [ \ @a -> ... ] :: [forall a. blah]
  * the @-binder is not the first binder in the lambda:
      \ x @a -> ...

Type patterns may also occur in a constructor pattern. Consider the following data declaration
   data T where
     MkTI :: forall {a}. Show a => a -> T   -- Inferred
     MkTS :: forall a.   Show a => a -> T   -- Specified
     MkTR :: forall a -> Show a => a -> T   -- Required  (NB: not implemented)

Matching on its constructors may look like this
   f (MkTI           x)       = rhs  -- Inferred: no type pattern
   f (MkTS           x)       = rhs  -- Specified: type pattern omitted
   f (MkTS @a       (x :: a)) = rhs  -- Specified: type pattern supplied
   f (MkTR (type a) (x :: a)) = rhs  -- Required: type pattern is compulsory, `type` qualifier used    (NB: not implemented)
   f (MkTR a        (x :: a)) = rhs  -- Required: type pattern is compulsory, `type` qualifier omitted (NB: not implemented)

The moving parts are as follows:
  (abbreviations used: "c.o." = "constructor of")

Syntax of types
---------------
* The types are all initially represented with HsForAllTy (c.o. HsType).
  The binders are in the (hst_tele :: HsForAllTelescope pass) field of the HsForAllTy
  At this stage, we have
      forall {a}. t    -- HsForAllInvis (c.o. HsForAllTelescope) and InferredSpec  (c.o. Specificity)
      forall a. t      -- HsForAllInvis (c.o. HsForAllTelescope) and SpecifiedSpec (c.o. Specificity)
      forall a -> t    -- HsForAllVis (c.o. HsForAllTelescope)

* By the time we get to checking applications/abstractions (e.g. GHC.Tc.Gen.App)
  the types have been kind-checked (e.g. by tcLHsType) into ForAllTy (c.o. Type).
  At this stage, we have:
      forall {a}. t    -- ForAllTy (c.o. Type) and Inferred  (c.o. ForAllTyFlag)
      forall a. t      -- ForAllTy (c.o. Type) and Specified (c.o. ForAllTyFlag)
      forall a -> t    -- ForAllTy (c.o. Type) and Required  (c.o. ForAllTyFlag)

Syntax of applications in HsExpr
--------------------------------
* We represent type applications in HsExpr like this (ignoring parameterisation)
    data HsExpr = HsApp HsExpr HsExpr      -- (f True)    (plain function application)
                | HsAppType HsExpr HsType  -- (f @True)   (function application with `@`)
                | HsEmbTy HsType           -- (type Int)  (embed a type into an expression with `type`)
                | ...

* So (f @ty) is represented, just as you might expect:
    HsAppType f ty

* But (f (type ty)) is represented by:
    HsApp f (HsEmbTy ty)

  Why the difference?  Because we /also/ need to express these /nested/ uses of `type`:

      g (Maybe (type Int))               -- valid for g :: forall (a :: Type) -> t
      g (Either (type Int) (type Bool))  -- valid for g :: forall (a :: Type) -> t

  This nesting makes `type` rather different from `@`. Remember, the HsEmbTy mainly just
  switches namespace, and is subject to the term-to-type transformation.

Syntax of abstractions in Pat
-----------------------------
* Type patterns are represented in Pat roughly like this
     data Pat = ConPat   ConLike [Pat]  -- (Con @tp1 @tp2 p1 p2)  (constructor pattern)
              | EmbTyPat HsTyPat        -- (type tp)              (embed a type into a pattern with `type`)
              | InvisPat HsTyPat        -- (@tp)                  (invisible type pattern)
              | ...
     data HsTyPat = HsTP LHsType
  (In ConPat, the type and term arguments are actually inside HsConPatDetails.)

  * Similar to HsAppType in HsExpr, InvisPat in ConPat is used for @ty arguments
  * Similar to HsEmbTy   in HsExpr, EmbTyPat lets you embed a type in a pattern

* Examples:
      \ (MkT @a  (x :: a)) -> rhs    -- ConPat (c.o. Pat) and InvisPat (c.o. Pat)
      \ (type a) (x :: a)  -> rhs    -- EmbTyPat (c.o. Pat)
      \ a        (x :: a)  -> rhs    -- VarPat (c.o. Pat)
      \ @a       (x :: a)  -> rhs    -- InvisPat (c.o. Pat)

* A HsTyPat is not necessarily a plain variable. At the very least,
  we support kind signatures and wildcards:
      \ (type _)           -> rhs
      \ (type (b :: Bool)) -> rhs
      \ (type (_ :: Bool)) -> rhs
  But in constructor patterns we also support full-on types
      \ (P @(a -> Either b c)) -> rhs
  All these forms are represented with HsTP (c.o. HsTyPat).

Renaming type applications
--------------------------
rnExpr delegates renaming of type arguments to rnHsWcType if possible:
    f @t        -- HsAppType,         t is renamed with rnHsWcType
    f (type t)  -- HsApp and HsEmbTy, t is renamed with rnHsWcType

But what about:
    f t         -- HsApp, no HsEmbTy
We simply rename `t` as a term using a recursive call to rnExpr; in particular,
the type of `f` does not affect name resolution (Lexical Scoping Principle).
We will later convert `t` from a `HsExpr` to a `Type`, see "Typechecking type
applications" later in this Note. The details are spelled out in the "Resolved
Syntax Tree" and "T2T-Mapping" sections of GHC Proposal #281.

Renaming type abstractions
--------------------------
rnPat delegates renaming of type arguments to rnHsTyPat if possible:
  f (P @t)   = rhs  -- ConPat,   t is renamed with rnHsTyPat
  f (type t) = rhs  -- EmbTyPat, t is renamed with rnHsTyPat

But what about:
  f t = rhs   -- VarPat
The solution is as before (see previous section), mutatis mutandis.
Rename `t` as a pattern using a recursive call to `rnPat`, convert it
to a type pattern later.

One particularly prickly issue is that of implicit quantification. Consider:

  f :: forall a -> ...
  f t = ...   -- binding site of `t`
    where
      g :: t -> t   -- use site of `t` or a fresh variable?
      g = ...

Does the signature of `g` refer to `t` bound in `f`, or is it a fresh,
implicitly quantified variable? This is normally controlled by
ScopedTypeVariables, but in this example the renamer can't tell `t` from a term
variable.  Only later (in the type checker) will we find out that it stands for
the forall-bound type variable `a`.  So when RequiredTypeArguments is in effect,
we change implicit quantification to take term variables into account; that is,
we do not implicitly quantify the signature of `g` to `g :: forall t. t->t`
because of the term-level `t` that is in scope.
See Note [Term variable capture and implicit quantification].

Typechecking type applications
------------------------------
Type applications are checked alongside ordinary function applications
in tcInstFun.

First of all, we assume that the function type is known (i.e. not a metavariable)
and contains a `forall`. Consider:
  f :: forall a. a -> a
  f x = const x (f @Int 5)
If the type signature is removed, the definition results in an error:
  Cannot apply expression of type ‘t1’
  to a visible type argument ‘Int’

The same principle applies to required type arguments:
  f :: forall a -> a -> a
  f (type a) x = const x (f (type Int) 5)
If the type signature is removed, the error is:
  Illegal type pattern.
  A type pattern must be checked against a visible forall.

When the type of the function is known and contains a `forall`, all we need to
do is instantiate the forall-bound variable with the supplied type argument.
This is done by tcVTA (if Specified) and tcVDQ (if Required).

tcVDQ unwraps the HsEmbTy and uses the type contained within it.  Crucially, in
tcVDQ we know that we are expecting a type argument.  This means that we can
support
    f (Maybe Int)   -- HsApp, no HsEmbTy
The type argument (Maybe Int) is represented as an HsExpr, but tcVDQ can easily
convert it to HsType.  This conversion is called the "T2T-Mapping" in GHC
Proposal #281.

Typechecking type abstractions
------------------------------
Type abstractions are checked alongside ordinary patterns in GHC.Tc.Gen.Pat.tcMatchPats.
One of its inputs is a list of ExpPatType that has two constructors
  * ExpFunPatTy    ...   -- the type A of a function A -> B
  * ExpForAllPatTy ...   -- the binder (a::A) of forall (a::A) -> B
so when we are checking
  f :: forall a b -> a -> b -> ...
  f (type a) (type b) (x :: a) (y :: b) = ...
our expected pattern types are
  [ ExpForAllPatTy ...      -- forall a ->
  , ExpForAllPatTy ...      -- forall b ->
  , ExpFunPatTy    ...      -- a ->
  , ExpFunPatTy    ...      -- b ->
  ]

The [ExpPatType] is initially constructed by GHC.Tc.Utils.Unify.matchExpectedFunTys,
by decomposing the type signature for `f` in our example.  If we are given a
definition
   g (type a) = ...
we never /infer/ a type g :: forall a -> blah.  We can only /check/
explicit type abstractions in terms.

The [ExpPatType] allows us to use different code paths for type abstractions
and ordinary patterns:
  * tc_pat :: Scaled ExpSigmaTypeFRR -> Checker (Pat GhcRn) (Pat GhcTc)
  * tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)

tc_forall_pat unwraps the EmbTyPat and uses the type pattern contained
within it. This is another spot where the "T2T-Mapping" can take place,
allowing us to support
  f a (x :: a) = rhs    -- no EmbTyPat

Type patterns in constructor patterns are handled in with tcConTyArg.
Both tc_forall_pat and tcConTyArg delegate most of the work to tcHsTyPat.

Note [VTA for out-of-scope functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose 'wurble' is not in scope, and we have
   (wurble @Int @Bool True 'x')

Then the renamer will make (HsHole (HsVar "wurble")) for 'wurble',
and the typechecker will typecheck it with tcUnboundId, giving it
a type 'alpha', and emitting a deferred Hole constraint, to
be reported later.

But then comes the visible type application. If we do nothing, we'll
generate an immediate failure (in tc_app_err), saying that a function
of type 'alpha' can't be applied to Bool.  That's insane!  And indeed
users complain bitterly (#13834, #17150.)

The right error is the Hole, which has /already/ been emitted by
tcUnboundId.  It later reports 'wurble' as out of scope, and tries to
give its type.

Fortunately in tcInstFun we still have access to the function, so we
can check if it is a HsHole.  We use this info to simply skip
over any visible type arguments.  We'll /already/ have emitted a
Hole constraint; failing preserves that constraint.

We do /not/ want to fail altogether in this case (via failM) because
that may abandon an entire instance decl, which (in the presence of
-fdefer-type-errors) leads to leading to #17792.

What about required type arguments?  Suppose we see
    f (type Int)
where `f` is out of scope.  Then again we don't want to crash because f's
type (which will be just a fresh unification variable) isn't a visible forall.
Instead we just skip the `(type Int)` argument, as before.

Downside: the typechecked term has lost its visible type arguments; we
don't even kind-check them.  But let's jump that bridge if we come to
it.  Meanwhile, let's not crash!

Note [Type application substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In `tc_inst_forall_arg`, suppose we are checking a visible type
application `f @hs_ty`, where `f :: forall (a :: k). body`.  We will:
  * Compute `ty <- tcHsTypeApp hs_ty k`
  * Then substitute `a :-> ty` in `body`.
Now, you might worry that `a` might not have the same kind as `ty`, so that the
substitution isn't kind-preserving.  How can that happen?  The kinds will
definitely be the same after zonking, and `ty` will be zonked (as this is
a postcondition of `tcHsTypeApp`). But the function type `forall a. body`
might not be fully zonked (hence the worry).

But it's OK!  During type checking, we don't require types to be well-kinded (without
zonking); we only require them to satsisfy the Purely Kinded Type Invariant (PKTI).
See Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType.

In the case of a type application:
  * `forall a. body` satisfies the PKTI
  * `ty` is zonked
  * If we substitute a fully-zonked thing into an un-zonked Type that
    satisfies the PKTI, the result still satisfies the PKTI.

This last statement isn't obvious, but read
Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType.
The tricky case is when `body` contains an application of the form `a b1 ... bn`,
and we substitute `a :-> ty` where `ty` has fewer arrows in its kind than `a` does.
That can't happen: the call `tcHsTypeApp hs_ty k` would have rejected the
type application as ill-kinded.

Historical remark: we used to require a stronger invariant than the PKTI,
namely that all types are well-kinded prior to zonking. In that context, we did
need to zonk `body` before performing the substitution above. See test case
#14158, as well as the discussion in #23661.
-}

{- *********************************************************************
*                                                                      *
              Quick Look
*                                                                      *
********************************************************************* -}

{- Note [Quick Look at value arguments]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The function quickLookArg implements the "QL argument" judgement of
the QL paper, in Fig 5 of "A quick look at impredicativity" (ICFP 2020),
rather directly.  The key rule, implemented by `quickLookArg` is

   G |-h h:sg                         -- Find the type of the head
   G |-inst sg;pis ~> phis;rho_r      -- tcInstFun on the args
   (A) rho = T sgs  OR  (B) fiv(phis) = emptyset  -- can_do_ql
   -------------------------------------- APP-QL
   G |-ql h pis : rho ~> qlUnify( rho, rho_r )

(The paper uses a lightning-bolt where we use "ql".)  The most straightforward
way to implement this rule for a call (f e1 ... en) would be:

   1. Take a quick look at the argumets e1..en to guide instantiation
      of the function f.
   2. Then typecheck e1..en from scratch.

That's wasteful, because in Step 1, the quick look at each argument, say (g
h1..hm), involves instantiating `h` and taking a quick look at /its/
arguments.  Then in Step 2 we typecheck (g h1..hm) and again take a quick look
at its arguments.  This is quadratic in the nesting depth of the arguments.

Instead, after the quick look, we /save/ the work we have done in an EValArgQL
record, and /resume/ it later.  The way to think of it is this:

  * `tcApp` typechecks an application.  It uses `tcInstFun`, which in turn
    calls `quickLookArg` on each value argument.

  * `quickLookArg` (which takes a quick look at the argument)

      - Does the "initial" part of `tcApp`, especially `tcInstFun`

      - Captures the result in an EValArgQL record

      - Later, `tcValArg` starts from the EValArgQL record, and
        completes the job of typechecking the application

This turned out to be more subtle than I expected.  Wrinkles:

(QLA1) `quickLookArg` decides whether or not premises (A) and (B) of the
  quick-look-arg judgement APP-QL are satisfied; this is captured in
  `arg_influences_enclosing_call`.

(QLA2) We avoid zonking, so the `arg_influences_enclosing_call` sees the
  argument type /before/ the QL substitution Theta is applied to it. So we
  achieve argument-order independence for free (see 5.7 in the paper).  See the
  `isGuardedTy orig_arg_rho` test in `quickLookArg`.

(QLA3) Deciding whether the premises are satisfied involves calling `tcInstFun`
  (which takes quite some work becuase it calls quickLookArg on nested calls).
  That's why we want to capture the work done, in EValArgQL.

  Do we really have to call `tcInstFun` before deciding (B) of
  `arg_influences_enclosing_call`? Yes (#24686).
  Suppose ids :: [forall a. a->a], and consider
     (:) (reverse ids) blah
  `tcApp` on the outer call will instantiate (:) with `kappa`, and take a
  quick look at (reverse ids). Only after instantiating `reverse` with kappa2,
  quick-looking at `ids` can we discover that (kappa2:=forall a. a->a), which
  satisfies premise (B) of `arg_influence_enclosing_call`.

(QLA4) When we resume typechecking an argument, in `tcValArg` on `EValArgQL`

  - Calling `tcInstFun` on the argument may have emitted some constraints, which
    we carefully captured in `quickLookArg` and stored in the EValArgQL.  We must
    now emit them with `emitConstraints`.  This must be done /under/ the skolemisation
    of the argument's type (see `tcSkolemise` in `tcValArg` for EValArgQL { ...}.
    Example:   f :: (forall b. Ord b => b -> b -> Bool) -> ...
       Call:   f (==)
    we must skolemise the argument type (forall b. Ord b => b -> b -> Bool)
    before emitting the [W] Eq alpha constraint arising from the call to (==).
    It will be solved from the Ord b!

  - quickLookArg may or may not have done `qlUnify` with the calling context.
    If not (eaql_encl = False) must do so now.  Example:  choose [] ids,
            where ids :: [forall a. a->a]
                  choose :: a -> a -> a
    We instantiate choose with `kappa` and discover from `ids` that
    (kappa = [forall a. a->a]).  Now we resume typechecking argument [], and
    we must take advantage of what we have now discovered about `kappa`,
    to typecheck   [] :: [forall a. a->a]

(QLA5) In the quicklook pass, we don't scale multiplicities. Since arguments
    aren't typechecked yet, we don't know their free variable usages
    anyway. But, in a nested call, the head of an application chain is fully
    typechecked.

    In order for the multiplicities in the head to be properly scaled, we store
    the head's usage environment in the eaql_fun_ue field. Then, when we do the
    full-typechecking pass, we can emit the head's usage environment where we
    would have typechecked the head in a naive algorithm.

(QLA6) `quickLookArg` is supposed to capture the result of partially typechecking
   the argument, so it can be resumed later.  "Capturing" should include all
   generated type-class/equality constraints and Linear-Haskell usage info. There
   are two calls in `quickLookArg1` that might generate such constraints:

     - `tcInferAppHead_maybe`.  This can generat Linear-Haskell usage info, via
       the call to `tcEmitBindingUsage` in `check_local_id`, which is called
       indirectly by `tcInferAppHead_maybe`.

       In contrast, `tcInferAppHead_maybe` does not generate any type-class or
       equality constraints, because it doesn't instantiate any functions.  [But
       see #25493 and #25494 for why this isn't quite true today.]

    - `tcInstFun` generates lots of type-class and equality constraints, as it
      instantiates the function.  But it generates no usage info, because that
      comes only from the call to `check_local_id`, whose usage info is captured
      in the call to `tcInferAppHead_maybe` in `quickLookArg1`.

  Conclusion: in quickLookArg1:
    - capture usage information (but not constraints)
        for the call to `tcInferAppHead_maybe`
    - capture constraints (but not usage information)
        for the call to `tcInstFun`

-}

quickLookArg :: QLFlag -> Int
             -> HsExprLoc -- ^ location span of the whole application
             -> (HsExpr GhcRn, SrcSpan) -- ^ Head of the application chain and its source span
             -> LHsExpr GhcRn          -- ^ Argument
             -> Scaled TcSigmaTypeFRR  -- ^ Type expected by the function
             -> TcM (HsExprArg 'TcpInst)
-- See Note [Quick Look at value arguments]
quickLookArg :: QLFlag
-> Int
-> SrcSpanAnnA
-> (HsExpr GhcRn, SrcSpan)
-> LHsExpr GhcRn
-> Scaled TcType
-> TcM (HsExprArg 'TcpInst)
quickLookArg QLFlag
NoQL Int
_ SrcSpanAnnA
app_lspan (HsExpr GhcRn, SrcSpan)
_ LHsExpr GhcRn
larg Scaled TcType
orig_arg_ty
  = SrcSpanAnnA
-> LHsExpr GhcRn -> Scaled TcType -> TcM (HsExprArg 'TcpInst)
skipQuickLook SrcSpanAnnA
app_lspan LHsExpr GhcRn
larg Scaled TcType
orig_arg_ty
quickLookArg QLFlag
DoQL Int
pos SrcSpanAnnA
app_lspan (HsExpr GhcRn, SrcSpan)
fun_and_lspan LHsExpr GhcRn
larg Scaled TcType
orig_arg_ty
  = do { is_rho <- TcType -> TcRnIf TcGblEnv TcLclEnv Bool
qlArgHasRhoType (Scaled TcType -> TcType
forall a. Scaled a -> a
scaledThing Scaled TcType
orig_arg_ty)
       ; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho)
       ; if not is_rho
         then skipQuickLook app_lspan larg orig_arg_ty
         else quickLookArg1 pos app_lspan fun_and_lspan larg orig_arg_ty }

skipQuickLook :: HsExprLoc -> LHsExpr GhcRn -> Scaled TcRhoType
              -> TcM (HsExprArg 'TcpInst)
skipQuickLook :: SrcSpanAnnA
-> LHsExpr GhcRn -> Scaled TcType -> TcM (HsExprArg 'TcpInst)
skipQuickLook SrcSpanAnnA
app_lspan LHsExpr GhcRn
larg Scaled TcType
arg_ty
  = HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (EValArg { ea_loc_span :: SrcSpanAnnA
ea_loc_span   = SrcSpanAnnA
app_lspan
                    , ea_arg :: LHsExpr (GhcPass (XPass 'TcpInst))
ea_arg    = LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpInst))
larg
                    , ea_arg_ty :: XEVAType 'TcpInst
ea_arg_ty = Scaled TcType
XEVAType 'TcpInst
arg_ty })

whenQL :: QLFlag -> ZonkM () -> TcM ()
whenQL :: QLFlag -> ZonkM () -> TcRn ()
whenQL QLFlag
DoQL ZonkM ()
thing_inside = ZonkM () -> TcRn ()
forall a. ZonkM a -> TcM a
liftZonkM ZonkM ()
thing_inside
whenQL QLFlag
NoQL ZonkM ()
_            = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

qlArgHasRhoType :: TcType -> TcM Bool
-- `qlArgHasRhoType` checks that the expected argument type in rule
-- App-lightning-bolt (Fig 5 in the paper) is indeed a rho-type.
--
-- It must apply the current QL substitution, so it any QLInstTyVar that it
-- comes across.   Why?  See Section 5.7 in the paper; argument order matters.
--
-- What if we find an /un-filled/ QLInstVar?  We treat this as a rho-type
-- even though a later argument might force it to be sigma-type.  See
-- Section 9 in the paper.
--
-- With -XDeepSubsunption we need a /deep/ rho-type.
-- (We don't need getDeepSubsumptionFlag_DataConHead here because this
-- is only about QuickLook.)

qlArgHasRhoType :: TcType -> TcRnIf TcGblEnv TcLclEnv Bool
qlArgHasRhoType TcType
ty
  = do { ds_flag <- TcM DeepSubsumptionFlag
getDeepSubsumptionFlag
       ; go ds_flag ty }
  where
    go :: DeepSubsumptionFlag -> TcType -> m Bool
go DeepSubsumptionFlag
ds_flag TcType
ty
      | TcType -> Bool
isSigmaTy TcType
ty
      = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

      | Just Id
kappa <- TcType -> Maybe Id
getTyVar_maybe TcType
ty
      , Id -> Bool
isQLInstTyVar Id
kappa
      = do { info <- Id -> m MetaDetails
forall (m :: * -> *). MonadIO m => Id -> m MetaDetails
readMetaTyVar Id
kappa
           ; case info of
               Indirect TcType
arg_ty' -> DeepSubsumptionFlag -> TcType -> m Bool
go DeepSubsumptionFlag
ds_flag TcType
arg_ty'
               MetaDetails
Flexi            -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }

      | Deep {} <- DeepSubsumptionFlag
ds_flag
      , Just (Scaled TcType
_, TcType
res_ty) <- TcType -> Maybe (Scaled TcType, TcType)
tcSplitFunTy_maybe TcType
ty
      = DeepSubsumptionFlag -> TcType -> m Bool
go DeepSubsumptionFlag
ds_flag TcType
res_ty

      | Bool
otherwise
      = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

isGuardedTy :: TcType -> Bool
isGuardedTy :: TcType -> Bool
isGuardedTy TcType
ty
  | Just (TyCon
tc,TcThetaType
_) <- HasDebugCallStack => TcType -> Maybe (TyCon, TcThetaType)
TcType -> Maybe (TyCon, TcThetaType)
tcSplitTyConApp_maybe TcType
ty = TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
Nominal
  | Just {} <- TcType -> Maybe (TcType, TcType)
tcSplitAppTy_maybe TcType
ty        = Bool
True
  | Bool
otherwise                               = Bool
False

quickLookArg1 :: Int
              -> HsExprLoc
              -> (HsExpr GhcRn, SrcSpan)
              -> LHsExpr GhcRn
              -> Scaled TcRhoType  -- Deeply skolemised
              -> TcM (HsExprArg 'TcpInst)
-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
quickLookArg1 :: Int
-> SrcSpanAnnA
-> (HsExpr GhcRn, SrcSpan)
-> LHsExpr GhcRn
-> Scaled TcType
-> TcM (HsExprArg 'TcpInst)
quickLookArg1 Int
pos SrcSpanAnnA
app_lspan (HsExpr GhcRn, SrcSpan)
rn_head larg :: LHsExpr GhcRn
larg@(L SrcSpanAnnA
_ HsExpr GhcRn
arg) sc_arg_ty :: Scaled TcType
sc_arg_ty@(Scaled TcType
_ TcType
orig_arg_rho)
  = Int
-> (HsExpr GhcRn, SrcSpan)
-> LHsExpr GhcRn
-> TcM (HsExprArg 'TcpInst)
-> TcM (HsExprArg 'TcpInst)
forall a.
Int -> (HsExpr GhcRn, SrcSpan) -> LHsExpr GhcRn -> TcM a -> TcM a
addArgCtxt Int
pos (HsExpr GhcRn, SrcSpan)
rn_head LHsExpr GhcRn
larg (TcM (HsExprArg 'TcpInst) -> TcM (HsExprArg 'TcpInst))
-> TcM (HsExprArg 'TcpInst) -> TcM (HsExprArg 'TcpInst)
forall a b. (a -> b) -> a -> b
$ -- Context needed for constraints
                                           -- generated by calls in arg
    do { String -> SDoc -> TcRn ()
traceTc String
"qla1" (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
arg)

       ; (rn_fun_arg, rn_args) <- HsExpr GhcRn -> TcM (HsExpr GhcRn, [HsExprArg 'TcpRn])
splitHsApps HsExpr GhcRn
arg

       ; traceTc "qla2" (ppr arg)

       ; fun_lspan_arg <- getFunSrcSpan rn_args

       -- Step 1: get the type of the head of the argument
       ; (fun_ue, mb_fun_ty) <- tcCollectingUsage $ tcInferAppHead_maybe rn_fun_arg
         -- tcCollectingUsage: the use of an Id at the head generates usage-info
         -- See the call to `tcEmitBindingUsage` in `check_local_id`.  So we must
         -- capture and save it in the `EValArgQL`.  See (QLA6) in
         -- Note [Quick Look at value arguments]

       ; traceTc "quickLookArg {" $
         vcat [ text "arg:" <+> ppr arg
              , text "orig_arg_rho:" <+> ppr orig_arg_rho
              , text "head:" <+> ppr rn_fun_arg <+> dcolon <+> ppr mb_fun_ty
              , text "args:" <+> ppr rn_args ]

       ; case mb_fun_ty of {
           Maybe (HsExpr GhcTc, TcType)
Nothing -> SrcSpanAnnA
-> LHsExpr GhcRn -> Scaled TcType -> TcM (HsExprArg 'TcpInst)
skipQuickLook SrcSpanAnnA
app_lspan LHsExpr GhcRn
larg Scaled TcType
sc_arg_ty ;    -- fun is too complicated
           Just (HsExpr GhcTc
tc_fun_arg_head, TcType
fun_sigma_arg_head) ->

       -- step 2: use |-inst to instantiate the head applied to the arguments
    do { let arg_tc_head :: (HsExpr GhcTc, SrcSpan)
arg_tc_head = (HsExpr GhcTc
tc_fun_arg_head, SrcSpan
fun_lspan_arg)
       ; do_ql <- HsExpr GhcRn -> TcM QLFlag
wantQuickLook HsExpr GhcRn
rn_fun_arg

       ; ((inst_args, app_res_rho), wanted)
             <- captureConstraints $
                tcInstFun do_ql True (rn_fun_arg, fun_lspan_arg) tc_fun_arg_head fun_sigma_arg_head rn_args
                -- We must capture type-class and equality constraints here, but
                -- not usage information.  See (QLA6) in Note [Quick Look at
                -- value arguments]

       ; traceTc "quickLookArg 2" $
         vcat [ text "arg:" <+> ppr arg
              , text "orig_arg_rho:" <+> ppr orig_arg_rho
              , text "app_res_rho:" <+> ppr app_res_rho ]

       -- Step 3: Check the two other premises of APP-lightning-bolt (Fig 5 in the paper)
       --         Namely: (A) is orig_arg_rho is guarded
         --           or: (B) fiv(app_res_rho) = emptyset
       -- This tells us if the quick look at the argument yields information that
       -- influences the enclosing function call
       -- NB: guardedness is computed based on the original,
       -- unzonked orig_arg_rho, so that we deliberately do
       -- not exploit guardedness that emerges a result of QL on earlier args
       -- We must do the anyFreeKappa test /after/ tcInstFun; see (QLA3).
       ; arg_influences_enclosing_call
            <- if isGuardedTy orig_arg_rho
               then return True
               else not <$> anyFreeKappa app_res_rho  -- (B)
                    -- For (B) see Note [The fiv test in quickLookArg]

       -- Step 4: do quick-look unification if either (A) or (B) hold
       -- NB: orig_arg_rho may not be zonked, but that's ok
       ; when arg_influences_enclosing_call $
         qlUnify app_res_rho orig_arg_rho

       ; traceTc "quickLookArg done }" (ppr rn_fun_arg)

       ; return (EValArgQL { eaql_loc_span = app_lspan
                           , eaql_arg_ty   = sc_arg_ty
                           , eaql_larg     = larg
                           , eaql_tc_fun   = arg_tc_head
                           , eaql_rn_fun   = rn_fun_arg
                           , eaql_fun_ue   = fun_ue
                           , eaql_args     = inst_args
                           , eaql_wanted   = wanted
                           , eaql_encl     = arg_influences_enclosing_call
                           , eaql_res_rho  = app_res_rho }) }}}


{- *********************************************************************
*                                                                      *
                 Folding over instantiation variables
*                                                                      *
********************************************************************* -}

{- Note [Monomorphise instantiation variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we are done with Quick Look on a call, we must turn any un-unified
/instantiation/ variables into regular /unification/ variables.  This is the
lower-case 'theta' (a mono-substitution) in the APP-DOWN rule of Fig 5 of the
Quick Look paper.

We so this by look at the arguments, left to right, monomorphising the free
instantiation variables of the /type/ arguments of the call.  Those type
arguments appear (only) in
  * the `WpTyApp` components of
  * the `HsWrapper` of
  * a `EWrap` argument
See `qlMonoHsWrapper`.

By going left to right, we are sure to monomorphise instantiation variables
before we encounter them in an argument type (in `tcValArg`).

All instantiation variables for a call will be reachable from the type(s)
at which the function is instantiated -- i.e. those WpTyApps.  Even instantiation
variables allocoated by tcInstFun itself, such as in the IRESULT rule, end up
connected to the original type(s) at which the function is instantiated.

To monomorphise the free QL instantiation variables of a type, we use
`foldQLInstVars`.

Wrinkles:

(MIV1) When monomorphising an instantiation variable, don't forget to
   monomorphise its kind. It might have type (a :: TYPE k), where both
  `a` and `k` are instantiation variables.

(MIV2) In `qlUnify`, `make_kinds_ok` may unify
    a :: k1  ~  b :: k2
  making a cast
    a := b |> (co :: k1 ~ k2)
  But now suppose k1 is an instantiation variable.  Then that coercion hole
  `co` is the only place that `k1` will show up in the traversal, and yet
  we want to monomrphise it.  Hence the do_hole in `foldQLInstTyVars`
-}

qlMonoHsWrapper :: HsWrapper -> ZonkM ()
-- See Note [Monomorphise instantiation variables]
qlMonoHsWrapper :: HsWrapper -> ZonkM ()
qlMonoHsWrapper (WpCompose HsWrapper
w1 HsWrapper
w2) = HsWrapper -> ZonkM ()
qlMonoHsWrapper HsWrapper
w1 ZonkM () -> ZonkM () -> ZonkM ()
forall a b. ZonkM a -> ZonkM b -> ZonkM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> HsWrapper -> ZonkM ()
qlMonoHsWrapper HsWrapper
w2
qlMonoHsWrapper (WpTyApp TcType
ty)      = TcType -> ZonkM ()
qlMonoTcType TcType
ty
qlMonoHsWrapper HsWrapper
_                 = () -> ZonkM ()
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

qlMonoTcType :: TcType -> ZonkM ()
-- See Note [Monomorphise instantiation variables]
qlMonoTcType :: TcType -> ZonkM ()
qlMonoTcType TcType
ty
  = do { String -> SDoc -> ZonkM ()
traceZonk String
"monomorphiseQLInstVars {" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty)
       ; TcType -> ZonkM ()
go_ty TcType
ty
       ; String -> SDoc -> ZonkM ()
traceZonk String
"monomorphiseQLInstVars }" SDoc
forall doc. IsOutput doc => doc
empty }
  where
    go_ty :: TcType -> ZonkM ()
    go_ty :: TcType -> ZonkM ()
go_ty TcType
ty = TcMUnit -> ZonkM ()
unTcMUnit ((Id -> TcMUnit) -> TcType -> TcMUnit
forall a. Monoid a => (Id -> a) -> TcType -> a
foldQLInstVars Id -> TcMUnit
go_tv TcType
ty)

    go_tv :: TcTyVar -> TcMUnit
    -- Precondition: tv is a QL instantiation variable
    -- If it is already unified, look through it and carry on
    -- If not, monomorphise it, by making a fresh unification variable,
    -- at the ambient level
    go_tv :: Id -> TcMUnit
go_tv Id
tv
      | MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref, mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
lvl, mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } <- Id -> TcTyVarDetails
tcTyVarDetails Id
tv
      = Bool -> SDoc -> TcMUnit -> TcMUnit
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (case TcLevel
lvl of TcLevel
QLInstVar -> Bool
True; TcLevel
_ -> Bool
False) (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv) (TcMUnit -> TcMUnit) -> TcMUnit -> TcMUnit
forall a b. (a -> b) -> a -> b
$
        ZonkM () -> TcMUnit
ZonkM () -> TcMUnit
TCMU (ZonkM () -> TcMUnit) -> ZonkM () -> TcMUnit
forall a b. (a -> b) -> a -> b
$ do { String -> SDoc -> ZonkM ()
traceZonk String
"qlMonoTcType" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv)
                  ; flex <- IORef MetaDetails -> ZonkM MetaDetails
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef IORef MetaDetails
ref
                  ; case flex of {
                      Indirect TcType
ty -> TcType -> ZonkM ()
go_ty TcType
ty ;
                      MetaDetails
Flexi       ->
               do { let kind :: TcType
kind = Id -> TcType
tyVarKind Id
tv
                  ; TcType -> ZonkM ()
go_ty TcType
kind  -- See (MIV1) in Note [Monomorphise instantiation variables]
                  ; ref2  <- MetaDetails -> ZonkM (IORef MetaDetails)
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
newTcRef MetaDetails
Flexi
                  ; lvl2  <- getZonkTcLevel
                  ; let details = MetaTv { mtv_info :: MetaInfo
mtv_info  = MetaInfo
info
                                         , mtv_ref :: IORef MetaDetails
mtv_ref   = IORef MetaDetails
ref2
                                         , mtv_tclvl :: TcLevel
mtv_tclvl = TcLevel
lvl2 }
                        tv2  = Name -> TcType -> TcTyVarDetails -> Id
mkTcTyVar (Id -> Name
tyVarName Id
tv) TcType
kind TcTyVarDetails
details
                 ; writeTcRef ref (Indirect (mkTyVarTy tv2)) }}}
      | Bool
otherwise
      = String -> SDoc -> TcMUnit
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"qlMonoTcType" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv)

newtype TcMUnit = TCMU { TcMUnit -> ZonkM ()
unTcMUnit :: ZonkM () }
instance Semigroup TcMUnit where
  TCMU ZonkM ()
ml <> :: TcMUnit -> TcMUnit -> TcMUnit
<> TCMU ZonkM ()
mr = ZonkM () -> TcMUnit
TCMU (ZonkM ()
ml ZonkM () -> ZonkM () -> ZonkM ()
forall a b. ZonkM a -> ZonkM b -> ZonkM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ZonkM ()
mr)
instance Monoid TcMUnit where
  mempty :: TcMUnit
mempty = ZonkM () -> TcMUnit
TCMU (() -> ZonkM ()
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

{- Note [The fiv test in quickLookArg]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In rule APP-lightning-bolt in Fig 5 of the paper, we have to test rho_r
for having no free instantiation variables.  We do this in Step 3 of quickLookArg1,
using anyFreeKappa.  Example:
    Suppose       ids :: [forall a. a->a]
    and consider  Just (ids++ids)
We will instantiate Just with kappa, say, and then call
    quickLookArg1 False {kappa} (ids ++ ids) kappa
The call to tcInstFun will return with app_res_rho = [forall a. a->a]
which has no free instantiation variables, so we can QL-unify
  kappa ~ [Forall a. a->a]
-}

anyFreeKappa :: TcType -> TcM Bool
-- True if there is a free instantiation variable
-- in the argument type, after zonking
-- See Note [The fiv test in quickLookArg]
anyFreeKappa :: TcType -> TcRnIf TcGblEnv TcLclEnv Bool
anyFreeKappa TcType
ty = TcMBool -> TcRnIf TcGblEnv TcLclEnv Bool
unTcMBool ((Id -> TcMBool) -> TcType -> TcMBool
forall a. Monoid a => (Id -> a) -> TcType -> a
foldQLInstVars Id -> TcMBool
go_tv TcType
ty)
  where
    go_tv :: Id -> TcMBool
go_tv Id
tv = TcRnIf TcGblEnv TcLclEnv Bool -> TcMBool
TcRnIf TcGblEnv TcLclEnv Bool -> TcMBool
TCMB (TcRnIf TcGblEnv TcLclEnv Bool -> TcMBool)
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcMBool
forall a b. (a -> b) -> a -> b
$ do { info <- Id -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => Id -> m MetaDetails
readMetaTyVar Id
tv
                         ; case info of
                             Indirect TcType
ty -> TcType -> TcRnIf TcGblEnv TcLclEnv Bool
anyFreeKappa TcType
ty
                             MetaDetails
Flexi       -> Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }

newtype TcMBool = TCMB { TcMBool -> TcRnIf TcGblEnv TcLclEnv Bool
unTcMBool :: TcM Bool }
instance Semigroup TcMBool where
  TCMB TcRnIf TcGblEnv TcLclEnv Bool
ml <> :: TcMBool -> TcMBool -> TcMBool
<> TCMB TcRnIf TcGblEnv TcLclEnv Bool
mr = TcRnIf TcGblEnv TcLclEnv Bool -> TcMBool
TCMB (do { l <- TcRnIf TcGblEnv TcLclEnv Bool
ml; if l then return True else mr })
instance Monoid TcMBool where
  mempty :: TcMBool
mempty = TcRnIf TcGblEnv TcLclEnv Bool -> TcMBool
TCMB (Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

foldQLInstVars :: forall a. Monoid a => (TcTyVar -> a) -> TcType -> a
{-# INLINE foldQLInstVars #-}
foldQLInstVars :: forall a. Monoid a => (Id -> a) -> TcType -> a
foldQLInstVars Id -> a
check_tv TcType
ty
  = FV () a -> () -> a
forall env acc. FV env acc -> env -> acc
runFV (TcType -> FV () a
do_ty TcType
ty) ()
  where
    (TcType -> FV () a
do_ty, TcThetaType -> FV () a
_, TcCoercion -> FV () a
_, [TcCoercion] -> FV () a
_) = TyCoFolder (FV () a)
-> (TcType -> FV () a, TcThetaType -> FV () a,
    TcCoercion -> FV () a, [TcCoercion] -> FV () a)
forall a.
Monoid a =>
TyCoFolder a
-> (TcType -> a, TcThetaType -> a, TcCoercion -> a,
    [TcCoercion] -> a)
foldTyCo TyCoFolder (FV () a)
folder

    folder :: TyCoFolder (FV () a)
    folder :: TyCoFolder (FV () a)
folder = TyCoFolder { tcf_view :: TcType -> Maybe TcType
tcf_view = TcType -> Maybe TcType
noView  -- See Note [Free vars and synonyms]
                                             -- in GHC.Core.TyCo.FVs
                        , tcf_tyvar :: Id -> FV () a
tcf_tyvar = Id -> FV () a
do_tv, tcf_covar :: Id -> FV () a
tcf_covar = Id -> FV () a
forall a. Monoid a => a
mempty
                        , tcf_hole :: CoercionHole -> FV () a
tcf_hole = CoercionHole -> FV () a
do_hole, tcf_tycobinder :: Id -> FV () a -> FV () a
tcf_tycobinder = Id -> FV () a -> FV () a
forall {p} {a}. p -> a -> a
do_bndr }

    do_bndr :: p -> a -> a
do_bndr p
_ = a -> a
forall a. a -> a
id

    do_hole :: CoercionHole -> FV () a
do_hole CoercionHole
hole = TcType -> FV () a
do_ty (Id -> TcType
coVarKind (CoercionHole -> Id
coHoleCoVar CoercionHole
hole))
                     -- See (MIV2) in Note [Monomorphise instantiation variables]

    do_tv :: TcTyVar -> FV () a
    do_tv :: Id -> FV () a
do_tv Id
tv | Id -> Bool
isQLInstTyVar Id
tv = (() -> a) -> FV () a
forall env acc. (env -> acc) -> FV env acc
MkFV ((() -> a) -> FV () a) -> (() -> a) -> FV () a
forall a b. (a -> b) -> a -> b
$ \()
_ -> Id -> a
check_tv Id
tv
             | Bool
otherwise        = FV () a
forall a. Monoid a => a
mempty

{- *********************************************************************
*                                                                      *
                 QuickLook unification
*                                                                      *
********************************************************************* -}

qlUnify ::  TcType -> TcType -> TcM ()
-- Unify ty1 with ty2:
--   * It can unify both instantiation variables (possibly with polytypes),
--     and ordinary unification variables (but only with monotypes)
--   * It does not return a coercion (unlike unifyType); it is called
--     for the sole purpose of unifying instantiation variables, although it
--     may also (opportunistically) unify regular unification variables.
--   * It never produces errors, even for mis-matched types
--   * It may return without having made the argument types equal, of course;
--     it just makes best efforts.
qlUnify :: TcType -> TcType -> TcRn ()
qlUnify TcType
ty1 TcType
ty2
  = do { String -> SDoc -> TcRn ()
traceTc String
"qlUnify" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2)
       ; TcType -> TcType -> TcRn ()
go TcType
ty1 TcType
ty2 }
  where
    go :: TcType -> TcType -> TcM ()

    -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
    -- and         (c1 => res1) ~   (c2 => res2)
    -- But for the latter we only learn instantiation info from res1~res2
    go :: TcType -> TcType -> TcRn ()
go (FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af1, ft_arg :: TcType -> TcType
ft_arg = TcType
arg1, ft_res :: TcType -> TcType
ft_res = TcType
res1 })
       (FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af2, ft_arg :: TcType -> TcType
ft_arg = TcType
arg2, ft_res :: TcType -> TcType
ft_res = TcType
res2 })
      | FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
af2 -- Match the arrow TyCon
      = do { Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af1) (TcType -> TcType -> TcRn ()
go TcType
arg1 TcType
arg2)

        -- NB: we do not unify the multiplicities; that would be too strong.
        -- We might only require mult1 ⩽ mult2, as in Note [Multiplicity in deep subsumption].
        -- ; when (isFUNArg af1)        (go mult1 mult2)

           ; TcType -> TcType -> TcRn ()
go TcType
res1 TcType
res2 }

    -- Make sure to not unify "kappa := (a %1 -> b)". See (UQL5).
    go (FunTy { ft_mult :: TcType -> TcType
ft_mult = TcType
OneTy }) TcType
_ = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    go TcType
_ (FunTy { ft_mult :: TcType -> TcType
ft_mult = TcType
OneTy }) = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- NB: we do want to be able to unify "kappa := a => b", as that's
      -- the main point of QuickLook (allowing meta-variables to be unified
      -- with qualified types).

    go (TyVarTy Id
tv) TcType
ty2
      | Id -> Bool
isMetaTyVar Id
tv = Id -> TcType -> TcRn ()
go_kappa Id
tv TcType
ty2
    go TcType
ty1 (TyVarTy Id
tv)
      | Id -> Bool
isMetaTyVar Id
tv = Id -> TcType -> TcRn ()
go_kappa Id
tv TcType
ty1

    go (CastTy TcType
ty1 TcCoercion
_) TcType
ty2 = TcType -> TcType -> TcRn ()
go TcType
ty1 TcType
ty2
    go TcType
ty1 (CastTy TcType
ty2 TcCoercion
_) = TcType -> TcType -> TcRn ()
go TcType
ty1 TcType
ty2

    go (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
      | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2 -- See GHC.Tc.Utils.Unify
      = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- Note [Expanding synonyms during unification]

    -- Now, and only now, expand synonyms
    go TcType
rho1 TcType
rho2
      | Just TcType
rho1 <- TcType -> Maybe TcType
coreView TcType
rho1 = TcType -> TcType -> TcRn ()
go TcType
rho1 TcType
rho2
      | Just TcType
rho2 <- TcType -> Maybe TcType
coreView TcType
rho2 = TcType -> TcType -> TcRn ()
go TcType
rho1 TcType
rho2

    go (TyConApp TyCon
tc1 TcThetaType
tys1) (TyConApp TyCon
tc2 TcThetaType
tys2)
      | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
      , Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1)
      , TcThetaType
tys1 TcThetaType -> TcThetaType -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` TcThetaType
tys2
      = (TcType -> TcType -> TcRn ())
-> TcThetaType -> TcThetaType -> TcRn ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ TcType -> TcType -> TcRn ()
go TcThetaType
tys1 TcThetaType
tys2

    -- Don't allow unifying (a => b) with the AppTy 'arr[tau] a b'.
    -- To ensure this, use 'tcSplitAppTyNoView_maybe' which does not split (=>).
    go (AppTy TcType
t1a TcType
t1b) TcType
ty2
      | Just (TcType
t2a, TcType
t2b) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTyNoView_maybe TcType
ty2
      = do { TcType -> TcType -> TcRn ()
go TcType
t1a TcType
t2a; TcType -> TcType -> TcRn ()
go TcType
t1b TcType
t2b }
    go TcType
ty1 (AppTy TcType
t2a TcType
t2b)
      | Just (TcType
t1a, TcType
t1b) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTyNoView_maybe TcType
ty1
      = do { TcType -> TcType -> TcRn ()
go TcType
t1a TcType
t2a; TcType -> TcType -> TcRn ()
go TcType
t1b TcType
t2b }

    go TcType
_ TcType
_ = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       -- Don't look under foralls; see (UQL4) of Note [QuickLook unification]

    ----------------
    go_kappa :: Id -> TcType -> TcRn ()
go_kappa Id
kappa TcType
ty2
      = Bool -> SDoc -> TcRn () -> TcRn ()
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Id -> Bool
isMetaTyVar Id
kappa) (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
kappa) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
        do { info <- Id -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => Id -> m MetaDetails
readMetaTyVar Id
kappa
           ; case info of
               Indirect TcType
ty1 -> TcType -> TcType -> TcRn ()
go TcType
ty1 TcType
ty2
               MetaDetails
Flexi        -> do { ty2 <- ZonkM TcType -> TcM TcType
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TcType -> TcM TcType) -> ZonkM TcType -> TcM TcType
forall a b. (a -> b) -> a -> b
$ TcType -> ZonkM TcType
zonkTcType TcType
ty2
                                  ; go_flexi kappa ty2 } }

    ----------------
    -- Swap (kappa1[conc] ~ kappa2[tau])
    -- otherwise we'll fail to unify and emit a coercion.
    -- Just an optimisation: emitting a coercion is fine
    go_flexi :: Id -> TcType -> TcRn ()
go_flexi Id
kappa (TyVarTy Id
tv2)
      | Id -> Int
lhsPriority Id
tv2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Id -> Int
lhsPriority Id
kappa
      = Id -> TcType -> TcRn ()
go_flexi1 Id
tv2 (Id -> TcType
TyVarTy Id
kappa)
    go_flexi Id
kappa TcType
ty2
      = Id -> TcType -> TcRn ()
go_flexi1 Id
kappa TcType
ty2

    go_flexi1 :: Id -> TcType -> TcRn ()
go_flexi1 Id
kappa TcType
ty2  -- ty2 is zonked
      = do { cur_lvl <- TcM TcLevel
getTcLevel
              -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
              -- Here we are in the TcM monad, which does not track enclosing
              -- Given equalities; so for quick-look unification we conservatively
              -- treat /any/ level outside this one as untouchable. Hence cur_lvl.
           ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of
              SimpleUnifyResult
SUC_CanUnify ->
                do { co <- Maybe TypedThing -> TcType -> TcType -> TcM TcCoercion
unifyKind (TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (TcType -> TypedThing
TypeThing TcType
ty2)) TcType
ty2_kind TcType
kappa_kind
                           -- unifyKind: see (UQL2) in Note [QuickLook unification]
                           --            and (MIV2) in Note [Monomorphise instantiation variables]
                   ; let ty2' = TcType -> TcCoercion -> TcType
mkCastTy TcType
ty2 TcCoercion
co
                   ; traceTc "qlUnify:update" $
                     ppr kappa <+> text ":=" <+> ppr ty2
                   ; liftZonkM $ writeMetaTyVar kappa ty2' }
              SimpleUnifyResult
_ -> () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- e.g. occurs-check or forall-bound variable
           }
      where
        kappa_kind :: TcType
kappa_kind = Id -> TcType
tyVarKind Id
kappa
        ty2_kind :: TcType
ty2_kind   = HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
ty2

{- Note [QuickLook unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
That is the entire point of qlUnify!   Wrinkles:

(UQL1) Before unifying an instantiation variable in `go_flexi`, we must check
  the usual unification conditions, by calling `GHC.Tc.Utils.Unify.simpleUnifyCheck`.
  For example that checks for
    * An occurs-check
    * Level mis-match
    * An attempt to unify a concrete type variable with a non-concrete type.

(UQL2) What if kappa and ty have different kinds?  We simply call the
  ordinary unifier and use the coercion to connect the two.

  If that coercion is not Refl, it is all in vain: The whole point of
  qlUnify is to impredicatively unify (kappa := forall a. blah). It is
  no good to unify (kappa := (forall a.blah) |> co) because we can't
  use that casted polytype.

  BUT: unifyKind has emitted constraint(s) into the Tc monad, so we may as well
  use them.  (An alternative; use uType directly, if the result is not Refl,
  discard the constraints and the coercion, and do not update the instantiation
  variable.  But see "Sadly discarded design alternative" below.)

(UQL3) Instantiation variables don't really have a settled level yet;
  they have level QLInstVar (see Note [QuickLook instantiation variables]
  in GHC.Tc.Utils.TcType.  You might worry that we might unify
      alpha[1] := Maybe kappa[qlinst]
  and later this kappa turns out to be a level-2 variable, and we have committed
  a skolem-escape error.

  But happily this can't happen: QL instantiation variables have level infinity,
  and we never unify a variable with a type from a deeper level.

(UQL4) Should we look under foralls in qlUnify? The use-case would be
     (forall a.  beta[qlinst] -> a)  ~  (forall a. (forall b. b->b) -> a)
  where we might hope for
     beta := forall b. b

  But in fact we don't attempt this:

  * The normal on-the-fly unifier doesn't look under foralls, so why
    should qlUnify?

  * Looking under foralls means we'd have to track the bound variables on both
    sides.  Tiresome but not a show stopper.

  * We might call the *regular* unifier (via unifyKind) under foralls, and that
    doesn't know about those bound variables (it controls scope through level
    numbers) so it might go totally wrong.  At least we'd have to instantaite
    the forall-types with skolems (with level numbers).  Maybe more.

  It's just not worth the trouble, we think (for now at least).

(UQL5) qlUnify must be careful about linear function arrows. Suppose for example
  we have a program like:

    data A = MkA Int Bool
      -- As per Note [Data constructors are linear by default],
      -- this means that MkA :: Int %1 -> Bool -> A

    foo :: Maybe (Bool -> A) -> ()
    foo _ ()
    bar = foo just_pap
      where
        just_pap = Just $ B 3

  Here, when typechecking the application 'B A', we will get a call to qlUnify:

    qlUnify
      (Bool %1 -> A)
      𝜈[tau:qlinst]

  We want to hold off on unifying 𝜈 := Bool %1 -> A: instead, we want to accept
  the program with the more lenient subtype check

    Bool %Many -> A  ⩽  𝜈

  The general principle is: treat linear arrows %1 -> similar to foralls and
  constraint arrows =>, so that (UQL4) applies to them as well.
  See Note [Multiplicity in deep subsumption].

Sadly discarded design alternative
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It is very tempting to use `unifyType` rather than `qlUnify`, killing off the
latter.  (Extending `unifyType` slightly to allow it to unify an instantiation
variable with a polytype is easy.).  But I could not see how to make it work:

 * `unifyType` makes the types /equal/, and returns a coercion, and it is hard to
   marry that up with DeepSubsumption.  Absent deep subsumption, this approach
   might just work.

 * I considered making a wrapper for `uType`, which simply discards any deferred
   equality constraints.  But we can't do that: in a heterogeneous equality we might
   have unified a unification variable (alpha := ty |> co), where `co` is only bound
   by those constraints.
-}

{- *********************************************************************
*                                                                      *
                 tagToEnum#
*                                                                      *
********************************************************************* -}

{- Note [tagToEnum#]
~~~~~~~~~~~~~~~~~~~~
Nasty check to ensure that tagToEnum# is applied to a type that is an
enumeration TyCon.  It's crude, because it relies on our
knowing *now* that the type is ok, which in turn relies on the
eager-unification part of the type checker pushing enough information
here.  In theory the Right Thing to do is to have a new form of
constraint but I definitely cannot face that!  And it works ok as-is.

Here's are two cases that should fail
        f :: forall a. a
        f = tagToEnum# 0        -- Can't do tagToEnum# at a type variable

        g :: Int
        g = tagToEnum# 0        -- Int is not an enumeration

When data type families are involved it's a bit more complicated.
     data family F a
     data instance F [Int] = A | B | C
Then we want to generate something like
     tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int]
Usually that coercion is hidden inside the wrappers for
constructors of F [Int] but here we have to do it explicitly.

It's all grotesquely complicated.
-}

isTagToEnum :: HsExpr GhcTc -> Bool
isTagToEnum :: HsExpr GhcTc -> Bool
isTagToEnum (HsVar XVar GhcTc
_ (L SrcSpanAnnN
_ Id
fun_id)) = Id
fun_id Id -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
tagToEnumKey
isTagToEnum HsExpr GhcTc
_ = Bool
False

tcTagToEnum :: HsExpr GhcTc -> [HsExprArg 'TcpTc] -> TcRhoType
            -> TcM (HsExpr GhcTc)
-- tagToEnum# :: forall a. Int# -> a
-- See Note [tagToEnum#]   Urgh!
tcTagToEnum :: HsExpr GhcTc -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args TcType
res_ty
  | [HsExprArg 'TcpTc
val_arg] <- (HsExprArg 'TcpTc -> Bool)
-> [HsExprArg 'TcpTc] -> [HsExprArg 'TcpTc]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool)
-> (HsExprArg 'TcpTc -> Bool) -> HsExprArg 'TcpTc -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExprArg 'TcpTc -> Bool
forall {p :: TcPass}. HsExprArg p -> Bool
isHsValArg) [HsExprArg 'TcpTc]
tc_args
  = do { res_ty <- ZonkM TcType -> TcM TcType
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TcType -> TcM TcType) -> ZonkM TcType -> TcM TcType
forall a b. (a -> b) -> a -> b
$ TcType -> ZonkM TcType
zonkTcType TcType
res_ty

       -- Check that the type is algebraic
       ; case tcSplitTyConApp_maybe res_ty of {
           Maybe (TyCon, TcThetaType)
Nothing -> do { TcRnMessage -> TcRn ()
addErrTc (TcType -> TcRnMessage
TcRnTagToEnumUnspecifiedResTy TcType
res_ty)
                         ; TcM (HsExpr GhcTc)
vanilla_result } ;
           Just (TyCon
tc, TcThetaType
tc_args) ->

    do { -- Look through any type family
       ; fam_envs <- TcM FamInstEnvs
tcGetFamInstEnvs
       ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of {
           Maybe (TyCon, TcThetaType, TcCoercion)
Nothing -> do { TcType -> TyCon -> TcRn ()
check_enumeration TcType
res_ty TyCon
tc
                         ; TcM (HsExpr GhcTc)
vanilla_result } ;
           Just (TyCon
rep_tc, TcThetaType
rep_args, TcCoercion
coi) ->

    do { -- coi :: tc tc_args ~R rep_tc rep_args
         TcType -> TyCon -> TcRn ()
check_enumeration TcType
res_ty TyCon
rep_tc
       ; let rep_ty :: TcType
rep_ty  = TyCon -> TcThetaType -> TcType
mkTyConApp TyCon
rep_tc TcThetaType
rep_args
             tc_fun' :: HsExpr GhcTc
tc_fun' = HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap (TcType -> HsWrapper
WpTyApp TcType
rep_ty) HsExpr GhcTc
tc_fun
             df_wrap :: HsWrapper
df_wrap = TcCoercion -> HsWrapper
mkWpCastR (TcCoercion -> TcCoercion
mkSymCo TcCoercion
coi)
             tc_expr :: HsExpr GhcTc
tc_expr = HsExpr GhcTc -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps HsExpr GhcTc
tc_fun' [HsExprArg 'TcpTc
val_arg]
       ; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap HsWrapper
df_wrap HsExpr GhcTc
tc_expr) }}}}}

  | Bool
otherwise
  = TcRnMessage -> TcM (HsExpr GhcTc)
forall a. TcRnMessage -> TcRn a
failWithTc TcRnMessage
TcRnTagToEnumMissingValArg

  where
    vanilla_result :: TcM (HsExpr GhcTc)
vanilla_result = HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsExpr GhcTc -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args)

    check_enumeration :: TcType -> TyCon -> TcRn ()
check_enumeration TcType
ty' TyCon
tc
      | -- isTypeDataTyCon: see wrinkle (W1) in
        -- Note [Type data declarations] in GHC.Rename.Module
        TyCon -> Bool
isTypeDataTyCon TyCon
tc    = TcRnMessage -> TcRn ()
addErrTc (TcType -> TcRnMessage
TcRnTagToEnumResTyTypeData TcType
ty')
      | TyCon -> Bool
isEnumerationTyCon TyCon
tc = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Bool
otherwise             = TcRnMessage -> TcRn ()
addErrTc (TcType -> TcRnMessage
TcRnTagToEnumResTyNotAnEnum TcType
ty')

{- *********************************************************************
*                                                                      *
             Pragmas on expressions
*                                                                      *
********************************************************************* -}

tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag (HsPragSCC XSCC GhcRn
x1 StringLiteral
ann) = XSCC GhcTc -> StringLiteral -> HsPragE GhcTc
forall p. XSCC p -> StringLiteral -> HsPragE p
HsPragSCC XSCC GhcRn
XSCC GhcTc
x1 StringLiteral
ann