GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-10-22T17:00:34Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/20356Constraint-vs-Type causes a panic2021-10-22T17:00:34ZRichard Eisenbergrae@richarde.devConstraint-vs-Type causes a panic@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type inst...@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type instance Id f = f
type T :: Constraint -> Constraint
type T = Id Eq
data Proxy p = MkProxy
id' :: f a -> f a
id' x = x
z = id' (MkProxy @T)
```
causes
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.3.20210824:
ASSERT failed!
Ill-kinded update to meta tyvar
a_aIJ[tau:1] :: Constraint -> Constraint
Constraint -> Constraint := Eq :: * -> Constraint
Call stack:
CallStack (from HasCallStack):
massertPpr, called at compiler/GHC/Tc/Utils/TcMType.hs:1009:10 in ghc:GHC.Tc.Utils.TcMType
```
when assertions are enabled (e.g. a `DEBUG` compiler).
Constraint-vs-Type is a difficult problem (see #11715), but I think we can pull this off and fix it. I imagine we just need to change an `eqType` to `tcEqType` somewhere.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/20312Deprecate -XTypeInType2022-06-06T16:13:20ZKrzysztof GogolewskiDeprecate -XTypeInTypeAccording to the accepted proposal [Embrace (Type :: Type)](https://github.com/ghc-proposals/ghc-proposals/pull/83)
> Two releases after this proposal is implemented, deprecate -XTypeInType.
The proposal has been implemented in GHC 8.6...According to the accepted proposal [Embrace (Type :: Type)](https://github.com/ghc-proposals/ghc-proposals/pull/83)
> Two releases after this proposal is implemented, deprecate -XTypeInType.
The proposal has been implemented in GHC 8.6. We can now deprecate `-XTypeInType`. The deprecation message should mention that it is replaced by `DataKinds` + `PolyKinds`.Rinat Striungislazybonesxp@gmail.comRinat Striungislazybonesxp@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/19677GHC does not rewrite in FunTy2022-02-21T17:09:27ZRichard Eisenbergrae@richarde.devGHC does not rewrite in FunTyConsider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
...Consider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
Lifty Int = LiftedRep
data G a where
MkG :: G Int
foo :: forall i (a :: TYPE (Lifty i)) (b :: TYPE (Lifty i)). G i -> (a -> b) -> ()
foo MkG = meth
```
GHC rejects, saying it cannot find an instance for `C (a -> b)`. But it should accept.
The problem is that the kinds of `a` and `b` are `TYPE (Lifty i)`. Even if we know `i ~ Int`, and therefore that `Lifty i ~ LiftedRep`, GHC does not rewrite these kinds internally, allowing instance matching to succeed.
!2477, when complete, should address this.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19196TypeInType prevents Typeable from being resolved from a given2021-01-11T03:19:52ZSerge KosyrevTypeInType prevents Typeable from being resolved from a givenThe following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}...The following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t -> LTag (Live t)
reconstruct :: Dynamic -> LTag l -> ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) ->
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
```
It is, however, rejected with `TypeInType`, as follows:
```haskell
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:19-25
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:10-17
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:16-56
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))
|
26 | (fromDynamic dyn :: Maybe (IOA (Live t)))
| ^^^^^^^^^^^^^^^
```
Potentially related to #16627https://gitlab.haskell.org/ghc/ghc/-/issues/18891Kind inference for newtypes in GADT syntax is deeply broken2020-12-08T21:03:16ZRichard Eisenbergrae@richarde.devKind inference for newtypes in GADT syntax is deeply brokenHere are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In th...Here are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
------------------------
```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N -> N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
type N :: forall k -> TYPE k
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18753Tighten up the treatment of loose types in the solver2020-09-30T16:21:20ZRichard 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...`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 kind-check.
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 inert-set 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 well-typed `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 double-check before I commit a fix.https://gitlab.haskell.org/ghc/ghc/-/issues/18714GHC panic (tcInvisibleTyBinder) when using constraint in a kind2020-09-21T21: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...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#L473-480):
```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#L496-507), 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 kind-level 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/ghc-stage2 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/17675eqType fails on comparing FunTys2022-02-21T17:09:27ZRichard 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 ...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 [Non-trivial 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/17567Never `Any`-ify during kind inference2021-01-11T13:09:30ZRichard 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
...#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, top-level 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 add-on to any of the above plans. Because `Type` is not always well-kinded, 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 top-level 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 context-building 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 constraint2021-01-11T13:07:45ZRichard 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
...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 super-classes 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 families2019-12-12T16: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,
D...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/17131Kind inference bug in type family declaration2021-09-15T13:05:09ZSimon 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 '[] = '[]
TypeR...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/16902Compile-time stack overflow exception in GHC HEAD only2019-07-05T07:29:45ZRyan ScottCompile-time 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 ::...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/ghc-stage2 --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 broken2023-06-15T22:08:29ZVladislav 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 unfo...# 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/ghc-kinds/kind-inference/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/16600Higher-rank kinds lead to substitution assertion failure2019-06-08T12:32:36ZRichard Eisenbergrae@richarde.devHigher-rank 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 ...# 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 higher-rank argument.
# Environment
* GHC version used: HEADhttps://gitlab.haskell.org/ghc/ghc/-/issues/16391"Quantified type's kind mentions quantified type variable" error with fancy-k...2020-07-27T08:24:27ZRyan Scott"Quantified type's kind mentions quantified type variable" error with fancy-kinded 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:
...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 one-line 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 fancy-kinded 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 one-line 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.1https://gitlab.haskell.org/ghc/ghc/-/issues/16347GHC HEAD regression: piResultTys12019-07-07T18:00:25ZRyan ScottGHC HEAD regression: piResultTys1The following program typechecks on GHC 8.0.2 through 8.6.3, but panics on HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data T f :: f Type -> Type where
MkT :: T f a
```
```
...The following program typechecks on GHC 8.0.2 through 8.6.3, but panics on HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data T f :: f Type -> Type where
MkT :: T f a
```
```
$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20190219 for x86_64-unknown-linux):
piResultTys1
k_a10k[tau:1]
[*]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1063:5 in ghc:Type
```8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/16310Program fails with "Impossible case alternative" when optimized2019-07-07T18:00:35ZRyan ScottProgram fails with "Impossible case alternative" when optimizedHere's an (unfortunately rather large) program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
...Here's an (unfortunately rather large) program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main (main) where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import Unsafe.Coerce (unsafeCoerce)
main :: IO ()
main = print $ traversableComposition @(M1 U1) @() @() @() @U1 @U1
sPureFun sPureFun (SM1 SU1)
-----
sPureFun :: forall f a. SApplicative f => Sing (PureSym0 :: a ~> f a)
sPureFun = singFun1 @PureSym0 sPure
data family Sing (a :: k)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data (.@#@$$$) :: forall a b c. (b ~> c) -> (a ~> b) -> a ~> c
type instance Apply (f .@#@$$$ g) x = Apply f (Apply g x)
newtype instance Sing (f :: k1 ~> k2) =
SLambda (forall t. Sing t -> Sing (Apply f t))
type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))
-----
data U1 p = U1
data instance Sing (z :: U1 p) where
SU1 :: Sing 'U1
newtype M1 f p = M1 (f p)
data instance Sing (z :: M1 f p) where
SM1 :: Sing x -> Sing ('M1 x)
data M1Sym0 :: forall k (f :: k -> Type) (p :: k). f p ~> M1 f p
type instance Apply M1Sym0 x = 'M1 x
newtype Compose f g x = Compose (f (g x))
data ComposeSym0 :: forall k1 k2 (f :: k2 -> Type) (g :: k1 -> k2) (x :: k1).
f (g x) ~> Compose f g x
type instance Apply ComposeSym0 x = 'Compose x
data instance Sing (z :: Compose f g a) where
SCompose :: Sing x -> Sing ('Compose x)
instance (PFunctor f, PFunctor g) => PFunctor (Compose f g) where
type Fmap h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x)
instance (SFunctor f, SFunctor g) => SFunctor (Compose f g) where
sFmap :: forall a b (h :: a ~> b) (x :: Compose f g a).
Sing h -> Sing x -> Sing (Fmap h x)
sFmap sh (SCompose sx) = SCompose (sFmap (singFun1 @(FmapSym1 h) (sFmap sh)) sx)
instance (PApplicative f, PApplicative g) => PApplicative (Compose f g) where
type Pure x = 'Compose (Pure (Pure x))
type 'Compose h <*> 'Compose x = 'Compose (Fmap (<*>@#@$) h <*> x)
instance (SApplicative f, SApplicative g) => SApplicative (Compose f g) where
sPure sx = SCompose (sPure (sPure sx))
SCompose sh %<*> SCompose sx = SCompose (sFmap (singFun2 @(<*>@#@$) (%<*>)) sh %<*> sx)
instance PFunctor U1 where
type Fmap _ _ = 'U1
instance SFunctor U1 where
sFmap _ _ = SU1
instance VFunctor U1 where
fmapCompose _ _ SU1 = Refl
instance PFunctor f => PFunctor (M1 f) where
type Fmap g ('M1 x) = 'M1 (Fmap g x)
instance SFunctor f => SFunctor (M1 f) where
sFmap sg (SM1 sx) = SM1 (sFmap sg sx)
instance VFunctor f => VFunctor (M1 f) where
fmapCompose sg sh (SM1 x) | Refl <- fmapCompose sg sh x = Refl
instance PApplicative U1 where
type Pure _ = 'U1
type _ <*> _ = 'U1
instance SApplicative U1 where
sPure _ = SU1
_ %<*> _ = SU1
instance VApplicative U1 where
applicativeHomomorphism _ _ = Refl
applicativeFmap _ _ = Refl
instance PTraversable U1 where
type Traverse _ _ = Pure 'U1
instance STraversable U1 where
sTraverse _ _ = sPure SU1
instance VTraversable U1 where
traversableComposition :: forall p q r (f :: Type -> Type) (g :: Type -> Type)
(h :: p ~> f q) (i :: q ~> g r) (x :: U1 p).
(VApplicative f, VApplicative g)
=> Sing h -> Sing i -> Sing x
-> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
:~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))
traversableComposition _ si _
| Refl <- applicativeHomomorphism @f sTraverseI sU1q
, Refl <- applicativeFmap @f sTraverseI (sPure sU1q)
= Refl
where
sTraverseI :: Sing (TraverseSym1 i :: U1 q ~> g (U1 r))
sTraverseI = singFun1 (sTraverse si)
sU1q :: Sing ('U1 :: U1 q)
sU1q = SU1
instance PTraversable f => PTraversable (M1 f) where
type Traverse g ('M1 x) = Fmap M1Sym0 (Traverse g x)
instance STraversable f => STraversable (M1 f) where
sTraverse sg (SM1 sx) = sFmap (singFun1 @M1Sym0 SM1) (sTraverse sg sx)
instance VTraversable f => VTraversable (M1 f) where
traversableComposition :: forall p q r (cf :: Type -> Type) (cg :: Type -> Type)
(h :: p ~> cf q) (i :: q ~> cg r) (x :: M1 f p).
(VApplicative cf, VApplicative cg)
=> Sing h -> Sing i -> Sing x
-> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
:~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))
traversableComposition sh si (SM1 (sfp :: Sing fp))
| Refl <- traversableComposition sh si sfp
, Refl <- fmapCompose @cf (singFun1 @(FmapSym1 M1Sym0) (sFmap sM1Fun))
sTraverseIFun sTraverseHIp
, Refl <- -- Fmap (FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i) (Traverse h fp)
-- :~: Fmap (TraverseSym1 i .@#@$$$ M1Sym0) (Traverse h fp)
Refl @FmapSym0
`apply` funExt @(f q) @(cg (M1 f r))
@(FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i)
@(TraverseSym1 i .@#@$$$ M1Sym0)
lemma
`apply` Refl @(Traverse h fp)
, Refl <- fmapCompose @cf sTraverseIFun sM1Fun sTraverseHIp
= Refl
where
lemma :: forall (z :: f q). Sing z
-> Fmap M1Sym0 (Traverse i z) :~: Traverse i (Apply M1Sym0 z)
lemma _ = Refl
sM1Fun :: forall z. Sing (M1Sym0 :: f z ~> M1 f z)
sM1Fun = singFun1 SM1
sTraverseHIp :: Sing (Traverse h fp)
sTraverseHIp = sTraverse sh sfp
sTraverseIFun :: forall hk. STraversable hk
=> Sing (TraverseSym1 i :: hk q ~> cg (hk r))
sTraverseIFun = singFun1 (sTraverse si)
-----
class PFunctor (f :: Type -> Type) where
type Fmap (g :: a ~> b) (x :: f a) :: f b
data FmapSym0 :: forall f a b. (a ~> b) ~> f a ~> f b
data FmapSym1 :: forall f a b. (a ~> b) -> f a ~> f b
type instance Apply FmapSym0 f = FmapSym1 f
type instance Apply (FmapSym1 f) x = Fmap f x
class SFunctor (f :: Type -> Type) where
sFmap :: forall a b (g :: a ~> b) (x :: f a).
Sing g -> Sing x -> Sing (Fmap g x)
class (PFunctor f, SFunctor f) => VFunctor f where
fmapCompose :: forall a b c (g :: b ~> c) (h :: a ~> b) (x :: f a).
Sing g -> Sing h -> Sing x
-> Fmap g (Fmap h x) :~: Fmap (g .@#@$$$ h) x
class PFunctor f => PApplicative f where
type Pure (x :: a) :: f a
type (g :: f (a ~> b)) <*> (x :: f a) :: f b
infixl 4 <*>
data PureSym0 :: forall (f :: Type -> Type) a. a ~> f a
type instance Apply PureSym0 x = Pure x
data (<*>@#@$) :: forall (f :: Type -> Type) a b. f (a ~> b) ~> f a ~> f b
data (<*>@#@$$) :: forall (f :: Type -> Type) a b. f (a ~> b) -> f a ~> f b
type instance Apply (<*>@#@$) f = (<*>@#@$$) f
type instance Apply ((<*>@#@$$) f) x = f <*> x
class SFunctor f => SApplicative f where
sPure :: forall a (x :: a).
Sing x -> Sing (Pure x :: f a)
(%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).
Sing g -> Sing x -> Sing (g <*> x)
class (PApplicative f, SApplicative f, VFunctor f) => VApplicative f where
applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).
Sing g -> Sing x
-> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
applicativeFmap :: forall a b (g :: a ~> b) (x :: f a).
Sing g -> Sing x
-> Fmap g x :~: (Pure g <*> x)
class PFunctor t => PTraversable t where
type Traverse (g :: a ~> f b) (x :: t a) :: f (t b)
data TraverseSym1 :: forall t f a b. (a ~> f b) -> t a ~> f (t b)
type instance Apply (TraverseSym1 f) x = Traverse f x
class SFunctor t => STraversable t where
sTraverse :: forall f a b (g :: a ~> f b) (x :: t a).
SApplicative f
=> Sing g -> Sing x -> Sing (Traverse g x)
class (PTraversable t, STraversable t, VFunctor t) => VTraversable t where
traversableComposition :: forall a b c (f :: Type -> Type) (g :: Type -> Type)
(h :: a ~> f b) (i :: b ~> g c) (x :: t a).
(VApplicative f, VApplicative g)
=> Sing h -> Sing i -> Sing x
-> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
:~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))
-----
funExt :: forall a b (f :: a ~> b) (g :: a ~> b).
(forall (x :: a). Sing x
-> Apply f x :~: Apply g x)
-> f :~: g
funExt _ = axiom
apply :: f :~: g -> a :~: b -> Apply f a :~: Apply g b
apply Refl Refl = Refl
axiom :: a :~: b
axiom = unsafeCoerce Refl
```
When compiled without optimization, this program prints "`Refl`", as you would expect:
```
$ /opt/ghc/8.6.3/bin/ghc -O0 Bug.hs -fforce-recomp
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking Bug ...
$ ./Bug
Refl
```
However, when compiled with optimizations, it starts failing at runtime!
```
$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking Bug ...
$ ./Bug
Bug: Impossible case alternative
```
This behavior can be observed on all versions of GHC from 8.2.2 to HEAD.
Interestingly, this program passes `-dcore-lint` on GHC 8.4.4 through HEAD, but on GHC 8.2.2, it fails `-dcore-lint`:
```
$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking Bug ...
$ /opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In a case alternative: (Refl cobox_a1UV :: (FmapSym0 :: (TyFun
(f1_X2dk b_a2aC
~> g_a2aF (M1 f1_X2dk c_a2aD))
(f_a2aE (f1_X2dk b_a2aC)
~> f_a2aE (g_a2aF (M1
f1_X2dk
c_a2aD)))
-> *))
~#
(FmapSym0 :: (TyFun
(f1_X2dk b_a2aC
~> g_a2aF (M1 f1_X2dk c_a2aD))
(f_a2aE (f1_X2dk b_a2aC)
~> f_a2aE (g_a2aF (M1
f1_X2dk
c_a2aD)))
-> *)))
No alternatives for a case scrutinee in head-normal form: ($WRefl
@ Any @ Any)
`cast` (((:~:)
(UnsafeCo nominal Any (f b
~> g (M1
f
c)))
(UnsafeCo nominal Any (FmapSym1
M1Sym0
.@#@$$$ TraverseSym1
i))
(UnsafeCo nominal Any (TraverseSym1
i
.@#@$$$ M1Sym0)))_R
:: ((Any :~: Any) :: *)
~R#
(((FmapSym1 M1Sym0
.@#@$$$ TraverseSym1
i_a2aH)
:~: (TraverseSym1 i_a2aH
.@#@$$$ M1Sym0)) :: *))
```
(The full Core Lint error is absolutely enormous, so I'll post it as a separate attachment.)
The one thing about this program that might be considered strange is the use of `axiom = unsafeCoerce Refl`. I believe this should be a perfectly safe use of `unsafeCoerce`, but nevertheless, there is always the possibility that GHC is doing something unsightly when optimizing it. As one curiosity, if you mark `axiom` as `NOINLINE`, then the program produces a different result:
```
$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking Bug ...
$ ./Bug
```
The program simply prints a newline, for some odd reason. (It doesn't appear to throw an exception either, since `echo $?` yields `0`.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Program fails with \"Impossible case alternative\" when optimized","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's an (unfortunately rather large) program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE InstanceSigs #-}\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\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Main (main) where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Type.Equality ((:~:)(..))\r\nimport Unsafe.Coerce (unsafeCoerce)\r\n\r\nmain :: IO ()\r\nmain = print $ traversableComposition @(M1 U1) @() @() @() @U1 @U1\r\n sPureFun sPureFun (SM1 SU1)\r\n\r\n-----\r\n\r\nsPureFun :: forall f a. SApplicative f => Sing (PureSym0 :: a ~> f a)\r\nsPureFun = singFun1 @PureSym0 sPure\r\n\r\ndata family Sing (a :: k)\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: a ~> b) (x :: a) :: b\r\n\r\ndata (.@#@$$$) :: forall a b c. (b ~> c) -> (a ~> b) -> a ~> c\r\ntype instance Apply (f .@#@$$$ g) x = Apply f (Apply g x)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda (forall t. Sing t -> Sing (Apply f t))\r\n\r\ntype SingFunction1 f = forall t. Sing t -> Sing (Apply f t)\r\nsingFun1 :: forall f. SingFunction1 f -> Sing f\r\nsingFun1 f = SLambda f\r\n\r\ntype SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)\r\nsingFun2 :: forall f. SingFunction2 f -> Sing f\r\nsingFun2 f = SLambda (\\x -> singFun1 (f x))\r\n\r\n-----\r\n\r\ndata U1 p = U1\r\ndata instance Sing (z :: U1 p) where\r\n SU1 :: Sing 'U1\r\n\r\nnewtype M1 f p = M1 (f p)\r\ndata instance Sing (z :: M1 f p) where\r\n SM1 :: Sing x -> Sing ('M1 x)\r\ndata M1Sym0 :: forall k (f :: k -> Type) (p :: k). f p ~> M1 f p\r\ntype instance Apply M1Sym0 x = 'M1 x\r\n\r\nnewtype Compose f g x = Compose (f (g x))\r\ndata ComposeSym0 :: forall k1 k2 (f :: k2 -> Type) (g :: k1 -> k2) (x :: k1).\r\n f (g x) ~> Compose f g x\r\ntype instance Apply ComposeSym0 x = 'Compose x\r\ndata instance Sing (z :: Compose f g a) where\r\n SCompose :: Sing x -> Sing ('Compose x)\r\n\r\ninstance (PFunctor f, PFunctor g) => PFunctor (Compose f g) where\r\n type Fmap h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x)\r\ninstance (SFunctor f, SFunctor g) => SFunctor (Compose f g) where\r\n sFmap :: forall a b (h :: a ~> b) (x :: Compose f g a).\r\n Sing h -> Sing x -> Sing (Fmap h x)\r\n sFmap sh (SCompose sx) = SCompose (sFmap (singFun1 @(FmapSym1 h) (sFmap sh)) sx)\r\n\r\ninstance (PApplicative f, PApplicative g) => PApplicative (Compose f g) where\r\n type Pure x = 'Compose (Pure (Pure x))\r\n type 'Compose h <*> 'Compose x = 'Compose (Fmap (<*>@#@$) h <*> x)\r\ninstance (SApplicative f, SApplicative g) => SApplicative (Compose f g) where\r\n sPure sx = SCompose (sPure (sPure sx))\r\n SCompose sh %<*> SCompose sx = SCompose (sFmap (singFun2 @(<*>@#@$) (%<*>)) sh %<*> sx)\r\n\r\ninstance PFunctor U1 where\r\n type Fmap _ _ = 'U1\r\ninstance SFunctor U1 where\r\n sFmap _ _ = SU1\r\ninstance VFunctor U1 where\r\n fmapCompose _ _ SU1 = Refl\r\n\r\ninstance PFunctor f => PFunctor (M1 f) where\r\n type Fmap g ('M1 x) = 'M1 (Fmap g x)\r\ninstance SFunctor f => SFunctor (M1 f) where\r\n sFmap sg (SM1 sx) = SM1 (sFmap sg sx)\r\ninstance VFunctor f => VFunctor (M1 f) where\r\n fmapCompose sg sh (SM1 x) | Refl <- fmapCompose sg sh x = Refl\r\n\r\ninstance PApplicative U1 where\r\n type Pure _ = 'U1\r\n type _ <*> _ = 'U1\r\ninstance SApplicative U1 where\r\n sPure _ = SU1\r\n _ %<*> _ = SU1\r\ninstance VApplicative U1 where\r\n applicativeHomomorphism _ _ = Refl\r\n applicativeFmap _ _ = Refl\r\n\r\ninstance PTraversable U1 where\r\n type Traverse _ _ = Pure 'U1\r\ninstance STraversable U1 where\r\n sTraverse _ _ = sPure SU1\r\ninstance VTraversable U1 where\r\n traversableComposition :: forall p q r (f :: Type -> Type) (g :: Type -> Type)\r\n (h :: p ~> f q) (i :: q ~> g r) (x :: U1 p).\r\n (VApplicative f, VApplicative g)\r\n => Sing h -> Sing i -> Sing x\r\n -> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x\r\n :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))\r\n traversableComposition _ si _\r\n | Refl <- applicativeHomomorphism @f sTraverseI sU1q\r\n , Refl <- applicativeFmap @f sTraverseI (sPure sU1q)\r\n = Refl\r\n where\r\n sTraverseI :: Sing (TraverseSym1 i :: U1 q ~> g (U1 r))\r\n sTraverseI = singFun1 (sTraverse si)\r\n\r\n sU1q :: Sing ('U1 :: U1 q)\r\n sU1q = SU1\r\n\r\ninstance PTraversable f => PTraversable (M1 f) where\r\n type Traverse g ('M1 x) = Fmap M1Sym0 (Traverse g x)\r\ninstance STraversable f => STraversable (M1 f) where\r\n sTraverse sg (SM1 sx) = sFmap (singFun1 @M1Sym0 SM1) (sTraverse sg sx)\r\ninstance VTraversable f => VTraversable (M1 f) where\r\n traversableComposition :: forall p q r (cf :: Type -> Type) (cg :: Type -> Type)\r\n (h :: p ~> cf q) (i :: q ~> cg r) (x :: M1 f p).\r\n (VApplicative cf, VApplicative cg)\r\n => Sing h -> Sing i -> Sing x\r\n -> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x\r\n :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))\r\n traversableComposition sh si (SM1 (sfp :: Sing fp))\r\n | Refl <- traversableComposition sh si sfp\r\n , Refl <- fmapCompose @cf (singFun1 @(FmapSym1 M1Sym0) (sFmap sM1Fun))\r\n sTraverseIFun sTraverseHIp\r\n , Refl <- -- Fmap (FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i) (Traverse h fp)\r\n -- :~: Fmap (TraverseSym1 i .@#@$$$ M1Sym0) (Traverse h fp)\r\n Refl @FmapSym0\r\n `apply` funExt @(f q) @(cg (M1 f r))\r\n @(FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i)\r\n @(TraverseSym1 i .@#@$$$ M1Sym0)\r\n lemma\r\n `apply` Refl @(Traverse h fp)\r\n , Refl <- fmapCompose @cf sTraverseIFun sM1Fun sTraverseHIp\r\n = Refl\r\n where\r\n lemma :: forall (z :: f q). Sing z\r\n -> Fmap M1Sym0 (Traverse i z) :~: Traverse i (Apply M1Sym0 z)\r\n lemma _ = Refl\r\n\r\n sM1Fun :: forall z. Sing (M1Sym0 :: f z ~> M1 f z)\r\n sM1Fun = singFun1 SM1\r\n\r\n sTraverseHIp :: Sing (Traverse h fp)\r\n sTraverseHIp = sTraverse sh sfp\r\n\r\n sTraverseIFun :: forall hk. STraversable hk\r\n => Sing (TraverseSym1 i :: hk q ~> cg (hk r))\r\n sTraverseIFun = singFun1 (sTraverse si)\r\n\r\n-----\r\n\r\nclass PFunctor (f :: Type -> Type) where\r\n type Fmap (g :: a ~> b) (x :: f a) :: f b\r\ndata FmapSym0 :: forall f a b. (a ~> b) ~> f a ~> f b\r\ndata FmapSym1 :: forall f a b. (a ~> b) -> f a ~> f b\r\ntype instance Apply FmapSym0 f = FmapSym1 f\r\ntype instance Apply (FmapSym1 f) x = Fmap f x\r\nclass SFunctor (f :: Type -> Type) where\r\n sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n Sing g -> Sing x -> Sing (Fmap g x)\r\nclass (PFunctor f, SFunctor f) => VFunctor f where\r\n fmapCompose :: forall a b c (g :: b ~> c) (h :: a ~> b) (x :: f a).\r\n Sing g -> Sing h -> Sing x\r\n -> Fmap g (Fmap h x) :~: Fmap (g .@#@$$$ h) x\r\n\r\nclass PFunctor f => PApplicative f where\r\n type Pure (x :: a) :: f a\r\n type (g :: f (a ~> b)) <*> (x :: f a) :: f b\r\ninfixl 4 <*>\r\ndata PureSym0 :: forall (f :: Type -> Type) a. a ~> f a\r\ntype instance Apply PureSym0 x = Pure x\r\ndata (<*>@#@$) :: forall (f :: Type -> Type) a b. f (a ~> b) ~> f a ~> f b\r\ndata (<*>@#@$$) :: forall (f :: Type -> Type) a b. f (a ~> b) -> f a ~> f b\r\ntype instance Apply (<*>@#@$) f = (<*>@#@$$) f\r\ntype instance Apply ((<*>@#@$$) f) x = f <*> x\r\nclass SFunctor f => SApplicative f where\r\n sPure :: forall a (x :: a).\r\n Sing x -> Sing (Pure x :: f a)\r\n\r\n (%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).\r\n Sing g -> Sing x -> Sing (g <*> x)\r\nclass (PApplicative f, SApplicative f, VFunctor f) => VApplicative f where\r\n applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).\r\n Sing g -> Sing x\r\n -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)\r\n applicativeFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n Sing g -> Sing x\r\n -> Fmap g x :~: (Pure g <*> x)\r\n\r\nclass PFunctor t => PTraversable t where\r\n type Traverse (g :: a ~> f b) (x :: t a) :: f (t b)\r\ndata TraverseSym1 :: forall t f a b. (a ~> f b) -> t a ~> f (t b)\r\ntype instance Apply (TraverseSym1 f) x = Traverse f x\r\nclass SFunctor t => STraversable t where\r\n sTraverse :: forall f a b (g :: a ~> f b) (x :: t a).\r\n SApplicative f\r\n => Sing g -> Sing x -> Sing (Traverse g x)\r\nclass (PTraversable t, STraversable t, VFunctor t) => VTraversable t where\r\n traversableComposition :: forall a b c (f :: Type -> Type) (g :: Type -> Type)\r\n (h :: a ~> f b) (i :: b ~> g c) (x :: t a).\r\n (VApplicative f, VApplicative g)\r\n => Sing h -> Sing i -> Sing x\r\n -> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x\r\n :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))\r\n\r\n-----\r\n\r\nfunExt :: forall a b (f :: a ~> b) (g :: a ~> b).\r\n (forall (x :: a). Sing x\r\n -> Apply f x :~: Apply g x)\r\n -> f :~: g\r\nfunExt _ = axiom\r\n\r\napply :: f :~: g -> a :~: b -> Apply f a :~: Apply g b\r\napply Refl Refl = Refl\r\n\r\naxiom :: a :~: b\r\naxiom = unsafeCoerce Refl\r\n}}}\r\n\r\nWhen compiled without optimization, this program prints \"`Refl`\", as you would expect:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc -O0 Bug.hs -fforce-recomp\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\nLinking Bug ...\r\n$ ./Bug \r\nRefl\r\n}}}\r\n\r\nHowever, when compiled with optimizations, it starts failing at runtime!\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\nLinking Bug ...\r\n\r\n$ ./Bug \r\nBug: Impossible case alternative\r\n}}}\r\n\r\nThis behavior can be observed on all versions of GHC from 8.2.2 to HEAD.\r\n\r\nInterestingly, this program passes `-dcore-lint` on GHC 8.4.4 through HEAD, but on GHC 8.2.2, it fails `-dcore-lint`:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\nLinking Bug ...\r\n\r\n$ /opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\n<no location info>: warning:\r\n In a case alternative: (Refl cobox_a1UV :: (FmapSym0 :: (TyFun\r\n (f1_X2dk b_a2aC\r\n ~> g_a2aF (M1 f1_X2dk c_a2aD))\r\n (f_a2aE (f1_X2dk b_a2aC)\r\n ~> f_a2aE (g_a2aF (M1\r\n f1_X2dk\r\n c_a2aD)))\r\n -> *))\r\n ~#\r\n (FmapSym0 :: (TyFun\r\n (f1_X2dk b_a2aC\r\n ~> g_a2aF (M1 f1_X2dk c_a2aD))\r\n (f_a2aE (f1_X2dk b_a2aC)\r\n ~> f_a2aE (g_a2aF (M1\r\n f1_X2dk\r\n c_a2aD)))\r\n -> *)))\r\n No alternatives for a case scrutinee in head-normal form: ($WRefl\r\n @ Any @ Any)\r\n `cast` (((:~:)\r\n (UnsafeCo nominal Any (f b\r\n ~> g (M1\r\n f\r\n c)))\r\n (UnsafeCo nominal Any (FmapSym1\r\n M1Sym0\r\n .@#@$$$ TraverseSym1\r\n i))\r\n (UnsafeCo nominal Any (TraverseSym1\r\n i\r\n .@#@$$$ M1Sym0)))_R\r\n :: ((Any :~: Any) :: *)\r\n ~R#\r\n (((FmapSym1 M1Sym0\r\n .@#@$$$ TraverseSym1\r\n i_a2aH)\r\n :~: (TraverseSym1 i_a2aH\r\n .@#@$$$ M1Sym0)) :: *))\r\n}}}\r\n\r\n(The full Core Lint error is absolutely enormous, so I'll post it as a separate attachment.)\r\n\r\nThe one thing about this program that might be considered strange is the use of `axiom = unsafeCoerce Refl`. I believe this should be a perfectly safe use of `unsafeCoerce`, but nevertheless, there is always the possibility that GHC is doing something unsightly when optimizing it. As one curiosity, if you mark `axiom` as `NOINLINE`, then the program produces a different result:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\nLinking Bug ...\r\n\r\n$ ./Bug \r\n\r\n}}}\r\n\r\nThe program simply prints a newline, for some odd reason. (It doesn't appear to throw an exception either, since `echo $?` yields `0`.)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16263Rework GHC's treatment of constraints in kinds2019-07-07T18:00:45ZRichard Eisenbergrae@richarde.devRework GHC's treatment of constraints in kindsGHC 8.6 accepts
```hs
data Q :: Eq a => Type
```
It shouldn't, as we can't have `Eq a` as a constraint in kinds. Note that writing a constructor for `Q` is rejected.
<details><summary>Trac metadata</summary>
| Trac field ...GHC 8.6 accepts
```hs
data Q :: Eq a => Type
```
It shouldn't, as we can't have `Eq a` as a constraint in kinds. Note that writing a constructor for `Q` is rejected.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC accepts illegal constraint in kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.6 accepts\r\n\r\n{{{#!hs\r\ndata Q :: Eq a => Type\r\n}}}\r\n\r\nIt shouldn't, as we can't have `Eq a` as a constraint in kinds. Note that writing a constructor for `Q` is rejected.","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/16247GHC 8.6 Core Lint regression (Kind application error)2019-07-07T18:00:49ZRyan ScottGHC 8.6 Core Lint regression (Kind application error)The following program produces a Core Lint error on GHC 8.6.3 and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data SameKind :: forall k. k -> k ...The following program produces a Core Lint error on GHC 8.6.3 and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data SameKind :: forall k. k -> k -> Type
data Foo :: forall a k (b :: k). SameKind a b -> Type where
MkFoo :: Foo sameKind
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of CorePrep ***
<no location info>: warning:
In the type ‘forall k (a :: k) k (b :: k) (sameKind :: SameKind
a b).
Foo sameKind’
Kind application error in type ‘SameKind a_aWE b_aWG’
Function kind = forall k. k -> k -> *
Arg kinds = [(k_aWF, *), (a_aWE, k_aWD), (b_aWG, k_aWF)]
Fun: k_aWF
(a_aWE, k_aWD)
*** Offending Program ***
<elided>
MkFoo
:: forall k (a :: k) k (b :: k) (sameKind :: SameKind a b).
Foo sameKind
```
(Confusingly, the type of `MkFoo` is rendered as `forall k (a :: k) k (b :: k) (sameKind :: SameKind a b). Foo sameKind` in that `-dcore-lint` error, but I think it really should be `forall k1 (a :: k1) k2 (b :: k2) (sameKind :: SameKind a b). Foo sameKind`.)
On GHC 8.4.4 and earlier, this simply produces an error message:
```
$ /opt/ghc/8.4.4/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:13: error:
• These kind and type variables: a k (b :: k)
are out of dependency order. Perhaps try this ordering:
k (a :: k) (b :: k)
• In the kind ‘forall a k (b :: k). SameKind a b -> Type’
|
9 | data Foo :: forall a k (b :: k). SameKind a b -> Type where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<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 8.6 Core Lint regression (Kind application error)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program produces a Core Lint error on GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k -> k -> Type\r\ndata Foo :: forall a k (b :: k). SameKind a b -> Type where\r\n MkFoo :: Foo sameKind\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of CorePrep ***\r\n<no location info>: warning:\r\n In the type ‘forall k (a :: k) k (b :: k) (sameKind :: SameKind\r\n a b).\r\n Foo sameKind’\r\n Kind application error in type ‘SameKind a_aWE b_aWG’\r\n Function kind = forall k. k -> k -> *\r\n Arg kinds = [(k_aWF, *), (a_aWE, k_aWD), (b_aWG, k_aWF)]\r\n Fun: k_aWF\r\n (a_aWE, k_aWD)\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\nMkFoo\r\n :: forall k (a :: k) k (b :: k) (sameKind :: SameKind a b).\r\n Foo sameKind\r\n}}}\r\n\r\n(Confusingly, the type of `MkFoo` is rendered as `forall k (a :: k) k (b :: k) (sameKind :: SameKind a b). Foo sameKind` in that `-dcore-lint` error, but I think it really should be `forall k1 (a :: k1) k2 (b :: k2) (sameKind :: SameKind a b). Foo sameKind`.)\r\n\r\nOn GHC 8.4.4 and earlier, this simply produces an error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.4/bin/ghc Bug.hs -dcore-lint\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:9:13: error:\r\n • These kind and type variables: a k (b :: k)\r\n are out of dependency order. Perhaps try this ordering:\r\n k (a :: k) (b :: k)\r\n • In the kind ‘forall a k (b :: k). SameKind a b -> Type’\r\n |\r\n9 | data Foo :: forall a k (b :: k). SameKind a b -> Type where\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1