diff options
author | sheaf <sam.derbyshire@gmail.com> | 2021-08-14 03:41:03 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-08-15 09:00:29 -0400 |
commit | 1e896b476086e83ed6e97fb9d0ba8b96fed07783 (patch) | |
tree | 9f55f42c4630878ed94f31ffefa0f8026da8e2b6 /compiler/GHC | |
parent | a975583c70e57434340d9a20c976c8f06fde9beb (diff) | |
download | haskell-1e896b476086e83ed6e97fb9d0ba8b96fed07783.tar.gz |
Detect TypeError when checking for insolubility
We detect insoluble Givens by making getInertInsols
take into account TypeError constraints, on top of insoluble equalities
such as Int ~ Bool (which it already took into account).
This allows pattern matches with insoluble contexts to be reported
as redundant (tyOracle calls tcCheckGivens which calls getInertInsols).
As a bonus, we get to remove a workaround in Data.Typeable.Internal:
we can directly use a NotApplication type family, as opposed to
needing to cook up an insoluble equality constraint.
Fixes #11503 #14141 #16377 #20180
Diffstat (limited to 'compiler/GHC')
-rw-r--r-- | compiler/GHC/HsToCore/Pmc/Solver.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Errors.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver.hs | 67 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 12 | ||||
-rw-r--r-- | compiler/GHC/Tc/Types/Constraint.hs | 51 | ||||
-rw-r--r-- | compiler/GHC/Utils/Binary/Typeable.hs | 23 |
6 files changed, 121 insertions, 36 deletions
diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs index e0d5c63698..3caced3468 100644 --- a/compiler/GHC/HsToCore/Pmc/Solver.hs +++ b/compiler/GHC/HsToCore/Pmc/Solver.hs @@ -617,6 +617,8 @@ addTyCts nabla@MkNabla{ nabla_ty_st = ty_st } new_ty_cs = do -- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we -- find a contradiction (e.g. @Int ~ Bool@). +-- +-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver. tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState) tyOracle ty_st@(TySt n inert) cts | isEmptyBag cts diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index dc95a6a81d..51ab0fca2a 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -583,7 +583,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics -- report1: ones that should *not* be suppressed by -- an insoluble somewhere else in the tree -- It's crucial that anything that is considered insoluble - -- (see GHC.Tc.Utils.insolubleCt) is caught here, otherwise + -- (see GHC.Tc.Utils.insolublWantedCt) is caught here, otherwise -- we might suppress its error message, and proceed on past -- type checking to get a Lint error later report1 = [ ("custom_error", unblocked is_user_type_error, True, mkUserTypeErrorReporter) diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index f645e4d49c..e2ea2f59de 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -806,9 +806,74 @@ simplifyDefault theta ; return (isEmptyWC unsolved) } ------------------ +{- Note [Pattern match warnings with insoluble Givens] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A pattern match on a GADT can introduce new type-level information, which needs +to be analysed in order to get the expected pattern match warnings. + +For example: + +> type IsBool :: Type -> Constraint +> type family IsBool a where +> IsBool Bool = () +> IsBool b = b ~ Bool +> +> data T a where +> MkTInt :: Int -> T Int +> MkTBool :: IsBool b => b -> T b +> +> f :: T Int -> Int +> f (MkTInt i) = i + +The pattern matching performed by `f` is complete: we can't ever call +`f (MkTBool b)`, as type-checking that application would require producing +evidence for `Int ~ Bool`, which can't be done. + +The pattern match checker uses `tcCheckGivens` to accumulate all the Given +constraints, and relies on `tcCheckGivens` to return Nothing if the +Givens become insoluble. `tcCheckGivens` in turn relies on `insolubleCt` +to identify these insoluble constraints. So the precise definition of +`insolubleCt` has a big effect on pattern match overlap warnings. + +To detect this situation, we check whether there are any insoluble Given +constraints. In the example above, the insoluble constraint was an +equality constraint, but it is also important to detect custom type errors: + +> type NotInt :: Type -> Constraint +> type family NotInt a where +> NotInt Int = TypeError (Text "That's Int, silly.") +> NotInt _ = () +> +> data R a where +> MkT1 :: a -> R a +> MkT2 :: NotInt a => R a +> +> foo :: R Int -> Int +> foo (MkT1 x) = x + +To see that we can't call `foo (MkT2)`, we must detect that `NotInt Int` is insoluble +because it is a custom type error. +Failing to do so proved quite inconvenient for users, as evidence by the +tickets #11503 #14141 #16377 #20180. +Test cases: T11503, T14141. + +Examples of constraints that tcCheckGivens considers insoluble: + - Int ~ Bool, + - Coercible Float Word, + - TypeError msg. + +Non-examples: + - constraints which we know aren't satisfied, + e.g. Show (Int -> Int) when no such instance is in scope, + - Eq (TypeError msg), + - C (Int ~ Bool), with @class C (c :: Constraint)@. +-} + tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet) -- ^ Return (Just new_inerts) if the Givens are satisfiable, Nothing if definitely --- contradictory +-- contradictory. +-- +-- See Note [Pattern match warnings with insoluble Givens] above. tcCheckGivens inerts given_ids = do (sat, new_inerts) <- runTcSInerts inerts $ do traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids) diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 5796e2bd6a..b957b0ed0c 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -824,10 +824,16 @@ getInnermostGivenEqLevel = do { inert <- getInertCans ; return (inert_given_eq_lvl inert) } getInertInsols :: TcS Cts --- Returns insoluble equality constraints --- specifically including Givens +-- Returns insoluble equality constraints and TypeError constraints, +-- specifically including Givens. +-- +-- Note that this function only inspects irreducible constraints; +-- a DictCan constraint such as 'Eq (TypeError msg)' is not +-- considered to be an insoluble constraint by this function. +-- +-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver. getInertInsols = do { inert <- getInertCans - ; return (filterBag insolubleEqCt (inert_irreds inert)) } + ; return $ filterBag insolubleCt (inert_irreds inert) } getInertGivens :: TcS [Ct] -- Returns the Given constraints in the inert set diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 0567211bfb..7c7b2df772 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -43,7 +43,7 @@ module GHC.Tc.Types.Constraint ( isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC, addInsols, dropMisleading, addSimples, addImplics, addHoles, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, - tyCoVarsOfWCList, insolubleCt, insolubleEqCt, + tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, insolubleCt, isDroppableCt, insolubleImplic, arisesFromGivens, @@ -1129,7 +1129,7 @@ dropMisleading :: WantedConstraints -> WantedConstraints -- for why this function is so strange, treating the 'simples' -- and the implications differently. Sigh. dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) - = WC { wc_simple = filterBag insolubleCt simples + = WC { wc_simple = filterBag insolubleWantedCt simples , wc_impl = mapBag drop_implic implics , wc_holes = filterBag isOutOfScopeHole holes } where @@ -1158,19 +1158,20 @@ insolubleImplic ic = isInsolubleStatus (ic_status ic) insolubleWC :: WantedConstraints -> Bool insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_holes = holes }) - = anyBag insolubleCt simples + = anyBag insolubleWantedCt simples || anyBag insolubleImplic implics || anyBag isOutOfScopeHole holes -- See Note [Insoluble holes] -insolubleCt :: Ct -> Bool +insolubleWantedCt :: Ct -> Bool -- Definitely insoluble, in particular /excluding/ type-hole constraints --- Namely: a) an equality constraint --- b) that is insoluble --- c) and does not arise from a Given -insolubleCt ct - | not (insolubleEqCt ct) = False - | arisesFromGivens ct = False -- See Note [Given insolubles] - | otherwise = True +-- Namely: +-- a) an insoluble constraint as per 'insolubleCt', i.e. either +-- - an insoluble equality constraint (e.g. Int ~ Bool), or +-- - a custom type error constraint, TypeError msg :: Constraint +-- b) that does not arise from a Given +-- +-- See Note [Given insolubles]. +insolubleWantedCt ct = insolubleCt ct && not (arisesFromGivens ct) insolubleEqCt :: Ct -> Bool -- Returns True of /equality/ constraints @@ -1190,6 +1191,34 @@ insolubleEqCt :: Ct -> Bool insolubleEqCt (CIrredCan { cc_reason = reason }) = isInsolubleReason reason insolubleEqCt _ = False +-- | Returns True of equality constraints that are definitely insoluble, +-- as well as TypeError constraints. +-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'. +-- +-- This function is critical for accurate pattern-match overlap warnings. +-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver +-- +-- Note that this does not traverse through the constraint to find +-- nested custom type errors: it only detects @TypeError msg :: Constraint@, +-- and not e.g. @Eq (TypeError msg)@. +insolubleCt :: Ct -> Bool +insolubleCt ct + | Just _ <- userTypeError_maybe (ctPred ct) + -- Don't use 'isUserTypeErrorCt' here, as that function is too eager: + -- the TypeError might appear inside a type family application + -- which might later reduce, but we only want to return 'True' + -- for constraints that are definitely insoluble. + -- + -- Test case: T11503, with the 'Assert' type family: + -- + -- > type Assert :: Bool -> Constraint -> Constraint + -- > type family Assert check errMsg where + -- > Assert 'True _errMsg = () + -- > Assert _check errMsg = errMsg + = True + | otherwise + = insolubleEqCt ct + -- | Does this hole represent an "out of scope" error? -- See Note [Insoluble holes] isOutOfScopeHole :: Hole -> Bool diff --git a/compiler/GHC/Utils/Binary/Typeable.hs b/compiler/GHC/Utils/Binary/Typeable.hs index b0f4833cbf..7bef358e73 100644 --- a/compiler/GHC/Utils/Binary/Typeable.hs +++ b/compiler/GHC/Utils/Binary/Typeable.hs @@ -1,10 +1,9 @@ {-# LANGUAGE CPP #-} -{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE GADTs #-} {-# OPTIONS_GHC -O2 -funbox-strict-fields #-} -{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_GHC -Wno-orphans -Wincomplete-patterns #-} #if MIN_VERSION_base(4,16,0) #define HAS_TYPELITCHAR #endif @@ -19,7 +18,7 @@ import GHC.Prelude import GHC.Utils.Binary -import GHC.Exts (TYPE, RuntimeRep(..), VecCount(..), VecElem(..)) +import GHC.Exts (RuntimeRep(..), VecCount(..), VecElem(..)) #if __GLASGOW_HASKELL__ >= 901 import GHC.Exts (Levity(Lifted, Unlifted)) #endif @@ -49,7 +48,6 @@ getSomeTypeRep bh = do 1 -> do con <- get bh :: IO TyCon ks <- get bh :: IO [SomeTypeRep] return $ SomeTypeRep $ mkTrCon con ks - 2 -> do SomeTypeRep f <- getSomeTypeRep bh SomeTypeRep x <- getSomeTypeRep bh case typeRepKind f of @@ -68,20 +66,8 @@ getSomeTypeRep bh = do [ " Applied type: " ++ show f , " To argument: " ++ show x ] - 3 -> do SomeTypeRep arg <- getSomeTypeRep bh - SomeTypeRep res <- getSomeTypeRep bh - if - | App argkcon _ <- typeRepKind arg - , App reskcon _ <- typeRepKind res - , Just HRefl <- argkcon `eqTypeRep` tYPErep - , Just HRefl <- reskcon `eqTypeRep` tYPErep - -> return $ SomeTypeRep $ Fun arg res - | otherwise -> failure "Kind mismatch" [] _ -> failure "Invalid SomeTypeRep" [] where - tYPErep :: TypeRep TYPE - tYPErep = typeRep - failure description info = fail $ unlines $ [ "Binary.getSomeTypeRep: "++description ] ++ map (" "++) info @@ -201,10 +187,7 @@ instance Binary TypeLitSort where _ -> fail "Binary.putTypeLitSort: invalid tag" putTypeRep :: BinHandle -> TypeRep a -> IO () --- Special handling for TYPE, (->), and RuntimeRep due to recursive kind --- relations. --- See Note [Mutually recursive representations of primitive types] -putTypeRep bh rep +putTypeRep bh rep -- Handle Type specially since it's so common | Just HRefl <- rep `eqTypeRep` (typeRep :: TypeRep Type) = put_ bh (0 :: Word8) putTypeRep bh (Con' con ks) = do |