{-# 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.Hs

import GHC.Tc.Gen.Head
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.Utils.Concrete( hasFixedRuntimeRep_syntactic )
import GHC.Tc.Zonk.TcType

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

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

import GHC.Types.Var
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 Language.Haskell.Syntax.Basic( isBoxed )

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

import GHC.Prelude

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

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

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

Some notes relative to the paper

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

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

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

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

Note [Instantiation variables are short lived]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* An instantation variable is a mutable meta-type-variable, whose level number
  is QLInstVar.

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

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

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

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

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

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

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

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


{- *********************************************************************
*                                                                      *
              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@(rn_fun,fun_ctxt), rn_args) <- HsExpr (GhcPass 'Renamed)
-> TcM ((HsExpr (GhcPass 'Renamed), AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr (GhcPass 'Renamed)
rn_expr
       ; do_ql <- wantQuickLook rn_fun
       ; (tc_fun, fun_sigma) <- tcInferAppHead fun
       ; (inst_args, app_res_sigma) <- tcInstFun do_ql inst (tc_fun, fun_ctxt) fun_sigma rn_args
       ; _ <- tcValArgs do_ql inst_args
       ; return 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

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

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

   (TCAPP1) Crucially, just before `tcApp` calls `tcInstFun`, it sets the
       ambient TcLevel to QLInstVar, so all unification variables allocated by
       tcInstFun, and in the quick-looks it does at the arguments, will be
       instantiation variables.

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

Now we split into two cases:

4. Case NoQL: no Quick Look

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

   4.2 Check the arguments with `tcValArgs`.

   4.3 Use `finishApp` to wrap up.

5. Case DoQL: use Quick Look

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

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

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

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

   5.4 Use `finishApp` to wrap up

The funcion `finishApp` mainly calls `rebuildHsApps` to rebuild the
application; but it also does a couple of gruesome final checks:
  * Horrible newtype check
  * Special case for tagToEnum

(TCAPP2) There is a lurking difficulty in the above plan:
  * Before calling tcInstFun, we set the ambient level in the monad
    to QLInstVar (Step 2 above).
  * Then, when kind-checking the visible type args of the application,
    we may perhaps build an implication constraint.
  * That means we'll try to add 1 to the ambient level; which is a no-op.
  * So skolem escape checks won't work right.
  This is pretty exotic, so I'm just deferring it for now, leaving
  this note to alert you to the possiblity.

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

tcApp :: HsExpr GhcRn
      -> ExpRhoType   -- When checking, -XDeepSubsumption <=> deeply skolemised
      -> 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 { -- Step 1: Split the application chain
         (fun@(rn_fun, fun_ctxt), rn_args) <- HsExpr (GhcPass 'Renamed)
-> TcM ((HsExpr (GhcPass 'Renamed), AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr (GhcPass 'Renamed)
rn_expr
       ; traceTc "tcApp {" $
           vcat [ text "rn_expr:" <+> ppr rn_expr
                , text "rn_fun:" <+> ppr rn_fun
                , text "fun_ctxt:" <+> ppr fun_ctxt
                , text "rn_args:" <+> ppr rn_args ]

       -- Step 2: Infer the type of `fun`, the head of the application
       ; (tc_fun, fun_sigma) <- tcInferAppHead fun
       ; let tc_head = (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt)

       -- Step 3: Instantiate the function type (taking a quick look at args)
       ; do_ql <- wantQuickLook rn_fun
       ; (inst_args, app_res_rho)
              <- setQLInstLevel do_ql $  -- See (TCAPP1) and (TCAPP2) in
                                         -- Note [tcApp: typechecking applications]
                 tcInstFun do_ql True tc_head fun_sigma rn_args

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

                         -- Step 4.1: subsumption check against expected result type
                         -- See Note [Unify with expected type before typechecking arguments]
                       ; res_wrap <- HsExpr (GhcPass 'Renamed)
-> (HsExpr GhcTc, AppCtxt)
-> [HsExprArg 'TcpInst]
-> TcType
-> ExpRhoType
-> TcM HsWrapper
forall (p :: TcPass).
HsExpr (GhcPass 'Renamed)
-> (HsExpr GhcTc, AppCtxt)
-> [HsExprArg p]
-> TcType
-> ExpRhoType
-> TcM HsWrapper
checkResultTy HsExpr (GhcPass 'Renamed)
rn_expr (HsExpr GhcTc, AppCtxt)
tc_head [HsExprArg 'TcpInst]
inst_args
                                                   TcType
app_res_rho ExpRhoType
exp_res_ty
                         -- Step 4.2: typecheck the  arguments
                       ; tc_args <- tcValArgs NoQL inst_args
                         -- Step 4.3: wrap up
                       ; finishApp tc_head tc_args app_res_rho res_wrap }

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

                         -- Step 5.1: Take a quick look at the result type
                       ; TcType -> ExpRhoType -> TcRn ()
quickLookResultType TcType
app_res_rho ExpRhoType
exp_res_ty
                         -- Step 5.2: typecheck the arguments, and monomorphise
                         --           any un-unified instantiation variables
                       ; tc_args <- QLFlag -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs QLFlag
DoQL [HsExprArg 'TcpInst]
inst_args
                         -- Step 5.3: typecheck the arguments
                       ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
                         -- Step 5.4: subsumption check against the expected type
                       ; res_wrap <- checkResultTy rn_expr tc_head inst_args
                                                   app_res_rho exp_res_ty
                         -- Step 5.5: wrap up
                       ; finishApp tc_head tc_args app_res_rho res_wrap } }

setQLInstLevel :: QLFlag -> TcM a -> TcM a
setQLInstLevel :: forall a. QLFlag -> TcM a -> TcM a
setQLInstLevel QLFlag
DoQL TcM a
thing_inside = TcLevel -> TcM a -> TcM a
forall a. TcLevel -> TcM a -> TcM a
setTcLevel TcLevel
QLInstVar TcM a
thing_inside
setQLInstLevel QLFlag
NoQL TcM a
thing_inside = TcM a
thing_inside

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

finishApp :: (HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpTc]
          -> TcRhoType -> HsWrapper
          -> TcM (HsExpr GhcTc)
-- Do final checks and wrap up the result
finishApp :: (HsExpr GhcTc, AppCtxt)
-> [HsExprArg 'TcpTc] -> TcType -> HsWrapper -> TcM (HsExpr GhcTc)
finishApp tc_head :: (HsExpr GhcTc, AppCtxt)
tc_head@(HsExpr GhcTc
tc_fun,AppCtxt
_) [HsExprArg 'TcpTc]
tc_args TcType
app_res_rho HsWrapper
res_wrap
  = do { -- Horrible newtype check
       ; (HsExpr GhcTc, AppCtxt) -> TcType -> TcRn ()
rejectRepPolyNewtypes (HsExpr GhcTc, AppCtxt)
tc_head TcType
app_res_rho

       -- Reconstruct, with a horrible special case for tagToEnum#.
       ; res_expr <- if HsExpr GhcTc -> Bool
isTagToEnum HsExpr GhcTc
tc_fun
                     then (HsExpr GhcTc, AppCtxt)
-> [HsExprArg 'TcpTc] -> TcType -> TcM (HsExpr GhcTc)
tcTagToEnum (HsExpr GhcTc, AppCtxt)
tc_head [HsExprArg 'TcpTc]
tc_args TcType
app_res_rho
                     else HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps (HsExpr GhcTc, AppCtxt)
tc_head [HsExprArg 'TcpTc]
tc_args)
       ; return (mkHsWrap res_wrap res_expr) }

checkResultTy :: HsExpr GhcRn
              -> (HsExpr GhcTc, AppCtxt)  -- Head
              -> [HsExprArg p]            -- Arguments, just error messages
              -> TcRhoType  -- Inferred type of the application; zonked to
                            --   expose foralls, but maybe not deeply instantiated
              -> ExpRhoType -- Expected type; this is deeply skolemised
              -> TcM HsWrapper
-- Connect up the inferred type of the application with the expected type
-- This is usually just a unification, but with deep subsumption there is more to do
checkResultTy :: forall (p :: TcPass).
HsExpr (GhcPass 'Renamed)
-> (HsExpr GhcTc, AppCtxt)
-> [HsExprArg p]
-> TcType
-> ExpRhoType
-> TcM HsWrapper
checkResultTy HsExpr (GhcPass 'Renamed)
_ (HsExpr GhcTc, AppCtxt)
_ [HsExprArg p]
_ TcType
app_res_rho (Infer InferResult
inf_res)
  = do { co <- TcType -> InferResult -> TcM TcCoercionN
fillInferResult TcType
app_res_rho InferResult
inf_res
       ; return (mkWpCastN co) }

checkResultTy HsExpr (GhcPass 'Renamed)
rn_expr (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt) [HsExprArg p]
inst_args TcType
app_res_rho (Check TcType
res_ty)
-- Unify with expected type from the context
-- See Note [Unify with expected type before typechecking arguments]
--
-- Match up app_res_rho: the result type of rn_expr
--     with res_ty:  the expected result type
 = TcM HsWrapper -> TcM HsWrapper
perhaps_add_res_ty_ctxt (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
   do { ds_flag <- TcM DeepSubsumptionFlag
getDeepSubsumptionFlag
      ; traceTc "checkResultTy {" $
          vcat [ text "tc_fun:" <+> ppr tc_fun
               , text "app_res_rho:" <+> ppr app_res_rho
               , text "res_ty:"  <+> ppr res_ty
               , text "ds_flag:" <+> ppr ds_flag ]
      ; case ds_flag of
          DeepSubsumptionFlag
Shallow -> -- No deep subsumption
             -- app_res_rho and res_ty are both rho-types,
             -- so with simple subsumption we can just unify them
             -- No need to zonk; the unifier does that
             do { co <- HsExpr (GhcPass 'Renamed) -> TcType -> TcType -> TcM TcCoercionN
unifyExprType HsExpr (GhcPass 'Renamed)
rn_expr TcType
app_res_rho TcType
res_ty
                ; traceTc "checkResultTy 1 }" (ppr co)
                ; return (mkWpCastN co) }

          DeepSubsumptionFlag
Deep ->   -- Deep subsumption
             -- Even though both app_res_rho and 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 { wrap <- HsExpr (GhcPass 'Renamed) -> TcType -> TcType -> TcM HsWrapper
tcSubTypeDS HsExpr (GhcPass 'Renamed)
rn_expr TcType
app_res_rho TcType
res_ty
                ; traceTc "checkResultTy 2 }" (ppr app_res_rho $$ ppr res_ty)
                ; return wrap } }
  where
    -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
    -- more confusing than helpful because the function at the head isn't in
    -- the source program; it was added by the renamer.  See
    -- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
    perhaps_add_res_ty_ctxt :: TcM HsWrapper -> TcM HsWrapper
perhaps_add_res_ty_ctxt TcM HsWrapper
thing_inside
      | 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 GhcTc
-> [HsExprArg p]
-> TcType
-> ExpRhoType
-> TcM HsWrapper
-> TcM HsWrapper
forall (p :: TcPass) a.
HsExpr GhcTc
-> [HsExprArg p] -> TcType -> ExpRhoType -> TcM a -> TcM a
addFunResCtxt HsExpr GhcTc
tc_fun [HsExprArg p]
inst_args TcType
app_res_rho (TcType -> ExpRhoType
mkCheckExpType TcType
res_ty) (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
        TcM HsWrapper
thing_inside

----------------
tcValArgs :: QLFlag -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
-- Importantly, tcValArgs works left-to-right, so that by the time we
-- encounter an argument, we have monomorphised all the instantiation
-- variables that its type contains.  All that is left to do is an ordinary
-- zonkTcType.  See Note [Monomorphise instantiation variables].
tcValArgs :: QLFlag -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs QLFlag
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 (QLFlag
-> HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
tcValArg QLFlag
do_ql) [HsExprArg 'TcpInst]
args

tcValArg :: QLFlag -> HsExprArg 'TcpInst    -- Actual argument
         -> TcM (HsExprArg 'TcpTc)          -- Resulting argument
tcValArg :: QLFlag
-> HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
tcValArg QLFlag
_     (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))
tcValArg QLFlag
_     (ETypeArg AppCtxt
l LHsWcType (GhcPass 'Renamed)
hty 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)
hty XETAType 'TcpInst
XETAType 'TcpTc
ty)
tcValArg QLFlag
do_ql (EWrap (EHsWrap HsWrapper
w)) = do { QLFlag -> ZonkM () -> TcRn ()
whenQL QLFlag
do_ql (ZonkM () -> TcRn ()) -> ZonkM () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ HsWrapper -> ZonkM ()
qlMonoHsWrapper HsWrapper
w
                                        ; HsExprArg 'TcpTc
-> 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 (HsWrapper -> EWrap
EHsWrap HsWrapper
w)) }
  -- qlMonoHsWrapper: see Note [Monomorphise instantiation variables]
tcValArg QLFlag
_     (EWrap EWrap
ew)          = 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
ew)

tcValArg QLFlag
do_ql (EValArg { ea_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
ea_ctxt   = AppCtxt
ctxt
                        , ea_arg :: forall (p :: TcPass). HsExprArg p -> LHsExpr (GhcPass (XPass p))
ea_arg    = larg :: LHsExpr (GhcPass (XPass 'TcpInst))
larg@(L SrcSpanAnnA
arg_loc HsExpr (GhcPass 'Renamed)
arg)
                        , ea_arg_ty :: forall (p :: TcPass). HsExprArg p -> XEVAType p
ea_arg_ty = XEVAType 'TcpInst
sc_arg_ty })
  = AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall a. AppCtxt -> LHsExpr (GhcPass 'Renamed) -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
LHsExpr (GhcPass (XPass 'TcpInst))
larg (IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
 -> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc))
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall a b. (a -> b) -> a -> b
$
    do { String -> SDoc -> TcRn ()
traceTc String
"tcValArg" (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
<+> Scaled TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr Scaled TcType
XEVAType 'TcpInst
sc_arg_ty
              , 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 ]

         -- Crucial step: expose QL results before checking exp_arg_ty
         -- So far as the paper is concerned, this step applies
         -- the poly-substitution Theta, learned by QL, so that we
         -- "see" the polymorphism in that argument type. E.g.
         --    (:) e ids, where ids :: [forall a. a->a]
         --                     (:) :: forall p. p->[p]->[p]
         -- Then Theta = [p :-> forall a. a->a], and we want
         -- to check 'e' with expected type (forall a. a->a)
         -- See Note [Instantiation variables are short lived]
       ; Scaled mult exp_arg_ty <- case QLFlag
do_ql of
              QLFlag
DoQL -> ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (Scaled TcType)
 -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType))
-> ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a b. (a -> b) -> a -> b
$ Scaled TcType -> ZonkM (Scaled TcType)
zonkScaledTcType Scaled TcType
XEVAType 'TcpInst
sc_arg_ty
              QLFlag
NoQL -> Scaled TcType -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Scaled TcType
XEVAType 'TcpInst
sc_arg_ty

         -- Now check the argument
       ; arg' <- tcScalingUsage mult $
                 tcPolyExpr arg (mkCheckExpType exp_arg_ty)

       ; return (EValArg { ea_ctxt = ctxt
                         , ea_arg = L arg_loc arg'
                         , ea_arg_ty = noExtField }) }

tcValArg QLFlag
_ (EValArgQL { eaql_wanted :: HsExprArg 'TcpInst -> WantedConstraints
eaql_wanted  = WantedConstraints
wanted
                      , eaql_ctxt :: HsExprArg 'TcpInst -> AppCtxt
eaql_ctxt    = AppCtxt
ctxt
                      , eaql_arg_ty :: HsExprArg 'TcpInst -> Scaled TcType
eaql_arg_ty  = Scaled TcType
sc_arg_ty
                      , eaql_larg :: HsExprArg 'TcpInst -> LHsExpr (GhcPass 'Renamed)
eaql_larg    = larg :: LHsExpr (GhcPass 'Renamed)
larg@(L SrcSpanAnnA
arg_loc HsExpr (GhcPass 'Renamed)
rn_expr)
                      , eaql_tc_fun :: HsExprArg 'TcpInst -> (HsExpr GhcTc, AppCtxt)
eaql_tc_fun  = (HsExpr GhcTc, AppCtxt)
tc_head
                      , eaql_args :: HsExprArg 'TcpInst -> [HsExprArg 'TcpInst]
eaql_args    = [HsExprArg 'TcpInst]
inst_args
                      , eaql_encl :: HsExprArg 'TcpInst -> Bool
eaql_encl    = Bool
arg_influences_enclosing_call
                      , eaql_res_rho :: HsExprArg 'TcpInst -> TcType
eaql_res_rho = TcType
app_res_rho })
  = AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall a. AppCtxt -> LHsExpr (GhcPass 'Renamed) -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
larg (IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
 -> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc))
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall a b. (a -> b) -> a -> b
$
    do { -- Expose QL results to tcSkolemise, as in EValArg case
         Scaled mult exp_arg_ty <- ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (Scaled TcType)
 -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType))
-> ZonkM (Scaled TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
forall a b. (a -> b) -> a -> b
$ Scaled TcType -> ZonkM (Scaled TcType)
zonkScaledTcType Scaled TcType
sc_arg_ty

       ; traceTc "tcEValArgQL {" (vcat [ text "app_res_rho:" <+> ppr app_res_rho
                                       , text "exp_arg_ty:" <+> ppr exp_arg_ty
                                       , text "args:" <+> ppr inst_args ])

       ; ds_flag <- getDeepSubsumptionFlag
       ; (wrap, arg')
            <- tcScalingUsage mult  $
               tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ TcType
exp_arg_rho ->
               do { -- Emit saved-up constraints, /under/ the tcSkolemise
                    -- See (QLA4) in Note [Quick Look at value arguments]
                    WantedConstraints -> TcRn ()
emitConstraints WantedConstraints
wanted

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

                  ; tc_args <- QLFlag -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs QLFlag
DoQL [HsExprArg 'TcpInst]
inst_args
                  ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
                  ; res_wrap <- checkResultTy rn_expr tc_head inst_args
                                              app_res_rho (mkCheckExpType exp_arg_rho)
                  ; finishApp tc_head tc_args app_res_rho res_wrap }

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

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


--------------------
wantQuickLook :: HsExpr GhcRn -> TcM QLFlag
wantQuickLook :: HsExpr (GhcPass 'Renamed) -> TcM QLFlag
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 = QLFlag -> TcM QLFlag
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return QLFlag
DoQL
wantQuickLook HsExpr (GhcPass 'Renamed)
_                      = do { impred <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
                                          ; if impred then return DoQL else return NoQL }

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

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

tcInstFun :: QLFlag
          -> Bool   -- False <=> Instantiate only /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)
          -> TcSigmaType -> [HsExprArg 'TcpRn]
          -> TcM ( [HsExprArg 'TcpInst]
                 , TcSigmaType )
-- This crucial function implements the |-inst judgement in Fig 4, plus the
-- modification in Fig 5, of the QL paper:
-- "A quick look at impredicativity" (ICFP'20).
tcInstFun :: QLFlag
-> Bool
-> (HsExpr GhcTc, AppCtxt)
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
tcInstFun QLFlag
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
<+> QLFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr QLFlag
do_ql ])
       ; Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go Int
1 [] TcType
fun_sigma [HsExprArg 'TcpRn]
rn_args }
  where
    fun_orig :: CtOrigin
fun_orig = case AppCtxt
fun_ctxt of
      VAExpansion (OrigStmt{}) SrcSpan
_ SrcSpan
_  -> CtOrigin
DoOrigin
      VAExpansion (OrigPat LPat (GhcPass 'Renamed)
pat) SrcSpan
_ SrcSpan
_ -> LPat (GhcPass 'Renamed) -> CtOrigin
DoPatOrigin LPat (GhcPass 'Renamed)
pat
      VAExpansion (OrigExpr HsExpr (GhcPass 'Renamed)
e) SrcSpan
_ SrcSpan
_  -> HsExpr (GhcPass 'Renamed) -> CtOrigin
exprCtOrigin HsExpr (GhcPass 'Renamed)
e
      VACall HsExpr (GhcPass 'Renamed)
e Int
_ SrcSpan
_                  -> 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.Utils.Concrete
    fun_conc_tvs :: ConcreteTyVars
fun_conc_tvs
      | HsVar XVar GhcTc
_ (L SrcSpanAnnN
_ Id
fun_id) <- HsExpr GhcTc
tc_fun
      = Id -> ConcreteTyVars
idConcreteTvs Id
fun_id
      -- Recall that DataCons are represented using ConLikeTc at GhcTc stage,
      -- see Note [Typechecking data constructors] in GHC.Tc.Gen.Head.
      | XExpr (ConLikeTc (RealDataCon DataCon
dc) [Id]
_ [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 :: Int                      -- Value-argument position of next arg
            -> [HsExprArg 'TcpInst]     -- Accumulator, reversed
            -> TcSigmaType -> [HsExprArg 'TcpRn]
            -> TcM ([HsExprArg 'TcpInst], TcSigmaType)

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

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

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

    -- Rule IALL from Fig 4 of the QL paper; applies even if args = []
    -- Instantiate invisible foralls and dictionaries.
    -- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
    go1 Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty [HsExprArg 'TcpRn]
args
      | ([Id]
tvs,   TcType
body1) <- (ForAllTyFlag -> Bool) -> TcType -> ([Id], TcType)
tcSplitSomeForAllTyVars ([HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
inst_fun [HsExprArg 'TcpRn]
args) TcType
fun_ty
      , (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
      , let no_tvs :: Bool
no_tvs   = [Id] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
tvs
            no_theta :: Bool
no_theta = ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta
      , Bool -> Bool
not (Bool
no_tvs Bool -> Bool -> Bool
&& Bool
no_theta)
      = do { (_inst_tvs, wrap, fun_rho) <-
                -- addHeadCtxt: important for the class constraints
                -- that may be emitted from instantiating fun_sigma
                AppCtxt
-> TcM ([Id], HsWrapper, TcType) -> TcM ([Id], HsWrapper, TcType)
forall a. AppCtxt -> TcM a -> TcM a
addHeadCtxt AppCtxt
fun_ctxt (TcM ([Id], HsWrapper, TcType) -> TcM ([Id], HsWrapper, TcType))
-> TcM ([Id], HsWrapper, TcType) -> TcM ([Id], HsWrapper, TcType)
forall a b. (a -> b) -> a -> b
$
                CtOrigin
-> ConcreteTyVars
-> [Id]
-> ThetaType
-> TcType
-> TcM ([Id], HsWrapper, TcType)
instantiateSigma CtOrigin
fun_orig ConcreteTyVars
fun_conc_tvs [Id]
tvs ThetaType
theta TcType
body2
                  -- See Note [Representation-polymorphism checking built-ins]
                  -- in GHC.Tc.Utils.Concrete.
                  -- NB: we are doing this even when "acc" is not empty,
                  -- to handle e.g.
                  --
                  --   badTup :: forall r (a :: TYPE r). a -> (# Int, a #)
                  --   badTup = (# , #) @LiftedRep
                  --
                  -- in which we already have instantiated the first RuntimeRep
                  -- argument of (#,#) to @LiftedRep, but want to rule out the
                  -- second instantiation @r.

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

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

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

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

    go1 Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty (EPrag AppCtxt
sp HsPragE (GhcPass (XPass 'TcpRn))
prag : [HsExprArg 'TcpRn]
args)
      = Int
-> [HsExprArg 'TcpInst]
-> TcType
-> [HsExprArg 'TcpRn]
-> TcM ([HsExprArg 'TcpInst], TcType)
go1 Int
pos (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) TcType
fun_ty [HsExprArg 'TcpRn]
args

    -- Rule ITYARG from Fig 4 of the QL paper
    go1 Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty ( ETypeArg { ea_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
ea_ctxt = AppCtxt
ctxt, ea_hs_ty :: forall (p :: TcPass). HsExprArg p -> LHsWcType (GhcPass 'Renamed)
ea_hs_ty = LHsWcType (GhcPass 'Renamed)
hs_ty }
                             : [HsExprArg 'TcpRn]
rest_args )
      = do { (ty_arg, 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' = ETypeArg { ea_ctxt :: AppCtxt
ea_ctxt = AppCtxt
ctxt, ea_hs_ty :: LHsWcType (GhcPass 'Renamed)
ea_hs_ty = LHsWcType (GhcPass 'Renamed)
hs_ty, ea_ty_arg :: XETAType 'TcpInst
ea_ty_arg = TcType
XETAType 'TcpInst
ty_arg }
           ; go pos (arg' : acc) inst_ty rest_args }

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

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

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

           ; go pos acc' fun_ty' args }

    -- Rule IARG from Fig 4 of the QL paper:
    go1 Int
pos [HsExprArg 'TcpInst]
acc TcType
fun_ty
        (EValArg { ea_arg :: forall (p :: TcPass). HsExprArg p -> LHsExpr (GhcPass (XPass p))
ea_arg = LHsExpr (GhcPass (XPass 'TcpRn))
arg, ea_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
ea_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)
           ; (wrap, arg_ty, res_ty) <-
                -- NB: matchActualFunTy does the rep-poly check.
                -- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
                -- In an application (f x), we need 'x' to have a fixed runtime
                -- representation; matchActualFunTy checks that when
                -- taking apart the arrow type (a -> Int).
                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

           ; arg' <- quickLookArg do_ql ctxt arg arg_ty
           ; let acc' = HsExprArg 'TcpInst
arg' HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall (p :: TcPass). HsWrapper -> [HsExprArg p] -> [HsExprArg p]
addArgWrap HsWrapper
wrap [HsExprArg 'TcpInst]
acc
           ; go (pos+1) acc' res_ty rest_args }

    new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
    -- Make a fresh nus for each argument in rule IVAR
    new_arg_ty :: LHsExpr (GhcPass 'Renamed)
-> Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcType)
new_arg_ty (L SrcSpanAnnA
_ HsExpr (GhcPass 'Renamed)
arg) Int
i
      = do { arg_nu <- FixedRuntimeRepContext -> TcM TcType
newOpenFlexiFRRTyVarTy (FixedRuntimeRepContext -> TcM TcType)
-> FixedRuntimeRepContext -> TcM TcType
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
               -- Following matchActualFunTy, we create nu_i :: TYPE kappa_i[conc],
               -- thereby ensuring that the arguments have concrete runtime representations

           ; mult_ty <- newFlexiTyVarTy multiplicityTy
               -- mult_ty: e need variables for argument multiplicities (#18731)
               -- Otherwise, 'undefined x' wouldn't be linear in x

           ; return (mkScaled mult_ty arg_nu) }

-- Is the argument supposed to instantiate a forall?
--
-- In other words, given a function application `fn arg`,
-- can we look at the `arg` and conclude that `fn :: forall x. t`
-- or `fn :: forall x -> t`?
--
-- This is a conservative heuristic that returns `False` for "don't know".
-- Used to improve error messages only.
-- See Note [VTA for out-of-scope functions].
looks_like_type_arg :: HsExprArg 'TcpRn -> Bool
looks_like_type_arg :: HsExprArg 'TcpRn -> Bool
looks_like_type_arg ETypeArg{} =
  -- The argument is clearly supposed to instantiate an invisible forall,
  -- i.e. when we see `f @a`, we expect `f :: forall x. t`.
  Bool
True
looks_like_type_arg EValArg{ ea_arg :: forall (p :: TcPass). HsExprArg p -> LHsExpr (GhcPass (XPass p))
ea_arg = L SrcSpanAnnA
_ HsExpr (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 { in_generated_code <- TcRnIf TcGblEnv TcLclEnv Bool
inGeneratedCode
       ; case 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.Utils.Concrete.
      -> TcType            -- ^ Function type
      -> LHsWcType GhcRn   -- ^ Argument type
      -> TcM (TcType, TcType)
-- Deal with a visible type application
-- The function type has already had its Inferred binders instantiated
tcVTA :: ConcreteTyVars
-> TcType -> LHsWcType (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 { (_, fun_ty) <- ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType))
-> ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType)
forall a b. (a -> b) -> a -> b
$ TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
emptyTidyEnv TcType
fun_ty
       ; failWith $ TcRnInvalidTypeApplication fun_ty hs_ty }

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

-- Convert a HsExpr into the equivalent HsType.
-- See [RequiredTypeArguments and the T2T mapping]
expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
expr_to_type :: LHsExpr (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 (HsFunArr XFunArr (GhcPass 'Renamed)
_ HsArrowOf (LHsExpr (GhcPass 'Renamed)) (GhcPass 'Renamed)
mult LHsExpr (GhcPass 'Renamed)
arg LHsExpr (GhcPass 'Renamed)
res)) =
      do { arg' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
arg
         ; mult' <- go_arrow mult
         ; res' <- go res
         ; return (L l (HsFunTy noExtField mult' arg' res'))}
         where
          go_arrow :: HsArrowOf (LHsExpr GhcRn) GhcRn -> TcM (HsArrow GhcRn)
          go_arrow :: HsArrowOf (LHsExpr (GhcPass 'Renamed)) (GhcPass 'Renamed)
-> TcM (HsArrow (GhcPass 'Renamed))
go_arrow (HsUnrestrictedArrow{}) = HsArrowOf
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsArrowOf
        (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
        (GhcPass 'Renamed))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (XUnrestrictedArrow
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
-> HsArrowOf
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
     (GhcPass 'Renamed)
forall mult pass.
XUnrestrictedArrow mult pass -> HsArrowOf mult pass
HsUnrestrictedArrow NoExtField
XUnrestrictedArrow
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
noExtField)
          go_arrow (HsLinearArrow{}) = HsArrowOf
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsArrowOf
        (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
        (GhcPass 'Renamed))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (XLinearArrow
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
-> HsArrowOf
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
     (GhcPass 'Renamed)
forall mult pass. XLinearArrow mult pass -> HsArrowOf mult pass
HsLinearArrow NoExtField
XLinearArrow
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
noExtField)
          go_arrow (HsExplicitMult XExplicitMult (LHsExpr (GhcPass 'Renamed)) (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
exp) = XExplicitMult
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
-> GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
-> HsArrowOf
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
     (GhcPass 'Renamed)
forall mult pass.
XExplicitMult mult pass -> mult -> HsArrowOf mult pass
HsExplicitMult NoExtField
XExplicitMult
  (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
  (GhcPass 'Renamed)
noExtField (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed))
 -> HsArrowOf
      (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
      (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (HsArrowOf
        (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
        (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)
exp
    go (L SrcSpanAnnA
l (HsForAll XForAll (GhcPass 'Renamed)
_ HsForAllTelescope (GhcPass 'Renamed)
tele LHsExpr (GhcPass 'Renamed)
expr)) =
      do { ty <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
expr
         ; return (L l (HsForAllTy noExtField tele ty))}
    go (L SrcSpanAnnA
l (HsQual XQual (GhcPass 'Renamed)
_ (L SrcSpanAnnC
ann [GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))]
ctxt) LHsExpr (GhcPass 'Renamed)
expr)) =
      do { ctxt' <- (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 :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (GenLocated SrcSpanAnnA (HsType (GhcPass 'Renamed)))
go [GenLocated SrcSpanAnnA (HsExpr (GhcPass 'Renamed))]
ctxt
         ; ty <- go expr
         ; return (L l (HsQualTy noExtField (L ann ctxt') ty)) }
    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 { lhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
lhs
         ; rhs' <- go rhs
         ; return (L l (HsAppTy noExtField lhs' rhs')) }
    go (L SrcSpanAnnA
l (HsAppType XAppTypeE (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
lhs LHsWcType (NoGhcTc (GhcPass 'Renamed))
rhs)) =
      do { lhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
lhs
         ; rhs' <- unwrap_wc rhs
         ; return (L l (HsAppKindTy noExtField lhs' 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 { lhs' <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
lhs
         ; op'  <- go op
         ; rhs' <- go rhs
         ; op_id <- unwrap_op_tv op'
         ; return (L l (HsOpTy noAnn NotPromoted lhs' op_id 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 { 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
           ; return (L l (HsExplicitTupleTy noExtField ts)) }
    go (L SrcSpanAnnA
l (ExplicitList XExplicitList (GhcPass 'Renamed)
_ [LHsExpr (GhcPass 'Renamed)]
es)) =
      do { 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
         ; return (L l (HsExplicitListTy noExtField NotPromoted ts)) }
    go (L SrcSpanAnnA
l (ExprWithTySig XExprWithTySig (GhcPass 'Renamed)
_ LHsExpr (GhcPass 'Renamed)
e LHsSigWcType (NoGhcTc (GhcPass 'Renamed))
sig_ty)) =
      do { t <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
e
         ; sig_ki <- (unwrap_sig <=< unwrap_wc) sig_ty
         ; return (L l (HsKindSig noAnn t sig_ki)) }
      where
        unwrap_sig :: LHsSigType GhcRn -> TcM (LHsType GhcRn)
        unwrap_sig :: LHsSigType (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)
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 { t <- LHsExpr (GhcPass 'Renamed) -> TcM (LHsType (GhcPass 'Renamed))
go LHsExpr (GhcPass 'Renamed)
e
         ; return (L l (HsParTy noAnn 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 { 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' = 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
           ; return (L l (HsSpliceTy splice_result' 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 { wildcards_enabled <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.NamedWildCards
             ; if wildcards_enabled
               then illegal_wc rdr
               else not_in_scope }
      | Bool
otherwise = TcM (LHsType (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) (ZonkAny 0))
-> [Name] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (RdrName -> IOEnv (Env TcGblEnv TcLclEnv) (ZonkAny 0)
forall t. RdrName -> TcM t
illegal_wc (RdrName -> IOEnv (Env TcGblEnv TcLclEnv) (ZonkAny 0))
-> (Name -> RdrName)
-> Name
-> IOEnv (Env TcGblEnv TcLclEnv) (ZonkAny 0)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RdrName
nameRdrName) [Name]
XHsWC (GhcPass 'Renamed) t
wcs
           ; t -> IOEnv (Env TcGblEnv TcLclEnv) t
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return t
t }

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

    illegal_implicit_tvs :: [Name] -> TcM t
    illegal_implicit_tvs :: forall t. [Name] -> TcM t
illegal_implicit_tvs [Name]
tvs
      = do { (Name -> TcRn ()) -> [Name] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TcRnMessage -> TcRn ()
addErr (TcRnMessage -> TcRn ())
-> (Name -> TcRnMessage) -> Name -> TcRn ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RdrName -> TcRnMessage
TcRnIllegalImplicitTyVarInTypeArgument (RdrName -> TcRnMessage)
-> (Name -> RdrName) -> Name -> TcRnMessage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RdrName
nameRdrName) [Name]
tvs
           ; IOEnv (Env TcGblEnv TcLclEnv) t
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 :: Id
tv   = TyVarBinder -> Id
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
tvb
             kind :: TcType
kind = Id -> TcType
tyVarKind Id
tv
             tv_nm :: Name
tv_nm   = Id -> Name
tyVarName Id
tv
             mb_conc :: Maybe ConcreteTvOrigin
mb_conc = ConcreteTyVars -> Name -> Maybe ConcreteTvOrigin
forall a. NameEnv a -> Name -> Maybe a
lookupNameEnv ConcreteTyVars
conc_tvs Name
tv_nm
       ; ty_arg0 <- LHsWcType (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.Utils.Concrete.
       ; th_stage <- getStage
       ; ty_arg <- case mb_conc of
           Maybe ConcreteTvOrigin
Nothing   -> TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
ty_arg0
           Just ConcreteTvOrigin
conc
             -- See [Wrinkle: Typed Template Haskell]
             -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
             | 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 { 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
                ; return $ case mco of { TcMCoercionN
MRefl -> TcType
ty_arg0; MCo TcCoercionN
co -> HasDebugCallStack => TcCoercionN -> TcType
TcCoercionN -> TcType
coercionRKind TcCoercionN
co } }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Syntax of abstractions in Pat
-----------------------------
* Type patterns are represented in Pat roughly like this
     data Pat = ConPat   ConLike [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.  The key rule, implemented by `quickLookArg` is

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

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

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

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

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

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

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

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

      - Captures the result in an EValArgQL record

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

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

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

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

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

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

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

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

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

quickLookArg :: QLFlag -> AppCtxt
             -> LHsExpr GhcRn          -- ^ Argument
             -> Scaled TcSigmaTypeFRR  -- ^ Type expected by the function
             -> TcM (HsExprArg 'TcpInst)
-- See Note [Quick Look at value arguments]
quickLookArg :: QLFlag
-> AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> Scaled TcType
-> TcM (HsExprArg 'TcpInst)
quickLookArg QLFlag
NoQL AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
larg Scaled TcType
orig_arg_ty
  = AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> Scaled TcType
-> TcM (HsExprArg 'TcpInst)
skipQuickLook AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
larg Scaled TcType
orig_arg_ty
quickLookArg QLFlag
DoQL AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
larg Scaled TcType
orig_arg_ty
  = do { is_rho <- TcType -> TcRnIf TcGblEnv TcLclEnv Bool
tcIsDeepRho (Scaled TcType -> TcType
forall a. Scaled a -> a
scaledThing Scaled TcType
orig_arg_ty)
       ; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho)
       ; if not is_rho
         then skipQuickLook ctxt larg orig_arg_ty
         else quickLookArg1 ctxt larg orig_arg_ty }

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

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

tcIsDeepRho :: TcType -> TcM Bool
-- This top-level zonk step, which is the reason we need a local 'go' loop,
-- is subtle. See Section 9 of the QL paper

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

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

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

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

isGuardedTy :: TcType -> Bool
isGuardedTy :: TcType -> Bool
isGuardedTy TcType
ty
  | Just (TyCon
tc,ThetaType
_) <- HasDebugCallStack => 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 :: AppCtxt -> LHsExpr GhcRn
              -> Scaled TcRhoType  -- Deeply skolemised
              -> TcM (HsExprArg 'TcpInst)
-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
quickLookArg1 :: AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> Scaled TcType
-> TcM (HsExprArg 'TcpInst)
quickLookArg1 AppCtxt
ctxt larg :: LHsExpr (GhcPass 'Renamed)
larg@(L SrcSpanAnnA
_ HsExpr (GhcPass 'Renamed)
arg) sc_arg_ty :: Scaled TcType
sc_arg_ty@(Scaled TcType
_ TcType
orig_arg_rho)
  = AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> TcM (HsExprArg 'TcpInst)
-> TcM (HsExprArg 'TcpInst)
forall a. AppCtxt -> LHsExpr (GhcPass 'Renamed) -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
larg (TcM (HsExprArg 'TcpInst) -> TcM (HsExprArg 'TcpInst))
-> TcM (HsExprArg 'TcpInst) -> TcM (HsExprArg 'TcpInst)
forall a b. (a -> b) -> a -> b
$ -- Context needed for constraints
                           -- generated by calls in arg
    do { ((rn_fun, fun_ctxt), rn_args) <- HsExpr (GhcPass 'Renamed)
-> TcM ((HsExpr (GhcPass 'Renamed), AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr (GhcPass 'Renamed)
arg

       -- Step 1: get the type of the head of the argument
       ; mb_fun_ty <- tcInferAppHead_maybe rn_fun
       ; traceTc "quickLookArg {" $
         vcat [ text "arg:" <+> ppr arg
              , text "orig_arg_rho:" <+> ppr orig_arg_rho
              , text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty
              , text "args:" <+> ppr rn_args ]

       ; case mb_fun_ty of {
           Maybe (HsExpr GhcTc, TcType)
Nothing -> AppCtxt
-> LHsExpr (GhcPass 'Renamed)
-> Scaled TcType
-> TcM (HsExprArg 'TcpInst)
skipQuickLook AppCtxt
ctxt LHsExpr (GhcPass 'Renamed)
larg Scaled TcType
sc_arg_ty ;    -- fun is too complicated
           Just (HsExpr GhcTc
tc_fun, TcType
fun_sigma) ->

       -- step 2: use |-inst to instantiate the head applied to the arguments
    do { let tc_head :: (HsExpr GhcTc, AppCtxt)
tc_head = (HsExpr GhcTc
tc_fun, AppCtxt
fun_ctxt)
       ; do_ql <- HsExpr (GhcPass 'Renamed) -> TcM QLFlag
wantQuickLook HsExpr (GhcPass 'Renamed)
rn_fun
       ; ((inst_args, app_res_rho), wanted)
             <- captureConstraints $
                tcInstFun do_ql True tc_head fun_sigma rn_args

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

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

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

       ; traceTc "quickLookArg done }" (ppr rn_fun)

       ; return (EValArgQL { eaql_ctxt    = ctxt
                           , eaql_arg_ty  = sc_arg_ty
                           , eaql_larg    = larg
                           , eaql_tc_fun  = tc_head
                           , eaql_args    = inst_args
                           , eaql_wanted  = wanted
                           , eaql_encl    = arg_influences_enclosing_call
                           , eaql_res_rho = app_res_rho }) }}}

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

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

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

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

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

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

Wrinkles:

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

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

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

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

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

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

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

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

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

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

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

    do_bndr :: p -> p -> p -> ()
do_bndr p
_ p
_ p
_ = ()

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

    do_tv :: () -> TcTyVar -> a
    do_tv :: () -> Id -> a
do_tv ()
_ Id
tv | Id -> Bool
isQLInstTyVar Id
tv = Id -> a
check_tv Id
tv
               | Bool
otherwise        = a
forall a. Monoid a => a
mempty

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

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

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

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

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

    go (TyConApp TyCon
tc1 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_ TcType -> TcType -> TcRn ()
go 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 (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) (TcType -> TcType -> TcRn ()
go TcType
arg1 TcType
arg2)
           ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FunTyFlag -> Bool
isFUNArg FunTyFlag
af1)        (TcType -> TcType -> TcRn ()
go TcType
mult1 TcType
mult2)
           ; TcType -> TcType -> TcRn ()
go 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  (AppTy TcType
t1a TcType
t1b) TcType
ty2
      | Just (TcType
t2a, TcType
t2b) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTyNoView_maybe TcType
ty2
      = do { TcType -> TcType -> TcRn ()
go TcType
t1a TcType
t2a; TcType -> TcType -> TcRn ()
go TcType
t1b TcType
t2b }

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

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

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

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

    go_flexi1 :: Id -> TcType -> TcRn ()
go_flexi1 Id
kappa TcType
ty2  -- ty2 is zonked
      | -- See Note [QuickLook unification] (UQL1)
        UnifyCheckCaller -> Id -> TcType -> Bool
simpleUnifyCheck UnifyCheckCaller
UC_QuickLook Id
kappa TcType
ty2
      = do { 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 (UQL2) in Note [QuickLook unification]
                   --            and (MIV2) in Note [Monomorphise instantiation variables]
           ; let ty2' = TcType -> TcCoercionN -> TcType
mkCastTy TcType
ty2 TcCoercionN
co
           ; traceTc "qlUnify:update" $
             ppr kappa <+> text ":=" <+> ppr ty2
           ; liftZonkM $ writeMetaTyVar kappa ty2' }

      | 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
      where
        kappa_kind :: TcType
kappa_kind = Id -> TcType
tyVarKind Id
kappa
        ty2_kind :: TcType
ty2_kind   = HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
ty2

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

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

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

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

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

  See also (TCAPP2) in Note [tcApp: typechecking applications].

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

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

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

  But in fact we don't attempt this:

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

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

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

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


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

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

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

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

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

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

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

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

It's all grotesquely complicated.
-}

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

tcTagToEnum :: (HsExpr GhcTc, 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 { res_ty <- ZonkM TcType -> TcM TcType
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TcType -> TcM TcType) -> ZonkM TcType -> TcM TcType
forall a b. (a -> b) -> a -> b
$ TcType -> ZonkM TcType
zonkTcType TcType
res_ty

       -- Check that the type is algebraic
       ; case tcSplitTyConApp_maybe res_ty of {
           Maybe (TyCon, 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
       ; fam_envs <- TcM FamInstEnvs
tcGetFamInstEnvs
       ; case tcLookupDataFamInst_maybe fam_envs tc 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)
             tc_expr :: HsExpr GhcTc
tc_expr = (HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps (HsExpr GhcTc
tc_fun', AppCtxt
fun_ctxt) [HsExprArg 'TcpTc
val_arg]
       ; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap HsWrapper
df_wrap HsExpr GhcTc
tc_expr) }}}}}

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

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

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


{- *********************************************************************
*                                                                      *
           Horrible hack for rep-poly unlifted newtypes
*                                                                      *
********************************************************************* -}

{- Note [Eta-expanding rep-poly unlifted newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Any occurrence of a newtype constructor must appear at a known representation.
If the newtype is applied to an argument, then we are done: by (I2) in
Note [Representation polymorphism invariants], the argument has a known
representation, and we are done. So we are left with the situation of an
unapplied newtype constructor. For example:

  type N :: TYPE r -> TYPE r
  newtype N a = MkN a

  ok :: N Int# -> N Int#
  ok = MkN

  bad :: forall r (a :: TYPE r). N (# Int, r #) -> N (# Int, r #)
  bad = MkN

The difficulty is that, unlike the situation described in
Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete,
it is not necessarily the case that we simply need to check the instantiation
of a single variable. Consider for example:

  type RR :: Type -> Type -> RuntimeRep
  type family RR a b where ...

  type T :: forall a -> forall b -> TYPE (RR a b)
  type family T a b where ...

  type M :: forall a -> forall b -> TYPE (RR a b)
  newtype M a b = MkM (T a b)

Now, suppose we instantiate MkM, say with two types X, Y from the environment:

  foo :: T X Y -> M X Y
  foo = MkM @X @Y

we need to check that we can eta-expand MkM, for which we need to know the
representation of its argument, which is "RR X Y".

To do this, in "rejectRepPolyNewtypes", we perform a syntactic representation-
polymorphism check on the instantiated argument of the newtype, and reject
the definition if the representation isn't concrete (in the sense of Note [Concrete types]
in GHC.Tc.Utils.Concrete).

For example, we would accept "ok" above, as "IntRep" is a concrete RuntimeRep.
However, we would reject "foo", because "RR X Y" is not a concrete RuntimeRep.
If we wanted to accept "foo" (performing a PHASE 2 check (in the sense of
Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete), we would have to
significantly re-engineer unlifted newtypes in GHC. Currently, "MkM" has type:

  MkM :: forall a b. T a b %1 -> M a b

However, we should only be able to use MkM when we know the representation of
T a b (which is RR a b). This means that MkM should instead have type:

  MkM :: forall {must_be_conc} a b (co :: RR a b ~# must_be_conc)
      .  T a b |> GRefl Nominal (TYPE co) %1 -> M a b

where "must_be_conc" is a skolem type variable that must be instantiated to a
concrete type, just as in Note [Representation-polymorphism checking built-ins]
in GHC.Tc.Utils.Concrete. This means that any instantiation of "MkM", such as
"MkM @X @Y" from "foo", would create a fresh concrete metavariable "gamma[conc]"
and emit a Wanted constraint

  [W] co :: RR X Y ~# gamma[conc]

However, this all seems like a lot of work for a feature that no one is asking for,
so we decided to keep the much simpler syntactic check. Note that one possible
advantage of this approach is that we should be able to stop skipping
representation-polymorphism checks in the output of the desugarer; see (C) in
Wrinkle [Representation-polymorphic lambdas] in Note [Typechecking data constructors].
-}

-- | Reject any unsaturated use of an unlifted newtype constructor
-- if the representation of its argument isn't known.
--
-- See Note [Eta-expanding rep-poly unlifted newtypes].
rejectRepPolyNewtypes :: (HsExpr GhcTc, AppCtxt)
                      -> TcRhoType
                      -> TcM ()
rejectRepPolyNewtypes :: (HsExpr GhcTc, AppCtxt) -> TcType -> TcRn ()
rejectRepPolyNewtypes (HsExpr GhcTc
fun,AppCtxt
_) TcType
app_res_rho = case HsExpr GhcTc
fun of

  XExpr (ConLikeTc (RealDataCon DataCon
con) [Id]
_ [Scaled TcType]
_)
    -- Check that this is an unsaturated occurrence of a
    -- representation-polymorphic newtype constructor.
    | DataCon -> Bool
isNewDataCon DataCon
con
    , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> Bool
tcHasFixedRuntimeRep (TyCon -> Bool) -> TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
dataConTyCon DataCon
con
    , Just (FunTyFlag
_rem_arg_af, TcType
_rem_arg_mult, TcType
rem_arg_ty, TcType
_nt_res_ty)
        <- TcType -> Maybe (FunTyFlag, TcType, TcType, TcType)
splitFunTy_maybe TcType
app_res_rho
    -> do { let frr_ctxt :: FixedRuntimeRepContext
frr_ctxt = DataCon -> FixedRuntimeRepContext
FRRRepPolyUnliftedNewtype DataCon
con
          ; HasDebugCallStack => FixedRuntimeRepContext -> TcType -> TcRn ()
FixedRuntimeRepContext -> TcType -> TcRn ()
hasFixedRuntimeRep_syntactic FixedRuntimeRepContext
frr_ctxt TcType
rem_arg_ty }

  HsExpr GhcTc
_ -> () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


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