GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20190719T13:45:18Zhttps://gitlab.haskell.org/ghc/ghc/issues/16957COMPLETE sets don't get typechecked20190719T13:45:18ZSebastian GrafCOMPLETE sets don't get typecheckedGHC does a bad job at checking whether the `ConLike`s of a `COMPLETE` set can actually appear in the same pattern match. Example:
```
{# LANGUAGE PatternSynonyms #}
module Lib where
pattern A :: Maybe Bool
pattern A < _
pattern B :: Maybe ()
pattern B < _
{# COMPLETE A, B #}
```
This compiles just fine, whereas I had at least expected a warning. Strange enough the program gets rejected when you remove the `Maybe` type constructor, so it seems there is some machinery in place which is just not robust enough.
My understanding of a proper fix would try to find a unifying type of all return types. So, starting with `a`, we want to gradually refine it to `Maybe b`, then get to know that `b ~ Bool`, then `b ~ ()` and reject. This would still allow
```
{# LANGUAGE PatternSynonyms #}
module Lib where
pattern A :: Either Bool b
pattern A < _
pattern B :: Either a ()
pattern B < _
{# COMPLETE A, B #}
f :: Either Bool () > ()
f A = ()
f B = ()
```
by inferring the most general unifying type `Either Bool ()` for the `COMPLETE` pragma.GHC does a bad job at checking whether the `ConLike`s of a `COMPLETE` set can actually appear in the same pattern match. Example:
```
{# LANGUAGE PatternSynonyms #}
module Lib where
pattern A :: Maybe Bool
pattern A < _
pattern B :: Maybe ()
pattern B < _
{# COMPLETE A, B #}
```
This compiles just fine, whereas I had at least expected a warning. Strange enough the program gets rejected when you remove the `Maybe` type constructor, so it seems there is some machinery in place which is just not robust enough.
My understanding of a proper fix would try to find a unifying type of all return types. So, starting with `a`, we want to gradually refine it to `Maybe b`, then get to know that `b ~ Bool`, then `b ~ ()` and reject. This would still allow
```
{# LANGUAGE PatternSynonyms #}
module Lib where
pattern A :: Either Bool b
pattern A < _
pattern B :: Either a ()
pattern B < _
{# COMPLETE A, B #}
f :: Either Bool () > ()
f A = ()
f B = ()
```
by inferring the most general unifying type `Either Bool ()` for the `COMPLETE` pragma.https://gitlab.haskell.org/ghc/ghc/issues/16892Allow to specify full type for COMPLETE pragmas20190707T17:59:57ZOleg GrenrusAllow to specify full type for COMPLETE pragmas# Summary
I'd like to be able to write
```haskell
{# COMPLETE NSI0 :: NS Identity '[x0] #}
{# COMPLETE NSI0, NSI1 :: NS Identity '[x0, x1] #}
{# COMPLETE NSI0, NSI1, NSI2 :: NS Identity '[x0, x1, x2] #}
{# COMPLETE NSI0, NSI1, NSI2, NSI3 :: NS Identity '[x0, x1, x2, x3] #}
```
# Motivation
```haskell
{# LANGUAGE GADTs, DataKinds, TypeOperators, PatternSynonyms, EmptyCase #}
{# OPTIONS_GHC Wall #}
import Data.Functor.Identity (Identity (..))
data NS f xs where
Z :: f x > NS f (x ': xs)
S :: NS f xs > NS f (x ': xs)
 ugly
ex01 :: NS Identity '[Int, Char, Bool] > String
ex01 (Z (Identity i)) = show i
ex01 (S (Z (Identity c))) = show c
ex01 (S (S (Z (Identity b)))) = show b
ex01 (S (S (S x))) = case x of {}
 let's define patterns
pattern NSI0 :: x0 > NS Identity (x0 ': xs)
pattern NSI0 x = Z (Identity x)
pattern NSI1 :: x1 > NS Identity (x0 ': x1 ': xs)
pattern NSI1 x = S (Z (Identity x))
pattern NSI2 :: x2 > NS Identity (x0 ': x1 ': x2 ': xs)
pattern NSI2 x = S (S (Z (Identity x)))
 ex02 looks nice, but warns

 In an equation for ‘ex02’: Patterns not matched: _
ex02 :: NS Identity '[Int, Char, Bool] > String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b
 we can make warning go away with:
{# COMPLETE NSI0, NSI1, NSI2 #}
 but then ex03
 warns with: Patterns not matched: _
ex03 :: NS Identity '[Int, Char] > String
ex03 (NSI0 i) = show i
ex03 (NSI1 c) = show c
 and ex04 is accepted without a warning
ex04 :: NS Identity '[Int, Char, Bool, ()] > String
ex04 (NSI0 i) = show i
ex04 (NSI1 c) = show c
ex04 (NSI2 b) = show b
 note missing 4th clause

 I'd like to write {# COMPLETE NSI0, NSI1, NSI2 :: NS Identity '[x0, x1, x2] #}

 but that is not accepted
```
# Proposal
Based on a *Disambiguating between multiple COMPLETE pragmas* section, GHC already does "something" do pick from various matching lists.
I propose to add
 `COMPLETE` type annotation is at least as polymorphic as pattern scrutinee type,
## "at least as polymorphic as"
```
lhs ≼ rhs
```
`rhs` is at least as polymorphic as `lhs`. ≼ is reflexive.
```haskell
 see example 2
forall a. a > a ≼ Bool > Bool
 see example 1
NS Identity '[x0] ⊀ NS Identity '[]
NS Identity '[x0] ≼ NS Identity '[x0]
NS Identity '[x0] ⊀ NS Identity '[x0, x1]
NS Identity '[x0] ⊀ NS Identity xs
NS Identity '[x0] ⊀ NS Identity (x0 ': xs)
NS Identity '[x0] ⊀ NS Identity (x0 ': x1 ': xs)
 ^^^ COMPLETE ^^^ scrutinee type
 annotation
```
## Unambiguous
Currently documentation says
> The result type must also be unambiguous. Usually this can be inferred but when all the pattern synonyms in a group are polymorphic in the constructor the user must provide a type signature.
I think for my needs requring the type annotation to start with a concrete `TyCon` is ok.
I cannot think how
```haskell
{# COMPLETE Pat1, Pat2 :: f ... #}
```
could even make sense.
The downside is that we'll need to change
```diff
 {# COMPLETE T :: [] #}
+ {# COMPLETE T :: [a] #}
```
## Example 1
given there are
```haskell
{# COMPLETE NSI0 :: NS Identity '[x0] #}
{# COMPLETE NSI0, NSI1 :: NS Identity '[x0, x1] #}
{# COMPLETE NSI0, NSI1, NSI2 :: NS Identity '[x0, x1, x2] #}
{# COMPLETE NSI0, NSI1, NSI2, NSI3 :: NS Identity '[x0, x1, x2, x3] #}
```
pragmas, and we are considering
```haskell
ex02 :: NS Identity '[Int, Char, Bool] > String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b
```
then only 3rd pragma "match".
### Variation
There is (almost) a problematic case:
```haskell
ex03 :: NS Identity (Int ': Char ': Bool ': xs) > String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b
```
then the the scrutinee type is `NS Identity (Int ': Char ': Bool': xs)`,
and **none** of the specified above `COMPLETE` pragmas match/apply.
If one adds another pattern synonym, with new `COMPLETE` pragma:
```haskell
pattern Rest2 :: NS f xs > NS f (x0 ': x1 ': xs)
pattern Rest2 x = S (S x)
{# COMPLETE NSI0, NSI1, Rest2 :: NS Identity (x0 ': x1 ': xs) #}
```
In this case, all the above scenarios same warnings will be produced.
But if we write
```haskell
ex03 :: NS Identity (Int ': Char ': xs) > String
ex03 (NSI0 i) = show i
ex03 (NSI1 c) = show c
ex03 (Rest2 _) = "rest"
```
it will be accepted without warnings as well. Note:
```
NS Identity (x0 ': x1 ': xs) ≼ NS Identity '[Int, Char, Bool]
```
from `ex02`. But as there is a `COMPLETE` pragma set which doesn't
produce any warnings, none warnings are reported.
## Example 2
The below snipped fors already today
```haskell
pattern Endo :: (a > a) > (a > a)
pattern Endo f = f
{# COMPLETE Endo :: (>) #}
double :: (a > a) > (a > a)
double (Endo f) = Endo (f . f)
```
The pragma should be changed to
```
{# COMPLETE Endo :: a > a #}  as in pattern type decl.
```
if we however specify **only**
```
{# COMPLETE Endo :: Int > Int #}
```
then
```
Int > Int ⊀ forall a. a > a
```
and incomplete match warning would be printed.# Summary
I'd like to be able to write
```haskell
{# COMPLETE NSI0 :: NS Identity '[x0] #}
{# COMPLETE NSI0, NSI1 :: NS Identity '[x0, x1] #}
{# COMPLETE NSI0, NSI1, NSI2 :: NS Identity '[x0, x1, x2] #}
{# COMPLETE NSI0, NSI1, NSI2, NSI3 :: NS Identity '[x0, x1, x2, x3] #}
```
# Motivation
```haskell
{# LANGUAGE GADTs, DataKinds, TypeOperators, PatternSynonyms, EmptyCase #}
{# OPTIONS_GHC Wall #}
import Data.Functor.Identity (Identity (..))
data NS f xs where
Z :: f x > NS f (x ': xs)
S :: NS f xs > NS f (x ': xs)
 ugly
ex01 :: NS Identity '[Int, Char, Bool] > String
ex01 (Z (Identity i)) = show i
ex01 (S (Z (Identity c))) = show c
ex01 (S (S (Z (Identity b)))) = show b
ex01 (S (S (S x))) = case x of {}
 let's define patterns
pattern NSI0 :: x0 > NS Identity (x0 ': xs)
pattern NSI0 x = Z (Identity x)
pattern NSI1 :: x1 > NS Identity (x0 ': x1 ': xs)
pattern NSI1 x = S (Z (Identity x))
pattern NSI2 :: x2 > NS Identity (x0 ': x1 ': x2 ': xs)
pattern NSI2 x = S (S (Z (Identity x)))
 ex02 looks nice, but warns

 In an equation for ‘ex02’: Patterns not matched: _
ex02 :: NS Identity '[Int, Char, Bool] > String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b
 we can make warning go away with:
{# COMPLETE NSI0, NSI1, NSI2 #}
 but then ex03
 warns with: Patterns not matched: _
ex03 :: NS Identity '[Int, Char] > String
ex03 (NSI0 i) = show i
ex03 (NSI1 c) = show c
 and ex04 is accepted without a warning
ex04 :: NS Identity '[Int, Char, Bool, ()] > String
ex04 (NSI0 i) = show i
ex04 (NSI1 c) = show c
ex04 (NSI2 b) = show b
 note missing 4th clause

 I'd like to write {# COMPLETE NSI0, NSI1, NSI2 :: NS Identity '[x0, x1, x2] #}

 but that is not accepted
```
# Proposal
Based on a *Disambiguating between multiple COMPLETE pragmas* section, GHC already does "something" do pick from various matching lists.
I propose to add
 `COMPLETE` type annotation is at least as polymorphic as pattern scrutinee type,
