[Git][ghc/ghc][wip/cfuneqcan-refactor] 7 commits: test LocalGivenEqs
Richard Eisenberg
gitlab at gitlab.haskell.org
Sat Nov 7 18:29:15 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
fb9c27ac by Richard Eisenberg at 2020-11-05T15:34:20-05:00
test LocalGivenEqs
- - - - -
29a8f7a2 by Richard Eisenberg at 2020-11-05T17:30:38-05:00
Update commentary about HasGivenEqs
- - - - -
3557866f by Richard Eisenberg at 2020-11-05T18:24:12-05:00
Update notes.
- - - - -
a98b07cb by Richard Eisenberg at 2020-11-07T11:30:54-05:00
More documentation around LocalGivenEqs
- - - - -
dc6d9ef0 by Richard Eisenberg at 2020-11-07T12:33:25-05:00
Rename the flat-cache. Document it, too.
- - - - -
058f4acb by Richard Eisenberg at 2020-11-07T13:16:23-05:00
Make EqualCtList into a newtype with NonEmpty
- - - - -
e2ec2ada by Richard Eisenberg at 2020-11-07T13:28:52-05:00
Remove Note [No FunEq improvement for Givens]
- - - - -
15 changed files:
- compiler/GHC/Data/Bag.hs
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- docs/users_guide/expected-undocumented-flags.txt
- docs/users_guide/exts/type_families.rst
- testsuite/tests/indexed-types/should_fail/T13784.stderr
- testsuite/tests/patsyn/should_fail/T11010.stderr
- + testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
- + testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Data/Bag.hs
=====================================
@@ -17,7 +17,7 @@ module GHC.Data.Bag (
filterBag, partitionBag, partitionBagWith,
concatBag, catBagMaybes, foldBag,
isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag,
- listToBag, bagToList, mapAccumBagL,
+ listToBag, nonEmptyToBag, bagToList, mapAccumBagL,
concatMapBag, concatMapBagPair, mapMaybeBag,
mapBagM, mapBagM_,
flatMapBagM, flatMapBagPairM,
@@ -35,6 +35,7 @@ import Control.Monad
import Data.Data
import Data.Maybe( mapMaybe )
import Data.List ( partition, mapAccumL )
+import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.Foldable as Foldable
infixr 3 `consBag`
@@ -299,6 +300,10 @@ listToBag [] = EmptyBag
listToBag [x] = UnitBag x
listToBag vs = ListBag vs
+nonEmptyToBag :: NonEmpty a -> Bag a
+nonEmptyToBag (x :| []) = UnitBag x
+nonEmptyToBag (x :| xs) = ListBag (x : xs)
+
bagToList :: Bag a -> [a]
bagToList b = foldr (:) [] b
=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -260,7 +260,7 @@ data GeneralFlag
| Opt_RPath
| Opt_RelativeDynlibPaths
| Opt_Hpc
- | Opt_FlatCache
+ | Opt_FamAppCache
| Opt_ExternalInterpreter
| Opt_OptimalApplicativeDo
| Opt_VersionMacros
=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -3404,7 +3404,7 @@ fFlagsDeps = [
flagSpec "expose-all-unfoldings" Opt_ExposeAllUnfoldings,
flagSpec "external-dynamic-refs" Opt_ExternalDynamicRefs,
flagSpec "external-interpreter" Opt_ExternalInterpreter,
- flagSpec "flat-cache" Opt_FlatCache,
+ flagSpec "family-application-cache" Opt_FamAppCache,
flagSpec "float-in" Opt_FloatIn,
flagSpec "force-recomp" Opt_ForceRecomp,
flagSpec "ignore-optim-changes" Opt_IgnoreOptimChanges,
@@ -3760,7 +3760,7 @@ defaultFlags settings
= [ Opt_AutoLinkPackages,
Opt_DiagnosticsShowCaret,
Opt_EmbedManifest,
- Opt_FlatCache,
+ Opt_FamAppCache,
Opt_GenManifest,
Opt_GhciHistory,
Opt_GhciSandbox,
@@ -5100,4 +5100,3 @@ initSDocContext dflags style = SDC
-- | Initialize the pretty-printing options using the default user style
initDefaultSDocContext :: DynFlags -> SDocContext
initDefaultSDocContext dflags = initSDocContext dflags defaultUserStyle
-
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1688,7 +1688,10 @@ When reporting that GHC can't solve (a ~ c), there are two givens in scope:
redundant), so it's not terribly useful to report it in an error message.
To accomplish this, we discard any Implications that do not bind any
equalities by filtering the `givens` selected in `misMatchOrCND` (based on
-the `ic_given_eqs` field of the Implication).
+the `ic_given_eqs` field of the Implication). Note that we discard givens
+that have no equalities whatsoever, but we want to keep ones with only *local*
+equalities, as these may be helpful to the user in understanding what went
+wrong.
But this is not enough to avoid all redundant givens! Consider this example,
from #15361:
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1596,7 +1596,7 @@ In this Note, "decomposition" refers to taking the constraint
where that notation indicates a list of new constraints, where the
new constraints may have different flavours and different roles.
-The key property to consider is injectivity. When decomposing a Given the
+The key property to consider is injectivity. When decomposing a Given, the
decomposition is sound if and only if T is injective in all of its type
arguments. When decomposing a Wanted, the decomposition is sound (assuming the
correct roles in the produced equality constraints), but it may be a guess --
@@ -1614,13 +1614,13 @@ Pursuing the details requires exploring three axes:
* Role: Nominal vs. Representational
* TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
-(So a type variable isn't a TyCon, but it's convenient to put the AppTy case
+(A type variable isn't a TyCon, of course, but it's convenient to put the AppTy case
in the same table.)
Right away, we can say that Derived behaves just as Wanted for the purposes
of decomposition. The difference between Derived and Wanted is the handling of
evidence. Since decomposition in these cases isn't a matter of soundness but of
-guessing, we want the same behavior regardless of evidence.
+guessing, we want the same behaviour regardless of evidence.
Here is a table (discussion following) detailing where decomposition of
(T s1 ... sn) ~r (T t1 .. tn)
@@ -1634,7 +1634,7 @@ NOMINAL GIVEN WANTED WHERE
Datatype YES YES canTyConApp
Newtype YES YES canTyConApp
Data family YES YES canTyConApp
-Type family NO{1} YES, in injective args{1} canEqFun
+Type family NO{1} YES, in injective args{1} canEqCanLHS2
AppTy YES YES can_eq_app
REPRESENTATIONAL GIVEN WANTED
@@ -1642,11 +1642,9 @@ REPRESENTATIONAL GIVEN WANTED
Datatype YES YES canTyConApp
Newtype NO{2} MAYBE{2} canTyConApp(can_decompose)
Data family NO{3} MAYBE{3} canTyConApp(can_decompose)
-Type family NO NO canEqFun
+Type family NO NO canEqCanLHS2
AppTy NO{4} NO{4} can_eq_nc'
-"RAE" update all this; no more canEqFun
-
{1}: Type families can be injective in some, but not all, of their arguments,
so we want to do partial decomposition. This is quite different than the way
other decomposition is done, where the decomposed equalities replace the original
@@ -1658,9 +1656,9 @@ decompose an injective-type-family Given.
{2}: See Note [Decomposing newtypes at representational role]
{3}: Because of the possibility of newtype instances, we must treat
-data families like newtypes. See also Note [Decomposing newtypes at
-representational role]. See #10534 and test case
-typecheck/should_fail/T10534.
+data families like newtypes. See also
+Note [Decomposing newtypes at representational role]. See #10534 and
+test case typecheck/should_fail/T10534.
{4}: See Note [Decomposing AppTy at representational role]
@@ -2189,7 +2187,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
| otherwise -- ordinary, non-injective type family
= []
- ; mapM_ (unifyDerived (ctEvLoc ev) Nominal) inj_eqns
+ ; unless (isGiven ev) $
+ mapM_ (unifyDerived (ctEvLoc ev) Nominal) inj_eqns
; tclvl <- getTcLevel
; dflags <- getDynFlags
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -31,6 +31,7 @@ import GHC.Tc.Solver.Monad as TcS
import GHC.Utils.Misc
import Control.Monad
import GHC.Utils.Monad ( zipWith3M )
+import Data.List.NonEmpty ( NonEmpty(..) )
import Control.Arrow ( first )
@@ -273,11 +274,9 @@ flattenType loc ty
{- Note [Flattening]
~~~~~~~~~~~~~~~~~~~~
-"RAE": update
-
flatten ty ==> (xi, co)
where
- xi has no type functions, unless they appear under ForAlls
+ xi has no reducible type functions
has no skolems that are mapped in the inert set
has no filled-in metavariables
co :: xi ~ ty
@@ -287,8 +286,7 @@ Key invariants:
(F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
(F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
-Note that it is flatten's job to flatten *every type function it sees*.
-flatten is only called on *arguments* to type functions, by canEqGiven.
+Note that it is flatten's job to try to reduce *every type function it sees*.
Flattening also:
* zonks, removing any metavariables, and
@@ -323,22 +321,12 @@ Recall that in comments we use alpha[flat = ty] to represent a
flattening skolem variable alpha which has been generated to stand in
for ty.
------ Example of flattening a constraint: ------
- flatten (List (F (G Int))) ==> (xi, cc)
- where
- xi = List alpha
- cc = { G Int ~ beta[flat = G Int],
- F beta ~ alpha[flat = F beta] }
-Here
- * alpha and beta are 'flattening skolem variables'.
- * All the constraints in cc are 'given', and all their coercion terms
- are the identity.
-
Note that we prefer to leave type synonyms unexpanded when possible,
so when the flattener encounters one, it first asks whether its
-transitive expansion contains any type function applications. If so,
+transitive expansion contains any type function applications or is
+forgetful -- that is, omits one or more type variables in its RHS. If so,
it expands the synonym and proceeds; if not, it simply returns the
-unexpanded synonym.
+unexpanded synonym. See also Note [Flattening synonyms].
Note [flatten_args performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -796,8 +784,8 @@ flatten_exact_fam_app_fully tc tys
ret_co = mkTyConAppCo role tc cos
-- ret_co :: F xis ~ F tys; might be heterogeneous
- -- Now, look in the cache
- ; mb_ct <- liftTcS $ lookupFlatCache tc xis
+ -- Now, look in the inerts and the cache
+ ; mb_ct <- liftTcS $ lookupFamApp tc xis
; dflags <- getDynFlags
; loc <- getLoc
; case mb_ct of
@@ -883,7 +871,7 @@ flatten_exact_fam_app_fully tc tys
; flavour <- getFlavour
-- NB: only extend cache with nominal, given equalities
; when (eq_rel == NomEq && flavour == Given) $
- liftTcS $ extendFlatCache tc tys (co, xi)
+ liftTcS $ extendFamAppCache tc tys (co, xi)
; let role = eqRelRole eq_rel
xi' = xi `mkCastTy` kind_co
co' = update_co $
@@ -1027,8 +1015,8 @@ flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
flatten_tyvar2 tv fr@(_, eq_rel)
= do { ieqs <- liftTcS $ getInertEqs
; case lookupDVarEnv ieqs tv of
- Just (ct:_) -- If the first doesn't work,
- -- the subsequent ones won't either
+ Just (EqualCtList (ct :| _)) -- If the first doesn't work,
+ -- the subsequent ones won't either
| CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
, cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
, let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -57,6 +57,7 @@ import GHC.Types.Unique( hasKey )
import GHC.Driver.Session
import GHC.Utils.Misc
import qualified GHC.LanguageExtensions as LangExt
+import Data.List.NonEmpty ( NonEmpty(..) )
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
@@ -1247,11 +1248,9 @@ improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcType
-- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y'
--
-- See Note [FunDep and implicit parameter reactions]
--- No Givens here: Note [No FunEq improvement for Givens]
-- Precondition: isImprovable work_ev
improveLocalFunEqs work_ev inerts fam_tc args rhs
- = ASSERT( not (isGiven work_ev) )
- ASSERT( isImprovable work_ev )
+ = ASSERT( isImprovable work_ev )
unless (null improvement_eqns) $
do { traceTcS "interactFunEq improvements: " $
vcat [ text "Eqns:" <+> ppr improvement_eqns
@@ -1260,7 +1259,8 @@ improveLocalFunEqs work_ev inerts fam_tc args rhs
; emitFunDepDeriveds improvement_eqns }
where
funeqs = inert_funeqs inerts
- funeqs_for_tc = [ funeq_ct | funeq_ct : _ <- findFunEqsByTyCon funeqs fam_tc
+ funeqs_for_tc = [ funeq_ct | EqualCtList (funeq_ct :| _)
+ <- findFunEqsByTyCon funeqs fam_tc
, NomEq == ctEqRel funeq_ct ]
-- representational equalities don't interact
-- with type family dependencies
@@ -1315,16 +1315,12 @@ improveLocalFunEqs work_ev inerts fam_tc args rhs
ctl_depth work_loc }
{- Note [Type inference for type families with injectivity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-"RAE": Update this Note.
-
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have a type family with an injectivity annotation:
type family F a b = r | r -> b
-Then if we have two CFunEqCan constraints for F with the same RHS
- F s1 t1 ~ rhs
- F s2 t2 ~ rhs
-then we can use the injectivity to get a new Derived constraint on
+Then if we have an equality like F s1 t1 ~ F s2 t2,
+we can use the injectivity to get a new Derived constraint on
the injective argument
[D] t1 ~ t2
@@ -1351,8 +1347,20 @@ We could go further and offer evidence from decomposing injective type-function
applications, but that would require new evidence forms, and an extension to
FC, so we don't do that right now (Dec 14).
-See also Note [Injective type families] in GHC.Core.TyCon
+We generate these Deriveds in three places, depending on how we notice the
+injectivity.
+
+1. When we have a [W/D] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and
+described in Note [Decomposing equality] in GHC.Tc.Solver.Canonical.
+
+2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these
+constraints rewrites the other, as they have different LHSs. This is done
+in improveLocalFunEqs, called during the interactWithInertsStage.
+
+3. When we have [W] F tys ~ T and an equation for F that looks like F tys' = T.
+This is done in improve_top_fun_eqs, called from the top-level reactions stage.
+See also Note [Injective type families] in GHC.Core.TyCon
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1454,22 +1462,19 @@ interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs
= do { traceTcS "Not unifying representational equality" (ppr workItem)
; continueWith workItem }
- | isGiven ev -- See Note [Touchables and givens]
- -- See Note [No FunEq improvement for Givens]
- = continueWith workItem
+ -- try improvement, if possible
+ | TyFamLHS fam_tc fam_args <- lhs
+ , isImprovable ev
+ = do { improveLocalFunEqs ev inerts fam_tc fam_args rhs
+ ; continueWith workItem }
| TyVarLHS tv <- lhs
+ , not (isGiven ev) -- See Note [Touchables and givens]
, canSolveByUnification tclvl tv rhs
= do { solveByUnification ev tv rhs
; n_kicked <- kickOutAfterUnification tv
; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
- -- try improvement, if possible
- | TyFamLHS fam_tc fam_args <- lhs
- , isImprovable ev
- = do { improveLocalFunEqs ev inerts fam_tc fam_args rhs
- ; continueWith workItem }
-
| otherwise
= continueWith workItem
@@ -1740,8 +1745,7 @@ doTopReactEq work_item = doTopReactOther work_item
improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcType -> TcS ()
-- See Note [FunDep and implicit parameter reactions]
improveTopFunEqs ev fam_tc args rhs
- | isGiven ev -- See Note [No FunEq improvement for Givens]
- || not (isImprovable ev)
+ | not (isImprovable ev)
= return ()
| otherwise
@@ -1871,24 +1875,6 @@ kinds much match too; so it's easier to let the normal machinery
handle it. Instead we are careful to orient the new derived
equality with the template on the left. Delicate, but it works.
-Note [No FunEq improvement for Givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We don't do improvements (injectivity etc) for Givens. Why?
-
-* It generates Derived constraints on skolems, which don't do us
- much good, except perhaps identify inaccessible branches.
- (They'd be perfectly valid though.)
-
-* For type-nat stuff the derived constraints include type families;
- e.g. (a < b), (b < c) ==> a < c If we generate a Derived for this,
- we'll generate a Derived/Wanted CFunEqCan; and, since the same
- InertCans (after solving Givens) are used for each iteration, that
- massively confused the unflattening step (GHC.Tc.Solver.Flatten.unflatten).
-
- In fact it led to some infinite loops:
- indexed-types/should_compile/T10806
- indexed-types/should_compile/T10507
- polykinds/T10742
-}
{- *******************************************************************
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1,4 +1,5 @@
-{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies, ScopedTypeVariables #-}
+{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies, ScopedTypeVariables, TypeApplications,
+ DerivingStrategies, GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates -Wno-incomplete-uni-patterns #-}
@@ -80,7 +81,7 @@ module GHC.Tc.Solver.Monad (
addDictsByClass, delDict, foldDicts, filterDicts, findDict,
-- Inert CEqCans
- EqualCtList, findTyEqs, foldTyEqs,
+ EqualCtList(..), findTyEqs, foldTyEqs,
findEq,
-- Inert solved dictionaries
@@ -90,7 +91,7 @@ module GHC.Tc.Solver.Monad (
foldIrreds,
-- The flattening cache
- lookupFlatCache, extendFlatCache,
+ lookupFamApp, extendFamAppCache,
pprKicked,
-- Inert function equalities
@@ -186,6 +187,8 @@ import GHC.Utils.Monad
import Data.IORef
import Data.List ( partition, mapAccumL )
import qualified Data.Semigroup as S
+import Data.List.NonEmpty ( NonEmpty(..), cons, toList, nonEmpty )
+import qualified Data.List.NonEmpty as NE
#if defined(DEBUG)
import GHC.Data.Graph.Directed
@@ -399,12 +402,13 @@ data InertSet
-- used to undo the cycle-breaking needed to handle
-- Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
- , inert_flat_cache :: FunEqMap (TcCoercion, TcType)
+ , inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
-- If F tys :-> (co, rhs, flav),
-- then co :: F tys ~ rhs
-- flav is [G]
--
- -- Just a hash-cons cache for use when flattening only
+ -- Just a hash-cons cache for use when reducing family applications
+ -- only
--
-- Only nominal, Given equalities end up in here (along with
-- top-level instances)
@@ -438,7 +442,7 @@ emptyInert :: InertSet
emptyInert
= IS { inert_cans = emptyInertCans
, inert_cycle_breakers = []
- , inert_flat_cache = emptyFunEqs
+ , inert_famapp_cache = emptyFunEqs
, inert_solved_dicts = emptyDictMap }
@@ -715,7 +719,35 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
}
type InertEqs = DTyVarEnv EqualCtList
-type EqualCtList = [Ct] -- See Note [EqualCtList invariants]
+
+newtype EqualCtList = EqualCtList (NonEmpty Ct)
+ deriving newtype Outputable
+ -- See Note [EqualCtList invariants]
+
+unitEqualCtList :: Ct -> EqualCtList
+unitEqualCtList ct = EqualCtList (ct :| [])
+
+addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
+-- NB: This function maintains the "derived-before-wanted" invariant of EqualCtList,
+-- but not the others. See Note [EqualCtList invariants]
+addToEqualCtList ct (EqualCtList old_eqs)
+ | isWantedCt ct
+ , eq1 :| eqs <- old_eqs
+ = EqualCtList (eq1 :| ct : eqs)
+ | otherwise
+ = EqualCtList (ct `cons` old_eqs)
+
+filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
+filterEqualCtList pred (EqualCtList cts)
+ = fmap EqualCtList (nonEmpty $ NE.filter pred cts)
+
+equalCtListToList :: EqualCtList -> [Ct]
+equalCtListToList (EqualCtList cts) = toList cts
+
+listToEqualCtList :: [Ct] -> Maybe EqualCtList
+-- NB: This does not maintain invariants other than having the EqualCtList be
+-- non-empty
+listToEqualCtList cts = EqualCtList <$> nonEmpty cts
{- Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -756,8 +788,6 @@ The Wanteds can't rewrite anything which is why we put them last
Note [inert_eqs: the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-"RAE": update. Don't forget to update (K1). See kick_out_rewritable
-
Definition [Can-rewrite relation]
A "can-rewrite" relation between flavours, written f1 >= f2, is a
binary relation with the following properties
@@ -770,25 +800,24 @@ Lemma. If f1 >= f then f1 >= f1
Proof. By property (R2), with f1=f2
Definition [Generalised substitution]
-A "generalised substitution" S is a set of triples (a -f-> t), where
- a is a type variable
+A "generalised substitution" S is a set of triples (t0 -f-> t), where
+ t0 is a type variable or an exactly-saturated type family application
t is a type
f is a flavour
such that
- (WF1) if (a -f1-> t1) in S
- (a -f2-> t2) in S
- then neither (f1 >= f2) nor (f2 >= f1) hold
- (WF2) if (a -f-> t) is in S, then t /= a
+ (WF1) if (t0 -f1-> t1) in S
+ (t0' -f2-> t2) in S
+ then either not (f1 >= f2) or t0 does not appear within t0'
+ (WF2) if (t0 -f-> t) is in S, then t /= t0
Definition [Applying a generalised substitution]
If S is a generalised substitution
- S(f,a) = t, if (a -fs-> t) in S, and fs >= f
- = a, otherwise
-Application extends naturally to types S(f,t), modulo roles.
-See Note [Flavours with roles].
+ S(f,t0) = t, if (t0 -fs-> t) in S, and fs >= f
+ = apply S to components of t0, otherwise
+See also Note [Flavours with roles].
-Theorem: S(f,a) is well defined as a function.
-Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
+Theorem: S(f,t0) is well defined as a function.
+Proof: Suppose (t0 -f1-> t1) and (t0 -f2-> t2) are both in S,
and f1 >= f and f2 >= f
Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
@@ -811,40 +840,41 @@ Our main invariant:
----------------------------------------------------------------
Note that inertness is not the same as idempotence. To apply S to a
-type, you may have to apply it recursive. But inertness does
+type, you may have to apply it recursively. But inertness does
guarantee that this recursive use will terminate.
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main Theorem [Stability under extension]
Suppose we have a "work item"
- a -fw-> t
+ t0 -fw-> t
and an inert generalised substitution S,
- THEN the extended substitution T = S+(a -fw-> t)
+ THEN the extended substitution T = S+(t0 -fw-> t)
is an inert generalised substitution
PROVIDED
- (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_)
- (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_)
- (T3) a not in t -- No occurs check in the work item
+ (T1) S(fw,t0) = t0 -- LHS of work-item is a fixpoint of S(fw,_)
+ (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_)
+ (T3) t0 not in t -- No occurs check in the work item
- AND, for every (b -fs-> s) in S:
+ AND, for every (t0' -fs-> s) in S:
(K0) not (fw >= fs)
Reason: suppose we kick out (a -fs-> s),
- and add (a -fw-> t) to the inert set.
+ and add (t0 -fw-> t) to the inert set.
The latter can't rewrite the former,
so the kick-out achieved nothing
- OR { (K1) not (
+ OR { (K1) t0 is not rewritable in t0'. That is, t0 does not occur
+ in t0' (except perhaps in a cast or coercion).
Reason: if fw >= fs, WF1 says we can't have both
- a -fw-> t and a -fs-> s
+ t0 -fw-> t and F t0 -fs-> s
AND (K2): guarantees inertness of the new substitution
{ (K2a) not (fs >= fs)
OR (K2b) fs >= fw
- OR (K2d) a not in s }
+ OR (K2d) t0 not in s }
AND (K3) See Note [K3: completeness of solving]
- { (K3a) If the role of fs is nominal: s /= a
+ { (K3a) If the role of fs is nominal: s /= t0
(K3b) If the role of fs is representational:
s is not of form (a t1 .. tn) } }
@@ -883,10 +913,10 @@ The idea is that
It's used to avoid even looking for constraint to kick out.
* Lemma (L1): The conditions of the Main Theorem imply that there is no
- (a -fs-> t) in S, s.t. (fs >= fw).
+ (t0 -fs-> t) in S, s.t. (fs >= fw).
Proof. Suppose the contrary (fs >= fw). Then because of (T1),
- S(fw,a)=a. But since fs>=fw, S(fw,a) = s, hence s=a. But now we
- have (a -fs-> a) in S, which contradicts (WF2).
+ S(fw,t0)=t0. But since fs>=fw, S(fw,t0) = s, hence s=t0. But now we
+ have (t0 -fs-> t0) in S, which contradicts (WF2).
* The extended substitution satisfies (WF1) and (WF2)
- (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
@@ -1034,7 +1064,7 @@ instance Outputable InertCans where
, text "Unsolved goals =" <+> int count
]
where
- folder eqs rest = listToBag eqs `andCts` rest
+ folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest
{- *********************************************************************
* *
@@ -1364,7 +1394,7 @@ should_split_match_args inert_eqs fun_eqs tys
canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool
canRewriteTv inert_eqs eq_rel tv
- | Just (ct : _) <- lookupDVarEnv inert_eqs tv
+ | Just (EqualCtList (ct :| _)) <- lookupDVarEnv inert_eqs tv
, CEqCan { cc_eq_rel = eq_rel1 } <- ct
= eq_rel1 `eqCanRewrite` eq_rel
| otherwise
@@ -1372,7 +1402,7 @@ canRewriteTv inert_eqs eq_rel tv
canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam fun_eqs eq_rel tf args
- | Just (ct : _) <- findFunEq fun_eqs tf args
+ | Just (EqualCtList (ct :| _)) <- findFunEq fun_eqs tf args
, CEqCan { cc_eq_rel = eq_rel1 } <- ct
= eq_rel1 `eqCanRewrite` eq_rel
| otherwise
@@ -1392,7 +1422,7 @@ isImprovable _ = True
addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq old_eqs tv ct
- = extendDVarEnv_C add_eq old_eqs tv [ct]
+ = extendDVarEnv_C add_eq old_eqs tv (unitEqualCtList ct)
where
add_eq old_eqs _ = addToEqualCtList ct old_eqs
@@ -1402,43 +1432,36 @@ addCanFunEq old_eqs fun_tc fun_args ct
= alterTcApp old_eqs fun_tc fun_args upd
where
upd (Just old_equal_ct_list) = Just $ addToEqualCtList ct old_equal_ct_list
- upd Nothing = Just $ [ct]
-
-addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
-addToEqualCtList ct old_eqs
- | isWantedCt ct
- , (eq1 : eqs) <- old_eqs
- = eq1 : ct : eqs
- | otherwise
- = ct : old_eqs
+ upd Nothing = Just $ unitEqualCtList ct
foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs k eqs z
- = foldDVarEnv (\cts z -> foldr k z cts) z eqs
+ = foldDVarEnv (\(EqualCtList cts) z -> foldr k z cts) z eqs
-findTyEqs :: InertCans -> TyVar -> EqualCtList
-findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
+findTyEqs :: InertCans -> TyVar -> [Ct]
+findTyEqs icans tv = maybe [] id (fmap @Maybe equalCtListToList $
+ lookupDVarEnv (inert_eqs icans) tv)
delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
delEq ic lhs rhs = case lhs of
TyVarLHS tv
- -> ic { inert_eqs = modifyDVarEnv (filter (not . isThisOne)) (inert_eqs ic) tv }
+ -> ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
TyFamLHS tf args
-> ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
- where
- upd (Just eq_ct_list)
- | null filtered = Nothing
- | otherwise = Just filtered
- where filtered = filter (not . isThisOne) eq_ct_list
- upd Nothing = Nothing
where
+ isThisOne :: Ct -> Bool
isThisOne (CEqCan { cc_rhs = t1 }) = tcEqTypeNoKindCheck rhs t1
isThisOne other = pprPanic "delEq" (ppr lhs $$ ppr ic $$ ppr other)
-findEq :: InertCans -> CanEqLHS -> EqualCtList
+ upd :: Maybe EqualCtList -> Maybe EqualCtList
+ upd (Just eq_ct_list) = filterEqualCtList (not . isThisOne) eq_ct_list
+ upd Nothing = Nothing
+
+findEq :: InertCans -> CanEqLHS -> [Ct]
findEq icans (TyVarLHS tv) = findTyEqs icans tv
findEq icans (TyFamLHS fun_tc fun_args)
- = findFunEq (inert_funeqs icans) fun_tc fun_args `orElse` []
+ = maybe [] id (fmap @Maybe equalCtListToList $
+ findFunEq (inert_funeqs icans) fun_tc fun_args)
{- *********************************************************************
* *
@@ -1707,11 +1730,12 @@ kick_out_rewritable new_fr new_lhs
-> EqualCtList -> ([Ct], container)
-> ([Ct], container)
kick_out_eqs extend eqs (acc_out, acc_in)
- = (eqs_out `chkAppend` acc_out, case eqs_in of
- [] -> acc_in
- (eq1:_) -> extend acc_in (cc_lhs eq1) eqs_in)
+ = (eqs_out `chkAppend` acc_out, case listToEqualCtList eqs_in of
+ Nothing -> acc_in
+ Just eqs_in_ecl@(EqualCtList (eq1 :| _))
+ -> extend acc_in (cc_lhs eq1) eqs_in_ecl)
where
- (eqs_out, eqs_in) = partition kick_out_eq eqs
+ (eqs_out, eqs_in) = partition kick_out_eq (equalCtListToList eqs)
-- Implements criteria K1-K3 in Note [Extending the inert equalities]
kick_out_eq (CEqCan { cc_lhs = lhs, cc_rhs = rhs_ty
@@ -1955,8 +1979,9 @@ getInertGivens :: TcS [Ct]
getInertGivens
= do { inerts <- getInertCans
; let all_cts = foldDicts (:) (inert_dicts inerts)
- $ foldFunEqs (++) (inert_funeqs inerts)
- $ concat (dVarEnvElts (inert_eqs inerts))
+ $ foldFunEqs (\ecl out -> equalCtListToList ecl ++ out)
+ (inert_funeqs inerts)
+ $ concatMap equalCtListToList (dVarEnvElts (inert_eqs inerts))
; return (filter isGivenCt all_cts) }
getPendingGivenScs :: TcS [Ct]
@@ -2043,8 +2068,9 @@ getUnsolvedInerts
add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
| otherwise = cts
- add_if_unsolveds :: [Ct] -> Cts -> Cts
- add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts new_cts
+ add_if_unsolveds :: EqualCtList -> Cts -> Cts
+ add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts
+ (equalCtListToList new_cts)
is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
@@ -2079,8 +2105,8 @@ getHasGivenEqs tclvl
lift_equal_ct_list :: (Ct -> HasGivenEqs) -> EqualCtList -> HasGivenEqs
-- returns NoGivenEqs for non-singleton lists, as Given lists are always
-- singletons
- lift_equal_ct_list check [ct] = check ct
- lift_equal_ct_list _ _ = NoGivenEqs
+ lift_equal_ct_list check (EqualCtList (ct :| [])) = check ct
+ lift_equal_ct_list _ _ = NoGivenEqs
check_local_given_tv_eq :: Ct -> HasGivenEqs
check_local_given_tv_eq (CEqCan { cc_lhs = TyVarLHS tv, cc_ev = ev})
@@ -2102,7 +2128,10 @@ getHasGivenEqs tclvl
is_outer_var :: TyCoVar -> Bool
is_outer_var tv
- | isTyVar tv = tclvl `strictlyDeeperThan` tcTyVarLevel tv
+ -- NB: a meta-tv alpha[3] may end up unifying with skolem b[2],
+ -- so treat it as an "outer" var, even at level 3.
+ | isTyVar tv = isTouchableMetaTyVar tclvl tv ||
+ tclvl `strictlyDeeperThan` tcTyVarLevel tv
| otherwise = False
-- | Returns Given constraints that might,
@@ -2215,8 +2244,6 @@ considered rigid.
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-"RAE": update note
-
Consider an implication
beta => alpha ~ Int
where beta is a unification variable that has already been unified
@@ -2245,23 +2272,38 @@ are some wrinkles:
beta => ...blah...
If we still don't know what beta is, we conservatively treat it as potentially
becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.
+ Note that we can't really know what's in an irred, so any irred is considered
+ a potential equality.
+
+ * What about something like forall a b. a ~ F b => [W] c ~ X y z? That Given
+ cannot affect the Wanted, because the Given is entirely *local*: it mentions
+ only skolems bound in the very same implication. Such equalities need not
+ prevent floating. (Test case typecheck/should_compile/LocalGivenEqs has a
+ real-life motivating example, with some detailed commentary.) These
+ equalities are noted with LocalGivenEqs: they do not prevent floating, but
+ they also are allowed to show up in error messages. See
+ Note [Suppress redundant givens during error reporting] in GHC.Tc.Errors.
+ The difference between what stops floating and what is suppressed from
+ error messages is why we need three options for HasGivenEqs.
+
+ There is also a simpler case that triggers this behaviour:
- * When flattening givens, we generate Given equalities like
- <F [a]> : F [a] ~ f,
- with Refl evidence, and we *don't* want those to count as an equality
- in the givens! After all, the entire flattening business is just an
- internal matter, and the evidence does not mention any of the 'givens'
- of this implication. So we do not treat inert_funeqs as a 'given equality'.
+ data T where
+ MkT :: F a ~ G b => a -> b -> T
+
+ f (MkT _ _) = True
+
+ Because of this behaviour around local equality givens, we can infer the
+ type of f. This is typecheck/should_compile/LocalGivenEqs2.
* See Note [Let-bound skolems] for another wrinkle
- * We do *not* need to worry about representational equalities, because
- these do not affect the ability to float constraints.
+ * We need not look at the equality relation involved (nominal vs representational),
+ because representational equalities can still imply nominal ones. For example,
+ if (G a ~R G b) and G's argument's role is nominal, then we can deduce a ~N b.
Note [Let-bound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
-"RAE": Update note.
-
If * the inert set contains a canonical Given CEqCan (a ~ ty)
and * 'a' is a skolem bound in this very implication,
@@ -2326,20 +2368,22 @@ removeInertCt is ct =
CIrredCan {} -> panic "removeInertCt: CIrredEvCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
-lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole))
-lookupFlatCache fam_tc tys
- = do { IS { inert_flat_cache = flat_cache
+-- | Looks up a family application in both the inerts and the famapp-cache
+lookupFamApp :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole))
+lookupFamApp fam_tc tys
+ = do { IS { inert_famapp_cache = famapp_cache
, inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
; return (firstJusts [lookup_inerts inert_funeqs,
- lookup_flats flat_cache]) }
+ lookup_famapps famapp_cache]) }
where
lookup_inerts inert_funeqs
- | Just (CEqCan { cc_ev = ctev, cc_rhs = rhs } : _) <- findFunEq inert_funeqs fam_tc tys
+ | Just (EqualCtList (CEqCan { cc_ev = ctev, cc_rhs = rhs } :| _))
+ <- findFunEq inert_funeqs fam_tc tys
= Just (ctEvCoercion ctev, rhs, ctEvFlavourRole ctev)
| otherwise = Nothing
- lookup_flats flat_cache
- | Just (co, rhs) <- findFunEq flat_cache fam_tc tys
+ lookup_famapps famapp_cache
+ | Just (co, rhs) <- findFunEq famapp_cache fam_tc tys
= Just (co, rhs, (Given, NomEq))
| otherwise = Nothing
@@ -2841,10 +2885,8 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
, tcs_count = count
} ->
do { inerts <- TcM.readTcRef old_inert_var
- ; let nest_inert = emptyInert
- { inert_cans = inert_cans inerts
- , inert_solved_dicts = inert_solved_dicts inerts }
- -- See Note [Do not inherit the flat cache]
+ ; let nest_inert = inerts { inert_cycle_breakers = [] }
+ -- all other InertSet fields are inherited
; new_inert_var <- TcM.newTcRef nest_inert
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = TcSEnv { tcs_ev_binds = ref
@@ -2865,22 +2907,10 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
#endif
; return res }
-{- Note [Do not inherit the flat cache]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We do not want to inherit the flat cache when processing nested
-implications. Consider
- a ~ F b, forall c. b~Int => blah
-If we have F b ~ fsk in the flat-cache, and we push that into the
-nested implication, we might miss that F b can be rewritten to F Int,
-and hence perhaps solve it. Moreover, the fsk from outside is
-flattened out after solving the outer level, but and we don't
-do that flattening recursively.
--}
-
nestTcS :: TcS a -> TcS a
-- Use the current untouchables, augmenting the current
-- evidence bindings, and solved dictionaries
--- But have no effect on the InertCans, or on the inert_flat_cache
+-- But have no effect on the InertCans, or on the inert_famapp_cache
-- (we want to inherit the latter from processing the Givens)
nestTcS (TcS thing_inside)
= TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
@@ -3168,15 +3198,15 @@ zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv)
----------------------------
-extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS ()
-extendFlatCache tc xi_args stuff@(_, ty)
+extendFamAppCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS ()
+extendFamAppCache tc xi_args stuff@(_, ty)
= do { dflags <- getDynFlags
- ; when (gopt Opt_FlatCache dflags) $
- do { traceTcS "extendFlatCache" (vcat [ ppr tc <+> ppr xi_args
- , ppr ty ])
+ ; when (gopt Opt_FamAppCache dflags) $
+ do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args
+ , ppr ty ])
-- 'co' can be bottom, in the case of derived items
- ; updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
- is { inert_flat_cache = insertFunEq fc tc xi_args stuff } } }
+ ; updInertTcS $ \ is@(IS { inert_famapp_cache = fc }) ->
+ is { inert_famapp_cache = insertFunEq fc tc xi_args stuff } } }
pprKicked :: Int -> SDoc
pprKicked 0 = empty
=====================================
docs/users_guide/expected-undocumented-flags.txt
=====================================
@@ -70,7 +70,6 @@
-fextended-default-rules
-fffi
-ffi
--fflat-cache
-ffloat-all-lams
-ffloat-lam-args
-ffrontend-opt
=====================================
docs/users_guide/exts/type_families.rst
=====================================
@@ -581,6 +581,51 @@ If the option :extension:`UndecidableInstances` is passed to the compiler, the
above restrictions are not enforced and it is on the programmer to ensure
termination of the normalisation of type families during type inference.
+Reducing type family applications
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. ghc-flag:: -ffamily-application-cache
+ :shortdesc: Use a cache when reducing type family applications
+ :type: dynamic
+ :reverse: -fno-family-application-cache
+ :category:
+
+ The flag :ghc-flag:`-ffamily-application-cache` (on by default) instructs
+ GHC to use a cache when reducing type family applications. In most cases,
+ this will speed up compilation. The use of this flag will not affect
+ runtime behaviour.
+
+When GHC encounters a type family application (like ``F Int a``) in a program,
+it must often reduce it in order to complete type checking. Here is a simple
+example::
+
+ type family F a where
+ F Int = Bool
+ F (Maybe Double) = Char
+
+ g :: F Int -> Bool
+ g = not
+
+Despite the fact that ``g``\'s type mentions ``F Int``, GHC must recognize that
+``g``\'s argument really has type ``Bool``. This is done by *reducing* ``F Int``
+to become ``Bool``. Sometimes, there is not enough information to reduce a type
+family application; we say such an application is *stuck*. Continuing this example,
+an occurrence of ``F (Maybe a)`` (for some type variable ``a``) would be stuck, as
+no equation applies.
+
+During type checking, GHC uses heuristics to determine which type family application
+to reduce next; there is no predictable ordering among different type family applications.
+The non-determinism rarely matters in practice. In most programs, type family reduction
+terminates, and so these choices are immaterial. However, if a type family application
+does not terminate, it is possible that type-checking may unpredictably diverge. (GHC
+will always take the same path for a given source program, but small changes in that
+source program may induce GHC to take a different path. Compiling a given, unchanged
+source program is still deterministic.)
+
+In order to speed up type family reduction, GHC normally uses a cache, remembering what
+type family applications it has previously reduced. This feature can be disabled with
+:ghc-flag:`-fno-family-application-cache`.
+
.. _type-wildcards-lhs:
Wildcards on the LHS of data and type family instances
=====================================
testsuite/tests/indexed-types/should_fail/T13784.stderr
=====================================
@@ -1,6 +1,11 @@
T13784.hs:29:28: error:
- • Couldn't match type ‘as’ with ‘a : Divide a as’
+ • Could not deduce: as ~ (a : Divide a as)
+ from the context: (a : as) ~ (a1 : as1)
+ bound by a pattern with constructor:
+ :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
+ in an equation for ‘divide’
+ at T13784.hs:29:13-19
Expected: Product (Divide a (a : as))
Actual: Product as1
‘as’ is a rigid type variable bound by
=====================================
testsuite/tests/patsyn/should_fail/T11010.stderr
=====================================
@@ -1,6 +1,9 @@
T11010.hs:9:36: error:
- • Couldn't match type ‘a1’ with ‘Int’
+ • Could not deduce: a1 ~ Int
+ from the context: a ~ Int
+ bound by the signature for pattern synonym ‘IntFun’
+ at T11010.hs:9:9-14
Expected: a -> b
Actual: a1 -> b
‘a1’ is a rigid type variable bound by
=====================================
testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
=====================================
@@ -0,0 +1,137 @@
+{-# LANGUAGE RankNTypes, TypeFamilies, FlexibleInstances #-}
+{-# OPTIONS_GHC -Wno-missing-methods -Wno-unused-matches #-}
+
+module LocalGivenEqs where
+
+-- See Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad;
+-- this tests custom treatment for LocalGivenEqs
+
+{-
+I (Richard E) tried somewhat half-heartedly to minimize this, but failed.
+The key bit is the use of the ECP constructor inside the lambda in happyReduction_508.
+(The lack of a type signature on that is not at issue, I believe.) The type
+of ECP is
+ (forall b. DisambECP b => PV (Located b)) -> ECP
+So, the argument to ECP gets a [G] DisambECP b, which (via its superclass) grants
+us [G] b ~ (Body b) GhcPs. In order to infer the type of happy_var_2, we need to
+float some wanted out past this equality. We have Note [Let-bound skolems]
+in GHC.Tc.Solver.Monad to consider this Given equality to be let-like, and thus
+not prevent floating. But, note that the equality isn't quite let-like, because
+it mentions b in its RHS. It thus triggers Note [Type variable cycles in Givens]
+in GHC.Tc.Solver.Canonical. That Note says we change the situation to
+ [G] b ~ cbv GhcPs
+ [G] Body b ~ cbv
+for some fresh CycleBreakerTv cbv. Now, our original equality looks to be let-like,
+but the new cbv equality is *not* let-like -- note that the variable is on the RHS.
+The solution is to consider any equality whose free variables are all at the current
+level to not stop equalities from floating. These are called *local*. Because both
+Givens are local in this way, they no longer prevent floating, and we can type-check
+this example.
+-}
+
+import Data.Kind ( Type )
+import GHC.Exts ( Any )
+
+infixr 9 `HappyStk`
+data HappyStk a = HappyStk a (HappyStk a)
+newtype HappyWrap201 = HappyWrap201 (ECP)
+newtype HappyWrap205 = HappyWrap205 (([Located Token],Bool))
+
+newtype HappyAbsSyn = HappyAbsSyn HappyAny
+type HappyAny = Any
+
+newtype ECP =
+ ECP { unECP :: forall b. DisambECP b => PV (Located b) }
+
+data PV a
+data P a
+data GhcPs
+data Token
+data Located a
+data AnnKeywordId = AnnIf | AnnThen | AnnElse | AnnSemi
+data AddAnn
+data SrcSpan
+type LHsExpr a = Located (HsExpr a)
+data HsExpr a
+
+class b ~ (Body b) GhcPs => DisambECP b where
+ type Body b :: Type -> Type
+ mkHsIfPV :: SrcSpan
+ -> LHsExpr GhcPs
+ -> Bool -- semicolon?
+ -> Located b
+ -> Bool -- semicolon?
+ -> Located b
+ -> PV (Located b)
+
+instance DisambECP (HsExpr GhcPs) where
+ type Body (HsExpr GhcPs) = HsExpr
+ mkHsIfPV = undefined
+
+instance Functor P
+instance Applicative P
+instance Monad P
+
+instance Functor PV
+instance Applicative PV
+instance Monad PV
+
+mj :: AnnKeywordId -> Located e -> AddAnn
+mj = undefined
+
+amms :: Monad m => m (Located a) -> [AddAnn] -> m (Located a)
+amms = undefined
+
+happyIn208 :: ECP -> HappyAbsSyn
+happyIn208 = undefined
+
+happyReturn :: () => a -> P a
+happyReturn = (return)
+
+happyThen :: () => P a -> (a -> P b) -> P b
+happyThen = (>>=)
+
+comb2 :: Located a -> Located b -> SrcSpan
+comb2 = undefined
+
+runPV :: PV a -> P a
+runPV = undefined
+
+happyOutTok :: HappyAbsSyn -> Located Token
+happyOutTok = undefined
+
+happyOut201 :: HappyAbsSyn -> HappyWrap201
+happyOut201 = undefined
+
+happyOut205 :: HappyAbsSyn -> HappyWrap205
+happyOut205 = undefined
+
+happyReduction_508 (happy_x_8 `HappyStk`
+ happy_x_7 `HappyStk`
+ happy_x_6 `HappyStk`
+ happy_x_5 `HappyStk`
+ happy_x_4 `HappyStk`
+ happy_x_3 `HappyStk`
+ happy_x_2 `HappyStk`
+ happy_x_1 `HappyStk`
+ happyRest) tk
+ = happyThen ((case happyOutTok happy_x_1 of { happy_var_1 ->
+ case happyOut201 happy_x_2 of { (HappyWrap201 happy_var_2) ->
+ case happyOut205 happy_x_3 of { (HappyWrap205 happy_var_3) ->
+ case happyOutTok happy_x_4 of { happy_var_4 ->
+ case happyOut201 happy_x_5 of { (HappyWrap201 happy_var_5) ->
+ case happyOut205 happy_x_6 of { (HappyWrap205 happy_var_6) ->
+ case happyOutTok happy_x_7 of { happy_var_7 ->
+ case happyOut201 happy_x_8 of { (HappyWrap201 happy_var_8) ->
+ -- uncomment this next signature to avoid the need
+ -- for special treatment of floating described above
+ ( runPV (unECP happy_var_2 {- :: PV (LHsExpr GhcPs) -}) >>= \ happy_var_2 ->
+ return $ ECP $
+ unECP happy_var_5 >>= \ happy_var_5 ->
+ unECP happy_var_8 >>= \ happy_var_8 ->
+ amms (mkHsIfPV (comb2 happy_var_1 happy_var_8) happy_var_2 (snd happy_var_3) happy_var_5 (snd happy_var_6) happy_var_8)
+ (mj AnnIf happy_var_1:mj AnnThen happy_var_4
+ :mj AnnElse happy_var_7
+ :(map (\l -> mj AnnSemi l) (fst happy_var_3))
+ ++(map (\l -> mj AnnSemi l) (fst happy_var_6))))}}}}}}}})
+ ) (\r -> happyReturn (happyIn208 r))
=====================================
testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, GADTSyntax, ExistentialQuantification #-}
+
+-- This is a simple case that exercises the LocalGivenEqs bullet
+-- of Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad
+-- If a future change rejects this, that's not the end of the world, but it's nice
+-- to be able to infer `f`.
+
+module LocalGivenEqs2 where
+
+type family F a
+type family G b
+
+data T where
+ MkT :: F a ~ G b => a -> b -> T
+
+f (MkT _ _) = True
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -726,3 +726,5 @@ test('T15942', normal, compile, [''])
test('CbvOverlap', normal, compile, [''])
test('InstanceGivenOverlap', normal, compile, [''])
test('InstanceGivenOverlap2', normal, compile, [''])
+test('LocalGivenEqs', normal, compile, [''])
+test('LocalGivenEqs2', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/86418442e025aa6e00f752bd65b67b40b66326db...e2ec2adab5f5af4756b0769dd8af8eb192700c05
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/86418442e025aa6e00f752bd65b67b40b66326db...e2ec2adab5f5af4756b0769dd8af8eb192700c05
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/20201107/b9c9ff9a/attachment-0001.html>
More information about the ghc-commits
mailing list