GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201130T16:30:41Zhttps://gitlab.haskell.org/ghc/ghc//issues/18929Investigate touchable metavariables in Givens20201130T16:30: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/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/16420Inconsistent validity checking for unnamed vs. named wildcards20190707T18:00:11ZRyan ScottInconsistent validity checking for unnamed vs. named wildcardsGHC HEAD rejects the following program:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PolyKinds #}
{# OPTIONS_GHC Wnopartialtypesignatures #}
module Bug where
import Data.Proxy
class C k (a :: k)
f :: (C _ a) => Proxy a
f = Proxy
```
```
GHCi, version 8.9.20190220: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:9: error:
Wildcard ‘_’ not allowed in a constraint
except as the last toplevel constraint of a type signature
e.g f :: (Eq a, _) => blah
in the type signature for ‘f’

12  f :: (C _ a) => Proxy a
 ^
```
But it accepts it if you change `_` to `_k`, a named wildcard!
```haskell
f :: (C _k a) => Proxy a
f = Proxy
```
This feels strangely inconsistent to me, as I would have expected GHC's treatment of these two programs to be the same.GHC HEAD rejects the following program:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PolyKinds #}
{# OPTIONS_GHC Wnopartialtypesignatures #}
module Bug where
import Data.Proxy
class C k (a :: k)
f :: (C _ a) => Proxy a
f = Proxy
```
```
GHCi, version 8.9.20190220: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:9: error:
Wildcard ‘_’ not allowed in a constraint
except as the last toplevel constraint of a type signature
e.g f :: (Eq a, _) => blah
in the type signature for ‘f’

12  f :: (C _ a) => Proxy a
 ^
```
But it accepts it if you change `_` to `_k`, a named wildcard!
```haskell
f :: (C _k a) => Proxy a
f = Proxy
```
This feels strangely inconsistent to me, as I would have expected GHC's treatment of these two programs to be the same.https://gitlab.haskell.org/ghc/ghc//issues/16203Unhelpful names for wildcard type variables20190707T18:00:58ZSimon Peyton JonesUnhelpful names for wildcard type variablesConsider
```
{# LANGUAGE PartialTypeSignatures #}
f :: _ > _
f x = x
```
With GHC 8.6 we got
```
T16152.hs:10:6: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘w’
Where: ‘w’ is a rigid type variable bound by
the inferred type of f :: w > w
at T16152.hs:11:17
• In the type signature: f :: _ > _

10  f :: _ > _
 ^
T16152.hs:10:11: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘w’
Where: ‘w’ is a rigid type variable bound by
the inferred type of f :: w > w
at T16152.hs:11:17
• In the type signature: f :: _ > _

10  f :: _ > _
 ^
```
But with HEAD we get
```
T16152.hs:10:6: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_’
Where: ‘_’ is a rigid type variable bound by
the inferred type of f :: _ > _
at T16152.hs:11:17
• In the type ‘_ > _’
In the type signature: f :: _ > _

10  f :: _ > _
 ^
T16152.hs:10:11: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_’
Where: ‘_’ is a rigid type variable bound by
the inferred type of f :: _ > _
at T16152.hs:11:17
• In the type ‘_ > _’
In the type signature: f :: _ > _

10  f :: _ > _
 ^
```
Saying "Found type wildcard ‘_’ standing for ‘_’" is unhelpful. The "w" form is much better.
The change is caused by
```
commit 17bd163566153babbf51adaff8397f948ae363ca
Author: mynguyen <mnguyen1@brynmawr.edu>
Date: Tue Dec 18 11:52:26 2018 0500
Visible kind application
```
which has this patch
```
newWildTyVar _name
+newWildTyVar
= do { kind < newMetaKindVar
; uniq < newUnique
; details < newMetaDetails TauTv
 ; let name = mkSysTvName uniq (fsLit "w")
+ ; let name = mkSysTvName uniq (fsLit "_")
tyvar = (mkTcTyVar name kind details)
; traceTc "newWildTyVar" (ppr tyvar)
; return tyvar }
```
What was the reason for this change? Can we change "_" back to "w" please?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Unhelpful names for wildcard type variables","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n{{{\r\n{# LANGUAGE PartialTypeSignatures #}\r\n\r\nf :: _ > _\r\nf x = x\r\n}}}\r\nWith GHC 8.6 we got\r\n{{{\r\nT16152.hs:10:6: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘w’\r\n Where: ‘w’ is a rigid type variable bound by\r\n the inferred type of f :: w > w\r\n at T16152.hs:11:17\r\n • In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n\r\nT16152.hs:10:11: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘w’\r\n Where: ‘w’ is a rigid type variable bound by\r\n the inferred type of f :: w > w\r\n at T16152.hs:11:17\r\n • In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n}}}\r\nBut with HEAD we get\r\n{{{\r\nT16152.hs:10:6: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘_’\r\n Where: ‘_’ is a rigid type variable bound by\r\n the inferred type of f :: _ > _\r\n at T16152.hs:11:17\r\n • In the type ‘_ > _’\r\n In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n\r\nT16152.hs:10:11: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘_’\r\n Where: ‘_’ is a rigid type variable bound by\r\n the inferred type of f :: _ > _\r\n at T16152.hs:11:17\r\n • In the type ‘_ > _’\r\n In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n}}}\r\nSaying \"Found type wildcard ‘_’ standing for ‘_’\" is unhelpful. The \"w\" form is much better.\r\n\r\nThe change is caused by\r\n{{{\r\ncommit 17bd163566153babbf51adaff8397f948ae363ca\r\nAuthor: mynguyen <mnguyen1@brynmawr.edu>\r\nDate: Tue Dec 18 11:52:26 2018 0500\r\n\r\n Visible kind application\r\n}}}\r\nwhich has this patch\r\n{{{\r\nnewWildTyVar _name\r\n+newWildTyVar\r\n = do { kind < newMetaKindVar\r\n ; uniq < newUnique\r\n ; details < newMetaDetails TauTv\r\n ; let name = mkSysTvName uniq (fsLit \"w\")\r\n+ ; let name = mkSysTvName uniq (fsLit \"_\")\r\n tyvar = (mkTcTyVar name kind details)\r\n ; traceTc \"newWildTyVar\" (ppr tyvar)\r\n ; return tyvar }\r\n}}}\r\nWhat was the reason for this change? Can we change \"_\" back to \"w\" please?\r\n","type_of_failure":"OtherFailure","blocking":[]} >Consider
```
{# LANGUAGE PartialTypeSignatures #}
f :: _ > _
f x = x
```
With GHC 8.6 we got
```
T16152.hs:10:6: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘w’
Where: ‘w’ is a rigid type variable bound by
the inferred type of f :: w > w
at T16152.hs:11:17
• In the type signature: f :: _ > _

10  f :: _ > _
 ^
T16152.hs:10:11: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘w’
Where: ‘w’ is a rigid type variable bound by
the inferred type of f :: w > w
at T16152.hs:11:17
• In the type signature: f :: _ > _

10  f :: _ > _
 ^
```
But with HEAD we get
```
T16152.hs:10:6: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_’
Where: ‘_’ is a rigid type variable bound by
the inferred type of f :: _ > _
at T16152.hs:11:17
• In the type ‘_ > _’
In the type signature: f :: _ > _

10  f :: _ > _
 ^
T16152.hs:10:11: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_’
Where: ‘_’ is a rigid type variable bound by
the inferred type of f :: _ > _
at T16152.hs:11:17
• In the type ‘_ > _’
In the type signature: f :: _ > _

10  f :: _ > _
 ^
```
Saying "Found type wildcard ‘_’ standing for ‘_’" is unhelpful. The "w" form is much better.
The change is caused by
```
commit 17bd163566153babbf51adaff8397f948ae363ca
Author: mynguyen <mnguyen1@brynmawr.edu>
Date: Tue Dec 18 11:52:26 2018 0500
Visible kind application
```
which has this patch
```
newWildTyVar _name
+newWildTyVar
= do { kind < newMetaKindVar
; uniq < newUnique
; details < newMetaDetails TauTv
 ; let name = mkSysTvName uniq (fsLit "w")
+ ; let name = mkSysTvName uniq (fsLit "_")
tyvar = (mkTcTyVar name kind details)
; traceTc "newWildTyVar" (ppr tyvar)
; return tyvar }
```
What was the reason for this change? Can we change "_" back to "w" please?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Unhelpful names for wildcard type variables","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n{{{\r\n{# LANGUAGE PartialTypeSignatures #}\r\n\r\nf :: _ > _\r\nf x = x\r\n}}}\r\nWith GHC 8.6 we got\r\n{{{\r\nT16152.hs:10:6: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘w’\r\n Where: ‘w’ is a rigid type variable bound by\r\n the inferred type of f :: w > w\r\n at T16152.hs:11:17\r\n • In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n\r\nT16152.hs:10:11: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘w’\r\n Where: ‘w’ is a rigid type variable bound by\r\n the inferred type of f :: w > w\r\n at T16152.hs:11:17\r\n • In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n}}}\r\nBut with HEAD we get\r\n{{{\r\nT16152.hs:10:6: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘_’\r\n Where: ‘_’ is a rigid type variable bound by\r\n the inferred type of f :: _ > _\r\n at T16152.hs:11:17\r\n • In the type ‘_ > _’\r\n In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n\r\nT16152.hs:10:11: warning: [Wpartialtypesignatures]\r\n • Found type wildcard ‘_’ standing for ‘_’\r\n Where: ‘_’ is a rigid type variable bound by\r\n the inferred type of f :: _ > _\r\n at T16152.hs:11:17\r\n • In the type ‘_ > _’\r\n In the type signature: f :: _ > _\r\n \r\n10  f :: _ > _\r\n  ^\r\n}}}\r\nSaying \"Found type wildcard ‘_’ standing for ‘_’\" is unhelpful. The \"w\" form is much better.\r\n\r\nThe change is caused by\r\n{{{\r\ncommit 17bd163566153babbf51adaff8397f948ae363ca\r\nAuthor: mynguyen <mnguyen1@brynmawr.edu>\r\nDate: Tue Dec 18 11:52:26 2018 0500\r\n\r\n Visible kind application\r\n}}}\r\nwhich has this patch\r\n{{{\r\nnewWildTyVar _name\r\n+newWildTyVar\r\n = do { kind < newMetaKindVar\r\n ; uniq < newUnique\r\n ; details < newMetaDetails TauTv\r\n ; let name = mkSysTvName uniq (fsLit \"w\")\r\n+ ; let name = mkSysTvName uniq (fsLit \"_\")\r\n tyvar = (mkTcTyVar name kind details)\r\n ; traceTc \"newWildTyVar\" (ppr tyvar)\r\n ; return tyvar }\r\n}}}\r\nWhat was the reason for this change? Can we change \"_\" back to \"w\" please?\r\n","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/16152Core lint error from PartialTypeSignatures20190902T13:01:51ZIcelandjackCore lint error from PartialTypeSignatures```hs
{# Language PartialTypeSignatures #}
{# Language PolyKinds #}
{# Language ScopedTypeVariables #}
{# Options_GHC dcorelint #}
top :: forall f. _
top = undefined where
x :: forall a. f a
x = undefined
```
causes Core lint errors:
```
$ ~/../inplace/bin/ghcstage2 interactive ignoredotghci 922_bug.hs
GHCi, version 8.7.20181230: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 922_bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
In the type ‘forall (f :: k_a1z6 > *) w. w’
@ k_a1z6 is out of scope
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)
top :: forall (f :: k_a1z6 > *) w. w
[LclIdX]
top
= \ (@ (f_a2BY :: k_a1z6 > *)) (@ w_a2BZ) >
(\ (@ k_a1z6) (@ (f_a1yV :: k_a1z6 > *)) (@ w_a1yN) >
let {
$dIP_a2BO :: ?callStack::CallStack
[LclId]
$dIP_a2BO
= emptyCallStack
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
let {
$dIP_a2BD :: HasCallStack
[LclId]
$dIP_a2BD
= (pushCallStack
(unpackCString# "undefined"#,
SrcLoc
(unpackCString# "main"#)
(unpackCString# "Main"#)
(unpackCString# "922_bug.hs"#)
(I# 8#)
(I# 7#)
(I# 8#)
(I# 16#))
($dIP_a2BO
`cast` (N:IP[0] <"callStack">_N <CallStack>_N
:: (?callStack::CallStack) ~R# CallStack)))
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
letrec {
top_a1yW :: w_a1yN
[LclId]
top_a1yW
= letrec {
x_a1yv :: forall (a :: k_a1z6). f_a1yV a
[LclId]
x_a1yv
= \ (@ (a_a1zd :: k_a1z6)) >
let {
$dIP_a2BP :: ?callStack::CallStack
[LclId]
$dIP_a2BP
= emptyCallStack
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
let {
$dIP_a2Bz :: HasCallStack
[LclId]
$dIP_a2Bz
= (pushCallStack
(unpackCString# "undefined"#,
SrcLoc
(unpackCString# "main"#)
(unpackCString# "Main"#)
(unpackCString# "922_bug.hs"#)
(I# 11#)
(I# 7#)
(I# 11#)
(I# 16#))
($dIP_a2BP
`cast` (N:IP[0] <"callStack">_N <CallStack>_N
:: (?callStack::CallStack) ~R# CallStack)))
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
break<0>() undefined @ 'LiftedRep @ (f_a1yV a_a1zd) $dIP_a2Bz; } in
break<1>() undefined @ 'LiftedRep @ w_a1yN $dIP_a2BD; } in
top_a1yW)
@ Any @ Any @ w_a2BZ
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 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":"Core lint error from PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language PartialTypeSignatures #}\r\n{# Language PolyKinds #}\r\n{# Language ScopedTypeVariables #}\r\n\r\n{# Options_GHC dcorelint #}\r\n\r\ntop :: forall f. _\r\ntop = undefined where\r\n\r\n x :: forall a. f a\r\n x = undefined\r\n}}}\r\n\r\ncauses Core lint errors:\r\n\r\n{{{\r\n$ ~/../inplace/bin/ghcstage2 interactive ignoredotghci 922_bug.hs\r\nGHCi, version 8.7.20181230: https://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 922_bug.hs, interpreted )\r\n*** Core Lint errors : in result of Desugar (before optimization) ***\r\n<no location info>: warning:\r\n In the type ‘forall (f :: k_a1z6 > *) w. w’\r\n @ k_a1z6 is out of scope\r\n*** Offending Program ***\r\nRec {\r\n$trModule :: Module\r\n[LclIdX]\r\n$trModule = Module (TrNameS \"main\"#) (TrNameS \"Main\"#)\r\n\r\ntop :: forall (f :: k_a1z6 > *) w. w\r\n[LclIdX]\r\ntop\r\n = \\ (@ (f_a2BY :: k_a1z6 > *)) (@ w_a2BZ) >\r\n (\\ (@ k_a1z6) (@ (f_a1yV :: k_a1z6 > *)) (@ w_a1yN) >\r\n let {\r\n $dIP_a2BO :: ?callStack::CallStack\r\n [LclId]\r\n $dIP_a2BO\r\n = emptyCallStack\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n let {\r\n $dIP_a2BD :: HasCallStack\r\n [LclId]\r\n $dIP_a2BD\r\n = (pushCallStack\r\n (unpackCString# \"undefined\"#,\r\n SrcLoc\r\n (unpackCString# \"main\"#)\r\n (unpackCString# \"Main\"#)\r\n (unpackCString# \"922_bug.hs\"#)\r\n (I# 8#)\r\n (I# 7#)\r\n (I# 8#)\r\n (I# 16#))\r\n ($dIP_a2BO\r\n `cast` (N:IP[0] <\"callStack\">_N <CallStack>_N\r\n :: (?callStack::CallStack) ~R# CallStack)))\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n letrec {\r\n top_a1yW :: w_a1yN\r\n [LclId]\r\n top_a1yW\r\n = letrec {\r\n x_a1yv :: forall (a :: k_a1z6). f_a1yV a\r\n [LclId]\r\n x_a1yv\r\n = \\ (@ (a_a1zd :: k_a1z6)) >\r\n let {\r\n $dIP_a2BP :: ?callStack::CallStack\r\n [LclId]\r\n $dIP_a2BP\r\n = emptyCallStack\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n let {\r\n $dIP_a2Bz :: HasCallStack\r\n [LclId]\r\n $dIP_a2Bz\r\n = (pushCallStack\r\n (unpackCString# \"undefined\"#,\r\n SrcLoc\r\n (unpackCString# \"main\"#)\r\n (unpackCString# \"Main\"#)\r\n (unpackCString# \"922_bug.hs\"#)\r\n (I# 11#)\r\n (I# 7#)\r\n (I# 11#)\r\n (I# 16#))\r\n ($dIP_a2BP\r\n `cast` (N:IP[0] <\"callStack\">_N <CallStack>_N\r\n :: (?callStack::CallStack) ~R# CallStack)))\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n break<0>() undefined @ 'LiftedRep @ (f_a1yV a_a1zd) $dIP_a2Bz; } in\r\n break<1>() undefined @ 'LiftedRep @ w_a1yN $dIP_a2BD; } in\r\n top_a1yW)\r\n @ Any @ Any @ w_a2BZ\r\nend Rec }\r\n\r\n*** End of Offense ***\r\n\r\n\r\n<no location info>: error:\r\nCompilation had errors\r\n\r\n\r\n*** Exception: ExitFailure 1\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language PartialTypeSignatures #}
{# Language PolyKinds #}
{# Language ScopedTypeVariables #}
{# Options_GHC dcorelint #}
top :: forall f. _
top = undefined where
x :: forall a. f a
x = undefined
```
causes Core lint errors:
```
$ ~/../inplace/bin/ghcstage2 interactive ignoredotghci 922_bug.hs
GHCi, version 8.7.20181230: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 922_bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
In the type ‘forall (f :: k_a1z6 > *) w. w’
@ k_a1z6 is out of scope
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)
top :: forall (f :: k_a1z6 > *) w. w
[LclIdX]
top
= \ (@ (f_a2BY :: k_a1z6 > *)) (@ w_a2BZ) >
(\ (@ k_a1z6) (@ (f_a1yV :: k_a1z6 > *)) (@ w_a1yN) >
let {
$dIP_a2BO :: ?callStack::CallStack
[LclId]
$dIP_a2BO
= emptyCallStack
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
let {
$dIP_a2BD :: HasCallStack
[LclId]
$dIP_a2BD
= (pushCallStack
(unpackCString# "undefined"#,
SrcLoc
(unpackCString# "main"#)
(unpackCString# "Main"#)
(unpackCString# "922_bug.hs"#)
(I# 8#)
(I# 7#)
(I# 8#)
(I# 16#))
($dIP_a2BO
`cast` (N:IP[0] <"callStack">_N <CallStack>_N
:: (?callStack::CallStack) ~R# CallStack)))
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
letrec {
top_a1yW :: w_a1yN
[LclId]
top_a1yW
= letrec {
x_a1yv :: forall (a :: k_a1z6). f_a1yV a
[LclId]
x_a1yv
= \ (@ (a_a1zd :: k_a1z6)) >
let {
$dIP_a2BP :: ?callStack::CallStack
[LclId]
$dIP_a2BP
= emptyCallStack
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
let {
$dIP_a2Bz :: HasCallStack
[LclId]
$dIP_a2Bz
= (pushCallStack
(unpackCString# "undefined"#,
SrcLoc
(unpackCString# "main"#)
(unpackCString# "Main"#)
(unpackCString# "922_bug.hs"#)
(I# 11#)
(I# 7#)
(I# 11#)
(I# 16#))
($dIP_a2BP
`cast` (N:IP[0] <"callStack">_N <CallStack>_N
:: (?callStack::CallStack) ~R# CallStack)))
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
break<0>() undefined @ 'LiftedRep @ (f_a1yV a_a1zd) $dIP_a2Bz; } in
break<1>() undefined @ 'LiftedRep @ w_a1yN $dIP_a2BD; } in
top_a1yW)
@ Any @ Any @ w_a2BZ
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 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":"Core lint error from PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language PartialTypeSignatures #}\r\n{# Language PolyKinds #}\r\n{# Language ScopedTypeVariables #}\r\n\r\n{# Options_GHC dcorelint #}\r\n\r\ntop :: forall f. _\r\ntop = undefined where\r\n\r\n x :: forall a. f a\r\n x = undefined\r\n}}}\r\n\r\ncauses Core lint errors:\r\n\r\n{{{\r\n$ ~/../inplace/bin/ghcstage2 interactive ignoredotghci 922_bug.hs\r\nGHCi, version 8.7.20181230: https://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 922_bug.hs, interpreted )\r\n*** Core Lint errors : in result of Desugar (before optimization) ***\r\n<no location info>: warning:\r\n In the type ‘forall (f :: k_a1z6 > *) w. w’\r\n @ k_a1z6 is out of scope\r\n*** Offending Program ***\r\nRec {\r\n$trModule :: Module\r\n[LclIdX]\r\n$trModule = Module (TrNameS \"main\"#) (TrNameS \"Main\"#)\r\n\r\ntop :: forall (f :: k_a1z6 > *) w. w\r\n[LclIdX]\r\ntop\r\n = \\ (@ (f_a2BY :: k_a1z6 > *)) (@ w_a2BZ) >\r\n (\\ (@ k_a1z6) (@ (f_a1yV :: k_a1z6 > *)) (@ w_a1yN) >\r\n let {\r\n $dIP_a2BO :: ?callStack::CallStack\r\n [LclId]\r\n $dIP_a2BO\r\n = emptyCallStack\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n let {\r\n $dIP_a2BD :: HasCallStack\r\n [LclId]\r\n $dIP_a2BD\r\n = (pushCallStack\r\n (unpackCString# \"undefined\"#,\r\n SrcLoc\r\n (unpackCString# \"main\"#)\r\n (unpackCString# \"Main\"#)\r\n (unpackCString# \"922_bug.hs\"#)\r\n (I# 8#)\r\n (I# 7#)\r\n (I# 8#)\r\n (I# 16#))\r\n ($dIP_a2BO\r\n `cast` (N:IP[0] <\"callStack\">_N <CallStack>_N\r\n :: (?callStack::CallStack) ~R# CallStack)))\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n letrec {\r\n top_a1yW :: w_a1yN\r\n [LclId]\r\n top_a1yW\r\n = letrec {\r\n x_a1yv :: forall (a :: k_a1z6). f_a1yV a\r\n [LclId]\r\n x_a1yv\r\n = \\ (@ (a_a1zd :: k_a1z6)) >\r\n let {\r\n $dIP_a2BP :: ?callStack::CallStack\r\n [LclId]\r\n $dIP_a2BP\r\n = emptyCallStack\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n let {\r\n $dIP_a2Bz :: HasCallStack\r\n [LclId]\r\n $dIP_a2Bz\r\n = (pushCallStack\r\n (unpackCString# \"undefined\"#,\r\n SrcLoc\r\n (unpackCString# \"main\"#)\r\n (unpackCString# \"Main\"#)\r\n (unpackCString# \"922_bug.hs\"#)\r\n (I# 11#)\r\n (I# 7#)\r\n (I# 11#)\r\n (I# 16#))\r\n ($dIP_a2BP\r\n `cast` (N:IP[0] <\"callStack\">_N <CallStack>_N\r\n :: (?callStack::CallStack) ~R# CallStack)))\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n break<0>() undefined @ 'LiftedRep @ (f_a1yV a_a1zd) $dIP_a2Bz; } in\r\n break<1>() undefined @ 'LiftedRep @ w_a1yN $dIP_a2BD; } in\r\n top_a1yW)\r\n @ Any @ Any @ w_a2BZ\r\nend Rec }\r\n\r\n*** End of Offense ***\r\n\r\n\r\n<no location info>: error:\r\nCompilation had errors\r\n\r\n\r\n*** Exception: ExitFailure 1\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16082Sort out treatment of underscores in types20200605T13:27:57ZRichard Eisenbergrae@richarde.devSort out treatment of underscores in typesI can count 4 different meanings for underscores in Haskell programs:
1. A pattern for which we don't care to write a name. (This dates back to antiquity.)
Example:
```hs
const x _ = x
```
1. An expression for which we want GHC to tell us what its expected type should be. (Relatively new: these are typed holes.)
Example:
```hs
plus x y = x + _
```
1. A type which we want GHC to infer, by looking at the expression. (Relatively new: these are wild cards in partial type signatures.)
Example:
```hs
plus :: forall a. Num a => a > a > _
plus x y = x + y
```
1. A type which we want GHC to infer, by looking at the underscore's context. (Relatively new: these are wild cards in type applications.)
Example:
```hs
x = const @_ @Bool 'x'  the _ is inferred to mean Char
```
Problems arise with the advent of visible kind application (#12045): In type signatures, 3 of these meanings make sense (2, 3, and 4). In type/data family patterns, 3 of these meanings make sense (1, 2, and 4). Ideally, the user should have the opportunity to choose which meaning they want. In contrast, right now we use heuristics: in visible type/kind applications, we always use (4); otherwise, we use (1) (in patterns) or (3) (in types).
This is a mess, for at least three reasons:
A. Users might conceivably want different behavior than what we provide. For example, perhaps a user is writing an intricate pattern (at either term or type level) and wants to know the type (resp. kind) of the next bit of pattern. Or maybe the user wants to do this in a visible type application. Right now, there's just no way to do this.
B. It causes trouble for prettyprinting. Aside from termlevel patterns, all the uses of underscores above are stored identically in the AST. This means that they are printed identically. But that's strange. For example, uses (3) and (4) might have different underscores meaning different variables. Should we number the underscores? But that would be silly for usage (1). It's all a bit muddy.
C. This causes awkwardness in the implementation. #12045 has to twiddle DynFlags to get its desired behavior, and that's sad.
This ticket is to track resolutions to these problems.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 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":"Sort out treatment of underscores in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I can count 4 different meanings for underscores in Haskell programs:\r\n\r\n1. A pattern for which we don't care to write a name. (This dates back to antiquity.)\r\nExample: \r\n{{{#!hs\r\nconst x _ = x\r\n}}}\r\n\r\n2. An expression for which we want GHC to tell us what its expected type should be. (Relatively new: these are typed holes.)\r\nExample: \r\n{{{#!hs\r\nplus x y = x + _\r\n}}}\r\n\r\n3. A type which we want GHC to infer, by looking at the expression. (Relatively new: these are wild cards in partial type signatures.)\r\nExample: \r\n{{{#!hs\r\nplus :: forall a. Num a => a > a > _\r\nplus x y = x + y\r\n}}}\r\n\r\n4. A type which we want GHC to infer, by looking at the underscore's context. (Relatively new: these are wild cards in type applications.)\r\nExample:\r\n{{{#!hs\r\nx = const @_ @Bool 'x'  the _ is inferred to mean Char\r\n}}}\r\n\r\nProblems arise with the advent of visible kind application (#12045): In type signatures, 3 of these meanings make sense (2, 3, and 4). In type/data family patterns, 3 of these meanings make sense (1, 2, and 4). Ideally, the user should have the opportunity to choose which meaning they want. In contrast, right now we use heuristics: in visible type/kind applications, we always use (4); otherwise, we use (1) (in patterns) or (3) (in types).\r\n\r\nThis is a mess, for at least three reasons:\r\n\r\nA. Users might conceivably want different behavior than what we provide. For example, perhaps a user is writing an intricate pattern (at either term or type level) and wants to know the type (resp. kind) of the next bit of pattern. Or maybe the user wants to do this in a visible type application. Right now, there's just no way to do this.\r\n\r\nB. It causes trouble for prettyprinting. Aside from termlevel patterns, all the uses of underscores above are stored identically in the AST. This means that they are printed identically. But that's strange. For example, uses (3) and (4) might have different underscores meaning different variables. Should we number the underscores? But that would be silly for usage (1). It's all a bit muddy.\r\n\r\nC. This causes awkwardness in the implementation. #12045 has to twiddle DynFlags to get its desired behavior, and that's sad.\r\n\r\nThis ticket is to track resolutions to these problems.","type_of_failure":"OtherFailure","blocking":[]} >I can count 4 different meanings for underscores in Haskell programs:
1. A pattern for which we don't care to write a name. (This dates back to antiquity.)
Example:
```hs
const x _ = x
```
1. An expression for which we want GHC to tell us what its expected type should be. (Relatively new: these are typed holes.)
Example:
```hs
plus x y = x + _
```
1. A type which we want GHC to infer, by looking at the expression. (Relatively new: these are wild cards in partial type signatures.)
Example:
```hs
plus :: forall a. Num a => a > a > _
plus x y = x + y
```
1. A type which we want GHC to infer, by looking at the underscore's context. (Relatively new: these are wild cards in type applications.)
Example:
```hs
x = const @_ @Bool 'x'  the _ is inferred to mean Char
```
Problems arise with the advent of visible kind application (#12045): In type signatures, 3 of these meanings make sense (2, 3, and 4). In type/data family patterns, 3 of these meanings make sense (1, 2, and 4). Ideally, the user should have the opportunity to choose which meaning they want. In contrast, right now we use heuristics: in visible type/kind applications, we always use (4); otherwise, we use (1) (in patterns) or (3) (in types).
This is a mess, for at least three reasons:
A. Users might conceivably want different behavior than what we provide. For example, perhaps a user is writing an intricate pattern (at either term or type level) and wants to know the type (resp. kind) of the next bit of pattern. Or maybe the user wants to do this in a visible type application. Right now, there's just no way to do this.
B. It causes trouble for prettyprinting. Aside from termlevel patterns, all the uses of underscores above are stored identically in the AST. This means that they are printed identically. But that's strange. For example, uses (3) and (4) might have different underscores meaning different variables. Should we number the underscores? But that would be silly for usage (1). It's all a bit muddy.
C. This causes awkwardness in the implementation. #12045 has to twiddle DynFlags to get its desired behavior, and that's sad.
This ticket is to track resolutions to these problems.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 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":"Sort out treatment of underscores in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I can count 4 different meanings for underscores in Haskell programs:\r\n\r\n1. A pattern for which we don't care to write a name. (This dates back to antiquity.)\r\nExample: \r\n{{{#!hs\r\nconst x _ = x\r\n}}}\r\n\r\n2. An expression for which we want GHC to tell us what its expected type should be. (Relatively new: these are typed holes.)\r\nExample: \r\n{{{#!hs\r\nplus x y = x + _\r\n}}}\r\n\r\n3. A type which we want GHC to infer, by looking at the expression. (Relatively new: these are wild cards in partial type signatures.)\r\nExample: \r\n{{{#!hs\r\nplus :: forall a. Num a => a > a > _\r\nplus x y = x + y\r\n}}}\r\n\r\n4. A type which we want GHC to infer, by looking at the underscore's context. (Relatively new: these are wild cards in type applications.)\r\nExample:\r\n{{{#!hs\r\nx = const @_ @Bool 'x'  the _ is inferred to mean Char\r\n}}}\r\n\r\nProblems arise with the advent of visible kind application (#12045): In type signatures, 3 of these meanings make sense (2, 3, and 4). In type/data family patterns, 3 of these meanings make sense (1, 2, and 4). Ideally, the user should have the opportunity to choose which meaning they want. In contrast, right now we use heuristics: in visible type/kind applications, we always use (4); otherwise, we use (1) (in patterns) or (3) (in types).\r\n\r\nThis is a mess, for at least three reasons:\r\n\r\nA. Users might conceivably want different behavior than what we provide. For example, perhaps a user is writing an intricate pattern (at either term or type level) and wants to know the type (resp. kind) of the next bit of pattern. Or maybe the user wants to do this in a visible type application. Right now, there's just no way to do this.\r\n\r\nB. It causes trouble for prettyprinting. Aside from termlevel patterns, all the uses of underscores above are stored identically in the AST. This means that they are printed identically. But that's strange. For example, uses (3) and (4) might have different underscores meaning different variables. Should we number the underscores? But that would be silly for usage (1). It's all a bit muddy.\r\n\r\nC. This causes awkwardness in the implementation. #12045 has to twiddle DynFlags to get its desired behavior, and that's sad.\r\n\r\nThis ticket is to track resolutions to these problems.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15433Internal error with PartialTypeSignatures and TH20200123T19:16:21ZKrzysztof 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.0.1https://gitlab.haskell.org/ghc/ghc//issues/14766Holey partial type signatures greatly slow down compile times20190707T18:15:43ZAlec TheriaultHoley partial type signatures greatly slow down compile timesThis time, I actually mean it. :)
Originally reported [here](https://github.com/simonmar/happy/issues/109), I distilled the example from [this comment](https://github.com/simonmar/happy/issues/109#issuecomment362957245) into a one file test case. `Sigs.hs` is exactly like `NoSigs.hs`, except for the fact that it has a bunch of extra type signatures that have a lot of holes. On my machine, this is what compilation times are (I gave up timing after 15 minutes):
<table><tr><td> GHC version </td>
<td> 8.0.2 </td>
<td> 8.2.1 </td>
<td> 8.4.1 (445554b6d9a2263f969e25bb9f532dd0c3a9dc8c) </td></tr>
<tr><td> `NoSigs.hs` </td>
<td> 24.13s </td>
<td> 22.93s </td>
<td> 34.05s </td></tr>
<tr><td> `Sigs.hs` </td>
<td> \>15m </td>
<td> \~13m </td>
<td> \>15m </td></tr></table>This time, I actually mean it. :)
Originally reported [here](https://github.com/simonmar/happy/issues/109), I distilled the example from [this comment](https://github.com/simonmar/happy/issues/109#issuecomment362957245) into a one file test case. `Sigs.hs` is exactly like `NoSigs.hs`, except for the fact that it has a bunch of extra type signatures that have a lot of holes. On my machine, this is what compilation times are (I gave up timing after 15 minutes):
<table><tr><td> GHC version </td>
<td> 8.0.2 </td>
<td> 8.2.1 </td>
<td> 8.4.1 (445554b6d9a2263f969e25bb9f532dd0c3a9dc8c) </td></tr>
<tr><td> `NoSigs.hs` </td>
<td> 24.13s </td>
<td> 22.93s </td>
<td> 34.05s </td></tr>
<tr><td> `Sigs.hs` </td>
<td> \>15m </td>
<td> \~13m </td>
<td> \>15m </td></tr></table>https://gitlab.haskell.org/ghc/ghc//issues/14662Partial type signatures + mutual recursion = confusion20190707T18:16:06ZRichard Eisenbergrae@richarde.devPartial type signatures + mutual recursion = confusionI'm trying to understand better how partial type signatures interact with mutual recursion. This is all in 8.4.1alpha1.
Example 1:
```hs
f :: forall a. _ > a > a
f _ x = g True x
g :: forall b. _ > b > b
g _ x = f 'x' x
```
This works  no problem.
Example 2:
```hs
f :: forall a. _ > a > a
f _ x = snd (g True 'a', x)
g :: forall b. _ > b > b
g _ x = f 'x' x
```
This fails, explaining that GHC inferred `g :: Bool > a > a` and that `a` doesn't match `Char` (in the second argument of the call site in the body of `f`). This is unsatisfactory because clearly `g` should be *instantiated* at `Char`. The manual does say that polymorphic recursion isn't available with partial type signatures, and I suppose this is an example of polymorphic (mutual) recursion.
Example 3:
```hs
f :: forall a. _ > a > a
f _ x = snd (g True 'a', x)
where
g :: forall b. _ > b > b
g _ y = f 'x' y
```
This is accepted. This is the same example as the last one, but now `g` is local. It does not capture any variables (including type variables) from `f`, so it seems to me that it should be equivalent to Example 2. But somehow GHC is clever enough to accept.
Example 4:
```hs
thdOf3 (_, _, c) = c
f :: forall a. _ > a > a
f _ x = thdOf3 (g True 'a', g False 5, x)
where
g :: forall b. _ > b > b
g _ y = f 'x' y
```
This works, too. Note that `g` is applied at several different types, so it really is being generalized.
Example 5:
```hs
f :: Int > forall a. _ > a > a
f n _ x = snd (g n True 'a', x)
g :: Int > forall b. _ > b > b
g n _ x = f n 'x' x
```
This is accepted. This is the same as Example 2, but each function now takes an `Int`, which is simply passed back and forth. Evidently, when you write the type nonprenex, polymorphic recursion is OK.
Example 6:
```hs
f :: Int > forall a. _ > a > a
f n _ x = snd (f n True 'x', x)
```
This is accepted, even though it's blatantly using polymorphic recursion.
Example 7:
```hs
f :: forall a. _ > a > a
f _ x = snd (f True 'x', x)
```
This is rejected as polymorphically recursive.

Something is fishy here. It's not the explicit prenex `forall`s  leaving those out doesn't change the behavior. I guess my big question is this:
 If the user quantifies a partial type signature (either by using `forall`, or just using an outofscope type variable and using Haskell's implicit quantification), why can't we use polymorphic recursion with that variable? I understand why we can't use polymorphic recursion with wildcards.

A little background for context: I'm struggling (in my work on #14066) with GHC's use of `SigTv`s for partial type signatures. I don't have a better suggestion, but `SigTv`s never make me feel good.
<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 + mutual recursion = confusion","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":"I'm trying to understand better how partial type signatures interact with mutual recursion. This is all in 8.4.1alpha1.\r\n\r\nExample 1:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = g True x\r\n\r\ng :: forall b. _ > b > b\r\ng _ x = f 'x' x\r\n}}}\r\n\r\nThis works  no problem.\r\n\r\nExample 2:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = snd (g True 'a', x)\r\n\r\ng :: forall b. _ > b > b\r\ng _ x = f 'x' x\r\n}}}\r\n\r\nThis fails, explaining that GHC inferred `g :: Bool > a > a` and that `a` doesn't match `Char` (in the second argument of the call site in the body of `f`). This is unsatisfactory because clearly `g` should be ''instantiated'' at `Char`. The manual does say that polymorphic recursion isn't available with partial type signatures, and I suppose this is an example of polymorphic (mutual) recursion.\r\n\r\nExample 3:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = snd (g True 'a', x)\r\n where\r\n g :: forall b. _ > b > b\r\n g _ y = f 'x' y\r\n}}}\r\n\r\nThis is accepted. This is the same example as the last one, but now `g` is local. It does not capture any variables (including type variables) from `f`, so it seems to me that it should be equivalent to Example 2. But somehow GHC is clever enough to accept.\r\n\r\nExample 4:\r\n\r\n{{{#!hs\r\nthdOf3 (_, _, c) = c\r\n\r\nf :: forall a. _ > a > a\r\nf _ x = thdOf3 (g True 'a', g False 5, x)\r\n where\r\n g :: forall b. _ > b > b\r\n g _ y = f 'x' y\r\n}}}\r\n\r\nThis works, too. Note that `g` is applied at several different types, so it really is being generalized.\r\n\r\nExample 5:\r\n\r\n{{{#!hs\r\nf :: Int > forall a. _ > a > a\r\nf n _ x = snd (g n True 'a', x)\r\n\r\ng :: Int > forall b. _ > b > b\r\ng n _ x = f n 'x' x\r\n}}}\r\n\r\nThis is accepted. This is the same as Example 2, but each function now takes an `Int`, which is simply passed back and forth. Evidently, when you write the type nonprenex, polymorphic recursion is OK.\r\n\r\nExample 6:\r\n\r\n{{{#!hs\r\nf :: Int > forall a. _ > a > a\r\nf n _ x = snd (f n True 'x', x)\r\n}}}\r\n\r\nThis is accepted, even though it's blatantly using polymorphic recursion.\r\n\r\nExample 7:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = snd (f True 'x', x)\r\n}}}\r\n\r\nThis is rejected as polymorphically recursive.\r\n\r\n\r\n\r\nSomething is fishy here. It's not the explicit prenex `forall`s  leaving those out doesn't change the behavior. I guess my big question is this:\r\n\r\n* If the user quantifies a partial type signature (either by using `forall`, or just using an outofscope type variable and using Haskell's implicit quantification), why can't we use polymorphic recursion with that variable? I understand why we can't use polymorphic recursion with wildcards.\r\n\r\n\r\n\r\nA little background for context: I'm struggling (in my work on #14066) with GHC's use of `SigTv`s for partial type signatures. I don't have a better suggestion, but `SigTv`s never make me feel good.","type_of_failure":"OtherFailure","blocking":[]} >I'm trying to understand better how partial type signatures interact with mutual recursion. This is all in 8.4.1alpha1.
Example 1:
```hs
f :: forall a. _ > a > a
f _ x = g True x
g :: forall b. _ > b > b
g _ x = f 'x' x
```
This works  no problem.
Example 2:
```hs
f :: forall a. _ > a > a
f _ x = snd (g True 'a', x)
g :: forall b. _ > b > b
g _ x = f 'x' x
```
This fails, explaining that GHC inferred `g :: Bool > a > a` and that `a` doesn't match `Char` (in the second argument of the call site in the body of `f`). This is unsatisfactory because clearly `g` should be *instantiated* at `Char`. The manual does say that polymorphic recursion isn't available with partial type signatures, and I suppose this is an example of polymorphic (mutual) recursion.
Example 3:
```hs
f :: forall a. _ > a > a
f _ x = snd (g True 'a', x)
where
g :: forall b. _ > b > b
g _ y = f 'x' y
```
This is accepted. This is the same example as the last one, but now `g` is local. It does not capture any variables (including type variables) from `f`, so it seems to me that it should be equivalent to Example 2. But somehow GHC is clever enough to accept.
Example 4:
```hs
thdOf3 (_, _, c) = c
f :: forall a. _ > a > a
f _ x = thdOf3 (g True 'a', g False 5, x)
where
g :: forall b. _ > b > b
g _ y = f 'x' y
```
This works, too. Note that `g` is applied at several different types, so it really is being generalized.
Example 5:
```hs
f :: Int > forall a. _ > a > a
f n _ x = snd (g n True 'a', x)
g :: Int > forall b. _ > b > b
g n _ x = f n 'x' x
```
This is accepted. This is the same as Example 2, but each function now takes an `Int`, which is simply passed back and forth. Evidently, when you write the type nonprenex, polymorphic recursion is OK.
Example 6:
```hs
f :: Int > forall a. _ > a > a
f n _ x = snd (f n True 'x', x)
```
This is accepted, even though it's blatantly using polymorphic recursion.
Example 7:
```hs
f :: forall a. _ > a > a
f _ x = snd (f True 'x', x)
```
This is rejected as polymorphically recursive.

Something is fishy here. It's not the explicit prenex `forall`s  leaving those out doesn't change the behavior. I guess my big question is this:
 If the user quantifies a partial type signature (either by using `forall`, or just using an outofscope type variable and using Haskell's implicit quantification), why can't we use polymorphic recursion with that variable? I understand why we can't use polymorphic recursion with wildcards.

A little background for context: I'm struggling (in my work on #14066) with GHC's use of `SigTv`s for partial type signatures. I don't have a better suggestion, but `SigTv`s never make me feel good.
<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 + mutual recursion = confusion","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":"I'm trying to understand better how partial type signatures interact with mutual recursion. This is all in 8.4.1alpha1.\r\n\r\nExample 1:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = g True x\r\n\r\ng :: forall b. _ > b > b\r\ng _ x = f 'x' x\r\n}}}\r\n\r\nThis works  no problem.\r\n\r\nExample 2:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = snd (g True 'a', x)\r\n\r\ng :: forall b. _ > b > b\r\ng _ x = f 'x' x\r\n}}}\r\n\r\nThis fails, explaining that GHC inferred `g :: Bool > a > a` and that `a` doesn't match `Char` (in the second argument of the call site in the body of `f`). This is unsatisfactory because clearly `g` should be ''instantiated'' at `Char`. The manual does say that polymorphic recursion isn't available with partial type signatures, and I suppose this is an example of polymorphic (mutual) recursion.\r\n\r\nExample 3:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = snd (g True 'a', x)\r\n where\r\n g :: forall b. _ > b > b\r\n g _ y = f 'x' y\r\n}}}\r\n\r\nThis is accepted. This is the same example as the last one, but now `g` is local. It does not capture any variables (including type variables) from `f`, so it seems to me that it should be equivalent to Example 2. But somehow GHC is clever enough to accept.\r\n\r\nExample 4:\r\n\r\n{{{#!hs\r\nthdOf3 (_, _, c) = c\r\n\r\nf :: forall a. _ > a > a\r\nf _ x = thdOf3 (g True 'a', g False 5, x)\r\n where\r\n g :: forall b. _ > b > b\r\n g _ y = f 'x' y\r\n}}}\r\n\r\nThis works, too. Note that `g` is applied at several different types, so it really is being generalized.\r\n\r\nExample 5:\r\n\r\n{{{#!hs\r\nf :: Int > forall a. _ > a > a\r\nf n _ x = snd (g n True 'a', x)\r\n\r\ng :: Int > forall b. _ > b > b\r\ng n _ x = f n 'x' x\r\n}}}\r\n\r\nThis is accepted. This is the same as Example 2, but each function now takes an `Int`, which is simply passed back and forth. Evidently, when you write the type nonprenex, polymorphic recursion is OK.\r\n\r\nExample 6:\r\n\r\n{{{#!hs\r\nf :: Int > forall a. _ > a > a\r\nf n _ x = snd (f n True 'x', x)\r\n}}}\r\n\r\nThis is accepted, even though it's blatantly using polymorphic recursion.\r\n\r\nExample 7:\r\n\r\n{{{#!hs\r\nf :: forall a. _ > a > a\r\nf _ x = snd (f True 'x', x)\r\n}}}\r\n\r\nThis is rejected as polymorphically recursive.\r\n\r\n\r\n\r\nSomething is fishy here. It's not the explicit prenex `forall`s  leaving those out doesn't change the behavior. I guess my big question is this:\r\n\r\n* If the user quantifies a partial type signature (either by using `forall`, or just using an outofscope type variable and using Haskell's implicit quantification), why can't we use polymorphic recursion with that variable? I understand why we can't use polymorphic recursion with wildcards.\r\n\r\n\r\n\r\nA little background for context: I'm struggling (in my work on #14066) with GHC's use of `SigTv`s for partial type signatures. I don't have a better suggestion, but `SigTv`s never make me feel good.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14040Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]20200123T19:31:02ZRyan ScottTyped holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2](Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type > Type where
WeirdNil :: WeirdList a
WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs
> p _ (WeirdCons x xs))
> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
> (forall y. p x0 t3 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs
> p (WeirdList z) t2 xs
> p z t1 ('WeirdCons x xs))
> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
> (forall y. p x0 t0 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))
> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

24  > (forall (y :: Type). p _ WeirdNil)
 ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64unknownlinux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #13877 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type > Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs\r\n > p _ (WeirdCons x xs))\r\n > p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n > (forall y. p x0 t3 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs\r\n > p (WeirdList z) t2 xs\r\n > p z t1 ('WeirdCons x xs))\r\n > p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n > (forall y. p x0 t0 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))\r\n > p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n24  > (forall (y :: Type). p _ WeirdNil)\r\n  ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64unknownlinux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} >(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type > Type where
WeirdNil :: WeirdList a
WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs
> p _ (WeirdCons x xs))
> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
> (forall y. p x0 t3 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs
> p (WeirdList z) t2 xs
> p z t1 ('WeirdCons x xs))
> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
> (forall y. p x0 t0 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))
> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

24  > (forall (y :: Type). p _ WeirdNil)
 ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64unknownlinux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #13877 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type > Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs\r\n > p _ (WeirdCons x xs))\r\n > p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n > (forall y. p x0 t3 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs\r\n > p (WeirdList z) t2 xs\r\n > p z t1 ('WeirdCons x xs))\r\n > p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n > (forall y. p x0 t0 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))\r\n > p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n24  > (forall (y :: Type). p _ WeirdNil)\r\n  ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64unknownlinux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/11641Allow wildcards for parameters functionally determined (also type synonyms)20190707T18:29:20ZIcelandjackAllow wildcards for parameters functionally determined (also type synonyms)```hs
class F a b  a > b where
foo :: a
 ...
myFoo :: F a b => a
myFoo = foo
```
Since *b* is not used and fully determined by *a* could the restriction on wildcards in constraints be lifted?
```hs
myFoo :: F a _ => a
myFoo = foo
```
and eventually hiding it behind a type synonym:
```hs
type F' a = F a _
myFoo' :: F' a => a
myFoo' = foo
```
I raised this issue at ICFP 2014, I haven't looked into whether dominique's response to [my comment](https://haskellphabricator.global.ssl.fastly.net/D168#4818) applies.

I could achieve similar things with a type family but not quite.

Or CPP :)```hs
class F a b  a > b where
foo :: a
 ...
myFoo :: F a b => a
myFoo = foo
```
Since *b* is not used and fully determined by *a* could the restriction on wildcards in constraints be lifted?
```hs
myFoo :: F a _ => a
myFoo = foo
```
and eventually hiding it behind a type synonym:
```hs
type F' a = F a _
myFoo' :: F' a => a
myFoo' = foo
```
I raised this issue at ICFP 2014, I haven't looked into whether dominique's response to [my comment](https://haskellphabricator.global.ssl.fastly.net/D168#4818) applies.

I could achieve similar things with a type family but not quite.

Or CPP :)https://gitlab.haskell.org/ghc/ghc//issues/10875Unexpected defaulting of partial type signatures and inconsistent behaviour w...20190707T18:33:20ZholzenspUnexpected defaulting of partial type signatures and inconsistent behaviour when fdefertypedholes is set.Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program:
```hs
{#LANGUAGE PartialTypeSignatures #}
{#LANGUAGE NamedWildCards #}
{#LANGUAGE NoMonomorphismRestriction #}
foo :: _ => _outer
foo x = round $ (undefined::_inner) (1 + x)
```
This produces the following output in GHCi:
```
Foo.hs:5:8: Warning:
Found hole ‘_’ with inferred constraints: (Integral b, Num a)
In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning:
Found hole ‘_outer’ with type: a > b
Where: ‘b’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a > b
at Foo.hs:6:1
‘a’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a > b
at Foo.hs:6:1
In the type signature for ‘foo’: _ => _outer
Foo.hs:6:29: Warning:
Found hole ‘_inner’ with type: a > Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a > b
at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a > b (bound at Foo.hs:6:1)
In an expression type signature: _inner
In the expression: undefined :: _inner
In the second argument of ‘($)’, namely
‘(undefined :: _inner) (1 + x)’
Ok, modules loaded: Main.
```
The inferred constraints for `_` (which I can't give a name, unfortunately) and the type reported in place of `_outer` are exactly what I expected. The type for `_inner` surprises me. Okay, the type is ambiguous, so for anything as general as `undefined`, arguably, it would need to default to something.
Let's use a typed hole instead of `undefined`:
```hs
foo :: _ => _outer
foo x = round $ _hole (1 + x)
```
gives
```
Foo.hs:6:17:
Found hole ‘_hole’ with type: a > Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a > b (bound at Foo.hs:6:1)
In the expression: _hole
In the second argument of ‘($)’, namely ‘_hole (1 + x)’
In the expression: round $ _hole (1 + x)
Failed, modules loaded: none.
```
Holy Guacamole, it still defaults to `Double`. I would consider this a bug, because GHC is telling me, that whatever I put there must result in a `Double`, which is too restrictive to be true. However, I seem to recall from the OutsideIn paper that there were some cases, even without GADTs, where principality was difficult. Was this one of them?
Moving on, I was actually trying to get all my holes typed for me in one compiler execution. GHC behaves according to spec; typed holes produce errors by default and when something breaks on an error, it doesn't produce the warnings for partial type signatures. Let's `fdefertypedholes` and compile again:
```
Prelude> :set fdefertypedholes
Prelude> :r
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:5:8: Warning:
Found hole ‘_’ with inferred constraints: ()
In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning:
Found hole ‘_outer’ with type: a > b
Where: ‘b’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
‘a’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
In the type signature for ‘foo’: _ => _outer
Foo.hs:6:17: Warning:
Found hole ‘_hole’ with type: a > Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a > b (bound at Foo.hs:6:1)
In the expression: _hole
In the second argument of ‘($)’, namely ‘_hole (1 + x)’
In the expression: round $ _hole (1 + x)
Ok, modules loaded: Main.
```
Surely, this must be wrong. Suddenly `()` is the inferred set of constraints and an unconstrained `a > b` will do for `_outer`. I would argue that the `1 +` still demainds `Num a` and that `round` still requires an instance of `Integral b`, even if `round`'s `RealFrac` constraint is satisfied by `_hole` producing a `Double`.
As said, maybe the erroneous types reported when `fdefertypedholes` are a separate issue from the type of `_hole` not being the principal type, but I'm unsure, so I reported them together.Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program:
```hs
{#LANGUAGE PartialTypeSignatures #}
{#LANGUAGE NamedWildCards #}
{#LANGUAGE NoMonomorphismRestriction #}
foo :: _ => _outer
foo x = round $ (undefined::_inner) (1 + x)
```
This produces the following output in GHCi:
```
Foo.hs:5:8: Warning:
Found hole ‘_’ with inferred constraints: (Integral b, Num a)
In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning:
Found hole ‘_outer’ with type: a > b
Where: ‘b’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a > b
at Foo.hs:6:1
‘a’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a > b
at Foo.hs:6:1
In the type signature for ‘foo’: _ => _outer
Foo.hs:6:29: Warning:
Found hole ‘_inner’ with type: a > Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: (Integral b, Num a) => a > b
at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a > b (bound at Foo.hs:6:1)
In an expression type signature: _inner
In the expression: undefined :: _inner
In the second argument of ‘($)’, namely
‘(undefined :: _inner) (1 + x)’
Ok, modules loaded: Main.
```
The inferred constraints for `_` (which I can't give a name, unfortunately) and the type reported in place of `_outer` are exactly what I expected. The type for `_inner` surprises me. Okay, the type is ambiguous, so for anything as general as `undefined`, arguably, it would need to default to something.
Let's use a typed hole instead of `undefined`:
```hs
foo :: _ => _outer
foo x = round $ _hole (1 + x)
```
gives
```
Foo.hs:6:17:
Found hole ‘_hole’ with type: a > Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a > b (bound at Foo.hs:6:1)
In the expression: _hole
In the second argument of ‘($)’, namely ‘_hole (1 + x)’
In the expression: round $ _hole (1 + x)
Failed, modules loaded: none.
```
Holy Guacamole, it still defaults to `Double`. I would consider this a bug, because GHC is telling me, that whatever I put there must result in a `Double`, which is too restrictive to be true. However, I seem to recall from the OutsideIn paper that there were some cases, even without GADTs, where principality was difficult. Was this one of them?
Moving on, I was actually trying to get all my holes typed for me in one compiler execution. GHC behaves according to spec; typed holes produce errors by default and when something breaks on an error, it doesn't produce the warnings for partial type signatures. Let's `fdefertypedholes` and compile again:
```
Prelude> :set fdefertypedholes
Prelude> :r
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:5:8: Warning:
Found hole ‘_’ with inferred constraints: ()
In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning:
Found hole ‘_outer’ with type: a > b
Where: ‘b’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
‘a’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
In the type signature for ‘foo’: _ => _outer
Foo.hs:6:17: Warning:
Found hole ‘_hole’ with type: a > Double
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: a > b at Foo.hs:6:1
Relevant bindings include
x :: a (bound at Foo.hs:6:5)
foo :: a > b (bound at Foo.hs:6:1)
In the expression: _hole
In the second argument of ‘($)’, namely ‘_hole (1 + x)’
In the expression: round $ _hole (1 + x)
Ok, modules loaded: Main.
```
Surely, this must be wrong. Suddenly `()` is the inferred set of constraints and an unconstrained `a > b` will do for `_outer`. I would argue that the `1 +` still demainds `Num a` and that `round` still requires an instance of `Integral b`, even if `round`'s `RealFrac` constraint is satisfied by `_hole` producing a `Double`.
As said, maybe the erroneous types reported when `fdefertypedholes` are a separate issue from the type of `_hole` not being the principal type, but I'm unsure, so I reported them together.https://gitlab.haskell.org/ghc/ghc//issues/10783Partial type signatures should work in pattern synonym signatures20190707T18:33:54ZMatthew PickeringPartial type signatures should work in pattern synonym signatures```hs
{# LANGUAGE PatternSynonyms #}
pattern MyJust :: _
pattern MyJust a = Just a
```
GHC can correctly infer the type for the pattern without the type signature so (to me) it is unexpected that this inferred type is not reported to me when using partial type signatures. It just seems to not be implemented currently.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.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 should work with pattern synonym signatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n\r\n{# LANGUAGE PatternSynonyms #}\r\n\r\npattern MyJust :: _\r\npattern MyJust a = Just a\r\n\r\n}}}\r\n\r\nGHC can correctly infer the type for the pattern without the type signature so (to me) it is unexpected that this inferred type is not reported to me when using partial type signatures. It just seems to not be implemented currently. \r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE PatternSynonyms #}
pattern MyJust :: _
pattern MyJust a = Just a
```
GHC can correctly infer the type for the pattern without the type signature so (to me) it is unexpected that this inferred type is not reported to me when using partial type signatures. It just seems to not be implemented currently.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.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 should work with pattern synonym signatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n\r\n{# LANGUAGE PatternSynonyms #}\r\n\r\npattern MyJust :: _\r\npattern MyJust a = Just a\r\n\r\n}}}\r\n\r\nGHC can correctly infer the type for the pattern without the type signature so (to me) it is unexpected that this inferred type is not reported to me when using partial type signatures. It just seems to not be implemented currently. \r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >