{-# LANGUAGE FlexibleContexts, RecursiveDo #-}
{-# LANGUAGE DisambiguateRecordFields #-}
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Utils.Instantiate (
topSkolemise, skolemiseRequired,
topInstantiate,
instantiateSigma,
instCall, instDFunType, instStupidTheta, instTyVarsWith,
newWanted, newWanteds,
tcInstType, tcInstTypeBndrs,
tcSkolemiseInvisibleBndrs,
tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarBndrsX,
tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
freshenTyVarBndrs, freshenCoVarBndrsX,
tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
newOverloadedLit, mkOverLit,
newClsInst, newFamInst,
tcGetInsts, tcGetInstEnvs, getOverlapFlag,
tcExtendLocalInstEnv,
instCallConstraints, newMethodFromName,
tcSyntaxName,
tyCoVarsOfWC,
tyCoVarsOfCt, tyCoVarsOfCts,
) where
import GHC.Prelude
import GHC.Driver.Session
import GHC.Driver.Env
import GHC.Builtin.Types ( integerTyConName )
import GHC.Builtin.Names
import GHC.Hs
import GHC.Hs.Syn.Type ( hsLitType )
import GHC.Core.InstEnv
import GHC.Core.FamInstEnv
import GHC.Core ( isOrphan )
import GHC.Core.Type
import GHC.Core.TyCo.Ppr ( debugPprType )
import GHC.Core.Class( Class )
import GHC.Core.Coercion.Axiom
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Env
import GHC.Tc.Types.Evidence
import GHC.Tc.Instance.FunDeps
import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Errors.Types
import GHC.Tc.Zonk.Monad ( ZonkM )
import GHC.Rename.Utils( mkRnSyntaxExpr )
import GHC.Types.Id.Make( mkDictFunId )
import GHC.Types.Basic ( TypeOrKind(..), Arity, VisArity )
import GHC.Types.Error
import GHC.Types.SourceText
import GHC.Types.SrcLoc as SrcLoc
import GHC.Types.Var.Env
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Types.Var
import qualified GHC.LanguageExtensions as LangExt
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Utils.Outputable
import GHC.Utils.Unique (sameUnique)
import GHC.Unit.State
import GHC.Unit.External
import GHC.Unit.Module.Warnings
import Data.List ( mapAccumL )
import qualified Data.List.NonEmpty as NE
import Control.Monad( when, unless )
import Data.Function ( on )
newMethodFromName
:: CtOrigin
-> Name
-> [TcRhoType]
-> TcM (HsExpr GhcTc)
newMethodFromName :: CtOrigin -> Name -> [Type] -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
origin Name
name [Type]
ty_args
= do { id <- Name -> TcM DFunId
tcLookupId Name
name
; let ty = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (DFunId -> Type
idType DFunId
id) [Type]
ty_args
(theta, _caller_knows_this) = tcSplitPhiTy ty
; wrap <- assert (not (isForAllTy ty) && isSingleton theta) $
instCall origin ty_args theta
; return (mkHsWrap wrap (HsVar noExtField (noLocA id))) }
topSkolemise :: SkolemInfo
-> TcSigmaType
-> TcM ( HsWrapper
, [(Name,TcInvisTVBinder)]
, [EvVar]
, TcRhoType )
topSkolemise :: SkolemInfo
-> Type
-> TcM (HsWrapper, [(Name, TcInvisTVBinder)], [DFunId], Type)
topSkolemise SkolemInfo
skolem_info Type
ty
= Subst
-> HsWrapper
-> [(Name, TcInvisTVBinder)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, TcInvisTVBinder)], [DFunId], Type)
go Subst
init_subst HsWrapper
idHsWrapper [] [] Type
ty
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty))
go :: Subst
-> HsWrapper
-> [(Name, TcInvisTVBinder)]
-> [DFunId]
-> Type
-> TcM (HsWrapper, [(Name, TcInvisTVBinder)], [DFunId], Type)
go Subst
subst HsWrapper
wrap [(Name, TcInvisTVBinder)]
tv_prs [DFunId]
ev_vars Type
ty
| ([TcInvisTVBinder]
bndrs, [Type]
theta, Type
inner_ty) <- Type -> ([TcInvisTVBinder], [Type], Type)
tcSplitSigmaTyBndrs Type
ty
, let tvs :: [DFunId]
tvs = [TcInvisTVBinder] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcInvisTVBinder]
bndrs
, Bool -> Bool
not ([DFunId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DFunId]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
= do { (subst', bndrs1) <- SkolemInfo
-> Subst -> [TcInvisTVBinder] -> TcM (Subst, [TcInvisTVBinder])
forall vis.
SkolemInfo
-> Subst
-> [VarBndr DFunId vis]
-> TcM (Subst, [VarBndr DFunId vis])
tcInstSkolTyVarBndrsX SkolemInfo
skolem_info Subst
subst [TcInvisTVBinder]
bndrs
; let tvs1 = [TcInvisTVBinder] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcInvisTVBinder]
bndrs1
; traceTc "topSkol" (vcat [ ppr tvs <+> vcat (map (ppr . getSrcSpan) tvs)
, ppr tvs1 <+> vcat (map (ppr . getSrcSpan) tvs1) ])
; ev_vars1 <- newEvVars (substTheta subst' theta)
; go subst'
(wrap <.> mkWpTyLams tvs1 <.> mkWpEvLams ev_vars1)
(tv_prs ++ (map tyVarName tvs `zip` bndrs1))
(ev_vars ++ ev_vars1)
inner_ty }
| Bool
otherwise
= (HsWrapper, [(Name, TcInvisTVBinder)], [DFunId], Type)
-> TcM (HsWrapper, [(Name, TcInvisTVBinder)], [DFunId], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap, [(Name, TcInvisTVBinder)]
tv_prs, [DFunId]
ev_vars, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty)
skolemiseRequired :: SkolemInfo -> VisArity -> TcSigmaType
-> TcM (VisArity, HsWrapper, [Name], [ForAllTyBinder], [EvVar], TcRhoType)
skolemiseRequired :: SkolemInfo
-> Arity
-> Type
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
skolemiseRequired SkolemInfo
skolem_info Arity
n_req Type
sigma
= Arity
-> Subst
-> HsWrapper
-> [Name]
-> [ForAllTyBinder]
-> [DFunId]
-> Type
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
go Arity
n_req Subst
init_subst HsWrapper
idHsWrapper [] [] [] Type
sigma
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
sigma))
go :: Arity
-> Subst
-> HsWrapper
-> [Name]
-> [ForAllTyBinder]
-> [DFunId]
-> Type
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
go Arity
n_req Subst
subst HsWrapper
wrap [Name]
acc_nms [ForAllTyBinder]
acc_bndrs [DFunId]
ev_vars Type
ty
| (Arity
n_req', [ForAllTyBinder]
bndrs, Type
inner_ty) <- Arity -> Type -> (Arity, [ForAllTyBinder], Type)
tcSplitForAllTyVarsReqTVBindersN Arity
n_req Type
ty
, Bool -> Bool
not ([ForAllTyBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ForAllTyBinder]
bndrs)
= do { (subst', bndrs1) <- SkolemInfo
-> Subst -> [ForAllTyBinder] -> TcM (Subst, [ForAllTyBinder])
forall vis.
SkolemInfo
-> Subst
-> [VarBndr DFunId vis]
-> TcM (Subst, [VarBndr DFunId vis])
tcInstSkolTyVarBndrsX SkolemInfo
skolem_info Subst
subst [ForAllTyBinder]
bndrs
; let tvs1 = [ForAllTyBinder] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [ForAllTyBinder]
bndrs1
fix_up_vis | Arity
n_req Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
n_req'
= HsWrapper
idHsWrapper
| Bool
otherwise
= [ForAllTyBinder] -> Type -> HsWrapper
mkWpForAllCast [ForAllTyBinder]
bndrs1 (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst' Type
inner_ty)
; go n_req' subst'
(wrap <.> fix_up_vis <.> mkWpTyLams tvs1)
(acc_nms ++ map (tyVarName . binderVar) bndrs)
(acc_bndrs ++ bndrs1)
ev_vars
inner_ty }
| ([Type]
theta, Type
inner_ty) <- Type -> ([Type], Type)
tcSplitPhiTy Type
ty
, Bool -> Bool
not ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
= do { ev_vars1 <- [Type] -> TcM [DFunId]
newEvVars (HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta)
; go n_req subst
(wrap <.> mkWpEvLams ev_vars1)
acc_nms
acc_bndrs
(ev_vars ++ ev_vars1)
inner_ty }
| Bool
otherwise
= (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
-> TcM (Arity, HsWrapper, [Name], [ForAllTyBinder], [DFunId], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Arity
n_req, HsWrapper
wrap, [Name]
acc_nms, [ForAllTyBinder]
acc_bndrs, [DFunId]
ev_vars, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty)
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 { (_, wrap1, body3) <- CtOrigin
-> ConcreteTyVars
-> [DFunId]
-> [Type]
-> Type
-> TcM ([DFunId], HsWrapper, Type)
instantiateSigma CtOrigin
orig ConcreteTyVars
noConcreteTyVars [DFunId]
tvs [Type]
theta Type
body2
; (wrap2, body4) <- topInstantiate orig body3
; return (wrap2 <.> wrap1, body4) }
| Bool
otherwise = (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, Type
sigma)
instantiateSigma :: CtOrigin
-> ConcreteTyVars
-> [TyVar]
-> TcThetaType -> TcSigmaType
-> TcM ([TcTyVar], HsWrapper, TcSigmaType)
instantiateSigma :: CtOrigin
-> ConcreteTyVars
-> [DFunId]
-> [Type]
-> Type
-> TcM ([DFunId], HsWrapper, Type)
instantiateSigma CtOrigin
orig ConcreteTyVars
concs [DFunId]
tvs [Type]
theta Type
body_ty
= do { rec (subst, inst_tvs) <- mapAccumLM (new_meta subst) empty_subst tvs
; let inst_theta = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta
inst_body = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
body_ty
inst_tv_tys = [DFunId] -> [Type]
mkTyVarTys [DFunId]
inst_tvs
; wrap <- instCall orig inst_tv_tys inst_theta
; traceTc "Instantiating"
(vcat [ text "origin" <+> pprCtOrigin orig
, text "tvs" <+> ppr tvs
, text "theta" <+> ppr theta
, text "type" <+> debugPprType body_ty
, text "with" <+> vcat (map debugPprType inst_tv_tys)
, text "theta:" <+> ppr inst_theta ])
; return (inst_tvs, wrap, inst_body) }
where
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType ([DFunId] -> [Type] -> Type -> Type
HasDebugCallStack => [DFunId] -> [Type] -> Type -> Type
mkSpecSigmaTy [DFunId]
tvs [Type]
theta Type
body_ty))
empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope
new_meta :: Subst -> Subst -> TyVar -> TcM (Subst, TcTyVar)
new_meta :: Subst
-> Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
new_meta Subst
final_subst Subst
subst DFunId
tv
| Just ConcreteTvOrigin
conc_orig0 <- ConcreteTyVars -> Name -> Maybe ConcreteTvOrigin
forall a. NameEnv a -> Name -> Maybe a
lookupNameEnv ConcreteTyVars
concs (DFunId -> Name
tyVarName DFunId
tv)
, let conc_orig :: ConcreteTvOrigin
conc_orig = Subst -> Type -> ConcreteTvOrigin -> ConcreteTvOrigin
substConcreteTvOrigin Subst
final_subst Type
body_ty ConcreteTvOrigin
conc_orig0
= ConcreteTvOrigin
-> Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newConcreteTyVarX ConcreteTvOrigin
conc_orig Subst
subst DFunId
tv
| Bool
otherwise
= Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv
instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM Subst
instTyVarsWith :: CtOrigin -> [DFunId] -> [Type] -> TcM Subst
instTyVarsWith CtOrigin
orig [DFunId]
tvs [Type]
tys
= Subst -> [DFunId] -> [Type] -> TcM Subst
go Subst
emptySubst [DFunId]
tvs [Type]
tys
where
go :: Subst -> [DFunId] -> [Type] -> TcM Subst
go Subst
subst [] []
= Subst -> TcM Subst
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
subst
go Subst
subst (DFunId
tv:[DFunId]
tvs) (Type
ty:[Type]
tys)
| Type
tv_kind HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty_kind
= Subst -> [DFunId] -> [Type] -> TcM Subst
go (Subst -> DFunId -> Type -> Subst
extendTvSubstAndInScope Subst
subst DFunId
tv Type
ty) [DFunId]
tvs [Type]
tys
| Bool
otherwise
= do { co <- CtOrigin -> TypeOrKind -> Role -> Type -> Type -> TcM Coercion
emitWantedEq CtOrigin
orig TypeOrKind
KindLevel Role
Nominal Type
ty_kind Type
tv_kind
; go (extendTvSubstAndInScope subst tv (ty `mkCastTy` co)) tvs tys }
where
tv_kind :: Type
tv_kind = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (DFunId -> Type
tyVarKind DFunId
tv)
ty_kind :: Type
ty_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty
go Subst
_ [DFunId]
_ [Type]
_ = String -> SDoc -> TcM Subst
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"instTysWith" ([DFunId] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunId]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
instCall :: CtOrigin -> [Type] -> [Type] -> TcM HsWrapper
instCall CtOrigin
orig [Type]
tys [Type]
theta
= do { dict_app <- CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
theta
; return (dict_app <.> mkWpTyApps tys) }
instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
instCallConstraints :: CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
preds
| [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
preds
= HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return HsWrapper
idHsWrapper
| Bool
otherwise
= do { evs <- (Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm)
-> [Type] -> IOEnv (Env TcGblEnv TcLclEnv) [EvTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtOrigin -> Type -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
emitWanted CtOrigin
orig) [Type]
preds
; traceTc "instCallConstraints" (ppr evs)
; return (mkWpEvApps evs) }
instDFunType :: DFunId -> [DFunInstType]
-> TcM ( [TcType]
, TcThetaType )
instDFunType :: DFunId -> [DFunInstType] -> TcM ([Type], [Type])
instDFunType DFunId
dfun_id [DFunInstType]
dfun_inst_tys
= do { (subst, inst_tys) <- Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go Subst
empty_subst [DFunId]
dfun_tvs [DFunInstType]
dfun_inst_tys
; return (inst_tys, substTheta subst dfun_theta) }
where
dfun_ty :: Type
dfun_ty = DFunId -> Type
idType DFunId
dfun_id
([DFunId]
dfun_tvs, [Type]
dfun_theta, Type
_) = Type -> ([DFunId], [Type], Type)
tcSplitSigmaTy Type
dfun_ty
empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
dfun_ty))
go :: Subst -> [TyVar] -> [DFunInstType] -> TcM (Subst, [TcType])
go :: Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go Subst
subst [] [] = (Subst, [Type]) -> TcM (Subst, [Type])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, [])
go Subst
subst (DFunId
tv:[DFunId]
tvs) (Just Type
ty : [DFunInstType]
mb_tys)
= do { (subst', tys) <- Subst -> [DFunId] -> [DFunInstType] -> TcM (Subst, [Type])
go (Subst -> DFunId -> Type -> Subst
extendTvSubstAndInScope Subst
subst DFunId
tv Type
ty)
[DFunId]
tvs
[DFunInstType]
mb_tys
; return (subst', ty : tys) }
go Subst
subst (DFunId
tv:[DFunId]
tvs) (DFunInstType
Nothing : [DFunInstType]
mb_tys)
= do { (subst', tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv
; (subst'', tys) <- go subst' tvs mb_tys
; return (subst'', mkTyVarTy tv' : tys) }
go Subst
_ [DFunId]
_ [DFunInstType]
_ = String -> SDoc -> TcM (Subst, [Type])
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"instDFunTypes" (DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr DFunId
dfun_id SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [DFunInstType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunInstType]
dfun_inst_tys)
instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
instStupidTheta :: CtOrigin -> [Type] -> TcRn ()
instStupidTheta CtOrigin
orig [Type]
theta
= do { _co <- CtOrigin -> [Type] -> TcM HsWrapper
instCallConstraints CtOrigin
orig [Type]
theta
; return () }
tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
tcInstInvisibleTyBinders :: Type -> Type -> TcM (Type, Type)
tcInstInvisibleTyBinders Type
ty Type
kind
= do { (extra_args, kind') <- Arity -> Type -> TcM ([Type], Type)
tcInstInvisibleTyBindersN Arity
n_invis Type
kind
; return (mkAppTys ty extra_args, kind') }
where
n_invis :: Arity
n_invis = Type -> Arity
invisibleBndrCount Type
kind
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 (ForAllTyBinder
bndr, Type
body) <- Type -> Maybe (ForAllTyBinder, Type)
tcSplitForAllTyVarBinder_maybe Type
kind
, ForAllTyFlag -> Bool
isInvisibleForAllTyFlag (ForAllTyBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag ForAllTyBinder
bndr)
= do { (subst', arg) <- Subst -> DFunId -> TcM (Subst, Type)
tcInstInvisibleTyBinder Subst
subst (ForAllTyBinder -> DFunId
forall tv argf. VarBndr tv argf -> tv
binderVar ForAllTyBinder
bndr)
; (args, inner_ty) <- go (n-1) subst' body
; return (arg:args, inner_ty) }
| Bool
otherwise
= ([Type], Type) -> TcM ([Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
kind)
tcInstInvisibleTyBinder :: Subst -> TyVar -> TcM (Subst, TcType)
tcInstInvisibleTyBinder :: Subst -> DFunId -> TcM (Subst, Type)
tcInstInvisibleTyBinder Subst
subst DFunId
tv
= do { (subst', tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarX Subst
subst DFunId
tv
; return (subst', mkTyVarTy tv') }
tcInstType :: ([TyVar] -> TcM (Subst, [TcTyVar]))
-> Id
-> TcM ([(Name, TcTyVar)], TcThetaType, TcType)
tcInstType :: ([DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId]))
-> DFunId -> TcM ([(Name, DFunId)], [Type], Type)
tcInstType [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
inst_tyvars DFunId
id
| [DFunId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DFunId]
tyvars
= ([(Name, DFunId)], [Type], Type)
-> TcM ([(Name, DFunId)], [Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Type]
theta, Type
tau)
| Bool
otherwise
= do { (subst, tyvars') <- [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
inst_tyvars [DFunId]
tyvars
; let tv_prs = (DFunId -> Name) -> [DFunId] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DFunId -> Name
tyVarName [DFunId]
tyvars [Name] -> [DFunId] -> [(Name, DFunId)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [DFunId]
tyvars'
subst' = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Type -> VarSet
tyCoVarsOfType Type
rho)
; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
where
([DFunId]
tyvars, Type
rho) = Type -> ([DFunId], Type)
tcSplitForAllInvisTyVars (DFunId -> Type
idType DFunId
id)
([Type]
theta, Type
tau) = Type -> ([Type], Type)
tcSplitPhiTy Type
rho
tcInstTypeBndrs :: Type -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
tcInstTypeBndrs :: Type -> TcM ([(Name, TcInvisTVBinder)], [Type], Type)
tcInstTypeBndrs Type
poly_ty
| [TcInvisTVBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcInvisTVBinder]
tyvars
= ([(Name, TcInvisTVBinder)], [Type], Type)
-> TcM ([(Name, TcInvisTVBinder)], [Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Type]
theta, Type
tau)
| Bool
otherwise
= do { (subst, tyvars') <- (Subst
-> TcInvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, TcInvisTVBinder))
-> Subst -> [TcInvisTVBinder] -> TcM (Subst, [TcInvisTVBinder])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM Subst
-> TcInvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, TcInvisTVBinder)
inst_invis_bndr Subst
emptySubst [TcInvisTVBinder]
tyvars
; let tv_prs = (TcInvisTVBinder -> Name) -> [TcInvisTVBinder] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (DFunId -> Name
tyVarName (DFunId -> Name)
-> (TcInvisTVBinder -> DFunId) -> TcInvisTVBinder -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcInvisTVBinder -> DFunId
forall tv argf. VarBndr tv argf -> tv
binderVar) [TcInvisTVBinder]
tyvars [Name] -> [TcInvisTVBinder] -> [(Name, TcInvisTVBinder)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [TcInvisTVBinder]
tyvars'
subst' = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Type -> VarSet
tyCoVarsOfType Type
rho)
; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
where
([TcInvisTVBinder]
tyvars, Type
rho) = Type -> ([TcInvisTVBinder], Type)
tcSplitForAllInvisTVBinders Type
poly_ty
([Type]
theta, Type
tau) = Type -> ([Type], Type)
tcSplitPhiTy Type
rho
inst_invis_bndr :: Subst -> InvisTVBinder
-> TcM (Subst, InvisTVBinder)
inst_invis_bndr :: Subst
-> TcInvisTVBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, TcInvisTVBinder)
inst_invis_bndr Subst
subst (Bndr DFunId
tv Specificity
spec)
= do { (subst', tv') <- Subst -> DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, DFunId)
newMetaTyVarTyVarX Subst
subst DFunId
tv
; return (subst', Bndr tv' spec) }
tcSkolDFunType :: Type -> TcM (SkolemInfoAnon, [TcTyVar], TcThetaType, Class, [TcType])
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 { skol_info <- mkSkolemInfo skol_info_anon
; (subst, inst_tvs) <- tcInstSuperSkolTyVars skol_info tvs
; let inst_tys = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys
skol_info_anon = Class -> [Type] -> SkolemInfoAnon
mkClsInstSkol Class
cls [Type]
inst_tys }
; let inst_theta = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst [Type]
theta
; return (skol_info_anon, inst_tvs, inst_theta, cls, inst_tys) }
tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (Subst, [TcTyVar])
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] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVars SkolemInfo
skol_info = SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
emptySubst
tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
tcInstSkolTyVarsX :: SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skol_info = SkolemInfo
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsPushLevel SkolemInfo
skol_info Bool
False
tcInstSkolTyVarBndrsX :: SkolemInfo -> Subst -> [VarBndr TyCoVar vis] -> TcM (Subst, [VarBndr TyCoVar vis])
tcInstSkolTyVarBndrsX :: forall vis.
SkolemInfo
-> Subst
-> [VarBndr DFunId vis]
-> TcM (Subst, [VarBndr DFunId vis])
tcInstSkolTyVarBndrsX SkolemInfo
skol_info Subst
subs [VarBndr DFunId vis]
bndrs = do
(subst', bndrs') <- SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
subs ([VarBndr DFunId vis] -> [DFunId]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr DFunId vis]
bndrs)
pure (subst', zipWith mkForAllTyBinder flags bndrs')
where
flags :: [vis]
flags = [VarBndr DFunId vis] -> [vis]
forall tv argf. [VarBndr tv argf] -> [argf]
binderFlags [VarBndr DFunId vis]
bndrs
tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
tcInstSuperSkolTyVars :: SkolemInfo
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSuperSkolTyVars SkolemInfo
skol_info = SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSuperSkolTyVarsX SkolemInfo
skol_info Subst
emptySubst
tcInstSuperSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
tcInstSuperSkolTyVarsX :: SkolemInfo
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSuperSkolTyVarsX SkolemInfo
skol_info Subst
subst = SkolemInfo
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsPushLevel SkolemInfo
skol_info Bool
True Subst
subst
tcInstSkolTyVarsPushLevel :: SkolemInfo -> Bool
-> Subst -> [TyVar]
-> TcM (Subst, [TcTyVar])
tcInstSkolTyVarsPushLevel :: SkolemInfo
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsPushLevel SkolemInfo
skol_info Bool
overlappable Subst
subst [DFunId]
tvs
= do { tc_lvl <- TcM TcLevel
getTcLevel
; let !pushed_lvl = TcLevel -> TcLevel
pushTcLevel TcLevel
tc_lvl
; tcInstSkolTyVarsAt skol_info pushed_lvl overlappable subst tvs }
tcInstSkolTyVarsAt :: SkolemInfo -> TcLevel -> Bool
-> Subst -> [TyVar]
-> TcM (Subst, [TcTyVar])
tcInstSkolTyVarsAt :: SkolemInfo
-> TcLevel
-> Bool
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
tcInstSkolTyVarsAt SkolemInfo
skol_info TcLevel
lvl Bool
overlappable Subst
subst [DFunId]
tvs
= (Name -> Type -> DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
new_skol_tv Subst
subst [DFunId]
tvs
where
sk_details :: TcTyVarDetails
sk_details = SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info TcLevel
lvl Bool
overlappable
new_skol_tv :: Name -> Type -> DFunId
new_skol_tv Name
name Type
kind = Name -> Type -> TcTyVarDetails -> DFunId
mkTcTyVar Name
name Type
kind TcTyVarDetails
sk_details
tcSkolemiseInvisibleBndrs :: SkolemInfoAnon -> Type -> TcM ([TcTyVar], TcType)
tcSkolemiseInvisibleBndrs :: SkolemInfoAnon -> Type -> TcM ([DFunId], Type)
tcSkolemiseInvisibleBndrs SkolemInfoAnon
skol_info Type
ty
= do { let ([DFunId]
tvs, Type
body_ty) = Type -> ([DFunId], Type)
tcSplitForAllInvisTyVars Type
ty
; lvl <- TcM TcLevel
getTcLevel
; skol_info <- mkSkolemInfo skol_info
; let details = SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info TcLevel
lvl Bool
False
mk_skol_tv Name
name Type
kind = DFunId -> TcM DFunId
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> TcTyVarDetails -> DFunId
mkTcTyVar Name
name Type
kind TcTyVarDetails
details)
; (subst, tvs') <- instantiateTyVarsX mk_skol_tv emptySubst tvs
; return (tvs', substTy subst body_ty) }
instantiateTyVarsX :: (Name -> Kind -> TcM TcTyVar)
-> Subst -> [TyVar]
-> TcM (Subst, [TcTyVar])
instantiateTyVarsX :: (Name -> Type -> TcM DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
instantiateTyVarsX Name -> Type -> TcM DFunId
mk_tv Subst
subst [DFunId]
tvs
= case [DFunId]
tvs of
[] -> (Subst, [DFunId])
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, [])
(DFunId
tv:[DFunId]
tvs) -> do { let kind1 :: Type
kind1 = Subst -> Type -> Type
substTyUnchecked Subst
subst (DFunId -> Type
tyVarKind DFunId
tv)
; tv' <- Name -> Type -> TcM DFunId
mk_tv (DFunId -> Name
tyVarName DFunId
tv) Type
kind1
; let subst1 = Subst -> DFunId -> DFunId -> Subst
extendTCvSubstWithClone Subst
subst DFunId
tv DFunId
tv'
; (subst', tvs') <- instantiateTyVarsX mk_tv subst1 tvs
; return (subst', tv':tvs') }
freshenTyVarBndrs :: [TyVar] -> TcM (Subst, [TyVar])
freshenTyVarBndrs :: [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyVarBndrs = (Name -> Type -> DFunId)
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mkTyVar
freshenCoVarBndrsX :: Subst -> [CoVar] -> TcM (Subst, [CoVar])
freshenCoVarBndrsX :: Subst
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenCoVarBndrsX Subst
subst = (Name -> Type -> DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mkCoVar Subst
subst
freshenTyCoVars :: (Name -> Kind -> TyCoVar)
-> [TyVar] -> TcM (Subst, [TyCoVar])
freshenTyCoVars :: (Name -> Type -> DFunId)
-> [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVars Name -> Type -> DFunId
mk_tcv = (Name -> Type -> DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mk_tcv Subst
emptySubst
freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
-> Subst -> [TyCoVar]
-> TcM (Subst, [TyCoVar])
freshenTyCoVarsX :: (Name -> Type -> DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyCoVarsX Name -> Type -> DFunId
mk_tcv
= (Name -> Type -> TcM DFunId)
-> Subst
-> [DFunId]
-> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
instantiateTyVarsX Name -> Type -> TcM DFunId
freshen_tcv
where
freshen_tcv :: Name -> Kind -> TcM TcTyVar
freshen_tcv :: Name -> Type -> TcM DFunId
freshen_tcv Name
name Type
kind
= do { loc <- TcRn SrcSpan
getSrcSpanM
; uniq <- newUnique
; let !occ_name = Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName Name
name
new_name = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
uniq OccName
occ_name SrcSpan
loc
; return (mk_tcv new_name kind) }
newOverloadedLit :: HsOverLit GhcRn
-> ExpRhoType
-> TcM (HsOverLit GhcTc)
newOverloadedLit :: HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newOverloadedLit HsOverLit GhcRn
lit ExpRhoType
res_ty
= do { mb_lit' <- HsOverLit GhcRn -> ExpRhoType -> TcM (Maybe (HsOverLit GhcTc))
tcShortCutLit HsOverLit GhcRn
lit ExpRhoType
res_ty
; case mb_lit' of
Just HsOverLit GhcTc
lit' -> HsOverLit GhcTc -> TcM (HsOverLit GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return HsOverLit GhcTc
lit'
Maybe (HsOverLit GhcTc)
Nothing -> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit HsOverLit GhcRn
lit ExpRhoType
res_ty }
newNonTrivialOverloadedLit :: HsOverLit GhcRn
-> ExpRhoType
-> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit :: HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTc)
newNonTrivialOverloadedLit
lit :: HsOverLit GhcRn
lit@(OverLit { ol_val :: forall p. HsOverLit p -> OverLitVal
ol_val = OverLitVal
val, ol_ext :: forall p. HsOverLit p -> XOverLit p
ol_ext = OverLitRn Bool
rebindable (L SrcSpanAnnN
loc Name
meth_name) })
ExpRhoType
res_ty
= do { hs_lit <- OverLitVal -> TcM (HsLit GhcTc)
mkOverLit OverLitVal
val
; let lit_ty = HsLit GhcTc -> Type
forall (p :: Pass). IsPass p => HsLit (GhcPass p) -> Type
hsLitType HsLit GhcTc
hs_lit
; (_, fi') <- tcSyntaxOp orig (mkRnSyntaxExpr meth_name)
[synKnownType lit_ty] res_ty $
\[Type]
_ [Type]
_ -> () -> TcRn ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
; let L _ witness = mkHsSyntaxApps (l2l loc) fi' [nlHsLit hs_lit]
; res_ty <- readExpType res_ty
; return (lit { ol_ext = OverLitTc { ol_rebindable = rebindable
, ol_witness = witness
, ol_type = res_ty } }) }
where
orig :: CtOrigin
orig = HsOverLit GhcRn -> CtOrigin
LiteralOrigin HsOverLit GhcRn
lit
mkOverLit :: OverLitVal -> TcM (HsLit GhcTc)
mkOverLit :: OverLitVal -> TcM (HsLit GhcTc)
mkOverLit (HsIntegral IntegralLit
i)
= do { integer_ty <- Name -> IOEnv (Env TcGblEnv TcLclEnv) Type
tcMetaTy Name
integerTyConName
; return (XLit $ HsInteger (il_text i) (il_value i) integer_ty) }
mkOverLit (HsFractional FractionalLit
r)
= do { rat_ty <- Name -> IOEnv (Env TcGblEnv TcLclEnv) Type
tcMetaTy Name
rationalTyConName
; return (XLit $ HsRat r rat_ty) }
mkOverLit (HsIsString SourceText
src FastString
s) = HsLit GhcTc -> TcM (HsLit GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsString GhcTc -> FastString -> HsLit GhcTc
forall x. XHsString x -> FastString -> HsLit x
HsString XHsString GhcTc
SourceText
src FastString
s)
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 rhs <- CtOrigin -> Name -> [Type] -> TcM (HsExpr GhcTc)
newMethodFromName CtOrigin
orig Name
std_nm [Type
ty]
return (std_nm, rhs)
tcSyntaxName CtOrigin
orig Type
ty (Name
std_nm, HsExpr GhcRn
user_nm_expr) = do
std_id <- Name -> TcM DFunId
tcLookupId Name
std_nm
let
([tv], _, tau) = tcSplitSigmaTy (idType std_id)
sigma1 = [DFunId] -> [Type] -> Type -> Type
HasDebugCallStack => [DFunId] -> [Type] -> Type -> Type
substTyWith [DFunId
tv] [Type
ty] Type
tau
span <- getSrcSpanM
addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1 span) $ do
expr <- tcCheckPolyExpr (L (noAnnSrcSpan span) user_nm_expr) sigma1
hasFixedRuntimeRepRes std_nm user_nm_expr sigma1
return (std_nm, unLoc expr)
syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> SrcSpan -> TidyEnv
-> ZonkM (TidyEnv, SDoc)
syntaxNameCtxt :: HsExpr GhcRn
-> CtOrigin -> Type -> SrcSpan -> TidyEnv -> ZonkM (TidyEnv, SDoc)
syntaxNameCtxt HsExpr GhcRn
name CtOrigin
orig Type
ty SrcSpan
loc TidyEnv
tidy_env = (TidyEnv, SDoc) -> ZonkM (TidyEnv, SDoc)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
msg)
where
msg :: SDoc
msg = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"When checking that" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
name)
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(needed by a syntactic construct)"
, Arity -> SDoc -> SDoc
nest Arity
2 (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"has the required type:"
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env Type
ty))
, Arity -> SDoc -> SDoc
nest Arity
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtOrigin
orig, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"at" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
loc])]
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
| Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
arrAName
= Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
3
| Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
composeAName
= Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
5
| Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
firstAName
= Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
4
| Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
appAName
= Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
2
| Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
choiceAName
= Arity -> Maybe Arity
forall a. a -> Maybe a
Just Arity
5
| Name -> Name -> Bool
forall a. Uniquable a => a -> a -> Bool
sameUnique Name
std_nm Name
loopAName
= 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_prag
= do { dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let overlap_ok = Extension -> DynFlags -> Bool
xopt Extension
LangExt.OverlappingInstances DynFlags
dflags
incoherent_ok = Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances DynFlags
dflags
noncanonical_incoherence = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_SpecialiseIncoherents DynFlags
dflags
overlap_mode
| Just OverlapMode
m <- Maybe OverlapMode
overlap_mode_prag = OverlapMode
m
| Bool
incoherent_ok = SourceText -> OverlapMode
Incoherent SourceText
NoSourceText
| Bool
overlap_ok = SourceText -> OverlapMode
Overlaps SourceText
NoSourceText
| Bool
otherwise = SourceText -> OverlapMode
NoOverlap SourceText
NoSourceText
final_overlap_mode
| Incoherent SourceText
s <- OverlapMode
overlap_mode
, Bool
noncanonical_incoherence = SourceText -> OverlapMode
NonCanonical SourceText
s
| Bool
otherwise = OverlapMode
overlap_mode
; return (OverlapFlag { isSafeOverlap = safeLanguageOn dflags
, overlapMode = final_overlap_mode }) }
tcGetInsts :: TcM [ClsInst]
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] -> Maybe (WarningTxt GhcRn) -> TcM ClsInst
newClsInst :: Maybe OverlapMode
-> Name
-> [DFunId]
-> [Type]
-> Class
-> [Type]
-> Maybe (WarningTxt GhcRn)
-> TcM ClsInst
newClsInst Maybe OverlapMode
overlap_mode Name
dfun_name [DFunId]
tvs [Type]
theta Class
clas [Type]
tys Maybe (WarningTxt GhcRn)
warn
= do { (subst, tvs') <- [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyVarBndrs [DFunId]
tvs
; let tys' = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys
dfun = Name -> [DFunId] -> [Type] -> Class -> [Type] -> DFunId
mkDictFunId Name
dfun_name [DFunId]
tvs [Type]
theta Class
clas [Type]
tys
; oflag <- getOverlapFlag overlap_mode
; let cls_inst = DFunId
-> OverlapFlag
-> [DFunId]
-> Class
-> [Type]
-> Maybe (WarningTxt GhcRn)
-> ClsInst
mkLocalClsInst DFunId
dfun OverlapFlag
oflag [DFunId]
tvs' Class
clas [Type]
tys' Maybe (WarningTxt GhcRn)
warn
; when (isOrphan (is_orphan cls_inst)) $
addDiagnostic (TcRnOrphanInstance $ Left cls_inst)
; return cls_inst }
tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
tcExtendLocalInstEnv :: forall a. [ClsInst] -> TcM a -> TcM a
tcExtendLocalInstEnv [ClsInst]
dfuns TcM a
thing_inside
= do { [ClsInst] -> TcRn ()
traceDFuns [ClsInst]
dfuns
; env <- IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
; let !init_inst_env = TcGblEnv -> InstEnv
tcg_inst_env TcGblEnv
env
!init_insts = TcGblEnv -> [ClsInst]
tcg_insts TcGblEnv
env
; (inst_env', cls_insts') <- foldlM addLocalInst
(init_inst_env, init_insts)
dfuns
; let env' = TcGblEnv
env { tcg_insts = cls_insts'
, tcg_inst_env = inst_env' }
; setGblEnv env' thing_inside }
addLocalInst :: (InstEnv, [ClsInst]) -> ClsInst -> TcM (InstEnv, [ClsInst])
addLocalInst :: (InstEnv, [ClsInst])
-> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
addLocalInst (InstEnv
home_ie, [ClsInst]
my_insts) ClsInst
ispec
= do {
; isGHCi <- TcRn Bool
getIsGHCi
; eps <- getEps
; tcg_env <- getGblEnv
; let home_ie'
| Bool
isGHCi = InstEnv -> ClsInst -> InstEnv
deleteFromInstEnv InstEnv
home_ie ClsInst
ispec
| Bool
otherwise = InstEnv
home_ie
global_ie = ExternalPackageState -> InstEnv
eps_inst_env ExternalPackageState
eps
inst_envs = InstEnvs { ie_global :: InstEnv
ie_global = InstEnv
global_ie
, ie_local :: InstEnv
ie_local = InstEnv
home_ie'
, ie_visible :: VisibleOrphanModules
ie_visible = TcGblEnv -> VisibleOrphanModules
tcVisibleOrphanMods TcGblEnv
tcg_env }
; let inconsistent_ispecs = InstEnvs -> ClsInst -> [ClsInst]
checkFunDeps InstEnvs
inst_envs ClsInst
ispec
; unless (null inconsistent_ispecs) $
funDepErr ispec inconsistent_ispecs
; let (_tvs, cls, tys) = instanceHead ispec
(matches, _, _) = lookupInstEnv False inst_envs cls tys
dups = (ClsInst -> Bool) -> [ClsInst] -> [ClsInst]
forall a. (a -> Bool) -> [a] -> [a]
filter (ClsInst -> ClsInst -> Bool
identicalClsInstHead ClsInst
ispec) ((InstMatch -> ClsInst) -> [InstMatch] -> [ClsInst]
forall a b. (a -> b) -> [a] -> [b]
map InstMatch -> ClsInst
forall a b. (a, b) -> a
fst [InstMatch]
matches)
; unless (null dups) $
dupInstErr ispec (head dups)
; return (extendInstEnv home_ie' ispec, ispec : my_insts) }
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
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 {
(subst, tvs') <- [DFunId] -> IOEnv (Env TcGblEnv TcLclEnv) (Subst, [DFunId])
freshenTyVarBndrs [DFunId]
tvs
; (subst, cvs') <- freshenCoVarBndrsX subst cvs
; let lhs' = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
lhs
rhs' = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
rhs
; let fam_inst = FamFlavor
-> CoAxiom Unbranched
-> [DFunId]
-> [DFunId]
-> [Type]
-> Type
-> FamInst
mkLocalFamInst FamFlavor
flavor CoAxiom Unbranched
axiom [DFunId]
tvs' [DFunId]
cvs' [Type]
lhs' Type
rhs'
; when (isOrphan (fi_orphan fam_inst)) $
addDiagnostic (TcRnOrphanInstance $ Right fam_inst)
; return fam_inst }
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
unit_state <- HasDebugCallStack => HscEnv -> UnitState
HscEnv -> UnitState
hsc_units (HscEnv -> UnitState)
-> IOEnv (Env TcGblEnv TcLclEnv) HscEnv
-> IOEnv (Env TcGblEnv TcLclEnv) UnitState
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
getTopEnv
setSrcSpan (getSrcSpan (NE.head sorted)) $
addErr $ mkErr unit_state sorted
where
sorted :: NonEmpty ClsInst
sorted = (ClsInst -> ClsInst -> Ordering)
-> NonEmpty ClsInst -> NonEmpty ClsInst
forall a. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
NE.sortBy (SrcSpan -> SrcSpan -> Ordering
SrcLoc.leftmost_smallest (SrcSpan -> SrcSpan -> Ordering)
-> (ClsInst -> SrcSpan) -> ClsInst -> ClsInst -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ClsInst -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan) NonEmpty ClsInst
ispecs