{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

\section{@Vars@: Variables}
-}

{-# LANGUAGE MultiWayIf, PatternSynonyms #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
{-# LANGUAGE DeriveFunctor #-}

-- |
-- #name_types#
-- GHC uses several kinds of name internally:
--
-- * 'GHC.Types.Name.Occurrence.OccName': see "GHC.Types.Name.Occurrence#name_types"
--
-- * 'GHC.Types.Name.Reader.RdrName': see "GHC.Types.Name.Reader#name_types"
--
-- * 'GHC.Types.Name.Name': see "GHC.Types.Name#name_types"
--
-- * 'GHC.Types.Id.Id': see "GHC.Types.Id#name_types"
--
-- * 'GHC.Types.Var.Var' is a synonym for the 'GHC.Types.Id.Id' type but it may additionally
--   potentially contain type variables, which have a 'GHC.Core.TyCo.Rep.Kind'
--   rather than a 'GHC.Core.TyCo.Rep.Type' and only contain some extra
--   details during typechecking.
--
--   These 'Var' names may either be global or local, see "GHC.Types.Var#globalvslocal"
--
-- #globalvslocal#
-- Global 'Id's and 'Var's are those that are imported or correspond
--    to a data constructor, primitive operation, or record selectors.
-- Local 'Id's and 'Var's are those bound within an expression
--    (e.g. by a lambda) or at the top level of the module being compiled.

module GHC.Types.Var (
        -- * The main data type and synonyms
        Var, CoVar, Id, NcId, DictId, DFunId, EvVar, EqVar, EvId, IpId, JoinId,
        TyVar, TcTyVar, TypeVar, KindVar, TKVar, TyCoVar,

        -- * In and Out variants
        InVar,  InCoVar,  InId,  InTyVar,
        OutVar, OutCoVar, OutId, OutTyVar,

        -- ** Taking 'Var's apart
        varName, varUnique, varType,
        varMultMaybe, idMult,

        -- ** Modifying 'Var's
        setVarName, setVarUnique, setVarType,
        updateVarType, updateVarTypeM,

        -- ** Constructing, taking apart, modifying 'Id's
        mkGlobalVar, mkLocalVar, mkExportedLocalVar, mkCoVar,
        idInfo, idDetails,
        lazySetIdInfo, setIdDetails, globaliseId,
        setIdExported, setIdNotExported, setIdMult,
        updateIdTypeButNotMult,
        updateIdTypeAndMult, updateIdTypeAndMultM,

        -- ** Predicates
        isId, isTyVar, isTcTyVar,
        isLocalVar, isLocalId, isLocalId_maybe, isCoVar, isNonCoVarId, isTyCoVar,
        isGlobalId, isExportedId,
        mustHaveLocalBinding,

        -- * ForAllTyFlags
        ForAllTyFlag(Invisible,Required,Specified,Inferred),
        Specificity(..),
        isVisibleForAllTyFlag, isInvisibleForAllTyFlag, isInferredForAllTyFlag,
        isSpecifiedForAllTyFlag,
        coreTyLamForAllTyFlag,

        -- * FunTyFlag
        FunTyFlag(..), isVisibleFunArg, isInvisibleFunArg, isFUNArg,
        mkFunTyFlag, visArg, invisArg,
        visArgTypeLike, visArgConstraintLike,
        invisArgTypeLike, invisArgConstraintLike,
        funTyFlagArgTypeOrConstraint, funTyFlagResultTypeOrConstraint,
        TypeOrConstraint(..),  -- Re-export this: it's an argument of FunTyFlag

        -- * PiTyBinder
        PiTyBinder(..), PiTyVarBinder,
        isInvisiblePiTyBinder, isInvisibleAnonPiTyBinder,
        isVisiblePiTyBinder,
        isTyBinder, isNamedPiTyBinder, isAnonPiTyBinder,
        namedPiTyBinder_maybe, anonPiTyBinderType_maybe, piTyBinderType,

        -- * TyVar's
        VarBndr(..), ForAllTyBinder, TyVarBinder,
        InvisTyBinder, InvisTVBinder, ReqTyBinder, ReqTVBinder,
        binderVar, binderVars, binderFlag, binderFlags, binderType,
        mkForAllTyBinder, mkForAllTyBinders,
        mkTyVarBinder, mkTyVarBinders,
        isVisibleForAllTyBinder, isInvisibleForAllTyBinder, isTyVarBinder,
        tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders,
        mapVarBndr, mapVarBndrs,

        -- ** ExportFlag
        ExportFlag(..),

        -- ** Constructing TyVar's
        mkTyVar, mkTcTyVar,

        -- ** Taking 'TyVar's apart
        tyVarName, tyVarKind, tcTyVarDetails, setTcTyVarDetails,

        -- ** Modifying 'TyVar's
        setTyVarName, setTyVarUnique, setTyVarKind, updateTyVarKind,
        updateTyVarKindM,

        nonDetCmpVar
        ) where

import GHC.Prelude

import {-# SOURCE #-}   GHC.Core.TyCo.Rep( Type, Kind, Mult, Scaled, scaledThing )
import {-# SOURCE #-}   GHC.Core.TyCo.Ppr( pprKind )
import {-# SOURCE #-}   GHC.Tc.Utils.TcType( TcTyVarDetails, pprTcTyVarDetails, vanillaSkolemTvUnk )
import {-# SOURCE #-}   GHC.Types.Id.Info( IdDetails, IdInfo, coVarDetails, isCoVarDetails,
                                           vanillaIdInfo, pprIdDetails )
import {-# SOURCE #-}   GHC.Builtin.Types ( manyDataConTy )
import GHC.Types.Name hiding (varName)
import GHC.Types.Unique ( Uniquable, Unique, getKey, getUnique
                        , nonDetCmpUnique )
import GHC.Types.Basic( TypeOrConstraint(..) )
import GHC.Utils.Misc
import GHC.Utils.Binary
import GHC.Utils.Outputable
import GHC.Utils.Panic

import GHC.Hs.Specificity ()
import Language.Haskell.Syntax.Specificity

import Data.Data

{-
************************************************************************
*                                                                      *
                     Synonyms
*                                                                      *
************************************************************************
-- These synonyms are here and not in Id because otherwise we need a very
-- large number of SOURCE imports of "GHC.Types.Id" :-(
-}

-- | Identifier
type Id    = Var       -- A term-level identifier
                       --  predicate: isId

-- | Coercion Variable
type CoVar = Id        -- See Note [Evidence: EvIds and CoVars]
                       --   predicate: isCoVar

-- |
type NcId  = Id        -- A term-level (value) variable that is
                       -- /not/ an (unlifted) coercion
                       --    predicate: isNonCoVarId

-- | Type or kind Variable
type TyVar   = Var     -- Type *or* kind variable (historical)

-- | Type or Kind Variable
type TKVar   = Var     -- Type *or* kind variable (historical)

-- | Type variable that might be a metavariable
type TcTyVar = Var

-- | Type Variable
type TypeVar = Var     -- Definitely a type variable

-- | Kind Variable
type KindVar = Var     -- Definitely a kind variable
                       -- See Note [Kind and type variables]

-- See Note [Evidence: EvIds and CoVars]
-- | Evidence Identifier
type EvId   = Id        -- Term-level evidence: DictId, IpId, or EqVar

-- | Evidence Variable
type EvVar  = EvId      -- ...historical name for EvId

-- | Dictionary Function Identifier
type DFunId = Id        -- A dictionary function

-- | Dictionary Identifier
type DictId = EvId      -- A dictionary variable

-- | Implicit parameter Identifier
type IpId   = EvId      -- A term-level implicit parameter

-- | Equality Variable
type EqVar  = EvId      -- Boxed equality evidence
type JoinId = Id        -- A join variable

-- | Type or Coercion Variable
type TyCoVar = Id       -- Type, *or* coercion variable
                        --   predicate: isTyCoVar


{- Many passes apply a substitution, and it's very handy to have type
   synonyms to remind us whether or not the substitution has been applied -}

type InVar      = Var
type InTyVar    = TyVar
type InCoVar    = CoVar
type InId       = Id
type OutVar     = Var
type OutTyVar   = TyVar
type OutCoVar   = CoVar
type OutId      = Id



{- Note [Evidence: EvIds and CoVars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* An EvId (evidence Id) is a term-level evidence variable
  (dictionary, implicit parameter, or equality). Could be boxed or unboxed.

* DictId, IpId, and EqVar are synonyms when we know what kind of
  evidence we are talking about.  For example, an EqVar has type (t1 ~ t2).

* A CoVar is always an un-lifted coercion, of type (t1 ~# t2) or (t1 ~R# t2)

Note [Kind and type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before kind polymorphism, TyVar were used to mean type variables. Now
they are used to mean kind *or* type variables. KindVar is used when we
know for sure that it is a kind variable. In future, we might want to
go over the whole compiler code to use:
   - TKVar   to mean kind or type variables
   - TypeVar to mean         type variables only
   - KindVar to mean kind         variables


************************************************************************
*                                                                      *
\subsection{The main data type declarations}
*                                                                      *
************************************************************************


Every @Var@ has a @Unique@, to uniquify it and for fast comparison, a
@Type@, and an @IdInfo@ (non-essential info about it, e.g.,
strictness).  The essential info about different kinds of @Vars@ is
in its @VarDetails@.
-}

-- | Variable
--
-- Essentially a typed 'Name', that may also contain some additional information
-- about the 'Var' and its use sites.
data Var
  = TyVar {  -- Type and kind variables
             -- see Note [Kind and type variables]
        Id -> Name
varName    :: !Name,
        Id -> Unique
realUnique :: {-# UNPACK #-} !Unique,
                                     -- ^ Key for fast comparison
                                     -- Identical to the Unique in the name,
                                     -- cached here for speed
        Id -> Mult
varType    :: Kind           -- ^ The type or kind of the 'Var' in question
 }

  | TcTyVar {                           -- Used only during type inference
                                        -- Used for kind variables during
                                        -- inference, as well
        varName        :: !Name,
        realUnique     :: {-# UNPACK #-} !Unique,
        varType        :: Kind,
        Id -> TcTyVarDetails
tc_tv_details  :: TcTyVarDetails
  }

  | Id {
        varName    :: !Name,
        realUnique :: {-# UNPACK #-} !Unique,
        varType    :: Type,
        Id -> Mult
varMult    :: Mult,             -- See Note [Multiplicity of let binders]
        Id -> IdScope
idScope    :: IdScope,
        Id -> IdDetails
id_details :: IdDetails,        -- Stable, doesn't change
        Id -> IdInfo
id_info    :: IdInfo }          -- Unstable, updated by simplifier

-- | Identifier Scope
data IdScope    -- See Note [GlobalId/LocalId]
  = GlobalId
  | LocalId ExportFlag

data ExportFlag   -- See Note [ExportFlag on binders]
  = NotExported   -- ^ Not exported: may be discarded as dead code.
  | Exported      -- ^ Exported: kept alive

{- Note [ExportFlag on binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
An ExportFlag of "Exported" on a top-level binder says "keep this
binding alive; do not drop it as dead code".  This transitively
keeps alive all the other top-level bindings that this binding refers
to.  This property is persisted all the way down the pipeline, so that
the binding will be compiled all the way to object code, and its
symbols will appear in the linker symbol table.

However, note that this use of "exported" is quite different to the
export list on a Haskell module.  Setting the ExportFlag on an Id does
/not/ mean that if you import the module (in Haskell source code) you
will see this Id.  Of course, things that appear in the export list
of the source Haskell module do indeed have their ExportFlag set.
But many other things, such as dictionary functions, are kept alive
by having their ExportFlag set, even though they are not exported
in the source-code sense.

We should probably use a different term for ExportFlag, like
KeepAlive.

Note [GlobalId/LocalId]
~~~~~~~~~~~~~~~~~~~~~~~
A GlobalId is
  * always a constant (top-level)
  * imported, or data constructor, or primop, or record selector
  * has a Unique that is globally unique across the whole
    GHC invocation (a single invocation may compile multiple modules)
  * never treated as a candidate by the free-variable finder;
        it's a constant!

A LocalId is
  * bound within an expression (lambda, case, local let(rec))
  * or defined at top level in the module being compiled
  * always treated as a candidate by the free-variable finder

In the output of CoreTidy, top level Ids are all GlobalIds, which are then
serialised into interface files. Do note however that CorePrep may introduce new
LocalIds for local floats (even at the top level). These will be visible in STG
and end up in generated code.

Note [Multiplicity of let binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Core, let-binders' multiplicity is always completely determined by syntax:
a recursive let will always have multiplicity Many (it's a prerequisite for
being recursive), and non-recursive let doesn't have a conventional multiplicity,
instead they act, for the purpose of multiplicity, as an alias for their
right-hand side.

Therefore, the `varMult` field of identifier is only used by binders in lambda
and case expressions. In a let expression the `varMult` field holds an
arbitrary value which will (and must!) be ignored.
-}

instance Outputable Var where
  ppr :: Id -> SDoc
ppr Id
var = SDoc -> (PprStyle -> SDoc) -> SDoc
forall doc. IsOutput doc => doc -> (PprStyle -> SDoc) -> doc
docWithStyle SDoc
ppr_code PprStyle -> SDoc
ppr_normal
    where
      -- don't display debug info with Code style (#25255)
      ppr_code :: SDoc
ppr_code = Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Name
varName Id
var)
      ppr_normal :: PprStyle -> SDoc
ppr_normal PprStyle
sty = (SDocContext -> Bool) -> (Bool -> SDoc) -> SDoc
forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
sdocOption SDocContext -> Bool
sdocSuppressVarKinds ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \Bool
supp_var_kinds ->
            (Bool -> SDoc) -> SDoc
forall doc. IsOutput doc => (Bool -> doc) -> doc
getPprDebug ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \Bool
debug ->
            let
              ppr_var :: SDoc
ppr_var = case Id
var of
                  (TyVar {})
                     | Bool
debug
                     -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
brackets (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tv")

                  (TcTyVar {tc_tv_details :: Id -> TcTyVarDetails
tc_tv_details = TcTyVarDetails
d})
                     | PprStyle -> Bool
dumpStyle PprStyle
sty Bool -> Bool -> Bool
|| Bool
debug
                     -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
brackets (TcTyVarDetails -> SDoc
pprTcTyVarDetails TcTyVarDetails
d)

                  (Id { idScope :: Id -> IdScope
idScope = IdScope
s, id_details :: Id -> IdDetails
id_details = IdDetails
d })
                     | Bool
debug
                     -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
brackets (IdScope -> SDoc
ppr_id_scope IdScope
s SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> IdDetails -> SDoc
pprIdDetails IdDetails
d)

                  Id
_  -> SDoc
forall doc. IsOutput doc => doc
empty
            in if
               |  Bool
debug Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
supp_var_kinds)
                 -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Name
varName Id
var) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe Mult -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Maybe Mult
varMultMaybe Id
var)
                                              SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
ppr_var SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>
                          SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Mult -> SDoc
pprKind (Id -> Mult
tyVarKind Id
var))
               |  Bool
otherwise
                 -> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Name
varName Id
var) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
ppr_var

ppr_id_scope :: IdScope -> SDoc
ppr_id_scope :: IdScope -> SDoc
ppr_id_scope IdScope
GlobalId              = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"gid"
ppr_id_scope (LocalId ExportFlag
Exported)    = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"lidx"
ppr_id_scope (LocalId ExportFlag
NotExported) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"lid"

instance NamedThing Var where
  getName :: Id -> Name
getName = Id -> Name
varName

instance Uniquable Var where
  getUnique :: Id -> Unique
getUnique = Id -> Unique
varUnique

instance Eq Var where
    Id
a == :: Id -> Id -> Bool
== Id
b = Id -> Unique
realUnique Id
a Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Id -> Unique
realUnique Id
b

instance Ord Var where
    Id
a <= :: Id -> Id -> Bool
<= Id
b = Unique -> Word64
getKey (Id -> Unique
realUnique Id
a) Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Unique -> Word64
getKey (Id -> Unique
realUnique Id
b)
    Id
a < :: Id -> Id -> Bool
<  Id
b = Unique -> Word64
getKey (Id -> Unique
realUnique Id
a) Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<  Unique -> Word64
getKey (Id -> Unique
realUnique Id
b)
    Id
a >= :: Id -> Id -> Bool
>= Id
b = Unique -> Word64
getKey (Id -> Unique
realUnique Id
a) Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Unique -> Word64
getKey (Id -> Unique
realUnique Id
b)
    Id
a > :: Id -> Id -> Bool
>  Id
b = Unique -> Word64
getKey (Id -> Unique
realUnique Id
a) Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>  Unique -> Word64
getKey (Id -> Unique
realUnique Id
b)
    Id
a compare :: Id -> Id -> Ordering
`compare` Id
b = Id
a Id -> Id -> Ordering
`nonDetCmpVar` Id
b

-- | Compare Vars by their Uniques.
-- This is what Ord Var does, provided here to make it explicit at the
-- call-site that it can introduce non-determinism.
-- See Note [Unique Determinism]
nonDetCmpVar :: Var -> Var -> Ordering
nonDetCmpVar :: Id -> Id -> Ordering
nonDetCmpVar Id
a Id
b = Id -> Unique
varUnique Id
a Unique -> Unique -> Ordering
`nonDetCmpUnique` Id -> Unique
varUnique Id
b

instance Data Var where
  -- don't traverse?
  toConstr :: Id -> Constr
toConstr Id
_   = String -> Constr
abstractConstr String
"Var"
  gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Id
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_  = String -> Constr -> c Id
forall a. HasCallStack => String -> a
error String
"gunfold"
  dataTypeOf :: Id -> DataType
dataTypeOf Id
_ = String -> DataType
mkNoRepType String
"Var"

instance HasOccName Var where
  occName :: Id -> OccName
occName = Name -> OccName
nameOccName (Name -> OccName) -> (Id -> Name) -> Id -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Name
varName

varUnique :: Var -> Unique
varUnique :: Id -> Unique
varUnique Id
var = Id -> Unique
realUnique Id
var

varMultMaybe :: Id -> Maybe Mult
varMultMaybe :: Id -> Maybe Mult
varMultMaybe (Id { varMult :: Id -> Mult
varMult = Mult
mult }) = Mult -> Maybe Mult
forall a. a -> Maybe a
Just Mult
mult
varMultMaybe Id
_ = Maybe Mult
forall a. Maybe a
Nothing

idMult :: HasDebugCallStack => Id -> Mult
idMult :: HasDebugCallStack => Id -> Mult
idMult (Id { varMult :: Id -> Mult
varMult = Mult
mult }) = Mult
mult
idMult Id
non_id                  = String -> SDoc -> Mult
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"idMult" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
non_id)

setVarUnique :: Var -> Unique -> Var
setVarUnique :: Id -> Unique -> Id
setVarUnique Id
var Unique
uniq
  = Id
var { realUnique = uniq,
          varName = setNameUnique (varName var) uniq }

setVarName :: Var -> Name -> Var
setVarName :: Id -> Name -> Id
setVarName Id
var Name
new_name
  = Id
var { realUnique = getUnique new_name,
          varName = new_name }

setVarType :: Var -> Type -> Var
setVarType :: Id -> Mult -> Id
setVarType Id
id Mult
ty = Id
id { varType = ty }

-- | Update a 'Var's type. Does not update the /multiplicity/
-- stored in an 'Id', if any. Because of the possibility for
-- abuse, ASSERTs that there is no multiplicity to update.
updateVarType :: (Type -> Type) -> Var -> Var
updateVarType :: (Mult -> Mult) -> Id -> Id
updateVarType Mult -> Mult
upd Id
var
  = case Id
var of
      Id { id_details :: Id -> IdDetails
id_details = IdDetails
details } -> Bool -> Id -> Id
forall a. HasCallStack => Bool -> a -> a
assert (IdDetails -> Bool
isCoVarDetails IdDetails
details) (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$
                                     Id
result
      Id
_ -> Id
result
  where
    result :: Id
result = Id
var { varType = upd (varType var) }

-- | Update a 'Var's type monadically. Does not update the /multiplicity/
-- stored in an 'Id', if any. Because of the possibility for
-- abuse, ASSERTs that there is no multiplicity to update.
updateVarTypeM :: Monad m => (Type -> m Type) -> Var -> m Var
updateVarTypeM :: forall (m :: * -> *). Monad m => (Mult -> m Mult) -> Id -> m Id
updateVarTypeM Mult -> m Mult
upd Id
var
  = case Id
var of
      Id { id_details :: Id -> IdDetails
id_details = IdDetails
details } -> Bool -> m Id -> m Id
forall a. HasCallStack => Bool -> a -> a
assert (IdDetails -> Bool
isCoVarDetails IdDetails
details) (m Id -> m Id) -> m Id -> m Id
forall a b. (a -> b) -> a -> b
$
                                     m Id
result
      Id
_ -> m Id
result
  where
    result :: m Id
result = do { ty' <- Mult -> m Mult
upd (Id -> Mult
varType Id
var)
                ; return (var { varType = ty' }) }

{- *********************************************************************
*                                                                      *
*                   FunTyFlag
*                                                                      *
********************************************************************* -}

-- | The non-dependent version of 'ForAllTyFlag'.
-- See Note [FunTyFlag]
-- Appears here partly so that it's together with its friends ForAllTyFlag
-- and ForallVisFlag, but also because it is used in IfaceType, rather
-- early in the compilation chain
data FunTyFlag
  = FTF_T_T           -- (->)  Type -> Type
  | FTF_T_C           -- (-=>) Type -> Constraint
  | FTF_C_T           -- (=>)  Constraint -> Type
  | FTF_C_C           -- (==>) Constraint -> Constraint
  deriving (FunTyFlag -> FunTyFlag -> Bool
(FunTyFlag -> FunTyFlag -> Bool)
-> (FunTyFlag -> FunTyFlag -> Bool) -> Eq FunTyFlag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FunTyFlag -> FunTyFlag -> Bool
== :: FunTyFlag -> FunTyFlag -> Bool
$c/= :: FunTyFlag -> FunTyFlag -> Bool
/= :: FunTyFlag -> FunTyFlag -> Bool
Eq, Eq FunTyFlag
Eq FunTyFlag =>
(FunTyFlag -> FunTyFlag -> Ordering)
-> (FunTyFlag -> FunTyFlag -> Bool)
-> (FunTyFlag -> FunTyFlag -> Bool)
-> (FunTyFlag -> FunTyFlag -> Bool)
-> (FunTyFlag -> FunTyFlag -> Bool)
-> (FunTyFlag -> FunTyFlag -> FunTyFlag)
-> (FunTyFlag -> FunTyFlag -> FunTyFlag)
-> Ord FunTyFlag
FunTyFlag -> FunTyFlag -> Bool
FunTyFlag -> FunTyFlag -> Ordering
FunTyFlag -> FunTyFlag -> FunTyFlag
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FunTyFlag -> FunTyFlag -> Ordering
compare :: FunTyFlag -> FunTyFlag -> Ordering
$c< :: FunTyFlag -> FunTyFlag -> Bool
< :: FunTyFlag -> FunTyFlag -> Bool
$c<= :: FunTyFlag -> FunTyFlag -> Bool
<= :: FunTyFlag -> FunTyFlag -> Bool
$c> :: FunTyFlag -> FunTyFlag -> Bool
> :: FunTyFlag -> FunTyFlag -> Bool
$c>= :: FunTyFlag -> FunTyFlag -> Bool
>= :: FunTyFlag -> FunTyFlag -> Bool
$cmax :: FunTyFlag -> FunTyFlag -> FunTyFlag
max :: FunTyFlag -> FunTyFlag -> FunTyFlag
$cmin :: FunTyFlag -> FunTyFlag -> FunTyFlag
min :: FunTyFlag -> FunTyFlag -> FunTyFlag
Ord, Typeable FunTyFlag
Typeable FunTyFlag =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FunTyFlag -> c FunTyFlag)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FunTyFlag)
-> (FunTyFlag -> Constr)
-> (FunTyFlag -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FunTyFlag))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunTyFlag))
-> ((forall b. Data b => b -> b) -> FunTyFlag -> FunTyFlag)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r)
-> (forall u. (forall d. Data d => d -> u) -> FunTyFlag -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> FunTyFlag -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag)
-> Data FunTyFlag
FunTyFlag -> Constr
FunTyFlag -> DataType
(forall b. Data b => b -> b) -> FunTyFlag -> FunTyFlag
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) -> FunTyFlag -> u
forall u. (forall d. Data d => d -> u) -> FunTyFlag -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunTyFlag
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunTyFlag -> c FunTyFlag
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunTyFlag)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunTyFlag)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunTyFlag -> c FunTyFlag
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunTyFlag -> c FunTyFlag
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunTyFlag
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunTyFlag
$ctoConstr :: FunTyFlag -> Constr
toConstr :: FunTyFlag -> Constr
$cdataTypeOf :: FunTyFlag -> DataType
dataTypeOf :: FunTyFlag -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunTyFlag)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunTyFlag)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunTyFlag)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunTyFlag)
$cgmapT :: (forall b. Data b => b -> b) -> FunTyFlag -> FunTyFlag
gmapT :: (forall b. Data b => b -> b) -> FunTyFlag -> FunTyFlag
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunTyFlag -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FunTyFlag -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> FunTyFlag -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunTyFlag -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunTyFlag -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunTyFlag -> m FunTyFlag
Data)

