GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:36:56Zhttps://gitlab.haskell.org/ghc/ghc//issues/10242Multiple constraint wildcards allowed with PartialTypeSignatures20190707T18:36:56ZMatthew PickeringMultiple constraint wildcards allowed with PartialTypeSignaturesThe [wiki](https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures) states that
> As a single extraconstraints wildcard is enough to infer any number of constraints, only one is allowed in a type signature and it should come last in the list of constraints.
However the following program compiles with GHC 7.10.1
```hs
{# LANGUAGE PartialTypeSignatures #}
f :: (Eq a, _, _) => a > a > Bool
f x y = x == y
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  alanz 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Multiple constraint wildcards allowed with PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":["alanz"],"type":"Bug","description":"The [https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures wiki] states that \r\n\r\n> As a single extraconstraints wildcard is enough to infer any number of constraints, only one is allowed in a type signature and it should come last in the list of constraints.\r\n\r\nHowever the following program compiles with GHC 7.10.1\r\n\r\n{{{#!hs\r\n{# LANGUAGE PartialTypeSignatures #}\r\n\r\nf :: (Eq a, _, _) => a > a > Bool\r\nf x y = x == y\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >The [wiki](https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures) states that
> As a single extraconstraints wildcard is enough to infer any number of constraints, only one is allowed in a type signature and it should come last in the list of constraints.
However the following program compiles with GHC 7.10.1
```hs
{# LANGUAGE PartialTypeSignatures #}
f :: (Eq a, _, _) => a > a > Bool
f x y = x == y
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  alanz 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Multiple constraint wildcards allowed with PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":["alanz"],"type":"Bug","description":"The [https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures wiki] states that \r\n\r\n> As a single extraconstraints wildcard is enough to infer any number of constraints, only one is allowed in a type signature and it should come last in the list of constraints.\r\n\r\nHowever the following program compiles with GHC 7.10.1\r\n\r\n{{{#!hs\r\n{# LANGUAGE PartialTypeSignatures #}\r\n\r\nf :: (Eq a, _, _) => a > a > Bool\r\nf x y = x == y\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >8.0.1thomaswthomaswhttps://gitlab.haskell.org/ghc/ghc//issues/14715GHC 8.4.1alpha regression with PartialTypeSignatures20190707T18:15:54ZRyan ScottGHC 8.4.1alpha regression with PartialTypeSignaturesThis bug prevents `lolapps`' tests and benchmarks from building with GHC 8.4.1alpha2. This is as much as I'm able to minimize the issue:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# OPTIONS_GHC Wnopartialtypesignatures #}
module Bug (bench_mulPublic) where
data Cyc r
data CT zp r'q
class Reduce a b
type family LiftOf b
bench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp > Cyc z > IO (zp,zq)
bench_mulPublic pt sk = do
ct :: CT zp (Cyc zq) < encrypt sk pt
undefined ct
encrypt :: forall z zp zq. Reduce z zq => Cyc z > Cyc zp > IO (CT zp (Cyc zq))
encrypt = undefined
```
On GHC 8.2.2, this compiles without issue. But on GHC 8.4.1alpha2, this errors with:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:1: error:
• Could not deduce (Reduce fsk0 zq)
from the context: (z ~ LiftOf zq, Reduce fsk zq)
bound by the inferred type for ‘bench_mulPublic’:
forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp > Cyc z > IO (zp, zq)
at Bug.hs:(15,1)(17,14)
The type variable ‘fsk0’ is ambiguous
• In the ambiguity check for the inferred type for ‘bench_mulPublic’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
bench_mulPublic :: forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp > Cyc z > IO (zp, zq)

15  bench_mulPublic pt sk = do
 ^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha regression with PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This bug prevents `lolapps`' tests and benchmarks from building with GHC 8.4.1alpha2. This is as much as I'm able to minimize the issue:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PartialTypeSignatures #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# OPTIONS_GHC Wnopartialtypesignatures #}\r\nmodule Bug (bench_mulPublic) where\r\n\r\ndata Cyc r\r\ndata CT zp r'q\r\nclass Reduce a b\r\ntype family LiftOf b\r\n\r\nbench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp > Cyc z > IO (zp,zq)\r\nbench_mulPublic pt sk = do\r\n ct :: CT zp (Cyc zq) < encrypt sk pt\r\n undefined ct\r\n\r\nencrypt :: forall z zp zq. Reduce z zq => Cyc z > Cyc zp > IO (CT zp (Cyc zq))\r\nencrypt = undefined\r\n}}}\r\n\r\nOn GHC 8.2.2, this compiles without issue. But on GHC 8.4.1alpha2, this errors with:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:1: error:\r\n • Could not deduce (Reduce fsk0 zq)\r\n from the context: (z ~ LiftOf zq, Reduce fsk zq)\r\n bound by the inferred type for ‘bench_mulPublic’:\r\n forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp > Cyc z > IO (zp, zq)\r\n at Bug.hs:(15,1)(17,14)\r\n The type variable ‘fsk0’ is ambiguous\r\n • In the ambiguity check for the inferred type for ‘bench_mulPublic’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the inferred type\r\n bench_mulPublic :: forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp > Cyc z > IO (zp, zq)\r\n \r\n15  bench_mulPublic pt sk = do\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This bug prevents `lolapps`' tests and benchmarks from building with GHC 8.4.1alpha2. This is as much as I'm able to minimize the issue:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# OPTIONS_GHC Wnopartialtypesignatures #}
module Bug (bench_mulPublic) where
data Cyc r
data CT zp r'q
class Reduce a b
type family LiftOf b
bench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp > Cyc z > IO (zp,zq)
bench_mulPublic pt sk = do
ct :: CT zp (Cyc zq) < encrypt sk pt
undefined ct
encrypt :: forall z zp zq. Reduce z zq => Cyc z > Cyc zp > IO (CT zp (Cyc zq))
encrypt = undefined
```
On GHC 8.2.2, this compiles without issue. But on GHC 8.4.1alpha2, this errors with:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:1: error:
• Could not deduce (Reduce fsk0 zq)
from the context: (z ~ LiftOf zq, Reduce fsk zq)
bound by the inferred type for ‘bench_mulPublic’:
forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp > Cyc z > IO (zp, zq)
at Bug.hs:(15,1)(17,14)
The type variable ‘fsk0’ is ambiguous
• In the ambiguity check for the inferred type for ‘bench_mulPublic’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
bench_mulPublic :: forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp > Cyc z > IO (zp, zq)

15  bench_mulPublic pt sk = do
 ^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha regression with PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This bug prevents `lolapps`' tests and benchmarks from building with GHC 8.4.1alpha2. This is as much as I'm able to minimize the issue:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PartialTypeSignatures #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# OPTIONS_GHC Wnopartialtypesignatures #}\r\nmodule Bug (bench_mulPublic) where\r\n\r\ndata Cyc r\r\ndata CT zp r'q\r\nclass Reduce a b\r\ntype family LiftOf b\r\n\r\nbench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp > Cyc z > IO (zp,zq)\r\nbench_mulPublic pt sk = do\r\n ct :: CT zp (Cyc zq) < encrypt sk pt\r\n undefined ct\r\n\r\nencrypt :: forall z zp zq. Reduce z zq => Cyc z > Cyc zp > IO (CT zp (Cyc zq))\r\nencrypt = undefined\r\n}}}\r\n\r\nOn GHC 8.2.2, this compiles without issue. But on GHC 8.4.1alpha2, this errors with:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:1: error:\r\n • Could not deduce (Reduce fsk0 zq)\r\n from the context: (z ~ LiftOf zq, Reduce fsk zq)\r\n bound by the inferred type for ‘bench_mulPublic’:\r\n forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp > Cyc z > IO (zp, zq)\r\n at Bug.hs:(15,1)(17,14)\r\n The type variable ‘fsk0’ is ambiguous\r\n • In the ambiguity check for the inferred type for ‘bench_mulPublic’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the inferred type\r\n bench_mulPublic :: forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp > Cyc z > IO (zp, zq)\r\n \r\n15  bench_mulPublic pt sk = do\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14643Partial type signatures in class constraints behave unexpectedly20190707T18:16:10ZmnislaihPartial type signatures in class constraints behave unexpectedlyMinimal example:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE TemplateHaskell #}
module Minimal where
id [d
f :: (Monad m, _) => [m a] > m [a]
f' :: (Monad m, _) => [m a] > m [a]
f = f'
f' [] = return []
f' (x:xx) = f xx
]
```
```
[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f :: (Monad m_a7NN, _) => [m_a7NN a_a7NO] > m_a7NN [a_a7NO]

5  id [d
 ^^^^^^...
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f' :: (Monad m_a7NL, _) => [m_a7NL a_a7NM] > m_a7NL [a_a7NM]

5  id [d
 ^^^^^^...
Ok, one module loaded.
:browse
f :: (Monad m, Monad m) => [m a] > m [a]
f' :: (Monad m, Monad m) => [m a] > m [a]
```
Notice the duplicate Monad m constraint.
Things get even more weird if the type signatures are declared together:
```hs
id [d
f, f' :: (Monad m, _) => [m a] > m [a]
f = f'
f' [] = return []
f' (x:xx) = f xx
]
```
```
[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]

5  id [d
 ^^^^^^...
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f' :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]

5  id [d
 ^^^^^^...
Ok, one module loaded.
:browse
f ::
(Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) =>
[ghcprim0.5.1.1:GHC.Types.Any ghcprim0.5.1.1:GHC.Types.Any]
> ghcprim0.5.1.1:GHC.Types.Any [ghcprim0.5.1.1:GHC.Types.Any]
f' ::
(Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) => [m a] > m [a]
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Partial type signatures in spliced TH declarations behave unexpectedly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Minimal example:\r\n{{{#!hs\r\n{# LANGUAGE PartialTypeSignatures #}\r\n{# LANGUAGE TemplateHaskell #}\r\nmodule Minimal where\r\n\r\nid [d\r\n f :: (Monad m, _) => [m a] > m [a]\r\n f' :: (Monad m, _) => [m a] > m [a]\r\n f = f'\r\n f' [] = return []\r\n f' (x:xx) = f xx\r\n ]\r\n}}}\r\n\r\n{{{\r\n[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f :: (Monad m_a7NN, _) => [m_a7NN a_a7NO] > m_a7NN [a_a7NO]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f' :: (Monad m_a7NL, _) => [m_a7NL a_a7NM] > m_a7NL [a_a7NM]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\nOk, one module loaded.\r\n :browse\r\nf :: (Monad m, Monad m) => [m a] > m [a]\r\nf' :: (Monad m, Monad m) => [m a] > m [a]\r\n}}}\r\n\r\nNotice the duplicate Monad m constraint.\r\n\r\nThings get even more weird if the type signatures are declared together:\r\n{{{#!hs\r\nid [d\r\n f, f' :: (Monad m, _) => [m a] > m [a]\r\n f = f'\r\n f' [] = return []\r\n f' (x:xx) = f xx\r\n ]\r\n}}}\r\n{{{\r\n[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f' :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\nOk, one module loaded.\r\n :browse\r\nf ::\r\n (Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) =>\r\n [ghcprim0.5.1.1:GHC.Types.Any ghcprim0.5.1.1:GHC.Types.Any]\r\n > ghcprim0.5.1.1:GHC.Types.Any [ghcprim0.5.1.1:GHC.Types.Any]\r\nf' ::\r\n (Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) => [m a] > m [a]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Minimal example:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE TemplateHaskell #}
module Minimal where
id [d
f :: (Monad m, _) => [m a] > m [a]
f' :: (Monad m, _) => [m a] > m [a]
f = f'
f' [] = return []
f' (x:xx) = f xx
]
```
```
[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f :: (Monad m_a7NN, _) => [m_a7NN a_a7NO] > m_a7NN [a_a7NO]

5  id [d
 ^^^^^^...
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f' :: (Monad m_a7NL, _) => [m_a7NL a_a7NM] > m_a7NL [a_a7NM]

5  id [d
 ^^^^^^...
Ok, one module loaded.
:browse
f :: (Monad m, Monad m) => [m a] > m [a]
f' :: (Monad m, Monad m) => [m a] > m [a]
```
Notice the duplicate Monad m constraint.
Things get even more weird if the type signatures are declared together:
```hs
id [d
f, f' :: (Monad m, _) => [m a] > m [a]
f = f'
f' [] = return []
f' (x:xx) = f xx
]
```
```
[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]

5  id [d
 ^^^^^^...
/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f' :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]

5  id [d
 ^^^^^^...
Ok, one module loaded.
:browse
f ::
(Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) =>
[ghcprim0.5.1.1:GHC.Types.Any ghcprim0.5.1.1:GHC.Types.Any]
> ghcprim0.5.1.1:GHC.Types.Any [ghcprim0.5.1.1:GHC.Types.Any]
f' ::
(Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) => [m a] > m [a]
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Partial type signatures in spliced TH declarations behave unexpectedly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Minimal example:\r\n{{{#!hs\r\n{# LANGUAGE PartialTypeSignatures #}\r\n{# LANGUAGE TemplateHaskell #}\r\nmodule Minimal where\r\n\r\nid [d\r\n f :: (Monad m, _) => [m a] > m [a]\r\n f' :: (Monad m, _) => [m a] > m [a]\r\n f = f'\r\n f' [] = return []\r\n f' (x:xx) = f xx\r\n ]\r\n}}}\r\n\r\n{{{\r\n[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f :: (Monad m_a7NN, _) => [m_a7NN a_a7NO] > m_a7NN [a_a7NO]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f' :: (Monad m_a7NL, _) => [m_a7NL a_a7NM] > m_a7NL [a_a7NM]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\nOk, one module loaded.\r\n :browse\r\nf :: (Monad m, Monad m) => [m a] > m [a]\r\nf' :: (Monad m, Monad m) => [m a] > m [a]\r\n}}}\r\n\r\nNotice the duplicate Monad m constraint.\r\n\r\nThings get even more weird if the type signatures are declared together:\r\n{{{#!hs\r\nid [d\r\n f, f' :: (Monad m, _) => [m a] > m [a]\r\n f = f'\r\n f' [] = return []\r\n f' (x:xx) = f xx\r\n ]\r\n}}}\r\n{{{\r\n[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debughoed/test/minimal.hs, interpreted )\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\n\r\n/Users/pepe/Dropbox/code/debughoed/test/minimal.hs:5:1: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f' :: (Monad m_a88E, _) => [m_a88E a_a88F] > m_a88E [a_a88F]\r\n \r\n5  id [d\r\n  ^^^^^^...\r\nOk, one module loaded.\r\n :browse\r\nf ::\r\n (Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) =>\r\n [ghcprim0.5.1.1:GHC.Types.Any ghcprim0.5.1.1:GHC.Types.Any]\r\n > ghcprim0.5.1.1:GHC.Types.Any [ghcprim0.5.1.1:GHC.Types.Any]\r\nf' ::\r\n (Monad ghcprim0.5.1.1:GHC.Types.Any, Monad m) => [m a] > m [a]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14265kinded holes20190707T18:17:42Zlspitznerkinded holesFor valuelevel holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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":"kinded holes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"For valuelevel holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.","type_of_failure":"OtherFailure","blocking":[]} >For valuelevel holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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":"kinded holes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"For valuelevel holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/15039Bizarre prettyprinting of inferred Coercible constraint in partial type sign...20190707T18:14:36ZRyan ScottBizarre prettyprinting of inferred Coercible constraint in partial type signatureConsider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:2:8: error:
• Found type wildcard ‘_’
standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of foo :: Coercible a b => Coercion a b
at <interactive>:2:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
λ> :set fprintexplicitkinds
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:4:8: error:
• Found type wildcard ‘_’
standing for ‘(a :: *) ~~ (b :: *) :: TYPE
('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of
foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b
at <interactive>:4:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
```
There are two things quite strange about this:
1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.
1. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1 
 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":"Bizarre prettyprinting of inferred Coercible constraint in partial type signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following GHCi session:\r\n\r\n{{{\r\n$ ghci\r\nGHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> import Data.Type.Coercion\r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:2:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of foo :: Coercible a b => Coercion a b\r\n at <interactive>:2:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\nλ> :set fprintexplicitkinds \r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:4:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘(a :: *) ~~ (b :: *) :: TYPE\r\n ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of\r\n foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b\r\n at <interactive>:4:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\n}}}\r\n\r\nThere are two things quite strange about this:\r\n\r\n1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.\r\n2. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:2:8: error:
• Found type wildcard ‘_’
standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of foo :: Coercible a b => Coercion a b
at <interactive>:2:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
λ> :set fprintexplicitkinds
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:4:8: error:
• Found type wildcard ‘_’
standing for ‘(a :: *) ~~ (b :: *) :: TYPE
('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of
foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b
at <interactive>:4:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
```
There are two things quite strange about this:
1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.
1. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1 
 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":"Bizarre prettyprinting of inferred Coercible constraint in partial type signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following GHCi session:\r\n\r\n{{{\r\n$ ghci\r\nGHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> import Data.Type.Coercion\r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:2:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of foo :: Coercible a b => Coercion a b\r\n at <interactive>:2:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\nλ> :set fprintexplicitkinds \r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:4:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘(a :: *) ~~ (b :: *) :: TYPE\r\n ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of\r\n foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b\r\n at <interactive>:4:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\n}}}\r\n\r\nThere are two things quite strange about this:\r\n\r\n1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.\r\n2. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/16728GHC HEADonly panic with PartialTypeSignatures20190707T18:00:04ZRyan ScottGHC HEADonly panic with PartialTypeSignaturesThe following program typechecks on GHC 8.8.1:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [Wpartialtypesignatures]ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.The following program typechecks on GHC 8.8.1:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [Wpartialtypesignatures]ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.8.10.1Richard Eisenbergrae@richarde.devRyan ScottRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/16334Named wildcards in kinds20200326T11:47:19ZVladislav ZavialovNamed wildcards in kindsThis works:
```
Prelude> :set XNamedWildCards XPartialTypeSignatures XPolyKinds
Prelude> k :: (Int :: _); k = 42
<interactive>:2:14: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘*’
• In the type signature: k :: (Int :: _)
```
And this doesn't:
```
Prelude> k :: (Int :: _t); k = 42
<interactive>:3:7: error:
• Expected kind ‘_t’, but ‘Int’ has kind ‘*’
• In the type signature: k :: (Int :: _t)
```
The issue, I suspect, is in `partition_nwcs`, which ignores kind variables for some reason.This works:
```
Prelude> :set XNamedWildCards XPartialTypeSignatures XPolyKinds
Prelude> k :: (Int :: _); k = 42
<interactive>:2:14: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘*’
• In the type signature: k :: (Int :: _)
```
And this doesn't:
```
Prelude> k :: (Int :: _t); k = 42
<interactive>:3:7: error:
• Expected kind ‘_t’, but ‘Int’ has kind ‘*’
• In the type signature: k :: (Int :: _t)
```
The issue, I suspect, is in `partition_nwcs`, which ignores kind variables for some reason.8.10.1https://gitlab.haskell.org/ghc/ghc//issues/16775Don't zap naughty quantification candidates: error instead20201215T12:32:56ZRichard Eisenbergrae@richarde.devDon't zap naughty quantification candidates: error insteadNote [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we simply don't know what to do with it. So, as the Note explains, we zap it to `Any`.
However, we recently decided not to `Any`ify in type declarations. And I think we are wrong to `Any`ify here, too. We should just error. If not, we risk having `Any` leak in error messages, and it seems a nice goal not to ever let users see `Any` (short of TH or reflection or other dastardly deeds).
The example is `partialsigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_168778 reports HEAD's error message. (The program and error message are all very intricate. Don't get distracted by reading them.) However, some of the wildcards in that error message have locallybound types, meaning there is no hope for them, regardless of other errors about. In other work (some refactoring to be posted soon), I spotted that `tcHsPartialSigType` was missing out on the action in Note [Naughty quantification candidates] and so fixed the problem. This means that the error for that program now mentions `Any`.
Here is a simpler test case:
```
foo :: forall (f :: forall a (b :: a > Type). b _). f _
foo = foo
```
Note that the type of the first `_` must be `a`, which is locally quantified. In HEAD, this program trips an assertion failure around the substitution invariant (and I have not investigated further). In my branch that duly checks partial signatures for naught quantification candidates, we get
```
• Expected kind ‘k > *’, but ‘f’ has kind ‘k > Any @*’
• In the type ‘f _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). f _
```
This is correct enough, but there's `Any` in the error message. I think it would be much better just to reject the type signature a priori.
If I make the program correct (by wrapping the `f _` in a call to `Proxy`, I get
```
Scratch.hs:44:50: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘Any @a :: a’
Where: ‘a’ is a rigid type variable bound by
‘forall a (b :: a > Type). b _’
at Scratch.hs:44:28
• In the first argument of ‘b’, namely ‘_’
In the kind ‘forall a (b :: a > Type). b _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
Scratch.hs:44:63: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_ :: k’
Where: ‘k’, ‘_’ are rigid type variables bound by
the inferred type of
foo :: Proxy
@{Any @Type} (f @Type @((>) @{'LiftedRep} @{'LiftedRep} k) _)
at Scratch.hs:45:19
• In the first argument of ‘f’, namely ‘_’
In the first argument of ‘Proxy’, namely ‘(f _)’
In the type ‘Proxy (f _)’

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
```
More `Any`s. No! Reject!
What think you (for any value of you)?Note [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we simply don't know what to do with it. So, as the Note explains, we zap it to `Any`.
However, we recently decided not to `Any`ify in type declarations. And I think we are wrong to `Any`ify here, too. We should just error. If not, we risk having `Any` leak in error messages, and it seems a nice goal not to ever let users see `Any` (short of TH or reflection or other dastardly deeds).
The example is `partialsigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_168778 reports HEAD's error message. (The program and error message are all very intricate. Don't get distracted by reading them.) However, some of the wildcards in that error message have locallybound types, meaning there is no hope for them, regardless of other errors about. In other work (some refactoring to be posted soon), I spotted that `tcHsPartialSigType` was missing out on the action in Note [Naughty quantification candidates] and so fixed the problem. This means that the error for that program now mentions `Any`.
Here is a simpler test case:
```
foo :: forall (f :: forall a (b :: a > Type). b _). f _
foo = foo
```
Note that the type of the first `_` must be `a`, which is locally quantified. In HEAD, this program trips an assertion failure around the substitution invariant (and I have not investigated further). In my branch that duly checks partial signatures for naught quantification candidates, we get
```
• Expected kind ‘k > *’, but ‘f’ has kind ‘k > Any @*’
• In the type ‘f _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). f _
```
This is correct enough, but there's `Any` in the error message. I think it would be much better just to reject the type signature a priori.
If I make the program correct (by wrapping the `f _` in a call to `Proxy`, I get
```
Scratch.hs:44:50: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘Any @a :: a’
Where: ‘a’ is a rigid type variable bound by
‘forall a (b :: a > Type). b _’
at Scratch.hs:44:28
• In the first argument of ‘b’, namely ‘_’
In the kind ‘forall a (b :: a > Type). b _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
Scratch.hs:44:63: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_ :: k’
Where: ‘k’, ‘_’ are rigid type variables bound by
the inferred type of
foo :: Proxy
@{Any @Type} (f @Type @((>) @{'LiftedRep} @{'LiftedRep} k) _)
at Scratch.hs:45:19
• In the first argument of ‘f’, namely ‘_’
In the first argument of ‘Proxy’, namely ‘(f _)’
In the type ‘Proxy (f _)’

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
```
More `Any`s. No! Reject!
What think you (for any value of you)?8.8.2https://gitlab.haskell.org/ghc/ghc//issues/18008Regression with PartialTypeSignatures in 8.1020200903T16:47:28ZAdam Sandberg ErikssonRegression with PartialTypeSignatures in 8.10This is a regression in 8.10, the code was fine in 8.8.2.
```haskell
 Bug.hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE PartialTypeSignatures #}
module Bug where
import Control.Exception
data WrappedException = WrappedException
deriving (Show)
fromSomeException :: SomeException > WrappedException
fromSomeException _ = WrappedException
instance Exception WrappedException
fun :: IO () > (forall e. (Exception e) => e > IO ()) > _  If I say IO () here it works
fun someComputation reportException =
try someComputation >>= \x > case x of
Left someException > reportException (fromSomeException someException)  or if I turn on TypeApplications and put @_ as the first argument here
Right _ > pure ()
```
Problem:
```
$ ghc version
The Glorious Glasgow Haskell Compilation System, version 8.10.1
$ ghc Bug.hs fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:27: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
WrappedException :: *
Exception e0 :: Constraint
Expected type: WrappedException > e0 > IO ()
Actual type: Exception e0 => e0 > IO ()
• The function ‘reportException’ is applied to one argument,
but its type ‘Exception e0 => e0 > IO ()’ has none
In the expression:
reportException (fromSomeException someException)
In a case alternative:
Left someException
> reportException (fromSomeException someException)

18  Left someException > reportException (fromSomeException someException)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```This is a regression in 8.10, the code was fine in 8.8.2.
```haskell
 Bug.hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE PartialTypeSignatures #}
module Bug where
import Control.Exception
data WrappedException = WrappedException
deriving (Show)
fromSomeException :: SomeException > WrappedException
fromSomeException _ = WrappedException
instance Exception WrappedException
fun :: IO () > (forall e. (Exception e) => e > IO ()) > _  If I say IO () here it works
fun someComputation reportException =
try someComputation >>= \x > case x of
Left someException > reportException (fromSomeException someException)  or if I turn on TypeApplications and put @_ as the first argument here
Right _ > pure ()
```
Problem:
```
$ ghc version
The Glorious Glasgow Haskell Compilation System, version 8.10.1
$ ghc Bug.hs fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:27: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
WrappedException :: *
Exception e0 :: Constraint
Expected type: WrappedException > e0 > IO ()
Actual type: Exception e0 => e0 > IO ()
• The function ‘reportException’ is applied to one argument,
but its type ‘Exception e0 => e0 > IO ()’ has none
In the expression:
reportException (fromSomeException someException)
In a case alternative:
Left someException
> reportException (fromSomeException someException)

18  Left someException > reportException (fromSomeException someException)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```8.10.2https://gitlab.haskell.org/ghc/ghc//issues/15433Internal error with PartialTypeSignatures and TH20210123T01:13:41ZKrzysztof GogolewskiInternal error with PartialTypeSignatures and THFile:
```
{# LANGUAGE TemplateHaskell #}
type T = $([t _ ])
```
gives a bad error message in 8.4 and HEAD:
```
• GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1sn :> ATcTyCon T :: k0]
• In the type ‘(_)’
In the type declaration for ‘T’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Internal error with PartialTypeSignatures and TH","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"File:\r\n\r\n{{{\r\n{# LANGUAGE TemplateHaskell #}\r\ntype T = $([t _ ])\r\n}}}\r\n\r\ngives a bad error message in 8.4 and HEAD:\r\n\r\n{{{\r\n • GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1sn :> ATcTyCon T :: k0]\r\n • In the type ‘(_)’\r\n In the type declaration for ‘T’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >File:
```
{# LANGUAGE TemplateHaskell #}
type T = $([t _ ])
```
gives a bad error message in 8.4 and HEAD:
```
• GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1sn :> ATcTyCon T :: k0]
• In the type ‘(_)’
In the type declaration for ‘T’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Internal error with PartialTypeSignatures and TH","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"File:\r\n\r\n{{{\r\n{# LANGUAGE TemplateHaskell #}\r\ntype T = $([t _ ])\r\n}}}\r\n\r\ngives a bad error message in 8.4 and HEAD:\r\n\r\n{{{\r\n • GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1sn :> ATcTyCon T :: k0]\r\n • In the type ‘(_)’\r\n In the type declaration for ‘T’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.2.1https://gitlab.haskell.org/ghc/ghc//issues/19106Partial type signature variable confuses instance solving20210125T22:40:41ZRichard Eisenbergrae@richarde.devPartial type signature variable confuses instance solvingWhen I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.When I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/19051Allow named wildcards in constraints20201223T15:23:55ZsheafAllow named wildcards in constraints```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PartialTypeSignatures #}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:112
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a

14  named = meth
 ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the typelevel inside the body of `named`.
(I came across this while thinking about #19010.)```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PartialTypeSignatures #}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:112
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a

14  named = meth
 ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the typelevel inside the body of `named`.
(I came across this while thinking about #19010.)https://gitlab.haskell.org/ghc/ghc//issues/19013Type wildcard infers differently than no type signature20201210T00:22:10ZdminuosoType wildcard infers differently than no type signature```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PartialTypeSignatures #}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghcwildcardbug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b > String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nixshell:~/git/ghcwildcardbug]$ cabal build
Build profile: w ghc8.8.4 O1
In order, the following will be built (use v for more details):
 ghcwildcardbug0.1.0.0 (exe:ghcwildcardbug) (file Main.hs changed)
Preprocessing executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
Building executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghcwildcardbug/distnewstyle/build/x86_64linux/ghc8.8.4/ghcwildcardbug0.1.0.0/x/ghcwildcardbug/build/ghcwildcardbug/ghcwildcardbugtmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10
 ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10

```
Also tried enabling NoMonomorphismRestriction to no avail.```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PartialTypeSignatures #}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghcwildcardbug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b > String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nixshell:~/git/ghcwildcardbug]$ cabal build
Build profile: w ghc8.8.4 O1
In order, the following will be built (use v for more details):
 ghcwildcardbug0.1.0.0 (exe:ghcwildcardbug) (file Main.hs changed)
Preprocessing executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
Building executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghcwildcardbug/distnewstyle/build/x86_64linux/ghc8.8.4/ghcwildcardbug0.1.0.0/x/ghcwildcardbug/build/ghcwildcardbug/ghcwildcardbugtmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10
 ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10

```
Also tried enabling NoMonomorphismRestriction to no avail.https://gitlab.haskell.org/ghc/ghc//issues/19010Partial type signature algorithm fails to infer constraints in the presence o...20201220T03:26:43ZsheafPartial type signature algorithm fails to infer constraints in the presence of GADTsI've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a > Float
class D a where
methD :: a > Float
foo :: forall bool a. _ => SBool bool > a > Float
foo sBool a = meth a
where
meth :: _ => a > Float
meth = case sBool of
STrue > methC
SFalse > methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:711
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methC
In a case alternative: STrue > methC
In the expression:
case sBool of
STrue > methC
SFalse > methD

23  STrue > methC
 ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:712
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methD
In a case alternative: SFalse > methD
In the expression:
case sBool of
STrue > methC
SFalse > methD

24  SFalse > methD
 ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).I've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a > Float
class D a where
methD :: a > Float
foo :: forall bool a. _ => SBool bool > a > Float
foo sBool a = meth a
where
meth :: _ => a > Float
meth = case sBool of
STrue > methC
SFalse > methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:711
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methC
In a case alternative: STrue > methC
In the expression:
case sBool of
STrue > methC
SFalse > methD

23  STrue > methC
 ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:712
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methD
In a case alternative: SFalse > methD
In the expression:
case sBool of
STrue > methC
SFalse > methD

24  SFalse > methD
 ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).https://gitlab.haskell.org/ghc/ghc//issues/18929Investigate touchable metavariables in Givens20210102T14:14:41ZRichard Eisenbergrae@richarde.devInvestigate touchable metavariables in Givens@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.https://gitlab.haskell.org/ghc/ghc//issues/17432Wildcards in standalone kind signatures20200112T20:22:51ZRichard Eisenbergrae@richarde.devWildcards in standalone kind signaturesWe should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ > Type
data Maybe a = Nothing  Just a
type Proxy :: forall (k :: _). k > _
data Proxy = MkP
```
Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.We should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ > Type
data Maybe a = Nothing  Just a
type Proxy :: forall (k :: _). k > _
data Proxy = MkP
```
Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.https://gitlab.haskell.org/ghc/ghc//issues/17024Poor interaction between functional dependencies and partial type signatures20200312T13:58:57ZDavid FeuerPoor interaction between functional dependencies and partial type signatures## Summary
A fundep is surprisingly unable to fill in a partial type signature
## Steps to reproduce
```haskell
{# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances , UndecidableInstances, PartialTypeSignatures #}
infixr 6 :::
data HList xs where
HNil :: HList '[]
(:::) :: a > HList as > HList (a ': as)
class AppHList ts o f  ts f > o, ts o > f where
appHList :: f > HList ts > o
instance AppHList '[] o o where
appHList x HNil = x
instance AppHList ts o f => AppHList (t : ts) o (t > f) where
appHList f (x ::: xs) = appHList (f x) xs
foo :: (a > b > c) > HList '[a, b] > _
foo = appHList
```
This fails with
```
AbstractList.hs:35:7: error:
• Couldn't match type ‘c’ with ‘w0’
arising from a functional dependency between:
constraint ‘AppHList '[] w0 c’ arising from a use of ‘appHList’
instance ‘AppHList '[] o o’ at AbstractList.hs:29:1025
‘c’ is a rigid type variable bound by
the inferred type of foo :: (a > b > c) > HList '[a, b] > w0
at AbstractList.hs:35:114
• In the expression: appHList
In an equation for ‘foo’: foo = appHList
• Relevant bindings include
foo :: (a > b > c) > HList '[a, b] > w0
(bound at AbstractList.hs:35:1)
```
## Expected behavior
I'd expect GHC to fill in `_` with `c`. Indeed, if I leave out the type signature and write
```haskell
foo (f :: a > b > c) (args :: HList '[a, b]) = appHList f args
```
then GHC correctly infers `foo :: (a > b > c) > HList '[a, b] > c`.
## Environment
* GHC version used: 8.6.3
Optional:
* Operating System:
* System Architecture:## Summary
A fundep is surprisingly unable to fill in a partial type signature
## Steps to reproduce
```haskell
{# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances , UndecidableInstances, PartialTypeSignatures #}
infixr 6 :::
data HList xs where
HNil :: HList '[]
(:::) :: a > HList as > HList (a ': as)
class AppHList ts o f  ts f > o, ts o > f where
appHList :: f > HList ts > o
instance AppHList '[] o o where
appHList x HNil = x
instance AppHList ts o f => AppHList (t : ts) o (t > f) where
appHList f (x ::: xs) = appHList (f x) xs
foo :: (a > b > c) > HList '[a, b] > _
foo = appHList
```
This fails with
```
AbstractList.hs:35:7: error:
• Couldn't match type ‘c’ with ‘w0’
arising from a functional dependency between:
constraint ‘AppHList '[] w0 c’ arising from a use of ‘appHList’
instance ‘AppHList '[] o o’ at AbstractList.hs:29:1025
‘c’ is a rigid type variable bound by
the inferred type of foo :: (a > b > c) > HList '[a, b] > w0
at AbstractList.hs:35:114
• In the expression: appHList
In an equation for ‘foo’: foo = appHList
• Relevant bindings include
foo :: (a > b > c) > HList '[a, b] > w0
(bound at AbstractList.hs:35:1)
```
## Expected behavior
I'd expect GHC to fill in `_` with `c`. Indeed, if I leave out the type signature and write
```haskell
foo (f :: a > b > c) (args :: HList '[a, b]) = appHList f args
```
then GHC correctly infers `foo :: (a > b > c) > HList '[a, b] > c`.
## Environment
* GHC version used: 8.6.3
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc//issues/16763Partial type signatures sometimes gets their ordering wrong20190608T12:28:07ZRichard Eisenbergrae@richarde.devPartial type signatures sometimes gets their ordering wrongIf I write
```
f1 :: forall b a. a > b > _
f1 x _ = x
```
GHC cleverly quantifies `b` before `a`, allowing visible type application to work as the user might expect.
But here are two cases where GHC is not so clever:
*Case 1:*
```
f2 :: forall k (a :: k). k > Proxy (a :: k)
f2 _ = Proxy
f3 :: forall a k. k > Proxy (a :: _)
f3 = f2
```
Of course, `f3`'s type is bogus: `k` has to come before `a`. And indeed GHC swizzles these around  but it shouldn't. Better would be to reject, because the user has requested the impossible.
*Case 2:*
```
f4 :: forall a b. a > b > _
f5 :: forall b a. a > b > _
f4 = f5
f5 = f4
```
Note that the ordering of variables in `f4` and `f5` is different. Yet GHC assigns the same quantification order to both.
*Solution:*
Currently, the working case works because of a series of delicate dependencies, starting with code in `decideQuantifiedTyVars` that sets an initial (correct) order, and blindly hopes that various data structures and functions preserve the order. They do, most of the time, but not in the cases above. Yet these functions are not really concerned with ordering, and so this might change in the future.
Better would be to fix the ordering in `chooseInferredQuantifiers`, which happens right at the end. At this point, we have the `psig_tvs`, which are the tvs as the user wrote them; and the `qtvs`, which are the variables that `simplifyInfer` has indicated should be quantified over. It should always be the case that `qtvs` is a superset of `psig_tvs`.
1. Compute `inferred = qtvs \\ psig_tvs`, where `\\` denotes setsubtraction.
2. Compute `final_qtvs = scopedSort (inferred ++ psig_tvs)`. That is, we seed `scopedSort` with the correct ordering. And we suggest that the `inferred` should go first.
3. Check that the ordering of the `psig_tvs` within `final_qtvs` is as expected. (That is, `psig_tvs` should be a subsequence of `final_qtvs`.) If not, error.
4. Label the qtvs correctly as `Specified` or `Inferred` (perhaps this can be done while doing step 3).
And off you go!If I write
```
f1 :: forall b a. a > b > _
f1 x _ = x
```
GHC cleverly quantifies `b` before `a`, allowing visible type application to work as the user might expect.
But here are two cases where GHC is not so clever:
*Case 1:*
```
f2 :: forall k (a :: k). k > Proxy (a :: k)
f2 _ = Proxy
f3 :: forall a k. k > Proxy (a :: _)
f3 = f2
```
Of course, `f3`'s type is bogus: `k` has to come before `a`. And indeed GHC swizzles these around  but it shouldn't. Better would be to reject, because the user has requested the impossible.
*Case 2:*
```
f4 :: forall a b. a > b > _
f5 :: forall b a. a > b > _
f4 = f5
f5 = f4
```
Note that the ordering of variables in `f4` and `f5` is different. Yet GHC assigns the same quantification order to both.
*Solution:*
Currently, the working case works because of a series of delicate dependencies, starting with code in `decideQuantifiedTyVars` that sets an initial (correct) order, and blindly hopes that various data structures and functions preserve the order. They do, most of the time, but not in the cases above. Yet these functions are not really concerned with ordering, and so this might change in the future.
Better would be to fix the ordering in `chooseInferredQuantifiers`, which happens right at the end. At this point, we have the `psig_tvs`, which are the tvs as the user wrote them; and the `qtvs`, which are the variables that `simplifyInfer` has indicated should be quantified over. It should always be the case that `qtvs` is a superset of `psig_tvs`.
1. Compute `inferred = qtvs \\ psig_tvs`, where `\\` denotes setsubtraction.
2. Compute `final_qtvs = scopedSort (inferred ++ psig_tvs)`. That is, we seed `scopedSort` with the correct ordering. And we suggest that the `inferred` should go first.
3. Check that the ordering of the `psig_tvs` within `final_qtvs` is as expected. (That is, `psig_tvs` should be a subsequence of `final_qtvs`.) If not, error.
4. Label the qtvs correctly as `Specified` or `Inferred` (perhaps this can be done while doing step 3).
And off you go!Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/16431Location for extraconstraints wildcards is wrong20200729T20:28:32ZSimon Peyton JonesLocation for extraconstraints wildcards is wrongIn T11515 we have
```
foo :: (ShowSyn a, _) => a > String
```
But the error says
```
T11515.hs:7:8: error:
• Found type wildcard ‘_’ standing for ‘()’
```
That column 8 is wrong: it's really column 20.
Patch comingIn T11515 we have
```
foo :: (ShowSyn a, _) => a > String
```
But the error says
```
T11515.hs:7:8: error:
• Found type wildcard ‘_’ standing for ‘()’
```
That column 8 is wrong: it's really column 20.
Patch cominghttps://gitlab.haskell.org/ghc/ghc//issues/16421Named wildcards require PartialTypeSignatures in visible kind applications, b...20190707T18:00:11ZRyan ScottNamed wildcards require PartialTypeSignatures in visible kind applications, but not type applicationsThe following program typechecks:
```haskell
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeApplications #}
module Bug where
data P (a :: k) = MkP
f :: P Int
f = MkP @_k
```
However, if I use a named wildcard in a visible //kind// application, such as in the following variant of `f`:
```haskell
g :: P @_k Int
g = MkP
```
Then GHC errors unless I enable `PartialTypeSignatures`:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:9: error:
• Found type wildcard ‘_k’ standing for ‘*’
To use the inferred type, enable PartialTypeSignatures
• In the type signature: g :: P @_k Int

11  g :: P @_k Int
 ^^
```
It feels strangely inconsistent to require the language extension in one place but not the other.The following program typechecks:
```haskell
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeApplications #}
module Bug where
data P (a :: k) = MkP
f :: P Int
f = MkP @_k
```
However, if I use a named wildcard in a visible //kind// application, such as in the following variant of `f`:
```haskell
g :: P @_k Int
g = MkP
```
Then GHC errors unless I enable `PartialTypeSignatures`:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:9: error:
• Found type wildcard ‘_k’ standing for ‘*’
To use the inferred type, enable PartialTypeSignatures
• In the type signature: g :: P @_k Int

11  g :: P @_k Int
 ^^
```
It feels strangely inconsistent to require the language extension in one place but not the other.