GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-06-16T15:54:59Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/17368Implement homogeneous equality2021-06-16T15:54: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/dep-roles/dep-roles.pdf), the primitive equality type in GHC can be made homogeneous. T...As observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/dep-roles/dep-roles.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 type-checker 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/dependent-haskell/phase2, which has much discussion.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/17327Kind-checking associated types2020-02-18T16:17:45ZmniipKind-checking 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, TypeFamil...## 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 kind-check (it has better instance resolution properties than the first which is why we want it).
## Environment
Tested on GHC 8.6.5 and GHC HEADhttps://gitlab.haskell.org/ghc/ghc/-/issues/17131Kind inference bug in type family 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.1https://gitlab.haskell.org/ghc/ghc/-/issues/16245GHC panic (No skolem info) with RankNTypes and strange scoping2020-12-31T13:44:06ZRyan 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...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_64-unknown-linux):
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 ill-scoped.
<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_64-unknown-linux):\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 ill-scoped.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16244Couldn't match kind ‘k1’ with ‘k1’2020-05-05T09:44:28ZRyan ScottCouldn't match kind ‘k1’ with ‘k1’The following program gives a hopelessly confusing error message on GHC 8.6.3 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
module Bug where...The following program gives a hopelessly confusing error message on GHC 8.6.3 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class SameKind a b => C (k :: Const Type a) (b :: k)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:18: error:
• Couldn't match kind ‘k1’ with ‘k1’
• In the second argument of ‘SameKind’, namely ‘b’
In the class declaration for ‘C’
|
11 | class SameKind a b => C (k :: Const Type a) (b :: k)
| ^
```
I imagine that the real issue is that `SameKind a b` would force `a :: k`, which would be ill-scoped. But figuring that out from this strange error message requires a lot of thought.
<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":"Couldn't match kind ‘k1’ with ‘k1’","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 gives a hopelessly confusing error message on GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE PolyKinds #-}\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 SameKind a b => C (k :: Const Type a) (b :: k)\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:18: error:\r\n • Couldn't match kind ‘k1’ with ‘k1’\r\n • In the second argument of ‘SameKind’, namely ‘b’\r\n In the class declaration for ‘C’\r\n |\r\n11 | class SameKind a b => C (k :: Const Type a) (b :: k)\r\n | ^\r\n}}}\r\n\r\nI imagine that the real issue is that `SameKind a b` would force `a :: k`, which would be ill-scoped. But figuring that out from this strange error message requires a lot of thought.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16225GHC HEAD-only Core Lint error (Trans coercion mis-match)2019-07-07T18:00:54ZRyan ScottGHC HEAD-only Core Lint error (Trans coercion mis-match)The following code compiles on GHC 8.0.2 through GHC 8.6.3 with `-dcore-lint`:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
mo...The following code compiles on GHC 8.0.2 through GHC 8.6.3 with `-dcore-lint`:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data family Sing :: k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data TyCon1 :: (k1 -> k2) -> (k1 ~> k2)
type instance Apply (TyCon1 f) x = f x
data SomeApply :: (k ~> Type) -> Type where
SomeApply :: Apply f a -> SomeApply f
f :: SomeApply (TyCon1 Sing :: k ~> Type)
-> SomeApply (TyCon1 Sing :: k ~> Type)
f (SomeApply s)
= SomeApply s
```
However, it chokes on GHC HEAD:
```
$ ~/Software/ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint
GHCi, version 8.7.20190120: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
In the expression: SomeApply
@ k_a1Dz
@ (TyCon1 Sing)
@ Any
(s_a1Bq
`cast` (Sub (D:R:ApplyabTyCon1x[0]
<k_a1Dz>_N
<*>_N
<Sing>_N
<a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]
<k_a1Dz>_N <*>_N <Sing>_N <Any>_N))
:: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing) Any))
Trans coercion mis-match: D:R:ApplyabTyCon1x[0]
<k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]
<k_a1Dz>_N
<*>_N
<Sing>_N
<Any>_N)
Apply (TyCon1 Sing) a_a1DB
Sing a_a1DB
Sing Any
Apply (TyCon1 Sing) Any
*** Offending Program ***
<elided>
f :: forall k. SomeApply (TyCon1 Sing) -> SomeApply (TyCon1 Sing)
[LclIdX]
f = \ (@ k_a1Dz) (ds_d1EV :: SomeApply (TyCon1 Sing)) ->
case ds_d1EV of wild_00 { SomeApply @ a_a1DB s_a1Bq ->
break<0>(s_a1Bq)
SomeApply
@ k_a1Dz
@ (TyCon1 Sing)
@ Any
(s_a1Bq
`cast` (Sub (D:R:ApplyabTyCon1x[0]
<k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]
<k_a1Dz>_N
<*>_N
<Sing>_N
<Any>_N))
:: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing) Any))
}
```
Note that if I change the definition of `Sing` to this:
```hs
data family Sing (a :: k)
```
Then the error goes away.
Also, if I extend `SomeProxy` with an additional `proxy` field:
```hs
data SomeApply :: (k ~> Type) -> Type where
SomeApply :: proxy a -> Apply f a -> SomeApply f
f :: SomeApply (TyCon1 Sing :: k ~> Type)
-> SomeApply (TyCon1 Sing :: k ~> Type)
f (SomeApply p s)
= SomeApply p s
```
Then the error also goes away. Perhaps `a` being ambiguous plays an important role here?
Possibly related to #16188 or #16204.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.7 |
| 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-only Core Lint error (Trans coercion mis-match)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles on GHC 8.0.2 through GHC 8.6.3 with `-dcore-lint`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing :: k -> Type\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 TyCon1 :: (k1 -> k2) -> (k1 ~> k2)\r\ntype instance Apply (TyCon1 f) x = f x\r\n\r\ndata SomeApply :: (k ~> Type) -> Type where\r\n SomeApply :: Apply f a -> SomeApply f\r\n\r\nf :: SomeApply (TyCon1 Sing :: k ~> Type)\r\n -> SomeApply (TyCon1 Sing :: k ~> Type)\r\nf (SomeApply s)\r\n = SomeApply s\r\n}}}\r\n\r\nHowever, it chokes on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint\r\nGHCi, version 8.7.20190120: https://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n*** Core Lint errors : in result of Desugar (before optimization) ***\r\n<no location info>: warning:\r\n In the expression: SomeApply\r\n @ k_a1Dz\r\n @ (TyCon1 Sing)\r\n @ Any\r\n (s_a1Bq\r\n `cast` (Sub (D:R:ApplyabTyCon1x[0]\r\n <k_a1Dz>_N\r\n <*>_N\r\n <Sing>_N\r\n <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]\r\n <k_a1Dz>_N <*>_N <Sing>_N <Any>_N))\r\n :: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing) Any))\r\n Trans coercion mis-match: D:R:ApplyabTyCon1x[0]\r\n <k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]\r\n <k_a1Dz>_N\r\n <*>_N\r\n <Sing>_N\r\n <Any>_N)\r\n Apply (TyCon1 Sing) a_a1DB\r\n Sing a_a1DB\r\n Sing Any\r\n Apply (TyCon1 Sing) Any\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\nf :: forall k. SomeApply (TyCon1 Sing) -> SomeApply (TyCon1 Sing)\r\n[LclIdX]\r\nf = \\ (@ k_a1Dz) (ds_d1EV :: SomeApply (TyCon1 Sing)) ->\r\n case ds_d1EV of wild_00 { SomeApply @ a_a1DB s_a1Bq ->\r\n break<0>(s_a1Bq)\r\n SomeApply\r\n @ k_a1Dz\r\n @ (TyCon1 Sing)\r\n @ Any\r\n (s_a1Bq\r\n `cast` (Sub (D:R:ApplyabTyCon1x[0]\r\n <k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ; Sym (D:R:ApplyabTyCon1x[0]\r\n <k_a1Dz>_N\r\n <*>_N\r\n <Sing>_N\r\n <Any>_N))\r\n :: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing) Any))\r\n }\r\n}}}\r\n\r\nNote that if I change the definition of `Sing` to this:\r\n\r\n{{{#!hs\r\ndata family Sing (a :: k)\r\n}}}\r\n\r\nThen the error goes away.\r\n\r\nAlso, if I extend `SomeProxy` with an additional `proxy` field:\r\n\r\n{{{#!hs\r\ndata SomeApply :: (k ~> Type) -> Type where\r\n SomeApply :: proxy a -> Apply f a -> SomeApply f\r\n\r\nf :: SomeApply (TyCon1 Sing :: k ~> Type)\r\n -> SomeApply (TyCon1 Sing :: k ~> Type)\r\nf (SomeApply p s)\r\n = SomeApply p s\r\n}}}\r\n\r\nThen the error also goes away. Perhaps `a` being ambiguous plays an important role here?\r\n\r\nPossibly related to #16188 or #16204.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/16204GHC HEAD-only Core Lint error (Argument value doesn't match argument type)2019-07-07T18:00:58ZRyan ScottGHC HEAD-only Core Lint error (Argument value doesn't match argument type)The following program passes Core Lint on GHC 8.6.3:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{...The following program passes Core Lint on GHC 8.6.3:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
-----
-- singletons machinery
-----
data family Sing :: forall k. k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
-----
-- (Simplified) GHC.Generics
-----
class Generic (a :: Type) where
type Rep a :: Type
from :: a -> Rep a
to :: Rep a -> a
class PGeneric (a :: Type) where
-- type PFrom ...
type PTo (x :: Rep a) :: a
class SGeneric k where
-- sFrom :: ...
sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
-----
class SingKind k where
type Demote k :: Type
-- fromSing :: ...
toSing :: Demote k -> SomeSing k
genericToSing :: forall k.
( SingKind k, SGeneric k, SingKind (Rep k)
, Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
=> Demote k -> SomeSing k
genericToSing d = withSomeSing @(Rep k) (from d) $ SomeSing . sTo
withSomeSing :: forall k r
. SingKind k
=> Demote k
-> (forall (a :: k). Sing a -> r)
-> r
withSomeSing x f =
case toSing x of
SomeSing x' -> f x'
```
But not on GHC HEAD:
```
$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
In the expression: $ @ 'LiftedRep
@ (forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)
@ (SomeSing k_a1cV)
(withSomeSing
@ (Rep k_a1cV)
@ (SomeSing k_a1cV)
$dSingKind_a1d5
((from
@ (Demote k_a1cV)
$dGeneric_a1d7
(d_aX7
`cast` (Sub co_a1dK
:: Demote k_a1cV[sk:1] ~R# Demote k_a1cV[sk:1])))
`cast` (Sub (Sym (Sym co_a1dR ; Sym co_a1dM) ; (Sym co_a1dQ ; (Demote
(Sym co_a1dO))_N))
:: Rep (Demote k_a1cV[sk:1]) ~R# Demote (Rep k_a1cV[sk:1]))))
(\ (@ (a_a1dc :: Rep k_a1cV)) ->
let {
$dSGeneric_a1dm :: SGeneric k_a1cV
[LclId]
$dSGeneric_a1dm = $dSGeneric_a1cY } in
. @ (Sing (PTo Any))
@ (SomeSing k_a1cV)
@ (Sing Any)
(SomeSing @ k_a1cV @ (PTo Any))
((sTo @ k_a1cV $dSGeneric_a1dm @ Any)
`cast` (Sym (Sing
(Sym co_a1dO) (Sym (GRefl nominal Any co_a1dO)))_R
->_R <Sing (PTo Any)>_R
:: (Sing Any -> Sing (PTo Any))
~R# (Sing Any -> Sing (PTo Any)))))
Argument value doesn't match argument type:
Fun type:
(forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)
-> SomeSing k_a1cV
Arg type: forall (a :: Rep k_a1cV). Sing Any -> SomeSing k_a1cV
Arg:
\ (@ (a_a1dc :: Rep k_a1cV)) ->
let {
$dSGeneric_a1dm :: SGeneric k_a1cV
[LclId]
$dSGeneric_a1dm = $dSGeneric_a1cY } in
. @ (Sing (PTo Any))
@ (SomeSing k_a1cV)
@ (Sing Any)
(SomeSing @ k_a1cV @ (PTo Any))
((sTo @ k_a1cV $dSGeneric_a1dm @ Any)
`cast` (Sym (Sing
(Sym co_a1dO) (Sym (GRefl nominal Any co_a1dO)))_R
->_R <Sing (PTo Any)>_R
:: (Sing Any -> Sing (PTo Any)) ~R# (Sing Any -> Sing (PTo Any))))
*** Offending Program ***
<elided>
genericToSing
:: forall k.
(SingKind k, SGeneric k, SingKind (Rep k), Generic (Demote k),
Rep (Demote k) ~ Demote (Rep k)) =>
Demote k -> SomeSing k
[LclIdX]
genericToSing
= \ (@ k_a1cV)
($dSingKind_a1cX :: SingKind k_a1cV)
($dSGeneric_a1cY :: SGeneric k_a1cV)
($dSingKind_a1cZ :: SingKind (Rep k_a1cV))
($dGeneric_a1d0 :: Generic (Demote k_a1cV))
($d~_a1d1 :: Rep (Demote k_a1cV) ~ Demote (Rep k_a1cV)) ->
let {
co_a1dQ :: Demote (Rep k_a1cV) ~# Demote (Rep k_a1cV)
[LclId[CoVarId]]
co_a1dQ = CO: <Demote (Rep k_a1cV)>_N } in
let {
co_a1dO :: Rep k_a1cV ~# Rep k_a1cV
[LclId[CoVarId]]
co_a1dO = CO: <Rep k_a1cV>_N } in
let {
$dSingKind_a1dT :: SingKind (Rep k_a1cV)
[LclId]
$dSingKind_a1dT
= $dSingKind_a1cZ
`cast` (Sub (Sym (SingKind (Sym co_a1dO))_N)
:: SingKind (Rep k_a1cV[sk:1])
~R# SingKind (Rep k_a1cV[sk:1])) } in
let {
$dSingKind_a1d5 :: SingKind (Rep k_a1cV)
[LclId]
$dSingKind_a1d5
= $dSingKind_a1dT
`cast` ((SingKind (Sym co_a1dO))_R
:: SingKind (Rep k_a1cV[sk:1])
~R# SingKind (Rep k_a1cV[sk:1])) } in
let {
co_a1dM :: Rep (Demote k_a1cV) ~# Rep (Demote k_a1cV)
[LclId[CoVarId]]
co_a1dM = CO: <Rep (Demote k_a1cV)>_N } in
let {
co_a1dK :: Demote k_a1cV ~# Demote k_a1cV
[LclId[CoVarId]]
co_a1dK = CO: <Demote k_a1cV>_N } in
let {
$dGeneric_a1dU :: Generic (Demote k_a1cV)
[LclId]
$dGeneric_a1dU
= $dGeneric_a1d0
`cast` (Sub (Sym (Generic (Sym co_a1dK))_N)
:: Generic (Demote k_a1cV[sk:1])
~R# Generic (Demote k_a1cV[sk:1])) } in
let {
$dGeneric_a1d7 :: Generic (Demote k_a1cV)
[LclId]
$dGeneric_a1d7 = $dGeneric_a1dU } in
case eq_sel
@ * @ (Rep (Demote k_a1cV)) @ (Demote (Rep k_a1cV)) $d~_a1d1
of co_a1dI
{ __DEFAULT ->
let {
co_a1dR :: Rep (Demote k_a1cV) ~# Demote (Rep k_a1cV)
[LclId[CoVarId]]
co_a1dR
= CO: ((Sym co_a1dM ; (Rep
(Sym co_a1dK))_N) ; co_a1dI) ; Sym (Sym co_a1dQ ; (Demote
(Sym co_a1dO))_N) } in
\ (d_aX7 :: Demote k_a1cV) ->
$ @ 'LiftedRep
@ (forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)
@ (SomeSing k_a1cV)
(withSomeSing
@ (Rep k_a1cV)
@ (SomeSing k_a1cV)
$dSingKind_a1d5
((from
@ (Demote k_a1cV)
$dGeneric_a1d7
(d_aX7
`cast` (Sub co_a1dK
:: Demote k_a1cV[sk:1] ~R# Demote k_a1cV[sk:1])))
`cast` (Sub (Sym (Sym co_a1dR ; Sym co_a1dM) ; (Sym co_a1dQ ; (Demote
(Sym co_a1dO))_N))
:: Rep (Demote k_a1cV[sk:1]) ~R# Demote (Rep k_a1cV[sk:1]))))
(\ (@ (a_a1dc :: Rep k_a1cV)) ->
let {
$dSGeneric_a1dm :: SGeneric k_a1cV
[LclId]
$dSGeneric_a1dm = $dSGeneric_a1cY } in
. @ (Sing (PTo Any))
@ (SomeSing k_a1cV)
@ (Sing Any)
(SomeSing @ k_a1cV @ (PTo Any))
((sTo @ k_a1cV $dSGeneric_a1dm @ Any)
`cast` (Sym (Sing
(Sym co_a1dO) (Sym (GRefl nominal Any co_a1dO)))_R
->_R <Sing (PTo Any)>_R
:: (Sing Any -> Sing (PTo Any)) ~R# (Sing Any -> Sing (PTo Any)))))
}
```
I'm not sure if this is related to #16188 (see #16188\##16204), but this Core Lint error is technically different from the one in that ticket, so I decided to open a new issue for this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.7 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #16188 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD-only Core Lint error (Argument value doesn't match argument type)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[16188],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program passes Core Lint on GHC 8.6.3:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\n-----\r\n-- singletons machinery\r\n-----\r\n\r\ndata family Sing :: forall k. k -> Type\r\ndata SomeSing :: Type -> Type where\r\n SomeSing :: Sing (a :: k) -> SomeSing k\r\n\r\n-----\r\n-- (Simplified) GHC.Generics\r\n-----\r\n\r\nclass Generic (a :: Type) where\r\n type Rep a :: Type\r\n from :: a -> Rep a\r\n to :: Rep a -> a\r\n\r\nclass PGeneric (a :: Type) where\r\n -- type PFrom ...\r\n type PTo (x :: Rep a) :: a\r\n\r\nclass SGeneric k where\r\n -- sFrom :: ...\r\n sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)\r\n\r\n-----\r\n\r\nclass SingKind k where\r\n type Demote k :: Type\r\n -- fromSing :: ...\r\n toSing :: Demote k -> SomeSing k\r\n\r\ngenericToSing :: forall k.\r\n ( SingKind k, SGeneric k, SingKind (Rep k)\r\n , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )\r\n => Demote k -> SomeSing k\r\ngenericToSing d = withSomeSing @(Rep k) (from d) $ SomeSing . sTo\r\n\r\nwithSomeSing :: forall k r\r\n . SingKind k\r\n => Demote k\r\n -> (forall (a :: k). Sing a -> r)\r\n -> r\r\nwithSomeSing x f =\r\n case toSing x of\r\n SomeSing x' -> f x'\r\n}}}\r\n\r\nBut not on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs -dcore-lint \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Desugar (before optimization) ***\r\n<no location info>: warning:\r\n In the expression: $ @ 'LiftedRep\r\n @ (forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)\r\n @ (SomeSing k_a1cV)\r\n (withSomeSing\r\n @ (Rep k_a1cV)\r\n @ (SomeSing k_a1cV)\r\n $dSingKind_a1d5\r\n ((from\r\n @ (Demote k_a1cV)\r\n $dGeneric_a1d7\r\n (d_aX7\r\n `cast` (Sub co_a1dK\r\n :: Demote k_a1cV[sk:1] ~R# Demote k_a1cV[sk:1])))\r\n `cast` (Sub (Sym (Sym co_a1dR ; Sym co_a1dM) ; (Sym co_a1dQ ; (Demote\r\n (Sym co_a1dO))_N))\r\n :: Rep (Demote k_a1cV[sk:1]) ~R# Demote (Rep k_a1cV[sk:1]))))\r\n (\\ (@ (a_a1dc :: Rep k_a1cV)) ->\r\n let {\r\n $dSGeneric_a1dm :: SGeneric k_a1cV\r\n [LclId]\r\n $dSGeneric_a1dm = $dSGeneric_a1cY } in\r\n . @ (Sing (PTo Any))\r\n @ (SomeSing k_a1cV)\r\n @ (Sing Any)\r\n (SomeSing @ k_a1cV @ (PTo Any))\r\n ((sTo @ k_a1cV $dSGeneric_a1dm @ Any)\r\n `cast` (Sym (Sing\r\n (Sym co_a1dO) (Sym (GRefl nominal Any co_a1dO)))_R\r\n ->_R <Sing (PTo Any)>_R\r\n :: (Sing Any -> Sing (PTo Any))\r\n ~R# (Sing Any -> Sing (PTo Any)))))\r\n Argument value doesn't match argument type:\r\n Fun type:\r\n (forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)\r\n -> SomeSing k_a1cV\r\n Arg type: forall (a :: Rep k_a1cV). Sing Any -> SomeSing k_a1cV\r\n Arg:\r\n \\ (@ (a_a1dc :: Rep k_a1cV)) ->\r\n let {\r\n $dSGeneric_a1dm :: SGeneric k_a1cV\r\n [LclId]\r\n $dSGeneric_a1dm = $dSGeneric_a1cY } in\r\n . @ (Sing (PTo Any))\r\n @ (SomeSing k_a1cV)\r\n @ (Sing Any)\r\n (SomeSing @ k_a1cV @ (PTo Any))\r\n ((sTo @ k_a1cV $dSGeneric_a1dm @ Any)\r\n `cast` (Sym (Sing\r\n (Sym co_a1dO) (Sym (GRefl nominal Any co_a1dO)))_R\r\n ->_R <Sing (PTo Any)>_R\r\n :: (Sing Any -> Sing (PTo Any)) ~R# (Sing Any -> Sing (PTo Any))))\r\n*** Offending Program ***\r\n<elided>\r\ngenericToSing\r\n :: forall k.\r\n (SingKind k, SGeneric k, SingKind (Rep k), Generic (Demote k),\r\n Rep (Demote k) ~ Demote (Rep k)) =>\r\n Demote k -> SomeSing k\r\n[LclIdX]\r\ngenericToSing\r\n = \\ (@ k_a1cV)\r\n ($dSingKind_a1cX :: SingKind k_a1cV)\r\n ($dSGeneric_a1cY :: SGeneric k_a1cV)\r\n ($dSingKind_a1cZ :: SingKind (Rep k_a1cV))\r\n ($dGeneric_a1d0 :: Generic (Demote k_a1cV))\r\n ($d~_a1d1 :: Rep (Demote k_a1cV) ~ Demote (Rep k_a1cV)) ->\r\n let {\r\n co_a1dQ :: Demote (Rep k_a1cV) ~# Demote (Rep k_a1cV)\r\n [LclId[CoVarId]]\r\n co_a1dQ = CO: <Demote (Rep k_a1cV)>_N } in\r\n let {\r\n co_a1dO :: Rep k_a1cV ~# Rep k_a1cV\r\n [LclId[CoVarId]]\r\n co_a1dO = CO: <Rep k_a1cV>_N } in\r\n let {\r\n $dSingKind_a1dT :: SingKind (Rep k_a1cV)\r\n [LclId]\r\n $dSingKind_a1dT\r\n = $dSingKind_a1cZ\r\n `cast` (Sub (Sym (SingKind (Sym co_a1dO))_N)\r\n :: SingKind (Rep k_a1cV[sk:1])\r\n ~R# SingKind (Rep k_a1cV[sk:1])) } in\r\n let {\r\n $dSingKind_a1d5 :: SingKind (Rep k_a1cV)\r\n [LclId]\r\n $dSingKind_a1d5\r\n = $dSingKind_a1dT\r\n `cast` ((SingKind (Sym co_a1dO))_R\r\n :: SingKind (Rep k_a1cV[sk:1])\r\n ~R# SingKind (Rep k_a1cV[sk:1])) } in\r\n let {\r\n co_a1dM :: Rep (Demote k_a1cV) ~# Rep (Demote k_a1cV)\r\n [LclId[CoVarId]]\r\n co_a1dM = CO: <Rep (Demote k_a1cV)>_N } in\r\n let {\r\n co_a1dK :: Demote k_a1cV ~# Demote k_a1cV\r\n [LclId[CoVarId]]\r\n co_a1dK = CO: <Demote k_a1cV>_N } in\r\n let {\r\n $dGeneric_a1dU :: Generic (Demote k_a1cV)\r\n [LclId]\r\n $dGeneric_a1dU\r\n = $dGeneric_a1d0\r\n `cast` (Sub (Sym (Generic (Sym co_a1dK))_N)\r\n :: Generic (Demote k_a1cV[sk:1])\r\n ~R# Generic (Demote k_a1cV[sk:1])) } in\r\n let {\r\n $dGeneric_a1d7 :: Generic (Demote k_a1cV)\r\n [LclId]\r\n $dGeneric_a1d7 = $dGeneric_a1dU } in\r\n case eq_sel\r\n @ * @ (Rep (Demote k_a1cV)) @ (Demote (Rep k_a1cV)) $d~_a1d1\r\n of co_a1dI\r\n { __DEFAULT ->\r\n let {\r\n co_a1dR :: Rep (Demote k_a1cV) ~# Demote (Rep k_a1cV)\r\n [LclId[CoVarId]]\r\n co_a1dR\r\n = CO: ((Sym co_a1dM ; (Rep\r\n (Sym co_a1dK))_N) ; co_a1dI) ; Sym (Sym co_a1dQ ; (Demote\r\n (Sym co_a1dO))_N) } in\r\n \\ (d_aX7 :: Demote k_a1cV) ->\r\n $ @ 'LiftedRep\r\n @ (forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)\r\n @ (SomeSing k_a1cV)\r\n (withSomeSing\r\n @ (Rep k_a1cV)\r\n @ (SomeSing k_a1cV)\r\n $dSingKind_a1d5\r\n ((from\r\n @ (Demote k_a1cV)\r\n $dGeneric_a1d7\r\n (d_aX7\r\n `cast` (Sub co_a1dK\r\n :: Demote k_a1cV[sk:1] ~R# Demote k_a1cV[sk:1])))\r\n `cast` (Sub (Sym (Sym co_a1dR ; Sym co_a1dM) ; (Sym co_a1dQ ; (Demote\r\n (Sym co_a1dO))_N))\r\n :: Rep (Demote k_a1cV[sk:1]) ~R# Demote (Rep k_a1cV[sk:1]))))\r\n (\\ (@ (a_a1dc :: Rep k_a1cV)) ->\r\n let {\r\n $dSGeneric_a1dm :: SGeneric k_a1cV\r\n [LclId]\r\n $dSGeneric_a1dm = $dSGeneric_a1cY } in\r\n . @ (Sing (PTo Any))\r\n @ (SomeSing k_a1cV)\r\n @ (Sing Any)\r\n (SomeSing @ k_a1cV @ (PTo Any))\r\n ((sTo @ k_a1cV $dSGeneric_a1dm @ Any)\r\n `cast` (Sym (Sing\r\n (Sym co_a1dO) (Sym (GRefl nominal Any co_a1dO)))_R\r\n ->_R <Sing (PTo Any)>_R\r\n :: (Sing Any -> Sing (PTo Any)) ~R# (Sing Any -> Sing (PTo Any)))))\r\n }\r\n}}}\r\n\r\nI'm not sure if this is related to #16188 (see https://ghc.haskell.org/trac/ghc/ticket/16188#comment:1), but this Core Lint error is technically different from the one in that ticket, so I decided to open a new issue for this.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/16188GHC HEAD-only panic (buildKindCoercion)2019-07-07T18:01:01ZRyan ScottGHC HEAD-only panic (buildKindCoercion)The following program compiles without issue on GHC 8.6.3:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators ...The following program compiles without issue on GHC 8.6.3:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind (Type)
import Data.Type.Bool (type (&&))
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data family Sing :: forall k. k -> Type
data instance Sing :: Bool -> Type where
SFalse :: Sing False
STrue :: Sing True
(%&&) :: forall (x :: Bool) (y :: Bool).
Sing x -> Sing y -> Sing (x && y)
SFalse %&& _ = SFalse
STrue %&& a = a
data RegExp :: Type -> Type where
App :: RegExp t -> RegExp t -> RegExp t
data instance Sing :: forall t. RegExp t -> Type where
SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)
data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
type instance Apply ReNotEmptySym0 r = ReNotEmpty r
type family ReNotEmpty (r :: RegExp t) :: Bool where
ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2
sReNotEmpty :: forall t (r :: RegExp t).
Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2
blah :: forall (t :: Type) (re :: RegExp t).
Sing re -> ()
blah (SApp sre1 sre2)
= case (sReNotEmpty sre1, sReNotEmpty sre2) of
(STrue, STrue) -> ()
```
However, it panics on GHC HEAD:
```
$ ~/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.20190114 for x86_64-unknown-linux):
buildKindCoercion
Any
ReNotEmpty re2_a1hm
Bool
t_a1hg
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.7 |
| 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-only panic (buildKindCoercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program compiles without issue on GHC 8.6.3:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Type.Bool (type (&&))\r\n\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\ndata family Sing :: forall k. k -> Type\r\n\r\ndata instance Sing :: Bool -> Type where\r\n SFalse :: Sing False\r\n STrue :: Sing True\r\n\r\n(%&&) :: forall (x :: Bool) (y :: Bool).\r\n Sing x -> Sing y -> Sing (x && y)\r\nSFalse %&& _ = SFalse\r\nSTrue %&& a = a\r\n\r\ndata RegExp :: Type -> Type where\r\n App :: RegExp t -> RegExp t -> RegExp t\r\n\r\ndata instance Sing :: forall t. RegExp t -> Type where\r\n SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)\r\n\r\ndata ReNotEmptySym0 :: forall t. RegExp t ~> Bool\r\ntype instance Apply ReNotEmptySym0 r = ReNotEmpty r\r\n\r\ntype family ReNotEmpty (r :: RegExp t) :: Bool where\r\n ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2\r\n\r\nsReNotEmpty :: forall t (r :: RegExp t).\r\n Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)\r\nsReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2\r\n\r\nblah :: forall (t :: Type) (re :: RegExp t).\r\n Sing re -> ()\r\nblah (SApp sre1 sre2)\r\n = case (sReNotEmpty sre1, sReNotEmpty sre2) of\r\n (STrue, STrue) -> ()\r\n}}}\r\n\r\nHowever, it panics on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20190114 for x86_64-unknown-linux):\r\n buildKindCoercion\r\n Any\r\n ReNotEmpty re2_a1hm\r\n Bool\r\n t_a1hg\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/16008GHC HEAD type family regression involving invisible arguments2019-07-07T18:02:02ZRyan ScottGHC HEAD type family regression involving invisible argumentsThe following code compiles on GHC 8.0.2 through 8.6.2:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C k where
type S :: k -> Type
data...The following code compiles on GHC 8.0.2 through 8.6.2:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C k where
type S :: k -> Type
data D :: Type -> Type
data SD :: forall a. D a -> Type
instance C (D a) where
type S = SD
```
But fails to compile on GHC HEAD (commit 73cce63f33ee80f5095085141df9313ac70d1cfa):
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:3: error:
• Type indexes must match class instance head
Expected: S @(D a)
Actual: S @(D a1)
• In the type instance declaration for ‘S’
In the instance declaration for ‘C (D a)’
|
15 | type S = SD
| ^^^^^^^^^^^
```
This regression prevents [the stitch library](https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.tar.gz) from compiling.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.7 |
| 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 type family regression involving invisible arguments","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles on GHC 8.0.2 through 8.6.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C k where\r\n type S :: k -> Type\r\n\r\ndata D :: Type -> Type\r\ndata SD :: forall a. D a -> Type\r\n\r\ninstance C (D a) where\r\n type S = SD\r\n}}}\r\n\r\nBut fails to compile on GHC HEAD (commit 73cce63f33ee80f5095085141df9313ac70d1cfa):\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:3: error:\r\n • Type indexes must match class instance head\r\n Expected: S @(D a)\r\n Actual: S @(D a1)\r\n • In the type instance declaration for ‘S’\r\n In the instance declaration for ‘C (D a)’\r\n |\r\n15 | type S = SD\r\n | ^^^^^^^^^^^\r\n}}}\r\n\r\nThis regression prevents [https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.tar.gz the stitch library] from compiling.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15942Associated type family can't be used at the kind level within other parts of ...2020-09-19T20:55:39ZIcelandjackAssociated 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 #-}...I 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)
```
```
$ ghc-stage2 --interactive -ignore-dot-ghci 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/15883GHC panic: newtype F rep = F (forall (a :: TYPE rep). a)2020-01-17T16:43:24ZIcelandjackGHC panic: newtype F rep = F (forall (a :: TYPE rep). a)```hs
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interact...```hs
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci /tmp/U.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64-unknown-linux):
isUnliftedType
forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type
isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic: newtype F rep = F (forall (a :: TYPE rep). a)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language KindSignatures #-}\r\n{-# Language PolyKinds #-}\r\n\r\nimport GHC.Exts\r\n\r\nnewtype Foo rep = MkFoo (forall (a :: TYPE rep). a)\r\n}}}\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci /tmp/U.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64-unknown-linux):\r\n isUnliftedType\r\n forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]\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/types/Type.hs:2332:10 in ghc:Type\r\n isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15881GHC Panic: data A n (a :: n) :: a -> Type2019-07-07T18:02:35ZIcelandjackGHC Panic: data A n (a :: n) :: a -> Type```hs
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Kind
data A n (a :: n) :: a -> Type
```
causes a panic on 8.7.20181017
```
$ ~/code/headghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_b...```hs
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Kind
data A n (a :: n) :: a -> Type
```
causes a panic on 8.7.20181017
```
$ ~/code/headghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 665_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64-unknown-linux):
ASSERT failed!
Type-correct unfilled coercion hole {co_a1xR}
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/TcHsSyn.hs:1805:99 in ghc:TcHsSyn
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
and an assertion failure in 8.7.20181029
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 665_bug.hs, interpreted )
*** Exception: ASSERT failed! file compiler/types/TyCon.hs, line 420
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC Panic: data A n (a :: n) :: a -> Type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language KindSignatures #-}\r\n{-# Language PolyKinds #-}\r\n\r\nimport Data.Kind\r\n\r\ndata A n (a :: n) :: a -> Type\r\n}}}\r\n\r\ncauses a panic on 8.7.20181017\r\n\r\n{{{\r\n$ ~/code/headghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 665_bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64-unknown-linux):\r\n\tASSERT failed!\r\n Type-correct unfilled coercion hole {co_a1xR}\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/TcHsSyn.hs:1805:99 in ghc:TcHsSyn\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}\r\n\r\nand an assertion failure in 8.7.20181029\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 665_bug.hs, interpreted )\r\n*** Exception: ASSERT failed! file compiler/types/TyCon.hs, line 420\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.3