[Git][ghc/ghc][wip/T25029] 2 commits: Don't introduce 'nospec' on the LHS of a RULE
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Aug 14 14:33:58 UTC 2024
Simon Peyton Jones pushed to branch wip/T25029 at Glasgow Haskell Compiler / GHC
Commits:
e6ffe039 by Simon Peyton Jones at 2024-08-14T15:33:27+01:00
Don't introduce 'nospec' on the LHS of a RULE
This patch address #25160. The main payload is:
* When desugaring the LHS of a RULE, do not introduce the `nospec` call
for non-canonical evidence. See GHC.Core.InstEnv
Note [Coherence and specialisation: overview]
The `nospec` call usually introdued in `dsHsWrapper`, but we don't want it
on the LHS of a RULE (that's what caused #25160). So now `dsHsWrapper` takes
a flag to say if it's on the LHS of a RULE. See wrinkle (NC1) in
`Note [Desugaring non-canonical evidence]` in GHC.HsToCore.Binds.
But I think this flag will go away again when I have finished with my
(entirely separate) speciaise-on-values patch (#24359).
All this meant I had to re-understand the `nospec` stuff and coherence, and
that in turn made me do some refactoring, and add a lot of new documentation
The big change is that in GHC.Core.InstEnv, I changed
the /type synonym/ `Canonical` into
a /data type/ `CanonicalEvidence`
and documented it a lot better.
That in turn made me realise that CalLStacks were being treated with a
bit of a hack, which I documented in `Note [CallStack and ExecptionContext hack]`.
- - - - -
b655485f by Simon Peyton Jones at 2024-08-14T15:33:27+01:00
Add defaulting of equalities
This MR adds one new defaulting strategy to the top-level
defaulting story: see Note [Defaulting equalities] in GHC.Tc.Solver.
This resolves #25029 and #25125, which showed that users were
accidentally relying on a GHC bug, which was fixed by
commit 04f5bb85c8109843b9ac2af2a3e26544d05e02f4
Author: Simon Peyton Jones <simon.peytonjones at gmail.com>
Date: Wed Jun 12 17:44:59 2024 +0100
Fix untouchability test
This MR fixes #24938. The underlying problem was tha the test for
"does this implication bring in scope any equalities" was plain wrong.
This fix gave rise to a number of user complaints; but the improved
defaulting story of this MR largely resolves them.
On the way I did a bit of refactoring, of course
* Completely restructure the extremely messy top-level defaulting
code. The new code is in GHC.Tc.Solver.tryDefaulting, and is much,
much, much esaier to grok.
- - - - -
25 changed files:
- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/indexed-types/should_compile/Simple14.hs
- − testsuite/tests/indexed-types/should_compile/Simple14.stderr
- testsuite/tests/indexed-types/should_compile/all.T
- + testsuite/tests/simplCore/should_compile/T25160.hs
- + testsuite/tests/simplCore/should_compile/T25160.stderr
- testsuite/tests/simplCore/should_compile/all.T
- + testsuite/tests/typecheck/should_compile/T25029.hs
- + testsuite/tests/typecheck/should_compile/T25125.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T21338.stderr
Changes:
=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -11,7 +11,7 @@ The bits common to GHC.Tc.TyCl.Instance and GHC.Tc.Deriv.
module GHC.Core.InstEnv (
DFunId, InstMatch, ClsInstLookupResult,
- Canonical, PotentialUnifiers(..), getPotentialUnifiers, nullUnifiers,
+ CanonicalEvidence(..), PotentialUnifiers(..), getCoherentUnifiers, nullUnifiers,
OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe,
ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprDFunId, pprInstances,
instanceWarning, instanceHead, instanceSig, mkLocalClsInst, mkImportedClsInst,
@@ -602,18 +602,22 @@ user manual simultaneously. The link may be this:
http://www.haskell.org/ghc/docs/latest/html/users_guide/glasgow_exts.html#instance-overlap
The willingness to be overlapped or incoherent is a property of the
-instance declaration itself, controlled as follows:
+instance declaration itself, controlled by its `OverlapMode`, as follows
- * An instance is "incoherent"
+ * An instance is "incoherent" (OverlapMode = `Incoherent` or `NonCanonical`)
if it has an `INCOHERENT` pragma, or
if it appears in a module compiled with `-XIncoherentInstances`.
+ In those cases:
+ -fspecialise-incoherents on => Incoherent
+ -fspecialise-incoherents off => NonCanonical
+ NB: it is on by default
- * An instance is "overlappable"
+ * An instance is "overlappable" (OverlapMode = `Overlappable` or `Overlaps`)
if it has an `OVERLAPPABLE` or `OVERLAPS` pragma, or
if it appears in a module compiled with `-XOverlappingInstances`, or
if the instance is incoherent.
- * An instance is "overlapping"
+ * An instance is "overlapping" (OverlapMode = `Overlapping` or `Overlaps`)
if it has an `OVERLAPPING` or `OVERLAPS` pragma, or
if it appears in a module compiled with `-XOverlappingInstances`, or
if the instance is incoherent.
@@ -640,19 +644,29 @@ of the target constraint (C ty1 .. tyn). The search works like this.
"either/or" design, rather than a "both/and" design, allow a
client to deliberately override an instance from a library,
without requiring a change to the library.)
+ This is done by `pruneOverlappingMatches`
(IL4) If all the remaining candidates are *incoherent*, the search succeeds,
returning an arbitrary surviving candidate.
+ If any coherent or non-canonical incoherent unifiers were discarded,
+ return NoUnifiers EvNonCanonical; if only canonical incoherent unifiers
+ were discarded, return NoUnifiers EvCanonical
+
(IL5) If more than one non-*incoherent* candidate remains, the search
fails. Otherwise there is exactly one non-*incoherent*
candidate; call it the "prime candidate".
(IL6) Now find all instances that unify with the target constraint,
but do not match it. Such non-candidate instances might match
- when the target constraint is further instantiated. If all of
- them are *incoherent* top-level instances, the search succeeds,
- returning the prime candidate. Otherwise the search fails.
+ when the target constraint is further instantiated.
+
+ If any are *coherent* (not incoherent) return them
+ as PotentialUnifiers.
+
+ If all are *incoherent* (OverlapFlag = Incoherent or NonCanonical)
+ return (NoUnifiers nc), where nc is EvNonCanonical if any of the discarded
+ unifiers are NonCanonical.
Notice that these rules are not influenced by flag settings in the
client module, where the instances are *used*. These rules make it
@@ -787,8 +801,11 @@ GHC's specialiser relies on the Coherence Assumption: that if
d1 :: C tys
d2 :: C tys
then the dictionary d1 can be used in place of d2 and vice versa; it is as if
-(C tys) is a singleton type. How do we guarantee this? Let's use this
-example
+(C tys) is a singleton type. If d1 and d2 are interchangeable, we say that
+they constitute /canonical evidence/ for (C tys). We have a special data type,
+`CanonoicalEvidence`, for recording whether evidence is canonical.
+
+Let's use this example
class C a where { op :: a -> Int }
instance C [a] where {...} -- (I1)
instance {-# OVERLAPPING #-} C [Int] where {...} -- (I2)
@@ -807,7 +824,7 @@ example
programmer can contrive, with some effort), all bets are off; we really
can't make any guarantees at all.
-* But what about [W] C [b], which might arise from
+* But what about [W] C [b]? This might arise from
risky :: b -> Int
risky x = op [x]
We can't pick (I2) because `b` is not Int. But if we pick (I1), and later
@@ -863,20 +880,22 @@ In short, sometimes we want to specialise on these incoherently-selected diction
and sometimes we don't. It would be best to have a per-instance pragma, but for now
we have a global flag:
-* If an instance has an `{-# INCOHERENT #-}` pragma, we use its `OverlapFlag` to
- label it as either
- * `Incoherent`: meaning incoherent but still specialisable, or
- * `NonCanonical`: meaning incoherent and not specialisable.
+* If an instance has an `{-# INCOHERENT #-}` pragma, we the `OverlapFlag` of the
+ `ClsInst` to label it as either
+ * `Incoherent`: meaning incoherent but still specialisable, or
+ * `NonCanonical`: meaning incoherent and not specialisable.
+ The module-wide `-fspecialise-incoherents` flag (on by default) determines
+ which choice is made.
-The module-wide `-fspecialise-incoherents` flag determines which
-choice is made. The rest of this note describes what happens for
-`NonCanonical` instances, i.e. with `-fno-specialise-incoherents`.
+ See GHC.Tc.Utils.Instantiate.getOverlapFlag.
+
+The rest of this note describes what happens for `NonCanonical`
+instances, i.e. with `-fno-specialise-incoherents`.
To avoid this incoherence breaking the specialiser,
-* We label as "non-canonical" the dictionary constructed by a
- (potentially) incoherent use of an instance declaration whose
- `OverlapFlag` is `NonCanonical`.
+* We label as "non-canonical" the dictionary constructed by a (potentially)
+ incoherent use of an ClsInst whose `OverlapFlag` is `NonCanonical`.
* We do not specialise a function if there is a non-canonical
dictionary in the /transistive dependencies/ of its dictionary
@@ -1016,22 +1035,42 @@ data LookupInstanceErrReason =
LookupInstErrNotFound
deriving (Generic)
-type Canonical = Bool
+-- | `CanonicalEvidence` says whether a piece of evidence has a singleton type;
+-- For example, given (d1 :: C Int), will any other (d2 :: C Int) do equally well?
+-- See Note [Coherence and specialisation: overview] above, and
+-- Note [Desugaring non-canonical evidence] in GHC.HsToCore.Binds
+data CanonicalEvidence
+ = EvCanonical
+ | EvNonCanonical
+
+andCanEv :: CanonicalEvidence -> CanonicalEvidence -> CanonicalEvidence
+-- Only canonical if both are
+andCanEv EvCanonical EvCanonical = EvCanonical
+andCanEv _ _ = EvNonCanonical
-- See Note [Recording coherence information in `PotentialUnifiers`]
-data PotentialUnifiers = NoUnifiers Canonical
- -- NoUnifiers True: We have a unique solution modulo canonicity
- -- NoUnifiers False: The solutions is not canonical, and thus
- -- we shouldn't specialise on it.
- | OneOrMoreUnifiers (NonEmpty ClsInst)
- -- This list is lazy as we only look at all the unifiers when
- -- printing an error message. It can be expensive to compute all
- -- the unifiers because if you are matching something like C a[sk] then
- -- all instances will unify.
+data PotentialUnifiers
+ = NoUnifiers CanonicalEvidence
+ -- Either there were no unifiers, or all were incoherent
+ --
+ -- NoUnifiers EvNonCanonical:
+ -- We discarded (via INCOHERENT) some instances that unify,
+ -- and that are marked NonCanonical; so the matching instance
+ -- should be traeated as EvNonCanonical
+ -- NoUnifiers EvCanonical:
+ -- We discarded no NonCanonical incoherent unifying instances,
+ -- so the matching instance can be treated as EvCanonical
+
+ | OneOrMoreUnifiers (NonEmpty ClsInst)
+ -- There are some /coherent/ unifiers; here they are
+ --
+ -- This list is lazy as we only look at all the unifiers when
+ -- printing an error message. It can be expensive to compute all
+ -- the unifiers because if you are matching something like C a[sk] then
+ -- all instances will unify.
{- Note [Recording coherence information in `PotentialUnifiers`]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
When we find a matching instance, there might be other instances that
could potentially unify with the goal. For `INCOHERENT` instances, we
don't care (see steps IL4 and IL6 in Note [Rules for instance
@@ -1047,18 +1086,23 @@ unifiers is empty, we record in `NoUnifiers` if the one solution is
`Canonical`.
-}
+instance Outputable CanonicalEvidence where
+ ppr EvCanonical = text "canonical"
+ ppr EvNonCanonical = text "non-canonical"
+
instance Outputable PotentialUnifiers where
- ppr (NoUnifiers c) = text "NoUnifiers" <+> if c then text "canonical" else text "non-canonical"
- ppr xs = ppr (getPotentialUnifiers xs)
+ ppr (NoUnifiers c) = text "NoUnifiers" <+> ppr c
+ ppr xs = ppr (getCoherentUnifiers xs)
instance Semigroup PotentialUnifiers where
- NoUnifiers c1 <> NoUnifiers c2 = NoUnifiers (c1 && c2)
+ NoUnifiers c1 <> NoUnifiers c2 = NoUnifiers (c1 `andCanEv` c2)
NoUnifiers _ <> u = u
- OneOrMoreUnifiers (unifier :| unifiers) <> u = OneOrMoreUnifiers (unifier :| (unifiers <> getPotentialUnifiers u))
+ OneOrMoreUnifiers (unifier :| unifiers) <> u
+ = OneOrMoreUnifiers (unifier :| (unifiers <> getCoherentUnifiers u))
-getPotentialUnifiers :: PotentialUnifiers -> [ClsInst]
-getPotentialUnifiers NoUnifiers{} = []
-getPotentialUnifiers (OneOrMoreUnifiers cls) = NE.toList cls
+getCoherentUnifiers :: PotentialUnifiers -> [ClsInst]
+getCoherentUnifiers NoUnifiers{} = []
+getCoherentUnifiers (OneOrMoreUnifiers cls) = NE.toList cls
nullUnifiers :: PotentialUnifiers -> Bool
nullUnifiers NoUnifiers{} = True
@@ -1081,7 +1125,7 @@ lookupInstEnv' :: InstEnv -- InstEnv to look in
-- giving a suitable error message
lookupInstEnv' (InstEnv rm) vis_mods cls tys
- = (foldr check_match [] rough_matches, check_unifier rough_unifiers)
+ = (foldr check_match [] rough_matches, check_unifiers rough_unifiers)
where
(rough_matches, rough_unifiers) = lookupRM' rough_tcs rm
rough_tcs = RML_KnownTc (className cls) : roughMatchTcsLookup tys
@@ -1094,29 +1138,23 @@ lookupInstEnv' (InstEnv rm) vis_mods cls tys
| Just subst <- tcMatchTys tpl_tys tys
= ((item, map (lookupTyVar subst) tpl_tvs) : acc)
+
| otherwise
= acc
+ check_unifiers :: [ClsInst] -> PotentialUnifiers
+ check_unifiers [] = NoUnifiers EvCanonical
+ check_unifiers (item at ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }:items)
- noncanonically_matched :: PotentialUnifiers -> PotentialUnifiers
- noncanonically_matched (NoUnifiers _) = NoUnifiers False
- noncanonically_matched u = u
-
- check_unifier :: [ClsInst] -> PotentialUnifiers
- check_unifier [] = NoUnifiers True
- check_unifier (item at ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }:items)
| not (instIsVisible vis_mods item)
- = check_unifier items -- See Note [Instance lookup and orphan instances]
- | Just {} <- tcMatchTys tpl_tys tys = check_unifier items
- -- Does not match, so next check whether the things unify
- -- See Note [Overlapping instances]
- -- Record that we encountered non-canonical instances: Note [Coherence and specialisation: overview]
- | isNonCanonical item
- = noncanonically_matched $ check_unifier items
- -- Ignore ones that are incoherent: Note [Incoherent instances]
- | isIncoherent item
- = check_unifier items
+ = check_unifiers items -- See Note [Instance lookup and orphan instances]
+ -- If it matches, check_match has gotten it, so skip over it here
+ | Just {} <- tcMatchTys tpl_tys tys
+ = check_unifiers items
+
+ -- Does not match, so next check whether the things unify
+ -- See Note [Overlapping instances]
| otherwise
= assertPpr (tys_tv_set `disjointVarSet` tpl_tv_set)
((ppr cls <+> ppr tys) $$
@@ -1128,16 +1166,30 @@ lookupInstEnv' (InstEnv rm) vis_mods cls tys
-- We consider MaybeApart to be a case where the instance might
-- apply in the future. This covers an instance like C Int and
-- a target like [W] C (F a), where F is a type family.
- SurelyApart -> check_unifier items
+ SurelyApart -> check_unifiers items
-- See Note [Infinitary substitution in lookup]
- MaybeApart MARInfinite _ -> check_unifier items
- _ ->
- OneOrMoreUnifiers (item :| getPotentialUnifiers (check_unifier items))
+ MaybeApart MARInfinite _ -> check_unifiers items
+ _ -> add_unifier item (check_unifiers items)
where
tpl_tv_set = mkVarSet tpl_tvs
tys_tv_set = tyCoVarsOfTypes tys
+ add_unifier :: ClsInst -> PotentialUnifiers -> PotentialUnifiers
+ -- Record that we encountered non-canonical instances:
+ -- Note [Coherence and specialisation: overview]
+ add_unifier item other_unifiers
+ | not (isIncoherent item)
+ = OneOrMoreUnifiers (item :| getCoherentUnifiers other_unifiers)
+
+ -- So `item` is incoherent; see Note [Incoherent instances]
+ | otherwise
+ = case other_unifiers of
+ OneOrMoreUnifiers{} -> other_unifiers
+ NoUnifiers{} | isNonCanonical item -> NoUnifiers EvNonCanonical
+ | otherwise -> other_unifiers
+
+
---------------
-- This is the common way to call this function.
lookupInstEnv :: Bool -- Check Safe Haskell overlap restrictions
@@ -1171,9 +1223,16 @@ lookupInstEnv check_overlap_safe
_ -> []
-- If the selected match is incoherent, discard all unifiers
+ -- See (IL4) of Note [Rules for instance lookup]
final_unifs = case final_matches of
- (m:_) | isIncoherent (fst m) -> NoUnifiers True
- _ -> all_unifs
+ (m:ms) | isIncoherent (fst m)
+ -- Incoherent match, so discard all unifiers, but
+ -- keep track of dropping coherent or non-canonical ones
+ -> assertPpr (null ms) (ppr final_matches) $
+ case all_unifs of
+ OneOrMoreUnifiers{} -> NoUnifiers EvNonCanonical
+ NoUnifiers{} -> all_unifs
+ _ -> all_unifs
-- Note [Safe Haskell isSafeOverlap]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1350,7 +1409,10 @@ noMatches = InstMatches { instMatches = [], instGuards = [] }
pruneOverlappedMatches :: [InstMatch] -> [InstMatch]
-- ^ Remove from the argument list any InstMatches for which another
-- element of the list is more specific, and overlaps it, using the
--- rules of Note [Rules for instance lookup]
+-- rules of Note [Rules for instance lookup], esp (IL3)
+--
+-- Incoherent instances are discarded, unless all are incoherent,
+-- in which case exactly one is kept.
pruneOverlappedMatches all_matches =
instMatches $ foldr insert_overlapping noMatches all_matches
@@ -1484,8 +1546,8 @@ it was only about the unify-check (Note [Overlapping instances]):
Example:
class C a b c where foo :: (a,b,c)
instance C [a] b Int
- instance [incoherent] [Int] b c
- instance [incoherent] C a Int c
+ instance {-# INCOHERENT #-} C [Int] b c
+ instance {-# INCOHERENT #-} C a Int c
Thanks to the incoherent flags,
[Wanted] C [a] b Int
works: Only instance one matches, the others just unify, but are marked
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -16,7 +16,8 @@ lower levels it is preserved with @let@/@letrec at s).
module GHC.HsToCore.Binds
( dsTopLHsBinds, dsLHsBinds, decomposeRuleLhs, dsSpec
- , dsHsWrapper, dsHsWrappers, dsEvTerm, dsTcEvBinds, dsTcEvBinds_s, dsEvBinds
+ , dsHsWrapper, dsHsWrappers
+ , dsEvTerm, dsTcEvBinds, dsTcEvBinds_s, dsEvBinds
, dsWarnOrphanRule
)
where
@@ -31,6 +32,8 @@ import GHC.Unit.Module
import {-# SOURCE #-} GHC.HsToCore.Expr ( dsLExpr )
import {-# SOURCE #-} GHC.HsToCore.Match ( matchWrapper )
+import GHC.HsToCore.Pmc.Utils( tracePm )
+
import GHC.HsToCore.Monad
import GHC.HsToCore.Errors.Types
import GHC.HsToCore.GuardedRHSs
@@ -41,7 +44,7 @@ import GHC.Hs -- lots of things
import GHC.Core -- lots of things
import GHC.Core.SimpleOpt ( simpleOptExpr )
import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr )
-import GHC.Core.InstEnv ( Canonical )
+import GHC.Core.InstEnv ( CanonicalEvidence(..) )
import GHC.Core.Make
import GHC.Core.Utils
import GHC.Core.Opt.Arity ( etaExpand )
@@ -837,7 +840,7 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl))
-- perhaps with the body of the lambda wrapped in some WpLets
-- E.g. /\a \(d:Eq a). let d2 = $df d in [] (Maybe a) d2
- ; dsHsWrapper spec_app $ \core_app -> do
+ ; dsHsWrapperForRuleLHS spec_app $ \core_app -> do
{ let ds_lhs = core_app (Var poly_id)
spec_ty = mkLamTypes spec_bndrs (exprType ds_lhs)
@@ -864,6 +867,12 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl))
; dsWarnOrphanRule rule
+ ; tracePm "dsSpec" (vcat
+ [ text "fun:" <+> ppr poly_id
+ , text "spec_co:" <+> ppr spec_co
+ , text "spec_bndrs:" <+> ppr spec_bndrs
+ , text "ds_lhs:" <+> ppr ds_lhs
+ , text "args:" <+> ppr rule_lhs_args ])
; return (Just (unitOL (spec_id, spec_rhs), rule))
-- NB: do *not* use makeCorePair on (spec_id,spec_rhs), because
-- makeCorePair overwrites the unfolding, which we have
@@ -1331,37 +1340,74 @@ inter-evidence dependency analysis to generate well-scoped
bindings. We then record this specialisability information in the
dsl_unspecables field of DsM's local environment.
+Wrinkle:
+
+(NC1) Don't do this in the LHS of a RULE. In paritcular, if we have
+ f :: (Num a, HasCallStack) => a -> a
+ {-# SPECIALISE f :: Int -> Int #-}
+ then making a rule like
+ RULE forall d1:Num Int, d2:HasCallStack.
+ f @Int d1 d2 = $sf
+ is pretty dodgy, because $sf won't get the call stack passed in d2.
+ But that's what you asked for in the SPECIALISE pragma, so we'll obey.
+
+ We definitely can't desugar that LHS into this!
+ nospec (f @Int d1) d2
+
+ Hence the `is_rule_lhs` flag in `ds_hs_wrapper`.
-}
+dsHsWrappers :: [HsWrapper] -> ([CoreExpr -> CoreExpr] -> DsM a) -> DsM a
+dsHsWrappers (wp:wps) k = dsHsWrapper wp $ \wrap -> dsHsWrappers wps $ \wraps -> k (wrap:wraps)
+dsHsWrappers [] k = k []
+
dsHsWrapper :: HsWrapper -> ((CoreExpr -> CoreExpr) -> DsM a) -> DsM a
-dsHsWrapper WpHole k = k $ \e -> e
-dsHsWrapper (WpTyApp ty) k = k $ \e -> App e (Type ty)
-dsHsWrapper (WpEvLam ev) k = k $ Lam ev
-dsHsWrapper (WpTyLam tv) k = k $ Lam tv
-dsHsWrapper (WpLet ev_binds) k = do { dsTcEvBinds ev_binds $ \bs -> do
- { k (mkCoreLets bs) } }
-dsHsWrapper (WpCompose c1 c2) k = do { dsHsWrapper c1 $ \w1 -> do
- { dsHsWrapper c2 $ \w2 -> do
- { k (w1 . w2) } } }
-dsHsWrapper (WpFun c1 c2 (Scaled w t1)) k -- See Note [Desugaring WpFun]
- = do { x <- newSysLocalDs w t1
- ; dsHsWrapper c1 $ \w1 -> do
- { dsHsWrapper c2 $ \w2 -> do
- { let app f a = mkCoreAppDs (text "dsHsWrapper") f a
- arg = w1 (Var x)
- ; k (\e -> (Lam x (w2 (app e arg)))) } } }
-dsHsWrapper (WpCast co) k = assert (coercionRole co == Representational) $
- k $ \e -> mkCastDs e co
-dsHsWrapper (WpEvApp tm) k = do { core_tm <- dsEvTerm tm
- ; unspecables <- getUnspecables
- ; let vs = exprFreeVarsList core_tm
- is_unspecable_var v = v `S.member` unspecables
- is_specable = not $ any (is_unspecable_var) vs -- See Note [Desugaring non-canonical evidence]
- ; k (\e -> app_ev is_specable e core_tm) }
+dsHsWrapper = ds_hs_wrapper False
+
+dsHsWrapperForRuleLHS :: HsWrapper -> ((CoreExpr -> CoreExpr) -> DsM a) -> DsM a
+dsHsWrapperForRuleLHS = ds_hs_wrapper True
+
+ds_hs_wrapper :: Bool -- True <=> LHS of a RULE
+ -- See (NC1) in Note [Desugaring non-canonical evidence]
+ -> HsWrapper
+ -> ((CoreExpr -> CoreExpr) -> DsM a)
+ -> DsM a
+ds_hs_wrapper is_rule_lhs wrap = go wrap
+ where
+ go WpHole k = k $ \e -> e
+ go (WpTyApp ty) k = k $ \e -> App e (Type ty)
+ go (WpEvLam ev) k = k $ Lam ev
+ go (WpTyLam tv) k = k $ Lam tv
+ go (WpCast co) k = assert (coercionRole co == Representational) $
+ k $ \e -> mkCastDs e co
+ go (WpLet ev_binds) k = dsTcEvBinds ev_binds $ \bs ->
+ k (mkCoreLets bs)
+ go (WpCompose c1 c2) k = go c1 $ \w1 ->
+ go c2 $ \w2 ->
+ k (w1 . w2)
+ go (WpFun c1 c2 st) k = -- See Note [Desugaring WpFun]
+ do { x <- newSysLocalDs st
+ ; go c1 $ \w1 ->
+ go c2 $ \w2 ->
+ let app f a = mkCoreAppDs (text "dsHsWrapper") f a
+ arg = w1 (Var x)
+ in k (\e -> (Lam x (w2 (app e arg)))) }
+ go (WpEvApp tm) k = do { core_tm <- dsEvTerm tm
+
+ -- See Note [Desugaring non-canonical evidence]
+ ; unspecables <- getUnspecables
+ ; let vs = exprFreeVarsList core_tm
+ is_unspecable_var v = v `S.member` unspecables
+ is_specable
+ | is_rule_lhs = True
+ | otherwise = not $ any (is_unspecable_var) vs
+
+ ; k (\e -> app_ev is_specable e core_tm) }
+
-- See Note [Coercions returned from tcSubMult] in GHC.Tc.Utils.Unify.
-dsHsWrapper (WpMultCoercion co) k = do { unless (isReflexiveCo co) $
- diagnosticDs DsMultiplicityCoercionsNotSupported
- ; k $ \e -> e }
+ go (WpMultCoercion co) k = do { unless (isReflexiveCo co) $
+ diagnosticDs DsMultiplicityCoercionsNotSupported
+ ; k $ \e -> e }
-- We are about to construct an evidence application `f dict`. If the dictionary is
-- non-specialisable, instead construct
@@ -1375,10 +1421,6 @@ app_ev is_specable k core_tm
| otherwise
= k `App` core_tm
-dsHsWrappers :: [HsWrapper] -> ([CoreExpr -> CoreExpr] -> DsM a) -> DsM a
-dsHsWrappers (wp:wps) k = dsHsWrapper wp $ \wrap -> dsHsWrappers wps $ \wraps -> k (wrap:wraps)
-dsHsWrappers [] k = k []
-
--------------------------------------
dsTcEvBinds_s :: [TcEvBinds] -> ([CoreBind] -> DsM a) -> DsM a
dsTcEvBinds_s [] k = k []
@@ -1399,18 +1441,19 @@ dsEvBinds ev_binds thing_inside
; let comps = sort_ev_binds ds_binds
; go comps thing_inside }
where
- go ::[SCC (Node EvVar (Canonical, CoreExpr))] -> ([CoreBind] -> DsM a) -> DsM a
+ go ::[SCC (Node EvVar (CanonicalEvidence, CoreExpr))] -> ([CoreBind] -> DsM a) -> DsM a
go (comp:comps) thing_inside
= do { unspecables <- getUnspecables
; let (core_bind, new_unspecables) = ds_component unspecables comp
- ; addUnspecables new_unspecables $ go comps $ \ core_binds -> thing_inside (core_bind:core_binds) }
+ ; addUnspecables new_unspecables $ go comps $ \ core_binds ->
+ thing_inside (core_bind:core_binds) }
go [] thing_inside = thing_inside []
ds_component unspecables (AcyclicSCC node) = (NonRec v rhs, new_unspecables)
where
((v, rhs), (this_canonical, deps)) = unpack_node node
- transitively_unspecable = not this_canonical || any is_unspecable deps
- is_unspecable dep = dep `S.member` unspecables
+ transitively_unspecable = is_unspecable this_canonical || any is_unspecable_dep deps
+ is_unspecable_dep dep = dep `S.member` unspecables
new_unspecables
| transitively_unspecable = S.singleton v
| otherwise = mempty
@@ -1419,7 +1462,8 @@ dsEvBinds ev_binds thing_inside
(pairs, direct_canonicity) = unzip $ map unpack_node nodes
is_unspecable_remote dep = dep `S.member` unspecables
- transitively_unspecable = or [ not this_canonical || any is_unspecable_remote deps | (this_canonical, deps) <- direct_canonicity ]
+ transitively_unspecable = or [ is_unspecable this_canonical || any is_unspecable_remote deps
+ | (this_canonical, deps) <- direct_canonicity ]
-- Bindings from a given SCC are transitively specialisable if
-- all are specialisable and all their remote dependencies are
-- also specialisable; see Note [Desugaring non-canonical evidence]
@@ -1428,19 +1472,24 @@ dsEvBinds ev_binds thing_inside
| transitively_unspecable = S.fromList [ v | (v, _) <- pairs]
| otherwise = mempty
- unpack_node DigraphNode { node_key = v, node_payload = (canonical, rhs), node_dependencies = deps } = ((v, rhs), (canonical, deps))
+ unpack_node DigraphNode { node_key = v, node_payload = (canonical, rhs), node_dependencies = deps }
+ = ((v, rhs), (canonical, deps))
+
+ is_unspecable :: CanonicalEvidence -> Bool
+ is_unspecable EvNonCanonical = True
+ is_unspecable EvCanonical = False
-sort_ev_binds :: Bag (Id, Canonical, CoreExpr) -> [SCC (Node EvVar (Canonical, CoreExpr))]
+sort_ev_binds :: Bag (Id, CanonicalEvidence, CoreExpr) -> [SCC (Node EvVar (CanonicalEvidence, CoreExpr))]
-- We do SCC analysis of the evidence bindings, /after/ desugaring
-- them. This is convenient: it means we can use the GHC.Core
-- free-variable functions rather than having to do accurate free vars
-- for EvTerm.
sort_ev_binds ds_binds = stronglyConnCompFromEdgedVerticesUniqR edges
where
- edges :: [ Node EvVar (Canonical, CoreExpr) ]
+ edges :: [ Node EvVar (CanonicalEvidence, CoreExpr) ]
edges = foldr ((:) . mk_node) [] ds_binds
- mk_node :: (Id, Canonical, CoreExpr) -> Node EvVar (Canonical, CoreExpr)
+ mk_node :: (Id, CanonicalEvidence, CoreExpr) -> Node EvVar (CanonicalEvidence, CoreExpr)
mk_node (var, canonical, rhs)
= DigraphNode { node_payload = (canonical, rhs)
, node_key = var
@@ -1451,11 +1500,11 @@ sort_ev_binds ds_binds = stronglyConnCompFromEdgedVerticesUniqR edges
-- is still deterministic even if the edges are in nondeterministic order
-- as explained in Note [Deterministic SCC] in GHC.Data.Graph.Directed.
-dsEvBind :: EvBind -> DsM (Id, Canonical, CoreExpr)
+dsEvBind :: EvBind -> DsM (Id, CanonicalEvidence, CoreExpr)
dsEvBind (EvBind { eb_lhs = v, eb_rhs = r, eb_info = info }) = do
e <- dsEvTerm r
let canonical = case info of
- EvBindGiven{} -> True
+ EvBindGiven{} -> EvCanonical
EvBindWanted{ ebi_canonical = canonical } -> canonical
return (v, canonical, e)
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1216,11 +1216,11 @@ addDeferredBinding ctxt err (EI { ei_evdest = Just dest, ei_pred = item_ty
; case dest of
EvVarDest evar
- -> addTcEvBind ev_binds_var $ mkWantedEvBind evar True err_tm
+ -> addTcEvBind ev_binds_var $ mkWantedEvBind evar EvNonCanonical err_tm
HoleDest hole
-> do { -- See Note [Deferred errors for coercion holes]
let co_var = coHoleCoVar hole
- ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var True err_tm
+ ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var EvNonCanonical err_tm
; fillCoercionHole hole (mkCoVarCo co_var) } }
addDeferredBinding _ _ _ = return () -- Do not set any evidence for Given
@@ -2260,7 +2260,7 @@ mk_dict_err ctxt (item, (matches, unifiers, unsafe_overlapped)) = case (NE.nonEm
-- Some matches => overlap errors
(Just matchesNE, Nothing) -> return $
- OverlappingInstances item (NE.map fst matchesNE) (getPotentialUnifiers unifiers)
+ OverlappingInstances item (NE.map fst matchesNE) (getCoherentUnifiers unifiers)
(Just (match :| []), Just unsafe_overlappedNE) -> return $
UnsafeOverlap item (fst match) (NE.map fst unsafe_overlappedNE)
@@ -2330,7 +2330,7 @@ mk_dict_err ctxt (item, (matches, unifiers, unsafe_overlapped)) = case (NE.nonEm
cannot_resolve_msg :: ErrorItem -> [ClsInst] -> RelevantBindings
-> [ImportError] -> [GhcHint] -> TcSolverReportMsg
cannot_resolve_msg item candidate_insts binds imp_errs field_suggestions
- = CannotResolveInstance item (getPotentialUnifiers unifiers) candidate_insts imp_errs field_suggestions binds
+ = CannotResolveInstance item (getCoherentUnifiers unifiers) candidate_insts imp_errs field_suggestions binds
{- Note [Report candidate instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -1931,7 +1931,7 @@ reifyInstances' th_nm th_tys
-> do { inst_envs <- tcGetInstEnvs
; let (matches, unifies, _) = lookupInstEnv False inst_envs cls tys
; traceTc "reifyInstances'1" (ppr matches)
- ; return $ Left (cls, map fst matches ++ getPotentialUnifiers unifies) }
+ ; return $ Left (cls, map fst matches ++ getCoherentUnifiers unifies) }
| isOpenFamilyTyCon tc
-> do { inst_envs <- tcGetFamInstEnvs
; let matches = lookupFamInstEnv inst_envs tc tys
=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -106,10 +106,11 @@ data ClsInstResult
| OneInst { cir_new_theta :: [TcPredType]
, cir_mk_ev :: [EvExpr] -> EvTerm
- , cir_canonical :: Canonical -- cir_canonical=True => you can specialise on this instance
- -- cir_canonical= False => you cannot specialise on this instance
- -- (its OverlapFlag is NonCanonical)
- -- See Note [Coherence and specialisation: overview]
+ , cir_canonical :: CanonicalEvidence
+ -- cir_canonical=EvCanonical => you can specialise on this instance
+ -- cir_canonical=EvNonCanonical => you cannot specialise on this instance
+ -- (its OverlapFlag is NonCanonical)
+ -- See Note [Coherence and specialisation: overview]
, cir_what :: InstanceWhat }
| NotSure -- Multiple matches and/or one or more unifiers
@@ -194,7 +195,7 @@ matchInstEnv dflags short_cut_solver clas tys
-> do { let dfun_id = instanceDFunId ispec
warn = instanceWarning ispec
; traceTc "matchClass success" $
- vcat [text "dict" <+> ppr pred <+> parens (if canonical then text "canonical" else text "non-canonical"),
+ vcat [text "dict" <+> ppr pred <+> ppr canonical,
text "witness" <+> ppr dfun_id
<+> ppr (idType dfun_id) ]
-- Record that this dfun is needed
@@ -209,7 +210,7 @@ matchInstEnv dflags short_cut_solver clas tys
where
pred = mkClassPred clas tys
-match_one :: SafeOverlapping -> Canonical -> DFunId -> [DFunInstType]
+match_one :: SafeOverlapping -> CanonicalEvidence -> DFunId -> [DFunInstType]
-> Maybe (WarningTxt GhcRn) -> TcM ClsInstResult
match_one so canonical dfun_id mb_inst_tys warn
= do { traceTc "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
@@ -254,7 +255,7 @@ matchCTuple :: Class -> [Type] -> TcM ClsInstResult
matchCTuple clas tys -- (isCTupleClass clas) holds
= return (OneInst { cir_new_theta = tys
, cir_mk_ev = tuple_ev
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinInstance })
-- The dfun *is* the data constructor!
where
@@ -418,7 +419,7 @@ makeLitDict clas ty et
, let ev_tm = mkEvCast et (mkSymCo (mkTransCo co_dict co_rep))
= return $ OneInst { cir_new_theta = []
, cir_mk_ev = \_ -> ev_tm
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinInstance }
| otherwise
@@ -467,7 +468,7 @@ matchWithDict [cls, mty]
; return $ OneInst { cir_new_theta = [mkPrimEqPred mty inst_meth_ty]
, cir_mk_ev = mk_ev
- , cir_canonical = False -- See (WD6) in Note [withDict]
+ , cir_canonical = EvNonCanonical -- See (WD6) in Note [withDict]
, cir_what = BuiltinInstance }
}
@@ -938,7 +939,7 @@ matchDataToTag dataToTagClass [levity, dty] = do
-> addUsedDataCons rdr_env repTyCon -- See wrinkles DTW2 and DTW3
$> OneInst { cir_new_theta = [] -- (Ignore stupid theta.)
, cir_mk_ev = mk_ev
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinInstance
}
| otherwise -> pure NoInstance
@@ -989,7 +990,7 @@ doFunTy :: Class -> Type -> Mult -> Type -> Type -> TcM ClsInstResult
doFunTy clas ty mult arg_ty ret_ty
= return $ OneInst { cir_new_theta = preds
, cir_mk_ev = mk_ev
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinInstance }
where
preds = map (mk_typeable_pred clas) [mult, arg_ty, ret_ty]
@@ -1006,7 +1007,7 @@ doTyConApp clas ty tc kind_args
| tyConIsTypeable tc
= return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) kind_args
, cir_mk_ev = mk_ev
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinTypeableInstance tc }
| otherwise
= return NoInstance
@@ -1038,7 +1039,7 @@ doTyApp clas ty f tk
| otherwise
= return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk]
, cir_mk_ev = mk_ev
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinInstance }
where
mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
@@ -1059,7 +1060,7 @@ doTyLit kc t = do { kc_clas <- tcLookupClass kc
mk_ev _ = panic "doTyLit"
; return (OneInst { cir_new_theta = [kc_pred]
, cir_mk_ev = mk_ev
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinInstance }) }
{- Note [Typeable (T a b c)]
@@ -1300,7 +1301,7 @@ matchHasField dflags short_cut clas tys
-- See Note [Detecting incomplete record selectors] in GHC.HsToCore.Pmc
; return OneInst { cir_new_theta = theta
, cir_mk_ev = mk_ev
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = BuiltinInstance } }
else matchInstEnv dflags short_cut clas tys }
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -34,6 +34,7 @@ import GHC.Core.Class
import GHC.Core
import GHC.Core.DataCon
import GHC.Core.Make
+import GHC.Core.Coercion( mkNomReflCo )
import GHC.Driver.DynFlags
import GHC.Data.FastString
import GHC.Data.List.SetOps
@@ -49,7 +50,8 @@ import GHC.Tc.Types.Evidence
import GHC.Tc.Solver.Solve ( solveSimpleGivens, solveSimpleWanteds )
import GHC.Tc.Solver.Dict ( makeSuperClasses, solveCallStack )
import GHC.Tc.Solver.Rewrite ( rewriteType )
-import GHC.Tc.Utils.Unify ( buildTvImplication )
+import GHC.Tc.Utils.Unify ( buildTvImplication, touchabilityAndShapeTest
+ , simpleUnifyCheck, UnifyCheckCaller(..) )
import GHC.Tc.Utils.TcMType as TcM
import GHC.Tc.Utils.Monad as TcM
import GHC.Tc.Zonk.TcType as TcM
@@ -84,7 +86,7 @@ import Data.Foldable ( toList, traverse_ )
import Data.List ( partition )
import Data.List.NonEmpty ( NonEmpty(..), nonEmpty )
import qualified Data.List.NonEmpty as NE
-import GHC.Data.Maybe ( mapMaybe, runMaybeT, MaybeT )
+import GHC.Data.Maybe ( isJust, mapMaybe, )
{-
*********************************************************************************
@@ -493,76 +495,70 @@ report_unsolved_equalities skol_info_anon skol_tvs tclvl wanted
-- | Simplify top-level constraints, but without reporting any unsolved
-- constraints nor unsafe overlapping.
simplifyTopWanteds :: WantedConstraints -> TcS WantedConstraints
- -- See Note [Top-level Defaulting Plan]
simplifyTopWanteds wanteds
- = do { wc_first_go <- nestTcS (solveWanteds wanteds)
- -- This is where the main work happens
- ; dflags <- getDynFlags
- ; wc_defaulted <- try_tyvar_defaulting dflags wc_first_go
-
- -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors,
- -- point (C).
- ; useUnsatisfiableGivens wc_defaulted }
- where
- try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints
- try_tyvar_defaulting dflags wc
- | isEmptyWC wc
- = return wc
- | insolubleWC wc
- , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles]
- = try_class_defaulting wc
- | otherwise
- = do { -- Need to zonk first, as the WantedConstraints are not yet zonked.
- ; free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
- ; let defaultable_tvs = filter can_default free_tvs
- can_default tv
- = isTyVar tv
- -- Weed out coercion variables.
-
- && isMetaTyVar tv
- -- Weed out runtime-skolems in GHCi, which we definitely
- -- shouldn't try to default.
-
- && not (tv `elemVarSet` nonDefaultableTyVarsOfWC wc)
- -- Weed out variables for which defaulting would be unhelpful,
- -- e.g. alpha appearing in [W] alpha[conc] ~# rr[sk].
-
- ; defaulted <- mapM defaultTyVarTcS defaultable_tvs -- Has unification side effects
- ; if or defaulted
- then do { wc_residual <- nestTcS (solveWanteds wc)
- -- See Note [Must simplify after defaulting]
- ; try_class_defaulting wc_residual }
- else try_class_defaulting wc } -- No defaulting took place
-
- try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
- try_class_defaulting wc
- | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles]
- = try_callstack_defaulting wc
- | otherwise -- See Note [When to do type-class defaulting]
- = do { something_happened <- applyDefaultingRules wc
- -- See Note [Top-level Defaulting Plan]
- ; if something_happened
- then do { wc_residual <- nestTcS (solveWanteds wc)
- ; try_class_defaulting wc_residual }
- -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
- else try_callstack_defaulting wc }
-
- try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints
- try_callstack_defaulting wc
- = defaultConstraints [defaultCallStack, defaultExceptionContext] wc
-
--- | If an implication contains a Given of the form @Unsatisfiable msg@, use
--- it to solve all Wanteds within the implication.
+ = do { -- Solve the constraints
+ wc_first_go <- nestTcS (solveWanteds wanteds)
+
+ -- Now try defaulting:
+ -- see Note [Top-level Defaulting Plan]
+ ; tryDefaulting wc_first_go }
+
+--------------------------
+tryDefaulting :: WantedConstraints -> TcS WantedConstraints
+tryDefaulting wc
+ = do { dflags <- getDynFlags
+ ; traceTcS "tryDefaulting:before" (ppr wc)
+ ; wc1 <- tryTyVarDefaulting dflags wc
+ ; wc2 <- tryConstraintDefaulting wc1
+ ; wc3 <- tryTypeClassDefaulting wc2
+ ; wc4 <- tryUnsatisfiableGivens wc3
+ ; traceTcS "tryDefaulting:after" (ppr wc)
+ ; return wc4 }
+
+solveAgainIf :: Bool -> WantedConstraints -> TcS WantedConstraints
+-- If the Bool is true, solve the wanted constraints again
+-- See Note [Must simplify after defaulting]
+solveAgainIf False wc = return wc
+solveAgainIf True wc = nestTcS (solveWanteds wc)
+
+--------------------------
+tryTyVarDefaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints
+tryTyVarDefaulting dflags wc
+ | isEmptyWC wc
+ = return wc
+ | insolubleWC wc
+ , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles]
+ = return wc
+ | otherwise
+ = do { -- Need to zonk first, as the WantedConstraints are not yet zonked.
+ ; free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
+ ; let defaultable_tvs = filter can_default free_tvs
+ can_default tv
+ = isTyVar tv
+ -- Weed out coercion variables.
+
+ && isMetaTyVar tv
+ -- Weed out runtime-skolems in GHCi, which we definitely
+ -- shouldn't try to default.
+
+ && not (tv `elemVarSet` nonDefaultableTyVarsOfWC wc)
+ -- Weed out variables for which defaulting would be unhelpful,
+ -- e.g. alpha appearing in [W] alpha[conc] ~# rr[sk].
+
+ ; unification_s <- mapM defaultTyVarTcS defaultable_tvs -- Has unification side effects
+ ; solveAgainIf (or unification_s) wc }
+ -- solveAgainIf: see Note [Must simplify after defaulting]
+
+----------------------------
+-- | If an implication contains a Given of the form @Unsatisfiable msg@,
+-- use it to solve all Wanteds within the implication.
+-- See point (C) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
--
-- This does a complete walk over the implication tree.
---
--- See point (C) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
-useUnsatisfiableGivens :: WantedConstraints -> TcS WantedConstraints
-useUnsatisfiableGivens wc =
+tryUnsatisfiableGivens :: WantedConstraints -> TcS WantedConstraints
+tryUnsatisfiableGivens wc =
do { (final_wc, did_work) <- (`runStateT` False) $ go_wc wc
- ; if did_work
- then nestTcS (solveWanteds final_wc)
- else return final_wc }
+ ; solveAgainIf did_work final_wc }
where
go_wc (WC { wc_simple = wtds, wc_impl = impls, wc_errors = errs })
= do impls' <- mapMaybeBagM go_impl impls
@@ -612,7 +608,7 @@ solveImplicationUsingUnsatGiven
go_simple ct = case ctEvidence ct of
CtWanted { ctev_pred = pty, ctev_dest = dst }
-> do { ev_expr <- unsatisfiableEvExpr unsat_given pty
- ; setWantedEvTerm dst True $ EvExpr ev_expr }
+ ; setWantedEvTerm dst EvNonCanonical $ EvExpr ev_expr }
_ -> return ()
-- | Create an evidence expression for an arbitrary constraint using
@@ -694,69 +690,122 @@ This allows us to indirectly box constraints with different representations
(such as primitive equality constraints).
-}
--- | A 'TcS' action which can may default a 'Ct'.
-type CtDefaultingStrategy = Ct -> MaybeT TcS ()
+-- | A 'TcS' action which can may solve a `Ct`
+type CtDefaultingStrategy = Ct -> TcS Bool
+ -- True <=> I solved the constraint
+
+--------------------------------
+tryConstraintDefaulting :: WantedConstraints -> TcS WantedConstraints
+-- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
+tryConstraintDefaulting wc
+ | isEmptyWC wc
+ = return wc
+ | otherwise
+ = do { (n_unifs, better_wc) <- reportUnifications (go_wc wc)
+ -- We may have done unifications; so solve again
+ ; solveAgainIf (n_unifs > 0) better_wc }
+ where
+ go_wc :: WantedConstraints -> TcS WantedConstraints
+ go_wc wc@(WC { wc_simple = simples, wc_impl = implics })
+ = do { mb_simples <- mapMaybeBagM go_simple simples
+ ; mb_implics <- mapMaybeBagM go_implic implics
+ ; return (wc { wc_simple = mb_simples, wc_impl = mb_implics }) }
+
+ go_simple :: Ct -> TcS (Maybe Ct)
+ go_simple ct = do { solved <- tryCtDefaultingStrategy ct
+ ; if solved then return Nothing
+ else return (Just ct) }
+
+ go_implic :: Implication -> TcS (Maybe Implication)
+ -- The Maybe is because solving the CallStack constraint
+ -- may well allow us to discard the implication entirely
+ go_implic implic
+ | isSolvedStatus (ic_status implic)
+ = return (Just implic) -- Nothing to solve inside here
+ | otherwise
+ = do { wanteds <- setEvBindsTcS (ic_binds implic) $
+ -- defaultCallStack sets a binding, so
+ -- we must set the correct binding group
+ go_wc (ic_wanted implic)
+ ; setImplicationStatus (implic { ic_wanted = wanteds }) }
+
+tryCtDefaultingStrategy :: CtDefaultingStrategy
+-- The composition of all the CtDefaultingStrategies we want
+tryCtDefaultingStrategy
+ = foldr1 combineStrategies
+ [ defaultCallStack
+ , defaultExceptionContext
+ , defaultEquality ]
-- | Default @ExceptionContext@ constraints to @emptyExceptionContext at .
defaultExceptionContext :: CtDefaultingStrategy
defaultExceptionContext ct
- = do { ClassPred cls tys <- pure $ classifyPredType (ctPred ct)
- ; Just {} <- pure $ isExceptionContextPred cls tys
- ; emptyEC <- Var <$> lift (lookupId emptyExceptionContextName)
+ | ClassPred cls tys <- classifyPredType (ctPred ct)
+ , isJust (isExceptionContextPred cls tys)
+ = do { warnTcS $ TcRnDefaultedExceptionContext (ctLoc ct)
+ ; empty_ec_id <- lookupId emptyExceptionContextName
; let ev = ctEvidence ct
- ; let ev_tm = mkEvCast emptyEC (wrapIP (ctEvPred ev))
- ; lift $ warnTcS $ TcRnDefaultedExceptionContext (ctLoc ct)
- ; lift $ setEvBindIfWanted ev False ev_tm
- }
+ ev_tm = mkEvCast (Var empty_ec_id) (wrapIP (ctEvPred ev))
+ ; setEvBindIfWanted ev EvCanonical ev_tm
+ -- EvCanonical: see Note [CallStack and ExecptionContext hack]
+ -- in GHC.Tc.Solver.Dict
+ ; return True }
+ | otherwise
+ = return False
-- | Default any remaining @CallStack@ constraints to empty @CallStack at s.
-- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
defaultCallStack :: CtDefaultingStrategy
defaultCallStack ct
- = do { ClassPred cls tys <- pure $ classifyPredType (ctPred ct)
- ; Just {} <- pure $ isCallStackPred cls tys
- ; lift $ solveCallStack (ctEvidence ct) EvCsEmpty
- }
-
-defaultConstraints :: [CtDefaultingStrategy]
- -> WantedConstraints
- -> TcS WantedConstraints
--- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
-defaultConstraints defaulting_strategies wanteds
- | isEmptyWC wanteds = return wanteds
+ | ClassPred cls tys <- classifyPredType (ctPred ct)
+ , isJust (isCallStackPred cls tys)
+ = do { solveCallStack (ctEvidence ct) EvCsEmpty
+ ; return True }
| otherwise
- = do simples <- handle_simples (wc_simple wanteds)
- mb_implics <- mapBagM handle_implic (wc_impl wanteds)
- return (wanteds { wc_simple = simples
- , wc_impl = catBagMaybes mb_implics })
+ = return False
+defaultEquality :: CtDefaultingStrategy
+-- See Note [Defaulting equalities]
+defaultEquality ct
+ | EqPred NomEq ty1 ty2 <- classifyPredType (ctPred ct)
+ , Just tv1 <- getTyVar_maybe ty1
+ = do { -- Remember: `ct` may not be zonked;
+ -- see (DE3) in Note [Defaulting equalities]
+ z_ty1 <- TcS.zonkTcTyVar tv1
+ ; z_ty2 <- TcS.zonkTcType ty2
+ ; case getTyVar_maybe z_ty1 of
+ Just z_tv1 | defaultable z_tv1 z_ty2
+ -> do { default_tv z_tv1 z_ty2
+ ; return True }
+ _ -> return False }
+ | otherwise
+ = return False
where
- handle_simples :: Bag Ct -> TcS (Bag Ct)
- handle_simples simples
- = catBagMaybes <$> mapBagM handle_simple simples
- where
- handle_simple :: Ct -> TcS (Maybe Ct)
- handle_simple ct = go defaulting_strategies
- where
- go [] = return (Just ct)
- go (f:fs) = do
- mb <- runMaybeT (f ct)
- case mb of
- Just () -> return Nothing
- Nothing -> go fs
-
- handle_implic :: Implication -> TcS (Maybe Implication)
- -- The Maybe is because solving the CallStack constraint
- -- may well allow us to discard the implication entirely
- handle_implic implic
- | isSolvedStatus (ic_status implic)
- = return (Just implic)
- | otherwise
- = do { wanteds <- setEvBindsTcS (ic_binds implic) $
- -- defaultCallStack sets a binding, so
- -- we must set the correct binding group
- defaultConstraints defaulting_strategies (ic_wanted implic)
- ; setImplicationStatus (implic { ic_wanted = wanteds }) }
+ defaultable tv1 ty2
+ = -- Do the standard unification checks;
+ -- c.f. uUnfilledVar2 in GHC.Tc.Utils.Unify
+ -- EXCEPT drop the untouchability test
+ tyVarKind tv1 `tcEqType` typeKind ty2
+ && touchabilityAndShapeTest topTcLevel tv1 ty2
+ -- topTcLevel makes the untoucability test vacuous,
+ -- which is the Whole Point of `defaultEquality`
+ -- See (DE2) in Note [Defaulting equalities]
+ && simpleUnifyCheck UC_Defaulting tv1 ty2
+
+ default_tv tv1 ty2
+ = do { unifyTyVar tv1 ty2 -- NB: unifyTyVar adds to the
+ -- TcS unification counter
+ ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
+ evCoercion (mkNomReflCo ty2) }
+
+combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy
+combineStrategies default1 default2 ct
+ = do { solved <- default1 ct
+ ; case solved of
+ True -> return True -- default1 solved it!
+ False -> default2 ct -- default1 failed, try default2
+ }
+
{- Note [When to do type-class defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -785,6 +834,56 @@ Another potential alternative would be to suppress *all* non-insoluble
errors if there are *any* insoluble errors, anywhere, but that seems
too drastic.
+Note [Defaulting 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
+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:
+
+ * 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 top-level defaulting, we already do several other somewhat-ad-hoc,
+but terribly convenient, unifications. This is just one more.
+
+Wrinkles:
+
+(DE1) Note carefully that this does not threaten principal type. The original
+ worry about unifying untouchable type variables was this:
+
+ data T a where
+ T1 :: T Bool
+ 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 te otehr
+
+(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.
+
+(DE3) The contraint we are looking at may not be fully zonked; for example,
+ an earlier deafaulting might have affected it. So we zonk-on-the fly in
+ `defaultEquality`.
+
Note [Don't default in syntactic equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When there are unsolved syntactic equalities such as
@@ -1025,11 +1124,12 @@ last example above.
------------------
simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
-simplifyAmbiguityCheck ty wanteds
+simplifyAmbiguityCheck ty wc
= do { traceTc "simplifyAmbiguityCheck {" $
- text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds
+ text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wc
- ; (final_wc, _) <- runTcS $ useUnsatisfiableGivens =<< solveWanteds wanteds
+ ; (final_wc, _) <- runTcS $ do { wc1 <- solveWanteds wc
+ ; tryUnsatisfiableGivens wc1 }
-- NB: no defaulting! See Note [No defaulting in the ambiguity check]
-- Note: we do still use Unsatisfiable Givens to solve Wanteds,
-- see Wrinkle [Ambiguity] under point (C) of
@@ -2879,11 +2979,11 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication)
-- setting the ic_status field
-- Precondition: the ic_status field is not already IC_Solved
-- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_status = status
+setImplicationStatus implic@(Implic { ic_status = old_status
, ic_info = info
, ic_wanted = wc
, ic_given = givens })
- | assertPpr (not (isSolvedStatus status)) (ppr info) $
+ | assertPpr (not (isSolvedStatus old_status)) (ppr info) $
-- Precondition: we only set the status if it is not already solved
not (isSolvedWC pruned_wc)
= do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
@@ -3387,28 +3487,34 @@ The constraint in f's signature is redundant; not used to typecheck
be an ambiguous variable in `g`.
-}
+type UnificationDone = Bool
+
+noUnification, didUnification :: UnificationDone
+noUnification = False
+didUnification = True
+
-- | Like 'defaultTyVar', but in the TcS monad.
-defaultTyVarTcS :: TcTyVar -> TcS Bool
+defaultTyVarTcS :: TcTyVar -> TcS UnificationDone
defaultTyVarTcS the_tv
| isTyVarTyVar the_tv
-- TyVarTvs should only be unified with a tyvar
-- never with a type; c.f. GHC.Tc.Utils.TcMType.defaultTyVar
-- and Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
- = return False
+ = return noUnification
| isRuntimeRepVar the_tv
= do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
; unifyTyVar the_tv liftedRepTy
- ; return True }
+ ; return didUnification }
| isLevityVar the_tv
= do { traceTcS "defaultTyVarTcS Levity" (ppr the_tv)
; unifyTyVar the_tv liftedDataConTy
- ; return True }
+ ; return didUnification }
| isMultiplicityVar the_tv
= do { traceTcS "defaultTyVarTcS Multiplicity" (ppr the_tv)
; unifyTyVar the_tv ManyTy
- ; return True }
+ ; return didUnification }
| otherwise
- = return False -- the common case
+ = return noUnification -- the common case
approximateWC :: Bool -- See Wrinkle (W3) in Note [ApproximateWC]
-> WantedConstraints
@@ -3646,14 +3752,20 @@ Wrinkle (DP2): Interactions between defaulting mechanisms
-}
+tryTypeClassDefaulting :: WantedConstraints -> TcS WantedConstraints
+tryTypeClassDefaulting wc
+ | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles]
+ = return wc
+ | otherwise -- See Note [When to do type-class defaulting]
+ = do { something_happened <- applyDefaultingRules wc
+ -- See Note [Top-level Defaulting Plan]
+ ; solveAgainIf something_happened wc }
+
applyDefaultingRules :: WantedConstraints -> TcS Bool
-- True <=> I did some defaulting, by unifying a meta-tyvar
-- Input WantedConstraints are not necessarily zonked
applyDefaultingRules wanteds
- | isEmptyWC wanteds
- = return False
- | otherwise
= do { info@(default_tys, _) <- getDefaultInfo
; wanteds <- TcS.zonkWC wanteds
@@ -3682,8 +3794,10 @@ applyDefaultingRules wanteds
; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
; return $ or something_happeneds || or plugin_defaulted }
- where run_defaulting_plugin wanteds p =
- do { groups <- runTcPluginTcS (p wanteds)
+
+ where
+ run_defaulting_plugin wanteds p
+ = do { groups <- runTcPluginTcS (p wanteds)
; defaultedGroups <-
filterM (\g -> disambigMultiGroup
wanteds
@@ -3699,9 +3813,7 @@ applyDefaultingRules wanteds
-- 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)
- }
-
+ return (wanteds', True) }
findDefaultableGroups
:: ( [Type]
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -189,11 +189,23 @@ solveCallStack ev ev_cs
-- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
= do { cs_tm <- evCallStack ev_cs
; let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
- ; setEvBindIfWanted ev True ev_tm }
-
-
-{- Note [Shadowing of implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ ; setEvBindIfWanted ev EvCanonical ev_tm }
+ -- EvCanonical: see Note [CallStack and ExecptionContext hack]
+
+{- Note [CallStack and ExecptionContext hack]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It isn't really right thta we treat CallStack and ExceptionContext dictionaries
+as canonical, in the sense of Note [Coherence and specialisation: overview].
+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
+without extra work) So, hackily, we just say that HasCallStack and ExceptionContext
+are canonical, even though they aren't really.
+
+Note [Shadowing of implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we add a new /given/ implicit parameter to the inert set, it /replaces/
any existing givens for the same implicit parameter. This makes a difference
in two places:
@@ -411,7 +423,7 @@ solveEqualityDict ev cls tys
; (co, _, _) <- wrapUnifierTcS ev role $ \uenv ->
uType uenv t1 t2
-- Set d :: (t1~t2) = Eq# co
- ; setWantedEvTerm dest True $
+ ; setWantedEvTerm dest EvCanonical $
evDataConApp data_con tys [Coercion co]
; stopWith ev "Solved wanted lifted equality" }
@@ -732,10 +744,10 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys
-- the inert from the work-item or vice-versa.
; case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of
KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr dict_w)
- ; setEvBindIfWanted ev_w True (ctEvTerm ev_i)
+ ; setEvBindIfWanted ev_w EvCanonical (ctEvTerm ev_i)
; return $ Stop ev_w (text "Dict equal" <+> ppr dict_w) }
KeepWork -> do { traceTcS "lookupInertDict:KeepWork" (ppr dict_w)
- ; setEvBindIfWanted ev_i True (ctEvTerm ev_w)
+ ; setEvBindIfWanted ev_i EvCanonical (ctEvTerm ev_w)
; updInertCans (updDicts $ delDict dict_w)
; continueWith () } } }
@@ -868,7 +880,7 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
-- See Note [No Given/Given fundeps]
| Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
- = do { setEvBindIfWanted ev True (ctEvTerm solved_ev)
+ = do { setEvBindIfWanted ev EvCanonical (ctEvTerm solved_ev)
; stopWith ev "Dict/Top (cached)" }
| otherwise -- Wanted, but not cached
@@ -1143,7 +1155,7 @@ matchLocalInst pred loc
->
do { let result = OneInst { cir_new_theta = theta
, cir_mk_ev = evDFunApp dfun_id tys
- , cir_canonical = True
+ , cir_canonical = EvCanonical
, cir_what = LocalInstance }
; traceTcS "Best local instance found:" $
vcat [ text "pred:" <+> ppr pred
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -350,7 +350,7 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
-- Literals
can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
| l1 == l2
- = do { setEvBindIfWanted ev True (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
+ = do { setEvBindIfWanted ev EvCanonical (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
; stopWith ev "Equal LitTy" }
-- Decompose FunTy: (s -> t) and (c => t)
@@ -1925,7 +1925,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
-- Provide Refl evidence for the constraint
-- Ignore 'swapped' because it's Refl!
- ; setEvBindIfWanted new_ev True $
+ ; setEvBindIfWanted new_ev EvCanonical $
evCoercion (mkNomReflCo final_rhs)
-- Kick out any constraints that can now be rewritten
@@ -2038,7 +2038,7 @@ canEqReflexive :: CtEvidence -- ty ~ ty
-> TcType -- ty
-> TcS (StopOrContinue a) -- always Stop
canEqReflexive ev eq_rel ty
- = do { setEvBindIfWanted ev True $
+ = do { setEvBindIfWanted ev EvCanonical $
evCoercion (mkReflCo (eqRelRole eq_rel) ty)
; stopWith ev "Solved by reflexivity" }
@@ -2617,7 +2617,7 @@ tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel })
= Stage $
do { inerts <- getInertCans
; if | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item
- -> do { setEvBindIfWanted ev True $
+ -> do { setEvBindIfWanted ev EvCanonical $
evCoercion (maybeSymCo swapped $
downgradeRole (eqRelRole eq_rel)
(ctEvRewriteRole ev_i)
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -73,9 +73,9 @@ try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
, text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
; case solveOneFromTheOther ct_i ct_w of
- KeepInert -> do { setEvBindIfWanted ev_w True (swap_me swap ev_i)
+ KeepInert -> do { setEvBindIfWanted ev_w EvCanonical (swap_me swap ev_i)
; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
- KeepWork -> do { setEvBindIfWanted ev_i True (swap_me swap ev_w)
+ KeepWork -> do { setEvBindIfWanted ev_i EvCanonical (swap_me swap ev_w)
; updInertCans (updIrreds (\_ -> others))
; continueWith () } }
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -44,6 +44,7 @@ module GHC.Tc.Solver.Monad (
-- Evidence creation and transformation
MaybeNew(..), freshGoals, isFresh, getEvExpr,
+ CanonicalEvidence(..),
newTcEvBinds, newNoTcEvBinds,
newWantedEq, emitNewWantedEq,
@@ -1693,7 +1694,7 @@ setWantedEq (HoleDest hole) co
setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev)
-- | Good for both equalities and non-equalities
-setWantedEvTerm :: TcEvDest -> Canonical -> EvTerm -> TcS ()
+setWantedEvTerm :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest hole) _canonical tm
| Just co <- evTermCoercion_maybe tm
= do { useVars (coVarsOfCo co)
@@ -1701,7 +1702,7 @@ setWantedEvTerm (HoleDest hole) _canonical tm
| otherwise
= -- See Note [Yukky eq_sel for a HoleDest]
do { let co_var = coHoleCoVar hole
- ; setEvBind (mkWantedEvBind co_var True tm)
+ ; setEvBind (mkWantedEvBind co_var EvCanonical tm)
; fillCoercionHole hole (mkCoVarCo co_var) }
setWantedEvTerm (EvVarDest ev_id) canonical tm
@@ -1731,7 +1732,7 @@ fillCoercionHole hole co
= do { wrapTcS $ TcM.fillCoercionHole hole co
; kickOutAfterFillingCoercionHole hole }
-setEvBindIfWanted :: CtEvidence -> Canonical -> EvTerm -> TcS ()
+setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted ev canonical tm
= case ev of
CtWanted { ctev_dest = dest } -> setWantedEvTerm dest canonical tm
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -425,7 +425,7 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
; ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds
- ; setWantedEvTerm dest True $
+ ; setWantedEvTerm dest EvCanonical $
EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
, et_binds = ev_binds, et_body = w_id }
@@ -557,7 +557,7 @@ finish_rewrite ev@(CtWanted { ctev_dest = dest
= do { mb_new_ev <- newWanted loc rewriters' new_pred
; let ev_rw_role = ctEvRewriteRole ev
; massert (coercionRole co == ev_rw_role)
- ; setWantedEvTerm dest True $
+ ; setWantedEvTerm dest EvCanonical $
mkEvCast (getEvExpr mb_new_ev)
(downgradeRole Representational ev_rw_role (mkSymCo co))
; case mb_new_ev of
@@ -632,7 +632,8 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 })
where
setEv :: (EvTerm,Ct) -> TcS ()
setEv (ev,ct) = case ctEvidence ct of
- CtWanted { ctev_dest = dest } -> setWantedEvTerm dest True ev -- TODO: plugins should be able to signal non-canonicity
+ CtWanted { ctev_dest = dest } -> setWantedEvTerm dest EvCanonical ev
+ -- TODO: plugins should be able to signal non-canonicity
_ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
-- | A pair of (given, wanted) constraints to pass to plugins
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -1497,7 +1497,7 @@ tcSuperClasses skol_info dfun_id cls tyvars dfun_evs dfun_ev_binds sc_theta
; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
; sc_ev_id <- newEvVar sc_pred
- ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id True sc_ev_tm
+ ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id EvCanonical sc_ev_tm
; let sc_top_ty = tcMkDFunSigmaTy tyvars (map idType dfun_evs) sc_pred
sc_top_id = mkLocalId sc_top_name ManyTy sc_top_ty
export = ABE { abe_wrap = idHsWrapper
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -70,7 +70,7 @@ import GHC.Types.Basic
import GHC.Core
import GHC.Core.Class (Class, classSCSelId )
import GHC.Core.FVs ( exprSomeFreeVars )
-import GHC.Core.InstEnv ( Canonical )
+import GHC.Core.InstEnv ( CanonicalEvidence(..) )
import GHC.Utils.Misc
import GHC.Utils.Panic
@@ -471,7 +471,7 @@ instance Outputable EvBindMap where
data EvBindInfo
= EvBindGiven { -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
}
- | EvBindWanted { ebi_canonical :: Canonical -- See Note [Desugaring non-canonical evidence]
+ | EvBindWanted { ebi_canonical :: CanonicalEvidence -- See Note [Desugaring non-canonical evidence]
}
-----------------
@@ -485,7 +485,7 @@ data EvBind
evBindVar :: EvBind -> EvVar
evBindVar = eb_lhs
-mkWantedEvBind :: EvVar -> Canonical -> EvTerm -> EvBind
+mkWantedEvBind :: EvVar -> CanonicalEvidence -> EvTerm -> EvBind
mkWantedEvBind ev c tm = EvBind { eb_info = EvBindWanted c, eb_lhs = ev, eb_rhs = tm }
-- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -935,43 +935,53 @@ hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity
************************************************************************
-}
-getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
+getOverlapFlag :: Maybe OverlapMode -- User pragma if any
+ -> TcM OverlapFlag
-- Construct the OverlapFlag from the global module flags,
-- but if the overlap_mode argument is (Just m),
-- set the OverlapMode to 'm'
-getOverlapFlag overlap_mode
+--
+-- The overlap_mode argument comes from a user pragma on the instance decl:
+-- Pragma overlap_mode_prag
+-- -----------------------------------------
+-- {-# OVERLAPPABLE #-} Overlappable
+-- {-# OVERLAPPING #-} Overlapping
+-- {-# OVERLAPS #-} Overlaps
+-- {-# INCOHERENT #-} Incoherent -- if -fspecialise-incoherent (on by default)
+-- {-# INCOHERENT #-} NonCanonical -- if -fno-specialise-incoherent
+-- See Note [Rules for instance lookup] in GHC.Core.InstEnv
+
+getOverlapFlag overlap_mode_prag
= do { dflags <- getDynFlags
; let overlap_ok = xopt LangExt.OverlappingInstances dflags
incoherent_ok = xopt LangExt.IncoherentInstances dflags
noncanonical_incoherence = not $ gopt Opt_SpecialiseIncoherents dflags
- use x = OverlapFlag { isSafeOverlap = safeLanguageOn dflags
- , overlapMode = x }
- default_oflag | incoherent_ok = use (Incoherent NoSourceText)
- | overlap_ok = use (Overlaps NoSourceText)
- | otherwise = use (NoOverlap NoSourceText)
+ overlap_mode
+ | Just m <- overlap_mode_prag = m
+ | incoherent_ok = Incoherent NoSourceText
+ | overlap_ok = Overlaps NoSourceText
+ | otherwise = NoOverlap NoSourceText
- oflag = setOverlapModeMaybe default_oflag overlap_mode
- final_oflag = effective_oflag noncanonical_incoherence oflag
- ; return final_oflag }
- where
- effective_oflag noncanonical_incoherence oflag at OverlapFlag{ overlapMode = overlap_mode }
- = oflag { overlapMode = effective_overlap_mode noncanonical_incoherence overlap_mode }
+ -- final_overlap_mode: the `-fspecialise-incoherents` flag controls the
+ -- meaning of the `Incoherent` overlap mode: as either an Incoherent overlap
+ -- flag, or a NonCanonical overlap flag.
+ -- See GHC.Core.InstEnv Note [Coherence and specialisation: overview]
+ final_overlap_mode
+ | Incoherent s <- overlap_mode
+ , noncanonical_incoherence = NonCanonical s
+ | otherwise = overlap_mode
- -- The `-fspecialise-incoherents` flag controls the meaning of the
- -- `Incoherent` overlap mode: as either an Incoherent overlap
- -- flag, or a NonCanonical overlap flag. See Note [Coherence and specialisation: overview]
- -- in GHC.Core.InstEnv for why we care about this distinction.
- effective_overlap_mode noncanonical_incoherence = \case
- Incoherent s | noncanonical_incoherence -> NonCanonical s
- overlap_mode -> overlap_mode
+ ; return (OverlapFlag { isSafeOverlap = safeLanguageOn dflags
+ , overlapMode = final_overlap_mode }) }
tcGetInsts :: TcM [ClsInst]
-- Gets the local class instances.
tcGetInsts = fmap tcg_insts getGblEnv
-newClsInst :: Maybe OverlapMode -> Name -> [TyVar] -> ThetaType
+newClsInst :: Maybe OverlapMode -- User pragma
+ -> Name -> [TyVar] -> ThetaType
-> Class -> [Type] -> Maybe (WarningTxt GhcRn) -> TcM ClsInst
newClsInst overlap_mode dfun_name tvs theta clas tys warn
= do { (subst, tvs') <- freshenTyVarBndrs tvs
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2906,18 +2906,20 @@ data UnifyCheckCaller
= UC_OnTheFly -- Called from the on-the-fly unifier
| UC_QuickLook -- Called from Quick Look
| UC_Solver -- Called from constraint solver
+ | UC_Defaulting -- Called when doing top-level defaulting
simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
-- simpleUnifyCheck does a fast check: True <=> unification is OK
-- If it says 'False' then unification might still be OK, but
-- it'll take more work to do -- use the full checkTypeEq
--
+-- * Rejects if lhs_tv occurs in rhs_ty (occurs check)
-- * Rejects foralls unless
-- lhs_tv is RuntimeUnk (used by GHCi debugger)
-- or is a QL instantiation variable
-- * Rejects a non-concrete type if lhs_tv is concrete
-- * Rejects type families unless fam_ok=True
--- * Does a level-check for type variables
+-- * Does a level-check for type variables, to avoid skolem escape
--
-- This function is pretty heavily used, so it's optimised not to allocate
simpleUnifyCheck caller lhs_tv rhs
@@ -2939,9 +2941,10 @@ simpleUnifyCheck caller lhs_tv rhs
-- families, so we let it through there (not very principled, but let's
-- see if it bites us)
fam_ok = case caller of
- UC_Solver -> True
- UC_QuickLook -> True
- UC_OnTheFly -> False
+ UC_Solver -> True
+ UC_QuickLook -> True
+ UC_OnTheFly -> False
+ UC_Defaulting -> True
go (TyVarTy tv)
| lhs_tv == tv = False
=====================================
testsuite/tests/indexed-types/should_compile/Simple14.hs
=====================================
@@ -1,6 +1,6 @@
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeOperators, AllowAmbiguousTypes #-}
module Simple14 where
@@ -19,12 +19,11 @@ ntI :: (forall p. EQ_ x y -> p) -> EQ_ x y
ntI x = error "ntI"
foo :: forall m n. EQ_ (Maybe m) (Maybe n)
-foo = ntI (\x -> x `eqE` (eqI :: EQ_ m n))
-
--- Alternative
--- foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
+foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
+-- Aug 2024: this test started passing with the fix to #25029
+-- See Note [Defaulting equalities] in GHC.Tc.Solver
-- eq :: EQ_ (Maybe m) (Maybe n)
-- Need (Maybe m ~ Maybe n) => EQ_ m n ~ EQ_ zeta zeta
--- which reduces to (m~n) => m ~ zeta
--- but then we are stuck
+-- which reduces to (m~n) => m ~ zeta, but then
+-- we were stuck; now we default zeta:=m in tryDefaulting
=====================================
testsuite/tests/indexed-types/should_compile/Simple14.stderr deleted
=====================================
@@ -1,21 +0,0 @@
-
-Simple14.hs:22:27: error: [GHC-83865]
- • Couldn't match type ‘z0’ with ‘n’
- Expected: EQ_ z0 z0
- Actual: EQ_ m n
- ‘z0’ is untouchable
- inside the constraints: Maybe m ~ Maybe n
- bound by a type expected by the context:
- (Maybe m ~ Maybe n) => EQ_ z0 z0
- at Simple14.hs:22:26-41
- ‘n’ is a rigid type variable bound by
- the type signature for:
- foo :: forall m n. EQ_ (Maybe m) (Maybe n)
- at Simple14.hs:21:1-42
- • In the second argument of ‘eqE’, namely ‘(eqI :: EQ_ m n)’
- In the expression: x `eqE` (eqI :: EQ_ m n)
- In the first argument of ‘ntI’, namely
- ‘(\ x -> x `eqE` (eqI :: EQ_ m n))’
- • Relevant bindings include
- x :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:13)
- foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:1)
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -11,7 +11,7 @@ test('Simple10', normal, compile, [''])
test('Simple11', normal, compile, [''])
test('Simple12', normal, compile, [''])
test('Simple13', normal, compile, [''])
-test('Simple14', normal, compile_fail, [''])
+test('Simple14', normal, compile, [''])
test('Simple15', normal, compile, [''])
test('Simple16', normal, compile, [''])
test('Simple17', normal, compile, [''])
=====================================
testsuite/tests/simplCore/should_compile/T25160.hs
=====================================
@@ -0,0 +1,25 @@
+{-# LANGUAGE MonoLocalBinds #-}
+{-# OPTIONS_GHC -fno-specialise-incoherents #-}
+module T25160 where
+
+class C a where
+ op :: a -> String
+
+instance {-# OVERLAPPABLE #-} C a where
+ op _ = "C a"
+ {-# NOINLINE op #-}
+
+instance {-# INCOHERENT #-} C () where
+ op _ = "C ()"
+ {-# NOINLINE op #-}
+
+-- | Inhibit inlining, but keep specialize-ability
+large :: a -> a
+large x = x
+{-# NOINLINE large #-}
+
+bar :: C a => a -> String
+bar x = large (large (large (large (large (large (large (large (large (large (large (large (large (large (op x))))))))))))))
+
+{-# SPECIALISE bar :: a -> String #-}
+-- The RULE for this specialisation was bogus!
=====================================
testsuite/tests/simplCore/should_compile/T25160.stderr
=====================================
@@ -0,0 +1,5 @@
+
+==================== Tidy Core rules ====================
+"USPEC bar @_" forall (@a) ($dC :: C a). bar @a $dC = bar_$sbar @a
+
+
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -528,3 +528,4 @@ test('T24944', [extra_files(['T24944a.hs'])], multimod_compile, ['T24944', '-v0
test('T24725a', [ grep_errmsg(r'testedRule')], compile, ['-O -ddump-rule-firings'])
test('T25033', normal, compile, ['-O'])
+test('T25160', normal, compile, ['-O -ddump-rules'])
=====================================
testsuite/tests/typecheck/should_compile/T25029.hs
=====================================
@@ -0,0 +1,28 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T25029 where
+
+import Data.Kind (Type)
+import GHC.TypeLits (Nat)
+
+type family RankedOf2 (f :: Type -> Type) :: Type -> Type
+type family PrimalOf2 (f :: Type -> Type) :: Type -> Type
+
+rrev :: forall r r1 u. (Floating r, Floating r1)
+ => (forall f. ( RankedOf2 (PrimalOf2 f) ~ PrimalOf2 f
+ , (forall r2. Floating r2 => Floating (f r2))
+-- , f r1 ~ f u
+ )
+ => f r -> f r1)
+ -> ()
+rrev f = ()
+
+-- fails
+testSin0RrevPP1 :: ()
+testSin0RrevPP1 = rrev @Double sin
+
+-- works
+testSin0RrevPP2 :: ()
+testSin0RrevPP2 = rrev @Double @Double sin
=====================================
testsuite/tests/typecheck/should_compile/T25125.hs
=====================================
@@ -0,0 +1,27 @@
+{-# LANGUAGE DataKinds #-}
+module T25125 where
+
+import GHC.TypeNats
+
+newtype NonEmptyText (n :: Nat) = NonEmptyText String
+
+toT :: NonEmptyText 10 -> String
+toT = undefined
+
+fromT :: forall n. String -> NonEmptyText n
+fromT t = undefined
+
+baz = ()
+ where
+ validate :: forall n. (1 <= n) => NonEmptyText 10 -> (NonEmptyText n)
+ validate n = fromT (toT (check n))
+
+
+ -- Giving a type signature works
+ --check :: forall n. (1 <= n) => NonEmptyText n -> AppM (NonEmptyText n)
+ check = check2
+ -- Eta expanding check works
+ --check x = check2 x
+
+ check2 :: forall n. (1 <= n) => NonEmptyText n -> (NonEmptyText n)
+ check2 inputText = undefined
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -920,3 +920,5 @@ test('T24810', normal, compile, [''])
test('T24887', normal, compile, [''])
test('T24938a', normal, compile, [''])
test('T25094', normal, compile, [''])
+test('T25029', normal, compile, [''])
+test('T25125', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T21338.stderr
=====================================
@@ -1,27 +1,4 @@
-T21338.hs:38:24: error: [GHC-83865]
- • Couldn't match type ‘flds0’ with ‘flds’
- Expected: NP (K String) flds
- Actual: NP (K String) flds0
- ‘flds0’ is untouchable
- inside the constraints: All flds0
- bound by a pattern with constructor:
- Record :: forall (xs :: [*]).
- All xs =>
- NP (K String) xs -> ConstructorInfo xs,
- in a case alternative
- at T21338.hs:38:3-11
- ‘flds’ is a rigid type variable bound by
- the type signature for:
- fieldNames :: forall a (flds :: [*]). NP (K String) flds
- at T21338.hs:36:1-57
- • In the second argument of ‘hmap’, namely ‘np’
- In the expression: hmap id np
- In a case alternative: Record np -> hmap id np
- • Relevant bindings include
- np :: NP (K String) flds0 (bound at T21338.hs:38:10)
- fieldNames :: NP (K String) flds (bound at T21338.hs:37:1)
-
T21338.hs:39:8: error: [GHC-95781]
• Cannot apply expression of type ‘h0 f0 xs0 -> h0 g0 xs0’
to a visible type argument ‘flds’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/db0dcf8bf9df93ab42bf8aefc288a62223e54af9...b655485fe887f3898736c79a068e4e240b846083
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/db0dcf8bf9df93ab42bf8aefc288a62223e54af9...b655485fe887f3898736c79a068e4e240b846083
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/20240814/59e06abb/attachment-0001.html>
More information about the ghc-commits
mailing list