[commit: ghc] master: Do not mark CoVars as dead in the occur-anal (02b303e)

git at git.haskell.org git at git.haskell.org
Thu Oct 4 15:03:52 UTC 2018


Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/02b303eed0170983921877801e57f55d012db301/ghc

>---------------------------------------------------------------

commit 02b303eed0170983921877801e57f55d012db301
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Oct 3 15:41:43 2018 +0100

    Do not mark CoVars as dead in the occur-anal
    
    For years we have been marking CoVars as dead, becuase we
    don't gather occurrence info from types.  This is obviously
    wrong and caused Trac #15695.
    
    See Note [Do not mark CoVars as dead] in OccurAnal.


>---------------------------------------------------------------

02b303eed0170983921877801e57f55d012db301
 compiler/simplCore/OccurAnal.hs                  | 23 ++++++++++++
 testsuite/tests/patsyn/should_fail/T15695.hs     | 48 ++++++++++++++++++++++++
 testsuite/tests/patsyn/should_fail/T15695.stderr | 45 ++++++++++++++++++++++
 testsuite/tests/patsyn/should_fail/all.T         |  1 +
 4 files changed, 117 insertions(+)

diff --git a/compiler/simplCore/OccurAnal.hs b/compiler/simplCore/OccurAnal.hs
index 236bb81..2cc38a2 100644
--- a/compiler/simplCore/OccurAnal.hs
+++ b/compiler/simplCore/OccurAnal.hs
@@ -2501,6 +2501,10 @@ zapDetails = markAllMany . markAllNonTailCalled -- effectively sets to noOccInfo
 
 lookupDetails :: UsageDetails -> Id -> OccInfo
 lookupDetails ud id
+  | isCoVar id  -- We do not currenly gather occurrence info (from types)
+  = noOccInfo   -- for CoVars, so we must conservatively mark them as used
+                -- See Note [DoO not mark CoVars as dead]
+  | otherwise
   = case lookupVarEnv (ud_env ud) id of
       Just occ -> doZapping ud id occ
       Nothing  -> IAmDead
@@ -2512,6 +2516,25 @@ udFreeVars :: VarSet -> UsageDetails -> VarSet
 -- Find the subset of bndrs that are mentioned in uds
 udFreeVars bndrs ud = restrictUniqSetToUFM bndrs (ud_env ud)
 
+{- Note [Do not mark CoVars as dead]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's obviously wrong to mark CoVars as dead if they are used.
+Currently we don't traverse types to gather usase info for CoVars,
+so we had better treat them as having noOccInfo.
+
+This showed up in Trac #15696 we had something like
+  case eq_sel d of co -> ...(typeError @(...co...) "urk")...
+
+Then 'd' was substitued by a dictionary, so the expression
+simpified to
+  case (Coercion <blah>) of co -> ...(typeError @(...co...) "urk")...
+
+But then the "drop the case altogether" equation of rebuildCase
+thought that 'co' was dead, and discarded the entire case. Urk!
+
+I have no idea how we managed to avoid this pitfall for so long!
+-}
+
 -------------------
 -- Auxiliary functions for UsageDetails implementation
 
