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

-}

{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}

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

module GHC.Tc.Utils.Instantiate (
       topSkolemise,
       topInstantiate, topInstantiateInferred,
       instCall, instDFunType, instStupidTheta, instTyVarsWith,
       newWanted, newWanteds,

       tcInstType, tcInstTypeBndrs,
       tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
       tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,

       freshenTyVarBndrs, freshenCoVarBndrsX,

       tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,

       newOverloadedLit, mkOverLit,

       newClsInst,
       tcGetInsts, tcGetInstEnvs, getOverlapFlag,
       tcExtendLocalInstEnv,
       instCallConstraints, newMethodFromName,
       tcSyntaxName,

       -- Simple functions over evidence variables
       tyCoVarsOfWC,
       tyCoVarsOfCt, tyCoVarsOfCts,
    ) where

#include "HsVersions.h"

import GHC.Prelude

import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
import {-# SOURCE #-}   GHC.Tc.Utils.Unify( unifyType, unifyKind )

import GHC.Types.Basic ( IntegralLit(..), SourceText(..) )
import GHC.Hs
import GHC.Tc.Utils.Zonk
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Env
import GHC.Tc.Types.Evidence
import GHC.Core.InstEnv
import GHC.Builtin.Types  ( heqDataCon, eqDataCon, integerTyConName )
import GHC.Core    ( isOrphan )
import GHC.Tc.Instance.FunDeps
import GHC.Tc.Utils.TcMType
import GHC.Core.Type
import GHC.Core.Multiplicity
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr ( debugPprType )
import GHC.Tc.Utils.TcType
import GHC.Driver.Types
import GHC.Core.Class( Class )
import GHC.Types.Id.Make( mkDictFunId )
import GHC.Core( Expr(..) )  -- For the Coercion constructor
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Var
import GHC.Core.DataCon
import GHC.Types.Var.Env
import GHC.Builtin.Names
import GHC.Types.SrcLoc as SrcLoc
import GHC.Driver.Session
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Types.Basic ( TypeOrKind(..) )
import qualified GHC.LanguageExtensions as LangExt

import Data.List ( sortBy, mapAccumL )
import Control.Monad( unless )
import Data.Function ( on )

{-
************************************************************************
*                                                                      *
                Creating and emittind constraints
*                                                                      *
************************************************************************
-}

newMethodFromName
  :: CtOrigin              -- ^ why do we need this?
  -> Name                  -- ^ name of the method
  -> [TcRhoType]           -- ^ types with which to instantiate the class
  -> TcM (HsExpr GhcTc)
-- ^ Used when 'Name' is the wired-in name for a wired-in class method,
-- so the caller knows its type for sure, which should be of form
--
-- > forall a. C a => <blah>
--
-- 'newMethodFromName' is supposed to instantiate just the outer
-- type variable and constraint

newMethodFromName :: CtOrigin -> Name -> ThetaType -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
origin Name
name ThetaType
ty_args
  = do { DFunId
id <- Name -> TcM DFunId
tcLookupId Name
name
              -- Use tcLookupId not tcLookupGlobalId; the method is almost
              -- always a class op, but with -XRebindableSyntax GHC is
              -- meant to find whatever thing is in scope, and that may
              -- be an ordinary function.

       ; let ty :: Type
ty = HasDebugCallStack => Type -> ThetaType -> Type
Type -> ThetaType -> Type
piResultTys (DFunId -> Type
idType DFunId
id) ThetaType
ty_args
             (ThetaType
theta, Type
_caller_knows_this) = Type -> (ThetaType, Type)
tcSplitPhiTy Type
ty
       ; HsWrapper
wrap <- ASSERT( not (isForAllTy ty) && isSingleton theta )
                 CtOrigin
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCall CtOrigin
origin ThetaType
ty_args ThetaType
theta

       ; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap HsWrapper
wrap (XVar GhcTc -> Located (IdP GhcTc) -> HsExpr GhcTc
forall p. XVar p -> Located (IdP p) -> HsExpr p
HsVar NoExtField
XVar GhcTc
noExtField (DFunId -> Located DFunId
forall e. e -> Located e
noLoc DFunId
id))) }

{-
************************************************************************
*                                                                      *
         Instantiation and skolemisation
*                                                                      *
************************************************************************

Note [Skolemisation]
~~~~~~~~~~~~~~~~~~~~
topSkolemise decomposes and skolemises a type, returning a type
with no top level foralls or (=>)

Examples:

  topSkolemise (forall a. Ord a => a -> a)
    =  ( wp, [a], [d:Ord a], a->a )
    where wp = /\a. \(d:Ord a). <hole> a d

  topSkolemise  (forall a. Ord a => forall b. Eq b => a->b->b)
    =  ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b )
    where wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2

This second example is the reason for the recursive 'go'
function in topSkolemise: we must remove successive layers
of foralls and (=>).

In general,
  if      topSkolemise ty = (wrap, tvs, evs, rho)
    and   e :: rho
  then    wrap e :: ty
    and   'wrap' binds {tvs, evs}

-}

topSkolemise :: TcSigmaType
             -> TcM ( HsWrapper
                    , [(Name,TyVar)]     -- All skolemised variables
                    , [EvVar]            -- All "given"s
                    , TcRhoType )
-- See Note [Skolemisation]
topSkolemise :: Type -> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
topSkolemise Type
ty
  = TCvSubst
-> HsWrapper
-> [(Name, DFunId)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
go TCvSubst
init_subst HsWrapper
idHsWrapper [] [] Type
ty
  where
    init_subst :: TCvSubst
init_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty))

    -- Why recursive?  See Note [Skolemisation]
    go :: TCvSubst
-> HsWrapper
-> [(Name, DFunId)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
go TCvSubst
subst HsWrapper
wrap [(Name, DFunId)]
tv_prs [DFunId]
ev_vars Type
ty
      | ([DFunId]
tvs, ThetaType
theta, Type
inner_ty) <- Type -> ([DFunId], ThetaType, Type)
tcSplitSigmaTy Type
ty
      , Bool -> Bool
not ([DFunId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DFunId]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
      = do { (TCvSubst
subst', [DFunId]
tvs1) <- TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsX TCvSubst
subst [DFunId]
tvs
           ; [DFunId]
ev_vars1       <- ThetaType -> TcM [DFunId]
newEvVars (HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst' ThetaType
theta)
           ; TCvSubst
-> HsWrapper
-> [(Name, DFunId)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
go TCvSubst
subst'
                (HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> [DFunId] -> HsWrapper
mkWpTyLams [DFunId]
tvs1 HsWrapper -> HsWrapper -> HsWrapper
<.> [DFunId] -> HsWrapper
mkWpLams [DFunId]
ev_vars1)
                ([(Name, DFunId)]
tv_prs [(Name, DFunId)] -> [(Name, DFunId)] -> [(Name, DFunId)]
forall a. [a] -> [a] -> [a]
++ ((DFunId -> Name) -> [DFunId] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DFunId -> Name
tyVarName [DFunId]
tvs [Name] -> [DFunId] -> [(Name, DFunId)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [DFunId]
tvs1))
                ([DFunId]
ev_vars [DFunId] -> [DFunId] -> [DFunId]
forall a. [a] -> [a] -> [a]
++ [DFunId]
ev_vars1)
                Type
inner_ty }

      | Bool
otherwise
      = (HsWrapper, [(Name, DFunId)], [DFunId], Type)
-> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap, [(Name, DFunId)]
tv_prs, [DFunId]
ev_vars, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
ty)
        -- substTy is a quick no-op on an empty substitution

-- | Instantiate all outer type variables
-- and any context. Never looks through arrows.
topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
-- if    topInstantiate ty = (wrap, rho)
-- and   e :: ty
-- then  wrap e :: rho  (that is, wrap :: ty "->" rho)
-- NB: always returns a rho-type, with no top-level forall or (=>)
topInstantiate :: CtOrigin -> Type -> TcM (HsWrapper, Type)
topInstantiate = Bool -> CtOrigin -> Type -> TcM (HsWrapper, Type)
top_instantiate Bool
True

-- | Instantiate all outer 'Inferred' binders
-- and any context. Never looks through arrows or specified type variables.
-- Used for visible type application.
topInstantiateInferred :: CtOrigin -> TcSigmaType
                       -> TcM (HsWrapper, TcSigmaType)
-- if    topInstantiate ty = (wrap, rho)
-- and   e :: ty
-- then  wrap e :: rho
-- NB: may return a sigma-type
topInstantiateInferred :: CtOrigin -> Type -> TcM (HsWrapper, Type)
topInstantiateInferred = Bool -> CtOrigin -> Type -> TcM (HsWrapper, Type)
top_instantiate Bool
False

top_instantiate :: Bool   -- True  <=> instantiate *all* variables
                          -- False <=> instantiate only the inferred ones
                -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
top_instantiate :: Bool -> CtOrigin -> Type -> TcM (HsWrapper, Type)
top_instantiate Bool
inst_all CtOrigin
orig Type
ty
  | ([VarBndr DFunId ArgFlag]
binders, Type
phi) <- Type -> ([VarBndr DFunId ArgFlag], Type)
tcSplitForAllVarBndrs Type
ty
  , (ThetaType
theta, Type
rho)   <- Type -> (ThetaType, Type)
tcSplitPhiTy Type
phi
  , Bool -> Bool
not ([VarBndr DFunId ArgFlag] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VarBndr DFunId ArgFlag]
binders Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
  = do { let ([VarBndr DFunId ArgFlag]
inst_bndrs, [VarBndr DFunId ArgFlag]
leave_bndrs) = (VarBndr DFunId ArgFlag -> Bool)
-> [VarBndr DFunId ArgFlag]
-> ([VarBndr DFunId ArgFlag], [VarBndr DFunId ArgFlag])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span VarBndr DFunId ArgFlag -> Bool
forall {tv}. VarBndr tv ArgFlag -> Bool
should_inst [VarBndr DFunId ArgFlag]
binders
             (ThetaType
inst_theta, ThetaType
leave_theta)
               | [VarBndr DFunId ArgFlag] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VarBndr DFunId ArgFlag]
leave_bndrs = (ThetaType
theta, [])
               | Bool
otherwise        = ([], ThetaType
theta)
             in_scope :: InScopeSet
in_scope    = VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty)
             empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope
             inst_tvs :: [DFunId]
inst_tvs    = [VarBndr DFunId ArgFlag] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr DFunId ArgFlag]
inst_bndrs
       ; (TCvSubst
subst, [DFunId]
inst_tvs') <- (TCvSubst
 -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId))
-> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM TCvSubst
-> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId)
newMetaTyVarX TCvSubst
empty_subst [DFunId]
inst_tvs
       ; let inst_theta' :: ThetaType
inst_theta' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst ThetaType
inst_theta
             sigma' :: Type
sigma'      = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst ([VarBndr DFunId ArgFlag] -> Type -> Type
mkForAllTys [VarBndr DFunId ArgFlag]
leave_bndrs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                                          ThetaType -> Type -> Type
mkPhiTy ThetaType
leave_theta Type
rho)
             inst_tv_tys' :: ThetaType
inst_tv_tys' = [DFunId] -> ThetaType
mkTyVarTys [DFunId]
inst_tvs'

       ; HsWrapper
wrap1 <- CtOrigin
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCall CtOrigin
orig ThetaType
inst_tv_tys' ThetaType
inst_theta'
       ; String -> SDoc -> TcRn ()
traceTc String
"Instantiating"
                 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"all tyvars?" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
inst_all
                       , String -> SDoc
text String
"origin" SDoc -> SDoc -> SDoc
<+> CtOrigin -> SDoc
pprCtOrigin CtOrigin
orig
                       , String -> SDoc
text String
"type" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
debugPprType Type
ty
                       , String -> SDoc
text String
"theta" SDoc -> SDoc -> SDoc
<+> ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
theta
                       , String -> SDoc
text String
"leave_bndrs" SDoc -> SDoc -> SDoc
<+> [VarBndr DFunId ArgFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [VarBndr DFunId ArgFlag]
leave_bndrs
                       , String -> SDoc
text String
"with" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((Type -> SDoc) -> ThetaType -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
debugPprType ThetaType
inst_tv_tys')
                       , String -> SDoc
text String
"theta:" SDoc -> SDoc -> SDoc
<+>  ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
inst_theta' ])

       ; (HsWrapper
wrap2, Type
rho2) <-
           if [VarBndr DFunId ArgFlag] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VarBndr DFunId ArgFlag]
leave_bndrs   -- NB: if inst_all is True then leave_bndrs = []

         -- account for types like forall a. Num a => forall b. Ord b => ...
           then Bool -> CtOrigin -> Type -> TcM (HsWrapper, Type)
top_instantiate Bool
inst_all CtOrigin
orig Type
sigma'

         -- but don't loop if there were any un-inst'able tyvars
           else (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, Type
sigma')

       ; (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap1, Type
rho2) }

  | Bool
otherwise = (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, Type
ty)
  where

    should_inst :: VarBndr tv ArgFlag -> Bool
should_inst VarBndr tv ArgFlag
bndr
      | Bool
inst_all  = Bool
True
      | Bool
otherwise = VarBndr tv ArgFlag -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag VarBndr tv ArgFlag
bndr ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ArgFlag
Inferred

instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
-- Use this when you want to instantiate (forall a b c. ty) with
-- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might
-- not yet match (perhaps because there are unsolved constraints; #14154)
-- If they don't match, emit a kind-equality to promise that they will
-- eventually do so, and thus make a kind-homongeneous substitution.
instTyVarsWith :: CtOrigin -> [DFunId] -> ThetaType -> TcM TCvSubst
instTyVarsWith CtOrigin
orig [DFunId]
tvs ThetaType
tys
  = TCvSubst -> [DFunId] -> ThetaType -> TcM TCvSubst
go TCvSubst
emptyTCvSubst [DFunId]
tvs ThetaType
tys
  where
    go :: TCvSubst -> [DFunId] -> ThetaType -> TcM TCvSubst
go TCvSubst
subst [] []
      = TCvSubst -> TcM TCvSubst
forall (m :: * -> *) a. Monad m => a -> m a
return TCvSubst
subst
    go TCvSubst
subst (DFunId
tv:[DFunId]
tvs) (Type
ty:ThetaType
tys)
      | Type
tv_kind HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty_kind
      = TCvSubst -> [DFunId] -> ThetaType -> TcM TCvSubst
go (TCvSubst -> DFunId -> Type -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst DFunId
tv Type
ty) [DFunId]
tvs ThetaType
tys
      | Bool
otherwise
      = do { Coercion
co <- CtOrigin -> TypeOrKind -> Role -> Type -> Type -> TcM Coercion
emitWantedEq CtOrigin
orig TypeOrKind
KindLevel Role
Nominal Type
ty_kind Type
tv_kind
           ; TCvSubst -> [DFunId] -> ThetaType -> TcM TCvSubst
go (TCvSubst -> DFunId -> Type -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst DFunId
tv (Type
ty Type -> Coercion -> Type
`mkCastTy` Coercion
co)) [DFunId]
tvs ThetaType
tys }
      where
        tv_kind :: Type
tv_kind = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (DFunId -> Type
tyVarKind DFunId
tv)
        ty_kind :: Type
ty_kind = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty

    go TCvSubst
_ [DFunId]
_ ThetaType
_ = String -> SDoc -> TcM TCvSubst
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"instTysWith" ([DFunId] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunId]
tvs SDoc -> SDoc -> SDoc
$$ ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
tys)


{-
************************************************************************
*                                                                      *
            Instantiating a call
*                                                                      *
************************************************************************

Note [Handling boxed equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The solver deals entirely in terms of unboxed (primitive) equality.
There should never be a boxed Wanted equality. Ever. But, what if
we are calling `foo :: forall a. (F a ~ Bool) => ...`? That equality
is boxed, so naive treatment here would emit a boxed Wanted equality.

So we simply check for this case and make the right boxing of evidence.

-}

----------------
instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
-- Instantiate the constraints of a call
--      (instCall o tys theta)
-- (a) Makes fresh dictionaries as necessary for the constraints (theta)
-- (b) Throws these dictionaries into the LIE
-- (c) Returns an HsWrapper ([.] tys dicts)

instCall :: CtOrigin
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCall CtOrigin
orig ThetaType
tys ThetaType
theta
  = do  { HsWrapper
dict_app <- CtOrigin -> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCallConstraints CtOrigin
orig ThetaType
theta
        ; HsWrapper -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
dict_app HsWrapper -> HsWrapper -> HsWrapper
<.> ThetaType -> HsWrapper
mkWpTyApps ThetaType
tys) }

----------------
instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
-- Instantiates the TcTheta, puts all constraints thereby generated
-- into the LIE, and returns a HsWrapper to enclose the call site.

instCallConstraints :: CtOrigin -> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCallConstraints CtOrigin
orig ThetaType
preds
  | ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
preds
  = HsWrapper -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return HsWrapper
idHsWrapper
  | Bool
otherwise
  = do { [EvTerm]
evs <- (Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm)
-> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) [EvTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
go ThetaType
preds
       ; String -> SDoc -> TcRn ()
traceTc String
"instCallConstraints" ([EvTerm] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EvTerm]
evs)
       ; HsWrapper -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvTerm] -> HsWrapper
