[Git][ghc/ghc][wip/cfuneqcan-refactor] 2 commits: Some small changes, mostly comments.
Richard Eisenberg
gitlab at gitlab.haskell.org
Tue Oct 27 03:23:11 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
4e538977 by Richard Eisenberg at 2020-10-26T21:48:36-04:00
Some small changes, mostly comments.
- - - - -
3cf175e0 by Richard Eisenberg at 2020-10-26T23:22:46-04:00
Fix #18875 by breaking type variable cycles.
- - - - -
11 changed files:
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- testsuite/tests/indexed-types/should_fail/Simple13.hs → testsuite/tests/indexed-types/should_compile/Simple13.hs
- testsuite/tests/indexed-types/should_compile/all.T
- testsuite/tests/indexed-types/should_fail/all.T
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -29,7 +29,7 @@ module GHC.Core.Type (
mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
- mkVisFunTy, mkInvisFunTy,
+ mkFunTy, mkVisFunTy, mkInvisFunTy,
mkVisFunTys,
mkVisFunTyMany, mkInvisFunTyMany,
mkVisFunTysMany, mkInvisFunTysMany,
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1003,9 +1003,11 @@ unify_ty env ty1 (TyVarTy tv2) kco
= uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
unify_ty env ty1 ty2 _kco
+ -- NB: This keeps Constraint and Type distinct, as it should for use in the
+ -- type-checker.
| Just (tc1, tys1) <- mb_tc_app1
, Just (tc2, tys2) <- mb_tc_app2
- , tc1 == tc2 || (tcIsLiftedTypeKind ty1 && tcIsLiftedTypeKind ty2)
+ , tc1 == tc2
= if isInjectiveTyCon tc1 Nominal
then unify_tys env tys1 tys2
else do { let inj | isTypeFamilyTyCon tc1
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2305,12 +2305,18 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
, TyVarLHS lhs_tv <- lhs
, NomEq <- eq_rel
-> do { traceTcS "canEqCanLHSFinish breaking a cycle" (ppr lhs $$ ppr rhs)
- ; new_rhs <- breakTyVarCycle lhs_tv rhs
+ ; new_rhs <- breakTyVarCycle (ctEvLoc ev) rhs
; traceTcS "new RHS:" (ppr new_rhs)
; let new_pred = mkPrimEqPred (mkTyVarTy lhs_tv) new_rhs
new_new_ev = new_ev { ctev_pred = new_pred }
- ; continueWith (CEqCan { cc_ev = new_new_ev, cc_lhs = lhs
- , cc_rhs = new_rhs, cc_eq_rel = eq_rel }) }
+ -- See Detail (6) of Note [Type variable cycles in Givens]
+
+ ; if anyRewritableTyVar True NomEq (\ _ tv -> tv == lhs_tv) new_rhs
+ then do { traceTcS "Note [Type variable cycles in Givens] Detail (1)"
+ (ppr new_new_ev)
+ ; continueWith (mkIrredCt status new_ev) }
+ else continueWith (CEqCan { cc_ev = new_new_ev, cc_lhs = lhs
+ , cc_rhs = new_rhs, cc_eq_rel = eq_rel }) }
-- We must not use it for further rewriting!
| otherwise
@@ -2610,43 +2616,39 @@ Instead, we detect this scenario by the following characteristics:
- a Given CEqCan constraint
- with a tyvar on its LHS
- with a soluble occurs-check failure
+ - and a nominal equality
-Having identified the scenario, we create a fresh untouchable metavariable a'
-(with MetaInfo CycleBreakerTv), and replace all occurrences of `a` in the RHS
-with a'. This is done by breakTyVarCycle. We have now disrupted the
-occurs-check problem and can make the CEqCan.
+Having identified the scenario, we wish to replace all type family
+applications on the RHS with fresh metavariables (with MetaInfo
+CycleBreakerTv). This is done in breakTyVarCycle. These metavariables are
+untouchable, but we also emit Givens relating the fresh variables to the type
+family applications they replace.
-Of course, we don't want a' leaking into e.g. error messages. So we
-restore the cycles by setting a' := a after we're done running the
-solver (in nestImplicTcS and runTcSWithEvBinds). This is done by
-restoreTyVarCycles, which uses the inert_tv_cycles field in InertSet,
-which contains the pairings invented in breakTyVarCycle.
+Of course, we don't want our fresh variables leaking into e.g. error messages.
+So we fill in the metavariables with their original type family applications
+after we're done running the solver (in nestImplicTcS and runTcSWithEvBinds).
+This is done by restoreTyVarCycles, which uses the inert_cycle_breakers field in
+InertSet, which contains the pairings invented in breakTyVarCycle.
-Note that we don't have to think about evidence here, because the
-loop-breaker variable just gets zonked right back to the original
-one. By the time we examine the evidence, all traces of this trick
-are very long gone.
+In our example, we start with
-There are drawbacks of this approach:
+ [G] a ~ Maybe (F a)
- 1. This trick allows us to use a loopy Given once, but not twice.
- And it's possible for twice to be necessary. #18875:
+We then change this to become
- type family G a b where
- G (Maybe c) d = d
+ [G] a ~ Maybe cbv
+ [G] F a ~ cbv
- h :: (e ~ Maybe (G e f)) => e -> f
- h (Just x) = x
+and set cbv := F a after we're done solving.
- In order to accept this, we have to use the Given twice, in order
- for G e f to reduce to show that e ~ Maybe f.
+There are drawbacks of this approach:
- 2. We apply this trick only for Givens, never for Wanted or Derived.
+ 1. We apply this trick only for Givens, never for Wanted or Derived.
It wouldn't make sense for Wanted, because Wanted never rewrite.
But it's conceivable that a Derived would benefit from this all.
I doubt it would ever happen, though, so I'm holding off.
- 3. We don't use this trick for representational equalities, as there
+ 2. We don't use this trick for representational equalities, as there
is no concrete use case where it is helpful (unlike for nominal
equalities). Furthermore, because function applications can be
CanEqLHSs, but newtype applications cannot, the disparities between
@@ -2658,8 +2660,56 @@ There are drawbacks of this approach:
f :: (Coercible a (N a b), Coercible (N a b) b) => a -> b
f = coerce
- failed with "Could not match 'b' with 'b'." Further work is saved
- for when we have a concrete incentive to explore this dark corner.
+ failed with "Could not match 'b' with 'b'." Further work is held off
+ until when we have a concrete incentive to explore this dark corner.
+
+Details:
+
+ (1) We don't look under foralls, at all, when substituting away type family
+ applications, because doing so can never be fruitful. Recall that we
+ are in a case like [G] a ~ forall b. ... a .... Until we have a type
+ family that can pull the body out from a forall, this will always be
+ insoluble. Note also that the forall cannot be in an argument to a
+ type family, or that outer type family application would already have
+ been substituted away.
+
+ However, we still must check to make sure that breakTyVarCycle actually
+ succeeds in getting rid of all occurrences of the offending variable.
+ If one is hidden under a forall, this won't be true. So we perform
+ an additional check after performing the substitution.
+
+ Skipping this check causes typecheck/should_fail/GivenForallLoop to loop.
+
+ (2) Our goal here is to avoid loops in rewriting. We can thus skip looking
+ in coercions, as we don't rewrite in coercions.
+
+ (3) As we're substituting, we can build ill-kinded
+ types. For example, if we have Proxy (F a) b, where (b :: F a), then
+ replacing this with Proxy cbv b is ill-kinded. However, we will later
+ set cbv := F a, and so the zonked type will be well-kinded again.
+ The temporary ill-kinded type hurts no one, and avoiding this would
+ be quite painfully difficult.
+
+ (4) The evidence for the produced Givens is all just reflexive, because
+ we will eventually set the cycle-breaker variable to be the type family,
+ and then, after the zonk, all will be well.
+
+ (5) The approach here is inefficient. For instance, we could choose to
+ affect only type family applications that mention the offending variable.
+ We could try to detect cases like a ~ (F a, F a) and use the same
+ tyvar to replace F a. (Cf. Note [Flattening] in GHC.Core.Unify, which
+ goes to this extra effort.) There may be other opportunities for
+ improvement. However, this is really a very small corner case, always
+ tickled by a user-written Given. The investment to craft a clever,
+ performant solution seems unworthwhile.
+
+ (6) We often get the predicate associated with a constraint from its
+ evidence. We thus must not only make sure the generated CEqCan's
+ fields have the updated RHS type, but we must also update the
+ evidence itself. As in Detail (4), we don't need to change the
+ evidence term (as in e.g. rewriteEqEvidence) because the cycle
+ breaker variables are all zonked away by the time we examine the
+ evidence.
-}
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -559,6 +559,10 @@ flatten_one :: TcType -> FlatM (Xi, Coercion)
-- Postcondition: Coercion :: Xi ~ TcType
-- The role on the result coercion matches the EqRel in the FlattenEnv
+flatten_one ty
+ | Just ty' <- flattenView ty -- See Note [Flattening synonyms]
+ = flatten_one ty'
+
flatten_one xi@(LitTy {})
= do { role <- getRole
; return (xi, mkReflCo role xi) }
@@ -569,16 +573,8 @@ flatten_one (TyVarTy tv)
flatten_one (AppTy ty1 ty2)
= flatten_app_tys ty1 [ty2]
-flatten_one ty@(TyConApp tc tys)
- -- Expand type synonyms that mention type families
- -- on the RHS; see Note [Flattening synonyms]
- | isForgetfulSynTyCon tc || not (isFamFreeTyCon tc)
- , Just expanded_ty <- tcView ty
- = flatten_one expanded_ty
-
- -- Otherwise, it's a type function application, and we have to
- -- flatten it away as well, and generate a new given equality constraint
- -- between the application and a newly generated flattening skolem variable.
+flatten_one (TyConApp tc tys)
+ -- If it's a type family application, try to reduce it
| isTypeFamilyTyCon tc
= flatten_fam_app tc tys
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -123,7 +123,7 @@ module GHC.Tc.Solver.Monad (
-- if the whole instance matcher simply belongs
-- here
- breakTyVarCycle
+ breakTyVarCycle, flattenView
) where
#include "HsVersions.h"
@@ -146,6 +146,7 @@ import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDict
import GHC.Tc.Utils.TcType
import GHC.Driver.Session
import GHC.Core.Type
+import qualified GHC.Core.TyCo.Rep as Rep -- this needs to be used only very locally
import GHC.Core.Coercion
import GHC.Core.Unify
@@ -392,8 +393,8 @@ data InertSet
-- Canonical Given, Wanted, Derived
-- Sometimes called "the inert set"
- , inert_tv_cycles :: [(TcTyVar, TcTyVar)]
- -- a list of CycleBreakerTv / original tv pairs (in that order)
+ , inert_cycle_breakers :: [(TcTyVar, TcType)]
+ -- a list of CycleBreakerTv / original family applications
-- used to undo the cycle-breaking needed to handle
-- Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
@@ -434,10 +435,10 @@ emptyInertCans
emptyInert :: InertSet
emptyInert
- = IS { inert_cans = emptyInertCans
- , inert_tv_cycles = []
- , inert_flat_cache = emptyFunEqs
- , inert_solved_dicts = emptyDictMap }
+ = IS { inert_cans = emptyInertCans
+ , inert_cycle_breakers = []
+ , inert_flat_cache = emptyFunEqs
+ , inert_solved_dicts = emptyDictMap }
{- Note [Solved dictionaries]
@@ -1397,7 +1398,7 @@ addTyEq old_eqs tv ct
addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct
-> FunEqMap EqualCtList
addCanFunEq old_eqs fun_tc fun_args ct
- = alterTcApp old_eqs (getUnique fun_tc) fun_args upd
+ = alterTcApp old_eqs fun_tc fun_args upd
where
upd (Just old_equal_ct_list) = Just $ addToEqualCtList ct old_equal_ct_list
upd Nothing = Just $ [ct]
@@ -1419,14 +1420,10 @@ findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
delEq ic lhs rhs = case lhs of
- TyVarLHS tv -> ic { inert_eqs = modifyDVarEnv
- (filter (not . isThisOne))
- (inert_eqs ic) tv }
- TyFamLHS tf args -> ic { inert_funeqs = alterTcApp
- (inert_funeqs ic)
- (getUnique tf)
- args
- upd }
+ TyVarLHS tv
+ -> ic { inert_eqs = modifyDVarEnv (filter (not . isThisOne)) (inert_eqs ic) tv }
+ TyFamLHS tf args
+ -> ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
where
upd (Just eq_ct_list)
| null filtered = Nothing
@@ -1508,11 +1505,11 @@ When adding an equality to the inerts:
kickOutRewritable with Nominal, Given. See kickOutAfterUnification.
-}
-addInertCan :: Ct -> TcS () -- Constraints *other than* equalities
+addInertCan :: Ct -> TcS ()
-- Precondition: item /is/ canonical
-- See Note [Adding an equality to the InertCans]
addInertCan ct
- = do { traceTcS "insertInertCan {" $
+ = do { traceTcS "addInertCan {" $
text "Trying to insert new inert item:" <+> ppr ct
; ics <- getInertCans
@@ -1702,7 +1699,7 @@ kick_out_rewritable new_fr new_lhs
extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList
-> FunEqMap EqualCtList
extend_fun_eqs eqs (TyFamLHS fam_tc fam_args) cts
- = insertTcApp eqs (getUnique fam_tc) fam_args cts
+ = insertTcApp eqs fam_tc fam_args cts
extend_fun_eqs eqs other _cts = pprPanic "extend_fun_eqs" (ppr eqs $$ ppr other)
kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container)
@@ -2338,7 +2335,7 @@ not match the requested info exactly!
-}
-type TcAppMap a = UniqDFM Unique (ListMap LooseTypeMap a)
+type TcAppMap a = UniqDFM TyCon (ListMap LooseTypeMap a)
-- Indexed by tycon then the arg types, using "loose" matching, where
-- we don't require kind equality. This allows, for example, (a |> co)
-- to match (a).
@@ -2352,27 +2349,24 @@ isEmptyTcAppMap m = isNullUDFM m
emptyTcAppMap :: TcAppMap a
emptyTcAppMap = emptyUDFM
-findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
-findTcApp m u tys = do { tys_map <- lookupUDFM m u
- ; lookupTM tys tys_map }
+findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a
+findTcApp m tc tys = do { tys_map <- lookupUDFM m tc
+ ; lookupTM tys tys_map }
-delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
-delTcApp m cls tys = adjustUDFM (deleteTM tys) m cls
+delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a
+delTcApp m tc tys = adjustUDFM (deleteTM tys) m tc
-insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
-insertTcApp m cls tys ct = alterUDFM alter_tm m cls
+insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
+insertTcApp m tc tys ct = alterUDFM alter_tm m tc
where
alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
-alterTcApp :: forall a. TcAppMap a -> Unique -> [Type] -> (Maybe a -> Maybe a) -> TcAppMap a
-alterTcApp m cls tys upd = alterUDFM alter_tm m cls
+alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> (Maybe a -> Maybe a) -> TcAppMap a
+alterTcApp m tc tys upd = alterUDFM alter_tm m tc
where
alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm m_elt = Just (alterTM tys upd (m_elt `orElse` emptyTM))
--- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
--- mapTcApp f = mapUDFM (mapTM f)
-
filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
filterTcAppMap f m
= mapUDFM do_tm m
@@ -2457,7 +2451,7 @@ findDict m loc cls tys
= Nothing -- See Note [Solving CallStack constraints]
| otherwise
- = findTcApp m (getUnique cls) tys
+ = findTcApp m (classTyCon cls) tys
findDictsByClass :: DictMap a -> Class -> Bag a
findDictsByClass m cls
@@ -2465,10 +2459,10 @@ findDictsByClass m cls
| otherwise = emptyBag
delDict :: DictMap a -> Class -> [Type] -> DictMap a
-delDict m cls tys = delTcApp m (getUnique cls) tys
+delDict m cls tys = delTcApp m (classTyCon cls) tys
addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
-addDict m cls tys item = insertTcApp m (getUnique cls) tys item
+addDict m cls tys item = insertTcApp m (classTyCon cls) tys item
addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
addDictsByClass m cls items
@@ -2511,7 +2505,7 @@ emptyFunEqs :: TcAppMap a
emptyFunEqs = emptyTcAppMap
findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
-findFunEq m tc tys = findTcApp m (getUnique tc) tys
+findFunEq m tc tys = findTcApp m tc tys
findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
-- Get inert function equation constraints that have the given tycon
@@ -2519,8 +2513,8 @@ findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
-- We use this to check for derived interactions with built-in type-function
-- constructors.
findFunEqsByTyCon m tc
- | Just tm <- lookupUDFM m (getUnique tc) = foldTM (:) tm []
- | otherwise = []
+ | Just tm <- lookupUDFM m tc = foldTM (:) tm []
+ | otherwise = []
foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs = foldTcAppMap
@@ -2535,7 +2529,7 @@ anyFunEqMap m test = foldFunEqs (\ a b -> b || test a) m False
-- filterFunEqs = filterTcAppMap
insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
-insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
+insertFunEq m tc tys val = insertTcApp m tc tys val
{-
************************************************************************
@@ -3435,24 +3429,61 @@ See GHC.Tc.Solver.Monad.deferTcSForAllEq
************************************************************************
-}
--- | Replace all occurrences of the LHS tyvar in an RHS with a fresh
--- variable, recording the pairing in the TcS monad.
+-- | Replace all type family applications in the RHS with fresh variables,
+-- emitting givens that relate the type family application to the variable.
-- See Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
-breakTyVarCycle :: TyVar -- the LHS tyvar
+breakTyVarCycle :: CtLoc
-> TcType -- the RHS
- -> TcS TcType -- new RHS that doesn't mention TyVar
-breakTyVarCycle lhs_tv rhs
- = do { new_tv <- wrapTcS (TcM.newCycleBreakerTyVar lhs_tv)
- ; updInertTcS $ \is ->
- is { inert_tv_cycles = (new_tv, lhs_tv) : inert_tv_cycles is }
- ; let in_scope = mkInScopeSet (tyCoVarsOfType rhs)
- subst0 = mkEmptyTCvSubst in_scope
- subst = extendTvSubstWithClone subst0 lhs_tv new_tv
- ; return (substTy subst rhs) }
+ -> TcS TcType -- new RHS that doesn't have any type families
+-- This could be considerably more efficient. See Detail (5) of Note.
+breakTyVarCycle loc = go
+ where
+ go ty | Just ty' <- flattenView ty = go ty'
+ go (Rep.TyConApp tc tys)
+ | isTypeFamilyTyCon tc
+ = do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
+ fun_app = mkTyConApp tc fun_args
+ fun_app_kind = tcTypeKind fun_app
+ ; new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind)
+ ; let new_ty = mkTyVarTy new_tv
+ given_pred = mkHeteroPrimEqPred fun_app_kind fun_app_kind
+ fun_app new_ty
+ given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note
+ ; new_given <- newGivenEvVar loc (given_pred, given_term)
+ ; traceTcS "breakTyVarCycle replacing type family" (ppr new_given)
+ ; emitWorkNC [new_given]
+ ; updInertTcS $ \is ->
+ is { inert_cycle_breakers = (new_tv, fun_app) :
+ inert_cycle_breakers is }
+ ; extra_args' <- mapM go extra_args
+ ; return (mkAppTys new_ty extra_args') }
+ -- Worried that this substitution will change kinds?
+ -- See Detail (3) of Note
+
+ | otherwise
+ = mkTyConApp tc <$> mapM go tys
+
+ go (Rep.AppTy ty1 ty2) = mkAppTy <$> go ty1 <*> go ty2
+ go (Rep.FunTy vis w arg res) = mkFunTy vis <$> go w <*> go arg <*> go res
+ go (Rep.CastTy ty co) = mkCastTy <$> go ty <*> pure co
+
+ go ty@(Rep.TyVarTy {}) = return ty
+ go ty@(Rep.LitTy {}) = return ty
+ go ty@(Rep.ForAllTy {}) = return ty -- See Detail (1) of Note
+ go ty@(Rep.CoercionTy {}) = return ty -- See Detail (2) of Note
-- | Filli in CycleBreakerTvs with the variables they stand for.
-- See Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles is
- = forM_ (inert_tv_cycles is) $ \ (cycle_breaker_tv, orig_tv) ->
- TcM.writeMetaTyVar cycle_breaker_tv (mkTyVarTy orig_tv)
+ = forM_ (inert_cycle_breakers is) $ \ (cycle_breaker_tv, orig_ty) ->
+ TcM.writeMetaTyVar cycle_breaker_tv orig_ty
+
+-- Unwrap a type synonym only when either:
+-- The type synonym is forgetful, or
+-- the type synonym mentions a type family in its expansion
+flattenView :: TcType -> Maybe TcType
+flattenView ty@(Rep.TyConApp tc _)
+ | isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
+ = tcView ty
+flattenView _other = Nothing
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -150,7 +150,7 @@ data Ct
-- a ~ [a] occurs check
}
- | CEqCan { -- tv ~ rhs
+ | CEqCan { -- CanEqLHS ~ rhs
-- Invariants:
-- * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.Monad
-- * Many are checked in checkTypeEq in GHC.Tc.Utils.Unify
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -871,11 +871,11 @@ cloneAnonMetaTyVar info tv kind
-- Make a new CycleBreakerTv. See Note [Type variable cycles in Givens]
-- in GHC.Tc.Solver.Canonical.
-newCycleBreakerTyVar :: TyVar -> TcM TcTyVar
-newCycleBreakerTyVar old_tv
+newCycleBreakerTyVar :: TcKind -> TcM TcTyVar
+newCycleBreakerTyVar kind
= do { details <- newMetaDetails CycleBreakerTv
- ; name <- cloneMetaTyVarName (tyVarName old_tv)
- ; return (mkTcTyVar name (tyVarKind old_tv) details) }
+ ; name <- newMetaTyVarName (fsLit "cbv")
+ ; return (mkTcTyVar name kind details) }
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
=====================================
testsuite/tests/indexed-types/should_fail/Simple13.hs → testsuite/tests/indexed-types/should_compile/Simple13.hs
=====================================
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -10,6 +10,7 @@ test('Simple9', normal, compile, [''])
test('Simple10', normal, compile, [''])
test('Simple11', normal, compile, [''])
test('Simple12', normal, compile, [''])
+test('Simple13', normal, compile, [''])
test('Simple14', normal, compile_fail, [''])
test('Simple15', normal, compile, [''])
test('Simple16', normal, compile, [''])
@@ -297,3 +298,4 @@ test('T17923', normal, compile, [''])
test('T18065', normal, compile, ['-O'])
test('CEqCanOccursCheck', normal, compile, [''])
test('GivenLoop', normal, compile, [''])
+test('T18875', normal, compile, [''])
=====================================
testsuite/tests/indexed-types/should_fail/all.T
=====================================
@@ -163,4 +163,3 @@ test('T17008a', normal, compile_fail, ['-fprint-explicit-kinds'])
test('T13571', normal, compile_fail, [''])
test('T13571a', normal, compile_fail, [''])
test('T18648', normal, compile_fail, [''])
-test('Simple13', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -584,3 +584,4 @@ test('too-many', normal, compile_fail, [''])
test('T18640a', normal, compile_fail, [''])
test('T18640b', normal, compile_fail, [''])
test('T18640c', normal, compile_fail, [''])
+test('GivenForallLoop', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/cdc73a4c3e789c7725e594b7582896301d77f8c7...3cf175e03363960bc603572eaaffbf13c559f0c5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/cdc73a4c3e789c7725e594b7582896301d77f8c7...3cf175e03363960bc603572eaaffbf13c559f0c5
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201026/dceb47f2/attachment-0001.html>
More information about the ghc-commits
mailing list