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



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

module GHC.Tc.TyCl.Build (
        buildDataCon,
        buildPatSyn,
        TcMethInfo, MethInfo, buildClass,
        mkNewTyConRhs,
        newImplicitBinder, newTyConRepName
    ) where

import GHC.Prelude

import GHC.Iface.Env
import GHC.Core.FamInstEnv( FamInstEnvs, mkNewTypeCoAxiom )
import GHC.Builtin.Types( isCTupleTyConName, unboxedUnitTy )
import GHC.Core.DataCon
import GHC.Core.PatSyn
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Basic
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Types.Id.Make
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.Type
import GHC.Types.SourceText
import GHC.Tc.Utils.TcType
import GHC.Core.Multiplicity

import GHC.Types.SrcLoc( SrcSpan, noSrcSpan )
import GHC.Tc.Utils.Monad
import GHC.Types.Unique.Supply
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic


mkNewTyConRhs :: Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
-- ^ Monadic because it makes a Name for the coercion TyCon
--   We pass the Name of the parent TyCon, as well as the TyCon itself,
--   because the latter is part of a knot, whereas the former is not.
mkNewTyConRhs :: forall m n. Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
mkNewTyConRhs Name
tycon_name TyCon
tycon DataCon
con
  = do  { Name
co_tycon_name <- Name -> (OccName -> OccName) -> TcRnIf m n Name
forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
tycon_name OccName -> OccName
mkNewTyCoOcc
        ; let nt_ax :: CoAxiom Unbranched
nt_ax = Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
mkNewTypeCoAxiom Name
co_tycon_name TyCon
tycon [TyVar]
etad_tvs [Role]
etad_roles Type
etad_rhs
        ; SDoc -> TcRnIf m n ()
forall m n. SDoc -> TcRnIf m n ()
traceIf (String -> SDoc
text String
"mkNewTyConRhs" SDoc -> SDoc -> SDoc
<+> CoAxiom Unbranched -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiom Unbranched
nt_ax)
        ; AlgTyConRhs -> TcRnIf m n AlgTyConRhs
forall a. a -> IOEnv (Env m n) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NewTyCon { data_con :: DataCon
data_con     = DataCon
con,
                             nt_rhs :: Type
nt_rhs       = Type
rhs_ty,
                             nt_etad_rhs :: ([TyVar], Type)
nt_etad_rhs  = ([TyVar]
etad_tvs, Type
etad_rhs),
                             nt_co :: CoAxiom Unbranched
nt_co        = CoAxiom Unbranched
nt_ax,
                             nt_fixed_rep :: Bool
nt_fixed_rep = (() :: Constraint) => Type -> Bool
Type -> Bool
isFixedRuntimeRepKind Type
res_kind } ) }
                             -- Coreview looks through newtypes with a Nothing
                             -- for nt_co, or uses explicit coercions otherwise
  where
    tvs :: [TyVar]
tvs      = TyCon -> [TyVar]
tyConTyVars TyCon
tycon
    roles :: [Role]
roles    = TyCon -> [Role]
tyConRoles TyCon
tycon
    res_kind :: Type
res_kind = TyCon -> Type
tyConResKind TyCon
tycon
    con_arg_ty :: Type
con_arg_ty = case DataCon -> [Scaled Type]
dataConRepArgTys DataCon
con of
                   [Scaled Type
arg_ty] -> Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
arg_ty
                   [Scaled Type]
tys -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkNewTyConRhs" (DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
con SDoc -> SDoc -> SDoc
<+> [Scaled Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Scaled Type]
tys)
    rhs_ty :: Type
rhs_ty = [TyVar] -> ThetaType -> Type -> Type
(() :: Constraint) => [TyVar] -> ThetaType -> Type -> Type
substTyWith (DataCon -> [TyVar]
dataConUnivTyVars DataCon
con)
                         ([TyVar] -> ThetaType
mkTyVarTys [TyVar]
tvs) Type
con_arg_ty
        -- Instantiate the newtype's RHS with the
        -- type variables from the tycon
        -- NB: a newtype DataCon has a type that must look like
        --        forall tvs.  <arg-ty> -> T tvs
        -- Note that we *can't* use dataConInstOrigArgTys here because
        -- the newtype arising from   class Foo a => Bar a where {}
        -- has a single argument (Foo a) that is a *type class*, so
        -- dataConInstOrigArgTys returns [].

    -- Eta-reduce the newtype
    -- See Note [Newtype eta] in GHC.Core.TyCon
    etad_tvs   :: [TyVar]  -- Matched lazily, so that mkNewTypeCo can
    etad_roles :: [Role]   -- return a TyCon without pulling on rhs_ty
    etad_rhs   :: Type     -- See Note [Tricky iface loop] in GHC.Iface.Load
    ([TyVar]
etad_tvs, [Role]
etad_roles, Type
etad_rhs) = [TyVar] -> [Role] -> Type -> ([TyVar], [Role], Type)
eta_reduce ([TyVar] -> [TyVar]
forall a. [a] -> [a]
reverse [TyVar]
tvs) ([Role] -> [Role]
forall a. [a] -> [a]
reverse [Role]
roles) Type
rhs_ty

    eta_reduce :: [TyVar]       -- Reversed
               -> [Role]        -- also reversed
               -> Type          -- Rhs type
               -> ([TyVar], [Role], Type)  -- Eta-reduced version
                                           -- (tyvars in normal order)
    eta_reduce :: [TyVar] -> [Role] -> Type -> ([TyVar], [Role], Type)
