-- (c) The University of Glasgow 2006

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase #-}

module GHC.Tc.Types.Evidence (

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

  -- * Evidence bindings
  TcEvBinds(..), EvBindsVar(..),
  EvBindMap(..), emptyEvBindMap, extendEvBinds,
  lookupEvBind, evBindMapBinds,
  foldEvBindMap, nonDetStrictFoldEvBindMap,
  filterEvBindMap,
  isEmptyEvBindMap,
  evBindMapToVarSet,
  varSetMinusEvBindMap,
  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(..),

  -- * HoleExprRef
  HoleExprRef(..),

  -- * TcCoercion
  TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
  TcMCoercion, TcMCoercionN, TcMCoercionR,
  Role(..), LeftOrRight(..), pickLR,
  mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
  mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
  mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
  mkTcSymCo, mkTcSymMCo,
  mkTcTransCo,
  mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSymCo,
  maybeTcSubCo, tcDowngradeRole,
  mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflRightMCo, mkTcGReflLeftCo, mkTcGReflLeftMCo,
  mkTcPhantomCo,
  mkTcCoherenceLeftCo,
  mkTcCoherenceRightCo,
  mkTcKindCo,
  tcCoercionKind,
  mkTcCoVarCo,
  mkTcFamilyTyConAppCo,
  isTcReflCo, isTcReflexiveCo,
  tcCoercionRole,
  unwrapIP, wrapIP,

  -- * QuoteWrapper
  QuoteWrapper(..), applyQuoteWrapper, quoteWrapperTyVarTy
  ) where

import GHC.Prelude

import GHC.Types.Unique.DFM
import GHC.Types.Unique.FM
import GHC.Types.Var
import GHC.Core.Coercion.Axiom
import GHC.Core.Coercion
import GHC.Core.Ppr ()   -- Instance OutputableBndr TyVar
import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.DataCon ( DataCon, dataConWrapId )
import GHC.Builtin.Names
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Core.Predicate
import GHC.Data.Pair
import GHC.Types.Basic

import GHC.Core
import GHC.Core.Class (Class, classSCSelId )
import GHC.Core.FVs   ( exprSomeFreeVars )

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

import GHC.Data.Bag
import GHC.Data.FastString

import qualified Data.Data as Data
import GHC.Types.SrcLoc
import Data.IORef( IORef )
import GHC.Types.Unique.Set
import GHC.Core.Multiplicity

import qualified Data.Semigroup as S

