Do not discard insolubles in implications
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 27 Jul 2017 13:52:38 +0000 (14:52 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 28 Jul 2017 08:31:55 +0000 (09:31 +0100)
Trac #14000 showed up two errors

* In TcRnTypes.dropInsolubles we dropped all implications, which
  might contain the very insolubles we wanted to keep.  This was
  an outright error, and is why the out-of-scope error was actually
  lost altogether in Trac #14000

* In TcSimplify.simplifyInfer, if there are definite (insoluble)
  errors, it's better to suppress the following ambiguity test,
  because the type may be bogus anyway.  See TcSimplify
  Note [Quantification with errors].  This fix seems a bit clunky,
  but it'll do for now.

13 files changed:
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/parser/should_fail/T7848.hs
testsuite/tests/parser/should_fail/T7848.stderr
testsuite/tests/th/T5358.stderr
testsuite/tests/typecheck/should_fail/T14000.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T14000.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T8142.stderr
testsuite/tests/typecheck/should_fail/all.T

index 7b01aba..2327b6f 100644 (file)
@@ -787,12 +787,12 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
        ; mapM_ (checkOverloadedSig mono) sigs
 
        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
-       ; (qtvs, givens, ev_binds)
+       ; (qtvs, givens, ev_binds, insoluble)
                  <- simplifyInfer tclvl infer_mode sigs name_taus wanted
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
-                    mapM (mkExport prag_fn qtvs inferred_theta) mono_infos
+                    mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos
 
        ; loc <- getSrcSpanM
        ; let poly_ids = map abe_poly exports
@@ -807,6 +807,8 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
 
 --------------
 mkExport :: TcPragEnv
+         -> Bool                        -- True <=> there was an insoluble type error
+                                        --          when typechecking the bindings
          -> [TyVar] -> TcThetaType      -- Both already zonked
          -> MonoBindInfo
          -> TcM (ABExport GhcTc)
@@ -823,12 +825,12 @@ mkExport :: TcPragEnv
 
 -- Pre-condition: the qtvs and theta are already zonked
 
-mkExport prag_fn qtvs theta
+mkExport prag_fn insoluble qtvs theta
          mono_info@(MBI { mbi_poly_name = poly_name
                         , mbi_sig       = mb_sig
                         , mbi_mono_id   = mono_id })
   = do  { mono_ty <- zonkTcType (idType mono_id)
-        ; poly_id <- mkInferredPolyId qtvs theta poly_name mb_sig mono_ty
+        ; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty
 
         -- NB: poly_id has a zonked type
         ; poly_id <- addInlinePrags poly_id prag_sigs
@@ -863,10 +865,12 @@ mkExport prag_fn qtvs theta
     prag_sigs = lookupPragEnv prag_fn poly_name
     sig_ctxt  = InfSigCtxt poly_name
 
-mkInferredPolyId :: [TyVar] -> TcThetaType
+mkInferredPolyId :: Bool  -- True <=> there was an insoluble error when
+                          --          checking the binding group for this Id
+                 -> [TyVar] -> TcThetaType
                  -> Name -> Maybe TcIdSigInst -> TcType
                  -> TcM TcId
-mkInferredPolyId qtvs inferred_theta poly_name mb_sig_inst mono_ty
+mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
   | Just (TISI { sig_inst_sig = sig })  <- mb_sig_inst
   , CompleteSig { sig_bndr = poly_id } <- sig
   = return poly_id
@@ -894,9 +898,13 @@ mkInferredPolyId qtvs inferred_theta poly_name mb_sig_inst mono_ty
 
        ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
                                           , ppr inferred_poly_ty])
-       ; addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
+       ; unless insoluble $
+         addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
          checkValidType (InfSigCtxt poly_name) inferred_poly_ty
          -- See Note [Validity of inferred types]