instance Outputable FunTyFlag where
  ppr :: FunTyFlag -> SDoc
ppr FunTyFlag
FTF_T_T  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"[->]"
  ppr FunTyFlag
FTF_T_C  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"[-=>]"
  ppr FunTyFlag
FTF_C_T  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"[=>]"
  ppr FunTyFlag
FTF_C_C  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"[==>]"

instance Binary FunTyFlag where
  put_ :: WriteBinHandle -> FunTyFlag -> IO ()
put_ WriteBinHandle
bh FunTyFlag
FTF_T_T = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
0
  put_ WriteBinHandle
bh FunTyFlag
FTF_T_C = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
1
  put_ WriteBinHandle
bh FunTyFlag
FTF_C_T = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
2
  put_ WriteBinHandle
bh FunTyFlag
FTF_C_C = WriteBinHandle -> Word8 -> IO ()
putByte WriteBinHandle
bh Word8
3

  get :: ReadBinHandle -> IO FunTyFlag
get ReadBinHandle
bh = do
    h <- ReadBinHandle -> IO Word8
getByte ReadBinHandle
bh
    case h of
      Word8
0 -> FunTyFlag -> IO FunTyFlag
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FunTyFlag
FTF_T_T
      Word8
1 -> FunTyFlag -> IO FunTyFlag
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FunTyFlag
FTF_T_C
      Word8