{-
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
type TcMCoercion  = MCoercion
type TcMCoercionN = MCoercionN  -- nominal
type TcMCoercionR = MCoercionR  -- representational

mkTcReflCo             :: Role -> TcType -> TcCoercion
mkTcSymCo              :: TcCoercion -> TcCoercion
mkTcSymMCo             :: TcMCoercion -> TcMCoercion
mkTcTransCo            :: TcCoercion -> TcCoercion -> TcCoercion
mkTcNomReflCo          :: TcType -> TcCoercionN
mkTcRepReflCo          :: TcType -> TcCoercionR
mkTcTyConAppCo         :: Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcAppCo              :: TcCoercion -> TcCoercionN -> TcCoercion
mkTcFunCo              :: Role -> TcCoercion -> 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              :: HasDebugCallStack => TcCoercionN -> TcCoercionR
tcDowngradeRole        :: Role -> Role -> TcCoercion -> TcCoercion
mkTcAxiomRuleCo        :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
mkTcGReflRightCo       :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcGReflRightMCo      :: Role -> TcType -> TcMCoercionN -> TcCoercion
mkTcGReflLeftCo        :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcGReflLeftMCo       :: Role -> TcType -> TcMCoercionN -> TcCoercion
mkTcCoherenceLeftCo    :: Role -> TcType -> TcCoercionN
                       -> TcCoercion -> TcCoercion
mkTcCoherenceRightCo   :: Role -> TcType -> TcCoercionN
                       -> TcCoercion -> TcCoercion
mkTcPhantomCo          :: TcCoercionN -> TcType -> TcType -> TcCoercionP
mkTcKindCo             :: TcCoercion -> TcCoercionN
mkTcCoVarCo            :: CoVar -> TcCoercion
mkTcFamilyTyConAppCo   :: TyCon -> [TcCoercionN] -> TcCoercionN

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

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

mkTcReflCo :: Role -> Mult -> TcCoercionR
mkTcReflCo             = Role -> Mult -> TcCoercionR
mkReflCo
mkTcSymCo :: TcCoercionR -> TcCoercionR
mkTcSymCo              = TcCoercionR -> TcCoercionR
mkSymCo
mkTcSymMCo :: TcMCoercion -> TcMCoercion
mkTcSymMCo             = TcMCoercion -> TcMCoercion
mkSymMCo
mkTcTransCo :: TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcTransCo            = TcCoercionR -> TcCoercionR -> TcCoercionR
mkTransCo
mkTcNomReflCo :: Mult -> TcCoercionR
mkTcNomReflCo          = Mult -> TcCoercionR
mkNomReflCo
mkTcRepReflCo :: Mult -> TcCoercionR
mkTcRepReflCo          = Mult -> TcCoercionR
mkRepReflCo
mkTcTyConAppCo :: Role -> TyCon -> [TcCoercionR] -> TcCoercionR
mkTcTyConAppCo         = (() :: Constraint) => Role -> TyCon -> [TcCoercionR] -> TcCoercionR
Role -> TyCon -> [TcCoercionR] -> TcCoercionR
mkTyConAppCo
mkTcAppCo :: TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcAppCo              = TcCoercionR -> TcCoercionR -> TcCoercionR
mkAppCo
mkTcFunCo :: Role -> TcCoercionR -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcFunCo              = Role -> TcCoercionR -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkFunCo
mkTcAxInstCo :: forall (br :: BranchFlag).
Role -> CoAxiom br -> Int -> [Mult] -> [TcCoercionR] -> TcCoercionR
mkTcAxInstCo           = Role -> CoAxiom br -> Int -> [Mult] -> [TcCoercionR] -> TcCoercionR
forall (br :: BranchFlag).
Role -> CoAxiom br -> Int -> [Mult] -> [TcCoercionR] -> TcCoercionR
mkAxInstCo
mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [Mult] -> [TcCoercionR] -> TcCoercionR
mkTcUnbranchedAxInstCo = Role
-> CoAxiom Unbranched -> [Mult] -> [TcCoercionR] -> TcCoercionR
mkUnbranchedAxInstCo Role
Representational
mkTcForAllCo :: Id -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcForAllCo           = Id -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkForAllCo
mkTcForAllCos :: [(Id, TcCoercionR)] -> TcCoercionR -> TcCoercionR
mkTcForAllCos          = [(Id, TcCoercionR)] -> TcCoercionR -> TcCoercionR
mkForAllCos
mkTcNthCo :: Role -> Int -> TcCoercionR -> TcCoercionR
mkTcNthCo              = (() :: Constraint) => Role -> Int -> TcCoercionR -> TcCoercionR
Role -> Int -> TcCoercionR -> TcCoercionR
mkNthCo
mkTcLRCo :: LeftOrRight -> TcCoercionR -> TcCoercionR
mkTcLRCo               = LeftOrRight -> TcCoercionR -> TcCoercionR
mkLRCo
mkTcSubCo :: (() :: Constraint) => TcCoercionR -> TcCoercionR
mkTcSubCo              = (() :: Constraint) => TcCoercionR -> TcCoercionR
TcCoercionR -> TcCoercionR
mkSubCo
tcDowngradeRole :: Role -> Role -> TcCoercionR -> TcCoercionR
tcDowngradeRole        = Role -> Role -> TcCoercionR -> TcCoercionR
downgradeRole
mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercionR] -> TcCoercionR
mkTcAxiomRuleCo        = CoAxiomRule -> [TcCoercionR] -> TcCoercionR
mkAxiomRuleCo
mkTcGReflRightCo :: Role -> Mult -> TcCoercionR -> TcCoercionR
mkTcGReflRightCo       = Role -> Mult -> TcCoercionR -> TcCoercionR
mkGReflRightCo
mkTcGReflRightMCo :: Role -> Mult -> TcMCoercion -> TcCoercionR
mkTcGReflRightMCo      = Role -> Mult -> TcMCoercion -> TcCoercionR
mkGReflRightMCo
mkTcGReflLeftCo :: Role -> Mult -> TcCoercionR -> TcCoercionR
mkTcGReflLeftCo        = Role -> Mult -> TcCoercionR -> TcCoercionR
mkGReflLeftCo
mkTcGReflLeftMCo :: Role -> Mult -> TcMCoercion -> TcCoercionR
mkTcGReflLeftMCo       = Role -> Mult -> TcMCoercion -> TcCoercionR
mkGReflLeftMCo
mkTcCoherenceLeftCo :: Role -> Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcCoherenceLeftCo    = Role -> Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkCoherenceLeftCo
mkTcCoherenceRightCo :: Role -> Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcCoherenceRightCo   = Role -> Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkCoherenceRightCo
mkTcPhantomCo :: TcCoercionR -> Mult -> Mult -> TcCoercionR
mkTcPhantomCo          = TcCoercionR -> Mult -> Mult -> TcCoercionR
mkPhantomCo
mkTcKindCo :: TcCoercionR -> TcCoercionR
mkTcKindCo             = TcCoercionR -> TcCoercionR
mkKindCo
mkTcCoVarCo :: Id -> TcCoercionR
mkTcCoVarCo            = Id -> TcCoercionR
mkCoVarCo
mkTcFamilyTyConAppCo :: TyCon -> [TcCoercionR] -> TcCoercionR
mkTcFamilyTyConAppCo   = TyCon -> [TcCoercionR] -> TcCoercionR
mkFamilyTyConAppCo

tcCoercionKind :: TcCoercionR -> Pair Mult
tcCoercionKind         = TcCoercionR -> Pair Mult
coercionKind
tcCoercionRole :: TcCoercionR -> Role
tcCoercionRole         = TcCoercionR -> Role
coercionRole
isTcReflCo :: TcCoercionR -> Bool
isTcReflCo             = TcCoercionR -> Bool
isReflCo
isTcReflexiveCo :: TcCoercionR -> Bool
isTcReflexiveCo        = TcCoercionR -> Bool
isReflexiveCo

-- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
-- Note that the input coercion should always be nominal.
maybeTcSubCo :: HasDebugCallStack => EqRel -> TcCoercionN -> TcCoercion
maybeTcSubCo :: (() :: Constraint) => EqRel -> TcCoercionR -> TcCoercionR
maybeTcSubCo EqRel
NomEq  = TcCoercionR -> TcCoercionR
forall a. a -> a
id
maybeTcSubCo EqRel
ReprEq = (() :: Constraint) => TcCoercionR -> TcCoercionR
TcCoercionR -> TcCoercionR
mkTcSubCo

-- | If a 'SwapFlag' is 'IsSwapped', flip the orientation of a coercion
maybeTcSymCo :: SwapFlag -> TcCoercion -> TcCoercion
maybeTcSymCo :: SwapFlag -> TcCoercionR -> TcCoercionR
maybeTcSymCo SwapFlag
IsSwapped  TcCoercionR
co = TcCoercionR -> TcCoercionR
mkTcSymCo TcCoercionR
co
maybeTcSymCo SwapFlag
NotSwapped TcCoercionR
co = TcCoercionR
co