mkWpEvApps [EvTerm]
evs) }
  where
    go :: TcPredType -> TcM EvTerm
    go :: Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
go Type
pred
     | Just (Role
Nominal, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pred -- Try short-cut #1
     = do  { Coercion
co <- Maybe (HsExpr GhcRn) -> Type -> Type -> TcM Coercion
unifyType Maybe (HsExpr GhcRn)
forall a. Maybe a
Nothing Type
ty1 Type
ty2
           ; EvTerm -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> EvTerm
evCoercion Coercion
co) }

       -- Try short-cut #2
     | Just (TyCon
tc, args :: ThetaType
args@[Type
_, Type
_, Type
ty1, Type
ty2]) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
pred
     , TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
     = do { Coercion
co <- Maybe (HsExpr GhcRn) -> Type -> Type -> TcM Coercion
unifyType Maybe (HsExpr GhcRn)
forall a. Maybe a
Nothing Type
ty1 Type
ty2
          ; EvTerm -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DFunId -> ThetaType -> [EvExpr] -> EvTerm
evDFunApp (DataCon -> DFunId
dataConWrapId DataCon
heqDataCon) ThetaType
args [Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion Coercion
co]) }

     | Bool
otherwise
     = CtOrigin -> Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
emitWanted CtOrigin
orig Type
pred

instDFunType :: DFunId -> [DFunInstType]
             -> TcM ( [TcType]      -- instantiated argument types
                    , TcThetaType ) -- instantiated constraint
-- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
instDFunType :: DFunId -> [DFunInstType] -> TcM (ThetaType, ThetaType)
instDFunType DFunId
dfun_id [DFunInstType]
dfun_inst_tys
  = do { (TCvSubst
subst, ThetaType
inst_tys) <- TCvSubst -> [DFunId] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go TCvSubst
empty_subst [DFunId]
dfun_tvs [DFunInstType]
dfun_inst_tys
       ; (ThetaType, ThetaType) -> TcM (ThetaType, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (ThetaType
inst_tys, HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst ThetaType
dfun_theta) }
  where
    dfun_ty :: Type
dfun_ty = DFunId -> Type
idType DFunId
dfun_id
    ([DFunId]
dfun_tvs, ThetaType
dfun_theta, Type
_) = Type -> ([DFunId], ThetaType, Type)
tcSplitSigmaTy Type
dfun_ty
    empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
dfun_ty))
                  -- With quantified constraints, the
                  -- type of a dfun may not be closed

    go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
    go :: TCvSubst -> [DFunId] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go TCvSubst
subst [] [] = (TCvSubst, ThetaType) -> TcM (TCvSubst, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst, [])
    go TCvSubst
subst (DFunId
tv:[DFunId]
tvs) (Just Type
ty : [DFunInstType]
mb_tys)
      = do { (TCvSubst
subst', ThetaType
tys) <- TCvSubst -> [DFunId] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go (TCvSubst -> DFunId -> Type -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst DFunId
tv Type
ty)
                                 [DFunId]
tvs
                                 [DFunInstType]
mb_tys
           ; (TCvSubst, ThetaType) -> TcM (TCvSubst, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst', Type
ty Type -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
: ThetaType
tys) }
    go TCvSubst
subst (DFunId
tv:[DFunId]
tvs) (DFunInstType
Nothing : [DFunInstType]
mb_tys)
      = do { (TCvSubst
subst', DFunId
tv') <- TCvSubst
-> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId)
newMetaTyVarX TCvSubst
subst DFunId
tv
           ; (TCvSubst
subst'', ThetaType
tys) <- TCvSubst -> [DFunId] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go TCvSubst
subst' [DFunId]
tvs [DFunInstType]
mb_tys
           ; (TCvSubst, ThetaType) -> TcM (TCvSubst, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst'', DFunId -> Type
mkTyVarTy DFunId
tv' Type -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
: ThetaType
tys) }
    go TCvSubst
_ [DFunId]
_ [DFunInstType]
_ = String -> SDoc -> TcM (TCvSubst, ThetaType)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"instDFunTypes" (DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr DFunId
dfun_id SDoc -> SDoc -> SDoc
$$ [DFunInstType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunInstType]
dfun_inst_tys)

----------------
instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
-- Similar to instCall, but only emit the constraints in the LIE
-- Used exclusively for the 'stupid theta' of a data constructor
instStupidTheta :: CtOrigin -> ThetaType -> TcRn ()
instStupidTheta CtOrigin
orig ThetaType
theta
  = do  { HsWrapper
_co <- CtOrigin -> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCallConstraints CtOrigin
orig ThetaType
theta -- Discard the coercion
        ; () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }


{- *********************************************************************
*                                                                      *
         Instantiating Kinds
*                                                                      *
********************************************************************* -}

-- | Given ty::forall k1 k2. k, instantiate all the invisible forall-binders
--   returning ty @kk1 @kk2 :: k[kk1/k1, kk2/k1]
tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
tcInstInvisibleTyBinders :: Type -> Type -> TcM (Type, Type)
tcInstInvisibleTyBinders Type
ty Type
kind
  = do { (ThetaType
extra_args, Type
kind') <- Int -> Type -> TcM (ThetaType, Type)
tcInstInvisibleTyBindersN Int
n_invis Type
kind
       ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> ThetaType -> Type
mkAppTys Type
ty ThetaType
extra_args, Type
kind') }
  where
    n_invis :: Int
n_invis = Type -> Int
invisibleTyBndrCount Type
kind

tcInstInvisibleTyBindersN :: Int -> TcKind -> TcM ([TcType], TcKind)
tcInstInvisibleTyBindersN :: Int -> Type -> TcM (ThetaType, Type)
tcInstInvisibleTyBindersN Int
0 Type
kind
  = (ThetaType, Type) -> TcM (ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
kind)
tcInstInvisibleTyBindersN Int
n Type
ty
  = Int -> TCvSubst -> Type -> TcM (ThetaType, Type)
forall {t}.
(Ord t, Num t) =>
t -> TCvSubst -> Type -> TcM (ThetaType, Type)
go Int
n TCvSubst
empty_subst Type
ty
  where
    empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty))

    go :: t -> TCvSubst -> Type -> TcM (ThetaType, Type)
go t
n TCvSubst
subst Type
kind
      | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0
      , Just (TyBinder
bndr, Type
body) <- Type -> Maybe (TyBinder, Type)
tcSplitPiTy_maybe Type
kind
      , TyBinder -> Bool
isInvisibleBinder TyBinder
bndr
      = do { (TCvSubst
subst', Type
arg) <- TCvSubst -> TyBinder -> TcM (TCvSubst, Type)
tcInstInvisibleTyBinder TCvSubst
subst TyBinder
bndr
           ; (ThetaType
args, Type
inner_ty) <- t -> TCvSubst -> Type -> TcM (ThetaType, Type)
go (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) TCvSubst
subst' Type
body
           ; (ThetaType, Type) -> TcM (ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
argType -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
:ThetaType
args, Type
inner_ty) }
      | Bool
otherwise
      = (ThetaType, Type) -> TcM (ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
kind)

