Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds
Travis Whitaker
pi.boy.travis at gmail.com
Tue Apr 30 04:25:18 UTC 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:1022
‘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:1022
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
 next part 
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghcdevs/attachments/20190429/08b362fe/attachment.html>
More information about the ghcdevs
mailing list