{-# 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,
     topInstantiate,
     instantiateSigma,
     instCall, instDFunType, instStupidTheta, instTyVarsWith,
     newWanted, newWanteds,

     tcInstType, tcInstTypeBndrs,
     tcSkolemiseInvisibleBndrs,
     tcInstSkolTyVars, tcInstSkolTyVarsX,
     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  ( heqDataCon, 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.Predicate
import GHC.Core ( Expr(..), isOrphan ) -- For the Coercion constructor
import GHC.Core.Type
import GHC.Core.TyCo.Ppr ( debugPprType )
import GHC.Core.Class( Class )
import GHC.Core.DataCon
import GHC.Core.Coercion.Axiom

import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
import {-# SOURCE #-}   GHC.Tc.Utils.Unify( unifyType )
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.Types.Id.Make( mkDictFunId )
import GHC.Types.Basic ( TypeOrKind(..), Arity )
import GHC.Types.Error
import GHC.Types.SourceText
import GHC.Types.SrcLoc as SrcLoc
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Var
import qualified GHC.LanguageExtensions as LangExt

import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Utils.Outputable

import GHC.Unit.State
import GHC.Unit.External

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 { 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 -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (DFunId -> Type
idType DFunId
id) [Type]
ty_args
             ([Type]
theta, Type
_caller_knows_this) = Type -> ([Type], Type)
tcSplitPhiTy Type
ty
       ; HsWrapper
wrap <- Bool -> TcM HsWrapper -> TcM HsWrapper
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (Type -> Bool
isForAllTy Type
ty) Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
isSingleton [Type]
theta) (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
                 CtOrigin -> [Type] -> [Type] -> TcM HsWrapper
instCall CtOrigin
origin [Type]
ty_args [Type]
theta

       ; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap HsWrapper
wrap (XVar GhcTc -> LIdP GhcTc -> HsExpr GhcTc
forall p. XVar p -> LIdP p -> HsExpr p
HsVar XVar GhcTc
NoExtField
noExtField (DFunId -> LocatedAn NameAnn DFunId
forall a an. a -> LocatedAn an a
noLocA 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 :: SkolemInfo
             -> TcSigmaType
             -> TcM ( HsWrapper
                    , [(Name,TyVar)]     -- All skolemised variables
                    , [EvVar]            -- All "given"s
                    , TcRhoType )
-- See Note [Skolemisation]
topSkolemise :: SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
topSkolemise SkolemInfo
skolem_info Type
ty
  = Subst
-> HsWrapper
-> [(Name, DFunId)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, DFunId)], [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]
    go :: Subst
-> HsWrapper
-> [(Name, DFunId)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
go Subst
subst HsWrapper
wrap [(Name, DFunId)]
tv_prs [DFunId]
ev_vars Type
ty
      | ([DFunId]
tvs, [Type]
theta, Type
inner_ty) <- Type -> ([DFunId], [Type], Type)
tcSplitSigmaTy Type
ty
      , 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
subst', [DFunId]
tvs1) <- SkolemInfo -> Subst -> [DFunId] -> TcM (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skolem_info Subst
subst [DFunId]
tvs
           ; [DFunId]
ev_vars1       <- [Type] -> TcM [DFunId]
newEvVars (HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst' [Type]
theta)
           ; Subst
-> HsWrapper
-> [(Name, DFunId)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, DFunId)], [DFunId], Type)
go Subst
subst'
                (HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> [DFunId] -> HsWrapper
mkWpTyLams [DFunId]
tvs1 HsWrapper -> HsWrapper -> HsWrapper
<.> [DFunId] -> HsWrapper
mkWpEvLams [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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap, [(Name, DFunId)]
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

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 { ([DFunId]
_, HsWrapper
wrap1, Type
body3) <- CtOrigin
-> [DFunId] -> [Type] -> Type -> TcM ([DFunId], HsWrapper, Type)
instantiateSigma CtOrigin
orig [DFunId]
tvs [Type]
theta Type
body2

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

       ; (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap1, Type
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 -> [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
-> [DFunId] -> [Type] -> Type -> TcM ([DFunId], HsWrapper, Type)
instantiateSigma CtOrigin
orig [DFunId]
tvs [Type]
theta Type
body_ty
  = do { (Subst
subst, [DFunId]
inst_tvs) <- (Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId))
-> Subst -> [DFunId] -> TcM (Subst, [DFunId])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
empty_subst [DFunId]
tvs
       ; let inst_theta :: [Type]
inst_theta  = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta
             inst_body :: Type
inst_body   = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
body_ty
             inst_tv_tys :: [Type]
inst_tv_tys = [DFunId] -> [Type]
mkTyVarTys [DFunId]
inst_tvs

       ; HsWrapper
wrap <- CtOrigin -> [Type] -> [Type] -> TcM HsWrapper
instCall CtOrigin
orig [Type]
inst_tv_tys [Type]
inst_theta
       ; String -> SDoc -> TcRn ()
traceTc String
"Instantiating"
                 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"origin" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CtOrigin -> SDoc
pprCtOrigin CtOrigin
orig
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tvs"   SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [DFunId] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunId]
tvs
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"theta" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
theta
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"type" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
debugPprType Type
body_ty
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"with" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Type -> SDoc) -> [Type] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
debugPprType [Type]
inst_tv_tys)
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"theta:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>  [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
inst_theta ])

      ; ([DFunId], HsWrapper, Type) -> TcM ([DFunId], HsWrapper, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DFunId]
inst_tvs, HsWrapper
wrap, Type
inst_body) }
  where
    free_tvs :: VarSet
free_tvs = Type -> VarSet
tyCoVarsOfType Type
body_ty VarSet -> VarSet -> VarSet
`unionVarSet` [Type] -> VarSet
tyCoVarsOfTypes [Type]
theta
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet
free_tvs VarSet -> [DFunId] -> VarSet
`delVarSetList` [DFunId]
tvs)
    empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope

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 { Coercion
co <- CtOrigin -> TypeOrKind -> Role -> Type -> Type -> TcM Coercion
emitWantedEq CtOrigin
orig TypeOrKind
KindLevel Role
Nominal Type
ty_kind Type
tv_kind
           ; Subst -> [DFunId] -> [Type] -> TcM Subst
go (Subst -> DFunId -> Type -> Subst
extendTvSubstAndInScope Subst
subst DFunId
tv (Type
ty Type -> Coercion -> Type
`mkCastTy` Coercion
co)) [DFunId]
tvs [Type]
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  { HsWrapper
dict_app <- CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
theta
        ; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
dict_app HsWrapper -> HsWrapper -> HsWrapper
<.> [Type] -> HsWrapper
mkWpTyApps [Type]
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 { [EvTerm]
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 Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
go [Type]
preds
       ; String -> SDoc -> TcRn ()
traceTc String
"instCallConstraints" ([EvTerm] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EvTerm]
evs)
       ; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing Type
ty1 Type
ty2
           ; EvTerm -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> EvTerm
evCoercion Coercion
co) }

       -- Try short-cut #2
     | Just (TyCon
tc, args :: [Type]
args@[Type
_, Type
_, Type
ty1, Type
ty2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
pred
     , TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
     = do { Coercion
co <- Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing Type
ty1 Type
ty2
          ; EvTerm -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp (DataCon -> DFunId
dataConWrapId DataCon
heqDataCon) [Type]
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 ([Type], [Type])
instDFunType DFunId
dfun_id [DFunInstType]
dfun_inst_tys
  = do { (Subst
subst, [Type]
inst_tys) <- Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go Subst
empty_subst [DFunId]
dfun_tvs [DFunInstType]
dfun_inst_tys
       ; ([Type], [Type]) -> TcM ([Type], [Type])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
inst_tys, HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
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
subst', [Type]
tys) <- Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go (Subst -> DFunId -> Type -> Subst
extendTvSubstAndInScope Subst
subst DFunId
tv Type
ty)
                                 [DFunId]
tvs
                                 [DFunInstType]
mb_tys
           ; (Subst, [Type]) -> TcM (Subst, [Type])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst', Type
ty Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tys) }
    go Subst
subst (DFunId
tv:[DFunId]
tvs) (DFunInstType
Nothing : [DFunInstType]
mb_tys)
      = do { (Subst
subst', DFunId
tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv
           ; (Subst
subst'', [Type]
tys) <- Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go Subst
subst' [DFunId]
tvs [DFunInstType]
mb_tys
           ; (Subst, [Type]) -> TcM (Subst, [Type])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst'', DFunId -> Type
mkTyVarTy DFunId
tv' Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
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  { HsWrapper
_co <- CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
theta -- Discard the coercion
        ; () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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]
-- 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 { ([Type]
extra_args, Type
kind') <- Arity -> Type -> TcM ([Type], Type)
tcInstInvisibleTyBindersN Arity
n_invis 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 -> [Type] -> Type
mkAppTys Type
ty [Type]
extra_args, Type
kind') }
  where
    n_invis :: Arity
n_invis = Type -> Arity
invisibleTyBndrCount Type
kind

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 (TyVarBinder
bndr, Type
body) <- Type -> Maybe (TyVarBinder, Type)
tcSplitForAllTyVarBinder_maybe Type
kind
      , ForAllTyFlag -> Bool
isInvisibleForAllTyFlag (TyVarBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag TyVarBinder
bndr)
      = do { (Subst
subst', Type
arg) <- Subst -> DFunId -> TcM (Subst, Type)
tcInstInvisibleTyBinder Subst
subst (TyVarBinder -> DFunId
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
bndr)
           ; ([Type]
args, Type
inner_ty) <- t -> Subst -> Type -> TcM ([Type], Type)
go (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Subst
subst' Type
body
           ; ([Type], Type) -> TcM ([Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args, Type
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
subst', DFunId
tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv
       ; (Subst, Type) -> TcM (Subst, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst', DFunId -> Type
mkTyVarTy DFunId
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] -> TcM (Subst, [DFunId]))
-> DFunId -> TcM ([(Name, DFunId)], [Type], Type)
tcInstType [DFunId] -> TcM (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
subst, [DFunId]
tyvars') <- [DFunId] -> TcM (Subst, [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' :: Subst
subst'  = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Type -> VarSet
tyCoVarsOfType Type
rho)
       ; ([(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 ([(Name, DFunId)]
tv_prs, HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst' [Type]
theta, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst' Type
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, InvisTVBinder)], [Type], Type)
tcInstTypeBndrs Type
poly_ty
  | [InvisTVBinder] -> Bool
forall a. [a] -> 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)], [Type], Type)
-> TcM ([(Name, InvisTVBinder)], [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
subst, [InvisTVBinder]
tyvars') <- (Subst
 -> InvisTVBinder
 -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, InvisTVBinder))
-> Subst
-> [InvisTVBinder]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [InvisTVBinder])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM Subst
-> InvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, InvisTVBinder)
inst_invis_bndr Subst
emptySubst [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' :: Subst
subst'  = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Type -> VarSet
tyCoVarsOfType Type
rho)
       ; ([(Name, InvisTVBinder)], [Type], Type)
-> TcM ([(Name, InvisTVBinder)], [Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, InvisTVBinder)]
tv_prs, HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst' [Type]
theta, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst' Type
tau) }
  where
    ([InvisTVBinder]
tyvars, Type
rho) = Type -> ([InvisTVBinder], 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
-> InvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, InvisTVBinder)
inst_invis_bndr Subst
subst (Bndr DFunId
tv Specificity
spec)
      = do { (Subst
subst', DFunId
tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarTyVarX Subst
subst DFunId
tv
           ; (Subst, InvisTVBinder)
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, InvisTVBinder)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst', DFunId -> Specificity -> InvisTVBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr DFunId
tv' Specificity
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 { SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo SkolemInfoAnon
skol_info_anon
             ; (Subst
subst, [DFunId]
inst_tvs) <- SkolemInfo -> [DFunId] -> TcM (Subst, [DFunId])
tcInstSuperSkolTyVars SkolemInfo
skol_info [DFunId]
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 :: [Type]
inst_tys = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys
                   skol_info_anon :: SkolemInfoAnon
skol_info_anon = Class -> [Type] -> SkolemInfoAnon
mkClsInstSkol Class
cls [Type]
inst_tys }

       ; let inst_theta :: [Type]
inst_theta = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta
       ; (SkolemInfoAnon, [DFunId], [Type], Class, [Type])
-> TcM (SkolemInfoAnon, [DFunId], [Type], Class, [Type])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SkolemInfoAnon
skol_info_anon, [DFunId]
inst_tvs, [Type]
inst_theta, Class
cls, [Type]
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] -> TcM (Subst, [DFunId])
tcInstSkolTyVars SkolemInfo
skol_info = SkolemInfo -> Subst -> [DFunId] -> TcM (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
emptySubst

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

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] -> TcM (Subst, [DFunId])
tcInstSuperSkolTyVars SkolemInfo
skol_info = SkolemInfo -> Subst -> [DFunId] -> TcM (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] -> TcM (Subst, [DFunId])
tcInstSuperSkolTyVarsX SkolemInfo
skol_info Subst
subst = SkolemInfo -> Bool -> Subst -> [DFunId] -> TcM (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] -> TcM (Subst, [DFunId])
tcInstSkolTyVarsPushLevel SkolemInfo
skol_info Bool
overlappable Subst
subst [DFunId]
tvs
  = do { TcLevel
tc_lvl <- TcM TcLevel
getTcLevel
       -- Do not retain the whole TcLclEnv
       ; let !pushed_lvl :: TcLevel
pushed_lvl = TcLevel -> TcLevel
pushTcLevel TcLevel
tc_lvl
       ; SkolemInfo
-> TcLevel -> Bool -> Subst -> [DFunId] -> TcM (Subst, [DFunId])
tcInstSkolTyVarsAt SkolemInfo
skol_info TcLevel
pushed_lvl Bool
overlappable Subst
subst [DFunId]
tvs }

tcInstSkolTyVarsAt :: SkolemInfo -> TcLevel -> Bool
                   -> Subst -> [TyVar]
                   -> TcM (Subst, [TcTyVar])
tcInstSkolTyVarsAt :: SkolemInfo
-> TcLevel -> Bool -> Subst -> [DFunId] -> TcM (Subst, [DFunId])
tcInstSkolTyVarsAt SkolemInfo
skol_info TcLevel
lvl Bool
overlappable Subst
subst [DFunId]
tvs
  = (Name -> Type -> DFunId)
-> Subst -> [DFunId] -> TcM (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
       ; TcLevel
lvl           <- TcM TcLevel
getTcLevel
       ; SkolemInfo
skol_info     <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo SkolemInfoAnon
skol_info
       ; let details :: TcTyVarDetails
details = SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info TcLevel
lvl Bool
False
             mk_skol_tv :: Name -> Type -> TcM DFunId
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
subst, [DFunId]
tvs') <- (Name -> Type -> TcM DFunId)
-> Subst -> [DFunId] -> TcM (Subst, [DFunId])
instantiateTyVarsX Name -> Type -> TcM DFunId
mk_skol_tv Subst
emptySubst [DFunId]
tvs
       ; ([DFunId], Type) -> TcM ([DFunId], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DFunId]
tvs', HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
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] -> TcM (Subst, [DFunId])
instantiateTyVarsX Name -> Type -> TcM DFunId
mk_tv Subst
subst [DFunId]
tvs
  = case [DFunId]
tvs of
      []       -> (Subst, [DFunId]) -> TcM (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)
                     ; DFunId
tv' <- Name -> Type -> TcM DFunId
mk_tv (DFunId -> Name
tyVarName DFunId
tv) Type
kind1
                     ; let subst1 :: Subst
subst1 = Subst -> DFunId -> DFunId -> Subst
extendTCvSubstWithClone Subst
subst DFunId
tv DFunId
tv'
                     ; (Subst
subst', [DFunId]
tvs') <- (Name -> Type -> TcM DFunId)
-> Subst -> [DFunId] -> TcM (Subst, [DFunId])
instantiateTyVarsX Name -> Type -> TcM DFunId
mk_tv Subst
subst1 [DFunId]
tvs
                     ; (Subst, [DFunId]) -> TcM (Subst, [DFunId])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst', DFunId
tv'DFunId -> [DFunId] -> [DFunId]
forall a. a -> [a] -> [a]
:[DFunId]
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] -> TcM (Subst, [DFunId])
freshenTyVarBndrs = (Name -> Type -> DFunId) -> [DFunId] -> TcM (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] -> TcM (Subst, [DFunId])
freshenCoVarBndrsX Subst
subst = (Name -> Type -> DFunId)
-> Subst -> [DFunId] -> TcM (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mkCoVar Subst
subst

------------------
freshenTyCoVars :: (Name -> Kind -> TyCoVar)
                -> [TyVar] -> TcM (Subst, [TyCoVar])
freshenTyCoVars :: (Name -> Type -> DFunId) -> [DFunId] -> TcM (Subst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mk_tcv = (Name -> Type -> DFunId)
-> Subst -> [DFunId] -> TcM (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] -> TcM (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mk_tcv
  = (Name -> Type -> TcM DFunId)
-> Subst -> [DFunId] -> TcM (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 { SrcSpan
loc  <- TcRn SrcSpan
getSrcSpanM
           ; Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
           ; let !occ_name :: OccName
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 :: Name
new_name = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
uniq OccName
occ_name SrcSpan
loc
           ; DFunId -> TcM DFunId
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> DFunId
mk_tcv Name
new_name Type
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 { Maybe (HsOverLit GhcTc)
mb_lit' <- HsOverLit GhcRn -> ExpRhoType -> TcM (Maybe (HsOverLit GhcTc))
tcShortCutLit HsOverLit GhcRn
lit ExpRhoType
res_ty
       ; case Maybe (HsOverLit GhcTc)
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
_ Name
meth_name) })
  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
-> ([Type] -> [Type] -> TcRn ())
-> TcM ((), SyntaxExprTc)
forall a.
CtOrigin
-> SyntaxExprRn
-> [SyntaxOpType]
-> ExpRhoType
-> ([Type] -> [Type] -> TcM a)
-> TcM (a, SyntaxExprTc)
tcSyntaxOp CtOrigin
orig (Name -> SyntaxExprRn
mkRnSyntaxExpr Name
meth_name)
                                      [Type -> SyntaxOpType
synKnownType Type
lit_ty] ExpRhoType
res_ty (([Type] -> [Type] -> TcRn ()) -> TcM ((), SyntaxExprTc))
-> ([Type] -> [Type] -> TcRn ()) -> TcM ((), SyntaxExprTc)
forall a b. (a -> b) -> a -> b
$
                      \[Type]
_ [Type]
_ -> () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        ; let L SrcSpanAnnA
_ HsExpr GhcTc
witness = SyntaxExprTc -> [LHsExpr GhcTc] -> LHsExpr GhcTc
nlHsSyntaxApps SyntaxExprTc
fi' [HsLit GhcTc -> LHsExpr GhcTc
forall (p :: Pass). HsLit (GhcPass p) -> LHsExpr (GhcPass p)
nlHsLit HsLit GhcTc
hs_lit]
        ; Type
res_ty <- ExpRhoType -> IOEnv (Env TcGblEnv TcLclEnv) Type
forall (m :: * -> *). MonadIO m => ExpRhoType -> m Type
readExpType ExpRhoType
res_ty
        ; HsOverLit GhcTc -> TcM (HsOverLit GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsOverLit GhcRn
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  { Type
integer_ty <- Name -> IOEnv (Env TcGblEnv TcLclEnv) Type
tcMetaTy Name
integerTyConName
        ; HsLit GhcTc -> TcM (HsLit GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 -> IOEnv (Env TcGblEnv TcLclEnv) Type
tcMetaTy Name
rationalTyConName
        ; HsLit GhcTc -> TcM (HsLit GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsRat GhcTc -> FractionalLit -> Type -> HsLit GhcTc
forall x. XHsRat x -> FractionalLit -> Type -> HsLit x
HsRat XHsRat GhcTc
NoExtField
noExtField FractionalLit
r Type
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 HsExpr GhcTc
rhs <- CtOrigin -> Name -> [Type] -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
orig Name
std_nm [Type
ty]
       (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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
        ([DFunId
tv], [Type]
_, Type
tau) = Type -> ([DFunId], [Type], Type)
tcSplitSigmaTy (DFunId -> Type
idType DFunId
std_id)
        sigma1 :: Type
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.

    SrcSpan
span <- TcRn SrcSpan
getSrcSpanM
    (TidyEnv -> ZonkM (TidyEnv, SDoc))
-> TcM (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall a. (TidyEnv -> ZonkM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (HsExpr GhcRn
-> CtOrigin -> Type -> SrcSpan -> TidyEnv -> ZonkM (TidyEnv, SDoc)
syntaxNameCtxt HsExpr GhcRn
user_nm_expr CtOrigin
orig Type
sigma1 SrcSpan
span) (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
     GenLocated SrcSpanAnnA (HsExpr GhcTc)
expr <- LHsExpr GhcRn -> Type -> TcM (LHsExpr GhcTc)
tcCheckPolyExpr (SrcSpanAnnA
-> HsExpr GhcRn -> GenLocated SrcSpanAnnA (HsExpr GhcRn)
forall l e. l -> e -> GenLocated l e
L (SrcSpan -> SrcSpanAnnA
forall ann. SrcSpan -> SrcAnn ann
noAnnSrcSpan SrcSpan
span) HsExpr GhcRn
user_nm_expr) Type
sigma1
     Name -> HsExpr GhcRn -> Type -> TcRn ()
hasFixedRuntimeRepRes Name
std_nm HsExpr GhcRn
user_nm_expr Type
sigma1
     (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
std_nm, GenLocated SrcSpanAnnA (HsExpr GhcTc) -> HsExpr GhcTc
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpanAnnA (HsExpr GhcTc)
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
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
arrAName     -- result used as an argument in, e.g., do_premap
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
3
     | Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
composeAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
5
     | Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
firstAName   -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
4
     | Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== 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
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
choiceAName  -- result used as an argument in, e.g., HsCmdIf
     = Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
5
     | Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== 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 -> 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
              noncanonical_incoherence :: Bool
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

              use :: OverlapMode -> OverlapFlag
use OverlapMode
x = 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)

              oflag :: OverlapFlag
oflag = OverlapFlag -> Maybe OverlapMode -> OverlapFlag
setOverlapModeMaybe OverlapFlag
default_oflag Maybe OverlapMode
overlap_mode
              final_oflag :: OverlapFlag
final_oflag = Bool -> OverlapFlag -> OverlapFlag
effective_oflag Bool
noncanonical_incoherence OverlapFlag
oflag
        ; OverlapFlag -> TcM OverlapFlag
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return OverlapFlag
final_oflag }
  where
    effective_oflag :: Bool -> OverlapFlag -> OverlapFlag
effective_oflag Bool
noncanonical_incoherence oflag :: OverlapFlag
oflag@OverlapFlag{ overlapMode :: OverlapFlag -> OverlapMode
overlapMode = OverlapMode
overlap_mode }
      = OverlapFlag
oflag { overlapMode = effective_overlap_mode noncanonical_incoherence 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 Note [Coherence and specialisation: overview]
    -- in GHC.Core.InstEnv for why we care about this distinction.
    effective_overlap_mode :: Bool -> OverlapMode -> OverlapMode
effective_overlap_mode Bool
noncanonical_incoherence = \case
        Incoherent SourceText
s | Bool
noncanonical_incoherence -> SourceText -> OverlapMode
NonCanonical SourceText
s
        OverlapMode
overlap_mode -> OverlapMode
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 -> Name -> [TyVar] -> ThetaType
           -> Class -> [Type] -> TcM ClsInst
newClsInst :: Maybe OverlapMode
-> Name -> [DFunId] -> [Type] -> Class -> [Type] -> TcM ClsInst
newClsInst Maybe OverlapMode
overlap_mode Name
dfun_name [DFunId]
tvs [Type]
theta Class
clas [Type]
tys
  = do { (Subst
subst, [DFunId]
tvs') <- [DFunId] -> TcM (Subst, [DFunId])
freshenTyVarBndrs [DFunId]
tvs
             -- Be sure to freshen those type variables,
             -- so they are sure not to appear in any lookup
       ; let tys' :: [Type]
tys' = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys

             dfun :: DFunId
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

       ; OverlapFlag
oflag <- Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag Maybe OverlapMode
overlap_mode
       ; let cls_inst :: ClsInst
cls_inst = DFunId -> OverlapFlag -> [DFunId] -> Class -> [Type] -> ClsInst
mkLocalClsInst DFunId
dfun OverlapFlag
oflag [DFunId]
tvs' Class
clas [Type]
tys'

       ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IsOrphan -> Bool
isOrphan (ClsInst -> IsOrphan
is_orphan ClsInst
cls_inst)) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         TcRnMessage -> TcRn ()
addDiagnostic (Either ClsInst FamInst -> TcRnMessage
TcRnOrphanInstance (Either ClsInst FamInst -> TcRnMessage)
-> Either ClsInst FamInst -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ ClsInst -> Either ClsInst FamInst
forall a b. a -> Either a b
Left ClsInst
cls_inst)

       ; ClsInst -> TcM ClsInst
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInst
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
      ; 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    = cls_insts'
                       , tcg_inst_env = inst_env' }
      ; TcGblEnv -> TcM a -> TcM a
forall gbl' lcl a gbl.
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 { 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 a. [a] -> 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, [Type]
tys) = ClsInst -> ([DFunId], Class, [Type])
instanceHead ClsInst
ispec
               ([InstMatch]
matches, PotentialUnifiers
_, [InstMatch]
_)  = Bool
-> InstEnvs
-> Class
-> [Type]
-> ([InstMatch], PotentialUnifiers, [InstMatch])
lookupInstEnv Bool
False InstEnvs
inst_envs Class
cls [Type]
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 a. [a] -> 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. HasCallStack => [a] -> a
head [ClsInst]
dups)

         ; (InstEnv, [ClsInst])
-> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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)

************************************************************************
*                                                                      *
                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
subst, [DFunId]
tvs') <- [DFunId] -> TcM (Subst, [DFunId])
freshenTyVarBndrs [DFunId]
tvs
       ; (Subst
subst, [DFunId]
cvs') <- Subst -> [DFunId] -> TcM (Subst, [DFunId])
freshenCoVarBndrsX Subst
subst [DFunId]
cvs
       ; let lhs' :: [Type]
lhs'     = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
lhs
             rhs' :: Type
rhs'     = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy  Subst
subst Type
rhs

       ; let fam_inst :: FamInst
fam_inst = FamFlavor
-> CoAxiom Unbranched
-> [DFunId]
-> [DFunId]
-> [Type]
-> Type
-> FamInst
mkLocalFamInst FamFlavor
flavor CoAxiom Unbranched
axiom [DFunId]
tvs' [DFunId]
cvs' [Type]
lhs' Type
rhs'
       ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IsOrphan -> Bool
isOrphan (FamInst -> IsOrphan
fi_orphan FamInst
fam_inst)) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         TcRnMessage -> TcRn ()
addDiagnostic (Either ClsInst FamInst -> TcRnMessage
TcRnOrphanInstance (Either ClsInst FamInst -> TcRnMessage)
-> Either ClsInst FamInst -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ FamInst -> Either ClsInst FamInst
forall a b. b -> Either a b
Right FamInst
fam_inst)

       ; FamInst -> TcM FamInst
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return FamInst
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
   UnitState
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
   SrcSpan -> TcRn () -> TcRn ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan (ClsInst -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan (NonEmpty ClsInst -> ClsInst
forall a. NonEmpty a -> a
NE.head NonEmpty ClsInst
sorted)) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
      TcRnMessage -> TcRn ()
addErr (TcRnMessage -> TcRn ()) -> TcRnMessage -> TcRn ()
forall a b. (a -> b) -> a -> b
$ UnitState -> NonEmpty ClsInst -> TcRnMessage
mkErr UnitState
unit_state NonEmpty ClsInst
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