Commit efa136f7 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Remove derived CFunEqCans after solving givens

See Note [The inert set after solving Givens] in TcSMonad.

This fixes Trac #10507.
parent 77e5ec83
......@@ -126,13 +126,14 @@ must keep track of them separately.
solveSimpleGivens :: CtLoc -> [EvVar] -> TcS Cts
-- Solves the givens, adding them to the inert set
-- Returns any insoluble givens, taking those ones out of the inert set
-- Returns any insoluble givens, which represent inaccessible code,
-- taking those ones out of the inert set
solveSimpleGivens loc givens
| null givens -- Shortcut for common case
= return emptyCts
| otherwise
= do { go (map mk_given_ct givens)
; takeInertInsolubles }
; takeGivenInsolubles }
where
mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
, ctev_pred = evVarPred ev_id
......
......@@ -9,7 +9,7 @@ module TcSMonad (
extendWorkListCts, appendWorkList,
selectNextWorkItem,
workListSize, workListWantedCount,
updWorkListTcS, updWorkListTcS_return,
updWorkListTcS,
-- The TcS monad
TcS, runTcS, runTcSWithEvBinds,
......@@ -41,7 +41,7 @@ module TcSMonad (
updInertTcS, updInertCans, updInertDicts, updInertIrreds,
getNoGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertModel, getInertGivens,
emptyInert, getTcSInerts, setTcSInerts, takeInertInsolubles,
emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
getUnsolvedInerts,
removeInertCts,
addInertCan, addInertEq, insertFunEq,
......@@ -1474,15 +1474,43 @@ getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
setInertCans :: InertCans -> TcS ()
setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
takeInertInsolubles :: TcS Cts
-- Take the insoluble constraints out of the inert set
takeInertInsolubles
takeGivenInsolubles :: TcS Cts
-- See Note [The inert set after solving Givens]
takeGivenInsolubles
= updRetInertCans $ \ cans ->
( inert_insols cans
, cans { inert_insols = emptyBag
, inert_funeqs = filterFunEqs isGivenCt (inert_funeqs cans) } )
{- Note [The inert set after solving Givens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
After solving the Givens we take two things out of the inert set
a) The insolubles; we return these to report inaccessible code
We return these separately. We don't want to leave them in
the inert set, lest we onfuse them with insolubles arising from
solving wanteds
b) Any Derived CFunEqCans. Derived CTyEqCans are in the
inert_model and do no harm. In contrast, Derived CFunEqCans
get mixed up with the Wanteds later and confuse the
post-solve-wanted unflattening (Trac #10507).
E.g. From [G] 1 <= m, [G] m <= n
We get [D] 1 <= n, and we must remove it!
Otherwise we unflatten it more then once, and assign
to its fmv more than once...disaster.
It's ok to remove them because they turned ont not to
yield an insoluble, and hence have now done their work.
-}
updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
-- Modify the inert set with the supplied function
updRetInertCans upd_fn
= do { is_var <- getTcSInertsRef
; wrapTcS (do { inerts <- TcM.readTcRef is_var
; let cans = inert_cans inerts
cans' = cans { inert_insols = emptyBag }
; let (res, cans') = upd_fn (inert_cans inerts)
; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
; return (inert_insols cans) }) }
; return res }) }
updInertCans :: (InertCans -> InertCans) -> TcS ()
-- Modify the inert set with the supplied function
......@@ -2282,17 +2310,6 @@ updWorkListTcS f
; let new_work = f wl_curr
; wrapTcS (TcM.writeTcRef wl_var new_work) }
updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
-- Process the work list, returning a depleted work list,
-- plus a value extracted from it (typically a work item removed from it)
updWorkListTcS_return f
= do { wl_var <- getTcSWorkListRef
; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
; traceTcS "updWorkList" (ppr wl_curr)
; let (res,new_work) = f wl_curr
; wrapTcS (TcM.writeTcRef wl_var new_work)
; return res }
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC evs
| null evs
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
module T10507 where
import Data.Type.Equality ( (:~:)(Refl) )
import Prelude (Maybe(..), undefined)
import GHC.TypeLits ( Nat, type (<=))
data V (n::Nat)
testEq :: (m <= n) => V m -> V n -> Maybe (m :~: n)
testEq = undefined
uext :: (1 <= m, m <= n) => V m -> V n -> V n
uext e w =
case testEq e w of
Just Refl -> e
......@@ -259,3 +259,5 @@ test('T10079', normal, compile, [''])
test('T10139', normal, compile, [''])
test('T10340', normal, compile, [''])
test('T10226', normal, compile, [''])
test('T10507', normal, compile, [''])
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