Minimise provided dictionaries in pattern synonyms
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 8 Nov 2017 08:52:06 +0000 (08:52 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 8 Nov 2017 11:12:37 +0000 (11:12 +0000)
Trac #14394 showed that it's possible to get redundant
constraints in the inferred provided constraints of a pattern
synonym.  This patch removes the redundancy with mkMinimalBySCs.

To do this I had to generalise the type of mkMinimalBySCs slightly.
And, to reduce confusing reversal, I made it stable: it now returns
its result in the same order as its input.  That led to a raft of
error message wibbles, mostly for the better.

29 files changed:
compiler/typecheck/TcDerivInfer.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
testsuite/tests/ado/ado004.stderr
testsuite/tests/deriving/should_fail/drvfail004.stderr
testsuite/tests/determinism/determ021/determ021.stdout
testsuite/tests/ghci/scripts/T10963.stdout
testsuite/tests/ghci/scripts/T11524a.stdout
testsuite/tests/ghci/scripts/T11975.stdout
testsuite/tests/ghci/scripts/T12550.stdout
testsuite/tests/indexed-types/should_compile/T3017.stderr
testsuite/tests/indexed-types/should_compile/T8889.stderr
testsuite/tests/indexed-types/should_fail/T1897b.stderr
testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
testsuite/tests/partial-sigs/should_compile/T12844.stderr
testsuite/tests/partial-sigs/should_compile/T13482.stderr
testsuite/tests/partial-sigs/should_compile/T14217.stderr
testsuite/tests/patsyn/should_compile/T11213.stderr
testsuite/tests/patsyn/should_compile/T14394.script [new file with mode: 0644]
testsuite/tests/patsyn/should_compile/T14394.stdout [new file with mode: 0644]
testsuite/tests/patsyn/should_compile/all.T
testsuite/tests/rebindable/rebindable6.stderr
testsuite/tests/typecheck/should_compile/Makefile
testsuite/tests/typecheck/should_compile/holes2.stderr
testsuite/tests/typecheck/should_fail/T8883.stderr
testsuite/tests/typecheck/should_fail/tcfail133.stderr

index 9095977..efad80f 100644 (file)
@@ -704,7 +704,7 @@ simplifyDeriv pred tvs thetas
          vcat [ ppr tvs_skols, ppr residual_simple, ppr good, ppr bad ]
 
        -- Return the good unsolved constraints (unskolemizing on the way out.)
-       ; let min_theta = mkMinimalBySCs (bagToList good)
+       ; let min_theta = mkMinimalBySCs id (bagToList good)
              -- An important property of mkMinimalBySCs (used above) is that in
              -- addition to removing constraints that are made redundant by
              -- superclass relationships, it also removes _duplicate_
index 0c6b54d..0e213be 100644 (file)
@@ -2374,10 +2374,7 @@ mkDictErr ctxt cts
     -- When simplifying [W] Ord (Set a), we need
     --    [W] Eq a, [W] Ord a
     -- but we really only want to report the latter
-    elim_superclasses cts
-      = filter (\ct -> any (eqType (ctPred ct)) min_preds) cts
-      where
-        min_preds = mkMinimalBySCs (map ctPred cts)
+    elim_superclasses cts = mkMinimalBySCs ctPred cts
 
 mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
             -> TcM (ReportErrCtxt, SDoc)
index 58d1506..2831272 100644 (file)
@@ -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"
index a5150e6..627a378 100644 (file)
@@ -832,7 +832,7 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
        -- into quantified skolems, so we have to zonk again
        ; candidates <- TcM.zonkTcTypes candidates
        ; let theta = pickQuantifiablePreds (mkVarSet qtvs) $
-                     mkMinimalBySCs $  -- See Note [Minimize by Superclasses]
+                     mkMinimalBySCs id $  -- See Note [Minimize by Superclasses]
                      candidates
 
        ; traceTc "decideQuantification"
index d752d1e..5e1e4be 100644 (file)
@@ -15,7 +15,7 @@ The "tc" prefix is for "TypeChecker", because the type checker
 is the principal client.
 -}
 
