[Git][ghc/ghc][master] Allow defaulting of representational equalities
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Sat Mar 8 21:32:56 UTC 2025
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
1e53277a by sheaf at 2025-03-08T16:32:25-05:00
Allow defaulting of representational equalities
This commit generalises the defaulting of equality constraints that
was introduced in 663daf8d (with follow-up in 6863503c) to allow
the defaulting of *representational* equality constraints.
Now we default a representational equality
ty1 ~R# ty2
by unifying ty1 ~# ty2.
This allows the following defaulting to take place:
- Coercible alpha[tau] Int ==> alpha := Int
- Coercible (IO beta[tau]) (IO Char) ==> beta := Char
See Note [Defaulting representational equalities] in GHC.Tc.Solver.Default
for more details.
Fixes #21003
- - - - -
14 changed files:
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
- docs/users_guide/9.14.1-notes.rst
- testsuite/tests/default/default-fail08.hs
- testsuite/tests/default/default-fail08.stderr
- testsuite/tests/rep-poly/T14561b.stderr
- testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
- + testsuite/tests/typecheck/should_compile/T21003.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T10495.hs
- testsuite/tests/typecheck/should_fail/T10495.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/Default.hs
=====================================
@@ -1,3 +1,5 @@
+{-# LANGUAGE MultiWayIf #-}
+
module GHC.Tc.Solver.Default(
tryDefaulting, tryUnsatisfiableGivens,
isInteractiveClass, isNumClass
@@ -26,7 +28,7 @@ import GHC.Core.Reduction( Reduction, reductionCoercion )
import GHC.Core
import GHC.Core.DataCon
import GHC.Core.Make
-import GHC.Core.Coercion( mkNomReflCo, isReflCo )
+import GHC.Core.Coercion( isReflCo, mkReflCo, mkSubCo )
import GHC.Core.Unify ( tcMatchTyKis )
import GHC.Core.Predicate
import GHC.Core.Type
@@ -362,9 +364,9 @@ tryConstraintDefaulting wc
where
go_wc :: WantedConstraints -> TcS WantedConstraints
go_wc wc@(WC { wc_simple = simples, wc_impl = implics })
- = do { mb_simples <- mapMaybeBagM go_simple simples
+ = do { simples' <- mapMaybeBagM go_simple simples
; mb_implics <- mapMaybeBagM go_implic implics
- ; return (wc { wc_simple = mb_simples, wc_impl = mb_implics }) }
+ ; return (wc { wc_simple = simples', wc_impl = mb_implics }) }
go_simple :: Ct -> TcS (Maybe Ct)
go_simple ct = do { solved <- tryCtDefaultingStrategy ct
@@ -403,7 +405,7 @@ defaultExceptionContext ct
; let ev = ctEvidence ct
ev_tm = mkEvCast (Var empty_ec_id) (wrapIP (ctEvPred ev))
; setEvBindIfWanted ev EvCanonical ev_tm
- -- EvCanonical: see Note [CallStack and ExecptionContext hack]
+ -- EvCanonical: see Note [CallStack and ExceptionContext hack]
-- in GHC.Tc.Solver.Dict
; return True }
| otherwise
@@ -423,19 +425,54 @@ defaultCallStack ct
defaultEquality :: CtDefaultingStrategy
-- See Note [Defaulting equalities]
defaultEquality ct
- | EqPred NomEq ty1 ty2 <- classifyPredType (ctPred ct)
+ | EqPred eq_rel ty1 ty2 <- classifyPredType (ctPred ct)
= do { -- Remember: `ct` may not be zonked;
-- see (DE3) in Note [Defaulting equalities]
z_ty1 <- TcS.zonkTcType ty1
; z_ty2 <- TcS.zonkTcType ty2
-
+ ; case eq_rel of
+ { NomEq ->
-- Now see if either LHS or RHS is a bare type variable
-- You might think the type variable will only be on the LHS
-- but with a type function we might get F t1 ~ alpha
- ; case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of
+ case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of
(Just z_tv1, _) -> try_default_tv z_tv1 z_ty2
(_, Just z_tv2) -> try_default_tv z_tv2 z_ty1
- _ -> return False }
+ _ -> return False ;
+
+ ; ReprEq
+ -- See Note [Defaulting representational equalities]
+ | CIrredCan (IrredCt { ir_reason }) <- ct
+ , isInsolubleReason ir_reason
+ -- Don't do this for definitely insoluble representational
+ -- equalities such as Int ~R# Bool.
+ -> return False
+ | otherwise
+ ->
+ do { traceTcS "defaultEquality ReprEq {" $ vcat
+ [ text "ct:" <+> ppr ct
+ , text "z_ty1:" <+> ppr z_ty1
+ , text "z_ty2:" <+> ppr z_ty2
+ ]
+ -- Promote this representational equality to a nominal equality.
+ --
+ -- This handles cases such as @IO alpha[tau] ~R# IO Int@
+ -- by defaulting @alpha := Int@, which is useful in practice
+ -- (see Note [Defaulting representational equalities]).
+ ; (co, new_eqs, _unifs, _rw) <-
+ wrapUnifierX (ctEvidence ct) Nominal $
+ -- NB: nominal equality!
+ \ uenv -> uType uenv z_ty1 z_ty2
+ -- Only accept this solution if no new equalities are produced
+ -- by the unifier.
+ --
+ -- See Note [Defaulting representational equalities].
+ ; if null new_eqs
+ then do { setEvBindIfWanted (ctEvidence ct) EvCanonical $
+ (evCoercion $ mkSubCo co)
+ ; return True }
+ else return False
+ } } }
| otherwise
= return False
@@ -477,8 +514,10 @@ defaultEquality ct
; unifyTyVar lhs_tv rhs_ty -- NB: unifyTyVar adds to the
-- TcS unification counter
; setEvBindIfWanted (ctEvidence ct) EvCanonical $
- evCoercion (mkNomReflCo rhs_ty)
- ; return True }
+ evCoercion (mkReflCo Nominal rhs_ty)
+ ; return True
+ }
+
combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy
combineStrategies default1 default2 ct
@@ -518,29 +557,42 @@ too drastic.
Note [Defaulting equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In top-level defaulting (as per Note [Top-level Defaulting Plan]), it makes
+sense to try to default equality constraints, in addition to e.g. typeclass
+defaulting: this doesn't threaten principal types (see DE1 below), but
+allows GHC to accept strictly more programs.
+
+This Note explains defaulting nominal equalities; see also
+Note [Defaulting representational equalities] which describes
+the defaulting of representational equalities.
+
Consider
+
f :: forall a. (forall t. (F t ~ Int) => a -> Int) -> Int
g :: Int
g = f id
We'll typecheck
+
id :: forall t. (F t ~ Int) => alpha[1] -> Int
+
where the `alpha[1]` comes from instantiating `f`. So we'll end up
with the implication constraint
+
forall[2] t. (F t ~ Int) => alpha[1] ~ Int
-And that can't be solved because `alpha` is untouchable under the
+
+and that can't be solved because `alpha` is untouchable under the
equality (F t ~ Int).
This is tiresome, and gave rise to user complaints: #25125 and #25029.
Moreover, in this case there is no good reason not to unify alpha:=Int.
Doing so solves the constraint, and since `alpha` is not otherwise
-constrained, it does no harm. So the new plan is this:
+constrained, it does no harm.
- * For the Wanted constraint
- [W] alpha ~ ty
- if the only reason for not unifying is untouchability, then during
- top-level defaulting, go ahead and unify
+In conclusion, for a Wanted equality constraint [W] lhs ~ rhs, if the only
+reason for not unifying is that either lhs or rhs is an untouchable metavariable
+then, in top-level defaulting, go ahead and unify.
In top-level defaulting, we already do several other somewhat-ad-hoc,
but terribly convenient, unifications. This is just one more.
@@ -555,12 +607,11 @@ Wrinkles:
f x = case x of T1 -> True
Should we infer f :: T a -> Bool, or f :: T a -> a. Both are valid, but
- neither is more general than the other
+ neither is more general than the other.
(DE2) We still can't unify if there is a skolem-escape check, or an occurs check,
or it it'd mean unifying a TyVarTv with a non-tyvar. It's only the
- "untouchability test" that we lift. We can lift it by saying that the innermost
- given equality is at top level.
+ "untouchability test" that we lift.
(DE3) The contraint we are looking at may not be fully zonked; for example,
an earlier defaulting might have affected it. So we zonk-on-the fly in
@@ -568,7 +619,7 @@ Wrinkles:
(DE4) Promotion. Suppose we see alpha[2] := Maybe beta[4]. We want to promote
beta[4] to level 2 and unify alpha[2] := Maybe beta'[2]. This is done by
- checkTyEqRhs.
+ checkTyEqRhs called in defaultEquality.
(DE5) Promotion. Suppose we see alpha[2] := F beta[4], where F is a type
family. Then we still want to promote beta to beta'[2], and unify. This is
@@ -587,6 +638,64 @@ Then when we default 'a' we can solve the constraint. And we want to do
that before starting in on type classes. We MUST do it before reporting
errors, because it isn't an error! #7967 was due to this.
+Note [Defaulting representational equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we end up with [W] alpha ~#R Int, with no other constraints on alpha.
+Then it makes sense to simply unify alpha := Int -- the alternative is to
+reject the program due to an ambiguous metavariable alpha, so it makes sense
+to unify and accept instead.
+
+This is particularly convenient for users of `coerce`, as it lessens the
+amount of type annotations required (see #21003). Consider for example:
+
+ -- 'foldMap' defined using 'traverse'
+ foldMapUsingTraverse :: forall t m a. (Traversable t, Monoid m) => (a -> m) -> t a -> m
+ foldMapUsingTraverse = coerce $ traverse @t @(Const m)
+
+ -- 'traverse_' defined using 'foldMap'
+ traverse_UsingFoldMap :: forall f t a. (Foldable t, Applicative f) => (a -> f ()) -> t a -> f ()
+ traverse_UsingFoldMap = coerce $ foldMap @t @(Ap f ())
+
+Typechecking these functions results in unsolved Wanted constraints of the form
+[W] alpha[tau] ~R# some_ty; accepting such programs by unifying
+alpha := some_ty avoids the need for users to specify tiresome additional
+type annotations, such as:
+
+ foldMapUsingTraverse = coerce $ traverse @t @(Const m) @a
+ traverse_UsingFoldMap = coerce $ foldMap @t @(Ap f ()) @a
+
+Consider also the following example:
+
+ -- 'sequence_', but for two nested 'Foldable' structures
+ sequenceNested_ :: forall f1 f2. (Foldable f1, Foldable f2) => f1 (f2 (IO ())) -> IO ()
+ sequenceNested_ = coerce $ sequence_ @( Compose f1 f2 )
+
+Here, we end up with [W] mu[tau] beta[tau] ~#R IO (), and it similarly makes
+sense to default mu := IO, beta := (). This avoids requiring the
+user to provide additional type applications:
+
+ sequenceNested_ = coerce $ sequence_ @( Compose f1 f2 ) @IO @()
+
+The plan for defaulting a representational equality, say [W] ty1 ~R# ty2,
+is thus as follows:
+
+ 1. attempt to unify ty1 ~# ty2 (at nominal role)
+ 2. a. if this succeeds without deferring any constraints, accept this solution
+ b. otherwise, keep the original constraint.
+
+(2b) ensures that we don't degrade all error messages by always turning unsolved
+representational equalities into nominal ones; we only want to default a
+representational equality when we can fully solve it.
+
+Note that this does not threaten principle types. Recall that the original worry
+(as per Note [Do not unify representational equalities]) was that we might have
+
+ [W] alpha ~R# Int
+ [W] alpha ~ Age
+
+in which case unifying alpha := Int would be wrong, as the correct solution is
+alpha := Age. This worry doesn't concern us in top-level defaulting, because
+defaulting takes place after generalisation; it is fully monomorphic.
*********************************************************************************
* *
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -189,9 +189,9 @@ solveCallStack ev ev_cs
= do { cs_tm <- evCallStack ev_cs
; let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
; setEvBindIfWanted ev EvCanonical ev_tm }
- -- EvCanonical: see Note [CallStack and ExecptionContext hack]
+ -- EvCanonical: see Note [CallStack and ExceptionContext hack]
-{- Note [CallStack and ExecptionContext hack]
+{- Note [CallStack and ExceptionContext hack]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It isn't really right that we treat CallStack and ExceptionContext dictionaries
as canonical, in the sense of Note [Coherence and specialisation: overview].
@@ -199,7 +199,7 @@ They definitely are not!
But if we use EvNonCanonical here we get lots of
nospec (error @Int) dict string
-(since `error` takes a HasCallStack dict), and that isn't bottomng (at least not
+(since `error` takes a HasCallStack dict), and that isn't bottoming (at least not
without extra work) So, hackily, we just say that HasCallStack and ExceptionContext
are canonical, even though they aren't really.
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2708,6 +2708,10 @@ and we want to get alpha := N b.
See also #15144, which was caused by unifying a representational
equality.
+Note that it does however make sense to perform such unifications, as a last
+resort, when doing top-level defaulting.
+See Note [Defaulting representational equalities].
+
Note [Solve by unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we solve
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -64,6 +64,8 @@ module GHC.Tc.Solver.Monad (
getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
tcLookupClass, tcLookupId, tcLookupTyCon,
+ getUnifiedRef,
+
-- Inerts
updInertSet, updInertCans,
@@ -98,7 +100,7 @@ module GHC.Tc.Solver.Monad (
instDFunType,
-- Unification
- wrapUnifierTcS, unifyFunDeps, uPairsTcM, unifyForAllBody,
+ wrapUnifierX, wrapUnifierTcS, unifyFunDeps, uPairsTcM, unifyForAllBody,
-- MetaTyVars
newFlexiTcSTy, instFlexiX,
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -3110,7 +3110,7 @@ mapCheck f xs
-----------------------------
-- | Options describing how to deal with a type equality
--- in the pure unifier. See 'checkTyEqRhs'
+-- in the eager unifier. See 'checkTyEqRhs'
data TyEqFlags m a
-- | LHS is a type family application; we are not unifying.
= TEFTyFam
=====================================
docs/users_guide/9.14.1-notes.rst
=====================================
@@ -40,6 +40,10 @@ Language
* Multiline strings are now accepted in foreign imports. (#25157)
+* GHC now does a better job at inferring types in calls to ``coerce``: instead of
+ complaining about ambiguous type variables, GHC will consider that such type
+ variables are determined by the ``Coercible`` constraints they appear in.
+
Compiler
~~~~~~~~
=====================================
testsuite/tests/default/default-fail08.hs
=====================================
@@ -1,12 +1,16 @@
--- | Default for a partially applied Coercible constraint doesn't trigger panic
+-- | Default for a partially applied constraint doesn't trigger panic
{-# LANGUAGE Haskell2010, ConstraintKinds, MultiParamTypeClasses, NamedDefaults #-}
-import Data.Coerce (Coercible, coerce)
import Data.Functor.Identity (Identity (Identity))
-type CoercibleFromInt = Coercible Int
+class C a b where
+ meth :: a -> b
+instance C Int Integer where
+ meth = fromIntegral
-default CoercibleFromInt (Identity Int)
+type CInt = C Int
-main = print (coerce (4 :: Int))
+default CInt (Integer)
+
+main = print (meth (4 :: Int))
=====================================
testsuite/tests/default/default-fail08.stderr
=====================================
@@ -1,7 +1,23 @@
+default-fail08.hs:16:8: error: [GHC-39999]
+ • Ambiguous type variable ‘a0’ arising from a use of ‘print’
+ prevents the constraint ‘(Show a0)’ from being solved.
+ Probable fix: use a type annotation to specify what ‘a0’ should be.
+ Potentially matching instances:
+ instance Show Ordering -- Defined in ‘GHC.Internal.Show’
+ instance Show Integer -- Defined in ‘GHC.Internal.Show’
+ ...plus 25 others
+ ...plus 15 instances involving out-of-scope types
+ (use -fprint-potential-instances to see them all)
+ • In the expression: print (meth (4 :: Int))
+ In an equation for ‘main’: main = print (meth (4 :: Int))
+
+default-fail08.hs:16:15: error: [GHC-39999]
+ • Ambiguous type variable ‘a0’ arising from a use of ‘meth’
+ prevents the constraint ‘(C Int a0)’ from being solved.
+ Probable fix: use a type annotation to specify what ‘a0’ should be.
+ Potentially matching instance:
+ instance C Int Integer -- Defined at default-fail08.hs:9:10
+ • In the first argument of ‘print’, namely ‘(meth (4 :: Int))’
+ In the expression: print (meth (4 :: Int))
+ In an equation for ‘main’: main = print (meth (4 :: Int))
-default-fail08.hs:12:15: [GHC-10283]
- Couldn't match representation of type ‘a0’ with that of ‘Int’
- arising from a use of ‘coerce’
- In the first argument of ‘print’, namely ‘(coerce (4 :: Int))’
- In the expression: print (coerce (4 :: Int))
- In an equation for ‘main’: main = print (coerce (4 :: Int))
=====================================
testsuite/tests/rep-poly/T14561b.stderr
=====================================
@@ -1,10 +1,10 @@
-
T14561b.hs:12:9: error: [GHC-55287]
• The first argument of ‘coerce’
does not have a fixed runtime representation.
Its type is:
- a0 :: TYPE k0
+ b0 :: TYPE k0
Cannot unify ‘r’ with the type variable ‘k0’
because the former is not a concrete ‘RuntimeRep’.
• In the expression: coerce
In an equation for ‘badId’: badId = coerce
+
=====================================
testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
=====================================
@@ -1,10 +1,10 @@
-
UnliftedNewtypesCoerceFail.hs:14:8: error: [GHC-55287]
• The first argument of ‘coerce’
does not have a fixed runtime representation.
Its type is:
- a0 :: TYPE k0
+ b0 :: TYPE k0
Cannot unify ‘rep’ with the type variable ‘k0’
because the former is not a concrete ‘RuntimeRep’.
• In the expression: coerce
In an equation for ‘goof’: goof = coerce
+
=====================================
testsuite/tests/typecheck/should_compile/T21003.hs
=====================================
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeApplications #-}
+
+module T21003 where
+
+import Data.IntMap (IntMap, mapKeysMonotonic, Key)
+import Data.Coerce (coerce)
+
+import Data.Functor.Compose (Compose(..))
+import Data.Functor.Const (Const(..))
+import Data.Foldable (sequence_)
+import Data.Monoid (Ap(..))
+
+-- Original example from #21003
+newtype MyMap = MyMap (IntMap Bool)
+shouldWork :: (Key -> Key) -> MyMap -> MyMap
+shouldWork = coerce mapKeysMonotonic
+
+-- Examples included in documentation
+
+-- 'foldMap' defined using 'traverse'
+foldMapUsingTraverse :: forall t m a. (Traversable t, Monoid m) => (a -> m) -> t a -> m
+foldMapUsingTraverse = coerce $ traverse @t @(Const m)
+
+-- 'traverse_' defined using 'foldMap'
+traverse_UsingFoldMap :: forall f t a. (Foldable t, Applicative f) => (a -> f ()) -> t a -> f ()
+traverse_UsingFoldMap = coerce $ foldMap @t @(Ap f ())
+
+-- 'sequence_', but for two nested 'Foldable' structures
+sequenceNested_ :: forall f1 f2. (Foldable f1, Foldable f2) => f1 (f2 (IO ())) -> IO ()
+sequenceNested_ = coerce $ sequence_ @(Compose f1 f2)
+
+-- Minimisation of an example from the 'vulkan' library
+newtype Size = Size Word
+test :: Size -> (Int -> ()) -> ()
+test sz f = f (fromIntegral $ coerce sz)
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -913,6 +913,7 @@ test('T23918', normal, compile, [''])
test('T17564', normal, compile, [''])
test('T24146', normal, compile, [''])
test('T22788', normal, compile, [''])
+test('T21003', normal, compile, [''])
test('T21206', normal, compile, [''])
test('T17594a', req_th, compile, [''])
test('T17594f', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T10495.hs
=====================================
@@ -1,5 +1,6 @@
module T10495 where
-import Data.Coerce
+class C a b where
+ meth :: a -> b
-foo = coerce
+foo = meth
=====================================
testsuite/tests/typecheck/should_fail/T10495.stderr
=====================================
@@ -1,8 +1,5 @@
+T10495.hs:6:7: error: [GHC-39999]
+ • No instance for ‘C a0 b0’ arising from a use of ‘meth’
+ • In the expression: meth
+ In an equation for ‘foo’: foo = meth
-T10495.hs:5:7: error: [GHC-10283]
- • Couldn't match representation of type ‘a0’ with that of ‘b0’
- arising from a use of ‘coerce’
- • In the expression: coerce
- In an equation for ‘foo’: foo = coerce
- • Relevant bindings include
- foo :: a0 -> b0 (bound at T10495.hs:5:1)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e53277af36d3f0b6ad5491f70ffc5593a49dcfd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e53277af36d3f0b6ad5491f70ffc5593a49dcfd
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/20250308/f5b873b8/attachment-0001.html>
More information about the ghc-commits
mailing list