Commit 20632d37 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Do not discard insoluble Derived constraints

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.
parent 74ae5989
......@@ -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.
%************************************************************************
......
......@@ -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
......
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)’
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
......
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##
T7368.hs:3:10:
Kind incompatibility when matching types:
Couldn't match kind ‘* -> *’ with ‘*’
When matching types
c0 :: (* -> *) -> *
(->) a0 :: * -> *
Expected type: a0 -> b0
......
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
T8262.hs:5:15:
Kind incompatibility when matching types:
Couldn't match kind ‘*’ with ‘#’
When matching types
a :: *
GHC.Prim.Int# :: #
Relevant bindings include
......
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]
......@@ -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
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
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
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
tcfail122.hs:8:9:
Kind incompatibility when matching types:
Couldn't match kind ‘* -> *’ with ‘*’
When matching types
c0 :: (* -> *) -> *
a :: * -> *
Expected type: a b
......
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#
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 }
tcfail200.hs:5:15:
Kind incompatibility when matching types:
Couldn't match kind ‘*’ with ‘#’
When matching types
t1 :: *
GHC.Prim.Int# :: #
Relevant bindings include
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment