<div dir="ltr">Sure, here it is.<div><br></div><div><a href="https://gitlab.haskell.org/ghc/ghc/issues/16614">https://gitlab.haskell.org/ghc/ghc/issues/16614</a><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Apr 29, 2019 at 11:46 PM Matthew Pickering <<a href="mailto:matthewtpickering@gmail.com">matthewtpickering@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Please can you open a bug report anyway? It is easier to discuss it<br>
there than on the mailing list.<br>
<br>
Matt<br>
<br>
On Tue, Apr 30, 2019 at 5:25 AM Travis Whitaker <<a href="mailto:pi.boy.travis@gmail.com" target="_blank">pi.boy.travis@gmail.com</a>> wrote:<br>
><br>
> Hello GHC Devs,<br>
><br>
> 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:<br>
><br>
> {-# LANGUAGE TypeFamilies<br>
>            , TypeFamilyDependencies<br>
>            , DataKinds<br>
>            , TypeOperators<br>
>            , GADTs<br>
>            , FlexibleContexts<br>
>            , PatternSynonyms<br>
>            #-}<br>
><br>
> module Strange where<br>
><br>
> data Expr a where<br>
>     Tuple :: NTup ts -> Expr (Flatten ts)<br>
><br>
> data NTup (ts :: [*]) where<br>
>     Unit :: NTup '[]<br>
>     Pair :: Expr a -> NTup ts -> NTup (a ': ts)<br>
><br>
> type family Flatten ts = r | r -> ts where<br>
>     Flatten '[] = ()<br>
>     Flatten '[a, b] = (a, b)<br>
><br>
> pattern P a b = Pair a (Pair b Unit)<br>
><br>
> fstExpr :: Expr (a, b) -> (Expr a, Expr b)<br>
> fstExpr (Tuple (P x y)) = (x, y)<br>
><br>
> 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.<br>
><br>
> P :: Expr a -> Expr a1 -> NTup '[a, a1]<br>
><br>
> However, annotating P with this type causes typechecking fstExpr to fail with:<br>
><br>
> Strange.hs:26:17: error:<br>
>     • Could not deduce: ts ~ '[a, b]<br>
>       from the context: (a, b) ~ Flatten ts<br>
>         bound by a pattern with constructor:<br>
>                    Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts),<br>
>                  in an equation for ‘fstExpr’<br>
>         at Strange.hs:26:10-22<br>
>       ‘ts’ is a rigid type variable bound by<br>
>         a pattern with constructor:<br>
>           Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts),<br>
>         in an equation for ‘fstExpr’<br>
>         at Strange.hs:26:10-22<br>
>       Expected type: NTup ts<br>
>         Actual type: NTup '[a, b]<br>
>     • In the pattern: P x y<br>
>       In the pattern: Tuple (P x y)<br>
>       In an equation for ‘fstExpr’: fstExpr (Tuple (P x y)) = (x, y)<br>
>     • Relevant bindings include<br>
>         fstExpr :: Expr (a, b) -> (Expr a, Expr b)<br>
>           (bound at Strange.hs:26:1)<br>
>    |<br>
> 26 | fstExpr (Tuple (P x y)) = (x, y)<br>
>    |                 ^^^^^<br>
><br>
> 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?<br>
><br>
> Thanks as always,<br>
><br>
> Travis<br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>