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

\section{@Vars@: Variables}
-}

{-# LANGUAGE FlexibleContexts, MultiWayIf, FlexibleInstances, DeriveDataTypeable,
             PatternSynonyms, BangPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}

-- |
-- #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,
        varMult, varMultMaybe,

        -- ** 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, isCoVar, isNonCoVarId, isTyCoVar,
        isGlobalId, isExportedId,
        mustHaveLocalBinding,

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

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

        -- * PiTyBinder
        PiTyBinder(..), PiTyVarBinder,
        isInvisiblePiTyBinder, 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,
        isTyVarBinder,
        tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders,
        mapVarBndr, mapVarBndrs,

        -- ** 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
                        , mkUniqueGrimily, nonDetCmpUnique )
import GHC.Types.Basic( TypeOrConstraint(..) )
import GHC.Utils.Misc
import GHC.Utils.Binary
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain

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]
        Var -> Name
varName    :: !Name,
        Var -> Int
realUnique :: {-# UNPACK #-} !Int,
                                     -- ^ Key for fast comparison
                                     -- Identical to the Unique in the name,
                                     -- cached here for speed
        Var -> 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 #-} !Int,
        varType        :: Kind,
        Var -> TcTyVarDetails
tc_tv_details  :: TcTyVarDetails
  }

  | Id {
        varName    :: !Name,
        realUnique :: {-# UNPACK #-} !Int,
        varType    :: Type,
        Var -> Mult
varMult    :: Mult,             -- See Note [Multiplicity of let binders]
        Var -> IdScope
idScope    :: IdScope,
        Var -> IdDetails
id_details :: IdDetails,        -- Stable, doesn't change
        Var -> 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

After CoreTidy, top-level LocalIds are turned into GlobalIds

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 :: Var -> SDoc
ppr Var
var = forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
sdocOption SDocContext -> Bool
sdocSuppressVarKinds forall a b. (a -> b) -> a -> b
$ \Bool
supp_var_kinds ->
            forall doc. IsOutput doc => (Bool -> doc) -> doc
getPprDebug forall a b. (a -> b) -> a -> b
$ \Bool
debug ->
            (PprStyle -> SDoc) -> SDoc
getPprStyle forall a b. (a -> b) -> a -> b
$ \PprStyle
sty ->
            let
              ppr_var :: SDoc
ppr_var = case Var
var of
                  (TyVar {})
                     | Bool
debug
                     -> forall doc. IsLine doc => doc -> doc
brackets (forall doc. IsLine doc => String -> doc
text String
"tv")

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

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

                  Var
_  -> forall doc. IsOutput doc => doc
empty
            in if
               |  Bool
debug Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
supp_var_kinds)
                 -> forall doc. IsLine doc => doc -> doc
parens (forall a. Outputable a => a -> SDoc
ppr (Var -> Name
varName Var
var) forall doc. IsLine doc => doc -> doc -> doc
<+> forall a. Outputable a => a -> SDoc
ppr (Var -> Maybe Mult
varMultMaybe Var
var)
                                              forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
ppr_var forall doc. IsLine doc => doc -> doc -> doc
<+>
                          SDoc
dcolon forall doc. IsLine doc => doc -> doc -> doc
<+> Mult -> SDoc
pprKind (Var -> Mult
tyVarKind Var
var))
               |  Bool
otherwise
                 -> forall a. Outputable a => a -> SDoc
ppr (Var -> Name
varName Var
var) 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              = forall doc. IsLine doc => String -> doc
text String
"gid"
ppr_id_scope (LocalId ExportFlag
Exported)    = forall doc. IsLine doc => String -> doc
text String
"lidx"
ppr_id_scope (LocalId ExportFlag
NotExported) = forall doc. IsLine doc => String -> doc
text String
"lid"

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

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

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

instance Ord Var where
    Var
a <= :: Var -> Var -> Bool
<= Var
b = Var -> Int
realUnique Var
a forall a. Ord a => a -> a -> Bool
<= Var -> Int
realUnique Var
b
    Var
a < :: Var -> Var -> Bool
<  Var
b = Var -> Int
realUnique Var
a forall a. Ord a => a -> a -> Bool
<  Var -> Int
realUnique Var
b
    Var
a >= :: Var -> Var -> Bool
>= Var
b = Var -> Int
realUnique Var
a forall a. Ord a => a -> a -> Bool
>= Var -> Int
realUnique Var
b
    Var
a > :: Var -> Var -> Bool
>  Var
b = Var -> Int
realUnique Var
a forall a. Ord a => a -> a -> Bool
>  Var -> Int
realUnique Var
b
    Var
a compare :: Var -> Var -> Ordering
`compare` Var
b = Var
a Var -> Var -> Ordering
`nonDetCmpVar` Var
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 :: Var -> Var -> Ordering
nonDetCmpVar Var
a Var
b = Var -> Unique
varUnique Var
a Unique -> Unique -> Ordering
`nonDetCmpUnique` Var -> Unique
varUnique Var
b

instance Data Var where
  -- don't traverse?
  toConstr :: Var -> Constr
toConstr Var
_   = 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 Var
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_  = forall a. HasCallStack => String -> a
error String
"gunfold"
  dataTypeOf :: Var -> DataType
dataTypeOf Var
_ = String -> DataType
mkNoRepType String
"Var"

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

varUnique :: Var -> Unique
varUnique :: Var -> Unique
varUnique Var
var = Int -> Unique
mkUniqueGrimily (Var -> Int
realUnique Var
var)

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

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

setVarName :: Var -> Name -> Var
setVarName :: Var -> Name -> Var
setVarName Var
var Name
new_name
  = Var
var { realUnique :: Int
realUnique = Unique -> Int
getKey (forall a. Uniquable a => a -> Unique
getUnique Name
new_name),
          varName :: Name
varName = Name
new_name }

setVarType :: Var -> Type -> Var
setVarType :: Var -> Mult -> Var
setVarType Var
id Mult
ty = Var
id { varType :: Mult
varType = Mult
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) -> Var -> Var
updateVarType Mult -> Mult
upd Var
var
  = case Var
var of
      Id { id_details :: Var -> IdDetails
id_details = IdDetails
details } -> forall a. HasCallStack => Bool -> a -> a
assert (IdDetails -> Bool
isCoVarDetails IdDetails
details) forall a b. (a -> b) -> a -> b
$
                                     Var
result
      Var
_ -> Var
result
  where
    result :: Var
result = Var
var { varType :: Mult
varType = Mult -> Mult
upd (Var -> Mult
varType Var
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) -> Var -> m Var
updateVarTypeM Mult -> m Mult
upd Var
var
  = case Var
var of
      Id { id_details :: Var -> IdDetails
id_details = IdDetails
details } -> forall a. HasCallStack => Bool -> a -> a
assert (IdDetails -> Bool
isCoVarDetails IdDetails
details) forall a b. (a -> b) -> a -> b
$
                                     m Var
result
      Var
_ -> m Var
result
  where
    result :: m Var
result = do { Mult
ty' <- Mult -> m Mult
upd (Var -> Mult
varType Var
var)
                ; forall (m :: * -> *) a. Monad m => a -> m a
return (Var
var { varType :: Mult
varType = Mult
ty' }) }

{- *********************************************************************
*                                                                      *
*                   ForAllTyFlag
*                                                                      *
********************************************************************* -}

-- | ForAllTyFlag
--
-- Is something required to appear in source Haskell ('Required'),
-- permitted by request ('Specified') (visible type application), or
-- prohibited entirely from appearing in source Haskell ('Inferred')?
-- See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep"
data ForAllTyFlag = Invisible Specificity
                  | Required
  deriving (ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ForAllTyFlag -> ForAllTyFlag -> Bool
$c/= :: ForAllTyFlag -> ForAllTyFlag -> Bool
== :: ForAllTyFlag -> ForAllTyFlag -> Bool
$c== :: ForAllTyFlag -> ForAllTyFlag -> Bool
Eq, Eq ForAllTyFlag
ForAllTyFlag -> ForAllTyFlag -> Bool
ForAllTyFlag -> ForAllTyFlag -> Ordering
ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag
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
min :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag
$cmin :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag
max :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag
$cmax :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag
>= :: ForAllTyFlag -> ForAllTyFlag -> Bool
$c>= :: ForAllTyFlag -> ForAllTyFlag -> Bool
> :: ForAllTyFlag -> ForAllTyFlag -> Bool
$c> :: ForAllTyFlag -> ForAllTyFlag -> Bool
<= :: ForAllTyFlag -> ForAllTyFlag -> Bool
$c<= :: ForAllTyFlag -> ForAllTyFlag -> Bool
< :: ForAllTyFlag -> ForAllTyFlag -> Bool
$c< :: ForAllTyFlag -> ForAllTyFlag -> Bool
compare :: ForAllTyFlag -> ForAllTyFlag -> Ordering
$ccompare :: ForAllTyFlag -> ForAllTyFlag -> Ordering
Ord, Typeable ForAllTyFlag
ForAllTyFlag -> DataType
ForAllTyFlag -> Constr
(forall b. Data b => b -> b) -> ForAllTyFlag -> ForAllTyFlag
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) -> ForAllTyFlag -> u
forall u. (forall d. Data d => d -> u) -> ForAllTyFlag -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ForAllTyFlag
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ForAllTyFlag -> c ForAllTyFlag
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ForAllTyFlag)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ForAllTyFlag)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ForAllTyFlag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ForAllTyFlag -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> ForAllTyFlag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ForAllTyFlag -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r
gmapT :: (forall b. Data b => b -> b) -> ForAllTyFlag -> ForAllTyFlag
$cgmapT :: (forall b. Data b => b -> b) -> ForAllTyFlag -> ForAllTyFlag
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ForAllTyFlag)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ForAllTyFlag)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ForAllTyFlag)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ForAllTyFlag)
dataTypeOf :: ForAllTyFlag -> DataType
$cdataTypeOf :: ForAllTyFlag -> DataType
toConstr :: ForAllTyFlag -> Constr
$ctoConstr :: ForAllTyFlag -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ForAllTyFlag
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ForAllTyFlag
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ForAllTyFlag -> c ForAllTyFlag
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ForAllTyFlag -> c ForAllTyFlag
Data)
  -- (<) on ForAllTyFlag means "is less visible than"