diff --git a/testsuite/tests/patsyn/should_fail/T15695.hs b/testsuite/tests/patsyn/should_fail/T15695.hs
new file mode 100644
index 0000000..de8035c
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15695.hs
@@ -0,0 +1,48 @@
+{-# Language RankNTypes, PatternSynonyms, DataKinds, PolyKinds, GADTs,
+             TypeOperators, MultiParamTypeClasses, TypeFamilies,
+             TypeSynonymInstances, FlexibleInstances, InstanceSigs, FlexibleContexts #-}
+
+{-# Options_GHC -fdefer-type-errors #-}
+
+module T15695 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data TyVar :: Type -> Type -> Type where
+ VO :: TyVar (a -> as) a
+ VS :: TyVar as a -> TyVar (b -> as) a
+
+data NP :: (k -> Type) -> ([k] -> Type) where
+ Nil :: NP f '[]
+ (:*) :: f a -> NP f as -> NP f (a:as)
+
+data NS :: (k -> Type) -> ([k] -> Type) where
+ Here  :: f a     -> NS f (a:as)
+ There :: NS f as -> NS f (a:as)
+
+infixr 6 :&:
+data Ctx :: Type -> Type where
+ E     :: Ctx(Type)
+ (:&:) :: a -> Ctx(as) -> Ctx(a -> as)
+
+data NA a
+
+type SOP(kind::Type) code = NS (NP NA) code
+
+data ApplyT(kind::Type) :: kind ->  Ctx(kind) -> Type where
+ AO :: a -> ApplyT(Type) a E
+ AS :: ApplyT(ks)      (f a) ctx
+    -> ApplyT(k -> ks) f     (a:&:ctx)
+
+from' :: ApplyT(Type -> Type -> Type) Either ctx -> NS (NP NA) '[ '[VO] ]
+from' (ASSO (Left  a)) = Here  (a :* Nil)
+from' (ASSO (Right b)) = There (Here undefined)
+
+pattern ASSO
+  :: () =>
+     forall (ks :: Type) k (f :: k -> ks) (a1 :: k) (ks1 :: Type) k1 (f1 :: k1 -> ks1) (a2 :: k1) a3.
+     (kind ~ (k -> k1 -> Type), a ~~ f, b ~~ (a1 :&: a2 :&: E),
+      f a1 ~~ f1, f1 a2 ~~ a3) =>
+     a3 -> ApplyT kind a b
+pattern ASSO a = AS (AS (AO a))
diff --git a/testsuite/tests/patsyn/should_fail/T15695.stderr b/testsuite/tests/patsyn/should_fail/T15695.stderr
new file mode 100644
index 0000000..6ef415a
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15695.stderr
@@ -0,0 +1,45 @@
+
+T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Could not deduce: a2 ~ NA 'VO
+      from the context: ((* -> * -> *) ~ (k1 -> k2 -> *), Either ~~ f,
+                         ctx ~~ (a2 ':&: (a3 ':&: 'E)), f a2 ~~ f1, f1 a3 ~~ a4)
+        bound by a pattern with pattern synonym:
+                   ASSO :: forall kind (a :: kind) (b :: Ctx kind).
+                           () =>
+                           forall ks k (f :: k -> ks) (a1 :: k) ks1 k1 (f1 :: k1 -> ks1)
+                                  (a2 :: k1) a3.
+                           (kind ~ (k -> k1 -> *), a ~~ f, b ~~ (a1 ':&: (a2 ':&: 'E)),
+                            f a1 ~~ f1, f1 a2 ~~ a3) =>
+                           a3 -> ApplyT kind a b,
+                 in an equation for ‘from'’
+        at T15695.hs:39:8-21
+      ‘a2’ is a rigid type variable bound by
+        a pattern with pattern synonym:
+          ASSO :: forall kind (a :: kind) (b :: Ctx kind).
+                  () =>
+                  forall ks k (f :: k -> ks) (a1 :: k) ks1 k1 (f1 :: k1 -> ks1)
+                         (a2 :: k1) a3.
+                  (kind ~ (k -> k1 -> *), a ~~ f, b ~~ (a1 ':&: (a2 ':&: 'E)),
+                   f a1 ~~ f1, f1 a2 ~~ a3) =>
+                  a3 -> ApplyT kind a b,
+        in an equation for ‘from'’
+        at T15695.hs:39:8-21
+      Expected type: a4
+        Actual type: Either (NA 'VO) a3
+    • In the pattern: Left a
+      In the pattern: ASSO (Left a)
+      In an equation for ‘from'’: from' (ASSO (Left a)) = Here (a :* Nil)
+    • Relevant bindings include
+        from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
+          (bound at T15695.hs:39:1)
+
+T15695.hs:40:26: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match type ‘a0 : as0’ with ‘'[]’
+      Expected type: NS (NP NA) '[ '[ 'VO]]
+        Actual type: NS (NP NA) ('[ 'VO] : a0 : as0)
+    • In the expression: There (Here undefined)
+      In an equation for ‘from'’:
+          from' (ASSO (Right b)) = There (Here undefined)
+    • Relevant bindings include
+        from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
+          (bound at T15695.hs:39:1)
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index c029f20..81e6644 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -34,6 +34,7 @@ test('T11667', normal, compile_fail, [''])
 test('T12165', normal, compile_fail, [''])
 test('T12819', normal, compile_fail, [''])
 test('UnliftedPSBind', normal, compile_fail, [''])
+test('T15695', normal, compile, [''])   # It has -fdefer-type-errors inside
 test('T13349', normal, compile_fail, [''])
 test('T13470', normal, compile_fail, [''])
 test('T14112', normal, compile_fail, [''])



More information about the ghc-commits mailing list