<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Hello GHC Devs,</div><div><br></div><div>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:</div><div><br></div><div><div><font face="monospace, monospace">{-# LANGUAGE TypeFamilies</font></div><div><font face="monospace, monospace">           , TypeFamilyDependencies</font></div><div><font face="monospace, monospace">           , DataKinds</font></div><div><font face="monospace, monospace">           , TypeOperators</font></div><div><font face="monospace, monospace">           , GADTs</font></div><div><font face="monospace, monospace">           , FlexibleContexts</font></div><div><font face="monospace, monospace">           , PatternSynonyms</font></div><div><font face="monospace, monospace">           #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">module Strange where</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">data Expr a where</font></div><div><font face="monospace, monospace">    Tuple :: NTup ts -> Expr (Flatten ts)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">data NTup (ts :: [*]) where</font></div><div><font face="monospace, monospace">    Unit :: NTup '[]</font></div><div><font face="monospace, monospace">    Pair :: Expr a -> NTup ts -> NTup (a ': ts)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">type family Flatten ts = r | r -> ts where</font></div><div><font face="monospace, monospace">    Flatten '[] = ()</font></div><div><font face="monospace, monospace">    Flatten '[a, b] = (a, b)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">pattern P a b = Pair a (Pair b Unit)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">fstExpr :: Expr (a, b) -> (Expr a, Expr b)</font></div><div><font face="monospace, monospace">fstExpr (Tuple (P x y)) = (x, y)</font></div></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">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.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="monospace, monospace">P :: Expr a -> Expr a1 -> NTup '[a, a1]</font><br></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">However, annotating P with this type causes typechecking fstExpr to fail with:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><div style=""><font face="monospace, monospace">Strange.hs:26:17: error:</font></div><div style=""><font face="monospace, monospace">    • Could not deduce: ts ~ '[a, b]</font></div><div style=""><font face="monospace, monospace">      from the context: (a, b) ~ Flatten ts</font></div><div style=""><font face="monospace, monospace">        bound by a pattern with constructor:</font></div><div style=""><font face="monospace, monospace">                   Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts),</font></div><div style=""><font face="monospace, monospace">                 in an equation for ‘fstExpr’</font></div><div style=""><font face="monospace, monospace">        at Strange.hs:26:10-22</font></div><div style=""><font face="monospace, monospace">      ‘ts’ is a rigid type variable bound by</font></div><div style=""><font face="monospace, monospace">        a pattern with constructor:</font></div><div style=""><font face="monospace, monospace">          Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts),</font></div><div style=""><font face="monospace, monospace">        in an equation for ‘fstExpr’</font></div><div style=""><font face="monospace, monospace">        at Strange.hs:26:10-22</font></div><div style=""><font face="monospace, monospace">      Expected type: NTup ts</font></div><div style=""><font face="monospace, monospace">        Actual type: NTup '[a, b]</font></div><div style=""><font face="monospace, monospace">    • In the pattern: P x y</font></div><div style=""><font face="monospace, monospace">      In the pattern: Tuple (P x y)</font></div><div style=""><font face="monospace, monospace">      In an equation for ‘fstExpr’: fstExpr (Tuple (P x y)) = (x, y)</font></div><div style=""><font face="monospace, monospace">    • Relevant bindings include</font></div><div style=""><font face="monospace, monospace">        fstExpr :: Expr (a, b) -> (Expr a, Expr b)</font></div><div style=""><font face="monospace, monospace">          (bound at Strange.hs:26:1)</font></div><div style=""><font face="monospace, monospace">   |</font></div><div style=""><font face="monospace, monospace">26 | fstExpr (Tuple (P x y)) = (x, y)</font></div><div style=""><font face="monospace, monospace">   |               </font><font face="arial, helvetica, sans-serif">  ^^^^^</font></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div><div style=""><font face="arial, helvetica, sans-serif">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?</font></div><div style=""><font face="arial, helvetica, sans-serif"><br></font></div><div style=""><font face="arial, helvetica, sans-serif">Thanks as always,</font></div><div style=""><font face="arial, helvetica, sans-serif"><br></font></div><div style=""><font face="arial, helvetica, sans-serif">Travis</font></div></div></div></div></div></div></div></div>