GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200626T16:28:20Zhttps://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/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/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/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/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/16245GHC panic (No skolem info) with RankNTypes and strange scoping20200811T15:22:16ZRyan ScottGHC panic (No skolem info) with RankNTypes and strange scopingThe following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<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":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >The following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<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":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15942Associated type family can't be used at the kind level within other parts of ...20200110T19:59:15ZIcelandjackAssociated type family can't be used at the kind level within other parts of parent classI want to run the following past you (using [Visible Kind Applications](https://phabricator.haskell.org/D5229) but may be unrelated). The following compiles
```hs
{# Language DataKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = Bool > Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun (Not bool)
```
but quantifying `Bool` invisibly all of a sudden I can't use `Not`
```hs
{# Language DataKinds #}
{# Language RankNTypes #}
{# Language TypeApplications #}
{# Language PolyKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = forall (b :: Bool). Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun @(Not bool)
```
```
$ ghcstage2 interactive ignoredotghci 739_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 739_bug.hs, interpreted )
739_bug.hs:17:16: error:
• Type constructor ‘Not’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘Fun’, namely ‘(Not bool)’
In the type signature: foo :: Fun @(Not bool)
In the class declaration for ‘F’

17  foo :: Fun @(Not bool)
 ^^^
Failed, no modules loaded.
```
Is this restriction warrantedI want to run the following past you (using [Visible Kind Applications](https://phabricator.haskell.org/D5229) but may be unrelated). The following compiles
```hs
{# Language DataKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = Bool > Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun (Not bool)
```
but quantifying `Bool` invisibly all of a sudden I can't use `Not`
```hs
{# Language DataKinds #}
{# Language RankNTypes #}
{# Language TypeApplications #}
{# Language PolyKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = forall (b :: Bool). Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun @(Not bool)
```
```
$ ghcstage2 interactive ignoredotghci 739_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 739_bug.hs, interpreted )
739_bug.hs:17:16: error:
• Type constructor ‘Not’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘Fun’, namely ‘(Not bool)’
In the type signature: foo :: Fun @(Not bool)
In the class declaration for ‘F’

17  foo :: Fun @(Not bool)
 ^^^
Failed, no modules loaded.
```
Is this restriction warranted8.6.3https://gitlab.haskell.org/ghc/ghc//issues/15710Should GHC accept a type signature that needs coercion quantification?20200415T15:28:19ZSimon Peyton JonesShould GHC accept a type signature that needs coercion quantification?Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 > *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being
```
f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1>*)). (f > co) x
```
But there is a problem: the user wrote `k ~ (k1 > *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see [ticket:15710\#comment:161240](https://gitlab.haskell.org//ghc/ghc/issues/15710#note_161240) in #15497Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 > *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being
```
f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1>*)). (f > co) x
```
But there is a problem: the user wrote `k ~ (k1 > *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see [ticket:15710\#comment:161240](https://gitlab.haskell.org//ghc/ghc/issues/15710#note_161240) in #15497https://gitlab.haskell.org/ghc/ghc//issues/15589Always promoting metavariables during type inference may be wrong20190707T18:04:00ZRichard Eisenbergrae@richarde.devAlways promoting metavariables during type inference may be wrongCurrently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
 We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
 In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
 If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
 Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
 Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs)  section 6.5 to be specific.)
<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":"Always promoting metavariables during type inference may be wrong","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":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis]  section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} >Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
 We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
 In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
 If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
 Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
 Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs)  section 6.5 to be specific.)
<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":"Always promoting metavariables during type inference may be wrong","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":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis]  section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15588Panic when abusing kind inference20190707T18:04:01ZRichard Eisenbergrae@richarde.devPanic when abusing kind inferenceWhen I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64appledarwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64appledarwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} >When I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64appledarwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64appledarwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15561TypeInType: Type error conditioned on ordering of GADT and type family defini...20190707T18:04:07ZBj0rnTypeInType: Type error conditioned on ordering of GADT and type family definitionsConsider this code which successfully compiles:
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs #}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a > IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’

