Do not discard insoluble Derived constraints
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 Sep 2014 09:44:46 +0000 (10:44 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 Sep 2014 09:56:47 +0000 (10:56 +0100)
This is preparing for a fix to Trac #9612. The idea is that insoluble
constraints are nice solid errors that we should not discard before
we have a chance to report them.  So TcRnTypes.dropDerivedWC now
keeps insoluble Derived constrains, and instead TcSimplify.solve_wanteds
filters them out

We get somewhat better error message for kind-equality failures too.

A slight downside is that to avoid *duplicate* kind-equality failures
when we float a kind-incompatible equality (e.g.  alpha:* ~ Int#),
I've disabled constraint-floating when there are insolubles.  But that
in turn makes a handful of error messages a little less informative;
good examples are mc21, mc22, mc25.  But I am re-jigging the
constraint floating machinery in another branch, which will make this
go back to the way it was before.

17 files changed:
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSimplify.lhs
testsuite/tests/indexed-types/should_fail/T3330c.stderr
testsuite/tests/typecheck/should_fail/T3950.stderr
testsuite/tests/typecheck/should_fail/T5570.stderr
testsuite/tests/typecheck/should_fail/T7368.stderr
testsuite/tests/typecheck/should_fail/T7368a.stderr
testsuite/tests/typecheck/should_fail/T8262.stderr
testsuite/tests/typecheck/should_fail/T8603.stderr
testsuite/tests/typecheck/should_fail/mc21.stderr
testsuite/tests/typecheck/should_fail/mc22.stderr
testsuite/tests/typecheck/should_fail/mc25.stderr
testsuite/tests/typecheck/should_fail/tcfail090.stderr
testsuite/tests/typecheck/should_fail/tcfail122.stderr
testsuite/tests/typecheck/should_fail/tcfail123.stderr
testsuite/tests/typecheck/should_fail/tcfail159.stderr
testsuite/tests/typecheck/should_fail/tcfail200.stderr

index f46bdfd..bff59ee 100644 (file)
@@ -1070,36 +1070,34 @@ ctPred ct = ctEvPred (cc_ev ct)
 
 dropDerivedWC :: WantedConstraints -> WantedConstraints
 -- See Note [Dropping derived constraints]
-dropDerivedWC wc@(WC { wc_flat = flats, wc_insol = insols })
-  = wc { wc_flat  = filterBag isWantedCt          flats
-       , wc_insol = filterBag (not . isDerivedCt) insols  }
-    -- Keep Givens from insols because they indicate unreachable code
-    -- The implications are (recursively) already filtered
+dropDerivedWC wc@(WC { wc_flat = flats })
+  = wc { wc_flat  = filterBag isWantedCt flats }
+    -- The wc_impl implications are already (recursively) filtered
 \end{code}
 
 Note [Dropping derived constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In general we discard derived constraints at the end of constraint solving;
-see dropDerivedWC.  A consequence is that
-   we never report an error for a derived constraint,
-   and hence we do not need to take much care with their CtLoc
-
-For example,
-
+see dropDerivedWC.  For example
  * If we have an unsolved (Ord a), we don't want to complain about
    an unsolved (Eq a) as well.
- * If we have kind-incompatible (a::* ~ Int#::#) equality, we
-   don't want to complain about the kind error twice.
-
-Arguably, for *some* derived constraints we might want to report errors.
-Notably, functional dependencies.  If we have
-    class C a b | a -> b
-and we have
-    [W] C a b, [W] C a c
-where a,b,c are all signature variables.  Then we could imagine
-reporting an error unifying (b ~ c). But it's better to report that we can't
-solve (C a b) and (C a c) since those arose directly from something the
-programmer wrote.
+
+But we keep Derived *insoluble* constraints because they indicate a solid,
+comprehensible error.  Particularly:
+
+ * Insolubles Givens indicate unreachable code
+
+ * Insoluble kind equalities (e.g. [D] * ~ (* -> *)) may arise from
+   a type equality a ~ Int#, say
+
+ * Insoluble derived wanted equalities (e.g. [D] Int ~ Bool) may
+   arise from functional dependency interactions.  We are careful
+   to keep a good CtOrigin on such constriants (FunDepOrigin1, FunDepOrigin2)
+   so that we can produce a good error message (Trac #9612)
+
+Since we leave these Derived constraints in the residual WantedConstraints,
+we must filter them out when we re-process the WantedConstraint,
+in TcSimplify.solve_wanteds.
 
 
 %************************************************************************
index 4fff6ab..ceb517d 100644 (file)
@@ -674,7 +674,10 @@ solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols
          -- of adding Derived insolubles twice; see
          -- TcSMonad Note [Do not add duplicate derived insolubles]
        ; traceTcS "solveFlats {" empty
-       ; let all_flats = flats `unionBags` insols
+       ; let all_flats = flats `unionBags` filterBag (not . isDerivedCt) insols
+             -- See Note [Dropping derived constraints] in TcRnTypes for
+             -- why the insolubles may have derived constraints
+
        ; impls_from_flats <- solveInteract all_flats
        ; traceTcS "solveFlats end }" (ppr impls_from_flats)
 
@@ -1135,9 +1138,11 @@ floatEqualities :: [TcTyVar] -> Bool -> WantedConstraints
 --
 -- Subtleties: Note [Float equalities from under a skolem binding]
 --             Note [Skolem escape]
-floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats })
+floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats, wc_insol = insols })
   | not no_given_eqs  -- There are some given equalities, so don't float
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
+  | not (isEmptyBag insols)
+  = return (emptyBag, wanteds)   -- Note [Do not float equalities if there are insolubles]
   | otherwise
   = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
        ; untch <- TcS.getUntouchables
@@ -1169,6 +1174,15 @@ floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats })
       | otherwise                 = tvs
 \end{code}
 
+Note [Do not float equalities if there are insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality.
+If we float the equality outwards, we'll get *another* Derived
+insoluble equality one level out, so the same error will be reported
+twice.  However, the equality is insoluble anyway, and when there are
+any insolubles we report only them, so there is no point in floating.
+
+
 Note [When does an implication have given equalities?]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      NB: This note is mainly referred to from TcSMonad
index f9108f2..afb9902 100644 (file)
@@ -1,24 +1,10 @@
 
 T3330c.hs:23:43:
-    Could not deduce (f1 ~ f1 x)
-    from the context (f ~ (f1 :+: g))
-      bound by a pattern with constructor
-                 RSum :: forall (f :: * -> *) (g :: * -> *).
-                         R f -> R g -> R (f :+: g),
-               in an equation for ‘plug'’
-      at T3330c.hs:23:8-17
-      ‘f1’ is a rigid type variable bound by
-           a pattern with constructor
-             RSum :: forall (f :: * -> *) (g :: * -> *).
-                     R f -> R g -> R (f :+: g),
-           in an equation for ‘plug'’
-           at T3330c.hs:23:8
+    Couldn't match kind ‘*’ with ‘* -> *’
+    When matching types
+      Der ((->) x) :: * -> *
+      R :: (* -> *) -> *
     Expected type: Der ((->) x) (f1 x)
       Actual type: R f1
-    Relevant bindings include
-      x :: x (bound at T3330c.hs:23:29)
-      df :: f1 x (bound at T3330c.hs:23:25)
-      rf :: R f1 (bound at T3330c.hs:23:13)
-      plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:23:1)
     In the first argument of ‘plug’, namely ‘rf’
     In the first argument of ‘Inl’, namely ‘(plug rf df x)’
index 0fc428e..7b4837c 100644 (file)
@@ -1,6 +1,9 @@
 
 T3950.hs:15:13:
-    Couldn't match type ‘Id p0 x0’ with ‘Id p’
+    Couldn't match kind ‘* -> *’ with ‘*’
+    When matching types
+      w :: (* -> * -> *) -> *
+      Sealed :: (* -> *) -> *
     Expected type: w (Id p)
       Actual type: Sealed (Id p0 x0)
     Relevant bindings include
index 626533c..21a4e0c 100644 (file)
@@ -1,8 +1,9 @@
-\r
-T5570.hs:7:16:\r
-    Kind incompatibility when matching types:\r
-      s0 :: *\r
-      Double# :: #\r
-    In the second argument of ‘($)’, namely ‘D# $ 3.0##’\r
-    In the expression: print $ D# $ 3.0##\r
-    In an equation for ‘main’: main = print $ D# $ 3.0##\r
+
+T5570.hs:7:16:
+    Couldn't match kind ‘*’ with ‘#’
+    When matching types
+      s0 :: *
+      Double# :: #
+    In the second argument of ‘($)’, namely ‘D# $ 3.0##’
+    In the expression: print $ D# $ 3.0##
+    In an equation for ‘main’: main = print $ D# $ 3.0##
index c2e6360..2a02264 100644 (file)
@@ -1,6 +1,7 @@
 
 T7368.hs:3:10:
-    Kind incompatibility when matching types:
+    Couldn't match kind ‘* -> *’ with ‘*’
+    When matching types
       c0 :: (* -> *) -> *
       (->) a0 :: * -> *
     Expected type: a0 -> b0