{-
%************************************************************************
%*                                                                      *
                  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 (Scaled TcTypeFRR)
       -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w 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
       --
       -- Use 'mkWpFun' to construct such a wrapper.

  | 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

  | WpMultCoercion Coercion     -- Require that a Coercion be reflexive; otherwise,
                                -- error in the desugarer. See GHC.Tc.Utils.Unify
                                -- Note [Wrapper returned from tcSubMult]
  deriving Typeable HsWrapper
Typeable HsWrapper
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HsWrapper)
-> (HsWrapper -> Constr)
-> (HsWrapper -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HsWrapper))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper))
-> ((forall b. Data b => b -> b) -> HsWrapper -> HsWrapper)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r)
-> (forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> HsWrapper -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper)
-> Data HsWrapper
HsWrapper -> Constr
HsWrapper -> DataType
(forall b. Data b => b -> b) -> HsWrapper -> HsWrapper
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. Int -> (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. Int -> (forall d. Data d => d -> u) -> HsWrapper -> u
forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsWrapper
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsWrapper -> c HsWrapper
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsWrapper)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsWrapper -> c HsWrapper
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsWrapper -> c HsWrapper
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsWrapper
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsWrapper
$ctoConstr :: HsWrapper -> Constr
toConstr :: HsWrapper -> Constr
$cdataTypeOf :: HsWrapper -> DataType
dataTypeOf :: HsWrapper -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsWrapper)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsWrapper)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper)
$cgmapT :: (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper
gmapT :: (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HsWrapper -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HsWrapper -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
Data.Data

-- | The Semigroup instance is a bit fishy, since @WpCompose@, as a data
-- constructor, is "syntactic" and not associative. Concretely, if @a@, @b@,
-- and @c@ aren't @WpHole@:
--
-- > (a <> b) <> c ?= a <> (b <> c)
--
-- ==>
--
-- > (a `WpCompose` b) `WpCompose` c /= @ a `WpCompose` (b `WpCompose` c)
--
-- However these two associations are are "semantically equal" in the sense
-- that they produce equal functions when passed to
-- @GHC.HsToCore.Binds.dsHsWrapper@.
instance S.Semigroup HsWrapper where
  <> :: HsWrapper -> HsWrapper -> HsWrapper
(<>) = HsWrapper -> HsWrapper -> HsWrapper
(<.>)

instance Monoid HsWrapper where
  mempty :: HsWrapper
mempty = HsWrapper
WpHole

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

-- | Smart constructor to create a 'WpFun' 'HsWrapper'.
--
-- PRECONDITION: the "from" type of the first wrapper must have a syntactically
-- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
mkWpFun :: HsWrapper -> HsWrapper
        -> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper
                            -- MUST have a fixed RuntimeRep
        -> TcType           -- ^ either type of the second wrapper (used only when the
                            -- second wrapper is the identity)
        -> HsWrapper
  -- NB: we can't check that the argument type has a fixed RuntimeRep with an assertion,
  -- because of [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]
  -- in GHC.Tc.Utils.Concrete.
mkWpFun :: HsWrapper -> HsWrapper -> Scaled Mult -> Mult -> HsWrapper
mkWpFun HsWrapper
WpHole       HsWrapper
WpHole       Scaled Mult
_             Mult
_  = HsWrapper
WpHole
mkWpFun HsWrapper
WpHole       (WpCast TcCoercionR
co2) (Scaled Mult
w Mult
t1) Mult
_  = TcCoercionR -> HsWrapper
WpCast (Role -> TcCoercionR -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcFunCo Role
Representational (Mult -> TcCoercionR
multToCo Mult
w) (Mult -> TcCoercionR
mkTcRepReflCo Mult
t1) TcCoercionR
co2)
mkWpFun (WpCast TcCoercionR
co1) HsWrapper
WpHole       (Scaled Mult
w Mult
_)  Mult
t2 = TcCoercionR -> HsWrapper
WpCast (Role -> TcCoercionR -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcFunCo Role
Representational (Mult -> TcCoercionR
multToCo Mult
w) (TcCoercionR -> TcCoercionR
mkTcSymCo TcCoercionR
co1) (Mult -> TcCoercionR
mkTcRepReflCo Mult
t2))
mkWpFun (WpCast TcCoercionR
co1) (WpCast TcCoercionR
co2) (Scaled Mult
w Mult
_)  Mult
_  = TcCoercionR -> HsWrapper
WpCast (Role -> TcCoercionR -> TcCoercionR -> TcCoercionR -> TcCoercionR
mkTcFunCo Role
Representational (Mult -> TcCoercionR
multToCo Mult
w) (TcCoercionR -> TcCoercionR
mkTcSymCo TcCoercionR
co1) TcCoercionR
co2)
mkWpFun HsWrapper
co1          HsWrapper
co2          Scaled Mult
t1            Mult
_  = HsWrapper -> HsWrapper -> Scaled Mult -> HsWrapper
WpFun HsWrapper
co1 HsWrapper
co2 Scaled Mult
t1

mkWpCastR :: TcCoercionR -> HsWrapper
mkWpCastR :: TcCoercionR -> HsWrapper
mkWpCastR TcCoercionR
co
  | TcCoercionR -> Bool
isTcReflCo TcCoercionR
co = HsWrapper
WpHole
  | Bool
otherwise     = Bool -> SDoc -> HsWrapper -> HsWrapper
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcCoercionR -> Role
tcCoercionRole TcCoercionR
co Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Representational) (TcCoercionR -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionR
co) (HsWrapper -> HsWrapper) -> HsWrapper -> HsWrapper
forall a b. (a -> b) -> a -> b
$
                    TcCoercionR -> HsWrapper
WpCast TcCoercionR
co

mkWpCastN :: TcCoercionN -> HsWrapper
mkWpCastN :: TcCoercionR -> HsWrapper
mkWpCastN TcCoercionR
co
  | TcCoercionR -> Bool
isTcReflCo TcCoercionR
co = HsWrapper
WpHole
  | Bool
otherwise     = Bool -> SDoc -> HsWrapper -> HsWrapper
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcCoercionR -> Role
tcCoercionRole TcCoercionR
co Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (TcCoercionR -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionR
co) (HsWrapper -> HsWrapper) -> HsWrapper -> HsWrapper
forall a b. (a -> b) -> a -> b
$
                    TcCoercionR -> HsWrapper
WpCast ((() :: Constraint) => TcCoercionR -> TcCoercionR
TcCoercionR -> TcCoercionR
mkTcSubCo TcCoercionR
co)
    -- The mkTcSubCo converts Nominal to Representational

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

mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvApps [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 :: [Id] -> HsWrapper
mkWpEvVarApps [Id]
vs = (EvTerm -> HsWrapper) -> [EvTerm] -> HsWrapper
forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn EvTerm -> HsWrapper
WpEvApp ((Id -> EvTerm) -> [Id] -> [EvTerm]
forall a b. (a -> b) -> [a] -> [b]
map (EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> (Id -> EvExpr) -> Id -> EvTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> EvExpr
evId) [Id]
vs)

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

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

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

mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn :: forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn a -> HsWrapper
f [a]
as = (a -> HsWrapper -> HsWrapper) -> HsWrapper -> [a] -> HsWrapper
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x 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 :: forall a. (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn a -> HsWrapper
f [a]
as = (a -> HsWrapper -> HsWrapper) -> HsWrapper -> [a] -> HsWrapper
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x 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 HsWrapper
WpHole = Bool
True
isIdHsWrapper HsWrapper
_      = Bool
False

hsWrapDictBinders :: HsWrapper -> Bag DictId
-- ^ Identifies the /lambda-bound/ dictionaries of an 'HsWrapper'. This is used
-- (only) to allow the pattern-match overlap checker to know what Given
-- dictionaries are in scope.
--
-- We specifically do not collect dictionaries bound in a 'WpLet'. These are
-- either superclasses of lambda-bound ones, or (extremely numerous) results of
-- binding Wanted dictionaries.  We definitely don't want all those cluttering
-- up the Given dictionaries for pattern-match overlap checking!
hsWrapDictBinders :: HsWrapper -> Bag Id
hsWrapDictBinders HsWrapper
wrap = HsWrapper -> Bag Id
go HsWrapper
wrap
 where
   go :: HsWrapper -> Bag Id
go (WpEvLam Id
dict_id)   = Id -> Bag Id
forall a. a -> Bag a
unitBag Id
dict_id
   go (HsWrapper
w1 `WpCompose` HsWrapper
w2) = HsWrapper -> Bag Id
go HsWrapper
w1 Bag Id -> Bag Id -> Bag Id
forall a. Bag a -> Bag a -> Bag a
`unionBags` HsWrapper -> Bag Id
go HsWrapper
w2
   go (WpFun HsWrapper
_ HsWrapper
w Scaled Mult
_)       = HsWrapper -> Bag Id
go HsWrapper
w
   go HsWrapper
WpHole              = Bag Id
forall a. Bag a
emptyBag
   go (WpCast  {})        = Bag Id
forall a. Bag a
emptyBag
   go (WpEvApp {})        = Bag Id
forall a. Bag a
emptyBag
   go (WpTyLam {})        = Bag Id
forall a. Bag a
emptyBag
   go (WpTyApp {})        = Bag Id
forall a. Bag a
emptyBag
   go (WpLet   {})        = Bag Id
forall a. Bag a
emptyBag
   go (WpMultCoercion {}) = Bag Id
forall a. Bag a
emptyBag

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 -> ([Id], HsWrapper)
collectHsWrapBinders HsWrapper
wrap = HsWrapper -> [HsWrapper] -> ([Id], HsWrapper)
go HsWrapper
wrap []
  where
    -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn)
    go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
    go :: HsWrapper -> [HsWrapper] -> ([Id], HsWrapper)
go (WpEvLam Id
v)       [HsWrapper]
wraps = Id -> ([Id], HsWrapper) -> ([Id], HsWrapper)
forall {a} {b}. a -> ([a], b) -> ([a], b)
add_lam Id
v ([HsWrapper] -> ([Id], HsWrapper)
gos [HsWrapper]
wraps)
    go (WpTyLam Id
v)       [HsWrapper]
wraps = Id -> ([Id], HsWrapper) -> ([Id], HsWrapper)
forall {a} {b}. a -> ([a], b) -> ([a], b)
add_lam Id
v ([HsWrapper] -> ([Id], HsWrapper)
gos [HsWrapper]
wraps)
    go (WpCompose HsWrapper
w1 HsWrapper
w2) [HsWrapper]
wraps = HsWrapper -> [HsWrapper] -> ([Id], HsWrapper)
go HsWrapper
w1 (HsWrapper
w2HsWrapper -> [HsWrapper] -> [HsWrapper]
forall a. a -> [a] -> [a]
:[HsWrapper]
wraps)
    go HsWrapper
wrap              [HsWrapper]
wraps = ([], (HsWrapper -> HsWrapper -> HsWrapper)
-> HsWrapper -> [HsWrapper] -> HsWrapper
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HsWrapper -> HsWrapper -> HsWrapper
(<.>) HsWrapper
wrap [HsWrapper]
wraps)

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

    add_lam :: a -> ([a], b) -> ([a], b)
add_lam a
v ([a]
vs,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 CoVarSet
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 GHC.Tc.Solver
    }

  | 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 TcEvBinds
_   = String -> Constr
abstractConstr String
"TcEvBinds"
  gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TcEvBinds
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_  = String -> Constr -> c TcEvBinds
forall a. HasCallStack => String -> a
error String
"gunfold"
  dataTypeOf :: TcEvBinds -> DataType
dataTypeOf TcEvBinds
_ = String -> DataType
Data.mkNoRepType String
"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

  - 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 GHC.Types.Unique.DFM for explanation why
            -- @UniqFM@ can lead to nondeterministic order.

emptyEvBindMap :: EvBindMap
emptyEvBindMap :: EvBindMap
emptyEvBindMap = 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 EvBindMap
bs EvBind
ev_bind
  = EvBindMap { ev_bind_varenv :: DVarEnv EvBind
ev_bind_varenv = DVarEnv EvBind -> Id -> EvBind -> DVarEnv EvBind
forall a. DVarEnv a -> Id -> a -> DVarEnv a
extendDVarEnv (EvBindMap -> DVarEnv EvBind
ev_bind_varenv EvBindMap
bs)
                                               (EvBind -> Id
eb_lhs EvBind
ev_bind)
                                               EvBind
ev_bind }

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

lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
lookupEvBind :: EvBindMap -> Id -> Maybe EvBind
lookupEvBind EvBindMap
bs = DVarEnv EvBind -> Id -> Maybe EvBind
forall a. DVarEnv a -> Id -> 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 :: forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
foldEvBindMap EvBind -> a -> a
k a
z 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)

-- See Note [Deterministic UniqFM] to learn about nondeterminism.
-- If you use this please provide a justification why it doesn't introduce
-- nondeterminism.
nonDetStrictFoldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
nonDetStrictFoldEvBindMap :: forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
nonDetStrictFoldEvBindMap EvBind -> a -> a
k a
z EvBindMap
bs = (EvBind -> a -> a) -> a -> DVarEnv EvBind -> a
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
nonDetStrictFoldDVarEnv 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 EvBind -> Bool
k (EvBindMap { ev_bind_varenv :: EvBindMap -> DVarEnv EvBind
ev_bind_varenv = DVarEnv EvBind
env })
  = 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 }

evBindMapToVarSet :: EvBindMap -> VarSet
evBindMapToVarSet :: EvBindMap -> CoVarSet
evBindMapToVarSet (EvBindMap DVarEnv EvBind
dve) = UniqFM Id Id -> CoVarSet
forall a. UniqFM a a -> UniqSet a
unsafeUFMToUniqSet ((EvBind -> Id) -> UniqFM Id EvBind -> UniqFM Id Id
forall elt1 elt2 key.
(elt1 -> elt2) -> UniqFM key elt1 -> UniqFM key elt2
mapUFM EvBind -> Id
evBindVar (DVarEnv EvBind -> UniqFM Id EvBind
forall key elt. UniqDFM key elt -> UniqFM key elt
udfmToUfm DVarEnv EvBind
dve))

varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet
varSetMinusEvBindMap :: CoVarSet -> EvBindMap -> CoVarSet
varSetMinusEvBindMap CoVarSet
vs (EvBindMap DVarEnv EvBind
dve) = CoVarSet
vs CoVarSet -> DVarEnv EvBind -> CoVarSet
forall key b. UniqSet key -> UniqDFM key b -> UniqSet key
`uniqSetMinusUDFM` DVarEnv EvBind
dve

instance Outputable EvBindMap where
  ppr :: EvBindMap -> SDoc
