{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}

{-
%
(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.Builtin.Types (multiplicityTy)
import GHC.Tc.Gen.Head
import GHC.Hs
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.TcMType
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType as TcType
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst (substTyWithInScope)
import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType )
import GHC.Core.Type
import GHC.Tc.Types.Evidence
import GHC.Types.Var.Set
import GHC.Builtin.PrimOps( tagToEnumKey )
import GHC.Builtin.Names
import GHC.Driver.Session
import GHC.Types.SrcLoc
import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )
import GHC.Data.Maybe
import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
import qualified GHC.LanguageExtensions as LangExt

import Control.Monad
import Data.Function

#include "GhclibHsVersions.h"

import GHC.Prelude

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

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

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

Some notes relative to the paper

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

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

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

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

Note [Instantiation variables are short lived]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
By the time QL is done, all filled-in occurrences of instantiation
variables have been zonked away (see "Crucial step" in tcValArgs),
and so the constraint /generator/ never subsequently sees a meta-type
variable filled in with a polytype -- a meta type variable stands
(only) for a monotype.  See Section 4.3 "Applications and instantiation"
of the paper.

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

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

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


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

tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
-- Used only to implement :type; see GHC.Tc.Module.tcRnExpr
-- True  <=> instantiate -- return a rho-type
-- False <=> don't instantiate -- return a sigma-type
tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
tcInferSigma Bool
inst (L loc rn_expr)
  | (fun :: (HsExpr GhcRn, AppCtxt)
fun@(HsExpr GhcRn
rn_fun,AppCtxt
_), [HsExprArg 'TcpRn]
rn_args) <- HsExpr GhcRn -> ((HsExpr GhcRn, AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr GhcRn
rn_expr
  = HsExpr GhcRn -> TcM TcSigmaType -> TcM TcSigmaType
forall a. HsExpr GhcRn -> TcRn a -> TcRn a
addExprCtxt HsExpr GhcRn
rn_expr (TcM TcSigmaType -> TcM TcSigmaType)
-> TcM TcSigmaType -> TcM TcSigmaType
forall a b. (a -> b) -> a -> b
$
    SrcSpan -> TcM TcSigmaType -> TcM TcSigmaType
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc      (TcM TcSigmaType -> TcM TcSigmaType)
-> TcM TcSigmaType -> TcM TcSigmaType
forall a b. (a -> b) -> a -> b
$
    do { Bool
do_ql <- HsExpr GhcRn -> TcM Bool
wantQuickLook HsExpr GhcRn
rn_fun
       ; (HsExpr GhcTc
_tc_fun, TcSigmaType
fun_sigma) <- (HsExpr GhcRn, AppCtxt)
-> [HsExprArg 'TcpRn]
-> Maybe TcSigmaType
-> TcM (HsExpr GhcTc, TcSigmaType)
tcInferAppHead (HsExpr GhcRn, AppCtxt)
fun [HsExprArg 'TcpRn]
rn_args Maybe TcSigmaType
forall a. Maybe a
Nothing
       ; (Delta
_delta, [HsExprArg 'TcpInst]
inst_args, TcSigmaType
app_res_sigma) <- Bool
-> Bool
-> (HsExpr GhcRn, AppCtxt)
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
tcInstFun Bool
do_ql Bool
inst (HsExpr GhcRn, AppCtxt)
fun TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args
       ; [HsExprArg 'TcpTc]
_tc_args <- Bool -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
do_ql [HsExprArg 'TcpInst]
inst_args
       ; TcSigmaType -> TcM TcSigmaType
forall (m :: * -> *) a. Monad m => a -> m a
return TcSigmaType
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           -- HsRecFld: 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 esay 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 arument 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 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, HsRecFld, and ExprWithTySig
   Otherwise, delegate back to tcExpr, which
     infers an (instantiated) TcRhoType

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

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

4. Use quickLookResultType to take a quick look at the result type,
   when in checking mode.  This is the shaded part of APP-Downarrow
   in Fig 5.

5. Use tcValArgs to typecheck the value arguments

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


Some cases that /won't/ work:

1. Consider this (which uses visible type application):

    (let { f :: forall a. a -> a; f x = x } in f) @Int

   Since 'let' is not among the special cases for tcInferAppHead,
   we'll delegate back to tcExpr, which will instantiate f's type
   and the type application to @Int will fail.  Too bad!

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

* ($): For a long time GHC has had a special typing rule for ($), that
  allows it to type (runST $ foo), which requires impredicative instantiation
  of ($), without language flags.  It's a bit ad-hoc, but it's been that
  way for ages.  Using quickLookIds 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.
-}

tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
-- See Note [tcApp: typechecking applications]
tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
tcApp HsExpr GhcRn
rn_expr ExpRhoType
exp_res_ty
  | (fun :: (HsExpr GhcRn, AppCtxt)
fun@(HsExpr GhcRn
rn_fun, AppCtxt
fun_ctxt), [HsExprArg 'TcpRn]
rn_args) <- HsExpr GhcRn -> ((HsExpr GhcRn, AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr GhcRn
rn_expr
  = do { (HsExpr GhcTc
tc_fun, TcSigmaType
fun_sigma) <- (HsExpr GhcRn, AppCtxt)
-> [HsExprArg 'TcpRn]
-> Maybe TcSigmaType
-> TcM (HsExpr GhcTc, TcSigmaType)
tcInferAppHead (HsExpr GhcRn, AppCtxt)
fun [HsExprArg 'TcpRn]
rn_args
                                    (ExpRhoType -> Maybe TcSigmaType
checkingExpType_maybe ExpRhoType
exp_res_ty)

       -- Instantiate
       ; Bool
do_ql <- HsExpr GhcRn -> TcM Bool
wantQuickLook HsExpr GhcRn
rn_fun
       ; (Delta
delta, [HsExprArg 'TcpInst]
inst_args, TcSigmaType
app_res_rho) <- Bool
-> Bool
-> (HsExpr GhcRn, AppCtxt)
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
tcInstFun Bool
do_ql Bool
True (HsExpr GhcRn, AppCtxt)
fun TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args

       -- Quick look at result
       ; Bool -> Delta -> TcSigmaType -> ExpRhoType -> TcM ()
quickLookResultType Bool
do_ql Delta
delta TcSigmaType
app_res_rho ExpRhoType
exp_res_ty

       ; DumpFlag -> TcM () -> TcM ()
forall gbl lcl. DumpFlag -> TcRnIf gbl lcl () -> TcRnIf gbl lcl ()
whenDOptM DumpFlag
Opt_D_dump_tc_trace (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
         do { [HsExprArg 'TcpInst]
inst_args <- (HsExprArg 'TcpInst
 -> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpInst))
-> [HsExprArg 'TcpInst]
-> IOEnv (Env TcGblEnv TcLclEnv) [HsExprArg 'TcpInst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpInst)
zonkArg [HsExprArg 'TcpInst]
inst_args  -- Only when tracing
            ; String -> SDoc -> TcM ()
traceTc String
"tcApp" ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"rn_fun"       SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun
                               , String -> SDoc
text String
"inst_args"    SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
brackets ((HsExprArg 'TcpInst -> SDoc) -> [HsExprArg 'TcpInst] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas HsExprArg 'TcpInst -> SDoc
pprHsExprArgTc [HsExprArg 'TcpInst]
inst_args)
                               , String -> SDoc
text String
"do_ql:  "     SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
do_ql
                               , String -> SDoc
text String
"fun_sigma:  " SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_sigma
                               , String -> SDoc
text String
"delta:      " SDoc -> SDoc -> SDoc
<+> Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta
                               , String -> SDoc
text String
"app_res_rho:" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
app_res_rho
                               , String -> SDoc
text String
"exp_res_ty:"  SDoc -> SDoc -> SDoc
<+> ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
exp_res_ty
                               , String -> SDoc
text String
"rn_expr:"     SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_expr ]) }

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

       -- Zonk the result type, to ensure that we substitute out
       -- any filled-in instantiation variable before calling tcWrapResultMono
       -- In the Check case, this isn't really necessary, because tcWrapResultMono
       -- just drops to tcUnify; but in the Infer case a filled-in instantiation
       -- variable might perhaps escape into the constraint generator. The safe
       -- thing to do is to any instantaition variables away.
       -- See Note [Instantiation variables are short lived]
       ; TcSigmaType
app_res_rho <- Bool -> TcSigmaType -> TcM TcSigmaType
zonkQuickLook Bool
do_ql TcSigmaType
app_res_rho

       -- Special case for tagToEnum#
       ; if HsExpr GhcRn -> Bool
isTagToEnum HsExpr GhcRn
rn_fun
         then HsExpr GhcRn
-> HsExpr GhcTc
-> AppCtxt
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcRn
rn_expr HsExpr GhcTc
tc_fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
tc_args TcSigmaType
app_res_rho ExpRhoType
exp_res_ty
         else

    do { -- Reconstruct
       ; let tc_expr :: HsExpr GhcTc
tc_expr = HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps HsExpr GhcTc
tc_fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
tc_args

             -- Set a context for the helpful
             --    "Probably cause: f applied to too many args"
             -- But not in generated code, where we don't want
             -- to mention internal (rebindable syntax) function names
             set_res_ctxt :: TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
set_res_ctxt TcM (HsExpr GhcTc)
thing_inside
                | [HsExprArg 'TcpTc] -> Bool
forall (p :: TcPass). [HsExprArg p] -> Bool
insideExpansion [HsExprArg 'TcpTc]
tc_args
                = TcM (HsExpr GhcTc)
thing_inside
                | Bool
otherwise
                = HsExpr GhcTc
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
-> TcM (HsExpr GhcTc)
forall a.
HsExpr GhcTc
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM a
-> TcM a
addFunResCtxt HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args TcSigmaType
app_res_rho ExpRhoType
exp_res_ty TcM (HsExpr GhcTc)
thing_inside

       -- Wrap the result
       ; TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
set_res_ctxt (TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc))
-> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$ HsExpr GhcRn
-> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResultMono HsExpr GhcRn
rn_expr HsExpr GhcTc
tc_expr TcSigmaType
app_res_rho ExpRhoType
exp_res_ty } }

--------------------
wantQuickLook :: HsExpr GhcRn -> TcM Bool
-- GHC switches on impredicativity all the time for ($)
wantQuickLook :: HsExpr GhcRn -> TcM Bool
wantQuickLook (HsVar XVar GhcRn
_ (L _ f))
  | Name -> Unique
forall a. Uniquable a => a -> Unique
getUnique Name
f Unique -> [Unique] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Unique]
quickLookKeys = Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
wantQuickLook HsExpr GhcRn
_                      = Extension -> TcM Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes

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

zonkQuickLook :: Bool -> TcType -> TcM TcType
-- After all Quick Look unifications are done, zonk to ensure that all
-- instantiation variables are substituted away
--
-- So far as the paper is concerned, this step applies
-- the poly-substitution Theta, learned by QL, so that we
-- "see" the polymorphism in that type
--
-- In implementation terms this ensures that no unification variable
-- linger on that have been filled in with a polytype
zonkQuickLook :: Bool -> TcSigmaType -> TcM TcSigmaType
zonkQuickLook Bool
do_ql TcSigmaType
ty
  | Bool
do_ql     = TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
ty
  | Bool
otherwise = TcSigmaType -> TcM TcSigmaType
forall (m :: * -> *) a. Monad m => a -> m a
return TcSigmaType
ty

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



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

    tc_arg eva :: HsExprArg 'TcpInst
eva@(EValArg { eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = EValArg 'TcpInst
arg, eva_arg_ty :: forall (p :: TcPass). HsExprArg p -> XEVAType p
eva_arg_ty = Scaled mult arg_ty
                        , eva_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
eva_ctxt = AppCtxt
ctxt })
      = do { -- Crucial step: expose QL results before checking arg_ty
             -- So far as the paper is concerned, this step applies
             -- the poly-substitution Theta, learned by QL, so that we
             -- "see" the polymorphism in that argument type. E.g.
             --    (:) e ids, where ids :: [forall a. a->a]
             --                     (:) :: forall p. p->[p]->[p]
             -- Then Theta = [p :-> forall a. a->a], and we want
             -- to check 'e' with expected type (forall a. a->a)
             -- See Note [Instantiation variables are short lived]
             TcSigmaType
arg_ty <- Bool -> TcSigmaType -> TcM TcSigmaType
zonkQuickLook Bool
do_ql TcSigmaType
arg_ty

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

           ; HsExprArg 'TcpTc
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsExprArg 'TcpInst
eva { eva_arg :: EValArg 'TcpTc
eva_arg    = LHsExpr (GhcPass (XPass 'TcpTc)) -> EValArg 'TcpTc
forall (p :: TcPass). LHsExpr (GhcPass (XPass p)) -> EValArg p
ValArg Located (HsExpr GhcTc)
LHsExpr (GhcPass (XPass 'TcpTc))
arg'
                         , eva_arg_ty :: XEVAType 'TcpTc
eva_arg_ty = TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
mult TcSigmaType
arg_ty }) }

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

tcEValArg AppCtxt
ctxt (ValArgQL { va_expr :: EValArg 'TcpInst -> LHsExpr GhcRn
va_expr = larg :: LHsExpr GhcRn
larg@(L arg_loc _)
                         , va_fun :: EValArg 'TcpInst -> (HsExpr GhcTc, AppCtxt)
va_fun = (HsExpr GhcTc
inner_fun, AppCtxt
fun_ctxt)
                         , va_args :: EValArg 'TcpInst -> [HsExprArg 'TcpInst]
va_args = [HsExprArg 'TcpInst]
inner_args
                         , va_ty :: EValArg 'TcpInst -> TcSigmaType
va_ty = TcSigmaType
app_res_rho }) TcSigmaType
exp_arg_sigma
  = AppCtxt
-> LHsExpr GhcRn
-> TcM (Located (HsExpr GhcTc))
-> TcM (Located (HsExpr GhcTc))
forall a. AppCtxt -> LHsExpr GhcRn -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr GhcRn
larg (TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc)))
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a b. (a -> b) -> a -> b
$
    do { String -> SDoc -> TcM ()
traceTc String
"tcEValArgQL {" ([SDoc] -> SDoc
vcat [ HsExpr GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcTc
inner_fun SDoc -> SDoc -> SDoc
<+> [HsExprArg 'TcpInst] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpInst]
inner_args ])
       ; [HsExprArg 'TcpTc]
tc_args <- Bool -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
True [HsExprArg 'TcpInst]
inner_args
       ; TcCoercionN
co      <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
forall a. Maybe a
Nothing TcSigmaType
app_res_rho TcSigmaType
exp_arg_sigma
       ; String -> SDoc -> TcM ()
traceTc String
"tcEValArg }" SDoc
empty
       ; Located (HsExpr GhcTc) -> TcM (Located (HsExpr GhcTc))
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpan -> HsExpr GhcTc -> Located (HsExpr GhcTc)
forall l e. l -> e -> GenLocated l e
L SrcSpan
arg_loc (HsExpr GhcTc -> Located (HsExpr GhcTc))
-> HsExpr GhcTc -> Located (HsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$ TcCoercionN -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrapCo TcCoercionN
co (HsExpr GhcTc -> HsExpr GhcTc) -> HsExpr GhcTc -> HsExpr GhcTc
forall a b. (a -> b) -> a -> b
$
                 HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps HsExpr GhcTc
inner_fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
tc_args) }

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

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

tcInstFun :: Bool   -- True  <=> Do quick-look
          -> Bool   -- False <=> Instantiate only /inferred/ variables at the end
                    --           so may return a sigma-typex
                    -- 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 GhcRn, AppCtxt)        -- Error messages only
          -> TcSigmaType -> [HsExprArg 'TcpRn]
          -> TcM ( Delta
                 , [HsExprArg 'TcpInst]
                 , TcSigmaType )
-- This function implements the |-inst judgement in Fig 4, plus the
-- modification in Fig 5, of the QL paper:
-- "A quick look at impredicativity" (ICFP'20).
tcInstFun :: Bool
-> Bool
-> (HsExpr GhcRn, AppCtxt)
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
tcInstFun Bool
do_ql Bool
inst_final (HsExpr GhcRn
rn_fun, AppCtxt
fun_ctxt) TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args
  = do { String -> SDoc -> TcM ()
traceTc String
"tcInstFun" ([SDoc] -> SDoc
vcat [ HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun, TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_sigma
                                   , String -> SDoc
text String
"args:" SDoc -> SDoc -> SDoc
<+> [HsExprArg 'TcpRn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpRn]
rn_args
                                   , String -> SDoc
text String
"do_ql" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
do_ql ])
       ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
emptyVarSet [] [] TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args }
  where
    fun_loc :: SrcSpan
fun_loc  = AppCtxt -> SrcSpan
appCtxtLoc AppCtxt
fun_ctxt
    fun_orig :: CtOrigin
fun_orig = HsExpr GhcRn -> CtOrigin
exprCtOrigin (case AppCtxt
fun_ctxt of
                               VAExpansion HsExpr GhcRn
e SrcSpan
_ -> HsExpr GhcRn
e
                               VACall HsExpr GhcRn
e Int
_ SrcSpan
_    -> HsExpr GhcRn
e)
    set_fun_ctxt :: IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
set_fun_ctxt IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
thing_inside
      | Bool -> Bool
not (SrcSpan -> Bool
isGoodSrcSpan SrcSpan
fun_loc)   -- noSrcSpan => no arguments
      = IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
thing_inside                  -- => context is already set
      | Bool
otherwise
      = SrcSpan
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
fun_loc (IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
 -> IOEnv
      (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType))
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
        case AppCtxt
fun_ctxt of
          VAExpansion HsExpr GhcRn
orig SrcSpan
_ -> HsExpr GhcRn
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
forall a. HsExpr GhcRn -> TcRn a -> TcRn a
addExprCtxt HsExpr GhcRn
orig IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
thing_inside
          VACall {}          -> IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
thing_inside

    herald :: SDoc
herald = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"The function" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun)
                 , String -> SDoc
text String
"is applied to"]

    -- 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 GhcRn
rn_fun of
          HsUnboundVar {} -> Bool
True
          HsExpr GhcRn
_               -> Bool
False

    inst_all :: ArgFlag -> Bool
    inst_all :: ArgFlag -> Bool
inst_all (Invisible {}) = Bool
True
    inst_all ArgFlag
Required       = Bool
False

    inst_inferred :: ArgFlag -> Bool
    inst_inferred :: ArgFlag -> Bool
inst_inferred (Invisible Specificity
InferredSpec)  = Bool
True
    inst_inferred (Invisible Specificity
SpecifiedSpec) = Bool
False
    inst_inferred ArgFlag
Required                  = Bool
False

    inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
    inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
inst_fun [] | Bool
inst_final  = ArgFlag -> Bool
inst_all
                | Bool
otherwise   = ArgFlag -> Bool
inst_inferred
    inst_fun (EValArg {} : [HsExprArg 'TcpRn]
_) = ArgFlag -> Bool
inst_all
    inst_fun [HsExprArg 'TcpRn]
_                = ArgFlag -> Bool
inst_inferred

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

    -- go: If fun_ty=kappa, look it up in Theta
    go :: Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
      | Just TcTyVar
kappa <- TcSigmaType -> Maybe TcTyVar
tcGetTyVar_maybe TcSigmaType
fun_ty
      , TcTyVar
kappa TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta
      = do { MetaDetails
cts <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
kappa
           ; case MetaDetails
cts of
                Indirect TcSigmaType
fun_ty' -> Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go  Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty' [HsExprArg 'TcpRn]
args
                MetaDetails
Flexi            -> Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty  [HsExprArg 'TcpRn]
args }
     | Bool
otherwise
     = Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args

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

    -- Rule IALL from Fig 4 of the QL paper
    -- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
    go1 :: Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
      | ([TcTyVar]
tvs,   TcSigmaType
body1) <- (ArgFlag -> Bool) -> TcSigmaType -> ([TcTyVar], TcSigmaType)
tcSplitSomeForAllTyVars ([HsExprArg 'TcpRn] -> ArgFlag -> Bool
inst_fun [HsExprArg 'TcpRn]
args) TcSigmaType
fun_ty
      , (ThetaType
theta, TcSigmaType
body2) <- TcSigmaType -> (ThetaType, TcSigmaType)
tcSplitPhiTy TcSigmaType
body1
      , Bool -> Bool
not ([TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
      = do { ([TcTyVar]
inst_tvs, HsWrapper
wrap, TcSigmaType
fun_rho) <- IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
set_fun_ctxt (IOEnv (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
 -> IOEnv
      (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType))
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
                                          CtOrigin
-> [TcTyVar]
-> ThetaType
-> TcSigmaType
-> IOEnv
     (Env TcGblEnv TcLclEnv) ([TcTyVar], HsWrapper, TcSigmaType)
instantiateSigma CtOrigin
fun_orig [TcTyVar]
tvs ThetaType
theta TcSigmaType
body2
                 -- set_fun_ctxt: important for the class constraints
                 -- that may be emitted from instantiating fun_sigma
           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go (Delta
delta Delta -> [TcTyVar] -> Delta
`extendVarSetList` [TcTyVar]
inst_tvs)
                (HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
addArgWrap HsWrapper
wrap [HsExprArg 'TcpInst]
acc) [Scaled TcSigmaType]
so_far TcSigmaType
fun_rho [HsExprArg 'TcpRn]
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
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
_ TcSigmaType
fun_ty []
       = do { String -> SDoc -> TcM ()
traceTc String
"tcInstFun:ret" (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_ty)
            ; (Delta, [HsExprArg 'TcpInst], TcSigmaType)
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. [a] -> [a]
reverse [HsExprArg 'TcpInst]
acc, TcSigmaType
fun_ty) }

    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty (EWrap EWrap
w : [HsExprArg 'TcpRn]
args)
      = Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta (EWrap -> HsExprArg 'TcpInst
forall (p :: TcPass). EWrap -> HsExprArg p
EWrap EWrap
w HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args

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

    -- Rule ITYARG from Fig 4 of the QL paper
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty ( ETypeArg { eva_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
eva_ctxt = AppCtxt
ctxt, eva_hs_ty :: forall (p :: TcPass). HsExprArg p -> LHsWcType GhcRn
eva_hs_ty = LHsWcType GhcRn
hs_ty }
                                : [HsExprArg 'TcpRn]
rest_args )
      | Bool
fun_is_out_of_scope   -- See Note [VTA for out-of-scope functions]
      = Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
rest_args

      | Bool
otherwise
      = do { (TcSigmaType
ty_arg, TcSigmaType
inst_ty) <- TcSigmaType -> LHsWcType GhcRn -> TcM (TcSigmaType, TcSigmaType)
tcVTA TcSigmaType
fun_ty LHsWcType GhcRn
hs_ty
           ; let arg' :: HsExprArg 'TcpInst
arg' = ETypeArg :: forall (p :: TcPass).
AppCtxt -> LHsWcType GhcRn -> XETAType p -> HsExprArg p
ETypeArg { eva_ctxt :: AppCtxt
eva_ctxt = AppCtxt
ctxt, eva_hs_ty :: LHsWcType GhcRn
eva_hs_ty = LHsWcType GhcRn
hs_ty, eva_ty :: XETAType 'TcpInst
eva_ty = TcSigmaType
XETAType 'TcpInst
ty_arg }
           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta (HsExprArg 'TcpInst
arg' HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) [Scaled TcSigmaType]
so_far TcSigmaType
inst_ty [HsExprArg 'TcpRn]
rest_args }

    -- Rule IVAR from Fig 4 of the QL paper:
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty args :: [HsExprArg 'TcpRn]
args@(EValArg {} : [HsExprArg 'TcpRn]
_)
      | Just TcTyVar
kappa <- TcSigmaType -> Maybe TcTyVar
tcGetTyVar_maybe TcSigmaType
fun_ty
      , TcTyVar
kappa TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta
      = -- Function type was of form   f :: forall a b. t1 -> t2 -> b
        -- with 'b', one of the quantified type variables, in the corner
        -- but the call applies it to three or more value args.
        -- Suppose b is instantiated by kappa.  Then we want to make fresh
        -- instantiation variables nu1, nu2, and set kappa := nu1 -> nu2
        --
        -- In principle what is happening here is not unlike matchActualFunTysRho
        -- but there are many small differences:
        --   - We know that the function type in unfilled meta-tyvar
        --     matchActualFunTysRho is much more general, has a loop, etc.
        --   - We must be sure to actually update the variable right now,
        --     not defer in any way, because this is a QL instantiation variable.
        --   - We need the freshly allocated unification variables, to extend
        --     delta with.
        -- It's easier just to do the job directly here.
        do { let valArgsCount :: Int
valArgsCount = [HsExprArg 'TcpRn] -> Int
forall (id :: TcPass). [HsExprArg id] -> Int
countLeadingValArgs [HsExprArg 'TcpRn]
args
           ; [TcTyVar]
arg_nus <- Int
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
-> IOEnv (Env TcGblEnv TcLclEnv) [TcTyVar]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
valArgsCount IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newOpenFlexiTyVar
             -- We need variables for multiplicity (#18731)
             -- Otherwise, 'undefined x' wouldn't be linear in x
           ; ThetaType
mults   <- Int -> TcM TcSigmaType -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
valArgsCount (TcSigmaType -> TcM TcSigmaType
newFlexiTyVarTy TcSigmaType
multiplicityTy)
           ; TcTyVar
res_nu  <- IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newOpenFlexiTyVar
           ; TcCoercionN
kind_co <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyKind Maybe SDoc
forall a. Maybe a
Nothing TcSigmaType
liftedTypeKind (TcTyVar -> TcSigmaType
tyVarKind TcTyVar
kappa)
           ; let delta' :: Delta
delta'  = Delta
delta Delta -> [TcTyVar] -> Delta
`extendVarSetList` (TcTyVar
res_nuTcTyVar -> [TcTyVar] -> [TcTyVar]
forall a. a -> [a] -> [a]
:[TcTyVar]
arg_nus)
                 arg_tys :: ThetaType
arg_tys = [TcTyVar] -> ThetaType
mkTyVarTys [TcTyVar]
arg_nus
                 res_ty :: TcSigmaType
res_ty  = TcTyVar -> TcSigmaType
mkTyVarTy TcTyVar
res_nu
                 fun_ty' :: TcSigmaType
fun_ty' = [Scaled TcSigmaType] -> TcSigmaType -> TcSigmaType
mkVisFunTys (String
-> (TcSigmaType -> TcSigmaType -> Scaled TcSigmaType)
-> ThetaType
-> ThetaType
-> [Scaled TcSigmaType]
forall a b c. String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"tcInstFun" TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
mkScaled ThetaType
mults ThetaType
arg_tys) TcSigmaType
res_ty
                 co_wrap :: HsWrapper
co_wrap = TcCoercionN -> HsWrapper
mkWpCastN (Role -> TcSigmaType -> TcCoercionN -> TcCoercionN
mkTcGReflLeftCo Role
Nominal TcSigmaType
fun_ty' TcCoercionN
kind_co)
                 acc' :: [HsExprArg 'TcpInst]
acc'    = HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
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'
           ; TcTyVar -> TcSigmaType -> TcM ()
writeMetaTyVar TcTyVar
kappa (TcSigmaType -> TcCoercionN -> TcSigmaType
mkCastTy TcSigmaType
fun_ty' TcCoercionN
kind_co)
                 -- kappa is uninstantiated ('go' already checked that)
           ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta' [HsExprArg 'TcpInst]
acc' [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty' [HsExprArg 'TcpRn]
args }

    -- Rule IARG from Fig 4 of the QL paper:
    go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty
        (eva :: HsExprArg 'TcpRn
eva@(EValArg { eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = ValArg LHsExpr (GhcPass (XPass 'TcpRn))
arg, eva_ctxt :: forall (p :: TcPass). HsExprArg p -> AppCtxt
eva_ctxt = AppCtxt
ctxt })  : [HsExprArg 'TcpRn]
rest_args)
      = do { (HsWrapper
wrap, Scaled TcSigmaType
arg_ty, TcSigmaType
res_ty) <- SDoc
-> Maybe SDoc
-> (Int, [Scaled TcSigmaType])
-> TcSigmaType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
matchActualFunTySigma SDoc
herald
                                          (SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun))
                                          (Int
n_val_args, [Scaled TcSigmaType]
so_far) TcSigmaType
fun_ty
          ; (Delta
delta', EValArg 'TcpInst
arg') <- if Bool
do_ql
                              then AppCtxt
-> LHsExpr GhcRn
-> TcM (Delta, EValArg 'TcpInst)
-> TcM (Delta, EValArg 'TcpInst)
forall a. AppCtxt -> LHsExpr GhcRn -> TcM a -> TcM a
addArgCtxt AppCtxt
ctxt LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpRn))
arg (TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst))
-> TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a b. (a -> b) -> a -> b
$
                                   -- Context needed for constraints
                                   -- generated by calls in arg
                                   Delta
-> LHsExpr GhcRn
-> Scaled TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg Delta
delta LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpRn))
arg Scaled TcSigmaType
arg_ty
                              else (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, LHsExpr (GhcPass (XPass 'TcpInst)) -> EValArg 'TcpInst
forall (p :: TcPass). LHsExpr (GhcPass (XPass p)) -> EValArg p
ValArg LHsExpr (GhcPass (XPass 'TcpRn))
LHsExpr (GhcPass (XPass 'TcpInst))
arg)
          ; let acc' :: [HsExprArg 'TcpInst]
acc' = HsExprArg 'TcpRn
eva { eva_arg :: EValArg 'TcpInst
eva_arg = EValArg 'TcpInst
arg', eva_arg_ty :: XEVAType 'TcpInst
eva_arg_ty = Scaled TcSigmaType
XEVAType 'TcpInst
arg_ty }
                       HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
addArgWrap HsWrapper
wrap [HsExprArg 'TcpInst]
acc
          ; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta' [HsExprArg 'TcpInst]
acc' (Scaled TcSigmaType
arg_tyScaled TcSigmaType -> [Scaled TcSigmaType] -> [Scaled TcSigmaType]
forall a. a -> [a] -> [a]
:[Scaled TcSigmaType]
so_far) TcSigmaType
res_ty [HsExprArg 'TcpRn]
rest_args }


addArgCtxt :: AppCtxt -> LHsExpr GhcRn
           -> TcM a -> TcM a
-- Adds a "In the third argument of f, namely blah"
-- context, unless we are in generated code, in which case
-- use "In the expression: arg"
---See Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
addArgCtxt :: AppCtxt -> LHsExpr GhcRn -> TcM a -> TcM a
addArgCtxt (VACall HsExpr GhcRn
fun Int
arg_no SrcSpan
_) (L arg_loc arg) TcM a
thing_inside
  = SrcSpan -> TcM a -> TcM a
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
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 GhcRn -> HsExpr GhcRn -> Int -> SDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> SDoc
funAppCtxt HsExpr GhcRn
fun HsExpr GhcRn
arg Int
arg_no) (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
    TcM a
thing_inside

addArgCtxt (VAExpansion {}) (L arg_loc arg) TcM a
thing_inside
  = SrcSpan -> TcM a -> TcM a
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
arg_loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
    HsExpr GhcRn -> TcM a -> TcM a
forall a. HsExpr GhcRn -> TcRn a -> TcRn a
addExprCtxt HsExpr GhcRn
arg    (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$  -- Auto-suppressed if arg_loc is generated
    TcM a
thing_inside

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

tcVTA :: 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 :: TcSigmaType -> LHsWcType GhcRn -> TcM (TcSigmaType, TcSigmaType)
tcVTA TcSigmaType
fun_ty LHsWcType GhcRn
hs_ty
  | Just (TyVarBinder
tvb, TcSigmaType
inner_ty) <- TcSigmaType -> Maybe (TyVarBinder, TcSigmaType)
tcSplitForAllTyVarBinder_maybe TcSigmaType
fun_ty
  , TyVarBinder -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag TyVarBinder
tvb ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ArgFlag
Specified
    -- It really can't be Inferred, because we've just
    -- instantiated those. But, oddly, it might just be Required.
    -- See Note [Required quantifiers in the type of a term]
  = do { let tv :: TcTyVar
tv   = TyVarBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
tvb
             kind :: TcSigmaType
kind = TcTyVar -> TcSigmaType
tyVarKind TcTyVar
tv
       ; TcSigmaType
ty_arg <- LHsWcType GhcRn -> TcSigmaType -> TcM TcSigmaType
tcHsTypeApp LHsWcType GhcRn
hs_ty TcSigmaType
kind

       ; TcSigmaType
inner_ty <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
inner_ty
             -- See Note [Visible type application zonk]

       ; let in_scope :: InScopeSet
in_scope  = Delta -> InScopeSet
mkInScopeSet (ThetaType -> Delta
tyCoVarsOfTypes [TcSigmaType
fun_ty, TcSigmaType
ty_arg])
             insted_ty :: TcSigmaType
insted_ty = InScopeSet -> [TcTyVar] -> ThetaType -> TcSigmaType -> TcSigmaType
substTyWithInScope InScopeSet
in_scope [TcTyVar
tv] [TcSigmaType
ty_arg] TcSigmaType
inner_ty
                         -- NB: tv and ty_arg have the same kind, so this
                         --     substitution is kind-respecting
       ; String -> SDoc -> TcM ()
traceTc String
"VTA" ([SDoc] -> SDoc
vcat [TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv, TcSigmaType -> SDoc
debugPprType TcSigmaType
kind
                             , TcSigmaType -> SDoc
debugPprType TcSigmaType
ty_arg
                             , TcSigmaType -> SDoc
debugPprType (HasDebugCallStack => TcSigmaType -> TcSigmaType
TcSigmaType -> TcSigmaType
tcTypeKind TcSigmaType
ty_arg)
                             , TcSigmaType -> SDoc
debugPprType TcSigmaType
inner_ty
                             , TcSigmaType -> SDoc
debugPprType TcSigmaType
insted_ty ])
       ; (TcSigmaType, TcSigmaType) -> TcM (TcSigmaType, TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType
ty_arg, TcSigmaType
insted_ty) }

  | Bool
otherwise
  = do { (TidyEnv
_, TcSigmaType
fun_ty) <- TidyEnv -> TcSigmaType -> TcM (TidyEnv, TcSigmaType)
zonkTidyTcType TidyEnv
emptyTidyEnv TcSigmaType
fun_ty
       ; SDoc -> TcM (TcSigmaType, TcSigmaType)
forall a. SDoc -> TcRn a
failWith (SDoc -> TcM (TcSigmaType, TcSigmaType))
-> SDoc -> TcM (TcSigmaType, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
         String -> SDoc
text String
"Cannot apply expression of type" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_ty) SDoc -> SDoc -> SDoc
$$
         String -> SDoc
text String
"to a visible type argument" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (HsWildCardBndrs GhcRn (Located (HsType GhcRn)) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsWildCardBndrs GhcRn (Located (HsType GhcRn))
LHsWcType GhcRn
hs_ty) }

{- Note [Required quantifiers in the type of a term]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#15859)

  data A k :: k -> Type      -- A      :: forall k -> k -> Type
  type KindOf (a :: k) = k   -- KindOf :: forall k. k -> Type
  a = (undefined :: KindOf A) @Int

With ImpredicativeTypes (thin ice, I know), we instantiate
KindOf at type (forall k -> k -> Type), so
  KindOf A = forall k -> k -> Type
whose first argument is Required

We want to reject this type application to Int, but in earlier
GHCs we had an ASSERT that Required could not occur here.

The ice is thin; c.f. Note [No Required TyCoBinder in terms]
in GHC.Core.TyCo.Rep.

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've already inferred the type of
the function (in tcInferAppHead), so 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.

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 [Visible type application zonk]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).

* tcHsTypeApp only guarantees that
    - ty_arg is zonked
    - kind(zonk(tv)) = kind(ty_arg)
  (checkExpectedKind zonks as it goes).

So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
and inner_ty. Otherwise we can build an ill-kinded type. An example was #14158,
where we had:
   id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
and we had the visible type application
  id @(->)

* We instantiated k := kappa, yielding
    forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
* That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
  Here q1 :: RuntimeRep
* Now we substitute
     cat  :->  (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
  but we must first zonk the inner_ty to get
      forall (a :: TYPE q1). cat a a
  so that the result of substitution is well-kinded
  Failing to do so led to #14158.

-}

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

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

Wrinkles:

* We avoid zonking, so quickLookArg thereby sees the argument type /before/
  the QL substitution Theta is applied to it. So we achieve argument-order
  independence for free (see 5.7 in the paper).

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

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

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

              -- This top-level zonk step, which is the reason
              -- we need a local 'go' loop, is subtle
              -- See Section 9 of the QL paper
              | Just TcTyVar
kappa <- TcSigmaType -> Maybe TcTyVar
tcGetTyVar_maybe TcSigmaType
arg_ty
              , TcTyVar
kappa TcTyVar -> Delta -> Bool
`elemVarSet` Delta
delta
              = do { MetaDetails
info <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
kappa
                   ; case MetaDetails
info of
                       Indirect TcSigmaType
arg_ty' -> TcSigmaType -> TcM (Delta, EValArg 'TcpInst)
go TcSigmaType
arg_ty'
                       MetaDetails
Flexi            -> Bool
-> Delta
-> LHsExpr GhcRn
-> TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta LHsExpr GhcRn
larg TcSigmaType
arg_ty }

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

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

quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaType
              -> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 :: Bool
-> Delta
-> LHsExpr GhcRn
-> TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta larg :: LHsExpr GhcRn
larg@(L _ arg) TcSigmaType
arg_ty
  = do { let (fun :: (HsExpr GhcRn, AppCtxt)
fun@(HsExpr GhcRn
rn_fun, AppCtxt
fun_ctxt), [HsExprArg 'TcpRn]
rn_args) = HsExpr GhcRn -> ((HsExpr GhcRn, AppCtxt), [HsExprArg 'TcpRn])
splitHsApps HsExpr GhcRn
arg
       ; Maybe (HsExpr GhcTc, TcSigmaType)
mb_fun_ty <- HsExpr GhcRn
-> [HsExprArg 'TcpRn]
-> Maybe TcSigmaType
-> TcM (Maybe (HsExpr GhcTc, TcSigmaType))
tcInferAppHead_maybe HsExpr GhcRn
rn_fun [HsExprArg 'TcpRn]
rn_args (TcSigmaType -> Maybe TcSigmaType
forall a. a -> Maybe a
Just TcSigmaType
arg_ty)
       ; String -> SDoc -> TcM ()
traceTc String
"quickLookArg 1" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"arg:" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
arg
              , String -> SDoc
text String
"head:" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Maybe (HsExpr GhcTc, TcSigmaType) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe (HsExpr GhcTc, TcSigmaType)
mb_fun_ty
              , String -> SDoc
text String
"args:" SDoc -> SDoc -> SDoc
<+> [HsExprArg 'TcpRn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpRn]
rn_args ]

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

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

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

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

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

----------------
quickLookResultType :: Bool -> Delta -> 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 :: Bool -> Delta -> TcSigmaType -> ExpRhoType -> TcM ()
quickLookResultType Bool
do_ql Delta
delta TcSigmaType
app_res_rho ExpRhoType
exp_res_ty
  | Bool
do_ql
  , Bool -> Bool
not (Delta -> Bool
isEmptyVarSet Delta
delta)  -- Optimisation only
  , Just TcSigmaType
exp_rho <- ExpRhoType -> Maybe TcSigmaType
checkingExpType_maybe ExpRhoType
exp_res_ty
                               -- In checking mode only
  = Delta -> TcSigmaType -> TcSigmaType -> TcM ()
qlUnify Delta
delta TcSigmaType
app_res_rho TcSigmaType
exp_rho
  | Bool
otherwise
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

    go (Delta, Delta)
bvs (CastTy TcSigmaType
ty1 TcCoercionN
_) TcSigmaType
ty2 = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
ty1 TcSigmaType
ty2
    go (Delta, Delta)
bvs TcSigmaType
ty1 (CastTy TcSigmaType
ty2 TcCoercionN
_) = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
ty1 TcSigmaType
ty2

    go (Delta, Delta)
_ (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
      | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2 -- See GHC.Tc.Utils.Unify
      = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- Note [Expanding synonyms during unification]

    -- Now, and only now, expand synonyms
    go (Delta, Delta)
bvs TcSigmaType
rho1 TcSigmaType
rho2
      | Just TcSigmaType
rho1 <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
rho1 = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
rho1 TcSigmaType
rho2
      | Just TcSigmaType
rho2 <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
rho2 = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
rho1 TcSigmaType
rho2

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

    -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
    -- and         (c1 => res1) ~   (c2 => res2)
    -- But for the latter we only learn instantiation info from t1~t2
    -- We look at the multiplicity too, although the chances of getting
    -- impredicative instantiation info from there seems...remote.
    go (Delta, Delta)
bvs (FunTy { ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
af1, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg1, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res1, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
mult1 })
           (FunTy { ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
af2, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg2, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res2, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
mult2 })
      | AnonArgFlag
af1 AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
af2
      = do { Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AnonArgFlag
af1 AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
VisArg) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
             do { (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
arg1 TcSigmaType
arg2; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
mult1 TcSigmaType
mult2 }
           ; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
res1 TcSigmaType
res2 }

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

    go (Delta, Delta)
bvs TcSigmaType
ty1 (AppTy TcSigmaType
t2a TcSigmaType
t2b)
      | Just (TcSigmaType
t1a, TcSigmaType
t1b) <- TcSigmaType -> Maybe (TcSigmaType, TcSigmaType)
tcRepSplitAppTy_maybe TcSigmaType
ty1
      = do { (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
t1a TcSigmaType
t2a; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
t1b TcSigmaType
t2b }

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

    go (Delta, Delta)
_ TcSigmaType
_ TcSigmaType
_ = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


    ----------------
    go_kappa :: (Delta, Delta) -> TcTyVar -> TcSigmaType -> TcM ()
go_kappa (Delta, Delta)
bvs TcTyVar
kappa TcSigmaType
ty2
      = ASSERT2( isMetaTyVar kappa, ppr kappa )
        do { MetaDetails
info <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
kappa
           ; case MetaDetails
info of
               Indirect TcSigmaType
ty1 -> (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
ty1 TcSigmaType
ty2
               MetaDetails
Flexi        -> do { TcSigmaType
ty2 <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
ty2
                                  ; (Delta, Delta) -> TcTyVar -> TcSigmaType -> TcM ()
forall a. (a, Delta) -> TcTyVar -> TcSigmaType -> TcM ()
go_flexi (Delta, Delta)
bvs TcTyVar
kappa TcSigmaType
ty2 } }

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

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

      | Bool
otherwise
      = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()   -- Occurs-check or forall-bound varialbe


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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

It's all grotesquely complicated.
-}

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

tcTagToEnum :: HsExpr GhcRn
            -> HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]
            -> TcRhoType -> ExpRhoType
            -> TcM (HsExpr GhcTc)
-- tagToEnum# :: forall a. Int# -> a
-- See Note [tagToEnum#]   Urgh!
tcTagToEnum :: HsExpr GhcRn
-> HsExpr GhcTc
-> AppCtxt
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcRn
expr HsExpr GhcTc
fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
args TcSigmaType
app_res_ty ExpRhoType
res_ty
  | [HsExprArg 'TcpTc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [HsExprArg 'TcpTc]
val_args
  = SDoc -> TcM (HsExpr GhcTc)
forall a. SDoc -> TcRn a
failWithTc (String -> SDoc
text String
"tagToEnum# must appear applied to one argument")

  | Bool
otherwise
  = do { TcSigmaType
res_ty <- ExpRhoType -> TcM TcSigmaType
readExpType ExpRhoType
res_ty
       ; TcSigmaType
ty'    <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
res_ty

       -- Check that the type is algebraic
       ; case HasCallStack => TcSigmaType -> Maybe (TyCon, ThetaType)
TcSigmaType -> Maybe (TyCon, ThetaType)
tcSplitTyConApp_maybe TcSigmaType
ty' of {
           Maybe (TyCon, ThetaType)
Nothing -> do { SDoc -> TcM ()
addErrTc (TcSigmaType -> SDoc -> SDoc
mk_error TcSigmaType
ty' SDoc
doc1)
                         ; TcM (HsExpr GhcTc)
vanilla_result } ;
           Just (TyCon
tc, ThetaType
tc_args) ->

    do { -- Look through any type family
       ; FamInstEnvs
fam_envs <- TcM FamInstEnvs
tcGetFamInstEnvs
       ; case FamInstEnvs
-> TyCon -> ThetaType -> Maybe (TyCon, ThetaType, TcCoercionN)
tcLookupDataFamInst_maybe FamInstEnvs
fam_envs TyCon
tc ThetaType
tc_args of {
           Maybe (TyCon, ThetaType, TcCoercionN)
Nothing -> do { TcSigmaType -> TyCon -> TcM ()
check_enumeration TcSigmaType
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
         TcSigmaType -> TyCon -> TcM ()
check_enumeration TcSigmaType
ty' TyCon
rep_tc
       ; let rep_ty :: TcSigmaType
rep_ty  = TyCon -> ThetaType -> TcSigmaType
mkTyConApp TyCon
rep_tc ThetaType
rep_args
             fun' :: HsExpr GhcTc
fun'    = HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap (TcSigmaType -> HsWrapper
WpTyApp TcSigmaType
rep_ty) HsExpr GhcTc
fun
             expr' :: HsExpr GhcTc
expr'   = HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps HsExpr GhcTc
fun' AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
val_args
             df_wrap :: HsWrapper
df_wrap = TcCoercionN -> HsWrapper
mkWpCastR (TcCoercionN -> TcCoercionN
mkTcSymCo TcCoercionN
coi)
       ; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap HsWrapper
df_wrap HsExpr GhcTc
expr') }}}}}

  where
    val_args :: [HsExprArg 'TcpTc]
val_args = (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]
args

    vanilla_result :: TcM (HsExpr GhcTc)
vanilla_result
      = do { let expr' :: HsExpr GhcTc
expr' = HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc] -> HsExpr GhcTc
rebuildHsApps HsExpr GhcTc
fun AppCtxt
fun_ctxt [HsExprArg 'TcpTc]
args
           ; HsExpr GhcRn
-> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResultMono HsExpr GhcRn
expr HsExpr GhcTc
expr' TcSigmaType
app_res_ty ExpRhoType
res_ty }

    check_enumeration :: TcSigmaType -> TyCon -> TcM ()
check_enumeration TcSigmaType
ty' TyCon
tc
      | TyCon -> Bool
isEnumerationTyCon TyCon
tc = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Bool
otherwise             = SDoc -> TcM ()
addErrTc (TcSigmaType -> SDoc -> SDoc
mk_error TcSigmaType
ty' SDoc
doc2)

    doc1 :: SDoc
doc1 = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Specify the type by giving a type signature"
                , String -> SDoc
text String
"e.g. (tagToEnum# x) :: Bool" ]
    doc2 :: SDoc
doc2 = String -> SDoc
text String
"Result type must be an enumeration type"

    mk_error :: TcType -> SDoc -> SDoc
    mk_error :: TcSigmaType -> SDoc -> SDoc
mk_error TcSigmaType
ty SDoc
what
      = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Bad call to tagToEnum#"
               SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"at type" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty)
           Int
2 SDoc
what


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

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