-{-# LANGUAGE CPP, MultiWayIf, FlexibleContexts #-}
+{-# LANGUAGE CPP, ScopedTypeVariables, MultiWayIf, FlexibleContexts #-}
 
 module TcType (
   --------------------------------
@@ -1949,29 +1949,47 @@ pickCapturedPreds qtvs theta
 
 -- Superclasses
 
-type PredWithSCs = (PredType, [PredType])
+type PredWithSCs a = (PredType, [PredType], a)
 
-mkMinimalBySCs :: [PredType] -> [PredType]
--- Remove predicates that can be deduced from others by superclasses,
--- including duplicate predicates. The result is a subset of the input.
-mkMinimalBySCs ptys = go preds_with_scs []
+mkMinimalBySCs :: forall a. (a -> PredType) -> [a] -> [a]
+-- Remove predicates that
+--
+--   - are the same as another predicate
+--
+--   - can be deduced from another by superclasses,
+--
+--   - are a reflexive equality (e.g  * ~ *)
+--     (see Note [Remove redundant provided dicts] in PatSyn)
+--
+-- The result is a subset of the input.
+-- The 'a' is just paired up with the PredType;
+--   typically it might be a dictionary Id
+mkMinimalBySCs get_pred xs = go preds_with_scs []
  where
-   preds_with_scs :: [PredWithSCs]
-   preds_with_scs = [ (pred, pred : transSuperClasses pred)
-                    | pred <- ptys ]
-
-   go :: [PredWithSCs]   -- Work list
-      -> [PredWithSCs]   -- Accumulating result
-      -> [PredType]
-   go [] min_preds = map fst min_preds
-   go (work_item@(p,_) : work_list) min_preds
+   preds_with_scs :: [PredWithSCs a]
+   preds_with_scs = [ (pred, pred : transSuperClasses pred, x)
+                    | x <- xs
+                    , let pred = get_pred x ]
+
+   go :: [PredWithSCs a]   -- Work list
+      -> [PredWithSCs a]   -- Accumulating result
+      -> [a]
+   go [] min_preds
+     = reverse (map thdOf3 min_preds)
+       -- The 'reverse' isn't strictly necessary, but it
+       -- means that the results are returned in the same
+       -- order as the input, which is generally saner
+   go (work_item@(p,_,_) : work_list) min_preds
+     | EqPred _ t1 t2 <- classifyPredType p
+     , t1 `tcEqType` t2   -- See Note [Discard reflexive equalities]
+     = go work_list min_preds
      | p `in_cloud` work_list || p `in_cloud` min_preds
      = go work_list min_preds
      | otherwise
      = go work_list (work_item : min_preds)
 
-   in_cloud :: PredType -> [PredWithSCs] -> Bool
-   in_cloud p ps = or [ p `eqType` p' | (_, scs) <- ps, p' <- scs ]
+   in_cloud :: PredType -> [PredWithSCs a] -> Bool
+   in_cloud p ps = or [ p `tcEqType` p' | (_, scs, _) <- ps, p' <- scs ]
 
 transSuperClasses :: PredType -> [PredType]
 -- (transSuperClasses p) returns (p's superclasses) not including p
index a3ef9e9..c4c7c0b 100644 (file)
@@ -9,37 +9,37 @@ TYPE SIGNATURES
     forall (f :: * -> *). Applicative f => (Int -> f Int) -> f Int
   test2 ::
     forall (f :: * -> *) t b.
-    (Num b, Num t, Applicative f) =>
+    (Applicative f, Num t, Num b) =>
     (t -> f b) -> f b
   test2a ::
     forall (f :: * -> *) t b.
-    (Num b, Num t, Functor f) =>
+    (Functor f, Num t, Num b) =>
     (t -> f b) -> f b
   test2b ::
-    forall (m :: * -> *) t a. (Num t, Monad m) => (t -> a) -> m a
+    forall (m :: * -> *) t a. (Monad m, Num t) => (t -> a) -> m a
   test2c ::
     forall (f :: * -> *) t b.
-    (Num b, Num t, Functor f) =>
+    (Functor f, Num t, Num b) =>
     (t -> f b) -> f b
   test2d ::
     forall (f :: * -> *) t1 b t2.
-    (Num b, Num t1, Functor f) =>
+    (Functor f, Num t1, Num b) =>
     (t1 -> f t2) -> f b
   test3 ::
     forall (m :: * -> *) t1 t2 a.
-    (Num t1, Monad m) =>
+    (Monad m, Num t1) =>
     (t1 -> m t2) -> (t2 -> t2 -> m a) -> m a
   test4 ::
     forall (m :: * -> *) t a1 a2.
-    (Num t, Monad m) =>
+    (Monad m, Num t) =>
     (t -> m a1) -> (a1 -> a1 -> m a2) -> m a2
   test5 ::
     forall (m :: * -> *) t a1 a2.
-    (Num t, Monad m) =>
+    (Monad m, Num t) =>
     (t -> m a1) -> (a1 -> a1 -> m a2) -> m a2
   test6 ::
     forall (m :: * -> *) a p.
-    (Num (m a), Monad m) =>
+    (Monad m, Num (m a)) =>
     (m a -> m (m a)) -> p -> m a
 TYPE CONSTRUCTORS
 COERCION AXIOMS
index 1b2d635..d182565 100644 (file)
@@ -2,7 +2,7 @@
 drvfail004.hs:8:12: error:
     • Could not deduce (Eq (Foo a b))
         arising from the 'deriving' clause of a data type declaration
-      from the context: (Ord b, Ord a)
+      from the context: (Ord a, Ord b)
         bound by the deriving clause for ‘Ord (Foo a b)’
         at drvfail004.hs:8:12-14
       Possible fix:
index 771a3af..3e8d27b 100644 (file)
@@ -2,7 +2,7 @@
 TYPE SIGNATURES
   test2 ::
     forall (f :: * -> *) t b.
-    (Num b, Num t, Applicative f) =>
+    (Applicative f, Num t, Num b) =>
     (t -> f b) -> f b
 TYPE CONSTRUCTORS
 COERCION AXIOMS
@@ -13,7 +13,7 @@ Dependent packages: [base-4.11.0.0, ghc-prim-0.5.2.0,
 TYPE SIGNATURES
   test2 ::
     forall (f :: * -> *) t b.
-    (Num b, Num t, Applicative f) =>
+    (Applicative f, Num t, Num b) =>
     (t -> f b) -> f b
 TYPE CONSTRUCTORS
 COERCION AXIOMS
index bf639a8..415c473 100644 (file)
@@ -1,4 +1,4 @@
-mapM :: (Monad m, Traversable t) => (a -> m b) -> t a -> m (t b)
+mapM :: (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b)
 mapM :: Monad m => (a -> m b) -> [a] -> m [b]
 length :: [a] -> Int
 foo :: Double -> Double
index 007d2ae..d1ab96e 100644 (file)
@@ -4,14 +4,14 @@ pattern P :: Bool     -- Defined at <interactive>:16:1
 pattern Pe :: a -> Ex  -- Defined at <interactive>:17:1
 pattern Pu :: p -> p   -- Defined at <interactive>:18:1
 pattern Pue :: a -> a1 -> (a, Ex)      -- Defined at <interactive>:19:1
-pattern Pur :: (Num a, Eq a) => a -> [a]
+pattern Pur :: (Eq a, Num a) => a -> [a]
        -- Defined at <interactive>:20:1
-pattern Purp :: (Num a, Eq a) => Show a1 => a
+pattern Purp :: (Eq a, Num a) => Show a1 => a
                                             -> a1 -> ([a], UnivProv a1)
        -- Defined at <interactive>:21:1
-pattern Pure :: (Num a, Eq a) => a -> a1 -> ([a], Ex)
+pattern Pure :: (Eq a, Num a) => a -> a1 -> ([a], Ex)
        -- Defined at <interactive>:22:1
-pattern Purep :: (Num a, Eq a) => Show a1 => a
+pattern Purep :: (Eq a, Num a) => Show a1 => a
                                              -> a1 -> ([a], ExProv)
        -- Defined at <interactive>:23:1
 pattern Pep :: () => Show a => a -> ExProv
@@ -29,15 +29,15 @@ pattern Pe :: () => forall {a}. a -> Ex
 pattern Pu :: forall {p}. p -> p       -- Defined at <interactive>:18:1
 pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex)
        -- Defined at <interactive>:19:1
-pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a]
+pattern Pur :: forall {a}. (Eq a, Num a) => a -> [a]
        -- Defined at <interactive>:20:1
-pattern Purp :: forall {a} {a1}. (Num a, Eq a) => Show a1 => a
+pattern Purp :: forall {a} {a1}. (Eq a, Num a) => Show a1 => a
                                                              -> a1 -> ([a], UnivProv a1)
        -- Defined at <interactive>:21:1
-pattern Pure :: forall {a}. (Num a, Eq a) => forall {a1}. a
+pattern Pure :: forall {a}. (Eq a, Num a) => forall {a1}. a
                                                           -> a1 -> ([a], Ex)
        -- Defined at <interactive>:22:1
-pattern Purep :: forall {a}. (Num a, Eq a) => forall {a1}. Show
+pattern Purep :: forall {a}. (Eq a, Num a) => forall {a1}. Show
                                                              a1 => a -> a1 -> ([a], ExProv)
        -- Defined at <interactive>:23:1
 pattern Pep :: () => forall {a}. Show a => a -> ExProv
index 1a3dd43..464ae2e 100644 (file)
@@ -1,6 +1,6 @@
 mapM
   :: forall {t :: * -> *} {m :: * -> *} {a} {b}.
-     (Monad m, Traversable t) =>
+     (Traversable t, Monad m) =>
      (a -> m b) -> t a -> m (t b)
 mapM
   :: forall (t :: * -> *).
index d4ac6b8..0955db3 100644 (file)
@@ -35,15 +35,15 @@ instance ∀ i (c ∷ Meta) (f ∷ ★ → ★). Functor f ⇒ Functor (M1 i c f
   -- Defined in ‘GHC.Generics’
 instance ∀ i c. Functor (K1 i c) -- Defined in ‘GHC.Generics’
 instance ∀ (f ∷ ★ → ★) (g ∷ ★ → ★).
-         (Functor g, Functor f) ⇒
+         (Functor f, Functor g) ⇒
          Functor (f :.: g)
   -- Defined in ‘GHC.Generics’
 instance ∀ (f ∷ ★ → ★) (g ∷ ★ → ★).
-         (Functor g, Functor f) ⇒
+         (Functor f, Functor g) ⇒
          Functor (f :+: g)
   -- Defined in ‘GHC.Generics’
 instance ∀ (f ∷ ★ → ★) (g ∷ ★ → ★).
-         (Functor g, Functor f) ⇒
+         (Functor f, Functor g) ⇒
          Functor (f :*: g)
   -- Defined in ‘GHC.Generics’
 instance ∀ a. Functor (Either a) -- Defined in ‘Data.Either’
index 0cef535..4a0ac28 100644 (file)
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   insert :: forall c. Coll c => Elem c -> c -> c
   test2 ::
-    forall c a b. (Elem c ~ (a, b), Num b, Num a, Coll c) => c -> c
+    forall c a b. (Coll c, Num a, Num b, Elem c ~ (a, b)) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c :: * open
index cef00df..551ced7 100644 (file)
@@ -1,4 +1,4 @@
 
 T8889.hs:12:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      f :: (C f, C_fmap f a) => (a -> b) -> f a -> f b
+      f :: (C_fmap f a, C f) => (a -> b) -> f a -> f b
index 7694672..5910998 100644 (file)
@@ -9,5 +9,5 @@ T1897b.hs:16:1: error:
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
         isValid :: forall (t :: * -> *) a.
-                   (Bug a, Foldable t) =>
+                   (Foldable t, Bug a) =>
                    t (Depend a) -> Bool
index 83edd5a..3d72b56 100644 (file)
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  arbitCs1 :: forall a. (Eq a, Enum a, Show a) => a -> String
+  arbitCs1 :: forall a. (Show a, Enum a, Eq a) => a -> String
   arbitCs2 :: forall a. (Show a, Enum a, Eq a) => a -> String
   arbitCs3 :: forall a. (Show a, Enum a, Eq a) => a -> String
   arbitCs4 :: forall a. (Eq a, Show a, Enum a) => a -> String
index 824bf3c..2de5614 100644 (file)
@@ -21,8 +21,8 @@ TYPE SIGNATURES
   >> :: forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
   >>= ::
     forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
-  ^ :: forall b a. (Num a, Integral b) => a -> b -> a
-  ^^ :: forall a b. (Integral b, Fractional a) => a -> b -> a
+  ^ :: forall b a. (Integral b, Num a) => a -> b -> a
+  ^^ :: forall a b. (Fractional a, Integral b) => a -> b -> a
   abs :: forall a. Num a => a -> a
   acos :: forall a. Floating a => a -> a
   acosh :: forall a. Floating a => a -> a
@@ -39,7 +39,7 @@ TYPE SIGNATURES
   atan2 :: forall a. RealFloat a => a -> a -> a
   atanh :: forall a. Floating a => a -> a
   break :: forall a. (a -> Bool) -> [a] -> ([a], [a])
-  ceiling :: forall a b. (Integral b, RealFrac a) => a -> b
+  ceiling :: forall a b. (RealFrac a, Integral b) => a -> b
   compare :: forall a. Ord a => a -> a -> Ordering
   concat :: forall (t :: * -> *) a. P.Foldable t => t [a] -> [a]
   concatMap ::
@@ -56,7 +56,7 @@ TYPE SIGNATURES
   dropWhile :: forall a. (a -> Bool) -> [a] -> [a]
   either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
   elem ::
-    forall (t :: * -> *) a. (Eq a, P.Foldable t) => a -> t a -> Bool
+    forall (t :: * -> *) a. (P.Foldable t, Eq a) => a -> t a -> Bool
   encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
   enumFrom :: forall a. Enum a => a -> [a]
   enumFromThen :: forall a. Enum a => a -> a -> [a]
@@ -72,7 +72,7 @@ TYPE SIGNATURES
   floatDigits :: forall a. RealFloat a => a -> Int
   floatRadix :: forall a. RealFloat a => a -> Integer
   floatRange :: forall a. RealFloat a => a -> (Int, Int)
-  floor :: forall a b. (Integral b, RealFrac a) => a -> b
+  floor :: forall a b. (RealFrac a, Integral b) => a -> b
   fmap ::
     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
   foldl ::
@@ -89,7 +89,7 @@ TYPE SIGNATURES
     forall (t :: * -> *) a. P.Foldable t => (a -> a -> a) -> t a -> a
   fromEnum :: forall a. Enum a => a -> Int
   fromInteger :: forall a. Num a => Integer -> a
-  fromIntegral :: forall a b. (Num b, Integral a) => a -> b
+  fromIntegral :: forall a b. (Integral a, Num b) => a -> b
   fromRational :: forall a. Fractional a => Rational -> a
   fst :: forall a b. (a, b) -> a
   gcd :: forall a. Integral a => a -> a -> a
@@ -118,26 +118,26 @@ TYPE SIGNATURES
   map :: forall a b. (a -> b) -> [a] -> [b]
   mapM ::
     forall (t :: * -> *) (m :: * -> *) a b.
-    (Monad m, P.Traversable t) =>
+    (P.Traversable t, Monad m) =>
     (a -> m b) -> t a -> m (t b)
   mapM_ ::
     forall (t :: * -> *) (m :: * -> *) a b.
-    (Monad m, P.Foldable t) =>
+    (P.Foldable t, Monad m) =>
     (a -> m b) -> t a -> m ()
   max :: forall a. Ord a => a -> a -> a
   maxBound :: forall w. Bounded w => w
   maximum ::
-    forall (t :: * -> *) a. (Ord a, P.Foldable t) => t a -> a
+    forall (t :: * -> *) a. (P.Foldable t, Ord a) => t a -> a
   maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
   min :: forall a. Ord a => a -> a -> a
   minBound :: forall w. Bounded w => w
   minimum ::
-    forall (t :: * -> *) a. (Ord a, P.Foldable t) => t a -> a
+    forall (t :: * -> *) a. (P.Foldable t, Ord a) => t a -> a
   mod :: forall a. Integral a => a -> a -> a
   negate :: forall a. Num a => a -> a
   not :: Bool -> Bool
   notElem ::
-    forall (t :: * -> *) a. (Eq a, P.Foldable t) => a -> t a -> Bool
+    forall (t :: * -> *) a. (P.Foldable t, Eq a) => a -> t a -> Bool
   null :: forall (t :: * -> *) a. P.Foldable t => t a -> Bool
   odd :: forall a. Integral a => a -> Bool
   or :: forall (t :: * -> *). P.Foldable t => t Bool -> Bool
@@ -146,9 +146,9 @@ TYPE SIGNATURES
   pred :: forall a. Enum a => a -> a
   print :: forall a. Show a => a -> IO ()
   product ::
-    forall (t :: * -> *) a. (Num a, P.Foldable t) => t a -> a
+    forall (t :: * -> *) a. (P.Foldable t, Num a) => t a -> a
   properFraction ::
-    forall a b. (Integral b, RealFrac a) => a -> (b, a)
+    forall a b. (RealFrac a, Integral b) => a -> (b, a)
   putChar :: Char -> IO ()
   putStr :: String -> IO ()
   putStrLn :: String -> IO ()
@@ -162,14 +162,14 @@ TYPE SIGNATURES
   readParen :: forall a. Bool -> ReadS a -> ReadS a
   reads :: forall a. Read a => ReadS a
   readsPrec :: forall a. Read a => Int -> ReadS a
-  realToFrac :: forall a b. (Fractional b, Real a) => a -> b
+  realToFrac :: forall a b. (Real a, Fractional b) => a -> b
   recip :: forall a. Fractional a => a -> a
   rem :: forall a. Integral a => a -> a -> a
   repeat :: forall a. a -> [a]
   replicate :: forall a. Int -> a -> [a]
   return :: forall (m :: * -> *) a. Monad m => a -> m a
   reverse :: forall a. [a] -> [a]
-  round :: forall a b. (Integral b, RealFrac a) => a -> b
+  round :: forall a b. (RealFrac a, Integral b) => a -> b
   scaleFloat :: forall a. RealFloat a => Int -> a -> a
   scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
   scanl1 :: forall a. (a -> a -> a) -> [a] -> [a]
@@ -178,11 +178,11 @@ TYPE SIGNATURES
   seq :: forall a b. a -> b -> b
   sequence ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (Monad m, P.Traversable t) =>
+    (P.Traversable t, Monad m) =>
     t (m a) -> m (t a)
   sequence_ ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (Monad m, P.Foldable t) =>
+    (P.Foldable t, Monad m) =>
     t (m a) -> m ()
   show :: forall a. Show a => a -> String
   showChar :: Char -> ShowS
@@ -201,7 +201,7 @@ TYPE SIGNATURES
   sqrt :: forall a. Floating a => a -> a
   subtract :: forall a. Num a => a -> a -> a
   succ :: forall a. Enum a => a -> a
-  sum :: forall (t :: * -> *) a. (Num a, P.Foldable t) => t a -> a
+  sum :: forall (t :: * -> *) a. (P.Foldable t, Num a) => t a -> a
   tail :: forall a. [a] -> [a]
   take :: forall a. Int -> [a] -> [a]
   takeWhile :: forall a. (a -> Bool) -> [a] -> [a]
@@ -210,7 +210,7 @@ TYPE SIGNATURES
   toEnum :: forall a. Enum a => Int -> a
   toInteger :: forall a. Integral a => a -> Integer
   toRational :: forall a. Real a => a -> Rational
-  truncate :: forall a b. (Integral b, RealFrac a) => a -> b
+  truncate :: forall a b. (RealFrac a, Integral b) => a -> b
   uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
   undefined :: forall w. w
   unlines :: [String] -> String
index 3846590..7049818 100644 (file)
@@ -1,10 +1,10 @@
 
 T12844.hs:12:9: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’
-        standing for ‘(Head rngs ~ '(r, r'), Foo rngs)’
-      Where: ‘r’, ‘r'’, ‘rngs’, ‘k’, ‘k1’
+        standing for ‘(Foo rngs, Head rngs ~ '(r, r'))’
+      Where: ‘rngs’, ‘r’, ‘k’, ‘r'’, ‘k1’
                are rigid type variables bound by
                the inferred type of
-                 bar :: (Head rngs ~ '(r, r'), Foo rngs) => FooData rngs
+                 bar :: (Foo rngs, Head rngs ~ '(r, r')) => FooData rngs
                at T12844.hs:13:1-9
     • In the type signature: bar :: _ => FooData rngs
index 87eef5c..dd46400 100644 (file)
@@ -1,17 +1,17 @@
 
 T13482.hs:8:32: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘(Monoid m, Eq m)’
+    • Found type wildcard ‘_’ standing for ‘(Eq m, Monoid m)’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of
-               minimal1_noksig :: (Monoid m, Eq m) => Int -> Bool
+                 minimal1_noksig :: (Eq m, Monoid m) => Int -> Bool
                at T13482.hs:9:1-50
     • In the type signature:
         minimal1_noksig :: forall m. _ => Int -> Bool
 
 T13482.hs:11:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘(Monoid m, Eq m)’
+    • Found type wildcard ‘_’ standing for ‘(Eq m, Monoid m)’
       Where: ‘m’ is a rigid type variable bound by
-               the inferred type of minimal1 :: (Monoid m, Eq m) => Bool
+               the inferred type of minimal1 :: (Eq m, Monoid m) => Bool
                at T13482.hs:12:1-41
     • In the type signature: minimal1 :: forall (m :: *). _ => Bool
 
index 71483f9..ebecbb9 100644 (file)
@@ -1,31 +1,31 @@
 
 T14217.hs:32:11: error:
     • Found type wildcard ‘_’
-        standing for ‘(Eq a63, Eq a62, Eq a61, Eq a60, Eq a59, Eq a58,
-                       Eq a57, Eq a56, Eq a55, Eq a54, Eq a53, Eq a52, Eq a51, Eq a50,
-                       Eq a49, Eq a48, Eq a47, Eq a46, Eq a45, Eq a44, Eq a43, Eq a42,
-                       Eq a41, Eq a40, Eq a39, Eq a38, Eq a37, Eq a36, Eq a35, Eq a34,
-                       Eq a33, Eq a32, Eq a31, Eq a30, Eq a29, Eq a28, Eq a27, Eq a26,
-                       Eq a25, Eq a24, Eq a23, Eq a22, Eq a21, Eq a20, Eq a19, Eq a18,
-                       Eq a17, Eq a16, Eq a15, Eq a14, Eq a13, Eq a12, Eq a11, Eq a10,
-                       Eq a9, Eq a8, Eq a7, Eq a6, Eq a5, Eq a4, Eq a3, Eq a2, Eq a1)’
-      Where: ‘a63’, ‘a62’, ‘a61’, ‘a60’, ‘a59’, ‘a58’, ‘a57’, ‘a56’,
-             ‘a55’, ‘a54’, ‘a53’, ‘a52’, ‘a51’, ‘a50’, ‘a49’, ‘a48’, ‘a47’,
-             ‘a46’, ‘a45’, ‘a44’, ‘a43’, ‘a42’, ‘a41’, ‘a40’, ‘a39’, ‘a38’,
-             ‘a37’, ‘a36’, ‘a35’, ‘a34’, ‘a33’, ‘a32’, ‘a31’, ‘a30’, ‘a29’,
-             ‘a28’, ‘a27’, ‘a26’, ‘a25’, ‘a24’, ‘a23’, ‘a22’, ‘a21’, ‘a20’,
-             ‘a19’, ‘a18’, ‘a17’, ‘a16’, ‘a15’, ‘a14’, ‘a13’, ‘a12’, ‘a11’,
-             ‘a10’, ‘a9’, ‘a8’, ‘a7’, ‘a6’, ‘a5’, ‘a4’, ‘a3’, ‘a2’, ‘a1
+        standing for ‘(Eq a1, Eq a2, Eq a3, Eq a4, Eq a5, Eq a6, Eq a7,
+                       Eq a8, Eq a9, Eq a10, Eq a11, Eq a12, Eq a13, Eq a14, Eq a15,
+                       Eq a16, Eq a17, Eq a18, Eq a19, Eq a20, Eq a21, Eq a22, Eq a23,
+                       Eq a24, Eq a25, Eq a26, Eq a27, Eq a28, Eq a29, Eq a30, Eq a31,
+                       Eq a32, Eq a33, Eq a34, Eq a35, Eq a36, Eq a37, Eq a38, Eq a39,
+                       Eq a40, Eq a41, Eq a42, Eq a43, Eq a44, Eq a45, Eq a46, Eq a47,
+                       Eq a48, Eq a49, Eq a50, Eq a51, Eq a52, Eq a53, Eq a54, Eq a55,
+                       Eq a56, Eq a57, Eq a58, Eq a59, Eq a60, Eq a61, Eq a62, Eq a63)’
+      Where: ‘a1’, ‘a2’, ‘a3’, ‘a4’, ‘a5’, ‘a6’, ‘a7’, ‘a8’, ‘a9’, ‘a10’,
+             ‘a11’, ‘a12’, ‘a13’, ‘a14’, ‘a15’, ‘a16’, ‘a17’, ‘a18’, ‘a19’,
+             ‘a20’, ‘a21’, ‘a22’, ‘a23’, ‘a24’, ‘a25’, ‘a26’, ‘a27’, ‘a28’,
+             ‘a29’, ‘a30’, ‘a31’, ‘a32’, ‘a33’, ‘a34’, ‘a35’, ‘a36’, ‘a37’,
+             ‘a38’, ‘a39’, ‘a40’, ‘a41’, ‘a42’, ‘a43’, ‘a44’, ‘a45’, ‘a46’,
+             ‘a47’, ‘a48’, ‘a49’, ‘a50’, ‘a51’, ‘a52’, ‘a53’, ‘a54’, ‘a55’,
+             ‘a56’, ‘a57’, ‘a58’, ‘a59’, ‘a60’, ‘a61’, ‘a62’, ‘a63
                are rigid type variables bound by
                the inferred type of
