[Git][ghc/ghc][wip/T22194-flags] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sat Mar 18 23:25:17 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
bbba89ea by Simon Peyton Jones at 2023-03-18T23:26:41+00:00
More wibbles
- - - - -
11 changed files:
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/polykinds/T18451a.hs
- testsuite/tests/polykinds/T22793.stderr
- testsuite/tests/polykinds/all.T
- testsuite/tests/typecheck/no_skolem_info/T14040.stderr
- testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr
- testsuite/tests/typecheck/should_compile/T13651.stderr
- testsuite/tests/typecheck/should_fail/tcfail097.stderr
Changes:
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1602,8 +1602,9 @@ mkEqErr_help :: SolverReportErrCtxt
mkEqErr_help ctxt item ty1 ty2
| Just casted_tv1 <- getCastedTyVar_maybe ty1
= mkTyVarEqErr ctxt item casted_tv1 ty2
- | Just casted_tv2 <- getCastedTyVar_maybe ty2
- = mkTyVarEqErr ctxt item casted_tv2 ty1
+-- ToDo: explain.. Cf T2627b
+-- | Just casted_tv2 <- getCastedTyVar_maybe ty2
+-- = mkTyVarEqErr ctxt item casted_tv2 ty1
| otherwise
= do { err <- reportEqErr ctxt item ty1 ty2
; return (err, noHints) }
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1530,7 +1530,7 @@ canEqCanLHS2 :: CtEvidence -- lhs ~ (rhs |> mco)
canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
| lhs1 `eqCanEqLHS` lhs2
-- It must be the case that mco is reflexive
- = canEqReflexive ev eq_rel (canEqLHSType lhs1)
+ = canEqReflexive ev eq_rel lhs1_ty
| TyVarLHS tv1 <- lhs1
, TyVarLHS tv2 <- lhs2
@@ -1610,15 +1610,23 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
else finish_without_swapping }
where
sym_mco = mkSymMCo mco
-
- finish_without_swapping = canEqCanLHSFinish ev eq_rel swapped
- lhs1 (ps_xi2 `mkCastTyMCo` mco)
- finish_with_swapping = canEqCanLHSFinish ev eq_rel (flipSwap swapped)
- lhs2 (ps_xi1 `mkCastTyMCo` sym_mco)
-
--- = 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) }
+ role = eqRelRole eq_rel
+ lhs1_ty = canEqLHSType lhs1
+ lhs2_ty = canEqLHSType lhs2
+
+ finish_without_swapping
+ = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco)
+
+ -- Swapping. We have ev : lhs1 ~ lhs2 |> co
+ -- We swap to new_ev : lhs2 ~ lhs1 |> sym co
+ -- ev = grefl1 ; sym new_ev ; grefl2
+ -- where grefl1 : lhs1 ~ lhs1 |> sym co
+ -- grefl2 : lhs2 ~ lhs2 |> co
+ finish_with_swapping
+ = do { let lhs1_redn = mkGReflRightMRedn role lhs1_ty sym_mco
+ lhs2_redn = mkGReflLeftMRedn role lhs2_ty mco
+ ; new_ev <-rewriteEqEvidence emptyRewriterSet ev swapped lhs1_redn lhs2_redn
+ ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq
-- See Note [Orienting TyVarLHS/TyFamLHS]
@@ -1717,10 +1725,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
-> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
-- See Note [Orienting TyVarLHS/TyFamLHS]
- -- If we have [W] alpha[2] ~ Maybe b[3]
- -- we can't unify (skolem-escape); but it /is/ canonical,
- -- and hence we /can/ use it for rewriting
- | reason `cterHasOnlyProblem` cteSkolemEscape
+ | reason `cterHasOnlyProblems` do_not_prevent_rewriting
-> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
| otherwise
@@ -1773,6 +1778,17 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
| otherwise
= canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
+ where
+ -- Some problems prevent /unification/ but not /rewriting/
+ -- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]
+ -- we can't unify (skolem-escape); but it /is/ canonical,
+ -- and hence we /can/ use it for rewriting
+ -- Concrete-ness: alpha[conc] ~ b[sk]
+ -- We can use it to rewrite; we still have to solve the original
+ do_not_prevent_rewriting :: CheckTyEqResult
+ do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>
+ cteProblem cteConcrete
+
---------------------------
-- Unification is off the table
canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
@@ -2307,24 +2323,6 @@ Details:
**********************************************************************
-}
-{-
-rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco) ~ lhs
- -> EqRel -> SwapFlag
- -> TcType -- lhs
- -> TcType -- rhs
- -> MCoercion -- mco
- -> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs
- -- result is independent of SwapFlag
-rewriteCastedEquality ev eq_rel swapped lhs rhs mco
- = rewriteEqEvidence emptyRewriterSet ev swapped lhs_redn rhs_redn
- where
- lhs_redn = mkGReflRightMRedn role lhs sym_mco
- rhs_redn = mkGReflLeftMRedn role rhs mco
-
- sym_mco = mkSymMCo mco
- role = eqRelRole eq_rel
--}
-
rewriteEqEvidence :: RewriterSet -- New rewriters
-- See GHC.Tc.Types.Constraint
-- Note [Wanteds rewrite Wanteds]
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -40,7 +40,7 @@ module GHC.Tc.Types.Constraint (
impredicativeProblem, insolubleOccursProblem, solubleOccursProblem,
occursProblem,
- cterHasNoProblem, cterHasProblem, cterHasOnlyProblem,
+ cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterHasOnlyProblems,
cterRemoveProblem, cterHasOccursCheck, cterFromKind,
CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
@@ -551,6 +551,9 @@ CTER bits `cterHasProblem` CTEP mask = (bits .&. mask) /= 0
cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
CTER bits `cterHasOnlyProblem` CTEP mask = bits == mask
+cterHasOnlyProblems :: CheckTyEqResult -> CheckTyEqResult -> Bool
+CTER bits `cterHasOnlyProblems` CTER mask = (bits .&. mask) == 0
+
cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
cterRemoveProblem (CTER bits) (CTEP mask) = CTER (bits .&. complement mask)
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2884,7 +2884,7 @@ But there are several cases we need to be wary of:
high a level. But, when unifying, we can promote any variables we encounter.
(3) We do not unify variables with a type with a free coercion hole.
- See (COERCION-HOLE) in Note [Unification preconditons].
+ See (COERCION-HOLE) in Note [Unification preconditions].
Note [Promotion and level-checking]
@@ -3014,7 +3014,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
---------------------
check_tv NotUnifying lhs_tv
-- We need an occurs-check here, but no level check
- -- See Note [No level-check or promotion when not unifying]
+ -- See Note [Promotion and level-checking]
| occursCheckTv lhs_tv occ_tv
= failCheckWith (cteProblem occ_prob)
| otherwise
=====================================
testsuite/tests/polykinds/T18451a.hs
=====================================
@@ -12,10 +12,7 @@ foo :: forall a b (c :: Const Type b). Proxy '[a, c]
foo = error "ruk"
-- We infer a :: k0, k0 ~ Const Type b
--- And Const is forgetful, so we expand it in the RHS of unifications;
--- so we end up with a :: Type. So the above is fine.
---
--- This is a change (March 2023); previously we didn't expand the
--- synonym, and hence failed.
---
--- See Note [Forgetful synonyms in checkTyConApp] in GHC.Tc.Utils.Unify
+-- We unify k0 := Const Type b (in the eager unifier)
+-- And that leaves us with
+-- forall (a :: Const Type b) (b :: Type) (c :: Const Type b). ...a
+-- Bad! But delicate becuase we could expand the synonym
=====================================
testsuite/tests/polykinds/T22793.stderr
=====================================
@@ -1,36 +1,13 @@
T22793.hs:15:42: error: [GHC-25897]
- • Couldn't match kind ‘ka’ with ‘k1’
- Expected kind ‘ks’, but ‘a’ has kind ‘ka’
+ • Expected kind ‘ks’, but ‘a’ has kind ‘ka’
‘ka’ is a rigid type variable bound by
the type signature for ‘bob’
at T22793.hs:13:26-27
- ‘k1’ is a rigid type variable bound by
- the type signature for ‘bob’
- at T22793.hs:13:16-17
- • In the second argument of ‘Foo’, namely ‘a’
- In the type signature:
- bob :: forall {k1}
- {ks}
- {ka}
- q
- (p :: k1 -> q -> Type)
- (f :: ka -> q)
- (s :: ks)
- (t :: ks)
- (a :: ka)
- (b :: ka). Foo s a => p a (f b) -> p s (f t)
-
-T22793.hs:16:11: error: [GHC-25897]
- • Couldn't match kind ‘ks’ with ‘k1’
- Expected kind ‘k1’, but ‘a’ has kind ‘ka’
‘ks’ is a rigid type variable bound by
the type signature for ‘bob’
at T22793.hs:13:21-22
- ‘k1’ is a rigid type variable bound by
- the type signature for ‘bob’
- at T22793.hs:13:16-17
- • In the first argument of ‘p’, namely ‘a’
+ • In the second argument of ‘Foo’, namely ‘a’
In the type signature:
bob :: forall {k1}
{ks}
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -225,7 +225,7 @@ test('T17841', normal, compile_fail, [''])
test('T17963', normal, compile_fail, [''])
test('T18300', normal, compile_fail, [''])
test('T18451', normal, compile_fail, [''])
-test('T18451a', normal, compile, [''])
+test('T18451a', normal, compile_fail, [''])
test('NestedProxies', normal, compile, [''])
test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
test('T18855', normal, compile, [''])
=====================================
testsuite/tests/typecheck/no_skolem_info/T14040.stderr
=====================================
@@ -1,7 +1,7 @@
T14040.hs:27:46: error: [GHC-46956]
- • Couldn't match kind ‘k1’ with ‘WeirdList z’
- Expected kind ‘WeirdList k1’,
+ • Couldn't match kind ‘k0’ with ‘WeirdList z’
+ Expected kind ‘WeirdList k0’,
but ‘xs’ has kind ‘WeirdList (WeirdList z)’
because kind variable ‘z’ would escape its scope
This (rigid, skolem) kind variable is bound by
@@ -25,8 +25,8 @@ T14040.hs:27:46: error: [GHC-46956]
-> p _ wl
T14040.hs:28:27: error: [GHC-46956]
- • Couldn't match kind ‘k0’ with ‘z’
- Expected kind ‘WeirdList k0’,
+ • Couldn't match kind ‘k1’ with ‘z’
+ Expected kind ‘WeirdList k1’,
but ‘WeirdCons x xs’ has kind ‘WeirdList z’
because kind variable ‘z’ would escape its scope
This (rigid, skolem) kind variable is bound by
=====================================
testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr
=====================================
@@ -8,3 +8,13 @@ PolytypeDecomp.hs:30:17: error: [GHC-91028]
• In the expression: x
In the first argument of ‘myLength’, namely ‘[x, f]’
In the expression: myLength [x, f]
+
+PolytypeDecomp.hs:30:19: error: [GHC-91028]
+ • Couldn't match type ‘a0’ with ‘[forall a. Maybe a]’
+ Expected: Id a0
+ Actual: [forall a. F [a]]
+ Cannot instantiate unification variable ‘a0’
+ with a type involving polytypes: [forall a. Maybe a]
+ • In the expression: f
+ In the first argument of ‘myLength’, namely ‘[x, f]’
+ In the expression: myLength [x, f]
=====================================
testsuite/tests/typecheck/should_compile/T13651.stderr
=====================================
@@ -1,6 +1,6 @@
T13651.hs:12:8: error: [GHC-25897]
- • Could not deduce ‘cr ~ Bar h (Foo r)’
+ • Could not deduce ‘cs ~ Bar (Foo h) (Foo s)’
from the context: (F cr cu ~ Bar h (Bar r u),
F cu cs ~ Bar (Foo h) (Bar u s))
bound by the type signature for:
@@ -8,7 +8,7 @@ T13651.hs:12:8: error: [GHC-25897]
(F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
at T13651.hs:(12,8)-(14,65)
- ‘cr’ is a rigid type variable bound by
+ ‘cs’ is a rigid type variable bound by
the type signature for:
foo :: forall cr cu h r u cs s.
(F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
=====================================
testsuite/tests/typecheck/should_fail/tcfail097.stderr
=====================================
@@ -8,9 +8,9 @@ tcfail097.hs:5:6: error: [GHC-39999]
The type variable ‘a0’ is ambiguous
Potentially matching instances:
instance Eq Ordering -- Defined in ‘GHC.Classes’
- instance Eq Integer -- Defined in ‘GHC.Num.Integer’
- ...plus 23 others
- ...plus four instances involving out-of-scope types
+ instance Eq () -- Defined in ‘GHC.Classes’
+ ...plus 22 others
+ ...plus five instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bbba89ea59ce41364b4b3a4fba7969ca2c711d28
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bbba89ea59ce41364b4b3a4fba7969ca2c711d28
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/20230318/289dfe60/attachment-0001.html>
More information about the ghc-commits
mailing list