{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DisambiguateRecordFields #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
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,
tcGetInsts, tcGetInstEnvs, getOverlapFlag,
tcExtendLocalInstEnv,
instCallConstraints, newMethodFromName,
tcSyntaxName,
tyCoVarsOfWC,
tyCoVarsOfCt, tyCoVarsOfCts,
) where
import GHC.Prelude
import GHC.Driver.Session
import GHC.Driver.Env
import GHC.Builtin.Types ( heqDataCon, eqDataCon, integerTyConName )
import GHC.Builtin.Names
import GHC.Hs
import GHC.Hs.Syn.Type ( hsLitType )
import GHC.Core.InstEnv
import GHC.Core.Predicate
import GHC.Core ( Expr(..), isOrphan )
import GHC.Core.Type
import GHC.Core.Multiplicity
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr ( debugPprType )
import GHC.Core.Class( Class )
import GHC.Core.DataCon
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType, unifyKind )
import GHC.Tc.Utils.Zonk
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.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 )
newMethodFromName
:: CtOrigin
-> Name
-> [TcRhoType]
-> TcM (HsExpr GhcTc)
newMethodFromName :: CtOrigin -> Name -> [Type] -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
origin Name
name [Type]
ty_args
= do { DFunId
id <- Name -> TcM DFunId
tcLookupId Name
name
; let ty :: Type
ty = (() :: Constraint) => 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))) }
topSkolemise :: SkolemInfo
-> TcSigmaType
-> TcM ( HsWrapper
, [(Name,TyVar)]
, [EvVar]
, TcRhoType )
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))
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 ((() :: Constraint) => 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, (() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty)
topInstantiate ::CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
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
; (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)
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 = (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta
inst_body :: Type
inst_body = (() :: Constraint) => 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
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 (() :: Constraint) => 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 = (() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (DFunId -> Type
tyVarKind DFunId
tv)
ty_kind :: Type
ty_kind = (() :: Constraint) => 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)
instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
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
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
= 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) }
| Just (TyCon
tc, args :: [Type]
args@[Type
_, Type
_, Type
ty1, Type
ty2]) <- (() :: Constraint) => 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]
, TcThetaType )
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, (() :: Constraint) => 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))
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 ()
instStupidTheta :: CtOrigin -> [Type] -> TcRn ()
instStupidTheta CtOrigin
orig [Type]
theta
= do { HsWrapper
_co <- CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
theta
; () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
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)
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 (PiTyVarBinder
bndr, Type
body) <- Type -> Maybe (PiTyVarBinder, Type)
tcSplitPiTy_maybe Type
kind
, PiTyVarBinder -> Bool
isInvisiblePiTyBinder PiTyVarBinder
bndr
= do { (Subst
subst', Type
arg) <- Subst -> PiTyVarBinder -> TcM (Subst, Type)
tcInstInvisibleTyBinder Subst
subst PiTyVarBinder
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 ([], (() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
kind)
tcInstInvisibleTyBinder :: Subst -> PiTyVarBinder -> TcM (Subst, TcType)
tcInstInvisibleTyBinder :: Subst -> PiTyVarBinder -> TcM (Subst, Type)
tcInstInvisibleTyBinder Subst
subst (Named (Bndr DFunId
tv ForAllTyFlag
_))
= 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') }
tcInstInvisibleTyBinder Subst
subst (Anon Scaled Type
ty FunTyFlag
af)
| Just (Coercion -> Type
mk, Type
k1, Type
k2) <- Type -> Maybe (Coercion -> Type, Type, Type)
get_eq_tys_maybe ((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
ty))
= Bool -> TcM (Subst, Type) -> TcM (Subst, Type)
forall a. HasCallStack => Bool -> a -> a
assert (FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af) (TcM (Subst, Type) -> TcM (Subst, Type))
-> TcM (Subst, Type) -> TcM (Subst, Type)
forall a b. (a -> b) -> a -> b
$
do { Coercion
co <- Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyKind Maybe TypedThing
forall a. Maybe a
Nothing Type
k1 Type
k2
; (Subst, Type) -> TcM (Subst, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, Coercion -> Type
mk Coercion
co) }
| Bool
otherwise
= String -> SDoc -> TcM (Subst, Type)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tcInvisibleTyBinder" (Scaled Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Scaled Type
ty)
get_eq_tys_maybe :: Type
-> Maybe ( Coercion -> Type
, Type
, Type
)
get_eq_tys_maybe :: Type -> Maybe (Coercion -> Type, Type, Type)
get_eq_tys_maybe Type
ty
| Just (TyCon
tc, [Type
_, Type
_, Type
k1, Type
k2]) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
= (Coercion -> Type, Type, Type)
-> Maybe (Coercion -> Type, Type, Type)
forall a. a -> Maybe a
Just (Type -> Type -> Coercion -> Type
mkHEqBoxTy Type
k1 Type
k2, Type
k1, Type
k2)
| Just (TyCon
tc, [Type
_, Type
k1, Type
k2]) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
= (Coercion -> Type, Type, Type)
-> Maybe (Coercion -> Type, Type, Type)
forall a. a -> Maybe a
Just (Type -> Type -> Coercion -> Type
mkEqBoxTy Type
k1 Type
k2, Type
k1, Type
k2)
| Bool
otherwise
= Maybe (Coercion -> Type, Type, Type)
forall a. Maybe a
Nothing
mkHEqBoxTy :: Type -> Type -> TcCoercion -> Type
mkHEqBoxTy :: Type -> Type -> Coercion -> Type
mkHEqBoxTy Type
ty1 Type
ty2 Coercion
co
= TyCon -> [Type] -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
heqDataCon) [Type
k1, Type
k2, Type
ty1, Type
ty2, Coercion -> Type
mkCoercionTy Coercion
co]
where k1 :: Type
k1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty1
k2 :: Type
k2 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty2
mkEqBoxTy :: Type -> Type -> TcCoercion -> Type
mkEqBoxTy :: Type -> Type -> Coercion -> Type
mkEqBoxTy Type
ty1 Type
ty2 Coercion
co
= TyCon -> [Type] -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
eqDataCon) [Type
k, Type
ty1, Type
ty2, Coercion -> Type
mkCoercionTy Coercion
co]
where k :: Type
k = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty1
tcInstType :: ([TyVar] -> TcM (Subst, [TcTyVar]))
-> Id
-> TcM ([(Name, TcTyVar)], TcThetaType, TcType)
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
= ([(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, (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst' [Type]
theta, (() :: Constraint) => 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)
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
= ([(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, (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst' [Type]
theta, (() :: Constraint) => 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 :: SkolemInfo -> DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
tcSkolDFunType :: SkolemInfo -> DFunId -> TcM ([DFunId], [Type], Type)
tcSkolDFunType SkolemInfo
skol_info DFunId
dfun
= do { ([(Name, DFunId)]
tv_prs, [Type]
theta, Type
tau) <- ([DFunId] -> TcM (Subst, [DFunId]))
-> DFunId -> TcM ([(Name, DFunId)], [Type], Type)
tcInstType (SkolemInfo -> [DFunId] -> TcM (Subst, [DFunId])
tcInstSuperSkolTyVars SkolemInfo
skol_info) DFunId
dfun
; ([DFunId], [Type], Type) -> TcM ([DFunId], [Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, DFunId) -> DFunId) -> [(Name, DFunId)] -> [DFunId]
forall a b. (a -> b) -> [a] -> [b]
map (Name, DFunId) -> DFunId
forall a b. (a, b) -> b
snd [(Name, DFunId)]
tv_prs, [Type]
theta, Type
tau) }
tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (Subst, [TcTyVar])
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
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
tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
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])
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])
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])
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
-> Subst -> [TyVar]
-> TcM (Subst, [TcTyVar])
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
; 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)
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)
; (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', (() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
body_ty) }
instantiateTyVarsX :: (Name -> Kind -> TcM TcTyVar)
-> Subst -> [TyVar]
-> TcM (Subst, [TcTyVar])
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])
freshenTyVarBndrs :: [DFunId] -> TcM (Subst, [DFunId])
freshenTyVarBndrs = (Name -> Type -> DFunId) -> [DFunId] -> TcM (Subst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mkTyVar
freshenCoVarBndrsX :: Subst -> [CoVar] -> TcM (Subst, [CoVar])
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])
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
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) }
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 }
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 -> TcM 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 -> TcM 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 -> TcM 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)
tcSyntaxName :: CtOrigin
-> TcType
-> (Name, HsExpr GhcRn)
-> TcM (Name, HsExpr GhcTc)
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
(() :: Constraint) => [DFunId] -> [Type] -> Type -> Type
substTyWith [DFunId
tv] [Type
ty] Type
tau
SrcSpan
span <- TcRn SrcSpan
getSrcSpanM
(TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM (Name, HsExpr GhcTc) -> TcM (Name, HsExpr GhcTc)
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (HsExpr GhcRn
-> CtOrigin -> Type -> SrcSpan -> TidyEnv -> TcM (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
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
-> TcRn (TidyEnv, SDoc)
syntaxNameCtxt :: HsExpr GhcRn
-> CtOrigin -> Type -> SrcSpan -> TidyEnv -> TcM (TidyEnv, SDoc)
syntaxNameCtxt HsExpr GhcRn
name CtOrigin
orig Type
ty SrcSpan
loc TidyEnv
tidy_env = (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) 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])]
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 ((PiTyVarBinder, Type) -> Type
forall a b. (a, b) -> b
snd ((PiTyVarBinder, Type) -> Type)
-> (Type -> (PiTyVarBinder, Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (PiTyVarBinder, Type)
splitPiTy) Type
ty
in (() :: Constraint) => 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
| Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
arrAName
= 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
= 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
= 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
= 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
= 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
= Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
4
| Bool
otherwise
= Maybe Arity
forall a. Maybe a
Nothing
getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag Maybe OverlapMode
overlap_mode
= do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let overlap_ok :: Bool
overlap_ok = Extension -> DynFlags -> Bool
xopt Extension
LangExt.OverlappingInstances DynFlags
dflags
incoherent_ok :: Bool
incoherent_ok = Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances DynFlags
dflags
use :: OverlapMode -> OverlapFlag
use OverlapMode
x = OverlapFlag { isSafeOverlap :: Bool
isSafeOverlap = DynFlags -> Bool
safeLanguageOn DynFlags
dflags
, overlapMode :: OverlapMode
overlapMode = OverlapMode
x }
default_oflag :: OverlapFlag
default_oflag | Bool
incoherent_ok = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
Incoherent SourceText
NoSourceText)
| Bool
overlap_ok = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
Overlaps SourceText
NoSourceText)
| Bool
otherwise = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
NoOverlap SourceText
NoSourceText)
final_oflag :: OverlapFlag
final_oflag = OverlapFlag -> Maybe OverlapMode -> OverlapFlag
setOverlapModeMaybe OverlapFlag
default_oflag Maybe OverlapMode
overlap_mode
; OverlapFlag -> TcM OverlapFlag
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return OverlapFlag
final_oflag }
tcGetInsts :: TcM [ClsInst]
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
; let tys' :: [Type]
tys' = (() :: Constraint) => 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
; OverlapFlag
oflag <- Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag Maybe OverlapMode
overlap_mode
; let inst :: ClsInst
inst = DFunId -> OverlapFlag -> [DFunId] -> Class -> [Type] -> ClsInst
mkLocalInstance 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
inst)) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
TcRnMessage -> TcRn ()
addDiagnostic (ClsInst -> TcRnMessage
TcRnOrphanInstance ClsInst
inst)
; ClsInst -> TcM ClsInst
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInst
inst }
tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
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
; 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])
addLocalInst :: (InstEnv, [ClsInst])
-> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
addLocalInst (InstEnv
home_ie, [ClsInst]
my_insts) ClsInst
ispec
= do {
; 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
; 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 }
; 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
; 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) }
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)
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 <- (() :: Constraint) => 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