Re: Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds
Please can you open a bug report anyway? It is easier to discuss it there than on the mailing list. Matt On Tue, Apr 30, 2019 at 5:25 AM Travis Whitaker wrote: > > Hello GHC Devs, > > I've found a case in which annotating a bidirectional pattern synonym with a > type signature causes the typechecker to reject an otherwise typeable > program. Before filing a bug report I want to check that I'm thinking about > this correctly. Consider this module: > > {-# LANGUAGE TypeFamilies >, TypeFamilyDependencies >, DataKinds >, TypeOperators >, GADTs >, FlexibleContexts >, PatternSynonyms >#-} > > module Strange where > > data Expr a where > Tuple :: NTup ts -> Expr (Flatten ts) > > data NTup (ts :: [*]) where > Unit :: NTup '[] > Pair :: Expr a -> NTup ts -> NTup (a ': ts) > > type family Flatten ts = r | r -> ts where > Flatten '[] = () > Flatten '[a, b] = (a, b) > > pattern P a b = Pair a (Pair b Unit) > > fstExpr :: Expr (a, b) -> (Expr a, Expr b) > fstExpr (Tuple (P x y)) = (x, y) > > The idea is that an NTup '[a, b, c ...] should be isomorphic to an (a, b, c, > ...), but removes a lot of repetitive code for dealing with Exprs of tuples. > This module compiles with GHC 8.6.4 and GHC infers the expected type for P. > > P :: Expr a -> Expr a1 -> NTup '[a, a1] > > However, annotating P with this type causes typechecking fstExpr to fail with: > > Strange.hs:26:17: error: > • Could not deduce: ts ~ '[a, b] > from the context: (a, b) ~ Flatten ts > bound by a pattern with constructor: >Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts), > in an equation for ‘fstExpr’ > at Strange.hs:26:10-22 > ‘ts’ is a rigid type variable bound by > a pattern with constructor: > Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts), > in an equation for ‘fstExpr’ > at Strange.hs:26:10-22 > Expected type: NTup ts > Actual type: NTup '[a, b] > • In the pattern: P x y > In the pattern: Tuple (P x y) > In an equation for ‘fstExpr’: fstExpr (Tuple (P x y)) = (x, y) > • Relevant bindings include > fstExpr :: Expr (a, b) -> (Expr a, Expr b) > (bound at Strange.hs:26:1) >| > 26 | fstExpr (Tuple (P x y)) = (x, y) >| ^ > > It seems that providing a type signature causes GHC to forget the injectivity > of Flatten (i.e (a, b) ~ Flatten ts implies ts ~ '[a, b]). Is this a bug, > some limitation of pattern synonyms, or am I missing something? > > Thanks as always, > > Travis > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds
Hello GHC Devs, I've found a case in which annotating a bidirectional pattern synonym with a type signature causes the typechecker to reject an otherwise typeable program. Before filing a bug report I want to check that I'm thinking about this correctly. Consider this module: {-# LANGUAGE TypeFamilies , TypeFamilyDependencies , DataKinds , TypeOperators , GADTs , FlexibleContexts , PatternSynonyms #-} module Strange where data Expr a where Tuple :: NTup ts -> Expr (Flatten ts) data NTup (ts :: [*]) where Unit :: NTup '[] Pair :: Expr a -> NTup ts -> NTup (a ': ts) type family Flatten ts = r | r -> ts where Flatten '[] = () Flatten '[a, b] = (a, b) pattern P a b = Pair a (Pair b Unit) fstExpr :: Expr (a, b) -> (Expr a, Expr b) fstExpr (Tuple (P x y)) = (x, y) The idea is that an NTup '[a, b, c ...] should be isomorphic to an (a, b, c, ...), but removes a lot of repetitive code for dealing with Exprs of tuples. This module compiles with GHC 8.6.4 and GHC infers the expected type for P. P :: Expr a -> Expr a1 -> NTup '[a, a1] However, annotating P with this type causes typechecking fstExpr to fail with: Strange.hs:26:17: error: • Could not deduce: ts ~ '[a, b] from the context: (a, b) ~ Flatten ts bound by a pattern with constructor: Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts), in an equation for ‘fstExpr’ at Strange.hs:26:10-22 ‘ts’ is a rigid type variable bound by a pattern with constructor: Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts), in an equation for ‘fstExpr’ at Strange.hs:26:10-22 Expected type: NTup ts Actual type: NTup '[a, b] • In the pattern: P x y In the pattern: Tuple (P x y) In an equation for ‘fstExpr’: fstExpr (Tuple (P x y)) = (x, y) • Relevant bindings include fstExpr :: Expr (a, b) -> (Expr a, Expr b) (bound at Strange.hs:26:1) | 26 | fstExpr (Tuple (P x y)) = (x, y) | ^ It seems that providing a type signature causes GHC to forget the injectivity of Flatten (i.e (a, b) ~ Flatten ts implies ts ~ '[a, b]). Is this a bug, some limitation of pattern synonyms, or am I missing something? Thanks as always, Travis ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Why not short out IND_STATICs in the GC?
On Sat, 27 Apr 2019 at 07:44, Ömer Sinan Ağacan wrote: > Hi Simon, > > I'm wondering why in the GC we don't short out IND_STATICs like we do in > INDs > and BLACKHOLEs. Is there a reason for that? In this code in evacuate(): > > case IND_STATIC: > evacuate_static_object(IND_STATIC_LINK((StgClosure *)q), q); > return; > > Why not do something like > > case IND_STATIC: > q = ((StgIndStatic*)q)->indirectee; > *p = q; > goto loop; > > I actually tried it and it broke a lot of things, but I don't understand > why. > We basically turn this > > heap closure -> IND_STATIC -> heap closure > > into > > heap closure -> heap closure > > To me this should work, but for some reason it doesn't. Could you comment > on why > this doesn't work? > I think it might be to do with generational GC, although I'm not completely sure and it would be good to nail down the precise reasoning and document it. CAFs live in the old generation, and when we first enter a CAF we add it to the mutable list (remembered set). If we ignore the IND_STATIC, then the closure will never get re-added to the mutable list, even if it still points into the young generation. So the data will remain live for one GC, but not the next GC. When we do an old-generation GC we might find the CAF to be live (via the SRTs), but we've already GC'd the value it pointed to, so it's too late. Cheers Simon > > > Thanks, > > Ömer > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs