Fix error-message suppress on given equalities
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 27 Mar 2017 09:32:08 +0000 (10:32 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 27 Mar 2017 15:31:01 +0000 (16:31 +0100)
I'd got the logic slightly wrong when reporting type errors
for insoluble 'given' equalities.  We suppress insoluble givens
under some circumstances (see Note [Given errors]), but we then
suppressed subsequent 'wanted' errors because the (suppressed)
'given' error "won".  Result: no errors at all :-(.

This patch fixes it and
 - Renames TcType.isTyVarUnderDatatype to the more
   perspicuous TcType.isInsolubleOccursCheck

In doing this I realise that I don't understand why we need
to keep the insolubles partitioned out separately at all...
but that is for another day.

13 files changed:
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcType.hs
testsuite/tests/ghci/scripts/Defer02.stderr
testsuite/tests/indexed-types/should_fail/T2627b.stderr
testsuite/tests/indexed-types/should_fail/T5934.stderr
testsuite/tests/indexed-types/should_fail/T6123.stderr
testsuite/tests/indexed-types/should_fail/T7354.stderr
testsuite/tests/typecheck/should_compile/T12427a.stderr
testsuite/tests/typecheck/should_fail/T12589.stderr
testsuite/tests/typecheck/should_fail/T13446.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T13446.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

index 8688c77..d5fa275 100644 (file)
@@ -1439,11 +1439,12 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
     CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
              , cc_rhs = xi2'', cc_eq_rel = eq_rel }
 
-  | otherwise  -- Occurs check error (or a forall)
-  = do { traceTcS "canEqTyVar2 occurs check error" (ppr tv1 $$ ppr xi2)
+  | otherwise  -- For some reason (occurs check, or forall) we can't unify
+               -- We must not use it for further rewriting!
+  = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr xi2)
        ; rewriteEqEvidence ev swapped xi1 xi2 co1 co2
          `andWhenContinue` \ new_ev ->
-         if eq_rel == NomEq || isTyVarUnderDatatype tv1 xi2
+         if isInsolubleOccursCheck eq_rel tv1 xi2
          then do { emitInsoluble (mkNonCanonical new_ev)
              -- If we have a ~ [a], it is not canonical, and in particular
              -- we don't want to rewrite existing inerts with it, otherwise
@@ -1456,7 +1457,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
              -- We might learn that b is the newtype Id.
              -- But, the occurs-check certainly prevents the equality from being
              -- canonical, and we might loop if we were to use it in rewriting.
-         else do { traceTcS "Occurs-check in representational equality"
+         else do { traceTcS "Possibly-soluble occurs check"
                            (ppr xi1 $$ ppr xi2)
                  ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
   where
index 4bcf673..84a28a7 100644 (file)
@@ -308,6 +308,25 @@ data ReportErrCtxt
                                     -- See Note [Suppressing error messages]
       }
 
+instance Outputable ReportErrCtxt where
+  ppr (CEC { cec_binds              = bvar
+           , cec_errors_as_warns    = ew
+           , cec_defer_type_errors  = dte
+           , cec_expr_holes         = eh
+           , cec_type_holes         = th
+           , cec_out_of_scope_holes = osh
+           , cec_warn_redundant     = wr
+           , cec_suppress           = sup })
+    = text "CEC" <+> braces (vcat
+         [ text "cec_binds"              <+> equals <+> ppr bvar
+         , text "cec_errors_as_warns"    <+> equals <+> ppr ew
+         , text "cec_defer_type_errors"  <+> equals <+> ppr dte
+         , text "cec_expr_holes"         <+> equals <+> ppr eh
+         , text "cec_type_holes"         <+> equals <+> ppr th
+         , text "cec_out_of_scope_holes" <+> equals <+> ppr osh
+         , text "cec_warn_redundant"     <+> equals <+> ppr wr
+         , text "cec_suppress"           <+> equals <+> ppr sup ])
+
 {-
 Note [Suppressing error messages]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -411,13 +430,14 @@ This only matters in instance declarations..
 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
 reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
   = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
+                                       , text "Insols =" <+> ppr insols
                                        , text "Suppress =" <+> ppr (cec_suppress ctxt)])
        ; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
 
          -- First deal with things that are utterly wrong
          -- Like Int ~ Bool (incl nullary TyCons)
          -- or  Int ~ t a   (AppTy on one side)
-         -- These ones are not suppressed by the incoming context
+         -- These /ones/ are not suppressed by the incoming context
        ; let ctxt_for_insols = ctxt { cec_suppress = False }
        ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
 
@@ -448,7 +468,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     -- type checking to get a Lint error later
     report1 = [ ("custom_error", is_user_type_error,
                                                   True, mkUserTypeErrorReporter)
-              , ("insoluble1",   is_given_eq,     True, mkGivenErrorReporter)
+              , given_eq_spec
               , ("insoluble2",   utterly_wrong,   True, mkGroupReporter mkEqErr)
               , ("skolem eq1",   very_wrong,      True, mkSkolReporter)
               , ("skolem eq2",   skolem_eq,       True, mkSkolReporter)
@@ -490,12 +510,6 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
     non_tv_eq _ _                    = False
 
---    rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
---
---    rigid_nom_tv_eq _ pred
---      | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
---      | otherwise              = False
-
     is_out_of_scope ct _ = isOutOfScopeCt ct
     is_hole         ct _ = isHoleCt ct
 
@@ -513,6 +527,22 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     is_irred _ (IrredPred {}) = True
     is_irred _ _              = False
 
+    given_eq_spec = case find_gadt_match (cec_encl ctxt) of
+       Just imp -> ("insoluble1a", is_given_eq, True,  mkGivenErrorReporter imp)
+       Nothing  -> ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
+                  -- False means don't suppress subsequent errors
+                  -- Reason: we don't report all given errors
+                  --         (see mkGivenErrorReporter), and we should only suppress
+                  --         subsequent errors if we actually report this one!
+                  --         Trac #13446 is an example
+
+    find_gadt_match [] = Nothing
+    find_gadt_match (implic : implics)
+      | PatSkol {} <- ic_info implic
+      , not (ic_no_eqs implic)
+      = Just implic
+      | otherwise
+      = find_gadt_match implics
 
 ---------------
 isSkolemTy :: TcLevel -> Type -> Bool
@@ -580,10 +610,9 @@ mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
                             Nothing  -> pprPanic "mkUserTypeError" (ppr ct)
 
 
-mkGivenErrorReporter :: Reporter
+mkGivenErrorReporter :: Implication -> Reporter
 -- See Note [Given errors]
-mkGivenErrorReporter ctxt cts
-  | Just implic <- find_gadt_match (cec_encl ctxt)
+mkGivenErrorReporter implic ctxt cts
   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
        ; dflags <- getDynFlags
        ; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
@@ -600,22 +629,17 @@ mkGivenErrorReporter ctxt cts
 
        ; traceTc "mkGivenErrorRporter" (ppr ct)
        ; maybeReportError ctxt err }
-
-  | otherwise   -- Discard Given errors that don't come from
-                -- a pattern match; maybe we should warn instead?
-  = do { traceTc "mkGivenErrorRporter no" (ppr ct $$ ppr (cec_encl ctxt))
-       ; return () }
   where
     (ct : _ )  = cts    -- Never empty
     (ty1, ty2) = getEqPredTys (ctPred ct)
 
-    find_gadt_match [] = Nothing
-    find_gadt_match (implic : implics)
-      | PatSkol {} <- ic_info implic
-      , not (ic_no_eqs implic)
-      = Just implic
-      | otherwise
-      = find_gadt_match implics
+ignoreErrorReporter :: Reporter
+-- Discard Given errors that don't come from
+-- a pattern match; maybe we should warn instead?ignoreErrorReporter ctxt cts
+ignoreErrorReporter ctxt cts
+  = do { traceTc "mkGivenErrorRporter no" (ppr cts $$ ppr (cec_encl ctxt))
+       ; return () }
+
 
 {- Note [Given errors]
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -1442,7 +1466,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
                             -- be oriented the other way round;
                             -- see TcCanonical.canEqTyVarTyVar
   || isSigTyVar tv1 && not (isTyVarTy ty2)
-  || ctEqRel ct == ReprEq && not (isTyVarUnderDatatype tv1 ty2)
+  || ctEqRel ct == ReprEq && not insoluble_occurs_check
      -- the cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct $ mconcat
         [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
@@ -1454,7 +1478,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
   -- generalised it).  So presumably it is an *untouchable*
   -- meta tyvar or a SigTv, else it'd have been unified
   | OC_Occurs <- occ_check_expand
-  , ctEqRel ct == NomEq || isTyVarUnderDatatype tv1 ty2
+  , insoluble_occurs_check
          -- See Note [Occurs check error] in TcCanonical
   = do { let occCheckMsg = important $ addArising (ctOrigin ct) $
                            hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
@@ -1547,7 +1571,8 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
         -- Not an occurs check, because F is a type function.
   where
     ty1 = mkTyVarTy tv1
-    occ_check_expand = occCheckForErrors dflags tv1 ty2
+    occ_check_expand       = occCheckForErrors dflags tv1 ty2
+    insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
 
     what = case ctLocTypeOrKind_maybe (ctLoc ct) of
       Just KindLevel -> text "kind"
index e5708b6..d4e8d4d 100644 (file)
@@ -78,7 +78,7 @@ module TcType (
   isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
-  isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
+  isPredTy, isTyVarClassPred, isTyVarExposed, isInsolubleOccursCheck,
   checkValidClsArgs, hasTyVarHead,
   isRigidEqPred, isRigidTy,
 
@@ -2149,26 +2149,35 @@ isTyVarExposed _  (FunTy {})      = False
 isTyVarExposed tv (CastTy ty _)   = isTyVarExposed tv ty
 isTyVarExposed _  (CoercionTy {}) = False
 
--- | Does the given tyvar appear under a type generative w.r.t.
--- representational equality? See Note [Occurs check error] in
+-- | Is the equality
+--        a ~r ...a....
+-- definitely insoluble or not?
+--      a ~r Maybe a      -- Definitely insoluble
+--      a ~N ...(F a)...  -- Not definitely insoluble
+--                        -- Perhaps (F a) reduces to Int
+--      a ~R ...(N a)...  -- Not definitely insoluble
+--                        -- Perhaps newtype N a = MkN Int
+-- See Note [Occurs check error] in
 -- TcCanonical for the motivation for this function.
-isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool
-isTyVarUnderDatatype tv = go False
+isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
+isInsolubleOccursCheck eq_rel tv ty
+  = go ty
   where
-    go under_dt ty | Just ty' <- coreView ty = go under_dt ty'
-    go under_dt (TyVarTy tv') = under_dt && (tv == tv')
-    go under_dt (TyConApp tc tys) = let under_dt' = under_dt ||
-                                                    isGenerativeTyCon tc
-                                                      Representational
-                                    in any (go under_dt') tys
-    go _        (LitTy {}) = False
-    go _        (FunTy arg res) = go True arg || go True res
-    go under_dt (AppTy fun arg) = go under_dt fun || go under_dt arg
-    go under_dt (ForAllTy (TvBndr tv' _) inner_ty)
+    go ty | Just ty' <- coreView ty = go ty'
+    go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
+    go (LitTy {})    = False
+    go (AppTy t1 t2) = go t1 || go t2
+    go (FunTy t1 t2) = go t1 || go t2
+    go (ForAllTy (TvBndr tv' _) inner_ty)
       | tv' == tv = False
-      | otherwise = go under_dt inner_ty
-    go under_dt (CastTy ty _)   = go under_dt ty
-    go _        (CoercionTy {}) = False
+      | otherwise = go (tyVarKind tv') || go inner_ty
+    go (CastTy ty _)  = go ty   -- ToDo: what about the coercion
+    go (CoercionTy _) = False   -- ToDo: what about the coercion
+    go (TyConApp tc tys)
+      | isGenerativeTyCon tc role = any go tys
+      | otherwise                 = False
+
+    role = eqRelRole eq_rel
 
 isRigidTy :: TcType -> Bool
 isRigidTy ty
index 527a987..5aa67f0 100644 (file)
@@ -84,6 +84,11 @@ Defer01.hs:43:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In the expression: myOp 23
       In an equation for ‘j’: j = myOp 23
 
+Defer01.hs:47:7: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘Bool’ with actual type ‘Int’
+    • In the expression: x
+      In an equation for ‘k’: k x = x
+
 Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘IO a0’
                   with actual type ‘Char -> IO ()’
index 63f11b9..1a09bd8 100644 (file)
@@ -1,9 +1,13 @@
 
 T2627b.hs:20:24: error:
-    • Occurs check: cannot construct the infinite type:
-        b0 ~ Dual (Dual b0)
+    • Couldn't match type ‘b0’ with ‘Dual (Dual b0)’
         arising from a use of ‘conn’
-      The type variable ‘b0’ is ambiguous
+        ‘b0’ is untouchable
+          inside the constraints: b ~ W e f
+          bound by a pattern with constructor:
+                     Wr :: forall e f. e -> Comm f -> Comm (W e f),
+                   in an equation for ‘conn’
+          at T2627b.hs:20:14-19
     • In the expression: conn undefined undefined
       In an equation for ‘conn’:
           conn (Rd k) (Wr a r) = conn undefined undefined
index 20b16b2..e303e54 100644 (file)
@@ -1,6 +1,20 @@
 
 T5934.hs:12:7: error:
-    • Couldn't match expected type ‘(forall s. GenST s) -> Int’
-                  with actual type ‘Integer’
+    • Cannot instantiate unification variable ‘a0’
+      with a type involving foralls: (forall s. GenST s) -> Int
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: 0
+      In an equation for ‘run’: run = 0
+
+T5934.hs:12:7: error:
+    • Ambiguous type variable ‘a0’ arising from the literal ‘0’
+      prevents the constraint ‘(Num a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Num Integer -- Defined in ‘GHC.Num’
+        instance Num Double -- Defined in ‘GHC.Float’
+        instance Num Float -- Defined in ‘GHC.Float’
+        ...plus two others
+        (use -fprint-potential-instances to see them all)
     • In the expression: 0
       In an equation for ‘run’: run = 0
index 0ae1a5e..eafd27c 100644 (file)
@@ -1,7 +1,6 @@
 
 T6123.hs:10:14: error:
-    • Occurs check: cannot construct the infinite type: a0 ~ Id a0
-        arising from a use of ‘cid’
+    • Couldn't match type ‘a0’ with ‘Id a0’ arising from a use of ‘cid’
       The type variable ‘a0’ is ambiguous
     • In the expression: cid undefined
       In an equation for ‘cundefined’: cundefined = cid undefined
index b7b70b8..f4c3c0d 100644 (file)
@@ -1,7 +1,8 @@
 
 T7354.hs:28:11: error:
-    • Occurs check: cannot construct the infinite type:
-        p ~ Base t (Prim [p] p)
+    • Couldn't match type ‘p’ with ‘Base t (Prim [p] p)’
+      ‘p’ is a rigid type variable bound by
+        the inferred type of foo :: Prim [p] p -> t at T7354.hs:28:1-13
       Expected type: Prim [p] p -> Base t (Prim [p] p)
         Actual type: Prim [p] p -> p
     • In the first argument of ‘ana’, namely ‘alg’
index fc2aece..05e9260 100644 (file)
@@ -2,15 +2,8 @@
 T12427a.hs:17:29: error:
     • Couldn't match expected type ‘p’
                   with actual type ‘(forall b. [b] -> [b]) -> Int’
-        ‘p’ is untouchable
-          inside the constraints: ()
-          bound by a pattern with constructor:
-                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
-                   in a case alternative
-          at T12427a.hs:17:19-24
       ‘p’ is a rigid type variable bound by
         the inferred type of h11 :: T -> p at T12427a.hs:17:1-29
-      Possible fix: add a type signature for ‘h11’
     • In the expression: v
       In a case alternative: T1 _ v -> v
       In the expression: case y of { T1 _ v -> v }
@@ -18,16 +11,8 @@ T12427a.hs:17:29: error:
         h11 :: T -> p (bound at T12427a.hs:17:1)
 
 T12427a.hs:28:6: error:
-    • Couldn't match expected type ‘p’
-                  with actual type ‘(forall b. [b] -> [b]) -> Int’
-        ‘p’ is untouchable
-          inside the constraints: ()
-          bound by a pattern with constructor:
-                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
-                   in a pattern binding
-          at T12427a.hs:28:1-7
-      ‘p’ is a rigid type variable bound by
-        the inferred type of x1 :: p at T12427a.hs:28:1-19
-      Possible fix: add a type signature for ‘x1’
+    • Cannot instantiate unification variable ‘p0’
+      with a type involving foralls: (forall b. [b] -> [b]) -> Int
+        GHC doesn't yet support impredicative polymorphism
     • In the pattern: T1 _ x1
       In a pattern binding: T1 _ x1 = undefined
index a2587e2..f77d645 100644 (file)
@@ -1,2 +1,11 @@
 
 T12589.hs:13:3: error: Variable not in scope: (&) :: t0 -> t1 -> t
+
+T12589.hs:13:5: error:
+    • Cannot instantiate unification variable ‘t1’
+      with a type involving foralls:
+        (forall a. Bounded a => f0 a) -> h0 f0 xs0
+        GHC doesn't yet support impredicative polymorphism
+    • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
+      In the expression: (&) minBound hcpure (Proxy @Bounded)
+      In an equation for ‘a’: a = (&) minBound hcpure (Proxy @Bounded)
diff --git a/testsuite/tests/typecheck/should_fail/T13446.hs b/testsuite/tests/typecheck/should_fail/T13446.hs
new file mode 100644 (file)
index 0000000..11a6077
--- /dev/null
@@ -0,0 +1,46 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{- # OPTIONS_GHC -fno-defer-type-errors #-}
+module T13446 where
+
+import Data.Coerce (Coercible)
+import GHC.Exts (Constraint)
+import GHC.TypeLits (Symbol)
+
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+
+infixr 9 :-
+newtype a :- b = Sub (a => Dict b)
+instance a => Show (a :- b) where
+  showsPrec d (Sub Dict) = showParen (d > 10) $ showString "Sub Dict"
+
+class Lifting p f where
+  lifting :: p a :- p (f a)
+
+data Blah a = Blah
+
+newtype J (a :: JType) = J (Blah (J a))
+newtype JComparable a = JComparable (J (T (JTy a)))
+
+instance Lifting JReference JComparable where
+  lifting = Sub 'a'
+
+class (Coercible a (J (JTy a))) => JReference a where
+  type JTy a :: JType
+
+type T a
+  = 'Generic ('Iface "java.lang.Comparable") '[a]
+data JType = Class Symbol
+           | Generic JType [JType]
+           | Iface Symbol
+type JObject = J (Class "java.lang.Object")
+instance JReference JObject where
+  type JTy JObject = 'Class "java.lang.Object"
diff --git a/testsuite/tests/typecheck/should_fail/T13446.stderr b/testsuite/tests/typecheck/should_fail/T13446.stderr
new file mode 100644 (file)
index 0000000..a0308f8
--- /dev/null
@@ -0,0 +1,10 @@
+
+T13446.hs:34:17: error:
+    • Couldn't match expected type ‘Dict (JReference (JComparable a))’
+                  with actual type ‘Char’
+    • In the first argument of ‘Sub’, namely ‘'a'’
+      In the expression: Sub 'a'
+      In an equation for ‘lifting’: lifting = Sub 'a'
+    • Relevant bindings include
+        lifting :: JReference a :- JReference (JComparable a)
+          (bound at T13446.hs:34:3)
index 13ea1d7..8fbe141 100644 (file)
@@ -430,3 +430,4 @@ test('LevPolyBounded', normal, compile_fail, [''])
 test('T13292', normal, multimod_compile, ['T13292', '-v0 -fdefer-type-errors'])
 test('T13300', normal, compile_fail, [''])
 test('T12709', normal, compile_fail, [''])
+test('T13446', normal, compile_fail, [''])