index 1316d5a..79396df 100644 (file)
@@ -1,11 +1,12 @@
-\r
-T7368a.hs:8:6:\r
-    Couldn't match type ‘f’ with ‘Bad’\r
-      ‘f’ is a rigid type variable bound by\r
-          the type signature for fun :: f (Bad f) -> Bool at T7368a.hs:7:15\r
-    Expected type: f (Bad f)\r
-      Actual type: Bad t0\r
-    Relevant bindings include\r
-      fun :: f (Bad f) -> Bool (bound at T7368a.hs:8:1)\r
-    In the pattern: Bad x\r
-    In an equation for ‘fun’: fun (Bad x) = True\r
+
+T7368a.hs:8:6:
+    Couldn't match kind ‘*’ with ‘* -> *’
+    When matching types
+      f :: * -> *
+      Bad :: (* -> *) -> *
+    Expected type: f (Bad f)
+      Actual type: Bad t0
+    Relevant bindings include
+      fun :: f (Bad f) -> Bool (bound at T7368a.hs:8:1)
+    In the pattern: Bad x
+    In an equation for ‘fun’: fun (Bad x) = True
index 44c2fb8..9bc46e3 100644 (file)
@@ -1,6 +1,7 @@
 
 T8262.hs:5:15:
-    Kind incompatibility when matching types:
+    Couldn't match kind ‘*’ with ‘#’
+    When matching types
       a :: *
       GHC.Prim.Int# :: #
     Relevant bindings include
index 8ee8ccc..d9d2aaf 100644 (file)
@@ -1,22 +1,25 @@
-\r
-T8603.hs:29:17:\r
-    Couldn't match type ‘(->) [a0]’ with ‘[Integer]’\r
-    Expected type: [Integer] -> StateT s RV t0\r
-      Actual type: t1 ((->) [a0]) (StateT s RV t0)\r
-    The function ‘lift’ is applied to two arguments,\r
-    but its type ‘([a0] -> StateT s RV t0)\r
-                  -> t1 ((->) [a0]) (StateT s RV t0)’\r
-    has only one\r
-    In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]\r
-    In the expression:\r
-      do { prize <- lift uniform [1, 2, ....];\r
-           return False }\r
-\r
-T8603.hs:29:22:\r
-    Couldn't match type ‘StateT s RV t0’ with ‘RV a0’\r
-    Expected type: [a0] -> StateT s RV t0\r
-      Actual type: [a0] -> RV a0\r
-    Relevant bindings include\r
-      testRVState1 :: RVState s Bool (bound at T8603.hs:28:1)\r
-    In the first argument of ‘lift’, namely ‘uniform’\r
-    In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]\r
+
+T8603.hs:29:17:
+    Couldn't match kind ‘* -> *’ with ‘*’
+    When matching types
+      t1 :: (* -> *) -> * -> *
+      (->) :: * -> * -> *
+    Expected type: [Integer] -> StateT s RV t0
+      Actual type: t1 ((->) [a0]) (StateT s RV t0)
+    The function ‘lift’ is applied to two arguments,
+    but its type ‘([a0] -> StateT s RV t0)
+                  -> t1 ((->) [a0]) (StateT s RV t0)’
+    has only one
+    In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
+    In the expression:
+      do { prize <- lift uniform [1, 2, ....];
+           return False }
+
+T8603.hs:29:22:
+    Couldn't match type ‘StateT s RV t0’ with ‘RV a0’
+    Expected type: [a0] -> StateT s RV t0
+      Actual type: [a0] -> RV a0
+    Relevant bindings include
+      testRVState1 :: RVState s Bool (bound at T8603.hs:28:1)
+    In the first argument of ‘lift’, namely ‘uniform’
+    In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
index 337c843..2305394 100644 (file)
@@ -2,8 +2,8 @@
 mc21.hs:12:26:
     Couldn't match type ‘a’ with ‘[a]’
       ‘a’ is a rigid type variable bound by
-          a type expected by the context: [a] -> [[a]] at mc21.hs:12:9
-    Expected type: [a] -> [[a]]
+          a type expected by the context: [a] -> t [a] at mc21.hs:12:9
+    Expected type: [a] -> t [a]
       Actual type: [a] -> [a]
     In the expression: take 5
     In a stmt of a monad comprehension: then group using take 5
index f3da3c5..44a2eeb 100644 (file)
@@ -1,21 +1,22 @@
 
 mc22.hs:10:9:
-    No instance for (Functor t) arising from a use of ‘fmap’
+    No instance for (Functor t1) arising from a use of ‘fmap’
     Possible fix:
-      add (Functor t) to the context of
-        a type expected by the context: (a -> b) -> t a -> t b
-        or the inferred type of foo :: [t [Char]]
+      add (Functor t1) to the context of
+        a type expected by the context: (a -> b) -> t1 a -> t1 b
+        or the inferred type of foo :: t (t1 [Char])
     In the expression: fmap
     In a stmt of a monad comprehension: then group using take 5
     In the expression:
       [x + 1 | x <- ["Hello", "World"], then group using take 5]
 
 mc22.hs:10:26:
-    Couldn't match type ‘a’ with ‘t a’
+    Couldn't match type ‘a’ with ‘t1 a’
       ‘a’ is a rigid type variable bound by