-- | Whether an 'Invisible' argument may appear in source Haskell.
data Specificity = InferredSpec
                   -- ^ the argument may not appear in source Haskell, it is
                   -- only inferred.
                 | SpecifiedSpec
                   -- ^ the argument may appear in source Haskell, but isn't
                   -- required.
  deriving (Specificity -> Specificity -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Specificity -> Specificity -> Bool
$c/= :: Specificity -> Specificity -> Bool
== :: Specificity -> Specificity -> Bool
$c== :: Specificity -> Specificity -> Bool
Eq, Eq Specificity
Specificity -> Specificity -> Bool
Specificity -> Specificity -> Ordering
Specificity -> Specificity -> Specificity
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
min :: Specificity -> Specificity -> Specificity
$cmin :: Specificity -> Specificity -> Specificity
max :: Specificity -> Specificity -> Specificity
$cmax :: Specificity -> Specificity -> Specificity
>= :: Specificity -> Specificity -> Bool
$c>= :: Specificity -> Specificity -> Bool
> :: Specificity -> Specificity -> Bool
$c> :: Specificity -> Specificity -> Bool
<= :: Specificity -> Specificity -> Bool
$c<= :: Specificity -> Specificity -> Bool
< :: Specificity -> Specificity -> Bool
$c< :: Specificity -> Specificity -> Bool
compare :: Specificity -> Specificity -> Ordering
$ccompare :: Specificity -> Specificity -> Ordering
Ord, Typeable Specificity
Specificity -> DataType
Specificity -> Constr
(forall b. Data b => b -> b) -> Specificity -> Specificity
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) -> Specificity -> u
forall u. (forall d. Data d => d -> u) -> Specificity -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Specificity -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Specificity -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Specificity
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specificity -> c Specificity
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Specificity)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Specificity)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Specificity -> m Specificity
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Specificity -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Specificity -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Specificity -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Specificity -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Specificity -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Specificity -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Specificity -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Specificity -> r
gmapT :: (forall b. Data b => b -> b) -> Specificity -> Specificity
$cgmapT :: (forall b. Data b => b -> b) -> Specificity -> Specificity
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Specificity)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Specificity)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Specificity)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Specificity)
dataTypeOf :: Specificity -> DataType
$cdataTypeOf :: Specificity -> DataType
toConstr :: Specificity -> Constr
$ctoConstr :: Specificity -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Specificity
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Specificity
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specificity -> c Specificity
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Specificity -> c Specificity
Data)