2 -> FunTyFlag -> IO FunTyFlag
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FunTyFlag
FTF_C_T
      Word8
_ -> FunTyFlag -> IO FunTyFlag
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FunTyFlag
FTF_C_C

mkFunTyFlag :: TypeOrConstraint -> TypeOrConstraint -> FunTyFlag
mkFunTyFlag :: TypeOrConstraint -> TypeOrConstraint -> FunTyFlag
mkFunTyFlag TypeOrConstraint
TypeLike       TypeOrConstraint
torc = TypeOrConstraint -> FunTyFlag
visArg TypeOrConstraint
torc
mkFunTyFlag TypeOrConstraint
ConstraintLike TypeOrConstraint
torc = TypeOrConstraint -> FunTyFlag
invisArg TypeOrConstraint
torc

visArg :: TypeOrConstraint -> FunTyFlag
visArg :: TypeOrConstraint -> FunTyFlag
visArg TypeOrConstraint
TypeLike       = FunTyFlag
FTF_T_T
visArg TypeOrConstraint
ConstraintLike = FunTyFlag
FTF_T_C

visArgTypeLike :: FunTyFlag
visArgTypeLike :: FunTyFlag
visArgTypeLike = FunTyFlag
FTF_T_T

visArgConstraintLike :: FunTyFlag
visArgConstraintLike :: FunTyFlag
visArgConstraintLike = FunTyFlag
FTF_T_C

invisArg :: TypeOrConstraint -> FunTyFlag
invisArg :: TypeOrConstraint -> FunTyFlag
invisArg TypeOrConstraint
TypeLike       = FunTyFlag
FTF_C_T
invisArg TypeOrConstraint
ConstraintLike = FunTyFlag
FTF_C_C

invisArgTypeLike :: FunTyFlag
invisArgTypeLike :: FunTyFlag
invisArgTypeLike = FunTyFlag
FTF_C_T

invisArgConstraintLike :: FunTyFlag
invisArgConstraintLike :: FunTyFlag
invisArgConstraintLike = FunTyFlag
FTF_C_C

isInvisibleFunArg :: FunTyFlag -> Bool
isInvisibleFunArg :: FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af = Bool -> Bool
not (FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af)

isVisibleFunArg :: FunTyFlag -> Bool
isVisibleFunArg :: FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
FTF_T_T = Bool
True
isVisibleFunArg FunTyFlag
FTF_T_C = Bool
True
isVisibleFunArg FunTyFlag
_       = Bool
False

isFUNArg :: FunTyFlag -> Bool
-- This one, FUN, or (->), has an extra multiplicity argument
isFUNArg :: FunTyFlag -> Bool
isFUNArg FunTyFlag
FTF_T_T = Bool
True
isFUNArg FunTyFlag
_       = Bool
False

funTyFlagArgTypeOrConstraint :: FunTyFlag -> TypeOrConstraint
-- Whether it /takes/ a type or a constraint
funTyFlagArgTypeOrConstraint :: FunTyFlag -> TypeOrConstraint
funTyFlagArgTypeOrConstraint FunTyFlag
FTF_T_T = TypeOrConstraint
TypeLike
funTyFlagArgTypeOrConstraint FunTyFlag
FTF_T_C = TypeOrConstraint
TypeLike
funTyFlagArgTypeOrConstraint FunTyFlag
_       = TypeOrConstraint
ConstraintLike