+         -- If we found an insoluble error in the function definition, don't
+         -- do this check; otherwise (Trac #14000) we may report an ambiguity
+         -- error for a rather bogus type.
 
        ; return (mkLocalIdOrCoVar poly_name inferred_poly_ty) }
 
index 1896c68..195ba01 100644 (file)
@@ -1561,7 +1561,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
                         = ApplyMR
                         | otherwise
                         = NoRestrictions
-       ; (qtvs, givens, ev_binds)
+       ; (qtvs, givens, ev_binds, _)
                  <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
        ; tau <- zonkTcType tau
        ; let inferred_theta = map evVarPred givens
index 36b6384..67e031a 100644 (file)
@@ -80,8 +80,8 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
 
        ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
 
-       ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl NoRestrictions []
-                                                      named_taus wanted
+       ; (qtvs, req_dicts, ev_binds, _) <- simplifyInfer tclvl NoRestrictions []
+                                                         named_taus wanted
 
        ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
              ex_tv_set  = mkVarSet ex_tvs
index 8a6d72e..ff20e30 100644 (file)
@@ -2191,9 +2191,9 @@ tcRnExpr hsc_env mode rdr_expr
                   else return expr_ty } ;
 
     -- Generalise
-    ((qtvs, dicts, _), lie_top) <- captureTopConstraints $
-                                   {-# SCC "simplifyInfer" #-}
-                                   simplifyInfer tclvl
+    ((qtvs, dicts, _, _), lie_top) <- captureTopConstraints $
+                                      {-# SCC "simplifyInfer" #-}
+                                      simplifyInfer tclvl
                                                  infer_mode
                                                  []    {- No sig vars -}
                                                  [(fresh_it, res_ty)]
index e30c33e..d3645e7 100644 (file)
@@ -2254,7 +2254,13 @@ getInsolubles = wc_insol
 
 insolublesOnly :: WantedConstraints -> WantedConstraints
 -- Keep only the insolubles
-insolublesOnly wc = wc { wc_simple = emptyBag, wc_impl = emptyBag }
+insolublesOnly (WC { wc_insol = insols, wc_impl = implics })
+  = WC { wc_simple = emptyBag
+       , wc_insol  = insols
+       , wc_impl = mapBag implic_insols_only implics }
+  where
+    implic_insols_only implic
+      = implic { ic_wanted = insolublesOnly (ic_wanted implic) }
 
 dropDerivedWC :: WantedConstraints -> WantedConstraints
 -- See Note [Dropping derived constraints]
index dca7f4d..a7a0461 100644 (file)
@@ -22,6 +22,7 @@ import Class         ( Class, classKey, classTyCon )
 import DynFlags      ( WarningFlag ( Opt_WarnMonomorphism )
                      , WarnReason ( Reason )
                      , DynFlags( solverIterations ) )
+import Id            ( idType )
 import Inst
 import ListSetOps
 import Maybes
@@ -576,14 +577,16 @@ simplifyInfer :: TcLevel               -- Used when generating the constraints
               -> WantedConstraints
               -> TcM ([TcTyVar],    -- Quantify over these type variables
                       [EvVar],      -- ... and these constraints (fully zonked)
-                      TcEvBinds)    -- ... binding these evidence variables
+                      TcEvBinds,    -- ... binding these evidence variables
+                      Bool)         -- True <=> there was an insoluble type error
+                                    --          in these bindings
 simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyCoVars
        ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
        ; qtkvs <- quantifyTyVars gbl_tvs dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
-       ; return (qtkvs, [], emptyTcEvBinds) }
+       ; return (qtkvs, [], emptyTcEvBinds, False) }
 
   | otherwise
   = do { traceTc "simplifyInfer {"  $ vcat
@@ -618,26 +621,24 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                   ; wanteds' <- solveWanteds wanteds
                   ; TcS.zonkWC wanteds' }
 
+
        -- Find quant_pred_candidates, the predicates that
        -- we'll consider quantifying over
        -- NB1: wanted_transformed does not include anything provable from
        --      the psig_theta; it's just the extra bit
        -- NB2: We do not do any defaulting when inferring a type, this can lead
        --      to less polymorphic types, see Note [Default while Inferring]
-
-       ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
-             quant_pred_candidates   -- Fully zonked
-                 | insolubleWC wanted_transformed_incl_derivs
-                 = []   -- See Note [Quantification with errors]
-                        -- NB: must include derived errors in this test,
-                        --     hence "incl_derivs"
-
-                 | otherwise
-                 = ctsPreds (approximateWC False wanted_transformed)
-
-       -- NB: quant_pred_candidates is already fully zonked
+       ; let definite_error = insolubleWC wanted_transformed_incl_derivs
+                              -- See Note [Quantification with errors]
+                              -- NB: must include derived errors in this test,
+                              --     hence "incl_derivs"
+             wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
+             quant_pred_candidates
+               | definite_error = []
+               | otherwise      = ctsPreds (approximateWC False wanted_transformed)
 
        -- Decide what type variables and constraints to quantify
+       -- NB: quant_pred_candidates is already fully zonked
        -- NB: bound_theta are constraints we want to quantify over,
        --     /apart from/ the psig_theta, which we always quantify over
        ; (qtvs, bound_theta) <- decideQuantification infer_mode rhs_tclvl
@@ -648,41 +649,58 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
         -- remaining constraints from the RHS.
         -- We must retain the psig_theta_vars, because we've used them in
         -- evidence bindings constructed by solveWanteds earlier
-       ; psig_theta_vars  <- mapM zonkId psig_theta_vars
+       ; psig_theta_vars  <- mapM zonkId       psig_theta_vars
        ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
-       ; let full_theta      = psig_theta      ++ bound_theta
-             full_theta_vars = psig_theta_vars ++ bound_theta_vars
-             skol_info   = InferSkol [ (name, mkSigmaTy [] full_theta ty)
-                                     | (name, ty) <- name_taus ]
-                        -- Don't add the quantified variables here, because
-                        -- they are also bound in ic_skols and we want them
-                        -- to be tidied uniformly
+       ; let full_theta_vars = psig_theta_vars ++ bound_theta_vars
 
-             implic = Implic { ic_tclvl    = rhs_tclvl
-                             , ic_skols    = qtvs
-                             , ic_no_eqs   = False
-                             , ic_given    = full_theta_vars
-                             , ic_wanted   = wanted_transformed
-                             , ic_status   = IC_Unsolved
-                             , ic_binds    = ev_binds_var
-                             , ic_info     = skol_info
-                             , ic_needed   = emptyVarSet
-                             , ic_env      = tc_lcl_env }
-       ; emitImplication implic
+       ; emitResidualImplication rhs_tclvl tc_lcl_env ev_binds_var
+                                 name_taus qtvs full_theta_vars
+                                 wanted_transformed
 
          -- All done!
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
          vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
               , text "psig_theta =" <+> ppr psig_theta
               , text "bound_theta =" <+> ppr bound_theta
-              , text "full_theta =" <+> ppr full_theta
+              , text "full_theta =" <+> ppr (map idType full_theta_vars)
               , text "qtvs ="       <+> ppr qtvs
-              , text "implic ="     <+> ppr implic ]
+              , text "definite_error =" <+> ppr definite_error ]
 