-                 eqFoo :: (Eq a63, Eq a62, Eq a61, Eq a60, Eq a59, Eq a58, Eq a57,
-                           Eq a56, Eq a55, Eq a54, Eq a53, Eq a52, Eq a51, Eq a50, Eq a49,
-                           Eq a48, Eq a47, Eq a46, Eq a45, Eq a44, Eq a43, Eq a42, Eq a41,
-                           Eq a40, Eq a39, Eq a38, Eq a37, Eq a36, Eq a35, Eq a34, Eq a33,
-                           Eq a32, Eq a31, Eq a30, Eq a29, Eq a28, Eq a27, Eq a26, Eq a25,
-                           Eq a24, Eq a23, Eq a22, Eq a21, Eq a20, Eq a19, Eq a18, Eq a17,
-                           Eq a16, Eq a15, Eq a14, Eq a13, Eq a12, Eq a11, Eq a10, Eq a9,
-                           Eq a8, Eq a7, Eq a6, Eq a5, Eq a4, Eq a3, Eq a2, Eq a1) =>
+                 eqFoo :: (Eq a1, Eq a2, Eq a3, Eq a4, Eq a5, Eq a6, Eq a7, Eq a8,
+                           Eq a9, Eq a10, Eq a11, Eq a12, Eq a13, Eq a14, Eq a15, Eq a16,
+                           Eq a17, Eq a18, Eq a19, Eq a20, Eq a21, Eq a22, Eq a23, Eq a24,
+                           Eq a25, Eq a26, Eq a27, Eq a28, Eq a29, Eq a30, Eq a31, Eq a32,
+                           Eq a33, Eq a34, Eq a35, Eq a36, Eq a37, Eq a38, Eq a39, Eq a40,
+                           Eq a41, Eq a42, Eq a43, Eq a44, Eq a45, Eq a46, Eq a47, Eq a48,
+                           Eq a49, Eq a50, Eq a51, Eq a52, Eq a53, Eq a54, Eq a55, Eq a56,
+                           Eq a57, Eq a58, Eq a59, Eq a60, Eq a61, Eq a62, Eq a63) =>
                           Foo
                             a1
                             a2