ppr (EvBindMap 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 -> Id
eb_lhs      :: EvVar
           , EvBind -> EvTerm
eb_rhs      :: EvTerm
           , EvBind -> Bool
eb_is_given :: Bool  -- True <=> given
                 -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
    }

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

mkWantedEvBind :: EvVar -> EvTerm -> EvBind
mkWantedEvBind :: Id -> EvTerm -> EvBind
mkWantedEvBind Id
ev EvTerm
tm = EvBind { eb_is_given :: Bool
eb_is_given = Bool
False, eb_lhs :: Id
eb_lhs = Id
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 :: Id -> EvTerm -> EvBind
mkGivenEvBind Id
ev EvTerm
tm = EvBind { eb_is_given :: Bool
eb_is_given = Bool
True, eb_lhs :: Id
eb_lhs = Id
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 -> [Id]
et_tvs   :: [TyVar]
      , EvTerm -> [Id]
et_given :: [EvVar]
      , EvTerm -> TcEvBinds
et_binds :: TcEvBinds -- This field is why we need an EvFun
                              -- constructor, and can't just use EvExpr
      , EvTerm -> Id
et_body  :: EvVar }

  deriving Typeable EvTerm
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. Int -> (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 -> Constr
EvTerm -> DataType
(forall b. Data b => b -> b) -> EvTerm -> 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. Int -> (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. Int -> (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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTerm -> c EvTerm
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTerm -> c EvTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTerm
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTerm
$ctoConstr :: EvTerm -> Constr
toConstr :: EvTerm -> Constr
$cdataTypeOf :: EvTerm -> DataType
dataTypeOf :: EvTerm -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTerm)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
$cgmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm
gmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvTerm -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> EvTerm -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTerm -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTerm -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTerm -> m 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 GHC.Tc.Types.EvTerm

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

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

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

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

evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp :: DataCon -> [Mult] -> [EvExpr] -> EvTerm
evDataConApp DataCon
dc [Mult]
tys [EvExpr]
ets = Id -> [Mult] -> [EvExpr] -> EvTerm
evDFunApp (DataCon -> Id
dataConWrapId DataCon
dc) [Mult]
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 :: Id -> [Mult] -> [EvExpr] -> EvExpr
evSelector Id
sel_id [Mult]
tys [EvExpr]
tms = Id -> EvExpr
forall b. Id -> Expr b
Var Id
sel_id EvExpr -> [Mult] -> EvExpr
forall b. Expr b -> [Mult] -> Expr b
`mkTyApps` [Mult]
tys EvExpr -> [EvExpr] -> EvExpr
forall b. Expr b -> [Expr b] -> Expr b
`mkApps` [EvExpr]
tms

-- Dictionary for (Typeable ty)
evTypeable :: Type -> EvTypeable -> EvTerm
evTypeable :: Mult -> EvTypeable -> EvTerm
evTypeable = Mult -> 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 EvTerm
    -- ^ Dictionary for @Typeable (s % w -> t)@,
    -- given a dictionaries for @w@, @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 #10348)
  deriving Typeable EvTypeable
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.
    Int -> (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 -> Constr
EvTypeable -> DataType
(forall b. Data b => b -> b) -> EvTypeable -> 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. Int -> (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. Int -> (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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTypeable
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvTypeable
$ctoConstr :: EvTypeable -> Constr
toConstr :: EvTypeable -> Constr
$cdataTypeOf :: EvTypeable -> DataType
dataTypeOf :: EvTypeable -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
$cgmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
gmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTypeable -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTypeable -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
Data.Data

-- | Evidence for @CallStack@ implicit parameters.
data EvCallStack
  -- See Note [Overview of implicit CallStacks]
  = EvCsEmpty
  | EvCsPushCall
        FastString   -- Usually the name of the function being called
                     --   but can also be "the literal 42"
                     --   or "an if-then-else expression", etc
        RealSrcSpan  -- Location of the call
        EvExpr       -- Rest of the stack
    -- ^ @EvCsPushCall origin loc stk@ represents a call from @origin@,
    --  occurring at @loc@, in a calling context @stk@.
  deriving Typeable EvCallStack
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.
    Int -> (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 -> Constr
EvCallStack -> DataType
(forall b. Data b => b -> b) -> EvCallStack -> 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. Int -> (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. Int -> (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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvCallStack
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EvCallStack
$ctoConstr :: EvCallStack -> Constr
toConstr :: EvCallStack -> Constr
$cdataTypeOf :: EvCallStack -> DataType
dataTypeOf :: EvCallStack -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EvCallStack)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EvCallStack)
$cgmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
gmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvCallStack -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvCallStack -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
Data.Data

{-
************************************************************************
*                                                                      *
         Evidence for holes
*                                                                      *
************************************************************************
-}

-- | Where to store evidence for expression holes
-- See Note [Holes] in GHC.Tc.Types.Constraint
data HoleExprRef = HER (IORef EvTerm)   -- ^ where to write the erroring expression
                       TcType           -- ^ expected type of that expression
                       Unique           -- ^ for debug output only

instance Outputable HoleExprRef where
  ppr :: HoleExprRef -> SDoc
ppr (HER IORef EvTerm
_ Mult
_ Unique
u) = Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u

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

{-
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 #7238 and Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint

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://gitlab.haskell.org/ghc/ghc/wikis/explicit-call-stack/implicit-locations)

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. Explicit, user-written occurrences of `?stk :: CallStack`
   which have IPOccOrigin, are solved directly from the given IP,
   just like a regular IP; see GHC.Tc.Solver.Interact.interactDict.

   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.

     foo :: (?stk :: CallStack) => a
     foo = 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 `foo "undefined!"` to

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

   We achieve this as follows:

   * At a call of foo :: (?stk :: CallStack) => blah
     we emit a Wanted
        [W] d1 : IP "stk" CallStack
     with CtOrigin = OccurrenceOf "foo"

   * We /solve/ this constraint, in GHC.Tc.Solver.Canonical.canClassNC
     by emitting a NEW Wanted
        [W] d2 :: IP "stk" CallStack
     with CtOrigin = IPOccOrigin

     and solve d1 = EvCsPushCall "foo" <foo's location> (EvId d1)

   * The new Wanted, for `d2` will be solved per rule (1), ie as a regular IP.

3. We use the predicate isPushCallStackOrigin to identify whether we
   want to do (1) solve directly, or (2) push and then solve directly.
   Key point (see #19918): the CtOrigin where we want to push an item on the
   call stack can include IfThenElseOrigin etc, when RebindableSyntax is
   involved.  See the defn of fun_orig in GHC.Tc.Gen.App.tcInstFun; it is
   this CtOrigin that is pinned on the constraints generated by functions
   in the "expansion" for rebindable syntax. c.f. GHC.Rename.Expr
   Note [Handling overloaded and rebindable constructs]

4. 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 GHC.Tc.Solver.simplifyTopWanteds and GHC.Tc.Solver.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 GHC.Tc.Solver..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 GHC.HsToCore.Binds.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 GHC.Tc.Solver.Interact.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 -> TcCoercionR -> EvTerm
mkEvCast EvExpr
ev TcCoercionR
lco
  | Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcCoercionR -> Role
tcCoercionRole TcCoercionR
lco Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Representational)
              ([SDoc] -> SDoc
vcat [String -> SDoc
text String
"Coercion of wrong role passed to mkEvCast:", EvExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvExpr
ev, TcCoercionR -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionR
lco]) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
    TcCoercionR -> Bool
isTcReflCo TcCoercionR
lco = EvExpr -> EvTerm
EvExpr EvExpr
ev
  | Bool
otherwise      = EvExpr -> TcCoercionR -> EvTerm
evCast EvExpr
ev TcCoercionR
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 -> [Mult] -> [(Mult, EvExpr)]
mkEvScSelectors Class
cls [Mult]
tys
   = (Mult -> Int -> (Mult, EvExpr))
-> [Mult] -> [Int] -> [(Mult, EvExpr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Mult -> Int -> (Mult, EvExpr)
mk_pr (Class -> [Mult] -> [Mult]
immSuperClasses Class
cls [Mult]
tys) [Int
0..]
  where
    mk_pr :: Mult -> Int -> (Mult, EvExpr)
mk_pr Mult
pred Int
i = (Mult
pred, Id -> EvExpr
forall b. Id -> Expr b
Var Id
sc_sel_id EvExpr -> [Mult] -> EvExpr
forall b. Expr b -> [Mult] -> Expr b
`mkTyApps` [Mult]
tys)
      where
        sc_sel_id :: Id
sc_sel_id  = Class -> Int -> Id
classSCSelId Class
cls Int
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 Bag EvBind
b)    = Bag EvBind -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag EvBind
b
isEmptyTcEvBinds (TcEvBinds {}) = String -> Bool
forall a. String -> a
panic String
"isEmptyTcEvBinds"

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

evTermCoercion :: EvTerm -> TcCoercion
evTermCoercion :: EvTerm -> TcCoercionR
evTermCoercion EvTerm
tm = case EvTerm -> Maybe TcCoercionR
evTermCoercion_maybe EvTerm
tm of
                      Just TcCoercionR
co -> TcCoercionR
co
                      Maybe TcCoercionR
Nothing -> String -> SDoc -> TcCoercionR
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"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 -> CoVarSet -> CoVarSet
findNeededEvVars EvBindMap
ev_binds CoVarSet
seeds
  = (CoVarSet -> CoVarSet) -> CoVarSet -> CoVarSet
transCloVarSet CoVarSet -> CoVarSet
also_needs CoVarSet
seeds
  where
   also_needs :: VarSet -> VarSet
   also_needs :: CoVarSet -> CoVarSet
also_needs CoVarSet
needs = (Id -> CoVarSet -> CoVarSet) -> CoVarSet -> CoVarSet -> CoVarSet
forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
nonDetStrictFoldUniqSet Id -> CoVarSet -> CoVarSet
add CoVarSet
emptyVarSet CoVarSet
needs
     -- It's OK to use a non-deterministic fold here because we immediately
     -- forget about the ordering by creating a set

   add :: Var -> VarSet -> VarSet
   add :: Id -> CoVarSet -> CoVarSet
add Id
v CoVarSet
needs
     | Just EvBind
ev_bind <- EvBindMap -> Id -> Maybe EvBind
lookupEvBind EvBindMap
ev_binds Id
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 -> CoVarSet
evVarsOfTerm EvTerm
rhs CoVarSet -> CoVarSet -> CoVarSet
`unionVarSet` CoVarSet
needs
     | Bool
otherwise
     = CoVarSet
needs

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

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

evVarsOfTypeable :: EvTypeable -> VarSet
evVarsOfTypeable :: EvTypeable -> CoVarSet
evVarsOfTypeable EvTypeable
ev =
  case EvTypeable
ev of
    EvTypeableTyCon TyCon
_ [EvTerm]
e      -> (EvTerm -> CoVarSet) -> [EvTerm] -> CoVarSet
forall a. (a -> CoVarSet) -> [a] -> CoVarSet
mapUnionVarSet EvTerm -> CoVarSet
evVarsOfTerm [EvTerm]
e
    EvTypeableTyApp EvTerm
e1 EvTerm
e2    -> [EvTerm] -> CoVarSet
evVarsOfTerms [EvTerm
e1,EvTerm
e2]
    EvTypeableTrFun EvTerm
em EvTerm
e1 EvTerm
e2 -> [EvTerm] -> CoVarSet
evVarsOfTerms [EvTerm
em,EvTerm
e1,EvTerm
e2]
    EvTypeableTyLit EvTerm
e        -> EvTerm -> CoVarSet
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 GHC.Tc.Solver.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 GHC.Tc.Solver).
  We can ignore usage from the EvFun altogether.

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

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

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 HsWrapper
wrap Bool -> SDoc
pp_thing_inside
  = (SDocContext -> Bool) -> (Bool -> SDoc) -> SDoc
forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
sdocOption SDocContext -> Bool
sdocPrintTypecheckerElaboration ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \case
      Bool
True  -> (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help Bool -> SDoc
pp_thing_inside HsWrapper
wrap Bool
False
      Bool
False -> 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 Bool -> SDoc
it HsWrapper
WpHole             = Bool -> SDoc
it
    help Bool -> SDoc
it (WpCompose HsWrapper
f1 HsWrapper
f2)  = (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help ((Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help Bool -> SDoc
it HsWrapper
f2) HsWrapper
f1
    help Bool -> SDoc
it (WpFun HsWrapper
f1 HsWrapper
f2 (Scaled Mult
w Mult
t1)) = SDoc -> Bool -> SDoc
add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"\\(x" SDoc -> SDoc -> SDoc
<> SDoc
dcolon SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
brackets (Mult -> SDoc
forall a. Outputable a => a -> SDoc
ppr Mult
w) SDoc -> SDoc -> SDoc
<> Mult -> SDoc
forall a. Outputable a => a -> SDoc
ppr Mult
t1 SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
")." SDoc -> SDoc -> SDoc
<+>
                                            (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help (\Bool
_ -> Bool -> SDoc
it Bool
True SDoc -> SDoc -> SDoc
<+> (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help (\Bool
_ -> String -> SDoc
text String
"x") HsWrapper
f1 Bool
True) HsWrapper
f2 Bool
False
    help Bool -> SDoc
it (WpCast TcCoercionR
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, Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"|>"
                                              SDoc -> SDoc -> SDoc
<+> TcCoercionR -> SDoc
pprParendCo TcCoercionR
co)]
    help Bool -> SDoc
it (WpEvApp 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, Int -> SDoc -> SDoc
nest Int
2 (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
id)]
    help Bool -> SDoc
it (WpTyApp Mult
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 String
"@" SDoc -> SDoc -> SDoc
<> Mult -> SDoc
pprParendType Mult
ty]
    help Bool -> SDoc
it (WpEvLam Id
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 String
"\\" SDoc -> SDoc -> SDoc
<> Id -> SDoc
pprLamBndr Id
id SDoc -> SDoc -> SDoc
<> SDoc
dot, Bool -> SDoc
it Bool
False]
    help Bool -> SDoc
it (WpTyLam Id
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 String
"/\\" SDoc -> SDoc -> SDoc
<> Id -> SDoc
pprLamBndr Id
tv SDoc -> SDoc -> SDoc
<> SDoc
dot, Bool -> SDoc
it Bool
False]
    help Bool -> SDoc
it (WpLet 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 String
"let" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces (TcEvBinds -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcEvBinds
binds), Bool -> SDoc
it Bool
False]
    help Bool -> SDoc
it (WpMultCoercion TcCoercionR
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, Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"<multiplicity coercion>"
                                              SDoc -> SDoc -> SDoc
<+> TcCoercionR -> SDoc
pprParendCo TcCoercionR
co)]

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

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

instance Outputable TcEvBinds where
  ppr :: TcEvBinds -> SDoc
ppr (TcEvBinds EvBindsVar
v) = EvBindsVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvBindsVar
v
  ppr (EvBinds Bag EvBind
bs)  = String -> SDoc
text String
"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 String
"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 String
"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 -> Id
eb_lhs = Id
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
<+> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v
           , Int -> SDoc -> SDoc
nest Int
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 Char
'G' else Char -> SDoc
char 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 EvExpr
e)         = EvExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvExpr
e
  ppr (EvTypeable Mult
ty EvTypeable
ev) = EvTypeable -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTypeable
ev SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"Typeable" SDoc -> SDoc -> SDoc
<+> Mult -> SDoc
forall a. Outputable a => a -> SDoc
ppr Mult
ty
  ppr (EvFun { et_tvs :: EvTerm -> [Id]
et_tvs = [Id]
tvs, et_given :: EvTerm -> [Id]
et_given = [Id]
gs, et_binds :: EvTerm -> TcEvBinds
et_binds = TcEvBinds
bs, et_body :: EvTerm -> Id
et_body = Id
w })
      = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"\\" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
sep ((Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SDoc
pprLamBndr ([Id]
tvs [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id]
gs)) SDoc -> SDoc -> SDoc
<+> SDoc
arrow)
           Int
2 (TcEvBinds -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcEvBinds
bs SDoc -> SDoc -> SDoc
$$ Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
w)   -- Not very pretty

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

instance Outputable EvTypeable where
  ppr :: EvTypeable -> SDoc
ppr (EvTypeableTyCon TyCon
ts [EvTerm]
_)  = String -> SDoc
text String
"TyCon" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
ts
  ppr (EvTypeableTyApp EvTerm
t1 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 EvTerm
tm EvTerm
t1 EvTerm
t2) = SDoc -> SDoc
parens (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
t1 SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
mulArrow (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
tm) SDoc -> SDoc -> SDoc
<+> EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
t2)
  ppr (EvTypeableTyLit EvTerm
t1)    = String -> SDoc
text String
"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
-- dictionary to expose the underlying value.
-- We expect the 'Type' to have the form `IP sym ty`,
-- and return a 'Coercion' `co :: IP sym ty ~ ty`
unwrapIP :: Type -> CoercionR
unwrapIP :: Mult -> TcCoercionR
unwrapIP Mult
ty =
  case TyCon -> Maybe ([Id], Mult, CoAxiom Unbranched)
unwrapNewTyCon_maybe TyCon
tc of
    Just ([Id]
_,Mult
_,CoAxiom Unbranched
ax) -> Role
-> CoAxiom Unbranched -> [Mult] -> [TcCoercionR] -> TcCoercionR
mkUnbranchedAxInstCo Role
Representational CoAxiom Unbranched
ax [Mult]
tys []
    Maybe ([Id], Mult, CoAxiom Unbranched)
Nothing       -> String -> SDoc -> TcCoercionR
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"unwrapIP" (SDoc -> TcCoercionR) -> SDoc -> TcCoercionR
forall a b. (a -> b) -> a -> b
$
                       String -> SDoc
text String
"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 String
"is not a newtype!"
  where
  (TyCon
tc, [Mult]
tys) = Mult -> (TyCon, [Mult])
splitTyConApp Mult
ty

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

----------------------------------------------------------------------
-- A datatype used to pass information when desugaring quotations
----------------------------------------------------------------------

-- We have to pass a `EvVar` and `Type` into `dsBracket` so that the
-- correct evidence and types are applied to all the TH combinators.
-- This data type bundles them up together with some convenience methods.
--
-- The EvVar is evidence for `Quote m`
-- The Type is a metavariable for `m`
--
data QuoteWrapper = QuoteWrapper EvVar Type deriving Typeable QuoteWrapper
Typeable QuoteWrapper
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QuoteWrapper)
-> (QuoteWrapper -> Constr)
-> (QuoteWrapper -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c QuoteWrapper))
-> ((forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r)
-> (forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper)
-> Data QuoteWrapper
QuoteWrapper -> Constr
QuoteWrapper -> DataType
(forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper
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. Int -> (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. Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u
forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QuoteWrapper
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QuoteWrapper)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QuoteWrapper
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QuoteWrapper
$ctoConstr :: QuoteWrapper -> Constr
toConstr :: QuoteWrapper -> Constr
$cdataTypeOf :: QuoteWrapper -> DataType
dataTypeOf :: QuoteWrapper -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QuoteWrapper)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QuoteWrapper)
$cgmapT :: (forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper
gmapT :: (forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
Data.Data

quoteWrapperTyVarTy :: QuoteWrapper -> Type
quoteWrapperTyVarTy :: QuoteWrapper -> Mult
quoteWrapperTyVarTy (QuoteWrapper Id
_ Mult
t) = Mult
t

-- | Convert the QuoteWrapper into a normal HsWrapper which can be used to
-- apply its contents.
applyQuoteWrapper :: QuoteWrapper -> HsWrapper
applyQuoteWrapper :: QuoteWrapper -> HsWrapper
applyQuoteWrapper (QuoteWrapper Id
ev_var Mult
m_var)
  = [Id] -> HsWrapper
mkWpEvVarApps [Id
ev_var] HsWrapper -> HsWrapper -> HsWrapper
<.> [Mult] -> HsWrapper
mkWpTyApps [Mult
m_var]