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

30 Apr 2019

      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

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

Travis Whitaker