pattern Inferred, Specified :: ForAllTyFlag
pattern $bInferred :: ForAllTyFlag
$mInferred :: forall {r}. ForAllTyFlag -> ((# #) -> r) -> ((# #) -> r) -> r
Inferred  = Invisible InferredSpec
pattern $bSpecified :: ForAllTyFlag
$mSpecified :: forall {r}. ForAllTyFlag -> ((# #) -> r) -> ((# #) -> r) -> r
Specified = Invisible SpecifiedSpec

{-# COMPLETE Required, Specified, Inferred #-}

-- | Does this 'ForAllTyFlag' classify an argument that is written in Haskell?
isVisibleForAllTyFlag :: ForAllTyFlag -> Bool
isVisibleForAllTyFlag :: ForAllTyFlag -> Bool
isVisibleForAllTyFlag ForAllTyFlag
af = Bool -> Bool
not (ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
af)

-- | Does this 'ForAllTyFlag' classify an argument that is not written in Haskell?
isInvisibleForAllTyFlag :: ForAllTyFlag -> Bool
isInvisibleForAllTyFlag :: ForAllTyFlag -> Bool
isInvisibleForAllTyFlag (Invisible {}) = Bool
True
isInvisibleForAllTyFlag ForAllTyFlag
Required       = Bool
False

isInferredForAllTyFlag :: ForAllTyFlag -> Bool
-- More restrictive than isInvisibleForAllTyFlag
isInferredForAllTyFlag :: ForAllTyFlag -> Bool
isInferredForAllTyFlag (Invisible Specificity
InferredSpec) = Bool
True
isInferredForAllTyFlag ForAllTyFlag
_                        = Bool
False

instance Outputable ForAllTyFlag where
  ppr :: ForAllTyFlag -> SDoc
ppr ForAllTyFlag
Required  = forall doc. IsLine doc => String -> doc
text String
"[req]"
  ppr ForAllTyFlag
Specified = forall doc. IsLine doc => String -> doc
text String
"[spec]"
  ppr ForAllTyFlag
Inferred  = forall doc. IsLine doc => String -> doc
text String
"[infrd]"

instance Binary Specificity where
  put_ :: BinHandle -> Specificity -> IO ()
put_ BinHandle
bh Specificity
SpecifiedSpec = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
0
  put_ BinHandle
bh Specificity
InferredSpec  = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1

  get :: BinHandle -> IO Specificity
get BinHandle
bh = do
    Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
    case Word8
h of
      Word8
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return Specificity
SpecifiedSpec
      Word8
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Specificity
InferredSpec

instance Binary ForAllTyFlag where
  put_ :: BinHandle -> ForAllTyFlag -> IO ()
put_ BinHandle
bh ForAllTyFlag
Required  = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
0
  put_ BinHandle
bh ForAllTyFlag
Specified = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1
  put_ BinHandle
bh ForAllTyFlag
Inferred  = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2

  get :: BinHandle -> IO ForAllTyFlag
get BinHandle
bh = do
    Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
    case Word8
h of
      Word8
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return ForAllTyFlag
Required
      Word8
1 -> forall (m :: * -> *) a. Monad m => a -> m a
return ForAllTyFlag
Specified
      Word8
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ForAllTyFlag
Inferred

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

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

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

  get :: BinHandle -> IO FunTyFlag
get BinHandle
bh = do
    Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
    case Word8
h of
      Word8
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return FunTyFlag
FTF_T_T
      Word8
1 -> forall (m :: * -> *) a. Monad m => a -> m a
return FunTyFlag
FTF_T_C
      Word8
2 -> forall (m :: * -> *) a. Monad m => a -> m a
return FunTyFlag
FTF_C_T
      Word8
_ -> 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

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

* TyCon.TyConPiTyBinder = VarBndr TyCoVar TyConBndrVis
  Binders of a PromotedDataCon
  See Note [Promoted GADT data constructors] 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( VarBndr var argf -> DataType
VarBndr var argf -> Constr
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 {var} {argf}.
(Data var, Data argf) =>
Typeable (VarBndr var argf)
forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> DataType
forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> Constr
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 (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 e. (Data d, Data e) => c (t d e))
-> Maybe (c (VarBndr var argf))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> VarBndr var argf -> m (VarBndr var argf)
$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)
gmapQi :: forall u.
Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> VarBndr var argf -> [u]
$cgmapQ :: forall var argf u.
(Data var, Data argf) =>
(forall d. Data d => d -> u) -> VarBndr var argf -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
$cgmapQl :: forall var argf r r'.
(Data var, Data argf) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarBndr var argf -> r
gmapT :: (forall b. Data b => b -> b)
-> VarBndr var argf -> VarBndr var argf
$cgmapT :: forall var argf.
(Data var, Data argf) =>
(forall b. Data b => b -> b)
-> VarBndr var argf -> 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))
$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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (VarBndr var argf))
$cdataCast1 :: forall var argf (t :: * -> *) (c :: * -> *).
(Data var, Data argf, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (VarBndr var argf))
dataTypeOf :: VarBndr var argf -> DataType
$cdataTypeOf :: forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> DataType
toConstr :: VarBndr var argf -> Constr
$ctoConstr :: forall var argf.
(Data var, Data argf) =>
VarBndr var argf -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
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)
$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)
Data )