eta_reduce (TyVar
a:[TyVar]
as) (Role
_:[Role]
rs) Type
ty
      | Just (Type
fun, Type
arg) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty
      , Just TyVar
tv <- Type -> Maybe TyVar
getTyVar_maybe Type
arg
      , TyVar
tv TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
a
      , Bool -> Bool
not (TyVar
a TyVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
fun)
      , (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
fun Type -> Type -> Bool
`eqType` (() :: Constraint) => Type -> Type
Type -> Type
typeKind (TyCon -> ThetaType -> Type
mkTyConApp TyCon
tycon ([TyVar] -> ThetaType
mkTyVarTys ([TyVar] -> ThetaType) -> [TyVar] -> ThetaType
forall a b. (a -> b) -> a -> b
$ [TyVar] -> [TyVar]
forall a. [a] -> [a]
reverse [TyVar]
as))
        -- Why this kind-check?  See Note [Newtype eta and homogeneous axioms]
      = [TyVar] -> [Role] -> Type -> ([TyVar], [Role], Type)
eta_reduce [TyVar]
as [Role]
rs Type
fun
    eta_reduce [TyVar]
as [Role]
rs Type
ty = ([TyVar] -> [TyVar]
forall a. [a] -> [a]
reverse [TyVar]
as, [Role] -> [Role]
forall a. [a] -> [a]
reverse [Role]
rs, Type
ty)

{- Note [Newtype eta and homogeneous axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When eta-reducing a newtype, we must be careful to make sure the axiom
is homogeneous.  (That is, the two types related by the axiom must
have the same kind.)  All known proofs of type safety for Core rely on
the homogeneity of axioms, so let's not monkey with that.

It is easy to mistakenly make an inhomogeneous axiom (#19739):
  type T :: forall (a :: Type) -> Type
  newtype T a = MkT (Proxy a)

Can we eta-reduce, thus?
  axT :: T ~ Proxy

No!  Because
   T     :: forall a -> Type
   Proxy :: Type     -> Type

This is inhomogeneous. Hence, we have an extra kind-check in eta_reduce,
to make sure the reducts have the same kind. This is simple, although
perhaps quadratic in complexity, if we eta-reduce many arguments (which
seems vanishingly unlikely in practice).  But NB that the free-variable
check, which immediately precedes the kind check, is also potentially
quadratic.

There are other ways we could do the check (discussion on #19739):

* We could look at the sequence of binders on the newtype and on the
  head of the representation type, and make sure the visibilities on
  the binders match up. This is quite a bit more code, and the reasoning
  is subtler.

* We could, say, do the kind-check at the end and then backtrack until the
  kinds match up. Hard to know whether that's more performant or not.
-}

------------------------------------------------------
buildDataCon :: FamInstEnvs
            -> DataConBangOpts
            -> Name
            -> Bool                     -- Declared infix
            -> TyConRepName
            -> [HsSrcBang]
           -> [FieldLabel]             -- Field labels
           -> [TyVar]                  -- Universals
           -> [TyCoVar]                -- Existentials
           -> [InvisTVBinder]          -- User-written 'TyVarBinder's
           -> [EqSpec]                 -- Equality spec
           -> KnotTied ThetaType       -- Does not include the "stupid theta"
                                       -- or the GADT equalities
           -> [KnotTied (Scaled Type)] -- Arguments
           -> KnotTied Type            -- Result types
           -> KnotTied TyCon           -- Rep tycon
           -> NameEnv ConTag           -- Maps the Name of each DataCon to its
                                       -- ConTag
           -> TcRnIf m n DataCon
-- A wrapper for DataCon.mkDataCon that
--   a) makes the worker Id
--   b) makes the wrapper Id if necessary, including
--      allocating its unique (hence monadic)
buildDataCon :: forall m n.
FamInstEnvs
-> DataConBangOpts
-> Name
-> Bool
-> Name
-> [HsSrcBang]
-> [FieldLabel]
-> [TyVar]
-> [TyVar]
-> [InvisTVBinder]
-> [EqSpec]
-> ThetaType
-> [Scaled Type]
-> Type
-> TyCon
-> NameEnv ConTag
-> TcRnIf m n DataCon
buildDataCon FamInstEnvs
fam_envs DataConBangOpts
dc_bang_opts Name
src_name Bool
declared_infix Name
prom_info [HsSrcBang]
src_bangs
             [FieldLabel]
field_lbls [TyVar]
univ_tvs [TyVar]
ex_tvs [InvisTVBinder]
user_tvbs [EqSpec]
eq_spec ThetaType
ctxt [Scaled Type]
arg_tys Type
res_ty
             TyCon
rep_tycon NameEnv ConTag
tag_map
  = do  { Name
wrap_name <- Name -> (OccName -> OccName) -> TcRnIf m n Name
forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
src_name OccName -> OccName
mkDataConWrapperOcc
        ; Name
work_name <- Name -> (OccName -> OccName) -> TcRnIf m n Name
forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
src_name OccName -> OccName
mkDataConWorkerOcc
        -- This last one takes the name of the data constructor in the source
        -- code, which (for Haskell source anyway) will be in the DataName name
        -- space, and puts it into the VarName name space

        ; SDoc -> TcRnIf m n ()
forall m n. SDoc -> TcRnIf m n ()
traceIf (String -> SDoc
text String
"buildDataCon 1" SDoc -> SDoc -> SDoc
<+> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
src_name)
        ; UniqSupply
us <- TcRnIf m n UniqSupply
forall gbl lcl. TcRnIf gbl lcl UniqSupply
newUniqueSupply
        ; let stupid_ctxt :: ThetaType
stupid_ctxt = TyCon -> ThetaType -> [TyVar] -> ThetaType
mkDataConStupidTheta TyCon
rep_tycon ((Scaled Type -> Type) -> [Scaled Type] -> ThetaType
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
arg_tys) [TyVar]
univ_tvs
              tag :: ConTag
tag = NameEnv ConTag -> Name -> ConTag
forall a. NameEnv a -> Name -> a
lookupNameEnv_NF NameEnv ConTag
tag_map Name
src_name
              -- See Note [Constructor tag allocation], fixes #14657
              data_con :: DataCon
data_con = Name
-> Bool
-> Name
-> [HsSrcBang]
-> [FieldLabel]
-> [TyVar]
-> [TyVar]
-> [InvisTVBinder]
-> [EqSpec]
-> ThetaType
-> [Scaled Type]
-> Type
-> RuntimeRepInfo
-> TyCon
-> ConTag
-> ThetaType
-> TyVar
-> DataConRep
-> DataCon
mkDataCon Name
src_name Bool
declared_infix Name
prom_info
                                   [HsSrcBang]
src_bangs [FieldLabel]
field_lbls
                                   [TyVar]
univ_tvs [TyVar]
ex_tvs [InvisTVBinder]
user_tvbs [EqSpec]
eq_spec ThetaType
ctxt
                                   [Scaled Type]
arg_tys Type
res_ty RuntimeRepInfo
NoRRI TyCon
rep_tycon ConTag
tag
                                   ThetaType
stupid_ctxt TyVar
dc_wrk DataConRep
dc_rep
              dc_wrk :: TyVar
dc_wrk = Name -> DataCon -> TyVar
mkDataConWorkId Name
work_name DataCon
data_con
              dc_rep :: DataConRep
dc_rep = UniqSupply -> UniqSM DataConRep -> DataConRep
forall a. UniqSupply -> UniqSM a -> a
initUs_ UniqSupply
us (DataConBangOpts
-> FamInstEnvs -> Name -> DataCon -> UniqSM DataConRep
mkDataConRep DataConBangOpts
dc_bang_opts FamInstEnvs
fam_envs Name
wrap_name DataCon
data_con)

        ; SDoc -> TcRnIf m n ()
forall m n. SDoc -> TcRnIf m n ()
traceIf (String -> SDoc
text String
"buildDataCon 2" SDoc -> SDoc -> SDoc
<+> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
src_name)
        ; DataCon -> TcRnIf m n DataCon
forall a. a -> IOEnv (Env m n) a
forall (m :: * -> *) a. Monad m => a -> m a
return DataCon
data_con }


-- The stupid context for a data constructor should be limited to
-- the type variables mentioned in the arg_tys
-- ToDo: Or functionally dependent on?
--       This whole stupid theta thing is, well, stupid.
--
-- See Note [The stupid context] in GHC.Core.DataCon.
mkDataConStupidTheta :: TyCon -> [Type] -> [TyVar] -> [PredType]
mkDataConStupidTheta :: TyCon -> ThetaType -> [TyVar] -> ThetaType
mkDataConStupidTheta TyCon
tycon ThetaType
arg_tys [TyVar]
univ_tvs
  | ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
stupid_theta = []      -- The common case
  | Bool
otherwise         = (Type -> Bool) -> ThetaType -> ThetaType
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
in_arg_tys ThetaType
stupid_theta
  where
    tc_subst :: TCvSubst
tc_subst     = [TyVar] -> ThetaType -> TCvSubst
(() :: Constraint) => [TyVar] -> ThetaType -> TCvSubst
zipTvSubst (TyCon -> [TyVar]
tyConTyVars TyCon
tycon)
                              ([TyVar] -> ThetaType
mkTyVarTys [TyVar]
univ_tvs)
    stupid_theta :: ThetaType
stupid_theta = (() :: Constraint) => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
tc_subst (TyCon -> ThetaType
tyConStupidTheta TyCon
tycon)
        -- Start by instantiating the master copy of the
        -- stupid theta, taken from the TyCon

    arg_tyvars :: VarSet
arg_tyvars      = ThetaType -> VarSet
tyCoVarsOfTypes ThetaType
arg_tys
    in_arg_tys :: Type -> Bool
in_arg_tys Type
pred = Type -> VarSet
tyCoVarsOfType Type
pred VarSet -> VarSet -> Bool
`intersectsVarSet` VarSet
arg_tyvars


------------------------------------------------------
buildPatSyn :: Name -> Bool
            -> PatSynMatcher -> PatSynBuilder
            -> ([InvisTVBinder], ThetaType) -- ^ Univ and req
            -> ([InvisTVBinder], ThetaType) -- ^ Ex and prov
            -> [FRRType]                    -- ^ Argument types
            -> Type                         -- ^ Result type
            -> [FieldLabel]                 -- ^ Field labels for
                                            --   a record pattern synonym
            -> PatSyn
buildPatSyn :: Name
-> Bool
-> PatSynMatcher
-> PatSynBuilder
-> ([InvisTVBinder], ThetaType)
-> ([InvisTVBinder], ThetaType)
-> ThetaType
-> Type
-> [FieldLabel]
-> PatSyn
buildPatSyn Name
src_name Bool
declared_infix matcher :: PatSynMatcher
matcher@(Name
_, Type
matcher_ty,Bool
_) PatSynBuilder
builder
            ([InvisTVBinder]
univ_tvs, ThetaType
req_theta) ([InvisTVBinder]
ex_tvs, ThetaType
prov_theta) ThetaType
arg_tys
            Type
pat_ty [FieldLabel]
field_labels
  = -- The assertion checks that the matcher is
    -- compatible with the pattern synonym
    Bool -> SDoc -> PatSyn -> PatSyn
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ [InvisTVBinder]
univ_tvs [InvisTVBinder] -> [TyVar] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [TyVar]
univ_tvs1
                   , [InvisTVBinder]
ex_tvs [InvisTVBinder] -> [TyVar] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [TyVar]
ex_tvs1
                   , Type
pat_ty Type -> Type -> Bool
`eqType` (() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
pat_ty1)
                   , ThetaType
prov_theta ThetaType -> ThetaType -> Bool
`eqTypes` (() :: Constraint) => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst ThetaType
prov_theta1
                   , ThetaType
req_theta ThetaType -> ThetaType -> Bool
`eqTypes` (() :: Constraint) => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst ThetaType
req_theta1
                   , ThetaType -> ThetaType -> Bool
compareArgTys ThetaType
arg_tys ((() :: Constraint) => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst ((Scaled Type -> Type) -> [Scaled Type] -> ThetaType
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
arg_tys1))
                   ])
              ([SDoc] -> SDoc
vcat [ [InvisTVBinder] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InvisTVBinder]
univ_tvs SDoc -> SDoc -> SDoc
<+> SDoc
twiddle SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
univ_tvs1
                    , [InvisTVBinder] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InvisTVBinder]
