GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200720T14:04:52Zhttps://gitlab.haskell.org/ghc/ghc//issues/17567Never `Any`ify during kind inference20200720T14:04:52ZRichard Eisenbergrae@richarde.devNever `Any`ify during kind inference#14198 concludes with a new plan: never `Any`ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`ification during kind inference:
#17301:
```hs
data B a
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
```
The RHS of that type family equation is really `MkATySing @alpha (SB @alpha)`, and the `alpha` gets zonked to `Any`.
#14198:
```hs
type T = forall a. Proxy a
```
The RHS of the type synonym is really `forall (a :: kappa). Proxy @kappa a`, and the `kappa` gets zonked to `Any`.
#17562:
```hs
class (forall a. a b ~ a c) => C b c
```
The superclass constraint is really `forall (a :: Type > kappa). (~) @kappa (a b) (a c))`, and the `kappa` gets zonked to `Any`.
We want to stop zonking to `Any`, preferring to error instead. But how should we implement?
* Option A: Use a new variant of `ZonkFlexi`, a choice carried around in a `ZonkEnv` that says what to do with empty metavariables. The new choice would cause an error. This new form of `ZonkFlexi` would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, toplevel type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
* Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of `ZonkFlexi` would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
* Option C: Look for all cases where `Any`ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new `ZonkFlexi` that panics. That way, we'll know if we've missed a case.
* Simon below proposes Option D: Zap to `Type` instead of `Any`. I (Richard) view D as an addon to any of the above plans. Because `Type` is not always wellkinded, we can only zap to `Type` sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat `Type` specially with XPolyKinds` enabled, and so I'd prefer that we don't do this.
* EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for `Wurble`" bits). This would mean building up useful contexts in the zonker.
* Option F: The new constructor for `ZonkFlexi` could carry the toplevel type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?#14198 concludes with a new plan: never `Any`ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`ification during kind inference:
#17301:
```hs
data B a
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
```
The RHS of that type family equation is really `MkATySing @alpha (SB @alpha)`, and the `alpha` gets zonked to `Any`.
#14198:
```hs
type T = forall a. Proxy a
```
The RHS of the type synonym is really `forall (a :: kappa). Proxy @kappa a`, and the `kappa` gets zonked to `Any`.
#17562:
```hs
class (forall a. a b ~ a c) => C b c
```
The superclass constraint is really `forall (a :: Type > kappa). (~) @kappa (a b) (a c))`, and the `kappa` gets zonked to `Any`.
We want to stop zonking to `Any`, preferring to error instead. But how should we implement?
* Option A: Use a new variant of `ZonkFlexi`, a choice carried around in a `ZonkEnv` that says what to do with empty metavariables. The new choice would cause an error. This new form of `ZonkFlexi` would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, toplevel type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
* Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of `ZonkFlexi` would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
* Option C: Look for all cases where `Any`ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new `ZonkFlexi` that panics. That way, we'll know if we've missed a case.
* Simon below proposes Option D: Zap to `Type` instead of `Any`. I (Richard) view D as an addon to any of the above plans. Because `Type` is not always wellkinded, we can only zap to `Type` sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat `Type` specially with XPolyKinds` enabled, and so I'd prefer that we don't do this.
* EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for `Wurble`" bits). This would mean building up useful contexts in the zonker.
* Option F: The new constructor for `ZonkFlexi` could carry the toplevel type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?https://gitlab.haskell.org/ghc/ghc//issues/14420Data families should not instantiate to nonType kinds20190710T12:48:27ZRichard Eisenbergrae@richarde.devData families should not instantiate to nonType kinds```hs
data family Any :: k  allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data families should not instantiate to nonType kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k  allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} >```hs
data family Any :: k  allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data families should not instantiate to nonType kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k  allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/12612Allow kinds of associated types to depend on earlier associated types20190707T18:25:50ZdavemenendezAllow kinds of associated types to depend on earlier associated typesGHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t > Type
m :: t > T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘K t > Type’
```
See [email discussion](https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html). This is connected to #12088, at least as far as defining instances of C.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow kinds of associated types to depend on earlier associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects the following code:\r\n\r\n{{{#!hs\r\nclass C t where\r\n type K t :: Type\r\n type T t :: K t > Type\r\n\r\n m :: t > T t a\r\n}}}\r\n\r\nwith this error message\r\n\r\n{{{\r\n • Type constructor ‘K’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘K t > Type’\r\n}}}\r\n\r\nSee [https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html email discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} >GHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t > Type
m :: t > T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘K t > Type’
```
See [email discussion](https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html). This is connected to #12088, at least as far as defining instances of C.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow kinds of associated types to depend on earlier associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects the following code:\r\n\r\n{{{#!hs\r\nclass C t where\r\n type K t :: Type\r\n type T t :: K t > Type\r\n\r\n m :: t > T t a\r\n}}}\r\n\r\nwith this error message\r\n\r\n{{{\r\n • Type constructor ‘K’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘K t > Type’\r\n}}}\r\n\r\nSee [https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html email discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/18753Tighten up the treatment of loose types in the solver20200927T02:25:14ZRichard Eisenbergrae@richarde.devTighten up the treatment of loose types in the solver`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.https://gitlab.haskell.org/ghc/ghc//issues/18714GHC panic (tcInvisibleTyBinder) when using constraint in a kind20200921T21:17:06ZRyan ScottGHC panic (tcInvisibleTyBinder) when using constraint in a kindThe following program will panic when compiled with GHC 8.10 or HEAD:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import GHC.Exts
type Id a = a
type F = Id (Any :: forall a. Show a => a > a)
```
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.2:
tcInvisibleTyBinder
Show a_avp[sk:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/Inst.hs:460:5 in ghc:Inst
```
I'm a bit surprised that this happens, since GHC has a validity check intended to rule out the use of arbitrary constraints in kinds. This check is implemented by [`GHC.Tc.Validity.allConstraintsAllowed`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L473480):
```hs
allConstraintsAllowed :: UserTypeCtxt > Bool
 We don't allow arbitrary constraints in kinds
allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
allConstraintsAllowed _ = True
```
Upon closer inspection, `allConstraintsAllowed` appears to be incomplete. Compare this to [`GHC.Tc.Validity.vdqAllowed`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L496507), which must also make a distinction between types and kinds:
```hs
vdqAllowed :: UserTypeCtxt > Bool
 Currently allowed in the kinds of types...
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
vdqAllowed (TySynKindCtxt {}) = True
vdqAllowed (TyFamResKindCtxt {}) = True
 ...but not in the types of terms.
...
```
Note that `vdqAllowed` identifies more `UserTypeCtxt`s as being kindlevel positions than `allConstraintsAllowed` does. Crucially, `allConstraintsAllowed` omits a case for `KindSigCtxt`. If I add such as case:
```diff
diff git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..39ebc260da 100644
 a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ 479,6 +479,7 @@ allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
+allConstraintsAllowed (KindSigCtxt {}) = False
allConstraintsAllowed _ = True
  Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
```
Then the program above no longer panics:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:14: error:
• Illegal constraint in a kind: forall a. Show a => a > a
• In the first argument of ‘Id’, namely
‘(Any :: forall a. Show a => a > a)’
In the type ‘Id (Any :: forall a. Show a => a > a)’
In the type declaration for ‘F’