funTyFlagResultTypeOrConstraint :: FunTyFlag -> TypeOrConstraint
-- Whether it /returns/ a type or a constraint
funTyFlagResultTypeOrConstraint :: FunTyFlag -> TypeOrConstraint
funTyFlagResultTypeOrConstraint FunTyFlag
FTF_T_T = TypeOrConstraint
TypeLike
funTyFlagResultTypeOrConstraint FunTyFlag
FTF_C_T = TypeOrConstraint
TypeLike
funTyFlagResultTypeOrConstraint FunTyFlag
_       = TypeOrConstraint
ConstraintLike

{- Note [FunTyFlag]
~~~~~~~~~~~~~~~~~~~~~
FunTyFlag is used principally in the FunTy constructor of Type.
  FunTy FTF_T_T t1 t2   means   t1 -> t2
  FunTy FTF_C_T t1 t2   means   t1 => t2
  FunTy FTF_T_C t1 t2   means   t1 -=> t2
  FunTy FTF_C_C t1 t2   means   t1 ==> t2

However, the FunTyFlag in a FunTy is just redundant, cached
information.  In (FunTy { ft_af = af, ft_arg = t1, ft_res = t2 })
  ---------------------------------------------
  (isPredTy t1)   (isPredTy ty)     FunTyFlag
  ---------------------------------------------
     False           False         FTF_T_T
     False           True          FTF_T_C
     True            False         FTF_C_T
     True            True          FTF_C_C
where isPredTy is defined in GHC.Core.Type, and sees if t1's
kind is Constraint.  See GHC.Core.Type.chooseFunTyFlag, and
GHC.Core.TyCo.Rep Note [Types for coercions, predicates, and evidence]

The term (Lam b e) donesn't carry an FunTyFlag; instead it uses
mkFunctionType when we want to get its types; see mkLamType.  This is
just an engineering choice; we could cache here too if we wanted.

Why bother with all this? After all, we are in Core, where (=>) and
(->) behave the same.  We maintain this distinction throughout Core so
that we can cheaply and conveniently determine
* How to print a type
* How to split up a type: tcSplitSigmaTy
* How to specialise it (over type classes; GHC.Core.Opt.Specialise)

For the specialisation point, consider
(\ (d :: Ord a). blah).  We want to give it type
           (Ord a => blah_ty)
with a fat arrow; that is, using mkInvisFunTy, not mkVisFunTy.
Why?  Because the /specialiser/ treats dictionary arguments specially.
Suppose we do w/w on 'foo', thus (#11272, #6056)
   foo :: Ord a => Int -> blah
   foo a d x = case x of I# x' -> $wfoo @a d x'

   $wfoo :: Ord a => Int# -> blah

Now, at a call we see (foo @Int dOrdInt).  The specialiser will
specialise this to $sfoo, where
   $sfoo :: Int -> blah
   $sfoo x = case x of I# x' -> $wfoo @Int dOrdInt x'

Now we /must/ also specialise $wfoo!  But it wasn't user-written,
and has a type built with mkLamTypes.

Conclusion: the easiest thing is to make mkLamType build
            (c => ty)
when the argument is a predicate type.  See GHC.Core.TyCo.Rep
Note [Types for coercions, predicates, and evidence]
-}

{- *********************************************************************
*                                                                      *
*                   VarBndr, ForAllTyBinder
*                                                                      *
********************************************************************* -}

{- Note [The VarBndr type and its uses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
VarBndr is polymorphic in both var and visibility fields.
Currently there are nine different uses of 'VarBndr':

* Var.ForAllTyBinder = VarBndr TyCoVar ForAllTyFlag
  Binder of a forall-type; see ForAllTy in GHC.Core.TyCo.Rep

* Var.TyVarBinder = VarBndr TyVar ForAllTyFlag
  Subset of ForAllTyBinder when we are sure the binder is a TyVar

* Var.InvisTVBinder = VarBndr TyVar Specificity
  Specialised form of TyVarBinder, when ForAllTyFlag = Invisible s
  See GHC.Core.Type.splitForAllInvisTVBinders

* Var.ReqTVBinder = VarBndr TyVar ()
  Specialised form of TyVarBinder, when ForAllTyFlag = Required
  See GHC.Core.Type.splitForAllReqTVBinders
  This one is barely used

* TyCon.TyConBinder = VarBndr TyVar TyConBndrVis
  Binders of a TyCon; see TyCon in GHC.Core.TyCon

* IfaceType.IfaceForAllBndr     = VarBndr IfaceBndr ForAllTyFlag
* IfaceType.IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity
* IfaceType.IfaceTyConBinder    = VarBndr IfaceBndr TyConBndrVis
-}

data VarBndr var argf = Bndr var argf
  -- See Note [The VarBndr type and its uses]
  deriving( Typeable (VarBndr var argf)
Typeable (VarBndr var argf) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> VarBndr var argf
 -> c (VarBndr var argf))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (VarBndr var argf))
-> (VarBndr var argf -> Constr)
-> (VarBndr var argf -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (VarBndr var argf)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (VarBndr var argf)))
-> ((forall b. Data b => b -> b)
    -> VarBndr var argf -> VarBndr var argf)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> VarBndr var argf -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> VarBndr var argf -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> VarBndr var argf -> m (VarBndr var argf))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> VarBndr var argf -> m (VarBndr var argf))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> VarBndr var argf -> m (VarBndr var argf))
