Commit 50bfd421 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Improve error reporting for untouchable type variables

This change adds a suggestion
    Possible fix: add a type signature for ‘f’
when we have a GADT-style definition with a
type we can't figure out.

See Note [Suggest adding a type signature] in TcErrors.

This initially came up in the discussion of Trac #8968.
parent cc3ccf9f
......@@ -48,7 +48,7 @@ import DynFlags
import ListSetOps ( equivClasses )
import Data.Maybe
import Data.List ( partition, mapAccumL, zip4 )
import Data.List ( partition, mapAccumL, zip4, nub )
\end{code}
%************************************************************************
......@@ -728,14 +728,15 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
| (implic:_) <- cec_encl ctxt -- Get the innermost context
, Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic
= do { let msg = misMatchMsg oriented ty1 ty2
untch_extra
untch_extra
= nest 2 $
sep [ quotes (ppr tv1) <+> ptext (sLit "is untouchable")
, nest 2 $ ptext (sLit "inside the constraints") <+> pprEvVarTheta given
, nest 2 $ ptext (sLit "bound by") <+> ppr skol_info
, nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ]
tv_extra = extraTyVarInfo ctxt ty1 ty2
; mkErrorMsg ctxt ct (vcat [msg, untch_extra, tv_extra, extra]) }
add_sig = suggestAddSig ctxt ty1 ty2
; mkErrorMsg ctxt ct (vcat [msg, untch_extra, tv_extra, add_sig, extra]) }
| otherwise
= reportEqErr ctxt extra ct oriented (mkTyVarTy tv1) ty2
......@@ -815,29 +816,42 @@ pp_givens givens
, ptext (sLit "at") <+> ppr loc])
extraTyVarInfo :: ReportErrCtxt -> TcType -> TcType -> SDoc
-- Add on extra info about the types themselves
-- Add on extra info about skolem constants
-- NB: The types themselves are already tidied
extraTyVarInfo ctxt ty1 ty2
= nest 2 (extra1 $$ extra2)
= nest 2 (tv_extra ty1 $$ tv_extra ty2)
where
extra1 = tyVarExtraInfoMsg (cec_encl ctxt) ty1
extra2 = tyVarExtraInfoMsg (cec_encl ctxt) ty2
tyVarExtraInfoMsg :: [Implication] -> Type -> SDoc
-- Shows a bit of extra info about skolem constants
tyVarExtraInfoMsg implics ty
| Just tv <- tcGetTyVar_maybe ty
, isTcTyVar tv, isSkolemTyVar tv
, let pp_tv = quotes (ppr tv)
= case tcTyVarDetails tv of
SkolemTv {} -> pp_tv <+> pprSkol (getSkolemInfo implics tv) (getSrcLoc tv)
FlatSkol {} -> pp_tv <+> ptext (sLit "is a flattening type variable")
RuntimeUnk {} -> pp_tv <+> ptext (sLit "is an interactive-debugger skolem")
MetaTv {} -> empty
| otherwise -- Normal case
= empty
implics = cec_encl ctxt
tv_extra ty | Just tv <- tcGetTyVar_maybe ty
, isTcTyVar tv, isSkolemTyVar tv
, let pp_tv = quotes (ppr tv)
= case tcTyVarDetails tv of
SkolemTv {} -> pp_tv <+> pprSkol (getSkolemInfo implics tv) (getSrcLoc tv)
FlatSkol {} -> pp_tv <+> ptext (sLit "is a flattening type variable")
RuntimeUnk {} -> pp_tv <+> ptext (sLit "is an interactive-debugger skolem")
MetaTv {} -> empty
| otherwise -- Normal case
= empty
suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
-- See Note [Suggest adding a type signature]
suggestAddSig ctxt ty1 ty2
| null inferred_bndrs
= empty
| [bndr] <- inferred_bndrs
= ptext (sLit "Possible fix: add a type signature for") <+> quotes (ppr bndr)
| otherwise
= ptext (sLit "Possible fix: add type signatures for some or all of") <+> (ppr inferred_bndrs)
where
inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
get_inf ty | Just tv <- tcGetTyVar_maybe ty
, isTcTyVar tv, isSkolemTyVar tv
, InferSkol prs <- getSkolemInfo (cec_encl ctxt) tv
= map fst prs
| otherwise
= []
kindErrorMsg :: TcType -> TcType -> SDoc -- Types are already tidy
kindErrorMsg ty1 ty2
= vcat [ ptext (sLit "Kind incompatibility when matching types:")
......@@ -907,6 +921,23 @@ sameOccExtra ty1 ty2
loc = nameSrcSpan nm
\end{code}
Note [Suggest adding a type signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The OutsideIn algorithm rejects GADT programs that don't have a principal
type, and indeed some that do. Example:
data T a where
MkT :: Int -> T Int
f (MkT n) = n
Does this have type f :: T a -> a, or f :: T a -> Int?
The error that shows up tends to be an attempt to unify an
untouchable type variable. So suggestAddSig sees if the offending
type variable is bound by an *inferred* signature, and suggests
adding a declared signature instead.
This initially came up in Trac #8968, concerning pattern synonyms.
Note [Disambiguating (X ~ X) errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See Trac #8278
......
......@@ -9,6 +9,7 @@ gadt-escape1.hs:19:58:
at gadt-escape1.hs:19:43-50
‘t’ is a rigid type variable bound by
the inferred type of weird1 :: t at gadt-escape1.hs:19:1
Possible fix: add a type signature for ‘weird1’
Expected type: t
Actual type: ExpGADT t1
Relevant bindings include
......
......@@ -10,6 +10,7 @@ gadt13.hs:15:13:
at gadt13.hs:15:6-8
‘t’ is a rigid type variable bound by
the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1
Possible fix: add a type signature for ‘shw’
Relevant bindings include
shw :: Term t1 -> t (bound at gadt13.hs:15:1)
In the expression: ("I " ++) . shows t
......
......@@ -11,6 +11,7 @@ gadt7.hs:16:38:
the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
‘t’ is a rigid type variable bound by
the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
Possible fix: add a type signature for ‘i1b’
Relevant bindings include
y1 :: t1 (bound at gadt7.hs:16:16)
y :: t1 (bound at gadt7.hs:16:7)
......
T7438.hs:6:14:
Couldn't match expected type ‘t1’ with actual type ‘t’
‘t’ is untouchable
inside the constraints (t2 ~ t3)
bound by a pattern with constructor
Nil :: forall (a :: k). Thrist a a,
in an equation for ‘go’
at T7438.hs:6:4-6
‘t’ is a rigid type variable bound by
the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1
‘t1’ is a rigid type variable bound by
the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1
Relevant bindings include
acc :: t (bound at T7438.hs:6:8)
go :: Thrist t2 t3 -> t -> t1 (bound at T7438.hs:6:1)
In the expression: acc
In an equation for ‘go’: go Nil acc = acc
T7438.hs:6:14:
Couldn't match expected type ‘t1’ with actual type ‘t’
‘t’ is untouchable
inside the constraints (t2 ~ t3)
bound by a pattern with constructor
Nil :: forall (a :: k). Thrist a a,
in an equation for ‘go’
at T7438.hs:6:4-6
‘t’ is a rigid type variable bound by
the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1
‘t1’ is a rigid type variable bound by
the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1
Possible fix: add a type signature for ‘go’
Relevant bindings include
acc :: t (bound at T7438.hs:6:8)
go :: Thrist t2 t3 -> t -> t1 (bound at T7438.hs:6:1)
In the expression: acc
In an equation for ‘go’: go Nil acc = acc
......@@ -7,6 +7,7 @@ T7594.hs:33:12:
at T7594.hs:33:8-19
‘b’ is a rigid type variable bound by
the inferred type of bar2 :: b at T7594.hs:33:1
Possible fix: add a type signature for ‘bar2’
Expected type: a -> b
Actual type: a -> IO ()
Relevant bindings include bar2 :: b (bound at T7594.hs:33: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