Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC
Commits:
17e57012 by Simon Peyton Jones at 2025-10-14T22:22:20+01:00
Tidy up trySolveImplication
This completes some leftover mess from
commit 14123ee646f2b9738a917b7cec30f9d3941c13de
Author: Simon Peyton Jones
Date: Wed Aug 20 00:35:48 2025 +0100
Solve forall-constraints via an implication, again
- - - - -
addfb498 by Simon Peyton Jones at 2025-10-15T22:26:30+01:00
Big increment in rewriter tracking
Needs more documentation
- - - - -
11 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Solver/Solve.hs-boot
- compiler/GHC/Tc/Types/Constraint.hs
- testsuite/tests/perf/compiler/T8095.hs
- testsuite/tests/perf/compiler/T9872a.hs
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1690,6 +1690,8 @@ data CoercionHole
-- See Note [CoercionHoles and coercion free variables]
, ch_ref :: IORef (Maybe (Coercion, RewriterSet))
+ -- The RewriterSet is (possibly a superset of)
+ -- the free coercion holes of the coercion
}
coHoleCoVar :: CoercionHole -> CoVar
=====================================
compiler/GHC/Tc/Solver/Default.hs
=====================================
@@ -447,7 +447,7 @@ defaultExceptionContext ct
; empty_ec_id <- lookupId emptyExceptionContextName
; let ev = ctEvidence ct
ev_tm = EvExpr (evWrapIPE (ctEvPred ev) (Var empty_ec_id))
- ; setEvBindIfWanted ev EvCanonical ev_tm
+ ; setDictIfWanted ev EvCanonical ev_tm
-- EvCanonical: see Note [CallStack and ExceptionContext hack]
-- in GHC.Tc.Solver.Dict
; return True }
@@ -541,8 +541,7 @@ defaultEquality encl_eqs ct
= do { traceTcS "defaultEquality success:" (ppr rhs_ty)
; unifyTyVar lhs_tv rhs_ty -- NB: unifyTyVar adds to the
-- TcS unification counter
- ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
- evCoercion (mkReflCo Nominal rhs_ty)
+ ; setEqIfWanted (ctEvidence ct) emptyRewriterSet (mkReflCo Nominal rhs_ty)
; return True
}
@@ -567,8 +566,7 @@ defaultEquality encl_eqs ct
-- See Note [Defaulting representational equalities].
; if null new_eqs
then do { traceTcS "defaultEquality ReprEq } (yes)" empty
- ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
- evCoercion $ mkSubCo co
+ ; setEqIfWanted (ctEvidence ct) emptyRewriterSet (mkSubCo co)
; return True }
else do { traceTcS "defaultEquality ReprEq } (no)" empty
; return False } }
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -178,7 +178,7 @@ solveCallStack ev ev_cs
-- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
= do { inner_stk <- evCallStack pred ev_cs
; let ev_tm = EvExpr (evWrapIPE pred inner_stk)
- ; setEvBindIfWanted ev EvCanonical ev_tm }
+ ; setDictIfWanted ev EvCanonical ev_tm }
-- EvCanonical: see Note [CallStack and ExceptionContext hack]
where
pred = ctEvPred ev
@@ -394,9 +394,18 @@ There are two more similar "equality classes" like this. The full list is
* Coercible coercibleTyCon
(See Note [The equality types story] in GHC.Builtin.Types.Prim.)
-(EQC1) For Givens, when expanding the superclasses of a equality class,
- we can /replace/ the constraint with its superclasses (which, remember, are
- equally powerful) rather than /adding/ them. This can make a huge difference.
+(EQC1) For a Given (boxed) equality like (t1 ~ t2), we /replace/ the constraint
+ with its superclass (which, remember, is equally powerful) rather than /adding/
+ it. Thus, we turn [G] d : t1 ~ t2 into
+ [G] g : t1 ~# t2
+ g := sc_sel d -- Extend the evidence bindings
+
+ We achieve this by
+ (a) not expanding superclasses for equality classes at all;
+ see the `isEqualityClass` test in `mk_strict_superclasses`
+ (b) special logic to solve (t1 ~ t2) in the Given case of `solveEqualityDict`.
+
+ Using replacement rather than adding can make a huge difference.
Consider T17836, which has a constraint like
forall b,c. a ~ (b,c) =>
forall d,e. c ~ (d,e) =>
@@ -411,11 +420,6 @@ There are two more similar "equality classes" like this. The full list is
pattern matching. Its compile-time allocation decreased by 40% when
I added the "replace" rather than "add" semantics.)
- We achieve this by
- (a) not expanding superclasses for equality classes at all;
- see the `isEqualityClass` test in `mk_strict_superclasses`
- (b) special logic to solve (t1 ~ t2) in `solveEqualityDict`.
-
(EQC2) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2,
without worrying about Note [Instance and Given overlap]. Why? Because
if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and
@@ -468,26 +472,29 @@ solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void
-- See Note [Solving equality classes]
-- Precondition: (isEqualityClass cls) True, so cls is (~), (~~), or Coercible
solveEqualityDict ev cls tys
+ | CtGiven (GivenCt { ctev_evar = ev_id }) <- ev
+ , [sel_id] <- classSCSelIds cls -- Equality classes have just one superclass
+ = Stage $
+ do { let loc = ctEvLoc ev
+ sc_pred = classMethodInstTy sel_id tys
+ ev_expr = EvExpr $ Var sel_id `mkTyApps` tys `App` evId ev_id
+ -- See (EQC1) in Note [Solving equality classes]
+ -- This call to newGivenEv makes the evidence binding for the (unboxed) coercion
+ ; given_ev <- newGivenEv loc (sc_pred, ev_expr)
+ ; startAgainWith (mkNonCanonical $ CtGiven given_ev) }
+
| CtWanted (WantedCt { ctev_dest = dest }) <- ev
= Stage $
do { let (role, t1, t2) = matchEqualityInst cls tys
-- Unify t1~t2, putting anything that can't be solved
-- immediately into the work list
- ; co <- wrapUnifierAndEmit ev role $ \uenv ->
- uType uenv t1 t2
+ ; (co,_rws) <- wrapUnifierAndEmit ev role $ \uenv ->
+ uType uenv t1 t2
-- Set d :: (t1~t2) = Eq# co
; setWantedDict dest EvCanonical $
evDictApp cls tys [Coercion co]
; stopWith ev "Solved wanted lifted equality" }
- | CtGiven (GivenCt { ctev_evar = ev_id }) <- ev
- , [sel_id] <- classSCSelIds cls -- Equality classes have just one superclass
- = Stage $
- do { let loc = ctEvLoc ev
- sc_pred = classMethodInstTy sel_id tys
- ev_expr = EvExpr $ Var sel_id `mkTyApps` tys `App` evId ev_id
- ; given_ev <- newGivenEv loc (sc_pred, ev_expr)
- ; startAgainWith (mkNonCanonical $ CtGiven given_ev) }
| otherwise
= pprPanic "solveEqualityDict" (ppr cls)
@@ -730,10 +737,10 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys
| otherwise -- We can either solve the inert from the work-item or vice-versa.
-> case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of
KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr dict_w)
- ; setEvBindIfWanted ev_w EvCanonical (ctEvTerm ev_i)
+ ; setDictIfWanted ev_w EvCanonical (ctEvTerm ev_i)
; return $ Stop ev_w (text "Dict equal" <+> ppr dict_w) }
KeepWork -> do { traceTcS "lookupInertDict:KeepWork" (ppr dict_w)
- ; setEvBindIfWanted ev_i EvCanonical (ctEvTerm ev_w)
+ ; setDictIfWanted ev_i EvCanonical (ctEvTerm ev_w)
; updInertCans (updDicts $ delDict dict_w)
; continueWith () } }
@@ -796,7 +803,7 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
-- See Note [No Given/Given fundeps]
| Just solved_ev <- lookupSolvedDict inerts cls xis -- Cached
- = do { setEvBindIfWanted ev EvCanonical (ctEvTerm solved_ev)
+ = do { setDictIfWanted ev EvCanonical (ctEvTerm solved_ev)
; stopWith ev "Dict/Top (cached)" }
| otherwise -- Wanted, but not cached
@@ -828,7 +835,7 @@ chooseInstance work_item
; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar)
(ppr work_item)
; evc_vars <- mapM (newWanted deeper_loc (ctEvRewriters work_item)) theta
- ; setEvBindIfWanted work_item canonical (mk_ev (map getEvExpr evc_vars))
+ ; setDictIfWanted work_item canonical (mk_ev (map getEvExpr evc_vars))
; emitWorkNC (map CtWanted $ freshGoals evc_vars)
; stopWith work_item "Dict/Top (solved wanted)" }
where
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -10,7 +10,7 @@ module GHC.Tc.Solver.Equality(
import GHC.Prelude
-import {-# SOURCE #-} GHC.Tc.Solver.Solve( trySolveImplication )
+import {-# SOURCE #-} GHC.Tc.Solver.Solve( solveSimpleWanteds )
import GHC.Tc.Solver.Irred( solveIrred )
import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
@@ -372,7 +372,7 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
-- Literals
can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
| l1 == l2
- = do { setEvBindIfWanted ev EvCanonical (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
+ = do { setEqIfWanted ev emptyRewriterSet (mkReflCo (eqRelRole eq_rel) ty1)
; stopWith ev "Equal LitTy" }
-- Decompose FunTy: (s -> t) and (c => t)
@@ -485,7 +485,7 @@ can_eq_nc_forall :: CtEvidence -> EqRel
-- See Note [Solving forall equalities]
can_eq_nc_forall ev eq_rel s1 s2
- | CtWanted (WantedCt { ctev_dest = orig_dest, ctev_rewriters = rws, ctev_loc = loc }) <- ev
+ | CtWanted (WantedCt { ctev_dest = orig_dest }) <- ev
= do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2
flags1 = binderFlags bndrs1
flags2 = binderFlags bndrs2
@@ -541,36 +541,40 @@ can_eq_nc_forall ev eq_rel s1 s2
; traceTcS "Generating wanteds" (ppr s1 $$ ppr s2)
- -- Generate the constraints that live in the body of the implication
- -- See (SF5) in Note [Solving forall equalities]
- ; (unifs, (lvl, (all_co, wanteds)))
- <- reportFineGrainUnifications $
- pushLevelNoWorkList (ppr skol_info) $
- wrapUnifier ev (eqRelRole eq_rel) $ \uenv ->
- go uenv skol_tvs init_subst2 bndrs1 bndrs2
+ -- Generate and solve the constraints that live in the body of the implication
+ -- See (SF5) and (SF6) in Note [Solving forall equalities]
+ ; (unifs, (all_co, solved))
+ <- reportFineGrainUnifications $
+ do { -- Generate constraints
+ (tclvl, (all_co, wanteds))
+ <- pushLevelNoWorkList (ppr skol_info) $
+ wrapUnifier ev (eqRelRole eq_rel) $ \uenv ->
+ go uenv skol_tvs init_subst2 bndrs1 bndrs2
+
+ ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds)
+
+ -- Solve the `wanteds` in a nested context
+ ; ev_binds_var <- newNoTcEvBinds
+ ; residual_wanted <- nestImplicTcS skol_info_anon ev_binds_var tclvl $
+ solveSimpleWanteds wanteds
+
+ ; return (all_co, isSolvedWC residual_wanted) }
+
-- Kick out any inerts constraints that mention unified type variables
; kickOutAfterUnification unifs
- -- Solve the implication right away, using `trySolveImplication`
- -- See (SF6) in Note [Solving forall equalities]
- ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds)
- ; ev_binds_var <- newNoTcEvBinds
- ; solved <- trySolveImplication $
- (implicationPrototype (ctLocEnv loc))
- { ic_tclvl = lvl
- , ic_binds = ev_binds_var
- , ic_info = skol_info_anon
- , ic_warn_inaccessible = False
- , ic_skols = skol_tvs
- , ic_given = []
- , ic_wanted = emptyWC { wc_simple = wanteds } }
-
; if solved
- then do { -- all_co <- zonkCo all_co
- -- -- ToDo: explain this zonk
- setWantedEq orig_dest rws all_co
+ then do { all_co <- zonkCo all_co
+ -- setWantedEq will add `all_co` to the `ebv_tcvs`, to record
+ -- that `all_co` is used. But if `all_co` contains filled
+ -- CoercionHoles, from the nested solve, and we may miss the
+ -- use of CoVars. Test T7196 showed this up
+
+ ; setWantedEq orig_dest emptyRewriterSet all_co
+ -- emptyRewriterSet: fully solved, so all_co has no holes
; stopWith ev "Polytype equality: solved" }
+
else canEqSoftFailure IrredShapeReason ev s1 s2 } }
| otherwise
@@ -592,11 +596,12 @@ can_eq_nc_forall ev eq_rel s1 s2
in (bndr1:bndrs1, phi1, bndr2:bndrs2, phi2)
split_foralls s1 s2 = ([], s1, [], s2)
+
{- Note [Solving forall equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To solve an equality between foralls
[W] (forall a. t1) ~ (forall b. t2)
-the basic plan is simple: use `trySolveImplication` to solve the
+the basic plan is simple: behave rather as if we were solving the
implication constraint
[W] forall a. { t1 ~ (t2[a/b]) }
@@ -643,19 +648,15 @@ There are lots of wrinkles of course:
because we want to /gather/ the equality constraint (to put in the implication)
rather than /emit/ them into the monad, as `wrapUnifierAndEmit` does.
-(SF6) We solve the implication on the spot, using `trySolveImplication`. In
- the past we instead generated an `Implication` to be solved later. Nice in
- some ways but it added complexity:
- - We needed a `wl_implics` field of `WorkList` to collect
- these emitted implications
- - The types of `solveSimpleWanteds` and friends were more complicated
- - Trickily, an `EvFun` had to contain an `EvBindsVar` ref-cell, which made
- `evVarsOfTerm` harder. Now an `EvFun` just contains the bindings.
- The disadvantage of solve-on-the-spot is that if we fail we are simply
- left with an unsolved (forall a. blah) ~ (forall b. blah), and it may
- not be clear /why/ we couldn't solve it. But on balance the error messages
- improve: it is easier to undertand that
- (forall a. a->a) ~ (forall b. b->Int)
+(SF6) We solve the nested constraints right away. In the past we instead generated
+ an `Implication` to be solved later, but we no longer have a convenient place
+ to accumulate such an implication for later solving. Instead we just try to solve
+ them on the spot, and abandon the attempt if we fail.
+
+ In the latter case we are left with an unsolved (forall a. blah) ~ (forall b. blah),
+ and it may not be clear /why/ we couldn't solve it. But on balance the error
+ messages improve: it is easier to understand that
+ (forall a. a->a) ~ (forall b. b->Int)
is insoluble than it is to understand a message about matching `a` with `Int`.
-}
@@ -809,11 +810,11 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-- to an irreducible constraint; see typecheck/should_compile/T10494
-- See Note [Decomposing AppTy equalities]
can_eq_app ev s1 t1 s2 t2
- | CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rws }) <- ev
+ | CtWanted (WantedCt { ctev_dest = dest }) <- ev
= do { traceTcS "can_eq_app" (vcat [ text "s1:" <+> ppr s1, text "t1:" <+> ppr t1
, text "s2:" <+> ppr s2, text "t2:" <+> ppr t2
, text "vis:" <+> ppr (isNextArgVisible s1) ])
- ; co <- wrapUnifierAndEmit ev Nominal $ \uenv ->
+ ; (co,rws) <- wrapUnifierAndEmit ev Nominal $ \uenv ->
-- Unify arguments t1/t2 before function s1/s2, because
-- the former have smaller kinds, and hence simpler error messages
-- c.f. GHC.Tc.Utils.Unify.uType (go_app)
@@ -1374,11 +1375,11 @@ canDecomposableTyConAppOK ev eq_rel tc (ty1,tys1) (ty2,tys2)
do { traceTcS "canDecomposableTyConAppOK"
(ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2)
; case ev of
- CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rws })
+ CtWanted (WantedCt { ctev_dest = dest })
-- new_locs and tc_roles are both infinite, so we are
-- guaranteed that cos has the same length as tys1 and tys2
-- See Note [Fast path when decomposing TyConApps]
- -> do { co <- wrapUnifierAndEmit ev role $ \uenv ->
+ -> do { (co,rws) <- wrapUnifierAndEmit ev role $ \uenv ->
do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2
-- zipWith4M: see Note [Work-list ordering]
; return (mkTyConAppCo role tc cos) }
@@ -1432,8 +1433,8 @@ canDecomposableFunTy ev eq_rel af f1@(ty1,m1,a1,r1) f2@(ty2,m2,a2,r2)
= do { traceTcS "canDecomposableFunTy"
(ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2)
; case ev of
- CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rws })
- -> do { co <- wrapUnifierAndEmit ev Nominal $ \ uenv ->
+ CtWanted (WantedCt { ctev_dest = dest })
+ -> do { (co,rws) <- wrapUnifierAndEmit ev Nominal $ \ uenv ->
do { let mult_env = uenv `updUEnvLoc` toInvisibleLoc InvisibleMultiplicity
`setUEnvRole` funRole role SelMult
; mult <- uType mult_env m1 m2
@@ -2011,6 +2012,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
then return ev
else rewriteEqEvidence emptyRewriterSet ev swapped
(mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
+ -- emptyRewriterSet: rhs_redn has no CoercionHoles
; let tv_ty = mkTyVarTy tv
final_rhs = reductionReducedType rhs_redn
@@ -2026,8 +2028,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
-- Provide Refl evidence for the constraint
-- Ignore 'swapped' because it's Refl!
- ; setEvBindIfWanted new_ev EvCanonical $
- evCoercion (mkNomReflCo final_rhs)
+ ; setEqIfWanted new_ev emptyRewriterSet (mkNomReflCo final_rhs)
-- Kick out any constraints that can now be rewritten
; kickOutAfterUnification (unitVarSet tv)
@@ -2147,8 +2148,7 @@ canEqReflexive :: CtEvidence -- ty ~ ty
-> TcType -- ty
-> TcS (StopOrContinue a) -- always Stop
canEqReflexive ev eq_rel ty
- = do { setEvBindIfWanted ev EvCanonical $
- evCoercion (mkReflCo (eqRelRole eq_rel) ty)
+ = do { setEqIfWanted ev emptyRewriterSet (mkReflCo (eqRelRole eq_rel) ty)
; stopWith ev "Solved by reflexivity" }
{- Note [Equalities with heterogeneous kinds]
@@ -2649,10 +2649,11 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio
| CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters }) <- old_ev
= do { let rewriters' = rewriters S.<> new_rewriters
- ; (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRewriteRole old_ev) nlhs nrhs
+ ; (new_ev, hole) <- newWantedEq loc rewriters' (ctEvRewriteRole old_ev) nlhs nrhs
; let co = maybeSymCo swapped $
- lhs_co `mkTransCo` hole_co `mkTransCo` mkSymCo rhs_co
- ; setWantedEq dest rewriters' co
+ lhs_co `mkTransCo` mkHoleCo hole `mkTransCo` mkSymCo rhs_co
+ -- new_rewriters has all the holes from lhs_co and rhs_co
+ ; setWantedEq dest (new_rewriters `mappend` unitRewriterSet hole) co
; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev
, ppr nlhs
, ppr nrhs
@@ -2730,11 +2731,11 @@ tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel })
= Stage $
do { inerts <- getInertCans
; if | Just (ev_i, swapped) <- inertsEqsCanDischarge inerts work_item
- -> do { setEvBindIfWanted ev EvCanonical $
- evCoercion (maybeSymCo swapped $
- downgradeRole (eqRelRole eq_rel)
- (ctEvRewriteRole ev_i)
- (ctEvCoercion ev_i))
+ -> do { setEqIfWanted ev (ctEvRewriterSet ev_i) $
+ maybeSymCo swapped $
+ downgradeRole (eqRelRole eq_rel)
+ (ctEvRewriteRole ev_i)
+ (ctEvCoercion ev_i)
; stopWith ev "Solved from inert" }
| otherwise
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -14,11 +14,10 @@ import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
import GHC.Tc.Solver.Monad
import GHC.Tc.Types.Evidence
-import GHC.Core.Coercion
-
import GHC.Types.Basic( SwapFlag(..) )
import GHC.Utils.Outputable
+import GHC.Utils.Panic
import GHC.Data.Bag
@@ -69,9 +68,9 @@ try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
, text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
; case solveOneFromTheOther ct_i ct_w of
- KeepInert -> do { setEvBindIfWanted ev_w EvCanonical (swap_me swap ev_i)
+ KeepInert -> do { setIrredIfWanted ev_w swap ev_i
; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
- KeepWork -> do { setEvBindIfWanted ev_i EvCanonical (swap_me swap ev_w)
+ KeepWork -> do { setIrredIfWanted ev_i swap ev_w
; updInertCans (updIrreds (\_ -> others))
; continueWith () } }
@@ -81,12 +80,19 @@ try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
where
ct_w = CIrredCan irred_w
- swap_me :: SwapFlag -> CtEvidence -> EvTerm
- swap_me swap ev
- = case swap of
- NotSwapped -> ctEvTerm ev
- IsSwapped -> evCoercion (mkSymCo (evTermCoercion (ctEvTerm ev)))
-
+setIrredIfWanted :: CtEvidence -> SwapFlag -> CtEvidence -> TcS ()
+-- Irreds can be equalities or dictionaries
+setIrredIfWanted ev_dest swap ev_source
+ | CtWanted (WantedCt { ctev_dest = dest }) <- ev_dest
+ = case dest of
+ HoleDest {} -> setWantedEq dest (ctEvRewriterSet ev_source)
+ (maybeSymCo swap (ctEvCoercion ev_source))
+
+ EvVarDest {} -> assertPpr (swap==NotSwapped) (ppr ev_dest $$ ppr ev_source) $
+ -- findMatchingIrreds only returns IsSwapped for equalities
+ setWantedDict dest EvCanonical (ctEvTerm ev_source)
+ | otherwise
+ = return ()
{- Note [Multiple matching irreds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -50,13 +50,12 @@ module GHC.Tc.Solver.Monad (
CanonicalEvidence(..),
newTcEvBinds, newNoTcEvBinds,
- newWantedEq, emitNewWantedEq,
+ newWantedEq,
newWanted,
newWantedNC, newWantedEvVarNC,
newBoundEvVarId,
unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications,
- setEvBind, setWantedEq, setWantedDict,
- setWantedEvTerm, setEvBindIfWanted,
+ setEvBind, setWantedEq, setWantedDict, setEqIfWanted, setDictIfWanted,
newEvVar, newGivenEv, emitNewGivens,
emitChildEqs, checkReductionDepth,
@@ -1209,12 +1208,28 @@ setTcLevelTcS :: TcLevel -> TcS a -> TcS a
setTcLevelTcS lvl (TcS thing_inside)
= TcS $ \ env -> TcM.setTcLevel lvl (thing_inside env)
+{- Note [nestImplicTcS]
+~~~~~~~~~~~~~~~~~~~~~~~
+`nestImplicTcS` is used to build a nested scope when we begin solving an implication.
+
+(NI1) One subtle point is that `nestImplicTcS` uses `resetInertCans` to
+ initialise the `InertSet` of the nested scope to the `inert_givens` (/not/
+ the `inert_cans`) of the current inert set. It is super-important not to
+ pollute the sub-solving problem with the unsolved Wanteds of the current
+ scope.
+
+ Whenever we do `solveSimpleGivens`, we snapshot the `inert_cans` into `inert_givens`.
+ (At that moment there should be no Wanteds.)
+-}
+
nestImplicTcS :: SkolemInfoAnon -> EvBindsVar
-> TcLevel -> TcS a
-> TcS a
+-- See Note [nestImplicTcS]
nestImplicTcS skol_info ev_binds_var inner_tclvl (TcS thing_inside)
= TcS $ \ env@(TcSEnv { tcs_inerts = old_inert_var }) ->
- do { nest_inert <- mk_nested_inert_set skol_info old_inert_var
+ do { old_inerts <- TcM.readTcRef old_inert_var
+ ; let nest_inert = mk_nested_inerts old_inerts
; new_inert_var <- TcM.newTcRef nest_inert
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = env { tcs_ev_binds = ev_binds_var
@@ -1233,24 +1248,18 @@ nestImplicTcS skol_info ev_binds_var inner_tclvl (TcS thing_inside)
#endif
; return res }
where
- mk_nested_inert_set skol_info old_inert_var
+ mk_nested_inerts old_inerts
-- For an implication that comes from a static form (static e),
-- start with a completely empty inert set; in particular, no Givens
-- See (SF3) in Note [Grand plan for static forms]
-- in GHC.Iface.Tidy.StaticPtrTable
| StaticFormSkol <- skol_info
- = return (emptyInertSet inner_tclvl)
+ = emptyInertSet inner_tclvl
| otherwise
- = do { inerts <- TcM.readTcRef old_inert_var
-
- -- resetInertCans: initialise the inert_cans from the inert_givens of the
- -- parent so that the child is not polluted with the parent's inert Wanteds
- -- See Note [trySolveImplication] in GHC.Tc.Solver.Solve
- -- All other InertSet fields are inherited
- ; return (pushCycleBreakerVarStack $
- resetInertCans $
- inerts) }
+ = pushCycleBreakerVarStack $
+ resetInertCans $ -- See (NI1) in Note [nestImplicTcS]
+ old_inerts
nestFunDepsTcS :: TcS a -> TcS a
nestFunDepsTcS (TcS thing_inside)
@@ -1950,64 +1959,40 @@ addUsedCoercion co
= do { ev_binds_var <- getTcEvBindsVar
; wrapTcS (TcM.updTcRef (ebv_tcvs ev_binds_var) (co :)) }
+setEqIfWanted :: CtEvidence -> RewriterSet -> TcCoercion -> TcS ()
+setEqIfWanted ev rewriters co
+ = case ev of
+ CtWanted (WantedCt { ctev_dest = dest })
+ -> setWantedEq dest rewriters co
+ _ -> return ()
+
setWantedEq :: HasDebugCallStack => TcEvDest -> RewriterSet -> TcCoercion -> TcS ()
-- ^ Equalities only
-setWantedEq (HoleDest hole) rewriters co
- = do { addUsedCoercion co
- ; fillCoercionHole hole rewriters co }
-setWantedEq (EvVarDest ev) _ _ = pprPanic "setWantedEq: EvVarDest" (ppr ev)
+setWantedEq dest rewriters co
+ = case dest of
+ HoleDest hole -> fillCoercionHole hole rewriters co
+ EvVarDest ev -> pprPanic "setWantedEq: EvVarDest" (ppr ev)
+
+setDictIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
+setDictIfWanted ev canonical tm
+ = case ev of
+ CtWanted (WantedCt { ctev_dest = dest })
+ -> setWantedDict dest canonical tm
+ _ -> return ()
setWantedDict :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
-- ^ Dictionaries only
-setWantedDict (EvVarDest ev_id) canonical tm
- = setEvBind (mkWantedEvBind ev_id canonical tm)
-setWantedDict (HoleDest h) _ _ = pprPanic "setWantedEq: HoleDest" (ppr h)
-
-setWantedEvTerm :: TcEvDest -> RewriterSet -> CanonicalEvidence -> EvTerm -> TcS ()
--- ^ Good for both equalities and non-equalities
-setWantedEvTerm (EvVarDest ev_id) _rewriters canonical tm
- = setEvBind (mkWantedEvBind ev_id canonical tm)
-setWantedEvTerm (HoleDest hole) rewriters _canonical tm
- | Just co <- evTermCoercion_maybe tm
- = do { addUsedCoercion co
- ; fillCoercionHole hole rewriters co }
- | otherwise
- = -- See Note [Yukky eq_sel for a HoleDest]
- do { let co_var = coHoleCoVar hole
- ; setEvBind (mkWantedEvBind co_var EvCanonical tm)
- ; fillCoercionHole hole rewriters (mkCoVarCo co_var) }
-
-{- Note [Yukky eq_sel for a HoleDest]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-How can it be that a Wanted with HoleDest gets evidence that isn't
-just a coercion? i.e. evTermCoercion_maybe returns Nothing.
-
-Consider [G] forall a. blah => a ~ T
- [W] S ~# T
-
-Then doTopReactEqPred carefully looks up the (boxed) constraint (S ~ T)
-in the quantified constraints, and wraps the (boxed) evidence it
-gets back in an eq_sel to extract the unboxed (S ~# T). We can't put
-that term into a coercion, so we add a value binding
- h = eq_sel (...)
-and the coercion variable h to fill the coercion hole.
-We even re-use the CoHole's Id for this binding!
-
-Yuk!
--}
+setWantedDict dest canonical tm
+ = case dest of
+ EvVarDest ev_id -> setEvBind (mkWantedEvBind ev_id canonical tm)
+ HoleDest h -> pprPanic "setWantedEq: HoleDest" (ppr h)
fillCoercionHole :: CoercionHole -> RewriterSet -> Coercion -> TcS ()
fillCoercionHole hole rewriters co
- = do { wrapTcS $ TcM.fillCoercionHole hole (co, rewriters)
+ = do { addUsedCoercion co
+ ; wrapTcS $ TcM.fillCoercionHole hole (co, rewriters)
; kickOutAfterFillingCoercionHole hole rewriters }
-setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
-setEvBindIfWanted ev canonical tm
- = case ev of
- CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters })
- -> setWantedEvTerm dest rewriters canonical tm
- _ -> return ()
-
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds = wrapTcS TcM.newTcEvBinds
@@ -2019,9 +2004,11 @@ newEvVar pred = wrapTcS (TcM.newEvVar pred)
newGivenEv :: CtLoc -> (TcPredType, EvTerm) -> TcS GivenCtEvidence
-- Make a new variable of the given PredType,
--- immediately bind it to the given term
--- and return its CtEvidence
+-- immediately bind it to the given term, and return its CtEvidence
-- See Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint
+--
+-- The `pred` can be an /equality predicate/ t1 ~# t2;
+-- see (EQC1) in Note [Solving equality classes] in GHC.Tc.Solver.Dict
newGivenEv loc (pred, rhs)
= do { new_ev <- newBoundEvVarId pred rhs
; return $ GivenCt { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc } }
@@ -2044,13 +2031,6 @@ emitNewGivens loc pts
, not (ty1 `tcEqType` ty2) ] -- Kill reflexive Givens at birth
; emitWorkNC (map CtGiven gs) }
-emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion
--- | Emit a new Wanted equality into the work-list
-emitNewWantedEq loc rewriters role ty1 ty2
- = do { (wtd, co) <- newWantedEq loc rewriters role ty1 ty2
- ; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical $ CtWanted wtd))
- ; return co }
-
emitChildEqs :: CtEvidence -> Cts -> TcS ()
-- Emit a bunch of equalities into the work list
-- See Note [Work-list ordering] in GHC.Tc.Solver.Equality
@@ -2067,14 +2047,14 @@ emitChildEqs ev eqs
-- | Create a new Wanted constraint holding a coercion hole
-- for an equality between the two types at the given 'Role'.
newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
- -> TcS (WantedCtEvidence, Coercion)
+ -> TcS (WantedCtEvidence, CoercionHole)
newWantedEq loc rewriters role ty1 ty2
= do { hole <- wrapTcS $ TcM.newCoercionHole pty
; let wtd = WantedCt { ctev_pred = pty
, ctev_dest = HoleDest hole
, ctev_loc = loc
, ctev_rewriters = rewriters }
- ; return (wtd, mkHoleCo hole) }
+ ; return (wtd, hole) }
where
pty = mkEqPredRole role ty1 ty2
@@ -2214,10 +2194,11 @@ uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns
wrapUnifierAndEmit :: CtEvidence -> Role
-> (UnifyEnv -> TcM a) -- Some calls to uType
- -> TcS a
+ -> TcS (a, RewriterSet)
-- Like wrapUnifier, but
-- emits any unsolved equalities into the work-list
-- kicks out any inert constraints that mention unified variables
+-- returns a RewriterSet describing the new unsolved goals
wrapUnifierAndEmit ev role do_unifications
= do { (unifs, (res, eqs)) <- reportFineGrainUnifications $
wrapUnifier ev role do_unifications
@@ -2228,7 +2209,7 @@ wrapUnifierAndEmit ev role do_unifications
-- Kick out any inert constraints mentioning the unified variables
; kickOutAfterUnification unifs
- ; return res }
+ ; return (res, rewriterSetFromCts eqs) }
wrapUnifier :: CtEvidence -> Role
-> (UnifyEnv -> TcM a) -- Some calls to uType
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -7,7 +7,6 @@ module GHC.Tc.Solver.Solve (
solveWanteds, -- Solves WantedConstraints
solveSimpleGivens, -- Solves [Ct]
solveSimpleWanteds, -- Solves Cts
- trySolveImplication,
setImplicationStatus
) where
@@ -369,35 +368,6 @@ solveNestedImplications implics
; return unsolved_implics }
-{- Note [trySolveImplication]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-`trySolveImplication` may be invoked while solving simple wanteds, notably from
-`solveWantedForAll`. It returns a Bool to say if solving succeeded or failed.
-
-It uses `nestImplicTcS` to build a nested scope. One subtle point is that
-`nestImplicTcS` uses the `inert_givens` (not the `inert_cans`) of the current
-inert set to initialse the `InertSet` of the nested scope. It is super-important not
-to pollute the sub-solving problem with the unsolved Wanteds of the current scope.
-
-Whenever we do `solveSimpleGivens`, we snapshot the `inert_cans` into `inert_givens`.
-(At that moment there should be no Wanteds.)
--}
-
-trySolveImplication :: Implication -> TcS Bool
--- See Note [trySolveImplication]
-trySolveImplication (Implic { ic_tclvl = tclvl
- , ic_binds = ev_binds_var
- , ic_given = given_ids
- , ic_wanted = wanteds
- , ic_env = ct_loc_env
- , ic_info = info })
- = nestImplicTcS info ev_binds_var tclvl $
- do { let loc = mkGivenLoc tclvl info ct_loc_env
- givens = mkGivens loc given_ids
- ; solveSimpleGivens givens
- ; residual_wanted <- solveWanteds wanteds
- ; return (isSolvedWC residual_wanted) }
-
solveImplication :: Implication -- Wanted
-> TcS Implication -- Simplified implication
-- Precondition: The TcS monad contains an empty worklist and given-only inerts
@@ -1091,7 +1061,7 @@ solveSimpleGivens givens
-- Capture the Givens in the inert_givens of the inert set
-- for use by subsequent calls of nestImplicTcS
- -- See Note [trySolveImplication]
+ -- See Note [nestImplicTcS] in GHc.Tc.Solver.Monad
; updInertSet (\is -> is { inert_givens = inert_cans is })
; cans <- getInertCans
@@ -1273,7 +1243,7 @@ solveCt (CEqCan (EqCt { eq_ev = ev, eq_eq_rel = eq_rel
= solveEquality ev eq_rel (canEqLHSType lhs) rhs
solveCt (CQuantCan qci@(QCI { qci_ev = ev }))
- = do { ev' <- rewriteEvidence ev
+ = do { ev' <- rewriteDictEvidence ev
-- It is (much) easier to rewrite and re-classify than to
-- rewrite the pieces and build a Reduction that will rewrite
-- the whole constraint
@@ -1284,7 +1254,7 @@ solveCt (CQuantCan qci@(QCI { qci_ev = ev }))
_ -> pprPanic "SolveCt" (ppr ev) }
solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc }))
- = do { ev <- rewriteEvidence ev
+ = do { ev <- rewriteDictEvidence ev
-- It is easier to rewrite and re-classify than to rewrite
-- the pieces and build a Reduction that will rewrite the
-- whole constraint
@@ -1309,7 +1279,7 @@ solveNC ev
_ ->
-- Do rewriting on the constraint, especially zonking
- do { ev <- rewriteEvidence ev
+ do { ev <- rewriteDictEvidence ev
-- And then re-classify
; case classifyPredType (ctEvPred ev) of
@@ -1582,7 +1552,7 @@ try_inert_qcs (QCI { qci_ev = ev_w }) inerts =
; continueWith () }
ev_i:_ ->
do { traceTcS "tryInertQCs:KeepInert" (ppr ev_i)
- ; setEvBindIfWanted ev_w EvCanonical (ctEvTerm ev_i)
+ ; setDictIfWanted ev_w EvCanonical (ctEvTerm ev_i)
; stopWith ev_w "Solved Wanted forall-constraint from inert" }
where
matching_inert (QCI { qci_ev = ev_i })
@@ -1689,10 +1659,12 @@ solveWantedQCI _ ct = return (Left ct)
************************************************************************
-}
-rewriteEvidence :: CtEvidence -> SolverStage CtEvidence
--- (rewriteEvidence old_ev new_pred co do_next)
+rewriteDictEvidence :: CtEvidence -> SolverStage CtEvidence
+-- (rewriteDictEvidence old_ev new_pred co do_next)
-- Main purpose: create new evidence for new_pred;
-- unless new_pred is cached already
+-- Precondition: new_pred is not an equality: the evidence is a term-level
+-- thing, hence "Dict".
-- * Calls do_next with (new_ev :: new_pred), with same wanted/given flag as old_ev
-- * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
-- * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
@@ -1723,8 +1695,8 @@ the rewriter set. We check this with an assertion.
-}
-rewriteEvidence ev
- = Stage $ do { traceTcS "rewriteEvidence" (ppr ev)
+rewriteDictEvidence ev
+ = Stage $ do { traceTcS "rewriteDictEvidence" (ppr ev)
; (redn, rewriters) <- rewrite ev (ctEvPred ev)
; finish_rewrite ev redn rewriters }
@@ -1761,8 +1733,8 @@ finish_rewrite
ev_rw_role = ctEvRewriteRole ev
; mb_new_ev <- newWanted loc rewriters' new_pred
; massert (coercionRole co == ev_rw_role)
- ; setWantedEvTerm dest rewriters' EvCanonical $
- evCast (getEvExpr mb_new_ev) $
+ ; setWantedDict dest EvCanonical $
+ evCast (getEvExpr mb_new_ev) $
downgradeRole Representational ev_rw_role (mkSymCo co)
; case mb_new_ev of
Fresh new_ev -> continueWith $ CtWanted new_ev
@@ -1826,17 +1798,22 @@ runTcPluginsWanted wanted
listToBag unsolved_wanted `andCts`
listToBag insols
- ; mapM_ setEv solved_wanted
+ ; mapM_ setPluginEv solved_wanted
; traceTcS "Finished plugins }" (ppr new_wanted)
; return ( notNull (pluginNewCts p), all_new_wanted ) } }
- where
- setEv :: (EvTerm,Ct) -> TcS ()
- setEv (ev,ct) = case ctEvidence ct of
- CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters })
- -> setWantedEvTerm dest rewriters EvCanonical ev
- -- TODO: plugins should be able to signal non-canonicity
- _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
+
+setPluginEv :: (EvTerm,Ct) -> TcS ()
+setPluginEv (tm,ct)
+ = case ctEvidence ct of
+ CtWanted (WantedCt { ctev_dest = dest })
+ -> case dest of
+ EvVarDest {} -> setWantedDict dest EvCanonical tm
+ -- TODO: plugins should be able to signal non-canonicity
+ HoleDest {} -> setWantedEq dest emptyRewriterSet (evTermCoercion tm)
+ -- TODO: should we try to track rewriters?
+
+ CtGiven {} -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
-- | A pair of (given, wanted) constraints to pass to plugins
type SplitCts = ([Ct], [Ct])
=====================================
compiler/GHC/Tc/Solver/Solve.hs-boot
=====================================
@@ -1,8 +1,6 @@
module GHC.Tc.Solver.Solve where
-import Prelude( Bool )
import GHC.Tc.Solver.Monad( TcS )
-import GHC.Tc.Types.Constraint( Cts, Implication, WantedConstraints )
+import GHC.Tc.Types.Constraint( Cts, WantedConstraints )
solveSimpleWanteds :: Cts -> TcS WantedConstraints
-trySolveImplication :: Implication -> TcS Bool
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -80,7 +80,8 @@ module GHC.Tc.Types.Constraint (
ctEvExpr, ctEvTerm,
ctEvCoercion, givenCtEvCoercion,
ctEvEvId, wantedCtEvEvId,
- ctEvRewriters, setWantedCtEvRewriters, ctEvUnique, tcEvDestUnique,
+ ctEvRewriters, ctEvRewriterSet, setWantedCtEvRewriters,
+ ctEvUnique, tcEvDestUnique,
ctEvRewriteRole, ctEvRewriteEqRel, setCtEvPredType, setCtEvLoc,
tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
@@ -2291,7 +2292,8 @@ For Givens we make new EvVars and bind them immediately. Two main reasons:
f :: C a b => ....
Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
But that superclass selector can't (yet) appear in a coercion
- (see evTermCoercion), so the easy thing is to bind it to an Id.
+ (see evTermCoercion), so the easy thing is to bind it to a (coercion) Id.
+ This happens in GHC.Tc.Solver.Dict.solveEqualityDict.
So a Given has EvVar inside it rather than (as previously) an EvTerm.
@@ -2393,6 +2395,12 @@ wantedCtHasNoRewriters (WantedCt { ctev_rewriters = rws })
setWantedCtEvRewriters :: WantedCtEvidence -> RewriterSet -> WantedCtEvidence
setWantedCtEvRewriters ev rs = ev { ctev_rewriters = rs }
+ctEvRewriterSet :: CtEvidence -> RewriterSet
+-- Returns the set of holes (empty or singleton) for the evidence itself
+-- Note the difference from ctEvRewriters!
+ctEvRewriterSet (CtWanted (WantedCt { ctev_dest = HoleDest hole })) = unitRewriterSet hole
+ctEvRewriterSet _ = emptyRewriterSet
+
rewriterSetFromCts :: Bag Ct -> RewriterSet
-- Take a bag of Wanted equalities, and collect them as a RewriterSet
rewriterSetFromCts cts
@@ -2404,8 +2412,8 @@ rewriterSetFromCts cts
_ -> rw_set
ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr
-ctEvExpr (CtWanted ev@(WantedCt { ctev_dest = HoleDest _ }))
- = Coercion $ ctEvCoercion (CtWanted ev)
+ctEvExpr (CtWanted (WantedCt { ctev_dest = HoleDest hole }))
+ = Coercion $ mkHoleCo hole
ctEvExpr ev = evId (ctEvEvId ev)
givenCtEvCoercion :: GivenCtEvidence -> TcCoercion
=====================================
testsuite/tests/perf/compiler/T8095.hs
=====================================
@@ -13,7 +13,9 @@ class Class a where
data Data (xs::a) = X | Y
deriving (Read,Show)
main = print test1
-instance (xs ~ Replicate1 ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Zero ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ()) => Class (Data xs) where
+-- instance (xs ~ Replicate1 ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Zero ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ()) => Class (Data xs) where
+instance (xs ~ Replicate1 ( Succ ( Succ ( Succ ( Succ ( Succ (Succ (Succ Zero ))))))) ()) => Class (Data xs) where
f X = Y
f Y = X
-test1 = f (X :: Data ( Replicate1 ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Zero ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) () ))
+test1 = f (X :: Data ( Replicate1 ( Succ ( Succ ( Succ ( Succ (Succ (Succ (Succ Zero))))))) () ))
+-- test1 = f (X :: Data ( Replicate1 ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Succ ( Zero ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) () ))
=====================================
testsuite/tests/perf/compiler/T9872a.hs
=====================================
@@ -140,7 +140,8 @@ type Cube2 = Cube W G B W R R
type Cube3 = Cube G W R B R R
type Cube4 = Cube B R G G W W
-type Cubes = Cons Cube1 (Cons Cube2 (Cons Cube3 (Cons Cube4 Nil)))
+-- type Cubes = Cons Cube1 (Cons Cube2 (Cons Cube3 (Cons Cube4 Nil)))
+type Cubes = Cons Cube1 Nil
type family Compatible c d :: *
type instance Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) =
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/5cf99a788eb64bf7289aa4fa0546a95...
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/5cf99a788eb64bf7289aa4fa0546a95...
You're receiving this email because of your account on gitlab.haskell.org.