-> Data (VarBndr var argf)
VarBndr var argf -> Constr
VarBndr var argf -> DataType
(forall b. Data b => b -> b)
-> VarBndr var argf -> VarBndr var argf
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) -> VarBndr var argf -> u
forall u. (forall d. Data d => d -> u) -> VarBndr var argf -> [u]
forall var argf.
(Data var, Data argf) =>
Typeable (VarBndr var argf)
forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> Constr
forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> DataType
forall var argf.
(Data var, Data argf) =>
(forall b. Data b => b -> b)
-> VarBndr var argf -> VarBndr var argf
forall var argf u.
(Data var, Data argf) =>
Int -> (forall d. Data d => d -> u) -> VarBndr var argf -> u
forall var argf u.
(Data var, Data argf) =>
(forall d. Data d => d -> u) -> VarBndr var argf -> [u]
forall var argf r r'.
(Data var, Data argf) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
forall var argf r r'.
(Data var, Data argf) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
forall var argf (m :: * -> *).
(Data var, Data argf, Monad m) =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
forall var argf (m :: * -> *).
(Data var, Data argf, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
forall var argf (c :: * -> *).
(Data var, Data argf) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VarBndr var argf)
forall var argf (c :: * -> *).
(Data var, Data argf) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarBndr var argf -> c (VarBndr var argf)
forall var argf (t :: * -> *) (c :: * -> *).
(Data var, Data argf, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (VarBndr var argf))
forall var argf (t :: * -> * -> *) (c :: * -> *).
(Data var, Data argf, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VarBndr var argf))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VarBndr var argf)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarBndr var argf -> c (VarBndr var argf)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (VarBndr var argf))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VarBndr var argf))
$cgfoldl :: forall var argf (c :: * -> *).
(Data var, Data argf) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarBndr var argf -> c (VarBndr var argf)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarBndr var argf -> c (VarBndr var argf)
$cgunfold :: forall var argf (c :: * -> *).
(Data var, Data argf) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VarBndr var argf)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VarBndr var argf)
$ctoConstr :: forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> Constr
toConstr :: VarBndr var argf -> Constr
$cdataTypeOf :: forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> DataType
dataTypeOf :: VarBndr var argf -> DataType
$cdataCast1 :: forall var argf (t :: * -> *) (c :: * -> *).
(Data var, Data argf, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (VarBndr var argf))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (VarBndr var argf))
$cdataCast2 :: forall var argf (t :: * -> * -> *) (c :: * -> *).
(Data var, Data argf, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VarBndr var argf))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VarBndr var argf))
$cgmapT :: forall var argf.
(Data var, Data argf) =>
(forall b. Data b => b -> b)
-> VarBndr var argf -> VarBndr var argf
gmapT :: (forall b. Data b => b -> b)
-> VarBndr var argf -> VarBndr var argf
$cgmapQl :: forall var argf r r'.
(Data var, Data argf) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
$cgmapQr :: forall var argf r r'.
(Data var, Data argf) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
$cgmapQ :: forall var argf u.
(Data var, Data argf) =>
(forall d. Data d => d -> u) -> VarBndr var argf -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> VarBndr var argf -> [u]
$cgmapQi :: forall var argf u.
(Data var, Data argf) =>
Int -> (forall d. Data d => d -> u) -> VarBndr var argf -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> VarBndr var argf -> u
$cgmapM :: forall var argf (m :: * -> *).
(Data var, Data argf, Monad m) =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
$cgmapMp :: forall var argf (m :: * -> *).
(Data var, Data argf, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
$cgmapMo :: forall var argf (m :: * -> *).
(Data var, Data argf, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
Data, VarBndr var argf -> VarBndr var argf -> Bool
(VarBndr var argf -> VarBndr var argf -> Bool)
-> (VarBndr var argf -> VarBndr var argf -> Bool)
-> Eq (VarBndr var argf)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall var argf.
(Eq var, Eq argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
$c== :: forall var argf.
(Eq var, Eq argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
== :: VarBndr var argf -> VarBndr var argf -> Bool
$c/= :: forall var argf.
(Eq var, Eq argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
/= :: VarBndr var argf -> VarBndr var argf -> Bool
Eq, Eq (VarBndr var argf)
Eq (VarBndr var argf) =>
(VarBndr var argf -> VarBndr var argf -> Ordering)
-> (VarBndr var argf -> VarBndr var argf -> Bool)
-> (VarBndr var argf -> VarBndr var argf -> Bool)
-> (VarBndr var argf -> VarBndr var argf -> Bool)
-> (VarBndr var argf -> VarBndr var argf -> Bool)
-> (VarBndr var argf -> VarBndr var argf -> VarBndr var argf)
-> (VarBndr var argf -> VarBndr var argf -> VarBndr var argf)
-> Ord (VarBndr var argf)
VarBndr var argf -> VarBndr var argf -> Bool
VarBndr var argf -> VarBndr var argf -> Ordering
VarBndr var argf -> VarBndr var argf -> VarBndr var argf
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall var argf. (Ord var, Ord argf) => Eq (VarBndr var argf)
forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> Ordering
forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> VarBndr var argf
$ccompare :: forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> Ordering
compare :: VarBndr var argf -> VarBndr var argf -> Ordering
$c< :: forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
< :: VarBndr var argf -> VarBndr var argf -> Bool
$c<= :: forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
<= :: VarBndr var argf -> VarBndr var argf -> Bool
$c> :: forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
> :: VarBndr var argf -> VarBndr var argf -> Bool
$c>= :: forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> Bool
>= :: VarBndr var argf -> VarBndr var argf -> Bool
$cmax :: forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> VarBndr var argf
max :: VarBndr var argf -> VarBndr var argf -> VarBndr var argf
$cmin :: forall var argf.
(Ord var, Ord argf) =>
VarBndr var argf -> VarBndr var argf -> VarBndr var argf
min :: VarBndr var argf -> VarBndr var argf -> VarBndr var argf
Ord)

-- | Variable Binder
--
-- A 'ForAllTyBinder' is the binder of a ForAllTy
-- It's convenient to define this synonym here rather its natural
-- home in "GHC.Core.TyCo.Rep", because it's used in GHC.Core.DataCon.hs-boot
--
-- A 'TyVarBinder' is a binder with only TyVar
type ForAllTyBinder = VarBndr TyCoVar ForAllTyFlag
type InvisTyBinder  = VarBndr TyCoVar Specificity
type ReqTyBinder    = VarBndr TyCoVar ()

type TyVarBinder    = VarBndr TyVar   ForAllTyFlag
type InvisTVBinder  = VarBndr TyVar   Specificity
type ReqTVBinder    = VarBndr TyVar   ()

tyVarSpecToBinders :: [VarBndr a Specificity] -> [VarBndr a ForAllTyFlag]
tyVarSpecToBinders :: forall a. [VarBndr a Specificity] -> [VarBndr a ForAllTyFlag]
tyVarSpecToBinders = (VarBndr a Specificity -> VarBndr a ForAllTyFlag)
-> [VarBndr a Specificity] -> [VarBndr a ForAllTyFlag]
forall a b. (a -> b) -> [a] -> [b]
map VarBndr a Specificity -> VarBndr a ForAllTyFlag
forall a. VarBndr a Specificity -> VarBndr a ForAllTyFlag
tyVarSpecToBinder

tyVarSpecToBinder :: VarBndr a Specificity -> VarBndr a ForAllTyFlag
tyVarSpecToBinder :: forall a. VarBndr a Specificity -> VarBndr a ForAllTyFlag
tyVarSpecToBinder (Bndr a
tv Specificity
vis) = a -> ForAllTyFlag -> VarBndr a ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr a
tv (Specificity -> ForAllTyFlag
Invisible Specificity
vis)

tyVarReqToBinders :: [VarBndr a ()] -> [VarBndr a ForAllTyFlag]
tyVarReqToBinders :: forall a. [VarBndr a ()] -> [VarBndr a ForAllTyFlag]
tyVarReqToBinders = (VarBndr a () -> VarBndr a ForAllTyFlag)
-> [VarBndr a ()] -> [VarBndr a ForAllTyFlag]
forall a b. (a -> b) -> [a] -> [b]
map VarBndr a () -> VarBndr a ForAllTyFlag
forall a. VarBndr a () -> VarBndr a ForAllTyFlag
tyVarReqToBinder

tyVarReqToBinder :: VarBndr a () -> VarBndr a ForAllTyFlag
tyVarReqToBinder :: forall a. VarBndr a () -> VarBndr a ForAllTyFlag
tyVarReqToBinder (Bndr a
tv ()
_) = a -> ForAllTyFlag -> VarBndr a ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr a
tv ForAllTyFlag
Required

isVisibleForAllTyBinder :: ForAllTyBinder -> Bool
isVisibleForAllTyBinder :: ForAllTyBinder -> Bool
isVisibleForAllTyBinder (Bndr Id
_ ForAllTyFlag
vis) = ForAllTyFlag -> Bool
isVisibleForAllTyFlag ForAllTyFlag
vis

isInvisibleForAllTyBinder :: ForAllTyBinder -> Bool
isInvisibleForAllTyBinder :: ForAllTyBinder -> Bool
isInvisibleForAllTyBinder (Bndr Id
_ ForAllTyFlag
vis) = ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
vis

binderVar :: VarBndr tv argf -> tv
binderVar :: forall tv argf. VarBndr tv argf -> tv
binderVar (Bndr tv
v argf
_) = tv
v

binderVars :: [VarBndr tv argf] -> [tv]
binderVars :: forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr tv argf]
tvbs = (VarBndr tv argf -> tv) -> [VarBndr tv argf] -> [tv]
forall a b. (a -> b) -> [a] -> [b]
map VarBndr tv argf -> tv
forall tv argf. VarBndr tv argf -> tv
binderVar [VarBndr tv argf]
tvbs

binderFlag :: VarBndr tv argf -> argf
binderFlag :: forall tv argf. VarBndr tv argf -> argf
binderFlag (Bndr tv
_ argf
argf) = argf
argf

binderFlags :: [VarBndr tv argf] -> [argf]
binderFlags :: forall tv argf. [VarBndr tv argf] -> [argf]
binderFlags [VarBndr tv argf]
tvbs = (VarBndr tv argf -> argf) -> [VarBndr tv argf] -> [argf]
forall a b. (a -> b) -> [a] -> [b]
map VarBndr tv argf -> argf
forall tv argf. VarBndr tv argf -> argf
binderFlag [VarBndr tv argf]
tvbs

binderType :: VarBndr TyCoVar argf -> Type
binderType :: forall argf. VarBndr Id argf -> Mult
binderType (Bndr Id
tv argf
_) = Id -> Mult
varType Id
tv

isTyVarBinder :: VarBndr TyCoVar vis -> Bool
isTyVarBinder :: forall vis. VarBndr Id vis -> Bool
isTyVarBinder (Bndr Id
tcv vis
_) = Id -> Bool
isTyVar Id
tcv

-- | Make a named binder
mkForAllTyBinder :: vis -> TyCoVar -> VarBndr TyCoVar vis
mkForAllTyBinder :: forall vis. vis -> Id -> VarBndr Id vis
mkForAllTyBinder vis
vis Id
var = Id -> vis -> VarBndr Id vis
forall var argf. var -> argf -> VarBndr var argf
Bndr Id
var vis
vis

-- | Make a named binder
-- 'var' should be a type variable
mkTyVarBinder :: vis -> TyVar -> VarBndr TyVar vis
mkTyVarBinder :: forall vis. vis -> Id -> VarBndr Id vis
mkTyVarBinder vis
vis Id
var
  = Bool -> VarBndr Id vis -> VarBndr Id vis
forall a. HasCallStack => Bool -> a -> a
assert (Id -> Bool
isTyVar Id
var) (VarBndr Id vis -> VarBndr Id vis)
-> VarBndr Id vis -> VarBndr Id vis
forall a b. (a -> b) -> a -> b
$
    Id -> vis -> VarBndr Id vis
forall var argf. var -> argf -> VarBndr var argf
Bndr Id
var vis
vis

-- | Make many named binders
mkForAllTyBinders :: vis -> [TyCoVar] -> [VarBndr TyCoVar vis]
mkForAllTyBinders :: forall vis. vis -> [Id] -> [VarBndr Id vis]
mkForAllTyBinders vis
vis = (Id -> VarBndr Id vis) -> [Id] -> [VarBndr Id vis]
forall a b. (a -> b) -> [a] -> [b]
map (vis -> Id -> VarBndr Id vis
forall vis. vis -> Id -> VarBndr Id vis
mkForAllTyBinder vis
vis)

-- | Make many named binders
-- Input vars should be type variables
mkTyVarBinders :: vis -> [TyVar] -> [VarBndr TyVar vis]
mkTyVarBinders :: forall vis. vis -> [Id] -> [VarBndr Id vis]
mkTyVarBinders vis
vis = (Id -> VarBndr Id vis) -> [Id] -> [VarBndr Id vis]
forall a b. (a -> b) -> [a] -> [b]
map (vis -> Id -> VarBndr Id vis
forall vis. vis -> Id -> VarBndr Id vis
mkTyVarBinder vis
vis)

mapVarBndr :: (var -> var') -> (VarBndr var flag) -> (VarBndr var' flag)
mapVarBndr :: forall var var' flag.
(var -> var') -> VarBndr var flag -> VarBndr var' flag
mapVarBndr var -> var'
f (Bndr var
v flag
fl) = var' -> flag -> VarBndr var' flag
forall var argf. var -> argf -> VarBndr var argf
Bndr (var -> var'
f var
v) flag
fl

mapVarBndrs :: (var -> var') -> [VarBndr var flag] -> [VarBndr var' flag]
mapVarBndrs :: forall var var' flag.
(var -> var') -> [VarBndr var flag] -> [VarBndr var' flag]
mapVarBndrs var -> var'
f = (VarBndr var flag -> VarBndr var' flag)
-> [VarBndr var flag] -> [VarBndr var' flag]
forall a b. (a -> b) -> [a] -> [b]
map ((var -> var') -> VarBndr var flag -> VarBndr var' flag
forall var var' flag.
(var -> var') -> VarBndr var flag -> VarBndr var' flag
mapVarBndr var -> var'
f)

instance Outputable tv => Outputable (VarBndr tv ForAllTyFlag) where
  ppr :: VarBndr tv ForAllTyFlag -> SDoc
ppr (Bndr tv
v ForAllTyFlag
Required)  = tv -> SDoc
forall a. Outputable a => a -> SDoc
ppr tv
v
  ppr (Bndr tv
v ForAllTyFlag
Specified) = Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'@' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> tv -> SDoc
forall a. Outputable a => a -> SDoc
ppr tv
v
  ppr (Bndr tv
v ForAllTyFlag
Inferred)  = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (tv -> SDoc
forall a. Outputable a => a -> SDoc
ppr tv
v)

instance Outputable tv => Outputable (VarBndr tv Specificity) where
  ppr :: VarBndr tv Specificity -> SDoc
ppr = VarBndr tv ForAllTyFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr (VarBndr tv ForAllTyFlag -> SDoc)
-> (VarBndr tv Specificity -> VarBndr tv ForAllTyFlag)
-> VarBndr tv Specificity
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarBndr tv Specificity -> VarBndr tv ForAllTyFlag
forall a. VarBndr a Specificity -> VarBndr a ForAllTyFlag
tyVarSpecToBinder

instance (Binary tv, Binary vis) => Binary (VarBndr tv vis) where
  put_ :: WriteBinHandle -> VarBndr tv vis -> IO ()
put_ WriteBinHandle
bh (Bndr tv
tv vis
vis) = do { WriteBinHandle -> tv -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
put_ WriteBinHandle
bh tv
tv; WriteBinHandle -> vis -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
put_ WriteBinHandle
bh vis
vis }

  get :: ReadBinHandle -> IO (VarBndr tv vis)
get ReadBinHandle
bh = do { tv <- ReadBinHandle -> IO tv
forall a. Binary a => ReadBinHandle -> IO a
get ReadBinHandle
bh; vis <- get bh; return (Bndr tv vis) }

instance NamedThing tv => NamedThing (VarBndr tv flag) where
  getName :: VarBndr tv flag -> Name
getName (Bndr tv
tv flag
_) = tv -> Name
forall a. NamedThing a => a -> Name
getName tv
tv


{- **********************************************************************
*                                                                       *
                  PiTyBinder
*                                                                       *
********************************************************************** -}

-- | A 'PiTyBinder' represents an argument to a function. PiTyBinders can be
-- dependent ('Named') or nondependent ('Anon'). They may also be visible or
-- not. See Note [PiTyBinders]
data PiTyBinder
  = Named ForAllTyBinder          -- A type-lambda binder, with a ForAllTyFlag
  | Anon (Scaled Type) FunTyFlag  -- A term-lambda binder. Type here can be CoercionTy.
                                  -- The arrow is described by the FunTyFlag
  deriving Typeable PiTyBinder
Typeable PiTyBinder =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PiTyBinder -> c PiTyBinder)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PiTyBinder)
-> (PiTyBinder -> Constr)
-> (PiTyBinder -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PiTyBinder))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PiTyBinder))
-> ((forall b. Data b => b -> b) -> PiTyBinder -> PiTyBinder)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r)
-> (forall u. (forall d. Data d => d -> u) -> PiTyBinder -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PiTyBinder -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder)
-> Data PiTyBinder
PiTyBinder -> Constr
PiTyBinder -> DataType
(forall b. Data b => b -> b) -> PiTyBinder -> PiTyBinder
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) -> PiTyBinder -> u
forall u. (forall d. Data d => d -> u) -> PiTyBinder -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PiTyBinder
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PiTyBinder -> c PiTyBinder
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PiTyBinder)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PiTyBinder)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PiTyBinder -> c PiTyBinder
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PiTyBinder -> c PiTyBinder
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PiTyBinder
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PiTyBinder
$ctoConstr :: PiTyBinder -> Constr
toConstr :: PiTyBinder -> Constr
$cdataTypeOf :: PiTyBinder -> DataType
dataTypeOf :: PiTyBinder -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PiTyBinder)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PiTyBinder)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PiTyBinder)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PiTyBinder)
$cgmapT :: (forall b. Data b => b -> b) -> PiTyBinder -> PiTyBinder
gmapT :: (forall b. Data b => b -> b) -> PiTyBinder -> PiTyBinder
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PiTyBinder -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PiTyBinder -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PiTyBinder -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PiTyBinder -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
Data