## "at least as polymorphic as"
```
lhs ≼ rhs
```
`rhs` is at least as polymorphic as `lhs`. ≼ is reflexive.
```haskell
 see example 2
forall a. a > a ≼ Bool > Bool
 see example 1
NS Identity '[x0] ⊀ NS Identity '[]
NS Identity '[x0] ≼ NS Identity '[x0]
NS Identity '[x0] ⊀ NS Identity '[x0, x1]
NS Identity '[x0] ⊀ NS Identity xs
NS Identity '[x0] ⊀ NS Identity (x0 ': xs)
NS Identity '[x0] ⊀ NS Identity (x0 ': x1 ': xs)
 ^^^ COMPLETE ^^^ scrutinee type
 annotation
```
## Unambiguous
Currently documentation says
> The result type must also be unambiguous. Usually this can be inferred but when all the pattern synonyms in a group are polymorphic in the constructor the user must provide a type signature.
I think for my needs requring the type annotation to start with a concrete `TyCon` is ok.
I cannot think how
```haskell
{# COMPLETE Pat1, Pat2 :: f ... #}
```
could even make sense.
The downside is that we'll need to change
```diff
 {# COMPLETE T :: [] #}
+ {# COMPLETE T :: [a] #}
```
## Example 1
given there are
```haskell
{# COMPLETE NSI0 :: NS Identity '[x0] #}
{# COMPLETE NSI0, NSI1 :: NS Identity '[x0, x1] #}
{# COMPLETE NSI0, NSI1, NSI2 :: NS Identity '[x0, x1, x2] #}
{# COMPLETE NSI0, NSI1, NSI2, NSI3 :: NS Identity '[x0, x1, x2, x3] #}
```
pragmas, and we are considering
```haskell
ex02 :: NS Identity '[Int, Char, Bool] > String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b
```
then only 3rd pragma "match".
### Variation
There is (almost) a problematic case:
```haskell
ex03 :: NS Identity (Int ': Char ': Bool ': xs) > String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b
```
then the the scrutinee type is `NS Identity (Int ': Char ': Bool': xs)`,
and **none** of the specified above `COMPLETE` pragmas match/apply.
If one adds another pattern synonym, with new `COMPLETE` pragma:
```haskell
pattern Rest2 :: NS f xs > NS f (x0 ': x1 ': xs)
pattern Rest2 x = S (S x)
{# COMPLETE NSI0, NSI1, Rest2 :: NS Identity (x0 ': x1 ': xs) #}
```
In this case, all the above scenarios same warnings will be produced.
But if we write
```haskell
ex03 :: NS Identity (Int ': Char ': xs) > String
ex03 (NSI0 i) = show i
ex03 (NSI1 c) = show c
ex03 (Rest2 _) = "rest"
```
it will be accepted without warnings as well. Note:
```
NS Identity (x0 ': x1 ': xs) ≼ NS Identity '[Int, Char, Bool]
```
from `ex02`. But as there is a `COMPLETE` pragma set which doesn't
produce any warnings, none warnings are reported.
## Example 2
The below snipped fors already today
```haskell
pattern Endo :: (a > a) > (a > a)
pattern Endo f = f
{# COMPLETE Endo :: (>) #}
double :: (a > a) > (a > a)
double (Endo f) = Endo (f . f)
```
The pragma should be changed to
```
{# COMPLETE Endo :: a > a #}  as in pattern type decl.
```
if we however specify **only**
```
{# COMPLETE Endo :: Int > Int #}
```
then
```
Int > Int ⊀ forall a. a > a
```
and incomplete match warning would be printed.⊥https://gitlab.haskell.org/ghc/ghc/issues/16595GHC is overly lax when typechecking bundled pattern synonyms20190420T18:42:12ZJoe HermaszewskiGHC is overly lax when typechecking bundled pattern synonyms# Summary
When a pattern synonym is bundled with a type, the type of the pattern synonym is required to match. This can be circumvented by giving the pattern a type annotation in which the head is polymorphic, but the context constrains it to be a type other than what it is being bundled with.
I'm afraid to say that code taking advantage of this bug does already exist, I'm currently using it as a means to allow importing several pattern synonyms at once as a workaround for https://github.com/ghcproposals/ghcproposals/pull/28
The users guide states
> Bundled pattern synonyms are type checked to ensure that they are of the same type as the type constructor which they are bundled with. A pattern synonym P can not be bundled with a type constructor T if P‘s type is visibly incompatible with T.
The users guide also mentions that the types in the example below are distinct for pattern synonyms. https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#typingofpatternsynonyms
# Steps to reproduce
 Compile this module
```haskell
{# LANGUAGE TypeFamilies #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE EmptyDataDecls #}
module A
( Foo
, FooPatterns(One)  No error is generated here
) where
newtype Foo = Foo Int
  An empty data declaration used to export the "One" pattern
data FooPatterns
 The commented signature causes GHC to fail with `Couldn't match expected
 type of ‘FooPatterns’ with actual type of ‘Foo’` when exporting this pattern
 bundled with `FooPatterns above`.
 pattern One :: Foo
pattern One :: (a ~ Foo) => a
pattern One = Foo 1
```
 Observe that no error is generated.
 Remove the type annotation for `pattern One`
 Observe that GHC reports the following error:
```
A.hs:7:520: error:
• Pattern synonyms can only be bundled with matching type constructors
Couldn't match expected type of ‘FooPatterns’ with actual type of ‘Foo’
• In the pattern synonym: One
In the export: FooPatterns(One)

7  , FooPatterns(One)
 ^^^^^^^^^^^^^^^^
```
# Expected behavior
GHC reports the error in both cases
# Environment
This behavior is present in GHC versions 8.7.20190115, 8.6.4, 8.4.4 and 8.2.2 at least.# Summary
When a pattern synonym is bundled with a type, the type of the pattern synonym is required to match. This can be circumvented by giving the pattern a type annotation in which the head is polymorphic, but the context constrains it to be a type other than what it is being bundled with.
I'm afraid to say that code taking advantage of this bug does already exist, I'm currently using it as a means to allow importing several pattern synonyms at once as a workaround for https://github.com/ghcproposals/ghcproposals/pull/28
The users guide states
> Bundled pattern synonyms are type checked to ensure that they are of the same type as the type constructor which they are bundled with. A pattern synonym P can not be bundled with a type constructor T if P‘s type is visibly incompatible with T.
The users guide also mentions that the types in the example below are distinct for pattern synonyms. https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#typingofpatternsynonyms
# Steps to reproduce
 Compile this module
```haskell
{# LANGUAGE TypeFamilies #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE EmptyDataDecls #}
module A
( Foo
, FooPatterns(One)  No error is generated here
) where
newtype Foo = Foo Int
  An empty data declaration used to export the "One" pattern
data FooPatterns
 The commented signature causes GHC to fail with `Couldn't match expected
 type of ‘FooPatterns’ with actual type of ‘Foo’` when exporting this pattern
 bundled with `FooPatterns above`.
 pattern One :: Foo
pattern One :: (a ~ Foo) => a
pattern One = Foo 1
```
 Observe that no error is generated.
 Remove the type annotation for `pattern One`
 Observe that GHC reports the following error:
```
A.hs:7:520: error:
• Pattern synonyms can only be bundled with matching type constructors
Couldn't match expected type of ‘FooPatterns’ with actual type of ‘Foo’
• In the pattern synonym: One
In the export: FooPatterns(One)

7  , FooPatterns(One)
 ^^^^^^^^^^^^^^^^
```
# Expected behavior
GHC reports the error in both cases
# Environment
This behavior is present in GHC versions 8.7.20190115, 8.6.4, 8.4.4 and 8.2.2 at least.https://gitlab.haskell.org/ghc/ghc/issues/16155Pattern Synonym for Ratio20190707T18:01:16ZZemylaPattern Synonym for Ratio`Data.Ratio` should export a simple pattern synonym that can be used by `Safe` code.
```hs
infixl 7 :%:
pattern n :%: d < n :% d where
n :%: d = n % d
```
It'd be much simpler to use than `numerator` and `denominator`, and pattern matching on it would turn into a regular pattern match, hopefully for free.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Core Libraries 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Pattern Synonym for Ratio","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["PatternSynonyms,","Ratio"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"`Data.Ratio` should export a simple pattern synonym that can be used by `Safe` code.\r\n\r\n{{{#!hs\r\ninfixl 7 :%:\r\n\r\npattern n :%: d < n :% d where\r\n n :%: d = n % d\r\n}}}\r\n\r\nIt'd be much simpler to use than `numerator` and `denominator`, and pattern matching on it would turn into a regular pattern match, hopefully for free.","type_of_failure":"OtherFailure","blocking":[]} >`Data.Ratio` should export a simple pattern synonym that can be used by `Safe` code.
```hs
infixl 7 :%:
pattern n :%: d < n :% d where
n :%: d = n % d
```
It'd be much simpler to use than `numerator` and `denominator`, and pattern matching on it would turn into a regular pattern match, hopefully for free.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Core Libraries 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Pattern Synonym for Ratio","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["PatternSynonyms,","Ratio"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"`Data.Ratio` should export a simple pattern synonym that can be used by `Safe` code.\r\n\r\n{{{#!hs\r\ninfixl 7 :%:\r\n\r\npattern n :%: d < n :% d where\r\n n :%: d = n % d\r\n}}}\r\n\r\nIt'd be much simpler to use than `numerator` and `denominator`, and pattern matching on it would turn into a regular pattern match, hopefully for free.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/15693Abstracting out pattern into a pattern synonym fails with scary error20190707T18:03:25ZIcelandjackAbstracting out pattern into a pattern synonym fails with scary errorThis **works**
```hs
{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}
import Data.Kind
data Ctx :: Type > Type where
E :: Ctx(Type)
(:&:) :: a > Ctx(as) > Ctx(a > as)
data ApplyT(kind::Type) :: kind > Ctx(kind) > Type where
AO :: a > ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
> ApplyT(k > ks) f (a:&:ctx)
foo :: ApplyT(Type > Type > Type) Either a > ()
foo (ASSO (Left a)) = ()
pattern ASSO a = AS (AS (AO a))
```
but then you might think, let's give a name (pattern synonym) to `ASSO (Left a)`
This **fails**
```hs
{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}
import Data.Kind
data Ctx :: Type > Type where
E :: Ctx(Type)
(:&:) :: a > Ctx(as) > Ctx(a > as)
data ApplyT(kind::Type) :: kind > Ctx(kind) > Type where
AO :: a > ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
> ApplyT(k > ks) f (a:&:ctx)
pattern ASSO a = AS (AS (AO a))
pattern ASSOLeft a = ASSO (Left a)
```
```
$ ghci ignoredotghci 464.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/464.hs, interpreted )
hs/464.hs:16:22: error:
• Couldn't match type ‘k1’ with ‘*’
‘k1’ is a rigid type variable bound by
the signature for pattern synonym ‘ASSOLeft’
at hs/464.hs:16:134
Expected type: ApplyT kind a b
Actual type: ApplyT (* > * > *) Either (a1 ':&: (a20 ':&: 'E))
• In the expression: ASSO (Left a)
In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a)

16  pattern ASSOLeft a = ASSO (Left a)
 ^^^^^^^^^^^^^
hs/464.hs:16:28: error:
• Could not deduce: k1 ~ *
from the context: (kind ~ (k > ks), a ~~ f, b ~~ (a2 ':&: ctx),
ks ~ (k1 > ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *,
f1 a3 ~~ a4, ctx1 ~~ 'E)
bound by a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 > ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:2234
‘k1’ is a rigid type variable bound by
a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 > ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:2234
When matching types
a3 :: k1
b0 :: *
Expected type: a4
Actual type: Either a1 b0
• In the pattern: Left a
In the pattern: ASSO (Left a)
In the declaration for pattern synonym ‘ASSOLeft’

16  pattern ASSOLeft a = ASSO (Left a)
 ^^^^^^
Failed, no modules loaded.
Prelude>
```

