Commit 5a66d574 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Better solving for representational equalities

This patch adds a bit of extra solving power for representational
equality constraints to fix Trac #14333

The main changes:

* Fix a buglet in TcType.isInsolubleOccursCheck which wrongly
  reported a definite occurs-check error for (a ~R# b a)

* Get rid of TcSMonad.emitInsolubles.  It had an ad-hoc duplicate-removal
  piece that is better handled in interactIrred, now that insolubles
  are Irreds.

  We need a little care to keep inert_count (which does not include
  insolubles) accurate.

* Refactor TcInteract.solveOneFromTheOther, to return a much simpler
  type.  It was just over-complicated before.

* Make TcInteract.interactIrred look for constraints that match
  either way around, in TcInteract.findMatchingIrreds

This wasn't hard and it cleaned up quite a bit of code.
parent 74cd1be0
......@@ -513,8 +513,8 @@ canHole ev hole
= do { let ty = ctEvPred ev
; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
do { emitInsoluble (CHoleCan { cc_ev = new_ev
, cc_hole = hole })
do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
, cc_hole = hole }))
; stopWith new_ev "Emit insoluble hole" } }
{-
......@@ -1310,8 +1310,7 @@ canEqHardFailure ev ty1 ty2
; (s2, co2) <- flatten FM_SubstOnly ev ty2
; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
`andWhenContinue` \ new_ev ->
do { emitInsoluble (mkInsolubleCt new_ev)
; stopWith new_ev "Definitely not equal" }}
continueWith (mkInsolubleCt new_ev) }
{-
Note [Decomposing TyConApps]
......@@ -1555,21 +1554,18 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
`andWhenContinue` \ new_ev ->
if isInsolubleOccursCheck eq_rel tv1 nrhs
then do { emitInsoluble (mkInsolubleCt new_ev)
then continueWith (mkInsolubleCt new_ev)
-- If we have a ~ [a], it is not canonical, and in particular
-- we don't want to rewrite existing inerts with it, otherwise
-- we'd risk divergence in the constraint solver
; stopWith new_ev "Occurs check" }
else continueWith (mkIrredCt new_ev) }
-- A representational equality with an occurs-check problem isn't
-- insoluble! For example:
-- a ~R b a
-- We might learn that b is the newtype Id.
-- But, the occurs-check certainly prevents the equality from being
-- canonical, and we might loop if we were to use it in rewriting.
else do { traceTcS "Possibly-soluble occurs check"
(ppr nlhs $$ ppr nrhs)
; continueWith (mkIrredCt new_ev) } }
where
role = eqRelRole eq_rel
......
This diff is collapsed.
......@@ -57,7 +57,7 @@ module TcSMonad (
getUnsolvedInerts,
removeInertCts, getPendingScDicts,
addInertCan, addInertEq, insertFunEq,
emitInsoluble, emitWorkNC, emitWork,
emitWorkNC, emitWork,
isImprovable,
-- The Model
......@@ -251,8 +251,16 @@ workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest =
= length eqs + length funeqs + length rest + length ders
workListWantedCount :: WorkList -> Int
-- Count the things we need to solve
-- excluding the insolubles (c.f. inert_count)
workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
= count isWantedCt eqs + count isWantedCt rest
= count isWantedCt eqs + count is_wanted rest
where
is_wanted ct
| CIrredCan { cc_ev = ev, cc_insol = insol } <- ct
= not insol && isWanted ev
| otherwise
= isWantedCt ct
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
......@@ -1416,14 +1424,12 @@ add_item :: InertCans -> Ct -> InertCans
add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
= ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
add_item ics item@(CIrredCan { cc_ev = ev })
= ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
, inert_count = bumpUnsolvedCount ev (inert_count ics) }
-- The 'False' is because the irreducible constraint might later instantiate
-- to an equality.
-- But since we try to simplify first, if there's a constraint function FC with
-- type instance FC Int = Show
-- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible
add_item ics@(IC { inert_irreds = irreds, inert_count = count })
item@(CIrredCan { cc_ev = ev, cc_insol = insoluble })
= ics { inert_irreds = irreds `Bag.snocBag` item
, inert_count = if insoluble
then count -- inert_count does not include insolubles
else bumpUnsolvedCount ev count }
add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
= ics { inert_dicts = addDict (inert_dicts ics) cls tys item
......@@ -2664,21 +2670,6 @@ emitWork cts
= do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
; updWorkListTcS (extendWorkListCts cts) }
emitInsoluble :: Ct -> TcS ()
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
emitInsoluble ct
= do { traceTcS "Emit insoluble" (ppr ct $$ pprCtLoc (ctLoc ct))
; updInertTcS add_insol }
where
this_pred = ctPred ct
add_insol is@(IS { inert_cans = ics@(IC { inert_irreds = old_irreds }) })
| drop_it = is
| otherwise = is { inert_cans = ics { inert_irreds = old_irreds `snocCts` ct } }
where
drop_it = isDroppableDerivedCt ct &&
anyBag (tcEqType this_pred . ctPred) old_irreds
-- See Note [Do not add duplicate derived insolubles]
newTcRef :: a -> TcS (TcRef a)
newTcRef x = wrapTcS (TcM.newTcRef x)
......@@ -2820,56 +2811,6 @@ zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC wc = wrapTcS (TcM.zonkWC wc)
{-
Note [Do not add duplicate derived insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In general we *must* add an insoluble (Int ~ Bool) even if there is
one such there already, because they may come from distinct call
sites. Not only do we want an error message for each, but with
-fdefer-type-errors we must generate evidence for each. But for
*derived* insolubles, we only want to report each one once. Why?
(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
equality many times, as the original constraint is successively rewritten.
(b) Ditto the successive iterations of the main solver itself, as it traverses
the constraint tree. See example below.
Also for *given* insolubles we may get repeated errors, as we
repeatedly traverse the constraint tree. These are relatively rare
anyway, so removing duplicates seems ok. (Alternatively we could take
the SrcLoc into account.)
Note that the test does not need to be particularly efficient because
it is only used if the program has a type error anyway.
Example of (b): assume a top-level class and instance declaration:
class D a b | a -> b
instance D [a] [a]
Assume we have started with an implication:
forall c. Eq c => { wc_simple = D [c] c [W] }
which we have simplified to:
forall c. Eq c => { wc_simple = D [c] c [W]
(c ~ [c]) [D] }
For some reason, e.g. because we floated an equality somewhere else,
we might try to re-solve this implication. If we do not do a
dropDerivedWC, then we will end up trying to solve the following
constraints the second time:
(D [c] c) [W]
(c ~ [c]) [D]
which will result in two Deriveds to end up in the insoluble set:
wc_simple = D [c] c [W]
(c ~ [c]) [D], (c ~ [c]) [D]
-}
{- *********************************************************************
* *
......
......@@ -2181,7 +2181,9 @@ isInsolubleOccursCheck eq_rel tv ty
go ty | Just ty' <- tcView ty = go ty'
go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
go (LitTy {}) = False
go (AppTy t1 t2) = go t1 || go t2
go (AppTy t1 t2) = case eq_rel of -- See Note [AppTy and ReprEq]
NomEq -> go t1 || go t2
ReprEq -> go t1
go (FunTy t1 t2) = go t1 || go t2
go (ForAllTy (TvBndr tv' _) inner_ty)
| tv' == tv = False
......@@ -2196,6 +2198,18 @@ isInsolubleOccursCheck eq_rel tv ty
role = eqRelRole eq_rel
{- Note [AppTy and ReprEq]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a ~R# b a
a ~R# a b
The former is /not/ a definite error; we might instantiate 'b' with Id
newtype Id a = MkId a
but the latter /is/ a definite error.
On the other hand, with nominal equality, both are definite errors
-}
isRigidTy :: TcType -> Bool
isRigidTy ty
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
......
module T14333 where
import Data.Coerce
bad :: Coercible (a b) (c d) => c d -> a b
bad = coerce
bad2 :: Coercible (c d) (a b) => c d -> a b
bad2 = coerce
bad3 :: Coercible (a b) b => b -> a b
bad3 = coerce
bad4 :: Coercible b (a b) => b -> a b
bad4 = coerce
newtype Id a = MkId a
foo :: Id Int
foo = bad3 (3 :: Int)
......@@ -577,3 +577,4 @@ test('T14149', normal, compile, [''])
test('T14154', normal, compile, [''])
test('T14158', normal, compile, [''])
test('T13943', normal, compile, ['-fsolve-constant-dicts'])
test('T14333', normal, compile, [''])
{-# LANGUAGE RankNTypes, GADTs, TypeFamilies #-}
module Test where
module Test where
data T a where
MkT :: a -> T a
MkT3 :: forall a. (a ~ Bool) => T a
data T a where
MkT :: a -> T a
MkT3 :: forall a. (a ~ Bool) => T a
-- Mismatches in givens
bloh :: T Int -> ()
bloh x = case x of
MkT3 -> ()
-- Mismatches in givens
bloh :: T Int -> ()
bloh x = case x of
MkT3 -> ()
type family F a b
type family F a b
type family G a b
type instance F a Bool = a
type instance F a Bool = a
type instance G a Char = a
goo1 :: forall a b. (F a b ~ [a]) => b -> a -> a
goo1 = undefined
goo1 = undefined
goo2 :: forall a. G a Char ~ [Int] => a -> a
goo2 = undefined
......@@ -31,16 +31,16 @@ test3 = goo1 False (goo2 undefined)
-- A frozen occurs check, now transformed to both a decomposition and occurs check
data M a where
M :: M a
data M a where
M :: M a
data T2 a b where
T2 :: T2 a b
T2 :: T2 a b
goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a
goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a
goo3 = undefined
goo4 :: forall a c. G a Char ~ T2 (T2 c c) c => a -> a
goo4 = undefined
goo4 = undefined
test4 = goo4 (goo3 False undefined)
test5 = goo3 False (goo4 undefined)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment