[commit: ghc] master: Fix Trac #12797: approximateWC (13508ba)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/13508bad4810d4fa8581afbcb4f41c97fe4c92e2/ghc

>---------------------------------------------------------------

commit 13508bad4810d4fa8581afbcb4f41c97fe4c92e2
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Nov 2 11:53:21 2016 +0000

    Fix Trac #12797: approximateWC
    
    This patch makes approximateWC a bit more gung-ho when called
    from the defaulting code.  See Note [ApproximateWC], item (1).


>---------------------------------------------------------------

13508bad4810d4fa8581afbcb4f41c97fe4c92e2
 compiler/typecheck/TcSimplify.hs                   | 28 ++++++++++++----------
 testsuite/tests/typecheck/should_compile/T12797.hs | 15 ++++++++++++
 testsuite/tests/typecheck/should_compile/all.T     |  1 +
 3 files changed, 32 insertions(+), 12 deletions(-)

diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index ddf0bce..0594313 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -595,7 +595,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                                -- NB: must include derived errors in this test,
                                --     hence "incl_derivs"
 
-              else do { let quant_cand = approximateWC wanted_transformed
+              else do { let quant_cand = approximateWC False wanted_transformed
                             meta_tvs   = filter isMetaTyVar $
                                          tyCoVarsOfCtsList quant_cand
 
@@ -1606,10 +1606,10 @@ defaultTyVarTcS the_tv
   | otherwise
   = return False  -- the common case
 
-approximateWC :: WantedConstraints -> Cts
+approximateWC :: Bool -> WantedConstraints -> Cts
 -- Postcondition: Wanted or Derived Cts
 -- See Note [ApproximateWC]
-approximateWC wc
+approximateWC float_past_equalities wc
   = float_wc emptyVarSet wc
   where
     float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
@@ -1630,18 +1630,17 @@ approximateWC wc
 
     float_implic :: TcTyCoVarSet -> Implication -> Cts
     float_implic trapping_tvs imp
-      | ic_no_eqs imp                 -- No equalities, so float
+      | float_past_equalities || ic_no_eqs imp
       = float_wc new_trapping_tvs (ic_wanted imp)
-      | otherwise                     -- Don't float out of equalities
-      = emptyCts                      -- See Note [ApproximateWC]
+      | otherwise   -- Take care with equalities
+      = emptyCts    -- See (1) under Note [ApproximateWC]
       where
         new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
     do_bag :: (a -> Bag c) -> Bag a -> Bag c
     do_bag f = foldrBag (unionBags.f) emptyBag
 
-{-
-Note [ApproximateWC]
-~~~~~~~~~~~~~~~~~~~~
+{- Note [ApproximateWC]
+~~~~~~~~~~~~~~~~~~~~~~~
 approximateWC takes a constraint, typically arising from the RHS of a
 let-binding whose type we are *inferring*, and extracts from it some
 *simple* constraints that we might plausibly abstract over.  Of course
@@ -1653,8 +1652,9 @@ to applyDefaultingRules) to extract constraints that that might be defaulted.
 
 There are two caveats:
 
-1.  We do *not* float anything out if the implication binds equality
-    constraints, because that defeats the OutsideIn story.  Consider
+1.  When infering most-general types (in simplifyInfer), we do *not*
+    float anything out if the implication binds equality constraints,
+    because that defeats the OutsideIn story.  Consider
        data T a where
          TInt :: T Int
          MkT :: T a
@@ -1669,6 +1669,10 @@ There are two caveats:
     float out of such implications, which meant it would happily infer
     non-principal types.)
 
+   HOWEVER (Trac #12797) in findDefaultableGroups we are not worried about
+   the most-general type; and we /do/ want to float out of equalities.
+   Hence the boolean flag to approximateWC.
+
 2. We do not float out an inner constraint that shares a type variable
    (transitively) with one that is trapped by a skolem.  Eg
        forall a.  F a ~ beta, Integral beta
@@ -2000,7 +2004,7 @@ findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
     , defaultable_tyvar tv
     , defaultable_classes (map sndOf3 group) ]
   where
-    simples                = approximateWC wanteds
+    simples                = approximateWC True wanteds
     (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
     unary_groups           = equivClasses cmp_tv unaries
 
diff --git a/testsuite/tests/typecheck/should_compile/T12797.hs b/testsuite/tests/typecheck/should_compile/T12797.hs
new file mode 100644
index 0000000..01bf5af
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12797.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE ExtendedDefaultRules      #-}
+
+module T12797 where
+
+import Prelude
+import Control.Monad.IO.Class
+
+type family FuncArg (m :: (* -> *)) :: Maybe *
+
+test2 :: (MonadIO m, FuncArg m ~ 'Nothing) => m ()
+test2 = liftIO $ print 6
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 93f1b5f..08a24d7 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -551,3 +551,4 @@ test('T12507', normal, compile, [''])
 test('T12734', normal, compile, [''])
 test('T12734a', normal, compile_fail, [''])
 test('T12763', normal, compile, [''])
+test('T12797', normal, compile, [''])