-       ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
+       ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
          -- NB: full_theta_vars must be fully zonked
 
 
+--------------------
+emitResidualImplication :: TcLevel -> TcLclEnv -> EvBindsVar
+                        -> [(Name, TcTauType)] -> [TcTyVar] -> [EvVar]
+                        -> WantedConstraints -> TcM ()
+emitResidualImplication rhs_tclvl tc_lcl_env ev_binds_var
+                        name_taus qtvs full_theta_vars wanteds
+ | isEmptyWC wanteds
+ = return ()
+ | otherwise
+ = do { traceTc "emitResidualImplication" (ppr implic)
+      ; emitImplication implic }
+ where
+   implic = Implic { ic_tclvl    = rhs_tclvl
+                   , ic_skols    = qtvs
+                   , ic_no_eqs   = False
+                   , ic_given    = full_theta_vars
+                   , ic_wanted   = wanteds
+                   , ic_status   = IC_Unsolved
+                   , ic_binds    = ev_binds_var
+                   , ic_info     = skol_info
+                   , ic_needed   = emptyVarSet
+                   , ic_env      = tc_lcl_env }
+
+   full_theta = map idType full_theta_vars
+   skol_info  = InferSkol [ (name, mkSigmaTy [] full_theta ty)
+                          | (name, ty) <- name_taus ]
+                        -- Don't add the quantified variables here, because
+                        -- they are also bound in ic_skols and we want them
+                        -- to be tidied uniformly
+
+--------------------
 ctsPreds :: Cts -> [PredType]
 ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
                              , let ev = ctEvidence ct ]
