-- (c) The University of Glasgow 2006

{-# LANGUAGE CPP, DeriveDataTypeable #-}

module TcEvidence (

  -- HsWrapper
  HsWrapper(..),
  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
  mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
  mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,

  -- Evidence bindings
  TcEvBinds(..), EvBindsVar(..),
  EvBindMap(..), emptyEvBindMap, extendEvBinds,
  lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
  isEmptyEvBindMap,
  EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
  evBindVar, isCoEvBindsVar,

  -- EvTerm (already a CoreExpr)
  EvTerm(..), EvExpr,
  evId, evCoercion, evCast, evDFunApp,  evDataConApp, evSelector,
  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,

  evTermCoercion, evTermCoercion_maybe,
  EvCallStack(..),
  EvTypeable(..),

  -- TcCoercion
  TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
  Role(..), LeftOrRight(..), pickLR,
  mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
  mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
  mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
  mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
  tcDowngradeRole,
  mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflLeftCo, mkTcPhantomCo,
  mkTcCoherenceLeftCo,
  mkTcCoherenceRightCo,
  mkTcKindCo,
  tcCoercionKind, coVarsOfTcCo,
  mkTcCoVarCo,
  isTcReflCo, isTcReflexiveCo,
  tcCoercionRole,
  unwrapIP, wrapIP
  ) where
#include "HsVersions.h"

import GhcPrelude

import Var
import CoAxiom
import Coercion
import PprCore ()   -- Instance OutputableBndr TyVar
import TcType
import Type
import TyCon
import DataCon( DataCon, dataConWrapId )
import Class( Class )
import PrelNames
import DynFlags   ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
import VarEnv
import VarSet
import Name
import Pair

import CoreSyn
import Class ( classSCSelId )
import Id ( isEvVar )
import CoreFVs ( exprSomeFreeVars )

import Util
import Bag
import qualified Data.Data as Data
import Outputable
import SrcLoc
import Data.IORef( IORef )
import UniqSet

{-
Note [TcCoercions]
~~~~~~~~~~~~~~~~~~
| TcCoercions are a hack used by the typechecker. Normally,
Coercions have free variables of type (a ~# b): we call these
CoVars. However, the type checker passes around equality evidence
(boxed up) at type (a ~ b).

An TcCoercion is simply a Coercion whose free variables have may be either
boxed or unboxed. After we are done with typechecking the desugarer finds the
boxed free variables, unboxes them, and creates a resulting real Coercion with
kosher free variables.

-}

type TcCoercion  = Coercion
type TcCoercionN = CoercionN    -- A Nominal          coercion ~N
type TcCoercionR = CoercionR    -- A Representational coercion ~R
type TcCoercionP = CoercionP    -- a phantom coercion

mkTcReflCo             :: Role -> TcType -> TcCoercion
mkTcSymCo              :: TcCoercion -> TcCoercion
mkTcTransCo            :: TcCoercion -> TcCoercion -> TcCoercion
mkTcNomReflCo          :: TcType -> TcCoercionN
mkTcRepReflCo          :: TcType -> TcCoercionR
mkTcTyConAppCo         :: Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcAppCo              :: TcCoercion -> TcCoercionN -> TcCoercion
mkTcFunCo              :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcAxInstCo           :: Role -> CoAxiom br -> BranchIndex
                       -> [TcType] -> [TcCoercion] -> TcCoercion
mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
                       -> [TcCoercion] -> TcCoercionR
mkTcForAllCo           :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
mkTcForAllCos          :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
mkTcNthCo              :: Role -> Int -> TcCoercion -> TcCoercion
mkTcLRCo               :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcSubCo              :: TcCoercionN -> TcCoercionR
maybeTcSubCo           :: EqRel -> TcCoercion -> TcCoercion
tcDowngradeRole        :: Role -> Role -> TcCoercion -> TcCoercion
mkTcAxiomRuleCo        :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
mkTcGReflRightCo       :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcGReflLeftCo        :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcCoherenceLeftCo    :: Role -> TcType -> TcCoercionN
                       -> TcCoercion -> TcCoercion
mkTcCoherenceRightCo   :: Role -> TcType -> TcCoercionN
                       -> TcCoercion -> TcCoercion
mkTcPhantomCo          :: TcCoercionN -> TcType -> TcType -> TcCoercionP
mkTcKindCo             :: TcCoercion -> TcCoercionN
mkTcCoVarCo            :: CoVar -> TcCoercion

tcCoercionKind         :: TcCoercion -> Pair TcType
tcCoercionRole         :: TcCoercion -> Role
coVarsOfTcCo           :: TcCoercion -> TcTyCoVarSet
isTcReflCo             :: TcCoercion -> Bool

-- | This version does a slow check, calculating the related types and seeing
-- if they are equal.
isTcReflexiveCo        :: TcCoercion -> Bool

mkTcReflCo :: Role -> TcType -> TcCoercion
mkTcReflCo             = Role -> TcType -> TcCoercion
mkReflCo
mkTcSymCo :: TcCoercion -> TcCoercion
mkTcSymCo              = TcCoercion -> TcCoercion
mkSymCo
mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo            = TcCoercion -> TcCoercion -> TcCoercion
mkTransCo
mkTcNomReflCo :: TcType -> TcCoercion
mkTcNomReflCo          = TcType -> TcCoercion
mkNomReflCo
mkTcRepReflCo :: TcType -> TcCoercion
mkTcRepReflCo          = TcType -> TcCoercion
mkRepReflCo
mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcTyConAppCo         = HasDebugCallStack => Role -> TyCon -> [TcCoercion] -> TcCoercion
Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTyConAppCo
mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
mkTcAppCo              = TcCoercion -> TcCoercion -> TcCoercion
mkAppCo
mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo              = Role -> TcCoercion -> TcCoercion -> TcCoercion
mkFunCo
mkTcAxInstCo :: Role
-> CoAxiom br
-> BranchIndex
-> [TcType]
-> [TcCoercion]
-> TcCoercion
mkTcAxInstCo           = Role
-> CoAxiom br
-> BranchIndex
-> [TcType]
-> [TcCoercion]
-> TcCoercion
forall (br :: BranchFlag).
Role
-> CoAxiom br
-> BranchIndex
-> [TcType]
-> [TcCoercion]
-> TcCoercion
mkAxInstCo
mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> [TcCoercion] -> TcCoercion
mkTcUnbranchedAxInstCo = Role
-> CoAxiom Unbranched -> [TcType] -> [TcCoercion] -> TcCoercion
mkUnbranchedAxInstCo Role
Representational
mkTcForAllCo :: TyVar -> TcCoercion -> TcCoercion -> TcCoercion
mkTcForAllCo           = TyVar -> TcCoercion -> TcCoercion -> TcCoercion
mkForAllCo
mkTcForAllCos :: [(TyVar, TcCoercion)] -> TcCoercion -> TcCoercion
mkTcForAllCos          = [(TyVar, TcCoercion)] -> TcCoercion -> TcCoercion
mkForAllCos
mkTcNthCo :: Role -> BranchIndex -> TcCoercion -> TcCoercion
mkTcNthCo              = HasDebugCallStack =>
Role -> BranchIndex -> TcCoercion -> TcCoercion
Role -> BranchIndex -> TcCoercion -> TcCoercion
mkNthCo
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcLRCo               = LeftOrRight -> TcCoercion -> TcCoercion
mkLRCo
mkTcSubCo :: TcCoercion -> TcCoercion
mkTcSubCo              = TcCoercion -> TcCoercion
mkSubCo
maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
maybeTcSubCo           = EqRel -> TcCoercion -> TcCoercion
maybeSubCo
tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
tcDowngradeRole        = Role -> Role -> TcCoercion -> TcCoercion
downgradeRole
mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercion
mkTcAxiomRuleCo        = CoAxiomRule -> [TcCoercion] -> TcCoercion
mkAxiomRuleCo
mkTcGReflRightCo :: Role -> TcType -> TcCoercion -> TcCoercion
mkTcGReflRightCo       = Role -> TcType -> TcCoercion -> TcCoercion
mkGReflRightCo
mkTcGReflLeftCo :: Role -> TcType -> TcCoercion -> TcCoercion
mkTcGReflLeftCo        = Role -> TcType -> TcCoercion -> TcCoercion
mkGReflLeftCo
mkTcCoherenceLeftCo :: Role -> TcType -> TcCoercion -> TcCoercion -> TcCoercion
mkTcCoherenceLeftCo    = Role -> TcType -> TcCoercion -> TcCoercion -> TcCoercion
mkCoherenceLeftCo
mkTcCoherenceRightCo :: Role -> TcType -> TcCoercion -> TcCoercion -> TcCoercion
mkTcCoherenceRightCo   = Role -> TcType -> TcCoercion -> TcCoercion -> TcCoercion
mkCoherenceRightCo
mkTcPhantomCo :: TcCoercion -> TcType -> TcType -> TcCoercion
mkTcPhantomCo          = TcCoercion -> TcType -> TcType -> TcCoercion
mkPhantomCo
mkTcKindCo :: TcCoercion -> TcCoercion
mkTcKindCo             = TcCoercion -> TcCoercion
mkKindCo
mkTcCoVarCo :: TyVar -> TcCoercion
mkTcCoVarCo            = TyVar -> TcCoercion
mkCoVarCo

tcCoercionKind :: TcCoercion -> Pair TcType
tcCoercionKind         = TcCoercion -> Pair TcType
coercionKind
tcCoercionRole :: TcCoercion -> Role
tcCoercionRole         = TcCoercion -> Role
coercionRole
coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet
coVarsOfTcCo           = TcCoercion -> TcTyCoVarSet
coVarsOfCo
isTcReflCo :: TcCoercion -> Bool
isTcReflCo             = TcCoercion -> Bool
isReflCo
isTcReflexiveCo :: TcCoercion -> Bool
isTcReflexiveCo        = TcCoercion -> Bool
isReflexiveCo

{-
%************************************************************************
%*                                                                      *
                  HsWrapper
*                                                                      *
************************************************************************
-}

data HsWrapper
  = WpHole                      -- The identity coercion

  | WpCompose HsWrapper HsWrapper
       -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
       --
       -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
       -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)

  | WpFun HsWrapper HsWrapper TcType SDoc
       -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ]
       -- So note that if  wrap1 :: exp_arg <= act_arg
       --                  wrap2 :: act_res <= exp_res
       --           then   WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
       -- This isn't the same as for mkFunCo, but it has to be this way
       -- because we can't use 'sym' to flip around these HsWrappers
       -- The TcType is the "from" type of the first wrapper
       -- The SDoc explains the circumstances under which we have created this
       -- WpFun, in case we run afoul of levity polymorphism restrictions in
       -- the desugarer. See Note [Levity polymorphism checking] in DsMonad

  | WpCast TcCoercionR        -- A cast:  [] `cast` co
                              -- Guaranteed not the identity coercion
                              -- At role Representational

        -- Evidence abstraction and application
        -- (both dictionaries and coercions)
  | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
  | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
        -- Kind and Type abstraction and application
  | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
  | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)


  | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
                                -- so that the identity coercion is always exactly WpHole

