[commit: ghc] master: Correct order of existentials in pattern synonyms (a693d1c)
git at git.haskell.org
git at git.haskell.org
Mon Oct 17 07:42:36 UTC 2016
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/a693d1cb0ee9499af3145d73b1aebe5b6df0da98/ghc
>---------------------------------------------------------------
commit a693d1cb0ee9499af3145d73b1aebe5b6df0da98
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Oct 14 15:54:14 2016 +0100
Correct order of existentials in pattern synonyms
Trac #12698 exposed a nasty bug in the typechecking for
pattern synonmys: the existential type variables weren't
being put in properly-scoped order.
For some reason TcPatSyn.tcCollectEx was colleting them as a
set, not as a list! Easily fixed.
>---------------------------------------------------------------
a693d1cb0ee9499af3145d73b1aebe5b6df0da98
compiler/hsSyn/HsPat.hs | 1 +
compiler/typecheck/TcPatSyn.hs | 35 +++++++-------
testsuite/tests/patsyn/should_compile/T12698.hs | 62 +++++++++++++++++++++++++
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 56e736a..ec5578f 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 548b746..e6c5074 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 at ConPatOut{} = merge (FV.mkFVs (pat_tvs con), pat_dicts con) $
- goConDetails $ pat_args con
+ go1 con at 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 0000000..6ba45e4
--- /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 d26fc84..4426c74 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, [''])
More information about the ghc-commits
mailing list