Commit e72d7880 authored by Ryan Scott's avatar Ryan Scott Committed by Krzysztof Gogolewski

Normalise EmptyCase types using the constraint solver

Summary:
Certain `EmptyCase` expressions were mistakently producing
warnings since their types did not have as many type families reduced
as they could have. The most direct way to fix this is to normalise
these types initially using the constraint solver to solve for any
local equalities that may be in scope.

Test Plan: make test TEST=T14813

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #14813

Differential Revision: https://phabricator.haskell.org/D5094
parent d00c3086
......@@ -12,10 +12,7 @@ module Check (
checkSingle, checkMatches, checkGuardMatches, isAnyPmCheckEnabled,
-- See Note [Type and Term Equality Propagation]
genCaseTmCs1, genCaseTmCs2,
-- Pattern-match-specific type operations
pmIsClosedType, pmTopNormaliseType_maybe
genCaseTmCs1, genCaseTmCs2
) where
#include "HsVersions.h"
......@@ -60,6 +57,7 @@ import Data.Maybe (catMaybes, isJust, fromMaybe)
import Control.Monad (forM, when, forM_, zipWithM)
import Coercion
import TcEvidence
import TcSimplify (tcNormalise)
import IOEnv
import qualified Data.Semigroup as Semi
......@@ -430,8 +428,7 @@ checkMatches' vars matches
checkEmptyCase' :: Id -> PmM PmResult
checkEmptyCase' var = do
tm_ty_css <- pmInitialTmTyCs
fam_insts <- liftD dsGetFamInstEnvs
mb_candidates <- inhabitationCandidates fam_insts (idType var)
mb_candidates <- inhabitationCandidates (delta_ty_cs tm_ty_css) (idType var)
case mb_candidates of
-- Inhabitation checking failed / the type is trivially inhabited
Left ty -> return (uncoveredWithTy ty)
......@@ -483,7 +480,8 @@ pmIsClosedType ty
is_algebraic_like :: TyCon -> Bool
is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon
pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type)
pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
-> PmM (Maybe (Type, [DataCon], Type))
-- ^ Get rid of *outermost* (or toplevel)
-- * type function redex
-- * data family redex
......@@ -492,9 +490,18 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type)
-- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
-- coercion, it returns useful information for issuing pattern matching
-- warnings. See Note [Type normalisation for EmptyCase] for details.
pmTopNormaliseType_maybe env typ
= do ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ
return (eq_src_ty ty (typ : ty_f [ty]), tm_f [], ty)
pmTopNormaliseType_maybe env ty_cs typ
= do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ
-- Before proceeding, we chuck typ into the constraint solver, in case
-- solving for given equalities may reduce typ some. See
-- "Wrinkle: local equalities" in
-- Note [Type normalisation for EmptyCase].
pure $ do typ' <- mb_typ'
((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ'
-- We need to do topNormaliseTypeX in addition to tcNormalise,
-- since topNormaliseX looks through newtypes, which
-- tcNormalise does not do.
Just (eq_src_ty ty (typ' : ty_f [ty]), tm_f [], ty)
where
-- Find the first type in the sequence of rewrites that is a data type,
-- newtype, or a data family application (not the representation tycon!).
......@@ -645,9 +652,10 @@ tmTyCsAreSatisfiable
checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
fam_insts <- liftD dsGetFamInstEnvs
let tys_to_check = filterOut (definitelyInhabitedType fam_insts)
strict_arg_tys
rec_max_bound | tys_to_check `lengthExceeds` 1
let definitely_inhabited =
definitelyInhabitedType fam_insts (delta_ty_cs amb_cs)
tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
let rec_max_bound | tys_to_check `lengthExceeds` 1
= 1
| otherwise
= defaultRecTcMaxBound
......@@ -667,8 +675,7 @@ nonVoid
-- 'False' if it is definitely uninhabitable by anything
-- (except bottom).
nonVoid rec_ts amb_cs strict_arg_ty = do
fam_insts <- liftD dsGetFamInstEnvs
mb_cands <- inhabitationCandidates fam_insts strict_arg_ty
mb_cands <- inhabitationCandidates (delta_ty_cs amb_cs) strict_arg_ty
case mb_cands of
Right (tc, cands)
| Just rec_ts' <- checkRecTc rec_ts tc
......@@ -707,12 +714,12 @@ nonVoid rec_ts amb_cs strict_arg_ty = do
--
-- See the \"Strict argument type constraints\" section of
-- @Note [Extensions to GADTs Meet Their Match]@.
definitelyInhabitedType :: FamInstEnvs -> Type -> Bool
definitelyInhabitedType env ty
| Just (_, cons, _) <- pmTopNormaliseType_maybe env ty
= any meets_criteria cons
| otherwise
= False
definitelyInhabitedType :: FamInstEnvs -> Bag EvVar -> Type -> PmM Bool
definitelyInhabitedType env ty_cs ty = do
mb_res <- pmTopNormaliseType_maybe env ty_cs ty
pure $ case mb_res of
Just (_, cons, _) -> any meets_criteria cons
Nothing -> False
where
meets_criteria :: DataCon -> Bool
meets_criteria con =
......@@ -733,7 +740,8 @@ It returns 3 results instead of one, because there are 2 subtle points:
2. The representational data family tycon is used internally but should not be
shown to the user
Hence, if pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty), then
Hence, if pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty),
then
(a) src_ty is the rewritten type which we can show to the user. That is, the
type we get if we rewrite type families but not data families or
newtypes.
......@@ -741,7 +749,7 @@ Hence, if pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty), then
newtype to it's core representation, we keep track of the source data
constructor.
(c) core_ty is the rewritten type. That is,
pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty)
pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty)
implies
topNormaliseType_maybe env ty = Just (co, core_ty)
for some coercion co.
......@@ -761,13 +769,34 @@ To see how all cases come into play, consider the following example:
type instance F Int = F Char
type instance F Char = G2
In this case pmTopNormaliseType_maybe env (F Int) results in
In this case pmTopNormaliseType_maybe env ty_cs (F Int) results in
Just (G2, [MkG2,MkG1], R:TInt)
Which means that in source Haskell:
- G2 is equivalent to F Int (in contrast, G1 isn't).
- if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).
-----
-- Wrinkle: Local equalities
-----
Given the following type family:
type family F a
type instance F Int = Void
Should the following program (from #14813) be considered exhaustive?
f :: (i ~ Int) => F i -> a
f x = case x of {}
You might think "of course, since `x` is obviously of type Void". But the
idType of `x` is technically F i, not Void, so if we pass F i to
inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive.
In order to avoid this pitfall, we need to normalise the type passed to
pmTopNormaliseType_maybe, using the constraint solver to solve for any local
equalities (such as i ~ Int) that may be in scope.
-}
-- | Generate all 'InhabitationCandidate's for a given type. The result is
......@@ -776,12 +805,14 @@ Which means that in source Haskell:
-- if it can. In this case, the candidates are the signature of the tycon, each
-- one accompanied by the term- and type- constraints it gives rise to.
-- See also Note [Checking EmptyCase Expressions]
inhabitationCandidates :: FamInstEnvs -> Type
inhabitationCandidates :: Bag EvVar -> Type
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
inhabitationCandidates fam_insts ty
= case pmTopNormaliseType_maybe fam_insts ty of
Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
Nothing -> alts_to_check ty ty []
inhabitationCandidates ty_cs ty = do
fam_insts <- liftD dsGetFamInstEnvs
mb_norm_res <- pmTopNormaliseType_maybe fam_insts ty_cs ty
case mb_norm_res of
Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
Nothing -> alts_to_check ty ty []
where
-- All these types are trivially inhabited
trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon
......
......@@ -1849,12 +1849,7 @@ tcUnboundId rn_expr unbound res_ty
; let occ = unboundVarOcc unbound
; name <- newSysName occ
; let ev = mkLocalId name ty
; loc <- getCtLocM HoleOrigin Nothing
; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty
, ctev_dest = EvVarDest ev
, ctev_nosh = WDeriv
, ctev_loc = loc}
, cc_hole = ExprHole unbound }
; can <- newHoleCt (ExprHole unbound) ev ty
; emitInsoluble can
; tcWrapResultO (UnboundOccurrenceOf occ) rn_expr (HsVar noExt (noLoc ev))
ty res_ty }
......
......@@ -39,7 +39,7 @@ module TcMType (
--------------------------------
-- Creating new evidence variables
newEvVar, newEvVars, newDict,
newWanted, newWanteds, cloneWanted, cloneWC,
newWanted, newWanteds, newHoleCt, cloneWanted, cloneWC,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
newTcEvBinds, newNoTcEvBinds, addTcEvBind,
......@@ -179,6 +179,16 @@ newWanted orig t_or_k pty
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)
-- | Create a new 'CHoleCan' 'Ct'.
newHoleCt :: Hole -> Id -> Type -> TcM Ct
newHoleCt hole ev ty = do
loc <- getCtLocM HoleOrigin Nothing
pure $ CHoleCan { cc_ev = CtWanted { ctev_pred = ty
, ctev_dest = EvVarDest ev
, ctev_nosh = WDeriv
, ctev_loc = loc }
, cc_hole = hole }
----------------------------------------------
-- Cloning constraints
----------------------------------------------
......
......@@ -10,6 +10,7 @@ module TcSimplify(
solveEqualities, solveLocalEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
tcNormalise,
captureTopConstraints,
......@@ -32,13 +33,15 @@ import Class ( Class, classKey, classTyCon )
import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
, WarnReason ( Reason )
, DynFlags( solverIterations ) )
import Id ( idType )
import HsExpr ( UnboundVar(..) )
import Id ( idType, mkLocalId )
import Inst
import ListSetOps
import Name
import Outputable
import PrelInfo
import PrelNames
import RdrName ( emptyGlobalRdrEnv )
import TcErrors
import TcEvidence
import TcInteract
......@@ -546,6 +549,35 @@ tcCheckSatisfiability given_ids
; solveSimpleGivens new_given
; getInertInsols }
-- | Normalise a type as much as possible using the given constraints.
-- See @Note [tcNormalise]@.
tcNormalise :: Bag EvVar -> Type -> TcM Type
tcNormalise given_ids ty
= do { lcl_env <- TcM.getLclEnv
; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
; wanted_ct <- mk_wanted_ct
; (res, _ev_binds) <- runTcS $
do { traceTcS "tcNormalise {" (ppr given_ids)
; let given_cts = mkGivens given_loc (bagToList given_ids)
; solveSimpleGivens given_cts
; wcs <- solveSimpleWanteds (unitBag wanted_ct)
-- It's an invariant that this wc_simple will always be
-- a singleton Ct, since that's what we fed in as input.
; let ty' = case bagToList (wc_simple wcs) of
(ct:_) -> ctEvPred (ctEvidence ct)
cts -> pprPanic "tcNormalise" (ppr cts)
; traceTcS "tcNormalise }" (ppr ty')
; pure ty' }
; return res }
where
mk_wanted_ct :: TcM Ct
mk_wanted_ct = do
let occ = mkVarOcc "$tcNorm"
name <- newSysName occ
let ev = mkLocalId name ty
hole = ExprHole $ OutOfScope occ emptyGlobalRdrEnv
newHoleCt hole ev ty
{- Note [Superclasses and satisfiability]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand superclasses before starting, because (Int ~ Bool), has
......@@ -566,6 +598,25 @@ the constraints /are/ satisfiable (Trac #10592 comment:12!).
For stratightforard situations without type functions the try_harder
step does nothing.
Note [tcNormalise]
~~~~~~~~~~~~~~~~~~
tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas
most invocations of the constraint solver are intended to simplify a set of
constraints or to decide if a particular set of constraints is satisfiable,
the purpose of tcNormalise is to take a type, plus some local constraints, and
normalise the type as much as possible with respect to those constraints.
Why is this useful? As one example, when coverage-checking an EmptyCase
expression, it's possible that the type of the scrutinee will only reduce
if some local equalities are solved for. See "Wrinkle: Local equalities"
in Note [Type normalisation for EmptyCase] in Check.
To accomplish its stated goal, tcNormalise first feeds the local constraints
into solveSimpleGivens, then stuffs the argument type in a CHoleCan, and feeds
that singleton Ct into solveSimpleWanteds, which reduces the type in the
CHoleCan as much as possible with respect to the local given constraints. When
solveSimpleWanteds is finished, we dig out the type from the CHoleCan and
return that.
***********************************************************************************
* *
......
......@@ -21,6 +21,7 @@ module MonadUtils
, foldlM, foldlM_, foldrM
, maybeMapM
, whenM, unlessM
, filterOutM
) where
-------------------------------------------------------------------------------
......@@ -31,6 +32,7 @@ import GhcPrelude
import Maybes
import Control.Applicative
import Control.Monad
import Control.Monad.Fix
import Control.Monad.IO.Class
......@@ -199,3 +201,8 @@ whenM mb thing = do { b <- mb
unlessM :: Monad m => m Bool -> m () -> m ()
unlessM condM acc = do { cond <- condM
; unless cond acc }
-- | Like 'filterM', only it reverses the sense of the test.
filterOutM :: (Applicative m) => (a -> m Bool) -> [a] -> m [a]
filterOutM p =
foldr (\ x -> liftA2 (\ flg -> if flg then id else (x:)) (p x)) (pure [])
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -Wall #-}
module T14813 where
import Data.Kind
import Data.Void
data SBool (z :: Bool) where
SFalse :: SBool 'False
STrue :: SBool 'True
type family F (b :: Bool) (a :: Type) :: Type where
F 'True a = a
F 'False _ = Void
dispatch :: forall (b :: Bool) (a :: Type). SBool b -> F b a -> a
dispatch STrue x = x
dispatch SFalse x = case x of {}
type family G a
type instance G Int = Void
fun :: i ~ Int => G i -> a
fun x = case x of {}
......@@ -36,15 +36,10 @@ data HsImplicitBndrs pass
fun2 :: HsImplicitBndrs (GhcPass pass) -> ()
fun2 UsefulConstructor = ()
{-
NB: the seemingly equivalent function
fun2' :: (p ~ GhcPass pass) => HsImplicitBndrs p -> ()
fun2' UsefulConstructor = ()
Is mistakenly deemed non-exhaustive at the moment due to #14813.
-}
-- Example 3
data Abyss = MkAbyss !Abyss
......
T15305.hs:53:23: warning: [-Wincomplete-patterns (in -Wextra)]
T15305.hs:48:23: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: (MkAbyss _)
......@@ -63,6 +63,8 @@ test('T14086', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T14098', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T14813', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T15305', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T15385', normal, compile,
......
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