instance Outputable PiTyBinder where
  ppr :: PiTyBinder -> SDoc
ppr (Anon Scaled Mult
ty FunTyFlag
af) = FunTyFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr FunTyFlag
af SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Scaled Mult -> SDoc
forall a. Outputable a => a -> SDoc
ppr Scaled Mult
ty
  ppr (Named (Bndr Id
v ForAllTyFlag
Required))  = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v
  ppr (Named (Bndr Id
v ForAllTyFlag
Specified)) = Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'@' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v
  ppr (Named (Bndr Id
v ForAllTyFlag
Inferred))  = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v)

-- | 'PiTyVarBinder' is like 'PiTyBinder', but there can only be 'TyVar'
-- in the 'Named' field.
type PiTyVarBinder = PiTyBinder

-- | Does this binder bind an invisible argument?
isInvisiblePiTyBinder :: PiTyBinder -> Bool
isInvisiblePiTyBinder :: PiTyBinder -> Bool
isInvisiblePiTyBinder (Named (Bndr Id
_ ForAllTyFlag
vis)) = ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
vis
isInvisiblePiTyBinder (Anon Scaled Mult
_ FunTyFlag
af)          = FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af

isInvisibleAnonPiTyBinder :: PiTyBinder -> Bool
isInvisibleAnonPiTyBinder :: PiTyBinder -> Bool
isInvisibleAnonPiTyBinder (Named {})  = Bool
False
isInvisibleAnonPiTyBinder (Anon Scaled Mult
_ FunTyFlag
af) = FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af

-- | Does this binder bind a visible argument?
isVisiblePiTyBinder :: PiTyBinder -> Bool
isVisiblePiTyBinder :: PiTyBinder -> Bool
isVisiblePiTyBinder = Bool -> Bool
not (Bool -> Bool) -> (PiTyBinder -> Bool) -> PiTyBinder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PiTyBinder -> Bool
isInvisiblePiTyBinder

isNamedPiTyBinder :: PiTyBinder -> Bool
isNamedPiTyBinder :: PiTyBinder -> Bool
isNamedPiTyBinder (Named {}) = Bool
True
isNamedPiTyBinder (Anon {})  = Bool
False

namedPiTyBinder_maybe :: PiTyBinder -> Maybe TyCoVar
namedPiTyBinder_maybe :: PiTyBinder -> Maybe Id
namedPiTyBinder_maybe (Named ForAllTyBinder
tv) = Id -> Maybe Id
forall a. a -> Maybe a
Just (Id -> Maybe Id) -> Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ ForAllTyBinder -> Id
forall tv argf. VarBndr tv argf -> tv
binderVar ForAllTyBinder
tv
namedPiTyBinder_maybe PiTyBinder
_          = Maybe Id
forall a. Maybe a
Nothing

-- | Does this binder bind a variable that is /not/ erased? Returns
-- 'True' for anonymous binders.
isAnonPiTyBinder :: PiTyBinder -> Bool
isAnonPiTyBinder :: PiTyBinder -> Bool
isAnonPiTyBinder (Named {}) = Bool
False
isAnonPiTyBinder (Anon {})  = Bool
True

-- | Extract a relevant type, if there is one.
anonPiTyBinderType_maybe :: PiTyBinder -> Maybe Type
anonPiTyBinderType_maybe :: PiTyBinder -> Maybe Mult
anonPiTyBinderType_maybe (Named {})  = Maybe Mult
forall a. Maybe a
Nothing
anonPiTyBinderType_maybe (Anon Scaled Mult
ty FunTyFlag
_) = Mult -> Maybe Mult
forall a. a -> Maybe a
Just (Scaled Mult -> Mult
forall a. Scaled a -> a
scaledThing Scaled Mult
ty)

-- | If its a named binder, is the binder a tyvar?
-- Returns True for nondependent binder.
-- This check that we're really returning a *Ty*Binder (as opposed to a
-- coercion binder). That way, if/when we allow coercion quantification
-- in more places, we'll know we missed updating some function.
isTyBinder :: PiTyBinder -> Bool
isTyBinder :: PiTyBinder -> Bool
isTyBinder (Named ForAllTyBinder
bnd) = ForAllTyBinder -> Bool
forall vis. VarBndr Id vis -> Bool
isTyVarBinder ForAllTyBinder
bnd
isTyBinder PiTyBinder
_ = Bool
True

piTyBinderType :: PiTyBinder -> Type
piTyBinderType :: PiTyBinder -> Mult
piTyBinderType (Named (Bndr Id
tv ForAllTyFlag
_)) = Id -> Mult
varType Id
tv
piTyBinderType (Anon Scaled Mult
ty FunTyFlag
_)         = Scaled Mult -> Mult
forall a. Scaled a -> a
scaledThing Scaled Mult
ty

