diff options
17 files changed, 143 insertions, 129 deletions
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index f46bdfd2d9..bff59ee274 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -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. %************************************************************************ diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 4fff6ab45a..ceb517d74a 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -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 diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr index f9108f2849..afb9902adf 100644 --- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr +++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr @@ -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)’ diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr index 0fc428e183..7b4837c8b9 100644 --- a/testsuite/tests/typecheck/should_fail/T3950.stderr +++ b/testsuite/tests/typecheck/should_fail/T3950.stderr @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/T5570.stderr b/testsuite/tests/typecheck/should_fail/T5570.stderr index 626533cdaa..21a4e0cfbe 100644 --- a/testsuite/tests/typecheck/should_fail/T5570.stderr +++ b/testsuite/tests/typecheck/should_fail/T5570.stderr @@ -1,8 +1,9 @@ -
-T5570.hs:7:16:
- Kind incompatibility 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##
+ +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## diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr index c2e6360018..2a022645d8 100644 --- a/testsuite/tests/typecheck/should_fail/T7368.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368.stderr @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr index 1316d5a8d4..79396df9d7 100644 --- a/testsuite/tests/typecheck/should_fail/T7368a.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr @@ -1,11 +1,12 @@ -
-T7368a.hs:8:6:
- Couldn't match type ‘f’ with ‘Bad’
- ‘f’ is a rigid type variable bound by
- the type signature for fun :: f (Bad f) -> Bool at T7368a.hs:7:15
- 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
+ +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 diff --git a/testsuite/tests/typecheck/should_fail/T8262.stderr b/testsuite/tests/typecheck/should_fail/T8262.stderr index 44c2fb861a..9bc46e3ebe 100644 --- a/testsuite/tests/typecheck/should_fail/T8262.stderr +++ b/testsuite/tests/typecheck/should_fail/T8262.stderr @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr index 8ee8cccb4a..d9d2aafd53 100644 --- a/testsuite/tests/typecheck/should_fail/T8603.stderr +++ b/testsuite/tests/typecheck/should_fail/T8603.stderr @@ -1,22 +1,25 @@ -
-T8603.hs:29:17:
- Couldn't match type ‘(->) [a0]’ with ‘[Integer]’
- 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]
+ +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] diff --git a/testsuite/tests/typecheck/should_fail/mc21.stderr b/testsuite/tests/typecheck/should_fail/mc21.stderr index 337c84369b..2305394260 100644 --- a/testsuite/tests/typecheck/should_fail/mc21.stderr +++ b/testsuite/tests/typecheck/should_fail/mc21.stderr @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/mc22.stderr b/testsuite/tests/typecheck/should_fail/mc22.stderr index f3da3c5eeb..44a2eebdc7 100644 --- a/testsuite/tests/typecheck/should_fail/mc22.stderr +++ b/testsuite/tests/typecheck/should_fail/mc22.stderr @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/mc25.stderr b/testsuite/tests/typecheck/should_fail/mc25.stderr index 6af388febe..e101f4b328 100644 --- a/testsuite/tests/typecheck/should_fail/mc25.stderr +++ b/testsuite/tests/typecheck/should_fail/mc25.stderr @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/tcfail090.stderr b/testsuite/tests/typecheck/should_fail/tcfail090.stderr index c4a8a31b60..37f96659cc 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail090.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail090.stderr @@ -1,7 +1,8 @@ -
-tcfail090.hs:11:9:
- Kind incompatibility when matching types:
- a0 :: *
- ByteArray# :: #
- In the expression: my_undefined
- In an equation for ‘die’: die _ = my_undefined
+ +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 diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr index b643d585a8..6ad75f49ca 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/tcfail123.stderr b/testsuite/tests/typecheck/should_fail/tcfail123.stderr index 1fcb62d1a3..1bc0246817 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail123.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail123.stderr @@ -1,8 +1,9 @@ -
-tcfail123.hs:11:9:
- Kind incompatibility 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#
+ +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# diff --git a/testsuite/tests/typecheck/should_fail/tcfail159.stderr b/testsuite/tests/typecheck/should_fail/tcfail159.stderr index 9154e4383e..a8ae57b510 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail159.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail159.stderr @@ -1,8 +1,9 @@ -
-tcfail159.hs:9:11:
- Kind incompatibility 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 }
+ +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 } diff --git a/testsuite/tests/typecheck/should_fail/tcfail200.stderr b/testsuite/tests/typecheck/should_fail/tcfail200.stderr index 5a35839689..ba9f0ceb54 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail200.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail200.stderr @@ -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 |