-- | 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 = forall a b. (a -> b) -> [a] -> [b]
map 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) = 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 = forall a b. (a -> b) -> [a] -> [b]
map 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 ()
_) = forall var argf. var -> argf -> VarBndr var argf
Bndr a
tv ForAllTyFlag
Required

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 = forall a b. (a -> b) -> [a] -> [b]
map 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 = forall a b. (a -> b) -> [a] -> [b]
map forall tv argf. VarBndr tv argf -> argf
binderFlag [VarBndr tv argf]
tvbs

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

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

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

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

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

-- | Make many named binders
-- Input vars should be type variables
mkTyVarBinders :: vis -> [TyVar] -> [VarBndr TyVar vis]
mkTyVarBinders :: forall vis. vis -> [Var] -> [VarBndr Var vis]
mkTyVarBinders vis
vis = forall a b. (a -> b) -> [a] -> [b]
map (forall vis. vis -> Var -> VarBndr Var 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) = 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 = forall a b. (a -> b) -> [a] -> [b]
map (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)  = forall a. Outputable a => a -> SDoc
ppr tv
v
  ppr (Bndr tv
v ForAllTyFlag
Specified) = forall doc. IsLine doc => Char -> doc
char Char
'@' forall doc. IsLine doc => doc -> doc -> doc
<> forall a. Outputable a => a -> SDoc
ppr tv
v
  ppr (Bndr tv
v ForAllTyFlag
Inferred)  = forall doc. IsLine doc => doc -> doc
braces (forall a. Outputable a => a -> SDoc
ppr tv
v)

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

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

  get :: BinHandle -> IO (VarBndr tv vis)
