{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE MultiWayIf          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
{-# LANGUAGE TypeApplications #-} -- 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
       , tcInferSigma
       , tcExprPrag ) where

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

import GHC.Types.Var
import GHC.Builtin.Types ( multiplicityTy )
import GHC.Tc.Gen.Head
import Language.Haskell.Syntax.Basic
import GHC.Hs
import GHC.Tc.Errors.Types
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.Origin
import GHC.Tc.Utils.TcType as TcType
import GHC.Tc.Zonk.TcType
import GHC.Core.ConLike (ConLike(..))
import GHC.Core.DataCon (dataConConcreteTyVars)
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst (substTyWithInScope)
import GHC.Core.TyCo.FVs
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Types.Var.Set
import GHC.Builtin.PrimOps( tagToEnumKey )
import GHC.Builtin.Names
import GHC.Driver.DynFlags
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.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 GHC.Prelude

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

{- Note [Quick Look]
~~~~~~~~~~~~~~~~~~~~
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

* The "instantiation variables" of the paper are ordinary unification
  variables.  We keep track of which variables are instantiation variables
  by keeping a set Delta of instantiation variables.

* 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.

* When QL is done, we don't need to turn the un-filled-in
  instantiation variables into unification variables -- they
  already /are/ unification variables!  See also
  Note [Instantiation variables are short lived].

* 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
By the time QL is done, all filled-in occurrences of instantiation
variables have been zonked away (see "Crucial step" in tcValArgs),
and so the constraint /generator/ never subsequently sees a meta-type
variable filled in with a polytype -- a meta type variable stands
(only) for a monotype.  See Section 4.3 "Applications and instantiation"
of the paper.

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.
-}


{- *********************************************************************
*                                                                      *
              tcInferSigma
*                                                                      *
********************************************************************* -}

tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
-- Used only to implement :type; see GHC.Tc.Module.tcRnExpr
-- True  <=> instantiate -- return a rho-type
-- False <=> don't instantiate -- return a sigma-type
tcInferSigma :: Bool -> LHsExpr (GhcPass 'Renamed) -> TcM TcType
tcInferSigma Bool
inst (L SrcSpanAnnA
loc HsExpr (GhcPass 'Renamed)
rn_expr)
  = HsExpr (GhcPass 'Renamed) -> TcM TcType -> TcM TcType
forall a. HsExpr (GhcPass 'Renamed) -> TcRn a -> TcRn a
addExprCtxt HsExpr (GhcPass 'Renamed)
rn_expr (TcM TcType -> TcM TcType) -> TcM TcType -> TcM TcType
forall a b. (a -> b) -> a -> b
$
    SrcSpanAnnA -> TcM TcType -> TcM TcType
forall ann a. EpAnn ann -> TcRn a -> TcRn a
setSrcSpanA SrcSpanAnnA
loc     (TcM TcType -> TcM TcType) -> TcM TcType -> TcM TcType
forall a b. (a -> b) -> a -> b
$
    do { (fun :: (HsExpr (GhcPass 'Renamed), AppCtxt)
fun@(HsExpr (GhcPass 'Renamed)
rn_fun,AppCtxt
fun_ctxt), [HsExprArg 'TcpRn]
rn_args) <- HsExpr (GhcPass 'Renamed)
-> TcM ((HsExpr (GhcPass 'Renamed), AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr (GhcPass 'Renamed)
rn_expr
       ; Bool
do_ql <- HsExpr (GhcPass 'Renamed) -> TcM Bool
wantQuickLook HsExpr (GhcPass 'Renamed)
rn_fun
       ; (HsExpr GhcTc
tc_fun, TcType
fun_sigma) <- (HsExpr (GhcPass 'Renamed), AppCtxt) -> TcM (HsExpr GhcTc, TcType)
tcInferAppHead (HsExpr (GhcPass 'Renamed), AppCtxt)
fun
       ; (Delta
_delta, [HsExprArg 'TcpInst]
inst_args, TcType
app_res_sigma) <- Bool
-> Bool
-> (HsExpr GhcTc, AppCtxt)
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
tcInstFun Bool
do_ql Bool
inst (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt) TcType
fun_sigma [HsExprArg 'TcpRn]
rn_args
       ; [HsExprArg 'TcpTc]
_tc_args <- Bool -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
do_ql [HsExprArg 'TcpInst]
inst_args
       ; TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
app_res_sigma }

{- *********************************************************************
*                                                                      *
              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
      |  other_expr       -- Other expressions

When tcExpr sees something that starts an application chain (namely,
any of the constructors in 'app' or 'head'), 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.

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 tcInfer).

There is no special treatment for HsUnboundVar, 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 works like this:

1. Use splitHsApps, which peels off
     HsApp, HsTypeApp, HsPrag, HsPar
   returning the function in the corner and the arguments

   splitHsApps can deal with infix as well as prefix application,
   and returns a Rebuilder to re-assemble the application after
   typechecking.

   The "list of arguments" is [HsExprArg], described in Note [HsExprArg].
   in GHC.Tc.Gen.Head

2. Use 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

3. Use 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].

4. 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 5.

5. Use unifyResultType to match up the result type of the call
   with that expected by the context.  See Note [Unify with
   expected type before typechecking arguments]

6. Use tcValArgs to typecheck the value arguments

7. After a gruesome special case for tagToEnum, rebuild the result.


Some cases that /won't/ work:

1. 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!

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 unifyExpectedType
before tcValArgs.
-}

tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
-- See Note [tcApp: typechecking applications]
tcApp :: HsExpr (GhcPass 'Renamed) -> ExpRhoType -> TcM (HsExpr GhcTc)
tcApp HsExpr (GhcPass 'Renamed)
rn_expr ExpRhoType
exp_res_ty
  = do { (fun :: (HsExpr (GhcPass 'Renamed), AppCtxt)
fun@(HsExpr (GhcPass 'Renamed)
rn_fun, AppCtxt
fun_ctxt), [HsExprArg 'TcpRn]
rn_args) <- HsExpr (GhcPass 'Renamed)
-> TcM ((HsExpr (GhcPass 'Renamed), AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr (GhcPass 'Renamed)
rn_expr
       ; String -> SDoc -> TcRn ()
traceTc String
"tcApp {" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
           [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rn_expr:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr (GhcPass 'Renamed) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr (GhcPass 'Renamed)
rn_expr
                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rn_fun:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr (GhcPass 'Renamed) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr (GhcPass 'Renamed)
rn_fun
                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"fun_ctxt:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> AppCtxt -> SDoc
forall a. Outputable a => a -> SDoc
ppr AppCtxt
fun_ctxt
                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rn_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 ]

       ; (HsExpr GhcTc
tc_fun, TcType
fun_sigma) <- (HsExpr (GhcPass 'Renamed), AppCtxt) -> TcM (HsExpr GhcTc, TcType)
tcInferAppHead (HsExpr (GhcPass 'Renamed), AppCtxt)
fun

       -- Instantiate
       ; Bool
do_ql <- HsExpr (GhcPass 'Renamed) -> TcM Bool
wantQuickLook HsExpr (GhcPass 'Renamed)
rn_fun
       ; (Delta
delta, [HsExprArg 'TcpInst]
inst_args, TcType
app_res_rho) <- Bool
-> Bool
-> (HsExpr GhcTc, AppCtxt)
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
tcInstFun Bool
do_ql Bool
True (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt) TcType
fun_sigma [HsExprArg 'TcpRn]
rn_args

       -- Quick look at result
       ; TcType
app_res_rho <- if Bool
do_ql
                        then Delta -> TcType -> ExpRhoType -> TcM TcType
quickLookResultType Delta
delta TcType
app_res_rho ExpRhoType
exp_res_ty
                        else TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
app_res_rho

       -- Unify with expected type from the context
       -- See Note [Unify with expected type before typechecking arguments]
       --
       -- 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
       ; let  perhaps_add_res_ty_ctxt :: TcM HsWrapper -> TcM HsWrapper
perhaps_add_res_ty_ctxt TcM HsWrapper
thing_inside
                 | AppCtxt -> Bool
insideExpansion AppCtxt
fun_ctxt
                 = AppCtxt -> TcM HsWrapper -> TcM HsWrapper
forall a. AppCtxt -> TcM a -> TcM a
addHeadCtxt AppCtxt
fun_ctxt TcM HsWrapper
thing_inside
                 | Bool
otherwise
                 = HsExpr (GhcPass 'Renamed)
-> [HsExprArg 'TcpRn]
-> TcType
-> ExpRhoType
-> TcM HsWrapper
-> TcM HsWrapper
forall a.
HsExpr (GhcPass 'Renamed)
-> [HsExprArg 'TcpRn] -> TcType -> ExpRhoType -> TcM a -> TcM a
addFunResCtxt HsExpr (GhcPass 'Renamed)
rn_fun [HsExprArg 'TcpRn]
rn_args TcType
app_res_rho ExpRhoType
exp_res_ty (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
                   TcM HsWrapper
thing_inside

       -- Match up app_res_rho: the result type of rn_expr
       --     with exp_res_ty:  the expected result type
       ; Bool
do_ds <- Extension -> TcM Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DeepSubsumption
       ; HsWrapper
res_wrap <- TcM HsWrapper -> TcM HsWrapper
perhaps_add_res_ty_ctxt (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
            if Bool -> Bool
not Bool
do_ds
            then -- No deep subsumption
                 -- app_res_rho and exp_res_ty are both rho-types,
                 -- so with simple subsumption we can just unify them
                 -- No need to zonk; the unifier does that
                 do { TcCoercionN
co <- HsExpr (GhcPass 'Renamed)
-> TcType -> ExpRhoType -> TcM TcCoercionN
unifyExpectedType HsExpr (GhcPass 'Renamed)
rn_expr TcType
app_res_rho ExpRhoType
exp_res_ty
                    ; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> HsWrapper
mkWpCastN TcCoercionN
co) }

            else -- Deep subsumption
                 -- Even though both app_res_rho and exp_res_ty are rho-types,
                 -- they may have nested polymorphism, so if deep subsumption
                 -- is on we must call tcSubType.
                 -- Zonk app_res_rho first, because QL may have instantiated some
                 -- delta variables to polytypes, and tcSubType doesn't expect that
                 do { TcType
app_res_rho <- 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
$ Bool -> TcType -> ZonkM TcType
zonkQuickLook Bool
do_ql TcType
app_res_rho
                    ; HsExpr (GhcPass 'Renamed) -> TcType -> ExpRhoType -> TcM HsWrapper
tcSubTypeDS HsExpr (GhcPass 'Renamed)
rn_expr TcType
app_res_rho ExpRhoType
exp_res_ty }

       -- Typecheck the value arguments
       ; [HsExprArg 'TcpTc]
tc_args <- Bool -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
do_ql [HsExprArg 'TcpInst]
inst_args

       -- Reconstruct, with a special case for tagToEnum#.
       ; HsExpr GhcTc
tc_expr <-
          if HsExpr (GhcPass 'Renamed) -> Bool
isTagToEnum HsExpr (GhcPass 'Renamed)
rn_fun
          then HsExpr GhcTc
-> AppCtxt -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcTc
tc_fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
tc_args TcType
app_res_rho
          else do HsExpr GhcTc
-> AppCtxt -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
rebuildHsApps HsExpr GhcTc
tc_fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
tc_args TcType
app_res_rho

       ; DumpFlag -> TcRn () -> TcRn ()
forall gbl lcl. DumpFlag -> TcRnIf gbl lcl () -> TcRnIf gbl lcl ()
whenDOptM DumpFlag
Opt_D_dump_tc_trace (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         do { [HsExprArg 'TcpInst]
inst_args <- ZonkM [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpInst]
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpInst])
-> ZonkM [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpInst]
forall a b. (a -> b) -> a -> b
$ (HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst))
-> [HsExprArg 'TcpInst] -> ZonkM [HsExprArg 'TcpInst]
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 HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
zonkArg [HsExprArg 'TcpInst]
inst_args  -- Only when tracing
            ; String -> SDoc -> TcRn ()
traceTc String
"tcApp }" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rn_fun:"      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr (GhcPass 'Renamed) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr (GhcPass 'Renamed)
rn_fun
                                      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rn_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
"inst_args"    SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
brackets ((HsExprArg 'TcpInst -> SDoc) -> [HsExprArg 'TcpInst] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas HsExprArg 'TcpInst -> SDoc
pprHsExprArgTc [HsExprArg 'TcpInst]
inst_args)
                                      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"do_ql:  "     SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
do_ql
                                      , 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
"delta:      " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta
                                      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"app_res_rho:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
app_res_rho
                                      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"exp_res_ty:"  SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
exp_res_ty
                                      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rn_expr:"     SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr (GhcPass 'Renamed) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr (GhcPass 'Renamed)
rn_expr
                                      , 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
"tc_args:"     SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [HsExprArg 'TcpTc] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpTc]
tc_args
                                      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tc_expr:"     SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcTc
tc_expr ]) }

       -- Wrap the result
       ; 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
res_wrap HsExpr GhcTc
tc_expr) }

--------------------
wantQuickLook :: HsExpr GhcRn -> TcM Bool
wantQuickLook :: HsExpr (GhcPass 'Renamed) -> TcM Bool
wantQuickLook (HsVar XVar (GhcPass 'Renamed)
_ (L SrcSpanAnnN
_ 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 = Bool -> TcM Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
wantQuickLook HsExpr (GhcPass 'Renamed)
_                      = Extension -> TcM Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes

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

zonkQuickLook :: Bool -> TcType -> ZonkM TcType
-- After all Quick Look unifications are done, zonk to ensure that all
-- instantiation variables are substituted away
--
-- 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 type
--
-- In implementation terms this ensures that no unification variable
-- linger on that have been filled in with a polytype
zonkQuickLook :: Bool -> TcType -> ZonkM TcType
zonkQuickLook Bool
do_ql TcType
ty
  | Bool
do_ql     = TcType -> ZonkM TcType
zonkTcType TcType
ty
  | Bool
otherwise = TcType -> ZonkM TcType
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
ty

-- zonkArg is used *only* during debug-tracing, to make it easier to
-- see what is going on.  For that reason, it is not a full zonk: add
-- more if you need it.
zonkArg :: HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
zonkArg :: HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
zonkArg eva :: HsExprArg 'TcpInst
eva@(EValArg { eva_arg_ty :: forall (p :: TcPass). HsExprArg p -> XEVAType p
eva_arg_ty = Scaled TcType
m TcType
ty })
  = do { TcType
ty' <- TcType -> ZonkM TcType
zonkTcType TcType
ty
       ; HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsExprArg 'TcpInst
eva { eva_arg_ty = Scaled m ty' }) }
zonkArg HsExprArg 'TcpInst
arg = HsExprArg 'TcpInst -> ZonkM (HsExprArg 'TcpInst)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return HsExprArg 'TcpInst
arg



----------------

tcValArgs :: Bool                    -- Quick-look on?
          -> [HsExprArg 'TcpInst]    -- Actual argument
          -> TcM [HsExprArg 'TcpTc]  -- Resulting argument
tcValArgs :: Bool -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
do_ql [HsExprArg 'TcpInst]
args
  = (HsExprArg 'TcpInst
 -> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc))
-> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
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 HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
tc_arg [HsExprArg 'TcpInst]
args
  where
    tc_arg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpTc)
    tc_arg :: HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
tc_arg (EPrag AppCtxt
l HsPragE (GhcPass (XPass 'TcpInst))
p) = HsExprArg 'TcpTc
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppCtxt -> HsPragE (GhcPass (XPass 'TcpTc)) -> HsExprArg 'TcpTc
forall (p :: TcPass).
AppCtxt -> HsPragE (GhcPass (XPass p)) -> HsExprArg p
EPrag AppCtxt
l (HsPragE (GhcPass 'Renamed) -> HsPragE GhcTc
tcExprPrag HsPragE (GhcPass 'Renamed)
HsPragE (GhcPass (XPass 'TcpInst))
p))
    tc_arg (EWrap EWrap
w)   = HsExprArg 'TcpTc
-> IOEnv (Env TcGblEnv TcLclEnv) (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
w)
    tc_arg (ETypeArg AppCtxt
l LHsWcType (GhcPass 'Renamed)
hs_ty XETAType 'TcpInst
ty) = HsExprArg 'TcpTc
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppCtxt
-> LHsWcType (GhcPass 'Renamed)
-> XETAType 'TcpTc
-> HsExprArg 'TcpTc
forall (p :: TcPass).
AppCtxt
-> LHsWcType (GhcPass 'Renamed) -> XETAType p -> HsExprArg p
ETypeArg AppCtxt
l LHsWcType (GhcPass 'Renamed)
hs_ty XETAType 'TcpInst
XETAType 'TcpTc
ty)

    tc_arg eva :: HsExprArg 'TcpInst
eva@(EValArg { eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = EValArg 'TcpInst
arg, eva_arg_ty :: forall (p :: TcPass). HsExprArg p -> XEVAType p
eva_arg_ty = Scaled TcType
mult TcType
arg_ty
                        , eva_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
eva_ctxt = AppCtxt
ctxt })
      = do { -- Crucial step: expose QL results before checking 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]
             TcType
arg_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
$ Bool -> TcType -> ZonkM TcType
zonkQuickLook Bool
do_ql TcType
arg_ty

             -- Now check the argument
           ; GenLocated SrcSpanAnnA (HsExpr GhcTc)
arg' <- TcType
-> TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc))
-> TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc))
forall a. TcType -> TcM a -> TcM a
tcScalingUsage TcType
mult (TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc))
 -> TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc)))
-> TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc))
-> TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc))
forall a b. (a -> b) -> a -> b
$
                     do { String -> SDoc -> TcRn ()
traceTc String
"tcEValArg" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
                          [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ AppCtxt -> SDoc
forall a. Outputable a => a -> SDoc
ppr AppCtxt
ctxt
                               , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
arg_ty
                               , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> EValArg 'TcpInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr EValArg 'TcpInst
arg ]
                        ; AppCtxt -> EValArg 'TcpInst -> TcType -> TcM (LHsExpr GhcTc)
tcEValArg AppCtxt
ctxt EValArg 'TcpInst
arg TcType
arg_ty }

           ; HsExprArg 'TcpTc
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsExprArg 'TcpInst
eva { eva_arg    = ValArg arg'
                         , eva_arg_ty = Scaled mult arg_ty }) }

tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaTypeFRR -> TcM (LHsExpr GhcTc)
-- Typecheck one value argument of a function call
tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcType -> TcM (LHsExpr GhcTc)
tcEValArg AppCtxt
ctxt (ValArg larg :: LHsExpr (GhcPass (XPass 'TcpInst))
larg@(L SrcSpanAnnA
arg_loc HsExpr (GhcPass 'Renamed)
arg)) TcType
exp_arg_sigma
  = AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> TcM (LHsExpr GhcTc)
-> TcM (LHsExpr GhcTc)
forall a. AppCtxt -> LHsExpr (GhcPass 'Renamed) -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
LHsExpr (GhcPass (XPass 'TcpInst))
larg (TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc))
-> TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$
    do { HsExpr GhcTc
arg' <- HsExpr (GhcPass 'Renamed) -> ExpRhoType -> TcM (HsExpr GhcTc)
tcPolyExpr HsExpr (GhcPass 'Renamed)
arg (TcType -> ExpRhoType
mkCheckExpType TcType
exp_arg_sigma)
       ; GenLocated SrcSpanAnnA (HsExpr GhcTc)
-> TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsExpr GhcTc -> GenLocated SrcSpanAnnA (HsExpr GhcTc)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
arg_loc HsExpr GhcTc
arg') }

tcEValArg AppCtxt
ctxt (ValArgQL { va_expr :: EValArg 'TcpInst -> LHsExpr (GhcPass 'Renamed)
va_expr = larg :: LHsExpr (GhcPass 'Renamed)
larg@(L SrcSpanAnnA
arg_loc HsExpr (GhcPass 'Renamed)
_)
                         , va_fun :: EValArg 'TcpInst -> (HsExpr GhcTc, AppCtxt)
va_fun = (HsExpr GhcTc
inner_fun, AppCtxt
fun_ctxt)
                         , va_args :: EValArg 'TcpInst -> [HsExprArg 'TcpInst]
va_args = [HsExprArg 'TcpInst]
inner_args
                         , va_ty :: EValArg 'TcpInst -> TcType
va_ty = TcType
app_res_rho }) TcType
exp_arg_sigma
  = AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> TcM (LHsExpr GhcTc)
-> TcM (LHsExpr GhcTc)
forall a. AppCtxt -> LHsExpr (GhcPass 'Renamed) -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
larg (TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc))
-> TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$
    do { String -> SDoc -> TcRn ()
traceTc String
"tcEValArgQL {" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ HsExpr GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcTc
inner_fun SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [HsExprArg 'TcpInst] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpInst]
inner_args ])
       ; [HsExprArg 'TcpTc]
tc_args <- Bool -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
True [HsExprArg 'TcpInst]
inner_args

       ; TcCoercionN
co   <- Maybe TypedThing -> TcType -> TcType -> TcM TcCoercionN
unifyType Maybe TypedThing
forall a. Maybe a
Nothing TcType
app_res_rho TcType
exp_arg_sigma
       ; HsExpr GhcTc
arg' <- TcCoercionN -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrapCo TcCoercionN
co (HsExpr GhcTc -> HsExpr GhcTc)
-> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HsExpr GhcTc
-> AppCtxt -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
rebuildHsApps HsExpr GhcTc
inner_fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
tc_args TcType
app_res_rho
       ; String -> SDoc -> TcRn ()
traceTc String
"tcEValArgQL }" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
           [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inner_fun:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcTc
inner_fun
                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"app_res_rho:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
app_res_rho
                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"exp_arg_sigma:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
exp_arg_sigma ]
       ; GenLocated SrcSpanAnnA (HsExpr GhcTc)
-> TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsExpr GhcTc -> GenLocated SrcSpanAnnA (HsExpr GhcTc)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
arg_loc HsExpr GhcTc
arg') }

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

type Delta = TcTyVarSet   -- Set of instantiation variables,
                          --   written \kappa in the QL paper
                          -- Just a set of ordinary unification variables,
                          --   but ones that QL may fill in with polytypes

tcInstFun :: Bool   -- True  <=> Do quick-look
          -> Bool   -- False <=> Instantiate only /inferred/ variables at the end
                    --           so may return a sigma-type
                    -- True  <=> Instantiate all type variables at the end:
                    --           return a rho-type
                    -- The /only/ call site that passes in False is the one
                    --    in tcInferSigma, which is used only to implement :type
                    -- Otherwise we do eager instantiation; in Fig 5 of the paper
                    --    |-inst returns a rho-type
          -> (HsExpr GhcTc, AppCtxt)
                -- ^ For error messages and to retrieve concreteness information
                -- of the function
          -> TcSigmaType -> [HsExprArg 'TcpRn]
          -> TcM ( Delta
                 , [HsExprArg 'TcpInst]
                 , TcSigmaType )
-- This 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 :: Bool
-> Bool
-> (HsExpr GhcTc, AppCtxt)
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
tcInstFun Bool
do_ql Bool
inst_final (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt) 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
"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
"fun_ctxt" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> AppCtxt -> SDoc
forall a. Outputable a => a -> SDoc
ppr AppCtxt
fun_ctxt
                                   , 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
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
do_ql ])
       ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go Delta
emptyVarSet [] [] TcType
fun_sigma [HsExprArg 'TcpRn]
rn_args }
  where
    fun_orig :: CtOrigin
fun_orig
      | VAExpansion (OrigStmt{}) SrcSpan
_ SrcSpan
_ <- AppCtxt
fun_ctxt
      = CtOrigin
DoOrigin
      | VAExpansion (OrigPat LPat (GhcPass 'Renamed)
pat) SrcSpan
_ SrcSpan
_ <- AppCtxt
fun_ctxt
      = LPat (GhcPass 'Renamed) -> CtOrigin
DoPatOrigin LPat (GhcPass 'Renamed)
pat
      | VAExpansion (OrigExpr HsExpr (GhcPass 'Renamed)
e) SrcSpan
_ SrcSpan
_ <- AppCtxt
fun_ctxt
      = HsExpr (GhcPass 'Renamed) -> CtOrigin
exprCtOrigin HsExpr (GhcPass 'Renamed)
e
      | VACall HsExpr (GhcPass 'Renamed)
e Int
_ SrcSpan
_ <- AppCtxt
fun_ctxt
      = HsExpr (GhcPass 'Renamed) -> CtOrigin
exprCtOrigin HsExpr (GhcPass 'Renamed)
e

    -- These are the type variables which must be instantiated to concrete
    -- types. See Note [Representation-polymorphic Ids with no binding]
    -- in GHC.Tc.Gen.Head.
    fun_conc_tvs :: ConcreteTyVars
fun_conc_tvs
      | HsVar XVar GhcTc
_ (L SrcSpanAnnN
_ TcTyVar
fun_id) <- HsExpr GhcTc
tc_fun
      = TcTyVar -> ConcreteTyVars
idConcreteTvs TcTyVar
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) [TcTyVar]
_ [Scaled TcType]
_) <- 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 (id :: TcPass). HsExprArg id -> 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
          HsUnboundVar {} -> Bool
True
          HsExpr GhcTc
_               -> Bool
False

    inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
    -- True <=> instantiate a tyvar with 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
                -- Using `const False` for `:type` avoids
                -- `forall {r1} (a :: TYPE r1) {r2} (b :: TYPE r2). a -> b`
                -- turning into `forall a {r2} (b :: TYPE r2). a -> b`.
                -- See #21088.
    inst_fun (EValArg {} : [HsExprArg 'TcpRn]
_) = ForAllTyFlag -> Bool
isInvisibleForAllTyFlag
    inst_fun [HsExprArg 'TcpRn]
_                = ForAllTyFlag -> Bool
isInferredForAllTyFlag

    -----------
    go, go1 :: Delta
            -> [HsExprArg 'TcpInst]     -- Accumulator, reversed
            -> [Scaled TcSigmaTypeFRR]  -- Value args to which applied so far
            -> TcSigmaType -> [HsExprArg 'TcpRn]
            -> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)

    -- go: If fun_ty=kappa, look it up in Theta
    go :: Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty [HsExprArg 'TcpRn]
args
      | Just TcTyVar
kappa <- TcType -> Maybe TcTyVar
getTyVar_maybe TcType
fun_ty
      , TcTyVar
kappa TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta
      = do { MetaDetails
cts <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
kappa
           ; case MetaDetails
cts of
                Indirect TcType
fun_ty' -> Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go  Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty' [HsExprArg 'TcpRn]
args
                MetaDetails
Flexi            -> Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty  [HsExprArg 'TcpRn]
args }
     | Bool
otherwise
     = Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far 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 :: Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far 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]
      = Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty [HsExprArg 'TcpRn]
rest_args

    -- Rule IALL from Fig 4 of the QL paper
    -- Instantiate invisible foralls and dictionaries.
    -- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty [HsExprArg 'TcpRn]
args
      | ([TcTyVar]
tvs,   TcType
body1) <- (ForAllTyFlag -> Bool) -> TcType -> ([TcTyVar], TcType)
tcSplitSomeForAllTyVars ([HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
inst_fun [HsExprArg 'TcpRn]
args) TcType
fun_ty
      , (ThetaType
theta, TcType
body2) <- if [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
inst_fun [HsExprArg 'TcpRn]
args ForAllTyFlag
Inferred
                          then TcType -> (ThetaType, 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
      , Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
      = do { ([TcTyVar]
inst_tvs, HsWrapper
wrap, TcType
fun_rho) <-
                -- addHeadCtxt: important for the class constraints
                -- that may be emitted from instantiating fun_sigma
                AppCtxt
-> TcM ([TcTyVar], HsWrapper, TcType)
-> TcM ([TcTyVar], HsWrapper, TcType)
forall a. AppCtxt -> TcM a -> TcM a
addHeadCtxt AppCtxt
fun_ctxt (TcM ([TcTyVar], HsWrapper, TcType)
 -> TcM ([TcTyVar], HsWrapper, TcType))
-> TcM ([TcTyVar], HsWrapper, TcType)
-> TcM ([TcTyVar], HsWrapper, TcType)
forall a b. (a -> b) -> a -> b
$
                CtOrigin
-> ConcreteTyVars
-> [TcTyVar]
-> ThetaType
-> TcType
-> TcM ([TcTyVar], HsWrapper, TcType)
instantiateSigma CtOrigin
fun_orig ConcreteTyVars
fun_conc_tvs [TcTyVar]
tvs ThetaType
theta TcType
body2
                  -- See Note [Representation-polymorphism checking built-ins]
                  -- in GHC.Tc.Gen.Head.
                  -- 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.

           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go (Delta
delta Delta -> [TcTyVar] -> Delta
`extendVarSetList` [TcTyVar]
inst_tvs)
                (HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall (p :: TcPass). HsWrapper -> [HsExprArg p] -> [HsExprArg p]
addArgWrap HsWrapper
wrap [HsExprArg 'TcpInst]
acc) [Scaled TcType]
so_far TcType
fun_rho [HsExprArg 'TcpRn]
args }
                -- Going around again means we deal easily with
                -- nested  forall a. Eq a => forall b. Show b => blah

    -- Rule ITVDQ from the GHC Proposal #281
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty ((EValArg { eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = ValArg 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 (Delta, [HsExprArg 'TcpInst], TcType)
-> TcM (Delta, [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 (GhcPass 'Renamed)) -> SDoc
forall a. Outputable a => a -> SDoc
ppr LHsExpr (GhcPass (XPass 'TcpRn))
GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
arg) (TcM (Delta, [HsExprArg 'TcpInst], TcType)
 -> TcM (Delta, [HsExprArg 'TcpInst], TcType))
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
-> TcM (Delta, [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 { (TcType
ty_arg, TcType
inst_body) <- ConcreteTyVars
-> (TyVarBinder, TcType)
-> LHsExpr (GhcPass 'Renamed)
-> TcM (TcType, TcType)
tcVDQ ConcreteTyVars
fun_conc_tvs (TyVarBinder
tvb, TcType
body) LHsExpr (GhcPass 'Renamed)
LHsExpr (GhcPass (XPass 'TcpRn))
arg
           ; let wrap :: HsWrapper
wrap = ThetaType -> HsWrapper
mkWpTyApps [TcType
ty_arg]
           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go Delta
delta (HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall (p :: TcPass). HsWrapper -> [HsExprArg p] -> [HsExprArg p]
addArgWrap HsWrapper
wrap [HsExprArg 'TcpInst]
acc) [Scaled TcType]
so_far TcType
inst_body [HsExprArg 'TcpRn]
rest_args }

    -- Rule IRESULT from Fig 4 of the QL paper
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
_ TcType
fun_ty []
       = do { String -> SDoc -> TcRn ()
traceTc String
"tcInstFun:ret" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
fun_ty)
            ; (Delta, [HsExprArg 'TcpInst], TcType)
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. [a] -> [a]
reverse [HsExprArg 'TcpInst]
acc, TcType
fun_ty) }

    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty (EWrap EWrap
w : [HsExprArg 'TcpRn]
args)
      = Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go1 Delta
delta (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) [Scaled TcType]
so_far TcType
fun_ty [HsExprArg 'TcpRn]
args

    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty (EPrag AppCtxt
sp HsPragE (GhcPass (XPass 'TcpRn))
prag : [HsExprArg 'TcpRn]
args)
      = Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go1 Delta
delta (AppCtxt -> HsPragE (GhcPass (XPass 'TcpInst)) -> HsExprArg 'TcpInst
forall (p :: TcPass).
AppCtxt -> HsPragE (GhcPass (XPass p)) -> HsExprArg p
EPrag AppCtxt
sp HsPragE (GhcPass (XPass 'TcpRn))
HsPragE (GhcPass (XPass 'TcpInst))
prag HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) [Scaled TcType]
so_far TcType
fun_ty [HsExprArg 'TcpRn]
args

    -- Rule ITYARG from Fig 4 of the QL paper
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty ( ETypeArg { eva_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
eva_ctxt = AppCtxt
ctxt, eva_hs_ty :: forall (p :: TcPass). HsExprArg p -> LHsWcType (GhcPass 'Renamed)
eva_hs_ty = LHsWcType (GhcPass 'Renamed)
hs_ty }
                                : [HsExprArg 'TcpRn]
rest_args )
      = do { (TcType
ty_arg, TcType
inst_ty) <- ConcreteTyVars
-> TcType -> LHsWcType (GhcPass 'Renamed) -> TcM (TcType, TcType)
tcVTA ConcreteTyVars
fun_conc_tvs TcType
fun_ty LHsWcType (GhcPass 'Renamed)
hs_ty
           ; let arg' :: HsExprArg 'TcpInst
arg' = ETypeArg { eva_ctxt :: AppCtxt
eva_ctxt = AppCtxt
ctxt, eva_hs_ty :: LHsWcType (GhcPass 'Renamed)
eva_hs_ty = LHsWcType (GhcPass 'Renamed)
hs_ty, eva_ty :: XETAType 'TcpInst
eva_ty = TcType
XETAType 'TcpInst
ty_arg }
           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go Delta
delta (HsExprArg 'TcpInst
arg' HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) [Scaled TcType]
so_far TcType
inst_ty [HsExprArg 'TcpRn]
rest_args }

    -- Rule IVAR from Fig 4 of the QL paper:
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty args :: [HsExprArg 'TcpRn]
args@(EValArg {} : [HsExprArg 'TcpRn]
_)
      | Just TcTyVar
kappa <- TcType -> Maybe TcTyVar
getTyVar_maybe TcType
fun_ty
      , TcTyVar
kappa TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta
      = -- 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.
        --   - We need the freshly allocated unification variables, to extend
        --     delta with.
        -- It's easier just to do the job directly here.
        do { let val_args :: [EValArg 'TcpRn]
val_args       = [HsExprArg 'TcpRn] -> [EValArg 'TcpRn]
forall (id :: TcPass). [HsExprArg id] -> [EValArg id]
leadingValArgs [HsExprArg 'TcpRn]
args
                 val_args_count :: Int
val_args_count = [EValArg 'TcpRn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [EValArg 'TcpRn]
val_args

            -- Create metavariables for the arguments. Following matchActualFunTy,
            -- we create nu_i :: TYPE kappa_i[conc], ensuring that the arguments
            -- have concrete runtime representations.
            -- When we come to unify the nus (in qlUnify), we will call
            -- unifyKind on the kinds. This will do the right thing, even though
            -- we are manually filling in the nu metavariables.
                 new_arg_tv :: EValArg 'TcpRn -> Int -> TcM TcTyVar
new_arg_tv (ValArg (L SrcSpanAnnA
_ HsExpr (GhcPass 'Renamed)
arg)) Int
i =
                   FixedRuntimeRepContext -> TcM TcTyVar
newOpenFlexiFRRTyVar (FixedRuntimeRepContext -> TcM TcTyVar)
-> FixedRuntimeRepContext -> TcM TcTyVar
forall a b. (a -> b) -> a -> b
$
                   ExpectedFunTyOrigin -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy (TypedThing -> HsExpr (GhcPass 'Renamed) -> ExpectedFunTyOrigin
forall (p :: Pass).
Outputable (HsExpr (GhcPass p)) =>
TypedThing -> HsExpr (GhcPass p) -> ExpectedFunTyOrigin
ExpectedFunTyArg (HsExpr GhcTc -> TypedThing
HsExprTcThing HsExpr GhcTc
tc_fun) HsExpr (GhcPass 'Renamed)
arg) Int
i
           ; [TcTyVar]
arg_nus <- (EValArg 'TcpRn -> Int -> TcM TcTyVar)
-> [EValArg 'TcpRn]
-> [Int]
-> IOEnv (Env TcGblEnv TcLclEnv) [TcTyVar]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM EValArg 'TcpRn -> Int -> TcM TcTyVar
new_arg_tv
                          [EValArg 'TcpRn]
val_args
                          [[Scaled TcType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Scaled TcType]
so_far Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 ..]
             -- We need variables for multiplicity (#18731)
             -- Otherwise, 'undefined x' wouldn't be linear in x
           ; ThetaType
mults   <- Int -> TcM TcType -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
val_args_count (TcType -> TcM TcType
newFlexiTyVarTy TcType
multiplicityTy)
           ; TcTyVar
res_nu  <- TcM TcTyVar
newOpenFlexiTyVar
           ; TcCoercionN
kind_co <- Maybe TypedThing -> TcType -> TcType -> TcM TcCoercionN
unifyKind Maybe TypedThing
forall a. Maybe a
Nothing TcType
liftedTypeKind (TcTyVar -> TcType
tyVarKind TcTyVar
kappa)
           ; let delta' :: Delta
delta'  = Delta
delta Delta -> [TcTyVar] -> Delta
`extendVarSetList` (TcTyVar
res_nuTcTyVar -> [TcTyVar] -> [TcTyVar]
forall a. a -> [a] -> [a]
:[TcTyVar]
arg_nus)
                 arg_tys :: ThetaType
arg_tys = [TcTyVar] -> ThetaType
mkTyVarTys [TcTyVar]
arg_nus
                 res_ty :: TcType
res_ty  = TcTyVar -> TcType
mkTyVarTy TcTyVar
res_nu
                 fun_ty' :: TcType
fun_ty' = [Scaled TcType] -> TcType -> TcType
HasDebugCallStack => [Scaled TcType] -> TcType -> TcType
mkScaledFunTys (String
-> (TcType -> TcType -> Scaled TcType)
-> ThetaType
-> ThetaType
-> [Scaled TcType]
forall a b c.
HasDebugCallStack =>
String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"tcInstFun" TcType -> TcType -> Scaled TcType
forall a. TcType -> a -> Scaled a
mkScaled ThetaType
mults ThetaType
arg_tys) TcType
res_ty
                 co_wrap :: HsWrapper
co_wrap = TcCoercionN -> HsWrapper
mkWpCastN (Role -> TcType -> TcCoercionN -> TcCoercionN
mkGReflLeftCo Role
Nominal TcType
fun_ty' TcCoercionN
kind_co)
                 acc' :: [HsExprArg 'TcpInst]
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'
           ; ZonkM () -> TcRn ()
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM () -> TcRn ()) -> ZonkM () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => TcTyVar -> TcType -> ZonkM ()
TcTyVar -> TcType -> ZonkM ()
writeMetaTyVar TcTyVar
kappa (TcType -> TcCoercionN -> TcType
mkCastTy TcType
fun_ty' TcCoercionN
kind_co)
                 -- kappa is uninstantiated ('go' already checked that)
           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go Delta
delta' [HsExprArg 'TcpInst]
acc' [Scaled TcType]
so_far TcType
fun_ty' [HsExprArg 'TcpRn]
args }

    -- Rule IARG from Fig 4 of the QL paper:
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcType]
so_far TcType
fun_ty
        (eva :: HsExprArg 'TcpRn
eva@(EValArg { eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = ValArg LHsExpr (GhcPass (XPass 'TcpRn))
arg, eva_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
eva_ctxt = AppCtxt
ctxt }) : [HsExprArg 'TcpRn]
rest_args)
      = do { let herald :: ExpectedFunTyOrigin
herald = case AppCtxt
fun_ctxt of
                             VAExpansion (OrigStmt{}) SrcSpan
_ SrcSpan
_ -> CtOrigin -> HsExpr GhcTc -> ExpectedFunTyOrigin
forall (p :: Pass).
OutputableBndrId p =>
CtOrigin -> HsExpr (GhcPass p) -> ExpectedFunTyOrigin
ExpectedFunTySyntaxOp CtOrigin
DoOrigin HsExpr GhcTc
tc_fun
                             AppCtxt
_ ->  TypedThing -> HsExpr (GhcPass 'Renamed) -> ExpectedFunTyOrigin
forall (p :: Pass).
Outputable (HsExpr (GhcPass p)) =>
TypedThing -> HsExpr (GhcPass p) -> ExpectedFunTyOrigin
ExpectedFunTyArg (HsExpr GhcTc -> TypedThing
HsExprTcThing HsExpr GhcTc
tc_fun) (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
-> HsExpr (GhcPass 'Renamed)
forall l e. GenLocated l e -> e
unLoc LHsExpr (GhcPass (XPass 'TcpRn))
GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
arg)
           ; (HsWrapper
wrap, Scaled TcType
arg_ty, TcType
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).
                ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Int, TcType)
-> TcType
-> TcM (HsWrapper, Scaled TcType, TcType)
matchActualFunTy ExpectedFunTyOrigin
herald
                  (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

           ; (Delta
delta', EValArg 'TcpInst
arg') <- if Bool
do_ql
                               then AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> TcM (Delta, EValArg 'TcpInst)
-> TcM (Delta, EValArg 'TcpInst)
forall a. AppCtxt -> LHsExpr (GhcPass 'Renamed) -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
LHsExpr (GhcPass (XPass 'TcpRn))
arg (TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst))
-> TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a b. (a -> b) -> a -> b
$
                                    -- Context needed for constraints
                                    -- generated by calls in arg
                                    Delta
-> LHsExpr (GhcPass 'Renamed)
-> Scaled TcType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg Delta
delta LHsExpr (GhcPass 'Renamed)
LHsExpr (GhcPass (XPass 'TcpRn))
arg Scaled TcType
arg_ty
                               else (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, LHsExpr (GhcPass (XPass 'TcpInst)) -> EValArg 'TcpInst
forall (p :: TcPass). LHsExpr (GhcPass (XPass p)) -> EValArg p
ValArg LHsExpr (GhcPass (XPass 'TcpRn))
LHsExpr (GhcPass (XPass 'TcpInst))
arg)
           ; let acc' :: [HsExprArg 'TcpInst]
acc' = HsExprArg 'TcpRn
eva { eva_arg = arg', eva_arg_ty = arg_ty }
                       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 HsWrapper
wrap [HsExprArg 'TcpInst]
acc
           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcType]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
go Delta
delta' [HsExprArg 'TcpInst]
acc' (Scaled TcType
arg_tyScaled TcType -> [Scaled TcType] -> [Scaled TcType]
forall a. a -> [a] -> [a]
:[Scaled TcType]
so_far) TcType
res_ty [HsExprArg 'TcpRn]
rest_args }

-- 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{ eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = ValArg (L SrcSpanAnnA
_ HsExpr (GhcPass 'Renamed)
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 (GhcPass 'Renamed) -> HsExpr (GhcPass 'Renamed)
forall (p :: Pass). HsExpr (GhcPass p) -> HsExpr (GhcPass p)
stripParensHsExpr HsExpr (GhcPass 'Renamed)
e of
    HsEmbTy XEmbTy (GhcPass 'Renamed)
_ LHsWcType (NoGhcTc (GhcPass 'Renamed))
_ -> Bool
True
    HsExpr (GhcPass 'Renamed)
_           -> Bool
False
looks_like_type_arg HsExprArg 'TcpRn
_ = Bool
False

addArgCtxt :: AppCtxt -> LHsExpr GhcRn
           -> TcM a -> TcM a
-- There are four cases:
-- 1. In the normal case, we add an informative context
--          "In the third argument of f, namely blah"
-- 2. If we are deep inside generated code (`isGeneratedCode` is `True`)
--    or if all or part of this particular application is an expansion
--    `VAExpansion`, just use the less-informative context
--          "In the expression: arg"
--   Unless the arg is also a generated thing, in which case do nothing.
--   See Note [Rebindable syntax and XXExprGhcRn] in GHC.Hs.Expr
-- 3. We are in an expanded `do`-block's non-bind statement
--    we simply add the statement context
--       "In the statement of the `do`-block .."
-- 4. We are in an expanded do block's bind statement
--    a. Then either we are typechecking the first argument of the bind which is user located
--       so we set the location to be that of the argument
--    b. Or, we are typechecking the second argument which would be a generated lambda
--       so we set the location to be whatever the location in the context is
--  See Note [Expanding HsDo with XXExprGhcRn] in GHC.Tc.Gen.Do
-- For future: we need a cleaner way of doing this bit of adding the right error context.
-- There is a delicate dance of looking at source locations and reconstructing
-- whether the piece of code is a `do`-expanded code or some other expanded code.
addArgCtxt :: forall a. AppCtxt -> LHsExpr (GhcPass 'Renamed) -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt (L SrcSpanAnnA
arg_loc HsExpr (GhcPass 'Renamed)
arg) TcM a
thing_inside
  = do { Bool
in_generated_code <- TcM Bool
inGeneratedCode
       ; case AppCtxt
ctxt of
           VACall HsExpr (GhcPass 'Renamed)
fun Int
arg_no SrcSpan
_ | Bool -> Bool
not Bool
in_generated_code
             -> do 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
$
                     SDoc -> TcM a -> TcM a
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (HsExpr (GhcPass 'Renamed)
-> HsExpr (GhcPass 'Renamed) -> Int -> SDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> SDoc
funAppCtxt HsExpr (GhcPass 'Renamed)
fun HsExpr (GhcPass 'Renamed)
arg Int
arg_no) (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                     TcM a
thing_inside

           VAExpansion (OrigStmt (L SrcSpanAnnA
_ stmt :: StmtLR
  (GhcPass 'Renamed)
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed)))
stmt@(BindStmt {}))) SrcSpan
_ SrcSpan
loc
             | SrcSpan -> Bool
isGeneratedSrcSpan (SrcSpanAnnA -> SrcSpan
forall a. HasLoc a => a -> SrcSpan
locA SrcSpanAnnA
arg_loc) -- This arg is the second argument to generated (>>=)
             -> SrcSpan -> TcM a -> TcM a
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                  ExprStmt (GhcPass 'Renamed) -> TcM a -> TcM a
forall a. ExprStmt (GhcPass 'Renamed) -> TcRn a -> TcRn a
addStmtCtxt ExprStmt (GhcPass 'Renamed)
StmtLR
  (GhcPass 'Renamed)
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed)))
stmt (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                  TcM a
thing_inside
             | Bool
otherwise                        -- This arg is the first argument to generated (>>=)
             -> 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
$
                  ExprStmt (GhcPass 'Renamed) -> TcM a -> TcM a
forall a. ExprStmt (GhcPass 'Renamed) -> TcRn a -> TcRn a
addStmtCtxt ExprStmt (GhcPass 'Renamed)
StmtLR
  (GhcPass 'Renamed)
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed)))
stmt (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                  TcM a
thing_inside
           VAExpansion (OrigStmt (L SrcSpanAnnA
loc StmtLR
  (GhcPass 'Renamed)
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed)))
stmt)) SrcSpan
_ SrcSpan
_
             -> SrcSpanAnnA -> TcM a -> TcM a
forall ann a. EpAnn ann -> TcRn a -> TcRn a
setSrcSpanA SrcSpanAnnA
loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                  ExprStmt (GhcPass 'Renamed) -> TcM a -> TcM a
forall a. ExprStmt (GhcPass 'Renamed) -> TcRn a -> TcRn a
addStmtCtxt ExprStmt (GhcPass 'Renamed)
StmtLR
  (GhcPass 'Renamed)
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed)))
stmt (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                  TcM a
thing_inside

           AppCtxt
_ -> 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 (GhcPass 'Renamed) -> TcM a -> TcM a
forall a. HsExpr (GhcPass 'Renamed) -> TcRn a -> TcRn a
addExprCtxt HsExpr (GhcPass 'Renamed)
arg     (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$  -- Auto-suppressed if arg_loc is generated
                  TcM a
thing_inside }

{- *********************************************************************
*                                                                      *
              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.Gen.Head.
      -> 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 (GhcPass 'Renamed) -> TcM (TcType, TcType)
tcVTA ConcreteTyVars
conc_tvs TcType
fun_ty LHsWcType (GhcPass 'Renamed)
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 (GhcPass 'Renamed)
-> TcM (TcType, TcType)
tc_inst_forall_arg ConcreteTyVars
conc_tvs (TyVarBinder
tvb, TcType
inner_ty) LHsWcType (GhcPass 'Renamed)
hs_ty }

  | Bool
otherwise
  = do { (TidyEnv
_, TcType
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
       ; TcRnMessage -> TcM (TcType, TcType)
forall a. TcRnMessage -> TcRn a
failWith (TcRnMessage -> TcM (TcType, TcType))
-> TcRnMessage -> TcM (TcType, TcType)
forall a b. (a -> b) -> a -> b
$ TcType -> LHsWcType (GhcPass 'Renamed) -> TcRnMessage
TcRnInvalidTypeApplication TcType
fun_ty LHsWcType (GhcPass 'Renamed)
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 (GhcPass 'Renamed)
-> TcM (TcType, TcType)
tcVDQ ConcreteTyVars
conc_tvs (TyVarBinder
tvb, TcType
inner_ty) LHsExpr (GhcPass 'Renamed)
arg
  = do { HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
hs_wc_ty <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsWcType (GhcPass 'Renamed))
expr_to_type LHsExpr (GhcPass 'Renamed)
arg
       ; ConcreteTyVars
-> (TyVarBinder, TcType)
-> LHsWcType (GhcPass 'Renamed)
-> TcM (TcType, TcType)
tc_inst_forall_arg ConcreteTyVars
conc_tvs (TyVarBinder
tvb, TcType
inner_ty) LHsWcType (GhcPass 'Renamed)
HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
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 (GhcPass 'Renamed) -> TcM (LHsWcType (GhcPass 'Renamed))
expr_to_type LHsExpr (GhcPass 'Renamed)
earg =
  case LHsExpr (GhcPass 'Renamed) -> LHsExpr (GhcPass 'Renamed)
forall (p :: Pass). LHsExpr (GhcPass p) -> LHsExpr (GhcPass p)
stripParensLHsExpr LHsExpr (GhcPass 'Renamed)
earg of
    L SrcSpanAnnA
_ (HsEmbTy XEmbTy (GhcPass 'Renamed)
_ LHsWcType (NoGhcTc (GhcPass 'Renamed))
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
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsWildCardBndrs
        (GhcPass 'Renamed)
        (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return LHsWcType (NoGhcTc (GhcPass 'Renamed))
HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
hs_ty
    LHsExpr (GhcPass 'Renamed)
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
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> HsWildCardBndrs
     (GhcPass 'Renamed)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall pass thing.
XHsWC pass thing -> thing -> HsWildCardBndrs pass thing
HsWC [] (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
 -> HsWildCardBndrs
      (GhcPass 'Renamed)
      (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsWildCardBndrs
        (GhcPass 'Renamed)
        (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
e
  where
    go :: LHsExpr GhcRn -> TcM (LHsType GhcRn)
    go :: LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go (L SrcSpanAnnA
_ (HsEmbTy XEmbTy (GhcPass 'Renamed)
_ LHsWcType (NoGhcTc (GhcPass 'Renamed))
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
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall t. HsWildCardBndrs (GhcPass 'Renamed) t -> TcM t
unwrap_wc LHsWcType (NoGhcTc (GhcPass 'Renamed))
HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
t
    go (L SrcSpanAnnA
l (HsVar XVar (GhcPass 'Renamed)
_ LIdP (GhcPass 'Renamed)
lname)) =
      -- as per #281: variables and constructors (regardless of their namespace)
      -- are mapped directly, without modification.
      GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XTyVar (GhcPass 'Renamed)
-> PromotionFlag
-> LIdP (GhcPass 'Renamed)
-> HsType (GhcPass 'Renamed)
forall pass.
XTyVar pass -> PromotionFlag -> LIdP pass -> HsType pass
HsTyVar [AddEpAnn]
XTyVar (GhcPass 'Renamed)
forall a. NoAnn a => a
noAnn PromotionFlag
NotPromoted LIdP (GhcPass 'Renamed)
lname))
    go (L SrcSpanAnnA
l (HsApp XApp (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
lhs LHsExpr (GhcPass 'Renamed)
rhs)) =
      do { GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
lhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
lhs
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
rhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
rhs
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XAppTy (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> HsType (GhcPass 'Renamed)
forall pass.
XAppTy pass -> LHsType pass -> LHsType pass -> HsType pass
HsAppTy XAppTy (GhcPass 'Renamed)
NoExtField
noExtField LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
lhs' LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
rhs')) }
    go (L SrcSpanAnnA
l (HsAppType XAppTypeE (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
lhs LHsWcType (NoGhcTc (GhcPass 'Renamed))
rhs)) =
      do { GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
lhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
lhs
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
rhs' <- HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall t. HsWildCardBndrs (GhcPass 'Renamed) t -> TcM t
unwrap_wc LHsWcType (NoGhcTc (GhcPass 'Renamed))
HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
rhs
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XAppKindTy (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> HsType (GhcPass 'Renamed)
forall pass.
XAppKindTy pass -> LHsType pass -> LHsType pass -> HsType pass
HsAppKindTy XAppKindTy (GhcPass 'Renamed)
NoExtField
noExtField LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
lhs' LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
rhs')) }
    go (L SrcSpanAnnA
l e :: HsExpr (GhcPass 'Renamed)
e@(OpApp XOpApp (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
lhs LHsExpr (GhcPass 'Renamed)
op LHsExpr (GhcPass 'Renamed)
rhs)) =
      do { GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
lhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
lhs
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
op'  <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
op
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
rhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
rhs
         ; LIdP (GhcPass 'Renamed)
op_id <- GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv (Env TcGblEnv TcLclEnv) (LIdP (GhcPass 'Renamed))
unwrap_op_tv GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
op'
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XOpTy (GhcPass 'Renamed)
-> PromotionFlag
-> LHsType (GhcPass 'Renamed)
-> LIdP (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> HsType (GhcPass 'Renamed)
forall pass.
XOpTy pass
-> PromotionFlag
-> LHsType pass
-> LIdP pass
-> LHsType pass
-> HsType pass
HsOpTy [AddEpAnn]
XOpTy (GhcPass 'Renamed)
forall a. NoAnn a => a
noAnn PromotionFlag
NotPromoted LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
lhs' LIdP (GhcPass 'Renamed)
op_id LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
rhs')) }
      where
        unwrap_op_tv :: GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv (Env TcGblEnv TcLclEnv) (LIdP (GhcPass 'Renamed))
unwrap_op_tv (L SrcSpanAnnA
_ (HsTyVar XTyVar (GhcPass 'Renamed)
_ PromotionFlag
_ LIdP (GhcPass 'Renamed)
op_id)) = LIdP (GhcPass 'Renamed)
-> IOEnv (Env TcGblEnv TcLclEnv) (LIdP (GhcPass 'Renamed))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return LIdP (GhcPass 'Renamed)
op_id
        unwrap_op_tv GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
_ = TcRnMessage
-> IOEnv (Env TcGblEnv TcLclEnv) (LIdP (GhcPass 'Renamed))
forall a. TcRnMessage -> TcRn a
failWith (TcRnMessage
 -> IOEnv (Env TcGblEnv TcLclEnv) (LIdP (GhcPass 'Renamed)))
-> TcRnMessage
-> IOEnv (Env TcGblEnv TcLclEnv) (LIdP (GhcPass 'Renamed))
forall a b. (a -> b) -> a -> b
$ LHsExpr (GhcPass 'Renamed) -> TcRnMessage
TcRnIllformedTypeArgument (SrcSpanAnnA
-> HsExpr (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l HsExpr (GhcPass 'Renamed)
e)
    go (L SrcSpanAnnA
l (HsOverLit XOverLitE (GhcPass 'Renamed)
_ HsOverLit (GhcPass 'Renamed)
lit))
      | Just HsTyLit (GhcPass 'Renamed)
tylit <- OverLitVal -> Maybe (HsTyLit (GhcPass 'Renamed))
tyLitFromOverloadedLit (HsOverLit (GhcPass 'Renamed) -> OverLitVal
forall p. HsOverLit p -> OverLitVal
ol_val HsOverLit (GhcPass 'Renamed)
lit)
      = GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XTyLit (GhcPass 'Renamed)
-> HsTyLit (GhcPass 'Renamed) -> HsType (GhcPass 'Renamed)
forall pass. XTyLit pass -> HsTyLit pass -> HsType pass
HsTyLit XTyLit (GhcPass 'Renamed)
NoExtField
noExtField HsTyLit (GhcPass 'Renamed)
tylit))
    go (L SrcSpanAnnA
l (HsLit XLitE (GhcPass 'Renamed)
_ HsLit (GhcPass 'Renamed)
lit))
      | Just HsTyLit (GhcPass 'Renamed)
tylit <- HsLit (GhcPass 'Renamed) -> Maybe (HsTyLit (GhcPass 'Renamed))
tyLitFromLit HsLit (GhcPass 'Renamed)
lit
      = GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XTyLit (GhcPass 'Renamed)
-> HsTyLit (GhcPass 'Renamed) -> HsType (GhcPass 'Renamed)
forall pass. XTyLit pass -> HsTyLit pass -> HsType pass
HsTyLit XTyLit (GhcPass 'Renamed)
NoExtField
noExtField HsTyLit (GhcPass 'Renamed)
tylit))
    go (L SrcSpanAnnA
l (ExplicitTuple XExplicitTuple (GhcPass 'Renamed)
_ [HsTupArg (GhcPass 'Renamed)]
tup_args Boxity
boxity))
      -- Neither unboxed tuples (#e1,e2#) nor tuple sections (e1,,e2,) can be promoted
      | Boxity -> Bool
isBoxed Boxity
boxity
      , Just [LHsExpr (GhcPass 'Renamed)]
es <- [HsTupArg (GhcPass 'Renamed)] -> Maybe [LHsExpr (GhcPass 'Renamed)]
forall (p :: Pass).
[HsTupArg (GhcPass p)] -> Maybe [LHsExpr (GhcPass p)]
tupArgsPresent_maybe [HsTupArg (GhcPass 'Renamed)]
tup_args
      = do { [GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))]
ts <- (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))))
-> [GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))]
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     [GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))]
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 (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
go [LHsExpr (GhcPass 'Renamed)]
[GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))]
es
           ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XExplicitTupleTy (GhcPass 'Renamed)
-> [LHsType (GhcPass 'Renamed)] -> HsType (GhcPass 'Renamed)
forall pass. XExplicitTupleTy pass -> [LHsType pass] -> HsType pass
HsExplicitTupleTy XExplicitTupleTy (GhcPass 'Renamed)
NoExtField
noExtField [LHsType (GhcPass 'Renamed)]
[GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))]
ts)) }
    go (L SrcSpanAnnA
l (ExplicitList XExplicitList (GhcPass 'Renamed)
_ [LHsExpr (GhcPass 'Renamed)]
es)) =
      do { [GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))]
ts <- (GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))))
-> [GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))]
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     [GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))]
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 (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
go [LHsExpr (GhcPass 'Renamed)]
[GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))]
es
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XExplicitListTy (GhcPass 'Renamed)
-> PromotionFlag
-> [LHsType (GhcPass 'Renamed)]
-> HsType (GhcPass 'Renamed)
forall pass.
XExplicitListTy pass
-> PromotionFlag -> [LHsType pass] -> HsType pass
HsExplicitListTy XExplicitListTy (GhcPass 'Renamed)
NoExtField
noExtField PromotionFlag
NotPromoted [LHsType (GhcPass 'Renamed)]
[GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))]
ts)) }
    go (L SrcSpanAnnA
l (ExprWithTySig XExprWithTySig (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
e LHsSigWcType (NoGhcTc (GhcPass 'Renamed))
sig_ty)) =
      do { GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
t <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
e
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
sig_ki <- (LHsSigType (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
unwrap_sig (GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed))
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))))
-> (HsWildCardBndrs
      (GhcPass 'Renamed)
      (GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed)))
    -> IOEnv
         (Env TcGblEnv TcLclEnv)
         (GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed))))
-> HsWildCardBndrs
     (GhcPass 'Renamed)
     (GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed)))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed)))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed)))
forall t. HsWildCardBndrs (GhcPass 'Renamed) t -> TcM t
unwrap_wc) LHsSigWcType (NoGhcTc (GhcPass 'Renamed))
HsWildCardBndrs
  (GhcPass 'Renamed)
  (GenLocated SrcSpanAnnA (HsSigType (GhcPass 'Renamed)))
sig_ty
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XKindSig (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> HsType (GhcPass 'Renamed)
forall pass.
XKindSig pass -> LHsType pass -> LHsType pass -> HsType pass
HsKindSig [AddEpAnn]
XKindSig (GhcPass 'Renamed)
forall a. NoAnn a => a
noAnn LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
t LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
sig_ki)) }
      where
        unwrap_sig :: LHsSigType GhcRn -> TcM (LHsType GhcRn)
        unwrap_sig :: LHsSigType (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
unwrap_sig (L SrcSpanAnnA
_ (HsSig XHsSig (GhcPass 'Renamed)
_ HsOuterImplicit{hso_ximplicit :: forall flag pass.
HsOuterTyVarBndrs flag pass -> XHsOuterImplicit pass
hso_ximplicit=XHsOuterImplicit (GhcPass 'Renamed)
bndrs} LHsType (GhcPass 'Renamed)
body))
          | [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
XHsOuterImplicit (GhcPass 'Renamed)
bndrs = GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
body
          | Bool
otherwise  = [Name]
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall t. [Name] -> TcM t
illegal_implicit_tvs [Name]
XHsOuterImplicit (GhcPass 'Renamed)
bndrs
        unwrap_sig (L SrcSpanAnnA
l (HsSig XHsSig (GhcPass 'Renamed)
_ HsOuterExplicit{hso_bndrs :: forall flag pass.
HsOuterTyVarBndrs flag pass -> [LHsTyVarBndr flag (NoGhcTc pass)]
hso_bndrs=[LHsTyVarBndr Specificity (NoGhcTc (GhcPass 'Renamed))]
bndrs} LHsType (GhcPass 'Renamed)
body)) =
          LHsType (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHsType (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed)))
-> LHsType (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
forall a b. (a -> b) -> a -> b
$ SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XForAllTy (GhcPass 'Renamed)
-> HsForAllTelescope (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed)
-> HsType (GhcPass 'Renamed)
forall pass.
XForAllTy pass
-> HsForAllTelescope pass -> LHsType pass -> HsType pass
HsForAllTy XForAllTy (GhcPass 'Renamed)
NoExtField
noExtField (XHsForAllInvis (GhcPass 'Renamed)
-> [LHsTyVarBndr Specificity (GhcPass 'Renamed)]
-> HsForAllTelescope (GhcPass 'Renamed)
forall pass.
XHsForAllInvis pass
-> [LHsTyVarBndr Specificity pass] -> HsForAllTelescope pass
HsForAllInvis XHsForAllInvis (GhcPass 'Renamed)
EpAnnForallTy
forall a. NoAnn a => a
noAnn [LHsTyVarBndr Specificity (NoGhcTc (GhcPass 'Renamed))]
[LHsTyVarBndr Specificity (GhcPass 'Renamed)]
bndrs) LHsType (GhcPass 'Renamed)
body)
    go (L SrcSpanAnnA
l (HsPar XPar (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
e)) =
      do { GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
t <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
e
         ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XParTy (GhcPass 'Renamed)
-> LHsType (GhcPass 'Renamed) -> HsType (GhcPass 'Renamed)
forall pass. XParTy pass -> LHsType pass -> HsType pass
HsParTy XParTy (GhcPass 'Renamed)
AnnParen
forall a. NoAnn a => a
noAnn LHsType (GhcPass 'Renamed)
GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
t)) }
    go (L SrcSpanAnnA
l (HsUntypedSplice XUntypedSplice (GhcPass 'Renamed)
splice_result HsUntypedSplice (GhcPass 'Renamed)
splice))
      | HsUntypedSpliceTop ThModFinalizers
finalizers HsExpr (GhcPass 'Renamed)
e <- XUntypedSplice (GhcPass 'Renamed)
splice_result
      = do { GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
t <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go (SrcSpanAnnA
-> HsExpr (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l HsExpr (GhcPass 'Renamed)
e)
           ; let splice_result' :: HsUntypedSpliceResult
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
splice_result' = ThModFinalizers
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> HsUntypedSpliceResult
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall thing.
ThModFinalizers -> thing -> HsUntypedSpliceResult thing
HsUntypedSpliceTop ThModFinalizers
finalizers GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
t
           ; GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XSpliceTy (GhcPass 'Renamed)
-> HsUntypedSplice (GhcPass 'Renamed) -> HsType (GhcPass 'Renamed)
forall pass. XSpliceTy pass -> HsUntypedSplice pass -> HsType pass
HsSpliceTy XSpliceTy (GhcPass 'Renamed)
HsUntypedSpliceResult
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
splice_result' HsUntypedSplice (GhcPass 'Renamed)
splice)) }
    go (L SrcSpanAnnA
l (HsUnboundVar XUnboundVar (GhcPass 'Renamed)
_ RdrName
rdr))
      | OccName -> Bool
isUnderscore OccName
occ = GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpanAnnA
-> HsType (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l (XWildCardTy (GhcPass 'Renamed) -> HsType (GhcPass 'Renamed)
forall pass. XWildCardTy pass -> HsType pass
HsWildCardTy XWildCardTy (GhcPass 'Renamed)
NoExtField
noExtField))
      | OccName -> Bool
startsWithUnderscore OccName
occ =
          -- See Note [Wildcards in the T2T translation]
          do { Bool
wildcards_enabled <- Extension -> TcM Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.NamedWildCards
             ; if Bool
wildcards_enabled
               then RdrName
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall t. RdrName -> TcM t
illegal_wc RdrName
rdr
               else IOEnv
  (Env TcGblEnv TcLclEnv)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
not_in_scope }
      | Bool
otherwise = TcM (LHsType (GhcPass 'Renamed))
IOEnv
  (Env TcGblEnv TcLclEnv)
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
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 (GhcPass 'Renamed)))
not_in_scope = TcRnMessage
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a. TcRnMessage -> TcRn a
failWith (TcRnMessage
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))))
-> TcRnMessage
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
forall a b. (a -> b) -> a -> b
$ RdrName -> NotInScopeError -> TcRnMessage
mkTcRnNotInScope RdrName
rdr NotInScopeError
NotInScope
    go (L SrcSpanAnnA
l (XExpr (ExpandedThingRn (OrigExpr HsExpr (GhcPass 'Renamed)
orig) HsExpr (GhcPass 'Renamed)
_))) =
      -- 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 (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go (SrcSpanAnnA
-> HsExpr (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
l HsExpr (GhcPass 'Renamed)
orig)
    go LHsExpr (GhcPass 'Renamed)
e = TcRnMessage -> TcM (LHsType (GhcPass 'Renamed))
forall a. TcRnMessage -> TcRn a
failWith (TcRnMessage -> TcM (LHsType (GhcPass 'Renamed)))
-> TcRnMessage -> TcM (LHsType (GhcPass 'Renamed))
forall a b. (a -> b) -> a -> b
$ LHsExpr (GhcPass 'Renamed) -> TcRnMessage
TcRnIllformedTypeArgument LHsExpr (GhcPass 'Renamed)
e

    unwrap_wc :: HsWildCardBndrs GhcRn t -> TcM t
    unwrap_wc :: forall t. HsWildCardBndrs (GhcPass 'Renamed) t -> TcM t
unwrap_wc (HsWC XHsWC (GhcPass 'Renamed) t
wcs t
t)
      = do { (Name -> IOEnv (Env TcGblEnv TcLclEnv) Any) -> [Name] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (RdrName -> IOEnv (Env TcGblEnv TcLclEnv) Any
forall t. RdrName -> TcM t
illegal_wc (RdrName -> IOEnv (Env TcGblEnv TcLclEnv) Any)
-> (Name -> RdrName) -> Name -> IOEnv (Env TcGblEnv TcLclEnv) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RdrName
nameRdrName) [Name]
XHsWC (GhcPass 'Renamed) t
wcs
           ; t -> TcM 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
TcRnIllegalImplicitTyVarInTypeArgument (RdrName -> TcRnMessage)
-> (Name -> RdrName) -> Name -> TcRnMessage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RdrName
nameRdrName) [Name]
tvs
           ; TcM t
forall env a. IOEnv env a
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 HsUnboundVar.
     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 (GhcPass 'Renamed)
-> TcM (TcType, TcType)
tc_inst_forall_arg ConcreteTyVars
conc_tvs (TyVarBinder
tvb, TcType
inner_ty) LHsWcType (GhcPass 'Renamed)
hs_ty
  = do { let tv :: TcTyVar
tv   = TyVarBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
tvb
             kind :: TcType
kind = TcTyVar -> TcType
tyVarKind TcTyVar
tv
             tv_nm :: Name
tv_nm   = TcTyVar -> Name
tyVarName TcTyVar
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
       ; TcType
ty_arg0 <- LHsWcType (GhcPass 'Renamed) -> TcType -> TcM TcType
tcHsTypeApp LHsWcType (GhcPass 'Renamed)
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.Gen.Head.
       ; ThStage
th_stage <- TcM ThStage
getStage
       ; TcType
ty_arg <- case Maybe ConcreteTvOrigin
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.
             | Brack ThStage
_ (TcPending {}) <- ThStage
th_stage
             -> 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.
             do { TcMCoercionN
mco <- HasDebugCallStack =>
FastString -> ConcreteTvOrigin -> TcType -> TcM TcMCoercionN
FastString -> ConcreteTvOrigin -> TcType -> TcM TcMCoercionN
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
                ; TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> TcM TcType) -> TcType -> TcM TcType
forall a b. (a -> b) -> a -> b
$ case TcMCoercionN
mco of { TcMCoercionN
MRefl -> TcType
ty_arg0; MCo TcCoercionN
co -> TcCoercionN -> TcType
coercionRKind TcCoercionN
co } }

       ; let fun_ty :: TcType
fun_ty    = TyVarBinder -> TcType -> TcType
mkForAllTy TyVarBinder
tvb TcType
inner_ty
             in_scope :: InScopeSet
in_scope  = Delta -> InScopeSet
mkInScopeSet (ThetaType -> Delta
tyCoVarsOfTypes [TcType
fun_ty, TcType
ty_arg])
             insted_ty :: TcType
insted_ty = HasDebugCallStack =>
InScopeSet -> [TcTyVar] -> ThetaType -> TcType -> TcType
InScopeSet -> [TcTyVar] -> ThetaType -> TcType -> TcType
substTyWithInScope InScopeSet
in_scope [TcTyVar
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].

       ; String -> SDoc -> TcRn ()
traceTc String
"tc_inst_forall_arg (VTA/VDQ)" (
                  [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"fun_ty" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
fun_ty
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
debugPprType TcType
kind
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_arg" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
debugPprType TcType
ty_arg SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon
                                       SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
debugPprType (HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
ty_arg)
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inner_ty" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
debugPprType TcType
inner_ty
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"insted_ty" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
debugPprType TcType
insted_ty ])
       ; (TcType, TcType) -> TcM (TcType, TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType
ty_arg, TcType
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 [HsTyPat] [Pat]  -- (Con @tp1 @tp2 p1 p2)  (constructor pattern)
              | EmbTyPat HsTyPat                  -- (type tp)              (embed a type into a pattern with `type`)
              | ...
     data HsTyPat = HsTP LHsType
  (In ConPat, the type and term arguments are actually inside HsConPatDetails.)

  * Similar to HsAppType in HsExpr, the [HsTyPat] in ConPat is used just 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 HsConPatTyArg (c.o. HsConPatTyArg)
      \ (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 (HsUnboundVar "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 HsUnboundVar.  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.

Wrinkles:

* We avoid zonking, so quickLookArg thereby 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).

* When we quick-look at an argument, we save the work done, by returning
  an EValArg with a ValArgQL inside it.  (It started life with a ValArg
  inside.)  The ValArgQL remembers all the work that QL did (notably,
  decomposing the argument and instantiating) so that tcValArgs does
  not need to repeat it.  Rather neat, and remarkably easy.
-}

----------------
quickLookArg :: Delta
             -> LHsExpr GhcRn          -- ^ Argument
             -> Scaled TcSigmaTypeFRR  -- ^ Type expected by the function
             -> TcM (Delta, EValArg 'TcpInst)
-- See Note [Quick Look at value arguments]
--
-- The returned Delta is a superset of the one passed in
-- with added instantiation variables from
--   (a) the call itself
--   (b) the arguments of the call
quickLookArg :: Delta
-> LHsExpr (GhcPass 'Renamed)
-> Scaled TcType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg Delta
delta LHsExpr (GhcPass 'Renamed)
larg (Scaled TcType
_ TcType
arg_ty)
  | Delta -> Bool
isEmptyVarSet Delta
delta  = Delta
-> LHsExpr (GhcPass 'Renamed) -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr (GhcPass 'Renamed)
larg
  | Bool
otherwise            = TcType -> TcM (Delta, EValArg 'TcpInst)
go TcType
arg_ty
  where
    guarded :: Bool
guarded = TcType -> Bool
isGuardedTy TcType
arg_ty
      -- NB: guardedness is computed based on the original,
      -- unzonked arg_ty, so we deliberately do not exploit
      -- guardedness that emerges a result of QL on earlier args

    go :: TcType -> TcM (Delta, EValArg 'TcpInst)
go TcType
arg_ty | Bool -> Bool
not (TcType -> Bool
isRhoTy TcType
arg_ty)
              = Delta
-> LHsExpr (GhcPass 'Renamed) -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr (GhcPass 'Renamed)
larg

              -- This top-level zonk step, which is the reason
              -- we need a local 'go' loop, is subtle
              -- See Section 9 of the QL paper
              | Just TcTyVar
kappa <- TcType -> Maybe TcTyVar
getTyVar_maybe TcType
arg_ty
              , TcTyVar
kappa TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta
              = do { MetaDetails
info <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
kappa
                   ; case MetaDetails
info of
                       Indirect TcType
arg_ty' -> TcType -> TcM (Delta, EValArg 'TcpInst)
go TcType
arg_ty'
                       MetaDetails
Flexi            -> Bool
-> Delta
-> LHsExpr (GhcPass 'Renamed)
-> TcType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta LHsExpr (GhcPass 'Renamed)
larg TcType
arg_ty }

              | Bool
otherwise
              = Bool
-> Delta
-> LHsExpr (GhcPass 'Renamed)
-> TcType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta LHsExpr (GhcPass 'Renamed)
larg TcType
arg_ty

isGuardedTy :: TcType -> Bool
isGuardedTy :: TcType -> Bool
isGuardedTy TcType
ty
  | Just (TyCon
tc,ThetaType
_) <- HasCallStack => TcType -> Maybe (TyCon, ThetaType)
TcType -> Maybe (TyCon, ThetaType)
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 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaTypeFRR
              -> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 :: Bool
-> Delta
-> LHsExpr (GhcPass 'Renamed)
-> TcType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta larg :: LHsExpr (GhcPass 'Renamed)
larg@(L SrcSpanAnnA
_ HsExpr (GhcPass 'Renamed)
arg) TcType
arg_ty
  = do { ((HsExpr (GhcPass 'Renamed)
rn_fun, AppCtxt
fun_ctxt), [HsExprArg 'TcpRn]
rn_args) <- HsExpr (GhcPass 'Renamed)
-> TcM ((HsExpr (GhcPass 'Renamed), AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr (GhcPass 'Renamed)
arg
       ; Maybe (HsExpr GhcTc, TcType)
mb_fun_ty <- HsExpr (GhcPass 'Renamed) -> TcM (Maybe (HsExpr GhcTc, TcType))
tcInferAppHead_maybe HsExpr (GhcPass 'Renamed)
rn_fun
       ; String -> SDoc -> TcRn ()
traceTc String
"quickLookArg 1" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr (GhcPass 'Renamed) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr (GhcPass 'Renamed)
arg
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"head:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr (GhcPass 'Renamed) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr (GhcPass 'Renamed)
rn_fun SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe (HsExpr GhcTc, TcType) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe (HsExpr GhcTc, TcType)
mb_fun_ty
              , 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 ]

       ; case Maybe (HsExpr GhcTc, TcType)
mb_fun_ty of {
           Maybe (HsExpr GhcTc, TcType)
Nothing     -> -- fun is too complicated
                          Delta
-> LHsExpr (GhcPass 'Renamed) -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr (GhcPass 'Renamed)
larg ;
           Just (HsExpr GhcTc
tc_fun, TcType
fun_sigma) ->

    do { let no_free_kappas :: Bool
no_free_kappas = TcType -> [HsExprArg 'TcpRn] -> Bool
findNoQuantVars TcType
fun_sigma [HsExprArg 'TcpRn]
rn_args
       ; String -> SDoc -> TcRn ()
traceTc String
"quickLookArg 2" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"no_free_kappas:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
no_free_kappas
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"guarded:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
guarded
              , 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
"fun_sigma:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
fun_sigma ]
       ; if Bool -> Bool
not (Bool
guarded Bool -> Bool -> Bool
|| Bool
no_free_kappas)
         then Delta
-> LHsExpr (GhcPass 'Renamed) -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr (GhcPass 'Renamed)
larg
         else
    do { Bool
do_ql <- HsExpr (GhcPass 'Renamed) -> TcM Bool
wantQuickLook HsExpr (GhcPass 'Renamed)
rn_fun
       ; (Delta
delta_app, [HsExprArg 'TcpInst]
inst_args, TcType
app_res_rho) <- Bool
-> Bool
-> (HsExpr GhcTc, AppCtxt)
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcType)
tcInstFun Bool
do_ql Bool
True (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt) TcType
fun_sigma [HsExprArg 'TcpRn]
rn_args
       ; String -> SDoc -> TcRn ()
traceTc String
"quickLookArg 3" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> HsExpr (GhcPass 'Renamed) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr (GhcPass 'Renamed)
arg
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"delta:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"delta_app:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta_app
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arg_ty:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
arg_ty
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"app_res_rho:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
app_res_rho ]

       -- Do quick-look unification
       -- NB: arg_ty may not be zonked, but that's ok
       ; let delta' :: Delta
delta' = Delta
delta Delta -> Delta -> Delta
`unionVarSet` Delta
delta_app
       ; Delta -> TcType -> TcType -> TcRn ()
qlUnify Delta
delta' TcType
arg_ty TcType
app_res_rho

       ; let ql_arg :: EValArg 'TcpInst
ql_arg = ValArgQL { va_expr :: LHsExpr (GhcPass 'Renamed)
va_expr  = LHsExpr (GhcPass 'Renamed)
larg
                               , va_fun :: (HsExpr GhcTc, AppCtxt)
va_fun   = (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt)
                               , va_args :: [HsExprArg 'TcpInst]
va_args  = [HsExprArg 'TcpInst]
inst_args
                               , va_ty :: TcType
va_ty    = TcType
app_res_rho }
       ; (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta', EValArg 'TcpInst
ql_arg) } } } }

skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook :: Delta
-> LHsExpr (GhcPass 'Renamed) -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr (GhcPass 'Renamed)
larg = (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, LHsExpr (GhcPass (XPass 'TcpInst)) -> EValArg 'TcpInst
forall (p :: TcPass). LHsExpr (GhcPass (XPass p)) -> EValArg p
ValArg LHsExpr (GhcPass 'Renamed)
LHsExpr (GhcPass (XPass 'TcpInst))
larg)

----------------
quickLookResultType :: Delta -> TcRhoType -> ExpRhoType -> TcM TcRhoType
-- This function implements the shaded bit of rule APP-Downarrow in
-- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
-- It returns its second argument, but with any variables in Delta
-- substituted out, so no variables in Delta escape

quickLookResultType :: Delta -> TcType -> ExpRhoType -> TcM TcType
quickLookResultType Delta
delta TcType
app_res_rho (Check TcType
exp_rho)
  = -- In checking mode only, do qlUnify with the expected result type
    do { Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Delta -> Bool
isEmptyVarSet Delta
delta)  (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ -- Optimisation only
         Delta -> TcType -> TcType -> TcRn ()
qlUnify Delta
delta TcType
app_res_rho TcType
exp_rho
       ; TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
app_res_rho }

quickLookResultType Delta
_ TcType
app_res_rho (Infer {})
  = 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
app_res_rho
    -- Zonk the result type, to ensure that we substitute out any
    -- filled-in instantiation variable before calling
    -- unifyExpectedType. In the Check case, this isn't necessary,
    -- because unifyExpectedType just drops to tcUnify; but in the
    -- Infer case a filled-in instantiation variable (filled in by
    -- tcInstFun) might perhaps escape into the constraint
    -- generator. The safe thing to do is to zonk any instantiation
    -- variables away.  See Note [Instantiation variables are short lived]

---------------------
qlUnify :: Delta -> TcType -> TcType -> TcM ()
-- Unify ty1 with ty2, unifying only variables in delta
qlUnify :: Delta -> TcType -> TcType -> TcRn ()
qlUnify Delta
delta TcType
ty1 TcType
ty2
  = do { String -> SDoc -> TcRn ()
traceTc String
"qlUnify" (Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ 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)
       ; (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta
emptyVarSet,Delta
emptyVarSet) TcType
ty1 TcType
ty2 }
  where
    go :: (TyVarSet, TcTyVarSet)
       -> TcType -> TcType
       -> TcM ()
    -- The TyVarSets give the variables bound by enclosing foralls
    -- for the corresponding type. Don't unify with these.
    go :: (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs (TyVarTy TcTyVar
tv) TcType
ty2
      | TcTyVar
tv TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta = (Delta, Delta) -> TcTyVar -> TcType -> TcRn ()
go_kappa (Delta, Delta)
bvs TcTyVar
tv TcType
ty2

    go (Delta
bvs1, Delta
bvs2) TcType
ty1 (TyVarTy TcTyVar
tv)
      | TcTyVar
tv TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta = (Delta, Delta) -> TcTyVar -> TcType -> TcRn ()
go_kappa (Delta
bvs2,Delta
bvs1) TcTyVar
tv TcType
ty1

    go (Delta, Delta)
bvs (CastTy TcType
ty1 TcCoercionN
_) TcType
ty2 = (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
ty1 TcType
ty2
    go (Delta, Delta)
bvs TcType
ty1 (CastTy TcType
ty2 TcCoercionN
_) = (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
ty1 TcType
ty2

    go (Delta, Delta)
_ (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 (Delta, Delta)
bvs TcType
rho1 TcType
rho2
      | Just TcType
rho1 <- TcType -> Maybe TcType
coreView TcType
rho1 = (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
rho1 TcType
rho2
      | Just TcType
rho2 <- TcType -> Maybe TcType
coreView TcType
rho2 = (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
rho1 TcType
rho2

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

    -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
    -- and         (c1 => res1) ~   (c2 => res2)
    -- But for the latter we only learn instantiation info from res1~res2
    -- We look at the multiplicity too, although the chances of getting
    -- impredicative instantiation info from there seems...remote.
    go (Delta, Delta)
bvs (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, ft_mult :: TcType -> TcType
ft_mult = TcType
mult1 })
           (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, ft_mult :: TcType -> TcType
ft_mult = TcType
mult2 })
      | 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) ((Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
arg1 TcType
arg2)
           ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FunTyFlag -> Bool
isFUNArg FunTyFlag
af1)        ((Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
mult1 TcType
mult2)
           ; (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
res1 TcType
res2 }

    -- ToDo: c.f. Tc.Utils.unify.uType,
    -- which does not split FunTy here
    -- Also NB tcSplitAppTyNoView here, which does not split (c => t)
    go (Delta, Delta)
bvs (AppTy TcType
t1a TcType
t1b) TcType
ty2
      | Just (TcType
t2a, TcType
t2b) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTyNoView_maybe TcType
ty2
      = do { (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
t1a TcType
t2a; (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
t1b TcType
t2b }

    go (Delta, Delta)
bvs TcType
ty1 (AppTy TcType
t2a TcType
t2b)
      | Just (TcType
t1a, TcType
t1b) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTyNoView_maybe TcType
ty1
      = do { (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
t1a TcType
t2a; (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
t1b TcType
t2b }

    go (Delta
bvs1, Delta
bvs2) (ForAllTy TyVarBinder
bv1 TcType
ty1) (ForAllTy TyVarBinder
bv2 TcType
ty2)
      = (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta
bvs1',Delta
bvs2') TcType
ty1 TcType
ty2
      where
       bvs1' :: Delta
bvs1' = Delta
bvs1 Delta -> TcTyVar -> Delta
`extendVarSet` TyVarBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
bv1
       bvs2' :: Delta
bvs2' = Delta
bvs2 Delta -> TcTyVar -> Delta
`extendVarSet` TyVarBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
bv2

    go (Delta, Delta)
_ TcType
_ TcType
_ = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


    ----------------
    go_kappa :: (Delta, Delta) -> TcTyVar -> TcType -> TcRn ()
go_kappa (Delta, Delta)
bvs TcTyVar
kappa TcType
ty2
      = Bool -> SDoc -> TcRn () -> TcRn ()
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcTyVar -> Bool
isMetaTyVar TcTyVar
kappa) (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
kappa) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
        do { MetaDetails
info <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
kappa
           ; case MetaDetails
info of
               Indirect TcType
ty1 -> (Delta, Delta) -> TcType -> TcType -> TcRn ()
go (Delta, Delta)
bvs TcType
ty1 TcType
ty2
               MetaDetails
Flexi        -> do { TcType
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
                                  ; (Delta, Delta) -> TcTyVar -> TcType -> TcRn ()
forall {a}. (a, Delta) -> TcTyVar -> TcType -> TcRn ()
go_flexi (Delta, Delta)
bvs TcTyVar
kappa TcType
ty2 } }

    ----------------
    go_flexi :: (a, Delta) -> TcTyVar -> TcType -> TcRn ()
go_flexi (a
_,Delta
bvs2) TcTyVar
kappa TcType
ty2  -- ty2 is zonked
      | -- See Note [Actual unification in qlUnify]
        let ty2_tvs :: Delta
ty2_tvs = TcType -> Delta
shallowTyCoVarsOfType TcType
ty2
      , Bool -> Bool
not (Delta
ty2_tvs Delta -> Delta -> Bool
`intersectsVarSet` Delta
bvs2)
          -- Can't instantiate a delta-varto a forall-bound variable
      , Just TcType
ty2 <- [TcTyVar] -> TcType -> Maybe TcType
occCheckExpand [TcTyVar
kappa] TcType
ty2
          -- Passes the occurs check
      = do { let ty2_kind :: TcType
ty2_kind   = HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
ty2
                 kappa_kind :: TcType
kappa_kind = TcTyVar -> TcType
tyVarKind TcTyVar
kappa
           ; TcCoercionN
co <- Maybe TypedThing -> TcType -> TcType -> TcM TcCoercionN
unifyKind (TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (TcType -> TypedThing
TypeThing TcType
ty2)) TcType
ty2_kind TcType
kappa_kind
                   -- unifyKind: see Note [Actual unification in qlUnify]

           ; String -> SDoc -> TcRn ()
traceTc String
"qlUnify:update" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
             [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
kappa SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
kappa_kind)
                       Int
2 (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2_kind)
                 , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"co:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcCoercionN -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionN
co ]
           ; ZonkM () -> TcRn ()
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM () -> TcRn ()) -> ZonkM () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => TcTyVar -> TcType -> ZonkM ()
TcTyVar -> TcType -> ZonkM ()
writeMetaTyVar TcTyVar
kappa (TcType -> TcCoercionN -> TcType
mkCastTy TcType
ty2 TcCoercionN
co) }

      | Bool
otherwise
      = () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()   -- Occurs-check or forall-bound variable


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

* We must not unify with anything bound by an enclosing forall; e.g.
    (forall a. kappa -> Int) ~ forall a. a -> Int)
  That's tracked by the 'bvs' arg of 'go'.

* We must not make an occurs-check; we use occCheckExpand for that.

* checkTypeEq also checks for various other things, including
  - foralls, and predicate types (which we want to allow here)
  - type families (relates to a very specific and exotic performance
    question, that is unlikely to bite here)
  - blocking coercion holes
  After some thought we believe that none of these are relevant
  here

* What if kappa and ty have different kinds?  We solve that problem by
  calling unifyKind, producing a coercion perhaps emitting some deferred
  equality constraints.  That is /different/ from the approach we use in
  the main constraint solver for heterogeneous equalities; see Note
  [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality

  Why different? Because:
  - We can't use qlUnify to solve the kind constraint because qlUnify
    won't unify ordinary (non-instantiation) unification variables.
    (It would have to worry about lots of things like untouchability
    if it did.)
  - qlUnify can't give up if the kinds look un-equal because that would
    mean that it might succeed some times (when the eager unifier
    has already unified those kinds) but not others -- order
    dependence.
  - We can't use the ordinary unifier/constraint solver instead,
    because it doesn't unify polykinds, and has all kinds of other
    magic.  qlUnify is very focused.

  TL;DR Calling unifyKind seems like the lesser evil.
  -}

{- *********************************************************************
*                                                                      *
              Guardedness
*                                                                      *
********************************************************************* -}

findNoQuantVars :: TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
-- True <=> there are no free quantified variables
--          in the result of the call
-- E.g. in the call (f e1 e2), if
--   f :: forall a b. a -> b -> Int   return True
--   f :: forall a b. a -> b -> b     return False (b is free)
findNoQuantVars :: TcType -> [HsExprArg 'TcpRn] -> Bool
findNoQuantVars TcType
fun_ty [HsExprArg 'TcpRn]
args
  = Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go Delta
emptyVarSet TcType
fun_ty [HsExprArg 'TcpRn]
args
  where
    need_instantiation :: [HsExprArg p] -> Bool
need_instantiation []               = Bool
True
    need_instantiation (EValArg {} : [HsExprArg p]
_) = Bool
True
    need_instantiation [HsExprArg p]
_                = Bool
False

    go :: TyVarSet -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
    go :: Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcType
fun_ty [HsExprArg 'TcpRn]
args
      | [HsExprArg 'TcpRn] -> Bool
forall {p :: TcPass}. [HsExprArg p] -> Bool
need_instantiation [HsExprArg 'TcpRn]
args
      , ([TcTyVar]
tvs, ThetaType
theta, TcType
rho) <- TcType -> ([TcTyVar], ThetaType, TcType)
tcSplitSigmaTy TcType
fun_ty
      , Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
      = Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go (Delta
bvs Delta -> [TcTyVar] -> Delta
`extendVarSetList` [TcTyVar]
tvs) TcType
rho [HsExprArg 'TcpRn]
args

    go Delta
bvs TcType
fun_ty [] =  TcType -> Delta
tyCoVarsOfType TcType
fun_ty Delta -> Delta -> Bool
`disjointVarSet` Delta
bvs

    go Delta
bvs TcType
fun_ty (EWrap {} : [HsExprArg 'TcpRn]
args) = Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcType
fun_ty [HsExprArg 'TcpRn]
args
    go Delta
bvs TcType
fun_ty (EPrag {} : [HsExprArg 'TcpRn]
args) = Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcType
fun_ty [HsExprArg 'TcpRn]
args

    go Delta
bvs TcType
fun_ty args :: [HsExprArg 'TcpRn]
args@(ETypeArg {} : [HsExprArg 'TcpRn]
rest_args)
      | ([TcTyVar]
tvs,  TcType
body1) <- (ForAllTyFlag -> Bool) -> TcType -> ([TcTyVar], TcType)
tcSplitSomeForAllTyVars (ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ForAllTyFlag
Inferred) TcType
fun_ty
      , (ThetaType
theta, TcType
body2) <- TcType -> (ThetaType, TcType)
tcSplitPhiTy TcType
body1
      , Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
      = Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go (Delta
bvs Delta -> [TcTyVar] -> Delta
`extendVarSetList` [TcTyVar]
tvs) TcType
body2 [HsExprArg 'TcpRn]
args
      | Just (TyVarBinder
_tv, TcType
res_ty) <- TcType -> Maybe (TyVarBinder, TcType)
tcSplitForAllTyVarBinder_maybe TcType
fun_ty
      = Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcType
res_ty [HsExprArg 'TcpRn]
rest_args
      | Bool
otherwise
      = Bool
False  -- E.g. head ids @Int

    go Delta
bvs TcType
fun_ty (EValArg {} : [HsExprArg 'TcpRn]
rest_args)
      | Just (Scaled TcType
_, TcType
res_ty) <- TcType -> Maybe (Scaled TcType, TcType)
tcSplitFunTy_maybe TcType
fun_ty
      = Delta -> TcType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcType
res_ty [HsExprArg 'TcpRn]
rest_args
      | Bool
otherwise
      = Bool
False  -- E.g. head id 'x'


{- *********************************************************************
*                                                                      *
                 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 GhcRn -> Bool
isTagToEnum :: HsExpr (GhcPass 'Renamed) -> Bool
isTagToEnum (HsVar XVar (GhcPass 'Renamed)
_ (L SrcSpanAnnN
_ Name
fun_id)) = Name
fun_id Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
tagToEnumKey
isTagToEnum HsExpr (GhcPass 'Renamed)
_ = Bool
False

tcTagToEnum :: HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]
            -> TcRhoType
            -> TcM (HsExpr GhcTc)
-- tagToEnum# :: forall a. Int# -> a
-- See Note [tagToEnum#]   Urgh!
tcTagToEnum :: HsExpr GhcTc
-> AppCtxt -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcTc
tc_fun AppCtxt
fun_ctxt [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 (id :: TcPass). HsExprArg id -> Bool
isHsValArg) [HsExprArg 'TcpTc]
tc_args
  = do { TcType
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 HasCallStack => TcType -> Maybe (TyCon, ThetaType)
TcType -> Maybe (TyCon, ThetaType)
tcSplitTyConApp_maybe TcType
res_ty of {
           Maybe (TyCon, ThetaType)
Nothing -> do { TcRnMessage -> TcRn ()
addErrTc (TcType -> TcRnMessage
TcRnTagToEnumUnspecifiedResTy TcType
res_ty)
                         ; TcM (HsExpr GhcTc)
vanilla_result } ;
           Just (TyCon
tc, ThetaType
tc_args) ->

    do { -- Look through any type family
       ; FamInstEnvs
fam_envs <- TcM FamInstEnvs
tcGetFamInstEnvs
       ; case FamInstEnvs
-> TyCon -> ThetaType -> Maybe (TyCon, ThetaType, TcCoercionN)
tcLookupDataFamInst_maybe FamInstEnvs
fam_envs TyCon
tc ThetaType
tc_args of {
           Maybe (TyCon, ThetaType, TcCoercionN)
Nothing -> do { TcType -> TyCon -> TcRn ()
check_enumeration TcType
res_ty TyCon
tc
                         ; TcM (HsExpr GhcTc)
vanilla_result } ;
           Just (TyCon
rep_tc, ThetaType
rep_args, TcCoercionN
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 -> ThetaType -> TcType
mkTyConApp TyCon
rep_tc ThetaType
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 = TcCoercionN -> HsWrapper
mkWpCastR (TcCoercionN -> TcCoercionN
mkSymCo TcCoercionN
coi)
       ; HsExpr GhcTc
tc_expr <- HsExpr GhcTc
-> AppCtxt -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
rebuildHsApps HsExpr GhcTc
tc_fun' AppCtxt
fun_ctxt [HsExprArg 'TcpTc
val_arg] TcType
res_ty
       ; 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
-> AppCtxt -> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
rebuildHsApps HsExpr GhcTc
tc_fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
tc_args TcType
res_ty

    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 (GhcPass 'Renamed) -> HsPragE GhcTc
tcExprPrag (HsPragSCC XSCC (GhcPass 'Renamed)
x1 StringLiteral
ann) = XSCC GhcTc -> StringLiteral -> HsPragE GhcTc
forall p. XSCC p -> StringLiteral -> HsPragE p
HsPragSCC XSCC (GhcPass 'Renamed)
XSCC GhcTc
x1 StringLiteral
ann