GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-02-25T01:15:47Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15862Panic with promoted types that Typeable doesn't support2020-02-25T01:15:47ZRyan ScottPanic with promoted types that Typeable doesn't supportThe following program panics on GHC 8.2 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Type.Reflection
newtype Foo ...The following program panics on GHC 8.2 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Type.Reflection
newtype Foo = MkFoo (forall a. a)
foo :: TypeRep MkFoo
foo = typeRep @MkFoo
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
GHC error in desugarer lookup in Bug:
attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.1 for x86_64-unknown-linux):
initDs
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typeable panic with promoted rank-2 kind (initDs)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC 8.2 and later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\nnewtype Foo = MkFoo (forall a. a)\r\n\r\nfoo :: TypeRep MkFoo\r\nfoo = typeRep @MkFoo\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nGHC error in desugarer lookup in Bug:\r\n attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.1 for x86_64-unknown-linux):\r\n initDs\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Ryan ScottRyan Scotthttps://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/13399Location of `forall` matters with higher-rank kind polymorphism2020-05-21T22:48:30ZEric CrockettLocation of `forall` matters with higher-rank kind polymorphismThe following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- erro...The following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- error on this line
```
with the error
```
• Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
• In the first argument of ‘C’, namely ‘Foo a’
In the instance declaration for ‘C (Foo a)’
```
Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:
Decl 2: `data Foo :: (* -> *) -> k -> *`
Decl 3: `data Foo (a :: * -> *) (b :: k)`
However, if I move the `forall` to a point *after* the first type parameter (which is where the instance is partially applied) thusly:
Decl 4: `data Foo :: (* -> *) -> forall k . k -> *`
then GHC happily accepts the instance of `C`.
From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.8.4.1https://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/12081TypeInType Compile-time Panic2020-09-19T19:52:25ZMichaelKTypeInType Compile-time PanicI've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:
```hs
{-# LANGUAGE TypeInType #-}
data Nat = Z | S Nat
class C (n :: Nat) where
type T n :: Nat
f :: (a :: T n)
```
```
...I've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:
```hs
{-# LANGUAGE TypeInType #-}
data Nat = Z | S Nat
class C (n :: Nat) where
type T n :: Nat
f :: (a :: T n)
```
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.0.20160421 for x86_64-apple-darwin):
isInjectiveTyCon sees a TcTyCon T
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc4 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeInType Compile-time Panic","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Nat = Z | S Nat\r\n\r\nclass C (n :: Nat) where\r\n type T n :: Nat\r\n f :: (a :: T n)\r\n}}}\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.0.20160421 for x86_64-apple-darwin):\r\n\tisInjectiveTyCon sees a TcTyCon T\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12174Recursive use of type-in-type results in infinite loop2020-09-19T19:52:25ZEdward Z. YangRecursive use of type-in-type results in infinite loopTypechecking this module results in an infinite loop:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
module X where
data V a
data T = forall (a :: S...Typechecking this module results in an infinite loop:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
module X where
data V a
data T = forall (a :: S). MkT (V a)
data S = forall (a :: T). MkS (V a)
```
There's a mutually recursive reference so it should be rejected but maybe the check is not happening early enough (or the existing check is only for self-reference.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Recursive use of type-in-type results in infinite loop","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Typechecking this module results in an infinite loop:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule X where\r\n\r\ndata V a\r\ndata T = forall (a :: S). MkT (V a)\r\ndata S = forall (a :: T). MkS (V a)\r\n}}}\r\n\r\nThere's a mutually recursive reference so it should be rejected but maybe the check is not happening early enough (or the existing check is only for self-reference.)","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11554Self quantification in GADT data declarations2020-09-19T20:01:19ZRafbillSelf quantification in GADT data declarationsGHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{-# LANGUAGE GADTs, TypeInType...GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{-# LANGUAGE GADTs, TypeInType #-}
import Data.Kind
data A :: Type where
B :: forall (a :: A). A
```
I guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc2 |
| 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":"Self quantification in GADT data declarations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56) :\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeInType #-}\r\nimport Data.Kind\r\ndata A :: Type where\r\n B :: forall (a :: A). A\r\n}}}\r\n\r\nI guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15942Associated type family can't be used at the kind level within other parts of ...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/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/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/15079GHC HEAD regression: cannot instantiate higher-rank kind2020-10-31T11:08:22ZRyan ScottGHC HEAD regression: cannot instantiate higher-rank kindThe following program typechecks on GHC 8.2.2 and 8.4.2:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Void
inf...The following program typechecks on GHC 8.2.2 and 8.4.2:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Void
infixl 4 :==
-- | Heterogeneous Leibnizian equality.
newtype (a :: j) :== (b :: k)
= HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }
newtype Coerce a = Coerce { uncoerce :: Starify a }
type family Starify (a :: k) :: Type where
Starify (a :: Type) = a
Starify _ = Void
coerce :: a :== b -> a -> b
coerce f = uncoerce . hsubst f . Coerce
```
But GHC HEAD rejects it:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:21:34: error:
• Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:
Coerce :: forall k. k -> *
Their kinds differ.
Expected type: a -> c0 * a
Actual type: Starify a -> Coerce a
• In the second argument of ‘(.)’, namely ‘Coerce’
In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
In the expression: uncoerce . hsubst f . Coerce
|
21 | coerce f = uncoerce . hsubst f . Coerce
| ^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression: cannot instantiate higher-rank kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.2.2 and 8.4.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ninfixl 4 :==\r\n-- | Heterogeneous Leibnizian equality.\r\nnewtype (a :: j) :== (b :: k)\r\n = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }\r\n\r\nnewtype Coerce a = Coerce { uncoerce :: Starify a }\r\ntype family Starify (a :: k) :: Type where\r\n Starify (a :: Type) = a\r\n Starify _ = Void\r\n\r\ncoerce :: a :== b -> a -> b\r\ncoerce f = uncoerce . hsubst f . Coerce\r\n}}}\r\n\r\nBut GHC HEAD rejects it:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:21:34: error:\r\n • Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:\r\n Coerce :: forall k. k -> *\r\n Their kinds differ.\r\n Expected type: a -> c0 * a\r\n Actual type: Starify a -> Coerce a\r\n • In the second argument of ‘(.)’, namely ‘Coerce’\r\n In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’\r\n In the expression: uncoerce . hsubst f . Coerce\r\n |\r\n21 | coerce f = uncoerce . hsubst f . Coerce\r\n | ^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://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/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/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/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/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/15474Error message mentions Any2021-01-11T13:19:08ZKrzysztof GogolewskiError message mentions AnyI'm not sure if this is a bug. File:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f...I'm not sure if this is a bug. File:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f2 :: Forall
f2 = f1
```
gives an error message mentioning Any:
```
• Couldn't match type ‘GHC.Types.Any’ with ‘*’
Expected type: Proxy t
Actual type: Proxy t0
```
The appearance of Any is suspicious to me - I thought it's an implementation detail?9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11196TypeInType performance regressions2021-03-31T16:11:18ZRichard Eisenbergrae@richarde.devTypeInType performance regressionsThis ticket is to track the handful of performance regressions seen with the addition of `TypeInType`. It is quite possibly a good idea to break these out into separate tickets, but until we investigate, they're all bundled here.
The re...This ticket is to track the handful of performance regressions seen with the addition of `TypeInType`. It is quite possibly a good idea to break these out into separate tickets, but until we investigate, they're all bundled here.
The regressions are (all in bytes allocated, unless otherwise noted):
- T3064, up by 14.9%
- T5030, up by 61.8%
- T5837, up by 13%
- T5321Fun, up by 11%
- T5631, up by 39%
- T9872d, **down** by 22% (see below)
- T9872a, up by 33.6%
- T9872c, up by 59.4%
- T9872b, up by 49.4%
- T9675, up by 29.7%, and peak megabytes allocated up by 28.4%
- haddock.base, up by 12.4%
- haddock.Cabal, up by 9.5%
I did add an optimization around type family reduction (the function `zonk_eq_types` in !TcCanonical) that could cause such a drastic reduction.8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14873The well-kinded type invariant (in TcType)2021-09-07T15:47:33ZRyan ScottThe well-kinded type invariant (in TcType)(Originally noticed [here](https://travis-ci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTyp...(Originally noticed [here](https://travis-ci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a -> a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type -> Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type -> Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x -> Sing y -> Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64-unknown-linux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] |> <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travis-ci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a -> a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type -> Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type -> Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x -> Sing y -> Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180201 for x86_64-unknown-linux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] |> <*>_N)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->9.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12369data families shouldn't be required to have return kind *, data instances should2021-09-09T23:17:59ZEdward Kmettdata families shouldn't be required to have return kind *, data instances shouldI'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1...I'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1: error:
• Kind signature on data type declaration has non-* return kind
(k -> *) -> k
• In the data family declaration for ‘Fix’
```
Ultimately I think the issue here is that data __instances__ should be required to end in kind \*, not the families, but this generalization didn't mean anything until we had `PolyKinds`.
As an example of a usecase, with the above, I could define a bifunctor fixed point such as
```hs
newtype instance Fix f a = In2 { out2 :: f (Fix f a) a }
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| 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":"data families shouldn't be required to have return kind *, data instances should","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I'd like to be able to define\r\n\r\n{{{#!hs\r\n{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}\r\ndata family Fix :: (k -> *) -> k\r\nnewtype instance Fix f = In { out :: f (Fix f) }\r\n}}}\r\n\r\nBut currently this is disallowed:\r\n\r\n{{{\r\nFix.hs:2:1: error:\r\n • Kind signature on data type declaration has non-* return kind\r\n (k -> *) -> k\r\n • In the data family declaration for ‘Fix’\r\n}}}\r\n\r\nUltimately I think the issue here is that data __instances__ should be required to end in kind *, not the families, but this generalization didn't mean anything until we had `PolyKinds`.\r\n\r\nAs an example of a usecase, with the above, I could define a bifunctor fixed point such as\r\n\r\n{{{#!hs\r\nnewtype instance Fix f a = In2 { out2 :: f (Fix f a) a }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1