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

[Matthew Pickering]

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