Pattern synonyms don't work with GADTs
Consider this variant of test T8968-1
:
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
module ShouldCompile where
data X :: * -> * where
Y :: a -> X (Maybe a)
pattern C :: a -> X (Maybe a)
pattern C x = Y x
foo :: X t -> t
foo (C x) = Just x
- If we had
(Y x)
instead of(C x)
in the LHS offoo
, then this is an ordinary GADT program and typechecks fine. - If we omit the pattern signature, it typechecks fine, and
:info C
says
pattern C :: t ~ Maybe a => a -> X t -- Defined in ‘ShouldCompile’
- But as written, it fails with
Foo.hs:11:6:
Couldn't match type ‘t’ with ‘Maybe a0’
‘t’ is a rigid type variable bound by
the type signature for: foo :: X t -> t at Foo.hs:10:8
Expected type: X t
Actual type: X (Maybe a0)
Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)
In the pattern: C x
In an equation for ‘foo’: foo (C x) = Just x
Moreover,
:info C
says
pattern C :: a -> X (Maybe a) -- Defined at Foo.hs:8:9
Do you see the difference? In the former, the "prov_theta" equality constraint is explicit, but in the latter it's implicit.
The exact thing happens for DataCons
. It's handled via the dcEqSpec
field. Essentially PatSyn
should have a new field for the implicit equality constraints. And, just as for data consructors, we need to generate the equality constraints, and the existentials that are needed, when we process the signature. Use the code in TcTyClsDecls.rejigConRes
(perhaps needs a better name).
This is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.4 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |