{-# LANGUAGE FlexibleContexts, RecursiveDo #-}
{-# LANGUAGE DisambiguateRecordFields #-}
{-# LANGUAGE LambdaCase #-}

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

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

-}

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

     tcInstType, tcInstTypeBndrs,
     tcSkolemiseInvisibleBndrs,
     tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarBndrsX,
     tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,

     freshenTyVarBndrs, freshenCoVarBndrsX,

     tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,

     newOverloadedLit, mkOverLit,

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

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

import GHC.Prelude

import GHC.Driver.Session
import GHC.Driver.Env

import GHC.Builtin.Types  ( integerTyConName )
import GHC.Builtin.Names

import GHC.Hs
import GHC.Hs.Syn.Type   ( hsLitType )

import GHC.Core.InstEnv
import GHC.Core.FamInstEnv
import GHC.Core ( isOrphan ) -- For the Coercion constructor
import GHC.Core.Type
import GHC.Core.TyCo.Ppr ( debugPprType )
import GHC.Core.Class( Class )
import GHC.Core.Coercion.Axiom

import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Env
import GHC.Tc.Types.Evidence
import GHC.Tc.Instance.FunDeps
import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Errors.Types
import GHC.Tc.Zonk.Monad ( ZonkM )

import GHC.Rename.Utils( mkRnSyntaxExpr )

import GHC.Types.Id.Make( mkDictFunId )
import GHC.Types.Basic ( TypeOrKind(..), Arity, VisArity )
import GHC.Types.Error
import GHC.Types.SourceText
import GHC.Types.SrcLoc as SrcLoc
import GHC.Types.Var.Env
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Types.Var
import qualified GHC.LanguageExtensions as LangExt

import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Utils.Outputable
import GHC.Utils.Unique (sameUnique)

import GHC.Unit.State
import GHC.Unit.External
import GHC.Unit.Module.Warnings

import Data.List ( mapAccumL )
import qualified Data.List.NonEmpty as NE
import Control.Monad( when, unless )
import Data.Function ( on )

{-
************************************************************************
*                                                                      *
                Creating and emitting 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 -> [Type] -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
origin Name
name [Type]
ty_args
  = do { 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 = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (DFunId -> Type
idType DFunId
id) [Type]
ty_args
             (theta, _caller_knows_this) = tcSplitPhiTy ty
       ; wrap <- assert (not (isForAllTy ty) && isSingleton theta) $
                 instCall origin ty_args theta

       ; return (mkHsWrap wrap (HsVar noExtField (noLocA 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

For nested foralls, see Note [Skolemisation en-bloc]

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

Note [Skolemisation en-bloc]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this case:

  topSkolemise  (forall a. Ord a => forall b. Eq b => a->b->b)

We /could/ return just
  (wp, [a], [d:Ord a, forall b. Eq b => a -> b -> b)

But in fact we skolemise "en-bloc", looping around (in `topSkolemise` for
example) to skolemise the (forall b. Eq b =>).  So in fact

  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 applies regardless of DeepSubsumption.

Why do we do this "en-bloc" loopy thing?  It is /nearly/ just an optimisation.
But not quite!  At the call site of `topSkolemise` (and its cousins) we
use `checkConstraints` to gather constraints and build an implication
constraint.   So skolemising just one level at a time would lead to nested
implication constraints. That is a bit less efficient, but there is /also/ a small
user-visible effect: see Note [Let-bound skolems] in GHC.Tc.Solver.InertSet.
Specifically, consider

   forall a. Eq a => forall b. (a ~ [b]) => blah

If we skolemise en-bloc, the equality (a~[b]) is like a let-binding and we
don't treat it like a GADT pattern match, limiting unification. With nested
implications, the inner one would be treated as having-given-equalities.

This is also relevant when Required foralls are involved; see #24810, and
the loop in `skolemiseRequired`.
-}

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

    -- Why recursive?  See Note [Skolemisation en-bloc]
    go :: Subst
-> HsWrapper
-> [(Name, TcInvisTVBinder)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, TcInvisTVBinder)], [DFunId], Type)
go Subst
subst HsWrapper
wrap [(Name, TcInvisTVBinder)]
tv_prs [DFunId]
ev_vars Type
ty
      | ([TcInvisTVBinder]
bndrs, [Type]
theta, Type
inner_ty) <- Type -> ([TcInvisTVBinder], [Type], Type)
tcSplitSigmaTyBndrs Type
ty
      , let tvs :: [DFunId]
tvs = [TcInvisTVBinder] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcInvisTVBinder]
bndrs
      , Bool -> Bool
not ([DFunId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DFunId]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
      = do { (subst', bndrs1) <- SkolemInfo
-> Subst -> [TcInvisTVBinder] -> TcM (Subst, [TcInvisTVBinder])
forall vis.
SkolemInfo
-> Subst
-> [VarBndr DFunId vis]
-> TcM (Subst, [VarBndr DFunId vis])
tcInstSkolTyVarBndrsX SkolemInfo
skolem_info Subst
subst [TcInvisTVBinder]
bndrs
           ; let tvs1 = [TcInvisTVBinder] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcInvisTVBinder]
bndrs1
           ; traceTc "topSkol" (vcat [ ppr tvs <+> vcat (map (ppr . getSrcSpan) tvs)
                                     , ppr tvs1 <+> vcat (map (ppr . getSrcSpan) tvs1) ])
           ; ev_vars1 <- newEvVars (substTheta subst' theta)
           ; go subst'
                (wrap <.> mkWpTyLams tvs1 <.> mkWpEvLams ev_vars1)
                (tv_prs ++ (map tyVarName tvs `zip` bndrs1))
                (ev_vars ++ ev_vars1)
                inner_ty }

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

skolemiseRequired :: SkolemInfo -> VisArity -> TcSigmaType
                  -> TcM (VisArity, HsWrapper, [Name], [ForAllTyBinder], [EvVar], TcRhoType)
-- Skolemise up to N required (visible) binders,
--    plus any invisible ones "in the way",
--    /and/ any trailing invisible ones.
-- So the result has no top-level invisible quantifiers.
-- Return the depleted arity.
skolemiseRequired :: SkolemInfo
-> Arity
-> Type
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
skolemiseRequired SkolemInfo
skolem_info Arity
n_req Type
sigma
  = Arity
-> Subst
-> HsWrapper
-> [Name]
-> [ForAllTyBinder]
-> [DFunId]
-> Type
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
go Arity
n_req Subst
init_subst HsWrapper
idHsWrapper [] [] [] Type
sigma
  where
    init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
sigma))

    -- Why recursive?  See Note [Skolemisation en-bloc]
    go :: Arity
-> Subst
-> HsWrapper
-> [Name]
-> [ForAllTyBinder]
-> [DFunId]
-> Type
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
go Arity
n_req Subst
subst HsWrapper
wrap [Name]
acc_nms [ForAllTyBinder]
acc_bndrs [DFunId]
ev_vars Type
ty
      | (Arity
n_req', [ForAllTyBinder]
bndrs, Type
inner_ty) <- Arity -> Type -> (Arity, [ForAllTyBinder], Type)
tcSplitForAllTyVarsReqTVBindersN Arity
n_req Type
ty
      , Bool -> Bool
not ([ForAllTyBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ForAllTyBinder]
bndrs)
      = do { (subst', bndrs1) <- SkolemInfo
-> Subst -> [ForAllTyBinder] -> TcM (Subst, [ForAllTyBinder])
forall vis.
SkolemInfo
-> Subst
-> [VarBndr DFunId vis]
-> TcM (Subst, [VarBndr DFunId vis])
tcInstSkolTyVarBndrsX SkolemInfo
skolem_info Subst
subst [ForAllTyBinder]
bndrs
           ; let tvs1 = [ForAllTyBinder] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [ForAllTyBinder]
bndrs1
                 -- fix_up_vis: see Note [Required foralls in Core]
                 --             in GHC.Core.TyCo.Rep
                 fix_up_vis | Arity
n_req Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
n_req'
                            = HsWrapper
idHsWrapper
                            | Bool
otherwise
                            = [ForAllTyBinder] -> Type -> HsWrapper
mkWpForAllCast [ForAllTyBinder]
bndrs1 (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst' Type
inner_ty)
           ; go n_req' subst'
                (wrap <.> fix_up_vis <.> mkWpTyLams tvs1)
                (acc_nms   ++ map (tyVarName . binderVar) bndrs)
                (acc_bndrs ++ bndrs1)
                ev_vars
                inner_ty }

      | ([Type]
theta, Type
inner_ty) <- Type -> ([Type], Type)
tcSplitPhiTy Type
ty
      , Bool -> Bool
not ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
      = do { ev_vars1 <- [Type] -> TcM [DFunId]
newEvVars (HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta)
           ; go n_req subst
                (wrap <.> mkWpEvLams ev_vars1)
                acc_nms
                acc_bndrs
                (ev_vars ++ ev_vars1)
                inner_ty }

      | Bool
otherwise
      = (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Arity
n_req, HsWrapper
wrap, [Name]
acc_nms, [ForAllTyBinder]
acc_bndrs, [DFunId]
ev_vars, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty)
        -- substTy is a quick no-op on an empty substitution

topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
-- Instantiate outer invisible binders (both Inferred and Specified)
-- If    top_instantiate ty = (wrap, inner_ty)
-- then  wrap :: inner_ty "->" ty
-- NB: returns a type with no (=>),
--     and no invisible forall at the top
topInstantiate :: CtOrigin -> Type -> TcM (HsWrapper, Type)
topInstantiate CtOrigin
orig Type
sigma
  | ([DFunId]
tvs,   Type
body1) <- (ForAllTyFlag -> Bool) -> Type -> ([DFunId], Type)
tcSplitSomeForAllTyVars ForAllTyFlag -> Bool
isInvisibleForAllTyFlag Type
sigma
  , ([Type]
theta, Type
body2) <- Type -> ([Type], Type)
tcSplitPhiTy Type
body1
  , Bool -> Bool
not ([DFunId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DFunId]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
  = do { (_, wrap1, body3) <- CtOrigin
-> ConcreteTyVars
-> [DFunId]
-> [Type]
-> Type
-> TcM ([DFunId], HsWrapper, Type)
instantiateSigma CtOrigin
orig ConcreteTyVars
noConcreteTyVars [DFunId]
tvs [Type]
theta Type
body2
           -- Why 'noConcreteTyVars' here?
           -- See Note [Representation-polymorphism checking built-ins]
           -- in GHC.Tc.Utils.Concrete.

       -- Loop, to account for types like
       --       forall a. Num a => forall b. Ord b => ...
       ; (wrap2, body4) <- topInstantiate orig body3

       ; return (wrap2 <.> wrap1, body4) }

  | Bool
otherwise = (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, Type
sigma)

instantiateSigma :: CtOrigin
                 -> ConcreteTyVars -- ^ concreteness information
                 -> [TyVar]
                 -> TcThetaType -> TcSigmaType
                 -> TcM ([TcTyVar], HsWrapper, TcSigmaType)
-- (instantiate orig tvs theta ty)
-- instantiates the type variables tvs, emits the (instantiated)
-- constraints theta, and returns the (instantiated) type ty
instantiateSigma :: CtOrigin
-> ConcreteTyVars
-> [DFunId]
-> [Type]
-> Type
-> TcM ([DFunId], HsWrapper, Type)
instantiateSigma CtOrigin
orig ConcreteTyVars
concs [DFunId]
tvs [Type]
theta Type
body_ty
  = do { rec (subst, inst_tvs) <- mapAccumLM (new_meta subst) empty_subst tvs
       ; let inst_theta  = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta
             inst_body   = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
body_ty
             inst_tv_tys = [DFunId] -> [Type]
mkTyVarTys [DFunId]
inst_tvs

       ; wrap <- instCall orig inst_tv_tys inst_theta
       ; traceTc "Instantiating"
                 (vcat [ text "origin" <+> pprCtOrigin orig
                       , text "tvs"   <+> ppr tvs
                       , text "theta" <+> ppr theta
                       , text "type" <+> debugPprType body_ty
                       , text "with" <+> vcat (map debugPprType inst_tv_tys)
                       , text "theta:" <+> ppr inst_theta ])

      ; return (inst_tvs, wrap, inst_body) }
  where
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType ([DFunId] -> [Type] -> Type -> Type
HasDebugCallStack => [DFunId] -> [Type] -> Type -> Type
mkSpecSigmaTy [DFunId]
tvs [Type]
theta Type
body_ty))
               -- mkSpecSigmaTy: Inferred vs Specified is not important here;
               --                We just want an accurate free-var set
    empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope
    new_meta :: Subst -> Subst -> TyVar -> TcM (Subst, TcTyVar)
    new_meta :: Subst
-> Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
new_meta Subst
final_subst Subst
subst DFunId
tv
      -- Is this a type variable that must be instantiated to a concrete type?
      -- If so, create a ConcreteTv metavariable instead of a plain TauTv.
      -- See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete.
      | Just ConcreteTvOrigin
conc_orig0 <- ConcreteTyVars -> Name -> Maybe ConcreteTvOrigin
forall a. NameEnv a -> Name -> Maybe a
lookupNameEnv ConcreteTyVars
concs (DFunId -> Name
tyVarName DFunId
tv)
      , let conc_orig :: ConcreteTvOrigin
conc_orig = Subst -> Type -> ConcreteTvOrigin -> ConcreteTvOrigin
substConcreteTvOrigin Subst
final_subst Type
body_ty ConcreteTvOrigin
conc_orig0
      -- See Note [substConcreteTvOrigin].
      = ConcreteTvOrigin
-> Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newConcreteTyVarX ConcreteTvOrigin
conc_orig Subst
subst DFunId
tv
      | Bool
otherwise
      = Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv

instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM Subst
-- 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-homogeneous substitution.
instTyVarsWith :: CtOrigin -> [DFunId] -> [Type] -> TcM Subst
instTyVarsWith CtOrigin
orig [DFunId]
tvs [Type]
tys
  = Subst -> [DFunId] -> [Type] -> TcM Subst
go Subst
emptySubst [DFunId]
tvs [Type]
tys
  where
    go :: Subst -> [DFunId] -> [Type] -> TcM Subst
go Subst
subst [] []
      = Subst -> TcM Subst
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
subst
    go Subst
subst (DFunId
tv:[DFunId]
tvs) (Type
ty:[Type]
tys)
      | Type
tv_kind HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty_kind
      = Subst -> [DFunId] -> [Type] -> TcM Subst
go (Subst -> DFunId -> Type -> Subst
extendTvSubstAndInScope Subst
subst DFunId
tv Type
ty) [DFunId]
tvs [Type]
tys
      | Bool
otherwise
      = do { co <- CtOrigin -> TypeOrKind -> Role -> Type -> Type -> TcM Coercion
emitWantedEq CtOrigin
orig TypeOrKind
KindLevel Role
Nominal Type
ty_kind Type
tv_kind
           ; go (extendTvSubstAndInScope subst tv (ty `mkCastTy` co)) tvs tys }
      where
        tv_kind :: Type
tv_kind = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (DFunId -> Type
tyVarKind DFunId
tv)
        ty_kind :: Type
ty_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty

    go Subst
_ [DFunId]
_ [Type]
_ = String -> SDoc -> TcM Subst
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"instTysWith" ([DFunId] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunId]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
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 -> [Type] -> [Type] -> TcM HsWrapper
instCall CtOrigin
orig [Type]
tys [Type]
theta
  = do  { dict_app <- CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
theta
        ; return (dict_app <.> mkWpTyApps 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 -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
preds
  | [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
preds
  = HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return HsWrapper
idHsWrapper
  | Bool
otherwise
  = do { evs <- (Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm)
-> [Type] -> IOEnv (Env TcGblEnv TcLclEnv) [EvTerm]
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 (CtOrigin -> Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
emitWanted CtOrigin
orig) [Type]
preds
                -- See Note [Possible fast path for equality constraints]
       ; traceTc "instCallConstraints" (ppr evs)
       ; return (mkWpEvApps evs) }

{- Note [Possible fast path for equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given  f :: forall a b. (a ~ [b]) => a -> b -> blah
rather than emitting ([W] alpha ~ [beta]) we could imagine calling unifyType
right here. But note

* Often such constraints look like (F a ~ G b), in which case unification would end up
  spitting out a wanted-equality anyway.

* So perhaps the main fast-path would be where the LHS or RHS was an instantiation
  variable. But note that this could, perhaps, impact on Quick Look:

  - The first arg of `f` changes from the naked `a` to the guarded `[b]` (or would do so
    if we zonked it).  That might affect typing under Quick Look.

  - We might imagine using the let-bound skolems trick:
         g :: forall a b. (a ~ forall c. c->c) => a -> [a] -> [a]
    Here we are just using `a` as a local abreviation for (forall c. c->c)
    See Note [Let-bound skolems] in GHC.Tc.Solver.InertSet.

    If we substitute aggressively (including zonking) that abbreviation could work.  But
    again it affects what is typeable.  And we don't support equalities over polytypes,
    currently, anyway.

* There is little point in trying to optimise for
   - (s ~# t), because this has kind Constraint#, not Constraint, and so will not be
               in the theta instantiated in instCall
   - (s ~~ t), becaues heterogeneous equality is rare, and more complicated.

Anyway, for now we don't take advantage of these potential effects.
-}

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

    go :: Subst -> [TyVar] -> [DFunInstType] -> TcM (Subst, [TcType])
    go :: Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go Subst
subst [] [] = (Subst, [Type]) -> TcM (Subst, [Type])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, [])
    go Subst
subst (DFunId
tv:[DFunId]
tvs) (Just Type
ty : [DFunInstType]
mb_tys)
      = do { (subst', tys) <- Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go (Subst -> DFunId -> Type -> Subst
extendTvSubstAndInScope Subst
subst DFunId
tv Type
ty)
                                 [DFunId]
tvs
                                 [DFunInstType]
mb_tys
           ; return (subst', ty : tys) }
    go Subst
subst (DFunId
tv:[DFunId]
tvs) (DFunInstType
Nothing : [DFunInstType]
mb_tys)
      = do { (subst', tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv
           ; (subst'', tys) <- go subst' tvs mb_tys
           ; return (subst'', mkTyVarTy tv' : tys) }
    go Subst
_ [DFunId]
_ [DFunInstType]
_ = String -> SDoc -> TcM (Subst, [Type])
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"instDFunTypes" (DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr DFunId
dfun_id SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [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 -> [Type] -> TcRn ()
instStupidTheta CtOrigin
orig [Type]
theta
  = do  { _co <- CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
theta -- Discard the coercion
        ; return () }


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

-- | Given ty::forall k1 k2. k, instantiate all the invisible forall-binders
--   returning ty @kk1 @kk2 :: k[kk1/k1, kk2/k1]
-- Called only to instantiate kinds, in user-written type signatures
tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
tcInstInvisibleTyBinders :: Type -> Type -> TcM (Type, Type)
tcInstInvisibleTyBinders Type
ty Type
kind
  = do { (extra_args, kind') <- Arity -> Type -> TcM ([Type], Type)
tcInstInvisibleTyBindersN Arity
n_invis Type
kind
       ; return (mkAppTys ty extra_args, kind') }
  where
    n_invis :: Arity
n_invis = Type -> Arity
invisibleBndrCount Type
kind
       -- We are re-using tcInstInvisibleTyBindersN, which is
       -- needed elsewhere; so all that matters is that n_invis
       -- is big enough! Does not matter if it is too big.
       -- 10,000 would do equally well :-)

tcInstInvisibleTyBindersN :: Int -> TcKind -> TcM ([TcType], TcKind)
-- Called only to instantiate kinds, in user-written type signatures
tcInstInvisibleTyBindersN :: Arity -> Type -> TcM ([Type], Type)
tcInstInvisibleTyBindersN Arity
0 Type
kind
  = ([Type], Type) -> TcM ([Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
kind)
tcInstInvisibleTyBindersN Arity
n Type
ty
  = Arity -> Subst -> Type -> TcM ([Type], Type)
forall {t}.
(Ord t, Num t) =>
t -> Subst -> Type -> TcM ([Type], Type)
go Arity
n Subst
empty_subst Type
ty
  where
    empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty))

    go :: t -> Subst -> Type -> TcM ([Type], Type)
go t
n Subst
subst Type
kind
      | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0
      , Just (ForAllTyBinder
bndr, Type
body) <- Type -> Maybe (ForAllTyBinder, Type)
tcSplitForAllTyVarBinder_maybe Type
kind
      , ForAllTyFlag -> Bool
isInvisibleForAllTyFlag (ForAllTyBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag ForAllTyBinder
bndr)
      = do { (subst', arg) <- Subst -> DFunId -> TcM (Subst, Type)
tcInstInvisibleTyBinder Subst
subst (ForAllTyBinder -> DFunId
forall tv argf. VarBndr tv argf -> tv
binderVar ForAllTyBinder
bndr)
           ; (args, inner_ty) <- go (n-1) subst' body
           ; return (arg:args, inner_ty) }
      | Bool
otherwise
      = ([Type], Type) -> TcM ([Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
kind)

tcInstInvisibleTyBinder :: Subst -> TyVar -> TcM (Subst, TcType)
-- Called only to instantiate kinds, in user-written type signatures

tcInstInvisibleTyBinder :: Subst -> DFunId -> TcM (Subst, Type)
tcInstInvisibleTyBinder Subst
subst DFunId
tv
  = do { (subst', tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv
       ; return (subst', mkTyVarTy tv') }

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

tcInstType :: ([TyVar] -> TcM (Subst, [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] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId]))
-> DFunId -> TcM ([(Name, DFunId)], [Type], Type)
tcInstType [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
inst_tyvars DFunId
id
  | [DFunId] -> Bool
forall a. [a] -> 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)], [Type], Type)
-> TcM ([(Name, DFunId)], [Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Type]
theta, Type
tau)
  | Bool
otherwise
  = do { (subst, tyvars') <- [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
inst_tyvars [DFunId]
tyvars
       ; let 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'  = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Type -> VarSet
tyCoVarsOfType Type
rho)
       ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
  where
    ([DFunId]
tyvars, Type
rho) = Type -> ([DFunId], Type)
tcSplitForAllInvisTyVars (DFunId -> Type
idType DFunId
id)
    ([Type]
theta, Type
tau)  = Type -> ([Type], Type)
tcSplitPhiTy Type
rho

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

    inst_invis_bndr :: Subst -> InvisTVBinder
                    -> TcM (Subst, InvisTVBinder)
    inst_invis_bndr :: Subst
-> TcInvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, TcInvisTVBinder)
inst_invis_bndr Subst
subst (Bndr DFunId
tv Specificity
spec)
      = do { (subst', tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarTyVarX Subst
subst DFunId
tv
           ; return (subst', Bndr tv' spec) }

--------------------------
tcSkolDFunType :: Type -> TcM (SkolemInfoAnon, [TcTyVar], TcThetaType, Class, [TcType])
-- Instantiate a type signature with skolem constants.
-- This freshens the names, but no need to do so
tcSkolDFunType :: Type -> TcM (SkolemInfoAnon, [DFunId], [Type], Class, [Type])
tcSkolDFunType Type
dfun_ty
  = do { let ([DFunId]
tvs, [Type]
theta, Class
cls, [Type]
tys) = Type -> ([DFunId], [Type], Class, [Type])
tcSplitDFunTy Type
dfun_ty

         -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
         --           in GHC.Tc.Utils.TcType
       ; rec { skol_info <- mkSkolemInfo skol_info_anon
             ; (subst, inst_tvs) <- tcInstSuperSkolTyVars skol_info tvs
                     -- We instantiate the dfun_tyd with superSkolems.
                     -- See Note [Subtle interaction of recursion and overlap]
                     -- and Note [Binding when looking up instances]
             ; let inst_tys = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys
                   skol_info_anon = Class -> [Type] -> SkolemInfoAnon
mkClsInstSkol Class
cls [Type]
inst_tys }

       ; let inst_theta = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta
       ; return (skol_info_anon, inst_tvs, inst_theta, cls, inst_tys) }

tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (Subst, [TcTyVar])
-- Make skolem constants, but do *not* give them new names, as above
-- As always, allocate them one level in
-- Moreover, make them "super skolems"; see GHC.Core.InstEnv
--    Note [Binding when looking up instances]
-- See Note [Kind substitution when instantiating]
-- Precondition: tyvars should be ordered by scoping
tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [DFunId] -> (Subst, [DFunId])
tcSuperSkolTyVars TcLevel
tc_lvl SkolemInfo
skol_info = (Subst -> DFunId -> (Subst, DFunId))
-> Subst -> [DFunId] -> (Subst, [DFunId])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL Subst -> DFunId -> (Subst, DFunId)
do_one Subst
emptySubst
  where
    details :: TcTyVarDetails
details = SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info (TcLevel -> TcLevel
pushTcLevel TcLevel
tc_lvl)
                       Bool
True   -- The "super" bit
    do_one :: Subst -> DFunId -> (Subst, DFunId)
do_one Subst
subst DFunId
tv = (Subst -> DFunId -> DFunId -> Subst
extendTvSubstWithClone Subst
subst DFunId
tv DFunId
new_tv, DFunId
new_tv)
      where
        kind :: Type
kind   = Subst -> Type -> Type
substTyUnchecked Subst
subst (DFunId -> Type
tyVarKind DFunId
tv)
        new_tv :: DFunId
new_tv = Name -> Type -> TcTyVarDetails -> DFunId
mkTcTyVar (DFunId -> Name
tyVarName DFunId
tv) Type
kind TcTyVarDetails
details

-- | 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 :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSkolTyVars :: SkolemInfo
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVars SkolemInfo
skol_info = SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
emptySubst

tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSkolTyVarsX :: SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skol_info = SkolemInfo
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsPushLevel SkolemInfo
skol_info Bool
False

tcInstSkolTyVarBndrsX :: SkolemInfo -> Subst -> [VarBndr TyCoVar vis] -> TcM (Subst, [VarBndr TyCoVar vis])
tcInstSkolTyVarBndrsX :: forall vis.
SkolemInfo
-> Subst
-> [VarBndr DFunId vis]
-> TcM (Subst, [VarBndr DFunId vis])
tcInstSkolTyVarBndrsX SkolemInfo
skol_info Subst
subs [VarBndr DFunId vis]
bndrs = do
  (subst', bndrs') <- SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
subs ([VarBndr DFunId vis] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr DFunId vis]
bndrs)
  pure (subst', zipWith mkForAllTyBinder flags bndrs')
  where
    flags :: [vis]
flags = [VarBndr DFunId vis] -> [vis]
forall tv argf. [VarBndr tv argf] -> [argf]
binderFlags [VarBndr DFunId vis]
bndrs

tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
-- This version freshens the names and creates "super skolems";
--    see comments around superSkolemTv.
-- Must be lazy in skol_info:
--   see Note [Keeping SkolemInfo inside a SkolemTv] in GHC.Tc.Utils.TcType
tcInstSuperSkolTyVars :: SkolemInfo
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSuperSkolTyVars SkolemInfo
skol_info = SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSuperSkolTyVarsX SkolemInfo
skol_info Subst
emptySubst

tcInstSuperSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
-- This version freshens the names and creates "super skolems";
-- see comments around superSkolemTv.
tcInstSuperSkolTyVarsX :: SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSuperSkolTyVarsX SkolemInfo
skol_info Subst
subst = SkolemInfo
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsPushLevel SkolemInfo
skol_info Bool
True Subst
subst

tcInstSkolTyVarsPushLevel :: SkolemInfo -> Bool  -- True <=> make "super skolem"
                          -> Subst -> [TyVar]
                          -> TcM (Subst, [TcTyVar])
-- Skolemise one level deeper, hence pushTcLevel
-- See Note [Skolemising type variables]
tcInstSkolTyVarsPushLevel :: SkolemInfo
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsPushLevel SkolemInfo
skol_info Bool
overlappable Subst
subst [DFunId]
tvs
  = do { tc_lvl <- TcM TcLevel
getTcLevel
       -- Do not retain the whole TcLclEnv
       ; let !pushed_lvl = TcLevel -> TcLevel
pushTcLevel TcLevel
tc_lvl
       ; tcInstSkolTyVarsAt skol_info pushed_lvl overlappable subst tvs }

tcInstSkolTyVarsAt :: SkolemInfo -> TcLevel -> Bool
                   -> Subst -> [TyVar]
                   -> TcM (Subst, [TcTyVar])
tcInstSkolTyVarsAt :: SkolemInfo
-> TcLevel
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsAt SkolemInfo
skol_info TcLevel
lvl Bool
overlappable Subst
subst [DFunId]
tvs
  = (Name -> Type -> DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
new_skol_tv Subst
subst [DFunId]
tvs
  where
    sk_details :: TcTyVarDetails
sk_details = SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info 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
sk_details

tcSkolemiseInvisibleBndrs :: SkolemInfoAnon -> Type -> TcM ([TcTyVar], TcType)
-- Skolemise the outer invisible binders of a type
-- Do /not/ freshen them, because their scope is broader than
-- just this type.  It's a bit dubious, but used in very limited ways.
tcSkolemiseInvisibleBndrs :: SkolemInfoAnon -> Type -> TcM ([DFunId], Type)
tcSkolemiseInvisibleBndrs SkolemInfoAnon
skol_info Type
ty
  = do { let ([DFunId]
tvs, Type
body_ty) = Type -> ([DFunId], Type)
tcSplitForAllInvisTyVars Type
ty
       ; lvl           <- TcM TcLevel
getTcLevel
       ; skol_info     <- mkSkolemInfo skol_info
       ; let details = SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info TcLevel
lvl Bool
False
             mk_skol_tv Name
name Type
kind = DFunId -> TcM DFunId
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> TcTyVarDetails -> DFunId
mkTcTyVar Name
name Type
kind TcTyVarDetails
details)  -- No freshening
       ; (subst, tvs') <- instantiateTyVarsX mk_skol_tv emptySubst tvs
       ; return (tvs', substTy subst body_ty) }

instantiateTyVarsX :: (Name -> Kind -> TcM TcTyVar)
                   -> Subst -> [TyVar]
                   -> TcM (Subst, [TcTyVar])
-- Instantiate each type variable in turn with the specified function
instantiateTyVarsX :: (Name -> Type -> TcM DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
instantiateTyVarsX Name -> Type -> TcM DFunId
mk_tv Subst
subst [DFunId]
tvs
  = case [DFunId]
tvs of
      []       -> (Subst, [DFunId])
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, [])
      (DFunId
tv:[DFunId]
tvs) -> do { let kind1 :: Type
kind1 = Subst -> Type -> Type
substTyUnchecked Subst
subst (DFunId -> Type
tyVarKind DFunId
tv)
                     ; tv' <- Name -> Type -> TcM DFunId
mk_tv (DFunId -> Name
tyVarName DFunId
tv) Type
kind1
                     ; let subst1 = Subst -> DFunId -> DFunId -> Subst
extendTCvSubstWithClone Subst
subst DFunId
tv DFunId
tv'
                     ; (subst', tvs') <- instantiateTyVarsX mk_tv subst1 tvs
                     ; return (subst', tv':tvs') }

------------------
freshenTyVarBndrs :: [TyVar] -> TcM (Subst, [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] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyVarBndrs = (Name -> Type -> DFunId)
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mkTyVar

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

------------------
freshenTyCoVars :: (Name -> Kind -> TyCoVar)
                -> [TyVar] -> TcM (Subst, [TyCoVar])
freshenTyCoVars :: (Name -> Type -> DFunId)
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mk_tcv = (Name -> Type -> DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mk_tcv Subst
emptySubst

freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
                 -> Subst -> [TyCoVar]
                 -> TcM (Subst, [TyCoVar])
-- This a complete freshening operation:
-- the skolems have a fresh unique, and a location from the monad
-- See Note [Skolemising type variables]
freshenTyCoVarsX :: (Name -> Type -> DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mk_tcv
  = (Name -> Type -> TcM DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
instantiateTyVarsX Name -> Type -> TcM DFunId
freshen_tcv
  where
    freshen_tcv :: Name -> Kind -> TcM TcTyVar
    freshen_tcv :: Name -> Type -> TcM DFunId
freshen_tcv Name
name Type
kind
      = do { loc  <- TcRn SrcSpan
getSrcSpanM
           ; uniq <- newUnique
           ; let !occ_name = Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName Name
name
                    -- Force so we don't retain reference to the old
                    -- name and id.   See (#19619) for more discussion
                 new_name = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
uniq OccName
occ_name SrcSpan
loc
           ; return (mk_tcv new_name kind) }

{- 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) Clone the variable to give a fresh unique.  This is essential.
   Consider (tc160)
       type Foo x = forall a. a -> x
   And typecheck the expression
       (e :: Foo (Foo ())
   We will skolemise the signature, but after expanding synonyms it
   looks like
        forall a. a -> forall a. a -> x
   We don't want to make two big-lambdas with the same unique!

d) We retain locations. Because the location of the variable is the correct
   location to report in errors (e.g. in the signature). We don't want the
   location to change to the body of the function, which does *not* explicitly
   bind the variable.

e) 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.

Example: 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 HsOverLit GhcRn
lit ExpRhoType
res_ty
  = do { mb_lit' <- HsOverLit GhcRn -> ExpRhoType -> TcM (Maybe (HsOverLit GhcTc))
tcShortCutLit HsOverLit GhcRn
lit ExpRhoType
res_ty
       ; case mb_lit' of
            Just HsOverLit GhcTc
lit' -> HsOverLit GhcTc -> TcM (HsOverLit GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return HsOverLit GhcTc
lit'
            Maybe (HsOverLit GhcTc)
Nothing   -> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit HsOverLit GhcRn
lit ExpRhoType
res_ty }

-- Does not handle things that 'shortCutLit' can handle. See also
-- newOverloadedLit in GHC.Tc.Utils.Unify
newNonTrivialOverloadedLit :: HsOverLit GhcRn
                           -> ExpRhoType
                           -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit :: HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit
  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 = OverLitRn Bool
rebindable (L SrcSpanAnnN
loc Name
meth_name) })
  ExpRhoType
res_ty
  = do  { hs_lit <- OverLitVal -> TcM (HsLit GhcTc)
mkOverLit OverLitVal
val
        ; let lit_ty = HsLit GhcTc -> Type
forall (p :: Pass). IsPass p => HsLit (GhcPass p) -> Type
hsLitType HsLit GhcTc
hs_lit
        ; (_, fi') <- tcSyntaxOp orig (mkRnSyntaxExpr meth_name)
                                      [synKnownType lit_ty] res_ty $
                      \[Type]
_ [Type]
_ -> () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        ; let L _ witness = mkHsSyntaxApps (l2l loc) fi' [nlHsLit hs_lit]
        ; res_ty <- readExpType res_ty
        ; return (lit { ol_ext = OverLitTc { ol_rebindable = rebindable
                                           , ol_witness = witness
                                           , ol_type = res_ty } }) }
  where
    orig :: CtOrigin
orig = HsOverLit GhcRn -> CtOrigin
LiteralOrigin HsOverLit GhcRn
lit

------------
mkOverLit :: OverLitVal -> TcM (HsLit GhcTc)
mkOverLit :: OverLitVal -> TcM (HsLit GhcTc)
mkOverLit (HsIntegral IntegralLit
i)
  = do  { integer_ty <- Name -> IOEnv (Env TcGblEnv TcLclEnv) Type
tcMetaTy Name
integerTyConName
        ; return (XLit $ HsInteger  (il_text i) (il_value i) integer_ty) }

mkOverLit (HsFractional FractionalLit
r)
  = do  { rat_ty <- Name -> IOEnv (Env TcGblEnv TcLclEnv) Type
tcMetaTy Name
rationalTyConName
        ; return (XLit $ HsRat r rat_ty) }

mkOverLit (HsIsString SourceText
src FastString
s) = HsLit GhcTc -> TcM (HsLit GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsString GhcTc -> FastString -> HsLit GhcTc
forall x. XHsString x -> FastString -> HsLit x
HsString XHsString GhcTc
SourceText
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 SrcSpanAnnN
_ Name
user_nm))
  | Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
user_nm
  = do rhs <- CtOrigin -> Name -> [Type] -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
orig Name
std_nm [Type
ty]
       return (std_nm, rhs)

tcSyntaxName CtOrigin
orig Type
ty (Name
std_nm, HsExpr GhcRn
user_nm_expr) = do
    std_id <- Name -> TcM DFunId
tcLookupId Name
std_nm
    let
        ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
        sigma1         = [DFunId] -> [Type] -> Type -> Type
HasDebugCallStack => [DFunId] -> [Type] -> 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.

    span <- getSrcSpanM
    addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1 span) $ do

        -- Check that the user-supplied thing has the
        -- same type as the standard one.
        -- Tiresome jiggling because tcCheckSigma takes a located expression
     expr <- tcCheckPolyExpr (L (noAnnSrcSpan span) user_nm_expr) sigma1
     hasFixedRuntimeRepRes std_nm user_nm_expr sigma1
     return (std_nm, unLoc expr)

syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> SrcSpan -> TidyEnv
               -> ZonkM (TidyEnv, SDoc)
syntaxNameCtxt :: HsExpr GhcRn
-> CtOrigin -> Type -> SrcSpan -> TidyEnv -> ZonkM (TidyEnv, SDoc)
syntaxNameCtxt HsExpr GhcRn
name CtOrigin
orig Type
ty SrcSpan
loc TidyEnv
tidy_env = (TidyEnv, SDoc) -> ZonkM (TidyEnv, SDoc)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
msg)
  where
    msg :: SDoc
msg = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"When checking that" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
name)
                          SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(needed by a syntactic construct)"
               , Arity -> SDoc -> SDoc
nest Arity
2 (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"has the required type:"
                         SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env Type
ty))
               , Arity -> SDoc -> SDoc
nest Arity
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtOrigin
orig, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"at" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
loc])]

{-
************************************************************************
*                                                                      *
                FixedRuntimeRep
*                                                                      *
************************************************************************
-}

-- | Check that the result type of an expression has a fixed runtime representation.
--
-- Used only for arrow operations such as 'arr', 'first', etc.
hasFixedRuntimeRepRes :: Name -> HsExpr GhcRn -> TcSigmaType -> TcM ()
hasFixedRuntimeRepRes :: Name -> HsExpr GhcRn -> Type -> TcRn ()
hasFixedRuntimeRepRes Name
std_nm HsExpr GhcRn
user_expr Type
ty = (Arity -> TcRn ()) -> Maybe Arity -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Arity -> TcRn ()
do_check Maybe Arity
mb_arity
  where
   do_check :: Arity -> TcM ()
   do_check :: Arity -> TcRn ()
do_check Arity
arity =
     let res_ty :: Type
res_ty = Arity -> (Type -> Type) -> Type -> Type
forall a. Arity -> (a -> a) -> a -> a
nTimes Arity
arity ((PiTyBinder, Type) -> Type
forall a b. (a, b) -> b
snd ((PiTyBinder, Type) -> Type)
-> (Type -> (PiTyBinder, Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (PiTyBinder, Type)
splitPiTy) Type
ty
     in HasDebugCallStack => FixedRuntimeRepContext -> Type -> TcRn ()
FixedRuntimeRepContext -> Type -> TcRn ()
hasFixedRuntimeRep_syntactic (FRRArrowContext -> FixedRuntimeRepContext
FRRArrow (FRRArrowContext -> FixedRuntimeRepContext)
-> FRRArrowContext -> FixedRuntimeRepContext
forall a b. (a -> b) -> a -> b
$ HsExpr GhcRn -> FRRArrowContext
ArrowFun HsExpr GhcRn
user_expr) Type
res_ty
   mb_arity :: Maybe Arity
   mb_arity :: Maybe Arity
mb_arity -- arity of the arrow operation, counting type-level arguments
     | Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
arrAName     -- result used as an argument in, e.g., do_premap
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
3
     | Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
composeAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
5
     | Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
firstAName   -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
4
     | Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
appAName     -- result used as an argument in, e.g., dsCmd/HsCmdArrApp/HsHigherOrderApp
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
2
     | Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
choiceAName  -- result used as an argument in, e.g., HsCmdIf
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
5
     | Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
loopAName    -- result used as an argument in, e.g., HsCmdIf
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
4
     | Bool
otherwise
     = Maybe Arity
forall a. Maybe a
Nothing

{-
************************************************************************
*                                                                      *
                Class instances
*                                                                      *
************************************************************************
-}

getOverlapFlag :: Maybe OverlapMode   -- User pragma if any
               -> TcM OverlapFlag
-- Construct the OverlapFlag from the global module flags,
-- but if the overlap_mode argument is (Just m),
--     set the OverlapMode to 'm'
--
-- The overlap_mode argument comes from a user pragma on the instance decl:
--    Pragma                      overlap_mode_prag
--    -----------------------------------------
--    {-# OVERLAPPABLE #-}        Overlappable
--    {-# OVERLAPPING #-}         Overlapping
--    {-# OVERLAPS #-}            Overlaps
--    {-# INCOHERENT #-}          Incoherent   -- if -fspecialise-incoherent (on by default)
--    {-# INCOHERENT #-}          NonCanonical -- if -fno-specialise-incoherent
-- See Note [Rules for instance lookup] in GHC.Core.InstEnv

getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag Maybe OverlapMode
overlap_mode_prag
  = do  { dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
        ; let overlap_ok               = Extension -> DynFlags -> Bool
xopt Extension
LangExt.OverlappingInstances DynFlags
dflags
              incoherent_ok            = Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances  DynFlags
dflags
              noncanonical_incoherence = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_SpecialiseIncoherents DynFlags
dflags

              overlap_mode
                | Just OverlapMode
m <- Maybe OverlapMode
overlap_mode_prag = OverlapMode
m
                | Bool
incoherent_ok               = SourceText -> OverlapMode
Incoherent SourceText
NoSourceText
                | Bool
overlap_ok                  = SourceText -> OverlapMode
Overlaps   SourceText
NoSourceText
                | Bool
otherwise                   = SourceText -> OverlapMode
NoOverlap  SourceText
NoSourceText

              -- final_overlap_mode: the `-fspecialise-incoherents` flag controls the
              -- meaning of the `Incoherent` overlap mode: as either an Incoherent overlap
              -- flag, or a NonCanonical overlap flag.
              -- See GHC.Core.InstEnv Note [Coherence and specialisation: overview]
              final_overlap_mode
                | Incoherent SourceText
s <- OverlapMode
overlap_mode
                , Bool
noncanonical_incoherence       = SourceText -> OverlapMode
NonCanonical SourceText
s
                | Bool
otherwise                      = OverlapMode
overlap_mode

        ; return (OverlapFlag { isSafeOverlap = safeLanguageOn dflags
                              , overlapMode   = final_overlap_mode }) }


tcGetInsts :: TcM [ClsInst]
-- Gets the local class instances.
tcGetInsts :: TcM [ClsInst]
tcGetInsts = (TcGblEnv -> [ClsInst])
-> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv -> TcM [ClsInst]
forall a b.
(a -> b)
-> IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
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   -- User pragma
           -> Name -> [TyVar] -> ThetaType
           -> Class -> [Type] -> Maybe (WarningTxt GhcRn) -> TcM ClsInst
newClsInst :: Maybe OverlapMode
-> Name
-> [DFunId]
-> [Type]
-> Class
-> [Type]
-> Maybe (WarningTxt GhcRn)
-> TcM ClsInst
newClsInst Maybe OverlapMode
overlap_mode Name
dfun_name [DFunId]
tvs [Type]
theta Class
clas [Type]
tys Maybe (WarningTxt GhcRn)
warn
  = do { (subst, tvs') <- [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyVarBndrs [DFunId]
tvs
             -- Be sure to freshen those type variables,
             -- so they are sure not to appear in any lookup
       ; let tys' = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys

             dfun = Name -> [DFunId] -> [Type] -> Class -> [Type] -> DFunId
mkDictFunId Name
dfun_name [DFunId]
tvs [Type]
theta Class
clas [Type]
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

       ; oflag <- getOverlapFlag overlap_mode
       ; let cls_inst = DFunId
-> OverlapFlag
-> [DFunId]
-> Class
-> [Type]
-> Maybe (WarningTxt GhcRn)
-> ClsInst
mkLocalClsInst DFunId
dfun OverlapFlag
oflag [DFunId]
tvs' Class
clas [Type]
tys' Maybe (WarningTxt GhcRn)
warn

       ; when (isOrphan (is_orphan cls_inst)) $
         addDiagnostic (TcRnOrphanInstance $ Left cls_inst)

       ; return cls_inst }

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
      ; 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 = TcGblEnv -> InstEnv
tcg_inst_env TcGblEnv
env
            !init_insts = TcGblEnv -> [ClsInst]
tcg_insts TcGblEnv
env
      ; (inst_env', cls_insts') <- foldlM addLocalInst
                                          (init_inst_env, init_insts)
                                          dfuns
      ; let env' = TcGblEnv
env { tcg_insts    = cls_insts'
                       , tcg_inst_env = inst_env' }
      ; setGblEnv env' 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
         ; isGHCi <- TcRn Bool
getIsGHCi
         ; eps    <- getEps
         ; tcg_env <- 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'
                 | Bool
isGHCi    = InstEnv -> ClsInst -> InstEnv
deleteFromInstEnv InstEnv
home_ie ClsInst
ispec
                 | Bool
otherwise = InstEnv
home_ie

               global_ie = ExternalPackageState -> InstEnv
eps_inst_env ExternalPackageState
eps
               inst_envs = 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 = InstEnvs -> ClsInst -> [ClsInst]
checkFunDeps InstEnvs
inst_envs ClsInst
ispec
         ; unless (null inconsistent_ispecs) $
           funDepErr ispec inconsistent_ispecs

             -- Check for duplicate instance decls.
         ; let (_tvs, cls, tys) = instanceHead ispec
               (matches, _, _)  = lookupInstEnv False inst_envs cls tys
               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)
         ; unless (null dups) $
           dupInstErr ispec (head dups)

         ; return (extendInstEnv home_ie' ispec, ispec : 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)

************************************************************************
*                                                                      *
                Family instances
*                                                                      *
************************************************************************
-}

-- All type variables in a FamInst must be fresh. This function
-- creates the fresh variables and applies the necessary substitution
-- It is defined here to avoid a dependency from FamInstEnv on the monad
-- code.

newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
-- Freshen the type variables of the FamInst branches
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
newFamInst FamFlavor
flavor CoAxiom Unbranched
axiom
  | CoAxBranch { cab_tvs :: CoAxBranch -> [DFunId]
cab_tvs = [DFunId]
tvs
               , cab_cvs :: CoAxBranch -> [DFunId]
cab_cvs = [DFunId]
cvs
               , cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs
               , cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs } <- CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
axiom
  = do { -- Freshen the type variables
         (subst, tvs') <- [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyVarBndrs [DFunId]
tvs
       ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
       ; let lhs'     = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
lhs
             rhs'     = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy  Subst
subst Type
rhs

       ; let fam_inst = FamFlavor
-> CoAxiom Unbranched
-> [DFunId]
-> [DFunId]
-> [Type]
-> Type
-> FamInst
mkLocalFamInst FamFlavor
flavor CoAxiom Unbranched
axiom [DFunId]
tvs' [DFunId]
cvs' [Type]
lhs' Type
rhs'
       ; when (isOrphan (fi_orphan fam_inst)) $
         addDiagnostic (TcRnOrphanInstance $ Right fam_inst)

       ; return fam_inst }


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

traceDFuns :: [ClsInst] -> TcRn ()
traceDFuns :: [ClsInst] -> TcRn ()
traceDFuns [ClsInst]
ispecs
  = String -> SDoc -> TcRn ()
traceTc String
"Adding instances:" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
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 -> Arity -> SDoc -> SDoc
hang (DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ClsInst -> DFunId
instanceDFunId ClsInst
ispec) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
forall doc. IsLine doc => doc
colon)
                  Arity
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
  = (UnitState -> NonEmpty ClsInst -> TcRnMessage)
-> NonEmpty ClsInst -> TcRn ()
addClsInstsErr UnitState -> NonEmpty ClsInst -> TcRnMessage
TcRnFunDepConflict (ClsInst
ispec ClsInst -> [ClsInst] -> NonEmpty ClsInst
forall a. a -> [a] -> NonEmpty a
NE.:| [ClsInst]
ispecs)

dupInstErr :: ClsInst -> ClsInst -> TcRn ()
dupInstErr :: ClsInst -> ClsInst -> TcRn ()
dupInstErr ClsInst
ispec ClsInst
dup_ispec
  = (UnitState -> NonEmpty ClsInst -> TcRnMessage)
-> NonEmpty ClsInst -> TcRn ()
addClsInstsErr UnitState -> NonEmpty ClsInst -> TcRnMessage
TcRnDupInstanceDecls (ClsInst
ispec ClsInst -> [ClsInst] -> NonEmpty ClsInst
forall a. a -> [a] -> NonEmpty a
NE.:| [ClsInst
dup_ispec])

addClsInstsErr :: (UnitState -> NE.NonEmpty ClsInst -> TcRnMessage)
               -> NE.NonEmpty ClsInst
               -> TcRn ()
addClsInstsErr :: (UnitState -> NonEmpty ClsInst -> TcRnMessage)
-> NonEmpty ClsInst -> TcRn ()
addClsInstsErr UnitState -> NonEmpty ClsInst -> TcRnMessage
mkErr NonEmpty ClsInst
ispecs = do
   unit_state <- HasDebugCallStack => HscEnv -> UnitState
HscEnv -> UnitState
hsc_units (HscEnv -> UnitState)
-> IOEnv (Env TcGblEnv TcLclEnv) HscEnv
-> IOEnv (Env TcGblEnv TcLclEnv) UnitState
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
getTopEnv
   setSrcSpan (getSrcSpan (NE.head sorted)) $
      addErr $ mkErr unit_state sorted
 where
   sorted :: NonEmpty ClsInst
sorted = (ClsInst -> ClsInst -> Ordering)
-> NonEmpty ClsInst -> NonEmpty ClsInst
forall a. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
NE.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) NonEmpty 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