[Git][ghc/ghc][wip/T20666] Add stuff for quantified constraints
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Jan 6 17:50:33 UTC 2023
Simon Peyton Jones pushed to branch wip/T20666 at Glasgow Haskell Compiler / GHC
Commits:
1e8add79 by Simon Peyton Jones at 2023-01-06T17:50:39+00:00
Add stuff for quantified constraints
- - - - -
12 changed files:
- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/Backpack.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcType.hs
Changes:
=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -232,10 +232,8 @@ pprInstances ispecs = vcat (map pprInstance ispecs)
instanceHead :: ClsInst -> ([TyVar], Class, [Type])
-- Returns the head, using the fresh tyvars from the ClsInst
-instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun })
+instanceHead (ClsInst { is_tvs = tvs, is_cls = cls, is_tys = tys })
= (tvs, cls, tys)
- where
- (_, _, cls, _) = tcSplitDFunTy (idType dfun)
-- | Collects the names of concrete types and type constructors that make
-- up the head of a class instance. For instance, given `class Foo a b`:
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -2691,7 +2691,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
-- superclass constraints caught by the subtleties described by
-- Note [Recursive superclasses] in GHC.TyCl.Instance
naked_sc_fixes
- | ScOrigin naked <- orig -- A superclass wanted
+ | ScOrigin _ naked <- orig -- A superclass wanted
, naked -- No instance decls used yet
, any non_tyvar_preds useful_givens -- Some non-tyvar givens
= [vcat [ text "If the constraint looks soluble from a superclass of the instance context,"
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1,6 +1,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE RecursiveDo #-}
module GHC.Tc.Solver.Canonical(
canonicalize,
@@ -600,8 +601,8 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
mk_sc_origin other_orig = pprPanic "Given constraint without given origin" $
ppr evar $$ ppr other_orig
- newly_blocked (InstSkol head_size) = isJust (this_size `ltPatersonSize` head_size)
- newly_blocked _ = False
+ newly_blocked (InstSkol _ head_size) = isJust (this_size `ltPatersonSize` head_size)
+ newly_blocked _ = False
mk_strict_superclasses rec_clss ev tvs theta cls tys
| all noFreeVarsOfType tys
@@ -862,16 +863,26 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
-- This setLclEnv is important: the emitImplicationTcS uses that
-- TcLclEnv for the implication, and that in turn sets the location
-- for the Givens when solving the constraint (#21006)
- do { skol_info <- mkSkolemInfo QuantCtxtSkol
- ; let empty_subst = mkEmptySubst $ mkInScopeSet $
+ do { let empty_subst = mkEmptySubst $ mkInScopeSet $
tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
- ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
- ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
+ -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ -- Very like the code in tcSkolDFunType
+ ; rec { skol_info <- mkSkolemInfo skol_info_anon
+ ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
+ ; let inst_pred = substTy subst pred
+ inst_theta = substTheta subst theta
+ skol_info_anon = InstSkol IsQC (get_size inst_pred) }
+
+ ; given_ev_vars <- mapM newEvVar inst_theta
; (lvl, (w_id, wanteds))
<- pushLevelNoWorkList (ppr skol_info) $
- do { wanted_ev <- newWantedEvVarNC loc rewriters $
- substTy subst pred
+ do { let loc' = setCtLocOrigin loc (ScOrigin IsQC False)
+ -- Set the thing to prove to have a ScOrigin, so we are
+ -- careful about its termination checks.
+ -- See (QC-INV) in Note [Solving a Wanted forall-constraint]
+ ; wanted_ev <- newWantedEvVarNC loc' rewriters inst_pred
; return ( ctEvEvId wanted_ev
, unitBag (mkNonCanonical wanted_ev)) }
@@ -883,6 +894,12 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
, et_binds = ev_binds, et_body = w_id }
; stopWith ev "Wanted forall-constraint" }
+ where
+ -- Getting the size of the head is a bit horrible
+ -- because of the special treament for class predicates
+ get_size pred = case classifyPredType pred of
+ ClassPred cls tys -> pSizeClassPred cls tys
+ _ -> pSizeType pred
-- See Note [Solving a Given forall-constraint]
solveForAll ev@(CtGiven {}) tvs _theta pred pend_sc
@@ -903,6 +920,23 @@ and discharge df thus:
where <binds> is filled in by solving the implication constraint.
All the machinery is to hand; there is little to do.
+The tricky point is about termination: see #19690. We want to maintain
+the invariant (QC-INV):
+
+ (QC-INV) Every quantified constraint returns a non-bottom dictionary
+
+just as every top-level instance declaration guarantees to return a non-bottom
+dictionary. But as #19690 shows, it is possible to get a bottom dicionary
+by superclass selection if we aren't careful. The situation is very similar
+to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance;
+and we use the same solution:
+
+* Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size))
+* Give the Wanted a CtOrigin of (ScOrigin IsQC False)
+
+Both of these things are done in solveForAll. Now the mechanism described
+in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over.
+
Note [Solving a Given forall-constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For a Given constraint
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -1639,7 +1639,7 @@ prohibitedSuperClassSolve :: CtLoc -- ^ is it loopy to use this one ...
-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2)
prohibitedSuperClassSolve given_loc wanted_loc
| GivenSCOrigin _ _ blocked <- ctLocOrigin given_loc
- , ScOrigin naked_sc <- ctLocOrigin wanted_loc
+ , ScOrigin _ naked_sc <- ctLocOrigin wanted_loc
= naked_sc && blocked
-- Prohibited if the Wanted is a superclass
-- and the Given has come via a superclass selection from
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -663,7 +663,10 @@ interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
-- See Note [Multiple matching irreds]
, let ev_i = ctEvidence ct_i
= do { what_next <- solveOneFromTheOther ct_i ct_w
- ; traceTcS "iteractIrred" (ppr ct_w $$ ppr what_next $$ ppr ct_i)
+ ; traceTcS "iteractIrred" $
+ vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
+ , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i))
+ , ppr what_next ]
; case what_next of
KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
@@ -2323,8 +2326,8 @@ checkInstanceOK loc what pred
-- False, so that prohibitedSuperClassSolve never fires
-- See Note [Solving superclass constraints] in
-- GHC.Tc.TyCl.Instance, (sc1).
- | ScOrigin {} <- origin
- = setCtLocOrigin loc (ScOrigin False)
+ | ScOrigin what _ <- origin
+ = setCtLocOrigin loc (ScOrigin what False)
| otherwise
= loc
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -791,7 +791,11 @@ data TcSEnv
}
---------------
-newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } deriving (Functor)
+newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
+ deriving (Functor)
+
+instance MonadFix TcS where
+ mfix k = TcS $ \env -> mfix (\x -> unTcS (k x) env)
-- | Smart constructor for 'TcS', as describe in Note [The one-shot state
-- monad trick] in "GHC.Utils.Monad".
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -490,7 +490,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
do { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty
; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty
-- NB: tcHsClsInstType does checkValidInstance
- ; skol_info <- mkSkolemInfo (mkInstSkol clas inst_tys)
+ ; skol_info <- mkSkolemInfo (mkClsInstSkol clas inst_tys)
; (subst, skol_tvs) <- tcInstSkolTyVars skol_info tyvars
; let tv_skol_prs = [ (tyVarName tv, skol_tv)
| (tv, skol_tv) <- tyvars `zip` skol_tvs ]
@@ -1232,7 +1232,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
setSrcSpan loc $
addErrCtxt (instDeclCtxt2 dfun_ty) $
do { -- Instantiate the instance decl with skolem constants
- (skol_info, inst_tyvars, dfun_theta, clas, inst_tys) <- tcSkolDFunType dfun_id
+ (skol_info, inst_tyvars, dfun_theta, clas, inst_tys) <- tcSkolDFunType dfun_ty
; dfun_ev_vars <- newEvVars dfun_theta
; let (class_tyvars, sc_theta, _, op_items) = classBigSig clas
@@ -1457,8 +1457,9 @@ tcSuperClasses skol_info dfun_id cls tyvars dfun_evs dfun_ev_binds sc_theta
loc = getSrcSpan dfun_id
tc_super (sc_pred, n)
= do { (sc_implic, ev_binds_var, sc_ev_tm)
- <- checkInstConstraints skol_info $ emitWanted (ScOrigin True) sc_pred
- -- ScOrigin True: see Note [Solving superclass constraints]
+ <- checkInstConstraints skol_info $
+ emitWanted (ScOrigin IsClsInst True) sc_pred
+ -- ScOrigin IsClsInst True: see Note [Solving superclass constraints]
; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
; sc_ev_id <- newEvVar sc_pred
@@ -2388,9 +2389,9 @@ instDeclCtxt1 hs_inst_ty
instDeclCtxt2 :: Type -> SDoc
instDeclCtxt2 dfun_ty
- = inst_decl_ctxt (ppr (mkClassPred cls tys))
+ = inst_decl_ctxt (ppr head_ty)
where
- (_,_,cls,tys) = tcSplitDFunTy dfun_ty
+ (_,_,head_ty) = tcSplitQuantPredTy dfun_ty
inst_decl_ctxt :: SDoc -> SDoc
inst_decl_ctxt doc = hang (text "In the instance declaration for")
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1700,7 +1700,6 @@ checkSkolInfoAnon sk1 sk2 = go sk1 sk2
and (zipWith eq_pr ids1 ids2)
go (UnifyForAllSkol t1) (UnifyForAllSkol t2) = t1 `tcEqType` t2
go ReifySkol ReifySkol = True
- go QuantCtxtSkol QuantCtxtSkol = True
go RuntimeUnkSkol RuntimeUnkSkol = True
go ArrowReboundIfSkol ArrowReboundIfSkol = True
go (UnkSkol _) (UnkSkol _) = True
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -13,7 +13,7 @@ module GHC.Tc.Types.Origin (
-- * SkolemInfo
SkolemInfo(..), SkolemInfoAnon(..), mkSkolemInfo, getSkolemInfo, pprSigSkolInfo, pprSkolInfo,
- unkSkol, unkSkolAnon, mkInstSkol,
+ unkSkol, unkSkolAnon, mkClsInstSkol,
-- * CtOrigin
CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin,
@@ -28,7 +28,7 @@ module GHC.Tc.Types.Origin (
-- * FixedRuntimeRep origin
FixedRuntimeRepOrigin(..), FixedRuntimeRepContext(..),
pprFixedRuntimeRepContext,
- StmtOrigin(..), RepPolyFun(..), ArgPos(..),
+ StmtOrigin(..), RepPolyFun(..), ArgPos(..), ClsInstOrQC(..),
-- * Arrow command origin
FRRArrowContext(..), pprFRRArrowContext,
@@ -250,8 +250,9 @@ data SkolemInfoAnon
| DerivSkol Type -- Bound by a 'deriving' clause;
-- the type is the instance we are trying to derive
- | InstSkol -- Bound at an instance decl
- PatersonSize -- whose head has the given PatersonSize
+ | InstSkol -- Bound at an instance decl, or quantified constraint
+ ClsInstOrQC -- Whether class instance or quantified constraint
+ PatersonSize -- Head has the given PatersonSize
| FamInstSkol -- Bound at a family instance decl
| PatSkol -- An existential type variable bound by a pattern for
@@ -283,9 +284,6 @@ data SkolemInfoAnon
| ReifySkol -- Bound during Template Haskell reification
- | QuantCtxtSkol -- Quantified context, e.g.
- -- f :: forall c. (forall a. c a => c [a]) => blah
-
| RuntimeUnkSkol -- Runtime skolem from the GHCi debugger #14628
| ArrowReboundIfSkol -- Bound by the expected type of the rebound arrow ifThenElse command.
@@ -315,8 +313,8 @@ mkSkolemInfo sk_anon = do
getSkolemInfo :: SkolemInfo -> SkolemInfoAnon
getSkolemInfo (SkolemInfo _ skol_anon) = skol_anon
-mkInstSkol :: Class -> [Type] -> SkolemInfoAnon
-mkInstSkol cls tys = InstSkol (pSizeClassPred cls tys)
+mkClsInstSkol :: Class -> [Type] -> SkolemInfoAnon
+mkClsInstSkol cls tys = InstSkol IsClsInst (pSizeClassPred cls tys)
instance Outputable SkolemInfo where
ppr (SkolemInfo _ sk_info ) = ppr sk_info
@@ -332,7 +330,10 @@ pprSkolInfo (ForAllSkol tvs) = text "an explicit forall" <+> ppr tvs
pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for"
<+> pprWithCommas ppr ips
pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred)
-pprSkolInfo (InstSkol {}) = text "the instance declaration"
+pprSkolInfo (InstSkol IsClsInst sz) = vcat [ text "the instance declaration"
+ , whenPprDebug (braces (ppr sz)) ]
+pprSkolInfo (InstSkol IsQC sz) = vcat [ text "a quantified context"
+ , whenPprDebug (braces (ppr sz)) ]
pprSkolInfo FamInstSkol = text "a family instance declaration"
pprSkolInfo BracketSkol = text "a Template Haskell bracket"
pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name
@@ -346,7 +347,6 @@ pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaratio
pprSkolInfo (DataConSkol name) = text "the type signature for" <+> quotes (ppr name)
pprSkolInfo ReifySkol = text "the type being reified"
-pprSkolInfo (QuantCtxtSkol {}) = text "a quantified context"
pprSkolInfo RuntimeUnkSkol = text "Unknown type from GHCi runtime"
pprSkolInfo ArrowReboundIfSkol = text "the expected type of a rebound if-then-else command"
@@ -524,6 +524,7 @@ data CtOrigin
-- | 'ScOrigin' is used only for the Wanted constraints for the
-- superclasses of an instance declaration.
| ScOrigin
+ ClsInstOrQC -- Whether class instance or quantified constraint
Bool -- The boolean affects only GHC.Tc.Solver.InertSet.prohibitedSuperClassSolve
-- * For the original superclass constraints we use (ScOrigin True)
-- * But after using an instance declaration we use (ScOrigin False)
@@ -596,6 +597,7 @@ data CtOrigin
| CycleBreakerOrigin
CtOrigin -- origin of the original constraint
+
-- See Detail (7) of Note [Type equality cycles] in GHC.Tc.Solver.Canonical
| FRROrigin
FixedRuntimeRepOrigin
@@ -617,6 +619,8 @@ data CtOrigin
-- like @sc_sel (sc_sel dg)@, where @dg@ is a Given.
type ScDepth = Int
+data ClsInstOrQC = IsClsInst | IsQC
+
-- An origin is visible if the place where the constraint arises is manifest
-- in user code. Currently, all origins are visible except for invisible
-- TypeEqOrigins. This is used when choosing which error of
@@ -723,8 +727,12 @@ lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS"
pprCtOrigin :: CtOrigin -> SDoc
-- "arising from ..."
-pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
-pprCtOrigin (GivenSCOrigin sk _ _) = ctoHerald <+> pprSkolInfo sk
+pprCtOrigin (GivenOrigin sk)
+ = ctoHerald <+> ppr sk
+
+pprCtOrigin (GivenSCOrigin sk d blk)
+ = vcat [ ctoHerald <+> pprSkolInfo sk
+ , whenPprDebug (braces (text "given-sc:" <+> ppr d <> comma <> ppr blk)) ]
pprCtOrigin (SpecPragOrigin ctxt)
= case ctxt of
@@ -850,8 +858,10 @@ pprCtO (HasFieldOrigin f) = hsep [text "selecting the field", quotes (ppr f)]
pprCtO AssocFamPatOrigin = text "the LHS of a family instance"
pprCtO TupleOrigin = text "a tuple"
pprCtO NegateOrigin = text "a use of syntactic negation"
-pprCtO (ScOrigin n) = text "the superclasses of an instance declaration"
- <> whenPprDebug (parens (ppr n))
+pprCtO (ScOrigin IsClsInst nkd) = vcat [ text "the superclasses of an instance declaration"
+ , whenPprDebug (braces (text "sc-origin:" <> ppr nkd)) ]
+pprCtO (ScOrigin IsQC nkd) = vcat [ text "the head of a quantified constraint"
+ , whenPprDebug (braces (text "sc-origin:" <> ppr nkd)) ]
pprCtO DerivClauseOrigin = text "the 'deriving' clause of a data type declaration"
pprCtO StandAloneDerivOrigin = text "a 'deriving' declaration"
pprCtO DefaultOrigin = text "a 'default' declaration"
=====================================
compiler/GHC/Tc/Utils/Backpack.hs
=====================================
@@ -34,6 +34,7 @@ import GHC.Types.Avail
import GHC.Types.SrcLoc
import GHC.Types.SourceFile
import GHC.Types.Var
+import GHC.Types.Id( idType )
import GHC.Types.Unique.DSet
import GHC.Types.Name.Shape
import GHC.Types.PkgQual
@@ -228,7 +229,7 @@ check_inst sig_inst@(ClsInst { is_dfun = dfun_id }) = do
-- Based off of 'simplifyDeriv'
let origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
- (skol_info, tvs_skols, inst_theta, cls, inst_tys) <- tcSkolDFunType dfun_id
+ (skol_info, tvs_skols, inst_theta, cls, inst_tys) <- tcSkolDFunType (idType dfun_id)
(tclvl,cts) <- pushTcLevelM $ do
wanted <- newWanted origin (Just TypeLevel) (mkClassPred cls inst_tys)
givens <- forM inst_theta $ \given -> do
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -446,21 +446,21 @@ tcInstTypeBndrs poly_ty
; return (subst', Bndr tv' spec) }
--------------------------
-tcSkolDFunType :: DFunId -> TcM (SkolemInfoAnon, [TcTyVar], TcThetaType, Class, [TcType])
+tcSkolDFunType :: Type -> TcM (SkolemInfoAnon, [TcTyVar], TcThetaType, Class, [TcType])
-- Instantiate a type signature with skolem constants.
-- This freshens the names, but no need to do so
-tcSkolDFunType dfun_id
- = do { let (tvs, theta, cls, tys) = tcSplitDFunTy (idType dfun_id)
+tcSkolDFunType dfun_ty
+ = do { let (tvs, theta, cls, tys) = tcSplitDFunTy dfun_ty
-- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
-- in GHC.Tc.Utils.TcType
; rec { skol_info <- mkSkolemInfo skol_info_anon
; (subst, inst_tvs) <- tcInstSuperSkolTyVars skol_info tvs
- -- We instantiate the dfun_id with superSkolems.
+ -- We instantiate the dfun_tyd with superSkolems.
-- See Note [Subtle interaction of recursion and overlap]
-- and Note [Binding when looking up instances]
; let inst_tys = substTys subst tys
- skol_info_anon = mkInstSkol cls inst_tys }
+ skol_info_anon = mkClsInstSkol cls inst_tys }
; let inst_theta = substTheta subst theta
; return (skol_info_anon, inst_tvs, inst_theta, cls, inst_tys) }
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -165,7 +165,7 @@ module GHC.Tc.Utils.TcType (
isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass,
mkClassPred,
- tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
+ tcSplitQuantPredTy, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
isRuntimeRepVar, isFixedRuntimeRepKind,
isVisiblePiTyBinder, isInvisiblePiTyBinder,
@@ -1611,20 +1611,23 @@ tcIsTyVarTy (TyVarTy _) = True
tcIsTyVarTy _ = False
-----------------------
-tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
--- Split the type of a dictionary function
--- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
--- have non-Pred arguments, such as
--- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
---
--- Also NB splitFunTys, not tcSplitFunTys;
+tcSplitQuantPredTy :: Type -> ([TyVar], [Type], PredType)
+-- Split up the type of a quantified predicate
+-- forall tys, theta => head
+-- NB splitFunTys, not tcSplitFunTys;
-- the latter specifically stops at PredTy arguments,
-- and we don't want to do that here
-tcSplitDFunTy ty
+tcSplitQuantPredTy ty
= case tcSplitForAllInvisTyVars ty of { (tvs, rho) ->
- case splitFunTys rho of { (theta, tau) ->
- case tcSplitDFunHead tau of { (clas, tys) ->
- (tvs, map scaledThing theta, clas, tys) }}}
+ case splitFunTys rho of { (theta, head) ->
+ (tvs, map scaledThing theta, head) }}
+
+tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
+-- Split the type of a dictionary function
+tcSplitDFunTy ty
+ = case tcSplitQuantPredTy ty of { (tvs, theta, head) ->
+ case tcSplitDFunHead head of { (clas, tys) ->
+ (tvs, theta, clas, tys) }}
tcSplitDFunHead :: Type -> (Class, [Type])
tcSplitDFunHead = getClassPredTys
@@ -2452,7 +2455,7 @@ pSizeType = pSizeTypeX emptyVarSet
pSizeTypes :: [Type] -> PatersonSize
pSizeTypes = pSizeTypesX emptyVarSet pSizeZero
--- Free variables of a type, retaining repetitions, and expanding synonyms
+-- Paterson size of a type, retaining repetitions, and expanding synonyms
-- This ignores coercions, as coercions aren't user-written
pSizeTypeX :: VarSet -> Type -> PatersonSize
pSizeTypeX bvs ty | Just exp_ty <- coreView ty = pSizeTypeX bvs exp_ty
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e8add793017a235f0723a60be4cc605865fb688
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e8add793017a235f0723a60be4cc605865fb688
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230106/f1c11bda/attachment-0001.html>
More information about the ghc-commits
mailing list