diff options
Diffstat (limited to 'compiler/typecheck/TcPatSyn.hs')
| -rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 56 |
1 files changed, 51 insertions, 5 deletions
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 58d1506812..283127215c 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -20,6 +20,7 @@ import TcPat import Type( mkEmptyTCvSubst, tidyTyVarBinders, tidyTypes, tidyType ) import TcRnMonad import TcSigs( emptyPragEnv, completeSigFromId ) +import TcType( mkMinimalBySCs ) import TcEnv import TcMType import TcHsSyn( zonkTyVarBindersX, zonkTcTypeToTypes @@ -88,18 +89,44 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, ; let (ex_tvs, prov_dicts) = tcCollectEx lpat' ex_tv_set = mkVarSet ex_tvs univ_tvs = filterOut (`elemVarSet` ex_tv_set) qtvs - prov_theta = map evVarPred prov_dicts req_theta = map evVarPred req_dicts + ; prov_dicts <- mapM zonkId prov_dicts + ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts + prov_theta = map evVarPred filtered_prov_dicts + -- Filtering: see Note [Remove redundant provided dicts] + ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs) ; tc_patsyn_finish lname dir is_infix lpat' (mkTyVarBinders Inferred univ_tvs , req_theta, ev_binds, req_dicts) (mkTyVarBinders Inferred ex_tvs - , mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts) + , mkTyVarTys ex_tvs, prov_theta, map EvId filtered_prov_dicts) (map nlHsVar args, map idType args) pat_ty rec_fields } +{- Note [Remove redundant provided dicts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Recall that + HRefl :: forall k1 k2 (a1:k1) (a2:k2). (k1 ~ k2, a1 ~ a2) + => a1 :~~: a2 +(NB: technically the (k1~k2) existential dictionary is not necessary, +but it's there at the moment.) + +Now consider (Trac #14394): + pattern Foo = HRefl +in a non-poly-kinded module. We don't want to get + pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b +with that redundant (* ~ *). We'd like to remove it; hence the call to +mkMinimalWithSCs. + +Similarly consider + data S a where { MkS :: Ord a => a -> S a } + pattern Bam x y <- (MkS (x::a), MkS (y::a))) + +The pattern (Bam x y) binds two (Ord a) dictionaries, but we only +need one. Agian mkMimimalWithSCs removes the redundant one. +-} tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn -> TcPatSynInfo @@ -332,7 +359,7 @@ tc_patsyn_finish lname dir is_infix lpat' (ze, univ_tvs') <- zonkTyVarBindersX emptyZonkEnv univ_tvs ; req_theta' <- zonkTcTypeToTypes ze req_theta ; (ze, ex_tvs') <- zonkTyVarBindersX ze ex_tvs - ; prov_theta' <- zonkTcTypeToTypes ze prov_theta + ; prov_theta' <- zonkTcTypeToTypes ze prov_theta ; pat_ty' <- zonkTcTypeToType ze pat_ty ; arg_tys' <- zonkTcTypeToTypes ze arg_tys @@ -813,10 +840,13 @@ tcCheckPatSynPat = go go = addLocM go1 go1 :: Pat GhcRn -> TcM () + -- See Note [Bad patterns] + go1 p@(AsPat _ _) = asPatInPatSynErr p + go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p + go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info) go1 VarPat{} = return () go1 WildPat{} = return () - go1 p@(AsPat _ _) = asPatInPatSynErr p go1 (LazyPat pat) = go pat go1 (ParPat pat) = go pat go1 (BangPat pat) = go pat @@ -833,7 +863,6 @@ tcCheckPatSynPat = go = do addModFinalizersWithLclEnv mod_finalizers go1 pat | otherwise = panic "non-pattern from spliced thing" - go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p go1 ConPatOut{} = panic "ConPatOut in output of renamer" go1 SigPatOut{} = panic "SigPatOut in output of renamer" go1 CoPat{} = panic "CoPat in output of renamer" @@ -850,6 +879,23 @@ nPlusKPatInPatSynErr pat hang (text "Pattern synonym definition cannot contain n+k-pattern:") 2 (ppr pat) +{- Note [Bad patterns] +~~~~~~~~~~~~~~~~~~~~~~ +We don't currently allow as-patterns or n+k patterns in a pattern synonym. +Reason: consider + pattern P x y = x@(Just y) + +What would + f (P Nothing False) = e +mean? Presumably something like + f Nothing@(Just False) = e +But as-patterns don't allow a pattern before the @ sign! Perhaps they +should -- with p1@p2 meaning match both p1 and p2 -- but they don't +currently. Hence bannning them in pattern synonyms. Actually lifting +the restriction would be simple and well-defined. See Trac #9793. +-} + + nonBidirectionalErr :: Outputable name => name -> TcM a nonBidirectionalErr name = failWithTc $ text "non-bidirectional pattern synonym" |