@@ -1092,13 +1110,33 @@ Notice that
 Note [Quantification with errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we find that the RHS of the definition has some absolutely-insoluble
-constraints, we abandon all attempts to find a context to quantify
-over, and instead make the function fully-polymorphic in whatever
-type we have found.  For two reasons
-  a) Minimise downstream errors
-  b) Avoid spurious errors from this function
-
-But NB that we must include *derived* errors in the check. Example:
+constraints (including especially "variable not in scope"), we
+
+* Abandon all attempts to find a context to quantify over,
+  and instead make the function fully-polymorphic in whatever
+  type we have found
+
+* Return a flag from simplifyInfer, indicating that we found an
+  insoluble constraint.  This flag is used to suppress the ambiguity
+  check for the inferred type, which may well be bogus, and which
+  tends to obscure the real error.  This fix feels a bit clunky,
+  but I failed to come up with anything better.
+
+Reasons:
+    - Avoid downstream errors
+    - Do not perform an ambiguity test on a bogus type, which might well
+      fail spuriously, thereby obfuscating the original insoluble error.
+      Trac #14000 is an example
+
+I tried an alterantive approach: simply failM, after emitting the
+residual implication constraint; the exception will be caught in
+TcBinds.tcPolyBinds, which gives all the binders in the group the type
+(forall a. a).  But that didn't work with -fdefer-type-errors, because
+the recovery from failM emits no code at all, so there is no function
+to run!   But -fdefer-type-errors aspires to produce a runnable program.
+
+NB that we must include *derived* errors in the check for insolubles.
+Example:
     (a::*) ~ Int#
 We get an insoluble derived error *~#, and we don't want to discard
 it before doing the isInsolubleWC test!  (Trac #8262)
index 25f0af7..920f28e 100644 (file)
@@ -8,4 +8,4 @@ x (+) ((&)@z) ((:&&) a b) (c :&& d) (e `A` f) (A g h) = y
         y _ = (&)
         {-# INLINE (&) #-}
         {-# SPECIALIZE (&) :: a #-}
-        (&) = x
+        (&) = 'c'
index 95ac737..413920d 100644 (file)
@@ -1,13 +1,7 @@
 
-T7848.hs:6:1: error:
-    • Occurs check: cannot construct the infinite type:
-        t ~ p0 -> p1 -> A -> A -> A -> A -> p2 -> t
-    • Relevant bindings include x :: t (bound at T7848.hs:6:1)
-
 T7848.hs:10:9: error:
-    • Couldn't match expected type ‘t’ with actual type ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match expected type ‘Char’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
         the type signature for:
           (&) :: forall a. a
         at T7848.hs:10:9-35
@@ -20,5 +14,4 @@ T7848.hs:10:9: error:
                 y _ = (&)
                 {-# INLINE (&) #-}
                 {-# SPECIALIZE (&) :: a #-}
-                (&) = x
-    • Relevant bindings include x :: t (bound at T7848.hs:6:1)
+                (&) = 'c'
index 4bfc53a..b698bc1 100644 (file)
@@ -1,4 +1,24 @@
 
+T5358.hs:10:13: error:
+    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
+    • The function ‘T5358.t1’ is applied to one argument,
+      but its type ‘Int’ has none
+      In the first argument of ‘(==)’, namely ‘T5358.t1 x’
+      In the expression: T5358.t1 x == T5358.t2 x
+    • Relevant bindings include
+        x :: t (bound at T5358.hs:10:9)
+        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
+
+T5358.hs:10:21: error:
+    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
+    • The function ‘T5358.t2’ is applied to one argument,
+      but its type ‘Int’ has none
+      In the second argument of ‘(==)’, namely ‘T5358.t2 x’
+      In the expression: T5358.t1 x == T5358.t2 x
+    • Relevant bindings include
+        x :: t (bound at T5358.hs:10:9)
+        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
+
 T5358.hs:14:12: error:
     • Exception when trying to run compile-time code:
         runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
diff --git a/testsuite/tests/typecheck/should_fail/T14000.hs b/testsuite/tests/typecheck/should_fail/T14000.hs
new file mode 100644 (file)
index 0000000..854a78b
--- /dev/null
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+module T14000 where
+
+class C a where
+    type T a
+    c :: a -> T a
+
+foo = c noSuchThing   -- noSuchThing is not in scope
diff --git a/testsuite/tests/typecheck/should_fail/T14000.stderr b/testsuite/tests/typecheck/should_fail/T14000.stderr
new file mode 100644 (file)
index 0000000..8b51e37
--- /dev/null
@@ -0,0 +1,2 @@
+
+T14000.hs:8:9: error: Variable not in scope: noSuchThing
index aec8b3b..25d60d1 100644 (file)
@@ -1,16 +1,24 @@
 
-T8142.hs:6:18: error:
-    • Couldn't match type ‘Nu g0’ with ‘Nu g
-      Expected type: Nu ((,) a) -> Nu g
+T8142.hs:6:10: error:
+    • Couldn't match type ‘Nu ((,) a0)’ with ‘c -> f c
+      Expected type: (c -> f c) -> c -> f c
         Actual type: Nu ((,) a0) -> Nu g0
-      NB: ‘Nu’ is a type function, and may not be injective
-      The type variable ‘g0’ is ambiguous
-    • In the ambiguity check for the inferred type for ‘h’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      When checking the inferred type
-        h :: forall a (g :: * -> *). Nu ((,) a) -> Nu g
+      The type variable ‘a0’ is ambiguous
+    • In the expression: h
       In an equation for ‘tracer’:
           tracer
             = h
             where
                 h = (\ (_, b) -> ((outI . fmap h) b)) . out
+    • Relevant bindings include
+        tracer :: (c -> f c) -> c -> f c (bound at T8142.hs:6:1)
+
+T8142.hs:6:57: error:
+    • Couldn't match type ‘Nu ((,) a)’ with ‘g (Nu ((,) a))’
+      Expected type: Nu ((,) a) -> (a, g (Nu ((,) a)))
+        Actual type: Nu ((,) a) -> (a, Nu ((,) a))
+    • In the second argument of ‘(.)’, namely ‘out’
+      In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
+      In an equation for ‘h’: h = (\ (_, b) -> ((outI . fmap h) b)) . out
+    • Relevant bindings include
+        h :: Nu ((,) a) -> Nu g (bound at T8142.hs:6:18)
index 3d2a595..e31c7ee 100644 (file)
@@ -452,3 +452,4 @@ test('T13610', normal, compile_fail, [''])
 test('T11672', normal, compile_fail, [''])
 test('T13819', normal, compile_fail, [''])
 test('T11963', normal, compile_fail, [''])
+test('T14000', normal, compile_fail, [''])