[Git][ghc/ghc][wip/T23162-spj] 2 commits: Tidy up trySolveImplication
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 <simon.peytonjones@gmail.com> 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.
participants (1)
-
Simon Peyton Jones (＠simonpj)