[Git][ghc/ghc][wip/T17656] Wibbles
Simon Peyton Jones
gitlab at gitlab.haskell.org
Wed Dec 9 23:36:18 UTC 2020
Simon Peyton Jones pushed to branch wip/T17656 at Glasgow Haskell Compiler / GHC
Commits:
d1ff4302 by Simon Peyton Jones at 2020-12-09T23:35:41+00:00
Wibbles
- - - - -
6 changed files:
- compiler/GHC/Runtime/Heap/Inspect.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Runtime/Heap/Inspect.hs
=====================================
@@ -577,7 +577,7 @@ newOpenVar = liftTcM (do { kind <- newOpenTypeKind
~~~~~~~~~~~~~~~~~~~~~~
In the GHCi debugger we use unification variables whose MetaInfo is
RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can
-unify with a polytype (see GHC.Tc.Utils.Unify.metaTyVarUpdateOK).
+unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq).
If we don't do this `:print <term>` will fail if the type of <term>
has nested `forall`s or `=>`s.
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -907,7 +907,7 @@ That is the entire point of qlUnify! Wrinkles:
* We must not make an occurs-check; we use occCheckExpand for that.
-* metaTyVarUpdateOK also checks for various other things, including
+* checkTypeEq also checks for various other things, including
- foralls, and predicate types (which we want to allow here)
- type families (relates to a very specific and exotic performance
question, that is unlikely to bite here)
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1674,11 +1674,11 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }
-- Any insoluble constraints are in 'simples' and so get rewritten
-- See Note [Rewrite insolubles] in GHC.Tc.Solver.Monad
- ; (_floated_eqs, implics2) <- solveNestedImplications $
- implics `unionBags` wc_impl wc1
+ ; implics2 <- solveNestedImplications $
+ implics `unionBags` wc_impl wc1
; dflags <- getDynFlags
- ; unif_happened <- getUnificationFlag
+ ; unif_happened <- resetUnificationFlag
; solved_wc <- simpl_loop 0 (solverIterations dflags) unif_happened
(wc1 { wc_impl = implics2 })
@@ -1704,17 +1704,12 @@ simpl_loop n limit unif_happened wc@(WC { wc_simple = simples })
addErrTcS (hang (text "solveWanteds: too many iterations"
<+> parens (text "limit =" <+> ppr limit))
2 (vcat [ text "Unsolved:" <+> ppr wc
--- , ppUnless (isEmptyBag floated_eqs) $
--- text "Floated equalities:" <+> ppr floated_eqs
, text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
]))
; return wc }
| unif_happened
= simplify_again n limit True wc
- -- Put floated_eqs first so they get solved first
- -- NB: the floated_eqs may include /derived/ equalities
- -- arising from fundeps inside an implication
| superClassesMightHelp wc
= -- We still have unsolved goals, and apparently no way to solve them,
@@ -1747,55 +1742,33 @@ simplify_again n limit no_new_given_scs
; wc1 <- solveSimpleWanteds simples
- ; (_floated_eqs2, implics2) <- solveNestedImplications $
- implics `unionBags` (wc_impl wc1)
- ; unif_happened <- getUnificationFlag
- ; simpl_loop (n+1) limit unif_happened (wc1 { wc_impl = implics2 })
+ ; implics2 <- solveNestedImplications $
+ implics `unionBags` (wc_impl wc1)
-{-
- -- See Note [Cutting off simpl_loop]
- -- We have already tried to solve the nested implications once
- -- Try again only if we have unified some meta-variables
- -- (which is a bit like adding more givens), or we have some
- -- new Given superclasses
- ; let new_implics = wc_impl wc1
- ; if no_new_given_scs &&
- isEmptyBag new_implics
-
- then -- Do not even try to solve the implications
- simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
-
- else -- Try to solve the implications
- do { (floated_eqs2, implics2) <- solveNestedImplications $
- implics `unionBags` new_implics
- ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 }) }
--}
- }
+ ; unif_happened <- resetUnificationFlag
+ ; simpl_loop (n+1) limit unif_happened (wc1 { wc_impl = implics2 }) }
solveNestedImplications :: Bag Implication
- -> TcS (Cts, Bag Implication)
+ -> TcS (Bag Implication)
-- Precondition: the TcS inerts may contain unsolved simples which have
-- to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
| isEmptyBag implics
- = return (emptyBag, emptyBag)
+ = return (emptyBag)
| otherwise
= do { traceTcS "solveNestedImplications starting {" empty
- ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
- ; let floated_eqs = concatBag floated_eqs_s
+ ; unsolved_implics <- mapBagM solveImplication implics
-- ... and we are back in the original TcS inerts
-- Notice that the original includes the _insoluble_simples so it was safe to ignore
-- them in the beginning of this function.
; traceTcS "solveNestedImplications end }" $
- vcat [ text "all floated_eqs =" <+> ppr floated_eqs
- , text "unsolved_implics =" <+> ppr unsolved_implics ]
+ vcat [ text "unsolved_implics =" <+> ppr unsolved_implics ]
- ; return (floated_eqs, catBagMaybes unsolved_implics) }
+ ; return (catBagMaybes unsolved_implics) }
solveImplication :: Implication -- Wanted
- -> TcS (Cts, -- All wanted or derived floated equalities: var = type
- Maybe Implication) -- Simplified implication (empty or singleton)
+ -> TcS (Maybe Implication) -- Simplified implication (empty or singleton)
-- Precondition: The TcS monad contains an empty worklist and given-only inerts
-- which after trying to solve this implication we must restore to their original value
solveImplication imp@(Implic { ic_tclvl = tclvl
@@ -1806,7 +1779,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
, ic_info = info
, ic_status = status })
| isSolvedStatus status
- = return (emptyCts, Just imp) -- Do nothing
+ = return (Just imp) -- Do nothing
| otherwise -- Even for IC_Insoluble it is worth doing more work
-- The insoluble stuff might be in one sub-implication
@@ -1828,7 +1801,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
; residual_wanted <- solveWanteds wanteds
-- solveWanteds, *not* solveWantedsAndDrop, because
-- we want to retain derived equalities so we can float
- -- them out in floatEqualities
+ -- them out in floatEqualities.
; (has_eqs, given_insols) <- getHasGivenEqs tclvl
-- Call getHasGivenEqs /after/ solveWanteds, because
@@ -1837,10 +1810,6 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
; return (has_eqs, given_insols, residual_wanted) }
- ; (floated_eqs, residual_wanted)
- <- floatEqualities skols given_ids ev_binds_var
- has_given_eqs residual_wanted
-
; traceTcS "solveImplication 2"
(ppr given_insols $$ ppr residual_wanted)
; let final_wanted = residual_wanted `addInsols` given_insols
@@ -1854,12 +1823,11 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
; traceTcS "solveImplication end }" $ vcat
[ text "has_given_eqs =" <+> ppr has_given_eqs
- , text "floated_eqs =" <+> ppr floated_eqs
, text "res_implic =" <+> ppr res_implic
, text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
, text "implication tvcs =" <+> ppr tcvs ]
- ; return (floated_eqs, res_implic) }
+ ; return res_implic }
-- TcLevels must be strictly increasing (see (ImplicInv) in
-- Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType),
@@ -2532,6 +2500,7 @@ no evidence for a fundep equality), but equality superclasses do matter (since
they carry evidence).
-}
+{-
floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> HasGivenEqs
-> WantedConstraints
-> TcS (Cts, WantedConstraints)
@@ -2553,7 +2522,6 @@ floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> HasGivenEqs
floatEqualities _ _ _ _ wanteds
= return (emptyBag, wanteds)
-{-
floatEqualities skols given_ids ev_binds_var has_given_eqs
wanteds@(WC { wc_simple = simples })
| MaybeGivenEqs <- has_given_eqs -- There are some given equalities, so don't float
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2270,8 +2270,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
-- This function handles the case where one side is a tyvar and the other is
-- a type family application. Which to put on the left?
--- If the tyvar is a meta-tyvar, put it on the left, as this may be our only
--- shot to unify.
+-- If the tyvar is a touchable meta-tyvar, put it on the left, as this may
+-- be our only shot to unify.
-- Otherwise, put the function on the left, because it's generally better to
-- rewrite away function calls. This makes types smaller. And it seems necessary:
-- [W] F alpha ~ alpha
@@ -2279,8 +2279,6 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
-- [W] G alpha beta ~ Int ( where we have type instance G a a = a )
-- If we end up with a stuck alpha ~ F alpha, we won't be able to solve this.
-- Test case: indexed-types/should_compile/CEqCanOccursCheck
--- It would probably work to always put the variable on the left, but we think
--- it would be less efficient.
canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco)
-- or (rhs |> mco) ~ lhs if swapped
-> EqRel -> SwapFlag
@@ -2342,7 +2340,11 @@ unifyTest ev tv1 rhs
does_not_escape tv_lvl fv
| isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv
- | otherwise = True -- Coercion variables
+ | otherwise = True
+ -- Coercion variables are not an escape risk
+ -- If an implication binds a coercion variable, it'll have equalities,
+ -- so the "intervening given equalities" test above will catch it
+ -- Coercion holes get filled with coercions, so again no problem.
is_promotable fv
| isTyVar fv
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -31,7 +31,7 @@ module GHC.Tc.Solver.Monad (
panicTcS, traceTcS,
traceFireTcS, bumpStepCountTcS, csTraceTcS,
wrapErrTcS, wrapWarnTcS,
- getUnificationFlag, setUnificationFlag,
+ resetUnificationFlag, setUnificationFlag,
-- Evidence creation and transformation
MaybeNew(..), freshGoals, isFresh, getEvExpr,
@@ -1512,12 +1512,24 @@ addInertForAll new_qci
= do { ics <- getInertCans
; ics1 <- add_qci ics
- -- C.f add_given_eq
+ -- Update given equalities. Painful! C.f updateGivenEqs
; tclvl <- getTcLevel
- ; let ics2 | tclvl `strictlyDeeperThan` inert_given_eq_lvl ics1
- = ics1 { inert_given_eq_lvl = tclvl }
- | otherwise
- = ics1
+ ; let ics2 | not_equality = ics1
+ | otherwise = ics1 { inert_given_eq_lvl = ge_lvl'
+ , inert_given_eqs = geqs' }
+ !(IC { inert_given_eq_lvl = ge_lvl
+ , inert_given_eqs = geqs }) = ics1
+
+ not_equality = isClassPred pred && not (isEqPred pred)
+ -- True <=> definitely not an equality
+ -- Heads like (f a) might be an equality
+
+ pred = qci_pred new_qci
+ is_eq_pred = isEqPred pred -- Definitely an equality
+ geqs' = geqs || is_eq_pred
+
+ ge_lvl' | tclvl `strictlyDeeperThan` ge_lvl = tclvl
+ | otherwise = ge_lvl
; setInertCans ics2 }
where
@@ -1602,13 +1614,13 @@ add_item :: TcLevel -> InertCans -> Ct -> InertCans
add_item tc_lvl
ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs })
item@(CEqCan { cc_lhs = lhs })
- = add_given_eq tc_lvl item $
+ = updateGivenEqs tc_lvl item $
case lhs of
TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item }
TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv item }
add_item tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {})
- = add_given_eq tc_lvl item $ -- An Irred might turn out to be an
+ = updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an
-- equality, so we play safe
ics { inert_irreds = irreds `Bag.snocBag` item }
@@ -1619,15 +1631,15 @@ add_item _ _ item
= pprPanic "upd_inert set: can't happen! Inserting " $
ppr item -- Can't be CNonCanonical because they only land in inert_irreds
-add_given_eq :: TcLevel -> Ct -> InertCans -> InertCans
+updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
-- Set the inert_given_eq_level to the current level (tclvl)
-- if the constraint is a given equality that should prevent
-- filling in an outer unification variable.
-- See See Note [When does an implication have given equalities?]
--
-- ToDo: what about Quantified Constraints?
-add_given_eq tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl
- , inert_given_eqs = geqs })
+updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl
+ , inert_given_eqs = geqs })
| not (isGivenCt ct) = inerts
| not_equality ct = inerts -- See Note [Let-bound skolems]
| otherwise = inerts { inert_given_eq_lvl = ge_lvl'
@@ -1651,7 +1663,9 @@ add_given_eq tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl
not_equality :: Ct -> Bool
-- True <=> definitely not an equality of any kind
- not_equality (CEqCan { cc_lhs = TyVarLHS tv }) = isLocalSkolem tclvl tv
+ -- except for a let-bound skolem, which doesn't count
+ -- See Note [Let-bound skolems]
+ not_equality (CEqCan { cc_lhs = TyVarLHS tv }) = not (isOuterTyVar tclvl tv)
not_equality (CDictCan {}) = True
not_equality _ = False
@@ -2184,81 +2198,38 @@ getHasGivenEqs :: TcLevel -- TcLevel of this implication
, Cts ) -- Insoluble equalities arising from givens
-- See Note [When does an implication have given equalities?]
getHasGivenEqs tclvl
- = do { inerts@(IC { inert_irreds = irreds
--- , inert_insts = qc_insts
--- , inert_eqs = ieqs, inert_funeqs = funeqs
- , inert_given_eqs = given_eqs
+ = do { inerts@(IC { inert_irreds = irreds
+ , inert_given_eqs = given_eqs
, inert_given_eq_lvl = ge_lvl })
<- getInertCans
-{-
- ; let has_given_eqs = foldMap check_local_given_ct irreds
- S.<> foldMap (lift_equal_ct_list check_local_given_tv_eq) ieqs
- S.<> foldMapFunEqs (lift_equal_ct_list check_local_given_ct) funeqs
- S.<> foldMap qc_eq_inst_given_here qc_insts
--}
; let insols = filterBag insolubleEqCt irreds
- -- Specifically includes ones that originated in some
+ -- Specifically includes ones that originated in some
-- outer context but were refined to an insoluble by
-- a local equality; so do /not/ add ct_given_here.
+ has_ge | given_eqs = LocalGivenEqs
+ | ge_lvl == tclvl = MaybeGivenEqs
+ | otherwise = NoGivenEqs
+
; traceTcS "getHasGivenEqs" $
vcat [ text "given_eqs:" <+> ppr given_eqs
, text "ge_lvl:" <+> ppr ge_lvl
, text "ambient level:" <+> ppr tclvl
, text "Inerts:" <+> ppr inerts
, text "Insols:" <+> ppr insols]
- ; let has_ge | given_eqs = LocalGivenEqs
--- | ge_lvl == tclvl = MaybeGivenEqs
- | otherwise = NoGivenEqs
; return (has_ge, insols) }
- where
-{-
- check_local_given_ct :: Ct -> HasGivenEqs
- check_local_given_ct ct = check_local_given_ev (ctEvidence ct)
-
- check_local_given_ev :: CtEvidence -> HasGivenEqs
- check_local_given_ev ev
- | not (given_bound_here ev) = NoGivenEqs
- | mentionsOuterVar tclvl ev = MaybeGivenEqs
- | otherwise = LocalGivenEqs
-
- lift_equal_ct_list :: (Ct -> HasGivenEqs) -> EqualCtList -> HasGivenEqs
- -- returns NoGivenEqs for non-singleton lists, as Given lists are always
- -- singletons
- lift_equal_ct_list check (EqualCtList (ct :| [])) = check ct
- lift_equal_ct_list _ _ = NoGivenEqs
-
- check_local_given_tv_eq :: Ct -> HasGivenEqs
- check_local_given_tv_eq (CEqCan { cc_lhs = TyVarLHS tv, cc_ev = ev})
- | not (given_bound_here ev) = NoGivenEqs
- | not (isLocalSkolem tclvl tv) = MaybeGivenEqs
- | otherwise = NoGivenEqs -- See Note [Let-bound skolems]
- check_local_given_tv_eq other_ct
- = check_local_given_ct other_ct
-
- qc_eq_inst_given_here :: QCInst -> HasGivenEqs
- -- True of a quantified constraint (which are always Given)
- -- for an equality, bound by this implication
- qc_eq_inst_given_here (QCI { qci_ev = ev, qci_pred = pred })
- | isEqPred pred = check_local_given_ev ev
- | otherwise = NoGivenEqs
-
- given_bound_here :: CtEvidence -> Bool
- -- True for a Given bound by the current implication,
- -- i.e. the current level
- given_bound_here ev = isGiven ev
- && tclvl == ctLocLevel (ctEvLoc ev)
--}
mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar tclvl ev
- = anyFreeVarsOfType (not . isLocalSkolem tclvl) $
+ = anyFreeVarsOfType (isOuterTyVar tclvl) $
ctEvPred ev
-isLocalSkolem :: TcLevel -> TyCoVar -> Bool
-isLocalSkolem tclvl tv
- | isTyVar tv = tclvl `sameDepthAs` tcTyVarLevel tv
- -- Includes CycleBreakerTvs which are meta-tyvars
- | otherwise = True -- Coercion variables; doesn't much matter
+isOuterTyVar :: TcLevel -> TyCoVar -> Bool
+-- True of a type variable that comes from a
+-- shallower level than the ambient level (tclvl)
+isOuterTyVar tclvl tv
+ | isTyVar tv = tclvl `strictlyDeeperThan` tcTyVarLevel tv
+ -- Includes CycleBreakerTvs which are meta-tyvars
+ | otherwise = False -- Coercion variables; doesn't much matter
-- | Returns Given constraints that might,
-- potentially, match the given pred. This is used when checking to see if a
@@ -2926,16 +2897,16 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
; n <- TcM.readTcRef ref
; TcM.writeTcRef ref (n+1) }
-getUnificationFlag :: TcS Bool
+resetUnificationFlag :: TcS Bool
-- We are at ambient level i
--- If the unification flag = Just i, set it to Nothing and return True
--- Otherwise return False
-getUnificationFlag
+-- If the unification flag = Just i, reset it to Nothing and return True
+-- Otherwise leave it unchanged and return False
+resetUnificationFlag
= TcS $ \env ->
do { let ref = tcs_unif_lvl env
; ambient_lvl <- TcM.getTcLevel
; mb_lvl <- TcM.readTcRef ref
- ; TcM.traceTc "getUnificationFlag" $
+ ; TcM.traceTc "resetUnificationFlag" $
vcat [ text "ambient:" <+> ppr ambient_lvl
, text "unif_lvl:" <+> ppr mb_lvl ]
; case mb_lvl of
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -37,7 +37,7 @@ module GHC.Tc.Utils.Unify (
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
- metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..),
+ occCheckForErrors, MetaTyVarUpdateResult(..),
checkTyVarEq, checkTyFamEq, checkTypeEq, AreTypeFamiliesOK(..)
) where
@@ -1435,9 +1435,9 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
go dflags cur_lvl
| isTouchableMetaTyVar cur_lvl tv1
, canSolveByUnification (metaTyVarInfo tv1) ty2
- , MTVU_OK ty2' <- metaTyVarUpdateOK dflags NoTypeFamilies tv1 ty2
+ , MTVU_OK {} <- checkTyVarEq dflags NoTypeFamilies tv1 ty2
-- See Note [Prevent unification with type families] about the NoTypeFamilies:
- = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
+ = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1)
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
, ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2)
@@ -1447,8 +1447,8 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
-- Only proceed if the kinds match
-- NB: tv1 should still be unfilled, despite the kind unification
-- because tv1 is not free in ty2 (or, hence, in its kind)
- then do { writeMetaTyVar tv1 ty2'
- ; return (mkTcNomReflCo ty2') }
+ then do { writeMetaTyVar tv1 ty2
+ ; return (mkTcNomReflCo ty2) }
else defer } -- This cannot be solved now. See GHC.Tc.Solver.Canonical
-- Note [Equalities with incompatible kinds]
@@ -1912,73 +1912,6 @@ instance Outputable AreTypeFamiliesOK where
ppr YesTypeFamilies = text "YesTypeFamilies"
ppr NoTypeFamilies = text "NoTypeFamilies"
-metaTyVarUpdateOK :: DynFlags
- -> AreTypeFamiliesOK -- allow type families in RHS?
- -> TcTyVar -- tv :: k1
- -> TcType -- ty :: k2
- -> MetaTyVarUpdateResult TcType -- possibly-expanded ty
--- (metaTyVarUpdateOK tv ty)
--- Checks that the equality tv~ty is OK to be used to rewrite
--- other equalities. Equivalently, checks the conditions for CEqCan
--- (a) that tv doesn't occur in ty (occurs check)
--- (b) that ty does not have any foralls or (perhaps) type functions
--- (c) that ty does not have any blocking coercion holes
--- See Note [Equalities with incompatible kinds] in "GHC.Tc.Solver.Canonical"
---
--- Used in two places:
--- - In the eager unifier: uUnfilledVar2
--- - In the canonicaliser: GHC.Tc.Solver.Canonical.canEqTyVar2
--- Note that in the latter case tv is not necessarily a meta-tyvar,
--- despite the name of this function.
-
--- We have two possible outcomes:
--- (1) Return the type to update the type variable with,
--- [we know the update is ok]
--- (2) Return Nothing,
--- [the update might be dodgy]
---
--- Note that "Nothing" does not mean "definite error". For example
--- type family F a
--- type instance F Int = Int
--- consider
--- a ~ F a
--- This is perfectly reasonable, if we later get a ~ Int. For now, though,
--- we return Nothing, leaving it to the later constraint simplifier to
--- sort matters out.
---
--- See Note [Refactoring hazard: metaTyVarUpdateOK]
-
-metaTyVarUpdateOK dflags ty_fam_ok tv rhs_ty
- = case checkTyVarEq dflags ty_fam_ok tv rhs_ty of
- _ | bad_tyvar_tv -> MTVU_Bad
- MTVU_OK _ -> MTVU_OK rhs_ty
- MTVU_Bad -> MTVU_Bad -- forall, predicate, type function
- MTVU_HoleBlocker -> MTVU_HoleBlocker -- coercion hole
- MTVU_Occurs -> case occCheckExpand [tv] rhs_ty of
- Just expanded_ty -> MTVU_OK expanded_ty
- Nothing -> MTVU_Occurs
- where
- bad_tyvar_tv, bad_rhs :: Bool
-
- -- True <=> we have alpha ~ ty, where alpha is a TyVarTv
- -- and ty is not a tyvar
- bad_tyvar_tv | MetaTv { mtv_info = TyVarTv } <- tcTyVarDetails tv
- = bad_rhs
- | otherwise
- = False
-
- -- True <=> RHS is not a tyvar, or
- -- (if a unification variable) is not a TyVarTv
- bad_rhs = case tcGetTyVar_maybe rhs_ty of
- Nothing -> True
- Just tv -> case tcTyVarDetails tv of
- MetaTv { mtv_info = info }
- -> case info of
- TyVarTv -> False
- _ -> True
- SkolemTv {} -> False
- RuntimeUnk -> False
-
checkTyVarEq :: DynFlags -> AreTypeFamiliesOK -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
checkTyVarEq dflags ty_fam_ok tv ty
= inline checkTypeEq dflags ty_fam_ok (TyVarLHS tv) ty
@@ -2002,6 +1935,14 @@ checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType
-- (d) a blocking coercion hole
-- (e) an occurrence of the LHS (occurs check)
--
+-- Note that an occurs-check does not mean "definite error". For example
+-- type family F a
+-- type instance F Int = Int
+-- consider
+-- b0 ~ F b0
+-- This is perfectly reasonable, if we later get b0 ~ Int. But we
+-- certainly can't unify b0 := F b0
+--
-- For (a), (b), and (c) we check only the top level of the type, NOT
-- inside the kinds of variables it mentions. For (d) we look deeply
-- in coercions when the LHS is a tyvar (but skip coercions for type family
@@ -2009,7 +1950,7 @@ checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType
--
-- checkTypeEq is called from
-- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the
--- case-analysis on 'lhs'
+-- case-analysis on 'lhs')
-- * checkEqCanLHSFinish, which does not know the form of 'lhs'
checkTypeEq dflags ty_fam_ok lhs ty
= go ty
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d1ff4302a8e92852d90d754f1d2de1ed509d4468
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d1ff4302a8e92852d90d754f1d2de1ed509d4468
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/20201209/0c939a21/attachment-0001.html>
More information about the ghc-commits
mailing list