11  type F = Id (Any :: forall a. Show a => a > a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```The following program will panic when compiled with GHC 8.10 or HEAD:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import GHC.Exts
type Id a = a
type F = Id (Any :: forall a. Show a => a > a)
```
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.2:
tcInvisibleTyBinder
Show a_avp[sk:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/Inst.hs:460:5 in ghc:Inst
```
I'm a bit surprised that this happens, since GHC has a validity check intended to rule out the use of arbitrary constraints in kinds. This check is implemented by [`GHC.Tc.Validity.allConstraintsAllowed`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L473480):
```hs
allConstraintsAllowed :: UserTypeCtxt > Bool
 We don't allow arbitrary constraints in kinds
allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
allConstraintsAllowed _ = True
```
Upon closer inspection, `allConstraintsAllowed` appears to be incomplete. Compare this to [`GHC.Tc.Validity.vdqAllowed`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L496507), which must also make a distinction between types and kinds:
```hs
vdqAllowed :: UserTypeCtxt > Bool
 Currently allowed in the kinds of types...
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
vdqAllowed (TySynKindCtxt {}) = True
vdqAllowed (TyFamResKindCtxt {}) = True
 ...but not in the types of terms.
...
```
Note that `vdqAllowed` identifies more `UserTypeCtxt`s as being kindlevel positions than `allConstraintsAllowed` does. Crucially, `allConstraintsAllowed` omits a case for `KindSigCtxt`. If I add such as case:
```diff
diff git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..39ebc260da 100644
 a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ 479,6 +479,7 @@ allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
+allConstraintsAllowed (KindSigCtxt {}) = False
allConstraintsAllowed _ = True
  Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
```
Then the program above no longer panics:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:14: error:
• Illegal constraint in a kind: forall a. Show a => a > a
• In the first argument of ‘Id’, namely
‘(Any :: forall a. Show a => a > a)’
In the type ‘Id (Any :: forall a. Show a => a > a)’
In the type declaration for ‘F’

11  type F = Id (Any :: forall a. Show a => a > a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc//issues/18689Why check for fdefertypeerrors in metaTyVarUpdateOK?20200921T22:31:11ZRichard Eisenbergrae@richarde.devWhy check for fdefertypeerrors in metaTyVarUpdateOK?Function `metaTyVarUpdateOK` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `preCheck` that deals with `badCoercionHoleCo`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Function `metaTyVarUpdateOK` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `preCheck` that deals with `badCoercionHoleCo`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/18308Order of StandaloneKindSignatures and CUSKs extensions significant20200626T16:28:20ZBjörn HegerforsOrder of StandaloneKindSignatures and CUSKs extensions significant## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding standalone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE CUSKs #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
but this doesn't:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE CUSKs #}
{# LANGUAGE StandaloneKindSignatures #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding standalone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE CUSKs #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
but this doesn't:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE CUSKs #}
{# LANGUAGE StandaloneKindSignatures #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc//issues/18062A cast might get in the way of instantiation20200427T10:20:56ZSimon Peyton JonesA cast might get in the way of instantiationSuppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kindchecks to
```
forall a. ((Eq a => Blah) > co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' < tc_hs_context mode ctxt
; ek < newOpenTypeKind  The body kind (result of the function) can
 be TYPE r, for any r, hence newOpenTypeKind
; ty' < tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) > co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{# LANGUAGE KindSignatures, TypeFamilies, DataKinds #}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a > Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a > Bool
Actual type: a0 > Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a > Bool’ has none
• Relevant bindings include
f :: Eq a => a > Bool (bound at Bug.hs:11:1)

11  f x = x == x
 ^^^^^^^^^^^^
```
Solution: teach instantiation to look through casts.Suppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kindchecks to
```
forall a. ((Eq a => Blah) > co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' < tc_hs_context mode ctxt
; ek < newOpenTypeKind  The body kind (result of the function) can
 be TYPE r, for any r, hence newOpenTypeKind
; ty' < tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) > co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{# LANGUAGE KindSignatures, TypeFamilies, DataKinds #}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a > Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a > Bool
Actual type: a0 > Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a > Bool’ has none
• Relevant bindings include
f :: Eq a => a > Bool (bound at Bug.hs:11:1)

11  f x = x == x
 ^^^^^^^^^^^^
```
Solution: teach instantiation to look through casts.https://gitlab.haskell.org/ghc/ghc//issues/17675eqType fails on comparing FunTys20200502T22:16:29ZRichard Eisenbergrae@richarde.deveqType fails on comparing FunTysSuppose I have `co :: IntRep ~ r` and `a :: TYPE IntRep`. Consider `t1 = a > ()` and `t2 = (a > TYPE co) > ()`. We have ``t1 `eqType` t2``, but if we call `splitTyConApp` on `t1` and `t2`, we'll get different arguments (the first arg in `t1` will be `IntRep` while the first arg in `t2` will be `r`). This violates property EQ of Note [Nontrivial definitional equality] in TyCoRep.
The fix is easy: in `nonDetCmpTypeX`, the `FunTy` case should recur into `nonDetCmpTypeX` for both argument and result. This does a kind check. Recurring into `go` skips the kind check.
Unfortunately, there are other places that also work with equality. This list includes at least
* [ ] `TcType.tc_eq_type`
* [ ] `CoreMap`
* [ ] Pure unifier in `Unify`, which probably also needs to recur in kinds on a `FunTy`. Or maybe this works via decomposition into a `TyConApp`, so all is OK. But it needs to be checked.
I believe Simon has some preliminary work on a branch.Suppose I have `co :: IntRep ~ r` and `a :: TYPE IntRep`. Consider `t1 = a > ()` and `t2 = (a > TYPE co) > ()`. We have ``t1 `eqType` t2``, but if we call `splitTyConApp` on `t1` and `t2`, we'll get different arguments (the first arg in `t1` will be `IntRep` while the first arg in `t2` will be `r`). This violates property EQ of Note [Nontrivial definitional equality] in TyCoRep.
The fix is easy: in `nonDetCmpTypeX`, the `FunTy` case should recur into `nonDetCmpTypeX` for both argument and result. This does a kind check. Recurring into `go` skips the kind check.
Unfortunately, there are other places that also work with equality. This list includes at least
* [ ] `TcType.tc_eq_type`
* [ ] `CoreMap`
* [ ] Pure unifier in `Unify`, which probably also needs to recur in kinds on a `FunTy`. Or maybe this works via decomposition into a `TyConApp`, so all is OK. But it needs to be checked.
I believe Simon has some preliminary work on a branch.https://gitlab.haskell.org/ghc/ghc//issues/17674Kill EQ120200518T17:02:46ZRichard Eisenbergrae@richarde.devKill EQ1Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
```
This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified `eqType` to look at the kind of arguments to `AppTy`s, then we wouldn't need EQ1, significantly simplifying `mkAppTy`. (Actually, it will just remove 2 lines. But it removes two calls to `decomposePiCos`. This will allow the one remaining call to this function to have more sway in the design of `decomposePiCos`, simplifying that bit of code, as well.)
Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245757.Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
```
This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified `eqType` to look at the kind of arguments to `AppTy`s, then we wouldn't need EQ1, significantly simplifying `mkAppTy`. (Actually, it will just remove 2 lines. But it removes two calls to `decomposePiCos`. This will allow the one remaining call to this function to have more sway in the design of `decomposePiCos`, simplifying that bit of code, as well.)
Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245757.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17621Typelevel multiplication parsed as application at kind *, no guidance provided20200105T03:00:19ZGeshTypelevel multiplication parsed as application at kind *, no guidance provided## Summary
Location of documentation issue: GHC error message
To reproduce:
```
Prelude> :set XDataKinds XTypeOperators
Prelude> import GHC.TypeNats
Prelude GHC.TypeNats> :k 2 * 4
<interactive>:1:1: error:
• Expected kind ‘* > GHC.Types.Nat > k0’,
but ‘2’ has kind ‘GHC.Types.Nat’
• In the type ‘2 * 4’
```
The error message is correct, but useless for someone getting started working
at the type level. At the very least, a suggestion of adding ```NoStarIsType```
is in order.
## Proposed improvements or changes
In a kinding error of form "expected ```* > r```, found ```s```" with
```StarInType```, suggest that this error might be the due to ```StarInType```.
## Environment
* GHC version used (if appropriate): 8.6.5. Asked on IRC, and @solonarv checked
this still exists in 8.8## Summary
Location of documentation issue: GHC error message
To reproduce:
```
Prelude> :set XDataKinds XTypeOperators
Prelude> import GHC.TypeNats
Prelude GHC.TypeNats> :k 2 * 4
<interactive>:1:1: error:
• Expected kind ‘* > GHC.Types.Nat > k0’,
but ‘2’ has kind ‘GHC.Types.Nat’
• In the type ‘2 * 4’
```
The error message is correct, but useless for someone getting started working
at the type level. At the very least, a suggestion of adding ```NoStarIsType```
is in order.
## Proposed improvements or changes
In a kinding error of form "expected ```* > r```, found ```s```" with
```StarInType```, suggest that this error might be the due to ```StarInType```.
## Environment
* GHC version used (if appropriate): 8.6.5. Asked on IRC, and @solonarv checked
this still exists in 8.8https://gitlab.haskell.org/ghc/ghc//issues/17562`Any` appearing in a quantified constraint20200118T00:00:32ZRichard Eisenbergrae@richarde.dev`Any` appearing in a quantified constraintIf I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.If I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.9.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17541Regression involving unboxed types and type families20191212T16:20:40ZMatthew PickeringRegression involving unboxed types and type familiesThis program compiles with 8.6.5 and 8.8.1 but not with HEAD.
```
{# LANGUAGE
MagicHash,
FlexibleInstances,
MultiParamTypeClasses,
TypeFamilies,
PolyKinds,
DataKinds,
FunctionalDependencies,
TypeFamilyDependencies #}
module A where
import GHC.Prim
import GHC.Exts
type family Rep rep where
Rep Int = IntRep
type family Unboxed rep = (urep :: TYPE (Rep rep))  urep > rep where
Unboxed Int = Int#
```
```
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:20:17: error:
• Expected kind ‘TYPE (Rep rep)’,
but ‘Int#’ has kind ‘TYPE 'IntRep’
• In the type ‘Int#’
In the type family declaration for ‘Unboxed’

20  Unboxed Int = Int#
 ^^^^
```This program compiles with 8.6.5 and 8.8.1 but not with HEAD.
```
{# LANGUAGE
MagicHash,
FlexibleInstances,
MultiParamTypeClasses,
TypeFamilies,
PolyKinds,
DataKinds,
FunctionalDependencies,
TypeFamilyDependencies #}
module A where
import GHC.Prim
import GHC.Exts
type family Rep rep where
Rep Int = IntRep
type family Unboxed rep = (urep :: TYPE (Rep rep))  urep > rep where
Unboxed Int = Int#
```
```
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:20:17: error:
• Expected kind ‘TYPE (Rep rep)’,
but ‘Int#’ has kind ‘TYPE 'IntRep’
• In the type ‘Int#’
In the type family declaration for ‘Unboxed’

20  Unboxed Int = Int#
 ^^^^
```https://gitlab.haskell.org/ghc/ghc//issues/17368Implement homogeneous equality20200310T14:21:59ZRichard Eisenbergrae@richarde.devImplement homogeneous equalityAs observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/deproles/deproles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the typechecker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/phase2, which has much discussion.As observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/deproles/deproles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the typechecker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/phase2, which has much discussion.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17327Kindchecking associated types20200218T16:17:45ZmniipKindchecking associated types## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeApplications #}
class C (k :: *) (a :: *) where
type F k a :: k
data D k (x :: k)
instance C k (D k x) where
type F k (D k x) = x  good
instance (k ~ l) => C l (D k x) where
type F l (D k x) = x  bad
{
b.hs:11:22: error:
• Expected kind ‘l’, but ‘x’ has kind ‘k’
• In the type ‘x’
In the type instance declaration for ‘F’
In the instance declaration for ‘C l (D k x)’

11  type F l (D k x) = x  bad
 ^
}
```
## Expected behavior
The second instance should kindcheck (it has better instance resolution properties than the first which is why we want it).
## Environment
Tested on GHC 8.6.5 and GHC HEAD## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeApplications #}
class C (k :: *) (a :: *) where
type F k a :: k
data D k (x :: k)
instance C k (D k x) where
type F k (D k x) = x  good
instance (k ~ l) => C l (D k x) where
type F l (D k x) = x  bad
{
b.hs:11:22: error:
• Expected kind ‘l’, but ‘x’ has kind ‘k’
• In the type ‘x’
In the type instance declaration for ‘F’
In the instance declaration for ‘C l (D k x)’

11  type F l (D k x) = x  bad
 ^
}
```
## Expected behavior
The second instance should kindcheck (it has better instance resolution properties than the first which is why we want it).
## Environment
Tested on GHC 8.6.5 and GHC HEADhttps://gitlab.haskell.org/ghc/ghc//issues/17131Kind inference bug in type family declaration20200513T09:45:32ZSimon Peyton JonesKind inference bug in type family declarationConsider this (cut down from #17113)
```
{# LANGUAGE MagicHash, UnboxedTuples, TypeInType, TypeFamilies, TypeOperators #}
module Test where
import GHC.Exts
type family TypeReps xs where
TypeReps '[] = '[]
TypeReps ((a::TYPE k) ': as) = k ': TypeReps as
type family Tuple# xs = (t :: TYPE ('TupleRep (TypeReps xs))) where
Tuple# '[a] = (# a #)
```
This compiles fine with GHC 8.6.4, but fails thus with HEAD:
```
T17113.hs:14:34: error:
• Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
• In the type ‘(# a #)’
In the type family declaration for ‘Tuple#’

14  Tuple# '[a] = (# a #)
 ^^^^^^^
```
Notice that free `xs` in the error message which is completely bogus. Something is badly wrong.Consider this (cut down from #17113)
```
{# LANGUAGE MagicHash, UnboxedTuples, TypeInType, TypeFamilies, TypeOperators #}
module Test where
import GHC.Exts
type family TypeReps xs where
TypeReps '[] = '[]
TypeReps ((a::TYPE k) ': as) = k ': TypeReps as
type family Tuple# xs = (t :: TYPE ('TupleRep (TypeReps xs))) where
Tuple# '[a] = (# a #)
```
This compiles fine with GHC 8.6.4, but fails thus with HEAD:
```
T17113.hs:14:34: error:
• Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
• In the type ‘(# a #)’
In the type family declaration for ‘Tuple#’

14  Tuple# '[a] = (# a #)
 ^^^^^^^
```
Notice that free `xs` in the error message which is completely bogus. Something is badly wrong.https://gitlab.haskell.org/ghc/ghc//issues/16902Compiletime stack overflow exception in GHC HEAD only20190705T07:29:45ZRyan ScottCompiletime stack overflow exception in GHC HEAD onlyIf I compile the following program in GHC HEAD:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data F (a :: k) :: (a ~~ k) => Type where
MkF :: F a
```
Then it simply loops until the stack overflows:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.9.0.20190620: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
*** Exception: stack overflow
```
This isn't strictly a regression since writing equality constraints in kinds (like in the kind of `F`) is a featurette that GHC has only really supported properly as of HEAD, although it is worth noting that previous versions of GHC did not exhibit this behavior.If I compile the following program in GHC HEAD:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data F (a :: k) :: (a ~~ k) => Type where
MkF :: F a
```
Then it simply loops until the stack overflows:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.9.0.20190620: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
*** Exception: stack overflow
```
This isn't strictly a regression since writing equality constraints in kinds (like in the kind of `F`) is a featurette that GHC has only really supported properly as of HEAD, although it is worth noting that previous versions of GHC did not exhibit this behavior.8.10.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc//issues/16635Scoped kind variables are broken20190925T18:06:23ZVladislav ZavialovScoped kind variables are broken# Summary
This does work:
```haskell
 f :: [a > Either a ()]
f = [Left @a :: forall a. a > Either a ()]
````
This does not:
```haskell
 type F :: [a > Either a ()]
type F = '[Left @a :: forall a. a > Either a ()]
```
An unfortunate asymmetry between terms & types. See a related discussion at https://gitlab.haskell.org/ghc/ghc/wikis/ghckinds/kindinference/tlks
# Steps to reproduce
```
ghci> :set XScopedTypeVariables XDataKinds XPolyKinds XTypeApplications
ghci> type F = '[Left @a :: forall a. a > Either a ()]
<interactive>:3:18: error: Not in scope: type variable ‘a’
```
# Expected behavior
No error.
# Environment
* GHC version used: HEAD.# Summary
This does work:
```haskell
 f :: [a > Either a ()]
f = [Left @a :: forall a. a > Either a ()]
````
This does not:
```haskell
 type F :: [a > Either a ()]
type F = '[Left @a :: forall a. a > Either a ()]
```
An unfortunate asymmetry between terms & types. See a related discussion at https://gitlab.haskell.org/ghc/ghc/wikis/ghckinds/kindinference/tlks
# Steps to reproduce
```
ghci> :set XScopedTypeVariables XDataKinds XPolyKinds XTypeApplications
ghci> type F = '[Left @a :: forall a. a > Either a ()]
<interactive>:3:18: error: Not in scope: type variable ‘a’
```
# Expected behavior
No error.
# Environment
* GHC version used: HEAD.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/16600Higherrank kinds lead to substitution assertion failure20190608T12:32:36ZRichard Eisenbergrae@richarde.devHigherrank kinds lead to substitution assertion failure# Summary
In a `DEBUG` compiler, I see an assertion failure in substitution while abusing GHC.
# Steps to reproduce
Compile this on a `DEBUG` compiler:
```hs
data Q :: forall d. Type
data HR :: (forall d. Type) > Type
x :: HR Q
x = undefined
```
# Expected behavior
Type error: the inferred kind of `HR` quantifies the kind of `d` outside the higherrank argument.
# Environment
* GHC version used: HEAD# Summary
In a `DEBUG` compiler, I see an assertion failure in substitution while abusing GHC.
# Steps to reproduce
Compile this on a `DEBUG` compiler:
```hs
data Q :: forall d. Type
data HR :: (forall d. Type) > Type
x :: HR Q
x = undefined
```
# Expected behavior
Type error: the inferred kind of `HR` quantifies the kind of `d` outside the higherrank argument.
# Environment
* GHC version used: HEADhttps://gitlab.haskell.org/ghc/ghc//issues/16391"Quantified type's kind mentions quantified type variable" error with fancyk...20200727T08:24:27ZRyan Scott"Quantified type's kind mentions quantified type variable" error with fancykinded GADTGiven the following:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
import Data.Kind
type Const (a :: Type) (b :: Type) = a
```
GHC happily accepts these definitions:
```hs
type family F :: Const Type a where
F = Int
type TS = (Int :: Const Type a)
```
However, the situation becomes murkier with data types. For some reason, GHC //rejects// this definition:
```hs
data T :: Const Type a where
MkT :: T
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Bug.hs:14:3: error:
• Quantified type's kind mentions quantified type variable
(skolem escape)
type: forall a1. T
of kind: Const * a
• In the definition of data constructor ‘MkT’
In the data type declaration for ‘T’

14  MkT :: T
 ^^^^^^^^
```
I'm not quite sure how to interpret that error message, but it seems fishy to me. Even fishier is the fact that GHC //accepts// this slight modification of `T`:
```hs
data T2 :: Const Type a > Type where
MkT2 :: T2 b
```
Quite mysterious.

I briefly looked into where this error message is being thrown from. It turns out if you make this oneline change to GHC:
```diff
diff git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 218f539c68..c7925767f9 100644
 a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ 635,7 +635,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
; check_type (ve{ve_tidy_env = env'}) tau
 Allow foralls to right of arrow
 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
+ ; checkTcM (not (any (`elemVarSet` exactTyCoVarsOfType phi_kind) tvs))
(forAllEscapeErr env' ty tau_kind)
}
where
```
Then GHC will accept `T`. Whether this change is the right choice to make, I don't think I'm qualified to say.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"\"Quantified type's kind mentions quantified type variable\" error with fancykinded GADT","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Given the following:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\nimport Data.Kind\r\n\r\ntype Const (a :: Type) (b :: Type) = a\r\n}}}\r\n\r\nGHC happily accepts these definitions:\r\n\r\n{{{#!hs\r\ntype family F :: Const Type a where\r\n F = Int\r\ntype TS = (Int :: Const Type a)\r\n}}}\r\n\r\nHowever, the situation becomes murkier with data types. For some reason, GHC //rejects// this definition:\r\n\r\n{{{#!hs\r\ndata T :: Const Type a where\r\n MkT :: T\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\n\r\nBug.hs:14:3: error:\r\n • Quantified type's kind mentions quantified type variable\r\n (skolem escape)\r\n type: forall a1. T\r\n of kind: Const * a\r\n • In the definition of data constructor ‘MkT’\r\n In the data type declaration for ‘T’\r\n \r\n14  MkT :: T\r\n  ^^^^^^^^\r\n}}}\r\n\r\nI'm not quite sure how to interpret that error message, but it seems fishy to me. Even fishier is the fact that GHC //accepts// this slight modification of `T`:\r\n\r\n{{{#!hs\r\ndata T2 :: Const Type a > Type where\r\n MkT2 :: T2 b\r\n}}}\r\n\r\nQuite mysterious.\r\n\r\n\r\n\r\nI briefly looked into where this error message is being thrown from. It turns out if you make this oneline change to GHC:\r\n\r\n{{{#!diff\r\ndiff git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs\r\nindex 218f539c68..c7925767f9 100644\r\n a/compiler/typecheck/TcValidity.hs\r\n+++ b/compiler/typecheck/TcValidity.hs\r\n@@ 635,7 +635,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt\r\n ; check_type (ve{ve_tidy_env = env'}) tau\r\n  Allow foralls to right of arrow\r\n\r\n ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))\r\n+ ; checkTcM (not (any (`elemVarSet` exactTyCoVarsOfType phi_kind) tvs))\r\n (forAllEscapeErr env' ty tau_kind)\r\n }\r\n where\r\n}}}\r\n\r\nThen GHC will accept `T`. Whether this change is the right choice to make, I don't think I'm qualified to say.","type_of_failure":"OtherFailure","blocking":[]} >Given the following:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
import Data.Kind
type Const (a :: Type) (b :: Type) = a
```
GHC happily accepts these definitions:
```hs
type family F :: Const Type a where
F = Int
type TS = (Int :: Const Type a)
```
However, the situation becomes murkier with data types. For some reason, GHC //rejects// this definition:
```hs
data T :: Const Type a where
MkT :: T
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Bug.hs:14:3: error:
• Quantified type's kind mentions quantified type variable
(skolem escape)
type: forall a1. T
of kind: Const * a
• In the definition of data constructor ‘MkT’
In the data type declaration for ‘T’

14  MkT :: T
 ^^^^^^^^
```
I'm not quite sure how to interpret that error message, but it seems fishy to me. Even fishier is the fact that GHC //accepts// this slight modification of `T`:
```hs
data T2 :: Const Type a > Type where
MkT2 :: T2 b
```
Quite mysterious.

I briefly looked into where this error message is being thrown from. It turns out if you make this oneline change to GHC:
```diff
diff git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 218f539c68..c7925767f9 100644
 a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ 635,7 +635,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
; check_type (ve{ve_tidy_env = env'}) tau
 Allow foralls to right of arrow
 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
+ ; checkTcM (not (any (`elemVarSet` exactTyCoVarsOfType phi_kind) tvs))
(forAllEscapeErr env' ty tau_kind)
}
where
```
Then GHC will accept `T`. Whether this change is the right choice to make, I don't think I'm qualified to say.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"\"Quantified type's kind mentions quantified type variable\" error with fancykinded GADT","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Given the following:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\nimport Data.Kind\r\n\r\ntype Const (a :: Type) (b :: Type) = a\r\n}}}\r\n\r\nGHC happily accepts these definitions:\r\n\r\n{{{#!hs\r\ntype family F :: Const Type a where\r\n F = Int\r\ntype TS = (Int :: Const Type a)\r\n}}}\r\n\r\nHowever, the situation becomes murkier with data types. For some reason, GHC //rejects// this definition:\r\n\r\n{{{#!hs\r\ndata T :: Const Type a where\r\n MkT :: T\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\n\r\nBug.hs:14:3: error:\r\n • Quantified type's kind mentions quantified type variable\r\n (skolem escape)\r\n type: forall a1. T\r\n of kind: Const * a\r\n • In the definition of data constructor ‘MkT’\r\n In the data type declaration for ‘T’\r\n \r\n14  MkT :: T\r\n  ^^^^^^^^\r\n}}}\r\n\r\nI'm not quite sure how to interpret that error message, but it seems fishy to me. Even fishier is the fact that GHC //accepts// this slight modification of `T`:\r\n\r\n{{{#!hs\r\ndata T2 :: Const Type a > Type where\r\n MkT2 :: T2 b\r\n}}}\r\n\r\nQuite mysterious.\r\n\r\n\r\n\r\nI briefly looked into where this error message is being thrown from. It turns out if you make this oneline change to GHC:\r\n\r\n{{{#!diff\r\ndiff git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs\r\nindex 218f539c68..c7925767f9 100644\r\n a/compiler/typecheck/TcValidity.hs\r\n+++ b/compiler/typecheck/TcValidity.hs\r\n@@ 635,7 +635,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt\r\n ; check_type (ve{ve_tidy_env = env'}) tau\r\n  Allow foralls to right of arrow\r\n\r\n ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))\r\n+ ; checkTcM (not (any (`elemVarSet` exactTyCoVarsOfType phi_kind) tvs))\r\n (forAllEscapeErr env' ty tau_kind)\r\n }\r\n where\r\n}}}\r\n\r\nThen GHC will accept `T`. Whether this change is the right choice to make, I don't think I'm qualified to say.","type_of_failure":"OtherFailure","blocking":[]} >8.10.1