-- Cannot derive Data instance because SDoc is not Data (it stores a function).
-- So we do it manually:
instance Data.Data HsWrapper where
  gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsWrapper -> c HsWrapper
gfoldl _ z :: forall g. g -> c g
z WpHole             = HsWrapper -> c HsWrapper
forall g. g -> c g
z HsWrapper
WpHole
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpCompose a1 :: HsWrapper
a1 a2 :: HsWrapper
a2)  = (HsWrapper -> HsWrapper -> HsWrapper)
-> c (HsWrapper -> HsWrapper -> HsWrapper)
forall g. g -> c g
z HsWrapper -> HsWrapper -> HsWrapper
WpCompose c (HsWrapper -> HsWrapper -> HsWrapper)
-> HsWrapper -> c (HsWrapper -> HsWrapper)
forall d b. Data d => c (d -> b) -> d -> c b
`k` HsWrapper
a1 c (HsWrapper -> HsWrapper) -> HsWrapper -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` HsWrapper
a2
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpFun a1 :: HsWrapper
a1 a2 :: HsWrapper
a2 a3 :: TcType
a3 _) = (HsWrapper -> HsWrapper -> TcType -> HsWrapper)
-> c (HsWrapper -> HsWrapper -> TcType -> HsWrapper)
forall g. g -> c g
z HsWrapper -> HsWrapper -> TcType -> HsWrapper
wpFunEmpty c (HsWrapper -> HsWrapper -> TcType -> HsWrapper)
-> HsWrapper -> c (HsWrapper -> TcType -> HsWrapper)
forall d b. Data d => c (d -> b) -> d -> c b
`k` HsWrapper
a1 c (HsWrapper -> TcType -> HsWrapper)
-> HsWrapper -> c (TcType -> HsWrapper)
forall d b. Data d => c (d -> b) -> d -> c b
`k` HsWrapper
a2 c (TcType -> HsWrapper) -> TcType -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` TcType
a3
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpCast a1 :: TcCoercion
a1)        = (TcCoercion -> HsWrapper) -> c (TcCoercion -> HsWrapper)
forall g. g -> c g
z TcCoercion -> HsWrapper
WpCast c (TcCoercion -> HsWrapper) -> TcCoercion -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` TcCoercion
a1
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpEvLam a1 :: TyVar
a1)       = (TyVar -> HsWrapper) -> c (TyVar -> HsWrapper)
forall g. g -> c g
z TyVar -> HsWrapper
WpEvLam c (TyVar -> HsWrapper) -> TyVar -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` TyVar
a1
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpEvApp a1 :: EvTerm
a1)       = (EvTerm -> HsWrapper) -> c (EvTerm -> HsWrapper)
forall g. g -> c g
z EvTerm -> HsWrapper
WpEvApp c (EvTerm -> HsWrapper) -> EvTerm -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` EvTerm
a1
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpTyLam a1 :: TyVar
a1)       = (TyVar -> HsWrapper) -> c (TyVar -> HsWrapper)
forall g. g -> c g
z TyVar -> HsWrapper
WpTyLam c (TyVar -> HsWrapper) -> TyVar -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` TyVar
a1
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpTyApp a1 :: TcType
a1)       = (TcType -> HsWrapper) -> c (TcType -> HsWrapper)
forall g. g -> c g
z TcType -> HsWrapper
WpTyApp c (TcType -> HsWrapper) -> TcType -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` TcType
a1
  gfoldl k :: forall d b. Data d => c (d -> b) -> d -> c b
k z :: forall g. g -> c g
z (WpLet a1 :: TcEvBinds
a1)         = (TcEvBinds -> HsWrapper) -> c (TcEvBinds -> HsWrapper)
forall g. g -> c g
z TcEvBinds -> HsWrapper
WpLet c (TcEvBinds -> HsWrapper) -> TcEvBinds -> c HsWrapper
forall d b. Data d => c (d -> b) -> d -> c b
`k` TcEvBinds
a1

  gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsWrapper
gunfold k :: forall b r. Data b => c (b -> r) -> c r
k z :: forall r. r -> c r
z c :: Constr
c = case Constr -> BranchIndex
Data.constrIndex Constr
c of
                    1 -> HsWrapper -> c HsWrapper
forall r. r -> c r
z HsWrapper
WpHole
                    2 -> c (HsWrapper -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k (c (HsWrapper -> HsWrapper -> HsWrapper)
-> c (HsWrapper -> HsWrapper)
forall b r. Data b => c (b -> r) -> c r
k ((HsWrapper -> HsWrapper -> HsWrapper)
-> c (HsWrapper -> HsWrapper -> HsWrapper)
forall r. r -> c r
z HsWrapper -> HsWrapper -> HsWrapper
WpCompose))
                    3 -> c (TcType -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k (c (HsWrapper -> TcType -> HsWrapper) -> c (TcType -> HsWrapper)
forall b r. Data b => c (b -> r) -> c r
k (c (HsWrapper -> HsWrapper -> TcType -> HsWrapper)
-> c (HsWrapper -> TcType -> HsWrapper)
forall b r. Data b => c (b -> r) -> c r
k ((HsWrapper -> HsWrapper -> TcType -> HsWrapper)
-> c (HsWrapper -> HsWrapper -> TcType -> HsWrapper)
forall r. r -> c r
z HsWrapper -> HsWrapper -> TcType -> HsWrapper
wpFunEmpty)))
                    4 -> c (TcCoercion -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k ((TcCoercion -> HsWrapper) -> c (TcCoercion -> HsWrapper)
forall r. r -> c r
z TcCoercion -> HsWrapper
WpCast)
                    5 -> c (TyVar -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k ((TyVar -> HsWrapper) -> c (TyVar -> HsWrapper)
forall r. r -> c r
z TyVar -> HsWrapper
WpEvLam)
                    6 -> c (EvTerm -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k ((EvTerm -> HsWrapper) -> c (EvTerm -> HsWrapper)
forall r. r -> c r
z EvTerm -> HsWrapper
WpEvApp)
                    7 -> c (TyVar -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k ((TyVar -> HsWrapper) -> c (TyVar -> HsWrapper)
forall r. r -> c r
z TyVar -> HsWrapper
WpTyLam)
                    8 -> c (TcType -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k ((TcType -> HsWrapper) -> c (TcType -> HsWrapper)
forall r. r -> c r
z TcType -> HsWrapper
WpTyApp)
                    _ -> c (TcEvBinds -> HsWrapper) -> c HsWrapper
forall b r. Data b => c (b -> r) -> c r
k ((TcEvBinds -> HsWrapper) -> c (TcEvBinds -> HsWrapper)
forall r. r -> c r
z TcEvBinds -> HsWrapper
WpLet)

  toConstr :: HsWrapper -> Constr
toConstr WpHole          = Constr
wpHole_constr
  toConstr (WpCompose _ _) = Constr
wpCompose_constr
  toConstr (WpFun _ _ _ _) = Constr
wpFun_constr
  toConstr (WpCast _)      = Constr
wpCast_constr
  toConstr (WpEvLam _)     = Constr
wpEvLam_constr
  toConstr (WpEvApp _)     = Constr
wpEvApp_constr
  toConstr (WpTyLam _)     = Constr
wpTyLam_constr
  toConstr (WpTyApp _)     = Constr
wpTyApp_constr
  toConstr (WpLet _)       = Constr
wpLet_constr

  dataTypeOf :: HsWrapper -> DataType
dataTypeOf _ = DataType
hsWrapper_dataType

hsWrapper_dataType :: Data.DataType
hsWrapper_dataType :: DataType
hsWrapper_dataType
  = String -> [Constr] -> DataType
Data.mkDataType "HsWrapper"
      [ Constr
wpHole_constr, Constr
wpCompose_constr, Constr
wpFun_constr, Constr
wpCast_constr
      , Constr
wpEvLam_constr, Constr
wpEvApp_constr, Constr
wpTyLam_constr, Constr
wpTyApp_constr
      , Constr
wpLet_constr]

wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr,
  wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr :: Data.Constr
wpHole_constr :: Constr
wpHole_constr    = String -> Constr
mkHsWrapperConstr "WpHole"
wpCompose_constr :: Constr
wpCompose_constr = String -> Constr
mkHsWrapperConstr "WpCompose"
wpFun_constr :: Constr
wpFun_constr     = String -> Constr
mkHsWrapperConstr "WpFun"
wpCast_constr :: Constr
wpCast_constr    = String -> Constr
mkHsWrapperConstr "WpCast"
wpEvLam_constr :: Constr
wpEvLam_constr   = String -> Constr
mkHsWrapperConstr "WpEvLam"
wpEvApp_constr :: Constr
wpEvApp_constr   = String -> Constr
mkHsWrapperConstr "WpEvApp"
wpTyLam_constr :: Constr
wpTyLam_constr   = String -> Constr
mkHsWrapperConstr "WpTyLam"
wpTyApp_constr :: Constr
wpTyApp_constr   = String -> Constr
mkHsWrapperConstr "WpTyApp"
wpLet_constr :: Constr
wpLet_constr     = String -> Constr
mkHsWrapperConstr "WpLet"

mkHsWrapperConstr :: String -> Data.Constr
mkHsWrapperConstr :: String -> Constr
mkHsWrapperConstr name :: String
name = DataType -> String -> [String] -> Fixity -> Constr
Data.mkConstr DataType
hsWrapper_dataType String
name [] Fixity
Data.Prefix

wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper
wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper
wpFunEmpty c1 :: HsWrapper
c1 c2 :: HsWrapper
c2 t1 :: TcType
t1 = HsWrapper -> HsWrapper -> TcType -> SDoc -> HsWrapper
WpFun HsWrapper
c1 HsWrapper
c2 TcType
t1 SDoc
empty

(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> :: HsWrapper -> HsWrapper -> HsWrapper
<.> c :: HsWrapper
c = HsWrapper
c
c :: HsWrapper
c <.> WpHole = HsWrapper
c
c1 :: HsWrapper
c1 <.> c2 :: HsWrapper
c2    = HsWrapper
c1 HsWrapper -> HsWrapper -> HsWrapper
`WpCompose` HsWrapper
c2

mkWpFun :: HsWrapper -> HsWrapper
        -> TcType    -- the "from" type of the first wrapper
        -> TcType    -- either type of the second wrapper (used only when the
                     -- second wrapper is the identity)
        -> SDoc      -- what caused you to want a WpFun? Something like "When converting ..."
        -> HsWrapper
mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> SDoc -> HsWrapper
mkWpFun WpHole       WpHole       _  _  _ = HsWrapper
WpHole
mkWpFun WpHole       (WpCast co2 :: TcCoercion
co2) t1 :: TcType
t1 _  _ = TcCoercion -> HsWrapper
WpCast (Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo Role
Representational (TcType -> TcCoercion
mkTcRepReflCo TcType
t1) TcCoercion
co2)
mkWpFun (WpCast co1 :: TcCoercion
co1) WpHole       _  t2 :: TcType
t2 _ = TcCoercion -> HsWrapper
WpCast (Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo Role
Representational (TcCoercion -> TcCoercion
mkTcSymCo TcCoercion
co1) (TcType -> TcCoercion
mkTcRepReflCo TcType
t2))
mkWpFun (WpCast co1 :: TcCoercion
co1) (WpCast co2 :: TcCoercion
co2) _  _  _ = TcCoercion -> HsWrapper
WpCast (Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo Role
Representational (TcCoercion -> TcCoercion
mkTcSymCo TcCoercion
co1) TcCoercion
co2)
mkWpFun co1 :: HsWrapper
co1          co2 :: HsWrapper
co2          t1 :: TcType
t1 _  d :: SDoc
d = HsWrapper -> HsWrapper -> TcType -> SDoc -> HsWrapper
WpFun HsWrapper
co1 HsWrapper
co2 TcType
t1 SDoc
d

-- | @mkWpFuns [(ty1, wrap1), (ty2, wrap2)] ty_res wrap_res@,
-- where @wrap1 :: ty1 "->" ty1'@ and @wrap2 :: ty2 "->" ty2'@,
-- @wrap3 :: ty3 "->" ty3'@ and @ty_res@ is /either/ @ty3@ or @ty3'@,
-- gives a wrapper @(ty1' -> ty2' -> ty3) "->" (ty1 -> ty2 -> ty3')@.
-- Notice that the result wrapper goes the other way round to all
-- the others. This is a result of sub-typing contravariance.
-- The SDoc is a description of what you were doing when you called mkWpFuns.
mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper
mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper
mkWpFuns args :: [(TcType, HsWrapper)]
args res_ty :: TcType
res_ty res_wrap :: HsWrapper
res_wrap doc :: SDoc
doc = (TcType, HsWrapper) -> HsWrapper
forall a b. (a, b) -> b
snd ((TcType, HsWrapper) -> HsWrapper)
-> (TcType, HsWrapper) -> HsWrapper
forall a b. (a -> b) -> a -> b
$ [(TcType, HsWrapper)] -> TcType -> HsWrapper -> (TcType, HsWrapper)
go [(TcType, HsWrapper)]
args TcType
res_ty HsWrapper
res_wrap
  where
    go :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> (TcType, HsWrapper)
go [] res_ty :: TcType
res_ty res_wrap :: HsWrapper
res_wrap = (TcType
res_ty, HsWrapper
res_wrap)
    go ((arg_ty :: TcType
arg_ty, arg_wrap :: HsWrapper
arg_wrap) : args :: [(TcType, HsWrapper)]
args) res_ty :: TcType
res_ty res_wrap :: HsWrapper
res_wrap
      = let (tail_ty :: TcType
tail_ty, tail_wrap :: HsWrapper
tail_wrap) = [(TcType, HsWrapper)] -> TcType -> HsWrapper -> (TcType, HsWrapper)
go [(TcType, HsWrapper)]
args TcType
res_ty HsWrapper
res_wrap in
        (TcType
arg_ty TcType -> TcType -> TcType
`mkFunTy` TcType
tail_ty, HsWrapper -> HsWrapper -> TcType -> TcType -> SDoc -> HsWrapper
mkWpFun HsWrapper
arg_wrap HsWrapper
tail_wrap TcType
arg_ty TcType
tail_ty SDoc
doc)

mkWpCastR :: TcCoercionR -> HsWrapper
mkWpCastR :: TcCoercion -> HsWrapper
mkWpCastR co :: TcCoercion
co
  | TcCoercion -> Bool
isTcReflCo TcCoercion
co = HsWrapper
WpHole
  | Bool
otherwise     = ASSERT2(tcCoercionRole co == Representational, ppr co)
                    TcCoercion -> HsWrapper
WpCast TcCoercion
co

mkWpCastN :: TcCoercionN -> HsWrapper
mkWpCastN :: TcCoercion -> HsWrapper
mkWpCastN co :: TcCoercion
co
  | TcCoercion -> Bool
isTcReflCo TcCoercion
co = HsWrapper
WpHole
  | Bool
otherwise     = ASSERT2(tcCoercionRole co == Nominal, ppr co)
                    TcCoercion -> HsWrapper
WpCast (TcCoercion -> TcCoercion
mkTcSubCo TcCoercion
co)
    -- The mkTcSubCo converts Nominal to Representational

mkWpTyApps :: [Type] -> HsWrapper
mkWpTyApps :: [TcType] -> HsWrapper
mkWpTyApps tys :: [TcType]
tys = (TcType -> HsWrapper) -> [TcType] -> HsWrapper
forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn TcType -> HsWrapper
WpTyApp [TcType]
tys

mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvApps args :: [EvTerm]
args = (EvTerm -> HsWrapper) -> [EvTerm] -> HsWrapper
forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn EvTerm -> HsWrapper
WpEvApp [EvTerm]
args

mkWpEvVarApps :: [EvVar] -> HsWrapper
mkWpEvVarApps :: [TyVar] -> HsWrapper
mkWpEvVarApps vs :: [TyVar]
vs = (EvTerm -> HsWrapper) -> [EvTerm] -> HsWrapper
forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn EvTerm -> HsWrapper
WpEvApp ((TyVar -> EvTerm) -> [TyVar] -> [EvTerm]
forall a b. (a -> b) -> [a] -> [b]
map (EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> (TyVar -> EvExpr) -> TyVar -> EvTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> EvExpr
evId) [TyVar]
vs)

mkWpTyLams :: [TyVar] -> HsWrapper
mkWpTyLams :: [TyVar] -> HsWrapper
mkWpTyLams ids :: [TyVar]
ids = (TyVar -> HsWrapper) -> [TyVar] -> HsWrapper
forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn TyVar -> HsWrapper
WpTyLam [TyVar]
ids

mkWpLams :: [Var] -> HsWrapper
mkWpLams :: [TyVar] -> HsWrapper
mkWpLams ids :: [TyVar]
ids = (TyVar -> HsWrapper) -> [TyVar] -> HsWrapper
forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn TyVar -> HsWrapper
WpEvLam [TyVar]
ids

mkWpLet :: TcEvBinds -> HsWrapper
-- This no-op is a quite a common case
mkWpLet :: TcEvBinds -> HsWrapper
mkWpLet (EvBinds b :: Bag EvBind
b) | Bag EvBind -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag EvBind
b = HsWrapper
WpHole
mkWpLet ev_binds :: TcEvBinds
ev_binds                   = TcEvBinds -> HsWrapper
WpLet TcEvBinds
ev_binds

mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn f :: a -> HsWrapper
f as :: [a]
as = (a -> HsWrapper -> HsWrapper) -> HsWrapper -> [a] -> HsWrapper
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\x :: a
x wrap :: HsWrapper
wrap -> a -> HsWrapper
f a
x HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap) HsWrapper
WpHole [a]
as

mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
-- For applications, the *first* argument must
-- come *last* in the composition sequence
mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn f :: a -> HsWrapper
f as :: [a]
as = (a -> HsWrapper -> HsWrapper) -> HsWrapper -> [a] -> HsWrapper
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\x :: a
x wrap :: HsWrapper
wrap -> HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> a -> HsWrapper
f a
x) HsWrapper
WpHole [a]
as

idHsWrapper :: HsWrapper
idHsWrapper :: HsWrapper
idHsWrapper = HsWrapper
WpHole

isIdHsWrapper :: HsWrapper -> Bool
isIdHsWrapper :: HsWrapper -> Bool
isIdHsWrapper WpHole = Bool
True
isIdHsWrapper _      = Bool
False

collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
-- Collect the outer lambda binders of a HsWrapper,
-- stopping as soon as you get to a non-lambda binder
collectHsWrapBinders :: HsWrapper -> ([TyVar], HsWrapper)
collectHsWrapBinders wrap :: HsWrapper
wrap = HsWrapper -> [HsWrapper] -> ([TyVar], HsWrapper)
go HsWrapper
wrap []
  where
    -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn)
    go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
    go :: HsWrapper -> [HsWrapper] -> ([TyVar], HsWrapper)
go (WpEvLam v :: TyVar
v)       wraps :: [HsWrapper]
wraps = TyVar -> ([TyVar], HsWrapper) -> ([TyVar], HsWrapper)
forall a b. a -> ([a], b) -> ([a], b)
add_lam TyVar
v ([HsWrapper] -> ([TyVar], HsWrapper)
gos [HsWrapper]
wraps)
    go (WpTyLam v :: TyVar
v)       wraps :: [HsWrapper]
wraps = TyVar -> ([TyVar], HsWrapper) -> ([TyVar], HsWrapper)
forall a b. a -> ([a], b) -> ([a], b)
add_lam TyVar
v ([HsWrapper] -> ([TyVar], HsWrapper)
gos [HsWrapper]
wraps)
    go (WpCompose w1 :: HsWrapper
w1 w2 :: HsWrapper
w2) wraps :: [HsWrapper]
wraps = HsWrapper -> [HsWrapper] -> ([TyVar], HsWrapper)
go HsWrapper
w1 (HsWrapper
w2HsWrapper -> [HsWrapper] -> [HsWrapper]
forall a. a -> [a] -> [a]
:[HsWrapper]
wraps)
    go wrap :: HsWrapper
wrap              wraps :: [HsWrapper]
wraps = ([], (HsWrapper -> HsWrapper -> HsWrapper)
-> HsWrapper -> [HsWrapper] -> HsWrapper
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HsWrapper -> HsWrapper -> HsWrapper
(<.>) HsWrapper
wrap [HsWrapper]
wraps)

    gos :: [HsWrapper] -> ([TyVar], HsWrapper)
gos []     = ([], HsWrapper
WpHole)
    gos (w :: HsWrapper
w:ws :: [HsWrapper]
ws) = HsWrapper -> [HsWrapper] -> ([TyVar], HsWrapper)
go HsWrapper
w [HsWrapper]
ws

    add_lam :: a -> ([a], b) -> ([a], b)
add_lam v :: a
v (vs :: [a]
vs,w :: b
w) = (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
vs, b
w)

{-
************************************************************************
*                                                                      *
                  Evidence bindings
*                                                                      *
************************************************************************
-}

data TcEvBinds
  = TcEvBinds           -- Mutable evidence bindings
       EvBindsVar       -- Mutable because they are updated "later"
                        --    when an implication constraint is solved

  | EvBinds             -- Immutable after zonking
       (Bag EvBind)

data EvBindsVar
  = EvBindsVar {
      EvBindsVar -> Unique
ebv_uniq :: Unique,
         -- The Unique is for debug printing only

      EvBindsVar -> IORef EvBindMap
ebv_binds :: IORef EvBindMap,
      -- The main payload: the value-level evidence bindings
      --     (dictionaries etc)
      -- Some Given, some Wanted

      EvBindsVar -> IORef TcTyCoVarSet
ebv_tcvs :: IORef CoVarSet
      -- The free Given coercion vars needed by Wanted coercions that
      -- are solved by filling in their HoleDest in-place. Since they
      -- don't appear in ebv_binds, we keep track of their free
      -- variables so that we can report unused given constraints
      -- See Note [Tracking redundant constraints] in TcSimplify
    }

  | CoEvBindsVar {  -- See Note [Coercion evidence only]

      -- See above for comments on ebv_uniq, ebv_tcvs
      ebv_uniq :: Unique,
      ebv_tcvs :: IORef CoVarSet
    }

instance Data.Data TcEvBinds where
  -- Placeholder; we can't travers into TcEvBinds
  toConstr :: TcEvBinds -> Constr
toConstr _   = String -> Constr
abstractConstr "TcEvBinds"
  gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TcEvBinds
gunfold _ _  = String -> Constr -> c TcEvBinds
forall a. HasCallStack => String -> a
error "gunfold"
  dataTypeOf :: TcEvBinds -> DataType
dataTypeOf _ = String -> DataType
Data.mkNoRepType "TcEvBinds"

{- Note [Coercion evidence only]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Class constraints etc give rise to /term/ bindings for evidence, and
we have nowhere to put term bindings in /types/.  So in some places we
use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
evidence bindings are allowed.  Notebly ():

  - Places in types where we are solving kind constraints (all of which
    are equalities); see solveEqualities, solveLocalEqualities,
    checkTvConstraints

  - When unifying forall-types
-}

isCoEvBindsVar :: EvBindsVar -> Bool
isCoEvBindsVar :: EvBindsVar -> Bool
isCoEvBindsVar (CoEvBindsVar {}) = Bool
True
isCoEvBindsVar (EvBindsVar {})   = Bool
False

-----------------
newtype EvBindMap
  = EvBindMap {
       EvBindMap -> DVarEnv EvBind
ev_bind_varenv :: DVarEnv EvBind
    }       -- Map from evidence variables to evidence terms
            -- We use @DVarEnv@ here to get deterministic ordering when we
            -- turn it into a Bag.
            -- If we don't do that, when we generate let bindings for
            -- dictionaries in dsTcEvBinds they will be generated in random
            -- order.
            --
            -- For example:
            --
            -- let $dEq = GHC.Classes.$fEqInt in
            -- let $$dNum = GHC.Num.$fNumInt in ...
            --
            -- vs
            --
            -- let $dNum = GHC.Num.$fNumInt in
            -- let $dEq = GHC.Classes.$fEqInt in ...
            --
            -- See Note [Deterministic UniqFM] in UniqDFM for explanation why
            -- @UniqFM@ can lead to nondeterministic order.

emptyEvBindMap :: EvBindMap
emptyEvBindMap :: EvBindMap
emptyEvBindMap = EvBindMap :: DVarEnv EvBind -> EvBindMap
EvBindMap { ev_bind_varenv :: DVarEnv EvBind
ev_bind_varenv = DVarEnv EvBind
forall a. DVarEnv a
emptyDVarEnv }

extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
extendEvBinds bs :: EvBindMap
bs ev_bind :: EvBind
ev_bind
  = EvBindMap :: DVarEnv EvBind -> EvBindMap
EvBindMap { ev_bind_varenv :: DVarEnv EvBind
ev_bind_varenv = DVarEnv EvBind -> TyVar -> EvBind -> DVarEnv EvBind
forall a. DVarEnv a -> TyVar -> a -> DVarEnv a
extendDVarEnv (EvBindMap -> DVarEnv EvBind
ev_bind_varenv EvBindMap
bs)
                                               (EvBind -> TyVar
eb_lhs EvBind
ev_bind)
                                               EvBind
ev_bind }

isEmptyEvBindMap :: EvBindMap -> Bool
isEmptyEvBindMap :: EvBindMap -> Bool
isEmptyEvBindMap (EvBindMap m :: DVarEnv EvBind
m) = DVarEnv EvBind -> Bool
forall a. DVarEnv a -> Bool
isEmptyDVarEnv DVarEnv EvBind
m

lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
lookupEvBind :: EvBindMap -> TyVar -> Maybe EvBind
lookupEvBind bs :: EvBindMap
bs = DVarEnv EvBind -> TyVar -> Maybe EvBind
forall a. DVarEnv a -> TyVar -> Maybe a
lookupDVarEnv (EvBindMap -> DVarEnv EvBind
ev_bind_varenv EvBindMap
bs)

evBindMapBinds :: EvBindMap -> Bag EvBind
evBindMapBinds :: EvBindMap -> Bag EvBind
evBindMapBinds = (EvBind -> Bag EvBind -> Bag EvBind)
-> Bag EvBind -> EvBindMap -> Bag EvBind
forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
foldEvBindMap EvBind -> Bag EvBind -> Bag EvBind
forall a. a -> Bag a -> Bag a
consBag Bag EvBind
forall a. Bag a
emptyBag

foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
foldEvBindMap k :: EvBind -> a -> a
k z :: a
z bs :: EvBindMap
bs = (EvBind -> a -> a) -> a -> DVarEnv EvBind -> a
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv EvBind -> a -> a
k a
z (EvBindMap -> DVarEnv EvBind
ev_bind_varenv EvBindMap
bs)

filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
filterEvBindMap k :: EvBind -> Bool
k (EvBindMap { ev_bind_varenv :: EvBindMap -> DVarEnv EvBind
ev_bind_varenv = DVarEnv EvBind
env })
  = EvBindMap :: DVarEnv EvBind -> EvBindMap
EvBindMap { ev_bind_varenv :: DVarEnv EvBind
ev_bind_varenv = (EvBind -> Bool) -> DVarEnv EvBind -> DVarEnv EvBind
forall a. (a -> Bool) -> DVarEnv a -> DVarEnv a
filterDVarEnv EvBind -> Bool
k DVarEnv EvBind
env }

instance Outputable EvBindMap where
  ppr :: EvBindMap -> SDoc
ppr (EvBindMap m :: DVarEnv EvBind
m) = DVarEnv EvBind -> SDoc
forall a. Outputable a => a -> SDoc
ppr DVarEnv EvBind
m

-----------------
-- All evidence is bound by EvBinds; no side effects
data EvBind
  = EvBind { EvBind -> TyVar
eb_lhs      :: EvVar
           , EvBind -> EvTerm
eb_rhs      :: EvTerm
           , EvBind -> Bool
eb_is_given :: Bool  -- True <=> given
                 -- See Note [Tracking redundant constraints] in TcSimplify
    }

evBindVar :: EvBind -> EvVar
evBindVar :: EvBind -> TyVar
evBindVar = EvBind -> TyVar
eb_lhs

mkWantedEvBind :: EvVar -> EvTerm -> EvBind
mkWantedEvBind :: TyVar -> EvTerm -> EvBind
mkWantedEvBind ev :: TyVar
ev tm :: EvTerm
tm = EvBind :: TyVar -> EvTerm -> Bool -> EvBind
EvBind { eb_is_given :: Bool
eb_is_given = Bool
False, eb_lhs :: TyVar
eb_lhs = TyVar
ev, eb_rhs :: EvTerm
eb_rhs = EvTerm
tm }

-- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
mkGivenEvBind :: EvVar -> EvTerm -> EvBind
mkGivenEvBind :: TyVar -> EvTerm -> EvBind
mkGivenEvBind ev :: TyVar
ev tm :: EvTerm
tm = EvBind :: TyVar -> EvTerm -> Bool -> EvBind
EvBind { eb_is_given :: Bool
eb_is_given = Bool
True, eb_lhs :: TyVar
eb_lhs = TyVar
ev, eb_rhs :: EvTerm
eb_rhs = EvTerm
tm }


-- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
-- Unfortunately, we cannot just do
--   type EvTerm  = CoreExpr
-- Because of staging problems issues around EvTypeable
data EvTerm
  = EvExpr EvExpr

  | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)

  | EvFun     -- /\as \ds. let binds in v
      { EvTerm -> [TyVar]
et_tvs   :: [TyVar]
      , EvTerm -> [TyVar]
et_given :: [EvVar]
      , EvTerm -> TcEvBinds
et_binds :: TcEvBinds -- This field is why we need an EvFun
                              -- constructor, and can't just use EvExpr
      , EvTerm -> TyVar
et_body  :: EvVar }

  deriving Typeable EvTerm
DataType
Constr
Typeable EvTerm =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EvTerm -> c EvTerm)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTerm)
-> (EvTerm -> Constr)
-> (EvTerm -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTerm))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm))
-> ((forall b. Data b => b -> b) -> EvTerm -> EvTerm)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTerm -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTerm -> r)
-> (forall u. (forall d. Data d => d -> u) -> EvTerm -> [u])
-> (forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> EvTerm -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm)
-> Data EvTerm
EvTerm -> DataType
EvTerm -> Constr
(forall b. Data b => b -> b) -> EvTerm -> EvTerm
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTerm -> c EvTerm
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTerm
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
BranchIndex -> (forall d. Data d => d -> u) -> EvTerm -> u
forall u. (forall d. Data d => d -> u) -> EvTerm -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTerm -> c EvTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
$cEvFun :: Constr
$cEvTypeable :: Constr
$cEvExpr :: Constr
$tEvTerm :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
gmapMp :: (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
gmapM :: (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
gmapQi :: BranchIndex -> (forall d. Data d => d -> u) -> EvTerm -> u
$cgmapQi :: forall u.
BranchIndex -> (forall d. Data d => d -> u) -> EvTerm -> u
gmapQ :: (forall d. Data d => d -> u) -> EvTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvTerm -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
gmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm
$cgmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EvTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTerm)
dataTypeOf :: EvTerm -> DataType
$cdataTypeOf :: EvTerm -> DataType
toConstr :: EvTerm -> Constr
$ctoConstr :: EvTerm -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTerm
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTerm -> c EvTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTerm -> c EvTerm
$cp1Data :: Typeable EvTerm
Data.Data

type EvExpr = CoreExpr

-- An EvTerm is (usually) constructed by any of the constructors here
-- and those more complicates ones who were moved to module TcEvTerm

-- | Any sort of evidence Id, including coercions
evId ::  EvId -> EvExpr
evId :: TyVar -> EvExpr
evId = TyVar -> EvExpr
forall b. TyVar -> Expr b
Var

-- coercion bindings
-- See Note [Coercion evidence terms]
evCoercion :: TcCoercion -> EvTerm
evCoercion :: TcCoercion -> EvTerm
evCoercion co :: TcCoercion
co = EvExpr -> EvTerm
EvExpr (TcCoercion -> EvExpr
forall b. TcCoercion -> Expr b
Coercion TcCoercion
co)

-- | d |> co
evCast :: EvExpr -> TcCoercion -> EvTerm
evCast :: EvExpr -> TcCoercion -> EvTerm
evCast et :: EvExpr
et tc :: TcCoercion
tc | TcCoercion -> Bool
isReflCo TcCoercion
tc = EvExpr -> EvTerm
EvExpr EvExpr
et
             | Bool
otherwise   = EvExpr -> EvTerm
EvExpr (EvExpr -> TcCoercion -> EvExpr
forall b. Expr b -> TcCoercion -> Expr b
Cast EvExpr
et TcCoercion
tc)

-- Dictionary instance application
evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp :: TyVar -> [TcType] -> [EvExpr] -> EvTerm
evDFunApp df :: TyVar
df tys :: [TcType]
tys ets :: [EvExpr]
ets = EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ TyVar -> EvExpr
forall b. TyVar -> Expr b
Var TyVar
df EvExpr -> [TcType] -> EvExpr
forall b. Expr b -> [TcType] -> Expr b
`mkTyApps` [TcType]
tys EvExpr -> [EvExpr] -> EvExpr
forall b. Expr b -> [Expr b] -> Expr b
`mkApps` [EvExpr]
ets

evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp :: DataCon -> [TcType] -> [EvExpr] -> EvTerm
evDataConApp dc :: DataCon
dc tys :: [TcType]
tys ets :: [EvExpr]
ets = TyVar -> [TcType] -> [EvExpr] -> EvTerm
evDFunApp (DataCon -> TyVar
dataConWrapId DataCon
dc) [TcType]
tys [EvExpr]
ets

-- Selector id plus the types at which it
-- should be instantiated, used for HasField
-- dictionaries; see Note [HasField instances]
-- in TcInterface
evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
evSelector :: TyVar -> [TcType] -> [EvExpr] -> EvExpr
evSelector sel_id :: TyVar
sel_id tys :: [TcType]
tys tms :: [EvExpr]
tms = TyVar -> EvExpr
forall b. TyVar -> Expr b
Var TyVar
sel_id EvExpr -> [TcType] -> EvExpr
forall b. Expr b -> [TcType] -> Expr b
`mkTyApps` [TcType]
tys EvExpr -> [EvExpr] -> EvExpr
forall b. Expr b -> [Expr b] -> Expr b
`mkApps` [EvExpr]
tms

-- Dictionary for (Typeable ty)
evTypeable :: Type -> EvTypeable -> EvTerm
evTypeable :: TcType -> EvTypeable -> EvTerm
evTypeable = TcType -> EvTypeable -> EvTerm
EvTypeable

-- | Instructions on how to make a 'Typeable' dictionary.
-- See Note [Typeable evidence terms]
data EvTypeable
  = EvTypeableTyCon TyCon [EvTerm]
    -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
    -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
    -- the applied kinds..

  | EvTypeableTyApp EvTerm EvTerm
    -- ^ Dictionary for @Typeable (s t)@,
    -- given a dictionaries for @s@ and @t@.

  | EvTypeableTrFun EvTerm EvTerm
    -- ^ Dictionary for @Typeable (s -> t)@,
    -- given a dictionaries for @s@ and @t@.

  | EvTypeableTyLit EvTerm
    -- ^ Dictionary for a type literal,
    -- e.g. @Typeable "foo"@ or @Typeable 3@
    -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
    -- (see Trac #10348)
  deriving Typeable EvTypeable
DataType
Constr
Typeable EvTypeable =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTypeable)
-> (EvTypeable -> Constr)
-> (EvTypeable -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTypeable))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c EvTypeable))
-> ((forall b. Data b => b -> b) -> EvTypeable -> EvTypeable)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r)
-> (forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u])
-> (forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> EvTypeable -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable)
-> Data EvTypeable
EvTypeable -> DataType
EvTypeable -> Constr
(forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTypeable
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
BranchIndex -> (forall d. Data d => d -> u) -> EvTypeable -> u
forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTypeable
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
$cEvTypeableTyLit :: Constr
$cEvTypeableTrFun :: Constr
$cEvTypeableTyApp :: Constr
$cEvTypeableTyCon :: Constr
$tEvTypeable :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
gmapMp :: (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
gmapM :: (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
gmapQi :: BranchIndex -> (forall d. Data d => d -> u) -> EvTypeable -> u
$cgmapQi :: forall u.
BranchIndex -> (forall d. Data d => d -> u) -> EvTypeable -> u
gmapQ :: (forall d. Data d => d -> u) -> EvTypeable -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
gmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
$cgmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
dataTypeOf :: EvTypeable -> DataType
$cdataTypeOf :: EvTypeable -> DataType
toConstr :: EvTypeable -> Constr
$ctoConstr :: EvTypeable -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTypeable
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTypeable
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
$cp1Data :: Typeable EvTypeable
Data.Data

-- | Evidence for @CallStack@ implicit parameters.
data EvCallStack
  -- See Note [Overview of implicit CallStacks]
  = EvCsEmpty
  | EvCsPushCall Name RealSrcSpan EvExpr
    -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
    -- @loc@, in a calling context @stk@.
  deriving Typeable EvCallStack
DataType
Constr
Typeable EvCallStack =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvCallStack)
-> (EvCallStack -> Constr)
-> (EvCallStack -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvCallStack))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c EvCallStack))
-> ((forall b. Data b => b -> b) -> EvCallStack -> EvCallStack)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r)
-> (forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u])
-> (forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> EvCallStack -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack)
-> Data EvCallStack
EvCallStack -> DataType
EvCallStack -> Constr
(forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvCallStack
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
BranchIndex -> (forall d. Data d => d -> u) -> EvCallStack -> u
forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvCallStack
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EvCallStack)
$cEvCsPushCall :: Constr
$cEvCsEmpty :: Constr
$tEvCallStack :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
gmapMp :: (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
gmapM :: (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
gmapQi :: BranchIndex -> (forall d. Data d => d -> u) -> EvCallStack -> u
$cgmapQi :: forall u.
BranchIndex -> (forall d. Data d => d -> u) -> EvCallStack -> u
gmapQ :: (forall d. Data d => d -> u) -> EvCallStack -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
gmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
$cgmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EvCallStack)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EvCallStack)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
dataTypeOf :: EvCallStack -> DataType
$cdataTypeOf :: EvCallStack -> DataType
toConstr :: EvCallStack -> Constr
$ctoConstr :: EvCallStack -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvCallStack
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvCallStack
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
$cp1Data :: Typeable EvCallStack
Data.Data

{-
Note [Typeable evidence terms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The EvTypeable data type looks isomorphic to Type, but the EvTerms
inside can be EvIds.  Eg
    f :: forall a. Typeable a => a -> TypeRep
    f x = typeRep (undefined :: Proxy [a])
Here for the (Typeable [a]) dictionary passed to typeRep we make
evidence
    dl :: Typeable [a] = EvTypeable [a]
                            (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
where
    d :: Typable a
is the lambda-bound dictionary passed into f.

Note [Coercion evidence terms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A "coercion evidence term" takes one of these forms
   co_tm ::= EvId v           where v :: t1 ~# t2
           | EvCoercion co
           | EvCast co_tm co

We do quite often need to get a TcCoercion from an EvTerm; see
'evTermCoercion'.

INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
a coercion evidence term.  Consider for example
    [G] d :: F Int a
If we have
    ax7 a :: F Int a ~ (a ~ Bool)
then we do NOT generate the constraint
    [G] (d |> ax7 a) :: a ~ Bool
because that does not satisfy the invariant (d is not a coercion variable).
Instead we make a binding
    g1 :: a~Bool = g |> ax7 a
and the constraint
    [G] g1 :: a~Bool
See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes

Note [EvBinds/EvTerm]
~~~~~~~~~~~~~~~~~~~~~
How evidence is created and updated. Bindings for dictionaries,
and coercions and implicit parameters are carried around in TcEvBinds
which during constraint generation and simplification is always of the
form (TcEvBinds ref). After constraint simplification is finished it
will be transformed to t an (EvBinds ev_bag).

Evidence for coercions *SHOULD* be filled in using the TcEvBinds
However, all EvVars that correspond to *wanted* coercion terms in
an EvBind must be mutable variables so that they can be readily
inlined (by zonking) after constraint simplification is finished.

Conclusion: a new wanted coercion variable should be made mutable.
[Notice though that evidence variables that bind coercion terms
 from super classes will be "given" and hence rigid]


Note [Overview of implicit CallStacks]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)

The goal of CallStack evidence terms is to reify locations
in the program source as runtime values, without any support
from the RTS. We accomplish this by assigning a special meaning
to constraints of type GHC.Stack.Types.HasCallStack, an alias

  type HasCallStack = (?callStack :: CallStack)

Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
important) are solved in three steps:

1. Occurrences of CallStack IPs are solved directly from the given IP,
   just like a regular IP. For example, the occurrence of `?stk` in

     error :: (?stk :: CallStack) => String -> a
     error s = raise (ErrorCall (s ++ prettyCallStack ?stk))

   will be solved for the `?stk` in `error`s context as before.

2. In a function call, instead of simply passing the given IP, we first
   append the current call-site to it. For example, consider a
   call to the callstack-aware `error` above.

     undefined :: (?stk :: CallStack) => a
     undefined = error "undefined!"

   Here we want to take the given `?stk` and append the current
   call-site, before passing it to `error`. In essence, we want to
   rewrite `error "undefined!"` to

     let ?stk = pushCallStack <error's location> ?stk
     in error "undefined!"

   We achieve this effect by emitting a NEW wanted

     [W] d :: IP "stk" CallStack

   from which we build the evidence term

     EvCsPushCall "error" <error's location> (EvId d)

   that we use to solve the call to `error`. The new wanted `d` will
   then be solved per rule (1), ie as a regular IP.

   (see TcInteract.interactDict)

3. We default any insoluble CallStacks to the empty CallStack. Suppose
   `undefined` did not request a CallStack, ie

     undefinedNoStk :: a
     undefinedNoStk = error "undefined!"

   Under the usual IP rules, the new wanted from rule (2) would be
   insoluble as there's no given IP from which to solve it, so we
   would get an "unbound implicit parameter" error.

   We don't ever want to emit an insoluble CallStack IP, so we add a
   defaulting pass to default any remaining wanted CallStacks to the
   empty CallStack with the evidence term

     EvCsEmpty

   (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks)

This provides a lightweight mechanism for building up call-stacks
explicitly, but is notably limited by the fact that the stack will
stop at the first function whose type does not include a CallStack IP.
For example, using the above definition of `undefined`:

  head :: [a] -> a
  head []    = undefined
  head (x:_) = x

  g = head []

the resulting CallStack will include the call to `undefined` in `head`
and the call to `error` in `undefined`, but *not* the call to `head`
in `g`, because `head` did not explicitly request a CallStack.


Important Details:
- GHC should NEVER report an insoluble CallStack constraint.

- GHC should NEVER infer a CallStack constraint unless one was requested
  with a partial type signature (See TcType.pickQuantifiablePreds).

- A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
  where the String is the name of the binder that is used at the
  SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
  package/module/file name, as well as the full source-span. Both
  CallStack and SrcLoc are kept abstract so only GHC can construct new
  values.

- We will automatically solve any wanted CallStack regardless of the
  name of the IP, i.e.

    f = show (?stk :: CallStack)
    g = show (?loc :: CallStack)

  are both valid. However, we will only push new SrcLocs onto existing
  CallStacks when the IP names match, e.g. in

    head :: (?loc :: CallStack) => [a] -> a
    head [] = error (show (?stk :: CallStack))

  the printed CallStack will NOT include head's call-site. This reflects the
  standard scoping rules of implicit-parameters.

- An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
  The desugarer will need to unwrap the IP newtype before pushing a new
  call-site onto a given stack (See DsBinds.dsEvCallStack)

- When we emit a new wanted CallStack from rule (2) we set its origin to
  `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
  (see TcInteract.interactDict).

  This is a bit shady, but is how we ensure that the new wanted is
  solved like a regular IP.