index a3df05c..ae8f15f 100644 (file)
@@ -16,24 +16,24 @@ T11213.hs:22:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:23:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
-      pattern Pur :: forall a. (Num a, Eq a) => a -> [a]
+      pattern Pur :: forall a. (Eq a, Num a) => a -> [a]
 
 T11213.hs:24:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
       pattern Purp :: forall a a1.
-                      (Num a, Eq a) =>
+                      (Eq a, Num a) =>
                       Show a1 => a -> a1 -> ([a], UnivProv a1)
 
 T11213.hs:25:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
       pattern Pure :: forall a.
-                      (Num a, Eq a) =>
+                      (Eq a, Num a) =>
                       forall a1. a -> a1 -> ([a], Ex)
 
 T11213.hs:26:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
       pattern Purep :: forall a.
-                       (Num a, Eq a) =>
+                       (Eq a, Num a) =>
                        forall a1. Show a1 => a -> a1 -> ([a], ExProv)
 
 T11213.hs:27:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
diff --git a/testsuite/tests/patsyn/should_compile/T14394.script b/testsuite/tests/patsyn/should_compile/T14394.script
new file mode 100644 (file)
index 0000000..208df0c
--- /dev/null
@@ -0,0 +1,24 @@
+:set -XPatternSynonyms -XGADTs -XViewPatterns -XScopedTypeVariables
+
+import Data.Type.Equality
+
+pattern Foo = HRefl
+
+:info Foo
+
+:set -XPolyKinds
+
+pattern Bar = HRefl
+-- Expecting no provided (* ~ *) constraint
+
+:info Bar
+
+-- This one generates two Ord a dictionaries
+-- but we only need one
+
+data S a where { MkS :: Ord a => a -> S a }
+
+pattern Bam x y <- (MkS (x::a), MkS (y::a))
+
+:info Bam
+-- Expecting only one provided Ord constraint
\ No newline at end of file
diff --git a/testsuite/tests/patsyn/should_compile/T14394.stdout b/testsuite/tests/patsyn/should_compile/T14394.stdout
new file mode 100644 (file)
index 0000000..0519ecb
--- /dev/null
@@ -0,0 +1 @@
\ No newline at end of file
index 8bc9dbd..19c9eaa 100644 (file)
@@ -74,3 +74,4 @@ test('T13768', normal, compile, [''])
 test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])],
                multimod_compile, ['T14058', '-v0'])
 test('T14326', normal, compile, [''])