-- | Used only in *types*
tcInstInvisibleTyBinder :: TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
tcInstInvisibleTyBinder :: TCvSubst -> TyBinder -> TcM (TCvSubst, Type)
tcInstInvisibleTyBinder TCvSubst
subst (Named (Bndr DFunId
tv ArgFlag
_))
  = do { (TCvSubst
subst', DFunId
tv') <- TCvSubst
-> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId)
newMetaTyVarX TCvSubst
subst DFunId
tv
       ; (TCvSubst, Type) -> TcM (TCvSubst, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst', DFunId -> Type
mkTyVarTy DFunId
tv') }

tcInstInvisibleTyBinder TCvSubst
subst (Anon AnonArgFlag
af Scaled Type
ty)
  | Just (Coercion -> TcM Type
mk, Type
k1, Type
k2) <- Type -> Maybe (Coercion -> TcM Type, Type, Type)
get_eq_tys_maybe (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
ty))
    -- Equality is the *only* constraint currently handled in types.
    -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
  = ASSERT( af == InvisArg )
    do { Coercion
co <- Maybe (HsType GhcRn) -> Type -> Type -> TcM Coercion
unifyKind Maybe (HsType GhcRn)
forall a. Maybe a
Nothing Type
k1 Type
k2
       ; Type
arg' <- Coercion -> TcM Type
mk Coercion
co
       ; (TCvSubst, Type) -> TcM (TCvSubst, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst, Type
arg') }

  | Bool
otherwise  -- This should never happen
               -- See GHC.Core.TyCo.Rep Note [Constraints in kinds]
  = String -> SDoc -> TcM (TCvSubst, Type)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tcInvisibleTyBinder" (Scaled Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Scaled Type
ty)

-------------------------------
get_eq_tys_maybe :: Type
                 -> Maybe ( Coercion -> TcM Type
                             -- given a coercion proving t1 ~# t2, produce the
                             -- right instantiation for the TyBinder at hand
                          , Type  -- t1
                          , Type  -- t2
                          )
-- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
get_eq_tys_maybe :: Type -> Maybe (Coercion -> TcM Type, Type, Type)
get_eq_tys_maybe Type
ty
  -- Lifted heterogeneous equality (~~)
  | Just (TyCon
tc, [Type
_, Type
_, Type
k1, Type
k2]) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty
  , TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
  = (Coercion -> TcM Type, Type, Type)
-> Maybe (Coercion -> TcM Type, Type, Type)
forall a. a -> Maybe a
Just (\Coercion
co -> Coercion -> Type -> Type -> TcM Type
mkHEqBoxTy Coercion
co Type
k1 Type
k2, Type
k1, Type
k2)

  -- Lifted homogeneous equality (~)
  | Just (TyCon
tc, [Type
_, Type
k1, Type
k2]) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty
  , TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
  = (Coercion -> TcM Type, Type, Type)
-> Maybe (Coercion -> TcM Type, Type, Type)
forall a. a -> Maybe a
Just (\Coercion
co -> Coercion -> Type -> Type -> TcM Type
mkEqBoxTy Coercion
co Type
k1 Type
k2, Type
k1, Type
k2)

  | Bool
otherwise
  = Maybe (Coercion -> TcM Type, Type, Type)
forall a. Maybe a
Nothing

-- | This takes @a ~# b@ and returns @a ~~ b@.
mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
-- monadic just for convenience with mkEqBoxTy
mkHEqBoxTy :: Coercion -> Type -> Type -> TcM Type
mkHEqBoxTy Coercion
co Type
ty1 Type
ty2
  = Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcM Type) -> Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    TyCon -> ThetaType -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
heqDataCon) [Type
k1, Type
k2, Type
ty1, Type
ty2, Coercion -> Type
mkCoercionTy Coercion
co]
  where k1 :: Type
k1 = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty1
        k2 :: Type
k2 = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty2

-- | This takes @a ~# b@ and returns @a ~ b@.
mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
mkEqBoxTy :: Coercion -> Type -> Type -> TcM Type
mkEqBoxTy Coercion
co Type
ty1 Type
ty2
  = Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcM Type) -> Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    TyCon -> ThetaType -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
eqDataCon) [Type
k, Type
ty1, Type
ty2, Coercion -> Type
mkCoercionTy Coercion
co]
  where k :: Type
k = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty1

{- *********************************************************************
*                                                                      *
        SkolemTvs (immutable)
*                                                                      *
********************************************************************* -}

tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
                   -- ^ How to instantiate the type variables
           -> Id                                           -- ^ Type to instantiate
           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
                -- (type vars, preds (incl equalities), rho)
tcInstType :: ([DFunId] -> TcM (TCvSubst, [DFunId]))
-> DFunId -> TcM ([(Name, DFunId)], ThetaType, Type)
tcInstType [DFunId] -> TcM (TCvSubst, [DFunId])
inst_tyvars DFunId
id
  | [DFunId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DFunId]
tyvars   -- There may be overloading despite no type variables;
                  --      (?x :: Int) => Int -> Int
  = ([(Name, DFunId)], ThetaType, Type)
-> TcM ([(Name, DFunId)], ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], ThetaType
theta, Type
tau)
  | Bool
otherwise
  = do { (TCvSubst
subst, [DFunId]
tyvars') <- [DFunId] -> TcM (TCvSubst, [DFunId])
inst_tyvars [DFunId]
tyvars
       ; let tv_prs :: [(Name, DFunId)]
tv_prs  = (DFunId -> Name) -> [DFunId] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DFunId -> Name
tyVarName [DFunId]
tyvars [Name] -> [DFunId] -> [(Name, DFunId)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [DFunId]
tyvars'
             subst' :: TCvSubst
subst'  = TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet TCvSubst
subst (Type -> VarSet
tyCoVarsOfType Type
rho)
       ; ([(Name, DFunId)], ThetaType, Type)
-> TcM ([(Name, DFunId)], ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, DFunId)]
tv_prs, HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst' ThetaType
theta, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst' Type
tau) }
  where
    ([DFunId]
tyvars, Type
rho) = Type -> ([DFunId], Type)
tcSplitForAllTys (DFunId -> Type
idType DFunId
id)
    (ThetaType
theta, Type
tau)  = Type -> (ThetaType, Type)
tcSplitPhiTy Type
rho

tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
                     -- (type vars, preds (incl equalities), rho)
-- Instantiate the binders of a type signature with TyVarTvs
tcInstTypeBndrs :: DFunId -> TcM ([(Name, InvisTVBinder)], ThetaType, Type)
tcInstTypeBndrs DFunId
id
  | [InvisTVBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [InvisTVBinder]
tyvars   -- There may be overloading despite no type variables;
                  --      (?x :: Int) => Int -> Int
  = ([(Name, InvisTVBinder)], ThetaType, Type)
-> TcM ([(Name, InvisTVBinder)], ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], ThetaType
theta, Type
tau)
  | Bool
otherwise
  = do { (TCvSubst
subst, [InvisTVBinder]
tyvars') <- (TCvSubst
 -> InvisTVBinder
 -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, InvisTVBinder))
-> TCvSubst
-> [InvisTVBinder]
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, [InvisTVBinder])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM TCvSubst
-> InvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, InvisTVBinder)
inst_invis_bndr TCvSubst
emptyTCvSubst [InvisTVBinder]
tyvars
       ; let tv_prs :: [(Name, InvisTVBinder)]
tv_prs  = (InvisTVBinder -> Name) -> [InvisTVBinder] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (DFunId -> Name
tyVarName (DFunId -> Name)
-> (InvisTVBinder -> DFunId) -> InvisTVBinder -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InvisTVBinder -> DFunId
forall tv argf. VarBndr tv argf -> tv
binderVar) [InvisTVBinder]
tyvars [Name] -> [InvisTVBinder] -> [(Name, InvisTVBinder)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [InvisTVBinder]
tyvars'
             subst' :: TCvSubst
subst'  = TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet TCvSubst
subst (Type -> VarSet
tyCoVarsOfType Type
rho)
       ; ([(Name, InvisTVBinder)], ThetaType, Type)
-> TcM ([(Name, InvisTVBinder)], ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, InvisTVBinder)]
tv_prs, HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst' ThetaType
theta, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst' Type
tau) }
  where
    ([InvisTVBinder]
tyvars, Type
rho) = Type -> ([InvisTVBinder], Type)
splitForAllTysInvis (DFunId -> Type
idType DFunId
id)
    (ThetaType
theta, Type
tau)  = Type -> (ThetaType, Type)
tcSplitPhiTy Type
rho

    inst_invis_bndr :: TCvSubst -> InvisTVBinder
                    -> TcM (TCvSubst, InvisTVBinder)
    inst_invis_bndr :: TCvSubst
-> InvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, InvisTVBinder)
inst_invis_bndr TCvSubst
subst (Bndr DFunId
tv Specificity
spec)
      = do { (TCvSubst
subst', DFunId
tv') <- TCvSubst
-> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId)
newMetaTyVarTyVarX TCvSubst
subst DFunId
tv
           ; (TCvSubst, InvisTVBinder)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, InvisTVBinder)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst', DFunId -> Specificity -> InvisTVBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr DFunId
tv' Specificity
spec) }

tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type signature with skolem constants.
-- We could give them fresh names, but no need to do so
tcSkolDFunType :: DFunId -> TcM ([DFunId], ThetaType, Type)
tcSkolDFunType DFunId
dfun
  = do { ([(Name, DFunId)]
tv_prs, ThetaType
theta, Type
tau) <- ([DFunId] -> TcM (TCvSubst, [DFunId]))
-> DFunId -> TcM ([(Name, DFunId)], ThetaType, Type)
tcInstType [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSuperSkolTyVars DFunId
dfun
       ; ([DFunId], ThetaType, Type) -> TcM ([DFunId], ThetaType, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, DFunId) -> DFunId) -> [(Name, DFunId)] -> [DFunId]
forall a b. (a -> b) -> [a] -> [b]
map (Name, DFunId) -> DFunId
forall a b. (a, b) -> b
snd [(Name, DFunId)]
tv_prs, ThetaType
theta, Type
tau) }

tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
-- Make skolem constants, but do *not* give them new names, as above
-- Moreover, make them "super skolems"; see comments with superSkolemTv
-- see Note [Kind substitution when instantiating]
-- Precondition: tyvars should be ordered by scoping
tcSuperSkolTyVars :: [DFunId] -> (TCvSubst, [DFunId])
tcSuperSkolTyVars = (TCvSubst -> DFunId -> (TCvSubst, DFunId))
-> TCvSubst -> [DFunId] -> (TCvSubst, [DFunId])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TCvSubst -> DFunId -> (TCvSubst, DFunId)
tcSuperSkolTyVar TCvSubst
emptyTCvSubst

tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
tcSuperSkolTyVar :: TCvSubst -> DFunId -> (TCvSubst, DFunId)
tcSuperSkolTyVar TCvSubst
subst DFunId
tv
  = (TCvSubst -> DFunId -> DFunId -> TCvSubst
extendTvSubstWithClone TCvSubst
subst DFunId
tv DFunId
new_tv, DFunId
new_tv)
  where
    kind :: Type
kind   = TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
subst (DFunId -> Type
tyVarKind DFunId
tv)
    new_tv :: DFunId
new_tv = Name -> Type -> TcTyVarDetails -> DFunId
mkTcTyVar (DFunId -> Name
tyVarName DFunId
tv) Type
kind TcTyVarDetails
superSkolemTv

-- | Given a list of @['TyVar']@, skolemize the type variables,
-- returning a substitution mapping the original tyvars to the
-- skolems, and the list of newly bound skolems.
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSkolTyVars :: [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVars = TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsX TCvSubst
emptyTCvSubst

tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSkolTyVarsX :: TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsX = Bool -> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsPushLevel Bool
False

tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSuperSkolTyVars :: [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSuperSkolTyVars = TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSuperSkolTyVarsX TCvSubst
emptyTCvSubst

tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSuperSkolTyVarsX :: TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSuperSkolTyVarsX TCvSubst
subst = Bool -> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsPushLevel Bool
True TCvSubst
subst

tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
                          -> TcM (TCvSubst, [TcTyVar])
-- Skolemise one level deeper, hence pushTcLevel
-- See Note [Skolemising type variables]
tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsPushLevel Bool
overlappable TCvSubst
subst [DFunId]
tvs
  = do { TcLevel
tc_lvl <- TcM TcLevel
getTcLevel
       ; let pushed_lvl :: TcLevel
pushed_lvl = TcLevel -> TcLevel
pushTcLevel TcLevel
tc_lvl
       ; TcLevel -> Bool -> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsAt TcLevel
pushed_lvl Bool
overlappable TCvSubst
subst [DFunId]
tvs }

tcInstSkolTyVarsAt :: TcLevel -> Bool
                   -> TCvSubst -> [TyVar]
                   -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVarsAt :: TcLevel -> Bool -> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
tcInstSkolTyVarsAt TcLevel
lvl Bool
overlappable TCvSubst
subst [DFunId]
tvs
  = (Name -> Type -> DFunId)
-> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
new_skol_tv TCvSubst
subst [DFunId]
tvs
  where
    details :: TcTyVarDetails
details = TcLevel -> Bool -> TcTyVarDetails
SkolemTv TcLevel
lvl Bool
overlappable
    new_skol_tv :: Name -> Type -> DFunId
new_skol_tv Name
name Type
kind = Name -> Type -> TcTyVarDetails -> DFunId
mkTcTyVar Name
name Type
kind TcTyVarDetails
details

------------------
freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
-- ^ Give fresh uniques to a bunch of TyVars, but they stay
--   as TyVars, rather than becoming TcTyVars
-- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
freshenTyVarBndrs :: [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyVarBndrs = (Name -> Type -> DFunId) -> [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mkTyVar

freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
-- ^ Give fresh uniques to a bunch of CoVars
-- Used in "GHC.Tc.Instance.Family.newFamInst"
freshenCoVarBndrsX :: TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
freshenCoVarBndrsX TCvSubst
subst = (Name -> Type -> DFunId)
-> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mkCoVar TCvSubst
subst

------------------
freshenTyCoVars :: (Name -> Kind -> TyCoVar)
                -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
freshenTyCoVars :: (Name -> Type -> DFunId) -> [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mk_tcv = (Name -> Type -> DFunId)
-> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mk_tcv TCvSubst
emptyTCvSubst

freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
                 -> TCvSubst -> [TyCoVar]
                 -> TcM (TCvSubst, [TyCoVar])
freshenTyCoVarsX :: (Name -> Type -> DFunId)
-> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mk_tcv = (TCvSubst
 -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId))
-> TCvSubst -> [DFunId] -> TcM (TCvSubst, [DFunId])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM ((Name -> Type -> DFunId)
-> TCvSubst
-> DFunId
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId)
freshenTyCoVarX Name -> Type -> DFunId
mk_tcv)

freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
                -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
-- This a complete freshening operation:
-- the skolems have a fresh unique, and a location from the monad
-- See Note [Skolemising type variables]
freshenTyCoVarX :: (Name -> Type -> DFunId)
-> TCvSubst
-> DFunId
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId)
freshenTyCoVarX Name -> Type -> DFunId
mk_tcv TCvSubst
subst DFunId
tycovar
  = do { SrcSpan
loc  <- TcRn SrcSpan
getSrcSpanM
       ; Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
       ; let old_name :: Name
old_name = DFunId -> Name
tyVarName DFunId
tycovar
             -- Force so we don't retain reference to the old name and id
             -- See (#19619) for more discussion
             !old_occ_name :: OccName
old_occ_name = Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName Name
old_name
             new_name :: Name
new_name = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
uniq OccName
old_occ_name SrcSpan
loc
             new_kind :: Type
new_kind = TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
subst (DFunId -> Type
tyVarKind DFunId
tycovar)
             new_tcv :: DFunId
new_tcv  = Name -> Type -> DFunId
mk_tcv Name
new_name Type
new_kind
             subst1 :: TCvSubst
subst1   = TCvSubst -> DFunId -> DFunId -> TCvSubst
extendTCvSubstWithClone TCvSubst
subst DFunId
tycovar DFunId
new_tcv
       ; (TCvSubst, DFunId)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, DFunId)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst1, DFunId
new_tcv) }

{- Note [Skolemising type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The tcInstSkolTyVars family of functions instantiate a list of TyVars
to fresh skolem TcTyVars. Important notes:

a) Level allocation. We generally skolemise /before/ calling
   pushLevelAndCaptureConstraints.  So we want their level to the level
   of the soon-to-be-created implication, which has a level ONE HIGHER
   than the current level.  Hence the pushTcLevel.  It feels like a
   slight hack.

b) The [TyVar] should be ordered (kind vars first)
   See Note [Kind substitution when instantiating]

c) It's a complete freshening operation: the skolems have a fresh
   unique, and a location from the monad

d) The resulting skolems are
        non-overlappable for tcInstSkolTyVars,
   but overlappable for tcInstSuperSkolTyVars
   See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
   of where this matters.

Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
expect them to be topologically sorted.
Then we have to instantiate the kind variables, build a substitution
from old variables to the new variables, then instantiate the type
variables substituting the original kind.

Exemple: If we want to instantiate
  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
we want
  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
instead of the bogus
  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
-}

{- *********************************************************************
*                                                                      *
                Literals
*                                                                      *
********************************************************************* -}

{-
In newOverloadedLit we convert directly to an Int or Integer if we
know that's what we want.  This may save some time, by not
temporarily generating overloaded literals, but it won't catch all
cases (the rest are caught in lookupInst).

-}

newOverloadedLit :: HsOverLit GhcRn
                 -> ExpRhoType
                 -> TcM (HsOverLit GhcTc)
newOverloadedLit :: HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newOverloadedLit
  lit :: HsOverLit GhcRn
lit@(OverLit { ol_val :: forall p. HsOverLit p -> OverLitVal
ol_val = OverLitVal
val, ol_ext :: forall p. HsOverLit p -> XOverLit p
ol_ext = XOverLit GhcRn
rebindable }) ExpRhoType
res_ty
  | Bool -> Bool
