[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 3 commits: Type inference for data family newtype instances
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Sat May 20 03:46:10 UTC 2023
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
525ed554 by Simon Peyton Jones at 2023-05-19T10:09:15-04:00
Type inference for data family newtype instances
This patch addresses #23408, a tricky case with data family
newtype instances. Consider
type family TF a where TF Char = Bool
data family DF a
newtype instance DF Bool = MkDF Int
and [W] Int ~R# DF (TF a), with a Given (a ~# Char). We must fully
rewrite the Wanted so the tpye family can fire; that wasn't happening.
- - - - -
4885518e by Peter Trommler at 2023-05-19T23:46:02-04:00
testsuite: fix predicate on rdynamic test
Test rdynamic requires dynamic linking support, which is
orthogonal to RTS linker support. Change the predicate accordingly.
Fixes #23316
- - - - -
d74a1111 by Matthew Pickering at 2023-05-19T23:46:03-04:00
docs: Use ghc-ticket directive where appropiate in users guide
Using the directive automatically formats and links the ticket
appropiately.
- - - - -
9 changed files:
- compiler/GHC/Tc/Solver/Equality.hs
- docs/users_guide/9.8.1-notes.rst
- docs/users_guide/extending_ghc.rst
- docs/users_guide/exts/rewrite_rules.rst
- docs/users_guide/exts/template_haskell.rst
- docs/users_guide/using-optimisation.rst
- + testsuite/tests/indexed-types/should_compile/T23408.hs
- testsuite/tests/indexed-types/should_compile/all.T
- testsuite/tests/rts/linker/all.T
Changes:
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -205,15 +205,22 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
-- Decompose type constructor applications
-- NB: we have expanded type synonyms already
-can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
+can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
| Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
- -- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better
- -- error messages rather than decomposing into AppTys;
- -- hence no direct match on TyConApp
- , not (isTypeFamilyTyCon tc1)
- , not (isTypeFamilyTyCon tc2)
- = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
+ -- tcSplitTyConApp_maybe: we want to catch e.g. Maybe Int ~ (Int -> Int)
+ -- here for better error messages rather than decomposing into AppTys;
+ -- hence not using a direct match on TyConApp
+
+ , not (isTypeFamilyTyCon tc1 || isTypeFamilyTyCon tc2)
+ -- A type family at the top of LHS or RHS: we want to fall through
+ -- to the canonical-LHS cases (look for canEqLHS_maybe)
+
+ -- See (TC1) in Note [Canonicalising TyCon/TyCon equalities]
+ , let role = eqRelRole eq_rel
+ both_generative = isGenerativeTyCon tc1 role && isGenerativeTyCon tc2 role
+ , rewritten || both_generative
+ = canTyConApp ev eq_rel both_generative tc1 tys1 tc2 tys2
can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
s1@(ForAllTy (Bndr _ vis1) _) _
@@ -248,7 +255,7 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
-- Only rewritten types end up below here.
----------------------------
--- NB: pattern match on True: we want only rewritten types sent to canEqLHS
+-- NB: pattern match on rewritten=True: we want only rewritten types sent to canEqLHS
-- This means we've rewritten any variables and reduced any type family redexes
-- See also Note [No top-level newtypes on RHS of representational equalities]
can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
@@ -278,7 +285,7 @@ can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
; case eq_rel of -- See Note [Unsolved equalities]
ReprEq -> solveIrredEquality ReprEqReason ev
NomEq -> solveIrredEquality ShapeMismatchReason ev }
- -- No need to call canEqFailure/canEqHardFailure because they
+ -- No need to call canEqSoftFailure/canEqHardFailure because they
-- rewrite, and the types involved here are already rewritten
@@ -720,33 +727,31 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
------------------------
canTyConApp :: CtEvidence -> EqRel
+ -> Bool -- Both TyCons are generative
-> TyCon -> [TcType]
-> TyCon -> [TcType]
-> TcS (StopOrContinue Ct)
-- See Note [Decomposing TyConApp equalities]
-- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family
-- But they can be data families.
-canTyConApp ev eq_rel tc1 tys1 tc2 tys2
+canTyConApp ev eq_rel both_generative tc1 tys1 tc2 tys2
| tc1 == tc2
, tys1 `equalLength` tys2
= do { inerts <- getTcSInerts
; if can_decompose inerts
then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
- else canEqFailure ev eq_rel ty1 ty2 }
+ else canEqSoftFailure ev eq_rel ty1 ty2 }
-- See Note [Skolem abstract data] in GHC.Core.Tycon
| tyConSkolem tc1 || tyConSkolem tc2
= do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
; solveIrredEquality AbstractTyConReason ev }
- -- Fail straight away for better error messages
- -- See Note [Use canEqFailure in canDecomposableTyConApp]
- | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
- isGenerativeTyCon tc2 Representational)
- = canEqFailure ev eq_rel ty1 ty2
-
- | otherwise
- = canEqHardFailure ev ty1 ty2
+ | otherwise -- Different TyCons
+ = if both_generative -- See (TC2) and (TC3) in
+ -- Note [Canonicalising TyCon/TyCon equalities]
+ then canEqHardFailure ev ty1 ty2
+ else canEqSoftFailure ev eq_rel ty1 ty2
where
-- Reconstruct the types for error messages. This would do
-- the wrong thing (from a pretty printing point of view)
@@ -768,37 +773,42 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
ctEvFlavour ev == Wanted && noGivenNewtypeReprEqs tc1 inerts)
-- See Note [Decomposing newtype equalities] (EX2)
-{-
-Note [Use canEqFailure in canDecomposableTyConApp]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We must use canEqFailure, not canEqHardFailure here, because there is
-the possibility of success if working with a representational equality.
-Here is one case:
+{- Note [Canonicalising TyCon/TyCon equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
type family TF a where TF Char = Bool
data family DF a
newtype instance DF Bool = MkDF Int
-Suppose we are canonicalising (Int ~R DF (TF a)), where we don't yet
-know `a`. This is *not* a hard failure, because we might soon learn
-that `a` is, in fact, Char, and then the equality succeeds.
+Suppose we are canonicalising [W] Int ~R# DF (TF a). Then
-Here is another case:
+(TC1) We might have an inert Given (a ~# Char), so if we rewrote the wanted
+ (i.e. went around again in `can_eq_nc` with `rewritten`=True, we'd get
+ [W] Int ~R# DF Bool
+ and then the `tcTopNormaliseNewTypeTF_maybe` call would fire and
+ we'd unwrap the newtype. So we must do that "go round again" bit.
+ Hence the complicated guard (rewritten || both_generative) in `can_eq_nc`.
- [G] Age ~R Int
+(TC2) If we can't rewrite `a` yet, we'll finish with an unsolved
+ [W] Int ~R# DF (TF a)
+ in the inert set. But we must use canEqSoftFailure, not canEqHardFailure,
+ because it might be solved "later" when we learn more about `a`.
+ Hence the use of `both_generative` in `canTyConApp`.
-where Age's constructor is not in scope. We don't want to report
-an "inaccessible code" error in the context of this Given!
+(TC3) Here's another example:
+ [G] Age ~R# Int
+ where Age's constructor is not in scope. We don't want to report
+ an "inaccessible code" error in the context of this Given! So again
+ we want `canEqSoftFailure`.
-For example, see typecheck/should_compile/T10493, repeated here:
+ For example, see typecheck/should_compile/T10493, repeated here:
+ import Data.Ord (Down) -- no constructor
+ foo :: Coercible (Down Int) Int => Down Int -> Int
+ foo = coerce
- import Data.Ord (Down) -- no constructor
-
- foo :: Coercible (Down Int) Int => Down Int -> Int
- foo = coerce
-
-That should compile, but only because we use canEqFailure and not
-canEqHardFailure.
+ That should compile, but only because we use canEqSoftFailure and
+ not canEqHardFailure.
Note [Fast path when decomposing TyConApps]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1289,20 +1299,19 @@ canDecomposableFunTy ev eq_rel af f1@(m1,a1,r1) f2@(m2,a2,r2)
loc = ctEvLoc ev
role = eqRelRole eq_rel
--- | Call when canonicalizing an equality fails, but if the equality is
--- representational, there is some hope for the future.
--- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
-canEqFailure :: CtEvidence -> EqRel
- -> TcType -> TcType -> TcS (StopOrContinue Ct)
-canEqFailure ev NomEq ty1 ty2
+-- | Call canEqSoftFailure when canonicalizing an equality fails, but if the
+-- equality is representational, there is some hope for the future.
+canEqSoftFailure :: CtEvidence -> EqRel
+ -> TcType -> TcType -> TcS (StopOrContinue Ct)
+canEqSoftFailure ev NomEq ty1 ty2
= canEqHardFailure ev ty1 ty2
-canEqFailure ev ReprEq ty1 ty2
+canEqSoftFailure ev ReprEq ty1 ty2
= do { (redn1, rewriters1) <- rewrite ev ty1
; (redn2, rewriters2) <- rewrite ev ty2
-- We must rewrite the types before putting them in the
-- inert set, so that we are sure to kick them out when
-- new equalities become available
- ; traceTcS "canEqFailure with ReprEq" $
+ ; traceTcS "canEqSoftFailure with ReprEq" $
vcat [ ppr ev, ppr redn1, ppr redn2 ]
; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
; continueWith (mkIrredCt ReprEqReason new_ev) }
=====================================
docs/users_guide/9.8.1-notes.rst
=====================================
@@ -33,11 +33,10 @@ Compiler
- Incoherent instance applications are no longer specialised. The previous implementation of
specialisation resulted in nondeterministic instance resolution in certain cases, breaking
- the specification described in the documentation of the `INCOHERENT` pragma. See GHC ticket
- #22448 for further details.
+ the specification described in the documentation of the `INCOHERENT` pragma. See :ghc-ticket:`22448` for further details.
- Fix a bug in TH causing excessive calls to ``setNumCapabilities`` when ``-j`` is greater than ``-N``.
- See GHC ticket #23049.
+ See :ghc-ticket:`23049`.
- The ``-Wno-⟨wflag⟩``, ``-Werror=⟨wflag⟩`` and ``-Wwarn=⟨wflag⟩`` options are
now defined systematically for all warning groups (for example,
@@ -121,7 +120,7 @@ Runtime system
~~~~~~~~~~~~~~
- On POSIX systems that support timerfd, RTS shutdown no longer has to wait for
- the next RTS 'tick' to occur before continuing the shutdown process. See #22692.
+ the next RTS 'tick' to occur before continuing the shutdown process. See :ghc-ticket:`22692`.
``base`` library
~~~~~~~~~~~~~~~~
=====================================
docs/users_guide/extending_ghc.rst
=====================================
@@ -287,7 +287,7 @@ would invoke GHC like this:
Plugins can be also be loaded from libraries directly. It allows plugins to be
-loaded in cross-compilers (as a workaround for #14335).
+loaded in cross-compilers (as a workaround for :ghc-ticket:`14335`).
.. ghc-flag:: -fplugin-library=⟨file-path⟩;⟨unit-id⟩;⟨module⟩;⟨args⟩
:shortdesc: Load a pre-compiled static plugin from an external library
=====================================
docs/users_guide/exts/rewrite_rules.rst
=====================================
@@ -262,7 +262,7 @@ From a semantic point of view:
{-# RULES forall @m (x :: KnownNat m => Proxy m). g x = blah #-}
- See `#21093 <https://gitlab.haskell.org/ghc/ghc/-/issues/21093>`_ for discussion.
+ See :ghc-ticket:`21093` for discussion.
.. _rules-inline:
=====================================
docs/users_guide/exts/template_haskell.rst
=====================================
@@ -135,7 +135,7 @@ The :extension:`TemplateHaskellQuotes` extension is considered safe under
spliced expression must have type ``Code Q a``
**NOTE**: Currently typed splices may inhibit the unused identifier warning for
- identifiers in scope. See `#16524 <https://gitlab.haskell.org/ghc/ghc/-/issues/16524>`
+ identifiers in scope. See :ghc-ticket:`16524`.
- A *typed* expression quotation is written as ``[|| ... ||]``, or
``[e|| ... ||]``, where the "..." is an expression; if the "..."
=====================================
docs/users_guide/using-optimisation.rst
=====================================
@@ -1691,7 +1691,7 @@ as such you shouldn't need to set any of them explicitly. A flag
overhead for the check disappears completely.
This can cause slight codesize increases. It will also cause many more functions
- to get a worker/wrapper split which can play badly with rules (see Ticket #20364)
+ to get a worker/wrapper split which can play badly with rules (see :ghc-ticket:`20364`)
which is why it's currently disabled by default.
In particular if you depend on rules firing on functions marked as NOINLINE without
marking use sites of these functions as INLINE or INLINEABLE then things will break
=====================================
testsuite/tests/indexed-types/should_compile/T23408.hs
=====================================
@@ -0,0 +1,42 @@
+{-# LANGUAGE TypeFamilies, TypeApplications, GADTs, FunctionalDependencies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses #-}
+
+module T23408 where
+
+import Data.Coerce
+import Data.Proxy
+
+f :: Proxy a -> Key a -> Maybe ()
+f _ _ = Nothing
+
+g :: Key a -> Proxy a -> Maybe ()
+g _ _ = Nothing
+
+data User
+
+data family Key a
+
+newtype instance Key User = UserKey String
+
+class Convert lhs result where
+ convert :: Proxy lhs -> Proxy result
+
+instance (rec ~ rec') => Convert rec rec' where
+ convert _ = Proxy
+
+a :: Maybe ()
+a = f (convert @User Proxy) (coerce "asdf")
+
+{- Typechecking `a`
+
+ convert @User Proxy :: Proxy alpha
+ [W] Convert User alpha
+ coerce "asdf" :: Key alpha
+ [W] Coercible String (Key alpha)
+
+ Solve [W] Convert User alpha ==> [W] User ~ alpha
+ [W] Coercible String (Key User)
+-}
+
+b :: Maybe ()
+b = g (coerce "asdf") (convert @User Proxy)
+
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -308,3 +308,4 @@ test('T4254', normal, compile, [''])
test('T22547', normal, compile, [''])
test('T22717', normal, makefile_test, ['T22717'])
test('T22717_fam_orph', normal, multimod_compile, ['T22717_fam_orph', '-v0'])
+test('T23408', normal, compile, [''])
=====================================
testsuite/tests/rts/linker/all.T
=====================================
@@ -131,7 +131,7 @@ test('linker_error3', [extra_files(['linker_error.c']),
######################################
test('rdynamic', [ unless(opsys('linux') or opsys('mingw32'), skip)
- , req_rts_linker
+ , unless(have_dynamic(), skip)
# this needs runtime infrastructure to do in ghci:
# '-rdynamic' ghc, load modules only via dlopen(RTLD_BLOBAL) and more.
, omit_ways(['ghci'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/5ff7788e2038160a9168466a8fd96dc1d5a9f270...d74a11115ee26942262f95a0f617945835cf2ed2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/5ff7788e2038160a9168466a8fd96dc1d5a9f270...d74a11115ee26942262f95a0f617945835cf2ed2
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/20230519/d4fc4d93/attachment-0001.html>
More information about the ghc-commits
mailing list