+test('T14394', normal, ghci_script, ['T14394.script'])
index 342ee53..1dbbab5 100644 (file)
@@ -33,7 +33,8 @@ rebindable6.hs:111:17: error:
         g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
         test_do :: IO a -> IO (Maybe b) -> IO b
           (bound at rebindable6.hs:108:9)
-      Probable fix: use a type annotation to specify what ‘p0’, ‘t0’ should be.
+      Probable fix: use a type annotation to specify what ‘p0’,
+                                                          ‘t0’ should be.
       These potential instance exist:
         instance HasBind (IO a -> (a -> IO b) -> IO b)
           -- Defined at rebindable6.hs:51:18
index fc90899..a7780ef 100644 (file)
@@ -2,6 +2,10 @@ TOP=../../..
 include $(TOP)/mk/boilerplate.mk
 include $(TOP)/mk/test.mk
 
+T14434:
+       '$(TEST_HC)' $(TEST_HC_OPTS) -c T14434.hs -ddump-simpl | grep toStringX
+         # Expecting toStringX = toString, not discarding argument
+
 tc170:
        $(RM) Tc170_Aux.hi Tc170_Aux.o tc170.hi tc170.o
        '$(TEST_HC)' $(TEST_HC_OPTS) -c Tc170_Aux.hs
