[Git][ghc/ghc][wip/issue-23821] 7 commits: ghc classes documentation: rm redundant comment
Gergő Érdi (@cactus)
gitlab at gitlab.haskell.org
Thu Aug 31 06:48:17 UTC 2023
Gergő Érdi pushed to branch wip/issue-23821 at Glasgow Haskell Compiler / GHC
Commits:
99fff496 by Dominik Schrempf at 2023-08-31T00:04:46-04:00
ghc classes documentation: rm redundant comment
- - - - -
fe021bab by Dominik Schrempf at 2023-08-31T00:04:46-04:00
prelude documentation: various nits
- - - - -
48c84547 by Dominik Schrempf at 2023-08-31T00:04:46-04:00
integer documentation: minor corrections
- - - - -
20cd12f4 by Dominik Schrempf at 2023-08-31T00:04:46-04:00
real documentation: nits
- - - - -
dd39bdc0 by sheaf at 2023-08-31T00:05:27-04:00
Add a test for #21765
This issue (of reporting a constraint as being redundant even though
removing it causes typechecking to fail) was fixed in aed1974e.
This commit simply adds a regression test.
Fixes #21765
- - - - -
7d9afe12 by Gergő Érdi at 2023-08-31T07:48:03+01:00
If we have multiple defaulting plugins, then we should zonk in between them
after any defaulting has taken place, to avoid a defaulting plugin seeing
a metavariable that has already been filled.
Fixes #23821.
- - - - -
8ddd852f by Gergő Érdi at 2023-08-31T07:48:03+01:00
Improvements to the documentation of defaulting plugins
Based on @simonpj's draft and comments in !11117
- - - - -
11 changed files:
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Types.hs
- docs/users_guide/extending_ghc.rst
- libraries/base/Data/Tuple.hs
- libraries/base/GHC/Enum.hs
- libraries/base/GHC/Real.hs
- libraries/ghc-bignum/src/GHC/Num/Integer.hs
- libraries/ghc-prim/GHC/Classes.hs
- testsuite/tests/plugins/defaulting-plugin/DefaultLifted.hs
- + testsuite/tests/typecheck/should_compile/T21765.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -3574,6 +3574,48 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
* Defaulting and disambiguation *
* *
*********************************************************************************
+
+Note [Defaulting plugins]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Defaulting plugins enable extending or overriding the defaulting
+behaviour. In `applyDefaulting`, before the built-in defaulting
+mechanism runs, the loaded defaulting plugins are passed the
+`WantedConstraints` and get a chance to propose defaulting assignments
+based on them.
+
+Proposals are represented as `[DefaultingProposal]` with each proposal
+consisting of a type variable to fill-in, the list of defaulting types to
+try in order, and a set of constraints to check at each try. This is
+the same representation (albeit in a nicely packaged-up data type) as
+the candidates generated by the built-in defaulting mechanism, so the
+actual trying of proposals is done by the same `disambigGroup` function.
+
+Wrinkle (DP1): The role of `WantedConstraints`
+
+ Plugins are passed `WantedConstraints` that can perhaps be
+ progressed on by defaulting. But a defaulting plugin is not a solver
+ plugin, its job is to provide defaulting proposals, i.e. mappings of
+ type variable to types. How do plugins know which type variables
+ they are supposed to default?
+
+ The `WantedConstraints` passed to the defaulting plugin are zonked
+ beforehand to ensure all remaining metavariables are unfilled. Thus,
+ the `WantedConstraints` serve a dual purpose: they are both the
+ constraints of the given context that can act as hints to the
+ defaulting, as well as the containers of the type variables under
+ consideration for defaulting.
+
+Wrinkle (DP2): Interactions between defaulting mechanisms
+
+ In the general case, we have multiple defaulting plugins loaded and
+ there is also the built-in defaulting mechanism. In this case, we
+ have to be careful to keep the `WantedConstraints` passed to the
+ plugins up-to-date by zonking between successful defaulting
+ rounds. Otherwise, two plugins might come up with a defaulting
+ proposal for the same metavariable; if the first one is accepted by
+ `disambigGroup` (thus the meta gets filled), the second proposal
+ becomes invalid (see #23821 for an example).
+
-}
applyDefaultingRules :: WantedConstraints -> TcS Bool
@@ -3590,20 +3632,16 @@ applyDefaultingRules wanteds
; tcg_env <- TcS.getGblEnv
; let plugins = tcg_defaulting_plugins tcg_env
- ; plugin_defaulted <- if null plugins then return [] else
+ -- Run any defaulting plugins
+ -- See Note [Defaulting plugins] for an overview
+ ; (wanteds, plugin_defaulted) <- if null plugins then return (wanteds, []) else
do {
; traceTcS "defaultingPlugins {" (ppr wanteds)
- ; defaultedGroups <- mapM (run_defaulting_plugin wanteds) plugins
+ ; (wanteds, defaultedGroups) <- mapAccumLM run_defaulting_plugin wanteds plugins
; traceTcS "defaultingPlugins }" (ppr defaultedGroups)
- ; return defaultedGroups
+ ; return (wanteds, defaultedGroups)
}
- -- If a defaulting plugin solves a tyvar, some of the wanteds
- -- will have filled-in metavars by now (see #23281). So we
- -- re-zonk to make sure the built-in defaulting rules don't try
- -- to solve the same metavars.
- ; wanteds <- if or plugin_defaulted then TcS.zonkWC wanteds else pure wanteds
-
; let groups = findDefaultableGroups info wanteds
; traceTcS "applyDefaultingRules {" $
@@ -3625,8 +3663,14 @@ applyDefaultingRules wanteds
groups
; traceTcS "defaultingPlugin " $ ppr defaultedGroups
; case defaultedGroups of
- [] -> return False
- _ -> return True
+ [] -> return (wanteds, False)
+ _ -> do
+ -- If a defaulting plugin solves any tyvars, some of the wanteds
+ -- will have filled-in metavars by now (see wrinkle DP2 of
+ -- Note [Defaulting plugins]). So we re-zonk to make sure later
+ -- defaulting doesn't try to solve the same metavars.
+ wanteds' <- TcS.zonkWC wanteds
+ return (wanteds', True)
}
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -86,7 +86,7 @@ module GHC.Tc.Types(
-- Defaulting plugin
DefaultingPlugin(..), DefaultingProposal(..),
- FillDefaulting, DefaultingPluginResult,
+ FillDefaulting,
-- Role annotations
RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv,
@@ -1069,8 +1069,12 @@ instance Outputable DefaultingProposal where
<+> ppr (deProposalCandidates p)
<+> ppr (deProposalCts p)
-type DefaultingPluginResult = [DefaultingProposal]
-type FillDefaulting = WantedConstraints -> TcPluginM DefaultingPluginResult
+type FillDefaulting
+ = WantedConstraints
+ -- Zonked constraints containing the unfilled metavariables that
+ -- can be defaulted. See wrinkle (DP1) of Note [Defaulting plugins]
+ -- in GHC.Tc.Solver
+ -> TcPluginM [DefaultingProposal]
-- | A plugin for controlling defaulting.
data DefaultingPlugin = forall s. DefaultingPlugin
=====================================
docs/users_guide/extending_ghc.rst
=====================================
@@ -1368,8 +1368,7 @@ Defaulting plugins have a single access point in the `GHC.Tc.Types` module
-- ^ The constraints against which defaults are checked.
}
- type DefaultingPluginResult = [DefaultingProposal]
- type FillDefaulting = WantedConstraints -> TcPluginM DefaultingPluginResult
+ type FillDefaulting = WantedConstraints -> TcPluginM [DefaultingProposal]
-- | A plugin for controlling defaulting.
data DefaultingPlugin = forall s. DefaultingPlugin
@@ -1381,18 +1380,36 @@ Defaulting plugins have a single access point in the `GHC.Tc.Types` module
-- ^ Clean up after the plugin, when exiting the type-checker.
}
-
-The plugin gets a combination of wanted constraints which can be most easily
-broken down into simple wanted constraints with ``approximateWC``. The result of
-running the plugin should be a ``DefaultingPluginResult``, a list of types that
-should be attempted for a given type variable that is ambiguous in a given
-context. GHC will check if one of the proposals is acceptable in the given
-context and then default to it. The most robust context to provide is the list
-of all wanted constraints that mention the variable you are defaulting. If you
-leave out a constraint, the default will be accepted, and then potentially
-result in a type checker error if it is incompatible with one of the constraints
-you left out. This can be a useful way of forcing a default and reporting errors
-to the user.
+The plugin has type ``WantedConstraints -> [DefaultingProposal]``.
+
+* It is given the currently unsolved constraints.
+* It returns a list of independent "defaulting proposals".
+* Each proposal of type ``DefaultingProposal`` specifies:
+ * ``deProposalTyVar``, ``deProposalCandidates``: specifies a list,
+ in priority order, of type to assign to that type variable
+ * ``deProposalCts :: [Ct]`` gives a set of constraints (always a
+ subset of the incoming ``WantedConstraints``) to use as a
+ criterion for acceptance
+
+After calling the plugin, GHC executes each ``DefaultingProposal`` in
+turn. To "execute" a proposal, GHC tries each of the proposed type
+assignments in ``deProposalCandidates`` in turn:
+
+* It assigns the proposed type to the type variable, and then tries to
+ solve ``deProposalCts``
+* If those constraints are completely solved by the assignment, GHC
+ accepts the assignment and moves on to the next ``DefaultingPropsal``
+* If not, GHC tries the next assignment in ``deProposalCandidates``.
+
+The plugin can assume that the incoming constraints are fully
+"zonked" (see :ghc-wiki:`the Wiki page on zonking <zonking>`).
+
+The most robust ``deProposalCts`` to provide is the list of all wanted
+constraints that mention the variable you are defaulting. If you leave
+out a constraint, the default may be accepted, and then potentially
+result in a type checker error if it is incompatible with one of the
+constraints you left out. This can be a useful way of forcing a
+default and reporting errors to the user.
There is an example of defaulting lifted types in the GHC test suite. In the
`testsuite/tests/plugins/` directory see `defaulting-plugin/` for the
=====================================
libraries/base/Data/Tuple.hs
=====================================
@@ -41,7 +41,7 @@ fst (x,_) = x
snd :: (a,b) -> b
snd (_,y) = y
--- | 'curry' converts an uncurried function to a curried function.
+-- | Convert an uncurried function to a curried function.
--
-- ==== __Examples__
--
=====================================
libraries/base/GHC/Enum.hs
=====================================
@@ -82,9 +82,9 @@ class Bounded a where
-- > | otherwise = minBound
--
class Enum a where
- -- | the successor of a value. For numeric types, 'succ' adds 1.
+ -- | Successor of a value. For numeric types, 'succ' adds 1.
succ :: a -> a
- -- | the predecessor of a value. For numeric types, 'pred' subtracts 1.
+ -- | Predecessor of a value. For numeric types, 'pred' subtracts 1.
pred :: a -> a
-- | Convert from an 'Int'.
toEnum :: Int -> a
@@ -92,11 +92,10 @@ class Enum a where
-- It is implementation-dependent what 'fromEnum' returns when
-- applied to a value that is too large to fit in an 'Int'.
fromEnum :: a -> Int
-
-- | Used in Haskell's translation of @[n..]@ with @[n..] = enumFrom n@,
-- a possible implementation being @enumFrom n = n : enumFrom (succ n)@.
- -- For example:
--
+ -- ==== __Examples__
-- * @enumFrom 4 :: [Integer] = [4,5,6,7,...]@
-- * @enumFrom 6 :: [Int] = [6,7,8,9,...,maxBound :: Int]@
enumFrom :: a -> [a]
@@ -104,22 +103,28 @@ class Enum a where
-- with @[n,n'..] = enumFromThen n n'@, a possible implementation being
-- @enumFromThen n n' = n : n' : worker (f x) (f x n')@,
-- @worker s v = v : worker s (s v)@, @x = fromEnum n' - fromEnum n@ and
- -- @f n y
+ --
+ -- @
+ -- f n y
-- | n > 0 = f (n - 1) (succ y)
-- | n < 0 = f (n + 1) (pred y)
- -- | otherwise = y@
- -- For example:
+ -- | otherwise = y
+ -- @
--
+ -- ==== __Examples__
-- * @enumFromThen 4 6 :: [Integer] = [4,6,8,10...]@
-- * @enumFromThen 6 2 :: [Int] = [6,2,-2,-6,...,minBound :: Int]@
enumFromThen :: a -> a -> [a]
-- | Used in Haskell's translation of @[n..m]@ with
-- @[n..m] = enumFromTo n m@, a possible implementation being
- -- @enumFromTo n m
+ --
+ -- @
+ -- enumFromTo n m
-- | n <= m = n : enumFromTo (succ n) m
- -- | otherwise = []@.
- -- For example:
+ -- | otherwise = []
+ -- @
--
+ -- ==== __Examples__
-- * @enumFromTo 6 10 :: [Int] = [6,7,8,9,10]@
-- * @enumFromTo 42 1 :: [Integer] = []@
enumFromTo :: a -> a -> [a]
@@ -127,15 +132,23 @@ class Enum a where
-- @[n,n'..m] = enumFromThenTo n n' m@, a possible implementation
-- being @enumFromThenTo n n' m = worker (f x) (c x) n m@,
-- @x = fromEnum n' - fromEnum n@, @c x = bool (>=) (<=) (x > 0)@
- -- @f n y
+ --
+ -- @
+ -- f n y
-- | n > 0 = f (n - 1) (succ y)
-- | n < 0 = f (n + 1) (pred y)
- -- | otherwise = y@ and
- -- @worker s c v m
+ -- | otherwise = y
+ -- @
+ --
+ -- and
+ --
+ -- @
+ -- worker s c v m
-- | c v m = v : worker s c (s v) m
- -- | otherwise = []@
- -- For example:
+ -- | otherwise = []
+ -- @
--
+ -- ==== __Examples__
-- * @enumFromThenTo 4 2 -6 :: [Integer] = [4,2,0,-2,-4,-6]@
-- * @enumFromThenTo 6 8 2 :: [Int] = []@
enumFromThenTo :: a -> a -> a -> [a]
=====================================
libraries/base/GHC/Real.hs
=====================================
@@ -212,7 +212,7 @@ denominator (_ :% y) = y
-- 'Foreign.C.Types.CDouble', etc., because these types contain non-finite values,
-- which cannot be roundtripped through 'Rational'.
class (Num a, Ord a) => Real a where
- -- | the rational equivalent of its real argument with full precision
+ -- | Rational equivalent of its real argument with full precision.
toRational :: a -> Rational
-- | Integral numbers, supporting integer division.
@@ -233,41 +233,41 @@ class (Num a, Ord a) => Real a where
-- In addition, 'toInteger` should be total, and 'fromInteger' should be a left
-- inverse for it, i.e. @fromInteger (toInteger i) = i at .
class (Real a, Enum a) => Integral a where
- -- | integer division truncated toward zero
+ -- | Integer division truncated toward zero.
--
-- WARNING: This function is partial (because it throws when 0 is passed as
-- the divisor) for all the integer types in @base at .
quot :: a -> a -> a
- -- | integer remainder, satisfying
+ -- | Integer remainder, satisfying
--
-- > (x `quot` y)*y + (x `rem` y) == x
--
-- WARNING: This function is partial (because it throws when 0 is passed as
-- the divisor) for all the integer types in @base at .
rem :: a -> a -> a
- -- | integer division truncated toward negative infinity
+ -- | Integer division truncated toward negative infinity.
--
-- WARNING: This function is partial (because it throws when 0 is passed as
-- the divisor) for all the integer types in @base at .
div :: a -> a -> a
- -- | integer modulus, satisfying
+ -- | Integer modulus, satisfying
--
-- > (x `div` y)*y + (x `mod` y) == x
--
-- WARNING: This function is partial (because it throws when 0 is passed as
-- the divisor) for all the integer types in @base at .
mod :: a -> a -> a
- -- | simultaneous 'quot' and 'rem'
+ -- | Simultaneous 'quot' and 'rem'.
--
-- WARNING: This function is partial (because it throws when 0 is passed as
-- the divisor) for all the integer types in @base at .
quotRem :: a -> a -> (a,a)
- -- | simultaneous 'div' and 'mod'
+ -- | simultaneous 'div' and 'mod'.
--
-- WARNING: This function is partial (because it throws when 0 is passed as
-- the divisor) for all the integer types in @base at .
divMod :: a -> a -> (a,a)
- -- | conversion to 'Integer'
+ -- | Conversion to 'Integer'.
toInteger :: a -> Integer
{-# INLINE quot #-}
=====================================
libraries/ghc-bignum/src/GHC/Num/Integer.hs
=====================================
@@ -167,11 +167,11 @@ default ()
-- Integers are stored in a kind of sign-magnitude form, hence do not expect
-- two's complement form when using bit operations.
--
--- If the value is small (fit into an 'Int'), 'IS' constructor is used.
--- Otherwise 'IP' and 'IN' constructors are used to store a 'BigNat'
--- representing respectively the positive or the negative value magnitude.
+-- If the value is small (i.e., fits into an 'Int'), the 'IS' constructor is
+-- used. Otherwise 'IP' and 'IN' constructors are used to store a 'BigNat'
+-- representing the positive or the negative value magnitude, respectively.
--
--- Invariant: 'IP' and 'IN' are used iff value doesn't fit in 'IS'
+-- Invariant: 'IP' and 'IN' are used iff the value does not fit in 'IS'.
data Integer
= IS !Int# -- ^ iff value in @[minBound::'Int', maxBound::'Int']@ range
| IP !BigNat# -- ^ iff value in @]maxBound::'Int', +inf[@ range
=====================================
libraries/ghc-prim/GHC/Classes.hs
=====================================
@@ -141,9 +141,6 @@ and @('>=')@ for the types in "GHC.Word" and "GHC.Int".
-- [__Extensionality__]: if @x == y@ = 'True' and @f@ is a function
-- whose return type is an instance of 'Eq', then @f x == f y@ = 'True'
-- [__Negation__]: @x /= y@ = @not (x == y)@
---
--- Minimal complete definition: either '==' or '/='.
---
class Eq a where
(==), (/=) :: a -> a -> Bool
=====================================
testsuite/tests/plugins/defaulting-plugin/DefaultLifted.hs
=====================================
@@ -68,7 +68,7 @@ data PluginState = PluginState { defaultClassName :: Name }
lookupName :: Module -> OccName -> TcPluginM Name
lookupName md occ = lookupOrig md occ
-solveDefaultType :: PluginState -> [Ct] -> TcPluginM DefaultingPluginResult
+solveDefaultType :: PluginState -> [Ct] -> TcPluginM [DefaultingProposal]
solveDefaultType _ [] = return []
solveDefaultType state wanteds = do
envs <- getInstEnvs
@@ -103,7 +103,7 @@ initialize :: TcPluginM PluginState
initialize = do
lookupDefaultTypes
-run :: PluginState -> WantedConstraints -> TcPluginM DefaultingPluginResult
+run :: PluginState -> WantedConstraints -> TcPluginM [DefaultingProposal]
run s ws = do
solveDefaultType s (ctsElts $ approximateWC False ws)
=====================================
testsuite/tests/typecheck/should_compile/T21765.hs
=====================================
@@ -0,0 +1,9 @@
+{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
+
+{-# OPTIONS_GHC -Wredundant-constraints #-}
+
+module T21765 where
+
+class Functor f => C f where c :: f Int
+
+instance (Functor f, Applicative f) => C f where c = pure 42
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -847,6 +847,7 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98'])
test('DeepSubsumption07', normal, compile, ['-XHaskell2010'])
test('DeepSubsumption08', normal, compile, [''])
test('DeepSubsumption09', normal, compile, [''])
+test('T21765', normal, compile, [''])
test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
test('T21550', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b75f401b3760906cb1d85734fb35f14d942a750c...8ddd852f7eeb39816eda5009997e37ffb025f69d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b75f401b3760906cb1d85734fb35f14d942a750c...8ddd852f7eeb39816eda5009997e37ffb025f69d
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/20230831/8b6c84c8/attachment-0001.html>
More information about the ghc-commits
mailing list