{- Note [PiTyBinders]
~~~~~~~~~~~~~~~~~~~
But a type like
   forall a. Maybe a -> forall b. (a,b) -> b

can be decomposed to a telescope of type [PiTyBinder], using splitPiTys.
That function splits off all leading foralls and arrows, giving
   ([Named a, Anon (Maybe a), Named b, Anon (a,b)], b)

A PiTyBinder represents the type of binders -- that is, the type of an
argument to a Pi-type. GHC Core currently supports two different
Pi-types:

 * Anon ty1 fun_flag: a non-dependent function type,
   written with ->, e.g. ty1 -> ty2
   represented as FunTy ty1 ty2. These are
   lifted to Coercions with the corresponding FunCo.

 * Named (Var tv forall_flag)
    A dependent compile-time-only polytype,
   written with forall, e.g.  forall (a:*). ty
   represented as ForAllTy (Bndr a v) ty

Both forms of Pi-types classify terms/types that take an argument. In other
words, if `x` is either a function or a polytype, `x arg` makes sense
(for an appropriate `arg`).

Wrinkles

* The Anon constructor of PiTyBinder contains a FunTyFlag.  Since
  the PiTyBinder really only describes the /argument/ it should perhaps
  only have a TypeOrConstraint rather than a full FunTyFlag.  But it's
  very convenient to have the full FunTyFlag, say in mkPiTys, so that's
  what we do.


Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* A ForAllTy (used for both types and kinds) contains a ForAllTyBinder.
  Each ForAllTyBinder
      Bndr a tvis
  is equipped with tvis::ForAllTyFlag, which says whether or not arguments
  for this binder should be visible (explicit) in source Haskell.

* A TyCon contains a list of TyConBinders.  Each TyConBinder
      Bndr a cvis
  is equipped with cvis::TyConBndrVis, which says whether or not type
  and kind arguments for this TyCon should be visible (explicit) in
  source Haskell.

This table summarises the visibility rules:
---------------------------------------------------------------------------------------
|                                                      Occurrences look like this
|                             GHC displays type as     in Haskell source code
|--------------------------------------------------------------------------------------
| Bndr a tvis :: ForAllTyBinder, in the binder of ForAllTy for a term
|  tvis :: ForAllTyFlag
|  tvis = Inferred:            f :: forall {a}. type    Arg not allowed:  f
                               f :: forall {co}. type   Arg not allowed:  f
|  tvis = Specified:           f :: forall a. type      Arg optional:     f  or  f @Int
|  tvis = Required:            f :: forall k -> type    Arg required:     f (type Int)
|
| Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon
|  cvis :: TyConBndrVis
|  cvis = AnonTCB:             T :: kind -> kind        Required:            T *
|  cvis = NamedTCB Inferred:   T :: forall {k}. kind    Arg not allowed:     T
|                              T :: forall {co}. kind   Arg not allowed:     T
|  cvis = NamedTCB Specified:  T :: forall k. kind      Arg not allowed[1]:  T
|  cvis = NamedTCB Required:   T :: forall k -> kind    Required:            T *
---------------------------------------------------------------------------------------

[1] In types, in the Specified case, it would make sense to allow
    optional kind applications, thus (T @*), but we have not
    yet implemented that

---- In term declarations ----

* Inferred.  Function defn, with no signature:  f1 x = x
  We infer f1 :: forall {a}. a -> a, with 'a' Inferred
  It's Inferred because it doesn't appear in any
  user-written signature for f1

* Specified.  Function defn, with signature (implicit forall):
     f2 :: a -> a; f2 x = x
  So f2 gets the type f2 :: forall a. a -> a, with 'a' Specified
  even though 'a' is not bound in the source code by an explicit forall

* Specified.  Function defn, with signature (explicit forall):
     f3 :: forall a. a -> a; f3 x = x
  So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified

* Required.  Function defn, with signature (explicit forall):
     f4 :: forall a -> a -> a; f4 (type _) x = x
  So f4 gets the type f4 :: forall a -> a -> a, with 'a' Required
  This is the experimental RequiredTypeArguments extension,
  see GHC Proposal #281 "Visible forall in types of terms"

* Inferred.  Function defn, with signature (explicit forall), marked as inferred:
     f5 :: forall {a}. a -> a; f5 x = x
  So f5 gets the type f5 :: forall {a}. a -> a, with 'a' Inferred
  It's Inferred because the user marked it as such, even though it does appear
  in the user-written signature for f5

* Inferred/Specified.  Function signature with inferred kind polymorphism.
     f6 :: a b -> Int
  So 'f6' gets the type f6 :: forall {k} (a :: k -> Type) (b :: k). a b -> Int
  Here 'k' is Inferred (it's not mentioned in the type),
  but 'a' and 'b' are Specified.

* Specified.  Function signature with explicit kind polymorphism
     f7 :: a (b :: k) -> Int
  This time 'k' is Specified, because it is mentioned explicitly,
  so we get f7 :: forall (k :: Type) (a :: k -> Type) (b :: k). a b -> Int

* Similarly pattern synonyms:
  Inferred - from inferred types (e.g. no pattern type signature)
           - or from inferred kind polymorphism

---- In type declarations ----

* Inferred (k)
     data T1 a b = MkT1 (a b)
  Here T1's kind is  T1 :: forall {k:*}. (k->*) -> k -> *
  The kind variable 'k' is Inferred, since it is not mentioned

  Note that 'a' and 'b' correspond to /Anon/ PiTyBinders in T1's kind,
  and Anon binders don't have a visibility flag. (Or you could think
  of Anon having an implicit Required flag.)

* Specified (k)
     data T2 (a::k->*) b = MkT (a b)
  Here T's kind is  T :: forall (k:*). (k->*) -> k -> *
  The kind variable 'k' is Specified, since it is mentioned in
  the signature.

* Required (k)
     data T k (a::k->*) b = MkT (a b)
  Here T's kind is  T :: forall k:* -> (k->*) -> k -> *
  The kind is Required, since it bound in a positional way in T's declaration
  Every use of T must be explicitly applied to a kind

* Inferred (k1), Specified (k)
     data T a b (c :: k) = MkT (a b) (Proxy c)
  Here T's kind is  T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
  So 'k' is Specified, because it appears explicitly,
  but 'k1' is Inferred, because it does not

Generally, in the list of TyConBinders for a TyCon,

* Inferred arguments always come first
* Specified, Anon and Required can be mixed

e.g.
  data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where ...

Here Foo's TyConBinders are
   [Required 'a', Specified 'b', Anon]
and its kind prints as
   Foo :: forall a -> forall b. (a -> b -> Type) -> Type

See also Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl

---- Printing -----

 We print forall types with enough syntax to tell you their visibility
 flag.  But this is not source Haskell, and these types may not all
 be parsable.

 Specified: a list of Specified binders is written between `forall` and `.`:
               const :: forall a b. a -> b -> a

 Inferred: like Specified, but every binder is written in braces:
               f :: forall {k} (a :: k). S k a -> Int

 Required: binders are put between `forall` and `->`:
              T :: forall k -> *

---- Other points -----

* In classic Haskell, all named binders (that is, the type variables in
  a polymorphic function type f :: forall a. a -> a) have been Inferred.

* Inferred variables correspond to "generalized" variables from the
  Visible Type Applications paper (ESOP'16).
-}



{-
************************************************************************
*                                                                      *
*                 Type and kind variables                              *
*                                                                      *
************************************************************************
-}

tyVarName :: TyVar -> Name
tyVarName :: Id -> Name
tyVarName = Id -> Name
varName

tyVarKind :: TyVar -> Kind
tyVarKind :: Id -> Mult
tyVarKind = Id -> Mult
varType

setTyVarUnique :: TyVar -> Unique -> TyVar
setTyVarUnique :: Id -> Unique -> Id
setTyVarUnique = Id -> Unique -> Id
setVarUnique

setTyVarName :: TyVar -> Name -> TyVar
setTyVarName :: Id -> Name -> Id
setTyVarName   = Id -> Name -> Id
setVarName

setTyVarKind :: TyVar -> Kind -> TyVar
setTyVarKind :: Id -> Mult -> Id
setTyVarKind Id
tv Mult
k = Id
tv {varType = k}

updateTyVarKind :: (Kind -> Kind) -> TyVar -> TyVar
updateTyVarKind :: (Mult -> Mult) -> Id -> Id
updateTyVarKind Mult -> Mult
update Id
tv = Id
tv {varType = update (tyVarKind tv)}

updateTyVarKindM :: (Monad m) => (Kind -> m Kind) -> TyVar -> m TyVar
updateTyVarKindM :: forall (m :: * -> *). Monad m => (Mult -> m Mult) -> Id -> m Id
updateTyVarKindM Mult -> m Mult
update Id
tv
  = do { k' <- Mult -> m Mult
update (Id -> Mult
tyVarKind Id
tv)
       ; return $ tv {varType = k'} }

mkTyVar :: Name -> Kind -> TyVar
mkTyVar :: Name -> Mult -> Id
mkTyVar Name
name Mult
kind = TyVar { varName :: Name
varName    = Name
name
                          , realUnique :: Unique
realUnique = Name -> Unique
nameUnique Name
name
                          , varType :: Mult
varType  = Mult
kind
                          }

mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar
mkTcTyVar :: Name -> Mult -> TcTyVarDetails -> Id
mkTcTyVar Name
name Mult
kind TcTyVarDetails
details
  = -- NB: 'kind' may be a coercion kind; cf, 'GHC.Tc.Utils.TcMType.newMetaCoVar'
    TcTyVar {   varName :: Name
varName    = Name
name,
                realUnique :: Unique
realUnique = Name -> Unique
nameUnique Name
name,
                varType :: Mult
varType  = Mult
kind,
                tc_tv_details :: TcTyVarDetails
tc_tv_details = TcTyVarDetails
details
        }

tcTyVarDetails :: TyVar -> TcTyVarDetails
-- See Note [TcTyVars and TyVars in the typechecker] in GHC.Tc.Utils.TcType
tcTyVarDetails :: Id -> TcTyVarDetails
tcTyVarDetails (TcTyVar { tc_tv_details :: Id -> TcTyVarDetails
tc_tv_details = TcTyVarDetails
details }) = TcTyVarDetails
details
-- MP: This should never happen, but it does. Future work is to turn this into a panic.
tcTyVarDetails (TyVar {})                            = TcTyVarDetails
HasDebugCallStack => TcTyVarDetails
vanillaSkolemTvUnk
tcTyVarDetails Id
var = String -> SDoc -> TcTyVarDetails
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tcTyVarDetails" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
var SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Mult -> SDoc
pprKind (Id -> Mult
tyVarKind Id
var))

setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar
setTcTyVarDetails :: Id -> TcTyVarDetails -> Id
setTcTyVarDetails Id
tv TcTyVarDetails
details = Id
tv { tc_tv_details = details }

{-
%************************************************************************
%*                                                                      *
\subsection{Ids}
*                                                                      *
************************************************************************
-}

idInfo :: HasDebugCallStack => Id -> IdInfo
idInfo :: HasDebugCallStack => Id -> IdInfo
idInfo (Id { id_info :: Id -> IdInfo
id_info = IdInfo
info }) = IdInfo
info
idInfo Id
other                   = String -> SDoc -> IdInfo
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"idInfo" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
other)

idDetails :: Id -> IdDetails
idDetails :: Id -> IdDetails
idDetails (Id { id_details :: Id -> IdDetails
id_details = IdDetails
details }) = IdDetails
details
idDetails Id
other                         = String -> SDoc -> IdDetails
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"idDetails" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
other)

-- The next three have a 'Var' suffix even though they always build
-- Ids, because "GHC.Types.Id" uses 'mkGlobalId' etc with different types
mkGlobalVar :: IdDetails -> Name -> Type -> IdInfo -> Id
mkGlobalVar :: IdDetails -> Name -> Mult -> IdInfo -> Id
mkGlobalVar IdDetails
details Name
name Mult
ty IdInfo
info
  = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Id
mk_id Name
name Mult
manyDataConTy Mult
ty IdScope
GlobalId IdDetails
details IdInfo
info
  -- There is no support for linear global variables yet. They would require
  -- being checked at link-time, which can be useful, but is not a priority.

