Commit ce6a492b authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari
Browse files

Fail fast in solveLocalEqualities

This patch makes us fail fast in TcSimplify.solveLocalEqualities,
and in TcHsType.tc_hs_sig_type, if there are insoluble constraints.

Previously we ploughed on even if there were insoluble constraints,
leading to a cascade of hard-to-understand type errors. Failing
eagerly is much better; hence a lot of testsuite error message
changes.  Eg if we have
          f :: [Maybe] -> blah
          f xs = e
then trying typecheck 'f x = e' with an utterly bogus type
is just asking for trouble.

I can't quite remember what provoked me to make this change,
but I think the error messages are notably improved, by
removing confusing clutter and focusing on the real error.

(cherry picked from commit 5c1f268e)
parent 048d4d22
......@@ -249,6 +249,10 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
tc_lvl wanted
-- See Note [Fail fast if there are insoluble kind equalities]
-- in TcSimplify
; when (insolubleWC wanted) failM
; return (mkInvForAllTys kvs ty1) }
tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
......
......@@ -152,7 +152,24 @@ solveLocalEqualities :: String -> TcM a -> TcM a
solveLocalEqualities callsite thing_inside
= do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside
; emitConstraints wanted
; return res }
-- See Note [Fail fast if there are insoluble kind equalities]
; if insolubleWC wanted
then failM
else return res }
{- Note [Fail fast if there are insoluble kind equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Rather like in simplifyInfer, fail fast if there is an insoluble
constraint. Otherwise we'll just succeed in kind-checking a nonsense
type, with a cascade of follow-up errors.
For example polykinds/T12593, T15577, and many others.
Take care to ensure that you emit the insoluble constraints before
failing, because they are what will ulimately lead to the error
messsage!
-}
solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a)
solveLocalEqualitiesX callsite thing_inside
......
......@@ -4,23 +4,7 @@ DepFail1.hs:7:6: error:
Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
• In the type signature: z :: Proxy Bool
DepFail1.hs:8:5: error:
• Couldn't match expected type ‘Proxy Bool’
with actual type ‘Proxy k0 a1’
• In the expression: P
In an equation for ‘z’: z = P
DepFail1.hs:10:16: error:
• Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
• In the second argument of ‘Proxy’, namely ‘Bool’
In the type signature: a :: Proxy Int Bool
DepFail1.hs:11:5: error:
• Couldn't match kind ‘*’ with ‘Int’
When matching types
a0 :: Int
Bool :: *
Expected type: Proxy Int Bool
Actual type: Proxy Int a0
• In the expression: P
In an equation for ‘a’: a = P
<interactive>:3:1: error:
• Couldn't match kind ‘()’ with ‘*’
When matching types
a0 :: *
'() :: ()
• In the expression: undefined :: '()
In an equation for ‘it’: it = undefined :: '()
<interactive>:3:14: error:
• Expected a type, but ‘'()’ has kind ‘()’
• In an expression type signature: '()
......@@ -19,34 +11,14 @@
In the expression: undefined :: Proxy '() Int
In an equation for ‘it’: it = undefined :: Proxy '() Int
<interactive>:5:1: error:
• Couldn't match kind ‘[*]’ with ‘*’
When matching types
a0 :: *
'[(), ()] :: [*]
• In the expression: undefined :: [(), ()]
In an equation for ‘it’: it = undefined :: [(), ()]
<interactive>:5:14: error:
• Expected a type, but ‘[(), ()]’ has kind ‘[*]’
• In an expression type signature: [(), ()]
In the expression: undefined :: [(), ()]
In an equation for ‘it’: it = undefined :: [(), ()]
<interactive>:6:1: error:
• Couldn't match kind ‘([k0], [k1])’ with ‘*’
When matching types
a0 :: *
'( '[], '[]) :: ([k0], [k1])
• In the expression: undefined :: '( '[], '[])
In an equation for ‘it’: it = undefined :: '( '[], '[])
• Relevant bindings include
it :: '( '[], '[]) (bound at <interactive>:6:1)
<interactive>:6:14: error:
• Expected a type, but ‘'( '[], '[])’ has kind ‘([k0], [k1])’
• In an expression type signature: '( '[], '[])
In the expression: undefined :: '( '[], '[])
In an equation for ‘it’: it = undefined :: '( '[], '[])
• Relevant bindings include
it :: '( '[], '[]) (bound at <interactive>:6:1)
T13877.hs:65:17: error:
• Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)’
Expected type: Sing x
-> Sing xs
-> App [a1] (':->) * p xs
-> App [a1] (':->) * p (x : xs)
Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
• In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
listElimTyFun = listElimPoly @(:->) @a @p @l
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
T13877.hs:65:41: error:
• Expecting one more argument to ‘p’
Expected kind ‘(-?>) [a1] * (':->)’, but ‘p’ has kind ‘[a1] ~> *’
Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
• In the type ‘p’
In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
......@@ -27,7 +9,7 @@ T13877.hs:65:41: error:
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a1) (xs :: [a1]).
-> (forall (x :: a) (xs :: [a]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
T11976.hs:7:7: error:
• Cannot instantiate unification variable ‘a0’
with a type involving foralls: Lens _3 _4 _5
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined :: Lens _ _ _
In an equation for ‘foo’: foo = undefined :: Lens _ _ _
• Relevant bindings include
foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
T11976.hs:7:20: error:
• Expected kind ‘k0 -> *’, but ‘Lens _ _’ has kind ‘*’
• In the type ‘Lens _ _ _’
In an expression type signature: Lens _ _ _
In the expression: undefined :: Lens _ _ _
• Relevant bindings include
foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
T12634.hs:14:19: error:
• Found type wildcard ‘_’ standing for ‘()’
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
bench_twacePow :: forall t m m' r.
_ => t m' r -> Bench '(t, m, m', r)
T12634.hs:14:58: error:
• Expected a type, but
‘'(t, m, m', r)’ has kind
‘(* -> * -> *, *, *, *)’
‘(k1 -> k2 -> *, k0, k1, k2)’
• In the first argument of ‘Bench’, namely ‘'(t, m, m', r)’
In the type ‘t m' r -> Bench '(t, m, m', r)’
In the type signature:
bench_twacePow :: forall t m m' r.
_ => t m' r -> Bench '(t, m, m', r)
T12634.hs:15:18: error:
• Couldn't match kind ‘(* -> * -> *, *, *, *)’ with ‘*’
When matching types
params0 :: *
'(t, m, m', r) :: (* -> * -> *, *, *, *)
Expected type: t m' r -> Bench '(t, m, m', r)
Actual type: t m' r -> Bench params0
• In the expression: bench (twacePowDec :: t m' r -> t m r)
In an equation for ‘bench_twacePow’:
bench_twacePow = bench (twacePowDec :: t m' r -> t m r)
• Relevant bindings include
bench_twacePow :: t m' r -> Bench '(t, m, m', r)
(bound at T12634.hs:15:1)
T15289.hs:5:16: error:
• Couldn't match expected type ‘Maybe’ with actual type ‘Bool’
• In the pattern: True
In the pattern: True :: Maybe
In the declaration for pattern synonym ‘What’
T15289.hs:5:24: error:
• Expecting one more argument to ‘Maybe’
Expected a type, but ‘Maybe’ has kind ‘* -> *’
......
T12593.hs:11:16: error:
• Expected kind ‘k0 -> k1 -> *’, but ‘Free k k1 k2 p’ has kind ‘*’
• In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:31: error:
• Expecting one more argument to ‘k’
Expected a type, but
‘k’ has kind
‘(((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint’
‘((k0 -> Constraint) -> k1 -> *) -> Constraint’
• In the kind ‘k’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:40: error:
• Expecting two more arguments to ‘k1’
Expected a type, but
‘k1’ has kind
‘((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *’
• In the kind ‘k1’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:47: error:
• Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *)
-> Constraint’
with ‘*’
When matching kinds
k3 :: *
k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint
• In the first argument of ‘p’, namely ‘c’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:49: error:
• Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *’
with ‘*’
When matching kinds
k4 :: *
k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
• In the second argument of ‘p’, namely ‘d’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:56: error:
• Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *)
-> Constraint’
with ‘*’
When matching kinds
k0 :: *
k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint
• In the first argument of ‘q’, namely ‘c’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:58: error:
• Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *’
with ‘*’
When matching kinds
k1 :: *
k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
• In the second argument of ‘q’, namely ‘d’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:14:6: error:
• Couldn't match type ‘Free k2 p0’ with ‘Free k6 k7 k8 p’
Expected type: Free k6 k7 k8 p a b
Actual type: Free k2 p0 a b
• In the pattern: Free cat
In an equation for ‘run’: run (Free cat) = cat
• Relevant bindings include
run :: Free k k4 k8 p a b
-> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b
(bound at T12593.hs:14:1)
T12593.hs:14:18: error:
• Couldn't match kind ‘*’
with ‘(((k3 -> k4 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint’
When matching kinds
k0 :: *
k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint
• In the expression: cat
In an equation for ‘run’: run (Free cat) = cat
• Relevant bindings include
cat :: forall (q :: k0 -> k1 -> *).
k2 q =>
(forall (c :: k0) (d :: k1). p0 c d -> q c d) -> q a b
(bound at T12593.hs:14:11)
run :: Free k k4 k8 p a b
-> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b
(bound at T12593.hs:14:1)
......@@ -7,65 +7,3 @@ T15577.hs:20:18: error:
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
T15577.hs:20:21: error:
• Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:20:24: error:
• Couldn't match kind ‘* -> *’ with ‘*’
When matching kinds
f1 :: * -> *
f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:20:26: error:
• Couldn't match kind ‘* -> *’ with ‘*’
When matching kinds
f1 :: * -> *
a1 :: *
• In the fourth argument of ‘f’, namely ‘r’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:21:7: error:
• Could not deduce: F r1 ~ r1
from the context: r0 ~ F r0
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
an equation for ‘g’
at T15577.hs:18:7-10
‘r1’ is a rigid type variable bound by
the type signature for:
g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1).
Proxy r1 -> F r1 :~: r1
at T15577.hs:17:1-76
Expected type: F r1 :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
......@@ -2,12 +2,3 @@
T11112.hs:3:9: error:
• Expected a type, but ‘Ord s’ has kind ‘Constraint’
• In the type signature: sort :: Ord s -> [s] -> [s]
T11112.hs:4:11: error:
• Couldn't match expected type ‘[s] -> [s]’
with actual type ‘Ord s’
• In the expression: xs
In an equation for ‘sort’: sort xs = xs
• Relevant bindings include
xs :: Ord s (bound at T11112.hs:4:6)
sort :: Ord s => [s] -> [s] (bound at T11112.hs:4:1)
T13819.hs:12:10: error:
• Couldn't match type ‘_0 -> A _0’ with ‘A a’
Expected type: a -> A a
Actual type: (_1 -> WrappedMonad A _2) (_0 -> A _0)
• In the expression: pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
In an equation for ‘pure’:
pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
In the instance declaration for ‘Applicative A’
• Relevant bindings include
pure :: a -> A a (bound at T13819.hs:12:3)
T13819.hs:12:17: error:
• Expected kind ‘* -> *’, but ‘_ -> WrappedMonad A _’ has kind ‘*’
• In the type ‘(_ -> WrappedMonad A _)’
......
......@@ -2,16 +2,3 @@
T14232.hs:3:6: error:
• Expected kind ‘* -> *’, but ‘String -> a’ has kind ‘*’
• In the type signature: f :: (String -> a) String -> a
T14232.hs:4:9: error:
• Couldn't match type ‘String -> a’ with ‘(->) t0’
Expected type: t0 -> [Char]
Actual type: (String -> a) String
• The function ‘g’ is applied to one argument,
but its type ‘(String -> a) String’ has none
In the expression: g s
In an equation for ‘f’: f g s = g s
• Relevant bindings include
s :: t0 (bound at T14232.hs:4:5)
g :: (String -> a) String (bound at T14232.hs:4:3)
f :: (String -> a) String -> a (bound at T14232.hs:4:1)
......@@ -3,16 +3,6 @@ T3540.hs:4:12: error:
• Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
• In the type signature: thing :: (a ~ Int)
T3540.hs:5:9: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
a ~ Int :: Constraint
• In the expression: undefined
In an equation for ‘thing’: thing = undefined
• Relevant bindings include
thing :: a ~ Int (bound at T3540.hs:5:1)
T3540.hs:7:20: error:
• Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
• In the type signature: thing1 :: Int -> (a ~ Int)
......
T7778.hs:3:6: error:
• Illegal qualified type: Num Int => Num
A constraint must be a monotype
Perhaps you intended to use QuantifiedConstraints
• In the type signature: v :: ((Num Int => Num) ()) => ()
T7778.hs:3:7: error:
• Expected kind ‘* -> Constraint’,
but ‘Num Int => Num’ has kind ‘*’
......
T8806.hs:5:6: error:
• Expected a constraint, but ‘Int’ has kind ‘*’
• In the type signature:
f :: Int => Int
• In the type signature: f :: Int => Int
T8806.hs:8:7: error:
• Expected a constraint, but ‘Int’ has kind ‘*’
• In the type signature:
g :: (Int => Show a) => Int
• In the type signature: g :: (Int => Show a) => Int
......@@ -25,17 +25,6 @@ VtaFail.hs:26:15: error:
In the expression: first @Int F
In an equation for ‘fInt’: fInt = first @Int F
VtaFail.hs:26:19: error:
• Couldn't match kind ‘*’ with ‘* -> *’
When matching types
a1 :: * -> *
Int :: *
Expected type: First Int
Actual type: First a1
• In the second argument of ‘first’, namely ‘F’
In the expression: first @Int F
In an equation for ‘fInt’: fInt = first @Int F
VtaFail.hs:33:18: error:
• Couldn't match type ‘Int’ with ‘Bool’
Expected type: Proxy Bool
......@@ -50,17 +39,6 @@ VtaFail.hs:40:17: error:
In the expression: too @Maybe T
In an equation for ‘threeBad’: threeBad = too @Maybe T
VtaFail.hs:40:23: error:
• Couldn't match kind ‘*’ with ‘k0 -> *’
When matching types
a0 :: * -> k0 -> *
Maybe :: * -> *
Expected type: Three Maybe
Actual type: Three a0
• In the second argument of ‘too’, namely ‘T’
In the expression: too @Maybe T
In an equation for ‘threeBad’: threeBad = too @Maybe T
VtaFail.hs:41:27: error:
• Couldn't match type ‘Either’ with ‘(->)’
Expected type: Three (->)
......
......@@ -2,12 +2,3 @@
tcfail057.hs:5:7: error:
• Expected a type, but ‘RealFrac a’ has kind ‘Constraint’
• In the type signature: f :: (RealFrac a) -> a -> a
tcfail057.hs:6:7: error:
• Couldn't match expected type ‘a -> a’
with actual type ‘RealFrac a’
• In the expression: x
In an equation for ‘f’: f x = x
• Relevant bindings include
x :: RealFrac a (bound at tcfail057.hs:6:3)
f :: RealFrac a => a -> a (bound at tcfail057.hs:6:1)
......@@ -3,23 +3,3 @@ tcfail058.hs:6:7: error:
• Expecting one more argument to ‘Array a’
Expected a constraint, but ‘Array a’ has kind ‘* -> *’
• In the type signature: f :: (Array a) => a -> b
tcfail058.hs:7:7: error:
• Could not deduce: a ~ b
from the context: Array a
bound by the type signature for:
f :: forall a b. Array a => a -> b
at tcfail058.hs:6:1-24
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a b. Array a => a -> b
at tcfail058.hs:6:1-24
‘b’ is a rigid type variable bound by
the type signature for:
f :: forall a b. Array a => a -> b
at tcfail058.hs:6:1-24
• In the expression: x
In an equation for ‘f’: f x = x
• Relevant bindings include
x :: a (bound at tcfail058.hs:7:3)
f :: a -> b (bound at tcfail058.hs:7:1)
......@@ -3,20 +3,3 @@ tcfail063.hs:6:9: error:
• Expecting one more argument to ‘Num’
Expected a constraint, but ‘Num’ has kind ‘* -> Constraint’
• In the type signature: moby :: Num => Int -> a -> Int
tcfail063.hs:7:14: error:
• Could not deduce: a ~ Int
from the context: Num
bound by the type signature for:
moby :: forall a. Num => Int -> a -> Int
at tcfail063.hs:6:1-30
‘a’ is a rigid type variable bound by
the type signature for:
moby :: forall a. Num => Int -> a -> Int
at tcfail063.hs:6:1-30
• In the second argument of ‘(+)’, namely ‘y’
In the expression: x + y
In an equation for ‘moby’: moby x y = x + y
• Relevant bindings include
y :: a (bound at tcfail063.hs:7:8)
moby :: Int -> a -> Int (bound at tcfail063.hs:7:1)
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