From 4f1f9868ae79b5730c6aa14b05394d3f1d10a857 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 12 Aug 2017 15:51:37 -0400 Subject: Change isClosedAlgType to be TYPE-aware, and rename it to pmIsClosedType Summary: In a267580e4ab37115dcc33f3b8a9af67b9364da12, I somewhat awkwardly inserted a special case for `TYPE` in the `EmptyCase` coverage checker. Instead of placing it there, @mpickering noted that `isClosedAlgType` would be a better fit for it. I do just that in this patch. I also renamed `isClosedAlgType` to `pmIsClosedType`, reflecting the fact that `TYPE` technically isn't an algebraic type (it's a primitive one), and that its behavior is pattern-match coverage checking-oriented. I also moved it to `Check`, which is a better home for this function than `Type`. Luckily, the only call sites for `isClosedAlgType` were in the pattern-match coverage checker anyways, so this change is simple enough. Test Plan: ./validate Reviewers: mpickering, austin, goldfire, bgamari Reviewed By: goldfire Subscribers: rwbarton, thomie, mpickering GHC Trac Issues: #14086 Differential Revision: https://phabricator.haskell.org/D3830 --- compiler/deSugar/Check.hs | 161 +++++++++++++++++++++++++++++++++++++++---- compiler/types/FamInstEnv.hs | 114 +----------------------------- compiler/types/Type.hs | 13 +--- 3 files changed, 150 insertions(+), 138 deletions(-) diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index b0155d3e2f..ab2047fcf3 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -12,7 +12,10 @@ module Check ( checkSingle, checkMatches, isAnyPmCheckEnabled, -- See Note [Type and Term Equality Propagation] - genCaseTmCs1, genCaseTmCs2 + genCaseTmCs1, genCaseTmCs2, + + -- Pattern-match-specific type operations + pmIsClosedType, pmTopNormaliseType_maybe ) where #include "HsVersions.h" @@ -43,6 +46,7 @@ import TcType (toTcType, isStringTy, isIntTy, isWordTy) import Bag import ErrUtils import Var (EvVar) +import TyCoRep import Type import UniqSupply import DsGRHSs (isTrueLHsExpr) @@ -408,6 +412,147 @@ checkEmptyCase' var = do else PmResult FromBuiltin [] uncovered [] Nothing -> return emptyPmResult +-- | Returns 'True' if the argument 'Type' is a fully saturated application of +-- a closed type constructor. +-- +-- Closed type constructors are those with a fixed right hand side, as +-- opposed to e.g. associated types. These are of particular interest for +-- pattern-match coverage checking, because GHC can exhaustively consider all +-- possible forms that values of a closed type can take on. +-- +-- Note that this function is intended to be used to check types of value-level +-- patterns, so as a consequence, the 'Type' supplied as an argument to this +-- function should be of kind @Type@. +pmIsClosedType :: Type -> Bool +pmIsClosedType ty + = case splitTyConApp_maybe ty of + Just (tc, ty_args) + | is_algebraic_like tc && not (isFamilyTyCon tc) + -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True + _other -> False + where + -- This returns True for TyCons which /act like/ algebraic types. + -- (See "Type#type_classification" for what an algebraic type is.) + -- + -- This is qualified with \"like\" because of a particular special + -- case: TYPE (the underlyind kind behind Type, among others). TYPE + -- is conceptually a datatype (and thus algebraic), but in practice it is + -- a primitive builtin type, so we must check for it specially. + -- + -- NB: it makes sense to think of TYPE as a closed type in a value-level, + -- pattern-matching context. However, at the kind level, TYPE is certainly + -- not closed! Since this function is specifically tailored towards pattern + -- matching, however, it's OK to label TYPE as closed. + is_algebraic_like :: TyCon -> Bool + is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon + +pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type) +-- ^ Get rid of *outermost* (or toplevel) +-- * type function redex +-- * data family redex +-- * newtypes +-- +-- 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) + 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!). + -- This is the one that is equal (in source Haskell) to the initial type. + -- If none is found in the list, then all of them are type family + -- applications, so we simply return the last one, which is the *simplest*. + eq_src_ty :: Type -> [Type] -> Type + eq_src_ty ty tys = maybe ty id (find is_closed_or_data_family tys) + + is_closed_or_data_family :: Type -> Bool + is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyAppType ty + + -- For efficiency, represent both lists as difference lists. + -- comb performs the concatenation, for both lists. + comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2) + + stepper = newTypeStepper `composeSteppers` tyFamStepper + + -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into + -- a loop. If it would fall into a loop, it produces 'NS_Abort'. + newTypeStepper :: NormaliseStepper ([Type] -> [Type],[DataCon] -> [DataCon]) + newTypeStepper rec_nts tc tys + | Just (ty', _co) <- instNewTyCon_maybe tc tys + = case checkRecTc rec_nts tc of + Just rec_nts' -> let tyf = ((TyConApp tc tys):) + tmf = ((tyConSingleDataCon tc):) + in NS_Step rec_nts' ty' (tyf, tmf) + Nothing -> NS_Abort + | otherwise + = NS_Done + + tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon]) + tyFamStepper rec_nts tc tys -- Try to step a type/data family + = let (_args_co, ntys) = normaliseTcArgs env Representational tc tys in + -- NB: It's OK to use normaliseTcArgs here instead of + -- normalise_tc_args (which takes the LiftingContext described + -- in Note [Normalising types]) because the reduceTyFamApp below + -- works only at top level. We'll never recur in this function + -- after reducing the kind of a bound tyvar. + + case reduceTyFamApp_maybe env Representational tc ntys of + Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id) + _ -> NS_Done + +{- Note [Type normalisation for EmptyCase] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +EmptyCase is an exception for pattern matching, since it is strict. This means +that it boils down to checking whether the type of the scrutinee is inhabited. +Function pmTopNormaliseType_maybe gets rid of the outermost type function/data +family redex and newtypes, in search of an algebraic type constructor, which is +easier to check for inhabitation. + +It returns 3 results instead of one, because there are 2 subtle points: +1. Newtypes are isomorphic to the underlying type in core but not in the source + language, +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 + (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. + (b) dcs is the list of data constructors "skipped", every time we normalise a + 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) + implies + topNormaliseType_maybe env ty = Just (co, core_ty) + for some coercion co. + +To see how all cases come into play, consider the following example: + + data family T a :: * + data instance T Int = T1 | T2 Bool + -- Which gives rise to FC: + -- data T a + -- data R:TInt = T1 | T2 Bool + -- axiom ax_ti : T Int ~R R:TInt + + newtype G1 = MkG1 (T Int) + newtype G2 = MkG2 G1 + + type instance F Int = F Char + type instance F Char = G2 + +In this case pmTopNormaliseType_maybe env (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). +-} + -- | Generate all inhabitation candidates for a given type. The result is -- either (Left ty), if the type cannot be reduced to a closed algebraic type -- (or if it's one trivially inhabited, like Int), or (Right candidates), if it @@ -442,19 +587,7 @@ inhabitationCandidates fam_insts ty let va = build_tm (PmVar var) dcs return $ Right [(va, mkIdEq var, emptyBag)] - -- TYPE (which is the underlying kind behind Type, among others) - -- is conceptually an empty datatype, so one would expect this code - -- (from #14086) to compile without warnings: - -- - -- f :: Type -> Int - -- f x = case x of {} - -- - -- However, since TYPE is a primitive builtin type, not an actual - -- datatype, we must convince the coverage checker of this fact by - -- adding a special case here. - | tc == tYPETyCon -> pure (Right []) - - | isClosedAlgType core_ty -> liftD $ do + | pmIsClosedType core_ty -> liftD $ do var <- mkPmId (toTcType core_ty) -- it would be wrong to unify x alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc) return $ Right [(build_tm va dcs, eq, cs) | (va, eq, cs) <- alts] diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs index b9aa43957e..cec7b58e38 100644 --- a/compiler/types/FamInstEnv.hs +++ b/compiler/types/FamInstEnv.hs @@ -29,9 +29,8 @@ module FamInstEnv ( -- Normalisation topNormaliseType, topNormaliseType_maybe, - normaliseType, normaliseTcApp, + normaliseType, normaliseTcApp, normaliseTcArgs, reduceTyFamApp_maybe, - pmTopNormaliseType_maybe, -- Flattening flattenTys @@ -43,7 +42,6 @@ import Unify import Type import TyCoRep import TyCon -import DataCon (DataCon) import Coercion import CoAxiom import VarSet @@ -62,7 +60,7 @@ import SrcLoc import FastString import MonadUtils import Control.Monad -import Data.List( mapAccumL, find ) +import Data.List( mapAccumL ) {- ************************************************************************ @@ -1273,114 +1271,6 @@ topNormaliseType_maybe env ty Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co) _ -> NS_Done ---------------- -pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type) --- ^ Get rid of *outermost* (or toplevel) --- * type function redex --- * data family redex --- * newtypes --- --- 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) - 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!). - -- This is the one that is equal (in source Haskell) to the initial type. - -- If none is found in the list, then all of them are type family - -- applications, so we simply return the last one, which is the *simplest*. - eq_src_ty :: Type -> [Type] -> Type - eq_src_ty ty tys = maybe ty id (find is_alg_or_data_family tys) - - is_alg_or_data_family :: Type -> Bool - is_alg_or_data_family ty = isClosedAlgType ty || isDataFamilyAppType ty - - -- For efficiency, represent both lists as difference lists. - -- comb performs the concatenation, for both lists. - comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2) - - stepper = newTypeStepper `composeSteppers` tyFamStepper - - -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into - -- a loop. If it would fall into a loop, it produces 'NS_Abort'. - newTypeStepper :: NormaliseStepper ([Type] -> [Type],[DataCon] -> [DataCon]) - newTypeStepper rec_nts tc tys - | Just (ty', _co) <- instNewTyCon_maybe tc tys - = case checkRecTc rec_nts tc of - Just rec_nts' -> let tyf = ((TyConApp tc tys):) - tmf = ((tyConSingleDataCon tc):) - in NS_Step rec_nts' ty' (tyf, tmf) - Nothing -> NS_Abort - | otherwise - = NS_Done - - tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon]) - tyFamStepper rec_nts tc tys -- Try to step a type/data family - = let (_args_co, ntys) = normaliseTcArgs env Representational tc tys in - -- NB: It's OK to use normaliseTcArgs here instead of - -- normalise_tc_args (which takes the LiftingContext described - -- in Note [Normalising types]) because the reduceTyFamApp below - -- works only at top level. We'll never recur in this function - -- after reducing the kind of a bound tyvar. - - case reduceTyFamApp_maybe env Representational tc ntys of - Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id) - _ -> NS_Done - -{- Note [Type normalisation for EmptyCase] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -EmptyCase is an exception for pattern matching, since it is strict. This means -that it boils down to checking whether the type of the scrutinee is inhabited. -Function pmTopNormaliseType_maybe gets rid of the outermost type function/data -family redex and newtypes, in search of an algebraic type constructor, which is -easier to check for inhabitation. - -It returns 3 results instead of one, because there are 2 subtle points: -1. Newtypes are isomorphic to the underlying type in core but not in the source - language, -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 - (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. - (b) dcs is the list of data constructors "skipped", every time we normalise a - 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) - implies - topNormaliseType_maybe env ty = Just (co, core_ty) - for some coercion co. - -To see how all cases come into play, consider the following example: - - data family T a :: * - data instance T Int = T1 | T2 Bool - -- Which gives rise to FC: - -- data T a - -- data R:TInt = T1 | T2 Bool - -- axiom ax_ti : T Int ~R R:TInt - - newtype G1 = MkG1 (T Int) - newtype G2 = MkG2 G1 - - type instance F Int = F Char - type instance F Char = G2 - -In this case pmTopNormaliseType_maybe env (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). --} - --------------- normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type) -- See comments on normaliseType for the arguments of this function diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index dcc134cbe3..f43e0e0b56 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -110,7 +110,7 @@ module Type ( -- (Lifting and boxity) isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType, - isAlgType, isClosedAlgType, isDataFamilyAppType, + isAlgType, isDataFamilyAppType, isPrimitiveType, isStrictType, isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy, dropRuntimeRepArgs, @@ -2019,17 +2019,6 @@ isAlgType ty isAlgTyCon tc _other -> False --- | See "Type#type_classification" for what an algebraic type is. --- Should only be applied to /types/, as opposed to e.g. partially --- saturated type constructors. Closed type constructors are those --- with a fixed right hand side, as opposed to e.g. associated types -isClosedAlgType :: Type -> Bool -isClosedAlgType ty - = case splitTyConApp_maybe ty of - Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc) - -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True - _other -> False - -- | Check whether a type is a data family type isDataFamilyAppType :: Type -> Bool isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of -- cgit v1.2.1