GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20191204T16:50:34Zhttps://gitlab.haskell.org/ghc/ghc/issues/17535Pattern synonyms allow unlifted toplevel bindings  and they're thunks!20191204T16:50:34ZRichard Eisenbergrae@richarde.devPattern synonyms allow unlifted toplevel bindings  and they're thunks!Feeling like being abusive to GHC (and in thinking about https://github.com/ghcproposals/ghcproposals/pull/265), I gave it this:
```hs
{# LANGUAGE PatternSynonyms, MagicHash #}
module Main where
import Debug.Trace
import GHC.Exts
pattern Strange < 0#
where Strange = case trace "evaluating now" 0 of
I# n > n
main = do
putStrLn "Starting"
print (I# Strange)
```
Two strange things happened:
1. This program was accepted, despite the fact that `Strange` is a toplevel unlifted binding.
2. `Strange` is actually a thunk. I see `Starting` in the output before `evaluating now`.
As I was writing this up, I realized that I probably knew this, deep down, having seen the implementation of this all (where a magical `Void#` parameter is added to unlifted pattern synonyms). But this should, at least, be documented in the manual, where I could not find it in the pattern synonyms section.Feeling like being abusive to GHC (and in thinking about https://github.com/ghcproposals/ghcproposals/pull/265), I gave it this:
```hs
{# LANGUAGE PatternSynonyms, MagicHash #}
module Main where
import Debug.Trace
import GHC.Exts
pattern Strange < 0#
where Strange = case trace "evaluating now" 0 of
I# n > n
main = do
putStrLn "Starting"
print (I# Strange)
```
Two strange things happened:
1. This program was accepted, despite the fact that `Strange` is a toplevel unlifted binding.
2. `Strange` is actually a thunk. I see `Starting` in the output before `evaluating now`.
As I was writing this up, I realized that I probably knew this, deep down, having seen the implementation of this all (where a magical `Void#` parameter is added to unlifted pattern synonyms). But this should, at least, be documented in the manual, where I could not find it in the pattern synonyms section.https://gitlab.haskell.org/ghc/ghc/issues/17218Pattern match exhaustiveness check only suggets constructors from the vanilla...20191001T09:22:31ZSebastian GrafPattern match exhaustiveness check only suggets constructors from the vanilla COMPLETE setDue to how [`getUnmatchedConstructor` is implemented](https://gitlab.haskell.org/ghc/ghc/blob/4853d962289db1b32886ec73e824cd37c9c5c002/compiler/deSugar/PmOracle.hs#L137), we only suggest unmatched constructors from the vanilla COMPLETE set. Example:
```
{# LANGUAGE PatternSynonyms #}
module Lib where
data T = A  B  C
pattern P = B
{# COMPLETE A, P #}
f :: T > ()
f A = ()
```
Generated warning:
```
Pattern match(es) are nonexhaustive
In an equation for ‘f’:
Patterns not matched:
B
C

11  f A = ()
 ^^^^^^^^
```
But `C` would be enough here! It's hard to say what the user wants here. We could just print all different residual COMPLETE sets, I guess.Due to how [`getUnmatchedConstructor` is implemented](https://gitlab.haskell.org/ghc/ghc/blob/4853d962289db1b32886ec73e824cd37c9c5c002/compiler/deSugar/PmOracle.hs#L137), we only suggest unmatched constructors from the vanilla COMPLETE set. Example:
```
{# LANGUAGE PatternSynonyms #}
module Lib where
data T = A  B  C
pattern P = B
{# COMPLETE A, P #}
f :: T > ()
f A = ()
```
Generated warning:
```
Pattern match(es) are nonexhaustive
In an equation for ‘f’:
Patterns not matched:
B
C

11  f A = ()
 ^^^^^^^^
```
But `C` would be enough here! It's hard to say what the user wants here. We could just print all different residual COMPLETE sets, I guess.Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/issues/17207PatternSynonyms on data family and COMPLETE signature lead to incorrect warning20191018T09:07:09ZSebastian GrafPatternSynonyms on data family and COMPLETE signature lead to incorrect warningNote that the original test case below is fixed in !1903. There's a more obscure test case in https://gitlab.haskell.org/ghc/ghc/issues/17207#note_227180, that's why this ticket is still open.

Here's a whitebox test I came up with that shouldn't produce any warnings:
```haskell
{# OPTIONS_GHC Wincompletepatterns Wnomissingmethods fforcerecomp #}
{# LANGUAGE GADTs, TypeFamilies, PatternSynonyms #}
module Lib where
data family T a
data instance T () where
A :: T ()
B :: T ()
pattern C :: T ()
pattern C = B
{# COMPLETE A, C #}
g :: T () > ()
g A = ()
g C = ()
h :: T () > ()
h C = ()
h A = ()
```
Yet it currently (after !963) produces the following warning:
```
testcases/LateInitOfShapes.hs:16:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’: Patterns not matched: B

16  g A = ()
 ^^^^^^^^...
```
This is loosely related to the observation in https://gitlab.haskell.org/ghc/ghc/issues/14059#note_140372: The first match of `g` commits the type of the value abstraction to the representation TyCon of `T ()`, at which point we don't see the COMPLETE set that is attached to the family `T`. To my knowledge there is no way to get back to `T ()` from the representation TyCon (Edit: yes, there is. `tyConFamInst_maybe`, which !1903 does), so the only way to recover this would be to make sense of the `CoPat` surrounding the match on `A`. There was a ticket where we discussed how to adding a `CoPat` variant to `PmPat`, but I couldn't find it. It's #14899, but I no longer think the `CoPat` idea is relevant.Note that the original test case below is fixed in !1903. There's a more obscure test case in https://gitlab.haskell.org/ghc/ghc/issues/17207#note_227180, that's why this ticket is still open.

Here's a whitebox test I came up with that shouldn't produce any warnings:
```haskell
{# OPTIONS_GHC Wincompletepatterns Wnomissingmethods fforcerecomp #}
{# LANGUAGE GADTs, TypeFamilies, PatternSynonyms #}
module Lib where
data family T a
data instance T () where
A :: T ()
B :: T ()
pattern C :: T ()
pattern C = B
{# COMPLETE A, C #}
g :: T () > ()
g A = ()
g C = ()
h :: T () > ()
h C = ()
h A = ()
```
Yet it currently (after !963) produces the following warning:
```
testcases/LateInitOfShapes.hs:16:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’: Patterns not matched: B

16  g A = ()
 ^^^^^^^^...
```
This is loosely related to the observation in https://gitlab.haskell.org/ghc/ghc/issues/14059#note_140372: The first match of `g` commits the type of the value abstraction to the representation TyCon of `T ()`, at which point we don't see the COMPLETE set that is attached to the family `T`. To my knowledge there is no way to get back to `T ()` from the representation TyCon (Edit: yes, there is. `tyConFamInst_maybe`, which !1903 does), so the only way to recover this would be to make sense of the `CoPat` surrounding the match on `A`. There was a ticket where we discussed how to adding a `CoPat` variant to `PmPat`, but I couldn't find it. It's #14899, but I no longer think the `CoPat` idea is relevant.Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/issues/17178Levity Polymorphic Pattern Synonyms20190912T22:38:32ZAndrew MartinLevity Polymorphic Pattern SynonymsGHC currently rejects the following program:
pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
pattern Just# a = (#  a #)
With this error message (the line number reference is the one where the signature of the pattern synonym is given):
A levitypolymorphic type is not allowed here:
Type: a
Kind: TYPE r

26  pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
I would like for GHC to accept this pattern synonym. I think that it should just be possible to remove the levitypolymorphism check from pattern synonym signatures. I don't this can lead to any unsoundness since patterns are just expanded in Core.GHC currently rejects the following program:
pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
pattern Just# a = (#  a #)
With this error message (the line number reference is the one where the signature of the pattern synonym is given):
A levitypolymorphic type is not allowed here:
Type: a
Kind: TYPE r

26  pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
I would like for GHC to accept this pattern synonym. I think that it should just be possible to remove the levitypolymorphism check from pattern synonym signatures. I don't this can lead to any unsoundness since patterns are just expanded in Core.https://gitlab.haskell.org/ghc/ghc/issues/17176Duplicate Record Fields do not work properly with Record Pattern Synonyms20191017T21:59:16ZDaniel WinogradCortDuplicate Record Fields do not work properly with Record Pattern Synonyms## Summary
Duplicate Record Fields do not work properly with Record Pattern Synonyms.
## Steps to reproduce
When I evaluate the following module in GHC 8.4.4:
```haskell
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE DuplicateRecordFields #}
module Test where
data Foo =
Bar { bar :: Int }
 BadBaz { baz :: Int }
pattern Baz :: Int > Foo
pattern Baz{baz} = BadBaz baz
```
I get the following error message.
```
Test.hs:10:13: error:
Multiple declarations of ‘baz’
Declared at: Test.hs:7:14
Test.hs:10:13

10  pattern Baz{baz} = BadBaz baz
```
## Expected behavior
Although pattern records aren't _exactly_ records, I would expect `DuplicateRecordFields` to work properly here and allow both declarations.
## Environment
* GHC version used: GHC 8.4.4.## Summary
Duplicate Record Fields do not work properly with Record Pattern Synonyms.
## Steps to reproduce
When I evaluate the following module in GHC 8.4.4:
```haskell
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE DuplicateRecordFields #}
module Test where
data Foo =
Bar { bar :: Int }
 BadBaz { baz :: Int }
pattern Baz :: Int > Foo
pattern Baz{baz} = BadBaz baz
```
I get the following error message.
```
Test.hs:10:13: error:
Multiple declarations of ‘baz’
Declared at: Test.hs:7:14
Test.hs:10:13

10  pattern Baz{baz} = BadBaz baz
```
## Expected behavior
Although pattern records aren't _exactly_ records, I would expect `DuplicateRecordFields` to work properly here and allow both declarations.
## Environment
* GHC version used: GHC 8.4.4.8.10.1https://gitlab.haskell.org/ghc/ghc/issues/17098Document how to write a pattern synonym that uses a view pattern20190822T15:44:46ZSimon JakobiDocument how to write a pattern synonym that uses a view patternIt took me a bit to figure out how to apply a function to the expression that I want to pattern match on – turns out you can use `ViewPatterns`, as for example `containers`' `Seq` does:
```
pattern (:<) :: a > Seq a > Seq a
pattern x :< xs < (viewl > x :< xs)
where
x :< xs = x < xs
```
I think this should be documented in [the user's guide](https://gitlab.haskell.org/ghc/ghc/blob/5e40356f65bc2d62c73be8015c759899f072ac9a/docs/users_guide/glasgow_exts.rst#L5433).It took me a bit to figure out how to apply a function to the expression that I want to pattern match on – turns out you can use `ViewPatterns`, as for example `containers`' `Seq` does:
```
pattern (:<) :: a > Seq a > Seq a
pattern x :< xs < (viewl > x :< xs)
where
x :< xs = x < xs
```
I think this should be documented in [the user's guide](https://gitlab.haskell.org/ghc/ghc/blob/5e40356f65bc2d62c73be8015c759899f072ac9a/docs/users_guide/glasgow_exts.rst#L5433).8.10.1https://gitlab.haskell.org/ghc/ghc/issues/17095A shorter COMPLETE pragma syntax for pattern synonyms that replace specific c...20190822T15:21:27ZSimon JakobiA shorter COMPLETE pragma syntax for pattern synonyms that replace specific constructorsIf I have a data type with many constructors and a pattern synonym that can be used instead of a single constructor, I currently have to list all the remaining constructors in the `COMPLETE` pragma. This is onerous, unreadable, and requires that I update the `COMPLETE` pragma whenever I add another constructor.
```
{# language PatternSynonyms #}
module M where
data D = C1  C2  C3  and so forth
{# COMPLETE P, C2, C3 ... #}
pattern P = C1
```
Instead I would like to concisely describe the constructors that my pattern synonym can substitute. For example:
```
{# SUBSTITUTE P (C1) #}
pattern P = C1
```
If a pattern synonym substitutes multiple constructors it could look like this:
```
{# SUBSTITUTE P (C1, C2) #}
```If I have a data type with many constructors and a pattern synonym that can be used instead of a single constructor, I currently have to list all the remaining constructors in the `COMPLETE` pragma. This is onerous, unreadable, and requires that I update the `COMPLETE` pragma whenever I add another constructor.
```
{# language PatternSynonyms #}
module M where
data D = C1  C2  C3  and so forth
{# COMPLETE P, C2, C3 ... #}
pattern P = C1
```
Instead I would like to concisely describe the constructors that my pattern synonym can substitute. For example:
```
{# SUBSTITUTE P (C1) #}
pattern P = C1
```
If a pattern synonym substitutes multiple constructors it could look like this:
```
{# SUBSTITUTE P (C1, C2) #}
```8.10.1https://gitlab.haskell.org/ghc/ghc/issues/17094Document that bundled pattern synonyms have only been supported since 8.0.120190822T15:21:05ZSimon JakobiDocument that bundled pattern synonyms have only been supported since 8.0.1Bundled pattern synonyms like in the example below have only been supported since `8.0.1`.
```
{# language PatternSynonyms #}
module Lib (D(P)) where
data D = C
pattern P = C
```
The [current documentation](https://gitlab.haskell.org/ghc/ghc/blob/5e40356f65bc2d62c73be8015c759899f072ac9a/docs/users_guide/glasgow_exts.rst#L57315746) is in a section marked `:since: 7.8.1`, which seems to imply that bundled exports have also been available since `7.8.1`.Bundled pattern synonyms like in the example below have only been supported since `8.0.1`.
```
{# language PatternSynonyms #}
module Lib (D(P)) where
data D = C
pattern P = C
```
The [current documentation](https://gitlab.haskell.org/ghc/ghc/blob/5e40356f65bc2d62c73be8015c759899f072ac9a/docs/users_guide/glasgow_exts.rst#L57315746) is in a section marked `:since: 7.8.1`, which seems to imply that bundled exports have also been available since `7.8.1`.8.10.1https://gitlab.haskell.org/ghc/ghc/issues/16957COMPLETE sets don't get typechecked20190828T15:31:49ZSebastian 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/14630name shadowing warnings by record pattern synonyms + RecordWildCards or Named...20190910T22:13:54Zmizunashi_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:05ZEdward Kmett{# 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:06ZEdward Kmett{# 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/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":[]} >