[Git][ghc/ghc][wip/T22194] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Mar 13 00:32:45 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194 at Glasgow Haskell Compiler / GHC
Commits:
26ce990b by Simon Peyton Jones at 2023-03-13T00:33:45+00:00
Wibbles
- - - - -
7 changed files:
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1534,21 +1534,20 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
| TyVarLHS tv1 <- lhs1
, TyVarLHS tv2 <- lhs2
- , swapOverTyVars (isGiven ev) tv1 tv2
= do { traceTcS "canEqLHS2 swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
- ; new_ev <- do_swap
- ; canEqCanLHSFinish new_ev eq_rel IsSwapped (TyVarLHS tv2)
- (ps_xi1 `mkCastTyMCo` sym_mco) }
+ ; if swapOverTyVars (isGiven ev) tv1 tv2
+ then finish_with_swapping
+ else finish_without_swapping }
- | TyVarLHS tv1 <- lhs1
- , TyFamLHS fun_tc2 fun_args2 <- lhs2
- = canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
+ -- See Note [Always put TyVarLHS on the left]
+ | TyVarLHS {} <- lhs1
+ , TyFamLHS {} <- lhs2
+ = finish_without_swapping
- | TyFamLHS fun_tc1 fun_args1 <- lhs1
- , TyVarLHS tv2 <- lhs2
- = do { new_ev <- do_swap
- ; canEqTyVarFunEq new_ev eq_rel IsSwapped tv2 ps_xi2
- fun_tc1 fun_args1 ps_xi1 sym_mco }
+ -- See Note [Always put TyVarLHS on the left]
+ | TyFamLHS {} <- lhs1
+ , TyVarLHS {} <- lhs2
+ = finish_with_swapping
| TyFamLHS fun_tc1 fun_args1 <- lhs1
, TyFamLHS fun_tc2 fun_args2 <- lhs2
@@ -1604,7 +1603,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
-- this check is just to avoid unfruitful swapping
swap_for_occurs = False
-{-
+
+{- ToDo: not sure about this
-- If we have F a ~ F (F a), we want to swap.
swap_for_occurs
| cterHasNoProblem $ checkTyFamEq fun_tc2 fun_args2
@@ -1617,55 +1617,34 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
-}
; if swap_for_rewriting || swap_for_occurs
- then do { new_ev <- do_swap
- ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
+ then finish_with_swapping
else finish_without_swapping }
-
- -- that's all the special cases. Now we just figure out which non-special case
- -- to continue to.
- | otherwise
- = finish_without_swapping
-
where
sym_mco = mkSymMCo mco
- do_swap = rewriteCastedEquality ev eq_rel swapped (canEqLHSType lhs1) (canEqLHSType lhs2) mco
- finish_without_swapping = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` 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 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
--- [W] F alpha ~ beta
--- [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
-canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco)
- -- or (rhs |> mco) ~ lhs if swapped
- -> EqRel -> SwapFlag
- -> TyVar -> TcType -- lhs (or if swapped rhs), pretty lhs
- -> TyCon -> [Xi] -> TcType -- rhs (or if swapped lhs) fun and args, pretty rhs
- -> MCoercion -- :: kind(rhs) ~N kind(lhs)
- -> TcS (StopOrContinue Ct)
-canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
- = do { given_eq_lvl <- getInnermostGivenEqLevel
- ; if | touchabilityTest given_eq_lvl tv1 rhs -- alpha ~ F tys, alpha touchable
- -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs
-
- | otherwise -- F tys ~ alpha
- -> do { new_ev <- rewriteCastedEquality ev eq_rel swapped
- (mkTyVarTy tv1) (mkTyConApp fun_tc2 fun_args2)
- mco
- ; canEqCanLHSFinish new_ev eq_rel IsSwapped
- (TyFamLHS fun_tc2 fun_args2)
- (ps_xi1 `mkCastTyMCo` sym_mco) } }
- where
- sym_mco = mkSymMCo mco
- rhs = ps_xi2 `mkCastTyMCo` mco
+ finish_without_swapping
+ = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco)
+ finish_with_swapping
+ = do { new_ev <- rewriteCastedEquality ev eq_rel swapped
+ (canEqLHSType lhs1) (canEqLHSType lhs2) mco
+ ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
+
+{- Note [Always put TyVarLHS on the left]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What if one side is a tyvar and the other is a type family
+application, (a ~ F tys) ? Which to put on the left? Answer:
+* Put the tyvar on the left, (a ~ F tys) as this may be our only shot to unify.
+* But if we fail to unify and end up in cantMakeCanonical,
+ then flip back to (F tys ~ a) because it's generally better
+ to rewrite away function calls. This makes types smaller.
+
+It's important to flip back. Consider
+ [W] F alpha ~ alpha
+ [W] F alpha ~ beta
+ [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
+-}
-- The RHS here is either not CanEqLHS, or it's one that we
-- want to rewrite the LHS to (as per e.g. swapOverTyVars)
@@ -1685,8 +1664,14 @@ canEqCanLHSFinish, canEqCanLHSFinish_try_unification,
---------------------------
canEqCanLHSFinish ev eq_rel swapped lhs rhs
- = do { -- Assertion: (TyEq:K) is already satisfied
- massert (canEqLHSKind lhs `eqType` typeKind rhs)
+ = do { traceTcS "canEqCanLHSFinish" $
+ vcat [ text "ev:" <+> ppr ev
+ , text "swapped:" <+> ppr swapped
+ , text "lhs:" <+> ppr lhs
+ , text "rhs:" <+> ppr rhs ]
+
+ -- Assertion: (TyEq:K) is already satisfied
+ ; massert (canEqLHSKind lhs `eqType` typeKind rhs)
-- Assertion: (TyEq:N) is already satisfied (if applicable)
; assertPprM ty_eq_N_OK $
@@ -1724,11 +1709,13 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
then canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
else
+ -- We have a touchable unification variable on the left
do { check_result <- checkTouchableTyVarEq ev tv rhs
; case check_result of {
PuFail reason -> cantMakeCanonical reason ev eq_rel swapped lhs rhs ;
PuOK redn _ ->
+ -- Success: we can solve by unification
do { let tv_ty = mkTyVarTy tv
final_rhs = reductionReducedType redn
tv_lvl = tcTyVarLevel tv
@@ -1778,15 +1765,27 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
(mkReflRedn Nominal (canEqLHSType lhs)) rhs_redn
- ; ics <- getInertCans
- ; interactEq ics (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs, eq_rhs = rhs }) }}}
+ ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
+ , eq_lhs = lhs
+ , eq_rhs = reductionReducedType rhs_redn }) }}}
----------------------
cantMakeCanonical :: CheckTyEqResult -> CtEvidence -> EqRel -> SwapFlag
-> CanEqLHS -> TcType
-> TcS (StopOrContinue Ct)
cantMakeCanonical reason ev eq_rel swapped lhs rhs
+ | TyVarLHS tv <- lhs
+ , Just (tc,tys) <- splitTyConApp_maybe rhs
+ , isFamilyTyCon tc
+ , let lhs_ty = mkTyVarTy tv
+ = -- Flip (a ~ F tys) to (F tys ~ a)
+ do { new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
+ (mkReflRedn role rhs) (mkReflRedn role lhs_ty)
+ ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
+ , eq_lhs = TyFamLHS tc tys
+ , eq_rhs = lhs_ty }) }
+
+ | otherwise
= do { traceTcS "cantMakeCanonical" (ppr lhs $$ ppr rhs)
; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
(mkReflRedn role (canEqLHSType lhs)) (mkReflRedn role rhs)
@@ -2386,24 +2385,24 @@ But it's not so simple:
call to strictly_more_visible.
-}
-interactEq :: InertCans -> EqCt -> TcS (StopOrContinue Ct)
-interactEq inerts
- work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
-
- | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item
- = do { setEvBindIfWanted ev IsCoherent $
- evCoercion (maybeSymCo swapped $
- downgradeRole (eqRelRole eq_rel)
- (ctEvRole ev_i)
- (ctEvCoercion ev_i))
- ; stopWith ev "Solved from inert" }
-
- | otherwise
- = case lhs of
- TyVarLHS {} -> finishEqCt work_item
- TyFamLHS tc args -> do { improveLocalFunEqs inerts tc args work_item
- ; improveTopFunEqs tc args work_item
- ; finishEqCt work_item }
+interactEq :: EqCt -> TcS (StopOrContinue Ct)
+interactEq work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
+
+ = do { inerts <- getInertCans
+ ; if | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item
+ -> do { setEvBindIfWanted ev IsCoherent $
+ evCoercion (maybeSymCo swapped $
+ downgradeRole (eqRelRole eq_rel)
+ (ctEvRole ev_i)
+ (ctEvCoercion ev_i))
+ ; stopWith ev "Solved from inert" }
+
+ | otherwise
+ -> case lhs of
+ TyVarLHS {} -> finishEqCt work_item
+ TyFamLHS tc args -> do { improveLocalFunEqs inerts tc args work_item
+ ; improveTopFunEqs tc args work_item
+ ; finishEqCt work_item } }
inertsCanDischarge :: InertCans -> EqCt
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -115,13 +115,10 @@ module GHC.Tc.Solver.Monad (
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchFamTcM,
checkWellStagedDFun,
- pprEq, -- Smaller utils, re-exported from TcM
- -- TODO (DV): these are only really used in the
- -- instance matcher in GHC.Tc.Solver. I am wondering
- -- if the whole instance matcher simply belongs
- -- here
+ pprEq,
- checkTypeEq, checkTouchableTyVarEq, rewriterView
+ -- Enforcing invariants for type equalities
+ checkTypeEq, checkTouchableTyVarEq
) where
import GHC.Prelude
@@ -169,7 +166,6 @@ import GHC.Types.Name.Reader
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
-import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import GHC.Unit.Module ( HasModule, getModule, extractModule )
import qualified GHC.Rename.Env as TcM
@@ -193,6 +189,7 @@ import Data.Foldable
import qualified Data.Semigroup as S
#if defined(DEBUG)
+import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import GHC.Data.Graph.Directed
#endif
@@ -2070,39 +2067,189 @@ checkTouchableTyVarEq
-> TcTyVar -- A touchable meta-tyvar
-> TcType -- The RHS
-> TcS (PuResult () Reduction)
--- Only used for Nominal, Wanted equalities, with a touchble meta-tyvar on LHS
+-- Used for Nominal, Wanted equalities, with a touchble meta-tyvar on LHS
-- If checkTouchableTyVarEq tv ty = PuOK redn cts
-- then we can unify
-- tv := ty |> redn
-- with extra wanteds 'cts'
---
--- If it returns (Left reason) we can't unify, and the reason explains why.
-checkTouchableTyVarEq ev tv rhs
- | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
- = do { check_result :: PuResult Ct Reduction
- <- wrapTcS $ checkTyEqRhs ghci_tv
- (flattenWantedFamApp ev tv_lvl)
- (checkTvUnif tv tv_info tv_lvl)
- (checkCoUnif tv)
- rhs
+-- If it returns (PuFail reason) we can't unify, and the reason explains why.
+checkTouchableTyVarEq ev lhs_tv rhs
+ | MetaTv { mtv_info = lhs_tv_info, mtv_tclvl = lhs_tv_lvl } <- tcTyVarDetails lhs_tv
+ = do { traceTcS "checkTouchableTyVarEq" (ppr lhs_tv $$ ppr rhs)
+ ; check_result <- wrapTcS (check_rhs lhs_tv_info lhs_tv_lvl)
+ ; traceTcS "checkTouchableTyVarEq 2" (ppr lhs_tv $$ ppr check_result)
; case check_result of
PuFail reason -> return (PuFail reason)
PuOK redn cts -> do { emitWork (bagToList cts)
; return (pure redn) } }
- -- Only called on meta-tyvars
- | otherwise = pprPanic "checkTouchableTyVarEq" (ppr tv)
+
+ | otherwise = pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
+ where
+ ghci_tv = isRuntimeUnkSkol lhs_tv
+
+ check_rhs lhs_tv_info lhs_tv_lvl = case coreFullView rhs of
+ TyConApp tc tys | isTypeFamilyTyCon tc
+ , not (isConcreteTyVar lhs_tv)
+ -> -- Special case for lhs ~ F tys
+ -- We don't want to flatten that (F tys)
+ do { tys_res <- mapCheck (simple_check lhs_tv_lvl) tys
+ ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
+
+ -- Normal case
+ _other -> checkTyEqRhs ghci_tv
+ (checkTvUnif lhs_tv lhs_tv_info lhs_tv_lvl)
+ (check_fam_app lhs_tv_lvl)
+ (checkCoUnif lhs_tv lhs_tv_lvl)
+ rhs
+
+ simple_check lhs_tv_lvl = simpleCheckRhs lhs_tv (UnifyingAt lhs_tv_lvl)
+
+ check_fam_app :: TcLevel -> TcType -> TyCon -> [TcType]
+ -> TcM (PuResult Ct Reduction)
+ check_fam_app lhs_tv_lvl fam_app_ty tc tys
+ | isConcreteTyVar lhs_tv
+ = failCheckWith (cteProblem cteConcrete)
+
+ | otherwise
+ = -- Try just checking the arguments
+ do { tys_res <- mapCheck (simple_check lhs_tv_lvl) tys
+ ; case tys_res of {
+ PuOK redns _ -> return (PuOK (mkTyConAppRedn Nominal tc redns) emptyCts) ;
+ PuFail {} ->
+
+ -- Occurs check or skolem escape; so flatten
+ do { new_tv_ty <- TcM.newMetaTyVarTyAtLevel lhs_tv_lvl (typeKind fam_app_ty)
+ ; let pty = mkPrimEqPredRole Nominal fam_app_ty new_tv_ty
+ ; hole <- TcM.newCoercionHole pty
+ ; let new_ev = CtWanted { ctev_pred = pty
+ , ctev_dest = HoleDest hole
+ , ctev_loc = cb_loc
+ , ctev_rewriters = ctEvRewriters ev }
+ ; return (PuOK (mkReduction (HoleCo hole) new_tv_ty)
+ (singleCt (mkNonCanonical new_ev))) }}}
+
+ -- See Detail (7) of the Note
+ cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
+
+-------------------------
+checkTvUnif :: TcTyVar -> MetaInfo -> TcLevel -- The LHS tv, a touchable meta tvar
+ -> TcTyVar -- An occurrence of a tyvar in the RHS
+ -> TcM (PuResult a Reduction)
+checkTvUnif lhs_tv lhs_tv_info lhs_tv_lvl occ_tv
+ | lhs_tv == occ_tv
+ = failCheckWith insolubleOccursProblem
+ -- Unification is always Nominal, so no faffing
+ -- with Note [Occurs check and representational equality]
+
+ | MetaTv { mtv_info = info_occ, mtv_tclvl = lvl_occ } <- occ_details
+ = do { mb_done <- TcM.isFilledMetaTyVar_maybe occ_tv
+ ; case mb_done of
+ Just ty -> okCheckRefl ty -- Already promoted; job done
+ Nothing -> check_tv occ_tv info_occ lvl_occ }
+
+ | SkolemTv _ lvl_occ _ <- occ_details
+ , need_to_promote lvl_occ -- Skolem tyvar that needs promotion; skolem escape
+ = failCheckWith (cteProblem cteSkolemEscape)
+
+ | otherwise
+ = okCheckRefl (mkTyVarTy occ_tv)
where
- ghci_tv = isRuntimeUnkSkol tv
+ occ_details = tcTyVarDetails occ_tv
+
+ check_tv occ_tv info_occ lvl_occ
+ | not (need_to_promote lvl_occ)
+ , not (need_to_make_concrete info_occ)
+ = okCheckRefl (mkTyVarTy occ_tv) -- No-op
+
+ | lhs_tv_is_concrete
+ , cant_make_concrete info_occ
+ = failCheckWith (cteProblem cteConcrete) -- E.g. alpha[conc] := Maybe beta[tv]
+ | otherwise
+ = do { let new_info | lhs_tv_is_concrete = lhs_tv_info
+ | otherwise = info_occ
+ new_lvl = lhs_tv_lvl `minTcLevel` lvl_occ
+ -- c[conc,3] ~ p[tau,2]: want to clone p:=p'[conc,2]
+ -- c[tau,2] ~ p[tau,3]: want to clone p:=p'[tau,2]
+ ; reason <- checkFreeVars lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv))
+ ; if cterHasNoProblem reason -- Successfully promoted
+ then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv
+ ; okCheckRefl new_tv_ty }
+ else failCheckWith reason }
+
+ need_to_promote lvl_occ = lvl_occ `strictlyDeeperThan` lhs_tv_lvl
+ need_to_make_concrete info_occ = lhs_tv_is_concrete &&
+ not (isConcreteInfo info_occ)
+
+ cant_make_concrete (ConcreteTv {}) = False
+ cant_make_concrete TauTv = False
+ cant_make_concrete _ = True
+ -- Don't attempt to make other type variables concrete
+ -- (e.g. SkolemTv, TyVarTv, CycleBreakerTv, RuntimeUnkTv).
+
+ lhs_tv_is_concrete = isConcreteInfo lhs_tv_info
+
+-------------------------
+checkCoUnif :: TcTyVar -> TcLevel -> TcCoercion -> TcM (PuResult a TcCoercion)
+-- No bother about impredicativity in coercions, as they're inferred
+-- Don't check coercions for type families; see commentary at top of function
+checkCoUnif lhs_tv lhs_tv_lvl co
+ | hasCoercionHoleCo co = failCheckWith (cteProblem cteCoercionHole)
+ | otherwise = do { reason <- checkFreeVars lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
+ ; if cterHasNoProblem reason
+ then return (pure co)
+ else failCheckWith reason }
+
+--------------------------
+simpleCheckRhs :: TcTyVar -> AreUnifying
+ -> TcType -> TcM (PuResult a Reduction)
+-- Used under a type family application
+-- Occurrence check and level check
+-- (failing with skolem-escape for the latter)
+simpleCheckRhs lhs_tv are_unifying
+ = checkTyEqRhs False {- No foralls -}
+ (simpleCheckTv lhs_tv are_unifying)
+ (simpleCheckFamApp lhs_tv are_unifying)
+ (simpleCheckCo lhs_tv (areUnifying are_unifying))
+
+
+simpleCheckTv :: TcTyVar -- LHS tyvar
+ -> AreUnifying -- Just lvl => we are unifying lhs tyvar with level lvl
+ -> TcTyVar -> TcM (PuResult a Reduction)
+-- Used under a type-family application
+simpleCheckTv lhs_tv are_unifying occ_tv
+ -- Occurs check
+ | occursCheckTv lhs_tv occ_tv
+ = failCheckWith insolubleOccursProblem
+
+ -- Level check if we are unifying
+ | UnifyingAt lhs_tv_lvl <- are_unifying
+ , tcTyVarLevel occ_tv `strictlyDeeperThan` lhs_tv_lvl
+ = failCheckWith (cteProblem cteSkolemEscape)
+
+ -- Otherwise all is good
+ | otherwise
+ = okCheckRefl (mkTyVarTy occ_tv)
+
+simpleCheckFamApp :: TcTyVar -> AreUnifying
+ -> TcType -> TyCon -> [TcType]
+ -> TcM (PuResult a Reduction)
+-- Just recurse into the arguments; no flattening or anything
+simpleCheckFamApp lhs_tv are_unifying _fam_app_ty tc tys
+ = do { tys_res <- mapCheck (simpleCheckRhs lhs_tv are_unifying) tys
+ ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
+
+------------------------
checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
-> TcS (PuResult () Reduction)
-- Used for general CanEqLHSs, ones that do
-- not have a touchable type variable on the LHS
+--
+-- For Givens, flatten to avoid an occurs-check
+-- For Wanteds, don't bother
checkTypeEq ev eq_rel lhs rhs
| isGiven ev
- = do { check_result :: PuResult (TcTyVar,TcType) Reduction
- <- wrapTcS $ checkTyEqRhs ghci_tv flattenGivenFamApp
- check_tv check_co rhs
+ = do { check_result <- wrapTcS (check_given rhs)
; case check_result of
PuFail reason -> return (PuFail reason)
PuOK redn prs -> do { let prs_list = bagToList prs
@@ -2112,37 +2259,52 @@ checkTypeEq ev eq_rel lhs rhs
; return (pure redn) } }
| otherwise -- Wanted
- = do { tc_lvl <- getTcLevel
- ; check_result :: PuResult Ct Reduction
- <- wrapTcS $ checkTyEqRhs ghci_tv (flattenWantedFamApp ev tc_lvl)
- check_tv check_co rhs
+ = do { check_result <- wrapTcS (check_wanted rhs)
; case check_result of
PuFail reason -> return (PuFail reason)
PuOK redn cts -> do { emitWork (bagToList cts)
; return (pure redn) } }
where
-
ghci_tv = False
- -- check_tv: unification is off the table, so we don't need a level check
- check_tv :: TcTyVar -> TcM (PuResult a Reduction)
- check_tv = case lhs of
- TyFamLHS {} -> \tv -> okCheckRefl (mkTyVarTy tv)
- TyVarLHS lhs_tv -> occ_check_tv lhs_tv
-
- check_co :: TcCoercion -> TcM (PuResult a Coercion)
- check_co = case lhs of
- TyFamLHS {} -> \co -> return (pure co)
- TyVarLHS lhs_tv -> occ_check_co lhs_tv
-
- occ_check_tv :: TcTyVar -> TcTyVar -> TcM (PuResult a Reduction)
- occ_check_tv lhs_tv occ_tv
+ check_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
+ check_given = case lhs of
+ TyFamLHS {} -> checkTyEqRhs ghci_tv refl_tv check_given_fam_app refl_co
+ TyVarLHS tv -> checkTyEqRhs ghci_tv (check_tv tv) check_given_fam_app (check_co tv)
+
+ check_wanted :: TcType -> TcM (PuResult Ct Reduction)
+ check_wanted = case lhs of
+ TyFamLHS {} -> checkTyEqRhs ghci_tv refl_tv check_wanted_fam_app refl_co
+ TyVarLHS tv -> checkTyEqRhs ghci_tv (check_tv tv) check_wanted_fam_app (check_co tv)
+
+ check_wanted_fam_app _ tc tys -- Just recurse; if there is an
+ -- occurs check etc, just fail
+ = do { tys_res <- mapCheck check_wanted tys
+ ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
+
+ check_given_fam_app fam_app tc tys
+ = -- Try just checking the arguments
+ do { tys_res <- mapCheck check_given tys
+ ; case tys_res of {
+ PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts) ;
+ PuFail {} ->
+
+ do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
+ ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv))
+ (unitBag (new_tv, fam_app))) } }}
+ -- Why reflexive? See Detail (4) of the Note
+
+ refl_tv tv = okCheckRefl (mkTyVarTy tv)
+
+ check_tv :: TcTyVar -> TcTyVar -> TcM (PuResult a Reduction)
+ check_tv lhs_tv occ_tv
| occursCheckTv lhs_tv occ_tv = failCheckWith (occursProblem eq_rel)
| otherwise = okCheckRefl (mkTyVarTy occ_tv)
- occ_check_co lhs_tv co
- | lhs_tv `elemVarSet` tyCoVarsOfCo co = failCheckWith insolubleOccursProblem
- | otherwise = return (pure co)
+ refl_co co = return (pure co)
+
+ check_co :: TcTyVar -> TcCoercion -> TcM (PuResult a Coercion)
+ check_co lhs_tv co = simpleCheckCo lhs_tv False co
mk_new_given :: (TcTyVar, TcType) -> TcS CtEvidence
mk_new_given (new_tv, fam_app)
@@ -2155,29 +2317,49 @@ checkTypeEq ev eq_rel lhs rhs
-- See Detail (7) of the Note
cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
+
-------------------------
-flattenGivenFamApp :: TcType -> TcM (PuResult (TcTyVar, TcType) Reduction)
-flattenGivenFamApp fam_app
- = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
- ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv))
- (unitBag (new_tv, fam_app))) }
- -- Why reflexive? See Detail (4) of the Note
-
-flattenWantedFamApp :: CtEvidence -> TcLevel
- -> TcType -> TcM (PuResult Ct Reduction)
-flattenWantedFamApp ev tv_lvl fam_app_ty
- = do { new_tv_ty <- TcM.newMetaTyVarTyAtLevel tv_lvl (typeKind fam_app_ty)
- ; let pty = mkPrimEqPredRole Nominal fam_app_ty new_tv_ty
- ; hole <- TcM.newCoercionHole pty
- ; let ev = CtWanted { ctev_pred = pty
- , ctev_dest = HoleDest hole
- , ctev_loc = cb_loc
- , ctev_rewriters = ctEvRewriters ev }
- ; return (PuOK (mkReduction (HoleCo hole) new_tv_ty)
- (singleCt (mkNonCanonical ev))) }
+checkFreeVars :: TcTyVar -> TcLevel -> TyCoVarSet -> TcM CheckTyEqResult
+-- Check this set of TyCoVars for
+-- (a) occurs check
+-- (b) promote if necessary, or report skolem escape
+checkFreeVars lhs_tv dest_lvl vs
+ = do { oks <- mapM do_one (nonDetEltsUniqSet vs)
+ ; return (mconcat oks) }
where
- -- See Detail (7) of the Note
- cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
+ do_one :: TyCoVar -> TcM CheckTyEqResult
+ do_one v | isCoVar v = return cteOK
+ | lhs_tv == v = return insolubleOccursProblem
+ | no_promotion = return cteOK
+ | not (isMetaTyVar v) = return (cteProblem cteSkolemEscape)
+ | otherwise = promote_one v
+ where
+ no_promotion = not (tcTyVarLevel v `strictlyDeeperThan` dest_lvl)
+
+ -- isCoVar case: 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.
+
+ promote_one tv = do { _ <- promote_meta_tyvar TauTv dest_lvl tv
+ ; return cteOK }
+
+promote_meta_tyvar :: MetaInfo -> TcLevel -> TcTyVar -> TcM TcType
+promote_meta_tyvar info dest_lvl occ_tv
+ = do { -- Check whether occ_tv is already unified. The rhs-type
+ -- started zonked, but we may have promoted one of its type
+ -- variables, and we then encounter it for the second time.
+ -- But if so, it'll definitely be another already-checked TyVar
+ mb_filled <- TcM.isFilledMetaTyVar_maybe occ_tv
+ ; case mb_filled of {
+ Just ty -> return ty ;
+ Nothing ->
+
+ -- OK, not done already, so clone/promote it
+ do { new_tv <- TcM.cloneMetaTyVarWithInfo info dest_lvl occ_tv
+ ; TcM.writeMetaTyVar occ_tv (mkTyVarTy new_tv)
+ ; TcM.traceTc "promoteTyVar" (ppr occ_tv <+> text "-->" <+> ppr new_tv)
+ ; return (mkTyVarTy new_tv) } } }
-------------------------
-- | Fill in CycleBreakerTvs with the variables they stand for.
@@ -2188,12 +2370,3 @@ restoreTyVarCycles is
{-# SPECIALISE forAllCycleBreakerBindings_ ::
CycleBreakerVarStack -> (TcTyVar -> TcType -> TcM ()) -> TcM () #-}
--- Unwrap a type synonym only when either:
--- The type synonym is forgetful, or
--- the type synonym mentions a type family in its expansion
--- See Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite.
-rewriterView :: TcType -> Maybe TcType
-rewriterView ty@(Rep.TyConApp tc _)
- | isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
- = coreView ty
-rewriterView _other = Nothing
=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -665,6 +665,16 @@ rewrite_vector ki roles tys
{-# INLINE rewrite_vector #-}
+-- Unwrap a type synonym only when either:
+-- The type synonym is forgetful, or
+-- the type synonym mentions a type family in its expansion
+-- See Note [Rewriting synonyms]
+rewriterView :: TcType -> Maybe TcType
+rewriterView ty@(TyConApp tc _)
+ | isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
+ = coreView ty
+rewriterView _other = Nothing
+
{- Note [Do not rewrite newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We flirted with unwrapping newtypes in the rewriter -- see GHC.Tc.Solver.Canonical
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -481,7 +481,7 @@ isInsolubleReason AbstractTyConReason = True
--
------------------------------------------------------------------------------
--- | A set of problems in checking the validity of a type equality.
+-- | A /set/ of problems in checking the validity of a type equality.
-- See 'checkTypeEq'.
newtype CheckTyEqResult = CTER Word8
@@ -494,7 +494,7 @@ cterHasNoProblem :: CheckTyEqResult -> Bool
cterHasNoProblem (CTER 0) = True
cterHasNoProblem _ = False
--- | An individual problem that might be logged in a 'CheckTyEqResult'
+-- | An /individual/ problem that might be logged in a 'CheckTyEqResult'
newtype CheckTyEqProblem = CTEP Word8
cteImpredicative, cteTypeFamily, cteInsolubleOccurs,
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -986,7 +986,7 @@ writeMetaTyVarRef tyvar ref ty
; let zonked_ty_kind = typeKind zonked_ty
zonked_ty_lvl = tcTypeLevel zonked_ty
level_check_ok = not (zonked_ty_lvl `strictlyDeeperThan` tv_lvl)
- level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
+ level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty $$ ppr zonked_ty
kind_check_ok = zonked_ty_kind `eqType` zonked_tv_kind
-- Note [Extra-constraint holes in partial type signatures] in GHC.Tc.Gen.HsType
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -38,7 +38,7 @@ module GHC.Tc.Utils.TcType (
-- TcLevel
TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
strictlyDeeperThan, deeperThanOrSame, sameDepthAs,
- tcTypeLevel, tcTyVarLevel, maxTcLevel,
+ tcTypeLevel, tcTyVarLevel, maxTcLevel, minTcLevel,
--------------------------------
-- MetaDetails
@@ -47,7 +47,7 @@ module GHC.Tc.Utils.TcType (
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar,
ConcreteTvOrigin(..), isConcreteTyVar_maybe, isConcreteTyVar,
- isConcreteTyVarTy, isConcreteTyVarTy_maybe,
+ isConcreteTyVarTy, isConcreteTyVarTy_maybe, isConcreteInfo,
isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
isFlexi, isIndirect, isRuntimeUnkSkol,
metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
@@ -800,6 +800,9 @@ touchable; but then 'b' has escaped its scope into the outer implication.
maxTcLevel :: TcLevel -> TcLevel -> TcLevel
maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
+minTcLevel :: TcLevel -> TcLevel -> TcLevel
+minTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `min` b)
+
topTcLevel :: TcLevel
-- See Note [TcLevel assignment]
topTcLevel = TcLevel 0 -- 0 = outermost level
@@ -1203,6 +1206,10 @@ isConcreteTyVar_maybe tv
| otherwise
= Nothing
+isConcreteInfo :: MetaInfo -> Bool
+isConcreteInfo (ConcreteTv {}) = True
+isConcreteInfo _ = False
+
-- | Is this type variable a concrete type variable, i.e.
-- it is a metavariable with 'ConcreteTv' 'MetaInfo'?
isConcreteTyVar :: TcTyVar -> Bool
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -33,9 +33,9 @@ module GHC.Tc.Utils.Unify (
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
- checkTyEqRhs, checkTvUnif, checkCoUnif, occursCheckTv,
- PuResult(..), failCheckWith, okCheckRefl
-
+ checkTyEqRhs, simpleCheckCo,
+ PuResult(..), failCheckWith, okCheckRefl, mapCheck,
+ AreUnifying(..), areUnifying, occursCheckTv
) where
import GHC.Prelude
@@ -2551,140 +2551,6 @@ kind had instead been
then this kind equality would rightly complain about unifying kappa
with (forall k. k->*)
--}
-
-{-
-{-# NOINLINE checkTyVarEq #-} -- checkTyVarEq becomes big after the `inline` fires
-checkTyVarEq :: TcTyVar -> TcType -> CheckTyEqResult
-checkTyVarEq tv ty
- = inline checkTypeEq (TyVarLHS tv) ty
- -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
-
-{-# NOINLINE checkTyFamEq #-} -- checkTyFamEq becomes big after the `inline` fires
-checkTyFamEq :: TyCon -- type function
- -> [TcType] -- args, exactly saturated
- -> TcType -- RHS
- -> CheckTyEqResult -- always drops cteTypeFamily
-checkTyFamEq fun_tc fun_args ty
- = inline checkTypeEq (TyFamLHS fun_tc fun_args) ty
- `cterRemoveProblem` cteTypeFamily
- -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
-
-checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult
--- If cteHasNoProblem (checkTypeEq dflags lhs rhs), then lhs ~ rhs
--- is a canonical CEqCan.
---
--- In particular, this looks for:
--- (a) a forall type (forall a. blah)
--- (b) a predicate type (c => ty)
--- (c) a type family; see Note [Prevent unification with type families]
--- (d) 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, and for (d) see
--- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
---
--- checkTypeEq is called from
--- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the
--- case-analysis on 'lhs')
--- * checkEqCanLHSFinish, which does not know the form of 'lhs'
-checkTypeEq lhs ty
- = go ty
- where
- impredicative = cteProblem cteImpredicative
- type_family = cteProblem cteTypeFamily
- insoluble_occurs = cteProblem cteInsolubleOccurs
- soluble_occurs = cteProblem cteSolubleOccurs
-
- -- The GHCi runtime debugger does its type-matching with
- -- unification variables that can unify with a polytype
- -- or a TyCon that would usually be disallowed by bad_tc
- -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect
- ghci_tv
- | TyVarLHS tv <- lhs
- , MetaTv { mtv_info = RuntimeUnkTv } <- tcTyVarDetails tv
- = True
-
- | otherwise
- = False
-
- go :: TcType -> CheckTyEqResult
- go (TyVarTy tv') = go_tv tv'
- go (TyConApp tc tys) = go_tc tc tys
- go (LitTy {}) = cteOK
- go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
- = go w S.<> go a S.<> go r S.<>
- if not ghci_tv && isInvisibleFunArg af
- then impredicative
- else cteOK
- go (AppTy fun arg) = go fun S.<> go arg
- go (CastTy ty co) = go ty S.<> go_co co
- go (CoercionTy co) = go_co co
- go (ForAllTy (Bndr tv' _) ty) = (case lhs of
- TyVarLHS tv | tv == tv' -> go_occ (tyVarKind tv') S.<> cterClearOccursCheck (go ty)
- | otherwise -> go_occ (tyVarKind tv') S.<> go ty
- _ -> go ty)
- S.<>
- if ghci_tv then cteOK else impredicative
-
- go_tv :: TcTyVar -> CheckTyEqResult
- -- this slightly peculiar way of defining this means
- -- we don't have to evaluate this `case` at every variable
- -- occurrence
- go_tv = case lhs of
- TyVarLHS tv -> \ tv' -> go_occ (tyVarKind tv') S.<>
- if tv == tv' then insoluble_occurs else cteOK
- TyFamLHS {} -> \ _tv' -> cteOK
- -- See Note [Occurrence checking: look inside kinds] in GHC.Core.Type
-
- -- For kinds, we only do an occurs check; we do not worry
- -- about type families or foralls
- -- See Note [Checking for foralls]
- go_occ k = cterFromKind $ go k
-
- go_tc :: TyCon -> [TcType] -> CheckTyEqResult
- -- this slightly peculiar way of defining this means
- -- we don't have to evaluate this `case` at every tyconapp
- go_tc = case lhs of
- TyVarLHS {} -> \ tc tys -> check_tc tc S.<> go_tc_args tc tys
- TyFamLHS fam_tc fam_args -> \ tc tys ->
- if tcEqTyConApps fam_tc fam_args tc tys
- then insoluble_occurs
- else check_tc tc S.<> go_tc_args tc tys
-
- -- just look at arguments, not the tycon itself
- go_tc_args :: TyCon -> [TcType] -> CheckTyEqResult
- go_tc_args tc tys | isGenerativeTyCon tc Nominal = foldMap go tys
- | otherwise
- = let (tf_args, non_tf_args) = splitAt (tyConArity tc) tys in
- cterSetOccursCheckSoluble (foldMap go tf_args) S.<> foldMap go non_tf_args
-
- -- no bother about impredicativity in coercions, as they're
- -- inferred
- go_co co | TyVarLHS tv <- lhs
- , tv `elemVarSet` tyCoVarsOfCo co
- = soluble_occurs
-
- -- Don't check coercions for type families; see commentary at top of function
- | otherwise
- = cteOK
-
- check_tc :: TyCon -> CheckTyEqResult
- check_tc
- | ghci_tv = \ _tc -> cteOK
- | otherwise = \ tc -> (if isTauTyCon tc then cteOK else impredicative) S.<>
- (if isFamFreeTyCon tc then cteOK else type_family)
--}
-
-{-
Note [prepareForUnification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
alpha[2] ~ ty
@@ -2762,53 +2628,94 @@ instance Applicative (PuResult a) where
PuOK {} <*> PuFail p2 = PuFail p2
PuOK f c1 <*> PuOK x c2 = PuOK (f x) (c1 `unionBags` c2)
+instance (Outputable a, Outputable b) => Outputable (PuResult a b) where
+ ppr (PuFail prob) = text "PuFail" <+> (ppr prob)
+ ppr (PuOK x cts) = text "PuOK" <> braces
+ (vcat [ text "redn:" <+> ppr x
+ , text "cts:" <+> ppr cts ])
+
okCheckRefl :: TcType -> TcM (PuResult a Reduction)
okCheckRefl ty = return (PuOK (mkReflRedn Nominal ty) emptyBag)
failCheckWith :: CheckTyEqResult -> TcM (PuResult a b)
failCheckWith p = return (PuFail p)
+mapCheck :: (x -> TcM (PuResult a Reduction))
+ -> [x]
+ -> TcM (PuResult a Reductions)
+mapCheck f xs
+ = do { (ress :: [PuResult a Reduction]) <- mapM f xs
+ ; return (unzipRedns <$> sequenceA ress) }
+ -- sequenceA :: [PuResult a Reduction] -> PuResult a [Reduction]
+ -- unzipRedns :: [Reduction] -> Reductions
+
+data AreUnifying
+ = UnifyingAt TcLevel -- We are trying to unify a meta-tyvar at level lvl
+ | NotUnifying -- Not attempting to unify
+
+areUnifying :: AreUnifying -> Bool
+areUnifying (UnifyingAt {}) = True
+areUnifying NotUnifying = False
+
+occursCheckTv :: TcTyVar -> TcTyVar -> Bool
+occursCheckTv lhs_tv occ_tv
+ = lhs_tv == occ_tv
+ || lhs_tv `elemVarSet` tyCoVarsOfType (tyVarKind occ_tv)
+
uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () ())
-uTypeCheckTouchableTyVarEq tv rhs
- | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
- = do { check_result <- checkTyEqRhs False dont_flatten
- (checkTvUnif tv tv_info tv_lvl)
- (checkCoUnif tv)
+uTypeCheckTouchableTyVarEq lhs_tv rhs
+ | MetaTv { mtv_info = tv_info } <- tcTyVarDetails lhs_tv
+ = do { check_result <- checkTyEqRhs False
+ (simple_check_tv (isConcreteInfo tv_info))
+ dont_flatten
+ (simpleCheckCo lhs_tv True)
rhs
- -- checkTvUnif will never do any promotion because tv_lvl is
- -- the ambient level. But we still need the concreteness changes
; case check_result of
PuFail reason -> return (PuFail reason)
- PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn))
- (ppr tv $$ ppr rhs $$ ppr redn) $
- return (PuOK () emptyBag) }
+ PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn))
+ (ppr lhs_tv $$ ppr rhs $$ ppr redn) $
+ return (PuOK () emptyBag) }
-- Only called on meta-tyvars
- | otherwise = pprPanic "uTypeCHeckTouchableTyVarEq" (ppr tv)
+ | otherwise = pprPanic "uTypeCHeckTouchableTyVarEq" (ppr lhs_tv)
where
- dont_flatten :: TcType -> TcM (PuResult () Reduction)
- dont_flatten _ = failCheckWith (cteProblem cteTypeFamily)
+ dont_flatten :: TcType -> TyCon -> [TcType] -> TcM (PuResult () Reduction)
+ dont_flatten _ _ _ = failCheckWith (cteProblem cteTypeFamily)
-- See Note [Prevent unification with type families]
+ simple_check_tv lhs_tv_is_concrete occ_tv
+ | occursCheckTv lhs_tv occ_tv
+ = failCheckWith insolubleOccursProblem
+ | lhs_tv_is_concrete, not (isConcreteTyVar occ_tv)
+ = failCheckWith (cteProblem cteConcrete)
+ | otherwise
+ = okCheckRefl (mkTyVarTy occ_tv)
+
+simpleCheckCo :: TcTyVar -> Bool -> TcCoercion -> TcM (PuResult a Coercion)
+-- No bother about impredicativity in coercions, as they're inferred
+-- Don't check coercions for type families; see commentary at top of function
+simpleCheckCo lhs_tv unifying co
+ | lhs_tv `elemVarSet` tyCoVarsOfCo co = failCheckWith insolubleOccursProblem
+ | unifying
+ , hasCoercionHoleCo co = failCheckWith (cteProblem cteCoercionHole)
+ | otherwise = return (PuOK co emptyBag)
+ -- hasCoercionHoleCo:
+ -- See (COERCION-HOLE) in Note [Unification preconditions]
+ --
+ -- ToDo: could combine these two folds
+ -- (free vars and coercion holes) into one
+
+-----------------------------
checkTyEqRhs :: forall a.
Bool -- RuntimeUnk tyvar on the LHS; accept foralls
- -> (TcType -> TcM (PuResult a Reduction))
-> (TcTyVar -> TcM (PuResult a Reduction))
+ -> (TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction))
-> (TcCoercion -> TcM (PuResult a TcCoercion))
-> TcType
-> TcM (PuResult a Reduction)
-checkTyEqRhs ghci_tv flatten_fam_app check_tv check_co rhs
- = case coreFullView rhs of
- -- Special case for lhs ~ F tys
- -- We don't want to flatten that (F tys)
- TyConApp tc tys | isTypeFamilyTyCon tc
- -> do { tys_res <- go_tys tys
- ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
-
- -- Normal case
- _other -> go rhs
-
+checkTyEqRhs ghci_tv check_tv flatten_fam_app check_co rhs
+ = go rhs
where
go :: TcType -> TcM (PuResult a Reduction)
go ty@(LitTy {}) = okCheckRefl ty
@@ -2840,23 +2747,17 @@ checkTyEqRhs ghci_tv flatten_fam_app check_tv check_co rhs
| ghci_tv = okCheckRefl ty
| otherwise = failCheckWith impredicativeProblem -- Not allowed (TyEq:F)
- go_tys :: [TcType] -> TcM (PuResult a Reductions)
- go_tys tys = do { (ress :: [PuResult a Reduction]) <- mapM go tys
- ; return (unzipRedns <$> sequenceA ress) }
- -- sequenceA :: [PuResult a] -> PuResult [a]
- -- unzipRedns :: [Reduction] -> Reductions
-
go_tc :: TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
go_tc ty tc tys
| isTypeFamilyTyCon tc
- = flatten_fam_app ty
+ = flatten_fam_app ty tc tys
| not (isFamFreeTyCon tc) -- e.g. S a where type S a = F [a]
, Just ty' <- coreView ty -- Only synonyms and type families reply
= go ty' -- False to isFamFreeTyCon
| otherwise
- = do { tys_res <- go_tys tys
+ = do { tys_res <- mapCheck go tys
; if | PuFail {} <- tys_res, Just ty' <- coreView ty
-> go ty' -- Expand synonyms on failure
| not (isTauTyCon tc || ghci_tv)
@@ -2864,83 +2765,6 @@ checkTyEqRhs ghci_tv flatten_fam_app check_tv check_co rhs
| otherwise
-> return (mkTyConAppRedn Nominal tc <$> tys_res) }
--------------------------
-checkCoUnif :: TcTyVar -> TcCoercion -> TcM (PuResult a TcCoercion)
--- No bother about impredicativity in coercions, as they're inferred
--- Don't check coercions for type families; see commentary at top of function
-checkCoUnif lhs_tv co
- | lhs_tv `elemVarSet` tyCoVarsOfCo co = failCheckWith insolubleOccursProblem
- | hasCoercionHoleCo co = failCheckWith (cteProblem cteCoercionHole)
- | otherwise = return (PuOK co emptyBag)
- -- ToDo: could combine these two folds
- -- (free vars and coercion holes) into one
-
--------------------------
-checkTvUnif :: TcTyVar -> MetaInfo -> TcLevel -- The LHS tv, a touchable meta tvar
- -> TcTyVar -- An occurrence of a tyvar in the RHS
- -> TcM (PuResult a Reduction)
-checkTvUnif lhs_tv lhs_tv_info lhs_tv_lvl occ_tv
- | occursCheckTv lhs_tv occ_tv
- = failCheckWith insolubleOccursProblem
- -- Unification is always Nominal, so no faffing
- -- with Note [Occurs check and representational equality]
-
- | MetaTv { mtv_info = info_occ, mtv_tclvl = lvl_occ } <- occ_details
- = -- Check for unified. The type started zonked, but we may have
- -- promoted one of its type variables, and we then encounter
- -- it for the second time. But if so, it'll definitely be another TyVar
- do { mb_filled <- isFilledMetaTyVar_maybe occ_tv
- ; case mb_filled of
- Just ty | Just occ_tv2 <- getTyVar_maybe ty
- -> checkTvUnif lhs_tv lhs_tv_info lhs_tv_lvl occ_tv2
- | otherwise -> pprPanic "checkTouchableTyVarEq" (ppr occ_tv $$ ppr ty)
- Nothing -> check_tv2 occ_tv info_occ lvl_occ }
-
- | SkolemTv _ lvl_occ _ <- occ_details
- , need_to_promote lvl_occ -- Skolem tyvar that needs promotion; skolem escape
- = failCheckWith (cteProblem cteSkolemEscape)
-
- | otherwise
- = okCheckRefl (mkTyVarTy occ_tv)
- where
- occ_details = tcTyVarDetails occ_tv
-
- check_tv2 occ_tv info_occ lvl_occ
- | not (need_to_promote lvl_occ)
- , not (need_to_make_concrete info_occ)
- = okCheckRefl (mkTyVarTy occ_tv) -- No-op
-
- | tv_is_concrete
- , cant_make_concrete info_occ
- = failCheckWith (cteProblem cteConcrete) -- E.g. alpha[conc] := Maybe beta[tv]
-
- | otherwise
- = do { let new_info | tv_is_concrete = lhs_tv_info
- | otherwise = info_occ
- ; new_tv <- cloneMetaTyVarWithInfo new_info lhs_tv_lvl occ_tv
- ; writeMetaTyVar occ_tv (mkTyVarTy new_tv)
- ; traceTc "promoteTyVar" (ppr occ_tv <+> text "-->" <+> ppr new_tv)
- ; okCheckRefl (mkTyVarTy new_tv) }
-
- need_to_promote lvl_occ = lvl_occ `strictlyDeeperThan` lhs_tv_lvl
- need_to_make_concrete info_occ = is_concrete lhs_tv_info && not (is_concrete info_occ)
-
- cant_make_concrete (ConcreteTv {}) = False
- cant_make_concrete TauTv = False
- cant_make_concrete _ = True
- -- Don't attempt to make other type variables concrete
- -- (e.g. SkolemTv, TyVarTv, CycleBreakerTv, RuntimeUnkTv).
-
- tv_is_concrete = is_concrete lhs_tv_info
-
- is_concrete (ConcreteTv {}) = True
- is_concrete _ = False
-
-occursCheckTv :: TcTyVar -> TcTyVar -> Bool
-occursCheckTv lhs_tv occ_tv
- = lhs_tv == occ_tv
- || lhs_tv `elemVarSet` tyCoVarsOfType (tyVarKind occ_tv)
-
-------------------------
touchabilityTest :: TcLevel -> TcTyVar -> TcType -> Bool
-- This is the key test for untouchability:
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/26ce990bef18ba7a9c8af12628085d1fb890e856
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/26ce990bef18ba7a9c8af12628085d1fb890e856
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/20230312/973ab75c/attachment-0001.html>
More information about the ghc-commits
mailing list