[Git][ghc/ghc][wip/T22194-flags] Bug fixes
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue Mar 14 20:24:08 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
2be09e53 by Simon Peyton Jones at 2023-03-14T20:23:53+00:00
Bug fixes
- - - - -
3 changed files:
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/typecheck/should_fail/T12785b.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -2092,10 +2092,10 @@ checkTouchableTyVarEq ev lhs_tv rhs
-- Normal case
_other -> checkTyEqRhs flags rhs
- flags | MetaTv { mtv_info = tv_info, mtv_tclvl = lvl } <- tcTyVarDetails lhs_tv
+ flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv
= TEF { tef_foralls = isRuntimeUnkSkol lhs_tv
- , tef_fam_app = TEFA_Break (break_wanted lvl)
- , tef_unifying = Unifying tv_info lvl LC_Promote
+ , tef_fam_app = mkTEFA_Break ev (break_wanted tv_lvl)
+ , tef_unifying = Unifying tv_info tv_lvl LC_Promote
, tef_lhs = TyVarLHS lhs_tv }
| otherwise = pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
@@ -2144,7 +2144,7 @@ checkTypeEq ev eq_rel lhs rhs
given_flags = TEF { tef_lhs = lhs
, tef_foralls = False
, tef_unifying = NotUnifying eq_rel
- , tef_fam_app = TEFA_Break break_given }
+ , tef_fam_app = mkTEFA_Break ev break_given }
-- TEFA_Break used for: [G] a ~ Maybe (F a)
-- or [W] F a ~ Maybe (F a)
@@ -2175,6 +2175,14 @@ checkTypeEq ev eq_rel lhs rhs
-- See Detail (7) of the Note
cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
+mkTEFA_Break :: CtEvidence -> FamAppBreaker a -> TyEqFamApp a
+-- See Detail (7) of Note [Type equality cycles] in GHC.Tc.Solver.Equality
+mkTEFA_Break ev breaker
+ | CycleBreakerOrigin {} <- ctLocOrigin (ctEvLoc ev)
+ = TEFA_Recurse
+ | otherwise
+ = TEFA_Break breaker
+
-------------------------
-- | Fill in CycleBreakerTvs with the variables they stand for.
-- See Note [Type equality cycles] in GHC.Tc.Solver.Canonical.
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -35,7 +35,7 @@ module GHC.Tc.Utils.Unify (
checkTyEqRhs,
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
- TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..),
+ TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
stopPromoting, occursCheckTv
) where
@@ -58,7 +58,7 @@ import GHC.Types.Name( Name, isSystemName )
import GHC.Core.Type
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs( injectiveVarsOfType )
-import GHC.Core.TyCo.Ppr( debugPprType )
+import GHC.Core.TyCo.Ppr( debugPprType, pprTyVar )
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Multiplicity
@@ -2079,19 +2079,19 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
do { check_result <- uTypeCheckTouchableTyVarEq tv1 ty2
; case check_result of {
PuFail {} -> not_ok_so_defer ;
- PuOK {} ->
- do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1)
+ PuOK ty2' _ ->
+ do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1)
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
- , ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
+ , ppr ty2 <+> dcolon <+> ppr (typeKind ty2')
, ppr (isReflCo co_k), ppr co_k ]
; if isReflCo co_k
-- 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 (mkNomReflCo ty2) }
+ -- because tv1 is not free in ty2' (or, hence, in its kind)
+ then do { writeMetaTyVar tv1 ty2'
+ ; return (mkNomReflCo ty2') }
else defer -- This cannot be solved now. See GHC.Tc.Solver.Canonical
-- Note [Equalities with incompatible kinds] for how
@@ -2525,19 +2525,23 @@ matchExpectedFunKind hs_ty n k = go n k
* *
********************************************************************* -}
-uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () ())
+uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () TcType)
+-- The check may expand type synonyms to avoid an occurs check,
+-- so we must use the return type
uTypeCheckTouchableTyVarEq lhs_tv rhs
- = do { check_result <- checkTyEqRhs flags rhs
+ = do { traceTc "uTypeCheckTouchableTyVarEq {" (pprTyVar lhs_tv $$ ppr rhs)
+ ; check_result <- checkTyEqRhs flags rhs :: TcM (PuResult () Reduction)
+ ; traceTc "uTypeCheckTouchableTyVarEq }" (ppr check_result)
; case check_result of
PuFail reason -> return (PuFail reason)
PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn))
(ppr lhs_tv $$ ppr rhs $$ ppr redn) $
- return (PuOK () emptyBag) }
+ return (PuOK (reductionReducedType redn) emptyBag) }
where
- flags | MetaTv { mtv_info = tv_info, mtv_tclvl = lvl } <- tcTyVarDetails lhs_tv
+ flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv
= TEF { tef_foralls = False
, tef_fam_app = TEFA_Fail
- , tef_unifying = Unifying tv_info lvl LC_None
+ , tef_unifying = Unifying tv_info tv_lvl LC_None
, tef_lhs = TyVarLHS lhs_tv }
| otherwise
= pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv)
@@ -2816,12 +2820,12 @@ checkTyConApp flags tc_app tc tys
, Just ty' <- coreView tc_app -- Only synonyms and type families reply
= checkTyEqRhs flags ty' -- False to isFamFreeTyCon
+ | not (isTauTyCon tc || tef_foralls flags)
+ = failCheckWith impredicativeProblem
+
| otherwise -- Recurse on arguments
= do { tys_res <- mapCheck (checkTyEqRhs flags) tys
- ; if | not (isTauTyCon tc || tef_foralls flags)
- -> failCheckWith impredicativeProblem
- | otherwise
- -> return (mkTyConAppRedn Nominal tc <$> tys_res) }
+ ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
-------------------
checkFamApp :: TyEqFlags a
@@ -2870,7 +2874,7 @@ checkTyVar flags occ_tv
---------------------
check_tv (NotUnifying eq_rel) lhs_tv
- | lhs_tv == occ_tv
+ | occursCheckTv lhs_tv occ_tv
= failCheckWith (occursProblem eq_rel)
| otherwise
= success
@@ -2888,6 +2892,9 @@ checkTyVar flags occ_tv
check_unif :: MetaInfo -> TcLevel -> LevelCheck
-> TcTyVar -> TcM (PuResult a Reduction)
check_unif lhs_tv_info lhs_tv_lvl prom lhs_tv
+ | lhs_tv == occ_tv -- We check the kind of occ_tv later, in checkFreeVars
+ = failCheckWith insolubleOccursProblem
+
| isConcreteInfo lhs_tv_info
, not (isConcreteTyVar occ_tv)
= if can_make_concrete occ_tv
=====================================
testsuite/tests/typecheck/should_fail/T12785b.stderr
=====================================
@@ -1,6 +1,6 @@
T12785b.hs:30:65: error: [GHC-25897]
- • Could not deduce ‘Payload (S n) (Payload n s1) ~ s’
+ • Could not deduce ‘s ~ Payload (S n) (Payload n s1)’
arising from a use of ‘SBranchX’
from the context: m ~ S n
bound by a pattern with constructor:
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2be09e532f1d19f1610c01b5cd3ad172e5c845a8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2be09e532f1d19f1610c01b5cd3ad172e5c845a8
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/20230314/d205526c/attachment-0001.html>
More information about the ghc-commits
mailing list