Commit 97db0edc authored by Simon Peyton Jones's avatar Simon Peyton Jones

Re-engineer the ambiguity test for user type signatures

Two main changes. First, re-engineer the ambiguity test.  Previously
TcMType.checkAmbiguity used a rather syntactic test to detect some
types that are certainly ambiguous.  But a much easier test is available,
and it is used for inferred types in TcBinds. Namely
    <type> is ambiguous
iff
   <type> `TcUnify.isSubType` <type>
fails to hold, where "isSubType" means "is provably more polymorphic than".
Example:
      C a => Int
is ambiguous, because isSubType instantiates the (C a => Int)
to (C alpha => Int) and then tries to deduce (C alpha) from (C a). This is
Martin Sulzmann's definition of ambiguity.  (Defn 10 of "Understanding
functional dependencies via constraint handling rules", JFP.)

This change is neat, reduces code, and correctly rejects more programs.
However is *is* just possible to have a useful program that would be
rejected. For example
          class C a b
          f :: C Int b => Int -> Int
Here 'f' would be rejected as having an ambiguous type. But it is
just possible that, at a *call* site there might be an instance
declaration  instance C Int b, which does not constrain 'b' at all.
This is pretty strange -- why is 'b' overloaded at all? -- but it's
possible, so I also added a flag -XAllowAmbiguousTypes that simply
removes the ambiguity check.  Let's see if anyone cares.  Meanwhile
the earlier error report will be useful for everyone else.

A handful of regression tests had to be adjusted as a result, because
they used ambiguous types, somewhat accidentally.

Second, split TcMType (already too large) into two

  * TcMType: a low-level module dealing with monadic operations like
    zonking, creating new evidence variables, etc

  * TcValidity: a brand-new higher-level module dealing with
    validity checking for types: checkValidType, checkValidInstance,
    checkFamInstPats etc

Apart from the fact that TcMType was too big, this allows TcValidity
to import TcUnify(tcSubType) without causing a loop.
parent afe9a3b0
......@@ -362,6 +362,7 @@ Library
TcHsType
TcInstDcls
TcMType
TcValidity
TcMatches
TcPat
TcRnDriver
......
......@@ -468,6 +468,7 @@ data ExtensionFlag
| Opt_ImplicitParams
| Opt_ImplicitPrelude
| Opt_ScopedTypeVariables
| Opt_AllowAmbiguousTypes
| Opt_UnboxedTuples
| Opt_BangPatterns
| Opt_TypeFamilies
......@@ -2585,6 +2586,7 @@ xFlags = [
( "ExtendedDefaultRules", Opt_ExtendedDefaultRules, nop ),
( "ImplicitParams", Opt_ImplicitParams, nop ),
( "ScopedTypeVariables", Opt_ScopedTypeVariables, nop ),
( "AllowAmbiguousTypes", Opt_AllowAmbiguousTypes, nop),
( "PatternSignatures", Opt_ScopedTypeVariables,
deprecatedForExtension "ScopedTypeVariables" ),
......
......@@ -601,7 +601,7 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
prag_sigs = prag_fn poly_name
origin = AmbigOrigin poly_name
origin = AmbigOrigin sig_ctxt
sig_ctxt = InfSigCtxt poly_name
\end{code}
......@@ -1162,16 +1162,28 @@ For example:
(Instantiation is only necessary because of type synonyms. Otherwise,
it's all cool; each signature has distinct type variables from the renamer.)
Note [Fail eagerly on bad signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If a type signaure is wrong, fail immediately:
* the type sigs may bind type variables, so proceeding without them
can lead to a cascade of errors
* the type signature might be ambiguous, in which case checking
the code against the signature will give a very similar error
to the ambiguity error.
ToDo: this means we fall over if any type sig
is wrong (eg at the top level of the module),
which is over-conservative
\begin{code}
tcTySigs :: [LSig Name] -> TcM ([TcId], TcSigFun)
tcTySigs hs_sigs
= do { ty_sigs <- concat <$> checkNoErrs (mapAndRecoverM tcTySig hs_sigs)
-- No recovery from bad signatures, because the type sigs
-- may bind type variables, so proceeding without them
-- can lead to a cascade of errors
-- ToDo: this means we fall over immediately if any type sig
-- is wrong, which is over-conservative, see Trac bug #745
; let env = mkNameEnv [(idName (sig_id sig), sig) | sig <- ty_sigs]
= checkNoErrs $ -- See Note [Fail eagerly on bad signatures]
do { ty_sigs_s<- mapAndRecoverM tcTySig hs_sigs
; let ty_sigs = concat ty_sigs_s
env = mkNameEnv [(idName (sig_id sig), sig) | sig <- ty_sigs]
; return (map sig_id ty_sigs, lookupNameEnv env) }
tcTySig :: LSig Name -> TcM [TcSigInfo]
......
......@@ -15,6 +15,8 @@ import DynFlags
import TcRnMonad
import FamInst
import TcErrors( reportAllUnsolved )
import TcValidity( validDerivPred )
import TcEnv
import TcTyClsDecls( tcFamTyPats, tcAddDataFamInstCtxt )
import TcClassDcl( tcAddDeclCtxt ) -- Small helper
......@@ -1433,6 +1435,136 @@ extendLocalInstEnv dfuns thing_inside
\end{code}
***********************************************************************************
* *
* Simplifyf derived constraints
* *
***********************************************************************************
\begin{code}
simplifyDeriv :: CtOrigin
-> PredType
-> [TyVar]
-> ThetaType -- Wanted
-> TcM ThetaType -- Needed
-- Given instance (wanted) => C inst_ty
-- Simplify 'wanted' as much as possibles
-- Fail if not possible
simplifyDeriv orig pred tvs theta
= do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
-- The constraint solving machinery
-- expects *TcTyVars* not TyVars.
-- We use *non-overlappable* (vanilla) skolems
-- See Note [Overlap and deriving]
; let subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
skol_set = mkVarSet tvs_skols
doc = ptext (sLit "deriving") <+> parens (ppr pred)
; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
; traceTc "simplifyDeriv" $
vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
; (residual_wanted, _ev_binds1)
<- solveWantedsTcM (mkFlatWC wanted)
-- Post: residual_wanted are already zonked
; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
-- See Note [Exotic derived instance contexts]
get_good :: Ct -> Either PredType Ct
get_good ct | validDerivPred skol_set p
, isWantedCt ct = Left p
-- NB: residual_wanted may contain unsolved
-- Derived and we stick them into the bad set
-- so that reportUnsolved may decide what to do with them
| otherwise = Right ct
where p = ctPred ct
-- We never want to defer these errors because they are errors in the
-- compiler! Hence the `False` below
; reportAllUnsolved (residual_wanted { wc_flat = bad })
; let min_theta = mkMinimalBySCs (bagToList good)
; return (substTheta subst_skol min_theta) }
\end{code}
Note [Overlap and deriving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider some overlapping instances:
data Show a => Show [a] where ..
data Show [Char] where ...
Now a data type with deriving:
data T a = MkT [a] deriving( Show )
We want to get the derived instance
instance Show [a] => Show (T a) where...
and NOT
instance Show a => Show (T a) where...
so that the (Show (T Char)) instance does the Right Thing
It's very like the situation when we're inferring the type
of a function
f x = show [x]
and we want to infer
f :: Show [a] => a -> String
BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
the context for the derived instance.
Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
Note [Exotic derived instance contexts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a 'derived' instance declaration, we *infer* the context. It's a
bit unclear what rules we should apply for this; the Haskell report is
silent. Obviously, constraints like (Eq a) are fine, but what about
data T f a = MkT (f a) deriving( Eq )
where we'd get an Eq (f a) constraint. That's probably fine too.
One could go further: consider
data T a b c = MkT (Foo a b c) deriving( Eq )
instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
Notice that this instance (just) satisfies the Paterson termination
conditions. Then we *could* derive an instance decl like this:
instance (C Int a, Eq b, Eq c) => Eq (T a b c)
even though there is no instance for (C Int a), because there just
*might* be an instance for, say, (C Int Bool) at a site where we
need the equality instance for T's.
However, this seems pretty exotic, and it's quite tricky to allow
this, and yet give sensible error messages in the (much more common)
case where we really want that instance decl for C.
So for now we simply require that the derived instance context
should have only type-variable constraints.
Here is another example:
data Fix f = In (f (Fix f)) deriving( Eq )
Here, if we are prepared to allow -XUndecidableInstances we
could derive the instance
instance Eq (f (Fix f)) => Eq (Fix f)
but this is so delicate that I don't think it should happen inside
'deriving'. If you want this, write it yourself!
NB: if you want to lift this condition, make sure you still meet the
termination conditions! If not, the deriving mechanism generates
larger and larger constraints. Example:
data Succ a = S a
data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
Note the lack of a Show instance for Succ. First we'll generate
instance (Show (Succ a), Show a) => Show (Seq a)
and then
instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
and so on. Instead we want to complain of no instance for (Show (Succ a)).
The bottom line
~~~~~~~~~~~~~~~
Allow constraints which consist only of type variables, with no repeats.
%************************************************************************
%* *
\subsection[TcDeriv-normal-binds]{Bindings for the various classes}
......
......@@ -285,7 +285,7 @@ mkUniReporter :: (ReportErrCtxt -> Ct -> TcM ErrMsg) -> Reporter
mkUniReporter mk_err ctxt
= mapM_ $ \ct ->
do { err <- mk_err ctxt ct
; maybeReportError ctxt err ct
; maybeReportError ctxt err
; maybeAddDeferredBinding ctxt err ct }
mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
......@@ -297,23 +297,23 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
mkGroupReporter _ _ []
= return ()
mkGroupReporter mk_err ctxt (ct1 : rest)
= do { err <- mk_err ctxt cts
; maybeReportError ctxt err ct1
; mapM_ (maybeAddDeferredBinding ctxt err) (ct1:rest)
= do { err <- mk_err ctxt first_group
; maybeReportError ctxt err
; mapM_ (maybeAddDeferredBinding ctxt err) first_group
-- Add deferred bindings for all
; mkGroupReporter mk_err ctxt others }
where
loc = cc_loc ct1
cts = ct1 : friends
first_group = ct1 : friends
(friends, others) = partition is_friend rest
is_friend friend = cc_loc friend `same_loc` loc
same_loc :: CtLoc -> CtLoc -> Bool
same_loc l1 l2 = ctLocSpan l1 == ctLocSpan l2
maybeReportError :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
-- Report the error and/or make a deferred binding for it
maybeReportError ctxt err _ct
maybeReportError ctxt err
| cec_defer ctxt -- We have -fdefer-type-errors
-- so warn about all, even if cec_suppress is on
= reportWarning (makeIntoWarning err)
......@@ -494,9 +494,8 @@ mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
----------------
mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkIPErr ctxt cts
= do { (ctxt, _, ambig_err) <- mkAmbigMsg ctxt cts
; (ctxt, bind_msg) <- relevantBindings ctxt ct1
; mkErrorMsg ctxt ct1 (msg $$ ambig_err $$ bind_msg) }
= do { (ctxt, bind_msg) <- relevantBindings ctxt ct1
; mkErrorMsg ctxt ct1 (msg $$ bind_msg) }
where
(ct1:_) = cts
orig = ctLocOrigin (cc_loc ct1)
......@@ -605,8 +604,8 @@ reportEqErr :: ReportErrCtxt -> SDoc
-> Maybe SwapFlag -- Nothing <=> not sure
-> TcType -> TcType -> TcM ErrMsg
reportEqErr ctxt extra1 ct oriented ty1 ty2
= do { (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
; mkErrorMsg ctxt' ct (vcat [ misMatchOrCND ctxt' ct oriented ty1 ty2
= do { let extra2 = mkEqInfoMsg ct ty1 ty2
; mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
, extra2, extra1]) }
mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> SDoc -> Ct
......@@ -629,8 +628,8 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
| OC_Occurs <- occ_check_expand
= do { let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:")
2 (sep [ppr ty1, char '~', ppr ty2])
; (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
; mkErrorMsg ctxt' ct (occCheckMsg $$ extra2 $$ extra) }
extra2 = mkEqInfoMsg ct ty1 ty2
; mkErrorMsg ctxt ct (occCheckMsg $$ extra2 $$ extra) }
| OC_Forall <- occ_check_expand
= do { let msg = vcat [ ptext (sLit "Cannot instantiate unification variable")
......@@ -694,20 +693,22 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
k2 = typeKind ty2
ty1 = mkTyVarTy tv1
mkEqInfoMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> TcM (ReportErrCtxt, SDoc)
mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
-- Report (a) ambiguity if either side is a type function application
-- e.g. F a0 ~ Int
-- (b) warning about injectivity if both sides are the same
-- type function application F a ~ F b
-- See Note [Non-injective type functions]
mkEqInfoMsg ctxt ct ty1 ty2
= do { (ctxt', _, ambig_msg) <- if isJust mb_fun1 || isJust mb_fun2
then mkAmbigMsg ctxt [ct]
else return (ctxt, False, empty)
; return (ctxt', tyfun_msg $$ ambig_msg) }
mkEqInfoMsg ct ty1 ty2
= tyfun_msg $$ ambig_msg
where
mb_fun1 = isTyFun_maybe ty1
mb_fun2 = isTyFun_maybe ty2
ambig_msg | isJust mb_fun1 || isJust mb_fun2
= snd (mkAmbigMsg ct)
| otherwise = empty
tyfun_msg | Just tc1 <- mb_fun1
, Just tc2 <- mb_fun2
, tc1 == tc2
......@@ -891,7 +892,7 @@ mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
-- from an overlap (returning Left clas), otherwise return (Right pred)
mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
| null matches -- No matches but perhaps several unifiers
= do { (ctxt, is_ambig, ambig_msg) <- mkAmbigMsg ctxt [ct]
= do { let (is_ambig, ambig_msg) = mkAmbigMsg ct
; (ctxt, binds_msg) <- relevantBindings ctxt ct
; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg)
; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) }
......@@ -912,19 +913,22 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg
= vcat [ addArising orig (no_inst_herald <+> pprParendType pred)
, vcat (pp_givens givens)
, if (has_ambig_tvs && not (null unifiers && null givens))
then vcat [ ambig_msg, binds_msg, potential_msg ]
else empty
, ppWhen (has_ambig_tvs && not (null unifiers && null givens))
(vcat [ ambig_msg, binds_msg, potential_msg ])
, show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
potential_msg
| null unifiers = empty
| otherwise
= hang (if isSingleton unifiers
= ppWhen (not (null unifiers) && want_potential orig) $
hang (if isSingleton unifiers
then ptext (sLit "Note: there is a potential instance available:")
else ptext (sLit "Note: there are several potential instances:"))
2 (ppr_insts unifiers)
-- Report "potential instances" only when the constraint arises
-- directly from the user's use of an overloaded function
want_potential (AmbigOrigin {}) = False
want_potential _ = True
add_to_ctxt_fixes has_ambig_tvs
| not has_ambig_tvs && all_tyvars
, (orig:origs) <- mapCatMaybes get_good_orig (cec_encl ctxt)
......@@ -960,15 +964,14 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
vcat [ addArising orig (ptext (sLit "Overlapping instances for")
<+> pprType (mkClassPred clas tys))
, if not (null matching_givens) then
, ppUnless (null matching_givens) $
sep [ptext (sLit "Matching givens (or their superclasses):")
, nest 2 (vcat matching_givens)]
else empty
, sep [ptext (sLit "Matching instances:"),
nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
, if null matching_givens && isSingleton matches && null unifiers then
, ppWhen (null matching_givens && isSingleton matches && null unifiers) $
-- Intuitively, some given matched the wanted in their
-- flattened or rewritten (from given equalities) form
-- but the matcher can't figure that out because the
......@@ -977,18 +980,14 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
-- context. Accelerate Smart.hs showed this problem.
sep [ ptext (sLit "There exists a (perhaps superclass) match:")
, nest 2 (vcat (pp_givens givens))]
else empty
, if not (isSingleton matches)
then -- Two or more matches
empty
else -- One match
parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
quotes (pprWithCommas ppr (varSetElems (tyVarsOfTypes tys))),
if null (matching_givens) then
vcat [ ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
ptext (sLit "when compiling the other instance declarations")]
else empty])]
, ppWhen (isSingleton matches) $
parens (vcat [ ptext (sLit "The choice depends on the instantiation of") <+>
quotes (pprWithCommas ppr (varSetElems (tyVarsOfTypes tys)))
, ppWhen (null (matching_givens)) $
vcat [ ptext (sLit "To pick the first instance above, use -XIncoherentInstances")
, ptext (sLit "when compiling the other instance declarations")]
])]
where
ispecs = [ispec | (ispec, _) <- matches]
......@@ -1091,59 +1090,25 @@ that match such things. And flattening under a for-all is problematic
anyway; consider C (forall a. F a)
\begin{code}
mkAmbigMsg :: ReportErrCtxt -> [Ct]
-> TcM (ReportErrCtxt, Bool, SDoc)
mkAmbigMsg ctxt cts
| isEmptyVarSet ambig_tv_set
= return (ctxt, False, empty)
| otherwise
= do { dflags <- getDynFlags
; prs <- mapSndM zonkTcType $
[ (id, idType id) | TcIdBndr id top_lvl <- ct1_bndrs
, isTopLevel top_lvl ]
; let ambig_ids = [id | (id, zonked_ty) <- prs
, tyVarsOfType zonked_ty `intersectsVarSet` ambig_tv_set]
; return (ctxt, True, mk_msg dflags ambig_ids) }
mkAmbigMsg :: Ct -> (Bool, SDoc)
mkAmbigMsg ct
| isEmptyVarSet ambig_tv_set = (False, empty)
| otherwise = (True, msg)
where
ct1:_ = cts
ct1_bndrs = tcl_bndrs (ctLocEnv (cc_loc ct1))
ambig_tv_set = foldr (unionVarSet . filterVarSet isAmbiguousTyVar . tyVarsOfCt)
emptyVarSet cts
ambig_tv_set = filterVarSet isAmbiguousTyVar (tyVarsOfCt ct)
ambig_tvs = varSetElems ambig_tv_set
is_or_are | isSingleton ambig_tvs = text "is"
| otherwise = text "are"
mk_msg dflags ambig_ids
| any isRuntimeUnkSkol ambig_tvs -- See Note [Runtime skolems]
= vcat [ ptext (sLit "Cannot resolve unknown runtime type") <> plural ambig_tvs
<+> pprQuotedList ambig_tvs
, ptext (sLit "Use :print or :force to determine these types")]
| otherwise
= vcat [ text "The type variable" <> plural ambig_tvs
<+> pprQuotedList ambig_tvs
<+> is_or_are <+> text "ambiguous"
, mk_extra_msg dflags ambig_ids ]
mk_extra_msg dflags ambig_ids
| null ambig_ids
= ptext (sLit "Possible fix: add a type signature that fixes these type variable(s)")
-- This happens in things like
-- f x = show (read "foo")
-- where monomorphism doesn't play any role
| otherwise
= vcat [ hang (ptext (sLit "Possible cause: the monomorphism restriction applied to:"))
2 (pprWithCommas (quotes . ppr) ambig_ids)
, ptext (sLit "Probable fix:") <+> vcat
[ ptext (sLit "give these definition(s) an explicit type signature")
, if xopt Opt_MonomorphismRestriction dflags
then ptext (sLit "or use -XNoMonomorphismRestriction")
else empty ] -- Only suggest adding "-XNoMonomorphismRestriction"
-- if it is not already set!
]
msg | any isRuntimeUnkSkol ambig_tvs -- See Note [Runtime skolems]
= vcat [ ptext (sLit "Cannot resolve unknown runtime type") <> plural ambig_tvs
<+> pprQuotedList ambig_tvs
, ptext (sLit "Use :print or :force to determine these types")]
| otherwise
= vcat [ text "The type variable" <> plural ambig_tvs
<+> pprQuotedList ambig_tvs
<+> is_or_are <+> text "ambiguous" ]
pprSkol :: SkolemInfo -> SrcLoc -> SDoc
pprSkol UnkSkol _
......
......@@ -10,12 +10,10 @@ module TcEvidence (
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet,
idHsWrapper, isIdHsWrapper, pprHsWrapper,
-- Evidence bindin
-- Evidence bindings
TcEvBinds(..), EvBindsVar(..),
EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
EvTerm(..), mkEvCast, evVarsOfTerm,
EvLit(..), evTermCoercion,
......
......@@ -50,6 +50,7 @@ import TcRnMonad
import TcEvidence( HsWrapper )
import TcEnv
import TcMType
import TcValidity
import TcUnify
import TcIface
import TcType
......
......@@ -28,6 +28,7 @@ import TcClassDcl( tcClassDecl2,
findMethodBind, instantiateMethod, tcInstanceMethodBody )
import TcPat ( addInlinePrags )
import TcRnMonad
import TcValidity
import TcMType
import TcType
import BuildTyCl
......
This diff is collapsed.
......@@ -31,6 +31,7 @@ import Var
import Name
import TcEnv
import TcMType
import TcValidity( arityErr )
import TcType
import TcUnify
import TcHsType
......
......@@ -1523,7 +1523,7 @@ data CtOrigin
| PArrSeqOrigin (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
| SectionOrigin
| TupleOrigin -- (..,..)
| AmbigOrigin Name -- f :: ty
| AmbigOrigin UserTypeCtxt -- Will be FunSigCtxt, InstDeclCtxt, or SpecInstCtxt
| ExprSigOrigin -- e :: ty
| PatSigOrigin -- p :: ty
| PatOrigin -- Instantiating a polytyped pattern at a constructor
......@@ -1549,7 +1549,11 @@ pprO AppOrigin = ptext (sLit "an application")
pprO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
pprO (IPOccOrigin name) = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
pprO RecordUpdOrigin = ptext (sLit "a record update")
pprO (AmbigOrigin name) = ptext (sLit "the ambiguity check for") <+> quotes (ppr name)
pprO (AmbigOrigin ctxt) = ptext (sLit "the ambiguity check for")
<+> case ctxt of
FunSigCtxt name -> quotes (ppr name)
InfSigCtxt name -> quotes (ppr name)
_ -> pprUserTypeCtxt ctxt
pprO ExprSigOrigin = ptext (sLit "an expression type signature")
pprO PatSigOrigin = ptext (sLit "a pattern type signature")
pprO PatOrigin = ptext (sLit "a pattern")
......
......@@ -1206,6 +1206,7 @@ emitInsoluble ct
= do { traceTcS "Emit insoluble" (ppr ct)
; updInertTcS add_insol }
where
this_pred = ctPred ct
add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
| already_there = is
| otherwise = is { inert_cans = ics { inert_insols = extendCts old_insols ct } }
......@@ -1213,8 +1214,6 @@ emitInsoluble ct
already_there = not (isWantedCt ct) && anyBag (eqType this_pred . ctPred) old_insols
-- See Note [Do not add duplicate derived insolubles]
this_pred = ctPred ct
getTcSImplicsRef :: TcS (IORef (Bag Implication))
getTcSImplicsRef = TcS (return . tcs_implics)
......@@ -1311,8 +1310,10 @@ zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
Note [Do not add duplicate derived insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In general we *do* want to add an insoluble (Int ~ Bool) even if there is one
such there already, because they may come from distinct call sites. But for
In general we *must* add an insoluble (Int ~ Bool) even if there is
one such there already, because they may come from distinct call
sites. Not only do we want an error message for each, but with
-fdefer-type-errors we must generate evidence for each. But for
*derived* insolubles, we only want to report each one once. Why?
(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
......
......@@ -8,7 +8,7 @@
module TcSimplify(
simplifyInfer, simplifyAmbiguityCheck,
simplifyDefault, simplifyDeriv,
simplifyDefault,
simplifyRule, simplifyTop, simplifyInteractive,
solveWantedsTcM
) where
......@@ -30,7 +30,6 @@ import Unique
import VarSet
import VarEnv
import TcEvidence
import TypeRep
import Name
import Bag
import ListSetOps
......@@ -177,135 +176,6 @@ simplifyDefault theta
\end{code}
***********************************************************************************
* *
* Deriving *
* *
***********************************************************************************
\begin{code}
simplifyDeriv :: CtOrigin
-> PredType
-> [TyVar]
-> ThetaType -- Wanted
-> TcM ThetaType -- Needed
-- Given instance (wanted) => C inst_ty
-- Simplify 'wanted' as much as possibles
-- Fail if not possible
simplifyDeriv orig pred tvs theta
= do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
-- The constraint solving machinery
-- expects *TcTyVars* not TyVars.
-- We use *non-overlappable* (vanilla) skolems
-- See Note [Overlap and deriving]
; let subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
skol_set = mkVarSet tvs_skols
doc = ptext (sLit "deriving") <+> parens (ppr pred)
; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
; traceTc "simplifyDeriv" $
vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
; (residual_wanted, _ev_binds1)
<- solveWantedsTcM (mkFlatWC wanted)
-- Post: residual_wanted are already zonked
; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
-- See Note [Exotic derived instance contexts]
get_good :: Ct -> Either PredType Ct
get_good ct | validDerivPred skol_set p
, isWantedCt ct = Left p
-- NB: residual_wanted may contain unsolved
-- Derived and we stick them into the bad set
-- so that reportUnsolved may decide what to do with them
| otherwise = Right ct
where p = ctPred ct
-- We never want to defer these errors because they are errors in the
-- compiler! Hence the `False` below
; reportAllUnsolved (residual_wanted { wc_flat = bad })
; let min_theta = mkMinimalBySCs (bagToList good)
; return (substTheta subst_skol min_theta) }
\end{code}
Note [Overlap and deriving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider some overlapping instances:
data Show a => Show [a] where ..
data Show [Char] where ...
Now a data type with deriving:
data T a = MkT [a] deriving( Show )
We want to get the derived instance
instance Show [a] => Show (T a) where...
and NOT
instance Show a => Show (T a) where...
so that the (Show (T Char)) instance does the Right Thing
It's very like the situation when we're inferring the type
of a function
f x = show [x]
and we want to infer
f :: Show [a] => a -> String
BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
the context for the derived instance.
Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
Note [Exotic derived instance contexts]