[commit: ghc] master: Remove derived CFunEqCans after solving givens (efa136f)
git at git.haskell.org
git at git.haskell.org
Mon Jun 15 12:26:22 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/efa136f7199f9313e91ba2c1724b307aff45c9eb/ghc
>---------------------------------------------------------------
commit efa136f7199f9313e91ba2c1724b307aff45c9eb
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Mon Jun 15 13:23:16 2015 +0100
Remove derived CFunEqCans after solving givens
See Note [The inert set after solving Givens] in TcSMonad.
This fixes Trac #10507.
>---------------------------------------------------------------
efa136f7199f9313e91ba2c1724b307aff45c9eb
compiler/typecheck/TcInteract.hs | 5 +-
compiler/typecheck/TcSMonad.hs | 55 ++++++++++++++--------
.../tests/indexed-types/should_compile/T10507.hs | 23 +++++++++
testsuite/tests/indexed-types/should_compile/all.T | 2 +
4 files changed, 64 insertions(+), 21 deletions(-)
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 0000ff0..01b0ba1 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -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
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index f067d74..2ea302e 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -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
diff --git a/testsuite/tests/indexed-types/should_compile/T10507.hs b/testsuite/tests/indexed-types/should_compile/T10507.hs
new file mode 100644
index 0000000..14ef057
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T10507.hs
@@ -0,0 +1,23 @@
+{-# 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
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index aaf89e9..67be121 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -259,3 +259,5 @@ test('T10079', normal, compile, [''])
test('T10139', normal, compile, [''])
test('T10340', normal, compile, [''])
test('T10226', normal, compile, [''])
+test('T10507', normal, compile, [''])
+
More information about the ghc-commits
mailing list