17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<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":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs #}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a > IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n \r\n17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} >Consider this code which successfully compiles:
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs #}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a > IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’

17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<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":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs #}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a > IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n \r\n17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15474Error message mentions Any20200123T19:16:21ZKrzysztof GogolewskiError message mentions AnyI'm not sure if this is a bug. File:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f2 :: Forall
f2 = f1
```
gives an error message mentioning Any:
```
• Couldn't match type ‘GHC.Types.Any’ with ‘*’
Expected type: Proxy t
Actual type: Proxy t0
```
The appearance of Any is suspicious to me  I thought it's an implementation detail?I'm not sure if this is a bug. File:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f2 :: Forall
f2 = f1
```
gives an error message mentioning Any:
```
• Couldn't match type ‘GHC.Types.Any’ with ‘*’
Expected type: Proxy t
Actual type: Proxy t0
```
The appearance of Any is suspicious to me  I thought it's an implementation detail?9.0.1https://gitlab.haskell.org/ghc/ghc//issues/14873The wellkinded type invariant (in TcType)20200124T11:45:58ZRyan ScottThe wellkinded type invariant (in TcType)(Originally noticed [here](https://travisci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a > a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type > Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type > Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x > Sing y > Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64unknownlinux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] > <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travisci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a > a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type > Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type > Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x > Sing y > Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180201 for x86_64unknownlinux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] > <*>_N)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >(Originally noticed [here](https://travisci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a > a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type > Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type > Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x > Sing y > Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64unknownlinux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] > <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travisci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a > a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type > Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type > Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x > Sing y > Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180201 for x86_64unknownlinux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] > <*>_N)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14668Ordering of declarations can cause typechecking to fail20190707T18:16:05ZheptahedronOrdering of declarations can cause typechecking to failThe following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
 data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’

23  type F' CInst (b :: F CInst) = G b

```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n \r\n23  type F' CInst (b :: F CInst) = G b\r\n  \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} >The following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
 data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’

23  type F' CInst (b :: F CInst) = G b

```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n \r\n23  type F' CInst (b :: F CInst) = G b\r\n  \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14645Allow type family in data family return kind20190707T18:16:10ZRichard Eisenbergrae@richarde.devAllow type family in data family return kindGHC currently allows
```hs
data family DF1 :: k1 > k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)
However, it rejects
```hs
type family TF (x :: Type) :: Type
data family DF2 :: x > TF x
```
when that's clearly just as sensible as the first definition.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 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 type family in data family return kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC currently allows\r\n\r\n{{{#!hs\r\ndata family DF1 :: k1 > k2\r\n}}}\r\n\r\nwhere it's expected (and checked) that all data ''instances'' have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)\r\n\r\nHowever, it rejects\r\n\r\n{{{#!hs\r\ntype family TF (x :: Type) :: Type\r\ndata family DF2 :: x > TF x\r\n}}}\r\n\r\nwhen that's clearly just as sensible as the first definition.","type_of_failure":"OtherFailure","blocking":[]} >GHC currently allows
```hs
data family DF1 :: k1 > k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)
However, it rejects
```hs
type family TF (x :: Type) :: Type
data family DF2 :: x > TF x
```
when that's clearly just as sensible as the first definition.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 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 type family in data family return kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC currently allows\r\n\r\n{{{#!hs\r\ndata family DF1 :: k1 > k2\r\n}}}\r\n\r\nwhere it's expected (and checked) that all data ''instances'' have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)\r\n\r\nHowever, it rejects\r\n\r\n{{{#!hs\r\ntype family TF (x :: Type) :: Type\r\ndata family DF2 :: x > TF x\r\n}}}\r\n\r\nwhen that's clearly just as sensible as the first definition.","type_of_failure":"OtherFailure","blocking":[]} >