Remove derived CFunEqCans after solving givens
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 15 Jun 2015 12:23:16 +0000 (13:23 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 15 Jun 2015 12:26:05 +0000 (13:26 +0100)
See Note [The inert set after solving Givens] in TcSMonad.

This fixes Trac #10507.

compiler/typecheck/TcInteract.hs
compiler/typecheck/TcSMonad.hs
testsuite/tests/indexed-types/should_compile/T10507.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T

index 0000ff0..01b0ba1 100644 (file)
@@ -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
index f067d74..2ea302e 100644 (file)
@@ -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 (file)
index 0000000..14ef057
--- /dev/null
@@ -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
index aaf89e9..67be121 100644 (file)
@@ -259,3 +259,5 @@ test('T10079', normal, compile, [''])
 test('T10139', normal, compile, [''])
 test('T10340', normal, compile, [''])
 test('T10226', normal, compile, [''])
+test('T10507', normal, compile, [''])
+