ex_tvs SDoc -> SDoc -> SDoc
<+> SDoc
twiddle SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
ex_tvs1
                    , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pat_ty SDoc -> SDoc -> SDoc
<+> SDoc
twiddle SDoc -> SDoc -> SDoc
<+> Scaled Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Scaled Type
pat_ty1
                    , ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
prov_theta SDoc -> SDoc -> SDoc
<+> SDoc
twiddle SDoc -> SDoc -> SDoc
<+> ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
prov_theta1
                    , ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
req_theta SDoc -> SDoc -> SDoc
<+> SDoc
twiddle SDoc -> SDoc -> SDoc
<+> ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
req_theta1
                    , ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
arg_tys SDoc -> SDoc -> SDoc
<+> SDoc
twiddle SDoc -> SDoc -> SDoc
<+> [Scaled Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Scaled Type]
arg_tys1]) (PatSyn -> PatSyn) -> PatSyn -> PatSyn
forall a b. (a -> b) -> a -> b
$
    Name
-> Bool
-> ([InvisTVBinder], ThetaType)
-> ([InvisTVBinder], ThetaType)
-> ThetaType
-> Type
-> PatSynMatcher
-> PatSynBuilder
-> [FieldLabel]
-> PatSyn
mkPatSyn Name
src_name Bool
declared_infix
             ([InvisTVBinder]
univ_tvs, ThetaType
req_theta) ([InvisTVBinder]
ex_tvs, ThetaType
prov_theta)
             ThetaType