get BinHandle
bh = do { tv
tv <- forall a. Binary a => BinHandle -> IO a
get BinHandle
bh; vis
vis <- forall a. Binary a => BinHandle -> IO a
get BinHandle
bh; forall (m :: * -> *) a. Monad m => a -> m a
return (forall var argf. var -> argf -> VarBndr var argf
Bndr tv
tv vis
vis) }

instance NamedThing tv => NamedThing (VarBndr tv flag) where
  getName :: VarBndr tv flag -> Name
getName (Bndr tv
tv flag
_) = 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
PiTyBinder -> DataType
PiTyBinder -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PiTyBinder -> m PiTyBinder
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PiTyBinder -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PiTyBinder -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> PiTyBinder -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PiTyBinder -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PiTyBinder -> r
gmapT :: (forall b. Data b => b -> b) -> PiTyBinder -> PiTyBinder
$cgmapT :: (forall b. Data b => b -> b) -> PiTyBinder -> PiTyBinder
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PiTyBinder)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PiTyBinder)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PiTyBinder)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PiTyBinder)
dataTypeOf :: PiTyBinder -> DataType
$cdataTypeOf :: PiTyBinder -> DataType
toConstr :: PiTyBinder -> Constr
$ctoConstr :: PiTyBinder -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PiTyBinder
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PiTyBinder
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PiTyBinder -> c PiTyBinder
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PiTyBinder -> c PiTyBinder
Data

instance Outputable PiTyBinder where
  ppr :: PiTyBinder -> SDoc
ppr (Anon Scaled Mult
ty FunTyFlag
af) = forall a. Outputable a => a -> SDoc
ppr FunTyFlag
af forall doc. IsLine doc => doc -> doc -> doc
<+> forall a. Outputable a => a -> SDoc
ppr Scaled Mult
ty
  ppr (Named (Bndr Var
v ForAllTyFlag
Required))  = forall a. Outputable a => a -> SDoc
ppr Var
v
  ppr (Named (Bndr Var
v ForAllTyFlag
Specified)) = forall doc. IsLine doc => Char -> doc
char Char
'@' forall doc. IsLine doc => doc -> doc -> doc
<> forall a. Outputable a => a -> SDoc
ppr Var
v
  ppr (Named (Bndr Var
v ForAllTyFlag
Inferred))  = forall doc. IsLine doc => doc -> doc
braces (forall a. Outputable a => a -> SDoc
ppr Var
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 Var
_ ForAllTyFlag
vis)) = ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
vis
isInvisiblePiTyBinder (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 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 Var
namedPiTyBinder_maybe (Named ForAllTyBinder
tv) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall tv argf. VarBndr tv argf -> tv
binderVar ForAllTyBinder
tv
namedPiTyBinder_maybe PiTyBinder
_          = 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 {})  = forall a. Maybe a
Nothing
anonPiTyBinderType_maybe (Anon Scaled Mult
ty FunTyFlag
_) = forall a. a -> Maybe a
Just (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) = forall vis. VarBndr Var vis -> Bool
isTyVarBinder ForAllTyBinder
bnd
isTyBinder PiTyBinder
_ = Bool
True

piTyBinderType :: PiTyBinder -> Type
piTyBinderType :: PiTyBinder -> Mult
piTyBinderType (Named (Bndr Var
tv ForAllTyFlag
_)) = Var -> Mult
varType Var
tv
piTyBinderType (Anon Scaled Mult
ty FunTyFlag
_)         = 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:            T :: forall k -> type    Arg required:     T *
|    This last form is illegal in terms: See Note [No Required PiTyBinder in terms]
|
| 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

* Inferred.  Function defn, with signature (explicit forall), marked as inferred:
     f4 :: forall {a}. a -> a; f4 x = x
  So f4 gets the type f4 :: 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 f4