not Bool
XOverLit GhcRn
rebindable
  = do { Type
res_ty <- ExpRhoType -> TcM Type
expTypeToType ExpRhoType
res_ty
       ; DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; let platform :: Platform
platform = DynFlags -> Platform
targetPlatform DynFlags
dflags
       ; case Platform -> OverLitVal -> Type -> Maybe (HsExpr GhcTc)
shortCutLit Platform
platform OverLitVal
val Type
res_ty of
        -- Do not generate a LitInst for rebindable syntax.
        -- Reason: If we do, tcSimplify will call lookupInst, which
        --         will call tcSyntaxName, which does unification,
        --         which tcSimplify doesn't like
           Just HsExpr GhcTc
expr -> HsOverLit GhcTc -> TcM (HsOverLit GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsOverLit GhcRn
lit { ol_witness :: HsExpr GhcTc
ol_witness = HsExpr GhcTc
expr
                                    , ol_ext :: XOverLit GhcTc
ol_ext = Bool -> Type -> OverLitTc
OverLitTc Bool
False Type
res_ty })
           Maybe (HsExpr GhcTc)
Nothing   -> CtOrigin -> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit CtOrigin
orig HsOverLit GhcRn
lit
                                                   (Type -> ExpRhoType
mkCheckExpType Type
res_ty) }

  | Bool
otherwise
  = CtOrigin -> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit CtOrigin
orig HsOverLit GhcRn
lit ExpRhoType
res_ty
  where
    orig :: CtOrigin
orig = HsOverLit GhcRn -> CtOrigin
LiteralOrigin HsOverLit GhcRn
lit

-- Does not handle things that 'shortCutLit' can handle. See also
-- newOverloadedLit in GHC.Tc.Utils.Unify
newNonTrivialOverloadedLit :: CtOrigin
                           -> HsOverLit GhcRn
                           -> ExpRhoType
                           -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit :: CtOrigin -> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit CtOrigin
orig
  lit :: HsOverLit GhcRn
lit@(OverLit { ol_val :: forall p. HsOverLit p -> OverLitVal
ol_val = OverLitVal
val, ol_witness :: forall p. HsOverLit p -> HsExpr p
ol_witness = HsVar XVar GhcRn
_ (L SrcSpan
_ IdP GhcRn
meth_name)
               , ol_ext :: forall p. HsOverLit p -> XOverLit p
ol_ext = XOverLit GhcRn
rebindable }) ExpRhoType
res_ty
  = do  { HsLit GhcTc
hs_lit <- OverLitVal -> TcM (HsLit GhcTc)
mkOverLit OverLitVal
val
        ; let lit_ty :: Type
lit_ty = HsLit GhcTc -> Type
forall (p :: Pass). HsLit (GhcPass p) -> Type
hsLitType HsLit GhcTc
hs_lit
        ; (()
_, SyntaxExprTc
fi') <- CtOrigin
-> SyntaxExprRn
-> [SyntaxOpType]
-> ExpRhoType
-> (ThetaType -> ThetaType -> TcRn ())
-> TcM ((), SyntaxExprTc)
forall a.
CtOrigin
-> SyntaxExprRn
-> [SyntaxOpType]
-> ExpRhoType
-> (ThetaType -> ThetaType -> TcM a)
-> TcM (a, SyntaxExprTc)
tcSyntaxOp CtOrigin
orig (Name -> SyntaxExprRn
mkRnSyntaxExpr Name
IdP GhcRn
meth_name)
                                      [Type -> SyntaxOpType
synKnownType Type
lit_ty] ExpRhoType
res_ty ((ThetaType -> ThetaType -> TcRn ()) -> TcM ((), SyntaxExprTc))
-> (ThetaType -> ThetaType -> TcRn ()) -> TcM ((), SyntaxExprTc)
forall a b. (a -> b) -> a -> b
$
                      \ThetaType
_ ThetaType
_ -> () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        ; let L SrcSpan
_ HsExpr GhcTc
witness = SyntaxExprTc
-> [GenLocated SrcSpan (HsExpr GhcTc)]
-> GenLocated SrcSpan (HsExpr GhcTc)
nlHsSyntaxApps SyntaxExprTc
fi' [HsLit GhcTc -> GenLocated SrcSpan (HsExpr GhcTc)
forall (p :: Pass). HsLit (GhcPass p) -> LHsExpr (GhcPass p)
nlHsLit HsLit GhcTc
hs_lit]
        ; Type
res_ty <- ExpRhoType -> TcM Type
readExpType ExpRhoType
res_ty
        ; HsOverLit GhcTc -> TcM (HsOverLit GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsOverLit GhcRn
lit { ol_witness :: HsExpr GhcTc
ol_witness = HsExpr GhcTc
witness
                      , ol_ext :: XOverLit GhcTc
ol_ext = Bool -> Type -> OverLitTc
OverLitTc Bool
XOverLit GhcRn
rebindable Type
res_ty }) }
newNonTrivialOverloadedLit CtOrigin
_ HsOverLit GhcRn
lit ExpRhoType
_
  = String -> SDoc -> TcM (HsOverLit GhcTc)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"newNonTrivialOverloadedLit" (HsOverLit GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsOverLit GhcRn
lit)

------------
mkOverLit ::OverLitVal -> TcM (HsLit GhcTc)
mkOverLit :: OverLitVal -> TcM (HsLit GhcTc)
mkOverLit (HsIntegral IntegralLit
i)
  = do  { Type
integer_ty <- Name -> TcM Type
tcMetaTy Name
integerTyConName
        ; HsLit GhcTc -> TcM (HsLit GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsInteger GhcTc -> Integer -> Type -> HsLit GhcTc
forall x. XHsInteger x -> Integer -> Type -> HsLit x
HsInteger (IntegralLit -> SourceText
il_text IntegralLit
i)
                            (IntegralLit -> Integer
il_value IntegralLit
i) Type
integer_ty) }

mkOverLit (HsFractional FractionalLit
r)
  = do  { Type
rat_ty <- Name -> TcM Type
tcMetaTy Name
rationalTyConName
        ; HsLit GhcTc -> TcM (HsLit GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsRat GhcTc -> FractionalLit -> Type -> HsLit GhcTc
forall x. XHsRat x -> FractionalLit -> Type -> HsLit x
HsRat NoExtField
XHsRat GhcTc
noExtField FractionalLit
r Type
rat_ty) }

mkOverLit (HsIsString SourceText
src FastString
s) = HsLit GhcTc -> TcM (HsLit GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsString GhcTc -> FastString -> HsLit GhcTc
forall x. XHsString x -> FastString -> HsLit x
HsString SourceText
XHsString GhcTc
src FastString
s)

{-
************************************************************************
*                                                                      *
                Re-mappable syntax

     Used only for arrow syntax -- find a way to nuke this
*                                                                      *
************************************************************************

Suppose we are doing the -XRebindableSyntax thing, and we encounter
a do-expression.  We have to find (>>) in the current environment, which is
done by the rename. Then we have to check that it has the same type as
Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
this:

  (>>) :: HB m n mn => m a -> n b -> mn b

So the idea is to generate a local binding for (>>), thus:

        let then72 :: forall a b. m a -> m b -> m b
            then72 = ...something involving the user's (>>)...
        in
        ...the do-expression...

Now the do-expression can proceed using then72, which has exactly
the expected type.

In fact tcSyntaxName just generates the RHS for then72, because we only
want an actual binding in the do-expression case. For literals, we can
just use the expression inline.
-}

tcSyntaxName :: CtOrigin
             -> TcType                 -- ^ Type to instantiate it at
             -> (Name, HsExpr GhcRn)   -- ^ (Standard name, user name)
             -> TcM (Name, HsExpr GhcTc)
                                       -- ^ (Standard name, suitable expression)
-- USED ONLY FOR CmdTop (sigh) ***
-- See Note [CmdSyntaxTable] in "GHC.Hs.Expr"

tcSyntaxName :: CtOrigin
-> Type -> (Name, HsExpr GhcRn) -> TcM (Name, HsExpr GhcTc)
tcSyntaxName CtOrigin
orig Type
ty (Name
std_nm, HsVar XVar GhcRn
_ (L SrcSpan
_ IdP GhcRn
user_nm))
  | Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
IdP GhcRn
user_nm
  = do HsExpr GhcTc
rhs <- CtOrigin -> Name -> ThetaType -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
orig Name
std_nm [Type
ty]
       (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
std_nm, HsExpr GhcTc
rhs)