-}

mkEvCast :: EvExpr -> TcCoercion -> EvTerm
mkEvCast :: EvExpr -> TcCoercion -> EvTerm
mkEvCast ev :: EvExpr
ev lco :: TcCoercion
lco
  | ASSERT2( tcCoercionRole lco == Representational
           , (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
    TcCoercion -> Bool
isTcReflCo TcCoercion
lco = EvExpr -> EvTerm
EvExpr EvExpr
ev
  | Bool
otherwise      = EvExpr -> TcCoercion -> EvTerm
evCast EvExpr
ev TcCoercion
lco


mkEvScSelectors         -- Assume   class (..., D ty, ...) => C a b
  :: Class -> [TcType]  -- C ty1 ty2
  -> [(TcPredType,      -- D ty[ty1/a,ty2/b]
       EvExpr)          -- :: C ty1 ty2 -> D ty[ty1/a,ty2/b]
     ]
mkEvScSelectors :: Class -> [TcType] -> [(TcType, EvExpr)]
mkEvScSelectors cls :: Class
cls tys :: [TcType]
tys
   = (TcType -> BranchIndex -> (TcType, EvExpr))
-> [TcType] -> [BranchIndex] -> [(TcType, EvExpr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TcType -> BranchIndex -> (TcType, EvExpr)
forall a b. a -> BranchIndex -> (a, Expr b)
mk_pr (Class -> [TcType] -> [TcType]
immSuperClasses Class
cls [TcType]
tys) [0..]
  where
    mk_pr :: a -> BranchIndex -> (a, Expr b)
mk_pr pred :: a
pred i :: BranchIndex
i = (a
pred, TyVar -> Expr b
forall b. TyVar -> Expr b
Var TyVar
sc_sel_id Expr b -> [TcType] -> Expr b
forall b. Expr b -> [TcType] -> Expr b
`mkTyApps` [TcType]
tys)
      where
        sc_sel_id :: TyVar
sc_sel_id  = Class -> BranchIndex -> TyVar
classSCSelId Class
cls BranchIndex
i -- Zero-indexed

emptyTcEvBinds :: TcEvBinds
emptyTcEvBinds :: TcEvBinds
emptyTcEvBinds = Bag EvBind -> TcEvBinds
EvBinds Bag EvBind
forall a. Bag a
emptyBag

isEmptyTcEvBinds :: TcEvBinds -> Bool
isEmptyTcEvBinds :: TcEvBinds -> Bool
isEmptyTcEvBinds (EvBinds b :: Bag EvBind
b)    = Bag EvBind -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag EvBind
b
isEmptyTcEvBinds (TcEvBinds {}) = String -> Bool
forall a. String -> a
panic "isEmptyTcEvBinds"

evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
-- Applied only to EvTerms of type (s~t)
-- See Note [Coercion evidence terms]
evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
evTermCoercion_maybe ev_term :: EvTerm
ev_term
  | EvExpr e :: EvExpr
e <- EvTerm
ev_term = EvExpr -> Maybe TcCoercion
go EvExpr
e
  | Bool
otherwise           = Maybe TcCoercion
forall a. Maybe a
Nothing
  where
    go :: EvExpr -> Maybe TcCoercion
    go :: EvExpr -> Maybe TcCoercion
go (Var v :: TyVar
v)       = TcCoercion -> Maybe TcCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcCoercion
mkCoVarCo TyVar
v)
    go (Coercion co :: TcCoercion
co) = TcCoercion -> Maybe TcCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return TcCoercion
co
    go (Cast tm :: EvExpr
tm co :: TcCoercion
co)  = do { TcCoercion
co' <- EvExpr -> Maybe TcCoercion
go EvExpr
tm
                          ; TcCoercion -> Maybe TcCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercion -> TcCoercion -> TcCoercion
mkCoCast TcCoercion
co' TcCoercion
co) }
    go _             = Maybe TcCoercion
forall a. Maybe a
Nothing

evTermCoercion :: EvTerm -> TcCoercion
evTermCoercion :: EvTerm -> TcCoercion
evTermCoercion tm :: EvTerm
tm = case EvTerm -> Maybe TcCoercion
evTermCoercion_maybe EvTerm
tm of
                      Just co :: TcCoercion
co -> TcCoercion
co
                      Nothing -> String -> SDoc -> TcCoercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic "evTermCoercion" (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
tm)


{- *********************************************************************
*                                                                      *
                  Free variables
*                                                                      *
********************************************************************* -}

findNeededEvVars :: EvBindMap -> VarSet -> VarSet
-- Find all the Given evidence needed by seeds,
-- looking transitively through binds
findNeededEvVars :: EvBindMap -> TcTyCoVarSet -> TcTyCoVarSet
findNeededEvVars ev_binds :: EvBindMap
ev_binds seeds :: TcTyCoVarSet
seeds
  = (TcTyCoVarSet -> TcTyCoVarSet) -> TcTyCoVarSet -> TcTyCoVarSet
transCloVarSet TcTyCoVarSet -> TcTyCoVarSet
also_needs TcTyCoVarSet
seeds
  where
   also_needs :: VarSet -> VarSet
   also_needs :: TcTyCoVarSet -> TcTyCoVarSet
also_needs needs :: TcTyCoVarSet
needs = (TyVar -> TcTyCoVarSet -> TcTyCoVarSet)
-> TcTyCoVarSet -> TcTyCoVarSet -> TcTyCoVarSet
forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
nonDetFoldUniqSet TyVar -> TcTyCoVarSet -> TcTyCoVarSet
add TcTyCoVarSet
emptyVarSet TcTyCoVarSet
needs
     -- It's OK to use nonDetFoldUFM here because we immediately
     -- forget about the ordering by creating a set

   add :: Var -> VarSet -> VarSet
   add :: TyVar -> TcTyCoVarSet -> TcTyCoVarSet
add v :: TyVar
v needs :: TcTyCoVarSet
needs
     | Just ev_bind :: EvBind
ev_bind <- EvBindMap -> TyVar -> Maybe EvBind
lookupEvBind EvBindMap
ev_binds TyVar
v
     , EvBind { eb_is_given :: EvBind -> Bool
eb_is_given = Bool
is_given, eb_rhs :: EvBind -> EvTerm
eb_rhs = EvTerm
rhs } <- EvBind
ev_bind
     , Bool
is_given
     = EvTerm -> TcTyCoVarSet
evVarsOfTerm EvTerm
rhs TcTyCoVarSet -> TcTyCoVarSet -> TcTyCoVarSet
`unionVarSet` TcTyCoVarSet
needs
     | Bool
otherwise
     = TcTyCoVarSet
needs

evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm :: EvTerm -> TcTyCoVarSet
evVarsOfTerm (EvExpr e :: EvExpr
e)         = InterestingVarFun -> EvExpr -> TcTyCoVarSet
exprSomeFreeVars InterestingVarFun
isEvVar EvExpr
e
evVarsOfTerm (EvTypeable _ ev :: EvTypeable
ev)  = EvTypeable -> TcTyCoVarSet
evVarsOfTypeable EvTypeable
ev
evVarsOfTerm (EvFun {})         = TcTyCoVarSet
emptyVarSet -- See Note [Free vars of EvFun]

evVarsOfTerms :: [EvTerm] -> VarSet
evVarsOfTerms :: [EvTerm] -> TcTyCoVarSet
evVarsOfTerms = (EvTerm -> TcTyCoVarSet) -> [EvTerm] -> TcTyCoVarSet
forall a. (a -> TcTyCoVarSet) -> [a] -> TcTyCoVarSet
mapUnionVarSet EvTerm -> TcTyCoVarSet
evVarsOfTerm

evVarsOfTypeable :: EvTypeable -> VarSet
evVarsOfTypeable :: EvTypeable -> TcTyCoVarSet
evVarsOfTypeable ev :: EvTypeable
ev =
  case EvTypeable
ev of
    EvTypeableTyCon _ e :: [EvTerm]
e   -> (EvTerm -> TcTyCoVarSet) -> [EvTerm] -> TcTyCoVarSet
forall a. (a -> TcTyCoVarSet) -> [a] -> TcTyCoVarSet
mapUnionVarSet EvTerm -> TcTyCoVarSet
evVarsOfTerm [EvTerm]
e
    EvTypeableTyApp e1 :: EvTerm
e1 e2 :: EvTerm
e2 -> [EvTerm] -> TcTyCoVarSet
evVarsOfTerms [EvTerm
e1,EvTerm
e2]
    EvTypeableTrFun e1 :: EvTerm
e1 e2 :: EvTerm
e2 -> [EvTerm] -> TcTyCoVarSet
evVarsOfTerms [EvTerm
e1,EvTerm
e2]
    EvTypeableTyLit e :: EvTerm
e     -> EvTerm -> TcTyCoVarSet
evVarsOfTerm EvTerm
e


{- Note [Free vars of EvFun]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Finding the free vars of an EvFun is made tricky by the fact the
bindings et_binds may be a mutable variable.  Fortunately, we
can just squeeze by.  Here's how.

* evVarsOfTerm is used only by TcSimplify.neededEvVars.
* Each EvBindsVar in an et_binds field of an EvFun is /also/ in the
  ic_binds field of an Implication
* So we can track usage via the processing for that implication,
  (see Note [Tracking redundant constraints] in TcSimplify).
  We can ignore usage from the EvFun altogether.

************************************************************************
*                                                                      *
                  Pretty printing
*                                                                      *
************************************************************************
-}

instance Outputable HsWrapper where
  ppr :: HsWrapper -> SDoc
ppr co_fn :: HsWrapper
co_fn = HsWrapper -> (Bool -> SDoc) -> SDoc
pprHsWrapper HsWrapper
co_fn (SDoc -> Bool -> SDoc
no_parens (String -> SDoc
text "<>"))

pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
-- With -fprint-typechecker-elaboration, print the wrapper
--   otherwise just print what's inside
-- The pp_thing_inside function takes Bool to say whether
--    it's in a position that needs parens for a non-atomic thing
pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
pprHsWrapper wrap :: HsWrapper
wrap pp_thing_inside :: Bool -> SDoc
pp_thing_inside
  = (DynFlags -> SDoc) -> SDoc
sdocWithDynFlags ((DynFlags -> SDoc) -> SDoc) -> (DynFlags -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \ dflags :: DynFlags
dflags ->
    if GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_PrintTypecheckerElaboration DynFlags
dflags
    then (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help Bool -> SDoc
pp_thing_inside HsWrapper
wrap Bool
False
    else Bool -> SDoc
pp_thing_inside Bool
False
  where
    help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    -- True  <=> appears in function application position
    -- False <=> appears as body of let or lambda
    help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help it :: Bool -> SDoc
it WpHole             = Bool -> SDoc
it
    help it :: Bool -> SDoc
it (WpCompose f1 :: HsWrapper
f1 f2 :: HsWrapper
f2)  = (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help ((Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help Bool -> SDoc
it HsWrapper
f2) HsWrapper
f1
    help it :: Bool -> SDoc
it (WpFun f1 :: HsWrapper
f1 f2 :: HsWrapper
f2 t1 :: TcType
t1 _) = SDoc -> Bool -> SDoc
add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "\\(x" SDoc -> SDoc -> SDoc
<> SDoc
dcolon SDoc -> SDoc -> SDoc
<> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
t1 SDoc -> SDoc -> SDoc
<> String -> SDoc
text ")." SDoc -> SDoc -> SDoc
<+>
                                              (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help (\_ -> Bool -> SDoc
it Bool
True SDoc -> SDoc -> SDoc
<+> (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help (\_ -> String -> SDoc
text "x") HsWrapper
f1 Bool
True) HsWrapper
f2 Bool
False
    help it :: Bool -> SDoc
it (WpCast co :: TcCoercion
co)   = SDoc -> Bool -> SDoc
add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [Bool -> SDoc
it Bool
False, BranchIndex -> SDoc -> SDoc
nest 2 (String -> SDoc
text "|>"
                                              SDoc -> SDoc -> SDoc
<+> TcCoercion -> SDoc
pprParendCo TcCoercion
co)]
    help it :: Bool -> SDoc
it (WpEvApp id :: EvTerm
id)  = SDoc -> Bool -> SDoc
no_parens  (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [Bool -> SDoc
it Bool
True, BranchIndex -> SDoc -> SDoc
nest 2 (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
id)]
    help it :: Bool -> SDoc
it (WpTyApp ty :: TcType
ty)  = SDoc -> Bool -> SDoc
no_parens  (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [Bool -> SDoc
it Bool
True, String -> SDoc
text "@" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprParendType TcType
ty]
    help it :: Bool -> SDoc
it (WpEvLam id :: TyVar
id)  = SDoc -> Bool -> SDoc
add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [ String -> SDoc
text "\\" SDoc -> SDoc -> SDoc
<> TyVar -> SDoc
pprLamBndr TyVar
id SDoc -> SDoc -> SDoc
<> SDoc
dot, Bool -> SDoc
it Bool
False]
    help it :: Bool -> SDoc
it (WpTyLam tv :: TyVar
tv)  = SDoc -> Bool -> SDoc
add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [String -> SDoc
text "/\\" SDoc -> SDoc -> SDoc
<> TyVar -> SDoc
pprLamBndr TyVar
tv SDoc -> SDoc -> SDoc
<> SDoc
dot, Bool -> SDoc
it Bool
False]
    help it :: Bool -> SDoc
it (WpLet binds :: TcEvBinds
binds) = SDoc -> Bool -> SDoc
add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [String -> SDoc
text "let" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces (TcEvBinds -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcEvBinds
binds), Bool -> SDoc
it Bool
False]

pprLamBndr :: Id -> SDoc
pprLamBndr :: TyVar -> SDoc
pprLamBndr v :: TyVar
v = BindingSite -> TyVar -> SDoc
forall a. OutputableBndr a => BindingSite -> a -> SDoc
pprBndr BindingSite
LambdaBind TyVar
v

add_parens, no_parens :: SDoc -> Bool -> SDoc
add_parens :: SDoc -> Bool -> SDoc
add_parens d :: SDoc
d True  = SDoc -> SDoc
parens SDoc
d
add_parens d :: SDoc
d False = SDoc
d
no_parens :: SDoc -> Bool -> SDoc
no_parens d :: SDoc
d _ = SDoc
d

instance Outputable TcEvBinds where
  ppr :: TcEvBinds -> SDoc
ppr (TcEvBinds v :: EvBindsVar
v) = EvBindsVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvBindsVar
v
  ppr (EvBinds bs :: Bag EvBind
bs)  = String -> SDoc
text "EvBinds" SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
braces ([SDoc] -> SDoc
vcat ((EvBind -> SDoc) -> [EvBind] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map EvBind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Bag EvBind -> [EvBind]
forall a. Bag a -> [a]
bagToList Bag EvBind
bs)))

instance Outputable EvBindsVar where
  ppr :: EvBindsVar -> SDoc
ppr (EvBindsVar { ebv_uniq :: EvBindsVar -> Unique
ebv_uniq = Unique
u })
     = String -> SDoc
text "EvBindsVar" SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
angleBrackets (Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u)
  ppr (CoEvBindsVar { ebv_uniq :: EvBindsVar -> Unique
ebv_uniq = Unique
u })
     = String -> SDoc
text "CoEvBindsVar" SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
angleBrackets (Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u)

instance Uniquable EvBindsVar where
  getUnique :: EvBindsVar -> Unique
getUnique = EvBindsVar -> Unique
ebv_uniq

instance Outputable EvBind where
  ppr :: EvBind -> SDoc
ppr (EvBind { eb_lhs :: EvBind -> TyVar
eb_lhs = TyVar
v, eb_rhs :: EvBind -> EvTerm
eb_rhs = EvTerm
e, eb_is_given :: EvBind -> Bool
eb_is_given = Bool
is_given })
     = [SDoc] -> SDoc
sep [ SDoc
pp_gw SDoc -> SDoc -> SDoc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
v
           , BranchIndex -> SDoc -> SDoc
nest 2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc
equals SDoc -> SDoc -> SDoc
<+> EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
e ]
     where
       pp_gw :: SDoc
pp_gw = SDoc -> SDoc
brackets (if Bool
is_given then Char -> SDoc
char 'G' else Char -> SDoc
char 'W')
   -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing

instance Outputable EvTerm where
  ppr :: EvTerm -> SDoc
ppr (EvExpr e :: EvExpr
e)         = EvExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvExpr
e
  ppr (EvTypeable ty :: TcType
ty ev :: EvTypeable
ev) = EvTypeable -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTypeable
ev SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "Typeable" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty
  ppr (EvFun { et_tvs :: EvTerm -> [TyVar]
et_tvs = [TyVar]
tvs, et_given :: EvTerm -> [TyVar]
et_given = [TyVar]
gs, et_binds :: EvTerm -> TcEvBinds
et_binds = TcEvBinds
bs, et_body :: EvTerm -> TyVar
et_body = TyVar
w })
      = SDoc -> BranchIndex -> SDoc -> SDoc
hang (String -> SDoc
text "\\" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
sep ((TyVar -> SDoc) -> [TyVar] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> SDoc
pprLamBndr ([TyVar]
tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
gs)) SDoc -> SDoc -> SDoc
<+> SDoc
arrow)
           2 (TcEvBinds -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcEvBinds
bs SDoc -> SDoc -> SDoc
$$ TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
w)   -- Not very pretty

instance Outputable EvCallStack where
  ppr :: EvCallStack -> SDoc
ppr EvCsEmpty
    = String -> SDoc
text "[]"
  ppr (EvCsPushCall name :: Name
name loc :: RealSrcSpan
loc tm :: EvExpr
tm)
    = (Name, RealSrcSpan) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Name
name,RealSrcSpan
loc) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text ":" SDoc -> SDoc -> SDoc
<+> EvExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvExpr
tm

instance Outputable EvTypeable where
  ppr :: EvTypeable -> SDoc
ppr (EvTypeableTyCon ts :: TyCon
ts _)  = String -> SDoc
text "TyCon" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
ts
  ppr (EvTypeableTyApp t1 :: EvTerm
t1 t2 :: EvTerm
t2) = SDoc -> SDoc
parens (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
t1 SDoc -> SDoc -> SDoc
<+> EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
t2)
  ppr (EvTypeableTrFun t1 :: EvTerm
t1 t2 :: EvTerm
t2) = SDoc -> SDoc
parens (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
t1 SDoc -> SDoc -> SDoc
<+> SDoc
arrow SDoc -> SDoc -> SDoc
<+> EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
t2)
  ppr (EvTypeableTyLit t1 :: EvTerm
t1)    = String -> SDoc
text "TyLit" SDoc -> SDoc -> SDoc
<> EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
t1


----------------------------------------------------------------------
-- Helper functions for dealing with IP newtype-dictionaries
----------------------------------------------------------------------

-- | Create a 'Coercion' that unwraps an implicit-parameter or
-- overloaded-label dictionary to expose the underlying value. We
-- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
-- and return a 'Coercion' `co :: IP sym ty ~ ty` or
-- `co :: IsLabel sym ty ~ Proxy# sym -> ty`.  See also
-- Note [Type-checking overloaded labels] in TcExpr.
unwrapIP :: Type -> CoercionR
unwrapIP :: TcType -> TcCoercion
unwrapIP ty :: TcType
ty =
  case TyCon -> Maybe ([TyVar], TcType, CoAxiom Unbranched)
unwrapNewTyCon_maybe TyCon
tc of
    Just (_,_,ax :: CoAxiom Unbranched
ax) -> Role
-> CoAxiom Unbranched -> [TcType] -> [TcCoercion] -> TcCoercion
mkUnbranchedAxInstCo Role
Representational CoAxiom Unbranched
ax [TcType]
tys []
    Nothing       -> String -> SDoc -> TcCoercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic "unwrapIP" (SDoc -> TcCoercion) -> SDoc -> TcCoercion
forall a b. (a -> b) -> a -> b
$
                       String -> SDoc
text "The dictionary for" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc)
                         SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "is not a newtype!"
  where
  (tc :: TyCon
tc, tys :: [TcType]
tys) = TcType -> (TyCon, [TcType])
splitTyConApp TcType
ty

-- | Create a 'Coercion' that wraps a value in an implicit-parameter
-- dictionary. See 'unwrapIP'.
wrapIP :: Type -> CoercionR
wrapIP :: TcType -> TcCoercion
wrapIP ty :: TcType
ty = TcCoercion -> TcCoercion
mkSymCo (TcType -> TcCoercion
unwrapIP TcType
ty)