Re: Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds
Sure, here it is.
https://gitlab.haskell.org/ghc/ghc/issues/16614
On Mon, Apr 29, 2019 at 11:46 PM Matthew Pickering <
matthewtpicker...@gmail.com> wrote:
> 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
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
