Commit 43856a00 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Improve -XAllowAmbiguousTypes (Trac #8392)

* Add a suggestion to add AllowAmbiguousTypes when there is an
  ambiguity error

* Move some of the logic to tcSimplifyAmbiguityCheck

* Report inaccessible code regardless of the ambiguity check
parent 7996d8f4
......@@ -531,18 +531,20 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
-- poly_ids are guaranteed zonked by mkExport
--------------
mkExport :: PragFun
mkExport :: PragFun
-> [TyVar] -> TcThetaType -- Both already zonked
-> MonoBindInfo
-> TcM (ABExport Id)
-- mkExport generates exports with
-- zonked type variables,
-- Only called for generalisation plan IferGen, not by CheckGen or NoGen
--
-- mkExport generates exports with
-- zonked type variables,
-- zonked poly_ids
-- The former is just because no further unifications will change
-- the quantified type variables, so we can fix their final form
-- right now.
-- The latter is needed because the poly_ids are used to extend the
-- type environment; see the invariant on TcEnv.tcExtendIdEnv
-- type environment; see the invariant on TcEnv.tcExtendIdEnv
-- Pre-condition: the qtvs and theta are already zonked
......@@ -567,20 +569,20 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
-- tcPrags requires a zonked poly_id
; let sel_poly_ty = mkSigmaTy qtvs theta mono_ty
; traceTc "mkExport: check sig"
(ppr poly_name $$ ppr sel_poly_ty $$ ppr (idType poly_id))
; traceTc "mkExport: check sig"
(ppr poly_name $$ ppr sel_poly_ty $$ ppr (idType poly_id))
-- Perform the impedence-matching and ambiguity check
-- right away. If it fails, we want to fail now (and recover
-- in tcPolyBinds). If we delay checking, we get an error cascade.
-- Remember we are in the tcPolyInfer case, so the type envt is
-- Remember we are in the tcPolyInfer case, so the type envt is
-- closed (unless we are doing NoMonoLocalBinds in which case all bets
-- are off)
-- See Note [Impedence matching]
; (wrap, wanted) <- addErrCtxtM (mk_msg poly_id) $
captureConstraints $
tcSubType origin sig_ctxt sel_poly_ty (idType poly_id)
; ev_binds <- simplifyAmbiguityCheck poly_name wanted
; ev_binds <- simplifyTop wanted
; return (ABE { abe_wrap = mkWpLet (EvBinds ev_binds) <.> wrap
, abe_poly = poly_id
......@@ -600,7 +602,6 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
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
......
......@@ -39,6 +39,8 @@ import ListSetOps
import Util
import PrelInfo
import PrelNames
import Control.Monad ( unless )
import DynFlags ( ExtensionFlag( Opt_AllowAmbiguousTypes ) )
import Class ( classKey )
import BasicTypes ( RuleName )
import Outputable
......@@ -69,26 +71,25 @@ simplifyTop wanteds
; traceTc "reportUnsolved {" empty
; binds2 <- reportUnsolved zonked_final_wc
; traceTc "reportUnsolved }" empty
; return (binds1 `unionBags` binds2) }
where
simpl_top :: WantedConstraints -> TcS WantedConstraints
-- See Note [Top-level Defaulting Plan]
simpl_top :: WantedConstraints -> TcS WantedConstraints
simpl_top wanteds
= do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
simpl_top wanteds
= do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
-- This is where the main work happens
; try_tyvar_defaulting wc_first_go }
; try_tyvar_defaulting wc_first_go }
where
try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
try_tyvar_defaulting wc
| isEmptyWC wc
| isEmptyWC wc
= return wc
| otherwise
= do { free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc)
= do { free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc)
; let meta_tvs = varSetElems (filterVarSet isMetaTyVar free_tvs)
-- zonkTyVarsAndFV: the wc_first_go is not yet zonked
-- filter isMetaTyVar: we might have runtime-skolems in GHCi,
-- filter isMetaTyVar: we might have runtime-skolems in GHCi,
-- and we definitely don't want to try to assign to those!
; meta_tvs' <- mapM defaultTyVar meta_tvs -- Has unification side effects
......@@ -98,7 +99,7 @@ simplifyTop wanteds
else do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
-- See Note [Must simplify after defaulting]
; try_class_defaulting wc_residual } }
try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
try_class_defaulting wc
| isEmptyWC wc || insolubleWC wc
......@@ -107,7 +108,7 @@ simplifyTop wanteds
| otherwise
= do { something_happened <- applyDefaultingRules (approximateWC wc)
-- See Note [Top-level Defaulting Plan]
; if something_happened
; if something_happened
then do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
; try_class_defaulting wc_residual }
else return wc }
......@@ -124,18 +125,18 @@ errors, because it isn't an error! Trac #7967 was due to this.
Note [Top-level Defaulting Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We have considered two design choices for where/when to apply defaulting.
(i) Do it in SimplCheck mode only /whenever/ you try to solve some
We have considered two design choices for where/when to apply defaulting.
(i) Do it in SimplCheck mode only /whenever/ you try to solve some
flat constraints, maybe deep inside the context of implications.
This used to be the case in GHC 7.4.1.
(ii) Do it in a tight loop at simplifyTop, once all other constraint has
(ii) Do it in a tight loop at simplifyTop, once all other constraint has
finished. This is the current story.
Option (i) had many disadvantages:
a) First it was deep inside the actual solver,
b) Second it was dependent on the context (Infer a type signature,
or Check a type signature, or Interactive) since we did not want
to always start defaulting when inferring (though there is an exception to
Option (i) had many disadvantages:
a) First it was deep inside the actual solver,
b) Second it was dependent on the context (Infer a type signature,
or Check a type signature, or Interactive) since we did not want
to always start defaulting when inferring (though there is an exception to
this see Note [Default while Inferring])
c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
f :: Int -> Bool
......@@ -156,27 +157,37 @@ go with option (i), implemented at SimplifyTop. Namely:
Now, that has to do with class defaulting. However there exists type variable /kind/
defaulting. Again this is done at the top-level and the plan is:
- At the top-level, once you had a go at solving the constraint, do
- At the top-level, once you had a go at solving the constraint, do
figure out /all/ the touchable unification variables of the wanted constraints.
- Apply defaulting to their kinds
More details in Note [DefaultTyVar].
\begin{code}
------------------
simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind)
simplifyAmbiguityCheck name wanteds
= traceTc "simplifyAmbiguityCheck" (text "name =" <+> ppr name) >>
simplifyTop wanteds -- NB: must be simplifyTop so that we
-- do ambiguity resolution.
-- See Note [Impedence matching] in TcBinds.
simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
simplifyAmbiguityCheck ty wanteds
= do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
; ev_binds_var <- newTcEvBinds
; zonked_final_wc <- solveWantedsTcMWithEvBinds ev_binds_var wanteds simpl_top
; traceTc "End simplifyAmbiguityCheck }" empty
-- Normally report all errors; but with -XAllowAmbiguousTypes
-- report only insoluble ones, since they represent genuinely
-- inaccessible code
; allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
; traceTc "reportUnsolved(ambig) {" empty
; unless (allow_ambiguous && not (insolubleWC zonked_final_wc))
(discardResult (reportUnsolved zonked_final_wc))
; traceTc "reportUnsolved(ambig) }" empty
; return () }
------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
simplifyInteractive wanteds
simplifyInteractive wanteds
= traceTc "simplifyInteractive" empty >>
simplifyTop wanteds
simplifyTop wanteds
------------------
simplifyDefault :: ThetaType -- Wanted; has no type variables in it
......@@ -188,7 +199,7 @@ simplifyDefault theta
; traceTc "reportUnsolved {" empty
-- See Note [Deferring coercion errors to runtime]
; reportAllUnsolved unsolved
; reportAllUnsolved unsolved
-- Postcondition of solveWantedsTcM is that returned
-- constraints are zonked. So Precondition of reportUnsolved
-- is true.
......
......@@ -18,7 +18,7 @@ module TcValidity (
-- friends:
import TcUnify ( tcSubType )
import TcSimplify ( simplifyTop )
import TcSimplify ( simplifyAmbiguityCheck )
import TypeRep
import TcType
import TcMType
......@@ -69,32 +69,31 @@ checkAmbiguity ctxt ty
-- (T k) is ambiguous!
| otherwise
= do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
; unless allow_ambiguous $
do { traceTc "Ambiguity check for" (ppr ty)
= do { traceTc "Ambiguity check for" (ppr ty)
; (subst, _tvs) <- tcInstSkolTyVars (varSetElems (tyVarsOfType ty))
; let ty' = substTy subst ty
; let ty' = substTy subst ty
-- The type might have free TyVars,
-- so we skolemise them as TcTyVars
-- Tiresome; but the type inference engine expects TcTyVars
-- Solve the constraints eagerly because an ambiguous type
-- can cause a cascade of further errors. Since the free
-- can cause a cascade of further errors. Since the free
-- tyvars are skolemised, we can safely use tcSimplifyTop
; addErrCtxtM (mk_msg ty') $
do { (_wrap, wanted) <- captureConstraints $
tcSubType (AmbigOrigin ctxt) ctxt ty' ty'
; _ev_binds <- simplifyTop wanted
; return () }
; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $
captureConstraints $
tcSubType (AmbigOrigin ctxt) ctxt ty' ty'
; simplifyAmbiguityCheck ty wanted
; traceTc "Done ambiguity check for" (ppr ty) } }
; traceTc "Done ambiguity check for" (ppr ty) }
where
mk_msg ty tidy_env
= return (tidy_env', msg)
mk_msg ty tidy_env
= do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
; return (tidy_env', msg $$ ppWhen (not allow_ambiguous) ambig_msg) }
where
(tidy_env', tidy_ty) = tidyOpenType tidy_env ty
msg = hang (ptext (sLit "In the ambiguity check for:"))
2 (ppr tidy_ty)
ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")
\end{code}
......
......@@ -6463,9 +6463,7 @@ The ambiguity check rejects functions that can never be called; for example:
</programlisting>
The idea is there can be no legal calls to <literal>f</literal> because every call will
give rise to an ambiguous constraint.
</para>
<para>
The <emphasis>only</emphasis> purpose of the
Indeed, the <emphasis>only</emphasis> purpose of the
ambiguity check is to report functions that cannot possibly be called.
We could soundly omit the
ambiguity check on type signatures entirely, at the expense of
......@@ -6510,18 +6508,48 @@ After all <literal>f</literal> has exactly the same type, and <literal>g=f</lite
But in fact <literal>f</literal>'s type
is instantiated and the instantiated constraints are solved against
the constraints bound by <literal>g</literal>'s signature. So, in the case an ambiguous type, solving will fail.
For example, consider the earlier definition <literal>f :: C a => Int</literal>. Then in <literal>g</literal>'s definition,
we'll instantiate to <literal>(C alpha)</literal> and try to
For example, consider the earlier definition <literal>f :: C a => Int</literal>:
<programlisting>
f :: C a => Int
f = ...blah...
g :: C a => Int
g = f
</programlisting>
In <literal>g</literal>'s definition,
we'll instantiate to <literal>(C alpha)</literal> and try to
deduce <literal>(C alpha)</literal> from <literal>(C a)</literal>,
and fail.
and fail.
</para>
<para>
So in fact we use this as our <emphasis>definition</emphasis> of ambiguity: a type
So in fact we use this as our <emphasis>definition</emphasis> of ambiguity: a type
<literal><replaceable>ty</replaceable></literal> is
ambiguious if and only if <literal>((undefined :: <replaceable>ty</replaceable>)
ambiguious if and only if <literal>((undefined :: <replaceable>ty</replaceable>)
:: <replaceable>ty</replaceable>)</literal> would fail to typecheck. We use a
very similar test for <emphasis>inferred</emphasis> types, to ensure that they too are
unambiguous.
unambiguous.
</para>
<para><emphasis>Switching off the ambiguity check.</emphasis>
Even if a function is has an ambiguous type according the "guiding principle",
it is possible that the function is callable. For example:
<programlisting>
class D a b where ...
instance D Bool b where ...
strange :: D a b => a -> a
strange = ...blah...
foo = strange True
</programlisting>
Here <literal>strange</literal>'s type is ambiguous, but the call in <literal>foo</literal>
is OK because it gives rise to a constraint <literal>(D Bool beta)</literal>, which is
soluble by the <literal>(D Bool b)</literal> instance. So the language extension
<option>-XAllowAmbiguousTypes</option> allows you to switch off the ambiguity check.
But even with ambiguity checking switched off, GHC will complain about a function
that can <emphasis>never</emphasis> be called, such as this one:
<programlisting>
f :: (Int ~ Bool) => a -> a
</programlisting>
</para>
<para>
......
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