arg_tys Type
pat_ty
             PatSynMatcher
matcher PatSynBuilder
builder [FieldLabel]
field_labels
  where
    ((TyVar
_:TyVar
_:[TyVar]
univ_tvs1), ThetaType
req_theta1, Type
tau) = Type -> ([TyVar], ThetaType, Type)
tcSplitSigmaTy (Type -> ([TyVar], ThetaType, Type))
-> Type -> ([TyVar], ThetaType, Type)
forall a b. (a -> b) -> a -> b
$ Type
matcher_ty
    ([Scaled Type
pat_ty1, Scaled Type
cont_sigma, Scaled Type
_], Type
_)      = Type -> ([Scaled Type], Type)
tcSplitFunTys Type
tau
    ([TyVar]
ex_tvs1, ThetaType
prov_theta1, Type
cont_tau)   = Type -> ([TyVar], ThetaType, Type)
tcSplitSigmaTy (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
cont_sigma)
    ([Scaled Type]
arg_tys1, Type
_) = (Type -> ([Scaled Type], Type)
tcSplitFunTys Type
cont_tau)
    twiddle :: SDoc
twiddle = Char -> SDoc
char Char
'~'
    subst :: TCvSubst
subst = [TyVar] -> ThetaType -> TCvSubst
(() :: Constraint) => [TyVar] -> ThetaType -> TCvSubst
zipTvSubst ([TyVar]
univ_tvs1 [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
ex_tvs1)
                       ([TyVar] -> ThetaType
mkTyVarTys ([InvisTVBinder] -> [TyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars ([InvisTVBinder]
univ_tvs [InvisTVBinder] -> [InvisTVBinder] -> [InvisTVBinder]
forall a. [a] -> [a] -> [a]
++ [InvisTVBinder]
ex_tvs)))

    -- For a nullary pattern synonym we add a single (# #) argument to the
    -- matcher to preserve laziness in the case of unlifted types.
    -- See #12746
    compareArgTys :: [Type] -> [Type] -> Bool
    compareArgTys :: ThetaType -> ThetaType -> Bool
compareArgTys [] [Type
x] = Type
x Type -> Type -> Bool
`eqType` Type
unboxedUnitTy
    compareArgTys ThetaType
arg_tys ThetaType
matcher_arg_tys = ThetaType
arg_tys ThetaType -> ThetaType -> Bool
`eqTypes` ThetaType
matcher_arg_tys


------------------------------------------------------
type TcMethInfo = MethInfo  -- this variant needs zonking
type MethInfo       -- A temporary intermediate, to communicate
                    -- between tcClassSigs and buildClass.
  = ( Name   -- Name of the class op
    , Type   -- Type of the class op
    , Maybe (DefMethSpec (SrcSpan, Type)))
         -- Nothing                    => no default method
         --
         -- Just VanillaDM             => There is an ordinary
         --                               polymorphic default method
         --
         -- Just (GenericDM (loc, ty)) => There is a generic default metho
         --                               Here is its type, and the location
         --                               of the type signature
         --    We need that location /only/ to attach it to the
         --    generic default method's Name; and we need /that/
         --    only to give the right location of an ambiguity error
         --    for the generic default method, spat out by checkValidClass

buildClass :: Name  -- Name of the class/tycon (they have the same Name)
           -> [TyConBinder]                -- Of the tycon
           -> [Role]
           -> [FunDep TyVar]               -- Functional dependencies
           -- Super classes, associated types, method info, minimal complete def.
           -- This is Nothing if the class is abstract.
           -> Maybe (KnotTied ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
           -> TcRnIf m n Class

buildClass :: forall m n.
Name
-> [TyConBinder]
-> [Role]
-> [FunDep TyVar]
-> Maybe
     (ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
-> TcRnIf m n Class
buildClass Name
tycon_name [TyConBinder]
binders [Role]
roles [FunDep TyVar]
fds Maybe
  (ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
Nothing
  = (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
forall a env. (a -> IOEnv env a) -> IOEnv env a
fixM  ((Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class)
-> (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
forall a b. (a -> b) -> a -> b
$ \ Class
rec_clas ->       -- Only name generation inside loop
    do  { SDoc -> TcRnIf m n ()
forall m n. SDoc -> TcRnIf m n ()
traceIf (String -> SDoc
text String
"buildClass")

        ; Name
tc_rep_name  <- Name -> TcRnIf m n Name
forall gbl lcl. Name -> TcRnIf gbl lcl Name
newTyConRepName Name
tycon_name
        ; let univ_tvs :: [TyVar]
univ_tvs = [TyConBinder] -> [TyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyConBinder]
binders
              tycon :: TyCon
tycon = Name
-> [TyConBinder] -> [Role] -> AlgTyConRhs -> Class -> Name -> TyCon
mkClassTyCon Name
tycon_name [TyConBinder]
binders [Role]
roles
                                   AlgTyConRhs
AbstractTyCon
                                   Class
rec_clas Name
tc_rep_name
              result :: Class
result = Name -> [TyVar] -> [FunDep TyVar] -> TyCon -> Class
mkAbstractClass Name
tycon_name [TyVar]
univ_tvs [FunDep TyVar]
fds TyCon
tycon
        ; SDoc -> TcRnIf m n ()
forall m n. SDoc -> TcRnIf m n ()
traceIf (String -> SDoc
text String
"buildClass" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon)
        ; Class -> IOEnv (Env m n) Class
forall a. a -> IOEnv (Env m n) a
forall (m :: * -> *) a. Monad m => a -> m a
return Class
result }

buildClass Name
tycon_name [TyConBinder]
binders [Role]
roles [FunDep TyVar]
fds
           (Just (ThetaType
sc_theta, [ClassATItem]
at_items, [KnotTied MethInfo]
sig_stuff, ClassMinimalDef
mindef))
  = (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
forall a env. (a -> IOEnv env a) -> IOEnv env a
fixM  ((Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class)
-> (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
forall a b. (a -> b) -> a -> b
$ \ Class
rec_clas ->       -- Only name generation inside loop
    do  { SDoc -> TcRnIf m n ()
forall m n. SDoc -> TcRnIf m n ()
traceIf (String -> SDoc
text String
"buildClass")

        ; Name
datacon_name <- Name -> (OccName -> OccName) -> TcRnIf m n Name
forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
tycon_name OccName -> OccName
mkClassDataConOcc
        ; Name
tc_rep_name  <- Name -> TcRnIf m n Name
forall gbl lcl. Name -> TcRnIf gbl lcl Name
newTyConRepName Name
tycon_name

        ; [ClassOpItem]
op_items <- (KnotTied MethInfo -> IOEnv (Env m n) ClassOpItem)
-> [KnotTied MethInfo] -> IOEnv (Env m n) [ClassOpItem]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Class -> KnotTied MethInfo -> IOEnv (Env m n) ClassOpItem
forall n m. Class -> KnotTied MethInfo -> TcRnIf n m ClassOpItem
mk_op_item Class
rec_clas) [KnotTied MethInfo]
sig_stuff
                        -- Build the selector id and default method id

              -- Make selectors for the superclasses
        ; [Name]
sc_sel_names <- (ConTag -> TcRnIf m n Name) -> [ConTag] -> IOEnv (Env m n) [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM  (Name -> (OccName -> OccName) -> TcRnIf m n Name
forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
tycon_name ((OccName -> OccName) -> TcRnIf m n Name)
-> (ConTag -> OccName -> OccName) -> ConTag -> TcRnIf m n Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConTag -> OccName -> OccName
mkSuperDictSelOcc)
                                (ThetaType -> [ConTag] -> [ConTag]
forall b a. [b] -> [a] -> [a]
takeList ThetaType
sc_theta [ConTag
fIRST_TAG..])
        ; let sc_sel_ids :: [TyVar]
sc_sel_ids = [ Name -> Class -> TyVar
mkDictSelId Name
sc_name Class
rec_clas
                           | Name
sc_name <- [Name]
sc_sel_names]
              -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we
              -- can construct names for the selectors. Thus
              --      class (C a, C b) => D a b where ...
              -- gives superclass selectors
              --      D_sc1, D_sc2
              -- (We used to call them D_C, but now we can have two different
              --  superclasses both called C!)

        ; let use_newtype :: Bool
use_newtype = ThetaType -> Bool
forall a. [a] -> Bool
isSingleton ThetaType
arg_tys
                -- Use a newtype if the data constructor
                --   (a) has exactly one value field
                --       i.e. exactly one operation or superclass taken together
                --   (b) that value is of lifted type (which they always are, because
                --       we box equality superclasses)
                -- See Note [Class newtypes and equality predicates]

                -- We treat the dictionary superclasses as ordinary arguments.
                -- That means that in the case of
                --     class C a => D a
                -- we don't get a newtype with no arguments!
              args :: [Name]
args       = [Name]
sc_sel_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
op_names
              op_tys :: ThetaType
op_tys     = [Type
ty | (Name
_,Type
ty,Maybe (DefMethSpec (SrcSpan, Type))
_) <- [KnotTied MethInfo]
sig_stuff]
              op_names :: [Name]
op_names   = [Name
op | (Name
op,Type
_,Maybe (DefMethSpec (SrcSpan, Type))
_) <- [KnotTied MethInfo]
sig_stuff]
              arg_tys :: ThetaType
arg_tys    = ThetaType
sc_theta ThetaType -> ThetaType -> ThetaType
forall a. [a] -> [a] -> [a]
++ ThetaType
op_tys
              rec_tycon :: TyCon
rec_tycon  = Class -> TyCon
classTyCon Class
rec_clas
              univ_bndrs :: [InvisTVBinder]
univ_bndrs = [TyConBinder] -> [InvisTVBinder]
tyConInvisTVBinders [TyConBinder]
binders
              univ_tvs :: [TyVar]
univ_tvs   = [InvisTVBinder] -> [TyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [InvisTVBinder]
univ_bndrs
              bang_opts :: DataConBangOpts
bang_opts  = [HsImplBang] -> DataConBangOpts
FixedBangOpts ((Name -> HsImplBang) -> [Name] -> [HsImplBang]
forall a b. (a -> b) -> [a] -> [b]
map (HsImplBang -> Name -> HsImplBang
forall a b. a -> b -> a
const HsImplBang
HsLazy) [Name]
args)

        ; Name
rep_nm   <- Name -> TcRnIf m n Name
forall gbl lcl. Name -> TcRnIf gbl lcl Name
newTyConRepName Name
datacon_name
        ; DataCon
dict_con <- FamInstEnvs
-> DataConBangOpts
-> Name
-> Bool
-> Name
-> [HsSrcBang]
-> [FieldLabel]
-> [TyVar]
-> [TyVar]
-> [InvisTVBinder]
-> [EqSpec]
-> ThetaType
-> [Scaled Type]
-> Type
-> TyCon
-> NameEnv ConTag
-> TcRnIf m n DataCon
forall m n.
FamInstEnvs
-> DataConBangOpts
-> Name
-> Bool
-> Name
-> [HsSrcBang]
-> [FieldLabel]
-> [TyVar]
-> [TyVar]
-> [InvisTVBinder]
-> [EqSpec]
-> ThetaType
-> [Scaled Type]
-> Type
-> TyCon
-> NameEnv ConTag
-> TcRnIf m n DataCon
buildDataCon (String -> FamInstEnvs
forall a. String -> a
panic String
"buildClass: FamInstEnvs")
                                   DataConBangOpts
bang_opts
                                   Name
datacon_name
                                   Bool
False        -- Not declared infix
                                   Name
rep_nm
                                   ((Name -> HsSrcBang) -> [Name] -> [HsSrcBang]
forall a b. (a -> b) -> [a] -> [b]
map (HsSrcBang -> Name -> HsSrcBang
forall a b. a -> b -> a
const HsSrcBang
no_bang) [Name]
args)
                                   [{- No fields -}]
                                   [TyVar]
univ_tvs
                                   [{- no existentials -}]
                                   [InvisTVBinder]
univ_bndrs
                                   [{- No GADT equalities -}]
                                   [{- No theta -}]
                                   ((Type -> Scaled Type) -> ThetaType -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Scaled Type
forall a. a -> Scaled a
unrestricted ThetaType
arg_tys) -- type classes are unrestricted
                                   (TyCon -> ThetaType -> Type
mkTyConApp TyCon
rec_tycon ([TyVar] -> ThetaType
mkTyVarTys [TyVar]
univ_tvs))
                                   TyCon
rec_tycon
                                   (TyCon -> NameEnv ConTag
mkTyConTagMap TyCon
rec_tycon)

        ; AlgTyConRhs
rhs <- case () of
                  ()
_ | Bool
use_newtype
                    -> Name -> TyCon -> DataCon -> IOEnv (Env m n) AlgTyConRhs
forall m n. Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
mkNewTyConRhs Name
tycon_name TyCon
rec_tycon DataCon
dict_con
                    | Name -> Bool
isCTupleTyConName Name
tycon_name
                    -> AlgTyConRhs -> IOEnv (Env m n) AlgTyConRhs
forall a. a -> IOEnv (Env m n) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TupleTyCon { data_con :: DataCon
data_con = DataCon
dict_con
                                          , tup_sort :: TupleSort
tup_sort = TupleSort
ConstraintTuple })
                    | Bool
otherwise
                    -> AlgTyConRhs -> IOEnv (Env m n) AlgTyConRhs
forall a. a -> IOEnv (Env m n) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DataCon] -> AlgTyConRhs
mkDataTyConRhs [DataCon
dict_con])

        ; let { tycon :: TyCon
tycon = Name
-> [TyConBinder] -> [Role] -> AlgTyConRhs -> Class -> Name -> TyCon
mkClassTyCon Name
tycon_name [TyConBinder]
binders [Role]
roles
                                     AlgTyConRhs
rhs Class
rec_clas Name
tc_rep_name
                -- A class can be recursive, and in the case of newtypes
                -- this matters.  For example
                --      class C a where { op :: C b => a -> b -> Int }
                -- Because C has only one operation, it is represented by
                -- a newtype, and it should be a *recursive* newtype.
                -- [If we don't make it a recursive newtype, we'll expand the
                -- newtype like a synonym, but that will lead to an infinite
                -- type]

              ; result :: Class
result = Name
-> [TyVar]
-> [FunDep TyVar]
-> ThetaType
-> [TyVar]
-> [ClassATItem]
-> [ClassOpItem]
-> ClassMinimalDef
-> TyCon
-> Class
mkClass Name
tycon_name [TyVar]
univ_tvs [FunDep TyVar]
fds
                                 ThetaType
sc_theta [TyVar]
sc_sel_ids [ClassATItem]
at_items
                                 [ClassOpItem]
op_items ClassMinimalDef
mindef TyCon
tycon
              }
        ; SDoc -> TcRnIf m n ()
forall m n. SDoc -> TcRnIf m n ()
traceIf (String -> SDoc
text String
"buildClass" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon)
        ; Class -> IOEnv (Env m n) Class
forall a. a -> IOEnv (Env m n) a
forall (m :: * -> *) a. Monad m => a -> m a
return Class
result }
  where
    no_bang :: HsSrcBang
no_bang = SourceText -> SrcUnpackedness -> SrcStrictness -> HsSrcBang
HsSrcBang SourceText
NoSourceText SrcUnpackedness
NoSrcUnpack SrcStrictness
NoSrcStrict

    mk_op_item :: Class -> TcMethInfo -> TcRnIf n m ClassOpItem
    mk_op_item :: forall n m. Class -> KnotTied MethInfo -> TcRnIf n m ClassOpItem
mk_op_item Class
rec_clas (Name
op_name, Type
_, Maybe (DefMethSpec (SrcSpan, Type))
dm_spec)
      = do { Maybe (Name, DefMethSpec Type)
dm_info <- Name
-> Maybe (DefMethSpec (SrcSpan, Type))
-> TcRnIf n m (Maybe (Name, DefMethSpec Type))
forall n m.
Name
-> Maybe (DefMethSpec (SrcSpan, Type))
-> TcRnIf n m (Maybe (Name, DefMethSpec Type))
mk_dm_info Name
op_name Maybe (DefMethSpec (SrcSpan, Type))
dm_spec
           ; ClassOpItem -> TcRnIf n m ClassOpItem
forall a. a -> IOEnv (Env n m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Class -> TyVar
mkDictSelId Name
op_name Class
rec_clas, Maybe (Name, DefMethSpec Type)
dm_info) }

    mk_dm_info :: Name -> Maybe (DefMethSpec (SrcSpan, Type))
               -> TcRnIf n m (Maybe (Name, DefMethSpec Type))
    mk_dm_info :: forall n m.
Name
-> Maybe (DefMethSpec (SrcSpan, Type))
-> TcRnIf n m (Maybe (Name, DefMethSpec Type))
mk_dm_info Name
_ Maybe (DefMethSpec (SrcSpan, Type))
Nothing
      = Maybe (Name, DefMethSpec Type)
-> IOEnv (Env n m) (Maybe (Name, DefMethSpec Type))
forall a. a -> IOEnv (Env n m) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Name, DefMethSpec Type)
forall a. Maybe a
Nothing
    mk_dm_info Name
op_name (Just DefMethSpec (SrcSpan, Type)
VanillaDM)
      = do { Name
dm_name <- Name -> (OccName -> OccName) -> TcRnIf n m Name
forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
op_name OccName -> OccName
mkDefaultMethodOcc
           ; Maybe (Name, DefMethSpec Type)
-> IOEnv (Env n m) (Maybe (Name, DefMethSpec Type))
forall a. a -> IOEnv (Env n m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, DefMethSpec Type) -> Maybe (Name, DefMethSpec Type)
forall a. a -> Maybe a
Just (Name
dm_name, DefMethSpec Type
forall ty. DefMethSpec ty
VanillaDM)) }
    mk_dm_info Name
op_name (Just (GenericDM (SrcSpan
loc, Type
dm_ty)))
      = do { Name
dm_name <- Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf n m Name
forall m n.
Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
newImplicitBinderLoc Name
op_name OccName -> OccName
mkDefaultMethodOcc SrcSpan
loc
           ; Maybe (Name, DefMethSpec Type)
-> IOEnv (Env n m) (Maybe (Name, DefMethSpec Type))
forall a. a -> IOEnv (Env n m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, DefMethSpec Type) -> Maybe (Name, DefMethSpec Type)
forall a. a -> Maybe a
Just (Name
dm_name, Type -> DefMethSpec Type
forall ty. ty -> DefMethSpec ty
GenericDM Type
dm_ty)) }

{-
Note [Class newtypes and equality predicates]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
        class (a ~ F b) => C a b where
          op :: a -> b

We cannot represent this by a newtype, even though it's not
existential, because there are two value fields (the equality
predicate and op. See #2238

Moreover,
          class (a ~ F b) => C a b where {}
Here we can't use a newtype either, even though there is only
one field, because equality predicates are unboxed, and classes
are boxed.
-}

newImplicitBinder :: Name                       -- Base name
                  -> (OccName -> OccName)       -- Occurrence name modifier
                  -> TcRnIf m n Name            -- Implicit name
-- Called in GHC.Tc.TyCl.Build to allocate the implicit binders of type/class decls
-- For source type/class decls, this is the first occurrence
-- For iface ones, GHC.Iface.Load has already allocated a suitable name in the cache
newImplicitBinder :: forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
base_name OccName -> OccName
mk_sys_occ
  = Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
forall m n.
Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
newImplicitBinderLoc Name
base_name OccName -> OccName
mk_sys_occ (Name -> SrcSpan
nameSrcSpan Name
base_name)

newImplicitBinderLoc :: Name                       -- Base name
                     -> (OccName -> OccName)       -- Occurrence name modifier
                     -> SrcSpan
                     -> TcRnIf m n Name            -- Implicit name
-- Just the same, but lets you specify the SrcSpan
newImplicitBinderLoc :: forall m n.
Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
newImplicitBinderLoc Name
base_name OccName -> OccName
mk_sys_occ SrcSpan
loc
  | Just Module
mod <- Name -> Maybe Module
nameModule_maybe Name
base_name
  = Module -> OccName -> SrcSpan -> TcRnIf m n Name
forall a b. Module -> OccName -> SrcSpan -> TcRnIf a b Name
newGlobalBinder Module
mod OccName
occ SrcSpan
loc
  | Bool
otherwise           -- When typechecking a [d| decl bracket |],
                        -- TH generates types, classes etc with Internal names,
                        -- so we follow suit for the implicit binders
  = do  { Unique
uniq <- TcRnIf m n Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
        ; Name -> TcRnIf m n Name
forall a. a -> IOEnv (Env m n) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
uniq OccName
occ SrcSpan
loc) }
  where
    occ :: OccName
occ = OccName -> OccName
mk_sys_occ (Name -> OccName
nameOccName Name
base_name)

-- | Make the 'TyConRepName' for this 'TyCon'
newTyConRepName :: Name -> TcRnIf gbl lcl TyConRepName
newTyConRepName :: forall gbl lcl. Name -> TcRnIf gbl lcl Name
newTyConRepName Name
tc_name
  | Just Module
mod <- Name -> Maybe Module
nameModule_maybe Name
tc_name
  , (Module
mod, OccName
occ) <- Module -> OccName -> (Module, OccName)
tyConRepModOcc Module
mod (Name -> OccName
nameOccName Name
tc_name)
  = Module -> OccName -> SrcSpan -> TcRnIf gbl lcl Name
forall a b. Module -> OccName -> SrcSpan -> TcRnIf a b Name
newGlobalBinder Module
mod OccName
occ SrcSpan
noSrcSpan
  | Bool
otherwise
  = Name -> (OccName -> OccName) -> TcRnIf gbl lcl Name
forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
newImplicitBinder Name
tc_name OccName -> OccName
mkTyConRepOcc