Correct order of existentials in pattern synonyms
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 14 Oct 2016 14:54:14 +0000 (15:54 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 17 Oct 2016 07:41:23 +0000 (08:41 +0100)
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.

compiler/hsSyn/HsPat.hs
compiler/typecheck/TcPatSyn.hs
testsuite/tests/patsyn/should_compile/T12698.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_compile/all.T

index 56e736a..ec5578f 100644 (file)
@@ -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
index 548b746..e6c5074 100644 (file)
@@ -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 (file)
index 0000000..6ba45e4
--- /dev/null
@@ -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
index d26fc84..4426c74 100644 (file)
@@ -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, [''])