Commit 56f8777f authored by Simon Peyton Jones's avatar Simon Peyton Jones

Improve error message in Trac #8883

The improvement is to report the inferred type in the error message,
as suggested in email on ghc-deves (10 Jun 14).
parent edd57645
......@@ -39,6 +39,7 @@ import TysPrim
import Id
import Var
import VarSet
import VarEnv( TidyEnv )
import Module
import Name
import NameSet
......@@ -56,7 +57,7 @@ import FastString
import Type(mkStrLitTy)
import Class(classTyCon)
import PrelNames(ipClassName)
import TcValidity (checkValidTheta)
import TcValidity (checkValidType)
import Control.Monad
......@@ -561,16 +562,11 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
; traceTc "simplifyInfer call" (ppr name_taus $$ ppr wanted)
; (qtvs, givens, mr_bites, ev_binds) <-
simplifyInfer closed mono name_taus wanted
; theta <- zonkTcThetaType (map evVarPred givens)
-- We need to check inferred theta for validity. The reason is that we
-- might have inferred theta that requires language extension that is
-- not turned on. See #8883. Example can be found in the T8883 testcase.
; checkValidTheta (InfSigCtxt (fst . head $ name_taus)) theta
; exports <- checkNoErrs $ mapM (mkExport prag_fn qtvs theta) mono_infos
; (qtvs, givens, mr_bites, ev_binds)
<- simplifyInfer closed mono name_taus wanted
; theta <- zonkTcThetaType (map evVarPred givens)
; exports <- checkNoErrs $ mapM (mkExport prag_fn qtvs theta) mono_infos
; loc <- getSrcSpanM
; let poly_ids = map abe_poly exports
final_closed | closed && not mr_bites = TopLevel
......@@ -605,20 +601,12 @@ mkExport :: PragFun
mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
= do { mono_ty <- zonkTcType (idType mono_id)
; let poly_id = case mb_sig of
Nothing -> mkLocalId poly_name inferred_poly_ty
Just sig -> sig_id sig
-- poly_id has a zonked type
-- In the inference case (no signature) this stuff figures out
-- the right type variables and theta to quantify over
-- See Note [Impedence matching]
my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType mono_ty))
-- Include kind variables! Trac #7916
my_tvs = filter (`elemVarSet` my_tvs2) qtvs -- Maintain original order
my_theta = filter (quantifyPred my_tvs2) theta
inferred_poly_ty = mkSigmaTy my_tvs my_theta mono_ty
; poly_id <- case mb_sig of
Just sig -> return (sig_id sig)
Nothing -> mkInferredPolyId poly_name qtvs theta mono_ty
-- NB: poly_id has a zonked type
; poly_id <- addInlinePrags poly_id prag_sigs
; spec_prags <- tcSpecPrags poly_id prag_sigs
-- tcPrags requires a zonked poly_id
......@@ -634,7 +622,7 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
-- closed (unless we are doing NoMonoLocalBinds in which case all bets
-- are off)
-- See Note [Impedence matching]
; (wrap, wanted) <- addErrCtxtM (mk_msg poly_id) $
; (wrap, wanted) <- addErrCtxtM (mk_bind_msg inferred True poly_name (idType poly_id)) $
captureConstraints $
tcSubType origin sig_ctxt sel_poly_ty (idType poly_id)
; ev_binds <- simplifyTop wanted
......@@ -645,24 +633,58 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
, abe_prags = SpecPrags spec_prags }) }
where
inferred = isNothing mb_sig
mk_msg poly_id tidy_env
= return (tidy_env', msg)
where
msg | inferred = hang (ptext (sLit "When checking that") <+> pp_name)
2 (ptext (sLit "has the inferred type") <+> pp_ty)
$$ ptext (sLit "Probable cause: the inferred type is ambiguous")
| otherwise = hang (ptext (sLit "When checking that") <+> pp_name)
2 (ptext (sLit "has the specified type") <+> pp_ty)
pp_name = quotes (ppr poly_name)
pp_ty = quotes (ppr tidy_ty)
(tidy_env', tidy_ty) = tidyOpenType tidy_env (idType poly_id)
prag_sigs = prag_fn poly_name
origin = AmbigOrigin sig_ctxt
sig_ctxt = InfSigCtxt poly_name
mkInferredPolyId :: Name -> [TyVar] -> TcThetaType -> TcType -> TcM Id
-- In the inference case (no signature) this stuff figures out
-- the right type variables and theta to quantify over
-- See Note [Validity of inferred types]
mkInferredPolyId poly_name qtvs theta mono_ty
= addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
do { checkValidType (InfSigCtxt poly_name) inferred_poly_ty
; return (mkLocalId poly_name inferred_poly_ty) }
where
my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType mono_ty))
-- Include kind variables! Trac #7916
my_tvs = filter (`elemVarSet` my_tvs2) qtvs -- Maintain original order
my_theta = filter (quantifyPred my_tvs2) theta
inferred_poly_ty = mkSigmaTy my_tvs my_theta mono_ty
mk_bind_msg :: Bool -> Bool -> Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_bind_msg inferred want_ambig poly_name poly_ty tidy_env
= return (tidy_env', msg)
where
msg = vcat [ ptext (sLit "When checking that") <+> quotes (ppr poly_name)
<+> ptext (sLit "has the") <+> what <+> ptext (sLit "type")
, nest 2 (ppr poly_name <+> dcolon <+> ppr tidy_ty)
, ppWhen want_ambig $
ptext (sLit "Probable cause: the inferred type is ambiguous") ]
what | inferred = ptext (sLit "inferred")
| otherwise = ptext (sLit "specified")
(tidy_env', tidy_ty) = tidyOpenType tidy_env poly_ty
\end{code}
Note [Validity of inferred types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to check inferred type for validity, in case it uses language
extensions that are not turned on. The principle is that if the user
simply adds the inferred type to the program source, it'll compile fine.
See #8883.
Examples that might fail:
- an inferred theta that requires type equalities e.g. (F a ~ G b)
or multi-parameter type classes
- an inferred type that includes unboxed tuples
However we don't do the ambiguity check (checkValidType omits it for
InfSigCtxt) because the impedence-matching stage, which follows
immediately, will do it and we don't want two error messages.
Moreover, because of the impedence matching stage, the ambiguity-check
suggestion of -XAllowAmbiguiousTypes will not work.
Note [Impedence matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
......
......@@ -69,6 +69,9 @@ checkAmbiguity ctxt ty
-- Then :k T should work in GHCi, not complain that
-- (T k) is ambiguous!
| InfSigCtxt {} <- ctxt -- See Note [Validity of inferred types] in TcBinds
= return ()
| otherwise
= do { traceTc "Ambiguity check for" (ppr ty)
; (subst, _tvs) <- tcInstSkolTyVars (varSetElems (tyVarsOfType ty))
......
T1897b.hs:16:1:
Could not deduce (Depend a0 ~ Depend a)
from the context (Bug a)
bound by the inferred type for ‘isValid’:
Bug a => [Depend a] -> Bool
at T1897b.hs:16:1-41
NB: ‘Depend’ is a type function, and may not be injective
The type variable ‘a0’ is ambiguous
Expected type: [Depend a] -> Bool
Actual type: [Depend a0] -> Bool
When checking that ‘isValid’
has the inferred type ‘forall a. Bug a => [Depend a] -> Bool’
Probable cause: the inferred type is ambiguous
T1897b.hs:16:1:
Could not deduce (Depend a0 ~ Depend a)
from the context (Bug a)
bound by the inferred type for ‘isValid’:
Bug a => [Depend a] -> Bool
at T1897b.hs:16:1-41
NB: ‘Depend’ is a type function, and may not be injective
The type variable ‘a0’ is ambiguous
Expected type: [Depend a] -> Bool
Actual type: [Depend a0] -> Bool
When checking that ‘isValid’ has the inferred type
isValid :: forall a. Bug a => [Depend a] -> Bool
Probable cause: the inferred type is ambiguous
T2693.hs:11:7:
Couldn't match expected type ‘TFn a’ with actual type ‘TFn a0’
NB: ‘TFn’ is a type function, and may not be injective
The type variable ‘a0’ is ambiguous
When checking that ‘x’ has the inferred type ‘forall a. TFn a’
Probable cause: the inferred type is ambiguous
In the expression:
do { let Just x = ...;
let n = fst x + fst x;
return () }
In an equation for ‘f’:
f = do { let Just x = ...;
let n = ...;
return () }
T2693.hs:19:15:
Couldn't match expected type ‘(a2, b0)’ with actual type ‘TFn a3’
The type variables ‘a2’, ‘b0’, ‘a3’ are ambiguous
Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
In the first argument of ‘fst’, namely ‘x’
In the first argument of ‘(+)’, namely ‘fst x’
T2693.hs:19:23:
Couldn't match expected type ‘(a4, a2)’ with actual type ‘TFn a5’
The type variables ‘a2’, ‘a4’, ‘a5’ are ambiguous
Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
In the first argument of ‘snd’, namely ‘x’
In the second argument of ‘(+)’, namely ‘snd x’
T2693.hs:29:20:
Couldn't match type ‘TFn a0’ with ‘PVR a1’
The type variables ‘a0’, ‘a1’ are ambiguous
Expected type: () -> Maybe (PVR a1)
Actual type: () -> Maybe (TFn a0)
In the first argument of ‘mapM’, namely ‘g’
In a stmt of a 'do' block: pvs <- mapM g undefined
T2693.hs:11:7:
Couldn't match expected type ‘TFn a’ with actual type ‘TFn a0’
NB: ‘TFn’ is a type function, and may not be injective
The type variable ‘a0’ is ambiguous
When checking that ‘x’ has the inferred type
x :: forall a. TFn a
Probable cause: the inferred type is ambiguous
In the expression:
do { let Just x = ...;
let n = fst x + fst x;
return () }
In an equation for ‘f’:
f = do { let Just x = ...;
let n = ...;
return () }
T2693.hs:19:15:
Couldn't match expected type ‘(a2, b0)’ with actual type ‘TFn a3’
The type variables ‘a2’, ‘b0’, ‘a3’ are ambiguous
Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
In the first argument of ‘fst’, namely ‘x’
In the first argument of ‘(+)’, namely ‘fst x’
T2693.hs:19:23:
Couldn't match expected type ‘(a4, a2)’ with actual type ‘TFn a5’
The type variables ‘a2’, ‘a4’, ‘a5’ are ambiguous
Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
In the first argument of ‘snd’, namely ‘x’
In the second argument of ‘(+)’, namely ‘snd x’
T2693.hs:29:20:
Couldn't match type ‘TFn a0’ with ‘PVR a1’
The type variables ‘a0’, ‘a1’ are ambiguous
Expected type: () -> Maybe (PVR a1)
Actual type: () -> Maybe (TFn a0)
In the first argument of ‘mapM’, namely ‘g’
In a stmt of a 'do' block: pvs <- mapM g undefined
T9171.hs:10:1:
Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
NB: ‘GetParam’ is a type function, and may not be injective
The kind variable ‘k0’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
When checking that ‘foo’
has the inferred type ‘forall (k :: BOX).
GetParam Base (GetParam Base Int)’
Probable cause: the inferred type is ambiguous
T9171.hs:10:20:
Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
NB: ‘GetParam’ is a type function, and may not be injective
The kind variable ‘k0’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
In the ambiguity check for:
forall (k :: BOX). GetParam Base (GetParam Base Int)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In an expression type signature: GetParam Base (GetParam Base Int)
In the expression: undefined :: GetParam Base (GetParam Base Int)
T9171.hs:10:1:
Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
NB: ‘GetParam’ is a type function, and may not be injective
The kind variable ‘k0’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
When checking that ‘foo’ has the inferred type
foo :: forall (k :: BOX). GetParam Base (GetParam Base Int)
Probable cause: the inferred type is ambiguous
T9171.hs:10:20:
Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
NB: ‘GetParam’ is a type function, and may not be injective
The kind variable ‘k0’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
In the ambiguity check for:
forall (k :: BOX). GetParam Base (GetParam Base Int)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In an expression type signature: GetParam Base (GetParam Base Int)
In the expression: undefined :: GetParam Base (GetParam Base Int)
tc168.hs:17:1:
Could not deduce (C a1 (a, b0))
arising from the ambiguity check for ‘g’
from the context (C a1 (a, b))
bound by the inferred type for ‘g’: C a1 (a, b) => a1 -> a
at tc168.hs:17:1-16
The type variable ‘b0’ is ambiguous
When checking that ‘g’
has the inferred type ‘forall a b a1. C a1 (a, b) => a1 -> a’
Probable cause: the inferred type is ambiguous
tc168.hs:17:1:
Could not deduce (C a1 (a, b0))
arising from the ambiguity check for ‘g’
from the context (C a1 (a, b))
bound by the inferred type for ‘g’: C a1 (a, b) => a1 -> a
at tc168.hs:17:1-16
The type variable ‘b0’ is ambiguous
When checking that ‘g’ has the inferred type
g :: forall a b a1. C a1 (a, b) => a1 -> a
Probable cause: the inferred type is ambiguous
T1897a.hs:9:1:
Could not deduce (Wob a0 b)
arising from the ambiguity check for ‘foo’
from the context (Wob a b)
bound by the inferred type for ‘foo’: Wob a b => b -> [b]
at T1897a.hs:9:1-24
The type variable ‘a0’ is ambiguous
When checking that ‘foo’
has the inferred type ‘forall a b. Wob a b => b -> [b]’
Probable cause: the inferred type is ambiguous
T1897a.hs:9:1:
Could not deduce (Wob a0 b)
arising from the ambiguity check for ‘foo’
from the context (Wob a b)
bound by the inferred type for ‘foo’: Wob a b => b -> [b]
at T1897a.hs:9:1-24
The type variable ‘a0’ is ambiguous
When checking that ‘foo’ has the inferred type
foo :: forall a b. Wob a b => b -> [b]
Probable cause: the inferred type is ambiguous
T8142.hs:6:18:
Couldn't match type ‘Nu ((,) t0)’ with ‘Nu ((,) t)’
NB: ‘Nu’ is a type function, and may not be injective
The type variable ‘t0’ is ambiguous
Expected type: Nu ((,) t) -> Nu f
Actual type: Nu ((,) t0) -> Nu f0
When checking that ‘h’
has the inferred type ‘forall t (f :: * -> *). Nu ((,) t) -> Nu f’
Probable cause: the inferred type is ambiguous
In an equation for ‘tracer’:
tracer
= h
where
h = (\ (_, b) -> ((outI . fmap h) b)) . out
T8142.hs:6:57:
Could not deduce (Nu ((,) t) ~ f1 (Nu ((,) t)))
from the context (Functor f, Coinductive f)
bound by the type signature for
tracer :: (Functor f, Coinductive f) => (c -> f c) -> c -> f c
at T8142.hs:5:11-64
Expected type: Nu ((,) t) -> (t, f1 (Nu ((,) t)))
Actual type: Nu ((,) t) -> (t, Nu ((,) t))
Relevant bindings include
h :: Nu ((,) t) -> Nu f1 (bound at T8142.hs:6:18)
In the second argument of ‘(.)’, namely ‘out’
In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
T8142.hs:6:18:
Couldn't match type ‘Nu ((,) t0)’ with ‘Nu ((,) t)’
NB: ‘Nu’ is a type function, and may not be injective
The type variable ‘t0’ is ambiguous
Expected type: Nu ((,) t) -> Nu f
Actual type: Nu ((,) t0) -> Nu f0
When checking that ‘h’ has the inferred type
h :: forall t (f :: * -> *). Nu ((,) t) -> Nu f
Probable cause: the inferred type is ambiguous
In an equation for ‘tracer’:
tracer
= h
where
h = (\ (_, b) -> ((outI . fmap h) b)) . out
T8142.hs:6:57:
Could not deduce (Nu ((,) t) ~ f1 (Nu ((,) t)))
from the context (Functor f, Coinductive f)
bound by the type signature for
tracer :: (Functor f, Coinductive f) => (c -> f c) -> c -> f c
at T8142.hs:5:11-64
Expected type: Nu ((,) t) -> (t, f1 (Nu ((,) t)))
Actual type: Nu ((,) t) -> (t, Nu ((,) t))
Relevant bindings include
h :: Nu ((,) t) -> Nu f1 (bound at T8142.hs:6:18)
In the second argument of ‘(.)’, namely ‘out’
In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
T8883.hs:17:1:
Non type-variable argument in the constraint: Functor (PF a)
(Use FlexibleContexts to permit this)
In the context: (Regular a, Functor (PF a))
While checking the inferred type for ‘fold’
T8883.hs:20:1:
Non type-variable argument in the constraint: Functor (PF a)
(Use FlexibleContexts to permit this)
When checking that ‘fold’ has the inferred type
fold :: forall a b.
(Regular a, Functor (PF a)) =>
(PF a b -> b) -> a -> b
......@@ -332,3 +332,4 @@ test('T8603', normal, compile_fail, [''])
test('T8806', normal, compile_fail, [''])
test('T8912', normal, compile_fail, [''])
test('T9033', normal, compile_fail, [''])
test('T8883', normal, compile_fail, [''])
tcfail080.hs:27:1:
Could not deduce (Collection c0 a)
arising from the ambiguity check for ‘q’
from the context (Collection c a)
bound by the inferred type for ‘q’: Collection c a => a -> Bool
at tcfail080.hs:27:1-27
The type variable ‘c0’ is ambiguous
When checking that ‘q’
has the inferred type ‘forall (c :: * -> *) a.
Collection c a =>
a -> Bool’
Probable cause: the inferred type is ambiguous
tcfail080.hs:27:1:
Could not deduce (Collection c0 a)
arising from the ambiguity check for ‘q’
from the context (Collection c a)
bound by the inferred type for ‘q’: Collection c a => a -> Bool
at tcfail080.hs:27:1-27
The type variable ‘c0’ is ambiguous
When checking that ‘q’ has the inferred type
q :: forall (c :: * -> *) a. Collection c a => a -> Bool
Probable cause: the inferred type is ambiguous
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