Can I, as a user, assume that any valid pattern `foo (ASSO (Left a)) = ...` can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Abstracting out pattern into a pattern synonym fails with scary error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This '''works'''\r\n\r\n{{{#!hs\r\n{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}\r\n\r\nimport Data.Kind\r\n\r\ndata Ctx :: Type > Type where\r\n E :: Ctx(Type)\r\n (:&:) :: a > Ctx(as) > Ctx(a > as)\r\n\r\ndata ApplyT(kind::Type) :: kind > Ctx(kind) > Type where\r\n AO :: a > ApplyT(Type) a E\r\n AS :: ApplyT(ks) (f a) ctx\r\n > ApplyT(k > ks) f (a:&:ctx)\r\n\r\nfoo :: ApplyT(Type > Type > Type) Either a > ()\r\nfoo (ASSO (Left a)) = ()\r\n\r\npattern ASSO a = AS (AS (AO a))\r\n}}}\r\n\r\nbut then you might think, let's give a name (pattern synonym) to `ASSO (Left a)`\r\n\r\nThis '''fails'''\r\n{{{#!hs\r\n{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}\r\n\r\nimport Data.Kind\r\n\r\ndata Ctx :: Type > Type where\r\n E :: Ctx(Type)\r\n (:&:) :: a > Ctx(as) > Ctx(a > as)\r\n\r\ndata ApplyT(kind::Type) :: kind > Ctx(kind) > Type where\r\n AO :: a > ApplyT(Type) a E\r\n AS :: ApplyT(ks) (f a) ctx\r\n > ApplyT(k > ks) f (a:&:ctx)\r\n\r\npattern ASSO a = AS (AS (AO a))\r\n\r\npattern ASSOLeft a = ASSO (Left a)\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci 464.hs\r\nGHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/464.hs, interpreted )\r\n\r\nhs/464.hs:16:22: error:\r\n • Couldn't match type ‘k1’ with ‘*’\r\n ‘k1’ is a rigid type variable bound by\r\n the signature for pattern synonym ‘ASSOLeft’\r\n at hs/464.hs:16:134\r\n Expected type: ApplyT kind a b\r\n Actual type: ApplyT (* > * > *) Either (a1 ':&: (a20 ':&: 'E))\r\n • In the expression: ASSO (Left a)\r\n In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a)\r\n \r\n16  pattern ASSOLeft a = ASSO (Left a)\r\n  ^^^^^^^^^^^^^\r\n\r\nhs/464.hs:16:28: error:\r\n • Could not deduce: k1 ~ *\r\n from the context: (kind ~ (k > ks), a ~~ f, b ~~ (a2 ':&: ctx),\r\n ks ~ (k1 > ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *,\r\n f1 a3 ~~ a4, ctx1 ~~ 'E)\r\n bound by a pattern with pattern synonym:\r\n ASSO :: forall kind (a :: kind) (b :: Ctx kind).\r\n () =>\r\n forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx\r\n ks) ks1 k1 (f1 :: k1\r\n > ks1) (a2 :: k1) (ctx1 :: Ctx\r\n ks1) a3.\r\n (kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),\r\n f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,\r\n ctx1 ~~ 'E) =>\r\n a3 > ApplyT kind a b,\r\n in a pattern synonym declaration\r\n at hs/464.hs:16:2234\r\n ‘k1’ is a rigid type variable bound by\r\n a pattern with pattern synonym:\r\n ASSO :: forall kind (a :: kind) (b :: Ctx kind).\r\n () =>\r\n forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx\r\n ks) ks1 k1 (f1 :: k1\r\n > ks1) (a2 :: k1) (ctx1 :: Ctx\r\n ks1) a3.\r\n (kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),\r\n f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,\r\n ctx1 ~~ 'E) =>\r\n a3 > ApplyT kind a b,\r\n in a pattern synonym declaration\r\n at hs/464.hs:16:2234\r\n When matching types\r\n a3 :: k1\r\n b0 :: *\r\n Expected type: a4\r\n Actual type: Either a1 b0\r\n • In the pattern: Left a\r\n In the pattern: ASSO (Left a)\r\n In the declaration for pattern synonym ‘ASSOLeft’\r\n \r\n16  pattern ASSOLeft a = ASSO (Left a)\r\n  ^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\n\r\n\r\nCan I, as a user, assume that any valid pattern `foo (ASSO (Left a)) = ...` can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect","type_of_failure":"OtherFailure","blocking":[]} >This **works**
```hs
{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}
import Data.Kind
data Ctx :: Type > Type where
E :: Ctx(Type)
(:&:) :: a > Ctx(as) > Ctx(a > as)
data ApplyT(kind::Type) :: kind > Ctx(kind) > Type where
AO :: a > ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
> ApplyT(k > ks) f (a:&:ctx)
foo :: ApplyT(Type > Type > Type) Either a > ()
foo (ASSO (Left a)) = ()
pattern ASSO a = AS (AS (AO a))
```
but then you might think, let's give a name (pattern synonym) to `ASSO (Left a)`
This **fails**
```hs
{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}
import Data.Kind
data Ctx :: Type > Type where
E :: Ctx(Type)
(:&:) :: a > Ctx(as) > Ctx(a > as)
data ApplyT(kind::Type) :: kind > Ctx(kind) > Type where
AO :: a > ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
> ApplyT(k > ks) f (a:&:ctx)
pattern ASSO a = AS (AS (AO a))
pattern ASSOLeft a = ASSO (Left a)
```
```
$ ghci ignoredotghci 464.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/464.hs, interpreted )
hs/464.hs:16:22: error:
• Couldn't match type ‘k1’ with ‘*’
‘k1’ is a rigid type variable bound by
the signature for pattern synonym ‘ASSOLeft’
at hs/464.hs:16:134
Expected type: ApplyT kind a b
Actual type: ApplyT (* > * > *) Either (a1 ':&: (a20 ':&: 'E))
• In the expression: ASSO (Left a)
In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a)

16  pattern ASSOLeft a = ASSO (Left a)
 ^^^^^^^^^^^^^
hs/464.hs:16:28: error:
• Could not deduce: k1 ~ *
from the context: (kind ~ (k > ks), a ~~ f, b ~~ (a2 ':&: ctx),
ks ~ (k1 > ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *,
f1 a3 ~~ a4, ctx1 ~~ 'E)
bound by a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 > ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:2234
‘k1’ is a rigid type variable bound by
a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 > ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:2234
When matching types
a3 :: k1
b0 :: *
Expected type: a4
Actual type: Either a1 b0
• In the pattern: Left a
In the pattern: ASSO (Left a)
In the declaration for pattern synonym ‘ASSOLeft’

16  pattern ASSOLeft a = ASSO (Left a)
 ^^^^^^
Failed, no modules loaded.
Prelude>
```

Can I, as a user, assume that any valid pattern `foo (ASSO (Left a)) = ...` can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Abstracting out pattern into a pattern synonym fails with scary error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This '''works'''\r\n\r\n{{{#!hs\r\n{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}\r\n\r\nimport Data.Kind\r\n\r\ndata Ctx :: Type > Type where\r\n E :: Ctx(Type)\r\n (:&:) :: a > Ctx(as) > Ctx(a > as)\r\n\r\ndata ApplyT(kind::Type) :: kind > Ctx(kind) > Type where\r\n AO :: a > ApplyT(Type) a E\r\n AS :: ApplyT(ks) (f a) ctx\r\n > ApplyT(k > ks) f (a:&:ctx)\r\n\r\nfoo :: ApplyT(Type > Type > Type) Either a > ()\r\nfoo (ASSO (Left a)) = ()\r\n\r\npattern ASSO a = AS (AS (AO a))\r\n}}}\r\n\r\nbut then you might think, let's give a name (pattern synonym) to `ASSO (Left a)`\r\n\r\nThis '''fails'''\r\n{{{#!hs\r\n{# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #}\r\n\r\nimport Data.Kind\r\n\r\ndata Ctx :: Type > Type where\r\n E :: Ctx(Type)\r\n (:&:) :: a > Ctx(as) > Ctx(a > as)\r\n\r\ndata ApplyT(kind::Type) :: kind > Ctx(kind) > Type where\r\n AO :: a > ApplyT(Type) a E\r\n AS :: ApplyT(ks) (f a) ctx\r\n > ApplyT(k > ks) f (a:&:ctx)\r\n\r\npattern ASSO a = AS (AS (AO a))\r\n\r\npattern ASSOLeft a = ASSO (Left a)\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci 464.hs\r\nGHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/464.hs, interpreted )\r\n\r\nhs/464.hs:16:22: error:\r\n • Couldn't match type ‘k1’ with ‘*’\r\n ‘k1’ is a rigid type variable bound by\r\n the signature for pattern synonym ‘ASSOLeft’\r\n at hs/464.hs:16:134\r\n Expected type: ApplyT kind a b\r\n Actual type: ApplyT (* > * > *) Either (a1 ':&: (a20 ':&: 'E))\r\n • In the expression: ASSO (Left a)\r\n In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a)\r\n \r\n16  pattern ASSOLeft a = ASSO (Left a)\r\n  ^^^^^^^^^^^^^\r\n\r\nhs/464.hs:16:28: error:\r\n • Could not deduce: k1 ~ *\r\n from the context: (kind ~ (k > ks), a ~~ f, b ~~ (a2 ':&: ctx),\r\n ks ~ (k1 > ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *,\r\n f1 a3 ~~ a4, ctx1 ~~ 'E)\r\n bound by a pattern with pattern synonym:\r\n ASSO :: forall kind (a :: kind) (b :: Ctx kind).\r\n () =>\r\n forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx\r\n ks) ks1 k1 (f1 :: k1\r\n > ks1) (a2 :: k1) (ctx1 :: Ctx\r\n ks1) a3.\r\n (kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),\r\n f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,\r\n ctx1 ~~ 'E) =>\r\n a3 > ApplyT kind a b,\r\n in a pattern synonym declaration\r\n at hs/464.hs:16:2234\r\n ‘k1’ is a rigid type variable bound by\r\n a pattern with pattern synonym:\r\n ASSO :: forall kind (a :: kind) (b :: Ctx kind).\r\n () =>\r\n forall ks k (f :: k > ks) (a1 :: k) (ctx :: Ctx\r\n ks) ks1 k1 (f1 :: k1\r\n > ks1) (a2 :: k1) (ctx1 :: Ctx\r\n ks1) a3.\r\n (kind ~ (k > ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 > ks1),\r\n f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,\r\n ctx1 ~~ 'E) =>\r\n a3 > ApplyT kind a b,\r\n in a pattern synonym declaration\r\n at hs/464.hs:16:2234\r\n When matching types\r\n a3 :: k1\r\n b0 :: *\r\n Expected type: a4\r\n Actual type: Either a1 b0\r\n • In the pattern: Left a\r\n In the pattern: ASSO (Left a)\r\n In the declaration for pattern synonym ‘ASSOLeft’\r\n \r\n16  pattern ASSOLeft a = ASSO (Left a)\r\n  ^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\n\r\n\r\nCan I, as a user, assume that any valid pattern `foo (ASSO (Left a)) = ...` can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc/issues/15416Higher rank types in pattern synonyms20190707T18:05:00ZmniipHigher rank types in pattern synonyms```hs
{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}
```
Consider the following two pattern synonyms:
```hs
pattern N :: () => () => forall r. r > (a > r) > r
pattern N < ((\f > f Nothing Just) > Nothing) where N = \n j > n
pattern J :: a > forall r. r > (a > r) > r
pattern J x < ((\f > f Nothing Just) > Just x) where J x = \n j > j x
```
The pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.
Now consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:
```hs
fooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
fooVPEqns ((\f > f Nothing Just) > Nothing) = Nothing
fooVPEqns ((\f > f Nothing Just) > Just x) = Just x
fooVPCase v = case v of
((\f > f Nothing Just) > Nothing) > Nothing
((\f > f Nothing Just) > Just x) > Just x
fooPSEqns N = Nothing
fooPSEqns (J x) = Just x
fooPSCase v = case v of
N > Nothing
J x > Just x
```
Three of these compile and work fine, the fourth breaks:
```hs
QuantPatSyn.hs:22:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a0 > r) > r’
• In the pattern: N
In a case alternative: N > Nothing
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

22  N > Nothing
 ^
QuantPatSyn.hs:23:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a > r) > r’
• In the pattern: J x
In a case alternative: J x > Just x
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

23  J x > Just x
 ^^^
```
The exact wording of the error message (the appearance of `forall` in the "actual type") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.
Another symptom can be observed with the following:
```hs
pattern V :: Void > (forall r. r)
pattern V x < ((\f > f) > x) where V x = absurd x
barVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void
barVPEqns ((\f > f) > x) = x
barVPCase v = case v of
((\f > f) > x) > x
barPSEqns (V x) = x
barPSCase v = case v of
V x > x
```
```hs
QuantPatSyn.hs:43:9: error:
• Cannot instantiate unification variable ‘r0’
with a type involving foralls: forall r. r
GHC doesn't yet support impredicative polymorphism
• In the pattern: V x
In a case alternative: V x > x
In the expression: case v of { V x > x }

43  V x > x
 ^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Higher rank types in pattern synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}\r\n}}}\r\nConsider the following two pattern synonyms:\r\n\r\n{{{#!hs\r\npattern N :: () => () => forall r. r > (a > r) > r\r\npattern N < ((\\f > f Nothing Just) > Nothing) where N = \\n j > n\r\n\r\npattern J :: a > forall r. r > (a > r) > r\r\npattern J x < ((\\f > f Nothing Just) > Just x) where J x = \\n j > j x\r\n}}}\r\n\r\nThe pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.\r\n\r\nNow consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:\r\n\r\n{{{#!hs\r\nfooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n\r\nfooVPEqns ((\\f > f Nothing Just) > Nothing) = Nothing\r\nfooVPEqns ((\\f > f Nothing Just) > Just x) = Just x\r\n\r\nfooVPCase v = case v of\r\n\t((\\f > f Nothing Just) > Nothing) > Nothing\r\n\t((\\f > f Nothing Just) > Just x) > Just x\r\n\r\nfooPSEqns N = Nothing\r\nfooPSEqns (J x) = Just x\r\n\r\nfooPSCase v = case v of\r\n\tN > Nothing\r\n\tJ x > Just x\r\n}}}\r\n\r\nThree of these compile and work fine, the fourth breaks:\r\n{{{#!hs\r\nQuantPatSyn.hs:22:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a0 > r) > r’\r\n • In the pattern: N\r\n In a case alternative: N > Nothing\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n22  N > Nothing\r\n  ^\r\n\r\nQuantPatSyn.hs:23:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a > r) > r’\r\n • In the pattern: J x\r\n In a case alternative: J x > Just x\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n23  J x > Just x\r\n  ^^^\r\n}}}\r\n\r\nThe exact wording of the error message (the appearance of `forall` in the \"actual type\") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.\r\n\r\nAnother symptom can be observed with the following:\r\n\r\n{{{#!hs\r\npattern V :: Void > (forall r. r)\r\npattern V x < ((\\f > f) > x) where V x = absurd x\r\n\r\nbarVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void\r\n\r\nbarVPEqns ((\\f > f) > x) = x\r\n\r\nbarVPCase v = case v of\r\n\t((\\f > f) > x) > x\r\n\r\nbarPSEqns (V x) = x\r\n\r\nbarPSCase v = case v of\r\n\tV x > x\r\n}}}\r\n{{{#!hs\r\nQuantPatSyn.hs:43:9: error:\r\n • Cannot instantiate unification variable ‘r0’\r\n with a type involving foralls: forall r. r\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the pattern: V x\r\n In a case alternative: V x > x\r\n In the expression: case v of { V x > x }\r\n \r\n43  V x > x\r\n  ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}
```
Consider the following two pattern synonyms:
```hs
pattern N :: () => () => forall r. r > (a > r) > r
pattern N < ((\f > f Nothing Just) > Nothing) where N = \n j > n
pattern J :: a > forall r. r > (a > r) > r
pattern J x < ((\f > f Nothing Just) > Just x) where J x = \n j > j x
```
The pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.
Now consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:
```hs
fooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
fooVPEqns ((\f > f Nothing Just) > Nothing) = Nothing
fooVPEqns ((\f > f Nothing Just) > Just x) = Just x
fooVPCase v = case v of
((\f > f Nothing Just) > Nothing) > Nothing
((\f > f Nothing Just) > Just x) > Just x
fooPSEqns N = Nothing
fooPSEqns (J x) = Just x
fooPSCase v = case v of
N > Nothing
J x > Just x
```
Three of these compile and work fine, the fourth breaks:
```hs
QuantPatSyn.hs:22:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a0 > r) > r’
• In the pattern: N
In a case alternative: N > Nothing
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

22  N > Nothing
 ^
QuantPatSyn.hs:23:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a > r) > r’
• In the pattern: J x
In a case alternative: J x > Just x
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

23  J x > Just x
 ^^^
```
The exact wording of the error message (the appearance of `forall` in the "actual type") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.
Another symptom can be observed with the following:
```hs
pattern V :: Void > (forall r. r)
pattern V x < ((\f > f) > x) where V x = absurd x
barVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void
barVPEqns ((\f > f) > x) = x
barVPCase v = case v of
((\f > f) > x) > x
barPSEqns (V x) = x
barPSCase v = case v of
V x > x
```
```hs
QuantPatSyn.hs:43:9: error:
• Cannot instantiate unification variable ‘r0’
with a type involving foralls: forall r. r
GHC doesn't yet support impredicative polymorphism
• In the pattern: V x
In a case alternative: V x > x
In the expression: case v of { V x > x }

43  V x > x
 ^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Higher rank types in pattern synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}\r\n}}}\r\nConsider the following two pattern synonyms:\r\n\r\n{{{#!hs\r\npattern N :: () => () => forall r. r > (a > r) > r\r\npattern N < ((\\f > f Nothing Just) > Nothing) where N = \\n j > n\r\n\r\npattern J :: a > forall r. r > (a > r) > r\r\npattern J x < ((\\f > f Nothing Just) > Just x) where J x = \\n j > j x\r\n}}}\r\n\r\nThe pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.\r\n\r\nNow consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:\r\n\r\n{{{#!hs\r\nfooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n\r\nfooVPEqns ((\\f > f Nothing Just) > Nothing) = Nothing\r\nfooVPEqns ((\\f > f Nothing Just) > Just x) = Just x\r\n\r\nfooVPCase v = case v of\r\n\t((\\f > f Nothing Just) > Nothing) > Nothing\r\n\t((\\f > f Nothing Just) > Just x) > Just x\r\n\r\nfooPSEqns N = Nothing\r\nfooPSEqns (J x) = Just x\r\n\r\nfooPSCase v = case v of\r\n\tN > Nothing\r\n\tJ x > Just x\r\n}}}\r\n\r\nThree of these compile and work fine, the fourth breaks:\r\n{{{#!hs\r\nQuantPatSyn.hs:22:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a0 > r) > r’\r\n • In the pattern: N\r\n In a case alternative: N > Nothing\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n22  N > Nothing\r\n  ^\r\n\r\nQuantPatSyn.hs:23:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a > r) > r’\r\n • In the pattern: J x\r\n In a case alternative: J x > Just x\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n23  J x > Just x\r\n  ^^^\r\n}}}\r\n\r\nThe exact wording of the error message (the appearance of `forall` in the \"actual type\") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.\r\n\r\nAnother symptom can be observed with the following:\r\n\r\n{{{#!hs\r\npattern V :: Void > (forall r. r)\r\npattern V x < ((\\f > f) > x) where V x = absurd x\r\n\r\nbarVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void\r\n\r\nbarVPEqns ((\\f > f) > x) = x\r\n\r\nbarVPCase v = case v of\r\n\t((\\f > f) > x) > x\r\n\r\nbarPSEqns (V x) = x\r\n\r\nbarPSCase v = case v of\r\n\tV x > x\r\n}}}\r\n{{{#!hs\r\nQuantPatSyn.hs:43:9: error:\r\n • Cannot instantiate unification variable ‘r0’\r\n with a type involving foralls: forall r. r\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the pattern: V x\r\n In a case alternative: V x > x\r\n In the expression: case v of { V x > x }\r\n \r\n43  V x > x\r\n  ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.10.1https://gitlab.haskell.org/ghc/ghc/issues/15020PatternSynonyms: Problems with quantified constraints / foralls20190707T18:14:40ZIcelandjackPatternSynonyms: Problems with quantified constraints / forallsI couldn't find a way to implement `PLam2` as a simply bidirectional pattern synonym, I expected it to work but I recall a similar ticket. I couldn't find it though.
```hs
{# Language RankNTypes, PatternSynonyms, ViewPatterns #}
newtype Lam1 = Lam1 (forall xx mm. Monad mm => mm xx)
pattern PLam1 :: (forall xx mm. Monad mm => mm xx) > Lam1
pattern PLam1 a = Lam1 a

newtype Lam2 a = Lam2 (forall mm. Monad mm => mm a)
newtype Forall f = Forall (forall xx. f xx)
 · FAILS ·
 pattern PLam2 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
 pattern PLam2 lam = Forall (Lam2 lam)

get :: Forall Lam2 > forall xx mm. Monad mm => mm xx
get (Forall (Lam2 lam)) = lam
pattern PLam3 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
pattern PLam3 lam < (get > lam)
where PLam3 lam = Forall (Lam2 lam)
```
The complaint is `V`, I wonder if this is a limitation of PatternSynonyms
```
• Couldn't match type ‘xx0’ with ‘xx’
because type variable ‘xx’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall xx (mm :: * > *). Monad mm => mm xx
at Test.hs:16:3436
Expected type: mm xx
Actual type: mm xx0
• In the declaration for pattern synonym ‘PLam2’
• Relevant bindings include
lam :: forall (mm :: * > *). Monad mm => mm xx0
(bound at Test.hs:16:34)

16  pattern PLam2 lam = Forall (Lam2 lam)
 ^^^
```I couldn't find a way to implement `PLam2` as a simply bidirectional pattern synonym, I expected it to work but I recall a similar ticket. I couldn't find it though.
```hs
{# Language RankNTypes, PatternSynonyms, ViewPatterns #}
newtype Lam1 = Lam1 (forall xx mm. Monad mm => mm xx)
pattern PLam1 :: (forall xx mm. Monad mm => mm xx) > Lam1
pattern PLam1 a = Lam1 a

newtype Lam2 a = Lam2 (forall mm. Monad mm => mm a)
newtype Forall f = Forall (forall xx. f xx)
 · FAILS ·
 pattern PLam2 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
 pattern PLam2 lam = Forall (Lam2 lam)

get :: Forall Lam2 > forall xx mm. Monad mm => mm xx
get (Forall (Lam2 lam)) = lam
pattern PLam3 :: (forall xx mm. Monad mm => mm xx) > Forall Lam2
pattern PLam3 lam < (get > lam)
where PLam3 lam = Forall (Lam2 lam)
```
The complaint is `V`, I wonder if this is a limitation of PatternSynonyms
```
• Couldn't match type ‘xx0’ with ‘xx’
because type variable ‘xx’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall xx (mm :: * > *). Monad mm => mm xx
at Test.hs:16:3436
Expected type: mm xx
Actual type: mm xx0
• In the declaration for pattern synonym ‘PLam2’
• Relevant bindings include
lam :: forall (mm :: * > *). Monad mm => mm xx0
(bound at Test.hs:16:34)

16  pattern PLam2 lam = Forall (Lam2 lam)
 ^^^
```8.10.1https://gitlab.haskell.org/ghc/ghc/issues/15014Exhaustivity check should suggest when COMPLETE could be helpful20190707T18:14:41ZEdward Z. YangExhaustivity check should suggest when COMPLETE could be helpful```
MacBookPro97:ghc ezyang$ cat A.hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern F :: a > b > (a, b)
pattern F x y = (x, y)
g :: (a, b) > (a, b)
g (F x y) = (x, y)
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp
A.hs:8:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’: Patterns not matched: _

8  g (F x y) = (x, y)
 ^^^^^^^^^^^^^^^^^^
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version
The Glorious Glasgow Haskell Compilation System, version 8.5.20180304
```
Any time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Exhaustivity check should suggest when COMPLETE could be helpful","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\nMacBookPro97:ghc ezyang$ cat A.hs\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule A where\r\n\r\npattern F :: a > b > (a, b)\r\npattern F x y = (x, y)\r\n\r\ng :: (a, b) > (a, b)\r\ng (F x y) = (x, y)\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp\r\n\r\nA.hs:8:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘g’: Patterns not matched: _\r\n \r\n8  g (F x y) = (x, y)\r\n  ^^^^^^^^^^^^^^^^^^\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version\r\nThe Glorious Glasgow Haskell Compilation System, version 8.5.20180304\r\n}}}\r\n\r\nAny time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.","type_of_failure":"OtherFailure","blocking":[]} >```
MacBookPro97:ghc ezyang$ cat A.hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern F :: a > b > (a, b)
pattern F x y = (x, y)
g :: (a, b) > (a, b)
g (F x y) = (x, y)
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp
A.hs:8:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’: Patterns not matched: _

8  g (F x y) = (x, y)
 ^^^^^^^^^^^^^^^^^^
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version
The Glorious Glasgow Haskell Compilation System, version 8.5.20180304
```
Any time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Exhaustivity check should suggest when COMPLETE could be helpful","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\nMacBookPro97:ghc ezyang$ cat A.hs\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule A where\r\n\r\npattern F :: a > b > (a, b)\r\npattern F x y = (x, y)\r\n\r\ng :: (a, b) > (a, b)\r\ng (F x y) = (x, y)\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp\r\n\r\nA.hs:8:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘g’: Patterns not matched: _\r\n \r\n8  g (F x y) = (x, y)\r\n  ^^^^^^^^^^^^^^^^^^\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version\r\nThe Glorious Glasgow Haskell Compilation System, version 8.5.20180304\r\n}}}\r\n\r\nAny time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.","type_of_failure":"OtherFailure","blocking":[]} >8.4.3https://gitlab.haskell.org/ghc/ghc/issues/14851"Pattern match has inaccessible right hand side" with TypeRep20190819T15:52:43ZRichard Eisenbergrae@richarde.dev"Pattern match has inaccessible right hand side" with TypeRepWhen I say
```hs
{# LANGUAGE PatternSynonyms, ViewPatterns #}
module Bug where
import Type.Reflection
pattern X arg < (checkFun > arg)
checkFun :: TypeRep fun > a
checkFun = undefined
f x = case (x, True) of
(X _, _) > 5
_ > 6
g x = case x of
(X _) > 5
_ > 6
```
I get
```
Bug.hs:13:11: warning: [Woverlappingpatterns]
Pattern match has inaccessible right hand side
In a case alternative: (X _, _) > ...

13  (X _, _) > 5
 ^^^^^^^^^^^^^
```
I'm troubled by two things:
1. There's nothing inaccessible about my righthand side.
1. This happens only for `f`, not `g`. If there's no tuple, there's no problem.
Note that this problems requires `TypeRep`. Even another polykinded tycon (like `Proxy`) didn't trigger the problem.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"\"Pattern match has inaccessible right hand side\" with TypeRep","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms, ViewPatterns #}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\npattern X arg < (checkFun > arg)\r\n\r\ncheckFun :: TypeRep fun > a\r\ncheckFun = undefined\r\n\r\nf x = case (x, True) of\r\n (X _, _) > 5\r\n _ > 6\r\n\r\ng x = case x of\r\n (X _) > 5\r\n _ > 6\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:13:11: warning: [Woverlappingpatterns]\r\n Pattern match has inaccessible right hand side\r\n In a case alternative: (X _, _) > ...\r\n \r\n13  (X _, _) > 5\r\n  ^^^^^^^^^^^^^\r\n}}}\r\n\r\nI'm troubled by two things:\r\n\r\n1. There's nothing inaccessible about my righthand side.\r\n2. This happens only for `f`, not `g`. If there's no tuple, there's no problem.\r\n\r\nNote that this problems requires `TypeRep`. Even another polykinded tycon (like `Proxy`) didn't trigger the problem.","type_of_failure":"OtherFailure","blocking":[]} >When I say
```hs
{# LANGUAGE PatternSynonyms, ViewPatterns #}
module Bug where
import Type.Reflection
pattern X arg < (checkFun > arg)
checkFun :: TypeRep fun > a
checkFun = undefined
f x = case (x, True) of
(X _, _) > 5
_ > 6
g x = case x of
(X _) > 5
_ > 6
```
I get
```
Bug.hs:13:11: warning: [Woverlappingpatterns]
Pattern match has inaccessible right hand side
In a case alternative: (X _, _) > ...

13  (X _, _) > 5
 ^^^^^^^^^^^^^
```
I'm troubled by two things:
1. There's nothing inaccessible about my righthand side.
1. This happens only for `f`, not `g`. If there's no tuple, there's no problem.
Note that this problems requires `TypeRep`. Even another polykinded tycon (like `Proxy`) didn't trigger the problem.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"\"Pattern match has inaccessible right hand side\" with TypeRep","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms, ViewPatterns #}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\npattern X arg < (checkFun > arg)\r\n\r\ncheckFun :: TypeRep fun > a\r\ncheckFun = undefined\r\n\r\nf x = case (x, True) of\r\n (X _, _) > 5\r\n _ > 6\r\n\r\ng x = case x of\r\n (X _) > 5\r\n _ > 6\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:13:11: warning: [Woverlappingpatterns]\r\n Pattern match has inaccessible right hand side\r\n In a case alternative: (X _, _) > ...\r\n \r\n13  (X _, _) > 5\r\n  ^^^^^^^^^^^^^\r\n}}}\r\n\r\nI'm troubled by two things:\r\n\r\n1. There's nothing inaccessible about my righthand side.\r\n2. This happens only for `f`, not `g`. If there's no tuple, there's no problem.\r\n\r\nNote that this problems requires `TypeRep`. Even another polykinded tycon (like `Proxy`) didn't trigger the problem.","type_of_failure":"OtherFailure","blocking":[]} >Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/issues/14630name shadowing warnings by record pattern synonyms + RecordWildCards or Named...20190707T18:16:13Zmizunashi_mananame shadowing warnings by record pattern synonyms + RecordWildCards or NamedFieldPunsWhen I use PatternSynonyms + RecordWildCards/NamedFieldPuns, I get name shadowing warnings. I am hoping that these warnings don't trigger in the below case.
```hs
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE RecordWildCards #}
{# LANGUAGE NamedFieldPuns #}
module TestPatternSynonyms where
pattern Tuple :: a > b > (a, b)
pattern Tuple{x, y} = (x, y)
{# COMPLETE Tuple #}
f :: (a, b) > a
f Tuple{x} = x
{ warning: [Wnameshadowing]
This binding for ‘x’ shadows the existing binding
}
g :: (Int, Int) > Int
g Tuple{..} = x + y
{ warning: [Wnameshadowing]
This binding for ‘x’ shadows the existing binding
This binding for ‘y’ shadows the existing binding
}
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"name shadowing warnings by record pattern synonyms + RecordWildCards or NamedFieldPuns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I use PatternSynonyms + RecordWildCards/NamedFieldPuns, I get name shadowing warnings. I am hoping that these warnings don't trigger in the below case.\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE RecordWildCards #}\r\n{# LANGUAGE NamedFieldPuns #}\r\n\r\nmodule TestPatternSynonyms where\r\n\r\npattern Tuple :: a > b > (a, b)\r\npattern Tuple{x, y} = (x, y)\r\n\r\n{# COMPLETE Tuple #}\r\n\r\nf :: (a, b) > a\r\nf Tuple{x} = x\r\n{ warning: [Wnameshadowing]\r\n This binding for ‘x’ shadows the existing binding\r\n}\r\n\r\ng :: (Int, Int) > Int\r\ng Tuple{..} = x + y\r\n{ warning: [Wnameshadowing]\r\n This binding for ‘x’ shadows the existing binding \r\n This binding for ‘y’ shadows the existing binding\r\n}\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >When I use PatternSynonyms + RecordWildCards/NamedFieldPuns, I get name shadowing warnings. I am hoping that these warnings don't trigger in the below case.
```hs
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE RecordWildCards #}
{# LANGUAGE NamedFieldPuns #}
module TestPatternSynonyms where
pattern Tuple :: a > b > (a, b)
pattern Tuple{x, y} = (x, y)
{# COMPLETE Tuple #}
f :: (a, b) > a
f Tuple{x} = x
{ warning: [Wnameshadowing]
This binding for ‘x’ shadows the existing binding
}
g :: (Int, Int) > Int
g Tuple{..} = x + y
{ warning: [Wnameshadowing]
This binding for ‘x’ shadows the existing binding
This binding for ‘y’ shadows the existing binding
}
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"name shadowing warnings by record pattern synonyms + RecordWildCards or NamedFieldPuns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I use PatternSynonyms + RecordWildCards/NamedFieldPuns, I get name shadowing warnings. I am hoping that these warnings don't trigger in the below case.\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE RecordWildCards #}\r\n{# LANGUAGE NamedFieldPuns #}\r\n\r\nmodule TestPatternSynonyms where\r\n\r\npattern Tuple :: a > b > (a, b)\r\npattern Tuple{x, y} = (x, y)\r\n\r\n{# COMPLETE Tuple #}\r\n\r\nf :: (a, b) > a\r\nf Tuple{x} = x\r\n{ warning: [Wnameshadowing]\r\n This binding for ‘x’ shadows the existing binding\r\n}\r\n\r\ng :: (Int, Int) > Int\r\ng Tuple{..} = x + y\r\n{ warning: [Wnameshadowing]\r\n This binding for ‘x’ shadows the existing binding \r\n This binding for ‘y’ shadows the existing binding\r\n}\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/14423{# complete #} should be able to handle  like {# minimal #}20190707T18:17:05Zekmett@gmail.com{# complete #} should be able to handle  like {# minimal #}It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns.
I have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.
Consider what happens if you add a mix of actual and smart views of a data type:
```hs
{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}
newtype Delta = Delta Int deriving (Eq,Num)
instance Monoid Delta where
mempty = 0
mappend = (+)
data Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp
rel 0 xs = xs
rel d (AP d' l r) = AP (d + d') l r
rel d (LAM d' b) = LAM (d + d') b
rel _ (Var n) = Var n
pattern Ap a b < AP d (rel d > a) (rel d > b) where
Ap a b = AP 0 a b
pattern Lam b < LAM d (rel d > b) where
Lam b = LAM 0 b
{# complete Var, AP, Lam #}
{# complete Var, Ap, LAM #}
{# complete Var, AP, LAM #}
```
Every data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.
On the other hand with `` patterns:
```hs
{# complete Var, (Ap  AP), (Lam  LAM) #}
```
extends linearly.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"{# complete #} should be able to handle  like {# minimal #}","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns. \r\n\r\nI have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.\r\n\r\nConsider what happens if you add a mix of actual and smart views of a data type:\r\n\r\n{{{#!hs\r\n{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}\r\n\r\nnewtype Delta = Delta Int deriving (Eq,Num)\r\n\r\ninstance Monoid Delta where\r\n mempty = 0\r\n mappend = (+)\r\n\r\ndata Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp\r\n\r\nrel 0 xs = xs\r\nrel d (AP d' l r) = AP (d + d') l r\r\nrel d (LAM d' b) = LAM (d + d') b\r\nrel _ (Var n) = Var n\r\n\r\npattern Ap a b < AP d (rel d > a) (rel d > b) where\r\n Ap a b = AP 0 a b\r\n\r\npattern Lam b < LAM d (rel d > b) where\r\n Lam b = LAM 0 b\r\n\r\n{# complete Var, AP, Lam #}\r\n{# complete Var, Ap, LAM #}\r\n{# complete Var, AP, LAM #}\r\n}}}\r\n\r\nEvery data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.\r\n\r\nOn the other hand with `` patterns:\r\n\r\n{{{#!hs\r\n{# complete Var, (Ap  AP), (Lam  LAM) #}\r\n}}} \r\n\r\nextends linearly.","type_of_failure":"OtherFailure","blocking":[]} >It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns.
I have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.
Consider what happens if you add a mix of actual and smart views of a data type:
```hs
{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}
newtype Delta = Delta Int deriving (Eq,Num)
instance Monoid Delta where
mempty = 0
mappend = (+)
data Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp
rel 0 xs = xs
rel d (AP d' l r) = AP (d + d') l r
rel d (LAM d' b) = LAM (d + d') b
rel _ (Var n) = Var n
pattern Ap a b < AP d (rel d > a) (rel d > b) where
Ap a b = AP 0 a b
pattern Lam b < LAM d (rel d > b) where
Lam b = LAM 0 b
{# complete Var, AP, Lam #}
{# complete Var, Ap, LAM #}
{# complete Var, AP, LAM #}
```
Every data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.
On the other hand with `` patterns:
```hs
{# complete Var, (Ap  AP), (Lam  LAM) #}
```
extends linearly.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"{# complete #} should be able to handle  like {# minimal #}","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns. \r\n\r\nI have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.\r\n\r\nConsider what happens if you add a mix of actual and smart views of a data type:\r\n\r\n{{{#!hs\r\n{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}\r\n\r\nnewtype Delta = Delta Int deriving (Eq,Num)\r\n\r\ninstance Monoid Delta where\r\n mempty = 0\r\n mappend = (+)\r\n\r\ndata Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp\r\n\r\nrel 0 xs = xs\r\nrel d (AP d' l r) = AP (d + d') l r\r\nrel d (LAM d' b) = LAM (d + d') b\r\nrel _ (Var n) = Var n\r\n\r\npattern Ap a b < AP d (rel d > a) (rel d > b) where\r\n Ap a b = AP 0 a b\r\n\r\npattern Lam b < LAM d (rel d > b) where\r\n Lam b = LAM 0 b\r\n\r\n{# complete Var, AP, Lam #}\r\n{# complete Var, Ap, LAM #}\r\n{# complete Var, AP, LAM #}\r\n}}}\r\n\r\nEvery data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.\r\n\r\nOn the other hand with `` patterns:\r\n\r\n{{{#!hs\r\n{# complete Var, (Ap  AP), (Lam  LAM) #}\r\n}}} \r\n\r\nextends linearly.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/14422{# complete #} should be able to be at least partially type directed20190719T13:45:06Zekmett@gmail.com{# complete #} should be able to be at least partially type directedThe fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"{# complete #} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} >The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"{# complete #} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/14253Pattern match checker mistakenly concludes pattern match on pattern synonym i...20190819T15:52:43ZBen GamariPattern match checker mistakenly concludes pattern match on pattern synonym is unreachableConsider this program,
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Test where
import GHC.Exts
import Data.Kind
data TypeRep (a :: k) where
Con :: TypeRep (a :: k)
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
TypeRep a
> TypeRep b
> TypeRep (a > b)
pattern Fun :: forall k (fun :: k). ()
=> forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(arg :: TYPE r1) (res :: TYPE r2).
(k ~ Type, fun ~~ (arg > res))
=> TypeRep arg
> TypeRep res
> TypeRep fun
pattern Fun arg res < TrFun arg res
where Fun arg res = undefined
data Dynamic where
Dynamic :: forall a. TypeRep a > a > Dynamic
 Removing this allows compilation to proceed
{# COMPLETE Con #}
dynApply :: Dynamic > Dynamic > Maybe Dynamic
 Changing Fun to TrFun allows compilation to proceed
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
dynApply _ _ = Nothing
```
As written the program fails with,
```
test.hs:34:1: warning: [Woverlappingpatterns]
Pattern match has inaccessible right hand side
In an equation for ‘dynApply’:
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ...

34  dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This can be worked around by doing one of the following,
1. Removing the `COMPLETE` pragma
1. Changing the use of the `Fun` pattern synonym into a use of the `TrFun` constructor.
Something is quite wrong here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  George 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["George"],"type":"Bug","description":"Consider this program,\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nmodule Test where\r\n\r\nimport GHC.Exts\r\nimport Data.Kind\r\n\r\ndata TypeRep (a :: k) where\r\n Con :: TypeRep (a :: k)\r\n TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)\r\n (a :: TYPE r1) (b :: TYPE r2).\r\n TypeRep a\r\n > TypeRep b\r\n > TypeRep (a > b)\r\n\r\npattern Fun :: forall k (fun :: k). ()\r\n => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)\r\n (arg :: TYPE r1) (res :: TYPE r2).\r\n (k ~ Type, fun ~~ (arg > res))\r\n => TypeRep arg\r\n > TypeRep res\r\n > TypeRep fun\r\npattern Fun arg res < TrFun arg res\r\n where Fun arg res = undefined\r\n\r\ndata Dynamic where\r\n Dynamic :: forall a. TypeRep a > a > Dynamic\r\n\r\n Removing this allows compilation to proceed\r\n{# COMPLETE Con #}\r\n\r\ndynApply :: Dynamic > Dynamic > Maybe Dynamic\r\n Changing Fun to TrFun allows compilation to proceed\r\ndynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined\r\ndynApply _ _ = Nothing\r\n}}}\r\n\r\nAs written the program fails with,\r\n{{{\r\ntest.hs:34:1: warning: [Woverlappingpatterns]\r\n Pattern match has inaccessible right hand side\r\n In an equation for ‘dynApply’:\r\n dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ...\r\n \r\n34  dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis can be worked around by doing one of the following,\r\n 1. Removing the `COMPLETE` pragma\r\n 2. Changing the use of the `Fun` pattern synonym into a use of the `TrFun` constructor.\r\n\r\nSomething is quite wrong here.","type_of_failure":"OtherFailure","blocking":[]} >Consider this program,
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Test where
import GHC.Exts
import Data.Kind
data TypeRep (a :: k) where
Con :: TypeRep (a :: k)
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
TypeRep a
> TypeRep b
> TypeRep (a > b)
pattern Fun :: forall k (fun :: k). ()
=> forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(arg :: TYPE r1) (res :: TYPE r2).
(k ~ Type, fun ~~ (arg > res))
=> TypeRep arg
> TypeRep res
> TypeRep fun
pattern Fun arg res < TrFun arg res
where Fun arg res = undefined
data Dynamic where
Dynamic :: forall a. TypeRep a > a > Dynamic
 Removing this allows compilation to proceed
{# COMPLETE Con #}
dynApply :: Dynamic > Dynamic > Maybe Dynamic
 Changing Fun to TrFun allows compilation to proceed
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
dynApply _ _ = Nothing
```
As written the program fails with,
```
test.hs:34:1: warning: [Woverlappingpatterns]
Pattern match has inaccessible right hand side
In an equation for ‘dynApply’:
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ...

34  dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This can be worked around by doing one of the following,
1. Removing the `COMPLETE` pragma
1. Changing the use of the `Fun` pattern synonym into a use of the `TrFun` constructor.
Something is quite wrong here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  George 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["George"],"type":"Bug","description":"Consider this program,\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nmodule Test where\r\n\r\nimport GHC.Exts\r\nimport Data.Kind\r\n\r\ndata TypeRep (a :: k) where\r\n Con :: TypeRep (a :: k)\r\n TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)\r\n (a :: TYPE r1) (b :: TYPE r2).\r\n TypeRep a\r\n > TypeRep b\r\n > TypeRep (a > b)\r\n\r\npattern Fun :: forall k (fun :: k). ()\r\n => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)\r\n (arg :: TYPE r1) (res :: TYPE r2).\r\n (k ~ Type, fun ~~ (arg > res))\r\n => TypeRep arg\r\n > TypeRep res\r\n > TypeRep fun\r\npattern Fun arg res < TrFun arg res\r\n where Fun arg res = undefined\r\n\r\ndata Dynamic where\r\n Dynamic :: forall a. TypeRep a > a > Dynamic\r\n\r\n Removing this allows compilation to proceed\r\n{# COMPLETE Con #}\r\n\r\ndynApply :: Dynamic > Dynamic > Maybe Dynamic\r\n Changing Fun to TrFun allows compilation to proceed\r\ndynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined\r\ndynApply _ _ = Nothing\r\n}}}\r\n\r\nAs written the program fails with,\r\n{{{\r\ntest.hs:34:1: warning: [Woverlappingpatterns]\r\n Pattern match has inaccessible right hand side\r\n In an equation for ‘dynApply’:\r\n dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ...\r\n \r\n34  dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis can be worked around by doing one of the following,\r\n 1. Removing the `COMPLETE` pragma\r\n 2. Changing the use of the `Fun` pattern synonym into a use of the `TrFun` constructor.\r\n\r\nSomething is quite wrong here.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/issues/14059COMPLETE sets don't work at all with data family instances20190819T15:52:43ZRyan ScottCOMPLETE sets don't work at all with data family instancesHere's some code that uses a pattern synonym for a data family GADT constructor, along with a corresponding `COMPLETE` set:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# OPTIONS_GHC Wincompletepatterns #}
module Bug where
data family Sing (a :: k)
data instance Sing (z :: Bool) where
SFalse :: Sing False
STrue :: Sing True
pattern STooGoodToBeTrue :: forall (z :: Bool). ()
=> z ~ True
=> Sing z
pattern STooGoodToBeTrue = STrue
{# COMPLETE SFalse, STooGoodToBeTrue #}
wibble :: Sing (z :: Bool) > Bool
wibble STrue = True
wobble :: Sing (z :: Bool) > Bool
wobble STooGoodToBeTrue = True
```
However, if you compile this, you might be surprised to find out that GHC only warns about `wibble` being nonexhaustive:
```
$ ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:23:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘wibble’: Patterns not matched: SFalse

23  wibble STrue = True
 ^^^^^^^^^^^^^^^^^^^
```
I believe the use of data families is the culprit here, since a variant of this program which doesn't use data families correctly warns for both `wibble` and `wobble`:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# OPTIONS_GHC Wincompletepatterns #}
module Foo where
data SBool (z :: Bool) where
SFalse :: SBool False
STrue :: SBool True
pattern STooGoodToBeTrue :: forall (z :: Bool). ()
=> z ~ True
=> SBool z
pattern STooGoodToBeTrue = STrue
{# COMPLETE SFalse, STooGoodToBeTrue #}
wibble :: SBool z > Bool
wibble STrue = True
wobble :: SBool z > Bool
wobble STooGoodToBeTrue = True
```
```
$ ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:20:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘wibble’: Patterns not matched: SFalse

20  wibble STrue = True
 ^^^^^^^^^^^^^^^^^^^
Foo.hs:23:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘wobble’: Patterns not matched: SFalse

23  wobble STooGoodToBeTrue = True
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"COMPLETE sets don't work at all with data family instances","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's some code that uses a pattern synonym for a data family GADT constructor, along with a corresponding `COMPLETE` set:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# OPTIONS_GHC Wincompletepatterns #}\r\nmodule Bug where\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata instance Sing (z :: Bool) where\r\n SFalse :: Sing False\r\n STrue :: Sing True\r\n\r\npattern STooGoodToBeTrue :: forall (z :: Bool). ()\r\n => z ~ True\r\n => Sing z\r\npattern STooGoodToBeTrue = STrue\r\n{# COMPLETE SFalse, STooGoodToBeTrue #}\r\n\r\nwibble :: Sing (z :: Bool) > Bool\r\nwibble STrue = True\r\n\r\nwobble :: Sing (z :: Bool) > Bool\r\nwobble STooGoodToBeTrue = True\r\n}}}\r\n\r\nHowever, if you compile this, you might be surprised to find out that GHC only warns about `wibble` being nonexhaustive:\r\n\r\n{{{\r\n$ ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:23:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘wibble’: Patterns not matched: SFalse\r\n \r\n23  wibble STrue = True\r\n  ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI believe the use of data families is the culprit here, since a variant of this program which doesn't use data families correctly warns for both `wibble` and `wobble`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# OPTIONS_GHC Wincompletepatterns #}\r\nmodule Foo where\r\n\r\ndata SBool (z :: Bool) where\r\n SFalse :: SBool False\r\n STrue :: SBool True\r\n\r\npattern STooGoodToBeTrue :: forall (z :: Bool). ()\r\n => z ~ True\r\n => SBool z\r\npattern STooGoodToBeTrue = STrue\r\n{# COMPLETE SFalse, STooGoodToBeTrue #}\r\n\r\nwibble :: SBool z > Bool\r\nwibble STrue = True\r\n\r\nwobble :: SBool z > Bool\r\nwobble STooGoodToBeTrue = True\r\n}}}\r\n\r\n{{{\r\n$ ghci Foo.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:20:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘wibble’: Patterns not matched: SFalse\r\n \r\n20  wibble STrue = True\r\n  ^^^^^^^^^^^^^^^^^^^\r\n\r\nFoo.hs:23:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘wobble’: Patterns not matched: SFalse\r\n \r\n23  wobble STooGoodToBeTrue = True\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Here's some code that uses a pattern synonym for a data family GADT constructor, along with a corresponding `COMPLETE` set:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# OPTIONS_GHC Wincompletepatterns #}
module Bug where
data family Sing (a :: k)
data instance Sing (z :: Bool) where
SFalse :: Sing False
STrue :: Sing True
pattern STooGoodToBeTrue :: forall (z :: Bool). ()
=> z ~ True
=> Sing z
pattern STooGoodToBeTrue = STrue
{# COMPLETE SFalse, STooGoodToBeTrue #}
wibble :: Sing (z :: Bool) > Bool
wibble STrue = True
wobble :: Sing (z :: Bool) > Bool
wobble STooGoodToBeTrue = True
```
However, if you compile this, you might be surprised to find out that GHC only warns about `wibble` being nonexhaustive:
```
$ ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:23:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘wibble’: Patterns not matched: SFalse

23  wibble STrue = True
 ^^^^^^^^^^^^^^^^^^^
```
I believe the use of data families is the culprit here, since a variant of this program which doesn't use data families correctly warns for both `wibble` and `wobble`:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# OPTIONS_GHC Wincompletepatterns #}
module Foo where
data SBool (z :: Bool) where
SFalse :: SBool False
STrue :: SBool True
pattern STooGoodToBeTrue :: forall (z :: Bool). ()
=> z ~ True
=> SBool z
pattern STooGoodToBeTrue = STrue
{# COMPLETE SFalse, STooGoodToBeTrue #}
wibble :: SBool z > Bool
wibble STrue = True
wobble :: SBool z > Bool
wobble STooGoodToBeTrue = True
```
```
$ ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:20:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘wibble’: Patterns not matched: SFalse

20  wibble STrue = True
 ^^^^^^^^^^^^^^^^^^^
Foo.hs:23:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘wobble’: Patterns not matched: SFalse

23  wobble STooGoodToBeTrue = True
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"COMPLETE sets don't work at all with data family instances","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's some code that uses a pattern synonym for a data family GADT constructor, along with a corresponding `COMPLETE` set:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# OPTIONS_GHC Wincompletepatterns #}\r\nmodule Bug where\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata instance Sing (z :: Bool) where\r\n SFalse :: Sing False\r\n STrue :: Sing True\r\n\r\npattern STooGoodToBeTrue :: forall (z :: Bool). ()\r\n => z ~ True\r\n => Sing z\r\npattern STooGoodToBeTrue = STrue\r\n{# COMPLETE SFalse, STooGoodToBeTrue #}\r\n\r\nwibble :: Sing (z :: Bool) > Bool\r\nwibble STrue = True\r\n\r\nwobble :: Sing (z :: Bool) > Bool\r\nwobble STooGoodToBeTrue = True\r\n}}}\r\n\r\nHowever, if you compile this, you might be surprised to find out that GHC only warns about `wibble` being nonexhaustive:\r\n\r\n{{{\r\n$ ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:23:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘wibble’: Patterns not matched: SFalse\r\n \r\n23  wibble STrue = True\r\n  ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI believe the use of data families is the culprit here, since a variant of this program which doesn't use data families correctly warns for both `wibble` and `wobble`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# OPTIONS_GHC Wincompletepatterns #}\r\nmodule Foo where\r\n\r\ndata SBool (z :: Bool) where\r\n SFalse :: SBool False\r\n STrue :: SBool True\r\n\r\npattern STooGoodToBeTrue :: forall (z :: Bool). ()\r\n => z ~ True\r\n => SBool z\r\npattern STooGoodToBeTrue = STrue\r\n{# COMPLETE SFalse, STooGoodToBeTrue #}\r\n\r\nwibble :: SBool z > Bool\r\nwibble STrue = True\r\n\r\nwobble :: SBool z > Bool\r\nwobble STooGoodToBeTrue = True\r\n}}}\r\n\r\n{{{\r\n$ ghci Foo.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:20:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘wibble’: Patterns not matched: SFalse\r\n \r\n20  wibble STrue = True\r\n  ^^^^^^^^^^^^^^^^^^^\r\n\r\nFoo.hs:23:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘wobble’: Patterns not matched: SFalse\r\n \r\n23  wobble STooGoodToBeTrue = True\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13975GHC can't infer pattern signature, untoucable kinds20190707T18:19:06ZIcelandjackGHC can't infer pattern signature, untoucable kinds```hs
{# Language TypeFamilyDependencies, TypeInType, KindSignatures, PolyKinds, PatternSynonyms, GADTs #}
import Data.Kind
data T = D  I
type SING k = k > Type
type family
Sing = (r :: SING k)  r > k where
Sing = ST
Sing = SPair
data ST :: SING T where
SD :: ST D
SI :: ST I
data SPair :: SING (k, k') where
SPair :: Sing a > Sing b > SPair '(a, b)
pattern DD :: SPair '(D, D)
pattern DD = SPair SD SD
```
works.. until we remove the pattern signature for `DD`, then we get
```
$ ghci8.0.1 ignoredotghci /tmp/aur.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/aur.hs, interpreted )
/tmp/aur.hs:21:20: error:
• Couldn't match kind ‘k’ with ‘T’
‘k’ is untouchable
inside the constraints: t ~ '(a, b)
bound by a pattern with constructor:
SPair :: forall k k' (a :: k) (b :: k').
Sing a > Sing b > SPair '(a, b),
in a pattern synonym declaration
at /tmp/aur.hs:21:1424
‘k’ is a rigid type variable bound by
the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
Possible fix: add a type signature for ‘DD’
When matching the kind of ‘a’
Expected type: Sing a
Actual type: ST a
• In the pattern: SD
In the pattern: SPair SD SD
In the declaration for pattern synonym ‘DD’
/tmp/aur.hs:21:23: error:
• Couldn't match kind ‘k'’ with ‘T’
‘k'’ is untouchable
inside the constraints: a ~ 'D
bound by a pattern with constructor: SD :: ST 'D,
in a pattern synonym declaration
at /tmp/aur.hs:21:2021
‘k'’ is a rigid type variable bound by
the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
Possible fix: add a type signature for ‘DD’
When matching the kind of ‘b’
Expected type: Sing b
Actual type: ST b
• In the pattern: SD
In the pattern: SPair SD SD
In the declaration for pattern synonym ‘DD’
Failed, modules loaded: none.
```
Restricting the kind of `SPair` to `SPair :: SING (T, T)` gets it to work, can it be made to work bidirectionally? Or can it only work unidirectionally
```hs
pattern DD :: () => (a ~ D, b ~ D, res ~ '(a, b)) => SPair res
pattern DD < SPair SD SD
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC can't infer pattern signature, untoucable kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language TypeFamilyDependencies, TypeInType, KindSignatures, PolyKinds, PatternSynonyms, GADTs #}\r\n\r\nimport Data.Kind\r\n\r\ndata T = D  I\r\n\r\ntype SING k = k > Type\r\n\r\ntype family\r\n Sing = (r :: SING k)  r > k where\r\n Sing = ST\r\n Sing = SPair\r\n\r\ndata ST :: SING T where\r\n SD :: ST D\r\n SI :: ST I\r\n\r\ndata SPair :: SING (k, k') where\r\n SPair :: Sing a > Sing b > SPair '(a, b)\r\n\r\npattern DD :: SPair '(D, D)\r\npattern DD = SPair SD SD\r\n}}}\r\n\r\nworks.. until we remove the pattern signature for `DD`, then we get\r\n\r\n{{{\r\n$ ghci8.0.1 ignoredotghci /tmp/aur.hs\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/aur.hs, interpreted )\r\n\r\n/tmp/aur.hs:21:20: error:\r\n • Couldn't match kind ‘k’ with ‘T’\r\n ‘k’ is untouchable\r\n inside the constraints: t ~ '(a, b)\r\n bound by a pattern with constructor:\r\n SPair :: forall k k' (a :: k) (b :: k').\r\n Sing a > Sing b > SPair '(a, b),\r\n in a pattern synonym declaration\r\n at /tmp/aur.hs:21:1424\r\n ‘k’ is a rigid type variable bound by\r\n the inferred type of DD :: SPair t at /tmp/aur.hs:21:9\r\n Possible fix: add a type signature for ‘DD’\r\n When matching the kind of ‘a’\r\n Expected type: Sing a\r\n Actual type: ST a\r\n • In the pattern: SD\r\n In the pattern: SPair SD SD\r\n In the declaration for pattern synonym ‘DD’\r\n\r\n/tmp/aur.hs:21:23: error:\r\n • Couldn't match kind ‘k'’ with ‘T’\r\n ‘k'’ is untouchable\r\n inside the constraints: a ~ 'D\r\n bound by a pattern with constructor: SD :: ST 'D,\r\n in a pattern synonym declaration\r\n at /tmp/aur.hs:21:2021\r\n ‘k'’ is a rigid type variable bound by\r\n the inferred type of DD :: SPair t at /tmp/aur.hs:21:9\r\n Possible fix: add a type signature for ‘DD’\r\n When matching the kind of ‘b’\r\n Expected type: Sing b\r\n Actual type: ST b\r\n • In the pattern: SD\r\n In the pattern: SPair SD SD\r\n In the declaration for pattern synonym ‘DD’\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nRestricting the kind of `SPair` to `SPair :: SING (T, T)` gets it to work, can it be made to work bidirectionally? Or can it only work unidirectionally\r\n\r\n{{{#!hs\r\npattern DD :: () => (a ~ D, b ~ D, res ~ '(a, b)) => SPair res\r\npattern DD < SPair SD SD\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language TypeFamilyDependencies, TypeInType, KindSignatures, PolyKinds, PatternSynonyms, GADTs #}
import Data.Kind
data T = D  I
type SING k = k > Type
type family
Sing = (r :: SING k)  r > k where
Sing = ST
Sing = SPair
data ST :: SING T where
SD :: ST D
SI :: ST I
data SPair :: SING (k, k') where
SPair :: Sing a > Sing b > SPair '(a, b)
pattern DD :: SPair '(D, D)
pattern DD = SPair SD SD
```
works.. until we remove the pattern signature for `DD`, then we get
```
$ ghci8.0.1 ignoredotghci /tmp/aur.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/aur.hs, interpreted )
/tmp/aur.hs:21:20: error:
• Couldn't match kind ‘k’ with ‘T’
‘k’ is untouchable
inside the constraints: t ~ '(a, b)
bound by a pattern with constructor:
SPair :: forall k k' (a :: k) (b :: k').
Sing a > Sing b > SPair '(a, b),
in a pattern synonym declaration
at /tmp/aur.hs:21:1424
‘k’ is a rigid type variable bound by
the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
Possible fix: add a type signature for ‘DD’
When matching the kind of ‘a’
Expected type: Sing a
Actual type: ST a
• In the pattern: SD
In the pattern: SPair SD SD
In the declaration for pattern synonym ‘DD’
/tmp/aur.hs:21:23: error:
• Couldn't match kind ‘k'’ with ‘T’
‘k'’ is untouchable
inside the constraints: a ~ 'D
bound by a pattern with constructor: SD :: ST 'D,
in a pattern synonym declaration
at /tmp/aur.hs:21:2021
‘k'’ is a rigid type variable bound by
the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
Possible fix: add a type signature for ‘DD’
When matching the kind of ‘b’
Expected type: Sing b
Actual type: ST b
• In the pattern: SD
In the pattern: SPair SD SD
In the declaration for pattern synonym ‘DD’
Failed, modules loaded: none.
```
Restricting the kind of `SPair` to `SPair :: SING (T, T)` gets it to work, can it be made to work bidirectionally? Or can it only work unidirectionally
```hs
pattern DD :: () => (a ~ D, b ~ D, res ~ '(a, b)) => SPair res
pattern DD < SPair SD SD
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC can't infer pattern signature, untoucable kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language TypeFamilyDependencies, TypeInType, KindSignatures, PolyKinds, PatternSynonyms, GADTs #}\r\n\r\nimport Data.Kind\r\n\r\ndata T = D  I\r\n\r\ntype SING k = k > Type\r\n\r\ntype family\r\n Sing = (r :: SING k)  r > k where\r\n Sing = ST\r\n Sing = SPair\r\n\r\ndata ST :: SING T where\r\n SD :: ST D\r\n SI :: ST I\r\n\r\ndata SPair :: SING (k, k') where\r\n SPair :: Sing a > Sing b > SPair '(a, b)\r\n\r\npattern DD :: SPair '(D, D)\r\npattern DD = SPair SD SD\r\n}}}\r\n\r\nworks.. until we remove the pattern signature for `DD`, then we get\r\n\r\n{{{\r\n$ ghci8.0.1 ignoredotghci /tmp/aur.hs\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/aur.hs, interpreted )\r\n\r\n/tmp/aur.hs:21:20: error:\r\n • Couldn't match kind ‘k’ with ‘T’\r\n ‘k’ is untouchable\r\n inside the constraints: t ~ '(a, b)\r\n bound by a pattern with constructor:\r\n SPair :: forall k k' (a :: k) (b :: k').\r\n Sing a > Sing b > SPair '(a, b),\r\n in a pattern synonym declaration\r\n at /tmp/aur.hs:21:1424\r\n ‘k’ is a rigid type variable bound by\r\n the inferred type of DD :: SPair t at /tmp/aur.hs:21:9\r\n Possible fix: add a type signature for ‘DD’\r\n When matching the kind of ‘a’\r\n Expected type: Sing a\r\n Actual type: ST a\r\n • In the pattern: SD\r\n In the pattern: SPair SD SD\r\n In the declaration for pattern synonym ‘DD’\r\n\r\n/tmp/aur.hs:21:23: error:\r\n • Couldn't match kind ‘k'’ with ‘T’\r\n ‘k'’ is untouchable\r\n inside the constraints: a ~ 'D\r\n bound by a pattern with constructor: SD :: ST 'D,\r\n in a pattern synonym declaration\r\n at /tmp/aur.hs:21:2021\r\n ‘k'’ is a rigid type variable bound by\r\n the inferred type of DD :: SPair t at /tmp/aur.hs:21:9\r\n Possible fix: add a type signature for ‘DD’\r\n When matching the kind of ‘b’\r\n Expected type: Sing b\r\n Actual type: ST b\r\n • In the pattern: SD\r\n In the pattern: SPair SD SD\r\n In the declaration for pattern synonym ‘DD’\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nRestricting the kind of `SPair` to `SPair :: SING (T, T)` gets it to work, can it be made to work bidirectionally? Or can it only work unidirectionally\r\n\r\n{{{#!hs\r\npattern DD :: () => (a ~ D, b ~ D, res ~ '(a, b)) => SPair res\r\npattern DD < SPair SD SD\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13965COMPLETE sets nerf redundant patternmatch warnings20190819T15:52:42ZRyan ScottCOMPLETE sets nerf redundant patternmatch warningsIf I give redundant patterns for a datatype with a `COMPLETE` set, then GHC doesn't warn me at all. Here's an example:
```hs
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ViewPatterns #}
module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where
data Boolean = F  T
deriving Eq
pattern TooGoodToBeTrue :: Boolean
pattern TooGoodToBeTrue < ((== T) > True)
where
TooGoodToBeTrue = T
{# COMPLETE F, TooGoodToBeTrue #}
catchAll :: Boolean > Int
catchAll F = 0
catchAll TooGoodToBeTrue = 1
catchAll F = 2
```
GHC thinks this is fine and dandy:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs Wall
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
```
This problem also persists across modules:
```hs
module Foo where
import Bug
catchAll2 :: Boolean > Int
catchAll2 F = 0
catchAll2 TooGoodToBeTrue = 1
catchAll2 F = 2
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs Wall
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 2] Compiling Bug ( Bug.hs, interpreted )
[2 of 2] Compiling Foo ( Foo.hs, interpreted )
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1rc2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"COMPLETE sets nerf redundant patternmatch warnings","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1rc2","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I give redundant patterns for a datatype with a `COMPLETE` set, then GHC doesn't warn me at all. Here's an example:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ViewPatterns #}\r\nmodule Bug (Boolean(F, TooGoodToBeTrue), catchAll) where\r\n\r\ndata Boolean = F  T\r\n deriving Eq\r\n\r\npattern TooGoodToBeTrue :: Boolean\r\npattern TooGoodToBeTrue < ((== T) > True)\r\n where\r\n TooGoodToBeTrue = T\r\n{# COMPLETE F, TooGoodToBeTrue #}\r\n\r\ncatchAll :: Boolean > Int\r\ncatchAll F = 0\r\ncatchAll TooGoodToBeTrue = 1\r\ncatchAll F = 2\r\n}}}\r\n\r\nGHC thinks this is fine and dandy:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs Wall\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\n}}}\r\n\r\nThis problem also persists across modules:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nimport Bug\r\n\r\ncatchAll2 :: Boolean > Int\r\ncatchAll2 F = 0\r\ncatchAll2 TooGoodToBeTrue = 1\r\ncatchAll2 F = 2\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs Wall\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 2] Compiling Bug ( Bug.hs, interpreted )\r\n[2 of 2] Compiling Foo ( Foo.hs, interpreted )\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >If I give redundant patterns for a datatype with a `COMPLETE` set, then GHC doesn't warn me at all. Here's an example:
```hs
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ViewPatterns #}
module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where
data Boolean = F  T
deriving Eq
pattern TooGoodToBeTrue :: Boolean
pattern TooGoodToBeTrue < ((== T) > True)
where
TooGoodToBeTrue = T
{# COMPLETE F, TooGoodToBeTrue #}
catchAll :: Boolean > Int
catchAll F = 0
catchAll TooGoodToBeTrue = 1
catchAll F = 2
```
GHC thinks this is fine and dandy:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs Wall
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
```
This problem also persists across modules:
```hs
module Foo where
import Bug
catchAll2 :: Boolean > Int
catchAll2 F = 0
catchAll2 TooGoodToBeTrue = 1
catchAll2 F = 2
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs Wall
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 2] Compiling Bug ( Bug.hs, interpreted )
[2 of 2] Compiling Foo ( Foo.hs, interpreted )
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1rc2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"COMPLETE sets nerf redundant patternmatch warnings","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1rc2","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I give redundant patterns for a datatype with a `COMPLETE` set, then GHC doesn't warn me at all. Here's an example:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ViewPatterns #}\r\nmodule Bug (Boolean(F, TooGoodToBeTrue), catchAll) where\r\n\r\ndata Boolean = F  T\r\n deriving Eq\r\n\r\npattern TooGoodToBeTrue :: Boolean\r\npattern TooGoodToBeTrue < ((== T) > True)\r\n where\r\n TooGoodToBeTrue = T\r\n{# COMPLETE F, TooGoodToBeTrue #}\r\n\r\ncatchAll :: Boolean > Int\r\ncatchAll F = 0\r\ncatchAll TooGoodToBeTrue = 1\r\ncatchAll F = 2\r\n}}}\r\n\r\nGHC thinks this is fine and dandy:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs Wall\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\n}}}\r\n\r\nThis problem also persists across modules:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nimport Bug\r\n\r\ncatchAll2 :: Boolean > Int\r\ncatchAll2 F = 0\r\ncatchAll2 TooGoodToBeTrue = 1\r\ncatchAll2 F = 2\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs Wall\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 2] Compiling Bug ( Bug.hs, interpreted )\r\n[2 of 2] Compiling Foo ( Foo.hs, interpreted )\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/issues/13964Patternmatch warnings for datatypes with COMPLETE sets break abstraction20190812T09:10:03ZRyan ScottPatternmatch warnings for datatypes with COMPLETE sets break abstractionHere's a file:
```hs
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ViewPatterns #}
module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where
data Boolean = F  T
deriving Eq
pattern TooGoodToBeTrue :: Boolean
pattern TooGoodToBeTrue < ((== T) > True)
where
TooGoodToBeTrue = T
{# COMPLETE F, TooGoodToBeTrue #}
catchAll :: Boolean > Int
catchAll F = 0
 catchAll TooGoodToBeTrue = 1
```
If you compile this with `Wall`, the warning will warn about `T`, not `TooGoodToBeTrue` (the other conlike in the `COMPLETE` set):
```
$ /opt/ghc/8.2.1/bin/ghc fforcerecomp Wall Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘catchAll’: Patterns not matched: T

15  catchAll F = 0
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Perhaps this isn't so bad, since it's intramodule. But the problem persists even across modules:
```hs
module Foo where
import Bug
catchAll2 :: Boolean > Int
catchAll2 F = 0
 catchAll2 TooGoodToBeTrue = 1
```
```
$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Bug.hs
$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Wall Foo.hs
Foo.hs:6:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘catchAll2’: Patterns not matched: Bug.T

6  catchAll2 F = 0
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This one is really bad, since it's warning about `Bug.T`, which should be hidden!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Patternmatch warnings for datatypes with COMPLETE sets break abstraction","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's a file:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ViewPatterns #}\r\nmodule Bug (Boolean(F, TooGoodToBeTrue), catchAll) where\r\n\r\ndata Boolean = F  T\r\n deriving Eq\r\n\r\npattern TooGoodToBeTrue :: Boolean\r\npattern TooGoodToBeTrue < ((== T) > True)\r\n where\r\n TooGoodToBeTrue = T\r\n{# COMPLETE F, TooGoodToBeTrue #}\r\n\r\ncatchAll :: Boolean > Int\r\ncatchAll F = 0\r\n catchAll TooGoodToBeTrue = 1\r\n}}}\r\n\r\nIf you compile this with `Wall`, the warning will warn about `T`, not `TooGoodToBeTrue` (the other conlike in the `COMPLETE` set):\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc fforcerecomp Wall Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘catchAll’: Patterns not matched: T\r\n \r\n15  catchAll F = 0\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nPerhaps this isn't so bad, since it's intramodule. But the problem persists even across modules:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nimport Bug\r\n\r\ncatchAll2 :: Boolean > Int\r\ncatchAll2 F = 0\r\n catchAll2 TooGoodToBeTrue = 1\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Bug.hs\r\n$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Wall Foo.hs\r\n\r\nFoo.hs:6:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘catchAll2’: Patterns not matched: Bug.T\r\n \r\n6  catchAll2 F = 0\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis one is really bad, since it's warning about `Bug.T`, which should be hidden!","type_of_failure":"OtherFailure","blocking":[]} >Here's a file:
```hs
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE ViewPatterns #}
module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where
data Boolean = F  T
deriving Eq
pattern TooGoodToBeTrue :: Boolean
pattern TooGoodToBeTrue < ((== T) > True)
where
TooGoodToBeTrue = T
{# COMPLETE F, TooGoodToBeTrue #}
catchAll :: Boolean > Int
catchAll F = 0
 catchAll TooGoodToBeTrue = 1
```
If you compile this with `Wall`, the warning will warn about `T`, not `TooGoodToBeTrue` (the other conlike in the `COMPLETE` set):
```
$ /opt/ghc/8.2.1/bin/ghc fforcerecomp Wall Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘catchAll’: Patterns not matched: T

15  catchAll F = 0
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Perhaps this isn't so bad, since it's intramodule. But the problem persists even across modules:
```hs
module Foo where
import Bug
catchAll2 :: Boolean > Int
catchAll2 F = 0
 catchAll2 TooGoodToBeTrue = 1
```
```
$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Bug.hs
$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Wall Foo.hs
Foo.hs:6:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘catchAll2’: Patterns not matched: Bug.T

6  catchAll2 F = 0
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This one is really bad, since it's warning about `Bug.T`, which should be hidden!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Patternmatch warnings for datatypes with COMPLETE sets break abstraction","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's a file:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE ViewPatterns #}\r\nmodule Bug (Boolean(F, TooGoodToBeTrue), catchAll) where\r\n\r\ndata Boolean = F  T\r\n deriving Eq\r\n\r\npattern TooGoodToBeTrue :: Boolean\r\npattern TooGoodToBeTrue < ((== T) > True)\r\n where\r\n TooGoodToBeTrue = T\r\n{# COMPLETE F, TooGoodToBeTrue #}\r\n\r\ncatchAll :: Boolean > Int\r\ncatchAll F = 0\r\n catchAll TooGoodToBeTrue = 1\r\n}}}\r\n\r\nIf you compile this with `Wall`, the warning will warn about `T`, not `TooGoodToBeTrue` (the other conlike in the `COMPLETE` set):\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc fforcerecomp Wall Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘catchAll’: Patterns not matched: T\r\n \r\n15  catchAll F = 0\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nPerhaps this isn't so bad, since it's intramodule. But the problem persists even across modules:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nimport Bug\r\n\r\ncatchAll2 :: Boolean > Int\r\ncatchAll2 F = 0\r\n catchAll2 TooGoodToBeTrue = 1\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Bug.hs\r\n$ /opt/ghc/8.2.1/bin/ghc fforcerecomp c Wall Foo.hs\r\n\r\nFoo.hs:6:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘catchAll2’: Patterns not matched: Bug.T\r\n \r\n6  catchAll2 F = 0\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis one is really bad, since it's warning about `Bug.T`, which should be hidden!","type_of_failure":"OtherFailure","blocking":[]} >Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/issues/13778explicitly bidirectional patterns should not report Recursive definition" whe...20190707T18:20:07ZGabor Greifexplicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression positionCompile this
```hs
pattern One < ((==One) > True)
where One = 1
```
I get
```
test.hs:1:1: error:
Recursive pattern synonym definition with following bindings:
One (defined at test.hs:(1,1)(1,15))

Compilation failed.
```
Note that the error is due to the usage in view pattern \*\*expression position\*\*.
But for *explicitly bidirectional* patterns, there is no recursivity going on. So this usage should be allowed.
I am testing with HEAD, but the issue is probably older.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"explicitly bidirectional patterns should not report Recursive definition\" when used in view pattern expression position","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compile this\r\n\r\n{{{#!hs\r\npattern One < ((==One) > True)\r\n where One = 1\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\ntest.hs:1:1: error: \r\n Recursive pattern synonym definition with following bindings:\r\n One (defined at test.hs:(1,1)(1,15))\r\n \r\nCompilation failed.\r\n}}}\r\n\r\nNote that the error is due to the usage in view pattern **expression position**.\r\n\r\nBut for ''explicitly bidirectional'' patterns, there is no recursivity going on. So this usage should be allowed.\r\n\r\nI am testing with HEAD, but the issue is probably older.","type_of_failure":"OtherFailure","blocking":[]} >Compile this
```hs
pattern One < ((==One) > True)
where One = 1
```
I get
```
test.hs:1:1: error:
Recursive pattern synonym definition with following bindings:
One (defined at test.hs:(1,1)(1,15))

Compilation failed.
```
Note that the error is due to the usage in view pattern \*\*expression position\*\*.
But for *explicitly bidirectional* patterns, there is no recursivity going on. So this usage should be allowed.
I am testing with HEAD, but the issue is probably older.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"explicitly bidirectional patterns should not report Recursive definition\" when used in view pattern expression position","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compile this\r\n\r\n{{{#!hs\r\npattern One < ((==One) > True)\r\n where One = 1\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\ntest.hs:1:1: error: \r\n Recursive pattern synonym definition with following bindings:\r\n One (defined at test.hs:(1,1)(1,15))\r\n \r\nCompilation failed.\r\n}}}\r\n\r\nNote that the error is due to the usage in view pattern **expression position**.\r\n\r\nBut for ''explicitly bidirectional'' patterns, there is no recursivity going on. So this usage should be allowed.\r\n\r\nI am testing with HEAD, but the issue is probably older.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc/issues/13717Pattern synonym exhaustiveness checks don't play well with EmptyCase20190816T16:36:39ZDavid FeuerPattern synonym exhaustiveness checks don't play well with EmptyCaseIn #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with `EmptyCase`. Suppose I write
```hs
newtype Fin (n :: Nat) = Fin Natural  constructor not exported
pattern FZ :: () => n ~ 'S m => Fin n
pattern FS :: () => n ~ 'S m => Fin m > Fin n
{# COMPLETE FZ, FS #}
```
I would very much like to be able to write
```hs
finZAbsurd :: Fin 'Z > Void
finZAbsurd x = case x of
```
but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this:
> When checking empty case, check that *at least one* complete pattern set is impossible.
In this case, it would see two complete pattern sets: the builtin `{Fin}` and the userdecreed `{FZ, FS}`. Since neither `FZ` nor `FS` have matching types, we should conclude that the empty case is fine.In #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with `EmptyCase`. Suppose I write
```hs
newtype Fin (n :: Nat) = Fin Natural  constructor not exported
pattern FZ :: () => n ~ 'S m => Fin n
pattern FS :: () => n ~ 'S m => Fin m > Fin n
{# COMPLETE FZ, FS #}
```
I would very much like to be able to write
```hs
finZAbsurd :: Fin 'Z > Void
finZAbsurd x = case x of
```
but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this:
> When checking empty case, check that *at least one* complete pattern set is impossible.
In this case, it would see two complete pattern sets: the builtin `{Fin}` and the userdecreed `{FZ, FS}`. Since neither `FZ` nor `FS` have matching types, we should conclude that the empty case is fine.8.10.1Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/issues/13572Add ArgMin / ArgMax pattern synonyms20190707T18:21:16ZIcelandjackAdd ArgMin / ArgMax pattern synonyms```hs
import Data.Semigroup
pattern ArgMin :: a > b > ArgMin a b
pattern ArgMin a b = Min (Arg a b)
pattern ArgMax :: a > b > ArgMax a b
pattern ArgMax a b = Max (Arg a b)
```
Or even record pattern synonyms, à la [this](https://github.com/energyflowanalysis/efa2.1/blob/3eb86c0b6b2d2fb66cd5b76ce5c0437d42f8cdf8/sandbox/delaunay/HalfPlaneMap.hs#L181)
```hs
pattern ArgMin :: a > b > ArgMin a b
pattern ArgMin {minArg, minValue} = Min (Arg minArg minValue)
pattern ArgMax :: a > b > ArgMax a b
pattern ArgMax {maxArg, maxValue} = Max (Arg maxArg maxValue)
```
and we can define
```hs
import Data.Semigroup.Foldable
argmin :: Ord k => Foldable1 f => (a > k) > (f a > a)
argmin f = minValue . foldMap1 (\a > ArgMin (f a) a)
argmax :: Ord k => Foldable1 f => (a > k) > (f a > a)
argmax f = maxValue . foldMap1 (\a > ArgMax (f a) a)
``````hs
import Data.Semigroup
pattern ArgMin :: a > b > ArgMin a b
pattern ArgMin a b = Min (Arg a b)
pattern ArgMax :: a > b > ArgMax a b
pattern ArgMax a b = Max (Arg a b)
```
Or even record pattern synonyms, à la [this](https://github.com/energyflowanalysis/efa2.1/blob/3eb86c0b6b2d2fb66cd5b76ce5c0437d42f8cdf8/sandbox/delaunay/HalfPlaneMap.hs#L181)
```hs
pattern ArgMin :: a > b > ArgMin a b
pattern ArgMin {minArg, minValue} = Min (Arg minArg minValue)
pattern ArgMax :: a > b > ArgMax a b
pattern ArgMax {maxArg, maxValue} = Max (Arg maxArg maxValue)
```
and we can define
```hs
import Data.Semigroup.Foldable
argmin :: Ord k => Foldable1 f => (a > k) > (f a > a)
argmin f = minValue . foldMap1 (\a > ArgMin (f a) a)
argmax :: Ord k => Foldable1 f => (a > k) > (f a > a)
argmax f = maxValue . foldMap1 (\a > ArgMax (f a) a)
```