tcSyntaxName CtOrigin
orig Type
ty (Name
std_nm, HsExpr GhcRn
user_nm_expr) = do
    DFunId
std_id <- Name -> TcM DFunId
tcLookupId Name
std_nm
    let
        -- C.f. newMethodAtLoc
        ([DFunId
tv], ThetaType
_, Type
tau) = Type -> ([DFunId], ThetaType, Type)
tcSplitSigmaTy (DFunId -> Type
idType DFunId
std_id)
        sigma1 :: Type
sigma1         = HasCallStack => [DFunId] -> ThetaType -> Type -> Type
[DFunId] -> ThetaType -> Type -> Type
substTyWith [DFunId
tv] [Type
ty] Type
tau
        -- Actually, the "tau-type" might be a sigma-type in the
        -- case of locally-polymorphic methods.

    (TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
syntaxNameCtxt HsExpr GhcRn
user_nm_expr CtOrigin
orig Type
sigma1) (TcM (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc))
-> TcM (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$ do

        -- Check that the user-supplied thing has the
        -- same type as the standard one.
        -- Tiresome jiggling because tcCheckSigma takes a located expression
     SrcSpan
span <- TcRn SrcSpan
getSrcSpanM
     GenLocated SrcSpan (HsExpr GhcTc)
expr <- LHsExpr GhcRn -> Type -> TcM (GenLocated SrcSpan (HsExpr GhcTc))
tcCheckPolyExpr (SrcSpan -> HsExpr GhcRn -> LHsExpr GhcRn
forall l e. l -> e -> GenLocated l e
L SrcSpan
span HsExpr GhcRn
user_nm_expr) Type
sigma1
     (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
std_nm, GenLocated SrcSpan (HsExpr GhcTc) -> HsExpr GhcTc
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan (HsExpr GhcTc)
expr)

syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv
               -> TcRn (TidyEnv, SDoc)
syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
syntaxNameCtxt HsExpr GhcRn
name CtOrigin
orig Type
ty TidyEnv
tidy_env
  = do { CtLoc
inst_loc <- CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM CtOrigin
orig (TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
TypeLevel)
       ; let msg :: SDoc
msg = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"When checking that" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
name)
                          SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"(needed by a syntactic construct)"
                        , Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"has the required type:"
                                  SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env Type
ty))
                        , Int -> SDoc -> SDoc
nest Int
2 (CtLoc -> SDoc
pprCtLoc CtLoc
inst_loc) ]
       ; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
msg) }

{-
************************************************************************
*                                                                      *
                Instances
*                                                                      *
************************************************************************
-}

getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
-- Construct the OverlapFlag from the global module flags,
-- but if the overlap_mode argument is (Just m),
--     set the OverlapMode to 'm'
getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag Maybe OverlapMode
overlap_mode
  = do  { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
        ; let overlap_ok :: Bool
overlap_ok    = Extension -> DynFlags -> Bool
xopt Extension
LangExt.OverlappingInstances DynFlags
dflags
              incoherent_ok :: Bool
incoherent_ok = Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances  DynFlags
dflags
              use :: OverlapMode -> OverlapFlag
use OverlapMode
x = OverlapFlag :: OverlapMode -> Bool -> OverlapFlag
OverlapFlag { isSafeOverlap :: Bool
isSafeOverlap = DynFlags -> Bool
safeLanguageOn DynFlags
dflags
                                  , overlapMode :: OverlapMode
overlapMode   = OverlapMode
x }
              default_oflag :: OverlapFlag
default_oflag | Bool
incoherent_ok = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
Incoherent SourceText
NoSourceText)
                            | Bool
overlap_ok    = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
Overlaps SourceText
NoSourceText)
                            | Bool
otherwise     = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
NoOverlap SourceText
NoSourceText)

              final_oflag :: OverlapFlag
final_oflag = OverlapFlag -> Maybe OverlapMode -> OverlapFlag
setOverlapModeMaybe OverlapFlag
default_oflag Maybe OverlapMode
overlap_mode
        ; OverlapFlag -> TcM OverlapFlag
forall (m :: * -> *) a. Monad m => a -> m a
return OverlapFlag
final_oflag }

tcGetInsts :: TcM [ClsInst]
-- Gets the local class instances.
tcGetInsts :: TcM [ClsInst]
tcGetInsts = (TcGblEnv -> [ClsInst])
-> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv -> TcM [ClsInst]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TcGblEnv -> [ClsInst]
tcg_insts IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv

newClsInst :: Maybe OverlapMode -> Name -> [TyVar] -> ThetaType
           -> Class -> [Type] -> TcM ClsInst
newClsInst :: Maybe OverlapMode
-> Name
-> [DFunId]
-> ThetaType
-> Class
-> ThetaType
-> TcM ClsInst
newClsInst Maybe OverlapMode
overlap_mode Name
dfun_name [DFunId]
tvs ThetaType
theta Class
clas ThetaType
tys
  = do { (TCvSubst
subst, [DFunId]
tvs') <- [DFunId] -> TcM (TCvSubst, [DFunId])
freshenTyVarBndrs [DFunId]
tvs
             -- Be sure to freshen those type variables,
             -- so they are sure not to appear in any lookup
       ; let tys' :: ThetaType
tys' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst ThetaType
tys

             dfun :: DFunId
dfun = Name -> [DFunId] -> ThetaType -> Class -> ThetaType -> DFunId
mkDictFunId Name
dfun_name [DFunId]
tvs ThetaType
theta Class
clas ThetaType
tys
             -- The dfun uses the original 'tvs' because
             -- (a) they don't need to be fresh
             -- (b) they may be mentioned in the ib_binds field of
             --     an InstInfo, and in GHC.Tc.Utils.Env.pprInstInfoDetails it's
             --     helpful to use the same names

       ; OverlapFlag
oflag <- Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag Maybe OverlapMode
overlap_mode
       ; let inst :: ClsInst
inst = DFunId -> OverlapFlag -> [DFunId] -> Class -> ThetaType -> ClsInst
mkLocalInstance DFunId
dfun OverlapFlag
oflag [DFunId]
tvs' Class
clas ThetaType
tys'
       ; WarningFlag -> Bool -> SDoc -> TcRn ()
warnIfFlag WarningFlag
Opt_WarnOrphans
                    (IsOrphan -> Bool
isOrphan (ClsInst -> IsOrphan
is_orphan ClsInst
inst))
                    (ClsInst -> SDoc
instOrphWarn ClsInst
inst)
       ; ClsInst -> TcM ClsInst
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInst
inst }

instOrphWarn :: ClsInst -> SDoc
instOrphWarn :: ClsInst -> SDoc
instOrphWarn ClsInst
inst
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Orphan instance:") Int
2 (ClsInst -> SDoc
pprInstanceHdr ClsInst
inst)
    SDoc -> SDoc -> SDoc
$$ String -> SDoc
text String
"To avoid this"
    SDoc -> SDoc -> SDoc
$$ Int -> SDoc -> SDoc
nest Int
4 ([SDoc] -> SDoc
vcat [SDoc]
possibilities)
  where
    possibilities :: [SDoc]
possibilities =
      String -> SDoc
text String
"move the instance declaration to the module of the class or of the type, or" SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
:
      String -> SDoc
text String
"wrap the type with a newtype and declare the instance on the new type." SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
:
      []

tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
  -- Add new locally-defined instances
tcExtendLocalInstEnv :: forall a. [ClsInst] -> TcM a -> TcM a
tcExtendLocalInstEnv [ClsInst]
dfuns TcM a
thing_inside
 = do { [ClsInst] -> TcRn ()
traceDFuns [ClsInst]
dfuns
      ; TcGblEnv
env <- IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
      -- Force the access to the TcgEnv so it isn't retained.
      -- During auditing it is much easier to observe in -hi profiles if
      -- there are a very small number of TcGblEnv. Keeping a TcGblEnv
      -- alive is quite dangerous because it contains reference to many
      -- large data structures.
      ; let !init_inst_env :: InstEnv
init_inst_env = TcGblEnv -> InstEnv
tcg_inst_env TcGblEnv
env
            !init_insts :: [ClsInst]
init_insts = TcGblEnv -> [ClsInst]
tcg_insts TcGblEnv
env
      ; (InstEnv
inst_env', [ClsInst]
cls_insts') <- ((InstEnv, [ClsInst])
 -> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst]))
-> (InstEnv, [ClsInst])
-> [ClsInst]
-> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (InstEnv, [ClsInst])
-> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
addLocalInst
                                          (InstEnv
init_inst_env, [ClsInst]
init_insts)
                                          [ClsInst]