-          a type expected by the context: [a] -> [t a] at mc22.hs:10:9
-    Expected type: [a] -> [t a]
+          a type expected by the context: [a] -> t (t1 a) at mc22.hs:10:9
+    Expected type: [a] -> t (t1 a)
       Actual type: [a] -> [a]
-    Relevant bindings include foo :: [t [Char]] (bound at mc22.hs:8:1)
+    Relevant bindings include
+      foo :: t (t1 [Char]) (bound at mc22.hs:8:1)
     In the expression: take 5
     In a stmt of a monad comprehension: then group using take 5
index 6af388f..e101f4b 100644 (file)
@@ -1,18 +1,18 @@
 
 mc25.hs:9:24:
-    No instance for (Functor t1) arising from a use of ‘fmap’
+    No instance for (Functor t2) arising from a use of ‘fmap’
     Possible fix:
-      add (Functor t1) to the context of
-        a type expected by the context: (a -> b) -> t1 a -> t1 b
-        or the inferred type of z :: [t1 t]
+      add (Functor t2) to the context of
+        a type expected by the context: (a -> b) -> t2 a -> t2 b
+        or the inferred type of z :: t (t2 t1)
     In the expression: fmap
     In a stmt of a monad comprehension: then group by x using take
     In the expression: [x | x <- [1 .. 10], then group by x using take]
 
 mc25.hs:9:46:
-    Couldn't match type ‘Int’ with ‘a -> t’
-    Expected type: (a -> t) -> [a] -> [t1 a]
+    Couldn't match type ‘Int’ with ‘a -> t1
+    Expected type: (a -> t1) -> [a] -> t (t2 a)
       Actual type: Int -> [a] -> [a]
-    Relevant bindings include z :: [t1 t] (bound at mc25.hs:9:1)
+    Relevant bindings include z :: t (t2 t1) (bound at mc25.hs:9:1)
     In the expression: take
     In a stmt of a monad comprehension: then group by x using take
index c4a8a31..37f9665 100644 (file)
@@ -1,7 +1,8 @@
-\r
-tcfail090.hs:11:9:\r
-    Kind incompatibility when matching types:\r
-      a0 :: *\r
-      ByteArray# :: #\r
-    In the expression: my_undefined\r
-    In an equation for ‘die’: die _ = my_undefined\r
+
+tcfail090.hs:11:9:
+    Couldn't match kind ‘*’ with ‘#’
+    When matching types
+      a0 :: *
+      ByteArray# :: #
+    In the expression: my_undefined
+    In an equation for ‘die’: die _ = my_undefined
index b643d58..6ad75f4 100644 (file)
@@ -1,6 +1,7 @@
 
 tcfail122.hs:8:9:
-    Kind incompatibility when matching types:
+    Couldn't match kind ‘* -> *’ with ‘*’
+    When matching types
       c0 :: (* -> *) -> *
       a :: * -> *
     Expected type: a b
index 1fcb62d..1bc0246 100644 (file)
@@ -1,8 +1,9 @@
-\r
-tcfail123.hs:11:9:\r
-    Kind incompatibility when matching types:\r
-      t0 :: *\r
-      GHC.Prim.Int# :: #\r
-    In the first argument of ‘f’, namely ‘3#’\r
-    In the expression: f 3#\r
-    In an equation for ‘h’: h v = f 3#\r
+
+tcfail123.hs:11:9:
+    Couldn't match kind ‘*’ with ‘#’
+    When matching types
+      t0 :: *
+      GHC.Prim.Int# :: #
+    In the first argument of ‘f’, namely ‘3#’
+    In the expression: f 3#
+    In an equation for ‘h’: h v = f 3#
index 9154e43..a8ae57b 100644 (file)
@@ -1,8 +1,9 @@
-\r
-tcfail159.hs:9:11:\r
-    Kind incompatibility when matching types:\r
-      t0 :: *\r
-      (# Int, Int #) :: #\r
-    In the pattern: ~(# p, q #)\r
-    In a case alternative: ~(# p, q #) -> p\r
-    In the expression: case h x of { ~(# p, q #) -> p }\r
+
+tcfail159.hs:9:11:
+    Couldn't match kind ‘*’ with ‘#’
+    When matching types
+      t0 :: *
+      (# Int, Int #) :: #
+    In the pattern: ~(# p, q #)
+    In a case alternative: ~(# p, q #) -> p
+    In the expression: case h x of { ~(# p, q #) -> p }
index 5a35839..ba9f0ce 100644 (file)
@@ -1,6 +1,7 @@
 
 tcfail200.hs:5:15:
-    Kind incompatibility when matching types:
+    Couldn't match kind ‘*’ with ‘#’
+    When matching types
       t1 :: *
       GHC.Prim.Int# :: #
     Relevant bindings include