[Git][ghc/ghc][wip/T22194-flags] Minor fixes
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Mar 15 09:29:55 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
42e00f60 by Simon Peyton Jones at 2023-03-15T09:30:37+00:00
Minor fixes
- - - - -
7 changed files:
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/polykinds/T18451a.hs
- − testsuite/tests/polykinds/T18451b.hs
- − testsuite/tests/polykinds/T18451b.stderr
- testsuite/tests/polykinds/T9017.stderr
- testsuite/tests/polykinds/all.T
- testsuite/tests/rep-poly/RepPolyBackpack1.stderr
Changes:
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2645,6 +2645,24 @@ Forall check
Fail with ForAllReason
+Note [Forgetful synonyms in checkTyConApp]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ type S a b = b -- Forgets 'a'
+
+ [W] alpha[2] ~ Maybe (S beta[4] gamma[2])
+
+We don't want to promote beta to level 2; rather, we should
+expand the synonym. (Currently, in checkTypeEqRhs promotion
+is irrevocable, by side effect.)
+
+To avoid this risk we eagerly expand forgetful synonyms.
+This also means we won't get an occurs check in
+ a ~ S a b
+
+The annoyance is that we might expand the synonym unnecessarily,
+something we generally try to avoid. But for now, this seems
+simple.
-}
data PuResult a b = PuFail CheckTyEqResult
@@ -2807,7 +2825,8 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
checkTyConApp :: TyEqFlags a
-> TcType -> TyCon -> [TcType]
-> TcM (PuResult a Reduction)
-checkTyConApp flags tc_app tc tys
+checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
+ tc_app tc tys
| isTypeFamilyTyCon tc
, let arity = tyConArity tc
= if tys `lengthIs` arity
@@ -2821,13 +2840,18 @@ checkTyConApp flags tc_app tc tys
| not (isFamFreeTyCon tc) || isForgetfulSynTyCon tc
-- e.g. S a where type S a = F [a]
-- or type S a = Int
- -- ToDo: explain why
+ -- See Note [Forgetful synonyms in checkTyConApp]
, Just ty' <- coreView tc_app -- Only synonyms and type families reply
= checkTyEqRhs flags ty' -- False to isFamFreeTyCon
- | not (isTauTyCon tc || tef_foralls flags)
+ | not (isTauTyCon tc || foralls_ok)
= failCheckWith impredicativeProblem
+ | Unifying info _ _ <- unifying
+ , isConcreteInfo info
+ , not (isConcreteTyCon tc)
+ = failCheckWith (cteProblem cteConcrete)
+
| otherwise -- Recurse on arguments
= do { tys_res <- mapCheck (checkTyEqRhs flags) tys
; return (mkTyConAppRedn Nominal tc <$> tys_res) }
@@ -2898,9 +2922,6 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
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 (cteProblem occ_prob)
-
| isConcreteInfo lhs_tv_info
, not (isConcreteTyVar occ_tv)
= if can_make_concrete occ_tv
@@ -2915,6 +2936,11 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
| isSkolemTyVar occ_tv -> failCheckWith (cteProblem cteSkolemEscape)
| otherwise -> promote lhs_tv lhs_tv_info lhs_tv_lvl
+ -- Do this after checking for promotion, because promotion
+ -- also looks at the free vars of occ_tv; avoid duplication.
+ | occursCheckTv lhs_tv occ_tv
+ = failCheckWith (cteProblem occ_prob)
+
| otherwise
= success
=====================================
testsuite/tests/polykinds/T18451a.hs
=====================================
@@ -10,3 +10,12 @@ type Const a b = a
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
=====================================
testsuite/tests/polykinds/T18451b.hs deleted
=====================================
@@ -1,12 +0,0 @@
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE DataKinds #-}
-module Bug where
-
-import Data.Kind
-import Data.Proxy
-
-type Const a b = a
-
-foo :: forall a b (c :: Const Type b). Proxy '[a, c]
-foo = error "ruk"
=====================================
testsuite/tests/polykinds/T18451b.stderr deleted
=====================================
@@ -1,7 +0,0 @@
-
-T18451b.hs:11:15: error: [GHC-97739]
- • These kind and type variables: a b (c :: Const Type b)
- are out of dependency order. Perhaps try this ordering:
- (b :: k) (a :: Const (*) b) (c :: Const (*) b)
- • In the type signature:
- foo :: forall a b (c :: Const Type b). Proxy '[a, c]
=====================================
testsuite/tests/polykinds/T9017.stderr
=====================================
@@ -1,12 +1,12 @@
T9017.hs:8:7: error: [GHC-25897]
- • Couldn't match kind ‘k2’ with ‘*’
+ • Couldn't match kind ‘k1’ with ‘*’
When matching types
a0 :: * -> * -> *
a :: k1 -> k2 -> *
Expected: a b (m b)
Actual: a0 b0 (m0 b0)
- ‘k2’ is a rigid type variable bound by
+ ‘k1’ is a rigid type variable bound by
the type signature for:
foo :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1)
(m :: k1 -> k2).
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -225,8 +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_fail, [''])
-test('T18451b', normal, compile_fail, [''])
+test('T18451a', normal, compile, [''])
test('NestedProxies', normal, compile, [''])
test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
test('T18855', normal, compile, [''])
=====================================
testsuite/tests/rep-poly/RepPolyBackpack1.stderr
=====================================
@@ -1,9 +1,9 @@
[1 of 1] Processing number-unknown
- [1 of 2] Compiling NumberUnknown[sig] ( number-unknown\NumberUnknown.hsig, nothing )
- [2 of 2] Compiling NumberStuff ( number-unknown\NumberStuff.hs, nothing )
+ [1 of 2] Compiling NumberUnknown[sig] ( number-unknown/NumberUnknown.hsig, nothing )
+ [2 of 2] Compiling NumberStuff ( number-unknown/NumberStuff.hs, nothing )
RepPolyBackpack1.bkp:17:5: error: [GHC-55287]
- The second pattern in the equation for ‘funcA’
+ The first pattern in the equation for ‘funcA’
does not have a fixed runtime representation.
Its type is:
Number l :: TYPE (Rep l)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/42e00f605c893f147a1c4bccdcca942f597f97bc
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/42e00f605c893f147a1c4bccdcca942f597f97bc
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/20230315/70a1e46e/attachment-0001.html>
More information about the ghc-commits
mailing list