Commit a693d1cb authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 609d2c81
......@@ -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
......
......@@ -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 = ([], [])
{-# 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
......@@ -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, [''])
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