index fd3073d..9cca0e2 100644 (file)
@@ -4,7 +4,7 @@ holes2.hs:3:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
       prevents the constraint ‘(Show a0)’ from being solved.
       Probable fix: use a type annotation to specify what ‘a0’ should be.
       These potential instances exist:
-        instance (Show b, Show a) => Show (Either a b)
+        instance (Show a, Show b) => Show (Either a b)
           -- Defined in ‘Data.Either’
         instance Show Ordering -- Defined in ‘GHC.Show’
         instance Show Integer -- Defined in ‘GHC.Show’
index 6f49466..d5a547d 100644 (file)
@@ -4,5 +4,5 @@ T8883.hs:20:1: error:
       (Use FlexibleContexts to permit this)
     • When checking the inferred type
         fold :: forall a b.
-                (Regular a, Functor (PF a)) =>
+                (Functor (PF a), Regular a) =>
                 (PF a b -> b) -> a -> b
index 5ec1212..bf37f16 100644 (file)
@@ -9,7 +9,7 @@ tcfail133.hs:68:7: error:
       These potential instances exist:
         instance Show Ordering -- Defined in ‘GHC.Show’
         instance Show Integer -- Defined in ‘GHC.Show’
-        instance (Show b, Show a, Digit b, Number a) => Show (a :@ b)
+        instance (Number a, Digit b, Show a, Show b) => Show (a :@ b)
           -- Defined at tcfail133.hs:11:54
         ...plus 25 others
         ...plus six instances involving out-of-scope types