Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds

[Travis Whitaker]

Sure, here it is.

https://gitlab.haskell.org/ghc/ghc/issues/16614

On Mon, Apr 29, 2019 at 11:46 PM Matthew Pickering <
matthewtpickering at 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 <pi.boy.travis at gmail.com>
> 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 at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190430/40131dfd/attachment.html>