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

4 files changed, 103 insertions, 64 deletions

diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index fced8ae53d..304d55bc4d 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -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
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index b2725ec7a8..16cabeb891 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -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.
diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index 091eef6db2..1e0b000d5d 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -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}
 
 
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index b7a2155f97..92305f28db 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -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>