diff options
| -rw-r--r-- | compiler/hsSyn/HsPat.hs | 1 | ||||
| -rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 35 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T12698.hs | 62 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/all.T | 1 |
4 files changed, 81 insertions, 18 deletions
diff --git a/compiler/hsSyn/HsPat.hs b/compiler/hsSyn/HsPat.hs index 56e736a2dd..ec5578f36d 100644 --- a/compiler/hsSyn/HsPat.hs +++ b/compiler/hsSyn/HsPat.hs @@ -175,6 +175,7 @@ data Pat id -- the type of the pattern pat_tvs :: [TyVar], -- Existentially bound type variables + -- in correctly-scoped order e.g. [k:*, x:k] pat_dicts :: [EvVar], -- Ditto *coercion variables* and *dictionaries* -- One reason for putting coercion variable here, I think, -- is to ensure their kinds are zonked diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 548b746fc4..e6c5074935 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -48,7 +48,6 @@ import FieldLabel import Bag import Util import ErrUtils -import FV import Control.Monad ( zipWithM ) import Data.List( partition ) @@ -84,12 +83,13 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl NoRestrictions [] named_taus wanted - ; let ((ex_tvs, ex_vars), prov_dicts) = tcCollectEx lpat' - univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs + ; 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 - ; traceTc "tcInferPatSynDecl }" $ ppr name + ; 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) @@ -802,17 +802,16 @@ nonBidirectionalErr name = failWithTc $ -- to be passed these pattern-bound evidences. tcCollectEx :: LPat Id - -> ( ([Var], VarSet) -- Existentially-bound type variables as a - -- deterministically ordered list and a set. - -- See Note [Deterministic FV] in FV - , [EvVar] - ) -tcCollectEx pat = let (fv, evs) = go pat in (fvVarListVarSet fv, evs) + -> ( [TyVar] -- Existentially-bound type variables + -- in correctly-scoped order; e.g. [ k:*, x:k ] + , [EvVar] ) -- and evidence variables + +tcCollectEx pat = go pat where - go :: LPat Id -> (FV, [EvVar]) + go :: LPat Id -> ([TyVar], [EvVar]) go = go1 . unLoc - go1 :: Pat Id -> (FV, [EvVar]) + go1 :: Pat Id -> ([TyVar], [EvVar]) go1 (LazyPat p) = go p go1 (AsPat _ p) = go p go1 (ParPat p) = go p @@ -822,23 +821,23 @@ tcCollectEx pat = let (fv, evs) = go pat in (fvVarListVarSet fv, evs) go1 (SumPat p _ _ _) = go p go1 (PArrPat ps _) = mergeMany . map go $ ps go1 (ViewPat _ p _) = go p - go1 con@ConPatOut{} = merge (FV.mkFVs (pat_tvs con), pat_dicts con) $ - goConDetails $ pat_args con + go1 con@ConPatOut{} = merge (pat_tvs con, pat_dicts con) $ + goConDetails $ pat_args con go1 (SigPatOut p _) = go p go1 (CoPat _ p _) = go1 p go1 (NPlusKPat n k _ geq subtract _) = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract go1 _ = empty - goConDetails :: HsConPatDetails Id -> (FV, [EvVar]) + goConDetails :: HsConPatDetails Id -> ([TyVar], [EvVar]) goConDetails (PrefixCon ps) = mergeMany . map go $ ps goConDetails (InfixCon p1 p2) = go p1 `merge` go p2 goConDetails (RecCon HsRecFields{ rec_flds = flds }) = mergeMany . map goRecFd $ flds - goRecFd :: LHsRecField Id (LPat Id) -> (FV, [EvVar]) + goRecFd :: LHsRecField Id (LPat Id) -> ([TyVar], [EvVar]) goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p - merge (vs1, evs1) (vs2, evs2) = (vs1 `unionFV` vs2, evs1 ++ evs2) + merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2) mergeMany = foldr merge empty - empty = (emptyFV, []) + empty = ([], []) diff --git a/testsuite/tests/patsyn/should_compile/T12698.hs b/testsuite/tests/patsyn/should_compile/T12698.hs new file mode 100644 index 0000000000..6ba45e4e85 --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T12698.hs @@ -0,0 +1,62 @@ +{-# Language ViewPatterns, TypeOperators, KindSignatures, PolyKinds, + TypeInType, StandaloneDeriving, GADTs, RebindableSyntax, + RankNTypes, LambdaCase, PatternSynonyms, TypeApplications #-} + +module T12698 where + +import GHC.Types +import Prelude hiding ( fromInteger ) +import Data.Type.Equality +import Data.Kind +import qualified Prelude + +class Ty (a :: k) where ty :: T a +instance Ty Int where ty = TI +instance Ty Bool where ty = TB +instance Ty a => Ty [a] where ty = TA TL ty +instance Ty [] where ty = TL +instance Ty (,) where ty = TP + +data AppResult (t :: k) where + App :: T a -> T b -> AppResult (a b) + +data T :: forall k. k -> Type where + TI :: T Int + TB :: T Bool + TL :: T [] + TP :: T (,) + TA :: T f -> T x -> T (f x) +deriving instance Show (T a) + +splitApp :: T a -> Maybe (AppResult a) +splitApp = \case + TI -> Nothing + TB -> Nothing + TL -> Nothing + TP -> Nothing + TA f x -> Just (App f x) + +data (a :: k1) :~~: (b :: k2) where + HRefl :: a :~~: a + +eqT :: T a -> T b -> Maybe (a :~~: b) +eqT a b = + case (a, b) of + (TI, TI) -> Just HRefl + (TB, TB) -> Just HRefl + (TL, TL) -> Just HRefl + (TP, TP) -> Just HRefl + +pattern List :: () => [] ~~ b => T b +pattern List <- (eqT (ty @(Type -> Type) @[]) -> Just HRefl) + where List = ty + +pattern Int :: () => Int ~~ b => T b +pattern Int <- (eqT (ty @Type @Int) -> Just HRefl) + where Int = ty + +pattern (:<->:) :: () => fx ~ f x => T f -> T x -> T fx +pattern f :<->: x <- (splitApp -> Just (App f x)) + where f :<->: x = TA f x + +pattern Foo <- List :<->: Int diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index d26fc84bec..4426c74733 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -60,3 +60,4 @@ test('T12108', normal, compile, ['']) test('T12484', normal, compile, ['']) test('T11987', normal, multimod_compile, ['T11987', '-v0']) test('T12615', normal, compile, ['']) +test('T12698', normal, compile, ['']) |