GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200530T20:42:20Zhttps://gitlab.haskell.org/ghc/ghc//issues/9671Allow expressions in patterns20200530T20:42:20ZIcelandjackAllow expressions in patternsI've outlined a proposal for extending pattern synonyms to depend on terms (PatternFamilies), the name is less than ideal but I'll keep the page under that name for now. The proposal's introduction has been rewritten.
The simplest use case are patterns that matches only when a set contains an element (`IsMember`) or when a set does not contain an element (`NotMember`):
\[\[Image(wiki:PatternFamilies:member.png)\]\]
```hs
hasKeys :: Set Item > IO ()
hasKeys (IsMember "keys") = leaveHouse
hasKeys (NotMember "keys") = findKeys >> leaveHouse
```
or a pattern that matches a map if the key exists:
\[\[Image(wiki:PatternFamilies:lookup.png)\]\]
used like this:
```hs
age :: Map Person Age > String
age (Lookup "Alice" 60) = "Alice is 60 years old!"
age (Lookup "Alice" age) = "Alice is " ++ show age ++ "."
age (Lookup "Bob" _) = "No info on Alice but we know how old Bob is."
age _ = "..."
```
Further details and examples can be found here: PatternFamilies, I discussed it with several people ICFP 2014. This would not require a new extension but would extend PatternSynonyms. This feature can be quite useful, especially when working with deeply nested structures (ASTs, JSON, XML, ...).
If people are fine with it I will implement it.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow expressions in patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":["pattern","patterns,","synonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I've outlined a proposal for extending pattern synonyms to depend on terms (PatternFamilies), the name is less than ideal but I'll keep the page under that name for now. The proposal's introduction has been rewritten.\r\n\r\nThe simplest use case are patterns that matches only when a set contains an element (`IsMember`) or when a set does not contain an element (`NotMember`):\r\n\r\n[[Image(wiki:PatternFamilies:member.png)]]\r\n\r\n{{{#!hs\r\n hasKeys :: Set Item > IO ()\r\n hasKeys (IsMember \"keys\") = leaveHouse\r\n hasKeys (NotMember \"keys\") = findKeys >> leaveHouse\r\n}}}\r\n\r\nor a pattern that matches a map if the key exists:\r\n\r\n[[Image(wiki:PatternFamilies:lookup.png)]]\r\n\r\nused like this:\r\n\r\n{{{#!hs\r\n age :: Map Person Age > String\r\n age (Lookup \"Alice\" 60) = \"Alice is 60 years old!\"\r\n age (Lookup \"Alice\" age) = \"Alice is \" ++ show age ++ \".\"\r\n age (Lookup \"Bob\" _) = \"No info on Alice but we know how old Bob is.\"\r\n age _ = \"...\"\r\n}}}\r\n\r\nFurther details and examples can be found here: PatternFamilies, I discussed it with several people ICFP 2014. This would not require a new extension but would extend PatternSynonyms. This feature can be quite useful, especially when working with deeply nested structures (ASTs, JSON, XML, ...).\r\n\r\nIf people are fine with it I will implement it.","type_of_failure":"OtherFailure","blocking":[]} >I've outlined a proposal for extending pattern synonyms to depend on terms (PatternFamilies), the name is less than ideal but I'll keep the page under that name for now. The proposal's introduction has been rewritten.
The simplest use case are patterns that matches only when a set contains an element (`IsMember`) or when a set does not contain an element (`NotMember`):
\[\[Image(wiki:PatternFamilies:member.png)\]\]
```hs
hasKeys :: Set Item > IO ()
hasKeys (IsMember "keys") = leaveHouse
hasKeys (NotMember "keys") = findKeys >> leaveHouse
```
or a pattern that matches a map if the key exists:
\[\[Image(wiki:PatternFamilies:lookup.png)\]\]
used like this:
```hs
age :: Map Person Age > String
age (Lookup "Alice" 60) = "Alice is 60 years old!"
age (Lookup "Alice" age) = "Alice is " ++ show age ++ "."
age (Lookup "Bob" _) = "No info on Alice but we know how old Bob is."
age _ = "..."
```
Further details and examples can be found here: PatternFamilies, I discussed it with several people ICFP 2014. This would not require a new extension but would extend PatternSynonyms. This feature can be quite useful, especially when working with deeply nested structures (ASTs, JSON, XML, ...).
If people are fine with it I will implement it.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow expressions in patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":["pattern","patterns,","synonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I've outlined a proposal for extending pattern synonyms to depend on terms (PatternFamilies), the name is less than ideal but I'll keep the page under that name for now. The proposal's introduction has been rewritten.\r\n\r\nThe simplest use case are patterns that matches only when a set contains an element (`IsMember`) or when a set does not contain an element (`NotMember`):\r\n\r\n[[Image(wiki:PatternFamilies:member.png)]]\r\n\r\n{{{#!hs\r\n hasKeys :: Set Item > IO ()\r\n hasKeys (IsMember \"keys\") = leaveHouse\r\n hasKeys (NotMember \"keys\") = findKeys >> leaveHouse\r\n}}}\r\n\r\nor a pattern that matches a map if the key exists:\r\n\r\n[[Image(wiki:PatternFamilies:lookup.png)]]\r\n\r\nused like this:\r\n\r\n{{{#!hs\r\n age :: Map Person Age > String\r\n age (Lookup \"Alice\" 60) = \"Alice is 60 years old!\"\r\n age (Lookup \"Alice\" age) = \"Alice is \" ++ show age ++ \".\"\r\n age (Lookup \"Bob\" _) = \"No info on Alice but we know how old Bob is.\"\r\n age _ = \"...\"\r\n}}}\r\n\r\nFurther details and examples can be found here: PatternFamilies, I discussed it with several people ICFP 2014. This would not require a new extension but would extend PatternSynonyms. This feature can be quite useful, especially when working with deeply nested structures (ASTs, JSON, XML, ...).\r\n\r\nIf people are fine with it I will implement it.","type_of_failure":"OtherFailure","blocking":[]} >8.0.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/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/17098Document how to write a pattern synonym that uses a view pattern20200123T18:14:56ZSimon 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).9.0.1https://gitlab.haskell.org/ghc/ghc//issues/15416Higher rank types in pattern synonyms20200123T19:16:21ZmniipHigher 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":[]} >9.0.1https://gitlab.haskell.org/ghc/ghc//issues/12178Allow inline pragmas on pattern synonyms20200123T18:29:42ZMatthew PickeringAllow inline pragmas on pattern synonymsRichard observes that it might be useful to allow inline pragmas to refer to pattern synonyms to ensure that
the matcher is inlined.
The main question to resolve is whether `{# INLINE P #}` means to inline just the matcher, just the builder
or both. It seems that without more fine grained control then the pragma should cause both the matcher and builder to be inline but I am not certain about this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow inline pragmas on pattern synonyms","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":"FeatureRequest","description":"Richard observes that it might be useful to allow inline pragmas to refer to pattern synonyms to ensure that\r\nthe matcher is inlined. \r\n\r\nThe main question to resolve is whether `{# INLINE P #}` means to inline just the matcher, just the builder\r\nor both. It seems that without more fine grained control then the pragma should cause both the matcher and builder to be inline but I am not certain about this. ","type_of_failure":"OtherFailure","blocking":[]} >Richard observes that it might be useful to allow inline pragmas to refer to pattern synonyms to ensure that
the matcher is inlined.
The main question to resolve is whether `{# INLINE P #}` means to inline just the matcher, just the builder
or both. It seems that without more fine grained control then the pragma should cause both the matcher and builder to be inline but I am not certain about this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow inline pragmas on pattern synonyms","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":"FeatureRequest","description":"Richard observes that it might be useful to allow inline pragmas to refer to pattern synonyms to ensure that\r\nthe matcher is inlined. \r\n\r\nThe main question to resolve is whether `{# INLINE P #}` means to inline just the matcher, just the builder\r\nor both. It seems that without more fine grained control then the pragma should cause both the matcher and builder to be inline but I am not certain about this. ","type_of_failure":"OtherFailure","blocking":[]} >9.0.1https://gitlab.haskell.org/ghc/ghc//issues/18247ddumpminimalimports does not dump some pattern imports correctly20200714T14:17:10Zjrp2014ddumpminimalimports does not dump some pattern imports correctly## Summary
The minimal imports generated by `ddumpminimalimports` are sometimes not correct.
For example, it generates `import Agda.Utils.List1 ( pattern (:) )` correctly, but doesn't include the `pattern` keyword for `Def` in `import qualified Agda.Syntax.Abstract as A ( QName, NameToExpr(nameToExpr), Expr(Con), Def )`, where `Def` is defined in the `Agda.Syntax.Abstract` module as:
```haskell
  Pattern synonym for regular Def
pattern Def :: QName > Expr
pattern Def x = Def' x NoSuffix
```
This limits the utility of the feature.
## Environment
* GHC version used: 8.10.1
* OS; MacOS Catalina## Summary
The minimal imports generated by `ddumpminimalimports` are sometimes not correct.
For example, it generates `import Agda.Utils.List1 ( pattern (:) )` correctly, but doesn't include the `pattern` keyword for `Def` in `import qualified Agda.Syntax.Abstract as A ( QName, NameToExpr(nameToExpr), Expr(Con), Def )`, where `Def` is defined in the `Agda.Syntax.Abstract` module as:
```haskell
  Pattern synonym for regular Def
pattern Def :: QName > Expr
pattern Def x = Def' x NoSuffix
```
This limits the utility of the feature.
## Environment
* GHC version used: 8.10.1
* OS; MacOS Catalina8.10.2Alan ZimmermanAlan Zimmermanhttps://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/11959Importing doubly exported pattern synonym and associated pattern synonym panics20190707T18:28:15ZdarchonImporting doubly exported pattern synonym and associated pattern synonym panicsGiven
```hs
{# LANGUAGE PatternSynonyms, ViewPatterns #}
module Pat (Vec2(Nil,(:>)), pattern (:>)) where
newtype Vec2 a = Vec2 {unvec2 :: [a]}
pattern Nil :: Vec2 a
pattern Nil = Vec2 []
pattern (:>) x xs < ((\ys > (head $ unvec2 ys,Vec2 . tail $ unvec2 ys)) > (x,xs))
where
(:>) x xs = Vec2 (x:unvec2 xs)
```
and
```hs
{# LANGUAGE PatternSynonyms #}
module Main where
import Pat (Vec2(..),pattern (:>))
```
I get:
```
$ ghci Main.hs
GHCi, version 8.0.0.20160411: http://www.haskell.org/ghc/ :? for help
[1 of 2] Compiling Pat ( Pat.hs, interpreted )
Pat.hs:2:29: warning: [Wduplicateexports]
‘:>’ is exported by ‘(:>)’ and ‘Vec2(Nil, type (:>))’
[2 of 2] Compiling Main ( Main.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.0.20160411 for x86_64unknownlinux):
filterImports/combine
(:>, :>, Nothing)
(:>, Vec2{Vec2, :>, Nil}, Nothing)
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Now, the warning about the duplicate export is of course correct. But the panic shouldn't happen when I try to import both the associated pattern synonym and the normal pattern synonym.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1rc3 
 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":"Importing doubly exported pattern synonym and associated pattern synonym panics","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1rc3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Given\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms, ViewPatterns #}\r\nmodule Pat (Vec2(Nil,(:>)), pattern (:>)) where\r\n\r\nnewtype Vec2 a = Vec2 {unvec2 :: [a]}\r\n\r\npattern Nil :: Vec2 a\r\npattern Nil = Vec2 []\r\n\r\npattern (:>) x xs < ((\\ys > (head $ unvec2 ys,Vec2 . tail $ unvec2 ys)) > (x,xs))\r\n where\r\n (:>) x xs = Vec2 (x:unvec2 xs)\r\n}}}\r\n\r\nand\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Main where\r\n\r\nimport Pat (Vec2(..),pattern (:>))\r\n}}}\r\n\r\nI get:\r\n\r\n{{{\r\n$ ghci Main.hs \r\nGHCi, version 8.0.0.20160411: http://www.haskell.org/ghc/ :? for help\r\n[1 of 2] Compiling Pat ( Pat.hs, interpreted )\r\n\r\nPat.hs:2:29: warning: [Wduplicateexports]\r\n ‘:>’ is exported by ‘(:>)’ and ‘Vec2(Nil, type (:>))’\r\n[2 of 2] Compiling Main ( Main.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.0.20160411 for x86_64unknownlinux):\r\n\tfilterImports/combine\r\n (:>, :>, Nothing)\r\n (:>, Vec2{Vec2, :>, Nil}, Nothing)\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nNow, the warning about the duplicate export is of course correct. But the panic shouldn't happen when I try to import both the associated pattern synonym and the normal pattern synonym.","type_of_failure":"OtherFailure","blocking":[]} >Given
```hs
{# LANGUAGE PatternSynonyms, ViewPatterns #}
module Pat (Vec2(Nil,(:>)), pattern (:>)) where
newtype Vec2 a = Vec2 {unvec2 :: [a]}
pattern Nil :: Vec2 a
pattern Nil = Vec2 []
pattern (:>) x xs < ((\ys > (head $ unvec2 ys,Vec2 . tail $ unvec2 ys)) > (x,xs))
where
(:>) x xs = Vec2 (x:unvec2 xs)
```
and
```hs
{# LANGUAGE PatternSynonyms #}
module Main where
import Pat (Vec2(..),pattern (:>))
```
I get:
```
$ ghci Main.hs
GHCi, version 8.0.0.20160411: http://www.haskell.org/ghc/ :? for help
[1 of 2] Compiling Pat ( Pat.hs, interpreted )
Pat.hs:2:29: warning: [Wduplicateexports]
‘:>’ is exported by ‘(:>)’ and ‘Vec2(Nil, type (:>))’
[2 of 2] Compiling Main ( Main.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.0.20160411 for x86_64unknownlinux):
filterImports/combine
(:>, :>, Nothing)
(:>, Vec2{Vec2, :>, Nil}, Nothing)
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Now, the warning about the duplicate export is of course correct. But the panic shouldn't happen when I try to import both the associated pattern synonym and the normal pattern synonym.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1rc3 
 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":"Importing doubly exported pattern synonym and associated pattern synonym panics","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1rc3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Given\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms, ViewPatterns #}\r\nmodule Pat (Vec2(Nil,(:>)), pattern (:>)) where\r\n\r\nnewtype Vec2 a = Vec2 {unvec2 :: [a]}\r\n\r\npattern Nil :: Vec2 a\r\npattern Nil = Vec2 []\r\n\r\npattern (:>) x xs < ((\\ys > (head $ unvec2 ys,Vec2 . tail $ unvec2 ys)) > (x,xs))\r\n where\r\n (:>) x xs = Vec2 (x:unvec2 xs)\r\n}}}\r\n\r\nand\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Main where\r\n\r\nimport Pat (Vec2(..),pattern (:>))\r\n}}}\r\n\r\nI get:\r\n\r\n{{{\r\n$ ghci Main.hs \r\nGHCi, version 8.0.0.20160411: http://www.haskell.org/ghc/ :? for help\r\n[1 of 2] Compiling Pat ( Pat.hs, interpreted )\r\n\r\nPat.hs:2:29: warning: [Wduplicateexports]\r\n ‘:>’ is exported by ‘(:>)’ and ‘Vec2(Nil, type (:>))’\r\n[2 of 2] Compiling Main ( Main.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.0.20160411 for x86_64unknownlinux):\r\n\tfilterImports/combine\r\n (:>, :>, Nothing)\r\n (:>, Vec2{Vec2, :>, Nil}, Nothing)\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nNow, the warning about the duplicate export is of course correct. But the panic shouldn't happen when I try to import both the associated pattern synonym and the normal pattern synonym.","type_of_failure":"OtherFailure","blocking":[]} >8.2.3https://gitlab.haskell.org/ghc/ghc//issues/18466Poor errors around importing pattern synonyms20200717T10:07:43ZRichard Eisenbergrae@richarde.devPoor errors around importing pattern synonymsInspired by https://mail.haskell.org/pipermail/ghcdevs/2020July/019048.html, by @erikd.
When compiling
```hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern Nada = Nothing
```
```hs
module B where
import A ()
nil = Nada
```
GHC reports
```
B.hs:5:7: error:
• Data constructor not in scope: Nada
• Perhaps you want to add ‘Nada’ to the import list
in the import of ‘A’ (B.hs:3:111).

5  nil = Nada
 ^^^^
```
This is downright wrong: `Nada` is not a data constructor. It's a pattern synonym. But maybe I don't know that. So I try
```hs
module B where
import A (Nada)
nil = Nada
```
Now GHC says
```
B.hs:3:11: error: Module ‘A’ does not export ‘Nada’

3  import A (Nada)
 ^^^^
```
which is unhelpful, as `A` really *does* export `Nada`  just not as a type (which is what my import spec is asking for). In a flash of inspiration, say, I try
```hs
module B where
import A (pattern Nada)
nil = Nada
```
which leads to
```
B.hs:3:19: error: parse error on input ‘Nada’

3  import A (pattern Nada)
 ^^^^
```
The problem is that I haven't enabled the right extension, `PatternSynonyms`. Finally,
```hs
{# LANGUAGE PatternSynonyms #}
module B where
import A (pattern Nada)
nil = Nada
```
does the trick.
I thus see four bugs here:
 [ ] GHC assumes that a capitalized identifier in an expression (maybe a pattern? didn't try) is a data constructor. It might not be. We can generalize the error message.
 [ ] If GHC has figured out that the solution is to add an identifier to an import list (and the identifier is a pattern synonym), it should recommend `PatternSynonyms` and the `pattern` prefix.
 [ ] If an import item names a pattern synonym but forgets the `pattern` prefix (assuming there is no type of the same name), GHC should suggest `PatternSynonyms` and the `pattern` prefix.
 [ ] If the `pattern` prefix is present but `PatternSynonyms` is not enabled, GHC should suggest `PatternSynonyms` instead of just failing with a parse error.
To be concrete, here are my proposed new error messages:
```
B.hs:5:7: error:
• Data constructor or pattern synonym not in scope: Nada
• Perhaps you want to add ‘pattern Nada’ to the import list
in the import of ‘A’ (B.hs:3:111).
You would need to enable PatternSynonyms.

5  nil = Nada
 ^^^^
```
```
B.hs:3:11: error:
• Module ‘A’ does not export type ‘Nada’
Perhaps you meant to import ‘pattern Nada’?
You would need to enable PatternSynonyms.

3  import A (Nada)
 ^^^^
```
```
B.hs:3:19: error:
• parse error on input ‘Nada’
Did you want to enable PatternSynonyms?

3  import A (pattern Nada)

```
@erikd Would these be better for you?Inspired by https://mail.haskell.org/pipermail/ghcdevs/2020July/019048.html, by @erikd.
When compiling
```hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern Nada = Nothing
```
```hs
module B where
import A ()
nil = Nada
```
GHC reports
```
B.hs:5:7: error:
• Data constructor not in scope: Nada
• Perhaps you want to add ‘Nada’ to the import list
in the import of ‘A’ (B.hs:3:111).

5  nil = Nada
 ^^^^
```
This is downright wrong: `Nada` is not a data constructor. It's a pattern synonym. But maybe I don't know that. So I try
```hs
module B where
import A (Nada)
nil = Nada
```
Now GHC says
```
B.hs:3:11: error: Module ‘A’ does not export ‘Nada’

3  import A (Nada)
 ^^^^
```
which is unhelpful, as `A` really *does* export `Nada`  just not as a type (which is what my import spec is asking for). In a flash of inspiration, say, I try
```hs
module B where
import A (pattern Nada)
nil = Nada
```
which leads to
```
B.hs:3:19: error: parse error on input ‘Nada’

3  import A (pattern Nada)
 ^^^^
```
The problem is that I haven't enabled the right extension, `PatternSynonyms`. Finally,
```hs
{# LANGUAGE PatternSynonyms #}
module B where
import A (pattern Nada)
nil = Nada
```
does the trick.
I thus see four bugs here:
 [ ] GHC assumes that a capitalized identifier in an expression (maybe a pattern? didn't try) is a data constructor. It might not be. We can generalize the error message.
 [ ] If GHC has figured out that the solution is to add an identifier to an import list (and the identifier is a pattern synonym), it should recommend `PatternSynonyms` and the `pattern` prefix.
 [ ] If an import item names a pattern synonym but forgets the `pattern` prefix (assuming there is no type of the same name), GHC should suggest `PatternSynonyms` and the `pattern` prefix.
 [ ] If the `pattern` prefix is present but `PatternSynonyms` is not enabled, GHC should suggest `PatternSynonyms` instead of just failing with a parse error.
To be concrete, here are my proposed new error messages:
```
B.hs:5:7: error:
• Data constructor or pattern synonym not in scope: Nada
• Perhaps you want to add ‘pattern Nada’ to the import list
in the import of ‘A’ (B.hs:3:111).
You would need to enable PatternSynonyms.

5  nil = Nada
 ^^^^
```
```
B.hs:3:11: error:
• Module ‘A’ does not export type ‘Nada’
Perhaps you meant to import ‘pattern Nada’?
You would need to enable PatternSynonyms.

3  import A (Nada)
 ^^^^
```
```
B.hs:3:19: error:
• parse error on input ‘Nada’
Did you want to enable PatternSynonyms?

3  import A (pattern Nada)

```
@erikd Would these be better for you?https://gitlab.haskell.org/ghc/ghc//issues/18452Pattern synonyms and record selectors20200717T10:13:20ZSimon Peyton JonesPattern synonyms and record selectorsConsider this
```
{# LANGUAGE PatternSynonyms, ExistentialQuantification #}
module ExQuant where
data Showable = forall a . Show a => Showable { fs :: a }
pattern Nasty{fn} = Showable fn
qux1 = fs (Showable True)
qux2 = fn (Showable True)
```
I have discovered that in `qux2`, the use of `fn` is a `HsVar`, not a `HsRecFld` as it should be. And the occurrence of `fs` in `qux1` is indeed a `HsFld`.
I'm not sure of the consequences, but it looks inconsistent and wrong.Consider this
```
{# LANGUAGE PatternSynonyms, ExistentialQuantification #}
module ExQuant where
data Showable = forall a . Show a => Showable { fs :: a }
pattern Nasty{fn} = Showable fn
qux1 = fs (Showable True)
qux2 = fn (Showable True)
```
I have discovered that in `qux2`, the use of `fn` is a `HsVar`, not a `HsRecFld` as it should be. And the occurrence of `fs` in `qux1` is indeed a `HsFld`.
I'm not sure of the consequences, but it looks inconsistent and wrong.https://gitlab.haskell.org/ghc/ghc//issues/18371COMPLETE sets don't interact well with type familyreturning pattern synonyms20200803T16:59:56ZRyan ScottCOMPLETE sets don't interact well with type familyreturning pattern synonyms_Originally reported by greatBigDot628 [here](https://www.reddit.com/r/haskell/comments/gu2ovt/monthly_hask_anything_june_2020/fvhfw0n/)._
`COMPLETE` sets don't quite appear to work when a pattern synonym in the set returns a type family. Consider the following example of this:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE ViewPatterns #}
{# OPTIONS_GHC Wincompletepatterns #}
module Bug where
import Data.Kind
import Unsafe.Coerce
type family Sing :: k > Type
class SingI a where
sing :: Sing a
data SingInstance :: forall k. k > Type where
SingInstance :: SingI a => SingInstance a
newtype DI (a :: k) = Don'tInstantiate (SingI a => SingInstance a)
singInstance :: forall k (a :: k). Sing a > SingInstance a
singInstance s = with_sing_i SingInstance
where
with_sing_i :: (SingI a => SingInstance a) > SingInstance a
with_sing_i si = unsafeCoerce (Don'tInstantiate si) s
{# COMPLETE Sing #}
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
pattern Sing < (singInstance > SingInstance)
where Sing = sing

data SBool :: Bool > Type where
SFalse :: SBool False
STrue :: SBool True
type instance Sing = SBool
f :: SBool b > ()
f Sing = ()
g :: Sing (b :: Bool) > ()
g Sing = ()
```
If you compile this with GHC 8.10.1 or HEAD, it will report `f` and `g` as nonexhaustive, despite the fact that they match on the `Sing` `COMPLETE` set:
```
$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:43:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘f’:
Patterns not matched:
SFalse
STrue

43  f Sing = ()
 ^^^^^^^^^^^
Bug.hs:46:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’:
Patterns not matched:
SFalse
STrue

46  g Sing = ()
 ^^^^^^^^^^^
```
This appears to be a regression from GHC 8.8.3, which does not report any warnings at all.
The fact that the `Sing` pattern synonym returns a type family appears to be crucial. If you define a variant of `Sing` that returns a concrete data type, for instance:
```hs
{# COMPLETE SingBool #}
pattern SingBool :: forall (b :: Bool). () => SingI b => SBool b
pattern SingBool = Sing
fSingBool :: SBool b > ()
fSingBool SingBool = ()
gSingBool :: Sing (b :: Bool) > ()
gSingBool SingBool = ()
```
Then the warnings go away. cc @sgraf812_Originally reported by greatBigDot628 [here](https://www.reddit.com/r/haskell/comments/gu2ovt/monthly_hask_anything_june_2020/fvhfw0n/)._
`COMPLETE` sets don't quite appear to work when a pattern synonym in the set returns a type family. Consider the following example of this:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE ViewPatterns #}
{# OPTIONS_GHC Wincompletepatterns #}
module Bug where
import Data.Kind
import Unsafe.Coerce
type family Sing :: k > Type
class SingI a where
sing :: Sing a
data SingInstance :: forall k. k > Type where
SingInstance :: SingI a => SingInstance a
newtype DI (a :: k) = Don'tInstantiate (SingI a => SingInstance a)
singInstance :: forall k (a :: k). Sing a > SingInstance a
singInstance s = with_sing_i SingInstance
where
with_sing_i :: (SingI a => SingInstance a) > SingInstance a
with_sing_i si = unsafeCoerce (Don'tInstantiate si) s
{# COMPLETE Sing #}
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
pattern Sing < (singInstance > SingInstance)
where Sing = sing

data SBool :: Bool > Type where
SFalse :: SBool False
STrue :: SBool True
type instance Sing = SBool
f :: SBool b > ()
f Sing = ()
g :: Sing (b :: Bool) > ()
g Sing = ()
```
If you compile this with GHC 8.10.1 or HEAD, it will report `f` and `g` as nonexhaustive, despite the fact that they match on the `Sing` `COMPLETE` set:
```
$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:43:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘f’:
Patterns not matched:
SFalse
STrue

43  f Sing = ()
 ^^^^^^^^^^^
Bug.hs:46:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’:
Patterns not matched:
SFalse
STrue

46  g Sing = ()
 ^^^^^^^^^^^
```
This appears to be a regression from GHC 8.8.3, which does not report any warnings at all.
The fact that the `Sing` pattern synonym returns a type family appears to be crucial. If you define a variant of `Sing` that returns a concrete data type, for instance:
```hs
{# COMPLETE SingBool #}
pattern SingBool :: forall (b :: Bool). () => SingI b => SBool b
pattern SingBool = Sing
fSingBool :: SBool b > ()
fSingBool SingBool = ()
gSingBool :: Sing (b :: Bool) > ()
gSingBool SingBool = ()
```
Then the warnings go away. cc @sgraf812https://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 warning20200803T16:59:55ZSebastian 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.https://gitlab.haskell.org/ghc/ghc//issues/17178Levity Polymorphic Pattern Synonyms20200217T14:51:54ZAndrew 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 Synonyms20200715T08:00:46ZDaniel 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.https://gitlab.haskell.org/ghc/ghc//issues/17095A shorter COMPLETE pragma syntax for pattern synonyms that replace specific c...20200123T19:42:31ZSimon 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) #}
```https://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/16595GHC is overly lax when typechecking bundled pattern synonyms20200210T22:00:58ZJoe 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.