* Inferred/Specified.  Function signature with inferred kind polymorphism.
     f5 :: a b -> Int
  So 'f5' gets the type f5 :: forall {k} (a:k->*) (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
     f6 :: a (b :: k) -> Int
  This time 'k' is Specified, because it is mentioned explicitly,
  so we get f6 :: forall (k:*) (a:k->*) (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).

Note [No Required PiTyBinder in terms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We don't allow Required foralls for term variables, including pattern
synonyms and data constructors.  Why?  Because then an application
would need a /compulsory/ type argument (possibly without an "@"?),
thus (f Int); and we don't have concrete syntax for that.

We could change this decision, but Required, Named PiTyBinders are rare
anyway.  (Most are Anons.)

However the type of a term can (just about) have a required quantifier;
see Note [Required quantifiers in the type of a term] in GHC.Tc.Gen.Expr.
-}



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

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

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

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

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

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

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

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

mkTyVar :: Name -> Kind -> TyVar
mkTyVar :: Name -> Mult -> Var
mkTyVar Name
name Mult
kind = TyVar { varName :: Name
varName    = Name
name
                          , realUnique :: Int
realUnique = Unique -> Int
getKey (Name -> Unique
nameUnique Name
name)
                          , varType :: Mult
varType  = Mult
kind
                          }

mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar
mkTcTyVar :: Name -> Mult -> TcTyVarDetails -> Var
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 :: Int
realUnique = Unique -> Int
getKey (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 :: Var -> TcTyVarDetails
tcTyVarDetails (TcTyVar { tc_tv_details :: Var -> 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 {})                            = HasCallStack => TcTyVarDetails
vanillaSkolemTvUnk
tcTyVarDetails Var
var = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tcTyVarDetails" (forall a. Outputable a => a -> SDoc
ppr Var
var forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon forall doc. IsLine doc => doc -> doc -> doc
<+> Mult -> SDoc
pprKind (Var -> Mult
tyVarKind Var
var))

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

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

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

idDetails :: Id -> IdDetails
idDetails :: Var -> IdDetails
idDetails (Id { id_details :: Var -> IdDetails
id_details = IdDetails
details }) = IdDetails
details
idDetails Var
other                         = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"idDetails" (forall a. Outputable a => a -> SDoc
ppr Var
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 -> Var
mkGlobalVar IdDetails
details Name
name Mult
ty IdInfo
info
  = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Var
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 -> Var
mkLocalVar IdDetails
details Name
name Mult
w Mult
ty IdInfo
info
  = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Var
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 -> Var
mkCoVar Name
name Mult
ty = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Var
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 -> Var
mkExportedLocalVar IdDetails
details Name
name Mult
ty IdInfo
info
  = Name -> Mult -> Mult -> IdScope -> IdDetails -> IdInfo -> Var
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 -> Var
mk_id Name
name !Mult
w Mult
ty IdScope
scope IdDetails
details IdInfo
info
  = Id { varName :: Name
varName    = Name
name,
         realUnique :: Int
realUnique = Unique -> Int
getKey (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 :: Var -> IdInfo -> Var
lazySetIdInfo Var
id IdInfo
info = Var
id { id_info :: IdInfo
id_info = IdInfo
info }

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

globaliseId :: Id -> Id
-- ^ If it's a local, make it global
globaliseId :: Var -> Var
globaliseId Var
id = Var
id { idScope :: IdScope
idScope = 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 :: Var -> Var
setIdExported id :: Var
id@(Id { idScope :: Var -> IdScope
idScope = LocalId {} }) = Var
id { idScope :: IdScope
idScope = ExportFlag -> IdScope
LocalId ExportFlag
Exported }
setIdExported id :: Var
id@(Id { idScope :: Var -> IdScope
idScope = IdScope
GlobalId })   = Var
id
setIdExported Var
tv                               = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setIdExported" (forall a. Outputable a => a -> SDoc
ppr Var
tv)

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

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


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

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

setIdMult :: Id -> Mult -> Id
setIdMult :: Var -> Mult -> Var
setIdMult Var
id !Mult
r | Var -> Bool
isId Var
id = Var
id { varMult :: Mult
varMult = Mult
r }
                | Bool
otherwise = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setIdMult" (forall a. Outputable a => a -> SDoc
ppr Var
id forall doc. IsLine doc => doc -> doc -> doc
<+> 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 :: Var -> Bool
isTyVar (TyVar {})   = Bool
True
isTyVar (TcTyVar {}) = Bool
True
isTyVar Var
_            = Bool
False

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

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

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

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

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

-- | '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 :: Var -> Bool
isLocalVar Var
v = Bool -> Bool
not (Var -> Bool
isGlobalId Var
v)

isGlobalId :: Var -> Bool
isGlobalId :: Var -> Bool
isGlobalId (Id { idScope :: Var -> IdScope
idScope = IdScope
GlobalId }) = Bool
True
isGlobalId Var
_                           = 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 :: Var -> Bool
mustHaveLocalBinding Var
var = Var -> Bool
isLocalVar Var
var

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