dfuns
      ; let env' :: TcGblEnv
env' = TcGblEnv
env { tcg_insts :: [ClsInst]
tcg_insts    = [ClsInst]
cls_insts'
                       , tcg_inst_env :: InstEnv
tcg_inst_env = InstEnv
inst_env' }
      ; TcGblEnv -> TcM a -> TcM a
forall gbl lcl a. gbl -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
setGblEnv TcGblEnv
env' TcM a
thing_inside }

addLocalInst :: (InstEnv, [ClsInst]) -> ClsInst -> TcM (InstEnv, [ClsInst])
-- Check that the proposed new instance is OK,
-- and then add it to the home inst env
-- If overwrite_inst, then we can overwrite a direct match
addLocalInst :: (InstEnv, [ClsInst])
-> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
addLocalInst (InstEnv
home_ie, [ClsInst]
my_insts) ClsInst
ispec
   = do {
             -- Load imported instances, so that we report
             -- duplicates correctly

             -- 'matches'  are existing instance declarations that are less
             --            specific than the new one
             -- 'dups'     are those 'matches' that are equal to the new one
         ; Bool
isGHCi <- TcRn Bool
getIsGHCi
         ; ExternalPackageState
eps    <- TcRnIf TcGblEnv TcLclEnv ExternalPackageState
forall gbl lcl. TcRnIf gbl lcl ExternalPackageState
getEps
         ; TcGblEnv
tcg_env <- IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv

           -- In GHCi, we *override* any identical instances
           -- that are also defined in the interactive context
           -- See Note [Override identical instances in GHCi]
         ; let home_ie' :: InstEnv
home_ie'
                 | Bool
isGHCi    = InstEnv -> ClsInst -> InstEnv
deleteFromInstEnv InstEnv
home_ie ClsInst
ispec
                 | Bool
otherwise = InstEnv
home_ie

               global_ie :: InstEnv
global_ie = ExternalPackageState -> InstEnv
eps_inst_env ExternalPackageState
eps
               inst_envs :: InstEnvs
inst_envs = InstEnvs :: InstEnv -> InstEnv -> VisibleOrphanModules -> InstEnvs
InstEnvs { ie_global :: InstEnv
ie_global  = InstEnv
global_ie
                                    , ie_local :: InstEnv
ie_local   = InstEnv
home_ie'
                                    , ie_visible :: VisibleOrphanModules
ie_visible = TcGblEnv -> VisibleOrphanModules
tcVisibleOrphanMods TcGblEnv
tcg_env }

             -- Check for inconsistent functional dependencies
         ; let inconsistent_ispecs :: [ClsInst]
inconsistent_ispecs = InstEnvs -> ClsInst -> [ClsInst]
checkFunDeps InstEnvs
inst_envs ClsInst
ispec
         ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
inconsistent_ispecs) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
           ClsInst -> [ClsInst] -> TcRn ()
funDepErr ClsInst
ispec [ClsInst]
inconsistent_ispecs

             -- Check for duplicate instance decls.
         ; let ([DFunId]
_tvs, Class
cls, ThetaType
tys) = ClsInst -> ([DFunId], Class, ThetaType)
instanceHead ClsInst
ispec
               ([InstMatch]
matches, [ClsInst]
_, [InstMatch]
_)  = Bool
-> InstEnvs
-> Class
-> ThetaType
-> ([InstMatch], [ClsInst], [InstMatch])
lookupInstEnv Bool
False InstEnvs
inst_envs Class
cls ThetaType
tys
               dups :: [ClsInst]
dups             = (ClsInst -> Bool) -> [ClsInst] -> [ClsInst]
forall a. (a -> Bool) -> [a] -> [a]
filter (ClsInst -> ClsInst -> Bool
identicalClsInstHead ClsInst
ispec) ((InstMatch -> ClsInst) -> [InstMatch] -> [ClsInst]
forall a b. (a -> b) -> [a] -> [b]
map InstMatch -> ClsInst
forall a b. (a, b) -> a
fst [InstMatch]
matches)
         ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
dups) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
           ClsInst -> ClsInst -> TcRn ()
dupInstErr ClsInst
ispec ([ClsInst] -> ClsInst
forall a. [a] -> a
head [ClsInst]
dups)

         ; (InstEnv, [ClsInst])
-> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
forall (m :: * -> *) a. Monad m => a -> m a
return (InstEnv -> ClsInst -> InstEnv
extendInstEnv InstEnv
home_ie' ClsInst
ispec, ClsInst
ispec ClsInst -> [ClsInst] -> [ClsInst]
forall a. a -> [a] -> [a]
: [ClsInst]
my_insts) }

{-
Note [Signature files and type class instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Instances in signature files do not have an effect when compiling:
when you compile a signature against an implementation, you will
see the instances WHETHER OR NOT the instance is declared in
the file (this is because the signatures go in the EPS and we
can't filter them out easily.)  This is also why we cannot
place the instance in the hi file: it would show up as a duplicate,
and we don't have instance reexports anyway.

However, you might find them useful when typechecking against
a signature: the instance is a way of indicating to GHC that
some instance exists, in case downstream code uses it.

Implementing this is a little tricky.  Consider the following
situation (sigof03):

 module A where
     instance C T where ...

 module ASig where
     instance C T

When compiling ASig, A.hi is loaded, which brings its instances
into the EPS.  When we process the instance declaration in ASig,
we should ignore it for the purpose of doing a duplicate check,
since it's not actually a duplicate. But don't skip the check
entirely, we still want this to fail (tcfail221):

 module ASig where
     instance C T
     instance C T

Note that in some situations, the interface containing the type
class instances may not have been loaded yet at all.  The usual
situation when A imports another module which provides the
instances (sigof02m):

 module A(module B) where
     import B

See also Note [Signature lazy interface loading].  We can't
rely on this, however, since sometimes we'll have spurious
type class instances in the EPS, see #9422 (sigof02dm)

************************************************************************
*                                                                      *
        Errors and tracing
*                                                                      *
************************************************************************
-}

traceDFuns :: [ClsInst] -> TcRn ()
traceDFuns :: [ClsInst] -> TcRn ()
traceDFuns [ClsInst]
ispecs
  = String -> SDoc -> TcRn ()
traceTc String
"Adding instances:" ([SDoc] -> SDoc
vcat ((ClsInst -> SDoc) -> [ClsInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ClsInst -> SDoc
pp [ClsInst]
ispecs))
  where
    pp :: ClsInst -> SDoc
pp ClsInst
ispec = SDoc -> Int -> SDoc -> SDoc
hang (DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ClsInst -> DFunId
instanceDFunId ClsInst
ispec) SDoc -> SDoc -> SDoc
<+> SDoc
colon)
                  Int
2 (ClsInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInst
ispec)
        -- Print the dfun name itself too

funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
funDepErr ClsInst
ispec [ClsInst]
ispecs
  = SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr (String -> SDoc
text String
"Functional dependencies conflict between instance declarations:")
                    (ClsInst
ispec ClsInst -> [ClsInst] -> [ClsInst]
forall a. a -> [a] -> [a]
: [ClsInst]
ispecs)

dupInstErr :: ClsInst -> ClsInst -> TcRn ()
dupInstErr :: ClsInst -> ClsInst -> TcRn ()
dupInstErr ClsInst
ispec ClsInst
dup_ispec
  = SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr (String -> SDoc
text String
"Duplicate instance declarations:")
                    [ClsInst
ispec, ClsInst
dup_ispec]

addClsInstsErr :: SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr :: SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr SDoc
herald [ClsInst]
ispecs
  = SrcSpan -> TcRn () -> TcRn ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan (ClsInst -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan ([ClsInst] -> ClsInst
forall a. [a] -> a
head [ClsInst]
sorted)) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
    SDoc -> TcRn ()
addErr (SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald Int
2 ([ClsInst] -> SDoc
pprInstances [ClsInst]
sorted))
 where
   sorted :: [ClsInst]
sorted = (ClsInst -> ClsInst -> Ordering) -> [ClsInst] -> [ClsInst]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (SrcSpan -> SrcSpan -> Ordering
SrcLoc.leftmost_smallest (SrcSpan -> SrcSpan -> Ordering)
-> (ClsInst -> SrcSpan) -> ClsInst -> ClsInst -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ClsInst -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan) [ClsInst]
ispecs
   -- The sortBy just arranges that instances are displayed in order
   -- of source location, which reduced wobbling in error messages,
   -- and is better for users