mkLocalVar :: IdDetails -> Name -> Mult -> Type -> IdInfo -> Id
mkLocalVar :: IdDetails -> Name -> Mult -> Mult -> IdInfo -> Id
mkLocalVar IdDetails
details Name
name Mult
w Mult
ty IdInfo
info
  = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Id
mk_id Name
name Mult
w Mult
ty (ExportFlag -> IdScope
LocalId ExportFlag
NotExported) IdDetails
details  IdInfo
info

mkCoVar :: Name -> Type -> CoVar
-- Coercion variables have no IdInfo
mkCoVar :: Name -> Mult -> Id
mkCoVar Name
name Mult
ty = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Id
mk_id Name
name Mult
manyDataConTy Mult
ty (ExportFlag -> IdScope
LocalId ExportFlag
NotExported) IdDetails
coVarDetails IdInfo
vanillaIdInfo

-- | Exported 'Var's will not be removed as dead code
mkExportedLocalVar :: IdDetails -> Name -> Type -> IdInfo -> Id
mkExportedLocalVar :: IdDetails -> Name -> Mult -> IdInfo -> Id
mkExportedLocalVar IdDetails
details Name
name Mult
ty IdInfo
info
  = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Id
mk_id Name
name Mult
manyDataConTy Mult
ty (ExportFlag -> IdScope
LocalId ExportFlag
Exported) IdDetails
details IdInfo
info
  -- There is no support for exporting linear variables. See also [mkGlobalVar]

mk_id :: Name -> Mult -> Type -> IdScope -> IdDetails -> IdInfo -> Id
mk_id :: Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Id
mk_id Name
name !Mult
w Mult
ty IdScope
scope IdDetails
details IdInfo
info
  = Id { varName :: Name
varName    = Name
name,
         realUnique :: Unique
realUnique = Name -> Unique
nameUnique Name
name,
         varMult :: Mult
varMult    = Mult
w,
         varType :: Mult
varType    = Mult
ty,
         idScope :: IdScope
idScope    = IdScope
scope,
         id_details :: IdDetails
id_details = IdDetails
details,
         id_info :: IdInfo
id_info    = IdInfo
info }

-------------------
lazySetIdInfo :: Id -> IdInfo -> Var
lazySetIdInfo :: Id -> IdInfo -> Id
lazySetIdInfo Id
id IdInfo
info = Id
id { id_info = info }

setIdDetails :: Id -> IdDetails -> Id
setIdDetails :: Id -> IdDetails -> Id
setIdDetails Id
id IdDetails
details = Id
id { id_details = details }

globaliseId :: Id -> Id
-- ^ If it's a local, make it global
globaliseId :: Id -> Id
globaliseId Id
id = Id
id { idScope = GlobalId }

setIdExported :: Id -> Id
-- ^ Exports the given local 'Id'. Can also be called on global 'Id's, such as data constructors
-- and class operations, which are born as global 'Id's and automatically exported
setIdExported :: Id -> Id
setIdExported id :: Id
id@(Id { idScope :: Id -> IdScope
idScope = LocalId {} }) = Id
id { idScope = LocalId Exported }
setIdExported id :: Id
id@(Id { idScope :: Id -> IdScope
idScope = IdScope
GlobalId })   = Id
id
setIdExported Id
tv                               = String -> SDoc -> Id
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setIdExported" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv)

setIdNotExported :: Id -> Id
-- ^ We can only do this to LocalIds
setIdNotExported :: Id -> Id
setIdNotExported Id
id = Bool -> Id -> Id
forall a. HasCallStack => Bool -> a -> a
assert (Id -> Bool
isLocalId Id
id) (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$
                      Id
id { idScope = LocalId NotExported }

-----------------------
updateIdTypeButNotMult :: (Type -> Type) -> Id -> Id
updateIdTypeButNotMult :: (Mult -> Mult) -> Id -> Id
updateIdTypeButNotMult Mult -> Mult
f Id
id = Id
id { varType = f (varType id) }


updateIdTypeAndMult :: (Type -> Type) -> Id -> Id
updateIdTypeAndMult :: (Mult -> Mult) -> Id -> Id
updateIdTypeAndMult Mult -> Mult
f id :: Id
id@(Id { varType :: Id -> Mult
varType = Mult
ty
                             , varMult :: Id -> Mult
varMult = Mult
mult })
  = Id
id { varType = ty'
       , varMult = mult' }
  where
    !ty' :: Mult
ty'   = Mult -> Mult
f Mult
ty
    !mult' :: Mult
mult' = Mult -> Mult
f Mult
mult
updateIdTypeAndMult Mult -> Mult
_ Id
other = String -> SDoc -> Id
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"updateIdTypeAndMult" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
other)

updateIdTypeAndMultM :: Monad m => (Type -> m Type) -> Id -> m Id
updateIdTypeAndMultM :: forall (m :: * -> *). Monad m => (Mult -> m Mult) -> Id -> m Id
updateIdTypeAndMultM Mult -> m Mult
f id :: Id
id@(Id { varType :: Id -> Mult
varType = Mult
ty
                              , varMult :: Id -> Mult
varMult = Mult
mult })
  = do { !ty' <- Mult -> m Mult
f Mult
ty
       ; !mult' <- f mult
       ; return (id { varType = ty', varMult = mult' }) }
updateIdTypeAndMultM Mult -> m Mult
_ Id
other = String -> SDoc -> m Id
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"updateIdTypeAndMultM" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
other)

setIdMult :: Id -> Mult -> Id
setIdMult :: Id -> Mult -> Id
setIdMult Id
id !Mult
r | Id -> Bool
isId Id
id = Id
id { varMult = r }
                | Bool
otherwise = String -> SDoc -> Id
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setIdMult" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
id SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Mult -> SDoc
forall a. Outputable a => a -> SDoc
ppr Mult
r)

{-
************************************************************************
*                                                                      *
\subsection{Predicates over variables}
*                                                                      *
************************************************************************
-}

-- | Is this a type-level (i.e., computationally irrelevant, thus erasable)
-- variable? Satisfies @isTyVar = not . isId@.
isTyVar :: Var -> Bool        -- True of both TyVar and TcTyVar
isTyVar :: Id -> Bool
isTyVar (TyVar {})   = Bool
True
isTyVar (TcTyVar {}) = Bool
True
isTyVar Id
_            = Bool
False

isTcTyVar :: Var -> Bool      -- True of TcTyVar only
isTcTyVar :: Id -> Bool
isTcTyVar (TcTyVar {}) = Bool
True
isTcTyVar Id
_            = Bool
False

isTyCoVar :: Var -> Bool
isTyCoVar :: Id -> Bool
isTyCoVar Id
v = Id -> Bool
isTyVar Id
v Bool -> Bool -> Bool
|| Id -> Bool
isCoVar Id
v

-- | Is this a value-level (i.e., computationally relevant) 'Id'entifier?
-- Satisfies @isId = not . isTyVar@.
isId :: Var -> Bool
isId :: Id -> Bool
isId (Id {}) = Bool
True
isId Id
_       = Bool
False

-- | Is this a coercion variable?
-- Satisfies @'isId' v ==> 'isCoVar' v == not ('isNonCoVarId' v)@.
isCoVar :: Var -> Bool
isCoVar :: Id -> Bool
isCoVar (Id { id_details :: Id -> IdDetails
id_details = IdDetails
details }) = IdDetails -> Bool
isCoVarDetails IdDetails
details
isCoVar Id
_                             = Bool
False

-- | Is this a term variable ('Id') that is /not/ a coercion variable?
-- Satisfies @'isId' v ==> 'isCoVar' v == not ('isNonCoVarId' v)@.
isNonCoVarId :: Var -> Bool
isNonCoVarId :: Id -> Bool
isNonCoVarId (Id { id_details :: Id -> IdDetails
id_details = IdDetails
details }) = Bool -> Bool
not (IdDetails -> Bool
isCoVarDetails IdDetails
details)
isNonCoVarId Id
_                             = Bool
False

isLocalId :: Var -> Bool
isLocalId :: Id -> Bool
isLocalId (Id { idScope :: Id -> IdScope
idScope = LocalId ExportFlag
_ }) = Bool
True
isLocalId Id
_                            = Bool
False

isLocalId_maybe :: Var -> Maybe ExportFlag
isLocalId_maybe :: Id -> Maybe ExportFlag
isLocalId_maybe (Id { idScope :: Id -> IdScope
idScope = LocalId ExportFlag
ef }) = ExportFlag -> Maybe ExportFlag
forall a. a -> Maybe a
Just ExportFlag
ef
isLocalId_maybe Id
_                             = Maybe ExportFlag
forall a. Maybe a
Nothing

-- | 'isLocalVar' returns @True@ for type variables as well as local 'Id's
-- These are the variables that we need to pay attention to when finding free
-- variables, or doing dependency analysis.
isLocalVar :: Var -> Bool
isLocalVar :: Id -> Bool
isLocalVar Id
v = Bool -> Bool
not (Id -> Bool
isGlobalId Id
v)

isGlobalId :: Var -> Bool
isGlobalId :: Id -> Bool
isGlobalId (Id { idScope :: Id -> IdScope
idScope = IdScope
GlobalId }) = Bool
True
isGlobalId Id
_                           = Bool
False

-- | 'mustHaveLocalBinding' returns @True@ of 'Id's and 'TyVar's
-- that must have a binding in this module.  The converse
-- is not quite right: there are some global 'Id's that must have
-- bindings, such as record selectors.  But that doesn't matter,
-- because it's only used for assertions
mustHaveLocalBinding        :: Var -> Bool
mustHaveLocalBinding :: Id -> Bool
mustHaveLocalBinding Id
var = Id -> Bool
isLocalVar Id
var

-- | 'isExportedIdVar' means \"don't throw this away\"
isExportedId :: Var -> Bool
isExportedId :: Id -> Bool
isExportedId (Id { idScope :: Id -> IdScope
idScope = IdScope
GlobalId })        = Bool
True
isExportedId (Id { idScope :: Id -> IdScope
idScope = LocalId ExportFlag
Exported}) = Bool
True
isExportedId Id
_ = Bool
False