GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:27:19Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/12176Failure of bidirectional type inference at the kind level2019-07-07T18:27:19ZRichard Eisenbergrae@richarde.devFailure of bidirectional type inference at the kind levelI'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:
```hs
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k). Proxy a -> X
type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
type family Foo (x :: forall (a :: k). Proxy a -> X) where
Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
```
Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi telling me the following (with `-fprint-explicit-kinds`):
```
λ> :i Foo
type family Foo k (x :: forall (a :: k). Proxy k a -> X)
:: Proxy * k
where [k] Foo k ('MkX k) = 'MkProxy * k
```
That is, I wished to extract the kind parameter to `MkK`, matching against a partially-applied `MkX`, and GHC understood that intention.
However, sadly, writing `Foo Expr` produces
```
• Expected kind ‘forall (a :: k0). Proxy k0 a -> X’,
but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’
• In the first argument of ‘Foo’, namely ‘Expr’
In the type ‘Foo Expr’
In the type family declaration for ‘XXX’
```
For some reason, `Expr` is getting instantiated when it shouldn't be.
Perhaps there's a simpler test case demonstrating the bug, but I feel so gleeful that this chicanery is accepted at all that I wanted to post.I'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:
```hs
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k). Proxy a -> X
type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
type family Foo (x :: forall (a :: k). Proxy a -> X) where
Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
```
Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi telling me the following (with `-fprint-explicit-kinds`):
```
λ> :i Foo
type family Foo k (x :: forall (a :: k). Proxy k a -> X)
:: Proxy * k
where [k] Foo k ('MkX k) = 'MkProxy * k
```
That is, I wished to extract the kind parameter to `MkK`, matching against a partially-applied `MkX`, and GHC understood that intention.
However, sadly, writing `Foo Expr` produces
```
• Expected kind ‘forall (a :: k0). Proxy k0 a -> X’,
but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’
• In the first argument of ‘Foo’, namely ‘Expr’
In the type ‘Foo Expr’
In the type family declaration for ‘XXX’
```
For some reason, `Expr` is getting instantiated when it shouldn't be.
Perhaps there's a simpler test case demonstrating the bug, but I feel so gleeful that this chicanery is accepted at all that I wanted to post.8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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). 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":[]} -->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/12102“Constraints in kinds” illegal family application in instance (+ documentatio...2019-07-07T18:27:39ZIcelandjack“Constraints in kinds” illegal family application in instance (+ documentation issues?)GHC 8.0.0.20160511. Example from the user guide: [Constraints in kinds](https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.html#constraints-in-kinds)
```hs
type family IsTypeLit a where
IsTypeLit Nat = 'True
IsTypeLit Symbol = 'True
IsTypeLit a = 'False
data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
MkNat :: T 42
MkSymbol :: T "Don't panic!"
```
Deriving a standalone `Show` instance \*without\* the constraint `(IsTypeLit a ~ 'True) => ` works fine
```hs
deriving instance Show (T a)
```
but I couldn't define a `Show` instance given the constraints:
```hs
-- • Couldn't match expected kind ‘'True’
-- with actual kind ‘IsTypeLit a0’
-- The type variable ‘a0’ is ambiguous
-- • In the first argument of ‘Show’, namely ‘T a’
-- In the stand-alone deriving instance for ‘Show (T a)’
deriving instance Show (T a)
```
let's add constraints
```hs
-- • Couldn't match expected kind ‘'True’
-- with actual kind ‘IsTypeLit lit’
-- • In the first argument of ‘Show’, namely ‘T (a :: lit)’
-- In the instance declaration for ‘Show (T (a :: lit))’
instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where
```
let's derive for a single literal
```hs
-- • Illegal type synonym family application in instance:
-- T Nat
-- ('Data.Type.Equality.C:~
-- Bool
-- (IsTypeLit Nat)
-- 'True
-- ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>))
-- 42
-- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’
deriving instance Show (T (42 :: Nat))
```
same happens with
```hs
instance Show (T 42) where
```
----
The documentation
> Note that explicitly quantifying with `forall a` is not necessary here.
seems to be wrong since removing it results in
```
tVDv.hs:10:17-18: error: …
• Expected kind ‘a’, but ‘42’ has kind ‘Nat’
• In the first argument of ‘T’, namely ‘42’
In the type ‘T 42’
In the definition of data constructor ‘MkNat’
Compilation failed.
```GHC 8.0.0.20160511. Example from the user guide: [Constraints in kinds](https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.html#constraints-in-kinds)
```hs
type family IsTypeLit a where
IsTypeLit Nat = 'True
IsTypeLit Symbol = 'True
IsTypeLit a = 'False
data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
MkNat :: T 42
MkSymbol :: T "Don't panic!"
```
Deriving a standalone `Show` instance \*without\* the constraint `(IsTypeLit a ~ 'True) => ` works fine
```hs
deriving instance Show (T a)
```
but I couldn't define a `Show` instance given the constraints:
```hs
-- • Couldn't match expected kind ‘'True’
-- with actual kind ‘IsTypeLit a0’
-- The type variable ‘a0’ is ambiguous
-- • In the first argument of ‘Show’, namely ‘T a’
-- In the stand-alone deriving instance for ‘Show (T a)’
deriving instance Show (T a)
```
let's add constraints
```hs
-- • Couldn't match expected kind ‘'True’
-- with actual kind ‘IsTypeLit lit’
-- • In the first argument of ‘Show’, namely ‘T (a :: lit)’
-- In the instance declaration for ‘Show (T (a :: lit))’
instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where
```
let's derive for a single literal
```hs
-- • Illegal type synonym family application in instance:
-- T Nat
-- ('Data.Type.Equality.C:~
-- Bool
-- (IsTypeLit Nat)
-- 'True
-- ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>))
-- 42
-- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’
deriving instance Show (T (42 :: Nat))
```
same happens with
```hs
instance Show (T 42) where
```
----
The documentation
> Note that explicitly quantifying with `forall a` is not necessary here.
seems to be wrong since removing it results in
```
tVDv.hs:10:17-18: error: …
• Expected kind ‘a’, but ‘42’ has kind ‘Nat’
• In the first argument of ‘T’, namely ‘42’
In the type ‘T 42’
In the definition of data constructor ‘MkNat’
Compilation failed.
```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)
```
```
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":[]} -->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/12045Visible kind application2019-07-07T18:27:52ZIcelandjackVisible kind applicationI've wanted this for a while
```
ghci> :kind (:~:)
(:~:) :: k -> k -> Type
```
```
ghci> :kind (:~:) @(Type -> Type)
(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) []
(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) [] Maybe
(:~:) @(Type -> Type) [] Maybe :: Type
```
Working like
```
ghci> type Same k (a::k) (b::k) = a :~: b
ghci> :kind Same
Same :: forall k -> k -> k -> *
```
```
ghci> :kind Same (Type -> Type)
Same (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *
ghci> :kind Same (Type -> Type) []
Same (Type -> Type) [] :: (Type -> Type) -> *
ghci> :kind Same (Type -> Type) [] Maybe
Same (Type -> Type) [] Maybe :: *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Visible kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeApplications","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I've wanted this for a while\r\n\r\n{{{\r\nghci> :kind (:~:)\r\n(:~:) :: k -> k -> Type\r\n}}}\r\n\r\n{{{\r\nghci> :kind (:~:) @(Type -> Type)\r\n(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) []\r\n(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) [] Maybe\r\n(:~:) @(Type -> Type) [] Maybe :: Type\r\n}}}\r\n\r\nWorking like\r\n\r\n{{{\r\nghci> type Same k (a::k) (b::k) = a :~: b\r\nghci> :kind Same\r\nSame :: forall k -> k -> k -> *\r\n}}}\r\n\r\n{{{\r\nghci> :kind Same (Type -> Type)\r\nSame (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) []\r\nSame (Type -> Type) [] :: (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) [] Maybe\r\nSame (Type -> Type) [] Maybe :: *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->I've wanted this for a while
```
ghci> :kind (:~:)
(:~:) :: k -> k -> Type
```
```
ghci> :kind (:~:) @(Type -> Type)
(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) []
(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) [] Maybe
(:~:) @(Type -> Type) [] Maybe :: Type
```
Working like
```
ghci> type Same k (a::k) (b::k) = a :~: b
ghci> :kind Same
Same :: forall k -> k -> k -> *
```
```
ghci> :kind Same (Type -> Type)
Same (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *
ghci> :kind Same (Type -> Type) []
Same (Type -> Type) [] :: (Type -> Type) -> *
ghci> :kind Same (Type -> Type) [] Maybe
Same (Type -> Type) [] Maybe :: *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Visible kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeApplications","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I've wanted this for a while\r\n\r\n{{{\r\nghci> :kind (:~:)\r\n(:~:) :: k -> k -> Type\r\n}}}\r\n\r\n{{{\r\nghci> :kind (:~:) @(Type -> Type)\r\n(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) []\r\n(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) [] Maybe\r\n(:~:) @(Type -> Type) [] Maybe :: Type\r\n}}}\r\n\r\nWorking like\r\n\r\n{{{\r\nghci> type Same k (a::k) (b::k) = a :~: b\r\nghci> :kind Same\r\nSame :: forall k -> k -> k -> *\r\n}}}\r\n\r\n{{{\r\nghci> :kind Same (Type -> Type)\r\nSame (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) []\r\nSame (Type -> Type) [] :: (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) [] Maybe\r\nSame (Type -> Type) [] Maybe :: *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1My NguyenMy Nguyenhttps://gitlab.haskell.org/ghc/ghc/-/issues/12030GHCi Proposal: Display (Data.Kind.)Type instead of *2019-07-07T18:27:55ZIcelandjackGHCi Proposal: Display (Data.Kind.)Type instead of *This is premature but what the darn,
```
>>> :kind Maybe
Maybe :: Type -> Type
>>> :kind StateT
StateT :: Type -> (Type -> Type) -> Type -> Type
>>> :kind Eq
Eq :: Type -> Constraint
>>> :info Functor
class Functor (f :: Type -> Type) where
...
```
`*` throws students off in my experience, makes it seem scarier than it is. Symbols are harder to search for and understand without documentation, `Type` on the other hand is descriptive.
There are arguments against:
1. It's a recent feature that is subject to change.
1. `*` is established in questions online, educational material, logs and blogs.
1. `Type` is not in scope by default: user cannot query GHCi.
`*` is established and searching for “Haskell asterisk” yields a lot resources but [‘\*’ is also a wildcard](https://support.google.com/websearch/answer/2466433?hl=en) in Google and ignored by GitHub. With time `Type` would be a good search term but currently it's chicken-and-the-egg.
Previous versions of GHCi error on `:kind *` and `:info *` only shows multiplication so that wouldn't be a huge difference but we can qualify by default:
```
>>> :kind Maybe
Maybe :: Data.Kind.Type -> Data.Kind.Type
>>> :kind StateT
StateT :: Data.Kind.Type -> (Data.Kind.Type -> Data.Kind.Type) -> Data.Kind.Type -> Data.Kind.Type
>>> :kind Eq
Eq :: Data.Kind.Type -> Constraint
>>> :info Functor
class Functor (f :: Data.Kind.Type -> Data.Kind.Type) where
...
```
or display `*` normally and only when `TypeInType` is set do we display `Type`. I don't love it (and love `GHC.Types.Type` slightly less) but there is a precedent for unqualified names, browsing the Prelude for example:
```hs
($) ::
forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
(a -> b) -> a -> b
undefined ::
forall (r :: GHC.Types.RuntimeRep) (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
```
__If__ the consensus is that this will happen sometime down the line consider that each passing release means many more books and blog posts get written using `*`.
I wasn't planning on resulting to scare tactics but [here we are](https://www.peoria.com/spaw/spawimages/members/member60763/shoot_this_dog.jpg)...
----
If needed a migration plan can be drafted like the Semigroup/FTP/AMP/BBP/MonadFail/expanding Float/... proposals, possibly culminating in `Type` fully replacing `*` and being imported by default. I'm sure there are some further reaching consequences to this and better arguments against.This is premature but what the darn,
```
>>> :kind Maybe
Maybe :: Type -> Type
>>> :kind StateT
StateT :: Type -> (Type -> Type) -> Type -> Type
>>> :kind Eq
Eq :: Type -> Constraint
>>> :info Functor
class Functor (f :: Type -> Type) where
...
```
`*` throws students off in my experience, makes it seem scarier than it is. Symbols are harder to search for and understand without documentation, `Type` on the other hand is descriptive.
There are arguments against:
1. It's a recent feature that is subject to change.
1. `*` is established in questions online, educational material, logs and blogs.
1. `Type` is not in scope by default: user cannot query GHCi.
`*` is established and searching for “Haskell asterisk” yields a lot resources but [‘\*’ is also a wildcard](https://support.google.com/websearch/answer/2466433?hl=en) in Google and ignored by GitHub. With time `Type` would be a good search term but currently it's chicken-and-the-egg.
Previous versions of GHCi error on `:kind *` and `:info *` only shows multiplication so that wouldn't be a huge difference but we can qualify by default:
```
>>> :kind Maybe
Maybe :: Data.Kind.Type -> Data.Kind.Type
>>> :kind StateT
StateT :: Data.Kind.Type -> (Data.Kind.Type -> Data.Kind.Type) -> Data.Kind.Type -> Data.Kind.Type
>>> :kind Eq
Eq :: Data.Kind.Type -> Constraint
>>> :info Functor
class Functor (f :: Data.Kind.Type -> Data.Kind.Type) where
...
```
or display `*` normally and only when `TypeInType` is set do we display `Type`. I don't love it (and love `GHC.Types.Type` slightly less) but there is a precedent for unqualified names, browsing the Prelude for example:
```hs
($) ::
forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
(a -> b) -> a -> b
undefined ::
forall (r :: GHC.Types.RuntimeRep) (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
```
__If__ the consensus is that this will happen sometime down the line consider that each passing release means many more books and blog posts get written using `*`.
I wasn't planning on resulting to scare tactics but [here we are](https://www.peoria.com/spaw/spawimages/members/member60763/shoot_this_dog.jpg)...
----
If needed a migration plan can be drafted like the Semigroup/FTP/AMP/BBP/MonadFail/expanding Float/... proposals, possibly culminating in `Type` fully replacing `*` and being imported by default. I'm sure there are some further reaching consequences to this and better arguments against.8.6.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/12029Notify user to import * from Data.Kind with TypeInType on2019-07-07T18:27:55ZIcelandjackNotify user to import * from Data.Kind with TypeInType onWith `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set -XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must import * from Data.Kind
<interactive>:1:1: error:
Illegal operator ‘*’ in type ‘*’
Use TypeOperators to allow operators in types
<interactive>:1:1: error: Operator applied to too few arguments: *
```
Should a similar warning be issued when she asks for information on it
```
ghci> :i *
class Num a where
...
(*) :: a -> a -> a
...
-- Defined in ‘GHC.Num’
infixl 7 *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | GHCi |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Notify user to import * from Data.Kind with TypeInType on","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `TypeInType` asking for the kind of `*` gives the user a warning to import it\r\n\r\n{{{\r\nghci> :set -XTypeInType \r\nghci> :k *\r\n\r\n<interactive>:1:1: error:\r\n Not in scope: type constructor or class ‘*’\r\n NB: With TypeInType, you must import * from Data.Kind\r\n\r\n<interactive>:1:1: error:\r\n Illegal operator ‘*’ in type ‘*’\r\n Use TypeOperators to allow operators in types\r\n\r\n<interactive>:1:1: error: Operator applied to too few arguments: *\r\n}}}\r\n\r\nShould a similar warning be issued when she asks for information on it\r\n\r\n{{{\r\nghci> :i *\r\nclass Num a where\r\n ...\r\n (*) :: a -> a -> a\r\n ...\r\n -- Defined in ‘GHC.Num’\r\ninfixl 7 *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->With `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set -XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must import * from Data.Kind
<interactive>:1:1: error:
Illegal operator ‘*’ in type ‘*’
Use TypeOperators to allow operators in types
<interactive>:1:1: error: Operator applied to too few arguments: *
```
Should a similar warning be issued when she asks for information on it
```
ghci> :i *
class Num a where
...
(*) :: a -> a -> a
...
-- Defined in ‘GHC.Num’
infixl 7 *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | GHCi |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Notify user to import * from Data.Kind with TypeInType on","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `TypeInType` asking for the kind of `*` gives the user a warning to import it\r\n\r\n{{{\r\nghci> :set -XTypeInType \r\nghci> :k *\r\n\r\n<interactive>:1:1: error:\r\n Not in scope: type constructor or class ‘*’\r\n NB: With TypeInType, you must import * from Data.Kind\r\n\r\n<interactive>:1:1: error:\r\n Illegal operator ‘*’ in type ‘*’\r\n Use TypeOperators to allow operators in types\r\n\r\n<interactive>:1:1: error: Operator applied to too few arguments: *\r\n}}}\r\n\r\nShould a similar warning be issued when she asks for information on it\r\n\r\n{{{\r\nghci> :i *\r\nclass Num a where\r\n ...\r\n (*) :: a -> a -> a\r\n ...\r\n -- Defined in ‘GHC.Num’\r\ninfixl 7 *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/11995Can't infer type2019-07-07T18:28:05ZIcelandjackCan't infer type```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → NP f xs → NP f (x:xs)
newtype K a b = K a deriving Show
unK (K a) = a
h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
Nil -> []
K x:*xs -> x : h'collapse xs
```
if we replace `xs` by an underscore:
```
tJN0.hs:13:29-30: error: …
• Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
from the context: ((k :: *) ~~ (ĸ :: *),
(t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
bound by a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3-9
‘xs’ is a rigid type variable bound by
a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3
Expected type: NP ĸ k (K ĸ a) t
Actual type: NP ĸ ĸ (K ĸ a) xs
• In the first argument of ‘h'collapse’, namely ‘xs’
In the second argument of ‘(:)’, namely ‘h'collapse xs’
In the expression: x : h'collapse xs
• Relevant bindings include
xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.
```
Should it not be able to infer that?
The Glorious Glasgow Haskell Compilation System, version 8.1.20160419```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → NP f xs → NP f (x:xs)
newtype K a b = K a deriving Show
unK (K a) = a
h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
Nil -> []
K x:*xs -> x : h'collapse xs
```
if we replace `xs` by an underscore:
```
tJN0.hs:13:29-30: error: …
• Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
from the context: ((k :: *) ~~ (ĸ :: *),
(t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
bound by a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3-9
‘xs’ is a rigid type variable bound by
a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3
Expected type: NP ĸ k (K ĸ a) t
Actual type: NP ĸ ĸ (K ĸ a) xs
• In the first argument of ‘h'collapse’, namely ‘xs’
In the second argument of ‘(:)’, namely ‘h'collapse xs’
In the expression: x : h'collapse xs
• Relevant bindings include
xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.
```
Should it not be able to infer that?
The Glorious Glasgow Haskell Compilation System, version 8.1.201604198.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/11966Surprising behavior with higher-rank quantification of kind variables2019-07-07T18:28:13ZOllie CharlesSurprising behavior with higher-rank quantification of kind variablesSorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Test where
import Data.Kind (Type)
-- Simplification
type family Col (f :: k -> j) (x :: k) :: Type
-- Base types
data PGBaseType = PGInteger | PGText
-- Transformations
data Column t = Column Symbol t
newtype Nullable t = Nullable t
newtype HasDefault t = HasDefault t
-- Interpretations
data Expr k
data Record (f :: forall k. k -> Type) =
Record {rX :: Col f ('Column "x" 'PGInteger)
,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
,rZ :: Col f ('HasDefault 'PGText)}
```
However, if I play with this in GHCI, I can get the following error:
```
λ> let x = undefined :: Record Expr
<interactive>:136:29-32: error:
• Expected kind ‘forall k. k -> Type’,
but ‘Expr’ has kind ‘forall k. k -> *’
• In the first argument of ‘Record’, namely ‘Expr’
In an expression type signature: Record Expr
In the expression: undefined :: Record Expr
```
It seems that if I write
```hs
data Expr :: forall k. k -> Type
```
things work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc3 |
| 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":"Surprising behavior with higher-rank quantification of kind variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Sorry about the rubbish title. I wrote the following code, which type checks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nimport Data.Kind (Type)\r\n\r\n-- Simplification\r\ntype family Col (f :: k -> j) (x :: k) :: Type\r\n\r\n-- Base types\r\ndata PGBaseType = PGInteger | PGText\r\n\r\n-- Transformations\r\ndata Column t = Column Symbol t\r\nnewtype Nullable t = Nullable t\r\nnewtype HasDefault t = HasDefault t\r\n\r\n-- Interpretations\r\ndata Expr k\r\n\r\ndata Record (f :: forall k. k -> Type) =\r\n Record {rX :: Col f ('Column \"x\" 'PGInteger)\r\n ,rY :: Col f ('Column \"y\" ('Nullable 'PGInteger))\r\n ,rZ :: Col f ('HasDefault 'PGText)}\r\n\r\n}}}\r\n\r\nHowever, if I play with this in GHCI, I can get the following error:\r\n\r\n{{{\r\nλ> let x = undefined :: Record Expr\r\n\r\n<interactive>:136:29-32: error:\r\n • Expected kind ‘forall k. k -> Type’,\r\n but ‘Expr’ has kind ‘forall k. k -> *’\r\n • In the first argument of ‘Record’, namely ‘Expr’\r\n In an expression type signature: Record Expr\r\n In the expression: undefined :: Record Expr\r\n}}}\r\n\r\nIt seems that if I write\r\n\r\n{{{#!hs\r\ndata Expr :: forall k. k -> Type\r\n}}}\r\n\r\nthings work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.","type_of_failure":"OtherFailure","blocking":[]} -->Sorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Test where
import Data.Kind (Type)
-- Simplification
type family Col (f :: k -> j) (x :: k) :: Type
-- Base types
data PGBaseType = PGInteger | PGText
-- Transformations
data Column t = Column Symbol t
newtype Nullable t = Nullable t
newtype HasDefault t = HasDefault t
-- Interpretations
data Expr k
data Record (f :: forall k. k -> Type) =
Record {rX :: Col f ('Column "x" 'PGInteger)
,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
,rZ :: Col f ('HasDefault 'PGText)}
```
However, if I play with this in GHCI, I can get the following error:
```
λ> let x = undefined :: Record Expr
<interactive>:136:29-32: error:
• Expected kind ‘forall k. k -> Type’,
but ‘Expr’ has kind ‘forall k. k -> *’
• In the first argument of ‘Record’, namely ‘Expr’
In an expression type signature: Record Expr
In the expression: undefined :: Record Expr
```
It seems that if I write
```hs
data Expr :: forall k. k -> Type
```
things work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc3 |
| 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":"Surprising behavior with higher-rank quantification of kind variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Sorry about the rubbish title. I wrote the following code, which type checks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nimport Data.Kind (Type)\r\n\r\n-- Simplification\r\ntype family Col (f :: k -> j) (x :: k) :: Type\r\n\r\n-- Base types\r\ndata PGBaseType = PGInteger | PGText\r\n\r\n-- Transformations\r\ndata Column t = Column Symbol t\r\nnewtype Nullable t = Nullable t\r\nnewtype HasDefault t = HasDefault t\r\n\r\n-- Interpretations\r\ndata Expr k\r\n\r\ndata Record (f :: forall k. k -> Type) =\r\n Record {rX :: Col f ('Column \"x\" 'PGInteger)\r\n ,rY :: Col f ('Column \"y\" ('Nullable 'PGInteger))\r\n ,rZ :: Col f ('HasDefault 'PGText)}\r\n\r\n}}}\r\n\r\nHowever, if I play with this in GHCI, I can get the following error:\r\n\r\n{{{\r\nλ> let x = undefined :: Record Expr\r\n\r\n<interactive>:136:29-32: error:\r\n • Expected kind ‘forall k. k -> Type’,\r\n but ‘Expr’ has kind ‘forall k. k -> *’\r\n • In the first argument of ‘Record’, namely ‘Expr’\r\n In an expression type signature: Record Expr\r\n In the expression: undefined :: Record Expr\r\n}}}\r\n\r\nIt seems that if I write\r\n\r\n{{{#!hs\r\ndata Expr :: forall k. k -> Type\r\n}}}\r\n\r\nthings work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/11964Without TypeInType, inconsistently accepts Data.Kind.Type but not type synonym2019-07-07T18:28:14ZEdward Z. YangWithout TypeInType, inconsistently accepts Data.Kind.Type but not type synonymFor convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `-XTypeInType`. Now we observe strange behavior:
```
ezyang@sabre:~$ ghc-8.0 --interactive C.hs
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( C.hs, interpreted )
Ok, modules loaded: Main.
*Main> :k T Type Int
T Type Int :: *
*Main> :k T Star Int
<interactive>:1:3: error:
• Data constructor ‘Star’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the first argument of ‘T’, namely ‘Star’
In the type ‘T Star Int’
```
Of course, if we pass `-TypeInType` to GHCi that fixes the problem (BTW, `DataKinds` does NOT solve the problem.)For convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `-XTypeInType`. Now we observe strange behavior:
```
ezyang@sabre:~$ ghc-8.0 --interactive C.hs
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( C.hs, interpreted )
Ok, modules loaded: Main.
*Main> :k T Type Int
T Type Int :: *
*Main> :k T Star Int
<interactive>:1:3: error:
• Data constructor ‘Star’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the first argument of ‘T’, namely ‘Star’
In the type ‘T Star Int’
```
Of course, if we pass `-TypeInType` to GHCi that fixes the problem (BTW, `DataKinds` does NOT solve the problem.)Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11963GHC introduces kind equality without TypeInType2019-07-07T18:28:14ZEdward Z. YangGHC introduces kind equality without TypeInTypeThe following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a circuitous way of saying:
```
{-# LANGUAGE TypeInType #-}
data Typ k (t :: k) = Typ
```
which does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?
Printing with explicit kinds makes it clear why the obvious check didn't fire:
```
ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( B.hs, interpreted )
Ok, modules loaded: Main.
*Main> :info Typ
type role Typ nominal nominal nominal
data Typ k k1 (t :: k) where
Typ :: forall k (t :: k).
(forall (a :: k -> *). a t -> a t) -> Typ k k t
-- Defined at B.hs:2:1
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| 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 introduces kind equality without TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program is accepted by GHC 8.0 rc2\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}\r\ndata Typ k t where\r\n Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t\r\n}}}\r\n\r\nThis probably shouldn't be accepted, because this is a circuitous way of saying:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata Typ k (t :: k) = Typ\r\n}}}\r\n\r\nwhich does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?\r\n\r\nPrinting with explicit kinds makes it clear why the obvious check didn't fire:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds\r\nGHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( B.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :info Typ\r\ntype role Typ nominal nominal nominal\r\ndata Typ k k1 (t :: k) where\r\n Typ :: forall k (t :: k).\r\n (forall (a :: k -> *). a t -> a t) -> Typ k k t\r\n \t-- Defined at B.hs:2:1\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->The following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a circuitous way of saying:
```
{-# LANGUAGE TypeInType #-}
data Typ k (t :: k) = Typ
```
which does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?
Printing with explicit kinds makes it clear why the obvious check didn't fire:
```
ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( B.hs, interpreted )
Ok, modules loaded: Main.
*Main> :info Typ
type role Typ nominal nominal nominal
data Typ k k1 (t :: k) where
Typ :: forall k (t :: k).
(forall (a :: k -> *). a t -> a t) -> Typ k k t
-- Defined at B.hs:2:1
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| 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 introduces kind equality without TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program is accepted by GHC 8.0 rc2\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}\r\ndata Typ k t where\r\n Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t\r\n}}}\r\n\r\nThis probably shouldn't be accepted, because this is a circuitous way of saying:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata Typ k (t :: k) = Typ\r\n}}}\r\n\r\nwhich does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?\r\n\r\nPrinting with explicit kinds makes it clear why the obvious check didn't fire:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds\r\nGHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( B.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :info Typ\r\ntype role Typ nominal nominal nominal\r\ndata Typ k k1 (t :: k) where\r\n Typ :: forall k (t :: k).\r\n (forall (a :: k -> *). a t -> a t) -> Typ k k t\r\n \t-- Defined at B.hs:2:1\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/11962Support induction recursion2020-01-06T11:26:23ZRichard Eisenbergrae@richarde.devSupport induction recursionNow that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
-- Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
-- A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k) -- we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) -> (El a -> U) -> U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x -> El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/internal#separating-type-signatures-from-definitions).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n -- Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n -- A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k) -- we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) -> (El a -> U) -> U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x -> El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} -->Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
-- Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
-- A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k) -- we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) -> (El a -> U) -> U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x -> El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/internal#separating-type-signatures-from-definitions).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n -- Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n -- A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k) -- we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) -> (El a -> U) -> U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x -> El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11821Internal error: not in scope during type checking, but it passed the renamer2019-07-07T18:28:23ZdarchonInternal error: not in scope during type checking, but it passed the renamerWhile trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )
NotInScope.hs:22:20: error:
• GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,
a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,
a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,
a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,
r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]
• In the kind ‘b’
In the definition of data constructor ‘Lgo1KindInference’
In the data declaration for ‘Lgo1’
```
for the following code:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
module NotInScope where
import Data.Proxy
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo f z0 xs0 z '[] = z
Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs
```
Note that the above code works fine in GHC 7.10.2.
There are two options to make the code compile on GHC8-rc3:
- Remove the kind annotations on the `forall arg .` binders
- Or make the following changes using TypeInType:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}
module NotInScope where
import Data.Proxy
import GHC.Types
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 a
b
l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 a
b
l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo a
b
f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo a b f z0 xs0 z '[] = z
Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs
```
I'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.
The error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc3 |
| 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":"Internal error: not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:\r\n\r\n{{{\r\n[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )\r\n\r\nNotInScope.hs:22:20: error:\r\n • GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,\r\n a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,\r\n a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,\r\n a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,\r\n r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]\r\n • In the kind ‘b’\r\n In the definition of data constructor ‘Lgo1KindInference’\r\n In the data declaration for ‘Lgo1’\r\n}}}\r\n\r\nfor the following code:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo f z0 xs0 z '[] = z\r\n Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nNote that the above code works fine in GHC 7.10.2.\r\n\r\nThere are two options to make the code compile on GHC8-rc3:\r\n* Remove the kind annotations on the {{{forall arg .}}} binders\r\n* Or make the following changes using TypeInType:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\nimport GHC.Types\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo a\r\n b\r\n f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo a b f z0 xs0 z '[] = z\r\n Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nI'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.\r\nThe error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.","type_of_failure":"OtherFailure","blocking":[]} -->While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )
NotInScope.hs:22:20: error:
• GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,
a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,
a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,
a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,
r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]
• In the kind ‘b’
In the definition of data constructor ‘Lgo1KindInference’
In the data declaration for ‘Lgo1’
```
for the following code:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
module NotInScope where
import Data.Proxy
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo f z0 xs0 z '[] = z
Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs
```
Note that the above code works fine in GHC 7.10.2.
There are two options to make the code compile on GHC8-rc3:
- Remove the kind annotations on the `forall arg .` binders
- Or make the following changes using TypeInType:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}
module NotInScope where
import Data.Proxy
import GHC.Types
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 a
b
l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 a
b
l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo a
b
f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo a b f z0 xs0 z '[] = z
Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs
```
I'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.
The error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc3 |
| 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":"Internal error: not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:\r\n\r\n{{{\r\n[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )\r\n\r\nNotInScope.hs:22:20: error:\r\n • GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,\r\n a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,\r\n a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,\r\n a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,\r\n r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]\r\n • In the kind ‘b’\r\n In the definition of data constructor ‘Lgo1KindInference’\r\n In the data declaration for ‘Lgo1’\r\n}}}\r\n\r\nfor the following code:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo f z0 xs0 z '[] = z\r\n Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nNote that the above code works fine in GHC 7.10.2.\r\n\r\nThere are two options to make the code compile on GHC8-rc3:\r\n* Remove the kind annotations on the {{{forall arg .}}} binders\r\n* Or make the following changes using TypeInType:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\nimport GHC.Types\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo a\r\n b\r\n f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo a b f z0 xs0 z '[] = z\r\n Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nI'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.\r\nThe error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/11811GHC sometimes misses a CUSK2019-07-07T18:28:26ZRichard Eisenbergrae@richarde.devGHC sometimes misses a CUSK```
{-# LANGUAGE TypeInType #-}
data Test (a :: x) (b :: x) :: x -> *
where K :: Test Int Bool Double
```
fails, because GHC thinks that `Test` does not have a CUSK.
It should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.
Fix en route.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"GHC sometimes misses a CUSK","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Test (a :: x) (b :: x) :: x -> *\r\n where K :: Test Int Bool Double\r\n}}}\r\n\r\nfails, because GHC thinks that `Test` does not have a CUSK.\r\n\r\nIt should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.\r\n\r\nFix en route.","type_of_failure":"OtherFailure","blocking":[]} -->```
{-# LANGUAGE TypeInType #-}
data Test (a :: x) (b :: x) :: x -> *
where K :: Test Int Bool Double
```
fails, because GHC thinks that `Test` does not have a CUSK.
It should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.
Fix en route.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"GHC sometimes misses a CUSK","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Test (a :: x) (b :: x) :: x -> *\r\n where K :: Test Int Bool Double\r\n}}}\r\n\r\nfails, because GHC thinks that `Test` does not have a CUSK.\r\n\r\nIt should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.\r\n\r\nFix en route.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11785Merge types and kinds in Template Haskell2019-07-07T18:28:33ZRichard Eisenbergrae@richarde.devMerge types and kinds in Template Haskell!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kinds should be treated like types in TcSplice","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.","type_of_failure":"OtherFailure","blocking":[]} -->!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kinds should be treated like types in TcSplice","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/11754Error in optCoercion2019-07-07T18:28:42ZSimon Peyton JonesError in optCoercionThis program fails Lint after a run of the simplifier.
```hs
{-# LANGUAGE TypeOperators, UndecidableSuperClasses, KindSignatures, TypeFamilies, FlexibleContexts #-}
module T11728a where
import Data.Kind
import Data.Void
newtype K a x = K a
newtype I x = I x
data (f + g) x = L (f x) | R (g x)
data (f × g) x = f x :×: g x
class Differentiable (D f) => Differentiable f where
type D (f :: Type -> Type) :: Type -> Type
instance Differentiable (K a) where
type D (K a) = K Void
instance Differentiable I where
type D I = K ()
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ + f₂) where
type D (f₁ + f₂) = D f₁ + D f₂
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ × f₂) where
type D (f₁ × f₂) = (D f₁ × f₂) + (f₁ × D f₂)
```
Originally reported in #11728, but it's a totally different problem.
Richard has nailed it already... patch coming from him.This program fails Lint after a run of the simplifier.
```hs
{-# LANGUAGE TypeOperators, UndecidableSuperClasses, KindSignatures, TypeFamilies, FlexibleContexts #-}
module T11728a where
import Data.Kind
import Data.Void
newtype K a x = K a
newtype I x = I x
data (f + g) x = L (f x) | R (g x)
data (f × g) x = f x :×: g x
class Differentiable (D f) => Differentiable f where
type D (f :: Type -> Type) :: Type -> Type
instance Differentiable (K a) where
type D (K a) = K Void
instance Differentiable I where
type D I = K ()
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ + f₂) where
type D (f₁ + f₂) = D f₁ + D f₂
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ × f₂) where
type D (f₁ × f₂) = (D f₁ × f₂) + (f₁ × D f₂)
```
Originally reported in #11728, but it's a totally different problem.
Richard has nailed it already... patch coming from him.8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11732Deriving Generic1 interacts poorly with TypeInType2019-07-07T18:28:52ZRichard Eisenbergrae@richarde.devDeriving Generic1 interacts poorly with TypeInTypeFrom \@RyanGlScott, [ticket:11357\#comment:117922](https://gitlab.haskell.org//ghc/ghc/issues/11357#note_117922):
Vanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered "instantiated" in a `Generic1` instance. For instance, this is rejected:
```
λ> data Proxy k (a :: k) = ProxyCon deriving Generic1
```
```
<interactive>:32:43: error:
• Can't make a derived instance of ‘Generic1 (Proxy *)’:
Proxy must not be instantiated; try deriving `Proxy k a' instead
• In the data declaration for ‘Proxy’
```
And rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!
```
λ> data family ProxyFam (a :: y) (b :: z)
λ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1
==================== Derived instances ====================
Derived instances:
instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where
...
```
\[Ryan needs\] to investigate further to see why this is the case.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Deriving Generic1 interacts poorly with TypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Generics","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From @RyanGlScott, comment:9:ticket:11357:\r\n\r\nVanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered \"instantiated\" in a `Generic1` instance. For instance, this is rejected:\r\n\r\n{{{\r\nλ> data Proxy k (a :: k) = ProxyCon deriving Generic1\r\n}}}\r\n\r\n{{{\r\n<interactive>:32:43: error:\r\n • Can't make a derived instance of ‘Generic1 (Proxy *)’:\r\n Proxy must not be instantiated; try deriving `Proxy k a' instead\r\n • In the data declaration for ‘Proxy’\r\n}}}\r\n\r\nAnd rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!\r\n\r\n{{{\r\nλ> data family ProxyFam (a :: y) (b :: z)\r\nλ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1\r\n\r\n==================== Derived instances ====================\r\nDerived instances:\r\n instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where\r\n ...\r\n}}}\r\n\r\n[Ryan needs] to investigate further to see why this is the case. ","type_of_failure":"OtherFailure","blocking":[]} -->From \@RyanGlScott, [ticket:11357\#comment:117922](https://gitlab.haskell.org//ghc/ghc/issues/11357#note_117922):
Vanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered "instantiated" in a `Generic1` instance. For instance, this is rejected:
```
λ> data Proxy k (a :: k) = ProxyCon deriving Generic1
```
```
<interactive>:32:43: error:
• Can't make a derived instance of ‘Generic1 (Proxy *)’:
Proxy must not be instantiated; try deriving `Proxy k a' instead
• In the data declaration for ‘Proxy’
```
And rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!
```
λ> data family ProxyFam (a :: y) (b :: z)
λ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1
==================== Derived instances ====================
Derived instances:
instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where
...
```
\[Ryan needs\] to investigate further to see why this is the case.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Deriving Generic1 interacts poorly with TypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Generics","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From @RyanGlScott, comment:9:ticket:11357:\r\n\r\nVanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered \"instantiated\" in a `Generic1` instance. For instance, this is rejected:\r\n\r\n{{{\r\nλ> data Proxy k (a :: k) = ProxyCon deriving Generic1\r\n}}}\r\n\r\n{{{\r\n<interactive>:32:43: error:\r\n • Can't make a derived instance of ‘Generic1 (Proxy *)’:\r\n Proxy must not be instantiated; try deriving `Proxy k a' instead\r\n • In the data declaration for ‘Proxy’\r\n}}}\r\n\r\nAnd rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!\r\n\r\n{{{\r\nλ> data family ProxyFam (a :: y) (b :: z)\r\nλ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1\r\n\r\n==================== Derived instances ====================\r\nDerived instances:\r\n instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where\r\n ...\r\n}}}\r\n\r\n[Ryan needs] to investigate further to see why this is the case. ","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11719Cannot use higher-rank kinds with type families2019-07-07T18:28:55ZOllie CharlesCannot use higher-rank kinds with type familiesThis ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell-cafe/2016-March/123462.html
Here's the code that should work, but doesn't:
```hs
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
type family (f :: a ~> b) @@ (x :: a) :: b
data Null a = Nullable a | NotNullable a
type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where
(f ∘ g) x = f @@ (g @@ x)
type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :(
-- BaseType k x = (@@) k x
```This ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell-cafe/2016-March/123462.html
Here's the code that should work, but doesn't:
```hs
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
type family (f :: a ~> b) @@ (x :: a) :: b
data Null a = Nullable a | NotNullable a
type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where
(f ∘ g) x = f @@ (g @@ x)
type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :(
-- BaseType k x = (@@) k x
```8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/11716Make TypeInType stress test work2019-07-07T18:28:57ZRichard Eisenbergrae@richarde.devMake TypeInType stress test workI used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Make TypeInType stress test work","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.","type_of_failure":"OtherFailure","blocking":[]} -->I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Make TypeInType stress test work","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11699Type families mistakingly report kind variables as unbound type variables2019-07-07T18:29:02ZmniipType families mistakingly report kind variables as unbound type variablesGHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.
Simplest test case:
```hs
{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family F a where F (f a) = f a
```
As seen on 8.0.1-rc2 and 7.10.2:
```
../File.hs:3:23:
Family instance purports to bind type variable ‘k1’
but the real LHS (expanding synonyms) is: F (f a) = ...
In the equations for closed type family ‘F’
In the type family declaration for ‘F’
```
The culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.
Now, I'm not too sure whether this is a "GHC rejects valid program", or "Incorrect warning at compile time", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)
<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":"Type families mistakingly report kind variables as unbound type variables","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 verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.\r\n\r\nSimplest test case:\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, PolyKinds #-}\r\ntype family F a where F (f a) = f a\r\n}}}\r\nAs seen on 8.0.1-rc2 and 7.10.2:\r\n{{{\r\n../File.hs:3:23:\r\n Family instance purports to bind type variable ‘k1’\r\n but the real LHS (expanding synonyms) is: F (f a) = ...\r\n In the equations for closed type family ‘F’\r\n In the type family declaration for ‘F’\r\n}}}\r\n\r\nThe culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.\r\n\r\nNow, I'm not too sure whether this is a \"GHC rejects valid program\", or \"Incorrect warning at compile time\", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)","type_of_failure":"OtherFailure","blocking":[]} -->GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.
Simplest test case:
```hs
{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family F a where F (f a) = f a
```
As seen on 8.0.1-rc2 and 7.10.2:
```
../File.hs:3:23:
Family instance purports to bind type variable ‘k1’
but the real LHS (expanding synonyms) is: F (f a) = ...
In the equations for closed type family ‘F’
In the type family declaration for ‘F’
```
The culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.
Now, I'm not too sure whether this is a "GHC rejects valid program", or "Incorrect warning at compile time", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)
<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":"Type families mistakingly report kind variables as unbound type variables","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 verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.\r\n\r\nSimplest test case:\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, PolyKinds #-}\r\ntype family F a where F (f a) = f a\r\n}}}\r\nAs seen on 8.0.1-rc2 and 7.10.2:\r\n{{{\r\n../File.hs:3:23:\r\n Family instance purports to bind type variable ‘k1’\r\n but the real LHS (expanding synonyms) is: F (f a) = ...\r\n In the equations for closed type family ‘F’\r\n In the type family declaration for ‘F’\r\n}}}\r\n\r\nThe culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.\r\n\r\nNow, I'm not too sure whether this is a \"GHC rejects valid program\", or \"Incorrect warning at compile time\", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev