Report a Wanted error even if there are Given ones
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 18 Oct 2018 14:41:44 +0000 (15:41 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 24 Oct 2018 15:38:55 +0000 (16:38 +0100)
We suppress some Given errors; see Note [Given errors]
in TcErrors.  But we must be careful not to suppress
Wanted errors because of the presence of these Given
errors -- else we might allow compilation to bogusly
proceed

The rubber hits the road in TcRnTypes.insolubleCt,
where we don't want to treat Givens as insoluble,
nor (and this is the new bit) Deriveds that arise
from Givens.  See Note [Given insolubles] in TcRnTypes.

This fixes #15767.

compiler/typecheck/TcErrors.hs
compiler/typecheck/TcRnTypes.hs
testsuite/tests/typecheck/should_fail/T15767.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T15767.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

index 35f31d1..951107b 100644 (file)
@@ -543,7 +543,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
     -- report1: ones that should *not* be suppresed by
     --          an insoluble somewhere else in the tree
     -- It's crucial that anything that is considered insoluble
-    -- (see TcRnTypes.insolubleWantedCt) is caught here, otherwise
+    -- (see TcRnTypes.insolubleCt) is caught here, otherwise
     -- we might suppress its error message, and proceed on past
     -- type checking to get a Lint error later
     report1 = [ ("Out of scope", is_out_of_scope,    True,  mkHoleReporter tidy_cts)
index 695d2ae..bbd85aa 100644 (file)
@@ -89,7 +89,7 @@ module TcRnTypes(
         isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
         addInsols, insolublesOnly, addSimples, addImplics,
         tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
-        tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt,
+        tyCoVarsOfWCList, insolubleCt, insolubleEqCt,
         isDroppableCt, insolubleImplic,
         arisesFromGivens,
 
@@ -2387,7 +2387,7 @@ addInsols wc cts
 insolublesOnly :: WantedConstraints -> WantedConstraints
 -- Keep only the definitely-insoluble constraints
 insolublesOnly (WC { wc_simple = simples, wc_impl = implics })
-  = WC { wc_simple = filterBag insolubleWantedCt simples
+  = WC { wc_simple = filterBag insolubleCt simples
        , wc_impl   = mapBag implic_insols_only implics }
   where
     implic_insols_only implic
@@ -2407,16 +2407,16 @@ insolubleImplic ic = isInsolubleStatus (ic_status ic)
 
 insolubleWC :: WantedConstraints -> Bool
 insolubleWC (WC { wc_impl = implics, wc_simple = simples })
-  =  anyBag insolubleWantedCt simples
+  =  anyBag insolubleCt simples
   || anyBag insolubleImplic implics
 
-insolubleWantedCt :: Ct -> Bool
+insolubleCt :: Ct -> Bool
 -- Definitely insoluble, in particular /excluding/ type-hole constraints
-insolubleWantedCt ct
-  | isGivenCt ct     = False              -- See Note [Given insolubles]
-  | isHoleCt ct      = isOutOfScopeCt ct  -- See Note [Insoluble holes]
-  | insolubleEqCt ct = True
-  | otherwise        = False
+insolubleCt ct
+  | not (insolubleEqCt ct) = False
+  | isHoleCt ct            = isOutOfScopeCt ct  -- See Note [Insoluble holes]
+  | arisesFromGivens ct    = False              -- See Note [Given insolubles]
+  | otherwise              = True
 
 insolubleEqCt :: Ct -> Bool
 -- Returns True of /equality/ constraints
@@ -2470,6 +2470,12 @@ because that'll suppress reports of [W] C b (f b).  But we
 may not report the insoluble [G] f b ~# b either (see Note [Given errors]
 in TcErrors), so we may fail to report anything at all!  Yikes.
 
+The same applies to Derived constraints that /arise from/ Givens.
+E.g.   f :: (C Int [a]) => blah
+where a fundep means we get
+       [D] Int ~ [a]
+By the same reasoning we must not suppress other errors (Trac #15767)
+
 Bottom line: insolubleWC (called in TcSimplify.setImplicationStatus)
              should ignore givens even if they are insoluble.
 
diff --git a/testsuite/tests/typecheck/should_fail/T15767.hs b/testsuite/tests/typecheck/should_fail/T15767.hs
new file mode 100644 (file)
index 0000000..f9f853d
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE FunctionalDependencies, FlexibleContexts #-}
+
+module T15767 where
+
+class C a b | b -> a where f :: a -> b
+
+y = x where
+  x :: (C () b, C Bool b) => b
+  x  = f ()
diff --git a/testsuite/tests/typecheck/should_fail/T15767.stderr b/testsuite/tests/typecheck/should_fail/T15767.stderr
new file mode 100644 (file)
index 0000000..2c20dd2
--- /dev/null
@@ -0,0 +1,9 @@
+
+T15767.hs:7:5: error:
+    • No instance for (C () b) arising from a use of ‘x’
+    • In the expression: x
+      In an equation for ‘y’:
+          y = x
+            where
+                x :: (C () b, C Bool b) => b
+                x = f ()
index 501c5e1..35c925e 100644 (file)
@@ -484,3 +484,4 @@ test('T15527', normal, compile_fail, [''])
 test('T15552', normal, compile, [''])
 test('T15552a', normal, compile_fail, [''])
 test('T15629', normal, compile_fail, [''])
+test('T15767', normal, compile_fail, [''])